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_def

⊢ ∀x. normalizes x ⇔
      (2 pow (bias float_format − 1))⁻¹ ≤ abs x ∧
      abs x < threshold float_format

Theorems

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)

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))

DEFLOAT_FLOAT_ROUND

⊢ ∀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)

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))))

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

ERROR_BOUND_NORM_STRONG_NORMALIZE

⊢ ∀x. normalizes x ⇒ ∃j. abs (error x) ≤ 2 pow j / 2 pow 150

ERROR_IS_ZERO

⊢ ∀a x. Finite a ∧ (Val a = x) ⇒ (error x = 0)

EXPONENT

⊢ ∀a. exponent a = FST (SND a)

FLOAT_ADD

⊢ ∀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_ADD_FINITE

⊢ ∀b a.
    Finite a ∧ Finite b ∧ abs (Val a + Val b) < threshold float_format ⇒
    Finite (a + b)

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))

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_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_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_EQ

⊢ ∀a b. Finite a ∧ Finite b ⇒ (a == b ⇔ (Val a = Val b))

FLOAT_EQ_REFL

⊢ ∀a. a == a ⇔ ¬Isnan a

FLOAT_GE

⊢ ∀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_INFINITES_DISTINCT

⊢ ∀a. ¬(a == Plus_infinity ∧ a == Minus_infinity)

FLOAT_INFINITIES

⊢ ∀a. Infinity a ⇔ a == Plus_infinity ∨ a == Minus_infinity

FLOAT_INFINITIES_SIGNED

⊢ (sign (defloat Plus_infinity) = 0) ∧ (sign (defloat Minus_infinity) = 1)

FLOAT_LARGEST_EXPLICIT

⊢ largest float_format = 340282346638528859811704183484516925440

FLOAT_LE

⊢ ∀a b. Finite a ∧ Finite b ⇒ (a ≤ b ⇔ Val a ≤ Val b)

FLOAT_LT

⊢ ∀a b. Finite a ∧ Finite b ⇒ (a < b ⇔ 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_MUL_FINITE

⊢ ∀b a.
    Finite a ∧ Finite b ∧ abs (Val a * Val b) < threshold float_format ⇒
    Finite (a * b)

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

⊢ ∀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_FINITE

⊢ ∀b a.
    Finite a ∧ Finite b ∧ abs (Val a − Val b) < threshold float_format ⇒
    Finite (a − b)

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_THRESHOLD_EXPLICIT

⊢ threshold float_format = 340282356779733661637539395458142568448

FRACTION

⊢ ∀a. fraction a = SND (SND a)

INFINITY_IS_INFINITY

⊢ Infinity Plus_infinity ∧ Infinity Minus_infinity

INFINITY_NOT_NAN

⊢ ¬Isnan Plus_infinity ∧ ¬Isnan Minus_infinity

ISFINITE

⊢ ∀a. Finite a ⇔ is_finite float_format (defloat a)

IS_CLOSEST_EXISTS

⊢ ∀v x s. FINITE s ⇒ s ≠ ∅ ⇒ ∃a. is_closest v s x a

IS_FINITE_CLOSEST

⊢ ∀X v p x. is_finite X (closest v p {a | is_finite X a} x)

IS_FINITE_EXPLICIT

⊢ ∀a. is_finite float_format a ⇔
      sign a < 2 ∧ exponent a < 255 ∧ fraction a < 8388608

IS_FINITE_FINITE

⊢ ∀X. FINITE {a | is_finite X a}

IS_FINITE_NONEMPTY

⊢ {a | is_finite X a} ≠ ∅

IS_VALID

⊢ ∀X a.
    is_valid X a ⇔
    sign a < 2 ∧ exponent a < 2 ** expwidth X ∧ fraction a < 2 ** fracwidth X

IS_VALID_CLOSEST

⊢ ∀X v p x. is_valid X (closest v p {a | is_finite X a} x)

IS_VALID_DEFLOAT

⊢ ∀a. is_valid float_format (defloat a)

IS_VALID_FINITE

⊢ FINITE {a | is_valid X a}

IS_VALID_NONEMPTY

⊢ {a | is_valid X a} ≠ ∅

IS_VALID_ROUND

⊢ ∀X x. is_valid X (round X To_nearest x)

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)

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

RELATIVE_ERROR

⊢ ∀x. normalizes x ⇒
      ∃e. abs e ≤ 1 / 2 pow 24 ∧
          (Val (float (round float_format To_nearest x)) = x * (1 + e))

SIGN

⊢ ∀a. sign a = FST a

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)

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)

VAL_FINITE

⊢ ∀a. Finite a ⇒ abs (Val a) ≤ largest float_format

VAL_THRESHOLD

⊢ ∀a. Finite a ⇒ abs (Val a) < threshold float_format

ZERO_IS_ZERO

⊢ Iszero Plus_zero ∧ Iszero Minus_zero

ZERO_NOT_NAN

⊢ ¬Isnan Plus_zero ∧ ¬Isnan Minus_zero