*To*: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso at ens-lyon.fr>*Subject*: Re: [isabelle] Interval Type*From*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Date*: Thu, 29 Jun 2006 10:35:51 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20060627133527.977qvpbpeb4scg0k@webmail.ens-lyon.fr>*Organization*: Australian National University*References*: <20060627133527.977qvpbpeb4scg0k@webmail.ens-lyon.fr>*User-agent*: Mozilla Thunderbird 0.9 (X11/20041124)

Francisco Jose Chaves Alonso wrote:

Hello I want to implement the interval arithmetic for use in the proof of expressions like: x \<in> [0,1] ==> x * (1 – x) \<in> [0,1] The interval [a,b] is the set of real numbers { x | a <= x <= b}. Based on the work of Daumas et al. on PVS, http://research.nianet.org/~munoz/Papers/arith-17.pdf, the idea is to show that x*(1 – x) is in the interval X*(1 – X) where X is the interval [0,1], and then show that X*(1 – X) \<subseteq> [0,1]. The operations on intervals are defined such that X at Y = { x at y | x \<in> X /\ y \<in> Y }, @ \<in> {+,-,*,/} To model the intervals I have at least the following possibilities: datatype interval = Interval real * real record interval = lb:: real ub:: real types interval:: real * real which could be a good choice for Isabelle? Other possibilities or suggestions? Thanks Francisco -- Francisco José Cháves (ENS-LIP) mailto: Francisco.Jose.Chaves.Alonso at ens-lyon.fr http://perso.ens-lyon.fr/francisco.jose.chaves.alonso ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE Phone: (+33) 4 72 72 84 36

Francisco, I did some work on intervals of real numbers some years ago.

It was written up in

see http://users.rsise.anu.edu.au/~jeremy/pubs/tic/ Software files in Isabelle are at http://users.rsise.anu.edu.au/~jeremy/isabelle/tic/ Jeremy

**Follow-Ups**:**Re: [isabelle] Interval Type***From:*Steve Stevenson

**References**:**[isabelle] Interval Type***From:*Francisco Jose Chaves Alonso

- Previous by Date: [isabelle] coinduct problem
- Next by Date: [isabelle] [CfP] MathUI 2006: call to participate and demonstrate
- Previous by Thread: Re: [isabelle] Interval Type
- Next by Thread: Re: [isabelle] Interval Type
- Cl-isabelle-users June 2006 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