src/HOL/Number_Theory/UniqueFactorization.thy
author nipkow
Mon Sep 13 11:13:15 2010 +0200 (2010-09-13)
changeset 39302 d7728f65b353
parent 37290 3464d7232670
child 40461 e876e95588ce
permissions -rw-r--r--
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
     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_empty:
    76   "msetprod f {#} = 1"
    77   by (simp add: msetprod_def)
    78 
    79 lemma msetprod_singleton:
    80   "msetprod f {#x#} = f x"
    81   by (simp add: msetprod_def)
    82 
    83 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
    84   apply (simp add: msetprod_def power_add)
    85   apply (subst setprod_Un2)
    86   apply auto
    87   apply (subgoal_tac 
    88       "(PROD x:set_of A - set_of B. f x ^ count A x * f x ^ count B x) =
    89        (PROD x:set_of A - set_of B. f x ^ count A x)")
    90   apply (erule ssubst)
    91   apply (subgoal_tac 
    92       "(PROD x:set_of B - set_of A. f x ^ count A x * f x ^ count B x) =
    93        (PROD x:set_of B - set_of A. f x ^ count B x)")
    94   apply (erule ssubst)
    95   apply (subgoal_tac "(PROD x:set_of A. f x ^ count A x) = 
    96     (PROD x:set_of A - set_of B. f x ^ count A x) *
    97     (PROD x:set_of A Int set_of B. f x ^ count A x)")
    98   apply (erule ssubst)
    99   apply (subgoal_tac "(PROD x:set_of B. f x ^ count B x) = 
   100     (PROD x:set_of B - set_of A. f x ^ count B x) *
   101     (PROD x:set_of A Int set_of B. f x ^ count B x)")
   102   apply (erule ssubst)
   103   apply (subst setprod_timesf)
   104   apply (force simp add: mult_ac)
   105   apply (subst setprod_Un_disjoint [symmetric])
   106   apply (auto intro: setprod_cong)
   107   apply (subst setprod_Un_disjoint [symmetric])
   108   apply (auto intro: setprod_cong)
   109 done
   110 
   111 
   112 subsection {* unique factorization: multiset version *}
   113 
   114 lemma multiset_prime_factorization_exists [rule_format]: "n > 0 --> 
   115     (EX M. (ALL (p::nat) : set_of M. prime p) & n = (PROD i :# M. i))"
   116 proof (rule nat_less_induct, clarify)
   117   fix n :: nat
   118   assume ih: "ALL m < n. 0 < m --> (EX M. (ALL p : set_of M. prime p) & m = 
   119       (PROD i :# M. i))"
   120   assume "(n::nat) > 0"
   121   then have "n = 1 | (n > 1 & prime n) | (n > 1 & ~ prime n)"
   122     by arith
   123   moreover 
   124   {
   125     assume "n = 1"
   126     then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
   127         by (auto simp add: msetprod_def)
   128   } 
   129   moreover 
   130   {
   131     assume "n > 1" and "prime n"
   132     then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
   133       by (auto simp add: msetprod_def)
   134   } 
   135   moreover 
   136   {
   137     assume "n > 1" and "~ prime n"
   138     from prems not_prime_eq_prod_nat
   139       obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
   140         by blast
   141     with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
   142         and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
   143       by blast
   144     hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
   145       by (auto simp add: prems msetprod_Un set_of_union)
   146     then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
   147   }
   148   ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
   149     by blast
   150 qed
   151 
   152 lemma multiset_prime_factorization_unique_aux:
   153   fixes a :: nat
   154   assumes "(ALL p : set_of M. prime p)" and
   155     "(ALL p : set_of N. prime p)" and
   156     "(PROD i :# M. i) dvd (PROD i:# N. i)"
   157   shows
   158     "count M a <= count N a"
   159 proof cases
   160   assume "a : set_of M"
   161   with prems have a: "prime a"
   162     by auto
   163   with prems have "a ^ count M a dvd (PROD i :# M. i)"
   164     by (auto intro: dvd_setprod simp add: msetprod_def)
   165   also have "... dvd (PROD i :# N. i)"
   166     by (rule prems)
   167   also have "... = (PROD i : (set_of N). i ^ (count N i))"
   168     by (simp add: msetprod_def)
   169   also have "... = 
   170       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
   171     proof (cases)
   172       assume "a : set_of N"
   173       hence b: "set_of N = {a} Un (set_of N - {a})"
   174         by auto
   175       thus ?thesis
   176         by (subst (1) b, subst setprod_Un_disjoint, auto)
   177     next
   178       assume "a ~: set_of N" 
   179       thus ?thesis
   180         by auto
   181     qed
   182   finally have "a ^ count M a dvd 
   183       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
   184   moreover have "coprime (a ^ count M a)
   185       (PROD i : (set_of N - {a}). i ^ (count N i))"
   186     apply (subst gcd_commute_nat)
   187     apply (rule setprod_coprime_nat)
   188     apply (rule primes_imp_powers_coprime_nat)
   189     apply (insert prems, auto) 
   190     done
   191   ultimately have "a ^ count M a dvd a^(count N a)"
   192     by (elim coprime_dvd_mult_nat)
   193   with a show ?thesis 
   194     by (intro power_dvd_imp_le, auto)
   195 next
   196   assume "a ~: set_of M"
   197   thus ?thesis by auto
   198 qed
   199 
   200 lemma multiset_prime_factorization_unique:
   201   assumes "(ALL (p::nat) : set_of M. prime p)" and
   202     "(ALL p : set_of N. prime p)" and
   203     "(PROD i :# M. i) = (PROD i:# N. i)"
   204   shows
   205     "M = N"
   206 proof -
   207   {
   208     fix a
   209     from prems have "count M a <= count N a"
   210       by (intro multiset_prime_factorization_unique_aux, auto) 
   211     moreover from prems have "count N a <= count M a"
   212       by (intro multiset_prime_factorization_unique_aux, auto) 
   213     ultimately have "count M a = count N a"
   214       by auto
   215   }
   216   thus ?thesis by (simp add:multiset_eq_iff)
   217 qed
   218 
   219 definition multiset_prime_factorization :: "nat => nat multiset" where
   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 transfer_morphism_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 transfer_morphism_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 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 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 transfer_morphism_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 transfer_morphism_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