header {* Rationals Floats and Reals *}
theory Float_Rat_Real
imports
  Float_Real
begin

subsection {* rational of float *}

definition rat_of_float::"float\<Rightarrow>rat" where "rat_of_float x = (THE y. real_of_rat y = x)"

lemma real_of_rat_Fract: "real_of_rat (Fract a b) = a / b"
  by (metis Ratreal_def Real.zero_real_code divide_zero of_rat_rat rat_number_collapse(6) real_of_int_def real_of_int_zero)

lemma numeral_powr_int: "b > 0 \<Longrightarrow> (numeral x::real) powr real b = real ((numeral x::int)^ nat b)"
  using powr_realpow[of 2 "nat b"] by (auto simp: powr_realpow[symmetric])

text {* TODO: serialize to native power! *}

lemma compute_rat_of_float[code]:
  "rat_of_float (Float a b) = Fract (if b > 0 then a * 2 ^ nat b else a) (if b < 0 then 2 ^ nat (-b) else 1)"
  unfolding rat_of_float_def
  apply (rule the_equality)
  apply (auto simp: real_of_rat_Fract eq_rat field_simps powr_realpow[symmetric] powr_add[symmetric])
  apply (case_tac y)
  apply (auto simp: real_of_rat_Fract field_simps eq_rat numeral_powr_int)
  apply (metis real_of_int_inject real_of_int_mult real_of_int_power real_of_ints(8))
  apply (case_tac y)
  apply (auto simp: real_of_rat_Fract field_simps eq_rat numeral_powr_int)
proof -
  case (goal1 c d)
  hence "2 powr real (-b) * real c = real d * real a"
    by (auto simp: powr_add[symmetric])
  thus ?case using goal1(2-4)
    apply (auto simp: real_of_rat_Fract field_simps eq_rat numeral_powr_int powr_realpow)
    apply (subst real_of_int_inject[symmetric])
    apply (simp add: powr_realpow[symmetric])
    done
next
  case goal2
  thus ?case
    by (metis divide_1 of_rat_eq_iff real_of_one real_of_rat_Fract)
qed

subsection {* rational representations... *}

text {* TODO: work entirely on rat? use quotients of floats?*}
subsection {* to rat *}

definition rat_of_real::"real\<Rightarrow>rat" where "rat_of_real x = (THE y. real_of_rat y = x)"

lemma compute_rat_of_real[code]: "rat_of_real (Floatreal a) = rat_of_float a"
  by (auto simp: rat_of_real_def rat_of_float_def)


subsection {* float real of rat *}

definition lreal_of_rat::"nat\<Rightarrow>rat\<Rightarrow>real"
  where "lreal_of_rat p x = (let (a, b) = quotient_of x in real_divl p a b)"

definition ureal_of_rat::"nat\<Rightarrow>rat\<Rightarrow>real"
  where "ureal_of_rat p x = (let (a, b) = quotient_of x in real_divl p a b)"

definition real_err_of_rat::"nat\<Rightarrow>rat\<Rightarrow>real*real"
  where "real_err_of_rat p x =
    (let
      a = lreal_of_rat p x;
      b = ureal_of_rat p x;
      ea = \<bar>rat_of_real a - x\<bar>;
      eb = \<bar>rat_of_real b - x\<bar>
    in if ea \<le> eb then (a, ureal_of_rat p ea) else (b, ureal_of_rat p eb))"

end
