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