*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Fri, 10 Aug 2012 14:07:09 +0200*In-reply-to*: <5024F332.1020505@cs.bham.ac.uk>*References*: <5024ABB2.8010900@cs.bham.ac.uk> <CAAMXsiayP7z=SKiXA3bhQ0iav_AMqdJDEU+itHRTKTgOMGZs-w@mail.gmail.com> <5024DD89.3010508@cs.bham.ac.uk> <42C8200D-3654-4FF1-A9A0-695F17077B21@cam.ac.uk> <5024F332.1020505@cs.bham.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.5) Gecko/20120624 Icedove/10.0.5

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.

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".

-- Lars

**References**:**[isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Christoph LANGE

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

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

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

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

- Previous by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Date: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Previous by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Next by Thread: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list