*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Generalized elimination rule?*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Fri, 26 Feb 2010 09:21:18 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B86BBA6.803@uni-muenster.de>*References*: <4B86BBA6.803@uni-muenster.de>

I second this request. More precisely, I'd like to be able to annotate a rule such that it is applied by the automatic proof methods only if the first n hypotheses are present in the current proof state. As a simple example, consider bspec, which would make a perfect elimination rule when its two assumptions can be proved by assumption. As others have pointed out, it is not hard to write a tactic that applies a rule only if the first n hypotheses can be proved by assumption, however, I don't know how to make such a tactic work inside auto and friends. Thanks, Stephan On 25 Feb 2010, at 19:04, Peter Lammich 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 > > 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. > > (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 > > >

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

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

- Previous by Date: Re: [isabelle] Locale import
- 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