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