src/HOL/Number_Theory/UniqueFactorization.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40461 e876e95588ce
child 41541 1fa4725c4656
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     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 "~~/src/HOL/Library/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 (metis prime_int_def)
   695   apply (metis prime_ge_0_int)
   696   apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
   697 done
   698 
   699 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
   700     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   701   apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   702   apply (erule ssubst)
   703   apply (subst multiplicity_prod_prime_powers_nat)
   704   apply auto
   705 done
   706 
   707 lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
   708     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   709   apply (frule prime_ge_0_int [of q])
   710   apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
   711   prefer 4
   712   apply assumption
   713   apply auto
   714 done
   715 
   716 lemma dvd_multiplicity_nat: 
   717     "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
   718   apply (case_tac "x = 0")
   719   apply (auto simp add: dvd_def multiplicity_product_nat)
   720 done
   721 
   722 lemma dvd_multiplicity_int: 
   723     "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
   724       multiplicity p x <= multiplicity p y"
   725   apply (case_tac "x = 0")
   726   apply (auto simp add: dvd_def)
   727   apply (subgoal_tac "0 < k")
   728   apply (auto simp add: multiplicity_product_int)
   729   apply (erule zero_less_mult_pos)
   730   apply arith
   731 done
   732 
   733 lemma dvd_prime_factors_nat [intro]:
   734     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   735   apply (simp only: prime_factors_altdef_nat)
   736   apply auto
   737   apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
   738 done
   739 
   740 lemma dvd_prime_factors_int [intro]:
   741     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   742   apply (auto simp add: prime_factors_altdef_int)
   743   apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
   744 done
   745 
   746 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
   747     ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow>
   748       x dvd y"
   749   apply (subst prime_factorization_nat [of x], assumption)
   750   apply (subst prime_factorization_nat [of y], assumption)
   751   apply (rule setprod_dvd_setprod_subset2)
   752   apply force
   753   apply (subst prime_factors_altdef_nat)+
   754   apply auto
   755   apply (metis gr0I le_0_eq less_not_refl)
   756   apply (metis le_imp_power_dvd)
   757 done
   758 
   759 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
   760     ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow>
   761       x dvd y"
   762   apply (subst prime_factorization_int [of x], assumption)
   763   apply (subst prime_factorization_int [of y], assumption)
   764   apply (rule setprod_dvd_setprod_subset2)
   765   apply force
   766   apply (subst prime_factors_altdef_int)+
   767   apply auto
   768   apply (metis le_imp_power_dvd prime_factors_ge_0_int)
   769 done
   770 
   771 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
   772     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   773 by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
   774           multiplicity_nonprime_nat neq0_conv)
   775 
   776 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   777     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   778 by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
   779           multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
   780 
   781 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   782     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
   783   by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
   784 
   785 lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
   786     (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
   787   by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
   788 
   789 lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
   790     (p : prime_factors n) = (prime p & p dvd n)"
   791   apply (case_tac "prime p")
   792   apply auto
   793   apply (subst prime_factorization_nat [where n = n], assumption)
   794   apply (rule dvd_trans) 
   795   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   796   apply (subst (asm) prime_factors_altdef_nat, force)
   797   apply (rule dvd_setprod)
   798   apply auto
   799   apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
   800 done
   801 
   802 lemma prime_factors_altdef2_int: 
   803   assumes "(n::int) > 0" 
   804   shows "(p : prime_factors n) = (prime p & p dvd n)"
   805 
   806   apply (case_tac "p >= 0")
   807   apply (rule prime_factors_altdef2_nat [transferred])
   808   using prems apply auto
   809   apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
   810 done
   811 
   812 lemma multiplicity_eq_nat:
   813   fixes x and y::nat 
   814   assumes [arith]: "x > 0" "y > 0" and
   815     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   816   shows "x = y"
   817 
   818   apply (rule dvd_antisym)
   819   apply (auto intro: multiplicity_dvd'_nat) 
   820 done
   821 
   822 lemma multiplicity_eq_int:
   823   fixes x and y::int 
   824   assumes [arith]: "x > 0" "y > 0" and
   825     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   826   shows "x = y"
   827 
   828   apply (rule dvd_antisym [transferred])
   829   apply (auto intro: multiplicity_dvd'_int) 
   830 done
   831 
   832 
   833 subsection {* An application *}
   834 
   835 lemma gcd_eq_nat: 
   836   assumes pos [arith]: "x > 0" "y > 0"
   837   shows "gcd (x::nat) y = 
   838     (PROD p: prime_factors x Un prime_factors y. 
   839       p ^ (min (multiplicity p x) (multiplicity p y)))"
   840 proof -
   841   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   842       p ^ (min (multiplicity p x) (multiplicity p y)))"
   843   have [arith]: "z > 0"
   844     unfolding z_def by (rule setprod_pos_nat, auto)
   845   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   846       min (multiplicity p x) (multiplicity p y)"
   847     unfolding z_def
   848     apply (subst multiplicity_prod_prime_powers_nat)
   849     apply (auto simp add: multiplicity_not_factor_nat)
   850     done
   851   have "z dvd x" 
   852     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   853   moreover have "z dvd y" 
   854     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   855   moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
   856     apply auto
   857     apply (case_tac "w = 0", auto)
   858     apply (erule multiplicity_dvd'_nat)
   859     apply (auto intro: dvd_multiplicity_nat simp add: aux)
   860     done
   861   ultimately have "z = gcd x y"
   862     by (subst gcd_unique_nat [symmetric], blast)
   863   thus ?thesis
   864     unfolding z_def by auto
   865 qed
   866 
   867 lemma lcm_eq_nat: 
   868   assumes pos [arith]: "x > 0" "y > 0"
   869   shows "lcm (x::nat) y = 
   870     (PROD p: prime_factors x Un prime_factors y. 
   871       p ^ (max (multiplicity p x) (multiplicity p y)))"
   872 proof -
   873   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   874       p ^ (max (multiplicity p x) (multiplicity p y)))"
   875   have [arith]: "z > 0"
   876     unfolding z_def by (rule setprod_pos_nat, auto)
   877   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   878       max (multiplicity p x) (multiplicity p y)"
   879     unfolding z_def
   880     apply (subst multiplicity_prod_prime_powers_nat)
   881     apply (auto simp add: multiplicity_not_factor_nat)
   882     done
   883   have "x dvd z" 
   884     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   885   moreover have "y dvd z" 
   886     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   887   moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
   888     apply auto
   889     apply (case_tac "w = 0", auto)
   890     apply (rule multiplicity_dvd'_nat)
   891     apply (auto intro: dvd_multiplicity_nat simp add: aux)
   892     done
   893   ultimately have "z = lcm x y"
   894     by (subst lcm_unique_nat [symmetric], blast)
   895   thus ?thesis
   896     unfolding z_def by auto
   897 qed
   898 
   899 lemma multiplicity_gcd_nat: 
   900   assumes [arith]: "x > 0" "y > 0"
   901   shows "multiplicity (p::nat) (gcd x y) = 
   902     min (multiplicity p x) (multiplicity p y)"
   903 
   904   apply (subst gcd_eq_nat)
   905   apply auto
   906   apply (subst multiplicity_prod_prime_powers_nat)
   907   apply auto
   908 done
   909 
   910 lemma multiplicity_lcm_nat: 
   911   assumes [arith]: "x > 0" "y > 0"
   912   shows "multiplicity (p::nat) (lcm x y) = 
   913     max (multiplicity p x) (multiplicity p y)"
   914 
   915   apply (subst lcm_eq_nat)
   916   apply auto
   917   apply (subst multiplicity_prod_prime_powers_nat)
   918   apply auto
   919 done
   920 
   921 lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
   922   apply (case_tac "x = 0 | y = 0 | z = 0") 
   923   apply auto
   924   apply (rule multiplicity_eq_nat)
   925   apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat 
   926       lcm_pos_nat)
   927 done
   928 
   929 lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
   930   apply (subst (1 2 3) gcd_abs_int)
   931   apply (subst lcm_abs_int)
   932   apply (subst (2) abs_of_nonneg)
   933   apply force
   934   apply (rule gcd_lcm_distrib_nat [transferred])
   935   apply auto
   936 done
   937 
   938 end