# Re: [isabelle] Isar Proof

```       Or else using guess (with a good dose of auto :) ...

lemma
assumes all: "ALL x . (P (x::'a) \<longrightarrow> \<not> Q x) \<and> (P x \<longrightarrow> \<not> R x) \<and> (Q x \<longrightarrow> \<not> R x)"
and     eP:  "EX x .  P x" and eQ: "EX x . Q x" and eR: "EX x . R x"
shows  "EX x y z. (\<not>((x::'a) = y) \<and> \<not>( x = z) \<and> \<not>( y = z))"
proof -
from eP guess x ..
moreover from eQ guess y ..
moreover from eR guess z ..
ultimately have "x \<noteq> y" and "x \<noteq> z" and "y \<noteq> z" using all by auto
thus ?thesis by auto
qed

Simon

At Wed, 18 Jun 2008 17:16:01 +0930,
"Dr. Brendan Patrick Mahony" <brendan.mahony at dsto.defence.gov.au> wrote:
>
>
> On 18/06/2008, at 8:11 AM, TIMOTHY KREMANN wrote:
>
> > lemma
> > "[| ALL x . (P (x::'a)  =>  ~ Q x)  /\
> >                (P x        => ~ R x) /\
> >               (Q x       =>  ~ R x);
> > EX x .  P x;
> > EX x .  Q x;
> > EX x .  R x|] ==>
> > EX  x y z. (~((x::'a) = y)  /\
> >          ~( x      = z)  /\
> >          ~( y      = z))"
> >  apply(elim ex_forward)
> >  apply(auto)
> > done

```

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