formal_lp/old/formal_interval/second_approx.hl

   1 needs "../formal_lp/formal_interval/lin_approx.hl";;\r
   2 \r
   3 (* Explicit formula (float) for inv(&2) *)\r
   4 \r
   5 let float_inv2_th =\r
   6   let one_float_eq_one = FLOAT_TO_NUM_CONV one_float in\r
   7   let inv2_eq_lemma = prove(`interval_arith (&2 * x) (&1, &1) ==> inv (&2) = x`,\r
   8                             REWRITE_TAC[interval_arith] THEN CONV_TAC REAL_FIELD) in\r
   9   let half_tm = (fst o dest_pair o rand o concl) (float_interval_inv 1 two_interval) in\r
  10   let half_interval = mk_const_interval half_tm in\r
  11   let mul_th = REWRITE_RULE[one_float_eq_one] (float_interval_mul 2 two_interval half_interval) in\r
  12     MATCH_MP inv2_eq_lemma mul_th;;\r
  13 \r
  14 let float_inv2 = rand (concl float_inv2_th);;\r
  15 let inv2_interval = mk_const_interval float_inv2;;\r
  16 \r
  17 let INTERVAL_IMP_HI = (RULE o prove)(`interval_arith x (lo, hi) ==> x <= hi`,\r
  18                                      REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
  19 \r
  20 let interval_imp_hi int_th =\r
  21   let lhs, bounds = dest_comb (concl int_th) in\r
  22   let x_tm, (lo_tm, hi_tm) = rand lhs, dest_pair bounds in\r
  23   let th0 = INST[x_tm, x_var_real; lo_tm, lo_var_real; hi_tm, hi_var_real] INTERVAL_IMP_HI in\r
  24     MY_PROVE_HYP int_th th0;;\r
  25 \r
  26 \r
  27 (*****************************)\r
  28 (* cell_domain *)\r
  29 \r
  30 let dest_cell_domain tm =\r
  31   let lhs, w_tm = dest_comb tm in\r
  32   let lhs2, z_tm = dest_comb lhs in\r
  33   let lhs3, y_tm = dest_comb lhs2 in\r
  34     rand lhs3, y_tm, z_tm, w_tm;;\r
  35 \r
  36 \r
  37 (******************************************)\r
  38 \r
  39 let CELL_DOMAIN_IMP_INTERVAL_ARITH = prove(`cell_domain x y z w ==> interval_arith y (x, z)`,\r
  40                                            REWRITE_TAC[cell_domain; interval_arith] THEN REAL_ARITH_TAC);;\r
  41 \r
  42 \r
  43 let MK_CELL_DOMAIN_0' = (UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o prove)\r
  44   (`(x <= y <=> T) /\ (y <= z <=> T) /\ y - x <= w1 /\ z - y <= w2 /\ (w1 <= w <=> T) /\ (w2 <= w <=> T) ==> \r
  45      cell_domain x y z w`,\r
  46    SIMP_TAC[cell_domain] THEN REAL_ARITH_TAC);;\r
  47 \r
  48 \r
  49 let MK_CELL_DOMAIN' = (UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o prove)\r
  50   (`(x <= y <=> T) /\ (y <= z <=> T) /\ y - x <= w1 /\ z - y <= w2 /\ max w1 w2 = w ==>\r
  51                                        cell_domain x y z w`, REWRITE_TAC[cell_domain] THEN REAL_ARITH_TAC);;\r
  52 \r
  53 \r
  54 let mk_cell_domain0 pp x_tm y_tm z_tm w_tm =\r
  55   let xy_th = float_le x_tm y_tm and\r
  56       yz_th = float_le y_tm z_tm in\r
  57   let yx_w1 = float_sub_hi pp y_tm x_tm and\r
  58       zy_w2 = float_sub_hi pp z_tm y_tm in\r
  59   let w1_tm = (rand o concl) yx_w1 and\r
  60       w2_tm = (rand o concl) zy_w2 in\r
  61   let w1w = float_le w1_tm w_tm and\r
  62       w2w = float_le w2_tm w_tm in\r
  63   let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; \r
  64                  w_tm, w_var_real; w1_tm, w1_var_real; w2_tm, w2_var_real] MK_CELL_DOMAIN_0' in\r
  65     (MY_PROVE_HYP xy_th o MY_PROVE_HYP yz_th o MY_PROVE_HYP yx_w1 o MY_PROVE_HYP zy_w2 o\r
  66        MY_PROVE_HYP w1w o MY_PROVE_HYP w2w) th0;;\r
  67 \r
  68 \r
  69 let mk_cell_domain pp x_tm y_tm z_tm =\r
  70   let w1_th = float_sub_hi pp y_tm x_tm and\r
  71       w2_th = float_sub_hi pp z_tm y_tm in\r
  72   let w1_tm = (rand o concl) w1_th and\r
  73       w2_tm = (rand o concl) w2_th in\r
  74   let max_th = float_max w1_tm w2_tm in\r
  75   let w_tm = (rand o concl) max_th in\r
  76   let x_le_y = float_le x_tm y_tm and\r
  77       y_le_z = float_le y_tm z_tm in\r
  78   let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;\r
  79                  w_tm, w_var_real; w1_tm, w1_var_real; w2_tm, w2_var_real] MK_CELL_DOMAIN' in\r
  80     (MY_PROVE_HYP x_le_y o MY_PROVE_HYP y_le_z o \r
  81        MY_PROVE_HYP w1_th o MY_PROVE_HYP w2_th o MY_PROVE_HYP max_th) th0;;\r
  82   \r
  83 \r
  84 \r
  85 \r
  86 (* TODO: remove formal computation of y *)\r
  87 let mk_center_domain pp x_tm z_tm =\r
  88   let y0_tm = (rand o concl) (float_add_hi pp x_tm z_tm) in\r
  89   let y_tm = (rand o concl) (float_mul_eq float_inv2 y0_tm) in\r
  90     mk_cell_domain pp x_tm y_tm z_tm;;\r
  91 \r
  92 \r
  93 (*\r
  94 let x_tm = mk_float 1 50;;\r
  95 let z_tm = mk_float 4 50;;\r
  96 \r
  97 let domain_th = mk_center_domain 2 x_tm z_tm;;\r
  98 \r
  99 let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th);;\r
 100 mk_cell_domain 2 x_tm y_tm z_tm;;\r
 101 mk_cell_domain0 2 x_tm y_tm z_tm w_tm;;\r
 102 *)\r
 103 \r
 104 \r
 105 (***************************************************)\r
 106 (* Elementary functions and their taylor intervals *)\r
 107 (***************************************************)\r
 108 \r
 109 \r
 110 (*****************************)\r
 111 (* f(x) = x *)\r
 112 \r
 113 let TAYLOR_X' = RULE taylor_x;;\r
 114 \r
 115 \r
 116 let eval_taylor_x domain_th =\r
 117   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 118   let th0 = INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real] TAYLOR_X' in\r
 119     MY_PROVE_HYP domain_th th0;;\r
 120 \r
 121  \r
 122 (*                        \r
 123 eval_taylor_x domain_th;;\r
 124 *)\r
 125 \r
 126 (********************************)\r
 127 (* f(x) = const *)\r
 128 \r
 129 let TAYLOR_CONST' = RULE taylor_const;;\r
 130 let eval_taylor_const domain_th c_tm =\r
 131   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 132     (MY_PROVE_HYP domain_th o\r
 133        INST[c_tm, c_var_real; x_tm, x_var_real; y_tm, y_var_real; \r
 134             z_tm, z_var_real; w_tm, w_var_real]) TAYLOR_CONST';;\r
 135 \r
 136 \r
 137 let TAYLOR_CONST_INTERVAL' = (RULE o prove)\r
 138   (`cell_domain x y z w ==> interval_arith c bounds ==>\r
 139      taylor_interval (\x. c) x y z w bounds (&0, &0) (&0, &0)`,\r
 140   REPEAT DISCH_TAC THEN\r
 141     MP_TAC (SPEC_ALL taylor_const) THEN ASM_SIMP_TAC[taylor_interval; lin_approx_eq]);;\r
 142 \r
 143 let eval_taylor_const_interval int_th domain_th =\r
 144   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 145   let lhs, bounds = dest_comb (concl int_th) in\r
 146   let c_tm = rand lhs in\r
 147     (MY_PROVE_HYP int_th o MY_PROVE_HYP domain_th o\r
 148        INST[c_tm, c_var_real; bounds, bounds_var; x_tm, x_var_real; y_tm, y_var_real;\r
 149             z_tm, z_var_real; w_tm, w_var_real]) TAYLOR_CONST_INTERVAL';;\r
 150 \r
 151 \r
 152 (*\r
 153 eval_taylor_const domain_th `&3`;;\r
 154 *)\r
 155 \r
 156 (***********************************)\r
 157 (* f(x) = atn x *)\r
 158 \r
 159 let taylor_atn = prove(`cell_domain x y z w ==>\r
 160                          bounded_on_int (\x. (-- &2 * x) / (&1 + x pow 2) pow 2) (x,z) dd_bounds ==>\r
 161                          lin_approx atn y f_bounds df_bounds ==>\r
 162                          taylor_interval atn x y z w f_bounds df_bounds dd_bounds`,\r
 163   REWRITE_TAC[cell_domain; taylor_interval; real_div; REAL_INV_POW] THEN REPEAT DISCH_TAC THEN \r
 164     ASM_REWRITE_TAC[] THEN\r
 165     MATCH_MP_TAC second_derivative_atn_bounds THEN ASM_REWRITE_TAC[]);;\r
 166 \r
 167 let TAYLOR_ATN' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2]) taylor_atn;;\r
 168 \r
 169 \r
 170 let eval_taylor_atn pp domain_th =\r
 171   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 172   let atn_lin = eval_lin_approx_atn pp y_tm in\r
 173   let _, _, f_bounds, df_bounds = dest_lin_approx (concl atn_lin) in\r
 174 \r
 175   let ddf_th = \r
 176     let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and\r
 177         ( * ) = float_interval_mul pp and\r
 178         (+) = float_interval_add pp and\r
 179         (/) = float_interval_div pp in\r
 180     let x2_1 = one_interval + x_th * x_th in\r
 181       mk_bounded_on_int ((neg_two_interval * x_th) / (x2_1 * x2_1)) in\r
 182  \r
 183   let dd_bounds = rand (concl ddf_th) in\r
 184     (MY_PROVE_HYP domain_th o MY_PROVE_HYP atn_lin o MY_PROVE_HYP ddf_th o\r
 185        INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 186             dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_ATN';;\r
 187 \r
 188 \r
 189 \r
 190 (*\r
 191 let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;\r
 192 let pp = 5;;\r
 193 eval_taylor_atn pp domain_th;;\r
 194 *)\r
 195 \r
 196 \r
 197 \r
 198 (***********************************)\r
 199 (* f(x) = inv x *)\r
 200 \r
 201 let taylor_inv = prove(`cell_domain x y z w ==>\r
 202                          interval_not_zero (x,z) ==>\r
 203                          bounded_on_int (\x. &2 * inv (x pow 3)) (x,z) dd_bounds ==>\r
 204                          lin_approx inv y f_bounds df_bounds ==>\r
 205                          taylor_interval inv x y z w f_bounds df_bounds dd_bounds`,\r
 206   REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN \r
 207     ASM_REWRITE_TAC[] THEN\r
 208     MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_inv_bounds) THEN ASM_REWRITE_TAC[]);;\r
 209 \r
 210 let TAYLOR_INV' = (UNDISCH_ALL o REWRITE_RULE[GSYM real_div; REAL_ARITH `x pow 3 = x * x * x`]) taylor_inv;;\r
 211 \r
 212 \r
 213 let eval_taylor_inv pp domain_th =\r
 214   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 215   let int_tm = mk_pair (x_tm, z_tm) in\r
 216   let lin_th = eval_lin_approx_inv pp y_tm in\r
 217   let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in\r
 218   let cond_th = check_interval_not_zero int_tm in\r
 219 \r
 220   let ddf_th = \r
 221     let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and\r
 222         ( * ) = float_interval_mul pp and\r
 223         (/) = float_interval_div pp in\r
 224       mk_bounded_on_int (two_interval / (x_th * (x_th * x_th))) in\r
 225  \r
 226   let dd_bounds = rand (concl ddf_th) in\r
 227     (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o\r
 228        INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 229             dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_INV';;\r
 230 \r
 231 \r
 232 \r
 233 (*\r
 234 let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;\r
 235 let pp = 5;;\r
 236 eval_taylor_inv pp domain_th;;\r
 237 *)\r
 238 \r
 239 \r
 240 (***********************************)\r
 241 (* f(x) = sqrt x *)\r
 242 \r
 243 let taylor_sqrt = prove(`cell_domain x y z w ==>\r
 244                          interval_pos (x,z) ==>\r
 245                          bounded_on_int (\x. --inv (&4 * sqrt (x pow 3))) (x,z) dd_bounds ==>\r
 246                          lin_approx sqrt y f_bounds df_bounds ==>\r
 247                          taylor_interval sqrt x y z w f_bounds df_bounds dd_bounds`,\r
 248   REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN \r
 249     ASM_REWRITE_TAC[] THEN\r
 250     MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_sqrt_bounds) THEN ASM_REWRITE_TAC[]);;\r
 251 \r
 252 let TAYLOR_SQRT' = (UNDISCH_ALL o REWRITE_RULE[REAL_ARITH `x pow 3 = x * x * x`]) taylor_sqrt;;\r
 253 let four_interval = mk_float_interval_small_num 4;;\r
 254 \r
 255 \r
 256 let eval_taylor_sqrt pp domain_th =\r
 257   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 258   let int_tm = mk_pair (x_tm, z_tm) in\r
 259   let lin_th = eval_lin_approx_sqrt pp y_tm in\r
 260   let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in\r
 261   let cond_th = check_interval_pos int_tm in\r
 262 \r
 263   let ddf_th = \r
 264     let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and\r
 265         ( * ) = float_interval_mul pp and\r
 266         sqrt = float_interval_sqrt pp and\r
 267         inv = float_interval_inv pp and\r
 268         neg = float_interval_neg in\r
 269       mk_bounded_on_int (neg (inv (four_interval * sqrt (x_th * (x_th * x_th))))) in\r
 270  \r
 271   let dd_bounds = rand (concl ddf_th) in\r
 272     (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o\r
 273        INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 274             dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_SQRT';;\r
 275 \r
 276 \r
 277 \r
 278 (*\r
 279 let domain_th = mk_center_domain 5 (mk_float 1 50) (mk_float 4 50);;\r
 280 let pp = 5;;\r
 281 eval_taylor_sqrt pp domain_th;;\r
 282 *)\r
 283 \r
 284 \r
 285 (***********************************)\r
 286 (* f(x) = acs x *)\r
 287 \r
 288 let iabs_lt1_lemma = \r
 289   (GEN_REWRITE_RULE (RAND_CONV o LAND_CONV o RAND_CONV) [GSYM (FLOAT_TO_NUM_CONV one_float)] o prove)\r
 290     (`iabs int < &1 <=> (iabs int < &1 <=> T)`, REWRITE_TAC[]);;\r
 291 \r
 292 let taylor_acs = prove(`cell_domain x y z w ==>\r
 293                          iabs (x,z) < &1 ==>\r
 294                          bounded_on_int (\x. --(x / sqrt ((&1 - x * x) pow 3))) (x,z) dd_bounds ==>\r
 295                          lin_approx acs y f_bounds df_bounds ==>\r
 296                          taylor_interval acs x y z w f_bounds df_bounds dd_bounds`,\r
 297   REWRITE_TAC[cell_domain; taylor_interval] THEN REPEAT DISCH_TAC THEN \r
 298     ASM_REWRITE_TAC[] THEN\r
 299     MATCH_MP_TAC (REWRITE_RULE[IMP_IMP] second_derivative_acs_bounds) THEN ASM_REWRITE_TAC[]);;\r
 300 \r
 301 let TAYLOR_ACS' = \r
 302   (UNDISCH_ALL o \r
 303      PURE_ONCE_REWRITE_RULE[iabs_lt1_lemma] o\r
 304      REWRITE_RULE[REAL_ARITH `x pow 3 = x * x * x`]) taylor_acs;;\r
 305 \r
 306 \r
 307 let eval_taylor_acs pp domain_th =\r
 308   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 309   let int_tm = mk_pair (x_tm, z_tm) in\r
 310   let lin_th = eval_lin_approx_acs pp y_tm in\r
 311   let _, _, f_bounds, df_bounds = dest_lin_approx (concl lin_th) in\r
 312   let cond_th = check_interval_iabs int_tm one_float in\r
 313 \r
 314   let ddf_th = \r
 315     let x_th = ASSUME (mk_interval x_var_real (mk_pair (x_tm, z_tm))) and\r
 316         ( * ) = float_interval_mul pp and\r
 317         (-) = float_interval_sub pp and\r
 318         (/) = float_interval_div pp and\r
 319         sqrt = float_interval_sqrt pp and\r
 320         neg = float_interval_neg in\r
 321     let x2_1 = one_interval - x_th * x_th in\r
 322       mk_bounded_on_int (neg (x_th / sqrt (x2_1 * (x2_1 * x2_1)))) in\r
 323  \r
 324   let dd_bounds = rand (concl ddf_th) in\r
 325     (MY_PROVE_HYP domain_th o MY_PROVE_HYP lin_th o MY_PROVE_HYP ddf_th o MY_PROVE_HYP cond_th o\r
 326        INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 327             dd_bounds, dd_bounds_var; f_bounds, f_bounds_var; df_bounds, df_bounds_var]) TAYLOR_ACS';;\r
 328 \r
 329 \r
 330 \r
 331 (*\r
 332 let domain_th1 = mk_center_domain 5 (mk_float 1 49) (mk_float 8 49);;\r
 333 let domain_th2 = mk_center_domain 5 (mk_float (-5) 49) (mk_float 1 49);;\r
 334 let pp = 5;;\r
 335 eval_taylor_acs pp domain_th1;;\r
 336 eval_taylor_atn pp domain_th1;;\r
 337 eval_taylor_inv pp domain_th1;;\r
 338 eval_taylor_sqrt pp domain_th1;;\r
 339 \r
 340 eval_taylor_acs pp domain_th2;;\r
 341 eval_taylor_atn pp domain_th2;;\r
 342 eval_taylor_inv pp domain_th2;;\r
 343 eval_taylor_sqrt pp domain_th2;;\r
 344 *)\r
 345 \r
 346 \r
 347 (***********************************************************)\r
 348 \r
 349 \r
 350 (***********************************)\r
 351 (* Taylor bounds *)\r
 352 \r
 353 \r
 354 let dest_taylor_interval tm =\r
 355   let lhs, dd_bounds = dest_comb tm in\r
 356   let lhs, df_bounds = dest_comb lhs in\r
 357   let lhs, f_bounds = dest_comb lhs in\r
 358   let lhs, w_tm = dest_comb lhs in\r
 359   let lhs, z_tm = dest_comb lhs in\r
 360   let lhs, y_tm = dest_comb lhs in\r
 361   let lhs, x_tm = dest_comb lhs in\r
 362     rand lhs, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds;;\r
 363 \r
 364 \r
 365 (****************************)\r
 366 (* f_bounds *)\r
 367 \r
 368 let TAYLOR_F_BOUNDS' = (RULE o REWRITE_RULE[float_inv2_th]) taylor_f_bounds;;\r
 369 \r
 370 \r
 371 let eval_taylor_f_bounds pp th =\r
 372   let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in\r
 373   let f_lo, f_hi = dest_pair f_bounds in\r
 374   let iabs_df_th = float_iabs df_bounds and\r
 375       iabs_dd_th = float_iabs dd_bounds in\r
 376   let df_tm = (rand o concl) iabs_df_th and\r
 377       dd_tm = (rand o concl) iabs_dd_th in\r
 378 \r
 379   let error_th =\r
 380     let df = mk_refl_ineq df_tm and\r
 381         inv2 = mk_refl_ineq float_inv2 and\r
 382         ( * ) = mul_ineq_pos_const_hi pp and\r
 383         ( + ) = add_ineq_hi pp in\r
 384       w_tm * (df + w_tm * (dd_tm * inv2)) in\r
 385 \r
 386   let t_tm = (rand o concl) error_th in\r
 387   let lo_th = float_sub_lo pp f_lo t_tm and\r
 388       hi_th = float_add_hi pp f_hi t_tm in\r
 389   let lo_tm = (lhand o concl) lo_th and\r
 390       hi_tm = (rand o concl) hi_th in\r
 391 \r
 392     (MY_PROVE_HYP lo_th o MY_PROVE_HYP hi_th o MY_PROVE_HYP error_th o \r
 393        MY_PROVE_HYP iabs_df_th o MY_PROVE_HYP iabs_dd_th o MY_PROVE_HYP th o\r
 394        INST[dd_bounds, dd_bounds_var; dd_tm, dd_var_real; df_bounds, df_bounds_var;\r
 395             df_tm, df_var_real; t_tm, t_var_real;\r
 396             lo_tm, lo_var_real; f_lo, f_lo_var;\r
 397             w_tm, w_var_real; f_hi, f_hi_var; hi_tm, hi_var_real;\r
 398             f_tm, f_var_fun; x_tm, x_var_real; \r
 399             y_tm, y_var_real; z_tm, z_var_real]) TAYLOR_F_BOUNDS';;\r
 400 \r
 401 \r
 402 (*\r
 403 let pp = 3;;\r
 404 let domain_th = mk_center_domain pp one_float two_float;;\r
 405 let th = eval_taylor_atn pp domain_th;;\r
 406 eval_taylor_f_bounds pp th;;\r
 407 (* 10: 1.620 *)\r
 408 test 1000 (eval_taylor_f_bounds pp) th;;\r
 409 *)\r
 410 \r
 411 \r
 412 (****************************)\r
 413 (* df_bounds *)\r
 414 \r
 415 \r
 416 let TAYLOR_DF_BOUNDS' = RULE taylor_df_bounds;;\r
 417 \r
 418 let eval_taylor_df_bounds pp th =\r
 419   let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in\r
 420   let df_lo, df_hi = dest_pair df_bounds in\r
 421   let iabs_dd_th = float_iabs dd_bounds in\r
 422   let dd_tm = (rand o concl) iabs_dd_th in\r
 423   let w_dd_hi = float_mul_hi pp w_tm dd_tm in\r
 424 \r
 425   let lo_th = sub_ineq_lo pp (mk_refl_ineq df_lo) w_dd_hi and\r
 426       hi_th = add_ineq_hi pp (mk_refl_ineq df_hi) w_dd_hi in\r
 427   let lo_tm = (lhand o concl) lo_th and\r
 428       hi_tm = (rand o concl) hi_th in\r
 429 \r
 430     (MY_PROVE_HYP lo_th o MY_PROVE_HYP hi_th o MY_PROVE_HYP th o MY_PROVE_HYP iabs_dd_th o\r
 431        INST[dd_bounds, dd_bounds_var; dd_tm, dd_var_real; f_bounds, f_bounds_var;\r
 432             lo_tm, lo_var_real; df_lo, df_lo_var;\r
 433             w_tm, w_var_real; df_hi, df_hi_var; hi_tm, hi_var_real;\r
 434             f_tm, f_var_fun; x_tm, x_var_real; \r
 435             y_tm, y_var_real; z_tm, z_var_real]) TAYLOR_DF_BOUNDS';;\r
 436 \r
 437 \r
 438 (*\r
 439 let pp = 3;;\r
 440 let th = eval_taylor_atn pp domain_th;;\r
 441 eval_taylor_df_bounds pp th;;\r
 442 *)\r
 443 \r
 444 (**************************************************)\r
 445 (* mk_taylor_interval_th, dest_taylor_interval_th *)\r
 446 \r
 447 let TAYLOR_INTERVAL_EQ' = (RULE o prove)(`taylor_interval f x y z w f_bounds df_bounds dd_bounds <=>\r
 448                                              cell_domain x y z w /\ lin_approx f y f_bounds df_bounds /\\r
 449                                              has_bounded_second_derivative f (x,z) dd_bounds`,\r
 450                                            SIMP_TAC[cell_domain; taylor_interval; CONJ_ACI]);;\r
 451 \r
 452 let MK_TAYLOR_INTERVAL' = (RULE o prove)(`cell_domain x y z w /\ \r
 453                                           lin_approx f y f_bounds df_bounds /\\r
 454                                           has_bounded_second_derivative f (x,z) dd_bounds ==>\r
 455                                           taylor_interval f x y z w f_bounds df_bounds dd_bounds`,\r
 456                                         SIMP_TAC[cell_domain; taylor_interval]);;\r
 457 \r
 458 \r
 459 let dest_taylor_interval_th th =\r
 460   let f_tm, x_tm, y_tm, z_tm, w_tm, f_bounds, df_bounds, dd_bounds = dest_taylor_interval (concl th) in\r
 461   let th0 = INST[f_tm, f_var_fun; x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;\r
 462                  w_tm, w_var_real; f_bounds, f_bounds_var;\r
 463                  df_bounds, df_bounds_var; dd_bounds, dd_bounds_var] TAYLOR_INTERVAL_EQ' in\r
 464   let [domain; approx; second] = CONJUNCTS (EQ_MP th0 th) in\r
 465     domain, approx, second;;\r
 466 \r
 467 \r
 468 \r
 469 let mk_taylor_interval_th domain_th approx_th second_th =\r
 470   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) in\r
 471   let f_tm, _, f_bounds, df_bounds = dest_lin_approx (concl approx_th) in\r
 472   let dd_bounds = rand (concl second_th) in\r
 473   let th0 = INST[f_tm, f_var_fun; x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real;\r
 474                  w_tm, w_var_real; f_bounds, f_bounds_var;\r
 475                  df_bounds, df_bounds_var; dd_bounds, dd_bounds_var] MK_TAYLOR_INTERVAL' in\r
 476     (MY_PROVE_HYP approx_th o MY_PROVE_HYP domain_th o MY_PROVE_HYP second_th) th0;;\r
 477   \r
 478 \r
 479 \r
 480 (*\r
 481 let th = eval_taylor_atn 5 domain_th;;\r
 482 let domain_th, approx_th, second_th = dest_taylor_interval_th th;;\r
 483 mk_taylor_interval_th domain_th approx_th second_th;;\r
 484 *)\r
 485 \r
 486 \r
 487 (**************************************)\r
 488 (* has_bounded_second_derivative_dest *)\r
 489 \r
 490 let HAS_BOUNDED_SECOND_DERIVATIVE_EQ' = SPEC_ALL has_bounded_second_derivative;;\r
 491 \r
 492 \r
 493 let dest_has_bounded_second_derivative tm =\r
 494   let lhs, dd_bounds = dest_comb tm in\r
 495   let lhs2, int_tm = dest_comb lhs in\r
 496     rand lhs2, int_tm, dd_bounds;;\r
 497 \r
 498 \r
 499 let dest_has_bounded_second_derivative_th th =\r
 500   let f_tm, int_tm, dd_bounds = dest_has_bounded_second_derivative (concl th) in\r
 501   let th0 = INST[f_tm, f_var_fun; int_tm, int_var; \r
 502                  dd_bounds, dd_bounds_var] HAS_BOUNDED_SECOND_DERIVATIVE_EQ' in\r
 503   let [diff_th; bounded_th] = CONJUNCTS (EQ_MP th0 th) in\r
 504     diff_th, bounded_th;;\r
 505 \r
 506 \r
 507 (*\r
 508 let diff_th, bounded_th = dest_has_bounded_second_derivative_th second_th;;\r
 509 *)\r
 510 \r
 511 (********************************************)\r
 512 \r
 513 \r
 514 (******************************)\r
 515 (* Taylor interval arithmetic *)\r
 516 (******************************)\r
 517 \r
 518 \r
 519 (**************************************)\r
 520 let taylor_interval_tm = `taylor_interval`;;\r
 521 \r
 522 let taylor_interval_norm th eq_th =\r
 523   let lhs1, d2f = dest_comb (concl th) in\r
 524   let lhs2, d1f = dest_comb lhs1 in\r
 525   let lhs3, d0f = dest_comb lhs2 in\r
 526   let lhs4, w = dest_comb lhs3 in\r
 527   let lhs5, z = dest_comb lhs4 in\r
 528   let lhs6, y = dest_comb lhs5 in\r
 529   let x = rand lhs6 in\r
 530   let th0 = AP_TERM taylor_interval_tm eq_th in\r
 531   let th1 = (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM (AP_THM th0 x) y) z) w) d0f) d1f) d2f) in\r
 532     EQ_MP th1 th;;\r
 533 \r
 534 \r
 535 (*************************************)\r
 536 (* taylor_interval_neg *)\r
 537 let TAYLOR_INTERVAL_NEG' = (UNDISCH_ALL o prove)\r
 538   (`cell_domain x y z w ==>\r
 539      lin_approx (\x. -- (f x)) y bounds d_bounds ==>\r
 540      nth_diff_strong_int 2 (x,z) f ==>\r
 541      bounded_on_int (\x. -- nth_derivative 2 f x) (x,z) dd_bounds ==>\r
 542      taylor_interval (\x. -- (f x)) x y z w bounds d_bounds dd_bounds`,\r
 543    SIMP_TAC[taylor_interval; cell_domain] THEN ONCE_REWRITE_TAC[REAL_ARITH `--a = (-- (&1)) * a`] THEN\r
 544      REPEAT STRIP_TAC THEN\r
 545      ASM_SIMP_TAC[second_derivative_scale_bounds]);;\r
 546 \r
 547 \r
 548 let taylor_interval_neg th1 =\r
 549   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in\r
 550   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in\r
 551 \r
 552   let approx_th = lin_approx_neg approx1_th in\r
 553   let dd_th = bounded_on_int_neg dd1_th in\r
 554 \r
 555   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 556       f_tm = (rand o concl) diff1_th and\r
 557       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 558       dd_bounds = (rand o concl) dd_th in\r
 559 \r
 560   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 561                MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o\r
 562                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 563                     f_tm, f_var_fun;\r
 564                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 565     TAYLOR_INTERVAL_NEG' in\r
 566   let eq_th = unary_beta_eq f_tm neg_op_real in\r
 567     taylor_interval_norm th0 eq_th;;\r
 568      \r
 569 \r
 570 (*\r
 571 let th1 = eval_taylor_x domain_th and\r
 572     th2 = eval_taylor_sqrt pp domain_th;;\r
 573 taylor_interval_neg th1;;\r
 574 taylor_interval_neg th2;;\r
 575 *)\r
 576 \r
 577 \r
 578 \r
 579 (*************************************)\r
 580 (* taylor_interval_add *)\r
 581 \r
 582 let TAYLOR_INTERVAL_ADD' = (UNDISCH_ALL o prove)\r
 583   (`cell_domain x y z w ==>\r
 584      lin_approx (\x. f x + g x) y bounds d_bounds ==>\r
 585      nth_diff_strong_int 2 (x,z) f ==>\r
 586      nth_diff_strong_int 2 (x,z) g ==>\r
 587      bounded_on_int (\x. nth_derivative 2 f x + nth_derivative 2 g x) (x,z) dd_bounds ==>\r
 588      taylor_interval (\x. f x + g x) x y z w bounds d_bounds dd_bounds`,\r
 589    SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 590      ASM_SIMP_TAC[second_derivative_add_bounds]);;\r
 591 \r
 592 \r
 593 let taylor_interval_add pp th1 th2 =\r
 594   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and\r
 595       _, approx2_th, second2_th = dest_taylor_interval_th th2 in\r
 596   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and\r
 597       diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in\r
 598 \r
 599   let approx_th = lin_approx_add pp approx1_th approx2_th in\r
 600   let dd_th = \r
 601     let (+) = bounded_on_int_add pp in\r
 602       dd1_th + dd2_th in\r
 603 \r
 604   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 605       f_tm = (rand o concl) diff1_th and\r
 606       g_tm = (rand o concl) diff2_th and\r
 607       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 608       dd_bounds = (rand o concl) dd_th in\r
 609 \r
 610   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 611                MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o\r
 612                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 613                     f_tm, f_var_fun; g_tm, g_var_fun;\r
 614                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 615     TAYLOR_INTERVAL_ADD' in\r
 616   let eq_th = binary_beta_eq f_tm g_tm add_op_real in\r
 617     taylor_interval_norm th0 eq_th;;\r
 618 \r
 619 \r
 620 \r
 621 (*\r
 622 let th1 = eval_taylor_x domain_th and\r
 623     th2 = eval_taylor_sqrt pp domain_th;;\r
 624 taylor_interval_add pp th1 th2;;\r
 625 *)\r
 626 \r
 627 \r
 628 (*************************************)\r
 629 (* taylor_interval_sub *)\r
 630 \r
 631 let TAYLOR_INTERVAL_SUB' = (UNDISCH_ALL o prove)\r
 632   (`cell_domain x y z w ==>\r
 633      lin_approx (\x. f x - g x) y bounds d_bounds ==>\r
 634      nth_diff_strong_int 2 (x,z) f ==>\r
 635      nth_diff_strong_int 2 (x,z) g ==>\r
 636      bounded_on_int (\x. nth_derivative 2 f x - nth_derivative 2 g x) (x,z) dd_bounds ==>\r
 637      taylor_interval (\x. f x - g x) x y z w bounds d_bounds dd_bounds`,\r
 638    SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 639      ASM_SIMP_TAC[second_derivative_sub_bounds]);;\r
 640 \r
 641 \r
 642 let taylor_interval_sub pp th1 th2 =\r
 643   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and\r
 644       _, approx2_th, second2_th = dest_taylor_interval_th th2 in\r
 645   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and\r
 646       diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in\r
 647 \r
 648   let approx_th = lin_approx_sub pp approx1_th approx2_th in\r
 649   let dd_th = \r
 650     let (-) = bounded_on_int_sub pp in\r
 651       dd1_th - dd2_th in\r
 652 \r
 653   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 654       f_tm = (rand o concl) diff1_th and\r
 655       g_tm = (rand o concl) diff2_th and\r
 656       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 657       dd_bounds = (rand o concl) dd_th in\r
 658 \r
 659   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 660                MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o\r
 661                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 662                     f_tm, f_var_fun; g_tm, g_var_fun;\r
 663                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 664     TAYLOR_INTERVAL_SUB' in\r
 665   let eq_th = binary_beta_eq f_tm g_tm sub_op_real in\r
 666     taylor_interval_norm th0 eq_th;;\r
 667 \r
 668 \r
 669 \r
 670 (*\r
 671 let th1 = eval_taylor_x domain_th and\r
 672     th2 = eval_taylor_sqrt pp domain_th;;\r
 673 taylor_interval_sub pp th1 th2;;\r
 674 *)\r
 675 \r
 676 \r
 677 (*************************************)\r
 678 (* taylor_interval_mul *)\r
 679 \r
 680 let TAYLOR_INTERVAL_MUL' = (UNDISCH_ALL o prove)\r
 681   (`cell_domain x y z w ==>\r
 682      lin_approx (\x. f x * g x) y bounds d_bounds ==>\r
 683      nth_diff_strong_int 2 (x,z) f ==>\r
 684      nth_diff_strong_int 2 (x,z) g ==>\r
 685      bounded_on_int (\x. f x * nth_derivative 2 g x + &2 * derivative f x * derivative g x +\r
 686                      nth_derivative 2 f x * g x) (x,z) dd_bounds ==>\r
 687      taylor_interval (\x. f x * g x) x y z w bounds d_bounds dd_bounds`,\r
 688    SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 689      ASM_SIMP_TAC[second_derivative_mul_bounds]);;\r
 690 \r
 691 \r
 692 let taylor_interval_mul pp th1 th2 =\r
 693   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and\r
 694       _, approx2_th, second2_th = dest_taylor_interval_th th2 in\r
 695   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and\r
 696       diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in\r
 697 \r
 698   let approx_th = lin_approx_mul pp approx1_th approx2_th in\r
 699   let dd_th =\r
 700     let dest = dest_bounded_on_int_raw in\r
 701     let f = (dest o eval_taylor_f_bounds pp) th1 and\r
 702         g = (dest o eval_taylor_f_bounds pp) th2 and\r
 703         df = (dest o eval_taylor_df_bounds pp) th1 and\r
 704         dg = (dest o eval_taylor_df_bounds pp) th2 and\r
 705         ddf = dest dd1_th and\r
 706         ddg = dest dd2_th and\r
 707         (+) = float_interval_add pp and\r
 708         ( * ) = float_interval_mul pp in\r
 709       mk_bounded_on_int (f * ddg + (two_interval * (df * dg) + ddf * g)) in\r
 710 \r
 711   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 712       f_tm = (rand o concl) diff1_th and\r
 713       g_tm = (rand o concl) diff2_th and\r
 714       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 715       dd_bounds = (rand o concl) dd_th in\r
 716 \r
 717   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 718                MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o\r
 719                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 720                     f_tm, f_var_fun; g_tm, g_var_fun;\r
 721                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 722     TAYLOR_INTERVAL_MUL' in\r
 723   let eq_th = binary_beta_eq f_tm g_tm mul_op_real in\r
 724     taylor_interval_norm th0 eq_th;;\r
 725 \r
 726 \r
 727 \r
 728 (*\r
 729 let th1 = eval_taylor_x domain_th and\r
 730     th2 = eval_taylor_sqrt pp domain_th;;\r
 731 let th3 = taylor_interval_sub pp th1 th2;;\r
 732 taylor_interval_mul pp th1 th3;;\r
 733 *)\r
 734 \r
 735 \r
 736 \r
 737 (*************************************)\r
 738 (* taylor_interval_div *)\r
 739 \r
 740 let TAYLOR_INTERVAL_DIV' = (UNDISCH_ALL o prove)\r
 741  (`cell_domain x y z w ==>\r
 742     bounded_on_int g (x,z) g_bounds ==>\r
 743     interval_not_zero g_bounds ==>\r
 744     lin_approx (\x. f x / g x) y bounds d_bounds ==>\r
 745     nth_diff_strong_int 2 (x,z) f ==>\r
 746     nth_diff_strong_int 2 (x,z) g ==>\r
 747     bounded_on_int (\x. ((nth_derivative 2 f x * g x - f x * nth_derivative 2 g x) * g x -\r
 748                          &2 * derivative g x * (derivative f x * g x - f x * derivative g x)) / \r
 749                       (g x * g x * g x)) (x,z) dd_bounds ==>\r
 750     taylor_interval (\x. f x / g x) x y z w bounds d_bounds dd_bounds`,\r
 751   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 752     MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_div_bounds) THEN\r
 753     ASM_REWRITE_TAC[REAL_ARITH `g x pow 3 = g x * g x * (g:real->real) x`]);;\r
 754 \r
 755 \r
 756 let taylor_interval_div pp th1 th2 =\r
 757   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 and\r
 758       _, approx2_th, second2_th = dest_taylor_interval_th th2 in\r
 759   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th and\r
 760       diff2_th, dd2_th = dest_has_bounded_second_derivative_th second2_th in\r
 761 \r
 762   let g_bounds_th = eval_taylor_f_bounds pp th2 and\r
 763       approx_th = lin_approx_div pp approx1_th approx2_th in\r
 764   let g_bounds = (rand o concl) g_bounds_th in\r
 765   let cond_th = check_interval_not_zero g_bounds in\r
 766 \r
 767   let dd_th =\r
 768     let dest = dest_bounded_on_int_raw in\r
 769     let f = (dest o eval_taylor_f_bounds pp) th1 and\r
 770         g = dest g_bounds_th and\r
 771         df = (dest o eval_taylor_df_bounds pp) th1 and\r
 772         dg = (dest o eval_taylor_df_bounds pp) th2 and\r
 773         ddf = dest dd1_th and\r
 774         ddg = dest dd2_th and\r
 775         (-) = float_interval_sub pp and\r
 776         ( * ) = float_interval_mul pp and\r
 777         (/) = float_interval_div pp in\r
 778       mk_bounded_on_int (((ddf * g - f * ddg) * g - two_interval * (dg * (df * g - f * dg))) / (g * (g * g))) in\r
 779 \r
 780   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 781       f_tm = (rand o concl) diff1_th and\r
 782       g_tm = (rand o concl) diff2_th and\r
 783       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 784       dd_bounds = (rand o concl) dd_th in\r
 785 \r
 786   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 787                MY_PROVE_HYP g_bounds_th o MY_PROVE_HYP cond_th o\r
 788                MY_PROVE_HYP diff1_th o MY_PROVE_HYP diff2_th o MY_PROVE_HYP dd_th o\r
 789                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 790                     f_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var;\r
 791                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 792     TAYLOR_INTERVAL_DIV' in\r
 793   let eq_th = binary_beta_eq f_tm g_tm div_op_real in\r
 794     taylor_interval_norm th0 eq_th;;\r
 795 \r
 796 \r
 797 (*\r
 798 let pp = 5;;\r
 799 let domain_th = mk_center_domain pp one_float two_float;;\r
 800 let th1 = eval_taylor_x domain_th and\r
 801     th2 = eval_taylor_sqrt pp domain_th;;\r
 802 let th3 = taylor_interval_sub pp th1 th2;;\r
 803 taylor_interval_div pp th1 th2;;\r
 804 taylor_interval_div pp th3 th2;;\r
 805 (* 10: 3.372 *)\r
 806 test 100 (taylor_interval_div pp th1) th2;;\r
 807 *)\r
 808 \r
 809 \r
 810 (*************************************)\r
 811 (* taylor_interval_atn *)\r
 812 \r
 813 let TAYLOR_INTERVAL_ATN' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2] o prove)\r
 814  (`cell_domain x y z w ==>\r
 815     lin_approx (\x. atn (f x)) y bounds d_bounds ==>\r
 816     nth_diff_strong_int 2 (x,z) f ==>\r
 817     bounded_on_int (\x. (nth_derivative 2 f x * (&1 + f x * f x) - &2 * f x * derivative f x pow 2) /\r
 818                       (&1 + f x * f x) pow 2) (x,z) dd_bounds ==>\r
 819     taylor_interval (\x. atn (f x)) x y z w bounds d_bounds dd_bounds`,\r
 820   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 821     MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_atn_bounds) THEN\r
 822     ASM_REWRITE_TAC[]);;\r
 823 \r
 824 \r
 825 let taylor_interval_atn pp th1 =\r
 826   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in\r
 827   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in\r
 828 \r
 829   let approx_th = lin_approx_atn pp approx1_th in\r
 830   let dd_th =\r
 831     let dest = dest_bounded_on_int_raw in\r
 832     let f = (dest o eval_taylor_f_bounds pp) th1 and\r
 833         df = (dest o eval_taylor_df_bounds pp) th1 and\r
 834         ddf = dest dd1_th and\r
 835         (+) = float_interval_add pp and\r
 836         (-) = float_interval_sub pp and\r
 837         ( * ) = float_interval_mul pp and\r
 838         (/) = float_interval_div pp in\r
 839     let ff1 = one_interval + f * f in\r
 840       mk_bounded_on_int ((ddf * ff1 - two_interval * (f * (df * df))) / (ff1 * ff1)) in\r
 841 \r
 842   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 843       f_tm = (rand o concl) diff1_th and\r
 844       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 845       dd_bounds = (rand o concl) dd_th in\r
 846 \r
 847   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 848                MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o\r
 849                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 850                     f_tm, f_var_fun;\r
 851                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 852     TAYLOR_INTERVAL_ATN' in\r
 853   let eq_th = unary_beta_eq f_tm atn_tm in\r
 854     taylor_interval_norm th0 eq_th;;\r
 855 \r
 856 \r
 857 (*\r
 858 let pp = 5;;\r
 859 let domain_th = mk_center_domain pp one_float two_float;;\r
 860 let th1 = eval_taylor_x domain_th and\r
 861     th2 = eval_taylor_sqrt pp domain_th;;\r
 862 let th3 = taylor_interval_add pp th1 th2;;\r
 863 taylor_interval_atn pp th1;;\r
 864 taylor_interval_atn pp th2;;\r
 865 taylor_interval_atn pp th3;;\r
 866 *)\r
 867 \r
 868 \r
 869 \r
 870 \r
 871 (*************************************)\r
 872 (* taylor_interval_inv *)\r
 873 \r
 874 let TAYLOR_INTERVAL_INV' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)\r
 875  (`cell_domain x y z w ==>\r
 876     bounded_on_int f (x,z) f_bounds ==>\r
 877     interval_not_zero f_bounds ==>\r
 878     lin_approx (\x. inv (f x)) y bounds d_bounds ==>\r
 879     nth_diff_strong_int 2 (x,z) f ==>\r
 880     bounded_on_int (\x. (&2 * derivative f x pow 2 - nth_derivative 2 f x * f x) / (f x pow 3)) (x,z) dd_bounds\r
 881     ==> taylor_interval (\x. inv (f x)) x y z w bounds d_bounds dd_bounds`,\r
 882   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 883     MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_inv_bounds) THEN\r
 884     ASM_REWRITE_TAC[]);;\r
 885 \r
 886 \r
 887 let taylor_interval_inv pp th1 =\r
 888   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in\r
 889   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in\r
 890 \r
 891   let f_bounds_th = eval_taylor_f_bounds pp th1 and\r
 892       approx_th = lin_approx_inv pp approx1_th in\r
 893   let f_bounds = (rand o concl) f_bounds_th in\r
 894   let cond_th = check_interval_not_zero f_bounds in\r
 895 \r
 896   let dd_th =\r
 897     let dest = dest_bounded_on_int_raw in\r
 898     let f = dest f_bounds_th and\r
 899         df = (dest o eval_taylor_df_bounds pp) th1 and\r
 900         ddf = dest dd1_th and\r
 901         (-) = float_interval_sub pp and\r
 902         ( * ) = float_interval_mul pp and\r
 903         (/) = float_interval_div pp in\r
 904       mk_bounded_on_int ((two_interval * (df * df) - ddf * f) / (f * (f * f))) in\r
 905 \r
 906   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 907       f_tm = (rand o concl) diff1_th and\r
 908       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 909       dd_bounds = (rand o concl) dd_th in\r
 910 \r
 911   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 912                MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o\r
 913                MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o\r
 914                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 915                     f_tm, f_var_fun; f_bounds, f_bounds_var;\r
 916                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 917     TAYLOR_INTERVAL_INV' in\r
 918   let eq_th = unary_beta_eq f_tm inv_tm in\r
 919     taylor_interval_norm th0 eq_th;;\r
 920 \r
 921 \r
 922 (*\r
 923 let pp = 5;;\r
 924 let domain_th = mk_center_domain pp one_float two_float;;\r
 925 let th1 = eval_taylor_x domain_th and\r
 926     th2 = eval_taylor_sqrt pp domain_th;;\r
 927 let th3 = taylor_interval_add pp th1 th2;;\r
 928 taylor_interval_inv pp th1;;\r
 929 taylor_interval_inv pp th2;;\r
 930 taylor_interval_inv pp th3;;\r
 931 *)\r
 932 \r
 933 \r
 934 \r
 935 (*************************************)\r
 936 (* taylor_interval_sqrt *)\r
 937 \r
 938 let TAYLOR_INTERVAL_SQRT' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)\r
 939  (`cell_domain x y z w ==>\r
 940     bounded_on_int f (x,z) f_bounds ==>\r
 941     interval_pos f_bounds ==>\r
 942     lin_approx (\x. sqrt (f x)) y bounds d_bounds ==>\r
 943     nth_diff_strong_int 2 (x,z) f ==>\r
 944     bounded_on_int (\x. (&2 * nth_derivative 2 f x * f x - derivative f x pow 2) /\r
 945                       (&4 * sqrt (f x pow 3))) (x,z) dd_bounds ==>\r
 946     taylor_interval (\x. sqrt (f x)) x y z w bounds d_bounds dd_bounds`,\r
 947   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
 948     MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_sqrt_bounds) THEN\r
 949     ASM_REWRITE_TAC[]);;\r
 950 \r
 951 \r
 952 let taylor_interval_sqrt pp th1 =\r
 953   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in\r
 954   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in\r
 955 \r
 956   let f_bounds_th = eval_taylor_f_bounds pp th1 and\r
 957       approx_th = lin_approx_sqrt pp approx1_th in\r
 958   let f_bounds = (rand o concl) f_bounds_th in\r
 959   let cond_th = check_interval_pos f_bounds in\r
 960 \r
 961   let dd_th =\r
 962     let dest = dest_bounded_on_int_raw in\r
 963     let f = dest f_bounds_th and\r
 964         df = (dest o eval_taylor_df_bounds pp) th1 and\r
 965         ddf = dest dd1_th and\r
 966         (-) = float_interval_sub pp and\r
 967         ( * ) = float_interval_mul pp and\r
 968         (/) = float_interval_div pp and\r
 969         sqrt = float_interval_sqrt pp in\r
 970       mk_bounded_on_int ((two_interval * (ddf * f) - df * df) / (four_interval * sqrt (f * (f * f)))) in\r
 971 \r
 972   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
 973       f_tm = (rand o concl) diff1_th and\r
 974       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
 975       dd_bounds = (rand o concl) dd_th in\r
 976 \r
 977   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
 978                MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o\r
 979                MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o\r
 980                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
 981                     f_tm, f_var_fun; f_bounds, f_bounds_var;\r
 982                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
 983     TAYLOR_INTERVAL_SQRT' in\r
 984   let eq_th = unary_beta_eq f_tm sqrt_tm in\r
 985     taylor_interval_norm th0 eq_th;;\r
 986 \r
 987 \r
 988 (*\r
 989 let pp = 5;;\r
 990 let domain_th = mk_center_domain pp one_float two_float;;\r
 991 let th1 = eval_taylor_x domain_th and\r
 992     th2 = eval_taylor_sqrt pp domain_th;;\r
 993 let th3 = taylor_interval_add pp th1 th2;;\r
 994 taylor_interval_sqrt pp th1;;\r
 995 taylor_interval_sqrt pp th2;;\r
 996 taylor_interval_sqrt pp th3;;\r
 997 *)\r
 998 \r
 999 \r
1000 (*************************************)\r
1001 (* taylor_interval_acs *)\r
1002 \r
1003 let TAYLOR_INTERVAL_ACS' = \r
1004   (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[iabs_lt1_lemma] o\r
1005      REWRITE_RULE[REAL_POW_2; REAL_ARITH `a pow 3 = a * a * a`] o prove)\r
1006  (`cell_domain x y z w ==>\r
1007     bounded_on_int f (x,z) f_bounds ==>\r
1008     (iabs f_bounds < &1 <=> T)==>\r
1009     lin_approx (\x. acs (f x)) y bounds d_bounds ==>\r
1010     nth_diff_strong_int 2 (x,z) f ==>\r
1011     bounded_on_int (\x. --((nth_derivative 2 f x * (&1 - f x * f x) + f x * derivative f x pow 2) /\r
1012                              sqrt ((&1 - f x * f x) pow 3))) (x,z) dd_bounds ==>\r
1013     taylor_interval (\x. acs (f x)) x y z w bounds d_bounds dd_bounds`,\r
1014   SIMP_TAC[taylor_interval; cell_domain] THEN REPEAT STRIP_TAC THEN\r
1015     MATCH_MP_TAC ((SPEC_ALL o REWRITE_RULE[IMP_IMP]) second_derivative_compose_acs_bounds) THEN\r
1016     ASM_REWRITE_TAC[]);;\r
1017 \r
1018 \r
1019 let taylor_interval_acs pp th1 =\r
1020   let domain_th, approx1_th, second1_th = dest_taylor_interval_th th1 in\r
1021   let diff1_th, dd1_th = dest_has_bounded_second_derivative_th second1_th in\r
1022 \r
1023   let f_bounds_th = eval_taylor_f_bounds pp th1 and\r
1024       approx_th = lin_approx_acs pp approx1_th in\r
1025   let f_bounds = (rand o concl) f_bounds_th in\r
1026   let cond_th = check_interval_iabs f_bounds one_float in\r
1027 \r
1028   let dd_th =\r
1029     let dest = dest_bounded_on_int_raw in\r
1030     let f = dest f_bounds_th and\r
1031         df = (dest o eval_taylor_df_bounds pp) th1 and\r
1032         ddf = dest dd1_th and\r
1033         (+) = float_interval_add pp and\r
1034         (-) = float_interval_sub pp and\r
1035         ( * ) = float_interval_mul pp and\r
1036         (/) = float_interval_div pp and\r
1037         sqrt = float_interval_sqrt pp and\r
1038         neg = float_interval_neg in\r
1039     let ff1 = one_interval - f * f in\r
1040       mk_bounded_on_int (neg ((ddf * ff1 + f * (df * df)) / sqrt (ff1 * (ff1 * ff1)))) in\r
1041 \r
1042   let x_tm, y_tm, z_tm, w_tm = dest_cell_domain (concl domain_th) and\r
1043       f_tm = (rand o concl) diff1_th and\r
1044       _, _, bounds, d_bounds = dest_lin_approx (concl approx_th) and\r
1045       dd_bounds = (rand o concl) dd_th in\r
1046 \r
1047   let th0 = (MY_PROVE_HYP domain_th o MY_PROVE_HYP approx_th o \r
1048                MY_PROVE_HYP f_bounds_th o MY_PROVE_HYP cond_th o\r
1049                MY_PROVE_HYP diff1_th o MY_PROVE_HYP dd_th o\r
1050                INST[x_tm, x_var_real; y_tm, y_var_real; z_tm, z_var_real; w_tm, w_var_real;\r
1051                     f_tm, f_var_fun; f_bounds, f_bounds_var;\r
1052                     bounds, bounds_var; d_bounds, d_bounds_var; dd_bounds, dd_bounds_var])\r
1053     TAYLOR_INTERVAL_ACS' in\r
1054   let eq_th = unary_beta_eq f_tm acs_tm in\r
1055     taylor_interval_norm th0 eq_th;;\r
1056 \r
1057 \r
1058 (*\r
1059 let pp = 5;;\r
1060 let domain_th = mk_center_domain pp (mk_float (-5) 49) (mk_float 3 49);;\r
1061 let th1 = eval_taylor_x domain_th and\r
1062     th2 = eval_taylor_atn pp domain_th;;\r
1063 let th3 = taylor_interval_mul pp th1 th2;;\r
1064 \r
1065 taylor_interval_acs pp th1;;\r
1066 taylor_interval_acs pp th2;;\r
1067 taylor_interval_acs pp th3;;\r
1068 *)\r
1069 \r
1070 \r
1071 \r
1072 \r
1073 \r
1074 \r
1075 \r
1076 (****************************************)\r
1077 (* Composition *)\r
1078 \r
1079 let dest_bounded_on_int_tm tm =\r
1080   let lhs, f_bounds = dest_comb tm in\r
1081   let lhs2, int_tm = dest_comb lhs in\r
1082     rand lhs2, int_tm, f_bounds;;\r
1083 \r
1084 let dest_interval_arith tm =\r
1085   let lhs, int_tm = dest_comb tm in\r
1086     rand lhs, int_tm;;\r
1087 \r
1088 \r
1089 let BOUNDED_SECOND_DERIVATIVE_COMPOSE' = (UNDISCH_ALL o REWRITE_RULE[REAL_POW_2] o SPEC_ALL) \r
1090   second_derivative_compose_bounds;;\r
1091 \r
1092 let BOUNDED_ON_INT_COMPOSE' = (UNDISCH_ALL o SPEC_ALL) bounded_on_int_compose;;\r
1093 \r
1094 let TAYLOR_INTERVAL_NARROW' = (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[REAL_ARITH `a <= b <=> (a <= b <=> T)`] o\r
1095                                  SPEC_ALL) taylor_interval_narrow;;\r
1096 \r
1097 let BOUNDED_ON_INT_IMP_INTERVAL' = (UNDISCH_ALL o SPEC_ALL) bounded_on_int_imp_interval_arith;;\r
1098 \r
1099 let LIN_APPROX_COMPOSE' = (UNDISCH_ALL o SPEC_ALL) lin_approx_compose;;\r
1100 \r
1101 \r
1102 \r
1103 let taylor_interval_compose pp eval_f eval_g domain_th =\r
1104   let g_taylor = eval_g pp domain_th in\r
1105   let _, lin_g, second_g =  dest_taylor_interval_th g_taylor in\r
1106   let dg_th, g2_th = dest_has_bounded_second_derivative_th second_g in\r
1107   let g0_th = eval_taylor_f_bounds pp g_taylor in\r
1108   let g1_th = eval_taylor_df_bounds pp g_taylor in\r
1109   let g_tm, y_tm, g_bounds0, _ = dest_lin_approx (concl lin_g) in\r
1110 \r
1111   (* narrow domain *)\r
1112   let g0_lo, g0_hi = dest_pair g_bounds0 in\r
1113   let fu_domain = mk_center_domain (pp + 1) g0_lo g0_hi in\r
1114   let w0_tm = (rand o concl) fu_domain in\r
1115 \r
1116   (* wide domain *)\r
1117   let _, u_tm, _, _ = dest_cell_domain (concl fu_domain) in\r
1118   let g_lo, g_hi = (dest_pair o rand o concl) g0_th in\r
1119   let fw_domain = mk_cell_domain pp g_lo u_tm g_hi in\r
1120   let w_tm = (rand o concl) fw_domain in\r
1121 \r
1122   (* taylor_interval f *)\r
1123   let f_taylor = eval_f pp fw_domain in\r
1124   let f1_th = eval_taylor_df_bounds pp f_taylor in\r
1125   let _, lin_f, second_f = dest_taylor_interval_th f_taylor in\r
1126   let f_tm, _, f_bounds0, df_bounds0 = dest_lin_approx (concl lin_f) in\r
1127   let df_th, f2_th = dest_has_bounded_second_derivative_th second_f in\r
1128 \r
1129   (* has_bounded_second_derivative (\x. f (g x)) *)\r
1130   let _, int_tm, g_bounds = dest_bounded_on_int_tm (concl g0_th) in\r
1131   let df_tm, _, df_bounds = dest_bounded_on_int_tm (concl f1_th) in\r
1132   let ddf_tm, _, ddf_bounds = dest_bounded_on_int_tm (concl f2_th) in\r
1133 \r
1134   let f2_g_bounded_th = (MY_PROVE_HYP g0_th o MY_PROVE_HYP f2_th o\r
1135                            INST[ddf_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var; \r
1136                                 ddf_bounds, f_bounds_var; int_tm, int_var]) BOUNDED_ON_INT_COMPOSE' in\r
1137   let f1_g_bounded_th = (MY_PROVE_HYP g0_th o MY_PROVE_HYP f1_th o\r
1138                            INST[df_tm, f_var_fun; g_tm, g_var_fun; g_bounds, g_bounds_var;\r
1139                                 df_bounds, f_bounds_var; int_tm, int_var]) BOUNDED_ON_INT_COMPOSE' in\r
1140 \r
1141   let fg2_bounded_th0 = \r
1142     let ( * ) = bounded_on_int_mul pp and\r
1143         (+) = bounded_on_int_add pp in\r
1144       (f2_g_bounded_th * (g1_th * g1_th) + f1_g_bounded_th * g2_th) in\r
1145 \r
1146   let dd_bounds = (rand o concl) fg2_bounded_th0 in\r
1147   let fg2_bounded_th = (MY_PROVE_HYP fg2_bounded_th0 o MY_PROVE_HYP g0_th o \r
1148                           MY_PROVE_HYP dg_th o MY_PROVE_HYP df_th o\r
1149                           INST[f_tm, f_var_fun; g_tm, g_var_fun; int_tm, int_var; \r
1150                                dd_bounds, dd_bounds_var; g_bounds, g_bounds_var]) \r
1151     BOUNDED_SECOND_DERIVATIVE_COMPOSE' in\r
1152 \r
1153   (* lin_approx (\x. f (g x)) *)\r
1154   let fu_taylor = (MY_PROVE_HYP (float_le g_lo g0_lo) o MY_PROVE_HYP (float_le g0_hi g_hi) o\r
1155                      MY_PROVE_HYP fu_domain o MY_PROVE_HYP f_taylor o\r
1156                      INST[g0_lo, x0_var_real; u_tm, y_var_real; g0_hi, z0_var_real; w0_tm, w0_var_real;\r
1157                           f_tm, f_var_fun; g_lo, x_var_real; g_hi, z_var_real; w_tm, w_var_real;\r
1158                           f_bounds0, f_bounds_var; df_bounds0, df_bounds_var; ddf_bounds, dd_bounds_var])\r
1159     TAYLOR_INTERVAL_NARROW' in\r
1160 \r
1161   let df0_th = \r
1162     let _, _, f_second = dest_taylor_interval_th fu_taylor in\r
1163       (fst o dest_has_bounded_second_derivative_th) f_second in\r
1164   let f00_th = eval_taylor_f_bounds pp fu_taylor in\r
1165   let f01_th = eval_taylor_df_bounds pp fu_taylor in\r
1166   let fg_bounds0 = (rand o concl) f00_th in\r
1167   let dfg_bounds0 = (rand o concl) f01_th in\r
1168 \r
1169   let dg0_th, int_g_th, int_dg_th = lin_approx_components lin_g in\r
1170   let gy_tm, _ = dest_interval_arith (concl int_g_th) in\r
1171 \r
1172   let int_df_g_th = (MY_PROVE_HYP int_g_th o MY_PROVE_HYP f01_th o\r
1173                        INST[df_tm, f_var_fun; gy_tm, y_var_real; g_bounds0, int_var; dfg_bounds0, f_bounds_var])\r
1174     BOUNDED_ON_INT_IMP_INTERVAL' in\r
1175 \r
1176   let int_dfg_th = float_interval_mul pp int_dg_th int_df_g_th in\r
1177   let dfg_bounds00 = rand (concl int_dfg_th) in\r
1178 \r
1179   let fg_lin_th = (MY_PROVE_HYP int_dfg_th o MY_PROVE_HYP int_g_th o MY_PROVE_HYP f00_th o \r
1180                      MY_PROVE_HYP dg0_th o MY_PROVE_HYP df0_th o\r
1181                      INST[f_tm, f_var_fun; g_tm, g_var_fun; y_tm, y_var_real; dfg_bounds00, d_bounds_var;\r
1182                           g_bounds0, g_bounds_var; fg_bounds0, f_bounds_var]) LIN_APPROX_COMPOSE' in\r
1183 \r
1184   (* beta reduction *)\r
1185   let gx_tm = mk_comb (g_tm, x_var_real) in\r
1186   let gx_th = if is_abs g_tm then BETA gx_tm else REFL gx_tm in\r
1187 \r
1188   let fgx_th0 = MK_COMB (REFL f_tm, gx_th) in\r
1189   let fgx_eq_th = ABS x_var_real \r
1190     (if is_abs f_tm then TRANS fgx_th0 (BETA_CONV (rand (concl fgx_th0))) else fgx_th0) in\r
1191 \r
1192   let fg_lin_th1 = norm_lin_approx fg_lin_th fgx_eq_th and\r
1193       fg2_bounded_th1 = norm_second_derivative fg2_bounded_th fgx_eq_th in\r
1194 \r
1195     mk_taylor_interval_th domain_th fg_lin_th1 fg2_bounded_th1;;\r
1196 \r
1197 \r
1198 \r
1199 \r
1200 \r