(********************************)
(* Interval arithmetic (theory) *)
(********************************)

module Interval_arith = struct

(* The main definition *)
let interval_arith = 
	new_definition `interval_arith (x:real) (lo, hi) <=> lo <= x /\ x <= hi`;;


let CONST_INTERVAL = 
prove(`!x. interval_arith x (x,x)`,

                           REWRITE_TAC[interval_arith; REAL_LE_REFL]);;


let APPROX_INTERVAL = 
prove(`(a <= lo /\ hi <= b) /\ interval_arith x (lo, hi)
                              ==> interval_arith x (a,b)`,

   REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;

let INTERVAL_NEG = 
prove(`interval_arith x (a, b) ==>
                           interval_arith (--x) (--b, --a)`,

                         REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;



end;;