(********************************)
(* 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;;