author haftmann Sun, 18 Sep 2016 17:57:55 +0200 changeset 63924 f91766530e13 parent 63923 c9bba9dba73b child 63925 500646ef617a
more generic algebraic lemmas
 src/HOL/GCD.thy file | annotate | diff | comparison | revisions src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Factorial_Ring.thy file | annotate | diff | comparison | revisions src/HOL/Power.thy file | annotate | diff | comparison | revisions src/HOL/Rings.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/GCD.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/GCD.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -939,6 +939,25 @@
lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
using lcm_proj1_iff [of n m] by (simp add: ac_simps)

+lemma dvd_productE:
+  assumes "p dvd (a * b)"
+  obtains x y where "p = x * y" "x dvd a" "y dvd b"
+proof (cases "a = 0")
+  case True
+  thus ?thesis by (intro that[of p 1]) simp_all
+next
+  case False
+  define x y where "x = gcd a p" and "y = p div x"
+  have "p = x * y" by (simp add: x_def y_def)
+  moreover have "x dvd a" by (simp add: x_def)
+  moreover from assms have "p dvd gcd (b * a) (b * p)"
+    by (intro gcd_greatest) (simp_all add: mult.commute)
+  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
+  with False have "y dvd b"
+    by (simp add: x_def y_def div_dvd_iff_mult assms)
+  ultimately show ?thesis by (rule that)
+qed
+
end

class ring_gcd = comm_ring_1 + semiring_gcd```
```--- a/src/HOL/Groups_Big.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -1130,8 +1130,8 @@

end

-lemma setprod_zero_iff [simp]:
-  fixes f :: "'b \<Rightarrow> 'a::semidom"
+lemma (in semidom) setprod_zero_iff [simp]:
+  fixes f :: "'b \<Rightarrow> 'a"
assumes "finite A"
shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
using assms by (induct A) (auto simp: no_zero_divisors)```
```--- a/src/HOL/Library/Multiset.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -247,6 +247,14 @@
by (auto simp del: count_greater_eq_Suc_zero_iff
simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)

+lemma multiset_nonemptyE [elim]:
+  assumes "A \<noteq> {#}"
+  obtains x where "x \<in># A"
+proof -
+  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
+  with that show ?thesis by blast
+qed
+

subsubsection \<open>Union\<close>

@@ -2041,6 +2049,10 @@
lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
by (auto simp: multiset_eq_iff)

+lemma image_replicate_mset [simp]:
+  "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
+  by (induct n) simp_all
+

subsection \<open>Big operators\<close>

@@ -2209,14 +2221,20 @@
translations
"\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"

-lemma (in comm_semiring_1) dvd_prod_mset:
+lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
+  assumes "A \<subseteq># B"
+  shows   "prod_mset A dvd prod_mset B"
+proof -
+  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
+  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
+  also have "prod_mset A dvd \<dots>" by simp
+  finally show ?thesis .
+qed
+
+lemma (in comm_monoid_mult) dvd_prod_mset:
assumes "x \<in># A"
shows "x dvd prod_mset A"
-proof -
-  from assms have "A = add_mset x (A - {#x#})" by simp
-  then obtain B where "A = add_mset x B" ..
-  then show ?thesis by simp
-qed
+  using assms prod_mset_subset_imp_dvd [of "{#x#}" A] by simp

lemma (in semidom) prod_mset_zero_iff [iff]:
"prod_mset A = 0 \<longleftrightarrow> 0 \<in># A"
@@ -2236,10 +2254,22 @@
shows "prod_mset (A - {#a#}) = prod_mset A div a"
using assms prod_mset_diff [of "{#a#}" A] by auto

