*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 10 Aug 2012 11:22:51 +0100*Cc*: Colin Rowat <c.rowat at bham.ac.uk>, Manfred Kerber <M.Kerber at cs.bham.ac.uk>, Brian Huffman <huffman at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5024DD89.3010508@cs.bham.ac.uk>*References*: <5024ABB2.8010900@cs.bham.ac.uk> <CAAMXsiayP7z=SKiXA3bhQ0iav_AMqdJDEU+itHRTKTgOMGZs-w@mail.gmail.com> <5024DD89.3010508@cs.bham.ac.uk>

The real difficulty here is that you are using assumes/shows. Then the assumption "x > 0" isn't explicitly part of the subgoal and isn't visible to Isabelle's automation. The one exception is sledgehammer, which sees everything, and instantly finds a proof. It would be better to state your problem more simply as follows: lemma greater_zero_implies_greater_equal_zero [simp] : fixes x::real shows "x > 0 \<Longrightarrow> x \<ge> 0" Or even more simply like this: lemma greater_zero_implies_greater_equal_zero [simp] : "(x::real) > 0 \<Longrightarrow> x \<ge> 0" Then almost anything will solve it: auto, simp, arith, force. I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time. Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule. It will be quite generally applicable, and could increase your simplification time or even (together with similarly general conditional rewrite rules) cause looping. Larry Paulson On 10 Aug 2012, at 11:08, Christoph LANGE wrote: > Dear Brian, > > 2012-08-10 10:15 Brian Huffman: >>> somewhere in a proof that involves real numbers from the theory "Real" I >>> would like to infer "(x::real) >= 0" from "x > 0". >>> >>> … >> >> by (rule less_imp_le) > > excellent, thanks a lot for your quick reply! > > Generally, when similar situations occur in future: Is there any documentation of such rules? In the manuals that come with Isabelle I didn't find anything. > > I see that this particular rule and similar ones are documented reasonably well by the comments in src/Provers/order.ML So would you generally suggest scanning the sources for applicable rules, or is there a nicer overview? > > Cheers, and thanks, > > Christoph > > -- > Christoph Lange, School of Computer Science, University of Birmingham > http://cs.bham.ac.uk/~langec, Skype duke4701 > > → Building & Exploring Web Based Environments. Seville, Spain, 27 Jan– > 1 Feb 2013. Deadline 2 Sep. http://iaria.org/conferences2013/WEB13.html >

**Follow-Ups**:**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Christoph LANGE

**References**:**[isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Christoph LANGE

**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Brian Huffman

**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Christoph LANGE

- Previous by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Date: Re: [isabelle] Parametricity as a poor man's dependent typing
- Previous by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Cl-isabelle-users August 2012 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