*To*: jdavis27 at uiuc.edu*Subject*: Re: [isabelle] Nonlinear arithmetic for real numbers*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 15 Mar 2006 10:31:47 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <7d80da11.990ca239.8298c00@expms4.cites.uiuc.edu>*References*: <7d80da11.990ca239.8298c00@expms4.cites.uiuc.edu>

Use "auto" or "simp" to perform constant folding.

lemma "3/10 + 70/100 = (x::real)" apply (simp add: Ring_and_Field.add_frac_eq) This simplifies to "x=1". Larry Paulson On 14 Mar 2006, at 20:44, <jdavis27 at uiuc.edu> <jdavis27 at uiuc.edu> wrote:

I am having difficulty proving the following: lemma "(1::real) * (1::real) = (1::real)"; lemma "(1::real) / (1::real) = (1::real)"; The "arith" tactic does not support multiplication, as explained in previous messages.

**References**:**[isabelle] Nonlinear arithmetic for real numbers***From:*jdavis27

- Previous by Date: Re: [isabelle] Mixed decimals and Real.thy
- Next by Date: Re: [isabelle] Mixed decimals and Real.thy
- Previous by Thread: [isabelle] Nonlinear arithmetic for real numbers
- Next by Thread: [isabelle] new AFP entries
- Cl-isabelle-users March 2006 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