Structure floatTheory

signature floatTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val error_def : thm
    val normalizes_def : thm
  
  (*  Theorems  *)
    val CLOSEST_IN_SET : thm
    val CLOSEST_IS_CLOSEST : thm
    val CLOSEST_IS_EVERYTHING : thm
    val DEFLOAT_FLOAT_ROUND : thm
    val DEFLOAT_FLOAT_ZEROSIGN_ROUND : thm
    val DEFLOAT_FLOAT_ZEROSIGN_ROUND_FINITE : thm
    val ERROR_BOUND_NORM_STRONG : thm
    val ERROR_BOUND_NORM_STRONG_NORMALIZE : thm
    val ERROR_IS_ZERO : thm
    val EXPONENT : thm
    val FLOAT_ADD : thm
    val FLOAT_ADD_FINITE : thm
    val FLOAT_ADD_RELATIVE : thm
    val FLOAT_CASES : thm
    val FLOAT_CASES_FINITE : thm
    val FLOAT_DISTINCT : thm
    val FLOAT_DISTINCT_FINITE : thm
    val FLOAT_DIV : thm
    val FLOAT_DIV_RELATIVE : thm
    val FLOAT_EQ : thm
    val FLOAT_EQ_REFL : thm
    val FLOAT_GE : thm
    val FLOAT_GT : thm
    val FLOAT_INFINITES_DISTINCT : thm
    val FLOAT_INFINITIES : thm
    val FLOAT_INFINITIES_SIGNED : thm
    val FLOAT_LARGEST_EXPLICIT : thm
    val FLOAT_LE : thm
    val FLOAT_LT : thm
    val FLOAT_MUL : thm
    val FLOAT_MUL_FINITE : thm
    val FLOAT_MUL_RELATIVE : thm
    val FLOAT_SUB : thm
    val FLOAT_SUB_FINITE : thm
    val FLOAT_SUB_RELATIVE : thm
    val FLOAT_THRESHOLD_EXPLICIT : thm
    val FRACTION : thm
    val INFINITY_IS_INFINITY : thm
    val INFINITY_NOT_NAN : thm
    val ISFINITE : thm
    val IS_CLOSEST_EXISTS : thm
    val IS_FINITE_CLOSEST : thm
    val IS_FINITE_EXPLICIT : thm
    val IS_FINITE_FINITE : thm
    val IS_FINITE_NONEMPTY : thm
    val IS_VALID : thm
    val IS_VALID_CLOSEST : thm
    val IS_VALID_DEFLOAT : thm
    val IS_VALID_FINITE : thm
    val IS_VALID_NONEMPTY : thm
    val IS_VALID_ROUND : thm
    val IS_VALID_SPECIAL : thm
    val REAL_IN_BINADE : thm
    val RELATIVE_ERROR : thm
    val SIGN : thm
    val VALOF : thm
    val VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND : thm
    val VAL_FINITE : thm
    val VAL_THRESHOLD : thm
    val ZERO_IS_ZERO : thm
    val ZERO_NOT_NAN : thm
  
  val float_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [ieee] Parent theory of "float"
   
   [error_def]  Definition
      
      ⊢ ∀x. error x = Val (float (round float_format To_nearest x)) − x
   
   [normalizes_def]  Definition
      
      ⊢ ∀x.
            normalizes x ⇔
            (2 pow (bias float_format − 1))⁻¹ ≤ abs x ∧
            abs x < threshold float_format
   
   [CLOSEST_IN_SET]  Theorem
      
      ⊢ ∀v p x s. FINITE s ⇒ s ≠ ∅ ⇒ closest v p s x ∈ s
   
   [CLOSEST_IS_CLOSEST]  Theorem
      
      ⊢ ∀v p x s. FINITE s ⇒ s ≠ ∅ ⇒ is_closest v s x (closest v p s x)
   
   [CLOSEST_IS_EVERYTHING]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x.
            defloat (float (round float_format To_nearest x)) =
            round float_format To_nearest x
   
   [DEFLOAT_FLOAT_ZEROSIGN_ROUND]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x. normalizes x ⇒ ∃j. abs (error x) ≤ 2 pow j / 2 pow 150
   
   [ERROR_IS_ZERO]  Theorem
      
      ⊢ ∀a x. Finite a ∧ (Val a = x) ⇒ (error x = 0)
   
   [EXPONENT]  Theorem
      
      ⊢ ∀a. exponent a = FST (SND a)
   
   [FLOAT_ADD]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀b a.
            Finite a ∧ Finite b ∧
            abs (Val a + Val b) < threshold float_format ⇒
            Finite (a + b)
   
   [FLOAT_ADD_RELATIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a. Isnan a ∨ Infinity a ∨ Isnormal a ∨ Isdenormal a ∨ Iszero a
   
   [FLOAT_CASES_FINITE]  Theorem
      
      ⊢ ∀a. Isnan a ∨ Infinity a ∨ Finite a
   
   [FLOAT_DISTINCT]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a.
            ¬(Isnan a ∧ Infinity a) ∧ ¬(Isnan a ∧ Finite a) ∧
            ¬(Infinity a ∧ Finite a)
   
   [FLOAT_DIV]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a b. Finite a ∧ Finite b ⇒ (a == b ⇔ (Val a = Val b))
   
   [FLOAT_EQ_REFL]  Theorem
      
      ⊢ ∀a. a == a ⇔ ¬Isnan a
   
   [FLOAT_GE]  Theorem
      
      ⊢ ∀a b. Finite a ∧ Finite b ⇒ (a ≥ b ⇔ Val a ≥ Val b)
   
   [FLOAT_GT]  Theorem
      
      ⊢ ∀a b. Finite a ∧ Finite b ⇒ (a > b ⇔ Val a > Val b)
   
   [FLOAT_INFINITES_DISTINCT]  Theorem
      
      ⊢ ∀a. ¬(a == Plus_infinity ∧ a == Minus_infinity)
   
   [FLOAT_INFINITIES]  Theorem
      
      ⊢ ∀a. Infinity a ⇔ a == Plus_infinity ∨ a == Minus_infinity
   
   [FLOAT_INFINITIES_SIGNED]  Theorem
      
      ⊢ (sign (defloat Plus_infinity) = 0) ∧
        (sign (defloat Minus_infinity) = 1)
   
   [FLOAT_LARGEST_EXPLICIT]  Theorem
      
      ⊢ largest float_format = 340282346638528859811704183484516925440
   
   [FLOAT_LE]  Theorem
      
      ⊢ ∀a b. Finite a ∧ Finite b ⇒ (a ≤ b ⇔ Val a ≤ Val b)
   
   [FLOAT_LT]  Theorem
      
      ⊢ ∀a b. Finite a ∧ Finite b ⇒ (a < b ⇔ Val a < Val b)
   
   [FLOAT_MUL]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀b a.
            Finite a ∧ Finite b ∧
            abs (Val a * Val b) < threshold float_format ⇒
            Finite (a * b)
   
   [FLOAT_MUL_RELATIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀b a.
            Finite a ∧ Finite b ∧
            abs (Val a − Val b) < threshold float_format ⇒
            Finite (a − b)
   
   [FLOAT_SUB_RELATIVE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ threshold float_format = 340282356779733661637539395458142568448
   
   [FRACTION]  Theorem
      
      ⊢ ∀a. fraction a = SND (SND a)
   
   [INFINITY_IS_INFINITY]  Theorem
      
      ⊢ Infinity Plus_infinity ∧ Infinity Minus_infinity
   
   [INFINITY_NOT_NAN]  Theorem
      
      ⊢ ¬Isnan Plus_infinity ∧ ¬Isnan Minus_infinity
   
   [ISFINITE]  Theorem
      
      ⊢ ∀a. Finite a ⇔ is_finite float_format (defloat a)
   
   [IS_CLOSEST_EXISTS]  Theorem
      
      ⊢ ∀v x s. FINITE s ⇒ s ≠ ∅ ⇒ ∃a. is_closest v s x a
   
   [IS_FINITE_CLOSEST]  Theorem
      
      ⊢ ∀X v p x. is_finite X (closest v p {a | is_finite X a} x)
   
   [IS_FINITE_EXPLICIT]  Theorem
      
      ⊢ ∀a.
            is_finite float_format a ⇔
            sign a < 2 ∧ exponent a < 255 ∧ fraction a < 8388608
   
   [IS_FINITE_FINITE]  Theorem
      
      ⊢ ∀X. FINITE {a | is_finite X a}
   
   [IS_FINITE_NONEMPTY]  Theorem
      
      ⊢ {a | is_finite X a} ≠ ∅
   
   [IS_VALID]  Theorem
      
      ⊢ ∀X a.
            is_valid X a ⇔
            sign a < 2 ∧ exponent a < 2 ** expwidth X ∧
            fraction a < 2 ** fracwidth X
   
   [IS_VALID_CLOSEST]  Theorem
      
      ⊢ ∀X v p x. is_valid X (closest v p {a | is_finite X a} x)
   
   [IS_VALID_DEFLOAT]  Theorem
      
      ⊢ ∀a. is_valid float_format (defloat a)
   
   [IS_VALID_FINITE]  Theorem
      
      ⊢ FINITE {a | is_valid X a}
   
   [IS_VALID_NONEMPTY]  Theorem
      
      ⊢ {a | is_valid X a} ≠ ∅
   
   [IS_VALID_ROUND]  Theorem
      
      ⊢ ∀X x. is_valid X (round X To_nearest x)
   
   [IS_VALID_SPECIAL]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀x.
            normalizes x ⇒
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                (Val (float (round float_format To_nearest x)) =
                 x * (1 + e))
   
   [SIGN]  Theorem
      
      ⊢ ∀a. sign a = FST a
   
   [VALOF]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a. Finite a ⇒ abs (Val a) ≤ largest float_format
   
   [VAL_THRESHOLD]  Theorem
      
      ⊢ ∀a. Finite a ⇒ abs (Val a) < threshold float_format
   
   [ZERO_IS_ZERO]  Theorem
      
      ⊢ Iszero Plus_zero ∧ Iszero Minus_zero
   
   [ZERO_NOT_NAN]  Theorem
      
      ⊢ ¬Isnan Plus_zero ∧ ¬Isnan Minus_zero
   
   
*)
end

HOL 4, Kananaskis-13