*To*: Brian Huffman <brianh at cs.pdx.edu>, Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] Proving equivalence*From*: s.wong.731 at gmail.com*Date*: Tue, 25 Jan 2011 21:56:06 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Tjark Weber <webertj at in.tum.de>*In-reply-to*: <0016e6dbe2b3231679049ab23ee9@google.com>

Steve On Jan 25, 2011 9:17pm, s.wong.731 at gmail.com wrote:

Hi,

Thanks for pointing out the inconsistency. Just curious, how could youcould spot the inconsistency? How could "(0::real) = 1" be derived fromthat axiom?

Thanks again

Steve

On Jan 25, 2011 6:11pm, Brian Huffman brianh at cs.pdx.edu> wrote: > Hi Steve, > > > > As Tjark pointed out recently, axioms are evil. It just so happens > > that both of your example axiomatizations are inconsistent. As you can > > see: > > > > lemma "(0::real) = 1" >> > using ax1 by metis > > > > (The same proof works also for ax2.) > > > > This might explain why metis can easily solve your lemma: because from > > ax1 or ax2 metis can prove any equation between real numbers! > > > > - Brian > > > > On Tue, Jan 25, 2011 at 9:18 AM, Tjark Weber webertj at in.tum.de> wrote: > > > Steve, > > > > > > On Tue, 2011-01-25 at 16:51 +0000, Steve W wrote: > > >> Auto can't find a proof. How come this is so difficult for auto? What > > >> is the proper way to do this proof? > > > > > > both "by blast" and "by metis" succeed. I didn't investigate why auto > > > fails. > > > > > > Kind regards, > > > Tjark > > > > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Proving equivalence***From:*Brian Huffman

**References**:**Re: [isabelle] Proving equivalence***From:*s . wong . 731

- Previous by Date: Re: [isabelle] Proving equivalence
- Next by Date: Re: [isabelle] Proving equivalence
- Previous by Thread: Re: [isabelle] Proving equivalence
- Next by Thread: Re: [isabelle] Proving equivalence
- Cl-isabelle-users January 2011 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