src/HOL/GCD.thy
 author nipkow Sun Jul 12 14:48:01 2009 +0200 (2009-07-12) changeset 31995 8f37cf60b885 parent 31992 f8aed98faae7 child 31996 1d93369079c4 permissions -rw-r--r--
more gcd/lcm lemmas
1 (*  Title:      GCD.thy
2     Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
3                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
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 Tobias Nipkow cleaned up a lot.
24 *)
29 theory GCD
30 imports NatTransfer
31 begin
33 declare One_nat_def [simp del]
35 subsection {* gcd *}
37 class gcd = zero + one + dvd +
39 fixes
40   gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
41   lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
43 begin
45 abbreviation
46   coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
47 where
48   "coprime x y == (gcd x y = 1)"
50 end
52 class prime = one +
54 fixes
55   prime :: "'a \<Rightarrow> bool"
58 (* definitions for the natural numbers *)
60 instantiation nat :: gcd
62 begin
64 fun
65   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
66 where
67   "gcd_nat x y =
68    (if y = 0 then x else gcd y (x mod y))"
70 definition
71   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
72 where
73   "lcm_nat x y = x * y div (gcd x y)"
75 instance proof qed
77 end
80 instantiation nat :: prime
82 begin
84 definition
85   prime_nat :: "nat \<Rightarrow> bool"
86 where
87   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
89 instance proof qed
91 end
94 (* definitions for the integers *)
96 instantiation int :: gcd
98 begin
100 definition
101   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
102 where
103   "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
105 definition
106   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
107 where
108   "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
110 instance proof qed
112 end
115 instantiation int :: prime
117 begin
119 definition
120   prime_int :: "int \<Rightarrow> bool"
121 where
122   [code del]: "prime_int p = prime (nat p)"
124 instance proof qed
126 end
129 subsection {* Set up Transfer *}
132 lemma transfer_nat_int_gcd:
133   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
134   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
135   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
136   unfolding gcd_int_def lcm_int_def prime_int_def
137   by auto
139 lemma transfer_nat_int_gcd_closures:
140   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
141   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
142   by (auto simp add: gcd_int_def lcm_int_def)
145     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
147 lemma transfer_int_nat_gcd:
148   "gcd (int x) (int y) = int (gcd x y)"
149   "lcm (int x) (int y) = int (lcm x y)"
150   "prime (int x) = prime x"
151   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
153 lemma transfer_int_nat_gcd_closures:
154   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
155   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
156   by (auto simp add: gcd_int_def lcm_int_def)
159     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
163 subsection {* GCD *}
165 (* was gcd_induct *)
166 lemma gcd_nat_induct:
167   fixes m n :: nat
168   assumes "\<And>m. P m 0"
169     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
170   shows "P m n"
171   apply (rule gcd_nat.induct)
172   apply (case_tac "y = 0")
173   using assms apply simp_all
174 done
176 (* specific to int *)
178 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
181 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
184 lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
187 lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
190 lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
191 by (metis abs_idempotent gcd_abs_int)
193 lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
194 by (metis abs_idempotent gcd_abs_int)
196 lemma gcd_cases_int:
197   fixes x :: int and y
198   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
199       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
200       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
201       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
202   shows "P (gcd x y)"
203 by (insert prems, auto simp add: gcd_neg1_int gcd_neg2_int, arith)
205 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
208 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
211 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
214 lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
217 lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
220 lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
221 by (metis abs_idempotent lcm_int_def)
223 lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
224 by (metis abs_idempotent lcm_int_def)
226 lemma lcm_cases_int:
227   fixes x :: int and y
228   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
229       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
230       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
231       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
232   shows "P (lcm x y)"
233 by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
235 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
238 (* was gcd_0, etc. *)
239 lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
240   by simp
242 (* was igcd_0, etc. *)
243 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
244   by (unfold gcd_int_def, auto)
246 lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
247   by simp
249 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
250   by (unfold gcd_int_def, auto)
252 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
253   by (case_tac "y = 0", auto)
255 (* weaker, but useful for the simplifier *)
257 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
258   by simp
260 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
261   by simp
263 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
266 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
269 lemma gcd_idem_nat: "gcd (x::nat) x = x"
270 by simp
272 lemma gcd_idem_int: "gcd (x::int) x = abs x"
273 by (auto simp add: gcd_int_def)
275 declare gcd_nat.simps [simp del]
277 text {*
278   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The
279   conjunctions don't seem provable separately.
280 *}
282 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
283   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
284   apply (induct m n rule: gcd_nat_induct)
286   apply (blast dest: dvd_mod_imp_dvd)
287 done
289 lemma gcd_dvd1_int [iff]: "gcd (x::int) y dvd x"
290 by (metis gcd_int_def int_dvd_iff gcd_dvd1_nat)
292 lemma gcd_dvd2_int [iff]: "gcd (x::int) y dvd y"
293 by (metis gcd_int_def int_dvd_iff gcd_dvd2_nat)
295 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
296 by(metis gcd_dvd1_nat dvd_trans)
298 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
299 by(metis gcd_dvd2_nat dvd_trans)
301 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
302 by(metis gcd_dvd1_int dvd_trans)
304 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
305 by(metis gcd_dvd2_int dvd_trans)
307 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
308   by (rule dvd_imp_le, auto)
310 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
311   by (rule dvd_imp_le, auto)
313 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
314   by (rule zdvd_imp_le, auto)
316 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
317   by (rule zdvd_imp_le, auto)
319 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
320 by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
322 lemma gcd_greatest_int:
323   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
324   apply (subst gcd_abs_int)
325   apply (subst abs_dvd_iff [symmetric])
326   apply (rule gcd_greatest_nat [transferred])
327   apply auto
328 done
330 lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
331     (k dvd m & k dvd n)"
332   by (blast intro!: gcd_greatest_nat intro: dvd_trans)
334 lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
335   by (blast intro!: gcd_greatest_int intro: dvd_trans)
337 lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
338   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
340 lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
341   by (auto simp add: gcd_int_def)
343 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
344   by (insert gcd_zero_nat [of m n], arith)
346 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
347   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
349 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
350   by (rule dvd_anti_sym, auto)
352 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
353   by (auto simp add: gcd_int_def gcd_commute_nat)
355 lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
356   apply (rule dvd_anti_sym)
357   apply (blast intro: dvd_trans)+
358 done
360 lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
361   by (auto simp add: gcd_int_def gcd_assoc_nat)
363 lemmas gcd_left_commute_nat =
364   mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
366 lemmas gcd_left_commute_int =
367   mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
369 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
370   -- {* gcd is an AC-operator *}
372 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
374 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
375     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
376   apply auto
377   apply (rule dvd_anti_sym)
378   apply (erule (1) gcd_greatest_nat)
379   apply auto
380 done
382 lemma gcd_unique_int: "d >= 0 & (d::int) 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 (case_tac "d = 0")
385   apply force
386   apply (rule iffI)
387   apply (rule zdvd_anti_sym)
388   apply arith
389   apply (subst gcd_pos_int)
390   apply clarsimp
391   apply (drule_tac x = "d + 1" in spec)
392   apply (frule zdvd_imp_le)
393   apply (auto intro: gcd_greatest_int)
394 done
396 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
397 by (metis dvd.eq_iff gcd_unique_nat)
399 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
400 by (metis dvd.eq_iff gcd_unique_nat)
402 lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
403 by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
405 lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
406 by (metis gcd_proj1_if_dvd_int gcd_commute_int)
409 text {*
410   \medskip Multiplication laws
411 *}
413 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
414     -- {* \cite[page 27]{davenport92} *}
415   apply (induct m n rule: gcd_nat_induct)
416   apply simp
417   apply (case_tac "k = 0")
418   apply (simp_all add: mod_geq gcd_non_0_nat mod_mult_distrib2)
419 done
421 lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
422   apply (subst (1 2) gcd_abs_int)
423   apply (subst (1 2) abs_mult)
424   apply (rule gcd_mult_distrib_nat [transferred])
425   apply auto
426 done
428 lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
429   apply (insert gcd_mult_distrib_nat [of m k n])
430   apply simp
431   apply (erule_tac t = m in ssubst)
432   apply simp
433   done
435 lemma coprime_dvd_mult_int:
436   "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
437 apply (subst abs_dvd_iff [symmetric])
438 apply (subst dvd_abs_iff [symmetric])
439 apply (subst (asm) gcd_abs_int)
440 apply (rule coprime_dvd_mult_nat [transferred])
441     prefer 4 apply assumption
442    apply auto
443 apply (subst abs_mult [symmetric], auto)
444 done
446 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
447     (k dvd m * n) = (k dvd m)"
448   by (auto intro: coprime_dvd_mult_nat)
450 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
451     (k dvd m * n) = (k dvd m)"
452   by (auto intro: coprime_dvd_mult_int)
454 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
455   apply (rule dvd_anti_sym)
456   apply (rule gcd_greatest_nat)
457   apply (rule_tac n = k in coprime_dvd_mult_nat)
461 done
463 lemma gcd_mult_cancel_int:
464   "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
465 apply (subst (1 2) gcd_abs_int)
466 apply (subst abs_mult)
467 apply (rule gcd_mult_cancel_nat [transferred], auto)
468 done
470 text {* \medskip Addition laws *}
472 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
473   apply (case_tac "n = 0")
475 done
477 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
478   apply (subst (1 2) gcd_commute_nat)
480   apply simp
481 done
483 (* to do: add the other variations? *)
485 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
486   by (subst gcd_add1_nat [symmetric], auto)
488 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
489   apply (subst gcd_commute_nat)
490   apply (subst gcd_diff1_nat [symmetric])
491   apply auto
492   apply (subst gcd_commute_nat)
493   apply (subst gcd_diff1_nat)
494   apply assumption
495   apply (rule gcd_commute_nat)
496 done
498 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
499   apply (frule_tac b = y and a = x in pos_mod_sign)
500   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
501   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
502     zmod_zminus1_eq_if)
503   apply (frule_tac a = x in pos_mod_bound)
504   apply (subst (1 2) gcd_commute_nat)
505   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
506     nat_le_eq_zle)
507 done
509 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
510   apply (case_tac "y = 0")
511   apply force
512   apply (case_tac "y > 0")
513   apply (subst gcd_non_0_int, auto)
514   apply (insert gcd_non_0_int [of "-y" "-x"])
515   apply (auto simp add: gcd_neg1_int gcd_neg2_int)
516 done
518 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
521 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
524 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
525 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
527 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
528 by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
531 (* to do: differences, and all variations of addition rules
532     as simplification rules for nat and int *)
534 (* FIXME remove iff *)
535 lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
536   using mult_dvd_mono [of 1] by auto
538 (* to do: add the three variations of these, and for ints? *)
540 lemma finite_divisors_nat[simp]:
541   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
542 proof-
543   have "finite{d. d <= m}" by(blast intro: bounded_nat_set_is_finite)
544   from finite_subset[OF _ this] show ?thesis using assms
545     by(bestsimp intro!:dvd_imp_le)
546 qed
548 lemma finite_divisors_int[simp]:
549   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
550 proof-
551   have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
552   hence "finite{d. abs d <= abs i}" by simp
553   from finite_subset[OF _ this] show ?thesis using assms
554     by(bestsimp intro!:dvd_imp_le_int)
555 qed
557 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
558 apply(rule antisym)
559  apply (fastsimp intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
560 apply simp
561 done
563 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
564 apply(rule antisym)
565  apply(rule Max_le_iff[THEN iffD2])
566    apply simp
567   apply fastsimp
568  apply (metis Collect_def abs_ge_self dvd_imp_le_int mem_def zle_trans)
569 apply simp
570 done
572 lemma gcd_is_Max_divisors_nat:
573   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
574 apply(rule Max_eqI[THEN sym])
575   apply (metis finite_Collect_conjI finite_divisors_nat)
576  apply simp
577  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
578 apply simp
579 done
581 lemma gcd_is_Max_divisors_int:
582   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
583 apply(rule Max_eqI[THEN sym])
584   apply (metis finite_Collect_conjI finite_divisors_int)
585  apply simp
586  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
587 apply simp
588 done
591 subsection {* Coprimality *}
593 lemma div_gcd_coprime_nat:
594   assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
595   shows "coprime (a div gcd a b) (b div gcd a b)"
596 proof -
597   let ?g = "gcd a b"
598   let ?a' = "a div ?g"
599   let ?b' = "b div ?g"
600   let ?g' = "gcd ?a' ?b'"
601   have dvdg: "?g dvd a" "?g dvd b" by simp_all
602   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
603   from dvdg dvdg' obtain ka kb ka' kb' where
604       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
605     unfolding dvd_def by blast
606   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
607     by simp_all
608   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
609     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
610       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
611   have "?g \<noteq> 0" using nz by (simp add: gcd_zero_nat)
612   then have gp: "?g > 0" by arith
613   from gcd_greatest_nat [OF dvdgg'] have "?g * ?g' dvd ?g" .
614   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
615 qed
617 lemma div_gcd_coprime_int:
618   assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
619   shows "coprime (a div gcd a b) (b div gcd a b)"
620 apply (subst (1 2 3) gcd_abs_int)
621 apply (subst (1 2) abs_div)
622   apply simp
623  apply simp
624 apply(subst (1 2) abs_gcd_int)
625 apply (rule div_gcd_coprime_nat [transferred])
626 using nz apply (auto simp add: gcd_abs_int [symmetric])
627 done
629 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
630   using gcd_unique_nat[of 1 a b, simplified] by auto
632 lemma coprime_Suc_0_nat:
633     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
634   using coprime_nat by (simp add: One_nat_def)
636 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
637     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
638   using gcd_unique_int [of 1 a b]
639   apply clarsimp
640   apply (erule subst)
641   apply (rule iffI)
642   apply force
643   apply (drule_tac x = "abs e" in exI)
644   apply (case_tac "e >= 0")
645   apply force
646   apply force
647 done
649 lemma gcd_coprime_nat:
650   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
651     b: "b = b' * gcd a b"
652   shows    "coprime a' b'"
654   apply (subgoal_tac "a' = a div gcd a b")
655   apply (erule ssubst)
656   apply (subgoal_tac "b' = b div gcd a b")
657   apply (erule ssubst)
658   apply (rule div_gcd_coprime_nat)
659   using prems
660   apply force
661   apply (subst (1) b)
662   using z apply force
663   apply (subst (1) a)
664   using z apply force
665 done
667 lemma gcd_coprime_int:
668   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
669     b: "b = b' * gcd a b"
670   shows    "coprime a' b'"
672   apply (subgoal_tac "a' = a div gcd a b")
673   apply (erule ssubst)
674   apply (subgoal_tac "b' = b div gcd a b")
675   apply (erule ssubst)
676   apply (rule div_gcd_coprime_int)
677   using prems
678   apply force
679   apply (subst (1) b)
680   using z apply force
681   apply (subst (1) a)
682   using z apply force
683 done
685 lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
686     shows "coprime d (a * b)"
687   apply (subst gcd_commute_nat)
688   using da apply (subst gcd_mult_cancel_nat)
689   apply (subst gcd_commute_nat, assumption)
690   apply (subst gcd_commute_nat, rule db)
691 done
693 lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
694     shows "coprime d (a * b)"
695   apply (subst gcd_commute_int)
696   using da apply (subst gcd_mult_cancel_int)
697   apply (subst gcd_commute_int, assumption)
698   apply (subst gcd_commute_int, rule db)
699 done
701 lemma coprime_lmult_nat:
702   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
703 proof -
704   have "gcd d a dvd gcd d (a * b)"
705     by (rule gcd_greatest_nat, auto)
706   with dab show ?thesis
707     by auto
708 qed
710 lemma coprime_lmult_int:
711   assumes "coprime (d::int) (a * b)" shows "coprime d a"
712 proof -
713   have "gcd d a dvd gcd d (a * b)"
714     by (rule gcd_greatest_int, auto)
715   with assms show ?thesis
716     by auto
717 qed
719 lemma coprime_rmult_nat:
720   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
721 proof -
722   have "gcd d b dvd gcd d (a * b)"
723     by (rule gcd_greatest_nat, auto intro: dvd_mult)
724   with assms show ?thesis
725     by auto
726 qed
728 lemma coprime_rmult_int:
729   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
730 proof -
731   have "gcd d b dvd gcd d (a * b)"
732     by (rule gcd_greatest_int, auto intro: dvd_mult)
733   with dab show ?thesis
734     by auto
735 qed
737 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
738     coprime d a \<and>  coprime d b"
739   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
740     coprime_mult_nat[of d a b]
741   by blast
743 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
744     coprime d a \<and>  coprime d b"
745   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
746     coprime_mult_int[of d a b]
747   by blast
749 lemma gcd_coprime_exists_nat:
750     assumes nz: "gcd (a::nat) b \<noteq> 0"
751     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
752   apply (rule_tac x = "a div gcd a b" in exI)
753   apply (rule_tac x = "b div gcd a b" in exI)
754   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
755 done
757 lemma gcd_coprime_exists_int:
758     assumes nz: "gcd (a::int) b \<noteq> 0"
759     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
760   apply (rule_tac x = "a div gcd a b" in exI)
761   apply (rule_tac x = "b div gcd a b" in exI)
762   using nz apply (auto simp add: div_gcd_coprime_int dvd_div_mult_self)
763 done
765 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
766   by (induct n, simp_all add: coprime_mult_nat)
768 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
769   by (induct n, simp_all add: coprime_mult_int)
771 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
772   apply (rule coprime_exp_nat)
773   apply (subst gcd_commute_nat)
774   apply (rule coprime_exp_nat)
775   apply (subst gcd_commute_nat, assumption)
776 done
778 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
779   apply (rule coprime_exp_int)
780   apply (subst gcd_commute_int)
781   apply (rule coprime_exp_int)
782   apply (subst gcd_commute_int, assumption)
783 done
785 lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
786 proof (cases)
787   assume "a = 0 & b = 0"
788   thus ?thesis by simp
789   next assume "~(a = 0 & b = 0)"
790   hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
791     by (auto simp:div_gcd_coprime_nat)
792   hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
793       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
794     apply (subst (1 2) mult_commute)
795     apply (subst gcd_mult_distrib_nat [symmetric])
796     apply simp
797     done
798   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
799     apply (subst div_power)
800     apply auto
801     apply (rule dvd_div_mult_self)
802     apply (rule dvd_power_same)
803     apply auto
804     done
805   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
806     apply (subst div_power)
807     apply auto
808     apply (rule dvd_div_mult_self)
809     apply (rule dvd_power_same)
810     apply auto
811     done
812   finally show ?thesis .
813 qed
815 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
816   apply (subst (1 2) gcd_abs_int)
817   apply (subst (1 2) power_abs)
818   apply (rule gcd_exp_nat [where n = n, transferred])
819   apply auto
820 done
822 lemma coprime_divprod_nat: "(d::nat) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
823   using coprime_dvd_mult_iff_nat[of d a b]
824   by (auto simp add: mult_commute)
826 lemma coprime_divprod_int: "(d::int) dvd a * b  \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
827   using coprime_dvd_mult_iff_int[of d a b]
828   by (auto simp add: mult_commute)
830 lemma division_decomp_nat: assumes dc: "(a::nat) 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 gcd_coprime_exists_nat[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" using dvd_trans[of a' a "b*c"] by simp
843     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
844     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
845     with z have th_1: "a' dvd b' * c" by auto
846     from coprime_dvd_mult_nat[OF ab'(3)] th_1
847     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
848     from ab' have "a = ?g*a'" by algebra
849     with thb thc have ?thesis by blast }
850   ultimately show ?thesis by blast
851 qed
853 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
854   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
855 proof-
856   let ?g = "gcd a b"
857   {assume "?g = 0" with dc have ?thesis by auto}
858   moreover
859   {assume z: "?g \<noteq> 0"
860     from gcd_coprime_exists_int[OF z]
861     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
862       by blast
863     have thb: "?g dvd b" by auto
864     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
865     with dc have th0: "a' dvd b*c"
866       using dvd_trans[of a' a "b*c"] by simp
867     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
868     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult_assoc)
869     with z have th_1: "a' dvd b' * c" by auto
870     from coprime_dvd_mult_int[OF ab'(3)] th_1
871     have thc: "a' dvd c" by (subst (asm) mult_commute, blast)
872     from ab' have "a = ?g*a'" by algebra
873     with thb thc have ?thesis by blast }
874   ultimately show ?thesis by blast
875 qed
877 lemma pow_divides_pow_nat:
878   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
879   shows "a dvd b"
880 proof-
881   let ?g = "gcd a b"
882   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
883   {assume "?g = 0" with ab n have ?thesis by auto }
884   moreover
885   {assume z: "?g \<noteq> 0"
886     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
887     from gcd_coprime_exists_nat[OF z]
888     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
889       by blast
890     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
892     hence "?g^n*a'^n dvd ?g^n *b'^n"
893       by (simp only: power_mult_distrib mult_commute)
894     with zn z n have th0:"a'^n dvd b'^n" by auto
895     have "a' dvd a'^n" by (simp add: m)
896     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
897     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
898     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
899     have "a' dvd b'" by (subst (asm) mult_commute, blast)
900     hence "a'*?g dvd b'*?g" by simp
901     with ab'(1,2)  have ?thesis by simp }
902   ultimately show ?thesis by blast
903 qed
905 lemma pow_divides_pow_int:
906   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
907   shows "a dvd b"
908 proof-
909   let ?g = "gcd a b"
910   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
911   {assume "?g = 0" with ab n have ?thesis by auto }
912   moreover
913   {assume z: "?g \<noteq> 0"
914     hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
915     from gcd_coprime_exists_int[OF z]
916     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
917       by blast
918     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
920     hence "?g^n*a'^n dvd ?g^n *b'^n"
921       by (simp only: power_mult_distrib mult_commute)
922     with zn z n have th0:"a'^n dvd b'^n" by auto
923     have "a' dvd a'^n" by (simp add: m)
924     with th0 have "a' dvd b'^n"
925       using dvd_trans[of a' "a'^n" "b'^n"] by simp
926     hence th1: "a' dvd b'^m * b'" by (simp add: m mult_commute)
927     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
928     have "a' dvd b'" by (subst (asm) mult_commute, blast)
929     hence "a'*?g dvd b'*?g" by simp
930     with ab'(1,2)  have ?thesis by simp }
931   ultimately show ?thesis by blast
932 qed
934 (* FIXME move to Divides(?) *)
935 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
936   by (auto intro: pow_divides_pow_nat dvd_power_same)
938 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
939   by (auto intro: pow_divides_pow_int dvd_power_same)
941 lemma divides_mult_nat:
942   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
943   shows "m * n dvd r"
944 proof-
945   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
946     unfolding dvd_def by blast
947   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
948   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
949   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
950   from n' k show ?thesis unfolding dvd_def by auto
951 qed
953 lemma divides_mult_int:
954   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
955   shows "m * n dvd r"
956 proof-
957   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
958     unfolding dvd_def by blast
959   from mr n' have "m dvd n'*n" by (simp add: mult_commute)
960   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
961   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
962   from n' k show ?thesis unfolding dvd_def by auto
963 qed
965 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
966   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
967   apply force
968   apply (rule dvd_diff_nat)
969   apply auto
970 done
972 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
973   using coprime_plus_one_nat by (simp add: One_nat_def)
975 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
976   apply (subgoal_tac "gcd (n + 1) n dvd (n + 1 - n)")
977   apply force
978   apply (rule dvd_diff)
979   apply auto
980 done
982 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
983   using coprime_plus_one_nat [of "n - 1"]
984     gcd_commute_nat [of "n - 1" n] by auto
986 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
987   using coprime_plus_one_int [of "n - 1"]
988     gcd_commute_int [of "n - 1" n] by auto
990 lemma setprod_coprime_nat [rule_format]:
991     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (PROD i:A. f i) x"
992   apply (case_tac "finite A")
993   apply (induct set: finite)
994   apply (auto simp add: gcd_mult_cancel_nat)
995 done
997 lemma setprod_coprime_int [rule_format]:
998     "(ALL i: A. coprime (f i) (x::int)) --> coprime (PROD i:A. f i) x"
999   apply (case_tac "finite A")
1000   apply (induct set: finite)
1001   apply (auto simp add: gcd_mult_cancel_int)
1002 done
1004 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1005   unfolding prime_nat_def
1006   apply (subst even_mult_two_ex)
1007   apply clarify
1008   apply (drule_tac x = 2 in spec)
1009   apply auto
1010 done
1012 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
1013   unfolding prime_int_def
1014   apply (frule prime_odd_nat)
1015   apply (auto simp add: even_nat_def)
1016 done
1018 lemma coprime_common_divisor_nat: "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow>
1019     x dvd b \<Longrightarrow> x = 1"
1020   apply (subgoal_tac "x dvd gcd a b")
1021   apply simp
1022   apply (erule (1) gcd_greatest_nat)
1023 done
1025 lemma coprime_common_divisor_int: "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow>
1026     x dvd b \<Longrightarrow> abs x = 1"
1027   apply (subgoal_tac "x dvd gcd a b")
1028   apply simp
1029   apply (erule (1) gcd_greatest_int)
1030 done
1032 lemma coprime_divisors_nat: "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow>
1033     coprime d e"
1034   apply (auto simp add: dvd_def)
1035   apply (frule coprime_lmult_int)
1036   apply (subst gcd_commute_int)
1037   apply (subst (asm) (2) gcd_commute_int)
1038   apply (erule coprime_lmult_int)
1039 done
1041 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
1042 apply (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
1043 done
1045 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
1046 apply (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
1047 done
1050 subsection {* Bezout's theorem *}
1052 (* Function bezw returns a pair of witnesses to Bezout's theorem --
1053    see the theorems that follow the definition. *)
1054 fun
1055   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
1056 where
1057   "bezw x y =
1058   (if y = 0 then (1, 0) else
1059       (snd (bezw y (x mod y)),
1060        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
1062 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
1064 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
1065        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
1066   by simp
1068 declare bezw.simps [simp del]
1070 lemma bezw_aux [rule_format]:
1071     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
1072 proof (induct x y rule: gcd_nat_induct)
1073   fix m :: nat
1074   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
1075     by auto
1076   next fix m :: nat and n
1077     assume ngt0: "n > 0" and
1078       ih: "fst (bezw n (m mod n)) * int n +
1079         snd (bezw n (m mod n)) * int (m mod n) =
1080         int (gcd n (m mod n))"
1081     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
1082       apply (simp add: bezw_non_0 gcd_non_0_nat)
1083       apply (erule subst)
1085       apply (subst mod_div_equality [of m n, symmetric])
1086       (* applying simp here undoes the last substitution!
1087          what is procedure cancel_div_mod? *)
1088       apply (simp only: ring_simps zadd_int [symmetric]
1089         zmult_int [symmetric])
1090       done
1091 qed
1093 lemma bezout_int:
1094   fixes x y
1095   shows "EX u v. u * (x::int) + v * y = gcd x y"
1096 proof -
1097   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
1098       EX u v. u * x + v * y = gcd x y"
1099     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
1100     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
1101     apply (unfold gcd_int_def)
1102     apply simp
1103     apply (subst bezw_aux [symmetric])
1104     apply auto
1105     done
1106   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
1107       (x \<le> 0 \<and> y \<le> 0)"
1108     by auto
1109   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
1110     by (erule (1) bezout_aux)
1111   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
1112     apply (insert bezout_aux [of x "-y"])
1113     apply auto
1114     apply (rule_tac x = u in exI)
1115     apply (rule_tac x = "-v" in exI)
1116     apply (subst gcd_neg2_int [symmetric])
1117     apply auto
1118     done
1119   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
1120     apply (insert bezout_aux [of "-x" y])
1121     apply auto
1122     apply (rule_tac x = "-u" in exI)
1123     apply (rule_tac x = v in exI)
1124     apply (subst gcd_neg1_int [symmetric])
1125     apply auto
1126     done
1127   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
1128     apply (insert bezout_aux [of "-x" "-y"])
1129     apply auto
1130     apply (rule_tac x = "-u" in exI)
1131     apply (rule_tac x = "-v" in exI)
1132     apply (subst gcd_neg1_int [symmetric])
1133     apply (subst gcd_neg2_int [symmetric])
1134     apply auto
1135     done
1136   ultimately show ?thesis by blast
1137 qed
1139 text {* versions of Bezout for nat, by Amine Chaieb *}
1141 lemma ind_euclid:
1142   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
1143   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
1144   shows "P a b"
1145 proof(induct n\<equiv>"a+b" arbitrary: a b rule: nat_less_induct)
1146   fix n a b
1147   assume H: "\<forall>m < n. \<forall>a b. m = a + b \<longrightarrow> P a b" "n = a + b"
1148   have "a = b \<or> a < b \<or> b < a" by arith
1149   moreover {assume eq: "a= b"
1150     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
1151     by simp}
1152   moreover
1153   {assume lt: "a < b"
1154     hence "a + b - a < n \<or> a = 0"  using H(2) by arith
1155     moreover
1156     {assume "a =0" with z c have "P a b" by blast }
1157     moreover
1158     {assume ab: "a + b - a < n"
1159       have th0: "a + b - a = a + (b - a)" using lt by arith
1160       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
1161       have "P a b" by (simp add: th0[symmetric])}
1162     ultimately have "P a b" by blast}
1163   moreover
1164   {assume lt: "a > b"
1165     hence "b + a - b < n \<or> b = 0"  using H(2) by arith
1166     moreover
1167     {assume "b =0" with z c have "P a b" by blast }
1168     moreover
1169     {assume ab: "b + a - b < n"
1170       have th0: "b + a - b = b + (a - b)" using lt by arith
1171       from add[rule_format, OF H(1)[rule_format, OF ab th0]]
1172       have "P b a" by (simp add: th0[symmetric])
1173       hence "P a b" using c by blast }
1174     ultimately have "P a b" by blast}
1175 ultimately  show "P a b" by blast
1176 qed
1178 lemma bezout_lemma_nat:
1179   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1180     (a * x = b * y + d \<or> b * x = a * y + d)"
1181   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
1182     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
1183   using ex
1184   apply clarsimp
1186   apply (case_tac "a * x = b * y + d" , simp_all)
1187   apply (rule_tac x="x + y" in exI)
1188   apply (rule_tac x="y" in exI)
1189   apply algebra
1190   apply (rule_tac x="x" in exI)
1191   apply (rule_tac x="x + y" in exI)
1192   apply algebra
1193 done
1195 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1196     (a * x = b * y + d \<or> b * x = a * y + d)"
1197   apply(induct a b rule: ind_euclid)
1198   apply blast
1199   apply clarify
1201   apply clarsimp
1202   apply (rule_tac x="d" in exI)
1203   apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
1204   apply (rule_tac x="x+y" in exI)
1205   apply (rule_tac x="y" in exI)
1206   apply algebra
1207   apply (rule_tac x="x" in exI)
1208   apply (rule_tac x="x+y" in exI)
1209   apply algebra
1210 done
1212 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
1213     (a * x - b * y = d \<or> b * x - a * y = d)"
1215   apply clarsimp
1216   apply (rule_tac x="d" in exI, simp)
1217   apply (rule_tac x="x" in exI)
1218   apply (rule_tac x="y" in exI)
1219   apply auto
1220 done
1222 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
1223   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
1224 proof-
1225  from nz have ap: "a > 0" by simp
1227  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
1228    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
1229  moreover
1230     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
1231      from H have ?thesis by blast }
1232  moreover
1233  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
1234    {assume b0: "b = 0" with H  have ?thesis by simp}
1235    moreover
1236    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
1237      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
1238        by auto
1239      moreover
1240      {assume db: "d=b"
1241        from prems have ?thesis apply simp
1242 	 apply (rule exI[where x = b], simp)
1243 	 apply (rule exI[where x = b])
1244 	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
1245     moreover
1246     {assume db: "d < b"
1247 	{assume "x=0" hence ?thesis  using prems by simp }
1248 	moreover
1249 	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
1250 	  from db have "d \<le> b - 1" by simp
1251 	  hence "d*b \<le> b*(b - 1)" by simp
1252 	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
1253 	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
1254 	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
1255             by simp
1256 	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
1257 	    by (simp only: mult_assoc right_distrib)
1258 	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
1259             by algebra
1260 	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
1261 	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
1262 	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
1263 	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
1264 	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
1265 	  hence ?thesis using H(1,2)
1266 	    apply -
1267 	    apply (rule exI[where x=d], simp)
1268 	    apply (rule exI[where x="(b - 1) * y"])
1269 	    by (rule exI[where x="x*(b - 1) - d"], simp)}
1270 	ultimately have ?thesis by blast}
1271     ultimately have ?thesis by blast}
1272   ultimately have ?thesis by blast}
1273  ultimately show ?thesis by blast
1274 qed
1276 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
1277   shows "\<exists>x y. a * x = b * y + gcd a b"
1278 proof-
1279   let ?g = "gcd a b"
1280   from bezout_add_strong_nat[OF a, of b]
1281   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
1282   from d(1,2) have "d dvd ?g" by simp
1283   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
1284   from d(3) have "a * x * k = (b * y + d) *k " by auto
1285   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
1286   thus ?thesis by blast
1287 qed
1290 subsection {* LCM *}
1292 lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1293   by (simp add: lcm_int_def lcm_nat_def zdiv_int
1294     zmult_int [symmetric] gcd_int_def)
1296 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
1297   unfolding lcm_nat_def
1298   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
1300 lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
1301   unfolding lcm_int_def gcd_int_def
1302   apply (subst int_mult [symmetric])
1303   apply (subst prod_gcd_lcm_nat [symmetric])
1304   apply (subst nat_abs_mult_distrib [symmetric])
1305   apply (simp, simp add: abs_mult)
1306 done
1308 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
1309   unfolding lcm_nat_def by simp
1311 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
1312   unfolding lcm_int_def by simp
1314 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
1315   unfolding lcm_nat_def by simp
1317 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
1318   unfolding lcm_int_def by simp
1320 lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
1321   unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
1323 lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
1324   unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
1327 lemma lcm_pos_nat:
1328   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
1329 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
1331 lemma lcm_pos_int:
1332   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
1333   apply (subst lcm_abs_int)
1334   apply (rule lcm_pos_nat [transferred])
1335   apply auto
1336 done
1338 lemma dvd_pos_nat:
1339   fixes n m :: nat
1340   assumes "n > 0" and "m dvd n"
1341   shows "m > 0"
1342 using assms by (cases m) auto
1344 lemma lcm_least_nat:
1345   assumes "(m::nat) dvd k" and "n dvd k"
1346   shows "lcm m n dvd k"
1347 proof (cases k)
1348   case 0 then show ?thesis by auto
1349 next
1350   case (Suc _) then have pos_k: "k > 0" by auto
1351   from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
1352   with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
1353   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
1354   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
1355   from pos_k k_m have pos_p: "p > 0" by auto
1356   from pos_k k_n have pos_q: "q > 0" by auto
1357   have "k * k * gcd q p = k * gcd (k * q) (k * p)"
1358     by (simp add: mult_ac gcd_mult_distrib_nat)
1359   also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
1360     by (simp add: k_m [symmetric] k_n [symmetric])
1361   also have "\<dots> = k * p * q * gcd m n"
1362     by (simp add: mult_ac gcd_mult_distrib_nat)
1363   finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
1364     by (simp only: k_m [symmetric] k_n [symmetric])
1365   then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
1367   with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
1368     by simp
1369   with prod_gcd_lcm_nat [of m n]
1370   have "lcm m n * gcd q p * gcd m n = k * gcd m n"
1372   with pos_gcd have "lcm m n * gcd q p = k" by auto
1373   then show ?thesis using dvd_def by auto
1374 qed
1376 lemma lcm_least_int:
1377   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
1378 apply (subst lcm_abs_int)
1379 apply (rule dvd_trans)
1380 apply (rule lcm_least_nat [transferred, of _ "abs k" _])
1381 apply auto
1382 done
1384 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
1385 proof (cases m)
1386   case 0 then show ?thesis by simp
1387 next
1388   case (Suc _)
1389   then have mpos: "m > 0" by simp
1390   show ?thesis
1391   proof (cases n)
1392     case 0 then show ?thesis by simp
1393   next
1394     case (Suc _)
1395     then have npos: "n > 0" by simp
1396     have "gcd m n dvd n" by simp
1397     then obtain k where "n = gcd m n * k" using dvd_def by auto
1398     then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
1400     also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
1401     finally show ?thesis by (simp add: lcm_nat_def)
1402   qed
1403 qed
1405 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
1406   apply (subst lcm_abs_int)
1407   apply (rule dvd_trans)
1408   prefer 2
1409   apply (rule lcm_dvd1_nat [transferred])
1410   apply auto
1411 done
1413 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
1414   by (subst lcm_commute_nat, rule lcm_dvd1_nat)
1416 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
1417   by (subst lcm_commute_int, rule lcm_dvd1_int)
1419 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
1420 by(metis lcm_dvd1_nat dvd_trans)
1422 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
1423 by(metis lcm_dvd2_nat dvd_trans)
1425 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
1426 by(metis lcm_dvd1_int dvd_trans)
1428 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
1429 by(metis lcm_dvd2_int dvd_trans)
1431 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
1432     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1433   by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
1435 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
1436     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1437   by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
1439 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
1440   apply (rule sym)
1441   apply (subst lcm_unique_nat [symmetric])
1442   apply auto
1443 done
1445 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
1446   apply (rule sym)
1447   apply (subst lcm_unique_int [symmetric])
1448   apply auto
1449 done
1451 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
1452 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
1454 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
1455 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
1457 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
1458 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
1460 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
1461 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
1463 lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
1464 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
1466 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
1467 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
1469 lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
1470 by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
1472 lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
1473 by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
1475 lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
1476 lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
1478 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
1479 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
1481 lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
1482 proof qed (auto simp add: gcd_ac_nat)
1484 lemma fun_left_comm_idem_gcd_int: "fun_left_comm_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
1485 proof qed (auto simp add: gcd_ac_int)
1487 lemma fun_left_comm_idem_lcm_nat: "fun_left_comm_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
1488 proof qed (auto simp add: lcm_ac_nat)
1490 lemma fun_left_comm_idem_lcm_int: "fun_left_comm_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
1491 proof qed (auto simp add: lcm_ac_int)
1494 (* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
1496 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1497 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
1499 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1500 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
1502 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
1503 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
1505 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
1506 by (metis abs_minus_one abs_mult_self lcm_proj1_if_dvd_int lcm_unique_int one_dvd zmult_eq_1_iff)
1509 subsection {* Primes *}
1511 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
1513 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
1514   by (unfold prime_nat_def, auto)
1516 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
1517   by (unfold prime_nat_def, auto)
1519 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
1520   by (unfold prime_nat_def, auto)
1522 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
1523   by (unfold prime_nat_def, auto)
1525 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
1526   by (unfold prime_nat_def, auto)
1528 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
1529   by (unfold prime_nat_def, auto)
1531 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
1532   by (unfold prime_nat_def, auto)
1534 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
1535   by (unfold prime_int_def prime_nat_def) auto
1537 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
1538   by (unfold prime_int_def prime_nat_def, auto)
1540 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
1541   by (unfold prime_int_def prime_nat_def, auto)
1543 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
1544   by (unfold prime_int_def prime_nat_def, auto)
1546 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
1547   by (unfold prime_int_def prime_nat_def, auto)
1550 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
1551     m = 1 \<or> m = p))"
1552   using prime_nat_def [transferred]
1553     apply (case_tac "p >= 0")
1554     by (blast, auto simp add: prime_ge_0_int)
1556 (* To do: determine primality of any numeral *)
1558 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
1561 lemma zero_not_prime_int [simp]: "~prime (0::int)"
1564 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
1567 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
1568   by (simp add: prime_nat_def One_nat_def)
1570 lemma one_not_prime_int [simp]: "~prime (1::int)"
1573 lemma two_is_prime_nat [simp]: "prime (2::nat)"
1574   apply (auto simp add: prime_nat_def)
1575   apply (case_tac m)
1576   apply (auto dest!: dvd_imp_le)
1577   done
1579 lemma two_is_prime_int [simp]: "prime (2::int)"
1580   by (rule two_is_prime_nat [transferred direction: nat "op <= (0::int)"])
1582 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1583   apply (unfold prime_nat_def)
1584   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
1585   done
1587 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
1588   apply (unfold prime_int_altdef)
1589   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
1590   done
1592 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1593   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
1595 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
1596   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
1598 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
1599     p dvd m * n = (p dvd m \<or> p dvd n)"
1600   by (rule iffI, rule prime_dvd_mult_nat, auto)
1602 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
1603     p dvd m * n = (p dvd m \<or> p dvd n)"
1604   by (rule iffI, rule prime_dvd_mult_int, auto)
1606 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1607     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1608   unfolding prime_nat_def dvd_def apply auto
1609   by(metis mult_commute linorder_neq_iff linorder_not_le mult_1 n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
1611 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
1612     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
1613   unfolding prime_int_altdef dvd_def
1614   apply auto
1615   by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
1617 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
1618     n > 0 --> (p dvd x^n --> p dvd x)"
1619   by (induct n rule: nat_induct, auto)
1621 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
1622     n > 0 --> (p dvd x^n --> p dvd x)"
1623   apply (induct n rule: nat_induct, auto)
1624   apply (frule prime_ge_0_int)
1625   apply auto
1626 done
1628 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
1629     coprime a (p^m)"
1630   apply (rule coprime_exp_nat)
1631   apply (subst gcd_commute_nat)
1632   apply (erule (1) prime_imp_coprime_nat)
1633 done
1635 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow>
1636     coprime a (p^m)"
1637   apply (rule coprime_exp_int)
1638   apply (subst gcd_commute_int)
1639   apply (erule (1) prime_imp_coprime_int)
1640 done
1642 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1643   apply (rule prime_imp_coprime_nat, assumption)
1644   apply (unfold prime_nat_def, auto)
1645 done
1647 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
1648   apply (rule prime_imp_coprime_int, assumption)
1649   apply (unfold prime_int_altdef, clarify)
1650   apply (drule_tac x = q in spec)
1651   apply (drule_tac x = p in spec)
1652   apply auto
1653 done
1655 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
1656     coprime (p^m) (q^n)"
1657   by (rule coprime_exp2_nat, rule primes_coprime_nat)
1659 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow>
1660     coprime (p^m) (q^n)"
1661   by (rule coprime_exp2_int, rule primes_coprime_int)
1663 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
1664   apply (induct n rule: nat_less_induct)
1665   apply (case_tac "n = 0")
1666   using two_is_prime_nat apply blast
1667   apply (case_tac "prime n")
1668   apply blast
1669   apply (subgoal_tac "n > 1")
1670   apply (frule (1) not_prime_eq_prod_nat)
1671   apply (auto intro: dvd_mult dvd_mult2)
1672 done
1674 (* An Isar version:
1676 lemma prime_factor_b_nat:
1677   fixes n :: nat
1678   assumes "n \<noteq> 1"
1679   shows "\<exists>p. prime p \<and> p dvd n"
1681 using `n ~= 1`
1682 proof (induct n rule: less_induct_nat)
1683   fix n :: nat
1684   assume "n ~= 1" and
1685     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
1686   thus "\<exists>p. prime p \<and> p dvd n"
1687   proof -
1688   {
1689     assume "n = 0"
1690     moreover note two_is_prime_nat
1691     ultimately have ?thesis
1692       by (auto simp del: two_is_prime_nat)
1693   }
1694   moreover
1695   {
1696     assume "prime n"
1697     hence ?thesis by auto
1698   }
1699   moreover
1700   {
1701     assume "n ~= 0" and "~ prime n"
1702     with `n ~= 1` have "n > 1" by auto
1703     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
1704       "n = m * k" and "1 < m" and "m < n" by blast
1705     with ih obtain p where "prime p" and "p dvd m" by blast
1706     with `n = m * k` have ?thesis by auto
1707   }
1708   ultimately show ?thesis by blast
1709   qed
1710 qed
1712 *)
1714 text {* One property of coprimality is easier to prove via prime factors. *}
1716 lemma prime_divprod_pow_nat:
1717   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
1718   shows "p^n dvd a \<or> p^n dvd b"
1719 proof-
1720   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
1721       apply (cases "n=0", simp_all)
1722       apply (cases "a=1", simp_all) done}
1723   moreover
1724   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
1725     then obtain m where m: "n = Suc m" by (cases n, auto)
1726     from n have "p dvd p^n" by (intro dvd_power, auto)
1727     also note pab
1728     finally have pab': "p dvd a * b".
1729     from prime_dvd_mult_nat[OF p pab']
1730     have "p dvd a \<or> p dvd b" .
1731     moreover
1732     {assume pa: "p dvd a"
1733       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
1734       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
1735       with p have "coprime b p"
1736         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
1737       hence pnb: "coprime (p^n) b"
1738         by (subst gcd_commute_nat, rule coprime_exp_nat)
1739       from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
1740     moreover
1741     {assume pb: "p dvd b"
1742       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
1743       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
1744         by auto
1745       with p have "coprime a p"
1746         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
1747       hence pna: "coprime (p^n) a"
1748         by (subst gcd_commute_nat, rule coprime_exp_nat)
1749       from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
1750     ultimately have ?thesis by blast}
1751   ultimately show ?thesis by blast
1752 qed
1754 end