1 (* =========================================================== *)
2 (* Formal arithmetic of taylor intervals 2 *)
3 (* Author: Alexey Solovyev *)
5 (* =========================================================== *)
7 needs "taylor/m_taylor_arith.hl";;
10 module M_taylor_arith2 = struct
24 (**************************************)
25 let mk_vars n name ty = map (fun i -> mk_var (name^string_of_int i, ty)) (1--n);;
28 let all_n_components2 n all_n_th =
29 let th0 = SYM (all_n_array.(n)) in
30 let _, list_tm, s_tm = dest_all_n (concl all_n_th) in
31 let list_ty = type_of list_tm in
32 let ty = (hd o snd o dest_type) list_ty in
33 let s_var = mk_var ("s", type_of s_tm) and
34 a_vars = mk_vars n "a" ty in
36 let list_tms = dest_list list_tm in
37 let th1 = (INST ([s_tm, s_var] @ zip list_tms a_vars) o INST_TYPE[ty, aty]) th0 in
38 CONJUNCTS (EQ_MP th1 all_n_th);;
42 (***************************************)
44 let gen_taylor_arith_thm arith_th final_rule n =
45 let num1_th = (SYM o REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `1` in
46 let th0 = (REWRITE_RULE[num1_th] o DISCH_ALL o INST_TYPE[n_type_array.(n), nty]) arith_th in
47 let pty = `:real#real` in
48 let dfs = mk_vars n "df" pty in
49 let ddfs' = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
50 let ddfs = map (fun list -> mk_list (list, pty)) ddfs' in
51 let d_bounds_list = mk_list (dfs, pty) in
52 let dd_bounds_list = mk_list (ddfs, type_of (hd ddfs)) in
53 let th1 = INST[d_bounds_list, d_bounds_list_var; dd_bounds_list, dd_bounds_list_var] th0 in
54 let th2 = (CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[all_n]) th1 in
55 (UNDISCH_ALL o final_rule o REWRITE_RULE[GSYM CONJ_ASSOC] o
56 NUMERALS_TO_NUM o PURE_REWRITE_RULE[FLOAT_OF_NUM; min_exp_def]) th2;;
59 let gen_add_thm = gen_taylor_arith_thm MK_M_TAYLOR_ADD' (CONV_RULE ALL_CONV);;
60 let gen_sub_thm = gen_taylor_arith_thm MK_M_TAYLOR_SUB' (CONV_RULE ALL_CONV);;
61 let gen_mul_thm = gen_taylor_arith_thm MK_M_TAYLOR_MUL' (CONV_RULE ALL_CONV);;
62 let gen_neg_thm = gen_taylor_arith_thm MK_M_TAYLOR_NEG' (CONV_RULE ALL_CONV);;
63 let gen_inv_thm = gen_taylor_arith_thm MK_M_TAYLOR_INV' (REWRITE_RULE[float2_eq]);;
64 let gen_sqrt_thm = gen_taylor_arith_thm MK_M_TAYLOR_SQRT' (REWRITE_RULE[float2_eq]);;
67 let pow2_th = (SYM o REWRITE_CONV[SYM num2_eq]) `x pow 2` in
68 gen_taylor_arith_thm MK_M_TAYLOR_ATN' (REWRITE_RULE[float2_eq; float1_eq; pow2_th]);;
71 let iabs_lemma = REWRITE_CONV[SYM float1_eq] `iabs f_bounds < &1` in
72 let pow3_lemma = (SYM o REWRITE_CONV[SYM num3_eq]) `x pow 3` in
73 gen_taylor_arith_thm MK_M_TAYLOR_ACS' (REWRITE_RULE[iabs_lemma] o REWRITE_RULE[float1_eq; pow3_lemma]);;
84 let gen = fun f -> Array.init (max_dim + 1) (fun i -> if i = 0 then TRUTH else f i) in
95 (*********************)
98 let eval_m_taylor_add2 n p_lin p_second taylor1_th taylor2_th =
99 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
100 let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
101 let f1_tm = (rand o concl) diff2_f1_th and
102 f2_tm = (rand o concl) diff2_f2_th in
103 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
104 let ty = type_of y_tm in
106 let x_var = mk_var ("x", ty) and
107 y_var = mk_var ("y", ty) and
108 w_var = mk_var ("w", ty) and
109 f_var = mk_var ("f", type_of f1_tm) and
110 g_var = mk_var ("g", type_of f2_tm) and
111 domain_var = mk_var ("domain", type_of domain_tm) in
113 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
114 _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
116 let bounds_th = float_interval_add p_lin bounds1_th bounds2_th in
117 let bounds_tm = (rand o concl) bounds_th in
120 let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
121 let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
122 map2 (float_interval_add p_lin) df1_ths df2_ths in
124 let df_th = end_itlist CONJ df_ths in
127 let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
128 let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
129 let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1' in
130 let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd2' in
131 map2 (map2 (float_interval_add p_second)) dd1 dd2 in
133 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
135 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
136 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
138 let dfs = map (rand o concl) df_ths in
139 let dds = map (map (rand o concl)) dd_ths in
140 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
142 let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
143 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
144 MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
145 INST([f1_tm, f_var; f2_tm, g_var;
146 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
147 bounds_tm, bounds_var] @ inst_list)) add_ths_array.(n) in
148 let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var add_op_real in
149 m_taylor_interval_norm th eq_th;;
152 (*********************)
155 let eval_m_taylor_sub2 n p_lin p_second taylor1_th taylor2_th =
156 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
157 let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
158 let f1_tm = (rand o concl) diff2_f1_th and
159 f2_tm = (rand o concl) diff2_f2_th in
160 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
161 let ty = type_of y_tm in
163 let x_var = mk_var ("x", ty) and
164 y_var = mk_var ("y", ty) and
165 w_var = mk_var ("w", ty) and
166 f_var = mk_var ("f", type_of f1_tm) and
167 g_var = mk_var ("g", type_of f2_tm) and
168 domain_var = mk_var ("domain", type_of domain_tm) in
170 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
171 _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
173 let bounds_th = float_interval_sub p_lin bounds1_th bounds2_th in
174 let bounds_tm = (rand o concl) bounds_th in
177 let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
178 let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
179 map2 (float_interval_sub p_lin) df1_ths df2_ths in
181 let df_th = end_itlist CONJ df_ths in
184 let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
185 let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
186 let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1' in
187 let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd2' in
188 map2 (map2 (float_interval_sub p_second)) dd1 dd2 in
190 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
192 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
193 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
195 let dfs = map (rand o concl) df_ths in
196 let dds = map (map (rand o concl)) dd_ths in
197 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
199 let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
200 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
201 MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
202 INST([f1_tm, f_var; f2_tm, g_var;
203 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
204 bounds_tm, bounds_var] @ inst_list)) sub_ths_array.(n) in
205 let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var sub_op_real in
206 m_taylor_interval_norm th eq_th;;
209 (*********************)
212 let eval_m_taylor_mul2 n p_lin p_second taylor1_th taylor2_th =
213 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
214 let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
215 let f1_tm = (rand o concl) diff2_f1_th and
216 f2_tm = (rand o concl) diff2_f2_th in
217 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
218 let ty = type_of y_tm in
220 let x_var = mk_var ("x", ty) and
221 y_var = mk_var ("y", ty) and
222 w_var = mk_var ("w", ty) and
223 f_var = mk_var ("f", type_of f1_tm) and
224 g_var = mk_var ("g", type_of f2_tm) and
225 domain_var = mk_var ("domain", type_of domain_tm) in
227 let undisch = UNDISCH o SPEC x_var in
229 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
230 _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
232 let bounds_th = float_interval_mul p_lin bounds1_th bounds2_th in
233 let bounds_tm = (rand o concl) bounds_th in
237 let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
238 let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
239 let ( * ), ( + ) = float_interval_mul p_lin, float_interval_add p_lin in
240 map2 (fun d1 d2 -> d1 * bounds2_th + bounds1_th * d2) df1_ths df2_ths in
242 let df_th = end_itlist CONJ df_ths in
244 (* second partials *)
245 let d1_bounds = map (fun i ->
246 undisch (eval_m_taylor_partial_bound n p_second i taylor1_th)) (1--n) in
247 let d2_bounds = map (fun i ->
248 undisch (eval_m_taylor_partial_bound n p_second i taylor2_th)) (1--n) in
249 let f1_bound = undisch (eval_m_taylor_bound n p_second taylor1_th) in
250 let f2_bound = undisch (eval_m_taylor_bound n p_second taylor2_th) in
254 let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
255 let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
256 let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) ns dd1' in
257 let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) ns dd2' in
258 let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
259 map2 (fun (dd1_list, dd2_list) i ->
260 let di1 = List.nth d1_bounds (i - 1) in
261 let di2 = List.nth d2_bounds (i - 1) in
262 map2 (fun (dd1, dd2) j ->
263 let dj1 = List.nth d1_bounds (j - 1) in
264 let dj2 = List.nth d2_bounds (j - 1) in
265 (dd1 * f2_bound + di1 * dj2) + (dj1 * di2 + f1_bound * dd2))
266 (zip dd1_list dd2_list) (1--i)) (zip dd1 dd2) ns in
268 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
270 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
271 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
273 let dfs = map (rand o concl) df_ths in
274 let dds = map (map (rand o concl)) dd_ths in
275 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
277 let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
278 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
279 MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
280 INST([f1_tm, f_var; f2_tm, g_var;
281 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
282 bounds_tm, bounds_var] @ inst_list)) mul_ths_array.(n) in
283 let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var mul_op_real in
284 m_taylor_interval_norm th eq_th;;
287 (*********************)
290 let eval_m_taylor_neg2 n taylor1_th =
291 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
292 let f1_tm = (rand o concl) diff2_f1_th in
293 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
294 let ty = type_of y_tm in
296 let x_var = mk_var ("x", ty) and
297 y_var = mk_var ("y", ty) and
298 w_var = mk_var ("w", ty) and
299 f_var = mk_var ("f", type_of f1_tm) and
300 domain_var = mk_var ("domain", type_of domain_tm) in
302 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
304 let bounds_th = float_interval_neg bounds1_th in
305 let bounds_tm = (rand o concl) bounds_th in
308 let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
309 map (float_interval_neg) df1_ths in
311 let df_th = end_itlist CONJ df_ths in
314 let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
315 let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1' in
316 map (map float_interval_neg) dd1 in
318 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
320 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
321 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
323 let dfs = map (rand o concl) df_ths in
324 let dds = map (map (rand o concl)) dd_ths in
325 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
327 let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP bounds_th o
328 MY_PROVE_HYP domain_th o MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
330 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
331 bounds_tm, bounds_var] @ inst_list)) neg_ths_array.(n) in
332 let eq_th = unary_beta_gen_eq f1_tm x_var neg_op_real in
333 m_taylor_interval_norm th eq_th;;
336 (******************************)
339 let eval_m_taylor_inv2 n p_lin p_second taylor1_th =
340 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
341 let f1_tm = (rand o concl) diff2_f1_th in
342 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
344 let ty = type_of y_tm in
345 let x_var = mk_var ("x", ty) and
346 y_var = mk_var ("y", ty) and
347 w_var = mk_var ("w", ty) and
348 f_var = mk_var ("f", type_of f1_tm) and
349 domain_var = mk_var ("domain", type_of domain_tm) in
351 let undisch = UNDISCH o SPEC x_var in
353 let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
354 let f1_bound = undisch f1_bound0 in
355 let f_bounds_tm = (rand o concl) f1_bound in
358 let cond_th = check_interval_not_zero f_bounds_tm in
360 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
362 let bounds_th = float_interval_inv p_lin bounds1_th in
363 let bounds_tm = (rand o concl) bounds_th in
367 let neg, inv, ( * ) = float_interval_neg, float_interval_inv p_lin, float_interval_mul p_lin in
368 neg (inv (bounds1_th * bounds1_th)) in
370 let df1_ths' = all_n_components2 n df1_th in
371 let df1_ths = map MY_BETA_RULE df1_ths' in
374 let ( * ) = float_interval_mul p_lin in
375 map (fun th1 -> u_bounds * th1) df1_ths in
377 let df_th = end_itlist CONJ df_ths in
379 (* second partials *)
381 let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
382 map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
384 let d1_bounds = map (fun i ->
385 let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
386 undisch th0) (1--n) in
388 (* u'(f x), u''(f x) *)
390 let inv, ( * ) = float_interval_inv p_second, float_interval_mul p_second in
391 let ff = f1_bound * f1_bound in
393 two_interval * inv (f1_bound * ff) in
396 let ( * ), ( - ) = float_interval_mul p_second, float_interval_sub p_second in
397 map2 (fun dd_list di1 ->
398 my_map2 (fun dd dj1 ->
399 (d2_th0 * dj1) * di1 - d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
401 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
404 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
405 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
407 let dfs = map (rand o concl) df_ths in
408 let dds = map (map (rand o concl)) dd_ths in
410 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
412 let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
413 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
414 MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
415 INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
416 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
417 bounds_tm, bounds_var] @ inst_list)) inv_ths_array.(n) in
418 let eq_th = unary_beta_gen_eq f1_tm x_var inv_op_real in
419 m_taylor_interval_norm th1 eq_th;;
423 (******************************)
426 let eval_m_taylor_sqrt2 n p_lin p_second taylor1_th =
427 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
428 let f1_tm = (rand o concl) diff2_f1_th in
429 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
431 let ty = type_of y_tm in
432 let x_var = mk_var ("x", ty) and
433 y_var = mk_var ("y", ty) and
434 w_var = mk_var ("w", ty) and
435 f_var = mk_var ("f", type_of f1_tm) and
436 domain_var = mk_var ("domain", type_of domain_tm) in
438 let undisch = UNDISCH o SPEC x_var in
440 let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
441 let f1_bound = undisch f1_bound0 in
442 let f_bounds_tm = (rand o concl) f1_bound in
445 let cond_th = check_interval_pos f_bounds_tm in
447 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
449 let bounds_th = float_interval_sqrt p_lin bounds1_th in
450 let bounds_tm = (rand o concl) bounds_th in
454 let inv, ( * ) = float_interval_inv p_lin, float_interval_mul p_lin in
455 inv (two_interval * bounds_th) in
457 let df1_ths' = all_n_components2 n df1_th in
458 let df1_ths = map MY_BETA_RULE df1_ths' in
461 let ( * ) = float_interval_mul p_lin in
462 map (fun th1 -> u_bounds * th1) df1_ths in
464 let df_th = end_itlist CONJ df_ths in
466 (* second partials *)
468 let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
469 map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
471 let d1_bounds = map (fun i ->
472 let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
473 undisch th0) (1--n) in
475 (* u'(f x), u''(f x) *)
477 let neg, sqrt, inv, ( * ) = float_interval_neg, float_interval_sqrt p_second,
478 float_interval_inv p_second, float_interval_mul p_second in
479 let two_sqrt_f = two_interval * sqrt f1_bound in
480 inv two_sqrt_f, neg (inv (two_sqrt_f * (two_interval * f1_bound))) in
483 let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
484 map2 (fun dd_list di1 ->
485 my_map2 (fun dd dj1 ->
486 (d2_th0 * dj1) * di1 + d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
488 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
491 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
492 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
494 let dfs = map (rand o concl) df_ths in
495 let dds = map (map (rand o concl)) dd_ths in
497 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
499 let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
500 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
501 MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
502 INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
503 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
504 bounds_tm, bounds_var] @ inst_list)) sqrt_ths_array.(n) in
505 let eq_th = unary_beta_gen_eq f1_tm x_var sqrt_tm in
506 m_taylor_interval_norm th1 eq_th;;
510 (******************************)
513 let eval_m_taylor_atn2 n p_lin p_second taylor1_th =
514 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
515 let f1_tm = (rand o concl) diff2_f1_th in
516 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
518 let ty = type_of y_tm in
519 let x_var = mk_var ("x", ty) and
520 y_var = mk_var ("y", ty) and
521 w_var = mk_var ("w", ty) and
522 f_var = mk_var ("f", type_of f1_tm) and
523 domain_var = mk_var ("domain", type_of domain_tm) in
525 let undisch = UNDISCH o SPEC x_var in
527 let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
528 let f1_bound = undisch f1_bound0 in
529 let f_bounds_tm = (rand o concl) f1_bound in
531 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
533 let bounds_th = float_interval_atn p_lin bounds1_th in
534 let bounds_tm = (rand o concl) bounds_th in
538 let inv, ( + ), ( * ) = float_interval_inv p_lin,
539 float_interval_add p_lin, float_interval_mul p_lin in
540 inv (one_interval + bounds1_th * bounds1_th) in
542 let df1_ths' = all_n_components2 n df1_th in
543 let df1_ths = map MY_BETA_RULE df1_ths' in
546 let ( * ) = float_interval_mul p_lin in
547 map (fun th1 -> u_bounds * th1) df1_ths in
549 let df_th = end_itlist CONJ df_ths in
551 (* second partials *)
553 let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
554 map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
556 let d1_bounds = map (fun i ->
557 let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
558 undisch th0) (1--n) in
560 (* u'(f x), u''(f x) *)
562 let neg, inv, ( + ), ( * ), pow2 = float_interval_neg, float_interval_inv p_second,
563 float_interval_add p_second, float_interval_mul p_second, float_interval_pow_simple p_second 2 in
564 let inv_one_ff = inv (one_interval + f1_bound * f1_bound) in
565 inv_one_ff, (neg_two_interval * f1_bound) * pow2 inv_one_ff in
568 let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
569 map2 (fun dd_list di1 ->
570 my_map2 (fun dd dj1 ->
571 (d2_th0 * dj1) * di1 + d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
573 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
576 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
577 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
579 let dfs = map (rand o concl) df_ths in
580 let dds = map (map (rand o concl)) dd_ths in
582 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
584 let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP f1_bound0 o
585 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
586 MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
587 INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
588 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
589 bounds_tm, bounds_var] @ inst_list)) atn_ths_array.(n) in
590 let eq_th = unary_beta_gen_eq f1_tm x_var atn_tm in
591 m_taylor_interval_norm th1 eq_th;;
594 (******************************)
597 let eval_m_taylor_acs2 n p_lin p_second taylor1_th =
598 let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
599 let f1_tm = (rand o concl) diff2_f1_th in
600 let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
602 let ty = type_of y_tm in
603 let x_var = mk_var ("x", ty) and
604 y_var = mk_var ("y", ty) and
605 w_var = mk_var ("w", ty) and
606 f_var = mk_var ("f", type_of f1_tm) and
607 domain_var = mk_var ("domain", type_of domain_tm) in
609 let undisch = UNDISCH o SPEC x_var in
611 let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
612 let f1_bound = undisch f1_bound0 in
613 let f_bounds_tm = (rand o concl) f1_bound in
616 let cond_th = EQT_ELIM (check_interval_iabs f_bounds_tm one_float) in
618 let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
620 let bounds_th = float_interval_acs p_lin bounds1_th in
621 let bounds_tm = (rand o concl) bounds_th in
625 let inv, sqrt, neg = float_interval_inv p_lin, float_interval_sqrt p_lin, float_interval_neg in
626 let ( * ), ( - ) = float_interval_mul p_lin, float_interval_sub p_lin in
627 neg (inv (sqrt (one_interval - bounds1_th * bounds1_th))) in
629 let df1_ths' = all_n_components2 n df1_th in
630 let df1_ths = map MY_BETA_RULE df1_ths' in
633 let ( * ) = float_interval_mul p_lin in
634 map (fun th1 -> u_bounds * th1) df1_ths in
636 let df_th = end_itlist CONJ df_ths in
638 (* second partials *)
640 let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
641 map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
643 let d1_bounds = map (fun i ->
644 let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
645 undisch th0) (1--n) in
647 (* u'(f x), u''(f x) *)
649 let neg, sqrt, inv = float_interval_neg, float_interval_sqrt p_second, float_interval_inv p_second in
650 let ( - ), ( * ), ( / ), pow3 = float_interval_sub p_second, float_interval_mul p_second,
651 float_interval_div p_second, float_interval_pow_simple p_second 3 in
652 let ff_1 = one_interval - f1_bound * f1_bound in
653 inv (sqrt ff_1), neg (f1_bound / sqrt (pow3 ff_1)) in
656 let ( * ), ( - ) = float_interval_mul p_second, float_interval_sub p_second in
657 map2 (fun dd_list di1 ->
658 my_map2 (fun dd dj1 ->
659 (d2_th0 * dj1) * di1 - d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
661 let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
664 let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
665 let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
667 let dfs = map (rand o concl) df_ths in
668 let dds = map (map (rand o concl)) dd_ths in
670 let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
672 let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
673 MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
674 MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
675 INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
676 domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
677 bounds_tm, bounds_var] @ inst_list)) acs_ths_array.(n) in
678 let eq_th = unary_beta_gen_eq f1_tm x_var acs_tm in
679 m_taylor_interval_norm th1 eq_th;;