+lemma (in algebraic_semidom) is_unit_prod_mset_iff:
+  "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x \<in># A. is_unit x)"
+  by (induct A) (auto simp: is_unit_mult_iff)
+
+lemma (in normalization_semidom) normalize_prod_mset:
+  "normalize (prod_mset A) = prod_mset (image_mset normalize A)"
+  by (induct A) (simp_all add: normalize_mult)
+
lemma (in normalization_semidom) normalized_prod_msetI:
assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
shows "normalize (prod_mset A) = prod_mset A"
-  using assms by (induct A) (simp_all add: normalize_mult)
+proof -
+  from assms have "image_mset normalize A = A"
+    by (induct A) simp_all
+  then show ?thesis by (simp add: normalize_prod_mset)
+qed

subsection \<open>Alternative representations\<close>```
```--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -112,23 +112,6 @@
by (auto intro!: euclidean_size_times_nonunit simp: )
qed

-lemma irreducible_normalized_divisors:
-  assumes "irreducible x" "y dvd x" "normalize y = y"
-  shows   "y = 1 \<or> y = normalize x"
-proof -
-  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
-  thus ?thesis
-  proof (elim disjE)
-    assume "is_unit y"
-    hence "normalize y = 1" by (simp add: is_unit_normalize)
-    with assms show ?thesis by simp
-  next
-    assume "x dvd y"
-    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
-    with assms show ?thesis by simp
-  qed
-qed
-
function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
where
"gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
@@ -720,4 +703,4 @@
semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
qed

-end
\ No newline at end of file
+end```
```--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -1,4 +1,5 @@
(*  Title:      HOL/Number_Theory/Factorial_Ring.thy
+    Author:     Manuel Eberl, TU Muenchen
Author:     Florian Haftmann, TU Muenchen
*)

@@ -7,29 +8,11 @@
theory Factorial_Ring
imports
Main
-  "../GCD"
+  "~~/src/HOL/GCD"
"~~/src/HOL/Library/Multiset"
begin

-lemma (in semiring_gcd) dvd_productE:
-  assumes "p dvd (a * b)"
-  obtains x y where "p = x * y" "x dvd a" "y dvd b"
-proof (cases "a = 0")
-  case True
-  thus ?thesis by (intro that[of p 1]) simp_all
-next
-  case False
-  define x y where "x = gcd a p" and "y = p div x"
-  have "p = x * y" by (simp add: x_def y_def)
-  moreover have "x dvd a" by (simp add: x_def)
-  moreover from assms have "p dvd gcd (b * a) (b * p)"
-    by (intro gcd_greatest) (simp_all add: mult.commute)
-  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
-  with False have "y dvd b"
-    by (simp add: x_def y_def div_dvd_iff_mult assms)
-  ultimately show ?thesis by (rule that)
-qed
-
+subsection \<open>Irreducible and prime elements\<close>

context comm_semiring_1
begin
@@ -83,7 +66,6 @@
shows "p \<noteq> 0"
using assms by (auto intro: ccontr)

-
lemma prime_elem_dvd_power:
"prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
@@ -105,10 +87,6 @@
context algebraic_semidom
begin

-(* TODO Move *)
-lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
-  by (subst mult.commute) (rule mult_unit_dvd_iff)
-
lemma prime_elem_imp_irreducible:
assumes "prime_elem p"
shows   "irreducible p"
@@ -123,6 +101,22 @@
by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
qed (insert assms, simp_all add: prime_elem_def)

+lemma (in algebraic_semidom) unit_imp_no_irreducible_divisors:
+  assumes "is_unit x" "irreducible p"
+  shows   "\<not>p dvd x"
+proof (rule notI)
+  assume "p dvd x"
+  with \<open>is_unit x\<close> have "is_unit p"
+    by (auto intro: dvd_trans)
+  with \<open>irreducible p\<close> show False
+qed
+
+lemma unit_imp_no_prime_divisors:
+  assumes "is_unit x" "prime_elem p"
+  shows   "\<not>p dvd x"
+  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
+
lemma prime_elem_mono:
assumes "prime_elem p" "\<not>q dvd 1" "q dvd p"
shows   "prime_elem q"
@@ -306,12 +300,17 @@
qed
qed

-lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
-  by arith
-
lemma prime_elem_power_dvd_cases:
-     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
-  using power_le_dvd by (blast dest: prime_elem_power_dvd_prod add_eq_Suc_lem)
+  assumes "p ^ c dvd m * n" and "a + b = Suc c" and "prime_elem p"
+  shows "p ^ a dvd m \<or> p ^ b dvd n"
+proof -
+  from assms obtain r s
+    where "r + s = c \<and> p ^ r dvd m \<and> p ^ s dvd n"
+    by (blast dest: prime_elem_power_dvd_prod)
+  moreover with assms have
+    "a \<le> r \<or> b \<le> s" by arith
+  ultimately show ?thesis by (auto intro: power_le_dvd)
+qed

lemma prime_elem_not_unit' [simp]:
"ASSUMPTION (prime_elem x) \<Longrightarrow> \<not>is_unit x"
@@ -358,9 +357,29 @@

end

+
+subsection \<open>Generalized primes: normalized prime elements\<close>
+
context normalization_semidom
begin

+lemma irreducible_normalized_divisors:
+  assumes "irreducible x" "y dvd x" "normalize y = y"
+  shows   "y = 1 \<or> y = normalize x"
+proof -
+  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
+  thus ?thesis
+  proof (elim disjE)
+    assume "is_unit y"
+    hence "normalize y = 1" by (simp add: is_unit_normalize)
+    with assms show ?thesis by simp
+  next
+    assume "x dvd y"
+    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
+    with assms show ?thesis by simp
+  qed
+qed
+
lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
using irreducible_mult_unit_left[of "1 div unit_factor x" x]
by (cases "x = 0") (simp_all add: unit_div_commute)
@@ -443,16 +462,6 @@
"prime p \<Longrightarrow> n > 0 \<Longrightarrow> p dvd x ^ n \<longleftrightarrow> p dvd x"
by (subst prime_elem_dvd_power_iff) simp_all

-lemma prod_mset_subset_imp_dvd:
-  assumes "A \<subseteq># B"
-  shows   "prod_mset A dvd prod_mset B"
-proof -
-  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
-  also have "prod_mset \<dots> = prod_mset (B - A) * prod_mset A" by simp
-  also have "prod_mset A dvd \<dots>" by simp
-  finally show ?thesis .
-qed
-
lemma prime_dvd_prod_mset_iff: "prime p \<Longrightarrow> p dvd prod_mset A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
by (induction A) (simp_all add: prime_elem_dvd_mult_iff prime_imp_prime_elem, blast+)

@@ -508,26 +517,11 @@
shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
using assms by (auto intro: prod_mset_subset_imp_dvd prod_mset_primes_dvd_imp_subset)

-lemma is_unit_prod_mset_iff:
-  "is_unit (prod_mset A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
-  by (induction A) (auto simp: is_unit_mult_iff)
-
-lemma multiset_emptyI: "(\<And>x. x \<notin># A) \<Longrightarrow> A = {#}"
-  by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
-
lemma is_unit_prod_mset_primes_iff:
assumes "\<And>x. x \<in># A \<Longrightarrow> prime x"
shows   "is_unit (prod_mset A) \<longleftrightarrow> A = {#}"
-proof
-  assume unit: "is_unit (prod_mset A)"
-  show "A = {#}"
-  proof (intro multiset_emptyI notI)
-    fix x assume "x \<in># A"
-    with unit have "is_unit x" by (subst (asm) is_unit_prod_mset_iff) blast
-    moreover from \<open>x \<in># A\<close> have "prime x" by (rule assms)
-    ultimately show False by simp
-  qed
-qed simp_all
+  by (auto simp add: is_unit_prod_mset_iff)
+    (meson all_not_in_conv assms not_prime_unit set_mset_eq_empty_iff)

lemma prod_mset_primes_irreducible_imp_prime:
assumes irred: "irreducible (prod_mset A)"
@@ -555,14 +549,6 @@
by (auto intro: prod_mset_subset_imp_dvd)
qed

