[isabelle] strange isabelle behaviour



I experienced some strange behaviour when using Isabelle
to check natural deduction proofs for first-order logic.

The following lemma is easily proved:

 lemma "EX y. P(x_0, y) ==> EX x. EX y. P(x, y)" by auto

Hence I thought that every formula that unifies with
the above, would also be provable.
As soon as negations come into play however, I get problems.

 lemma "EX y. ~ x_0 = y ==> EX x. EX y. ~ x = y" by auto

is not accepted. Why is this the case? As far as I'm concerned

 ?P = %(x, y). ~ x = y

unifies the two premises (and conclusions) of the two lemmas.
Thus they should both be provable.

cheers

christian





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