formal_ineqs/taylor/m_taylor_arith2.hl

   1 (* =========================================================== *)
   2 (* Formal arithmetic of taylor intervals 2                     *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 needs "taylor/m_taylor_arith.hl";;
   8
   9
  10 module M_taylor_arith2 = struct
  11
  12 open Arith_misc;;
  13 open Arith_nat;;
  14 open Arith_float;;
  15 open More_float;;
  16 open Float_atn;;
  17 open Float_theory;;
  18 open M_taylor;;
  19 open M_taylor_arith;;
  20 open Misc_vars;;
  21
  22
  23
  24 (**************************************)
  25 let mk_vars n name ty = map (fun i -> mk_var (name^string_of_int i, ty)) (1--n);;
  26
  27
  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
  35
  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);;
  39
  40
  41
  42 (***************************************)
  43
  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;;
  57
  58
  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]);;
  65
  66 let gen_atn_thm =
  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]);;
  69
  70 let gen_acs_thm =
  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]);;
  74
  75
  76 let add_ths_array,
  77   sub_ths_array,
  78   mul_ths_array,
  79   neg_ths_array,
  80   inv_ths_array,
  81   sqrt_ths_array,
  82   atn_ths_array,
  83   acs_ths_array =
  84   let gen = fun f -> Array.init (max_dim + 1) (fun i -> if i = 0 then TRUTH else f i) in
  85     gen gen_add_thm,
  86   gen gen_sub_thm,
  87   gen gen_mul_thm,
  88   gen gen_neg_thm,
  89   gen gen_inv_thm,
  90   gen gen_sqrt_thm,
  91   gen gen_atn_thm,
  92   gen gen_acs_thm;;
  93
  94
  95 (*********************)
  96 (* add *)
  97
  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
 105
 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
 112
 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
 115
 116   let bounds_th = float_interval_add p_lin bounds1_th bounds2_th in
 117   let bounds_tm = (rand o concl) bounds_th in
 118
 119   let df_ths =
 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
 123
 124   let df_th = end_itlist CONJ df_ths in
 125
 126   let dd_ths =
 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
 132
 133   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 134
 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
 137
 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
 141
 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;;
 150
 151
 152 (*********************)
 153 (* sub *)
 154
 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
 162
 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
 169
 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
 172
 173   let bounds_th = float_interval_sub p_lin bounds1_th bounds2_th in
 174   let bounds_tm = (rand o concl) bounds_th in
 175
 176   let df_ths =
 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
 180
 181   let df_th = end_itlist CONJ df_ths in
 182
 183   let dd_ths =
 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
 189
 190   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 191
 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
 194
 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
 198
 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;;
 207
 208
 209 (*********************)
 210 (* mul *)
 211
 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
 219
 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
 226
 227   let undisch = UNDISCH o SPEC x_var in
 228
 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
 231
 232   let bounds_th = float_interval_mul p_lin bounds1_th bounds2_th in
 233   let bounds_tm = (rand o concl) bounds_th in
 234
 235   (* first partials *)
 236   let df_ths =
 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
 241
 242   let df_th = end_itlist CONJ df_ths in
 243
 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
 251
 252   let dd_ths =
 253     let ns = 1--n 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
 267
 268   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 269
 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
 272
 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
 276
 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;;
 285
 286
 287 (*********************)
 288 (* neg *)
 289
 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
 295
 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
 301
 302   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 303
 304   let bounds_th = float_interval_neg bounds1_th in
 305   let bounds_tm = (rand o concl) bounds_th in
 306
 307   let df_ths =
 308     let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
 309       map (float_interval_neg) df1_ths in
 310
 311   let df_th = end_itlist CONJ df_ths in
 312
 313   let dd_ths =
 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
 317
 318   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 319
 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
 322
 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
 326
 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
 329               INST([f1_tm, f_var;
 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;;
 334
 335
 336 (******************************)
 337 (* inv *)
 338
 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
 343
 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
 350
 351   let undisch = UNDISCH o SPEC x_var in
 352
 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
 356
 357   (* cond *)
 358   let cond_th = check_interval_not_zero f_bounds_tm in
 359
 360   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 361
 362   let bounds_th = float_interval_inv p_lin bounds1_th in
 363   let bounds_tm = (rand o concl) bounds_th in
 364
 365   (* first partials *)
 366   let u_bounds =
 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
 369
 370   let df1_ths' = all_n_components2 n df1_th in
 371   let df1_ths = map MY_BETA_RULE df1_ths' in
 372
 373   let df_ths =
 374     let ( * ) = float_interval_mul p_lin in
 375       map (fun th1 -> u_bounds * th1) df1_ths in
 376
 377   let df_th = end_itlist CONJ df_ths in
 378
 379   (* second partials *)
 380   let dd_ths =
 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
 383
 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
 387
 388   (* u'(f x), u''(f x) *)
 389   let d1_th0, d2_th0 =
 390     let inv, ( * ) = float_interval_inv p_second, float_interval_mul p_second in
 391     let ff = f1_bound * f1_bound in
 392       inv ff,
 393     two_interval * inv (f1_bound * ff) in
 394
 395   let dd_ths =
 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
 400
 401   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 402
 403   (***)
 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
 406
 407   let dfs = map (rand o concl) df_ths in
 408   let dds = map (map (rand o concl)) dd_ths in
 409
 410   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 411
 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;;
 420
 421
 422
 423 (******************************)
 424 (* sqrt *)
 425
 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
 430
 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
 437
 438   let undisch = UNDISCH o SPEC x_var in
 439
 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
 443
 444   (* cond *)
 445   let cond_th = check_interval_pos f_bounds_tm in
 446
 447   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 448
 449   let bounds_th = float_interval_sqrt p_lin bounds1_th in
 450   let bounds_tm = (rand o concl) bounds_th in
 451
 452   (* first partials *)
 453   let u_bounds =
 454     let inv, ( * ) = float_interval_inv p_lin, float_interval_mul p_lin in
 455       inv (two_interval * bounds_th) in
 456
 457   let df1_ths' = all_n_components2 n df1_th in
 458   let df1_ths = map MY_BETA_RULE df1_ths' in
 459
 460   let df_ths =
 461     let ( * ) = float_interval_mul p_lin in
 462       map (fun th1 -> u_bounds * th1) df1_ths in
 463
 464   let df_th = end_itlist CONJ df_ths in
 465
 466   (* second partials *)
 467   let dd_ths =
 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
 470
 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
 474
 475   (* u'(f x), u''(f x) *)
 476   let d1_th0, d2_th0 =
 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
 481
 482   let dd_ths =
 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
 487
 488   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 489
 490   (***)
 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
 493
 494   let dfs = map (rand o concl) df_ths in
 495   let dds = map (map (rand o concl)) dd_ths in
 496
 497   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 498
 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;;
 507
 508
 509
 510 (******************************)
 511 (* atn *)
 512
 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
 517
 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
 524
 525   let undisch = UNDISCH o SPEC x_var in
 526
 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
 530
 531   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 532
 533   let bounds_th = float_interval_atn p_lin bounds1_th in
 534   let bounds_tm = (rand o concl) bounds_th in
 535
 536   (* first partials *)
 537   let u_bounds =
 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
 541
 542   let df1_ths' = all_n_components2 n df1_th in
 543   let df1_ths = map MY_BETA_RULE df1_ths' in
 544
 545   let df_ths =
 546     let ( * ) = float_interval_mul p_lin in
 547       map (fun th1 -> u_bounds * th1) df1_ths in
 548
 549   let df_th = end_itlist CONJ df_ths in
 550
 551   (* second partials *)
 552   let dd_ths =
 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
 555
 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
 559
 560   (* u'(f x), u''(f x) *)
 561   let d1_th0, d2_th0 =
 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
 566
 567   let dd_ths =
 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
 572
 573   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 574
 575   (***)
 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
 578
 579   let dfs = map (rand o concl) df_ths in
 580   let dds = map (map (rand o concl)) dd_ths in
 581
 582   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 583
 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;;
 592
 593
 594 (******************************)
 595 (* acs *)
 596
 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
 601
 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
 608
 609   let undisch = UNDISCH o SPEC x_var in
 610
 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
 614
 615   (* cond *)
 616   let cond_th = EQT_ELIM (check_interval_iabs f_bounds_tm one_float) in
 617
 618   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 619
 620   let bounds_th = float_interval_acs p_lin bounds1_th in
 621   let bounds_tm = (rand o concl) bounds_th in
 622
 623   (* first partials *)
 624   let u_bounds =
 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
 628
 629   let df1_ths' = all_n_components2 n df1_th in
 630   let df1_ths = map MY_BETA_RULE df1_ths' in
 631
 632   let df_ths =
 633     let ( * ) = float_interval_mul p_lin in
 634       map (fun th1 -> u_bounds * th1) df1_ths in
 635
 636   let df_th = end_itlist CONJ df_ths in
 637
 638   (* second partials *)
 639   let dd_ths =
 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
 642
 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
 646
 647   (* u'(f x), u''(f x) *)
 648   let d1_th0, d2_th0 =
 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
 654
 655   let dd_ths =
 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
 660
 661   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 662
 663   (***)
 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
 666
 667   let dfs = map (rand o concl) df_ths in
 668   let dds = map (map (rand o concl)) dd_ths in
 669
 670   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 671
 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;;
 680
 681
 682 end;;