[isabelle] real number calculation



Dear all,

I want to prove some theorems concerning real number calculation.

For example, we have the operator \<start> as:

a \<start> b = 0.5 + 2 * (a - 0.5) * (b - 0.5).

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

Also, how to express the pre-condition that "a is within the area [0,1]"?

Thanks
Xiaoqi


Yahoo! Music Unlimited - Access over 1 million songs. Try it free.

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