*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Date*: Fri, 10 Aug 2012 13:24:23 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <1344594145.1841.79.camel@macbroy12.informatik.tu-muenchen.de>*Organization*: University of Birmingham*References*: <5024ABB2.8010900@cs.bham.ac.uk> <CAAMXsiayP7z=SKiXA3bhQ0iav_AMqdJDEU+itHRTKTgOMGZs-w@mail.gmail.com> <5024DD89.3010508@cs.bham.ac.uk> <1344594145.1841.79.camel@macbroy12.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120720 Thunderbird/14.0

2012-08-10 12:22 Johannes Hölzl:

Am Freitag, den 10.08.2012, 12:08 +0200 schrieb Christoph LANGE:2012-08-10 10:15 Brian Huffman:by (rule less_imp_le)… 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 "_ > _ ==> _ >= _"

^

… 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)

--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- Command find_theorems searches for specific theorems in the current theory. Search criteria include pattern matching on terms and on names. For details see the Isabelle/Isar Reference Manual [4]. --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- … but the reference manual does't mention it.

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

Excellent, very helpful too! Cheers, 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**:

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

**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Johannes Hölzl

- Previous by Date: Re: [isabelle] Parametricity as a poor man's dependent typing
- 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