*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*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Fri, 10 Aug 2012 12:22:25 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5024DD89.3010508@cs.bham.ac.uk>*Organization*: Technische Universität München*References*: <5024ABB2.8010900@cs.bham.ac.uk> <CAAMXsiayP7z=SKiXA3bhQ0iav_AMqdJDEU+itHRTKTgOMGZs-w@mail.gmail.com> <5024DD89.3010508@cs.bham.ac.uk>

Am Freitag, den 10.08.2012, 12:08 +0200 schrieb Christoph LANGE: > 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. The theories are documented in http://isabelle.in.tum.de/dist/library/HOL/Orderings.html but this is neither searchable nor very readable. There are two better methods: * use find_theorems like: find_theorems "_ > _ ==> _ >= _" This is fast, but the result depends very strong on the pattern you are searching for. General rule: give a list of constants and not more: find_theorems (200) "_ > _" "_ >= _" name: Ord (the (200) tells find theorem to list the first 200 results) * use sledgehammer: lemma "(x::real) > 0 --> x >= 0" sledgehammer This will now try to find a proof for this. The proof will contain the necessary lemmas. - Johannes > 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 >

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