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