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