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"
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.
TIMOTHY KREMANN wrote:
"[| 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))"
Can someone suggest an Isar equivalent for the above proof?
This archive was generated by a fusion of
Pipermail (Mailman edition) and