floatScript.sml
1(* =========================================================================
2 Useful properties of floating point numbers.
3 ========================================================================= *)
4
5Theory float
6Ancestors
7 pair pred_set prim_rec num arithmetic real ieee
8Libs
9 numLib realSimps RealArith Ho_Rewrite
10
11val _ = ParseExtras.temp_loose_equality()
12val _ = diminish_srw_ss ["RMULCANON", "RMULRELNORM"]
13
14
15(* Compute some constant values *)
16
17val () = computeLib.add_funs [realTheory.REAL_INV_1OVER]
18val EVAL_PROVE = EQT_ELIM o EVAL
19fun EVAL' thms = SIMP_CONV (srw_ss()) thms THENC EVAL
20fun eval thms = rhs o concl o EVAL' thms
21val expw_tm = eval [expwidth, float_format] ``expwidth float_format``
22val fracw_tm = eval [fracwidth, float_format] ``fracwidth float_format``
23val bias_tm = eval [bias, expwidth, float_format] ``bias float_format``
24val emax_tm = eval [emax, expwidth, float_format] ``emax float_format``
25val pemax_tm = eval [] ``^emax_tm - 1``
26val sfracw_tm = eval [] ``^fracw_tm + 1``
27val frac_tm = eval [] ``2 EXP ^fracw_tm``
28val pfrac_tm = eval [] ``&(^frac_tm - 1) : real``
29val exp_pemax_tm = eval [] ``&(2 EXP ^pemax_tm) : real``
30val exp_emaxmfrac_tm = eval [fracwidth, float_format]
31 ``^exp_pemax_tm - &(2 EXP (^pemax_tm - ^fracw_tm))``
32val sbias_tm = eval [] ``^bias_tm + 1``
33val pbias_tm = eval [] ``^bias_tm - 1``
34val ppbias_tm = eval [] ``^pbias_tm - 1``
35val pppbias_tm = eval [] ``^ppbias_tm - 1``
36val bias_frac_tm = eval [] ``^bias_tm + ^fracw_tm``
37
38(* -------------------------------------------------------------------------
39 Useful lemmas.
40 ------------------------------------------------------------------------- *)
41
42Theorem SIGN:
43 !a. sign a = FST a
44Proof
45 gen_tac \\ pairLib.PairCases_on `a` \\ simp [sign]
46QED
47
48Theorem EXPONENT:
49 !a. exponent a = FST (SND a)
50Proof
51 gen_tac \\ pairLib.PairCases_on `a` \\ simp [exponent]
52QED
53
54Theorem FRACTION:
55 !a. fraction a = SND (SND a)
56Proof
57 gen_tac \\ pairLib.PairCases_on `a` \\ simp [fraction]
58QED
59
60Theorem IS_VALID:
61 !X a. is_valid X a =
62 sign a < 2 /\ exponent a < 2 EXP (expwidth X) /\
63 fraction a < 2 EXP (fracwidth X)
64Proof
65 REPEAT gen_tac
66 \\ pairLib.PairCases_on `a`
67 \\ simp [is_valid, sign, exponent, fraction]
68QED
69
70Theorem VALOF:
71 !X a.
72 valof X a =
73 if exponent a = 0 then
74 ~1 pow sign a * (2 / 2 pow bias X) * (&fraction a / 2 pow fracwidth X)
75 else
76 ~1 pow sign a * (2 pow exponent a / 2 pow bias X) *
77 (1 + &fraction a / 2 pow fracwidth X)
78Proof
79 REPEAT gen_tac
80 \\ pairLib.PairCases_on `a`
81 \\ simp [valof, sign, exponent, fraction]
82QED
83
84(*-----------------------*)
85
86Theorem IS_VALID_DEFLOAT:
87 !a. is_valid float_format (defloat a)
88Proof
89 REWRITE_TAC[float_tybij]
90QED
91
92Theorem IS_FINITE_EXPLICIT:
93 !a. is_finite float_format a =
94 sign a < 2 /\ exponent a < ^emax_tm /\ fraction a < ^frac_tm
95Proof
96 gen_tac
97 \\ pairLib.PairCases_on `a`
98 \\ simp [is_valid, is_finite, is_normal, is_denormal, is_zero, exponent, emax,
99 float_format, fraction, expwidth, fracwidth, sign]
100QED
101
102(*-----------------------*)
103
104Theorem FLOAT_CASES:
105 !a. Isnan a \/ Infinity a \/ Isnormal a \/ Isdenormal a \/ Iszero a
106Proof
107 gen_tac
108 \\ mp_tac (Q.SPEC `a:float` IS_VALID_DEFLOAT)
109 \\ rw [Isnan, Infinity, Isnormal, Isdenormal, Iszero,
110 is_nan, is_infinity, is_normal, is_denormal, is_zero, IS_VALID, emax]
111QED
112
113Theorem FLOAT_CASES_FINITE:
114 !a. Isnan a \/ Infinity a \/ Finite a
115Proof
116 rewrite_tac [FLOAT_CASES, Finite]
117QED
118
119(*-----------------------*)
120
121Theorem FLOAT_DISTINCT:
122 !a. ~(Isnan a /\ Infinity a) /\
123 ~(Isnan a /\ Isnormal a) /\
124 ~(Isnan a /\ Isdenormal a) /\
125 ~(Isnan a /\ Iszero a) /\
126 ~(Infinity a /\ Isnormal a) /\
127 ~(Infinity a /\ Isdenormal a) /\
128 ~(Infinity a /\ Iszero a) /\
129 ~(Isnormal a /\ Isdenormal a) /\
130 ~(Isnormal a /\ Iszero a) /\
131 ~(Isdenormal a /\ Iszero a)
132Proof
133 rw [Isnan, Infinity, Isnormal, Isdenormal, Iszero,
134 is_nan, is_infinity, is_normal, is_denormal, is_zero,
135 float_format, emax, expwidth, exponent, fraction]
136QED
137
138Theorem FLOAT_DISTINCT_FINITE:
139 !a. ~(Isnan a /\ Infinity a) /\ ~(Isnan a /\ Finite a) /\
140 ~(Infinity a /\ Finite a)
141Proof
142 prove_tac [FLOAT_DISTINCT, Finite]
143QED
144
145(*-----------------------*)
146
147Theorem FLOAT_INFINITIES_SIGNED:
148 (sign (defloat Plus_infinity) = 0) /\ (sign (defloat Minus_infinity) = 1)
149Proof
150 `(defloat (float (plus_infinity float_format)) =
151 plus_infinity float_format) /\
152 (defloat(float(minus_infinity float_format)) =
153 minus_infinity float_format)`
154 by simp [GSYM float_tybij, is_valid, plus_infinity, minus_infinity,
155 float_format, emax, fracwidth, expwidth]
156 \\ fs [Plus_infinity, Minus_infinity, sign, plus_infinity, minus_infinity]
157QED
158
159Theorem INFINITY_IS_INFINITY:
160 Infinity Plus_infinity /\ Infinity Minus_infinity
161Proof
162 `(defloat (float (plus_infinity float_format)) =
163 plus_infinity float_format) /\
164 (defloat (float (minus_infinity float_format)) =
165 minus_infinity float_format)`
166 by simp [GSYM float_tybij, is_valid, plus_infinity, minus_infinity,
167 float_format, emax, fracwidth, expwidth]
168 \\ fs [Infinity, Plus_infinity, Minus_infinity, is_infinity, plus_infinity,
169 minus_infinity, exponent, fraction]
170QED
171
172Theorem ZERO_IS_ZERO:
173 Iszero Plus_zero /\ Iszero Minus_zero
174Proof
175 `(defloat (float (plus_zero float_format)) = plus_zero float_format) /\
176 (defloat (float (minus_zero float_format)) = minus_zero float_format)`
177 by simp [GSYM float_tybij, is_valid, plus_zero, minus_zero, float_format,
178 emax, fracwidth, expwidth]
179 \\ fs [Iszero, Plus_zero, Minus_zero, is_zero, plus_zero, minus_zero,
180 exponent, fraction]
181QED
182
183(*-----------------------*)
184
185Theorem INFINITY_NOT_NAN:
186 ~Isnan Plus_infinity /\ ~Isnan Minus_infinity
187Proof
188 PROVE_TAC [INFINITY_IS_INFINITY, FLOAT_DISTINCT_FINITE]
189QED
190
191Theorem ZERO_NOT_NAN:
192 ~Isnan Plus_zero /\ ~Isnan Minus_zero
193Proof
194 PROVE_TAC [ZERO_IS_ZERO, FLOAT_DISTINCT]
195QED
196
197(*-----------------------*)
198
199Theorem FLOAT_INFINITIES:
200 !a. Infinity a = (a == Plus_infinity) \/ (a == Minus_infinity)
201Proof
202 gen_tac
203 \\ strip_assume_tac (Q.SPEC `a:float` FLOAT_CASES_FINITE)
204 >- (`~Infinity a` by prove_tac [FLOAT_DISTINCT_FINITE]
205 \\ fs [Isnan, Infinity, fcompare, feq, float_eq])
206 >- (`~Isnan a` by prove_tac [FLOAT_DISTINCT_FINITE]
207 \\ fs [Isnan, Infinity, fcompare, feq, float_eq,
208 REWRITE_RULE [Isnan] INFINITY_NOT_NAN,
209 REWRITE_RULE [Infinity] INFINITY_IS_INFINITY,
210 FLOAT_INFINITIES_SIGNED]
211 \\ rw []
212 \\ metis_tac [IS_VALID_DEFLOAT, IS_VALID,
213 DECIDE ``a < 2n ==> (a = 0) \/ (a = 1)``])
214 \\ `~Infinity a /\ ~Isnan a` by prove_tac [FLOAT_DISTINCT_FINITE]
215 \\ fs [Isnan, Infinity, fcompare, feq, float_eq,
216 REWRITE_RULE [Isnan] INFINITY_NOT_NAN,
217 REWRITE_RULE [Infinity] INFINITY_IS_INFINITY,
218 FLOAT_INFINITIES_SIGNED]
219QED
220
221Theorem FLOAT_INFINITES_DISTINCT:
222 !a. ~(a == Plus_infinity /\ a == Minus_infinity)
223Proof
224 rw [Plus_infinity, Minus_infinity, feq, float_eq, fcompare]
225 \\ fs [REWRITE_RULE [Plus_infinity, Minus_infinity] FLOAT_INFINITIES_SIGNED,
226 REWRITE_RULE [Infinity, Plus_infinity, Minus_infinity]
227 INFINITY_IS_INFINITY,
228 REWRITE_RULE [Isnan, Plus_infinity, Minus_infinity] INFINITY_NOT_NAN]
229QED
230
231(* ------------------------------------------------------------------------- *)
232(* Lifting of the nonexceptional comparison operations. *)
233(* ------------------------------------------------------------------------- *)
234
235val FLOAT_LIFT_TAC =
236 REPEAT strip_tac
237 \\ `~Isnan a /\ ~Infinity a /\ ~Isnan b /\ ~Infinity b`
238 by prove_tac [FLOAT_DISTINCT_FINITE]
239 \\ fs [Finite, Isnan, Infinity, Isnormal, Isdenormal, Iszero,
240 float_lt, flt, float_gt, fgt, float_le, fle, float_ge, fge,
241 float_eq, feq, fcompare, Val, real_gt, real_ge, GSYM REAL_NOT_LT]
242 \\ REPEAT COND_CASES_TAC
243 \\ fs []
244 \\ prove_tac [REAL_LT_ANTISYM, REAL_LT_TOTAL]
245
246
247Theorem FLOAT_LT:
248 !a b. Finite a /\ Finite b ==> (a < b = Val a < Val b)
249Proof FLOAT_LIFT_TAC
250QED
251
252Theorem FLOAT_GT:
253 !a b. Finite a /\ Finite b ==> (a > b = Val a > Val b)
254Proof FLOAT_LIFT_TAC
255QED
256
257Theorem FLOAT_LE:
258 !a b. Finite a /\ Finite b ==> (a <= b = Val a <= Val b)
259Proof FLOAT_LIFT_TAC
260QED
261
262Theorem FLOAT_GE:
263 !a b. Finite a /\ Finite b ==> (a >= b = Val a >= Val b)
264Proof FLOAT_LIFT_TAC
265QED
266
267Theorem FLOAT_EQ:
268 !a b. Finite a /\ Finite b ==> (a == b = (Val a = Val b))
269Proof FLOAT_LIFT_TAC
270QED
271
272Theorem FLOAT_EQ_REFL:
273 !a. (a == a) = ~Isnan a
274Proof rw [float_eq, feq, fcompare, Isnan]
275QED
276
277(* ------------------------------------------------------------------------- *)
278(* Various lemmas. *)
279(* ------------------------------------------------------------------------- *)
280
281Theorem IS_VALID_SPECIAL:
282 !X. is_valid X (minus_infinity X) /\ is_valid X (plus_infinity X) /\
283 is_valid X (topfloat X) /\ is_valid X (bottomfloat X) /\
284 is_valid X (plus_zero X) /\ is_valid X (minus_zero X)
285Proof
286 simp [is_valid, minus_infinity, plus_infinity, plus_zero, minus_zero,
287 topfloat, bottomfloat, emax]
288QED
289
290(*-------------------------------------------------------*)
291
292Theorem IS_CLOSEST_EXISTS:
293 !v x s. FINITE s ==> s <> EMPTY ==> ?a:num#num#num. is_closest v s x a
294Proof
295 gen_tac
296 \\ gen_tac
297 \\ HO_MATCH_MP_TAC FINITE_INDUCT
298 \\ simp [NOT_INSERT_EMPTY]
299 \\ gen_tac
300 \\ Cases_on `s = EMPTY`
301 >- simp [is_closest]
302 \\ Cases_on `FINITE s`
303 \\ rw []
304 \\ Cases_on `abs (v a - x) <= abs (v e - x)`
305 \\ fs [is_closest]
306 >- (qexists_tac `a` \\ rw [] \\ simp [])
307 \\ qexists_tac `e`
308 \\ rw []
309 >- simp []
310 \\ qpat_x_assum `!b:num#num#num. P` (qspec_then `b` mp_tac)
311 \\ qpat_x_assum `~(abs (v a - x) <= abs (v e - x))` mp_tac
312 \\ simp []
313 \\ REAL_ARITH_TAC
314QED
315
316Theorem CLOSEST_IS_EVERYTHING:
317 !v p s x.
318 FINITE s ==> s <> EMPTY ==>
319 is_closest v s x (closest v p s x) /\
320 ((?b:num#num#num. is_closest v s x b /\ p b) ==> p (closest v p s x))
321Proof
322 rw [closest]
323 \\ SELECT_ELIM_TAC
324 \\ prove_tac [IS_CLOSEST_EXISTS]
325QED
326
327Theorem CLOSEST_IN_SET:
328 !v p x s:(num#num#num) set.
329 FINITE s ==> s <> EMPTY ==> (closest v p s x) IN s
330Proof
331 prove_tac [CLOSEST_IS_EVERYTHING, is_closest]
332QED
333
334
335Theorem CLOSEST_IS_CLOSEST:
336 !v p x s:(num#num#num) set.
337 FINITE s ==> s <> EMPTY ==> is_closest v s x (closest v p s x)
338Proof
339 prove_tac [CLOSEST_IS_EVERYTHING]
340QED
341
342(*-------------------------------------------------------*)
343
344Theorem FLOAT_FIRSTCROSS[local]:
345 !m n p.
346 {a: num # num # num | FST a < m /\ FST (SND a) < n /\ SND (SND a) < p} =
347 IMAGE (\(x,(y,z)). (x,y,z))
348 ({x | x < m} CROSS ({y | y < n} CROSS {z | z < p}))
349Proof
350 rw [EXTENSION]
351 \\ pairLib.PairCases_on `x`
352 \\ simp []
353 \\ eq_tac
354 \\ rw []
355 >- (qexists_tac `(x0, x1, x2)` \\ fs [])
356 \\ pairLib.PairCases_on `x'`
357 \\ fs []
358QED
359
360Theorem FLOAT_COUNTINDUCT[local]:
361 !n. ({x | x < 0n} = EMPTY) /\ ({x | x < SUC n} = n INSERT {x | x < n})
362Proof
363 rw [EXTENSION]
364QED
365
366Theorem FLOAT_FINITECOUNT[local]:
367 !n:num. FINITE {x | x < n}
368Proof
369 Induct \\ rw [FLOAT_COUNTINDUCT]
370QED
371
372Theorem FINITE_R3[local]:
373 !m n p.
374 FINITE {a: num # num # num |
375 FST a < m /\ FST (SND a) < n /\ SND (SND a) < p}
376Proof
377 rw [FLOAT_FIRSTCROSS, IMAGE_FINITE, FLOAT_FIRSTCROSS, FLOAT_FINITECOUNT]
378QED
379
380Theorem IS_VALID_FINITE:
381 FINITE {a:num#num#num | is_valid (X:num#num) a}
382Proof
383 rewrite_tac [IS_VALID, SIGN, EXPONENT, FRACTION, FINITE_R3]
384QED
385
386(*-------------------------------------------------------*)
387
388Theorem FLOAT_IS_FINITE_SUBSET[local]:
389 !X. {a | is_finite X a} SUBSET {a | is_valid X a}
390Proof
391 rw [is_finite, SUBSET_DEF]
392QED
393
394Theorem MATCH_FLOAT_FINITE[local]:
395 !X. {a | is_finite X a} SUBSET {a | is_valid X a} ==>
396 FINITE {a | is_finite X a}
397Proof
398 metis_tac [SUBSET_FINITE, IS_VALID_FINITE]
399QED
400
401Theorem IS_FINITE_FINITE:
402 !X. FINITE {a | is_finite X a}
403Proof
404 metis_tac [MATCH_FLOAT_FINITE, FLOAT_IS_FINITE_SUBSET]
405QED
406
407(*-----------------------*)
408
409Theorem IS_VALID_NONEMPTY:
410 {a | is_valid X a} <> EMPTY
411Proof
412 rw [EXTENSION]
413 \\ qexists_tac `(0,0,0)`
414 \\ rw [is_valid]
415QED
416
417Theorem IS_FINITE_NONEMPTY:
418 {a | is_finite X a} <> EMPTY
419Proof
420 rw [EXTENSION]
421 \\ qexists_tac `(0,0,0)`
422 \\ rw [is_finite, is_valid, is_zero, exponent, fraction]
423QED
424
425(*-----------------------*)
426
427Theorem IS_FINITE_CLOSEST:
428 !X v p x. is_finite X (closest v p {a | is_finite X a} x)
429Proof
430 REPEAT gen_tac
431 \\ `closest v p {a | is_finite X a} x IN {a | is_finite X a}`
432 by metis_tac [CLOSEST_IN_SET, IS_FINITE_FINITE, IS_FINITE_NONEMPTY]
433 \\ fs []
434QED
435
436Theorem IS_VALID_CLOSEST:
437 !X v p x. is_valid X (closest v p {a | is_finite X a} x)
438Proof
439 metis_tac [IS_FINITE_CLOSEST, is_finite]
440QED
441
442(*-----------------------*)
443
444Theorem IS_VALID_ROUND:
445 !X x. is_valid X (round X To_nearest x)
446Proof
447 rw [is_valid, round_def, IS_VALID_SPECIAL, IS_VALID_CLOSEST]
448QED
449
450(*-----------------------*)
451
452Theorem DEFLOAT_FLOAT_ROUND:
453 !x. defloat (float (round float_format To_nearest x)) =
454 round float_format To_nearest x
455Proof
456 rewrite_tac [GSYM float_tybij, IS_VALID_ROUND]
457QED
458
459(*-----------------------*)
460
461Theorem DEFLOAT_FLOAT_ZEROSIGN_ROUND:
462 !x b. defloat (float (zerosign float_format b
463 (round float_format To_nearest x))) =
464 zerosign float_format b (round float_format To_nearest x)
465Proof
466 rw [GSYM float_tybij, zerosign, IS_VALID_ROUND, IS_VALID_SPECIAL]
467QED
468
469(*-----------------------*)
470
471Theorem VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND:
472 !x b. valof float_format
473 (defloat (float (zerosign float_format b
474 (round float_format To_nearest x)))) =
475 valof float_format (round float_format To_nearest x)
476Proof
477 rw [DEFLOAT_FLOAT_ZEROSIGN_ROUND, zerosign, minus_zero, plus_zero]
478 \\ `?p q r. round float_format To_nearest x = (p, q, r)`
479 by metis_tac [pairTheory.pair_CASES]
480 \\ fs [is_zero, exponent, fraction, valof]
481QED
482
483(*--------------------------------------------------------------*)
484
485Theorem ISFINITE:
486 !a. Finite a = is_finite float_format (defloat a)
487Proof
488 rewrite_tac [Finite, is_finite, Isnormal, Isdenormal, Iszero, float_tybij]
489QED
490
491(*--------------------------------------*)
492
493Theorem REAL_ABS_INV[local]:
494 !x. abs (inv x) = inv (abs x)
495Proof
496 gen_tac
497 \\ Cases_on `x = 0r`
498 \\ simp [REAL_INV_0, REAL_ABS_0, ABS_INV]
499QED
500
501Theorem REAL_ABS_DIV[local]:
502 !x y. abs (x / y) = abs x / abs y
503Proof
504 rewrite_tac [real_div, REAL_ABS_INV, REAL_ABS_MUL]
505QED
506
507Theorem REAL_POW_LE_1[local]:
508 !n x. 1r <= x ==> 1 <= x pow n
509Proof
510 Induct
511 \\ rw [pow]
512 \\ GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID]
513 \\ match_mp_tac REAL_LE_MUL2
514 \\ simp []
515QED
516
517Theorem REAL_POW_MONO[local] = realTheory.REAL_POW_MONO
518
519Theorem VAL_FINITE:
520 !a. Finite a ==> abs (Val a) <= largest float_format
521Proof
522 rw [Val, VALOF, ISFINITE, IS_FINITE_EXPLICIT, float_format, fracwidth, bias,
523 emax, expwidth, largest, GSYM POW_ABS, REAL_ABS_MUL, REAL_ABS_DIV,
524 ABS_NEG, ABS_N, POW_ONE, realTheory.mult_rat]
525 \\ EVAL_TAC
526 >- simp [realTheory.REAL_LE_LDIV_EQ]
527 \\ `exponent (defloat a) <= ^pemax_tm /\ 1r <= 2 /\
528 0r <= &fraction (defloat a) / &^frac_tm /\
529 &fraction (defloat a) / &^frac_tm <=
530 1 + &fraction (defloat a) / &^frac_tm`
531 by simp [realTheory.REAL_LE_DIV, realTheory.REAL_LE_ADDL]
532 \\ `2 pow exponent (defloat a) <= 2 pow ^pemax_tm /\
533 (abs (1 + &fraction (defloat a) / &^frac_tm) =
534 1 + &fraction (defloat a) / &^frac_tm)`
535 by prove_tac [realTheory.REAL_LE_TRANS, ABS_REFL, REAL_POW_MONO]
536 \\ simp [realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_LDISTRIB,
537 ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] realTheory.mult_ratr]
538 \\ SUBST1_TAC (GSYM (EVAL ``^exp_pemax_tm + ^exp_emaxmfrac_tm``))
539 \\ match_mp_tac realTheory.REAL_LE_ADD2
540 \\ fs [realTheory.mult_ratr, realTheory.REAL_LE_LDIV_EQ]
541 \\ SUBST1_TAC (GSYM (EVAL ``^exp_pemax_tm * ^pfrac_tm``))
542 \\ match_mp_tac realTheory.REAL_LE_MUL2
543 \\ fs [realTheory.POW_POS]
544QED
545
546(* ------------------------------------------------------------------------- *)
547(* Explicit numeric value for threshold, to save repeated recalculation. *)
548(* ------------------------------------------------------------------------- *)
549
550Theorem FLOAT_THRESHOLD_EXPLICIT =
551 EVAL' [threshold, float_format, emax, bias, fracwidth, expwidth]
552 ``threshold float_format``
553
554Theorem FLOAT_LARGEST_EXPLICIT =
555 EVAL' [largest, float_format, emax, bias, fracwidth, expwidth]
556 ``largest float_format``
557
558Theorem VAL_THRESHOLD:
559 !a. Finite a ==> abs (Val a) < threshold float_format
560Proof
561 REPEAT strip_tac
562 \\ match_mp_tac REAL_LET_TRANS
563 \\ qexists_tac `largest float_format`
564 \\ simp [VAL_FINITE, FLOAT_THRESHOLD_EXPLICIT, FLOAT_LARGEST_EXPLICIT]
565QED
566
567(* ------------------------------------------------------------------------- *)
568(* Lifting up of rounding (to nearest). *)
569(* ------------------------------------------------------------------------- *)
570
571Definition error:
572 error x = Val (float (round float_format To_nearest x)) - x
573End
574
575(*-----------------------*)
576
577Theorem BOUND_AT_WORST_LEMMA[local]:
578 !a x. abs x < threshold float_format /\ is_finite float_format a ==>
579 abs (valof float_format (round float_format To_nearest x) - x) <=
580 abs (valof float_format a - x)
581Proof
582 rw [round_def, REAL_ARITH ``abs x < y = ~(x <= ~y) /\ ~(x >= y)``]
583 \\ match_mp_tac
584 (IS_FINITE_FINITE
585 |> Q.SPEC `float_format`
586 |> MATCH_MP CLOSEST_IS_CLOSEST
587 |> Q.SPECL [`valof float_format`, `\a. EVEN (fraction a)`, `x`]
588 |> REWRITE_RULE [IS_FINITE_NONEMPTY, is_closest]
589 |> CONJUNCT2)
590 \\ simp []
591QED
592
593Theorem ERROR_AT_WORST_LEMMA[local]:
594 !a x. abs x < threshold float_format /\ Finite a ==>
595 abs (error x) <= abs (Val a - x)
596Proof
597 rewrite_tac [ISFINITE, Val, error, BOUND_AT_WORST_LEMMA, DEFLOAT_FLOAT_ROUND]
598QED
599
600Theorem ERROR_IS_ZERO:
601 !a x. Finite a /\ (Val a = x) ==> (error x = 0)
602Proof
603 rw []
604 \\ match_mp_tac
605 (ERROR_AT_WORST_LEMMA
606 |> Q.SPECL [`a`, `Val a`]
607 |> SIMP_RULE (srw_ss())
608 [REAL_ABS_0, REAL_ARITH ``abs x <= 0 = (x = 0r)``])
609 \\ simp [VAL_THRESHOLD]
610QED
611
612(*--------------------------------------------------------------*)
613
614Theorem ERROR_BOUND_LEMMA1[local]:
615 !x. 0r <= x /\ x < 1 ==>
616 ?n. n < 2n EXP ^fracw_tm /\ &n / 2 pow ^fracw_tm <= x /\
617 x < &(SUC n) / 2 pow ^fracw_tm
618Proof
619 REPEAT strip_tac
620 \\ qspec_then `\n. &n / 2 pow ^fracw_tm <= x` mp_tac EXISTS_GREATEST
621 \\ simp []
622 \\ Lib.W (Lib.C SUBGOAL_THEN (fn th => rewrite_tac [th]) o lhs o lhand o snd)
623 >- (conj_tac
624 >- (qexists_tac `0n` \\ simp [])
625 \\ qexists_tac `^frac_tm`
626 \\ rw [REAL_LE_LDIV_EQ]
627 \\ fs [realTheory.REAL_NOT_LE, realTheory.real_gt,
628 REAL_ARITH ``&^frac_tm < y /\ x < 1 ==> x * &^frac_tm < y``])
629 \\ disch_then (Q.X_CHOOSE_THEN `n` strip_assume_tac)
630 \\ pop_assum (qspec_then `SUC n` assume_tac)
631 \\ qexists_tac `n`
632 \\ fs [REAL_NOT_LE]
633 \\ fs [REAL_LE_LDIV_EQ]
634 \\ `&n < &^frac_tm`
635 by metis_tac
636 [REAL_ARITH ``!n. x < 1 /\ n <= x * &^frac_tm ==> n < &^frac_tm``]
637 \\ fs []
638QED
639
640(*---------------------------*)
641
642Theorem ERROR_BOUND_LEMMA2[local]:
643 !x. 0r <= x /\ x < 1 ==>
644 ?n. n <= 2 EXP ^fracw_tm /\
645 abs (x - &n / 2 pow ^fracw_tm) <= inv (2 pow ^sfracw_tm)
646Proof
647 gen_tac
648 \\ disch_then
649 (fn th => Q.X_CHOOSE_THEN `n` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)
650 (MATCH_MP ERROR_BOUND_LEMMA1 th)
651 \\ strip_assume_tac th)
652 \\ disch_then (mp_tac o Q.SPEC `inv (2 pow ^sfracw_tm)` o MATCH_MP
653 (REAL_ARITH ``!a:real b x d. a <= x /\ x < b ==> b <= a + 2 * d ==>
654 abs (x - a) <= d \/ abs (x - b) <= d``))
655 \\ Lib.W (Lib.C SUBGOAL_THEN
656 (fn th => rewrite_tac [th]) o lhand o lhand o snd)
657 >- (simp [] \\ EVAL_TAC \\ simp [realTheory.REAL_DIV_ADD, ADD1])
658 \\ rw []
659 >- (qexists_tac `n` \\ fs [])
660 \\ qexists_tac `SUC n`
661 \\ fs []
662QED
663
664(*---------------------------*)
665
666Theorem ERROR_BOUND_LEMMA3[local]:
667 !x. 1r <= x /\ x < 2 ==>
668 ?n. n <= 2 EXP ^fracw_tm /\
669 abs ((1 + &n / 2 pow ^fracw_tm) - x) <= inv (2 pow ^sfracw_tm)
670Proof
671 REPEAT strip_tac
672 \\ Q.SUBGOAL_THEN `0r <= x - 1 /\ x - 1 < 1`
673 (assume_tac o MATCH_MP ERROR_BOUND_LEMMA2)
674 >- (NTAC 2 (POP_ASSUM mp_tac) \\ REAL_ARITH_TAC)
675 \\ metis_tac
676 [ABS_NEG, REAL_NEG_SUB, REAL_ARITH ``a - (b - c) = (c + a:real) - b``]
677QED
678
679(*---------------------------*)
680
681Theorem ERROR_BOUND_LEMMA4[local]:
682 !x. 1r <= x /\ x < 2 ==>
683 ?e f. abs (Val (float (0,e,f)) - x) <= inv (2 pow ^sfracw_tm) /\
684 f < 2 EXP ^fracw_tm /\
685 ((e = bias float_format) \/
686 (e = SUC (bias float_format)) /\ (f = 0))
687Proof
688 gen_tac
689 \\ DISCH_TAC
690 \\ first_assum (Q.X_CHOOSE_THEN `n` (MP_TAC o REWRITE_RULE [LESS_OR_EQ]) o
691 MATCH_MP ERROR_BOUND_LEMMA3)
692 \\ strip_tac
693 >- (qexists_tac `bias float_format`
694 \\ qexists_tac `n`
695 \\ `defloat (float (0,bias float_format,n)) = (0,bias float_format,n)`
696 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth,
697 fracwidth]
698 \\ fs [Val, valof, bias, expwidth, fracwidth, float_format])
699 \\ qexists_tac `SUC (bias float_format)`
700 \\ qexists_tac `0`
701 \\ `defloat (float (0,SUC (bias float_format),0)) =
702 (0,SUC (bias float_format),0)`
703 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth, fracwidth]
704 \\ rfs [Val, valof, bias, expwidth, fracwidth, float_format]
705QED
706
707(*---------------------------*)
708
709Theorem ERROR_BOUND_LEMMA5[local]:
710 !x. 1r <= abs x /\ abs x < 2 ==>
711 ?s e f. abs (Val (float (s,e,f)) - x) <= inv (2 pow ^sfracw_tm) /\
712 s < 2 /\ f < 2 EXP ^fracw_tm /\
713 ((e = bias float_format) \/
714 (e = SUC (bias float_format)) /\ (f = 0))
715Proof
716 gen_tac
717 \\ DISCH_TAC
718 \\ SUBGOAL_THEN ``1 <= x /\ x < 2 \/ 1 <= ~x /\ ~x < 2``
719 (DISJ_CASES_THEN
720 (Q.X_CHOOSE_THEN `e` (Q.X_CHOOSE_THEN `f` assume_tac) o
721 MATCH_MP ERROR_BOUND_LEMMA4))
722 >- (pop_assum mp_tac \\ REAL_ARITH_TAC)
723 >| [qexists_tac `0`,
724 qexists_tac `1`
725 \\ `(defloat (float (1,bias float_format,f)) = (1,bias float_format,f)) /\
726 (defloat (float (1,SUC (bias float_format),0)) =
727 (1,SUC (bias float_format),0)) /\
728 (defloat (float (0,bias float_format,f)) = (0,bias float_format,f)) /\
729 (defloat (float (0,SUC (bias float_format),0)) =
730 (0,SUC (bias float_format),0))`
731 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth,
732 fracwidth]
733 ]
734 \\ qexists_tac `e`
735 \\ qexists_tac `f`
736 \\ ntac 2 (fs [Val, valof, bias, expwidth, fracwidth, float_format,
737 REAL_ARITH ``abs (-2 - x) = abs (2 - -x)``,
738 REAL_ARITH ``abs (-1 * y - x) = abs (y - -x)``])
739QED
740
741(*---------------------------*)
742
743val REAL_LE_LCANCEL_IMP =
744 METIS_PROVE [REAL_LE_LMUL] ``!x y z. 0r < x /\ x * y <= x * z ==> y <= z``
745
746Theorem ERROR_BOUND_LEMMA6[local]:
747 !x. 0 <= x /\ x < inv (2 pow ^pbias_tm) ==>
748 ?n. n <= 2 EXP ^fracw_tm /\
749 abs (x - 2 / 2 pow ^bias_tm * &n / 2 pow ^fracw_tm) <=
750 inv (2 pow ^bias_frac_tm)
751Proof
752 REPEAT strip_tac
753 \\ Q.SPEC_THEN `2 pow ^pbias_tm * x` mp_tac ERROR_BOUND_LEMMA2
754 \\ Lib.W (Lib.C SUBGOAL_THEN MP_TAC o lhand o lhand o snd)
755 >- (conj_tac
756 >- (match_mp_tac realTheory.REAL_LE_MUL \\ simp [])
757 \\ pop_assum mp_tac
758 \\ simp [realTheory.REAL_INV_1OVER, realTheory.lt_ratr])
759 \\ DISCH_THEN (fn th => rewrite_tac [th])
760 \\ DISCH_THEN (Q.X_CHOOSE_THEN `n` strip_assume_tac)
761 \\ qexists_tac `n`
762 \\ asm_rewrite_tac []
763 \\ qspec_then `2 pow ^pbias_tm` match_mp_tac REAL_LE_LCANCEL_IMP
764 \\ conj_tac
765 >- EVAL_TAC
766 \\ rewrite_tac
767 [realTheory.ABS_MUL
768 |> GSYM
769 |> Q.SPEC `2 pow ^pbias_tm`
770 |> REWRITE_RULE [EVAL_PROVE ``abs (2 pow ^pbias_tm) = 2 pow ^pbias_tm``]]
771 \\ fs [realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_MUL_ASSOC, real_div]
772 \\ pop_assum mp_tac
773 \\ EVAL_TAC
774 \\ simp []
775QED
776
777(*---------------------------*)
778
779Theorem ERROR_BOUND_LEMMA7[local]:
780 !x. 0 <= x /\ x < inv (2 pow ^pbias_tm) ==>
781 ?e f. abs (Val (float (0,e,f)) - x) <= inv (2 pow ^bias_frac_tm) /\
782 f < 2 EXP ^fracw_tm /\ ((e = 0) \/ (e = 1) /\ (f = 0))
783Proof
784 gen_tac
785 \\ DISCH_TAC
786 \\ FIRST_ASSUM (Q.X_CHOOSE_THEN `n` MP_TAC o MATCH_MP ERROR_BOUND_LEMMA6)
787 \\ DISCH_THEN (CONJUNCTS_THEN2 (strip_assume_tac o REWRITE_RULE [LESS_OR_EQ])
788 ASSUME_TAC)
789 >- (qexists_tac `0`
790 \\ qexists_tac `n`
791 \\ `defloat (float (0,0,n)) = (0,0,n)`
792 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth,
793 fracwidth]
794 \\ fs [Val, valof, bias, expwidth, fracwidth, float_format]
795 \\ simp [Once realTheory.ABS_SUB]
796 \\ fs [realTheory.mult_rat, realTheory.mult_ratl,
797 Once realTheory.div_ratl])
798 \\ qexists_tac `1`
799 \\ qexists_tac `0`
800 \\ `defloat (float (0,1,0)) = (0,1,0)`
801 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth, fracwidth]
802 \\ fs [Val, valof, bias, expwidth, fracwidth, float_format]
803 \\ simp [Once realTheory.ABS_SUB]
804 \\ rfs [realTheory.mult_rat, realTheory.mult_ratl, Once realTheory.div_ratl]
805QED
806
807(*---------------------------*)
808
809Theorem ERROR_BOUND_LEMMA8[local]:
810 !x. abs x < inv (2 pow ^pbias_tm) ==>
811 ?s e f. abs (Val (float(s,e,f)) - x) <= inv (2 pow ^bias_frac_tm) /\
812 s < 2 /\ f < 2 EXP ^fracw_tm /\ ((e = 0) \/ (e = 1) /\ (f = 0))
813Proof
814 gen_tac
815 \\ DISCH_TAC
816 \\ SUBGOAL_THEN ``0 <= x /\ x < inv (2 pow ^pbias_tm) \/
817 0 <= ~x /\ ~x < inv (2 pow ^pbias_tm)``
818 (DISJ_CASES_THEN
819 (Q.X_CHOOSE_THEN `e` (Q.X_CHOOSE_THEN `f` assume_tac) o
820 MATCH_MP ERROR_BOUND_LEMMA7))
821 >- (pop_assum mp_tac \\ REAL_ARITH_TAC)
822 \\ `(defloat (float (0,0,f)) = (0,0,f)) /\
823 (defloat (float (0,e,f)) = (0,e,f)) /\
824 (defloat (float (0,1,0)) = (0,1,0)) /\
825 (defloat (float (1,0,f)) = (1,0,f)) /\
826 (defloat (float (1,1,0)) = (1,1,0))`
827 by fs [GSYM float_tybij, is_valid, float_format, bias, expwidth, fracwidth]
828 >| [qexists_tac `0`, qexists_tac `1`]
829 \\ qexists_tac `e`
830 \\ qexists_tac `f`
831 \\ ntac 2
832 (fs [Val, valof, bias, expwidth, fracwidth, float_format,
833 REAL_MUL_ASSOC, REAL_ARITH ``abs (y - -x) = abs (-1 * y - x)``])
834QED
835
836(*---------------------------*)
837
838Theorem VALOF_SCALE_UP[local]:
839 !s e k f.
840 e <> 0 ==>
841 (valof float_format (s,e + k,f) = 2 pow k * valof float_format (s,e,f))
842Proof
843 simp [valof, REAL_POW_ADD, real_div, AC REAL_MUL_ASSOC REAL_MUL_COMM]
844QED
845
846Theorem VALOF_SCALE_DOWN[local]:
847 !s e k f.
848 k < e ==> (valof float_format (s,e - k,f) =
849 inv (2 pow k) * valof float_format (s,e,f))
850Proof
851 REPEAT strip_tac
852 \\ `e - k <> 0 /\ (e = (e - k) + k)` by decide_tac
853 \\ pop_assum (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th])))
854 \\ simp [VALOF_SCALE_UP, REAL_MUL_ASSOC, REAL_MUL_LINV, POW_NZ]
855QED
856
857(*---------------------------*)
858
859Theorem ISFINITE_LEMMA[local]:
860 !s e f. s < 2 /\ e < ^emax_tm /\ f < 2 EXP ^fracw_tm ==>
861 Finite (float (s,e,f)) /\ is_valid float_format (s,e,f)
862Proof
863 NTAC 4 strip_tac
864 \\ `defloat (float (s,e,f)) = (s,e,f)`
865 by fs [GSYM float_tybij, is_valid, float_format, expwidth, fracwidth]
866 \\ fs [ISFINITE, IS_FINITE_EXPLICIT, is_valid, fraction, exponent, sign,
867 float_format, expwidth, fracwidth]
868QED
869
870Theorem ERROR_BOUND_BIG1[local]:
871 !x k. 2 pow k <= abs x /\ abs x < 2 pow SUC k /\
872 abs x < threshold float_format ==>
873 ?a. Finite a /\ abs (Val a - x) <= 2 pow k / 2 pow ^sfracw_tm
874Proof
875 REPEAT strip_tac
876 \\ qspec_then `x / 2 pow k` mp_tac ERROR_BOUND_LEMMA5
877 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhand o lhand o snd)
878 >- (simp [ABS_DIV, GSYM realTheory.POW_ABS, ABS_N, POW_NZ, REAL_POW_LT,
879 REAL_LT_LDIV_EQ, GSYM (CONJUNCT2 pow)]
880 \\ match_mp_tac realTheory.REAL_LE_RDIV
881 \\ simp [realTheory.REAL_POW_LT])
882 \\ DISCH_THEN (fn th => rewrite_tac [th])
883 \\ `2 pow k < threshold float_format` by metis_tac [REAL_LET_TRANS]
884 \\ `k < ^sbias_tm`
885 by (spose_not_then (assume_tac o REWRITE_RULE [NOT_LESS])
886 \\ `2r pow ^sbias_tm <= 2 pow k`
887 by (match_mp_tac REAL_POW_MONO \\ simp [])
888 \\ `2r pow ^sbias_tm < threshold float_format`
889 by metis_tac [REAL_LET_TRANS]
890 \\ pop_assum mp_tac
891 \\ simp [threshold, float_format, emax, bias, expwidth, fracwidth]
892 \\ EVAL_TAC)
893 \\ strip_tac
894 >| [all_tac,
895 Cases_on `k = ^bias_tm`
896 >- (`defloat (float (s,^sbias_tm,0)) = (s,^sbias_tm,0)`
897 by simp [GSYM float_tybij, is_valid, expwidth, fracwidth,
898 float_format, bias]
899 \\ spose_not_then kall_tac
900 \\ qpat_x_assum `abs xx <= inv (2 pow ^sfracw_tm)`
901 (mp_tac o (MATCH_MP (REAL_ARITH
902 ``abs (a - b) <= c ==> abs(a) <= abs(b) + c``)))
903 \\ Q.UNDISCH_TAC `abs x < threshold float_format`
904 \\ simp [threshold, float_format, emax, bias, expwidth, fracwidth,
905 Val, valof, REAL_ABS_MUL, GSYM POW_ABS, ABS_NEG, ABS_DIV,
906 ABS_N, POW_ONE, lt_ratl, REAL_NOT_LE, REAL_LT_ADD_SUB])
907 \\ `e + k < ^emax_tm`
908 by fs [threshold, float_format, emax, bias, expwidth, fracwidth]
909 ]
910 \\ (qexists_tac `float (s,e + k,f)`
911 \\ `Finite (float (s,e + k,f)) /\ is_valid float_format (s,e + k,f)`
912 by (match_mp_tac ISFINITE_LEMMA \\ simp [bias, float_format, expwidth])
913 \\ conj_tac >- asm_rewrite_tac []
914 \\ rewrite_tac [Val]
915 \\ first_assum (SUBST1_TAC o REWRITE_RULE [float_tybij])
916 \\ SUBGOAL_THEN ``e <> 0n``
917 (fn th => rewrite_tac [MATCH_MP VALOF_SCALE_UP th])
918 >- simp [float_format, bias, expwidth, fracwidth]
919 \\ match_mp_tac REAL_LE_LCANCEL_IMP
920 \\ qexists_tac `inv (2 pow k)`
921 \\ conj_tac
922 >- simp [REAL_LT_INV_EQ, REAL_POW_LT]
923 \\ `!x. inv (2 pow k) * abs x = abs (inv (2 pow k) * x)`
924 by rewrite_tac
925 [REAL_ABS_MUL, REAL_ABS_INV, GSYM realTheory.POW_ABS, ABS_N]
926 \\ `defloat (float (s,e,f)) = (s,e,f)`
927 by fs [GSYM float_tybij, is_valid, expwidth, fracwidth, float_format,
928 bias]
929 \\ qpat_x_assum `zz <= inv (2 pow ^sfracw_tm)` mp_tac
930 \\ simp [REAL_SUB_LDISTRIB, REAL_MUL_ASSOC, real_div, POW_NZ,
931 REAL_MUL_LINV, Val]
932 \\ simp [AC REAL_MUL_COMM REAL_MUL_ASSOC]
933 )
934QED
935
936Theorem ERROR_BOUND_BIG[local]:
937 !k x. 2 pow k <= abs x /\ abs x < 2 pow (SUC k) /\
938 abs x < threshold float_format ==>
939 abs (error x) <= 2 pow k / 2 pow ^sfracw_tm
940Proof
941 prove_tac [ERROR_BOUND_BIG1, ERROR_AT_WORST_LEMMA, REAL_LE_TRANS]
942QED
943
944(*-----------------------------------------------*)
945
946Theorem ERROR_BOUND_SMALL1[local]:
947 !x k. inv (2 pow SUC k) <= abs x /\ abs x < inv (2 pow k) /\
948 k < ^pbias_tm ==>
949 ?a. Finite a /\
950 abs (Val a - x) <= inv (2 pow SUC k * 2 pow ^sfracw_tm)
951Proof
952 REPEAT strip_tac
953 \\ qspec_then `x * 2 pow (SUC k)` mp_tac ERROR_BOUND_LEMMA5
954 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhand o lhand o snd)
955 >- (fs [ABS_MUL, GSYM POW_ABS, REAL_INV_1OVER, REAL_LE_LDIV_EQ,
956 REAL_LT_RDIV_EQ, REAL_POW_LT]
957 \\ simp [pow, REAL_ARITH ``a * (2r * b) < 2 = a * b < 1``])
958 \\ DISCH_THEN (fn th => rewrite_tac [th])
959 \\ DISCH_THEN
960 (Q.X_CHOOSE_THEN `s`
961 (Q.X_CHOOSE_THEN `e`
962 (Q.X_CHOOSE_THEN `f` (REPEAT_TCL CONJUNCTS_THEN assume_tac))))
963 \\ qexists_tac `float (s,e - SUC k,f)`
964 \\ `Finite (float (s,e - SUC k,f)) /\ is_valid float_format (s,e - SUC k,f)`
965 by (match_mp_tac ISFINITE_LEMMA \\ fs [bias, float_format, expwidth])
966 \\ `defloat (float (s,e,f)) = (s,e,f)`
967 by fs [GSYM float_tybij, is_valid, expwidth, fracwidth, float_format, bias]
968 \\ `SUC k < e` by fs [bias, float_format, expwidth]
969 \\ NO_STRIP_FULL_SIMP_TAC std_ss
970 [Val, CONJUNCT2 float_tybij, VALOF_SCALE_DOWN]
971 \\ match_mp_tac REAL_LE_LCANCEL_IMP
972 \\ qexists_tac `2 pow (SUC k)`
973 \\ `!x. 2 pow (SUC k) * abs x = abs (2 pow (SUC k) * x)`
974 by rewrite_tac [REAL_ABS_MUL, REAL_ABS_INV, GSYM POW_ABS, ABS_N]
975 \\ `!a b. 0 < a ==> (a * (inv a * b) = b)`
976 by simp [REAL_MUL_ASSOC, REAL_MUL_RINV, REAL_POS_NZ]
977 \\ simp [REAL_POW_LT, REAL_SUB_LDISTRIB, REAL_POS_NZ, REAL_INV_MUL]
978 \\ NO_STRIP_FULL_SIMP_TAC (srw_ss()) [AC REAL_MUL_ASSOC REAL_MUL_COMM]
979QED
980
981Theorem ERROR_BOUND_SMALL[local]:
982 !k x. inv (2 pow (SUC k)) <= abs x /\ abs x < inv (2 pow k) /\
983 k < ^pbias_tm ==>
984 abs (error x) <= inv (2 pow (SUC k) * 2 pow ^sfracw_tm)
985Proof
986 REPEAT strip_tac
987 \\ `?a. Finite a /\
988 abs (Val a - x) <= inv (2 pow (SUC k) * 2 pow ^sfracw_tm)`
989 by simp [ERROR_BOUND_SMALL1]
990 \\ match_mp_tac REAL_LE_TRANS
991 \\ qexists_tac `abs (Val a - x)`
992 \\ simp []
993 \\ match_mp_tac ERROR_AT_WORST_LEMMA
994 \\ simp []
995 \\ match_mp_tac REAL_LT_TRANS
996 \\ qexists_tac `inv (2 pow k)`
997 \\ simp []
998 \\ match_mp_tac REAL_LET_TRANS
999 \\ qexists_tac `inv 1`
1000 \\ conj_tac
1001 >- (match_mp_tac REAL_LE_INV2 \\ simp [REAL_POW_LE_1])
1002 \\ simp [threshold, float_format, bias, fracwidth, expwidth, emax]
1003 \\ EVAL_TAC
1004QED
1005
1006(*-----------------------------------------------*)
1007
1008Theorem ERROR_BOUND_TINY[local]:
1009 !x. abs x < inv (2 pow ^pbias_tm) ==>
1010 abs (error x) <= inv (2 pow ^bias_frac_tm)
1011Proof
1012 REPEAT strip_tac
1013 \\ `?a. Finite a /\ abs (Val a - x) <= inv (2 pow ^bias_frac_tm)`
1014 by metis_tac [ERROR_BOUND_LEMMA8, ISFINITE_LEMMA, Val,
1015 DECIDE ``0 < ^emax_tm /\ 1 < ^emax_tm``]
1016 \\ match_mp_tac REAL_LE_TRANS
1017 \\ qexists_tac `abs (Val a - x)`
1018 \\ simp []
1019 \\ match_mp_tac ERROR_AT_WORST_LEMMA
1020 \\ asm_rewrite_tac []
1021 \\ match_mp_tac REAL_LT_TRANS
1022 \\ qexists_tac `inv (2 pow ^pbias_tm)`
1023 \\ asm_rewrite_tac []
1024 \\ simp [threshold, float_format, bias, emax, expwidth, fracwidth]
1025 \\ EVAL_TAC
1026QED
1027
1028(* -------------------------------------------------------------------------
1029 Stronger versions not requiring exact location of the interval.
1030 ------------------------------------------------------------------------- *)
1031
1032Theorem ERROR_BOUND_NORM_STRONG:
1033 !x j.
1034 abs x < threshold float_format /\
1035 abs x < 2 pow (SUC j) / 2 pow ^pbias_tm ==>
1036 abs (error x) <= 2 pow j / 2 pow ^bias_frac_tm
1037Proof
1038 gen_tac
1039 \\ Induct
1040 >- (rw_tac std_ss
1041 [pow, POW_1, real_div, REAL_MUL_LID, REAL_MUL_RID,
1042 EVAL_PROVE ``2 * inv (2 pow ^pbias_tm) = inv (2 pow ^ppbias_tm)``]
1043 \\ Cases_on `abs x < inv (2 pow ^pbias_tm)`
1044 >- metis_tac [ERROR_BOUND_TINY]
1045 \\ qspecl_then [`^ppbias_tm`, `x`]
1046 (match_mp_tac o SIMP_RULE std_ss [GSYM REAL_POW_ADD, ADD1])
1047 ERROR_BOUND_SMALL
1048 \\ asm_rewrite_tac [GSYM REAL_NOT_LT])
1049 \\ strip_tac
1050 \\ Cases_on `abs x < 2 pow SUC j / 2 pow ^pbias_tm`
1051 >- (match_mp_tac REAL_LE_TRANS
1052 \\ qexists_tac `2 pow j / 2 pow ^bias_frac_tm`
1053 \\ asm_simp_tac std_ss [real_div, pow]
1054 \\ match_mp_tac realTheory.REAL_LE_RMUL_IMP
1055 \\ simp_tac std_ss [REAL_LE_INV_EQ, POW_POS, REAL_ARITH ``0 <= 2r``,
1056 REAL_ARITH ``0r <= a ==> a <= 2 * a``])
1057 \\ Cases_on `j <= ^pppbias_tm`
1058 >- (`?k. ^pppbias_tm - j = k` by prove_tac []
1059 \\ `inv (2 pow (SUC k + ^sfracw_tm)) = 2 pow SUC j / 2 pow ^bias_frac_tm`
1060 by (`SUC j + (SUC k + ^sfracw_tm) = ^bias_frac_tm` by decide_tac
1061 \\ asm_simp_tac std_ss
1062 [REAL_EQ_RDIV_EQ, REAL_EQ_LDIV_EQ, REAL_POW_LT, REAL_INV_1OVER,
1063 POW_NZ, mult_ratl, REAL_MUL_LID, GSYM POW_ADD,
1064 REAL_ARITH ``0 < 2r /\ 0 <> 2r``])
1065 \\ pop_assum
1066 (fn th =>
1067 qspecl_then [`k`, `x`]
1068 (match_mp_tac o SIMP_RULE std_ss [GSYM REAL_POW_ADD, th])
1069 ERROR_BOUND_SMALL)
1070 \\ full_simp_tac arith_ss [REAL_NOT_LT]
1071 \\ `^pbias_tm = k + SUC (SUC j)` by decide_tac
1072 \\ conj_tac
1073 >- (match_mp_tac REAL_LE_TRANS
1074 \\ qexists_tac `2 pow SUC j / 2 pow ^pbias_tm`
1075 \\ asm_rewrite_tac []
1076 \\ rewrite_tac
1077 [REAL_POW_ADD, pow, real_div,
1078 REAL_ARITH ``a * (b * (c * d)) : real = b * a * (c * d)``]
1079 \\ rewrite_tac [GSYM (CONJUNCT2 pow)]
1080 \\ simp_tac std_ss
1081 [REAL_INV_MUL, POW_NZ, REAL_ARITH ``2 <> 0r``, REAL_MUL_RINV,
1082 REAL_ARITH ``a * (b * c) : real = a * c * b``, REAL_MUL_LID,
1083 REAL_LE_REFL])
1084 \\ match_mp_tac REAL_LTE_TRANS
1085 \\ qexists_tac `2 pow SUC (SUC j) / 2 pow ^pbias_tm`
1086 \\ asm_simp_tac std_ss
1087 [REAL_LE_LDIV_EQ, REAL_POW_LT, REAL_ARITH ``0r < 2``,
1088 REAL_POW_ADD, REAL_MUL_ASSOC, REAL_MUL_LINV, POW_NZ,
1089 REAL_ARITH ``2 <> 0r``, REAL_MUL_LID, REAL_LE_REFL]
1090 )
1091 \\ `?i. j = ^ppbias_tm + i` by (qexists_tac `j - ^ppbias_tm` \\ decide_tac)
1092 \\ assume_tac
1093 (REAL_DIV_RMUL_CANCEL
1094 |> Q.SPECL [`2 pow ^pbias_tm`, `a`, `1`]
1095 |> SIMP_RULE std_ss
1096 [POW_NZ, REAL_ARITH ``2 <> 0r``, REAL_MUL_LID, REAL_OVER1]
1097 |> GEN_ALL)
1098 \\ full_simp_tac arith_ss
1099 [ADD1, POW_ADD, REAL_NOT_LT,
1100 POW_ADD
1101 |> Q.SPECL [`2`, `^pbias_tm`, `^sfracw_tm`]
1102 |> SIMP_RULE std_ss [],
1103 REAL_DIV_RMUL_CANCEL
1104 |> Q.SPEC `2 pow ^pbias_tm`
1105 |> SIMP_RULE std_ss [POW_NZ, REAL_ARITH ``2 <> 0r``]
1106 |> CONV_RULE (PATH_CONV "bblrr" (ONCE_REWRITE_CONV [REAL_MUL_COMM]))]
1107 \\ match_mp_tac ERROR_BOUND_BIG
1108 \\ full_simp_tac std_ss
1109 [POW_ADD |> Q.SPECL [`2`, `1`, `^pbias_tm`] |> SIMP_RULE std_ss [],
1110 REAL_MUL_ASSOC, POW_1,
1111 pow |> CONJUNCT2 |> ONCE_REWRITE_RULE [REAL_MUL_COMM] |> GSYM]
1112QED
1113
1114(* -------------------------------------------------------------------------
1115 "1 + Epsilon" property (relative error bounding).
1116 ------------------------------------------------------------------------- *)
1117
1118Definition normalizes:
1119 normalizes x =
1120 inv (2 pow (bias float_format - 1)) <= abs x /\
1121 abs x < threshold float_format
1122End
1123
1124(* ------------------------------------------------------------------------- *)
1125
1126(* 2 pow (2 EXP ^pbias_tm) is too big to EVAL directly *)
1127Theorem THRESHOLD_MUL_LT[local]:
1128 threshold float_format * 2 pow ^pbias_tm < 2 pow (2 EXP ^pbias_tm)
1129Proof
1130 `2 pow ^pemax_tm * inv (2 pow ^bias_tm) = 2 pow ^bias_tm`
1131 by simp_tac bool_ss
1132 [GSYM (EVAL ``^bias_tm + ^bias_tm``), REAL_POW_ADD, REAL_MUL_RINV,
1133 REAL_MUL_RID, POW_NZ, REAL_ARITH ``2r <> 0``, GSYM REAL_MUL_ASSOC]
1134 \\ asm_simp_tac std_ss
1135 [threshold, float_format, emax, bias, fracwidth, expwidth, real_div]
1136 \\ rewrite_tac
1137 [GSYM REAL_MUL_ASSOC, REAL_SUB_RDISTRIB, REAL_SUB_LDISTRIB,
1138 GSYM pow, GSYM POW_ADD]
1139 \\ rewrite_tac
1140 [DECIDE
1141 ``^pbias_tm = ^sfracw_tm + ^(eval [] ``^pbias_tm - ^sfracw_tm``)``,
1142 REAL_POW_ADD, REAL_ARITH ``a * (b * (c * d)) = a * (b * c) * d : real``]
1143 \\ simp_tac std_ss
1144 [REAL_MUL_LINV, POW_NZ, REAL_ARITH ``2r <> 0``, REAL_MUL_RID,
1145 GSYM REAL_POW_ADD]
1146 \\ match_mp_tac REAL_LT_TRANS
1147 \\ qexists_tac `2 pow ^pemax_tm`
1148 \\ conj_tac >- EVAL_TAC
1149 \\ match_mp_tac REAL_POW_MONO_LT
1150 \\ EVAL_TAC
1151QED
1152
1153(* ------------------------------------------------------------------------- *)
1154
1155Theorem LT_THRESHOLD_LT_POW_INV[local]:
1156 !x. x < threshold (^expw_tm,^fracw_tm) ==>
1157 x < 2 pow (emax (^expw_tm,^fracw_tm) - 1) / 2 pow ^pbias_tm
1158Proof
1159 simp [FLOAT_THRESHOLD_EXPLICIT, emax, expwidth, GSYM float_format]
1160 \\ gen_tac
1161 \\ match_mp_tac (REAL_ARITH ``b < c ==> (a < b ==> a < c : real)``)
1162 \\ EVAL_TAC
1163QED
1164
1165Theorem REAL_POS_IN_BINADE[local]:
1166 !x. normalizes x /\ 0 <= x ==>
1167 ?j. j <= emax float_format - 2 /\ 2 pow j / 2 pow ^pbias_tm <= x /\
1168 x < 2 pow (SUC j) / 2 pow ^pbias_tm
1169Proof
1170 rw_tac arith_ss [normalizes, bias, expwidth, float_format, abs]
1171 \\ qspec_then `\n. 2 pow n / 2 pow ^pbias_tm <= x` mp_tac EXISTS_GREATEST
1172 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhs o lhand o snd)
1173 >- (
1174 conj_tac
1175 >- (qexists_tac `0` \\ asm_simp_tac std_ss [REAL_MUL_LID , pow, real_div])
1176 \\ qexists_tac `2 EXP ^pbias_tm`
1177 \\ Q.X_GEN_TAC `n`
1178 \\ rw_tac bool_ss
1179 [GSYM real_lt, REAL_LT_RDIV_EQ, REAL_POW_LT, REAL_ARITH ``0 < 2r``]
1180 \\ match_mp_tac REAL_LT_TRANS
1181 \\ qexists_tac `2 pow (2 EXP ^pbias_tm)`
1182 \\ conj_tac
1183 >- metis_tac [THRESHOLD_MUL_LT, REAL_LT_RMUL, REAL_LT_TRANS, float_format,
1184 REAL_POW_LT, REAL_ARITH ``0 < 2r``]
1185 \\ match_mp_tac REAL_POW_MONO_LT
1186 \\ asm_simp_tac bool_ss [REAL_ARITH ``1 < 2r``, GSYM GREATER_DEF])
1187 \\ DISCH_THEN (fn th => rewrite_tac [th])
1188 \\ DISCH_THEN
1189 (X_CHOOSE_THEN ``n:num``
1190 (CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o Q.SPEC `SUC n`)))
1191 \\ rw_tac arith_ss [REAL_NOT_LE]
1192 \\ qexists_tac `n`
1193 \\ full_simp_tac std_ss [emax, expwidth]
1194 \\ qpat_x_assum `x < threshold (^expw_tm,^fracw_tm)`
1195 (assume_tac o MATCH_MP LT_THRESHOLD_LT_POW_INV)
1196 \\ `2 pow n / 2 pow ^pbias_tm <
1197 2 pow (emax (^expw_tm,^fracw_tm) - 1) / 2 pow ^pbias_tm`
1198 by metis_tac [REAL_LET_TRANS]
1199 \\ spose_not_then assume_tac
1200 \\ `^pemax_tm <= n` by decide_tac
1201 \\ `2 pow ^pemax_tm <= 2 pow n`
1202 by metis_tac [REAL_POW_MONO, REAL_ARITH ``1 <= 2r``]
1203 \\ full_simp_tac std_ss
1204 [REAL_LT_RDIV, REAL_POW_LT, REAL_ARITH ``0 < 2r``, real_lte,
1205 emax, expwidth]
1206QED
1207
1208Theorem REAL_NEG_IN_BINADE[local]:
1209 !x. normalizes x /\ 0 <= ~x ==>
1210 ?j. j <= emax float_format - 2 /\ 2 pow j / 2 pow ^pbias_tm <= ~x /\
1211 ~x < 2 pow (SUC j) / 2 pow ^pbias_tm
1212Proof
1213 metis_tac [normalizes, ABS_NEG, REAL_POS_IN_BINADE]
1214QED
1215
1216Theorem REAL_IN_BINADE:
1217 !x. normalizes x ==>
1218 ?j. j <= emax float_format - 2 /\ 2 pow j / 2 pow ^pbias_tm <= abs x /\
1219 abs x < 2 pow (SUC j) / 2 pow ^pbias_tm
1220Proof
1221 gen_tac
1222 \\ Cases_on `0 <= x`
1223 \\ asm_simp_tac arith_ss [abs, REAL_NEG_IN_BINADE, REAL_POS_IN_BINADE,
1224 REAL_ARITH ``~(0r <= x) ==> 0 <= ~x``]
1225QED
1226
1227(* ------------------------------------------------------------------------- *)
1228
1229Theorem ERROR_BOUND_NORM_STRONG_NORMALIZE:
1230 !x. normalizes x ==> ?j. abs (error x) <= 2 pow j / 2 pow ^bias_frac_tm
1231Proof
1232 metis_tac [REAL_IN_BINADE, ERROR_BOUND_NORM_STRONG, normalizes]
1233QED
1234
1235(* ------------------------------------------------------------------------- *)
1236
1237Theorem inv_le[local]:
1238 !a b. 0 < a /\ 0 < b ==> (inv a <= inv b = b <= a)
1239Proof
1240 rw [realTheory.REAL_INV_1OVER, realTheory.REAL_LE_LDIV_EQ,
1241 realTheory.mult_ratl, realTheory.REAL_LE_RDIV_EQ]
1242QED
1243
1244Theorem relative_bound_lem[local]:
1245 !x j. x <> 0 ==>
1246 (2 pow j * inv (2 pow ^pbias_tm) <= abs x =
1247 inv (abs x) <= inv (2 pow j * inv (2 pow ^pbias_tm)))
1248Proof
1249 REPEAT strip_tac
1250 \\ match_mp_tac (GSYM inv_le)
1251 \\ asm_simp_tac std_ss [REAL_ARITH ``x <> 0 ==> 0 < abs x``]
1252 \\ match_mp_tac realTheory.REAL_LT_MUL
1253 \\ simp_tac std_ss [realTheory.REAL_POW_LT, realTheory.REAL_LT_INV_EQ,
1254 REAL_ARITH ``0 < 2r``]
1255QED
1256
1257Theorem inv_mul[local]:
1258 !a b. a <> 0 /\ b <> 0 ==> (inv (a * inv b) = b / a)
1259Proof
1260 rw [realTheory.REAL_INV_MUL, realTheory.REAL_INV_NZ, realTheory.REAL_INV_INV]
1261 \\ simp [realTheory.REAL_INV_1OVER, realTheory.mult_ratl]
1262QED
1263
1264Theorem RELATIVE_ERROR_ZERO[local]:
1265 !x. normalizes x /\ (x = 0) ==>
1266 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1267 (Val (float (round float_format To_nearest x)) = x * (1 + e))
1268Proof
1269 rw []
1270 \\ qexists_tac `0`
1271 \\ qspec_then `0`
1272 (fn th => simp [REWRITE_RULE [realTheory.REAL_SUB_RZERO] th])
1273 (GSYM error)
1274 \\ match_mp_tac ERROR_IS_ZERO
1275 \\ qexists_tac `float (0, 0, 0)`
1276 \\ `defloat (float (0, 0, 0)) = (0, 0, 0)`
1277 by simp [GSYM float_tybij, is_valid, float_format, expwidth, fracwidth]
1278 \\ simp [Finite, Iszero, is_zero, exponent, fraction, Val, valof]
1279QED
1280
1281Theorem RELATIVE_ERROR:
1282 !x. normalizes x ==>
1283 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1284 (Val (float (round float_format To_nearest x)) = x * (1 + e))
1285Proof
1286 REPEAT strip_tac
1287 \\ Cases_on `x = 0r` >- metis_tac [RELATIVE_ERROR_ZERO]
1288 \\ `x < 0r \/ 0 < x` by (POP_ASSUM MP_TAC \\ REAL_ARITH_TAC)
1289 \\ (qspec_then `x` mp_tac REAL_IN_BINADE
1290 \\ rw_tac std_ss []
1291 \\ full_simp_tac std_ss [normalizes]
1292 \\ qspecl_then [`x`,`j`] MP_TAC ERROR_BOUND_NORM_STRONG
1293 \\ rw_tac std_ss []
1294 \\ `2 pow j * inv (2 pow ^pbias_tm) <= abs x =
1295 inv (abs x) <= inv (2 pow j * inv (2 pow ^pbias_tm))`
1296 by metis_tac [relative_bound_lem]
1297 \\ Q.UNDISCH_TAC `2 pow j / 2 pow ^pbias_tm <= abs x`
1298 \\ asm_simp_tac std_ss [real_div]
1299 \\ rw_tac std_ss []
1300 \\ `0 <= inv (abs x)` by simp [REAL_LE_INV_EQ, ABS_POS]
1301 \\ qspec_then `(error x):real` assume_tac ABS_POS
1302 \\ qspecl_then
1303 [`abs (error x)`, `2 pow j / 2 pow ^bias_frac_tm`, `inv (abs x)`,
1304 `inv (2 pow j * inv (2 pow ^pbias_tm))`] mp_tac REAL_LE_MUL2
1305 \\ asm_simp_tac std_ss []
1306 \\ strip_tac
1307 \\ qexists_tac `error x * inv x`
1308 \\ conj_tac
1309 >- (simp_tac std_ss [realTheory.ABS_MUL, realTheory.REAL_MUL_LID]
1310 \\ match_mp_tac realTheory.REAL_LE_TRANS
1311 \\ qexists_tac `2 pow j / 2 pow ^bias_frac_tm *
1312 inv (2 pow j * inv (2 pow ^pbias_tm))`
1313 \\ asm_simp_tac std_ss [realTheory.ABS_INV]
1314 \\ simp_tac std_ss
1315 [inv_mul, realTheory.POW_NZ, REAL_ARITH ``2 <> 0r``,
1316 realTheory.REAL_POS_NZ, realTheory.REAL_INV_NZ,
1317 realTheory.REAL_DIV_OUTER_CANCEL]
1318 \\ EVAL_TAC
1319 )
1320 \\ asm_simp_tac std_ss
1321 [error, REAL_LDISTRIB, REAL_MUL_RID, REAL_MUL_RINV,
1322 REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_MUL_LID, REAL_SUB_ADD2,
1323 REAL_ARITH ``x * (Val qq * inv x) = (x * inv x) * Val qq``])
1324QED
1325
1326(* -------------------------------------------------------------------------
1327 We also want to ensure that the result is actually finite!
1328 ------------------------------------------------------------------------- *)
1329
1330Theorem DEFLOAT_FLOAT_ZEROSIGN_ROUND_FINITE:
1331 !b x. abs x < threshold float_format ==>
1332 is_finite float_format
1333 (defloat (float (zerosign float_format b
1334 (round float_format To_nearest x))))
1335Proof
1336 rw [round_def, REAL_ARITH ``abs x < y = ~(x <= ~y) /\ ~(x >= y)``]
1337 \\ `is_finite float_format
1338 (zerosign float_format b
1339 (closest (valof float_format) (\a. EVEN (fraction a))
1340 {a | is_finite float_format a} x))`
1341 by (rw [zerosign, IS_FINITE_CLOSEST]
1342 \\ simp [IS_FINITE_EXPLICIT, plus_zero, minus_zero, float_format,
1343 sign, exponent, fraction])
1344 \\ metis_tac [is_finite, float_tybij]
1345QED
1346
1347(* -------------------------------------------------------------------------
1348 Lifting of arithmetic operations.
1349 ------------------------------------------------------------------------- *)
1350
1351Theorem Val_FLOAT_ROUND_VALOF[local]:
1352 !x. Val (float (round float_format To_nearest x)) =
1353 valof float_format (round float_format To_nearest x)
1354Proof
1355 simp [Val, DEFLOAT_FLOAT_ROUND]
1356QED
1357
1358val lift_arith_tac =
1359 REPEAT gen_tac \\ strip_tac
1360 \\ `~Isnan a /\ ~Infinity a /\ ~Isnan b /\ ~Infinity b`
1361 by metis_tac [FLOAT_DISTINCT_FINITE]
1362 \\ imp_res_tac RELATIVE_ERROR
1363 \\ full_simp_tac real_ss
1364 [ISFINITE, Isnan, Infinity, Isnormal, Isdenormal, Iszero, Val, error,
1365 float_add, fadd, float_sub, fsub, float_mul, fmul, float_div, fdiv,
1366 VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND, DEFLOAT_FLOAT_ROUND,
1367 DEFLOAT_FLOAT_ZEROSIGN_ROUND_FINITE, normalizes]
1368 \\ metis_tac [Val_FLOAT_ROUND_VALOF]
1369
1370Theorem FLOAT_ADD:
1371 !a b.
1372 Finite a /\ Finite b /\ abs (Val a + Val b) < threshold float_format ==>
1373 Finite (a + b) /\ (Val (a + b) = Val a + Val b + error (Val a + Val b))
1374Proof
1375 lift_arith_tac
1376QED
1377
1378Theorem FLOAT_SUB:
1379 !a b.
1380 Finite a /\ Finite b /\ abs (Val a - Val b) < threshold float_format ==>
1381 Finite (a - b) /\ (Val (a - b) = Val a - Val b + error (Val a - Val b))
1382Proof
1383 lift_arith_tac
1384QED
1385
1386Theorem FLOAT_MUL:
1387 !a b.
1388 Finite a /\ Finite b /\ abs (Val a * Val b) < threshold float_format ==>
1389 Finite (a * b) /\ (Val (a * b) = Val a * Val b + error (Val a * Val b))
1390Proof
1391 lift_arith_tac
1392QED
1393
1394Theorem FLOAT_DIV:
1395 !a b.
1396 Finite a /\ Finite b /\ ~Iszero b /\
1397 abs (Val a / Val b) < threshold float_format ==>
1398 Finite (a / b) /\ (Val (a / b) = Val a / Val b + error (Val a / Val b))
1399Proof
1400 lift_arith_tac
1401QED
1402
1403(*-----------------------*)
1404
1405val finite_rule =
1406 Q.GENL [`b`, `a`] o
1407 MATCH_MP (DECIDE ``(a /\ b /\ c ==> d /\ e) ==> (a /\ b /\ c ==> d)``) o
1408 Drule.SPEC_ALL
1409
1410Theorem FLOAT_ADD_FINITE = finite_rule FLOAT_ADD
1411Theorem FLOAT_SUB_FINITE = finite_rule FLOAT_SUB
1412Theorem FLOAT_MUL_FINITE = finite_rule FLOAT_MUL
1413
1414(*-----------------------*)
1415
1416Theorem FLOAT_ADD_RELATIVE:
1417 !a b.
1418 Finite a /\ Finite b /\ normalizes (Val a + Val b) ==>
1419 Finite (a + b) /\
1420 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1421 (Val (a + b) = (Val a + Val b) * (1 + e))
1422Proof
1423 lift_arith_tac
1424QED
1425
1426Theorem FLOAT_SUB_RELATIVE:
1427 !a b.
1428 Finite a /\ Finite b /\ normalizes (Val a - Val b) ==>
1429 Finite (a - b) /\
1430 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1431 (Val (a - b) = (Val a - Val b) * (1 + e))
1432Proof
1433 lift_arith_tac
1434QED
1435
1436Theorem FLOAT_MUL_RELATIVE:
1437 !a b.
1438 Finite a /\ Finite b /\ normalizes (Val a * Val b) ==>
1439 Finite (a * b) /\
1440 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1441 (Val (a * b) = (Val a * Val b) * (1 + e))
1442Proof
1443 lift_arith_tac
1444QED
1445
1446Theorem FLOAT_DIV_RELATIVE:
1447 !a b.
1448 Finite a /\ Finite b /\ ~Iszero b /\ normalizes (Val a / Val b) ==>
1449 Finite (a / b) /\
1450 ?e. abs e <= 1 / 2 pow ^sfracw_tm /\
1451 (Val (a / b) = (Val a / Val b) * (1 + e))
1452Proof
1453 lift_arith_tac
1454QED
1455
1456(*---------------------------------------------------------------------------*)