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

The real difficulty here is that you are using assumes/shows. Then the assumption "x > 0" isn't explicitly part of the subgoal and isn't visible to Isabelle's automation. The one exception is sledgehammer, which sees everything, and instantly finds a proof.

It would be better to state your problem more simply as follows:

lemma greater_zero_implies_greater_equal_zero [simp] :
 fixes x::real
 shows  "x > 0 \<Longrightarrow> x \<ge> 0"

Or even more simply like this:

lemma greater_zero_implies_greater_equal_zero [simp] :
  "(x::real) > 0 \<Longrightarrow> x \<ge> 0"

Then almost anything will solve it: auto, simp, arith, force. I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time.

Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule. It will be quite generally applicable, and could increase your simplification time or even (together with similarly general conditional rewrite rules) cause looping.

Larry Paulson

On 10 Aug 2012, at 11:08, Christoph LANGE 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?
> Cheers, and thanks,
> Christoph
> -- 
> Christoph Lange, School of Computer Science, University of Birmingham
>, Skype duke4701
> → Building & Exploring Web Based Environments.  Seville, Spain, 27 Jan–
>  1 Feb 2013.  Deadline 2 Sep.

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