src/HOL/Number_Theory/Primes.thy
 author eberlm Tue Aug 09 12:30:31 2016 +0200 (2016-08-09) changeset 63635 858a225ebb62 parent 63633 2accfb71e33b child 63766 695d60817cb1 permissions -rw-r--r--
Tuned primes
1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow,
3                 Manuel Eberl
6 This file deals with properties of primes. Definitions and lemmas are
7 proved uniformly for the natural numbers and integers.
9 This file combines and revises a number of prior developments.
11 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
12 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
13 gcd, lcm, and prime for the natural numbers.
15 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
16 extended gcd, lcm, primes to the integers. Amine Chaieb provided
17 another extension of the notions to the integers, and added a number
18 of results to "Primes" and "GCD". IntPrimes also defined and developed
19 the congruence relations on the integers. The notion was extended to
20 the natural numbers by Chaieb.
22 Jeremy Avigad combined all of these, made everything uniform for the
23 natural numbers and the integers, and added a number of new theorems.
25 Tobias Nipkow cleaned up a lot.
27 Florian Haftmann and Manuel Eberl put primality and prime factorisation
28 onto an algebraic foundation and thus generalised these concepts to
29 other rings, such as polynomials. (see also the Factorial_Ring theory).
31 There were also previous formalisations of unique factorisation by
32 Thomas Marthedal Rasmussen, Jeremy Avigad, and David Gray.
33 *)
36 section \<open>Primes\<close>
38 theory Primes
39 imports "~~/src/HOL/Binomial" Euclidean_Algorithm
40 begin
42 (* As a simp or intro rule,
44      prime p \<Longrightarrow> p > 0
46    wreaks havoc here. When the premise includes \<forall>x \<in># M. prime x, it
47    leads to the backchaining
49      x > 0
50      prime x
51      x \<in># M   which is, unfortunately,
52      count M x > 0
53 *)
55 declare [[coercion int]]
56 declare [[coercion_enabled]]
58 lemma prime_elem_nat_iff:
59   "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
60 proof safe
61   assume *: "prime_elem n"
62   from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
63   thus "n > 1" by (cases n) simp_all
64   fix m assume m: "m dvd n" "m \<noteq> n"
65   from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
66     by (intro irreducibleD' prime_elem_imp_irreducible)
67   with m show "m = 1" by (auto dest: dvd_antisym)
68 next
69   assume "n > 1" "\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n"
70   thus "prime_elem n"
71     by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
72 qed
74 lemma prime_nat_iff_prime_elem: "prime (n :: nat) \<longleftrightarrow> prime_elem n"
75   by (simp add: prime_def)
77 lemma prime_nat_iff:
78   "prime (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
79   by (simp add: prime_nat_iff_prime_elem prime_elem_nat_iff)
81 lemma prime_elem_int_nat_transfer: "prime_elem (n::int) \<longleftrightarrow> prime_elem (nat (abs n))"
82 proof
83   assume "prime_elem n"
84   thus "prime_elem (nat (abs n))" by (auto simp: prime_elem_def nat_dvd_iff)
85 next
86   assume "prime_elem (nat (abs n))"
87   thus "prime_elem n"
88     by (auto simp: dvd_int_unfold_dvd_nat prime_elem_def abs_mult nat_mult_distrib)
89 qed
91 lemma prime_elem_nat_int_transfer [simp]: "prime_elem (int n) \<longleftrightarrow> prime_elem n"
92   by (auto simp: prime_elem_int_nat_transfer)
94 lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
95   by (auto simp: prime_elem_int_nat_transfer prime_def)
97 lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
98   by (auto simp: prime_elem_int_nat_transfer prime_def)
100 lemma prime_int_iff:
101   "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
102 proof (intro iffI conjI allI impI; (elim conjE)?)
103   assume *: "prime n"
104   hence irred: "irreducible n" by (simp add: prime_elem_imp_irreducible)
105   from * have "n \<ge> 0" "n \<noteq> 0" "n \<noteq> 1"
106     by (auto simp: prime_def zabs_def not_less split: if_splits)
107   thus "n > 1" by presburger
108   fix m assume "m dvd n" \<open>m \<ge> 0\<close>
109   with irred have "m dvd 1 \<or> n dvd m" by (auto simp: irreducible_altdef)
110   with \<open>m dvd n\<close> \<open>m \<ge> 0\<close> \<open>n > 1\<close> show "m = 1 \<or> m = n"
111     using associated_iff_dvd[of m n] by auto
112 next
113   assume n: "1 < n" "\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n"
114   hence "nat n > 1" by simp
115   moreover have "\<forall>m. m dvd nat n \<longrightarrow> m = 1 \<or> m = nat n"
116   proof (intro allI impI)
117     fix m assume "m dvd nat n"
118     with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
119     with n(2) have "int m = 1 \<or> int m = n" by auto
120     thus "m = 1 \<or> m = nat n" by auto
121   qed
122   ultimately show "prime n"
123     unfolding prime_int_nat_transfer prime_nat_iff by auto
124 qed
127 lemma prime_nat_not_dvd:
128   assumes "prime p" "p > n" "n \<noteq> (1::nat)"
129   shows   "\<not>n dvd p"
130 proof
131   assume "n dvd p"
132   from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
133   from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
134     by (cases "n = 0") (auto dest!: dvd_imp_le)
135 qed
137 lemma prime_int_not_dvd:
138   assumes "prime p" "p > n" "n > (1::int)"
139   shows   "\<not>n dvd p"
140 proof
141   assume "n dvd p"
142   from assms(1) have "irreducible p" by (simp add: prime_elem_imp_irreducible)
143   from irreducibleD'[OF this \<open>n dvd p\<close>] \<open>n dvd p\<close> \<open>p > n\<close> assms show False
144     by (auto dest!: zdvd_imp_le)
145 qed
147 lemma prime_odd_nat: "prime p \<Longrightarrow> p > (2::nat) \<Longrightarrow> odd p"
148   by (intro prime_nat_not_dvd) auto
150 lemma prime_odd_int: "prime p \<Longrightarrow> p > (2::int) \<Longrightarrow> odd p"
151   by (intro prime_int_not_dvd) auto
153 lemma prime_ge_0_int: "prime p \<Longrightarrow> p \<ge> (0::int)"
154   unfolding prime_int_iff by auto
156 lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > (0::nat)"
157   unfolding prime_nat_iff by auto
159 lemma prime_gt_0_int: "prime p \<Longrightarrow> p > (0::int)"
160   unfolding prime_int_iff by auto
162 lemma prime_ge_1_nat: "prime p \<Longrightarrow> p \<ge> (1::nat)"
163   unfolding prime_nat_iff by auto
165 lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p \<ge> Suc 0"
166   unfolding prime_nat_iff by auto
168 lemma prime_ge_1_int: "prime p \<Longrightarrow> p \<ge> (1::int)"
169   unfolding prime_int_iff by auto
171 lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > (1::nat)"
172   unfolding prime_nat_iff by auto
174 lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
175   unfolding prime_nat_iff by auto
177 lemma prime_gt_1_int: "prime p \<Longrightarrow> p > (1::int)"
178   unfolding prime_int_iff by auto
180 lemma prime_ge_2_nat: "prime p \<Longrightarrow> p \<ge> (2::nat)"
181   unfolding prime_nat_iff by auto
183 lemma prime_ge_2_int: "prime p \<Longrightarrow> p \<ge> (2::int)"
184   unfolding prime_int_iff by auto
186 lemma prime_int_altdef:
187   "prime p = (1 < p \<and> (\<forall>m::int. m \<ge> 0 \<longrightarrow> m dvd p \<longrightarrow>
188     m = 1 \<or> m = p))"
189   unfolding prime_int_iff by blast
191 lemma not_prime_eq_prod_nat:
192   assumes "m > 1" "\<not>prime (m::nat)"
193   shows   "\<exists>n k. n = m * k \<and> 1 < m \<and> m < n \<and> 1 < k \<and> k < n"
194   using assms irreducible_altdef[of m]
195   by (auto simp: prime_elem_iff_irreducible prime_def irreducible_altdef)
198 subsubsection \<open>Make prime naively executable\<close>
200 lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
201   unfolding One_nat_def [symmetric] by (rule not_prime_1)
203 lemma prime_nat_iff':
204   "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
205 proof safe
206   assume "p > 1" and *: "\<forall>n\<in>{1<..<p}. \<not>n dvd p"
207   show "prime p" unfolding prime_nat_iff
208   proof (intro conjI allI impI)
209     fix m assume "m dvd p"
210     with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
211     hence "m \<ge> 1" by simp
212     moreover from \<open>m dvd p\<close> and * have "m \<notin> {1<..<p}" by blast
213     with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
214     ultimately show "m = 1 \<or> m = p" by simp
215   qed fact+
216 qed (auto simp: prime_nat_iff)
218 lemma prime_nat_code [code_unfold]:
219   "(prime :: nat \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
220   by (rule ext, rule prime_nat_iff')
222 lemma prime_int_iff':
223   "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
224 proof
225   assume "?lhs"
226   thus "?rhs" by (auto simp: prime_int_nat_transfer dvd_int_unfold_dvd_nat prime_nat_code)
227 next
228   assume "?rhs"
229   thus "?lhs" by (auto simp: prime_int_nat_transfer zdvd_int prime_nat_code)
230 qed
232 lemma prime_int_code [code_unfold]:
233   "(prime :: int \<Rightarrow> bool) = (\<lambda>p. p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p))"
234   by (rule ext, rule prime_int_iff')
236 lemma prime_nat_simp:
237     "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
238   by (auto simp add: prime_nat_code)
240 lemma prime_int_simp:
241     "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
242   by (auto simp add: prime_int_code)
244 lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
246 lemma two_is_prime_nat [simp]: "prime (2::nat)"
247   by simp
249 declare prime_int_nat_transfer[of "numeral m" for m, simp]
252 text\<open>A bit of regression testing:\<close>
254 lemma "prime(97::nat)" by simp
255 lemma "prime(997::nat)" by eval
256 lemma "prime(97::int)" by simp
257 lemma "prime(997::int)" by eval
259 lemma prime_factor_nat:
260   "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
261   using prime_divisor_exists[of n]
262   by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
265 subsection \<open>Infinitely many primes\<close>
267 lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
268 proof-
269   have f1: "fact n + 1 \<noteq> (1::nat)" using fact_ge_1 [of n, where 'a=nat] by arith
270   from prime_factor_nat [OF f1]
271   obtain p :: nat where "prime p" and "p dvd fact n + 1" by auto
272   then have "p \<le> fact n + 1" apply (intro dvd_imp_le) apply auto done
273   { assume "p \<le> n"
274     from \<open>prime p\<close> have "p \<ge> 1"
275       by (cases p, simp_all)
276     with \<open>p <= n\<close> have "p dvd fact n"
277       by (intro dvd_fact)
278     with \<open>p dvd fact n + 1\<close> have "p dvd fact n + 1 - fact n"
279       by (rule dvd_diff_nat)
280     then have "p dvd 1" by simp
281     then have "p <= 1" by auto
282     moreover from \<open>prime p\<close> have "p > 1"
283       using prime_nat_iff by blast
284     ultimately have False by auto}
285   then have "n < p" by presburger
286   with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
287 qed
289 lemma bigger_prime: "\<exists>p. prime p \<and> p > (n::nat)"
290   using next_prime_bound by auto
292 lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
293 proof
294   assume "finite {(p::nat). prime p}"
295   with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
296     by auto
297   then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
298     by auto
299   with bigger_prime [of b] show False
300     by auto
301 qed
303 subsection\<open>Powers of Primes\<close>
305 text\<open>Versions for type nat only\<close>
307 lemma prime_product:
308   fixes p::nat
309   assumes "prime (p * q)"
310   shows "p = 1 \<or> q = 1"
311 proof -
312   from assms have
313     "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
314     unfolding prime_nat_iff by auto
315   from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
316   then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
317   have "p dvd p * q" by simp
318   then have "p = 1 \<or> p = p * q" by (rule P)
319   then show ?thesis by (simp add: Q)
320 qed
322 (* TODO: Generalise? *)
323 lemma prime_power_mult_nat:
324   fixes p::nat
325   assumes p: "prime p" and xy: "x * y = p ^ k"
326   shows "\<exists>i j. x = p ^i \<and> y = p^ j"
327 using xy
328 proof(induct k arbitrary: x y)
329   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
330 next
331   case (Suc k x y)
332   from Suc.prems have pxy: "p dvd x*y" by auto
333   from prime_dvd_multD [OF p pxy] have pxyc: "p dvd x \<or> p dvd y" .
334   from p have p0: "p \<noteq> 0" by - (rule ccontr, simp)
335   {assume px: "p dvd x"
336     then obtain d where d: "x = p*d" unfolding dvd_def by blast
337     from Suc.prems d  have "p*d*y = p^Suc k" by simp
338     hence th: "d*y = p^k" using p0 by simp
339     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "y = p^j" by blast
340     with d have "x = p^Suc i" by simp
341     with ij(2) have ?case by blast}
342   moreover
343   {assume px: "p dvd y"
344     then obtain d where d: "y = p*d" unfolding dvd_def by blast
345     from Suc.prems d  have "p*d*x = p^Suc k" by (simp add: mult.commute)
346     hence th: "d*x = p^k" using p0 by simp
347     from Suc.hyps[OF th] obtain i j where ij: "d = p^i" "x = p^j" by blast
348     with d have "y = p^Suc i" by simp
349     with ij(2) have ?case by blast}
350   ultimately show ?case  using pxyc by blast
351 qed
353 lemma prime_power_exp_nat:
354   fixes p::nat
355   assumes p: "prime p" and n: "n \<noteq> 0"
356     and xn: "x^n = p^k" shows "\<exists>i. x = p^i"
357   using n xn
358 proof(induct n arbitrary: k)
359   case 0 thus ?case by simp
360 next
361   case (Suc n k) hence th: "x*x^n = p^k" by simp
362   {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
363   moreover
364   {assume n: "n \<noteq> 0"
365     from prime_power_mult_nat[OF p th]
366     obtain i j where ij: "x = p^i" "x^n = p^j"by blast
367     from Suc.hyps[OF n ij(2)] have ?case .}
368   ultimately show ?case by blast
369 qed
371 lemma divides_primepow_nat:
372   fixes p::nat
373   assumes p: "prime p"
374   shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
375 proof
376   assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
377     unfolding dvd_def  apply (auto simp add: mult.commute) by blast
378   from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
379   from e ij have "p^(i + j) = p^k" by (simp add: power_add)
380   hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
381   hence "i \<le> k" by arith
382   with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
383 next
384   {fix i assume H: "i \<le> k" "d = p^i"
385     then obtain j where j: "k = i + j"
386       by (metis le_add_diff_inverse)
387     hence "p^k = p^j*d" using H(2) by (simp add: power_add)
388     hence "d dvd p^k" unfolding dvd_def by auto}
389   thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
390 qed
393 subsection \<open>Chinese Remainder Theorem Variants\<close>
395 lemma bezout_gcd_nat:
396   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
397   using bezout_nat[of a b]
398 by (metis bezout_nat diff_add_inverse gcd_add_mult gcd.commute
399   gcd_nat.right_neutral mult_0)
401 lemma gcd_bezout_sum_nat:
402   fixes a::nat
403   assumes "a * x + b * y = d"
404   shows "gcd a b dvd d"
405 proof-
406   let ?g = "gcd a b"
407     have dv: "?g dvd a*x" "?g dvd b * y"
408       by simp_all
409     from dvd_add[OF dv] assms
410     show ?thesis by auto
411 qed
414 text \<open>A binary form of the Chinese Remainder Theorem.\<close>
416 (* TODO: Generalise? *)
417 lemma chinese_remainder:
418   fixes a::nat  assumes ab: "coprime a b" and a: "a \<noteq> 0" and b: "b \<noteq> 0"
419   shows "\<exists>x q1 q2. x = u + q1 * a \<and> x = v + q2 * b"
420 proof-
421   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
422   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
423     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
424   then have d12: "d1 = 1" "d2 =1"
425     by (metis ab coprime_nat)+
426   let ?x = "v * a * x1 + u * b * x2"
427   let ?q1 = "v * x1 + u * y2"
428   let ?q2 = "v * y1 + u * x2"
429   from dxy2(3)[simplified d12] dxy1(3)[simplified d12]
430   have "?x = u + ?q1 * a" "?x = v + ?q2 * b"
431     by algebra+
432   thus ?thesis by blast
433 qed
435 text \<open>Primality\<close>
437 lemma coprime_bezout_strong:
438   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
439   shows "\<exists>x y. a * x = b * y + 1"
440 by (metis assms bezout_nat gcd_nat.left_neutral)
442 lemma bezout_prime:
443   assumes p: "prime p" and pa: "\<not> p dvd a"
444   shows "\<exists>x y. a*x = Suc (p*y)"
445 proof -
446   have ap: "coprime a p"
447     by (metis gcd.commute p pa prime_imp_coprime)
448   moreover from p have "p \<noteq> 1" by auto
449   ultimately have "\<exists>x y. a * x = p * y + 1"
450     by (rule coprime_bezout_strong)
451   then show ?thesis by simp
452 qed
453 (* END TODO *)
457 subsection \<open>Multiplicity and primality for natural numbers and integers\<close>
459 lemma prime_factors_gt_0_nat:
460   "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
461   by (simp add: prime_factors_prime prime_gt_0_nat)
463 lemma prime_factors_gt_0_int:
464   "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
465   by (simp add: prime_factors_prime prime_gt_0_int)
467 lemma prime_factors_ge_0_int [elim]:
468   fixes n :: int
469   shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
470   unfolding prime_factors_def
471   by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
473 lemma msetprod_prime_factorization_int:
474   fixes n :: int
475   assumes "n > 0"
476   shows   "msetprod (prime_factorization n) = n"
477   using assms by (simp add: msetprod_prime_factorization)
479 lemma prime_factorization_exists_nat:
480   "n > 0 \<Longrightarrow> (\<exists>M. (\<forall>p::nat \<in> set_mset M. prime p) \<and> n = (\<Prod>i \<in># M. i))"
481   using prime_factorization_exists[of n] by (auto simp: prime_def)
483 lemma msetprod_prime_factorization_nat [simp]:
484   "(n::nat) > 0 \<Longrightarrow> msetprod (prime_factorization n) = n"
485   by (subst msetprod_prime_factorization) simp_all
487 lemma prime_factorization_nat:
488     "n > (0::nat) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
489   by (simp add: setprod_prime_factors)
491 lemma prime_factorization_int:
492     "n > (0::int) \<Longrightarrow> n = (\<Prod>p \<in> prime_factors n. p ^ multiplicity p n)"
493   by (simp add: setprod_prime_factors)
495 lemma prime_factorization_unique_nat:
496   fixes f :: "nat \<Rightarrow> _"
497   assumes S_eq: "S = {p. 0 < f p}"
498     and "finite S"
499     and S: "\<forall>p\<in>S. prime p" "n = (\<Prod>p\<in>S. p ^ f p)"
500   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
501   using assms by (intro prime_factorization_unique'') auto
503 lemma prime_factorization_unique_int:
504   fixes f :: "int \<Rightarrow> _"
505   assumes S_eq: "S = {p. 0 < f p}"
506     and "finite S"
507     and S: "\<forall>p\<in>S. prime p" "abs n = (\<Prod>p\<in>S. p ^ f p)"
508   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
509   using assms by (intro prime_factorization_unique'') auto
511 lemma prime_factors_characterization_nat:
512   "S = {p. 0 < f (p::nat)} \<Longrightarrow>
513     finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
514   by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
516 lemma prime_factors_characterization'_nat:
517   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
518     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
519       prime_factors (\<Prod>p | 0 < f p. p ^ f p) = {p. 0 < f p}"
520   by (rule prime_factors_characterization_nat) auto
522 lemma prime_factors_characterization_int:
523   "S = {p. 0 < f (p::int)} \<Longrightarrow> finite S \<Longrightarrow>
524     \<forall>p\<in>S. prime p \<Longrightarrow> abs n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> prime_factors n = S"
525   by (rule prime_factorization_unique_int [THEN conjunct1, symmetric])
527 (* TODO Move *)
528 lemma abs_setprod: "abs (setprod f A :: 'a :: linordered_idom) = setprod (\<lambda>x. abs (f x)) A"
529   by (cases "finite A", induction A rule: finite_induct) (simp_all add: abs_mult)
531 lemma primes_characterization'_int [rule_format]:
532   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow> \<forall>p. 0 < f p \<longrightarrow> prime p \<Longrightarrow>
533       prime_factors (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = {p. p \<ge> 0 \<and> 0 < f p}"
534   by (rule prime_factors_characterization_int) (auto simp: abs_setprod prime_ge_0_int)
536 lemma multiplicity_characterization_nat:
537   "S = {p. 0 < f (p::nat)} \<Longrightarrow> finite S \<Longrightarrow> \<forall>p\<in>S. prime p \<Longrightarrow> prime p \<Longrightarrow>
538     n = (\<Prod>p\<in>S. p ^ f p) \<Longrightarrow> multiplicity p n = f p"
539   by (frule prime_factorization_unique_nat [of S f n, THEN conjunct2, rule_format, symmetric]) auto
541 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
542     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<longrightarrow> prime p \<longrightarrow>
543       multiplicity p (\<Prod>p | 0 < f p. p ^ f p) = f p"
544   by (intro impI, rule multiplicity_characterization_nat) auto
546 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
547     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"
548   by (frule prime_factorization_unique_int [of S f n, THEN conjunct2, rule_format, symmetric])
549      (auto simp: abs_setprod power_abs prime_ge_0_int intro!: setprod.cong)
551 lemma multiplicity_characterization'_int [rule_format]:
552   "finite {p. p \<ge> 0 \<and> 0 < f (p::int)} \<Longrightarrow>
553     (\<forall>p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> prime p \<Longrightarrow>
554       multiplicity p (\<Prod>p | p \<ge> 0 \<and> 0 < f p. p ^ f p) = f p"
555   by (rule multiplicity_characterization_int) (auto simp: prime_ge_0_int)
557 lemma multiplicity_one_nat [simp]: "multiplicity p (Suc 0) = 0"
558   unfolding One_nat_def [symmetric] by (rule multiplicity_one)
560 lemma multiplicity_eq_nat:
561   fixes x and y::nat
562   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
563   shows "x = y"
564   using multiplicity_eq_imp_eq[of x y] assms by simp
566 lemma multiplicity_eq_int:
567   fixes x y :: int
568   assumes "x > 0" "y > 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
569   shows "x = y"
570   using multiplicity_eq_imp_eq[of x y] assms by simp
572 lemma multiplicity_prod_prime_powers:
573   assumes "finite S" "\<And>x. x \<in> S \<Longrightarrow> prime x" "prime p"
574   shows   "multiplicity p (\<Prod>p \<in> S. p ^ f p) = (if p \<in> S then f p else 0)"
575 proof -
576   define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
577   define A where "A = Abs_multiset g"
578   have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
579   from finite_subset[OF this assms(1)] have [simp]: "g :  multiset"
580     by (simp add: multiset_def)
581   from assms have count_A: "count A x = g x" for x unfolding A_def
582     by simp
583   have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
584     unfolding set_mset_def count_A by (auto simp: g_def)
585   with assms have prime: "prime x" if "x \<in># A" for x using that by auto
586   from set_mset_A assms have "(\<Prod>p \<in> S. p ^ f p) = (\<Prod>p \<in> S. p ^ g p) "
587     by (intro setprod.cong) (auto simp: g_def)
588   also from set_mset_A assms have "\<dots> = (\<Prod>p \<in> set_mset A. p ^ g p)"
589     by (intro setprod.mono_neutral_right) (auto simp: g_def set_mset_A)
590   also have "\<dots> = msetprod A"
591     by (auto simp: msetprod_multiplicity count_A set_mset_A intro!: setprod.cong)
592   also from assms have "multiplicity p \<dots> = msetsum (image_mset (multiplicity p) A)"
593     by (subst prime_elem_multiplicity_msetprod_distrib) (auto dest: prime)
594   also from assms have "image_mset (multiplicity p) A = image_mset (\<lambda>x. if x = p then 1 else 0) A"
595     by (intro image_mset_cong) (auto simp: prime_multiplicity_other dest: prime)
596   also have "msetsum \<dots> = (if p \<in> S then f p else 0)" by (simp add: msetsum_delta count_A g_def)
597   finally show ?thesis .
598 qed
600 (* TODO Legacy names *)
601 lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
602 lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
603 lemmas prime_dvd_mult_nat = prime_dvd_mult_iff[where ?'a = nat]
604 lemmas prime_dvd_mult_int = prime_dvd_mult_iff[where ?'a = int]
605 lemmas prime_dvd_mult_eq_nat = prime_dvd_mult_iff[where ?'a = nat]
606 lemmas prime_dvd_mult_eq_int = prime_dvd_mult_iff[where ?'a = int]
607 lemmas prime_dvd_power_nat = prime_dvd_power[where ?'a = nat]
608 lemmas prime_dvd_power_int = prime_dvd_power[where ?'a = int]
609 lemmas prime_dvd_power_nat_iff = prime_dvd_power_iff[where ?'a = nat]
610 lemmas prime_dvd_power_int_iff = prime_dvd_power_iff[where ?'a = int]
611 lemmas prime_imp_power_coprime_nat = prime_imp_power_coprime[where ?'a = nat]
612 lemmas prime_imp_power_coprime_int = prime_imp_power_coprime[where ?'a = int]
613 lemmas primes_coprime_nat = primes_coprime[where ?'a = nat]
614 lemmas primes_coprime_int = primes_coprime[where ?'a = nat]
615 lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
616 lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
618 end