src/HOL/Number_Theory/UniqueFactorization.thy
changeset 32479 521cc9bf2958
parent 31952 40501bb2d57c
child 33657 a4179bf442d1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,967 @@
     1.4 +(*  Title:      UniqueFactorization.thy
     1.5 +    ID:         
     1.6 +    Author:     Jeremy Avigad
     1.7 +
     1.8 +    
     1.9 +    Unique factorization for the natural numbers and the integers.
    1.10 +
    1.11 +    Note: there were previous Isabelle formalizations of unique
    1.12 +    factorization due to Thomas Marthedal Rasmussen, and, building on
    1.13 +    that, by Jeremy Avigad and David Gray.  
    1.14 +*)
    1.15 +
    1.16 +header {* UniqueFactorization *}
    1.17 +
    1.18 +theory UniqueFactorization
    1.19 +imports Cong Multiset
    1.20 +begin
    1.21 +
    1.22 +(* inherited from Multiset *)
    1.23 +declare One_nat_def [simp del] 
    1.24 +
    1.25 +(* As a simp or intro rule,
    1.26 +
    1.27 +     prime p \<Longrightarrow> p > 0
    1.28 +
    1.29 +   wreaks havoc here. When the premise includes ALL x :# M. prime x, it 
    1.30 +   leads to the backchaining
    1.31 +
    1.32 +     x > 0  
    1.33 +     prime x 
    1.34 +     x :# M   which is, unfortunately,
    1.35 +     count M x > 0
    1.36 +*)
    1.37 +
    1.38 +
    1.39 +(* useful facts *)
    1.40 +
    1.41 +lemma setsum_Un2: "finite (A Un B) \<Longrightarrow> 
    1.42 +    setsum f (A Un B) = setsum f (A - B) + setsum f (B - A) + 
    1.43 +      setsum f (A Int B)"
    1.44 +  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
    1.45 +  apply (erule ssubst)
    1.46 +  apply (subst setsum_Un_disjoint)
    1.47 +  apply auto
    1.48 +  apply (subst setsum_Un_disjoint)
    1.49 +  apply auto
    1.50 +done
    1.51 +
    1.52 +lemma setprod_Un2: "finite (A Un B) \<Longrightarrow> 
    1.53 +    setprod f (A Un B) = setprod f (A - B) * setprod f (B - A) * 
    1.54 +      setprod f (A Int B)"
    1.55 +  apply (subgoal_tac "A Un B = (A - B) Un (B - A) Un (A Int B)")
    1.56 +  apply (erule ssubst)
    1.57 +  apply (subst setprod_Un_disjoint)
    1.58 +  apply auto
    1.59 +  apply (subst setprod_Un_disjoint)
    1.60 +  apply auto
    1.61 +done
    1.62 + 
    1.63 +(* Should this go in Multiset.thy? *)
    1.64 +(* TN: No longer an intro-rule; needed only once and might get in the way *)
    1.65 +lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
    1.66 +  by (subst multiset_eq_conv_count_eq, blast)
    1.67 +
    1.68 +(* Here is a version of set product for multisets. Is it worth moving
    1.69 +   to multiset.thy? If so, one should similarly define msetsum for abelian 
    1.70 +   semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    1.71 +   "ALL i :# M. P i"? 
    1.72 +*)
    1.73 +
    1.74 +constdefs
    1.75 +  msetprod :: "('a => ('b::{power,comm_monoid_mult})) => 'a multiset => 'b"
    1.76 +  "msetprod f M == setprod (%x. (f x)^(count M x)) (set_of M)"
    1.77 +
    1.78 +syntax
    1.79 +  "_msetprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" 
    1.80 +      ("(3PROD _:#_. _)" [0, 51, 10] 10)
    1.81 +
    1.82 +translations
    1.83 +  "PROD i :# A. b" == "msetprod (%i. b) A"
    1.84 +
    1.85 +lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
    1.86 +  apply (simp add: msetprod_def power_add)
    1.87 +  apply (subst setprod_Un2)
    1.88 +  apply auto
    1.89 +  apply (subgoal_tac 
    1.90 +      "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
    1.91 +       (PROD x:set_of A - set_of B. f x ^ count A x)")
    1.92 +  apply (erule ssubst)
    1.93 +  apply (subgoal_tac 
    1.94 +      "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
    1.95 +       (PROD x:set_of B - set_of A. f x ^ count B x)")
    1.96 +  apply (erule ssubst)
    1.97 +  apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
    1.98 +    (PROD x:set_of A - set_of B. f x ^ count A x) *
    1.99 +    (PROD x:set_of A Int set_of B. f x ^ count A x)")
   1.100 +  apply (erule ssubst)
   1.101 +  apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
   1.102 +    (PROD x:set_of B - set_of A. f x ^ count B x) *
   1.103 +    (PROD x:set_of A Int set_of B. f x ^ count B x)")
   1.104 +  apply (erule ssubst)
   1.105 +  apply (subst setprod_timesf)
   1.106 +  apply (force simp add: mult_ac)
   1.107 +  apply (subst setprod_Un_disjoint [symmetric])
   1.108 +  apply (auto intro: setprod_cong)
   1.109 +  apply (subst setprod_Un_disjoint [symmetric])
   1.110 +  apply (auto intro: setprod_cong)
   1.111 +done
   1.112 +
   1.113 +
   1.114 +subsection {* unique factorization: multiset version *}
   1.115 +
   1.116 +lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
   1.117 +    (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
   1.118 +proof (rule nat_less_induct, clarify)
   1.119 +  fix n :: nat
   1.120 +  assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
   1.121 +      (PROD i :# M. i))"
   1.122 +  assume "(n::nat) > 0"
   1.123 +  then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
   1.124 +    by arith
   1.125 +  moreover 
   1.126 +  {
   1.127 +    assume "n = 1"
   1.128 +    then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
   1.129 +        by (auto simp add: msetprod_def)
   1.130 +  } 
   1.131 +  moreover 
   1.132 +  {
   1.133 +    assume "n > 1" and "prime n"
   1.134 +    then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
   1.135 +      by (auto simp add: msetprod_def)
   1.136 +  } 
   1.137 +  moreover 
   1.138 +  {
   1.139 +    assume "n > 1" and "~ prime n"
   1.140 +    from prems not_prime_eq_prod_nat
   1.141 +      obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
   1.142 +        by blast
   1.143 +    with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
   1.144 +        and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
   1.145 +      by blast
   1.146 +    hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
   1.147 +      by (auto simp add: prems msetprod_Un set_of_union)
   1.148 +    then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
   1.149 +  }
   1.150 +  ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
   1.151 +    by blast
   1.152 +qed
   1.153 +
   1.154 +lemma multiset_prime_factorization_unique_aux:
   1.155 +  fixes a :: nat
   1.156 +  assumes "(ALL p : set_of M. prime p)" and
   1.157 +    "(ALL p : set_of N. prime p)" and
   1.158 +    "(PROD i :# M. i) dvd (PROD i:# N. i)"
   1.159 +  shows
   1.160 +    "count M a <= count N a"
   1.161 +proof cases
   1.162 +  assume "a : set_of M"
   1.163 +  with prems have a: "prime a"
   1.164 +    by auto
   1.165 +  with prems have "a ^ count M a dvd (PROD i :# M. i)"
   1.166 +    by (auto intro: dvd_setprod simp add: msetprod_def)
   1.167 +  also have "... dvd (PROD i :# N. i)"
   1.168 +    by (rule prems)
   1.169 +  also have "... = (PROD i : (set_of N). i ^ (count N i))"
   1.170 +    by (simp add: msetprod_def)
   1.171 +  also have "... = 
   1.172 +      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
   1.173 +    proof (cases)
   1.174 +      assume "a : set_of N"
   1.175 +      hence b: "set_of N = {a} Un (set_of N - {a})"
   1.176 +        by auto
   1.177 +      thus ?thesis
   1.178 +        by (subst (1) b, subst setprod_Un_disjoint, auto)
   1.179 +    next
   1.180 +      assume "a ~: set_of N" 
   1.181 +      thus ?thesis
   1.182 +        by auto
   1.183 +    qed
   1.184 +  finally have "a ^ count M a dvd 
   1.185 +      a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
   1.186 +  moreover have "coprime (a ^ count M a)
   1.187 +      (PROD i : (set_of N - {a}). i ^ (count N i))"
   1.188 +    apply (subst gcd_commute_nat)
   1.189 +    apply (rule setprod_coprime_nat)
   1.190 +    apply (rule primes_imp_powers_coprime_nat)
   1.191 +    apply (insert prems, auto) 
   1.192 +    done
   1.193 +  ultimately have "a ^ count M a dvd a^(count N a)"
   1.194 +    by (elim coprime_dvd_mult_nat)
   1.195 +  with a show ?thesis 
   1.196 +    by (intro power_dvd_imp_le, auto)
   1.197 +next
   1.198 +  assume "a ~: set_of M"
   1.199 +  thus ?thesis by auto
   1.200 +qed
   1.201 +
   1.202 +lemma multiset_prime_factorization_unique:
   1.203 +  assumes "(ALL (p::nat) : set_of M. prime p)" and
   1.204 +    "(ALL p : set_of N. prime p)" and
   1.205 +    "(PROD i :# M. i) = (PROD i:# N. i)"
   1.206 +  shows
   1.207 +    "M = N"
   1.208 +proof -
   1.209 +  {
   1.210 +    fix a
   1.211 +    from prems have "count M a <= count N a"
   1.212 +      by (intro multiset_prime_factorization_unique_aux, auto) 
   1.213 +    moreover from prems have "count N a <= count M a"
   1.214 +      by (intro multiset_prime_factorization_unique_aux, auto) 
   1.215 +    ultimately have "count M a = count N a"
   1.216 +      by auto
   1.217 +  }
   1.218 +  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
   1.219 +qed
   1.220 +
   1.221 +constdefs
   1.222 +  multiset_prime_factorization :: "nat => nat multiset"
   1.223 +  "multiset_prime_factorization n ==
   1.224 +     if n > 0 then (THE M. ((ALL p : set_of M. prime p) & 
   1.225 +       n = (PROD i :# M. i)))
   1.226 +     else {#}"
   1.227 +
   1.228 +lemma multiset_prime_factorization: "n > 0 ==>
   1.229 +    (ALL p : set_of (multiset_prime_factorization n). prime p) &
   1.230 +       n = (PROD i :# (multiset_prime_factorization n). i)"
   1.231 +  apply (unfold multiset_prime_factorization_def)
   1.232 +  apply clarsimp
   1.233 +  apply (frule multiset_prime_factorization_exists)
   1.234 +  apply clarify
   1.235 +  apply (rule theI)
   1.236 +  apply (insert multiset_prime_factorization_unique, blast)+
   1.237 +done
   1.238 +
   1.239 +
   1.240 +subsection {* Prime factors and multiplicity for nats and ints *}
   1.241 +
   1.242 +class unique_factorization =
   1.243 +
   1.244 +fixes
   1.245 +  multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" and
   1.246 +  prime_factors :: "'a \<Rightarrow> 'a set"
   1.247 +
   1.248 +(* definitions for the natural numbers *)
   1.249 +
   1.250 +instantiation nat :: unique_factorization
   1.251 +
   1.252 +begin
   1.253 +
   1.254 +definition
   1.255 +  multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   1.256 +where
   1.257 +  "multiplicity_nat p n = count (multiset_prime_factorization n) p"
   1.258 +
   1.259 +definition
   1.260 +  prime_factors_nat :: "nat \<Rightarrow> nat set"
   1.261 +where
   1.262 +  "prime_factors_nat n = set_of (multiset_prime_factorization n)"
   1.263 +
   1.264 +instance proof qed
   1.265 +
   1.266 +end
   1.267 +
   1.268 +(* definitions for the integers *)
   1.269 +
   1.270 +instantiation int :: unique_factorization
   1.271 +
   1.272 +begin
   1.273 +
   1.274 +definition
   1.275 +  multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
   1.276 +where
   1.277 +  "multiplicity_int p n = multiplicity (nat p) (nat n)"
   1.278 +
   1.279 +definition
   1.280 +  prime_factors_int :: "int \<Rightarrow> int set"
   1.281 +where
   1.282 +  "prime_factors_int n = int ` (prime_factors (nat n))"
   1.283 +
   1.284 +instance proof qed
   1.285 +
   1.286 +end
   1.287 +
   1.288 +
   1.289 +subsection {* Set up transfer *}
   1.290 +
   1.291 +lemma transfer_nat_int_prime_factors: 
   1.292 +  "prime_factors (nat n) = nat ` prime_factors n"
   1.293 +  unfolding prime_factors_int_def apply auto
   1.294 +  by (subst transfer_int_nat_set_return_embed, assumption)
   1.295 +
   1.296 +lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> 
   1.297 +    nat_set (prime_factors n)"
   1.298 +  by (auto simp add: nat_set_def prime_factors_int_def)
   1.299 +
   1.300 +lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   1.301 +  multiplicity (nat p) (nat n) = multiplicity p n"
   1.302 +  by (auto simp add: multiplicity_int_def)
   1.303 +
   1.304 +declare TransferMorphism_nat_int[transfer add return: 
   1.305 +  transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   1.306 +  transfer_nat_int_multiplicity]
   1.307 +
   1.308 +
   1.309 +lemma transfer_int_nat_prime_factors:
   1.310 +    "prime_factors (int n) = int ` prime_factors n"
   1.311 +  unfolding prime_factors_int_def by auto
   1.312 +
   1.313 +lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
   1.314 +    nat_set (prime_factors n)"
   1.315 +  by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
   1.316 +
   1.317 +lemma transfer_int_nat_multiplicity: 
   1.318 +    "multiplicity (int p) (int n) = multiplicity p n"
   1.319 +  by (auto simp add: multiplicity_int_def)
   1.320 +
   1.321 +declare TransferMorphism_int_nat[transfer add return: 
   1.322 +  transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   1.323 +  transfer_int_nat_multiplicity]
   1.324 +
   1.325 +
   1.326 +subsection {* Properties of prime factors and multiplicity for nats and ints *}
   1.327 +
   1.328 +lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
   1.329 +  by (unfold prime_factors_int_def, auto)
   1.330 +
   1.331 +lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
   1.332 +  apply (case_tac "n = 0")
   1.333 +  apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
   1.334 +  apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
   1.335 +done
   1.336 +
   1.337 +lemma prime_factors_prime_int [intro]:
   1.338 +  assumes "n >= 0" and "p : prime_factors (n::int)"
   1.339 +  shows "prime p"
   1.340 +
   1.341 +  apply (rule prime_factors_prime_nat [transferred, of n p])
   1.342 +  using prems apply auto
   1.343 +done
   1.344 +
   1.345 +lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
   1.346 +  by (frule prime_factors_prime_nat, auto)
   1.347 +
   1.348 +lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
   1.349 +    p > (0::int)"
   1.350 +  by (frule (1) prime_factors_prime_int, auto)
   1.351 +
   1.352 +lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
   1.353 +  by (unfold prime_factors_nat_def, auto)
   1.354 +
   1.355 +lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
   1.356 +  by (unfold prime_factors_int_def, auto)
   1.357 +
   1.358 +lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
   1.359 +    {p. multiplicity p n > 0}"
   1.360 +  by (force simp add: prime_factors_nat_def multiplicity_nat_def)
   1.361 +
   1.362 +lemma prime_factors_altdef_int: "prime_factors (n::int) = 
   1.363 +    {p. p >= 0 & multiplicity p n > 0}"
   1.364 +  apply (unfold prime_factors_int_def multiplicity_int_def)
   1.365 +  apply (subst prime_factors_altdef_nat)
   1.366 +  apply (auto simp add: image_def)
   1.367 +done
   1.368 +
   1.369 +lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
   1.370 +    n = (PROD p : prime_factors n. p^(multiplicity p n))"
   1.371 +  by (frule multiset_prime_factorization, 
   1.372 +    simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
   1.373 +
   1.374 +thm prime_factorization_nat [transferred] 
   1.375 +
   1.376 +lemma prime_factorization_int: 
   1.377 +  assumes "(n::int) > 0"
   1.378 +  shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
   1.379 +
   1.380 +  apply (rule prime_factorization_nat [transferred, of n])
   1.381 +  using prems apply auto
   1.382 +done
   1.383 +
   1.384 +lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
   1.385 +  by auto
   1.386 +
   1.387 +lemma prime_factorization_unique_nat: 
   1.388 +    "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   1.389 +      n = (PROD p : S. p^(f p)) \<Longrightarrow>
   1.390 +        S = prime_factors n & (ALL p. f p = multiplicity p n)"
   1.391 +  apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset
   1.392 +      f")
   1.393 +  apply (unfold prime_factors_nat_def multiplicity_nat_def)
   1.394 +  apply (simp add: set_of_def count_def Abs_multiset_inverse multiset_def)
   1.395 +  apply (unfold multiset_prime_factorization_def)
   1.396 +  apply (subgoal_tac "n > 0")
   1.397 +  prefer 2
   1.398 +  apply force
   1.399 +  apply (subst if_P, assumption)
   1.400 +  apply (rule the1_equality)
   1.401 +  apply (rule ex_ex1I)
   1.402 +  apply (rule multiset_prime_factorization_exists, assumption)
   1.403 +  apply (rule multiset_prime_factorization_unique)
   1.404 +  apply force
   1.405 +  apply force
   1.406 +  apply force
   1.407 +  unfolding set_of_def count_def msetprod_def
   1.408 +  apply (subgoal_tac "f : multiset")
   1.409 +  apply (auto simp only: Abs_multiset_inverse)
   1.410 +  unfolding multiset_def apply force 
   1.411 +done
   1.412 +
   1.413 +lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   1.414 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   1.415 +      prime_factors n = S"
   1.416 +  by (rule prime_factorization_unique_nat [THEN conjunct1, symmetric],
   1.417 +    assumption+)
   1.418 +
   1.419 +lemma prime_factors_characterization'_nat: 
   1.420 +  "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   1.421 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   1.422 +      prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
   1.423 +  apply (rule prime_factors_characterization_nat)
   1.424 +  apply auto
   1.425 +done
   1.426 +
   1.427 +(* A minor glitch:*)
   1.428 +
   1.429 +thm prime_factors_characterization'_nat 
   1.430 +    [where f = "%x. f (int (x::nat))", 
   1.431 +      transferred direction: nat "op <= (0::int)", rule_format]
   1.432 +
   1.433 +(*
   1.434 +  Transfer isn't smart enough to know that the "0 < f p" should 
   1.435 +  remain a comparison between nats. But the transfer still works. 
   1.436 +*)
   1.437 +
   1.438 +lemma primes_characterization'_int [rule_format]: 
   1.439 +    "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   1.440 +      (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   1.441 +        prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
   1.442 +          {p. p >= 0 & 0 < f p}"
   1.443 +
   1.444 +  apply (insert prime_factors_characterization'_nat 
   1.445 +    [where f = "%x. f (int (x::nat))", 
   1.446 +    transferred direction: nat "op <= (0::int)"])
   1.447 +  apply auto
   1.448 +done
   1.449 +
   1.450 +lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   1.451 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   1.452 +      prime_factors n = S"
   1.453 +  apply simp
   1.454 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   1.455 +  apply (simp only:)
   1.456 +  apply (subst primes_characterization'_int)
   1.457 +  apply auto
   1.458 +  apply (auto simp add: prime_ge_0_int)
   1.459 +done
   1.460 +
   1.461 +lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   1.462 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   1.463 +      multiplicity p n = f p"
   1.464 +  by (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, 
   1.465 +    symmetric], auto)
   1.466 +
   1.467 +lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
   1.468 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
   1.469 +      multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
   1.470 +  apply (rule impI)+
   1.471 +  apply (rule multiplicity_characterization_nat)
   1.472 +  apply auto
   1.473 +done
   1.474 +
   1.475 +lemma multiplicity_characterization'_int [rule_format]: 
   1.476 +  "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   1.477 +    (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
   1.478 +      multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
   1.479 +
   1.480 +  apply (insert multiplicity_characterization'_nat 
   1.481 +    [where f = "%x. f (int (x::nat))", 
   1.482 +      transferred direction: nat "op <= (0::int)", rule_format])
   1.483 +  apply auto
   1.484 +done
   1.485 +
   1.486 +lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   1.487 +    finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   1.488 +      p >= 0 \<Longrightarrow> multiplicity p n = f p"
   1.489 +  apply simp
   1.490 +  apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   1.491 +  apply (simp only:)
   1.492 +  apply (subst multiplicity_characterization'_int)
   1.493 +  apply auto
   1.494 +  apply (auto simp add: prime_ge_0_int)
   1.495 +done
   1.496 +
   1.497 +lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
   1.498 +  by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
   1.499 +
   1.500 +lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
   1.501 +  by (simp add: multiplicity_int_def) 
   1.502 +
   1.503 +lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
   1.504 +  by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
   1.505 +
   1.506 +lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
   1.507 +  by (simp add: multiplicity_int_def)
   1.508 +
   1.509 +lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
   1.510 +  apply (subst multiplicity_characterization_nat
   1.511 +      [where f = "(%q. if q = p then 1 else 0)"])
   1.512 +  apply auto
   1.513 +  apply (case_tac "x = p")
   1.514 +  apply auto
   1.515 +done
   1.516 +
   1.517 +lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
   1.518 +  unfolding prime_int_def multiplicity_int_def by auto
   1.519 +
   1.520 +lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> 
   1.521 +    multiplicity p (p^n) = n"
   1.522 +  apply (case_tac "n = 0")
   1.523 +  apply auto
   1.524 +  apply (subst multiplicity_characterization_nat
   1.525 +      [where f = "(%q. if q = p then n else 0)"])
   1.526 +  apply auto
   1.527 +  apply (case_tac "x = p")
   1.528 +  apply auto
   1.529 +done
   1.530 +
   1.531 +lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> 
   1.532 +    multiplicity p (p^n) = n"
   1.533 +  apply (frule prime_ge_0_int)
   1.534 +  apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
   1.535 +done
   1.536 +
   1.537 +lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> 
   1.538 +    multiplicity p n = 0"
   1.539 +  apply (case_tac "n = 0")
   1.540 +  apply auto
   1.541 +  apply (frule multiset_prime_factorization)
   1.542 +  apply (auto simp add: set_of_def multiplicity_nat_def)
   1.543 +done
   1.544 +
   1.545 +lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
   1.546 +  by (unfold multiplicity_int_def prime_int_def, auto)
   1.547 +
   1.548 +lemma multiplicity_not_factor_nat [simp]: 
   1.549 +    "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
   1.550 +  by (subst (asm) prime_factors_altdef_nat, auto)
   1.551 +
   1.552 +lemma multiplicity_not_factor_int [simp]: 
   1.553 +    "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
   1.554 +  by (subst (asm) prime_factors_altdef_int, auto)
   1.555 +
   1.556 +lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
   1.557 +    (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   1.558 +    (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   1.559 +  apply (rule prime_factorization_unique_nat)
   1.560 +  apply (simp only: prime_factors_altdef_nat)
   1.561 +  apply auto
   1.562 +  apply (subst power_add)
   1.563 +  apply (subst setprod_timesf)
   1.564 +  apply (rule arg_cong2)back back
   1.565 +  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
   1.566 +      (prime_factors l - prime_factors k)")
   1.567 +  apply (erule ssubst)
   1.568 +  apply (subst setprod_Un_disjoint)
   1.569 +  apply auto
   1.570 +  apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
   1.571 +      (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
   1.572 +  apply (erule ssubst)
   1.573 +  apply (simp add: setprod_1)
   1.574 +  apply (erule prime_factorization_nat)
   1.575 +  apply (rule setprod_cong, auto)
   1.576 +  apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
   1.577 +      (prime_factors k - prime_factors l)")
   1.578 +  apply (erule ssubst)
   1.579 +  apply (subst setprod_Un_disjoint)
   1.580 +  apply auto
   1.581 +  apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
   1.582 +      (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
   1.583 +  apply (erule ssubst)
   1.584 +  apply (simp add: setprod_1)
   1.585 +  apply (erule prime_factorization_nat)
   1.586 +  apply (rule setprod_cong, auto)
   1.587 +done
   1.588 +
   1.589 +(* transfer doesn't have the same problem here with the right 
   1.590 +   choice of rules. *)
   1.591 +
   1.592 +lemma multiplicity_product_aux_int: 
   1.593 +  assumes "(k::int) > 0" and "l > 0"
   1.594 +  shows 
   1.595 +    "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   1.596 +    (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   1.597 +
   1.598 +  apply (rule multiplicity_product_aux_nat [transferred, of l k])
   1.599 +  using prems apply auto
   1.600 +done
   1.601 +
   1.602 +lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   1.603 +    prime_factors k Un prime_factors l"
   1.604 +  by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
   1.605 +
   1.606 +lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   1.607 +    prime_factors k Un prime_factors l"
   1.608 +  by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
   1.609 +
   1.610 +lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
   1.611 +    multiplicity p k + multiplicity p l"
   1.612 +  by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
   1.613 +      symmetric])
   1.614 +
   1.615 +lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
   1.616 +    multiplicity p (k * l) = multiplicity p k + multiplicity p l"
   1.617 +  by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
   1.618 +      symmetric])
   1.619 +
   1.620 +lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
   1.621 +    multiplicity (p::nat) (PROD x : S. f x) = 
   1.622 +      (SUM x : S. multiplicity p (f x))"
   1.623 +  apply (induct set: finite)
   1.624 +  apply auto
   1.625 +  apply (subst multiplicity_product_nat)
   1.626 +  apply auto
   1.627 +done
   1.628 +
   1.629 +(* Transfer is delicate here for two reasons: first, because there is
   1.630 +   an implicit quantifier over functions (f), and, second, because the 
   1.631 +   product over the multiplicity should not be translated to an integer 
   1.632 +   product.
   1.633 +
   1.634 +   The way to handle the first is to use quantifier rules for functions.
   1.635 +   The way to handle the second is to turn off the offending rule.
   1.636 +*)
   1.637 +
   1.638 +lemma transfer_nat_int_sum_prod_closure3:
   1.639 +  "(SUM x : A. int (f x)) >= 0"
   1.640 +  "(PROD x : A. int (f x)) >= 0"
   1.641 +  apply (rule setsum_nonneg, auto)
   1.642 +  apply (rule setprod_nonneg, auto)
   1.643 +done
   1.644 +
   1.645 +declare TransferMorphism_nat_int[transfer 
   1.646 +  add return: transfer_nat_int_sum_prod_closure3
   1.647 +  del: transfer_nat_int_sum_prod2 (1)]
   1.648 +
   1.649 +lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
   1.650 +  (ALL x : S. f x > 0) \<Longrightarrow> 
   1.651 +    multiplicity (p::int) (PROD x : S. f x) = 
   1.652 +      (SUM x : S. multiplicity p (f x))"
   1.653 +
   1.654 +  apply (frule multiplicity_setprod_nat
   1.655 +    [where f = "%x. nat(int(nat(f x)))", 
   1.656 +      transferred direction: nat "op <= (0::int)"])
   1.657 +  apply auto
   1.658 +  apply (subst (asm) setprod_cong)
   1.659 +  apply (rule refl)
   1.660 +  apply (rule if_P)
   1.661 +  apply auto
   1.662 +  apply (rule setsum_cong)
   1.663 +  apply auto
   1.664 +done
   1.665 +
   1.666 +declare TransferMorphism_nat_int[transfer 
   1.667 +  add return: transfer_nat_int_sum_prod2 (1)]
   1.668 +
   1.669 +lemma multiplicity_prod_prime_powers_nat:
   1.670 +    "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
   1.671 +       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   1.672 +  apply (subgoal_tac "(PROD p : S. p ^ f p) = 
   1.673 +      (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
   1.674 +  apply (erule ssubst)
   1.675 +  apply (subst multiplicity_characterization_nat)
   1.676 +  prefer 5 apply (rule refl)
   1.677 +  apply (rule refl)
   1.678 +  apply auto
   1.679 +  apply (subst setprod_mono_one_right)
   1.680 +  apply assumption
   1.681 +  prefer 3
   1.682 +  apply (rule setprod_cong)
   1.683 +  apply (rule refl)
   1.684 +  apply auto
   1.685 +done
   1.686 +
   1.687 +(* Here the issue with transfer is the implicit quantifier over S *)
   1.688 +
   1.689 +lemma multiplicity_prod_prime_powers_int:
   1.690 +    "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   1.691 +       multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   1.692 +
   1.693 +  apply (subgoal_tac "int ` nat ` S = S")
   1.694 +  apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
   1.695 +    and S = "nat ` S", transferred])
   1.696 +  apply auto
   1.697 +  apply (subst prime_int_def [symmetric])
   1.698 +  apply auto
   1.699 +  apply (subgoal_tac "xb >= 0")
   1.700 +  apply force
   1.701 +  apply (rule prime_ge_0_int)
   1.702 +  apply force
   1.703 +  apply (subst transfer_nat_int_set_return_embed)
   1.704 +  apply (unfold nat_set_def, auto)
   1.705 +done
   1.706 +
   1.707 +lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
   1.708 +    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   1.709 +  apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   1.710 +  apply (erule ssubst)
   1.711 +  apply (subst multiplicity_prod_prime_powers_nat)
   1.712 +  apply auto
   1.713 +done
   1.714 +
   1.715 +lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
   1.716 +    p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   1.717 +  apply (frule prime_ge_0_int [of q])
   1.718 +  apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
   1.719 +  prefer 4
   1.720 +  apply assumption
   1.721 +  apply auto
   1.722 +done
   1.723 +
   1.724 +lemma dvd_multiplicity_nat: 
   1.725 +    "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
   1.726 +  apply (case_tac "x = 0")
   1.727 +  apply (auto simp add: dvd_def multiplicity_product_nat)
   1.728 +done
   1.729 +
   1.730 +lemma dvd_multiplicity_int: 
   1.731 +    "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
   1.732 +      multiplicity p x <= multiplicity p y"
   1.733 +  apply (case_tac "x = 0")
   1.734 +  apply (auto simp add: dvd_def)
   1.735 +  apply (subgoal_tac "0 < k")
   1.736 +  apply (auto simp add: multiplicity_product_int)
   1.737 +  apply (erule zero_less_mult_pos)
   1.738 +  apply arith
   1.739 +done
   1.740 +
   1.741 +lemma dvd_prime_factors_nat [intro]:
   1.742 +    "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   1.743 +  apply (simp only: prime_factors_altdef_nat)
   1.744 +  apply auto
   1.745 +  apply (frule dvd_multiplicity_nat)
   1.746 +  apply auto
   1.747 +(* It is a shame that auto and arith don't get this. *)
   1.748 +  apply (erule order_less_le_trans)back
   1.749 +  apply assumption
   1.750 +done
   1.751 +
   1.752 +lemma dvd_prime_factors_int [intro]:
   1.753 +    "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   1.754 +  apply (auto simp add: prime_factors_altdef_int)
   1.755 +  apply (erule order_less_le_trans)
   1.756 +  apply (rule dvd_multiplicity_int)
   1.757 +  apply auto
   1.758 +done
   1.759 +
   1.760 +lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
   1.761 +    ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
   1.762 +      x dvd y"
   1.763 +  apply (subst prime_factorization_nat [of x], assumption)
   1.764 +  apply (subst prime_factorization_nat [of y], assumption)
   1.765 +  apply (rule setprod_dvd_setprod_subset2)
   1.766 +  apply force
   1.767 +  apply (subst prime_factors_altdef_nat)+
   1.768 +  apply auto
   1.769 +(* Again, a shame that auto and arith don't get this. *)
   1.770 +  apply (drule_tac x = xa in spec, auto)
   1.771 +  apply (rule le_imp_power_dvd)
   1.772 +  apply blast
   1.773 +done
   1.774 +
   1.775 +lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
   1.776 +    ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
   1.777 +      x dvd y"
   1.778 +  apply (subst prime_factorization_int [of x], assumption)
   1.779 +  apply (subst prime_factorization_int [of y], assumption)
   1.780 +  apply (rule setprod_dvd_setprod_subset2)
   1.781 +  apply force
   1.782 +  apply (subst prime_factors_altdef_int)+
   1.783 +  apply auto
   1.784 +  apply (rule dvd_power_le)
   1.785 +  apply auto
   1.786 +  apply (drule_tac x = xa in spec)
   1.787 +  apply (erule impE)
   1.788 +  apply auto
   1.789 +done
   1.790 +
   1.791 +lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
   1.792 +    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   1.793 +  apply (cases "y = 0")
   1.794 +  apply auto
   1.795 +  apply (rule multiplicity_dvd_nat, auto)
   1.796 +  apply (case_tac "prime p")
   1.797 +  apply auto
   1.798 +done
   1.799 +
   1.800 +lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   1.801 +    \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   1.802 +  apply (cases "y = 0")
   1.803 +  apply auto
   1.804 +  apply (rule multiplicity_dvd_int, auto)
   1.805 +  apply (case_tac "prime p")
   1.806 +  apply auto
   1.807 +done
   1.808 +
   1.809 +lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   1.810 +    (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
   1.811 +  by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
   1.812 +
   1.813 +lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
   1.814 +    (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
   1.815 +  by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
   1.816 +
   1.817 +lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
   1.818 +    (p : prime_factors n) = (prime p & p dvd n)"
   1.819 +  apply (case_tac "prime p")
   1.820 +  apply auto
   1.821 +  apply (subst prime_factorization_nat [where n = n], assumption)
   1.822 +  apply (rule dvd_trans) 
   1.823 +  apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   1.824 +  apply (subst (asm) prime_factors_altdef_nat, force)
   1.825 +  apply (rule dvd_setprod)
   1.826 +  apply auto  
   1.827 +  apply (subst prime_factors_altdef_nat)
   1.828 +  apply (subst (asm) dvd_multiplicity_eq_nat)
   1.829 +  apply auto
   1.830 +  apply (drule spec [where x = p])
   1.831 +  apply auto
   1.832 +done
   1.833 +
   1.834 +lemma prime_factors_altdef2_int: 
   1.835 +  assumes "(n::int) > 0" 
   1.836 +  shows "(p : prime_factors n) = (prime p & p dvd n)"
   1.837 +
   1.838 +  apply (case_tac "p >= 0")
   1.839 +  apply (rule prime_factors_altdef2_nat [transferred])
   1.840 +  using prems apply auto
   1.841 +  apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
   1.842 +done
   1.843 +
   1.844 +lemma multiplicity_eq_nat:
   1.845 +  fixes x and y::nat 
   1.846 +  assumes [arith]: "x > 0" "y > 0" and
   1.847 +    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   1.848 +  shows "x = y"
   1.849 +
   1.850 +  apply (rule dvd_anti_sym)
   1.851 +  apply (auto intro: multiplicity_dvd'_nat) 
   1.852 +done
   1.853 +
   1.854 +lemma multiplicity_eq_int:
   1.855 +  fixes x and y::int 
   1.856 +  assumes [arith]: "x > 0" "y > 0" and
   1.857 +    mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   1.858 +  shows "x = y"
   1.859 +
   1.860 +  apply (rule dvd_anti_sym [transferred])
   1.861 +  apply (auto intro: multiplicity_dvd'_int) 
   1.862 +done
   1.863 +
   1.864 +
   1.865 +subsection {* An application *}
   1.866 +
   1.867 +lemma gcd_eq_nat: 
   1.868 +  assumes pos [arith]: "x > 0" "y > 0"
   1.869 +  shows "gcd (x::nat) y = 
   1.870 +    (PROD p: prime_factors x Un prime_factors y. 
   1.871 +      p ^ (min (multiplicity p x) (multiplicity p y)))"
   1.872 +proof -
   1.873 +  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   1.874 +      p ^ (min (multiplicity p x) (multiplicity p y)))"
   1.875 +  have [arith]: "z > 0"
   1.876 +    unfolding z_def by (rule setprod_pos_nat, auto)
   1.877 +  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   1.878 +      min (multiplicity p x) (multiplicity p y)"
   1.879 +    unfolding z_def
   1.880 +    apply (subst multiplicity_prod_prime_powers_nat)
   1.881 +    apply (auto simp add: multiplicity_not_factor_nat)
   1.882 +    done
   1.883 +  have "z dvd x" 
   1.884 +    by (intro multiplicity_dvd'_nat, auto simp add: aux)
   1.885 +  moreover have "z dvd y" 
   1.886 +    by (intro multiplicity_dvd'_nat, auto simp add: aux)
   1.887 +  moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
   1.888 +    apply auto
   1.889 +    apply (case_tac "w = 0", auto)
   1.890 +    apply (erule multiplicity_dvd'_nat)
   1.891 +    apply (auto intro: dvd_multiplicity_nat simp add: aux)
   1.892 +    done
   1.893 +  ultimately have "z = gcd x y"
   1.894 +    by (subst gcd_unique_nat [symmetric], blast)
   1.895 +  thus ?thesis
   1.896 +    unfolding z_def by auto
   1.897 +qed
   1.898 +
   1.899 +lemma lcm_eq_nat: 
   1.900 +  assumes pos [arith]: "x > 0" "y > 0"
   1.901 +  shows "lcm (x::nat) y = 
   1.902 +    (PROD p: prime_factors x Un prime_factors y. 
   1.903 +      p ^ (max (multiplicity p x) (multiplicity p y)))"
   1.904 +proof -
   1.905 +  def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   1.906 +      p ^ (max (multiplicity p x) (multiplicity p y)))"
   1.907 +  have [arith]: "z > 0"
   1.908 +    unfolding z_def by (rule setprod_pos_nat, auto)
   1.909 +  have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   1.910 +      max (multiplicity p x) (multiplicity p y)"
   1.911 +    unfolding z_def
   1.912 +    apply (subst multiplicity_prod_prime_powers_nat)
   1.913 +    apply (auto simp add: multiplicity_not_factor_nat)
   1.914 +    done
   1.915 +  have "x dvd z" 
   1.916 +    by (intro multiplicity_dvd'_nat, auto simp add: aux)
   1.917 +  moreover have "y dvd z" 
   1.918 +    by (intro multiplicity_dvd'_nat, auto simp add: aux)
   1.919 +  moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
   1.920 +    apply auto
   1.921 +    apply (case_tac "w = 0", auto)
   1.922 +    apply (rule multiplicity_dvd'_nat)
   1.923 +    apply (auto intro: dvd_multiplicity_nat simp add: aux)
   1.924 +    done
   1.925 +  ultimately have "z = lcm x y"
   1.926 +    by (subst lcm_unique_nat [symmetric], blast)
   1.927 +  thus ?thesis
   1.928 +    unfolding z_def by auto
   1.929 +qed
   1.930 +
   1.931 +lemma multiplicity_gcd_nat: 
   1.932 +  assumes [arith]: "x > 0" "y > 0"
   1.933 +  shows "multiplicity (p::nat) (gcd x y) = 
   1.934 +    min (multiplicity p x) (multiplicity p y)"
   1.935 +
   1.936 +  apply (subst gcd_eq_nat)
   1.937 +  apply auto
   1.938 +  apply (subst multiplicity_prod_prime_powers_nat)
   1.939 +  apply auto
   1.940 +done
   1.941 +
   1.942 +lemma multiplicity_lcm_nat: 
   1.943 +  assumes [arith]: "x > 0" "y > 0"
   1.944 +  shows "multiplicity (p::nat) (lcm x y) = 
   1.945 +    max (multiplicity p x) (multiplicity p y)"
   1.946 +
   1.947 +  apply (subst lcm_eq_nat)
   1.948 +  apply auto
   1.949 +  apply (subst multiplicity_prod_prime_powers_nat)
   1.950 +  apply auto
   1.951 +done
   1.952 +
   1.953 +lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
   1.954 +  apply (case_tac "x = 0 | y = 0 | z = 0") 
   1.955 +  apply auto
   1.956 +  apply (rule multiplicity_eq_nat)
   1.957 +  apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat 
   1.958 +      lcm_pos_nat)
   1.959 +done
   1.960 +
   1.961 +lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
   1.962 +  apply (subst (1 2 3) gcd_abs_int)
   1.963 +  apply (subst lcm_abs_int)
   1.964 +  apply (subst (2) abs_of_nonneg)
   1.965 +  apply force
   1.966 +  apply (rule gcd_lcm_distrib_nat [transferred])
   1.967 +  apply auto
   1.968 +done
   1.969 +
   1.970 +end