Theory float

⊢ ∀x. error x = Val (float (round float_format To_nearest x)) − x

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

⊢ ∀v p x s. FINITE s ⇒ s ≠ ∅ ⇒ closest v p s x ∈ s

⊢ ∀v p x s. FINITE s ⇒ s ≠ ∅ ⇒ is_closest v s x (closest v p s x)

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

⊢ ∀x. defloat (float (round float_format To_nearest x)) =
      round float_format To_nearest x

⊢ ∀x b.
    defloat
      (float (zerosign float_format b (round float_format To_nearest x))) =
    zerosign float_format b (round float_format To_nearest x)

⊢ ∀b x.
    abs x < threshold float_format ⇒
    is_finite float_format
      (defloat
         (float (zerosign float_format b (round float_format To_nearest x))))

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

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

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

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

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

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

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

⊢ ∀a. Isnan a ∨ Infinity a ∨ Isnormal a ∨ Isdenormal a ∨ Iszero a

⊢ ∀a. Isnan a ∨ Infinity a ∨ Finite a

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

⊢ ∀a. ¬(Isnan a ∧ Infinity a) ∧ ¬(Isnan a ∧ Finite a) ∧
      ¬(Infinity a ∧ Finite a)

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

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

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

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

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

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

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

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

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

⊢ largest float_format = 340282346638528859811704183484516925440

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

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

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

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

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

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

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

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

⊢ threshold float_format = 340282356779733661637539395458142568448

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

⊢ Infinity Plus_infinity ∧ Infinity Minus_infinity

⊢ ¬Isnan Plus_infinity ∧ ¬Isnan Minus_infinity

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

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

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

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

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

⊢ {a | is_finite X a} ≠ ∅

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

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

⊢ ∀a. is_valid float_format (defloat a)

⊢ FINITE {a | is_valid X a}

⊢ {a | is_valid X a} ≠ ∅

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

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

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

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

⊢ ∀a. sign a = FST a

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

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

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

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

⊢ Iszero Plus_zero ∧ Iszero Minus_zero

⊢ ¬Isnan Plus_zero ∧ ¬Isnan Minus_zero