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



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?

Cheers, and thanks,

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





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