Re: [isabelle] efficiency



On Friday 27 October 2006 10:31, Julien wrote:
> I am trying to prove a goal P knowing:
>
> a implies P ; b implies P ;  c implies P ; a \/ b \/ c
>
> Each term a, b and c are of the form u /\ v.
> The conclusion P is of the form u /\ (x \/ y \/ z ...).
> But this should not matter for the proof.
>
> With small formulae, auto or force work. But otherwise they both never
> terminate.

Try

lemma "[| a --> P; b --> P; c --> P; a | b | c --> P |]" ==> P
  by ((erule disjE)?, erule mp, assumption)+

Best,
Tjark





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