1 (* =========================================================== *)
\r
2 (* Additional floating point procedures *)
\r
3 (* Author: Alexey Solovyev *)
\r
4 (* Date: 2012-10-27 *)
\r
5 (* =========================================================== *)
\r
7 needs "arith/float.hl";;
\r
8 needs "misc/vars.hl";;
\r
10 module More_float = struct
\r
14 open Interval_arith;;
\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
20 (*************************************)
\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
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
39 (* Creates a float term with the value (n * base^e) *)
\r
41 let float_const = `float_num` in
\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
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
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
61 (*********************)
\r
63 let float_F_const = `float_num F`;;
\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
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
78 (***********************************)
\r
81 let FLOAT_EQ_0' = (GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [NUMERAL] o SPEC_ALL)
\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
94 (***********************************)
\r
95 (* float_interval_scale *)
\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
102 (***********************************)
\r
103 (* float_interval_lt0 *)
\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
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
118 (**********************************)
\r
120 let FLOAT_F_POS' = SPEC_ALL FLOAT_F_POS;;
\r
122 (* Returns &0 <= float F n e *)
\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
129 (************************************)
\r
132 let FLOAT_NEG_F' = RULE FLOAT_NEG_T;;
\r
133 let FLOAT_NEG_T' = RULE FLOAT_NEG_F;;
\r
136 let sign, n_tm, e_tm = dest_float tm in
\r
138 INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_T'
\r
140 INST[n_tm, n_var_num; e_tm, e_var_num] FLOAT_NEG_F';;
\r
143 let IABS' = RULE iabs;;
\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
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
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
170 (****************************)
\r
171 (* interval_not_zero *)
\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
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
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
188 (MY_PROVE_HYP gt_th o inst) INTERVAL_NOT_ZERO1'
\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
194 (MY_PROVE_HYP lt_th o inst) INTERVAL_NOT_ZERO2';;
\r
198 (*************************************)
\r
201 let INTERVAL_POS' = (UNDISCH_ALL o prove)
\r
202 (`(&0 < lo <=> T) ==> interval_pos (lo, hi:real)`, SIMP_TAC[interval_pos]);;
\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
211 (MY_PROVE_HYP gt_th o INST[lo, lo_var_real; hi, hi_var_real]) INTERVAL_POS';;
\r
215 (************************************)
\r
216 (* check_interval_iabs *)
\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
226 let th0 = AP_THM (AP_TERM lt_op_real iabs_eq) rhs_tm in
\r
231 (****************************)
\r
234 let INV_EQ_DIV_LEMMA = prove(`&1 / x = inv x`, REWRITE_TAC[real_div; REAL_MUL_LID]);;
\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
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
256 let float_inv2 = rand (concl float_inv2_th);;
\r
257 let inv2_interval = mk_const_interval float_inv2;;
\r
261 (*****************************************)
\r
262 (* bounded_on_int *)
\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
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
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
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
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
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
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
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
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
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
345 (***********************************)
\r
346 (* bounded_on_int arithmetic *)
\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
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
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
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
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
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
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
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
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
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
415 let REAL_LE_REFL' = RULE REAL_LE_REFL in
\r
416 fun tm -> INST[tm, x_var_real] REAL_LE_REFL';;
\r
418 let dest_le_op ineq =
\r
419 let lhs, y_tm = dest_comb ineq in
\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
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
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
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
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
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