*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] real number calculation*From*: Isabelle <isabellemxq at yahoo.com>*Date*: Mon, 28 Nov 2005 11:58:00 -0800 (PST)*Domainkey-signature*: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:Received:Date:From:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=FtJLhBbV65sr0dQqDuCg/OTj0ZMYf6X3EoBqDWsEdsu8sDRb1YyRPbVEVJ5V40aBB41JVadR3mUCZVZl91L+XMyeMf2Oa9ZD74a7kyC4r5LoFg+BaaA8EVLYmcvNlqqcYz1uuTvbOgqLLW5ioagUVY9ltkh1R4xoTKv5OnHQ+wY= ;

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

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.

**Follow-Ups**:**[isabelle] precedences and orderings***From:*Lucas Dixon

**Re: [isabelle] real number calculation***From:*nipkow

**Re: [isabelle] real number calculation***From:*Lawrence Paulson

- Previous by Date: [isabelle] Call for Papers [Reminder]: JAR Special Issue on User Interfaces for Theorem Proving.
- Next by Date: Re: [isabelle] Creating new Isar theorem attributes
- Previous by Thread: [isabelle] Call for Papers [Reminder]: JAR Special Issue on User Interfaces for Theorem Proving.
- Next by Thread: [isabelle] precedences and orderings
- 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