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