lift_ieeeScript.sml
1(* ------------------------------------------------------------------------
2 Some basic properties of IEEE-754 (base 2) floating-point arithmetic
3 ------------------------------------------------------------------------ *)
4Theory lift_ieee
5Ancestors
6 binary_ieee real words[qualified]
7Libs
8 wordsLib realLib realSimps
9
10
11val _ = ParseExtras.temp_loose_equality()
12val _ = diminish_srw_ss ["RMULCANON","RMULRELNORM"]
13
14Overload bias[local] = “words$INT_MAX”
15
16(* ------------------------------------------------------------------------ *)
17
18Definition error_def:
19 error (:'t # 'w) x =
20 float_to_real (round roundTiesToEven x : ('t, 'w) float) - x
21End
22
23Definition normalizes_def:
24 normalizes (:'t # 'w) x =
25 1 < bias (:'w) /\
26 inv (2 pow (bias (:'w) - 1)) <= abs x /\ abs x < threshold (:'t # 'w)
27End
28
29(* ------------------------------------------------------------------------
30 Lifting comparison operations
31 ------------------------------------------------------------------------ *)
32
33Theorem float_lt:
34 !x y. float_is_finite x /\ float_is_finite y ==>
35 (float_less_than x y = float_to_real x < float_to_real y)
36Proof
37 rw [float_less_than_def, float_compare_def, float_is_finite_def,
38 float_value_def]
39 \\ rw []
40QED
41
42Theorem float_le:
43 !x y. float_is_finite x /\ float_is_finite y ==>
44 (float_less_equal x y = float_to_real x <= float_to_real y)
45Proof
46 rw [float_less_equal_def, float_compare_def, float_is_finite_def,
47 float_value_def]
48 \\ rw [realTheory.REAL_LT_IMP_LE,
49 REAL_ARITH ``~(a < b : real) /\ a <> b ==> ~(a <= b)``]
50QED
51
52Theorem float_gt:
53 !x y. float_is_finite x /\ float_is_finite y ==>
54 (float_greater_than x y = float_to_real x > float_to_real y)
55Proof
56 rw [float_greater_than_def, float_compare_def, float_is_finite_def,
57 float_value_def]
58 \\ rw [REAL_ARITH ``a < b : real ==> ~(a > b)``,
59 REAL_ARITH ``~(a < b : real) /\ a <> b ==> a > b``,
60 REAL_ARITH ``~(a > a : real)``]
61QED
62
63Theorem float_ge:
64 !x y. float_is_finite x /\ float_is_finite y ==>
65 (float_greater_equal x y = float_to_real x >= float_to_real y)
66Proof
67 rw [float_greater_equal_def, float_compare_def, float_is_finite_def,
68 float_value_def]
69 \\ rw [REAL_ARITH ``a < b : real ==> ~(a >= b)``,
70 REAL_ARITH ``~(a < b : real) /\ a <> b ==> a >= b``,
71 REAL_ARITH ``a >= a : real``]
72QED
73
74Theorem float_eq:
75 !x y. float_is_finite x /\ float_is_finite y ==>
76 (float_equal x y = (float_to_real x = float_to_real y))
77Proof
78 rw [float_equal_def, float_compare_def, float_is_finite_def,
79 float_value_def]
80 \\ rw [REAL_ARITH ``a < b : real ==> a <> b``]
81QED
82
83Theorem float_eq_refl:
84 !x. float_equal x x = ~float_is_nan x
85Proof
86 rw [float_equal_def, float_is_nan_def, float_compare_def, float_is_finite_def,
87 float_value_def]
88QED
89
90
91(* ------------------------------------------------------------------------
92 Closest
93 ------------------------------------------------------------------------ *)
94
95Theorem closest_is_everything:
96 !p s x. s <> EMPTY ==>
97 is_closest s x (closest_such p s x) /\
98 ((?b. is_closest s x b /\ p b) ==> p (closest_such p s x))
99Proof
100 rw [closest_such_def]
101 \\ SELECT_ELIM_TAC
102 \\ metis_tac [is_closest_exists]
103QED
104
105Theorem closest_in_set:
106 !p s x. s <> EMPTY ==> closest_such p s x IN s
107Proof
108 metis_tac [closest_is_everything, is_closest_def]
109QED
110
111Theorem closest_is_closest:
112 !p s x. s <> EMPTY ==> is_closest s x (closest_such p s x)
113Proof
114 metis_tac [closest_is_everything]
115QED
116
117(* ------------------------------------------------------------------------
118
119 ------------------------------------------------------------------------ *)
120
121Theorem float_finite:
122 FINITE (univ (:('t, 'w) float))
123Proof
124 simp[]
125QED
126
127Theorem is_finite_finite:
128 FINITE {a | float_is_finite a}
129Proof
130 metis_tac [pred_setTheory.SUBSET_FINITE, float_finite,
131 pred_setTheory.SUBSET_UNIV]
132QED
133
134Theorem is_finite_nonempty:
135 {a | float_is_finite a} <> EMPTY
136Proof
137 rw [pred_setTheory.EXTENSION]
138 \\ qexists_tac `float_plus_zero (:'a # 'b)`
139 \\ simp [binary_ieeeTheory.zero_properties]
140QED
141
142Theorem is_finite_closest:
143 !p x. float_is_finite (closest_such p {a | float_is_finite a} x)
144Proof
145 rpt strip_tac
146 \\ `closest_such p {a | float_is_finite a} x IN {a | float_is_finite a}`
147 by metis_tac [closest_in_set, is_finite_finite, is_finite_nonempty]
148 \\ fs []
149QED
150
151(* ------------------------------------------------------------------------
152
153 ------------------------------------------------------------------------ *)
154
155Theorem REAL_ABS_INV[local]:
156 !x. abs (inv x) = inv (abs x)
157Proof
158 gen_tac
159 \\ Cases_on `x = 0r`
160 \\ simp [REAL_INV_0, REAL_ABS_0, ABS_INV]
161QED
162
163Theorem REAL_ABS_DIV[local]:
164 !x y. abs (x / y) = abs x / abs y
165Proof
166 rewrite_tac [real_div, REAL_ABS_INV, REAL_ABS_MUL]
167QED
168
169Theorem REAL_LE_LDIV2[local]:
170 !x y z. 0r < z ==> (x / z <= y / z <=> x <= y)
171Proof
172 simp [REAL_LE_LDIV_EQ, REAL_DIV_RMUL, REAL_POS_NZ]
173QED
174
175Theorem REAL_POW_LE_1[local]:
176 !n x. 1r <= x ==> 1 <= x pow n
177Proof
178 Induct
179 \\ rw [pow]
180 \\ Ho_Rewrite.GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID]
181 \\ match_mp_tac REAL_LE_MUL2
182 \\ simp []
183QED
184
185val REAL_POW_MONO = realTheory.REAL_POW_MONO
186
187Theorem exponent_le[local]:
188 !e : 'a word. e <> -1w ==> (w2n e <= UINT_MAX (:'a) - 1)
189Proof
190 simp_tac std_ss
191 [wordsTheory.WORD_NEG_1, wordsTheory.UINT_MAX_def, wordsTheory.word_T_def]
192 \\ Cases
193 \\ simp []
194QED
195
196Theorem float_to_real_finite:
197 !x : ('t, 'w) float.
198 float_is_finite x ==> (abs (float_to_real x) <= largest (:'t # 'w))
199Proof
200 rw[float_to_real_def, largest_def, ABS_MUL, ABS_INV, GSYM POW_ABS, real_div,
201 wordsTheory.UINT_MAX_def, wordsTheory.dimword_def,
202 SF RMULRELNORM_ss, SF RMULCANON_ss] >>
203 simp[REAL_SUB_LDISTRIB] >>
204 Cases_on ‘x.Significand’ using wordsTheory.ranged_word_nchotomy >>
205 gs[wordsTheory.dimword_def, SF RMULCANON_ss] >>
206 qabbrev_tac ‘X = 2 pow (2 ** dimindex(:'w) - 2)’
207 >- (REWRITE_TAC[GSYM REAL_MUL,
208 REAL_ARITH “2r * (x * y) - y = (2 * x - 1) * y”] >>
209 irule REAL_LE_TRANS >>
210 qexists_tac ‘2 * 2 pow dimindex(:'t) - 1’ >> conj_tac
211 >- simp[REAL_SUB, REAL_OF_NUM_POW] >>
212 simp[REAL_OF_NUM_POW, REAL_SUB, SF RMULRELNORM_ss] >>
213 simp[REAL_OF_NUM_POW, Abbr‘X’]) >>
214 irule (iffLR REAL_LE_LMUL) >> qexists_tac ‘2 pow dimindex (:'t)’ >>
215 REWRITE_TAC [REAL_SUB_LDISTRIB] >>
216 simp[iffRL ABS_REFL, REAL_LE_ADD, REAL_LE_INV_EQ, REAL_LE_MUL] >>
217 simp[REAL_LDISTRIB, REAL_RDISTRIB, SF RMULCANON_ss] >>
218 Cases_on‘x.Exponent’ using wordsTheory.ranged_word_nchotomy >>
219 rename [‘x.Significand = n2w s’, ‘x.Exponent = n2w e’] >> simp[] >>
220 simp[REAL_ARITH “2r * (x * y) - x = x * (2 * y - 1)”] >>
221 gs[wordsTheory.dimword_def]>>
222 simp[REAL_ARITH “x * 2 pow e + y * 2 pow e = 2 pow e * (x + y)”] >>
223 irule REAL_LE_MUL2 >> simp[] >> rpt conj_tac
224 >- (simp[Abbr‘X’, REAL_OF_NUM_POW] >>
225 ‘e <> 2 ** dimindex(:'w) - 1’ suffices_by simp[] >>
226 strip_tac >>
227 gs[float_is_finite_def, float_value_def, wordsTheory.word_2comp_def,
228 wordsTheory.dimword_def] >>
229 Cases_on ‘s = 0’ >> gs[])
230 >- simp[REAL_OF_NUM_POW, REAL_SUB] >>
231 simp[REAL_OF_NUM_POW]
232QED
233
234Theorem float_to_real_threshold:
235 !x : ('t, 'w) float.
236 float_is_finite x ==> (abs (float_to_real x) < threshold (:'t # 'w))
237Proof
238 metis_tac [REAL_LET_TRANS, float_to_real_finite, largest_lt_threshold]
239QED
240
241(* ------------------------------------------------------------------------
242 Lifting up of rounding to nearest
243 ------------------------------------------------------------------------ *)
244
245Theorem bound_at_worst_lemma[local]:
246 !a : ('t, 'w) float x.
247 abs x < threshold (:'t # 'w) /\ float_is_finite a ==>
248 abs (float_to_real (round roundTiesToEven x : ('t, 'w) float) - x) <=
249 abs (float_to_real a - x)
250Proof
251 rw [round_def, REAL_ARITH ``abs x < y = ~(x <= ~y) /\ ~(x >= y)``]
252 \\ match_mp_tac
253 (MATCH_MP closest_is_closest is_finite_nonempty
254 |> Q.SPECL [`\a. ~word_lsb a.Significand`, `x`]
255 |> REWRITE_RULE [is_finite_nonempty, is_closest_def,
256 pred_setTheory.GSPEC_ETA]
257 |> CONJUNCT2)
258 \\ simp [pred_setTheory.SPECIFICATION]
259QED
260
261Theorem error_at_worst_lemma:
262 !a : ('t, 'w) float x.
263 abs x < threshold (:'t # 'w) /\ float_is_finite a ==>
264 abs (error (:'t # 'w) x) <= abs (float_to_real a - x)
265Proof
266 simp [error_def, bound_at_worst_lemma]
267QED
268
269Theorem error_is_zero:
270 !a : ('t, 'w) float x.
271 float_is_finite a /\ (float_to_real a = x) ==> (error (:'t # 'w) x = 0)
272Proof
273 rw []
274 \\ match_mp_tac
275 (error_at_worst_lemma
276 |> Q.SPECL [`a : ('t, 'w) float`, `float_to_real (a : ('t, 'w) float)`]
277 |> SIMP_RULE (srw_ss())
278 [REAL_ABS_0, REAL_ARITH ``abs x <= 0 = (x = 0r)``])
279 \\ simp [float_to_real_threshold]
280QED
281
282(* ------------------------------------------------------------------------ *)
283
284Theorem lem[local]:
285 !a b. 0 < b /\ b < a ==> 1 < a / b : real
286Proof
287 simp [realTheory.REAL_LT_RDIV_EQ]
288QED
289
290Theorem lem2[local]:
291 !n x. 0r < n /\ n <= n * x ==> 1 <= x
292Proof
293 rpt strip_tac
294 \\ spose_not_then assume_tac
295 \\ qpat_x_assum `n <= n * x` mp_tac
296 \\ fs [realTheory.REAL_NOT_LE,
297 GSYM (ONCE_REWRITE_RULE [REAL_MUL_COMM] realTheory.REAL_LT_RDIV_EQ),
298 realTheory.REAL_DIV_REFL, realTheory.REAL_POS_NZ]
299QED
300
301Theorem error_bound_lemma1:
302 !fracw x.
303 0r <= x /\ x < 1 /\ 0 < fracw ==>
304 ?n. n < 2 EXP fracw /\ &n / 2 pow fracw <= x /\
305 x < &(SUC n) / 2 pow fracw
306Proof
307 rpt strip_tac
308 \\ qspec_then `\n. &n / 2 pow fracw <= x` mp_tac
309 arithmeticTheory.EXISTS_GREATEST
310 \\ simp []
311 \\ Lib.W (Lib.C SUBGOAL_THEN (fn th => rewrite_tac [th]) o lhs o lhand o snd)
312 >- (conj_tac
313 >- (qexists_tac `0n` \\ simp [REAL_LE_MUL])
314 \\ simp[REAL_NOT_LE, arithmeticTheory.GREATER_DEF, real_div,
315 SF RMULRELNORM_ss]
316 \\ qexists_tac `2 ** fracw`
317 \\ rw []
318 \\ irule REAL_LT_TRANS
319 \\ qexists_tac ‘2 pow fracw’
320 \\ simp[SF RMULRELNORM_ss, REAL_OF_NUM_POW])
321 \\ disch_then (Q.X_CHOOSE_THEN `n` strip_assume_tac)
322 \\ pop_assum (qspec_then `SUC n` assume_tac)
323 \\ qexists_tac `n`
324 \\ fs [REAL_NOT_LE]
325 \\ spose_not_then assume_tac
326 \\ gs[arithmeticTheory.NOT_LESS, SF RMULRELNORM_ss]
327 \\ `2 pow fracw <= &n` by simp [realTheory.REAL_OF_NUM_POW]
328 \\ `2 pow fracw <= x * 2 pow fracw`
329 by imp_res_tac realTheory.REAL_LE_TRANS
330 \\ metis_tac [binary_ieeeTheory.zero_lt_twopow, REAL_MUL_COMM, lem2,
331 realTheory.real_lt]
332QED
333
334Theorem error_bound_lemma2 :
335 !fracw x.
336 0r <= x /\ x < 1 /\ 0 < fracw ==>
337 ?n. n <= 2 EXP fracw /\
338 abs (x - &n / 2 pow fracw) <= inv (2 pow (fracw + 1))
339Proof
340 ntac 2 gen_tac
341 \\ disch_then
342 (fn th => Q.X_CHOOSE_THEN `n` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)
343 (MATCH_MP error_bound_lemma1 th)
344 \\ strip_assume_tac th)
345 \\ disch_then (mp_tac o Q.SPEC `inv (2 pow (fracw + 1))` o MATCH_MP
346 (REAL_ARITH ``!a:real b x d. a <= x /\ x < b ==> b <= a + 2 * d ==>
347 abs (x - a) <= d \/ abs (x - b) <= d``))
348 \\ Lib.W (Lib.C SUBGOAL_THEN
349 (fn th => rewrite_tac [th]) o lhand o lhand o snd)
350 >- simp [realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_RDISTRIB,
351 realTheory.REAL_DIV_RMUL, realTheory.REAL_MUL_LINV,
352 realTheory.REAL_POW_ADD,
353 REAL_ARITH ``a * inv (b * a) * b = inv (b * a) * (b * a)``]
354 \\ rw []
355 >- (qexists_tac `n` \\ fs [])
356 \\ qexists_tac `SUC n`
357 \\ fs []
358QED
359
360Theorem error_bound_lemma3 :
361 !fracw x.
362 1r <= x /\ x < 2 /\ 0 < fracw ==>
363 ?n. n <= 2 EXP fracw /\
364 abs ((1 + &n / 2 pow fracw) - x) <= inv (2 pow (fracw + 1))
365Proof
366 rpt strip_tac
367 \\ Q.SUBGOAL_THEN `0r <= x - 1 /\ x - 1 < 1 /\ 0 < fracw`
368 (assume_tac o MATCH_MP error_bound_lemma2)
369 >- (simp []
370 \\ pop_assum kall_tac
371 \\ ntac 2 (POP_ASSUM mp_tac)
372 \\ REAL_ARITH_TAC
373 )
374 \\ metis_tac
375 [ABS_NEG, REAL_NEG_SUB, REAL_ARITH ``a - (b - c) = (c + a:real) - b``]
376QED
377
378(* ------------------------------------------------------------------------ *)
379
380Theorem two_pow_over_pre[local]:
381 !n. 0 < n ==> (2 pow n / 2 pow (n - 1) = 2)
382Proof
383 rpt strip_tac
384 \\ imp_res_tac arithmeticTheory.LESS_ADD_1
385 \\ fs [POW_ADD,
386 realTheory.REAL_DIV_LMUL_CANCEL
387 |> Q.SPECL [`2 pow n`, `2`, `1`]
388 |> SIMP_RULE (srw_ss()) []]
389QED
390
391Theorem error_bound_lemma4[local]:
392 !x. 1r <= x /\ x < 2 /\ 1 < dimindex (:'w) ==>
393 ?e f.
394 abs (float_to_real <| Sign := 0w;
395 Exponent := e : 'w word;
396 Significand := f : 't word |> - x) <=
397 inv (2 pow (dimindex (:'t) + 1)) /\
398 ((e = n2w (bias (:'w))) \/ (e = n2w (INT_MIN (:'w))) /\ (f = 0w))
399Proof
400 gen_tac
401 \\ DISCH_TAC
402 \\ Q.SUBGOAL_THEN `1 <= x /\ x < 2 /\ 0 < dimindex (:'t)` assume_tac
403 >- simp []
404 \\ first_assum
405 (Q.X_CHOOSE_THEN `n`
406 (MP_TAC o REWRITE_RULE [arithmeticTheory.LESS_OR_EQ]) o
407 MATCH_MP error_bound_lemma3)
408 \\ strip_tac
409 >- (qexists_tac `n2w (bias (:'w))`
410 \\ qexists_tac `n2w n`
411 \\ fs [float_to_real_def, wordsTheory.INT_MAX_LT_DIMWORD,
412 GSYM wordsTheory.dimword_def, wordsTheory.ZERO_LT_INT_MAX,
413 realTheory.REAL_DIV_REFL, DECIDE ``0 < x ==> x <> 0n``]
414 )
415 \\ qexists_tac `n2w (INT_MIN (:'w))`
416 \\ qexists_tac `0w`
417 \\ rfs [float_to_real_def, GSYM realTheory.REAL_OF_NUM_POW, two_pow_over_pre,
418 realTheory.REAL_DIV_REFL, wordsTheory.INT_MAX_def,
419 wordsTheory.INT_MIN_LT_DIMWORD, DECIDE ``0 < x ==> x <> 0n``]
420QED
421
422(* ------------------------------------------------------------------------ *)
423
424Theorem error_bound_lemma5[local]:
425 !x. 1r <= abs x /\ abs x < 2 /\ 1 < dimindex (:'w) ==>
426 ?s e f.
427 abs (float_to_real <| Sign := s;
428 Exponent := e : 'w word;
429 Significand := f : 't word |> - x) <=
430 inv (2 pow (dimindex (:'t) + 1)) /\
431 ((e = n2w (bias (:'w))) \/ (e = n2w (INT_MIN (:'w))) /\ (f = 0w))
432Proof
433 gen_tac
434 \\ DISCH_TAC
435 \\ SUBGOAL_THEN ``1 <= (x:real) /\ x < 2 /\ 1 < dimindex (:'w) \/
436 1 <= ~x /\ ~x < 2 /\ 1 < dimindex (:'w)``
437 (DISJ_CASES_THEN
438 (Q.X_CHOOSE_THEN `e` (Q.X_CHOOSE_THEN `f` assume_tac) o
439 MATCH_MP error_bound_lemma4))
440 >- (simp [] \\ pop_assum mp_tac \\ REAL_ARITH_TAC)
441 >| [qexists_tac `0w`, qexists_tac `1w`]
442 \\ qexists_tac `e`
443 \\ qexists_tac `f`
444 \\ ntac 2 (fs [float_to_real_def, wordsTheory.INT_MAX_LT_DIMWORD,
445 wordsTheory.INT_MIN_LT_DIMWORD, realTheory.REAL_DIV_REFL,
446 DECIDE ``0 < x ==> x <> 0n``, wordsTheory.ZERO_LT_INT_MAX,
447 REAL_ARITH ``abs (-2 - x) = abs (2 - -x)``,
448 REAL_ARITH ``abs (-1 * y - x) = abs (y - -x)``])
449 \\ rfs [DECIDE ``0 < x ==> x <> 0n``, wordsTheory.ZERO_LT_INT_MAX]
450QED
451
452(* ------------------------------------------------------------------------ *)
453
454val REAL_LE_LCANCEL_IMP =
455 METIS_PROVE [REAL_LE_LMUL] ``!x y z. 0r < x /\ x * y <= x * z ==> y <= z``
456
457Theorem lem[local]:
458 !a x.
459 1 < a ==> (2 pow (a - 2) * inv (2 pow (a - 1 + x)) = inv (2 pow (x + 1)))
460Proof
461 rw [realTheory.REAL_INV_1OVER, realTheory.mult_ratr, realTheory.mult_ratl,
462 realTheory.REAL_EQ_RDIV_EQ, GSYM realTheory.POW_ADD,
463 realTheory.REAL_DIV_REFL]
464QED
465
466Theorem error_bound_lemma6[local]:
467 !expw fracw x.
468 0 <= x /\ x < inv (2 pow (2 ** (expw - 1) - 2)) /\
469 1 < expw /\ 0 < fracw ==>
470 ?n. n <= 2 EXP fracw /\
471 abs (x - 2 / 2 pow (2 ** (expw - 1) - 1) * &n / 2 pow fracw) <=
472 inv (2 pow (2 ** (expw - 1) - 1 + fracw))
473Proof
474 rpt strip_tac
475 \\ Q.SPECL_THEN [`fracw`, `2 pow (2 ** (expw - 1) - 2) * x`] mp_tac
476 error_bound_lemma2
477 \\ Lib.W (Lib.C SUBGOAL_THEN MP_TAC o lhand o lhand o snd)
478 >- (conj_tac
479 >- (match_mp_tac realTheory.REAL_LE_MUL \\ simp [])
480 \\ qpat_x_assum `x < _` mp_tac
481 \\ simp [realTheory.REAL_INV_1OVER, realTheory.REAL_LT_RDIV_EQ,
482 realTheory.lt_ratr]
483 \\ metis_tac [REAL_MUL_COMM]
484 )
485 \\ DISCH_THEN (fn th => rewrite_tac [th])
486 \\ DISCH_THEN (Q.X_CHOOSE_THEN `n` strip_assume_tac)
487 \\ qexists_tac `n`
488 \\ asm_rewrite_tac []
489 \\ qspec_then `2 pow (2 ** (expw - 1) - 2)` match_mp_tac REAL_LE_LCANCEL_IMP
490 \\ conj_tac
491 >- simp []
492 \\ rewrite_tac
493 [realTheory.ABS_MUL
494 |> GSYM
495 |> Q.SPEC `2 pow (2 ** (expw - 1) - 2)`
496 |> SIMP_RULE (srw_ss()) [GSYM realTheory.POW_ABS]
497 ]
498 \\ `1n < 2 ** (expw - 1)`
499 by metis_tac [EVAL ``2n ** 0``, bitTheory.TWOEXP_MONO,
500 DECIDE ``1n < n ==> 0 < n - 1``]
501 \\ fs [realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_MUL_ASSOC, real_div, lem,
502 DECIDE ``1 < n ==> (SUC (n - 2) = n - 1)``, realTheory.REAL_MUL_RINV,
503 realTheory.pow
504 |> CONJUNCT2
505 |> GSYM
506 |> ONCE_REWRITE_RULE [REAL_MUL_COMM]
507 ]
508QED
509
510(* ------------------------------------------------------------------------ *)
511
512Theorem lem[local]:
513 !n. &(2 * 2 ** n) = 2 * 2 pow n
514Proof
515 simp [realTheory.REAL_OF_NUM_POW]
516QED
517
518Theorem error_bound_lemma7[local]:
519 !x. 0 <= x /\ x < inv (2 pow (bias (:'w) - 1)) /\ 1 < dimindex (:'w) ==>
520 ?e f.
521 abs (float_to_real <| Sign := 0w;
522 Exponent := e : 'w word;
523 Significand := f : 't word |> - x) <=
524 inv (2 pow (bias (:'w) + dimindex (:'t))) /\
525 ((e = 0w) \/ (e = 1w) /\ (f = 0w))
526Proof
527 gen_tac
528 \\ DISCH_TAC
529 \\ Q.SUBGOAL_THEN
530 `0 <= x /\ x < inv (2 pow (2 ** (dimindex (:'w) - 1) - 2)) /\
531 1 < dimindex (:'w) /\ 0 < dimindex (:'t)` assume_tac
532 >- fs [wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
533 \\ FIRST_ASSUM (Q.X_CHOOSE_THEN `n` MP_TAC o MATCH_MP error_bound_lemma6)
534 \\ DISCH_THEN
535 (CONJUNCTS_THEN2
536 (strip_assume_tac o REWRITE_RULE [arithmeticTheory.LESS_OR_EQ])
537 ASSUME_TAC)
538 >- (
539 qexists_tac `0w`
540 \\ qexists_tac `n2w n`
541 \\ fs [float_to_real_def, GSYM wordsTheory.dimword_def,
542 wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
543 \\ simp [Once realTheory.ABS_SUB]
544 \\ fs [realTheory.mult_rat, realTheory.mult_ratl,
545 Once realTheory.div_ratl]
546 )
547 \\ qexists_tac `1w`
548 \\ qexists_tac `0w`
549 \\ fs [float_to_real_def, wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
550 \\ simp [Once realTheory.ABS_SUB]
551 \\ rfs [realTheory.mult_rat, realTheory.mult_ratl, Once realTheory.div_ratl,
552 realTheory.REAL_DIV_RMUL_CANCEL, lem]
553QED
554
555(* ------------------------------------------------------------------------ *)
556
557Theorem error_bound_lemma8[local]:
558 !x. abs x < inv (2 pow (bias (:'w) - 1)) /\ 1 < dimindex (:'w) ==>
559 ?s e f.
560 abs (float_to_real <| Sign := s;
561 Exponent := e : 'w word;
562 Significand := f : 't word |> - x) <=
563 inv (2 pow (bias (:'w) + dimindex (:'t))) /\
564 ((e = 0w) \/ (e = 1w) /\ (f = 0w))
565Proof
566 gen_tac
567 \\ DISCH_TAC
568 \\ SUBGOAL_THEN
569 ``0 <= x /\ x < inv (2 pow (bias (:'w) - 1)) /\ 1 < dimindex (:'w) \/
570 0 <= ~x /\ ~x < inv (2 pow (bias (:'w) - 1)) /\ 1 < dimindex (:'w) ``
571 (DISJ_CASES_THEN
572 (Q.X_CHOOSE_THEN `e` (Q.X_CHOOSE_THEN `f` assume_tac) o
573 MATCH_MP error_bound_lemma7))
574 >- (simp [] \\ pop_assum mp_tac \\ REAL_ARITH_TAC)
575 >| [qexists_tac `0w`, qexists_tac `1w`]
576 \\ qexists_tac `e`
577 \\ qexists_tac `f`
578 \\ ntac 2 (fs [float_to_real_def, wordsTheory.INT_MAX_LT_DIMWORD,
579 wordsTheory.INT_MIN_LT_DIMWORD, REAL_MUL_ASSOC,
580 DECIDE ``0 < x ==> x <> 0n``, wordsTheory.ZERO_LT_INT_MAX,
581 REAL_ARITH ``abs (y - -x) = abs (-1 * y - x)``])
582 \\ rfs [DECIDE ``0 < x ==> x <> 0n``, wordsTheory.ZERO_LT_INT_MAX]
583QED
584
585(* ------------------------------------------------------------------------ *)
586
587Theorem float_to_real_scale_up[local]:
588 !s e f k.
589 e <> 0w /\ (e + n2w k <> 0w) /\ (w2n (e + n2w k) = w2n e + k) ==>
590 (float_to_real <| Sign := s;
591 Exponent := e + n2w k : 'w word;
592 Significand := f : 't word |> =
593 2 pow k * float_to_real <| Sign := s;
594 Exponent := e : 'w word;
595 Significand := f : 't word |>)
596Proof
597 simp [float_to_real_def, REAL_POW_ADD, real_div,
598 AC REAL_MUL_ASSOC REAL_MUL_COMM]
599QED
600
601Theorem float_to_real_scale_down[local]:
602 !s e f k.
603 e <> 0w /\ n2w k <> e /\
604 (w2n (e - n2w k + n2w k) = w2n (e - n2w k) + k) ==>
605 (float_to_real <| Sign := s;
606 Exponent := e - n2w k : 'w word;
607 Significand := f : 't word |> =
608 inv (2 pow k) *
609 float_to_real <| Sign := s;
610 Exponent := e : 'w word;
611 Significand := f : 't word |>)
612Proof
613 rpt strip_tac
614 \\ `e + -n2w k <> 0w /\ (e = (e - n2w k) + n2w k)`
615 by metis_tac [wordsTheory.WORD_EQ_SUB_ZERO, wordsTheory.WORD_SUB_INTRO,
616 wordsTheory.WORD_LESS_NOT_EQ, wordsTheory.WORD_SUB_ADD]
617 \\ pop_assum (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th])))
618 \\ asm_simp_tac (std_ss++simpLib.type_ssfrag ``:('a, 'b) float``)
619 [float_to_real_def, POW_ADD, AC REAL_MUL_ASSOC REAL_MUL_COMM]
620 \\ simp [SIMP_CONV (srw_ss()) [] ``a + b + -b : 'a word``,
621 REAL_MUL_ASSOC, realTheory.mult_ratr, REAL_MUL_LINV, POW_NZ,
622 REAL_ARITH ``inv a * b * c * a * d = (inv a * a) * b * c * d``]
623QED
624
625(* ------------------------------------------------------------------------ *)
626
627Theorem two_times_bias_lt[local]:
628 bias (:'a) + bias (:'a) < dimword (:'a) - 1
629Proof
630 simp [wordsTheory.INT_MAX_def, wordsTheory.INT_MAX_def,
631 GSYM wordsTheory.dimword_IS_TWICE_INT_MIN,
632 DECIDE ``1n < n ==> 0 < n - 1``]
633QED
634
635Theorem int_min_bias_plus1[local]:
636 INT_MIN (:'a) = INT_MAX (:'a) + 1
637Proof
638 simp [wordsTheory.INT_MAX_def, DECIDE ``0n < n ==> (n - 1 + 1 = n)``]
639QED
640
641
642Theorem lem[local]:
643 1 < dimindex (:'a) ==>
644 2 pow (UINT_MAX (:'a) - 1) / 2 pow (INT_MAX (:'a)) <= 2 pow (INT_MAX (:'a))
645Proof
646 rw [GSYM POW_ADD, realTheory.REAL_LE_LDIV_EQ]
647 \\ match_mp_tac REAL_POW_MONO
648 \\ simp [wordsTheory.UINT_MAX_def, wordsTheory.ZERO_LT_INT_MAX,
649 DECIDE ``0n < a ==> 0 < 2 * a``,
650 wordsTheory.dimword_IS_TWICE_INT_MIN]
651 \\ simp [wordsTheory.INT_MAX_def]
652QED
653
654Theorem lem2[local]:
655 !a b c d : real. 0 < b /\ 0 <= c /\ a < b * c /\ b <= d ==> a < c * d
656Proof
657 rw []
658 \\ `?p. 0 <= p /\ (d = b + p)`
659 by (qexists_tac `d - b`
660 \\ simp [REAL_ARITH ``b <= d : real ==> (b + (d - b) = d) /\ 0 <= d - b``]
661 )
662 \\ simp [realTheory.REAL_LDISTRIB, AC REAL_MUL_ASSOC REAL_MUL_COMM]
663 \\ `0 <= c * p`
664 by simp[
665 realTheory.REAL_LE_MUL2
666 |> Q.SPECL [`0`, `c`, `0`, `p`]
667 |> SIMP_RULE (srw_ss()) []]
668 \\ simp [REAL_ARITH ``0 <= c /\ a < b ==> a < b + c : real``]
669QED
670
671Theorem error_bound_big1[local]:
672 !x k. 2 pow k <= abs x /\ abs x < 2 pow SUC k /\
673 abs x < threshold (:'t # 'w) /\ 1 < dimindex (:'w) ==>
674 ?a : ('t, 'w) float.
675 float_is_finite a /\
676 abs (float_to_real a - x) <= 2 pow k / 2 pow (dimindex (:'t) + 1)
677Proof
678 rpt strip_tac
679 \\ qspec_then `x / 2 pow k` mp_tac error_bound_lemma5
680 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhand o lhand o snd)
681 >- (simp [ABS_DIV, GSYM realTheory.POW_ABS, ABS_N, POW_NZ, REAL_POW_LT,
682 REAL_LT_LDIV_EQ, GSYM (CONJUNCT2 pow)]
683 \\ match_mp_tac realTheory.REAL_LE_RDIV
684 \\ simp [realTheory.REAL_POW_LT])
685 \\ DISCH_THEN (fn th => rewrite_tac [th])
686 \\ `2 pow k < threshold (:'t # 'w)` by metis_tac [REAL_LET_TRANS]
687 \\ `k < bias (:'w) + 1`
688 by (spose_not_then (assume_tac o REWRITE_RULE [arithmeticTheory.NOT_LESS])
689 \\ `2r pow (bias (:'w) + 1) <= 2 pow k`
690 by (match_mp_tac REAL_POW_MONO \\ simp [])
691 \\ `2r pow (bias (:'w) + 1) < threshold (:'t # 'w)`
692 by metis_tac [REAL_LET_TRANS]
693 \\ pop_assum mp_tac
694 \\ simp [threshold, realTheory.REAL_LT_RDIV_EQ,
695 GSYM realTheory.REAL_OF_NUM_POW, GSYM realTheory.POW_ADD,
696 wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def,
697 wordsTheory.UINT_MAX_def,
698 DECIDE ``0n < n ==> (n - 1 + 1 = n) /\ (SUC (n - 1) = n)``,
699 GSYM (CONJUNCT2 arithmeticTheory.EXP)]
700 \\ simp [realTheory.REAL_NOT_LT, GSYM wordsTheory.dimword_def,
701 realTheory.REAL_SUB_LDISTRIB, realTheory.mult_ratr,
702 DECIDE ``1n < n ==> (SUC (n - 2) = n - 1)``,
703 DECIDE ``1n < n ==> n <> 0``,
704 GSYM
705 (ONCE_REWRITE_RULE [REAL_MUL_COMM] (CONJUNCT2 realTheory.pow))
706 ]
707 \\ match_mp_tac (REAL_ARITH ``0 < a /\ 0 <= b ==> (a - b <= a : real)``)
708 \\ simp [realTheory.REAL_LE_RDIV_EQ, DECIDE ``1n < n ==> 0 < 2 * n``]
709 )
710 \\ strip_tac
711 >| [all_tac,
712 Cases_on `k = bias (:'w)`
713 >- (
714 spose_not_then kall_tac
715 \\ qpat_x_assum `abs _ <= inv (2 pow _)`
716 (mp_tac o (MATCH_MP (REAL_ARITH
717 ``abs (a - b) <= c ==> abs(a) <= abs(b) + c``)))
718 \\ simp [realTheory.REAL_NOT_LE, REAL_ABS_MUL, GSYM POW_ABS, ABS_NEG,
719 ABS_DIV, ABS_N, float_to_real_def,
720 wordsTheory.INT_MIN_LT_DIMWORD, prim_recTheory.LESS_NOT_EQ]
721 \\ simp [int_min_bias_plus1, POW_ADD, realTheory.POW_ONE,
722 realTheory.REAL_LT_ADD_SUB, realTheory.REAL_LT_LDIV_EQ,
723 realTheory.REAL_DIV_LMUL_CANCEL
724 |> Q.SPECL [`2 pow n`, `2`, `1`]
725 |> SIMP_RULE (srw_ss()) []]
726 \\ match_mp_tac lem2
727 \\ qexists_tac `2 pow (UINT_MAX (:'w) - 1) / 2 pow bias (:'w)`
728 \\ fs [threshold_def, pow, lem, AC REAL_MUL_ASSOC REAL_MUL_COMM,
729 realTheory.REAL_LT_RDIV_0, realTheory.REAL_SUB_LE,
730 realTheory.REAL_INV_1OVER, realTheory.REAL_LE_LDIV_EQ,
731 realTheory.POW_2_LE1, REAL_ARITH ``0r < n ==> 0 < 2 * n``,
732 REAL_ARITH ``1r <= n ==> 1 <= 2 * (2 * n)``]
733 )
734 \\ `k < bias (:'w)` by decide_tac
735 ]
736 \\ (
737 qexists_tac `<| Sign := s;
738 Exponent := e + n2w k;
739 Significand := f |> : ('t, 'w) float`
740 \\ conj_tac
741 >- simp [float_tests, wordsTheory.word_add_n2w, int_min_bias_plus1,
742 wordsTheory.word_2comp_n2w, two_times_bias_lt,
743 DECIDE ``k < b + 1n /\ (b + b) < w - 1 ==>
744 k + b < w /\ k + b <> w - 1``,
745 DECIDE ``k < b /\ (b + b) < w - 1n ==>
746 k + (b + 1) < w /\ k + (b + 1) <> w - 1``]
747 \\ Q.SUBGOAL_THEN
748 `e <> 0w /\ e + n2w k <> 0w /\ (w2n (e + n2w k) = w2n e + k)`
749 (fn th => rewrite_tac [MATCH_MP float_to_real_scale_up th])
750 >- (
751 fs [wordsTheory.INT_MAX_LT_DIMWORD, prim_recTheory.LESS_NOT_EQ,
752 wordsTheory.INT_MIN_LT_DIMWORD, wordsTheory.ZERO_LT_INT_MAX,
753 wordsTheory.word_add_n2w, two_times_bias_lt,
754 DECIDE ``k < b + 1n /\ (b + b) < w - 1 ==>
755 k + b < w /\ k + b <> w - 1``]
756 \\ simp [int_min_bias_plus1, two_times_bias_lt,
757 DECIDE ``k < b /\ (b + b) < w - 1n ==>
758 k + (b + 1) < w /\ k + (b + 1) <> w - 1``]
759 )
760 \\ match_mp_tac REAL_LE_LCANCEL_IMP
761 \\ qexists_tac `inv (2 pow k)`
762 \\ conj_tac
763 >- simp [REAL_LT_INV_EQ, REAL_POW_LT]
764 \\ `!x. inv (2 pow k) * abs x = abs (inv (2 pow k) * x)`
765 by rewrite_tac
766 [REAL_ABS_MUL, REAL_ABS_INV, GSYM realTheory.POW_ABS, ABS_N]
767 \\ qpat_x_assum `zz <= inv (2 pow _)` mp_tac
768 \\ simp [REAL_SUB_LDISTRIB, REAL_MUL_ASSOC, real_div, POW_NZ,
769 REAL_MUL_LINV, float_to_real_def]
770 \\ simp [AC REAL_MUL_COMM REAL_MUL_ASSOC, wordsTheory.ZERO_LT_INT_MAX,
771 wordsTheory.INT_MAX_LT_DIMWORD, prim_recTheory.LESS_NOT_EQ
772 ]
773 )
774QED
775
776Theorem error_bound_big[local]:
777 !k x.
778 2 pow k <= abs x /\ abs x < 2 pow (SUC k) /\
779 abs x < threshold (:'t # 'w) /\ 1 < dimindex (:'w) ==>
780 abs (error (:'t # 'w) x) <= 2 pow k / 2 pow (dimindex (:'t) + 1)
781Proof
782 prove_tac [error_bound_big1, error_at_worst_lemma, REAL_LE_TRANS]
783QED
784
785(* ------------------------------------------------------------------------ *)
786
787Theorem suc_bias_lt_dimword[local]:
788 1 < dimindex (:'a) ==> bias (:'a) + 1 < dimword (:'a)
789Proof
790 simp [wordsTheory.INT_MAX_def, wordsTheory.dimword_IS_TWICE_INT_MIN,
791 DECIDE ``0n < n ==> (n - 1 + 1 = n)``]
792QED
793
794Theorem error_bound_small1[local]:
795 !x k. inv (2 pow SUC k) <= abs x /\ abs x < inv (2 pow k) /\
796 k < bias (:'w) - 1 /\ 1 < dimindex (:'w) ==>
797 ?a : ('t, 'w) float.
798 float_is_finite a /\
799 abs (float_to_real a - x) <=
800 inv (2 pow SUC k * 2 pow (dimindex (:'t) + 1))
801Proof
802 rpt strip_tac
803 \\ qspec_then `x * 2 pow (SUC k)` mp_tac error_bound_lemma5
804 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhand o lhand o snd)
805 >- (fs [ABS_MUL, GSYM POW_ABS, REAL_INV_1OVER, REAL_LE_LDIV_EQ,
806 REAL_LT_RDIV_EQ, REAL_POW_LT]
807 \\ simp [pow, REAL_ARITH ``a * (2r * b) < 2 = a * b < 1``])
808 \\ DISCH_THEN (fn th => rewrite_tac [th])
809 \\ DISCH_THEN
810 (Q.X_CHOOSE_THEN `s`
811 (Q.X_CHOOSE_THEN `e`
812 (Q.X_CHOOSE_THEN `f` (REPEAT_TCL CONJUNCTS_THEN assume_tac))))
813 \\ qexists_tac `<| Sign := s;
814 Exponent := e - n2w (SUC k);
815 Significand := f |> : ('t, 'w) float`
816 \\ conj_tac
817 >- (
818 fs [float_tests, wordsTheory.WORD_LITERAL_ADD, int_min_bias_plus1]
819 \\ `bias (:'w) - SUC k < dimword (:'w)`
820 by (match_mp_tac arithmeticTheory.LESS_TRANS
821 \\ qexists_tac `bias (:'w)`
822 \\ simp [wordsTheory.INT_MAX_LT_DIMWORD]
823 )
824 \\ `bias (:'w) + 1 - SUC k < dimword (:'w)`
825 by (match_mp_tac arithmeticTheory.LESS_TRANS
826 \\ qexists_tac `bias (:'w) + 1`
827 \\ simp [wordsTheory.INT_MAX_def,
828 wordsTheory.dimword_IS_TWICE_INT_MIN,
829 DECIDE ``0n < n ==> (n - 1 + 1 = n)``]
830 )
831 \\ simp_tac std_ss [wordsTheory.WORD_NEG_1, wordsTheory.word_T_def]
832 \\ simp [wordsTheory.BOUND_ORDER, wordsTheory.INT_MAX_LT_DIMWORD]
833 \\ simp [wordsTheory.INT_MAX_def, wordsTheory.UINT_MAX_def,
834 wordsTheory.dimword_IS_TWICE_INT_MIN,
835 DECIDE ``0 < a /\ 0 < b ==> a - b <> 2 * a - 1n``
836 ]
837 )
838 \\ `e <> 0w /\ n2w (SUC k) <> e /\
839 (w2n (e - n2w (SUC k) + n2w (SUC k)) = w2n (e - n2w (SUC k)) + SUC k)`
840 by (
841 `SUC k < dimword (:'w)`
842 by metis_tac [wordsTheory.ZERO_LT_INT_MAX, wordsTheory.INT_MAX_LT_DIMWORD,
843 arithmeticTheory.LESS_TRANS,
844 DECIDE ``0n < b /\ k < b - 1 ==> SUC k < b``]
845 \\ fs [wordsTheory.INT_MAX_LT_DIMWORD, wordsTheory.INT_MIN_LT_DIMWORD,
846 prim_recTheory.LESS_NOT_EQ,
847 int_min_bias_plus1, suc_bias_lt_dimword,
848 SIMP_CONV (srw_ss()) [] ``a + b + -b : 'a word``,
849 SIMP_CONV (srw_ss()) [] ``b + a + -b : 'a word``]
850 \\ simp [wordsTheory.WORD_LITERAL_ADD, wordsTheory.INT_MAX_LT_DIMWORD,
851 DECIDE ``0n < a /\ a < n ==> (a - SUC k < n) /\
852 (a + 1 - SUC k < n)``]
853 )
854 \\ NO_STRIP_FULL_SIMP_TAC std_ss [float_to_real_scale_down]
855 \\ match_mp_tac REAL_LE_LCANCEL_IMP
856 \\ qexists_tac `2 pow (SUC k)`
857 \\ `!x. 2 pow (SUC k) * abs x = abs (2 pow (SUC k) * x)`
858 by rewrite_tac [REAL_ABS_MUL, REAL_ABS_INV, GSYM POW_ABS, ABS_N]
859 \\ `!a b. 0 < a ==> (a * (inv a * b) = b)`
860 by simp [REAL_MUL_ASSOC, REAL_MUL_RINV, REAL_POS_NZ]
861 \\ simp [REAL_POW_LT, REAL_SUB_LDISTRIB, REAL_POS_NZ, REAL_INV_MUL]
862 \\ NO_STRIP_FULL_SIMP_TAC (srw_ss()) [AC REAL_MUL_ASSOC REAL_MUL_COMM]
863QED
864
865Theorem REAL_LE_INV2[local]:
866 !x y. 0 < x /\ x <= y ==> inv y <= inv x
867Proof
868 metis_tac [REAL_LE_LT, REAL_LT_INV]
869QED
870
871Theorem lem[local]:
872 !n m. 2n <= n /\ 0 < m ==>
873 2 pow (n - 1) < 2 pow (2 * n - 1) - 2 pow (2 * n - 2) / &(4 * m)
874Proof
875 rw [realTheory.REAL_LT_SUB_LADD]
876 \\ `1 < 4 * m /\ 0 < 4 * m` by decide_tac
877 \\ `!x y:real. x < y = x * &(4 * m) < y * &(4 * m)`
878 by metis_tac [realTheory.REAL_LT_RMUL,
879 SIMP_CONV (srw_ss()) [] ``0r < &(4 * m)``]
880 \\ pop_assum (fn th => once_rewrite_tac [th])
881 \\ simp [realTheory.REAL_ADD_RDISTRIB, realTheory.REAL_DIV_RMUL,
882 REAL_ARITH ``!n. x * (4 * n) = 2 * x * n + 2 * x * n : real``
883 |> Q.SPEC `&n`
884 |> SIMP_RULE (srw_ss()) []]
885 \\ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [REAL_ADD_COMM]))
886 \\ match_mp_tac realTheory.REAL_LTE_ADD2
887 \\ Q.SPECL_THEN [`2`, `n`] imp_res_tac arithmeticTheory.LESS_EQUAL_ADD
888 \\ fs []
889 \\ rw [realTheory.REAL_DOUBLE]
890 >- (
891 simp [realTheory.REAL_OF_NUM_POW, DECIDE ``x + 3 = SUC (x + 2)``,
892 arithmeticTheory.EXP, arithmeticTheory.RIGHT_ADD_DISTRIB,
893 arithmeticTheory.LEFT_ADD_DISTRIB]
894 \\ rewrite_tac [arithmeticTheory.MULT_ASSOC,
895 arithmeticTheory.LT_MULT_CANCEL_LBARE]
896 \\ simp []
897 )
898 \\ `m <> 0` by decide_tac
899 \\ asm_simp_tac std_ss
900 [realTheory.REAL_NZ_IMP_LT, realTheory.REAL_LE_RMUL, REAL_MUL_ASSOC]
901 \\ asm_simp_tac std_ss
902 [realTheory.REAL_LE_LMUL, GSYM REAL_MUL_ASSOC, REAL_ARITH ``0 < 2r``]
903 \\ simp [GSYM (CONJUNCT2 pow)]
904 \\ match_mp_tac REAL_POW_MONO
905 \\ simp []
906QED
907
908Theorem threshold_gt1[local]:
909 1 < dimindex (:'w) ==> 1 < threshold (:'t # 'w)
910Proof
911 simp [threshold, realTheory.REAL_INV_1OVER, realTheory.REAL_LT_RDIV_EQ,
912 realTheory.mult_ratl, realTheory.mult_ratr,
913 GSYM realTheory.REAL_OF_NUM_POW, prim_recTheory.LESS_NOT_EQ,
914 wordsTheory.ZERO_LT_INT_MAX, two_pow_over_pre,
915 realTheory.REAL_SUB_LDISTRIB, DECIDE ``0n < n ==> (SUC (n - 1) = n)``,
916 GSYM (CONJUNCT2 arithmeticTheory.EXP)]
917 \\ simp [wordsTheory.UINT_MAX_def, wordsTheory.INT_MAX_def,
918 wordsTheory.dimword_IS_TWICE_INT_MIN]
919 \\ qabbrev_tac `n = INT_MIN (:'w)`
920 \\ qabbrev_tac `m = INT_MIN (:'t)`
921 \\ strip_tac
922 \\ `2n <= n` by simp [Abbr `n`, wordsTheory.INT_MIN_def]
923 \\ `0n < m` by simp [Abbr `m`, wordsTheory.INT_MIN_def]
924 \\ simp [lem]
925QED
926
927Theorem error_bound_small[local]:
928 !k x.
929 inv (2 pow (SUC k)) <= abs x /\ abs x < inv (2 pow k) /\
930 k < bias (:'w) - 1 /\ 1 < dimindex (:'w) ==>
931 abs (error (:'t # 'w) x) <=
932 inv (2 pow (SUC k) * 2 pow (dimindex (:'t) + 1))
933Proof
934 rpt strip_tac
935 \\ `?a : ('t, 'w) float.
936 float_is_finite a /\
937 abs (float_to_real a - x) <=
938 inv (2 pow (SUC k) * 2 pow (dimindex (:'t) + 1))`
939 by metis_tac [error_bound_small1]
940 \\ match_mp_tac REAL_LE_TRANS
941 \\ qexists_tac `abs (float_to_real a - x)`
942 \\ simp []
943 \\ match_mp_tac error_at_worst_lemma
944 \\ simp []
945 \\ match_mp_tac REAL_LT_TRANS
946 \\ qexists_tac `inv (2 pow k)`
947 \\ simp []
948 \\ match_mp_tac REAL_LET_TRANS
949 \\ qexists_tac `inv 1`
950 \\ conj_tac
951 >- (match_mp_tac REAL_LE_INV2 \\ simp [REAL_POW_LE_1])
952 \\ simp [realTheory.REAL_INV_1OVER, threshold_gt1]
953QED
954
955(* ------------------------------------------------------------------------ *)
956
957Theorem lem[local]:
958 1 < dimindex (:'w) ==> -1w <> (1w : 'w word)
959Proof
960 srw_tac [wordsLib.WORD_BIT_EQ_ss] []
961 \\ qexists_tac `1`
962 \\ simp [wordsTheory.word_index]
963QED
964
965Theorem error_bound_tiny[local]:
966 !x. abs x < inv (2 pow (bias (:'w) - 1)) /\ 1 < dimindex (:'w) ==>
967 abs (error (:'t # 'w) x) <= inv (2 pow (bias (:'w) + dimindex (:'t)))
968Proof
969 strip_tac
970 \\ DISCH_TAC
971 \\ `?a : ('t, 'w) float.
972 float_is_finite a /\
973 abs (float_to_real a - x) <= inv (2 pow (bias (:'w) + dimindex (:'t)))`
974 by (pop_assum (fn th => mp_tac (MATCH_MP error_bound_lemma8 th)
975 \\ assume_tac th)
976 \\ DISCH_THEN
977 (Q.X_CHOOSE_THEN `s`
978 (Q.X_CHOOSE_THEN `e`
979 (Q.X_CHOOSE_THEN `f` (REPEAT_TCL CONJUNCTS_THEN assume_tac))))
980 \\ qexists_tac `<|Sign := s; Exponent := e; Significand := f|>`
981 \\ fs [float_tests, wordsTheory.word_T_not_zero, lem]
982 )
983 \\ match_mp_tac REAL_LE_TRANS
984 \\ qexists_tac `abs (float_to_real a - x)`
985 \\ simp []
986 \\ match_mp_tac error_at_worst_lemma
987 \\ asm_rewrite_tac []
988 \\ match_mp_tac REAL_LT_TRANS
989 \\ qexists_tac `inv (2 pow (bias (:'w) - 1))`
990 \\ asm_rewrite_tac []
991 \\ match_mp_tac realTheory.REAL_LET_TRANS
992 \\ qexists_tac `1`
993 \\ simp [realTheory.REAL_INV_1OVER, realTheory.REAL_LE_LDIV_EQ, threshold_gt1]
994 \\ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM (EVAL ``2r pow 0``)]))
995 \\ match_mp_tac REAL_POW_MONO
996 \\ simp []
997QED
998
999(* -------------------------------------------------------------------------
1000 Stronger versions not requiring exact location of the interval.
1001 ------------------------------------------------------------------------- *)
1002
1003Theorem lem[local]:
1004 !n. 1 < n ==> (2 * inv (2 pow (n - 1)) = inv (2 pow (n - 2)))
1005Proof
1006 rw [realTheory.REAL_INV_1OVER, realTheory.REAL_EQ_RDIV_EQ,
1007 REAL_ARITH ``2 * (a:real) * b = a * (2 * b)``, GSYM (CONJUNCT2 pow),
1008 DECIDE ``1 < n ==> (SUC (n - 2) = n - 1)``,
1009 realTheory.REAL_DIV_RMUL
1010 ]
1011QED
1012
1013Theorem error_bound_norm_strong[local]:
1014 !x j.
1015 abs x < threshold (:'t # 'w) /\
1016 abs x < 2 pow (SUC j) / 2 pow (bias (:'w) - 1) /\ 1 < bias (:'w) ==>
1017 abs (error (:'t # 'w) x) <= 2 pow j / 2 pow (bias (:'w) + dimindex (:'t))
1018Proof
1019 gen_tac
1020 \\ Induct
1021 >- (
1022 rw_tac std_ss [pow, POW_1, real_div, REAL_MUL_LID, REAL_MUL_RID]
1023 \\ fs [lem]
1024 \\ `1 < dimindex (:'w)`
1025 by (
1026 spose_not_then assume_tac
1027 \\ `(dimindex (:'w) = 0) \/ (dimindex (:'w) = 1)` by decide_tac
1028 \\ fs [wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
1029 )
1030 \\ Cases_on `abs x < inv (2 pow (bias (:'w) - 1))`
1031 >- metis_tac [error_bound_tiny]
1032 \\ qspecl_then [`bias (:'w) - 2`, `x`] mp_tac error_bound_small
1033 \\ fs [GSYM REAL_POW_ADD, arithmeticTheory.ADD1, GSYM REAL_NOT_LT]
1034 )
1035 \\ strip_tac
1036 \\ `1 < dimindex (:'w)`
1037 by (
1038 spose_not_then assume_tac
1039 \\ `(dimindex (:'w) = 0) \/ (dimindex (:'w) = 1)` by decide_tac
1040 \\ fs [wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
1041 )
1042 \\ Cases_on `abs x < 2 pow SUC j / 2 pow (bias (:'w) - 1)`
1043 >- (match_mp_tac REAL_LE_TRANS
1044 \\ qexists_tac `2 pow j / 2 pow (bias (:'w) + dimindex (:'t))`
1045 \\ asm_simp_tac std_ss [real_div, pow]
1046 \\ match_mp_tac realTheory.REAL_LE_RMUL_IMP
1047 \\ simp_tac std_ss [REAL_LE_INV_EQ, POW_POS, REAL_ARITH ``0 <= 2r``,
1048 REAL_ARITH ``0r <= a ==> a <= 2 * a``]
1049 )
1050 \\ Cases_on `SUC j <= bias (:'w) - 2`
1051 >- (
1052 `2 pow SUC j / 2 pow (bias (:'w) + dimindex (:'t)) =
1053 inv (2 pow SUC ((bias (:'w) - 2) - SUC j) * 2 pow (dimindex (:'t) + 1))`
1054 by simp [GSYM POW_ADD, realTheory.REAL_EQ_LDIV_EQ,
1055 realTheory.REAL_EQ_RDIV_EQ,
1056 arithmeticTheory.ADD1, REAL_INV_1OVER, realTheory.mult_ratl]
1057 \\ asm_rewrite_tac []
1058 \\ match_mp_tac error_bound_small
1059 \\ `inv (2 pow (SUC (bias (:'w) - (SUC j + 2)))) =
1060 2 pow SUC j / 2 pow (bias (:'w) - 1)`
1061 by simp [GSYM POW_ADD, realTheory.REAL_EQ_LDIV_EQ,
1062 realTheory.REAL_EQ_RDIV_EQ,
1063 arithmeticTheory.ADD1, REAL_INV_1OVER, realTheory.mult_ratl]
1064 \\ `inv (2 pow (bias (:'w) - (SUC j + 2))) =
1065 2 pow SUC (SUC j) / 2 pow (bias (:'w) - 1)`
1066 by simp [GSYM POW_ADD, realTheory.REAL_EQ_LDIV_EQ,
1067 realTheory.REAL_EQ_RDIV_EQ,
1068 arithmeticTheory.ADD1, REAL_INV_1OVER, realTheory.mult_ratl]
1069 \\ fs [realTheory.REAL_NOT_LT]
1070 )
1071 \\ `?i. j = (bias (:'w) - 2) + i`
1072 by (qexists_tac `j - (bias (:'w) - 2)` \\ decide_tac)
1073 \\ asm_simp_tac std_ss
1074 [DECIDE ``1n < b ==> (b + i = b - 1 + SUC i) /\
1075 (SUC (b - 2 + i) = b - 1 + i)``]
1076 \\ simp_tac std_ss [POW_ADD]
1077 \\ simp [realTheory.REAL_DIV_LMUL_CANCEL, arithmeticTheory.ADD1]
1078 \\ match_mp_tac error_bound_big
1079 \\ qpat_x_assum `~(_ < _)` mp_tac
1080 \\ full_simp_tac bool_ss
1081 [realTheory.REAL_NOT_LT, POW_ADD,
1082 DECIDE ``1n < b ==> (SUC (b - 2 + i) = i + (b - 1))``,
1083 DECIDE ``SUC (i + (b - 1)) = SUC i + (b - 1)``,
1084 realTheory.REAL_DIV_RMUL_CANCEL
1085 |> Q.SPECL [`2 pow n`, `a`, `1`]
1086 |> SIMP_RULE (srw_ss()) []
1087 ]
1088QED
1089
1090Theorem absolute_error_denormal:
1091 !x. abs x < threshold (:'t # 'w) /\ abs x < 2 * 1 / 2 pow (bias (:'w) - 1) /\
1092 1 < bias (:'w) ==>
1093 ?e. abs (float_to_real(round roundTiesToEven x:('t,'w) float) - x) <= e /\
1094 e <= 1 / 2 pow (bias (:'w) + dimindex (:'t))
1095Proof
1096 rw[] \\ qspecl_then [‘x’,‘0’] mp_tac error_bound_norm_strong
1097 \\ impl_tac >- gs[]
1098 \\ once_rewrite_tac[realaxTheory.real_abs]
1099 \\ gs[error_def] \\ COND_CASES_TAC
1100 \\ rpt strip_tac
1101 >- (
1102 qexists_tac ‘float_to_real ((round roundTiesToEven x):('t,'w) float) - x’
1103 \\ gs[])
1104 \\ qexists_tac ‘- (float_to_real ((round roundTiesToEven x):('t,'w) float) - x)’
1105 \\ gs[]
1106QED
1107
1108(* -------------------------------------------------------------------------
1109 "1 + Epsilon" property (relative error bounding).
1110 ------------------------------------------------------------------------- *)
1111
1112Theorem bias_imp_dimindex[local]:
1113 1 < bias (:'a) ==> 1 < dimindex (:'a)
1114Proof
1115 rw [wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def]
1116 \\ spose_not_then assume_tac
1117 \\ `dimindex (:'a) = 1` by simp [DECIDE ``0n < n /\ ~(1 < n) ==> (n = 1)``]
1118 \\ fs []
1119QED
1120
1121Theorem lem[local]:
1122 !n : num. n + SUC (n - 1) <= 2 ** n
1123Proof
1124 Induct \\ rw [arithmeticTheory.EXP]
1125QED
1126
1127Theorem THRESHOLD_MUL_LT[local]:
1128 threshold (:'t # 'w) * 2 pow (bias (:'w) - 1) < 2 pow (2 EXP (bias (:'w)))
1129Proof
1130 `2 pow (UINT_MAX (:'w) - 1) * inv (2 pow (bias (:'w))) = 2 pow (bias (:'w))`
1131 by (simp [REAL_INV_1OVER, realTheory.mult_ratr, realTheory.REAL_EQ_LDIV_EQ,
1132 GSYM REAL_POW_ADD]
1133 \\ simp [realTheory.REAL_OF_NUM_POW, wordsTheory.UINT_MAX_def,
1134 wordsTheory.INT_MAX_def, wordsTheory.dimword_IS_TWICE_INT_MIN,
1135 arithmeticTheory.LEFT_SUB_DISTRIB])
1136 \\ asm_simp_tac std_ss [threshold_def, real_div]
1137 \\ rewrite_tac
1138 [GSYM REAL_MUL_ASSOC, REAL_SUB_RDISTRIB, REAL_SUB_LDISTRIB,
1139 GSYM pow, GSYM POW_ADD]
1140 \\ match_mp_tac REAL_LTE_TRANS
1141 \\ qexists_tac `2 pow (bias (:'w) + SUC (bias (:'w) - 1))`
1142 \\ conj_tac
1143 >- (
1144 match_mp_tac (REAL_ARITH ``0 < a /\ 0r < x ==> (a - x < a)``)
1145 \\ simp [realTheory.REAL_LT_RMUL_0, realTheory.REAL_LT_LMUL_0,
1146 realTheory.REAL_LT_INV_EQ]
1147 )
1148 \\ match_mp_tac REAL_POW_MONO
1149 \\ simp [lem]
1150QED
1151
1152Theorem lem[local]:
1153 !a b c:real. 0 < b ==> ((a / b) * c = a * (c / b))
1154Proof
1155 rw [realTheory.mult_ratl, realTheory.mult_ratr]
1156QED
1157
1158Theorem LT_THRESHOLD_LT_POW_INV[local]:
1159 !x. 1 < dimindex (:'w) ==> x < threshold (:'t # 'w) ==>
1160 x < 2 pow (UINT_MAX (:'w) - 1) / 2 pow (bias (:'w) - 1)
1161Proof
1162 gen_tac
1163 \\ strip_tac
1164 \\ simp [threshold]
1165 \\ match_mp_tac (REAL_ARITH ``b < c ==> (a < b ==> a < c : real)``)
1166 \\ simp [realTheory.REAL_LT_LDIV_EQ, GSYM realTheory.REAL_OF_NUM_POW, lem,
1167 two_pow_over_pre, wordsTheory.ZERO_LT_INT_MAX,
1168 realTheory.REAL_LT_LMUL]
1169 \\ match_mp_tac (REAL_ARITH ``0r < a /\ 0r < b ==> a - b < a``)
1170 \\ `0r < &(2 * dimword (:'t))` by simp [DECIDE ``0n < n ==> 0 < 2 * n``]
1171 \\ simp [realTheory.REAL_LT_RDIV_0]
1172QED
1173
1174Theorem real_pos_in_binade[local]:
1175 !x. normalizes (:'t # 'w) x /\ 0 <= x ==>
1176 ?j. j <= UINT_MAX (:'w) - 2 /\ 2 pow j / 2 pow (bias (:'w) - 1) <= x /\
1177 x < 2 pow (SUC j) / 2 pow (bias (:'w) - 1)
1178Proof
1179 rw_tac arith_ss [normalizes_def, abs]
1180 \\ imp_res_tac bias_imp_dimindex
1181 \\ qspec_then `\n. 2 pow n / 2 pow (bias (:'w) - 1) <= x`
1182 mp_tac arithmeticTheory.EXISTS_GREATEST
1183 \\ Lib.W (Lib.C SUBGOAL_THEN mp_tac o lhs o lhand o snd)
1184 >- (
1185 conj_tac
1186 >- (qexists_tac `0` \\ asm_simp_tac std_ss [REAL_MUL_LID , pow, real_div])
1187 \\ qexists_tac `2 EXP (bias (:'w))`
1188 \\ Q.X_GEN_TAC `n`
1189 \\ rw_tac bool_ss
1190 [GSYM real_lt, REAL_LT_RDIV_EQ, REAL_POW_LT, REAL_ARITH ``0 < 2r``]
1191 \\ match_mp_tac REAL_LT_TRANS
1192 \\ qexists_tac `2 pow (2 EXP (bias (:'w)))`
1193 \\ conj_tac
1194 >- (
1195 match_mp_tac realTheory.REAL_LT_TRANS
1196 \\ qexists_tac `threshold (:'t # 'w) * 2 pow (bias (:'w) - 1)`
1197 \\ simp [REAL_LT_RMUL, THRESHOLD_MUL_LT]
1198 )
1199 \\ match_mp_tac REAL_POW_MONO_LT
1200 \\ asm_simp_tac bool_ss
1201 [REAL_ARITH ``1 < 2r``, GSYM arithmeticTheory.GREATER_DEF]
1202 )
1203 \\ DISCH_THEN (fn th => rewrite_tac [th])
1204 \\ DISCH_THEN
1205 (X_CHOOSE_THEN ``n:num``
1206 (CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o Q.SPEC `SUC n`)))
1207 \\ rw_tac arith_ss [REAL_NOT_LE]
1208 \\ qexists_tac `n`
1209 \\ full_simp_tac std_ss []
1210 \\ imp_res_tac LT_THRESHOLD_LT_POW_INV
1211 \\ `2 pow n / 2 pow (bias (:'w) - 1) <
1212 2 pow (UINT_MAX (:'w) - 1) / 2 pow (bias (:'w) - 1)`
1213 by metis_tac [REAL_LET_TRANS]
1214 \\ spose_not_then assume_tac
1215 \\ `UINT_MAX (:'w) - 1 <= n` by decide_tac
1216 \\ `2 pow (UINT_MAX (:'w) - 1) <= 2 pow n`
1217 by metis_tac [REAL_POW_MONO, REAL_ARITH ``1 <= 2r``]
1218 \\ full_simp_tac std_ss
1219 [REAL_LT_RDIV, REAL_POW_LT, REAL_ARITH ``0 < 2r``, real_lte]
1220QED
1221
1222Theorem real_neg_in_binade[local]:
1223 !x. normalizes (:'t # 'w) x /\ 0 <= ~x ==>
1224 ?j. j <= UINT_MAX (:'w) - 2 /\ 2 pow j / 2 pow (bias (:'w) - 1) <= ~x /\
1225 ~x < 2 pow (SUC j) / 2 pow (bias (:'w) - 1)
1226Proof
1227 metis_tac [normalizes_def, ABS_NEG, real_pos_in_binade]
1228QED
1229
1230Theorem real_in_binade[local]:
1231 !x. normalizes (:'t # 'w) x ==>
1232 ?j. j <= UINT_MAX (:'w) - 2 /\
1233 2 pow j / 2 pow (bias (:'w) - 1) <= abs x /\
1234 abs x < 2 pow (SUC j) / 2 pow (bias (:'w) - 1)
1235Proof
1236 gen_tac
1237 \\ Cases_on `0 <= x`
1238 \\ asm_simp_tac arith_ss [abs, real_neg_in_binade, real_pos_in_binade,
1239 REAL_ARITH ``~(0r <= x) ==> 0 <= ~x``]
1240QED
1241
1242(* ------------------------------------------------------------------------- *)
1243
1244Theorem error_bound_norm_strong_normalize[local]:
1245 !x. normalizes (:'t # 'w) x ==>
1246 ?j. abs (error (:'t # 'w) x) <=
1247 2 pow j / 2 pow (bias (:'w) + dimindex (:'t))
1248Proof
1249 metis_tac [real_in_binade, error_bound_norm_strong, normalizes_def]
1250QED
1251
1252(* ------------------------------------------------------------------------- *)
1253
1254Theorem inv_le[local]:
1255 !a b. 0 < a /\ 0 < b ==> (inv a <= inv b = b <= a)
1256Proof
1257 rw [realTheory.REAL_INV_1OVER, realTheory.REAL_LE_LDIV_EQ,
1258 realTheory.mult_ratl, realTheory.REAL_LE_RDIV_EQ]
1259QED
1260
1261Theorem relative_bound_lem[local]:
1262 !x j. x <> 0 ==>
1263 (2 pow j * inv (2 pow (bias (:'w) - 1)) <= abs x =
1264 inv (abs x) <= inv (2 pow j * inv (2 pow (bias (:'w) - 1))))
1265Proof
1266 REPEAT strip_tac
1267 \\ match_mp_tac (GSYM inv_le)
1268 \\ asm_simp_tac std_ss [REAL_ARITH ``x <> 0 ==> 0 < abs x``]
1269 \\ match_mp_tac realTheory.REAL_LT_MUL
1270 \\ simp_tac std_ss [realTheory.REAL_POW_LT, realTheory.REAL_LT_INV_EQ,
1271 REAL_ARITH ``0 < 2r``]
1272QED
1273
1274Theorem inv_mul[local]:
1275 !a b. a <> 0 /\ b <> 0 ==> (inv (a * inv b) = b / a)
1276Proof
1277 rw [realTheory.REAL_INV_MUL, realTheory.REAL_INV_NZ, realTheory.REAL_INV_INV]
1278 \\ simp [realTheory.REAL_INV_1OVER, realTheory.mult_ratl]
1279QED
1280
1281Theorem relative_error_zero[local]:
1282 !x. (x = 0) ==>
1283 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1284 (float_to_real (round roundTiesToEven x : ('t, 'w) float) =
1285 x * (1 + e))
1286Proof
1287 rw []
1288 \\ qexists_tac `0`
1289 \\ qspec_then `0`
1290 (fn th => simp [REWRITE_RULE [realTheory.REAL_SUB_RZERO] th])
1291 (GSYM error_def)
1292 \\ match_mp_tac error_is_zero
1293 \\ qexists_tac `float_plus_zero (:'t # 'w)`
1294 \\ simp [binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties]
1295QED
1296
1297Theorem relative_error:
1298 !x. normalizes (:'t # 'w) x ==>
1299 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1300 (float_to_real (round roundTiesToEven x : ('t, 'w) float) =
1301 x * (1 + e))
1302Proof
1303 rpt strip_tac
1304 \\ Cases_on `x = 0r`
1305 >- (match_mp_tac relative_error_zero \\ simp [])
1306 \\ imp_res_tac bias_imp_dimindex
1307 \\ `x < 0r \/ 0 < x` by (qpat_assum `x <> 0` MP_TAC \\ REAL_ARITH_TAC)
1308 \\ (qspec_then `x` mp_tac real_in_binade
1309 \\ rw_tac std_ss []
1310 \\ full_simp_tac std_ss [normalizes_def]
1311 \\ qspecl_then [`x`,`j`] MP_TAC error_bound_norm_strong
1312 \\ rw_tac std_ss []
1313 \\ `2 pow j * inv (2 pow (bias (:'w) - 1)) <= abs x =
1314 inv (abs x) <= inv (2 pow j * inv (2 pow (bias (:'w) - 1)))`
1315 by metis_tac [relative_bound_lem]
1316 \\ Q.UNDISCH_TAC `2 pow j / 2 pow (bias (:'w) - 1) <= abs x`
1317 \\ asm_simp_tac std_ss [real_div]
1318 \\ rw_tac std_ss []
1319 \\ `0 <= inv (abs x)` by simp [REAL_LE_INV_EQ, ABS_POS]
1320 \\ qspec_then `error (:'t # 'w) x` assume_tac ABS_POS
1321 \\ qspecl_then
1322 [`abs (error (:'t # 'w) x)`,
1323 `2 pow j / 2 pow (bias (:'w) + dimindex (:'t))`,
1324 `inv (abs x)`,
1325 `inv (2 pow j * inv (2 pow (bias (:'w) - 1)))`] mp_tac REAL_LE_MUL2
1326 \\ asm_simp_tac std_ss []
1327 \\ strip_tac
1328 \\ qexists_tac `error (:'t # 'w) x * inv x`
1329 \\ conj_tac
1330 >- (simp_tac std_ss [realTheory.ABS_MUL, realTheory.REAL_MUL_LID]
1331 \\ match_mp_tac realTheory.REAL_LE_TRANS
1332 \\ qexists_tac `2 pow j / 2 pow (bias (:'w) + dimindex (:'t)) *
1333 inv (2 pow j * inv (2 pow (bias (:'w) - 1)))`
1334 \\ asm_simp_tac std_ss [realTheory.ABS_INV]
1335 \\ simp_tac std_ss
1336 [inv_mul, realTheory.POW_NZ, REAL_ARITH ``2 <> 0r``,
1337 realTheory.REAL_POS_NZ, realTheory.REAL_INV_NZ,
1338 realTheory.REAL_DIV_OUTER_CANCEL]
1339 \\ simp [realTheory.REAL_INV_1OVER, realTheory.mult_ratl,
1340 realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_LE_RDIV_EQ]
1341 \\ simp [GSYM POW_ADD]
1342 \\ EVAL_TAC
1343 )
1344 \\ asm_simp_tac std_ss
1345 [error_def, REAL_LDISTRIB, REAL_MUL_RID, REAL_MUL_RINV,
1346 REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB, REAL_MUL_LID, REAL_SUB_ADD2,
1347 REAL_ARITH ``x * (float_to_real qq * inv x) =
1348 (x * inv x) * float_to_real qq``]
1349 )
1350QED
1351
1352(* -------------------------------------------------------------------------
1353 Ensure that the result is actually finite.
1354 ------------------------------------------------------------------------- *)
1355
1356Theorem float_round_finite:
1357 !b x. abs x < threshold (:'t # 'w) ==>
1358 float_is_finite (float_round roundTiesToEven b x : ('t, 'w) float)
1359Proof
1360 rw [float_round_def, round_def, binary_ieeeTheory.zero_properties,
1361 REAL_ARITH ``abs x < y = ~(x <= ~y) /\ ~(x >= y)``,
1362 REWRITE_RULE [pred_setTheory.GSPEC_ETA] is_finite_closest]
1363QED
1364
1365Theorem float_value_finite[local]:
1366 !a. float_is_finite a ==> (float_value a = Float (float_to_real a))
1367Proof
1368 Cases
1369 \\ rename [`float s e f`]
1370 \\ `float s e f = <| Sign := s; Exponent := e; Significand := f |>`
1371 by simp [float_component_equality]
1372 \\ simp [binary_ieeeTheory.float_tests, float_value_def]
1373QED
1374
1375(* -------------------------------------------------------------------------
1376 Lifting of arithmetic operations.
1377 ------------------------------------------------------------------------- *)
1378
1379Theorem finite_not[local]:
1380 !a. float_is_finite a ==> ~float_is_infinite a /\ ~float_is_nan a
1381Proof
1382 strip_tac
1383 \\ Cases_on `float_value a`
1384 \\ simp [float_is_finite_def, float_is_infinite_def, float_is_nan_def]
1385QED
1386
1387Theorem zero_le_ulp[local]:
1388 0 <= ulp (:'t # 'w)
1389Proof
1390 simp [ulp_def, ULP_def]
1391QED
1392
1393val round_zero =
1394 binary_ieeeTheory.round_roundTiesToEven_is_zero
1395 |> Q.SPEC `0`
1396 |> SIMP_RULE (srw_ss()) [zero_le_ulp]
1397
1398val lift_tac =
1399 rpt gen_tac
1400 \\ strip_tac
1401 \\ full_simp_tac (srw_ss()++real_SS++boolSimps.LET_ss)
1402 [float_value_finite, error_def, float_round_finite, normalizes_def,
1403 float_add_def, float_sub_def, float_mul_def, float_div_def,
1404 float_sqrt_def, float_mul_add_def, float_mul_sub_def,
1405 binary_ieeeTheory.float_is_zero_to_real, float_round_with_flags_def]
1406 \\ rw [float_round_finite, finite_not,
1407 binary_ieeeTheory.float_is_zero_to_real,
1408 binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties]
1409 \\ rw [float_round_def, finite_not, binary_ieeeTheory.float_is_zero_to_real,
1410 binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties]
1411
1412Theorem float_add:
1413 !a b : ('t, 'w) float.
1414 float_is_finite a /\ float_is_finite b /\
1415 abs (float_to_real a + float_to_real b) < threshold (:'t # 'w) ==>
1416 float_is_finite (SND (float_add roundTiesToEven a b)) /\
1417 (float_to_real (SND (float_add roundTiesToEven a b)) =
1418 float_to_real a + float_to_real b +
1419 error (:'t # 'w) (float_to_real a + float_to_real b))
1420Proof
1421 lift_tac
1422QED
1423
1424Theorem float_sub:
1425 !a b : ('t, 'w) float.
1426 float_is_finite a /\ float_is_finite b /\
1427 abs (float_to_real a - float_to_real b) < threshold (:'t # 'w) ==>
1428 float_is_finite (SND (float_sub roundTiesToEven a b)) /\
1429 (float_to_real (SND (float_sub roundTiesToEven a b)) =
1430 float_to_real a - float_to_real b +
1431 error (:'t # 'w) (float_to_real a - float_to_real b))
1432Proof
1433 lift_tac
1434QED
1435
1436Theorem float_mul:
1437 !a b : ('t, 'w) float.
1438 float_is_finite a /\ float_is_finite b /\
1439 abs (float_to_real a * float_to_real b) < threshold (:'t # 'w) ==>
1440 float_is_finite (SND (float_mul roundTiesToEven a b)) /\
1441 (float_to_real (SND (float_mul roundTiesToEven a b)) =
1442 float_to_real a * float_to_real b +
1443 error (:'t # 'w) (float_to_real a * float_to_real b))
1444Proof
1445 lift_tac
1446QED
1447
1448Theorem float_div:
1449 !a b : ('t, 'w) float.
1450 float_is_finite a /\ float_is_finite b /\ ~float_is_zero b /\
1451 abs (float_to_real a / float_to_real b) < threshold (:'t # 'w) ==>
1452 float_is_finite (SND (float_div roundTiesToEven a b)) /\
1453 (float_to_real (SND (float_div roundTiesToEven a b)) =
1454 float_to_real a / float_to_real b +
1455 error (:'t # 'w) (float_to_real a / float_to_real b))
1456Proof
1457 lift_tac
1458QED
1459
1460Definition sqrtable_def:
1461 sqrtable f <=> (f.Sign = 0w) \/ (f = NEG0)
1462End
1463
1464Theorem float_sqrt:
1465 !a : ('t, 'w) float.
1466 float_is_finite a /\ sqrtable a /\
1467 abs (sqrt (float_to_real a)) < threshold (:'t # 'w) ==>
1468 float_is_finite (SND (float_sqrt roundTiesToEven a)) /\
1469 (float_to_real (SND (float_sqrt roundTiesToEven a)) =
1470 sqrt (float_to_real a) + error (:'t # 'w) (sqrt (float_to_real a)))
1471Proof
1472 lift_tac >> gvs[sqrtable_def, SQRT_0]
1473QED
1474
1475Theorem float_mul_add:
1476 !a b c : ('t, 'w) float.
1477 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1478 abs (float_to_real a * float_to_real b + float_to_real c) <
1479 threshold (:'t # 'w) ==>
1480 float_is_finite (SND (float_mul_add roundTiesToEven a b c)) /\
1481 (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
1482 float_to_real a * float_to_real b + float_to_real c +
1483 error (:'t # 'w) (float_to_real a * float_to_real b + float_to_real c))
1484Proof
1485 lift_tac
1486QED
1487
1488Theorem float_mul_sub:
1489 !a b c : ('t, 'w) float.
1490 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1491 abs (float_to_real a * float_to_real b - float_to_real c) <
1492 threshold (:'t # 'w) ==>
1493 float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) /\
1494 (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
1495 float_to_real a * float_to_real b - float_to_real c +
1496 error (:'t # 'w) (float_to_real a * float_to_real b - float_to_real c))
1497Proof
1498 lift_tac
1499QED
1500
1501(*-----------------------*)
1502
1503fun try_gen q th = Q.GEN q th handle HOL_ERR _ => th
1504
1505val finite_rule =
1506 Q.GEN `a` o try_gen `b` o try_gen `c` o
1507 MATCH_MP (DECIDE ``(X ==> a /\ b) ==> (X ==> a)``) o
1508 Drule.SPEC_ALL
1509
1510Theorem float_add_finite = finite_rule float_add
1511Theorem float_sub_finite = finite_rule float_sub
1512Theorem float_mul_finite = finite_rule float_mul
1513Theorem float_div_finite = finite_rule float_div
1514Theorem float_sqrt_finite = finite_rule float_sqrt
1515
1516Theorem float_mul_add_finite =
1517 finite_rule float_mul_add
1518
1519Theorem float_mul_sub_finite =
1520 finite_rule float_mul_sub
1521
1522(*-----------------------*)
1523
1524val relative_tac =
1525 rpt gen_tac
1526 \\ strip_tac
1527 \\ conj_tac
1528 >- fs [normalizes_def, float_add_finite, float_sub_finite, float_mul_finite,
1529 float_div_finite, float_sqrt_finite, float_mul_add_finite,
1530 float_mul_sub_finite]
1531 \\ imp_res_tac relative_error
1532 \\ qexists_tac `e`
1533 \\ full_simp_tac (srw_ss()++real_SS++boolSimps.LET_ss)
1534 [float_value_finite, error_def, float_round_finite, normalizes_def,
1535 float_add_def, float_sub_def, float_mul_def, float_div_def,
1536 float_sqrt_def, float_mul_add_def, float_mul_sub_def,
1537 binary_ieeeTheory.float_is_zero_to_real,
1538 float_round_with_flags_def]
1539 \\ rw [float_round_def, binary_ieeeTheory.float_is_zero_to_real, finite_not,
1540 binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties]
1541 \\ rw [real_to_float_def, float_round_def, finite_not,
1542 binary_ieeeTheory.float_is_zero_to_real,
1543 binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties]
1544
1545val denorm_relative_tac =
1546 rpt gen_tac
1547 \\ strip_tac
1548 \\ conj_tac
1549 >- fs [float_add_finite, float_sub_finite, float_mul_finite,
1550 float_div_finite, float_sqrt_finite, float_mul_add_finite,
1551 float_mul_sub_finite]
1552 \\ last_assum (mp_then Any mp_tac error_bound_norm_strong)
1553 \\ disch_then (qspec_then `0` mp_tac)
1554 \\ impl_tac >- fs[]
1555 \\ qmatch_abbrev_tac `abs (err_op) <= _ ==> _`
1556 \\ strip_tac
1557 \\ qexists_tac `err_op`
1558 \\ unabbrev_all_tac \\ fs[error_def]
1559 \\ full_simp_tac (srw_ss()++real_SS++boolSimps.LET_ss)
1560 [float_value_finite, error_def, float_round_finite, normalizes_def,
1561 float_add_def, float_sub_def, float_mul_def, float_div_def,
1562 float_sqrt_def, float_mul_add_def, float_mul_sub_def,
1563 binary_ieeeTheory.float_is_zero_to_real,
1564 float_round_with_flags_def]
1565 \\ rw [float_round_def, binary_ieeeTheory.float_is_zero_to_real, finite_not,
1566 binary_ieeeTheory.zero_to_real, binary_ieeeTheory.zero_properties];
1567
1568Theorem float_add_relative:
1569 !a b : ('t, 'w) float.
1570 float_is_finite a /\ float_is_finite b /\
1571 normalizes (:'t # 'w) (float_to_real a + float_to_real b) ==>
1572 float_is_finite (SND (float_add roundTiesToEven a b)) /\
1573 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1574 (float_to_real (SND (float_add roundTiesToEven a b)) =
1575 (float_to_real a + float_to_real b) * (1 + e))
1576Proof
1577 relative_tac
1578QED
1579
1580Theorem float_add_relative_denorm:
1581 !a b : ('t, 'w) float.
1582 float_is_finite a /\ float_is_finite b /\
1583 abs (float_to_real a + float_to_real b) < 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1584 abs (float_to_real a + float_to_real b) < threshold (:'t # 'w) /\
1585 1 < bias (:'w) ==>
1586 float_is_finite (SND (float_add roundTiesToEven a b)) /\
1587 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1588 (float_to_real (SND (float_add roundTiesToEven a b)) =
1589 (float_to_real a + float_to_real b) + e)
1590Proof
1591 denorm_relative_tac
1592QED
1593
1594Theorem float_sub_relative:
1595 !a b : ('t, 'w) float.
1596 float_is_finite a /\ float_is_finite b /\
1597 normalizes (:'t # 'w) (float_to_real a - float_to_real b) ==>
1598 float_is_finite (SND (float_sub roundTiesToEven a b)) /\
1599 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1600 (float_to_real (SND (float_sub roundTiesToEven a b)) =
1601 (float_to_real a - float_to_real b) * (1 + e))
1602Proof
1603 relative_tac
1604QED
1605
1606Theorem float_sub_relative_denorm:
1607 !a b : ('t, 'w) float.
1608 float_is_finite a /\ float_is_finite b /\
1609 abs (float_to_real a - float_to_real b) < 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1610 abs (float_to_real a - float_to_real b) < threshold (:'t # 'w) /\
1611 1 < bias (:'w) ==>
1612 float_is_finite (SND (float_sub roundTiesToEven a b)) /\
1613 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1614 (float_to_real (SND (float_sub roundTiesToEven a b)) =
1615 (float_to_real a - float_to_real b) + e)
1616Proof
1617 denorm_relative_tac
1618QED
1619
1620Theorem float_mul_relative:
1621 !a b : ('t, 'w) float.
1622 float_is_finite a /\ float_is_finite b /\
1623 normalizes (:'t # 'w) (float_to_real a * float_to_real b) ==>
1624 float_is_finite (SND (float_mul roundTiesToEven a b)) /\
1625 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1626 (float_to_real (SND (float_mul roundTiesToEven a b)) =
1627 (float_to_real a * float_to_real b) * (1 + e))
1628Proof
1629 relative_tac
1630QED
1631
1632Theorem float_mul_relative_denorm:
1633 !a b : ('t, 'w) float.
1634 float_is_finite a /\ float_is_finite b /\
1635 abs (float_to_real a * float_to_real b) < 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1636 abs (float_to_real a * float_to_real b) < threshold (:'t # 'w) /\
1637 1 < bias (:'w) ==>
1638 float_is_finite (SND (float_mul roundTiesToEven a b)) /\
1639 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1640 (float_to_real (SND (float_mul roundTiesToEven a b)) =
1641 (float_to_real a * float_to_real b) + e)
1642Proof
1643 denorm_relative_tac
1644QED
1645
1646Theorem float_div_relative:
1647 !a b : ('t, 'w) float.
1648 float_is_finite a /\ float_is_finite b /\ ~float_is_zero b /\
1649 normalizes (:'t # 'w) (float_to_real a / float_to_real b) ==>
1650 float_is_finite (SND (float_div roundTiesToEven a b)) /\
1651 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1652 (float_to_real (SND (float_div roundTiesToEven a b)) =
1653 (float_to_real a / float_to_real b) * (1 + e))
1654Proof
1655 relative_tac
1656QED
1657
1658Theorem float_div_relative_denorm:
1659 !a b : ('t, 'w) float.
1660 float_is_finite a /\ float_is_finite b /\ ~float_is_zero b /\
1661 abs (float_to_real a / float_to_real b) < 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1662 abs (float_to_real a / float_to_real b) < threshold (:'t # 'w) /\
1663 1 < bias (:'w) ==>
1664 float_is_finite (SND (float_div roundTiesToEven a b)) /\
1665 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1666 (float_to_real (SND (float_div roundTiesToEven a b)) =
1667 (float_to_real a / float_to_real b) + e)
1668Proof
1669 denorm_relative_tac
1670QED
1671
1672Theorem float_sqrt_relative:
1673 !a : ('t, 'w) float.
1674 float_is_finite a /\ sqrtable a /\
1675 normalizes (:'t # 'w) (sqrt (float_to_real a)) ==>
1676 float_is_finite (SND (float_sqrt roundTiesToEven a)) /\
1677 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1678 (float_to_real (SND (float_sqrt roundTiesToEven a)) =
1679 (sqrt (float_to_real a) * (1 + e)))
1680Proof
1681 relative_tac >> gvs[SQRT_0, sqrtable_def]
1682QED
1683
1684Theorem float_sqrt_relative_denorm:
1685 !a : ('t, 'w) float.
1686 float_is_finite a /\ sqrtable a /\
1687 abs (sqrt (float_to_real a)) < 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1688 abs (sqrt (float_to_real a)) < threshold (:'t # 'w) /\
1689 1 < bias (:'w) ==>
1690 float_is_finite (SND (float_sqrt roundTiesToEven a)) /\
1691 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1692 (float_to_real (SND (float_sqrt roundTiesToEven a)) =
1693 (sqrt (float_to_real a) + e))
1694Proof
1695 denorm_relative_tac >> gs[sqrtable_def, SQRT_0, float_to_real_round0]
1696QED
1697
1698Theorem float_mul_add_relative:
1699 !a b c : ('t, 'w) float.
1700 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1701 normalizes (:'t # 'w)
1702 (float_to_real a * float_to_real b + float_to_real c) ==>
1703 float_is_finite (SND (float_mul_add roundTiesToEven a b c)) /\
1704 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1705 (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
1706 (float_to_real a * float_to_real b + float_to_real c) * (1 + e))
1707Proof
1708 relative_tac
1709QED
1710
1711Theorem float_mul_add_relative_denorm:
1712 !a b c: ('t, 'w) float.
1713 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1714 abs (float_to_real a * float_to_real b + float_to_real c) <
1715 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1716 abs (float_to_real a * float_to_real b + float_to_real c) <
1717 threshold (:'t # 'w) /\
1718 1 < bias (:'w) ==>
1719 float_is_finite (SND (float_mul_add roundTiesToEven a b c)) /\
1720 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1721 (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
1722 (float_to_real a * float_to_real b + float_to_real c) + e)
1723Proof
1724 denorm_relative_tac
1725QED
1726
1727Theorem float_mul_sub_relative:
1728 !a b c : ('t, 'w) float.
1729 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1730 normalizes (:'t # 'w)
1731 (float_to_real a * float_to_real b - float_to_real c) ==>
1732 float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) /\
1733 ?e. abs e <= 1 / 2 pow (dimindex (:'t) + 1) /\
1734 (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
1735 (float_to_real a * float_to_real b - float_to_real c) * (1 + e))
1736Proof
1737 relative_tac
1738QED
1739
1740Theorem float_mul_sub_relative_denorm:
1741 !a b c: ('t, 'w) float.
1742 float_is_finite a /\ float_is_finite b /\ float_is_finite c /\
1743 abs (float_to_real a * float_to_real b - float_to_real c) <
1744 2 pow 1 / 2 pow (bias (:'w) - 1) /\
1745 abs (float_to_real a * float_to_real b - float_to_real c) <
1746 threshold (:'t # 'w) /\
1747 1 < bias (:'w) ==>
1748 float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) /\
1749 ?e. abs e <= 1 / 2 pow (bias(:'w) + dimindex (:'t)) /\
1750 (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
1751 (float_to_real a * float_to_real b - float_to_real c) + e)
1752Proof
1753 denorm_relative_tac
1754QED
1755
1756(* ------------------------------------------------------------------------- *)
1757
1758Theorem finite_float_within_threshold:
1759 !f:('a , 'b) float.
1760 float_is_finite f ==>
1761 ~(float_to_real f <= -threshold (:'a # 'b)) /\
1762 ~(float_to_real f >= threshold (:'a # 'b))
1763Proof
1764 rpt strip_tac
1765 \\ Q.ISPECL_THEN [`f`] assume_tac float_to_real_threshold
1766 \\ fs[realTheory.abs]
1767 \\ BasicProvers.every_case_tac
1768 \\ res_tac
1769 \\ REAL_ASM_ARITH_TAC
1770QED
1771
1772Theorem round_finite_normal_float_id:
1773 !f.
1774 float_is_finite f /\
1775 ~ float_is_zero f ==>
1776 (round roundTiesToEven (float_to_real f) = f)
1777Proof
1778 rw[]
1779 \\ qpat_assum `float_is_finite _` mp_tac
1780 \\ rewrite_tac [float_is_finite_def, float_value_def]
1781 \\ simp[]
1782 \\ strip_tac
1783 \\ once_rewrite_tac [round_def]
1784 \\ fs[finite_float_within_threshold]
1785 \\ once_rewrite_tac [closest_such_def]
1786 \\ SELECT_ELIM_TAC
1787 \\ rw[]
1788 >- (qexists_tac `f`
1789 \\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS]
1790 \\ Cases_on `f = b` \\ fs[]
1791 \\ first_x_assum (qspec_then `f` mp_tac)
1792 \\ fs[realTheory.REAL_SUB_REFL]
1793 \\ strip_tac
1794 \\ `float_to_real b - float_to_real f = 0`
1795 by (REAL_ASM_ARITH_TAC)
1796 \\ fs[float_to_real_eq]
1797 \\ rfs[])
1798 \\ CCONTR_TAC
1799 \\ fs[is_closest_def, IN_DEF]
1800 \\ qpat_x_assum `!x._ ` mp_tac
1801 \\ first_x_assum (qspec_then `f` mp_tac)
1802 \\ fs[realTheory.REAL_SUB_REFL]
1803 \\ rpt strip_tac
1804 \\ `float_to_real x - float_to_real f = 0`
1805 by (REAL_ASM_ARITH_TAC)
1806 \\ fs[float_to_real_eq]
1807 \\ rfs[]
1808QED
1809
1810Theorem real_to_float_finite_normal_id:
1811 !f.
1812 float_is_finite f /\
1813 ~ float_is_zero f ==>
1814 (real_to_float roundTiesToEven (float_to_real f) = f)
1815Proof
1816 rpt strip_tac
1817 \\ fs[real_to_float_def, float_round_def, round_finite_normal_float_id]
1818QED
1819
1820Theorem float_to_real_real_to_float_zero_id:
1821 float_to_real (real_to_float roundTiesToEven 0) = 0
1822Proof
1823 once_rewrite_tac[real_to_float_def]
1824 \\ `float_round roundTiesToEven F 0 = (float_plus_zero(:'a # 'b))`
1825 by (irule round_roundTiesToEven_is_plus_zero
1826 \\ fs[ulp_def, ULP_def])
1827 \\ fs[float_to_real_def, float_plus_zero_def]
1828QED
1829
1830Theorem non_representable_float_is_zero:
1831 !ff P.
1832 2 * abs ff <= ulp ((:'a#'b) :('a#'b) itself) ==>
1833 (float_to_real ((float_round roundTiesToEven P ff):('a, 'b) float) = 0)
1834Proof
1835 rpt strip_tac \\ Cases_on `P`
1836 \\ fs [round_roundTiesToEven_is_plus_zero,
1837 round_roundTiesToEven_is_minus_zero, zero_to_real]
1838QED