# [isabelle] Interval Type

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

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