# [isabelle] Generalized elimination rule?

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