*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 25 Feb 2010 10:54:19 -0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B86BBA6.803@uni-muenster.de>*References*: <4B86BBA6.803@uni-muenster.de>*Sender*: huffman.brian.c at gmail.com

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. > > There is a consumes-flag for cases rules, however, simply doing: > > lemma AB_elim[consumes 2]: "[| A; B; Foo => thesis |] ==> thesis" > > lemma "[| A; B; C |] ==> Foo" > apply (cases rule: AB_elim) > > does not work, and leaves me with three subgoals, the last one being: > [|A; B; C; Foo |] ==> Foo > > apply (erule (1) AB_elim) leaves me with one subgoal being: > [| B; C; Foo |] ==> Foo > > However, I want something that yields the subgoal: > [| C; Foo |] ==> Foo Hi Peter, The "consumes" attribute only has an effect when you are in an Isar-style proof with chained facts. Here's a situation where it works as you expect: lemma "[|A; B; C|] ==> Foo" proof - assume "A" and "B" and "C" then show "Foo" (* there are now 3 chained facts: "A", "B", "C" *) apply (cases rule: AB_elim) Now the first 2 chained facts are matched with rule AB_elim and disappear. The remaining fact "C" stays in the remaining subgoal, leaving "[| C; Foo |] ==> Foo". > and that also works if the A and B are not in order, i.e. for > [| ...; B; ...; A; ... |] ==> Foo > apply (?? AB_elim) shall yield: > [| ...; ...; ...; Foo |] ==> Foo > i.e. removing the matching A and B from the premises. Unfortunately, chained facts can only be matched in the given order (for efficiency reasons, I believe), so this doesn't really do what you want. > (I need this for termination and proper behavior of a set of elimination > rules that I apply exhaustively with apply (...)+ ): > > Regards and thanks for any hints, > Peter 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. 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. - Brian

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

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

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