# HG changeset patch # User haftmann # Date 1267178255 -3600 # Node ID d84eec57969577c2f3c1a9e0e836e44af70bcd39 # Parent 2fcd08c624958bb0546aba7f155477c76bf9fc2a# Parent 212b1dc5212dde8eb40d81703f66b10eac0fd759 merged diff -r 2fcd08c62495 -r d84eec579695 NEWS --- a/NEWS Thu Feb 25 22:46:52 2010 +0100 +++ b/NEWS Fri Feb 26 10:57:35 2010 +0100 @@ -54,6 +54,9 @@ *** HOL *** +* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. +INCOMPATIBILITY. + * New set of rules "ac_simps" provides combined assoc / commute rewrites for all interpretations of the appropriate generic locales. diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Code_Evaluation.thy Fri Feb 26 10:57:35 2010 +0100 @@ -119,6 +119,44 @@ end *} +setup {* +let + fun mk_term_of_eq thy ty vs tyco abs ty_rep proj = + let + val arg = Var (("x", 0), ty); + val rhs = Abs ("y", @{typ term}, HOLogic.reflect_term (Const (abs, ty_rep --> ty) $ Bound 0)) $ + (HOLogic.mk_term_of ty_rep (Const (proj, ty --> ty_rep) $ arg)) + |> Thm.cterm_of thy; + val cty = Thm.ctyp_of thy ty; + in + @{thm term_of_anything} + |> Drule.instantiate' [SOME cty] [SOME (Thm.cterm_of thy arg), SOME rhs] + |> Thm.varifyT + end; + fun add_term_of_code tyco raw_vs abs raw_ty_rep proj thy = + let + val algebra = Sign.classes_of thy; + val vs = map (fn (v, sort) => + (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; + val ty = Type (tyco, map TFree vs); + val ty_rep = map_atyps + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + val eq = mk_term_of_eq thy ty vs tyco abs ty_rep proj; + in + thy + |> Code.del_eqns const + |> Code.add_eqn eq + end; + fun ensure_term_of_code (tyco, (raw_vs, ((abs, ty), (proj, _)))) thy = + let + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort term_of}; + in if has_inst then add_term_of_code tyco raw_vs abs ty proj thy else thy end; +in + Code.abstype_interpretation ensure_term_of_code +end +*} + subsubsection {* Code generator setup *} diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Divides.thy Fri Feb 26 10:57:35 2010 +0100 @@ -309,6 +309,15 @@ apply (simp add: no_zero_divisors) done +lemma div_mult_swap: + assumes "c dvd b" + shows "a * (b div c) = (a * b) div c" +proof - + from assms have "b div c * (a div 1) = b * a div (c * 1)" + by (simp only: div_mult_div_if_dvd one_dvd) + then show ?thesis by (simp add: mult_commute) +qed + lemma div_mult_mult2 [simp]: "c \ 0 \ (a * c) div (b * c) = a div b" by (drule div_mult_mult1) (simp add: mult_commute) @@ -347,6 +356,24 @@ apply(simp add: div_mult_div_if_dvd dvd_power_same) done +lemma dvd_div_eq_mult: + assumes "a \ 0" and "a dvd b" + shows "b div a = c \ b = c * a" +proof + assume "b = c * a" + then show "b div a = c" by (simp add: assms) +next + assume "b div a = c" + then have "b div a * a = c * a" by simp + moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self) + ultimately show "b = c * a" by simp +qed + +lemma dvd_div_div_eq_mult: + assumes "a \ 0" "c \ 0" and "a dvd b" "c dvd d" + shows "b div a = d div c \ b * c = a * d" + using assms by (auto simp add: mult_commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym) + end class ring_div = semiring_div + idom diff -r 2fcd08c62495 -r d84eec579695 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/GCD.thy Fri Feb 26 10:57:35 2010 +0100 @@ -412,6 +412,33 @@ apply (rule gcd_mult_cancel_nat [transferred], auto) done +lemma coprime_crossproduct_nat: + fixes a b c d :: nat + assumes "coprime a d" and "coprime b c" + shows "a * c = b * d \ a = b \ c = d" (is "?lhs \ ?rhs") +proof + assume ?rhs then show ?lhs by simp +next + assume ?lhs + from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym) + with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat) + from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym) + with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat) + from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute) + with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) + from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute) + with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat) + from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym) + moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym) + ultimately show ?rhs .. +qed + +lemma coprime_crossproduct_int: + fixes a b c d :: int + assumes "coprime a d" and "coprime b c" + shows "\a\ * \c\ = \b\ * \d\ \ \a\ = \b\ \ \c\ = \d\" + using assms by (intro coprime_crossproduct_nat [transferred]) auto + text {* \medskip Addition laws *} lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n" diff -r 2fcd08c62495 -r d84eec579695 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/IsaMakefile Fri Feb 26 10:57:35 2010 +0100 @@ -352,7 +352,7 @@ PReal.thy \ Parity.thy \ RComplete.thy \ - Rational.thy \ + Rat.thy \ Real.thy \ RealDef.thy \ RealPow.thy \ diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Library/Binomial.thy Fri Feb 26 10:57:35 2010 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Binomial.thy +(* Title: HOL/Library/Binomial.thy Author: Lawrence C Paulson, Amine Chaieb Copyright 1997 University of Cambridge *) @@ -6,7 +6,7 @@ header {* Binomial Coefficients *} theory Binomial -imports Fact SetInterval Presburger Main Rational +imports Complex_Main begin text {* This development is based on the work of Andy Gordon and diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Library/Countable.thy Fri Feb 26 10:57:35 2010 +0100 @@ -5,12 +5,7 @@ header {* Encoding (almost) everything into natural numbers *} theory Countable -imports - "~~/src/HOL/List" - "~~/src/HOL/Hilbert_Choice" - "~~/src/HOL/Nat_Int_Bij" - "~~/src/HOL/Rational" - Main +imports Main Rat Nat_Int_Bij begin subsection {* The class of countable types *} @@ -213,8 +208,8 @@ proof fix r::rat show "\n. r = nat_to_rat_surj n" - proof(cases r) - fix i j assume [simp]: "r = Fract i j" and "j \ 0" + proof (cases r) + fix i j assume [simp]: "r = Fract i j" and "j > 0" have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j in nat_to_rat_surj(nat2_to_nat (m,n)))" using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij] diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Library/Fraction_Field.thy Fri Feb 26 10:57:35 2010 +0100 @@ -1,12 +1,12 @@ -(* Title: Fraction_Field.thy +(* Title: HOL/Library/Fraction_Field.thy Author: Amine Chaieb, University of Cambridge *) header{* A formalization of the fraction field of any integral domain - A generalization of Rational.thy from int to any integral domain *} + A generalization of Rat.thy from int to any integral domain *} theory Fraction_Field -imports Main (* Equiv_Relations Plain *) +imports Main begin subsection {* General fractions construction *} diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 10:57:35 2010 +0100 @@ -8,7 +8,7 @@ header {* Examples Featuring Nitpick Applied to Typedefs *} theory Typedef_Nits -imports Main Rational +imports Complex_Main begin nitpick_params [card = 1\4, sat_solver = MiniSat_JNI, max_threads = 1, diff -r 2fcd08c62495 -r d84eec579695 src/HOL/PReal.thy --- a/src/HOL/PReal.thy Thu Feb 25 22:46:52 2010 +0100 +++ b/src/HOL/PReal.thy Fri Feb 26 10:57:35 2010 +0100 @@ -9,7 +9,7 @@ header {* Positive real numbers *} theory PReal -imports Rational +imports Rat begin text{*Could be generalized and moved to @{text Groups}*} diff -r 2fcd08c62495 -r d84eec579695 src/HOL/Rat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Rat.thy Fri Feb 26 10:57:35 2010 +0100 @@ -0,0 +1,1210 @@ +(* Title: HOL/Rat.thy + Author: Markus Wenzel, TU Muenchen +*) + +header {* Rational numbers *} + +theory Rat +imports GCD Archimedean_Field +uses ("Tools/float_syntax.ML") +begin + +subsection {* Rational numbers as quotient *} + +subsubsection {* Construction of the type of rational numbers *} + +definition + ratrel :: "((int \ int) \ (int \ int)) set" where + "ratrel = {(x, y). snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x}" + +lemma ratrel_iff [simp]: + "(x, y) \ ratrel \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" + by (simp add: ratrel_def) + +lemma refl_on_ratrel: "refl_on {x. snd x \ 0} ratrel" + by (auto simp add: refl_on_def ratrel_def) + +lemma sym_ratrel: "sym ratrel" + by (simp add: ratrel_def sym_def) + +lemma trans_ratrel: "trans ratrel" +proof (rule transI, unfold split_paired_all) + fix a b a' b' a'' b'' :: int + assume A: "((a, b), (a', b')) \ ratrel" + assume B: "((a', b'), (a'', b'')) \ ratrel" + have "b' * (a * b'') = b'' * (a * b')" by simp + also from A have "a * b' = a' * b" by auto + also have "b'' * (a' * b) = b * (a' * b'')" by simp + also from B have "a' * b'' = a'' * b'" by auto + also have "b * (a'' * b') = b' * (a'' * b)" by simp + finally have "b' * (a * b'') = b' * (a'' * b)" . + moreover from B have "b' \ 0" by auto + ultimately have "a * b'' = a'' * b" by simp + with A B show "((a, b), (a'', b'')) \ ratrel" by auto +qed + +lemma equiv_ratrel: "equiv {x. snd x \ 0} ratrel" + by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel]) + +lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] +lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] + +lemma equiv_ratrel_iff [iff]: + assumes "snd x \ 0" and "snd y \ 0" + shows "ratrel `` {x} = ratrel `` {y} \ (x, y) \ ratrel" + by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms) + +typedef (Rat) rat = "{x. snd x \ 0} // ratrel" +proof + have "(0::int, 1::int) \ {x. snd x \ 0}" by simp + then show "ratrel `` {(0, 1)} \ {x. snd x \ 0} // ratrel" by (rule quotientI) +qed + +lemma ratrel_in_Rat [simp]: "snd x \ 0 \ ratrel `` {x} \ Rat" + by (simp add: Rat_def quotientI) + +declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] + + +subsubsection {* Representation and basic operations *} + +definition + Fract :: "int \ int \ rat" where + "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" + +lemma eq_rat: + shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" + and "\a. Fract a 0 = Fract 0 1" + and "\a c. Fract 0 a = Fract 0 c" + by (simp_all add: Fract_def) + +lemma Rat_cases [case_names Fract, cases type: rat]: + assumes "\a b. q = Fract a b \ b > 0 \ coprime a b \ C" + shows C +proof - + obtain a b :: int where "q = Fract a b" and "b \ 0" + by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) + let ?a = "a div gcd a b" + let ?b = "b div gcd a b" + from `b \ 0` have "?b * gcd a b = b" + by (simp add: dvd_div_mult_self) + with `b \ 0` have "?b \ 0" by auto + from `q = Fract a b` `b \ 0` `?b \ 0` have q: "q = Fract ?a ?b" + by (simp add: eq_rat dvd_div_mult mult_commute [of a]) + from `b \ 0` have coprime: "coprime ?a ?b" + by (auto intro: div_gcd_coprime_int) + show C proof (cases "b > 0") + case True + note assms + moreover note q + moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) + moreover note coprime + ultimately show C . + next + case False + note assms + moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def) + moreover from False `b \ 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) + moreover from coprime have "coprime (- ?a) (- ?b)" by simp + ultimately show C . + qed +qed + +lemma Rat_induct [case_names Fract, induct type: rat]: + assumes "\a b. b > 0 \ coprime a b \ P (Fract a b)" + shows "P q" + using assms by (cases q) simp + +instantiation rat :: comm_ring_1 +begin + +definition + Zero_rat_def: "0 = Fract 0 1" + +definition + One_rat_def: "1 = Fract 1 1" + +definition + add_rat_def: + "q + r = Abs_Rat (\x \ Rep_Rat q. \y \ Rep_Rat r. + ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" + +lemma add_rat [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" +proof - + have "(\x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)}) + respects2 ratrel" + by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib) + with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2) +qed + +definition + minus_rat_def: + "- q = Abs_Rat (\x \ Rep_Rat q. ratrel `` {(- fst x, snd x)})" + +lemma minus_rat [simp]: "- Fract a b = Fract (- a) b" +proof - + have "(\x. ratrel `` {(- fst x, snd x)}) respects ratrel" + by (simp add: congruent_def) + then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel) +qed + +lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b" + by (cases "b = 0") (simp_all add: eq_rat) + +definition + diff_rat_def: "q - r = q + - (r::rat)" + +lemma diff_rat [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" + using assms by (simp add: diff_rat_def) + +definition + mult_rat_def: + "q * r = Abs_Rat (\x \ Rep_Rat q. \y \ Rep_Rat r. + ratrel``{(fst x * fst y, snd x * snd y)})" + +lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" +proof - + have "(\x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel" + by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all + then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2) +qed + +lemma mult_rat_cancel: + assumes "c \ 0" + shows "Fract (c * a) (c * b) = Fract a b" +proof - + from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) + then show ?thesis by (simp add: mult_rat [symmetric]) +qed + +instance proof + fix q r s :: rat show "(q * r) * s = q * (r * s)" + by (cases q, cases r, cases s) (simp add: eq_rat) +next + fix q r :: rat show "q * r = r * q" + by (cases q, cases r) (simp add: eq_rat) +next + fix q :: rat show "1 * q = q" + by (cases q) (simp add: One_rat_def eq_rat) +next + fix q r s :: rat show "(q + r) + s = q + (r + s)" + by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) +next + fix q r :: rat show "q + r = r + q" + by (cases q, cases r) (simp add: eq_rat) +next + fix q :: rat show "0 + q = q" + by (cases q) (simp add: Zero_rat_def eq_rat) +next + fix q :: rat show "- q + q = 0" + by (cases q) (simp add: Zero_rat_def eq_rat) +next + fix q r :: rat show "q - r = q + - r" + by (cases q, cases r) (simp add: eq_rat) +next + fix q r s :: rat show "(q + r) * s = q * s + r * s" + by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) +next + show "(0::rat) \ 1" by (simp add: Zero_rat_def One_rat_def eq_rat) +qed + +end + +lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" + by (induct k) (simp_all add: Zero_rat_def One_rat_def) + +lemma of_int_rat: "of_int k = Fract k 1" + by (cases k rule: int_diff_cases) (simp add: of_nat_rat) + +lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" + by (rule of_nat_rat [symmetric]) + +lemma Fract_of_int_eq: "Fract k 1 = of_int k" + by (rule of_int_rat [symmetric]) + +instantiation rat :: number_ring +begin + +definition + rat_number_of_def: "number_of w = Fract w 1" + +instance proof +qed (simp add: rat_number_of_def of_int_rat) + +end + +lemma rat_number_collapse: + "Fract 0 k = 0" + "Fract 1 1 = 1" + "Fract (number_of k) 1 = number_of k" + "Fract k 0 = 0" + by (cases "k = 0") + (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def) + +lemma rat_number_expand [code_unfold]: + "0 = Fract 0 1" + "1 = Fract 1 1" + "number_of k = Fract (number_of k) 1" + by (simp_all add: rat_number_collapse) + +lemma iszero_rat [simp]: + "iszero (number_of k :: rat) \ iszero (number_of k :: int)" + by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) + +lemma Rat_cases_nonzero [case_names Fract 0]: + assumes Fract: "\a b. q = Fract a b \ b > 0 \ a \ 0 \ coprime a b \ C" + assumes 0: "q = 0 \ C" + shows C +proof (cases "q = 0") + case True then show C using 0 by auto +next + case False + then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto + moreover with False have "0 \ Fract a b" by simp + with `b > 0` have "a \ 0" by (simp add: Zero_rat_def eq_rat) + with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast +qed + +subsubsection {* Function @{text normalize} *} + +lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" +proof (cases "b = 0") + case True then show ?thesis by (simp add: eq_rat) +next + case False + moreover have "b div gcd a b * gcd a b = b" + by (rule dvd_div_mult_self) simp + ultimately have "b div gcd a b \ 0" by auto + with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a]) +qed + +definition normalize :: "int \ int \ int \ int" where + "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) + else if snd p = 0 then (0, 1) + else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))" + +lemma normalize_crossproduct: + assumes "q \ 0" "s \ 0" + assumes "normalize (p, q) = normalize (r, s)" + shows "p * s = r * q" +proof - + have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \ q * gcd r s = sgn (q * s) * s * gcd p q \ p * s = q * r" + proof - + assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" + then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp + with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0) + qed + from assms show ?thesis + by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) +qed + +lemma normalize_eq: "normalize (a, b) = (p, q) \ Fract p q = Fract a b" + by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse + split:split_if_asm) + +lemma normalize_denom_pos: "normalize r = (p, q) \ q > 0" + by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff + split:split_if_asm) + +lemma normalize_coprime: "normalize r = (p, q) \ coprime p q" + by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int + split:split_if_asm) + +lemma normalize_stable [simp]: + "q > 0 \ coprime p q \ normalize (p, q) = (p, q)" + by (simp add: normalize_def) + +lemma normalize_denom_zero [simp]: + "normalize (p, 0) = (0, 1)" + by (simp add: normalize_def) + +lemma normalize_negative [simp]: + "q < 0 \ normalize (p, q) = normalize (- p, - q)" + by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) + +text{* + Decompose a fraction into normalized, i.e. coprime numerator and denominator: +*} + +definition quotient_of :: "rat \ int \ int" where + "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & + snd pair > 0 & coprime (fst pair) (snd pair))" + +lemma quotient_of_unique: + "\!p. r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" +proof (cases r) + case (Fract a b) + then have "r = Fract (fst (a, b)) (snd (a, b)) \ snd (a, b) > 0 \ coprime (fst (a, b)) (snd (a, b))" by auto + then show ?thesis proof (rule ex1I) + fix p + obtain c d :: int where p: "p = (c, d)" by (cases p) + assume "r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" + with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all + have "c = a \ d = b" + proof (cases "a = 0") + case True with Fract Fract' show ?thesis by (simp add: eq_rat) + next + case False + with Fract Fract' have *: "c * b = a * d" and "c \ 0" by (auto simp add: eq_rat) + then have "c * b > 0 \ a * d > 0" by auto + with `b > 0` `d > 0` have "a > 0 \ c > 0" by (simp add: zero_less_mult_iff) + with `a \ 0` `c \ 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less) + from `coprime a b` `coprime c d` have "\a\ * \d\ = \c\ * \b\ \ \a\ = \c\ \ \d\ = \b\" + by (simp add: coprime_crossproduct_int) + with `b > 0` `d > 0` have "\a\ * d = \c\ * b \ \a\ = \c\ \ d = b" by simp + then have "a * sgn a * d = c * sgn c * b \ a * sgn a = c * sgn c \ d = b" by (simp add: abs_sgn) + with sgn * show ?thesis by (auto simp add: sgn_0_0) + qed + with p show "p = (a, b)" by simp + qed +qed + +lemma quotient_of_Fract [code]: + "quotient_of (Fract a b) = normalize (a, b)" +proof - + have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) + by (rule sym) (auto intro: normalize_eq) + moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) + by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) + moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) + by (rule normalize_coprime) simp + ultimately have "?Fract \ ?denom_pos \ ?coprime" by blast + with quotient_of_unique have + "(THE p. Fract a b = Fract (fst p) (snd p) \ 0 < snd p \ coprime (fst p) (snd p)) = normalize (a, b)" + by (rule the1_equality) + then show ?thesis by (simp add: quotient_of_def) +qed + +lemma quotient_of_number [simp]: + "quotient_of 0 = (0, 1)" + "quotient_of 1 = (1, 1)" + "quotient_of (number_of k) = (number_of k, 1)" + by (simp_all add: rat_number_expand quotient_of_Fract) + +lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \ Fract p q = Fract a b" + by (simp add: quotient_of_Fract normalize_eq) + +lemma quotient_of_denom_pos: "quotient_of r = (p, q) \ q > 0" + by (cases r) (simp add: quotient_of_Fract normalize_denom_pos) + +lemma quotient_of_coprime: "quotient_of r = (p, q) \ coprime p q" + by (cases r) (simp add: quotient_of_Fract normalize_coprime) + +lemma quotient_of_inject: + assumes "quotient_of a = quotient_of b" + shows "a = b" +proof - + obtain p q r s where a: "a = Fract p q" + and b: "b = Fract r s" + and "q > 0" and "s > 0" by (cases a, cases b) + with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) +qed + +lemma quotient_of_inject_eq: + "quotient_of a = quotient_of b \ a = b" + by (auto simp add: quotient_of_inject) + + +subsubsection {* The field of rational numbers *} + +instantiation rat :: "{field, division_by_zero}" +begin + +definition + inverse_rat_def: + "inverse q = Abs_Rat (\x \ Rep_Rat q. + ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" + +lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" +proof - + have "(\x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel" + by (auto simp add: congruent_def mult_commute) + then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel) +qed + +definition + divide_rat_def: "q / r = q * inverse (r::rat)" + +lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" + by (simp add: divide_rat_def) + +instance proof + show "inverse 0 = (0::rat)" by (simp add: rat_number_expand) + (simp add: rat_number_collapse) +next + fix q :: rat + assume "q \ 0" + then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero) + (simp_all add: rat_number_expand eq_rat) +next + fix q r :: rat + show "q / r = q * inverse r" by (simp add: divide_rat_def) +qed + +end + + +subsubsection {* Various *} + +lemma Fract_add_one: "n \ 0 ==> Fract (m + n) n = Fract m n + 1" + by (simp add: rat_number_expand) + +lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" + by (simp add: Fract_of_int_eq [symmetric]) + +lemma Fract_number_of_quotient: + "Fract (number_of k) (number_of l) = number_of k / number_of l" + unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. + +lemma Fract_1_number_of: + "Fract 1 (number_of k) = 1 / number_of k" + unfolding Fract_of_int_quotient number_of_eq by simp + +subsubsection {* The ordered field of rational numbers *} + +instantiation rat :: linorder +begin + +definition + le_rat_def: + "q \ r \ contents (\x \ Rep_Rat q. \y \ Rep_Rat r. + {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)})" + +lemma le_rat [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" +proof - + have "(\x y. {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)}) + respects2 ratrel" + proof (clarsimp simp add: congruent2_def) + fix a b a' b' c d c' d'::int + assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" + assume eq1: "a * b' = a' * b" + assume eq2: "c * d' = c' * d" + + let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" + { + fix a b c d x :: int assume x: "x \ 0" + have "?le a b c d = ?le (a * x) (b * x) c d" + proof - + from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) + hence "?le a b c d = + ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" + by (simp add: mult_le_cancel_right) + also have "... = ?le (a * x) (b * x) c d" + by (simp add: mult_ac) + finally show ?thesis . + qed + } note le_factor = this + + let ?D = "b * d" and ?D' = "b' * d'" + from neq have D: "?D \ 0" by simp + from neq have "?D' \ 0" by simp + hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" + by (rule le_factor) + also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" + by (simp add: mult_ac) + also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" + by (simp only: eq1 eq2) + also have "... = ?le (a' * ?D) (b' * ?D) c' d'" + by (simp add: mult_ac) + also from D have "... = ?le a' b' c' d'" + by (rule le_factor [symmetric]) + finally show "?le a b c d = ?le a' b' c' d'" . + qed + with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2) +qed + +definition + less_rat_def: "z < (w::rat) \ z \ w \ z \ w" + +lemma less_rat [simp]: + assumes "b \ 0" and "d \ 0" + shows "Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)" + using assms by (simp add: less_rat_def eq_rat order_less_le) + +instance proof + fix q r s :: rat + { + assume "q \ r" and "r \ s" + then show "q \ s" + proof (induct q, induct r, induct s) + fix a b c d e f :: int + assume neq: "b > 0" "d > 0" "f > 0" + assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f" + show "Fract a b \ Fract e f" + proof - + from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" + by (auto simp add: zero_less_mult_iff linorder_neq_iff) + have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" + proof - + from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + with ff show ?thesis by (simp add: mult_le_cancel_right) + qed + also have "... = (c * f) * (d * f) * (b * b)" by algebra + also have "... \ (e * d) * (d * f) * (b * b)" + proof - + from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" + by simp + with bb show ?thesis by (simp add: mult_le_cancel_right) + qed + finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" + by (simp only: mult_ac) + with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" + by (simp add: mult_le_cancel_right) + with neq show ?thesis by simp + qed + qed + next + assume "q \ r" and "r \ q" + then show "q = r" + proof (induct q, induct r) + fix a b c d :: int + assume neq: "b > 0" "d > 0" + assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b" + show "Fract a b = Fract c d" + proof - + from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + also have "... \ (a * d) * (b * d)" + proof - + from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" + by simp + thus ?thesis by (simp only: mult_ac) + qed + finally have "(a * d) * (b * d) = (c * b) * (b * d)" . + moreover from neq have "b * d \ 0" by simp + ultimately have "a * d = c * b" by simp + with neq show ?thesis by (simp add: eq_rat) + qed + qed + next + show "q \ q" + by (induct q) simp + show "(q < r) = (q \ r \ \ r \ q)" + by (induct q, induct r) (auto simp add: le_less mult_commute) + show "q \ r \ r \ q" + by (induct q, induct r) + (simp add: mult_commute, rule linorder_linear) + } +qed + +end + +instantiation rat :: "{distrib_lattice, abs_if, sgn_if}" +begin + +definition + abs_rat_def: "\q\ = (if q < 0 then -q else (q::rat))" + +lemma abs_rat [simp, code]: "\Fract a b\ = Fract \a\ \b\" + by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff) + +definition + sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" + +lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)" + unfolding Fract_of_int_eq + by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) + (auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) + +definition + "(inf \ rat \ rat \ rat) = min" + +definition + "(sup \ rat \ rat \ rat) = max" + +instance by intro_classes + (auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) + +end + +instance rat :: linordered_field +proof + fix q r s :: rat + show "q \ r ==> s + q \ s + r" + proof (induct q, induct r, induct s) + fix a b c d e f :: int + assume neq: "b > 0" "d > 0" "f > 0" + assume le: "Fract a b \ Fract c d" + show "Fract e f + Fract a b \ Fract e f + Fract c d" + proof - + let ?F = "f * f" from neq have F: "0 < ?F" + by (auto simp add: zero_less_mult_iff) + from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" + by simp + with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" + by (simp add: mult_le_cancel_right) + with neq show ?thesis by (simp add: mult_ac int_distrib) + qed + qed + show "q < r ==> 0 < s ==> s * q < s * r" + proof (induct q, induct r, induct s) + fix a b c d e f :: int + assume neq: "b > 0" "d > 0" "f > 0" + assume le: "Fract a b < Fract c d" + assume gt: "0 < Fract e f" + show "Fract e f * Fract a b < Fract e f * Fract c d" + proof - + let ?E = "e * f" and ?F = "f * f" + from neq gt have "0 < ?E" + by (auto simp add: Zero_rat_def order_less_le eq_rat) + moreover from neq have "0 < ?F" + by (auto simp add: zero_less_mult_iff) + moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" + by simp + ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" + by (simp add: mult_less_cancel_right) + with neq show ?thesis + by (simp add: mult_ac) + qed + qed +qed auto + +lemma Rat_induct_pos [case_names Fract, induct type: rat]: + assumes step: "\a b. 0 < b \ P (Fract a b)" + shows "P q" +proof (cases q) + have step': "\a b. b < 0 \ P (Fract a b)" + proof - + fix a::int and b::int + assume b: "b < 0" + hence "0 < -b" by simp + hence "P (Fract (-a) (-b))" by (rule step) + thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) + qed + case (Fract a b) + thus "P q" by (force simp add: linorder_neq_iff step step') +qed + +lemma zero_less_Fract_iff: + "0 < b \ 0 < Fract a b \ 0 < a" + by (simp add: Zero_rat_def zero_less_mult_iff) + +lemma Fract_less_zero_iff: + "0 < b \ Fract a b < 0 \ a < 0" + by (simp add: Zero_rat_def mult_less_0_iff) + +lemma zero_le_Fract_iff: + "0 < b \ 0 \ Fract a b \ 0 \ a" + by (simp add: Zero_rat_def zero_le_mult_iff) + +lemma Fract_le_zero_iff: + "0 < b \ Fract a b \ 0 \ a \ 0" + by (simp add: Zero_rat_def mult_le_0_iff) + +lemma one_less_Fract_iff: + "0 < b \ 1 < Fract a b \ b < a" + by (simp add: One_rat_def mult_less_cancel_right_disj) + +lemma Fract_less_one_iff: + "0 < b \ Fract a b < 1 \ a < b" + by (simp add: One_rat_def mult_less_cancel_right_disj) + +lemma one_le_Fract_iff: + "0 < b \ 1 \ Fract a b \ b \ a" + by (simp add: One_rat_def mult_le_cancel_right) + +lemma Fract_le_one_iff: + "0 < b \ Fract a b \ 1 \ a \ b" + by (simp add: One_rat_def mult_le_cancel_right) + + +subsubsection {* Rationals are an Archimedean field *} + +lemma rat_floor_lemma: + shows "of_int (a div b) \ Fract a b \ Fract a b < of_int (a div b + 1)" +proof - + have "Fract a b = of_int (a div b) + Fract (a mod b) b" + by (cases "b = 0", simp, simp add: of_int_rat) + moreover have "0 \ Fract (a mod b) b \ Fract (a mod b) b < 1" + unfolding Fract_of_int_quotient + by (rule linorder_cases [of b 0]) + (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos) + ultimately show ?thesis by simp +qed + +instance rat :: archimedean_field +proof + fix r :: rat + show "\z. r \ of_int z" + proof (induct r) + case (Fract a b) + have "Fract a b \ of_int (a div b + 1)" + using rat_floor_lemma [of a b] by simp + then show "\z. Fract a b \ of_int z" .. + qed +qed + +lemma floor_Fract: "floor (Fract a b) = a div b" + using rat_floor_lemma [of a b] + by (simp add: floor_unique) + + +subsection {* Linear arithmetic setup *} + +declaration {* + K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] + (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) + #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] + (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) + #> Lin_Arith.add_simps [@{thm neg_less_iff_less}, + @{thm True_implies_equals}, + read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, + @{thm divide_1}, @{thm divide_zero_left}, + @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, + @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, + @{thm of_int_minus}, @{thm of_int_diff}, + @{thm of_int_of_nat_eq}] + #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors + #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) + #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) +*} + + +subsection {* Embedding from Rationals to other Fields *} + +class field_char_0 = field + ring_char_0 + +subclass (in linordered_field) field_char_0 .. + +context field_char_0 +begin + +definition of_rat :: "rat \ 'a" where + "of_rat q = contents (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" + +end + +lemma of_rat_congruent: + "(\(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel" +apply (rule congruent.intro) +apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) +apply (simp only: of_int_mult [symmetric]) +done + +lemma of_rat_rat: "b \ 0 \ of_rat (Fract a b) = of_int a / of_int b" + unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent) + +lemma of_rat_0 [simp]: "of_rat 0 = 0" +by (simp add: Zero_rat_def of_rat_rat) + +lemma of_rat_1 [simp]: "of_rat 1 = 1" +by (simp add: One_rat_def of_rat_rat) + +lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" +by (induct a, induct b, simp add: of_rat_rat add_frac_eq) + +lemma of_rat_minus: "of_rat (- a) = - of_rat a" +by (induct a, simp add: of_rat_rat) + +lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" +by (simp only: diff_minus of_rat_add of_rat_minus) + +lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" +apply (induct a, induct b, simp add: of_rat_rat) +apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) +done + +lemma nonzero_of_rat_inverse: + "a \ 0 \ of_rat (inverse a) = inverse (of_rat a)" +apply (rule inverse_unique [symmetric]) +apply (simp add: of_rat_mult [symmetric]) +done + +lemma of_rat_inverse: + "(of_rat (inverse a)::'a::{field_char_0,division_by_zero}) = + inverse (of_rat a)" +by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) + +lemma nonzero_of_rat_divide: + "b \ 0 \ of_rat (a / b) = of_rat a / of_rat b" +by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) + +lemma of_rat_divide: + "(of_rat (a / b)::'a::{field_char_0,division_by_zero}) + = of_rat a / of_rat b" +by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) + +lemma of_rat_power: + "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" +by (induct n) (simp_all add: of_rat_mult) + +lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" +apply (induct a, induct b) +apply (simp add: of_rat_rat eq_rat) +apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) +apply (simp only: of_int_mult [symmetric] of_int_eq_iff) +done + +lemma of_rat_less: + "(of_rat r :: 'a::linordered_field) < of_rat s \ r < s" +proof (induct r, induct s) + fix a b c d :: int + assume not_zero: "b > 0" "d > 0" + then have "b * d > 0" by (rule mult_pos_pos) + have of_int_divide_less_eq: + "(of_int a :: 'a) / of_int b < of_int c / of_int d + \ (of_int a :: 'a) * of_int d < of_int c * of_int b" + using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) + show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) + \ Fract a b < Fract c d" + using not_zero `b * d > 0` + by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) +qed + +lemma of_rat_less_eq: + "(of_rat r :: 'a::linordered_field) \ of_rat s \ r \ s" + unfolding le_less by (auto simp add: of_rat_less) + +lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] + +lemma of_rat_eq_id [simp]: "of_rat = id" +proof + fix a + show "of_rat a = id a" + by (induct a) + (simp add: of_rat_rat Fract_of_int_eq [symmetric]) +qed + +text{*Collapse nested embeddings*} +lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" +by (induct n) (simp_all add: of_rat_add) + +lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" +by (cases z rule: int_diff_cases) (simp add: of_rat_diff) + +lemma of_rat_number_of_eq [simp]: + "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})" +by (simp add: number_of_eq) + +lemmas zero_rat = Zero_rat_def +lemmas one_rat = One_rat_def + +abbreviation + rat_of_nat :: "nat \ rat" +where + "rat_of_nat \ of_nat" + +abbreviation + rat_of_int :: "int \ rat" +where + "rat_of_int \ of_int" + +subsection {* The Set of Rational Numbers *} + +context field_char_0 +begin + +definition + Rats :: "'a set" where + "Rats = range of_rat" + +notation (xsymbols) + Rats ("\") + +end + +lemma Rats_of_rat [simp]: "of_rat r \ Rats" +by (simp add: Rats_def) + +lemma Rats_of_int [simp]: "of_int z \ Rats" +by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) + +lemma Rats_of_nat [simp]: "of_nat n \ Rats" +by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) + +lemma Rats_number_of [simp]: + "(number_of w::'a::{number_ring,field_char_0}) \ Rats" +by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat) + +lemma Rats_0 [simp]: "0 \ Rats" +apply (unfold Rats_def) +apply (rule range_eqI) +apply (rule of_rat_0 [symmetric]) +done + +lemma Rats_1 [simp]: "1 \ Rats" +apply (unfold Rats_def) +apply (rule range_eqI) +apply (rule of_rat_1 [symmetric]) +done + +lemma Rats_add [simp]: "\a \ Rats; b \ Rats\ \ a + b \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_add [symmetric]) +done + +lemma Rats_minus [simp]: "a \ Rats \ - a \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_minus [symmetric]) +done + +lemma Rats_diff [simp]: "\a \ Rats; b \ Rats\ \ a - b \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_diff [symmetric]) +done + +lemma Rats_mult [simp]: "\a \ Rats; b \ Rats\ \ a * b \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_mult [symmetric]) +done + +lemma nonzero_Rats_inverse: + fixes a :: "'a::field_char_0" + shows "\a \ Rats; a \ 0\ \ inverse a \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (erule nonzero_of_rat_inverse [symmetric]) +done + +lemma Rats_inverse [simp]: + fixes a :: "'a::{field_char_0,division_by_zero}" + shows "a \ Rats \ inverse a \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_inverse [symmetric]) +done + +lemma nonzero_Rats_divide: + fixes a b :: "'a::field_char_0" + shows "\a \ Rats; b \ Rats; b \ 0\ \ a / b \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (erule nonzero_of_rat_divide [symmetric]) +done + +lemma Rats_divide [simp]: + fixes a b :: "'a::{field_char_0,division_by_zero}" + shows "\a \ Rats; b \ Rats\ \ a / b \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_divide [symmetric]) +done + +lemma Rats_power [simp]: + fixes a :: "'a::field_char_0" + shows "a \ Rats \ a ^ n \ Rats" +apply (auto simp add: Rats_def) +apply (rule range_eqI) +apply (rule of_rat_power [symmetric]) +done + +lemma Rats_cases [cases set: Rats]: + assumes "q \ \" + obtains (of_rat) r where "q = of_rat r" + unfolding Rats_def +proof - + from `q \ \` have "q \ range of_rat" unfolding Rats_def . + then obtain r where "q = of_rat r" .. + then show thesis .. +qed + +lemma Rats_induct [case_names of_rat, induct set: Rats]: + "q \ \ \ (\r. P (of_rat r)) \ P q" + by (rule Rats_cases) auto + + +subsection {* Implementation of rational numbers as pairs of integers *} + +definition Frct :: "int \ int \ rat" where + [simp]: "Frct p = Fract (fst p) (snd p)" + +code_abstype Frct quotient_of +proof (rule eq_reflection) + fix r :: rat + show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq) +qed + +lemma Frct_code_post [code_post]: + "Frct (0, k) = 0" + "Frct (k, 0) = 0" + "Frct (1, 1) = 1" + "Frct (number_of k, 1) = number_of k" + "Frct (1, number_of k) = 1 / number_of k" + "Frct (number_of k, number_of l) = number_of k / number_of l" + by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of) + +declare quotient_of_Fract [code abstract] + +lemma rat_zero_code [code abstract]: + "quotient_of 0 = (0, 1)" + by (simp add: Zero_rat_def quotient_of_Fract normalize_def) + +lemma rat_one_code [code abstract]: + "quotient_of 1 = (1, 1)" + by (simp add: One_rat_def quotient_of_Fract normalize_def) + +lemma rat_plus_code [code abstract]: + "quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + in normalize (a * d + b * c, c * d))" + by (cases p, cases q) (simp add: quotient_of_Fract) + +lemma rat_uminus_code [code abstract]: + "quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))" + by (cases p) (simp add: quotient_of_Fract) + +lemma rat_minus_code [code abstract]: + "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + in normalize (a * d - b * c, c * d))" + by (cases p, cases q) (simp add: quotient_of_Fract) + +lemma rat_times_code [code abstract]: + "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + in normalize (a * b, c * d))" + by (cases p, cases q) (simp add: quotient_of_Fract) + +lemma rat_inverse_code [code abstract]: + "quotient_of (inverse p) = (let (a, b) = quotient_of p + in if a = 0 then (0, 1) else (sgn a * b, \a\))" +proof (cases p) + case (Fract a b) then show ?thesis + by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute) +qed + +lemma rat_divide_code [code abstract]: + "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + in normalize (a * d, c * b))" + by (cases p, cases q) (simp add: quotient_of_Fract) + +lemma rat_abs_code [code abstract]: + "quotient_of \p\ = (let (a, b) = quotient_of p in (\a\, b))" + by (cases p) (simp add: quotient_of_Fract) + +lemma rat_sgn_code [code abstract]: + "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" +proof (cases p) + case (Fract a b) then show ?thesis + by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) +qed + +instantiation rat :: eq +begin + +definition [code]: + "eq_class.eq a b \ quotient_of a = quotient_of b" + +instance proof +qed (simp add: eq_rat_def quotient_of_inject_eq) + +lemma rat_eq_refl [code nbe]: + "eq_class.eq (r::rat) r \ True" + by (rule HOL.eq_refl) + +end + +lemma rat_less_eq_code [code]: + "p \ q \