Theory "float"

Parents ieee word

Signature

Constant	Type
normalizes	:real -> bool
error	:real -> real

Definitions

error_def

|- !x. error x = Val (float (round float_format To_nearest x)) - x

normalizes

|- !x.
     normalizes x =
     inv (2 pow (bias float_format - 1)) <= abs x /\
     abs x < threshold float_format

Theorems

FLOAT_DIV_RELATIVE

|- !a b.
     Finite a /\ Finite b /\ ~Iszero b /\ normalizes (Val a / Val b) ==>
     Finite (a / b) /\
     ?e. abs e <= 1 / 2 pow 24 /\ (Val (a / b) = Val a / Val b * (1 + e))

FLOAT_MUL_RELATIVE

|- !a b.
     Finite a /\ Finite b /\ normalizes (Val a * Val b) ==>
     Finite (a * b) /\
     ?e. abs e <= 1 / 2 pow 24 /\ (Val (a * b) = Val a * Val b * (1 + e))

FLOAT_SUB_RELATIVE

|- !a b.
     Finite a /\ Finite b /\ normalizes (Val a - Val b) ==>
     Finite (a - b) /\
     ?e. abs e <= 1 / 2 pow 24 /\ (Val (a - b) = (Val a - Val b) * (1 + e))

FLOAT_ADD_RELATIVE

|- !a b.
     Finite a /\ Finite b /\ normalizes (Val a + Val b) ==>
     Finite (a + b) /\
     ?e. abs e <= 1 / 2 pow 24 /\ (Val (a + b) = (Val a + Val b) * (1 + e))

Val_FLOAT_ROUND_VALOF

|- !x.
     Val (float (round float_format To_nearest x)) =
     valof float_format (round float_format To_nearest x)

FLOAT_DIV

|- !a b.
     Finite a /\ Finite b /\ ~Iszero b /\
     abs (Val a / Val b) < threshold float_format ==>
     Finite (a / b) /\ (Val (a / b) = Val a / Val b + error (Val a / Val b))

FLOAT_MUL

|- !a b.
     Finite a /\ Finite b /\ abs (Val a * Val b) < threshold float_format ==>
     Finite (a * b) /\ (Val (a * b) = Val a * Val b + error (Val a * Val b))

FLOAT_SUB

|- !a b.
     Finite a /\ Finite b /\ abs (Val a - Val b) < threshold float_format ==>
     Finite (a - b) /\ (Val (a - b) = Val a - Val b + error (Val a - Val b))

REAL_POW_LE_1

|- !n x. 1 <= x ==> 1 <= x pow n

REAL_POW_EQ_0

|- !x n. (x pow n = 0) = (x = 0) /\ ~(n = 0)

REAL_LE_RCANCEL_IMP

|- !x y z. 0 < z /\ x * z <= y * z ==> x <= y

REAL_LT_RCANCEL_IMP

|- !x y z. 0 < z /\ x * z < y * z ==> x < y

VALOF_SCALE_DOWN

|- !s e k f.
     k < e ==>
     (valof float_format (s,e - k,f) =
      inv (2 pow k) * valof float_format (s,e,f))

VALOF_SCALE_UP

|- !s e k f.
     ~(e = 0) ==>
     (valof float_format (s,e + k,f) = 2 pow k * valof float_format (s,e,f))

ERROR_BOUND_LEMMA8

|- !x.
     abs x < inv (2 pow 126) ==>
     ?s e f.
       abs (Val (float (s,e,f)) - x) <= inv (2 pow 150) /\ s < 2 /\
       f < 2 ** 23 /\ ((e = 0) \/ (e = 1) /\ (f = 0))

ERROR_BOUND_LEMMA7

|- !x.
     0 <= x /\ x < inv (2 pow 126) ==>
     ?e f.
       abs (Val (float (0,e,f)) - x) <= inv (2 pow 150) /\ f < 2 ** 23 /\
       ((e = 0) \/ (e = 1) /\ (f = 0))

EXP_LT_0

|- !n x. 0 < x ** n = ~(x = 0) \/ (n = 0)

ERROR_BOUND_LEMMA6

|- !x.
     0 <= x /\ x < inv (2 pow 126) ==>
     ?n.
       n <= 2 ** 23 /\
       abs (x - 2 / 2 pow 127 * & n / 2 pow 23) <= inv (2 pow 150)

REAL_LE_LCANCEL_IMP

|- !x y z. 0 < x /\ x * y <= x * z ==> y <= z

REAL_MUL_AC

