*To*: Isabelle <isabellemxq at yahoo.com>*Subject*: Re: [isabelle] real number calculation*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Wed, 30 Nov 2005 10:36:53 +0000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20051128195800.38901.qmail@web32611.mail.mud.yahoo.com>*References*: <20051128195800.38901.qmail@web32611.mail.mud.yahoo.com>*Sender*: "L. Paulson" <lp15 at hermes.cam.ac.uk>

Larry Paulson On 28 Nov 2005, at 19:58, Isabelle wrote:

We define \<start> in Isabelle using the following statement: constdefs star :: "real=>real=>real" "(a \<start> b) == 1/2 + 2*(a-(1/2))*(b-(1/2))" Is there any problem with that? How to prove "1 \<start> a = a" and "a \<start> (b \<start> c) = (a \<start> b) \<start> c"?

**References**:**[isabelle] real number calculation***From:*Isabelle

- Previous by Date: Re: [isabelle] Trying to simplify with setsum
- Next by Date: Re: [isabelle] Trying to simplify with setsum
- Previous by Thread: Re: [isabelle] real number calculation
- Next by Thread: [isabelle] CTL formalization
- Cl-isabelle-users November 2005 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