Theory IEEE_Floating_Point.IEEE_Properties

(* Author: Lei Yu, University of Cambridge
   Author: Fabian Hellauer
           Fabian Immler
*)

section ‹Proofs of Properties about Floating Point Arithmetic›

theory IEEE_Properties
imports IEEE
begin

subsection ‹Theorems derived from definitions›

lemma valof_eq:
  "valof x =
    (if exponent x = 0
       then (- 1) ^ sign x * (2 / 2 ^ bias TYPE(('a, 'b) float)) *
            (real (fraction x) / 2 ^ LENGTH('b))
       else (- 1) ^ sign x * (2 ^ exponent x / 2 ^ bias TYPE(('a, 'b) float)) *
            (1 + real (fraction x) / 2 ^ LENGTH('b)))"
  for x::"('a, 'b) float"
  unfolding Let_def
  by transfer (auto simp: bias_def divide_simps unat_eq_0)

lemma exponent_le [simp]:
  ‹exponent a ≤ mask LENGTH('a)› for a :: ‹('a, _) float›
  by transfer (auto simp add: of_nat_mask_eq intro: word_unat_less_le split: prod.split)

lemma exponent_not_less [simp]:
  ‹¬ mask LENGTH('a) < IEEE.exponent a› for a :: ‹('a, _) float›
  by (simp add: not_less)

lemma infinity_simps:
  "sign (plus_infinity::('e, 'f)float) = 0"
  "sign (minus_infinity::('e, 'f)float) = 1"
  "exponent (plus_infinity::('e, 'f)float) = emax TYPE(('e, 'f)float)"
  "exponent (minus_infinity::('e, 'f)float) = emax TYPE(('e, 'f)float)"
  "fraction (plus_infinity::('e, 'f)float) = 0"
  "fraction (minus_infinity::('e, 'f)float) = 0"
  subgoal by transfer auto
  subgoal by transfer auto
  subgoal by transfer (simp add: emax_def mask_eq_exp_minus_1)
  subgoal by transfer (simp add: emax_def mask_eq_exp_minus_1)
  subgoal by transfer auto
  subgoal by transfer auto
  done

lemma zero_simps:
  "sign (0::('e, 'f)float) = 0"
  "sign (- 0::('e, 'f)float) = 1"
  "exponent (0::('e, 'f)float) = 0"
  "exponent (- 0::('e, 'f)float) = 0"
  "fraction (0::('e, 'f)float) = 0"
  "fraction (- 0::('e, 'f)float) = 0"
  subgoal by transfer auto
  subgoal by transfer auto
  subgoal by transfer auto
  subgoal by transfer auto
  subgoal by transfer auto
  subgoal by transfer auto
  done

lemma emax_eq: "emax x = 2 ^ LENGTH('e) - 1"
  for x::"('e, 'f)float itself"
  by (simp add: emax_def unsigned_minus_1_eq_mask mask_eq_exp_minus_1)

lemma topfloat_simps:
  "sign (topfloat::('e, 'f)float) = 0"
  "exponent (topfloat::('e, 'f)float) = emax TYPE(('e, 'f)float) - 1"
  "fraction (topfloat::('e, 'f)float) = 2 ^ (fracwidth TYPE(('e, 'f)float)) - 1"
  and bottomfloat_simps:
  "sign (bottomfloat::('e, 'f)float) = 1"
  "exponent (bottomfloat::('e, 'f)float) = emax TYPE(('e, 'f)float) - 1"
  "fraction (bottomfloat::('e, 'f)float) = 2 ^ (fracwidth TYPE(('e, 'f)float)) - 1"
  subgoal by transfer simp
  subgoal by transfer (simp add: emax_eq take_bit_minus_small_eq nat_diff_distrib nat_power_eq)
  subgoal by transfer (simp add: unsigned_minus_1_eq_mask mask_eq_exp_minus_1)
  subgoal by transfer simp
  subgoal by transfer (simp add: emax_eq take_bit_minus_small_eq nat_diff_distrib nat_power_eq)
  subgoal by transfer (simp add: unsigned_minus_1_eq_mask mask_eq_exp_minus_1)
  done

lemmas float_defs =
  is_finite_def is_infinity_def is_zero_def is_nan_def
  is_normal_def is_denormal_def valof_eq
  less_eq_float_def less_float_def
  flt_def fgt_def fle_def fge_def feq_def
  fcompare_def
  infinity_simps
  zero_simps
  topfloat_simps
  bottomfloat_simps
  float_eq_def

lemma float_cases: "is_nan a ∨ is_infinity a ∨ is_normal a ∨ is_denormal a ∨ is_zero a"
  by (auto simp add: float_defs not_less le_less emax_def unsigned_minus_1_eq_mask)

lemma float_cases_finite: "is_nan a ∨ is_infinity a ∨ is_finite a"
  by (simp add: float_cases is_finite_def)

lemma float_zero1 [simp]: "is_zero 0"
  unfolding float_defs
  by transfer auto

lemma float_zero2 [simp]: "is_zero (- x) ⟷ is_zero x"
  unfolding float_defs
  by transfer auto

lemma emax_pos [simp]: "0 < emax x" "emax x ≠ 0"
  by (auto simp: emax_def)


text ‹The types of floating-point numbers are mutually distinct.›
lemma float_distinct:
  "¬ (is_nan a ∧ is_infinity a)"
  "¬ (is_nan a ∧ is_normal a)"
  "¬ (is_nan a ∧ is_denormal a)"
  "¬ (is_nan a ∧ is_zero a)"
  "¬ (is_infinity a ∧ is_normal a)"
  "¬ (is_infinity a ∧ is_denormal a)"
  "¬ (is_infinity a ∧ is_zero a)"
  "¬ (is_normal a ∧ is_denormal a)"
  "¬ (is_denormal a ∧ is_zero a)"
  by (auto simp: float_defs)

lemma denormal_imp_not_zero: "is_denormal f ⟹ ¬is_zero f"
  by (simp add: is_denormal_def is_zero_def)

lemma normal_imp_not_zero: "is_normal f ⟹ ¬is_zero f"
  by (simp add: is_normal_def is_zero_def)

lemma normal_imp_not_denormal: "is_normal f ⟹ ¬is_denormal f"
  by (simp add: is_normal_def is_denormal_def)

lemma denormal_zero [simp]: "¬is_denormal 0" "¬is_denormal minus_zero"
  using denormal_imp_not_zero float_zero1 float_zero2 by blast+

lemma normal_zero [simp]: "¬is_normal 0" "¬is_normal minus_zero"
  using normal_imp_not_zero float_zero1 float_zero2 by blast+

lemma float_distinct_finite: "¬ (is_nan a ∧ is_finite a)" "¬(is_infinity a ∧ is_finite a)"
  by (auto simp: float_defs)

lemma finite_infinity: "is_finite a ⟹ ¬ is_infinity a"
  by (auto simp: float_defs)

lemma finite_nan: "is_finite a ⟹ ¬ is_nan a"
  by (auto simp: float_defs)

text ‹For every real number, the floating-point numbers closest to it always exists.›
lemma is_closest_exists:
  fixes v :: "('e, 'f)float ⇒ real"
    and s :: "('e, 'f)float set"
  assumes finite: "finite s"
    and non_empty: "s ≠ {}"
  shows "∃a. is_closest v s x a"
  using finite non_empty
proof (induct s rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert z s)
  show ?case
  proof (cases "s = {}")
    case True
    then have "is_closest v (insert z s) x z"
      by (auto simp: is_closest_def)
    then show ?thesis by metis
  next
    case False
    then obtain a where a: "is_closest v s x a"
      using insert by metis
    then show ?thesis
    proof (cases "¦v a - x¦" "¦v z - x¦" rule: le_cases)
      case le
      then show ?thesis
        by (metis insert_iff a is_closest_def)
    next
      case ge
      have "∀b. b ∈ s ⟶ ¦v a - x¦ ≤ ¦v b - x¦"
        by (metis a is_closest_def)
      then have "∀b. b ∈ insert z s ⟶ ¦v z - x¦ ≤ ¦v b - x¦"
        by (metis eq_iff ge insert_iff order.trans)
      then show ?thesis using is_closest_def a
        by (metis insertI1)
    qed
  qed
qed

lemma closest_is_everything:
  fixes v :: "('e, 'f)float ⇒ real"
    and s :: "('e, 'f)float set"
  assumes finite: "finite s"
    and non_empty: "s ≠ {}"
  shows "is_closest v s x (closest v p s x) ∧
    ((∃b. is_closest v s x b ∧ p b) ⟶ p (closest v p s x))"
  unfolding closest_def
  by (rule someI_ex) (metis assms is_closest_exists [of s v x])

lemma closest_in_set:
  fixes v :: "('e, 'f)float ⇒ real"
  assumes "finite s" and "s ≠ {}"
  shows "closest v p s x ∈ s"
  by (metis assms closest_is_everything is_closest_def)

lemma closest_is_closest_finite:
  fixes v :: "('e, 'f)float ⇒ real"
  assumes "finite s" and "s ≠ {}"
  shows "is_closest v s x (closest v p s x)"
  by (metis closest_is_everything assms)

instance float::(len, len) finite proof qed (transfer, simp)

lemma is_finite_nonempty: "{a. is_finite a} ≠ {}"
proof -
  have "0 ∈ {a. is_finite a}"
    unfolding float_defs
    by transfer auto
  then show ?thesis by (metis empty_iff)
qed

lemma closest_is_closest:
  fixes v :: "('e, 'f)float ⇒ real"
  assumes "s ≠ {}"
  shows "is_closest v s x (closest v p s x)"
  by (rule closest_is_closest_finite) (auto simp: assms)


subsection ‹Properties about ordering and bounding›

text ‹Lifting of non-exceptional comparisons.›
lemma float_lt [simp]:
  assumes "is_finite a" "is_finite b"
  shows "a < b ⟷ valof a < valof b"
proof
  assume "valof a < valof b"
  moreover have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms by (auto simp: finite_nan finite_infinity)
  ultimately have "fcompare a b = Lt"
    by (auto simp add: is_infinity_def is_nan_def valof_def fcompare_def)
  then show "a < b" by (auto simp: float_defs)
next
  assume "a < b"
  then have lt: "fcompare a b = Lt"
    by (simp add: float_defs)
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms by (auto simp: finite_nan finite_infinity)
  then show "valof a < valof b"
    using lt assms
    by (simp add: fcompare_def is_nan_def is_infinity_def valof_def split: if_split_asm)
qed

lemma float_eq [simp]:
  assumes "is_finite a" "is_finite b"
  shows "a ≐ b ⟷ valof a = valof b"
proof
  assume *: "valof a = valof b"
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms float_distinct_finite by auto
  with * have "fcompare a b = Eq"
    by (auto simp add: is_infinity_def is_nan_def valof_def fcompare_def)
  then show "a ≐ b" by (auto simp: float_defs)
next
  assume "a ≐ b"
  then have eq: "fcompare a b = Eq"
    by (simp add: float_defs)
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms float_distinct_finite by auto
  then show "valof a = valof b"
    using eq assms
    by (simp add: fcompare_def is_nan_def is_infinity_def valof_def split: if_split_asm)
qed

lemma float_le [simp]:
  assumes "is_finite a" "is_finite b"
  shows "a ≤ b ⟷ valof a ≤ valof b"
proof -
  have "a ≤ b ⟷  a < b ∨ a ≐ b"
    by (auto simp add: float_defs)
  then show ?thesis
    by (auto simp add: assms)
qed

text ‹Reflexivity of equality for non-NaNs.›
lemma float_eq_refl [simp]: "a ≐ a ⟷ ¬ is_nan a"
  by (auto simp: float_defs)


text ‹Properties about ordering.›
lemma float_lt_trans: "is_finite a ⟹ is_finite b ⟹ is_finite c ⟹ a < b ⟹ b < c ⟹ a < c"
  by (auto simp: le_trans)

lemma float_le_less_trans: "is_finite a ⟹ is_finite b ⟹ is_finite c ⟹ a ≤ b ⟹ b < c ⟹ a < c"
  by (auto simp: le_trans)

lemma float_le_trans: "is_finite a ⟹ is_finite b ⟹ is_finite c ⟹ a ≤ b ⟹ b ≤ c ⟹ a ≤ c"
  by (auto simp: le_trans)

lemma float_le_neg: "is_finite a ⟹ is_finite b ⟹ ¬ a < b ⟷ b ≤ a"
  by auto


text ‹Properties about bounding.›

lemma float_le_plus_infinity [simp]: "¬ is_nan a ⟹ a ≤ plus_infinity"
  unfolding float_defs
  by auto

lemma minus_infinity_le_float [simp]: "¬ is_nan a ⟹ minus_infinity ≤ a"
  unfolding float_defs
  by auto

lemma zero_le_topfloat [simp]: "0 ≤ topfloat" "- 0 ≤ topfloat"
  by (auto simp: float_defs field_simps power_gt1_lemma of_nat_diff mask_eq_exp_minus_1)

lemma LENGTH_contr:
  "Suc 0 < LENGTH('e) ⟹ 2 ^ LENGTH('e::len) ≤ Suc (Suc 0) ⟹ False"
  by (metis le_antisym len_gt_0 n_less_equal_power_2 not_less_eq numeral_2_eq_2 one_le_numeral
      self_le_power)

lemma valof_topfloat: "valof (topfloat::('e, 'f)float) = largest TYPE(('e, 'f)float)"
  if "LENGTH('e) > 1"
  using that LENGTH_contr
  by (auto simp add: emax_eq largest_def divide_simps float_defs of_nat_diff mask_eq_exp_minus_1)

lemma float_frac_le: "fraction a ≤ 2^LENGTH('f) - 1"
  for a::"('e, 'f)float"
  unfolding float_defs
  using less_Suc_eq_le
  by transfer fastforce

lemma float_exp_le: "is_finite a ⟹ exponent a ≤ emax TYPE(('e, 'f)float) - 1"
  for a::"('e, 'f)float"
  unfolding float_defs
  by auto

lemma float_sign_le: "(-1::real)^(sign a) = 1 ∨ (-1::real)^(sign a) = -1"
  by (metis neg_one_even_power neg_one_odd_power)

lemma exp_less: "a ≤ b ⟹ (2::real)^a ≤ 2^b" for a b :: nat
  by auto

lemma div_less: "a ≤ b ∧ c > 0 ⟹ a/c ≤ b/c" for a b c :: "'a::linordered_field"
  by (metis divide_le_cancel less_asym)

lemma finite_topfloat: "is_finite topfloat"
  unfolding float_defs
  by auto

lemmas float_leI = float_le[THEN iffD2]

lemma factor_minus: "x * a - x = x * (a - 1)"
  for x a::"'a::comm_semiring_1_cancel"
  by (simp add: algebra_simps)

lemma real_le_power_numeral_diff: "real a ≤ numeral b ^ n - 1 ⟷ a ≤ numeral b ^ n - 1"
  by (metis (mono_tags, lifting) of_nat_1 of_nat_diff of_nat_le_iff of_nat_numeral
      one_le_numeral one_le_power semiring_1_class.of_nat_power)

definition denormal_exponent::"('e, 'f)float itself ⇒ int" where
  "denormal_exponent x = 1 - (int (LENGTH('f)) + int (bias TYPE(('e, 'f)float)))"

definition normal_exponent::"('e, 'f)float ⇒ int" where
  "normal_exponent x = int (exponent x) - int (bias TYPE(('e, 'f)float)) - int (LENGTH('f))"

definition denormal_mantissa::"('e, 'f)float ⇒ int" where
  "denormal_mantissa x = (-1::int)^sign x * int (fraction x)"

definition normal_mantissa::"('e, 'f)float ⇒ int" where
  "normal_mantissa x = (-1::int)^sign x * (2^LENGTH('f) + int (fraction x))"

lemma unat_one_word_le: "unat a ≤ Suc 0" for a::"1 word"
  using unat_lt2p[of a]
  by auto

lemma one_word_le: "a ≤ 1" for a::"1 word"
  by (auto simp: word_le_nat_alt unat_one_word_le)

lemma sign_cases[case_names pos neg]:
  obtains "sign x = 0" | "sign x = 1"
proof cases
  assume "sign x = 0"
  then show ?thesis ..
next
  assume "sign x ≠ 0"
  have "sign x ≤ 1"
    by transfer (auto simp: unat_one_word_le)
  then have "sign x = 1" using ‹sign x ≠ 0›
    by auto
  then show ?thesis ..
qed

lemma is_infinity_cases:
  assumes "is_infinity x"
  obtains "x = plus_infinity" | "x = minus_infinity"
proof (cases rule: sign_cases[of x])
  assume "sign x = 0"
  then have "x = plus_infinity" using assms
    apply (unfold float_defs)
    apply transfer
    apply (auto simp add: unat_eq_of_nat emax_def of_nat_mask_eq)
    done
  then show ?thesis ..
next
  assume "sign x = 1"
  then have "x = minus_infinity" using assms
    apply (unfold float_defs)
    apply transfer
    apply (auto simp add: unat_eq_of_nat emax_def of_nat_mask_eq)
    done
  then show ?thesis ..
qed

lemma is_zero_cases:
  assumes "is_zero x"
  obtains "x = 0" | "x = - 0"
proof (cases rule: sign_cases[of x])
  assume "sign x = 0"
  then have "x = 0" using assms
    unfolding float_defs
    by transfer (auto simp: emax_def unat_eq_0)
  then show ?thesis ..
next
  assume "sign x = 1"
  then have "x = minus_zero" using assms
    unfolding float_defs
    by transfer (auto simp: emax_def unat_eq_of_nat)
  then show ?thesis ..
qed

lemma minus_minus_float [simp]: "- (-f) = f" for f::"('e, 'f)float"
  by transfer auto

lemma sign_minus_float: "sign (-f) = (1 - sign f)" for f::"('e, 'f)float"
  by transfer (auto simp: unat_eq_1 one_word_le unat_sub)

lemma exponent_uminus [simp]: "exponent (- f) = exponent f" by transfer auto
lemma fraction_uminus [simp]: "fraction (- f) = fraction f" by transfer auto

lemma is_normal_minus_float [simp]: "is_normal (-f) = is_normal f" for f::"('e, 'f)float"
  by (auto simp: is_normal_def)

lemma is_denormal_minus_float [simp]: "is_denormal (-f) = is_denormal f" for f::"('e, 'f)float"
  by (auto simp: is_denormal_def)

lemma bitlen_normal_mantissa:
  "bitlen (abs (normal_mantissa x)) = Suc LENGTH('f)" for x::"('e, 'f)float"
proof -
  have "fraction x < 2 ^ LENGTH('f)"
    using float_frac_le[of x]
    by (metis One_nat_def Suc_pred le_imp_less_Suc pos2 zero_less_power)
  moreover have "- int (fraction x) ≤ 2 ^ LENGTH('f)"
    using negative_zle_0 order_trans zero_le_numeral zero_le_power by blast
  ultimately show ?thesis
    by (cases x rule: sign_cases)
      (auto simp: bitlen_le_iff_power bitlen_ge_iff_power nat_add_distrib
        normal_mantissa_def intro!: antisym)
qed

lemma less_int_natI: "x < y" if "0 ≤ x" "nat x < nat y"
  using that by arith

lemma normal_exponent_bounds_int:
  "2 - 2 ^ (LENGTH('e) - 1) - int LENGTH('f) ≤ normal_exponent x"
  "normal_exponent x ≤ 2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1"
  if "is_normal x"
  for x::"('e, 'f)float"
  using that
   apply (auto simp add: normal_exponent_def is_normal_def emax_eq bias_def diff_le_eq diff_less_eq
    mask_eq_exp_minus_1 of_nat_diff simp flip: zless_nat_eq_int_zless power_Suc)
  apply (simp flip: power_Suc mask_eq_exp_minus_1 add: nat_mask_eq)
  apply (simp add: mask_eq_exp_minus_1)
  done

lemmas of_int_leI = of_int_le_iff[THEN iffD2]

lemma normal_exponent_bounds_real:
  "2 - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) ≤ normal_exponent x"
  "normal_exponent x ≤ 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1"
  if "is_normal x"
  for x::"('e, 'f)float"
  subgoal by (rule order_trans[OF _ of_int_leI[OF normal_exponent_bounds_int(1)[OF that]]]) auto
  subgoal by (rule order_trans[OF of_int_leI[OF normal_exponent_bounds_int(2)[OF that]]]) auto
  done

lemma float_eqI:
  "x = y" if "sign x = sign y" "fraction x = fraction y" "exponent x = exponent y"
  using that by transfer (auto simp add: word_unat_eq_iff)

lemma float_induct[induct type:float, case_names normal denormal neg zero infinity nan]:
  fixes a::"('e, 'f)float"
  assumes normal:
    "⋀x. is_normal x ⟹ valof x = normal_mantissa x * 2 powr normal_exponent x ⟹ P x"
  assumes denormal:
    "⋀x. is_denormal x ⟹
      valof x = denormal_mantissa x * 2 powr denormal_exponent TYPE(('e, 'f)float) ⟹
      P x"
  assumes zero: "P 0" "P minus_zero"
  assumes infty: "P plus_infinity" "P minus_infinity"
  assumes nan: "⋀x. is_nan x ⟹ P x"
  shows "P a"
proof -
  from float_cases[of a]
  consider "is_nan a" | "is_infinity a" | "is_normal a" | "is_denormal a" | "is_zero a" by blast
  then show ?thesis
  proof cases
    case 1
    then show ?thesis by (rule nan)
  next
    case 2
    then consider "a = plus_infinity" | "a = minus_infinity" by (rule is_infinity_cases)
    then show ?thesis
      by cases (auto intro: infty)
  next
    case hyps: 3
    from hyps have "valof a = normal_mantissa a * 2 powr normal_exponent a"
      by (cases a rule: sign_cases)
        (auto simp: valof_eq normal_mantissa_def normal_exponent_def is_normal_def
          powr_realpow[symmetric] powr_diff powr_add field_simps)
    from hyps this show ?thesis
      by (rule normal)
  next
    case hyps: 4
    from hyps have "valof a = denormal_mantissa a * 2 powr denormal_exponent TYPE(('e, 'f)float)"
      by (cases a rule: sign_cases)
        (auto simp: valof_eq denormal_mantissa_def denormal_exponent_def is_denormal_def
          powr_realpow[symmetric] powr_diff powr_add field_simps)
    from hyps this show ?thesis
      by (rule denormal)
  next
    case 5
    then consider "a = 0" | "a = minus_zero" by (rule is_zero_cases)
    then show ?thesis
      by cases (auto intro: zero)
  qed
qed

lemma infinite_infinity [simp]: "¬ is_finite plus_infinity" "¬ is_finite minus_infinity"
  by (auto simp: is_finite_def is_normal_def infinity_simps is_denormal_def is_zero_def)

lemma nan_not_finite [simp]: "is_nan x ⟹ ¬ is_finite x"
  using float_distinct_finite(1) by blast

lemma valof_nonneg:
  "valof x ≥ 0" if "sign x = 0" for x::"('e, 'f)float"
  by (auto simp: valof_eq that)

lemma valof_nonpos:
  "valof x ≤ 0" if "sign x = 1" for x::"('e, 'f)float"
  using that
  by (auto simp: valof_eq is_finite_def)

lemma real_le_intI: "x ≤ y" if "floor x ≤ floor y" "x ∈ ℤ" for x y::real
  using that(2,1)
  by (induction rule: Ints_induct) (auto elim!: Ints_induct simp: le_floor_iff)

lemma real_of_int_le_2_powr_bitlenI:
  "real_of_int x ≤ 2 powr n - 1" if "bitlen (abs x) ≤ m" "m ≤ n"
proof -
  have "real_of_int x ≤ abs (real_of_int x)" by simp
  also have "… < 2 powr (bitlen (abs x))"
    by (rule abs_real_le_2_powr_bitlen)
  finally have "real_of_int x ≤ 2 powr (bitlen (abs x)) - 1"
    by (auto simp: powr_real_of_int bitlen_nonneg intro!: real_le_intI)
  also have "… ≤ 2 powr m - 1"
    by (simp add: that)
  also have "… ≤ 2 powr n - 1"
    by (simp add: that)
  finally show ?thesis .
qed

lemma largest_eq:
  "largest TYPE(('e, 'f)float) =
    (2 ^ (LENGTH('f) + 1) - 1) * 2 powr real_of_int (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)"
proof -
  have "2 ^ LENGTH('e) - 1 - 1 = (2::nat) ^ LENGTH('e) - 2"
    by arith
  then have "largest TYPE(('e, 'f)float) =
    (2 ^ (LENGTH('f) + 1) - 1) *
    2 powr (real (2 ^ LENGTH('e) - 2) + 1 - real (2 ^ (LENGTH('e) - 1)) - LENGTH('f))"
    by (auto simp add: largest_def emax_eq bias_def powr_minus field_simps powr_diff powr_add of_nat_diff
      mask_eq_exp_minus_1 simp flip: powr_realpow)
  also
  have "2 ^ LENGTH('e) ≥ (2::nat)"
    by (simp add: self_le_power)
  then have "(real (2 ^ LENGTH('e) - 2) + 1 - real (2 ^ (LENGTH('e) - 1)) - LENGTH('f)) =
    (real (2 ^ LENGTH('e)) - 2 ^ (LENGTH('e) - 1) - LENGTH('f)) - 1"
    by (auto simp add: of_nat_diff)
  also have "real (2 ^ LENGTH('e)) = 2 ^ LENGTH('e)" by auto
  also have "(2 ^ LENGTH('e) - 2 ^ (LENGTH('e) - 1) - real LENGTH('f) - 1) =
    real_of_int ((2 ^ (LENGTH('e) - 1) - int (LENGTH('f)) - 1))"
    by (simp, subst power_Suc[symmetric], simp)
  finally show ?thesis by simp
qed

lemma bitlen_denormal_mantissa:
  "bitlen (abs (denormal_mantissa x)) ≤ LENGTH('f)" for x::"('e, 'f)float"
proof -
  have "fraction x < 2 ^ LENGTH('f)"
    using float_frac_le[of x]
    by (metis One_nat_def Suc_pred le_imp_less_Suc pos2 zero_less_power)
  moreover have "- int (fraction x) ≤ 2 ^ LENGTH('f)"
    using negative_zle_0 order_trans zero_le_numeral zero_le_power by blast
  ultimately show ?thesis
    by (cases x rule: sign_cases)
      (auto simp: bitlen_le_iff_power denormal_mantissa_def intro!: antisym)
qed

lemma float_le_topfloat:
  fixes a::"('e, 'f)float"
  assumes "is_finite a" "LENGTH('e) > 1"
  shows "a ≤ topfloat"
  using assms(1)
proof (induction a rule: float_induct)
  case (normal x)
  note normal(2)
  also have "real_of_int (normal_mantissa x) * 2 powr real_of_int (normal_exponent x) ≤
    (2 powr (LENGTH('f) + 1) - 1) * 2 powr (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)"
    using normal_exponent_bounds_real(2)[OF ‹is_normal x›]
    by (auto intro!: mult_mono real_of_int_le_2_powr_bitlenI
        simp: bitlen_normal_mantissa powr_realpow[symmetric] ge_one_powr_ge_zero)
  also have "… = largest TYPE(('e, 'f) IEEE.float)"
    unfolding largest_eq
    by (auto simp: powr_realpow powr_add)
  also have "… = valof (topfloat::('e, 'f) float)"
    using assms
    by (simp add: valof_topfloat)
  finally show ?case
    by (intro float_leI normal finite_topfloat)
next
  case (denormal x)
  note denormal(2)
  also
  have "3 ≤ 2 powr (1 + real (LENGTH('e) - Suc 0))"
  proof -
    have "3 ≤ 2 powr (2::real)" by simp
    also have "… ≤ 2 powr (1 + real (LENGTH('e) - Suc 0))"
      using assms
      by (subst powr_le_cancel_iff) auto
    finally show ?thesis .
  qed
  then have "real_of_int (denormal_mantissa x) * 2 powr real_of_int (denormal_exponent TYPE(('e, 'f)float)) ≤
    (2 powr (LENGTH('f) + 1) - 1) * 2 powr (2 ^ (LENGTH('e) - 1) - int LENGTH('f) - 1)"
    using bitlen_denormal_mantissa[of x]
    by (auto intro!: mult_mono real_of_int_le_2_powr_bitlenI
        simp: bitlen_normal_mantissa powr_realpow[symmetric] ge_one_powr_ge_zero mask_eq_exp_minus_1
        denormal_exponent_def bias_def powr_mult_base of_nat_diff)
  also have "… ≤ largest TYPE(('e, 'f) IEEE.float)"
    unfolding largest_eq
    by (rule mult_mono)
      (auto simp: powr_realpow powr_add power_Suc[symmetric] simp del: power_Suc)
  also have "… = valof (topfloat::('e, 'f) float)"
    using assms
    by (simp add: valof_topfloat)
  finally show ?case
    by (intro float_leI denormal finite_topfloat)
qed auto

lemma float_val_le_largest:
  "valof a ≤ largest TYPE(('e, 'f)float)"
  if "is_finite a" "LENGTH('e) > 1"
  for a::"('e, 'f)float"
  by (metis that finite_topfloat float_le float_le_topfloat valof_topfloat)

lemma float_val_lt_threshold:
  "valof a < threshold TYPE(('e, 'f)float)"
  if "is_finite a" "LENGTH('e) > 1"
  for a::"('e, 'f)float"
proof -
  have "valof a ≤ largest TYPE(('e, 'f)float)"
    by (rule float_val_le_largest [OF that])
  also have "… < threshold TYPE(('e, 'f)float)"
    by (auto simp: largest_def threshold_def divide_simps)
  finally show ?thesis .
qed


subsection ‹Algebraic properties about basic arithmetic›

text ‹Commutativity of addition.›
lemma
  assumes "is_finite a" "is_finite b"
  shows float_plus_comm_eq: "a + b = b + a"
    and float_plus_comm: "is_finite (a + b) ⟹ (a + b) ≐ (b + a)" (*FIXME: this should hold unconditionally?*)
proof -
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms by (auto simp: finite_nan finite_infinity)
  then show "a + b = b + a"
    by (simp add: float_defs fadd_def plus_float_def add.commute)
  then show "is_finite (a + b) ⟹ (a + b) ≐ (b + a)"
    by (metis float_eq)
qed

text ‹The floating-point number ‹a› falls into the same category as the negation of ‹a›.›
lemma is_zero_uminus [simp]: "is_zero (- a) ⟷ is_zero a"
  by (simp add: is_zero_def)

lemma is_infinity_uminus [simp]: "is_infinity (- a) = is_infinity a"
  by (simp add: is_infinity_def)

lemma is_finite_uminus [simp]: "is_finite (- a) ⟷ is_finite a"
  by (simp add: is_finite_def)

lemma is_nan_uminus [simp]: "is_nan (- a) ⟷ is_nan a"
  by (simp add: is_nan_def)

text ‹The sign of ‹a› and the sign of ‹a›'s negation are different.›
lemma float_neg_sign: "sign a ≠ sign (- a)"
  by (cases a rule: sign_cases) (auto simp: sign_minus_float)

lemma float_neg_sign1: "sign a = sign (- b) ⟷ sign a ≠ sign b"
  by (metis float_neg_sign sign_cases)

lemma valof_uminus:
  assumes "is_finite a"
  shows "valof (- a) = - valof a"
  by (cases a rule: sign_cases)  (auto simp: valof_eq sign_minus_float)

text ‹Showing ‹a + (- b) ≐ a - b›.›
lemma float_plus_minus:
  assumes "is_finite a" "is_finite b" "is_finite (a - b)"
  shows "(a + - b) ≐ (a - b)"
proof -
  have nab: "¬ is_nan a" "¬ is_nan (- b)" "¬ is_infinity a" "¬ is_infinity (-  b)"
    using assms by (auto simp: finite_nan finite_infinity)
  have "a - b = (zerosign
        (if is_zero a ∧ is_zero b ∧ sign a ≠ sign b then (sign a) else 0)
        (round RNE (valof a - valof b)))"
    using nab
    by (auto simp: minus_float_def fsub_def)
  also have "… =
    (zerosign
        (if is_zero a ∧ is_zero (- b) ∧ sign a = sign (- b) then sign a else 0)
        (round RNE (valof a + valof (- b))))"
    using assms
    by (simp add: float_neg_sign1 valof_uminus)
  also have "… = a + - b"
    using nab by (auto simp: float_defs fadd_def plus_float_def)
  finally show ?thesis
    using assms by (metis float_eq)
qed

lemma finite_bottomfloat: "is_finite bottomfloat"
  by (simp add: finite_topfloat)

lemma bottomfloat_eq_m_largest: "valof (bottomfloat::('e, 'f)float) = - largest TYPE(('e, 'f)float)"
  if "LENGTH('e) > 1"
  using that
  by (auto simp: valof_topfloat valof_uminus finite_topfloat)

lemma float_val_ge_bottomfloat: "valof a ≥ valof (bottomfloat::('e, 'f)float)"
  if "LENGTH('e) > 1" "is_finite a"
  for a::"('e,'f)float"
proof -
  have "- a ≤ topfloat"
    using that
    by (auto intro: float_le_topfloat)
  then show ?thesis
    using that
    by (auto simp: valof_uminus finite_topfloat)
qed

lemma float_ge_bottomfloat: "is_finite a ⟹ a ≥ bottomfloat"
  if "LENGTH('e) > 1" "is_finite a"
  for a::"('e,'f)float"
  by (metis finite_bottomfloat float_le float_val_ge_bottomfloat that)

lemma float_val_ge_largest:
  fixes a::"('e,'f)float"
  assumes "LENGTH('e) > 1" "is_finite a"
  shows "valof a ≥ - largest TYPE(('e,'f)float)"
proof -
  have "- largest TYPE(('e,'f)float) = valof (bottomfloat::('e,'f)float)"
    using assms
    by (simp add: bottomfloat_eq_m_largest)
  also have "… ≤ valof a"
    using assms by (simp add: float_val_ge_bottomfloat)
  finally show ?thesis .
qed

lemma float_val_gt_threshold:
  fixes a::"('e,'f)float"
  assumes "LENGTH('e) > 1" "is_finite a"
  shows "valof a > - threshold TYPE(('e,'f)float)"
proof -
  have largest: "valof a ≥ -largest TYPE(('e,'f)float)"
    using assms by (metis float_val_ge_largest)
  then have "-largest TYPE(('e,'f)float) > - threshold TYPE(('e,'f)float)"
    by (auto simp: bias_def threshold_def largest_def divide_simps)
  then show ?thesis
    by (metis largest less_le_trans)
qed

text ‹Showing ‹abs (- a) = abs a›.›
lemma float_abs [simp]: "¬ is_nan a ⟹ abs (- a) = abs a"
  by (metis IEEE.abs_float_def float_neg_sign1 minus_minus_float zero_simps(1))

lemma neg_zerosign: "- (zerosign s a) = zerosign (1 - s) (- a)"
  by (auto simp: zerosign_def)


subsection ‹Properties about Rounding Errors›

definition error :: "('e, 'f)float itself ⇒ real ⇒ real"
  where "error _ x = valof (round RNE x::('e, 'f)float) - x"

lemma bound_at_worst_lemma:
  fixes a::"('e, 'f)float"
  assumes threshold: "¦x¦ < threshold TYPE(('e, 'f)float)"
  assumes finite: "is_finite a"
  shows "¦valof (round RNE x::('e, 'f)float) - x¦ ≤ ¦valof a - x¦"
proof -
  have *: "(round RNE x::('e,'f)float) =
      closest valof (λa. even (fraction a)) {a. is_finite a} x"
    using threshold finite
    by auto
  have "is_closest (valof) {a. is_finite a} x (round RNE x::('e,'f)float)"
    using is_finite_nonempty
    unfolding *
    by (intro closest_is_closest) auto
  then show ?thesis
    using finite is_closest_def by (metis mem_Collect_eq)
qed

lemma error_at_worst_lemma:
  fixes a::"('e, 'f)float"
  assumes threshold: "¦x¦ < threshold TYPE(('e, 'f)float)"
    and "is_finite a"
  shows "¦error TYPE(('e, 'f)float) x¦ ≤ ¦valof a - x¦ "
  unfolding error_def
  by (rule bound_at_worst_lemma; fact)

lemma error_is_zero [simp]:
  fixes a::"('e, 'f)float"
  assumes "is_finite a" "1 < LENGTH('e)"
  shows "error TYPE(('e, 'f)float) (valof a) = 0"
proof -
  have "¦valof a¦ < threshold TYPE(('e, 'f)float)"
    by (metis abs_less_iff minus_less_iff float_val_gt_threshold float_val_lt_threshold assms)
  then show ?thesis
    by (metis abs_le_zero_iff abs_zero diff_self error_at_worst_lemma assms(1))
qed

lemma is_finite_zerosign [simp]: "is_finite (zerosign s a) ⟷ is_finite a"
  by (auto simp: zerosign_def is_finite_def)

lemma is_finite_closest: "is_finite (closest (v::_⇒real) p {a. is_finite a} x)"
  using closest_is_closest[OF is_finite_nonempty, of v x p]
  by (auto simp: is_closest_def)

lemma defloat_float_zerosign_round_finite:
  assumes threshold: "¦x¦ < threshold TYPE(('e, 'f)float)"
  shows "is_finite (zerosign s (round RNE x::('e, 'f)float))"
proof -
  have "(round RNE x::('e, 'f)float) =
      (closest valof (λa. even (fraction a)) {a. is_finite a} x)"
    using threshold by (metis (full_types) abs_less_iff leD le_minus_iff round.simps(1))
  then have "is_finite (round RNE x::('e, 'f)float)"
    by (metis is_finite_closest)
  then show ?thesis
    using is_finite_zerosign by auto
qed

lemma valof_zero [simp]: "valof 0 = 0" "valof minus_zero = 0"
  by (auto simp add: zerosign_def valof_eq zero_simps)

lemma signzero_zero:
  "is_zero a ⟹ valof (zerosign s a) = 0"
  by (auto simp add: zerosign_def)

lemma val_zero: "is_zero a ⟹ valof a = 0"
  by (cases a rule: is_zero_cases) auto

lemma float_add:
  fixes a b::"('e, 'f)float"
  assumes "is_finite a"
    and "is_finite b"
    and threshold: "¦valof a + valof b¦ < threshold TYPE(('e, 'f)float)"
  shows finite_float_add: "is_finite (a + b)"
    and error_float_add:  "valof (a + b) = valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b)"
proof -
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms float_distinct_finite by auto
  then have ab: "(a + b) =
    (zerosign
      (if is_zero a ∧ is_zero b ∧ sign a = sign b then (sign a) else 0)
      (round RNE (valof a + valof b)))"
    using assms by (auto simp add: float_defs fadd_def plus_float_def)
  then show "is_finite ((a + b))"
    by (metis threshold defloat_float_zerosign_round_finite)
  have val_ab: "valof (a + b) =
    valof (zerosign
      (if is_zero a ∧ is_zero b ∧ sign a = sign b then (sign a) else 0)
      (round RNE (valof a + valof b)::('e, 'f)float))"
    by (auto simp: ab is_infinity_def is_nan_def valof_def)
  show "valof (a + b) = valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b)"
  proof (cases "is_zero (round RNE (valof a + valof b)::('e, 'f)float)")
    case True
    have "valof a + valof b + error TYPE(('e, 'f)float) (valof a + valof b) =
        valof (round RNE (valof a + valof b)::('e, 'f)float)"
      unfolding error_def
      by simp
    then show ?thesis
      by (metis True signzero_zero val_zero val_ab)
  next
    case False
    then show ?thesis
      by (metis ab add.commute eq_diff_eq' error_def zerosign_def)
  qed
qed

lemma float_sub:
  fixes a b::"('e, 'f)float"
  assumes "is_finite a"
    and "is_finite b"
    and threshold: "¦valof a - valof b¦ < threshold TYPE(('e, 'f)float)"
  shows finite_float_sub: "is_finite (a - b)"
    and error_float_sub: "valof (a - b) = valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b)"
proof -
  have "¬ is_nan a" and "¬ is_nan b" and "¬ is_infinity a" and "¬ is_infinity b"
    using assms by (auto simp: finite_nan finite_infinity)
  then have ab: "a - b =
    (zerosign
      (if is_zero a ∧ is_zero b ∧ sign a ≠ sign b then sign a else 0)
      (round RNE (valof a - valof b)))"
    using assms by (auto simp add: float_defs fsub_def minus_float_def)
  then show "is_finite (a - b)"
   by (metis threshold defloat_float_zerosign_round_finite)
  have val_ab: "valof (a - b) =
    valof (zerosign
      (if is_zero a ∧ is_zero b ∧ sign a ≠ sign b then sign a else 0)
      (round RNE (valof a - valof b)::('e, 'f)float))"
    by (auto simp: ab is_infinity_def is_nan_def valof_def)
  show "valof (a - b) = valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b)"
  proof (cases "is_zero (round RNE (valof a - valof b)::('e, 'f)float)")
    case True
    have "valof a - valof b + error TYPE(('e, 'f)float) (valof a - valof b) =
        valof (round RNE (valof a - valof b)::('e, 'f)float)"
      unfolding error_def by simp
    then show ?thesis
      by (metis True signzero_zero val_zero val_ab)
  next
    case False
    then show ?thesis
      by (metis ab add.commute eq_diff_eq' error_def zerosign_def)
  qed
qed

lemma float_mul:
  fixes a b::"('e, 'f)float"
  assumes "is_finite a"
    and "is_finite b"
    and threshold: "¦valof a * valof b¦ < threshold TYPE(('e, 'f)float)"
  shows finite_float_mul: "is_finite (a * b)"
    and error_float_mul: "valof (a * b) = valof a * valof b + error TYPE(('e, 'f)float) (valof a * valof b)"
proof -
  have non: "¬ is_nan a" "¬ is_nan b" "¬ is_infinity a" "¬ is_infinity b"
    using assms float_distinct_finite by auto
  then have ab: "a * b =
    (zerosign (of_bool (sign a ≠ sign b))
      (round RNE (valof a * valof b)::('e, 'f)float))"
    using assms by (auto simp: float_defs fmul_def times_float_def)
  then show "is_finite (a * b)"
    by (metis threshold defloat_float_zerosign_round_finite)
  have val_ab: "valof (a * b) =
      valof (zerosign (of_bool (sign a ≠ sign b))
        (round RNE (valof a * valof b)::('e, 'f)float))"
    by (auto simp: ab float_defs of_bool_def)
  show "valof (a * b) = valof a * valof b + error TYPE(('e, 'f)float) (valof a * valof b)"
  proof (cases "is_zero (round RNE (valof a * valof b)::('e, 'f)float)")
    case True
    have "valof a * valof b + error TYPE(('e, 'f)float)  (valof a * valof b) =
        valof (round RNE (valof a * valof b)::('e, 'f)float)"
      unfolding error_def
      by simp
    then show ?thesis
      by (metis True signzero_zero val_zero val_ab)
  next
    case False then show ?thesis
      by (metis ab add.commute eq_diff_eq' error_def zerosign_def)
  qed
qed

lemma float_div:
  fixes a b::"('e, 'f)float"
  assumes "is_finite a"
    and "is_finite b"
    and not_zero: "¬ is_zero b"
    and threshold: "¦valof a / valof b¦ < threshold TYPE(('e, 'f)float)"
  shows finite_float_div: "is_finite (a / b)"
    and error_float_div: "valof (a / b) = valof a / valof b + error TYPE(('e, 'f)float) (valof a / valof b)"
proof -
  have ab: "a / b =
    (zerosign (of_bool (sign a ≠ sign b))
      (round RNE (valof a / valof b)))"
     using assms
     by (simp add: divide_float_def fdiv_def finite_infinity finite_nan not_zero float_defs [symmetric])
  then show "is_finite (a / b)"
    by (metis threshold defloat_float_zerosign_round_finite)
  have val_ab: "valof (a / b) =
      valof (zerosign (of_bool (sign a ≠ sign b))
        (round RNE (valof a / valof b))::('e, 'f)float)"
    by (auto simp: ab float_defs of_bool_def)
  show "valof (a / b) = valof a / valof b + error TYPE(('e, 'f)float)  (valof a / valof b)"
  proof (cases "is_zero (round RNE (valof a / valof b)::('e, 'f)float)")
    case True
    have "valof a / valof b + error TYPE(('e, 'f)float) (valof a / valof b) =
        valof (round RNE (valof a / valof b)::('e, 'f)float)"
      unfolding error_def
      by simp
    then show ?thesis
      by (metis True signzero_zero val_zero val_ab)
  next
    case False then show ?thesis
      by (metis ab add.commute eq_diff_eq' error_def zerosign_def)
  qed
qed

lemma valof_one [simp]: "valof (1 :: ('e, 'f) float) = of_bool (LENGTH('e) > 1)"
  apply transfer
  apply (auto simp add: bias_def unat_mask_eq simp flip: mask_eq_exp_minus_1)
  apply (simp add: mask_eq_exp_minus_1)
  done

end