|- (m * n = n * m) /\ (m * n * p = m * (n * p)) /\ (m * (n * p) = n * (m * p))

ERROR_BOUND_LEMMA5

|- !x.
     1 <= abs x /\ abs x < 2 ==>
     ?s e f.
       abs (Val (float (s,e,f)) - x) <= inv (2 pow 24) /\ s < 2 /\
       f < 2 ** 23 /\
       ((e = bias float_format) \/ (e = SUC (bias float_format)) /\ (f = 0))

ERROR_BOUND_LEMMA4

|- !x.
     1 <= x /\ x < 2 ==>
     ?e f.
       abs (Val (float (0,e,f)) - x) <= inv (2 pow 24) /\ f < 2 ** 23 /\
       ((e = bias float_format) \/ (e = SUC (bias float_format)) /\ (f = 0))

ERROR_BOUND_LEMMA3

|- !x.
     1 <= x /\ x < 2 ==>
     ?n. n <= 2 ** 23 /\ abs (1 + & n / 2 pow 23 - x) <= inv (2 pow 24)

ERROR_BOUND_LEMMA2

|- !x.
     0 <= x /\ x < 1 ==>
     ?n. n <= 2 ** 23 /\ abs (x - & n / 2 pow 23) <= inv (2 pow 24)

ERROR_BOUND_LEMMA1

|- !x.
     0 <= x /\ x < 1 ==>
     ?n. n < 2 ** 23 /\ & n / 2 pow 23 <= x /\ x < & (SUC n) / 2 pow 23

REAL_OF_NUM_LT

|- !m n. & m < & n = m < n

TWO_EXP_GE_1

|- !n. 1 <= 2 ** n

egtff

|- 8 = 4 + 4

ftt

|- 4 = 2 + 2

tpetfs

|- 2 pow 8 = 256

egt1

|- 1 < 8

temonz

|- ~(2 ** 8 - 1 = 0)

tteettto

|- 23 = 8 + 8 + 2 + 2 + 2 + 1

tptteteesze

|- 2 pow 23 = 8388608

tfflttfs

|- 255 < 256

inv23gt0

|- 0 < inv (2 pow 23)

v23not0

|- ~(2 pow 23 = 0)

v127not0

|- ~(2 pow 127 = 0)

noteteeszegtz

|- 0 < 8388608

lt1eqmul

|- x < 1 = x * 8388608 < 8388608

twogz

|- !n. 0 < 2 pow n

not2eqz

|- ~(2 = 0)

tittfittt

|- 2 * inv (2 pow 24) = inv (2 pow 23)

ttpinv

|- 2 * 2 pow 127 * inv (2 pow 127) = 2

RRRC1

|- 2 * 8388608 <= 2 pow 254 * (2 * 8388608 - 1)

RRRC2

|- 2 pow 103 * (2 pow 24 * 2) - 2 pow 103 <= 2 pow 128

RRRC3

|- 340282356779733661637539395458142568448 <= 2 pow 128

RRRC4

|- 2 pow 128 - 2 pow 103 = 340282356779733661637539395458142568448

RRRC5

|- inv 1 < 2 pow 103 * (2 pow 24 * 2) - 2 pow 103

RRRC6

|- 0 < 2 pow 150

RRRC7

|- 2 pow 254 - 2 pow 229 < 2 pow 254

RRRC8

|- 2 pow 103 * (2 pow 24 * 2) - 2 pow 103 =
   340282356779733661637539395458142568448

RRRC9

|- 2 pow 127 * 2 - 2 pow 104 < 340282356779733661637539395458142568448

RRRC10

|- 1 < 2 pow 254 - 2 pow 229

RRRC11

|- 340282356779733661637539395458142568448 * 2 pow 126 < 2 pow 254

sucminmullt

|- (2 pow SUC 127 - 2 pow 103) * 2 pow 126 < 2 pow 255

SIGN

|- !a. sign a = FST a

EXPONENT

|- !a. exponent a = FST (SND a)

FRACTION

|- !a. fraction a = SND (SND a)

IS_VALID

|- !X a.
     is_valid X a =
     sign a < 2 /\ exponent a < 2 ** expwidth X /\
     fraction a < 2 ** fracwidth X

VALOF

|- !X a.
     valof X a =
     (if exponent a = 0 then
        ~1 pow sign a * (2 / 2 pow bias X) *
        (& (fraction a) / 2 pow fracwidth X)
      else
        ~1 pow sign a * (2 pow exponent a / 2 pow bias X) *
        (1 + & (fraction a) / 2 pow fracwidth X))

IS_VALID_DEFLOAT

