*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Fri, 26 Feb 2010 10:45:23 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Peter Lammich <peter.lammich at uni-muenster.de>*In-reply-to*: <cc2478ab1002251054r16465cc0t1f7be1a9ad9a44f2@mail.gmail.com>*References*: <4B86BBA6.803@uni-muenster.de> <cc2478ab1002251054r16465cc0t1f7be1a9ad9a44f2@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

Brian Huffman wrote:

On Thu, Feb 25, 2010 at 10:04 AM, Peter Lammich <peter.lammich at uni-muenster.de> wrote:Hi all, I'm curious whether it is (easily) possible to apply elimination rules in Isabelle that eliminate more than one premise.[...]

I don't think there is any easy way to accomplish what you want to do---at least, I don't know of any already-implemented tactic in Isabelle that does this. I do think such a tactic would be useful, though; I've wished for it a few times myself. It might be possible to implement such a tactic in ML. The obvious approach of trying to generalize eresolve_tac probably won't work, because eresolve_tac is implemented in terms of Thm.biresolution, which is part of Isabelle's trusted kernel. You could probably define this tactic on top of eresolve_tac: Basically you would do "erule (n)" (which is basically "erule" then "assumption" n times) followed by n calls to "thin_tac" to eliminate the extra assumptions from the final proof state. The tricky bit would be to figure out how to record which assumptions were matched by "assumption", so you can tell "thin_tac" which ones to get rid of later.

Brian, Peter, et al,

Thus for a long time I have used forget :: "'a => 'a" forget_def : "forget f == f"

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).

(* 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 *)

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.

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

**References**:**[isabelle] Generalized elimination rule?***From:*Peter Lammich

**Re: [isabelle] Generalized elimination rule?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Setting up a logic: need instructions.
- Next by Date: Re: [isabelle] Locale import
- Previous by Thread: Re: [isabelle] Generalized elimination rule?
- Next by Thread: Re: [isabelle] Generalized elimination rule?
- Cl-isabelle-users February 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