needs "../formal_lp/formal_interval/lin_approx.hl";;

(* Explicit formula (float) for inv(&2) *)

let float_inv2_th =
  let one_float_eq_one = FLOAT_TO_NUM_CONV one_float in
  let inv2_eq_lemma = prove(`interval_arith (&2 * x) (&1, &1) ==> inv (&2) = x`,
			    REWRITE_TAC[interval_arith] THEN CONV_TAC REAL_FIELD) in
  let half_tm = (fst o dest_pair o rand o concl) (float_interval_inv 1 two_interval) in
  let half_interval = mk_const_interval half_tm in
  let mul_th = REWRITE_RULE[one_float_eq_one] (float_interval_mul 2 two_interval half_interval) in
    MATCH_MP inv2_eq_lemma mul_th;;

let float_inv2 = rand (concl float_inv2_th);;
let inv2_interval = mk_const_interval float_inv2;;

let INTERVAL_IMP_HI = (RULE o prove)(`interval_arith x (lo, hi) ==> x <= hi`,
				     REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;

let interval_imp_hi int_th =
  let lhs, bounds = dest_comb (concl int_th) in
  let x_tm, (lo_tm, hi_tm) = rand lhs, dest_pair bounds in
  let th0 = INST[x_tm, x_var_real; lo_tm, lo_var_real; hi_tm, hi_var_real] INTERVAL_IMP_HI in
    MY_PROVE_HYP int_th th0;;


(*****************************)
(* cell_domain *)

let dest_cell_domain tm =
  let lhs, w_tm = dest_comb tm in
  let lhs2, z_tm = dest_comb lhs in
  let lhs3, y_tm = dest_comb lhs2 in
    rand lhs3, y_tm, z_tm, w_tm;;


(******************************************)

let CELL_DOMAIN_IMP_INTERVAL_ARITH = prove(`cell_domain x y z w ==> interval_arith y (x, z)`,
					   REWRITE_TAC[cell_domain; interval_arith] THEN REAL_ARITH_TAC);;


let MK_CELL_DOMAIN_0' = (UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o prove)
  (`(x <= y <=> T) /\ (y <= z <=> T) /\ y - x <= w1 /\ z - y <= w2 /\ (w1 <= w <=> T) /\ (w2 <= w <=> T) ==> 
     cell_domain x y z w`,
   SIMP_TAC[cell_domain] THEN REAL_ARITH_TAC);;


let MK_CELL_DOMAIN' = (UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o prove)
  (`(x <= y <=> T) /\ (y <= z <=> T) /\ y - x <= w1 /\ z - y <= w2 /\ max w1 w2 = w ==>
				       cell_domain x y z w`, REWRITE_TAC[cell_domain] THEN REAL_ARITH_TAC);;


let mk_cell_domain0 pp x_tm y_tm z_tm w_tm =
  let xy_th = float_le x_tm y_tm and
      yz_th = float_le y_tm z_tm in
  let yx_w1 = float_sub_hi pp y_tm x_tm and
      zy_w2 = float_sub_hi pp z_tm y_tm in
  let w1_tm = (rand o concl) yx_w1 and
      w2_tm = (rand o concl) zy_w2 in
  let w1w = float_le w1_tm w_tm and
      w2w = float_le w2_tm w_tm in
  let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; 
		 w_tm, w_var_real; w1_tm, w1_var_real; w2_tm, w2_var_real] MK_CELL_DOMAIN_0' in
    (MY_PROVE_HYP xy_th o MY_PROVE_HYP yz_th o MY_PROVE_HYP yx_w1 o MY_PROVE_HYP zy_w2 o
       MY_PROVE_HYP w1w o MY_PROVE_HYP w2w) th0;;


let mk_cell_domain pp x_tm y_tm z_tm =
  let w1_th = float_sub_hi pp y_tm x_tm and
      w2_th = float_sub_hi pp z_tm y_tm in
  let w1_tm = (rand o concl) w1_th and
      w2_tm = (rand o concl) w2_th in
  let max_th = float_max w1_tm w2_tm in
  let w_tm = (rand o concl) max_th in
  let x_le_y = float_le x_tm y_tm and
      y_le_z = float_le y_tm z_tm in
  let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;
		 w_tm, w_var_real; w1_tm, w1_var_real; w2_tm, w2_var_real] MK_CELL_DOMAIN' in
    (MY_PROVE_HYP x_le_y o MY_PROVE_HYP y_le_z o 
       MY_PROVE_HYP w1_th o MY_PROVE_HYP w2_th o MY_PROVE_HYP max_th) th0;;
  



(* TODO: remove formal computation of y *)
let mk_center_domain pp x_tm z_tm =
  let y0_tm = (rand o concl) (float_add_hi pp x_tm z_tm) in
  let y_tm = (rand o concl) (float_mul_eq float_inv2 y0_tm) in
    mk_cell_domain pp x_tm y_tm z_tm;;


(*
let x_tm = mk_float 1 50;;
let z_tm = mk_float 4 50;;

let domain_th = mk_center_domain 2 x_tm z_tm;;

let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th);;
mk_cell_domain 2 x_tm y_tm z_tm;;
mk_cell_domain0 2 x_tm y_tm z_tm w_tm;;
*)


(***************************************************)
(* Elementary functions and their taylor intervals *)
(***************************************************)


(*****************************)
(* f(x) = x *)

let TAYLOR_X' = RULE taylor_x;;


let eval_taylor_x domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real] TAYLOR_X' in
    MY_PROVE_HYP domain_th th0;;

 
(*			  
eval_taylor_x domain_th;;
*)

