Theory LLVM_Float_Types

theory LLVM_Float_Types
imports "IEEE_FP_Extensions/IEEE_Float_Extend_Integer"
begin

subsection ‹Double›

typedef double = "UNIV::(11, 52) float set"
  morphisms float_of_double double_of_float  
  ..
  
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) = double_of_float`(UNIV::float64 set)"
      apply auto
      by (metis double_of_float_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 .

lift_definition infinity_double::"double" is plus_infinity .

lift_definition is_normal_double::"double ⇒ bool" is IEEE.is_normal .
lift_definition is_zero_double::"double ⇒ bool" is IEEE.is_zero .
lift_definition is_finite_double::"double ⇒ bool" is IEEE.is_finite .
lift_definition is_nan_double::"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 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_double_nearest where "round_double_nearest ≡ round_double To_nearest"
abbreviation round_double_zero where "round_double_zero ≡ round_double float_To_zero"
abbreviation round_double_up where "round_double_up ≡ round_double To_pinfinity"
abbreviation round_double_down where "round_double_down ≡ round_double To_ninfinity"

subsection ‹Single›
typedef single = "UNIV::float32 set" 
  morphisms float_of_single single_of_float  
  ..


setup_lifting type_definition_single

text ‹Operations with default round-to-nearest›

instantiation single :: "{uminus,plus,times,minus,zero,one,abs,ord,inverse,finite}" begin
  lift_definition uminus_single::"single ⇒ single" is uminus .
  lift_definition plus_single::"single ⇒ single ⇒ single" is plus .
  lift_definition times_single::"single ⇒ single ⇒ single" is times .
  lift_definition divide_single::"single ⇒ single ⇒ single" is divide .
  lift_definition inverse_single::"single ⇒ single" is inverse .
  lift_definition minus_single::"single ⇒ single ⇒ single" is minus .
  lift_definition zero_single::"single" is "0::float32" .
  lift_definition one_single::"single" is "1::float32" .
  lift_definition less_eq_single::"single ⇒ single ⇒ bool" is "(≤)" .
  lift_definition less_single::"single ⇒ single ⇒ bool" is "(<)" .
  instance proof
    have [simp]: "(UNIV :: single set) = single_of_float`(UNIV::float32 set)"
      apply auto
      by (metis single_of_float_cases range_eqI)
    show "finite (UNIV :: single set)" by (simp)
  qed
end

text ‹Operations with explicit rounding mode›

lift_definition sradd :: "roundmode ⇒ single ⇒ single ⇒ single" is fadd .
lift_definition srsub :: "roundmode ⇒ single ⇒ single ⇒ single" is fsub .
lift_definition srmul :: "roundmode ⇒ single ⇒ single ⇒ single" is fmul .
lift_definition srdiv :: "roundmode ⇒ single ⇒ single ⇒ single" is fdiv .
lift_definition srrem :: "roundmode ⇒ single ⇒ single ⇒ single" is frem .
lift_definition srsqrt :: "roundmode ⇒ single ⇒ single" is fsqrt .
lift_definition srfmadd :: "roundmode ⇒ single ⇒ single ⇒ single ⇒ single" is fmul_add .

definition "srem ≡ srrem To_nearest"
definition "ssqrt ≡ srsqrt To_nearest"

lift_definition eq_single::"single⇒single⇒bool" is float_eq .

lift_definition sqrt_single::"single⇒single" is float_sqrt .

lift_definition infinity_single::"single" is plus_infinity .

lift_definition is_normal_single::"single ⇒ bool" is IEEE.is_normal .
lift_definition is_zero_single::"single ⇒ bool" is IEEE.is_zero .
lift_definition is_finite_single::"single ⇒ bool" is IEEE.is_finite .
lift_definition is_nan_single::"single ⇒ bool" is IEEE.is_nan .


lift_definition single_of_word :: "32 word ⇒ single" is float_of_fp32 .
lift_definition word_of_single :: "single ⇒ 32 word" is fp32_of_float .

lemma single_of_word_inv[simp]:
  "single_of_word (word_of_single d) = d"
  "word_of_single (single_of_word w) = w"
  by (determ transfer, simp)+
    
lemma single_of_word_zero[simp]: "single_of_word 0 = 0"
  by transfer' simp
  
lemma word_of_single_zero[simp]: "word_of_single 0 = 0"  
  by transfer' simp
  

lift_definition real_of_single :: "single ⇒ real" is IEEE.valof .

lift_definition round_single :: "roundmode ⇒ real ⇒ single" is round .

abbreviation round_single_nearest where "round_single_nearest ≡ round_single To_nearest"
abbreviation round_single_zero where "round_single_zero ≡ round_single float_To_zero"
abbreviation round_single_up where "round_single_up ≡ round_single To_pinfinity"
abbreviation round_single_down where "round_single_down ≡ round_single To_ninfinity"


subsection ‹Extension Correctness Theorem›

text ‹Version for single and double: ›
theorem fext_int_single_double_correct:
  fixes i32 :: "integer"
  defines "i64 ≡ fext_int_32_64 i32"
  defines "f32 ≡ single_of_word (word_of_integer i32)"
  defines "f64 ≡ double_of_word (word_of_integer i64)"
  shows "correct_extension (float_of_single f32) (float_of_double f64)"
  using double_of_word.rep_eq f32_def f64_def fext_int_32_64_correct i64_def single_of_word.rep_eq 
  by presburger

end