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