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 *)
"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_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 *)
(* lower *)
(* bound *)
(* 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 *)
"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 *)
"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]);;
(* 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;;