|- !a. is_valid float_format (defloat a)

ADD_SUB2

|- !m n. m + n - m = n

REAL_OF_NUM_SUB

|- !m n. m <= n ==> (& n - & m = & (n - m))

IS_FINITE_ALT1

|- !a.
     is_normal float_format a \/ is_denormal float_format a \/
     is_zero float_format a =
     exponent a < 255

IS_FINITE_ALT

|- !a. is_finite float_format a = is_valid float_format a /\ exponent a < 255

IS_FINITE_EXPLICIT

|- !a.
     is_finite float_format a =
     sign a < 2 /\ exponent a < 255 /\ fraction a < 8388608

LT_SUC_LE

|- !m n. m < SUC n = m <= n

FLOAT_CASES

|- !a. Isnan a \/ Infinity a \/ Isnormal a \/ Isdenormal a \/ Iszero a

FLOAT_CASES_FINITE

|- !a. Isnan a \/ Infinity a \/ Finite a

FLOAT_DISTINCT

|- !a.
     ~(Isnan a /\ Infinity a) /\ ~(Isnan a /\ Isnormal a) /\
     ~(Isnan a /\ Isdenormal a) /\ ~(Isnan a /\ Iszero a) /\
     ~(Infinity a /\ Isnormal a) /\ ~(Infinity a /\ Isdenormal a) /\
     ~(Infinity a /\ Iszero a) /\ ~(Isnormal a /\ Isdenormal a) /\
     ~(Isnormal a /\ Iszero a) /\ ~(Isdenormal a /\ Iszero a)

FLOAT_DISTINCT_FINITE

|- !a.
     ~(Isnan a /\ Infinity a) /\ ~(Isnan a /\ Finite a) /\
     ~(Infinity a /\ Finite a)

FLOAT_INFINITIES_SIGNED

|- (sign (defloat Plus_infinity) = 0) /\ (sign (defloat Minus_infinity) = 1)

INFINITY_IS_INFINITY

|- Infinity Plus_infinity /\ Infinity Minus_infinity

ZERO_IS_ZERO

|- Iszero Plus_zero /\ Iszero Minus_zero

INFINITY_NOT_NAN

|- ~Isnan Plus_infinity /\ ~Isnan Minus_infinity

ZERO_NOT_NAN

|- ~Isnan Plus_zero /\ ~Isnan Minus_zero

FLOAT_INFINITIES

|- !a. Infinity a = a == Plus_infinity \/ a == Minus_infinity

FLOAT_INFINITES_DISTINCT

|- !a. ~(a == Plus_infinity /\ a == Minus_infinity)

FLOAT_LT

|- !a b. Finite a /\ Finite b ==> (a < b = Val a < Val b)

FLOAT_GT

|- !a b. Finite a /\ Finite b ==> (a > b = Val a > Val b)

FLOAT_LE

|- !a b. Finite a /\ Finite b ==> (a <= b = Val a <= Val b)

FLOAT_GE

|- !a b. Finite a /\ Finite b ==> (a >= b = Val a >= Val b)

FLOAT_EQ

|- !a b. Finite a /\ Finite b ==> (a == b = (Val a = Val b))

FLOAT_EQ_REFL

|- !a. a == a = ~Isnan a

EXP_GT_ZERO

|- !n. 0 < 2 ** n

IS_VALID_SPECIAL

|- !X.
     is_valid X (minus_infinity X) /\ is_valid X (plus_infinity X) /\
     is_valid X (topfloat X) /\ is_valid X (bottomfloat X) /\
     is_valid X (plus_zero X) /\ is_valid X (minus_zero X)

IS_CLOSEST_EXISTS

|- !v x s. FINITE s ==> ~(s = {}) ==> ?a. is_closest v s x a

CLOSEST_IS_EVERYTHING

|- !v p s x.
     FINITE s ==>
     ~(s = {}) ==>
     is_closest v s x (closest v p s x) /\
     ((?b. is_closest v s x b /\ p b) ==> p (closest v p s x))

CLOSEST_IN_SET

|- !v p x s. FINITE s ==> ~(s = {}) ==> closest v p s x IN s

CLOSEST_IS_CLOSEST

|- !v p x s. FINITE s ==> ~(s = {}) ==> is_closest v s x (closest v p s x)

FLOAT_FIRSTCROSS1

