1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
4 Arith_cache.reset_stat();
5 Arith_cache.reset_cache();
6 Arith_float.reset_stat();
7 Arith_float.reset_cache();;
13 let poly1 = expr_to_vector_fun `x1 * x2 * x3 + x2 * (x4 + x5) pow 3`;;
14 let n = (get_dim o fst o dest_abs) poly1;;
15 let xx = `[-- &3; -- &3; -- &3; -- &3; -- &3]` and
16 zz = `[&2; &2; &2; &2; &2]`;;
18 let xx1 = convert_to_float_list n true xx and
19 zz1 = convert_to_float_list n false zz;;
21 let eval_poly, tf, ti = mk_verification_functions pp poly1 false `&0`;;
22 let dom_th = mk_m_center_domain n pp xx1 zz1;;
24 let th = eval_poly.taylor pp pp dom_th;;
28 test 100 (eval_poly.taylor pp pp) dom_th;;
30 test 100 (eval_poly.taylor pp pp) dom_th;;
36 test 100 (eval_m_taylor_add n pp pp th) th;;
38 test 100 (eval_m_taylor_add n pp pp th) th;;
43 let p_lin = pp and p_second = pp and
44 taylor1_th = th and taylor2_th = th;;
48 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th;;
49 let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th;;
50 let f1_tm = (rand o concl) diff2_f1_th and
51 f2_tm = (rand o concl) diff2_f2_th;;
52 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th);;
53 let ty = type_of y_tm;;
55 let x_var = mk_var ("x", ty) and
56 y_var = mk_var ("y", ty) and
57 w_var = mk_var ("w", ty) and
58 f_var = mk_var ("f", type_of f1_tm) and
59 g_var = mk_var ("g", type_of f2_tm) and
60 domain_var = mk_var ("domain", type_of domain_tm);;
62 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
63 _, bounds2_th, df2_th = m_lin_approx_components n lin2_th;;
65 let bounds_th = float_interval_add p_lin bounds1_th bounds2_th;;
66 let bounds_tm = (rand o concl) bounds_th;;
68 let add_lemma0 = (INST[f1_tm, f_var; f2_tm, g_var; y_tm, x_var] o
69 INST_TYPE[n_type_array.(n), nty]) add_partial_lemma';;
72 let add_th = float_interval_add p_lin th1 th2 in
73 let int_tm = rand (concl add_th) and
74 i_tm = (rand o rator o rator o lhand) (concl th1) in
75 let th0 = INST[i_tm, i_var_num; int_tm, int_var] add_lemma0 in
78 let df_th = eval_all_n2 df1_th df2_th true add;;
79 let d_bounds_list = (rand o rator o concl) df_th;;
82 let dd1 = second_bounded_components n second1_th;;
83 let dd2 = second_bounded_components n second2_th;;
85 let add_second_lemma0 = (INST[f1_tm, f_var; f2_tm, g_var] o
86 INST_TYPE[n_type_array.(n), nty]) add_second_lemma';;
88 let add_second_lemma1 = (INST[f1_tm, f_var; f2_tm, g_var] o
89 INST_TYPE[n_type_array.(n), nty]) add_second_lemma'';;
92 let add_second2 th1 th2 =
93 let i_tm = (rand o rator o concl) th1 in
94 let th1, th2 = BETA_RULE th1, BETA_RULE th2 in
95 let lemma = INST[i_tm, i_var_num] add_second_lemma0 in
96 let add_second th1 th2 =
97 let add_th = float_interval_add p_second th1 th2 in
98 let int_tm = rand (concl add_th) and
99 j_tm = (rand o rator o rator o rator o lhand) (concl th1) in
100 let th0 = INST[j_tm, j_var_num; int_tm, int_var] lemma in
102 let add_th = eval_all_n2 th1 th2 true add_second in
103 let list_tm = (rand o rator o concl) add_th in
104 let lemma1 = INST[i_tm, i_var_num; list_tm, list_var_real_pair] add_second_lemma1 in
105 EQ_MP lemma1 add_th;;
108 let dd_th0 = eval_all_n2 dd1 dd2 false add_second2;;
109 let dd_list = (rand o rator o concl) dd_th0;;
110 let dd_th = GEN x_var (DISCH_ALL dd_th0);;
112 let th = (MY_PROVE_HYP dd_th o MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
113 MY_PROVE_HYP bounds_th o MY_PROVE_HYP df_th o MY_PROVE_HYP domain_th o
114 INST[f1_tm, f_var; f2_tm, g_var;
115 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
116 bounds_tm, bounds_var; d_bounds_list, d_bounds_list_var;
117 dd_list, dd_bounds_list_var] o
118 INST_TYPE[n_type_array.(n), nty]) MK_M_TAYLOR_ADD';;
119 let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var add_op_real;;
120 m_taylor_interval_norm th eq_th;;
123 (********************)
127 test 100 (dest_m_taylor_thms n) taylor1_th;;
129 test 100 (dest_m_taylor_thms n) taylor2_th;;
133 let a =(rand o concl) diff2_f1_th and
134 b = (rand o concl) diff2_f2_th in
140 test 100 dest_m_cell_domain (concl domain_th);;
142 test 100 type_of y_tm;;
146 let x_var = mk_var ("x", ty) and
147 y_var = mk_var ("y", ty) and
148 w_var = mk_var ("w", ty) and
149 f_var = mk_var ("f", type_of f1_tm) and
150 g_var = mk_var ("g", type_of f2_tm) and
151 domain_var = mk_var ("domain", type_of domain_tm) in
152 x_var, y_var, w_var, f_var, g_var, domain_var;;
157 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
158 _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
159 bounds1_th, df1_th, bounds2_th, df2_th;;
163 test 100 (float_interval_add p_lin bounds1_th) bounds2_th;;
165 test 100 (rand o concl) bounds_th;;
168 test 100 (INST[f1_tm, f_var; f2_tm, g_var; y_tm, x_var] o
169 INST_TYPE[n_type_array.(n), nty]) add_partial_lemma';;
172 let add_th = float_interval_add p_lin th1 th2 in
173 let int_tm = rand (concl add_th) and
174 i_tm = (rand o rator o rator o lhand) (concl th1) in
175 let th0 = INST[i_tm, i_var_num; int_tm, int_var] add_lemma0 in
179 test 100 (eval_all_n2 df1_th df2_th true) add;;
181 test 100 (rand o rator o concl) df_th;;
184 test 100 (second_bounded_components n) second1_th;;
186 test 100 (second_bounded_components n) second2_th;;
189 test 100 (INST[f1_tm, f_var; f2_tm, g_var] o
190 INST_TYPE[n_type_array.(n), nty]) add_second_lemma';;
193 test 100 (INST[f1_tm, f_var; f2_tm, g_var] o
194 INST_TYPE[n_type_array.(n), nty]) add_second_lemma'';;
197 let add_second2 th1 th2 =
198 let i_tm = (rand o rator o concl) th1 in
199 let th1, th2 = BETA_RULE th1, BETA_RULE th2 in
200 let lemma = INST[i_tm, i_var_num] add_second_lemma0 in
201 let add_second th1 th2 =
202 let add_th = float_interval_add p_second th1 th2 in
203 let int_tm = rand (concl add_th) and
204 j_tm = (rand o rator o rator o rator o lhand) (concl th1) in
205 let th0 = INST[j_tm, j_var_num; int_tm, int_var] lemma in
207 let add_th = eval_all_n2 th1 th2 true add_second in
208 let list_tm = (rand o rator o concl) add_th in
209 let lemma1 = INST[i_tm, i_var_num; list_tm, list_var_real_pair] add_second_lemma1 in
210 EQ_MP lemma1 add_th;;
214 test 100 (eval_all_n2 dd1 dd2 false) add_second2;;
216 test 100 (rand o rator o concl) dd_th0;;
218 test 100 (GEN x_var o DISCH_ALL) dd_th0;;
221 test 100 (MY_PROVE_HYP dd_th o MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
222 MY_PROVE_HYP bounds_th o MY_PROVE_HYP df_th o MY_PROVE_HYP domain_th o
223 INST[f1_tm, f_var; f2_tm, g_var;
224 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
225 bounds_tm, bounds_var; d_bounds_list, d_bounds_list_var;
226 dd_list, dd_bounds_list_var] o
227 INST_TYPE[n_type_array.(n), nty]) MK_M_TAYLOR_ADD';;
229 test 100 (binary_beta_gen_eq f1_tm f2_tm x_var) add_op_real;;
231 test 100 (m_taylor_interval_norm th) eq_th;;
234 (***********************)
236 test 100 (eval_all_n2 df1_th df2_th true) add;;
238 (* Constructs all_n n (map2 s list1 list2) *)
239 let all_n1_th = df1_th and all_n2_th = df2_th and beta_flag = true and s = add;;
243 let ths1', suc_ths = all_n_components all_n1_th;;
244 let ths2', _ = all_n_components all_n2_th;;
246 if beta_flag then map BETA_RULE ths1', map BETA_RULE ths2' else ths1', ths2';;
248 let ths1, ths2, suc_ths = List.rev ths1, List.rev ths2, List.rev suc_ths;;
249 let ths = map2 s ths1 ths2;;
250 build_all_n ths suc_ths;;
256 test 100 all_n_components all_n1_th;;
258 test 100 all_n_components all_n2_th;;
260 test 100 (map BETA_RULE) ths1';;
262 test 100 (map BETA_RULE) ths2';;
265 BETA_RULE (hd ths1');;
269 let ths1, ths2, suc_ths = List.rev ths1, List.rev ths2, List.rev suc_ths in
270 ths1, ths2, suc_ths;;
274 test 100 (map2 s ths1) ths2;;
276 test 100 (build_all_n ths) suc_ths;;
285 test 1000 BETA_RULE th0;;
288 let MY_BETA_RULE th =
290 let op, arg = dest_comb tm in
292 let op_th = AP_THM (beta op) arg in
293 let beta_th = BETA_CONV (rand (concl op_th)) in
297 EQ_MP (beta (concl th)) th;;
300 let MY_BETA_RULE2 th0 =
302 let lhs, rhs = dest_comb c in
304 let th1 = BETA_CONV lhs in
305 let th2 = AP_THM th1 rhs in
306 let th3 = BETA_CONV (rand (concl th2)) in
307 EQ_MP (TRANS th2 th3) th0;;
311 test 1000 MY_BETA_RULE2 th0;;