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

module M_taylor_old = struct

let gen_second_bounded_eq_thm n =
  let ty, _, x_var, _, _, _, domain_var = get_types_and_vars n in
  let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(j).(i)) (1--n)) (1--n) in
  let dd_bounds_list = mk_list (map (fun l -> mk_list (l, real_pair_ty)) dd_vars, real_pair_list_ty) in
  let th0 = (SPECL[domain_var; dd_bounds_list] o inst_first_type_var ty) second_bounded in
  let th1 = (CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[all_n]) th0 in
    th1;;

let gen_second_bounded_poly_thm poly_tm partials2 =
  let x_var, _ = dest_abs poly_tm in
  let n = get_dim x_var in
  let partials2' = List.flatten partials2 in
  let second_th = (REWRITE_RULE partials2' o SPECL [poly_tm]) (gen_second_bounded_eq_thm n) in
    second_th;;


let gen_second_bounded_poly_thm0 poly_tm =
  let x_var, _ = dest_abs poly_tm in
  let n = get_dim x_var in
  let partials = map (fun i -> gen_partial_poly i poly_tm) (1--n) in
  let get_partial i eq_th = 
    let partial_i = gen_partial_poly i (rand (concl eq_th)) in
    let pi = (rator o lhand o concl) partial_i in
      REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in
  let partials2 = map (fun th -> map (fun i -> get_partial i th) (1--n)) partials in
    gen_second_bounded_poly_thm poly_tm partials2;;


(* eval_second_bounded *)
let eval_second_bounded pp0 second_bounded_th =
  let poly_tm = (lhand o rator o lhand o concl) second_bounded_th in
  let th0 = second_bounded_th in
  let n = (get_dim o fst o dest_abs) poly_tm in
  let x_vector = mk_vector_list (map (fun i -> x_vars_array.(i)) (1--n)) and
      z_vector = mk_vector_list (map (fun i -> z_vars_array.(i)) (1--n)) in
  let _, _, _, _, _, _, domain_var = get_types_and_vars n in

  let th1 = INST[mk_pair (x_vector, z_vector), domain_var] th0 in
  let th2 = REWRITE_RULE[IN_INTERVAL; dimindex_array.(n)] th1 in
  let th3 = REWRITE_RULE[gen_in_interval n; GSYM interval_arith] th2 in
  let th4 = (REWRITE_RULE[CONJ_ACI] o REWRITE_RULE (Array.to_list comp_thms_array.(n))) th3 in
  let final_th0 = (UNDISCH_ALL o MATCH_MP iffRL) th4 in

  let x_var, h_tm = (dest_forall o hd o hyp) final_th0 in
  let _, h2 = dest_imp h_tm in
  let concl_ints = striplist dest_conj h2 in

  let i_funs = map (fun int -> 
		      let expr, var = dest_interval_arith int in
			(eval_constants pp0 o build_interval_fun) expr, var) concl_ints in

  let rec split_rules i_list =
    match i_list with
      | [] -> ([], [])
      | ((i_fun, var_tm) :: es) -> 
	  let th_list, i_list' = split_rules es in
	    match i_fun with
	      | Int_const th -> (var_tm, th) :: th_list, i_list'
	      | _ -> th_list, (var_tm, i_fun) :: i_list' in

  let const_th_list, i_list0 = split_rules i_funs in
  let th5 = itlist (fun (var_tm, th) th0 -> 
		      let b_tm = rand (concl th) in
			(REWRITE_RULE[th] o INST[b_tm, var_tm]) th0) const_th_list (SYM th4) in
  let final_th = REWRITE_RULE[GSYM IMP_IMP] th5 in
  let v_list, i_list' = unzip i_list0 in
  let i_list = find_and_replace_all i_list' [] in

    fun pp x_vector_tm z_vector_tm ->
      let x_vals = dest_vector x_vector_tm and
	  z_vals = dest_vector z_vector_tm in
	if length x_vals <> n or length z_vals <> n then 
	  failwith (sprintf "Wrong vector size; expected size: %d" n)
	else
	  let x_vars = map (fun i -> x_vars_array.(i)) (1--n) and
	      z_vars = map (fun i -> z_vars_array.(i)) (1--n) in

	  let inst_th = (INST (zip x_vals x_vars) o INST (zip z_vals z_vars)) final_th in
	    if (not o is_eq) (concl inst_th) then inst_th 
	    else
	      let x_var, lhs = (dest_forall o lhand o concl) inst_th in
	      let hs = (butlast o striplist dest_imp) lhs in
	      let vars = map (rand o rator) hs in
	      let int_vars = zip vars (map ASSUME hs) in

	      let dd_ints = eval_interval_fun_list pp i_list int_vars in
	      let inst_dd = map2 (fun var th -> (rand o concl) th, var) v_list dd_ints in
	      let inst_th2 = INST inst_dd inst_th in

	      let conj_th = end_itlist CONJ dd_ints in
	      let lhs_th = GEN x_var (itlist DISCH hs conj_th) in
		EQ_MP inst_th2 lhs_th;;



let eval_second_bounded_poly0 pp0 poly_tm =
  eval_second_bounded pp0 (gen_second_bounded_poly_thm0 poly_tm);;


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

let eval_m_taylor pp0 diff2c_th lin_th second_th =
  let poly_tm = (rand o concl) diff2c_th in
  let n = (get_dim o fst o dest_abs) poly_tm in
  let eval_lin = eval_lin_approx pp0 lin_th and
      eval_second = eval_second_bounded pp0 second_th in

  let ty, _, x_var, f_var, y_var, w_var, domain_var = get_types_and_vars n in
  let th0 = (SPEC_ALL o inst_first_type_var ty) m_taylor_interval in
  let th1 = INST[poly_tm, f_var] th0 in
  let th2 = (UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o MATCH_MP iffRL o REWRITE_RULE[diff2c_th]) th1 in

    fun p_lin p_second domain_th ->
      let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
      let x_tm, z_tm = dest_pair domain_tm in

      let lin_th = eval_lin p_lin y_tm and
	  second_th = eval_second p_second x_tm z_tm in

      let _, _, f_bounds, df_bounds_list = dest_lin_approx (concl lin_th) in
      let dd_bounds_list = (rand o concl) second_th in
      let df_var = mk_var ("d_bounds_list", type_of df_bounds_list) and
	  dd_var = mk_var ("dd_bounds_list", type_of dd_bounds_list) in

	(MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP second_th o
	   INST[domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
		f_bounds, f_bounds_var; df_bounds_list, df_var; dd_bounds_list, dd_var]) th2;;


let eval_m_taylor_poly0 pp0 poly_tm =
  let diff2_th = gen_diff2c_domain_poly poly_tm in
  let x_var, _ = dest_abs poly_tm in
  let n = get_dim x_var in
  let partials = map (fun i -> gen_partial_poly i poly_tm) (1--n) in
  let get_partial i eq_th = 
    let partial_i = gen_partial_poly i (rand (concl eq_th)) in
    let pi = (rator o lhand o concl) partial_i in
      REWRITE_RULE[GSYM partial2] (TRANS (AP_TERM pi eq_th) partial_i) in
  let partials2 = map (fun th -> map (fun i -> get_partial i th) (1--n)) partials in
  let second_th = gen_second_bounded_poly_thm poly_tm partials2 in
  let diff_th = gen_diff_poly poly_tm in
  let lin_th = gen_lin_approx_poly_thm poly_tm diff_th partials in
    eval_m_taylor pp0 diff2_th lin_th second_th;;



(********************************)
(* m_taylor_error *)


(* Sum of the list elements *)

let ITLIST2_EQ_SUM = 
prove(`!(f:A->real) l1 l2. LENGTH l1 = LENGTH l2 ==> ITLIST2 (\x y z. x * f y + z) l1 l2 (&0) = sum (1..(LENGTH l1)) (\i. EL (i - 1) l1 * f (EL (i - 1) l2))`,
GEN_TAC THEN LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; ITLIST2] THEN TRY ARITH_TAC THENL [ REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH]; ALL_TAC ] THEN REWRITE_TAC[eqSS] THEN DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN REWRITE_TAC[GSYM add1n] THEN new_rewrite [] [] SUM_ADD_SPLIT THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[TWO; add1n; SUM_SING_NUMSEG; subnn; EL; HD] THEN REWRITE_TAC[GSYM addn1; SUM_OFFSET; REAL_EQ_ADD_LCANCEL] THEN MATCH_MP_TAC SUM_EQ THEN move ["i"] THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> (i + 1) - 1 = SUC (i - 1)`; EL; TL]);;
let M_TAYLOR_ERROR_ITLIST2 = 
prove(`!f domain y w dd_bounds_list error. m_cell_domain domain y (vector w) ==> second_bounded (f:real^N->real) domain dd_bounds_list ==> LENGTH w = dimindex (:N) ==> LENGTH dd_bounds_list = dimindex (:N) ==> ALL (\list. LENGTH list = dimindex (:N)) dd_bounds_list ==> ITLIST2 (\x list z. x * ITLIST2 (\a b c. a * iabs b + c) w list (&0) + z) w dd_bounds_list (&0) <= error ==> m_taylor_error f domain (vector w) error`,
REWRITE_TAC[second_bounded; m_taylor_error] THEN REPEAT GEN_TAC THEN set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN move ["domain";
"second"; "lw"; "ldd"; "ldd_all"; "s_le"; "x"; "x_in"] THEN SUBGOAL_THEN `!i. i IN 1..dimindex (:N) ==> &0 <= EL (i - 1) w` (LABEL_TAC "w_ge0") THENL [ GEN_TAC THEN DISCH_TAC THEN REMOVE_THEN "domain" MP_TAC THEN new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN DISCH_THEN (MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC ] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "s" THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN move ["i"; "i_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN USE_THEN "i_in" (ASSUME_TAC o REWRITE_RULE[IN_NUMSEG]) THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[] THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THENL [ REMOVE_THEN "ldd_all" MP_TAC THEN REWRITE_TAC[GSYM ALL_EL] THEN DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN ANTS_TAC THENL [ ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN (fun th -> REWRITE_TAC[th]); ALL_TAC ] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN move ["j"; "j_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN USE_THEN "j_in" (ASSUME_TAC o REWRITE_RULE[IN_NUMSEG]) THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[] THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[ALL_N_EL] THEN DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN ANTS_TAC THENL [ REMOVE_THEN "i_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN ANTS_TAC THENL [ REMOVE_THEN "ldd_all" MP_TAC THEN REWRITE_TAC[GSYM ALL_EL] THEN DISCH_THEN (new_rewrite [] []) THEN ASM_REWRITE_TAC[] THENL [ REMOVE_THEN "i_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN REMOVE_THEN "j_in" MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN SUBGOAL_THEN `1 + j - 1 = j /\ 1 + i - 1 = i` (fun th -> REWRITE_TAC[th]) THENL [ REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN REWRITE_TAC[partial2] THEN DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;
let M_TAYLOR_ERROR_LIST_SUM2 = 
prove(`!f domain y w dd_bounds_list error. m_cell_domain domain y (vector w) ==> second_bounded (f:real^N->real) domain dd_bounds_list ==> LENGTH w = dimindex (:N) ==> LENGTH dd_bounds_list = dimindex (:N) ==> ALL (\list. LENGTH list = dimindex (:N)) dd_bounds_list ==> list_sum2 (error_mul_f1 w) w dd_bounds_list <= error ==> m_taylor_error f domain (vector w) error`,
(**********************************) let m_taylor_error_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i)] o inst_first_type_var (n_type_array.(i))) M_TAYLOR_ERROR_LIST_SUM2);; let REFL_CONV tm = let rhs = rand tm in let th0 = EQT_INTRO (REFL rhs) in th0;; let eval_m_taylor_error n pp m_taylor_th = let domain_th, _, _, second_th = dest_m_taylor_thms n m_taylor_th in let f_tm = (rand o rator o rator o concl) second_th in let domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th in let dd_bounds_list = (rand o concl) second_th in let w_list = rand w_tm in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP second_th o INST[dd_bounds_list, dd_bounds_list_var; w_list, w_var_list; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_error_array.(n) in let len_dd = eval_length dd_bounds_list in let len_w = eval_length w_list in let th1 = (MY_PROVE_HYP len_dd o MY_PROVE_HYP len_w) th0 in let [all_tm; sum2_tm] = hyp th1 in let l_conv = (BETA_CONV THENC LAND_CONV length_conv THENC REFL_CONV) in let all_len = EQT_ELIM (all_conv_univ l_conv all_tm) in let sum2_le_th = list_sum2_le_conv pp (error_mul_f1_le_conv w_list) (lhand sum2_tm) in let error_tm = (rand o concl) sum2_le_th in (MY_PROVE_HYP all_len o MY_PROVE_HYP sum2_le_th o INST[error_tm, error_var]) th1;; (**********************) (* taylor_upper_bound *) (* upper *)
let M_TAYLOR_UPPER_BOUND' = 
prove(`m_cell_domain domain (y:real^N) (vector w) /\ diff2c_domain domain f /\ m_lin_approx f y (f_lo, f_hi) d_bounds_list /\ m_taylor_error f domain (vector w) error /\ list_sum2 error_mul_f2 w d_bounds_list <= b /\ b + inv(&2) * error <= a /\ f_hi + a <= hi /\ LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==> (!p. p IN interval [domain] ==> f p <= hi)`,
REWRITE_TAC[m_lin_approx; interval_arith; list_sum2; error_mul_f2; ALL_N_EL] THEN set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN STRIP_TAC THEN SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL [ UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN SIMP_TAC[diff2_domain; diff2c_domain; diff2c]; ALL_TAC ] THEN apply_tac m_taylor_upper_bound THEN MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `f_hi:real`] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `f_hi + a:real` THEN ASM_REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `b + inv (&2) * error` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "s" THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN new_rewrite [] [] REAL_MUL_SYM THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[VECTOR_COMPONENT; REAL_LE_REFL; REAL_ABS_POS] THEN CONJ_TAC THENL [ UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN DISCH_THEN (MP_TAC o SPEC `x:num`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC ] THEN FIRST_X_ASSUM (MP_TAC o SPEC `x - 1`) THEN ANTS_TAC THENL [ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN SUBGOAL_THEN `1 + x - 1 = x` (fun th -> REWRITE_TAC[th]) THENL [ POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;
(* lower *)
let M_TAYLOR_LOWER_BOUND' = 
prove(`m_cell_domain domain (y:real^N) (vector w) /\ diff2c_domain domain f /\ m_lin_approx f y (f_lo, f_hi) d_bounds_list /\ m_taylor_error f domain (vector w) error /\ list_sum2 error_mul_f2 w d_bounds_list <= b /\ b + inv(&2) * error <= a /\ lo <= f_lo - a /\ LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==> (!p. p IN interval [domain] ==> lo <= f p)`,
REWRITE_TAC[m_lin_approx; interval_arith; list_sum2; error_mul_f2; ALL_N_EL] THEN set_tac "s" `ITLIST2 _1 _2 _3 _4` THEN STRIP_TAC THEN SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL [ UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN SIMP_TAC[diff2_domain; diff2c_domain; diff2c]; ALL_TAC ] THEN apply_tac m_taylor_lower_bound THEN MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `f_lo:real`] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `f_lo - a:real` THEN ASM_REWRITE_TAC[real_div; real_sub] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_LE_REFL; REAL_LE_NEG] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `b + inv (&2) * error` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `s:real` THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "s" THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN REPEAT STRIP_TAC THEN new_rewrite [] [] REAL_MUL_SYM THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC[VECTOR_COMPONENT; REAL_LE_REFL; REAL_ABS_POS] THEN CONJ_TAC THENL [ UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN DISCH_THEN (MP_TAC o SPEC `x:num`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC ] THEN FIRST_X_ASSUM (MP_TAC o SPEC `x - 1`) THEN ANTS_TAC THENL [ POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN SUBGOAL_THEN `1 + x - 1 = x` (fun th -> REWRITE_TAC[th]) THENL [ POP_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC; ALL_TAC ] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;
(* bound *)
let M_TAYLOR_BOUND' = 
prove(`m_cell_domain domain (y:real^N) (vector w) /\ diff2c_domain domain f /\ m_lin_approx f y (f_lo, f_hi) d_bounds_list /\ m_taylor_error f domain (vector w) error /\ list_sum2 error_mul_f2 w d_bounds_list <= b /\ b + inv(&2) * error <= a /\ lo <= f_lo - a /\ f_hi + a <= hi /\ LENGTH w = dimindex (:N) /\ LENGTH d_bounds_list = dimindex (:N) ==> (!x. x IN interval [domain] ==> interval_arith (f x) (lo, hi))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[interval_arith] THEN MP_TAC M_TAYLOR_UPPER_BOUND' THEN MP_TAC M_TAYLOR_LOWER_BOUND' THEN ASM_REWRITE_TAC[] THEN REPEAT (DISCH_THEN (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC));;
(* arrays *) let m_taylor_upper_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i))) M_TAYLOR_UPPER_BOUND');; let m_taylor_lower_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i))) M_TAYLOR_LOWER_BOUND');; let m_taylor_bound_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else (MY_RULE_NUM o REWRITE_RULE[dimindex_array.(i); float_inv2_th] o inst_first_type_var (n_type_array.(i))) M_TAYLOR_BOUND');; (* upper *) let b_var_real = `b:real`;; let eval_m_taylor_upper_bound n pp m_taylor_th = let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in let error_th = eval_m_taylor_error n pp m_taylor_th in let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and error_tm = (rand o concl) error_th in let w_list = rand w_tm and f_lo, f_hi = dest_pair f_bounds in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_upper_array.(n) in let len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in let sum2_tm = (C List.nth 2 o hyp) th1 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let b_tm = (rand o concl) sum2_le_th in let ineq1_th = let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in mk_refl_ineq b_tm + float_inv2 * error_tm in let a_tm = (rand o concl) ineq1_th in let ineq2_th = float_add_hi pp f_hi a_tm in let hi_tm = (rand o concl) ineq2_th in (MY_PROVE_HYP ineq2_th o MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o INST[a_tm, a_var_real; b_tm, b_var_real; hi_tm, hi_var_real]) th1;; (* lower *) let eval_m_taylor_lower_bound n pp m_taylor_th = let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in let error_th = eval_m_taylor_error n pp m_taylor_th in let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and error_tm = (rand o concl) error_th in let w_list = rand w_tm and f_lo, f_hi = dest_pair f_bounds in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_lower_array.(n) in let len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in let sum2_tm = (C List.nth 2 o hyp) th1 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let b_tm = (rand o concl) sum2_le_th in let ineq1_th = let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in mk_refl_ineq b_tm + float_inv2 * error_tm in let a_tm = (rand o concl) ineq1_th in let ineq2_th = float_sub_lo pp f_lo a_tm in let lo_tm = (lhand o concl) ineq2_th in (MY_PROVE_HYP ineq2_th o MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o INST[a_tm, a_var_real; b_tm, b_var_real; lo_tm, lo_var_real]) th1;; (* bound *) let eval_m_taylor_bound n pp m_taylor_th = let domain_th, diff_th, lin_th, _ = dest_m_taylor_thms n m_taylor_th in let error_th = eval_m_taylor_error n pp m_taylor_th in let f_tm, _, f_bounds, d_bounds_list = dest_lin_approx (concl lin_th) and domain_tm, y_tm, w_tm = (dest_m_cell_domain o concl) domain_th and error_tm = (rand o concl) error_th in let w_list = rand w_tm and f_lo, f_hi = dest_pair f_bounds in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP diff_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP error_th o INST[d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_lo, f_lo_var; f_hi, f_hi_var; error_tm, error_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_bound_array.(n) in let len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th) th0 in let sum2_tm = (C List.nth 3 o hyp) th1 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let b_tm = (rand o concl) sum2_le_th in let ineq1_th = let ( * ), ( + ) = float_mul_hi pp, add_ineq_hi pp in mk_refl_ineq b_tm + float_inv2 * error_tm in let a_tm = (rand o concl) ineq1_th in let ineq2_th = float_add_hi pp f_hi a_tm in let hi_tm = (rand o concl) ineq2_th in let ineq3_th = float_sub_lo pp f_lo a_tm in let lo_tm = (lhand o concl) ineq3_th in (MY_PROVE_HYP ineq3_th o MY_PROVE_HYP ineq2_th o MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o INST[a_tm, a_var_real; b_tm, b_var_real; hi_tm, hi_var_real; lo_tm, lo_var_real]) th1;; (******************************) (* taylor_upper_partial_bound *) (* taylor_lower_partial_bound *) (* upper *)
let M_TAYLOR_UPPER_PARTIAL_BOUND' = 
prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\ i IN 1..dimindex (:N) /\ EL (i - 1) d_bounds_list = (df_lo, df_hi) /\ EL (i - 1) dd_bounds_list = dd_list /\ LENGTH d_bounds_list = dimindex (:N) /\ LENGTH dd_bounds_list = dimindex (:N) /\ LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\ list_sum2 error_mul_f2 w dd_list <= error /\ df_hi + error <= hi ==> (!p. p IN interval [domain] ==> partial i f p <= hi)`,
REWRITE_TAC[m_taylor_interval; m_lin_approx; second_bounded; ALL_N_EL] THEN STRIP_TAC THEN SUBGOAL_THEN `1 <= i /\ i <= dimindex (:N)` (LABEL_TAC "i_in") THENL [ ASM_REWRITE_TAC[GSYM IN_NUMSEG]; ALL_TAC ] THEN SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL [ UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN SIMP_TAC[diff2_domain; diff2c_domain; diff2c]; ALL_TAC ] THEN apply_tac m_taylor_upper_partial_bound THEN MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `df_hi:real`] THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> 1 + i - 1 = i`; interval_arith] THEN DISCH_THEN (fun th -> ALL_TAC) THEN REWRITE_TAC[m_taylor_partial_error] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `list_sum2 error_mul_f2 w dd_list <= error` THEN REWRITE_TAC[list_sum2; error_mul_f2] THEN MATCH_MP_TAC (REWRITE_RULE[GSYM IMP_IMP] REAL_LE_TRANS) THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN move ["j";
"j_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [ UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN DISCH_THEN (MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC ] THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN ASM_SIMP_TAC[ARITH_RULE `1 <= j /\ j <= n ==> j - 1 < n`] THEN ASM_SIMP_TAC[ARITH_RULE `!i. 1 <= i ==> 1 + i - 1 = i`; GSYM partial2] THEN DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);; (* lower *)
let M_TAYLOR_LOWER_PARTIAL_BOUND' = 
prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\ i IN 1..dimindex (:N) /\ EL (i - 1) d_bounds_list = (df_lo, df_hi) /\ EL (i - 1) dd_bounds_list = dd_list /\ LENGTH d_bounds_list = dimindex (:N) /\ LENGTH dd_bounds_list = dimindex (:N) /\ LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\ list_sum2 error_mul_f2 w dd_list <= error /\ lo <= df_lo - error ==> (!p. p IN interval [domain] ==> lo <= partial i f p)`,
REWRITE_TAC[m_taylor_interval; m_lin_approx; second_bounded; ALL_N_EL] THEN STRIP_TAC THEN SUBGOAL_THEN `1 <= i /\ i <= dimindex (:N)` (LABEL_TAC "i_in") THENL [ ASM_REWRITE_TAC[GSYM IN_NUMSEG]; ALL_TAC ] THEN SUBGOAL_THEN `diff2_domain domain (f:real^N->real)` ASSUME_TAC THENL [ UNDISCH_TAC `diff2c_domain domain (f:real^N->real)` THEN SIMP_TAC[diff2_domain; diff2c_domain; diff2c]; ALL_TAC ] THEN apply_tac m_taylor_lower_partial_bound THEN MAP_EVERY EXISTS_TAC [`y:real^N`; `vector w:real^N`; `error:real`; `df_lo:real`] THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i ==> 1 + i - 1 = i`; interval_arith] THEN DISCH_THEN (fun th -> ALL_TAC) THEN REWRITE_TAC[m_taylor_partial_error] THEN REPEAT STRIP_TAC THEN UNDISCH_TAC `list_sum2 error_mul_f2 w dd_list <= error` THEN REWRITE_TAC[list_sum2; error_mul_f2] THEN MATCH_MP_TAC (REWRITE_RULE[GSYM IMP_IMP] REAL_LE_TRANS) THEN new_rewrite [] [] ITLIST2_EQ_SUM THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG] THEN move ["j";
"j_in"] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [ UNDISCH_TAC `m_cell_domain domain (y:real^N) (vector w)` THEN new_rewrite [] [] pair_eq THEN REWRITE_TAC[m_cell_domain] THEN DISCH_THEN (MP_TAC o SPEC `j:num`) THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[VECTOR_COMPONENT] THEN REAL_ARITH_TAC; ALL_TAC ] THEN FIRST_X_ASSUM (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN (MP_TAC o SPEC `i - 1`) THEN ASM_SIMP_TAC[ARITH_RULE `1 <= i /\ i <= n ==> i - 1 < n`] THEN DISCH_THEN (MP_TAC o SPEC `j - 1`) THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[IN_NUMSEG] THEN DISCH_TAC THEN ASM_SIMP_TAC[ARITH_RULE `1 <= j /\ j <= n ==> j - 1 < n`] THEN ASM_SIMP_TAC[ARITH_RULE `!i. 1 <= i ==> 1 + i - 1 = i`; GSYM partial2] THEN DISCH_THEN (MP_TAC o MATCH_MP interval_arith_abs_le) THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[REAL_LE_REFL]);;
let M_TAYLOR_PARTIAL_BOUND' = 
prove(`m_taylor_interval f domain (y:real^N) (vector w) f_bounds d_bounds_list dd_bounds_list /\ i IN 1..dimindex (:N) /\ EL (i - 1) d_bounds_list = (df_lo, df_hi) /\ EL (i - 1) dd_bounds_list = dd_list /\ LENGTH d_bounds_list = dimindex (:N) /\ LENGTH dd_bounds_list = dimindex (:N) /\ LENGTH dd_list = dimindex (:N) /\ LENGTH w = dimindex (:N) /\ list_sum2 error_mul_f2 w dd_list <= error /\ df_hi + error <= hi ==> lo <= df_lo - error ==> (!x. x IN interval [domain] ==> interval_arith (partial i f x) (lo, hi))`,
REPEAT STRIP_TAC THEN REWRITE_TAC[interval_arith] THEN MP_TAC M_TAYLOR_UPPER_PARTIAL_BOUND' THEN MP_TAC M_TAYLOR_LOWER_PARTIAL_BOUND' THEN ASM_REWRITE_TAC[] THEN REPEAT (DISCH_THEN (MP_TAC o SPEC `x:real^N`) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC));;
(* The (n, i)-th element is the theorem |- i IN 1..dimindex (:n) *) let i_in_array = Array.init (max_dim + 1) (fun i -> Array.init (i + 1) (fun j -> if j < 1 then TRUTH else let j_tm = mk_small_numeral j in let tm0 = `j IN 1..dimindex (:N)` in let tm1 = (subst [j_tm, `j:num`] o inst [n_type_array.(i), nty]) tm0 in prove(tm1, REWRITE_TAC[dimindex_array.(i); IN_NUMSEG] THEN ARITH_TAC)));; let m_taylor_upper_partial_array = Array.init (max_dim + 1) (fun i -> Array.init (i + 1) (fun j -> if j < 1 then TRUTH else let j_tm = mk_small_numeral j in (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i)) M_TAYLOR_UPPER_PARTIAL_BOUND'));; let m_taylor_lower_partial_array = Array.init (max_dim + 1) (fun i -> Array.init (i + 1) (fun j -> if j < 1 then TRUTH else let j_tm = mk_small_numeral j in (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i)) M_TAYLOR_LOWER_PARTIAL_BOUND'));; let m_taylor_interval_partial_array = Array.init (max_dim + 1) (fun i -> Array.init (i + 1) (fun j -> if j < 1 then TRUTH else let j_tm = mk_small_numeral j in (MY_RULE_NUM o CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[dimindex_array.(i); IN_NUMSEG] o INST[j_tm, `i:num`] o inst_first_type_var n_type_array.(i)) M_TAYLOR_PARTIAL_BOUND'));; (* upper_partial *) let eval_m_taylor_upper_partial n pp i m_taylor_th = let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = dest_m_taylor (concl m_taylor_th) in let w_list = rand w_tm in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP m_taylor_th o INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_bounds, f_bounds_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_upper_partial_array.(n).(i) in let el_dd_list_tm = (hd o hyp) th0 in let dd_list_th = el_conv (lhand el_dd_list_tm) in let dd_list_tm = (rand o concl) dd_list_th in let len_dd_list_th = eval_length dd_list_tm and len_dd_th = eval_length dd_bounds_list and len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o INST[dd_list_tm, dd_list_var]) th0 in let el_d_list_tm = (hd o hyp) th1 in let d_list_th = el_conv (lhand el_d_list_tm) in let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in let sum2_tm = (C List.nth 1 o hyp) th2 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let error_tm = (rand o concl) sum2_le_th in let ineq1_th = float_add_hi pp df_hi error_tm in let hi_tm = (rand o concl) ineq1_th in (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o INST[error_tm, error_var; hi_tm, hi_var_real]) th2;; (* lower_partial *) let eval_m_taylor_lower_partial n pp i m_taylor_th = let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = dest_m_taylor (concl m_taylor_th) in let w_list = rand w_tm in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP m_taylor_th o INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_bounds, f_bounds_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_lower_partial_array.(n).(i) in let el_dd_list_tm = (hd o hyp) th0 in let dd_list_th = el_conv (lhand el_dd_list_tm) in let dd_list_tm = (rand o concl) dd_list_th in let len_dd_list_th = eval_length dd_list_tm and len_dd_th = eval_length dd_bounds_list and len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o INST[dd_list_tm, dd_list_var]) th0 in let el_d_list_tm = (hd o hyp) th1 in let d_list_th = el_conv (lhand el_d_list_tm) in let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in let sum2_tm = (C List.nth 1 o hyp) th2 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let error_tm = (rand o concl) sum2_le_th in let ineq1_th = float_sub_lo pp df_lo error_tm in let lo_tm = (lhand o concl) ineq1_th in (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP sum2_le_th o INST[error_tm, error_var; lo_tm, lo_var_real]) th2;; (* interval_partial *) let eval_m_taylor_interval_partial n pp i m_taylor_th = let f_tm, domain_tm, y_tm, w_tm, f_bounds, d_bounds_list, dd_bounds_list = dest_m_taylor (concl m_taylor_th) in let w_list = rand w_tm in let y_var = mk_var ("y", type_of y_tm) and f_var = mk_var ("f", type_of f_tm) and domain_var = mk_var ("domain", type_of domain_tm) in let th0 = (MY_PROVE_HYP m_taylor_th o INST[dd_bounds_list, dd_bounds_list_var; d_bounds_list, d_bounds_list_var; w_list, w_var_list; f_bounds, f_bounds_var; domain_tm, domain_var; y_tm, y_var; f_tm, f_var]) m_taylor_interval_partial_array.(n).(i) in let el_dd_list_tm = (hd o hyp) th0 in let dd_list_th = el_conv (lhand el_dd_list_tm) in let dd_list_tm = (rand o concl) dd_list_th in let len_dd_list_th = eval_length dd_list_tm and len_dd_th = eval_length dd_bounds_list and len_d_th = eval_length d_bounds_list and len_w_th = eval_length w_list in let th1 = (MY_PROVE_HYP len_dd_list_th o MY_PROVE_HYP len_dd_th o MY_PROVE_HYP len_d_th o MY_PROVE_HYP len_w_th o MY_PROVE_HYP dd_list_th o INST[dd_list_tm, dd_list_var]) th0 in let el_d_list_tm = (hd o hyp) th1 in let d_list_th = el_conv (lhand el_d_list_tm) in let df_lo, df_hi = (dest_pair o rand o concl) d_list_th in let th2 = (MY_PROVE_HYP d_list_th o INST[df_lo, df_lo_var; df_hi, df_hi_var]) th1 in let sum2_tm = (C List.nth 2 o hyp) th2 in let sum2_le_th = list_sum2_le_conv pp error_mul_f2_le_conv2 (lhand sum2_tm) in let error_tm = (rand o concl) sum2_le_th in let ineq1_th = float_sub_lo pp df_lo error_tm in let lo_tm = (lhand o concl) ineq1_th in let ineq2_th = float_add_hi pp df_hi error_tm in let hi_tm = (rand o concl) ineq2_th in (MY_PROVE_HYP ineq1_th o MY_PROVE_HYP ineq2_th o MY_PROVE_HYP sum2_le_th o INST[error_tm, error_var; lo_tm, lo_var_real; hi_tm, hi_var_real]) th2;; end;;