src/HOL/Number_Theory/UniqueFactorization.thy

+(*  Title:      UniqueFactorization.thy
+    ID:         
+    Author:     Jeremy Avigad
+
+    
+    Unique factorization for the natural numbers and the integers.
+
+    Note: there were previous Isabelle formalizations of unique
+    factorization due to Thomas Marthedal Rasmussen, and, building on
+    that, by Jeremy Avigad and David Gray.  
+*)
+
+header {* UniqueFactorization *}
+
+theory UniqueFactorization
+imports Cong Multiset
+begin
+
+(* inherited from Multiset *)
+declare One_nat_def [simp del] 
+
+(* As a simp or intro rule,
+
+     prime p \<Longrightarrow> p > 0
+
+   wreaks havoc here. When the premise includes ALL x :# M. prime x, it 
+   leads to the backchaining
+
+     x > 0  
+     prime x 
+     x :# M   which is, unfortunately,
+     count M x > 0
+*)
+
+
+(* useful facts *)
+
+lemma setsum_Un2: "finite (A Un B) \<Longrightarrow> 
+    setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) + 
+      setsum f (A Int B)"
+  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
+  apply (erule ssubst)
+  apply (subst setsum_Un_disjoint)
+  apply auto
+  apply (subst setsum_Un_disjoint)
+  apply auto
+done
+
+lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 
+    setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) * 
+      setprod f (A Int B)"
+  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
+  apply (erule ssubst)
+  apply (subst setprod_Un_disjoint)
+  apply auto
+  apply (subst setprod_Un_disjoint)
+  apply auto
+done
+ 
+(* Should this go in Multiset.thy? *)
+(* TN: No longer an intro-rule; needed only once and might get in the way *)
+lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
+  by (subst multiset_eq_conv_count_eq, blast)
+
+(* Here is a version of set product for multisets. Is it worth moving
+   to multiset.thy? If so, one should similarly define msetsum for abelian 
+   semirings, using of_nat. Also, is it worth developing bounded quantifiers 
+   "ALL i :# M. P i"? 
+*)
+
+constdefs
+  msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
+  "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
+
+syntax
+  "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
+      ("(3PROD _:#_. _)" [0, 51, 10] 10)
+
+translations
+  "PROD i :# A. b" == "msetprod (%i. b) A"
+
+lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
+  apply (simp add: msetprod_def power_add)
+  apply (subst setprod_Un2)
+  apply auto
+  apply (subgoal_tac 
+      "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
+       (PROD x:set_of A - set_of B. f x ^ count A x)")
+  apply (erule ssubst)
+  apply (subgoal_tac 
+      "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
+       (PROD x:set_of B - set_of A. f x ^ count B x)")
+  apply (erule ssubst)
+  apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
+    (PROD x:set_of A - set_of B. f x ^ count A x) *
+    (PROD x:set_of A Int set_of B. f x ^ count A x)")
+  apply (erule ssubst)
+  apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
+    (PROD x:set_of B - set_of A. f x ^ count B x) *
+    (PROD x:set_of A Int set_of B. f x ^ count B x)")
+  apply (erule ssubst)
+  apply (subst setprod_timesf)
+  apply (force simp add: mult_ac)
+  apply (subst setprod_Un_disjoint [symmetric])
+  apply (auto intro: setprod_cong)
+  apply (subst setprod_Un_disjoint [symmetric])
+  apply (auto intro: setprod_cong)
+done
+
+
+subsection {* unique factorization: multiset version *}
+
+lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
+    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
+proof (rule nat_less_induct, clarify)
+  fix n :: nat
+  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
+      (PROD i :# M. i))"
+  assume "(n::nat) > 0"
+  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
+    by arith
+  moreover 
+  {
+    assume "n = 1"
+    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
+        by (auto simp add: msetprod_def)
+  } 
+  moreover 
+  {
+    assume "n > 1" and "prime n"
+    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
+      by (auto simp add: msetprod_def)
+  } 
+  moreover 
+  {
+    assume "n > 1" and "~ prime n"
+    from prems not_prime_eq_prod_nat
+      obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
+        by blast
+    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
+        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
+      by blast
+    hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
+      by (auto simp add: prems msetprod_Un set_of_union)
+    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
+  }
+  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
+    by blast
+qed
+
+lemma multiset_prime_factorization_unique_aux:
+  fixes a :: nat
+  assumes "(ALL p : set_of M. prime p)" and
+    "(ALL p : set_of N. prime p)" and
+    "(PROD i :# M. i) dvd (PROD i:# N. i)"
+  shows
+    "count M a <= count N a"
+proof cases
+  assume "a : set_of M"
+  with prems have a: "prime a"
+    by auto
+  with prems have "a ^ count M a dvd (PROD i :# M. i)"
+    by (auto intro: dvd_setprod simp add: msetprod_def)
+  also have "... dvd (PROD i :# N. i)"
+    by (rule prems)
+  also have "... = (PROD i : (set_of N). i ^ (count N i))"
+    by (simp add: msetprod_def)
+  also have "... = 
+      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
+    proof (cases)
+      assume "a : set_of N"
+      hence b: "set_of N = {a} Un (set_of N - {a})"
+        by auto
+      thus ?thesis
+        by (subst (1) b, subst setprod_Un_disjoint, auto)
+    next
+      assume "a ~: set_of N" 
+      thus ?thesis
+        by auto
+    qed
+  finally have "a ^ count M a dvd 
+      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
+  moreover have "coprime (a ^ count M a)
+      (PROD i : (set_of N - {a}). i ^ (count N i))"
+    apply (subst gcd_commute_nat)
+    apply (rule setprod_coprime_nat)
+    apply (rule primes_imp_powers_coprime_nat)
+    apply (insert prems, auto) 
+    done
+  ultimately have "a ^ count M a dvd a^(count N a)"
+    by (elim coprime_dvd_mult_nat)
+  with a show ?thesis 
+    by (intro power_dvd_imp_le, auto)
+next
+  assume "a ~: set_of M"
+  thus ?thesis by auto
+qed
+
+lemma multiset_prime_factorization_unique:
+  assumes "(ALL (p::nat) : set_of M. prime p)" and
+    "(ALL p : set_of N. prime p)" and
+    "(PROD i :# M. i) = (PROD i:# N. i)"
+  shows
+    "M = N"
+proof -
+  {
+    fix a
+    from prems have "count M a <= count N a"
+      by (intro multiset_prime_factorization_unique_aux, auto) 
+    moreover from prems have "count N a <= count M a"
+      by (intro multiset_prime_factorization_unique_aux, auto) 
+    ultimately have "count M a = count N a"
+      by auto
+  }
+  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
+qed
+
+constdefs
+  multiset_prime_factorization :: "nat => nat multiset"
+  "multiset_prime_factorization n ==
+     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
+       n = (PROD i :# M. i)))
+     else {#}"
+
+lemma multiset_prime_factorization: "n > 0 ==>
+    (ALL p : set_of (multiset_prime_factorization n). prime p) &
+       n = (PROD i :# (multiset_prime_factorization n). i)"
+  apply (unfold multiset_prime_factorization_def)
+  apply clarsimp
+  apply (frule multiset_prime_factorization_exists)
+  apply clarify
+  apply (rule theI)
+  apply (insert multiset_prime_factorization_unique, blast)+
+done
+
+
+subsection {* Prime factors and multiplicity for nats and ints *}
+
+class unique_factorization =
+
+fixes
+  multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
+  prime_factors :: "'a \<Rightarrow> 'a set"
+
+(* definitions for the natural numbers *)
+
+instantiation nat :: unique_factorization
+
+begin
+
+definition
+  multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "multiplicity_nat p n = count (multiset_prime_factorization n) p"
+
+definition
+  prime_factors_nat :: "nat \<Rightarrow> nat set"
+where
+  "prime_factors_nat n = set_of (multiset_prime_factorization n)"
+
+instance proof qed
+
+end
+
+(* definitions for the integers *)
+
+instantiation int :: unique_factorization
+
+begin
+
+definition
+  multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
+where
+  "multiplicity_int p n = multiplicity (nat p) (nat n)"
+
+definition
+  prime_factors_int :: "int \<Rightarrow> int set"
+where
+  "prime_factors_int n = int ` (prime_factors (nat n))"
+
+instance proof qed
+
+end
+
+
+subsection {* Set up transfer *}
+
+lemma transfer_nat_int_prime_factors: 
+  "prime_factors (nat n) = nat ` prime_factors n"
+  unfolding prime_factors_int_def apply auto
+  by (subst transfer_int_nat_set_return_embed, assumption)
+
+lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> 
+    nat_set (prime_factors n)"
+  by (auto simp add: nat_set_def prime_factors_int_def)
+
+lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
+  multiplicity (nat p) (nat n) = multiplicity p n"
+  by (auto simp add: multiplicity_int_def)
+
+declare TransferMorphism_nat_int[transfer add return: 
+  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
+  transfer_nat_int_multiplicity]
+
+
+lemma transfer_int_nat_prime_factors:
+    "prime_factors (int n) = int ` prime_factors n"
+  unfolding prime_factors_int_def by auto
+
+lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
+    nat_set (prime_factors n)"
+  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
+
+lemma transfer_int_nat_multiplicity: 
+    "multiplicity (int p) (int n) = multiplicity p n"
+  by (auto simp add: multiplicity_int_def)
+
+declare TransferMorphism_int_nat[transfer add return: 
+  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
+  transfer_int_nat_multiplicity]
+
+
+subsection {* Properties of prime factors and multiplicity for nats and ints *}
+
+lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
+  by (unfold prime_factors_int_def, auto)
+
+lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
+  apply (case_tac "n = 0")
+  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
+  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
+done
+
+lemma prime_factors_prime_int [intro]:
+  assumes "n >= 0" and "p : prime_factors (n::int)"
+  shows "prime p"
+
+  apply (rule prime_factors_prime_nat [transferred, of n p])
+  using prems apply auto
+done
+
+lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
+  by (frule prime_factors_prime_nat, auto)
+
+lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
+    p > (0::int)"
+  by (frule (1) prime_factors_prime_int, auto)
+
+lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
+  by (unfold prime_factors_nat_def, auto)
+
+lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
+  by (unfold prime_factors_int_def, auto)
+
+lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
+    {p. multiplicity p n > 0}"
+  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
+
+lemma prime_factors_altdef_int: "prime_factors (n::int) = 
+    {p. p >= 0 & multiplicity p n > 0}"
+  apply (unfold prime_factors_int_def multiplicity_int_def)
+  apply (subst prime_factors_altdef_nat)
+  apply (auto simp add: image_def)
+done
+
+lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
+    n = (PROD p : prime_factors n. p^(multiplicity p n))"
+  by (frule multiset_prime_factorization, 
+    simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
+
+thm prime_factorization_nat [transferred] 
+
+lemma prime_factorization_int: 
+  assumes "(n::int) > 0"
+  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
+
+  apply (rule prime_factorization_nat [transferred, of n])
+  using prems apply auto
+done
+
+lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
+  by auto
+
+lemma prime_factorization_unique_nat: 
+    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
+      n = (PROD p : S. p^(f p)) \<Longrightarrow>
+        S = prime_factors n & (ALL p. f p = multiplicity p n)"
+  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
+      f")
+  apply (unfold prime_factors_nat_def multiplicity_nat_def)
+  apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
+  apply (unfold multiset_prime_factorization_def)
+  apply (subgoal_tac "n > 0")
+  prefer 2
+  apply force
+  apply (subst if_P, assumption)
+  apply (rule the1_equality)
+  apply (rule ex_ex1I)
+  apply (rule multiset_prime_factorization_exists, assumption)
+  apply (rule multiset_prime_factorization_unique)
+  apply force
+  apply force
+  apply force
+  unfolding set_of_def count_def msetprod_def
+  apply (subgoal_tac "f : multiset")
+  apply (auto simp only: Abs_multiset_inverse)
+  unfolding multiset_def apply force 
+done
+
+lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
+    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+      prime_factors n = S"
+  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
+    assumption+)
+
+lemma prime_factors_characterization'_nat: 
+  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
+    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
+  apply (rule prime_factors_characterization_nat)
+  apply auto
+done
+
+(* A minor glitch:*)
+
+thm prime_factors_characterization'_nat 
+    [where f = "%x. f (int (x::nat))", 
+      transferred direction: nat "op <= (0::int)", rule_format]
+
+(*
+  Transfer isn't smart enough to know that the "0 < f p" should 
+  remain a comparison between nats. But the transfer still works. 
+*)
+
+lemma primes_characterization'_int [rule_format]: 
+    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
+      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
+        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
+          {p. p >= 0 & 0 < f p}"
+
+  apply (insert prime_factors_characterization'_nat 
+    [where f = "%x. f (int (x::nat))", 
+    transferred direction: nat "op <= (0::int)"])
+  apply auto
+done
+
+lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
+    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+      prime_factors n = S"
+  apply simp
+  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+  apply (simp only:)
+  apply (subst primes_characterization'_int)
+  apply auto
+  apply (auto simp add: prime_ge_0_int)
+done
+
+lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
+    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+      multiplicity p n = f p"
+  by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, 
+    symmetric], auto)
+
+lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
+    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
+      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
+  apply (rule impI)+
+  apply (rule multiplicity_characterization_nat)
+  apply auto
+done
+
+lemma multiplicity_characterization'_int [rule_format]: 
+  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
+    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
+      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
+
+  apply (insert multiplicity_characterization'_nat 
+    [where f = "%x. f (int (x::nat))", 
+      transferred direction: nat "op <= (0::int)", rule_format])
+  apply auto
+done
+
+lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
+    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
+      p >= 0 \<Longrightarrow> multiplicity p n = f p"
+  apply simp
+  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
+  apply (simp only:)
+  apply (subst multiplicity_characterization'_int)
+  apply auto
+  apply (auto simp add: prime_ge_0_int)
+done
+
+lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
+  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
+
+lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
+  by (simp add: multiplicity_int_def) 
+
+lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
+  by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
+
+lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
+  by (simp add: multiplicity_int_def)
+
+lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
+  apply (subst multiplicity_characterization_nat
+      [where f = "(%q. if q = p then 1 else 0)"])
+  apply auto
+  apply (case_tac "x = p")
+  apply auto
+done
+
+lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
+  unfolding prime_int_def multiplicity_int_def by auto
+
+lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> 
+    multiplicity p (p^n) = n"
+  apply (case_tac "n = 0")
+  apply auto
+  apply (subst multiplicity_characterization_nat
+      [where f = "(%q. if q = p then n else 0)"])
+  apply auto
+  apply (case_tac "x = p")
+  apply auto
+done
+
+lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> 
+    multiplicity p (p^n) = n"
+  apply (frule prime_ge_0_int)
+  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
+done
+
+lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> 
+    multiplicity p n = 0"
+  apply (case_tac "n = 0")
+  apply auto
+  apply (frule multiset_prime_factorization)
+  apply (auto simp add: set_of_def multiplicity_nat_def)
+done
+
+lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
+  by (unfold multiplicity_int_def prime_int_def, auto)
+
+lemma multiplicity_not_factor_nat [simp]: 
+    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
+  by (subst (asm) prime_factors_altdef_nat, auto)
+
+lemma multiplicity_not_factor_int [simp]: 
+    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
+  by (subst (asm) prime_factors_altdef_int, auto)
+
+lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
+    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
+    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+  apply (rule prime_factorization_unique_nat)
+  apply (simp only: prime_factors_altdef_nat)
+  apply auto
+  apply (subst power_add)
+  apply (subst setprod_timesf)
+  apply (rule arg_cong2)back back
+  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
+      (prime_factors l - prime_factors k)")
+  apply (erule ssubst)
+  apply (subst setprod_Un_disjoint)
+  apply auto
+  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
+      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
+  apply (erule ssubst)
+  apply (simp add: setprod_1)
+  apply (erule prime_factorization_nat)
+  apply (rule setprod_cong, auto)
+  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
+      (prime_factors k - prime_factors l)")
+  apply (erule ssubst)
+  apply (subst setprod_Un_disjoint)
+  apply auto
+  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
+      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
+  apply (erule ssubst)
+  apply (simp add: setprod_1)
+  apply (erule prime_factorization_nat)
+  apply (rule setprod_cong, auto)
+done
+
+(* transfer doesn't have the same problem here with the right 
+   choice of rules. *)
+
+lemma multiplicity_product_aux_int: 
+  assumes "(k::int) > 0" and "l > 0"
+  shows 
+    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
+    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
+
+  apply (rule multiplicity_product_aux_nat [transferred, of l k])
+  using prems apply auto
+done
+
+lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
+    prime_factors k Un prime_factors l"
+  by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
+
+lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
+    prime_factors k Un prime_factors l"
+  by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
+
+lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
+    multiplicity p k + multiplicity p l"
+  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
+      symmetric])
+
+lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
+    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
+  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
+      symmetric])
+
+lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
+    multiplicity (p::nat) (PROD x : S. f x) = 
+      (SUM x : S. multiplicity p (f x))"
+  apply (induct set: finite)
+  apply auto
+  apply (subst multiplicity_product_nat)
+  apply auto
+done
+
+(* Transfer is delicate here for two reasons: first, because there is
+   an implicit quantifier over functions (f), and, second, because the 
+   product over the multiplicity should not be translated to an integer 
+   product.
+
+   The way to handle the first is to use quantifier rules for functions.
+   The way to handle the second is to turn off the offending rule.
+*)
+
+lemma transfer_nat_int_sum_prod_closure3:
+  "(SUM x : A. int (f x)) >= 0"
+  "(PROD x : A. int (f x)) >= 0"
+  apply (rule setsum_nonneg, auto)
+  apply (rule setprod_nonneg, auto)
+done
+
+declare TransferMorphism_nat_int[transfer 
+  add return: transfer_nat_int_sum_prod_closure3
+  del: transfer_nat_int_sum_prod2 (1)]
+
+lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
+  (ALL x : S. f x > 0) \<Longrightarrow> 
+    multiplicity (p::int) (PROD x : S. f x) = 
+      (SUM x : S. multiplicity p (f x))"
+
+  apply (frule multiplicity_setprod_nat
+    [where f = "%x. nat(int(nat(f x)))", 
+      transferred direction: nat "op <= (0::int)"])
+  apply auto
+  apply (subst (asm) setprod_cong)
+  apply (rule refl)
+  apply (rule if_P)
+  apply auto
+  apply (rule setsum_cong)
+  apply auto
+done
+
+declare TransferMorphism_nat_int[transfer 
+  add return: transfer_nat_int_sum_prod2 (1)]
+
+lemma multiplicity_prod_prime_powers_nat:
+    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
+       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
+  apply (subgoal_tac "(PROD p : S. p ^ f p) = 
+      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
+  apply (erule ssubst)
+  apply (subst multiplicity_characterization_nat)
+  prefer 5 apply (rule refl)
+  apply (rule refl)
+  apply auto
+  apply (subst setprod_mono_one_right)
+  apply assumption
+  prefer 3
+  apply (rule setprod_cong)
+  apply (rule refl)
+  apply auto
+done
+
+(* Here the issue with transfer is the implicit quantifier over S *)
+
+lemma multiplicity_prod_prime_powers_int:
+    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
+       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
+
+  apply (subgoal_tac "int ` nat ` S = S")
+  apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
+    and S = "nat ` S", transferred])
+  apply auto
+  apply (subst prime_int_def [symmetric])
+  apply auto
+  apply (subgoal_tac "xb >= 0")
+  apply force
+  apply (rule prime_ge_0_int)
+  apply force
+  apply (subst transfer_nat_int_set_return_embed)
+  apply (unfold nat_set_def, auto)
+done
+
+lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
+    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
+  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
+  apply (erule ssubst)
+  apply (subst multiplicity_prod_prime_powers_nat)
+  apply auto
+done
+
+lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
+    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
+  apply (frule prime_ge_0_int [of q])
+  apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
+  prefer 4
+  apply assumption
+  apply auto
+done
+
+lemma dvd_multiplicity_nat: 
+    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
+  apply (case_tac "x = 0")
+  apply (auto simp add: dvd_def multiplicity_product_nat)
+done
+
+lemma dvd_multiplicity_int: 
+    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
+      multiplicity p x <= multiplicity p y"
+  apply (case_tac "x = 0")
+  apply (auto simp add: dvd_def)
+  apply (subgoal_tac "0 < k")
+  apply (auto simp add: multiplicity_product_int)
+  apply (erule zero_less_mult_pos)
+  apply arith
+done
+
+lemma dvd_prime_factors_nat [intro]:
+    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+  apply (simp only: prime_factors_altdef_nat)
+  apply auto
+  apply (frule dvd_multiplicity_nat)
+  apply auto
+(* It is a shame that auto and arith don't get this. *)
+  apply (erule order_less_le_trans)back
+  apply assumption
+done
+
+lemma dvd_prime_factors_int [intro]:
+    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
+  apply (auto simp add: prime_factors_altdef_int)
+  apply (erule order_less_le_trans)
+  apply (rule dvd_multiplicity_int)
+  apply auto
+done
+
+lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
+    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
+      x dvd y"
+  apply (subst prime_factorization_nat [of x], assumption)
+  apply (subst prime_factorization_nat [of y], assumption)
+  apply (rule setprod_dvd_setprod_subset2)
+  apply force
+  apply (subst prime_factors_altdef_nat)+
+  apply auto
+(* Again, a shame that auto and arith don't get this. *)
+  apply (drule_tac x = xa in spec, auto)
+  apply (rule le_imp_power_dvd)
+  apply blast
+done
+
+lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
+    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
+      x dvd y"
+  apply (subst prime_factorization_int [of x], assumption)
+  apply (subst prime_factorization_int [of y], assumption)
+  apply (rule setprod_dvd_setprod_subset2)
+  apply force
+  apply (subst prime_factors_altdef_int)+
+  apply auto
+  apply (rule dvd_power_le)
+  apply auto
+  apply (drule_tac x = xa in spec)
+  apply (erule impE)
+  apply auto
+done
+
+lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
+    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
+  apply (cases "y = 0")
+  apply auto
+  apply (rule multiplicity_dvd_nat, auto)
+  apply (case_tac "prime p")
+  apply auto
+done
+
+lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
+    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
+  apply (cases "y = 0")
+  apply auto
+  apply (rule multiplicity_dvd_int, auto)
+  apply (case_tac "prime p")
+  apply auto
+done
+
+lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
+    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
+  by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
+
+lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
+    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
+  by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
+
+lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
+    (p : prime_factors n) = (prime p & p dvd n)"
+  apply (case_tac "prime p")
+  apply auto
+  apply (subst prime_factorization_nat [where n = n], assumption)
+  apply (rule dvd_trans) 
+  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
+  apply (subst (asm) prime_factors_altdef_nat, force)
+  apply (rule dvd_setprod)
+  apply auto  
+  apply (subst prime_factors_altdef_nat)
+  apply (subst (asm) dvd_multiplicity_eq_nat)
+  apply auto
+  apply (drule spec [where x = p])
+  apply auto
+done
+
+lemma prime_factors_altdef2_int: 
+  assumes "(n::int) > 0" 
+  shows "(p : prime_factors n) = (prime p & p dvd n)"
+
+  apply (case_tac "p >= 0")
+  apply (rule prime_factors_altdef2_nat [transferred])
+  using prems apply auto
+  apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
+done
+
+lemma multiplicity_eq_nat:
+  fixes x and y::nat 
+  assumes [arith]: "x > 0" "y > 0" and
+    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  shows "x = y"
+
+  apply (rule dvd_anti_sym)
+  apply (auto intro: multiplicity_dvd'_nat) 
+done
+
+lemma multiplicity_eq_int:
+  fixes x and y::int 
+  assumes [arith]: "x > 0" "y > 0" and
+    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
+  shows "x = y"
+
+  apply (rule dvd_anti_sym [transferred])
+  apply (auto intro: multiplicity_dvd'_int) 
+done
+
+
+subsection {* An application *}
+
+lemma gcd_eq_nat: 
+  assumes pos [arith]: "x > 0" "y > 0"
+  shows "gcd (x::nat) y = 
+    (PROD p: prime_factors x Un prime_factors y. 
+      p ^ (min (multiplicity p x) (multiplicity p y)))"
+proof -
+  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
+      p ^ (min (multiplicity p x) (multiplicity p y)))"
+  have [arith]: "z > 0"
+    unfolding z_def by (rule setprod_pos_nat, auto)
+  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
+      min (multiplicity p x) (multiplicity p y)"
+    unfolding z_def
+    apply (subst multiplicity_prod_prime_powers_nat)
+    apply (auto simp add: multiplicity_not_factor_nat)
+    done
+  have "z dvd x" 
+    by (intro multiplicity_dvd'_nat, auto simp add: aux)
+  moreover have "z dvd y" 
+    by (intro multiplicity_dvd'_nat, auto simp add: aux)
+  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
+    apply auto
+    apply (case_tac "w = 0", auto)
+    apply (erule multiplicity_dvd'_nat)
+    apply (auto intro: dvd_multiplicity_nat simp add: aux)
+    done
+  ultimately have "z = gcd x y"
+    by (subst gcd_unique_nat [symmetric], blast)
+  thus ?thesis
+    unfolding z_def by auto
+qed
+
+lemma lcm_eq_nat: 
+  assumes pos [arith]: "x > 0" "y > 0"
+  shows "lcm (x::nat) y = 
+    (PROD p: prime_factors x Un prime_factors y. 
+      p ^ (max (multiplicity p x) (multiplicity p y)))"
+proof -
+  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
+      p ^ (max (multiplicity p x) (multiplicity p y)))"
+  have [arith]: "z > 0"
+    unfolding z_def by (rule setprod_pos_nat, auto)
+  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
+      max (multiplicity p x) (multiplicity p y)"
+    unfolding z_def
+    apply (subst multiplicity_prod_prime_powers_nat)
+    apply (auto simp add: multiplicity_not_factor_nat)
+    done
+  have "x dvd z" 
+    by (intro multiplicity_dvd'_nat, auto simp add: aux)
+  moreover have "y dvd z" 
+    by (intro multiplicity_dvd'_nat, auto simp add: aux)
+  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
+    apply auto
+    apply (case_tac "w = 0", auto)
+    apply (rule multiplicity_dvd'_nat)
+    apply (auto intro: dvd_multiplicity_nat simp add: aux)
+    done
+  ultimately have "z = lcm x y"
+    by (subst lcm_unique_nat [symmetric], blast)
+  thus ?thesis
+    unfolding z_def by auto
+qed
+
+lemma multiplicity_gcd_nat: 
+  assumes [arith]: "x > 0" "y > 0"
+  shows "multiplicity (p::nat) (gcd x y) = 
+    min (multiplicity p x) (multiplicity p y)"
+
+  apply (subst gcd_eq_nat)
+  apply auto
+  apply (subst multiplicity_prod_prime_powers_nat)
+  apply auto
+done
+
+lemma multiplicity_lcm_nat: 
+  assumes [arith]: "x > 0" "y > 0"
+  shows "multiplicity (p::nat) (lcm x y) = 
+    max (multiplicity p x) (multiplicity p y)"
+
+  apply (subst lcm_eq_nat)
+  apply auto
+  apply (subst multiplicity_prod_prime_powers_nat)
+  apply auto
+done
+
+lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
+  apply (case_tac "x = 0 | y = 0 | z = 0") 
+  apply auto
+  apply (rule multiplicity_eq_nat)
+  apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat 
+      lcm_pos_nat)
+done
+
+lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
+  apply (subst (1 2 3) gcd_abs_int)
+  apply (subst lcm_abs_int)
+  apply (subst (2) abs_of_nonneg)
+  apply force
+  apply (rule gcd_lcm_distrib_nat [transferred])
+  apply auto
+done
+
+end