Theory LLVM_Double
theory LLVM_Double
imports IEEE_Floating_Point.Conversion_IEEE_Float IEEE_Floating_Point.FP64
begin
typedef double = "UNIV::(11, 52) float set" ..
setup_lifting type_definition_double
text ‹Operations with default round-to-nearest›
instantiation double :: "{uminus,plus,times,minus,zero,one,abs,ord,inverse,finite}" begin
lift_definition uminus_double::"double ⇒ double" is uminus .
lift_definition plus_double::"double ⇒ double ⇒ double" is plus .
lift_definition times_double::"double ⇒ double ⇒ double" is times .
lift_definition divide_double::"double ⇒ double ⇒ double" is divide .
lift_definition inverse_double::"double ⇒ double" is inverse .
lift_definition minus_double::"double ⇒ double ⇒ double" is minus .
lift_definition zero_double::"double" is "0::float64" .
lift_definition one_double::"double" is "1::float64" .
lift_definition less_eq_double::"double ⇒ double ⇒ bool" is "(≤)" .
lift_definition less_double::"double ⇒ double ⇒ bool" is "(<)" .
instance proof
have [simp]: "(UNIV :: double set) = Abs_double`(UNIV::float64 set)"
apply auto
by (metis Abs_double_cases range_eqI)
show "finite (UNIV :: double set)" by (simp)
qed
end
text ‹Operations with explicit rounding mode›
lift_definition dradd :: "roundmode ⇒ double ⇒ double ⇒ double" is fadd .
lift_definition drsub :: "roundmode ⇒ double ⇒ double ⇒ double" is fsub .
lift_definition drmul :: "roundmode ⇒ double ⇒ double ⇒ double" is fmul .
lift_definition drdiv :: "roundmode ⇒ double ⇒ double ⇒ double" is fdiv .
lift_definition drrem :: "roundmode ⇒ double ⇒ double ⇒ double" is frem .
lift_definition drsqrt :: "roundmode ⇒ double ⇒ double" is fsqrt .
lift_definition drfmadd :: "roundmode ⇒ double ⇒ double ⇒ double ⇒ double" is fmul_add .
definition "drem ≡ drrem To_nearest"
definition "dsqrt ≡ drsqrt To_nearest"
lift_definition eq_double::"double⇒double⇒bool" is float_eq .
lift_definition sqrt_double::"double⇒double" is float_sqrt .
no_notation plus_infinity ("∞")
lift_definition infinity_double::"double" ("∞") is plus_infinity .
lift_definition is_normal::"double ⇒ bool" is IEEE.is_normal .
lift_definition is_zero::"double ⇒ bool" is IEEE.is_zero .
lift_definition is_finite::"double ⇒ bool" is IEEE.is_finite .
lift_definition is_nan::"double ⇒ bool" is IEEE.is_nan .
lift_definition double_of_word :: "64 word ⇒ double" is float_of_fp64 .
lift_definition word_of_double :: "double ⇒ 64 word" is fp64_of_float .
lemma word_split_0[simp]: "word_split 0 = (0,0)"
by (auto simp: word_split_def)
lemma float_of_fp64_zero[simp]: "float_of_fp64 0 = 0"
unfolding zero_float_def float_of_fp64_def
by (auto simp: Abs_float_inject)
lemma fp64_of_float_zero[simp]: "fp64_of_float 0 = 0"
by (metis float_of_fp64_inverse float_of_fp64_zero)
lemma double_of_word_inv[simp]:
"double_of_word (word_of_double d) = d"
"word_of_double (double_of_word w) = w"
by (determ transfer, simp)+
lemma double_of_word_zero[simp]: "double_of_word 0 = 0"
by transfer' simp
lemma word_of_double_zero[simp]: "word_of_double 0 = 0"
by transfer' simp
lift_definition real_of_double :: "double ⇒ real" is IEEE.valof .
lift_definition round_double :: "roundmode ⇒ real ⇒ double" is round .
abbreviation round_nearest where "round_nearest ≡ round_double To_nearest"
abbreviation round_zero where "round_zero ≡ round_double float_To_zero"
abbreviation round_up where "round_up ≡ round_double To_pinfinity"
abbreviation round_down where "round_down ≡ round_double To_ninfinity"
end