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.