[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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and