*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Tue, 09 Mar 2010 18:04:39 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Brian Huffman <brianh at cs.pdx.edu>*In-reply-to*: <4B870B93.1030904@rsise.anu.edu.au>*References*: <4B86BBA6.803@uni-muenster.de> <cc2478ab1002251054r16465cc0t1f7be1a9ad9a44f2@mail.gmail.com> <4B870B93.1030904@rsise.anu.edu.au>*User-agent*: Thunderbird 2.0.0.22 (X11/20090625)

Hi Brian, Many thanks you for your answer.

val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ; produces premises that are doubly-wrapped into keep. What's the best way around? Only counting "plain" premises? (How?) Can keepI be defined to also wrap higher-order premises? Best, Peter Jeremy Dawson schrieb:

Brian, Peter, et al,My solution of this "tricky bit" depends on an idea presented byKonrad Slindfor HOL at TPHOLs 2002, which was to annotate selected goals (or, moregenerally, subterms) _within_ the logic.For this problem I defined keep_def : "keep b f == f" keep :: "bool => 'a => 'a" val _ = ListPair.app bind_thm (["keepD", "keepI"], [keep_def] RL defDs) ; val _ = bind_thm ("keepTD", read_instantiate [("b", "True")] keepD) ; val _ = bind_thm ("keepFD", read_instantiate [("b", "False")] keepD) ; val _ = bind_thm ("keepF_thin", keepFD RS thin_rl) ; > keepTD ; val it = "keep True ?P ==> ?P" : Thm.thm > keepFD ; val it = "keep False ?P ==> ?P" : Thm.thm > keepF_thin ; val it = "[| keep False ?P; PROP ?W |] ==> PROP ?W" : Thm.thm (You should change the uses of bind_thm if you're using Isar).Then the tactic is as follows - it is no doubt rather inefficient, butseems to work OK.I've done the analogue of fatac which deletes all matched premisesfrom remaining subgoals because it's simpler to follow (datac alreadydeleted the first matched premise, and eatac also matches theconclusion, which I think is here an additional irrelevant complication).(* fetac : thm -> int -> int -> tactic like fatac n but also deletes hypotheses matched *) fun fetac th n sg st = let val fth = thin_rl RS (replicate n keepFD MRS th) : thm ; val subgoal = List.nth (prems_of st, sg - 1) : term ; (* turn all subgoal hypotheses H into keep ?b H *) val nhyps = length (Logic.strip_assums_hyp subgoal) ; val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ; (* then apply ftac fth - see later *) (* then apply atac n times, which marks the hypotheses to be deleted with keep False *) val atacs = EVERY' (replicate n atac) ; (* treat other instances of keep ?b as keep True, and erase them *) val ekttac = REPEAT o dtac keepTD : int -> tactic ; (* delete hypotheses which are (keep False ...) *) val ekftac = REPEAT o etac keepF_thin : int -> tactic ; (* combine all the above *)val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW(ekttac THEN' ekftac) : int -> tactic ;in ctac sg st end ;Unfortunately, most of the development effort now is focused on Isar-style proofs with chained facts, and not so much on tactics for apply-style proofs. So I'd say it is unlikely that this feature will be implemented by the main Isabelle development team. But be sure to report back if you try to implement this yourself; I'm sure plenty of people would find it useful.I hope so. Incidentally, on a related topic - sometimes using etac I_don't_ want the matched premise deleted from the resulting subgoals(which is why all_dupE is given as an alternative to allE).To achieve this for any elimination rule, I have fun mk_dupE thE = zero_var_indexes (rotate_prems ~1 (tacsthm [PRIMITIVE (fn th => th RS cut_rl), atac 1] thE)) ; thus mk_dupE allE is approximately all_dupE Regards, Jeremy- Brian

**Follow-Ups**:**Re: [isabelle] Generalized elimination rule?***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] Question about classes
- Next by Date: [isabelle] bijections to/from the natural numbers
- Previous by Thread: Re: [isabelle] Error when using \<sqinter> instead of inf
- Next by Thread: Re: [isabelle] Generalized elimination rule?
- Cl-isabelle-users March 2010 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