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