src/HOL/GCD.thy
 author paulson Tue Apr 25 16:39:54 2017 +0100 (2017-04-25) changeset 65578 e4997c181cce parent 65555 85ed070017b7 child 65811 2653f1cd8775 permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
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
9 This file deals with the functions gcd and lcm.  Definitions and
10 lemmas are proved uniformly for the natural numbers and integers.
12 This file combines and revises a number of prior developments.
14 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
15 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
16 gcd, lcm, and prime for the natural numbers.
18 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
19 extended gcd, lcm, primes to the integers. Amine Chaieb provided
20 another extension of the notions to the integers, and added a number
21 of results to "Primes" and "GCD". IntPrimes also defined and developed
22 the congruence relations on the integers. The notion was extended to
23 the natural numbers by Chaieb.
25 Jeremy Avigad combined all of these, made everything uniform for the
26 natural numbers and the integers, and added a number of new theorems.
28 Tobias Nipkow cleaned up a lot.
29 *)
31 section \<open>Greatest common divisor and least common multiple\<close>
33 theory GCD
34   imports Groups_List
35 begin
37 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
39 locale 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>"
49 begin
51 lemma left_idem [simp]:
52   "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
53   using assoc [of a a b, symmetric] by simp
55 lemma right_idem [simp]:
56   "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
57   using left_idem [of b a] by (simp add: ac_simps)
59 lemma comp_fun_idem: "comp_fun_idem f"
60   by standard (simp_all add: fun_eq_iff ac_simps)
62 interpretation comp_fun_idem f
63   by (fact comp_fun_idem)
65 lemma top_right_normalize [simp]:
66   "a \<^bold>* \<^bold>\<top> = normalize a"
67   using top_left_normalize [of a] by (simp add: ac_simps)
69 lemma bottom_right_bottom [simp]:
70   "a \<^bold>* \<^bold>\<bottom> = \<^bold>\<bottom>"
71   using bottom_left_bottom [of a] by (simp add: ac_simps)
73 lemma 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)
77 end
79 locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
80 begin
82 interpretation comp_fun_idem f
83   by (fact comp_fun_idem)
85 definition F :: "'a set \<Rightarrow> 'a"
86 where
87   eq_fold: "F A = (if finite A then Finite_Set.fold f \<^bold>\<top> A else \<^bold>\<bottom>)"
89 lemma infinite [simp]:
90   "infinite A \<Longrightarrow> F A = \<^bold>\<bottom>"
91   by (simp add: eq_fold)
93 lemma set_eq_fold [code]:
94   "F (set xs) = fold f xs \<^bold>\<top>"
95   by (simp add: eq_fold fold_set_fold)
97 lemma empty [simp]:
98   "F {} = \<^bold>\<top>"
99   by (simp add: eq_fold)
101 lemma insert [simp]:
102   "F (insert a A) = a \<^bold>* F A"
103   by (cases "finite A") (simp_all add: eq_fold)
105 lemma normalize [simp]:
106   "normalize (F A) = F A"
107   by (induct A rule: infinite_finite_induct) simp_all
109 lemma 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 add: left_commute [of a])
115 lemma 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)
120 lemma remove:
121   assumes "a \<in> A"
122   shows "F A = a \<^bold>* F (A - {a})"
123 proof -
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
127 qed
129 lemma insert_remove:
130   "F (insert a A) = a \<^bold>* F (A - {a})"
131   by (cases "a \<in> A") (simp_all add: insert_absorb remove)
133 lemma 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)
138 end
140 subsection \<open>Abstract GCD and LCM\<close>
142 class gcd = zero + one + dvd +
143   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
144     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
145 begin
147 abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
148   where "coprime x y \<equiv> gcd x y = 1"
150 end
152 class Gcd = gcd +
153   fixes Gcd :: "'a set \<Rightarrow> 'a"
154     and Lcm :: "'a set \<Rightarrow> 'a"
155 begin
157 abbreviation GREATEST_COMMON_DIVISOR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
158   where "GREATEST_COMMON_DIVISOR A f \<equiv> Gcd (f ` A)"
160 abbreviation LEAST_COMMON_MULTIPLE :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
161   where "LEAST_COMMON_MULTIPLE A f \<equiv> Lcm (f ` A)"
163 end
165 syntax
166   "_GCD1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3GCD _./ _)" [0, 10] 10)
167   "_GCD"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
168   "_LCM1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3LCM _./ _)" [0, 10] 10)
169   "_LCM"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
170 translations
171   "GCD x y. B"   \<rightleftharpoons> "GCD x. GCD y. B"
172   "GCD x. B"     \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR CONST UNIV (\<lambda>x. B)"
173   "GCD x. B"     \<rightleftharpoons> "GCD x \<in> CONST UNIV. B"
174   "GCD x\<in>A. B"   \<rightleftharpoons> "CONST GREATEST_COMMON_DIVISOR A (\<lambda>x. B)"
175   "LCM x y. B"   \<rightleftharpoons> "LCM x. LCM y. B"
176   "LCM x. B"     \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE CONST UNIV (\<lambda>x. B)"
177   "LCM x. B"     \<rightleftharpoons> "LCM x \<in> CONST UNIV. B"
178   "LCM x\<in>A. B"   \<rightleftharpoons> "CONST LEAST_COMMON_MULTIPLE A (\<lambda>x. B)"
180 print_translation \<open>
181   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax GREATEST_COMMON_DIVISOR} @{syntax_const "_GCD"},
182     Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax LEAST_COMMON_MULTIPLE} @{syntax_const "_LCM"}]
183 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
185 class semiring_gcd = normalization_semidom + gcd +
186   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
187     and gcd_dvd2 [iff]: "gcd a b dvd b"
188     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
189     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
190     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
191 begin
193 lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
194   by (blast intro!: gcd_greatest intro: dvd_trans)
196 lemma gcd_dvdI1: "a dvd c \<Longrightarrow> gcd a b dvd c"
197   by (rule dvd_trans) (rule gcd_dvd1)
199 lemma gcd_dvdI2: "b dvd c \<Longrightarrow> gcd a b dvd c"
200   by (rule dvd_trans) (rule gcd_dvd2)
202 lemma dvd_gcdD1: "a dvd gcd b c \<Longrightarrow> a dvd b"
203   using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
205 lemma dvd_gcdD2: "a dvd gcd b c \<Longrightarrow> a dvd c"
206   using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
208 lemma gcd_0_left [simp]: "gcd 0 a = normalize a"
209   by (rule associated_eqI) simp_all
211 lemma gcd_0_right [simp]: "gcd a 0 = normalize a"
212   by (rule associated_eqI) simp_all
214 lemma gcd_eq_0_iff [simp]: "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
215   (is "?P \<longleftrightarrow> ?Q")
216 proof
217   assume ?P
218   then have "0 dvd gcd a b"
219     by simp
220   then have "0 dvd a" and "0 dvd b"
221     by (blast intro: dvd_trans)+
222   then show ?Q
223     by simp
224 next
225   assume ?Q
226   then show ?P
227     by simp
228 qed
230 lemma unit_factor_gcd: "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
231 proof (cases "gcd a b = 0")
232   case True
233   then show ?thesis by simp
234 next
235   case False
236   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
237     by (rule unit_factor_mult_normalize)
238   then have "unit_factor (gcd a b) * gcd a b = gcd a b"
239     by simp
240   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
241     by simp
242   with False show ?thesis
243     by simp
244 qed
246 lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
247   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
249 sublocale gcd: abel_semigroup gcd
250 proof
251   fix a b c
252   show "gcd a b = gcd b a"
253     by (rule associated_eqI) simp_all
254   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
255     by (rule dvd_trans) simp
256   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
257     by (rule dvd_trans) simp
258   ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
259     by (auto intro!: gcd_greatest)
260   from gcd_dvd2 have "gcd a (gcd b c) dvd b"
261     by (rule dvd_trans) simp
262   moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
263     by (rule dvd_trans) simp
264   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
265     by (auto intro!: gcd_greatest)
266   from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
267     by (rule associated_eqI) simp_all
268 qed
270 sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
271 proof
272   show "gcd a a = normalize a" for a
273   proof -
274     have "a dvd gcd a a"
275       by (rule gcd_greatest) simp_all
276     then show ?thesis
277       by (auto intro: associated_eqI)
278   qed
279   show "gcd (normalize a) b = gcd a b" for a b
280     using gcd_dvd1 [of "normalize a" b]
281     by (auto intro: associated_eqI)
282   show "coprime 1 a" for a
283     by (rule associated_eqI) simp_all
284 qed simp_all
286 lemma gcd_self: "gcd a a = normalize a"
287   by (fact gcd.idem_normalize)
289 lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
290   by (fact gcd.left_idem)
292 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
293   by (fact gcd.right_idem)
295 lemma coprime_1_left: "coprime 1 a"
296   by (fact gcd.bottom_left_bottom)
298 lemma coprime_1_right: "coprime a 1"
299   by (fact gcd.bottom_right_bottom)
301 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
302 proof (cases "c = 0")
303   case True
304   then show ?thesis by simp
305 next
306   case False
307   then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
308     by (auto intro: gcd_greatest)
309   moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
310     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
311   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
312     by (auto intro: associated_eqI)
313   then show ?thesis
314     by (simp add: normalize_mult)
315 qed
317 lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
318   using gcd_mult_left [of c a b] by (simp add: ac_simps)
320 lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
321   by (simp add: gcd_mult_left mult.assoc [symmetric])
323 lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
324   using mult_gcd_left [of c a b] by (simp add: ac_simps)
326 lemma dvd_lcm1 [iff]: "a dvd lcm a b"
327 proof -
328   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
329     by (simp add: lcm_gcd normalize_mult div_mult_swap)
330   then show ?thesis
331     by (simp add: lcm_gcd)
332 qed
334 lemma dvd_lcm2 [iff]: "b dvd lcm a b"
335 proof -
336   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
337     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
338   then show ?thesis
339     by (simp add: lcm_gcd)
340 qed
342 lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
343   by (rule dvd_trans) (assumption, blast)
345 lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
346   by (rule dvd_trans) (assumption, blast)
348 lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
349   using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
351 lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
352   using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
354 lemma lcm_least:
355   assumes "a dvd c" and "b dvd c"
356   shows "lcm a b dvd c"
357 proof (cases "c = 0")
358   case True
359   then show ?thesis by simp
360 next
361   case False
362   then have *: "is_unit (unit_factor c)"
363     by simp
364   show ?thesis
365   proof (cases "gcd a b = 0")
366     case True
367     with assms show ?thesis by simp
368   next
369     case False
370     then have "a \<noteq> 0 \<or> b \<noteq> 0"
371       by simp
372     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
373       by (simp_all add: mult_dvd_mono)
374     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
375       by (auto intro: gcd_greatest simp add: ac_simps)
376     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
377       using * by (simp add: dvd_mult_unit_iff)
378     then have "normalize (a * b) dvd gcd a b * c"
379       by (simp add: mult_gcd_right [of a b c])
380     then have "normalize (a * b) div gcd a b dvd c"
381       using False by (simp add: div_dvd_iff_mult ac_simps)
382     then show ?thesis
383       by (simp add: lcm_gcd)
384   qed
385 qed
387 lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
388   by (blast intro!: lcm_least intro: dvd_trans)
390 lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
391   by (simp add: lcm_gcd dvd_normalize_div)
393 lemma lcm_0_left [simp]: "lcm 0 a = 0"
394   by (simp add: lcm_gcd)
396 lemma lcm_0_right [simp]: "lcm a 0 = 0"
397   by (simp add: lcm_gcd)
399 lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
400   (is "?P \<longleftrightarrow> ?Q")
401 proof
402   assume ?P
403   then have "0 dvd lcm a b"
404     by simp
405   then have "0 dvd normalize (a * b) div gcd a b"
406     by (simp add: lcm_gcd)
407   then have "0 * gcd a b dvd normalize (a * b)"
408     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
409   then have "normalize (a * b) = 0"
410     by simp
411   then show ?Q
412     by simp
413 next
414   assume ?Q
415   then show ?P
416     by auto
417 qed
419 lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
420   by (auto intro: associated_eqI)
422 lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
423   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
425 sublocale lcm: abel_semigroup lcm
426 proof
427   fix a b c
428   show "lcm a b = lcm b a"
429     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
430   have "lcm (lcm a b) c dvd lcm a (lcm b c)"
431     and "lcm a (lcm b c) dvd lcm (lcm a b) c"
432     by (auto intro: lcm_least
433       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
434       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
435       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
436       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
437   then show "lcm (lcm a b) c = lcm a (lcm b c)"
438     by (rule associated_eqI) simp_all
439 qed
441 sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
442 proof
443   show "lcm a a = normalize a" for a
444   proof -
445     have "lcm a a dvd a"
446       by (rule lcm_least) simp_all
447     then show ?thesis
448       by (auto intro: associated_eqI)
449   qed
450   show "lcm (normalize a) b = lcm a b" for a b
451     using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
452     by (auto intro: associated_eqI)
453   show "lcm 1 a = normalize a" for a
454     by (rule associated_eqI) simp_all
455 qed simp_all
457 lemma lcm_self: "lcm a a = normalize a"
458   by (fact lcm.idem_normalize)
460 lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
461   by (fact lcm.left_idem)
463 lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
464   by (fact lcm.right_idem)
466 lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
467   by (simp add: lcm_gcd normalize_mult)
469 lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
470   using gcd_mult_lcm [of a b] by (simp add: ac_simps)
472 lemma gcd_lcm:
473   assumes "a \<noteq> 0" and "b \<noteq> 0"
474   shows "gcd a b = normalize (a * b) div lcm a b"
475 proof -
476   from assms have "lcm a b \<noteq> 0"
477     by (simp add: lcm_eq_0_iff)
478   have "gcd a b * lcm a b = normalize a * normalize b"
479     by simp
480   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
481     by (simp_all add: normalize_mult)
482   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
483     using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
484 qed
486 lemma lcm_1_left: "lcm 1 a = normalize a"
487   by (fact lcm.top_left_normalize)
489 lemma lcm_1_right: "lcm a 1 = normalize a"
490   by (fact lcm.top_right_normalize)
492 lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
493   by (cases "c = 0")
494     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
495       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
497 lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
498   using lcm_mult_left [of c a b] by (simp add: ac_simps)
500 lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
501   by (simp add: lcm_mult_left mult.assoc [symmetric])
503 lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
504   using mult_lcm_left [of c a b] by (simp add: ac_simps)
506 lemma gcdI:
507   assumes "c dvd a" and "c dvd b"
508     and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
509     and "normalize c = c"
510   shows "c = gcd a b"
511   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
513 lemma gcd_unique:
514   "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"
515   by rule (auto intro: gcdI simp: gcd_greatest)
517 lemma gcd_dvd_prod: "gcd a b dvd k * b"
518   using mult_dvd_mono [of 1] by auto
520 lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b"
521   by (rule gcdI [symmetric]) simp_all
523 lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a"
524   by (rule gcdI [symmetric]) simp_all
526 lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
527 proof
528   assume *: "gcd m n = normalize m"
529   show "m dvd n"
530   proof (cases "m = 0")
531     case True
532     with * show ?thesis by simp
533   next
534     case [simp]: False
535     from * have **: "m = gcd m n * unit_factor m"
536       by (simp add: unit_eq_div2)
537     show ?thesis
538       by (subst **) (simp add: mult_unit_dvd_iff)
539   qed
540 next
541   assume "m dvd n"
542   then show "gcd m n = normalize m"
543     by (rule gcd_proj1_if_dvd)
544 qed
546 lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
547   using gcd_proj1_iff [of n m] by (simp add: ac_simps)
549 lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
550   by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
552 lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
553 proof-
554   have "normalize k * gcd a b = gcd (k * a) (k * b)"
555     by (simp add: gcd_mult_distrib')
556   then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
557     by simp
558   then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
559     by (simp only: ac_simps)
560   then show ?thesis
561     by simp
562 qed
564 lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
565   by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
567 lemma lcm_mult_unit2: "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
568   using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
570 lemma lcm_div_unit1:
571   "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
572   by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
574 lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
575   by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
577 lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
578   by (fact lcm.normalize_left_idem)
580 lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
581   by (fact lcm.normalize_right_idem)
583 lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
584   apply (rule gcdI)
585      apply simp_all
586   apply (rule dvd_trans)
587    apply (rule gcd_dvd1)
588   apply (simp add: unit_simps)
589   done
591 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
592   apply (subst gcd.commute)
593   apply (subst gcd_mult_unit1)
594    apply assumption
595   apply (rule gcd.commute)
596   done
598 lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
599   by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
601 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
602   by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
604 lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
605   by (fact gcd.normalize_left_idem)
607 lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
608   by (fact gcd.normalize_right_idem)
610 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
611   by standard (simp_all add: fun_eq_iff ac_simps)
613 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
614   by standard (simp_all add: fun_eq_iff ac_simps)
616 lemma 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"
617 proof (rule gcdI)
618   assume *: "gcd a b dvd gcd c d"
619     and **: "gcd c d dvd gcd a b"
620   have "gcd c d dvd c"
621     by simp
622   with * show "gcd a b dvd c"
623     by (rule dvd_trans)
624   have "gcd c d dvd d"
625     by simp
626   with * show "gcd a b dvd d"
627     by (rule dvd_trans)
628   show "normalize (gcd a b) = gcd a b"
629     by simp
630   fix l assume "l dvd c" and "l dvd d"
631   then have "l dvd gcd c d"
632     by (rule gcd_greatest)
633   from this and ** show "l dvd gcd a b"
634     by (rule dvd_trans)
635 qed
637 lemma coprime_dvd_mult:
638   assumes "coprime a b" and "a dvd c * b"
639   shows "a dvd c"
640 proof (cases "c = 0")
641   case True
642   then show ?thesis by simp
643 next
644   case False
645   then have unit: "is_unit (unit_factor c)"
646     by simp
647   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
648   have "gcd (c * a) (c * b) * unit_factor c = c"
649     by (simp add: ac_simps)
650   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
651     by (simp add: dvd_mult_unit_iff unit)
652   ultimately show ?thesis
653     by simp
654 qed
656 lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
657   by (auto intro: coprime_dvd_mult)
659 lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
660   apply (rule associated_eqI)
661      apply (rule gcd_greatest)
662       apply (rule_tac b = c in coprime_dvd_mult)
663        apply (simp add: gcd.assoc)
664        apply (simp_all add: ac_simps)
665   done
667 lemma coprime_crossproduct:
668   fixes a b c d :: 'a
669   assumes "coprime a d" and "coprime b c"
670   shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
671     normalize a = normalize b \<and> normalize c = normalize d"
672     (is "?lhs \<longleftrightarrow> ?rhs")
673 proof
674   assume ?rhs
675   then show ?lhs by simp
676 next
677   assume ?lhs
678   from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
679     by (auto intro: dvdI dest: sym)
680   with \<open>coprime a d\<close> have "a dvd b"
681     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
682   from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
683     by (auto intro: dvdI dest: sym)
684   with \<open>coprime b c\<close> have "b dvd a"
685     by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
686   from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
687     by (auto intro: dvdI dest: sym simp add: mult.commute)
688   with \<open>coprime b c\<close> have "c dvd d"
689     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
690   from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
691     by (auto intro: dvdI dest: sym simp add: mult.commute)
692   with \<open>coprime a d\<close> have "d dvd c"
693     by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
694   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
695     by (rule associatedI)
696   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
697     by (rule associatedI)
698   ultimately show ?rhs ..
699 qed
701 lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
702   by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
704 lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
705   using gcd_add1 [of n m] by (simp add: ac_simps)
707 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
708   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
710 lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
711   by (rule sym, rule gcdI) simp_all
713 lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
714   by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
716 lemma div_gcd_coprime:
717   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
718   shows "coprime (a div gcd a b) (b div gcd a b)"
719 proof -
720   let ?g = "gcd a b"
721   let ?a' = "a div ?g"
722   let ?b' = "b div ?g"
723   let ?g' = "gcd ?a' ?b'"
724   have dvdg: "?g dvd a" "?g dvd b"
725     by simp_all
726   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
727     by simp_all
728   from dvdg dvdg' obtain ka kb ka' kb' where
729     kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
730     unfolding dvd_def by blast
731   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
732     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
733   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
734     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
735   have "?g \<noteq> 0"
736     using nz by simp
737   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
738   ultimately show ?thesis
739     using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
740 qed
742 lemma divides_mult:
743   assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
744   shows "a * b dvd c"
745 proof -
746   from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
747   with \<open>a dvd c\<close> have "a dvd b' * b"
748     by (simp add: ac_simps)
749   with \<open>coprime a b\<close> have "a dvd b'"
750     by (simp add: coprime_dvd_mult_iff)
751   then obtain a' where "b' = a * a'" ..
752   with \<open>c = b * b'\<close> have "c = (a * b) * a'"
753     by (simp add: ac_simps)
754   then show ?thesis ..
755 qed
757 lemma coprime_lmult:
758   assumes dab: "gcd d (a * b) = 1"
759   shows "gcd d a = 1"
760 proof (rule coprimeI)
761   fix l
762   assume "l dvd d" and "l dvd a"
763   then have "l dvd a * b"
764     by simp
765   with \<open>l dvd d\<close> and dab show "l dvd 1"
766     by (auto intro: gcd_greatest)
767 qed
769 lemma coprime_rmult:
770   assumes dab: "gcd d (a * b) = 1"
771   shows "gcd d b = 1"
772 proof (rule coprimeI)
773   fix l
774   assume "l dvd d" and "l dvd b"
775   then have "l dvd a * b"
776     by simp
777   with \<open>l dvd d\<close> and dab show "l dvd 1"
778     by (auto intro: gcd_greatest)
779 qed
781 lemma coprime_mult:
782   assumes "coprime d a"
783     and "coprime d b"
784   shows "coprime d (a * b)"
785   apply (subst gcd.commute)
786   using assms(1) apply (subst gcd_mult_cancel)
787    apply (subst gcd.commute)
788    apply assumption
789   apply (subst gcd.commute)
790   apply (rule assms(2))
791   done
793 lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
794   using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
795   by blast
797 lemma coprime_mul_eq':
798   "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
799   using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
801 lemma gcd_coprime:
802   assumes c: "gcd a b \<noteq> 0"
803     and a: "a = a' * gcd a b"
804     and b: "b = b' * gcd a b"
805   shows "gcd a' b' = 1"
806 proof -
807   from c have "a \<noteq> 0 \<or> b \<noteq> 0"
808     by simp
809   with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
810   also from assms have "a div gcd a b = a'"
811     using dvd_div_eq_mult local.gcd_dvd1 by blast
812   also from assms have "b div gcd a b = b'"
813     using dvd_div_eq_mult local.gcd_dvd1 by blast
814   finally show ?thesis .
815 qed
817 lemma coprime_power:
818   assumes "0 < n"
819   shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
820   using assms
821 proof (induct n)
822   case 0
823   then show ?case by simp
824 next
825   case (Suc n)
826   then show ?case
827     by (cases n) (simp_all add: coprime_mul_eq)
828 qed
830 lemma gcd_coprime_exists:
831   assumes "gcd a b \<noteq> 0"
832   shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
833   apply (rule_tac x = "a div gcd a b" in exI)
834   apply (rule_tac x = "b div gcd a b" in exI)
835   using assms
836   apply (auto intro: div_gcd_coprime)
837   done
839 lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
840   by (induct n) (simp_all add: coprime_mult)
842 lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
843   by (induct n) (simp_all add: gcd_mult_cancel)
845 lemma coprime_exp2:
846   assumes "coprime a b"
847   shows "coprime (a ^ n) (b ^ m)"
848 proof (rule coprime_exp_left)
849   from assms show "coprime a (b ^ m)"
850     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
851 qed
853 lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
854 proof (cases "a = 0 \<and> b = 0")
855   case True
856   then show ?thesis
857     by (cases n) simp_all
858 next
859   case False
860   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
861     using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
862   then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
863     by simp
864   also note gcd_mult_distrib
865   also have "unit_factor (gcd a b ^ n) = 1"
866     using False by (auto simp add: unit_factor_power unit_factor_gcd)
867   also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
868     apply (subst ac_simps)
869     apply (subst div_power)
870      apply simp
871     apply (rule dvd_div_mult_self)
872     apply (rule dvd_power_same)
873     apply simp
874     done
875   also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
876     apply (subst ac_simps)
877     apply (subst div_power)
878      apply simp
879     apply (rule dvd_div_mult_self)
880     apply (rule dvd_power_same)
881     apply simp
882     done
883   finally show ?thesis by simp
884 qed
886 lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
887   apply (subgoal_tac "a dvd gcd a b")
888    apply simp
889   apply (erule (1) gcd_greatest)
890   done
892 lemma division_decomp:
893   assumes "a dvd b * c"
894   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
895 proof (cases "gcd a b = 0")
896   case True
897   then have "a = 0 \<and> b = 0"
898     by simp
899   then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
900     by simp
901   then show ?thesis by blast
902 next
903   case False
904   let ?d = "gcd a b"
905   from gcd_coprime_exists [OF False]
906     obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
907     by blast
908   from ab'(1) have "a' dvd a"
909     unfolding dvd_def by blast
910   with assms have "a' dvd b * c"
911     using dvd_trans [of a' a "b * c"] by simp
912   from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
913     by simp
914   then have "?d * a' dvd ?d * (b' * c)"
915     by (simp add: mult_ac)
916   with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
917     by simp
918   with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
919     by (subst (asm) ac_simps) blast
920   with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
921     by (simp add: mult_ac)
922   then show ?thesis by blast
923 qed
925 lemma pow_divs_pow:
926   assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
927   shows "a dvd b"
928 proof (cases "gcd a b = 0")
929   case True
930   then show ?thesis by simp
931 next
932   case False
933   let ?d = "gcd a b"
934   from n obtain m where m: "n = Suc m"
935     by (cases n) simp_all
936   from False have zn: "?d ^ n \<noteq> 0"
937     by (rule power_not_zero)
938   from gcd_coprime_exists [OF False]
939   obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
940     by blast
941   from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
942     by (simp add: ab'(1,2)[symmetric])
943   then have "?d^n * a'^n dvd ?d^n * b'^n"
944     by (simp only: power_mult_distrib ac_simps)
945   with zn have "a'^n dvd b'^n"
946     by simp
947   then have "a' dvd b'^n"
948     using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
949   then have "a' dvd b'^m * b'"
950     by (simp add: m ac_simps)
951   with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
952   have "a' dvd b'" by (subst (asm) ac_simps) blast
953   then have "a' * ?d dvd b' * ?d"
954     by (rule mult_dvd_mono) simp
955   with ab'(1,2) show ?thesis
956     by simp
957 qed
959 lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
960   by (auto intro: pow_divs_pow dvd_power_same)
962 lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
963   by (subst add_commute) simp
965 lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
966   by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
968 lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
969   by (induct xs) (simp_all add: gcd_mult_cancel)
971 lemma coprime_divisors:
972   assumes "d dvd a" "e dvd b" "gcd a b = 1"
973   shows "gcd d e = 1"
974 proof -
975   from assms obtain k l where "a = d * k" "b = e * l"
976     unfolding dvd_def by blast
977   with assms have "gcd (d * k) (e * l) = 1"
978     by simp
979   then have "gcd (d * k) e = 1"
980     by (rule coprime_lmult)
981   also have "gcd (d * k) e = gcd e (d * k)"
982     by (simp add: ac_simps)
983   finally have "gcd e d = 1"
984     by (rule coprime_lmult)
985   then show ?thesis
986     by (simp add: ac_simps)
987 qed
989 lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
990   by (simp add: lcm_gcd)
992 declare unit_factor_lcm [simp]
994 lemma lcmI:
995   assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
996     and "normalize c = c"
997   shows "c = lcm a b"
998   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
1000 lemma gcd_dvd_lcm [simp]: "gcd a b dvd lcm a b"
1001   using gcd_dvd2 by (rule dvd_lcmI2)
1003 lemmas lcm_0 = lcm_0_right
1005 lemma lcm_unique:
1006   "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"
1007   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
1009 lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
1010   by (subst lcm_gcd) simp
1012 lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
1013   apply (cases "a = 0")
1014    apply simp
1015   apply (rule sym)
1016   apply (rule lcmI)
1017      apply simp_all
1018   done
1020 lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
1021   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
1023 lemma lcm_proj1_iff: "lcm m n = normalize m \<longleftrightarrow> n dvd m"
1024 proof
1025   assume *: "lcm m n = normalize m"
1026   show "n dvd m"
1027   proof (cases "m = 0")
1028     case True
1029     then show ?thesis by simp
1030   next
1031     case [simp]: False
1032     from * have **: "m = lcm m n * unit_factor m"
1033       by (simp add: unit_eq_div2)
1034     show ?thesis by (subst **) simp
1035   qed
1036 next
1037   assume "n dvd m"
1038   then show "lcm m n = normalize m"
1039     by (rule lcm_proj1_if_dvd)
1040 qed
1042 lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
1043   using lcm_proj1_iff [of n m] by (simp add: ac_simps)
1045 lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
1046   by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
1048 lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
1049 proof-
1050   have "normalize k * lcm a b = lcm (k * a) (k * b)"
1051     by (simp add: lcm_mult_distrib')
1052   then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
1053     by simp
1054   then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
1055     by (simp only: ac_simps)
1056   then show ?thesis
1057     by simp
1058 qed
1060 lemma dvd_productE:
1061   assumes "p dvd (a * b)"
1062   obtains x y where "p = x * y" "x dvd a" "y dvd b"
1063 proof (cases "a = 0")
1064   case True
1065   thus ?thesis by (intro that[of p 1]) simp_all
1066 next
1067   case False
1068   define x y where "x = gcd a p" and "y = p div x"
1069   have "p = x * y" by (simp add: x_def y_def)
1070   moreover have "x dvd a" by (simp add: x_def)
1071   moreover from assms have "p dvd gcd (b * a) (b * p)"
1072     by (intro gcd_greatest) (simp_all add: mult.commute)
1073   hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
1074   with False have "y dvd b"
1075     by (simp add: x_def y_def div_dvd_iff_mult assms)
1076   ultimately show ?thesis by (rule that)
1077 qed
1079 lemma coprime_crossproduct':
1080   fixes a b c d
1081   assumes "b \<noteq> 0"
1082   assumes unit_factors: "unit_factor b = unit_factor d"
1083   assumes coprime: "coprime a b" "coprime c d"
1084   shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
1085 proof safe
1086   assume eq: "a * d = b * c"
1087   hence "normalize a * normalize d = normalize c * normalize b"
1088     by (simp only: normalize_mult [symmetric] mult_ac)
1089   with coprime have "normalize b = normalize d"
1090     by (subst (asm) coprime_crossproduct) simp_all
1091   from this and unit_factors show "b = d"
1092     by (rule normalize_unit_factor_eqI)
1093   from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
1094   with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
1095 qed (simp_all add: mult_ac)
1097 end
1099 class ring_gcd = comm_ring_1 + semiring_gcd
1100 begin
1102 lemma coprime_minus_one: "coprime (n - 1) n"
1103   using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
1105 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
1106   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
1108 lemma gcd_neg2 [simp]: "gcd a (-b) = gcd a b"
1109   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
1111 lemma gcd_neg_numeral_1 [simp]: "gcd (- numeral n) a = gcd (numeral n) a"
1112   by (fact gcd_neg1)
1114 lemma gcd_neg_numeral_2 [simp]: "gcd a (- numeral n) = gcd a (numeral n)"
1115   by (fact gcd_neg2)
1117 lemma gcd_diff1: "gcd (m - n) n = gcd m n"
1118   by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric], subst gcd_add1, simp)
1120 lemma gcd_diff2: "gcd (n - m) n = gcd m n"
1121   by (subst gcd_neg1[symmetric]) (simp only: minus_diff_eq gcd_diff1)
1123 lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
1124   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
1126 lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
1127   by (rule sym, rule lcmI) (simp_all add: lcm_least lcm_eq_0_iff)
1129 lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
1130   by (fact lcm_neg1)
1132 lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
1133   by (fact lcm_neg2)
1135 end
1137 class semiring_Gcd = semiring_gcd + Gcd +
1138   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1139     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
1140     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
1141   assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
1142     and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
1143     and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
1144 begin
1146 lemma Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
1147   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
1149 lemma Gcd_Lcm: "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
1150   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
1152 lemma Gcd_empty [simp]: "Gcd {} = 0"
1153   by (rule dvd_0_left, rule Gcd_greatest) simp
1155 lemma Lcm_empty [simp]: "Lcm {} = 1"
1156   by (auto intro: associated_eqI Lcm_least)
1158 lemma Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
1159 proof -
1160   have "Gcd (insert a A) dvd gcd a (Gcd A)"
1161     by (auto intro: Gcd_dvd Gcd_greatest)
1162   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
1163   proof (rule Gcd_greatest)
1164     fix b
1165     assume "b \<in> insert a A"
1166     then show "gcd a (Gcd A) dvd b"
1167     proof
1168       assume "b = a"
1169       then show ?thesis
1170         by simp
1171     next
1172       assume "b \<in> A"
1173       then have "Gcd A dvd b"
1174         by (rule Gcd_dvd)
1175       moreover have "gcd a (Gcd A) dvd Gcd A"
1176         by simp
1177       ultimately show ?thesis
1178         by (blast intro: dvd_trans)
1179     qed
1180   qed
1181   ultimately show ?thesis
1182     by (auto intro: associated_eqI)
1183 qed
1185 lemma Lcm_insert [simp]: "Lcm (insert a A) = lcm a (Lcm A)"
1186 proof (rule sym)
1187   have "lcm a (Lcm A) dvd Lcm (insert a A)"
1188     by (auto intro: dvd_Lcm Lcm_least)
1189   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
1190   proof (rule Lcm_least)
1191     fix b
1192     assume "b \<in> insert a A"
1193     then show "b dvd lcm a (Lcm A)"
1194     proof
1195       assume "b = a"
1196       then show ?thesis by simp
1197     next
1198       assume "b \<in> A"
1199       then have "b dvd Lcm A"
1200         by (rule dvd_Lcm)
1201       moreover have "Lcm A dvd lcm a (Lcm A)"
1202         by simp
1203       ultimately show ?thesis
1204         by (blast intro: dvd_trans)
1205     qed
1206   qed
1207   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
1208     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
1209 qed
1211 lemma LcmI:
1212   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b"
1213     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
1214     and "normalize b = b"
1215   shows "b = Lcm A"
1216   by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
1218 lemma Lcm_subset: "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
1219   by (blast intro: Lcm_least dvd_Lcm)
1221 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
1222   apply (rule lcmI)
1223      apply (blast intro: Lcm_subset)
1224     apply (blast intro: Lcm_subset)
1225    apply (intro Lcm_least ballI, elim UnE)
1226     apply (rule dvd_trans, erule dvd_Lcm, assumption)
1227    apply (rule dvd_trans, erule dvd_Lcm, assumption)
1228   apply simp
1229   done
1231 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
1232   (is "?P \<longleftrightarrow> ?Q")
1233 proof
1234   assume ?P
1235   show ?Q
1236   proof
1237     fix a
1238     assume "a \<in> A"
1239     then have "Gcd A dvd a"
1240       by (rule Gcd_dvd)
1241     with \<open>?P\<close> have "a = 0"
1242       by simp
1243     then show "a \<in> {0}"
1244       by simp
1245   qed
1246 next
1247   assume ?Q
1248   have "0 dvd Gcd A"
1249   proof (rule Gcd_greatest)
1250     fix a
1251     assume "a \<in> A"
1252     with \<open>?Q\<close> have "a = 0"
1253       by auto
1254     then show "0 dvd a"
1255       by simp
1256   qed
1257   then show ?P
1258     by simp
1259 qed
1261 lemma Lcm_1_iff [simp]: "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
1262   (is "?P \<longleftrightarrow> ?Q")
1263 proof
1264   assume ?P
1265   show ?Q
1266   proof
1267     fix a
1268     assume "a \<in> A"
1269     then have "a dvd Lcm A"
1270       by (rule dvd_Lcm)
1271     with \<open>?P\<close> show "is_unit a"
1272       by simp
1273   qed
1274 next
1275   assume ?Q
1276   then have "is_unit (Lcm A)"
1277     by (blast intro: Lcm_least)
1278   then have "normalize (Lcm A) = 1"
1279     by (rule is_unit_normalize)
1280   then show ?P
1281     by simp
1282 qed
1284 lemma unit_factor_Lcm: "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1285 proof (cases "Lcm A = 0")
1286   case True
1287   then show ?thesis
1288     by simp
1289 next
1290   case False
1291   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
1292     by blast
1293   with False show ?thesis
1294     by simp
1295 qed
1297 lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1298   by (simp add: Gcd_Lcm unit_factor_Lcm)
1300 lemma GcdI:
1301   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a"
1302     and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
1303     and "normalize b = b"
1304   shows "b = Gcd A"
1305   by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
1307 lemma Gcd_eq_1_I:
1308   assumes "is_unit a" and "a \<in> A"
1309   shows "Gcd A = 1"
1310 proof -
1311   from assms have "is_unit (Gcd A)"
1312     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
1313   then have "normalize (Gcd A) = 1"
1314     by (rule is_unit_normalize)
1315   then show ?thesis
1316     by simp
1317 qed
1319 lemma Lcm_eq_0_I:
1320   assumes "0 \<in> A"
1321   shows "Lcm A = 0"
1322 proof -
1323   from assms have "0 dvd Lcm A"
1324     by (rule dvd_Lcm)
1325   then show ?thesis
1326     by simp
1327 qed
1329 lemma Gcd_UNIV [simp]: "Gcd UNIV = 1"
1330   using dvd_refl by (rule Gcd_eq_1_I) simp
1332 lemma Lcm_UNIV [simp]: "Lcm UNIV = 0"
1333   by (rule Lcm_eq_0_I) simp
1335 lemma Lcm_0_iff:
1336   assumes "finite A"
1337   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
1338 proof (cases "A = {}")
1339   case True
1340   then show ?thesis by simp
1341 next
1342   case False
1343   with assms show ?thesis
1344     by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
1345 qed
1347 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
1348 proof -
1349   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
1350   proof -
1351     from that obtain B where "A = insert a B"
1352       by blast
1353     moreover have "gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
1354       by (rule gcd_dvd1)
1355     ultimately show "Gcd (normalize ` A) dvd a"
1356       by simp
1357   qed
1358   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
1359     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
1360   then show ?thesis
1361     by (auto intro: associated_eqI)
1362 qed
1364 lemma Gcd_eqI:
1365   assumes "normalize a = a"
1366   assumes "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
1367     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> c dvd b) \<Longrightarrow> c dvd a"
1368   shows "Gcd A = a"
1369   using assms by (blast intro: associated_eqI Gcd_greatest Gcd_dvd normalize_Gcd)
1371 lemma dvd_GcdD: "x dvd Gcd A \<Longrightarrow> y \<in> A \<Longrightarrow> x dvd y"
1372   using Gcd_dvd dvd_trans by blast
1374 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
1375   by (blast dest: dvd_GcdD intro: Gcd_greatest)
1377 lemma Gcd_mult: "Gcd (op * c ` A) = normalize c * Gcd A"
1378 proof (cases "c = 0")
1379   case True
1380   then show ?thesis by auto
1381 next
1382   case [simp]: False
1383   have "Gcd (op * c ` A) div c dvd Gcd A"
1384     by (intro Gcd_greatest, subst div_dvd_iff_mult)
1385        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
1386   then have "Gcd (op * c ` A) dvd c * Gcd A"
1387     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
1388   also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
1389     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
1390   also have "Gcd (op * c ` A) dvd \<dots> \<longleftrightarrow> Gcd (op * c ` A) dvd normalize c * Gcd A"
1391     by (simp add: dvd_mult_unit_iff)
1392   finally have "Gcd (op * c ` A) dvd normalize c * Gcd A" .
1393   moreover have "normalize c * Gcd A dvd Gcd (op * c ` A)"
1394     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
1395   ultimately have "normalize (Gcd (op * c ` A)) = normalize (normalize c * Gcd A)"
1396     by (rule associatedI)
1397   then show ?thesis
1398     by (simp add: normalize_mult)
1399 qed
1401 lemma Lcm_eqI:
1402   assumes "normalize a = a"
1403     and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
1404     and "\<And>c. (\<And>b. b \<in> A \<Longrightarrow> b dvd c) \<Longrightarrow> a dvd c"
1405   shows "Lcm A = a"
1406   using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
1408 lemma Lcm_dvdD: "Lcm A dvd x \<Longrightarrow> y \<in> A \<Longrightarrow> y dvd x"
1409   using dvd_Lcm dvd_trans by blast
1411 lemma Lcm_dvd_iff: "Lcm A dvd x \<longleftrightarrow> (\<forall>y\<in>A. y dvd x)"
1412   by (blast dest: Lcm_dvdD intro: Lcm_least)
1414 lemma Lcm_mult:
1415   assumes "A \<noteq> {}"
1416   shows "Lcm (op * c ` A) = normalize c * Lcm A"
1417 proof (cases "c = 0")
1418   case True
1419   with assms have "op * c ` A = {0}"
1420     by auto
1421   with True show ?thesis by auto
1422 next
1423   case [simp]: False
1424   from assms obtain x where x: "x \<in> A"
1425     by blast
1426   have "c dvd c * x"
1427     by simp
1428   also from x have "c * x dvd Lcm (op * c ` A)"
1429     by (intro dvd_Lcm) auto
1430   finally have dvd: "c dvd Lcm (op * c ` A)" .
1432   have "Lcm A dvd Lcm (op * c ` A) div c"
1433     by (intro Lcm_least dvd_mult_imp_div)
1434       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
1435   then have "c * Lcm A dvd Lcm (op * c ` A)"
1436     by (subst (asm) dvd_div_iff_mult) (auto intro!: Lcm_least simp: mult_ac dvd)
1437   also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
1438     by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
1439   also have "\<dots> dvd Lcm (op * c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm (op * c ` A)"
1440     by (simp add: mult_unit_dvd_iff)
1441   finally have "normalize c * Lcm A dvd Lcm (op * c ` A)" .
1442   moreover have "Lcm (op * c ` A) dvd normalize c * Lcm A"
1443     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
1444   ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm (op * c ` A))"
1445     by (rule associatedI)
1446   then show ?thesis
1447     by (simp add: normalize_mult)
1448 qed
1450 lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
1451 proof -
1452   have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A"
1453     by blast
1454   then have "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
1455     by (simp add: Lcm_Un [symmetric])
1456   also have "Lcm {a\<in>A. is_unit a} = 1"
1457     by simp
1458   finally show ?thesis
1459     by simp
1460 qed
1462 lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> (\<nexists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
1463   by (metis Lcm_least dvd_0_left dvd_Lcm)
1465 lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not> a dvd m)) \<Longrightarrow> Lcm A = 0"
1466   by (auto simp: Lcm_0_iff')
1468 lemma Lcm_singleton [simp]: "Lcm {a} = normalize a"
1469   by simp
1471 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
1472   by simp
1474 lemma Lcm_coprime:
1475   assumes "finite A"
1476     and "A \<noteq> {}"
1477     and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
1478   shows "Lcm A = normalize (\<Prod>A)"
1479   using assms
1480 proof (induct rule: finite_ne_induct)
1481   case singleton
1482   then show ?case by simp
1483 next
1484   case (insert a A)
1485   have "Lcm (insert a A) = lcm a (Lcm A)"
1486     by simp
1487   also from insert have "Lcm A = normalize (\<Prod>A)"
1488     by blast
1489   also have "lcm a \<dots> = lcm a (\<Prod>A)"
1490     by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
1491   also from insert have "gcd a (\<Prod>A) = 1"
1492     by (subst gcd.commute, intro prod_coprime) auto
1493   with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
1494     by (simp add: lcm_coprime)
1495   finally show ?case .
1496 qed
1498 lemma Lcm_coprime':
1499   "card A \<noteq> 0 \<Longrightarrow>
1500     (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
1501     Lcm A = normalize (\<Prod>A)"
1502   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
1504 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
1505   by (auto intro!: Gcd_eq_1_I)
1507 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
1508   by simp
1510 lemma Gcd_2 [simp]: "Gcd {a, b} = gcd a b"
1511   by simp
1514 definition pairwise_coprime
1515   where "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
1517 lemma pairwise_coprimeI [intro?]:
1518   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
1519   by (simp add: pairwise_coprime_def)
1521 lemma pairwise_coprimeD:
1522   "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
1523   by (simp add: pairwise_coprime_def)
1525 lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
1526   by (force simp: pairwise_coprime_def)
1528 end
1531 subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
1533 context semiring_gcd
1534 begin
1536 sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
1537 defines
1538   Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _"  900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
1540 abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
1541   where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
1543 sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
1544 defines
1545   Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _"  900) = Lcm_fin.F ..
1547 abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
1548   where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
1550 lemma Gcd_fin_dvd:
1551   "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
1552   by (induct A rule: infinite_finite_induct)
1553     (auto intro: dvd_trans)
1555 lemma dvd_Lcm_fin:
1556   "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
1557   by (induct A rule: infinite_finite_induct)
1558     (auto intro: dvd_trans)
1560 lemma Gcd_fin_greatest:
1561   "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
1562   using that by (induct A) simp_all
1564 lemma Lcm_fin_least:
1565   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
1566   using that by (induct A) simp_all
1568 lemma gcd_list_greatest:
1569   "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
1570   by (rule Gcd_fin_greatest) (simp_all add: that)
1572 lemma lcm_list_least:
1573   "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
1574   by (rule Lcm_fin_least) (simp_all add: that)
1576 lemma dvd_Gcd_fin_iff:
1577   "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
1578   using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
1580 lemma dvd_gcd_list_iff:
1581   "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
1582   by (simp add: dvd_Gcd_fin_iff)
1584 lemma Lcm_fin_dvd_iff:
1585   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
1586   using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
1588 lemma lcm_list_dvd_iff:
1589   "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
1590   by (simp add: Lcm_fin_dvd_iff)
1592 lemma Gcd_fin_mult:
1593   "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
1594 using that proof induct
1595   case empty
1596   then show ?case
1597     by simp
1598 next
1599   case (insert a A)
1600   have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
1601     by simp
1602   also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
1603     by (simp add: normalize_mult)
1604   finally show ?case
1605     using insert by (simp add: gcd_mult_distrib')
1606 qed
1608 lemma Lcm_fin_mult:
1609   "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
1610 proof (cases "b = 0")
1611   case True
1612   moreover from that have "times 0 ` A = {0}"
1613     by auto
1614   ultimately show ?thesis
1615     by simp
1616 next
1617   case False
1618   then have "inj (times b)"
1619     by (rule inj_times)
1620   show ?thesis proof (cases "finite A")
1621     case False
1622     moreover from \<open>inj (times b)\<close>
1623     have "inj_on (times b) A"
1624       by (rule inj_on_subset) simp
1625     ultimately have "infinite (times b ` A)"
1626       by (simp add: finite_image_iff)
1627     with False show ?thesis
1628       by simp
1629   next
1630     case True
1631     then show ?thesis using that proof (induct A rule: finite_ne_induct)
1632       case (singleton a)
1633       then show ?case
1634         by (simp add: normalize_mult)
1635     next
1636       case (insert a A)
1637       have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
1638         by simp
1639       also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
1640         by (simp add: normalize_mult)
1641       finally show ?case
1642         using insert by (simp add: lcm_mult_distrib')
1643     qed
1644   qed
1645 qed
1647 end
1649 context semiring_Gcd
1650 begin
1652 lemma Gcd_fin_eq_Gcd [simp]:
1653   "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
1654   using that by induct simp_all
1656 lemma Gcd_set_eq_fold [code_unfold]:
1657   "Gcd (set xs) = fold gcd xs 0"
1658   by (simp add: Gcd_fin.set_eq_fold [symmetric])
1660 lemma Lcm_fin_eq_Lcm [simp]:
1661   "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
1662   using that by induct simp_all
1664 lemma Lcm_set_eq_fold [code_unfold]:
1665   "Lcm (set xs) = fold lcm xs 1"
1666   by (simp add: Lcm_fin.set_eq_fold [symmetric])
1668 end
1670 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
1672 instantiation nat :: gcd
1673 begin
1675 fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1676   where "gcd_nat x y = (if y = 0 then x else gcd y (x mod y))"
1678 definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1679   where "lcm_nat x y = x * y div (gcd x y)"
1681 instance ..
1683 end
1685 instantiation int :: gcd
1686 begin
1688 definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
1689   where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1691 definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
1692   where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1694 instance ..
1696 end
1698 text \<open>Transfer setup\<close>
1700 lemma transfer_nat_int_gcd:
1701   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
1702   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
1703   for x y :: int
1704   unfolding gcd_int_def lcm_int_def by auto
1706 lemma transfer_nat_int_gcd_closures:
1707   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
1708   "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
1709   for x y :: int
1710   by (auto simp add: gcd_int_def lcm_int_def)
1712 declare transfer_morphism_nat_int
1713   [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
1715 lemma transfer_int_nat_gcd:
1716   "gcd (int x) (int y) = int (gcd x y)"
1717   "lcm (int x) (int y) = int (lcm x y)"
1718   by (auto simp: gcd_int_def lcm_int_def)
1720 lemma transfer_int_nat_gcd_closures:
1721   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
1722   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
1723   by (auto simp: gcd_int_def lcm_int_def)
1725 declare transfer_morphism_int_nat
1726   [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
1728 lemma gcd_nat_induct:
1729   fixes m n :: nat
1730   assumes "\<And>m. P m 0"
1731     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
1732   shows "P m n"
1733   apply (rule gcd_nat.induct)
1734   apply (case_tac "y = 0")
1735   using assms
1736    apply simp_all
1737   done
1740 text \<open>Specific to \<open>int\<close>.\<close>
1742 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
1743   by (simp add: gcd_int_def)
1745 lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
1746   by (simp add: lcm_int_def)
1748 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
1749   for x y :: int
1750   by (simp add: gcd_int_def)
1752 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
1753   for x y :: int
1754   by (simp add: gcd_int_def)
1756 lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
1757   for x y :: int
1758   by (simp add: gcd_int_def)
1760 lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
1761   for x y :: int
1762   by (simp add: gcd_int_def)
1764 lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
1765   for x y :: int
1766   by (metis abs_idempotent gcd_abs_int)
1768 lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
1769   for x y :: int
1770   by (metis abs_idempotent gcd_abs_int)
1772 lemma gcd_cases_int:
1773   fixes x y :: int
1774   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd x y)"
1775     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd x (- y))"
1776     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (gcd (- x) y)"
1777     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (gcd (- x) (- y))"
1778   shows "P (gcd x y)"
1779   using assms by auto arith
1781 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
1782   for x y :: int
1783   by (simp add: gcd_int_def)
1785 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
1786   for x y :: int
1787   by (simp add: lcm_int_def)
1789 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
1790   for x y :: int
1791   by (simp add: lcm_int_def)
1793 lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
1794   for x y :: int
1795   by (simp add: lcm_int_def)
1797 lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
1798   for i j :: int
1799   by (simp add:lcm_int_def)
1801 lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
1802   for x y :: int
1803   by (metis abs_idempotent lcm_int_def)
1805 lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
1806   for x y :: int
1807   by (metis abs_idempotent lcm_int_def)
1809 lemma lcm_cases_int:
1810   fixes x y :: int
1811   assumes "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm x y)"
1812     and "x \<ge> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm x (- y))"
1813     and "x \<le> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> P (lcm (- x) y)"
1814     and "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> P (lcm (- x) (- y))"
1815   shows "P (lcm x y)"
1816   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
1818 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
1819   for x y :: int
1820   by (simp add: lcm_int_def)
1822 lemma gcd_0_nat: "gcd x 0 = x"
1823   for x :: nat
1824   by simp
1826 lemma gcd_0_int [simp]: "gcd x 0 = \<bar>x\<bar>"
1827   for x :: int
1828   by (auto simp: gcd_int_def)
1830 lemma gcd_0_left_nat: "gcd 0 x = x"
1831   for x :: nat
1832   by simp
1834 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
1835   for x :: int
1836   by (auto simp:gcd_int_def)
1838 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
1839   for x y :: nat
1840   by (cases "y = 0") auto
1843 text \<open>Weaker, but useful for the simplifier.\<close>
1845 lemma gcd_non_0_nat: "y \<noteq> 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
1846   for x y :: nat
1847   by simp
1849 lemma gcd_1_nat [simp]: "gcd m 1 = 1"
1850   for m :: nat
1851   by simp
1853 lemma gcd_Suc_0 [simp]: "gcd m (Suc 0) = Suc 0"
1854   for m :: nat
1855   by simp
1857 lemma gcd_1_int [simp]: "gcd m 1 = 1"
1858   for m :: int
1859   by (simp add: gcd_int_def)
1861 lemma gcd_idem_nat: "gcd x x = x"
1862   for x :: nat
1863   by simp
1865 lemma gcd_idem_int: "gcd x x = \<bar>x\<bar>"
1866   for x :: int
1867   by (auto simp add: gcd_int_def)
1869 declare gcd_nat.simps [simp del]
1871 text \<open>
1872   \<^medskip> @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.
1873   The conjunctions don't seem provable separately.
1874 \<close>
1876 instance nat :: semiring_gcd
1877 proof
1878   fix m n :: nat
1879   show "gcd m n dvd m" and "gcd m n dvd n"
1880   proof (induct m n rule: gcd_nat_induct)
1881     fix m n :: nat
1882     assume "gcd n (m mod n) dvd m mod n"
1883       and "gcd n (m mod n) dvd n"
1884     then have "gcd n (m mod n) dvd m"
1885       by (rule dvd_mod_imp_dvd)
1886     moreover assume "0 < n"
1887     ultimately show "gcd m n dvd m"
1888       by (simp add: gcd_non_0_nat)
1889   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
1890 next
1891   fix m n k :: nat
1892   assume "k dvd m" and "k dvd n"
1893   then show "k dvd gcd m n"
1894     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
1895 qed (simp_all add: lcm_nat_def)
1897 instance int :: ring_gcd
1898   by standard
1899     (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def
1900       zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
1902 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
1903   for a b :: nat
1904   by (rule dvd_imp_le) auto
1906 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd a b \<le> b"
1907   for a b :: nat
1908   by (rule dvd_imp_le) auto
1910 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd a b \<le> a"
1911   for a b :: int
1912   by (rule zdvd_imp_le) auto
1914 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd a b \<le> b"
1915   for a b :: int
1916   by (rule zdvd_imp_le) auto
1918 lemma gcd_pos_nat [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
1919   for m n :: nat
1920   using gcd_eq_0_iff [of m n] by arith
1922 lemma gcd_pos_int [simp]: "gcd m n > 0 \<longleftrightarrow> m \<noteq> 0 \<or> n \<noteq> 0"
1923   for m n :: int
1924   using gcd_eq_0_iff [of m n] gcd_ge_0_int [of m n] by arith
1926 lemma 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"
1927   for d a :: nat
1928   apply auto
1929   apply (rule dvd_antisym)
1930    apply (erule (1) gcd_greatest)
1931   apply auto
1932   done
1934 lemma gcd_unique_int:
1935   "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"
1936   for d a :: int
1937   apply (cases "d = 0")
1938    apply simp
1939   apply (rule iffI)
1940    apply (rule zdvd_antisym_nonneg)
1941       apply (auto intro: gcd_greatest)
1942   done
1944 interpretation gcd_nat:
1945   semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
1946   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
1948 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
1949   for x y :: int
1950   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
1952 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
1953   for x y :: int
1954   by (metis gcd_proj1_if_dvd_int gcd.commute)
1957 text \<open>\<^medskip> Multiplication laws.\<close>
1959 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
1960   for k m n :: nat
1961   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
1962   apply (induct m n rule: gcd_nat_induct)
1963    apply simp
1964   apply (cases "k = 0")
1965    apply (simp_all add: gcd_non_0_nat)
1966   done
1968 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
1969   for k m n :: int
1970   apply (subst (1 2) gcd_abs_int)
1971   apply (subst (1 2) abs_mult)
1972   apply (rule gcd_mult_distrib_nat [transferred])
1973     apply auto
1974   done
1976 lemma coprime_crossproduct_nat:
1977   fixes a b c d :: nat
1978   assumes "coprime a d" and "coprime b c"
1979   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
1980   using assms coprime_crossproduct [of a d b c] by simp
1982 lemma coprime_crossproduct_int:
1983   fixes a b c d :: int
1984   assumes "coprime a d" and "coprime b c"
1985   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>"
1986   using assms coprime_crossproduct [of a d b c] by simp
1989 text \<open>\medskip Addition laws.\<close>
1991 (* TODO: add the other variations? *)
1993 lemma gcd_diff1_nat: "m \<ge> n \<Longrightarrow> gcd (m - n) n = gcd m n"
1994   for m n :: nat
1995   by (subst gcd_add1 [symmetric]) auto
1997 lemma gcd_diff2_nat: "n \<ge> m \<Longrightarrow> gcd (n - m) n = gcd m n"
1998   for m n :: nat
1999   apply (subst gcd.commute)
2000   apply (subst gcd_diff1_nat [symmetric])
2001    apply auto
2002   apply (subst gcd.commute)
2003   apply (subst gcd_diff1_nat)
2004    apply assumption
2005   apply (rule gcd.commute)
2006   done
2008 lemma gcd_non_0_int: "y > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
2009   for x y :: int
2010   apply (frule_tac b = y and a = x in pos_mod_sign)
2011   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
2012   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
2013   apply (frule_tac a = x in pos_mod_bound)
2014   apply (subst (1 2) gcd.commute)
2015   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat nat_le_eq_zle)
2016   done
2018 lemma gcd_red_int: "gcd x y = gcd y (x mod y)"
2019   for x y :: int
2020   apply (cases "y = 0")
2021    apply force
2022   apply (cases "y > 0")
2023    apply (subst gcd_non_0_int, auto)
2024   apply (insert gcd_non_0_int [of "- y" "- x"])
2025   apply auto
2026   done
2028 (* TODO: differences, and all variations of addition rules
2029     as simplification rules for nat and int *)
2031 (* TODO: add the three variations of these, and for ints? *)
2033 lemma finite_divisors_nat [simp]: (* FIXME move *)
2034   fixes m :: nat
2035   assumes "m > 0"
2036   shows "finite {d. d dvd m}"
2037 proof-
2038   from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
2039     by (auto dest: dvd_imp_le)
2040   then show ?thesis
2041     using finite_Collect_le_nat by (rule finite_subset)
2042 qed
2044 lemma finite_divisors_int [simp]:
2045   fixes i :: int
2046   assumes "i \<noteq> 0"
2047   shows "finite {d. d dvd i}"
2048 proof -
2049   have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
2050     by (auto simp: abs_if)
2051   then have "finite {d. \<bar>d\<bar> \<le> \<bar>i\<bar>}"
2052     by simp
2053   from finite_subset [OF _ this] show ?thesis
2054     using assms by (simp add: dvd_imp_le_int subset_iff)
2055 qed
2057 lemma Max_divisors_self_nat [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::nat. d dvd n} = n"
2058   apply (rule antisym)
2059    apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
2060   apply simp
2061   done
2063 lemma Max_divisors_self_int [simp]: "n \<noteq> 0 \<Longrightarrow> Max {d::int. d dvd n} = \<bar>n\<bar>"
2064   apply (rule antisym)
2065    apply (rule Max_le_iff [THEN iffD2])
2066      apply (auto intro: abs_le_D1 dvd_imp_le_int)
2067   done
2069 lemma gcd_is_Max_divisors_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
2070   for m n :: nat
2071   apply (rule Max_eqI[THEN sym])
2072     apply (metis finite_Collect_conjI finite_divisors_nat)
2073    apply simp
2074    apply (metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
2075   apply simp
2076   done
2078 lemma gcd_is_Max_divisors_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> gcd m n = Max {d. d dvd m \<and> d dvd n}"
2079   for m n :: int
2080   apply (rule Max_eqI[THEN sym])
2081     apply (metis finite_Collect_conjI finite_divisors_int)
2082    apply simp
2083    apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
2084   apply simp
2085   done
2087 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
2088   for k l :: int
2089   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
2092 subsection \<open>Coprimality\<close>
2094 lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
2095   for a b :: nat
2096   using coprime [of a b] by simp
2098 lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
2099   for a b :: nat
2100   using coprime_nat by simp
2102 lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
2103   for a b :: int
2104   using gcd_unique_int [of 1 a b]
2105   apply clarsimp
2106   apply (erule subst)
2107   apply (rule iffI)
2108    apply force
2109   using abs_dvd_iff abs_ge_zero apply blast
2110   done
2112 lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
2113   for a b n :: nat
2114   using pow_divs_eq[of n] by simp
2116 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
2117   using coprime_plus_one[of n] by simp
2119 lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
2120   for n :: nat
2121   using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
2123 lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
2124   for a b :: nat
2125   by (metis gcd_greatest_iff nat_dvd_1_iff_1)
2127 lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
2128   for a b :: int
2129   using gcd_greatest_iff [of x a b] by auto
2131 lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
2132   for m x y :: nat
2133   by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
2135 lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
2136   for m x y :: int
2137   by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
2140 subsection \<open>Bezout's theorem\<close>
2142 text \<open>
2143   Function \<open>bezw\<close> returns a pair of witnesses to Bezout's theorem --
2144   see the theorems that follow the definition.
2145 \<close>
2147 fun bezw :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
2148   where "bezw x y =
2149     (if y = 0 then (1, 0)
2150      else
2151       (snd (bezw y (x mod y)),
2152        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
2154 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)"
2155   by simp
2157 lemma bezw_non_0:
2158   "y > 0 \<Longrightarrow> bezw x y =
2159     (snd (bezw y (x mod y)), fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
2160   by simp
2162 declare bezw.simps [simp del]
2164 lemma bezw_aux: "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
2165 proof (induct x y rule: gcd_nat_induct)
2166   fix m :: nat
2167   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
2168     by auto
2169 next
2170   fix m n :: nat
2171   assume ngt0: "n > 0"
2172     and ih: "fst (bezw n (m mod n)) * int n + snd (bezw n (m mod n)) * int (m mod n) =
2173       int (gcd n (m mod n))"
2174   then show "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
2175     apply (simp add: bezw_non_0 gcd_non_0_nat)
2176     apply (erule subst)
2177     apply (simp add: field_simps)
2178     apply (subst div_mult_mod_eq [of m n, symmetric])
2179       (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *)
2180     apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
2181     done
2182 qed
2184 lemma bezout_int: "\<exists>u v. u * x + v * y = gcd x y"
2185   for x y :: int
2186 proof -
2187   have aux: "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> \<exists>u v. u * x + v * y = gcd x y" for x y :: int
2188     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
2189     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
2190     apply (unfold gcd_int_def)
2191     apply simp
2192     apply (subst bezw_aux [symmetric])
2193     apply auto
2194     done
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     by atomize_elim auto
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       apply -
2205       apply (insert aux [of x "-y"])
2206       apply auto
2207       apply (rule_tac x = u in exI)
2208       apply (rule_tac x = "-v" in exI)
2209       apply (subst gcd_neg2_int [symmetric])
2210       apply auto
2211       done
2212   next
2213     case 3
2214     then show ?thesis
2215       apply -
2216       apply (insert aux [of "-x" y])
2217       apply auto
2218       apply (rule_tac x = "-u" in exI)
2219       apply (rule_tac x = v in exI)
2220       apply (subst gcd_neg1_int [symmetric])
2221       apply auto
2222       done
2223   next
2224     case 4
2225     then show ?thesis
2226       apply -
2227       apply (insert aux [of "-x" "-y"])
2228       apply auto
2229       apply (rule_tac x = "-u" in exI)
2230       apply (rule_tac x = "-v" in exI)
2231       apply (subst gcd_neg1_int [symmetric])
2232       apply (subst gcd_neg2_int [symmetric])
2233       apply auto
2234       done
2235   qed
2236 qed
2239 text \<open>Versions of Bezout for \<open>nat\<close>, by Amine Chaieb.\<close>
2241 lemma ind_euclid:
2242   fixes P :: "nat \<Rightarrow> nat \<Rightarrow> bool"
2243   assumes c: " \<forall>a b. P a b \<longleftrightarrow> P b a"
2244     and z: "\<forall>a. P a 0"
2245     and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
2246   shows "P a b"
2247 proof (induct "a + b" arbitrary: a b rule: less_induct)
2248   case less
2249   consider (eq) "a = b" | (lt) "a < b" "a + b - a < a + b" | "b = 0" | "b + a - b < a + b"
2250     by arith
2251   show ?case
2252   proof (cases a b rule: linorder_cases)
2253     case equal
2254     with add [rule_format, OF z [rule_format, of a]] show ?thesis by simp
2255   next
2256     case lt: less
2257     then consider "a = 0" | "a + b - a < a + b" by arith
2258     then show ?thesis
2259     proof cases
2260       case 1
2261       with z c show ?thesis by blast
2262     next
2263       case 2
2264       also have *: "a + b - a = a + (b - a)" using lt by arith
2265       finally have "a + (b - a) < a + b" .
2266       then have "P a (a + (b - a))" by (rule add [rule_format, OF less])
2267       then show ?thesis by (simp add: *[symmetric])
2268     qed
2269   next
2270     case gt: greater
2271     then consider "b = 0" | "b + a - b < a + b" by arith
2272     then show ?thesis
2273     proof cases
2274       case 1
2275       with z c show ?thesis by blast
2276     next
2277       case 2
2278       also have *: "b + a - b = b + (a - b)" using gt by arith
2279       finally have "b + (a - b) < a + b" .
2280       then have "P b (b + (a - b))" by (rule add [rule_format, OF less])
2281       then have "P b a" by (simp add: *[symmetric])
2282       with c show ?thesis by blast
2283     qed
2284   qed
2285 qed
2287 lemma bezout_lemma_nat:
2288   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
2289     (a * x = b * y + d \<or> b * x = a * y + d)"
2290   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
2291     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
2292   using ex
2293   apply clarsimp
2294   apply (rule_tac x="d" in exI)
2295   apply simp
2296   apply (case_tac "a * x = b * y + d")
2297    apply simp_all
2298    apply (rule_tac x="x + y" in exI)
2299    apply (rule_tac x="y" in exI)
2300    apply algebra
2301   apply (rule_tac x="x" in exI)
2302   apply (rule_tac x="x + y" in exI)
2303   apply algebra
2304   done
2306 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
2307     (a * x = b * y + d \<or> b * x = a * y + d)"
2308   apply (induct a b rule: ind_euclid)
2309     apply blast
2310    apply clarify
2311    apply (rule_tac x="a" in exI)
2312    apply simp
2313   apply clarsimp
2314   apply (rule_tac x="d" in exI)
2315   apply (case_tac "a * x = b * y + d")
2316    apply simp_all
2317    apply (rule_tac x="x+y" in exI)
2318    apply (rule_tac x="y" in exI)
2319    apply algebra
2320   apply (rule_tac x="x" in exI)
2321   apply (rule_tac x="x+y" in exI)
2322   apply algebra
2323   done
2325 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
2326     (a * x - b * y = d \<or> b * x - a * y = d)"
2327   using bezout_add_nat[of a b]
2328   apply clarsimp
2329   apply (rule_tac x="d" in exI)
2330   apply simp
2331   apply (rule_tac x="x" in exI)
2332   apply (rule_tac x="y" in exI)
2333   apply auto
2334   done
2337   fixes a b :: nat
2338   assumes a: "a \<noteq> 0"
2339   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
2340 proof -
2341   consider d x y where "d dvd a" "d dvd b" "a * x = b * y + d"
2342     | d x y where "d dvd a" "d dvd b" "b * x = a * y + d"
2343     using bezout_add_nat [of a b] by blast
2344   then show ?thesis
2345   proof cases
2346     case 1
2347     then show ?thesis by blast
2348   next
2349     case H: 2
2350     show ?thesis
2351     proof (cases "b = 0")
2352       case True
2353       with H show ?thesis by simp
2354     next
2355       case False
2356       then have bp: "b > 0" by simp
2357       with dvd_imp_le [OF H(2)] consider "d = b" | "d < b"
2358         by atomize_elim auto
2359       then show ?thesis
2360       proof cases
2361         case 1
2362         with a H show ?thesis
2363           apply simp
2364           apply (rule exI[where x = b])
2365           apply simp
2366           apply (rule exI[where x = b])
2367           apply (rule exI[where x = "a - 1"])
2368           apply (simp add: diff_mult_distrib2)
2369           done
2370       next
2371         case 2
2372         show ?thesis
2373         proof (cases "x = 0")
2374           case True
2375           with a H show ?thesis by simp
2376         next
2377           case x0: False
2378           then have xp: "x > 0" by simp
2379           from \<open>d < b\<close> have "d \<le> b - 1" by simp
2380           then have "d * b \<le> b * (b - 1)" by simp
2381           with xp mult_mono[of "1" "x" "d * b" "b * (b - 1)"]
2382           have dble: "d * b \<le> x * b * (b - 1)" using bp by simp
2383           from H(3) have "d + (b - 1) * (b * x) = d + (b - 1) * (a * y + d)"
2384             by simp
2385           then have "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
2386             by (simp only: mult.assoc distrib_left)
2387           then have "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x * b * (b - 1)"
2388             by algebra
2389           then have "a * ((b - 1) * y) = d + x * b * (b - 1) - d * b"
2390             using bp by simp
2391           then have "a * ((b - 1) * y) = d + (x * b * (b - 1) - d * b)"
2392             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
2393           then have "a * ((b - 1) * y) = b * (x * (b - 1) - d) + d"
2394             by (simp only: diff_mult_distrib2 ac_simps)
2395           with H(1,2) show ?thesis
2396             apply -
2397             apply (rule exI [where x = d])
2398             apply simp
2399             apply (rule exI [where x = "(b - 1) * y"])
2400             apply (rule exI [where x = "x * (b - 1) - d"])
2401             apply simp
2402             done
2403         qed
2404       qed
2405     qed
2406   qed
2407 qed
2409 lemma bezout_nat:
2410   fixes a :: nat
2411   assumes a: "a \<noteq> 0"
2412   shows "\<exists>x y. a * x = b * y + gcd a b"
2413 proof -
2414   obtain d x y where d: "d dvd a" "d dvd b" and eq: "a * x = b * y + d"
2415     using bezout_add_strong_nat [OF a, of b] by blast
2416   from d have "d dvd gcd a b"
2417     by simp
2418   then obtain k where k: "gcd a b = d * k"
2419     unfolding dvd_def by blast
2420   from eq have "a * x * k = (b * y + d) * k"
2421     by auto
2422   then have "a * (x * k) = b * (y * k) + gcd a b"
2423     by (algebra add: k)
2424   then show ?thesis
2425     by blast
2426 qed
2429 subsection \<open>LCM properties on @{typ nat} and @{typ int}\<close>
2431 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
2432   for a b :: int
2433   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
2435 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
2436   for m n :: nat
2437   unfolding lcm_nat_def
2438   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
2440 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
2441   for m n :: int
2442   unfolding lcm_int_def gcd_int_def
2443   apply (subst of_nat_mult [symmetric])
2444   apply (subst prod_gcd_lcm_nat [symmetric])
2445   apply (subst nat_abs_mult_distrib [symmetric])
2446   apply (simp add: abs_mult)
2447   done
2449 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
2450   for m n :: nat
2451   by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
2453 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
2454   for m n :: int
2455   apply (subst lcm_abs_int)
2456   apply (rule lcm_pos_nat [transferred])
2457      apply auto
2458   done
2460 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
2461   for m n :: nat
2462   by (cases m) auto
2464 lemma lcm_unique_nat:
2465   "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"
2466   for a b d :: nat
2467   by (auto intro: dvd_antisym lcm_least)
2469 lemma lcm_unique_int:
2470   "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"
2471   for a b d :: int
2472   using lcm_least zdvd_antisym_nonneg by auto
2474 lemma lcm_proj2_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm x y = y"
2475   for x y :: nat
2476   apply (rule sym)
2477   apply (subst lcm_unique_nat [symmetric])
2478   apply auto
2479   done
2481 lemma lcm_proj2_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
2482   for x y :: int
2483   apply (rule sym)
2484   apply (subst lcm_unique_int [symmetric])
2485   apply auto
2486   done
2488 lemma lcm_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> lcm y x = y"
2489   for x y :: nat
2490   by (subst lcm.commute) (erule lcm_proj2_if_dvd_nat)
2492 lemma lcm_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
2493   for x y :: int
2494   by (subst lcm.commute) (erule lcm_proj2_if_dvd_int)
2496 lemma lcm_proj1_iff_nat [simp]: "lcm m n = m \<longleftrightarrow> n dvd m"
2497   for m n :: nat
2498   by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
2500 lemma lcm_proj2_iff_nat [simp]: "lcm m n = n \<longleftrightarrow> m dvd n"
2501   for m n :: nat
2502   by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
2504 lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m\<bar> \<longleftrightarrow> n dvd m"
2505   for m n :: int
2506   by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
2508 lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n\<bar> \<longleftrightarrow> m dvd n"
2509   for m n :: int
2510   by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
2512 lemma lcm_1_iff_nat [simp]: "lcm m n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
2513   for m n :: nat
2514   using lcm_eq_1_iff [of m n] by simp
2516 lemma lcm_1_iff_int [simp]: "lcm m n = 1 \<longleftrightarrow> (m = 1 \<or> m = -1) \<and> (n = 1 \<or> n = -1)"
2517   for m n :: int
2518   by auto
2521 subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
2523 text \<open>
2524   Lifting \<open>gcd\<close> and \<open>lcm\<close> to sets (\<open>Gcd\<close> / \<open>Lcm\<close>).
2525   \<open>Gcd\<close> is defined via \<open>Lcm\<close> to facilitate the proof that we have a complete lattice.
2526 \<close>
2528 instantiation nat :: semiring_Gcd
2529 begin
2531 interpretation semilattice_neutr_set lcm "1::nat"
2532   by standard simp_all
2534 definition "Lcm M = (if finite M then F M else 0)" for M :: "nat set"
2536 lemma Lcm_nat_empty: "Lcm {} = (1::nat)"
2537   by (simp add: Lcm_nat_def del: One_nat_def)
2539 lemma Lcm_nat_insert: "Lcm (insert n M) = lcm n (Lcm M)" for n :: nat
2540   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
2542 lemma Lcm_nat_infinite: "infinite M \<Longrightarrow> Lcm M = 0" for M :: "nat set"
2543   by (simp add: Lcm_nat_def)
2545 lemma dvd_Lcm_nat [simp]:
2546   fixes M :: "nat set"
2547   assumes "m \<in> M"
2548   shows "m dvd Lcm M"
2549 proof -
2550   from assms have "insert m M = M"
2551     by auto
2552   moreover have "m dvd Lcm (insert m M)"
2553     by (simp add: Lcm_nat_insert)
2554   ultimately show ?thesis
2555     by simp
2556 qed
2558 lemma Lcm_dvd_nat [simp]:
2559   fixes M :: "nat set"
2560   assumes "\<forall>m\<in>M. m dvd n"
2561   shows "Lcm M dvd n"
2562 proof (cases "n > 0")
2563   case False
2564   then show ?thesis by simp
2565 next
2566   case True
2567   then have "finite {d. d dvd n}"
2568     by (rule finite_divisors_nat)
2569   moreover have "M \<subseteq> {d. d dvd n}"
2570     using assms by fast
2571   ultimately have "finite M"
2572     by (rule rev_finite_subset)
2573   then show ?thesis
2574     using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
2575 qed
2577 definition "Gcd M = Lcm {d. \<forall>m\<in>M. d dvd m}" for M :: "nat set"
2579 instance
2580 proof
2581   fix N :: "nat set"
2582   fix n :: nat
2583   show "Gcd N dvd n" if "n \<in> N"
2584     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
2585   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m"
2586     using that by (induct N rule: infinite_finite_induct) (auto simp add: Gcd_nat_def)
2587   show "n dvd Lcm N" if "n \<in> N"
2588     using that by (induct N rule: infinite_finite_induct) auto
2589   show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n"
2590     using that by (induct N rule: infinite_finite_induct) auto
2591   show "normalize (Gcd N) = Gcd N" and "normalize (Lcm N) = Lcm N"
2592     by simp_all
2593 qed
2595 end
2597 lemma Gcd_nat_eq_one: "1 \<in> N \<Longrightarrow> Gcd N = 1"
2598   for N :: "nat set"
2599   by (rule Gcd_eq_1_I) auto
2602 text \<open>Alternative characterizations of Gcd:\<close>
2604 lemma Gcd_eq_Max:
2605   fixes M :: "nat set"
2606   assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
2607   shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
2608 proof (rule antisym)
2609   from assms obtain m where "m \<in> M" and "m > 0"
2610     by auto
2611   from \<open>m > 0\<close> have "finite {d. d dvd m}"
2612     by (blast intro: finite_divisors_nat)
2613   with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
2614     by blast
2615   from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
2616     by (auto intro: Max_ge Gcd_dvd)
2617   from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
2618     apply (rule Max.boundedI)
2619      apply auto
2620     apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
2621     done
2622 qed
2624 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0})"
2625   for M :: "nat set"
2626   apply (induct pred: finite)
2627    apply simp
2628   apply (case_tac "x = 0")
2629    apply simp
2630   apply (subgoal_tac "insert x F - {0} = insert x (F - {0})")
2631    apply simp
2632   apply blast
2633   done
2635 lemma Lcm_in_lcm_closed_set_nat:
2636   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M \<in> M"
2637   for M :: "nat set"
2638   apply (induct rule: finite_linorder_min_induct)
2639    apply simp
2640   apply simp
2641   apply (subgoal_tac "\<forall>m n. m \<in> A \<longrightarrow> n \<in> A \<longrightarrow> lcm m n \<in> A")
2642    apply simp
2643    apply(case_tac "A = {}")
2644     apply simp
2645    apply simp
2646   apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
2647   done
2649 lemma Lcm_eq_Max_nat:
2650   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> \<forall>m n. m \<in> M \<longrightarrow> n \<in> M \<longrightarrow> lcm m n \<in> M \<Longrightarrow> Lcm M = Max M"
2651   for M :: "nat set"
2652   apply (rule antisym)
2653    apply (rule Max_ge)
2654     apply assumption
2655    apply (erule (2) Lcm_in_lcm_closed_set_nat)
2656   apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
2657   done
2659 lemma mult_inj_if_coprime_nat:
2660   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. coprime (f a) (g b) \<Longrightarrow>
2661     inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
2662   for f :: "'a \<Rightarrow> nat" and g :: "'b \<Rightarrow> nat"
2663   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
2666 subsubsection \<open>Setwise GCD and LCM for integers\<close>
2668 instantiation int :: semiring_Gcd
2669 begin
2671 definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
2673 definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
2675 instance
2676   by standard
2677     (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
2678       Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
2680 end
2682 lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
2683   for K :: "int set"
2684   using normalize_Gcd [of K] by simp
2686 lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
2687   for K :: "int set"
2688   using normalize_Lcm [of K] by simp
2690 lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
2691   by (simp add: Gcd_int_def comp_def image_image)
2693 lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
2694   by (simp add: Lcm_int_def comp_def image_image)
2697 subsection \<open>GCD and LCM on @{typ integer}\<close>
2699 instantiation integer :: gcd
2700 begin
2702 context
2703   includes integer.lifting
2704 begin
2706 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
2708 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
2710 end
2712 instance ..
2714 end
2716 lifting_update integer.lifting
2717 lifting_forget integer.lifting
2719 context
2720   includes integer.lifting
2721 begin
2723 lemma 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>"
2724   by transfer (fact gcd_code_int)
2726 lemma lcm_code_integer [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
2727   for a b :: integer
2728   by transfer (fact lcm_altdef_int)
2730 end
2732 code_printing
2733   constant "gcd :: integer \<Rightarrow> _" \<rightharpoonup>
2734     (OCaml) "Big'_int.gcd'_big'_int"
2735   and (Haskell) "Prelude.gcd"
2736   and (Scala) "_.gcd'((_)')"
2737   \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
2739 text \<open>Some code equations\<close>
2741 lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
2742 lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
2743 lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
2744 lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
2746 text \<open>Fact aliases.\<close>
2748 lemma lcm_0_iff_nat [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
2749   for m n :: nat
2750   by (fact lcm_eq_0_iff)
2752 lemma lcm_0_iff_int [simp]: "lcm m n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
2753   for m n :: int
2754   by (fact lcm_eq_0_iff)
2756 lemma dvd_lcm_I1_nat [simp]: "k dvd m \<Longrightarrow> k dvd lcm m n"
2757   for k m n :: nat
2758   by (fact dvd_lcmI1)
2760 lemma dvd_lcm_I2_nat [simp]: "k dvd n \<Longrightarrow> k dvd lcm m n"
2761   for k m n :: nat
2762   by (fact dvd_lcmI2)
2764 lemma dvd_lcm_I1_int [simp]: "i dvd m \<Longrightarrow> i dvd lcm m n"
2765   for i m n :: int
2766   by (fact dvd_lcmI1)
2768 lemma dvd_lcm_I2_int [simp]: "i dvd n \<Longrightarrow> i dvd lcm m n"
2769   for i m n :: int
2770   by (fact dvd_lcmI2)
2772 lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
2773   for a b :: nat
2774   by (fact coprime_exp2)
2776 lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
2777   for a b :: int
2778   by (fact coprime_exp2)
2780 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
2781 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
2782 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
2783 lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
2785 lemma dvd_Lcm_int [simp]: "m \<in> M \<Longrightarrow> m dvd Lcm M"
2786   for M :: "int set"
2787   by (fact dvd_Lcm)
2789 lemma gcd_neg_numeral_1_int [simp]: "gcd (- numeral n :: int) x = gcd (numeral n) x"
2790   by (fact gcd_neg1_int)
2792 lemma gcd_neg_numeral_2_int [simp]: "gcd x (- numeral n :: int) = gcd x (numeral n)"
2793   by (fact gcd_neg2_int)
2795 lemma gcd_proj1_if_dvd_nat [simp]: "x dvd y \<Longrightarrow> gcd x y = x"
2796   for x y :: nat
2797   by (fact gcd_nat.absorb1)
2799 lemma gcd_proj2_if_dvd_nat [simp]: "y dvd x \<Longrightarrow> gcd x y = y"
2800   for x y :: nat
2801   by (fact gcd_nat.absorb2)
2803 lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
2804 lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
2805 lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
2807 end