src/HOL/Number_Theory/UniqueFactorization.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 44872 a98ef45122f3
child 48822 21d4ed91912f
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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: "msetprod f {#} = 1"
    75   by (simp add: msetprod_def)
    76 
    77 lemma msetprod_singleton: "msetprod f {#x#} = f x"
    78   by (simp add: msetprod_def)
    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     assume "n = 1"
   122     then have "(ALL p : set_of {#}. prime p) & n = (PROD i :# {#}. i)"
   123         by (auto simp add: msetprod_def)
   124   } moreover {
   125     assume "n > 1" and "prime n"
   126     then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
   127       by (auto simp add: msetprod_def)
   128   } moreover {
   129     assume "n > 1" and "~ prime n"
   130     with not_prime_eq_prod_nat
   131     obtain m k where n: "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     then have "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
   137       by (auto simp add: n msetprod_Un)
   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 M: "a : set_of M"
   153   with assms have a: "prime a" by auto
   154   with M have "a ^ count M a dvd (PROD i :# M. i)"
   155     by (auto intro: dvd_setprod simp add: msetprod_def)
   156   also have "... dvd (PROD i :# N. i)" by (rule assms)
   157   also have "... = (PROD i : (set_of N). i ^ (count N i))"
   158     by (simp add: msetprod_def)
   159   also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
   160   proof (cases)
   161     assume "a : set_of N"
   162     then have b: "set_of N = {a} Un (set_of N - {a})"
   163       by auto
   164     then show ?thesis
   165       by (subst (1) b, subst setprod_Un_disjoint, auto)
   166   next
   167     assume "a ~: set_of N" 
   168     then show ?thesis by auto
   169   qed
   170   finally have "a ^ count M a dvd 
   171       a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))".
   172   moreover
   173   have "coprime (a ^ count M a) (PROD i : (set_of N - {a}). i ^ (count N i))"
   174     apply (subst gcd_commute_nat)
   175     apply (rule setprod_coprime_nat)
   176     apply (rule primes_imp_powers_coprime_nat)
   177     using assms M
   178     apply auto
   179     done
   180   ultimately have "a ^ count M a dvd a^(count N a)"
   181     by (elim coprime_dvd_mult_nat)
   182   with a show ?thesis 
   183     apply (intro power_dvd_imp_le)
   184     apply auto
   185     done
   186 next
   187   assume "a ~: set_of M"
   188   then show ?thesis by auto
   189 qed
   190 
   191 lemma multiset_prime_factorization_unique:
   192   assumes "(ALL (p::nat) : set_of M. prime p)" and
   193     "(ALL p : set_of N. prime p)" and
   194     "(PROD i :# M. i) = (PROD i:# N. i)"
   195   shows
   196     "M = N"
   197 proof -
   198   {
   199     fix a
   200     from assms have "count M a <= count N a"
   201       by (intro multiset_prime_factorization_unique_aux, auto) 
   202     moreover from assms have "count N a <= count M a"
   203       by (intro multiset_prime_factorization_unique_aux, auto) 
   204     ultimately have "count M a = count N a"
   205       by auto
   206   }
   207   then show ?thesis by (simp add:multiset_eq_iff)
   208 qed
   209 
   210 definition multiset_prime_factorization :: "nat => nat multiset"
   211 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   fixes multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat"
   233     and prime_factors :: "'a \<Rightarrow> 'a set"
   234 
   235 (* definitions for the natural numbers *)
   236 
   237 instantiation nat :: unique_factorization
   238 begin
   239 
   240 definition multiplicity_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   241   where "multiplicity_nat p n = count (multiset_prime_factorization n) p"
   242 
   243 definition prime_factors_nat :: "nat \<Rightarrow> nat set"
   244   where "prime_factors_nat n = set_of (multiset_prime_factorization n)"
   245 
   246 instance ..
   247 
   248 end
   249 
   250 (* definitions for the integers *)
   251 
   252 instantiation int :: unique_factorization
   253 begin
   254 
   255 definition multiplicity_int :: "int \<Rightarrow> int \<Rightarrow> nat"
   256   where "multiplicity_int p n = multiplicity (nat p) (nat n)"
   257 
   258 definition prime_factors_int :: "int \<Rightarrow> int set"
   259   where "prime_factors_int n = int ` (prime_factors (nat n))"
   260 
   261 instance ..
   262 
   263 end
   264 
   265 
   266 subsection {* Set up transfer *}
   267 
   268 lemma transfer_nat_int_prime_factors: "prime_factors (nat n) = nat ` prime_factors n"
   269   unfolding prime_factors_int_def
   270   apply auto
   271   apply (subst transfer_int_nat_set_return_embed)
   272   apply assumption
   273   done
   274 
   275 lemma transfer_nat_int_prime_factors_closure: "n >= 0 \<Longrightarrow> nat_set (prime_factors n)"
   276   by (auto simp add: nat_set_def prime_factors_int_def)
   277 
   278 lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   279     multiplicity (nat p) (nat n) = multiplicity p n"
   280   by (auto simp add: multiplicity_int_def)
   281 
   282 declare transfer_morphism_nat_int[transfer add return: 
   283   transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   284   transfer_nat_int_multiplicity]
   285 
   286 
   287 lemma transfer_int_nat_prime_factors: "prime_factors (int n) = int ` prime_factors n"
   288   unfolding prime_factors_int_def by auto
   289 
   290 lemma transfer_int_nat_prime_factors_closure: "is_nat n \<Longrightarrow> 
   291     nat_set (prime_factors n)"
   292   by (simp only: transfer_nat_int_prime_factors_closure is_nat_def)
   293 
   294 lemma transfer_int_nat_multiplicity: 
   295     "multiplicity (int p) (int n) = multiplicity p n"
   296   by (auto simp add: multiplicity_int_def)
   297 
   298 declare transfer_morphism_int_nat[transfer add return: 
   299   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   300   transfer_int_nat_multiplicity]
   301 
   302 
   303 subsection {* Properties of prime factors and multiplicity for nats and ints *}
   304 
   305 lemma prime_factors_ge_0_int [elim]: "p : prime_factors (n::int) \<Longrightarrow> p >= 0"
   306   unfolding prime_factors_int_def by auto
   307 
   308 lemma prime_factors_prime_nat [intro]: "p : prime_factors (n::nat) \<Longrightarrow> prime p"
   309   apply (cases "n = 0")
   310   apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
   311   apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
   312   done
   313 
   314 lemma prime_factors_prime_int [intro]:
   315   assumes "n >= 0" and "p : prime_factors (n::int)"
   316   shows "prime p"
   317   apply (rule prime_factors_prime_nat [transferred, of n p])
   318   using assms apply auto
   319   done
   320 
   321 lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
   322   apply (frule prime_factors_prime_nat)
   323   apply auto
   324   done
   325 
   326 lemma prime_factors_gt_0_int [elim]: "x >= 0 \<Longrightarrow> p : prime_factors x \<Longrightarrow> 
   327     p > (0::int)"
   328   apply (frule (1) prime_factors_prime_int)
   329   apply auto
   330   done
   331 
   332 lemma prime_factors_finite_nat [iff]: "finite (prime_factors (n::nat))"
   333   unfolding prime_factors_nat_def by auto
   334 
   335 lemma prime_factors_finite_int [iff]: "finite (prime_factors (n::int))"
   336   unfolding prime_factors_int_def by auto
   337 
   338 lemma prime_factors_altdef_nat: "prime_factors (n::nat) = 
   339     {p. multiplicity p n > 0}"
   340   by (force simp add: prime_factors_nat_def multiplicity_nat_def)
   341 
   342 lemma prime_factors_altdef_int: "prime_factors (n::int) = 
   343     {p. p >= 0 & multiplicity p n > 0}"
   344   apply (unfold prime_factors_int_def multiplicity_int_def)
   345   apply (subst prime_factors_altdef_nat)
   346   apply (auto simp add: image_def)
   347   done
   348 
   349 lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
   350     n = (PROD p : prime_factors n. p^(multiplicity p n))"
   351   apply (frule multiset_prime_factorization)
   352   apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
   353   done
   354 
   355 lemma prime_factorization_int: 
   356   assumes "(n::int) > 0"
   357   shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
   358   apply (rule prime_factorization_nat [transferred, of n])
   359   using assms apply auto
   360   done
   361 
   362 lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
   363   by auto
   364 
   365 lemma prime_factorization_unique_nat: 
   366     "S = { (p::nat) . f p > 0} \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   367       n = (PROD p : S. p^(f p)) \<Longrightarrow>
   368         S = prime_factors n & (ALL p. f p = multiplicity p n)"
   369   apply (subgoal_tac "multiset_prime_factorization n = Abs_multiset f")
   370   apply (unfold prime_factors_nat_def multiplicity_nat_def)
   371   apply (simp add: set_of_def Abs_multiset_inverse multiset_def)
   372   apply (unfold multiset_prime_factorization_def)
   373   apply (subgoal_tac "n > 0")
   374   prefer 2
   375   apply force
   376   apply (subst if_P, assumption)
   377   apply (rule the1_equality)
   378   apply (rule ex_ex1I)
   379   apply (rule multiset_prime_factorization_exists, assumption)
   380   apply (rule multiset_prime_factorization_unique)
   381   apply force
   382   apply force
   383   apply force
   384   unfolding set_of_def msetprod_def
   385   apply (subgoal_tac "f : multiset")
   386   apply (auto simp only: Abs_multiset_inverse)
   387   unfolding multiset_def apply force 
   388   done
   389 
   390 lemma prime_factors_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   391     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   392       prime_factors n = S"
   393   apply (rule prime_factorization_unique_nat [THEN conjunct1, symmetric])
   394   apply assumption+
   395   done
   396 
   397 lemma prime_factors_characterization'_nat: 
   398   "finite {p. 0 < f (p::nat)} \<Longrightarrow>
   399     (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   400       prime_factors (PROD p | 0 < f p . p ^ f p) = {p. 0 < f p}"
   401   apply (rule prime_factors_characterization_nat)
   402   apply auto
   403   done
   404 
   405 (* A minor glitch:*)
   406 
   407 thm prime_factors_characterization'_nat 
   408     [where f = "%x. f (int (x::nat))", 
   409       transferred direction: nat "op <= (0::int)", rule_format]
   410 
   411 (*
   412   Transfer isn't smart enough to know that the "0 < f p" should 
   413   remain a comparison between nats. But the transfer still works. 
   414 *)
   415 
   416 lemma primes_characterization'_int [rule_format]: 
   417     "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   418       (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow>
   419         prime_factors (PROD p | p >=0 & 0 < f p . p ^ f p) = 
   420           {p. p >= 0 & 0 < f p}"
   421 
   422   apply (insert prime_factors_characterization'_nat 
   423     [where f = "%x. f (int (x::nat))", 
   424     transferred direction: nat "op <= (0::int)"])
   425   apply auto
   426   done
   427 
   428 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   429     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   430       prime_factors n = S"
   431   apply simp
   432   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   433   apply (simp only:)
   434   apply (subst primes_characterization'_int)
   435   apply auto
   436   apply (auto simp add: prime_ge_0_int)
   437   done
   438 
   439 lemma multiplicity_characterization_nat: "S = {p. 0 < f (p::nat)} \<Longrightarrow> 
   440     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   441       multiplicity p n = f p"
   442   apply (frule prime_factorization_unique_nat [THEN conjunct2, rule_format, symmetric])
   443   apply auto
   444   done
   445 
   446 lemma multiplicity_characterization'_nat: "finite {p. 0 < f (p::nat)} \<longrightarrow>
   447     (ALL p. 0 < f p \<longrightarrow> prime p) \<longrightarrow>
   448       multiplicity p (PROD p | 0 < f p . p ^ f p) = f p"
   449   apply (intro impI)
   450   apply (rule multiplicity_characterization_nat)
   451   apply auto
   452   done
   453 
   454 lemma multiplicity_characterization'_int [rule_format]: 
   455   "finite {p. p >= 0 & 0 < f (p::int)} \<Longrightarrow>
   456     (ALL p. 0 < f p \<longrightarrow> prime p) \<Longrightarrow> p >= 0 \<Longrightarrow>
   457       multiplicity p (PROD p | p >= 0 & 0 < f p . p ^ f p) = f p"
   458   apply (insert multiplicity_characterization'_nat 
   459     [where f = "%x. f (int (x::nat))", 
   460       transferred direction: nat "op <= (0::int)", rule_format])
   461   apply auto
   462   done
   463 
   464 lemma multiplicity_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
   465     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
   466       p >= 0 \<Longrightarrow> multiplicity p n = f p"
   467   apply simp
   468   apply (subgoal_tac "{p. 0 < f p} = {p. 0 <= p & 0 < f p}")
   469   apply (simp only:)
   470   apply (subst multiplicity_characterization'_int)
   471   apply auto
   472   apply (auto simp add: prime_ge_0_int)
   473   done
   474 
   475 lemma multiplicity_zero_nat [simp]: "multiplicity (p::nat) 0 = 0"
   476   by (simp add: multiplicity_nat_def multiset_prime_factorization_def)
   477 
   478 lemma multiplicity_zero_int [simp]: "multiplicity (p::int) 0 = 0"
   479   by (simp add: multiplicity_int_def) 
   480 
   481 lemma multiplicity_one_nat [simp]: "multiplicity p (1::nat) = 0"
   482   by (subst multiplicity_characterization_nat [where f = "%x. 0"], auto)
   483 
   484 lemma multiplicity_one_int [simp]: "multiplicity p (1::int) = 0"
   485   by (simp add: multiplicity_int_def)
   486 
   487 lemma multiplicity_prime_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p p = 1"
   488   apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then 1 else 0)"])
   489   apply auto
   490   apply (case_tac "x = p")
   491   apply auto
   492   done
   493 
   494 lemma multiplicity_prime_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p p = 1"
   495   unfolding prime_int_def multiplicity_int_def by auto
   496 
   497 lemma multiplicity_prime_power_nat [simp]: "prime (p::nat) \<Longrightarrow> multiplicity p (p^n) = n"
   498   apply (cases "n = 0")
   499   apply auto
   500   apply (subst multiplicity_characterization_nat [where f = "(%q. if q = p then n else 0)"])
   501   apply auto
   502   apply (case_tac "x = p")
   503   apply auto
   504   done
   505 
   506 lemma multiplicity_prime_power_int [simp]: "prime (p::int) \<Longrightarrow> multiplicity p (p^n) = n"
   507   apply (frule prime_ge_0_int)
   508   apply (auto simp add: prime_int_def multiplicity_int_def nat_power_eq)
   509   done
   510 
   511 lemma multiplicity_nonprime_nat [simp]: "~ prime (p::nat) \<Longrightarrow> multiplicity p n = 0"
   512   apply (cases "n = 0")
   513   apply auto
   514   apply (frule multiset_prime_factorization)
   515   apply (auto simp add: set_of_def multiplicity_nat_def)
   516   done
   517 
   518 lemma multiplicity_nonprime_int [simp]: "~ prime (p::int) \<Longrightarrow> multiplicity p n = 0"
   519   unfolding multiplicity_int_def prime_int_def by auto
   520 
   521 lemma multiplicity_not_factor_nat [simp]: 
   522     "p ~: prime_factors (n::nat) \<Longrightarrow> multiplicity p n = 0"
   523   apply (subst (asm) prime_factors_altdef_nat)
   524   apply auto
   525   done
   526 
   527 lemma multiplicity_not_factor_int [simp]: 
   528     "p >= 0 \<Longrightarrow> p ~: prime_factors (n::int) \<Longrightarrow> multiplicity p n = 0"
   529   apply (subst (asm) prime_factors_altdef_int)
   530   apply auto
   531   done
   532 
   533 lemma multiplicity_product_aux_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow>
   534     (prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   535     (ALL p. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   536   apply (rule prime_factorization_unique_nat)
   537   apply (simp only: prime_factors_altdef_nat)
   538   apply auto
   539   apply (subst power_add)
   540   apply (subst setprod_timesf)
   541   apply (rule arg_cong2)back back
   542   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors k Un 
   543       (prime_factors l - prime_factors k)")
   544   apply (erule ssubst)
   545   apply (subst setprod_Un_disjoint)
   546   apply auto
   547   apply (subgoal_tac "(\<Prod>p\<in>prime_factors l - prime_factors k. p ^ multiplicity p k) = 
   548       (\<Prod>p\<in>prime_factors l - prime_factors k. 1)")
   549   apply (erule ssubst)
   550   apply (simp add: setprod_1)
   551   apply (erule prime_factorization_nat)
   552   apply (rule setprod_cong, auto)
   553   apply (subgoal_tac "prime_factors k Un prime_factors l = prime_factors l Un 
   554       (prime_factors k - prime_factors l)")
   555   apply (erule ssubst)
   556   apply (subst setprod_Un_disjoint)
   557   apply auto
   558   apply (subgoal_tac "(\<Prod>p\<in>prime_factors k - prime_factors l. p ^ multiplicity p l) = 
   559       (\<Prod>p\<in>prime_factors k - prime_factors l. 1)")
   560   apply (erule ssubst)
   561   apply (simp add: setprod_1)
   562   apply (erule prime_factorization_nat)
   563   apply (rule setprod_cong, auto)
   564   done
   565 
   566 (* transfer doesn't have the same problem here with the right 
   567    choice of rules. *)
   568 
   569 lemma multiplicity_product_aux_int: 
   570   assumes "(k::int) > 0" and "l > 0"
   571   shows 
   572     "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
   573     (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
   574   apply (rule multiplicity_product_aux_nat [transferred, of l k])
   575   using assms apply auto
   576   done
   577 
   578 lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   579     prime_factors k Un prime_factors l"
   580   by (rule multiplicity_product_aux_nat [THEN conjunct1, symmetric])
   581 
   582 lemma prime_factors_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) = 
   583     prime_factors k Un prime_factors l"
   584   by (rule multiplicity_product_aux_int [THEN conjunct1, symmetric])
   585 
   586 lemma multiplicity_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> multiplicity p (k * l) = 
   587     multiplicity p k + multiplicity p l"
   588   by (rule multiplicity_product_aux_nat [THEN conjunct2, rule_format, 
   589       symmetric])
   590 
   591 lemma multiplicity_product_int: "(k::int) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> p >= 0 \<Longrightarrow> 
   592     multiplicity p (k * l) = multiplicity p k + multiplicity p l"
   593   by (rule multiplicity_product_aux_int [THEN conjunct2, rule_format, 
   594       symmetric])
   595 
   596 lemma multiplicity_setprod_nat: "finite S \<Longrightarrow> (ALL x : S. f x > 0) \<Longrightarrow> 
   597     multiplicity (p::nat) (PROD x : S. f x) = 
   598       (SUM x : S. multiplicity p (f x))"
   599   apply (induct set: finite)
   600   apply auto
   601   apply (subst multiplicity_product_nat)
   602   apply auto
   603   done
   604 
   605 (* Transfer is delicate here for two reasons: first, because there is
   606    an implicit quantifier over functions (f), and, second, because the 
   607    product over the multiplicity should not be translated to an integer 
   608    product.
   609 
   610    The way to handle the first is to use quantifier rules for functions.
   611    The way to handle the second is to turn off the offending rule.
   612 *)
   613 
   614 lemma transfer_nat_int_sum_prod_closure3:
   615   "(SUM x : A. int (f x)) >= 0"
   616   "(PROD x : A. int (f x)) >= 0"
   617   apply (rule setsum_nonneg, auto)
   618   apply (rule setprod_nonneg, auto)
   619   done
   620 
   621 declare transfer_morphism_nat_int[transfer 
   622   add return: transfer_nat_int_sum_prod_closure3
   623   del: transfer_nat_int_sum_prod2 (1)]
   624 
   625 lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
   626   (ALL x : S. f x > 0) \<Longrightarrow> 
   627     multiplicity (p::int) (PROD x : S. f x) = 
   628       (SUM x : S. multiplicity p (f x))"
   629 
   630   apply (frule multiplicity_setprod_nat
   631     [where f = "%x. nat(int(nat(f x)))", 
   632       transferred direction: nat "op <= (0::int)"])
   633   apply auto
   634   apply (subst (asm) setprod_cong)
   635   apply (rule refl)
   636   apply (rule if_P)
   637   apply auto
   638   apply (rule setsum_cong)
   639   apply auto
   640   done
   641 
   642 declare transfer_morphism_nat_int[transfer 
   643   add return: transfer_nat_int_sum_prod2 (1)]
   644 
   645 lemma multiplicity_prod_prime_powers_nat:
   646     "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
   647        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   648   apply (subgoal_tac "(PROD p : S. p ^ f p) = 
   649       (PROD p : S. p ^ (%x. if x : S then f x else 0) p)")
   650   apply (erule ssubst)
   651   apply (subst multiplicity_characterization_nat)
   652   prefer 5 apply (rule refl)
   653   apply (rule refl)
   654   apply auto
   655   apply (subst setprod_mono_one_right)
   656   apply assumption
   657   prefer 3
   658   apply (rule setprod_cong)
   659   apply (rule refl)
   660   apply auto
   661 done
   662 
   663 (* Here the issue with transfer is the implicit quantifier over S *)
   664 
   665 lemma multiplicity_prod_prime_powers_int:
   666     "(p::int) >= 0 \<Longrightarrow> finite S \<Longrightarrow> (ALL p : S. prime p) \<Longrightarrow>
   667        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"
   668   apply (subgoal_tac "int ` nat ` S = S")
   669   apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
   670     and S = "nat ` S", transferred])
   671   apply auto
   672   apply (metis prime_int_def)
   673   apply (metis prime_ge_0_int)
   674   apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
   675   done
   676 
   677 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
   678     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   679   apply (subgoal_tac "q^n = setprod (%x. x^n) {q}")
   680   apply (erule ssubst)
   681   apply (subst multiplicity_prod_prime_powers_nat)
   682   apply auto
   683   done
   684 
   685 lemma multiplicity_distinct_prime_power_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow>
   686     p ~= q \<Longrightarrow> multiplicity p (q^n) = 0"
   687   apply (frule prime_ge_0_int [of q])
   688   apply (frule multiplicity_distinct_prime_power_nat [transferred leaving: n]) 
   689   prefer 4
   690   apply assumption
   691   apply auto
   692   done
   693 
   694 lemma dvd_multiplicity_nat:
   695     "(0::nat) < y \<Longrightarrow> x dvd y \<Longrightarrow> multiplicity p x <= multiplicity p y"
   696   apply (cases "x = 0")
   697   apply (auto simp add: dvd_def multiplicity_product_nat)
   698   done
   699 
   700 lemma dvd_multiplicity_int: 
   701     "(0::int) < y \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> p >= 0 \<Longrightarrow> 
   702       multiplicity p x <= multiplicity p y"
   703   apply (cases "x = 0")
   704   apply (auto simp add: dvd_def)
   705   apply (subgoal_tac "0 < k")
   706   apply (auto simp add: multiplicity_product_int)
   707   apply (erule zero_less_mult_pos)
   708   apply arith
   709   done
   710 
   711 lemma dvd_prime_factors_nat [intro]:
   712     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   713   apply (simp only: prime_factors_altdef_nat)
   714   apply auto
   715   apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
   716   done
   717 
   718 lemma dvd_prime_factors_int [intro]:
   719     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   720   apply (auto simp add: prime_factors_altdef_int)
   721   apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
   722   done
   723 
   724 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
   725     ALL p. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
   726   apply (subst prime_factorization_nat [of x], assumption)
   727   apply (subst prime_factorization_nat [of y], assumption)
   728   apply (rule setprod_dvd_setprod_subset2)
   729   apply force
   730   apply (subst prime_factors_altdef_nat)+
   731   apply auto
   732   apply (metis gr0I le_0_eq less_not_refl)
   733   apply (metis le_imp_power_dvd)
   734   done
   735 
   736 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
   737     ALL p >= 0. multiplicity p x <= multiplicity p y \<Longrightarrow> x dvd y"
   738   apply (subst prime_factorization_int [of x], assumption)
   739   apply (subst prime_factorization_int [of y], assumption)
   740   apply (rule setprod_dvd_setprod_subset2)
   741   apply force
   742   apply (subst prime_factors_altdef_int)+
   743   apply auto
   744   apply (metis le_imp_power_dvd prime_factors_ge_0_int)
   745   done
   746 
   747 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
   748     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   749   by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
   750       multiplicity_nonprime_nat neq0_conv)
   751 
   752 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
   753     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
   754   by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv
   755       multiplicity_dvd_int multiplicity_nonprime_int nat_int transfer_nat_int_relations(4)
   756       less_le)
   757 
   758 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   759     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
   760   by (auto intro: dvd_multiplicity_nat multiplicity_dvd_nat)
   761 
   762 lemma dvd_multiplicity_eq_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow>
   763     (x dvd y) = (ALL p >= 0. multiplicity p x <= multiplicity p y)"
   764   by (auto intro: dvd_multiplicity_int multiplicity_dvd_int)
   765 
   766 lemma prime_factors_altdef2_nat: "(n::nat) > 0 \<Longrightarrow> 
   767     (p : prime_factors n) = (prime p & p dvd n)"
   768   apply (cases "prime p")
   769   apply auto
   770   apply (subst prime_factorization_nat [where n = n], assumption)
   771   apply (rule dvd_trans) 
   772   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   773   apply (subst (asm) prime_factors_altdef_nat, force)
   774   apply (rule dvd_setprod)
   775   apply auto
   776   apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
   777   done
   778 
   779 lemma prime_factors_altdef2_int: 
   780   assumes "(n::int) > 0" 
   781   shows "(p : prime_factors n) = (prime p & p dvd n)"
   782   apply (cases "p >= 0")
   783   apply (rule prime_factors_altdef2_nat [transferred])
   784   using assms apply auto
   785   apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
   786   done
   787 
   788 lemma multiplicity_eq_nat:
   789   fixes x and y::nat 
   790   assumes [arith]: "x > 0" "y > 0" and
   791     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   792   shows "x = y"
   793   apply (rule dvd_antisym)
   794   apply (auto intro: multiplicity_dvd'_nat) 
   795   done
   796 
   797 lemma multiplicity_eq_int:
   798   fixes x and y::int 
   799   assumes [arith]: "x > 0" "y > 0" and
   800     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   801   shows "x = y"
   802   apply (rule dvd_antisym [transferred])
   803   apply (auto intro: multiplicity_dvd'_int) 
   804   done
   805 
   806 
   807 subsection {* An application *}
   808 
   809 lemma gcd_eq_nat: 
   810   assumes pos [arith]: "x > 0" "y > 0"
   811   shows "gcd (x::nat) y = 
   812     (PROD p: prime_factors x Un prime_factors y. 
   813       p ^ (min (multiplicity p x) (multiplicity p y)))"
   814 proof -
   815   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   816       p ^ (min (multiplicity p x) (multiplicity p y)))"
   817   have [arith]: "z > 0"
   818     unfolding z_def by (rule setprod_pos_nat, auto)
   819   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   820       min (multiplicity p x) (multiplicity p y)"
   821     unfolding z_def
   822     apply (subst multiplicity_prod_prime_powers_nat)
   823     apply auto
   824     done
   825   have "z dvd x" 
   826     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   827   moreover have "z dvd y" 
   828     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   829   moreover have "ALL w. w dvd x & w dvd y \<longrightarrow> w dvd z"
   830     apply auto
   831     apply (case_tac "w = 0", auto)
   832     apply (erule multiplicity_dvd'_nat)
   833     apply (auto intro: dvd_multiplicity_nat simp add: aux)
   834     done
   835   ultimately have "z = gcd x y"
   836     by (subst gcd_unique_nat [symmetric], blast)
   837   then show ?thesis
   838     unfolding z_def by auto
   839 qed
   840 
   841 lemma lcm_eq_nat: 
   842   assumes pos [arith]: "x > 0" "y > 0"
   843   shows "lcm (x::nat) y = 
   844     (PROD p: prime_factors x Un prime_factors y. 
   845       p ^ (max (multiplicity p x) (multiplicity p y)))"
   846 proof -
   847   def z == "(PROD p: prime_factors (x::nat) Un prime_factors y. 
   848       p ^ (max (multiplicity p x) (multiplicity p y)))"
   849   have [arith]: "z > 0"
   850     unfolding z_def by (rule setprod_pos_nat, auto)
   851   have aux: "!!p. prime p \<Longrightarrow> multiplicity p z = 
   852       max (multiplicity p x) (multiplicity p y)"
   853     unfolding z_def
   854     apply (subst multiplicity_prod_prime_powers_nat)
   855     apply auto
   856     done
   857   have "x dvd z" 
   858     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   859   moreover have "y dvd z" 
   860     by (intro multiplicity_dvd'_nat, auto simp add: aux)
   861   moreover have "ALL w. x dvd w & y dvd w \<longrightarrow> z dvd w"
   862     apply auto
   863     apply (case_tac "w = 0", auto)
   864     apply (rule multiplicity_dvd'_nat)
   865     apply (auto intro: dvd_multiplicity_nat simp add: aux)
   866     done
   867   ultimately have "z = lcm x y"
   868     by (subst lcm_unique_nat [symmetric], blast)
   869   then show ?thesis
   870     unfolding z_def by auto
   871 qed
   872 
   873 lemma multiplicity_gcd_nat: 
   874   assumes [arith]: "x > 0" "y > 0"
   875   shows "multiplicity (p::nat) (gcd x y) = min (multiplicity p x) (multiplicity p y)"
   876   apply (subst gcd_eq_nat)
   877   apply auto
   878   apply (subst multiplicity_prod_prime_powers_nat)
   879   apply auto
   880   done
   881 
   882 lemma multiplicity_lcm_nat: 
   883   assumes [arith]: "x > 0" "y > 0"
   884   shows "multiplicity (p::nat) (lcm x y) = max (multiplicity p x) (multiplicity p y)"
   885   apply (subst lcm_eq_nat)
   886   apply auto
   887   apply (subst multiplicity_prod_prime_powers_nat)
   888   apply auto
   889   done
   890 
   891 lemma gcd_lcm_distrib_nat: "gcd (x::nat) (lcm y z) = lcm (gcd x y) (gcd x z)"
   892   apply (cases "x = 0 | y = 0 | z = 0") 
   893   apply auto
   894   apply (rule multiplicity_eq_nat)
   895   apply (auto simp add: multiplicity_gcd_nat multiplicity_lcm_nat lcm_pos_nat)
   896   done
   897 
   898 lemma gcd_lcm_distrib_int: "gcd (x::int) (lcm y z) = lcm (gcd x y) (gcd x z)"
   899   apply (subst (1 2 3) gcd_abs_int)
   900   apply (subst lcm_abs_int)
   901   apply (subst (2) abs_of_nonneg)
   902   apply force
   903   apply (rule gcd_lcm_distrib_nat [transferred])
   904   apply auto
   905   done
   906 
   907 end