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.