Re: [isabelle] A proof for existential



On Wed, Aug 4, 2010 at 8:41 AM, Thomas Sewell
<Thomas.Sewell at nicta.com.au> wrote:
> 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.
>

Indeed. Apologies for the typo.

> 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.
>

I'm a bit confused: If ax2 is a truism, why is the goal false? To
prove the goal, wouldn't I need to show that there exists some x which
is a strict maximum of h (ax1)?

Thanks
John

> 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.