src/HOL/Computational_Algebra/Primes.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 65583 8d53b3bebab4 child 66453 cc19f7ca2ed6 permissions -rw-r--r--
executable domain membership checks
1 (*  Title:      HOL/Computational_Algebra/Primes.thy
2     Author:     Christophe Tabacznyj
3     Author:     Lawrence C. Paulson
4     Author:     Amine Chaieb
5     Author:     Thomas M. Rasmussen
6     Author:     Jeremy Avigad
7     Author:     Tobias Nipkow
8     Author:     Manuel Eberl
10 This theory deals with properties of primes. Definitions and lemmas are
11 proved uniformly for the natural numbers and integers.
13 This file combines and revises a number of prior developments.
15 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
16 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
17 gcd, lcm, and prime for the natural numbers.
19 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
20 extended gcd, lcm, primes to the integers. Amine Chaieb provided
21 another extension of the notions to the integers, and added a number
22 of results to "Primes" and "GCD". IntPrimes also defined and developed
23 the congruence relations on the integers. The notion was extended to
24 the natural numbers by Chaieb.
26 Jeremy Avigad combined all of these, made everything uniform for the
27 natural numbers and the integers, and added a number of new theorems.
29 Tobias Nipkow cleaned up a lot.
31 Florian Haftmann and Manuel Eberl put primality and prime factorisation
32 onto an algebraic foundation and thus generalised these concepts to
33 other rings, such as polynomials. (see also the Factorial_Ring theory).
35 There were also previous formalisations of unique factorisation by
36 Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
37 *)
39 section \<open>Primes\<close>
41 theory Primes
42 imports "~~/src/HOL/Binomial" Euclidean_Algorithm
43 begin
45 (* As a simp or intro rule,
47      prime p \<Longrightarrow> p > 0
49    wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
50    leads to the backchaining
52      x > 0
53      prime x
54      x \<in># M   which is, unfortunately,
55      count M x > 0
56 *)
58 declare [[coercion int]]
59 declare [[coercion_enabled]]
61 lemma prime_elem_nat_iff:
62   "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
63 proof safe
64   assume *: "prime_elem n"
65   from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
66   thus "n > 1" by (cases n) simp_all
67   fix m assume m: "m dvd n" "m \<noteq> n"
68   from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
69     by (intro irreducibleD' prime_elem_imp_irreducible)
70   with m show "m = 1" by (auto dest: dvd_antisym)
71 next
72   assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
73   thus "prime_elem n"
74     by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
75 qed
77 lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
78   by (simp add: prime_def)
80 lemma prime_nat_iff:
81   "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
82   by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
84 lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
85 proof
86   assume "prime_elem n"
87   thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
88 next
89   assume "prime_elem (nat (abs n))"
90   thus "prime_elem n"
91     by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
92 qed
94 lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
95   by (auto simp: prime_elem_int_nat_transfer)
97 lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
98   by (auto simp: prime_elem_int_nat_transfer prime_def)
100 lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
101   by (auto simp: prime_elem_int_nat_transfer prime_def)
103 lemma prime_int_iff:
104   "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
105 proof (intro iffI conjI allI impI; (elim conjE)?)
106   assume *: "prime n"
107   hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
108   from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
109     by (auto simp: prime_def zabs_def not_less split: if_splits)
110   thus "n > 1" by presburger
111   fix m assume "m dvd n" \<open>m \<ge> 0\<close>
112   with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
113   with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
114     using associated_iff_dvd[of m n] by auto
115 next
116   assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
117   hence "nat n > 1" by simp
118   moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
119   proof (intro allI impI)
120     fix m assume "m dvd nat n"
121     with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
122     with n(2) have "int m = 1 \<or> int m = n"
123       using of_nat_0_le_iff by blast
124     thus "m = 1 \<or> m = nat n" by auto
125   qed
126   ultimately show "prime n"
127     unfolding prime_int_nat_transfer prime_nat_iff by auto
128 qed
131 lemma prime_nat_not_dvd:
132   assumes "prime p" "p > n" "n \<noteq> (1::nat)"
133   shows   "\<not>n dvd p"
134 proof
135   assume "n dvd p"
136   from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
137   from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
138     by (cases "n = 0") (auto dest!: dvd_imp_le)
139 qed
141 lemma prime_int_not_dvd:
142   assumes "prime p" "p > n" "n > (1::int)"
143   shows   "\<not>n dvd p"
144 proof
145   assume "n dvd p"
146   from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
147   from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
148     by (auto dest!: zdvd_imp_le)
149 qed
151 lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
152   by (intro prime_nat_not_dvd) auto
154 lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
155   by (intro prime_int_not_dvd) auto
157 lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
158   unfolding prime_int_iff by auto
160 lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
161   unfolding prime_nat_iff by auto
163 lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
164   unfolding prime_int_iff by auto
166 lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
167   unfolding prime_nat_iff by auto
169 lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
170   unfolding prime_nat_iff by auto
172 lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
173   unfolding prime_int_iff by auto
175 lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
176   unfolding prime_nat_iff by auto
178 lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
179   unfolding prime_nat_iff by auto
181 lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
182   unfolding prime_int_iff by auto
184 lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
185   unfolding prime_nat_iff by auto
187 lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
188   unfolding prime_int_iff by auto
190 lemma prime_int_altdef:
191   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
192     m = 1 \<or> m = p))"
193   unfolding prime_int_iff by blast
195 lemma not_prime_eq_prod_nat:
196   assumes "m > 1" "\<not>prime (m::nat)"
197   shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
198   using assms irreducible_altdef[of m]
199   by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
202 subsection\<open>Largest exponent of a prime factor\<close>
203 text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
205 lemma prime_power_cancel_less:
206   assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and less: "k < k'" and "\<not> p dvd m"
207   shows False
208 proof -
209   obtain l where l: "k' = k + l" and "l > 0"
210     using less less_imp_add_positive by auto
211   have "m = m * (p ^ k) div (p ^ k)"
212     using \<open>prime p\<close> by simp
213   also have "\<dots> = m' * (p ^ k') div (p ^ k)"
214     using eq by simp
215   also have "\<dots> = m' * (p ^ l) * (p ^ k) div (p ^ k)"
216     by (simp add: l mult.commute mult.left_commute power_add)
217   also have "... = m' * (p ^ l)"
218     using \<open>prime p\<close> by simp
219   finally have "p dvd m"
220     using \<open>l > 0\<close> by simp
221   with assms show False
222     by simp
223 qed
225 lemma prime_power_cancel:
226   assumes "prime p" and eq: "m * (p ^ k) = m' * (p ^ k')" and "\<not> p dvd m" "\<not> p dvd m'"
227   shows "k = k'"
228   using prime_power_cancel_less [OF \<open>prime p\<close>] assms
229   by (metis linorder_neqE_nat)
231 lemma prime_power_cancel2:
232   assumes "prime p" "m * (p ^ k) = m' * (p ^ k')" "\<not> p dvd m" "\<not> p dvd m'"
233   obtains "m = m'" "k = k'"
234   using prime_power_cancel [OF assms] assms by auto
236 lemma prime_power_canonical:
237   fixes m::nat
238   assumes "prime p" "m > 0"
239   shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
240 using \<open>m > 0\<close>
241 proof (induction m rule: less_induct)
242   case (less m)
243   show ?case
244   proof (cases "p dvd m")
245     case True
246     then obtain m' where m': "m = p * m'"
247       using dvdE by blast
248     with \<open>prime p\<close> have "0 < m'" "m' < m"
249       using less.prems prime_nat_iff by auto
250     with m' less show ?thesis
251       by (metis power_Suc mult.left_commute)
252   next
253     case False
254     then show ?thesis
255       by (metis mult.right_neutral power_0)
256   qed
257 qed
260 subsubsection \<open>Make prime naively executable\<close>
262 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
263   unfolding One_nat_def [symmetric] by (rule not_prime_1)
265 lemma prime_nat_iff':
266   "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
267 proof safe
268   assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
269   show "prime p" unfolding prime_nat_iff
270   proof (intro conjI allI impI)
271     fix m assume "m dvd p"
272     with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
273     hence "m \<ge> 1" by simp
274     moreover from \<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast
275     with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
276     ultimately show "m = 1 \<or> m = p" by simp
277   qed fact+
278 qed (auto simp: prime_nat_iff)
280 lemma prime_int_iff':
281   "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
282 proof
283   assume "?lhs"
284   thus "?rhs"
285       by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_iff')
286 next
287   assume "?rhs"
288   thus "?lhs"
289     by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_iff')
290 qed
292 lemma prime_int_numeral_eq [simp]:
293   "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
294   by (simp add: prime_int_nat_transfer)
296 lemma two_is_prime_nat [simp]: "prime (2::nat)"
297   by (simp add: prime_nat_iff')
299 lemma prime_nat_numeral_eq [simp]:
300   "prime (numeral m :: nat) \<longleftrightarrow>
301     (1::nat) < numeral m \<and>
302     (\<forall>n::nat \<in> set [2..<numeral m]. \<not> n dvd numeral m)"
303   by (simp only: prime_nat_iff' set_upt)  \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
306 text\<open>A bit of regression testing:\<close>
308 lemma "prime(97::nat)" by simp
309 lemma "prime(97::int)" by simp
311 lemma prime_factor_nat:
312   "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
313   using prime_divisor_exists[of n]
314   by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
317 subsection \<open>Infinitely many primes\<close>
319 lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
320 proof-
321   have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
322   from prime_factor_nat [OF f1]
323   obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
324   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
325   { assume "p \<le> n"
326     from \<open>prime p\<close> have "p \<ge> 1"
327       by (cases p, simp_all)
328     with \<open>p <= n\<close> have "p dvd fact n"
329       by (intro dvd_fact)
330     with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
331       by (rule dvd_diff_nat)
332     then have "p dvd 1" by simp
333     then have "p <= 1" by auto
334     moreover from \<open>prime p\<close> have "p > 1"
335       using prime_nat_iff by blast
336     ultimately have False by auto}
337   then have "n < p" by presburger
338   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
339 qed
341 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
342   using next_prime_bound by auto
344 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
345 proof
346   assume "finite {(p::nat). prime p}"
347   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
348     by auto
349   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
350     by auto
351   with bigger_prime [of b] show False
352     by auto
353 qed
355 subsection\<open>Powers of Primes\<close>
357 text\<open>Versions for type nat only\<close>
359 lemma prime_product:
360   fixes p::nat
361   assumes "prime (p * q)"
362   shows "p = 1 \<or> q = 1"
363 proof -
364   from assms have
365     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
366     unfolding prime_nat_iff by auto
367   from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
368   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
369   have "p dvd p * q" by simp
370   then have "p = 1 \<or> p = p * q" by (rule P)
371   then show ?thesis by (simp add: Q)
372 qed
374 (* TODO: Generalise? *)
375 lemma prime_power_mult_nat:
376   fixes p::nat
377   assumes p: "prime p" and xy: "x * y = p ^ k"
378   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
379 using xy
380 proof(induct k arbitrary: x y)
381   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
382 next
383   case (Suc k x y)
384   from Suc.prems have pxy: "p dvd x*y" by auto
385   from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
386   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
387   {assume px: "p dvd x"
388     then obtain d where d: "x = p*d" unfolding dvd_def by blast
389     from Suc.prems d  have "p*d*y = p^Suc k" by simp
390     hence th: "d*y = p^k" using p0 by simp
391     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
392     with d have "x = p^Suc i" by simp
393     with ij(2) have ?case by blast}
394   moreover
395   {assume px: "p dvd y"
396     then obtain d where d: "y = p*d" unfolding dvd_def by blast
397     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
398     hence th: "d*x = p^k" using p0 by simp
399     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
400     with d have "y = p^Suc i" by simp
401     with ij(2) have ?case by blast}
402   ultimately show ?case  using pxyc by blast
403 qed
405 lemma prime_power_exp_nat:
406   fixes p::nat
407   assumes p: "prime p" and n: "n \<noteq> 0"
408     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
409   using n xn
410 proof(induct n arbitrary: k)
411   case 0 thus ?case by simp
412 next
413   case (Suc n k) hence th: "x*x^n = p^k" by simp
414   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
415   moreover
416   {assume n: "n \<noteq> 0"
417     from prime_power_mult_nat[OF p th]
418     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
419     from Suc.hyps[OF n ij(2)] have ?case .}
420   ultimately show ?case by blast
421 qed
423 lemma divides_primepow_nat:
424   fixes p::nat
425   assumes p: "prime p"
426   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
427 proof
428   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
429     unfolding dvd_def  apply (auto simp add: mult.commute) by blast
430   from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
431   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
432   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
433   hence "i \<le> k" by arith
434   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
435 next
436   {fix i assume H: "i \<le> k" "d = p^i"
437     then obtain j where j: "k = i + j"
438       by (metis le_add_diff_inverse)
439     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
440     hence "d dvd p^k" unfolding dvd_def by auto}
441   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
442 qed
445 subsection \<open>Chinese Remainder Theorem Variants\<close>
447 lemma bezout_gcd_nat:
448   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
449   using bezout_nat[of a b]
450 by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
451   gcd_nat.right_neutral mult_0)
453 lemma gcd_bezout_sum_nat:
454   fixes a::nat
455   assumes "a * x + b * y = d"
456   shows "gcd a b dvd d"
457 proof-
458   let ?g = "gcd a b"
459     have dv: "?g dvd a*x" "?g dvd b * y"
460       by simp_all
461     from dvd_add[OF dv] assms
462     show ?thesis by auto
463 qed
466 text \<open>A binary form of the Chinese Remainder Theorem.\<close>
468 (* TODO: Generalise? *)
469 lemma chinese_remainder:
470   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
471   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
472 proof-
473   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
474   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
475     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
476   then have d12: "d1 = 1" "d2 =1"
477     by (metis ab coprime_nat)+
478   let ?x = "v * a * x1 + u * b * x2"
479   let ?q1 = "v * x1 + u * y2"
480   let ?q2 = "v * y1 + u * x2"
481   from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
482   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
483     by algebra+
484   thus ?thesis by blast
485 qed
487 text \<open>Primality\<close>
489 lemma coprime_bezout_strong:
490   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
491   shows "\<exists>x y. a * x = b * y + 1"
492 by (metis assms bezout_nat gcd_nat.left_neutral)
494 lemma bezout_prime:
495   assumes p: "prime p" and pa: "\<not> p dvd a"
496   shows "\<exists>x y. a*x = Suc (p*y)"
497 proof -
498   have ap: "coprime a p"
499     by (metis gcd.commute p pa prime_imp_coprime)
500   moreover from p have "p \<noteq> 1" by auto
501   ultimately have "\<exists>x y. a * x = p * y + 1"
502     by (rule coprime_bezout_strong)
503   then show ?thesis by simp
504 qed
505 (* END TODO *)
509 subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
511 lemma prime_factors_gt_0_nat:
512   "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
513   by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
515 lemma prime_factors_gt_0_int:
516   "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
517   by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
519 lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
520   fixes n :: int
521   shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
522   by (drule prime_factors_gt_0_int) simp
524 lemma prod_mset_prime_factorization_int:
525   fixes n :: int
526   assumes "n > 0"
527   shows   "prod_mset (prime_factorization n) = n"
528   using assms by (simp add: prod_mset_prime_factorization)
530 lemma prime_factorization_exists_nat:
531   "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
532   using prime_factorization_exists[of n] by (auto simp: prime_def)
534 lemma prod_mset_prime_factorization_nat [simp]:
535   "(n::nat) > 0 \<Longrightarrow> prod_mset (prime_factorization n) = n"
536   by (subst prod_mset_prime_factorization) simp_all
538 lemma prime_factorization_nat:
539     "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
540   by (simp add: prod_prime_factors)
542 lemma prime_factorization_int:
543     "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
544   by (simp add: prod_prime_factors)
546 lemma prime_factorization_unique_nat:
547   fixes f :: "nat \<Rightarrow> _"
548   assumes S_eq: "S = {p. 0 < f p}"
549     and "finite S"
550     and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
551   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
552   using assms by (intro prime_factorization_unique'') auto
554 lemma prime_factorization_unique_int:
555   fixes f :: "int \<Rightarrow> _"
556   assumes S_eq: "S = {p. 0 < f p}"
557     and "finite S"
558     and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
559   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
560   using assms by (intro prime_factorization_unique'') auto
562 lemma prime_factors_characterization_nat:
563   "S = {p. 0 < f (p::nat)} \<Longrightarrow>
564     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
565   by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
567 lemma prime_factors_characterization'_nat:
568   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
569     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
570       prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
571   by (rule prime_factors_characterization_nat) auto
573 lemma prime_factors_characterization_int:
574   "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
575     \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
576   by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
578 (* TODO Move *)
579 lemma abs_prod: "abs (prod f A :: 'a :: linordered_idom) = prod (\<lambda>x. abs (f x)) A"
580   by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
582 lemma primes_characterization'_int [rule_format]:
583   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
584       prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
585   by (rule prime_factors_characterization_int) (auto simp: abs_prod prime_ge_0_int)
587 lemma multiplicity_characterization_nat:
588   "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
589     n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
590   by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
592 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
593     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
594       multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
595   by (intro impI, rule multiplicity_characterization_nat) auto
597 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
598     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
599   by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
600      (auto simp: abs_prod power_abs prime_ge_0_int intro!: prod.cong)
602 lemma multiplicity_characterization'_int [rule_format]:
603   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
604     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
605       multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
606   by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
608 lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
609   unfolding One_nat_def [symmetric] by (rule multiplicity_one)
611 lemma multiplicity_eq_nat:
612   fixes x and y::nat
613   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
614   shows "x = y"
615   using multiplicity_eq_imp_eq[of x y] assms by simp
617 lemma multiplicity_eq_int:
618   fixes x y :: int
619   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
620   shows "x = y"
621   using multiplicity_eq_imp_eq[of x y] assms by simp
623 lemma multiplicity_prod_prime_powers:
624   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
625   shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
626 proof -
627   define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
628   define A where "A = Abs_multiset g"
629   have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
630   from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
631     by (simp add: multiset_def)
632   from assms have count_A: "count A x = g x" for x unfolding A_def
633     by simp
634   have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
635     unfolding set_mset_def count_A by (auto simp: g_def)
636   with assms have prime: "prime x" if "x \<in># A" for x using that by auto
637   from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
638     by (intro prod.cong) (auto simp: g_def)
639   also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
640     by (intro prod.mono_neutral_right) (auto simp: g_def set_mset_A)
641   also have "\<dots> = prod_mset A"
642     by (auto simp: prod_mset_multiplicity count_A set_mset_A intro!: prod.cong)
643   also from assms have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
644     by (subst prime_elem_multiplicity_prod_mset_distrib) (auto dest: prime)
645   also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
646     by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
647   also have "sum_mset \<dots> = (if p \<in> S then f p else 0)" by (simp add: sum_mset_delta count_A g_def)
648   finally show ?thesis .
649 qed
651 lemma prime_factorization_prod_mset:
652   assumes "0 \<notin># A"
653   shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
654   using assms by (induct A) (auto simp add: prime_factorization_mult)
656 lemma prime_factors_prod:
657   assumes "finite A" and "0 \<notin> f ` A"
658   shows "prime_factors (prod f A) = UNION A (prime_factors \<circ> f)"
659   using assms by (simp add: prod_unfold_prod_mset prime_factorization_prod_mset)
661 lemma prime_factors_fact:
662   "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
663 proof (rule set_eqI)
664   fix p
665   { fix m :: nat
666     assume "p \<in> prime_factors m"
667     then have "prime p" and "p dvd m" by auto
668     moreover assume "m > 0"
669     ultimately have "2 \<le> p" and "p \<le> m"
670       by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
671     moreover assume "m \<le> n"
672     ultimately have "2 \<le> p" and "p \<le> n"
673       by (auto intro: order_trans)
674   } note * = this
675   show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
676     by (auto simp add: fact_prod prime_factors_prod Suc_le_eq dest!: prime_prime_factors intro: *)
677 qed
679 lemma prime_dvd_fact_iff:
680   assumes "prime p"
681   shows "p dvd fact n \<longleftrightarrow> p \<le> n"
682   using assms
683   by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
684     prime_factorization_prime prime_factors_fact prime_ge_2_nat)
686 (* TODO Legacy names *)
687 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
688 lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
689 lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
690 lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
691 lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
692 lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
693 lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
694 lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
695 lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
696 lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
697 lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
698 lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
699 lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
700 lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
701 lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
702 lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
704 text \<open>Code generation\<close>
706 context
707 begin
709 qualified definition prime_nat :: "nat \<Rightarrow> bool"
710   where [simp, code_abbrev]: "prime_nat = prime"
712 lemma prime_nat_naive [code]:
713   "prime_nat p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
714   by (auto simp add: prime_nat_iff')
716 qualified definition prime_int :: "int \<Rightarrow> bool"
717   where [simp, code_abbrev]: "prime_int = prime"
719 lemma prime_int_naive [code]:
720   "prime_int p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
721   by (auto simp add: prime_int_iff')
723 lemma "prime(997::nat)" by eval
725 lemma "prime(997::int)" by eval
727 end
729 end