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
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
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
This is entirely a matter of preference. I usually prefer structured
This archive was generated by a fusion of
Pipermail (Mailman edition) and