formal_ineqs/arith/more_float.hl

   1 (* =========================================================== *)\r
   2 (* Additional floating point procedures                        *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 needs "arith/float.hl";;\r
   8 needs "misc/vars.hl";;\r
   9 \r
  10 module More_float = struct\r
  11 \r
  12 open Arith_misc;;\r
  13 open Float_theory;;\r
  14 open Interval_arith;;\r
  15 open Arith_float;;\r
  16 open Misc_vars;;\r
  17 \r
  18 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
  19 \r
  20 (*************************************)\r
  21 (* More float *)\r
  22 \r
  23 \r
  24 (* Converts a float term to the corresponding rational number *)\r
  25 let num_of_float_tm tm =\r
  26   let s, n_tm, e_tm = dest_float tm in\r
  27   let b = Num.num_of_int Arith_hash.arith_base in\r
  28   let m = Num.num_of_int Float_theory.min_exp in\r
  29   let ( * ), (^), (-), (!) = ( */ ), ( **/ ), (-/), Arith_nat.raw_dest_hash in\r
  30   let r = !n_tm * (b ^ (!e_tm - m)) in\r
  31     if s = "T" then minus_num r else r;;\r
  32 \r
  33 (* Converts a float term to a floating point number *)\r
  34 (* Note: float_of_num gives a very bad approximation in some cases *)\r
  35 let float_of_float_tm tm =\r
  36   (float_of_string o approx_num_exp 30 o num_of_float_tm) tm;;\r
  37 \r
  38 \r
  39 (* Creates a float term with the value (n * base^e) *)\r
  40 let mk_float =\r
  41         let float_const = `float_num` in\r
  42         fun n e ->\r
  43   let n, s = if n < 0 then -n, `T` else n, `F` in\r
  44   let n_tm = rand (Arith_nat.mk_small_numeral_array n) in\r
  45   let e_tm = rand (Arith_nat.mk_small_numeral_array (e + Float_theory.min_exp)) in\r
  46     mk_comb(mk_comb(mk_comb (float_const, s), n_tm), e_tm);;\r
  47 \r
  48 \r
  49 (* |- ##0 = &0, |- ##1 = &1, |- ##2 = &2, |- ##3 = &3, |- ##4 = &4 *)\r
  50 let float0_eq = FLOAT_TO_NUM_CONV (mk_float 0 0) and\r
  51     float1_eq = FLOAT_TO_NUM_CONV (mk_float 1 0) and\r
  52     float2_eq = FLOAT_TO_NUM_CONV (mk_float 2 0) and\r
  53     float3_eq = FLOAT_TO_NUM_CONV (mk_float 3 0) and\r
  54     float4_eq = FLOAT_TO_NUM_CONV (mk_float 4 0);;\r
  55 \r
  56 (* |- D_k _0 = k for k = 1, 2, 3 *)\r
  57 let num1_eq, num2_eq, num3_eq = \r
  58   let conv = SYM o REWRITE_RULE[Arith_hash.NUM_THM] o Arith_nat.NUMERAL_TO_NUM_CONV in\r
  59     conv `1`, conv `2`, conv `3`;;\r
  60 \r
  61 (*********************)\r
  62 \r
  63 let float_F_const = `float_num F`;;\r
  64 \r
  65 let mk_float_small n =\r
  66   let n_tm0 = mk_small_numeral n in\r
  67   let n_th = Arith_nat.NUMERAL_TO_NUM_CONV n_tm0 in\r
  68   let n_tm = rand(rand(concl n_th)) in\r
  69     mk_comb(mk_comb(float_F_const, n_tm), min_exp_num_const);;\r
  70 \r
  71 (* Small float constants and intervals *)\r
  72 let one_float = mk_float_small 1 and\r
  73     two_float = mk_float_small 2 and\r
  74     one_interval = mk_float_interval_small_num 1 and\r
  75     two_interval = mk_float_interval_small_num 2;;\r
  76 let neg_two_interval = float_interval_neg two_interval;;\r
  77 \r
  78 (***********************************)\r
  79 (* float_eq0 *)\r
  80 \r
  81 let FLOAT_EQ_0' = (GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [NUMERAL] o SPEC_ALL) \r
  82   FLOAT_EQ_0;;\r
  83 \r
  84 \r
  85 let float_eq0 f_tm =\r
  86   let lhs, e_tm = dest_comb f_tm in\r
  87   let lhs2, n_tm = dest_comb lhs in\r
  88   let th0 = INST[rand lhs2, s_var_bool; n_tm, n_var_num; e_tm, e_var_num] FLOAT_EQ_0' in\r
  89   let eq_th = Arith_nat.raw_eq0_hash_conv n_tm in\r
  90     TRANS th0 eq_th;;\r
  91 \r
  92 \r
  93 \r
  94 (***********************************)\r
  95 (* float_interval_scale *)\r
  96 \r
  97 let float_interval_scale pp c_tm th =\r
  98   let c_th = mk_const_interval c_tm in\r
  99     float_interval_mul pp c_th th;;\r
 100 \r
 101 \r
 102 (***********************************)\r
 103 (* float_interval_lt0 *)\r
 104 \r
 105 let FLOAT_INTERVAL_LT0' = (UNDISCH_ALL o prove)\r
 106   (`interval_arith x (lo, hi) ==> (hi < &0 <=> T) ==> x < &0`,\r
 107    REWRITE_TAC[interval_arith] THEN REAL_ARITH_TAC);;\r
 108 \r
 109 let float_interval_lt0 th =\r
 110   let x_tm, bounds = dest_interval_arith (concl th) in\r
 111   let lo_tm, hi_tm = dest_pair bounds in\r
 112   let lt0_th = float_lt0 hi_tm in\r
 113   let _ = ((rand o concl) lt0_th = t_const) or failwith "float_interval_lt0: &0 <= hi" in\r
 114   let th0 = INST[x_tm, x_var_real; lo_tm, lo_var_real; hi_tm, hi_var_real] FLOAT_INTERVAL_LT0' in\r
 115     (MY_PROVE_HYP th o MY_PROVE_HYP lt0_th) th0;;\r
 116 \r
 117 \r
 118 (**********************************)\r
 119 (* float_pos *)\r
 120 let FLOAT_F_POS' = SPEC_ALL FLOAT_F_POS;;\r
 121 \r
 122 (* Returns &0 <= float F n e *)\r
 123 let float_pos tm =\r
 124   let _, n_tm, e_tm = dest_float tm in\r
 125     INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_F_POS';;\r
 126 \r
 127 \r
 128 \r
 129 (************************************)\r
 130 (* float_iabs *)\r
 131 \r
 132 let FLOAT_NEG_F' = RULE FLOAT_NEG_T;;\r
 133 let FLOAT_NEG_T' = RULE FLOAT_NEG_F;;\r
 134 \r
 135 let float_neg tm =\r
 136   let sign, n_tm, e_tm = dest_float tm in\r
 137     if sign = "T" then\r
 138       INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_T'\r
 139     else\r
 140       INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_F';;\r
 141 \r
 142 \r
 143 let IABS' = RULE iabs;;\r
 144 \r
 145 \r
 146 let float_iabs int_tm =\r
 147   let lo_tm, hi_tm = dest_pair int_tm in\r
 148   let neg_lo_th = float_neg lo_tm in\r
 149   let max_th = SYM (float_max hi_tm ((rand o rator o concl) neg_lo_th)) in\r
 150   let lhs, rhs = dest_comb (concl max_th) in\r
 151   let th0 = SYM (EQ_MP (AP_TERM lhs (AP_TERM (rator rhs) neg_lo_th)) max_th) in\r
 152   let th1 = INST[lo_tm, x_lo_var; hi_tm, x_hi_var] IABS' in\r
 153     TRANS th1 th0;;\r
 154 \r
 155 \r
 156 let FLOAT_IABS_FF = prove(`iabs (float_num F n1 e1, float_num F n2 e2) = float_num F n2 e2`,\r
 157   REWRITE_TAC[iabs] THEN\r
 158     MP_TAC (SPECL [`n1:num`; `e1:num`] FLOAT_F_POS) THEN\r
 159     MP_TAC (SPECL [`n2:num`; `e2:num`] FLOAT_F_POS) THEN\r
 160     REAL_ARITH_TAC);;\r
 161 \r
 162 \r
 163 let FLOAT_IABS_TT = prove(`iabs (float_num T n1 e1, float_num T n2 e2) = float_num F n1 e1`,\r
 164   REWRITE_TAC[iabs; GSYM FLOAT_NEG_F] THEN\r
 165     MP_TAC (SPECL [`n1:num`; `e1:num`] FLOAT_F_POS) THEN\r
 166     MP_TAC (SPECL [`n2:num`; `e2:num`] FLOAT_T_NEG) THEN\r
 167     REAL_ARITH_TAC);;\r
 168 \r
 169 \r
 170 (****************************)\r
 171 (* interval_not_zero *)\r
 172 \r
 173 let INTERVAL_NOT_ZERO1' = (UNDISCH_ALL o prove)\r
 174   (`(&0 < lo <=> T) ==> interval_not_zero (lo, hi)`, SIMP_TAC[interval_not_zero]);;\r
 175 let INTERVAL_NOT_ZERO2' = (UNDISCH_ALL o prove)\r
 176   (`(hi < &0 <=> T) ==> interval_not_zero (lo, hi)`, SIMP_TAC[interval_not_zero]);;\r
 177 \r
 178 \r
 179 let check_interval_not_zero int_tm =\r
 180   let lo, hi = dest_pair int_tm in\r
 181   let inst = INST[lo, lo_var_real; hi, hi_var_real] in\r
 182   let s1, _, _ = dest_float lo in\r
 183     if s1 = "F" then\r
 184       let gt_th = float_gt0 lo in\r
 185         if (fst o dest_const o rand o concl) gt_th <> "T" then\r
 186           failwith "check_interval_not_zero: &0 < lo <=> F"\r
 187         else\r
 188           (MY_PROVE_HYP gt_th o inst) INTERVAL_NOT_ZERO1'\r
 189     else\r
 190       let lt_th = float_lt0 hi in\r
 191         if (fst o dest_const o rand o concl) lt_th <> "T" then\r
 192           failwith "check_interval_not_zero: hi < &0 <=> F"\r
 193         else\r
 194           (MY_PROVE_HYP lt_th o inst) INTERVAL_NOT_ZERO2';;\r
 195 \r
 196 \r
 197 \r
 198 (*************************************)\r
 199 (* interval_pos *)\r
 200 \r
 201 let INTERVAL_POS' = (UNDISCH_ALL o prove)\r
 202   (`(&0 < lo <=> T) ==> interval_pos (lo, hi:real)`, SIMP_TAC[interval_pos]);;\r
 203 \r
 204 \r
 205 let check_interval_pos int_tm =\r
 206   let lo, hi = dest_pair int_tm in\r
 207   let gt_th = float_gt0 lo in\r
 208     if (fst o dest_const o rand o concl) gt_th <> "T" then\r
 209       failwith "check_interval_pos: &0 < lo <=> F"\r
 210     else\r
 211       (MY_PROVE_HYP gt_th o INST[lo, lo_var_real; hi, hi_var_real]) INTERVAL_POS';;\r
 212 \r
 213 \r
 214 \r
 215 (************************************)\r
 216 (* check_interval_iabs *)\r
 217 \r
 218 \r
 219 (* proves |- iabs int < rhs <=> T *)\r
 220 let check_interval_iabs int_tm rhs_tm =\r
 221   let iabs_eq = float_iabs int_tm in\r
 222   let lt_th = float_lt (rand (concl iabs_eq)) rhs_tm in\r
 223     if (fst o dest_const o rand o concl) lt_th <> "T" then\r
 224       failwith "check_interval_iabs: iabs < rhs <=> F"\r
 225     else\r
 226       let th0 = AP_THM (AP_TERM lt_op_real iabs_eq) rhs_tm in\r
 227         TRANS th0 lt_th;;\r
 228       \r
 229 \r
 230 \r
 231 (****************************)\r
 232 (* inv *)\r
 233 \r
 234 let INV_EQ_DIV_LEMMA = prove(`&1 / x = inv x`, REWRITE_TAC[real_div; REAL_MUL_LID]);;\r
 235 \r
 236 \r
 237 let float_interval_inv pp th =\r
 238   let x_tm = (rand o rator o concl) th in\r
 239   let div_th = INST[x_tm, x_var_real] INV_EQ_DIV_LEMMA in\r
 240   let th0 = float_interval_div pp one_interval th in\r
 241   let lhs, rhs = dest_comb (concl th0) in\r
 242   let lhs2, rhs2 = dest_comb lhs in\r
 243     EQ_MP (AP_THM (AP_TERM lhs2 div_th) rhs) th0;;\r
 244 \r
 245 \r
 246 (* Explicit representation of inv(&2) *)\r
 247 let float_inv2_th =\r
 248   let one_float_eq_one = FLOAT_TO_NUM_CONV one_float in\r
 249   let inv2_eq_lemma = prove(`interval_arith (&2 * x) (&1, &1) ==> inv (&2) = x`,\r
 250                             REWRITE_TAC[interval_arith] THEN CONV_TAC REAL_FIELD) in\r
 251   let half_tm = (fst o dest_pair o rand o concl) (float_interval_inv 1 two_interval) in\r
 252   let half_interval = mk_const_interval half_tm in\r
 253   let mul_th = REWRITE_RULE[one_float_eq_one] (float_interval_mul 2 two_interval half_interval) in\r
 254     MATCH_MP inv2_eq_lemma mul_th;;\r
 255 \r
 256 let float_inv2 = rand (concl float_inv2_th);;\r
 257 let inv2_interval = mk_const_interval float_inv2;;\r
 258 \r
 259 \r
 260 \r
 261 (*****************************************)\r
 262 (* bounded_on_int *)\r
 263 \r
 264 let norm_derivative d_th eq_th =\r
 265   let lhs, rhs = (dest_eq o concl) d_th in\r
 266   let lhs2, rhs2 = dest_comb lhs in\r
 267   let th0 = AP_THM (AP_TERM (rator lhs2) eq_th) rhs2 in\r
 268     TRANS (SYM th0) d_th;;\r
 269 \r
 270 let norm_diff d_th eq_th =\r
 271   let lhs, rhs = (dest_comb o concl) d_th in\r
 272   let th0 = AP_THM (AP_TERM (rator lhs) eq_th) rhs in\r
 273     EQ_MP th0 d_th;;\r
 274 \r
 275 let norm_interval int_th eq_th =\r
 276   let lhs, rhs = (dest_comb o concl) int_th in\r
 277   let th0 = AP_THM (AP_TERM (rator lhs) eq_th) rhs in\r
 278     EQ_MP (SYM th0) int_th;;\r
 279 \r
 280 let norm_second_derivative th eq_th =\r
 281   let lhs, dd_bounds = dest_comb (concl th) in\r
 282   let lhs2, int_tm = dest_comb lhs in\r
 283   let th0 = AP_THM (AP_THM (AP_TERM (rator lhs2) eq_th) int_tm) dd_bounds in\r
 284     EQ_MP th0 th;;\r
 285 \r
 286 let norm_lin_approx th eq_th =\r
 287   let lhs, df_bounds = dest_comb (concl th) in\r
 288   let lhs2, f_bounds = dest_comb lhs in\r
 289   let lhs3, x_tm = dest_comb lhs2 in\r
 290   let th0 = AP_THM (AP_THM (AP_THM (AP_TERM (rator lhs3) eq_th) x_tm) f_bounds) df_bounds in\r
 291     EQ_MP th0 th;;\r
 292 \r
 293 \r
 294 \r
 295 let BOUNDED_ON_INT = (UNDISCH_ALL o prove)(`(!x. interval_arith x int ==> \r
 296                                                interval_arith (f x) f_bounds) \r
 297                            ==> bounded_on_int f int f_bounds`,\r
 298   REWRITE_TAC[bounded_on_int; interval_arith]);;\r
 299 \r
 300 \r
 301 let BOUNDED_ON_INT_DEST = (UNDISCH_ALL o prove)(`bounded_on_int f int f_bounds ==>\r
 302                         (!x. interval_arith x int ==> interval_arith (f x) f_bounds)`,\r
 303   REWRITE_TAC[bounded_on_int; interval_arith]);;\r
 304 \r
 305 \r
 306 (* Given a theorem (interval_arith x int |- interval_arith (f x) f_bounds), yields\r
 307    |- bounded_on_int (\x. f x) int f_bounds *)\r
 308 let mk_bounded_on_int th =\r
 309   let int_tm = (rand o hd o hyp) th in\r
 310   let lhs, f_bounds_tm = dest_comb (concl th) in\r
 311   let lhs2, rhs2 = dest_comb lhs in\r
 312   let f_tm = mk_abs (x_var_real, rhs2) in\r
 313   let b_th0 = (SYM o BETA_CONV) (mk_comb (f_tm , x_var_real)) in\r
 314   let b_th1 = AP_THM (AP_TERM lhs2 b_th0) f_bounds_tm in\r
 315   let th2 = EQ_MP b_th1 th in\r
 316   let th3 = DISCH_ALL th2 in\r
 317   let th4 = GEN x_var_real th3 in\r
 318   let th_int = INST[int_tm, int_var; f_bounds_tm, f_bounds_var;\r
 319                     f_tm, f_var_fun] BOUNDED_ON_INT in\r
 320     MY_PROVE_HYP th4 th_int;;\r
 321 \r
 322 \r
 323 let dest_bounded_on_int th =\r
 324   let lhs, f_bounds = dest_comb (concl th) in\r
 325   let lhs2, int_tm = dest_comb lhs in\r
 326   let f_tm = rand lhs2 in\r
 327   let th0 = INST[f_tm, f_var_fun; int_tm, int_var; f_bounds, f_bounds_var] BOUNDED_ON_INT_DEST in\r
 328   let th1 = UNDISCH_ALL (SPEC x_var_real (MY_PROVE_HYP th th0)) in\r
 329     if is_abs f_tm then\r
 330       let f_tm = (rand o rator o concl) th1 in\r
 331       let eq_th = BETA_CONV f_tm in\r
 332         norm_interval th1 (SYM eq_th)\r
 333     else\r
 334       th1;;\r
 335 \r
 336 \r
 337 let dest_bounded_on_int_raw th =\r
 338   let lhs, f_bounds = dest_comb (concl th) in\r
 339   let lhs2, int_tm = dest_comb lhs in\r
 340   let f_tm = rand lhs2 in\r
 341   let th0 = INST[f_tm, f_var_fun; int_tm, int_var; f_bounds, f_bounds_var] BOUNDED_ON_INT_DEST in\r
 342     UNDISCH_ALL (SPEC x_var_real (MY_PROVE_HYP th th0));;\r
 343     \r
 344 \r
 345 (***********************************)\r
 346 (* bounded_on_int arithmetic *)\r
 347 \r
 348 let bounded_on_int_scale pp c_tm th =\r
 349   let i_th = dest_bounded_on_int th in\r
 350   let th0 = float_interval_scale pp c_tm i_th in\r
 351     mk_bounded_on_int th0;;\r
 352 \r
 353 \r
 354 let bounded_on_int_mul_int pp int_th th =\r
 355   let i_th = dest_bounded_on_int th in\r
 356   let th0 = float_interval_mul pp int_th i_th in\r
 357     mk_bounded_on_int th0;;\r
 358 \r
 359 \r
 360 let bounded_on_int_neg th1 =\r
 361   let i_th = dest_bounded_on_int th1 in\r
 362   let th0 = float_interval_neg i_th in\r
 363     mk_bounded_on_int th0;;\r
 364 \r
 365 \r
 366 let bounded_on_int_add pp th1 th2 =\r
 367   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 368   let th0 = float_interval_add pp i_th1 i_th2 in\r
 369     mk_bounded_on_int th0;;\r
 370 \r
 371 \r
 372 let bounded_on_int_sub pp th1 th2 =\r
 373   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 374   let th0 = float_interval_sub pp i_th1 i_th2 in\r
 375     mk_bounded_on_int th0;;\r
 376 \r
 377 \r
 378 let bounded_on_int_mul pp th1 th2 =\r
 379   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 380   let th0 = float_interval_mul pp i_th1 i_th2 in\r
 381     mk_bounded_on_int th0;;\r
 382 \r
 383 \r
 384 let bounded_on_int_mul_raw pp th1 th2 =\r
 385   let i_th1, i_th2 = dest_bounded_on_int_raw th1, dest_bounded_on_int_raw th2 in\r
 386   let th0 = float_interval_mul pp i_th1 i_th2 in\r
 387     mk_bounded_on_int th0;;\r
 388 \r
 389 \r
 390 \r
 391 let bounded_on_int_div pp th1 th2 =\r
 392   let i_th1, i_th2 = dest_bounded_on_int th1, dest_bounded_on_int th2 in\r
 393   let th0 = float_interval_div pp i_th1 i_th2 in\r
 394     mk_bounded_on_int th0;;\r
 395 \r
 396 \r
 397 (************************************)\r
 398 let ADD_INEQ_HI = (RULE o REAL_ARITH) `x1 <= y1 /\ x2 <= y2 /\ y1 + y2 <= y ==> x1 + x2 <= y`;;\r
 399 let ADD_INEQ_LO = (RULE o REAL_ARITH) `x1 <= y1 /\ x2 <= y2 /\ x <= x1 + x2 ==> x <= y1 + y2`;;\r
 400 let SUB_INEQ_HI = (RULE o REAL_ARITH) `x1 <= y1 /\ y2 <= x2 /\ y1 - y2 <= y ==> x1 - x2 <= y`;;\r
 401 let SUB_INEQ_LO = (RULE o REAL_ARITH) `x1 <= y1 /\ y2 <= x2 /\ x <= x1 - x2 ==> x <= y1 - y2`;;\r
 402 let MUL_INEQ_HI = (UNDISCH_ALL o REWRITE_RULE[GSYM IMP_IMP] o prove) \r
 403   (`&0 <= x1 /\ &0 <= x2 /\ x1 <= y1 /\ x2 <= y2 /\ y1 * y2 <= y ==> x1 * x2 <= y`,\r
 404   DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN\r
 405     EXISTS_TAC `y1 * y2` THEN ASM_REWRITE_TAC[] THEN\r
 406     MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[]);;\r
 407 \r
 408 let MUL_INEQ_POS_CONST_HI = (UNDISCH_ALL o prove)\r
 409   (`(&0 <= x <=> T) ==> y1 <= y2 ==> x * y2 <= z ==> x * y1 <= z`, \r
 410    REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x * y2` THEN\r
 411      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[]);;\r
 412 \r
 413 \r
 414 let mk_refl_ineq =\r
 415   let REAL_LE_REFL' = RULE REAL_LE_REFL in\r
 416     fun tm -> INST[tm, x_var_real] REAL_LE_REFL';;\r
 417 \r
 418 let dest_le_op ineq =\r
 419   let lhs, y_tm = dest_comb ineq in \r
 420     (rand lhs, y_tm);;\r
 421 \r
 422 \r
 423 let mul_ineq_pos_const_hi pp c_tm ineq =\r
 424   let y1_tm, y2_tm = dest_le_op (concl ineq) in\r
 425   let ge0_th = float_ge0 c_tm in\r
 426   let mul_hi_th = float_mul_hi pp c_tm y2_tm in\r
 427   let z_tm = (rand o concl) mul_hi_th in\r
 428     (MY_PROVE_HYP ge0_th o MY_PROVE_HYP ineq o MY_PROVE_HYP mul_hi_th o\r
 429        INST[c_tm, x_var_real; y1_tm, y1_var_real; y2_tm, y2_var_real; z_tm, z_var_real])\r
 430       MUL_INEQ_POS_CONST_HI;;\r
 431 \r
 432 \r
 433 let mul_ineq_hi pp ineq1 ineq2 =\r
 434   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 435   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 436   let x1_pos, x2_pos = float_pos x1_tm, float_pos x2_tm in\r
 437   let rhs_mul = float_mul_hi pp y1_tm y2_tm in\r
 438   let y_tm = (rand o concl) rhs_mul in\r
 439   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 440                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 441                  y_tm, y_var_real] MUL_INEQ_HI in\r
 442     (MY_PROVE_HYP x1_pos o MY_PROVE_HYP x2_pos o MY_PROVE_HYP ineq1 o\r
 443        MY_PROVE_HYP ineq2 o MY_PROVE_HYP rhs_mul) th0;;\r
 444 \r
 445 \r
 446 \r
 447 let sub_ineq_hi pp ineq1 ineq2 =\r
 448   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 449   let y2_tm, x2_tm = dest_le_op (concl ineq2) in\r
 450   let rhs_sub = float_sub_hi pp y1_tm y2_tm in\r
 451   let y_tm = (rand o concl) rhs_sub in\r
 452   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 453                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 454                  y_tm, y_var_real] SUB_INEQ_HI in\r
 455     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP rhs_sub th0));;\r
 456 \r
 457 \r
 458 let sub_ineq_lo pp ineq1 ineq2 =\r
 459   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 460   let y2_tm, x2_tm = dest_le_op (concl ineq2) in\r
 461   let lhs_sub = float_sub_lo pp x1_tm x2_tm in\r
 462   let x_tm = (lhand o concl) lhs_sub in\r
 463   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 464                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 465                  x_tm, x_var_real] SUB_INEQ_LO in\r
 466     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP lhs_sub th0));;\r
 467 \r
 468 \r
 469 let add_ineq_hi pp ineq1 ineq2 =\r
 470   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 471   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 472   let rhs_sum = float_add_hi pp y1_tm y2_tm in\r
 473   let y_tm = (rand o concl) rhs_sum in\r
 474   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 475                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 476                  y_tm, y_var_real] ADD_INEQ_HI in\r
 477     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP rhs_sum th0));;\r
 478 \r
 479 \r
 480 let add_ineq_lo pp ineq1 ineq2 =\r
 481   let x1_tm, y1_tm = dest_le_op (concl ineq1) in\r
 482   let x2_tm, y2_tm = dest_le_op (concl ineq2) in\r
 483   let lhs_sum = float_add_lo pp x1_tm x2_tm in\r
 484   let x_tm = (lhand o concl) lhs_sum in\r
 485   let th0 = INST[x1_tm, x1_var_real; y1_tm, y1_var_real; \r
 486                  x2_tm, x2_var_real; y2_tm, y2_var_real;\r
 487                  x_tm, x_var_real] ADD_INEQ_LO in\r
 488     MY_PROVE_HYP ineq1 (MY_PROVE_HYP ineq2 (MY_PROVE_HYP lhs_sum th0));;\r
 489 \r
 490 \r
 491 end;;\r