(********************************)
(* f(x) = const *)

let TAYLOR_CONST' = RULE taylor_const;;
let eval_taylor_const domain_th c_tm =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
    (MY_PROVE_HYP domain_th o
       INST[c_tm, c_var_real; x_tm, x_var_real; y_tm, y_var_real; 
	    z_tm, z_var_real; w_tm, w_var_real]) TAYLOR_CONST';;


let TAYLOR_CONST_INTERVAL' = (RULE o prove)
  (`cell_domain x y z w ==> interval_arith c bounds ==>
     taylor_interval (\x. c) x y z w bounds (&0, &0) (&0, &0)`,
  REPEAT DISCH_TAC THEN
    MP_TAC (SPEC_ALL taylor_const) THEN ASM_SIMP_TAC[taylor_interval; lin_approx_eq]);;

let eval_taylor_const_interval int_th domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let lhs, bounds = dest_comb (concl int_th) in
  let c_tm = rand lhs in
    (MY_PROVE_HYP int_th o MY_PROVE_HYP domain_th o
       INST[c_tm, c_var_real; bounds, bounds_var; x_tm, x_var_real; y_tm, y_var_real;
	    z_tm, z_var_real; w_tm, w_var_real]) TAYLOR_CONST_INTERVAL';;


(*
eval_taylor_const domain_th `&3`;;
*)

(***********************************)
(* f(x) = atn x *)

let taylor_atn = prove(`cell_domain x y z w ==>
			 bounded_on_int (\x. (-- &2 * x) / (&1 + x pow 2) pow 2) (x,z) dd_bounds ==>
			 lin_approx atn y f_bounds df_bounds ==>
			 taylor_interval atn x y z w f_bounds df_bounds dd_bounds`,
  REWRITE_TAC[cell_domain; taylor_interval; real_div; REAL_INV_POW] THEN REPEAT DISCH_TAC THEN 
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC second_derivative_atn_bounds THEN ASM_REWRITE_TAC[]);;

let TAYLOR_ATN' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2]) taylor_atn;;


let eval_taylor_atn pp domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let atn_lin = eval_lin_approx_atn pp y_tm in
  let _, _, f_bounds, df_bounds = dest_lin_approx (concl atn_lin) in

  let ddf_th = 
    let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and
	( * ) = float_interval_mul pp and
	(+) = float_interval_add pp and
	(/) = float_interval_div pp in
    let x2_1 = one_interval + x_th * x_th in
      mk_bounded_on_int ((neg_two_interval * x_th) / (x2_1 * x2_1)) in
 
  let dd_bounds = rand (concl ddf_th) in
    (MY_PROVE_HYP domain_th o MY_PROVE_HYP atn_lin o MY_PROVE_HYP ddf_th o
       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
	    dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_ATN';;



(*
let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;
let pp = 5;;
eval_taylor_atn pp domain_th;;
*)



(***********************************)
(* f(x) = inv x *)

let taylor_inv = prove(`cell_domain x y z w ==>
			 interval_not_zero (x,z) ==>
			 bounded_on_int (\x. &2 * inv (x pow 3)) (x,z) dd_bounds ==>
			 lin_approx inv y f_bounds df_bounds ==>
			 taylor_interval inv x y z w f_bounds df_bounds dd_bounds`,
  REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN 
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_inv_bounds) THEN ASM_REWRITE_TAC[]);;

let TAYLOR_INV' = (UNDISCH_ALL o REWRITE_RULE[GSYM real_div; REAL_ARITH `x pow 3 = x * x * x`]) taylor_inv;;


let eval_taylor_inv pp domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let int_tm = mk_pair (x_tm, z_tm) in
  let lin_th = eval_lin_approx_inv pp y_tm in
  let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in
  let cond_th = check_interval_not_zero int_tm in

  let ddf_th = 
    let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp in
      mk_bounded_on_int (two_interval / (x_th * (x_th * x_th))) in
 
  let dd_bounds = rand (concl ddf_th) in
    (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o
       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
	    dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_INV';;



(*
let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;
let pp = 5;;
eval_taylor_inv pp domain_th;;
*)


(***********************************)
(* f(x) = sqrt x *)

let taylor_sqrt = prove(`cell_domain x y z w ==>
			 interval_pos (x,z) ==>
			 bounded_on_int (\x. --inv (&4 * sqrt (x pow 3))) (x,z) dd_bounds ==>
			 lin_approx sqrt y f_bounds df_bounds ==>
			 taylor_interval sqrt x y z w f_bounds df_bounds dd_bounds`,
  REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN 
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_sqrt_bounds) THEN ASM_REWRITE_TAC[]);;

let TAYLOR_SQRT' = (UNDISCH_ALL o REWRITE_RULE[REAL_ARITH `x pow 3 = x * x * x`]) taylor_sqrt;;
let four_interval = mk_float_interval_small_num 4;;


