*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*: Brian Huffman <huffman at in.tum.de>*Date*: Fri, 10 Aug 2012 12:22:32 +0200*Cc*: Colin Rowat <c.rowat at bham.ac.uk>, Manfred Kerber <M.Kerber at cs.bham.ac.uk>, 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>

On Fri, Aug 10, 2012 at 12:08 PM, Christoph LANGE <c.lange at cs.bham.ac.uk> 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? Scanning the *ML* sources is probably not very useful. If you want to familiarize yourself with the set of available theorems, it is better to browse the .thy files in src/HOL (most lemmas about < and <= are in Orderings.thy) or else browse the generated pdf documentation for Isabelle/HOL (follow "document" or "outline" link from https://isabelle.in.tum.de/dist/library/HOL/index.html). If you are looking for a specific lemma, you should definitely learn the "find_theorems" command. See e.g. section 3.1.11 of the "Tutorial on Isabelle/HOL". - Brian

**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] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- 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