Theory Is_Rat_To_Rat

(*  
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
*)
section ‹Conversions to Rational Numbers›

text ‹We define a class which provides tests whether a number is rational, and
  a conversion from to rational numbers. 
  These conversion functions are principle the inverse functions of \emph{of-rat}, but
  they can be implemented for individual types more efficiently.
  
  Similarly, we define tests and conversions between integer and rational numbers.›

theory Is_Rat_To_Rat
imports 
  Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
begin

class is_rat = field_char_0 +
  fixes is_rat :: "'a ⇒ bool"
  and to_rat :: "'a ⇒ rat"
  assumes is_rat[simp]: "is_rat x = (x ∈ ℚ)"
  and to_rat: "to_rat x = (if x ∈ ℚ then (THE y. x = of_rat y) else 0)"

lemma of_rat_to_rat[simp]: "x ∈ ℚ ⟹ of_rat (to_rat x) = x"
  unfolding to_rat Rats_def by auto

lemma to_rat_of_rat[simp]: "to_rat (of_rat x) = x" unfolding to_rat by simp

instantiation rat :: is_rat
begin
definition "is_rat_rat (x :: rat) = True"
definition "to_rat_rat (x :: rat) = x"
  instance
  by (intro_classes, auto simp: is_rat_rat_def to_rat_rat_def Rats_def)
end

text ‹The definition for reals at the moment is not executable, but it will become
  executable after loading the real algebraic numbers theory.›
instantiation real :: is_rat
begin
definition "is_rat_real (x :: real) = (x ∈ ℚ)"
definition "to_rat_real (x :: real) = (if x ∈ ℚ then (THE y. x = of_rat y) else 0)"
  instance by (intro_classes, auto simp: is_rat_real_def to_rat_real_def)
end

lemma of_nat_complex: "of_nat n = Complex (of_nat n) 0"
  by (simp add: complex_eqI)

lemma of_int_complex: "of_int z = Complex (of_int z) 0"
  by (simp add: complex_eq_iff)

lemma of_rat_complex: "of_rat q = Complex (of_rat q) 0"
proof -
  obtain d n where dn: "quotient_of q = (d,n)" by force
  from quotient_of_div[OF dn] have q: "q = of_int d / of_int n" by auto
  then have "of_rat q = complex_of_real (real_of_rat q) ∨ (0::complex) = of_int n ∨ 0 = real_of_int n"
    by (simp add: of_rat_divide q)
  then show ?thesis
    using Complex_eq_0 complex_of_real_def q by auto
qed

lemma complex_of_real_of_rat[simp]: "complex_of_real (real_of_rat q) = of_rat q"
  unfolding complex_of_real_def of_rat_complex by simp

lemma is_rat_complex_iff: "x ∈ ℚ ⟷ Re x ∈ ℚ ∧ Im x = 0"
proof
  assume "x ∈ ℚ"
  then obtain q where x: "x = of_rat q" unfolding Rats_def by auto
  let ?y = "Complex (of_rat q) 0"
  have "x - ?y = 0" unfolding x by (simp add: Complex_eq)
  hence x: "x = ?y" by simp
  show "Re x ∈ ℚ ∧ Im x = 0" unfolding x complex.sel by auto
next
  assume "Re x ∈ ℚ ∧ Im x = 0"
  then obtain q where "Re x = of_rat q" "Im x = 0" unfolding Rats_def by auto
  hence "x = Complex (of_rat q) 0" by (metis complex_surj)
  thus "x ∈ ℚ" by (simp add: Complex_eq)
qed
  
instantiation complex :: is_rat
begin
definition "is_rat_complex (x :: complex) = (is_rat (Re x) ∧ Im x = 0)"
definition "to_rat_complex (x :: complex) = (if is_rat (Re x) ∧ Im x = 0 then to_rat (Re x) else 0)"


instance proof (intro_classes, auto simp: is_rat_complex_def to_rat_complex_def is_rat_complex_iff)
  fix x
  assume r: "Re x ∈ ℚ" and i: "Im x = 0"
  hence "x ∈ ℚ" unfolding is_rat_complex_iff by auto
  then obtain y where x: "x = of_rat y" unfolding Rats_def by blast
  from this[unfolded of_rat_complex] have x: "x = Complex (real_of_rat y) 0" by auto
  show "to_rat (Re x) = (THE y. x = of_rat y)" 
    by (subst of_rat_eq_iff[symmetric, where 'a = real], unfold of_rat_to_rat[OF r] of_rat_complex,
    unfold x complex.sel, auto)
qed
end

lemma in_rats_code_unfold[code_unfold]: "(x ∈ ℚ) = (is_rat x)" by simp

definition is_int_rat :: "rat ⇒ bool" where
  "is_int_rat x ≡ snd (quotient_of x) = 1"

definition int_of_rat :: "rat ⇒ int" where
  "int_of_rat x ≡ fst (quotient_of x)"

lemma is_int_rat[simp]: "is_int_rat x = (x ∈ ℤ)"
  unfolding is_int_rat_def Ints_def 
  by (metis Ints_def Ints_induct 
    quotient_of_int is_int_rat_def old.prod.exhaust quotient_of_inject rangeI snd_conv)

lemma in_ints_code_unfold[code_unfold]: "(x ∈ ℤ) = is_int_rat x"
  by simp

lemma int_of_rat[simp]: "int_of_rat (rat_of_int x) = x" "z ∈ ℤ ⟹ rat_of_int (int_of_rat z) = z"
proof (force simp: int_of_rat_def)
  assume "z ∈ ℤ"
  thus "rat_of_int (int_of_rat z) = z" unfolding int_of_rat_def
    by (metis Ints_cases Pair_inject quotient_of_int surjective_pairing)
qed

lemma int_of_rat_0[simp]: "(int_of_rat x = 0) = (x = 0)" unfolding int_of_rat_def
  using quotient_of_div[of x] by (cases "quotient_of x", auto)

end