let eval_taylor_sqrt pp domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let int_tm = mk_pair (x_tm, z_tm) in
  let lin_th = eval_lin_approx_sqrt pp y_tm in
  let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in
  let cond_th = check_interval_pos int_tm in

  let ddf_th = 
    let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and
	( * ) = float_interval_mul pp and
	sqrt = float_interval_sqrt pp and
	inv = float_interval_inv pp and
	neg = float_interval_neg in
      mk_bounded_on_int (neg (inv (four_interval * sqrt (x_th * (x_th * x_th))))) in
 
  let dd_bounds = rand (concl ddf_th) in
    (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o
       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
	    dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_SQRT';;



(*
let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;
let pp = 5;;
eval_taylor_sqrt pp domain_th;;
*)


(***********************************)
(* f(x) = acs x *)

let iabs_lt1_lemma = 
  (GEN_REWRITE_RULE (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM (FLOAT_TO_NUM_CONV one_float)] o prove)
    (`iabs int < &1 <=> (iabs int < &1 <=> T)`, REWRITE_TAC[]);;

let taylor_acs = prove(`cell_domain x y z w ==>
			 iabs (x,z) < &1 ==>
			 bounded_on_int (\x. --(x / sqrt ((&1 - x * x) pow 3))) (x,z) dd_bounds ==>
			 lin_approx acs y f_bounds df_bounds ==>
			 taylor_interval acs x y z w f_bounds df_bounds dd_bounds`,
  REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN 
    ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_acs_bounds) THEN ASM_REWRITE_TAC[]);;

let TAYLOR_ACS' = 
  (UNDISCH_ALL o 
     PURE_ONCE_REWRITE_RULE[iabs_lt1_lemma] o
     REWRITE_RULE[REAL_ARITH `x pow 3 = x * x * x`]) taylor_acs;;


