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