Structure binary_ieeeTheory
signature binary_ieeeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ULP_primitive_def : thm
val check_for_signalling_def : thm
val clear_flags_def : thm
val closest_def : thm
val closest_such_def : thm
val dividezero_flags_def : thm
val exponent_boundary_def : thm
val flags_DivideByZero : thm
val flags_DivideByZero_fupd : thm
val flags_InvalidOp : thm
val flags_InvalidOp_fupd : thm
val flags_Overflow : thm
val flags_Overflow_fupd : thm
val flags_Precision : thm
val flags_Precision_fupd : thm
val flags_TY_DEF : thm
val flags_Underflow_AfterRounding : thm
val flags_Underflow_AfterRounding_fupd : thm
val flags_Underflow_BeforeRounding : thm
val flags_Underflow_BeforeRounding_fupd : thm
val flags_case_def : thm
val flags_size_def : thm
val float_Exponent : thm
val float_Exponent_fupd : thm
val float_Sign : thm
val float_Sign_fupd : thm
val float_Significand : thm
val float_Significand_fupd : thm
val float_TY_DEF : thm
val float_abs_def : thm
val float_add_def : thm
val float_bottom_def : thm
val float_case_def : thm
val float_compare_BIJ : thm
val float_compare_CASE : thm
val float_compare_TY_DEF : thm
val float_compare_def : thm
val float_compare_size_def : thm
val float_div_def : thm
val float_equal_def : thm
val float_greater_equal_def : thm
val float_greater_than_def : thm
val float_is_finite_def : thm
val float_is_infinite_def : thm
val float_is_integral_def : thm
val float_is_nan_def : thm
val float_is_normal_def : thm
val float_is_signalling_def : thm
val float_is_subnormal_def : thm
val float_is_zero_def : thm
val float_less_equal_def : thm
val float_less_than_def : thm
val float_minus_infinity_def : thm
val float_minus_min_def : thm
val float_minus_zero_def : thm
val float_mul_add_def : thm
val float_mul_def : thm
val float_mul_sub_def : thm
val float_negate_def : thm
val float_plus_infinity_def : thm
val float_plus_min_def : thm
val float_plus_zero_def : thm
val float_round_def : thm
val float_round_to_integral_def : thm
val float_round_with_flags_def : thm
val float_size_def : thm
val float_some_qnan_def : thm
val float_sqrt_def : thm
val float_sub_def : thm
val float_to_int_def : thm
val float_to_real_def : thm
val float_top_def : thm
val float_value_TY_DEF : thm
val float_value_case_def : thm
val float_value_def : thm
val float_value_size_def : thm
val fp_op_TY_DEF : thm
val fp_op_case_def : thm
val fp_op_size_def : thm
val integral_round_def : thm
val invalidop_flags_def : thm
val is_closest_def : thm
val is_integral_def : thm
val largest_def : thm
val real_to_float_def : thm
val real_to_float_with_flags_def : thm
val round_def : thm
val rounding_BIJ : thm
val rounding_CASE : thm
val rounding_TY_DEF : thm
val rounding_size_def : thm
val threshold_def : thm
val ulp_def : thm
(* Theorems *)
val EXISTS_flags : thm
val EXISTS_float : thm
val FORALL_flags : thm
val FORALL_float : thm
val ULP_def : thm
val ULP_ind : thm
val ULP_le_mono : thm
val abs_float_value : thm
val bottom_properties : thm
val datatype_flags : thm
val datatype_float : thm
val datatype_float_compare : thm
val datatype_float_value : thm
val datatype_fp_op : thm
val datatype_rounding : thm
val diff_float_ULP : thm
val diff_lt_ulp_eq0 : thm
val diff_lt_ulp_even : thm
val diff_lt_ulp_even4 : thm
val div_eq0 : thm
val exp_ge2 : thm
val exp_gt2 : thm
val flags_11 : thm
val flags_Axiom : thm
val flags_accessors : thm
val flags_accfupds : thm
val flags_case_cong : thm
val flags_case_eq : thm
val flags_component_equality : thm
val flags_fn_updates : thm
val flags_fupdcanon : thm
val flags_fupdcanon_comp : thm
val flags_fupdfupds : thm
val flags_fupdfupds_comp : thm
val flags_induction : thm
val flags_literal_11 : thm
val flags_literal_nchotomy : thm
val flags_nchotomy : thm
val flags_updates_eq_literal : thm
val float_11 : thm
val float_Axiom : thm
val float_accessors : thm
val float_accfupds : thm
val float_add_compute : thm
val float_add_finite : thm
val float_add_finite_minus_infinity : thm
val float_add_finite_plus_infinity : thm
val float_add_minus_infinity_finite : thm
val float_add_nan : thm
val float_add_plus_infinity_finite : thm
val float_case_cong : thm
val float_case_eq : thm
val float_cases : thm
val float_cases_finite : thm
val float_compare2num_11 : thm
val float_compare2num_ONTO : thm
val float_compare2num_num2float_compare : thm
val float_compare2num_thm : thm
val float_compare_Axiom : thm
val float_compare_EQ_float_compare : thm
val float_compare_case_cong : thm
val float_compare_case_def : thm
val float_compare_case_eq : thm
val float_compare_distinct : thm
val float_compare_induction : thm
val float_compare_nchotomy : thm
val float_component_equality : thm
val float_components : thm
val float_distinct : thm
val float_distinct_finite : thm
val float_div_compute : thm
val float_div_finite : thm
val float_div_finite_minus_infinity : thm
val float_div_finite_plus_infinity : thm
val float_div_minus_infinity_finite : thm
val float_div_nan : thm
val float_div_plus_infinity_finite : thm
val float_fn_updates : thm
val float_fupdcanon : thm
val float_fupdcanon_comp : thm
val float_fupdfupds : thm
val float_fupdfupds_comp : thm
val float_induction : thm
val float_infinities : thm
val float_infinities_distinct : thm
val float_infinity_negate_abs : thm
val float_is_distinct : thm
val float_is_finite : thm
val float_is_zero : thm
val float_is_zero_to_real : thm
val float_literal_11 : thm
val float_literal_nchotomy : thm
val float_minus_infinity : thm
val float_minus_zero : thm
val float_mul_compute : thm
val float_mul_finite : thm
val float_mul_finite_minus_infinity : thm
val float_mul_finite_plus_infinity : thm
val float_mul_minus_infinity_finite : thm
val float_mul_nan : thm
val float_mul_plus_infinity_finite : thm
val float_nchotomy : thm
val float_negate_negate : thm
val float_round_bottom : thm
val float_round_minus_infinity : thm
val float_round_non_zero : thm
val float_round_plus_infinity : thm
val float_round_roundTowardNegative_minus_infinity : thm
val float_round_roundTowardNegative_top : thm
val float_round_roundTowardPositive_bottom : thm
val float_round_roundTowardPositive_plus_infinity : thm
val float_round_roundTowardZero_bottom : thm
val float_round_roundTowardZero_top : thm
val float_round_to_integral_compute : thm
val float_round_top : thm
val float_sets : thm
val float_sub_compute : thm
val float_sub_finite : thm
val float_sub_finite_minus_infinity : thm
val float_sub_finite_plus_infinity : thm
val float_sub_minus_infinity_finite : thm
val float_sub_nan : thm
val float_sub_plus_infinity_finite : thm
val float_tests : thm
val float_to_real : thm
val float_to_real_eq : thm
val float_to_real_negate : thm
val float_updates_eq_literal : thm
val float_value_11 : thm
val float_value_Axiom : thm
val float_value_case_cong : thm
val float_value_case_eq : thm
val float_value_distinct : thm
val float_value_induction : thm
val float_value_nchotomy : thm
val float_values : thm
val fp_op_11 : thm
val fp_op_Axiom : thm
val fp_op_case_cong : thm
val fp_op_case_eq : thm
val fp_op_distinct : thm
val fp_op_induction : thm
val fp_op_nchotomy : thm
val infinity_properties : thm
val largest : thm
val largest_is_positive : thm
val largest_is_top : thm
val largest_lt_threshold : thm
val le2 : thm
val less_than_ulp : thm
val min_properties : thm
val neg_ulp : thm
val num2float_compare_11 : thm
val num2float_compare_ONTO : thm
val num2float_compare_float_compare2num : thm
val num2float_compare_thm : thm
val num2rounding_11 : thm
val num2rounding_ONTO : thm
val num2rounding_rounding2num : thm
val num2rounding_thm : thm
val round_roundTiesToEven : thm
val round_roundTiesToEven0 : thm
val round_roundTiesToEven_is_minus_zero : thm
val round_roundTiesToEven_is_plus_zero : thm
val round_roundTiesToEven_is_zero : thm
val round_roundTiesToEven_minus_infinity : thm
val round_roundTiesToEven_plus_infinity : thm
val round_roundTowardNegative_minus_infinity : thm
val round_roundTowardNegative_top : thm
val round_roundTowardPositive_bottom : thm
val round_roundTowardPositive_plus_infinity : thm
val round_roundTowardZero : thm
val round_roundTowardZero_bottom : thm
val round_roundTowardZero_is_minus_zero : thm
val round_roundTowardZero_is_plus_zero : thm
val round_roundTowardZero_is_zero : thm
val round_roundTowardZero_top : thm
val rounding2num_11 : thm
val rounding2num_ONTO : thm
val rounding2num_num2rounding : thm
val rounding2num_thm : thm
val rounding_Axiom : thm
val rounding_EQ_rounding : thm
val rounding_case_cong : thm
val rounding_case_def : thm
val rounding_case_eq : thm
val rounding_distinct : thm
val rounding_induction : thm
val rounding_nchotomy : thm
val sign_not_zero : thm
val some_nan_properties : thm
val threshold : thm
val threshold_is_positive : thm
val top_properties : thm
val ulp : thm
val ulp_lt_ULP : thm
val ulp_lt_largest : thm
val ulp_lt_threshold : thm
val zero_le_pos_div_twopow : thm
val zero_le_twopow : thm
val zero_lt_twopow : thm
val zero_neq_twopow : thm
val zero_properties : thm
val zero_to_real : thm
val binary_ieee_grammars : type_grammar.grammar * term_grammar.grammar
(*
[intreal] Parent theory of "binary_ieee"
[transc] Parent theory of "binary_ieee"
[words] Parent theory of "binary_ieee"
[ULP_primitive_def] Definition
⊢ ULP =
WFREC (@R. WF R)
(λULP a.
case a of
(v,v1) =>
I
(2 pow (if v = 0w then 1 else w2n v) /
2 pow (bias (:χ) + precision (:τ))))
[check_for_signalling_def] Definition
⊢ ∀l. check_for_signalling l =
clear_flags with InvalidOp := EXISTS float_is_signalling l
[clear_flags_def] Definition
⊢ clear_flags =
<|DivideByZero := F; InvalidOp := F; Overflow := F; Precision := F;
Underflow_BeforeRounding := F; Underflow_AfterRounding := F|>
[closest_def] Definition
⊢ closest = closest_such (K T)
[closest_such_def] Definition
⊢ ∀p s x.
closest_such p s x =
@a. is_closest s x a ∧ ∀b. is_closest s x b ∧ p b ⇒ p a
[dividezero_flags_def] Definition
⊢ dividezero_flags = clear_flags with DivideByZero := T
[exponent_boundary_def] Definition
⊢ ∀y x.
exponent_boundary y x ⇔
(x.Sign = y.Sign) ∧ (w2n x.Exponent = w2n y.Exponent + 1) ∧
x.Exponent ≠ 1w ∧ (y.Significand = -1w) ∧ (x.Significand = 0w)
[flags_DivideByZero] Definition
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b
[flags_DivideByZero_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
flags (f b) b0 b1 b2 b3 b4
[flags_InvalidOp] Definition
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0
[flags_InvalidOp_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
flags b (f b0) b1 b2 b3 b4
[flags_Overflow] Definition
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1
[flags_Overflow_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
flags b b0 (f b1) b2 b3 b4
[flags_Precision] Definition
⊢ ∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2
[flags_Precision_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Precision updated_by f =
flags b b0 b1 (f b2) b3 b4
[flags_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('flags').
(∀a0'.
(∃a0 a1 a2 a3 a4 a5.
a0' =
(λa0 a1 a2 a3 a4 a5.
ind_type$CONSTR 0 (a0,a1,a2,a3,a4,a5)
(λn. ind_type$BOTTOM)) a0 a1 a2 a3 a4 a5) ⇒
$var$('flags') a0') ⇒
$var$('flags') a0') rep
[flags_Underflow_AfterRounding] Definition
⊢ ∀b b0 b1 b2 b3 b4.
(flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
[flags_Underflow_AfterRounding_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
flags b b0 b1 b2 b3 (f b4)
[flags_Underflow_BeforeRounding] Definition
⊢ ∀b b0 b1 b2 b3 b4.
(flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3
[flags_Underflow_BeforeRounding_fupd] Definition
⊢ ∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Underflow_BeforeRounding updated_by f =
flags b b0 b1 b2 (f b3) b4
[flags_case_def] Definition
⊢ ∀a0 a1 a2 a3 a4 a5 f.
flags_CASE (flags a0 a1 a2 a3 a4 a5) f = f a0 a1 a2 a3 a4 a5
[flags_size_def] Definition
⊢ ∀a0 a1 a2 a3 a4 a5.
flags_size (flags a0 a1 a2 a3 a4 a5) =
1 +
(bool_size a0 +
(bool_size a1 +
(bool_size a2 + (bool_size a3 + (bool_size a4 + bool_size a5)))))
[float_Exponent] Definition
⊢ ∀c c0 c1. (float c c0 c1).Exponent = c0
[float_Exponent_fupd] Definition
⊢ ∀f c c0 c1.
float c c0 c1 with Exponent updated_by f = float c (f c0) c1
[float_Sign] Definition
⊢ ∀c c0 c1. (float c c0 c1).Sign = c
[float_Sign_fupd] Definition
⊢ ∀f c c0 c1.
float c c0 c1 with Sign updated_by f = float (f c) c0 c1
[float_Significand] Definition
⊢ ∀c c0 c1. (float c c0 c1).Significand = c1
[float_Significand_fupd] Definition
⊢ ∀f c c0 c1.
float c c0 c1 with Significand updated_by f = float c c0 (f c1)
[float_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('float').
(∀a0'.
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR 0 (a0,a1,a2)
(λn. ind_type$BOTTOM)) a0 a1 a2) ⇒
$var$('float') a0') ⇒
$var$('float') a0') rep
[float_abs_def] Definition
⊢ ∀x. float_abs x = x with Sign := 0w
[float_add_def] Definition
⊢ ∀mode x y.
float_add mode x y =
case (float_value x,float_value y) of
(Float r1,Float r2) =>
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ (x.Sign = y.Sign) then
x.Sign = 1w
else (mode = roundTowardNegative)) (r1 + r2)
| (Float r1,Infinity) => (clear_flags,y)
| (Float r1,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Add mode x y))
| (Infinity,Float v7) => (clear_flags,x)
| (Infinity,Infinity) =>
if x.Sign = y.Sign then (clear_flags,x)
else (invalidop_flags,float_some_qnan (FP_Add mode x y))
| (Infinity,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Add mode x y))
| (NaN,v1) =>
(check_for_signalling [x; y],float_some_qnan (FP_Add mode x y))
[float_bottom_def] Definition
⊢ float_bottom (:τ # χ) = float_negate (float_top (:τ # χ))
[float_case_def] Definition
⊢ ∀a0 a1 a2 f. float_CASE (float a0 a1 a2) f = f a0 a1 a2
[float_compare_BIJ] Definition
⊢ (∀a. num2float_compare (float_compare2num a) = a) ∧
∀r. (λn. n < 4) r ⇔ (float_compare2num (num2float_compare r) = r)
[float_compare_CASE] Definition
⊢ ∀x v0 v1 v2 v3.
(case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
(λm.
if m < 1 then v0
else if m < 2 then v1
else if m = 2 then v2
else v3) (float_compare2num x)
[float_compare_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
[float_compare_def] Definition
⊢ ∀x y.
float_compare x y =
case (float_value x,float_value y) of
(Float r1,Float r2) =>
if r1 < r2 then LT else if r1 = r2 then EQ else GT
| (Float r1,Infinity) => if y.Sign = 1w then GT else LT
| (Float r1,NaN) => UN
| (Infinity,Float v7) => if x.Sign = 1w then LT else GT
| (Infinity,Infinity) =>
if x.Sign = y.Sign then EQ else if x.Sign = 1w then LT else GT
| (Infinity,NaN) => UN
| (NaN,v1) => UN
[float_compare_size_def] Definition
⊢ ∀x. float_compare_size x = 0
[float_div_def] Definition
⊢ ∀mode x y.
float_div mode x y =
case (float_value x,float_value y) of
(Float 0,Float 0) =>
(invalidop_flags,float_some_qnan (FP_Div mode x y))
| (Float r1,Float 0) =>
(dividezero_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
| (Float r1,Float r2) =>
float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2)
| (Float r1,Infinity) =>
(clear_flags,
if x.Sign = y.Sign then float_plus_zero (:τ # χ)
else float_minus_zero (:τ # χ))
| (Float r1,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Div mode x y))
| (Infinity,Float v7) =>
(clear_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
| (Infinity,Infinity) =>
(invalidop_flags,float_some_qnan (FP_Div mode x y))
| (Infinity,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Div mode x y))
| (NaN,v1) =>
(check_for_signalling [x; y],float_some_qnan (FP_Div mode x y))
[float_equal_def] Definition
⊢ ∀x y. float_equal x y ⇔ (float_compare x y = EQ)
[float_greater_equal_def] Definition
⊢ ∀x y.
float_greater_equal x y ⇔
case float_compare x y of LT => F | EQ => T | GT => T | UN => F
[float_greater_than_def] Definition
⊢ ∀x y. float_greater_than x y ⇔ (float_compare x y = GT)
[float_is_finite_def] Definition
⊢ ∀x. float_is_finite x ⇔
case float_value x of Float v1 => T | Infinity => F | NaN => F
[float_is_infinite_def] Definition
⊢ ∀x. float_is_infinite x ⇔
case float_value x of Float v1 => F | Infinity => T | NaN => F
[float_is_integral_def] Definition
⊢ ∀x. float_is_integral x ⇔
case float_value x of
Float r => is_integral r
| Infinity => F
| NaN => F
[float_is_nan_def] Definition
⊢ ∀x. float_is_nan x ⇔
case float_value x of Float v1 => F | Infinity => F | NaN => T
[float_is_normal_def] Definition
⊢ ∀x. float_is_normal x ⇔ x.Exponent ≠ 0w ∧ x.Exponent ≠ UINT_MAXw
[float_is_signalling_def] Definition
⊢ ∀x. float_is_signalling x ⇔
float_is_nan x ∧ ¬word_msb x.Significand
[float_is_subnormal_def] Definition
⊢ ∀x. float_is_subnormal x ⇔ (x.Exponent = 0w) ∧ x.Significand ≠ 0w
[float_is_zero_def] Definition
⊢ ∀x. float_is_zero x ⇔
case float_value x of
Float r => r = 0
| Infinity => F
| NaN => F
[float_less_equal_def] Definition
⊢ ∀x y.
float_less_equal x y ⇔
case float_compare x y of LT => T | EQ => T | GT => F | UN => F
[float_less_than_def] Definition
⊢ ∀x y. float_less_than x y ⇔ (float_compare x y = LT)
[float_minus_infinity_def] Definition
⊢ float_minus_infinity (:τ # χ) =
float_negate (float_plus_infinity (:τ # χ))
[float_minus_min_def] Definition
⊢ float_minus_min (:τ # χ) = float_negate (float_plus_min (:τ # χ))
[float_minus_zero_def] Definition
⊢ float_minus_zero (:τ # χ) = float_negate (float_plus_zero (:τ # χ))
[float_mul_add_def] Definition
⊢ ∀mode x y z.
float_mul_add mode x y z =
(let
signP = x.Sign ⊕ y.Sign;
infP = float_is_infinite x ∨ float_is_infinite y
in
if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
(check_for_signalling [x; y; z],
float_some_qnan (FP_MulAdd mode x y z))
else if
float_is_infinite x ∧ float_is_zero y ∨
float_is_zero x ∧ float_is_infinite y ∨
float_is_infinite z ∧ infP ∧ signP ≠ z.Sign
then
(invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
else if
float_is_infinite z ∧ (z.Sign = 0w) ∨ infP ∧ (signP = 0w)
then
(clear_flags,float_plus_infinity (:τ # χ))
else if
float_is_infinite z ∧ (z.Sign = 1w) ∨ infP ∧ (signP = 1w)
then
(clear_flags,float_minus_infinity (:τ # χ))
else
(let
r1 = float_to_real x * float_to_real y and
r2 = float_to_real z
in
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ (signP = z.Sign) then
signP = 1w
else (mode = roundTowardNegative)) (r1 + r2)))
[float_mul_def] Definition
⊢ ∀mode x y.
float_mul mode x y =
case (float_value x,float_value y) of
(Float r',Float r2) =>
float_round_with_flags mode (x.Sign ≠ y.Sign) (r' * r2)
| (Float 0,Infinity) =>
(invalidop_flags,float_some_qnan (FP_Mul mode x y))
| (Float r',Infinity) =>
(clear_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
| (Float r',NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
| (Infinity,Float 0) =>
(invalidop_flags,float_some_qnan (FP_Mul mode x y))
| (Infinity,Float r) =>
(clear_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
| (Infinity,Infinity) =>
(clear_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
| (Infinity,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Mul mode x y))
| (NaN,v1) =>
(check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y))
[float_mul_sub_def] Definition
⊢ ∀mode x y z.
float_mul_sub mode x y z =
(let
signP = x.Sign ⊕ y.Sign;
infP = float_is_infinite x ∨ float_is_infinite y
in
if float_is_nan x ∨ float_is_nan y ∨ float_is_nan z then
(check_for_signalling [x; y; z],
float_some_qnan (FP_MulSub mode x y z))
else if
float_is_infinite x ∧ float_is_zero y ∨
float_is_zero x ∧ float_is_infinite y ∨
float_is_infinite z ∧ infP ∧ (signP = z.Sign)
then
(invalidop_flags,float_some_qnan (FP_MulAdd mode x y z))
else if
float_is_infinite z ∧ (z.Sign = 1w) ∨ infP ∧ (signP = 0w)
then
(clear_flags,float_plus_infinity (:τ # χ))
else if
float_is_infinite z ∧ (z.Sign = 0w) ∨ infP ∧ (signP = 1w)
then
(clear_flags,float_minus_infinity (:τ # χ))
else
(let
r1 = float_to_real x * float_to_real y and
r2 = float_to_real z
in
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ signP ≠ z.Sign then
signP = 1w
else (mode = roundTowardNegative)) (r1 − r2)))
[float_negate_def] Definition
⊢ ∀x. float_negate x = x with Sign := ¬x.Sign
[float_plus_infinity_def] Definition
⊢ float_plus_infinity (:τ # χ) =
<|Sign := 0w; Exponent := UINT_MAXw; Significand := 0w|>
[float_plus_min_def] Definition
⊢ float_plus_min (:τ # χ) =
<|Sign := 0w; Exponent := 0w; Significand := 1w|>
[float_plus_zero_def] Definition
⊢ float_plus_zero (:τ # χ) =
<|Sign := 0w; Exponent := 0w; Significand := 0w|>
[float_round_def] Definition
⊢ ∀mode toneg r.
float_round mode toneg r =
(let
x = round mode r
in
if float_is_zero x then
if toneg then float_minus_zero (:τ # χ)
else float_plus_zero (:τ # χ)
else x)
[float_round_to_integral_def] Definition
⊢ ∀mode x.
float_round_to_integral mode x =
case float_value x of
Float r => integral_round mode r
| Infinity => x
| NaN => x
[float_round_with_flags_def] Definition
⊢ ∀mode to_neg r.
float_round_with_flags mode to_neg r =
(let
x = float_round mode to_neg r and a = abs r;
inexact = float_value x ≠ Float r
in
(clear_flags with
<|Overflow := (float_is_infinite x ∨ 2 pow INT_MIN (:χ) ≤ a);
Underflow_BeforeRounding :=
(inexact ∧ a < 2 / 2 pow bias (:χ));
Underflow_AfterRounding :=
(inexact ∧
(float_round mode to_neg r).Exponent ≤₊
n2w (INT_MIN (:χ))); Precision := inexact|>,x))
[float_size_def] Definition
⊢ ∀f f1 a0 a1 a2. float_size f f1 (float a0 a1 a2) = 1
[float_some_qnan_def] Definition
⊢ ∀fp_op.
float_some_qnan fp_op =
(@f. (let
qnan = f fp_op
in
float_is_nan qnan ∧ ¬float_is_signalling qnan)) fp_op
[float_sqrt_def] Definition
⊢ ∀mode x.
float_sqrt mode x =
if x.Sign = 0w then
case float_value x of
Float r => float_round_with_flags mode F (sqrt r)
| Infinity => (clear_flags,float_plus_infinity (:τ # χ))
| NaN =>
(check_for_signalling [x],float_some_qnan (FP_Sqrt mode x))
else (invalidop_flags,float_some_qnan (FP_Sqrt mode x))
[float_sub_def] Definition
⊢ ∀mode x y.
float_sub mode x y =
case (float_value x,float_value y) of
(Float r1,Float r2) =>
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ x.Sign ≠ y.Sign then x.Sign = 1w
else (mode = roundTowardNegative)) (r1 − r2)
| (Float r1,Infinity) => (clear_flags,float_negate y)
| (Float r1,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
| (Infinity,Float v7) => (clear_flags,x)
| (Infinity,Infinity) =>
if x.Sign = y.Sign then
(invalidop_flags,float_some_qnan (FP_Sub mode x y))
else (clear_flags,x)
| (Infinity,NaN) =>
(check_for_signalling [y],float_some_qnan (FP_Sub mode x y))
| (NaN,v1) =>
(check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y))
[float_to_int_def] Definition
⊢ ∀mode x.
float_to_int mode x =
case float_value x of
Float r =>
SOME
(case mode of
roundTiesToEven =>
(let
f = flr r;
df = abs (r − real_of_int f)
in
if
df < 1 / 2 ∨ (df = 1 / 2) ∧ EVEN (Num (ABS f))
then
f
else clg r)
| roundTowardPositive => clg r
| roundTowardNegative => flr r
| roundTowardZero => if x.Sign = 1w then clg r else flr r)
| Infinity => NONE
| NaN => NONE
[float_to_real_def] Definition
⊢ ∀x. float_to_real x =
if x.Exponent = 0w then
-1 pow w2n x.Sign * (2 / 2 pow bias (:χ)) *
(&w2n x.Significand / 2 pow precision (:τ))
else
-1 pow w2n x.Sign *
(2 pow w2n x.Exponent / 2 pow bias (:χ)) *
(1 + &w2n x.Significand / 2 pow precision (:τ))
[float_top_def] Definition
⊢ float_top (:τ # χ) =
<|Sign := 0w; Exponent := UINT_MAXw − 1w;
Significand := UINT_MAXw|>
[float_value_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0.
∀ $var$('float_value').
(∀a0.
(∃a. a0 =
(λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
a) ∨
(a0 =
ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM)) ∨
(a0 =
ind_type$CONSTR (SUC (SUC 0)) ARB
(λn. ind_type$BOTTOM)) ⇒
$var$('float_value') a0) ⇒
$var$('float_value') a0) rep
[float_value_case_def] Definition
⊢ (∀a f v v1. float_value_CASE (Float a) f v v1 = f a) ∧
(∀f v v1. float_value_CASE Infinity f v v1 = v) ∧
∀f v v1. float_value_CASE NaN f v v1 = v1
[float_value_def] Definition
⊢ ∀x. float_value x =
if x.Exponent = UINT_MAXw then
if x.Significand = 0w then Infinity else NaN
else Float (float_to_real x)
[float_value_size_def] Definition
⊢ (∀a. float_value_size (Float a) = 1) ∧
(float_value_size Infinity = 0) ∧ (float_value_size NaN = 0)
[fp_op_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('fp_op').
(∀a0'.
(∃a0 a1.
a0' =
(λa0 a1.
ind_type$CONSTR 0 (a0,a1,ARB,ARB)
(λn. ind_type$BOTTOM)) a0 a1) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC 0) (a0,a1,a2,ARB)
(λn. ind_type$BOTTOM)) a0 a1 a2) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC (SUC 0)) (a0,a1,a2,ARB)
(λn. ind_type$BOTTOM)) a0 a1 a2) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC (SUC (SUC 0)))
(a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
a2) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC (SUC (SUC (SUC 0))))
(a0,a1,a2,ARB) (λn. ind_type$BOTTOM)) a0 a1
a2) ∨
(∃a0 a1 a2 a3.
a0' =
(λa0 a1 a2 a3.
ind_type$CONSTR
(SUC (SUC (SUC (SUC (SUC 0)))))
(a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
a2 a3) ∨
(∃a0 a1 a2 a3.
a0' =
(λa0 a1 a2 a3.
ind_type$CONSTR
(SUC (SUC (SUC (SUC (SUC (SUC 0))))))
(a0,a1,a2,a3) (λn. ind_type$BOTTOM)) a0 a1
a2 a3) ⇒
$var$('fp_op') a0') ⇒
$var$('fp_op') a0') rep
[fp_op_case_def] Definition
⊢ (∀a0 a1 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_Sqrt a0 a1) f f1 f2 f3 f4 f5 f6 = f a0 a1) ∧
(∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_Add a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f1 a0 a1 a2) ∧
(∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_Sub a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f2 a0 a1 a2) ∧
(∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_Mul a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f3 a0 a1 a2) ∧
(∀a0 a1 a2 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_Div a0 a1 a2) f f1 f2 f3 f4 f5 f6 = f4 a0 a1 a2) ∧
(∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_MulAdd a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 =
f5 a0 a1 a2 a3) ∧
∀a0 a1 a2 a3 f f1 f2 f3 f4 f5 f6.
fp_op_CASE (FP_MulSub a0 a1 a2 a3) f f1 f2 f3 f4 f5 f6 =
f6 a0 a1 a2 a3
[fp_op_size_def] Definition
⊢ (∀f f1 a0 a1.
fp_op_size f f1 (FP_Sqrt a0 a1) =
1 + (rounding_size a0 + float_size f f1 a1)) ∧
(∀f f1 a0 a1 a2.
fp_op_size f f1 (FP_Add a0 a1 a2) =
1 +
(rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
(∀f f1 a0 a1 a2.
fp_op_size f f1 (FP_Sub a0 a1 a2) =
1 +
(rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
(∀f f1 a0 a1 a2.
fp_op_size f f1 (FP_Mul a0 a1 a2) =
1 +
(rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
(∀f f1 a0 a1 a2.
fp_op_size f f1 (FP_Div a0 a1 a2) =
1 +
(rounding_size a0 + (float_size f f1 a1 + float_size f f1 a2))) ∧
(∀f f1 a0 a1 a2 a3.
fp_op_size f f1 (FP_MulAdd a0 a1 a2 a3) =
1 +
(rounding_size a0 +
(float_size f f1 a1 +
(float_size f f1 a2 + float_size f f1 a3)))) ∧
∀f f1 a0 a1 a2 a3.
fp_op_size f f1 (FP_MulSub a0 a1 a2 a3) =
1 +
(rounding_size a0 +
(float_size f f1 a1 + (float_size f f1 a2 + float_size f f1 a3)))
[integral_round_def] Definition
⊢ ∀mode x.
integral_round mode x =
case mode of
roundTiesToEven =>
(let
t = threshold (:τ # χ)
in
if x ≤ -t then float_minus_infinity (:τ # χ)
else if x ≥ t then float_plus_infinity (:τ # χ)
else
closest_such
(λa. ∃n. EVEN n ∧ (abs (float_to_real a) = &n))
float_is_integral x)
| roundTowardPositive =>
(let
t = largest (:τ # χ)
in
if x < -t then float_bottom (:τ # χ)
else if x > t then float_plus_infinity (:τ # χ)
else
closest {a | float_is_integral a ∧ float_to_real a ≥ x} x)
| roundTowardNegative =>
(let
t = largest (:τ # χ)
in
if x < -t then float_minus_infinity (:τ # χ)
else if x > t then float_top (:τ # χ)
else
closest {a | float_is_integral a ∧ float_to_real a ≤ x} x)
| roundTowardZero =>
(let
t = largest (:τ # χ)
in
if x < -t then float_bottom (:τ # χ)
else if x > t then float_top (:τ # χ)
else
closest
{a | float_is_integral a ∧ abs (float_to_real a) ≤ abs x}
x)
[invalidop_flags_def] Definition
⊢ invalidop_flags = clear_flags with InvalidOp := T
[is_closest_def] Definition
⊢ ∀s x a.
is_closest s x a ⇔
a ∈ s ∧
∀b. b ∈ s ⇒ abs (float_to_real a − x) ≤ abs (float_to_real b − x)
[is_integral_def] Definition
⊢ ∀r. is_integral r ⇔ ∃n. abs r = &n
[largest_def] Definition
⊢ largest (:τ # χ) =
2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
(2 − (2 pow precision (:τ))⁻¹)
[real_to_float_def] Definition
⊢ ∀m. real_to_float m = float_round m (m = roundTowardNegative)
[real_to_float_with_flags_def] Definition
⊢ ∀m. real_to_float_with_flags m =
float_round_with_flags m (m = roundTowardNegative)
[round_def] Definition
⊢ ∀mode x.
round mode x =
case mode of
roundTiesToEven =>
(let
t = threshold (:τ # χ)
in
if x ≤ -t then float_minus_infinity (:τ # χ)
else if x ≥ t then float_plus_infinity (:τ # χ)
else
closest_such (λa. ¬word_lsb a.Significand)
float_is_finite x)
| roundTowardPositive =>
(let
t = largest (:τ # χ)
in
if x < -t then float_bottom (:τ # χ)
else if x > t then float_plus_infinity (:τ # χ)
else closest {a | float_is_finite a ∧ float_to_real a ≥ x} x)
| roundTowardNegative =>
(let
t = largest (:τ # χ)
in
if x < -t then float_minus_infinity (:τ # χ)
else if x > t then float_top (:τ # χ)
else closest {a | float_is_finite a ∧ float_to_real a ≤ x} x)
| roundTowardZero =>
(let
t = largest (:τ # χ)
in
if x < -t then float_bottom (:τ # χ)
else if x > t then float_top (:τ # χ)
else
closest
{a | float_is_finite a ∧ abs (float_to_real a) ≤ abs x}
x)
[rounding_BIJ] Definition
⊢ (∀a. num2rounding (rounding2num a) = a) ∧
∀r. (λn. n < 4) r ⇔ (rounding2num (num2rounding r) = r)
[rounding_CASE] Definition
⊢ ∀x v0 v1 v2 v3.
(case x of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) =
(λm.
if m < 1 then v0
else if m < 2 then v1
else if m = 2 then v2
else v3) (rounding2num x)
[rounding_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION (λn. n < 4) rep
[rounding_size_def] Definition
⊢ ∀x. rounding_size x = 0
[threshold_def] Definition
⊢ threshold (:τ # χ) =
2 pow (UINT_MAX (:χ) − 1) / 2 pow bias (:χ) *
(2 − (2 pow SUC (precision (:τ)))⁻¹)
[ulp_def] Definition
⊢ ulp (:τ # χ) = ULP (0w,(:τ))
[EXISTS_flags] Theorem
⊢ ∀P. (∃f. P f) ⇔
∃b4 b3 b2 b1 b0 b.
P
<|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
Precision := b1; Underflow_BeforeRounding := b0;
Underflow_AfterRounding := b|>
[EXISTS_float] Theorem
⊢ ∀P. (∃f. P f) ⇔
∃c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
[FORALL_flags] Theorem
⊢ ∀P. (∀f. P f) ⇔
∀b4 b3 b2 b1 b0 b.
P
<|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
Precision := b1; Underflow_BeforeRounding := b0;
Underflow_AfterRounding := b|>
[FORALL_float] Theorem
⊢ ∀P. (∀f. P f) ⇔
∀c1 c0 c. P <|Sign := c1; Exponent := c0; Significand := c|>
[ULP_def] Theorem
⊢ ULP (e,(:τ)) =
2 pow (if e = 0w then 1 else w2n e) /
2 pow (bias (:χ) + precision (:τ))
[ULP_ind] Theorem
⊢ ∀P. (∀e. P (e,(:τ))) ⇒ ∀v v1. P (v,v1)
[ULP_le_mono] Theorem
⊢ ∀e1 e2. e2 ≠ 0w ⇒ (ULP (e1,(:τ)) ≤ ULP (e2,(:τ)) ⇔ e1 ≤₊ e2)
[abs_float_value] Theorem
⊢ (∀b c d. abs (-1 pow w2n b * c * d) = abs (c * d)) ∧
∀b c. abs (-1 pow w2n b * c) = abs c
[bottom_properties] Theorem
⊢ ¬float_is_zero (float_bottom (:τ # χ)) ∧
float_is_finite (float_bottom (:τ # χ)) ∧
¬float_is_nan (float_bottom (:τ # χ)) ∧
(float_is_normal (float_bottom (:τ # χ)) ⇔ precision (:χ) ≠ 1) ∧
(float_is_subnormal (float_bottom (:τ # χ)) ⇔ (precision (:χ) = 1)) ∧
¬float_is_infinite (float_bottom (:τ # χ))
[datatype_flags] Theorem
⊢ DATATYPE
(record flags DivideByZero InvalidOp Overflow Precision
Underflow_BeforeRounding Underflow_AfterRounding)
[datatype_float] Theorem
⊢ DATATYPE (record float Sign Exponent Significand)
[datatype_float_compare] Theorem
⊢ DATATYPE (float_compare LT EQ GT UN)
[datatype_float_value] Theorem
⊢ DATATYPE (float_value Float Infinity NaN)
[datatype_fp_op] Theorem
⊢ DATATYPE
(fp_op FP_Sqrt FP_Add FP_Sub FP_Mul FP_Div FP_MulAdd FP_MulSub)
[datatype_rounding] Theorem
⊢ DATATYPE
(rounding roundTiesToEven roundTowardPositive roundTowardNegative
roundTowardZero)
[diff_float_ULP] Theorem
⊢ ∀x y.
float_to_real x ≠ float_to_real y ∧ ¬exponent_boundary y x ⇒
ULP (x.Exponent,(:τ)) ≤ abs (float_to_real x − float_to_real y)
[diff_lt_ulp_eq0] Theorem
⊢ ∀a b x.
¬exponent_boundary b a ∧
abs (x − float_to_real a) < ULP (a.Exponent,(:τ)) ∧
abs (x − float_to_real b) < ULP (a.Exponent,(:τ)) ∧
abs (float_to_real a) ≤ abs x ∧ abs (float_to_real b) ≤ abs x ∧
¬float_is_zero a ⇒
(b = a)
[diff_lt_ulp_even] Theorem
⊢ ∀a b x.
¬exponent_boundary b a ∧
2 * abs (float_to_real a − x) < ULP (a.Exponent,(:τ)) ∧
2 * abs (float_to_real b − x) < ULP (a.Exponent,(:τ)) ∧
¬float_is_zero a ⇒
(b = a)
[diff_lt_ulp_even4] Theorem
⊢ ∀a b x.
¬exponent_boundary b a ∧
4 * abs (float_to_real a − x) ≤ ULP (a.Exponent,(:τ)) ∧
4 * abs (float_to_real b − x) ≤ ULP (a.Exponent,(:τ)) ∧
¬float_is_zero a ⇒
(b = a)
[div_eq0] Theorem
⊢ ∀a b. 0 < b ⇒ ((a / b = 0) ⇔ (a = 0))
[exp_ge2] Theorem
⊢ ∀b. 2 ≤ 2 ** b ⇔ 1 ≤ b
[exp_gt2] Theorem
⊢ ∀b. 2 < 2 ** b ⇔ 1 < b
[flags_11] Theorem
⊢ ∀a0 a1 a2 a3 a4 a5 a0' a1' a2' a3' a4' a5'.
(flags a0 a1 a2 a3 a4 a5 = flags a0' a1' a2' a3' a4' a5') ⇔
(a0 ⇔ a0') ∧ (a1 ⇔ a1') ∧ (a2 ⇔ a2') ∧ (a3 ⇔ a3') ∧ (a4 ⇔ a4') ∧
(a5 ⇔ a5')
[flags_Axiom] Theorem
⊢ ∀f. ∃fn. ∀a0 a1 a2 a3 a4 a5.
fn (flags a0 a1 a2 a3 a4 a5) = f a0 a1 a2 a3 a4 a5
[flags_accessors] Theorem
⊢ (∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).DivideByZero ⇔ b) ∧
(∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).InvalidOp ⇔ b0) ∧
(∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Overflow ⇔ b1) ∧
(∀b b0 b1 b2 b3 b4. (flags b b0 b1 b2 b3 b4).Precision ⇔ b2) ∧
(∀b b0 b1 b2 b3 b4.
(flags b b0 b1 b2 b3 b4).Underflow_BeforeRounding ⇔ b3) ∧
∀b b0 b1 b2 b3 b4.
(flags b b0 b1 b2 b3 b4).Underflow_AfterRounding ⇔ b4
[flags_accfupds] Theorem
⊢ (∀f0 f.
(f with InvalidOp updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
(∀f0 f.
(f with Overflow updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
(∀f0 f.
(f with Precision updated_by f0).DivideByZero ⇔ f.DivideByZero) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).DivideByZero ⇔
f.DivideByZero) ∧
(∀f0 f.
(f with Underflow_AfterRounding updated_by f0).DivideByZero ⇔
f.DivideByZero) ∧
(∀f0 f. (f with DivideByZero updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
(∀f0 f. (f with Overflow updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
(∀f0 f. (f with Precision updated_by f0).InvalidOp ⇔ f.InvalidOp) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).InvalidOp ⇔
f.InvalidOp) ∧
(∀f0 f.
(f with Underflow_AfterRounding updated_by f0).InvalidOp ⇔
f.InvalidOp) ∧
(∀f0 f. (f with DivideByZero updated_by f0).Overflow ⇔ f.Overflow) ∧
(∀f0 f. (f with InvalidOp updated_by f0).Overflow ⇔ f.Overflow) ∧
(∀f0 f. (f with Precision updated_by f0).Overflow ⇔ f.Overflow) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).Overflow ⇔
f.Overflow) ∧
(∀f0 f.
(f with Underflow_AfterRounding updated_by f0).Overflow ⇔
f.Overflow) ∧
(∀f0 f. (f with DivideByZero updated_by f0).Precision ⇔ f.Precision) ∧
(∀f0 f. (f with InvalidOp updated_by f0).Precision ⇔ f.Precision) ∧
(∀f0 f. (f with Overflow updated_by f0).Precision ⇔ f.Precision) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).Precision ⇔
f.Precision) ∧
(∀f0 f.
(f with Underflow_AfterRounding updated_by f0).Precision ⇔
f.Precision) ∧
(∀f0 f.
(f with DivideByZero updated_by f0).Underflow_BeforeRounding ⇔
f.Underflow_BeforeRounding) ∧
(∀f0 f.
(f with InvalidOp updated_by f0).Underflow_BeforeRounding ⇔
f.Underflow_BeforeRounding) ∧
(∀f0 f.
(f with Overflow updated_by f0).Underflow_BeforeRounding ⇔
f.Underflow_BeforeRounding) ∧
(∀f0 f.
(f with Precision updated_by f0).Underflow_BeforeRounding ⇔
f.Underflow_BeforeRounding) ∧
(∀f0 f.
(f with Underflow_AfterRounding updated_by f0).
Underflow_BeforeRounding ⇔ f.Underflow_BeforeRounding) ∧
(∀f0 f.
(f with DivideByZero updated_by f0).Underflow_AfterRounding ⇔
f.Underflow_AfterRounding) ∧
(∀f0 f.
(f with InvalidOp updated_by f0).Underflow_AfterRounding ⇔
f.Underflow_AfterRounding) ∧
(∀f0 f.
(f with Overflow updated_by f0).Underflow_AfterRounding ⇔
f.Underflow_AfterRounding) ∧
(∀f0 f.
(f with Precision updated_by f0).Underflow_AfterRounding ⇔
f.Underflow_AfterRounding) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).
Underflow_AfterRounding ⇔ f.Underflow_AfterRounding) ∧
(∀f0 f.
(f with DivideByZero updated_by f0).DivideByZero ⇔
f0 f.DivideByZero) ∧
(∀f0 f. (f with InvalidOp updated_by f0).InvalidOp ⇔ f0 f.InvalidOp) ∧
(∀f0 f. (f with Overflow updated_by f0).Overflow ⇔ f0 f.Overflow) ∧
(∀f0 f. (f with Precision updated_by f0).Precision ⇔ f0 f.Precision) ∧
(∀f0 f.
(f with Underflow_BeforeRounding updated_by f0).
Underflow_BeforeRounding ⇔ f0 f.Underflow_BeforeRounding) ∧
∀f0 f.
(f with Underflow_AfterRounding updated_by f0).
Underflow_AfterRounding ⇔ f0 f.Underflow_AfterRounding
[flags_case_cong] Theorem
⊢ ∀M M' f.
(M = M') ∧
(∀a0 a1 a2 a3 a4 a5.
(M' = flags a0 a1 a2 a3 a4 a5) ⇒
(f a0 a1 a2 a3 a4 a5 = f' a0 a1 a2 a3 a4 a5)) ⇒
(flags_CASE M f = flags_CASE M' f')
[flags_case_eq] Theorem
⊢ (flags_CASE x f = v) ⇔
∃b b0 b1 b2 b3 b4.
(x = flags b b0 b1 b2 b3 b4) ∧ (f b b0 b1 b2 b3 b4 = v)
[flags_component_equality] Theorem
⊢ ∀f1 f2.
(f1 = f2) ⇔
(f1.DivideByZero ⇔ f2.DivideByZero) ∧
(f1.InvalidOp ⇔ f2.InvalidOp) ∧ (f1.Overflow ⇔ f2.Overflow) ∧
(f1.Precision ⇔ f2.Precision) ∧
(f1.Underflow_BeforeRounding ⇔ f2.Underflow_BeforeRounding) ∧
(f1.Underflow_AfterRounding ⇔ f2.Underflow_AfterRounding)
[flags_fn_updates] Theorem
⊢ (∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with DivideByZero updated_by f =
flags (f b) b0 b1 b2 b3 b4) ∧
(∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with InvalidOp updated_by f =
flags b (f b0) b1 b2 b3 b4) ∧
(∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Overflow updated_by f =
flags b b0 (f b1) b2 b3 b4) ∧
(∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Precision updated_by f =
flags b b0 b1 (f b2) b3 b4) ∧
(∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with
Underflow_BeforeRounding updated_by f =
flags b b0 b1 b2 (f b3) b4) ∧
∀f b b0 b1 b2 b3 b4.
flags b b0 b1 b2 b3 b4 with Underflow_AfterRounding updated_by f =
flags b b0 b1 b2 b3 (f b4)
[flags_fupdcanon] Theorem
⊢ (∀g f0 f.
f with <|InvalidOp updated_by f0; DivideByZero updated_by g|> =
f with <|DivideByZero updated_by g; InvalidOp updated_by f0|>) ∧
(∀g f0 f.
f with <|Overflow updated_by f0; DivideByZero updated_by g|> =
f with <|DivideByZero updated_by g; Overflow updated_by f0|>) ∧
(∀g f0 f.
f with <|Overflow updated_by f0; InvalidOp updated_by g|> =
f with <|InvalidOp updated_by g; Overflow updated_by f0|>) ∧
(∀g f0 f.
f with <|Precision updated_by f0; DivideByZero updated_by g|> =
f with <|DivideByZero updated_by g; Precision updated_by f0|>) ∧
(∀g f0 f.
f with <|Precision updated_by f0; InvalidOp updated_by g|> =
f with <|InvalidOp updated_by g; Precision updated_by f0|>) ∧
(∀g f0 f.
f with <|Precision updated_by f0; Overflow updated_by g|> =
f with <|Overflow updated_by g; Precision updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_BeforeRounding updated_by f0;
DivideByZero updated_by g|> =
f with
<|DivideByZero updated_by g;
Underflow_BeforeRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_BeforeRounding updated_by f0;
InvalidOp updated_by g|> =
f with
<|InvalidOp updated_by g;
Underflow_BeforeRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_BeforeRounding updated_by f0;
Overflow updated_by g|> =
f with
<|Overflow updated_by g;
Underflow_BeforeRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_BeforeRounding updated_by f0;
Precision updated_by g|> =
f with
<|Precision updated_by g;
Underflow_BeforeRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0;
DivideByZero updated_by g|> =
f with
<|DivideByZero updated_by g;
Underflow_AfterRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0;
InvalidOp updated_by g|> =
f with
<|InvalidOp updated_by g;
Underflow_AfterRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0; Overflow updated_by g|> =
f with
<|Overflow updated_by g; Underflow_AfterRounding updated_by f0|>) ∧
(∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0;
Precision updated_by g|> =
f with
<|Precision updated_by g;
Underflow_AfterRounding updated_by f0|>) ∧
∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0;
Underflow_BeforeRounding updated_by g|> =
f with
<|Underflow_BeforeRounding updated_by g;
Underflow_AfterRounding updated_by f0|>
[flags_fupdcanon_comp] Theorem
⊢ ((∀g f0.
InvalidOp_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd g ∘ InvalidOp_fupd f0) ∧
∀h g f0.
InvalidOp_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd g ∘ InvalidOp_fupd f0 ∘ h) ∧
((∀g f0.
Overflow_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd g ∘ Overflow_fupd f0) ∧
∀h g f0.
Overflow_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
((∀g f0.
Overflow_fupd f0 ∘ InvalidOp_fupd g =
InvalidOp_fupd g ∘ Overflow_fupd f0) ∧
∀h g f0.
Overflow_fupd f0 ∘ InvalidOp_fupd g ∘ h =
InvalidOp_fupd g ∘ Overflow_fupd f0 ∘ h) ∧
((∀g f0.
Precision_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd g ∘ Precision_fupd f0) ∧
∀h g f0.
Precision_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd g ∘ Precision_fupd f0 ∘ h) ∧
((∀g f0.
Precision_fupd f0 ∘ InvalidOp_fupd g =
InvalidOp_fupd g ∘ Precision_fupd f0) ∧
∀h g f0.
Precision_fupd f0 ∘ InvalidOp_fupd g ∘ h =
InvalidOp_fupd g ∘ Precision_fupd f0 ∘ h) ∧
((∀g f0.
Precision_fupd f0 ∘ Overflow_fupd g =
Overflow_fupd g ∘ Precision_fupd f0) ∧
∀h g f0.
Precision_fupd f0 ∘ Overflow_fupd g ∘ h =
Overflow_fupd g ∘ Precision_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
∀h g f0.
Underflow_BeforeRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g =
InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
∀h g f0.
Underflow_BeforeRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
InvalidOp_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g =
Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
∀h g f0.
Underflow_BeforeRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
Overflow_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g =
Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0) ∧
∀h g f0.
Underflow_BeforeRounding_fupd f0 ∘ Precision_fupd g ∘ h =
Precision_fupd g ∘ Underflow_BeforeRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g =
InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘ InvalidOp_fupd g ∘ h =
InvalidOp_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g =
Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘ Overflow_fupd g ∘ h =
Overflow_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
((∀g f0.
Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g =
Precision_fupd g ∘ Underflow_AfterRounding_fupd f0) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘ Precision_fupd g ∘ h =
Precision_fupd g ∘ Underflow_AfterRounding_fupd f0 ∘ h) ∧
(∀g f0.
Underflow_AfterRounding_fupd f0 ∘
Underflow_BeforeRounding_fupd g =
Underflow_BeforeRounding_fupd g ∘
Underflow_AfterRounding_fupd f0) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘
Underflow_BeforeRounding_fupd g ∘ h =
Underflow_BeforeRounding_fupd g ∘
Underflow_AfterRounding_fupd f0 ∘ h
[flags_fupdfupds] Theorem
⊢ (∀g f0 f.
f with <|DivideByZero updated_by f0; DivideByZero updated_by g|> =
f with DivideByZero updated_by f0 ∘ g) ∧
(∀g f0 f.
f with <|InvalidOp updated_by f0; InvalidOp updated_by g|> =
f with InvalidOp updated_by f0 ∘ g) ∧
(∀g f0 f.
f with <|Overflow updated_by f0; Overflow updated_by g|> =
f with Overflow updated_by f0 ∘ g) ∧
(∀g f0 f.
f with <|Precision updated_by f0; Precision updated_by g|> =
f with Precision updated_by f0 ∘ g) ∧
(∀g f0 f.
f with
<|Underflow_BeforeRounding updated_by f0;
Underflow_BeforeRounding updated_by g|> =
f with Underflow_BeforeRounding updated_by f0 ∘ g) ∧
∀g f0 f.
f with
<|Underflow_AfterRounding updated_by f0;
Underflow_AfterRounding updated_by g|> =
f with Underflow_AfterRounding updated_by f0 ∘ g
[flags_fupdfupds_comp] Theorem
⊢ ((∀g f0.
DivideByZero_fupd f0 ∘ DivideByZero_fupd g =
DivideByZero_fupd (f0 ∘ g)) ∧
∀h g f0.
DivideByZero_fupd f0 ∘ DivideByZero_fupd g ∘ h =
DivideByZero_fupd (f0 ∘ g) ∘ h) ∧
((∀g f0.
InvalidOp_fupd f0 ∘ InvalidOp_fupd g = InvalidOp_fupd (f0 ∘ g)) ∧
∀h g f0.
InvalidOp_fupd f0 ∘ InvalidOp_fupd g ∘ h =
InvalidOp_fupd (f0 ∘ g) ∘ h) ∧
((∀g f0.
Overflow_fupd f0 ∘ Overflow_fupd g = Overflow_fupd (f0 ∘ g)) ∧
∀h g f0.
Overflow_fupd f0 ∘ Overflow_fupd g ∘ h =
Overflow_fupd (f0 ∘ g) ∘ h) ∧
((∀g f0.
Precision_fupd f0 ∘ Precision_fupd g = Precision_fupd (f0 ∘ g)) ∧
∀h g f0.
Precision_fupd f0 ∘ Precision_fupd g ∘ h =
Precision_fupd (f0 ∘ g) ∘ h) ∧
((∀g f0.
Underflow_BeforeRounding_fupd f0 ∘
Underflow_BeforeRounding_fupd g =
Underflow_BeforeRounding_fupd (f0 ∘ g)) ∧
∀h g f0.
Underflow_BeforeRounding_fupd f0 ∘
Underflow_BeforeRounding_fupd g ∘ h =
Underflow_BeforeRounding_fupd (f0 ∘ g) ∘ h) ∧
(∀g f0.
Underflow_AfterRounding_fupd f0 ∘ Underflow_AfterRounding_fupd g =
Underflow_AfterRounding_fupd (f0 ∘ g)) ∧
∀h g f0.
Underflow_AfterRounding_fupd f0 ∘
Underflow_AfterRounding_fupd g ∘ h =
Underflow_AfterRounding_fupd (f0 ∘ g) ∘ h
[flags_induction] Theorem
⊢ ∀P. (∀b b0 b1 b2 b3 b4. P (flags b b0 b1 b2 b3 b4)) ⇒ ∀f. P f
[flags_literal_11] Theorem
⊢ ∀b41 b31 b21 b11 b01 b1 b42 b32 b22 b12 b02 b2.
(<|DivideByZero := b41; InvalidOp := b31; Overflow := b21;
Precision := b11; Underflow_BeforeRounding := b01;
Underflow_AfterRounding := b1|> =
<|DivideByZero := b42; InvalidOp := b32; Overflow := b22;
Precision := b12; Underflow_BeforeRounding := b02;
Underflow_AfterRounding := b2|>) ⇔
(b41 ⇔ b42) ∧ (b31 ⇔ b32) ∧ (b21 ⇔ b22) ∧ (b11 ⇔ b12) ∧
(b01 ⇔ b02) ∧ (b1 ⇔ b2)
[flags_literal_nchotomy] Theorem
⊢ ∀f. ∃b4 b3 b2 b1 b0 b.
f =
<|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
Precision := b1; Underflow_BeforeRounding := b0;
Underflow_AfterRounding := b|>
[flags_nchotomy] Theorem
⊢ ∀ff. ∃b b0 b1 b2 b3 b4. ff = flags b b0 b1 b2 b3 b4
[flags_updates_eq_literal] Theorem
⊢ ∀f b4 b3 b2 b1 b0 b.
f with
<|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
Precision := b1; Underflow_BeforeRounding := b0;
Underflow_AfterRounding := b|> =
<|DivideByZero := b4; InvalidOp := b3; Overflow := b2;
Precision := b1; Underflow_BeforeRounding := b0;
Underflow_AfterRounding := b|>
[float_11] Theorem
⊢ ∀a0 a1 a2 a0' a1' a2'.
(float a0 a1 a2 = float a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')
[float_Axiom] Theorem
⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (float a0 a1 a2) = f a0 a1 a2
[float_accessors] Theorem
⊢ (∀c c0 c1. (float c c0 c1).Sign = c) ∧
(∀c c0 c1. (float c c0 c1).Exponent = c0) ∧
∀c c0 c1. (float c c0 c1).Significand = c1
[float_accfupds] Theorem
⊢ (∀f0 f. (f with Exponent updated_by f0).Sign = f.Sign) ∧
(∀f0 f. (f with Significand updated_by f0).Sign = f.Sign) ∧
(∀f0 f. (f with Sign updated_by f0).Exponent = f.Exponent) ∧
(∀f0 f. (f with Significand updated_by f0).Exponent = f.Exponent) ∧
(∀f0 f. (f with Sign updated_by f0).Significand = f.Significand) ∧
(∀f0 f. (f with Exponent updated_by f0).Significand = f.Significand) ∧
(∀f0 f. (f with Sign updated_by f0).Sign = f0 f.Sign) ∧
(∀f0 f. (f with Exponent updated_by f0).Exponent = f0 f.Exponent) ∧
∀f0 f.
(f with Significand updated_by f0).Significand = f0 f.Significand
[float_add_compute] Theorem
⊢ (∀mode x fp_op.
float_add mode (float_some_qnan fp_op) x =
(check_for_signalling [x],
float_some_qnan (FP_Add mode (float_some_qnan fp_op) x))) ∧
(∀mode x fp_op.
float_add mode x (float_some_qnan fp_op) =
(check_for_signalling [x],
float_some_qnan (FP_Add mode x (float_some_qnan fp_op)))) ∧
(∀mode.
float_add mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ))) ∧
(∀mode.
float_add mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Add mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ))))) ∧
(∀mode.
float_add mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ))) ∧
∀mode.
float_add mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Add mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ))))
[float_add_finite] Theorem
⊢ ∀mode x y r1 r2.
(float_value x = Float r1) ∧ (float_value y = Float r2) ⇒
(float_add mode x y =
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ (x.Sign = y.Sign) then x.Sign = 1w
else (mode = roundTowardNegative)) (r1 + r2))
[float_add_finite_minus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_add mode x (float_minus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ)))
[float_add_finite_plus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_add mode x (float_plus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ)))
[float_add_minus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_add mode (float_minus_infinity (:τ # χ)) x =
(clear_flags,float_minus_infinity (:τ # χ)))
[float_add_nan] Theorem
⊢ ∀mode x y.
(float_value x = NaN) ∨ (float_value y = NaN) ⇒
(float_add mode x y =
(check_for_signalling [x; y],float_some_qnan (FP_Add mode x y)))
[float_add_plus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_add mode (float_plus_infinity (:τ # χ)) x =
(clear_flags,float_plus_infinity (:τ # χ)))
[float_case_cong] Theorem
⊢ ∀M M' f.
(M = M') ∧
(∀a0 a1 a2. (M' = float a0 a1 a2) ⇒ (f a0 a1 a2 = f' a0 a1 a2)) ⇒
(float_CASE M f = float_CASE M' f')
[float_case_eq] Theorem
⊢ (float_CASE x f = v) ⇔
∃c c0 c1. (x = float c c0 c1) ∧ (f c c0 c1 = v)
[float_cases] Theorem
⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_normal x ∨
float_is_subnormal x ∨ float_is_zero x
[float_cases_finite] Theorem
⊢ ∀x. float_is_nan x ∨ float_is_infinite x ∨ float_is_finite x
[float_compare2num_11] Theorem
⊢ ∀a a'. (float_compare2num a = float_compare2num a') ⇔ (a = a')
[float_compare2num_ONTO] Theorem
⊢ ∀r. r < 4 ⇔ ∃a. r = float_compare2num a
[float_compare2num_num2float_compare] Theorem
⊢ ∀r. r < 4 ⇔ (float_compare2num (num2float_compare r) = r)
[float_compare2num_thm] Theorem
⊢ (float_compare2num LT = 0) ∧ (float_compare2num EQ = 1) ∧
(float_compare2num GT = 2) ∧ (float_compare2num UN = 3)
[float_compare_Axiom] Theorem
⊢ ∀x0 x1 x2 x3. ∃f.
(f LT = x0) ∧ (f EQ = x1) ∧ (f GT = x2) ∧ (f UN = x3)
[float_compare_EQ_float_compare] Theorem
⊢ ∀a a'. (a = a') ⇔ (float_compare2num a = float_compare2num a')
[float_compare_case_cong] Theorem
⊢ ∀M M' v0 v1 v2 v3.
(M = M') ∧ ((M' = LT) ⇒ (v0 = v0')) ∧ ((M' = EQ) ⇒ (v1 = v1')) ∧
((M' = GT) ⇒ (v2 = v2')) ∧ ((M' = UN) ⇒ (v3 = v3')) ⇒
((case M of LT => v0 | EQ => v1 | GT => v2 | UN => v3) =
case M' of LT => v0' | EQ => v1' | GT => v2' | UN => v3')
[float_compare_case_def] Theorem
⊢ (∀v0 v1 v2 v3.
(case LT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v0) ∧
(∀v0 v1 v2 v3.
(case EQ of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v1) ∧
(∀v0 v1 v2 v3.
(case GT of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v2) ∧
∀v0 v1 v2 v3.
(case UN of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v3
[float_compare_case_eq] Theorem
⊢ ((case x of LT => v0 | EQ => v1 | GT => v2 | UN => v3) = v) ⇔
(x = LT) ∧ (v0 = v) ∨ (x = EQ) ∧ (v1 = v) ∨ (x = GT) ∧ (v2 = v) ∨
(x = UN) ∧ (v3 = v)
[float_compare_distinct] Theorem
⊢ LT ≠ EQ ∧ LT ≠ GT ∧ LT ≠ UN ∧ EQ ≠ GT ∧ EQ ≠ UN ∧ GT ≠ UN
[float_compare_induction] Theorem
⊢ ∀P. P EQ ∧ P GT ∧ P LT ∧ P UN ⇒ ∀a. P a
[float_compare_nchotomy] Theorem
⊢ ∀a. (a = LT) ∨ (a = EQ) ∨ (a = GT) ∨ (a = UN)
[float_component_equality] Theorem
⊢ ∀f1 f2.
(f1 = f2) ⇔
(f1.Sign = f2.Sign) ∧ (f1.Exponent = f2.Exponent) ∧
(f1.Significand = f2.Significand)
[float_components] Theorem
⊢ ((float_plus_infinity (:τ # χ)).Sign = 0w) ∧
((float_plus_infinity (:τ # χ)).Exponent = UINT_MAXw) ∧
((float_plus_infinity (:τ # χ)).Significand = 0w) ∧
((float_minus_infinity (:τ # χ)).Sign = 1w) ∧
((float_minus_infinity (:τ # χ)).Exponent = UINT_MAXw) ∧
((float_minus_infinity (:τ # χ)).Significand = 0w) ∧
((float_plus_zero (:τ # χ)).Sign = 0w) ∧
((float_plus_zero (:τ # χ)).Exponent = 0w) ∧
((float_plus_zero (:τ # χ)).Significand = 0w) ∧
((float_minus_zero (:τ # χ)).Sign = 1w) ∧
((float_minus_zero (:τ # χ)).Exponent = 0w) ∧
((float_minus_zero (:τ # χ)).Significand = 0w) ∧
((float_plus_min (:τ # χ)).Sign = 0w) ∧
((float_plus_min (:τ # χ)).Exponent = 0w) ∧
((float_plus_min (:τ # χ)).Significand = 1w) ∧
((float_minus_min (:τ # χ)).Sign = 1w) ∧
((float_minus_min (:τ # χ)).Exponent = 0w) ∧
((float_minus_min (:τ # χ)).Significand = 1w) ∧
((float_top (:τ # χ)).Sign = 0w) ∧
((float_top (:τ # χ)).Exponent = UINT_MAXw − 1w) ∧
((float_top (:τ # χ)).Significand = UINT_MAXw) ∧
((float_bottom (:τ # χ)).Sign = 1w) ∧
((float_bottom (:τ # χ)).Exponent = UINT_MAXw − 1w) ∧
((float_bottom (:τ # χ)).Significand = UINT_MAXw) ∧
(∀fp_op. (float_some_qnan fp_op).Exponent = UINT_MAXw) ∧
(∀fp_op. (float_some_qnan fp_op).Significand ≠ 0w) ∧
(∀x. (float_negate x).Sign = ¬x.Sign) ∧
(∀x. (float_negate x).Exponent = x.Exponent) ∧
∀x. (float_negate x).Significand = x.Significand
[float_distinct] Theorem
⊢ float_plus_infinity (:τ # χ) ≠ float_minus_infinity (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_plus_zero (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
float_plus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
(∀fp_op. float_plus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_minus_infinity (:τ # χ) ≠ float_plus_zero (:τ # χ) ∧
float_minus_infinity (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
float_minus_infinity (:τ # χ) ≠ float_top (:τ # χ) ∧
float_minus_infinity (:τ # χ) ≠ float_bottom (:τ # χ) ∧
float_minus_infinity (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
float_minus_infinity (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
(∀fp_op. float_minus_infinity (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_plus_zero (:τ # χ) ≠ float_minus_zero (:τ # χ) ∧
float_plus_zero (:τ # χ) ≠ float_top (:τ # χ) ∧
float_plus_zero (:τ # χ) ≠ float_bottom (:τ # χ) ∧
float_plus_zero (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
float_plus_zero (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
(∀fp_op. float_plus_zero (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_minus_zero (:τ # χ) ≠ float_top (:τ # χ) ∧
float_minus_zero (:τ # χ) ≠ float_bottom (:τ # χ) ∧
float_minus_zero (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
float_minus_zero (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
(∀fp_op. float_minus_zero (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_top (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
float_top (:τ # χ) ≠ float_bottom (:τ # χ) ∧
(∀fp_op. float_top (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_bottom (:τ # χ) ≠ float_plus_min (:τ # χ) ∧
(∀fp_op. float_bottom (:τ # χ) ≠ float_some_qnan fp_op) ∧
(∀fp_op. float_plus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
float_plus_min (:τ # χ) ≠ float_minus_min (:τ # χ) ∧
(∀fp_op. float_minus_min (:τ # χ) ≠ float_some_qnan fp_op) ∧
∀x. float_negate x ≠ x
[float_distinct_finite] Theorem
⊢ ∀x. ¬(float_is_nan x ∧ float_is_infinite x) ∧
¬(float_is_nan x ∧ float_is_finite x) ∧
¬(float_is_infinite x ∧ float_is_finite x)
[float_div_compute] Theorem
⊢ (∀mode x fp_op.
float_div mode (float_some_qnan fp_op) x =
(check_for_signalling [x],
float_some_qnan (FP_Div mode (float_some_qnan fp_op) x))) ∧
(∀mode x fp_op.
float_div mode x (float_some_qnan fp_op) =
(check_for_signalling [x],
float_some_qnan (FP_Div mode x (float_some_qnan fp_op)))) ∧
(∀mode.
float_div mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Div mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ))))) ∧
(∀mode.
float_div mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Div mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ))))) ∧
(∀mode.
float_div mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Div mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ))))) ∧
∀mode.
float_div mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Div mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ))))
[float_div_finite] Theorem
⊢ ∀mode x y r1 r2.
(float_value x = Float r1) ∧ (float_value y = Float r2) ⇒
(float_div mode x y =
if r2 = 0 then
if r1 = 0 then
(invalidop_flags,float_some_qnan (FP_Div mode x y))
else
(dividezero_flags,
if x.Sign = y.Sign then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ))
else float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 / r2))
[float_div_finite_minus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_div mode x (float_minus_infinity (:τ # χ)) =
(clear_flags,
if x.Sign = 0w then float_minus_zero (:τ # χ)
else float_plus_zero (:τ # χ)))
[float_div_finite_plus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_div mode x (float_plus_infinity (:τ # χ)) =
(clear_flags,
if x.Sign = 0w then float_plus_zero (:τ # χ)
else float_minus_zero (:τ # χ)))
[float_div_minus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_div mode (float_minus_infinity (:τ # χ)) x =
(clear_flags,
if x.Sign = 0w then float_minus_infinity (:τ # χ)
else float_plus_infinity (:τ # χ)))
[float_div_nan] Theorem
⊢ ∀mode x y.
(float_value x = NaN) ∨ (float_value y = NaN) ⇒
(float_div mode x y =
(check_for_signalling [x; y],float_some_qnan (FP_Div mode x y)))
[float_div_plus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_div mode (float_plus_infinity (:τ # χ)) x =
(clear_flags,
if x.Sign = 0w then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ)))
[float_fn_updates] Theorem
⊢ (∀f c c0 c1.
float c c0 c1 with Sign updated_by f = float (f c) c0 c1) ∧
(∀f c c0 c1.
float c c0 c1 with Exponent updated_by f = float c (f c0) c1) ∧
∀f c c0 c1.
float c c0 c1 with Significand updated_by f = float c c0 (f c1)
[float_fupdcanon] Theorem
⊢ (∀g f0 f.
f with <|Exponent updated_by f0; Sign updated_by g|> =
f with <|Sign updated_by g; Exponent updated_by f0|>) ∧
(∀g f0 f.
f with <|Significand updated_by f0; Sign updated_by g|> =
f with <|Sign updated_by g; Significand updated_by f0|>) ∧
∀g f0 f.
f with <|Significand updated_by f0; Exponent updated_by g|> =
f with <|Exponent updated_by g; Significand updated_by f0|>
[float_fupdcanon_comp] Theorem
⊢ ((∀g f0.
Exponent_fupd f0 ∘ Sign_fupd g = Sign_fupd g ∘ Exponent_fupd f0) ∧
∀h g f0.
Exponent_fupd f0 ∘ Sign_fupd g ∘ h =
Sign_fupd g ∘ Exponent_fupd f0 ∘ h) ∧
((∀g f0.
Significand_fupd f0 ∘ Sign_fupd g =
Sign_fupd g ∘ Significand_fupd f0) ∧
∀h g f0.
Significand_fupd f0 ∘ Sign_fupd g ∘ h =
Sign_fupd g ∘ Significand_fupd f0 ∘ h) ∧
(∀g f0.
Significand_fupd f0 ∘ Exponent_fupd g =
Exponent_fupd g ∘ Significand_fupd f0) ∧
∀h g f0.
Significand_fupd f0 ∘ Exponent_fupd g ∘ h =
Exponent_fupd g ∘ Significand_fupd f0 ∘ h
[float_fupdfupds] Theorem
⊢ (∀g f0 f.
f with <|Sign updated_by f0; Sign updated_by g|> =
f with Sign updated_by f0 ∘ g) ∧
(∀g f0 f.
f with <|Exponent updated_by f0; Exponent updated_by g|> =
f with Exponent updated_by f0 ∘ g) ∧
∀g f0 f.
f with <|Significand updated_by f0; Significand updated_by g|> =
f with Significand updated_by f0 ∘ g
[float_fupdfupds_comp] Theorem
⊢ ((∀g f0. Sign_fupd f0 ∘ Sign_fupd g = Sign_fupd (f0 ∘ g)) ∧
∀h g f0. Sign_fupd f0 ∘ Sign_fupd g ∘ h = Sign_fupd (f0 ∘ g) ∘ h) ∧
((∀g f0.
Exponent_fupd f0 ∘ Exponent_fupd g = Exponent_fupd (f0 ∘ g)) ∧
∀h g f0.
Exponent_fupd f0 ∘ Exponent_fupd g ∘ h =
Exponent_fupd (f0 ∘ g) ∘ h) ∧
(∀g f0.
Significand_fupd f0 ∘ Significand_fupd g =
Significand_fupd (f0 ∘ g)) ∧
∀h g f0.
Significand_fupd f0 ∘ Significand_fupd g ∘ h =
Significand_fupd (f0 ∘ g) ∘ h
[float_induction] Theorem
⊢ ∀P. (∀c c0 c1. P (float c c0 c1)) ⇒ ∀f. P f
[float_infinities] Theorem
⊢ ∀x. float_is_infinite x ⇔
(x = float_plus_infinity (:τ # χ)) ∨
(x = float_minus_infinity (:τ # χ))
[float_infinities_distinct] Theorem
⊢ ∀x. ¬((x = float_plus_infinity (:τ # χ)) ∧
(x = float_minus_infinity (:τ # χ)))
[float_infinity_negate_abs] Theorem
⊢ (float_negate (float_plus_infinity (:τ # χ)) =
float_minus_infinity (:τ # χ)) ∧
(float_negate (float_minus_infinity (:τ # χ)) =
float_plus_infinity (:τ # χ)) ∧
(float_abs (float_plus_infinity (:τ # χ)) =
float_plus_infinity (:τ # χ)) ∧
(float_abs (float_minus_infinity (:τ # χ)) =
float_plus_infinity (:τ # χ))
[float_is_distinct] Theorem
⊢ ∀x. ¬(float_is_nan x ∧ float_is_infinite x) ∧
¬(float_is_nan x ∧ float_is_normal x) ∧
¬(float_is_nan x ∧ float_is_subnormal x) ∧
¬(float_is_nan x ∧ float_is_zero x) ∧
¬(float_is_infinite x ∧ float_is_normal x) ∧
¬(float_is_infinite x ∧ float_is_subnormal x) ∧
¬(float_is_infinite x ∧ float_is_zero x) ∧
¬(float_is_normal x ∧ float_is_subnormal x) ∧
¬(float_is_normal x ∧ float_is_zero x) ∧
¬(float_is_subnormal x ∧ float_is_zero x)
[float_is_finite] Theorem
⊢ ∀x. float_is_finite x ⇔
float_is_normal x ∨ float_is_subnormal x ∨ float_is_zero x
[float_is_zero] Theorem
⊢ ∀x. float_is_zero x ⇔ (x.Exponent = 0w) ∧ (x.Significand = 0w)
[float_is_zero_to_real] Theorem
⊢ ∀x. float_is_zero x ⇔ (float_to_real x = 0)
[float_literal_11] Theorem
⊢ ∀c11 c01 c1 c12 c02 c2.
(<|Sign := c11; Exponent := c01; Significand := c1|> =
<|Sign := c12; Exponent := c02; Significand := c2|>) ⇔
(c11 = c12) ∧ (c01 = c02) ∧ (c1 = c2)
[float_literal_nchotomy] Theorem
⊢ ∀f. ∃c1 c0 c. f = <|Sign := c1; Exponent := c0; Significand := c|>
[float_minus_infinity] Theorem
⊢ float_minus_infinity (:τ # χ) =
<|Sign := 1w; Exponent := UINT_MAXw; Significand := 0w|>
[float_minus_zero] Theorem
⊢ float_minus_zero (:τ # χ) =
<|Sign := 1w; Exponent := 0w; Significand := 0w|>
[float_mul_compute] Theorem
⊢ (∀mode x fp_op.
float_mul mode (float_some_qnan fp_op) x =
(check_for_signalling [x],
float_some_qnan (FP_Mul mode (float_some_qnan fp_op) x))) ∧
(∀mode x fp_op.
float_mul mode x (float_some_qnan fp_op) =
(check_for_signalling [x],
float_some_qnan (FP_Mul mode x (float_some_qnan fp_op)))) ∧
(∀mode.
float_mul mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ))) ∧
(∀mode.
float_mul mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ))) ∧
(∀mode.
float_mul mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ))) ∧
∀mode.
float_mul mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ))
[float_mul_finite] Theorem
⊢ ∀mode x y r1 r2.
(float_value x = Float r1) ∧ (float_value y = Float r2) ⇒
(float_mul mode x y =
float_round_with_flags mode (x.Sign ≠ y.Sign) (r1 * r2))
[float_mul_finite_minus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_mul mode x (float_minus_infinity (:τ # χ)) =
if r = 0 then
(invalidop_flags,
float_some_qnan
(FP_Mul mode x (float_minus_infinity (:τ # χ))))
else
(clear_flags,
if x.Sign = 0w then float_minus_infinity (:τ # χ)
else float_plus_infinity (:τ # χ)))
[float_mul_finite_plus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_mul mode x (float_plus_infinity (:τ # χ)) =
if r = 0 then
(invalidop_flags,
float_some_qnan
(FP_Mul mode x (float_plus_infinity (:τ # χ))))
else
(clear_flags,
if x.Sign = 0w then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ)))
[float_mul_minus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_mul mode (float_minus_infinity (:τ # χ)) x =
if r = 0 then
(invalidop_flags,
float_some_qnan
(FP_Mul mode (float_minus_infinity (:τ # χ)) x))
else
(clear_flags,
if x.Sign = 0w then float_minus_infinity (:τ # χ)
else float_plus_infinity (:τ # χ)))
[float_mul_nan] Theorem
⊢ ∀mode x y.
(float_value x = NaN) ∨ (float_value y = NaN) ⇒
(float_mul mode x y =
(check_for_signalling [x; y],float_some_qnan (FP_Mul mode x y)))
[float_mul_plus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_mul mode (float_plus_infinity (:τ # χ)) x =
if r = 0 then
(invalidop_flags,
float_some_qnan
(FP_Mul mode (float_plus_infinity (:τ # χ)) x))
else
(clear_flags,
if x.Sign = 0w then float_plus_infinity (:τ # χ)
else float_minus_infinity (:τ # χ)))
[float_nchotomy] Theorem
⊢ ∀ff. ∃c c0 c1. ff = float c c0 c1
[float_negate_negate] Theorem
⊢ ∀x. float_negate (float_negate x) = x
[float_round_bottom] Theorem
⊢ ∀mode toneg r.
(round mode r = float_bottom (:τ # χ)) ⇒
(float_round mode toneg r = float_bottom (:τ # χ))
[float_round_minus_infinity] Theorem
⊢ ∀mode toneg r.
(round mode r = float_minus_infinity (:τ # χ)) ⇒
(float_round mode toneg r = float_minus_infinity (:τ # χ))
[float_round_non_zero] Theorem
⊢ ∀mode toneg r s e f.
(round mode r = <|Sign := s; Exponent := e; Significand := f|>) ∧
(e ≠ 0w ∨ f ≠ 0w) ⇒
(float_round mode toneg r =
<|Sign := s; Exponent := e; Significand := f|>)
[float_round_plus_infinity] Theorem
⊢ ∀mode toneg r.
(round mode r = float_plus_infinity (:τ # χ)) ⇒
(float_round mode toneg r = float_plus_infinity (:τ # χ))
[float_round_roundTowardNegative_minus_infinity] Theorem
⊢ ∀b y x.
x < -largest (:τ # χ) ⇒
(float_round roundTowardNegative b x =
float_minus_infinity (:τ # χ))
[float_round_roundTowardNegative_top] Theorem
⊢ ∀b y x.
largest (:τ # χ) < x ⇒
(float_round roundTowardNegative b x = float_top (:τ # χ))
[float_round_roundTowardPositive_bottom] Theorem
⊢ ∀b y x.
x < -largest (:τ # χ) ⇒
(float_round roundTowardPositive b x = float_bottom (:τ # χ))
[float_round_roundTowardPositive_plus_infinity] Theorem
⊢ ∀b y x.
largest (:τ # χ) < x ⇒
(float_round roundTowardPositive b x =
float_plus_infinity (:τ # χ))
[float_round_roundTowardZero_bottom] Theorem
⊢ ∀b y x.
x < -largest (:τ # χ) ⇒
(float_round roundTowardZero b x = float_bottom (:τ # χ))
[float_round_roundTowardZero_top] Theorem
⊢ ∀b y x.
largest (:τ # χ) < x ⇒
(float_round roundTowardZero b x = float_top (:τ # χ))
[float_round_to_integral_compute] Theorem
⊢ (∀m. float_round_to_integral m (float_minus_infinity (:τ # χ)) =
float_minus_infinity (:τ # χ)) ∧
(∀m. float_round_to_integral m (float_plus_infinity (:τ # χ)) =
float_plus_infinity (:τ # χ)) ∧
∀m fp_op.
float_round_to_integral m (float_some_qnan fp_op) =
float_some_qnan fp_op
[float_round_top] Theorem
⊢ ∀mode toneg r.
(round mode r = float_top (:τ # χ)) ⇒
(float_round mode toneg r = float_top (:τ # χ))
[float_sets] Theorem
⊢ (float_is_zero =
{float_minus_zero (:τ # χ); float_plus_zero (:τ # χ)}) ∧
(float_is_infinite =
{float_minus_infinity (:τ # χ); float_plus_infinity (:τ # χ)})
[float_sub_compute] Theorem
⊢ (∀mode x fp_op.
float_sub mode (float_some_qnan fp_op) x =
(check_for_signalling [x],
float_some_qnan (FP_Sub mode (float_some_qnan fp_op) x))) ∧
(∀mode x fp_op.
float_sub mode x (float_some_qnan fp_op) =
(check_for_signalling [x],
float_some_qnan (FP_Sub mode x (float_some_qnan fp_op)))) ∧
(∀mode.
float_sub mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Sub mode (float_minus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ))))) ∧
(∀mode.
float_sub mode (float_minus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ))) ∧
(∀mode.
float_sub mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ)) =
(invalidop_flags,
float_some_qnan
(FP_Sub mode (float_plus_infinity (:τ # χ))
(float_plus_infinity (:τ # χ))))) ∧
∀mode.
float_sub mode (float_plus_infinity (:τ # χ))
(float_minus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ))
[float_sub_finite] Theorem
⊢ ∀mode x y r1 r2.
(float_value x = Float r1) ∧ (float_value y = Float r2) ⇒
(float_sub mode x y =
float_round_with_flags mode
(if (r1 = 0) ∧ (r2 = 0) ∧ x.Sign ≠ y.Sign then x.Sign = 1w
else (mode = roundTowardNegative)) (r1 − r2))
[float_sub_finite_minus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_sub mode x (float_minus_infinity (:τ # χ)) =
(clear_flags,float_plus_infinity (:τ # χ)))
[float_sub_finite_plus_infinity] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_sub mode x (float_plus_infinity (:τ # χ)) =
(clear_flags,float_minus_infinity (:τ # χ)))
[float_sub_minus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_sub mode (float_minus_infinity (:τ # χ)) x =
(clear_flags,float_minus_infinity (:τ # χ)))
[float_sub_nan] Theorem
⊢ ∀mode x y.
(float_value x = NaN) ∨ (float_value y = NaN) ⇒
(float_sub mode x y =
(check_for_signalling [x; y],float_some_qnan (FP_Sub mode x y)))
[float_sub_plus_infinity_finite] Theorem
⊢ ∀mode x r.
(float_value x = Float r) ⇒
(float_sub mode (float_plus_infinity (:τ # χ)) x =
(clear_flags,float_plus_infinity (:τ # χ)))
[float_tests] Theorem
⊢ (∀s e f.
float_is_nan <|Sign := s; Exponent := e; Significand := f|> ⇔
(e = -1w) ∧ f ≠ 0w) ∧
(∀s e f.
float_is_signalling
<|Sign := s; Exponent := e; Significand := f|> ⇔
(e = -1w) ∧ ¬word_msb f ∧ f ≠ 0w) ∧
(∀s e f.
float_is_infinite <|Sign := s; Exponent := e; Significand := f|> ⇔
(e = -1w) ∧ (f = 0w)) ∧
(∀s e f.
float_is_normal <|Sign := s; Exponent := e; Significand := f|> ⇔
e ≠ 0w ∧ e ≠ -1w) ∧
(∀s e f.
float_is_subnormal
<|Sign := s; Exponent := e; Significand := f|> ⇔
(e = 0w) ∧ f ≠ 0w) ∧
(∀s e f.
float_is_zero <|Sign := s; Exponent := e; Significand := f|> ⇔
(e = 0w) ∧ (f = 0w)) ∧
∀s e f.
float_is_finite <|Sign := s; Exponent := e; Significand := f|> ⇔
e ≠ -1w
[float_to_real] Theorem
⊢ ∀s e f.
float_to_real <|Sign := s; Exponent := e; Significand := f|> =
(let
r =
if e = 0w then
2 / &(2 ** bias (:χ)) * (&w2n f / &dimword (:τ))
else
&(2 ** w2n e) / &(2 ** bias (:χ)) *
(1 + &w2n f / &dimword (:τ))
in
if s = 1w then -r else r)
[float_to_real_eq] Theorem
⊢ ∀x y.
(float_to_real x = float_to_real y) ⇔
(x = y) ∨ float_is_zero x ∧ float_is_zero y
[float_to_real_negate] Theorem
⊢ ∀x. float_to_real (float_negate x) = -float_to_real x
[float_updates_eq_literal] Theorem
⊢ ∀f c1 c0 c.
f with <|Sign := c1; Exponent := c0; Significand := c|> =
<|Sign := c1; Exponent := c0; Significand := c|>
[float_value_11] Theorem
⊢ ∀a a'. (Float a = Float a') ⇔ (a = a')
[float_value_Axiom] Theorem
⊢ ∀f0 f1 f2. ∃fn.
(∀a. fn (Float a) = f0 a) ∧ (fn Infinity = f1) ∧ (fn NaN = f2)
[float_value_case_cong] Theorem
⊢ ∀M M' f v v1.
(M = M') ∧ (∀a. (M' = Float a) ⇒ (f a = f' a)) ∧
((M' = Infinity) ⇒ (v = v')) ∧ ((M' = NaN) ⇒ (v1 = v1')) ⇒
(float_value_CASE M f v v1 = float_value_CASE M' f' v' v1')
[float_value_case_eq] Theorem
⊢ (float_value_CASE x f v v1 = v') ⇔
(∃r. (x = Float r) ∧ (f r = v')) ∨ (x = Infinity) ∧ (v = v') ∨
(x = NaN) ∧ (v1 = v')
[float_value_distinct] Theorem
⊢ (∀a. Float a ≠ Infinity) ∧ (∀a. Float a ≠ NaN) ∧ Infinity ≠ NaN
[float_value_induction] Theorem
⊢ ∀P. (∀r. P (Float r)) ∧ P Infinity ∧ P NaN ⇒ ∀f. P f
[float_value_nchotomy] Theorem
⊢ ∀ff. (∃r. ff = Float r) ∨ (ff = Infinity) ∨ (ff = NaN)
[float_values] Theorem
⊢ (float_value (float_plus_infinity (:τ # χ)) = Infinity) ∧
(float_value (float_minus_infinity (:τ # χ)) = Infinity) ∧
(∀fp_op. float_value (float_some_qnan fp_op) = NaN) ∧
(float_value (float_plus_zero (:τ # χ)) = Float 0) ∧
(float_value (float_minus_zero (:τ # χ)) = Float 0) ∧
(float_value (float_plus_min (:τ # χ)) =
Float (2 / 2 pow (bias (:χ) + precision (:τ)))) ∧
(float_value (float_minus_min (:τ # χ)) =
Float (-2 / 2 pow (bias (:χ) + precision (:τ))))
[fp_op_11] Theorem
⊢ (∀a0 a1 a0' a1'.
(FP_Sqrt a0 a1 = FP_Sqrt a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
(∀a0 a1 a2 a0' a1' a2'.
(FP_Add a0 a1 a2 = FP_Add a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
(∀a0 a1 a2 a0' a1' a2'.
(FP_Sub a0 a1 a2 = FP_Sub a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
(∀a0 a1 a2 a0' a1' a2'.
(FP_Mul a0 a1 a2 = FP_Mul a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
(∀a0 a1 a2 a0' a1' a2'.
(FP_Div a0 a1 a2 = FP_Div a0' a1' a2') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')) ∧
(∀a0 a1 a2 a3 a0' a1' a2' a3'.
(FP_MulAdd a0 a1 a2 a3 = FP_MulAdd a0' a1' a2' a3') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2') ∧ (a3 = a3')) ∧
∀a0 a1 a2 a3 a0' a1' a2' a3'.
(FP_MulSub a0 a1 a2 a3 = FP_MulSub a0' a1' a2' a3') ⇔
(a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2') ∧ (a3 = a3')
[fp_op_Axiom] Theorem
⊢ ∀f0 f1 f2 f3 f4 f5 f6. ∃fn.
(∀a0 a1. fn (FP_Sqrt a0 a1) = f0 a0 a1) ∧
(∀a0 a1 a2. fn (FP_Add a0 a1 a2) = f1 a0 a1 a2) ∧
(∀a0 a1 a2. fn (FP_Sub a0 a1 a2) = f2 a0 a1 a2) ∧
(∀a0 a1 a2. fn (FP_Mul a0 a1 a2) = f3 a0 a1 a2) ∧
(∀a0 a1 a2. fn (FP_Div a0 a1 a2) = f4 a0 a1 a2) ∧
(∀a0 a1 a2 a3. fn (FP_MulAdd a0 a1 a2 a3) = f5 a0 a1 a2 a3) ∧
∀a0 a1 a2 a3. fn (FP_MulSub a0 a1 a2 a3) = f6 a0 a1 a2 a3
[fp_op_case_cong] Theorem
⊢ ∀M M' f f1 f2 f3 f4 f5 f6.
(M = M') ∧
(∀a0 a1. (M' = FP_Sqrt a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ∧
(∀a0 a1 a2. (M' = FP_Add a0 a1 a2) ⇒ (f1 a0 a1 a2 = f1' a0 a1 a2)) ∧
(∀a0 a1 a2. (M' = FP_Sub a0 a1 a2) ⇒ (f2 a0 a1 a2 = f2' a0 a1 a2)) ∧
(∀a0 a1 a2. (M' = FP_Mul a0 a1 a2) ⇒ (f3 a0 a1 a2 = f3' a0 a1 a2)) ∧
(∀a0 a1 a2. (M' = FP_Div a0 a1 a2) ⇒ (f4 a0 a1 a2 = f4' a0 a1 a2)) ∧
(∀a0 a1 a2 a3.
(M' = FP_MulAdd a0 a1 a2 a3) ⇒
(f5 a0 a1 a2 a3 = f5' a0 a1 a2 a3)) ∧
(∀a0 a1 a2 a3.
(M' = FP_MulSub a0 a1 a2 a3) ⇒
(f6 a0 a1 a2 a3 = f6' a0 a1 a2 a3)) ⇒
(fp_op_CASE M f f1 f2 f3 f4 f5 f6 =
fp_op_CASE M' f' f1' f2' f3' f4' f5' f6')
[fp_op_case_eq] Theorem
⊢ (fp_op_CASE x f f1 f2 f3 f4 f5 f6 = v) ⇔
(∃r f'. (x = FP_Sqrt r f') ∧ (f r f' = v)) ∨
(∃r f' f0. (x = FP_Add r f' f0) ∧ (f1 r f' f0 = v)) ∨
(∃r f' f0. (x = FP_Sub r f' f0) ∧ (f2 r f' f0 = v)) ∨
(∃r f' f0. (x = FP_Mul r f' f0) ∧ (f3 r f' f0 = v)) ∨
(∃r f' f0. (x = FP_Div r f' f0) ∧ (f4 r f' f0 = v)) ∨
(∃r f' f0 f1'. (x = FP_MulAdd r f' f0 f1') ∧ (f5 r f' f0 f1' = v)) ∨
∃r f' f0 f1'. (x = FP_MulSub r f' f0 f1') ∧ (f6 r f' f0 f1' = v)
[fp_op_distinct] Theorem
⊢ (∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Add a0' a1' a2) ∧
(∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Sub a0' a1' a2) ∧
(∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Mul a0' a1' a2) ∧
(∀a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_Div a0' a1' a2) ∧
(∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulAdd a0' a1' a2 a3) ∧
(∀a3 a2 a1' a1 a0' a0. FP_Sqrt a0 a1 ≠ FP_MulSub a0' a1' a2 a3) ∧
(∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Sub a0' a1' a2') ∧
(∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
(∀a2' a2 a1' a1 a0' a0. FP_Add a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Add a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Add a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
(∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Mul a0' a1' a2') ∧
(∀a2' a2 a1' a1 a0' a0. FP_Sub a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Sub a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Sub a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
(∀a2' a2 a1' a1 a0' a0. FP_Mul a0 a1 a2 ≠ FP_Div a0' a1' a2') ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Mul a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Mul a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Div a0 a1 a2 ≠ FP_MulAdd a0' a1' a2' a3) ∧
(∀a3 a2' a2 a1' a1 a0' a0.
FP_Div a0 a1 a2 ≠ FP_MulSub a0' a1' a2' a3) ∧
∀a3' a3 a2' a2 a1' a1 a0' a0.
FP_MulAdd a0 a1 a2 a3 ≠ FP_MulSub a0' a1' a2' a3'
[fp_op_induction] Theorem
⊢ ∀P. (∀r f. P (FP_Sqrt r f)) ∧ (∀r f f0. P (FP_Add r f f0)) ∧
(∀r f f0. P (FP_Sub r f f0)) ∧ (∀r f f0. P (FP_Mul r f f0)) ∧
(∀r f f0. P (FP_Div r f f0)) ∧
(∀r f f0 f1. P (FP_MulAdd r f f0 f1)) ∧
(∀r f f0 f1. P (FP_MulSub r f f0 f1)) ⇒
∀f. P f
[fp_op_nchotomy] Theorem
⊢ ∀ff.
(∃r f. ff = FP_Sqrt r f) ∨ (∃r f f0. ff = FP_Add r f f0) ∨
(∃r f f0. ff = FP_Sub r f f0) ∨ (∃r f f0. ff = FP_Mul r f f0) ∨
(∃r f f0. ff = FP_Div r f f0) ∨
(∃r f f0 f1. ff = FP_MulAdd r f f0 f1) ∨
∃r f f0 f1. ff = FP_MulSub r f f0 f1
[infinity_properties] Theorem
⊢ ¬float_is_zero (float_plus_infinity (:τ # χ)) ∧
¬float_is_zero (float_minus_infinity (:τ # χ)) ∧
¬float_is_finite (float_plus_infinity (:τ # χ)) ∧
¬float_is_finite (float_minus_infinity (:τ # χ)) ∧
¬float_is_integral (float_plus_infinity (:τ # χ)) ∧
¬float_is_integral (float_minus_infinity (:τ # χ)) ∧
¬float_is_nan (float_plus_infinity (:τ # χ)) ∧
¬float_is_nan (float_minus_infinity (:τ # χ)) ∧
¬float_is_normal (float_plus_infinity (:τ # χ)) ∧
¬float_is_normal (float_minus_infinity (:τ # χ)) ∧
¬float_is_subnormal (float_plus_infinity (:τ # χ)) ∧
¬float_is_subnormal (float_minus_infinity (:τ # χ)) ∧
float_is_infinite (float_plus_infinity (:τ # χ)) ∧
float_is_infinite (float_minus_infinity (:τ # χ))
[largest] Theorem
⊢ largest (:τ # χ) =
&(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &dimword (:τ)) /
&(2 ** bias (:χ))
[largest_is_positive] Theorem
⊢ 0 ≤ largest (:τ # χ)
[largest_is_top] Theorem
⊢ 1 < precision (:χ) ⇒
(largest (:τ # χ) = float_to_real (float_top (:τ # χ)))
[largest_lt_threshold] Theorem
⊢ largest (:τ # χ) < threshold (:τ # χ)
[le2] Theorem
⊢ ∀n m. 2 ≤ n ∧ 2 ≤ m ⇒ 2 ≤ n * m
[less_than_ulp] Theorem
⊢ ∀a. abs (float_to_real a) < ulp (:τ # χ) ⇔
(a.Exponent = 0w) ∧ (a.Significand = 0w)
[min_properties] Theorem
⊢ ¬float_is_zero (float_plus_min (:τ # χ)) ∧
float_is_finite (float_plus_min (:τ # χ)) ∧
(float_is_integral (float_plus_min (:τ # χ)) ⇔
(precision (:χ) = 1) ∧ (precision (:τ) = 1)) ∧
¬float_is_nan (float_plus_min (:τ # χ)) ∧
¬float_is_normal (float_plus_min (:τ # χ)) ∧
float_is_subnormal (float_plus_min (:τ # χ)) ∧
¬float_is_infinite (float_plus_min (:τ # χ)) ∧
¬float_is_zero (float_minus_min (:τ # χ)) ∧
float_is_finite (float_minus_min (:τ # χ)) ∧
(float_is_integral (float_minus_min (:τ # χ)) ⇔
(precision (:χ) = 1) ∧ (precision (:τ) = 1)) ∧
¬float_is_nan (float_minus_min (:τ # χ)) ∧
¬float_is_normal (float_minus_min (:τ # χ)) ∧
float_is_subnormal (float_minus_min (:τ # χ)) ∧
¬float_is_infinite (float_minus_min (:τ # χ))
[neg_ulp] Theorem
⊢ -ulp (:τ # χ) =
float_to_real (float_negate (float_plus_min (:τ # χ)))
[num2float_compare_11] Theorem
⊢ ∀r r'.
r < 4 ⇒
r' < 4 ⇒
((num2float_compare r = num2float_compare r') ⇔ (r = r'))
[num2float_compare_ONTO] Theorem
⊢ ∀a. ∃r. (a = num2float_compare r) ∧ r < 4
[num2float_compare_float_compare2num] Theorem
⊢ ∀a. num2float_compare (float_compare2num a) = a
[num2float_compare_thm] Theorem
⊢ (num2float_compare 0 = LT) ∧ (num2float_compare 1 = EQ) ∧
(num2float_compare 2 = GT) ∧ (num2float_compare 3 = UN)
[num2rounding_11] Theorem
⊢ ∀r r'.
r < 4 ⇒ r' < 4 ⇒ ((num2rounding r = num2rounding r') ⇔ (r = r'))
[num2rounding_ONTO] Theorem
⊢ ∀a. ∃r. (a = num2rounding r) ∧ r < 4
[num2rounding_rounding2num] Theorem
⊢ ∀a. num2rounding (rounding2num a) = a
[num2rounding_thm] Theorem
⊢ (num2rounding 0 = roundTiesToEven) ∧
(num2rounding 1 = roundTowardPositive) ∧
(num2rounding 2 = roundTowardNegative) ∧
(num2rounding 3 = roundTowardZero)
[round_roundTiesToEven] Theorem
⊢ ∀y x r.
(float_value y = Float r) ∧
((y.Significand = 0w) ∧ y.Exponent ≠ 1w ⇒ abs r ≤ abs x) ∧
2 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧
((2 * abs (r − x) = ULP (y.Exponent,(:τ))) ⇒
¬word_lsb y.Significand) ∧ ulp (:τ # χ) < 2 * abs x ∧
abs x < threshold (:τ # χ) ⇒
(round roundTiesToEven x = y)
[round_roundTiesToEven0] Theorem
⊢ ∀y x r.
(float_value y = Float r) ∧
((y.Significand = 0w) ∧ y.Exponent ≠ 1w ∧ ¬(abs r ≤ abs x)) ∧
4 * abs (r − x) ≤ ULP (y.Exponent,(:τ)) ∧
ulp (:τ # χ) < 2 * abs x ∧ abs x < threshold (:τ # χ) ⇒
(round roundTiesToEven x = y)
[round_roundTiesToEven_is_minus_zero] Theorem
⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
(float_round roundTiesToEven T x = float_minus_zero (:τ # χ))
[round_roundTiesToEven_is_plus_zero] Theorem
⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
(float_round roundTiesToEven F x = float_plus_zero (:τ # χ))
[round_roundTiesToEven_is_zero] Theorem
⊢ ∀x. 2 * abs x ≤ ulp (:τ # χ) ⇒
(round roundTiesToEven x = float_plus_zero (:τ # χ)) ∨
(round roundTiesToEven x = float_minus_zero (:τ # χ))
[round_roundTiesToEven_minus_infinity] Theorem
⊢ ∀y x.
x ≤ -threshold (:τ # χ) ⇒
(round roundTiesToEven x = float_minus_infinity (:τ # χ))
[round_roundTiesToEven_plus_infinity] Theorem
⊢ ∀y x.
threshold (:τ # χ) ≤ x ⇒
(round roundTiesToEven x = float_plus_infinity (:τ # χ))
[round_roundTowardNegative_minus_infinity] Theorem
⊢ ∀y x.
x < -largest (:τ # χ) ⇒
(round roundTowardNegative x = float_minus_infinity (:τ # χ))
[round_roundTowardNegative_top] Theorem
⊢ ∀y x.
largest (:τ # χ) < x ⇒
(round roundTowardNegative x = float_top (:τ # χ))
[round_roundTowardPositive_bottom] Theorem
⊢ ∀y x.
x < -largest (:τ # χ) ⇒
(round roundTowardPositive x = float_bottom (:τ # χ))
[round_roundTowardPositive_plus_infinity] Theorem
⊢ ∀y x.
largest (:τ # χ) < x ⇒
(round roundTowardPositive x = float_plus_infinity (:τ # χ))
[round_roundTowardZero] Theorem
⊢ ∀y x r.
(float_value y = Float r) ∧ abs (r − x) < ULP (y.Exponent,(:τ)) ∧
abs r ≤ abs x ∧ ulp (:τ # χ) ≤ abs x ∧ abs x ≤ largest (:τ # χ) ⇒
(round roundTowardZero x = y)
[round_roundTowardZero_bottom] Theorem
⊢ ∀y x.
x < -largest (:τ # χ) ⇒
(round roundTowardZero x = float_bottom (:τ # χ))
[round_roundTowardZero_is_minus_zero] Theorem
⊢ ∀x. abs x < ulp (:τ # χ) ⇒
(float_round roundTowardZero T x = float_minus_zero (:τ # χ))
[round_roundTowardZero_is_plus_zero] Theorem
⊢ ∀x. abs x < ulp (:τ # χ) ⇒
(float_round roundTowardZero F x = float_plus_zero (:τ # χ))
[round_roundTowardZero_is_zero] Theorem
⊢ ∀x. abs x < ulp (:τ # χ) ⇒
(round roundTowardZero x = float_plus_zero (:τ # χ)) ∨
(round roundTowardZero x = float_minus_zero (:τ # χ))
[round_roundTowardZero_top] Theorem
⊢ ∀y x.
largest (:τ # χ) < x ⇒
(round roundTowardZero x = float_top (:τ # χ))
[rounding2num_11] Theorem
⊢ ∀a a'. (rounding2num a = rounding2num a') ⇔ (a = a')
[rounding2num_ONTO] Theorem
⊢ ∀r. r < 4 ⇔ ∃a. r = rounding2num a
[rounding2num_num2rounding] Theorem
⊢ ∀r. r < 4 ⇔ (rounding2num (num2rounding r) = r)
[rounding2num_thm] Theorem
⊢ (rounding2num roundTiesToEven = 0) ∧
(rounding2num roundTowardPositive = 1) ∧
(rounding2num roundTowardNegative = 2) ∧
(rounding2num roundTowardZero = 3)
[rounding_Axiom] Theorem
⊢ ∀x0 x1 x2 x3. ∃f.
(f roundTiesToEven = x0) ∧ (f roundTowardPositive = x1) ∧
(f roundTowardNegative = x2) ∧ (f roundTowardZero = x3)
[rounding_EQ_rounding] Theorem
⊢ ∀a a'. (a = a') ⇔ (rounding2num a = rounding2num a')
[rounding_case_cong] Theorem
⊢ ∀M M' v0 v1 v2 v3.
(M = M') ∧ ((M' = roundTiesToEven) ⇒ (v0 = v0')) ∧
((M' = roundTowardPositive) ⇒ (v1 = v1')) ∧
((M' = roundTowardNegative) ⇒ (v2 = v2')) ∧
((M' = roundTowardZero) ⇒ (v3 = v3')) ⇒
((case M of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) =
case M' of
roundTiesToEven => v0'
| roundTowardPositive => v1'
| roundTowardNegative => v2'
| roundTowardZero => v3')
[rounding_case_def] Theorem
⊢ (∀v0 v1 v2 v3.
(case roundTiesToEven of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) = v0) ∧
(∀v0 v1 v2 v3.
(case roundTowardPositive of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) = v1) ∧
(∀v0 v1 v2 v3.
(case roundTowardNegative of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) = v2) ∧
∀v0 v1 v2 v3.
(case roundTowardZero of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) = v3
[rounding_case_eq] Theorem
⊢ ((case x of
roundTiesToEven => v0
| roundTowardPositive => v1
| roundTowardNegative => v2
| roundTowardZero => v3) = v) ⇔
(x = roundTiesToEven) ∧ (v0 = v) ∨
(x = roundTowardPositive) ∧ (v1 = v) ∨
(x = roundTowardNegative) ∧ (v2 = v) ∨
(x = roundTowardZero) ∧ (v3 = v)
[rounding_distinct] Theorem
⊢ roundTiesToEven ≠ roundTowardPositive ∧
roundTiesToEven ≠ roundTowardNegative ∧
roundTiesToEven ≠ roundTowardZero ∧
roundTowardPositive ≠ roundTowardNegative ∧
roundTowardPositive ≠ roundTowardZero ∧
roundTowardNegative ≠ roundTowardZero
[rounding_induction] Theorem
⊢ ∀P. P roundTiesToEven ∧ P roundTowardNegative ∧
P roundTowardPositive ∧ P roundTowardZero ⇒
∀a. P a
[rounding_nchotomy] Theorem
⊢ ∀a. (a = roundTiesToEven) ∨ (a = roundTowardPositive) ∨
(a = roundTowardNegative) ∨ (a = roundTowardZero)
[sign_not_zero] Theorem
⊢ ∀s. -1 pow w2n s ≠ 0
[some_nan_properties] Theorem
⊢ ∀fp_op.
¬float_is_zero (float_some_qnan fp_op) ∧
¬float_is_finite (float_some_qnan fp_op) ∧
¬float_is_integral (float_some_qnan fp_op) ∧
float_is_nan (float_some_qnan fp_op) ∧
¬float_is_signalling (float_some_qnan fp_op) ∧
¬float_is_normal (float_some_qnan fp_op) ∧
¬float_is_subnormal (float_some_qnan fp_op) ∧
¬float_is_infinite (float_some_qnan fp_op)
[threshold] Theorem
⊢ threshold (:τ # χ) =
&(2 ** (UINT_MAX (:χ) − 1)) * (2 − 1 / &(2 * dimword (:τ))) /
&(2 ** bias (:χ))
[threshold_is_positive] Theorem
⊢ 0 < threshold (:τ # χ)
[top_properties] Theorem
⊢ ¬float_is_zero (float_top (:τ # χ)) ∧
float_is_finite (float_top (:τ # χ)) ∧
¬float_is_nan (float_top (:τ # χ)) ∧
(float_is_normal (float_top (:τ # χ)) ⇔ precision (:χ) ≠ 1) ∧
(float_is_subnormal (float_top (:τ # χ)) ⇔ (precision (:χ) = 1)) ∧
¬float_is_infinite (float_top (:τ # χ))
[ulp] Theorem
⊢ ulp (:τ # χ) = float_to_real (float_plus_min (:τ # χ))
[ulp_lt_ULP] Theorem
⊢ ∀e. ulp (:τ # χ) ≤ ULP (e,(:τ))
[ulp_lt_largest] Theorem
⊢ ulp (:τ # χ) < largest (:τ # χ)
[ulp_lt_threshold] Theorem
⊢ ulp (:τ # χ) < threshold (:τ # χ)
[zero_le_pos_div_twopow] Theorem
⊢ ∀m n. 0 ≤ &m / 2 pow n
[zero_le_twopow] Theorem
⊢ ∀n. 0 ≤ 2 pow n
[zero_lt_twopow] Theorem
⊢ ∀n. 0 < 2 pow n
[zero_neq_twopow] Theorem
⊢ ∀n. 2 pow n ≠ 0
[zero_properties] Theorem
⊢ float_is_zero (float_plus_zero (:τ # χ)) ∧
float_is_zero (float_minus_zero (:τ # χ)) ∧
float_is_finite (float_plus_zero (:τ # χ)) ∧
float_is_finite (float_minus_zero (:τ # χ)) ∧
float_is_integral (float_plus_zero (:τ # χ)) ∧
float_is_integral (float_minus_zero (:τ # χ)) ∧
¬float_is_nan (float_plus_zero (:τ # χ)) ∧
¬float_is_nan (float_minus_zero (:τ # χ)) ∧
¬float_is_normal (float_plus_zero (:τ # χ)) ∧
¬float_is_normal (float_minus_zero (:τ # χ)) ∧
¬float_is_subnormal (float_plus_zero (:τ # χ)) ∧
¬float_is_subnormal (float_minus_zero (:τ # χ)) ∧
¬float_is_infinite (float_plus_zero (:τ # χ)) ∧
¬float_is_infinite (float_minus_zero (:τ # χ))
[zero_to_real] Theorem
⊢ (float_to_real (float_plus_zero (:τ # χ)) = 0) ∧
(float_to_real (float_minus_zero (:τ # χ)) = 0)
*)
end
HOL 4, Kananaskis-14