Re: [isabelle] A proof for existential

There is a parse problem with your axioms ax1 and ax2. I am assuming that by => you mean the operator --> which is the implication operator of HOL.

If so, the problem is that your goal is false. The real problem is that your second axiom is a truism. It says there exists an x which is a zero of g if it is a strict maximum of h. In fact there always exist infinitely many x which satisfy this property - they may not be zeroes of g, but they are not the strict maximum of h.

From: cl-isabelle-users-bounces at [cl-isabelle-users-bounces at] On Behalf Of munddr at [munddr at]
Sent: Wednesday, August 04, 2010 4:29 AM
To: isabelle-users at
Subject: [isabelle] A proof for existential

Hi all,

I've been stuck trying to find a proof for the following, could someone
please shed some light?

f :: "real => real" and
g :: "real => real" and
h :: "real => real" where
ax1: "EX x. ALL y. x ~= y => hx > h y" and
ax2 :"EX x. (ALL y. x ~= y => hx > hy) => gx = 0"

lemma "EX x. gx = 0"

I've tried:

lemma "EX x. gx = 0"
using ax1 ax2
apply (intro exI)
apply (erule exE)+
apply (erule allE)
apply (erule impE)

which gives 2 subgoals, but they don't seem to be in the right direction...

Thanks for the help in advance.


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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