-lemma multiset_nonemptyE [elim]:
-  assumes "A \<noteq> {#}"
-  obtains x where "x \<in># A"
-proof -
-  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
-  with that show ?thesis by blast
-qed
-
lemma prod_mset_primes_finite_divisor_powers:
assumes A: "\<And>x. x \<in># A \<Longrightarrow> prime x"
assumes B: "\<And>x. x \<in># B \<Longrightarrow> prime x"
@@ -585,11 +571,10 @@
ultimately show ?thesis by (rule finite_subset)
qed

-lemma normalize_prod_mset:
-  "normalize (prod_mset A) = prod_mset (image_mset normalize A)"
-  by (induction A) (simp_all add: normalize_mult mult_ac)
+end

-end
+
+subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>

context semiring_gcd
begin
@@ -652,9 +637,83 @@
end

+subsection \<open>Factorial semirings: algebraic structures with unique prime factorizations\<close>
+
class factorial_semiring = normalization_semidom +
assumes prime_factorization_exists:
-            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
+    "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
+
+text \<open>Alternative characterization\<close>
+
+lemma (in normalization_semidom) factorial_semiring_altI_aux:
+  assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
+  assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
+  assumes "x \<noteq> 0"
+  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
+using \<open>x \<noteq> 0\<close>
+proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
+  case (less a)
+  let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
+  show ?case
+  proof (cases "is_unit a")
+    case True
+    thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
+  next
+    case False
+    show ?thesis
+    proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
+      case False
+      with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
+      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
+      thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
+    next
+      case True
+      then guess b by (elim exE conjE) note b = this
+
+      from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
+      moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
+      hence "?fctrs b \<noteq> ?fctrs a" by blast
+      ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
+      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
+        by (rule psubset_card_mono)
+      moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
+      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
+        by (intro less) auto
+      then guess A .. note A = this
+
+      define c where "c = a div b"
+      from b have c: "a = b * c" by (simp add: c_def)
+      from less.prems c have "c \<noteq> 0" by auto
+      from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
+      moreover have "normalize a \<notin> ?fctrs c"
+      proof safe
+        assume "normalize a dvd c"
+        hence "b * c dvd 1 * c" by (simp add: c)
+        hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
+        with b show False by simp
+      qed
+      with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
+      ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
+      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
+        by (rule psubset_card_mono)
+      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
+        by (intro less) auto
+      then guess B .. note B = this
+
+      from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
+    qed
+  qed
+qed
+
+lemma factorial_semiring_altI:
+  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
+  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
+  shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
+  by intro_classes (rule factorial_semiring_altI_aux[OF assms])
+
+text \<open>Properties\<close>
+
+context factorial_semiring
begin

lemma prime_factorization_exists':
@@ -784,24 +843,6 @@
lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x"
by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])

-lemma dvd_power_iff:
-  assumes "x \<noteq> 0"
-  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
-proof
-  assume *: "x ^ m dvd x ^ n"
-  {
-    assume "m > n"
-    note *
-    also have "x ^ n = x ^ n * 1" by simp
-    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
-    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
-    finally have "x ^ (m - n) dvd 1"
-      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
-    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
-  }
-  thus "is_unit x \<or> m \<le> n" by force
-qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
-
context
fixes x p :: 'a
assumes xp: "x \<noteq> 0" "\<not>is_unit p"
@@ -965,6 +1006,65 @@
qed
qed simp_all

