src/HOL/Rat.thy
 author haftmann Mon Nov 29 13:44:54 2010 +0100 (2010-11-29) changeset 40815 6e2d17cc0d1d parent 39910 10097e0a9dbd child 40816 19c492929756 permissions -rw-r--r--
equivI has replaced equiv.intro
 haftmann@35372 ` 1` ```(* Title: HOL/Rat.thy ``` paulson@14365 ` 2` ``` Author: Markus Wenzel, TU Muenchen ``` paulson@14365 ` 3` ```*) ``` paulson@14365 ` 4` wenzelm@14691 ` 5` ```header {* Rational numbers *} ``` paulson@14365 ` 6` haftmann@35372 ` 7` ```theory Rat ``` huffman@30097 ` 8` ```imports GCD Archimedean_Field ``` huffman@35343 ` 9` ```uses ("Tools/float_syntax.ML") ``` nipkow@15131 ` 10` ```begin ``` paulson@14365 ` 11` haftmann@27551 ` 12` ```subsection {* Rational numbers as quotient *} ``` paulson@14365 ` 13` haftmann@27551 ` 14` ```subsubsection {* Construction of the type of rational numbers *} ``` huffman@18913 ` 15` wenzelm@21404 ` 16` ```definition ``` wenzelm@21404 ` 17` ``` ratrel :: "((int \ int) \ (int \ int)) set" where ``` haftmann@27551 ` 18` ``` "ratrel = {(x, y). snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x}" ``` paulson@14365 ` 19` huffman@18913 ` 20` ```lemma ratrel_iff [simp]: ``` haftmann@27551 ` 21` ``` "(x, y) \ ratrel \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" ``` haftmann@27551 ` 22` ``` by (simp add: ratrel_def) ``` paulson@14365 ` 23` nipkow@30198 ` 24` ```lemma refl_on_ratrel: "refl_on {x. snd x \ 0} ratrel" ``` nipkow@30198 ` 25` ``` by (auto simp add: refl_on_def ratrel_def) ``` huffman@18913 ` 26` huffman@18913 ` 27` ```lemma sym_ratrel: "sym ratrel" ``` haftmann@27551 ` 28` ``` by (simp add: ratrel_def sym_def) ``` paulson@14365 ` 29` huffman@18913 ` 30` ```lemma trans_ratrel: "trans ratrel" ``` haftmann@27551 ` 31` ```proof (rule transI, unfold split_paired_all) ``` haftmann@27551 ` 32` ``` fix a b a' b' a'' b'' :: int ``` haftmann@27551 ` 33` ``` assume A: "((a, b), (a', b')) \ ratrel" ``` haftmann@27551 ` 34` ``` assume B: "((a', b'), (a'', b'')) \ ratrel" ``` haftmann@27551 ` 35` ``` have "b' * (a * b'') = b'' * (a * b')" by simp ``` haftmann@27551 ` 36` ``` also from A have "a * b' = a' * b" by auto ``` haftmann@27551 ` 37` ``` also have "b'' * (a' * b) = b * (a' * b'')" by simp ``` haftmann@27551 ` 38` ``` also from B have "a' * b'' = a'' * b'" by auto ``` haftmann@27551 ` 39` ``` also have "b * (a'' * b') = b' * (a'' * b)" by simp ``` haftmann@27551 ` 40` ``` finally have "b' * (a * b'') = b' * (a'' * b)" . ``` haftmann@27551 ` 41` ``` moreover from B have "b' \ 0" by auto ``` haftmann@27551 ` 42` ``` ultimately have "a * b'' = a'' * b" by simp ``` haftmann@27551 ` 43` ``` with A B show "((a, b), (a'', b'')) \ ratrel" by auto ``` paulson@14365 ` 44` ```qed ``` haftmann@27551 ` 45` ``` ``` haftmann@27551 ` 46` ```lemma equiv_ratrel: "equiv {x. snd x \ 0} ratrel" ``` haftmann@40815 ` 47` ``` by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel]) ``` paulson@14365 ` 48` huffman@18913 ` 49` ```lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] ``` huffman@18913 ` 50` ```lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] ``` paulson@14365 ` 51` haftmann@27551 ` 52` ```lemma equiv_ratrel_iff [iff]: ``` haftmann@27551 ` 53` ``` assumes "snd x \ 0" and "snd y \ 0" ``` haftmann@27551 ` 54` ``` shows "ratrel `` {x} = ratrel `` {y} \ (x, y) \ ratrel" ``` haftmann@27551 ` 55` ``` by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms) ``` paulson@14365 ` 56` haftmann@27551 ` 57` ```typedef (Rat) rat = "{x. snd x \ 0} // ratrel" ``` haftmann@27551 ` 58` ```proof ``` haftmann@27551 ` 59` ``` have "(0::int, 1::int) \ {x. snd x \ 0}" by simp ``` haftmann@27551 ` 60` ``` then show "ratrel `` {(0, 1)} \ {x. snd x \ 0} // ratrel" by (rule quotientI) ``` haftmann@27551 ` 61` ```qed ``` haftmann@27551 ` 62` haftmann@27551 ` 63` ```lemma ratrel_in_Rat [simp]: "snd x \ 0 \ ratrel `` {x} \ Rat" ``` haftmann@27551 ` 64` ``` by (simp add: Rat_def quotientI) ``` haftmann@27551 ` 65` haftmann@27551 ` 66` ```declare Abs_Rat_inject [simp] Abs_Rat_inverse [simp] ``` haftmann@27551 ` 67` haftmann@27551 ` 68` haftmann@27551 ` 69` ```subsubsection {* Representation and basic operations *} ``` haftmann@27551 ` 70` haftmann@27551 ` 71` ```definition ``` haftmann@27551 ` 72` ``` Fract :: "int \ int \ rat" where ``` haftmann@35369 ` 73` ``` "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})" ``` haftmann@27551 ` 74` haftmann@27551 ` 75` ```lemma eq_rat: ``` haftmann@27551 ` 76` ``` shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" ``` haftmann@27652 ` 77` ``` and "\a. Fract a 0 = Fract 0 1" ``` haftmann@27652 ` 78` ``` and "\a c. Fract 0 a = Fract 0 c" ``` haftmann@27551 ` 79` ``` by (simp_all add: Fract_def) ``` haftmann@27551 ` 80` haftmann@35369 ` 81` ```lemma Rat_cases [case_names Fract, cases type: rat]: ``` haftmann@35369 ` 82` ``` assumes "\a b. q = Fract a b \ b > 0 \ coprime a b \ C" ``` haftmann@35369 ` 83` ``` shows C ``` haftmann@35369 ` 84` ```proof - ``` haftmann@35369 ` 85` ``` obtain a b :: int where "q = Fract a b" and "b \ 0" ``` haftmann@35369 ` 86` ``` by (cases q) (clarsimp simp add: Fract_def Rat_def quotient_def) ``` haftmann@35369 ` 87` ``` let ?a = "a div gcd a b" ``` haftmann@35369 ` 88` ``` let ?b = "b div gcd a b" ``` haftmann@35369 ` 89` ``` from `b \ 0` have "?b * gcd a b = b" ``` haftmann@35369 ` 90` ``` by (simp add: dvd_div_mult_self) ``` haftmann@35369 ` 91` ``` with `b \ 0` have "?b \ 0" by auto ``` haftmann@35369 ` 92` ``` from `q = Fract a b` `b \ 0` `?b \ 0` have q: "q = Fract ?a ?b" ``` haftmann@35369 ` 93` ``` by (simp add: eq_rat dvd_div_mult mult_commute [of a]) ``` haftmann@35369 ` 94` ``` from `b \ 0` have coprime: "coprime ?a ?b" ``` haftmann@35369 ` 95` ``` by (auto intro: div_gcd_coprime_int) ``` haftmann@35369 ` 96` ``` show C proof (cases "b > 0") ``` haftmann@35369 ` 97` ``` case True ``` haftmann@35369 ` 98` ``` note assms ``` haftmann@35369 ` 99` ``` moreover note q ``` haftmann@35369 ` 100` ``` moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) ``` haftmann@35369 ` 101` ``` moreover note coprime ``` haftmann@35369 ` 102` ``` ultimately show C . ``` haftmann@35369 ` 103` ``` next ``` haftmann@35369 ` 104` ``` case False ``` haftmann@35369 ` 105` ``` note assms ``` haftmann@35369 ` 106` ``` moreover from q have "q = Fract (- ?a) (- ?b)" by (simp add: Fract_def) ``` haftmann@35369 ` 107` ``` moreover from False `b \ 0` have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) ``` haftmann@35369 ` 108` ``` moreover from coprime have "coprime (- ?a) (- ?b)" by simp ``` haftmann@35369 ` 109` ``` ultimately show C . ``` haftmann@35369 ` 110` ``` qed ``` haftmann@35369 ` 111` ```qed ``` haftmann@35369 ` 112` haftmann@35369 ` 113` ```lemma Rat_induct [case_names Fract, induct type: rat]: ``` haftmann@35369 ` 114` ``` assumes "\a b. b > 0 \ coprime a b \ P (Fract a b)" ``` haftmann@35369 ` 115` ``` shows "P q" ``` haftmann@35369 ` 116` ``` using assms by (cases q) simp ``` haftmann@35369 ` 117` haftmann@31017 ` 118` ```instantiation rat :: comm_ring_1 ``` haftmann@25571 ` 119` ```begin ``` haftmann@25571 ` 120` haftmann@25571 ` 121` ```definition ``` haftmann@35369 ` 122` ``` Zero_rat_def: "0 = Fract 0 1" ``` paulson@14365 ` 123` haftmann@25571 ` 124` ```definition ``` haftmann@35369 ` 125` ``` One_rat_def: "1 = Fract 1 1" ``` huffman@18913 ` 126` haftmann@25571 ` 127` ```definition ``` haftmann@35369 ` 128` ``` add_rat_def: ``` haftmann@27551 ` 129` ``` "q + r = Abs_Rat (\x \ Rep_Rat q. \y \ Rep_Rat r. ``` haftmann@27551 ` 130` ``` ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})" ``` haftmann@27551 ` 131` haftmann@27652 ` 132` ```lemma add_rat [simp]: ``` haftmann@27551 ` 133` ``` assumes "b \ 0" and "d \ 0" ``` haftmann@27551 ` 134` ``` shows "Fract a b + Fract c d = Fract (a * d + c * b) (b * d)" ``` haftmann@27551 ` 135` ```proof - ``` haftmann@27551 ` 136` ``` have "(\x y. ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)}) ``` haftmann@27551 ` 137` ``` respects2 ratrel" ``` haftmann@27551 ` 138` ``` by (rule equiv_ratrel [THEN congruent2_commuteI]) (simp_all add: left_distrib) ``` haftmann@27551 ` 139` ``` with assms show ?thesis by (simp add: Fract_def add_rat_def UN_ratrel2) ``` haftmann@27551 ` 140` ```qed ``` huffman@18913 ` 141` haftmann@25571 ` 142` ```definition ``` haftmann@35369 ` 143` ``` minus_rat_def: ``` haftmann@27551 ` 144` ``` "- q = Abs_Rat (\x \ Rep_Rat q. ratrel `` {(- fst x, snd x)})" ``` haftmann@27551 ` 145` haftmann@35369 ` 146` ```lemma minus_rat [simp]: "- Fract a b = Fract (- a) b" ``` haftmann@27551 ` 147` ```proof - ``` haftmann@27551 ` 148` ``` have "(\x. ratrel `` {(- fst x, snd x)}) respects ratrel" ``` haftmann@27551 ` 149` ``` by (simp add: congruent_def) ``` haftmann@27551 ` 150` ``` then show ?thesis by (simp add: Fract_def minus_rat_def UN_ratrel) ``` haftmann@27551 ` 151` ```qed ``` haftmann@27551 ` 152` haftmann@27652 ` 153` ```lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b" ``` haftmann@27551 ` 154` ``` by (cases "b = 0") (simp_all add: eq_rat) ``` haftmann@25571 ` 155` haftmann@25571 ` 156` ```definition ``` haftmann@35369 ` 157` ``` diff_rat_def: "q - r = q + - (r::rat)" ``` huffman@18913 ` 158` haftmann@27652 ` 159` ```lemma diff_rat [simp]: ``` haftmann@27551 ` 160` ``` assumes "b \ 0" and "d \ 0" ``` haftmann@27551 ` 161` ``` shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)" ``` haftmann@27652 ` 162` ``` using assms by (simp add: diff_rat_def) ``` haftmann@25571 ` 163` haftmann@25571 ` 164` ```definition ``` haftmann@35369 ` 165` ``` mult_rat_def: ``` haftmann@27551 ` 166` ``` "q * r = Abs_Rat (\x \ Rep_Rat q. \y \ Rep_Rat r. ``` haftmann@27551 ` 167` ``` ratrel``{(fst x * fst y, snd x * snd y)})" ``` paulson@14365 ` 168` haftmann@27652 ` 169` ```lemma mult_rat [simp]: "Fract a b * Fract c d = Fract (a * c) (b * d)" ``` haftmann@27551 ` 170` ```proof - ``` haftmann@27551 ` 171` ``` have "(\x y. ratrel `` {(fst x * fst y, snd x * snd y)}) respects2 ratrel" ``` haftmann@27551 ` 172` ``` by (rule equiv_ratrel [THEN congruent2_commuteI]) simp_all ``` haftmann@27551 ` 173` ``` then show ?thesis by (simp add: Fract_def mult_rat_def UN_ratrel2) ``` paulson@14365 ` 174` ```qed ``` paulson@14365 ` 175` haftmann@27652 ` 176` ```lemma mult_rat_cancel: ``` haftmann@27551 ` 177` ``` assumes "c \ 0" ``` haftmann@27551 ` 178` ``` shows "Fract (c * a) (c * b) = Fract a b" ``` haftmann@27551 ` 179` ```proof - ``` haftmann@27551 ` 180` ``` from assms have "Fract c c = Fract 1 1" by (simp add: Fract_def) ``` haftmann@27652 ` 181` ``` then show ?thesis by (simp add: mult_rat [symmetric]) ``` haftmann@27551 ` 182` ```qed ``` huffman@27509 ` 183` huffman@27509 ` 184` ```instance proof ``` chaieb@27668 ` 185` ``` fix q r s :: rat show "(q * r) * s = q * (r * s)" ``` haftmann@27652 ` 186` ``` by (cases q, cases r, cases s) (simp add: eq_rat) ``` haftmann@27551 ` 187` ```next ``` haftmann@27551 ` 188` ``` fix q r :: rat show "q * r = r * q" ``` haftmann@27652 ` 189` ``` by (cases q, cases r) (simp add: eq_rat) ``` haftmann@27551 ` 190` ```next ``` haftmann@27551 ` 191` ``` fix q :: rat show "1 * q = q" ``` haftmann@27652 ` 192` ``` by (cases q) (simp add: One_rat_def eq_rat) ``` haftmann@27551 ` 193` ```next ``` haftmann@27551 ` 194` ``` fix q r s :: rat show "(q + r) + s = q + (r + s)" ``` nipkow@29667 ` 195` ``` by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) ``` haftmann@27551 ` 196` ```next ``` haftmann@27551 ` 197` ``` fix q r :: rat show "q + r = r + q" ``` haftmann@27652 ` 198` ``` by (cases q, cases r) (simp add: eq_rat) ``` haftmann@27551 ` 199` ```next ``` haftmann@27551 ` 200` ``` fix q :: rat show "0 + q = q" ``` haftmann@27652 ` 201` ``` by (cases q) (simp add: Zero_rat_def eq_rat) ``` haftmann@27551 ` 202` ```next ``` haftmann@27551 ` 203` ``` fix q :: rat show "- q + q = 0" ``` haftmann@27652 ` 204` ``` by (cases q) (simp add: Zero_rat_def eq_rat) ``` haftmann@27551 ` 205` ```next ``` haftmann@27551 ` 206` ``` fix q r :: rat show "q - r = q + - r" ``` haftmann@27652 ` 207` ``` by (cases q, cases r) (simp add: eq_rat) ``` haftmann@27551 ` 208` ```next ``` haftmann@27551 ` 209` ``` fix q r s :: rat show "(q + r) * s = q * s + r * s" ``` nipkow@29667 ` 210` ``` by (cases q, cases r, cases s) (simp add: eq_rat algebra_simps) ``` haftmann@27551 ` 211` ```next ``` haftmann@27551 ` 212` ``` show "(0::rat) \ 1" by (simp add: Zero_rat_def One_rat_def eq_rat) ``` huffman@27509 ` 213` ```qed ``` huffman@27509 ` 214` huffman@27509 ` 215` ```end ``` huffman@27509 ` 216` haftmann@27551 ` 217` ```lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1" ``` haftmann@27652 ` 218` ``` by (induct k) (simp_all add: Zero_rat_def One_rat_def) ``` haftmann@27551 ` 219` haftmann@27551 ` 220` ```lemma of_int_rat: "of_int k = Fract k 1" ``` haftmann@27652 ` 221` ``` by (cases k rule: int_diff_cases) (simp add: of_nat_rat) ``` haftmann@27551 ` 222` haftmann@27551 ` 223` ```lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k" ``` haftmann@27551 ` 224` ``` by (rule of_nat_rat [symmetric]) ``` haftmann@27551 ` 225` haftmann@27551 ` 226` ```lemma Fract_of_int_eq: "Fract k 1 = of_int k" ``` haftmann@27551 ` 227` ``` by (rule of_int_rat [symmetric]) ``` haftmann@27551 ` 228` haftmann@27551 ` 229` ```instantiation rat :: number_ring ``` haftmann@27551 ` 230` ```begin ``` haftmann@27551 ` 231` haftmann@27551 ` 232` ```definition ``` haftmann@35369 ` 233` ``` rat_number_of_def: "number_of w = Fract w 1" ``` haftmann@27551 ` 234` haftmann@30960 ` 235` ```instance proof ``` haftmann@30960 ` 236` ```qed (simp add: rat_number_of_def of_int_rat) ``` haftmann@27551 ` 237` haftmann@27551 ` 238` ```end ``` haftmann@27551 ` 239` haftmann@35369 ` 240` ```lemma rat_number_collapse: ``` haftmann@27551 ` 241` ``` "Fract 0 k = 0" ``` haftmann@27551 ` 242` ``` "Fract 1 1 = 1" ``` haftmann@27551 ` 243` ``` "Fract (number_of k) 1 = number_of k" ``` haftmann@27551 ` 244` ``` "Fract k 0 = 0" ``` haftmann@27551 ` 245` ``` by (cases "k = 0") ``` haftmann@27551 ` 246` ``` (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def) ``` haftmann@27551 ` 247` haftmann@31998 ` 248` ```lemma rat_number_expand [code_unfold]: ``` haftmann@27551 ` 249` ``` "0 = Fract 0 1" ``` haftmann@27551 ` 250` ``` "1 = Fract 1 1" ``` haftmann@27551 ` 251` ``` "number_of k = Fract (number_of k) 1" ``` haftmann@27551 ` 252` ``` by (simp_all add: rat_number_collapse) ``` haftmann@27551 ` 253` haftmann@27551 ` 254` ```lemma iszero_rat [simp]: ``` haftmann@27551 ` 255` ``` "iszero (number_of k :: rat) \ iszero (number_of k :: int)" ``` haftmann@27551 ` 256` ``` by (simp add: iszero_def rat_number_expand number_of_is_id eq_rat) ``` haftmann@27551 ` 257` haftmann@27551 ` 258` ```lemma Rat_cases_nonzero [case_names Fract 0]: ``` haftmann@35369 ` 259` ``` assumes Fract: "\a b. q = Fract a b \ b > 0 \ a \ 0 \ coprime a b \ C" ``` haftmann@27551 ` 260` ``` assumes 0: "q = 0 \ C" ``` haftmann@27551 ` 261` ``` shows C ``` haftmann@27551 ` 262` ```proof (cases "q = 0") ``` haftmann@27551 ` 263` ``` case True then show C using 0 by auto ``` haftmann@27551 ` 264` ```next ``` haftmann@27551 ` 265` ``` case False ``` haftmann@35369 ` 266` ``` then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto ``` haftmann@27551 ` 267` ``` moreover with False have "0 \ Fract a b" by simp ``` haftmann@35369 ` 268` ``` with `b > 0` have "a \ 0" by (simp add: Zero_rat_def eq_rat) ``` haftmann@35369 ` 269` ``` with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast ``` haftmann@27551 ` 270` ```qed ``` haftmann@27551 ` 271` nipkow@33805 ` 272` ```subsubsection {* Function @{text normalize} *} ``` nipkow@33805 ` 273` haftmann@35369 ` 274` ```lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" ``` haftmann@35369 ` 275` ```proof (cases "b = 0") ``` haftmann@35369 ` 276` ``` case True then show ?thesis by (simp add: eq_rat) ``` haftmann@35369 ` 277` ```next ``` haftmann@35369 ` 278` ``` case False ``` haftmann@35369 ` 279` ``` moreover have "b div gcd a b * gcd a b = b" ``` haftmann@35369 ` 280` ``` by (rule dvd_div_mult_self) simp ``` haftmann@35369 ` 281` ``` ultimately have "b div gcd a b \ 0" by auto ``` haftmann@35369 ` 282` ``` with False show ?thesis by (simp add: eq_rat dvd_div_mult mult_commute [of a]) ``` haftmann@35369 ` 283` ```qed ``` nipkow@33805 ` 284` haftmann@35369 ` 285` ```definition normalize :: "int \ int \ int \ int" where ``` haftmann@35369 ` 286` ``` "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) ``` haftmann@35369 ` 287` ``` else if snd p = 0 then (0, 1) ``` haftmann@35369 ` 288` ``` else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))" ``` haftmann@35369 ` 289` haftmann@35369 ` 290` ```lemma normalize_crossproduct: ``` haftmann@35369 ` 291` ``` assumes "q \ 0" "s \ 0" ``` haftmann@35369 ` 292` ``` assumes "normalize (p, q) = normalize (r, s)" ``` haftmann@35369 ` 293` ``` shows "p * s = r * q" ``` haftmann@35369 ` 294` ```proof - ``` haftmann@35369 ` 295` ``` 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" ``` haftmann@35369 ` 296` ``` proof - ``` haftmann@35369 ` 297` ``` assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" ``` haftmann@35369 ` 298` ``` 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 ``` haftmann@35369 ` 299` ``` with assms show "p * s = q * r" by (auto simp add: mult_ac sgn_times sgn_0_0) ``` haftmann@35369 ` 300` ``` qed ``` haftmann@35369 ` 301` ``` from assms show ?thesis ``` haftmann@35369 ` 302` ``` by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult_commute sgn_times split: if_splits intro: aux) ``` nipkow@33805 ` 303` ```qed ``` nipkow@33805 ` 304` haftmann@35369 ` 305` ```lemma normalize_eq: "normalize (a, b) = (p, q) \ Fract p q = Fract a b" ``` haftmann@35369 ` 306` ``` by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse ``` haftmann@35369 ` 307` ``` split:split_if_asm) ``` haftmann@35369 ` 308` haftmann@35369 ` 309` ```lemma normalize_denom_pos: "normalize r = (p, q) \ q > 0" ``` haftmann@35369 ` 310` ``` by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff ``` haftmann@35369 ` 311` ``` split:split_if_asm) ``` haftmann@35369 ` 312` haftmann@35369 ` 313` ```lemma normalize_coprime: "normalize r = (p, q) \ coprime p q" ``` haftmann@35369 ` 314` ``` by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime_int ``` haftmann@35369 ` 315` ``` split:split_if_asm) ``` haftmann@35369 ` 316` haftmann@35369 ` 317` ```lemma normalize_stable [simp]: ``` haftmann@35369 ` 318` ``` "q > 0 \ coprime p q \ normalize (p, q) = (p, q)" ``` haftmann@35369 ` 319` ``` by (simp add: normalize_def) ``` haftmann@35369 ` 320` haftmann@35369 ` 321` ```lemma normalize_denom_zero [simp]: ``` haftmann@35369 ` 322` ``` "normalize (p, 0) = (0, 1)" ``` haftmann@35369 ` 323` ``` by (simp add: normalize_def) ``` haftmann@35369 ` 324` haftmann@35369 ` 325` ```lemma normalize_negative [simp]: ``` haftmann@35369 ` 326` ``` "q < 0 \ normalize (p, q) = normalize (- p, - q)" ``` haftmann@35369 ` 327` ``` by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) ``` haftmann@35369 ` 328` haftmann@35369 ` 329` ```text{* ``` haftmann@35369 ` 330` ``` Decompose a fraction into normalized, i.e. coprime numerator and denominator: ``` haftmann@35369 ` 331` ```*} ``` haftmann@35369 ` 332` haftmann@35369 ` 333` ```definition quotient_of :: "rat \ int \ int" where ``` haftmann@35369 ` 334` ``` "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & ``` haftmann@35369 ` 335` ``` snd pair > 0 & coprime (fst pair) (snd pair))" ``` haftmann@35369 ` 336` haftmann@35369 ` 337` ```lemma quotient_of_unique: ``` haftmann@35369 ` 338` ``` "\!p. r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" ``` haftmann@35369 ` 339` ```proof (cases r) ``` haftmann@35369 ` 340` ``` case (Fract a b) ``` haftmann@35369 ` 341` ``` then have "r = Fract (fst (a, b)) (snd (a, b)) \ snd (a, b) > 0 \ coprime (fst (a, b)) (snd (a, b))" by auto ``` haftmann@35369 ` 342` ``` then show ?thesis proof (rule ex1I) ``` haftmann@35369 ` 343` ``` fix p ``` haftmann@35369 ` 344` ``` obtain c d :: int where p: "p = (c, d)" by (cases p) ``` haftmann@35369 ` 345` ``` assume "r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" ``` haftmann@35369 ` 346` ``` with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all ``` haftmann@35369 ` 347` ``` have "c = a \ d = b" ``` haftmann@35369 ` 348` ``` proof (cases "a = 0") ``` haftmann@35369 ` 349` ``` case True with Fract Fract' show ?thesis by (simp add: eq_rat) ``` haftmann@35369 ` 350` ``` next ``` haftmann@35369 ` 351` ``` case False ``` haftmann@35369 ` 352` ``` with Fract Fract' have *: "c * b = a * d" and "c \ 0" by (auto simp add: eq_rat) ``` haftmann@35369 ` 353` ``` then have "c * b > 0 \ a * d > 0" by auto ``` haftmann@35369 ` 354` ``` with `b > 0` `d > 0` have "a > 0 \ c > 0" by (simp add: zero_less_mult_iff) ``` haftmann@35369 ` 355` ``` with `a \ 0` `c \ 0` have sgn: "sgn a = sgn c" by (auto simp add: not_less) ``` haftmann@35369 ` 356` ``` from `coprime a b` `coprime c d` have "\a\ * \d\ = \c\ * \b\ \ \a\ = \c\ \ \d\ = \b\" ``` haftmann@35369 ` 357` ``` by (simp add: coprime_crossproduct_int) ``` haftmann@35369 ` 358` ``` with `b > 0` `d > 0` have "\a\ * d = \c\ * b \ \a\ = \c\ \ d = b" by simp ``` haftmann@35369 ` 359` ``` then have "a * sgn a * d = c * sgn c * b \ a * sgn a = c * sgn c \ d = b" by (simp add: abs_sgn) ``` haftmann@35369 ` 360` ``` with sgn * show ?thesis by (auto simp add: sgn_0_0) ``` nipkow@33805 ` 361` ``` qed ``` haftmann@35369 ` 362` ``` with p show "p = (a, b)" by simp ``` nipkow@33805 ` 363` ``` qed ``` nipkow@33805 ` 364` ```qed ``` nipkow@33805 ` 365` haftmann@35369 ` 366` ```lemma quotient_of_Fract [code]: ``` haftmann@35369 ` 367` ``` "quotient_of (Fract a b) = normalize (a, b)" ``` haftmann@35369 ` 368` ```proof - ``` haftmann@35369 ` 369` ``` have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) ``` haftmann@35369 ` 370` ``` by (rule sym) (auto intro: normalize_eq) ``` haftmann@35369 ` 371` ``` moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) ``` haftmann@35369 ` 372` ``` by (cases "normalize (a, b)") (rule normalize_denom_pos, simp) ``` haftmann@35369 ` 373` ``` moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) ``` haftmann@35369 ` 374` ``` by (rule normalize_coprime) simp ``` haftmann@35369 ` 375` ``` ultimately have "?Fract \ ?denom_pos \ ?coprime" by blast ``` haftmann@35369 ` 376` ``` with quotient_of_unique have ``` haftmann@35369 ` 377` ``` "(THE p. Fract a b = Fract (fst p) (snd p) \ 0 < snd p \ coprime (fst p) (snd p)) = normalize (a, b)" ``` haftmann@35369 ` 378` ``` by (rule the1_equality) ``` haftmann@35369 ` 379` ``` then show ?thesis by (simp add: quotient_of_def) ``` haftmann@35369 ` 380` ```qed ``` haftmann@35369 ` 381` haftmann@35369 ` 382` ```lemma quotient_of_number [simp]: ``` haftmann@35369 ` 383` ``` "quotient_of 0 = (0, 1)" ``` haftmann@35369 ` 384` ``` "quotient_of 1 = (1, 1)" ``` haftmann@35369 ` 385` ``` "quotient_of (number_of k) = (number_of k, 1)" ``` haftmann@35369 ` 386` ``` by (simp_all add: rat_number_expand quotient_of_Fract) ``` nipkow@33805 ` 387` haftmann@35369 ` 388` ```lemma quotient_of_eq: "quotient_of (Fract a b) = (p, q) \ Fract p q = Fract a b" ``` haftmann@35369 ` 389` ``` by (simp add: quotient_of_Fract normalize_eq) ``` haftmann@35369 ` 390` haftmann@35369 ` 391` ```lemma quotient_of_denom_pos: "quotient_of r = (p, q) \ q > 0" ``` haftmann@35369 ` 392` ``` by (cases r) (simp add: quotient_of_Fract normalize_denom_pos) ``` haftmann@35369 ` 393` haftmann@35369 ` 394` ```lemma quotient_of_coprime: "quotient_of r = (p, q) \ coprime p q" ``` haftmann@35369 ` 395` ``` by (cases r) (simp add: quotient_of_Fract normalize_coprime) ``` nipkow@33805 ` 396` haftmann@35369 ` 397` ```lemma quotient_of_inject: ``` haftmann@35369 ` 398` ``` assumes "quotient_of a = quotient_of b" ``` haftmann@35369 ` 399` ``` shows "a = b" ``` haftmann@35369 ` 400` ```proof - ``` haftmann@35369 ` 401` ``` obtain p q r s where a: "a = Fract p q" ``` haftmann@35369 ` 402` ``` and b: "b = Fract r s" ``` haftmann@35369 ` 403` ``` and "q > 0" and "s > 0" by (cases a, cases b) ``` haftmann@35369 ` 404` ``` with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) ``` haftmann@35369 ` 405` ```qed ``` haftmann@35369 ` 406` haftmann@35369 ` 407` ```lemma quotient_of_inject_eq: ``` haftmann@35369 ` 408` ``` "quotient_of a = quotient_of b \ a = b" ``` haftmann@35369 ` 409` ``` by (auto simp add: quotient_of_inject) ``` nipkow@33805 ` 410` haftmann@27551 ` 411` haftmann@27551 ` 412` ```subsubsection {* The field of rational numbers *} ``` haftmann@27551 ` 413` haftmann@36409 ` 414` ```instantiation rat :: field_inverse_zero ``` haftmann@27551 ` 415` ```begin ``` haftmann@27551 ` 416` haftmann@27551 ` 417` ```definition ``` haftmann@35369 ` 418` ``` inverse_rat_def: ``` haftmann@27551 ` 419` ``` "inverse q = Abs_Rat (\x \ Rep_Rat q. ``` haftmann@27551 ` 420` ``` ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})" ``` haftmann@27551 ` 421` haftmann@27652 ` 422` ```lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" ``` haftmann@27551 ` 423` ```proof - ``` haftmann@27551 ` 424` ``` have "(\x. ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)}) respects ratrel" ``` haftmann@27551 ` 425` ``` by (auto simp add: congruent_def mult_commute) ``` haftmann@27551 ` 426` ``` then show ?thesis by (simp add: Fract_def inverse_rat_def UN_ratrel) ``` huffman@27509 ` 427` ```qed ``` huffman@27509 ` 428` haftmann@27551 ` 429` ```definition ``` haftmann@35369 ` 430` ``` divide_rat_def: "q / r = q * inverse (r::rat)" ``` haftmann@27551 ` 431` haftmann@27652 ` 432` ```lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)" ``` haftmann@27652 ` 433` ``` by (simp add: divide_rat_def) ``` haftmann@27551 ` 434` haftmann@27551 ` 435` ```instance proof ``` haftmann@27551 ` 436` ``` fix q :: rat ``` haftmann@27551 ` 437` ``` assume "q \ 0" ``` haftmann@27551 ` 438` ``` then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero) ``` huffman@35216 ` 439` ``` (simp_all add: rat_number_expand eq_rat) ``` haftmann@27551 ` 440` ```next ``` haftmann@27551 ` 441` ``` fix q r :: rat ``` haftmann@27551 ` 442` ``` show "q / r = q * inverse r" by (simp add: divide_rat_def) ``` haftmann@36415 ` 443` ```next ``` haftmann@36415 ` 444` ``` show "inverse 0 = (0::rat)" by (simp add: rat_number_expand, simp add: rat_number_collapse) ``` haftmann@36415 ` 445` ```qed ``` haftmann@27551 ` 446` haftmann@27551 ` 447` ```end ``` haftmann@27551 ` 448` haftmann@27551 ` 449` haftmann@27551 ` 450` ```subsubsection {* Various *} ``` haftmann@27551 ` 451` haftmann@27551 ` 452` ```lemma Fract_add_one: "n \ 0 ==> Fract (m + n) n = Fract m n + 1" ``` haftmann@27652 ` 453` ``` by (simp add: rat_number_expand) ``` haftmann@27551 ` 454` haftmann@27551 ` 455` ```lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" ``` haftmann@27652 ` 456` ``` by (simp add: Fract_of_int_eq [symmetric]) ``` haftmann@27551 ` 457` haftmann@35369 ` 458` ```lemma Fract_number_of_quotient: ``` haftmann@27551 ` 459` ``` "Fract (number_of k) (number_of l) = number_of k / number_of l" ``` haftmann@27551 ` 460` ``` unfolding Fract_of_int_quotient number_of_is_id number_of_eq .. ``` haftmann@27551 ` 461` haftmann@35369 ` 462` ```lemma Fract_1_number_of: ``` haftmann@27652 ` 463` ``` "Fract 1 (number_of k) = 1 / number_of k" ``` haftmann@27652 ` 464` ``` unfolding Fract_of_int_quotient number_of_eq by simp ``` haftmann@27551 ` 465` haftmann@27551 ` 466` ```subsubsection {* The ordered field of rational numbers *} ``` huffman@27509 ` 467` huffman@27509 ` 468` ```instantiation rat :: linorder ``` huffman@27509 ` 469` ```begin ``` huffman@27509 ` 470` huffman@27509 ` 471` ```definition ``` haftmann@35369 ` 472` ``` le_rat_def: ``` haftmann@39910 ` 473` ``` "q \ r \ the_elem (\x \ Rep_Rat q. \y \ Rep_Rat r. ``` haftmann@27551 ` 474` ``` {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)})" ``` haftmann@27551 ` 475` haftmann@27652 ` 476` ```lemma le_rat [simp]: ``` haftmann@27551 ` 477` ``` assumes "b \ 0" and "d \ 0" ``` haftmann@27551 ` 478` ``` shows "Fract a b \ Fract c d \ (a * d) * (b * d) \ (c * b) * (b * d)" ``` haftmann@27551 ` 479` ```proof - ``` haftmann@27551 ` 480` ``` have "(\x y. {(fst x * snd y) * (snd x * snd y) \ (fst y * snd x) * (snd x * snd y)}) ``` haftmann@27551 ` 481` ``` respects2 ratrel" ``` haftmann@27551 ` 482` ``` proof (clarsimp simp add: congruent2_def) ``` haftmann@27551 ` 483` ``` fix a b a' b' c d c' d'::int ``` haftmann@27551 ` 484` ``` assume neq: "b \ 0" "b' \ 0" "d \ 0" "d' \ 0" ``` haftmann@27551 ` 485` ``` assume eq1: "a * b' = a' * b" ``` haftmann@27551 ` 486` ``` assume eq2: "c * d' = c' * d" ``` haftmann@27551 ` 487` haftmann@27551 ` 488` ``` let ?le = "\a b c d. ((a * d) * (b * d) \ (c * b) * (b * d))" ``` haftmann@27551 ` 489` ``` { ``` haftmann@27551 ` 490` ``` fix a b c d x :: int assume x: "x \ 0" ``` haftmann@27551 ` 491` ``` have "?le a b c d = ?le (a * x) (b * x) c d" ``` haftmann@27551 ` 492` ``` proof - ``` haftmann@27551 ` 493` ``` from x have "0 < x * x" by (auto simp add: zero_less_mult_iff) ``` haftmann@27551 ` 494` ``` hence "?le a b c d = ``` haftmann@27551 ` 495` ``` ((a * d) * (b * d) * (x * x) \ (c * b) * (b * d) * (x * x))" ``` haftmann@27551 ` 496` ``` by (simp add: mult_le_cancel_right) ``` haftmann@27551 ` 497` ``` also have "... = ?le (a * x) (b * x) c d" ``` haftmann@27551 ` 498` ``` by (simp add: mult_ac) ``` haftmann@27551 ` 499` ``` finally show ?thesis . ``` haftmann@27551 ` 500` ``` qed ``` haftmann@27551 ` 501` ``` } note le_factor = this ``` haftmann@27551 ` 502` haftmann@27551 ` 503` ``` let ?D = "b * d" and ?D' = "b' * d'" ``` haftmann@27551 ` 504` ``` from neq have D: "?D \ 0" by simp ``` haftmann@27551 ` 505` ``` from neq have "?D' \ 0" by simp ``` haftmann@27551 ` 506` ``` hence "?le a b c d = ?le (a * ?D') (b * ?D') c d" ``` haftmann@27551 ` 507` ``` by (rule le_factor) ``` chaieb@27668 ` 508` ``` also have "... = ((a * b') * ?D * ?D' * d * d' \ (c * d') * ?D * ?D' * b * b')" ``` haftmann@27551 ` 509` ``` by (simp add: mult_ac) ``` haftmann@27551 ` 510` ``` also have "... = ((a' * b) * ?D * ?D' * d * d' \ (c' * d) * ?D * ?D' * b * b')" ``` haftmann@27551 ` 511` ``` by (simp only: eq1 eq2) ``` haftmann@27551 ` 512` ``` also have "... = ?le (a' * ?D) (b' * ?D) c' d'" ``` haftmann@27551 ` 513` ``` by (simp add: mult_ac) ``` haftmann@27551 ` 514` ``` also from D have "... = ?le a' b' c' d'" ``` haftmann@27551 ` 515` ``` by (rule le_factor [symmetric]) ``` haftmann@27551 ` 516` ``` finally show "?le a b c d = ?le a' b' c' d'" . ``` haftmann@27551 ` 517` ``` qed ``` haftmann@27551 ` 518` ``` with assms show ?thesis by (simp add: Fract_def le_rat_def UN_ratrel2) ``` haftmann@27551 ` 519` ```qed ``` huffman@27509 ` 520` huffman@27509 ` 521` ```definition ``` haftmann@35369 ` 522` ``` less_rat_def: "z < (w::rat) \ z \ w \ z \ w" ``` huffman@27509 ` 523` haftmann@27652 ` 524` ```lemma less_rat [simp]: ``` haftmann@27551 ` 525` ``` assumes "b \ 0" and "d \ 0" ``` haftmann@27551 ` 526` ``` shows "Fract a b < Fract c d \ (a * d) * (b * d) < (c * b) * (b * d)" ``` haftmann@27652 ` 527` ``` using assms by (simp add: less_rat_def eq_rat order_less_le) ``` huffman@27509 ` 528` huffman@27509 ` 529` ```instance proof ``` paulson@14365 ` 530` ``` fix q r s :: rat ``` paulson@14365 ` 531` ``` { ``` paulson@14365 ` 532` ``` assume "q \ r" and "r \ s" ``` haftmann@35369 ` 533` ``` then show "q \ s" ``` haftmann@35369 ` 534` ``` proof (induct q, induct r, induct s) ``` paulson@14365 ` 535` ``` fix a b c d e f :: int ``` haftmann@35369 ` 536` ``` assume neq: "b > 0" "d > 0" "f > 0" ``` paulson@14365 ` 537` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract e f" ``` paulson@14365 ` 538` ``` show "Fract a b \ Fract e f" ``` paulson@14365 ` 539` ``` proof - ``` paulson@14365 ` 540` ``` from neq obtain bb: "0 < b * b" and dd: "0 < d * d" and ff: "0 < f * f" ``` paulson@14365 ` 541` ``` by (auto simp add: zero_less_mult_iff linorder_neq_iff) ``` paulson@14365 ` 542` ``` have "(a * d) * (b * d) * (f * f) \ (c * b) * (b * d) * (f * f)" ``` paulson@14365 ` 543` ``` proof - ``` paulson@14365 ` 544` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` haftmann@27652 ` 545` ``` by simp ``` paulson@14365 ` 546` ``` with ff show ?thesis by (simp add: mult_le_cancel_right) ``` paulson@14365 ` 547` ``` qed ``` chaieb@27668 ` 548` ``` also have "... = (c * f) * (d * f) * (b * b)" by algebra ``` paulson@14365 ` 549` ``` also have "... \ (e * d) * (d * f) * (b * b)" ``` paulson@14365 ` 550` ``` proof - ``` paulson@14365 ` 551` ``` from neq 2 have "(c * f) * (d * f) \ (e * d) * (d * f)" ``` haftmann@27652 ` 552` ``` by simp ``` paulson@14365 ` 553` ``` with bb show ?thesis by (simp add: mult_le_cancel_right) ``` paulson@14365 ` 554` ``` qed ``` paulson@14365 ` 555` ``` finally have "(a * f) * (b * f) * (d * d) \ e * b * (b * f) * (d * d)" ``` paulson@14365 ` 556` ``` by (simp only: mult_ac) ``` paulson@14365 ` 557` ``` with dd have "(a * f) * (b * f) \ (e * b) * (b * f)" ``` paulson@14365 ` 558` ``` by (simp add: mult_le_cancel_right) ``` haftmann@27652 ` 559` ``` with neq show ?thesis by simp ``` paulson@14365 ` 560` ``` qed ``` paulson@14365 ` 561` ``` qed ``` paulson@14365 ` 562` ``` next ``` paulson@14365 ` 563` ``` assume "q \ r" and "r \ q" ``` haftmann@35369 ` 564` ``` then show "q = r" ``` haftmann@35369 ` 565` ``` proof (induct q, induct r) ``` paulson@14365 ` 566` ``` fix a b c d :: int ``` haftmann@35369 ` 567` ``` assume neq: "b > 0" "d > 0" ``` paulson@14365 ` 568` ``` assume 1: "Fract a b \ Fract c d" and 2: "Fract c d \ Fract a b" ``` paulson@14365 ` 569` ``` show "Fract a b = Fract c d" ``` paulson@14365 ` 570` ``` proof - ``` paulson@14365 ` 571` ``` from neq 1 have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` haftmann@27652 ` 572` ``` by simp ``` paulson@14365 ` 573` ``` also have "... \ (a * d) * (b * d)" ``` paulson@14365 ` 574` ``` proof - ``` paulson@14365 ` 575` ``` from neq 2 have "(c * b) * (d * b) \ (a * d) * (d * b)" ``` haftmann@27652 ` 576` ``` by simp ``` paulson@14365 ` 577` ``` thus ?thesis by (simp only: mult_ac) ``` paulson@14365 ` 578` ``` qed ``` paulson@14365 ` 579` ``` finally have "(a * d) * (b * d) = (c * b) * (b * d)" . ``` paulson@14365 ` 580` ``` moreover from neq have "b * d \ 0" by simp ``` paulson@14365 ` 581` ``` ultimately have "a * d = c * b" by simp ``` paulson@14365 ` 582` ``` with neq show ?thesis by (simp add: eq_rat) ``` paulson@14365 ` 583` ``` qed ``` paulson@14365 ` 584` ``` qed ``` paulson@14365 ` 585` ``` next ``` paulson@14365 ` 586` ``` show "q \ q" ``` haftmann@27652 ` 587` ``` by (induct q) simp ``` haftmann@27682 ` 588` ``` show "(q < r) = (q \ r \ \ r \ q)" ``` haftmann@27682 ` 589` ``` by (induct q, induct r) (auto simp add: le_less mult_commute) ``` paulson@14365 ` 590` ``` show "q \ r \ r \ q" ``` huffman@18913 ` 591` ``` by (induct q, induct r) ``` haftmann@27652 ` 592` ``` (simp add: mult_commute, rule linorder_linear) ``` paulson@14365 ` 593` ``` } ``` paulson@14365 ` 594` ```qed ``` paulson@14365 ` 595` huffman@27509 ` 596` ```end ``` huffman@27509 ` 597` haftmann@27551 ` 598` ```instantiation rat :: "{distrib_lattice, abs_if, sgn_if}" ``` haftmann@25571 ` 599` ```begin ``` haftmann@25571 ` 600` haftmann@25571 ` 601` ```definition ``` haftmann@35369 ` 602` ``` abs_rat_def: "\q\ = (if q < 0 then -q else (q::rat))" ``` haftmann@27551 ` 603` haftmann@27652 ` 604` ```lemma abs_rat [simp, code]: "\Fract a b\ = Fract \a\ \b\" ``` huffman@35216 ` 605` ``` by (auto simp add: abs_rat_def zabs_def Zero_rat_def not_less le_less eq_rat zero_less_mult_iff) ``` haftmann@27551 ` 606` haftmann@27551 ` 607` ```definition ``` haftmann@35369 ` 608` ``` sgn_rat_def: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)" ``` haftmann@27551 ` 609` haftmann@27652 ` 610` ```lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)" ``` haftmann@27551 ` 611` ``` unfolding Fract_of_int_eq ``` haftmann@27652 ` 612` ``` by (auto simp: zsgn_def sgn_rat_def Zero_rat_def eq_rat) ``` haftmann@27551 ` 613` ``` (auto simp: rat_number_collapse not_less le_less zero_less_mult_iff) ``` haftmann@27551 ` 614` haftmann@27551 ` 615` ```definition ``` haftmann@25571 ` 616` ``` "(inf \ rat \ rat \ rat) = min" ``` haftmann@25571 ` 617` haftmann@25571 ` 618` ```definition ``` haftmann@25571 ` 619` ``` "(sup \ rat \ rat \ rat) = max" ``` haftmann@25571 ` 620` haftmann@27551 ` 621` ```instance by intro_classes ``` haftmann@27551 ` 622` ``` (auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def) ``` haftmann@22456 ` 623` haftmann@25571 ` 624` ```end ``` haftmann@25571 ` 625` haftmann@36409 ` 626` ```instance rat :: linordered_field_inverse_zero ``` haftmann@27551 ` 627` ```proof ``` paulson@14365 ` 628` ``` fix q r s :: rat ``` paulson@14365 ` 629` ``` show "q \ r ==> s + q \ s + r" ``` paulson@14365 ` 630` ``` proof (induct q, induct r, induct s) ``` paulson@14365 ` 631` ``` fix a b c d e f :: int ``` haftmann@35369 ` 632` ``` assume neq: "b > 0" "d > 0" "f > 0" ``` paulson@14365 ` 633` ``` assume le: "Fract a b \ Fract c d" ``` paulson@14365 ` 634` ``` show "Fract e f + Fract a b \ Fract e f + Fract c d" ``` paulson@14365 ` 635` ``` proof - ``` paulson@14365 ` 636` ``` let ?F = "f * f" from neq have F: "0 < ?F" ``` paulson@14365 ` 637` ``` by (auto simp add: zero_less_mult_iff) ``` paulson@14365 ` 638` ``` from neq le have "(a * d) * (b * d) \ (c * b) * (b * d)" ``` haftmann@27652 ` 639` ``` by simp ``` paulson@14365 ` 640` ``` with F have "(a * d) * (b * d) * ?F * ?F \ (c * b) * (b * d) * ?F * ?F" ``` paulson@14365 ` 641` ``` by (simp add: mult_le_cancel_right) ``` haftmann@27652 ` 642` ``` with neq show ?thesis by (simp add: mult_ac int_distrib) ``` paulson@14365 ` 643` ``` qed ``` paulson@14365 ` 644` ``` qed ``` paulson@14365 ` 645` ``` show "q < r ==> 0 < s ==> s * q < s * r" ``` paulson@14365 ` 646` ``` proof (induct q, induct r, induct s) ``` paulson@14365 ` 647` ``` fix a b c d e f :: int ``` haftmann@35369 ` 648` ``` assume neq: "b > 0" "d > 0" "f > 0" ``` paulson@14365 ` 649` ``` assume le: "Fract a b < Fract c d" ``` paulson@14365 ` 650` ``` assume gt: "0 < Fract e f" ``` paulson@14365 ` 651` ``` show "Fract e f * Fract a b < Fract e f * Fract c d" ``` paulson@14365 ` 652` ``` proof - ``` paulson@14365 ` 653` ``` let ?E = "e * f" and ?F = "f * f" ``` paulson@14365 ` 654` ``` from neq gt have "0 < ?E" ``` haftmann@27652 ` 655` ``` by (auto simp add: Zero_rat_def order_less_le eq_rat) ``` paulson@14365 ` 656` ``` moreover from neq have "0 < ?F" ``` paulson@14365 ` 657` ``` by (auto simp add: zero_less_mult_iff) ``` paulson@14365 ` 658` ``` moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)" ``` haftmann@27652 ` 659` ``` by simp ``` paulson@14365 ` 660` ``` ultimately have "(a * d) * (b * d) * ?E * ?F < (c * b) * (b * d) * ?E * ?F" ``` paulson@14365 ` 661` ``` by (simp add: mult_less_cancel_right) ``` paulson@14365 ` 662` ``` with neq show ?thesis ``` haftmann@27652 ` 663` ``` by (simp add: mult_ac) ``` paulson@14365 ` 664` ``` qed ``` paulson@14365 ` 665` ``` qed ``` haftmann@27551 ` 666` ```qed auto ``` paulson@14365 ` 667` haftmann@27551 ` 668` ```lemma Rat_induct_pos [case_names Fract, induct type: rat]: ``` haftmann@27551 ` 669` ``` assumes step: "\a b. 0 < b \ P (Fract a b)" ``` haftmann@27551 ` 670` ``` shows "P q" ``` paulson@14365 ` 671` ```proof (cases q) ``` haftmann@27551 ` 672` ``` have step': "\a b. b < 0 \ P (Fract a b)" ``` paulson@14365 ` 673` ``` proof - ``` paulson@14365 ` 674` ``` fix a::int and b::int ``` paulson@14365 ` 675` ``` assume b: "b < 0" ``` paulson@14365 ` 676` ``` hence "0 < -b" by simp ``` paulson@14365 ` 677` ``` hence "P (Fract (-a) (-b))" by (rule step) ``` paulson@14365 ` 678` ``` thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) ``` paulson@14365 ` 679` ``` qed ``` paulson@14365 ` 680` ``` case (Fract a b) ``` paulson@14365 ` 681` ``` thus "P q" by (force simp add: linorder_neq_iff step step') ``` paulson@14365 ` 682` ```qed ``` paulson@14365 ` 683` paulson@14365 ` 684` ```lemma zero_less_Fract_iff: ``` huffman@30095 ` 685` ``` "0 < b \ 0 < Fract a b \ 0 < a" ``` huffman@30095 ` 686` ``` by (simp add: Zero_rat_def zero_less_mult_iff) ``` huffman@30095 ` 687` huffman@30095 ` 688` ```lemma Fract_less_zero_iff: ``` huffman@30095 ` 689` ``` "0 < b \ Fract a b < 0 \ a < 0" ``` huffman@30095 ` 690` ``` by (simp add: Zero_rat_def mult_less_0_iff) ``` huffman@30095 ` 691` huffman@30095 ` 692` ```lemma zero_le_Fract_iff: ``` huffman@30095 ` 693` ``` "0 < b \ 0 \ Fract a b \ 0 \ a" ``` huffman@30095 ` 694` ``` by (simp add: Zero_rat_def zero_le_mult_iff) ``` huffman@30095 ` 695` huffman@30095 ` 696` ```lemma Fract_le_zero_iff: ``` huffman@30095 ` 697` ``` "0 < b \ Fract a b \ 0 \ a \ 0" ``` huffman@30095 ` 698` ``` by (simp add: Zero_rat_def mult_le_0_iff) ``` huffman@30095 ` 699` huffman@30095 ` 700` ```lemma one_less_Fract_iff: ``` huffman@30095 ` 701` ``` "0 < b \ 1 < Fract a b \ b < a" ``` huffman@30095 ` 702` ``` by (simp add: One_rat_def mult_less_cancel_right_disj) ``` huffman@30095 ` 703` huffman@30095 ` 704` ```lemma Fract_less_one_iff: ``` huffman@30095 ` 705` ``` "0 < b \ Fract a b < 1 \ a < b" ``` huffman@30095 ` 706` ``` by (simp add: One_rat_def mult_less_cancel_right_disj) ``` huffman@30095 ` 707` huffman@30095 ` 708` ```lemma one_le_Fract_iff: ``` huffman@30095 ` 709` ``` "0 < b \ 1 \ Fract a b \ b \ a" ``` huffman@30095 ` 710` ``` by (simp add: One_rat_def mult_le_cancel_right) ``` huffman@30095 ` 711` huffman@30095 ` 712` ```lemma Fract_le_one_iff: ``` huffman@30095 ` 713` ``` "0 < b \ Fract a b \ 1 \ a \ b" ``` huffman@30095 ` 714` ``` by (simp add: One_rat_def mult_le_cancel_right) ``` paulson@14365 ` 715` paulson@14378 ` 716` huffman@30097 ` 717` ```subsubsection {* Rationals are an Archimedean field *} ``` huffman@30097 ` 718` huffman@30097 ` 719` ```lemma rat_floor_lemma: ``` huffman@30097 ` 720` ``` shows "of_int (a div b) \ Fract a b \ Fract a b < of_int (a div b + 1)" ``` huffman@30097 ` 721` ```proof - ``` huffman@30097 ` 722` ``` have "Fract a b = of_int (a div b) + Fract (a mod b) b" ``` huffman@35293 ` 723` ``` by (cases "b = 0", simp, simp add: of_int_rat) ``` huffman@30097 ` 724` ``` moreover have "0 \ Fract (a mod b) b \ Fract (a mod b) b < 1" ``` huffman@35293 ` 725` ``` unfolding Fract_of_int_quotient ``` haftmann@36409 ` 726` ``` by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos) ``` huffman@30097 ` 727` ``` ultimately show ?thesis by simp ``` huffman@30097 ` 728` ```qed ``` huffman@30097 ` 729` huffman@30097 ` 730` ```instance rat :: archimedean_field ``` huffman@30097 ` 731` ```proof ``` huffman@30097 ` 732` ``` fix r :: rat ``` huffman@30097 ` 733` ``` show "\z. r \ of_int z" ``` huffman@30097 ` 734` ``` proof (induct r) ``` huffman@30097 ` 735` ``` case (Fract a b) ``` huffman@35293 ` 736` ``` have "Fract a b \ of_int (a div b + 1)" ``` huffman@35293 ` 737` ``` using rat_floor_lemma [of a b] by simp ``` huffman@30097 ` 738` ``` then show "\z. Fract a b \ of_int z" .. ``` huffman@30097 ` 739` ``` qed ``` huffman@30097 ` 740` ```qed ``` huffman@30097 ` 741` huffman@35293 ` 742` ```lemma floor_Fract: "floor (Fract a b) = a div b" ``` huffman@35293 ` 743` ``` using rat_floor_lemma [of a b] ``` huffman@30097 ` 744` ``` by (simp add: floor_unique) ``` huffman@30097 ` 745` huffman@30097 ` 746` haftmann@31100 ` 747` ```subsection {* Linear arithmetic setup *} ``` paulson@14387 ` 748` haftmann@31100 ` 749` ```declaration {* ``` haftmann@31100 ` 750` ``` K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] ``` haftmann@31100 ` 751` ``` (* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) ``` haftmann@31100 ` 752` ``` #> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_int_eq_iff} RS iffD2] ``` haftmann@31100 ` 753` ``` (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) ``` haftmann@31100 ` 754` ``` #> Lin_Arith.add_simps [@{thm neg_less_iff_less}, ``` haftmann@31100 ` 755` ``` @{thm True_implies_equals}, ``` haftmann@31100 ` 756` ``` read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, ``` haftmann@31100 ` 757` ``` @{thm divide_1}, @{thm divide_zero_left}, ``` haftmann@31100 ` 758` ``` @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, ``` haftmann@31100 ` 759` ``` @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, ``` haftmann@31100 ` 760` ``` @{thm of_int_minus}, @{thm of_int_diff}, ``` haftmann@31100 ` 761` ``` @{thm of_int_of_nat_eq}] ``` haftmann@31100 ` 762` ``` #> Lin_Arith.add_simprocs Numeral_Simprocs.field_cancel_numeral_factors ``` haftmann@31100 ` 763` ``` #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) ``` haftmann@31100 ` 764` ``` #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) ``` haftmann@31100 ` 765` ```*} ``` paulson@14387 ` 766` huffman@23342 ` 767` huffman@23342 ` 768` ```subsection {* Embedding from Rationals to other Fields *} ``` huffman@23342 ` 769` haftmann@24198 ` 770` ```class field_char_0 = field + ring_char_0 ``` huffman@23342 ` 771` haftmann@35028 ` 772` ```subclass (in linordered_field) field_char_0 .. ``` huffman@23342 ` 773` haftmann@27551 ` 774` ```context field_char_0 ``` haftmann@27551 ` 775` ```begin ``` haftmann@27551 ` 776` haftmann@27551 ` 777` ```definition of_rat :: "rat \ 'a" where ``` haftmann@39910 ` 778` ``` "of_rat q = the_elem (\(a,b) \ Rep_Rat q. {of_int a / of_int b})" ``` huffman@23342 ` 779` haftmann@27551 ` 780` ```end ``` haftmann@27551 ` 781` huffman@23342 ` 782` ```lemma of_rat_congruent: ``` haftmann@27551 ` 783` ``` "(\(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel" ``` huffman@23342 ` 784` ```apply (rule congruent.intro) ``` huffman@23342 ` 785` ```apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) ``` huffman@23342 ` 786` ```apply (simp only: of_int_mult [symmetric]) ``` huffman@23342 ` 787` ```done ``` huffman@23342 ` 788` haftmann@27551 ` 789` ```lemma of_rat_rat: "b \ 0 \ of_rat (Fract a b) = of_int a / of_int b" ``` haftmann@27551 ` 790` ``` unfolding Fract_def of_rat_def by (simp add: UN_ratrel of_rat_congruent) ``` huffman@23342 ` 791` huffman@23342 ` 792` ```lemma of_rat_0 [simp]: "of_rat 0 = 0" ``` huffman@23342 ` 793` ```by (simp add: Zero_rat_def of_rat_rat) ``` huffman@23342 ` 794` huffman@23342 ` 795` ```lemma of_rat_1 [simp]: "of_rat 1 = 1" ``` huffman@23342 ` 796` ```by (simp add: One_rat_def of_rat_rat) ``` huffman@23342 ` 797` huffman@23342 ` 798` ```lemma of_rat_add: "of_rat (a + b) = of_rat a + of_rat b" ``` haftmann@27652 ` 799` ```by (induct a, induct b, simp add: of_rat_rat add_frac_eq) ``` huffman@23342 ` 800` huffman@23343 ` 801` ```lemma of_rat_minus: "of_rat (- a) = - of_rat a" ``` haftmann@27652 ` 802` ```by (induct a, simp add: of_rat_rat) ``` huffman@23343 ` 803` huffman@23343 ` 804` ```lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" ``` huffman@23343 ` 805` ```by (simp only: diff_minus of_rat_add of_rat_minus) ``` huffman@23343 ` 806` huffman@23342 ` 807` ```lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" ``` haftmann@27652 ` 808` ```apply (induct a, induct b, simp add: of_rat_rat) ``` huffman@23342 ` 809` ```apply (simp add: divide_inverse nonzero_inverse_mult_distrib mult_ac) ``` huffman@23342 ` 810` ```done ``` huffman@23342 ` 811` huffman@23342 ` 812` ```lemma nonzero_of_rat_inverse: ``` huffman@23342 ` 813` ``` "a \ 0 \ of_rat (inverse a) = inverse (of_rat a)" ``` huffman@23343 ` 814` ```apply (rule inverse_unique [symmetric]) ``` huffman@23343 ` 815` ```apply (simp add: of_rat_mult [symmetric]) ``` huffman@23342 ` 816` ```done ``` huffman@23342 ` 817` huffman@23342 ` 818` ```lemma of_rat_inverse: ``` haftmann@36409 ` 819` ``` "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) = ``` huffman@23342 ` 820` ``` inverse (of_rat a)" ``` huffman@23342 ` 821` ```by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) ``` huffman@23342 ` 822` huffman@23342 ` 823` ```lemma nonzero_of_rat_divide: ``` huffman@23342 ` 824` ``` "b \ 0 \ of_rat (a / b) = of_rat a / of_rat b" ``` huffman@23342 ` 825` ```by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) ``` huffman@23342 ` 826` huffman@23342 ` 827` ```lemma of_rat_divide: ``` haftmann@36409 ` 828` ``` "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero}) ``` huffman@23342 ` 829` ``` = of_rat a / of_rat b" ``` haftmann@27652 ` 830` ```by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) ``` huffman@23342 ` 831` huffman@23343 ` 832` ```lemma of_rat_power: ``` haftmann@31017 ` 833` ``` "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" ``` huffman@30273 ` 834` ```by (induct n) (simp_all add: of_rat_mult) ``` huffman@23343 ` 835` huffman@23343 ` 836` ```lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" ``` huffman@23343 ` 837` ```apply (induct a, induct b) ``` huffman@23343 ` 838` ```apply (simp add: of_rat_rat eq_rat) ``` huffman@23343 ` 839` ```apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) ``` huffman@23343 ` 840` ```apply (simp only: of_int_mult [symmetric] of_int_eq_iff) ``` huffman@23343 ` 841` ```done ``` huffman@23343 ` 842` haftmann@27652 ` 843` ```lemma of_rat_less: ``` haftmann@35028 ` 844` ``` "(of_rat r :: 'a::linordered_field) < of_rat s \ r < s" ``` haftmann@27652 ` 845` ```proof (induct r, induct s) ``` haftmann@27652 ` 846` ``` fix a b c d :: int ``` haftmann@27652 ` 847` ``` assume not_zero: "b > 0" "d > 0" ``` haftmann@27652 ` 848` ``` then have "b * d > 0" by (rule mult_pos_pos) ``` haftmann@27652 ` 849` ``` have of_int_divide_less_eq: ``` haftmann@27652 ` 850` ``` "(of_int a :: 'a) / of_int b < of_int c / of_int d ``` haftmann@27652 ` 851` ``` \ (of_int a :: 'a) * of_int d < of_int c * of_int b" ``` haftmann@27652 ` 852` ``` using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) ``` haftmann@35028 ` 853` ``` show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) ``` haftmann@27652 ` 854` ``` \ Fract a b < Fract c d" ``` haftmann@27652 ` 855` ``` using not_zero `b * d > 0` ``` haftmann@27652 ` 856` ``` by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) ``` haftmann@27652 ` 857` ```qed ``` haftmann@27652 ` 858` haftmann@27652 ` 859` ```lemma of_rat_less_eq: ``` haftmann@35028 ` 860` ``` "(of_rat r :: 'a::linordered_field) \ of_rat s \ r \ s" ``` haftmann@27652 ` 861` ``` unfolding le_less by (auto simp add: of_rat_less) ``` haftmann@27652 ` 862` huffman@23343 ` 863` ```lemmas of_rat_eq_0_iff [simp] = of_rat_eq_iff [of _ 0, simplified] ``` huffman@23343 ` 864` haftmann@27652 ` 865` ```lemma of_rat_eq_id [simp]: "of_rat = id" ``` huffman@23343 ` 866` ```proof ``` huffman@23343 ` 867` ``` fix a ``` huffman@23343 ` 868` ``` show "of_rat a = id a" ``` huffman@23343 ` 869` ``` by (induct a) ``` haftmann@27652 ` 870` ``` (simp add: of_rat_rat Fract_of_int_eq [symmetric]) ``` huffman@23343 ` 871` ```qed ``` huffman@23343 ` 872` huffman@23343 ` 873` ```text{*Collapse nested embeddings*} ``` huffman@23343 ` 874` ```lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" ``` huffman@23343 ` 875` ```by (induct n) (simp_all add: of_rat_add) ``` huffman@23343 ` 876` huffman@23343 ` 877` ```lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" ``` haftmann@27652 ` 878` ```by (cases z rule: int_diff_cases) (simp add: of_rat_diff) ``` huffman@23343 ` 879` huffman@23343 ` 880` ```lemma of_rat_number_of_eq [simp]: ``` huffman@23343 ` 881` ``` "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})" ``` huffman@23343 ` 882` ```by (simp add: number_of_eq) ``` huffman@23343 ` 883` haftmann@23879 ` 884` ```lemmas zero_rat = Zero_rat_def ``` haftmann@23879 ` 885` ```lemmas one_rat = One_rat_def ``` haftmann@23879 ` 886` haftmann@24198 ` 887` ```abbreviation ``` haftmann@24198 ` 888` ``` rat_of_nat :: "nat \ rat" ``` haftmann@24198 ` 889` ```where ``` haftmann@24198 ` 890` ``` "rat_of_nat \ of_nat" ``` haftmann@24198 ` 891` haftmann@24198 ` 892` ```abbreviation ``` haftmann@24198 ` 893` ``` rat_of_int :: "int \ rat" ``` haftmann@24198 ` 894` ```where ``` haftmann@24198 ` 895` ``` "rat_of_int \ of_int" ``` haftmann@24198 ` 896` huffman@28010 ` 897` ```subsection {* The Set of Rational Numbers *} ``` berghofe@24533 ` 898` nipkow@28001 ` 899` ```context field_char_0 ``` nipkow@28001 ` 900` ```begin ``` nipkow@28001 ` 901` nipkow@28001 ` 902` ```definition ``` nipkow@28001 ` 903` ``` Rats :: "'a set" where ``` haftmann@35369 ` 904` ``` "Rats = range of_rat" ``` nipkow@28001 ` 905` nipkow@28001 ` 906` ```notation (xsymbols) ``` nipkow@28001 ` 907` ``` Rats ("\") ``` nipkow@28001 ` 908` nipkow@28001 ` 909` ```end ``` nipkow@28001 ` 910` huffman@28010 ` 911` ```lemma Rats_of_rat [simp]: "of_rat r \ Rats" ``` huffman@28010 ` 912` ```by (simp add: Rats_def) ``` huffman@28010 ` 913` huffman@28010 ` 914` ```lemma Rats_of_int [simp]: "of_int z \ Rats" ``` huffman@28010 ` 915` ```by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) ``` huffman@28010 ` 916` huffman@28010 ` 917` ```lemma Rats_of_nat [simp]: "of_nat n \ Rats" ``` huffman@28010 ` 918` ```by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) ``` huffman@28010 ` 919` huffman@28010 ` 920` ```lemma Rats_number_of [simp]: ``` huffman@28010 ` 921` ``` "(number_of w::'a::{number_ring,field_char_0}) \ Rats" ``` huffman@28010 ` 922` ```by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat) ``` huffman@28010 ` 923` huffman@28010 ` 924` ```lemma Rats_0 [simp]: "0 \ Rats" ``` huffman@28010 ` 925` ```apply (unfold Rats_def) ``` huffman@28010 ` 926` ```apply (rule range_eqI) ``` huffman@28010 ` 927` ```apply (rule of_rat_0 [symmetric]) ``` huffman@28010 ` 928` ```done ``` huffman@28010 ` 929` huffman@28010 ` 930` ```lemma Rats_1 [simp]: "1 \ Rats" ``` huffman@28010 ` 931` ```apply (unfold Rats_def) ``` huffman@28010 ` 932` ```apply (rule range_eqI) ``` huffman@28010 ` 933` ```apply (rule of_rat_1 [symmetric]) ``` huffman@28010 ` 934` ```done ``` huffman@28010 ` 935` huffman@28010 ` 936` ```lemma Rats_add [simp]: "\a \ Rats; b \ Rats\ \ a + b \ Rats" ``` huffman@28010 ` 937` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 938` ```apply (rule range_eqI) ``` huffman@28010 ` 939` ```apply (rule of_rat_add [symmetric]) ``` huffman@28010 ` 940` ```done ``` huffman@28010 ` 941` huffman@28010 ` 942` ```lemma Rats_minus [simp]: "a \ Rats \ - a \ Rats" ``` huffman@28010 ` 943` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 944` ```apply (rule range_eqI) ``` huffman@28010 ` 945` ```apply (rule of_rat_minus [symmetric]) ``` huffman@28010 ` 946` ```done ``` huffman@28010 ` 947` huffman@28010 ` 948` ```lemma Rats_diff [simp]: "\a \ Rats; b \ Rats\ \ a - b \ Rats" ``` huffman@28010 ` 949` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 950` ```apply (rule range_eqI) ``` huffman@28010 ` 951` ```apply (rule of_rat_diff [symmetric]) ``` huffman@28010 ` 952` ```done ``` huffman@28010 ` 953` huffman@28010 ` 954` ```lemma Rats_mult [simp]: "\a \ Rats; b \ Rats\ \ a * b \ Rats" ``` huffman@28010 ` 955` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 956` ```apply (rule range_eqI) ``` huffman@28010 ` 957` ```apply (rule of_rat_mult [symmetric]) ``` huffman@28010 ` 958` ```done ``` huffman@28010 ` 959` huffman@28010 ` 960` ```lemma nonzero_Rats_inverse: ``` huffman@28010 ` 961` ``` fixes a :: "'a::field_char_0" ``` huffman@28010 ` 962` ``` shows "\a \ Rats; a \ 0\ \ inverse a \ Rats" ``` huffman@28010 ` 963` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 964` ```apply (rule range_eqI) ``` huffman@28010 ` 965` ```apply (erule nonzero_of_rat_inverse [symmetric]) ``` huffman@28010 ` 966` ```done ``` huffman@28010 ` 967` huffman@28010 ` 968` ```lemma Rats_inverse [simp]: ``` haftmann@36409 ` 969` ``` fixes a :: "'a::{field_char_0, field_inverse_zero}" ``` huffman@28010 ` 970` ``` shows "a \ Rats \ inverse a \ Rats" ``` huffman@28010 ` 971` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 972` ```apply (rule range_eqI) ``` huffman@28010 ` 973` ```apply (rule of_rat_inverse [symmetric]) ``` huffman@28010 ` 974` ```done ``` huffman@28010 ` 975` huffman@28010 ` 976` ```lemma nonzero_Rats_divide: ``` huffman@28010 ` 977` ``` fixes a b :: "'a::field_char_0" ``` huffman@28010 ` 978` ``` shows "\a \ Rats; b \ Rats; b \ 0\ \ a / b \ Rats" ``` huffman@28010 ` 979` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 980` ```apply (rule range_eqI) ``` huffman@28010 ` 981` ```apply (erule nonzero_of_rat_divide [symmetric]) ``` huffman@28010 ` 982` ```done ``` huffman@28010 ` 983` huffman@28010 ` 984` ```lemma Rats_divide [simp]: ``` haftmann@36409 ` 985` ``` fixes a b :: "'a::{field_char_0, field_inverse_zero}" ``` huffman@28010 ` 986` ``` shows "\a \ Rats; b \ Rats\ \ a / b \ Rats" ``` huffman@28010 ` 987` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 988` ```apply (rule range_eqI) ``` huffman@28010 ` 989` ```apply (rule of_rat_divide [symmetric]) ``` huffman@28010 ` 990` ```done ``` huffman@28010 ` 991` huffman@28010 ` 992` ```lemma Rats_power [simp]: ``` haftmann@31017 ` 993` ``` fixes a :: "'a::field_char_0" ``` huffman@28010 ` 994` ``` shows "a \ Rats \ a ^ n \ Rats" ``` huffman@28010 ` 995` ```apply (auto simp add: Rats_def) ``` huffman@28010 ` 996` ```apply (rule range_eqI) ``` huffman@28010 ` 997` ```apply (rule of_rat_power [symmetric]) ``` huffman@28010 ` 998` ```done ``` huffman@28010 ` 999` huffman@28010 ` 1000` ```lemma Rats_cases [cases set: Rats]: ``` huffman@28010 ` 1001` ``` assumes "q \ \" ``` huffman@28010 ` 1002` ``` obtains (of_rat) r where "q = of_rat r" ``` huffman@28010 ` 1003` ``` unfolding Rats_def ``` huffman@28010 ` 1004` ```proof - ``` huffman@28010 ` 1005` ``` from `q \ \` have "q \ range of_rat" unfolding Rats_def . ``` huffman@28010 ` 1006` ``` then obtain r where "q = of_rat r" .. ``` huffman@28010 ` 1007` ``` then show thesis .. ``` huffman@28010 ` 1008` ```qed ``` huffman@28010 ` 1009` huffman@28010 ` 1010` ```lemma Rats_induct [case_names of_rat, induct set: Rats]: ``` huffman@28010 ` 1011` ``` "q \ \ \ (\r. P (of_rat r)) \ P q" ``` huffman@28010 ` 1012` ``` by (rule Rats_cases) auto ``` huffman@28010 ` 1013` nipkow@28001 ` 1014` berghofe@24533 ` 1015` ```subsection {* Implementation of rational numbers as pairs of integers *} ``` berghofe@24533 ` 1016` haftmann@35369 ` 1017` ```definition Frct :: "int \ int \ rat" where ``` haftmann@35369 ` 1018` ``` [simp]: "Frct p = Fract (fst p) (snd p)" ``` haftmann@35369 ` 1019` haftmann@36112 ` 1020` ```lemma [code abstype]: ``` haftmann@36112 ` 1021` ``` "Frct (quotient_of q) = q" ``` haftmann@36112 ` 1022` ``` by (cases q) (auto intro: quotient_of_eq) ``` haftmann@35369 ` 1023` haftmann@35369 ` 1024` ```lemma Frct_code_post [code_post]: ``` haftmann@35369 ` 1025` ``` "Frct (0, k) = 0" ``` haftmann@35369 ` 1026` ``` "Frct (k, 0) = 0" ``` haftmann@35369 ` 1027` ``` "Frct (1, 1) = 1" ``` haftmann@35369 ` 1028` ``` "Frct (number_of k, 1) = number_of k" ``` haftmann@35369 ` 1029` ``` "Frct (1, number_of k) = 1 / number_of k" ``` haftmann@35369 ` 1030` ``` "Frct (number_of k, number_of l) = number_of k / number_of l" ``` haftmann@35369 ` 1031` ``` by (simp_all add: rat_number_collapse Fract_number_of_quotient Fract_1_number_of) ``` haftmann@35369 ` 1032` haftmann@35369 ` 1033` ```declare quotient_of_Fract [code abstract] ``` haftmann@35369 ` 1034` haftmann@35369 ` 1035` ```lemma rat_zero_code [code abstract]: ``` haftmann@35369 ` 1036` ``` "quotient_of 0 = (0, 1)" ``` haftmann@35369 ` 1037` ``` by (simp add: Zero_rat_def quotient_of_Fract normalize_def) ``` haftmann@35369 ` 1038` haftmann@35369 ` 1039` ```lemma rat_one_code [code abstract]: ``` haftmann@35369 ` 1040` ``` "quotient_of 1 = (1, 1)" ``` haftmann@35369 ` 1041` ``` by (simp add: One_rat_def quotient_of_Fract normalize_def) ``` haftmann@35369 ` 1042` haftmann@35369 ` 1043` ```lemma rat_plus_code [code abstract]: ``` haftmann@35369 ` 1044` ``` "quotient_of (p + q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q ``` haftmann@35369 ` 1045` ``` in normalize (a * d + b * c, c * d))" ``` haftmann@35369 ` 1046` ``` by (cases p, cases q) (simp add: quotient_of_Fract) ``` haftmann@27652 ` 1047` haftmann@35369 ` 1048` ```lemma rat_uminus_code [code abstract]: ``` haftmann@35369 ` 1049` ``` "quotient_of (- p) = (let (a, b) = quotient_of p in (- a, b))" ``` haftmann@35369 ` 1050` ``` by (cases p) (simp add: quotient_of_Fract) ``` haftmann@35369 ` 1051` haftmann@35369 ` 1052` ```lemma rat_minus_code [code abstract]: ``` haftmann@35369 ` 1053` ``` "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q ``` haftmann@35369 ` 1054` ``` in normalize (a * d - b * c, c * d))" ``` haftmann@35369 ` 1055` ``` by (cases p, cases q) (simp add: quotient_of_Fract) ``` haftmann@35369 ` 1056` haftmann@35369 ` 1057` ```lemma rat_times_code [code abstract]: ``` haftmann@35369 ` 1058` ``` "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q ``` haftmann@35369 ` 1059` ``` in normalize (a * b, c * d))" ``` haftmann@35369 ` 1060` ``` by (cases p, cases q) (simp add: quotient_of_Fract) ``` berghofe@24533 ` 1061` haftmann@35369 ` 1062` ```lemma rat_inverse_code [code abstract]: ``` haftmann@35369 ` 1063` ``` "quotient_of (inverse p) = (let (a, b) = quotient_of p ``` haftmann@35369 ` 1064` ``` in if a = 0 then (0, 1) else (sgn a * b, \a\))" ``` haftmann@35369 ` 1065` ```proof (cases p) ``` haftmann@35369 ` 1066` ``` case (Fract a b) then show ?thesis ``` haftmann@35369 ` 1067` ``` by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd_int.commute) ``` haftmann@35369 ` 1068` ```qed ``` haftmann@35369 ` 1069` haftmann@35369 ` 1070` ```lemma rat_divide_code [code abstract]: ``` haftmann@35369 ` 1071` ``` "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q ``` haftmann@35369 ` 1072` ``` in normalize (a * d, c * b))" ``` haftmann@35369 ` 1073` ``` by (cases p, cases q) (simp add: quotient_of_Fract) ``` haftmann@35369 ` 1074` haftmann@35369 ` 1075` ```lemma rat_abs_code [code abstract]: ``` haftmann@35369 ` 1076` ``` "quotient_of \p\ = (let (a, b) = quotient_of p in (\a\, b))" ``` haftmann@35369 ` 1077` ``` by (cases p) (simp add: quotient_of_Fract) ``` haftmann@35369 ` 1078` haftmann@35369 ` 1079` ```lemma rat_sgn_code [code abstract]: ``` haftmann@35369 ` 1080` ``` "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" ``` haftmann@35369 ` 1081` ```proof (cases p) ``` haftmann@35369 ` 1082` ``` case (Fract a b) then show ?thesis ``` haftmann@35369 ` 1083` ``` by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) ``` haftmann@35369 ` 1084` ```qed ``` berghofe@24533 ` 1085` haftmann@38857 ` 1086` ```instantiation rat :: equal ``` haftmann@26513 ` 1087` ```begin ``` haftmann@26513 ` 1088` haftmann@35369 ` 1089` ```definition [code]: ``` haftmann@38857 ` 1090` ``` "HOL.equal a b \ quotient_of a = quotient_of b" ``` haftmann@26513 ` 1091` haftmann@35369 ` 1092` ```instance proof ``` haftmann@38857 ` 1093` ```qed (simp add: equal_rat_def quotient_of_inject_eq) ``` haftmann@26513 ` 1094` haftmann@28351 ` 1095` ```lemma rat_eq_refl [code nbe]: ``` haftmann@38857 ` 1096` ``` "HOL.equal (r::rat) r \ True" ``` haftmann@38857 ` 1097` ``` by (rule equal_refl) ``` haftmann@28351 ` 1098` haftmann@26513 ` 1099` ```end ``` berghofe@24533 ` 1100` haftmann@35369 ` 1101` ```lemma rat_less_eq_code [code]: ``` haftmann@35369 ` 1102` ``` "p \ q \ (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \ c * b)" ``` haftmann@35726 ` 1103` ``` by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) ``` berghofe@24533 ` 1104` haftmann@35369 ` 1105` ```lemma rat_less_code [code]: ``` haftmann@35369 ` 1106` ``` "p < q \ (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" ``` haftmann@35726 ` 1107` ``` by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) ``` berghofe@24533 ` 1108` haftmann@35369 ` 1109` ```lemma [code]: ``` haftmann@35369 ` 1110` ``` "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" ``` haftmann@35369 ` 1111` ``` by (cases p) (simp add: quotient_of_Fract of_rat_rat) ``` haftmann@27652 ` 1112` haftmann@31203 ` 1113` ```definition (in term_syntax) ``` haftmann@32657 ` 1114` ``` valterm_fract :: "int \ (unit \ Code_Evaluation.term) \ int \ (unit \ Code_Evaluation.term) \ rat \ (unit \ Code_Evaluation.term)" where ``` haftmann@32657 ` 1115` ``` [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\} k {\} l" ``` haftmann@31203 ` 1116` haftmann@37751 ` 1117` ```notation fcomp (infixl "\>" 60) ``` haftmann@37751 ` 1118` ```notation scomp (infixl "\\" 60) ``` haftmann@31203 ` 1119` haftmann@31203 ` 1120` ```instantiation rat :: random ``` haftmann@31203 ` 1121` ```begin ``` haftmann@31203 ` 1122` haftmann@31203 ` 1123` ```definition ``` haftmann@37751 ` 1124` ``` "Quickcheck.random i = Quickcheck.random i \\ (\num. Random.range i \\ (\denom. Pair ( ``` haftmann@31205 ` 1125` ``` let j = Code_Numeral.int_of (denom + 1) ``` haftmann@32657 ` 1126` ``` in valterm_fract num (j, \u. Code_Evaluation.term_of j))))" ``` haftmann@31203 ` 1127` haftmann@31203 ` 1128` ```instance .. ``` haftmann@31203 ` 1129` haftmann@31203 ` 1130` ```end ``` haftmann@31203 ` 1131` haftmann@37751 ` 1132` ```no_notation fcomp (infixl "\>" 60) ``` haftmann@37751 ` 1133` ```no_notation scomp (infixl "\\" 60) ``` haftmann@31203 ` 1134` haftmann@24622 ` 1135` ```text {* Setup for SML code generator *} ``` berghofe@24533 ` 1136` berghofe@24533 ` 1137` ```types_code ``` berghofe@24533 ` 1138` ``` rat ("(int */ int)") ``` berghofe@24533 ` 1139` ```attach (term_of) {* ``` berghofe@24533 ` 1140` ```fun term_of_rat (p, q) = ``` haftmann@24622 ` 1141` ``` let ``` haftmann@35372 ` 1142` ``` val rT = Type ("Rat.rat", []) ``` berghofe@24533 ` 1143` ``` in ``` berghofe@24533 ` 1144` ``` if q = 1 orelse p = 0 then HOLogic.mk_number rT p ``` berghofe@25885 ` 1145` ``` else @{term "op / \ rat \ rat \ rat"} \$ ``` berghofe@24533 ` 1146` ``` HOLogic.mk_number rT p \$ HOLogic.mk_number rT q ``` berghofe@24533 ` 1147` ``` end; ``` berghofe@24533 ` 1148` ```*} ``` berghofe@24533 ` 1149` ```attach (test) {* ``` berghofe@24533 ` 1150` ```fun gen_rat i = ``` berghofe@24533 ` 1151` ``` let ``` berghofe@24533 ` 1152` ``` val p = random_range 0 i; ``` berghofe@24533 ` 1153` ``` val q = random_range 1 (i + 1); ``` berghofe@24533 ` 1154` ``` val g = Integer.gcd p q; ``` wenzelm@24630 ` 1155` ``` val p' = p div g; ``` wenzelm@24630 ` 1156` ``` val q' = q div g; ``` berghofe@25885 ` 1157` ``` val r = (if one_of [true, false] then p' else ~ p', ``` haftmann@31666 ` 1158` ``` if p' = 0 then 1 else q') ``` berghofe@24533 ` 1159` ``` in ``` berghofe@25885 ` 1160` ``` (r, fn () => term_of_rat r) ``` berghofe@24533 ` 1161` ``` end; ``` berghofe@24533 ` 1162` ```*} ``` berghofe@24533 ` 1163` berghofe@24533 ` 1164` ```consts_code ``` haftmann@27551 ` 1165` ``` Fract ("(_,/ _)") ``` berghofe@24533 ` 1166` berghofe@24533 ` 1167` ```consts_code ``` haftmann@35375 ` 1168` ``` quotient_of ("{*normalize*}") ``` haftmann@35375 ` 1169` haftmann@35375 ` 1170` ```consts_code ``` berghofe@24533 ` 1171` ``` "of_int :: int \ rat" ("\rat'_of'_int") ``` berghofe@24533 ` 1172` ```attach {* ``` haftmann@31674 ` 1173` ```fun rat_of_int i = (i, 1); ``` berghofe@24533 ` 1174` ```*} ``` berghofe@24533 ` 1175` blanchet@38287 ` 1176` ```declaration {* ``` blanchet@38287 ` 1177` ``` Nitpick_HOL.register_frac_type @{type_name rat} ``` wenzelm@33209 ` 1178` ``` [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}), ``` wenzelm@33209 ` 1179` ``` (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}), ``` wenzelm@33209 ` 1180` ``` (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}), ``` wenzelm@33209 ` 1181` ``` (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}), ``` wenzelm@33209 ` 1182` ``` (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}), ``` wenzelm@33209 ` 1183` ``` (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}), ``` wenzelm@33209 ` 1184` ``` (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}), ``` blanchet@37397 ` 1185` ``` (@{const_name ord_rat_inst.less_rat}, @{const_name Nitpick.less_frac}), ``` wenzelm@33209 ` 1186` ``` (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}), ``` wenzelm@33209 ` 1187` ``` (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}), ``` wenzelm@35402 ` 1188` ``` (@{const_name field_char_0_class.Rats}, @{const_abbrev UNIV})] ``` blanchet@33197 ` 1189` ```*} ``` blanchet@33197 ` 1190` blanchet@33197 ` 1191` ```lemmas [nitpick_def] = inverse_rat_inst.inverse_rat ``` blanchet@37397 ` 1192` ``` number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_rat ``` blanchet@37397 ` 1193` ``` ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat ``` blanchet@37397 ` 1194` ``` uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat ``` blanchet@33197 ` 1195` huffman@35343 ` 1196` ```subsection{* Float syntax *} ``` huffman@35343 ` 1197` huffman@35343 ` 1198` ```syntax "_Float" :: "float_const \ 'a" ("_") ``` huffman@35343 ` 1199` huffman@35343 ` 1200` ```use "Tools/float_syntax.ML" ``` huffman@35343 ` 1201` ```setup Float_Syntax.setup ``` huffman@35343 ` 1202` huffman@35343 ` 1203` ```text{* Test: *} ``` huffman@35343 ` 1204` ```lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)" ``` huffman@35343 ` 1205` ```by simp ``` huffman@35343 ` 1206` wenzelm@37143 ` 1207` wenzelm@37143 ` 1208` ```hide_const (open) normalize ``` wenzelm@37143 ` 1209` huffman@29880 ` 1210` ```end ```