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
```