1(* ------------------------------------------------------------------------ 2 Theory of IEEE-754 (base 2) floating-point (basic) arithmetic 3 ------------------------------------------------------------------------ *) 4 5open HolKernel boolLib bossLib 6open intrealTheory realLib wordsLib 7 8val () = new_theory "binary_ieee" 9val _ = ParseExtras.temp_loose_equality() 10val _ = diminish_srw_ss ["RMULCANON_ss","RMULRELNORM_ss","NORMEQ_ss"] 11 12local 13 open String 14 val mesg_to_string = !Feedback.MESG_to_string 15 fun f s = if isPrefix "mk_functional" s andalso isSubstring "completion" s 16 then "" 17 else mesg_to_string s 18in 19 val () = Feedback.set_trace "Theory.save_thm_reporting" 0 20 val () = Feedback.MESG_to_string := f 21end 22 23val Define = bossLib.zDefine 24 25(* ------------------------------------------------------------------------ 26 Binary floating point representation 27 ------------------------------------------------------------------------ *) 28 29val () = Datatype` 30 float = <| Sign : word1; Exponent : 'w word; Significand : 't word |>` 31 32(* ------------------------------------------------------------------------ 33 Maps to other representations 34 ------------------------------------------------------------------------ *) 35 36val () = Datatype `float_value = Float real | Infinity | NaN` 37 38val () = List.app Parse.temp_overload_on 39 [("precision", ``fcp$dimindex``), ("bias", ``words$INT_MAX``)] 40 41val float_to_real_def = Define` 42 float_to_real (x: ('t, 'w) float) = 43 if x.Exponent = 0w 44 then -1r pow (w2n x.Sign) * 45 (2r / 2r pow (bias (:'w))) * 46 (&(w2n x.Significand) / 2r pow (precision (:'t))) 47 else -1r pow (w2n x.Sign) * 48 (2r pow (w2n x.Exponent) / 2r pow (bias (:'w))) * 49 (1r + &(w2n x.Significand) / 2r pow (precision (:'t)))` 50 51val float_value_def = Define` 52 float_value (x: ('t, 'w) float) = 53 if x.Exponent = UINT_MAXw 54 then if x.Significand = 0w then Infinity else NaN 55 else Float (float_to_real x)` 56 57(* ------------------------------------------------------------------------ 58 Tests 59 ------------------------------------------------------------------------ *) 60 61val float_is_nan_def = Define` 62 float_is_nan (x: ('t, 'w) float) = 63 case float_value x of 64 NaN => T 65 | _ => F` 66 67val float_is_signalling_def = Define` 68 float_is_signalling (x: ('t, 'w) float) = 69 float_is_nan x /\ ~word_msb x.Significand` 70 71val float_is_infinite_def = Define` 72 float_is_infinite (x: ('t, 'w) float) = 73 case float_value x of 74 Infinity => T 75 | _ => F` 76 77val float_is_normal_def = Define` 78 float_is_normal (x: ('t, 'w) float) = 79 x.Exponent <> 0w /\ x.Exponent <> UINT_MAXw` 80 81val float_is_subnormal_def = Define` 82 float_is_subnormal (x: ('t, 'w) float) = 83 (x.Exponent = 0w) /\ x.Significand <> 0w` 84 85val float_is_zero_def = Define` 86 float_is_zero (x: ('t, 'w) float) = 87 case float_value x of 88 Float r => r = 0 89 | _ => F` 90 91val float_is_finite_def = Define` 92 float_is_finite (x: ('t, 'w) float) = 93 case float_value x of 94 Float _ => T 95 | _ => F` 96 97val is_integral_def = Define `is_integral r = ?n. abs r = &(n:num)` 98 99val float_is_integral_def = Define` 100 float_is_integral (x: ('t, 'w) float) = 101 case float_value x of 102 Float r => is_integral r 103 | _ => F` 104 105(* ------------------------------------------------------------------------ 106 Abs and Negate 107 (On some architectures the signalling behaviour changes from IEEE754:1985 108 and IEEE754:2008) 109 ------------------------------------------------------------------------ *) 110 111val float_negate_def = Define` 112 float_negate (x: ('t, 'w) float) = x with Sign := ~x.Sign` 113 114val float_abs_def = Define` 115 float_abs (x: ('t, 'w) float) = x with Sign := 0w` 116 117(* ------------------------------------------------------------------------ 118 Some constants 119 ------------------------------------------------------------------------ *) 120 121val float_plus_infinity_def = Define` 122 float_plus_infinity (:'t # 'w) = 123 <| Sign := 0w; 124 Exponent := UINT_MAXw: 'w word; 125 Significand := 0w: 't word |>` 126 127val float_plus_zero_def = Define` 128 float_plus_zero (:'t # 'w) = 129 <| Sign := 0w; 130 Exponent := 0w: 'w word; 131 Significand := 0w: 't word |>` 132 133val float_top_def = Define` 134 float_top (:'t # 'w) = 135 <| Sign := 0w; 136 Exponent := UINT_MAXw - 1w: 'w word; 137 Significand := UINT_MAXw: 't word |>` 138 139val float_plus_min_def = Define` 140 float_plus_min (:'t # 'w) = 141 <| Sign := 0w; 142 Exponent := 0w: 'w word; 143 Significand := 1w: 't word |>` 144 145val float_minus_infinity_def = Define` 146 float_minus_infinity (:'t # 'w) = 147 float_negate (float_plus_infinity (:'t # 'w))` 148 149val float_minus_zero_def = Define` 150 float_minus_zero (:'t # 'w) = float_negate (float_plus_zero (:'t # 'w))` 151 152val float_bottom_def = Define` 153 float_bottom (:'t # 'w) = float_negate (float_top (:'t # 'w))` 154 155val float_minus_min_def = Define` 156 float_minus_min (:'t # 'w) = float_negate (float_plus_min (:'t # 'w))` 157 158(* ------------------------------------------------------------------------ 159 Rounding reals to floating-point values 160 ------------------------------------------------------------------------ *) 161 162val () = Datatype` 163 flags = <| DivideByZero : bool 164 ; InvalidOp : bool 165 ; Overflow : bool 166 ; Precision : bool 167 ; Underflow_BeforeRounding : bool 168 ; Underflow_AfterRounding : bool 169 |>` 170 171val clear_flags_def = Define` 172 clear_flags = <| DivideByZero := F 173 ; InvalidOp := F 174 ; Overflow := F 175 ; Precision := F 176 ; Underflow_BeforeRounding := F 177 ; Underflow_AfterRounding := F 178 |>` 179 180val invalidop_flags_def = Define` 181 invalidop_flags = clear_flags with InvalidOp := T` 182 183val dividezero_flags_def = Define` 184 dividezero_flags = clear_flags with DivideByZero := T` 185 186val () = Datatype` 187 rounding = roundTiesToEven 188 | roundTowardPositive 189 | roundTowardNegative 190 | roundTowardZero` 191 192val is_closest_def = Define` 193 is_closest s x a = 194 a IN s /\ 195 !b. b IN s ==> abs (float_to_real a - x) <= abs (float_to_real b - x)` 196 197val closest_such_def = Define` 198 closest_such p s x = 199 @a. is_closest s x a /\ (!b. is_closest s x b /\ p b ==> p a)` 200 201val closest_def = Define `closest = closest_such (K T)` 202 203val largest_def = Define` 204 largest (:'t # 'w) = 205 (2r pow (UINT_MAX (:'w) - 1) / 2r pow (INT_MAX (:'w))) * 206 (2r - inv (2r pow dimindex(:'t)))` 207 208val threshold_def = Define` 209 threshold (:'t # 'w) = 210 (2r pow (UINT_MAX (:'w) - 1) / 2r pow (INT_MAX (:'w))) * 211 (2r - inv (2r pow SUC (dimindex(:'t))))` 212 213(* Unit in the Last Place (of least precision) *) 214 215(* For a given exponent (applies when significand is not zero) *) 216 217val ULP_def = Define` 218 ULP (e:'w word, (:'t)) = 219 2 pow (if e = 0w then 1 else w2n e) / 2 pow (bias (:'w) + precision (:'t))` 220 221(* Smallest ULP *) 222 223val ulp_def = Define `ulp (:'t # 'w) = ULP (0w:'w word, (:'t))` 224 225(* rounding *) 226 227val round_def = Define` 228 round mode (x: real) = 229 case mode of 230 roundTiesToEven => 231 let t = threshold (:'t # 'w) in 232 if x <= -t 233 then float_minus_infinity (:'t # 'w) 234 else if x >= t 235 then float_plus_infinity (:'t # 'w) 236 else closest_such (\a. ~word_lsb a.Significand) float_is_finite x 237 | roundTowardZero => 238 let t = largest (:'t # 'w) in 239 if x < -t 240 then float_bottom (:'t # 'w) 241 else if x > t 242 then float_top (:'t # 'w) 243 else closest 244 {a | float_is_finite a /\ abs (float_to_real a) <= abs x} x 245 | roundTowardPositive => 246 let t = largest (:'t # 'w) in 247 if x < -t 248 then float_bottom (:'t # 'w) 249 else if x > t 250 then float_plus_infinity (:'t # 'w) 251 else closest {a | float_is_finite a /\ float_to_real a >= x} x 252 | roundTowardNegative => 253 let t = largest (:'t # 'w) in 254 if x < -t 255 then float_minus_infinity (:'t # 'w) 256 else if x > t 257 then float_top (:'t # 'w) 258 else closest {a | float_is_finite a /\ float_to_real a <= x} x` 259 260val integral_round_def = Define` 261 integral_round mode (x: real) = 262 case mode of 263 roundTiesToEven => 264 let t = threshold (:'t # 'w) in 265 if x <= -t 266 then float_minus_infinity (:'t # 'w) 267 else if x >= t 268 then float_plus_infinity (:'t # 'w) 269 else closest_such (\a. ?n. EVEN n /\ (abs (float_to_real a) = &n)) 270 float_is_integral x 271 | roundTowardZero => 272 let t = largest (:'t # 'w) in 273 if x < -t 274 then float_bottom (:'t # 'w) 275 else if x > t 276 then float_top (:'t # 'w) 277 else closest 278 {a | float_is_integral a /\ abs (float_to_real a) <= abs x} x 279 | roundTowardPositive => 280 let t = largest (:'t # 'w) in 281 if x < -t 282 then float_bottom (:'t # 'w) 283 else if x > t 284 then float_plus_infinity (:'t # 'w) 285 else closest {a | float_is_integral a /\ float_to_real a >= x} x 286 | roundTowardNegative => 287 let t = largest (:'t # 'w) in 288 if x < -t 289 then float_minus_infinity (:'t # 'w) 290 else if x > t 291 then float_top (:'t # 'w) 292 else closest {a | float_is_integral a /\ float_to_real a <= x} x` 293 294(* ------------------------------------------------------------------------ 295 NaNs 296 ------------------------------------------------------------------------ *) 297 298val () = Datatype` 299 fp_op = 300 FP_Sqrt rounding (('t, 'w) float) 301 | FP_Add rounding (('t, 'w) float) (('t, 'w) float) 302 | FP_Sub rounding (('t, 'w) float) (('t, 'w) float) 303 | FP_Mul rounding (('t, 'w) float) (('t, 'w) float) 304 | FP_Div rounding (('t, 'w) float) (('t, 'w) float) 305 | FP_MulAdd rounding (('t, 'w) float) (('t, 'w) float) (('t, 'w) float) 306 | FP_MulSub rounding (('t, 'w) float) (('t, 'w) float) (('t, 'w) float)` 307 308val float_some_qnan_def = Define` 309 float_some_qnan (fp_op : ('t, 'w) fp_op) = 310 (@f. let qnan = f fp_op in float_is_nan qnan /\ ~float_is_signalling qnan) 311 fp_op : ('t, 'w) float` 312 313(* ------------------------------------------------------------------------ 314 Some arithmetic operations 315 ------------------------------------------------------------------------ *) 316 317(* Round, choosing between -0.0 or +0.0 *) 318 319val float_round_def = Define` 320 float_round mode toneg r = 321 let x = round mode r in 322 if float_is_zero x 323 then if toneg 324 then float_minus_zero (:'t # 'w) 325 else float_plus_zero (:'t # 'w) 326 else x` 327 328val float_round_with_flags_def = Define` 329 float_round_with_flags mode to_neg r = 330 let x = float_round mode to_neg r : ('t, 'w) float and a = abs r in 331 let inexact = float_value x <> Float r in 332 ((clear_flags with 333 <| Overflow := (float_is_infinite x \/ 2 pow (INT_MIN (:'w)) <= a) 334 (* IEEE-754 permits a number of ways to detect underflow. Below 335 are two possible methods. *) 336 ; Underflow_BeforeRounding := (inexact /\ a < 2 / 2 pow (bias(:'w))) 337 ; Underflow_AfterRounding := 338 (inexact /\ 339 ((float_round mode to_neg r : ('t, 'w + 1) float).Exponent <=+ 340 n2w (INT_MIN (:'w)))) 341 ; Precision := inexact 342 |>), x)` 343 344val check_for_signalling_def = Define` 345 check_for_signalling l = 346 clear_flags with InvalidOp := EXISTS float_is_signalling l` 347 348val real_to_float_def = Define` 349 real_to_float m = float_round m (m = roundTowardNegative)` 350 351val real_to_float_with_flags_def = Define` 352 real_to_float_with_flags m = 353 float_round_with_flags m (m = roundTowardNegative)` 354 355val float_round_to_integral_def = Define` 356 float_round_to_integral mode (x: ('t, 'w) float) = 357 case float_value x of 358 Float r => integral_round mode r 359 | _ => x` 360 361val float_to_int_def = Define` 362 float_to_int mode (x: ('t, 'w) float) = 363 case float_value x of 364 Float r => 365 SOME (case mode of 366 roundTiesToEven => 367 let f = INT_FLOOR r in 368 let df = abs (r - real_of_int f) in 369 if (df < 1r / 2) \/ (df = 1r / 2) /\ EVEN (Num (ABS f)) then 370 f 371 else 372 INT_CEILING r 373 | roundTowardPositive => INT_CEILING r 374 | roundTowardNegative => INT_FLOOR r 375 | roundTowardZero => 376 if x.Sign = 1w then INT_CEILING r else INT_FLOOR r) 377 | _ => NONE` 378 379val float_sqrt_def = Define` 380 float_sqrt mode (x: ('t, 'w) float) = 381 if x.Sign = 0w then 382 case float_value x of 383 NaN => (check_for_signalling [x], float_some_qnan (FP_Sqrt mode x)) 384 | Infinity => (clear_flags, float_plus_infinity (:'t # 'w)) 385 | Float r => (float_round_with_flags mode F (sqrt r)) 386 else 387 (invalidop_flags, float_some_qnan (FP_Sqrt mode x))` 388 389val float_add_def = Define` 390 float_add mode (x: ('t, 'w) float) (y: ('t, 'w) float) = 391 case float_value x, float_value y of 392 NaN, _ => (check_for_signalling [x; y], 393 float_some_qnan (FP_Add mode x y)) 394 | _, NaN => (check_for_signalling [y], 395 float_some_qnan (FP_Add mode x y)) 396 | Infinity, Infinity => 397 if x.Sign = y.Sign then 398 (clear_flags, x) 399 else 400 (invalidop_flags, float_some_qnan (FP_Add mode x y)) 401 | Infinity, _ => (clear_flags, x) 402 | _, Infinity => (clear_flags, y) 403 | Float r1, Float r2 => 404 float_round_with_flags mode 405 (if (r1 = 0) /\ (r2 = 0) /\ (x.Sign = y.Sign) then 406 x.Sign = 1w 407 else mode = roundTowardNegative) (r1 + r2)` 408 409val float_sub_def = Define` 410 float_sub mode (x: ('t, 'w) float) (y: ('t, 'w) float) = 411 case float_value x, float_value y of 412 NaN, _ => (check_for_signalling [x; y], 413 float_some_qnan (FP_Sub mode x y)) 414 | _, NaN => (check_for_signalling [y], 415 float_some_qnan (FP_Sub mode x y)) 416 | Infinity, Infinity => 417 if x.Sign = y.Sign then 418 (invalidop_flags, float_some_qnan (FP_Sub mode x y)) 419 else 420 (clear_flags, x) 421 | Infinity, _ => (clear_flags, x) 422 | _, Infinity => (clear_flags, float_negate y) 423 | Float r1, Float r2 => 424 float_round_with_flags mode 425 (if (r1 = 0) /\ (r2 = 0) /\ x.Sign <> y.Sign then 426 x.Sign = 1w 427 else mode = roundTowardNegative) (r1 - r2)` 428 429val float_mul_def = Define` 430 float_mul mode (x: ('t, 'w) float) (y: ('t, 'w) float) = 431 case float_value x, float_value y of 432 NaN, _ => (check_for_signalling [x; y], 433 float_some_qnan (FP_Mul mode x y)) 434 | _, NaN => (check_for_signalling [y], 435 float_some_qnan (FP_Mul mode x y)) 436 | Infinity, Float r => 437 if r = 0 then 438 (invalidop_flags, float_some_qnan (FP_Mul mode x y)) 439 else 440 (clear_flags, 441 if x.Sign = y.Sign then 442 float_plus_infinity (:'t # 'w) 443 else float_minus_infinity (:'t # 'w)) 444 | Float r, Infinity => 445 if r = 0 then 446 (invalidop_flags, float_some_qnan (FP_Mul mode x y)) 447 else 448 (clear_flags, 449 if x.Sign = y.Sign then 450 float_plus_infinity (:'t # 'w) 451 else float_minus_infinity (:'t # 'w)) 452 | Infinity, Infinity => 453 (clear_flags, 454 if x.Sign = y.Sign then 455 float_plus_infinity (:'t # 'w) 456 else float_minus_infinity (:'t # 'w)) 457 | Float r1, Float r2 => 458 float_round_with_flags mode (x.Sign <> y.Sign) (r1 * r2)` 459 460val float_div_def = Define` 461 float_div mode (x: ('t, 'w) float) (y: ('t, 'w) float) = 462 case float_value x, float_value y of 463 NaN, _ => (check_for_signalling [x; y], 464 float_some_qnan (FP_Div mode x y)) 465 | _, NaN => (check_for_signalling [y], 466 float_some_qnan (FP_Div mode x y)) 467 | Infinity, Infinity => 468 (invalidop_flags, float_some_qnan (FP_Div mode x y)) 469 | Infinity, _ => 470 (clear_flags, 471 if x.Sign = y.Sign then 472 float_plus_infinity (:'t # 'w) 473 else float_minus_infinity (:'t # 'w)) 474 | _, Infinity => 475 (clear_flags, 476 if x.Sign = y.Sign then 477 float_plus_zero (:'t # 'w) 478 else float_minus_zero (:'t # 'w)) 479 | Float r1, Float r2 => 480 if r2 = 0 481 then if r1 = 0 then 482 (invalidop_flags, float_some_qnan (FP_Div mode x y)) 483 else 484 (dividezero_flags, 485 if x.Sign = y.Sign then 486 float_plus_infinity (:'t # 'w) 487 else float_minus_infinity (:'t # 'w)) 488 else float_round_with_flags mode (x.Sign <> y.Sign) (r1 / r2)` 489 490val float_mul_add_def = Define` 491 float_mul_add mode 492 (x: ('t, 'w) float) (y: ('t, 'w) float) (z: ('t, 'w) float) = 493 let signP = x.Sign ?? y.Sign in 494 let infP = float_is_infinite x \/ float_is_infinite y 495 in 496 if float_is_nan x \/ float_is_nan y \/ float_is_nan z then 497 (check_for_signalling [x; y; z], 498 float_some_qnan (FP_MulAdd mode x y z)) 499 else if float_is_infinite x /\ float_is_zero y \/ 500 float_is_zero x /\ float_is_infinite y \/ 501 float_is_infinite z /\ infP /\ signP <> z.Sign then 502 (invalidop_flags, float_some_qnan (FP_MulAdd mode x y z)) 503 else if float_is_infinite z /\ (z.Sign = 0w) \/ infP /\ (signP = 0w) 504 then (clear_flags, float_plus_infinity (:'t # 'w)) 505 else if float_is_infinite z /\ (z.Sign = 1w) \/ infP /\ (signP = 1w) 506 then (clear_flags, float_minus_infinity (:'t # 'w)) 507 else 508 let r1 = float_to_real x * float_to_real y 509 and r2 = float_to_real z 510 in 511 float_round_with_flags mode 512 (if (r1 = 0) /\ (r2 = 0) /\ (signP = z.Sign) then 513 signP = 1w 514 else mode = roundTowardNegative) (r1 + r2)` 515 516val float_mul_sub_def = Define` 517 float_mul_sub mode 518 (x: ('t, 'w) float) (y: ('t, 'w) float) (z: ('t, 'w) float) = 519 let signP = x.Sign ?? y.Sign in 520 let infP = float_is_infinite x \/ float_is_infinite y 521 in 522 if float_is_nan x \/ float_is_nan y \/ float_is_nan z then 523 (check_for_signalling [x; y; z], 524 float_some_qnan (FP_MulSub mode x y z)) 525 else if float_is_infinite x /\ float_is_zero y \/ 526 float_is_zero x /\ float_is_infinite y \/ 527 float_is_infinite z /\ infP /\ (signP = z.Sign) then 528 (invalidop_flags, float_some_qnan (FP_MulAdd mode x y z)) 529 else if float_is_infinite z /\ (z.Sign = 1w) \/ infP /\ (signP = 0w) 530 then (clear_flags, float_plus_infinity (:'t # 'w)) 531 else if float_is_infinite z /\ (z.Sign = 0w) \/ infP /\ (signP = 1w) 532 then (clear_flags, float_minus_infinity (:'t # 'w)) 533 else 534 let r1 = float_to_real x * float_to_real y 535 and r2 = float_to_real z 536 in 537 float_round_with_flags mode 538 (if (r1 = 0) /\ (r2 = 0) /\ signP <> z.Sign then 539 signP = 1w 540 else mode = roundTowardNegative) (r1 - r2)` 541 542(* ------------------------------------------------------------------------ 543 Some comparison operations 544 ------------------------------------------------------------------------ *) 545 546val () = Datatype `float_compare = LT | EQ | GT | UN` 547 548val float_compare_def = Define` 549 float_compare (x: ('t, 'w) float) (y: ('t, 'w) float) = 550 case float_value x, float_value y of 551 NaN, _ => UN 552 | _, NaN => UN 553 | Infinity, Infinity => 554 if x.Sign = y.Sign 555 then EQ 556 else if x.Sign = 1w 557 then LT 558 else GT 559 | Infinity, _ => if x.Sign = 1w then LT else GT 560 | _, Infinity => if y.Sign = 1w then GT else LT 561 | Float r1, Float r2 => 562 if r1 < r2 563 then LT 564 else if r1 = r2 565 then EQ 566 else GT` 567 568val float_less_than_def = Define` 569 float_less_than (x: ('t, 'w) float) y = 570 (float_compare x y = LT)` 571 572val float_less_equal_def = Define` 573 float_less_equal (x: ('t, 'w) float) y = 574 case float_compare x y of 575 LT => T 576 | EQ => T 577 | _ => F` 578 579val float_greater_than_def = Define` 580 float_greater_than (x: ('t, 'w) float) y = 581 (float_compare x y = GT)` 582 583val float_greater_equal_def = Define` 584 float_greater_equal (x: ('t, 'w) float) y = 585 case float_compare x y of 586 GT => T 587 | EQ => T 588 | _ => F` 589 590val float_equal_def = Define` 591 float_equal (x: ('t, 'w) float) y = 592 (float_compare x y = EQ)` 593 594val exponent_boundary_def = Define` 595 exponent_boundary (y: ('t, 'w) float) (x: ('t, 'w) float) = 596 (x.Sign = y.Sign) /\ (w2n x.Exponent = w2n y.Exponent + 1) /\ 597 (x.Exponent <> 1w) /\ (y.Significand = -1w) /\ (x.Significand = 0w)` 598 599(* ------------------------------------------------------------------------ 600 Some arithmetic theorems 601 ------------------------------------------------------------------------ *) 602 603val () = Feedback.set_trace "Theory.save_thm_reporting" 1 604 605val rrw = SRW_TAC [boolSimps.LET_ss, realSimps.REAL_ARITH_ss] 606 607(* |- !n. 0 < 2 pow n *) 608Theorem zero_lt_twopow[simp] = 609 realTheory.REAL_POW_LT |> Q.SPEC `2` |> SIMP_RULE (srw_ss()) []; 610 611(* |- !n. 0 <= 2 pow n *) 612Theorem zero_le_twopow[simp] = 613 MATCH_MP realTheory.REAL_LT_IMP_LE (Drule.SPEC_ALL zero_lt_twopow) |> GEN_ALL; 614 615 616Theorem zero_neq_twopow: !n. 2 pow n <> 0 617Proof simp[] 618QED 619 620Theorem zero_le_pos_div_twopow[simp]: 621 !m n. 0 <= &m / 2 pow n 622Proof 623 rw [realTheory.REAL_LE_DIV, realTheory.REAL_LT_IMP_LE] 624QED 625 626Theorem div_eq0[simp]: 627 !a b. 0r < b ==> ((a / b = 0) = (a = 0)) 628Proof 629 rw [realTheory.REAL_EQ_LDIV_EQ] 630QED 631 632(* !b. 2 <= 2 ** b <=> 1 <= b *) 633Theorem exp_ge2[simp] = 634 logrootTheory.LE_EXP_ISO |> Q.SPECL [`2`, `1`] |> reduceLib.REDUCE_RULE 635 |> Conv.GSYM; 636 637 638(* !b. 4 <= 2 ** b <=> 2 <= b *) 639val exp_ge4 = 640 logrootTheory.LE_EXP_ISO 641 |> Q.SPECL [`2`, `2`] 642 |> reduceLib.REDUCE_RULE 643 |> Conv.GSYM 644 645Theorem exp_gt2[simp] = 646 logrootTheory.LT_EXP_ISO 647 |> Q.SPECL [`2`, `1`] 648 |> reduceLib.REDUCE_RULE 649 |> Conv.GSYM 650 ; 651 652(* !n x u. (x / 2 pow n = u / 2 pow n) <=> (x = u) *) 653val div_twopow = 654 realTheory.eq_rat 655 |> Q.INST [`y` |-> `2 pow n`, `v` |-> `2 pow n`] 656 |> SIMP_RULE (srw_ss()) [] 657 |> Q.GENL [`n`, `x`, `u`] 658 659val div_le = Q.prove( 660 `!a b c. 0r < a ==> (b / a <= c / a = b <= c)`, 661 metis_tac [realTheory.REAL_LE_LMUL, realTheory.REAL_DIV_RMUL, 662 realTheory.REAL_POS_NZ, realTheory.REAL_MUL_COMM] 663 ) 664 665val tac = 666 NTAC 2 strip_tac 667 \\ Cases_on `n <= 2` 668 >- (`(n = 1) \/ (n = 2)` by decide_tac \\ rw []) 669 \\ `2 < n` by decide_tac 670 \\ lrw [] 671 672val two_mod_not_one = Q.prove( 673 `!n. 0 < n ==> 2 MOD n <> 1`, tac) 674 675val two_mod_eq_zero = Q.prove( 676 `!n. 0 < n ==> ((2 MOD n = 0) = (n = 1) \/ (n = 2))`, 677 tac 678 ) 679 680(* |- !c a. c <> 0 ==> (c * a / c = a) *) 681val mul_cancel = 682 realTheory.REAL_DIV_LMUL_CANCEL 683 |> Drule.SPEC_ALL 684 |> Q.INST [`b` |-> `1`] 685 |> SIMP_RULE (srw_ss()) [] 686 |> Q.GENL [`a`, `c`] 687 688val ge2 = Q.prove( 689 `dimindex(:'a) <> 1 ==> 2 <= dimindex (:'a)`, 690 rw [DECIDE ``0 < a /\ a <> 1 ==> 2n <= a``]) 691 692val ge2b = Q.prove( 693 `!n. 2n <= n ==> 1 <= 2n ** (n - 1) - 1`, 694 REPEAT strip_tac 695 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 696 \\ simp [arithmeticTheory.EXP_ADD, DECIDE ``0 < n ==> 1n <= 2 * n - 1``]) 697 698val ge2c = Q.prove( 699 `!n m. 1r <= n /\ 2 < m ==> 2 < n * m`, 700 rrw [GSYM realTheory.REAL_LT_LDIV_EQ] 701 \\ `2r / m < 1` by (match_mp_tac realTheory.REAL_LT_1 \\ simp []) 702 \\ METIS_TAC [realTheory.REAL_LTE_TRANS] 703 ) 704 705val ge1_pow = Q.prove( 706 `!a b. 1 <= a /\ 1n <= b ==> a <= a pow b`, 707 Induct_on `b` 708 \\ rw [realTheory.pow] 709 \\ once_rewrite_tac [realTheory.REAL_MUL_COMM] 710 \\ `0r < a /\ a <> 0` 711 by METIS_TAC [realLib.REAL_ARITH ``1 <= a ==> 0r < a``, 712 realTheory.REAL_POS_NZ] 713 \\ simp [GSYM realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_DIV_REFL] 714 \\ Cases_on `b = 0` 715 \\ simp [] 716 \\ `1 <= b` by decide_tac 717 \\ metis_tac [realTheory.REAL_LE_TRANS] 718 ) 719 720(* |- !n x. 1 < x /\ 1 < n ==> x < x pow n *) 721val gt1_pow = 722 realTheory.REAL_POW_MONO_LT 723 |> Q.SPEC `1` 724 |> REWRITE_RULE [realTheory.POW_1] 725 726(* |- !a b. 2 <= a /\ 1 <= b ==> 2 <= a * b *) 727val prod_ge2 = 728 realTheory.REAL_LE_MUL2 729 |> Q.SPECL [`2`, `a`, `1`, `b`] 730 |> SIMP_RULE (srw_ss()) [] 731 |> Q.GENL [`a`, `b`] 732 733val le1 = Q.prove( 734 `!x y. 0 < y /\ x <= y ==> x / y <= 1r`, 735 REPEAT STRIP_TAC 736 \\ Cases_on `x = y` 737 \\ ASM_SIMP_TAC bool_ss 738 [realTheory.REAL_LE_REFL, realTheory.REAL_DIV_REFL, 739 realTheory.REAL_POS_NZ] 740 \\ ASM_SIMP_TAC bool_ss [realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_MUL_LID] 741 ) 742 743val le2 = Q.store_thm("le2", 744 `!n m. 2r <= n /\ 2 <= m ==> 2 <= n * m`, 745 rrw [prod_ge2] 746 ) 747 748val ge4 = Q.prove( 749 `!n. n <> 0 ==> 4n <= 2 EXP n * 2`, 750 Cases 751 \\ simp [arithmeticTheory.EXP] 752 ) 753 754val ge2d = Q.prove( 755 `!n m. 2r <= n /\ 2 <= m ==> 2 < n * m`, 756 rrw [GSYM realTheory.REAL_LT_LDIV_EQ] 757 \\ `2r / m <= 1` 758 by (match_mp_tac le1 \\ ASM_SIMP_TAC (srw_ss()++realSimps.REAL_ARITH_ss) []) 759 \\ imp_res_tac (realLib.REAL_ARITH ``a <= 1 ==> a < 2r``) 760 \\ METIS_TAC [realTheory.REAL_LTE_TRANS] 761 ) 762 763(* |- !b. 0 < w2n b <=> b <> 0w *) 764val word_lt0 = 765 wordsTheory.WORD_LO 766 |> Q.SPEC `0w` 767 |> REWRITE_RULE [wordsTheory.word_0_n2w, wordsTheory.WORD_LO_word_0] 768 |> GSYM 769 770val word_ge1 = Q.prove( 771 `!x. x <> 0w ==> 1 <= w2n x`, 772 simp [GSYM word_lt0] 773 ) 774 775val not_max_suc_lt_dimword = Q.prove( 776 `!a:'a word. a <> -1w ==> w2n a + 1 < 2 ** dimindex(:'a)`, 777 Cases 778 \\ lrw [wordsTheory.word_eq_n2w, bitTheory.MOD_2EXP_MAX_def, 779 bitTheory.MOD_2EXP_def, GSYM wordsTheory.dimword_def] 780 ) 781 782(* |- !a. a <> 0w ==> 2 <= 2 pow w2n a *) 783val pow_ge2 = 784 ge1_pow 785 |> Q.SPECL [`2`, `w2n (a:'w word)`] 786 |> SIMP_RULE (srw_ss()) [DECIDE ``1n <= n = 0 < n``, word_lt0] 787 |> GEN_ALL 788 789val mult_id = Q.prove( 790 `!a b. 1 < a ==> ((a * b = a) = (b = 1n))`, 791 Induct_on `b` 792 \\ lrw [arithmeticTheory.MULT_CLAUSES] 793 ) 794 795(* |- !x y. 1 <= y /\ 0 < x ==> x <= x * y *) 796val le_mult = 797 realTheory.REAL_LE_LDIV_EQ 798 |> Q.SPECL [`x`, `y`, `x`] 799 |> Q.DISCH `1 <= y` 800 |> SIMP_RULE bool_ss [boolTheory.AND_IMP_INTRO, realTheory.REAL_POS_NZ, 801 realTheory.REAL_DIV_REFL] 802 |> ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] 803 |> Q.GENL [`x`, `y`] 804 805(* |- !x y. x < 1 /\ 0 < y ==> y * x < y *) 806val lt_mult = 807 realTheory.REAL_LT_RDIV_EQ 808 |> Q.SPECL [`x`, `y`, `y`] 809 |> Q.DISCH `x < 1` 810 |> SIMP_RULE bool_ss [boolTheory.AND_IMP_INTRO, realTheory.REAL_POS_NZ, 811 realTheory.REAL_DIV_REFL] 812 |> ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] 813 |> Q.GENL [`x`, `y`] 814 815(* |- !x y. 1 < y /\ 0 < x ==> x < y * x *) 816val gt_mult = 817 realTheory.REAL_LT_LDIV_EQ 818 |> Q.SPECL [`x`, `y`, `x`] 819 |> Q.DISCH `1 < y` 820 |> SIMP_RULE bool_ss [boolTheory.AND_IMP_INTRO, realTheory.REAL_POS_NZ, 821 realTheory.REAL_DIV_REFL] 822 |> Q.GENL [`x`, `y`] 823 824val exp_id = Q.prove( 825 `!a b. 1 < a ==> ((a EXP b = a) = (b = 1))`, 826 REPEAT strip_tac 827 \\ Cases_on `b = 0` 828 >- lrw [arithmeticTheory.EXP] 829 \\ Cases_on `b = 1` 830 >- lrw [arithmeticTheory.EXP] 831 \\ `1 < b` by decide_tac 832 \\ imp_res_tac arithmeticTheory.LESS_ADD 833 \\ pop_assum kall_tac 834 \\ pop_assum (SUBST1_TAC o REWRITE_RULE [GSYM arithmeticTheory.ADD1] o SYM) 835 \\ lrw [arithmeticTheory.EXP, mult_id]) 836 837val sub_rat_same_base = Q.prove( 838 `!a b d. 0r < d ==> (a / d - b / d = (a - b) / d)`, 839 rrw [realTheory.REAL_EQ_RDIV_EQ, realTheory.REAL_SUB_RDISTRIB, 840 realTheory.REAL_DIV_RMUL] 841 ) 842 843(* |- !x. 0 <= x ==> (abs x = x) *) 844val gt0_abs = 845 realTheory.ABS_REFL 846 |> Q.SPEC `x` 847 |> Q.DISCH `0 <= x` 848 |> SIMP_RULE bool_ss [] 849 |> Drule.GEN_ALL 850 851(* 852(* !z x y. 0 <> z ==> ((x = y) <=> (x * z = y * z)) *) 853val mul_into = 854 realTheory.REAL_EQ_RMUL 855 |> Drule.SPEC_ALL 856 |> Q.DISCH `z <> 0` 857 |> SIMP_RULE std_ss [] 858 |> Conv.GSYM 859 |> Q.GENL [`y`, `x`, `z`] 860*) 861 862(* ------------------------------------------------------------------------ 863 Some basic theorems 864 ------------------------------------------------------------------------ *) 865 866val rsimp = ASM_SIMP_TAC (srw_ss()++realSimps.REAL_ARITH_ss) 867val rrw = SRW_TAC [boolSimps.LET_ss, realSimps.REAL_ARITH_ss] 868val rlfs = full_simp_tac (srw_ss()++realSimps.REAL_ARITH_ss) 869 870val float_component_equality = DB.theorem "float_component_equality" 871 872val sign_inconsistent = 873 Drule.GEN_ALL $ wordsLib.WORD_DECIDE ���~(x <> -1w /\ x <> 0w: word1) /\ 874 ~(x <> 1w /\ x <> 0w)��� 875 876 877val sign_neq = Q.prove( 878 `!x. ~x <> x: word1`, 879 wordsLib.Cases_word_value 880 \\ simp [] 881 ) 882 883val lem = Q.prove( 884 `(1w #>> 1 <> 0w : 'a word) /\ word_msb (1w : 'a word #>> 1)`, 885 simp_tac (srw_ss()++wordsLib.WORD_BIT_EQ_ss) [] 886 \\ conj_tac 887 >| [qexists_tac `dimindex(:'a) - 1`, all_tac] 888 \\ simp [DECIDE ``0n < n ==> (n - 1 + 1 = n)``, wordsTheory.word_index] 889 ) 890 891Theorem some_nan_components[local]: 892 !fp_op. 893 ((float_some_qnan fp_op).Exponent = UINT_MAXw) /\ 894 ((float_some_qnan fp_op).Significand <> 0w) 895Proof 896 strip_tac \\ simp [float_some_qnan_def] 897 \\ SELECT_ELIM_TAC 898 \\ conj_tac 899 >- ( 900 simp [float_is_nan_def, float_is_signalling_def] 901 \\ EXISTS_TAC 902 ``(K (<| Sign := 0w; 903 Exponent := UINT_MAXw: 'b word; 904 Significand := (1w #>> 1): 'a word |>)) : 905 ('a, 'b) fp_op -> ('a, 'b) float`` 906 \\ simp [float_value_def, lem] 907 ) 908 \\ strip_tac 909 \\ Cases_on `float_value (x fp_op)` 910 \\ simp [float_is_nan_def] 911 \\ pop_assum mp_tac 912 \\ rw [float_value_def] 913QED 914 915Theorem float_components[simp]: 916 ((float_plus_infinity (:'t # 'w)).Sign = 0w) /\ 917 ((float_plus_infinity (:'t # 'w)).Exponent = UINT_MAXw) /\ 918 ((float_plus_infinity (:'t # 'w)).Significand = 0w) /\ 919 ((float_minus_infinity (:'t # 'w)).Sign = 1w) /\ 920 ((float_minus_infinity (:'t # 'w)).Exponent = UINT_MAXw) /\ 921 ((float_minus_infinity (:'t # 'w)).Significand = 0w) /\ 922 ((float_plus_zero (:'t # 'w)).Sign = 0w) /\ 923 ((float_plus_zero (:'t # 'w)).Exponent = 0w) /\ 924 ((float_plus_zero (:'t # 'w)).Significand = 0w) /\ 925 ((float_minus_zero (:'t # 'w)).Sign = 1w) /\ 926 ((float_minus_zero (:'t # 'w)).Exponent = 0w) /\ 927 ((float_minus_zero (:'t # 'w)).Significand = 0w) /\ 928 ((float_plus_min (:'t # 'w)).Sign = 0w) /\ 929 ((float_plus_min (:'t # 'w)).Exponent = 0w) /\ 930 ((float_plus_min (:'t # 'w)).Significand = 1w) /\ 931 ((float_minus_min (:'t # 'w)).Sign = 1w) /\ 932 ((float_minus_min (:'t # 'w)).Exponent = 0w) /\ 933 ((float_minus_min (:'t # 'w)).Significand = 1w) /\ 934 ((float_top (:'t # 'w)).Sign = 0w) /\ 935 ((float_top (:'t # 'w)).Exponent = UINT_MAXw - 1w) /\ 936 ((float_top (:'t # 'w)).Significand = UINT_MAXw) /\ 937 ((float_bottom (:'t # 'w)).Sign = 1w) /\ 938 ((float_bottom (:'t # 'w)).Exponent = UINT_MAXw - 1w) /\ 939 ((float_bottom (:'t # 'w)).Significand = UINT_MAXw) /\ 940 (!fp_op. (float_some_qnan fp_op).Exponent = UINT_MAXw) /\ 941 (!fp_op. (float_some_qnan fp_op).Significand <> 0w) /\ 942 (!x. (float_negate x).Sign = ~x.Sign) /\ 943 (!x. (float_negate x).Exponent = x.Exponent) /\ 944 (!x. (float_negate x).Significand = x.Significand) 945Proof 946 rw [float_plus_infinity_def, float_minus_infinity_def, 947 float_plus_zero_def, float_minus_zero_def, float_plus_min_def, 948 float_minus_min_def, float_top_def, float_bottom_def, 949 some_nan_components, float_negate_def] 950QED 951 952Theorem float_distinct[simp]: 953 (float_plus_infinity (:'t # 'w) <> float_minus_infinity (:'t # 'w)) /\ 954 (float_plus_infinity (:'t # 'w) <> float_plus_zero (:'t # 'w)) /\ 955 (float_plus_infinity (:'t # 'w) <> float_minus_zero (:'t # 'w)) /\ 956 (float_plus_infinity (:'t # 'w) <> float_top (:'t # 'w)) /\ 957 (float_plus_infinity (:'t # 'w) <> float_bottom (:'t # 'w)) /\ 958 (float_plus_infinity (:'t # 'w) <> float_plus_min (:'t # 'w)) /\ 959 (float_plus_infinity (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 960 (!fp_op. float_plus_infinity (:'t # 'w) <> float_some_qnan fp_op) /\ 961 (float_minus_infinity (:'t # 'w) <> float_plus_zero (:'t # 'w)) /\ 962 (float_minus_infinity (:'t # 'w) <> float_minus_zero (:'t # 'w)) /\ 963 (float_minus_infinity (:'t # 'w) <> float_top (:'t # 'w)) /\ 964 (float_minus_infinity (:'t # 'w) <> float_bottom (:'t # 'w)) /\ 965 (float_minus_infinity (:'t # 'w) <> float_plus_min (:'t # 'w)) /\ 966 (float_minus_infinity (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 967 (!fp_op. float_minus_infinity (:'t # 'w) <> float_some_qnan fp_op) /\ 968 (float_plus_zero (:'t # 'w) <> float_minus_zero (:'t # 'w)) /\ 969 (float_plus_zero (:'t # 'w) <> float_top (:'t # 'w)) /\ 970 (float_plus_zero (:'t # 'w) <> float_bottom (:'t # 'w)) /\ 971 (float_plus_zero (:'t # 'w) <> float_plus_min (:'t # 'w)) /\ 972 (float_plus_zero (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 973 (!fp_op. float_plus_zero (:'t # 'w) <> float_some_qnan fp_op) /\ 974 (float_minus_zero (:'t # 'w) <> float_top (:'t # 'w)) /\ 975 (float_minus_zero (:'t # 'w) <> float_bottom (:'t # 'w)) /\ 976 (float_minus_zero (:'t # 'w) <> float_plus_min (:'t # 'w)) /\ 977 (float_minus_zero (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 978 (!fp_op. float_minus_zero (:'t # 'w) <> float_some_qnan fp_op) /\ 979 (float_top (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 980 (float_top (:'t # 'w) <> float_bottom (:'t # 'w)) /\ 981 (!fp_op. float_top (:'t # 'w) <> float_some_qnan fp_op) /\ 982 (float_bottom (:'t # 'w) <> float_plus_min (:'t # 'w)) /\ 983 (!fp_op. float_bottom (:'t # 'w) <> float_some_qnan fp_op) /\ 984 (!fp_op. float_plus_min (:'t # 'w) <> float_some_qnan fp_op) /\ 985 (float_plus_min (:'t # 'w) <> float_minus_min (:'t # 'w)) /\ 986 (!fp_op. float_minus_min (:'t # 'w) <> float_some_qnan fp_op) /\ 987 (!x. float_negate x <> x) 988Proof 989 rw [float_component_equality, float_components, two_mod_not_one, sign_neq, 990 wordsTheory.word_T_not_zero, wordsTheory.WORD_EQ_NEG] 991QED 992 993Theorem float_values[simp]: 994 (float_value (float_plus_infinity (:'t # 'w)) = Infinity) /\ 995 (float_value (float_minus_infinity (:'t # 'w)) = Infinity) /\ 996 (!fp_op. float_value (float_some_qnan fp_op) = NaN) /\ 997 (float_value (float_plus_zero (:'t # 'w)) = Float 0) /\ 998 (float_value (float_minus_zero (:'t # 'w)) = Float 0) /\ 999 (float_value (float_plus_min (:'t # 'w)) = 1000 Float (2r / (2r pow (bias (:'w) + precision (:'t))))) /\ 1001 (float_value (float_minus_min (:'t # 'w)) = 1002 Float (-2r / (2r pow (bias (:'w) + precision (:'t))))) 1003Proof 1004 rw [float_plus_infinity_def, float_minus_infinity_def, 1005 float_plus_zero_def, float_minus_zero_def, float_plus_min_def, 1006 float_minus_min_def, some_nan_components, float_negate_def, 1007 float_value_def, float_to_real_def, wordsTheory.word_T_not_zero, 1008 realTheory.mult_rat, realTheory.POW_ADD, GSYM realTheory.REAL_NEG_MINUS1, 1009 GSYM realTheory.REAL_MUL_LNEG, realTheory.neg_rat] 1010QED 1011 1012Theorem zero_to_real[simp]: 1013 (float_to_real (float_plus_zero (:'t # 'w)) = 0) /\ 1014 (float_to_real (float_minus_zero (:'t # 'w)) = 0) 1015Proof 1016 rw [float_plus_zero_def, float_minus_zero_def, 1017 float_negate_def, float_to_real_def] 1018QED 1019 1020val sign_not_zero = Q.store_thm("sign_not_zero", 1021 `!s: word1. -1 pow w2n s <> 0`, 1022 wordsLib.Cases_word_value \\ EVAL_TAC) 1023 1024val float_sets = Q.store_thm("float_sets", 1025 `(float_is_zero = {float_minus_zero (:'t # 'w); 1026 float_plus_zero (:'t # 'w)}) /\ 1027 (float_is_infinite = {float_minus_infinity (:'t # 'w); 1028 float_plus_infinity (:'t # 'w)})`, 1029 rw [FUN_EQ_THM, float_is_infinite_def, float_is_zero_def, float_value_def, 1030 float_plus_infinity_def, float_minus_infinity_def, 1031 float_plus_zero_def, float_minus_zero_def, float_to_real_def, 1032 float_negate_def, float_component_equality] 1033 \\ rw [sign_not_zero, realLib.REAL_ARITH ``0r <= n ==> 1 + n <> 0``] 1034 \\ wordsLib.Cases_on_word_value `x.Sign` 1035 \\ simp [] 1036 ) 1037 1038val tac = 1039 rw [float_is_nan_def, float_is_normal_def, float_is_subnormal_def, 1040 float_is_finite_def, float_is_infinite_def, float_is_zero_def, 1041 float_is_integral_def, is_integral_def, float_values, 1042 some_nan_components] 1043 \\ rw [float_plus_infinity_def, float_minus_infinity_def, 1044 float_plus_zero_def, float_minus_zero_def, float_top_def, 1045 float_bottom_def, float_some_qnan_def, float_plus_min_def, 1046 float_minus_min_def, float_negate_def, float_value_def, 1047 wordsTheory.WORD_EQ_NEG, realTheory.REAL_EQ_LDIV_EQ, two_mod_not_one] 1048 1049Theorem infinity_properties[simp]: 1050 ~float_is_zero (float_plus_infinity (:'t # 'w)) /\ 1051 ~float_is_zero (float_minus_infinity (:'t # 'w)) /\ 1052 ~float_is_finite (float_plus_infinity (:'t # 'w)) /\ 1053 ~float_is_finite (float_minus_infinity (:'t # 'w)) /\ 1054 ~float_is_integral (float_plus_infinity (:'t # 'w)) /\ 1055 ~float_is_integral (float_minus_infinity (:'t # 'w)) /\ 1056 ~float_is_nan (float_plus_infinity (:'t # 'w)) /\ 1057 ~float_is_nan (float_minus_infinity (:'t # 'w)) /\ 1058 ~float_is_normal (float_plus_infinity (:'t # 'w)) /\ 1059 ~float_is_normal (float_minus_infinity (:'t # 'w)) /\ 1060 ~float_is_subnormal (float_plus_infinity (:'t # 'w)) /\ 1061 ~float_is_subnormal (float_minus_infinity (:'t # 'w)) /\ 1062 float_is_infinite (float_plus_infinity (:'t # 'w)) /\ 1063 float_is_infinite (float_minus_infinity (:'t # 'w)) 1064Proof tac 1065QED 1066 1067Theorem zero_properties[simp]: 1068 float_is_zero (float_plus_zero (:'t # 'w)) /\ 1069 float_is_zero (float_minus_zero (:'t # 'w)) /\ 1070 float_is_finite (float_plus_zero (:'t # 'w)) /\ 1071 float_is_finite (float_minus_zero (:'t # 'w)) /\ 1072 float_is_integral (float_plus_zero (:'t # 'w)) /\ 1073 float_is_integral (float_minus_zero (:'t # 'w)) /\ 1074 ~float_is_nan (float_plus_zero (:'t # 'w)) /\ 1075 ~float_is_nan (float_minus_zero (:'t # 'w)) /\ 1076 ~float_is_normal (float_plus_zero (:'t # 'w)) /\ 1077 ~float_is_normal (float_minus_zero (:'t # 'w)) /\ 1078 ~float_is_subnormal (float_plus_zero (:'t # 'w)) /\ 1079 ~float_is_subnormal (float_minus_zero (:'t # 'w)) /\ 1080 ~float_is_infinite (float_plus_zero (:'t # 'w)) /\ 1081 ~float_is_infinite (float_minus_zero (:'t # 'w)) 1082Proof tac 1083QED 1084 1085val some_nan_properties = Q.store_thm("some_nan_properties", 1086 `!fp_op. 1087 ~float_is_zero (float_some_qnan fp_op) /\ 1088 ~float_is_finite (float_some_qnan fp_op) /\ 1089 ~float_is_integral (float_some_qnan fp_op) /\ 1090 float_is_nan (float_some_qnan fp_op) /\ 1091 ~float_is_signalling (float_some_qnan fp_op) /\ 1092 ~float_is_normal (float_some_qnan fp_op) /\ 1093 ~float_is_subnormal (float_some_qnan fp_op) /\ 1094 ~float_is_infinite (float_some_qnan fp_op)`, 1095 tac 1096 \\ SELECT_ELIM_TAC 1097 \\ simp [] 1098 \\ qexists_tac 1099 `(K (<| Sign := 0w; 1100 Exponent := UINT_MAXw: 'b word; 1101 Significand := (1w #>> 1): 'a word |>))` 1102 \\ simp [float_is_signalling_def] 1103 \\ tac 1104 \\ fs [lem] 1105 ) 1106 1107Theorem min_properties[simp]: 1108 ~float_is_zero (float_plus_min (:'t # 'w)) /\ 1109 float_is_finite (float_plus_min (:'t # 'w)) /\ 1110 (float_is_integral (float_plus_min (:'t # 'w)) = 1111 (precision(:'w) = 1) /\ (precision(:'t) = 1)) /\ 1112 ~float_is_nan (float_plus_min (:'t # 'w)) /\ 1113 ~float_is_normal (float_plus_min (:'t # 'w)) /\ 1114 float_is_subnormal (float_plus_min (:'t # 'w)) /\ 1115 ~float_is_infinite (float_plus_min (:'t # 'w)) /\ 1116 ~float_is_zero (float_minus_min (:'t # 'w)) /\ 1117 float_is_finite (float_minus_min (:'t # 'w)) /\ 1118 (float_is_integral (float_minus_min (:'t # 'w)) = 1119 (precision(:'w) = 1) /\ (precision(:'t) = 1)) /\ 1120 ~float_is_nan (float_minus_min (:'t # 'w)) /\ 1121 ~float_is_normal (float_minus_min (:'t # 'w)) /\ 1122 float_is_subnormal (float_minus_min (:'t # 'w)) /\ 1123 ~float_is_infinite (float_minus_min (:'t # 'w)) 1124Proof 1125 tac (* after this the float_is_integral cases remain *) 1126 \\ (simp [realTheory.REAL_EQ_LDIV_EQ, realTheory.ABS_DIV, 1127 wordsTheory.INT_MAX_def, wordsTheory.INT_MIN_def, gt0_abs] 1128 \\ Cases_on `precision (:'t) = 1` 1129 \\ Cases_on `precision (:'w) = 1` 1130 \\ imp_res_tac ge2 1131 \\ srw_tac[][] 1132 >- (qexists_tac `1n` \\ decide_tac) 1133 \\ Cases_on `n` 1134 \\ simp [] 1135 \\ rewrite_tac [realTheory.REAL, realTheory.REAL_RDISTRIB] 1136 \\ match_mp_tac 1137 (realLib.REAL_ARITH ``2r < n /\ 0 <= x ==> 2 <> x + 1 * n``) 1138 \\ simp [realTheory.REAL_LT_IMP_LE, realTheory.REAL_LE_MUL] 1139 \\ imp_res_tac ge2b 1140 \\ match_mp_tac gt1_pow 1141 \\ simp []) 1142QED 1143 1144val lem1 = Q.prove( 1145 `0w <+ (-2w:'a word) = (dimindex(:'a) <> 1)`, 1146 once_rewrite_tac [wordsTheory.WORD_LESS_NEG_RIGHT] 1147 \\ simp [two_mod_eq_zero, wordsTheory.dimword_def, exp_id, 1148 DECIDE ``0 < n ==> n <> 0n``] 1149 ) 1150 1151val lem2 = Q.prove( 1152 `dimindex(:'a) <> 1 ==> -2w <+ (-1w:'a word)`, 1153 once_rewrite_tac [wordsTheory.WORD_LESS_NEG_RIGHT] 1154 \\ simp [two_mod_eq_zero, wordsTheory.dimword_def, exp_id, 1155 DECIDE ``0 < n ==> n <> 0n``, wordsTheory.word_lo_n2w] 1156 \\ strip_tac 1157 \\ `1 < dimindex(:'a)` by simp [DECIDE ``0 < n /\ n <> 1 ==> 1n < n``] 1158 \\ imp_res_tac 1159 (bitTheory.TWOEXP_MONO 1160 |> Q.SPECL [`1`, `dimindex(:'a)`] 1161 |> numLib.REDUCE_RULE) 1162 \\ lrw [] 1163 ) 1164 1165val tac = 1166 tac 1167 \\ srw_tac[] [float_to_real_def, two_mod_eq_zero, wordsTheory.dimword_def, 1168 realLib.REAL_ARITH ``0r <= n ==> 1 + n <> 0``, exp_id, lem1, 1169 DECIDE ``0 < n ==> n <> 0n``] 1170 \\ Cases_on `dimindex(:'w) = 1` 1171 \\ lrw [lem2] 1172 1173Theorem top_properties[simp]: 1174 ~float_is_zero (float_top (:'t # 'w)) /\ 1175 float_is_finite (float_top (:'t # 'w)) /\ 1176 (* float_is_integral (float_top (:'t # 'w)) = ?? /\ *) 1177 ~float_is_nan (float_top (:'t # 'w)) /\ 1178 (float_is_normal (float_top (:'t # 'w)) = (precision(:'w) <> 1)) /\ 1179 (float_is_subnormal (float_top (:'t # 'w)) = (precision(:'w) = 1)) /\ 1180 ~float_is_infinite (float_top (:'t # 'w)) 1181Proof tac 1182QED 1183 1184Theorem bottom_properties[simp]: 1185 ~float_is_zero (float_bottom (:'t # 'w)) /\ 1186 float_is_finite (float_bottom (:'t # 'w)) /\ 1187 (* float_is_integral (float_bottom (:'t # 'w)) = ?? /\ *) 1188 ~float_is_nan (float_bottom (:'t # 'w)) /\ 1189 (float_is_normal (float_bottom (:'t # 'w)) = (precision(:'w) <> 1)) /\ 1190 (float_is_subnormal (float_bottom (:'t # 'w)) = (precision(:'w) = 1)) /\ 1191 ~float_is_infinite (float_bottom (:'t # 'w)) 1192Proof tac 1193QED 1194 1195val float_is_zero = Q.store_thm("float_is_zero", 1196 `!x. float_is_zero x = (x.Exponent = 0w) /\ (x.Significand = 0w)`, 1197 rw [float_is_zero_def, float_value_def, float_to_real_def, sign_not_zero, 1198 realLib.REAL_ARITH ``0 <= x ==> 1 + x <> 0r``, 1199 realTheory.REAL_LE_DIV, realTheory.REAL_LT_IMP_LE]) 1200 1201val float_is_finite = Q.store_thm("float_is_finite", 1202 `!x. float_is_finite x = 1203 float_is_normal x \/ float_is_subnormal x \/ float_is_zero x`, 1204 rw [float_is_finite_def, float_is_normal_def, float_is_subnormal_def, 1205 float_is_zero, float_value_def] 1206 \\ Cases_on `x.Exponent = 0w` 1207 \\ Cases_on `x.Significand = 0w` 1208 \\ fs [] 1209 ) 1210 1211val float_cases_finite = Q.store_thm("float_cases_finite", 1212 `!x. float_is_nan x \/ float_is_infinite x \/ float_is_finite x`, 1213 rw [float_is_nan_def, float_is_infinite_def, float_is_finite_def] 1214 \\ Cases_on `float_value x` 1215 \\ fs [] 1216 ) 1217 1218val float_distinct_finite = Q.store_thm("float_distinct_finite", 1219 `!x. ~(float_is_nan x /\ float_is_infinite x) /\ 1220 ~(float_is_nan x /\ float_is_finite x) /\ 1221 ~(float_is_infinite x /\ float_is_finite x)`, 1222 rw [float_is_nan_def, float_is_infinite_def, float_is_finite_def] 1223 \\ Cases_on `float_value x` 1224 \\ fs [] 1225 ) 1226 1227val float_cases = Q.store_thm("float_cases", 1228 `!x. float_is_nan x \/ float_is_infinite x \/ float_is_normal x \/ 1229 float_is_subnormal x \/ float_is_zero x`, 1230 metis_tac [float_cases_finite, float_is_finite] 1231 ) 1232 1233val float_is_distinct = Q.store_thm("float_is_distinct", 1234 `!x. ~(float_is_nan x /\ float_is_infinite x) /\ 1235 ~(float_is_nan x /\ float_is_normal x) /\ 1236 ~(float_is_nan x /\ float_is_subnormal x) /\ 1237 ~(float_is_nan x /\ float_is_zero x) /\ 1238 ~(float_is_infinite x /\ float_is_normal x) /\ 1239 ~(float_is_infinite x /\ float_is_subnormal x) /\ 1240 ~(float_is_infinite x /\ float_is_zero x) /\ 1241 ~(float_is_normal x /\ float_is_subnormal x) /\ 1242 ~(float_is_normal x /\ float_is_zero x) /\ 1243 ~(float_is_subnormal x /\ float_is_zero x)`, 1244 rw [] 1245 \\ TRY (metis_tac [float_is_finite, float_distinct_finite]) 1246 \\ fs [float_is_normal_def, float_is_subnormal_def, float_is_zero] 1247 \\ Cases_on `x.Exponent = 0w` 1248 \\ Cases_on `x.Exponent = -1w` 1249 \\ Cases_on `x.Significand = 0w` 1250 \\ fs [] 1251 ) 1252 1253val float_infinities = Q.store_thm("float_infinities", 1254 `!x. float_is_infinite x = 1255 (x = float_plus_infinity (:'t # 'w)) \/ 1256 (x = float_minus_infinity (:'t # 'w))`, 1257 strip_tac 1258 \\ Q.ISPEC_THEN `x : ('t, 'w) float` strip_assume_tac float_cases_finite 1259 \\ TRY (metis_tac [float_distinct_finite, infinity_properties]) 1260 \\ Cases_on `float_value x` 1261 \\ Cases_on `x.Exponent = -1w` 1262 \\ Cases_on `x.Significand = 0w` 1263 \\ fs [float_is_infinite_def, float_value_def, 1264 float_plus_infinity_def, float_minus_infinity_def, 1265 float_negate_def, float_component_equality] 1266 \\ wordsLib.Cases_on_word_value `x.Sign` 1267 \\ simp [] 1268 ) 1269 1270val float_infinities_distinct = Q.store_thm("float_infinities_distinct", 1271 `!x. ~((x = float_plus_infinity (:'t # 'w)) /\ 1272 (x = float_minus_infinity (:'t # 'w)))`, 1273 simp [float_plus_infinity_def, float_minus_infinity_def, 1274 float_negate_def, float_component_equality] 1275 ) 1276(* ------------------------------------------------------------------------ *) 1277 1278val float_to_real_negate = Q.store_thm("float_to_real_negate", 1279 `!x. float_to_real (float_negate x) = -float_to_real x`, 1280 rw [float_to_real_def, float_negate_def] 1281 \\ wordsLib.Cases_on_word_value `x.Sign` 1282 \\ rsimp [] 1283 ) 1284 1285Theorem float_negate_negate[simp]: 1286 !x. float_negate (float_negate x) = x 1287Proof 1288 simp [float_negate_def, float_component_equality] 1289QED 1290 1291(* ------------------------------------------------------------------------ 1292 Lemma support for rounding theorems 1293 ------------------------------------------------------------------------ *) 1294 1295(* 1296val () = List.app Parse.clear_overloads_on ["bias", "precision"] 1297*) 1298 1299local 1300 val cnv = 1301 Conv.QCONV 1302 (REWRITE_CONV [realTheory.REAL_LDISTRIB, realTheory.REAL_RDISTRIB]) 1303 val dec = 1304 METIS_PROVE 1305 [realTheory.REAL_DIV_RMUL, realTheory.REAL_MUL_COMM, 1306 realTheory.REAL_MUL_ASSOC, zero_neq_twopow, 1307 realTheory.mult_ratr 1308 |> Q.INST [`z` |-> `2 pow n`] 1309 |> REWRITE_RULE [zero_neq_twopow] 1310 |> GEN_ALL] 1311in 1312 fun CANCEL_PROVE tm = 1313 let 1314 val thm1 = cnv tm 1315 val tm1 = boolSyntax.rhs (Thm.concl thm1) 1316 val thm2 = Drule.EQT_INTRO (dec tm1) 1317 in 1318 Drule.EQT_ELIM (Thm.TRANS thm1 thm2) 1319 end 1320end 1321 1322val cancel_rwts = Q.prove( 1323 `(!a b. (2 pow a * b) / 2 pow a = b) /\ 1324 (!a b c. 2 pow a * (b / 2 pow a * c) = b * c) /\ 1325 (!a b c. a * (b / 2 pow c) * 2 pow c = a * b) /\ 1326 (!a b c. a * (2 pow b * c) / 2 pow b = a * c) /\ 1327 (!a b c. a / 2 pow b * (2 pow b * c) = a * c) /\ 1328 (!a b c. a / 2 pow b * c * 2 pow b = a * c) /\ 1329 (!a b c d. a / 2 pow b * c * (2 pow b * d) = a * c * d) /\ 1330 (!a b c d. a * (2 pow b * c) * d / 2 pow b = a * c * d)`, 1331 metis_tac 1332 [realTheory.REAL_DIV_RMUL, realTheory.REAL_MUL_COMM, 1333 realTheory.REAL_MUL_ASSOC, zero_neq_twopow, 1334 realTheory.mult_ratr 1335 |> Q.INST [`z` |-> `2 pow n`] 1336 |> REWRITE_RULE [zero_neq_twopow] 1337 |> GEN_ALL] 1338 ) 1339 1340val cancel_rwt = 1341 CANCEL_PROVE 1342 ``(!a b c d. a * (b + c / 2 pow d) * 2 pow d = a * b * 2 pow d + a * c)`` 1343 1344val ulp = Q.store_thm("ulp", 1345 `ulp (:'t # 'w) = float_to_real (float_plus_min (:'t # 'w))`, 1346 simp [ulp_def, ULP_def, float_to_real_def, float_plus_min_def, 1347 realTheory.mult_rat, GSYM realTheory.POW_ADD] 1348 ) 1349 1350val neg_ulp = Q.store_thm("neg_ulp", 1351 `-ulp (:'t # 'w) = 1352 float_to_real (float_negate (float_plus_min (:'t # 'w)))`, 1353 simp [float_to_real_negate, ulp] 1354 ) 1355 1356val ULP_gt0 = Q.prove( 1357 `!e. 0 < ULP (e:'w word, (:'t))`, 1358 rw [ULP_def, realTheory.REAL_LT_RDIV_0]) 1359 1360val ulp_gt0 = (REWRITE_RULE [GSYM ulp_def] o Q.SPEC `0w`) ULP_gt0 1361 1362val ULP_le_mono = Q.store_thm("ULP_le_mono", 1363 `!e1 e2. e2 <> 0w ==> (ULP (e1, (:'t)) <= ULP (e2, (:'t)) = e1 <=+ e2)`, 1364 Cases 1365 \\ Cases 1366 \\ lrw [ULP_def, wordsTheory.word_ls_n2w, div_le] 1367 \\ simp [realTheory.REAL_OF_NUM_POW] 1368 ) 1369 1370val ulp_lt_ULP = Q.store_thm("ulp_lt_ULP", 1371 `!e: 'w word. ulp (:'t # 'w) <= ULP (e,(:'t))`, 1372 rw [ulp_def] 1373 \\ Cases_on `e = 0w` 1374 \\ simp [ULP_le_mono] 1375 ) 1376 1377val lem = Q.prove( 1378 `!n. 0 < n ==> 3 < 2 pow SUC n`, 1379 Induct 1380 \\ rw [Once realTheory.pow] 1381 \\ Cases_on `0 < n` 1382 \\ simp [DECIDE ``~(0n < n) ==> (n = 0)``, 1383 realLib.REAL_ARITH ``3r < n ==> 3 < 2 * n``] 1384 ) 1385 1386val ulp_lt_largest = Q.store_thm("ulp_lt_largest", 1387 `ulp (:'t # 'w) < largest (:'t # 'w)`, 1388 simp [ulp_def, ULP_def, largest_def, realTheory.REAL_LT_RMUL_0, cancel_rwts, 1389 realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD] 1390 \\ simp [realTheory.REAL_SUB_RDISTRIB, realTheory.REAL_SUB_LDISTRIB, 1391 realTheory.REAL_MUL_LINV, GSYM realaxTheory.REAL_MUL_ASSOC, 1392 GSYM (CONJUNCT2 realTheory.pow)] 1393 \\ simp [realLib.REAL_ARITH ``(a * b) - a = a * (b - 1): real``] 1394 \\ match_mp_tac ge2c 1395 \\ rw [GSYM realTheory.REAL_LT_ADD_SUB, realTheory.POW_2_LE1, lem] 1396 ) 1397 1398val ulp_lt_threshold = Q.store_thm("ulp_lt_threshold", 1399 `ulp (:'t # 'w) < threshold (:'t # 'w)`, 1400 simp [ulp_def, ULP_def, threshold_def, realTheory.REAL_LT_RMUL_0, 1401 cancel_rwts, realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD, 1402 realTheory.pow] 1403 \\ simp [realTheory.REAL_SUB_RDISTRIB, realTheory.REAL_SUB_LDISTRIB, 1404 realTheory.REAL_MUL_LINV, realTheory.REAL_INV_MUL, 1405 GSYM realaxTheory.REAL_MUL_ASSOC] 1406 \\ simp [realLib.REAL_ARITH ``(a * b) - a * c = a * (b - c): real``] 1407 \\ match_mp_tac ge2c 1408 \\ rw [realTheory.POW_2_LE1, GSYM realTheory.REAL_LT_ADD_SUB, 1409 realTheory.REAL_INV_1OVER, GSYM (CONJUNCT2 realTheory.pow), 1410 realTheory.REAL_LT_LDIV_EQ, lem, 1411 realLib.REAL_ARITH ``3r < n ==> 5 < n * 2``] 1412 ) 1413 1414val lt_ulp_not_infinity0 = 1415 MATCH_MP 1416 (realLib.REAL_ARITH ``u < l ==> abs x < u ==> ~(x < -l) /\ ~(x > l)``) 1417 ulp_lt_largest 1418 |> Drule.GEN_ALL 1419 1420val lt_ulp_not_infinity1 = 1421 MATCH_MP 1422 (realLib.REAL_ARITH 1423 ``u < l ==> 2 * abs x <= u ==> ~(x <= -l) /\ ~(x >= l)``) 1424 ulp_lt_threshold 1425 |> Drule.GEN_ALL 1426 1427val abs_float_value = Q.store_thm("abs_float_value", 1428 `(!b: word1 c d. abs (-1 pow w2n b * c * d) = abs (c * d)) /\ 1429 (!b: word1 c. abs (-1 pow w2n b * c) = abs c)`, 1430 conj_tac 1431 \\ wordsLib.Cases_word_value 1432 \\ simp [realTheory.ABS_MUL]) 1433 1434(* |- !x n. abs (1 + &n / 2 pow x) = 1 + &n / 2 pow x *) 1435val abs_significand = 1436 realLib.REAL_ARITH ``!a b. 0 <= a /\ 0 <= b ==> (abs (a + b) = a + b)`` 1437 |> Q.SPECL [`1`, `&n / 2 pow x`] 1438 |> Conv.CONV_RULE 1439 (Conv.RATOR_CONV (SIMP_CONV (srw_ss()++realSimps.REAL_ARITH_ss) 1440 [realTheory.REAL_LE_DIV, realTheory.REAL_POS, 1441 realTheory.REAL_LT_IMP_LE])) 1442 |> REWRITE_RULE [] 1443 |> GEN_ALL 1444 1445val less_than_ulp = Q.store_thm("less_than_ulp", 1446 `!a: ('t, 'w) float. 1447 abs (float_to_real a) < ulp (:'t # 'w) = 1448 (a.Exponent = 0w) /\ (a.Significand = 0w)`, 1449 strip_tac 1450 \\ eq_tac 1451 \\ rw [ulp_def, ULP_def, float_to_real_def, abs_float_value, abs_significand, 1452 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, 1453 gt0_abs, realTheory.mult_rat, realTheory.REAL_LT_RDIV_0] 1454 >| [ 1455 SPOSE_NOT_THEN strip_assume_tac 1456 \\ qpat_x_assum `x < y: real` mp_tac 1457 \\ simp [realTheory.REAL_NOT_LT, GSYM realTheory.POW_ADD, 1458 realTheory.REAL_LE_RDIV_EQ, realTheory.REAL_DIV_RMUL] 1459 \\ Cases_on `a.Significand` 1460 \\ lfs [], 1461 (* -- *) 1462 simp [realTheory.REAL_NOT_LT, realTheory.REAL_LDISTRIB, 1463 realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_RDISTRIB, 1464 realTheory.POW_ADD, cancel_rwts] 1465 \\ simp [GSYM realaxTheory.REAL_LDISTRIB] 1466 \\ match_mp_tac le2 1467 \\ conj_tac 1468 >- (match_mp_tac ge1_pow 1469 \\ Cases_on `a.Exponent` 1470 \\ lfs []) 1471 \\ match_mp_tac 1472 (realLib.REAL_ARITH ``2r <= a /\ 0 <= x ==> 2 <= a + x``) 1473 \\ simp [ge1_pow, DECIDE ``0n < a ==> 1 <= a``] 1474 ]) 1475 1476(* ------------------------------------------------------------------------ *) 1477 1478val Float_is_finite = Q.prove( 1479 `!y: ('t, 'w) float r. 1480 (float_value y = Float r) ==> float_is_finite y`, 1481 rw [float_is_finite_def]) 1482 1483val Float_float_to_real = Q.prove( 1484 `!y: ('t, 'w) float r. 1485 (float_value y = Float r) ==> (float_to_real y = r)`, 1486 rw [float_value_def]) 1487 1488val float_is_zero_to_real = Q.store_thm("float_is_zero_to_real", 1489 `!x. float_is_zero x = (float_to_real x = 0)`, 1490 rw [float_is_zero_def, float_value_def] 1491 \\ simp [float_to_real_def] 1492 \\ wordsLib.Cases_on_word_value `x.Sign` 1493 \\ rsimp [realLib.REAL_ARITH ``0r <= x ==> 1 + x <> 0``] 1494 ) 1495 1496(* !x. float_is_zero x ==> (float_to_real x = 0) *) 1497val float_is_zero_to_real_imp = 1498 float_is_zero_to_real 1499 |> Drule.SPEC_ALL 1500 |> Thm.EQ_IMP_RULE 1501 |> fst 1502 |> Drule.GEN_ALL 1503 1504val pos_subnormal = Q.prove( 1505 `!a b n. 0 <= 2 / 2 pow a * (&n / 2 pow b)`, 1506 rrw [realTheory.REAL_LE_MUL] 1507 ) 1508 1509val pos_normal = Q.prove( 1510 `!a b c n. 0 <= 2 pow a / 2 pow b * (1 + &n / 2 pow c)`, 1511 rw [realTheory.REAL_LE_DIV, realTheory.REAL_LE_MUL, 1512 realLib.REAL_ARITH ``0r <= n ==> 0 <= 1 + n``] 1513 ) 1514 1515val pos_normal2 = Q.prove( 1516 `!a b c n. 0 <= 2 pow a / 2 pow b * (&n / 2 pow c)`, 1517 rw [realTheory.REAL_LE_DIV, realTheory.REAL_LE_MUL, 1518 realLib.REAL_ARITH ``0r <= n ==> 0 <= 1 + n``] 1519 ) 1520 1521val thms = 1522 List.map realLib.REAL_ARITH 1523 [``a <= b /\ 0 <= c ==> a <= b + c: real``, 1524 ``0 <= b /\ a <= c ==> a <= b + c: real``, 1525 ``0 <= b /\ a <= c /\ 0 <= d ==> a <= b + (c + d): real``, 1526 ``a <= b /\ 0 <= c /\ 0 <= d ==> a <= b + c + d: real``, 1527 ``a <= b /\ 0 <= c /\ 0 <= d /\ 0 <= e ==> a <= b + c + (d + e): real``] 1528 1529val diff_sign_ULP = Q.prove( 1530 `!x: ('t, 'w) float y: ('t, 'w) float. 1531 ~(float_is_zero x /\ float_is_zero y) /\ x.Sign <> y.Sign ==> 1532 ULP (x.Exponent,(:'t)) <= abs (float_to_real x - float_to_real y)`, 1533 NTAC 2 strip_tac 1534 \\ wordsLib.Cases_on_word_value `x.Sign` 1535 \\ wordsLib.Cases_on_word_value `y.Sign` 1536 \\ rw [ULP_def, float_to_real_def, float_is_zero, realTheory.ABS_NEG, 1537 pos_normal, pos_subnormal, 1538 realLib.REAL_ARITH ``a - -1r * b * c = a + b * c``, 1539 realLib.REAL_ARITH ``-1r * b * c - a = -(b * c + a)``, 1540 realLib.REAL_ARITH ``0 <= a /\ 0 <= b ==> (abs (a + b) = a + b)``] 1541 \\ rw [realTheory.REAL_LDISTRIB] 1542 >| (List.map match_mp_tac (thms @ thms)) 1543 \\ rrw [pos_subnormal, pos_normal2, word_lt0, realTheory.POW_ADD, 1544 realTheory.REAL_LE_LDIV_EQ, le2, pow_ge2, ge1_pow, le_mult, 1545 fcpTheory.DIMINDEX_GE_1, realTheory.REAL_LE_DIV, realTheory.POW_2_LE1, 1546 cancel_rwts, DECIDE ``n <> 0n ==> 1 <= 2 * n``, 1547 realLib.REAL_ARITH ``2 <= a ==> 1r <= a``] 1548 ) 1549 1550Theorem diff_sign_ULP_gt[local]: 1551 !x: ('t, 'w) float y: ('t, 'w) float. 1552 ~float_is_zero x /\ ~float_is_zero y /\ x.Sign <> y.Sign ==> 1553 ULP (x.Exponent,(:'t)) < abs (float_to_real x - float_to_real y) 1554Proof 1555 NTAC 2 strip_tac 1556 \\ wordsLib.Cases_on_word_value `x.Sign` 1557 \\ wordsLib.Cases_on_word_value `y.Sign` 1558 \\ rw [ULP_def, float_to_real_def, float_is_zero, realTheory.ABS_NEG, 1559 pos_normal, pos_subnormal, 1560 realLib.REAL_ARITH ``a - -1r * b * c = a + b * c``, 1561 realLib.REAL_ARITH ``-1r * b * c - a = -(b * c + a)``, 1562 realLib.REAL_ARITH ``0 <= a /\ 0 <= b ==> (abs (a + b) = a + b)``] 1563 \\ rrw [realTheory.REAL_LDISTRIB, realTheory.REAL_RDISTRIB, 1564 realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_LE_MUL, 1565 realTheory.POW_2_LE1, realTheory.POW_ADD, 1566 pos_subnormal, pos_normal2, word_lt0, cancel_rwts, word_lt0, 1567 prod_ge2, pow_ge2, le_mult, 1568 DECIDE ``0n < a /\ 0 < b ==> 2 < 2 * a + 2 * b``, 1569 DECIDE ``1n <= n = 0 < n``, 1570 DECIDE ``0n < x ==> 0 < 2 * x``, 1571 realLib.REAL_ARITH ``a <= b /\ 0r <= c /\ 1 <= d ==> a < b + c + d``, 1572 realLib.REAL_ARITH 1573 ``a <= b /\ 0r <= c /\ 2 <= d /\ 0 <= e ==> a < b + c + (d + e)``, 1574 realLib.REAL_ARITH 1575 ``1 <= a /\ 2r <= b /\ 0 <= c ==> 2 < 2 * a + (b + c)`` 1576 |> Q.INST [`a` |-> `&n`] 1577 |> SIMP_RULE (srw_ss()) [] 1578 ] 1579QED 1580 1581(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 1582 1583(* |- !w. w2n w < 2 ** precision (:'a) *) 1584val w2n_lt_pow = REWRITE_RULE [wordsTheory.dimword_def] wordsTheory.w2n_lt 1585 1586Theorem w2n_lt_pow_sub1[local]: 1587 !x:'a word. x <> -1w ==> w2n x < 2 ** dimindex(:'a) - 1 1588Proof 1589 REPEAT strip_tac 1590 \\ match_mp_tac (DECIDE ``a < b /\ a <> b - 1 ==> a < b - 1n``) 1591 \\ simp [w2n_lt_pow] 1592 \\ Cases_on `x` 1593 \\ fs [wordsTheory.WORD_NEG_1, wordsTheory.word_T_def, wordsTheory.w2n_n2w, 1594 wordsTheory.UINT_MAX_def, wordsTheory.dimword_def] 1595QED 1596 1597Theorem nobias_denormal_lt_1[local]: 1598 !w:'t word. &w2n w / 2 pow precision (:'t) < 1 1599Proof 1600 rw [realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_OF_NUM_POW, w2n_lt_pow] 1601QED 1602 1603Theorem nobias_denormal_lt_2[local]: 1604 !w:'t word. 2 * (&w2n w / 2 pow precision (:'t)) < 2 1605Proof 1606 rw [realLib.REAL_ARITH ``2r * n < 2 = n < 1``, nobias_denormal_lt_1] 1607QED 1608 1609Theorem subnormal_lt_normal[local]: 1610 !x y z. 1611 y <> 0w ==> 1612 2 / 2 pow bias (:'w) * (&w2n (x:'t word) / 2 pow precision (:'t)) < 1613 2 pow w2n (y:'w word) / 2 pow bias (:'w) * 1614 (1 + &w2n (z:'t word) / 2 pow precision (:'t)) 1615Proof 1616 REPEAT strip_tac 1617 \\ once_rewrite_tac 1618 [realTheory.REAL_LT_LMUL 1619 |> Q.SPEC `2 pow bias (:'w)` 1620 |> REWRITE_RULE [zero_lt_twopow] 1621 |> GSYM] 1622 \\ rewrite_tac [cancel_rwts, realTheory.REAL_LDISTRIB] 1623 \\ match_mp_tac 1624 (realLib.REAL_ARITH ``a < 2r /\ 2 <= b /\ 0 <= c ==> a < b + c``) 1625 \\ rw [nobias_denormal_lt_2, pow_ge2, realTheory.REAL_LE_MUL] 1626QED 1627 1628fun tac thm = 1629 REPEAT strip_tac 1630 \\ match_mp_tac (Q.SPECL [`a`, `b - c`, `x * b - c`] thm) 1631 \\ rsimp [realTheory.REAL_LE_SUB_CANCEL2, GSYM realTheory.REAL_LE_LDIV_EQ, 1632 realTheory.REAL_DIV_REFL, realTheory.REAL_SUB_ADD] 1633 1634val weaken_leq = Q.prove( 1635 `!x a b c. 1r <= x /\ a <= b - c /\ 0 < b ==> a <= x * b - c`, 1636 tac realTheory.REAL_LE_TRANS 1637 ) 1638 1639val weaken_lt = Q.prove( 1640 `!x a b c. 1r <= x /\ a < b - c /\ 0 < b ==> a < x * b - c`, 1641 tac realTheory.REAL_LTE_TRANS 1642 ) 1643 1644val abs_diff1 = Q.prove( 1645 `!s:word1 a b. 1646 a < b ==> (abs (-1 pow w2n s * a - -1 pow w2n s * b) = (b - a))`, 1647 wordsLib.Cases_word_value \\ rrw []) 1648 1649val abs_diff2 = Q.prove( 1650 `!s:word1 a b. 1651 b < a ==> (abs (-1 pow w2n s * a - -1 pow w2n s * b) = (a - b))`, 1652 wordsLib.Cases_word_value \\ rrw []) 1653 1654Theorem abs_diff1a[local] = 1655 abs_diff1 1656 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1657 `(2 / 2 pow bias (:'w)) * 1658 (&w2n (x:('t,'w) float).Significand / 2 pow precision (:'t))`, 1659 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1660 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1661 1662Theorem abs_diff1b[local] = 1663 abs_diff1 1664 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1665 `(2 pow w2n (x:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1666 (1 + &w2n x.Significand / 2 pow precision (:'t))`, 1667 `(2 pow (p + (w2n (x:('t,'w) float).Exponent + 1)) / 1668 2 pow bias (:'w)) * 1669 (1 + &w2n (y:('t,'w) float).Significand / 1670 2 pow precision (:'t))`] 1671 1672Theorem abs_diff1c[local] = 1673 abs_diff1 1674 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1675 `(2 / 2 pow bias (:'w)) * 1676 (&w2n (x:('t,'w) float).Significand / 2 pow precision (:'t))`, 1677 `(2 / 2 pow bias (:'w)) * 1678 (&w2n (y:('t,'w) float).Significand / 2 pow precision (:'t))`] 1679 1680Theorem abs_diff1d[local] = 1681 abs_diff1 1682 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1683 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1684 (1 + &w2n (x:('t,'w) float).Significand / 1685 2 pow precision (:'t))`, 1686 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1687 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1688 1689Theorem abs_diff1e[local] = 1690 abs_diff1 1691 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1692 `(2 / 2 pow bias (:'w))`, 1693 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1694 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1695 1696Theorem abs_diff1f[local] = 1697 abs_diff1 1698 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1699 `(2 pow w2n (x:('t,'w) float).Exponent / 2 pow bias (:'w))`, 1700 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1701 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1702 1703val abs_diff2a = 1704 abs_diff2 1705 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1706 `(2 pow w2n (x:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1707 (1 + &w2n x.Significand / 2 pow precision (:'t))`, 1708 `(2 / 2 pow bias (:'w)) * 1709 (&w2n (y:('t,'w) float).Significand / 2 pow precision (:'t))`] 1710 1711val abs_diff2b = 1712 abs_diff2 1713 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1714 `(2 pow (p + (w2n (y:('t,'w) float).Exponent + 1)) / 1715 2 pow bias (:'w)) * 1716 (1 + &w2n (x:('t,'w) float).Significand / 1717 2 pow precision (:'t))`, 1718 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1719 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1720 1721val abs_diff2c = 1722 abs_diff2 1723 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1724 `(2 / 2 pow bias (:'w)) * 1725 (&w2n (x:('t,'w) float).Significand / 2 pow precision (:'t))`, 1726 `(2 / 2 pow bias (:'w)) * 1727 (&w2n (y:('t,'w) float).Significand / 2 pow precision (:'t))`] 1728 1729val abs_diff2d = 1730 abs_diff2 1731 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1732 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1733 (1 + &w2n (x:('t,'w) float).Significand / 1734 2 pow precision (:'t))`, 1735 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1736 (1 + &w2n y.Significand / 2 pow precision (:'t))`] 1737 1738val abs_diff2e = 1739 abs_diff2 1740 |> Q.SPECL [`(y:('t,'w) float).Sign`, 1741 `(2 pow (w2n (y:('t,'w) float).Exponent + 1) / 1742 2 pow bias (:'w))`, 1743 `(2 pow w2n (y:('t,'w) float).Exponent / 2 pow bias (:'w)) * 1744 (1 + &w2n (-1w: 't word) / 2 pow precision (:'t))`] 1745 1746fun abs_diff_tac thm = 1747 SUBGOAL_THEN 1748 (boolSyntax.rand (Thm.concl thm)) 1749 (fn th => rewrite_tac [REWRITE_RULE [realTheory.REAL_MUL_ASSOC] th]) 1750 1751Theorem diff_exponent_boundary[local]: 1752 !x: ('t, 'w) float y: ('t, 'w) float. 1753 exponent_boundary y x ==> 1754 (abs (float_to_real x - float_to_real y) = ULP (y.Exponent, (:'t))) 1755Proof 1756 rw [ULP_def, exponent_boundary_def, float_to_real_def] 1757 >- (Cases_on `x.Exponent` \\ fs []) 1758 \\ abs_diff_tac abs_diff2e 1759 >- (match_mp_tac abs_diff2e 1760 \\ simp [realTheory.REAL_LT_RDIV_EQ, realTheory.REAL_LT_LMUL, 1761 realLib.REAL_ARITH ``2 * a = a * 2r``, 1762 realLib.REAL_ARITH ``1 + n < 2 = n < 1r``, cancel_rwts, 1763 REWRITE_RULE [arithmeticTheory.ADD1] realTheory.pow] 1764 \\ simp [realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_OF_NUM_POW, 1765 w2n_lt_pow] 1766 ) 1767 \\ simp [realTheory.REAL_EQ_RDIV_EQ, realTheory.POW_ADD, 1768 realTheory.REAL_SUB_RDISTRIB, cancel_rwts] 1769 \\ simp [realLib.REAL_ARITH 1770 ``(a * b * c - a * d * e) = a * (b * c - d * e: real)``, 1771 (GSYM o ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM]) 1772 realTheory.REAL_EQ_RDIV_EQ, 1773 realTheory.REAL_DIV_REFL] 1774 \\ simp [realTheory.REAL_DIV_RMUL, realTheory.REAL_EQ_SUB_RADD, 1775 realTheory.REAL_ADD_RDISTRIB, wordsTheory.w2n_minus1, 1776 wordsTheory.dimword_def] 1777 \\ rsimp [realTheory.REAL_OF_NUM_POW, 1778 DECIDE ``0 < n ==> (1 + (n + (n - 1)) = 2n * n)``] 1779QED 1780 1781val not_next_tac = 1782 REPEAT strip_tac 1783 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 1784 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 1785 \\ pop_assum kall_tac 1786 \\ REV_FULL_SIMP_TAC (srw_ss()) 1787 [DECIDE ``1 < b ==> ((b - 1 = e) = (b = e + 1n))``] 1788 \\ simp [arithmeticTheory.LEFT_ADD_DISTRIB] 1789 1790local 1791 val lem1 = Q.prove( 1792 `!a b c. a < b /\ 1n < c ==> 2 * a + 2 <= b * c`, 1793 REPEAT strip_tac 1794 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 1795 \\ simp [] 1796 ) 1797 1798 val lem1b = Q.prove( 1799 `!a b c. a + 1 < b /\ 1n < c ==> 2 * a + 2 < b * c`, 1800 REPEAT strip_tac 1801 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 1802 \\ simp [] 1803 ) 1804 1805 val lem2 = Q.prove( 1806 `!x. x <> 0w ==> 1n < 2 EXP w2n x`, 1807 Cases 1808 \\ rw [] 1809 \\ `0 < n` by decide_tac 1810 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 1811 \\ simp [GSYM arithmeticTheory.ADD1, arithmeticTheory.EXP, 1812 DECIDE ``0n < n ==> 1 < 2 * n``] 1813 ) 1814 1815 val lem3 = Q.prove( 1816 `!a b c. 2n <= b /\ 2 <= c /\ a < b ==> 2 * a + c <= b * c`, 1817 not_next_tac 1818 ) 1819 1820 val lem3b = Q.prove( 1821 `!a b c d. 0 < b /\ 2n <= d /\ 2 <= c /\ a < d ==> 1822 2 * a + c < b * c + d * c`, 1823 not_next_tac 1824 ) 1825 1826 val lem3c = Q.prove( 1827 `!a b c. 2n <= b /\ 2 <= c /\ a + 1 < b ==> 2 * a + c < b * c`, 1828 not_next_tac 1829 ) 1830 1831 val lem4 = Q.prove( 1832 `!a b c d. 1n < b /\ (4 <= a /\ c < b \/ 1833 2 <= a /\ c < b - 1 \/ 1834 2 <= a /\ c < b /\ 0 < d) ==> 1835 a + (b + c) <= a * (b + d)`, 1836 not_next_tac 1837 ) 1838 1839 val lem4b = Q.prove( 1840 `!a b c d. 2n <= a /\ 1n < b /\ 0 < d /\ c < b ==> 1841 a + (b + c) < a * (b + d)`, 1842 not_next_tac 1843 ) 1844 1845 (* |- 1 < 2 ** precision (:'a) *) 1846 val lem5 = REWRITE_RULE [wordsTheory.dimword_def] wordsTheory.ONE_LT_dimword 1847 1848 val t1 = 1849 simp [realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_LT_LDIV_EQ, 1850 realTheory.POW_ADD, realTheory.REAL_SUB_RDISTRIB, 1851 realTheory.REAL_LE_SUB_LADD, realTheory.REAL_LT_SUB_LADD, 1852 GSYM realaxTheory.REAL_LDISTRIB, cancel_rwt, cancel_rwts] 1853 \\ simp [realTheory.REAL_LDISTRIB] 1854 val t2 = 1855 once_rewrite_tac 1856 [realTheory.REAL_LT_LMUL 1857 |> Q.SPEC `2 pow bias (:'w)` 1858 |> SIMP_RULE (srw_ss()) [] 1859 |> GSYM] 1860 \\ rewrite_tac [cancel_rwts] 1861 \\ simp [realTheory.POW_ADD] 1862 \\ once_rewrite_tac 1863 [realLib.REAL_ARITH ``a * (b * c) * d = b * (a * c * d): real``] 1864 \\ simp [realTheory.REAL_LT_LMUL, realTheory.REAL_LDISTRIB] 1865 \\ match_mp_tac 1866 (realLib.REAL_ARITH 1867 ``a < 1r /\ 1 <= b /\ 0 <= c ==> 1 + a < b * 2 + c``) 1868 \\ simp [nobias_denormal_lt_1, realTheory.REAL_LE_MUL, 1869 realTheory.POW_2_LE1] 1870 val t3 = 1871 simp [realTheory.REAL_LE_LDIV_EQ, realTheory.REAL_LT_LDIV_EQ] 1872 \\ simp [realTheory.POW_ADD, cancel_rwts, 1873 realTheory.REAL_SUB_RDISTRIB, realTheory.REAL_DIV_RMUL] 1874 \\ simp [realTheory.REAL_DIV_RMUL, 1875 realLib.REAL_ARITH 1876 ``a * (b + c) * d = a * (b * d + c * d): real``] 1877 \\ simp [realTheory.REAL_LE_SUB_LADD, realTheory.REAL_LT_SUB_LADD, 1878 realTheory.REAL_LDISTRIB] 1879 val t4 = 1880 match_mp_tac (realLib.REAL_ARITH ``a <= b /\ 0r <= c ==> a <= b + c``) 1881 \\ simp [realTheory.REAL_LE_MUL, GSYM realTheory.REAL_LE_SUB_LADD] 1882 \\ once_rewrite_tac 1883 [realLib.REAL_ARITH 1884 ``p * (a * 2r) * x - (a * x + a * y) = 1885 a * ((p * (2 * x)) - (x + y))``] 1886 \\ match_mp_tac le_mult 1887 \\ simp [] 1888 \\ match_mp_tac weaken_leq 1889 \\ simp [realTheory.POW_2_LE1, realTheory.REAL_LT_MUL, 1890 realLib.REAL_ARITH ``2r * a - (a + z) = a - z``] 1891 fun tac thm q = 1892 abs_diff_tac thm 1893 >- (match_mp_tac thm \\ t2) 1894 \\ Q.ABBREV_TAC `z:real = &w2n ^(Parse.Term q)` 1895 \\ t3 1896in 1897 fun tac1 thm = 1898 abs_diff_tac thm 1899 >- (match_mp_tac thm \\ simp [subnormal_lt_normal]) 1900 \\ t1 1901 \\ match_mp_tac (realLib.REAL_ARITH ``0r <= c /\ a <= b ==> a <= b + c``) 1902 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW, 1903 fcpTheory.DIMINDEX_GE_1, lem1, lem2, lem3, lem5, 1904 word_ge1, w2n_lt_pow] 1905 val tac2 = 1906 tac abs_diff1b `(x: ('t, 'w) float).Significand` 1907 \\ t4 1908 \\ `?q. 1 <= q /\ (2 pow precision (:'t) = z + q)` 1909 by (ASSUME_TAC (Q.ISPEC `(x: ('t, 'w) float).Significand` w2n_lt_pow) 1910 \\ pop_assum 1911 (strip_assume_tac o MATCH_MP arithmeticTheory.LESS_ADD_1) 1912 \\ qexists_tac `&(p' + 1n)` 1913 \\ simp [realTheory.REAL_OF_NUM_POW, Abbr `z`]) 1914 \\ rsimp [] 1915 val tac3 = 1916 tac abs_diff2b `(y: ('t, 'w) float).Significand` 1917 \\ once_rewrite_tac 1918 [div_le 1919 |> Q.SPEC `2r pow w2n (y:('t, 'w) float).Exponent` 1920 |> SIMP_RULE (srw_ss()) [] 1921 |> GSYM] 1922 \\ simp [GSYM realTheory.REAL_DIV_ADD, GSYM realTheory.REAL_ADD_LDISTRIB, 1923 cancel_rwts] 1924 \\ rsimp [realTheory.REAL_OF_NUM_POW, Abbr `z`] 1925 \\ match_mp_tac lem4 1926 \\ full_simp_tac (srw_ss()) [exponent_boundary_def] 1927 \\ REV_FULL_SIMP_TAC (srw_ss()) 1928 [w2n_lt_pow, w2n_lt_pow_sub1, word_lt0, ge4, lem5] 1929 \\ `p <> 0` by (strip_tac \\ 1930 full_simp_tac (srw_ss()) 1931 [DECIDE ``(1 = x + 1) = (x = 0n)``]) 1932 \\ full_simp_tac (srw_ss()) [ge4] 1933 val tac4 = 1934 abs_diff_tac abs_diff1a 1935 >- (match_mp_tac abs_diff1a \\ simp [subnormal_lt_normal]) 1936 \\ t1 1937 \\ match_mp_tac (realLib.REAL_ARITH ``0r <= c /\ a < b ==> a < b + c``) 1938 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW, 1939 fcpTheory.DIMINDEX_GE_1, not_max_suc_lt_dimword, lem1b, lem2] 1940 val tac5 = 1941 abs_diff_tac abs_diff2a 1942 >- (match_mp_tac abs_diff2a \\ simp [subnormal_lt_normal]) 1943 \\ t1 1944 \\ simp [realTheory.REAL_OF_NUM_POW] 1945 \\ match_mp_tac lem3b 1946 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW, 1947 fcpTheory.DIMINDEX_GE_1, word_lt0, not_max_suc_lt_dimword, 1948 lem1b, lem2, word_ge1, w2n_lt_pow] 1949 val tac6 = 1950 tac abs_diff1b `(x: ('t, 'w) float).Significand` 1951 \\ match_mp_tac (realLib.REAL_ARITH ``a < b /\ 0r <= c ==> a < b + c``) 1952 \\ simp [realTheory.REAL_LE_MUL, GSYM realTheory.REAL_LT_SUB_LADD] 1953 \\ once_rewrite_tac 1954 [realLib.REAL_ARITH 1955 ``p * (a * 2r) * x - (a * x + a * y) = 1956 a * ((p * (2 * x)) - (x + y))``] 1957 \\ match_mp_tac (ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] gt_mult) 1958 \\ simp [] 1959 \\ match_mp_tac weaken_lt 1960 \\ simp [realTheory.POW_2_LE1, realTheory.REAL_LT_MUL, 1961 realLib.REAL_ARITH ``2r * a - (a + z) = a - z``] 1962 \\ simp [GSYM realTheory.REAL_LT_ADD_SUB, not_max_suc_lt_dimword, 1963 realTheory.REAL_OF_NUM_POW, Abbr `z`] 1964 val tac7 = 1965 tac abs_diff2b `(y: ('t, 'w) float).Significand` 1966 \\ once_rewrite_tac 1967 [realTheory.REAL_LT_RDIV 1968 |> Q.SPECL [`x`, `y`, `2 pow w2n (y:('t, 'w) float).Exponent`] 1969 |> SIMP_RULE (srw_ss()) [] 1970 |> GSYM] 1971 \\ simp [GSYM realTheory.REAL_DIV_ADD, GSYM realTheory.REAL_ADD_LDISTRIB, 1972 cancel_rwts] 1973 \\ rsimp [realTheory.REAL_OF_NUM_POW, Abbr `z`] 1974 \\ match_mp_tac lem4b 1975 \\ REV_FULL_SIMP_TAC (srw_ss()) [w2n_lt_pow, word_lt0, lem5] 1976end 1977 1978Theorem diff_exponent_ULP[local]: 1979 !x: ('t, 'w) float y: ('t, 'w) float. 1980 (x.Sign = y.Sign) /\ x.Exponent <> y.Exponent /\ 1981 ~exponent_boundary y x ==> 1982 ULP (x.Exponent, (:'t)) <= abs (float_to_real x - float_to_real y) 1983Proof 1984 rw [ULP_def, float_to_real_def] 1985 >- tac1 abs_diff1a 1986 >- tac1 abs_diff2a 1987 \\ `w2n x.Exponent < w2n y.Exponent \/ w2n y.Exponent < w2n x.Exponent` 1988 by metis_tac [arithmeticTheory.LESS_LESS_CASES, wordsTheory.w2n_11] 1989 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 1990 \\ simp [] 1991 >- tac2 1992 \\ fs [] 1993 \\ tac3 1994QED 1995 1996Theorem diff_exponent_ULP_gt[local]: 1997 !x: ('t, 'w) float y: ('t, 'w) float. 1998 (x.Sign = y.Sign) /\ x.Exponent <> y.Exponent /\ 1999 x.Significand NOTIN {0w; -1w} ==> 2000 ULP (x.Exponent, (:'t)) < abs (float_to_real x - float_to_real y) 2001Proof 2002 rw [ULP_def, float_to_real_def] 2003 >- tac4 2004 >- tac5 2005 \\ `w2n x.Exponent < w2n y.Exponent \/ w2n y.Exponent < w2n x.Exponent` 2006 by metis_tac [arithmeticTheory.LESS_LESS_CASES, wordsTheory.w2n_11] 2007 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 2008 \\ simp [] 2009 >- tac6 2010 \\ fs [] 2011 \\ tac7 2012QED 2013 2014val lem = Q.prove( 2015 `!a b m. 2n <= a /\ 2 <= b /\ 1 <= m ==> a * b + b < 2 * (m * a * b)`, 2016 REPEAT strip_tac 2017 \\ imp_res_tac arithmeticTheory.LESS_EQUAL_ADD 2018 \\ simp [arithmeticTheory.LEFT_ADD_DISTRIB] 2019 ) 2020 2021Theorem diff_exponent_ULP_gt0[local]: 2022 !x: ('t, 'w) float y: ('t, 'w) float. 2023 (x.Sign = y.Sign) /\ x.Exponent <+ y.Exponent /\ 2024 (x.Significand = 0w) /\ ~float_is_zero x ==> 2025 ULP (x.Exponent, (:'t)) < abs (float_to_real x - float_to_real y) 2026Proof 2027 rw [ULP_def, float_to_real_def, realTheory.ABS_NEG, abs_float_value, 2028 abs_significand, realTheory.ABS_MUL, realTheory.ABS_DIV, 2029 realTheory.ABS_N, gt0_abs, wordsTheory.WORD_LO] 2030 >- rfs [realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD, 2031 realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_SUB_RDISTRIB, 2032 realTheory.REAL_LT_SUB_LADD, cancel_rwts, cancel_rwt, float_is_zero] 2033 \\ abs_diff_tac abs_diff1f 2034 >- (match_mp_tac abs_diff1f 2035 \\ simp [realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_ADD_LDISTRIB, 2036 cancel_rwts] 2037 \\ simp [realTheory.REAL_OF_NUM_POW, realTheory.REAL_LE_MUL, 2038 realLib.REAL_ARITH ``a < b /\ 0 <= c ==> a < b + c: real``]) 2039 \\ simp [realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD, 2040 realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_SUB_RDISTRIB, 2041 realTheory.REAL_LT_SUB_LADD, cancel_rwts, cancel_rwt] 2042 \\ match_mp_tac (realLib.REAL_ARITH ``a < b /\ 0r <= c ==> a < b + c``) 2043 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW] 2044 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 2045 \\ simp [arithmeticTheory.EXP_ADD, lem, fcpTheory.DIMINDEX_GE_1, exp_ge4, 2046 word_ge1] 2047QED 2048 2049val lem = Q.prove( 2050 `!a b. 2 <= a /\ 4n <= b ==> 2 * a + 2 < a * b`, 2051 not_next_tac 2052 ) 2053 2054Theorem diff_exponent_ULP_gt01[local]: 2055 !x: ('t, 'w) float y: ('t, 'w) float. 2056 (x.Sign = y.Sign) /\ x.Exponent <> y.Exponent /\ 2057 y.Significand <> -1w /\ (x.Significand = 0w) /\ (x.Exponent = 1w) ==> 2058 ULP (x.Exponent, (:'t)) < abs (float_to_real x - float_to_real y) 2059Proof 2060 rw [ULP_def, float_to_real_def, realTheory.ABS_NEG, abs_float_value, 2061 abs_significand, realTheory.ABS_MUL, realTheory.ABS_DIV, 2062 realTheory.ABS_N, gt0_abs, nobias_denormal_lt_1, 2063 realLib.REAL_ARITH ``a - a * b = a * (1 - b): real``, 2064 realLib.REAL_ARITH ``a < 1 ==> (abs (1 - a) = 1 - a)``] 2065 >- (simp [realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD, cancel_rwts, 2066 realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_SUB_RDISTRIB, 2067 realTheory.REAL_LT_SUB_LADD] 2068 \\ rewrite_tac [simpLib.SIMP_PROVE (srw_ss()++ARITH_ss) [] 2069 ``&(2n * n + 2) = 2r * &(n + 1)``] 2070 \\ simp [realTheory.REAL_LT_LMUL, realTheory.REAL_OF_NUM_POW, 2071 not_max_suc_lt_dimword]) 2072 \\ `1w <+ y.Exponent` 2073 by metis_tac 2074 [wordsLib.WORD_DECIDE ``a:'a word <> 0w /\ a <> 1w ==> 1w <+ a``] 2075 \\ fs [wordsTheory.WORD_LO] 2076 \\ abs_diff_tac abs_diff1e 2077 >- (match_mp_tac abs_diff1e 2078 \\ simp [realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_LDISTRIB, 2079 cancel_rwts, cancel_rwt] 2080 \\ match_mp_tac (realLib.REAL_ARITH ``a < b /\ 0r <= c ==> a < b + c``) 2081 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW]) 2082 \\ simp [realTheory.REAL_LT_LDIV_EQ, realTheory.POW_ADD, 2083 realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_SUB_RDISTRIB, 2084 realTheory.REAL_LT_SUB_LADD, cancel_rwts, cancel_rwt] 2085 \\ match_mp_tac (realLib.REAL_ARITH ``a < b /\ 0r <= c ==> a < b + c``) 2086 \\ simp [realTheory.REAL_LE_MUL, realTheory.REAL_OF_NUM_POW, lem, 2087 fcpTheory.DIMINDEX_GE_1, exp_ge4] 2088QED 2089 2090val lem = Q.prove( 2091 `!a b c. a < b /\ 2n <= c ==> 2 * a < b * c`, 2092 not_next_tac 2093 ) 2094 2095val lem2 = Q.prove( 2096 `!a b c. a < b /\ 1n <= c ==> a + b < 2 * (c * b)`, 2097 not_next_tac 2098 ) 2099 2100Theorem float_to_real_lt_exponent_mono[local]: 2101 !x: ('t, 'w) float y: ('t, 'w) float. 2102 (x.Sign = y.Sign) /\ abs (float_to_real x) <= abs (float_to_real y) ==> 2103 x.Exponent <=+ y.Exponent 2104Proof 2105 rw [float_to_real_def, realTheory.ABS_NEG, abs_float_value, 2106 abs_significand, realTheory.ABS_MUL, realTheory.ABS_DIV, 2107 realTheory.ABS_N, gt0_abs, wordsTheory.WORD_LS] 2108 >| [ 2109 Cases_on `x.Sign = y.Sign` 2110 \\ simp [realTheory.REAL_NOT_LE] 2111 \\ once_rewrite_tac 2112 [realTheory.REAL_LT_RMUL 2113 |> Q.SPECL [`x`, `y`, `2 pow bias (:'w)`] 2114 |> REWRITE_RULE [zero_lt_twopow] 2115 |> GSYM] 2116 \\ rewrite_tac [cancel_rwts, cancel_rwt] 2117 \\ simp [realTheory.REAL_LDISTRIB, realTheory.REAL_RDISTRIB, 2118 realTheory.REAL_OF_NUM_POW, realTheory.REAL_DIV_RMUL, 2119 realTheory.REAL_LT_LDIV_EQ, realTheory.mult_ratr, 2120 cancel_rwts, cancel_rwt, w2n_lt_pow, 2121 word_ge1, lem, DECIDE ``a < b ==> a < x + b: num``], 2122 (* --- *) 2123 pop_assum mp_tac 2124 \\ Cases_on `w2n x.Exponent <= w2n y.Exponent` 2125 \\ simp [realTheory.REAL_NOT_LE] 2126 \\ fs [arithmeticTheory.NOT_LESS_EQUAL] 2127 \\ once_rewrite_tac 2128 [realTheory.REAL_LT_RMUL 2129 |> Q.SPECL [`x`, `y`, `2 pow bias (:'w)`] 2130 |> REWRITE_RULE [zero_lt_twopow] 2131 |> GSYM] 2132 \\ rewrite_tac [cancel_rwts, cancel_rwt] 2133 \\ once_rewrite_tac 2134 [realTheory.REAL_LT_RMUL 2135 |> Q.SPECL [`x`, `y`, `2 pow precision (:'t)`] 2136 |> REWRITE_RULE [zero_lt_twopow] 2137 |> GSYM] 2138 \\ rewrite_tac [cancel_rwts, cancel_rwt] 2139 \\ simp [realTheory.REAL_OF_NUM_POW] 2140 \\ match_mp_tac (DECIDE ``a < b ==> a < x + b: num``) 2141 \\ imp_res_tac arithmeticTheory.LESS_ADD_1 2142 \\ asm_simp_tac bool_ss 2143 [arithmeticTheory.EXP_ADD, arithmeticTheory.LT_MULT_RCANCEL, 2144 GSYM arithmeticTheory.RIGHT_ADD_DISTRIB, 2145 DECIDE ``a * (b * (c * d)) = (a * c * d) * b: num``] 2146 \\ simp [lem2, w2n_lt_pow] 2147 ] 2148QED 2149 2150(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 2151 2152fun tac thm = 2153 abs_diff_tac thm 2154 >- (match_mp_tac thm 2155 \\ simp [realTheory.REAL_LT_LMUL, realTheory.REAL_LT_DIV, 2156 realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_DIV_RMUL]) 2157 \\ simp [realLib.REAL_ARITH ``a < b ==> (abs (a - b) = b - a)``, 2158 realLib.REAL_ARITH ``b < a ==> (abs (a - b) = a - b)``, 2159 realTheory.REAL_SUB_RDISTRIB, realTheory.REAL_LDISTRIB, 2160 realTheory.POW_ADD, realTheory.mult_rat] 2161 \\ simp [realTheory.mult_ratr] 2162 2163fun tac2 thm = 2164 abs_diff_tac thm 2165 >- (match_mp_tac thm 2166 \\ simp [realTheory.REAL_LT_LMUL, realTheory.REAL_LT_DIV, 2167 realTheory.REAL_LT_LDIV_EQ, realTheory.REAL_DIV_RMUL]) 2168 \\ simp [realLib.REAL_ARITH ``a < b ==> (abs (a - b) = b - a)``, 2169 realLib.REAL_ARITH ``b < a ==> (abs (a - b) = a - b)``, 2170 realLib.REAL_ARITH ``1 + a - (1 + b) = a - b: real``, 2171 GSYM realTheory.REAL_SUB_LDISTRIB, sub_rat_same_base] 2172 \\ simp [realTheory.POW_ADD, realTheory.mult_rat] 2173 \\ simp_tac (srw_ss()++realSimps.real_ac_SS) [realTheory.mult_ratr] 2174 2175val diff_significand_ULP_mul = Q.prove( 2176 `!x: ('t, 'w) float y: ('t, 'w) float. 2177 (x.Sign = y.Sign) /\ (x.Exponent = y.Exponent) ==> 2178 (abs (float_to_real x - float_to_real y) = 2179 abs (&w2n x.Significand - &w2n y.Significand) * 2180 ULP (x.Exponent, (:'t)))`, 2181 rw [ULP_def, float_to_real_def] 2182 \\ (Cases_on `x.Significand = y.Significand` 2183 >- rsimp []) 2184 \\ `w2n x.Significand < w2n y.Significand \/ 2185 w2n y.Significand < w2n x.Significand` 2186 by metis_tac [arithmeticTheory.LESS_LESS_CASES, wordsTheory.w2n_11] 2187 >- tac abs_diff1c 2188 >- tac abs_diff2c 2189 >- tac2 abs_diff1d 2190 \\ tac2 abs_diff2d 2191 ) 2192 2193val diff_ge1 = Q.prove( 2194 `!a b. 1 <= abs (&a - &b) = &a <> (&b: real)`, 2195 lrw [realTheory.REAL_SUB, realTheory.ABS_NEG, realTheory.ABS_N] 2196 ) 2197 2198val diff_significand_ULP = Q.prove( 2199 `!x: ('t, 'w) float y: ('t, 'w) float. 2200 (x.Sign = y.Sign) /\ (x.Exponent = y.Exponent) /\ 2201 x.Significand <> y.Significand ==> 2202 ULP (x.Exponent, (:'t)) <= abs (float_to_real x - float_to_real y)`, 2203 rw [diff_significand_ULP_mul, ULP_gt0, diff_ge1, 2204 ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] le_mult] 2205 ) 2206 2207(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 2208 2209val ULP_same = Q.prove( 2210 `!x y. 2211 (x = y) ==> 2212 ~(ULP (x.Exponent, (:'t)) <= abs (float_to_real x - float_to_real y))`, 2213 rrw [ULP_gt0, realTheory.REAL_NOT_LE]) 2214 2215val diff_sign_neq = Q.prove( 2216 `!x: ('t, 'w) float y: ('t, 'w) float. 2217 ~(float_is_zero x /\ float_is_zero y) /\ x.Sign <> y.Sign ==> 2218 float_to_real x <> float_to_real y`, 2219 metis_tac [diff_sign_ULP, ULP_same] 2220 ) 2221 2222val diff_exponent_neq = Q.prove( 2223 `!x: ('t, 'w) float y: ('t, 'w) float. 2224 (x.Sign = y.Sign) /\ x.Exponent <> y.Exponent ==> 2225 float_to_real x <> float_to_real y`, 2226 REPEAT strip_tac 2227 \\ Cases_on `exponent_boundary y x` 2228 >- (fs [] 2229 \\ imp_res_tac diff_exponent_boundary 2230 \\ rfs [ULP_gt0, realTheory.REAL_POS_NZ]) 2231 \\metis_tac [diff_exponent_ULP, ULP_same] 2232 ) 2233 2234val float_to_real_eq = Q.store_thm("float_to_real_eq", 2235 `!x: ('t, 'w) float y: ('t, 'w) float. 2236 (float_to_real x = float_to_real y) = 2237 (x = y) \/ (float_is_zero x /\ float_is_zero y)`, 2238 NTAC 2 strip_tac 2239 \\ Cases_on `x = y` 2240 \\ simp [] 2241 \\ Cases_on `float_is_zero x /\ float_is_zero y` 2242 \\ simp [float_is_zero_to_real_imp] 2243 \\ Cases_on `x.Sign <> y.Sign` 2244 >- metis_tac [diff_sign_neq] 2245 \\ Cases_on `x.Exponent <> y.Exponent` 2246 >- metis_tac [diff_exponent_neq] 2247 \\ qpat_x_assum `~(p /\ q)` kall_tac 2248 \\ fs [float_component_equality] 2249 \\ rw [float_to_real_def, sign_not_zero, div_twopow] 2250 ) 2251 2252val diff_float_ULP = Q.store_thm("diff_float_ULP", 2253 `!x: ('t, 'w) float y: ('t, 'w) float. 2254 float_to_real x <> float_to_real y /\ ~exponent_boundary y x ==> 2255 ULP (x.Exponent, (:'t)) <= abs (float_to_real x - float_to_real y)`, 2256 rw [float_to_real_eq, float_component_equality] 2257 \\ metis_tac [diff_sign_ULP, diff_exponent_ULP, diff_significand_ULP]) 2258 2259(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 2260 2261(* |- !x y. ~float_is_zero y ==> 2262 ((float_to_real x = float_to_real y) <=> (x = y)) *) 2263Theorem float_to_real_11_right[local] = 2264 float_to_real_eq 2265 |> Drule.SPEC_ALL 2266 |> Q.DISCH `~float_is_zero y` 2267 |> SIMP_RULE bool_ss [] 2268 |> Q.GENL [`x`, `y`] 2269 2270(* |- !x y. ~float_is_zero x ==> 2271 ((float_to_real x = float_to_real y) <=> (x = y)) 2272val float_to_real_11_left = 2273 float_to_real_eq 2274 |> Drule.SPEC_ALL 2275 |> Q.DISCH `~float_is_zero x` 2276 |> SIMP_RULE bool_ss [] 2277 |> Drule.GEN_ALL 2278*) 2279 2280(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 2281 2282Theorem diff1pos[local]: 2283 !a. a <> 0w ==> (&w2n a - &w2n (a + -1w) = 1r) 2284Proof 2285 Cases 2286 \\ Cases_on `n` 2287 \\ simp [wordsTheory.n2w_SUC] 2288 \\ rrw [realTheory.REAL_SUB, bitTheory.SUC_SUB, DECIDE ``~(SUC n <= n)``] 2289QED 2290 2291Theorem diff1neg[local]: 2292 !a. a <> -1w ==> (&w2n a - &w2n (a + 1w) = -1r) 2293Proof 2294 rw [realTheory.REAL_SUB, bitTheory.SUC_SUB, DECIDE ``~(SUC n <= n)``, 2295 GSYM wordsTheory.WORD_LS, 2296 ONCE_REWRITE_RULE [GSYM wordsTheory.WORD_ADD_COMM] 2297 wordsTheory.WORD_ADD_RIGHT_LS2] 2298 \\ lfs [wordsTheory.WORD_NOT_LOWER, wordsTheory.WORD_LS_word_T] 2299 \\ `a <=+ a + 1w` by wordsLib.WORD_DECIDE_TAC 2300 \\ simp [GSYM wordsTheory.word_sub_w2n] 2301QED 2302 2303Theorem must_be_1[local]: 2304 !a b: real. 0 < b ==> ((a * b = b) = (a = 1)) 2305Proof 2306 REPEAT strip_tac 2307 \\ Cases_on `a = 1` 2308 >- simp [] 2309 \\ Cases_on `a < 1` 2310 >- rsimp [realTheory.REAL_LT_IMP_NE, 2311 ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] lt_mult] 2312 \\ `1 < a` by rsimp [] 2313 \\ simp [realTheory.REAL_LT_IMP_NE, gt_mult] 2314QED 2315 2316Theorem w2n_add1[local]: 2317 !a. a <> -1w ==> (w2n a + 1 = w2n (a + 1w)) 2318Proof 2319 Cases 2320 \\ lrw [wordsTheory.word_eq_n2w, wordsTheory.word_add_n2w, 2321 bitTheory.MOD_2EXP_MAX_def, bitTheory.MOD_2EXP_def, 2322 GSYM wordsTheory.dimword_def] 2323QED 2324 2325Theorem diff_ulp_next_float[local]: 2326 !x y: ('t, 'w) float. 2327 ~float_is_zero x /\ y.Significand NOTIN {0w; -1w} ==> 2328 ((abs (float_to_real y - float_to_real x) = ULP (y.Exponent,(:'t))) = 2329 (x = y with Significand := y.Significand - 1w) \/ 2330 (x = y with Significand := y.Significand + 1w)) 2331Proof 2332 REPEAT strip_tac 2333 \\ eq_tac 2334 >| [ 2335 `~float_is_zero y` by fs [float_is_zero] 2336 \\ Cases_on `x.Sign <> y.Sign` 2337 >- prove_tac [realTheory.REAL_LT_IMP_NE, diff_sign_ULP_gt] 2338 \\ Cases_on `x.Exponent <> y.Exponent` 2339 >- prove_tac [realTheory.REAL_LT_IMP_NE, diff_exponent_ULP_gt] 2340 \\ fs [diff_significand_ULP_mul, must_be_1, ULP_gt0, 2341 float_component_equality] 2342 \\ Cases_on `x.Significand = y.Significand + -1w` 2343 \\ simp [] 2344 \\ Cases_on `x.Significand = y.Significand + 1w` 2345 \\ rsimp [realLib.REAL_ARITH ``(abs x = 1) = (x = 1) \/ (x = -1)``, 2346 realLib.REAL_ARITH ``(a = -1 + c) = (c = a + 1r)``, 2347 realTheory.REAL_EQ_SUB_RADD, w2n_add1] 2348 \\ Cases_on `x.Significand = -1w` 2349 \\ simp [ONCE_REWRITE_RULE [arithmeticTheory.ADD_COMM] w2n_add1, 2350 wordsTheory.w2n_minus1, DECIDE ``0n < n ==> (1 + (n - 1) = n)``, 2351 wordsTheory.w2n_lt, prim_recTheory.LESS_NOT_EQ, 2352 wordsLib.WORD_ARITH_PROVE 2353 ``a:'a word <> b + -1w ==> b <> a + 1w``], 2354 (* --- *) 2355 rw [] 2356 \\ rw [float_to_real_def, abs_float_value, abs_significand, 2357 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, 2358 gt0_abs, GSYM realTheory.REAL_SUB_LDISTRIB, sub_rat_same_base, 2359 realLib.REAL_ARITH ``1r + a - (1 + b) = a - b``] 2360 \\ fs [diff1pos, diff1neg, realTheory.mult_rat, ULP_def, 2361 realTheory.POW_ADD] 2362 ] 2363QED 2364 2365Theorem diff_ulp_next_float0[local]: 2366 !x y: ('t, 'w) float. 2367 ~float_is_zero x /\ ~float_is_zero y /\ (y.Significand = 0w) /\ 2368 abs (float_to_real y) <= abs (float_to_real x) ==> 2369 ((abs (float_to_real y - float_to_real x) = ULP (y.Exponent,(:'t))) = 2370 (x = y with Significand := y.Significand + 1w)) 2371Proof 2372 REPEAT strip_tac 2373 \\ eq_tac 2374 >| [ 2375 Cases_on `x.Sign <> y.Sign` 2376 >- prove_tac [realTheory.REAL_LT_IMP_NE, diff_sign_ULP_gt] 2377 \\ imp_res_tac float_to_real_lt_exponent_mono 2378 \\ Cases_on `x.Exponent <> y.Exponent` 2379 >- prove_tac 2380 [realTheory.REAL_LT_IMP_NE, diff_exponent_ULP_gt0, 2381 wordsLib.WORD_DECIDE ``a <> b /\ a <=+ b ==> a <+ b:'a word``] 2382 \\ fs [diff_significand_ULP_mul, must_be_1, ULP_gt0, 2383 float_component_equality, realTheory.ABS_NEG, realTheory.ABS_N] 2384 \\ Cases_on `x.Significand` 2385 \\ simp [], 2386 (* --- *) 2387 rw [] 2388 \\ rw [float_to_real_def, abs_float_value, abs_significand, 2389 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, 2390 realTheory.ABS_NEG, gt0_abs, realTheory.REAL_LDISTRIB, 2391 realLib.REAL_ARITH ``a - (a + c) = -c: real``] 2392 \\ fs [diff1pos, diff1neg, realTheory.mult_rat, ULP_def, 2393 realTheory.POW_ADD] 2394 ] 2395QED 2396 2397Theorem diff_ulp_next_float01[local]: 2398 !x y: ('t, 'w) float. 2399 ~float_is_zero x /\ ~float_is_zero y /\ 2400 x.Significand <> -1w /\ (y.Significand = 0w) /\ (y.Exponent = 1w) ==> 2401 ((abs (float_to_real y - float_to_real x) = ULP (y.Exponent,(:'t))) = 2402 (x = y with Significand := y.Significand + 1w)) 2403Proof 2404 REPEAT strip_tac 2405 \\ eq_tac 2406 >| [ 2407 Cases_on `x.Sign <> y.Sign` 2408 >- prove_tac [realTheory.REAL_LT_IMP_NE, diff_sign_ULP_gt] 2409 \\ Cases_on `x.Exponent <> y.Exponent` 2410 >- prove_tac [realTheory.REAL_LT_IMP_NE, diff_exponent_ULP_gt01] 2411 \\ fs [diff_significand_ULP_mul, must_be_1, ULP_gt0, 2412 float_component_equality, realTheory.ABS_NEG, realTheory.ABS_N] 2413 \\ Cases_on `x.Significand` 2414 \\ simp [], 2415 (* --- *) 2416 rw [] 2417 \\ rw [float_to_real_def, abs_float_value, abs_significand, 2418 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, 2419 realTheory.ABS_NEG, gt0_abs, realTheory.REAL_LDISTRIB, 2420 realLib.REAL_ARITH ``a - (a + c) = -c: real``] 2421 \\ fs [diff1pos, diff1neg, realTheory.mult_rat, ULP_def, 2422 realTheory.POW_ADD] 2423 ] 2424QED 2425 2426Theorem float_min_equiv_ULP_eq_float_to_real[local]: 2427 !y: ('t, 'w) float. 2428 (abs (float_to_real y) = ULP (y.Exponent,(:'t))) <=> 2429 y IN {float_plus_min (:'t # 'w); float_minus_min (:'t # 'w)} 2430Proof 2431 strip_tac 2432 \\ Cases_on `float_is_zero y` 2433 >- fs [float_sets, zero_to_real, float_components, float_distinct, 2434 GSYM float_distinct, ULP_gt0, 2435 realLib.REAL_ARITH ``0 < b ==> 0r <> b``] 2436 \\ Cases_on `(y = float_plus_min (:'t # 'w)) \/ 2437 (y = float_minus_min (:'t # 'w))` 2438 >- rw [GSYM neg_ulp, GSYM ulp, float_minus_min_def, float_components, 2439 ulp_def, ULP_gt0, gt0_abs, realTheory.REAL_LT_IMP_LE, 2440 realTheory.ABS_NEG] 2441 \\ fs [] 2442 \\ rw [float_to_real_def, ULP_def, abs_float_value, abs_significand, 2443 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, gt0_abs, 2444 realTheory.REAL_EQ_RDIV_EQ] 2445 \\ simp [realTheory.POW_ADD, GSYM realTheory.REAL_LDISTRIB, 2446 cancel_rwts, cancel_rwt, realTheory.REAL_DIV_REFL, 2447 realTheory.REAL_EQ_RDIV_EQ 2448 |> ONCE_REWRITE_RULE [GSYM realTheory.REAL_MUL_COMM] 2449 |> GSYM] 2450 >| [ 2451 strip_tac 2452 \\ `y.Significand = 1w` 2453 by metis_tac [wordsTheory.w2n_11, wordsTheory.word_1_n2w] 2454 \\ fs [float_plus_min_def, float_minus_min_def, float_negate_def, 2455 float_component_equality] 2456 \\ metis_tac [sign_inconsistent], 2457 simp [realTheory.REAL_OF_NUM_POW, GSYM wordsTheory.dimword_def, 2458 DECIDE ``1 < a ==> a + b <> 1n``] 2459 ] 2460QED 2461 2462(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 2463 2464val tac = 2465 REPEAT strip_tac 2466 \\ spose_not_then assume_tac 2467 \\ `float_to_real a <> float_to_real b` 2468 by metis_tac [float_to_real_eq] 2469 \\ imp_res_tac diff_float_ULP 2470 \\ rlfs [] 2471 2472val diff_lt_ulp_eq0 = Q.store_thm("diff_lt_ulp_eq0", 2473 `!a: ('t, 'w) float b: ('t, 'w) float x. 2474 ~exponent_boundary b a /\ 2475 abs (x - float_to_real a) < ULP (a.Exponent, (:'t)) /\ 2476 abs (x - float_to_real b) < ULP (a.Exponent, (:'t)) /\ 2477 abs (float_to_real a) <= abs x /\ abs (float_to_real b) <= abs x /\ 2478 ~float_is_zero a ==> 2479 (b = a)`, 2480 tac) 2481 2482val diff_lt_ulp_even = Q.store_thm("diff_lt_ulp_even", 2483 `!a: ('t, 'w) float b: ('t, 'w) float x. 2484 ~exponent_boundary b a /\ 2485 2 * abs (float_to_real a - x) < ULP (a.Exponent, (:'t)) /\ 2486 2 * abs (float_to_real b - x) < ULP (a.Exponent, (:'t)) /\ 2487 ~float_is_zero a ==> 2488 (b = a)`, 2489 REPEAT strip_tac 2490 \\ spose_not_then assume_tac 2491 \\ `float_to_real a <> float_to_real b` 2492 by metis_tac [float_to_real_eq] 2493 \\ imp_res_tac diff_float_ULP 2494 \\ rlfs [] 2495 ) 2496 2497val diff_lt_ulp_even4 = Q.store_thm("diff_lt_ulp_even4", 2498 `!a: ('t, 'w) float b: ('t, 'w) float x. 2499 ~exponent_boundary b a /\ 2500 4 * abs (float_to_real a - x) <= ULP (a.Exponent, (:'t)) /\ 2501 4 * abs (float_to_real b - x) <= ULP (a.Exponent, (:'t)) /\ 2502 ~float_is_zero a ==> 2503 (b = a)`, 2504 REPEAT strip_tac 2505 \\ spose_not_then assume_tac 2506 \\ `float_to_real a <> float_to_real b` 2507 by metis_tac [float_to_real_eq] 2508 \\ imp_res_tac diff_float_ULP 2509 \\ rlfs [] 2510 ) 2511 2512(* 2513val diff_lt_ulp_eq_pos = Q.store_thm("diff_lt_ulp_eq_pos", 2514 `!a: ('t, 'w) float b: ('t, 'w) float x. 2515 ~exponent_boundary b a /\ 2516 abs (x - float_to_real a) < ULP (a.Exponent, (:'t)) /\ 2517 abs (x - float_to_real b) < ULP (a.Exponent, (:'t)) /\ 2518 float_to_real a >= x /\ float_to_real b >= x /\ 2519 ~float_is_zero b ==> 2520 (a = b)`, 2521 tac) 2522 2523val diff_lt_ulp_eq_neg = Q.store_thm("diff_lt_ulp_eq_neg", 2524 `!a: ('t, 'w) float b: ('t, 'w) float x. 2525 ~exponent_boundary b a /\ 2526 abs (x - float_to_real a) < ULP (a.Exponent, (:'t)) /\ 2527 abs (x - float_to_real b) < ULP (a.Exponent, (:'t)) /\ 2528 float_to_real a <= x /\ float_to_real b <= x /\ 2529 ~float_is_zero b ==> 2530 (a = b)`, 2531 tac) 2532*) 2533 2534val exponent_boundary_lt = Q.prove( 2535 `!a b. 2536 exponent_boundary a b ==> abs (float_to_real a) < abs (float_to_real b)`, 2537 rrw [float_to_real_def, exponent_boundary_def, abs_float_value, 2538 abs_significand, realTheory.ABS_MUL, realTheory.ABS_DIV, 2539 realTheory.ABS_N, gt0_abs] 2540 >- (match_mp_tac lt_mult 2541 \\ rsimp [nobias_denormal_lt_1, realTheory.REAL_LT_DIV]) 2542 \\ simp [realTheory.REAL_LT_LMUL, realTheory.REAL_LT_RDIV_EQ, cancel_rwts, 2543 realTheory.POW_ADD, realLib.REAL_ARITH ``1 + x < 2 = x < 1r``, 2544 nobias_denormal_lt_1] 2545 ) 2546 2547val exponent_boundary_not_float_zero = Q.prove( 2548 `!x y. exponent_boundary x y ==> ~float_is_zero y`, 2549 rw [exponent_boundary_def, float_is_zero] 2550 \\ strip_tac 2551 \\ fs [] 2552 ) 2553 2554val ULP_lt_float_to_real = Q.prove( 2555 `!y:('t,'w) float. 2556 ~float_is_zero y ==> ULP (y.Exponent,(:'t)) <= abs (float_to_real y)`, 2557 rw [ULP_def, float_to_real_def, abs_float_value, abs_significand, 2558 realTheory.ABS_MUL, realTheory.ABS_DIV, realTheory.ABS_N, 2559 gt0_abs, realTheory.REAL_LE_LDIV_EQ, float_is_zero, GSYM word_lt0] 2560 \\ simp [realTheory.POW_ADD, cancel_rwt, cancel_rwts] 2561 \\ simp [GSYM realTheory.REAL_LDISTRIB, realTheory.POW_2_LE1, 2562 le_mult, realLib.REAL_ARITH ``1r <= x /\ 0 <= n ==> 1 <= x + n``] 2563 ) 2564 2565(* |- !y. ~float_is_zero y ==> ulp (:'t # 'w) <= abs (float_to_real y) *) 2566val ulp_lt_float_to_real = 2567 diff_float_ULP 2568 |> Q.SPEC `float_plus_zero (:'t # 'w)` 2569 |> SIMP_RULE (srw_ss()) 2570 [realTheory.ABS_NEG, float_components, zero_to_real, zero_properties, 2571 exponent_boundary_def, GSYM ulp_def, GSYM float_is_zero_to_real] 2572 2573val abs_limits = realLib.REAL_ARITH ``!x l. abs x <= l = ~(x < -l) /\ ~(x > l)`` 2574 2575val abs_limits2 = 2576 realLib.REAL_ARITH ``!x l. abs x < l = ~(x <= -l) /\ ~(x >= l)`` 2577 2578(* ------------------------------------------------------------------------ 2579 Rounding to regular value 2580 ------------------------------------------------------------------------ *) 2581 2582val round_roundTowardZero = Q.store_thm("round_roundTowardZero", 2583 `!y: ('t, 'w) float x r. 2584 (float_value y = Float r) /\ 2585 abs (r - x) < ULP (y.Exponent, (:'t)) /\ abs r <= abs x /\ 2586 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2587 (round roundTowardZero x = y)`, 2588 lrw [round_def, closest_def, is_closest_def, closest_such_def] 2589 >- imp_res_tac abs_limits 2590 >- imp_res_tac abs_limits 2591 \\ SELECT_ELIM_TAC 2592 \\ rw [] 2593 >| [ 2594 qexists_tac `y` 2595 \\ imp_res_tac Float_float_to_real 2596 \\ rw [Float_is_finite] 2597 \\ Cases_on `float_to_real b = float_to_real y` 2598 >- simp [] 2599 \\ Cases_on `exponent_boundary b y` 2600 >- (`ULP (y.Exponent,(:'t)) <= abs (float_to_real y)` 2601 by metis_tac [ULP_lt_float_to_real, exponent_boundary_not_float_zero] 2602 \\ match_mp_tac 2603 (realLib.REAL_ARITH 2604 ``abs (a - x) < abs x /\ abs b < abs a /\ abs a <= abs x ==> 2605 abs (a - x) <= abs (b - x)``) 2606 \\ rsimp [exponent_boundary_lt]) 2607 \\ match_mp_tac 2608 (realLib.REAL_ARITH 2609 ``ULP ((y: ('t, 'w) float).Exponent, (:'t)) <= abs (ra - rb) /\ 2610 abs (ra - x) < ULP (y.Exponent, (:'t)) /\ 2611 abs ra <= abs x /\ abs rb <= abs x ==> 2612 abs (ra - x) <= abs (rb - x)``) 2613 \\ simp [] 2614 \\ metis_tac [diff_float_ULP], 2615 (* -- *) 2616 Cases_on `float_is_zero y` 2617 >- ( 2618 `r = 0` by (pop_assum mp_tac \\ simp [float_is_zero_def]) 2619 \\ `y.Exponent = 0w` 2620 by (qpat_x_assum `float_is_zero y` mp_tac \\ simp [float_is_zero]) 2621 \\ rlfs [ulp_def] 2622 \\ metis_tac [realLib.REAL_ARITH ``~(x < b /\ b <= x: real)``] 2623 ) 2624 \\ imp_res_tac Float_float_to_real 2625 \\ pop_assum (SUBST_ALL_TAC o SYM) 2626 \\ `abs (float_to_real x' - x) <= abs (float_to_real y - x)` 2627 by metis_tac [Float_is_finite] 2628 \\ `abs (x - float_to_real x') < ULP (y.Exponent, (:'t))` 2629 by metis_tac [realTheory.REAL_LET_TRANS, realTheory.ABS_SUB] 2630 \\ Cases_on `exponent_boundary x' y` 2631 >- ( 2632 `ULP (y.Exponent,(:'t)) <= abs (float_to_real y)` 2633 by metis_tac [ULP_lt_float_to_real, exponent_boundary_not_float_zero] 2634 \\ `abs (float_to_real y - x) <= abs (float_to_real x' - x)` 2635 by (match_mp_tac 2636 (realLib.REAL_ARITH 2637 ``abs (a - x) < abs x /\ abs b < abs a /\ abs a <= abs x ==> 2638 abs (a - x) <= abs (b - x)``) 2639 \\ rsimp [exponent_boundary_lt] 2640 ) 2641 \\ simp [GSYM float_to_real_11_right] 2642 \\ match_mp_tac 2643 (realLib.REAL_ARITH 2644 ``abs a <= abs x /\ abs b <= abs x /\ 2645 (abs (a - x) = abs (b - x)) ==> (a = b)``) 2646 \\ rsimp [] 2647 ) 2648 \\ match_mp_tac diff_lt_ulp_eq0 2649 \\ qexists_tac `x` 2650 \\ rsimp [] 2651 ]) 2652 2653(* 2654val ULP01 = Q.store_thm("ULP01", 2655 `ULP (0w:'w word, (:'t)) = ULP (1w:'w word, (:'t))`, 2656 rw [ULP_def] 2657 ) 2658 2659val ULP_lt_mono = Q.store_thm("ULP_lt_mono", 2660 `!e1 e2. 1w <+ e2 ==> (ULP (e1, (:'t)) < ULP (e2, (:'t)) = e1 <+ e2)`, 2661 Cases 2662 \\ Cases 2663 \\ lrw [ULP_def, wordsTheory.word_lo_n2w, realTheory.REAL_LT_RDIV] 2664 \\ simp [realTheory.REAL_OF_NUM_POW] 2665 ) 2666 2667val exponent_boundary_exp_gt1 = Q.prove( 2668 `!b y: ('t, 'w) float. 2669 exponent_boundary b y ==> b.Exponent <+ y.Exponent /\ 1w <+ y.Exponent`, 2670 rw [exponent_boundary_def, wordsTheory.WORD_LO] 2671 \\ Cases_on `b.Exponent` 2672 \\ Cases_on `y.Exponent` 2673 \\ lfs [] 2674 ) 2675*) 2676 2677val word_lsb_plus_1 = Q.prove( 2678 `!a. word_lsb (a + 1w) = ~word_lsb a`, 2679 Cases 2680 \\ simp [wordsTheory.word_add_n2w, arithmeticTheory.ODD, 2681 GSYM arithmeticTheory.ADD1] 2682 ) 2683 2684val word_lsb_minus_1 = Q.prove( 2685 `!a. word_lsb (a - 1w) = ~word_lsb a`, 2686 Cases 2687 \\ Cases_on `n` 2688 \\ simp [GSYM wordsTheory.word_add_n2w, arithmeticTheory.ODD, 2689 arithmeticTheory.ADD1] 2690 ) 2691 2692val tac = 2693 qpat_x_assum `!a. q \/ t` (qspec_then `y` strip_assume_tac) 2694 \\ fs [realTheory.REAL_NOT_LE] 2695 \\ qpat_x_assum `!b. p` (qspec_then `b` imp_res_tac) 2696 \\ rlfs [] 2697 \\ rfs [] 2698 2699val round_roundTiesToEven = Q.store_thm("round_roundTiesToEven", 2700 `!y: ('t, 'w) float x r. 2701 (float_value y = Float r) /\ 2702 ((y.Significand = 0w) /\ y.Exponent <> 1w ==> abs r <= abs x) /\ 2703 2 * abs (r - x) <= ULP (y.Exponent, (:'t)) /\ 2704 ((2 * abs (r - x) = ULP (y.Exponent, (:'t))) ==> 2705 ~word_lsb (y.Significand)) /\ 2706 ulp (:'t # 'w) < 2 * abs x /\ abs x < threshold (:'t # 'w) ==> 2707 (round roundTiesToEven x = y)`, 2708 lrw [round_def, closest_def, is_closest_def, closest_such_def, 2709 pred_setTheory.SPECIFICATION] 2710 >- imp_res_tac abs_limits2 2711 >- imp_res_tac abs_limits2 2712 \\ SELECT_ELIM_TAC 2713 \\ rw [] 2714 >| [ 2715 qexists_tac `y` 2716 \\ imp_res_tac Float_float_to_real 2717 \\ `float_is_finite y` by simp [Float_is_finite] 2718 \\ rw [] 2719 >| [ 2720 Cases_on `float_to_real y = float_to_real b` 2721 >- simp [] 2722 \\ Cases_on `exponent_boundary b y` 2723 >- ( 2724 `ULP (y.Exponent,(:'t)) <= abs (float_to_real y)` 2725 by metis_tac [ULP_lt_float_to_real, exponent_boundary_not_float_zero] 2726 \\ imp_res_tac exponent_boundary_lt 2727 \\ `2 * abs (float_to_real y - x) <= abs (float_to_real y)` 2728 by imp_res_tac realTheory.REAL_LE_TRANS 2729 \\ match_mp_tac 2730 (realLib.REAL_ARITH 2731 ``abs b < abs a /\ abs a <= abs x /\ 2732 2 * abs (a - x) <= abs a ==> abs (a - x) <= abs (b - x)``) 2733 \\ rlfs [exponent_boundary_def] 2734 ) 2735 \\ metis_tac 2736 [diff_float_ULP, 2737 realLib.REAL_ARITH 2738 ``2 * abs (r - x) <= u /\ u <= abs (r - b) ==> 2739 abs (r - x) <= abs (b - x)``], 2740 (* -- *) 2741 strip_tac 2742 \\ fs [] 2743 \\ `a' <> y` by metis_tac [] 2744 \\ Cases_on `float_is_zero y` 2745 >- fs [float_is_zero] 2746 \\ `float_to_real y <> float_to_real a'` 2747 by simp [float_to_real_eq] 2748 \\ Cases_on `exponent_boundary a' y` 2749 >- fs [exponent_boundary_def] 2750 \\ imp_res_tac diff_float_ULP 2751 \\ `2 * abs (float_to_real y - x) < ULP (y.Exponent,(:'t))` 2752 by rsimp [] 2753 \\ metis_tac 2754 [realLib.REAL_ARITH 2755 ``2 * abs (r - x) < u /\ u <= abs (r - a) ==> 2756 ~(abs (a - x) <= abs (r - x))``] 2757 ], 2758 (* -- *) 2759 `float_is_finite y` by simp [Float_is_finite] 2760 \\ Cases_on `float_is_zero y` 2761 >- (`r = 0` by (pop_assum mp_tac \\ simp [float_is_zero_def]) 2762 \\ `y.Exponent = 0w` 2763 by (qpat_x_assum `float_is_zero y` mp_tac \\ simp [float_is_zero]) 2764 \\ rlfs [ulp_def] 2765 \\ metis_tac [ULP_gt0, 2766 realLib.REAL_ARITH ``~(0 < x /\ x < b /\ 2 * b <= x: real)``]) 2767 \\ imp_res_tac Float_float_to_real 2768 \\ pop_assum (SUBST_ALL_TAC o SYM) 2769 \\ Cases_on `exponent_boundary x' y` 2770 >- (`abs (float_to_real y) <= abs x` by fs [exponent_boundary_def] 2771 \\ metis_tac 2772 [realTheory.REAL_LE_TRANS, exponent_boundary_lt, 2773 ULP_lt_float_to_real, 2774 realLib.REAL_ARITH 2775 ``~(2 * abs (a - x) <= abs a /\ abs a <= abs x /\ 2776 abs b < abs a /\ abs (b - x) <= abs (a - x))``]) 2777 \\ Cases_on `2 * abs (float_to_real y - x) < ULP (y.Exponent,(:'t))` 2778 >- (`2 * abs (float_to_real x' - x) <= 2 * abs (float_to_real y - x)` 2779 by metis_tac [Float_is_finite, 2780 realLib.REAL_ARITH ``2 * abs a <= 2 * abs b = abs a <= abs b``] 2781 \\ metis_tac [realTheory.REAL_LET_TRANS, diff_lt_ulp_even]) 2782 \\ `2 * abs (float_to_real y - x) = ULP (y.Exponent,(:'t))` by rsimp [] 2783 \\ fs [] 2784 \\ Cases_on `float_to_real y = float_to_real x'` 2785 >- (fs [float_to_real_eq] \\ fs []) 2786 \\ imp_res_tac diff_float_ULP 2787 \\ `abs (float_to_real x' - x) <= abs (float_to_real y - x)` 2788 by metis_tac [] 2789 \\ `abs (float_to_real y - float_to_real x') = 2790 ULP (y.Exponent,(:'t))` 2791 by metis_tac 2792 [realLib.REAL_ARITH 2793 ``(2 * abs (a - x) = u) /\ u <= abs (a - b) /\ 2794 abs (b - x) <= abs (a - x) ==> (abs (a - b) = u)``] 2795 \\ `y.Significand <> -1w` by (strip_tac \\ fs []) 2796 \\ `~float_is_zero x'` 2797 by (strip_tac 2798 \\ imp_res_tac float_is_zero_to_real 2799 \\ fs [float_min_equiv_ULP_eq_float_to_real] 2800 \\ fs [float_components]) 2801 \\ Cases_on `y.Significand = 0w` 2802 >- (qpat_x_assum `~float_is_zero y` assume_tac 2803 \\ `x'.Significand <> -1w` by (strip_tac \\ fs [] \\ tac) 2804 \\ Cases_on `y.Exponent = 1w` 2805 >- (fs [diff_ulp_next_float01] \\ tac) 2806 \\ Cases_on `abs (float_to_real x') < abs (float_to_real y)` 2807 \\ fs [realTheory.REAL_NOT_LT] 2808 >- metis_tac 2809 [realTheory.REAL_LE_TRANS, ULP_lt_float_to_real, 2810 realLib.REAL_ARITH 2811 ``~(2 * abs (a - x) <= abs a /\ abs a <= abs x /\ 2812 abs b < abs a /\ abs (b - x) <= abs (a - x))``] 2813 \\ `abs (float_to_real x' - x) = abs (float_to_real y - x)` 2814 by imp_res_tac 2815 (realLib.REAL_ARITH 2816 ``(2 * abs (a - x) = u) /\ abs (b - x) <= abs (a - x) /\ 2817 (abs (a - b) = u) ==> (abs (b - x) = abs (a - x))``) 2818 \\ fs [diff_ulp_next_float0] 2819 \\ tac 2820 ) 2821 \\ `y.Significand NOTIN {0w; -1w}` by simp [] 2822 \\ fs [diff_ulp_next_float] 2823 \\ `word_lsb x'.Significand` 2824 by simp [word_lsb_plus_1, SIMP_RULE (srw_ss()) [] word_lsb_minus_1] 2825 \\ fs [] 2826 \\ tac 2827 ]) 2828 2829val not_one_lem = wordsLib.WORD_DECIDE ``(x:'a word) <> 1w ==> w2n x <> 1`` 2830val pow_add1 = REWRITE_RULE [arithmeticTheory.ADD1] realTheory.pow 2831 2832val exponent_boundary_ULPs = Q.prove( 2833 `!x y. exponent_boundary x y ==> 2834 (ULP (y.Exponent, (:'t)) = 2 * ULP (x.Exponent, (:'t)))`, 2835 srw_tac [] [exponent_boundary_def, ULP_def, pow_add1, realTheory.mult_ratr] 2836 \\ fs [not_one_lem] 2837 ) 2838 2839val round_roundTiesToEven0 = Q.store_thm("round_roundTiesToEven0", 2840 `!y: ('t, 'w) float x r. 2841 (float_value y = Float r) /\ 2842 ((y.Significand = 0w) /\ y.Exponent <> 1w /\ ~(abs r <= abs x)) /\ 2843 4 * abs (r - x) <= ULP (y.Exponent, (:'t)) /\ 2844 ulp (:'t # 'w) < 2 * abs x /\ abs x < threshold (:'t # 'w) ==> 2845 (round roundTiesToEven x = y)`, 2846 lrw [round_def, closest_def, is_closest_def, closest_such_def, 2847 pred_setTheory.SPECIFICATION] 2848 >- imp_res_tac abs_limits2 2849 >- imp_res_tac abs_limits2 2850 \\ SELECT_ELIM_TAC 2851 \\ rw [] 2852 >| [ 2853 qexists_tac `y` 2854 \\ imp_res_tac Float_float_to_real 2855 \\ `float_is_finite y` by simp [Float_is_finite] 2856 \\ rw [] 2857 \\ Cases_on `float_to_real y = float_to_real b` 2858 >- simp [] 2859 \\ Cases_on `exponent_boundary b y` 2860 >- ( 2861 imp_res_tac diff_exponent_boundary 2862 \\ `2 * ULP (b.Exponent,(:'t)) = ULP (y.Exponent,(:'t))` 2863 by (fs [exponent_boundary_def, ULP_def] 2864 \\ rw [pow_add1, realTheory.mult_ratr] 2865 \\ fs [not_one_lem]) 2866 \\ match_mp_tac 2867 (realLib.REAL_ARITH 2868 ``~(abs a <= abs x) /\ 4 * abs (a - x) <= 2 * abs (a - b) ==> 2869 abs (a - x) <= abs (b - x)``) 2870 \\ simp [] 2871 ) 2872 \\ metis_tac 2873 [diff_float_ULP, 2874 realLib.REAL_ARITH ``4 * abs (r - x) <= u /\ u <= abs (r - b) ==> 2875 abs (r - x) <= abs (b - x)``], 2876 (* -- *) 2877 `float_is_finite y` by simp [Float_is_finite] 2878 \\ Cases_on `float_is_zero y` 2879 >- (`r = 0` by (pop_assum mp_tac \\ simp [float_is_zero_def]) 2880 \\ `y.Exponent = 0w` 2881 by (qpat_x_assum `float_is_zero y` mp_tac \\ simp [float_is_zero]) 2882 \\ rlfs [ulp_def]) 2883 \\ imp_res_tac Float_float_to_real 2884 \\ pop_assum (SUBST_ALL_TAC o SYM) 2885 \\ `abs (float_to_real x' - x) <= abs (float_to_real y - x)` by res_tac 2886 \\ `4 * abs (float_to_real x' - x) <= 4 * abs (float_to_real y - x)` 2887 by rsimp [] 2888 \\ `4 * abs (float_to_real x' - x) <= ULP (y.Exponent,(:'t))` 2889 by metis_tac [realTheory.REAL_LE_TRANS] 2890 \\ match_mp_tac diff_lt_ulp_even4 2891 \\ qexists_tac `x` 2892 \\ simp [] 2893 \\ spose_not_then assume_tac 2894 \\ imp_res_tac exponent_boundary_ULPs 2895 \\ fs [realLib.REAL_ARITH ``4r * a <= 2 * b = 2 * a <= b``] 2896 \\ imp_res_tac diff_exponent_boundary 2897 \\ `abs (float_to_real x' - x) = abs (float_to_real y - x)` 2898 by metis_tac 2899 [realLib.REAL_ARITH 2900 ``2 * abs (a - x) <= u /\ 2901 2 * abs (b - x) <= u /\ 2902 (abs (a - b) = u) ==> (abs (a - x) = abs (b - x))``] 2903 \\ `~word_lsb y.Significand ==> ~word_lsb x'.Significand` 2904 by metis_tac [] 2905 \\ rfs [exponent_boundary_def] 2906 ]) 2907 2908(* 2909 2910val round_roundTowardPositive = Q.store_thm("round_roundTowardPositive", 2911 `!y: ('t, 'w) float x r. 2912 (float_value y = Float r) /\ 2913 abs (x - r) < ulp (:'t # 'w) /\ r >= x /\ 2914 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2915 (round roundTowardPositive x = y)`, 2916 tac (realLib.REAL_ARITH 2917 ``ulp (:'t # 'w) <= abs (ra - rb) /\ 2918 abs (x - ra) < ulp (:'t # 'w) /\ 2919 ra >= x /\ rb >= x ==> 2920 abs (ra - x) <= abs (rb - x)``) 2921 diff_lt_ulp_eq_pos) 2922 2923val round_roundTowardNegative = Q.store_thm("round_roundTowardNegative", 2924 `!y: ('t, 'w) float x r. 2925 (float_value y = Float r) /\ 2926 abs (x - r) < ulp (:'t # 'w) /\ r <= x /\ 2927 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2928 (round roundTowardNegative x = y)`, 2929 tac (realLib.REAL_ARITH 2930 ``ulp (:'t # 'w) <= abs (ra - rb) /\ 2931 abs (x - ra) < ulp (:'t # 'w) /\ 2932 ra <= x /\ rb <= x ==> 2933 abs (ra - x) <= abs (rb - x)``) 2934 diff_lt_ulp_eq_neg) 2935 2936val tac = 2937 REPEAT strip_tac 2938 \\ Cases_on `float_is_zero y` 2939 >- ( 2940 `r = 0` by (pop_assum mp_tac \\ simp [float_is_zero_def]) 2941 \\ qpat_x_assum `float_is_zero y` mp_tac 2942 \\ rw [float_is_zero] 2943 \\ fs [ulp_def] 2944 \\ prove_tac [realLib.REAL_ARITH ``~(x < b /\ b <= x: real)``, 2945 realLib.REAL_ARITH ``2 * abs (-x) <= u ==> abs x <= u``] 2946 ) 2947 \\ lrw [float_round_def] 2948 \\ metis_tac [zero_properties, round_roundTowardZero, round_roundTiesToEven 2949 (*, round_roundTowardPositive, round_roundTowardNegative *)] 2950 2951 2952val float_round_roundTowardZero = Q.store_thm( 2953 "float_round_roundTowardZero", 2954 `!b y: ('t, 'w) float x r. 2955 (float_value y = Float r) /\ 2956 abs (x - r) < ULP (y.Exponent, (:'t)) /\ abs r <= abs x /\ 2957 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2958 (float_round roundTowardZero b x = y)`, 2959 tac 2960 ) 2961 2962val float_round_roundTiesToEven = Q.store_thm("float_round_roundTiesToEven", 2963 `!b y: ('t, 'w) float x r. 2964 (float_value y = Float r) /\ 2965 ((y.Significand = 0w) /\ y.Exponent <> 1w ==> abs r <= abs x) /\ 2966 2 * abs (r - x) <= ULP (y.Exponent, (:'t)) /\ 2967 ((2 * abs (r - x) = ULP (y.Exponent, (:'t))) ==> 2968 ~word_lsb (y.Significand)) /\ 2969 ulp (:'t # 'w) < abs x /\ abs x < threshold (:'t # 'w) ==> 2970 (float_round roundTiesToEven b x = y)`, 2971 tac 2972 ) 2973 2974val float_round_roundTowardPositive = Q.store_thm( 2975 "float_round_roundTowardPositive", 2976 `!b y: ('t, 'w) float x r. 2977 (float_value y = Float r) /\ 2978 abs (x - r) < ulp (:'t # 'w) /\ r >= x /\ 2979 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2980 (float_round roundTowardPositive b x = y)`, 2981 tac) 2982 2983val float_round_roundTowardNegative = Q.store_thm( 2984 "float_round_roundTowardNegative", 2985 `!b y: ('t, 'w) float x r. 2986 (float_value y = Float r) /\ 2987 abs (x - r) < ulp (:'t # 'w) /\ r <= x /\ 2988 ulp (:'t # 'w) <= abs x /\ abs x <= largest (:'t # 'w) ==> 2989 (float_round roundTowardNegative b x = y)`, 2990 tac) 2991 2992*) 2993 2994(* ------------------------------------------------------------------------ 2995 Rounding to +/- 0 2996 ------------------------------------------------------------------------ *) 2997 2998val round_roundTowardZero_is_zero = Q.store_thm("round_roundTowardZero_is_zero", 2999 `!x. abs x < ulp (:'t # 'w) ==> 3000 (round roundTowardZero x = float_plus_zero (:'t # 'w)) \/ 3001 (round roundTowardZero x = float_minus_zero (:'t # 'w))`, 3002 REPEAT strip_tac 3003 \\ qabbrev_tac `r: ('t, 'w) float = round roundTowardZero x` 3004 \\ pop_assum (mp_tac o SYM o REWRITE_RULE [markerTheory.Abbrev_def]) 3005 \\ simp [round_def, lt_ulp_not_infinity0, 3006 closest_such_def, closest_def, is_closest_def] 3007 \\ SELECT_ELIM_TAC 3008 \\ rw [] 3009 >| [ 3010 qexists_tac `float_plus_zero (:'t # 'w)` 3011 \\ simp [zero_properties, zero_to_real, realTheory.ABS_POS, 3012 realTheory.ABS_NEG] 3013 \\ REPEAT strip_tac 3014 \\ imp_res_tac realTheory.REAL_LET_TRANS 3015 \\ imp_res_tac less_than_ulp 3016 \\ Cases_on `b` 3017 \\ lfs [float_to_real_def, realTheory.ABS_NEG], 3018 (* -- *) 3019 imp_res_tac realTheory.REAL_LET_TRANS 3020 \\ imp_res_tac less_than_ulp 3021 \\ Cases_on `r` 3022 \\ lfs [float_plus_zero_def, float_minus_zero_def, float_negate_def, 3023 float_component_equality] 3024 \\ wordsLib.Cases_on_word_value `c` 3025 \\ simp [] 3026 ]) 3027 3028val float_to_real_min_pos = Q.prove( 3029 `!r: ('t, 'w) float. 3030 (abs (float_to_real r) = ulp (:'t # 'w)) = 3031 r IN {float_plus_min (:'t # 'w); 3032 float_negate (float_plus_min (:'t # 'w))}`, 3033 rw [float_plus_min_def, float_negate_def, ulp_def, ULP_def, 3034 float_to_real_def, float_component_equality, abs_float_value, 3035 abs_significand, realTheory.ABS_MUL, realTheory.ABS_DIV, 3036 realTheory.ABS_N, gt0_abs] 3037 >| [ 3038 wordsLib.Cases_on_word_value `r.Sign` 3039 \\ Cases_on `r.Significand = 1w` 3040 \\ simp [realTheory.mult_rat, realTheory.POW_ADD, 3041 div_twopow 3042 |> Q.SPEC `m + n` 3043 |> REWRITE_RULE [realTheory.POW_ADD] 3044 |> Drule.GEN_ALL] 3045 \\ Cases_on `r.Significand` 3046 \\ fs [], 3047 simp [realTheory.REAL_EQ_RDIV_EQ] 3048 \\ simp [realTheory.POW_ADD, GSYM realTheory.REAL_LDISTRIB, 3049 cancel_rwts, cancel_rwt] 3050 \\ match_mp_tac (realLib.REAL_ARITH ``2r < a * b ==> b * a <> 2``) 3051 \\ match_mp_tac ge2d 3052 \\ simp [realTheory.REAL_OF_NUM_POW, pow_ge2, exp_ge2, 3053 DECIDE ``2n <= a ==> 2 <= b + a``, 3054 fcpTheory.DIMINDEX_GE_1 ] 3055 ]) 3056 3057val compare_with_zero_tac = 3058 qpat_x_assum `!b. float_is_finite b ==> p` 3059 (fn th => 3060 assume_tac 3061 (SIMP_RULE (srw_ss()) 3062 [realTheory.ABS_NEG, zero_to_real, zero_properties] 3063 (Q.SPEC `float_plus_zero (:'t # 'w)` th)) 3064 \\ assume_tac th) 3065 3066Theorem half_ulp[local]: 3067 !x r: ('t, 'w) float. 3068 (2 * abs x = ulp (:'t # 'w)) /\ 3069 (!b: ('t, 'w) float. 3070 float_is_finite b ==> 3071 abs (float_to_real r - x) <= abs (float_to_real b - x)) ==> 3072 float_is_zero r \/ 3073 r IN {float_plus_min (:'t # 'w); 3074 float_negate (float_plus_min (:'t # 'w))} 3075Proof 3076 REPEAT strip_tac 3077 \\ Cases_on `float_is_zero r` 3078 \\ simp [] 3079 \\ compare_with_zero_tac 3080 \\ `abs (float_to_real r) = ulp (:'t # 'w)` 3081 by metis_tac 3082 [ulp_lt_float_to_real, 3083 realLib.REAL_ARITH 3084 ``(2 * abs x = u) /\ u <= abs r /\ abs (r - x) <= abs x ==> 3085 (abs r = u)``] 3086 \\ fs [float_to_real_min_pos] 3087QED 3088 3089Theorem min_pos_odd[local]: 3090 !r: ('t, 'w) float. 3091 r IN {float_plus_min (:'t # 'w); 3092 float_negate (float_plus_min (:'t # 'w))} ==> 3093 word_lsb r.Significand 3094Proof rw [float_plus_min_def, float_negate_def] \\ simp [] 3095QED 3096 3097val round_roundTiesToEven_is_zero = Q.store_thm("round_roundTiesToEven_is_zero", 3098 `!x. 2 * abs x <= ulp (:'t # 'w) ==> 3099 (round roundTiesToEven x = float_plus_zero (:'t # 'w)) \/ 3100 (round roundTiesToEven x = float_minus_zero (:'t # 'w))`, 3101 REPEAT strip_tac 3102 \\ qabbrev_tac `r: ('t, 'w) float = round roundTiesToEven x` 3103 \\ pop_assum (mp_tac o SYM o REWRITE_RULE [markerTheory.Abbrev_def]) 3104 \\ simp [round_def, lt_ulp_not_infinity1, pred_setTheory.SPECIFICATION, 3105 closest_such_def, closest_def, is_closest_def] 3106 \\ SELECT_ELIM_TAC 3107 \\ rw [] 3108 >| [ 3109 qexists_tac `float_plus_zero (:'t # 'w)` 3110 \\ simp [zero_properties, zero_to_real, realTheory.ABS_POS, 3111 realTheory.ABS_NEG] 3112 \\ rw [float_plus_zero_def] 3113 \\ Cases_on `float_is_zero b` 3114 \\ rsimp [float_is_zero_to_real_imp] 3115 \\ metis_tac 3116 [ULP_lt_float_to_real, ulp_lt_ULP, realTheory.REAL_LE_TRANS, 3117 realLib.REAL_ARITH ``2 * abs x <= abs c ==> abs x <= abs (c - x)``], 3118 (* -- *) 3119 Cases_on `float_is_zero r` 3120 >- fs [float_sets] 3121 \\ Cases_on `2 * abs x < ulp (:'t # 'w)` 3122 >| [ 3123 imp_res_tac ulp_lt_float_to_real 3124 \\ compare_with_zero_tac 3125 \\ metis_tac 3126 [realLib.REAL_ARITH 3127 ``~(2 * abs x < u /\ u <= abs r /\ abs (r - x) <= abs x)``], 3128 (* -- *) 3129 imp_res_tac 3130 (realLib.REAL_ARITH ``a <= b /\ ~(a < b) ==> (a = b: real)``) 3131 \\ imp_res_tac half_ulp 3132 \\ imp_res_tac min_pos_odd 3133 \\ compare_with_zero_tac 3134 \\ fs [] 3135 \\ qpat_x_assum `!a. q \/ t` 3136 (qspec_then `float_plus_zero (:'t # 'w)` strip_assume_tac) 3137 \\ rfs [realTheory.ABS_NEG, zero_properties, zero_to_real, 3138 float_components, GSYM ulp, GSYM neg_ulp] 3139 \\ qpat_x_assum `!b. p` (qspec_then `b` imp_res_tac) 3140 \\ metis_tac 3141 [realLib.REAL_ARITH 3142 ``~((2 * abs x = u) /\ abs (u - x) <= abs x /\ 3143 ~(abs x <= abs (b - x)) /\ abs (u - x) <= abs (b - x))``, 3144 realLib.REAL_ARITH 3145 ``~((2 * abs x = u) /\ abs (-u - x) <= abs x /\ 3146 ~(abs x <= abs (b - x)) /\ abs (-u - x) <= abs (b - x))``] 3147 ] 3148 ]) 3149 3150val tac = 3151 lrw [float_round_def] 3152 \\ metis_tac [round_roundTowardZero_is_zero, round_roundTiesToEven_is_zero, 3153 zero_properties] 3154 3155val round_roundTowardZero_is_minus_zero = Q.store_thm( 3156 "round_roundTowardZero_is_minus_zero", 3157 `!x. abs x < ulp (:'t # 'w) ==> 3158 (float_round roundTowardZero T x = float_minus_zero (:'t # 'w))`, 3159 tac 3160 ) 3161 3162val round_roundTowardZero_is_plus_zero = Q.store_thm( 3163 "round_roundTowardZero_is_plus_zero", 3164 `!x. abs x < ulp (:'t # 'w) ==> 3165 (float_round roundTowardZero F x = float_plus_zero (:'t # 'w))`, 3166 tac 3167 ) 3168 3169val round_roundTiesToEven_is_minus_zero = Q.store_thm( 3170 "round_roundTiesToEven_is_minus_zero", 3171 `!x. 2 * abs x <= ulp (:'t # 'w) ==> 3172 (float_round roundTiesToEven T x = float_minus_zero (:'t # 'w))`, 3173 tac 3174 ) 3175 3176val round_roundTiesToEven_is_plus_zero = Q.store_thm( 3177 "round_roundTiesToEven_is_plus_zero", 3178 `!x. 2 * abs x <= ulp (:'t # 'w) ==> 3179 (float_round roundTiesToEven F x = float_plus_zero (:'t # 'w))`, 3180 tac 3181 ) 3182 3183(* ------------------------------------------------------------------------ 3184 Rounding to limits 3185 ------------------------------------------------------------------------ *) 3186 3187Theorem largest_is_positive[simp]: 3188 0 <= largest (:'t # 'w) 3189Proof 3190 simp [largest_def, realTheory.REAL_LE_MUL, realTheory.REAL_LE_DIV, 3191 realTheory.REAL_SUB_LE, realTheory.POW_2_LE1, 3192 realTheory.REAL_INV_1OVER, realTheory.REAL_LE_LDIV_EQ, 3193 realLib.REAL_ARITH ``1r <= n ==> 1 <= 2 * n``] 3194QED 3195 3196Theorem threshold_is_positive[simp]: 3197 0 < threshold (:'t # 'w) 3198Proof 3199 simp [threshold_def, realTheory.REAL_LT_MUL, realTheory.REAL_LT_DIV, 3200 realTheory.REAL_SUB_LT, realTheory.POW_2_LE1, 3201 realTheory.REAL_INV_1OVER, realTheory.REAL_LT_LDIV_EQ, realTheory.pow, 3202 realLib.REAL_ARITH ``1r <= n ==> 1 < 2 * (2 * n)``] 3203QED 3204 3205val tac = 3206 rrw [round_def] 3207 \\ rlfs [largest_is_positive, 3208 realLib.REAL_ARITH ``0 <= l /\ l < x ==> ~(x < -l: real)``] 3209 \\ metis_tac [threshold_is_positive, largest_is_positive, 3210 realLib.REAL_ARITH ���(0r < i /\ x <= -i ==> ~(i <= x)) /\ 3211 (0r <= i /\ x < -i ==> ~(i < x))���] 3212 3213val round_roundTiesToEven_plus_infinity = Q.store_thm( 3214 "round_roundTiesToEven_plus_infinity", 3215 `!y: ('t, 'w) float x. 3216 threshold (:'t # 'w) <= x ==> 3217 (round roundTiesToEven x = float_plus_infinity (:'t # 'w))`, 3218 tac 3219 ) 3220 3221val round_roundTiesToEven_minus_infinity = Q.store_thm( 3222 "round_roundTiesToEven_minus_infinity", 3223 `!y: ('t, 'w) float x. 3224 x <= -threshold (:'t # 'w) ==> 3225 (round roundTiesToEven x = float_minus_infinity (:'t # 'w))`, 3226 tac 3227 ) 3228 3229Theorem round_roundTowardZero_top: 3230 !y: ('t, 'w) float x. 3231 largest (:'t # 'w) < x ==> (round roundTowardZero x = float_top (:'t # 'w)) 3232Proof tac 3233QED 3234 3235val round_roundTowardZero_bottom = Q.store_thm("round_roundTowardZero_bottom", 3236 `!y: ('t, 'w) float x. 3237 x < -largest (:'t # 'w) ==> 3238 (round roundTowardZero x = float_bottom (:'t # 'w))`, 3239 tac 3240 ) 3241 3242val round_roundTowardPositive_plus_infinity = Q.store_thm( 3243 "round_roundTowardPositive_plus_infinity", 3244 `!y: ('t, 'w) float x. 3245 largest (:'t # 'w) < x ==> 3246 (round roundTowardPositive x = float_plus_infinity (:'t # 'w))`, 3247 tac 3248 ) 3249 3250val round_roundTowardPositive_bottom = Q.store_thm( 3251 "round_roundTowardPositive_bottom", 3252 `!y: ('t, 'w) float x. 3253 x < -largest (:'t # 'w) ==> 3254 (round roundTowardPositive x = float_bottom (:'t # 'w))`, 3255 tac 3256 ) 3257 3258val round_roundTowardNegative_top = Q.store_thm( 3259 "round_roundTowardNegative_top", 3260 `!y: ('t, 'w) float x. 3261 largest (:'t # 'w) < x ==> 3262 (round roundTowardNegative x = float_top (:'t # 'w))`, 3263 tac 3264 ) 3265 3266Theorem round_roundTowardNegative_minus_infinity: 3267 !y: ('t, 'w) float x. 3268 x < -largest (:'t # 'w) ==> 3269 (round roundTowardNegative x = float_minus_infinity (:'t # 'w)) 3270Proof tac 3271QED 3272 3273val tac = 3274 lrw [float_round_def, round_roundTowardZero_top, 3275 round_roundTowardZero_bottom, round_roundTowardPositive_plus_infinity, 3276 round_roundTowardPositive_bottom, round_roundTowardNegative_top, 3277 round_roundTowardNegative_minus_infinity, 3278 top_properties, bottom_properties, infinity_properties] 3279 3280val float_round_roundTowardZero_top = Q.store_thm( 3281 "float_round_roundTowardZero_top", 3282 `!b y: ('t, 'w) float x. 3283 largest (:'t # 'w) < x ==> 3284 (float_round roundTowardZero b x = float_top (:'t # 'w))`, 3285 tac 3286 ) 3287 3288val float_round_roundTowardZero_bottom = Q.store_thm( 3289 "float_round_roundTowardZero_bottom", 3290 `!b y: ('t, 'w) float x. 3291 x < -largest (:'t # 'w) ==> 3292 (float_round roundTowardZero b x = float_bottom (:'t # 'w))`, 3293 tac 3294 ) 3295 3296val float_round_roundTowardPositive_plus_infinity = Q.store_thm( 3297 "float_round_roundTowardPositive_plus_infinity", 3298 `!b y: ('t, 'w) float x. 3299 largest (:'t # 'w) < x ==> 3300 (float_round roundTowardPositive b x = float_plus_infinity (:'t # 'w))`, 3301 tac 3302 ) 3303 3304val float_round_roundTowardPositive_bottom = Q.store_thm( 3305 "float_round_roundTowardPositive_bottom", 3306 `!b y: ('t, 'w) float x. 3307 x < -largest (:'t # 'w) ==> 3308 (float_round roundTowardPositive b x = float_bottom (:'t # 'w))`, 3309 tac 3310 ) 3311 3312val float_round_roundTowardNegative_top = Q.store_thm( 3313 "float_round_roundTowardNegative_top", 3314 `!b y: ('t, 'w) float x. 3315 largest (:'t # 'w) < x ==> 3316 (float_round roundTowardNegative b x = float_top (:'t # 'w))`, 3317 tac 3318 ) 3319 3320val float_round_roundTowardNegative_minus_infinity = Q.store_thm( 3321 "float_round_roundTowardNegative_minus_infinity", 3322 `!b y: ('t, 'w) float x. 3323 x < -largest (:'t # 'w) ==> 3324 (float_round roundTowardNegative b x = float_minus_infinity (:'t # 'w))`, 3325 tac 3326 ) 3327 3328(* ------------------------------------------------------------------------ 3329 Theorem support for evaluation 3330 ------------------------------------------------------------------------ *) 3331 3332val float_minus_zero = Q.store_thm("float_minus_zero", 3333 `float_minus_zero (:'t # 'w) = 3334 <| Sign := 1w; Exponent := 0w; Significand := 0w |>`, 3335 simp [float_minus_zero_def, float_plus_zero_def, float_negate_def] 3336 ) 3337 3338val float_minus_infinity = Q.store_thm("float_minus_infinity", 3339 `float_minus_infinity (:'t # 'w) = 3340 <| Sign := 1w; Exponent := UINT_MAXw; Significand := 0w |>`, 3341 simp [float_minus_infinity_def, float_plus_infinity_def, float_negate_def] 3342 ) 3343 3344val float_round_non_zero = Q.store_thm("float_round_non_zero", 3345 `!mode toneg r s e f. 3346 (round mode r = <| Sign := s; Exponent := e; Significand := f |>) /\ 3347 (e <> 0w \/ f <> 0w) ==> 3348 (float_round mode toneg r = 3349 <| Sign := s; Exponent := e; Significand := f |>)`, 3350 lrw [float_round_def, float_is_zero] 3351 ) 3352 3353val float_round_plus_infinity = Q.store_thm("float_round_plus_infinity", 3354 `!mode toneg r. 3355 (round mode r = float_plus_infinity (:'t # 'w)) ==> 3356 (float_round mode toneg r = float_plus_infinity (:'t # 'w))`, 3357 lrw [float_round_def, infinity_properties] 3358 ) 3359 3360val float_round_minus_infinity = Q.store_thm("float_round_minus_infinity", 3361 `!mode toneg r. 3362 (round mode r = float_minus_infinity (:'t # 'w)) ==> 3363 (float_round mode toneg r = float_minus_infinity (:'t # 'w))`, 3364 lrw [float_round_def, infinity_properties] 3365 ) 3366 3367val float_round_top = Q.store_thm("float_round_top", 3368 `!mode toneg r. 3369 (round mode r = float_top (:'t # 'w)) ==> 3370 (float_round mode toneg r = float_top (:'t # 'w))`, 3371 lrw [float_round_def, top_properties] 3372 ) 3373 3374val float_round_bottom = Q.store_thm("float_round_bottom", 3375 `!mode toneg r. 3376 (round mode r = float_bottom (:'t # 'w)) ==> 3377 (float_round mode toneg r = float_bottom (:'t # 'w))`, 3378 lrw [float_round_def, bottom_properties] 3379 ) 3380 3381fun tac thms = 3382 rrw ([largest_def, threshold_def, float_to_real_def, wordsTheory.dimword_def, 3383 GSYM realTheory.REAL_NEG_MINUS1, realTheory.REAL_OF_NUM_POW, 3384 wordsLib.WORD_DECIDE ``x <> 1w ==> (x = 0w: word1)``] @ thms) 3385 3386val float_to_real = Q.store_thm("float_to_real", 3387 `!s e:'w word f:'t word. 3388 float_to_real <| Sign := s; Exponent := e; Significand := f |> = 3389 let r = if e = 0w 3390 then 2r / &(2 EXP INT_MAX (:'w)) * (&w2n f / &dimword (:'t)) 3391 else &(2 EXP (w2n e)) / &(2 EXP INT_MAX (:'w)) * 3392 (1r + &w2n f / &dimword (:'t)) 3393 in 3394 if s = 1w then -r else r`, 3395 tac [] 3396 ) 3397 3398val largest = Q.store_thm("largest", 3399 `largest (:'t # 'w) = 3400 &(2 EXP (UINT_MAX (:'w) - 1)) * (2 - 1 / &dimword (:'t)) / 3401 &(2 EXP INT_MAX (:'w))`, 3402 tac [realTheory.REAL_INV_1OVER, realTheory.mult_ratl] 3403 ) 3404 3405val threshold = Q.store_thm("threshold", 3406 `threshold (:'t # 'w) = 3407 &(2 EXP (UINT_MAX (:'w) - 1)) * (2 - 1 / &(2 * dimword (:'t))) / 3408 &(2 EXP INT_MAX (:'w))`, 3409 tac [realTheory.REAL_INV_1OVER, realTheory.mult_ratl, arithmeticTheory.EXP] 3410 ) 3411 3412val largest_top_lem = Q.prove( 3413 `w2n (n2w (UINT_MAX (:'w)) + -1w : 'w word) = UINT_MAX (:'w) - 1`, 3414 simp_tac arith_ss 3415 [wordsTheory.WORD_LITERAL_ADD 3416 |> CONJUNCT2 3417 |> Q.SPECL [`UINT_MAX (:'w)`, `1`] 3418 |> SIMP_RULE std_ss [wordsTheory.ZERO_LT_UINT_MAX, 3419 DECIDE ``0n < x ==> 1 <= x``], 3420 wordsTheory.w2n_n2w, wordsTheory.BOUND_ORDER, 3421 DECIDE ``a < b ==> (a - 1n < b)``] 3422 ) 3423 3424val largest_top_lem2 = Q.prove( 3425 `&UINT_MAX (:'t) + 1 = &dimword (:'t) : real`, 3426 simp [wordsTheory.UINT_MAX_def, DECIDE ``1n < n ==> (n - 1 + 1 = n)``]) 3427 3428val largest_is_top = Q.store_thm("largest_is_top", 3429 `1 < dimindex(:'w) ==> 3430 (largest (:'t # 'w) = float_to_real (float_top (:'t # 'w)))`, 3431 strip_tac 3432 \\ `dimword(:'w) <> 2` 3433 by fs [wordsTheory.dimword_def, 3434 arithmeticTheory.EXP_BASE_INJECTIVE 3435 |> Q.SPEC `2` 3436 |> REWRITE_RULE [DECIDE ``1n < 2``] 3437 |> Q.SPECL [`n`, `1`] 3438 |> REWRITE_RULE [arithmeticTheory.EXP_1]] 3439 \\ `2 < dimword(:'w)` by simp [DECIDE ``1 < n /\ n <> 2 ==> 2n < n``] 3440 \\ `UINT_MAXw - 1w <> 0w : 'w word` by simp [] 3441 \\ asm_simp_tac std_ss [largest, float_top_def, float_to_real] 3442 \\ simp_tac std_ss [wordsTheory.word_T_def] 3443 \\ simp [realTheory.REAL_EQ_LDIV_EQ, DECIDE ``0n < n ==> n <> 0``, 3444 realTheory.REAL_SUB_LDISTRIB, realTheory.REAL_ADD_LDISTRIB, 3445 realTheory.REAL_EQ_SUB_RADD, realTheory.REAL_DIV_REFL, 3446 realTheory.mult_ratr, realTheory.mult_ratl, wordsTheory.BOUND_ORDER, 3447 ONCE_REWRITE_RULE [realTheory.REAL_MUL_COMM] mul_cancel, 3448 largest_top_lem] 3449 \\ simp_tac std_ss 3450 [GSYM realTheory.REAL_ADD_ASSOC, realTheory.REAL_DIV_ADD, 3451 GSYM realTheory.REAL_MUL, largest_top_lem2, 3452 mul_cancel |> Q.SPECL [`a`, `&(n : num)`] |> SIMP_RULE (srw_ss()) [], 3453 wordsTheory.ZERO_LT_dimword, DECIDE ``0 < n ==> n <> 0n``, 3454 REAL_ARITH ``a * b + b = (a + 1r) * b``, realTheory.REAL_DOUBLE] 3455 ) 3456 3457Theorem largest_lt_threshold: 3458 largest (:'t # 'w) < threshold (:'t # 'w) 3459Proof 3460 rw [largest, threshold, realTheory.REAL_LT_RDIV, realTheory.REAL_LT_LMUL, 3461 realLib.REAL_ARITH ``a - b < a - c = c < b : real``, 3462 realTheory.REAL_LT_RDIV_EQ, realTheory.REAL_LT_LDIV_EQ, 3463 realTheory.mult_ratl] >> 3464 fs[wordsTheory.dimword_def] 3465QED 3466 3467val float_tests = Q.store_thm("float_tests", 3468 `(!s e f. 3469 float_is_nan <| Sign := s; Exponent := e; Significand := f |> = 3470 (e = -1w) /\ (f <> 0w)) /\ 3471 (!s e f. 3472 float_is_signalling <| Sign := s; Exponent := e; Significand := f |> = 3473 (e = -1w) /\ ~word_msb f /\ (f <> 0w)) /\ 3474 (!s e f. 3475 float_is_infinite <| Sign := s; Exponent := e; Significand := f |> = 3476 (e = -1w) /\ (f = 0w)) /\ 3477 (!s e f. 3478 float_is_normal <| Sign := s; Exponent := e; Significand := f |> = 3479 (e <> 0w) /\ (e <> -1w)) /\ 3480 (!s e f. 3481 float_is_subnormal <| Sign := s; Exponent := e; Significand := f |> = 3482 (e = 0w) /\ (f <> 0w)) /\ 3483 (!s e f. 3484 float_is_zero <| Sign := s; Exponent := e; Significand := f |> = 3485 (e = 0w) /\ (f = 0w)) /\ 3486 (!s e f. 3487 float_is_finite <| Sign := s; Exponent := e; Significand := f |> = 3488 (e <> -1w))`, 3489 rw [float_is_nan_def, float_is_signalling_def, float_is_infinite_def, 3490 float_is_finite_def, float_is_normal_def, float_is_subnormal_def, 3491 float_value_def] 3492 \\ rw [float_sets, float_minus_zero_def, float_plus_zero_def, 3493 float_is_finite_def, float_negate_def] 3494 \\ wordsLib.Cases_on_word_value `s` 3495 \\ simp [] 3496 ) 3497 3498val float_infinity_negate_abs = Q.store_thm("float_infinity_negate_abs", 3499 `(float_negate (float_plus_infinity (:'t # 'w)) = 3500 float_minus_infinity (:'t # 'w)) /\ 3501 (float_negate (float_minus_infinity (:'t # 'w)) = 3502 float_plus_infinity (:'t # 'w)) /\ 3503 (float_abs (float_plus_infinity (:'t # 'w)) = 3504 float_plus_infinity (:'t # 'w)) /\ 3505 (float_abs (float_minus_infinity (:'t # 'w)) = 3506 float_plus_infinity (:'t # 'w))`, 3507 rw [float_plus_infinity_def, float_minus_infinity_def, 3508 float_negate_def, float_abs_def] 3509 ) 3510 3511(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 3512 3513val float_round_to_integral_compute = Q.store_thm( 3514 "float_round_to_integral_compute", 3515 `(!m. float_round_to_integral m (float_minus_infinity (:'t # 'w)) = 3516 float_minus_infinity (:'t # 'w)) /\ 3517 (!m. float_round_to_integral m (float_plus_infinity (:'t # 'w)) = 3518 float_plus_infinity (:'t # 'w)) /\ 3519 (!m fp_op. 3520 float_round_to_integral m (float_some_qnan fp_op) = 3521 float_some_qnan fp_op)`, 3522 simp [float_round_to_integral_def, float_values] 3523 ) 3524 3525(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 3526 3527val float_add_compute = Q.store_thm("float_add_compute", 3528 `(!mode x fp_op. 3529 float_add mode (float_some_qnan fp_op) x = 3530 (check_for_signalling [x], 3531 float_some_qnan (FP_Add mode (float_some_qnan fp_op) x))) 3532 /\ 3533 (!mode x fp_op. 3534 float_add mode x (float_some_qnan fp_op) = 3535 (check_for_signalling [x], 3536 float_some_qnan (FP_Add mode x (float_some_qnan fp_op)))) 3537 /\ 3538 (!mode. 3539 float_add mode (float_minus_infinity (:'t # 'w)) 3540 (float_minus_infinity (:'t # 'w)) = 3541 (clear_flags, float_minus_infinity (:'t # 'w))) /\ 3542 (!mode. 3543 float_add mode (float_minus_infinity (:'t # 'w)) 3544 (float_plus_infinity (:'t # 'w)) = 3545 (invalidop_flags, 3546 float_some_qnan (FP_Add mode (float_minus_infinity (:'t # 'w)) 3547 (float_plus_infinity (:'t # 'w))))) /\ 3548 (!mode. 3549 float_add mode (float_plus_infinity (:'t # 'w)) 3550 (float_plus_infinity (:'t # 'w)) = 3551 (clear_flags, float_plus_infinity (:'t # 'w))) /\ 3552 (!mode. 3553 float_add mode (float_plus_infinity (:'t # 'w)) 3554 (float_minus_infinity (:'t # 'w)) = 3555 (invalidop_flags, 3556 float_some_qnan (FP_Add mode (float_plus_infinity (:'t # 'w)) 3557 (float_minus_infinity (:'t # 'w))))) 3558 `, 3559 simp [float_add_def, float_values, float_components, some_nan_properties, 3560 check_for_signalling_def] 3561 \\ strip_tac 3562 \\ strip_tac 3563 \\ Cases_on `float_value x` 3564 \\ simp [float_is_signalling_def, float_is_nan_def] 3565 ) 3566 3567val float_add_nan = Q.store_thm("float_add_nan", 3568 `!mode x y. 3569 (float_value x = NaN) \/ (float_value y = NaN) ==> 3570 (float_add mode x y = 3571 (check_for_signalling [x; y], float_some_qnan (FP_Add mode x y)))`, 3572 NTAC 3 strip_tac 3573 \\ Cases_on `float_value x` 3574 \\ Cases_on `float_value y` 3575 \\ simp [float_add_def, check_for_signalling_def, 3576 float_is_signalling_def, float_is_nan_def] 3577 ) 3578 3579val float_add_finite = Q.store_thm("float_add_finite", 3580 `!mode x y r1 r2. 3581 (float_value x = Float r1) /\ (float_value y = Float r2) ==> 3582 (float_add mode x y = 3583 float_round_with_flags mode 3584 (if (r1 = 0) /\ (r2 = 0) /\ (x.Sign = y.Sign) then 3585 x.Sign = 1w 3586 else mode = roundTowardNegative) (r1 + r2))`, 3587 simp [float_add_def] 3588 ) 3589 3590val float_add_finite_plus_infinity = Q.store_thm( 3591 "float_add_finite_plus_infinity", 3592 `!mode x r. 3593 (float_value x = Float r) ==> 3594 (float_add mode x (float_plus_infinity (:'t # 'w)) = 3595 (clear_flags, float_plus_infinity (:'t # 'w)))`, 3596 simp [float_add_def, float_values] 3597 ) 3598 3599val float_add_plus_infinity_finite = Q.store_thm( 3600 "float_add_plus_infinity_finite", 3601 `!mode x r. 3602 (float_value x = Float r) ==> 3603 (float_add mode (float_plus_infinity (:'t # 'w)) x = 3604 (clear_flags, float_plus_infinity (:'t # 'w)))`, 3605 simp [float_add_def, float_values] 3606 ) 3607 3608val float_add_finite_minus_infinity = Q.store_thm( 3609 "float_add_finite_minus_infinity", 3610 `!mode x r. 3611 (float_value x = Float r) ==> 3612 (float_add mode x (float_minus_infinity (:'t # 'w)) = 3613 (clear_flags, float_minus_infinity (:'t # 'w)))`, 3614 simp [float_add_def, float_values] 3615 ) 3616 3617val float_add_minus_infinity_finite = Q.store_thm( 3618 "float_add_minus_infinity_finite", 3619 `!mode x r. 3620 (float_value x = Float r) ==> 3621 (float_add mode (float_minus_infinity (:'t # 'w)) x = 3622 (clear_flags, float_minus_infinity (:'t # 'w)))`, 3623 simp [float_add_def, float_values] 3624 ) 3625 3626(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 3627 3628val float_sub_compute = Q.store_thm("float_sub_compute", 3629 `(!mode x fp_op. 3630 float_sub mode (float_some_qnan fp_op) x = 3631 (check_for_signalling [x], 3632 float_some_qnan (FP_Sub mode (float_some_qnan fp_op) x))) /\ 3633 (!mode x fp_op. 3634 float_sub mode x (float_some_qnan fp_op) = 3635 (check_for_signalling [x], 3636 float_some_qnan (FP_Sub mode x (float_some_qnan fp_op)))) /\ 3637 (!mode. 3638 float_sub mode (float_minus_infinity (:'t # 'w)) 3639 (float_minus_infinity (:'t # 'w)) = 3640 (invalidop_flags, 3641 float_some_qnan (FP_Sub mode (float_minus_infinity (:'t # 'w)) 3642 (float_minus_infinity (:'t # 'w))))) /\ 3643 (!mode. 3644 float_sub mode (float_minus_infinity (:'t # 'w)) 3645 (float_plus_infinity (:'t # 'w)) = 3646 (clear_flags, float_minus_infinity (:'t # 'w))) /\ 3647 (!mode. 3648 float_sub mode (float_plus_infinity (:'t # 'w)) 3649 (float_plus_infinity (:'t # 'w)) = 3650 (invalidop_flags, 3651 float_some_qnan (FP_Sub mode (float_plus_infinity (:'t # 'w)) 3652 (float_plus_infinity (:'t # 'w))))) /\ 3653 (!mode. 3654 float_sub mode (float_plus_infinity (:'t # 'w)) 3655 (float_minus_infinity (:'t # 'w)) = 3656 (clear_flags, float_plus_infinity (:'t # 'w))) 3657 `, 3658 simp [float_sub_def, float_values, float_components, some_nan_properties, 3659 check_for_signalling_def] 3660 \\ strip_tac 3661 \\ strip_tac 3662 \\ Cases_on `float_value x` 3663 \\ simp [float_is_signalling_def, float_is_nan_def] 3664 ) 3665 3666val float_sub_nan = Q.store_thm("float_sub_nan", 3667 `!mode x y. 3668 (float_value x = NaN) \/ (float_value y = NaN) ==> 3669 (float_sub mode x y = 3670 (check_for_signalling [x; y], float_some_qnan (FP_Sub mode x y)))`, 3671 NTAC 3 strip_tac 3672 \\ Cases_on `float_value x` 3673 \\ Cases_on `float_value y` 3674 \\ simp [float_sub_def, check_for_signalling_def, 3675 float_is_signalling_def, float_is_nan_def] 3676 ) 3677 3678val float_sub_finite = Q.store_thm("float_sub_finite", 3679 `!mode x y r1 r2. 3680 (float_value x = Float r1) /\ (float_value y = Float r2) ==> 3681 (float_sub mode x y = 3682 float_round_with_flags mode 3683 (if (r1 = 0) /\ (r2 = 0) /\ x.Sign <> y.Sign then 3684 x.Sign = 1w 3685 else mode = roundTowardNegative) (r1 - r2))`, 3686 simp [float_sub_def] 3687 ) 3688 3689val float_sub_finite_plus_infinity = Q.store_thm( 3690 "float_sub_finite_plus_infinity", 3691 `!mode x r. 3692 (float_value x = Float r) ==> 3693 (float_sub mode x (float_plus_infinity (:'t # 'w)) = 3694 (clear_flags, float_minus_infinity (:'t # 'w)))`, 3695 simp [float_sub_def, float_values, float_minus_infinity_def] 3696 ) 3697 3698val float_sub_plus_infinity_finite = Q.store_thm( 3699 "float_sub_plus_infinity_finite", 3700 `!mode x r. 3701 (float_value x = Float r) ==> 3702 (float_sub mode (float_plus_infinity (:'t # 'w)) x = 3703 (clear_flags, float_plus_infinity (:'t # 'w)))`, 3704 simp [float_sub_def, float_values] 3705 ) 3706 3707val float_sub_finite_minus_infinity = Q.store_thm( 3708 "float_sub_finite_minus_infinity", 3709 `!mode x r. 3710 (float_value x = Float r) ==> 3711 (float_sub mode x (float_minus_infinity (:'t # 'w)) = 3712 (clear_flags, float_plus_infinity (:'t # 'w)))`, 3713 simp [float_sub_def, float_values, float_negate_negate, 3714 float_minus_infinity_def] 3715 ) 3716 3717val float_sub_minus_infinity_finite = Q.store_thm( 3718 "float_sub_minus_infinity_finite", 3719 `!mode x r. 3720 (float_value x = Float r) ==> 3721 (float_sub mode (float_minus_infinity (:'t # 'w)) x = 3722 (clear_flags, float_minus_infinity (:'t # 'w)))`, 3723 simp [float_sub_def, float_values] 3724 ) 3725 3726(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 3727 3728val float_mul_compute = Q.store_thm("float_mul_compute", 3729 `(!mode x fp_op. 3730 float_mul mode (float_some_qnan fp_op) x = 3731 (check_for_signalling [x], 3732 float_some_qnan (FP_Mul mode (float_some_qnan fp_op) x))) /\ 3733 (!mode x fp_op. 3734 float_mul mode x (float_some_qnan fp_op) = 3735 (check_for_signalling [x], 3736 float_some_qnan (FP_Mul mode x (float_some_qnan fp_op)))) /\ 3737 (!mode. 3738 float_mul mode (float_minus_infinity (:'t # 'w)) 3739 (float_minus_infinity (:'t # 'w)) = 3740 (clear_flags, float_plus_infinity (:'t # 'w))) /\ 3741 (!mode. 3742 float_mul mode (float_minus_infinity (:'t # 'w)) 3743 (float_plus_infinity (:'t # 'w)) = 3744 (clear_flags, float_minus_infinity (:'t # 'w))) /\ 3745 (!mode. 3746 float_mul mode (float_plus_infinity (:'t # 'w)) 3747 (float_plus_infinity (:'t # 'w)) = 3748 (clear_flags, float_plus_infinity (:'t # 'w))) /\ 3749 (!mode. 3750 float_mul mode (float_plus_infinity (:'t # 'w)) 3751 (float_minus_infinity (:'t # 'w)) = 3752 (clear_flags, float_minus_infinity (:'t # 'w))) 3753 `, 3754 simp [float_mul_def, float_values, float_components, some_nan_properties, 3755 check_for_signalling_def] 3756 \\ strip_tac 3757 \\ strip_tac 3758 \\ Cases_on `float_value x` 3759 \\ simp [float_is_signalling_def, float_is_nan_def] 3760 ) 3761 3762val float_mul_nan = Q.store_thm("float_mul_nan", 3763 `!mode x y. 3764 (float_value x = NaN) \/ (float_value y = NaN) ==> 3765 (float_mul mode x y = 3766 (check_for_signalling [x; y], float_some_qnan (FP_Mul mode x y)))`, 3767 NTAC 3 strip_tac 3768 \\ Cases_on `float_value x` 3769 \\ Cases_on `float_value y` 3770 \\ simp [float_mul_def, check_for_signalling_def, 3771 float_is_signalling_def, float_is_nan_def] 3772 ) 3773 3774val float_mul_finite = Q.store_thm("float_mul_finite", 3775 `!mode x y r1 r2. 3776 (float_value x = Float r1) /\ (float_value y = Float r2) ==> 3777 (float_mul mode x y = 3778 float_round_with_flags mode (x.Sign <> y.Sign) (r1 * r2))`, 3779 simp [float_mul_def] 3780 ) 3781 3782val float_mul_finite_plus_infinity = Q.store_thm( 3783 "float_mul_finite_plus_infinity", 3784 `!mode x r. 3785 (float_value x = Float r) ==> 3786 (float_mul mode x (float_plus_infinity (:'t # 'w)) = 3787 if r = 0 then 3788 (invalidop_flags, 3789 float_some_qnan (FP_Mul mode x (float_plus_infinity (:'t # 'w)))) 3790 else (clear_flags, 3791 if x.Sign = 0w then 3792 float_plus_infinity (:'t # 'w) 3793 else float_minus_infinity (:'t # 'w)))`, 3794 rw [float_mul_def, float_values] 3795 \\ fs [float_plus_infinity_def] 3796 ) 3797 3798val float_mul_plus_infinity_finite = Q.store_thm( 3799 "float_mul_plus_infinity_finite", 3800 `!mode x r. 3801 (float_value x = Float r) ==> 3802 (float_mul mode (float_plus_infinity (:'t # 'w)) x = 3803 if r = 0 then 3804 (invalidop_flags, 3805 float_some_qnan (FP_Mul mode (float_plus_infinity (:'t # 'w)) x)) 3806 else (clear_flags, 3807 if x.Sign = 0w 3808 then float_plus_infinity (:'t # 'w) 3809 else float_minus_infinity (:'t # 'w)))`, 3810 rw [float_mul_def, float_values] 3811 \\ fs [float_plus_infinity_def] 3812 ) 3813 3814val float_mul_finite_minus_infinity = Q.store_thm( 3815 "float_mul_finite_minus_infinity", 3816 `!mode x r. 3817 (float_value x = Float r) ==> 3818 (float_mul mode x (float_minus_infinity (:'t # 'w)) = 3819 if r = 0 then 3820 (invalidop_flags, 3821 float_some_qnan (FP_Mul mode x (float_minus_infinity (:'t # 'w)))) 3822 else (clear_flags, 3823 if x.Sign = 0w 3824 then float_minus_infinity (:'t # 'w) 3825 else float_plus_infinity (:'t # 'w)))`, 3826 rw [float_mul_def, float_values] 3827 \\ fs [float_minus_infinity_def, float_plus_infinity_def, float_negate_def] 3828 \\ metis_tac [sign_inconsistent] 3829 ) 3830 3831val float_mul_minus_infinity_finite = Q.store_thm( 3832 "float_mul_minus_infinity_finite", 3833 `!mode x r. 3834 (float_value x = Float r) ==> 3835 (float_mul mode (float_minus_infinity (:'t # 'w)) x = 3836 if r = 0 then 3837 (invalidop_flags, 3838 float_some_qnan (FP_Mul mode (float_minus_infinity (:'t # 'w)) x)) 3839 else (clear_flags, 3840 if x.Sign = 0w 3841 then float_minus_infinity (:'t # 'w) 3842 else float_plus_infinity (:'t # 'w)))`, 3843 rw [float_mul_def, float_values] 3844 \\ fs [float_minus_infinity_def, float_plus_infinity_def, float_negate_def] 3845 \\ metis_tac [sign_inconsistent] 3846 ) 3847 3848(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *) 3849 3850val float_div_compute = Q.store_thm("float_div_compute", 3851 `(!mode x fp_op. 3852 float_div mode (float_some_qnan fp_op) x = 3853 (check_for_signalling [x], 3854 float_some_qnan (FP_Div mode (float_some_qnan fp_op) x))) /\ 3855 (!mode x fp_op. 3856 float_div mode x (float_some_qnan fp_op) = 3857 (check_for_signalling [x], 3858 float_some_qnan (FP_Div mode x (float_some_qnan fp_op)))) /\ 3859 (!mode. 3860 float_div mode (float_minus_infinity (:'t # 'w)) 3861 (float_minus_infinity (:'t # 'w)) = 3862 (invalidop_flags, 3863 float_some_qnan (FP_Div mode (float_minus_infinity (:'t # 'w)) 3864 (float_minus_infinity (:'t # 'w))))) /\ 3865 (!mode. 3866 float_div mode (float_minus_infinity (:'t # 'w)) 3867 (float_plus_infinity (:'t # 'w)) = 3868 (invalidop_flags, 3869 float_some_qnan (FP_Div mode (float_minus_infinity (:'t # 'w)) 3870 (float_plus_infinity (:'t # 'w))))) /\ 3871 (!mode. 3872 float_div mode (float_plus_infinity (:'t # 'w)) 3873 (float_plus_infinity (:'t # 'w)) = 3874 (invalidop_flags, 3875 float_some_qnan (FP_Div mode (float_plus_infinity (:'t # 'w)) 3876 (float_plus_infinity (:'t # 'w))))) /\ 3877 (!mode. 3878 float_div mode (float_plus_infinity (:'t # 'w)) 3879 (float_minus_infinity (:'t # 'w)) = 3880 (invalidop_flags, 3881 float_some_qnan (FP_Div mode (float_plus_infinity (:'t # 'w)) 3882 (float_minus_infinity (:'t # 'w))))) 3883 `, 3884 simp [float_div_def, float_values, float_components, some_nan_properties, 3885 check_for_signalling_def] 3886 \\ strip_tac 3887 \\ strip_tac 3888 \\ Cases_on `float_value x` 3889 \\ simp [float_is_signalling_def, float_is_nan_def] 3890 ) 3891 3892val float_div_nan = Q.store_thm("float_div_nan", 3893 `!mode x y. 3894 (float_value x = NaN) \/ (float_value y = NaN) ==> 3895 (float_div mode x y = 3896 (check_for_signalling [x; y], float_some_qnan (FP_Div mode x y)))`, 3897 NTAC 3 strip_tac 3898 \\ Cases_on `float_value x` 3899 \\ Cases_on `float_value y` 3900 \\ simp [float_div_def, check_for_signalling_def, 3901 float_is_signalling_def, float_is_nan_def] 3902 ) 3903 3904val float_div_finite = Q.store_thm("float_div_finite", 3905 `!mode x y r1 r2. 3906 (float_value x = Float r1) /\ (float_value y = Float r2) ==> 3907 (float_div mode x y = 3908 if r2 = 0 3909 then if r1 = 0 then 3910 (invalidop_flags, float_some_qnan (FP_Div mode x y)) 3911 else 3912 (dividezero_flags, 3913 if x.Sign = y.Sign then float_plus_infinity (:'t # 'w) 3914 else float_minus_infinity (:'t # 'w)) 3915 else float_round_with_flags mode (x.Sign <> y.Sign) (r1 / r2))`, 3916 simp [float_div_def] 3917 ) 3918 3919val float_div_finite_plus_infinity = Q.store_thm( 3920 "float_div_finite_plus_infinity", 3921 `!mode x r. 3922 (float_value x = Float r) ==> 3923 (float_div mode x (float_plus_infinity (:'t # 'w)) = 3924 (clear_flags, 3925 if x.Sign = 0w then float_plus_zero (:'t # 'w) 3926 else float_minus_zero (:'t # 'w)))`, 3927 rw [float_div_def, float_values] 3928 \\ fs [float_plus_infinity_def] 3929 ) 3930 3931val float_div_plus_infinity_finite = Q.store_thm( 3932 "float_div_plus_infinity_finite", 3933 `!mode x r. 3934 (float_value x = Float r) ==> 3935 (float_div mode (float_plus_infinity (:'t # 'w)) x = 3936 (clear_flags, 3937 if x.Sign = 0w then float_plus_infinity (:'t # 'w) 3938 else float_minus_infinity (:'t # 'w)))`, 3939 rw [float_div_def, float_values] 3940 \\ fs [float_plus_infinity_def] 3941 ) 3942 3943val float_div_finite_minus_infinity = Q.store_thm( 3944 "float_div_finite_minus_infinity", 3945 `!mode x r. 3946 (float_value x = Float r) ==> 3947 (float_div mode x (float_minus_infinity (:'t # 'w)) = 3948 (clear_flags, 3949 if x.Sign = 0w then float_minus_zero (:'t # 'w) 3950 else float_plus_zero (:'t # 'w)))`, 3951 rw [float_div_def, float_values] 3952 \\ fs [float_minus_infinity_def, float_plus_infinity_def, float_negate_def] 3953 \\ metis_tac [sign_inconsistent] 3954 ) 3955 3956val float_div_minus_infinity_finite = Q.store_thm( 3957 "float_div_minus_infinity_finite", 3958 `!mode x r. 3959 (float_value x = Float r) ==> 3960 (float_div mode (float_minus_infinity (:'t # 'w)) x = 3961 (clear_flags, 3962 if x.Sign = 0w then float_minus_infinity (:'t # 'w) 3963 else float_plus_infinity (:'t # 'w)))`, 3964 rw [float_div_def, float_values] 3965 \\ fs [float_minus_infinity_def, float_plus_infinity_def, float_negate_def] 3966 \\ metis_tac [sign_inconsistent] 3967 ) 3968 3969(* ------------------------------------------------------------------------ *) 3970 3971val () = export_theory () 3972