src/HOL/Number_Theory/Primes.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58645 94bef115c08f child 58898 1ebf0a1f12a4 permissions -rw-r--r--
modernized header uniformly as section;
1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
5 This file deals with properties of primes. Definitions and lemmas are
6 proved uniformly for the natural numbers and integers.
8 This file combines and revises a number of prior developments.
10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
11 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
12 gcd, lcm, and prime for the natural numbers.
14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
16 another extension of the notions to the integers, and added a number
17 of results to "Primes" and "GCD". IntPrimes also defined and developed
18 the congruence relations on the integers. The notion was extended to
19 the natural numbers by Chaieb.
21 Jeremy Avigad combined all of these, made everything uniform for the
22 natural numbers and the integers, and added a number of new theorems.
24 Tobias Nipkow cleaned up a lot.
25 *)
28 section {* Primes *}
30 theory Primes
31 imports "~~/src/HOL/GCD"
32 begin
34 declare [[coercion int]]
35 declare [[coercion_enabled]]
37 definition prime :: "nat \<Rightarrow> bool"
38   where "prime p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
40 lemmas prime_nat_def = prime_def
43 subsection {* Primes *}
45 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
46   apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
47   apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
48   done
50 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
52 lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
53   unfolding prime_nat_def by auto
55 lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
56   unfolding prime_nat_def by auto
58 lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
59   unfolding prime_nat_def by auto
61 lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
62   unfolding prime_nat_def by auto
64 lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
65   unfolding prime_nat_def by auto
67 lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
68   unfolding prime_nat_def by auto
70 lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
71   apply (unfold prime_nat_def)
72   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
73   done
75 lemma prime_int_altdef:
76   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
77     m = 1 \<or> m = p))"
78   apply (simp add: prime_def)
79   apply (auto simp add: )
80   apply (metis One_nat_def int_1 nat_0_le nat_dvd_iff)
81   apply (metis zdvd_int One_nat_def le0 of_nat_0 of_nat_1 of_nat_eq_iff of_nat_le_iff)
82   done
84 lemma prime_imp_coprime_int:
85   fixes n::int shows "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
86   apply (unfold prime_int_altdef)
87   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
88   done
90 lemma prime_dvd_mult_nat: "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
91   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
93 lemma prime_dvd_mult_int:
94   fixes n::int shows "prime p \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
95   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
97 lemma prime_dvd_mult_eq_nat [simp]: "prime p \<Longrightarrow>
98     p dvd m * n = (p dvd m \<or> p dvd n)"
99   by (rule iffI, rule prime_dvd_mult_nat, auto)
101 lemma prime_dvd_mult_eq_int [simp]:
102   fixes n::int
103   shows "prime p \<Longrightarrow> p dvd m * n = (p dvd m \<or> p dvd n)"
104   by (rule iffI, rule prime_dvd_mult_int, auto)
106 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
107     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
108   unfolding prime_nat_def dvd_def apply auto
109   by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
110       n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
112 lemma prime_dvd_power_nat: "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
113   by (induct n) auto
115 lemma prime_dvd_power_int:
116   fixes x::int shows "prime p \<Longrightarrow> p dvd x^n \<Longrightarrow> p dvd x"
117   by (induct n) auto
119 lemma prime_dvd_power_nat_iff: "prime p \<Longrightarrow> n > 0 \<Longrightarrow>
120     p dvd x^n \<longleftrightarrow> p dvd x"
121   by (cases n) (auto elim: prime_dvd_power_nat)
123 lemma prime_dvd_power_int_iff:
124   fixes x::int
125   shows "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x^n \<longleftrightarrow> p dvd x"
126   by (cases n) (auto elim: prime_dvd_power_int)
129 subsubsection {* Make prime naively executable *}
131 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
132   by (simp add: prime_nat_def)
134 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
135   by (simp add: prime_nat_def)
137 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
138   by (simp add: prime_nat_def)
140 lemma prime_nat_code [code]:
141     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
142   apply (simp add: Ball_def)
143   apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
144   done
146 lemma prime_nat_simp:
147     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
148   by (auto simp add: prime_nat_code)
150 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
152 lemma two_is_prime_nat [simp]: "prime (2::nat)"
153   by simp
155 text{* A bit of regression testing: *}
157 lemma "prime(97::nat)" by simp
158 lemma "prime(997::nat)" by eval
161 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
162   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
164 lemma prime_imp_power_coprime_int:
165   fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
166   by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
168 lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
169   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
171 lemma primes_imp_powers_coprime_nat:
172     "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
173   by (rule coprime_exp2_nat, rule primes_coprime_nat)
175 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
176   apply (induct n rule: nat_less_induct)
177   apply (case_tac "n = 0")
178   using two_is_prime_nat
179   apply blast
180   apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
181     nat_dvd_not_less neq0_conv prime_nat_def)
182   done
184 text {* One property of coprimality is easier to prove via prime factors. *}
186 lemma prime_divprod_pow_nat:
187   assumes p: "prime p" and ab: "coprime a b" and pab: "p^n dvd a * b"
188   shows "p^n dvd a \<or> p^n dvd b"
189 proof-
190   { assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
191       apply (cases "n=0", simp_all)
192       apply (cases "a=1", simp_all)
193       done }
194   moreover
195   { assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
196     then obtain m where m: "n = Suc m" by (cases n) auto
197     from n have "p dvd p^n" apply (intro dvd_power) apply auto done
198     also note pab
199     finally have pab': "p dvd a * b".
200     from prime_dvd_mult_nat[OF p pab']
201     have "p dvd a \<or> p dvd b" .
202     moreover
203     { assume pa: "p dvd a"
204       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
205       with p have "coprime b p"
206         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
207       then have pnb: "coprime (p^n) b"
208         by (subst gcd_commute_nat, rule coprime_exp_nat)
209       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
210     moreover
211     { assume pb: "p dvd b"
212       have pnba: "p^n dvd b*a" using pab by (simp add: mult.commute)
213       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
214         by auto
215       with p have "coprime a p"
216         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
217       then have pna: "coprime (p^n) a"
218         by (subst gcd_commute_nat, rule coprime_exp_nat)
219       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
220     ultimately have ?thesis by blast }
221   ultimately show ?thesis by blast
222 qed
225 subsection {* Infinitely many primes *}
227 lemma next_prime_bound: "\<exists>p. prime p \<and> n < p \<and> p <= fact n + 1"
228 proof-
229   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
230   from prime_factor_nat [OF f1]
231   obtain p where "prime p" and "p dvd fact n + 1" by auto
232   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
233   { assume "p \<le> n"
234     from `prime p` have "p \<ge> 1"
235       by (cases p, simp_all)
236     with `p <= n` have "p dvd fact n"
237       by (intro dvd_fact_nat)
238     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
239       by (rule dvd_diff_nat)
240     then have "p dvd 1" by simp
241     then have "p <= 1" by auto
242     moreover from `prime p` have "p > 1" by auto
243     ultimately have False by auto}
244   then have "n < p" by presburger
245   with `prime p` and `p <= fact n + 1` show ?thesis by auto
246 qed
248 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
249   using next_prime_bound by auto
251 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
252 proof
253   assume "finite {(p::nat). prime p}"
254   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
255     by auto
256   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
257     by auto
258   with bigger_prime [of b] show False
259     by auto
260 qed
262 subsection{*Powers of Primes*}
264 text{*Versions for type nat only*}
266 lemma prime_product:
267   fixes p::nat
268   assumes "prime (p * q)"
269   shows "p = 1 \<or> q = 1"
270 proof -
271   from assms have
272     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
273     unfolding prime_nat_def by auto
274   from `1 < p * q` have "p \<noteq> 0" by (cases p) auto
275   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
276   have "p dvd p * q" by simp
277   then have "p = 1 \<or> p = p * q" by (rule P)
278   then show ?thesis by (simp add: Q)
279 qed
281 lemma prime_exp:
282   fixes p::nat
283   shows "prime (p^n) \<longleftrightarrow> prime p \<and> n = 1"
284 proof(induct n)
285   case 0 thus ?case by simp
286 next
287   case (Suc n)
288   {assume "p = 0" hence ?case by simp}
289   moreover
290   {assume "p=1" hence ?case by simp}
291   moreover
292   {assume p: "p \<noteq> 0" "p\<noteq>1"
293     {assume pp: "prime (p^Suc n)"
294       hence "p = 1 \<or> p^n = 1" using prime_product[of p "p^n"] by simp
295       with p have n: "n = 0"
296         by (metis One_nat_def nat_power_eq_Suc_0_iff)
297       with pp have "prime p \<and> Suc n = 1" by simp}
298     moreover
299     {assume n: "prime p \<and> Suc n = 1" hence "prime (p^Suc n)" by simp}
300     ultimately have ?case by blast}
301   ultimately show ?case by blast
302 qed
304 lemma prime_power_mult:
305   fixes p::nat
306   assumes p: "prime p" and xy: "x * y = p ^ k"
307   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
308 using xy
309 proof(induct k arbitrary: x y)
310   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
311 next
312   case (Suc k x y)
313   from Suc.prems have pxy: "p dvd x*y" by auto
314   from Primes.prime_dvd_mult_nat [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
315   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
316   {assume px: "p dvd x"
317     then obtain d where d: "x = p*d" unfolding dvd_def by blast
318     from Suc.prems d  have "p*d*y = p^Suc k" by simp
319     hence th: "d*y = p^k" using p0 by simp
320     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
321     with d have "x = p^Suc i" by simp
322     with ij(2) have ?case by blast}
323   moreover
324   {assume px: "p dvd y"
325     then obtain d where d: "y = p*d" unfolding dvd_def by blast
326     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
327     hence th: "d*x = p^k" using p0 by simp
328     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
329     with d have "y = p^Suc i" by simp
330     with ij(2) have ?case by blast}
331   ultimately show ?case  using pxyc by blast
332 qed
334 lemma prime_power_exp:
335   fixes p::nat
336   assumes p: "prime p" and n: "n \<noteq> 0"
337     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
338   using n xn
339 proof(induct n arbitrary: k)
340   case 0 thus ?case by simp
341 next
342   case (Suc n k) hence th: "x*x^n = p^k" by simp
343   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
344   moreover
345   {assume n: "n \<noteq> 0"
346     from prime_power_mult[OF p th]
347     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
348     from Suc.hyps[OF n ij(2)] have ?case .}
349   ultimately show ?case by blast
350 qed
352 lemma divides_primepow:
353   fixes p::nat
354   assumes p: "prime p"
355   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
356 proof
357   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
358     unfolding dvd_def  apply (auto simp add: mult.commute) by blast
359   from prime_power_mult[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
360   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
361   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
362   hence "i \<le> k" by arith
363   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
364 next
365   {fix i assume H: "i \<le> k" "d = p^i"
366     then obtain j where j: "k = i + j"
367       by (metis le_add_diff_inverse)
368     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
369     hence "d dvd p^k" unfolding dvd_def by auto}
370   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
371 qed
373 subsection {*Chinese Remainder Theorem Variants*}
375 lemma bezout_gcd_nat:
376   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
377   using bezout_nat[of a b]
378 by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
379   gcd_nat.right_neutral mult_0)
381 lemma gcd_bezout_sum_nat:
382   fixes a::nat
383   assumes "a * x + b * y = d"
384   shows "gcd a b dvd d"
385 proof-
386   let ?g = "gcd a b"
387     have dv: "?g dvd a*x" "?g dvd b * y"
388       by simp_all
389     from dvd_add[OF dv] assms
390     show ?thesis by auto
391 qed
394 text {* A binary form of the Chinese Remainder Theorem. *}
396 lemma chinese_remainder:
397   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
398   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
399 proof-
400   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
401   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
402     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
403   then have d12: "d1 = 1" "d2 =1"
404     by (metis ab coprime_nat)+
405   let ?x = "v * a * x1 + u * b * x2"
406   let ?q1 = "v * x1 + u * y2"
407   let ?q2 = "v * y1 + u * x2"
408   from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
409   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
410     by algebra+
411   thus ?thesis by blast
412 qed
414 text {* Primality *}
416 lemma coprime_bezout_strong:
417   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
418   shows "\<exists>x y. a * x = b * y + 1"
419 by (metis assms bezout_nat gcd_nat.left_neutral)
421 lemma bezout_prime:
422   assumes p: "prime p" and pa: "\<not> p dvd a"
423   shows "\<exists>x y. a*x = Suc (p*y)"
424 proof-
425   have ap: "coprime a p"
426     by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
427   from coprime_bezout_strong[OF ap] show ?thesis
428     by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
429 qed
431 end