src/HOL/Number_Theory/UniqueFactorization.thy
 author wenzelm Fri Dec 17 17:43:54 2010 +0100 (2010-12-17) changeset 41229 d797baa3d57c parent 40461 e876e95588ce child 41413 64cd30d6b0b8 permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
1 (*  Title:      UniqueFactorization.thy
5     Unique factorization for the natural numbers and the integers.
7     Note: there were previous Isabelle formalizations of unique
8     factorization due to Thomas Marthedal Rasmussen, and, building on
9     that, by Jeremy Avigad and David Gray.
10 *)
14 theory UniqueFactorization
15 imports Cong Multiset
16 begin
18 (* inherited from Multiset *)
19 declare One_nat_def [simp del]
21 (* As a simp or intro rule,
23      prime p \<Longrightarrow> p > 0
25    wreaks havoc here. When the premise includes ALL x :# M. prime x, it
28      x > 0
29      prime x
30      x :# M   which is, unfortunately,
31      count M x > 0
32 *)
35 (* useful facts *)
37 lemma setsum_Un2: "finite (A Un B) \<Longrightarrow>
38     setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) +
39       setsum f (A Int B)"
40   apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
41   apply (erule ssubst)
42   apply (subst setsum_Un_disjoint)
43   apply auto
44   apply (subst setsum_Un_disjoint)
45   apply auto
46 done
48 lemma setprod_Un2: "finite (A Un B) \<Longrightarrow>
49     setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) *
50       setprod f (A Int B)"
51   apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
52   apply (erule ssubst)
53   apply (subst setprod_Un_disjoint)
54   apply auto
55   apply (subst setprod_Un_disjoint)
56   apply auto
57 done
59 (* Here is a version of set product for multisets. Is it worth moving
60    to multiset.thy? If so, one should similarly define msetsum for abelian
61    semirings, using of_nat. Also, is it worth developing bounded quantifiers
62    "ALL i :# M. P i"?
63 *)
65 definition msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b" where
66   "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
68 syntax
69   "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"
70       ("(3PROD _:#_. _)" [0, 51, 10] 10)
72 translations
73   "PROD i :# A. b" == "CONST msetprod (%i. b) A"
75 lemma msetprod_empty:
76   "msetprod f {#} = 1"
79 lemma msetprod_singleton:
80   "msetprod f {#x#} = f x"
83 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
85   apply (subst setprod_Un2)
86   apply auto
87   apply (subgoal_tac
88       "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
89        (PROD x:set_of A - set_of B. f x ^ count A x)")
90   apply (erule ssubst)
91   apply (subgoal_tac
92       "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
93        (PROD x:set_of B - set_of A. f x ^ count B x)")
94   apply (erule ssubst)
95   apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) =
96     (PROD x:set_of A - set_of B. f x ^ count A x) *
97     (PROD x:set_of A Int set_of B. f x ^ count A x)")
98   apply (erule ssubst)
99   apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) =
100     (PROD x:set_of B - set_of A. f x ^ count B x) *
101     (PROD x:set_of A Int set_of B. f x ^ count B x)")
102   apply (erule ssubst)
103   apply (subst setprod_timesf)
104   apply (force simp add: mult_ac)
105   apply (subst setprod_Un_disjoint [symmetric])
106   apply (auto intro: setprod_cong)
107   apply (subst setprod_Un_disjoint [symmetric])
108   apply (auto intro: setprod_cong)
109 done
112 subsection {* unique factorization: multiset version *}
114 lemma multiset_prime_factorization_exists [rule_format]: "n > 0 -->
115     (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
116 proof (rule nat_less_induct, clarify)
117   fix n :: nat
118   assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m =
119       (PROD i :# M. i))"
120   assume "(n::nat) > 0"
121   then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
122     by arith
123   moreover
124   {
125     assume "n = 1"
126     then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
127         by (auto simp add: msetprod_def)
128   }
129   moreover
130   {
131     assume "n > 1" and "prime n"
132     then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
133       by (auto simp add: msetprod_def)
134   }
135   moreover
136   {
137     assume "n > 1" and "~ prime n"
138     from prems not_prime_eq_prod_nat
139       obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
140         by blast
141     with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
142         and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
143       by blast
144     hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
145       by (auto simp add: prems msetprod_Un set_of_union)
146     then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
147   }
148   ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
149     by blast
150 qed
152 lemma multiset_prime_factorization_unique_aux:
153   fixes a :: nat
154   assumes "(ALL p : set_of M. prime p)" and
155     "(ALL p : set_of N. prime p)" and
156     "(PROD i :# M. i) dvd (PROD i:# N. i)"
157   shows
158     "count M a <= count N a"
159 proof cases
160   assume "a : set_of M"
161   with prems have a: "prime a"
162     by auto
163   with prems have "a ^ count M a dvd (PROD i :# M. i)"
164     by (auto intro: dvd_setprod simp add: msetprod_def)
165   also have "... dvd (PROD i :# N. i)"
166     by (rule prems)
167   also have "... = (PROD i : (set_of N). i ^ (count N i))"
169   also have "... =
170       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
171     proof (cases)
172       assume "a : set_of N"
173       hence b: "set_of N = {a} Un (set_of N - {a})"
174         by auto
175       thus ?thesis
176         by (subst (1) b, subst setprod_Un_disjoint, auto)
177     next
178       assume "a ~: set_of N"
179       thus ?thesis
180         by auto
181     qed
182   finally have "a ^ count M a dvd
183       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
184   moreover have "coprime (a ^ count M a)
185       (PROD i : (set_of N - {a}). i ^ (count N i))"
186     apply (subst gcd_commute_nat)
187     apply (rule setprod_coprime_nat)
188     apply (rule primes_imp_powers_coprime_nat)
189     apply (insert prems, auto)
190     done
191   ultimately have "a ^ count M a dvd a^(count N a)"
192     by (elim coprime_dvd_mult_nat)
193   with a show ?thesis
194     by (intro power_dvd_imp_le, auto)
195 next
196   assume "a ~: set_of M"
197   thus ?thesis by auto
198 qed
200 lemma multiset_prime_factorization_unique:
201   assumes "(ALL (p::nat) : set_of M. prime p)" and
202     "(ALL p : set_of N. prime p)" and
203     "(PROD i :# M. i) = (PROD i:# N. i)"
204   shows
205     "M = N"
206 proof -
207   {
208     fix a
209     from prems have "count M a <= count N a"
210       by (intro multiset_prime_factorization_unique_aux, auto)
211     moreover from prems have "count N a <= count M a"
212       by (intro multiset_prime_factorization_unique_aux, auto)
213     ultimately have "count M a = count N a"
214       by auto
215   }
216   thus ?thesis by (simp add:multiset_eq_iff)
217 qed
219 definition multiset_prime_factorization :: "nat => nat multiset" where
220   "multiset_prime_factorization n ==
221      if n > 0 then (THE M. ((ALL p : set_of M. prime p) &
222        n = (PROD i :# M. i)))
223      else {#}"
225 lemma multiset_prime_factorization: "n > 0 ==>
226     (ALL p : set_of (multiset_prime_factorization n). prime p) &
227        n = (PROD i :# (multiset_prime_factorization n). i)"
228   apply (unfold multiset_prime_factorization_def)
229   apply clarsimp
230   apply (frule multiset_prime_factorization_exists)
231   apply clarify
232   apply (rule theI)
233   apply (insert multiset_prime_factorization_unique, blast)+
234 done
237 subsection {* Prime factors and multiplicity for nats and ints *}
239 class unique_factorization =
241 fixes
242   multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
243   prime_factors :: "'a \<Rightarrow> 'a set"
245 (* definitions for the natural numbers *)
247 instantiation nat :: unique_factorization
249 begin
251 definition
252   multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
253 where
254   "multiplicity_nat p n = count (multiset_prime_factorization n) p"
256 definition
257   prime_factors_nat :: "nat \<Rightarrow> nat set"
258 where
259   "prime_factors_nat n = set_of (multiset_prime_factorization n)"
261 instance proof qed
263 end
265 (* definitions for the integers *)
267 instantiation int :: unique_factorization
269 begin
271 definition
272   multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
273 where
274   "multiplicity_int p n = multiplicity (nat p) (nat n)"
276 definition
277   prime_factors_int :: "int \<Rightarrow> int set"
278 where
279   "prime_factors_int n = int ` (prime_factors (nat n))"
281 instance proof qed
283 end
286 subsection {* Set up transfer *}
288 lemma transfer_nat_int_prime_factors:
289   "prime_factors (nat n) = nat ` prime_factors n"
290   unfolding prime_factors_int_def apply auto
291   by (subst transfer_int_nat_set_return_embed, assumption)
293 lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow>
294     nat_set (prime_factors n)"
295   by (auto simp add: nat_set_def prime_factors_int_def)
297 lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
298   multiplicity (nat p) (nat n) = multiplicity p n"
299   by (auto simp add: multiplicity_int_def)
302   transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
303   transfer_nat_int_multiplicity]
306 lemma transfer_int_nat_prime_factors:
307     "prime_factors (int n) = int ` prime_factors n"
308   unfolding prime_factors_int_def by auto
310 lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow>
311     nat_set (prime_factors n)"
312   by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
314 lemma transfer_int_nat_multiplicity:
315     "multiplicity (int p) (int n) = multiplicity p n"
316   by (auto simp add: multiplicity_int_def)
319   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
320   transfer_int_nat_multiplicity]
323 subsection {* Properties of prime factors and multiplicity for nats and ints *}
325 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
326   by (unfold prime_factors_int_def, auto)
328 lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
329   apply (case_tac "n = 0")
330   apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
331   apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
332 done
334 lemma prime_factors_prime_int [intro]:
335   assumes "n >= 0" and "p : prime_factors (n::int)"
336   shows "prime p"
338   apply (rule prime_factors_prime_nat [transferred, of n p])
339   using prems apply auto
340 done
342 lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
343   by (frule prime_factors_prime_nat, auto)
345 lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow>
346     p > (0::int)"
347   by (frule (1) prime_factors_prime_int, auto)
349 lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
350   by (unfold prime_factors_nat_def, auto)
352 lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
353   by (unfold prime_factors_int_def, auto)
355 lemma prime_factors_altdef_nat: "prime_factors (n::nat) =
356     {p. multiplicity p n > 0}"
357   by (force simp add: prime_factors_nat_def multiplicity_nat_def)
359 lemma prime_factors_altdef_int: "prime_factors (n::int) =
360     {p. p >= 0 & multiplicity p n > 0}"
361   apply (unfold prime_factors_int_def multiplicity_int_def)
362   apply (subst prime_factors_altdef_nat)
363   apply (auto simp add: image_def)
364 done
366 lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
367     n = (PROD p : prime_factors n. p^(multiplicity p n))"
368   by (frule multiset_prime_factorization,
369     simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
371 thm prime_factorization_nat [transferred]
373 lemma prime_factorization_int:
374   assumes "(n::int) > 0"
375   shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
377   apply (rule prime_factorization_nat [transferred, of n])
378   using prems apply auto
379 done
381 lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
382   by auto
384 lemma prime_factorization_unique_nat:
385     "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
386       n = (PROD p : S. p^(f p)) \<Longrightarrow>
387         S = prime_factors n & (ALL p. f p = multiplicity p n)"
388   apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
389       f")
390   apply (unfold prime_factors_nat_def multiplicity_nat_def)
391   apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
392   apply (unfold multiset_prime_factorization_def)
393   apply (subgoal_tac "n > 0")
394   prefer 2
395   apply force
396   apply (subst if_P, assumption)
397   apply (rule the1_equality)
398   apply (rule ex_ex1I)
399   apply (rule multiset_prime_factorization_exists, assumption)
400   apply (rule multiset_prime_factorization_unique)
401   apply force
402   apply force
403   apply force
404   unfolding set_of_def msetprod_def
405   apply (subgoal_tac "f : multiset")
406   apply (auto simp only: Abs_multiset_inverse)
407   unfolding multiset_def apply force
408 done
410 lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
411     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
412       prime_factors n = S"
413   by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
414     assumption+)
416 lemma prime_factors_characterization'_nat:
417   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
418     (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
419       prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
420   apply (rule prime_factors_characterization_nat)
421   apply auto
422 done
424 (* A minor glitch:*)
426 thm prime_factors_characterization'_nat
427     [where f = "%x. f (int (x::nat))",
428       transferred direction: nat "op <= (0::int)", rule_format]
430 (*
431   Transfer isn't smart enough to know that the "0 < f p" should
432   remain a comparison between nats. But the transfer still works.
433 *)
435 lemma primes_characterization'_int [rule_format]:
436     "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
437       (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
438         prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) =
439           {p. p >= 0 & 0 < f p}"
441   apply (insert prime_factors_characterization'_nat
442     [where f = "%x. f (int (x::nat))",
443     transferred direction: nat "op <= (0::int)"])
444   apply auto
445 done
447 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
448     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
449       prime_factors n = S"
450   apply simp
451   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
452   apply (simp only:)
453   apply (subst primes_characterization'_int)
454   apply auto
455   apply (auto simp add: prime_ge_0_int)
456 done
458 lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow>
459     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
460       multiplicity p n = f p"
461   by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format,
462     symmetric], auto)
464 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
465     (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
466       multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
467   apply (rule impI)+
468   apply (rule multiplicity_characterization_nat)
469   apply auto
470 done
472 lemma multiplicity_characterization'_int [rule_format]:
473   "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
474     (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
475       multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
477   apply (insert multiplicity_characterization'_nat
478     [where f = "%x. f (int (x::nat))",
479       transferred direction: nat "op <= (0::int)", rule_format])
480   apply auto
481 done
483 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
484     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
485       p >= 0 \<Longrightarrow> multiplicity p n = f p"
486   apply simp
487   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
488   apply (simp only:)
489   apply (subst multiplicity_characterization'_int)
490   apply auto
491   apply (auto simp add: prime_ge_0_int)
492 done
494 lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
495   by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
497 lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
500 lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
501   by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
503 lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
506 lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
507   apply (subst multiplicity_characterization_nat
508       [where f = "(%q. if q = p then 1 else 0)"])
509   apply auto
510   apply (case_tac "x = p")
511   apply auto
512 done
514 lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
515   unfolding prime_int_def multiplicity_int_def by auto
517 lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow>
518     multiplicity p (p^n) = n"
519   apply (case_tac "n = 0")
520   apply auto
521   apply (subst multiplicity_characterization_nat
522       [where f = "(%q. if q = p then n else 0)"])
523   apply auto
524   apply (case_tac "x = p")
525   apply auto
526 done
528 lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow>
529     multiplicity p (p^n) = n"
530   apply (frule prime_ge_0_int)
531   apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
532 done
534 lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow>
535     multiplicity p n = 0"
536   apply (case_tac "n = 0")
537   apply auto
538   apply (frule multiset_prime_factorization)
539   apply (auto simp add: set_of_def multiplicity_nat_def)
540 done
542 lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
543   by (unfold multiplicity_int_def prime_int_def, auto)
545 lemma multiplicity_not_factor_nat [simp]:
546     "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
547   by (subst (asm) prime_factors_altdef_nat, auto)
549 lemma multiplicity_not_factor_int [simp]:
550     "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
551   by (subst (asm) prime_factors_altdef_int, auto)
553 lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
554     (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
555     (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
556   apply (rule prime_factorization_unique_nat)
557   apply (simp only: prime_factors_altdef_nat)
558   apply auto
560   apply (subst setprod_timesf)
561   apply (rule arg_cong2)back back
562   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un
563       (prime_factors l - prime_factors k)")
564   apply (erule ssubst)
565   apply (subst setprod_Un_disjoint)
566   apply auto
567   apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) =
568       (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
569   apply (erule ssubst)
571   apply (erule prime_factorization_nat)
572   apply (rule setprod_cong, auto)
573   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un
574       (prime_factors k - prime_factors l)")
575   apply (erule ssubst)
576   apply (subst setprod_Un_disjoint)
577   apply auto
578   apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) =
579       (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
580   apply (erule ssubst)
582   apply (erule prime_factorization_nat)
583   apply (rule setprod_cong, auto)
584 done
586 (* transfer doesn't have the same problem here with the right
587    choice of rules. *)
589 lemma multiplicity_product_aux_int:
590   assumes "(k::int) > 0" and "l > 0"
591   shows
592     "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
593     (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
595   apply (rule multiplicity_product_aux_nat [transferred, of l k])
596   using prems apply auto
597 done
599 lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
600     prime_factors k Un prime_factors l"
601   by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
603 lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
604     prime_factors k Un prime_factors l"
605   by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
607 lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) =
608     multiplicity p k + multiplicity p l"
609   by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format,
610       symmetric])
612 lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow>
613     multiplicity p (k * l) = multiplicity p k + multiplicity p l"
614   by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format,
615       symmetric])
617 lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow>
618     multiplicity (p::nat) (PROD x : S. f x) =
619       (SUM x : S. multiplicity p (f x))"
620   apply (induct set: finite)
621   apply auto
622   apply (subst multiplicity_product_nat)
623   apply auto
624 done
626 (* Transfer is delicate here for two reasons: first, because there is
627    an implicit quantifier over functions (f), and, second, because the
628    product over the multiplicity should not be translated to an integer
629    product.
631    The way to handle the first is to use quantifier rules for functions.
632    The way to handle the second is to turn off the offending rule.
633 *)
635 lemma transfer_nat_int_sum_prod_closure3:
636   "(SUM x : A. int (f x)) >= 0"
637   "(PROD x : A. int (f x)) >= 0"
638   apply (rule setsum_nonneg, auto)
639   apply (rule setprod_nonneg, auto)
640 done
642 declare transfer_morphism_nat_int[transfer
644   del: transfer_nat_int_sum_prod2 (1)]
646 lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow>
647   (ALL x : S. f x > 0) \<Longrightarrow>
648     multiplicity (p::int) (PROD x : S. f x) =
649       (SUM x : S. multiplicity p (f x))"
651   apply (frule multiplicity_setprod_nat
652     [where f = "%x. nat(int(nat(f x)))",
653       transferred direction: nat "op <= (0::int)"])
654   apply auto
655   apply (subst (asm) setprod_cong)
656   apply (rule refl)
657   apply (rule if_P)
658   apply auto
659   apply (rule setsum_cong)
660   apply auto
661 done
663 declare transfer_morphism_nat_int[transfer
666 lemma multiplicity_prod_prime_powers_nat:
667     "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
668        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
669   apply (subgoal_tac "(PROD p : S. p ^ f p) =
670       (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
671   apply (erule ssubst)
672   apply (subst multiplicity_characterization_nat)
673   prefer 5 apply (rule refl)
674   apply (rule refl)
675   apply auto
676   apply (subst setprod_mono_one_right)
677   apply assumption
678   prefer 3
679   apply (rule setprod_cong)
680   apply (rule refl)
681   apply auto
682 done
684 (* Here the issue with transfer is the implicit quantifier over S *)
686 lemma multiplicity_prod_prime_powers_int:
687     "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
688        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
690   apply (subgoal_tac "int ` nat ` S = S")
691   apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)"
692     and S = "nat ` S", transferred])
693   apply auto
694   apply (metis prime_int_def)
695   apply (metis prime_ge_0_int)
696   apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
697 done
699 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
700     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
701   apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
702   apply (erule ssubst)
703   apply (subst multiplicity_prod_prime_powers_nat)
704   apply auto
705 done
707 lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
708     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
709   apply (frule prime_ge_0_int [of q])
710   apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n])
711   prefer 4
712   apply assumption
713   apply auto
714 done
716 lemma dvd_multiplicity_nat:
717     "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
718   apply (case_tac "x = 0")
719   apply (auto simp add: dvd_def multiplicity_product_nat)
720 done
722 lemma dvd_multiplicity_int:
723     "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow>
724       multiplicity p x <= multiplicity p y"
725   apply (case_tac "x = 0")
726   apply (auto simp add: dvd_def)
727   apply (subgoal_tac "0 < k")
728   apply (auto simp add: multiplicity_product_int)
729   apply (erule zero_less_mult_pos)
730   apply arith
731 done
733 lemma dvd_prime_factors_nat [intro]:
734     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
735   apply (simp only: prime_factors_altdef_nat)
736   apply auto
737   apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
738 done
740 lemma dvd_prime_factors_int [intro]:
741     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
742   apply (auto simp add: prime_factors_altdef_int)
743   apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
744 done
746 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
747     ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
748       x dvd y"
749   apply (subst prime_factorization_nat [of x], assumption)
750   apply (subst prime_factorization_nat [of y], assumption)
751   apply (rule setprod_dvd_setprod_subset2)
752   apply force
753   apply (subst prime_factors_altdef_nat)+
754   apply auto
755   apply (metis gr0I le_0_eq less_not_refl)
756   apply (metis le_imp_power_dvd)
757 done
759 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
760     ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
761       x dvd y"
762   apply (subst prime_factorization_int [of x], assumption)
763   apply (subst prime_factorization_int [of y], assumption)
764   apply (rule setprod_dvd_setprod_subset2)
765   apply force
766   apply (subst prime_factors_altdef_int)+
767   apply auto
768   apply (metis le_imp_power_dvd prime_factors_ge_0_int)
769 done
771 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow>
772     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
773 by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
774           multiplicity_nonprime_nat neq0_conv)
776 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
777     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
778 by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
779           multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
781 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
782     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
783   by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
785 lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
786     (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
787   by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
789 lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow>
790     (p : prime_factors n) = (prime p & p dvd n)"
791   apply (case_tac "prime p")
792   apply auto
793   apply (subst prime_factorization_nat [where n = n], assumption)
794   apply (rule dvd_trans)
795   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
796   apply (subst (asm) prime_factors_altdef_nat, force)
797   apply (rule dvd_setprod)
798   apply auto
799   apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)
800 done
802 lemma prime_factors_altdef2_int:
803   assumes "(n::int) > 0"
804   shows "(p : prime_factors n) = (prime p & p dvd n)"
806   apply (case_tac "p >= 0")
807   apply (rule prime_factors_altdef2_nat [transferred])
808   using prems apply auto
809   apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
810 done
812 lemma multiplicity_eq_nat:
813   fixes x and y::nat
814   assumes [arith]: "x > 0" "y > 0" and
815     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
816   shows "x = y"
818   apply (rule dvd_antisym)
819   apply (auto intro: multiplicity_dvd'_nat)
820 done
822 lemma multiplicity_eq_int:
823   fixes x and y::int
824   assumes [arith]: "x > 0" "y > 0" and
825     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
826   shows "x = y"
828   apply (rule dvd_antisym [transferred])
829   apply (auto intro: multiplicity_dvd'_int)
830 done
833 subsection {* An application *}
835 lemma gcd_eq_nat:
836   assumes pos [arith]: "x > 0" "y > 0"
837   shows "gcd (x::nat) y =
838     (PROD p: prime_factors x Un prime_factors y.
839       p ^ (min (multiplicity p x) (multiplicity p y)))"
840 proof -
841   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
842       p ^ (min (multiplicity p x) (multiplicity p y)))"
843   have [arith]: "z > 0"
844     unfolding z_def by (rule setprod_pos_nat, auto)
845   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
846       min (multiplicity p x) (multiplicity p y)"
847     unfolding z_def
848     apply (subst multiplicity_prod_prime_powers_nat)
849     apply (auto simp add: multiplicity_not_factor_nat)
850     done
851   have "z dvd x"
852     by (intro multiplicity_dvd'_nat, auto simp add: aux)
853   moreover have "z dvd y"
854     by (intro multiplicity_dvd'_nat, auto simp add: aux)
855   moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
856     apply auto
857     apply (case_tac "w = 0", auto)
858     apply (erule multiplicity_dvd'_nat)
859     apply (auto intro: dvd_multiplicity_nat simp add: aux)
860     done
861   ultimately have "z = gcd x y"
862     by (subst gcd_unique_nat [symmetric], blast)
863   thus ?thesis
864     unfolding z_def by auto
865 qed
867 lemma lcm_eq_nat:
868   assumes pos [arith]: "x > 0" "y > 0"
869   shows "lcm (x::nat) y =
870     (PROD p: prime_factors x Un prime_factors y.
871       p ^ (max (multiplicity p x) (multiplicity p y)))"
872 proof -
873   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y.
874       p ^ (max (multiplicity p x) (multiplicity p y)))"
875   have [arith]: "z > 0"
876     unfolding z_def by (rule setprod_pos_nat, auto)
877   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z =
878       max (multiplicity p x) (multiplicity p y)"
879     unfolding z_def
880     apply (subst multiplicity_prod_prime_powers_nat)
881     apply (auto simp add: multiplicity_not_factor_nat)
882     done
883   have "x dvd z"
884     by (intro multiplicity_dvd'_nat, auto simp add: aux)
885   moreover have "y dvd z"
886     by (intro multiplicity_dvd'_nat, auto simp add: aux)
887   moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
888     apply auto
889     apply (case_tac "w = 0", auto)
890     apply (rule multiplicity_dvd'_nat)
891     apply (auto intro: dvd_multiplicity_nat simp add: aux)
892     done
893   ultimately have "z = lcm x y"
894     by (subst lcm_unique_nat [symmetric], blast)
895   thus ?thesis
896     unfolding z_def by auto
897 qed
899 lemma multiplicity_gcd_nat:
900   assumes [arith]: "x > 0" "y > 0"
901   shows "multiplicity (p::nat) (gcd x y) =
902     min (multiplicity p x) (multiplicity p y)"
904   apply (subst gcd_eq_nat)
905   apply auto
906   apply (subst multiplicity_prod_prime_powers_nat)
907   apply auto
908 done
910 lemma multiplicity_lcm_nat:
911   assumes [arith]: "x > 0" "y > 0"
912   shows "multiplicity (p::nat) (lcm x y) =
913     max (multiplicity p x) (multiplicity p y)"
915   apply (subst lcm_eq_nat)
916   apply auto
917   apply (subst multiplicity_prod_prime_powers_nat)
918   apply auto
919 done
921 lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
922   apply (case_tac "x = 0 | y = 0 | z = 0")
923   apply auto
924   apply (rule multiplicity_eq_nat)
925   apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat
926       lcm_pos_nat)
927 done
929 lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
930   apply (subst (1 2 3) gcd_abs_int)
931   apply (subst lcm_abs_int)
932   apply (subst (2) abs_of_nonneg)
933   apply force
934   apply (rule gcd_lcm_distrib_nat [transferred])
935   apply auto
936 done
938 end