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