Structure floatTheory
signature floatTheory =
sig
type thm = Thm.thm
(* Definitions *)
val error_def : thm
val normalizes : thm
(* Theorems *)
val ADD_SUB2 : thm
val BOUND_AT_WORST_LEMMA : thm
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_AT_WORST_LEMMA : thm
val ERROR_BOUND_BIG : thm
val ERROR_BOUND_BIG1 : thm
val ERROR_BOUND_LEMMA1 : thm
val ERROR_BOUND_LEMMA2 : thm
val ERROR_BOUND_LEMMA3 : thm
val ERROR_BOUND_LEMMA4 : thm
val ERROR_BOUND_LEMMA5 : thm
val ERROR_BOUND_LEMMA6 : thm
val ERROR_BOUND_LEMMA7 : thm
val ERROR_BOUND_LEMMA8 : thm
val ERROR_BOUND_NORM_STRONG : thm
val ERROR_BOUND_NORM_STRONG_NORMALIZE : thm
val ERROR_BOUND_SMALL : thm
val ERROR_BOUND_SMALL1 : thm
val ERROR_BOUND_TINY : thm
val ERROR_IS_ZERO : thm
val EXPONENT : thm
val EXP_GT_ZERO : thm
val EXP_LT_0 : thm
val FINITE_R3 : thm
val FLOAT_ADD : thm
val FLOAT_ADD_RELATIVE : thm
val FLOAT_CASES : thm
val FLOAT_CASES_FINITE : thm
val FLOAT_COUNTINDUCT : 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_FINITECOUNT : thm
val FLOAT_FIRSTCROSS : thm
val FLOAT_FIRSTCROSS1 : thm
val FLOAT_FIRSTCROSS2 : thm
val FLOAT_FIRSTCROSS3 : 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_IS_FINITE_SUBSET : 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 ISFINITE_LEMMA : thm
val IS_CLOSEST_EXISTS : thm
val IS_FINITE_ALT : thm
val IS_FINITE_ALT1 : 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 LT_SUC_LE : thm
val LT_THRESHOLD_LT_POW_INV : thm
val MATCH_FLOAT_FINITE : thm
val REAL_ABS_DIV : thm
val REAL_ABS_INV : thm
val REAL_ABS_NUM : thm
val REAL_ABS_POW : thm
val REAL_IN_BINADE : thm
val REAL_LE_INV2 : thm
val REAL_LE_LCANCEL_IMP : thm
val REAL_LE_RCANCEL_IMP : thm
val REAL_LT_LCANCEL_IMP : thm
val REAL_LT_RCANCEL_IMP : thm
val REAL_MUL_AC : thm
val REAL_NEG_IN_BINADE : thm
val REAL_OF_NUM_LT : thm
val REAL_OF_NUM_POW : thm
val REAL_OF_NUM_SUB : thm
val REAL_POS_IN_BINADE : thm
val REAL_POW_EQ_0 : thm
val REAL_POW_LE_1 : thm
val REAL_POW_MONO : thm
val RELATIVE_ERROR : thm
val RELATIVE_ERROR_NEG : thm
val RELATIVE_ERROR_POS : thm
val RELATIVE_ERROR_ZERO : thm
val RRRC1 : thm
val RRRC10 : thm
val RRRC11 : thm
val RRRC2 : thm
val RRRC3 : thm
val RRRC4 : thm
val RRRC5 : thm
val RRRC6 : thm
val RRRC7 : thm
val RRRC8 : thm
val RRRC9 : thm
val SIGN : thm
val THRESHOLD_LT_POW_INV : thm
val THRESHOLD_MUL_LT : thm
val TWO_EXP_GE_1 : thm
val VALOF : thm
val VALOF_DEFLOAT_FLOAT_ZEROSIGN_ROUND : thm
val VALOF_SCALE_DOWN : thm
val VALOF_SCALE_UP : thm
val VAL_FINITE : thm
val VAL_THRESHOLD : thm
val Val_FLOAT_ROUND_VALOF : thm
val ZERO_IS_ZERO : thm
val ZERO_NOT_NAN : thm
val egt1 : thm
val egtff : thm
val ftt : thm
val inv23gt0 : thm
val lt1eqmul : thm
val not2eqz : thm
val noteteeszegtz : thm
val sucminmullt : thm
val temonz : thm
val tfflttfs : thm
val tittfittt : thm
val tpetfs : thm
val tptteteesze : thm
val tteettto : thm
val ttpinv : thm
val twogz : thm
val v127not0 : thm
val v23not0 : 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] Definition
|- ∀x.
normalizes x ⇔
inv (2 pow (bias float_format − 1)) ≤ abs x ∧
abs x < threshold float_format
[ADD_SUB2] Theorem
|- ∀m n. m + n − m = n
[BOUND_AT_WORST_LEMMA] Theorem
|- ∀a x.
abs x < threshold float_format ∧ is_finite float_format a ⇒
abs (valof float_format (round float_format To_nearest x) − x) ≤
abs (valof float_format a − x)
[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 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_AT_WORST_LEMMA] Theorem
|- ∀a x.
abs x < threshold float_format ∧ Finite a ⇒
abs (error x) ≤ abs (Val a − x)
[ERROR_BOUND_BIG] Theorem
|- ∀k x.
2 pow k ≤ abs x ∧ abs x < 2 pow SUC k ∧
abs x < threshold float_format ⇒
abs (error x) ≤ 2 pow k / 2 pow 24
[ERROR_BOUND_BIG1] Theorem
|- ∀x k.
2 pow k ≤ abs x ∧ abs x < 2 pow SUC k ∧
abs x < threshold float_format ⇒
∃a. Finite a ∧ abs (Val a − x) ≤ 2 pow k / 2 pow 24
[ERROR_BOUND_LEMMA1] Theorem
|- ∀x.
0 ≤ x ∧ x < 1 ⇒
∃n. n < 2 ** 23 ∧ &n / 2 pow 23 ≤ x ∧ x < &SUC n / 2 pow 23
[ERROR_BOUND_LEMMA2] Theorem
|- ∀x.
0 ≤ x ∧ x < 1 ⇒
∃n. n ≤ 2 ** 23 ∧ abs (x − &n / 2 pow 23) ≤ inv (2 pow 24)
[ERROR_BOUND_LEMMA3] Theorem
|- ∀x.
1 ≤ x ∧ x < 2 ⇒
∃n. n ≤ 2 ** 23 ∧ abs (1 + &n / 2 pow 23 − x) ≤ inv (2 pow 24)
[ERROR_BOUND_LEMMA4] Theorem
|- ∀x.
1 ≤ x ∧ x < 2 ⇒
∃e f.
abs (Val (float (0,e,f)) − x) ≤ inv (2 pow 24) ∧ f < 2 ** 23 ∧
((e = bias float_format) ∨
(e = SUC (bias float_format)) ∧ (f = 0))
[ERROR_BOUND_LEMMA5] Theorem
|- ∀x.
1 ≤ abs x ∧ abs x < 2 ⇒
∃s e f.
abs (Val (float (s,e,f)) − x) ≤ inv (2 pow 24) ∧ s < 2 ∧
f < 2 ** 23 ∧
((e = bias float_format) ∨
(e = SUC (bias float_format)) ∧ (f = 0))
[ERROR_BOUND_LEMMA6] Theorem
|- ∀x.
0 ≤ x ∧ x < inv (2 pow 126) ⇒
∃n.
n ≤ 2 ** 23 ∧
abs (x − 2 / 2 pow 127 * &n / 2 pow 23) ≤ inv (2 pow 150)
[ERROR_BOUND_LEMMA7] Theorem
|- ∀x.
0 ≤ x ∧ x < inv (2 pow 126) ⇒
∃e f.
abs (Val (float (0,e,f)) − x) ≤ inv (2 pow 150) ∧
f < 2 ** 23 ∧ ((e = 0) ∨ (e = 1) ∧ (f = 0))
[ERROR_BOUND_LEMMA8] Theorem
|- ∀x.
abs x < inv (2 pow 126) ⇒
∃s e f.
abs (Val (float (s,e,f)) − x) ≤ inv (2 pow 150) ∧ s < 2 ∧
f < 2 ** 23 ∧ ((e = 0) ∨ (e = 1) ∧ (f = 0))
[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_BOUND_SMALL] Theorem
|- ∀k x.
inv (2 pow SUC k) ≤ abs x ∧ abs x < inv (2 pow k) ∧ k < 126 ⇒
abs (error x) ≤ inv (2 pow SUC k * 2 pow 24)
[ERROR_BOUND_SMALL1] Theorem
|- ∀x k.
inv (2 pow SUC k) ≤ abs x ∧ abs x < inv (2 pow k) ∧ k < 126 ⇒
∃a. Finite a ∧ abs (Val a − x) ≤ inv (2 pow SUC k * 2 pow 24)
[ERROR_BOUND_TINY] Theorem
|- ∀x. abs x < inv (2 pow 126) ⇒ abs (error x) ≤ inv (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)
[EXP_GT_ZERO] Theorem
|- ∀n. 0 < 2 ** n
[EXP_LT_0] Theorem
|- ∀n x. 0 < x ** n ⇔ x ≠ 0 ∨ (n = 0)
[FINITE_R3] Theorem
|- ∀m n p. FINITE {a | FST a < m ∧ FST (SND a) < n ∧ SND (SND a) < p}
[FLOAT_ADD] Theorem
|- ∀a b.
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_COUNTINDUCT] Theorem
|- ∀n. ({x | x < 0} = ∅) ∧ ({x | x < SUC n} = n INSERT {x | x < n})
[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_FINITECOUNT] Theorem
|- ∀n. FINITE {x | x < n}
[FLOAT_FIRSTCROSS] Theorem
|- ∀m n p.
{a | FST a < m ∧ FST (SND a) < n ∧ SND (SND a) < p} =
IMAGE (λ(x,y,z). (x,y,z))
({x | x < m} × ({y | y < n} × {z | z < p}))
[FLOAT_FIRSTCROSS1] Theorem
|- ∀x m n p.
(∃x'.
(x = (λ(x,y,z). (x,y,z)) x') ∧ FST x' < m ∧
FST (SND x') < n ∧ SND (SND x') < p) ⇒
FST x < m ∧ FST (SND x) < n ∧ SND (SND x) < p
[FLOAT_FIRSTCROSS2] Theorem
|- ∀x m n p.
FST x < m ∧ FST (SND x) < n ∧ SND (SND x) < p ⇒
∃x'.
(x = (λ(x,y,z). (x,y,z)) x') ∧ FST x' < m ∧ FST (SND x') < n ∧
SND (SND x') < p
[FLOAT_FIRSTCROSS3] Theorem
|- ∀x m n p.
FST x < m ∧ FST (SND x) < n ∧ SND (SND x) < p ⇔
∃x'.
(x = (λ(x,y,z). (x,y,z)) x') ∧ FST x' < m ∧ FST (SND x') < n ∧
SND (SND x') < p
[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_IS_FINITE_SUBSET] Theorem
|- ∀X. {a | is_finite X a} ⊆ {a | is_valid X a}
[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
|- ∀a b.
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
|- ∀a b.
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)
[ISFINITE_LEMMA] Theorem
|- ∀s e f.
s < 2 ∧ e < 255 ∧ f < 2 ** 23 ⇒
Finite (float (s,e,f)) ∧ is_valid float_format (s,e,f)
[IS_CLOSEST_EXISTS] Theorem
|- ∀v x s. FINITE s ⇒ s ≠ ∅ ⇒ ∃a. is_closest v s x a
[IS_FINITE_ALT] Theorem
|- ∀a.
is_finite float_format a ⇔
is_valid float_format a ∧ exponent a < 255
[IS_FINITE_ALT1] Theorem
|- ∀a.
is_normal float_format a ∨ is_denormal float_format a ∨
is_zero float_format a ⇔ exponent a < 255
[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)
[LT_SUC_LE] Theorem
|- ∀m n. m < SUC n ⇔ m ≤ n
[LT_THRESHOLD_LT_POW_INV] Theorem
|- ∀x. x < threshold (8,23) ⇒ x < 2 pow (emax (8,23) − 1) / 2 pow 126
[MATCH_FLOAT_FINITE] Theorem
|- ∀X.
{a | is_finite X a} ⊆ {a | is_valid X a} ⇒
FINITE {a | is_finite X a}
[REAL_ABS_DIV] Theorem
|- ∀x y. abs (x / y) = abs x / abs y
[REAL_ABS_INV] Theorem
|- ∀x. abs (inv x) = inv (abs x)
[REAL_ABS_NUM] Theorem
|- abs (&n) = &n
[REAL_ABS_POW] Theorem
|- ∀x n. abs (x pow n) = abs x pow n
[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
[REAL_LE_INV2] Theorem
|- ∀x y. 0 < x ∧ x ≤ y ⇒ inv y ≤ inv x
[REAL_LE_LCANCEL_IMP] Theorem
|- ∀x y z. 0 < x ∧ x * y ≤ x * z ⇒ y ≤ z
[REAL_LE_RCANCEL_IMP] Theorem
|- ∀x y z. 0 < z ∧ x * z ≤ y * z ⇒ x ≤ y
[REAL_LT_LCANCEL_IMP] Theorem
|- ∀x y z. 0 < x ∧ x * y < x * z ⇒ y < z
[REAL_LT_RCANCEL_IMP] Theorem
|- ∀x y z. 0 < z ∧ x * z < y * z ⇒ x < y
[REAL_MUL_AC] Theorem
|- (m * n = n * m) ∧ (m * n * p = m * (n * p)) ∧
(m * (n * p) = n * (m * p))
[REAL_NEG_IN_BINADE] Theorem
|- ∀x.
normalizes x ∧ 0 ≤ -x ⇒
∃j.
j ≤ emax float_format − 2 ∧ 2 pow j / 2 pow 126 ≤ -x ∧
-x < 2 pow SUC j / 2 pow 126
[REAL_OF_NUM_LT] Theorem
|- ∀m n. &m < &n ⇔ m < n
[REAL_OF_NUM_POW] Theorem
|- ∀x n. &x pow n = &(x ** n)
[REAL_OF_NUM_SUB] Theorem
|- ∀m n. m ≤ n ⇒ (&n − &m = &(n − m))
[REAL_POS_IN_BINADE] Theorem
|- ∀x.
normalizes x ∧ 0 ≤ x ⇒
∃j.
j ≤ emax float_format − 2 ∧ 2 pow j / 2 pow 126 ≤ x ∧
x < 2 pow SUC j / 2 pow 126
[REAL_POW_EQ_0] Theorem
|- ∀x n. (x pow n = 0) ⇔ (x = 0) ∧ n ≠ 0
[REAL_POW_LE_1] Theorem
|- ∀n x. 1 ≤ x ⇒ 1 ≤ x pow n
[REAL_POW_MONO] Theorem
|- ∀m n x. 1 ≤ x ∧ m ≤ n ⇒ x pow m ≤ x pow n
[RELATIVE_ERROR] Theorem
|- ∀x.
normalizes x ⇒
∃e.
abs e ≤ 1 / 2 pow 24 ∧
(Val (float (round float_format To_nearest x)) = x * (1 + e))
[RELATIVE_ERROR_NEG] Theorem
|- ∀x.
normalizes x ∧ x < 0 ⇒
∃e.
abs e ≤ 1 / 2 pow 24 ∧
(Val (float (round float_format To_nearest x)) = x * (1 + e))
[RELATIVE_ERROR_POS] Theorem
|- ∀x.
normalizes x ∧ 0 < x ⇒
∃e.
abs e ≤ 1 / 2 pow 24 ∧
(Val (float (round float_format To_nearest x)) = x * (1 + e))
[RELATIVE_ERROR_ZERO] Theorem
|- ∀x.
normalizes x ∧ (x = 0) ⇒
∃e.
abs e ≤ 1 / 2 pow 24 ∧
(Val (float (round float_format To_nearest x)) = x * (1 + e))
[RRRC1] Theorem
|- 2 * 8388608 ≤ 2 pow 254 * (2 * 8388608 − 1)
[RRRC10] Theorem
|- 1 < 2 pow 254 − 2 pow 229
[RRRC11] Theorem
|- 340282356779733661637539395458142568448 * 2 pow 126 < 2 pow 254
[RRRC2] Theorem
|- 2 pow 103 * (2 pow 24 * 2) − 2 pow 103 ≤ 2 pow 128
[RRRC3] Theorem
|- 340282356779733661637539395458142568448 ≤ 2 pow 128
[RRRC4] Theorem
|- 2 pow 128 − 2 pow 103 = 340282356779733661637539395458142568448
[RRRC5] Theorem
|- inv 1 < 2 pow 103 * (2 pow 24 * 2) − 2 pow 103
[RRRC6] Theorem
|- 0 < 2 pow 150
[RRRC7] Theorem
|- 2 pow 254 − 2 pow 229 < 2 pow 254
[RRRC8] Theorem
|- 2 pow 103 * (2 pow 24 * 2) − 2 pow 103 =
340282356779733661637539395458142568448
[RRRC9] Theorem
|- 2 pow 127 * 2 − 2 pow 104 <
340282356779733661637539395458142568448
[SIGN] Theorem
|- ∀a. sign a = FST a
[THRESHOLD_LT_POW_INV] Theorem
|- 340282356779733661637539395458142568448 <
2 pow 254 * inv (2 pow 126)
[THRESHOLD_MUL_LT] Theorem
|- threshold float_format * 2 pow 126 < 2 pow 2 ** 126
[TWO_EXP_GE_1] Theorem
|- ∀n. 1 ≤ 2 ** n
[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)
[VALOF_SCALE_DOWN] Theorem
|- ∀s e k f.
k < e ⇒
(valof float_format (s,e − k,f) =
inv (2 pow k) * valof float_format (s,e,f))
[VALOF_SCALE_UP] Theorem
|- ∀s e k f.
e ≠ 0 ⇒
(valof float_format (s,e + k,f) =
2 pow k * valof float_format (s,e,f))
[VAL_FINITE] Theorem
|- ∀a. Finite a ⇒ abs (Val a) ≤ largest float_format
[VAL_THRESHOLD] Theorem
|- ∀a. Finite a ⇒ abs (Val a) < threshold float_format
[Val_FLOAT_ROUND_VALOF] Theorem
|- ∀x.
Val (float (round float_format To_nearest x)) =
valof float_format (round float_format To_nearest x)
[ZERO_IS_ZERO] Theorem
|- Iszero Plus_zero ∧ Iszero Minus_zero
[ZERO_NOT_NAN] Theorem
|- ¬Isnan Plus_zero ∧ ¬Isnan Minus_zero
[egt1] Theorem
|- 1 < 8
[egtff] Theorem
|- 8 = 4 + 4
[ftt] Theorem
|- 4 = 2 + 2
[inv23gt0] Theorem
|- 0 < inv (2 pow 23)
[lt1eqmul] Theorem
|- x < 1 ⇔ x * 8388608 < 8388608
[not2eqz] Theorem
|- 2 ≠ 0
[noteteeszegtz] Theorem
|- 0 < 8388608
[sucminmullt] Theorem
|- (2 pow SUC 127 − 2 pow 103) * 2 pow 126 < 2 pow 255
[temonz] Theorem
|- 2 ** 8 − 1 ≠ 0
[tfflttfs] Theorem
|- 255 < 256
[tittfittt] Theorem
|- 2 * inv (2 pow 24) = inv (2 pow 23)
[tpetfs] Theorem
|- 2 pow 8 = 256
[tptteteesze] Theorem
|- 2 pow 23 = 8388608
[tteettto] Theorem
|- 23 = 8 + 8 + 2 + 2 + 2 + 1
[ttpinv] Theorem
|- 2 * 2 pow 127 * inv (2 pow 127) = 2
[twogz] Theorem
|- ∀n. 0 < 2 pow n
[v127not0] Theorem
|- 2 pow 127 ≠ 0
[v23not0] Theorem
|- 2 pow 23 ≠ 0
*)
end
HOL 4, Kananaskis-10