*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Date*: Fri, 10 Aug 2012 13:40:34 +0200*Cc*: Colin Rowat <c.rowat at bham.ac.uk>, Manfred Kerber <M.Kerber at cs.bham.ac.uk>, Brian Huffman <huffman at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <42C8200D-3654-4FF1-A9A0-695F17077B21@cam.ac.uk>*Organization*: University of Birmingham*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>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:14.0) Gecko/20120720 Thunderbird/14.0

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.

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"

Then almost anything will solve it: auto, simp, arith, force.

I suggest reserving assumes/shows for complicated theorems where there are many assumptions and they aren't all wanted at the same time.

Another remark: I'm not sure it's a good idea to declare something like this as a default simplification rule.

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

**Follow-Ups**:**Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?***From:*Lars Noschinski

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

**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

- 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