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)
> 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.
The theories are documented in
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"
This will now try to find a proof for this.
The proof will contain the necessary lemmas.
> 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and