Re: [isabelle] Tactic for Eliminating Parameters Wanted ...



Dear Burkhart,

I normally use apply(unfold triv_forall_equality) to get rid of all irrelevant parameters.

Best,
Andreas

On 26/02/15 12:55, Burkhart Wolff wrote:
Dear all,

is there any way to actually eliminate a parameter or a goal ?

After case-splits, parameters are often no longer of relevance.


MY PROBLEM:
============

I have something like:

"âS. PUT (S::(...) actionâiâpâc)â

which I reduce via case-splitting to:

"(âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)â

which I would like to reduce to:

"(â ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)â

(so canceling the parameter S irrelevant in the goal).


SOME ELEMENTS OF A SOLUTION:
I cooked up some sketch of a tactics which does nearly what I want:


ML{* val XX = Unsynchronized.ref(@{thm impI})
      fun PEEK st = (XX:=st; all_tac st)
*}
lemma "âS. PUT (S::(...) actionâiâpâc)"
apply(tactic "Induct_Tacs.case_tac @{context} \"S\" 1", hypsubst)
apply(tactic "PEEK")
oops
ML{* val st = !XX;
      val thy = #thy (rep_thm (st));
      val _ $ (_ $ Abs(x,ty,t))  = concl_of(st);
      val cFree = cterm_of thy (Free(x,ty))
*}
ML{* val _ $ Abs(ss,_,T) = term_of (cprem_of (st) 1) ;
      val T' =  cterm_of thy (subst_bounds([Bound 0],T)) *}

ML{* val Q  = Thm.assume T'*}
ML{* val Q' = Thm.forall_intr cFree  (Q) ; *}
ML{* val Q'' = Thm.implies_intr T' Q'*}
ML{* val Q''' = Q'' RS (st)*}

Unfortunately, the very last composition step fails:
exception THM 1 raised (line 332 of "drule.ML"):
   RSN: no unifiers
   (âipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â
   (âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction))
   (âS ipc_stage ipc_direction. PUT (IPC ipc_stage ipc_direction)) â (âS. PUT S)

which looks bizarre. The types and class types are confrom.


Any ideas ?


Best

bu








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.