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