+lemma multiplicity_self:
+  assumes "p \<noteq> 0" "\<not>is_unit p"
+  shows   "multiplicity p p = 1"
+proof -
+  from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
+  also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
+    using dvd_power_iff[of p n 1] by auto
+  hence "{n. p ^ n dvd p} = {..1}" by auto
+  also have "\<dots> = {0,1}" by auto
+  finally show ?thesis by simp
+qed
+
+lemma multiplicity_times_unit_left:
+  assumes "is_unit c"
+  shows   "multiplicity (c * p) x = multiplicity p x"
+proof -
+  from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
+    by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
+  thus ?thesis by (simp add: multiplicity_def)
+qed
+
+lemma multiplicity_times_unit_right:
+  assumes "is_unit c"
+  shows   "multiplicity p (c * x) = multiplicity p x"
+proof -
+  from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
+    by (subst mult.commute) (simp add: dvd_mult_unit_iff)
+  thus ?thesis by (simp add: multiplicity_def)
+qed
+
+lemma multiplicity_normalize_left [simp]:
+  "multiplicity (normalize p) x = multiplicity p x"
+proof (cases "p = 0")
+  case [simp]: False
+  have "normalize p = (1 div unit_factor p) * p"
+    by (simp add: unit_div_commute is_unit_unit_factor)
+  also have "multiplicity \<dots> x = multiplicity p x"
+    by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
+  finally show ?thesis .
+qed simp_all
+
+lemma multiplicity_normalize_right [simp]:
+  "multiplicity p (normalize x) = multiplicity p x"
+proof (cases "x = 0")
+  case [simp]: False
+  have "normalize x = (1 div unit_factor x) * x"
+    by (simp add: unit_div_commute is_unit_unit_factor)
+  also have "multiplicity p \<dots> = multiplicity p x"
+    by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
+  finally show ?thesis .
+qed simp_all
+
+lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
+  by (rule multiplicity_self) auto
+
+lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
+  by (subst multiplicity_same_power') auto
+
lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
"\<lambda>x p. if prime p then multiplicity p x else 0"
unfolding multiset_def
@@ -996,15 +1096,14 @@
"count (prime_factorization x) p = (if prime p then multiplicity p x else 0)"
by transfer simp

-lemma unit_imp_no_irreducible_divisors:
-  assumes "is_unit x" "irreducible p"
-  shows   "\<not>p dvd x"
-  using assms dvd_unit_imp_unit irreducible_not_unit by blast
-
-lemma unit_imp_no_prime_divisors:
-  assumes "is_unit x" "prime_elem p"
-  shows   "\<not>p dvd x"
-  using unit_imp_no_irreducible_divisors[OF assms(1) prime_elem_imp_irreducible[OF assms(2)]] .
+lemma dvd_imp_multiplicity_le:
+  assumes "a dvd b" "b \<noteq> 0"
+  shows   "multiplicity p a \<le> multiplicity p b"
+proof (cases "is_unit p")
+  case False
+  with assms show ?thesis
+    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
+qed (insert assms, auto simp: multiplicity_unit_left)

lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
@@ -1100,18 +1199,17 @@
"p \<in> prime_factors x \<Longrightarrow> p dvd x"

-lemma multiplicity_self:
-  assumes "p \<noteq> 0" "\<not>is_unit p"
-  shows   "multiplicity p p = 1"
-proof -
-  from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
-  also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
-    using dvd_power_iff[of p n 1] by auto
-  hence "{n. p ^ n dvd p} = {..1}" by auto
-  also have "\<dots> = {0,1}" by auto
-  finally show ?thesis by simp
-qed
+lemma prime_factorsI:
+  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
+  by (auto simp: in_prime_factors_iff)
+
+lemma prime_factors_dvd:
+  "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
+  by (auto intro: prime_factorsI)
+
+lemma prime_factors_multiplicity:
+  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
+  by (cases "n = 0") (auto simp add: prime_factors_dvd prime_multiplicity_gt_zero_iff)

lemma prime_factorization_prime:
assumes "prime p"
@@ -1136,44 +1234,6 @@
by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
qed simp_all

-lemma multiplicity_times_unit_left:
-  assumes "is_unit c"
-  shows   "multiplicity (c * p) x = multiplicity p x"
-proof -
-  from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
-    by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
-  thus ?thesis by (simp add: multiplicity_def)
-qed
-
-lemma multiplicity_times_unit_right:
-  assumes "is_unit c"
-  shows   "multiplicity p (c * x) = multiplicity p x"
-proof -
-  from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
-    by (subst mult.commute) (simp add: dvd_mult_unit_iff)
-  thus ?thesis by (simp add: multiplicity_def)
-qed
-
-lemma multiplicity_normalize_left [simp]: "multiplicity (normalize p) x = multiplicity p x"
-proof (cases "p = 0")
-  case [simp]: False
-  have "normalize p = (1 div unit_factor p) * p"
-    by (simp add: unit_div_commute is_unit_unit_factor)
-  also have "multiplicity \<dots> x = multiplicity p x"
-    by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
-  finally show ?thesis .
-qed simp_all
-
-lemma multiplicity_normalize_right [simp]: "multiplicity p (normalize x) = multiplicity p x"
-proof (cases "x = 0")
-  case [simp]: False
-  have "normalize x = (1 div unit_factor x) * x"
-    by (simp add: unit_div_commute is_unit_unit_factor)
-  also have "multiplicity p \<dots> = multiplicity p x"
-    by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
-  finally show ?thesis .
-qed simp_all
-
lemma prime_factorization_cong:
"normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
@@ -1206,6 +1266,51 @@
finally show ?thesis .
qed

+lemma prime_elem_multiplicity_mult_distrib:
+  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
+  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
+proof -
+  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
+    by (subst count_prime_factorization_prime) (simp_all add: assms)
+  also from assms
+    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
+      by (intro prime_factorization_mult)
+  also have "count \<dots> (normalize p) =
+    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
+    by simp
+  also have "\<dots> = multiplicity p x + multiplicity p y"
+    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
+  finally show ?thesis .
+qed
+
+lemma prime_elem_multiplicity_prod_mset_distrib:
+  assumes "prime_elem p" "0 \<notin># A"
+  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
+  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
+
+lemma prime_elem_multiplicity_power_distrib:
+  assumes "prime_elem p" "x \<noteq> 0"
+  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
+  using assms prime_elem_multiplicity_prod_mset_distrib [of p "replicate_mset n x"]
+  by simp
+
+lemma prime_elem_multiplicity_setprod_distrib:
+  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
+  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
+proof -
+  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
+    using assms by (subst setprod_unfold_prod_mset)
+                      multiset.map_comp o_def)
+  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
+    by (induction A rule: finite_induct) simp_all
+  finally show ?thesis .
+qed
+
+lemma multiplicity_distinct_prime_power:
+  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
+  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
+
lemma prime_factorization_prime_power:
"prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
by (induction n)
@@ -1243,60 +1348,10 @@
lemma zero_not_in_prime_factors [simp]: "0 \<notin> prime_factors x"
by (auto dest: in_prime_factors_imp_prime)

