*To*: Michael Daniels <dayzman at gmail.com>*Subject*: Re: [isabelle] Proving lemmas containing a squareroot*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 4 Jun 2010 07:36:33 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTintDKxYCcQNGUIuYAANd65eAdQqmnHc4SMyMpf5@mail.gmail.com>*References*: <AANLkTintDKxYCcQNGUIuYAANd65eAdQqmnHc4SMyMpf5@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Thu, Jun 3, 2010 at 9:15 PM, Michael Daniels <dayzman at gmail.com> wrote: > Hi > > I'm hoping some of you could help me with the following lemma: ... > lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b" > using gt > sledgehammer; > > It seems like a rather simple lemma but sledgehammer (E, SPASS, and > Vampire) can't seem to return the set of theorems for metis. Does > anyone know how to prove it? This lemma rt4 is obviously false. Consider the case where a and b are equal. lemma rt4_wrong: "~ (ALL a b. sqrt(4) / pl a > sqrt(4) / pl b)" apply simp apply (rule exI [where x=1]) apply (rule exI [where x=1]) apply simp done Perhaps you meant "EX a b. sqrt(4) / pl a > sqrt(4) / pl b" ? - Brian

**Follow-Ups**:**Re: [isabelle] Proving lemmas containing a squareroot***From:*Michael Daniels

**References**:**[isabelle] Proving lemmas containing a squareroot***From:*Michael Daniels

- Previous by Date: [isabelle] Translating syntactic sugar
- Next by Date: Re: [isabelle] Proving lemmas containing a squareroot
- Previous by Thread: Re: [isabelle] Proving lemmas containing a squareroot
- Next by Thread: Re: [isabelle] Proving lemmas containing a squareroot
- Cl-isabelle-users June 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