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.
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