-
-lemma prime_elem_multiplicity_mult_distrib:
-  assumes "prime_elem p" "x \<noteq> 0" "y \<noteq> 0"
-  shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"
-proof -
-  have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
-    by (subst count_prime_factorization_prime) (simp_all add: assms)
-  also from assms
-    have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
-      by (intro prime_factorization_mult)
-  also have "count \<dots> (normalize p) =
-    count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
-    by simp
-  also have "\<dots> = multiplicity p x + multiplicity p y"
-    by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
-  finally show ?thesis .
-qed
-
-lemma prime_elem_multiplicity_power_distrib:
-  assumes "prime_elem p" "x \<noteq> 0"
-  shows   "multiplicity p (x ^ n) = n * multiplicity p x"
-  by (induction n) (simp_all add: assms prime_elem_multiplicity_mult_distrib)
-
-lemma prime_elem_multiplicity_prod_mset_distrib:
-  assumes "prime_elem p" "0 \<notin># A"
-  shows   "multiplicity p (prod_mset A) = sum_mset (image_mset (multiplicity p) A)"
-  using assms by (induction A) (auto simp: prime_elem_multiplicity_mult_distrib)
-
-lemma prime_elem_multiplicity_setprod_distrib:
-  assumes "prime_elem p" "0 \<notin> f ` A" "finite A"
-  shows   "multiplicity p (setprod f A) = (\<Sum>x\<in>A. multiplicity p (f x))"
-proof -
-  have "multiplicity p (setprod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
-    using assms by (subst setprod_unfold_prod_mset)
-                      multiset.map_comp o_def)
-  also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
-    by (induction A rule: finite_induct) simp_all
-  finally show ?thesis .
-qed
-
-lemma prime_factorsI:
-  "x \<noteq> 0 \<Longrightarrow> prime p \<Longrightarrow> p dvd x \<Longrightarrow> p \<in> prime_factors x"
-  by (auto simp: in_prime_factors_iff)
-
lemma prime_prime_factors:
"prime p \<Longrightarrow> prime_factors p = {p}"
by (drule prime_factorization_prime) simp

