Re: [isabelle] Interval Type

Your best bet is to contact the folks doing interval arithmetic research: reliable_computing at and interval at

To the point, there has been recent discussions on the mis- representation of intervals by Mathematica. The problems become very complex, really quickly, if you're doing symbolic mathematics on intervals.
steve at

On Jun 28, 2006, at 8:35 PM, Jeremy Dawson wrote:

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.