# Re: [isabelle] Generalized elimination rule?

```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
>
>
>

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.