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