# Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 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.
```
```
```
Thanks! Grepping the *.thy source files has been very useful for me so far. Actually the only reason why I ended up in the ML sources was that in the theory sources there was a lot of "noise" from this rule being _applied_, so I just overlooked the lemma.
```
```
```There are two better methods:
```
```
```
Thanks a lot – very helpful. As a newbie, obviously, I knew neither of them.
```
```
```  * use find_theorems
like: find_theorems "_ > _ ==> _ >= _"
```
```                           ^
```
I think here it expects a numeric argument as said below; didn't work without.
```
```
```…
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)
```
```
```
BTW in the documentation find_theorems is only mentioned in prog-prove.pdf (just searched all files with pdfgrep), and there it says:
```
--- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< --- %< ---
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.

```
Generally, I had no idea that one can apply _any_ theorem using (rule name_of_theorem). This wasn't obvious to me, and instead I had thought that "rules" are something special that's built in at the level of "a calculus for a logic".
```
```
```  * 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.
```
```

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:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.