Re: [isabelle] Interval Type

Francisco Jose Chaves Alonso wrote:

I want to implement the interval arithmetic for use in the proof of expressions

     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,,
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?



-- Francisco José Cháves (ENS-LIP)
mailto: Francisco.Jose.Chaves.Alonso at
ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE
Phone: (+33) 4 72 72 84 36


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,


Software files in Isabelle are at


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