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