*To*: Christoph LANGE <c.lange at cs.bham.ac.uk>*Subject*: Re: [isabelle] Inequalities on real numbers: How to use "(x::real) > 0 --> x >= 0"?*From*: Brian Huffman <huffman at in.tum.de>*Date*: Fri, 10 Aug 2012 10:15:27 +0200*Cc*: Colin Rowat <c.rowat at bham.ac.uk>, Manfred Kerber <M.Kerber at cs.bham.ac.uk>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5024ABB2.8010900@cs.bham.ac.uk>*References*: <5024ABB2.8010900@cs.bham.ac.uk>

On Fri, Aug 10, 2012 at 8:35 AM, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote: > Dear Isabelle experts, > > somewhere in a proof that involves real numbers from the theory "Real" I > would like to infer "(x::real) >= 0" from "x > 0". > > For now I solved the problem by introducing the following axiomatic "lemma": > > lemma greater_zero_implies_greater_equal_zero [simp] : > fixes x::real > assumes "x > 0" > shows "x ≥ 0" by (rule less_imp_le) - Brian

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

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

- Previous by Date: [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: [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