1(* Title: HOL/GCD.thy 2 Author: Christophe Tabacznyj 3 Author: Lawrence C. Paulson 4 Author: Amine Chaieb 5 Author: Thomas M. Rasmussen 6 Author: Jeremy Avigad 7 Author: Tobias Nipkow 8 9This file deals with the functions gcd and lcm. Definitions and 10lemmas are proved uniformly for the natural numbers and integers. 11 12This file combines and revises a number of prior developments. 13 14The original theories "GCD" and "Primes" were by Christophe Tabacznyj 15and Lawrence C. Paulson, based on @{cite davenport92}. They introduced 16gcd, lcm, and prime for the natural numbers. 17 18The original theory "IntPrimes" was by Thomas M. Rasmussen, and 19extended gcd, lcm, primes to the integers. Amine Chaieb provided 20another extension of the notions to the integers, and added a number 21of results to "Primes" and "GCD". IntPrimes also defined and developed 22the congruence relations on the integers. The notion was extended to 23the natural numbers by Chaieb. 24 25Jeremy Avigad combined all of these, made everything uniform for the 26natural numbers and the integers, and added a number of new theorems. 27 28Tobias Nipkow cleaned up a lot. 29*) 30 31section \<open>Greatest common divisor and least common multiple\<close> 32 33theory GCD 34 imports Groups_List 35begin 36 37subsection \<open>Abstract bounded quasi semilattices as common foundation\<close> 38 39locale bounded_quasi_semilattice = abel_semigroup + 40 fixes top :: 'a ("\<^bold>\<top>") and bot :: 'a ("\<^bold>\<bottom>") 41 and normalize :: "'a \<Rightarrow> 'a" 42 assumes idem_normalize [simp]: "a \<^bold>* a = normalize a" 43 and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b" 44 and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b" 45 and normalize_top [simp]: "normalize \<^bold>\<top> = \<^bold>\<top>" 46 and normalize_bottom [simp]: "normalize \<^bold>\<bottom> = \<^bold>\<bottom>" 47 and top_left_normalize [simp]: "\<^bold>\<top> \<^bold>* a = normalize a" 48 and bottom_left_bottom [simp]: "\<^bold>\<bottom> \<^bold>* a = \<^bold>\<bottom>" 49begin 50 51lemma left_idem [simp]: 52 "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" 53 using assoc [of a a b, symmetric] by simp 54 55lemma right_idem [simp]: 56 "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" 57 using left_idem [of b a] by (simp add: ac_simps) 58 59lemma comp_fun_idem: "comp_fun_idem f" 60 by standard (simp_all add: fun_eq_iff ac_simps) 61 62interpretation comp_fun_idem f 63 by (fact comp_fun_idem) 64 65lemma top_right_normalize [simp]: 66 "a \<^bold>* \<^bold>\<top> = normalize a" 67 using top_left_normalize [of a] by (simp add: ac_simps) 68 69lemma bottom_right_bottom [simp]: 70 "a \<^bold>* \<^bold>\<bottom> = \<^bold>\<bottom>" 71 using bottom_left_bottom [of a] by (simp add: ac_simps) 72 73lemma normalize_right_idem [simp]: 74 "a \<^bold>* normalize b = a \<^bold>* b" 75 using normalize_left_idem [of b a] by (simp add: ac_simps) 76 77end 78 79locale bounded_quasi_semilattice_set = bounded_quasi_semilattice 80begin 81 82interpretation comp_fun_idem f 83 by (fact comp_fun_idem) 84 85definition F :: "'a set \<Rightarrow> 'a" 86where 87 eq_fold: "F A = (if finite A then Finite_Set.fold f \<^bold>\<top> A else \<^bold>\<bottom>)" 88 89lemma infinite [simp]: 90 "infinite A \<Longrightarrow> F A = \<^bold>\<bottom>" 91 by (simp add: eq_fold) 92 93lemma set_eq_fold [code]: 94 "F (set xs) = fold f xs \<^bold>\<top>" 95 by (simp add: eq_fold fold_set_fold) 96 97lemma empty [simp]: 98 "F {} = \<^bold>\<top>" 99 by (simp add: eq_fold) 100 101lemma insert [simp]: 102 "F (insert a A) = a \<^bold>* F A" 103 by (cases "finite A") (simp_all add: eq_fold) 104 105lemma normalize [simp]: 106 "normalize (F A) = F A" 107 by (induct A rule: infinite_finite_induct) simp_all 108 109lemma in_idem: 110 assumes "a \<in> A" 111 shows "a \<^bold>* F A = F A" 112 using assms by (induct A rule: infinite_finite_induct) 113 (auto simp: left_commute [of a]) 114 115lemma union: 116 "F (A \<union> B) = F A \<^bold>* F B" 117 by (induct A rule: infinite_finite_induct) 118 (simp_all add: ac_simps) 119 120lemma remove: 121 assumes "a \<in> A" 122 shows "F A = a \<^bold>* F (A - {a})" 123proof - 124 from assms obtain B where "A = insert a B" and "a \<notin> B" 125 by (blast dest: mk_disjoint_insert) 126 with assms show ?thesis by simp 127qed 128 129lemma insert_remove: 130 "F (insert a A) = a \<^bold>* F (A - {a})" 131 by (cases "a \<in> A") (simp_all add: insert_absorb remove) 132 133lemma subset: 134 assumes "B \<subseteq> A" 135 shows "F B \<^bold>* F A = F A" 136 using assms by (simp add: union [symmetric] Un_absorb1) 137 138end 139 140subsection \<open>Abstract GCD and LCM\<close> 141 142class gcd = zero + one + dvd + 143 fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 144 and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 145 146class Gcd = gcd + 147 fixes Gcd :: "'a set \<Rightarrow> 'a" 148 and Lcm :: "'a set \<Rightarrow> 'a" 149 150syntax 151 "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _./ _)" [0, 10] 10) 152 "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _\<in>_./ _)" [0, 0, 10] 10) 153 "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _./ _)" [0, 10] 10) 154 "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _\<in>_./ _)" [0, 0, 10] 10) 155 156translations 157 "GCD x y. f" \<rightleftharpoons> "GCD x. GCD y. f" 158 "GCD x. f" \<rightleftharpoons> "CONST Gcd (CONST range (\<lambda>x. f))" 159 "GCD x\<in>A. f" \<rightleftharpoons> "CONST Gcd ((\<lambda>x. f) ` A)" 160 "LCM x y. f" \<rightleftharpoons> "LCM x. LCM y. f" 161 "LCM x. f" \<rightleftharpoons> "CONST Lcm (CONST range (\<lambda>x. f))" 162 "LCM x\<in>A. f" \<rightleftharpoons> "CONST Lcm ((\<lambda>x. f) ` A)" 163 164class semiring_gcd = normalization_semidom + gcd + 165 assumes gcd_dvd1 [iff]: "gcd a b dvd a" 166 and gcd_dvd2 [iff]: "gcd a b dvd b" 167 and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" 168 and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b" 169 and lcm_gcd: "lcm a b = normalize (a * b div gcd a b)" 170begin 171 172lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c" 173 by (blast intro!: gcd_greatest intro: dvd_trans) 174 175lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c" 176 by (rule dvd_trans) (rule gcd_dvd1) 177 178lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c" 179 by (rule dvd_trans) (rule gcd_dvd2) 180 181lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b" 182 using gcd_dvd1 [of b c] by (blast intro: dvd_trans) 183 184lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c" 185 using gcd_dvd2 [of b c] by (blast intro: dvd_trans) 186 187lemma gcd_0_left [simp]: "gcd 0 a = normalize a" 188 by (rule associated_eqI) simp_all 189 190lemma gcd_0_right [simp]: "gcd a 0 = normalize a" 191 by (rule associated_eqI) simp_all 192 193lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" 194 (is "?P \<longleftrightarrow> ?Q") 195proof 196 assume ?P 197 then have "0 dvd gcd a b" 198 by simp 199 then have "0 dvd a" and "0 dvd b" 200 by (blast intro: dvd_trans)+ 201 then show ?Q 202 by simp 203next 204 assume ?Q 205 then show ?P 206 by simp 207qed 208 209lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" 210proof (cases "gcd a b = 0") 211 case True 212 then show ?thesis by simp 213next 214 case False 215 have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b" 216 by (rule unit_factor_mult_normalize) 217 then have "unit_factor (gcd a b) * gcd a b = gcd a b" 218 by simp 219 then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b" 220 by simp 221 with False show ?thesis 222 by simp 223qed 224 225lemma is_unit_gcd_iff [simp]: 226 "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1" 227 by (cases "a = 0 \<and> b = 0") (auto simp: unit_factor_gcd dest: is_unit_unit_factor) 228 229sublocale gcd: abel_semigroup gcd 230proof 231 fix a b c 232 show "gcd a b = gcd b a" 233 by (rule associated_eqI) simp_all 234 from gcd_dvd1 have "gcd (gcd a b) c dvd a" 235 by (rule dvd_trans) simp 236 moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b" 237 by (rule dvd_trans) simp 238 ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)" 239 by (auto intro!: gcd_greatest) 240 from gcd_dvd2 have "gcd a (gcd b c) dvd b" 241 by (rule dvd_trans) simp 242 moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c" 243 by (rule dvd_trans) simp 244 ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c" 245 by (auto intro!: gcd_greatest) 246 from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)" 247 by (rule associated_eqI) simp_all 248qed 249 250sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize 251proof 252 show "gcd a a = normalize a" for a 253 proof - 254 have "a dvd gcd a a" 255 by (rule gcd_greatest) simp_all 256 then show ?thesis 257 by (auto intro: associated_eqI) 258 qed 259 show "gcd (normalize a) b = gcd a b" for a b 260 using gcd_dvd1 [of "normalize a" b] 261 by (auto intro: associated_eqI) 262 show "gcd 1 a = 1" for a 263 by (rule associated_eqI) simp_all 264qed simp_all 265 266lemma gcd_self: "gcd a a = normalize a" 267 by (fact gcd.idem_normalize) 268 269lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b" 270 by (fact gcd.left_idem) 271 272lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b" 273 by (fact gcd.right_idem) 274 275lemma gcdI: 276 assumes "c dvd a" and "c dvd b" 277 and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c" 278 and "normalize c = c" 279 shows "c = gcd a b" 280 by (rule associated_eqI) (auto simp: assms intro: gcd_greatest) 281 282lemma gcd_unique: 283 "d dvd a \<and> d dvd b \<and> normalize d = d \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 284 by rule (auto intro: gcdI simp: gcd_greatest) 285 286lemma gcd_dvd_prod: "gcd a b dvd k * b" 287 using mult_dvd_mono [of 1] by auto 288 289lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b" 290 by (rule gcdI [symmetric]) simp_all 291 292lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a" 293 by (rule gcdI [symmetric]) simp_all 294 295lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n" 296proof 297 assume *: "gcd m n = normalize m" 298 show "m dvd n" 299 proof (cases "m = 0") 300 case True 301 with * show ?thesis by simp 302 next 303 case [simp]: False 304 from * have **: "m = gcd m n * unit_factor m" 305 by (simp add: unit_eq_div2) 306 show ?thesis 307 by (subst **) (simp add: mult_unit_dvd_iff) 308 qed 309next 310 assume "m dvd n" 311 then show "gcd m n = normalize m" 312 by (rule gcd_proj1_if_dvd) 313qed 314 315lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m" 316 using gcd_proj1_iff [of n m] by (simp add: ac_simps) 317 318lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize (c * gcd a b)" 319proof (cases "c = 0") 320 case True 321 then show ?thesis by simp 322next 323 case False 324 then have *: "c * gcd a b dvd gcd (c * a) (c * b)" 325 by (auto intro: gcd_greatest) 326 moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b" 327 by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute) 328 ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)" 329 by (auto intro: associated_eqI) 330 then show ?thesis 331 by (simp add: normalize_mult) 332qed 333 334lemma gcd_mult_right: "gcd (a * c) (b * c) = normalize (gcd b a * c)" 335 using gcd_mult_left [of c a b] by (simp add: ac_simps) 336 337lemma dvd_lcm1 [iff]: "a dvd lcm a b" 338 by (metis div_mult_swap dvd_mult2 dvd_normalize_iff dvd_refl gcd_dvd2 lcm_gcd) 339 340lemma dvd_lcm2 [iff]: "b dvd lcm a b" 341 by (metis dvd_div_mult dvd_mult dvd_normalize_iff dvd_refl gcd_dvd1 lcm_gcd) 342 343lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c" 344 by (rule dvd_trans) (assumption, blast) 345 346lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c" 347 by (rule dvd_trans) (assumption, blast) 348 349lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c" 350 using dvd_lcm1 [of a b] by (blast intro: dvd_trans) 351 352lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c" 353 using dvd_lcm2 [of a b] by (blast intro: dvd_trans) 354 355lemma lcm_least: 356 assumes "a dvd c" and "b dvd c" 357 shows "lcm a b dvd c" 358proof (cases "c = 0") 359 case True 360 then show ?thesis by simp 361next 362 case False 363 then have *: "is_unit (unit_factor c)" 364 by simp 365 show ?thesis 366 proof (cases "gcd a b = 0") 367 case True 368 with assms show ?thesis by simp 369 next 370 case False 371 have "a * b dvd normalize (c * gcd a b)" 372 using assms by (subst gcd_mult_left [symmetric]) (auto intro!: gcd_greatest simp: mult_ac) 373 with False have "(a * b div gcd a b) dvd c" 374 by (subst div_dvd_iff_mult) auto 375 thus ?thesis by (simp add: lcm_gcd) 376 qed 377qed 378 379lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c" 380 by (blast intro!: lcm_least intro: dvd_trans) 381 382lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b" 383 by (simp add: lcm_gcd dvd_normalize_div) 384 385lemma lcm_0_left [simp]: "lcm 0 a = 0" 386 by (simp add: lcm_gcd) 387 388lemma lcm_0_right [simp]: "lcm a 0 = 0" 389 by (simp add: lcm_gcd) 390 391lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 392 (is "?P \<longleftrightarrow> ?Q") 393proof 394 assume ?P 395 then have "0 dvd lcm a b" 396 by simp 397 also have "lcm a b dvd (a * b)" 398 by simp 399 finally show ?Q 400 by auto 401next 402 assume ?Q 403 then show ?P 404 by auto 405qed 406 407lemma zero_eq_lcm_iff: "0 = lcm a b \<longleftrightarrow> a = 0 \<or> b = 0" 408 using lcm_eq_0_iff[of a b] by auto 409 410lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b" 411 by (auto intro: associated_eqI) 412 413lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)" 414 using lcm_eq_0_iff[of a b] by (cases "lcm a b = 0") (auto simp: lcm_gcd) 415 416sublocale lcm: abel_semigroup lcm 417proof 418 fix a b c 419 show "lcm a b = lcm b a" 420 by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div) 421 have "lcm (lcm a b) c dvd lcm a (lcm b c)" 422 and "lcm a (lcm b c) dvd lcm (lcm a b) c" 423 by (auto intro: lcm_least 424 dvd_trans [of b "lcm b c" "lcm a (lcm b c)"] 425 dvd_trans [of c "lcm b c" "lcm a (lcm b c)"] 426 dvd_trans [of a "lcm a b" "lcm (lcm a b) c"] 427 dvd_trans [of b "lcm a b" "lcm (lcm a b) c"]) 428 then show "lcm (lcm a b) c = lcm a (lcm b c)" 429 by (rule associated_eqI) simp_all 430qed 431 432sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize 433proof 434 show "lcm a a = normalize a" for a 435 proof - 436 have "lcm a a dvd a" 437 by (rule lcm_least) simp_all 438 then show ?thesis 439 by (auto intro: associated_eqI) 440 qed 441 show "lcm (normalize a) b = lcm a b" for a b 442 using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff 443 by (auto intro: associated_eqI) 444 show "lcm 1 a = normalize a" for a 445 by (rule associated_eqI) simp_all 446qed simp_all 447 448lemma lcm_self: "lcm a a = normalize a" 449 by (fact lcm.idem_normalize) 450 451lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b" 452 by (fact lcm.left_idem) 453 454lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b" 455 by (fact lcm.right_idem) 456 457lemma gcd_lcm: 458 assumes "a \<noteq> 0" and "b \<noteq> 0" 459 shows "gcd a b = normalize (a * b div lcm a b)" 460proof - 461 from assms have [simp]: "a * b div gcd a b \<noteq> 0" 462 by (subst dvd_div_eq_0_iff) auto 463 let ?u = "unit_factor (a * b div gcd a b)" 464 have "gcd a b * normalize (a * b div gcd a b) = 465 gcd a b * ((a * b div gcd a b) * (1 div ?u))" 466 by simp 467 also have "\<dots> = a * b div ?u" 468 by (subst mult.assoc [symmetric]) auto 469 also have "\<dots> dvd a * b" 470 by (subst div_unit_dvd_iff) auto 471 finally have "gcd a b dvd ((a * b) div lcm a b)" 472 by (intro dvd_mult_imp_div) (auto simp: lcm_gcd) 473 moreover have "a * b div lcm a b dvd a" and "a * b div lcm a b dvd b" 474 using assms by (subst div_dvd_iff_mult; simp add: lcm_eq_0_iff mult.commute[of b "lcm a b"])+ 475 ultimately have "normalize (gcd a b) = normalize (a * b div lcm a b)" 476 apply - 477 apply (rule associated_eqI) 478 using assms 479 apply (auto simp: div_dvd_iff_mult zero_eq_lcm_iff) 480 done 481 thus ?thesis by simp 482qed 483 484lemma lcm_1_left: "lcm 1 a = normalize a" 485 by (fact lcm.top_left_normalize) 486 487lemma lcm_1_right: "lcm a 1 = normalize a" 488 by (fact lcm.top_right_normalize) 489 490lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize (c * lcm a b)" 491proof (cases "c = 0") 492 case True 493 then show ?thesis by simp 494next 495 case False 496 then have *: "lcm (c * a) (c * b) dvd c * lcm a b" 497 by (auto intro: lcm_least) 498 moreover have "lcm a b dvd lcm (c * a) (c * b) div c" 499 by (intro lcm_least) (auto intro!: dvd_mult_imp_div simp: mult_ac) 500 hence "c * lcm a b dvd lcm (c * a) (c * b)" 501 using False by (subst (asm) dvd_div_iff_mult) (auto simp: mult_ac intro: dvd_lcmI1) 502 ultimately have "normalize (lcm (c * a) (c * b)) = normalize (c * lcm a b)" 503 by (auto intro: associated_eqI) 504 then show ?thesis 505 by (simp add: normalize_mult) 506qed 507 508lemma lcm_mult_right: "lcm (a * c) (b * c) = normalize (lcm b a * c)" 509 using lcm_mult_left [of c a b] by (simp add: ac_simps) 510 511lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c" 512 by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1) 513 514lemma lcm_mult_unit2: "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c" 515 using lcm_mult_unit1 [of a c b] by (simp add: ac_simps) 516 517lemma lcm_div_unit1: 518 "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c" 519 by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 520 521lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c" 522 by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2) 523 524lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b" 525 by (fact lcm.normalize_left_idem) 526 527lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b" 528 by (fact lcm.normalize_right_idem) 529 530lemma comp_fun_idem_gcd: "comp_fun_idem gcd" 531 by standard (simp_all add: fun_eq_iff ac_simps) 532 533lemma comp_fun_idem_lcm: "comp_fun_idem lcm" 534 by standard (simp_all add: fun_eq_iff ac_simps) 535 536lemma gcd_dvd_antisym: "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d" 537proof (rule gcdI) 538 assume *: "gcd a b dvd gcd c d" 539 and **: "gcd c d dvd gcd a b" 540 have "gcd c d dvd c" 541 by simp 542 with * show "gcd a b dvd c" 543 by (rule dvd_trans) 544 have "gcd c d dvd d" 545 by simp 546 with * show "gcd a b dvd d" 547 by (rule dvd_trans) 548 show "normalize (gcd a b) = gcd a b" 549 by simp 550 fix l assume "l dvd c" and "l dvd d" 551 then have "l dvd gcd c d" 552 by (rule gcd_greatest) 553 from this and ** show "l dvd gcd a b" 554 by (rule dvd_trans) 555qed 556 557declare unit_factor_lcm [simp] 558 559lemma lcmI: 560 assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d" 561 and "normalize c = c" 562 shows "c = lcm a b" 563 by (rule associated_eqI) (auto simp: assms intro: lcm_least) 564 565lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b" 566 using gcd_dvd2 by (rule dvd_lcmI2) 567 568lemmas lcm_0 = lcm_0_right 569 570lemma lcm_unique: 571 "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" 572 by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff) 573 574lemma lcm_proj1_if_dvd: 575 assumes "b dvd a" shows "lcm a b = normalize a" 576proof - 577 have "normalize (lcm a b) = normalize a" 578 by (rule associatedI) (use assms in auto) 579 thus ?thesis by simp 580qed 581 582lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b" 583 using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps) 584 585lemma lcm_proj1_iff: "lcm m n = normalize m \<longleftrightarrow> n dvd m" 586proof 587 assume *: "lcm m n = normalize m" 588 show "n dvd m" 589 proof (cases "m = 0") 590 case True 591 then show ?thesis by simp 592 next 593 case [simp]: False 594 from * have **: "m = lcm m n * unit_factor m" 595 by (simp add: unit_eq_div2) 596 show ?thesis by (subst **) simp 597 qed 598next 599 assume "n dvd m" 600 then show "lcm m n = normalize m" 601 by (rule lcm_proj1_if_dvd) 602qed 603 604lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n" 605 using lcm_proj1_iff [of n m] by (simp add: ac_simps) 606 607lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d" 608 by (simp add: gcd_dvdI1 gcd_dvdI2) 609 610lemma lcm_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> lcm a b dvd lcm c d" 611 by (simp add: dvd_lcmI1 dvd_lcmI2) 612 613lemma dvd_productE: 614 assumes "p dvd a * b" 615 obtains x y where "p = x * y" "x dvd a" "y dvd b" 616proof (cases "a = 0") 617 case True 618 thus ?thesis by (intro that[of p 1]) simp_all 619next 620 case False 621 define x y where "x = gcd a p" and "y = p div x" 622 have "p = x * y" by (simp add: x_def y_def) 623 moreover have "x dvd a" by (simp add: x_def) 624 moreover from assms have "p dvd gcd (b * a) (b * p)" 625 by (intro gcd_greatest) (simp_all add: mult.commute) 626 hence "p dvd b * gcd a p" by (subst (asm) gcd_mult_left) auto 627 with False have "y dvd b" 628 by (simp add: x_def y_def div_dvd_iff_mult assms) 629 ultimately show ?thesis by (rule that) 630qed 631 632lemma gcd_mult_unit1: 633 assumes "is_unit a" shows "gcd (b * a) c = gcd b c" 634proof - 635 have "gcd (b * a) c dvd b" 636 using assms dvd_mult_unit_iff by blast 637 then show ?thesis 638 by (rule gcdI) simp_all 639qed 640 641lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c" 642 using gcd.commute gcd_mult_unit1 by auto 643 644lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c" 645 by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1) 646 647lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c" 648 by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2) 649 650lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b" 651 by (fact gcd.normalize_left_idem) 652 653lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b" 654 by (fact gcd.normalize_right_idem) 655 656lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n" 657 by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff) 658 659lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n" 660 using gcd_add1 [of n m] by (simp add: ac_simps) 661 662lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n" 663 by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff) 664 665end 666 667class ring_gcd = comm_ring_1 + semiring_gcd 668begin 669 670lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b" 671 by (rule sym, rule gcdI) (simp_all add: gcd_greatest) 672 673lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b" 674 by (rule sym, rule gcdI) (simp_all add: gcd_greatest) 675 676lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a" 677 by (fact gcd_neg1) 678 679lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)" 680 by (fact gcd_neg2) 681 682lemma gcd_diff1: "gcd (m - n) n = gcd m n" 683 by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp) 684 685lemma gcd_diff2: "gcd (n - m) n = gcd m n" 686 by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1) 687 688lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b" 689 by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff) 690 691lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b" 692 by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff) 693 694lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a" 695 by (fact lcm_neg1) 696 697lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)" 698 by (fact lcm_neg2) 699 700end 701 702class semiring_Gcd = semiring_gcd + Gcd + 703 assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a" 704 and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A" 705 and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A" 706 assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A" 707 and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a" 708 and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A" 709begin 710 711lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}" 712 by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 713 714lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}" 715 by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least) 716 717lemma Gcd_empty [simp]: "Gcd {} = 0" 718 by (rule dvd_0_left, rule Gcd_greatest) simp 719 720lemma Lcm_empty [simp]: "Lcm {} = 1" 721 by (auto intro: associated_eqI Lcm_least) 722 723lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)" 724proof - 725 have "Gcd (insert a A) dvd gcd a (Gcd A)" 726 by (auto intro: Gcd_dvd Gcd_greatest) 727 moreover have "gcd a (Gcd A) dvd Gcd (insert a A)" 728 proof (rule Gcd_greatest) 729 fix b 730 assume "b \<in> insert a A" 731 then show "gcd a (Gcd A) dvd b" 732 proof 733 assume "b = a" 734 then show ?thesis 735 by simp 736 next 737 assume "b \<in> A" 738 then have "Gcd A dvd b" 739 by (rule Gcd_dvd) 740 moreover have "gcd a (Gcd A) dvd Gcd A" 741 by simp 742 ultimately show ?thesis 743 by (blast intro: dvd_trans) 744 qed 745 qed 746 ultimately show ?thesis 747 by (auto intro: associated_eqI) 748qed 749 750lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)" 751proof (rule sym) 752 have "lcm a (Lcm A) dvd Lcm (insert a A)" 753 by (auto intro: dvd_Lcm Lcm_least) 754 moreover have "Lcm (insert a A) dvd lcm a (Lcm A)" 755 proof (rule Lcm_least) 756 fix b 757 assume "b \<in> insert a A" 758 then show "b dvd lcm a (Lcm A)" 759 proof 760 assume "b = a" 761 then show ?thesis by simp 762 next 763 assume "b \<in> A" 764 then have "b dvd Lcm A" 765 by (rule dvd_Lcm) 766 moreover have "Lcm A dvd lcm a (Lcm A)" 767 by simp 768 ultimately show ?thesis 769 by (blast intro: dvd_trans) 770 qed 771 qed 772 ultimately show "lcm a (Lcm A) = Lcm (insert a A)" 773 by (rule associated_eqI) (simp_all add: lcm_eq_0_iff) 774qed 775 776lemma LcmI: 777 assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" 778 and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c" 779 and "normalize b = b" 780 shows "b = Lcm A" 781 by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least) 782 783lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B" 784 by (blast intro: Lcm_least dvd_Lcm) 785 786lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)" 787proof - 788 have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d" 789 by (meson UnE Lcm_least dvd_Lcm dvd_trans) 790 then show ?thesis 791 by (meson Lcm_subset lcm_unique normalize_Lcm sup.cobounded1 sup.cobounded2) 792qed 793 794lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" 795 (is "?P \<longleftrightarrow> ?Q") 796proof 797 assume ?P 798 show ?Q 799 proof 800 fix a 801 assume "a \<in> A" 802 then have "Gcd A dvd a" 803 by (rule Gcd_dvd) 804 with \<open>?P\<close> have "a = 0" 805 by simp 806 then show "a \<in> {0}" 807 by simp 808 qed 809next 810 assume ?Q 811 have "0 dvd Gcd A" 812 proof (rule Gcd_greatest) 813 fix a 814 assume "a \<in> A" 815 with \<open>?Q\<close> have "a = 0" 816 by auto 817 then show "0 dvd a" 818 by simp 819 qed 820 then show ?P 821 by simp 822qed 823 824lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" 825 (is "?P \<longleftrightarrow> ?Q") 826proof 827 assume ?P 828 show ?Q 829 proof 830 fix a 831 assume "a \<in> A" 832 then have "a dvd Lcm A" 833 by (rule dvd_Lcm) 834 with \<open>?P\<close> show "is_unit a" 835 by simp 836 qed 837next 838 assume ?Q 839 then have "is_unit (Lcm A)" 840 by (blast intro: Lcm_least) 841 then have "normalize (Lcm A) = 1" 842 by (rule is_unit_normalize) 843 then show ?P 844 by simp 845qed 846 847lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" 848proof (cases "Lcm A = 0") 849 case True 850 then show ?thesis 851 by simp 852next 853 case False 854 with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1" 855 by blast 856 with False show ?thesis 857 by simp 858qed 859 860lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)" 861 by (simp add: Gcd_Lcm unit_factor_Lcm) 862 863lemma GcdI: 864 assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" 865 and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b" 866 and "normalize b = b" 867 shows "b = Gcd A" 868 by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest) 869 870lemma Gcd_eq_1_I: 871 assumes "is_unit a" and "a \<in> A" 872 shows "Gcd A = 1" 873proof - 874 from assms have "is_unit (Gcd A)" 875 by (blast intro: Gcd_dvd dvd_unit_imp_unit) 876 then have "normalize (Gcd A) = 1" 877 by (rule is_unit_normalize) 878 then show ?thesis 879 by simp 880qed 881 882lemma Lcm_eq_0_I: 883 assumes "0 \<in> A" 884 shows "Lcm A = 0" 885proof - 886 from assms have "0 dvd Lcm A" 887 by (rule dvd_Lcm) 888 then show ?thesis 889 by simp 890qed 891 892lemma Gcd_UNIV [simp]: "Gcd UNIV = 1" 893 using dvd_refl by (rule Gcd_eq_1_I) simp 894 895lemma Lcm_UNIV [simp]: "Lcm UNIV = 0" 896 by (rule Lcm_eq_0_I) simp 897 898lemma Lcm_0_iff: 899 assumes "finite A" 900 shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" 901proof (cases "A = {}") 902 case True 903 then show ?thesis by simp 904next 905 case False 906 with assms show ?thesis 907 by (induct A rule: finite_ne_induct) (auto simp: lcm_eq_0_iff) 908qed 909 910lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A" 911proof - 912 have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a 913 proof - 914 from that obtain B where "A = insert a B" 915 by blast 916 moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a" 917 by (rule gcd_dvd1) 918 ultimately show "Gcd (normalize ` A) dvd a" 919 by simp 920 qed 921 then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)" 922 by (auto intro!: Gcd_greatest intro: Gcd_dvd) 923 then show ?thesis 924 by (auto intro: associated_eqI) 925qed 926 927lemma Gcd_eqI: 928 assumes "normalize a = a" 929 assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b" 930 and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a" 931 shows "Gcd A = a" 932 using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd) 933 934lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y" 935 using Gcd_dvd dvd_trans by blast 936 937lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)" 938 by (blast dest: dvd_GcdD intro: Gcd_greatest) 939 940lemma Gcd_mult: "Gcd ((*) c ` A) = normalize (c * Gcd A)" 941proof (cases "c = 0") 942 case True 943 then show ?thesis by auto 944next 945 case [simp]: False 946 have "Gcd ((*) c ` A) div c dvd Gcd A" 947 by (intro Gcd_greatest, subst div_dvd_iff_mult) 948 (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c]) 949 then have "Gcd ((*) c ` A) dvd c * Gcd A" 950 by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac) 951 moreover have "c * Gcd A dvd Gcd ((*) c ` A)" 952 by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd) 953 ultimately have "normalize (Gcd ((*) c ` A)) = normalize (c * Gcd A)" 954 by (rule associatedI) 955 then show ?thesis by simp 956qed 957 958lemma Lcm_eqI: 959 assumes "normalize a = a" 960 and "\<And>b. b \<in> A \<Longrightarrow> b dvd a" 961 and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c" 962 shows "Lcm A = a" 963 using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm) 964 965lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x" 966 using dvd_Lcm dvd_trans by blast 967 968lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)" 969 by (blast dest: Lcm_dvdD intro: Lcm_least) 970 971lemma Lcm_mult: 972 assumes "A \<noteq> {}" 973 shows "Lcm ((*) c ` A) = normalize (c * Lcm A)" 974proof (cases "c = 0") 975 case True 976 with assms have "(*) c ` A = {0}" 977 by auto 978 with True show ?thesis by auto 979next 980 case [simp]: False 981 from assms obtain x where x: "x \<in> A" 982 by blast 983 have "c dvd c * x" 984 by simp 985 also from x have "c * x dvd Lcm ((*) c ` A)" 986 by (intro dvd_Lcm) auto 987 finally have dvd: "c dvd Lcm ((*) c ` A)" . 988 moreover have "Lcm A dvd Lcm ((*) c ` A) div c" 989 by (intro Lcm_least dvd_mult_imp_div) 990 (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c]) 991 ultimately have "c * Lcm A dvd Lcm ((*) c ` A)" 992 by auto 993 moreover have "Lcm ((*) c ` A) dvd c * Lcm A" 994 by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm) 995 ultimately have "normalize (c * Lcm A) = normalize (Lcm ((*) c ` A))" 996 by (rule associatedI) 997 then show ?thesis by simp 998qed 999 1000lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})" 1001proof - 1002 have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" 1003 by blast 1004 then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})" 1005 by (simp add: Lcm_Un [symmetric]) 1006 also have "Lcm {a\<in>A. is_unit a} = 1" 1007 by simp 1008 finally show ?thesis 1009 by simp 1010qed 1011 1012lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" 1013 by (metis Lcm_least dvd_0_left dvd_Lcm) 1014 1015lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0" 1016 by (auto simp: Lcm_0_iff') 1017 1018lemma Lcm_singleton [simp]: "Lcm {a} = normalize a" 1019 by simp 1020 1021lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b" 1022 by simp 1023 1024lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1" 1025 by (auto intro!: Gcd_eq_1_I) 1026 1027lemma Gcd_singleton [simp]: "Gcd {a} = normalize a" 1028 by simp 1029 1030lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b" 1031 by simp 1032 1033lemma Gcd_mono: 1034 assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x" 1035 shows "(GCD x\<in>A. f x) dvd (GCD x\<in>A. g x)" 1036proof (intro Gcd_greatest, safe) 1037 fix x assume "x \<in> A" 1038 hence "(GCD x\<in>A. f x) dvd f x" 1039 by (intro Gcd_dvd) auto 1040 also have "f x dvd g x" 1041 using \<open>x \<in> A\<close> assms by blast 1042 finally show "(GCD x\<in>A. f x) dvd \<dots>" . 1043qed 1044 1045lemma Lcm_mono: 1046 assumes "\<And>x. x \<in> A \<Longrightarrow> f x dvd g x" 1047 shows "(LCM x\<in>A. f x) dvd (LCM x\<in>A. g x)" 1048proof (intro Lcm_least, safe) 1049 fix x assume "x \<in> A" 1050 hence "f x dvd g x" by (rule assms) 1051 also have "g x dvd (LCM x\<in>A. g x)" 1052 using \<open>x \<in> A\<close> by (intro dvd_Lcm) auto 1053 finally show "f x dvd \<dots>" . 1054qed 1055 1056end 1057 1058 1059subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close> 1060 1061context semiring_gcd 1062begin 1063 1064sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize 1065defines 1066 Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" .. 1067 1068abbreviation gcd_list :: "'a list \<Rightarrow> 'a" 1069 where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)" 1070 1071sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize 1072defines 1073 Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F .. 1074 1075abbreviation lcm_list :: "'a list \<Rightarrow> 'a" 1076 where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)" 1077 1078lemma Gcd_fin_dvd: 1079 "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a" 1080 by (induct A rule: infinite_finite_induct) 1081 (auto intro: dvd_trans) 1082 1083lemma dvd_Lcm_fin: 1084 "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A" 1085 by (induct A rule: infinite_finite_induct) 1086 (auto intro: dvd_trans) 1087 1088lemma Gcd_fin_greatest: 1089 "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b" 1090 using that by (induct A) simp_all 1091 1092lemma Lcm_fin_least: 1093 "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a" 1094 using that by (induct A) simp_all 1095 1096lemma gcd_list_greatest: 1097 "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b" 1098 by (rule Gcd_fin_greatest) (simp_all add: that) 1099 1100lemma lcm_list_least: 1101 "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a" 1102 by (rule Lcm_fin_least) (simp_all add: that) 1103 1104lemma dvd_Gcd_fin_iff: 1105 "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A" 1106 using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"]) 1107 1108lemma dvd_gcd_list_iff: 1109 "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)" 1110 by (simp add: dvd_Gcd_fin_iff) 1111 1112lemma Lcm_fin_dvd_iff: 1113 "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A" 1114 using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b]) 1115 1116lemma lcm_list_dvd_iff: 1117 "lcm_list xs dvd b \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)" 1118 by (simp add: Lcm_fin_dvd_iff) 1119 1120lemma Gcd_fin_mult: 1121 "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A)" if "finite A" 1122 using that by induction (auto simp: gcd_mult_left) 1123 1124lemma Lcm_fin_mult: 1125 "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A)" if "A \<noteq> {}" 1126proof (cases "b = 0") 1127 case True 1128 moreover from that have "times 0 ` A = {0}" 1129 by auto 1130 ultimately show ?thesis 1131 by simp 1132next 1133 case False 1134 show ?thesis proof (cases "finite A") 1135 case False 1136 moreover have "inj_on (times b) A" 1137 using \<open>b \<noteq> 0\<close> by (rule inj_on_mult) 1138 ultimately have "infinite (times b ` A)" 1139 by (simp add: finite_image_iff) 1140 with False show ?thesis 1141 by simp 1142 next 1143 case True 1144 then show ?thesis using that 1145 by (induct A rule: finite_ne_induct) (auto simp: lcm_mult_left) 1146 qed 1147qed 1148 1149lemma unit_factor_Gcd_fin: 1150 "unit_factor (Gcd\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Gcd\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)" 1151 by (rule normalize_idem_imp_unit_factor_eq) simp 1152 1153lemma unit_factor_Lcm_fin: 1154 "unit_factor (Lcm\<^sub>f\<^sub>i\<^sub>n A) = of_bool (Lcm\<^sub>f\<^sub>i\<^sub>n A \<noteq> 0)" 1155 by (rule normalize_idem_imp_unit_factor_eq) simp 1156 1157lemma is_unit_Gcd_fin_iff [simp]: 1158 "is_unit (Gcd\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A = 1" 1159 by (rule normalize_idem_imp_is_unit_iff) simp 1160 1161lemma is_unit_Lcm_fin_iff [simp]: 1162 "is_unit (Lcm\<^sub>f\<^sub>i\<^sub>n A) \<longleftrightarrow> Lcm\<^sub>f\<^sub>i\<^sub>n A = 1" 1163 by (rule normalize_idem_imp_is_unit_iff) simp 1164 1165lemma Gcd_fin_0_iff: 1166 "Gcd\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> A \<subseteq> {0} \<and> finite A" 1167 by (induct A rule: infinite_finite_induct) simp_all 1168 1169lemma Lcm_fin_0_iff: 1170 "Lcm\<^sub>f\<^sub>i\<^sub>n A = 0 \<longleftrightarrow> 0 \<in> A" if "finite A" 1171 using that by (induct A) (auto simp: lcm_eq_0_iff) 1172 1173lemma Lcm_fin_1_iff: 1174 "Lcm\<^sub>f\<^sub>i\<^sub>n A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a) \<and> finite A" 1175 by (induct A rule: infinite_finite_induct) simp_all 1176 1177end 1178 1179context semiring_Gcd 1180begin 1181 1182lemma Gcd_fin_eq_Gcd [simp]: 1183 "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set" 1184 using that by induct simp_all 1185 1186lemma Gcd_set_eq_fold [code_unfold]: 1187 "Gcd (set xs) = fold gcd xs 0" 1188 by (simp add: Gcd_fin.set_eq_fold [symmetric]) 1189 1190lemma Lcm_fin_eq_Lcm [simp]: 1191 "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set" 1192 using that by induct simp_all 1193 1194lemma Lcm_set_eq_fold [code_unfold]: 1195 "Lcm (set xs) = fold lcm xs 1" 1196 by (simp add: Lcm_fin.set_eq_fold [symmetric]) 1197 1198end 1199 1200 1201subsection \<open>Coprimality\<close> 1202 1203context semiring_gcd 1204begin 1205 1206lemma coprime_imp_gcd_eq_1 [simp]: 1207 "gcd a b = 1" if "coprime a b" 1208proof - 1209 define t r s where "t = gcd a b" and "r = a div t" and "s = b div t" 1210 then have "a = t * r" and "b = t * s" 1211 by simp_all 1212 with that have "coprime (t * r) (t * s)" 1213 by simp 1214 then show ?thesis 1215 by (simp add: t_def) 1216qed 1217 1218lemma gcd_eq_1_imp_coprime [dest!]: 1219 "coprime a b" if "gcd a b = 1" 1220proof (rule coprimeI) 1221 fix c 1222 assume "c dvd a" and "c dvd b" 1223 then have "c dvd gcd a b" 1224 by (rule gcd_greatest) 1225 with that show "is_unit c" 1226 by simp 1227qed 1228 1229lemma coprime_iff_gcd_eq_1 [presburger, code]: 1230 "coprime a b \<longleftrightarrow> gcd a b = 1" 1231 by rule (simp_all add: gcd_eq_1_imp_coprime) 1232 1233lemma is_unit_gcd [simp]: 1234 "is_unit (gcd a b) \<longleftrightarrow> coprime a b" 1235 by (simp add: coprime_iff_gcd_eq_1) 1236 1237lemma coprime_add_one_left [simp]: "coprime (a + 1) a" 1238 by (simp add: gcd_eq_1_imp_coprime ac_simps) 1239 1240lemma coprime_add_one_right [simp]: "coprime a (a + 1)" 1241 using coprime_add_one_left [of a] by (simp add: ac_simps) 1242 1243lemma coprime_mult_left_iff [simp]: 1244 "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c" 1245proof 1246 assume "coprime (a * b) c" 1247 with coprime_common_divisor [of "a * b" c] 1248 have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d 1249 using that by blast 1250 have "coprime a c" 1251 by (rule coprimeI, rule *) simp_all 1252 moreover have "coprime b c" 1253 by (rule coprimeI, rule *) simp_all 1254 ultimately show "coprime a c \<and> coprime b c" .. 1255next 1256 assume "coprime a c \<and> coprime b c" 1257 then have "coprime a c" "coprime b c" 1258 by simp_all 1259 show "coprime (a * b) c" 1260 proof (rule coprimeI) 1261 fix d 1262 assume "d dvd a * b" 1263 then obtain r s where d: "d = r * s" "r dvd a" "s dvd b" 1264 by (rule dvd_productE) 1265 assume "d dvd c" 1266 with d have "r * s dvd c" 1267 by simp 1268 then have "r dvd c" "s dvd c" 1269 by (auto intro: dvd_mult_left dvd_mult_right) 1270 from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close> 1271 have "is_unit r" 1272 by (rule coprime_common_divisor) 1273 moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close> 1274 have "is_unit s" 1275 by (rule coprime_common_divisor) 1276 ultimately show "is_unit d" 1277 by (simp add: d is_unit_mult_iff) 1278 qed 1279qed 1280 1281lemma coprime_mult_right_iff [simp]: 1282 "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b" 1283 using coprime_mult_left_iff [of a b c] by (simp add: ac_simps) 1284 1285lemma coprime_power_left_iff [simp]: 1286 "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0" 1287proof (cases "n = 0") 1288 case True 1289 then show ?thesis 1290 by simp 1291next 1292 case False 1293 then have "n > 0" 1294 by simp 1295 then show ?thesis 1296 by (induction n rule: nat_induct_non_zero) simp_all 1297qed 1298 1299lemma coprime_power_right_iff [simp]: 1300 "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0" 1301 using coprime_power_left_iff [of b n a] by (simp add: ac_simps) 1302 1303lemma prod_coprime_left: 1304 "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a" 1305 using that by (induct A rule: infinite_finite_induct) simp_all 1306 1307lemma prod_coprime_right: 1308 "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)" 1309 using that prod_coprime_left [of A f a] by (simp add: ac_simps) 1310 1311lemma prod_list_coprime_left: 1312 "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a" 1313 using that by (induct xs) simp_all 1314 1315lemma prod_list_coprime_right: 1316 "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x" 1317 using that prod_list_coprime_left [of xs a] by (simp add: ac_simps) 1318 1319lemma coprime_dvd_mult_left_iff: 1320 "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c" 1321proof 1322 assume "a dvd b" 1323 then show "a dvd b * c" 1324 by simp 1325next 1326 assume "a dvd b * c" 1327 show "a dvd b" 1328 proof (cases "b = 0") 1329 case True 1330 then show ?thesis 1331 by simp 1332 next 1333 case False 1334 then have unit: "is_unit (unit_factor b)" 1335 by simp 1336 from \<open>coprime a c\<close> 1337 have "gcd (b * a) (b * c) * unit_factor b = b" 1338 by (subst gcd_mult_left) (simp add: ac_simps) 1339 moreover from \<open>a dvd b * c\<close> 1340 have "a dvd gcd (b * a) (b * c) * unit_factor b" 1341 by (simp add: dvd_mult_unit_iff unit) 1342 ultimately show ?thesis 1343 by simp 1344 qed 1345qed 1346 1347lemma coprime_dvd_mult_right_iff: 1348 "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c" 1349 using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps) 1350 1351lemma divides_mult: 1352 "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b" 1353proof - 1354 from \<open>b dvd c\<close> obtain b' where "c = b * b'" .. 1355 with \<open>a dvd c\<close> have "a dvd b' * b" 1356 by (simp add: ac_simps) 1357 with \<open>coprime a b\<close> have "a dvd b'" 1358 by (simp add: coprime_dvd_mult_left_iff) 1359 then obtain a' where "b' = a * a'" .. 1360 with \<open>c = b * b'\<close> have "c = (a * b) * a'" 1361 by (simp add: ac_simps) 1362 then show ?thesis .. 1363qed 1364 1365lemma div_gcd_coprime: 1366 assumes "a \<noteq> 0 \<or> b \<noteq> 0" 1367 shows "coprime (a div gcd a b) (b div gcd a b)" 1368proof - 1369 let ?g = "gcd a b" 1370 let ?a' = "a div ?g" 1371 let ?b' = "b div ?g" 1372 let ?g' = "gcd ?a' ?b'" 1373 have dvdg: "?g dvd a" "?g dvd b" 1374 by simp_all 1375 have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" 1376 by simp_all 1377 from dvdg dvdg' obtain ka kb ka' kb' where 1378 kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'" 1379 unfolding dvd_def by blast 1380 from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" 1381 by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"]) 1382 then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b" 1383 by (auto simp: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def) 1384 have "?g \<noteq> 0" 1385 using assms by simp 1386 moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" . 1387 ultimately show ?thesis 1388 using dvd_times_left_cancel_iff [of "gcd a b" _ 1] 1389 by simp (simp only: coprime_iff_gcd_eq_1) 1390qed 1391 1392lemma gcd_coprime: 1393 assumes c: "gcd a b \<noteq> 0" 1394 and a: "a = a' * gcd a b" 1395 and b: "b = b' * gcd a b" 1396 shows "coprime a' b'" 1397proof - 1398 from c have "a \<noteq> 0 \<or> b \<noteq> 0" 1399 by simp 1400 with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" . 1401 also from assms have "a div gcd a b = a'" 1402 using dvd_div_eq_mult gcd_dvd1 by blast 1403 also from assms have "b div gcd a b = b'" 1404 using dvd_div_eq_mult gcd_dvd1 by blast 1405 finally show ?thesis . 1406qed 1407 1408lemma gcd_coprime_exists: 1409 assumes "gcd a b \<noteq> 0" 1410 shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'" 1411proof - 1412 have "coprime (a div gcd a b) (b div gcd a b)" 1413 using assms div_gcd_coprime by auto 1414 then show ?thesis 1415 by force 1416qed 1417 1418lemma pow_divides_pow_iff [simp]: 1419 "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0" 1420proof (cases "gcd a b = 0") 1421 case True 1422 then show ?thesis 1423 by simp 1424next 1425 case False 1426 show ?thesis 1427 proof 1428 let ?d = "gcd a b" 1429 from \<open>n > 0\<close> obtain m where m: "n = Suc m" 1430 by (cases n) simp_all 1431 from False have zn: "?d ^ n \<noteq> 0" 1432 by (rule power_not_zero) 1433 from gcd_coprime_exists [OF False] 1434 obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'" 1435 by blast 1436 assume "a ^ n dvd b ^ n" 1437 then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n" 1438 by (simp add: ab'(1,2)[symmetric]) 1439 then have "?d^n * a'^n dvd ?d^n * b'^n" 1440 by (simp only: power_mult_distrib ac_simps) 1441 with zn have "a' ^ n dvd b' ^ n" 1442 by simp 1443 then have "a' dvd b' ^ n" 1444 using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m) 1445 then have "a' dvd b' ^ m * b'" 1446 by (simp add: m ac_simps) 1447 moreover have "coprime a' (b' ^ n)" 1448 using \<open>coprime a' b'\<close> by simp 1449 then have "a' dvd b'" 1450 using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast 1451 then have "a' * ?d dvd b' * ?d" 1452 by (rule mult_dvd_mono) simp 1453 with ab'(1,2) show "a dvd b" 1454 by simp 1455 next 1456 assume "a dvd b" 1457 with \<open>n > 0\<close> show "a ^ n dvd b ^ n" 1458 by (induction rule: nat_induct_non_zero) 1459 (simp_all add: mult_dvd_mono) 1460 qed 1461qed 1462 1463lemma coprime_crossproduct: 1464 fixes a b c d :: 'a 1465 assumes "coprime a d" and "coprime b c" 1466 shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow> 1467 normalize a = normalize b \<and> normalize c = normalize d" 1468 (is "?lhs \<longleftrightarrow> ?rhs") 1469proof 1470 assume ?rhs 1471 then show ?lhs by simp 1472next 1473 assume ?lhs 1474 from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d" 1475 by (auto intro: dvdI dest: sym) 1476 with \<open>coprime a d\<close> have "a dvd b" 1477 by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric]) 1478 from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c" 1479 by (auto intro: dvdI dest: sym) 1480 with \<open>coprime b c\<close> have "b dvd a" 1481 by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric]) 1482 from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b" 1483 by (auto intro: dvdI dest: sym simp add: mult.commute) 1484 with \<open>coprime b c\<close> have "c dvd d" 1485 by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric]) 1486 from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a" 1487 by (auto intro: dvdI dest: sym simp add: mult.commute) 1488 with \<open>coprime a d\<close> have "d dvd c" 1489 by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric]) 1490 from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b" 1491 by (rule associatedI) 1492 moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d" 1493 by (rule associatedI) 1494 ultimately show ?rhs .. 1495qed 1496 1497lemma gcd_mult_left_left_cancel: 1498 "gcd (c * a) b = gcd a b" if "coprime b c" 1499proof - 1500 have "coprime (gcd b (a * c)) c" 1501 by (rule coprimeI) (auto intro: that coprime_common_divisor) 1502 then have "gcd b (a * c) dvd a" 1503 using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a] 1504 by simp 1505 then show ?thesis 1506 by (auto intro: associated_eqI simp add: ac_simps) 1507qed 1508 1509lemma gcd_mult_left_right_cancel: 1510 "gcd (a * c) b = gcd a b" if "coprime b c" 1511 using that gcd_mult_left_left_cancel [of b c a] 1512 by (simp add: ac_simps) 1513 1514lemma gcd_mult_right_left_cancel: 1515 "gcd a (c * b) = gcd a b" if "coprime a c" 1516 using that gcd_mult_left_left_cancel [of a c b] 1517 by (simp add: ac_simps) 1518 1519lemma gcd_mult_right_right_cancel: 1520 "gcd a (b * c) = gcd a b" if "coprime a c" 1521 using that gcd_mult_right_left_cancel [of a c b] 1522 by (simp add: ac_simps) 1523 1524lemma gcd_exp_weak: 1525 "gcd (a ^ n) (b ^ n) = normalize (gcd a b ^ n)" 1526proof (cases "a = 0 \<and> b = 0 \<or> n = 0") 1527 case True 1528 then show ?thesis 1529 by (cases n) simp_all 1530next 1531 case False 1532 then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0" 1533 by (auto intro: div_gcd_coprime) 1534 then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 1535 by simp 1536 then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)" 1537 by simp 1538 then have "normalize (gcd a b ^ n) = normalize (gcd a b ^ n * \<dots>)" 1539 by simp 1540 also have "\<dots> = gcd (gcd a b ^ n * (a div gcd a b) ^ n) (gcd a b ^ n * (b div gcd a b) ^ n)" 1541 by (rule gcd_mult_left [symmetric]) 1542 also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n" 1543 by (simp add: ac_simps div_power dvd_power_same) 1544 also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n" 1545 by (simp add: ac_simps div_power dvd_power_same) 1546 finally show ?thesis by simp 1547qed 1548 1549lemma division_decomp: 1550 assumes "a dvd b * c" 1551 shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c" 1552proof (cases "gcd a b = 0") 1553 case True 1554 then have "a = 0 \<and> b = 0" 1555 by simp 1556 then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c" 1557 by simp 1558 then show ?thesis by blast 1559next 1560 case False 1561 let ?d = "gcd a b" 1562 from gcd_coprime_exists [OF False] 1563 obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'" 1564 by blast 1565 from ab'(1) have "a' dvd a" .. 1566 with assms have "a' dvd b * c" 1567 using dvd_trans [of a' a "b * c"] by simp 1568 from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c" 1569 by simp 1570 then have "?d * a' dvd ?d * (b' * c)" 1571 by (simp add: mult_ac) 1572 with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" 1573 by simp 1574 then have "a' dvd c" 1575 using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff) 1576 with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" 1577 by (simp add: ac_simps) 1578 then show ?thesis by blast 1579qed 1580 1581lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)" 1582 by (subst lcm_gcd) simp 1583 1584end 1585 1586context ring_gcd 1587begin 1588 1589lemma coprime_minus_left_iff [simp]: 1590 "coprime (- a) b \<longleftrightarrow> coprime a b" 1591 by (rule; rule coprimeI) (auto intro: coprime_common_divisor) 1592 1593lemma coprime_minus_right_iff [simp]: 1594 "coprime a (- b) \<longleftrightarrow> coprime a b" 1595 using coprime_minus_left_iff [of b a] by (simp add: ac_simps) 1596 1597lemma coprime_diff_one_left [simp]: "coprime (a - 1) a" 1598 using coprime_add_one_right [of "a - 1"] by simp 1599 1600lemma coprime_doff_one_right [simp]: "coprime a (a - 1)" 1601 using coprime_diff_one_left [of a] by (simp add: ac_simps) 1602 1603end 1604 1605context semiring_Gcd 1606begin 1607 1608lemma Lcm_coprime: 1609 assumes "finite A" 1610 and "A \<noteq> {}" 1611 and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b" 1612 shows "Lcm A = normalize (\<Prod>A)" 1613 using assms 1614proof (induct rule: finite_ne_induct) 1615 case singleton 1616 then show ?case by simp 1617next 1618 case (insert a A) 1619 have "Lcm (insert a A) = lcm a (Lcm A)" 1620 by simp 1621 also from insert have "Lcm A = normalize (\<Prod>A)" 1622 by blast 1623 also have "lcm a \<dots> = lcm a (\<Prod>A)" 1624 by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2) 1625 also from insert have "coprime a (\<Prod>A)" 1626 by (subst coprime_commute, intro prod_coprime_left) auto 1627 with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))" 1628 by (simp add: lcm_coprime) 1629 finally show ?case . 1630qed 1631 1632lemma Lcm_coprime': 1633 "card A \<noteq> 0 \<Longrightarrow> 1634 (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow> 1635 Lcm A = normalize (\<Prod>A)" 1636 by (rule Lcm_coprime) (simp_all add: card_eq_0_iff) 1637 1638end 1639 1640 1641subsection \<open>GCD and LCM for multiplicative normalisation functions\<close> 1642 1643class semiring_gcd_mult_normalize = semiring_gcd + normalization_semidom_multiplicative 1644begin 1645 1646lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)" 1647 by (simp add: gcd_mult_left normalize_mult mult.assoc [symmetric]) 1648 1649lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c" 1650 using mult_gcd_left [of c a b] by (simp add: ac_simps) 1651 1652lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)" 1653 by (subst gcd_mult_left) (simp_all add: normalize_mult) 1654 1655lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 1656proof- 1657 have "normalize k * gcd a b = gcd (k * a) (k * b)" 1658 by (simp add: gcd_mult_distrib') 1659 then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k" 1660 by simp 1661 then have "normalize k * unit_factor k * gcd a b = gcd (k * a) (k * b) * unit_factor k" 1662 by (simp only: ac_simps) 1663 then show ?thesis 1664 by simp 1665qed 1666 1667lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b" 1668 by (simp add: lcm_gcd normalize_mult dvd_normalize_div) 1669 1670lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b" 1671 using gcd_mult_lcm [of a b] by (simp add: ac_simps) 1672 1673lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)" 1674 by (simp add: lcm_mult_left mult.assoc [symmetric] normalize_mult) 1675 1676lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c" 1677 using mult_lcm_left [of c a b] by (simp add: ac_simps) 1678 1679lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)" 1680 by (simp add: lcm_gcd dvd_normalize_div normalize_mult) 1681 1682lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)" 1683 by (subst lcm_mult_left) (simp add: normalize_mult) 1684 1685lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k" 1686proof- 1687 have "normalize k * lcm a b = lcm (k * a) (k * b)" 1688 by (simp add: lcm_mult_distrib') 1689 then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k" 1690 by simp 1691 then have "normalize k * unit_factor k * lcm a b = lcm (k * a) (k * b) * unit_factor k" 1692 by (simp only: ac_simps) 1693 then show ?thesis 1694 by simp 1695qed 1696 1697lemma coprime_crossproduct': 1698 fixes a b c d 1699 assumes "b \<noteq> 0" 1700 assumes unit_factors: "unit_factor b = unit_factor d" 1701 assumes coprime: "coprime a b" "coprime c d" 1702 shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d" 1703proof safe 1704 assume eq: "a * d = b * c" 1705 hence "normalize a * normalize d = normalize c * normalize b" 1706 by (simp only: normalize_mult [symmetric] mult_ac) 1707 with coprime have "normalize b = normalize d" 1708 by (subst (asm) coprime_crossproduct) simp_all 1709 from this and unit_factors show "b = d" 1710 by (rule normalize_unit_factor_eqI) 1711 from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac) 1712 with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp 1713qed (simp_all add: mult_ac) 1714 1715lemma gcd_exp [simp]: 1716 "gcd (a ^ n) (b ^ n) = gcd a b ^ n" 1717 using gcd_exp_weak[of a n b] by (simp add: normalize_power) 1718 1719end 1720 1721 1722subsection \<open>GCD and LCM on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> 1723 1724instantiation nat :: gcd 1725begin 1726 1727fun gcd_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 1728 where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))" 1729 1730definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" 1731 where "lcm_nat x y = x * y div (gcd x y)" 1732 1733instance .. 1734 1735end 1736 1737instantiation int :: gcd 1738begin 1739 1740definition gcd_int :: "int \<Rightarrow> int \<Rightarrow> int" 1741 where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" 1742 1743definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int" 1744 where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))" 1745 1746instance .. 1747 1748end 1749 1750lemma gcd_int_int_eq [simp]: 1751 "gcd (int m) (int n) = int (gcd m n)" 1752 by (simp add: gcd_int_def) 1753 1754lemma gcd_nat_abs_left_eq [simp]: 1755 "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))" 1756 by (simp add: gcd_int_def) 1757 1758lemma gcd_nat_abs_right_eq [simp]: 1759 "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)" 1760 by (simp add: gcd_int_def) 1761 1762lemma abs_gcd_int [simp]: 1763 "\<bar>gcd x y\<bar> = gcd x y" 1764 for x y :: int 1765 by (simp only: gcd_int_def) 1766 1767lemma gcd_abs1_int [simp]: 1768 "gcd \<bar>x\<bar> y = gcd x y" 1769 for x y :: int 1770 by (simp only: gcd_int_def) simp 1771 1772lemma gcd_abs2_int [simp]: 1773 "gcd x \<bar>y\<bar> = gcd x y" 1774 for x y :: int 1775 by (simp only: gcd_int_def) simp 1776 1777lemma lcm_int_int_eq [simp]: 1778 "lcm (int m) (int n) = int (lcm m n)" 1779 by (simp add: lcm_int_def) 1780 1781lemma lcm_nat_abs_left_eq [simp]: 1782 "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))" 1783 by (simp add: lcm_int_def) 1784 1785lemma lcm_nat_abs_right_eq [simp]: 1786 "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)" 1787 by (simp add: lcm_int_def) 1788 1789lemma lcm_abs1_int [simp]: 1790 "lcm \<bar>x\<bar> y = lcm x y" 1791 for x y :: int 1792 by (simp only: lcm_int_def) simp 1793 1794lemma lcm_abs2_int [simp]: 1795 "lcm x \<bar>y\<bar> = lcm x y" 1796 for x y :: int 1797 by (simp only: lcm_int_def) simp 1798 1799lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j" 1800 for i j :: int 1801 by (simp only: lcm_int_def) 1802 1803lemma gcd_nat_induct [case_names base step]: 1804 fixes m n :: nat 1805 assumes "\<And>m. P m 0" 1806 and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n" 1807 shows "P m n" 1808proof (induction m n rule: gcd_nat.induct) 1809 case (1 x y) 1810 then show ?case 1811 using assms neq0_conv by blast 1812qed 1813 1814lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y" 1815 for x y :: int 1816 by (simp only: gcd_int_def) simp 1817 1818lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y" 1819 for x y :: int 1820 by (simp only: gcd_int_def) simp 1821 1822lemma gcd_cases_int: 1823 fixes x y :: int 1824 assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)" 1825 and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))" 1826 and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)" 1827 and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))" 1828 shows "P (gcd x y)" 1829 using assms by auto arith 1830 1831lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0" 1832 for x y :: int 1833 by (simp add: gcd_int_def) 1834 1835lemma lcm_neg1_int: "lcm (- x) y = lcm x y" 1836 for x y :: int 1837 by (simp only: lcm_int_def) simp 1838 1839lemma lcm_neg2_int: "lcm x (- y) = lcm x y" 1840 for x y :: int 1841 by (simp only: lcm_int_def) simp 1842 1843lemma lcm_cases_int: 1844 fixes x y :: int 1845 assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)" 1846 and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))" 1847 and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)" 1848 and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))" 1849 shows "P (lcm x y)" 1850 using assms by (auto simp: lcm_neg1_int lcm_neg2_int) arith 1851 1852lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0" 1853 for x y :: int 1854 by (simp only: lcm_int_def) 1855 1856lemma gcd_0_nat: "gcd x 0 = x" 1857 for x :: nat 1858 by simp 1859 1860lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>" 1861 for x :: int 1862 by (auto simp: gcd_int_def) 1863 1864lemma gcd_0_left_nat: "gcd 0 x = x" 1865 for x :: nat 1866 by simp 1867 1868lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>" 1869 for x :: int 1870 by (auto simp: gcd_int_def) 1871 1872lemma gcd_red_nat: "gcd x y = gcd y (x mod y)" 1873 for x y :: nat 1874 by (cases "y = 0") auto 1875 1876 1877text \<open>Weaker, but useful for the simplifier.\<close> 1878 1879lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)" 1880 for x y :: nat 1881 by simp 1882 1883lemma gcd_1_nat [simp]: "gcd m 1 = 1" 1884 for m :: nat 1885 by simp 1886 1887lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0" 1888 for m :: nat 1889 by simp 1890 1891lemma gcd_1_int [simp]: "gcd m 1 = 1" 1892 for m :: int 1893 by (simp add: gcd_int_def) 1894 1895lemma gcd_idem_nat: "gcd x x = x" 1896 for x :: nat 1897 by simp 1898 1899lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>" 1900 for x :: int 1901 by (auto simp: gcd_int_def) 1902 1903declare gcd_nat.simps [simp del] 1904 1905text \<open> 1906 \<^medskip> \<^term>\<open>gcd m n\<close> divides \<open>m\<close> and \<open>n\<close>. 1907 The conjunctions don't seem provable separately. 1908\<close> 1909 1910instance nat :: semiring_gcd 1911proof 1912 fix m n :: nat 1913 show "gcd m n dvd m" and "gcd m n dvd n" 1914 proof (induct m n rule: gcd_nat_induct) 1915 case (step m n) 1916 then have "gcd n (m mod n) dvd m" 1917 by (metis dvd_mod_imp_dvd) 1918 with step show "gcd m n dvd m" 1919 by (simp add: gcd_non_0_nat) 1920 qed (simp_all add: gcd_0_nat gcd_non_0_nat) 1921next 1922 fix m n k :: nat 1923 assume "k dvd m" and "k dvd n" 1924 then show "k dvd gcd m n" 1925 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat) 1926qed (simp_all add: lcm_nat_def) 1927 1928instance int :: ring_gcd 1929proof 1930 fix k l r :: int 1931 show [simp]: "gcd k l dvd k" "gcd k l dvd l" 1932 using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"] 1933 gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"] 1934 by simp_all 1935 show "lcm k l = normalize (k * l div gcd k l)" 1936 using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"] 1937 by (simp add: nat_eq_iff of_nat_div abs_mult abs_div) 1938 assume "r dvd k" "r dvd l" 1939 then show "r dvd gcd k l" 1940 using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"] 1941 by simp 1942qed simp 1943 1944lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a" 1945 for a b :: nat 1946 by (rule dvd_imp_le) auto 1947 1948lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b" 1949 for a b :: nat 1950 by (rule dvd_imp_le) auto 1951 1952lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a" 1953 for a b :: int 1954 by (rule zdvd_imp_le) auto 1955 1956lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b" 1957 for a b :: int 1958 by (rule zdvd_imp_le) auto 1959 1960lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0" 1961 for m n :: nat 1962 using gcd_eq_0_iff [of m n] by arith 1963 1964lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0" 1965 for m n :: int 1966 using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith 1967 1968lemma gcd_unique_nat: "d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 1969 for d a :: nat 1970 using gcd_unique by fastforce 1971 1972lemma gcd_unique_int: 1973 "d \<ge> 0 \<and> d dvd a \<and> d dvd b \<and> (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b" 1974 for d a :: int 1975 using zdvd_antisym_nonneg by auto 1976 1977interpretation gcd_nat: 1978 semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" 1979 by standard (auto simp: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans) 1980 1981lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>" 1982 for x y :: int 1983 by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int) 1984 1985lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>" 1986 for x y :: int 1987 by (metis gcd_proj1_if_dvd_int gcd.commute) 1988 1989 1990text \<open>\<^medskip> Multiplication laws.\<close> 1991 1992lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)" 1993 for k m n :: nat 1994 \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close> 1995 by (simp add: gcd_mult_left) 1996 1997lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)" 1998 for k m n :: int 1999 by (simp add: gcd_mult_left abs_mult) 2000 2001text \<open>\medskip Addition laws.\<close> 2002 2003(* TODO: add the other variations? *) 2004 2005lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n" 2006 for m n :: nat 2007 by (subst gcd_add1 [symmetric]) auto 2008 2009lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n" 2010 for m n :: nat 2011 by (metis gcd.commute gcd_add2 gcd_diff1_nat le_add_diff_inverse2) 2012 2013lemma gcd_non_0_int: 2014 fixes x y :: int 2015 assumes "y > 0" shows "gcd x y = gcd y (x mod y)" 2016proof (cases "x mod y = 0") 2017 case False 2018 then have neg: "x mod y = y - (- x) mod y" 2019 by (simp add: zmod_zminus1_eq_if) 2020 have xy: "0 \<le> x mod y" 2021 by (simp add: assms) 2022 show ?thesis 2023 proof (cases "x < 0") 2024 case True 2025 have "nat (- x mod y) \<le> nat y" 2026 by (simp add: assms dual_order.order_iff_strict) 2027 moreover have "gcd (nat (- x)) (nat y) = gcd (nat (- x mod y)) (nat y)" 2028 using True assms gcd_non_0_nat nat_mod_distrib by auto 2029 ultimately have "gcd (nat (- x)) (nat y) = gcd (nat y) (nat (x mod y))" 2030 using assms 2031 by (simp add: neg nat_diff_distrib') (metis gcd.commute gcd_diff2_nat) 2032 with assms \<open>0 \<le> x mod y\<close> show ?thesis 2033 by (simp add: True dual_order.order_iff_strict gcd_int_def) 2034 next 2035 case False 2036 with assms xy have "gcd (nat x) (nat y) = gcd (nat y) (nat x mod nat y)" 2037 using gcd_red_nat by blast 2038 with False assms show ?thesis 2039 by (simp add: gcd_int_def nat_mod_distrib) 2040 qed 2041qed (use assms in auto) 2042 2043lemma gcd_red_int: "gcd x y = gcd y (x mod y)" 2044 for x y :: int 2045proof (cases y "0::int" rule: linorder_cases) 2046 case less 2047 with gcd_non_0_int [of "- y" "- x"] show ?thesis 2048 by auto 2049next 2050 case greater 2051 with gcd_non_0_int [of y x] show ?thesis 2052 by auto 2053qed auto 2054 2055(* TODO: differences, and all variations of addition rules 2056 as simplification rules for nat and int *) 2057 2058(* TODO: add the three variations of these, and for ints? *) 2059 2060lemma finite_divisors_nat [simp]: (* FIXME move *) 2061 fixes m :: nat 2062 assumes "m > 0" 2063 shows "finite {d. d dvd m}" 2064proof- 2065 from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}" 2066 by (auto dest: dvd_imp_le) 2067 then show ?thesis 2068 using finite_Collect_le_nat by (rule finite_subset) 2069qed 2070 2071lemma finite_divisors_int [simp]: 2072 fixes i :: int 2073 assumes "i \<noteq> 0" 2074 shows "finite {d. d dvd i}" 2075proof - 2076 have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}" 2077 by (auto simp: abs_if) 2078 then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}" 2079 by simp 2080 from finite_subset [OF _ this] show ?thesis 2081 using assms by (simp add: dvd_imp_le_int subset_iff) 2082qed 2083 2084lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n" 2085 by (fastforce intro: antisym Max_le_iff[THEN iffD2] simp: dvd_imp_le) 2086 2087lemma Max_divisors_self_int [simp]: 2088 assumes "n \<noteq> 0" shows "Max {d::int. d dvd n} = \<bar>n\<bar>" 2089proof (rule antisym) 2090 show "Max {d. d dvd n} \<le> \<bar>n\<bar>" 2091 using assms by (auto intro: abs_le_D1 dvd_imp_le_int intro!: Max_le_iff [THEN iffD2]) 2092qed (simp add: assms) 2093 2094lemma gcd_is_Max_divisors_nat: 2095 fixes m n :: nat 2096 assumes "n > 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}" 2097proof (rule Max_eqI[THEN sym], simp_all) 2098 show "finite {d. d dvd m \<and> d dvd n}" 2099 by (simp add: \<open>n > 0\<close>) 2100 show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n" 2101 by (simp add: \<open>n > 0\<close> dvd_imp_le) 2102qed 2103 2104lemma gcd_is_Max_divisors_int: 2105 fixes m n :: int 2106 assumes "n \<noteq> 0" shows "gcd m n = Max {d. d dvd m \<and> d dvd n}" 2107proof (rule Max_eqI[THEN sym], simp_all) 2108 show "finite {d. d dvd m \<and> d dvd n}" 2109 by (simp add: \<open>n \<noteq> 0\<close>) 2110 show "\<And>y. y dvd m \<and> y dvd n \<Longrightarrow> y \<le> gcd m n" 2111 by (simp add: \<open>n \<noteq> 0\<close> zdvd_imp_le) 2112qed 2113 2114lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>" 2115 for k l :: int 2116 using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp 2117 2118lemma coprime_Suc_left_nat [simp]: 2119 "coprime (Suc n) n" 2120 using coprime_add_one_left [of n] by simp 2121 2122lemma coprime_Suc_right_nat [simp]: 2123 "coprime n (Suc n)" 2124 using coprime_Suc_left_nat [of n] by (simp add: ac_simps) 2125 2126lemma coprime_diff_one_left_nat [simp]: 2127 "coprime (n - 1) n" if "n > 0" for n :: nat 2128 using that coprime_Suc_right_nat [of "n - 1"] by simp 2129 2130lemma coprime_diff_one_right_nat [simp]: 2131 "coprime n (n - 1)" if "n > 0" for n :: nat 2132 using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps) 2133 2134lemma coprime_crossproduct_nat: 2135 fixes a b c d :: nat 2136 assumes "coprime a d" and "coprime b c" 2137 shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" 2138 using assms coprime_crossproduct [of a d b c] by simp 2139 2140lemma coprime_crossproduct_int: 2141 fixes a b c d :: int 2142 assumes "coprime a d" and "coprime b c" 2143 shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>" 2144 using assms coprime_crossproduct [of a d b c] by simp 2145 2146 2147subsection \<open>Bezout's theorem\<close> 2148 2149text \<open> 2150 Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem -- 2151 see the theorems that follow the definition. 2152\<close> 2153 2154fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int" 2155 where "bezw x y = 2156 (if y = 0 then (1, 0) 2157 else 2158 (snd (bezw y (x mod y)), 2159 fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))" 2160 2161lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" 2162 by simp 2163 2164lemma bezw_non_0: 2165 "y > 0 \<Longrightarrow> bezw x y = 2166 (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))" 2167 by simp 2168 2169declare bezw.simps [simp del] 2170 2171 2172lemma bezw_aux: "int (gcd x y) = fst (bezw x y) * int x + snd (bezw x y) * int y" 2173proof (induct x y rule: gcd_nat_induct) 2174 case (step m n) 2175 then have "fst (bezw m n) * int m + snd (bezw m n) * int n - int (gcd m n) 2176 = int m * snd (bezw n (m mod n)) - 2177 (int (m mod n) * snd (bezw n (m mod n)) + int n * (int (m div n) * snd (bezw n (m mod n))))" 2178 by (simp add: bezw_non_0 gcd_non_0_nat field_simps) 2179 also have "\<dots> = int m * snd (bezw n (m mod n)) - (int (m mod n) + int (n * (m div n))) * snd (bezw n (m mod n))" 2180 by (simp add: distrib_right) 2181 also have "\<dots> = 0" 2182 by (metis cancel_comm_monoid_add_class.diff_cancel mod_mult_div_eq of_nat_add) 2183 finally show ?case 2184 by simp 2185qed auto 2186 2187 2188lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y" 2189 for x y :: int 2190proof - 2191 have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int 2192 apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI) 2193 apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI) 2194 by (simp add: bezw_aux gcd_int_def) 2195 consider "x \<ge> 0" "y \<ge> 0" | "x \<ge> 0" "y \<le> 0" | "x \<le> 0" "y \<ge> 0" | "x \<le> 0" "y \<le> 0" 2196 using linear by blast 2197 then show ?thesis 2198 proof cases 2199 case 1 2200 then show ?thesis by (rule aux) 2201 next 2202 case 2 2203 then show ?thesis 2204 using aux [of x "-y"] 2205 by (metis gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le) 2206 next 2207 case 3 2208 then show ?thesis 2209 using aux [of "-x" y] 2210 by (metis gcd.commute gcd_neg2_int mult.commute mult_minus_right neg_0_le_iff_le) 2211 next 2212 case 4 2213 then show ?thesis 2214 using aux [of "-x" "-y"] 2215 by (metis diff_0 diff_ge_0_iff_ge gcd_neg1_int gcd_neg2_int mult.commute mult_minus_right) 2216 qed 2217qed 2218 2219 2220text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close> 2221 2222lemma Euclid_induct [case_names swap zero add]: 2223 fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool" 2224 assumes c: "\<And>a b. P a b \<longleftrightarrow> P b a" 2225 and z: "\<And>a. P a 0" 2226 and add: "\<And>a b. P a b \<longrightarrow> P a (a + b)" 2227 shows "P a b" 2228proof (induct "a + b" arbitrary: a b rule: less_induct) 2229 case less 2230 consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b" 2231 by arith 2232 show ?case 2233 proof (cases a b rule: linorder_cases) 2234 case equal 2235 with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp 2236 next 2237 case lt: less 2238 then consider "a = 0" | "a + b - a < a + b" by arith 2239 then show ?thesis 2240 proof cases 2241 case 1 2242 with z c show ?thesis by blast 2243 next 2244 case 2 2245 also have *: "a + b - a = a + (b - a)" using lt by arith 2246 finally have "a + (b - a) < a + b" . 2247 then have "P a (a + (b - a))" by (rule add [rule_format, OF less]) 2248 then show ?thesis by (simp add: *[symmetric]) 2249 qed 2250 next 2251 case gt: greater 2252 then consider "b = 0" | "b + a - b < a + b" by arith 2253 then show ?thesis 2254 proof cases 2255 case 1 2256 with z c show ?thesis by blast 2257 next 2258 case 2 2259 also have *: "b + a - b = b + (a - b)" using gt by arith 2260 finally have "b + (a - b) < a + b" . 2261 then have "P b (b + (a - b))" by (rule add [rule_format, OF less]) 2262 then have "P b a" by (simp add: *[symmetric]) 2263 with c show ?thesis by blast 2264 qed 2265 qed 2266qed 2267 2268lemma bezout_lemma_nat: 2269 fixes d::nat 2270 shows "\<lbrakk>d dvd a; d dvd b; a * x = b * y + d \<or> b * x = a * y + d\<rbrakk> 2271 \<Longrightarrow> \<exists>x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)" 2272 apply auto 2273 apply (metis add_mult_distrib2 left_add_mult_distrib) 2274 apply (rule_tac x=x in exI) 2275 by (metis add_mult_distrib2 mult.commute add.assoc) 2276 2277lemma bezout_add_nat: 2278 "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x = b * y + d \<or> b * x = a * y + d)" 2279proof (induct a b rule: Euclid_induct) 2280 case (swap a b) 2281 then show ?case 2282 by blast 2283next 2284 case (zero a) 2285 then show ?case 2286 by fastforce 2287next 2288 case (add a b) 2289 then show ?case 2290 by (meson bezout_lemma_nat) 2291qed 2292 2293lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and> (a * x - b * y = d \<or> b * x - a * y = d)" 2294 using bezout_add_nat[of a b] by (metis add_diff_cancel_left') 2295 2296lemma bezout_add_strong_nat: 2297 fixes a b :: nat 2298 assumes a: "a \<noteq> 0" 2299 shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d" 2300proof - 2301 consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d" 2302 | d x y where "d dvd a" "d dvd b" "b * x = a * y + d" 2303 using bezout_add_nat [of a b] by blast 2304 then show ?thesis 2305 proof cases 2306 case 1 2307 then show ?thesis by blast 2308 next 2309 case H: 2 2310 show ?thesis 2311 proof (cases "b = 0") 2312 case True 2313 with H show ?thesis by simp 2314 next 2315 case False 2316 then have bp: "b > 0" by simp 2317 with dvd_imp_le [OF H(2)] consider "d = b" | "d < b" 2318 by atomize_elim auto 2319 then show ?thesis 2320 proof cases 2321 case 1 2322 with a H show ?thesis 2323 by (metis Suc_pred add.commute mult.commute mult_Suc_right neq0_conv) 2324 next 2325 case 2 2326 show ?thesis 2327 proof (cases "x = 0") 2328 case True 2329 with a H show ?thesis by simp 2330 next 2331 case x0: False 2332 then have xp: "x > 0" by simp 2333 from \<open>d < b\<close> have "d \<le> b - 1" by simp 2334 then have "d * b \<le> b * (b - 1)" by simp 2335 with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"] 2336 have dble: "d * b \<le> x * b * (b - 1)" using bp by simp 2337 from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)" 2338 by simp 2339 then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x" 2340 by (simp only: mult.assoc distrib_left) 2341 then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)" 2342 by algebra 2343 then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b" 2344 using bp by simp 2345 then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)" 2346 by (simp only: diff_add_assoc[OF dble, of d, symmetric]) 2347 then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d" 2348 by (simp only: diff_mult_distrib2 ac_simps) 2349 with H(1,2) show ?thesis 2350 by blast 2351 qed 2352 qed 2353 qed 2354 qed 2355qed 2356 2357lemma bezout_nat: 2358 fixes a :: nat 2359 assumes a: "a \<noteq> 0" 2360 shows "\<exists>x y. a * x = b * y + gcd a b" 2361proof - 2362 obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d" 2363 using bezout_add_strong_nat [OF a, of b] by blast 2364 from d have "d dvd gcd a b" 2365 by simp 2366 then obtain k where k: "gcd a b = d * k" 2367 unfolding dvd_def by blast 2368 from eq have "a * x * k = (b * y + d) * k" 2369 by auto 2370 then have "a * (x * k) = b * (y * k) + gcd a b" 2371 by (algebra add: k) 2372 then show ?thesis 2373 by blast 2374qed 2375 2376 2377subsection \<open>LCM properties on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> 2378 2379lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b" 2380 for a b :: int 2381 by (simp add: abs_mult lcm_gcd abs_div) 2382 2383lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n" 2384 for m n :: nat 2385 by (simp add: lcm_gcd) 2386 2387lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n" 2388 for m n :: int 2389 by (simp add: lcm_gcd abs_div abs_mult) 2390 2391lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0" 2392 for m n :: nat 2393 using lcm_eq_0_iff [of m n] by auto 2394 2395lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0" 2396 for m n :: int 2397 by (simp add: less_le lcm_eq_0_iff) 2398 2399lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0" (* FIXME move *) 2400 for m n :: nat 2401 by auto 2402 2403lemma lcm_unique_nat: 2404 "a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" 2405 for a b d :: nat 2406 by (auto intro: dvd_antisym lcm_least) 2407 2408lemma lcm_unique_int: 2409 "d \<ge> 0 \<and> a dvd d \<and> b dvd d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" 2410 for a b d :: int 2411 using lcm_least zdvd_antisym_nonneg by auto 2412 2413lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y" 2414 for x y :: nat 2415 by (simp add: lcm_proj2_if_dvd) 2416 2417lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>" 2418 for x y :: int 2419 by (simp add: lcm_proj2_if_dvd) 2420 2421lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y" 2422 for x y :: nat 2423 by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat) 2424 2425lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>" 2426 for x y :: int 2427 by (subst lcm.commute) (erule lcm_proj2_if_dvd_int) 2428 2429lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m" 2430 for m n :: nat 2431 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat) 2432 2433lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n" 2434 for m n :: nat 2435 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat) 2436 2437lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m" 2438 for m n :: int 2439 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int) 2440 2441lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n" 2442 for m n :: int 2443 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int) 2444 2445lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0" 2446 for m n :: nat 2447 using lcm_eq_1_iff [of m n] by simp 2448 2449lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)" 2450 for m n :: int 2451 by auto 2452 2453 2454subsection \<open>The complete divisibility lattice on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> 2455 2456text \<open> 2457 Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>). 2458 \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice. 2459\<close> 2460 2461instantiation nat :: semiring_Gcd 2462begin 2463 2464interpretation semilattice_neutr_set lcm "1::nat" 2465 by standard simp_all 2466 2467definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set" 2468 2469lemma Lcm_nat_empty: "Lcm {} = (1::nat)" 2470 by (simp add: Lcm_nat_def del: One_nat_def) 2471 2472lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat 2473 by (cases "finite M") (auto simp: Lcm_nat_def simp del: One_nat_def) 2474 2475lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set" 2476 by (simp add: Lcm_nat_def) 2477 2478lemma dvd_Lcm_nat [simp]: 2479 fixes M :: "nat set" 2480 assumes "m \<in> M" 2481 shows "m dvd Lcm M" 2482proof - 2483 from assms have "insert m M = M" 2484 by auto 2485 moreover have "m dvd Lcm (insert m M)" 2486 by (simp add: Lcm_nat_insert) 2487 ultimately show ?thesis 2488 by simp 2489qed 2490 2491lemma Lcm_dvd_nat [simp]: 2492 fixes M :: "nat set" 2493 assumes "\<forall>m\<in>M. m dvd n" 2494 shows "Lcm M dvd n" 2495proof (cases "n > 0") 2496 case False 2497 then show ?thesis by simp 2498next 2499 case True 2500 then have "finite {d. d dvd n}" 2501 by (rule finite_divisors_nat) 2502 moreover have "M \<subseteq> {d. d dvd n}" 2503 using assms by fast 2504 ultimately have "finite M" 2505 by (rule rev_finite_subset) 2506 then show ?thesis 2507 using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert) 2508qed 2509 2510definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set" 2511 2512instance 2513proof 2514 fix N :: "nat set" 2515 fix n :: nat 2516 show "Gcd N dvd n" if "n \<in> N" 2517 using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def) 2518 show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" 2519 using that by (induct N rule: infinite_finite_induct) (auto simp: Gcd_nat_def) 2520 show "n dvd Lcm N" if "n \<in> N" 2521 using that by (induct N rule: infinite_finite_induct) auto 2522 show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" 2523 using that by (induct N rule: infinite_finite_induct) auto 2524 show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N" 2525 by simp_all 2526qed 2527 2528end 2529 2530lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1" 2531 for N :: "nat set" 2532 by (rule Gcd_eq_1_I) auto 2533 2534instance nat :: semiring_gcd_mult_normalize 2535 by intro_classes (auto simp: unit_factor_nat_def) 2536 2537 2538text \<open>Alternative characterizations of Gcd:\<close> 2539 2540lemma Gcd_eq_Max: 2541 fixes M :: "nat set" 2542 assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M" 2543 shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})" 2544proof (rule antisym) 2545 from assms obtain m where "m \<in> M" and "m > 0" 2546 by auto 2547 from \<open>m > 0\<close> have "finite {d. d dvd m}" 2548 by (blast intro: finite_divisors_nat) 2549 with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})" 2550 by blast 2551 from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})" 2552 by (auto intro: Max_ge Gcd_dvd) 2553 from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M" 2554 proof (rule Max.boundedI, simp_all) 2555 show "(\<Inter>m\<in>M. {d. d dvd m}) \<noteq> {}" 2556 by auto 2557 show "\<And>a. \<forall>x\<in>M. a dvd x \<Longrightarrow> a \<le> Gcd M" 2558 by (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat) 2559 qed 2560qed 2561 2562lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})" 2563 for M :: "nat set" 2564proof (induct pred: finite) 2565 case (insert x M) 2566 then show ?case 2567 by (simp add: insert_Diff_if) 2568qed auto 2569 2570lemma Lcm_in_lcm_closed_set_nat: 2571 fixes M :: "nat set" 2572 assumes "finite M" "M \<noteq> {}" "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M" 2573 shows "Lcm M \<in> M" 2574 using assms 2575proof (induction M rule: finite_linorder_min_induct) 2576 case (insert x M) 2577 then have "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> lcm m n \<in> M" 2578 by (metis dvd_lcm1 gr0I insert_iff lcm_pos_nat nat_dvd_not_less) 2579 with insert show ?case 2580 by simp (metis Lcm_nat_empty One_nat_def dvd_1_left dvd_lcm2) 2581qed auto 2582 2583lemma Lcm_eq_Max_nat: 2584 fixes M :: "nat set" 2585 assumes M: "finite M" "M \<noteq> {}" "0 \<notin> M" and lcm: "\<And>m n. \<lbrakk>m \<in> M; n \<in> M\<rbrakk> \<Longrightarrow> lcm m n \<in> M" 2586 shows "Lcm M = Max M" 2587proof (rule antisym) 2588 show "Lcm M \<le> Max M" 2589 by (simp add: Lcm_in_lcm_closed_set_nat \<open>finite M\<close> \<open>M \<noteq> {}\<close> lcm) 2590 show "Max M \<le> Lcm M" 2591 by (meson Lcm_0_iff Max_in M dvd_Lcm dvd_imp_le le_0_eq not_le) 2592qed 2593 2594lemma mult_inj_if_coprime_nat: 2595 "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> (\<And>a b. \<lbrakk>a\<in>A; b\<in>B\<rbrakk> \<Longrightarrow> coprime (f a) (g b)) \<Longrightarrow> 2596 inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)" 2597 for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat" 2598 by (auto simp: inj_on_def coprime_crossproduct_nat simp del: One_nat_def) 2599 2600 2601subsubsection \<open>Setwise GCD and LCM for integers\<close> 2602 2603instantiation int :: Gcd 2604begin 2605 2606definition Gcd_int :: "int set \<Rightarrow> int" 2607 where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)" 2608 2609definition Lcm_int :: "int set \<Rightarrow> int" 2610 where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)" 2611 2612instance .. 2613 2614end 2615 2616lemma Gcd_int_eq [simp]: 2617 "(GCD n\<in>N. int n) = int (Gcd N)" 2618 by (simp add: Gcd_int_def image_image) 2619 2620lemma Gcd_nat_abs_eq [simp]: 2621 "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)" 2622 by (simp add: Gcd_int_def) 2623 2624lemma abs_Gcd_eq [simp]: 2625 "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set" 2626 by (simp only: Gcd_int_def) 2627 2628lemma Gcd_int_greater_eq_0 [simp]: 2629 "Gcd K \<ge> 0" 2630 for K :: "int set" 2631 using abs_ge_zero [of "Gcd K"] by simp 2632 2633lemma Gcd_abs_eq [simp]: 2634 "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K" 2635 for K :: "int set" 2636 by (simp only: Gcd_int_def image_image) simp 2637 2638lemma Lcm_int_eq [simp]: 2639 "(LCM n\<in>N. int n) = int (Lcm N)" 2640 by (simp add: Lcm_int_def image_image) 2641 2642lemma Lcm_nat_abs_eq [simp]: 2643 "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)" 2644 by (simp add: Lcm_int_def) 2645 2646lemma abs_Lcm_eq [simp]: 2647 "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set" 2648 by (simp only: Lcm_int_def) 2649 2650lemma Lcm_int_greater_eq_0 [simp]: 2651 "Lcm K \<ge> 0" 2652 for K :: "int set" 2653 using abs_ge_zero [of "Lcm K"] by simp 2654 2655lemma Lcm_abs_eq [simp]: 2656 "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K" 2657 for K :: "int set" 2658 by (simp only: Lcm_int_def image_image) simp 2659 2660instance int :: semiring_Gcd 2661proof 2662 fix K :: "int set" and k :: int 2663 show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K" 2664 using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"] 2665 dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"] 2666 by (simp_all add: comp_def) 2667 show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l" 2668 proof - 2669 have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)" 2670 by (rule Gcd_greatest) (use that in auto) 2671 then show ?thesis by simp 2672 qed 2673 show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k" 2674 proof - 2675 have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>" 2676 by (rule Lcm_least) (use that in auto) 2677 then show ?thesis by simp 2678 qed 2679qed (simp_all add: sgn_mult) 2680 2681instance int :: semiring_gcd_mult_normalize 2682 by intro_classes (auto simp: sgn_mult) 2683 2684 2685subsection \<open>GCD and LCM on \<^typ>\<open>integer\<close>\<close> 2686 2687instantiation integer :: gcd 2688begin 2689 2690context 2691 includes integer.lifting 2692begin 2693 2694lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd . 2695 2696lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm . 2697 2698end 2699 2700instance .. 2701 2702end 2703 2704lifting_update integer.lifting 2705lifting_forget integer.lifting 2706 2707context 2708 includes integer.lifting 2709begin 2710 2711lemma gcd_code_integer [code]: "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>" 2712 by transfer (fact gcd_code_int) 2713 2714lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b" 2715 for a b :: integer 2716 by transfer (fact lcm_altdef_int) 2717 2718end 2719 2720code_printing 2721 constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup> 2722 (OCaml) "!(fun k l -> if Z.equal k Z.zero then/ Z.abs l else if Z.equal/ l Z.zero then Z.abs k else Z.gcd k l)" 2723 and (Haskell) "Prelude.gcd" 2724 and (Scala) "_.gcd'((_)')" 2725 \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close> 2726 2727text \<open>Some code equations\<close> 2728 2729lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat] 2730lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat] 2731lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int] 2732lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int] 2733 2734text \<open>Fact aliases.\<close> 2735 2736lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" 2737 for m n :: nat 2738 by (fact lcm_eq_0_iff) 2739 2740lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" 2741 for m n :: int 2742 by (fact lcm_eq_0_iff) 2743 2744lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n" 2745 for k m n :: nat 2746 by (fact dvd_lcmI1) 2747 2748lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n" 2749 for k m n :: nat 2750 by (fact dvd_lcmI2) 2751 2752lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n" 2753 for i m n :: int 2754 by (fact dvd_lcmI1) 2755 2756lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n" 2757 for i m n :: int 2758 by (fact dvd_lcmI2) 2759 2760lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat] 2761lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int] 2762lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat] 2763lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int] 2764 2765lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M" 2766 for M :: "int set" 2767 by (fact dvd_Lcm) 2768 2769lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x" 2770 by (fact gcd_neg1_int) 2771 2772lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)" 2773 by (fact gcd_neg2_int) 2774 2775lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x" 2776 for x y :: nat 2777 by (fact gcd_nat.absorb1) 2778 2779lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y" 2780 for x y :: nat 2781 by (fact gcd_nat.absorb2) 2782 2783lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat] 2784lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat] 2785lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int] 2786 2787end 2788