Re: [isabelle] real number calculation

The definition of star looks fine to me. The proof of those theorems will require simplification using the definition (star_def) and various properties of + - * and /. You can find the ones you are likely to need using the Find button in proof general. I can't guarantee that the multiplication of fractions will be done cleverly. We haven't done much of that.

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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.