src/HOL/Number_Theory/Primes.thy
 author haftmann Wed Jun 02 16:24:14 2010 +0200 (2010-06-02) changeset 37294 a2a8216999a2 parent 35644 d20cf282342e child 37607 ebb8b1a79c4c permissions -rw-r--r--
absolute import -- must work with Main.thy / HOL-Proofs
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 *)
30 theory Primes
31 imports "~~/src/HOL/GCD"
32 begin
34 declare One_nat_def [simp del]
36 class prime = one +
38 fixes
39   prime :: "'a \<Rightarrow> bool"
41 instantiation nat :: prime
43 begin
45 definition
46   prime_nat :: "nat \<Rightarrow> bool"
47 where
48   [code del]: "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
50 instance proof qed
52 end
54 instantiation int :: prime
56 begin
58 definition
59   prime_int :: "int \<Rightarrow> bool"
60 where
61   [code del]: "prime_int p = prime (nat p)"
63 instance proof qed
65 end
68 subsection {* Set up Transfer *}
71 lemma transfer_nat_int_prime:
72   "(x::int) >= 0 \<Longrightarrow> prime (nat x) = prime x"
73   unfolding gcd_int_def lcm_int_def prime_int_def
74   by auto
77     transfer_nat_int_prime]
79 lemma transfer_int_nat_prime:
80   "prime (int x) = prime x"
81   by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
84     transfer_int_nat_prime]
87 subsection {* Primes *}
89 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
90   unfolding prime_nat_def
91   apply (subst even_mult_two_ex)
92   apply clarify
93   apply (drule_tac x = 2 in spec)
94   apply auto
95 done
97 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
98   unfolding prime_int_def
99   apply (frule prime_odd_nat)
100   apply (auto simp add: even_nat_def)
101 done
103 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
105 lemma prime_ge_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 0"
106   by (unfold prime_nat_def, auto)
108 lemma prime_gt_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 0"
109   by (unfold prime_nat_def, auto)
111 lemma prime_ge_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 1"
112   by (unfold prime_nat_def, auto)
114 lemma prime_gt_1_nat [elim]: "prime (p::nat) \<Longrightarrow> p > 1"
115   by (unfold prime_nat_def, auto)
117 lemma prime_ge_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= Suc 0"
118   by (unfold prime_nat_def, auto)
120 lemma prime_gt_Suc_0_nat [elim]: "prime (p::nat) \<Longrightarrow> p > Suc 0"
121   by (unfold prime_nat_def, auto)
123 lemma prime_ge_2_nat [elim]: "prime (p::nat) \<Longrightarrow> p >= 2"
124   by (unfold prime_nat_def, auto)
126 lemma prime_ge_0_int [elim]: "prime (p::int) \<Longrightarrow> p >= 0"
127   by (unfold prime_int_def prime_nat_def) auto
129 lemma prime_gt_0_int [elim]: "prime (p::int) \<Longrightarrow> p > 0"
130   by (unfold prime_int_def prime_nat_def, auto)
132 lemma prime_ge_1_int [elim]: "prime (p::int) \<Longrightarrow> p >= 1"
133   by (unfold prime_int_def prime_nat_def, auto)
135 lemma prime_gt_1_int [elim]: "prime (p::int) \<Longrightarrow> p > 1"
136   by (unfold prime_int_def prime_nat_def, auto)
138 lemma prime_ge_2_int [elim]: "prime (p::int) \<Longrightarrow> p >= 2"
139   by (unfold prime_int_def prime_nat_def, auto)
142 lemma prime_int_altdef: "prime (p::int) = (1 < p \<and> (\<forall>m \<ge> 0. m dvd p \<longrightarrow>
143     m = 1 \<or> m = p))"
144   using prime_nat_def [transferred]
145     apply (case_tac "p >= 0")
146     by (blast, auto simp add: prime_ge_0_int)
148 lemma prime_imp_coprime_nat: "prime (p::nat) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
149   apply (unfold prime_nat_def)
150   apply (metis gcd_dvd1_nat gcd_dvd2_nat)
151   done
153 lemma prime_imp_coprime_int: "prime (p::int) \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
154   apply (unfold prime_int_altdef)
155   apply (metis gcd_dvd1_int gcd_dvd2_int gcd_ge_0_int)
156   done
158 lemma prime_dvd_mult_nat: "prime (p::nat) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
159   by (blast intro: coprime_dvd_mult_nat prime_imp_coprime_nat)
161 lemma prime_dvd_mult_int: "prime (p::int) \<Longrightarrow> p dvd m * n \<Longrightarrow> p dvd m \<or> p dvd n"
162   by (blast intro: coprime_dvd_mult_int prime_imp_coprime_int)
164 lemma prime_dvd_mult_eq_nat [simp]: "prime (p::nat) \<Longrightarrow>
165     p dvd m * n = (p dvd m \<or> p dvd n)"
166   by (rule iffI, rule prime_dvd_mult_nat, auto)
168 lemma prime_dvd_mult_eq_int [simp]: "prime (p::int) \<Longrightarrow>
169     p dvd m * n = (p dvd m \<or> p dvd n)"
170   by (rule iffI, rule prime_dvd_mult_int, auto)
172 lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
173     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
174   unfolding prime_nat_def dvd_def apply auto
175   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)
177 lemma not_prime_eq_prod_int: "(n::int) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
178     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
179   unfolding prime_int_altdef dvd_def
180   apply auto
181   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)
183 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
184     n > 0 --> (p dvd x^n --> p dvd x)"
185   by (induct n rule: nat_induct, auto)
187 lemma prime_dvd_power_int [rule_format]: "prime (p::int) -->
188     n > 0 --> (p dvd x^n --> p dvd x)"
189   apply (induct n rule: nat_induct, auto)
190   apply (frule prime_ge_0_int)
191   apply auto
192 done
194 subsubsection{* Make prime naively executable *}
196 lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
199 lemma zero_not_prime_int [simp]: "~prime (0::int)"
202 lemma one_not_prime_nat [simp]: "~prime (1::nat)"
205 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
206   by (simp add: prime_nat_def One_nat_def)
208 lemma one_not_prime_int [simp]: "~prime (1::int)"
211 lemma prime_nat_code[code]:
212  "prime(p::nat) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))"
214 apply (metis less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
215 done
217 lemma prime_nat_simp:
218  "prime(p::nat) = (p > 1 & (list_all (%n. ~ n dvd p) [2..<p]))"
219 apply(simp only:prime_nat_code list_ball_code greaterThanLessThan_upt)
221 done
223 lemmas prime_nat_simp_number_of[simp] = prime_nat_simp[of "number_of m", standard]
225 lemma prime_int_code[code]:
226   "prime(p::int) = (p > 1 & (ALL n : {1<..<p}. ~(n dvd p)))" (is "?L = ?R")
227 proof
228   assume "?L" thus "?R"
229     by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
230 next
231     assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
232 qed
234 lemma prime_int_simp:
235   "prime(p::int) = (p > 1 & (list_all (%n. ~ n dvd p) [2..p - 1]))"
236 apply(simp only:prime_int_code list_ball_code greaterThanLessThan_upto)
237 apply simp
238 done
240 lemmas prime_int_simp_number_of[simp] = prime_int_simp[of "number_of m", standard]
242 lemma two_is_prime_nat [simp]: "prime (2::nat)"
243 by simp
245 lemma two_is_prime_int [simp]: "prime (2::int)"
246 by simp
248 text{* A bit of regression testing: *}
250 lemma "prime(97::nat)"
251 by simp
253 lemma "prime(97::int)"
254 by simp
256 lemma "prime(997::nat)"
257 by eval
259 lemma "prime(997::int)"
260 by eval
263 lemma prime_imp_power_coprime_nat: "prime (p::nat) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
264   apply (rule coprime_exp_nat)
265   apply (subst gcd_commute_nat)
266   apply (erule (1) prime_imp_coprime_nat)
267 done
269 lemma prime_imp_power_coprime_int: "prime (p::int) \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
270   apply (rule coprime_exp_int)
271   apply (subst gcd_commute_int)
272   apply (erule (1) prime_imp_coprime_int)
273 done
275 lemma primes_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
276   apply (rule prime_imp_coprime_nat, assumption)
277   apply (unfold prime_nat_def, auto)
278 done
280 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
281   apply (rule prime_imp_coprime_int, assumption)
282   apply (unfold prime_int_altdef, clarify)
283   apply (drule_tac x = q in spec)
284   apply (drule_tac x = p in spec)
285   apply auto
286 done
288 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
289   by (rule coprime_exp2_nat, rule primes_coprime_nat)
291 lemma primes_imp_powers_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
292   by (rule coprime_exp2_int, rule primes_coprime_int)
294 lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
295   apply (induct n rule: nat_less_induct)
296   apply (case_tac "n = 0")
297   using two_is_prime_nat apply blast
298   apply (case_tac "prime n")
299   apply blast
300   apply (subgoal_tac "n > 1")
301   apply (frule (1) not_prime_eq_prod_nat)
302   apply (auto intro: dvd_mult dvd_mult2)
303 done
305 (* An Isar version:
307 lemma prime_factor_b_nat:
308   fixes n :: nat
309   assumes "n \<noteq> 1"
310   shows "\<exists>p. prime p \<and> p dvd n"
312 using `n ~= 1`
313 proof (induct n rule: less_induct_nat)
314   fix n :: nat
315   assume "n ~= 1" and
316     ih: "\<forall>m<n. m \<noteq> 1 \<longrightarrow> (\<exists>p. prime p \<and> p dvd m)"
317   thus "\<exists>p. prime p \<and> p dvd n"
318   proof -
319   {
320     assume "n = 0"
321     moreover note two_is_prime_nat
322     ultimately have ?thesis
323       by (auto simp del: two_is_prime_nat)
324   }
325   moreover
326   {
327     assume "prime n"
328     hence ?thesis by auto
329   }
330   moreover
331   {
332     assume "n ~= 0" and "~ prime n"
333     with `n ~= 1` have "n > 1" by auto
334     with `~ prime n` and not_prime_eq_prod_nat obtain m k where
335       "n = m * k" and "1 < m" and "m < n" by blast
336     with ih obtain p where "prime p" and "p dvd m" by blast
337     with `n = m * k` have ?thesis by auto
338   }
339   ultimately show ?thesis by blast
340   qed
341 qed
343 *)
345 text {* One property of coprimality is easier to prove via prime factors. *}
347 lemma prime_divprod_pow_nat:
348   assumes p: "prime (p::nat)" and ab: "coprime a b" and pab: "p^n dvd a * b"
349   shows "p^n dvd a \<or> p^n dvd b"
350 proof-
351   {assume "n = 0 \<or> a = 1 \<or> b = 1" with pab have ?thesis
352       apply (cases "n=0", simp_all)
353       apply (cases "a=1", simp_all) done}
354   moreover
355   {assume n: "n \<noteq> 0" and a: "a\<noteq>1" and b: "b\<noteq>1"
356     then obtain m where m: "n = Suc m" by (cases n, auto)
357     from n have "p dvd p^n" by (intro dvd_power, auto)
358     also note pab
359     finally have pab': "p dvd a * b".
360     from prime_dvd_mult_nat[OF p pab']
361     have "p dvd a \<or> p dvd b" .
362     moreover
363     { assume pa: "p dvd a"
364       from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
365       with p have "coprime b p"
366         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
367       hence pnb: "coprime (p^n) b"
368         by (subst gcd_commute_nat, rule coprime_exp_nat)
369       from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
370     moreover
371     { assume pb: "p dvd b"
372       have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
373       from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
374         by auto
375       with p have "coprime a p"
376         by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
377       hence pna: "coprime (p^n) a"
378         by (subst gcd_commute_nat, rule coprime_exp_nat)
379       from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
380     ultimately have ?thesis by blast}
381   ultimately show ?thesis by blast
382 qed
384 subsection {* Infinitely many primes *}
386 lemma next_prime_bound: "\<exists>(p::nat). prime p \<and> n < p \<and> p <= fact n + 1"
387 proof-
388   have f1: "fact n + 1 \<noteq> 1" using fact_ge_one_nat [of n] by arith
389   from prime_factor_nat [OF f1]
390       obtain p where "prime p" and "p dvd fact n + 1" by auto
391   hence "p \<le> fact n + 1"
392     by (intro dvd_imp_le, auto)
393   {assume "p \<le> n"
394     from `prime p` have "p \<ge> 1"
395       by (cases p, simp_all)
396     with `p <= n` have "p dvd fact n"
397       by (intro dvd_fact_nat)
398     with `p dvd fact n + 1` have "p dvd fact n + 1 - fact n"
399       by (rule dvd_diff_nat)
400     hence "p dvd 1" by simp
401     hence "p <= 1" by auto
402     moreover from `prime p` have "p > 1" by auto
403     ultimately have False by auto}
404   hence "n < p" by arith
405   with `prime p` and `p <= fact n + 1` show ?thesis by auto
406 qed
408 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
409 using next_prime_bound by auto
411 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
412 proof
413   assume "finite {(p::nat). prime p}"
414   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
415     by auto
416   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
417     by auto
418   with bigger_prime [of b] show False by auto
419 qed
422 end