src/HOL/Number_Theory/Factorial_Ring.thy
author nipkow
Mon Oct 17 11:46:22 2016 +0200 (2016-10-17)
changeset 64267 b9a1486e79be
parent 63924 f91766530e13
child 64272 f76b6dda2e56
permissions -rw-r--r--
setsum -> sum
     1 (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     2     Author:     Manuel Eberl, TU Muenchen
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 section \<open>Factorial (semi)rings\<close>
     7 
     8 theory Factorial_Ring
     9 imports 
    10   Main
    11   "~~/src/HOL/GCD"
    12   "~~/src/HOL/Library/Multiset"
    13 begin
    14 
    15 subsection \<open>Irreducible and prime elements\<close>
    16 
    17 context comm_semiring_1
    18 begin
    19 
    20 definition irreducible :: "'a \<Rightarrow> bool" where
    21   "irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)"
    22 
    23 lemma not_irreducible_zero [simp]: "\<not>irreducible 0"
    24   by (simp add: irreducible_def)
    25 
    26 lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1"
    27   by (simp add: irreducible_def)
    28 
    29 lemma not_irreducible_one [simp]: "\<not>irreducible 1"
    30   by (simp add: irreducible_def)
    31 
    32 lemma irreducibleI:
    33   "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p"
    34   by (simp add: irreducible_def)
    35 
    36 lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
    37   by (simp add: irreducible_def)
    38 
    39 definition prime_elem :: "'a \<Rightarrow> bool" where
    40   "prime_elem p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p dvd (a * b) \<longrightarrow> p dvd a \<or> p dvd b)"
    41 
    42 lemma not_prime_elem_zero [simp]: "\<not>prime_elem 0"
    43   by (simp add: prime_elem_def)
    44 
    45 lemma prime_elem_not_unit: "prime_elem p \<Longrightarrow> \<not>p dvd 1"
    46   by (simp add: prime_elem_def)
    47 
    48 lemma prime_elemI:
    49     "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> prime_elem p"
    50   by (simp add: prime_elem_def)
    51 
    52 lemma prime_elem_dvd_multD:
    53     "prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
    54   by (simp add: prime_elem_def)
    55 
    56 lemma prime_elem_dvd_mult_iff:
    57   "prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
    58   by (auto simp: prime_elem_def)
    59 
    60 lemma not_prime_elem_one [simp]:
    61   "\<not> prime_elem 1"
    62   by (auto dest: prime_elem_not_unit)
    63 
    64 lemma prime_elem_not_zeroI:
    65   assumes "prime_elem p"
    66   shows "p \<noteq> 0"
    67   using assms by (auto intro: ccontr)
    68 
    69 lemma prime_elem_dvd_power: 
    70   "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
    71   by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
    72 
    73 lemma prime_elem_dvd_power_iff:
    74   "prime_elem p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
    75   by (auto dest: prime_elem_dvd_power intro: dvd_trans)
    76 
    77 lemma prime_elem_imp_nonzero [simp]:
    78   "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 0"
    79   unfolding ASSUMPTION_def by (rule prime_elem_not_zeroI)
    80 
    81 lemma prime_elem_imp_not_one [simp]:
    82   "ASSUMPTION (prime_elem x) \<Longrightarrow> x \<noteq> 1"
    83   unfolding ASSUMPTION_def by auto
    84 
    85 end
    86 
    87 context algebraic_semidom
    88 begin
    89 
    90 lemma prime_elem_imp_irreducible:
    91   assumes "prime_elem p"
    92   shows   "irreducible p"
    93 proof (rule irreducibleI)
    94   fix a b
    95   assume p_eq: "p = a * b"
    96   with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
    97   from p_eq have "p dvd a * b" by simp
    98   with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
    99   with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
   100   thus "a dvd 1 \<or> b dvd 1"
   101     by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
   102 qed (insert assms, simp_all add: prime_elem_def)
   103 
   104 lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors:
   105   assumes "is_unit x" "irreducible p"
   106   shows   "\<not>p dvd x"
   107 proof (rule notI)
   108   assume "p dvd x"
   109   with \<open>is_unit x\<close> have "is_unit p"
   110     by (auto intro: dvd_trans)
   111   with \<open>irreducible p\<close> show False
   112     by (simp add: irreducible_not_unit)
   113 qed
   114    
   115 lemma unit_imp_no_prime_divisors:
   116   assumes "is_unit x" "prime_elem p"
   117   shows   "\<not>p dvd x"
   118   using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
   119 
   120 lemma prime_elem_mono:
   121   assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
   122   shows   "prime_elem q"
   123 proof -
   124   from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
   125   hence "p dvd q * r" by simp
   126   with \<open>prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_elem_dvd_multD)
   127   hence "p dvd q"
   128   proof
   129     assume "p dvd r"
   130     then obtain s where s: "r = p * s" by (elim dvdE)
   131     from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
   132     with \<open>prime_elem p\<close> have "q dvd 1"
   133       by (subst (asm) mult_cancel_left) auto
   134     with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
   135   qed
   136 
   137   show ?thesis
   138   proof (rule prime_elemI)
   139     fix a b assume "q dvd (a * b)"
   140     with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
   141     with \<open>prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_elem_dvd_multD)
   142     with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
   143   qed (insert assms, auto)
   144 qed
   145 
   146 lemma irreducibleD':
   147   assumes "irreducible a" "b dvd a"
   148   shows   "a dvd b \<or> is_unit b"
   149 proof -
   150   from assms obtain c where c: "a = b * c" by (elim dvdE)
   151   from irreducibleD[OF assms(1) this] have "is_unit b \<or> is_unit c" .
   152   thus ?thesis by (auto simp: c mult_unit_dvd_iff)
   153 qed
   154 
   155 lemma irreducibleI':
   156   assumes "a \<noteq> 0" "\<not>is_unit a" "\<And>b. b dvd a \<Longrightarrow> a dvd b \<or> is_unit b"
   157   shows   "irreducible a"
   158 proof (rule irreducibleI)
   159   fix b c assume a_eq: "a = b * c"
   160   hence "a dvd b \<or> is_unit b" by (intro assms) simp_all
   161   thus "is_unit b \<or> is_unit c"
   162   proof
   163     assume "a dvd b"
   164     hence "b * c dvd b * 1" by (simp add: a_eq)
   165     moreover from \<open>a \<noteq> 0\<close> a_eq have "b \<noteq> 0" by auto
   166     ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto
   167   qed blast
   168 qed (simp_all add: assms(1,2))
   169 
   170 lemma irreducible_altdef:
   171   "irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)"
   172   using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
   173 
   174 lemma prime_elem_multD:
   175   assumes "prime_elem (a * b)"
   176   shows "is_unit a \<or> is_unit b"
   177 proof -
   178   from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: prime_elem_not_zeroI)
   179   moreover from assms prime_elem_dvd_multD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
   180     by auto
   181   ultimately show ?thesis
   182     using dvd_times_left_cancel_iff [of a b 1]
   183       dvd_times_right_cancel_iff [of b a 1]
   184     by auto
   185 qed
   186 
   187 lemma prime_elemD2:
   188   assumes "prime_elem p" and "a dvd p" and "\<not> is_unit a"
   189   shows "p dvd a"
   190 proof -
   191   from \<open>a dvd p\<close> obtain b where "p = a * b" ..
   192   with \<open>prime_elem p\<close> prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
   193   with \<open>p = a * b\<close> show ?thesis
   194     by (auto simp add: mult_unit_dvd_iff)
   195 qed
   196 
   197 lemma prime_elem_dvd_prod_msetE:
   198   assumes "prime_elem p"
   199   assumes dvd: "p dvd prod_mset A"
   200   obtains a where "a \<in># A" and "p dvd a"
   201 proof -
   202   from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   203   proof (induct A)
   204     case empty then show ?case
   205     using \<open>prime_elem p\<close> by (simp add: prime_elem_not_unit)
   206   next
   207     case (add a A)
   208     then have "p dvd a * prod_mset A" by simp
   209     with \<open>prime_elem p\<close> consider (A) "p dvd prod_mset A" | (B) "p dvd a"
   210       by (blast dest: prime_elem_dvd_multD)
   211     then show ?case proof cases
   212       case B then show ?thesis by auto
   213     next
   214       case A
   215       with add.hyps obtain b where "b \<in># A" "p dvd b"
   216         by auto
   217       then show ?thesis by auto
   218     qed
   219   qed
   220   with that show thesis by blast
   221 qed
   222 
   223 context
   224 begin
   225 
   226 private lemma prime_elem_powerD:
   227   assumes "prime_elem (p ^ n)"
   228   shows   "prime_elem p \<and> n = 1"
   229 proof (cases n)
   230   case (Suc m)
   231   note assms
   232   also from Suc have "p ^ n = p * p^m" by simp
   233   finally have "is_unit p \<or> is_unit (p^m)" by (rule prime_elem_multD)
   234   moreover from assms have "\<not>is_unit p" by (simp add: prime_elem_def is_unit_power_iff)
   235   ultimately have "is_unit (p ^ m)" by simp
   236   with \<open>\<not>is_unit p\<close> have "m = 0" by (simp add: is_unit_power_iff)
   237   with Suc assms show ?thesis by simp
   238 qed (insert assms, simp_all)
   239 
   240 lemma prime_elem_power_iff:
   241   "prime_elem (p ^ n) \<longleftrightarrow> prime_elem p \<and> n = 1"
   242   by (auto dest: prime_elem_powerD)
   243 
   244 end
   245 
   246 lemma irreducible_mult_unit_left:
   247   "is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
   248   by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
   249         mult_unit_dvd_iff dvd_mult_unit_iff)
   250 
   251 lemma prime_elem_mult_unit_left:
   252   "is_unit a \<Longrightarrow> prime_elem (a * p) \<longleftrightarrow> prime_elem p"
   253   by (auto simp: prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
   254 
   255 lemma prime_elem_dvd_cases:
   256   assumes pk: "p*k dvd m*n" and p: "prime_elem p"
   257   shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
   258 proof -
   259   have "p dvd m*n" using dvd_mult_left pk by blast
   260   then consider "p dvd m" | "p dvd n"
   261     using p prime_elem_dvd_mult_iff by blast
   262   then show ?thesis
   263   proof cases
   264     case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
   265       then have "\<exists>x. k dvd x * n \<and> m = p * x"
   266         using p pk by (auto simp: mult.assoc)
   267     then show ?thesis ..
   268   next
   269     case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
   270     with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
   271       by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
   272     then show ?thesis ..
   273   qed
   274 qed
   275 
   276 lemma prime_elem_power_dvd_prod:
   277   assumes pc: "p^c dvd m*n" and p: "prime_elem p"
   278   shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
   279 using pc
   280 proof (induct c arbitrary: m n)
   281   case 0 show ?case by simp
   282 next
   283   case (Suc c)
   284   consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
   285     using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
   286   then show ?case
   287   proof cases
   288     case (1 x) 
   289     with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
   290     with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
   291       by (auto intro: mult_dvd_mono)
   292     thus ?thesis by blast
   293   next
   294     case (2 y) 
   295     with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
   296     with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
   297       by (auto intro: mult_dvd_mono)
   298     with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
   299       by force
   300   qed
   301 qed
   302 
   303 lemma prime_elem_power_dvd_cases:
   304   assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p"
   305   shows "p ^ a dvd m \<or> p ^ b dvd n"
   306 proof -
   307   from assms obtain r s
   308     where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n"
   309     by (blast dest: prime_elem_power_dvd_prod)
   310   moreover with assms have
   311     "a \<le> r \<or> b \<le> s" by arith
   312   ultimately show ?thesis by (auto intro: power_le_dvd)
   313 qed
   314 
   315 lemma prime_elem_not_unit' [simp]:
   316   "ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
   317   unfolding ASSUMPTION_def by (rule prime_elem_not_unit)
   318 
   319 lemma prime_elem_dvd_power_iff:
   320   assumes "prime_elem p"
   321   shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
   322   using assms by (induct n) (auto dest: prime_elem_not_unit prime_elem_dvd_multD)
   323 
   324 lemma prime_power_dvd_multD:
   325   assumes "prime_elem p"
   326   assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   327   shows "p ^ n dvd b"
   328   using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> 
   329 proof (induct n arbitrary: b)
   330   case 0 then show ?case by simp
   331 next
   332   case (Suc n) show ?case
   333   proof (cases "n = 0")
   334     case True with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
   335       by (simp add: prime_elem_dvd_mult_iff)
   336   next
   337     case False then have "n > 0" by simp
   338     from \<open>prime_elem p\<close> have "p \<noteq> 0" by auto
   339     from Suc.prems have *: "p * p ^ n dvd a * b"
   340       by simp
   341     then have "p dvd a * b"
   342       by (rule dvd_mult_left)
   343     with Suc \<open>prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
   344       by (simp add: prime_elem_dvd_mult_iff)
   345     moreover define c where "c = b div p"
   346     ultimately have b: "b = p * c" by simp
   347     with * have "p * p ^ n dvd p * (a * c)"
   348       by (simp add: ac_simps)
   349     with \<open>p \<noteq> 0\<close> have "p ^ n dvd a * c"
   350       by simp
   351     with Suc.hyps \<open>n > 0\<close> have "p ^ n dvd c"
   352       by blast
   353     with \<open>p \<noteq> 0\<close> show ?thesis
   354       by (simp add: b)
   355   qed
   356 qed
   357 
   358 end
   359 
   360 
   361 subsection \<open>Generalized primes: normalized prime elements\<close>
   362 
   363 context normalization_semidom
   364 begin
   365 
   366 lemma irreducible_normalized_divisors:
   367   assumes "irreducible x" "y dvd x" "normalize y = y"
   368   shows   "y = 1 \<or> y = normalize x"
   369 proof -
   370   from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
   371   thus ?thesis
   372   proof (elim disjE)
   373     assume "is_unit y"
   374     hence "normalize y = 1" by (simp add: is_unit_normalize)
   375     with assms show ?thesis by simp
   376   next
   377     assume "x dvd y"
   378     with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
   379     with assms show ?thesis by simp
   380   qed
   381 qed
   382 
   383 lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
   384   using irreducible_mult_unit_left[of "1 div unit_factor x" x]
   385   by (cases "x = 0") (simp_all add: unit_div_commute)
   386 
   387 lemma prime_elem_normalize_iff [simp]: "prime_elem (normalize x) = prime_elem x"
   388   using prime_elem_mult_unit_left[of "1 div unit_factor x" x]
   389   by (cases "x = 0") (simp_all add: unit_div_commute)
   390 
   391 lemma prime_elem_associated:
   392   assumes "prime_elem p" and "prime_elem q" and "q dvd p"
   393   shows "normalize q = normalize p"
   394 using \<open>q dvd p\<close> proof (rule associatedI)
   395   from \<open>prime_elem q\<close> have "\<not> is_unit q"
   396     by (auto simp add: prime_elem_not_unit)
   397   with \<open>prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
   398     by (blast intro: prime_elemD2)
   399 qed
   400 
   401 definition prime :: "'a \<Rightarrow> bool" where
   402   "prime p \<longleftrightarrow> prime_elem p \<and> normalize p = p"
   403 
   404 lemma not_prime_0 [simp]: "\<not>prime 0" by (simp add: prime_def)
   405 
   406 lemma not_prime_unit: "is_unit x \<Longrightarrow> \<not>prime x"
   407   using prime_elem_not_unit[of x] by (auto simp add: prime_def)
   408 
   409 lemma not_prime_1 [simp]: "\<not>prime 1" by (simp add: not_prime_unit)
   410 
   411 lemma primeI: "prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> prime x"
   412   by (simp add: prime_def)
   413 
   414 lemma prime_imp_prime_elem [dest]: "prime p \<Longrightarrow> prime_elem p"
   415   by (simp add: prime_def)
   416 
   417 lemma normalize_prime: "prime p \<Longrightarrow> normalize p = p"
   418   by (simp add: prime_def)
   419 
   420 lemma prime_normalize_iff [simp]: "prime (normalize p) \<longleftrightarrow> prime_elem p"
   421   by (auto simp add: prime_def)
   422 
   423 lemma prime_power_iff:
   424   "prime (p ^ n) \<longleftrightarrow> prime p \<and> n = 1"
   425   by (auto simp: prime_def prime_elem_power_iff)
   426 
   427 lemma prime_imp_nonzero [simp]:
   428   "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 0"
   429   unfolding ASSUMPTION_def prime_def by auto
   430 
   431 lemma prime_imp_not_one [simp]:
   432   "ASSUMPTION (prime x) \<Longrightarrow> x \<noteq> 1"
   433   unfolding ASSUMPTION_def by auto
   434 
   435 lemma prime_not_unit' [simp]:
   436   "ASSUMPTION (prime x) \<Longrightarrow> \<not>is_unit x"
   437   unfolding ASSUMPTION_def prime_def by auto
   438 
   439 lemma prime_normalize' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> normalize x = x"
   440   unfolding ASSUMPTION_def prime_def by simp
   441 
   442 lemma unit_factor_prime: "prime x \<Longrightarrow> unit_factor x = 1"
   443   using unit_factor_normalize[of x] unfolding prime_def by auto
   444 
   445 lemma unit_factor_prime' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> unit_factor x = 1"
   446   unfolding ASSUMPTION_def by (rule unit_factor_prime)
   447 
   448 lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (prime x) \<Longrightarrow> prime_elem x"
   449   by (simp add: prime_def ASSUMPTION_def)
   450 
   451 lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
   452   by (intro prime_elem_dvd_multD) simp_all
   453 
   454 lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   455   by (auto dest: prime_dvd_multD)
   456 
   457 lemma prime_dvd_power: 
   458   "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   459   by (auto dest!: prime_elem_dvd_power simp: prime_def)
   460 
   461 lemma prime_dvd_power_iff:
   462   "prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
   463   by (subst prime_elem_dvd_power_iff) simp_all
   464 
   465 lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
   466   by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)
   467 
   468 lemma primes_dvd_imp_eq:
   469   assumes "prime p" "prime q" "p dvd q"
   470   shows   "p = q"
   471 proof -
   472   from assms have "irreducible q" by (simp add: prime_elem_imp_irreducible prime_def)
   473   from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
   474   with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
   475   with assms show "p = q" by simp
   476 qed
   477 
   478 lemma prime_dvd_prod_mset_primes_iff:
   479   assumes "prime p" "\<And>q. q \<in># A \<Longrightarrow> prime q"
   480   shows   "p dvd prod_mset A \<longleftrightarrow> p \<in># A"
   481 proof -
   482   from assms(1) have "p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_prod_mset_iff)
   483   also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
   484   finally show ?thesis .
   485 qed
   486 
   487 lemma prod_mset_primes_dvd_imp_subset:
   488   assumes "prod_mset A dvd prod_mset B" "\<And>p. p \<in># A \<Longrightarrow> prime p" "\<And>p. p \<in># B \<Longrightarrow> prime p"
   489   shows   "A \<subseteq># B"
   490 using assms
   491 proof (induction A arbitrary: B)
   492   case empty
   493   thus ?case by simp
   494 next
   495   case (add p A B)
   496   hence p: "prime p" by simp
   497   define B' where "B' = B - {#p#}"
   498   from add.prems have "p dvd prod_mset B" by (simp add: dvd_mult_left)
   499   with add.prems have "p \<in># B"
   500     by (subst (asm) (2) prime_dvd_prod_mset_primes_iff) simp_all
   501   hence B: "B = B' + {#p#}" by (simp add: B'_def)
   502   from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
   503   thus ?case by (simp add: B)
   504 qed
   505 
   506 lemma normalize_prod_mset_primes:
   507   "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
   508 proof (induction A)
   509   case (add p A)
   510   hence "prime p" by simp
   511   hence "normalize p = p" by simp
   512   with add show ?case by (simp add: normalize_mult)
   513 qed simp_all
   514 
   515 lemma prod_mset_dvd_prod_mset_primes_iff:
   516   assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
   517   shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
   518   using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)
   519 
   520 lemma is_unit_prod_mset_primes_iff:
   521   assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
   522   shows   "is_unit (prod_mset A) \<longleftrightarrow> A = {#}"
   523   by (auto simp add: is_unit_prod_mset_iff)
   524     (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff)
   525 
   526 lemma prod_mset_primes_irreducible_imp_prime:
   527   assumes irred: "irreducible (prod_mset A)"
   528   assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   529   assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   530   assumes C: "\<And>x. x \<in># C \<Longrightarrow> prime x"
   531   assumes dvd: "prod_mset A dvd prod_mset B * prod_mset C"
   532   shows   "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C"
   533 proof -
   534   from dvd have "prod_mset A dvd prod_mset (B + C)"
   535     by simp
   536   with A B C have subset: "A \<subseteq># B + C"
   537     by (subst (asm) prod_mset_dvd_prod_mset_primes_iff) auto
   538   define A1 and A2 where "A1 = A \<inter># B" and "A2 = A - A1"
   539   have "A = A1 + A2" unfolding A1_def A2_def
   540     by (rule sym, intro subset_mset.add_diff_inverse) simp_all
   541   from subset have "A1 \<subseteq># B" "A2 \<subseteq># C"
   542     by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute)
   543   from \<open>A = A1 + A2\<close> have "prod_mset A = prod_mset A1 * prod_mset A2" by simp
   544   from irred and this have "is_unit (prod_mset A1) \<or> is_unit (prod_mset A2)"
   545     by (rule irreducibleD)
   546   with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def
   547     by (subst (asm) (1 2) is_unit_prod_mset_primes_iff) (auto dest: Multiset.in_diffD)
   548   with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis
   549     by (auto intro: prod_mset_subset_imp_dvd)
   550 qed
   551 
   552 lemma prod_mset_primes_finite_divisor_powers:
   553   assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
   554   assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
   555   assumes "A \<noteq> {#}"
   556   shows   "finite {n. prod_mset A ^ n dvd prod_mset B}"
   557 proof -
   558   from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast
   559   define m where "m = count B x"
   560   have "{n. prod_mset A ^ n dvd prod_mset B} \<subseteq> {..m}"
   561   proof safe
   562     fix n assume dvd: "prod_mset A ^ n dvd prod_mset B"
   563     from x have "x ^ n dvd prod_mset A ^ n" by (intro dvd_power_same dvd_prod_mset)
   564     also note dvd
   565     also have "x ^ n = prod_mset (replicate_mset n x)" by simp
   566     finally have "replicate_mset n x \<subseteq># B"
   567       by (rule prod_mset_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
   568     thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def)
   569   qed
   570   moreover have "finite {..m}" by simp
   571   ultimately show ?thesis by (rule finite_subset)
   572 qed
   573 
   574 end
   575 
   576 
   577 subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
   578 
   579 context semiring_gcd
   580 begin
   581 
   582 lemma irreducible_imp_prime_elem_gcd:
   583   assumes "irreducible x"
   584   shows   "prime_elem x"
   585 proof (rule prime_elemI)
   586   fix a b assume "x dvd a * b"
   587   from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
   588   from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
   589   with yz show "x dvd a \<or> x dvd b"
   590     by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
   591 qed (insert assms, auto simp: irreducible_not_unit)
   592 
   593 lemma prime_elem_imp_coprime:
   594   assumes "prime_elem p" "\<not>p dvd n"
   595   shows   "coprime p n"
   596 proof (rule coprimeI)
   597   fix d assume "d dvd p" "d dvd n"
   598   show "is_unit d"
   599   proof (rule ccontr)
   600     assume "\<not>is_unit d"
   601     from \<open>prime_elem p\<close> and \<open>d dvd p\<close> and this have "p dvd d"
   602       by (rule prime_elemD2)
   603     from this and \<open>d dvd n\<close> have "p dvd n" by (rule dvd_trans)
   604     with \<open>\<not>p dvd n\<close> show False by contradiction
   605   qed
   606 qed
   607 
   608 lemma prime_imp_coprime:
   609   assumes "prime p" "\<not>p dvd n"
   610   shows   "coprime p n"
   611   using assms by (simp add: prime_elem_imp_coprime)
   612 
   613 lemma prime_elem_imp_power_coprime: 
   614   "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   615   by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
   616 
   617 lemma prime_imp_power_coprime: 
   618   "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   619   by (simp add: prime_elem_imp_power_coprime)
   620 
   621 lemma prime_elem_divprod_pow:
   622   assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   623   shows   "p^n dvd a \<or> p^n dvd b"
   624   using assms
   625 proof -
   626   from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
   627     by (auto simp: coprime prime_elem_def)
   628   with p have "coprime (p^n) a \<or> coprime (p^n) b" 
   629     by (auto intro: prime_elem_imp_coprime coprime_exp_left)
   630   with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
   631 qed
   632 
   633 lemma primes_coprime: 
   634   "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   635   using prime_imp_coprime primes_dvd_imp_eq by blast
   636 
   637 end
   638 
   639 
   640 subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close>
   641 
   642 class factorial_semiring = normalization_semidom +
   643   assumes prime_factorization_exists:
   644     "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   645 
   646 text \<open>Alternative characterization\<close>
   647   
   648 lemma (in normalization_semidom) factorial_semiring_altI_aux:
   649   assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   650   assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
   651   assumes "x \<noteq> 0"
   652   shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
   653 using \<open>x \<noteq> 0\<close>
   654 proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
   655   case (less a)
   656   let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
   657   show ?case
   658   proof (cases "is_unit a")
   659     case True
   660     thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
   661   next
   662     case False
   663     show ?thesis
   664     proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
   665       case False
   666       with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
   667       hence "prime_elem a" by (rule irreducible_imp_prime_elem)
   668       thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
   669     next
   670       case True
   671       then guess b by (elim exE conjE) note b = this
   672 
   673       from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
   674       moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
   675       hence "?fctrs b \<noteq> ?fctrs a" by blast
   676       ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
   677       with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
   678         by (rule psubset_card_mono)
   679       moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
   680       ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
   681         by (intro less) auto
   682       then guess A .. note A = this
   683 
   684       define c where "c = a div b"
   685       from b have c: "a = b * c" by (simp add: c_def)
   686       from less.prems c have "c \<noteq> 0" by auto
   687       from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
   688       moreover have "normalize a \<notin> ?fctrs c"
   689       proof safe
   690         assume "normalize a dvd c"
   691         hence "b * c dvd 1 * c" by (simp add: c)
   692         hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
   693         with b show False by simp
   694       qed
   695       with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
   696       ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
   697       with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
   698         by (rule psubset_card_mono)
   699       with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
   700         by (intro less) auto
   701       then guess B .. note B = this
   702 
   703       from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
   704     qed
   705   qed
   706 qed 
   707 
   708 lemma factorial_semiring_altI:
   709   assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   710   assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
   711   shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
   712   by intro_classes (rule factorial_semiring_altI_aux[OF assms])
   713   
   714 text \<open>Properties\<close>
   715 
   716 context factorial_semiring
   717 begin
   718 
   719 lemma prime_factorization_exists':
   720   assumes "x \<noteq> 0"
   721   obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x"
   722 proof -
   723   from prime_factorization_exists[OF assms] obtain A
   724     where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast
   725   define A' where "A' = image_mset normalize A"
   726   have "prod_mset A' = normalize (prod_mset A)"
   727     by (simp add: A'_def normalize_prod_mset)
   728   also note A(2)
   729   finally have "prod_mset A' = normalize x" by simp
   730   moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
   731   ultimately show ?thesis by (intro that[of A']) blast
   732 qed
   733 
   734 lemma irreducible_imp_prime_elem:
   735   assumes "irreducible x"
   736   shows   "prime_elem x"
   737 proof (rule prime_elemI)
   738   fix a b assume dvd: "x dvd a * b"
   739   from assms have "x \<noteq> 0" by auto
   740   show "x dvd a \<or> x dvd b"
   741   proof (cases "a = 0 \<or> b = 0")
   742     case False
   743     hence "a \<noteq> 0" "b \<noteq> 0" by blast+
   744     note nz = \<open>x \<noteq> 0\<close> this
   745     from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
   746     from assms ABC have "irreducible (prod_mset A)" by simp
   747     from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
   748       show ?thesis by (simp add: normalize_mult [symmetric])
   749   qed auto
   750 qed (insert assms, simp_all add: irreducible_def)
   751 
   752 lemma finite_divisor_powers:
   753   assumes "y \<noteq> 0" "\<not>is_unit x"
   754   shows   "finite {n. x ^ n dvd y}"
   755 proof (cases "x = 0")
   756   case True
   757   with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left)
   758   thus ?thesis by simp
   759 next
   760   case False
   761   note nz = this \<open>y \<noteq> 0\<close>
   762   from nz[THEN prime_factorization_exists'] guess A B . note AB = this
   763   from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
   764   from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
   765     show ?thesis by (simp add: normalize_power [symmetric])
   766 qed
   767 
   768 lemma finite_prime_divisors:
   769   assumes "x \<noteq> 0"
   770   shows   "finite {p. prime p \<and> p dvd x}"
   771 proof -
   772   from prime_factorization_exists'[OF assms] guess A . note A = this
   773   have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
   774   proof safe
   775     fix p assume p: "prime p" and dvd: "p dvd x"
   776     from dvd have "p dvd normalize x" by simp
   777     also from A have "normalize x = prod_mset A" by simp
   778     finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff)
   779   qed
   780   moreover have "finite (set_mset A)" by simp
   781   ultimately show ?thesis by (rule finite_subset)
   782 qed
   783 
   784 lemma prime_elem_iff_irreducible: "prime_elem x \<longleftrightarrow> irreducible x"
   785   by (blast intro: irreducible_imp_prime_elem prime_elem_imp_irreducible)
   786 
   787 lemma prime_divisor_exists:
   788   assumes "a \<noteq> 0" "\<not>is_unit a"
   789   shows   "\<exists>b. b dvd a \<and> prime b"
   790 proof -
   791   from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   792   moreover from A and assms have "A \<noteq> {#}" by auto
   793   then obtain x where "x \<in># A" by blast
   794   with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset)
   795   with A have "x dvd a" by simp
   796   with * show ?thesis by blast
   797 qed
   798 
   799 lemma prime_divisors_induct [case_names zero unit factor]:
   800   assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
   801   shows   "P x"
   802 proof (cases "x = 0")
   803   case False
   804   from prime_factorization_exists'[OF this] guess A . note A = this
   805   from A(1) have "P (unit_factor x * prod_mset A)"
   806   proof (induction A)
   807     case (add p A)
   808     from add.prems have "prime p" by simp
   809     moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all
   810     ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3))
   811     thus ?case by (simp add: mult_ac)
   812   qed (simp_all add: assms False)
   813   with A show ?thesis by simp
   814 qed (simp_all add: assms(1))
   815 
   816 lemma no_prime_divisors_imp_unit:
   817   assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> prime_elem b"
   818   shows "is_unit a"
   819 proof (rule ccontr)
   820   assume "\<not>is_unit a"
   821   from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
   822   with assms(2)[of b] show False by (simp add: prime_def)
   823 qed
   824 
   825 lemma prime_divisorE:
   826   assumes "a \<noteq> 0" and "\<not> is_unit a"
   827   obtains p where "prime p" and "p dvd a"
   828   using assms no_prime_divisors_imp_unit unfolding prime_def by blast
   829 
   830 definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
   831   "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
   832 
   833 lemma multiplicity_dvd: "p ^ multiplicity p x dvd x"
   834 proof (cases "finite {n. p ^ n dvd x}")
   835   case True
   836   hence "multiplicity p x = Max {n. p ^ n dvd x}"
   837     by (simp add: multiplicity_def)
   838   also have "\<dots> \<in> {n. p ^ n dvd x}"
   839     by (rule Max_in) (auto intro!: True exI[of _ "0::nat"])
   840   finally show ?thesis by simp
   841 qed (simp add: multiplicity_def)
   842 
   843 lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x"
   844   by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])
   845 
   846 context
   847   fixes x p :: 'a
   848   assumes xp: "x \<noteq> 0" "\<not>is_unit p"
   849 begin
   850 
   851 lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}"
   852   using finite_divisor_powers[OF xp] by (simp add: multiplicity_def)
   853 
   854 lemma multiplicity_geI:
   855   assumes "p ^ n dvd x"
   856   shows   "multiplicity p x \<ge> n"
   857 proof -
   858   from assms have "n \<le> Max {n. p ^ n dvd x}"
   859     by (intro Max_ge finite_divisor_powers xp) simp_all
   860   thus ?thesis by (subst multiplicity_eq_Max)
   861 qed
   862 
   863 lemma multiplicity_lessI:
   864   assumes "\<not>p ^ n dvd x"
   865   shows   "multiplicity p x < n"
   866 proof (rule ccontr)
   867   assume "\<not>(n > multiplicity p x)"
   868   hence "p ^ n dvd x" by (intro multiplicity_dvd') simp
   869   with assms show False by contradiction
   870 qed
   871 
   872 lemma power_dvd_iff_le_multiplicity:
   873   "p ^ n dvd x \<longleftrightarrow> n \<le> multiplicity p x"
   874   using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
   875 
   876 lemma multiplicity_eq_zero_iff:
   877   shows   "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   878   using power_dvd_iff_le_multiplicity[of 1] by auto
   879 
   880 lemma multiplicity_gt_zero_iff:
   881   shows   "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   882   using power_dvd_iff_le_multiplicity[of 1] by auto
   883 
   884 lemma multiplicity_decompose:
   885   "\<not>p dvd (x div p ^ multiplicity p x)"
   886 proof
   887   assume *: "p dvd x div p ^ multiplicity p x"
   888   have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)"
   889     using multiplicity_dvd[of p x] by simp
   890   also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp
   891   also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x =
   892                x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)"
   893     by (simp add: mult_assoc)
   894   also have "p ^ Suc (multiplicity p x) dvd \<dots>" by (rule dvd_triv_right)
   895   finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp
   896 qed
   897 
   898 lemma multiplicity_decompose':
   899   obtains y where "x = p ^ multiplicity p x * y" "\<not>p dvd y"
   900   using that[of "x div p ^ multiplicity p x"]
   901   by (simp add: multiplicity_decompose multiplicity_dvd)
   902 
   903 end
   904 
   905 lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
   906   by (simp add: multiplicity_def)
   907 
   908 lemma prime_elem_multiplicity_eq_zero_iff:
   909   "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
   910   by (rule multiplicity_eq_zero_iff) simp_all
   911 
   912 lemma prime_multiplicity_other:
   913   assumes "prime p" "prime q" "p \<noteq> q"
   914   shows   "multiplicity p q = 0"
   915   using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
   916 
   917 lemma prime_multiplicity_gt_zero_iff:
   918   "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
   919   by (rule multiplicity_gt_zero_iff) simp_all
   920 
   921 lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
   922   by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
   923 
   924 lemma multiplicity_unit_right:
   925   assumes "is_unit x"
   926   shows   "multiplicity p x = 0"
   927 proof (cases "is_unit p \<or> x = 0")
   928   case False
   929   with multiplicity_lessI[of x p 1] this assms
   930     show ?thesis by (auto dest: dvd_unit_imp_unit)
   931 qed (auto simp: multiplicity_unit_left)
   932 
   933 lemma multiplicity_one [simp]: "multiplicity p 1 = 0"
   934   by (rule multiplicity_unit_right) simp_all
   935 
   936 lemma multiplicity_eqI:
   937   assumes "p ^ n dvd x" "\<not>p ^ Suc n dvd x"
   938   shows   "multiplicity p x = n"
   939 proof -
   940   consider "x = 0" | "is_unit p" | "x \<noteq> 0" "\<not>is_unit p" by blast
   941   thus ?thesis
   942   proof cases
   943     assume xp: "x \<noteq> 0" "\<not>is_unit p"
   944     from xp assms(1) have "multiplicity p x \<ge> n" by (intro multiplicity_geI)
   945     moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI)
   946     ultimately show ?thesis by simp
   947   next
   948     assume "is_unit p"
   949     hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc)
   950     hence "p ^ Suc n dvd x" by (rule unit_imp_dvd)
   951     with \<open>\<not>p ^ Suc n dvd x\<close> show ?thesis by contradiction
   952   qed (insert assms, simp_all)
   953 qed
   954 
   955 
   956 context
   957   fixes x p :: 'a
   958   assumes xp: "x \<noteq> 0" "\<not>is_unit p"
   959 begin
   960 
   961 lemma multiplicity_times_same:
   962   assumes "p \<noteq> 0"
   963   shows   "multiplicity p (p * x) = Suc (multiplicity p x)"
   964 proof (rule multiplicity_eqI)
   965   show "p ^ Suc (multiplicity p x) dvd p * x"
   966     by (auto intro!: mult_dvd_mono multiplicity_dvd)
   967   from xp assms show "\<not> p ^ Suc (Suc (multiplicity p x)) dvd p * x"
   968     using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp
   969 qed
   970 
   971 end
   972 
   973 lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \<or> is_unit p then 0 else n)"
   974 proof -
   975   consider "p = 0" | "is_unit p" |"p \<noteq> 0" "\<not>is_unit p" by blast
   976   thus ?thesis
   977   proof cases
   978     assume "p \<noteq> 0" "\<not>is_unit p"
   979     thus ?thesis by (induction n) (simp_all add: multiplicity_times_same)
   980   qed (simp_all add: power_0_left multiplicity_unit_left)
   981 qed
   982 
   983 lemma multiplicity_same_power:
   984   "p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
   985   by (simp add: multiplicity_same_power')
   986 
   987 lemma multiplicity_prime_elem_times_other:
   988   assumes "prime_elem p" "\<not>p dvd q"
   989   shows   "multiplicity p (q * x) = multiplicity p x"
   990 proof (cases "x = 0")
   991   case False
   992   show ?thesis
   993   proof (rule multiplicity_eqI)
   994     have "1 * p ^ multiplicity p x dvd q * x"
   995       by (intro mult_dvd_mono multiplicity_dvd) simp_all
   996     thus "p ^ multiplicity p x dvd q * x" by simp
   997   next
   998     define n where "n = multiplicity p x"
   999     from assms have "\<not>is_unit p" by simp
  1000     from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
  1001     from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
  1002     also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
  1003     also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
  1004     also from assms y have "\<dots> \<longleftrightarrow> False" by simp
  1005     finally show "\<not>(p ^ Suc n dvd q * x)" by blast
  1006   qed
  1007 qed simp_all
  1008 
  1009 lemma multiplicity_self:
  1010   assumes "p \<noteq> 0" "\<not>is_unit p"
  1011   shows   "multiplicity p p = 1"
  1012 proof -
  1013   from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
  1014     by (simp add: multiplicity_eq_Max)
  1015   also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
  1016     using dvd_power_iff[of p n 1] by auto
  1017   hence "{n. p ^ n dvd p} = {..1}" by auto
  1018   also have "\<dots> = {0,1}" by auto
  1019   finally show ?thesis by simp
  1020 qed
  1021 
  1022 lemma multiplicity_times_unit_left:
  1023   assumes "is_unit c"
  1024   shows   "multiplicity (c * p) x = multiplicity p x"
  1025 proof -
  1026   from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
  1027     by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
  1028   thus ?thesis by (simp add: multiplicity_def)
  1029 qed
  1030 
  1031 lemma multiplicity_times_unit_right:
  1032   assumes "is_unit c"
  1033   shows   "multiplicity p (c * x) = multiplicity p x"
  1034 proof -
  1035   from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
  1036     by (subst mult.commute) (simp add: dvd_mult_unit_iff)
  1037   thus ?thesis by (simp add: multiplicity_def)
  1038 qed
  1039 
  1040 lemma multiplicity_normalize_left [simp]:
  1041   "multiplicity (normalize p) x = multiplicity p x"
  1042 proof (cases "p = 0")
  1043   case [simp]: False
  1044   have "normalize p = (1 div unit_factor p) * p"
  1045     by (simp add: unit_div_commute is_unit_unit_factor)
  1046   also have "multiplicity \<dots> x = multiplicity p x"
  1047     by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
  1048   finally show ?thesis .
  1049 qed simp_all
  1050 
  1051 lemma multiplicity_normalize_right [simp]:
  1052   "multiplicity p (normalize x) = multiplicity p x"
  1053 proof (cases "x = 0")
  1054   case [simp]: False
  1055   have "normalize x = (1 div unit_factor x) * x"
  1056     by (simp add: unit_div_commute is_unit_unit_factor)
  1057   also have "multiplicity p \<dots> = multiplicity p x"
  1058     by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
  1059   finally show ?thesis .
  1060 qed simp_all   
  1061 
  1062 lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
  1063   by (rule multiplicity_self) auto
  1064 
  1065 lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
  1066   by (subst multiplicity_same_power') auto
  1067 
  1068 lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
  1069   "\<lambda>x p. if prime p then multiplicity p x else 0"
  1070   unfolding multiset_def
  1071 proof clarify
  1072   fix x :: 'a
  1073   show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
  1074   proof (cases "x = 0")
  1075     case False
  1076     from False have "?A \<subseteq> {p. prime p \<and> p dvd x}"
  1077       by (auto simp: multiplicity_gt_zero_iff)
  1078     moreover from False have "finite {p. prime p \<and> p dvd x}"
  1079       by (rule finite_prime_divisors)
  1080     ultimately show ?thesis by (rule finite_subset)
  1081   qed simp_all
  1082 qed
  1083 
  1084 abbreviation prime_factors :: "'a \<Rightarrow> 'a set" where
  1085   "prime_factors a \<equiv> set_mset (prime_factorization a)"
  1086 
  1087 lemma count_prime_factorization_nonprime:
  1088   "\<not>prime p \<Longrightarrow> count (prime_factorization x) p = 0"
  1089   by transfer simp
  1090 
  1091 lemma count_prime_factorization_prime:
  1092   "prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
  1093   by transfer simp
  1094 
  1095 lemma count_prime_factorization:
  1096   "count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
  1097   by transfer simp
  1098 
  1099 lemma dvd_imp_multiplicity_le:
  1100   assumes "a dvd b" "b \<noteq> 0"
  1101   shows   "multiplicity p a \<le> multiplicity p b"
  1102 proof (cases "is_unit p")
  1103   case False
  1104   with assms show ?thesis
  1105     by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
  1106 qed (insert assms, auto simp: multiplicity_unit_left)
  1107 
  1108 lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
  1109   by (simp add: multiset_eq_iff count_prime_factorization)
  1110 
  1111 lemma prime_factorization_empty_iff:
  1112   "prime_factorization x = {#} \<longleftrightarrow> x = 0 \<or> is_unit x"
  1113 proof
  1114   assume *: "prime_factorization x = {#}"
  1115   {
  1116     assume x: "x \<noteq> 0" "\<not>is_unit x"
  1117     {
  1118       fix p assume p: "prime p"
  1119       have "count (prime_factorization x) p = 0" by (simp add: *)
  1120       also from p have "count (prime_factorization x) p = multiplicity p x"
  1121         by (rule count_prime_factorization_prime)
  1122       also from x p have "\<dots> = 0 \<longleftrightarrow> \<not>p dvd x" by (simp add: multiplicity_eq_zero_iff)
  1123       finally have "\<not>p dvd x" .
  1124     }
  1125     with prime_divisor_exists[OF x] have False by blast
  1126   }
  1127   thus "x = 0 \<or> is_unit x" by blast
  1128 next
  1129   assume "x = 0 \<or> is_unit x"
  1130   thus "prime_factorization x = {#}"
  1131   proof
  1132     assume x: "is_unit x"
  1133     {
  1134       fix p assume p: "prime p"
  1135       from p x have "multiplicity p x = 0"
  1136         by (subst multiplicity_eq_zero_iff)
  1137            (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
  1138     }
  1139     thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization)
  1140   qed simp_all
  1141 qed
  1142 
  1143 lemma prime_factorization_unit:
  1144   assumes "is_unit x"
  1145   shows   "prime_factorization x = {#}"
  1146 proof (rule multiset_eqI)
  1147   fix p :: 'a
  1148   show "count (prime_factorization x) p = count {#} p"
  1149   proof (cases "prime p")
  1150     case True
  1151     with assms have "multiplicity p x = 0"
  1152       by (subst multiplicity_eq_zero_iff)
  1153          (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
  1154     with True show ?thesis by (simp add: count_prime_factorization_prime)
  1155   qed (simp_all add: count_prime_factorization_nonprime)
  1156 qed
  1157 
  1158 lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}"
  1159   by (simp add: prime_factorization_unit)
  1160 
  1161 lemma prime_factorization_times_prime:
  1162   assumes "x \<noteq> 0" "prime p"
  1163   shows   "prime_factorization (p * x) = {#p#} + prime_factorization x"
  1164 proof (rule multiset_eqI)
  1165   fix q :: 'a
  1166   consider "\<not>prime q" | "p = q" | "prime q" "p \<noteq> q" by blast
  1167   thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
  1168   proof cases
  1169     assume q: "prime q" "p \<noteq> q"
  1170     with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
  1171     with q assms show ?thesis
  1172       by (simp add: multiplicity_prime_elem_times_other count_prime_factorization)
  1173   qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
  1174 qed
  1175 
  1176 lemma prod_mset_prime_factorization:
  1177   assumes "x \<noteq> 0"
  1178   shows   "prod_mset (prime_factorization x) = normalize x"
  1179   using assms
  1180   by (induction x rule: prime_divisors_induct)
  1181      (simp_all add: prime_factorization_unit prime_factorization_times_prime
  1182                     is_unit_normalize normalize_mult)
  1183 
  1184 lemma in_prime_factors_iff:
  1185   "p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  1186 proof -
  1187   have "p \<in> prime_factors x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
  1188   also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
  1189    by (subst count_prime_factorization, cases "x = 0")
  1190       (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
  1191   finally show ?thesis .
  1192 qed
  1193 
  1194 lemma in_prime_factors_imp_prime [intro]:
  1195   "p \<in> prime_factors x \<Longrightarrow> prime p"
  1196   by (simp add: in_prime_factors_iff)
  1197 
  1198 lemma in_prime_factors_imp_dvd [dest]:
  1199   "p \<in> prime_factors x \<Longrightarrow> p dvd x"
  1200   by (simp add: in_prime_factors_iff)
  1201 
  1202 lemma prime_factorsI:
  1203   "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
  1204   by (auto simp: in_prime_factors_iff)
  1205 
  1206 lemma prime_factors_dvd:
  1207   "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
  1208   by (auto intro: prime_factorsI)
  1209 
  1210 lemma prime_factors_multiplicity:
  1211   "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
  1212   by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff)
  1213 
  1214 lemma prime_factorization_prime:
  1215   assumes "prime p"
  1216   shows   "prime_factorization p = {#p#}"
  1217 proof (rule multiset_eqI)
  1218   fix q :: 'a
  1219   consider "\<not>prime q" | "q = p" | "prime q" "q \<noteq> p" by blast
  1220   thus "count (prime_factorization p) q = count {#p#} q"
  1221     by cases (insert assms, auto dest: primes_dvd_imp_eq
  1222                 simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
  1223 qed
  1224 
  1225 lemma prime_factorization_prod_mset_primes:
  1226   assumes "\<And>p. p \<in># A \<Longrightarrow> prime p"
  1227   shows   "prime_factorization (prod_mset A) = A"
  1228   using assms
  1229 proof (induction A)
  1230   case (add p A)
  1231   from add.prems[of 0] have "0 \<notin># A" by auto
  1232   hence "prod_mset A \<noteq> 0" by auto
  1233   with add show ?case
  1234     by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
  1235 qed simp_all
  1236 
  1237 lemma prime_factorization_cong:
  1238   "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
  1239   by (simp add: multiset_eq_iff count_prime_factorization
  1240                 multiplicity_normalize_right [of _ x, symmetric]
  1241                 multiplicity_normalize_right [of _ y, symmetric]
  1242            del:  multiplicity_normalize_right)
  1243 
  1244 lemma prime_factorization_unique:
  1245   assumes "x \<noteq> 0" "y \<noteq> 0"
  1246   shows   "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y"
  1247 proof
  1248   assume "prime_factorization x = prime_factorization y"
  1249   hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
  1250   with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
  1251 qed (rule prime_factorization_cong)
  1252 
  1253 lemma prime_factorization_mult:
  1254   assumes "x \<noteq> 0" "y \<noteq> 0"
  1255   shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
  1256 proof -
  1257   have "prime_factorization (prod_mset (prime_factorization (x * y))) =
  1258           prime_factorization (prod_mset (prime_factorization x + prime_factorization y))"
  1259     by (simp add: prod_mset_prime_factorization assms normalize_mult)
  1260   also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
  1261                prime_factorization (x * y)"
  1262     by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime)
  1263   also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
  1264                prime_factorization x + prime_factorization y"
  1265     by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime)
  1266   finally show ?thesis .
  1267 qed
  1268 
  1269 lemma prime_elem_multiplicity_mult_distrib:
  1270   assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
  1271   shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
  1272 proof -
  1273   have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
  1274     by (subst count_prime_factorization_prime) (simp_all add: assms)
  1275   also from assms 
  1276     have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
  1277       by (intro prime_factorization_mult)
  1278   also have "count \<dots> (normalize p) = 
  1279     count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
  1280     by simp
  1281   also have "\<dots> = multiplicity p x + multiplicity p y" 
  1282     by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
  1283   finally show ?thesis .
  1284 qed
  1285 
  1286 lemma prime_elem_multiplicity_prod_mset_distrib:
  1287   assumes "prime_elem p" "0 \<notin># A"
  1288   shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
  1289   using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
  1290 
  1291 lemma prime_elem_multiplicity_power_distrib:
  1292   assumes "prime_elem p" "x \<noteq> 0"
  1293   shows   "multiplicity p (x ^ n) = n * multiplicity p x"
  1294   using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
  1295   by simp
  1296 
  1297 lemma prime_elem_multiplicity_setprod_distrib:
  1298   assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
  1299   shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
  1300 proof -
  1301   have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
  1302     using assms by (subst setprod_unfold_prod_mset)
  1303                    (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset 
  1304                       multiset.map_comp o_def)
  1305   also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
  1306     by (induction A rule: finite_induct) simp_all
  1307   finally show ?thesis .
  1308 qed
  1309 
  1310 lemma multiplicity_distinct_prime_power:
  1311   "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
  1312   by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
  1313 
  1314 lemma prime_factorization_prime_power:
  1315   "prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
  1316   by (induction n)
  1317      (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
  1318 
  1319 lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
  1320   by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
  1321 
  1322 lemma prime_factorization_subset_iff_dvd:
  1323   assumes [simp]: "x \<noteq> 0" "y \<noteq> 0"
  1324   shows   "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y"
  1325 proof -
  1326   have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
  1327     by (simp add: prod_mset_prime_factorization)
  1328   also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
  1329     by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd)
  1330   finally show ?thesis ..
  1331 qed
  1332 
  1333 lemma prime_factorization_subset_imp_dvd: 
  1334   "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
  1335   by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
  1336 
  1337 lemma prime_factorization_divide:
  1338   assumes "b dvd a"
  1339   shows   "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
  1340 proof (cases "a = 0")
  1341   case [simp]: False
  1342   from assms have [simp]: "b \<noteq> 0" by auto
  1343   have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b"
  1344     by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE)
  1345   with assms show ?thesis by simp
  1346 qed simp_all
  1347 
  1348 lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x"
  1349   by (auto dest: in_prime_factors_imp_prime)
  1350 
  1351 lemma prime_prime_factors:
  1352   "prime p \<Longrightarrow> prime_factors p = {p}"
  1353   by (drule prime_factorization_prime) simp
  1354 
  1355 lemma setprod_prime_factors:
  1356   assumes "x \<noteq> 0"
  1357   shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
  1358 proof -
  1359   have "normalize x = prod_mset (prime_factorization x)"
  1360     by (simp add: prod_mset_prime_factorization assms)
  1361   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
  1362     by (subst prod_mset_multiplicity) simp_all
  1363   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
  1364     by (intro setprod.cong) 
  1365       (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
  1366   finally show ?thesis ..
  1367 qed
  1368 
  1369 lemma prime_factorization_unique'':
  1370   assumes S_eq: "S = {p. 0 < f p}"
  1371     and "finite S"
  1372     and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
  1373   shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  1374 proof
  1375   define A where "A = Abs_multiset f"
  1376   from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
  1377   with S(2) have nz: "n \<noteq> 0" by auto
  1378   from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
  1379     unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
  1380   from S_eq count_A have set_mset_A: "set_mset A = S"
  1381     by (simp only: set_mset_def)
  1382   from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
  1383   also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
  1384   also from nz have "normalize n = prod_mset (prime_factorization n)" 
  1385     by (simp add: prod_mset_prime_factorization)
  1386   finally have "prime_factorization (prod_mset A) = 
  1387                   prime_factorization (prod_mset (prime_factorization n))" by simp
  1388   also from S(1) have "prime_factorization (prod_mset A) = A"
  1389     by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
  1390   also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
  1391     by (intro prime_factorization_prod_mset_primes) auto
  1392   finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
  1393   
  1394   show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
  1395   proof safe
  1396     fix p :: 'a assume p: "prime p"
  1397     have "multiplicity p n = multiplicity p (normalize n)" by simp
  1398     also have "normalize n = prod_mset A" 
  1399       by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
  1400     also from p set_mset_A S(1) 
  1401     have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
  1402       by (intro prime_elem_multiplicity_prod_mset_distrib) auto
  1403     also from S(1) p
  1404     have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
  1405       by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
  1406     also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
  1407     finally show "f p = multiplicity p n" ..
  1408   qed
  1409 qed
  1410 
  1411 lemma prime_factors_product: 
  1412   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
  1413   by (simp add: prime_factorization_mult)
  1414 
  1415 lemma dvd_prime_factors [intro]:
  1416   "y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
  1417   by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
  1418 
  1419 (* RENAMED multiplicity_dvd *)
  1420 lemma multiplicity_le_imp_dvd:
  1421   assumes "x \<noteq> 0" "\<And>p. prime p \<Longrightarrow> multiplicity p x \<le> multiplicity p y"
  1422   shows   "x dvd y"
  1423 proof (cases "y = 0")
  1424   case False
  1425   from assms this have "prime_factorization x \<subseteq># prime_factorization y"
  1426     by (intro mset_subset_eqI) (auto simp: count_prime_factorization)
  1427   with assms False show ?thesis by (subst (asm) prime_factorization_subset_iff_dvd)
  1428 qed auto
  1429 
  1430 lemma dvd_multiplicity_eq:
  1431   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
  1432   by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)
  1433 
  1434 lemma multiplicity_eq_imp_eq:
  1435   assumes "x \<noteq> 0" "y \<noteq> 0"
  1436   assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
  1437   shows   "normalize x = normalize y"
  1438   using assms by (intro associatedI multiplicity_le_imp_dvd) simp_all
  1439 
  1440 lemma prime_factorization_unique':
  1441   assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "(\<Prod>i \<in># M. i) = (\<Prod>i \<in># N. i)"
  1442   shows   "M = N"
  1443 proof -
  1444   have "prime_factorization (\<Prod>i \<in># M. i) = prime_factorization (\<Prod>i \<in># N. i)"
  1445     by (simp only: assms)
  1446   also from assms have "prime_factorization (\<Prod>i \<in># M. i) = M"
  1447     by (subst prime_factorization_prod_mset_primes) simp_all
  1448   also from assms have "prime_factorization (\<Prod>i \<in># N. i) = N"
  1449     by (subst prime_factorization_prod_mset_primes) simp_all
  1450   finally show ?thesis .
  1451 qed
  1452 
  1453 lemma multiplicity_cong:
  1454   "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
  1455   by (simp add: multiplicity_def)
  1456 
  1457 lemma not_dvd_imp_multiplicity_0: 
  1458   assumes "\<not>p dvd x"
  1459   shows   "multiplicity p x = 0"
  1460 proof -
  1461   from assms have "multiplicity p x < 1"
  1462     by (intro multiplicity_lessI) auto
  1463   thus ?thesis by simp
  1464 qed
  1465 
  1466 
  1467 subsection \<open>GCD and LCM computation with unique factorizations\<close>
  1468 
  1469 definition "gcd_factorial a b = (if a = 0 then normalize b
  1470      else if b = 0 then normalize a
  1471      else prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1472 
  1473 definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
  1474      else prod_mset (prime_factorization a \<union># prime_factorization b))"
  1475 
  1476 definition "Gcd_factorial A =
  1477   (if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))"
  1478 
  1479 definition "Lcm_factorial A =
  1480   (if A = {} then 1
  1481    else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then
  1482      prod_mset (Sup (prime_factorization ` A))
  1483    else
  1484      0)"
  1485 
  1486 lemma prime_factorization_gcd_factorial:
  1487   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1488   shows   "prime_factorization (gcd_factorial a b) = prime_factorization a \<inter># prime_factorization b"
  1489 proof -
  1490   have "prime_factorization (gcd_factorial a b) =
  1491           prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1492     by (simp add: gcd_factorial_def)
  1493   also have "\<dots> = prime_factorization a \<inter># prime_factorization b"
  1494     by (subst prime_factorization_prod_mset_primes) auto
  1495   finally show ?thesis .
  1496 qed
  1497 
  1498 lemma prime_factorization_lcm_factorial:
  1499   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1500   shows   "prime_factorization (lcm_factorial a b) = prime_factorization a \<union># prime_factorization b"
  1501 proof -
  1502   have "prime_factorization (lcm_factorial a b) =
  1503           prime_factorization (prod_mset (prime_factorization a \<union># prime_factorization b))"
  1504     by (simp add: lcm_factorial_def)
  1505   also have "\<dots> = prime_factorization a \<union># prime_factorization b"
  1506     by (subst prime_factorization_prod_mset_primes) auto
  1507   finally show ?thesis .
  1508 qed
  1509 
  1510 lemma prime_factorization_Gcd_factorial:
  1511   assumes "\<not>A \<subseteq> {0}"
  1512   shows   "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
  1513 proof -
  1514   from assms obtain x where x: "x \<in> A - {0}" by auto
  1515   hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
  1516     by (intro subset_mset.cInf_lower) simp_all
  1517   hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in> prime_factors x"
  1518     by (auto dest: mset_subset_eqD)
  1519   with in_prime_factors_imp_prime[of _ x]
  1520     have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> prime p" by blast
  1521   with assms show ?thesis
  1522     by (simp add: Gcd_factorial_def prime_factorization_prod_mset_primes)
  1523 qed
  1524 
  1525 lemma prime_factorization_Lcm_factorial:
  1526   assumes "0 \<notin> A" "subset_mset.bdd_above (prime_factorization ` A)"
  1527   shows   "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
  1528 proof (cases "A = {}")
  1529   case True
  1530   hence "prime_factorization ` A = {}" by auto
  1531   also have "Sup \<dots> = {#}" by (simp add: Sup_multiset_empty)
  1532   finally show ?thesis by (simp add: Lcm_factorial_def)
  1533 next
  1534   case False
  1535   have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> prime y"
  1536     by (auto simp: in_Sup_multiset_iff assms)
  1537   with assms False show ?thesis
  1538     by (simp add: Lcm_factorial_def prime_factorization_prod_mset_primes)
  1539 qed
  1540 
  1541 lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a"
  1542   by (simp add: gcd_factorial_def multiset_inter_commute)
  1543 
  1544 lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a"
  1545 proof (cases "a = 0 \<or> b = 0")
  1546   case False
  1547   hence "gcd_factorial a b \<noteq> 0" by (auto simp: gcd_factorial_def)
  1548   with False show ?thesis
  1549     by (subst prime_factorization_subset_iff_dvd [symmetric])
  1550        (auto simp: prime_factorization_gcd_factorial)
  1551 qed (auto simp: gcd_factorial_def)
  1552 
  1553 lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b"
  1554   by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1)
  1555 
  1556 lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b"
  1557 proof -
  1558   have "normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)) =
  1559           prod_mset (prime_factorization a \<inter># prime_factorization b)"
  1560     by (intro normalize_prod_mset_primes) auto
  1561   thus ?thesis by (simp add: gcd_factorial_def)
  1562 qed
  1563 
  1564 lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c
  1565 proof (cases "a = 0 \<or> b = 0")
  1566   case False
  1567   with that have [simp]: "c \<noteq> 0" by auto
  1568   let ?p = "prime_factorization"
  1569   from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b"
  1570     by (simp_all add: prime_factorization_subset_iff_dvd)
  1571   hence "prime_factorization c \<subseteq>#
  1572            prime_factorization (prod_mset (prime_factorization a \<inter># prime_factorization b))"
  1573     using False by (subst prime_factorization_prod_mset_primes) auto
  1574   with False show ?thesis
  1575     by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric])
  1576 qed (auto simp: gcd_factorial_def that)
  1577 
  1578 lemma lcm_factorial_gcd_factorial:
  1579   "lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b
  1580 proof (cases "a = 0 \<or> b = 0")
  1581   case False
  1582   let ?p = "prime_factorization"
  1583   from False have "prod_mset (?p (a * b)) div gcd_factorial a b =
  1584                      prod_mset (?p a + ?p b - ?p a \<inter># ?p b)"
  1585     by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def
  1586                                 prime_factorization_mult subset_mset.le_infI1)
  1587   also from False have "prod_mset (?p (a * b)) = normalize (a * b)"
  1588     by (intro prod_mset_prime_factorization) simp_all
  1589   also from False have "prod_mset (?p a + ?p b - ?p a \<inter># ?p b) = lcm_factorial a b"
  1590     by (simp add: union_diff_inter_eq_sup lcm_factorial_def)
  1591   finally show ?thesis ..
  1592 qed (auto simp: lcm_factorial_def)
  1593 
  1594 lemma normalize_Gcd_factorial:
  1595   "normalize (Gcd_factorial A) = Gcd_factorial A"
  1596 proof (cases "A \<subseteq> {0}")
  1597   case False
  1598   then obtain x where "x \<in> A" "x \<noteq> 0" by blast
  1599   hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
  1600     by (intro subset_mset.cInf_lower) auto
  1601   hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
  1602     using that by (auto dest: mset_subset_eqD)
  1603   with False show ?thesis
  1604     by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
  1605 qed (simp_all add: Gcd_factorial_def)
  1606 
  1607 lemma Gcd_factorial_eq_0_iff:
  1608   "Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}"
  1609   by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits)
  1610 
  1611 lemma Gcd_factorial_dvd:
  1612   assumes "x \<in> A"
  1613   shows   "Gcd_factorial A dvd x"
  1614 proof (cases "x = 0")
  1615   case False
  1616   with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
  1617     by (intro prime_factorization_Gcd_factorial) auto
  1618   also from False assms have "\<dots> \<subseteq># prime_factorization x"
  1619     by (intro subset_mset.cInf_lower) auto
  1620   finally show ?thesis
  1621     by (subst (asm) prime_factorization_subset_iff_dvd)
  1622        (insert assms False, auto simp: Gcd_factorial_eq_0_iff)
  1623 qed simp_all
  1624 
  1625 lemma Gcd_factorial_greatest:
  1626   assumes "\<And>y. y \<in> A \<Longrightarrow> x dvd y"
  1627   shows   "x dvd Gcd_factorial A"
  1628 proof (cases "A \<subseteq> {0}")
  1629   case False
  1630   from False obtain y where "y \<in> A" "y \<noteq> 0" by auto
  1631   with assms[of y] have nz: "x \<noteq> 0" by auto
  1632   from nz assms have "prime_factorization x \<subseteq># prime_factorization y" if "y \<in> A - {0}" for y
  1633     using that by (subst prime_factorization_subset_iff_dvd) auto
  1634   with False have "prime_factorization x \<subseteq># Inf (prime_factorization ` (A - {0}))"
  1635     by (intro subset_mset.cInf_greatest) auto
  1636   also from False have "\<dots> = prime_factorization (Gcd_factorial A)"
  1637     by (rule prime_factorization_Gcd_factorial [symmetric])
  1638   finally show ?thesis
  1639     by (subst (asm) prime_factorization_subset_iff_dvd)
  1640        (insert nz False, auto simp: Gcd_factorial_eq_0_iff)
  1641 qed (simp_all add: Gcd_factorial_def)
  1642 
  1643 
  1644 lemma normalize_Lcm_factorial:
  1645   "normalize (Lcm_factorial A) = Lcm_factorial A"
  1646 proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
  1647   case True
  1648   hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
  1649            prod_mset (Sup (prime_factorization ` A))"
  1650     by (intro normalize_prod_mset_primes)
  1651        (auto simp: in_Sup_multiset_iff)
  1652   with True show ?thesis by (simp add: Lcm_factorial_def)
  1653 qed (auto simp: Lcm_factorial_def)
  1654 
  1655 lemma Lcm_factorial_eq_0_iff:
  1656   "Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)"
  1657   by (auto simp: Lcm_factorial_def in_Sup_multiset_iff)
  1658 
  1659 lemma dvd_Lcm_factorial:
  1660   assumes "x \<in> A"
  1661   shows   "x dvd Lcm_factorial A"
  1662 proof (cases "0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` A)")
  1663   case True
  1664   with assms have [simp]: "0 \<notin> A" "x \<noteq> 0" "A \<noteq> {}" by auto
  1665   from assms True have "prime_factorization x \<subseteq># Sup (prime_factorization ` A)"
  1666     by (intro subset_mset.cSup_upper) auto
  1667   also have "\<dots> = prime_factorization (Lcm_factorial A)"
  1668     by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all)
  1669   finally show ?thesis
  1670     by (subst (asm) prime_factorization_subset_iff_dvd)
  1671        (insert True, auto simp: Lcm_factorial_eq_0_iff)
  1672 qed (insert assms, auto simp: Lcm_factorial_def)
  1673 
  1674 lemma Lcm_factorial_least:
  1675   assumes "\<And>y. y \<in> A \<Longrightarrow> y dvd x"
  1676   shows   "Lcm_factorial A dvd x"
  1677 proof -
  1678   consider "A = {}" | "0 \<in> A" | "x = 0" | "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" by blast
  1679   thus ?thesis
  1680   proof cases
  1681     assume *: "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0"
  1682     hence nz: "x \<noteq> 0" if "x \<in> A" for x using that by auto
  1683     from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)"
  1684       by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"])
  1685          (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
  1686     have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
  1687       by (rule prime_factorization_Lcm_factorial) fact+
  1688     also from * have "\<dots> \<subseteq># prime_factorization x"
  1689       by (intro subset_mset.cSup_least)
  1690          (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
  1691     finally show ?thesis
  1692       by (subst (asm) prime_factorization_subset_iff_dvd)
  1693          (insert * bdd, auto simp: Lcm_factorial_eq_0_iff)
  1694   qed (auto simp: Lcm_factorial_def dest: assms)
  1695 qed
  1696 
  1697 lemmas gcd_lcm_factorial =
  1698   gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest
  1699   normalize_gcd_factorial lcm_factorial_gcd_factorial
  1700   normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest
  1701   normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least
  1702 
  1703 end
  1704 
  1705 class factorial_semiring_gcd = factorial_semiring + gcd + Gcd +
  1706   assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b"
  1707   and     lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b"
  1708   and     Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A"
  1709   and     Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A"
  1710 begin
  1711 
  1712 lemma prime_factorization_gcd:
  1713   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1714   shows   "prime_factorization (gcd a b) = prime_factorization a \<inter># prime_factorization b"
  1715   by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial)
  1716 
  1717 lemma prime_factorization_lcm:
  1718   assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
  1719   shows   "prime_factorization (lcm a b) = prime_factorization a \<union># prime_factorization b"
  1720   by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial)
  1721 
  1722 lemma prime_factorization_Gcd:
  1723   assumes "Gcd A \<noteq> 0"
  1724   shows   "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))"
  1725   using assms
  1726   by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff)
  1727 
  1728 lemma prime_factorization_Lcm:
  1729   assumes "Lcm A \<noteq> 0"
  1730   shows   "prime_factorization (Lcm A) = Sup (prime_factorization ` A)"
  1731   using assms
  1732   by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff)
  1733 
  1734 subclass semiring_gcd
  1735   by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial)
  1736      (rule gcd_lcm_factorial; assumption)+
  1737 
  1738 subclass semiring_Gcd
  1739   by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
  1740      (rule gcd_lcm_factorial; assumption)+
  1741 
  1742 lemma
  1743   assumes "x \<noteq> 0" "y \<noteq> 0"
  1744   shows gcd_eq_factorial': 
  1745           "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. 
  1746                           p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
  1747     and lcm_eq_factorial':
  1748           "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. 
  1749                           p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
  1750 proof -
  1751   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
  1752   also have "\<dots> = ?rhs1"
  1753     by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
  1754           count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
  1755   finally show "gcd x y = ?rhs1" .
  1756   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
  1757   also have "\<dots> = ?rhs2"
  1758     by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
  1759           count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: setprod.cong)
  1760   finally show "lcm x y = ?rhs2" .
  1761 qed
  1762 
  1763 lemma
  1764   assumes "x \<noteq> 0" "y \<noteq> 0" "prime p"
  1765   shows   multiplicity_gcd: "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)"
  1766     and   multiplicity_lcm: "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)"
  1767 proof -
  1768   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
  1769   also from assms have "multiplicity p \<dots> = min (multiplicity p x) (multiplicity p y)"
  1770     by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_gcd_factorial)
  1771   finally show "multiplicity p (gcd x y) = min (multiplicity p x) (multiplicity p y)" .
  1772   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
  1773   also from assms have "multiplicity p \<dots> = max (multiplicity p x) (multiplicity p y)"
  1774     by (simp add: count_prime_factorization_prime [symmetric] prime_factorization_lcm_factorial)
  1775   finally show "multiplicity p (lcm x y) = max (multiplicity p x) (multiplicity p y)" .
  1776 qed
  1777 
  1778 lemma gcd_lcm_distrib:
  1779   "gcd x (lcm y z) = lcm (gcd x y) (gcd x z)"
  1780 proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
  1781   case True
  1782   thus ?thesis
  1783     by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
  1784 next
  1785   case False
  1786   hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
  1787     by (intro associatedI prime_factorization_subset_imp_dvd)
  1788        (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
  1789           subset_mset.inf_sup_distrib1)
  1790   thus ?thesis by simp
  1791 qed
  1792 
  1793 lemma lcm_gcd_distrib:
  1794   "lcm x (gcd y z) = gcd (lcm x y) (lcm x z)"
  1795 proof (cases "x = 0 \<or> y = 0 \<or> z = 0")
  1796   case True
  1797   thus ?thesis
  1798     by (auto simp: lcm_proj1_if_dvd lcm_proj2_if_dvd)
  1799 next
  1800   case False
  1801   hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
  1802     by (intro associatedI prime_factorization_subset_imp_dvd)
  1803        (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
  1804           subset_mset.sup_inf_distrib1)
  1805   thus ?thesis by simp
  1806 qed
  1807 
  1808 end
  1809 
  1810 class factorial_ring_gcd = factorial_semiring_gcd + idom
  1811 begin
  1812 
  1813 subclass ring_gcd ..
  1814 
  1815 subclass idom_divide ..
  1816 
  1817 end
  1818 
  1819 end