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