Re: [isabelle] Isar Proof



I know this is not what you asked. But this goal can also be solved automatically by the recent tactic "metis"

apply (metis)

although not by the older tactics blast and fast. The drawback of metis is that you have to give it explicitly any additional lemmas beyond pure logic that are needed. Here there are none.

Tobias

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
Can someone suggest an Isar equivalent for the above proof?
Thanks,
Tim





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