src/HOL/GCD.thy
 author nipkow Sat Jun 20 13:34:54 2009 +0200 (2009-06-20) changeset 31730 d74830dc3e4a parent 31729 b9299916d618 child 31734 a4a79836d07b permissions -rw-r--r--
1 (*  Title:      GCD.thy
2     Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
3                 Thomas M. Rasmussen, Jeremy Avigad
6 This file deals with the functions gcd and lcm, and properties of
7 primes. Definitions and lemmas are proved uniformly for the natural
8 numbers and integers.
10 This file combines and revises a number of prior developments.
12 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
13 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
14 gcd, lcm, and prime for the natural numbers.
16 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
17 extended gcd, lcm, primes to the integers. Amine Chaieb provided
18 another extension of the notions to the integers, and added a number
19 of results to "Primes" and "GCD". IntPrimes also defined and developed
20 the congruence relations on the integers. The notion was extended to
21 the natural numbers by Chiaeb.
23 *)
28 theory GCD
29 imports NatTransfer
30 begin
32 declare One_nat_def [simp del]
34 subsection {* gcd *}
36 class gcd = one +
38 fixes
39   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
40   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
42 begin
44 abbreviation
45   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
46 where
47   "coprime x y == (gcd x y = 1)"
49 end
51 class prime = one +
53 fixes
54   prime :: "'a \<Rightarrow> bool"
57 (* definitions for the natural numbers *)
59 instantiation nat :: gcd
61 begin
63 fun
64   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
65 where
66   "gcd_nat x y =
67    (if y = 0 then x else gcd y (x mod y))"
69 definition
70   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
71 where
72   "lcm_nat x y = x * y div (gcd x y)"
74 instance proof qed
76 end
79 instantiation nat :: prime
81 begin
83 definition
84   prime_nat :: "nat \<Rightarrow> bool"
85 where
86   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
88 instance proof qed
90 end
93 (* definitions for the integers *)
95 instantiation int :: gcd
97 begin
99 definition
100   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
101 where
102   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
104 definition
105   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
106 where
107   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
109 instance proof qed
111 end
114 instantiation int :: prime
116 begin
118 definition
119   prime_int :: "int \<Rightarrow> bool"
120 where
121   [code del]: "prime_int p = prime (nat p)"
123 instance proof qed
125 end
128 subsection {* Set up Transfer *}
131 lemma transfer_nat_int_gcd:
132   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
133   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
134   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
135   unfolding gcd_int_def lcm_int_def prime_int_def
136   by auto
138 lemma transfer_nat_int_gcd_closures:
139   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
140   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
141   by (auto simp add: gcd_int_def lcm_int_def)
144     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
146 lemma transfer_int_nat_gcd:
147   "gcd (int x) (int y) = int (gcd x y)"
148   "lcm (int x) (int y) = int (lcm x y)"
149   "prime (int x) = prime x"
150   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
152 lemma transfer_int_nat_gcd_closures:
153   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
154   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
155   by (auto simp add: gcd_int_def lcm_int_def)
158     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
162 subsection {* GCD *}
164 (* was gcd_induct *)
165 lemma nat_gcd_induct:
166   fixes m n :: nat
167   assumes "\<And>m. P m 0"
168     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
169   shows "P m n"
170   apply (rule gcd_nat.induct)
171   apply (case_tac "y = 0")
172   using assms apply simp_all
173 done
175 (* specific to int *)
177 lemma int_gcd_neg1 [simp]: "gcd (-x::int) y = gcd x y"
180 lemma int_gcd_neg2 [simp]: "gcd (x::int) (-y) = gcd x y"
183 lemma int_gcd_abs: "gcd (x::int) y = gcd (abs x) (abs y)"
186 lemma int_gcd_cases:
187   fixes x :: int and y
188   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
189       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
190       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
191       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
192   shows "P (gcd x y)"
193 by (insert prems, auto simp add: int_gcd_neg1 int_gcd_neg2, arith)
195 lemma int_gcd_ge_0 [simp]: "gcd (x::int) y >= 0"
198 lemma int_lcm_neg1: "lcm (-x::int) y = lcm x y"
201 lemma int_lcm_neg2: "lcm (x::int) (-y) = lcm x y"
204 lemma int_lcm_abs: "lcm (x::int) y = lcm (abs x) (abs y)"
207 lemma int_lcm_cases:
208   fixes x :: int and y
209   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
210       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
211       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
212       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
213   shows "P (lcm x y)"
214 by (insert prems, auto simp add: int_lcm_neg1 int_lcm_neg2, arith)
216 lemma int_lcm_ge_0 [simp]: "lcm (x::int) y >= 0"
219 (* was gcd_0, etc. *)
220 lemma nat_gcd_0 [simp]: "gcd (x::nat) 0 = x"
221   by simp
223 (* was igcd_0, etc. *)
224 lemma int_gcd_0 [simp]: "gcd (x::int) 0 = abs x"
225   by (unfold gcd_int_def, auto)
227 lemma nat_gcd_0_left [simp]: "gcd 0 (x::nat) = x"
228   by simp
230 lemma int_gcd_0_left [simp]: "gcd 0 (x::int) = abs x"
231   by (unfold gcd_int_def, auto)
233 lemma nat_gcd_red: "gcd (x::nat) y = gcd y (x mod y)"
234   by (case_tac "y = 0", auto)
236 (* weaker, but useful for the simplifier *)
238 lemma nat_gcd_non_0: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
239   by simp
241 lemma nat_gcd_1 [simp]: "gcd (m::nat) 1 = 1"
242   by simp
244 lemma nat_gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
247 lemma int_gcd_1 [simp]: "gcd (m::int) 1 = 1"
250 lemma nat_gcd_self [simp]: "gcd (x::nat) x = x"
251   by simp
253 lemma int_gcd_def [simp]: "gcd (x::int) x = abs x"
254   by (subst int_gcd_abs, auto simp add: gcd_int_def)
256 declare gcd_nat.simps [simp del]
258 text {*
259   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
260   conjunctions don't seem provable separately.
261 *}
263 lemma nat_gcd_dvd1 [iff]: "(gcd (m::nat)) n dvd m"
264   and nat_gcd_dvd2 [iff]: "(gcd m n) dvd n"
265   apply (induct m n rule: nat_gcd_induct)
267   apply (blast dest: dvd_mod_imp_dvd)
268 done
270 thm nat_gcd_dvd1 [transferred]
272 lemma int_gcd_dvd1 [iff]: "gcd (x::int) y dvd x"
273   apply (subst int_gcd_abs)
274   apply (rule dvd_trans)
275   apply (rule nat_gcd_dvd1 [transferred])
276   apply auto
277 done
279 lemma int_gcd_dvd2 [iff]: "gcd (x::int) y dvd y"
280   apply (subst int_gcd_abs)
281   apply (rule dvd_trans)
282   apply (rule nat_gcd_dvd2 [transferred])
283   apply auto
284 done
286 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
287 by(metis nat_gcd_dvd1 dvd_trans)
289 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
290 by(metis nat_gcd_dvd2 dvd_trans)
292 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
293 by(metis int_gcd_dvd1 dvd_trans)
295 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
296 by(metis int_gcd_dvd2 dvd_trans)
298 lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
299   by (rule dvd_imp_le, auto)
301 lemma nat_gcd_le2 [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
302   by (rule dvd_imp_le, auto)
304 lemma int_gcd_le1 [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
305   by (rule zdvd_imp_le, auto)
307 lemma int_gcd_le2 [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
308   by (rule zdvd_imp_le, auto)
310 lemma nat_gcd_greatest: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
311   by (induct m n rule: nat_gcd_induct) (simp_all add: nat_gcd_non_0 dvd_mod)
313 lemma int_gcd_greatest:
314   assumes "(k::int) dvd m" and "k dvd n"
315   shows "k dvd gcd m n"
317   apply (subst int_gcd_abs)
318   apply (subst abs_dvd_iff [symmetric])
319   apply (rule nat_gcd_greatest [transferred])
320   using prems apply auto
321 done
323 lemma nat_gcd_greatest_iff [iff]: "(k dvd gcd (m::nat) n) =
324     (k dvd m & k dvd n)"
325   by (blast intro!: nat_gcd_greatest intro: dvd_trans)
327 lemma int_gcd_greatest_iff: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
328   by (blast intro!: int_gcd_greatest intro: dvd_trans)
330 lemma nat_gcd_zero [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
331   by (simp only: dvd_0_left_iff [symmetric] nat_gcd_greatest_iff)
333 lemma int_gcd_zero [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
334   by (auto simp add: gcd_int_def)
336 lemma nat_gcd_pos [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
337   by (insert nat_gcd_zero [of m n], arith)
339 lemma int_gcd_pos [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
340   by (insert int_gcd_zero [of m n], insert int_gcd_ge_0 [of m n], arith)
342 lemma nat_gcd_commute: "gcd (m::nat) n = gcd n m"
343   by (rule dvd_anti_sym, auto)
345 lemma int_gcd_commute: "gcd (m::int) n = gcd n m"
346   by (auto simp add: gcd_int_def nat_gcd_commute)
348 lemma nat_gcd_assoc: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
349   apply (rule dvd_anti_sym)
350   apply (blast intro: dvd_trans)+
351 done
353 lemma int_gcd_assoc: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
354   by (auto simp add: gcd_int_def nat_gcd_assoc)
356 lemma nat_gcd_left_commute: "gcd (k::nat) (gcd m n) = gcd m (gcd k n)"
357   apply (rule nat_gcd_commute [THEN trans])
358   apply (rule nat_gcd_assoc [THEN trans])
359   apply (rule nat_gcd_commute [THEN arg_cong])
360 done
362 lemma int_gcd_left_commute: "gcd (k::int) (gcd m n) = gcd m (gcd k n)"
363   apply (rule int_gcd_commute [THEN trans])
364   apply (rule int_gcd_assoc [THEN trans])
365   apply (rule int_gcd_commute [THEN arg_cong])
366 done
368 lemmas nat_gcd_ac = nat_gcd_assoc nat_gcd_commute nat_gcd_left_commute
369   -- {* gcd is an AC-operator *}
371 lemmas int_gcd_ac = int_gcd_assoc int_gcd_commute int_gcd_left_commute
373 lemma nat_gcd_1_left [simp]: "gcd (1::nat) m = 1"
374   by (subst nat_gcd_commute, simp)
376 lemma nat_gcd_Suc_0_left [simp]: "gcd (Suc 0) m = Suc 0"
377   by (subst nat_gcd_commute, simp add: One_nat_def)
379 lemma int_gcd_1_left [simp]: "gcd (1::int) m = 1"
380   by (subst int_gcd_commute, simp)
382 lemma nat_gcd_unique: "(d::nat) dvd a \<and> d dvd b \<and>
383     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
384   apply auto
385   apply (rule dvd_anti_sym)
386   apply (erule (1) nat_gcd_greatest)
387   apply auto
388 done
390 lemma int_gcd_unique: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
391     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
392   apply (case_tac "d = 0")
393   apply force
394   apply (rule iffI)
395   apply (rule zdvd_anti_sym)
396   apply arith
397   apply (subst int_gcd_pos)
398   apply clarsimp
399   apply (drule_tac x = "d + 1" in spec)
400   apply (frule zdvd_imp_le)
401   apply (auto intro: int_gcd_greatest)
402 done
404 text {*
405   \medskip Multiplication laws
406 *}
408 lemma nat_gcd_mult_distrib: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
409     -- {* \cite[page 27]{davenport92} *}
410   apply (induct m n rule: nat_gcd_induct)
411   apply simp
412   apply (case_tac "k = 0")
413   apply (simp_all add: mod_geq nat_gcd_non_0 mod_mult_distrib2)
414 done
416 lemma int_gcd_mult_distrib: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
417   apply (subst (1 2) int_gcd_abs)
419   apply (rule nat_gcd_mult_distrib [transferred])
420   apply auto
421 done
423 lemma nat_gcd_mult [simp]: "gcd (k::nat) (k * n) = k"
424   by (rule nat_gcd_mult_distrib [of k 1 n, simplified, symmetric])
426 lemma int_gcd_mult [simp]: "gcd (k::int) (k * n) = abs k"
427   by (rule int_gcd_mult_distrib [of k 1 n, simplified, symmetric])
429 lemma nat_coprime_dvd_mult: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
430   apply (insert nat_gcd_mult_distrib [of m k n])
431   apply simp
432   apply (erule_tac t = m in ssubst)
433   apply simp
434   done
436 lemma int_coprime_dvd_mult:
437   assumes "coprime (k::int) n" and "k dvd m * n"
438   shows "k dvd m"
440   using prems
441   apply (subst abs_dvd_iff [symmetric])
442   apply (subst dvd_abs_iff [symmetric])
443   apply (subst (asm) int_gcd_abs)
444   apply (rule nat_coprime_dvd_mult [transferred])
445   apply auto
446   apply (subst abs_mult [symmetric], auto)
447 done
449 lemma nat_coprime_dvd_mult_iff: "coprime (k::nat) n \<Longrightarrow>
450     (k dvd m * n) = (k dvd m)"
451   by (auto intro: nat_coprime_dvd_mult)
453 lemma int_coprime_dvd_mult_iff: "coprime (k::int) n \<Longrightarrow>
454     (k dvd m * n) = (k dvd m)"
455   by (auto intro: int_coprime_dvd_mult)
457 lemma nat_gcd_mult_cancel: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
458   apply (rule dvd_anti_sym)
459   apply (rule nat_gcd_greatest)
460   apply (rule_tac n = k in nat_coprime_dvd_mult)
464 done
466 lemma int_gcd_mult_cancel:
467   assumes "coprime (k::int) n"
468   shows "gcd (k * m) n = gcd m n"
470   using prems
471   apply (subst (1 2) int_gcd_abs)
472   apply (subst abs_mult)
473   apply (rule nat_gcd_mult_cancel [transferred])
474   apply (auto simp add: int_gcd_abs [symmetric])
475 done
477 text {* \medskip Addition laws *}
479 lemma nat_gcd_add1 [simp]: "gcd ((m::nat) + n) n = gcd m n"
480   apply (case_tac "n = 0")
482 done
484 lemma nat_gcd_add2 [simp]: "gcd (m::nat) (m + n) = gcd m n"
485   apply (subst (1 2) nat_gcd_commute)
487   apply simp
488 done
490 (* to do: add the other variations? *)
492 lemma nat_gcd_diff1: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
493   by (subst nat_gcd_add1 [symmetric], auto)
495 lemma nat_gcd_diff2: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
496   apply (subst nat_gcd_commute)
497   apply (subst nat_gcd_diff1 [symmetric])
498   apply auto
499   apply (subst nat_gcd_commute)
500   apply (subst nat_gcd_diff1)
501   apply assumption
502   apply (rule nat_gcd_commute)
503 done
505 lemma int_gcd_non_0: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
506   apply (frule_tac b = y and a = x in pos_mod_sign)
507   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
508   apply (auto simp add: nat_gcd_non_0 nat_mod_distrib [symmetric]
509     zmod_zminus1_eq_if)
510   apply (frule_tac a = x in pos_mod_bound)
511   apply (subst (1 2) nat_gcd_commute)
512   apply (simp del: pos_mod_bound add: nat_diff_distrib nat_gcd_diff2
513     nat_le_eq_zle)
514 done
516 lemma int_gcd_red: "gcd (x::int) y = gcd y (x mod y)"
517   apply (case_tac "y = 0")
518   apply force
519   apply (case_tac "y > 0")
520   apply (subst int_gcd_non_0, auto)
521   apply (insert int_gcd_non_0 [of "-y" "-x"])
522   apply (auto simp add: int_gcd_neg1 int_gcd_neg2)
523 done
525 lemma int_gcd_add1 [simp]: "gcd ((m::int) + n) n = gcd m n"
526   apply (case_tac "n = 0", force)
527   apply (subst (1 2) int_gcd_red)
528   apply auto
529 done
531 lemma int_gcd_add2 [simp]: "gcd m ((m::int) + n) = gcd m n"
532   apply (subst int_gcd_commute)
535   apply (subst int_gcd_commute)
536   apply (rule refl)
537 done
539 lemma nat_gcd_add_mult: "gcd (m::nat) (k * m + n) = gcd m n"
540   by (induct k, simp_all add: ring_simps)
542 lemma int_gcd_add_mult: "gcd (m::int) (k * m + n) = gcd m n"
543   apply (subgoal_tac "ALL s. ALL m. ALL n.
544       gcd m (int (s::nat) * m + n) = gcd m n")
545   apply (case_tac "k >= 0")
546   apply (drule_tac x = "nat k" in spec, force)
547   apply (subst (1 2) int_gcd_neg2 [symmetric])
548   apply (drule_tac x = "nat (- k)" in spec)
549   apply (drule_tac x = "m" in spec)
550   apply (drule_tac x = "-n" in spec)
551   apply auto
552   apply (rule nat_induct)
553   apply auto
554   apply (auto simp add: left_distrib)
556   apply simp
557 done
559 (* to do: differences, and all variations of addition rules
560     as simplification rules for nat and int *)
562 lemma nat_gcd_dvd_prod [iff]: "gcd (m::nat) n dvd k * n"
563   using mult_dvd_mono [of 1] by auto
565 (* to do: add the three variations of these, and for ints? *)
568 subsection {* Coprimality *}
570 lemma nat_div_gcd_coprime [intro]:
571   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
572   shows "coprime (a div gcd a b) (b div gcd a b)"
573 proof -
574   let ?g = "gcd a b"
575   let ?a' = "a div ?g"
576   let ?b' = "b div ?g"
577   let ?g' = "gcd ?a' ?b'"
578   have dvdg: "?g dvd a" "?g dvd b" by simp_all
579   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
580   from dvdg dvdg' obtain ka kb ka' kb' where
581       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
582     unfolding dvd_def by blast
583   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
584     by simp_all
585   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
586     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
587       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
588   have "?g \<noteq> 0" using nz by (simp add: nat_gcd_zero)
589   then have gp: "?g > 0" by arith
590   from nat_gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
591   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
592 qed
594 lemma int_div_gcd_coprime [intro]:
595   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
596   shows "coprime (a div gcd a b) (b div gcd a b)"
598   apply (subst (1 2 3) int_gcd_abs)
599   apply (subst (1 2) abs_div)
600   apply auto
601   prefer 3
602   apply (rule nat_div_gcd_coprime [transferred])
603   using nz apply (auto simp add: int_gcd_abs [symmetric])
604 done
606 lemma nat_coprime: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
607   using nat_gcd_unique[of 1 a b, simplified] by auto
609 lemma nat_coprime_Suc_0:
610     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
611   using nat_coprime by (simp add: One_nat_def)
613 lemma int_coprime: "coprime (a::int) b \<longleftrightarrow>
614     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
615   using int_gcd_unique [of 1 a b]
616   apply clarsimp
617   apply (erule subst)
618   apply (rule iffI)
619   apply force
620   apply (drule_tac x = "abs e" in exI)
621   apply (case_tac "e >= 0")
622   apply force
623   apply force
624 done
626 lemma nat_gcd_coprime:
627   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
628     b: "b = b' * gcd a b"
629   shows    "coprime a' b'"
631   apply (subgoal_tac "a' = a div gcd a b")
632   apply (erule ssubst)
633   apply (subgoal_tac "b' = b div gcd a b")
634   apply (erule ssubst)
635   apply (rule nat_div_gcd_coprime)
636   using prems
637   apply force
638   apply (subst (1) b)
639   using z apply force
640   apply (subst (1) a)
641   using z apply force
642 done
644 lemma int_gcd_coprime:
645   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
646     b: "b = b' * gcd a b"
647   shows    "coprime a' b'"
649   apply (subgoal_tac "a' = a div gcd a b")
650   apply (erule ssubst)
651   apply (subgoal_tac "b' = b div gcd a b")
652   apply (erule ssubst)
653   apply (rule int_div_gcd_coprime)
654   using prems
655   apply force
656   apply (subst (1) b)
657   using z apply force
658   apply (subst (1) a)
659   using z apply force
660 done
662 lemma nat_coprime_mult: assumes da: "coprime (d::nat) a" and db: "coprime d b"
663     shows "coprime d (a * b)"
664   apply (subst nat_gcd_commute)
665   using da apply (subst nat_gcd_mult_cancel)
666   apply (subst nat_gcd_commute, assumption)
667   apply (subst nat_gcd_commute, rule db)
668 done
670 lemma int_coprime_mult: assumes da: "coprime (d::int) a" and db: "coprime d b"
671     shows "coprime d (a * b)"
672   apply (subst int_gcd_commute)
673   using da apply (subst int_gcd_mult_cancel)
674   apply (subst int_gcd_commute, assumption)
675   apply (subst int_gcd_commute, rule db)
676 done
678 lemma nat_coprime_lmult:
679   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
680 proof -
681   have "gcd d a dvd gcd d (a * b)"
682     by (rule nat_gcd_greatest, auto)
683   with dab show ?thesis
684     by auto
685 qed
687 lemma int_coprime_lmult:
688   assumes dab: "coprime (d::int) (a * b)" shows "coprime d a"
689 proof -
690   have "gcd d a dvd gcd d (a * b)"
691     by (rule int_gcd_greatest, auto)
692   with dab show ?thesis
693     by auto
694 qed
696 lemma nat_coprime_rmult:
697   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d b"
698 proof -
699   have "gcd d b dvd gcd d (a * b)"
700     by (rule nat_gcd_greatest, auto intro: dvd_mult)
701   with dab show ?thesis
702     by auto
703 qed
705 lemma int_coprime_rmult:
706   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
707 proof -
708   have "gcd d b dvd gcd d (a * b)"
709     by (rule int_gcd_greatest, auto intro: dvd_mult)
710   with dab show ?thesis
711     by auto
712 qed
714 lemma nat_coprime_mul_eq: "coprime (d::nat) (a * b) \<longleftrightarrow>
715     coprime d a \<and>  coprime d b"
716   using nat_coprime_rmult[of d a b] nat_coprime_lmult[of d a b]
717     nat_coprime_mult[of d a b]
718   by blast
720 lemma int_coprime_mul_eq: "coprime (d::int) (a * b) \<longleftrightarrow>
721     coprime d a \<and>  coprime d b"
722   using int_coprime_rmult[of d a b] int_coprime_lmult[of d a b]
723     int_coprime_mult[of d a b]
724   by blast
726 lemma nat_gcd_coprime_exists:
727     assumes nz: "gcd (a::nat) b \<noteq> 0"
728     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
729   apply (rule_tac x = "a div gcd a b" in exI)
730   apply (rule_tac x = "b div gcd a b" in exI)
731   using nz apply (auto simp add: nat_div_gcd_coprime dvd_div_mult)
732 done
734 lemma int_gcd_coprime_exists:
735     assumes nz: "gcd (a::int) b \<noteq> 0"
736     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
737   apply (rule_tac x = "a div gcd a b" in exI)
738   apply (rule_tac x = "b div gcd a b" in exI)
739   using nz apply (auto simp add: int_div_gcd_coprime dvd_div_mult_self)
740 done
742 lemma nat_coprime_exp: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
743   by (induct n, simp_all add: nat_coprime_mult)
745 lemma int_coprime_exp: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
746   by (induct n, simp_all add: int_coprime_mult)
748 lemma nat_coprime_exp2 [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
749   apply (rule nat_coprime_exp)
750   apply (subst nat_gcd_commute)
751   apply (rule nat_coprime_exp)
752   apply (subst nat_gcd_commute, assumption)
753 done
755 lemma int_coprime_exp2 [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
756   apply (rule int_coprime_exp)
757   apply (subst int_gcd_commute)
758   apply (rule int_coprime_exp)
759   apply (subst int_gcd_commute, assumption)
760 done
762 lemma nat_gcd_exp: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
763 proof (cases)
764   assume "a = 0 & b = 0"
765   thus ?thesis by simp
766   next assume "~(a = 0 & b = 0)"
767   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
768     by auto
769   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
770       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
771     apply (subst (1 2) mult_commute)
772     apply (subst nat_gcd_mult_distrib [symmetric])
773     apply simp
774     done
775   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
776     apply (subst div_power)
777     apply auto
778     apply (rule dvd_div_mult_self)
779     apply (rule dvd_power_same)
780     apply auto
781     done
782   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
783     apply (subst div_power)
784     apply auto
785     apply (rule dvd_div_mult_self)
786     apply (rule dvd_power_same)
787     apply auto
788     done
789   finally show ?thesis .
790 qed
792 lemma int_gcd_exp: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
793   apply (subst (1 2) int_gcd_abs)
794   apply (subst (1 2) power_abs)
795   apply (rule nat_gcd_exp [where n = n, transferred])
796   apply auto
797 done
799 lemma nat_coprime_divprod: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
800   using nat_coprime_dvd_mult_iff[of d a b]
801   by (auto simp add: mult_commute)
803 lemma int_coprime_divprod: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
804   using int_coprime_dvd_mult_iff[of d a b]
805   by (auto simp add: mult_commute)
807 lemma nat_division_decomp: assumes dc: "(a::nat) dvd b * c"
808   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
809 proof-
810   let ?g = "gcd a b"
811   {assume "?g = 0" with dc have ?thesis by auto}
812   moreover
813   {assume z: "?g \<noteq> 0"
814     from nat_gcd_coprime_exists[OF z]
815     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
816       by blast
817     have thb: "?g dvd b" by auto
818     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
819     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
820     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
821     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
822     with z have th_1: "a' dvd b' * c" by auto
823     from nat_coprime_dvd_mult[OF ab'(3)] th_1
824     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
825     from ab' have "a = ?g*a'" by algebra
826     with thb thc have ?thesis by blast }
827   ultimately show ?thesis by blast
828 qed
830 lemma int_division_decomp: assumes dc: "(a::int) dvd b * c"
831   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
832 proof-
833   let ?g = "gcd a b"
834   {assume "?g = 0" with dc have ?thesis by auto}
835   moreover
836   {assume z: "?g \<noteq> 0"
837     from int_gcd_coprime_exists[OF z]
838     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
839       by blast
840     have thb: "?g dvd b" by auto
841     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
842     with dc have th0: "a' dvd b*c"
843       using dvd_trans[of a' a "b*c"] by simp
844     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
845     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
846     with z have th_1: "a' dvd b' * c" by auto
847     from int_coprime_dvd_mult[OF ab'(3)] th_1
848     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
849     from ab' have "a = ?g*a'" by algebra
850     with thb thc have ?thesis by blast }
851   ultimately show ?thesis by blast
852 qed
854 lemma nat_pow_divides_pow:
855   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
856   shows "a dvd b"
857 proof-
858   let ?g = "gcd a b"
859   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
860   {assume "?g = 0" with ab n have ?thesis by auto }
861   moreover
862   {assume z: "?g \<noteq> 0"
863     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
864     from nat_gcd_coprime_exists[OF z]
865     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
866       by blast
867     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
869     hence "?g^n*a'^n dvd ?g^n *b'^n"
870       by (simp only: power_mult_distrib mult_commute)
871     with zn z n have th0:"a'^n dvd b'^n" by auto
872     have "a' dvd a'^n" by (simp add: m)
873     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
874     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
875     from nat_coprime_dvd_mult[OF nat_coprime_exp [OF ab'(3), of m]] th1
876     have "a' dvd b'" by (subst (asm) mult_commute, blast)
877     hence "a'*?g dvd b'*?g" by simp
878     with ab'(1,2)  have ?thesis by simp }
879   ultimately show ?thesis by blast
880 qed
882 lemma int_pow_divides_pow:
883   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
884   shows "a dvd b"
885 proof-
886   let ?g = "gcd a b"
887   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
888   {assume "?g = 0" with ab n have ?thesis by auto }
889   moreover
890   {assume z: "?g \<noteq> 0"
891     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
892     from int_gcd_coprime_exists[OF z]
893     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
894       by blast
895     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
897     hence "?g^n*a'^n dvd ?g^n *b'^n"
898       by (simp only: power_mult_distrib mult_commute)
899     with zn z n have th0:"a'^n dvd b'^n" by auto
900     have "a' dvd a'^n" by (simp add: m)
901     with th0 have "a' dvd b'^n"
902       using dvd_trans[of a' "a'^n" "b'^n"] by simp
903     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
904     from int_coprime_dvd_mult[OF int_coprime_exp [OF ab'(3), of m]] th1
905     have "a' dvd b'" by (subst (asm) mult_commute, blast)
906     hence "a'*?g dvd b'*?g" by simp
907     with ab'(1,2)  have ?thesis by simp }
908   ultimately show ?thesis by blast
909 qed
911 lemma nat_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
912   by (auto intro: nat_pow_divides_pow dvd_power_same)
914 lemma int_pow_divides_eq [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
915   by (auto intro: int_pow_divides_pow dvd_power_same)
917 lemma nat_divides_mult:
918   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
919   shows "m * n dvd r"
920 proof-
921   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
922     unfolding dvd_def by blast
923   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
924   hence "m dvd n'" using nat_coprime_dvd_mult_iff[OF mn] by simp
925   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
926   from n' k show ?thesis unfolding dvd_def by auto
927 qed
929 lemma int_divides_mult:
930   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
931   shows "m * n dvd r"
932 proof-
933   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
934     unfolding dvd_def by blast
935   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
936   hence "m dvd n'" using int_coprime_dvd_mult_iff[OF mn] by simp
937   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
938   from n' k show ?thesis unfolding dvd_def by auto
939 qed
941 lemma nat_coprime_plus_one [simp]: "coprime ((n::nat) + 1) n"
942   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
943   apply force
944   apply (rule nat_dvd_diff)
945   apply auto
946 done
948 lemma nat_coprime_Suc [simp]: "coprime (Suc n) n"
949   using nat_coprime_plus_one by (simp add: One_nat_def)
951 lemma int_coprime_plus_one [simp]: "coprime ((n::int) + 1) n"
952   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
953   apply force
954   apply (rule dvd_diff)
955   apply auto
956 done
958 lemma nat_coprime_minus_one: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
959   using nat_coprime_plus_one [of "n - 1"]
960     nat_gcd_commute [of "n - 1" n] by auto
962 lemma int_coprime_minus_one: "coprime ((n::int) - 1) n"
963   using int_coprime_plus_one [of "n - 1"]
964     int_gcd_commute [of "n - 1" n] by auto
966 lemma nat_setprod_coprime [rule_format]:
967     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
968   apply (case_tac "finite A")
969   apply (induct set: finite)
970   apply (auto simp add: nat_gcd_mult_cancel)
971 done
973 lemma int_setprod_coprime [rule_format]:
974     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
975   apply (case_tac "finite A")
976   apply (induct set: finite)
977   apply (auto simp add: int_gcd_mult_cancel)
978 done
980 lemma nat_prime_odd: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
981   unfolding prime_nat_def
982   apply (subst even_mult_two_ex)
983   apply clarify
984   apply (drule_tac x = 2 in spec)
985   apply auto
986 done
988 lemma int_prime_odd: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
989   unfolding prime_int_def
990   apply (frule nat_prime_odd)
991   apply (auto simp add: even_nat_def)
992 done
994 lemma nat_coprime_common_divisor: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
995     x dvd b \<Longrightarrow> x = 1"
996   apply (subgoal_tac "x dvd gcd a b")
997   apply simp
998   apply (erule (1) nat_gcd_greatest)
999 done
1001 lemma int_coprime_common_divisor: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
1002     x dvd b \<Longrightarrow> abs x = 1"
1003   apply (subgoal_tac "x dvd gcd a b")
1004   apply simp
1005   apply (erule (1) int_gcd_greatest)
1006 done
1008 lemma nat_coprime_divisors: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
1009     coprime d e"
1010   apply (auto simp add: dvd_def)
1011   apply (frule int_coprime_lmult)
1012   apply (subst int_gcd_commute)
1013   apply (subst (asm) (2) int_gcd_commute)
1014   apply (erule int_coprime_lmult)
1015 done
1017 lemma nat_invertible_coprime: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
1018 apply (metis nat_coprime_lmult nat_gcd_1 nat_gcd_commute nat_gcd_red)
1019 done
1021 lemma int_invertible_coprime: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
1022 apply (metis int_coprime_lmult int_gcd_1 int_gcd_commute int_gcd_red)
1023 done
1026 subsection {* Bezout's theorem *}
1028 (* Function bezw returns a pair of witnesses to Bezout's theorem --
1029    see the theorems that follow the definition. *)
1030 fun
1031   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
1032 where
1033   "bezw x y =
1034   (if y = 0 then (1, 0) else
1035       (snd (bezw y (x mod y)),
1036        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
1038 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
1040 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
1041        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
1042   by simp
1044 declare bezw.simps [simp del]
1046 lemma bezw_aux [rule_format]:
1047     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
1048 proof (induct x y rule: nat_gcd_induct)
1049   fix m :: nat
1050   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
1051     by auto
1052   next fix m :: nat and n
1053     assume ngt0: "n > 0" and
1054       ih: "fst (bezw n (m mod n)) * int n +
1055         snd (bezw n (m mod n)) * int (m mod n) =
1056         int (gcd n (m mod n))"
1057     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
1058       apply (simp add: bezw_non_0 nat_gcd_non_0)
1059       apply (erule subst)
1061       apply (subst mod_div_equality [of m n, symmetric])
1062       (* applying simp here undoes the last substitution!
1063          what is procedure cancel_div_mod? *)
1064       apply (simp only: ring_simps zadd_int [symmetric]
1065         zmult_int [symmetric])
1066       done
1067 qed
1069 lemma int_bezout:
1070   fixes x y
1071   shows "EX u v. u * (x::int) + v * y = gcd x y"
1072 proof -
1073   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
1074       EX u v. u * x + v * y = gcd x y"
1075     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
1076     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
1077     apply (unfold gcd_int_def)
1078     apply simp
1079     apply (subst bezw_aux [symmetric])
1080     apply auto
1081     done
1082   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
1083       (x \<le> 0 \<and> y \<le> 0)"
1084     by auto
1085   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
1086     by (erule (1) bezout_aux)
1087   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
1088     apply (insert bezout_aux [of x "-y"])
1089     apply auto
1090     apply (rule_tac x = u in exI)
1091     apply (rule_tac x = "-v" in exI)
1092     apply (subst int_gcd_neg2 [symmetric])
1093     apply auto
1094     done
1095   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
1096     apply (insert bezout_aux [of "-x" y])
1097     apply auto
1098     apply (rule_tac x = "-u" in exI)
1099     apply (rule_tac x = v in exI)
1100     apply (subst int_gcd_neg1 [symmetric])
1101     apply auto
1102     done
1103   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
1104     apply (insert bezout_aux [of "-x" "-y"])
1105     apply auto
1106     apply (rule_tac x = "-u" in exI)
1107     apply (rule_tac x = "-v" in exI)
1108     apply (subst int_gcd_neg1 [symmetric])
1109     apply (subst int_gcd_neg2 [symmetric])
1110     apply auto
1111     done
1112   ultimately show ?thesis by blast
1113 qed
1115 text {* versions of Bezout for nat, by Amine Chaieb *}
1117 lemma ind_euclid:
1118   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
1119   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
1120   shows "P a b"
1121 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
1122   fix n a b
1123   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
1124   have "a = b \<or> a < b \<or> b < a" by arith
1125   moreover {assume eq: "a= b"
1126     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
1127     by simp}
1128   moreover
1129   {assume lt: "a < b"
1130     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
1131     moreover
1132     {assume "a =0" with z c have "P a b" by blast }
1133     moreover
1134     {assume ab: "a + b - a < n"
1135       have th0: "a + b - a = a + (b - a)" using lt by arith
1136       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
1137       have "P a b" by (simp add: th0[symmetric])}
1138     ultimately have "P a b" by blast}
1139   moreover
1140   {assume lt: "a > b"
1141     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
1142     moreover
1143     {assume "b =0" with z c have "P a b" by blast }
1144     moreover
1145     {assume ab: "b + a - b < n"
1146       have th0: "b + a - b = b + (a - b)" using lt by arith
1147       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
1148       have "P b a" by (simp add: th0[symmetric])
1149       hence "P a b" using c by blast }
1150     ultimately have "P a b" by blast}
1151 ultimately  show "P a b" by blast
1152 qed
1154 lemma nat_bezout_lemma:
1155   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1156     (a * x = b * y + d \<or> b * x = a * y + d)"
1157   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
1158     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
1159   using ex
1160   apply clarsimp
1162   apply (case_tac "a * x = b * y + d" , simp_all)
1163   apply (rule_tac x="x + y" in exI)
1164   apply (rule_tac x="y" in exI)
1165   apply algebra
1166   apply (rule_tac x="x" in exI)
1167   apply (rule_tac x="x + y" in exI)
1168   apply algebra
1169 done
1171 lemma nat_bezout_add: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1172     (a * x = b * y + d \<or> b * x = a * y + d)"
1173   apply(induct a b rule: ind_euclid)
1174   apply blast
1175   apply clarify
1177   apply clarsimp
1178   apply (rule_tac x="d" in exI)
1179   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
1180   apply (rule_tac x="x+y" in exI)
1181   apply (rule_tac x="y" in exI)
1182   apply algebra
1183   apply (rule_tac x="x" in exI)
1184   apply (rule_tac x="x+y" in exI)
1185   apply algebra
1186 done
1188 lemma nat_bezout1: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1189     (a * x - b * y = d \<or> b * x - a * y = d)"
1191   apply clarsimp
1192   apply (rule_tac x="d" in exI, simp)
1193   apply (rule_tac x="x" in exI)
1194   apply (rule_tac x="y" in exI)
1195   apply auto
1196 done
1198 lemma nat_bezout_add_strong: assumes nz: "a \<noteq> (0::nat)"
1199   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
1200 proof-
1201  from nz have ap: "a > 0" by simp
1203  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
1204    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
1205  moreover
1206     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
1207      from H have ?thesis by blast }
1208  moreover
1209  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
1210    {assume b0: "b = 0" with H  have ?thesis by simp}
1211    moreover
1212    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
1213      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
1214        by auto
1215      moreover
1216      {assume db: "d=b"
1217        from prems have ?thesis apply simp
1218 	 apply (rule exI[where x = b], simp)
1219 	 apply (rule exI[where x = b])
1220 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
1221     moreover
1222     {assume db: "d < b"
1223 	{assume "x=0" hence ?thesis  using prems by simp }
1224 	moreover
1225 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
1226 	  from db have "d \<le> b - 1" by simp
1227 	  hence "d*b \<le> b*(b - 1)" by simp
1228 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
1229 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
1230 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
1231             by simp
1232 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
1233 	    by (simp only: mult_assoc right_distrib)
1234 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
1235             by algebra
1236 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
1237 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
1238 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
1239 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
1240 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
1241 	  hence ?thesis using H(1,2)
1242 	    apply -
1243 	    apply (rule exI[where x=d], simp)
1244 	    apply (rule exI[where x="(b - 1) * y"])
1245 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
1246 	ultimately have ?thesis by blast}
1247     ultimately have ?thesis by blast}
1248   ultimately have ?thesis by blast}
1249  ultimately show ?thesis by blast
1250 qed
1252 lemma nat_bezout: assumes a: "(a::nat) \<noteq> 0"
1253   shows "\<exists>x y. a * x = b * y + gcd a b"
1254 proof-
1255   let ?g = "gcd a b"
1256   from nat_bezout_add_strong[OF a, of b]
1257   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
1258   from d(1,2) have "d dvd ?g" by simp
1259   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
1260   from d(3) have "a * x * k = (b * y + d) *k " by auto
1261   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
1262   thus ?thesis by blast
1263 qed
1266 subsection {* LCM *}
1268 lemma int_lcm_altdef: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1269   by (simp add: lcm_int_def lcm_nat_def zdiv_int
1270     zmult_int [symmetric] gcd_int_def)
1272 lemma nat_prod_gcd_lcm: "(m::nat) * n = gcd m n * lcm m n"
1273   unfolding lcm_nat_def
1274   by (simp add: dvd_mult_div_cancel [OF nat_gcd_dvd_prod])
1276 lemma int_prod_gcd_lcm: "abs(m::int) * abs n = gcd m n * lcm m n"
1277   unfolding lcm_int_def gcd_int_def
1278   apply (subst int_mult [symmetric])
1279   apply (subst nat_prod_gcd_lcm [symmetric])
1280   apply (subst nat_abs_mult_distrib [symmetric])
1281   apply (simp, simp add: abs_mult)
1282 done
1284 lemma nat_lcm_0 [simp]: "lcm (m::nat) 0 = 0"
1285   unfolding lcm_nat_def by simp
1287 lemma int_lcm_0 [simp]: "lcm (m::int) 0 = 0"
1288   unfolding lcm_int_def by simp
1290 lemma nat_lcm_1 [simp]: "lcm (m::nat) 1 = m"
1291   unfolding lcm_nat_def by simp
1293 lemma nat_lcm_Suc_0 [simp]: "lcm (m::nat) (Suc 0) = m"
1294   unfolding lcm_nat_def by (simp add: One_nat_def)
1296 lemma int_lcm_1 [simp]: "lcm (m::int) 1 = abs m"
1297   unfolding lcm_int_def by simp
1299 lemma nat_lcm_0_left [simp]: "lcm (0::nat) n = 0"
1300   unfolding lcm_nat_def by simp
1302 lemma int_lcm_0_left [simp]: "lcm (0::int) n = 0"
1303   unfolding lcm_int_def by simp
1305 lemma nat_lcm_1_left [simp]: "lcm (1::nat) m = m"
1306   unfolding lcm_nat_def by simp
1308 lemma nat_lcm_Suc_0_left [simp]: "lcm (Suc 0) m = m"
1309   unfolding lcm_nat_def by (simp add: One_nat_def)
1311 lemma int_lcm_1_left [simp]: "lcm (1::int) m = abs m"
1312   unfolding lcm_int_def by simp
1314 lemma nat_lcm_commute: "lcm (m::nat) n = lcm n m"
1315   unfolding lcm_nat_def by (simp add: nat_gcd_commute ring_simps)
1317 lemma int_lcm_commute: "lcm (m::int) n = lcm n m"
1318   unfolding lcm_int_def by (subst nat_lcm_commute, rule refl)
1320 (* to do: show lcm is associative, and then declare ac simps *)
1322 lemma nat_lcm_pos:
1323   assumes mpos: "(m::nat) > 0"
1324   and npos: "n>0"
1325   shows "lcm m n > 0"
1326 proof(rule ccontr, simp add: lcm_nat_def nat_gcd_zero)
1327   assume h:"m*n div gcd m n = 0"
1328   from mpos npos have "gcd m n \<noteq> 0" using nat_gcd_zero by simp
1329   hence gcdp: "gcd m n > 0" by simp
1330   with h
1331   have "m*n < gcd m n"
1332     by (cases "m * n < gcd m n")
1333        (auto simp add: div_if[OF gcdp, where m="m*n"])
1334   moreover
1335   have "gcd m n dvd m" by simp
1336   with mpos dvd_imp_le have t1:"gcd m n \<le> m" by simp
1337   with npos have t1:"gcd m n*n \<le> m*n" by simp
1338   have "gcd m n \<le> gcd m n*n" using npos by simp
1339   with t1 have "gcd m n \<le> m*n" by arith
1340   ultimately show "False" by simp
1341 qed
1343 lemma int_lcm_pos:
1344   assumes mneq0: "(m::int) ~= 0"
1345   and npos: "n ~= 0"
1346   shows "lcm m n > 0"
1348   apply (subst int_lcm_abs)
1349   apply (rule nat_lcm_pos [transferred])
1350   using prems apply auto
1351 done
1353 lemma nat_dvd_pos:
1354   fixes n m :: nat
1355   assumes "n > 0" and "m dvd n"
1356   shows "m > 0"
1357 using assms by (cases m) auto
1359 lemma nat_lcm_least:
1360   assumes "(m::nat) dvd k" and "n dvd k"
1361   shows "lcm m n dvd k"
1362 proof (cases k)
1363   case 0 then show ?thesis by auto
1364 next
1365   case (Suc _) then have pos_k: "k > 0" by auto
1366   from assms nat_dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
1367   with nat_gcd_zero [of m n] have pos_gcd: "gcd m n > 0" by simp
1368   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
1369   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
1370   from pos_k k_m have pos_p: "p > 0" by auto
1371   from pos_k k_n have pos_q: "q > 0" by auto
1372   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
1373     by (simp add: mult_ac nat_gcd_mult_distrib)
1374   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
1375     by (simp add: k_m [symmetric] k_n [symmetric])
1376   also have "\<dots> = k * p * q * gcd m n"
1377     by (simp add: mult_ac nat_gcd_mult_distrib)
1378   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
1379     by (simp only: k_m [symmetric] k_n [symmetric])
1380   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
1382   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
1383     by simp
1384   with nat_prod_gcd_lcm [of m n]
1385   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
1387   with pos_gcd have "lcm m n * gcd q p = k" by auto
1388   then show ?thesis using dvd_def by auto
1389 qed
1391 lemma int_lcm_least:
1392   assumes "(m::int) dvd k" and "n dvd k"
1393   shows "lcm m n dvd k"
1395   apply (subst int_lcm_abs)
1396   apply (rule dvd_trans)
1397   apply (rule nat_lcm_least [transferred, of _ "abs k" _])
1398   using prems apply auto
1399 done
1401 lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
1402 proof (cases m)
1403   case 0 then show ?thesis by simp
1404 next
1405   case (Suc _)
1406   then have mpos: "m > 0" by simp
1407   show ?thesis
1408   proof (cases n)
1409     case 0 then show ?thesis by simp
1410   next
1411     case (Suc _)
1412     then have npos: "n > 0" by simp
1413     have "gcd m n dvd n" by simp
1414     then obtain k where "n = gcd m n * k" using dvd_def by auto
1415     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
1417     also have "\<dots> = m * k" using mpos npos nat_gcd_zero by simp
1418     finally show ?thesis by (simp add: lcm_nat_def)
1419   qed
1420 qed
1422 lemma int_lcm_dvd1: "(m::int) dvd lcm m n"
1423   apply (subst int_lcm_abs)
1424   apply (rule dvd_trans)
1425   prefer 2
1426   apply (rule nat_lcm_dvd1 [transferred])
1427   apply auto
1428 done
1430 lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n"
1431   by (subst nat_lcm_commute, rule nat_lcm_dvd1)
1433 lemma int_lcm_dvd2: "(n::int) dvd lcm m n"
1434   by (subst int_lcm_commute, rule int_lcm_dvd1)
1436 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
1437 by(metis nat_lcm_dvd1 dvd_trans)
1439 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
1440 by(metis nat_lcm_dvd2 dvd_trans)
1442 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
1443 by(metis int_lcm_dvd1 dvd_trans)
1445 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
1446 by(metis int_lcm_dvd2 dvd_trans)
1448 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
1449     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1450   by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2)
1452 lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
1453     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1454   by (auto intro: dvd_anti_sym [transferred] int_lcm_least)
1456 lemma nat_lcm_dvd_eq [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
1457   apply (rule sym)
1458   apply (subst nat_lcm_unique [symmetric])
1459   apply auto
1460 done
1462 lemma int_lcm_dvd_eq [simp]: "0 <= y \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm x y = y"
1463   apply (rule sym)
1464   apply (subst int_lcm_unique [symmetric])
1465   apply auto
1466 done
1468 lemma nat_lcm_dvd_eq' [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
1469   by (subst nat_lcm_commute, erule nat_lcm_dvd_eq)
1471 lemma int_lcm_dvd_eq' [simp]: "y >= 0 \<Longrightarrow> (x::int) dvd y \<Longrightarrow> lcm y x = y"
1472   by (subst int_lcm_commute, erule (1) int_lcm_dvd_eq)
1476 subsection {* Primes *}
1478 (* Is there a better way to handle these, rather than making them
1479    elim rules? *)
1481 lemma nat_prime_ge_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
1482   by (unfold prime_nat_def, auto)
1484 lemma nat_prime_gt_0 [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
1485   by (unfold prime_nat_def, auto)
1487 lemma nat_prime_ge_1 [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
1488   by (unfold prime_nat_def, auto)
1490 lemma nat_prime_gt_1 [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
1491   by (unfold prime_nat_def, auto)
1493 lemma nat_prime_ge_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
1494   by (unfold prime_nat_def, auto)
1496 lemma nat_prime_gt_Suc_0 [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
1497   by (unfold prime_nat_def, auto)
1499 lemma nat_prime_ge_2 [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
1500   by (unfold prime_nat_def, auto)
1502 lemma int_prime_ge_0 [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
1503   by (unfold prime_int_def prime_nat_def, auto)
1505 lemma int_prime_gt_0 [elim]: "prime (p::int) \<Longrightarrow> p > 0"
1506   by (unfold prime_int_def prime_nat_def, auto)
1508 lemma int_prime_ge_1 [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
1509   by (unfold prime_int_def prime_nat_def, auto)
1511 lemma int_prime_gt_1 [elim]: "prime (p::int) \<Longrightarrow> p > 1"
1512   by (unfold prime_int_def prime_nat_def, auto)
1514 lemma int_prime_ge_2 [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
1515   by (unfold prime_int_def prime_nat_def, auto)
1517 thm prime_nat_def;
1518 thm prime_nat_def [transferred];
1520 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
1521     m = 1 \<or> m = p))"
1522   using prime_nat_def [transferred]
1523     apply (case_tac "p >= 0")
1524     by (blast, auto simp add: int_prime_ge_0)
1526 (* To do: determine primality of any numeral *)
1528 lemma nat_zero_not_prime [simp]: "~prime (0::nat)"
1531 lemma int_zero_not_prime [simp]: "~prime (0::int)"
1534 lemma nat_one_not_prime [simp]: "~prime (1::nat)"
1537 lemma nat_Suc_0_not_prime [simp]: "~prime (Suc 0)"
1538   by (simp add: prime_nat_def One_nat_def)
1540 lemma int_one_not_prime [simp]: "~prime (1::int)"
1543 lemma nat_two_is_prime [simp]: "prime (2::nat)"
1544   apply (auto simp add: prime_nat_def)
1545   apply (case_tac m)
1546   apply (auto dest!: dvd_imp_le)
1547   done
1549 lemma int_two_is_prime [simp]: "prime (2::int)"
1550   by (rule nat_two_is_prime [transferred direction: nat "op <= (0::int)"])
1552 lemma nat_prime_imp_coprime: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1553   apply (unfold prime_nat_def)
1554   apply (metis nat_gcd_dvd1 nat_gcd_dvd2)
1555   done
1557 lemma int_prime_imp_coprime: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1558   apply (unfold prime_int_altdef)
1559   apply (metis int_gcd_dvd1 int_gcd_dvd2 int_gcd_ge_0)
1560   done
1562 lemma nat_prime_dvd_mult: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1563   by (blast intro: nat_coprime_dvd_mult nat_prime_imp_coprime)
1565 lemma int_prime_dvd_mult: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1566   by (blast intro: int_coprime_dvd_mult int_prime_imp_coprime)
1568 lemma nat_prime_dvd_mult_eq [simp]: "prime (p::nat) \<Longrightarrow>
1569     p dvd m * n = (p dvd m \<or> p dvd n)"
1570   by (rule iffI, rule nat_prime_dvd_mult, auto)
1572 lemma int_prime_dvd_mult_eq [simp]: "prime (p::int) \<Longrightarrow>
1573     p dvd m * n = (p dvd m \<or> p dvd n)"
1574   by (rule iffI, rule int_prime_dvd_mult, auto)
1576 lemma nat_not_prime_eq_prod: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1577     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1578   unfolding prime_nat_def dvd_def apply auto
1579   apply (subgoal_tac "k > 1")
1580   apply force
1581   apply (subgoal_tac "k ~= 0")
1582   apply force
1583   apply (rule notI)
1584   apply force
1585 done
1587 (* there's a lot of messing around with signs of products here --
1588    could this be made more automatic? *)
1589 lemma int_not_prime_eq_prod: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1590     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1591   unfolding prime_int_altdef dvd_def
1592   apply auto
1593   apply (rule_tac x = m in exI)
1594   apply (rule_tac x = k in exI)
1595   apply (auto simp add: mult_compare_simps)
1596   apply (subgoal_tac "k > 0")
1597   apply arith
1598   apply (case_tac "k <= 0")
1599   apply (subgoal_tac "m * k <= 0")
1600   apply force
1601   apply (subst zero_compare_simps(8))
1602   apply auto
1603   apply (subgoal_tac "m * k <= 0")
1604   apply force
1605   apply (subst zero_compare_simps(8))
1606   apply auto
1607 done
1609 lemma nat_prime_dvd_power [rule_format]: "prime (p::nat) -->
1610     n > 0 --> (p dvd x^n --> p dvd x)"
1611   by (induct n rule: nat_induct, auto)
1613 lemma int_prime_dvd_power [rule_format]: "prime (p::int) -->
1614     n > 0 --> (p dvd x^n --> p dvd x)"
1615   apply (induct n rule: nat_induct, auto)
1616   apply (frule int_prime_ge_0)
1617   apply auto
1618 done
1620 lemma nat_prime_imp_power_coprime: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
1621     coprime a (p^m)"
1622   apply (rule nat_coprime_exp)
1623   apply (subst nat_gcd_commute)
1624   apply (erule (1) nat_prime_imp_coprime)
1625 done
1627 lemma int_prime_imp_power_coprime: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
1628     coprime a (p^m)"
1629   apply (rule int_coprime_exp)
1630   apply (subst int_gcd_commute)
1631   apply (erule (1) int_prime_imp_coprime)
1632 done
1634 lemma nat_primes_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1635   apply (rule nat_prime_imp_coprime, assumption)
1636   apply (unfold prime_nat_def, auto)
1637 done
1639 lemma int_primes_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1640   apply (rule int_prime_imp_coprime, assumption)
1641   apply (unfold prime_int_altdef, clarify)
1642   apply (drule_tac x = q in spec)
1643   apply (drule_tac x = p in spec)
1644   apply auto
1645 done
1647 lemma nat_primes_imp_powers_coprime: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
1648     coprime (p^m) (q^n)"
1649   by (rule nat_coprime_exp2, rule nat_primes_coprime)
1651 lemma int_primes_imp_powers_coprime: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
1652     coprime (p^m) (q^n)"
1653   by (rule int_coprime_exp2, rule int_primes_coprime)
1655 lemma nat_prime_factor: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
1656   apply (induct n rule: nat_less_induct)
1657   apply (case_tac "n = 0")
1658   using nat_two_is_prime apply blast
1659   apply (case_tac "prime n")
1660   apply blast
1661   apply (subgoal_tac "n > 1")
1662   apply (frule (1) nat_not_prime_eq_prod)
1663   apply (auto intro: dvd_mult dvd_mult2)
1664 done
1666 (* An Isar version:
1668 lemma nat_prime_factor_b:
1669   fixes n :: nat
1670   assumes "n \<noteq> 1"
1671   shows "\<exists>p. prime p \<and> p dvd n"
1673 using `n ~= 1`
1674 proof (induct n rule: nat_less_induct)
1675   fix n :: nat
1676   assume "n ~= 1" and
1677     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
1678   thus "\<exists>p. prime p \<and> p dvd n"
1679   proof -
1680   {
1681     assume "n = 0"
1682     moreover note nat_two_is_prime
1683     ultimately have ?thesis
1684       by (auto simp del: nat_two_is_prime)
1685   }
1686   moreover
1687   {
1688     assume "prime n"
1689     hence ?thesis by auto
1690   }
1691   moreover
1692   {
1693     assume "n ~= 0" and "~ prime n"
1694     with `n ~= 1` have "n > 1" by auto
1695     with `~ prime n` and nat_not_prime_eq_prod obtain m k where
1696       "n = m * k" and "1 < m" and "m < n" by blast
1697     with ih obtain p where "prime p" and "p dvd m" by blast
1698     with `n = m * k` have ?thesis by auto
1699   }
1700   ultimately show ?thesis by blast
1701   qed
1702 qed
1704 *)
1706 text {* One property of coprimality is easier to prove via prime factors. *}
1708 lemma nat_prime_divprod_pow:
1709   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
1710   shows "p^n dvd a \<or> p^n dvd b"
1711 proof-
1712   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
1713       apply (cases "n=0", simp_all)
1714       apply (cases "a=1", simp_all) done}
1715   moreover
1716   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
1717     then obtain m where m: "n = Suc m" by (cases n, auto)
1718     from n have "p dvd p^n" by (intro dvd_power, auto)
1719     also note pab
1720     finally have pab': "p dvd a * b".
1721     from nat_prime_dvd_mult[OF p pab']
1722     have "p dvd a \<or> p dvd b" .
1723     moreover
1724     {assume pa: "p dvd a"
1725       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
1726       from nat_coprime_common_divisor [OF ab, OF pa] p have "\<not> p dvd b" by auto
1727       with p have "coprime b p"
1728         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
1729       hence pnb: "coprime (p^n) b"
1730         by (subst nat_gcd_commute, rule nat_coprime_exp)
1731       from nat_coprime_divprod[OF pnba pnb] have ?thesis by blast }
1732     moreover
1733     {assume pb: "p dvd b"
1734       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
1735       from nat_coprime_common_divisor [OF ab, of p] pb p have "\<not> p dvd a"
1736         by auto
1737       with p have "coprime a p"
1738         by (subst nat_gcd_commute, intro nat_prime_imp_coprime)
1739       hence pna: "coprime (p^n) a"
1740         by (subst nat_gcd_commute, rule nat_coprime_exp)
1741       from nat_coprime_divprod[OF pab pna] have ?thesis by blast }
1742     ultimately have ?thesis by blast}
1743   ultimately show ?thesis by blast
1744 qed
1746 end