Re: [isabelle] A proof for existential
On Thu, 2010-08-05 at 11:19 +0100, John Munroe wrote:
> Thanks for the reply. What if ax2 was ax2 :"ALL x. (ALL y. x ~= y -->
> h x > h y) --> g x = 0", would the lemma follow from ax1 and ax2 then?
Yes; see the attached Isabelle theory for an automatic proof.
theory John imports Complex_Main
f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y --> h x > h y" and
ax2: "ALL x. (ALL y. x ~= y --> h x > h y) --> g x = 0"
lemma "EX x. g x = 0"
by (metis ax1 ax2)
This archive was generated by a fusion of
Pipermail (Mailman edition) and