let eval_taylor_acs pp domain_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let int_tm = mk_pair (x_tm, z_tm) in
  let lin_th = eval_lin_approx_acs pp y_tm in
  let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in
  let cond_th = check_interval_iabs int_tm one_float in

  let ddf_th = 
    let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and
	( * ) = float_interval_mul pp and
	(-) = float_interval_sub pp and
	(/) = float_interval_div pp and
	sqrt = float_interval_sqrt pp and
	neg = float_interval_neg in
    let x2_1 = one_interval - x_th * x_th in
      mk_bounded_on_int (neg (x_th / sqrt (x2_1 * (x2_1 * x2_1)))) in
 
  let dd_bounds = rand (concl ddf_th) in
    (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o
       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
	    dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_ACS';;



(*
let domain_th1 = mk_center_domain 5 (mk_float 1 49) (mk_float 8 49);;
let domain_th2 = mk_center_domain 5 (mk_float (-5) 49) (mk_float 1 49);;
let pp = 5;;
eval_taylor_acs pp domain_th1;;
eval_taylor_atn pp domain_th1;;
eval_taylor_inv pp domain_th1;;
eval_taylor_sqrt pp domain_th1;;

eval_taylor_acs pp domain_th2;;
eval_taylor_atn pp domain_th2;;
eval_taylor_inv pp domain_th2;;
eval_taylor_sqrt pp domain_th2;;
*)


(***********************************************************)


(***********************************)
(* Taylor bounds *)


let dest_taylor_interval tm =
  let lhs, dd_bounds = dest_comb tm in
  let lhs, df_bounds = dest_comb lhs in
  let lhs, f_bounds = dest_comb lhs in
  let lhs, w_tm = dest_comb lhs in
  let lhs, z_tm = dest_comb lhs in
  let lhs, y_tm = dest_comb lhs in
  let lhs, x_tm = dest_comb lhs in
    rand lhs, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds;;


(****************************)
(* f_bounds *)

let TAYLOR_F_BOUNDS' = (RULE o REWRITE_RULE[float_inv2_th]) taylor_f_bounds;;


let eval_taylor_f_bounds pp th =
  let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in
  let f_lo, f_hi = dest_pair f_bounds in
  let iabs_df_th = float_iabs df_bounds and
      iabs_dd_th = float_iabs dd_bounds in
  let df_tm = (rand o concl) iabs_df_th and
      dd_tm = (rand o concl) iabs_dd_th in

  let error_th =
    let df = mk_refl_ineq df_tm and
	inv2 = mk_refl_ineq float_inv2 and
	( * ) = mul_ineq_pos_const_hi pp and
	( + ) = add_ineq_hi pp in
      w_tm * (df + w_tm * (dd_tm * inv2)) in

  let t_tm = (rand o concl) error_th in
  let lo_th = float_sub_lo pp f_lo t_tm and
      hi_th = float_add_hi pp f_hi t_tm in
  let lo_tm = (lhand o concl) lo_th and
      hi_tm = (rand o concl) hi_th in

    (MY_PROVE_HYP lo_th o MY_PROVE_HYP hi_th o MY_PROVE_HYP error_th o 
       MY_PROVE_HYP iabs_df_th o MY_PROVE_HYP iabs_dd_th o MY_PROVE_HYP th o
       INST[dd_bounds, dd_bounds_var; dd_tm, dd_var_real; df_bounds, df_bounds_var;
	    df_tm, df_var_real; t_tm, t_var_real;
	    lo_tm, lo_var_real; f_lo, f_lo_var;
	    w_tm, w_var_real; f_hi, f_hi_var; hi_tm, hi_var_real;
	    f_tm, f_var_fun; x_tm, x_var_real; 
	    y_tm, y_var_real; z_tm, z_var_real]) TAYLOR_F_BOUNDS';;


(*
let pp = 3;;
let domain_th = mk_center_domain pp one_float two_float;;
let th = eval_taylor_atn pp domain_th;;
eval_taylor_f_bounds pp th;;
(* 10: 1.620 *)
test 1000 (eval_taylor_f_bounds pp) th;;
*)


(****************************)
(* df_bounds *)


let TAYLOR_DF_BOUNDS' = RULE taylor_df_bounds;;

let eval_taylor_df_bounds pp th =
  let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in
  let df_lo, df_hi = dest_pair df_bounds in
  let iabs_dd_th = float_iabs dd_bounds in
  let dd_tm = (rand o concl) iabs_dd_th in
  let w_dd_hi = float_mul_hi pp w_tm dd_tm in

  let lo_th = sub_ineq_lo pp (mk_refl_ineq df_lo) w_dd_hi and
      hi_th = add_ineq_hi pp (mk_refl_ineq df_hi) w_dd_hi in
  let lo_tm = (lhand o concl) lo_th and
      hi_tm = (rand o concl) hi_th in

    (MY_PROVE_HYP lo_th o MY_PROVE_HYP hi_th o MY_PROVE_HYP th o MY_PROVE_HYP iabs_dd_th o
       INST[dd_bounds, dd_bounds_var; dd_tm, dd_var_real; f_bounds, f_bounds_var;
	    lo_tm, lo_var_real; df_lo, df_lo_var;
	    w_tm, w_var_real; df_hi, df_hi_var; hi_tm, hi_var_real;
	    f_tm, f_var_fun; x_tm, x_var_real; 
	    y_tm, y_var_real; z_tm, z_var_real]) TAYLOR_DF_BOUNDS';;


(*
let pp = 3;;
let th = eval_taylor_atn pp domain_th;;
eval_taylor_df_bounds pp th;;
*)

(**************************************************)
(* mk_taylor_interval_th, dest_taylor_interval_th *)

let TAYLOR_INTERVAL_EQ' = (RULE o prove)(`taylor_interval f x y z w f_bounds df_bounds dd_bounds <=>
					     cell_domain x y z w /\ lin_approx f y f_bounds df_bounds /\
					     has_bounded_second_derivative f (x,z) dd_bounds`,
					   SIMP_TAC[cell_domain; taylor_interval; CONJ_ACI]);;

let MK_TAYLOR_INTERVAL' = (RULE o prove)(`cell_domain x y z w /\ 
					  lin_approx f y f_bounds df_bounds /\
					  has_bounded_second_derivative f (x,z) dd_bounds ==>
					  taylor_interval f x y z w f_bounds df_bounds dd_bounds`,
					SIMP_TAC[cell_domain; taylor_interval]);;


let dest_taylor_interval_th th =
  let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in
  let th0 = INST[f_tm, f_var_fun; x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;
		 w_tm, w_var_real; f_bounds, f_bounds_var;
		 df_bounds, df_bounds_var; dd_bounds, dd_bounds_var] TAYLOR_INTERVAL_EQ' in
  let [domain; approx; second] = CONJUNCTS (EQ_MP th0 th) in
    domain, approx, second;;



let mk_taylor_interval_th domain_th approx_th second_th =
  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in
  let f_tm, _, f_bounds, df_bounds = dest_lin_approx (concl approx_th) in
  let dd_bounds = rand (concl second_th) in
  let th0 = INST[f_tm, f_var_fun; x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;
		 w_tm, w_var_real; f_bounds, f_bounds_var;
		 df_bounds, df_bounds_var; dd_bounds, dd_bounds_var] MK_TAYLOR_INTERVAL' in
    (MY_PROVE_HYP approx_th o MY_PROVE_HYP domain_th o MY_PROVE_HYP second_th) th0;;
  


(*
let th = eval_taylor_atn 5 domain_th;;
let domain_th, approx_th, second_th = dest_taylor_interval_th th;;
mk_taylor_interval_th domain_th approx_th second_th;;
*)


(**************************************)
(* has_bounded_second_derivative_dest *)

let HAS_BOUNDED_SECOND_DERIVATIVE_EQ' = SPEC_ALL has_bounded_second_derivative;;


let dest_has_bounded_second_derivative tm =
  let lhs, dd_bounds = dest_comb tm in
  let lhs2, int_tm = dest_comb lhs in
    rand lhs2, int_tm, dd_bounds;;


let dest_has_bounded_second_derivative_th th =
  let f_tm, int_tm, dd_bounds = dest_has_bounded_second_derivative (concl th) in
  let th0 = INST[f_tm, f_var_fun; int_tm, int_var; 
		 dd_bounds, dd_bounds_var] HAS_BOUNDED_SECOND_DERIVATIVE_EQ' in
  let [diff_th; bounded_th] = CONJUNCTS (EQ_MP th0 th) in
    diff_th, bounded_th;;


(*
let diff_th, bounded_th = dest_has_bounded_second_derivative_th second_th;;
*)

(********************************************)


(******************************)
(* Taylor interval arithmetic *)
(******************************)


(**************************************)
let taylor_interval_tm = `taylor_interval`;;

let taylor_interval_norm th eq_th =
  let lhs1, d2f = dest_comb (concl th) in
  let lhs2, d1f = dest_comb lhs1 in
  let lhs3, d0f = dest_comb lhs2 in
  let lhs4, w = dest_comb lhs3 in
  let lhs5, z = dest_comb lhs4 in
  let lhs6, y = dest_comb lhs5 in
  let x = rand lhs6 in
  let th0 = AP_TERM taylor_interval_tm eq_th in
  let th1 = (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM th0 x) y) z) w) d0f) d1f) d2f) in
    EQ_MP th1 th;;


(*************************************)
(* taylor_interval_neg *)
let TAYLOR_INTERVAL_NEG' = (UNDISCH_ALL o prove)
  (`cell_domain x y z w ==>
     lin_approx (\x. -- (f x)) y bounds d_bounds ==>
     nth_diff_strong_int 2 (x,z) f ==>
     bounded_on_int (\x. -- nth_derivative 2 f x) (x,z) dd_bounds ==>
     taylor_interval (\x. -- (f x)) x y z w bounds d_bounds dd_bounds`,
   SIMP_TAC[taylor_interval; cell_domain] THEN ONCE_REWRITE_TAC[REAL_ARITH `--a = (-- (&1)) * a`] THEN
     REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[second_derivative_scale_bounds]);;


let taylor_interval_neg th1 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in

  let approx_th = lin_approx_neg approx1_th in
  let dd_th = bounded_on_int_neg dd1_th in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_NEG' in
  let eq_th = unary_beta_eq f_tm neg_op_real in
    taylor_interval_norm th0 eq_th;;
     

(*
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
taylor_interval_neg th1;;
taylor_interval_neg th2;;
*)



(*************************************)
(* taylor_interval_add *)

let TAYLOR_INTERVAL_ADD' = (UNDISCH_ALL o prove)
  (`cell_domain x y z w ==>
     lin_approx (\x. f x + g x) y bounds d_bounds ==>
     nth_diff_strong_int 2 (x,z) f ==>
     nth_diff_strong_int 2 (x,z) g ==>
     bounded_on_int (\x. nth_derivative 2 f x + nth_derivative 2 g x) (x,z) dd_bounds ==>
     taylor_interval (\x. f x + g x) x y z w bounds d_bounds dd_bounds`,
   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[second_derivative_add_bounds]);;


let taylor_interval_add pp th1 th2 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and
      _, approx2_th, second2_th = dest_taylor_interval_th th2 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and
      diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in

  let approx_th = lin_approx_add pp approx1_th approx2_th in
  let dd_th = 
    let (+) = bounded_on_int_add pp in
      dd1_th + dd2_th in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      g_tm = (rand o concl) diff2_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; g_tm, g_var_fun;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_ADD' in
  let eq_th = binary_beta_eq f_tm g_tm add_op_real in
    taylor_interval_norm th0 eq_th;;



(*
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
taylor_interval_add pp th1 th2;;
*)


(*************************************)
(* taylor_interval_sub *)

let TAYLOR_INTERVAL_SUB' = (UNDISCH_ALL o prove)
  (`cell_domain x y z w ==>
     lin_approx (\x. f x - g x) y bounds d_bounds ==>
     nth_diff_strong_int 2 (x,z) f ==>
     nth_diff_strong_int 2 (x,z) g ==>
     bounded_on_int (\x. nth_derivative 2 f x - nth_derivative 2 g x) (x,z) dd_bounds ==>
     taylor_interval (\x. f x - g x) x y z w bounds d_bounds dd_bounds`,
   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[second_derivative_sub_bounds]);;


let taylor_interval_sub pp th1 th2 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and
      _, approx2_th, second2_th = dest_taylor_interval_th th2 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and
      diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in

  let approx_th = lin_approx_sub pp approx1_th approx2_th in
  let dd_th = 
    let (-) = bounded_on_int_sub pp in
      dd1_th - dd2_th in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      g_tm = (rand o concl) diff2_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; g_tm, g_var_fun;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_SUB' in
  let eq_th = binary_beta_eq f_tm g_tm sub_op_real in
    taylor_interval_norm th0 eq_th;;



(*
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
taylor_interval_sub pp th1 th2;;
*)


(*************************************)
(* taylor_interval_mul *)

let TAYLOR_INTERVAL_MUL' = (UNDISCH_ALL o prove)
  (`cell_domain x y z w ==>
     lin_approx (\x. f x * g x) y bounds d_bounds ==>
     nth_diff_strong_int 2 (x,z) f ==>
     nth_diff_strong_int 2 (x,z) g ==>
     bounded_on_int (\x. f x * nth_derivative 2 g x + &2 * derivative f x * derivative g x +
		     nth_derivative 2 f x * g x) (x,z) dd_bounds ==>
     taylor_interval (\x. f x * g x) x y z w bounds d_bounds dd_bounds`,
   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
     ASM_SIMP_TAC[second_derivative_mul_bounds]);;


let taylor_interval_mul pp th1 th2 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and
      _, approx2_th, second2_th = dest_taylor_interval_th th2 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and
      diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in

  let approx_th = lin_approx_mul pp approx1_th approx2_th in
  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = (dest o eval_taylor_f_bounds pp) th1 and
	g = (dest o eval_taylor_f_bounds pp) th2 and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	dg = (dest o eval_taylor_df_bounds pp) th2 and
	ddf = dest dd1_th and
	ddg = dest dd2_th and
	(+) = float_interval_add pp and
	( * ) = float_interval_mul pp in
      mk_bounded_on_int (f * ddg + (two_interval * (df * dg) + ddf * g)) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      g_tm = (rand o concl) diff2_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; g_tm, g_var_fun;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_MUL' in
  let eq_th = binary_beta_eq f_tm g_tm mul_op_real in
    taylor_interval_norm th0 eq_th;;



(*
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
let th3 = taylor_interval_sub pp th1 th2;;
taylor_interval_mul pp th1 th3;;
*)



(*************************************)
(* taylor_interval_div *)

let TAYLOR_INTERVAL_DIV' = (UNDISCH_ALL o prove)
 (`cell_domain x y z w ==>
    bounded_on_int g (x,z) g_bounds ==>
    interval_not_zero g_bounds ==>
    lin_approx (\x. f x / g x) y bounds d_bounds ==>
    nth_diff_strong_int 2 (x,z) f ==>
    nth_diff_strong_int 2 (x,z) g ==>
    bounded_on_int (\x. ((nth_derivative 2 f x * g x - f x * nth_derivative 2 g x) * g x -
			 &2 * derivative g x * (derivative f x * g x - f x * derivative g x)) / 
		      (g x * g x * g x)) (x,z) dd_bounds ==>
    taylor_interval (\x. f x / g x) x y z w bounds d_bounds dd_bounds`,
  SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_div_bounds) THEN
    ASM_REWRITE_TAC[REAL_ARITH `g x pow 3 = g x * g x * (g:real->real) x`]);;


let taylor_interval_div pp th1 th2 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and
      _, approx2_th, second2_th = dest_taylor_interval_th th2 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and
      diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in

  let g_bounds_th = eval_taylor_f_bounds pp th2 and
      approx_th = lin_approx_div pp approx1_th approx2_th in
  let g_bounds = (rand o concl) g_bounds_th in
  let cond_th = check_interval_not_zero g_bounds in

  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = (dest o eval_taylor_f_bounds pp) th1 and
	g = dest g_bounds_th and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	dg = (dest o eval_taylor_df_bounds pp) th2 and
	ddf = dest dd1_th and
	ddg = dest dd2_th and
	(-) = float_interval_sub pp and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp in
      mk_bounded_on_int (((ddf * g - f * ddg) * g - two_interval * (dg * (df * g - f * dg))) / (g * (g * g))) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      g_tm = (rand o concl) diff2_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP g_bounds_th o MY_PROVE_HYP cond_th o
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_DIV' in
  let eq_th = binary_beta_eq f_tm g_tm div_op_real in
    taylor_interval_norm th0 eq_th;;


(*
let pp = 5;;
let domain_th = mk_center_domain pp one_float two_float;;
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
let th3 = taylor_interval_sub pp th1 th2;;
taylor_interval_div pp th1 th2;;
taylor_interval_div pp th3 th2;;
(* 10: 3.372 *)
test 100 (taylor_interval_div pp th1) th2;;
*)


(*************************************)
(* taylor_interval_atn *)

let TAYLOR_INTERVAL_ATN' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2] o prove)
 (`cell_domain x y z w ==>
    lin_approx (\x. atn (f x)) y bounds d_bounds ==>
    nth_diff_strong_int 2 (x,z) f ==>
    bounded_on_int (\x. (nth_derivative 2 f x * (&1 + f x * f x) - &2 * f x * derivative f x pow 2) /
		      (&1 + f x * f x) pow 2) (x,z) dd_bounds ==>
    taylor_interval (\x. atn (f x)) x y z w bounds d_bounds dd_bounds`,
  SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_atn_bounds) THEN
    ASM_REWRITE_TAC[]);;


let taylor_interval_atn pp th1 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in

  let approx_th = lin_approx_atn pp approx1_th in
  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = (dest o eval_taylor_f_bounds pp) th1 and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	ddf = dest dd1_th and
	(+) = float_interval_add pp and
	(-) = float_interval_sub pp and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp in
    let ff1 = one_interval + f * f in
      mk_bounded_on_int ((ddf * ff1 - two_interval * (f * (df * df))) / (ff1 * ff1)) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_ATN' in
  let eq_th = unary_beta_eq f_tm atn_tm in
    taylor_interval_norm th0 eq_th;;


(*
let pp = 5;;
let domain_th = mk_center_domain pp one_float two_float;;
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
let th3 = taylor_interval_add pp th1 th2;;
taylor_interval_atn pp th1;;
taylor_interval_atn pp th2;;
taylor_interval_atn pp th3;;
*)




(*************************************)
(* taylor_interval_inv *)

let TAYLOR_INTERVAL_INV' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)
 (`cell_domain x y z w ==>
    bounded_on_int f (x,z) f_bounds ==>
    interval_not_zero f_bounds ==>
    lin_approx (\x. inv (f x)) y bounds d_bounds ==>
    nth_diff_strong_int 2 (x,z) f ==>
    bounded_on_int (\x. (&2 * derivative f x pow 2 - nth_derivative 2 f x * f x) / (f x pow 3)) (x,z) dd_bounds
    ==> taylor_interval (\x. inv (f x)) x y z w bounds d_bounds dd_bounds`,
  SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_inv_bounds) THEN
    ASM_REWRITE_TAC[]);;


let taylor_interval_inv pp th1 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in

  let f_bounds_th = eval_taylor_f_bounds pp th1 and
      approx_th = lin_approx_inv pp approx1_th in
  let f_bounds = (rand o concl) f_bounds_th in
  let cond_th = check_interval_not_zero f_bounds in

  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = dest f_bounds_th and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	ddf = dest dd1_th and
	(-) = float_interval_sub pp and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp in
      mk_bounded_on_int ((two_interval * (df * df) - ddf * f) / (f * (f * f))) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; f_bounds, f_bounds_var;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_INV' in
  let eq_th = unary_beta_eq f_tm inv_tm in
    taylor_interval_norm th0 eq_th;;


(*
let pp = 5;;
let domain_th = mk_center_domain pp one_float two_float;;
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
let th3 = taylor_interval_add pp th1 th2;;
taylor_interval_inv pp th1;;
taylor_interval_inv pp th2;;
taylor_interval_inv pp th3;;
*)



(*************************************)
(* taylor_interval_sqrt *)

let TAYLOR_INTERVAL_SQRT' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)
 (`cell_domain x y z w ==>
    bounded_on_int f (x,z) f_bounds ==>
    interval_pos f_bounds ==>
    lin_approx (\x. sqrt (f x)) y bounds d_bounds ==>
    nth_diff_strong_int 2 (x,z) f ==>
    bounded_on_int (\x. (&2 * nth_derivative 2 f x * f x - derivative f x pow 2) /
		      (&4 * sqrt (f x pow 3))) (x,z) dd_bounds ==>
    taylor_interval (\x. sqrt (f x)) x y z w bounds d_bounds dd_bounds`,
  SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_sqrt_bounds) THEN
    ASM_REWRITE_TAC[]);;


let taylor_interval_sqrt pp th1 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in

  let f_bounds_th = eval_taylor_f_bounds pp th1 and
      approx_th = lin_approx_sqrt pp approx1_th in
  let f_bounds = (rand o concl) f_bounds_th in
  let cond_th = check_interval_pos f_bounds in

  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = dest f_bounds_th and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	ddf = dest dd1_th and
	(-) = float_interval_sub pp and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp and
	sqrt = float_interval_sqrt pp in
      mk_bounded_on_int ((two_interval * (ddf * f) - df * df) / (four_interval * sqrt (f * (f * f)))) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; f_bounds, f_bounds_var;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_SQRT' in
  let eq_th = unary_beta_eq f_tm sqrt_tm in
    taylor_interval_norm th0 eq_th;;


(*
let pp = 5;;
let domain_th = mk_center_domain pp one_float two_float;;
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_sqrt pp domain_th;;
let th3 = taylor_interval_add pp th1 th2;;
taylor_interval_sqrt pp th1;;
taylor_interval_sqrt pp th2;;
taylor_interval_sqrt pp th3;;
*)


(*************************************)
(* taylor_interval_acs *)

let TAYLOR_INTERVAL_ACS' = 
  (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[iabs_lt1_lemma] o
     REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)
 (`cell_domain x y z w ==>
    bounded_on_int f (x,z) f_bounds ==>
    (iabs f_bounds < &1 <=> T)==>
    lin_approx (\x. acs (f x)) y bounds d_bounds ==>
    nth_diff_strong_int 2 (x,z) f ==>
    bounded_on_int (\x. --((nth_derivative 2 f x * (&1 - f x * f x) + f x * derivative f x pow 2) /
			     sqrt ((&1 - f x * f x) pow 3))) (x,z) dd_bounds ==>
    taylor_interval (\x. acs (f x)) x y z w bounds d_bounds dd_bounds`,
  SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN
    MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_acs_bounds) THEN
    ASM_REWRITE_TAC[]);;


let taylor_interval_acs pp th1 =
  let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in
  let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in

  let f_bounds_th = eval_taylor_f_bounds pp th1 and
      approx_th = lin_approx_acs pp approx1_th in
  let f_bounds = (rand o concl) f_bounds_th in
  let cond_th = check_interval_iabs f_bounds one_float in

  let dd_th =
    let dest = dest_bounded_on_int_raw in
    let f = dest f_bounds_th and
	df = (dest o eval_taylor_df_bounds pp) th1 and
	ddf = dest dd1_th and
	(+) = float_interval_add pp and
	(-) = float_interval_sub pp and
	( * ) = float_interval_mul pp and
	(/) = float_interval_div pp and
	sqrt = float_interval_sqrt pp and
	neg = float_interval_neg in
    let ff1 = one_interval - f * f in
      mk_bounded_on_int (neg ((ddf * ff1 + f * (df * df)) / sqrt (ff1 * (ff1 * ff1)))) in

  let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and
      f_tm = (rand o concl) diff1_th and
      _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and
      dd_bounds = (rand o concl) dd_th in

  let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o 
	       MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o
	       MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o
	       INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;
		    f_tm, f_var_fun; f_bounds, f_bounds_var;
		    bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_ACS' in
  let eq_th = unary_beta_eq f_tm acs_tm in
    taylor_interval_norm th0 eq_th;;


(*
let pp = 5;;
let domain_th = mk_center_domain pp (mk_float (-5) 49) (mk_float 3 49);;
let th1 = eval_taylor_x domain_th and
    th2 = eval_taylor_atn pp domain_th;;
let th3 = taylor_interval_mul pp th1 th2;;

taylor_interval_acs pp th1;;
taylor_interval_acs pp th2;;
taylor_interval_acs pp th3;;
*)







(****************************************)
(* Composition *)

let dest_bounded_on_int_tm tm =
  let lhs, f_bounds = dest_comb tm in
  let lhs2, int_tm = dest_comb lhs in
    rand lhs2, int_tm, f_bounds;;

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


let BOUNDED_SECOND_DERIVATIVE_COMPOSE' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2] o SPEC_ALL) 
  second_derivative_compose_bounds;;

let BOUNDED_ON_INT_COMPOSE' = (UNDISCH_ALL o SPEC_ALL) bounded_on_int_compose;;

let TAYLOR_INTERVAL_NARROW' = (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[REAL_ARITH `a <= b <=> (a <= b <=> T)`] o
				 SPEC_ALL) taylor_interval_narrow;;

let BOUNDED_ON_INT_IMP_INTERVAL' = (UNDISCH_ALL o SPEC_ALL) bounded_on_int_imp_interval_arith;;

let LIN_APPROX_COMPOSE' = (UNDISCH_ALL o SPEC_ALL) lin_approx_compose;;



let taylor_interval_compose pp eval_f eval_g domain_th =
  let g_taylor = eval_g pp domain_th in
  let _, lin_g, second_g =  dest_taylor_interval_th g_taylor in
  let dg_th, g2_th = dest_has_bounded_second_derivative_th second_g in
  let g0_th = eval_taylor_f_bounds pp g_taylor in
  let g1_th = eval_taylor_df_bounds pp g_taylor in
  let g_tm, y_tm, g_bounds0, _ = dest_lin_approx (concl lin_g) in

  (* narrow domain *)
  let g0_lo, g0_hi = dest_pair g_bounds0 in
  let fu_domain = mk_center_domain (pp + 1) g0_lo g0_hi in
  let w0_tm = (rand o concl) fu_domain in

  (* wide domain *)
  let _, u_tm, _, _ = dest_cell_domain (concl fu_domain) in
  let g_lo, g_hi = (dest_pair o rand o concl) g0_th in
  let fw_domain = mk_cell_domain pp g_lo u_tm g_hi in
  let w_tm = (rand o concl) fw_domain in

  (* taylor_interval f *)
  let f_taylor = eval_f pp fw_domain in
  let f1_th = eval_taylor_df_bounds pp f_taylor in
  let _, lin_f, second_f = dest_taylor_interval_th f_taylor in
  let f_tm, _, f_bounds0, df_bounds0 = dest_lin_approx (concl lin_f) in
  let df_th, f2_th = dest_has_bounded_second_derivative_th second_f in

  (* has_bounded_second_derivative (\x. f (g x)) *)
  let _, int_tm, g_bounds = dest_bounded_on_int_tm (concl g0_th) in
  let df_tm, _, df_bounds = dest_bounded_on_int_tm (concl f1_th) in
  let ddf_tm, _, ddf_bounds = dest_bounded_on_int_tm (concl f2_th) in

  let f2_g_bounded_th = (MY_PROVE_HYP g0_th o MY_PROVE_HYP f2_th o
			   INST[ddf_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var; 
				ddf_bounds, f_bounds_var; int_tm, int_var]) BOUNDED_ON_INT_COMPOSE' in
  let f1_g_bounded_th = (MY_PROVE_HYP g0_th o MY_PROVE_HYP f1_th o
			   INST[df_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var;
				df_bounds, f_bounds_var; int_tm, int_var]) BOUNDED_ON_INT_COMPOSE' in

  let fg2_bounded_th0 = 
    let ( * ) = bounded_on_int_mul pp and
	(+) = bounded_on_int_add pp in
      (f2_g_bounded_th * (g1_th * g1_th) + f1_g_bounded_th * g2_th) in

  let dd_bounds = (rand o concl) fg2_bounded_th0 in
  let fg2_bounded_th = (MY_PROVE_HYP fg2_bounded_th0 o MY_PROVE_HYP g0_th o 
			  MY_PROVE_HYP dg_th o MY_PROVE_HYP df_th o
			  INST[f_tm, f_var_fun; g_tm, g_var_fun; int_tm, int_var; 
			       dd_bounds, dd_bounds_var; g_bounds, g_bounds_var]) 
    BOUNDED_SECOND_DERIVATIVE_COMPOSE' in

  (* lin_approx (\x. f (g x)) *)
  let fu_taylor = (MY_PROVE_HYP (float_le g_lo g0_lo) o MY_PROVE_HYP (float_le g0_hi g_hi) o
		     MY_PROVE_HYP fu_domain o MY_PROVE_HYP f_taylor o
		     INST[g0_lo, x0_var_real; u_tm, y_var_real; g0_hi, z0_var_real; w0_tm, w0_var_real;
			  f_tm, f_var_fun; g_lo, x_var_real; g_hi, z_var_real; w_tm, w_var_real;
			  f_bounds0, f_bounds_var; df_bounds0, df_bounds_var; ddf_bounds, dd_bounds_var])
    TAYLOR_INTERVAL_NARROW' in

  let df0_th = 
    let _, _, f_second = dest_taylor_interval_th fu_taylor in
      (fst o dest_has_bounded_second_derivative_th) f_second in
  let f00_th = eval_taylor_f_bounds pp fu_taylor in
  let f01_th = eval_taylor_df_bounds pp fu_taylor in
  let fg_bounds0 = (rand o concl) f00_th in
  let dfg_bounds0 = (rand o concl) f01_th in

  let dg0_th, int_g_th, int_dg_th = lin_approx_components lin_g in
  let gy_tm, _ = dest_interval_arith (concl int_g_th) in

  let int_df_g_th = (MY_PROVE_HYP int_g_th o MY_PROVE_HYP f01_th o
		       INST[df_tm, f_var_fun; gy_tm, y_var_real; g_bounds0, int_var; dfg_bounds0, f_bounds_var])
    BOUNDED_ON_INT_IMP_INTERVAL' in

  let int_dfg_th = float_interval_mul pp int_dg_th int_df_g_th in
  let dfg_bounds00 = rand (concl int_dfg_th) in

  let fg_lin_th = (MY_PROVE_HYP int_dfg_th o MY_PROVE_HYP int_g_th o MY_PROVE_HYP f00_th o 
		     MY_PROVE_HYP dg0_th o MY_PROVE_HYP df0_th o
		     INST[f_tm, f_var_fun; g_tm, g_var_fun; y_tm, y_var_real; dfg_bounds00, d_bounds_var;
			  g_bounds0, g_bounds_var; fg_bounds0, f_bounds_var]) LIN_APPROX_COMPOSE' in

  (* beta reduction *)
  let gx_tm = mk_comb (g_tm, x_var_real) in
  let gx_th = if is_abs g_tm then BETA gx_tm else REFL gx_tm in

  let fgx_th0 = MK_COMB (REFL f_tm, gx_th) in
  let fgx_eq_th = ABS x_var_real 
    (if is_abs f_tm then TRANS fgx_th0 (BETA_CONV (rand (concl fgx_th0))) else fgx_th0) in

  let fg_lin_th1 = norm_lin_approx fg_lin_th fgx_eq_th and
      fg2_bounded_th1 = norm_second_derivative fg2_bounded_th fgx_eq_th in

    mk_taylor_interval_th domain_th fg_lin_th1 fg2_bounded_th1;;