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

Dear Larry, dear all (some more general-interest comments below; search for "objectives"),
```
2012-08-10 12:22 Lawrence Paulson:
```
```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.
```
```
```
Thanks, that's good to know. I really had thought that "assumes/shows" is just syntactic sugar for certain more complex expressions within the logic.
```
```
(Note: Don't be too worried when I say "I thought" or "I didn't know" or "I had no idea" – I still need to learn a lot. Whenever I think that something should really be presented in a more learnable way, I will make it explicit, as in a bug report :-))
```
```
```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"
```
```
```
Nice! I had no idea that one can omit the universal quantification of x::real here.
```
```
```Then almost anything will solve it: auto, simp, arith, force.
```
```
```
So from x::real these provers will know that it is a real number and therefore an element of an ordered set?
```
```
```I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time.
```
```
```
Thanks, that's good to know. One of the objectives of our project (http://cs.bham.ac.uk/research/projects/formare/) is to teach ATP/ITP to non-experts from application domains, economics in our case.
```
```
We are interested in formalising new theorems that haven't been formalised before, but also re-formalising things that have been formalised before, but in a way that doesn't "just get the proof done", but in a way that we think we could teach to economists.
```
```
Therefore we would like to keep as closely as possible to paper textbook style, and for this reason I thought "the more Isar syntactic sugar the better".
```
```
We just got started with Isabelle (have done some formalisation in Theorema before), but first public results can be expected soon.
```
```
```Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule.
```
```
```
Thanks for the heads-up – indeed that approach resulted from the misunderstanding; I didn't know that one can simply say (rule name_of_lemma).
```
Cheers,

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.