*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] A proof for existential*From*: John Munroe <munddr at gmail.com>*Date*: Wed, 4 Aug 2010 09:32:04 +0100*In-reply-to*: <AANLkTin8WTbEfhLpVFd6Mx2UxAku+1Dv-wrAzWSBsOHJ@mail.gmail.com>*References*: <0015174be6a81d7e5d048cef80e6@google.com> <2EB36A07AAE8C44BBB1986425E7A22D0127DFE1328@atp-mbx1.in.nicta.com.au> <AANLkTin8WTbEfhLpVFd6Mx2UxAku+1Dv-wrAzWSBsOHJ@mail.gmail.com>

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

**References**:**[isabelle] A proof for existential***From:*munddr

**Re: [isabelle] A proof for existential***From:*Thomas Sewell

- Previous by Date: Re: [isabelle] A proof for existential
- Next by Date: Re: [isabelle] A proof for existential
- Previous by Thread: Re: [isabelle] A proof for existential
- Next by Thread: Re: [isabelle] A proof for existential
- Cl-isabelle-users August 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list