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

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

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