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