*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Tactic for Eliminating Parameters Wanted ...*From*: Jeremy Dawson <Jeremy.Dawson at anu.edu.au>*Date*: Thu, 26 Feb 2015 23:43:50 +1100*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=Jeremy.Dawson@anu.edu.au;*In-reply-to*: <DA9EE04C-C629-488B-B0F4-782218F1B237@lri.fr>*References*: <DA9EE04C-C629-488B-B0F4-782218F1B237@lri.fr>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.3.0

Hi Burkhart,

triv_forall_equality ; val it = "(!!x. PROP ?V) == PROP ?V" : Thm.thm

Cheers, Jeremy On 26/02/15 22: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

**References**:**[isabelle] Tactic for Eliminating Parameters Wanted ...***From:*Burkhart Wolff

- Previous by Date: Re: [isabelle] Tactic for Eliminating Parameters Wanted ...
- Next by Date: Re: [isabelle] Trying to instantiate a class
- Previous by Thread: Re: [isabelle] Tactic for Eliminating Parameters Wanted ...
- Next by Thread: [isabelle] change proposal: eliminating overloading for factorials
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list