formal_lp/old/formal_interval/m_taylor_arith2.hl

   1 needs "../formal_lp/formal_interval/m_taylor_arith.hl";;
   2
   3
   4
   5
   6 (**************************************)
   7 let real_pair_ty = `:real#real`;;
   8 let mk_vars n name ty = map (fun i -> mk_var (name^string_of_int i, ty)) (1--n);;
   9
  10
  11 let all_n_components2 n all_n_th =
  12   let th0 = SYM (all_n_array.(n)) in
  13   let _, list_tm, s_tm = dest_all_n (concl all_n_th) in
  14   let list_ty = type_of list_tm in
  15   let ty = (hd o snd o dest_type) list_ty in
  16   let s_var = mk_var ("s", type_of s_tm) and
  17       a_vars = mk_vars n "a" ty in
  18
  19   let list_tms = dest_list list_tm in
  20   let th1 = (INST ([s_tm, s_var] @ zip list_tms a_vars) o INST_TYPE[ty, aty]) th0 in
  21     CONJUNCTS (EQ_MP th1 all_n_th);;
  22
  23
  24
  25 (***************************************)
  26
  27 let gen_taylor_arith_thm arith_th final_rule n =
  28   let num1_th = (SYM o REWRITE_RULE[Arith_hash.NUM_THM] o NUMERAL_TO_NUM_CONV) `1` in
  29   let th0 = (REWRITE_RULE[num1_th] o DISCH_ALL o INST_TYPE[n_type_array.(n), nty]) arith_th in
  30   let pty = `:real#real` in
  31   let dfs = mk_vars n "df" pty in
  32   let ddfs' = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
  33   let ddfs = map (fun list -> mk_list (list, pty)) ddfs' in
  34   let d_bounds_list = mk_list (dfs, pty) in
  35   let dd_bounds_list = mk_list (ddfs, type_of (hd ddfs)) in
  36   let th1 = INST[d_bounds_list, d_bounds_list_var; dd_bounds_list, dd_bounds_list_var] th0 in
  37   let th2 = (CONV_RULE NUM_REDUCE_CONV o REWRITE_RULE[all_n]) th1 in
  38     (UNDISCH_ALL o final_rule o REWRITE_RULE[GSYM CONJ_ASSOC] o
  39        NUMERALS_TO_NUM o PURE_REWRITE_RULE[FLOAT_OF_NUM; min_exp_def]) th2;;
  40
  41
  42 let gen_add_thm = gen_taylor_arith_thm MK_M_TAYLOR_ADD' (CONV_RULE ALL_CONV);;
  43 let gen_sub_thm = gen_taylor_arith_thm MK_M_TAYLOR_SUB' (CONV_RULE ALL_CONV);;
  44 let gen_mul_thm = gen_taylor_arith_thm MK_M_TAYLOR_MUL' (CONV_RULE ALL_CONV);;
  45 let gen_inv_thm = gen_taylor_arith_thm MK_M_TAYLOR_INV' (REWRITE_RULE[float2_eq]);;
  46 let gen_sqrt_thm = gen_taylor_arith_thm MK_M_TAYLOR_SQRT' (REWRITE_RULE[float2_eq]);;
  47
  48 let gen_atn_thm =
  49   let pow2_th = (SYM o REWRITE_CONV[SYM num2_eq]) `x pow 2` in
  50     gen_taylor_arith_thm MK_M_TAYLOR_ATN' (REWRITE_RULE[float2_eq; float1_eq; pow2_th]);;
  51
  52 let gen_acs_thm =
  53   let iabs_lemma = REWRITE_CONV[SYM float1_eq] `iabs f_bounds < &1` in
  54   let pow3_lemma = (SYM o REWRITE_CONV[SYM num3_eq]) `x pow 3` in
  55     gen_taylor_arith_thm MK_M_TAYLOR_ACS' (REWRITE_RULE[iabs_lemma] o REWRITE_RULE[float1_eq; pow3_lemma]);;
  56
  57
  58 let add_ths_array,
  59   sub_ths_array,
  60   mul_ths_array,
  61   inv_ths_array,
  62   sqrt_ths_array,
  63   atn_ths_array,
  64   acs_ths_array =
  65   let gen = fun f -> Array.init (max_dim + 1) (fun i -> if i = 0 then TRUTH else f i) in
  66     gen gen_add_thm,
  67   gen gen_sub_thm,
  68   gen gen_mul_thm,
  69   gen gen_inv_thm,
  70   gen gen_sqrt_thm,
  71   gen gen_atn_thm,
  72   gen gen_acs_thm;;
  73
  74
  75 (*********************)
  76 (* add *)
  77
  78 let eval_m_taylor_add2 n p_lin p_second taylor1_th taylor2_th =
  79   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
  80   let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
  81   let f1_tm = (rand o concl) diff2_f1_th and
  82       f2_tm = (rand o concl) diff2_f2_th in
  83   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
  84   let ty = type_of y_tm in
  85
  86   let x_var = mk_var ("x", ty) and
  87       y_var = mk_var ("y", ty) and
  88       w_var = mk_var ("w", ty) and
  89       f_var = mk_var ("f", type_of f1_tm) and
  90       g_var = mk_var ("g", type_of f2_tm) and
  91       domain_var = mk_var ("domain", type_of domain_tm) in
  92
  93   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
  94       _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
  95
  96   let bounds_th = float_interval_add p_lin bounds1_th bounds2_th in
  97   let bounds_tm = (rand o concl) bounds_th in
  98
  99   let df_ths =
 100     let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
 101     let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
 102       map2 (float_interval_add p_lin) df1_ths df2_ths in
 103
 104   let df_th = end_itlist CONJ df_ths in
 105
 106   let dd_ths =
 107     let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
 108     let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
 109     let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1' in
 110     let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd2' in
 111       map2 (map2 (float_interval_add p_second)) dd1 dd2 in
 112
 113   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 114
 115   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 116   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 117
 118   let dfs = map (rand o concl) df_ths in
 119   let dds = map (map (rand o concl)) dd_ths in
 120   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 121
 122   let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
 123               MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 124               MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
 125               INST([f1_tm, f_var; f2_tm, g_var;
 126                    domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 127                    bounds_tm, bounds_var] @ inst_list)) add_ths_array.(n) in
 128   let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var add_op_real in
 129     m_taylor_interval_norm th eq_th;;
 130
 131
 132 (*********************)
 133 (* sub *)
 134
 135 let eval_m_taylor_sub2 n p_lin p_second taylor1_th taylor2_th =
 136   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 137   let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
 138   let f1_tm = (rand o concl) diff2_f1_th and
 139       f2_tm = (rand o concl) diff2_f2_th in
 140   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 141   let ty = type_of y_tm in
 142
 143   let x_var = mk_var ("x", ty) and
 144       y_var = mk_var ("y", ty) and
 145       w_var = mk_var ("w", ty) and
 146       f_var = mk_var ("f", type_of f1_tm) and
 147       g_var = mk_var ("g", type_of f2_tm) and
 148       domain_var = mk_var ("domain", type_of domain_tm) in
 149
 150   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
 151       _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
 152
 153   let bounds_th = float_interval_sub p_lin bounds1_th bounds2_th in
 154   let bounds_tm = (rand o concl) bounds_th in
 155
 156   let df_ths =
 157     let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
 158     let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
 159       map2 (float_interval_sub p_lin) df1_ths df2_ths in
 160
 161   let df_th = end_itlist CONJ df_ths in
 162
 163   let dd_ths =
 164     let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
 165     let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
 166     let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1' in
 167     let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd2' in
 168       map2 (map2 (float_interval_sub p_second)) dd1 dd2 in
 169
 170   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 171
 172   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 173   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 174
 175   let dfs = map (rand o concl) df_ths in
 176   let dds = map (map (rand o concl)) dd_ths in
 177   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 178
 179   let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
 180               MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 181               MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
 182               INST([f1_tm, f_var; f2_tm, g_var;
 183                    domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 184                    bounds_tm, bounds_var] @ inst_list)) sub_ths_array.(n) in
 185   let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var sub_op_real in
 186     m_taylor_interval_norm th eq_th;;
 187
 188
 189 (*********************)
 190 (* mul *)
 191
 192 let eval_m_taylor_mul2 n p_lin p_second taylor1_th taylor2_th =
 193   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 194   let _, diff2_f2_th, lin2_th, second2_th = dest_m_taylor_thms n taylor2_th in
 195   let f1_tm = (rand o concl) diff2_f1_th and
 196       f2_tm = (rand o concl) diff2_f2_th in
 197   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 198   let ty = type_of y_tm in
 199
 200   let x_var = mk_var ("x", ty) and
 201       y_var = mk_var ("y", ty) and
 202       w_var = mk_var ("w", ty) and
 203       f_var = mk_var ("f", type_of f1_tm) and
 204       g_var = mk_var ("g", type_of f2_tm) and
 205       domain_var = mk_var ("domain", type_of domain_tm) in
 206
 207   let undisch = UNDISCH o SPEC x_var in
 208
 209   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th and
 210       _, bounds2_th, df2_th = m_lin_approx_components n lin2_th in
 211
 212   let bounds_th = float_interval_mul p_lin bounds1_th bounds2_th in
 213   let bounds_tm = (rand o concl) bounds_th in
 214
 215   (* first partials *)
 216   let df_ths =
 217     let df1_ths = map MY_BETA_RULE (all_n_components2 n df1_th) in
 218     let df2_ths = map MY_BETA_RULE (all_n_components2 n df2_th) in
 219     let ( * ), ( + ) = float_interval_mul p_lin, float_interval_add p_lin in
 220       map2 (fun d1 d2 -> d1 * bounds2_th + bounds1_th * d2) df1_ths df2_ths in
 221
 222   let df_th = end_itlist CONJ df_ths in
 223
 224   (* second partials *)
 225   let d1_bounds = map (fun i ->
 226                          undisch (eval_m_taylor_partial_bound n p_second i taylor1_th)) (1--n) in
 227   let d2_bounds = map (fun i ->
 228                          undisch (eval_m_taylor_partial_bound n p_second i taylor2_th)) (1--n) in
 229   let f1_bound = undisch (eval_m_taylor_bound n p_second taylor1_th) in
 230   let f2_bound = undisch (eval_m_taylor_bound n p_second taylor2_th) in
 231
 232   let dd_ths =
 233     let ns = 1--n in
 234     let dd1' = all_n_components2 n (second_bounded_components n second1_th) in
 235     let dd2' = all_n_components2 n (second_bounded_components n second2_th) in
 236     let dd1 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) ns dd1' in
 237     let dd2 = map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) ns dd2' in
 238     let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
 239       map2 (fun (dd1_list, dd2_list) i ->
 240               let di1 = List.nth d1_bounds (i - 1) in
 241               let di2 = List.nth d2_bounds (i - 1) in
 242                 map2 (fun (dd1, dd2) j ->
 243                         let dj1 = List.nth d1_bounds (j - 1) in
 244                         let dj2 = List.nth d2_bounds (j - 1) in
 245                           (dd1 * f2_bound + di1 * dj2) + (dj1 * di2 + f1_bound * dd2))
 246                   (zip dd1_list dd2_list) (1--i)) (zip dd1 dd2) ns in
 247
 248   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 249
 250   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 251   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 252
 253   let dfs = map (rand o concl) df_ths in
 254   let dds = map (map (rand o concl)) dd_ths in
 255   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 256
 257   let th = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP diff2_f2_th o
 258               MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 259               MY_PROVE_HYP df_th o MY_PROVE_HYP dd_th o
 260               INST([f1_tm, f_var; f2_tm, g_var;
 261                    domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 262                    bounds_tm, bounds_var] @ inst_list)) mul_ths_array.(n) in
 263   let eq_th = binary_beta_gen_eq f1_tm f2_tm x_var mul_op_real in
 264     m_taylor_interval_norm th eq_th;;
 265
 266
 267
 268 (******************************)
 269 (* inv *)
 270
 271 let eval_m_taylor_inv2 n p_lin p_second taylor1_th =
 272   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 273   let f1_tm = (rand o concl) diff2_f1_th in
 274   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 275
 276   let ty = type_of y_tm in
 277   let x_var = mk_var ("x", ty) and
 278       y_var = mk_var ("y", ty) and
 279       w_var = mk_var ("w", ty) and
 280       f_var = mk_var ("f", type_of f1_tm) and
 281       domain_var = mk_var ("domain", type_of domain_tm) in
 282
 283   let undisch = UNDISCH o SPEC x_var in
 284
 285   let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
 286   let f1_bound = undisch f1_bound0 in
 287   let f_bounds_tm = (rand o concl) f1_bound in
 288
 289   (* cond *)
 290   let cond_th = check_interval_not_zero f_bounds_tm in
 291
 292   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 293
 294   let bounds_th = float_interval_inv p_lin bounds1_th in
 295   let bounds_tm = (rand o concl) bounds_th in
 296
 297   (* first partials *)
 298   let u_bounds =
 299     let neg, inv, ( * ) = float_interval_neg, float_interval_inv p_lin, float_interval_mul p_lin in
 300       neg (inv (bounds1_th * bounds1_th)) in
 301
 302   let df1_ths' = all_n_components2 n df1_th in
 303   let df1_ths = map MY_BETA_RULE df1_ths' in
 304
 305   let df_ths =
 306     let ( * ) = float_interval_mul p_lin in
 307       map (fun th1 -> u_bounds * th1) df1_ths in
 308
 309   let df_th = end_itlist CONJ df_ths in
 310
 311   (* second partials *)
 312   let dd_ths =
 313     let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
 314       map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
 315
 316   let d1_bounds = map (fun i ->
 317                          let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
 318                            undisch th0) (1--n) in
 319
 320   (* u'(f x), u''(f x) *)
 321   let d1_th0, d2_th0 =
 322     let inv, ( * ) = float_interval_inv p_second, float_interval_mul p_second in
 323     let ff = f1_bound * f1_bound in
 324       inv ff,
 325     two_interval * inv (f1_bound * ff) in
 326
 327   let dd_ths =
 328     let ( * ), ( - ) = float_interval_mul p_second, float_interval_sub p_second in
 329       map2 (fun dd_list di1 ->
 330               my_map2 (fun dd dj1 ->
 331                          (d2_th0 * dj1) * di1 - d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
 332
 333   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 334
 335   (***)
 336   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 337   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 338
 339   let dfs = map (rand o concl) df_ths in
 340   let dds = map (map (rand o concl)) dd_ths in
 341
 342   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 343
 344   let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
 345                MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 346                MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
 347                INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
 348                   domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 349                   bounds_tm, bounds_var] @ inst_list)) inv_ths_array.(n) in
 350   let eq_th = unary_beta_gen_eq f1_tm x_var inv_op_real in
 351     m_taylor_interval_norm th1 eq_th;;
 352
 353
 354
 355 (******************************)
 356 (* sqrt *)
 357
 358 let eval_m_taylor_sqrt2 n p_lin p_second taylor1_th =
 359   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 360   let f1_tm = (rand o concl) diff2_f1_th in
 361   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 362
 363   let ty = type_of y_tm in
 364   let x_var = mk_var ("x", ty) and
 365       y_var = mk_var ("y", ty) and
 366       w_var = mk_var ("w", ty) and
 367       f_var = mk_var ("f", type_of f1_tm) and
 368       domain_var = mk_var ("domain", type_of domain_tm) in
 369
 370   let undisch = UNDISCH o SPEC x_var in
 371
 372   let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
 373   let f1_bound = undisch f1_bound0 in
 374   let f_bounds_tm = (rand o concl) f1_bound in
 375
 376   (* cond *)
 377   let cond_th = check_interval_pos f_bounds_tm in
 378
 379   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 380
 381   let bounds_th = float_interval_sqrt p_lin bounds1_th in
 382   let bounds_tm = (rand o concl) bounds_th in
 383
 384   (* first partials *)
 385   let u_bounds =
 386     let inv, ( * ) = float_interval_inv p_lin, float_interval_mul p_lin in
 387       inv (two_interval * bounds_th) in
 388
 389   let df1_ths' = all_n_components2 n df1_th in
 390   let df1_ths = map MY_BETA_RULE df1_ths' in
 391
 392   let df_ths =
 393     let ( * ) = float_interval_mul p_lin in
 394       map (fun th1 -> u_bounds * th1) df1_ths in
 395
 396   let df_th = end_itlist CONJ df_ths in
 397
 398   (* second partials *)
 399   let dd_ths =
 400     let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
 401       map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
 402
 403   let d1_bounds = map (fun i ->
 404                          let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
 405                            undisch th0) (1--n) in
 406
 407   (* u'(f x), u''(f x) *)
 408   let d1_th0, d2_th0 =
 409     let neg, sqrt, inv, ( * ) = float_interval_neg, float_interval_sqrt p_second,
 410       float_interval_inv p_second, float_interval_mul p_second in
 411     let two_sqrt_f = two_interval * sqrt f1_bound in
 412       inv two_sqrt_f, neg (inv (two_sqrt_f * (two_interval * f1_bound))) in
 413
 414   let dd_ths =
 415     let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
 416       map2 (fun dd_list di1 ->
 417               my_map2 (fun dd dj1 ->
 418                       (d2_th0 * dj1) * di1 + d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
 419
 420   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 421
 422   (***)
 423   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 424   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 425
 426   let dfs = map (rand o concl) df_ths in
 427   let dds = map (map (rand o concl)) dd_ths in
 428
 429   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 430
 431   let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
 432                MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 433                MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
 434                INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
 435                   domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 436                   bounds_tm, bounds_var] @ inst_list)) sqrt_ths_array.(n) in
 437   let eq_th = unary_beta_gen_eq f1_tm x_var sqrt_tm in
 438     m_taylor_interval_norm th1 eq_th;;
 439
 440
 441
 442 (******************************)
 443 (* atn *)
 444
 445 let eval_m_taylor_atn2 n p_lin p_second taylor1_th =
 446   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 447   let f1_tm = (rand o concl) diff2_f1_th in
 448   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 449
 450   let ty = type_of y_tm in
 451   let x_var = mk_var ("x", ty) and
 452       y_var = mk_var ("y", ty) and
 453       w_var = mk_var ("w", ty) and
 454       f_var = mk_var ("f", type_of f1_tm) and
 455       domain_var = mk_var ("domain", type_of domain_tm) in
 456
 457   let undisch = UNDISCH o SPEC x_var in
 458
 459   let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
 460   let f1_bound = undisch f1_bound0 in
 461   let f_bounds_tm = (rand o concl) f1_bound in
 462
 463   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 464
 465   let bounds_th = float_interval_atn p_lin bounds1_th in
 466   let bounds_tm = (rand o concl) bounds_th in
 467
 468   (* first partials *)
 469   let u_bounds =
 470     let inv, ( + ), ( * ) = float_interval_inv p_lin,
 471       float_interval_add p_lin, float_interval_mul p_lin in
 472       inv (one_interval + bounds1_th * bounds1_th) in
 473
 474   let df1_ths' = all_n_components2 n df1_th in
 475   let df1_ths = map MY_BETA_RULE df1_ths' in
 476
 477   let df_ths =
 478     let ( * ) = float_interval_mul p_lin in
 479       map (fun th1 -> u_bounds * th1) df1_ths in
 480
 481   let df_th = end_itlist CONJ df_ths in
 482
 483   (* second partials *)
 484   let dd_ths =
 485     let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
 486       map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
 487
 488   let d1_bounds = map (fun i ->
 489                          let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
 490                            undisch th0) (1--n) in
 491
 492   (* u'(f x), u''(f x) *)
 493   let d1_th0, d2_th0 =
 494     let neg, inv, ( + ), ( * ), pow2 = float_interval_neg, float_interval_inv p_second,
 495       float_interval_add p_second, float_interval_mul p_second, float_interval_pow_simple p_second 2 in
 496     let inv_one_ff = inv (one_interval + f1_bound * f1_bound) in
 497       inv_one_ff, (neg_two_interval * f1_bound) * pow2 inv_one_ff in
 498
 499   let dd_ths =
 500     let ( * ), ( + ) = float_interval_mul p_second, float_interval_add p_second in
 501       map2 (fun dd_list di1 ->
 502               my_map2 (fun dd dj1 ->
 503                       (d2_th0 * dj1) * di1 + d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
 504
 505   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 506
 507   (***)
 508   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 509   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 510
 511   let dfs = map (rand o concl) df_ths in
 512   let dds = map (map (rand o concl)) dd_ths in
 513
 514   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 515
 516   let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP f1_bound0 o
 517                MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 518                MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
 519                INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
 520                   domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 521                   bounds_tm, bounds_var] @ inst_list)) atn_ths_array.(n) in
 522   let eq_th = unary_beta_gen_eq f1_tm x_var atn_tm in
 523     m_taylor_interval_norm th1 eq_th;;
 524
 525
 526 (******************************)
 527 (* acs *)
 528
 529 let eval_m_taylor_acs2 n p_lin p_second taylor1_th =
 530   let domain_th, diff2_f1_th, lin1_th, second1_th = dest_m_taylor_thms n taylor1_th in
 531   let f1_tm = (rand o concl) diff2_f1_th in
 532   let domain_tm, y_tm, w_tm = dest_m_cell_domain (concl domain_th) in
 533
 534   let ty = type_of y_tm in
 535   let x_var = mk_var ("x", ty) and
 536       y_var = mk_var ("y", ty) and
 537       w_var = mk_var ("w", ty) and
 538       f_var = mk_var ("f", type_of f1_tm) and
 539       domain_var = mk_var ("domain", type_of domain_tm) in
 540
 541   let undisch = UNDISCH o SPEC x_var in
 542
 543   let f1_bound0 = eval_m_taylor_bound n p_second taylor1_th in
 544   let f1_bound = undisch f1_bound0 in
 545   let f_bounds_tm = (rand o concl) f1_bound in
 546
 547   (* cond *)
 548   let cond_th = EQT_ELIM (check_interval_iabs f_bounds_tm one_float) in
 549
 550   let _, bounds1_th, df1_th = m_lin_approx_components n lin1_th in
 551
 552   let bounds_th = float_interval_acs p_lin bounds1_th in
 553   let bounds_tm = (rand o concl) bounds_th in
 554
 555   (* first partials *)
 556   let u_bounds =
 557     let inv, sqrt, neg = float_interval_inv p_lin, float_interval_sqrt p_lin, float_interval_neg in
 558     let ( * ), ( - ) = float_interval_mul p_lin, float_interval_sub p_lin in
 559       neg (inv (sqrt (one_interval - bounds1_th * bounds1_th))) in
 560
 561   let df1_ths' = all_n_components2 n df1_th in
 562   let df1_ths = map MY_BETA_RULE df1_ths' in
 563
 564   let df_ths =
 565     let ( * ) = float_interval_mul p_lin in
 566       map (fun th1 -> u_bounds * th1) df1_ths in
 567
 568   let df_th = end_itlist CONJ df_ths in
 569
 570   (* second partials *)
 571   let dd_ths =
 572     let dd1 = all_n_components2 n (second_bounded_components n second1_th) in
 573       map2 (fun i -> map MY_BETA_RULE o all_n_components2 i o MY_BETA_RULE) (1--n) dd1 in
 574
 575   let d1_bounds = map (fun i ->
 576                          let th0 = eval_m_taylor_partial_bound n p_second i taylor1_th in
 577                            undisch th0) (1--n) in
 578
 579   (* u'(f x), u''(f x) *)
 580   let d1_th0, d2_th0 =
 581     let neg, sqrt, inv = float_interval_neg, float_interval_sqrt p_second, float_interval_inv p_second in
 582     let ( - ), ( * ), ( / ), pow3 = float_interval_sub p_second, float_interval_mul p_second,
 583       float_interval_div p_second, float_interval_pow_simple p_second 3 in
 584     let ff_1 = one_interval - f1_bound * f1_bound in
 585       inv (sqrt ff_1), neg (f1_bound / sqrt (pow3 ff_1)) in
 586
 587   let dd_ths =
 588     let ( * ), ( - ) = float_interval_mul p_second, float_interval_sub p_second in
 589       map2 (fun dd_list di1 ->
 590               my_map2 (fun dd dj1 ->
 591                          (d2_th0 * dj1) * di1 - d1_th0 * dd) dd_list d1_bounds) dd_ths d1_bounds in
 592
 593   let dd_th = (GEN x_var o DISCH_ALL o end_itlist CONJ) (List.flatten dd_ths) in
 594
 595   (***)
 596   let df_vars = map (fun i -> df_vars_array.(i)) (1--n) in
 597   let dd_vars = map (fun i -> map (fun j -> dd_vars_array.(i).(j)) (1--i)) (1--n) in
 598
 599   let dfs = map (rand o concl) df_ths in
 600   let dds = map (map (rand o concl)) dd_ths in
 601
 602   let inst_list = union (zip dfs df_vars) (zip (List.flatten dds) (List.flatten dd_vars)) in
 603
 604   let th1 = (MY_PROVE_HYP diff2_f1_th o MY_PROVE_HYP cond_th o MY_PROVE_HYP f1_bound0 o
 605                MY_PROVE_HYP bounds_th o MY_PROVE_HYP domain_th o
 606                MY_PROVE_HYP dd_th o MY_PROVE_HYP df_th o
 607                INST([f1_tm, f_var; f_bounds_tm, f_bounds_var;
 608                   domain_tm, domain_var; y_tm, y_var; w_tm, w_var;
 609                   bounds_tm, bounds_var] @ inst_list)) acs_ths_array.(n) in
 610   let eq_th = unary_beta_gen_eq f1_tm x_var acs_tm in
 611     m_taylor_interval_norm th1 eq_th;;
 612
 613
 614
 615 (*******************************)
 616
 617
 618 (*
 619 let n = 3;;
 620 let pp = 2;;
 621
 622 let xx = mk_vector_list [one_float; one_float; one_float];;
 623 let r = mk_float 27182 46;;
 624 let r = mk_float 11 49;;
 625 let zz = mk_vector_list [r; r; r];;
 626
 627 let r = mk_float 0 50;;
 628 let xx = mk_vector_list [r; r; r];;
 629 let r = mk_float 1 49;;
 630 let zz = mk_vector_list [r; r; r];;
 631
 632 let domain_th = mk_m_center_domain n pp (rand xx) (rand zz);;
 633 let f1 = expr_to_vector_fun `x1 + x2 * x3 + pi`;;
 634 let f2 = `\x:real^3. x$2 * x$2 + &2 * pi`;;
 635 let taylor1 = eval_m_taylor_poly0 pp f1 pp pp domain_th;;
 636 let taylor2 = eval_m_taylor_poly0 pp f2 pp pp domain_th;;
 637
 638 eval_m_taylor_inv n pp pp taylor1;;
 639 eval_m_taylor_inv2 n pp pp taylor1;;
 640 (* 200: 1.240 *)
 641 test 100 (eval_m_taylor_inv n pp pp) taylor1;;
 642 (* 200: 1.124 *)
 643 test 100 (eval_m_taylor_inv2 n pp pp) taylor1;;
 644
 645 (* 200: 1.236 *)
 646 test 100 (eval_m_taylor_sqrt 3 2 2) taylor1;;
 647 (* 200: 0.992 *)
 648 test 100 (eval_m_taylor_sqrt2 3 2 2) taylor1;;
 649
 650 eval_m_taylor_add2 3 2 2 taylor1 taylor2;;
 651 eval_m_taylor_sub2 3 2 2 taylor1 taylor2;;
 652 (* 200: 0.604 *)
 653 test 100 (eval_m_taylor_add 3 2 2 taylor1) taylor2;;
 654 (* 200: 0.392 *)
 655 test 100 (eval_m_taylor_add2 3 2 2 taylor1) taylor2;;
 656
 657 eval_m_taylor_mul2 3 2 2 taylor1 taylor2;;
 658 (* 200: 2.140 *)
 659 test 100 (eval_m_taylor_mul 3 2 2 taylor1) taylor2;;
 660 (* 200: 1.924 *)
 661 test 100 (eval_m_taylor_mul2 3 2 2 taylor1) taylor2;;
 662
 663 eval_m_taylor_atn2 3 2 2 taylor1;;
 664 (* 200: 1.416 *)
 665 test 100 (eval_m_taylor_atn 3 2 2) taylor1;;
 666 (* 200: 1.152 *)
 667 test 100 (eval_m_taylor_atn2 3 2 2) taylor1;;
 668 *)
 669