Structure lift_machine_ieeeTheory
signature lift_machine_ieeeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val fp16_to_real_value_def : thm
val fp32_to_real_value_def : thm
val fp64_to_real_value_def : thm
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"
[fp16_to_real_value_def] Definition
⊢ fp16_to_real_value = float_to_real ∘ fp16_to_float
[fp32_to_real_value_def] Definition
⊢ fp32_to_real_value = float_to_real ∘ fp32_to_float
[fp64_to_real_value_def] Definition
⊢ fp64_to_real_value = float_to_real ∘ fp64_to_float
[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_value a + fp16_to_real_value 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_value (fp16_add roundTiesToEven a b) =
(fp16_to_real_value a + fp16_to_real_value b) * (1 + e))
[fp16_float_div_relative] Theorem
⊢ ∀a b.
fp16_isFinite a ∧ fp16_isFinite b ∧ ¬fp16_isZero b ∧
abs (fp16_to_real_value a / fp16_to_real_value 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_value (fp16_div roundTiesToEven a b) =
fp16_to_real_value a / fp16_to_real_value 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_value a * fp16_to_real_value b +
fp16_to_real_value 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_value (fp16_mul_add roundTiesToEven a b c) =
(fp16_to_real_value a * fp16_to_real_value b +
fp16_to_real_value c) * (1 + e))
[fp16_float_mul_relative] Theorem
⊢ ∀a b.
fp16_isFinite a ∧ fp16_isFinite b ∧
abs (fp16_to_real_value a * fp16_to_real_value 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_value (fp16_mul roundTiesToEven a b) =
fp16_to_real_value a * fp16_to_real_value 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_value a * fp16_to_real_value b −
fp16_to_real_value 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_value (fp16_mul_sub roundTiesToEven a b c) =
(fp16_to_real_value a * fp16_to_real_value b −
fp16_to_real_value c) * (1 + e))
[fp16_float_sqrt_relative] Theorem
⊢ ∀a.
fp16_isFinite a ∧ ¬word_msb a ∧
abs (sqrt (fp16_to_real_value 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_value (fp16_sqrt roundTiesToEven a) =
sqrt (fp16_to_real_value a) * (1 + e))
[fp16_float_sub_relative] Theorem
⊢ ∀a b.
fp16_isFinite a ∧ fp16_isFinite b ∧
abs (fp16_to_real_value a − fp16_to_real_value 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_value (fp16_sub roundTiesToEven a b) =
(fp16_to_real_value a − fp16_to_real_value b) * (1 + e))
[fp32_float_add_relative] Theorem
⊢ ∀a b.
fp32_isFinite a ∧ fp32_isFinite b ∧
abs (fp32_to_real_value a + fp32_to_real_value 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_value (fp32_add roundTiesToEven a b) =
(fp32_to_real_value a + fp32_to_real_value b) * (1 + e))
[fp32_float_div_relative] Theorem
⊢ ∀a b.
fp32_isFinite a ∧ fp32_isFinite b ∧ ¬fp32_isZero b ∧
abs (fp32_to_real_value a / fp32_to_real_value 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_value (fp32_div roundTiesToEven a b) =
fp32_to_real_value a / fp32_to_real_value 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_value a * fp32_to_real_value b +
fp32_to_real_value 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_value (fp32_mul_add roundTiesToEven a b c) =
(fp32_to_real_value a * fp32_to_real_value b +
fp32_to_real_value c) * (1 + e))
[fp32_float_mul_relative] Theorem
⊢ ∀a b.
fp32_isFinite a ∧ fp32_isFinite b ∧
abs (fp32_to_real_value a * fp32_to_real_value 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_value (fp32_mul roundTiesToEven a b) =
fp32_to_real_value a * fp32_to_real_value 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_value a * fp32_to_real_value b −
fp32_to_real_value 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_value (fp32_mul_sub roundTiesToEven a b c) =
(fp32_to_real_value a * fp32_to_real_value b −
fp32_to_real_value c) * (1 + e))
[fp32_float_sqrt_relative] Theorem
⊢ ∀a.
fp32_isFinite a ∧ ¬word_msb a ∧
abs (sqrt (fp32_to_real_value 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_value (fp32_sqrt roundTiesToEven a) =
sqrt (fp32_to_real_value a) * (1 + e))
[fp32_float_sub_relative] Theorem
⊢ ∀a b.
fp32_isFinite a ∧ fp32_isFinite b ∧
abs (fp32_to_real_value a − fp32_to_real_value 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_value (fp32_sub roundTiesToEven a b) =
(fp32_to_real_value a − fp32_to_real_value b) * (1 + e))
[fp64_float_add_relative] Theorem
⊢ ∀a b.
fp64_isFinite a ∧ fp64_isFinite b ∧
abs (fp64_to_real_value a + fp64_to_real_value 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_value (fp64_add roundTiesToEven a b) =
(fp64_to_real_value a + fp64_to_real_value b) * (1 + e))
[fp64_float_div_relative] Theorem
⊢ ∀a b.
fp64_isFinite a ∧ fp64_isFinite b ∧ ¬fp64_isZero b ∧
abs (fp64_to_real_value a / fp64_to_real_value 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_value (fp64_div roundTiesToEven a b) =
fp64_to_real_value a / fp64_to_real_value 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_value a * fp64_to_real_value b +
fp64_to_real_value 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_value (fp64_mul_add roundTiesToEven a b c) =
(fp64_to_real_value a * fp64_to_real_value b +
fp64_to_real_value c) * (1 + e))
[fp64_float_mul_relative] Theorem
⊢ ∀a b.
fp64_isFinite a ∧ fp64_isFinite b ∧
abs (fp64_to_real_value a * fp64_to_real_value 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_value (fp64_mul roundTiesToEven a b) =
fp64_to_real_value a * fp64_to_real_value 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_value a * fp64_to_real_value b −
fp64_to_real_value 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_value (fp64_mul_sub roundTiesToEven a b c) =
(fp64_to_real_value a * fp64_to_real_value b −
fp64_to_real_value c) * (1 + e))
[fp64_float_sqrt_relative] Theorem
⊢ ∀a.
fp64_isFinite a ∧ ¬word_msb a ∧
abs (sqrt (fp64_to_real_value 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_value (fp64_sqrt roundTiesToEven a) =
sqrt (fp64_to_real_value a) * (1 + e))
[fp64_float_sub_relative] Theorem
⊢ ∀a b.
fp64_isFinite a ∧ fp64_isFinite b ∧
abs (fp64_to_real_value a − fp64_to_real_value 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_value (fp64_sub roundTiesToEven a b) =
(fp64_to_real_value a − fp64_to_real_value b) * (1 + e))
*)
end
HOL 4, Kananaskis-11