*To*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*Subject*: Re: [isabelle] Interval Type*From*: Steve Stevenson <steve at cs.clemson.edu>*Date*: Thu, 29 Jun 2006 09:39:16 -0400*Cc*: Francisco Jose Chaves Alonso <francisco.jose.chaves.alonso at ens-lyon.fr>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <44A32067.4030300@rsise.anu.edu.au>*References*: <20060627133527.977qvpbpeb4scg0k@webmail.ens-lyon.fr> <44A32067.4030300@rsise.anu.edu.au>

-- steve steve at cs.clemson.edu On Jun 28, 2006, at 8:35 PM, Jeremy Dawson wrote:

Francisco Jose Chaves Alonso wrote:HelloI want to implement the interval arithmetic for use in the proofof expressionslike: 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 theinterval [0,1], and then show that X*(1 – X) \<subseteq> [0,1].The operationson 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 * realwhich could be a good choice for Isabelle? Other possibilities orsuggestions?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 36Francisco, I did some work on intervals of real numbers some years ago.The work was based on some existing literature, and involved setsof intervals (more complicated than single intervals!) which couldbe either open or closed at either endpoint.It was written up inJeremy E. Dawson & Rajeev Goré, Machine-checking the TimedInterval Calculus, 15th Australian Joint Conference on ArtificialIntelligence (AI'02), LNCS 2557, 95-106,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

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

**Re: [isabelle] Interval Type***From:*Jeremy Dawson

- Previous by Date: [isabelle] [CfP] MathUI 2006: call to participate and demonstrate
- Next by Date: [isabelle] Setting up the Simplifier in Isabelle2005
- Previous by Thread: Re: [isabelle] Interval Type
- Next by Thread: [isabelle] CFP: SAVCBS'06 (Specification & Verification of Component-Based Systems)
- 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