(* 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