Structure lift_ieeeTheory

signature lift_ieeeTheory =
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 error_at_worst_lemma : thm
    val error_is_zero : thm
    val finite_float_within_threshold : thm
    val float_add : thm
    val float_add_finite : thm
    val float_add_relative : thm
    val float_div : thm
    val float_div_finite : thm
    val float_div_relative : thm
    val float_eq : thm
    val float_eq_refl : thm
    val float_finite : thm
    val float_ge : thm
    val float_gt : thm
    val float_le : thm
    val float_lt : thm
    val float_mul : thm
    val float_mul_add : thm
    val float_mul_add_finite : thm
    val float_mul_add_relative : thm
    val float_mul_finite : thm
    val float_mul_relative : thm
    val float_mul_sub : thm
    val float_mul_sub_finite : thm
    val float_mul_sub_relative : thm
    val float_round_finite : thm
    val float_sqrt : thm
    val float_sqrt_finite : thm
    val float_sqrt_relative : thm
    val float_sub : thm
    val float_sub_finite : thm
    val float_sub_relative : thm
    val float_to_real_finite : thm
    val float_to_real_real_to_float_zero_id : thm
    val float_to_real_threshold : thm
    val is_closest_exits : thm
    val is_finite_closest : thm
    val is_finite_finite : thm
    val is_finite_nonempty : thm
    val non_representable_float_is_zero : thm
    val real_to_float_finite_normal_id : thm
    val relative_error : thm
    val round_finite_normal_float_id : thm
  
  val lift_ieee_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [binary_ieee] Parent theory of "lift_ieee"
   
   [error_def]  Definition
      
      ⊢ ∀x. error (:τ # χ) x = float_to_real (round roundTiesToEven x) − x
   
   [normalizes_def]  Definition
      
      ⊢ ∀x.
            normalizes (:τ # χ) x ⇔
            1 < bias (:χ) ∧ (2 pow (bias (:χ) − 1))⁻¹ ≤ abs x ∧
            abs x < threshold (:τ # χ)
   
   [closest_in_set]  Theorem
      
      ⊢ ∀p s x. FINITE s ⇒ s ≠ ∅ ⇒ closest_such p s x ∈ s
   
   [closest_is_closest]  Theorem
      
      ⊢ ∀p s x. FINITE s ⇒ s ≠ ∅ ⇒ is_closest s x (closest_such p s x)
   
   [closest_is_everything]  Theorem
      
      ⊢ ∀p s x.
            FINITE s ⇒
            s ≠ ∅ ⇒
            is_closest s x (closest_such p s x) ∧
            ((∃b. is_closest s x b ∧ p b) ⇒ p (closest_such p s x))
   
   [error_at_worst_lemma]  Theorem
      
      ⊢ ∀a x.
            abs x < threshold (:τ # χ) ∧ float_is_finite a ⇒
            abs (error (:τ # χ) x) ≤ abs (float_to_real a − x)
   
   [error_is_zero]  Theorem
      
      ⊢ ∀a x.
            float_is_finite a ∧ (float_to_real a = x) ⇒
            (error (:τ # χ) x = 0)
   
   [finite_float_within_threshold]  Theorem
      
      ⊢ ∀f.
            float_is_finite f ⇒
            ¬(float_to_real f ≤ -threshold (:α # β)) ∧
            ¬(float_to_real f ≥ threshold (:α # β))
   
   [float_add]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_add roundTiesToEven a b)) ∧
            (float_to_real (SND (float_add roundTiesToEven a b)) =
             float_to_real a + float_to_real b +
             error (:τ # χ) (float_to_real a + float_to_real b))
   
   [float_add_finite]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a + float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_add roundTiesToEven a b))
   
   [float_add_relative]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            normalizes (:τ # χ) (float_to_real a + float_to_real b) ⇒
            float_is_finite (SND (float_add roundTiesToEven a b)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_add roundTiesToEven a b)) =
                 (float_to_real a + float_to_real b) * (1 + e))
   
   [float_div]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
            abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_div roundTiesToEven a b)) ∧
            (float_to_real (SND (float_div roundTiesToEven a b)) =
             float_to_real a / float_to_real b +
             error (:τ # χ) (float_to_real a / float_to_real b))
   
   [float_div_finite]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
            abs (float_to_real a / float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_div roundTiesToEven a b))
   
   [float_div_relative]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧ ¬float_is_zero b ∧
            normalizes (:τ # χ) (float_to_real a / float_to_real b) ⇒
            float_is_finite (SND (float_div roundTiesToEven a b)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_div roundTiesToEven a b)) =
                 float_to_real a / float_to_real b * (1 + e))
   
   [float_eq]  Theorem
      
      ⊢ ∀x y.
            float_is_finite x ∧ float_is_finite y ⇒
            (float_equal x y ⇔ (float_to_real x = float_to_real y))
   
   [float_eq_refl]  Theorem
      
      ⊢ ∀x. float_equal x x ⇔ ¬float_is_nan x
   
   [float_finite]  Theorem
      
      ⊢ FINITE 𝕌(:(τ, χ) float)
   
   [float_ge]  Theorem
      
      ⊢ ∀x y.
            float_is_finite x ∧ float_is_finite y ⇒
            (float_greater_equal x y ⇔ float_to_real x ≥ float_to_real y)
   
   [float_gt]  Theorem
      
      ⊢ ∀x y.
            float_is_finite x ∧ float_is_finite y ⇒
            (float_greater_than x y ⇔ float_to_real x > float_to_real y)
   
   [float_le]  Theorem
      
      ⊢ ∀x y.
            float_is_finite x ∧ float_is_finite y ⇒
            (float_less_equal x y ⇔ float_to_real x ≤ float_to_real y)
   
   [float_lt]  Theorem
      
      ⊢ ∀x y.
            float_is_finite x ∧ float_is_finite y ⇒
            (float_less_than x y ⇔ float_to_real x < float_to_real y)
   
   [float_mul]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul roundTiesToEven a b)) ∧
            (float_to_real (SND (float_mul roundTiesToEven a b)) =
             float_to_real a * float_to_real b +
             error (:τ # χ) (float_to_real a * float_to_real b))
   
   [float_mul_add]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            abs (float_to_real a * float_to_real b + float_to_real c) <
            threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
            (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
             float_to_real a * float_to_real b + float_to_real c +
             error (:τ # χ)
               (float_to_real a * float_to_real b + float_to_real c))
   
   [float_mul_add_finite]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            abs (float_to_real a * float_to_real b + float_to_real c) <
            threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul_add roundTiesToEven a b c))
   
   [float_mul_add_relative]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            normalizes (:τ # χ)
              (float_to_real a * float_to_real b + float_to_real c) ⇒
            float_is_finite (SND (float_mul_add roundTiesToEven a b c)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_mul_add roundTiesToEven a b c)) =
                 (float_to_real a * float_to_real b + float_to_real c) *
                 (1 + e))
   
   [float_mul_finite]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a * float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul roundTiesToEven a b))
   
   [float_mul_relative]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            normalizes (:τ # χ) (float_to_real a * float_to_real b) ⇒
            float_is_finite (SND (float_mul roundTiesToEven a b)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_mul roundTiesToEven a b)) =
                 float_to_real a * float_to_real b * (1 + e))
   
   [float_mul_sub]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            abs (float_to_real a * float_to_real b − float_to_real c) <
            threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
            (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
             float_to_real a * float_to_real b − float_to_real c +
             error (:τ # χ)
               (float_to_real a * float_to_real b − float_to_real c))
   
   [float_mul_sub_finite]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            abs (float_to_real a * float_to_real b − float_to_real c) <
            threshold (:τ # χ) ⇒
            float_is_finite (SND (float_mul_sub roundTiesToEven a b c))
   
   [float_mul_sub_relative]  Theorem
      
      ⊢ ∀a b c.
            float_is_finite a ∧ float_is_finite b ∧ float_is_finite c ∧
            normalizes (:τ # χ)
              (float_to_real a * float_to_real b − float_to_real c) ⇒
            float_is_finite (SND (float_mul_sub roundTiesToEven a b c)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_mul_sub roundTiesToEven a b c)) =
                 (float_to_real a * float_to_real b − float_to_real c) *
                 (1 + e))
   
   [float_round_finite]  Theorem
      
      ⊢ ∀b x.
            abs x < threshold (:τ # χ) ⇒
            float_is_finite (float_round roundTiesToEven b x)
   
   [float_sqrt]  Theorem
      
      ⊢ ∀a.
            float_is_finite a ∧ (a.Sign = 0w) ∧
            abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
            (float_to_real (SND (float_sqrt roundTiesToEven a)) =
             sqrt (float_to_real a) +
             error (:τ # χ) (sqrt (float_to_real a)))
   
   [float_sqrt_finite]  Theorem
      
      ⊢ ∀a.
            float_is_finite a ∧ (a.Sign = 0w) ∧
            abs (sqrt (float_to_real a)) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_sqrt roundTiesToEven a))
   
   [float_sqrt_relative]  Theorem
      
      ⊢ ∀a.
            float_is_finite a ∧ (a.Sign = 0w) ∧
            normalizes (:τ # χ) (sqrt (float_to_real a)) ⇒
            float_is_finite (SND (float_sqrt roundTiesToEven a)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_sqrt roundTiesToEven a)) =
                 sqrt (float_to_real a) * (1 + e))
   
   [float_sub]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_sub roundTiesToEven a b)) ∧
            (float_to_real (SND (float_sub roundTiesToEven a b)) =
             float_to_real a − float_to_real b +
             error (:τ # χ) (float_to_real a − float_to_real b))
   
   [float_sub_finite]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            abs (float_to_real a − float_to_real b) < threshold (:τ # χ) ⇒
            float_is_finite (SND (float_sub roundTiesToEven a b))
   
   [float_sub_relative]  Theorem
      
      ⊢ ∀a b.
            float_is_finite a ∧ float_is_finite b ∧
            normalizes (:τ # χ) (float_to_real a − float_to_real b) ⇒
            float_is_finite (SND (float_sub roundTiesToEven a b)) ∧
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (SND (float_sub roundTiesToEven a b)) =
                 (float_to_real a − float_to_real b) * (1 + e))
   
   [float_to_real_finite]  Theorem
      
      ⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) ≤ largest (:τ # χ)
   
   [float_to_real_real_to_float_zero_id]  Theorem
      
      ⊢ float_to_real (real_to_float roundTiesToEven 0) = 0
   
   [float_to_real_threshold]  Theorem
      
      ⊢ ∀x. float_is_finite x ⇒ abs (float_to_real x) < threshold (:τ # χ)
   
   [is_closest_exits]  Theorem
      
      ⊢ ∀x s. FINITE s ⇒ s ≠ ∅ ⇒ ∃a. is_closest s x a
   
   [is_finite_closest]  Theorem
      
      ⊢ ∀p x. float_is_finite (closest_such p {a | float_is_finite a} x)
   
   [is_finite_finite]  Theorem
      
      ⊢ FINITE {a | float_is_finite a}
   
   [is_finite_nonempty]  Theorem
      
      ⊢ {a | float_is_finite a} ≠ ∅
   
   [non_representable_float_is_zero]  Theorem
      
      ⊢ ∀ff P.
            2 * abs ff ≤ ulp (:α # β) ⇒
            (float_to_real (float_round roundTiesToEven P ff) = 0)
   
   [real_to_float_finite_normal_id]  Theorem
      
      ⊢ ∀f.
            float_is_finite f ∧ ¬float_is_zero f ⇒
            (real_to_float roundTiesToEven (float_to_real f) = f)
   
   [relative_error]  Theorem
      
      ⊢ ∀x.
            normalizes (:τ # χ) x ⇒
            ∃e.
                abs e ≤ 1 / 2 pow (dimindex (:τ) + 1) ∧
                (float_to_real (round roundTiesToEven x) = x * (1 + e))
   
   [round_finite_normal_float_id]  Theorem
      
      ⊢ ∀f.
            float_is_finite f ∧ ¬float_is_zero f ⇒
            (round roundTiesToEven (float_to_real f) = f)
   
   
*)
end

HOL 4, Kananaskis-13