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

```On 10.08.2012 13:40, Christoph LANGE wrote:
```
```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.
```
```
```
You will get the same theorem in the end, but it is handled differently in Isar; the assumptions will need to be used explicitly, e.g.
```
lemma greater_zero_implies_greater_equal_zero [simp] :
fixes x::real assumes "x > 0" shows "x \<ge> 0"
using assms by auto

```
```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".
```
```
```
This is entirely a matter of preference. I usually prefer structured lemma statements.
```
-- Lars

```

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