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