Re: [isabelle] Interval Type



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.
The work was based on some existing literature, and involved sets of intervals (more complicated than single intervals!) which could be either open or closed at either endpoint.

It was written up in

Jeremy E. Dawson & Rajeev Goré, Machine-checking the Timed Interval Calculus, 15th Australian Joint Conference on Artificial Intelligence (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






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