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