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.