Theory "float"

Parents ieee

Signature

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

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 ∈ 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} × ({y | y < n} × {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} ⊆ {a | is_valid X a}

MATCH_FLOAT_FINITE

|- ∀X. {a | is_finite X a} ⊆ {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)