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.

Yours,
    Thomas.
________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of munddr at gmail.com [munddr at gmail.com]
Sent: Wednesday, August 04, 2010 4:29 AM
To: isabelle-users at cl.cam.ac.uk
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?

axiomatization
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"
oops

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.

Thanks
John

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.