Quelle  intervals_real.pvs

intervals_real[T: TYPE FROM real]: THEORY
BEGIN

   AUTO_REWRITE+ member

   x,y: VAR T
   S,S1,S2: VAR set[T]
   
   r: VAR posreal

   open_intv(a:T,b:{x:T|a<x})(x)  : MACRO bool = a <  x AND x <  b
   closed_intv(a:T,b:{x:T|a<=x})(x): MACRO bool = a <= x AND x <= b

   open_interval(a:T,b:{x:T|a<x}): TYPE = (open_intv(a,b))
   closed_interval(a:T,b:{x:T|a<=x}): TYPE = (closed_intv(a,b))

   Open_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES (a < x AND x < b)) 
                                      AND (b < a  IMPLIES (b < x AND x < a))}

   Closed_interval(a,b:T): TYPE = {x: T | (a <= b IMPLIES (a <= x AND x <= b)) 
                                      AND (b < a  IMPLIES (b <= x AND x <= a))}


   above_intv(a:T)(x) : MACRO bool = x > a
   below_intv(a:T)(x) : MACRO bool = x < a

   a,b: VAR T


END intervals_real