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