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