Structure lift_machine_ieeeTheory

signature lift_machine_ieeeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val interval_def : thm
  
  (*  Theorems  *)
    val fp16_float_add_relative : thm
    val fp16_float_div_relative : thm
    val fp16_float_mul_add_relative : thm
    val fp16_float_mul_relative : thm
    val fp16_float_mul_sub_relative : thm
    val fp16_float_sqrt_relative : thm
    val fp16_float_sub_relative : thm
    val fp32_float_add_relative : thm
    val fp32_float_div_relative : thm
    val fp32_float_mul_add_relative : thm
    val fp32_float_mul_relative : thm
    val fp32_float_mul_sub_relative : thm
    val fp32_float_sqrt_relative : thm
    val fp32_float_sub_relative : thm
    val fp64_float_add_relative : thm
    val fp64_float_div_relative : thm
    val fp64_float_mul_add_relative : thm
    val fp64_float_mul_relative : thm
    val fp64_float_mul_sub_relative : thm
    val fp64_float_sqrt_relative : thm
    val fp64_float_sub_relative : thm
  
  val lift_machine_ieee_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [lift_ieee] Parent theory of "lift_machine_ieee"
   
   [machine_ieee] Parent theory of "lift_machine_ieee"
   
   [interval_def]  Definition
      
      ⊢ ∀a b. (a .. b) = {x | a ≤ x ∧ x < b}
   
   [fp16_float_add_relative]  Theorem
      
      ⊢ ∀a b.
            fp16_isFinite a ∧ fp16_isFinite b ∧
            abs (fp16_to_real a + fp16_to_real b) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_add roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_add roundTiesToEven a b) =
                (fp16_to_real a + fp16_to_real b) * (1 + e)
   
   [fp16_float_div_relative]  Theorem
      
      ⊢ ∀a b.
            fp16_isFinite a ∧ fp16_isFinite b ∧ ¬fp16_isZero b ∧
            abs (fp16_to_real a / fp16_to_real b) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_div roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_div roundTiesToEven a b) =
                fp16_to_real a / fp16_to_real b * (1 + e)
   
   [fp16_float_mul_add_relative]  Theorem
      
      ⊢ ∀a b c.
            fp16_isFinite a ∧ fp16_isFinite b ∧ fp16_isFinite c ∧
            abs (fp16_to_real a * fp16_to_real b + fp16_to_real c) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_mul_add roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_mul_add roundTiesToEven a b c) =
                (fp16_to_real a * fp16_to_real b + fp16_to_real c) *
                (1 + e)
   
   [fp16_float_mul_relative]  Theorem
      
      ⊢ ∀a b.
            fp16_isFinite a ∧ fp16_isFinite b ∧
            abs (fp16_to_real a * fp16_to_real b) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_mul roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_mul roundTiesToEven a b) =
                fp16_to_real a * fp16_to_real b * (1 + e)
   
   [fp16_float_mul_sub_relative]  Theorem
      
      ⊢ ∀a b c.
            fp16_isFinite a ∧ fp16_isFinite b ∧ fp16_isFinite c ∧
            abs (fp16_to_real a * fp16_to_real b − fp16_to_real c) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_mul_sub roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_mul_sub roundTiesToEven a b c) =
                (fp16_to_real a * fp16_to_real b − fp16_to_real c) *
                (1 + e)
   
   [fp16_float_sqrt_relative]  Theorem
      
      ⊢ ∀a.
            fp16_isFinite a ∧ ¬word_msb a ∧
            abs (sqrt (fp16_to_real a)) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_sqrt roundTiesToEven a) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_sqrt roundTiesToEven a) =
                sqrt (fp16_to_real a) * (1 + e)
   
   [fp16_float_sub_relative]  Theorem
      
      ⊢ ∀a b.
            fp16_isFinite a ∧ fp16_isFinite b ∧
            abs (fp16_to_real a − fp16_to_real b) ∈
            (1 / 2 pow 14 .. 2 pow 30 / 2 pow 15 * (2 − 1 / 2 pow 11)) ⇒
            fp16_isFinite (fp16_sub roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 11 ∧
                fp16_to_real (fp16_sub roundTiesToEven a b) =
                (fp16_to_real a − fp16_to_real b) * (1 + e)
   
   [fp32_float_add_relative]  Theorem
      
      ⊢ ∀a b.
            fp32_isFinite a ∧ fp32_isFinite b ∧
            abs (fp32_to_real a + fp32_to_real b) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_add roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_add roundTiesToEven a b) =
                (fp32_to_real a + fp32_to_real b) * (1 + e)
   
   [fp32_float_div_relative]  Theorem
      
      ⊢ ∀a b.
            fp32_isFinite a ∧ fp32_isFinite b ∧ ¬fp32_isZero b ∧
            abs (fp32_to_real a / fp32_to_real b) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_div roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_div roundTiesToEven a b) =
                fp32_to_real a / fp32_to_real b * (1 + e)
   
   [fp32_float_mul_add_relative]  Theorem
      
      ⊢ ∀a b c.
            fp32_isFinite a ∧ fp32_isFinite b ∧ fp32_isFinite c ∧
            abs (fp32_to_real a * fp32_to_real b + fp32_to_real c) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_mul_add roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_mul_add roundTiesToEven a b c) =
                (fp32_to_real a * fp32_to_real b + fp32_to_real c) *
                (1 + e)
   
   [fp32_float_mul_relative]  Theorem
      
      ⊢ ∀a b.
            fp32_isFinite a ∧ fp32_isFinite b ∧
            abs (fp32_to_real a * fp32_to_real b) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_mul roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_mul roundTiesToEven a b) =
                fp32_to_real a * fp32_to_real b * (1 + e)
   
   [fp32_float_mul_sub_relative]  Theorem
      
      ⊢ ∀a b c.
            fp32_isFinite a ∧ fp32_isFinite b ∧ fp32_isFinite c ∧
            abs (fp32_to_real a * fp32_to_real b − fp32_to_real c) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_mul_sub roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_mul_sub roundTiesToEven a b c) =
                (fp32_to_real a * fp32_to_real b − fp32_to_real c) *
                (1 + e)
   
   [fp32_float_sqrt_relative]  Theorem
      
      ⊢ ∀a.
            fp32_isFinite a ∧ ¬word_msb a ∧
            abs (sqrt (fp32_to_real a)) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_sqrt roundTiesToEven a) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_sqrt roundTiesToEven a) =
                sqrt (fp32_to_real a) * (1 + e)
   
   [fp32_float_sub_relative]  Theorem
      
      ⊢ ∀a b.
            fp32_isFinite a ∧ fp32_isFinite b ∧
            abs (fp32_to_real a − fp32_to_real b) ∈
            (1 / 2 pow 126 .. 2 pow 254 / 2 pow 127 * (2 − 1 / 2 pow 24)) ⇒
            fp32_isFinite (fp32_sub roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 24 ∧
                fp32_to_real (fp32_sub roundTiesToEven a b) =
                (fp32_to_real a − fp32_to_real b) * (1 + e)
   
   [fp64_float_add_relative]  Theorem
      
      ⊢ ∀a b.
            fp64_isFinite a ∧ fp64_isFinite b ∧
            abs (fp64_to_real a + fp64_to_real b) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_add roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_add roundTiesToEven a b) =
                (fp64_to_real a + fp64_to_real b) * (1 + e)
   
   [fp64_float_div_relative]  Theorem
      
      ⊢ ∀a b.
            fp64_isFinite a ∧ fp64_isFinite b ∧ ¬fp64_isZero b ∧
            abs (fp64_to_real a / fp64_to_real b) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_div roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_div roundTiesToEven a b) =
                fp64_to_real a / fp64_to_real b * (1 + e)
   
   [fp64_float_mul_add_relative]  Theorem
      
      ⊢ ∀a b c.
            fp64_isFinite a ∧ fp64_isFinite b ∧ fp64_isFinite c ∧
            abs (fp64_to_real a * fp64_to_real b + fp64_to_real c) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_mul_add roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_mul_add roundTiesToEven a b c) =
                (fp64_to_real a * fp64_to_real b + fp64_to_real c) *
                (1 + e)
   
   [fp64_float_mul_relative]  Theorem
      
      ⊢ ∀a b.
            fp64_isFinite a ∧ fp64_isFinite b ∧
            abs (fp64_to_real a * fp64_to_real b) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_mul roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_mul roundTiesToEven a b) =
                fp64_to_real a * fp64_to_real b * (1 + e)
   
   [fp64_float_mul_sub_relative]  Theorem
      
      ⊢ ∀a b c.
            fp64_isFinite a ∧ fp64_isFinite b ∧ fp64_isFinite c ∧
            abs (fp64_to_real a * fp64_to_real b − fp64_to_real c) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_mul_sub roundTiesToEven a b c) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_mul_sub roundTiesToEven a b c) =
                (fp64_to_real a * fp64_to_real b − fp64_to_real c) *
                (1 + e)
   
   [fp64_float_sqrt_relative]  Theorem
      
      ⊢ ∀a.
            fp64_isFinite a ∧ ¬word_msb a ∧
            abs (sqrt (fp64_to_real a)) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_sqrt roundTiesToEven a) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_sqrt roundTiesToEven a) =
                sqrt (fp64_to_real a) * (1 + e)
   
   [fp64_float_sub_relative]  Theorem
      
      ⊢ ∀a b.
            fp64_isFinite a ∧ fp64_isFinite b ∧
            abs (fp64_to_real a − fp64_to_real b) ∈
            (1 / 2 pow 1022 .. 2 pow 2046 / 2 pow 1023 * (2 − 1 / 2 pow 53)) ⇒
            fp64_isFinite (fp64_sub roundTiesToEven a b) ∧
            ∃e.
                abs e ≤ 1 / 2 pow 53 ∧
                fp64_to_real (fp64_sub roundTiesToEven a b) =
                (fp64_to_real a − fp64_to_real b) * (1 + e)
   
   
*)
end

HOL 4, Kananaskis-13