Theory IEEE_Floating_Point.FP64

theory FP64
imports
  IEEE
  Word_Lib.Word_64
begin

section ‹Concrete encodings›

text ‹Floating point operations defined as operations on words.
  Called ''fixed precision'' (fp) word in HOL4.›

type_synonym float64 = "(11,52)float"
type_synonym fp64 = "64 word"

lift_definition fp64_of_float :: "float64 ⇒ fp64" is
  "λ(s::1 word, e::11 word, f::52 word). word_cat s (word_cat e f::63 word)" .

lift_definition float_of_fp64 :: "fp64 ⇒ float64" is
  "λx. apsnd word_split (word_split x::1 word * 63 word)" .

definition "rel_fp64 ≡ (λx (y::word64). x = float_of_fp64 y)"

definition eq_fp64::"float64 ⇒ float64 ⇒ bool" where [simp]: "eq_fp64 ≡ (=)"

lemma float_of_fp64_inverse[simp]: "fp64_of_float (float_of_fp64 a) = a"
  by (auto
      simp: fp64_of_float_def float_of_fp64_def Abs_float_inverse apsnd_def map_prod_def word_size
      dest!: word_cat_split_alt[rotated]
      split: prod.splits)

lemma float_of_fp64_inj_iff[simp]: "fp64_of_float r = fp64_of_float s ⟷ r = s"
  using Rep_float_inject
  by (force simp: fp64_of_float_def word_cat_inj word_size split: prod.splits)

lemma fp64_of_float_inverse[simp]: "float_of_fp64 (fp64_of_float a) = a"
  using float_of_fp64_inj_iff float_of_fp64_inverse by blast

lemma Quotientfp: "Quotient eq_fp64 fp64_of_float float_of_fp64 rel_fp64"
  ―‹\<^term>‹eq_fp64› is a workaround to prevent a (failing -- TODO: why?)
      code setup in ‹setup_lifting›.›
  by (force intro!: QuotientI simp: rel_fp64_def)

setup_lifting Quotientfp

lift_definition fp64_lessThan::"fp64 ⇒ fp64 ⇒ bool" is
  "flt::float64⇒float64⇒bool" by simp

lift_definition fp64_lessEqual::"fp64 ⇒ fp64 ⇒ bool" is
  "fle::float64⇒float64⇒bool" by simp

lift_definition fp64_greaterThan::"fp64 ⇒ fp64 ⇒ bool" is
  "fgt::float64⇒float64⇒bool" by simp

lift_definition fp64_greaterEqual::"fp64 ⇒ fp64 ⇒ bool" is
  "fge::float64⇒float64⇒bool" by simp

lift_definition fp64_equal::"fp64 ⇒ fp64 ⇒ bool" is
  "feq::float64⇒float64⇒bool" by simp

lift_definition fp64_abs::"fp64 ⇒ fp64" is
  "abs::float64⇒float64" by simp

lift_definition fp64_negate::"fp64 ⇒ fp64" is
  "uminus::float64⇒float64" by simp

lift_definition fp64_sqrt::"roundmode ⇒ fp64 ⇒ fp64" is
  "fsqrt::roundmode⇒float64⇒float64" by simp

lift_definition fp64_add::"roundmode ⇒ fp64 ⇒ fp64 ⇒ fp64" is
  "fadd::roundmode⇒float64⇒float64⇒float64" by simp

lift_definition fp64_sub::"roundmode ⇒ fp64 ⇒ fp64 ⇒ fp64" is
  "fsub::roundmode⇒float64⇒float64⇒float64" by simp

lift_definition fp64_mul::"roundmode ⇒ fp64 ⇒ fp64 ⇒ fp64" is
  "fmul::roundmode⇒float64⇒float64⇒float64" by simp

lift_definition fp64_div::"roundmode ⇒ fp64 ⇒ fp64 ⇒ fp64" is
  "fdiv::roundmode⇒float64⇒float64⇒float64" by simp

lift_definition fp64_mul_add::"roundmode ⇒ fp64 ⇒ fp64 ⇒ fp64 ⇒ fp64" is
  "fmul_add::roundmode⇒float64⇒float64⇒float64⇒float64" by simp

end