Theory Conversion_IEEE_Float

(* Author: Fabian Hellauer
           Fabian Immler
*)
theory Conversion_IEEE_Float
  imports
    "HOL-Library.Float"
    IEEE_Properties
    "HOL-Library.Code_Target_Numeral"
begin

definition "of_finite (x::('e, 'f)float) =
  (if is_normal x then (Float (normal_mantissa x) (normal_exponent x))
    else if is_denormal x then (Float (denormal_mantissa x) (denormal_exponent TYPE(('e, 'f)float)))
    else 0)"

lemma float_val_of_finite: "is_finite x  of_finite x = valof x"
  by (induction x) (auto simp: normal_imp_not_denormal of_finite_def)

definition is_normal_Float::"('e, 'f)float itself  Float.float  bool" where
  "is_normal_Float x f 
    mantissa f  0 
    bitlen ¦mantissa f¦  fracwidth x + 1 
    - int (bias x) - bitlen ¦mantissa f¦ + 1 < Float.exponent f 
    Float.exponent f < 2^(LENGTH('e)) - bitlen ¦mantissa f¦ - bias x"

definition is_denormal_Float::"('e, 'f)float itself  Float.float  bool" where
  "is_denormal_Float x f 
    mantissa f  0 
    bitlen ¦mantissa f¦  1 - Float.exponent f - int (bias x) 
    1 - 2^(LENGTH('e) - 1) - int LENGTH('f) < Float.exponent f"

lemmas is_denormal_FloatD =
  is_denormal_Float_def[THEN iffD1, THEN conjunct1]
  is_denormal_Float_def[THEN iffD1, THEN conjunct2]

definition is_finite_Float::"('e, 'f)float itself  Float.float  bool" where
  "is_finite_Float x f  is_normal_Float x f  is_denormal_Float x f  f = 0"

lemma is_finite_Float_eq:
  "is_finite_Float TYPE(('e, 'f)float) f 
    (let e = Float.exponent f; bm = bitlen (abs (mantissa f))
    in bm  Suc LENGTH('f) 
     bm  2 ^ (LENGTH('e) - 1) - e 
     1 - 2 ^ (LENGTH('e) - 1) - int LENGTH('f) < e)"
proof -
  have *: "(2::int) ^ (LENGTH('e) - Suc 0) - 1 < 2 ^ LENGTH('e)"
    by (metis Suc_1 diff_le_self lessI linorder_not_less one_less_numeral_iff
        power_strict_increasing_iff zle_diff1_eq)
  have **: "1 - 2 ^ (LENGTH('e) - Suc 0) < int LENGTH('f)"
    by (smt len_gt_0 of_nat_0_less_iff zero_less_power)
  have ***: "2 ^ (LENGTH('e) - 1) + 1 =
    2 ^ LENGTH('e) - int (bias TYPE(('e, 'f) IEEE.float))"
    by (simp add: bias_def power_Suc[symmetric] of_nat_diff mask_eq_exp_minus_1)
  have rewr: "x  2 ^ n - e  x + e < 2 ^ n + 1" for x::int and n e
    by auto
  show ?thesis
    unfolding *** rewr
    using * **
    unfolding is_finite_Float_def is_normal_Float_def is_denormal_Float_def
    by (auto simp: Let_def bias_def mantissa_eq_zero_iff of_nat_diff mask_eq_exp_minus_1
        intro: le_less_trans[OF add_right_mono])
qed

lift_definition normal_of_Float :: "Float.float  ('e, 'f)float"
  is "λx. let m = mantissa x; e = Float.exponent x in
    (if m > 0 then 0 else 1,
      word_of_int (e + int (bias TYPE(('e, 'f)float)) + bitlen ¦m¦ - 1),
      word_of_int (¦m¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦m¦)) - 2 ^ (LENGTH('f))))"
  .

lemma sign_normal_of_Float:"sign (normal_of_Float x) = (if x > 0 then 0 else 1)"
  by transfer (auto simp: Let_def mantissa_pos_iff)

lemma uint_word_of_int_bitlen_eq:
  "uint (word_of_int x::'a::len word) = x" if "bitlen x  LENGTH('a)" "x  0"
  using that by (simp add: bitlen_le_iff_power take_bit_int_eq_self unsigned_of_int)

lemma fraction_normal_of_Float:"fraction (normal_of_Float x::('e, 'f)float) =
  (nat ¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦)) - 2 ^ LENGTH('f))"
  if "is_normal_Float TYPE(('e, 'f)float) x"
proof -
  from that have bmp: "bitlen ¦mantissa x¦ > 0"
    by (metis abs_of_nonneg bitlen_bounds bitlen_def is_normal_Float_def nat_code(2) of_nat_0_le_iff
        power.simps(1) zabs_less_one_iff zero_less_abs_iff)
  have mless: "¦mantissa x¦ < 2 ^ nat (bitlen ¦mantissa x¦)"
    using bitlen_bounds by force
  have lem: "2 ^ nat (bitlen ¦mantissa x¦ - 1)  ¦mantissa x¦"
    using bitlen_bounds is_normal_Float_def that zero_less_abs_iff by blast
  from that have nble: "nat (bitlen ¦mantissa x¦)  Suc LENGTH('f)"
    using bitlen_bounds by (auto simp: is_normal_Float_def)
  have nn: "0  ¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦)) - 2 ^ LENGTH('f)"
    apply (rule add_le_imp_le_diff)
    apply (rule order_trans[rotated])
     apply (rule mult_right_mono)
      apply (rule lem, force)
    unfolding power_add[symmetric]
    using nble bmp
    by (auto)
  have "¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦)) < 2 * 2 ^ LENGTH('f)"
    apply (rule less_le_trans)
     apply (rule mult_strict_right_mono)
      apply (rule mless)
     apply force
    unfolding power_add[symmetric] power_Suc[symmetric]
    apply (rule power_increasing)
    using nble
    by auto
  then have "bitlen (¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦)) - 2 ^ LENGTH('f))
     int LENGTH('f)"
    unfolding bitlen_le_iff_power
    by simp
  then show ?thesis
    apply (transfer fixing: x)
    unfolding Let_def split_beta' fst_conv snd_conv uint_nat [symmetric] nat_uint_eq [symmetric]
    using nn
    apply (subst uint_word_of_int_bitlen_eq)
      apply (auto simp: nat_mult_distrib nat_diff_distrib nat_power_eq)
    done
qed

lemma exponent_normal_of_Float:"exponent (normal_of_Float x::('e, 'f)float) =
  nat (Float.exponent x + (bias TYPE(('e, 'f)float)) + bitlen ¦mantissa x¦ - 1)"
  if "is_normal_Float TYPE(('e, 'f)float) x"
  using that
  apply (transfer fixing: x)
  apply (simp flip: uint_nat nat_uint_eq add: Let_def)
  apply (auto simp: is_normal_Float_def bitlen_le_iff_power uint_word_of_int_bitlen_eq Let_def)
  apply transfer
  apply (simp add: nat_take_bit_eq take_bit_int_eq_self)
  done

lift_definition denormal_of_Float :: "Float.float  ('e, 'f)float"
  is "λx. let m = mantissa x; e = Float.exponent x in
  (if m  0 then 0 else 1, 0,
    word_of_int (¦m¦ * 2 ^ nat (e + bias TYPE(('e, 'f)float) + fracwidth TYPE(('e, 'f)float) - 1)))"
  .

lemma sign_denormal_of_Float:"sign (denormal_of_Float x) = (if x  0 then 0 else 1)"
  by transfer (auto simp: Let_def mantissa_nonneg_iff)

lemma exponent_denormal_of_Float:"exponent (denormal_of_Float x::('e, 'f)float) = 0"
  by (transfer fixing: x) (auto simp: Let_def)

lemma fraction_denormal_of_Float:"fraction (denormal_of_Float x::('e, 'f)float) =
  (nat ¦mantissa x¦ * 2 ^ nat (Float.exponent x + bias TYPE(('e, 'f)float) + LENGTH('f) - 1))"
  if "is_denormal_Float TYPE(('e, 'f)float) x"
proof -
  have mless: "¦mantissa x¦ < 2 ^ nat (bitlen ¦mantissa x¦)"
    using bitlen_bounds by force
  have *: "nat (bitlen ¦mantissa x¦) +
    nat (Float.exponent x + (2 ^ (LENGTH('e) - Suc 0) + int LENGTH('f)) - 2)
     LENGTH('f)"
    using that
    by (auto simp: is_denormal_Float_def nat_diff_distrib' le_diff_conv mask_eq_exp_minus_1
        bitlen_nonneg nat_le_iff bias_def nat_add_distrib[symmetric] of_nat_diff)
  have "¦mantissa x¦ *  2 ^ nat (Float.exponent x + int (bias TYPE(('e, 'f)float)) +
    LENGTH('f) - 1) < 2 ^ LENGTH('f)"
    apply (rule less_le_trans)
     apply (rule mult_strict_right_mono)
      apply (rule mless, force)
    unfolding power_add[symmetric] power_Suc[symmetric]
    apply (rule power_increasing)
     apply (auto simp: bias_def)
    using that *
    by (auto simp: is_denormal_Float_def algebra_simps of_nat_diff mask_eq_exp_minus_1)
  then show ?thesis
    apply (transfer fixing: x)
    apply transfer
    apply (simp add: Let_def nat_eq_iff take_bit_eq_mod)
    done
qed

definition of_finite_Float :: "Float.float  ('e, 'f) float" where
  "of_finite_Float x = (if is_normal_Float TYPE(('e, 'f)float) x then normal_of_Float x
    else if is_denormal_Float TYPE(('e, 'f)float) x then denormal_of_Float x
    else 0)"

lemma valof_normal_of_Float: "valof (normal_of_Float x::('e, 'f)float) = x"
  if "is_normal_Float TYPE(('e, 'f)float) x"
proof -
  have "valof (normal_of_Float x::('e, 'f)float) =
    (- 1) ^ sign (normal_of_Float x::('e, 'f)float) *
    ((1 + real (nat ¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦)) - 2 ^ LENGTH('f)) / 2 ^ LENGTH('f)) *
      2 powr (bitlen ¦mantissa x¦ - 1)) *
    2 powr Float.exponent x"
    (is "_ = ?s * ?m * ?e")
    using that
    by (auto simp: is_normal_Float_def valof_eq fraction_normal_of_Float
        powr_realpow[symmetric] exponent_normal_of_Float powr_diff powr_add)
  also
  have "¦mantissa x¦ > 0"
    using that
    by (auto simp: is_normal_Float_def)
  have bound: "2 ^ LENGTH('f)  nat ¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦))"
  proof -
    have "(2::nat) ^ LENGTH('f)  2 ^ nat (bitlen ¦mantissa x¦ - 1) * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦))"
      by (simp add: power_add[symmetric])
    also have "  nat ¦mantissa x¦ * 2 ^ (Suc LENGTH('f) - nat (bitlen ¦mantissa x¦))"
      using bitlen_bounds[of "¦mantissa x¦"] that
      by (auto simp: is_normal_Float_def)
    finally show ?thesis .
  qed
  have "?m = abs (mantissa x)"
    apply (subst of_nat_diff)
    subgoal using bound by auto
    subgoal
      using that
      by (auto simp: powr_realpow[symmetric] powr_add[symmetric]
          is_normal_Float_def bitlen_nonneg of_nat_diff divide_simps)
    done
  finally show ?thesis
    by (auto simp: mantissa_exponent sign_normal_of_Float abs_real_def zero_less_mult_iff)
qed

lemma valof_denormal_of_Float: "valof (denormal_of_Float x::('e, 'f)float) = x"
  if "is_denormal_Float TYPE(('e, 'f)float) x"
proof -
  have less: "0 < Float.exponent x + (int (bias TYPE(('e, 'f) IEEE.float)) + int LENGTH('f))"
    using that
    by (auto simp: is_denormal_Float_def bias_def of_nat_diff mask_eq_exp_minus_1)
  have "valof (denormal_of_Float x::('e, 'f)float) =
    ((- 1) ^ sign (denormal_of_Float x::('e, 'f)float) * ¦real_of_int (mantissa x)¦) *
    (2 powr real (nat (Float.exponent x + int (bias TYPE(('e, 'f) IEEE.float)) + int LENGTH('f) - 1)) /
      (2 powr real (bias TYPE(('e, 'f) IEEE.float)) * 2 powr LENGTH('f)) * 2)"
    (is "_ = ?m * ?e")
    by (auto simp: valof_eq exponent_denormal_of_Float fraction_denormal_of_Float that
        mantissa_exponent powr_realpow[symmetric])
  also have "?m = mantissa x"
    by (auto simp: sign_denormal_of_Float abs_real_def mantissa_neg_iff)
  also have "?e = 2 powr Float.exponent x"
    by (auto simp: powr_add[symmetric] divide_simps powr_mult_base less ac_simps)
  finally show ?thesis by (simp add: mantissa_exponent)
qed

lemma valof_of_finite_Float:
  "is_finite_Float (TYPE(('e, 'f) IEEE.float)) x  valof (of_finite_Float x::('e, 'f)float) = x"
  by (auto simp: of_finite_Float_def is_finite_Float_def valof_denormal_of_Float valof_normal_of_Float)

lemma is_normal_normal_of_Float:
  "is_normal (normal_of_Float x::('e, 'f)float)" if "is_normal_Float TYPE(('e, 'f)float) x"
  using that
  by (auto simp: is_normal_def exponent_normal_of_Float that is_normal_Float_def
      emax_eq nat_less_iff of_nat_diff)

lemma is_denormal_denormal_of_Float: "is_denormal (denormal_of_Float x::('e, 'f)float)"
  if "is_denormal_Float TYPE(('e, 'f)float) x"
  using that
  by (auto simp: is_denormal_def exponent_denormal_of_Float that is_denormal_Float_def
      emax_eq fraction_denormal_of_Float le_nat_iff bias_def)

lemma is_finite_of_finite_Float: "is_finite (of_finite_Float x)"
  by (auto simp: is_finite_def of_finite_Float_def is_normal_normal_of_Float
      is_denormal_denormal_of_Float)

lemma Float_eq_zero_iff: "Float m e = 0  m = 0"
  by (metis Float.compute_is_float_zero Float_0_eq_0)

lemma bitlen_mantissa_Float:
  shows "bitlen ¦mantissa (Float m e)¦ = (if m = 0 then 0 else bitlen ¦m¦ + e) - Float.exponent (Float m e)"
  using bitlen_Float[of m e] by auto

lemma exponent_Float:
  shows "Float.exponent (Float m e) = (if m = 0 then 0 else bitlen ¦m¦ + e) - bitlen ¦mantissa (Float m e)¦ "
  using bitlen_Float[of m e] by auto

lemma is_normal_Float_normal:
  "is_normal_Float TYPE(('e, 'f)float) (Float (normal_mantissa x) (normal_exponent x))"
  if "is_normal x" for x::"('e, 'f)float"
proof -
  define f where "f = Float (normal_mantissa x) (normal_exponent x)"
  from that have "f  0"
    by (auto simp: f_def is_normal_def zero_float_def[symmetric]
        Float_eq_zero_iff normal_mantissa_def add_nonneg_eq_0_iff)
  from denormalize_shift[OF f_def this] obtain i where
    i: "normal_mantissa x = mantissa f * 2 ^ i" "normal_exponent x = Float.exponent f - int i"
    by auto
  have "mantissa f  0"
    by (auto simp: f  0 i mantissa_eq_zero_iff Float_eq_zero_iff)
  moreover
  have "normal_exponent x  Float.exponent f" unfolding i by simp
  then have " bitlen ¦mantissa f¦  1 + int LENGTH('f)"
    unfolding bitlen_mantissa_Float bitlen_normal_mantissa f_def
    by auto
  moreover
  have "- int (bias TYPE(('e, 'f)float)) - bitlen ¦mantissa f¦ + 1 < Float.exponent f"
    unfolding bitlen_mantissa_Float bitlen_normal_mantissa f_def
    using that
    by (auto simp: mantissa_eq_zero_iff abs_mult bias_def normal_mantissa_def normal_exponent_def
        is_normal_def emax_eq less_diff_conv add_nonneg_eq_0_iff)
  moreover
  have "2 ^ (LENGTH('e) - Suc 0) + - (1::int) * 2 ^ LENGTH('e)  0"
    by simp
  then have "(2::int) ^ (LENGTH('e) - Suc 0) < 1 + 2 ^ LENGTH('e)" by arith
  then have "Float.exponent f <
      2 ^ LENGTH('e) - bitlen ¦mantissa f¦ - int (bias TYPE(('e, 'f)float))"
    using normal_exponent_bounds_int[OF that]
    unfolding bitlen_mantissa_Float bitlen_normal_mantissa f_def
    by (auto simp: bias_def algebra_simps power_Suc[symmetric] of_nat_diff mask_eq_exp_minus_1
        intro: le_less_trans[OF add_right_mono] normal_exponent_bounds_int[OF that])
  ultimately
  show ?thesis
    by (auto simp: is_normal_Float_def f_def)
qed


lemma is_denormal_Float_denormal:
  "is_denormal_Float TYPE(('e, 'f)float)
    (Float (denormal_mantissa x) (denormal_exponent TYPE(('e, 'f)float)))"
  if "is_denormal x" for x::"('e, 'f)float"
proof -
  define f where "f = Float (denormal_mantissa x) (denormal_exponent TYPE(('e, 'f)float))"
  from that have "f  0"
    by (auto simp: f_def is_denormal_def zero_float_def[symmetric]
        Float_eq_zero_iff denormal_mantissa_def add_nonneg_eq_0_iff)
  from denormalize_shift[OF f_def this] obtain i where
    i: "denormal_mantissa x = mantissa f * 2 ^ i" "denormal_exponent TYPE(('e, 'f)float) = Float.exponent f - int i"
    by auto
  have "mantissa f  0"
    by (auto simp: f  0 i mantissa_eq_zero_iff Float_eq_zero_iff)
  moreover
  have "bitlen ¦mantissa f¦  1 - Float.exponent f - int (bias TYPE(('e, 'f) IEEE.float))"
    using mantissa f  0
    unfolding f_def bitlen_mantissa_Float
    using bitlen_denormal_mantissa[of x]
    by (auto simp: denormal_exponent_def)
  moreover
  have "2 - 2 ^ (LENGTH('e) - Suc 0) - int LENGTH('f)  Float.exponent f"
    (is "?l  _")
  proof -
    have "?l  denormal_exponent TYPE(('e, 'f)float) + i"
      using that
      by (auto simp: is_denormal_def bias_def denormal_exponent_def of_nat_diff mask_eq_exp_minus_1)
    also have " = Float.exponent f" unfolding i by auto
    finally show ?thesis .
  qed
  ultimately
  show ?thesis
    unfolding is_denormal_Float_def exponent_Float f_def[symmetric]
    by auto
qed

lemma is_finite_Float_of_finite: "is_finite_Float TYPE(('e, 'f)float) (of_finite x)" for x::"('e, 'f)float"
  by (auto simp: is_finite_Float_def of_finite_def is_normal_Float_normal
      is_denormal_Float_denormal)

end