formal_lp/old/formal_interval/more_float.hl

   1 needs "tame/ArcProperties.hl";;\r
   2 needs "../formal_lp/arith/float_atn.hl";;\r
   3 \r
   4 \r
   5 let REAL_LE_POW_2 = prove(`!x. &0 <= x pow 2`,\r
   6   REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;\r
   7 \r
   8 let REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT = \r
   9   prove(`!f s. real_open s ==>\r
  10           (f real_continuous_on s <=> (!x. x IN s ==> f real_continuous atreal x))`,\r
  11   REWRITE_TAC[REAL_OPEN; REAL_CONTINUOUS_ON; REAL_CONTINUOUS_CONTINUOUS_ATREAL] THEN\r
  12     REPEAT STRIP_TAC THEN\r
  13     MP_TAC (ISPECL[`lift o f o drop`; `IMAGE lift s`] CONTINUOUS_ON_EQ_CONTINUOUS_AT) THEN\r
  14     ASM_REWRITE_TAC[] THEN DISCH_THEN (fun th -> REWRITE_TAC[th; IN_IMAGE_LIFT_DROP]) THEN\r
  15     EQ_TAC THEN REPEAT STRIP_TAC THENL\r
  16     [\r
  17       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[LIFT_DROP];\r
  18       FIRST_X_ASSUM (MP_TAC o SPEC `drop x`) THEN ASM_REWRITE_TAC[LIFT_DROP]\r
  19     ]);;\r
  20                                         \r
  21 \r
  22 let ALL_EL = prove\r
  23  (`!P l. (!i. i < LENGTH l ==> P (EL i l)) <=> ALL P l`,\r
  24   REWRITE_TAC[GSYM ALL_MEM; MEM_EXISTS_EL] THEN MESON_TAC[]);;\r
  25 \r
  26 \r
  27 needs "../formal_lp/formal_interval/theory/taylor_interval.hl";;\r
  28 \r
  29 open Arith_misc;;\r
  30 open Float_theory;;\r
  31 open Interval_arith;;\r
  32 open Arith_float;;\r
  33 open Float_atn;;\r
  34 \r
  35 \r
  36 let RULE = UNDISCH_ALL o Arith_nat.NUMERALS_TO_NUM o REWRITE_RULE[FLOAT_OF_NUM; min_exp_def; GSYM IMP_IMP] o SPEC_ALL;;\r
  37 \r
  38 let x_var_real = `x:real` and\r
  39     y_var_real = `y:real` and\r
  40     w_var_real = `w:real` and\r
  41     f_var_fun = `f : real->real` and\r
  42     g_var_fun = `g : real->real` and\r
  43     f1_var_fun = `f1 : real->real` and\r
  44     f2_var_fun = `f2 : real->real` and\r
  45     int_var = `int : real#real` and\r
  46     f_bounds_var = `f_bounds : real#real` and\r
  47     df_bounds_var = `df_bounds : real#real` and\r
  48     dd_bounds_var = `dd_bounds : real#real` and\r
  49     x_lo_var = `x_lo : real` and\r
  50     x_hi_var = `x_hi : real` and\r
  51     dd_var_real = `dd : real` and\r
  52     df_lo_var = `df_lo : real` and\r
  53     df_hi_var = `df_hi : real` and\r
  54     df_var_real = `df : real` and\r
  55     f_lo_var = `f_lo : real` and\r
  56     f_hi_var = `f_hi : real` and\r
  57     s_var_bool = `s:bool` and\r
  58     n_var_num = `n:num` and\r
  59     e_var_num = `e:num`;;\r
  60 \r
  61 let add_op_real = `(+):real->real->real` and\r
  62     mul_op_real = `( * ):real->real->real` and\r
  63     sub_op_real = `(-):real->real->real` and\r
  64     div_op_real = `(/):real->real->real` and\r
  65     inv_op_real = `inv` and\r
  66     neg_op_real = `--` and\r
  67     eq_op_real = `(=):real->real->bool` and\r
  68     lt_op_real = `(<):real->real->bool`;;\r
  69 \r
  70 let w1_var_real = `w1 : real` and\r
  71     w2_var_real = `w2 : real` and\r
  72     t_var_real = `t : real` and\r
  73     g_bounds_var = `g_bounds : real#real` and\r
  74     dg_bounds_var = `dg_bounds : real#real` and\r
  75     bounds_var = `bounds : real#real` and\r
  76     d_bounds_var = `d_bounds : real#real` and\r
  77     x0_var_real = `x0 : real` and\r
  78     z0_var_real = `z0 : real` and\r
  79     w0_var_real = `w0 : real`;;\r
  80 \r
  81         \r
  82 (*************************************)\r
  83 (* More float *)\r
  84 \r
  85 \r
  86 (* Converts a float term to the corresponding rational number *)\r
  87 let num_of_float_tm tm =\r
  88   let s, n_tm, e_tm = dest_float tm in\r
  89   let b = Num.num_of_int Arith_options.base in\r
  90   let m = Num.num_of_int Arith_options.min_exp in\r
  91   let ( * ), (^), (-), (!) = ( */ ), ( **/ ), (-/), Arith_nat.raw_dest_hash in\r
  92   let r = !n_tm * (b ^ (!e_tm - m)) in\r
  93     if s = "T" then minus_num r else r;;\r
  94 \r
  95 \r
  96 let float_of_float_tm tm =\r
  97   float_of_num (num_of_float_tm tm);;\r
  98 \r
  99 \r
 100 \r
 101 let mk_float n e =\r
 102   let n, s = if n < 0 then -n, `T` else n, `F` in\r
 103   let n_tm = rand (Arith_nat.mk_small_numeral_array n) in\r
 104   let e_tm = rand (Arith_nat.mk_small_numeral_array e) in\r
 105     mk_comb(mk_comb(mk_comb (`float`, s), n_tm), e_tm);;\r
 106 \r
 107 \r
 108 let float0_eq = FLOAT_TO_NUM_CONV (mk_float 0 Arith_options.min_exp);;\r
 109 let float1_eq = FLOAT_TO_NUM_CONV (mk_float 1 Arith_options.min_exp);;\r
 110 let float2_eq = FLOAT_TO_NUM_CONV (mk_float 2 Arith_options.min_exp);;\r
 111 let float3_eq = FLOAT_TO_NUM_CONV (mk_float 3 Arith_options.min_exp);;\r
 112 let float4_eq = FLOAT_TO_NUM_CONV (mk_float 4 Arith_options.min_exp);;\r
 113 \r
 114 let num1_eq = (SYM o REWRITE_RULE[Arith_hash.NUM_THM] o Arith_nat.NUMERAL_TO_NUM_CONV) `1`;;\r
 115 let num2_eq = (SYM o REWRITE_RULE[Arith_hash.NUM_THM] o Arith_nat.NUMERAL_TO_NUM_CONV) `2`;;\r
 116 let num3_eq = (SYM o REWRITE_RULE[Arith_hash.NUM_THM] o Arith_nat.NUMERAL_TO_NUM_CONV) `3`;;\r
 117 \r
 118 (*********************)\r
 119 \r
 120 \r
 121 \r
 122 let interval_tm = `interval_arith`;;\r
 123 \r
 124 let mk_interval tm bounds =\r
 125   mk_comb(mk_comb(interval_tm, tm), bounds);;\r
 126   \r
 127 \r
 128 (* const interval *)\r
 129 \r
 130 let CONST_INTERVAL' = SPEC_ALL CONST_INTERVAL;;\r
 131 let mk_const_interval tm = INST[tm, x_var_real] CONST_INTERVAL';;\r
 132 \r
 133 let float_F_const = `float F`;;\r
 134 \r
 135 let mk_float_small n =\r
 136   let n_tm0 = mk_small_numeral n in\r
 137   let n_th = Arith_nat.NUMERAL_TO_NUM_CONV n_tm0 in\r
 138   let n_tm = rand(rand(concl n_th)) in\r
 139     mk_comb(mk_comb(float_F_const, n_tm), min_exp_num_const);;\r
 140 \r
 141 \r
 142 let one_float = mk_float_small 1;;\r
 143 let two_float = mk_float_small 2;;\r
 144 let one_interval = mk_float_interval_small_num 1;;\r
 145 let two_interval = mk_float_interval_small_num 2;;\r
 146 let neg_two_interval = float_interval_neg two_interval;;\r
 147 \r
 148 \r
 149 (***********************************)\r
 150 (* float_eq0 *)\r
 151 \r
 152 let FLOAT_EQ_0' = (GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [NUMERAL] o SPEC_ALL) \r
 153   FLOAT_EQ_0;;\r
 154 \r
 155 \r
 156 let float_eq0 f_tm =\r
 157   let lhs, e_tm = dest_comb f_tm in\r
 158   let lhs2, n_tm = dest_comb lhs in\r
 159   let th0 = INST[rand lhs2, s_var_bool; n_tm, n_var_num; e_tm, e_var_num] FLOAT_EQ_0' in\r
 160   let eq_th = Arith_nat.raw_eq0_hash_conv n_tm in\r
 161     TRANS th0 eq_th;;\r
 162 \r
 163 \r
 164 \r
 165 \r
 166 (***********************************)\r
 167 (* float_interval_scale *)\r
 168 \r
 169 let float_interval_scale pp c_tm th =\r
 170   let c_th = mk_const_interval c_tm in\r
 171     float_interval_mul pp c_th th;;\r
 172 \r
 173 \r
 174 (**********************************)\r
 175 (* float_pos *)\r
 176 \r
 177 let FLOAT_F_POS' = SPEC_ALL FLOAT_F_POS;;\r
 178 \r
 179 (* Returns &0 <= float F n e *)\r
 180 let float_pos tm =\r
 181   let _, n_tm, e_tm = dest_float tm in\r
 182     INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_F_POS';;\r
 183 \r
 184 \r
 185 \r
 186 (************************************)\r
 187 (* float_iabs *)\r
 188 \r
 189 let FLOAT_NEG_F' = (RULE) FLOAT_NEG_T;;\r
 190 let FLOAT_NEG_T' = (RULE) FLOAT_NEG_F;;\r
 191 \r
 192 let float_neg tm =\r
 193   let sign, n_tm, e_tm = dest_float tm in\r
 194     if sign = "T" then\r
 195       INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_T'\r
 196     else\r
 197       INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_F';;\r
 198 \r
 199 \r
 200 let IABS' = RULE iabs;;\r
 201 \r
 202 \r
 203 let float_iabs int_tm =\r
 204   let lo_tm, hi_tm = dest_pair int_tm in\r
 205   let neg_lo_th = float_neg lo_tm in\r
 206   let max_th = SYM (float_max hi_tm ((rand o rator o concl) neg_lo_th)) in\r
 207   let lhs, rhs = dest_comb (concl max_th) in\r
 208   let th0 = SYM (EQ_MP (AP_TERM lhs (AP_TERM (rator rhs) neg_lo_th)) max_th) in\r
 209   let th1 = INST[lo_tm, x_lo_var; hi_tm, x_hi_var] IABS' in\r
 210     TRANS th1 th0;;\r
 211 \r
 212 \r
 213 let FLOAT_IABS_FF = prove(`iabs (float F n1 e1, float F n2 e2) = float F n2 e2`,\r
 214   REWRITE_TAC[iabs] THEN\r
 215     MP_TAC (SPECL [`n1:num`; `e1:num`] FLOAT_F_POS) THEN\r
 216     MP_TAC (SPECL [`n2:num`; `e2:num`] FLOAT_F_POS) THEN\r
 217     REAL_ARITH_TAC);;\r
 218 \r
 219 \r
 220 let FLOAT_IABS_TT = prove(`iabs (float T n1 e1, float T n2 e2) = float F n1 e1`,\r
 221   REWRITE_TAC[iabs; GSYM FLOAT_NEG_F] THEN\r
 222     MP_TAC (SPECL [`n1:num`; `e1:num`] FLOAT_F_POS) THEN\r
 223     MP_TAC (SPECL [`n2:num`; `e2:num`] FLOAT_T_NEG) THEN\r
 224     REAL_ARITH_TAC);;\r
 225 \r
 226 (* let FLOAT_IABS_FT = prove(`iabs (float F n1 e1, float T n2 e2)  *)\r
 227 \r
 228 \r
 229 (****************************)\r
 230 (* interval_not_zero *)\r
 231 \r
 232 let INTERVAL_NOT_ZERO1' = (UNDISCH_ALL o prove)\r
 233   (`(&0 < lo <=> T) ==> interval_not_zero (lo, hi)`, SIMP_TAC[interval_not_zero]);;\r
 234 let INTERVAL_NOT_ZERO2' = (UNDISCH_ALL o prove)\r
 235   (`(hi < &0 <=> T) ==> interval_not_zero (lo, hi)`, SIMP_TAC[interval_not_zero]);;\r
 236 \r
 237 let lo_var_real = `lo:real` and\r
 238     hi_var_real = `hi:real`;;\r
 239 \r
 240 \r
 241 let check_interval_not_zero int_tm =\r
 242   let lo, hi = dest_pair int_tm in\r
 243   let inst = INST[lo, lo_var_real; hi, hi_var_real] in\r
 244   let s1, _, _ = dest_float lo in\r
 245     if s1 = "F" then\r
 246       let gt_th = float_gt0 lo in\r
 247         if (fst o dest_const o rand o concl) gt_th <> "T" then\r
 248           failwith "check_interval_not_zero: &0 < lo <=> F"\r
 249         else\r
 250           (MY_PROVE_HYP gt_th o inst) INTERVAL_NOT_ZERO1'\r
 251     else\r
 252       let lt_th = float_lt0 hi in\r
 253         if (fst o dest_const o rand o concl) lt_th <> "T" then\r
 254           failwith "check_interval_not_zero: hi < &0 <=> F"\r
 255         else\r
 256           (MY_PROVE_HYP lt_th o inst) INTERVAL_NOT_ZERO2';;\r
 257 \r
 258 \r
 259 \r
 260 (*\r
 261 let int1 = mk_pair (mk_float 3 50, mk_float 4 50);;\r
 262 let int2 = mk_pair (mk_float (-4) 50, mk_float (-3) 50);;\r
 263 \r
 264 check_interval_not_zero int1;;\r
 265 check_interval_not_zero int2;;\r
 266 *)\r
 267 \r
 268 (*************************************)\r
 269 (* interval_pos *)\r
 270 \r
 271 let INTERVAL_POS' = (UNDISCH_ALL o prove)\r
 272   (`(&0 < lo <=> T) ==> interval_pos (lo, hi:real)`, SIMP_TAC[interval_pos]);;\r
 273 \r
 274 \r
 275 let check_interval_pos int_tm =\r
 276   let lo, hi = dest_pair int_tm in\r
 277   let gt_th = float_gt0 lo in\r
 278     if (fst o dest_const o rand o concl) gt_th <> "T" then\r
 279       failwith "check_interval_pos: &0 < lo <=> F"\r
 280     else\r
 281       (MY_PROVE_HYP gt_th o INST[lo, lo_var_real; hi, hi_var_real]) INTERVAL_POS';;\r
 282 \r
 283 \r
 284 (*\r
 285 check_interval_pos int1;;\r
 286 check_interval_pos int2;;\r
 287 *)\r
 288 \r
 289 (************************************)\r
 290 (* check_interval_iabs *)\r
 291 \r
 292 \r
 293 (* proves iabs int < rhs *)\r
 294 let check_interval_iabs int_tm rhs_tm =\r
 295   let iabs_eq = float_iabs int_tm in\r
 296   let lt_th = float_lt (rand (concl iabs_eq)) rhs_tm in\r
 297     if (fst o dest_const o rand o concl) lt_th <> "T" then\r
 298       failwith "check_interval_iabs: iabs < rhs <=> F"\r
 299     else\r
 300       let th0 = AP_THM (AP_TERM lt_op_real iabs_eq) rhs_tm in\r
 301         TRANS th0 lt_th;;\r
 302       \r
 303 \r
 304 (*\r
 305 check_interval_iabs int2 (mk_float 41 49);;\r
 306 *)\r
 307 \r
 308 \r
 309 (****************************)\r
 310 (* inv *)\r
 311 \r
 312 let INV_EQ_DIV_LEMMA = prove(`&1 / x = inv x`, REWRITE_TAC[real_div; REAL_MUL_LID]);;\r
 313 \r
 314 \r
 315 let float_interval_inv pp th =\r
 316   let x_tm = (rand o rator o concl) th in\r
 317   let div_th = INST[x_tm, x_var_real] INV_EQ_DIV_LEMMA in\r
 318   let th0 = float_interval_div pp one_interval th in\r
 319   let lhs, rhs = dest_comb (concl th0) in\r
 320   let lhs2, rhs2 = dest_comb lhs in\r
 321     EQ_MP (AP_THM (AP_TERM lhs2 div_th) rhs) th0;;\r
 322 \r
 323 \r
 324 \r
 325 (*****************************************)\r
 326 (* bounded_on_int *)\r
 327 \r
 328 \r
 329 let norm_derivative d_th eq_th =\r
 330   let lhs, rhs = (dest_eq o concl) d_th in\r
 331   let lhs2, rhs2 = dest_comb lhs in\r
 332   let th0 = AP_THM (AP_TERM (rator lhs2) eq_th) rhs2 in\r
 333     TRANS (SYM th0) d_th;;\r
 334 \r
 335 let norm_diff d_th eq_th =\r
 336   let lhs, rhs = (dest_comb o concl) d_th in\r
 337   let th0 = AP_THM (AP_TERM (rator lhs) eq_th) rhs in\r
 338     EQ_MP th0 d_th;;\r
 339 \r
 340 let norm_interval int_th eq_th =\r
 341   let lhs, rhs = (dest_comb o concl) int_th in\r
 342   let th0 = AP_THM (AP_TERM (rator lhs) eq_th) rhs in\r
 343     EQ_MP (SYM th0) int_th;;\r
 344 \r
 345 let norm_second_derivative th eq_th =\r
 346   let lhs, dd_bounds = dest_comb (concl th) in\r
 347   let lhs2, int_tm = dest_comb lhs in\r
 348   let th0 = AP_THM (AP_THM (AP_TERM (rator lhs2) eq_th) int_tm) dd_bounds in\r
 349     EQ_MP th0 th;;\r
 350 \r
 351 let norm_lin_approx th eq_th =\r
 352   let lhs, df_bounds = dest_comb (concl th) in\r
 353   let lhs2, f_bounds = dest_comb lhs in\r
 354   let lhs3, x_tm = dest_comb lhs2 in\r
 355   let th0 = AP_THM (AP_THM (AP_THM (AP_TERM (rator lhs3) eq_th) x_tm) f_bounds) df_bounds in\r
 356     EQ_MP th0 th;;\r
 357 \r
 358 \r
 359 \r
 360 \r
 361 \r
 362 let BOUNDED_ON_INT = (UNDISCH_ALL o prove)(`(!x. interval_arith x int ==> \r
 363                                                interval_arith (f x) f_bounds) \r
 364                            ==> bounded_on_int f int f_bounds`,\r
 365   REWRITE_TAC[bounded_on_int; interval_arith; IN_REAL_INTERVAL]);;\r
 366 \r
 367 \r
 368 let BOUNDED_ON_INT_DEST = (UNDISCH_ALL o prove)(`bounded_on_int f int f_bounds ==>\r
 369                         (!x. interval_arith x int ==> interval_arith (f x) f_bounds)`,\r
 370   REWRITE_TAC[bounded_on_int; interval_arith; IN_REAL_INTERVAL]);;\r
 371 \r
 372 \r
 373 let mk_bounded_on_int th =\r
 374   let int_tm = (rand o hd o hyp) th in\r
 375   let lhs, f_bounds_tm = dest_comb (concl th) in\r
 376   let lhs2, rhs2 = dest_comb lhs in\r
 377   let f_tm = mk_abs (x_var_real, rhs2) in\r
 378   let b_th0 = (SYM o BETA_CONV) (mk_comb (f_tm , x_var_real)) in\r
 379   let b_th1 = AP_THM (AP_TERM lhs2 b_th0) f_bounds_tm in\r
 380   let th2 = EQ_MP b_th1 th in\r
 381   let th3 = DISCH_ALL th2 in\r
 382   let th4 = GEN x_var_real th3 in\r
 383   let th_int = INST[int_tm, int_var; f_bounds_tm, f_bounds_var;\r
 384                     f_tm, f_var_fun] BOUNDED_ON_INT in\r
 385     MY_PROVE_HYP th4 th_int;;\r
 386 \r
 387 \r
 388 \r
 389 let dest_bounded_on_int th =\r
 390   let lhs, f_bounds = dest_comb (concl th) in\r
 391   let lhs2, int_tm = dest_comb lhs in\r
 392   let f_tm = rand lhs2 in\r
 393   let th0 = INST[f_tm, f_var_fun; int_tm, int_var; f_bounds, f_bounds_var] BOUNDED_ON_INT_DEST in\r
 394   let th1 = UNDISCH_ALL (SPEC x_var_real (MY_PROVE_HYP th th0)) in\r
 395     if is_abs f_tm then\r
 396       let f_tm = (rand o rator o concl) th1 in\r
 397       let eq_th = BETA_CONV f_tm in\r
 398         norm_interval th1 (SYM eq_th)\r
 399     else\r
 400       th1;;\r
 401 \r
 402 \r
 403 let dest_bounded_on_int_raw th =\r
 404   let lhs, f_bounds = dest_comb (concl th) in\r
 405   let lhs2, int_tm = dest_comb lhs in\r
 406   let f_tm = rand lhs2 in\r
 407   let th0 = INST[f_tm, f_var_fun; int_tm, int_var; f_bounds, f_bounds_var] BOUNDED_ON_INT_DEST in\r
 408     UNDISCH_ALL (SPEC x_var_real (MY_PROVE_HYP th th0));;\r
 409     \r
 410 \r
 411 (*\r
 412 let pp = 5;;\r
 413 let th0 = (RULE o ASSUME) `interval_arith x (&2, &3)`;;\r
 414 let th = float_interval_atn pp th0;;\r
 415 let b_th = mk_bounded_on_int th;;\r
 416 let d_th = dest_bounded_on_int b_th;;\r
 417 *)\r
 418 \r
 419 (***********************************)\r
 420 (* bounded_on_int arithmetic *)\r
 421 \r
 422 let bounded_on_int_scale pp c_tm th =\r
 423   let i_th = dest_bounded_on_int th in\r
 424   let th0 = float_interval_scale pp c_tm i_th in\r
 425     mk_bounded_on_int th0;;\r
 426 \r
 427 \r
 428 let bounded_on_int_mul_int pp int_th th =\r
 429   let i_th = dest_bounded_on_int th in\r
 430   let th0 = float_interval_mul pp int_th i_th in\r
 431     mk_bounded_on_int th0;;\r
 432 \r
 433 \r
 434 let bounded_on_int_neg th1 =\r
 435   let i_th = dest_bounded_on_int th1 in\r
 436   let th0 = float_interval_neg i_th in\r
 437     mk_bounded_on_int th0;;\r
 438 \r
 439 \r
 440 let bounded_on_int_add pp th1 th2 =\r
 441   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 442   let th0 = float_interval_add pp i_th1 i_th2 in\r
 443     mk_bounded_on_int th0;;\r
 444 \r
 445 \r
 446 let bounded_on_int_sub pp th1 th2 =\r
 447   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 448   let th0 = float_interval_sub pp i_th1 i_th2 in\r
 449     mk_bounded_on_int th0;;\r
 450 \r
 451 \r
 452 let bounded_on_int_mul pp th1 th2 =\r
 453   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 454   let th0 = float_interval_mul pp i_th1 i_th2 in\r
 455     mk_bounded_on_int th0;;\r
 456 \r
 457 \r
 458 let bounded_on_int_mul_raw pp th1 th2 =\r
 459   let i_th1, i_th2 = dest_bounded_on_int_raw th1, dest_bounded_on_int_raw th2 in\r
 460   let th0 = float_interval_mul pp i_th1 i_th2 in\r
 461     mk_bounded_on_int th0;;\r
 462 \r
 463 \r
 464 \r
 465 let bounded_on_int_div pp th1 th2 =\r
 466   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 467   let th0 = float_interval_div pp i_th1 i_th2 in\r
 468     mk_bounded_on_int th0;;\r
 469 \r
 470 \r
 471 (*\r
 472 let b_sub = bounded_on_int_sub pp b_th b_th;;\r
 473 bounded_on_int_mul pp b_sub b_th;;\r
 474 *)\r
 475 \r
 476 \r
 477 (************************************)\r
 478 let ADD_INEQ_HI = (RULE o REAL_ARITH) `x1 <= y1 /\ x2 <= y2 /\ y1 + y2 <= y ==> x1 + x2 <= y`;;\r
 479 let ADD_INEQ_LO = (RULE o REAL_ARITH) `x1 <= y1 /\ x2 <= y2 /\ x <= x1 + x2 ==> x <= y1 + y2`;;\r
 480 let SUB_INEQ_HI = (RULE o REAL_ARITH) `x1 <= y1 /\ y2 <= x2 /\ y1 - y2 <= y ==> x1 - x2 <= y`;;\r
 481 let SUB_INEQ_LO = (RULE o REAL_ARITH) `x1 <= y1 /\ y2 <= x2 /\ x <= x1 - x2 ==> x <= y1 - y2`;;\r
 482 let MUL_INEQ_HI = (UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o prove) \r
 483   (`&0 <= x1 /\ &0 <= x2 /\ x1 <= y1 /\ x2 <= y2 /\ y1 * y2 <= y ==> x1 * x2 <= y`,\r
 484   DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN\r
 485     EXISTS_TAC `y1 * y2` THEN ASM_REWRITE_TAC[] THEN\r
 486     MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[]);;\r
 487 \r
 488 let MUL_INEQ_POS_CONST_HI = (UNDISCH_ALL o prove)\r
 489   (`(&0 <= x <=> T) ==> y1 <= y2 ==> x * y2 <= z ==> x * y1 <= z`, \r
 490    REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x * y2` THEN\r
 491      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[]);;\r
 492 \r
 493 \r
 494 let REAL_LE_REFL' = RULE REAL_LE_REFL;;\r
 495 \r
 496 \r
 497 let mk_refl_ineq tm = INST[tm, x_var_real] REAL_LE_REFL';;\r
 498 \r
 499 let dest_le_op ineq =\r
 500   let lhs, y_tm = dest_comb ineq in (rand lhs, y_tm);;\r
 501 \r
 502 \r
 503 let y1_var_real = `y1:real` and\r
 504     x1_var_real = `x1:real` and\r
 505     y2_var_real = `y2:real` and\r
 506     x2_var_real = `x2:real` and\r
 507     z_var_real = `z:real`;;\r
 508 \r
 509 \r
 510 let mul_ineq_pos_const_hi pp c_tm ineq =\r
 511   let y1_tm, y2_tm = dest_le_op (concl ineq) in\r
 512   let ge0_th = float_ge0 c_tm in\r
 513   let mul_hi_th = float_mul_hi pp c_tm y2_tm in\r
 514   let z_tm = (rand o concl) mul_hi_th in\r
 515     (MY_PROVE_HYP ge0_th o MY_PROVE_HYP ineq o MY_PROVE_HYP mul_hi_th o\r
 516        INST[c_tm, x_var_real; y1_tm, y1_var_real; y2_tm, y2_var_real; z_tm, z_var_real])\r
 517       MUL_INEQ_POS_CONST_HI;;\r
 518 \r
 519 \r
 520 let mul_ineq_hi pp ineq1 ineq2 =\r
 521   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 522   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 523   let x1_pos, x2_pos = float_pos x1_tm, float_pos x2_tm in\r
 524   let rhs_mul = float_mul_hi pp y1_tm y2_tm in\r
 525   let y_tm = (rand o concl) rhs_mul in\r
 526   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 527                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 528                  y_tm, y_var_real] MUL_INEQ_HI in\r
 529     (MY_PROVE_HYP x1_pos o MY_PROVE_HYP x2_pos o MY_PROVE_HYP ineq1 o\r
 530        MY_PROVE_HYP ineq2 o MY_PROVE_HYP rhs_mul) th0;;\r
 531 \r
 532 \r
 533 \r
 534 let sub_ineq_hi pp ineq1 ineq2 =\r
 535   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 536   let y2_tm, x2_tm = dest_le_op (concl ineq2) in\r
 537   let rhs_sub = float_sub_hi pp y1_tm y2_tm in\r
 538   let y_tm = (rand o concl) rhs_sub in\r
 539   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 540                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 541                  y_tm, y_var_real] SUB_INEQ_HI in\r
 542     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP rhs_sub th0));;\r
 543 \r
 544 let sub_ineq_lo pp ineq1 ineq2 =\r
 545   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 546   let y2_tm, x2_tm = dest_le_op (concl ineq2) in\r
 547   let lhs_sub = float_sub_lo pp x1_tm x2_tm in\r
 548   let x_tm = (lhand o concl) lhs_sub in\r
 549   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 550                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 551                  x_tm, x_var_real] SUB_INEQ_LO in\r
 552     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP lhs_sub th0));;\r
 553 \r
 554 \r
 555 \r
 556 let add_ineq_hi pp ineq1 ineq2 =\r
 557   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 558   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 559   let rhs_sum = float_add_hi pp y1_tm y2_tm in\r
 560   let y_tm = (rand o concl) rhs_sum in\r
 561   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 562                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 563                  y_tm, y_var_real] ADD_INEQ_HI in\r
 564     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP rhs_sum th0));;\r
 565 \r
 566 \r
 567 let add_ineq_lo pp ineq1 ineq2 =\r
 568   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 569   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 570   let lhs_sum = float_add_lo pp x1_tm x2_tm in\r
 571   let x_tm = (lhand o concl) lhs_sum in\r
 572   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 573                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 574                  x_tm, x_var_real] ADD_INEQ_LO in\r
 575     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP lhs_sum th0));;\r
 576 \r