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