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
https://isabelle.in.tum.de/dist/library/HOL/index.html).

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
on Isabelle/HOL".

- Brian





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