|- !x m n p.
     (?x'.
        (x = (\(x,y,z). (x,y,z)) x') /\ FST x' < m /\ FST (SND x') < n /\
        SND (SND x') < p) ==>
     FST x < m /\ FST (SND x) < n /\ SND (SND x) < p

FLOAT_FIRSTCROSS2

|- !x m n p.
     FST x < m /\ FST (SND x) < n /\ SND (SND x) < p ==>
     ?x'.
       (x = (\(x,y,z). (x,y,z)) x') /\ FST x' < m /\ FST (SND x') < n /\
       SND (SND x') < p

FLOAT_FIRSTCROSS3

|- !x m n p.
     FST x < m /\ FST (SND x) < n /\ SND (SND x) < p =
     ?x'.
       (x = (\(x,y,z). (x,y,z)) x') /\ FST x' < m /\ FST (SND x') < n /\
       SND (SND x') < p

FLOAT_FIRSTCROSS

|- !m n p.
     {a | FST a < m /\ FST (SND a) < n /\ SND (SND a) < p} =
     IMAGE (\(x,y,z). (x,y,z))
       ({x | x < m} CROSS ({y | y < n} CROSS {z | z < p}))

FLOAT_COUNTINDUCT

|- !n. ({x | x < 0} = {}) /\ ({x | x < SUC n} = n INSERT {x | x < n})

FLOAT_FINITECOUNT

|- !n. FINITE {x | x < n}

FINITE_R3

|- !m n p. FINITE {a | FST a < m /\ FST (SND a) < n /\ SND (SND a) < p}

REAL_OF_NUM_POW

|- !x n. & x pow n = & (x ** n)

IS_VALID_FINITE

|- FINITE {a | is_valid X a}

FLOAT_IS_FINITE_SUBSET

|- !X. {a | is_finite X a} SUBSET {a | is_valid X a}

MATCH_FLOAT_FINITE

|- !X.
     {a | is_finite X a} SUBSET {a | is_valid X a} ==>
     FINITE {a | is_finite X a}

IS_FINITE_FINITE

|- !X. FINITE {a | is_finite X a}

IS_VALID_NONEMPTY

|- ~({a | is_valid X a} = {})

IS_FINITE_NONEMPTY

|- ~({a | is_finite X a} = {})

IS_FINITE_CLOSEST

|- !X v p x. is_finite X (closest v p {a | is_finite X a} x)

IS_VALID_CLOSEST

|- !X v p x. is_valid X (closest v p {a | is_finite X a} x)

IS_VALID_ROUND

|- !X x. is_valid X (round X To_nearest x)

DEFLOAT_FLOAT_ROUND

|- !X x.
     defloat (float (round float_format To_nearest x)) =
     round float_format To_nearest x

DEFLOAT_FLOAT_ZEROSIGN_ROUND

|- !x b.
     defloat
       (float (zerosign float_format b (round float_format To_nearest x))) =
     zerosign float_format b (round float_format To_nearest x)

VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND

|- !x b.
     valof float_format
       (defloat
          (float
             (zerosign float_format b (round float_format To_nearest x)))) =
     valof float_format (round float_format To_nearest x)

REAL_ABS_NUM

|- abs (& n) = & n

REAL_ABS_POW

|- !x n. abs (x pow n) = abs x pow n

ISFINITE

|- !a. Finite a = is_finite float_format (defloat a)

REAL_ABS_INV

|- !x. abs (inv x) = inv (abs x)

REAL_ABS_DIV

|- !x y. abs (x / y) = abs x / abs y

REAL_LT_LCANCEL_IMP

|- !x y z. 0 < x /\ x * y < x * z ==> y < z

ERROR_IS_ZERO

|- !a x. Finite a /\ (Val a = x) ==> (error x = 0)

ERROR_AT_WORST_LEMMA

|- !a x.
     abs x < threshold float_format /\ Finite a ==>
     abs (error x) <= abs (Val a - x)

BOUND_AT_WORST_LEMMA

|- !a x.
     abs x < threshold float_format /\ is_finite float_format a ==>
     abs (valof float_format (round float_format To_nearest x) - x) <=
     abs (valof float_format a - x)

VAL_THRESHOLD

|- !a. Finite a ==> abs (Val a) < threshold float_format

FLOAT_THRESHOLD_EXPLICIT

|- threshold float_format = 340282356779733661637539395458142568448

ISFINITE_LEMMA

|- !s e f.
     s < 2 /\ e < 255 /\ f < 2 ** 23 ==>
     Finite (float (s,e,f)) /\ is_valid float_format (s,e,f)

VAL_FINITE

|- !a. Finite a ==> abs (Val a) <= largest float_format

REAL_POW_MONO

|- !m n x. 1 <= x /\ m <= n ==> x pow m <= x pow n

ERROR_BOUND_BIG1

|- !x k.
     2 pow k <= abs x /\ abs x < 2 pow SUC k /\
     abs x < threshold float_format ==>
     ?a. Finite a /\ abs (Val a - x) <= 2 pow k / 2 pow 24

ERROR_BOUND_BIG

|- !k x.
     2 pow k <= abs x /\ abs x < 2 pow SUC k /\
     abs x < threshold float_format ==>
     abs (error x) <= 2 pow k / 2 pow 24

REAL_LE_INV2

|- !x y. 0 < x /\ x <= y ==> inv y <= inv x

ERROR_BOUND_SMALL1

|- !x k.
     inv (2 pow SUC k) <= abs x /\ abs x < inv (2 pow k) /\ k < 126 ==>
     ?a. Finite a /\ abs (Val a - x) <= inv (2 pow SUC k * 2 pow 24)

ERROR_BOUND_SMALL

|- !k x.
     inv (2 pow SUC k) <= abs x /\ abs x < inv (2 pow k) /\ k < 126 ==>
     abs (error x) <= inv (2 pow SUC k * 2 pow 24)

ERROR_BOUND_TINY

|- !x. abs x < inv (2 pow 126) ==> abs (error x) <= inv (2 pow 150)

ERROR_BOUND_NORM_STRONG

|- !x j.
     abs x < threshold float_format /\ abs x < 2 pow SUC j / 2 pow 126 ==>
     abs (error x) <= 2 pow j / 2 pow 150

THRESHOLD_MUL_LT

|- threshold float_format * 2 pow 126 < 2 pow 2 ** 126

THRESHOLD_LT_POW_INV

|- 340282356779733661637539395458142568448 < 2 pow 254 * inv (2 pow 126)

LT_THRESHOLD_LT_POW_INV

|- !x. x < threshold (8,23) ==> x < 2 pow (emax (8,23) - 1) / 2 pow 126

REAL_POS_IN_BINADE

|- !x.
     normalizes x /\ 0 <= x ==>
     ?j.
       j <= emax float_format - 2 /\ 2 pow j / 2 pow 126 <= x /\
       x < 2 pow SUC j / 2 pow 126

REAL_NEG_IN_BINADE

|- !x.
     normalizes x /\ 0 <= ~x ==>
     ?j.
       j <= emax float_format - 2 /\ 2 pow j / 2 pow 126 <= ~x /\
       ~x < 2 pow SUC j / 2 pow 126

REAL_IN_BINADE

|- !x.
     normalizes x ==>
     ?j.
       j <= emax float_format - 2 /\ 2 pow j / 2 pow 126 <= abs x /\
       abs x < 2 pow SUC j / 2 pow 126

ERROR_BOUND_NORM_STRONG_NORMALIZE

|- !x. normalizes x ==> ?j. abs (error x) <= 2 pow j / 2 pow 150

RELATIVE_ERROR_POS

|- !x.
     normalizes x /\ 0 < x ==>
     ?e.
       abs e <= 1 / 2 pow 24 /\
       (Val (float (round float_format To_nearest x)) = x * (1 + e))

RELATIVE_ERROR_NEG

|- !x.
     normalizes x /\ x < 0 ==>
     ?e.
       abs e <= 1 / 2 pow 24 /\
       (Val (float (round float_format To_nearest x)) = x * (1 + e))

RELATIVE_ERROR_ZERO

|- !x.
     normalizes x /\ (x = 0) ==>
     ?e.
       abs e <= 1 / 2 pow 24 /\
       (Val (float (round float_format To_nearest x)) = x * (1 + e))

RELATIVE_ERROR

|- !x.
     normalizes x ==>
     ?e.
       abs e <= 1 / 2 pow 24 /\
       (Val (float (round float_format To_nearest x)) = x * (1 + e))

DEFLOAT_FLOAT_ZEROSIGN_ROUND_FINITE

|- !b x.
     abs x < threshold float_format ==>
     is_finite float_format
       (defloat
          (float (zerosign float_format b (round float_format To_nearest x))))

FLOAT_ADD

|- !a b.
     Finite a /\ Finite b /\ abs (Val a + Val b) < threshold float_format ==>
     Finite (a + b)

FLOAT_SUB_FINITE

|- !a b.
     Finite a /\ Finite b /\ abs (Val a - Val b) < threshold float_format ==>
     Finite (a - b)

FLOAT_MUL_FINITE

|- !a b.
     Finite a /\ Finite b /\ abs (Val a * Val b) < threshold float_format ==>
     Finite (a * b)