-lemma prime_factors_altdef_multiplicity:
-  "prime_factors n = {p. prime p \<and> multiplicity p n > 0}"
-  by (cases "n = 0")
-     (auto simp: prime_multiplicity_gt_zero_iff in_prime_factors_iff)
-
lemma setprod_prime_factors:
assumes "x \<noteq> 0"
shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
@@ -1311,13 +1366,6 @@
finally show ?thesis ..
qed

-(* TODO Move *)
-lemma (in semidom) setprod_zero_iff [simp]:
-  assumes "finite A"
-  shows "setprod f A = 0 \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
-  using assms by (induct A) (auto simp: no_zero_divisors)
-(* END TODO *)
-
lemma prime_factorization_unique'':
assumes S_eq: "S = {p. 0 < f p}"
and "finite S"
@@ -1360,29 +1408,10 @@
qed
qed

-lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
-  by (rule multiplicity_self) auto
-
-lemma multiplicity_prime_power [simp]: "prime_elem p \<Longrightarrow> multiplicity p (p ^ n) = n"
-  by (subst multiplicity_same_power') auto
-
lemma prime_factors_product:
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"

-lemma multiplicity_distinct_prime_power:
-  "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> multiplicity p (q ^ n) = 0"
-  by (subst prime_elem_multiplicity_power_distrib) (auto simp: prime_multiplicity_other)
-
-lemma dvd_imp_multiplicity_le:
-  assumes "a dvd b" "b \<noteq> 0"
-  shows   "multiplicity p a \<le> multiplicity p b"
-proof (cases "is_unit p")
-  case False
-  with assms show ?thesis
-    by (intro multiplicity_geI ) (auto intro: dvd_trans[OF multiplicity_dvd' assms(1)])
-qed (insert assms, auto simp: multiplicity_unit_left)
-
lemma dvd_prime_factors [intro]:
"y \<noteq> 0 \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x \<subseteq> prime_factors y"
by (intro set_mset_mono, subst prime_factorization_subset_iff_dvd) auto
@@ -1402,9 +1431,6 @@
"x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x dvd y \<longleftrightarrow> (\<forall>p. multiplicity p x \<le> multiplicity p y)"
by (auto intro: dvd_imp_multiplicity_le multiplicity_le_imp_dvd)

-lemma prime_factors_altdef: "x \<noteq> 0 \<Longrightarrow> prime_factors x = {p. prime p \<and> p dvd x}"
-  by (auto intro: prime_factorsI)
-
lemma multiplicity_eq_imp_eq:
assumes "x \<noteq> 0" "y \<noteq> 0"
assumes "\<And>p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
@@ -1438,6 +1464,8 @@
qed

+subsection \<open>GCD and LCM computation with unique factorizations\<close>
+
definition "gcd_factorial a b = (if a = 0 then normalize b
else if b = 0 then normalize a
else prod_mset (prime_factorization a \<inter># prime_factorization b))"
@@ -1674,73 +1702,6 @@

end

-lemma (in normalization_semidom) factorial_semiring_altI_aux:
-  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
-  assumes irreducible_imp_prime_elem: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
-  assumes "(x::'a) \<noteq> 0"
-  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
-using \<open>x \<noteq> 0\<close>
-proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
-  case (less a)
-  let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
-  show ?case
-  proof (cases "is_unit a")
-    case True
-    thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
-  next
-    case False
-    show ?thesis
-    proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
-      case False
-      with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
-      hence "prime_elem a" by (rule irreducible_imp_prime_elem)
-      thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
-    next
-      case True
-      then guess b by (elim exE conjE) note b = this
-
-      from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
-      moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
-      hence "?fctrs b \<noteq> ?fctrs a" by blast
-      ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
-      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
-        by (rule psubset_card_mono)
-      moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
-      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize b"
-        by (intro less) auto
-      then guess A .. note A = this
-
-      define c where "c = a div b"
-      from b have c: "a = b * c" by (simp add: c_def)
-      from less.prems c have "c \<noteq> 0" by auto
-      from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
-      moreover have "normalize a \<notin> ?fctrs c"
-      proof safe
-        assume "normalize a dvd c"
-        hence "b * c dvd 1 * c" by (simp add: c)
-        hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
-        with b show False by simp
-      qed
-      with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
-      ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
-      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
-        by (rule psubset_card_mono)
-      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize c"
-        by (intro less) auto
-      then guess B .. note B = this
-
-      from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
-    qed
-  qed
-qed
-
-lemma factorial_semiring_altI:
-  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
-  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
-  shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
-  by intro_classes (rule factorial_semiring_altI_aux[OF assms])
-
-
class factorial_semiring_gcd = factorial_semiring + gcd + Gcd +
assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b"
and     lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b"
@@ -1846,7 +1807,6 @@

end

-
class factorial_ring_gcd = factorial_semiring_gcd + idom
begin
```
```--- a/src/HOL/Power.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Power.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -297,6 +297,25 @@
lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
by (induct n) (auto simp add: is_unit_mult_iff)

+lemma dvd_power_iff:
+  assumes "x \<noteq> 0"
+  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
+proof
+  assume *: "x ^ m dvd x ^ n"
+  {
+    assume "m > n"
+    note *
+    also have "x ^ n = x ^ n * 1" by simp
+    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
+    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
+    finally have "x ^ (m - n) dvd 1"
+      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
+    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
+  }
+  thus "is_unit x \<or> m \<le> n" by force
+qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
+
+
end

context normalization_semidom```
```--- a/src/HOL/Rings.thy	Tue Sep 20 14:51:58 2016 +0200
+++ b/src/HOL/Rings.thy	Sun Sep 18 17:57:55 2016 +0200
@@ -862,6 +862,9 @@
then show "a * b dvd c" by (rule dvdI)
qed

+lemma mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
+  using mult_unit_dvd_iff [of a b c] by (simp add: ac_simps)
+
lemma dvd_mult_unit_iff:
assumes "is_unit b"
shows "a dvd c * b \<longleftrightarrow> a dvd c"
@@ -878,14 +881,18 @@
then show "a dvd c * b" by simp
qed

+lemma dvd_mult_unit_iff': "is_unit b \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd c"
+  using dvd_mult_unit_iff [of b a c] by (simp add: ac_simps)
+
lemma div_unit_dvd_iff: "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)

lemma dvd_div_unit_iff: "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)

-lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
-  dvd_mult_unit_iff dvd_div_unit_iff  (* FIXME consider named_theorems *)
+lemmas unit_dvd_iff = mult_unit_dvd_iff mult_unit_dvd_iff'
+  dvd_mult_unit_iff dvd_mult_unit_iff'
+  div_unit_dvd_iff dvd_div_unit_iff (* FIXME consider named_theorems *)

lemma unit_mult_div_div [simp]: "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
by (erule is_unitE [of _ b]) simp```