Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and