(* =========================================================== *)
(* Theoretical results for interval arithmetic                 *)
(* Author: Alexey Solovyev                                     *)
(* Date: 2012-10-27                                            *)
(* =========================================================== *)

needs "misc/vars.hl";;

module Interval_arith = struct

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

(* Additional definitions *)
let bounded_on = new_definition `bounded_on f s f_bounds <=>
	!x. x IN s ==> interval_arith (f x) f_bounds`;;

let bounded_on_int = new_definition `bounded_on_int f int f_bounds <=>
	!x. interval_arith x int ==> interval_arith (f x) f_bounds`;;
	
let iabs = new_definition `iabs (x_lo, x_hi) = max x_hi (-- x_lo)`;;
let interval_not_zero = new_definition `interval_not_zero (lo, hi) <=> &0 < lo \/ hi < &0`;;
let interval_pos = new_definition `interval_pos (lo, hi) <=> &0 < lo`;;


(********************************)
(* Lemmas *)
let CONST_INTERVAL = prove(`!x. interval_arith x (x,x)`,
                           REWRITE_TAC[interval_arith; REAL_LE_REFL]);;

let APPROX_INTERVAL = (GEN_ALL o 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 = (GEN_ALL o prove)(`interval_arith x (a, b) ==>
                           interval_arith (--x) (--b, --a)`,
                         REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;
						 

(**************************************)
(* Conversions *)		
open Misc_vars;;
				 
let interval_tm = `interval_arith`;;

let dest_interval_arith tm =
  let lhs, int_tm = dest_comb tm in
    rand lhs, int_tm;;

let mk_interval tm bounds =
	mk_comb (mk_comb (interval_tm, tm), bounds);;
	
let mk_const_interval =
	let lemma = SPEC_ALL CONST_INTERVAL in
		fun tm -> INST[tm, x_var_real] lemma;;

end;;