# HG changeset patch
# User nipkow
# Date 1579703022 -3600
# Node ID 58ddd7c5c84e9ae63f93536168f6da86be62c5f1
# Parent  e0237f2eb49d487b563a1ad1e8833f78d7422723# Parent  a77a3506548da3122c309fe8d214a21569eaf553
merged

diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -67,7 +67,7 @@
   by (simp add: gcd.simps [of b 0] gcd.simps [of b a])
 
 qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  where "lcm a b = normalize (a * b) div gcd a b"
+  where "lcm a b = normalize (a * b div gcd a b)"
 
 qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment> \<open>Somewhat complicated definition of Lcm that has the advantage of working
     for infinite sets as well\<close>
@@ -106,7 +106,7 @@
     by (induct a b rule: eucl_induct)
       (simp_all add: local.gcd_0 local.gcd_mod)
 next
-  show "lcm a b = normalize (a * b) div gcd a b" for a b
+  show "lcm a b = normalize (a * b div gcd a b)" for a b
     by (fact local.lcm_def)
 qed
 
@@ -234,31 +234,30 @@
         from y have x: "x = y * z" by (simp add: z_def)
         with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
         have normalized_factors_product:
-          "{p. p dvd a * b \<and> normalize p = p} = 
-             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
+          "{p. p dvd a * b \<and> normalize p = p} \<subseteq>
+             (\<lambda>(x,y). normalize (x * y)) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
           for a b
         proof safe
           fix p assume p: "p dvd a * b" "normalize p = p"
           from p(1) obtain x y where xy: "p = x * y" "x dvd a" "y dvd b"
             by (rule dvd_productE)
           define x' y' where "x' = normalize x" and "y' = normalize y"
-          have "p = x' * y'"
-            by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
-          moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" 
-            by (simp_all add: x'_def y'_def)
-          ultimately show "p \<in> (\<lambda>(x, y). x * y) ` 
-            ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
-            by blast
-        qed (auto simp: normalize_mult mult_dvd_mono)
+          have "p = normalize (x' * y')"
+            using p by (simp add: xy x'_def y'_def)
+          moreover have "x' dvd a \<and> normalize x' = x'" and "y' dvd b \<and> normalize y' = y'"
+            using xy by (auto simp: x'_def y'_def)
+          ultimately show "p \<in> (\<lambda>(x, y). normalize (x * y)) `
+              ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" by fast
+        qed
         from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
-        have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
+        have "?fctrs x \<subseteq> (\<lambda>(p,p'). normalize (p * p')) ` (?fctrs y \<times> ?fctrs z)"
           by (subst x) (rule normalized_factors_product)
-        also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
+        moreover have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
           by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
-        hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
+        hence "finite ((\<lambda>(p,p'). normalize (p * p')) ` (?fctrs y \<times> ?fctrs z))"
           by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
              (auto simp: x)
-        finally show ?thesis .
+        ultimately show ?thesis by (rule finite_subset)
       qed
     qed
   next
@@ -566,6 +565,26 @@
 
 end
 
+class normalization_euclidean_semiring_multiplicative =
+  normalization_euclidean_semiring + normalization_semidom_multiplicative
+begin
+
+subclass factorial_semiring_multiplicative ..
+
+end
+
+class field_gcd =
+  field + unique_euclidean_ring + euclidean_ring_gcd + normalization_semidom_multiplicative
+begin
+
+subclass normalization_euclidean_semiring_multiplicative ..
+
+subclass normalization_euclidean_semiring ..
+
+subclass semiring_gcd_mult_normalize ..
+
+end
+
 
 subsection \<open>Typical instances\<close>
 
@@ -603,6 +622,8 @@
     by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
 qed
 
+instance nat :: normalization_euclidean_semiring_multiplicative ..
+
 lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
   unfolding One_nat_def [symmetric] using prime_factorization_1 .
 
@@ -652,4 +673,6 @@
     by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
 qed
 
+instance int :: normalization_euclidean_semiring_multiplicative ..
+
 end
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -35,6 +35,20 @@
 lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
   by (simp add: irreducible_def)
 
+lemma irreducible_mono:
+  assumes irr: "irreducible b" and "a dvd b" "\<not>a dvd 1"
+  shows   "irreducible a"
+proof (rule irreducibleI)
+  fix c d assume "a = c * d"
+  from assms obtain k where [simp]: "b = a * k" by auto
+  from \<open>a = c * d\<close> have "b = c * d * k"
+    by simp
+  hence "c dvd 1 \<or> (d * k) dvd 1"
+    using irreducibleD[OF irr, of c "d * k"] by (auto simp: mult.assoc)
+  thus "c dvd 1 \<or> d dvd 1"
+    by auto
+qed (use assms in \<open>auto simp: irreducible_def\<close>)
+
 definition prime_elem :: "'a \<Rightarrow> bool" where
   "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)"
 
@@ -83,6 +97,82 @@
 
 end
 
+
+lemma (in normalization_semidom) irreducible_cong:
+  assumes "normalize a = normalize b"
+  shows   "irreducible a \<longleftrightarrow> irreducible b"
+proof (cases "a = 0 \<or> a dvd 1")
+  case True
+  hence "\<not>irreducible a" by (auto simp: irreducible_def)
+  from True have "normalize a = 0 \<or> normalize a dvd 1"
+    by auto
+  also note assms
+  finally have "b = 0 \<or> b dvd 1" by simp
+  hence "\<not>irreducible b" by (auto simp: irreducible_def)
+  with \<open>\<not>irreducible a\<close> show ?thesis by simp
+next
+  case False
+  hence b: "b \<noteq> 0" "\<not>is_unit b" using assms
+    by (auto simp: is_unit_normalize[of b])
+  show ?thesis
+  proof
+    assume "irreducible a"
+    thus "irreducible b"
+      by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD2\<close>)
+  next
+    assume "irreducible b"
+    thus "irreducible a"
+      by (rule irreducible_mono) (use assms False b in \<open>auto dest: associatedD1\<close>)
+  qed
+qed
+
+lemma (in normalization_semidom) associatedE1:
+  assumes "normalize a = normalize b"
+  obtains u where "is_unit u" "a = u * b"
+proof (cases "a = 0")
+  case [simp]: False
+  from assms have [simp]: "b \<noteq> 0" by auto
+  show ?thesis
+  proof (rule that)
+    show "is_unit (unit_factor a div unit_factor b)"
+      by auto
+    have "unit_factor a div unit_factor b * b = unit_factor a * (b div unit_factor b)"
+      using \<open>b \<noteq> 0\<close> unit_div_commute unit_div_mult_swap unit_factor_is_unit by metis
+    also have "b div unit_factor b = normalize b" by simp
+    finally show "a = unit_factor a div unit_factor b * b"
+      by (metis assms unit_factor_mult_normalize)
+  qed
+next
+  case [simp]: True
+  hence [simp]: "b = 0"
+    using assms[symmetric] by auto
+  show ?thesis
+    by (intro that[of 1]) auto
+qed
+
+lemma (in normalization_semidom) associatedE2:
+  assumes "normalize a = normalize b"
+  obtains u where "is_unit u" "b = u * a"
+proof -
+  from assms have "normalize b = normalize a"
+    by simp
+  then obtain u where "is_unit u" "b = u * a"
+    by (elim associatedE1)
+  thus ?thesis using that by blast
+qed
+  
+
+(* TODO Move *)
+lemma (in normalization_semidom) normalize_power_normalize:
+  "normalize (normalize x ^ n) = normalize (x ^ n)"
+proof (induction n)
+  case (Suc n)
+  have "normalize (normalize x ^ Suc n) = normalize (x * normalize (normalize x ^ n))"
+    by simp
+  also note Suc.IH
+  finally show ?case by simp
+qed auto
+
 context algebraic_semidom
 begin
 
@@ -506,15 +596,6 @@
   thus ?case by (simp add: B)
 qed
 
-lemma normalize_prod_mset_primes:
-  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
-proof (induction A)
-  case (add p A)
-  hence "prime p" by simp
-  hence "normalize p = p" by simp
-  with add show ?case by (simp add: normalize_mult)
-qed simp_all
-
 lemma prod_mset_dvd_prod_mset_primes_iff:
   assumes "\<And>x. x \<in># A \<Longrightarrow> prime x" "\<And>x. x \<in># B \<Longrightarrow> prime x"
   shows   "prod_mset A dvd prod_mset B \<longleftrightarrow> A \<subseteq># B"
@@ -647,7 +728,7 @@
 
 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> normalize (prod_mset A) = normalize x"
 
 text \<open>Alternative characterization\<close>
 
@@ -655,7 +736,7 @@
   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"
+  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (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)
@@ -683,7 +764,7 @@
       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"
+      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize b"
         by (intro less) auto
       then guess A .. note A = this
 
@@ -702,11 +783,22 @@
       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"
+      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (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)
+      show ?thesis
+      proof (rule exI[of _ "A + B"]; safe)
+        have "normalize (prod_mset (A + B)) =
+                normalize (normalize (prod_mset A) * normalize (prod_mset B))"
+          by simp
+        also have "\<dots> = normalize (b * c)"
+          by (simp only: A B) auto
+        also have "b * c = a"
+          using c by simp
+        finally show "normalize (prod_mset (A + B)) = normalize a" .
+      next
+      qed (use A B in auto)
     qed
   qed
 qed
@@ -724,15 +816,15 @@
 
 lemma prime_factorization_exists':
   assumes "x \<noteq> 0"
-  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "prod_mset A = normalize x"
+  obtains A where "\<And>x. x \<in># A \<Longrightarrow> prime x" "normalize (prod_mset A) = normalize x"
 proof -
   from prime_factorization_exists[OF assms] obtain A
-    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "prod_mset A = normalize x" by blast
+    where A: "\<And>x. x \<in># A \<Longrightarrow> prime_elem x" "normalize (prod_mset A) = normalize x" by blast
   define A' where "A' = image_mset normalize A"
-  have "prod_mset A' = normalize (prod_mset A)"
-    by (simp add: A'_def normalize_prod_mset)
+  have "normalize (prod_mset A') = normalize (prod_mset A)"
+    by (simp add: A'_def normalize_prod_mset_normalize)
   also note A(2)
-  finally have "prod_mset A' = normalize x" by simp
+  finally have "normalize (prod_mset A') = normalize x" by simp
   moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> prime x" by (auto simp: prime_def A'_def)
   ultimately show ?thesis by (intro that[of A']) blast
 qed
@@ -749,9 +841,19 @@
     hence "a \<noteq> 0" "b \<noteq> 0" by blast+
     note nz = \<open>x \<noteq> 0\<close> this
     from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
-    from assms ABC have "irreducible (prod_mset A)" by simp
-    from dvd prod_mset_primes_irreducible_imp_prime[of A B C, OF this ABC(1,3,5)] ABC(2,4,6)
-      show ?thesis by (simp add: normalize_mult [symmetric])
+
+    have "irreducible (prod_mset A)"
+      by (subst irreducible_cong[OF ABC(2)]) fact
+    moreover have "normalize (prod_mset A) dvd
+                     normalize (normalize (prod_mset B) * normalize (prod_mset C))"
+      unfolding ABC using dvd by simp
+    hence "prod_mset A dvd prod_mset B * prod_mset C"
+      unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
+    ultimately have "prod_mset A dvd prod_mset B \<or> prod_mset A dvd prod_mset C"
+      by (intro prod_mset_primes_irreducible_imp_prime) (use ABC in auto)
+    hence "normalize (prod_mset A) dvd normalize (prod_mset B) \<or>
+           normalize (prod_mset A) dvd normalize (prod_mset C)" by simp
+    thus ?thesis unfolding ABC by simp
   qed auto
 qed (insert assms, simp_all add: irreducible_def)
 
@@ -768,7 +870,13 @@
   from nz[THEN prime_factorization_exists'] guess A B . note AB = this
   from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
   from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
-    show ?thesis by (simp add: normalize_power [symmetric])
+    have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp
+  also have "{n. prod_mset A ^ n dvd prod_mset B} =
+             {n. normalize (normalize (prod_mset A) ^ n) dvd normalize (prod_mset B)}"
+    unfolding normalize_power_normalize by simp
+  also have "\<dots> = {n. x ^ n dvd y}"
+    unfolding AB unfolding normalize_power_normalize by simp
+  finally show ?thesis .
 qed
 
 lemma finite_prime_divisors:
@@ -780,8 +888,11 @@
   proof safe
     fix p assume p: "prime p" and dvd: "p dvd x"
     from dvd have "p dvd normalize x" by simp
-    also from A have "normalize x = prod_mset A" by simp
-    finally show "p \<in># A" using p A by (subst (asm) prime_dvd_prod_mset_primes_iff)
+    also from A have "normalize x = normalize (prod_mset A)" by simp
+    finally have "p dvd prod_mset A"
+      by simp
+    thus  "p \<in># A" using p A
+      by (subst (asm) prime_dvd_prod_mset_primes_iff)
   qed
   moreover have "finite (set_mset A)" by simp
   ultimately show ?thesis by (rule finite_subset)
@@ -797,8 +908,9 @@
   from prime_factorization_exists'[OF assms(1)] guess A . note A = this
   moreover from A and assms have "A \<noteq> {#}" by auto
   then obtain x where "x \<in># A" by blast
-  with A(1) have *: "x dvd prod_mset A" "prime x" by (auto simp: dvd_prod_mset)
-  with A have "x dvd a" by simp
+  with A(1) have *: "x dvd normalize (prod_mset A)" "prime x"
+    by (auto simp: dvd_prod_mset)
+  hence "x dvd a" unfolding A by simp
   with * show ?thesis by blast
 qed
 
@@ -808,15 +920,18 @@
 proof (cases "x = 0")
   case False
   from prime_factorization_exists'[OF this] guess A . note A = this
-  from A(1) have "P (unit_factor x * prod_mset A)"
+  from A obtain u where u: "is_unit u" "x = u * prod_mset A"
+    by (elim associatedE2)
+
+  from A(1) have "P (u * prod_mset A)"
   proof (induction A)
     case (add p A)
     from add.prems have "prime p" by simp
-    moreover from add.prems have "P (unit_factor x * prod_mset A)" by (intro add.IH) simp_all
-    ultimately have "P (p * (unit_factor x * prod_mset A))" by (rule assms(3))
+    moreover from add.prems have "P (u * prod_mset A)" by (intro add.IH) simp_all
+    ultimately have "P (p * (u * prod_mset A))" by (rule assms(3))
     thus ?case by (simp add: mult_ac)
-  qed (simp_all add: assms False)
-  with A show ?thesis by simp
+  qed (simp_all add: assms False u)
+  with A u show ?thesis by simp
 qed (simp_all add: assms(1))
 
 lemma no_prime_divisors_imp_unit:
@@ -1213,13 +1328,19 @@
   qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
 qed
 
-lemma prod_mset_prime_factorization:
+lemma prod_mset_prime_factorization_weak:
   assumes "x \<noteq> 0"
-  shows   "prod_mset (prime_factorization x) = normalize x"
+  shows   "normalize (prod_mset (prime_factorization x)) = normalize x"
   using assms
-  by (induction x rule: prime_divisors_induct)
-     (simp_all add: prime_factorization_unit prime_factorization_times_prime
-                    is_unit_normalize normalize_mult)
+proof (induction x rule: prime_divisors_induct)
+  case (factor p x)
+  have "normalize (prod_mset (prime_factorization (p * x))) =
+          normalize (p * normalize (prod_mset (prime_factorization x)))"
+    using factor.prems factor.hyps by (simp add: prime_factorization_times_prime)
+  also have "normalize (prod_mset (prime_factorization x)) = normalize x"
+    by (rule factor.IH) (use factor in auto)
+  finally show ?case by simp
+qed (auto simp: prime_factorization_unit is_unit_normalize)
 
 lemma in_prime_factors_iff:
   "p \<in> prime_factors x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> prime p"
@@ -1287,28 +1408,43 @@
 proof
   assume "prime_factorization x = prime_factorization y"
   hence "prod_mset (prime_factorization x) = prod_mset (prime_factorization y)" by simp
-  with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
+  hence "normalize (prod_mset (prime_factorization x)) =
+         normalize (prod_mset (prime_factorization y))"
+    by (simp only: )
+  with assms show "normalize x = normalize y"
+    by (simp add: prod_mset_prime_factorization_weak)
 qed (rule prime_factorization_cong)
 
-lemma prime_factorization_eqI:
+lemma prime_factorization_normalize [simp]:
+  "prime_factorization (normalize x) = prime_factorization x"
+  by (cases "x = 0", simp, subst prime_factorization_unique) auto
+
+lemma prime_factorization_eqI_strong:
   assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n"
   shows   "prime_factorization n = P"
   using prime_factorization_prod_mset_primes[of P] assms by simp
 
+lemma prime_factorization_eqI:
+  assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "normalize (prod_mset P) = normalize n"
+  shows   "prime_factorization n = P"
+proof -
+  have "P = prime_factorization (normalize (prod_mset P))"
+    using prime_factorization_prod_mset_primes[of P] assms(1) by simp
+  with assms(2) show ?thesis by simp
+qed
+
 lemma prime_factorization_mult:
   assumes "x \<noteq> 0" "y \<noteq> 0"
   shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
 proof -
-  have "prime_factorization (prod_mset (prime_factorization (x * y))) =
-          prime_factorization (prod_mset (prime_factorization x + prime_factorization y))"
-    by (simp add: prod_mset_prime_factorization assms normalize_mult)
-  also have "prime_factorization (prod_mset (prime_factorization (x * y))) =
-               prime_factorization (x * y)"
-    by (rule prime_factorization_prod_mset_primes) (simp_all add: in_prime_factors_imp_prime)
-  also have "prime_factorization (prod_mset (prime_factorization x + prime_factorization y)) =
-               prime_factorization x + prime_factorization y"
-    by (rule prime_factorization_prod_mset_primes) (auto simp: in_prime_factors_imp_prime)
-  finally show ?thesis .
+  have "normalize (prod_mset (prime_factorization x) * prod_mset (prime_factorization y)) =
+          normalize (normalize (prod_mset (prime_factorization x)) *
+                     normalize (prod_mset (prime_factorization y)))"
+    by (simp only: normalize_mult_normalize_left normalize_mult_normalize_right)
+  also have "\<dots> = normalize (x * y)"
+    by (subst (1 2) prod_mset_prime_factorization_weak) (use assms in auto)
+  finally show ?thesis
+    by (intro prime_factorization_eqI) auto
 qed
 
 lemma prime_factorization_prod:
@@ -1367,15 +1503,13 @@
   by (induction n)
      (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
 
-lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
-  by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
-
 lemma prime_factorization_subset_iff_dvd:
   assumes [simp]: "x \<noteq> 0" "y \<noteq> 0"
   shows   "prime_factorization x \<subseteq># prime_factorization y \<longleftrightarrow> x dvd y"
 proof -
-  have "x dvd y \<longleftrightarrow> prod_mset (prime_factorization x) dvd prod_mset (prime_factorization y)"
-    by (simp add: prod_mset_prime_factorization)
+  have "x dvd y \<longleftrightarrow>
+    normalize (prod_mset (prime_factorization x)) dvd normalize (prod_mset (prime_factorization y))"
+    using assms by (subst (1 2) prod_mset_prime_factorization_weak) auto
   also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
     by (auto intro!: prod_mset_primes_dvd_imp_subset prod_mset_subset_imp_dvd)
   finally show ?thesis ..
@@ -1403,63 +1537,6 @@
   "prime p \<Longrightarrow> prime_factors p = {p}"
   by (drule prime_factorization_prime) simp
 
-lemma prod_prime_factors:
-  assumes "x \<noteq> 0"
-  shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
-proof -
-  have "normalize x = prod_mset (prime_factorization x)"
-    by (simp add: prod_mset_prime_factorization assms)
-  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
-    by (subst prod_mset_multiplicity) simp_all
-  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
-    by (intro prod.cong)
-      (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
-  finally show ?thesis ..
-qed
-
-lemma prime_factorization_unique'':
-  assumes S_eq: "S = {p. 0 < f p}"
-    and "finite S"
-    and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
-  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
-proof
-  define A where "A = Abs_multiset f"
-  from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
-  with S(2) have nz: "n \<noteq> 0" by auto
-  from S_eq \<open>finite S\<close> have count_A: "count A = f"
-    unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
-  from S_eq count_A have set_mset_A: "set_mset A = S"
-    by (simp only: set_mset_def)
-  from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
-  also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
-  also from nz have "normalize n = prod_mset (prime_factorization n)"
-    by (simp add: prod_mset_prime_factorization)
-  finally have "prime_factorization (prod_mset A) =
-                  prime_factorization (prod_mset (prime_factorization n))" by simp
-  also from S(1) have "prime_factorization (prod_mset A) = A"
-    by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
-  also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
-    by (intro prime_factorization_prod_mset_primes) auto
-  finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
-
-  show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
-  proof safe
-    fix p :: 'a assume p: "prime p"
-    have "multiplicity p n = multiplicity p (normalize n)" by simp
-    also have "normalize n = prod_mset A"
-      by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
-    also from p set_mset_A S(1)
-    have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
-      by (intro prime_elem_multiplicity_prod_mset_distrib) auto
-    also from S(1) p
-    have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
-      by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
-    also have "sum_mset \<dots> = f p"
-      by (simp add: semiring_1_class.sum_mset_delta' count_A)
-    finally show "f p = multiplicity p n" ..
-  qed
-qed
-
 lemma prime_factors_product:
   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
   by (simp add: prime_factorization_mult)
@@ -1502,6 +1579,20 @@
   finally show ?thesis .
 qed
 
+lemma prime_factorization_unique'':
+  assumes "\<forall>p \<in># M. prime p" "\<forall>p \<in># N. prime p" "normalize (\<Prod>i \<in># M. i) = normalize (\<Prod>i \<in># N. i)"
+  shows   "M = N"
+proof -
+  have "prime_factorization (normalize (\<Prod>i \<in># M. i)) =
+        prime_factorization (normalize (\<Prod>i \<in># N. i))"
+    by (simp only: assms)
+  also from assms have "prime_factorization (normalize (\<Prod>i \<in># M. i)) = M"
+    by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all
+  also from assms have "prime_factorization (normalize (\<Prod>i \<in># N. i)) = N"
+    by (subst prime_factorization_normalize, subst prime_factorization_prod_mset_primes) simp_all
+  finally show ?thesis .
+qed
+
 lemma multiplicity_cong:
   "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
   by (simp add: multiplicity_def)
@@ -1526,26 +1617,30 @@
     with assms[of P] assms[of Q] PQ show "P = Q" by simp
 qed
 
-lemma divides_primepow:
+lemma divides_primepow_weak:
   assumes "prime p" and "a dvd p ^ n"
-  obtains m where "m \<le> n" and "normalize a = p ^ m"
+  obtains m where "m \<le> n" and "normalize a = normalize (p ^ m)"
 proof -
   from assms have "a \<noteq> 0"
     by auto
   with assms
-  have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
-    by (simp add: prod_mset_prime_factorization)
+  have "normalize (prod_mset (prime_factorization a)) dvd
+          normalize (prod_mset (prime_factorization (p ^ n)))"
+    by (subst (1 2) prod_mset_prime_factorization_weak) auto
   then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
     by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
   with assms have "prime_factorization a \<subseteq># replicate_mset n p"
     by (simp add: prime_factorization_prime_power)
   then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
     by (rule msubseteq_replicate_msetE)
-  then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
+  then have *: "normalize (prod_mset (prime_factorization a)) =
+                  normalize (prod_mset (replicate_mset m p))" by metis
+  also have "normalize (prod_mset (prime_factorization a)) = normalize a"
+    using \<open>a \<noteq> 0\<close> by (simp add: prod_mset_prime_factorization_weak)
+  also have "prod_mset (replicate_mset m p) = p ^ m"
     by simp
-  with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
-    by (simp add: prod_mset_prime_factorization)
-  with \<open>m \<le> n\<close> show thesis ..
+  finally show ?thesis using \<open>m \<le> n\<close> 
+    by (intro that[of m])
 qed
 
 lemma divide_out_primepow_ex:
@@ -1568,37 +1663,24 @@
   obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
   using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms
         prime_factorsI by metis
-  
-lemma Ex_other_prime_factor:
-  assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
-  shows   "\<exists>q\<in>prime_factors n. q \<noteq> p"
-proof (rule ccontr)
-  assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
-  have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
-    using assms(1) by (intro prod_prime_factors [symmetric]) auto
-  also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
-    using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
-  finally have "normalize n = p ^ multiplicity p n" by auto
-  with assms show False by auto
-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))"
+     else normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)))"
 
 definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
-     else prod_mset (prime_factorization a \<union># prime_factorization b))"
+     else normalize (prod_mset (prime_factorization a \<union># prime_factorization b)))"
 
 definition "Gcd_factorial A =
-  (if A \<subseteq> {0} then 0 else prod_mset (Inf (prime_factorization ` (A - {0}))))"
+  (if A \<subseteq> {0} then 0 else normalize (prod_mset (Inf (prime_factorization ` (A - {0})))))"
 
 definition "Lcm_factorial A =
   (if A = {} then 1
    else if 0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` (A - {0})) then
-     prod_mset (Sup (prime_factorization ` A))
+     normalize (prod_mset (Sup (prime_factorization ` A)))
    else
      0)"
 
@@ -1672,13 +1754,11 @@
 lemma gcd_factorial_dvd2: "gcd_factorial a b dvd b"
   by (subst gcd_factorial_commute) (rule gcd_factorial_dvd1)
 
-lemma normalize_gcd_factorial: "normalize (gcd_factorial a b) = gcd_factorial a b"
-proof -
-  have "normalize (prod_mset (prime_factorization a \<inter># prime_factorization b)) =
-          prod_mset (prime_factorization a \<inter># prime_factorization b)"
-    by (intro normalize_prod_mset_primes) auto
-  thus ?thesis by (simp add: gcd_factorial_def)
-qed
+lemma normalize_gcd_factorial [simp]: "normalize (gcd_factorial a b) = gcd_factorial a b"
+  by (simp add: gcd_factorial_def)
+
+lemma normalize_lcm_factorial [simp]: "normalize (lcm_factorial a b) = lcm_factorial a b"
+  by (simp add: lcm_factorial_def)
 
 lemma gcd_factorial_greatest: "c dvd gcd_factorial a b" if "c dvd a" "c dvd b" for a b c
 proof (cases "a = 0 \<or> b = 0")
@@ -1695,33 +1775,39 @@
 qed (auto simp: gcd_factorial_def that)
 
 lemma lcm_factorial_gcd_factorial:
-  "lcm_factorial a b = normalize (a * b) div gcd_factorial a b" for a b
+  "lcm_factorial a b = normalize (a * b div gcd_factorial a b)" for a b
 proof (cases "a = 0 \<or> b = 0")
   case False
   let ?p = "prime_factorization"
-  from False have "prod_mset (?p (a * b)) div gcd_factorial a b =
-                     prod_mset (?p a + ?p b - ?p a \<inter># ?p b)"
-    by (subst prod_mset_diff) (auto simp: lcm_factorial_def gcd_factorial_def
-                                prime_factorization_mult subset_mset.le_infI1)
-  also from False have "prod_mset (?p (a * b)) = normalize (a * b)"
-    by (intro prod_mset_prime_factorization) simp_all
-  also from False have "prod_mset (?p a + ?p b - ?p a \<inter># ?p b) = lcm_factorial a b"
-    by (simp add: union_diff_inter_eq_sup lcm_factorial_def)
-  finally show ?thesis ..
+  have 1: "normalize x * normalize y dvd z \<longleftrightarrow> x * y dvd z" for x y z :: 'a
+  proof -
+    have "normalize (normalize x * normalize y) dvd z \<longleftrightarrow> x * y dvd z"
+      unfolding normalize_mult_normalize_left normalize_mult_normalize_right by simp
+    thus ?thesis unfolding normalize_dvd_iff by simp
+  qed
+
+  have "?p (a * b) = (?p a \<union># ?p b) + (?p a \<inter># ?p b)"
+    using False by (subst prime_factorization_mult) (auto intro!: multiset_eqI)
+  hence "normalize (prod_mset (?p (a * b))) =
+           normalize (prod_mset ((?p a \<union># ?p b) + (?p a \<inter># ?p b)))"
+    by (simp only:)
+  hence *: "normalize (a * b) = normalize (lcm_factorial a b * gcd_factorial a b)" using False
+    by (subst (asm) prod_mset_prime_factorization_weak)
+       (auto simp: lcm_factorial_def gcd_factorial_def)
+
+  have [simp]: "gcd_factorial a b dvd a * b" "lcm_factorial a b dvd a * b"
+    using associatedD2[OF *] by auto
+  from False have [simp]: "gcd_factorial a b \<noteq> 0" "lcm_factorial a b \<noteq> 0"
+    by (auto simp: gcd_factorial_def lcm_factorial_def)
+  
+  show ?thesis
+    by (rule associated_eqI)
+       (use * in \<open>auto simp: dvd_div_iff_mult div_dvd_iff_mult dest: associatedD1 associatedD2\<close>)
 qed (auto simp: lcm_factorial_def)
 
 lemma normalize_Gcd_factorial:
   "normalize (Gcd_factorial A) = Gcd_factorial A"
-proof (cases "A \<subseteq> {0}")
-  case False
-  then obtain x where "x \<in> A" "x \<noteq> 0" by blast
-  hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
-    by (intro subset_mset.cInf_lower) auto
-  hence "prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
-    using that by (auto dest: mset_subset_eqD)
-  with False show ?thesis
-    by (auto simp add: Gcd_factorial_def normalize_prod_mset_primes)
-qed (simp_all add: Gcd_factorial_def)
+  by (simp add: Gcd_factorial_def)
 
 lemma Gcd_factorial_eq_0_iff:
   "Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}"
@@ -1761,14 +1847,7 @@
 
 lemma normalize_Lcm_factorial:
   "normalize (Lcm_factorial A) = Lcm_factorial A"
-proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
-  case True
-  hence "normalize (prod_mset (Sup (prime_factorization ` A))) =
-           prod_mset (Sup (prime_factorization ` A))"
-    by (intro normalize_prod_mset_primes)
-       (auto simp: in_Sup_multiset_iff)
-  with True show ?thesis by (simp add: Lcm_factorial_def)
-qed (auto simp: Lcm_factorial_def)
+  by (simp add: Lcm_factorial_def)
 
 lemma Lcm_factorial_eq_0_iff:
   "Lcm_factorial A = 0 \<longleftrightarrow> 0 \<in> A \<or> \<not>subset_mset.bdd_above (prime_factorization ` A)"
@@ -1870,21 +1949,23 @@
 lemma
   assumes "x \<noteq> 0" "y \<noteq> 0"
   shows gcd_eq_factorial':
-          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
+          "gcd x y = normalize (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
                           p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
     and lcm_eq_factorial':
-          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
+          "lcm x y = normalize (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
                           p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
 proof -
   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
   also have "\<dots> = ?rhs1"
     by (auto simp: gcd_factorial_def assms prod_mset_multiplicity
-          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
+          count_prime_factorization_prime
+          intro!: arg_cong[of _ _ normalize] dest: in_prime_factors_imp_prime intro!: prod.cong)
   finally show "gcd x y = ?rhs1" .
   have "lcm x y = lcm_factorial x y" by (rule lcm_eq_lcm_factorial)
   also have "\<dots> = ?rhs2"
     by (auto simp: lcm_factorial_def assms prod_mset_multiplicity
-          count_prime_factorization_prime dest: in_prime_factors_imp_prime intro!: prod.cong)
+          count_prime_factorization_prime intro!: arg_cong[of _ _ normalize] 
+          dest: in_prime_factors_imp_prime intro!: prod.cong)
   finally show "lcm x y = ?rhs2" .
 qed
 
@@ -1944,4 +2025,107 @@
 
 end
 
+
+class factorial_semiring_multiplicative =
+  factorial_semiring + normalization_semidom_multiplicative
+begin
+
+lemma normalize_prod_mset_primes:
+  "(\<And>p. p \<in># A \<Longrightarrow> prime p) \<Longrightarrow> normalize (prod_mset A) = prod_mset A"
+proof (induction A)
+  case (add p A)
+  hence "prime p" by simp
+  hence "normalize p = p" by simp
+  with add show ?case by (simp add: normalize_mult)
+qed simp_all
+
+lemma prod_mset_prime_factorization:
+  assumes "x \<noteq> 0"
+  shows   "prod_mset (prime_factorization x) = normalize x"
+  using assms
+  by (induction x rule: prime_divisors_induct)
+     (simp_all add: prime_factorization_unit prime_factorization_times_prime
+                    is_unit_normalize normalize_mult)
+
+lemma prime_decomposition: "unit_factor x * prod_mset (prime_factorization x) = x"
+  by (cases "x = 0") (simp_all add: prod_mset_prime_factorization)
+
+lemma prod_prime_factors:
+  assumes "x \<noteq> 0"
+  shows   "(\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
+proof -
+  have "normalize x = prod_mset (prime_factorization x)"
+    by (simp add: prod_mset_prime_factorization assms)
+  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
+    by (subst prod_mset_multiplicity) simp_all
+  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
+    by (intro prod.cong)
+      (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
+  finally show ?thesis ..
+qed
+
+lemma prime_factorization_unique'':
+  assumes S_eq: "S = {p. 0 < f p}"
+    and "finite S"
+    and S: "\<forall>p\<in>S. prime p" "normalize n = (\<Prod>p\<in>S. p ^ f p)"
+  shows "S = prime_factors n \<and> (\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
+proof
+  define A where "A = Abs_multiset f"
+  from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
+  with S(2) have nz: "n \<noteq> 0" by auto
+  from S_eq \<open>finite S\<close> have count_A: "count A = f"
+    unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+  from S_eq count_A have set_mset_A: "set_mset A = S"
+    by (simp only: set_mset_def)
+  from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
+  also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
+  also from nz have "normalize n = prod_mset (prime_factorization n)"
+    by (simp add: prod_mset_prime_factorization)
+  finally have "prime_factorization (prod_mset A) =
+                  prime_factorization (prod_mset (prime_factorization n))" by simp
+  also from S(1) have "prime_factorization (prod_mset A) = A"
+    by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
+  also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
+    by (intro prime_factorization_prod_mset_primes) auto
+  finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
+
+  show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
+  proof safe
+    fix p :: 'a assume p: "prime p"
+    have "multiplicity p n = multiplicity p (normalize n)" by simp
+    also have "normalize n = prod_mset A"
+      by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
+    also from p set_mset_A S(1)
+    have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
+      by (intro prime_elem_multiplicity_prod_mset_distrib) auto
+    also from S(1) p
+    have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
+      by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
+    also have "sum_mset \<dots> = f p"
+      by (simp add: semiring_1_class.sum_mset_delta' count_A)
+    finally show "f p = multiplicity p n" ..
+  qed
+qed
+
+lemma divides_primepow:
+  assumes "prime p" and "a dvd p ^ n"
+  obtains m where "m \<le> n" and "normalize a = p ^ m"
+  using divides_primepow_weak[OF assms] that assms
+  by (auto simp add: normalize_power)
+
+lemma Ex_other_prime_factor:
+  assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
+  shows   "\<exists>q\<in>prime_factors n. q \<noteq> p"
+proof (rule ccontr)
+  assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
+  have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
+    using assms(1) by (intro prod_prime_factors [symmetric]) auto
+  also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
+    using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
+  finally have "normalize n = p ^ multiplicity p n" by auto
+  with assms show False by auto
+qed
+
 end
+
+end
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Field_as_Ring.thy
--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -24,7 +24,8 @@
 
 end
 
-instantiation real :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instantiation real ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
@@ -55,7 +56,11 @@
 
 end
 
-instantiation rat :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance real :: field_gcd ..
+
+
+instantiation rat :: 
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
@@ -86,7 +91,11 @@
 
 end
 
-instantiation complex :: "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance rat :: field_gcd ..
+
+
+instantiation complex ::
+  "{unique_euclidean_ring, normalization_euclidean_semiring, normalization_semidom_multiplicative}"
 begin
 
 definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
@@ -117,4 +126,6 @@
 
 end
 
+instance complex :: field_gcd ..
+
 end
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -2906,7 +2906,7 @@
 
 qed (rule fps_divide_times_eq, simp_all add: fps_divide_def)
 
-instantiation fps :: (field) normalization_semidom
+instantiation fps :: (field) normalization_semidom_multiplicative
 begin
 
 definition fps_normalize_def [simp]:
@@ -2914,10 +2914,17 @@
 
 instance proof
   fix f g :: "'a fps"
-  show "unit_factor (f * g) = unit_factor f * unit_factor g"
-    using fps_unit_factor_mult by simp
+  assume "is_unit f"
+  thus "unit_factor (f * g) = f * unit_factor g"
+    using fps_unit_factor_mult[of f g] by simp
+next
+  fix f g :: "'a fps"
   show "unit_factor f * normalize f = f"
     by (simp add: fps_shift_times_fps_X_power)
+next
+  fix f g :: "'a fps"
+  show "unit_factor (f * g) = unit_factor f * unit_factor g"
+    using fps_unit_factor_mult[of f g] by simp
 qed (simp_all add: fps_divide_def Let_def)
 
 end
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -12,7 +12,7 @@
 definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
   "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
 
-definition normalize_quot :: "'a :: {ring_gcd,idom_divide} \<times> 'a \<Rightarrow> 'a \<times> 'a" where
+definition normalize_quot :: "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} \<times> 'a \<Rightarrow> 'a \<times> 'a" where
   "normalize_quot = 
      (\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))" 
 
@@ -118,7 +118,8 @@
   using assms by (subst (1 2) fractrel_iff_normalize_quot_eq) auto
 
   
-lift_definition quot_of_fract :: "'a :: {ring_gcd,idom_divide} fract \<Rightarrow> 'a \<times> 'a" 
+lift_definition quot_of_fract :: 
+  "'a :: {ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract \<Rightarrow> 'a \<times> 'a" 
     is normalize_quot
   by (subst (asm) fractrel_iff_normalize_quot_eq) simp_all
   
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Nth_Powers.thy
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -48,7 +48,7 @@
   by (simp add: One_nat_def [symmetric] del: One_nat_def)
 
 lemma is_nth_power_conv_multiplicity: 
-  fixes x :: "'a :: factorial_semiring"
+  fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}"
   assumes "n > 0"
   shows   "is_nth_power n (normalize x) \<longleftrightarrow> (\<forall>p. prime p \<longrightarrow> n dvd multiplicity p x)"
 proof (cases "x = 0")
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -3445,10 +3445,18 @@
   assume "p \<noteq> 0"
   then show "is_unit (unit_factor p)"
     by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
+next
+  fix a b :: "'a poly" assume "is_unit a" 
+  thus "unit_factor (a * b) = a * unit_factor b"
+    by (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult elim!: is_unit_polyE)
 qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
 
 end
 
+instance poly :: ("{semidom_divide_unit_factor,idom_divide,normalization_semidom_multiplicative}") 
+  normalization_semidom_multiplicative
+  by intro_classes (auto simp: unit_factor_poly_def lead_coeff_mult unit_factor_mult)
+
 lemma normalize_poly_eq_map_poly: "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
 proof -
   have "[:unit_factor (lead_coeff p):] dvd p"
@@ -3489,7 +3497,9 @@
 lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
   by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
 
-lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
+lemma normalize_smult:
+  fixes c :: "'a :: {normalization_semidom_multiplicative, idom_divide}"
+  shows "normalize (smult c p) = smult (normalize c) (normalize p)"
 proof -
   have "smult c p = [:c:] * p" by simp
   also have "normalize \<dots> = smult (normalize c) (normalize p)"
@@ -4488,8 +4498,10 @@
   then show "content p = 1" by simp
 qed auto
 
-lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
-  by (simp add: content_def coeffs_smult Gcd_fin_mult)
+lemma content_smult [simp]:
+  fixes c :: "'a :: {normalization_semidom_multiplicative, semiring_gcd}"
+  shows "content (smult c p) = normalize c * content p"
+  by (simp add: content_def coeffs_smult Gcd_fin_mult normalize_mult)
 
 lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   by (auto simp: content_def simp: poly_eq_iff coeffs_def)
@@ -4528,6 +4540,7 @@
 qed
 
 lemma content_primitive_part [simp]:
+  fixes p :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly"
   assumes "p \<noteq> 0"
   shows "content (primitive_part p) = 1"
 proof -
@@ -4544,7 +4557,7 @@
 qed
 
 lemma content_decompose:
-  obtains p' :: "'a::semiring_gcd poly"
+  obtains p' :: "'a :: {normalization_semidom_multiplicative, semiring_gcd} poly"
   where "p = smult (content p) p'" "content p' = 1"
 proof (cases "p = 0")
   case True
@@ -4581,7 +4594,8 @@
 qed
 
 lemma smult_content_normalize_primitive_part [simp]:
-  "smult (content p) (normalize (primitive_part p)) = normalize p"
+  fixes p :: "'a :: {normalization_semidom_multiplicative, semiring_gcd, idom_divide} poly"
+  shows "smult (content p) (normalize (primitive_part p)) = normalize p"
 proof -
   have "smult (content p) (normalize (primitive_part p)) =
       normalize ([:content p:] * primitive_part p)"
@@ -4623,7 +4637,7 @@
 qed (insert assms, auto)
 
 lemma content_mult:
-  fixes p q :: "'a :: {factorial_semiring, semiring_gcd} poly"
+  fixes p q :: "'a :: {factorial_semiring, semiring_gcd, normalization_semidom_multiplicative} poly"
   shows "content (p * q) = content p * content q"
 proof (cases "p * q = 0")
   case False
@@ -4646,7 +4660,8 @@
 end
 
 lemma primitive_part_mult:
-  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+                       normalization_semidom_multiplicative} poly"
   shows "primitive_part (p * q) = primitive_part p * primitive_part q"
 proof -
   have "primitive_part (p * q) = p * q div [:content (p * q):]"
@@ -4659,7 +4674,8 @@
 qed
 
 lemma primitive_part_smult:
-  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+                     normalization_semidom_multiplicative} poly"
   shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
 proof -
   have "smult a p = [:a:] * p" by simp
@@ -4669,17 +4685,19 @@
 qed  
 
 lemma primitive_part_dvd_primitive_partI [intro]:
-  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide,
+                       normalization_semidom_multiplicative} poly"
   shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
   by (auto elim!: dvdE simp: primitive_part_mult)
 
 lemma content_prod_mset: 
-  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
+  fixes A :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative}
+      poly multiset"
   shows "content (prod_mset A) = prod_mset (image_mset content A)"
   by (induction A) (simp_all add: content_mult mult_ac)
 
 lemma content_prod_eq_1_iff: 
-  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, normalization_semidom_multiplicative} poly"
   shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
 proof safe
   assume A: "content (p * q) = 1"
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -160,7 +160,7 @@
   using fract_poly_dvd[of p 1] by simp
 
 lemma fract_poly_smult_eqE:
-  fixes c :: "'a :: {idom_divide,ring_gcd} fract"
+  fixes c :: "'a :: {idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract"
   assumes "fract_poly p = smult c (fract_poly q)"
   obtains a b 
     where "c = to_fract b / to_fract a" "smult a p = smult b q" "coprime a b" "normalize a = a"
@@ -180,16 +180,16 @@
 subsection \<open>Fractional content\<close>
 
 abbreviation (input) Lcm_coeff_denoms 
-    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} fract poly \<Rightarrow> 'a"
+    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a"
   where "Lcm_coeff_denoms p \<equiv> Lcm (snd ` quot_of_fract ` set (coeffs p))"
   
 definition fract_content :: 
-      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a fract" where
+      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a fract" where
   "fract_content p = 
      (let d = Lcm_coeff_denoms p in Fract (content (unfract_poly (smult (to_fract d) p))) d)" 
 
 definition primitive_part_fract :: 
-      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly \<Rightarrow> 'a poly" where
+      "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} fract poly \<Rightarrow> 'a poly" where
   "primitive_part_fract p = 
      primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
 
@@ -201,7 +201,10 @@
   unfolding fract_content_def Let_def Zero_fract_def
   by (subst eq_fract) (auto simp: Lcm_0_iff map_poly_eq_0_iff)
 
-lemma content_primitive_part_fract [simp]: "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
+lemma content_primitive_part_fract [simp]:
+  fixes p :: "'a :: {semiring_gcd_mult_normalize,
+                     factorial_semiring, ring_gcd, semiring_Gcd,idom_divide} fract poly"
+  shows "p \<noteq> 0 \<Longrightarrow> content (primitive_part_fract p) = 1"
   unfolding primitive_part_fract_def
   by (rule content_primitive_part)
      (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
@@ -256,7 +259,8 @@
 qed
 
 lemma content_decompose_fract:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,
+                     semiring_gcd_mult_normalize} fract poly"
   obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
 proof (cases "p = 0")
   case True
@@ -347,7 +351,8 @@
 qed (auto intro: lift_prime_elem_poly)
 
 lemma fract_poly_dvdD:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,
+                     semiring_gcd_mult_normalize} poly"
   assumes "fract_poly p dvd fract_poly q" "content p = 1"
   shows   "p dvd q"
 proof -
@@ -372,7 +377,7 @@
 begin
 
 interpretation field_poly: 
-  normalization_euclidean_semiring where zero = "0 :: 'a :: field poly"
+  normalization_euclidean_semiring_multiplicative where zero = "0 :: 'a :: field poly"
     and one = 1 and plus = plus and minus = minus
     and times = times
     and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
@@ -392,7 +397,7 @@
     by (simp add: irreducible_dict)
   show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
     by (simp add: prime_elem_dict)
-  show "class.normalization_euclidean_semiring divide plus minus (0 :: 'a poly) times 1
+  show "class.normalization_euclidean_semiring_multiplicative divide plus minus (0 :: 'a poly) times 1
     modulo (\<lambda>p. if p = 0 then 0 else 2 ^ degree p)
     (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)"
   proof (standard, fold dvd_dict)
@@ -407,13 +412,17 @@
     fix p :: "'a poly" assume "p \<noteq> 0"
     then show "is_unit [:lead_coeff p:]"
       by (simp add: is_unit_pCons_iff)
+  next
+    fix a b :: "'a poly" assume "is_unit a"
+    thus "[:lead_coeff (a * b):] = a * [:lead_coeff b:]"
+      by (auto elim!: is_unit_polyE)
   qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
 qed
 
 lemma field_poly_irreducible_imp_prime:
   "prime_elem p" if "irreducible p" for p :: "'a :: field poly"
   using that by (fact field_poly.irreducible_imp_prime_elem)
-
+find_theorems name:prod_mset_prime_factorization
 lemma field_poly_prod_mset_prime_factorization:
   "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
   if "p \<noteq> 0" for p :: "'a :: field poly"
@@ -429,7 +438,7 @@
 subsection \<open>Primality and irreducibility in polynomial rings\<close>
 
 lemma nonconst_poly_irreducible_iff:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "degree p \<noteq> 0"
   shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
 proof safe
@@ -507,7 +516,7 @@
 qed
 
 private lemma irreducible_imp_prime_poly:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "irreducible p"
   shows   "prime_elem p"
 proof (cases "degree p = 0")
@@ -542,7 +551,7 @@
 qed
 
 lemma irreducible_primitive_part_fract:
-  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly"
   assumes "irreducible p"
   shows   "irreducible (primitive_part_fract p)"
 proof -
@@ -561,7 +570,7 @@
 qed
 
 lemma prime_elem_primitive_part_fract:
-  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd,semiring_gcd_mult_normalize} fract poly"
   shows "irreducible p \<Longrightarrow> prime_elem (primitive_part_fract p)"
   by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
 
@@ -583,13 +592,13 @@
   by (rule field_poly_irreducible_imp_prime, rule irreducible_linear_field_poly)
 
 lemma irreducible_linear_poly:
-  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
+  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}"
   shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> irreducible [:a,b:]"
   by (auto intro!: irreducible_linear_field_poly 
            simp:   nonconst_poly_irreducible_iff content_def map_poly_pCons)
 
 lemma prime_elem_linear_poly:
-  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
+  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd,semiring_gcd_mult_normalize}"
   shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
   by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
 
@@ -597,7 +606,7 @@
 subsection \<open>Prime factorisation of polynomials\<close>   
 
 private lemma poly_prime_factorization_exists_content_1:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "p \<noteq> 0" "content p = 1"
   shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
 proof -
@@ -657,19 +666,25 @@
 qed
 
 lemma poly_prime_factorization_exists:
-  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly"
   assumes "p \<noteq> 0"
-  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
+  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> normalize (prod_mset A) = normalize p"
 proof -
   define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
   have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
     by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
   then guess A by (elim exE conjE) note A = this
-  moreover from assms have "prod_mset B = [:content p:]"
-    by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
+  have "normalize (prod_mset (A + B)) = normalize (prod_mset A * normalize (prod_mset B))"
+    by simp
+  also from assms have "normalize (prod_mset B) = normalize [:content p:]"
+    by (simp add: prod_mset_const_poly normalize_const_poly prod_mset_prime_factorization_weak B_def)
+  also have "prod_mset A = normalize (primitive_part p)"
+    using A by simp
+  finally have "normalize (prod_mset (A + B)) = normalize (primitive_part p * [:content p:])"
+    by simp
   moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
     by (auto simp: B_def intro!: lift_prime_elem_poly dest: in_prime_factors_imp_prime)
-  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
+  ultimately show ?thesis using A by (intro exI[of _ "A + B"]) (auto)
 qed
 
 end
@@ -677,10 +692,10 @@
 
 subsection \<open>Typeclass instances\<close>
 
-instance poly :: (factorial_ring_gcd) factorial_semiring
+instance poly :: ("{factorial_ring_gcd,semiring_gcd_mult_normalize}") factorial_semiring
   by standard (rule poly_prime_factorization_exists)  
 
-instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
+instantiation poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") factorial_ring_gcd
 begin
 
 definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
@@ -699,7 +714,10 @@
 
 end
 
-instantiation poly :: ("{field,factorial_ring_gcd}") "{unique_euclidean_ring, normalization_euclidean_semiring}"
+instance poly :: ("{factorial_ring_gcd, semiring_gcd_mult_normalize}") semiring_gcd_mult_normalize ..
+
+instantiation poly :: ("{field,factorial_ring_gcd,semiring_gcd_mult_normalize}")
+   "{unique_euclidean_ring, normalization_euclidean_semiring}"
 begin
 
 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
@@ -724,14 +742,15 @@
 
 end
 
-instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
+instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd,
+                    semiring_gcd_mult_normalize}") euclidean_ring_gcd
   by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard
 
   
 subsection \<open>Polynomial GCD\<close>
 
 lemma gcd_poly_decompose:
-  fixes p q :: "'a :: factorial_ring_gcd poly"
+  fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
   shows "gcd p q = 
            smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
 proof (rule sym, rule gcdI)
@@ -755,7 +774,7 @@
   
 
 lemma gcd_poly_pseudo_mod:
-  fixes p q :: "'a :: factorial_ring_gcd poly"
+  fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
   assumes nz: "q \<noteq> 0" and prim: "content p = 1" "content q = 1"
   shows   "gcd p q = gcd q (primitive_part (pseudo_mod p q))"
 proof -
@@ -834,12 +853,14 @@
   by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
 
 lemma lcm_poly_code [code]: 
-  fixes p q :: "'a :: factorial_ring_gcd poly"
-  shows "lcm p q = normalize (p * q) div gcd p q"
+  fixes p q :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
+  shows "lcm p q = normalize (p * q div gcd p q)"
   by (fact lcm_gcd)
 
-lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
-lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+lemmas Gcd_poly_set_eq_fold [code] =
+  Gcd_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
+lemmas Lcm_poly_set_eq_fold [code] =
+  Lcm_set_eq_fold [where ?'a = "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly"]
 
 text \<open>Example:
   @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/GCD.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -166,7 +166,7 @@
     and gcd_dvd2 [iff]: "gcd a b dvd b"
     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
-    and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
+    and lcm_gcd: "lcm a b = normalize (a * b div gcd a b)"
 begin
 
 lemma gcd_greatest_iff [simp]: "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
@@ -272,211 +272,6 @@
 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   by (fact gcd.right_idem)
 
-lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
-proof (cases "c = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
-    by (auto intro: gcd_greatest)
-  moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
-    by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
-  ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
-    by (auto intro: associated_eqI)
-  then show ?thesis
-    by (simp add: normalize_mult)
-qed
-
-lemma gcd_mult_right: "gcd (a * c) (b * c) = gcd b a * normalize c"
-  using gcd_mult_left [of c a b] by (simp add: ac_simps)
-
-lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
-  by (simp add: gcd_mult_left mult.assoc [symmetric])
-
-lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
-  using mult_gcd_left [of c a b] by (simp add: ac_simps)
-
-lemma dvd_lcm1 [iff]: "a dvd lcm a b"
-proof -
-  have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
-    by (simp add: lcm_gcd normalize_mult div_mult_swap)
-  then show ?thesis
-    by (simp add: lcm_gcd)
-qed
-
-lemma dvd_lcm2 [iff]: "b dvd lcm a b"
-proof -
-  have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
-    by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
-  then show ?thesis
-    by (simp add: lcm_gcd)
-qed
-
-lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
-  by (rule dvd_trans) (assumption, blast)
-
-lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
-  by (rule dvd_trans) (assumption, blast)
-
-lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
-  using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
-
-lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
-  using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
-
-lemma lcm_least:
-  assumes "a dvd c" and "b dvd c"
-  shows "lcm a b dvd c"
-proof (cases "c = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have *: "is_unit (unit_factor c)"
-    by simp
-  show ?thesis
-  proof (cases "gcd a b = 0")
-    case True
-    with assms show ?thesis by simp
-  next
-    case False
-    then have "a \<noteq> 0 \<or> b \<noteq> 0"
-      by simp
-    with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
-      by (simp_all add: mult_dvd_mono)
-    then have "normalize (a * b) dvd gcd (a * c) (b * c)"
-      by (auto intro: gcd_greatest simp add: ac_simps)
-    then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
-      using * by (simp add: dvd_mult_unit_iff)
-    then have "normalize (a * b) dvd gcd a b * c"
-      by (simp add: mult_gcd_right [of a b c])
-    then have "normalize (a * b) div gcd a b dvd c"
-      using False by (simp add: div_dvd_iff_mult ac_simps)
-    then show ?thesis
-      by (simp add: lcm_gcd)
-  qed
-qed
-
-lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
-  by (blast intro!: lcm_least intro: dvd_trans)
-
-lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
-  by (simp add: lcm_gcd dvd_normalize_div)
-
-lemma lcm_0_left [simp]: "lcm 0 a = 0"
-  by (simp add: lcm_gcd)
-
-lemma lcm_0_right [simp]: "lcm a 0 = 0"
-  by (simp add: lcm_gcd)
-
-lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
-  (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  then have "0 dvd lcm a b"
-    by simp
-  then have "0 dvd normalize (a * b) div gcd a b"
-    by (simp add: lcm_gcd)
-  then have "0 * gcd a b dvd normalize (a * b)"
-    using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
-  then have "normalize (a * b) = 0"
-    by simp
-  then show ?Q
-    by simp
-next
-  assume ?Q
-  then show ?P
-    by auto
-qed
-
-lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
-  by (auto intro: associated_eqI)
-
-lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
-  by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
-
-sublocale lcm: abel_semigroup lcm
-proof
-  fix a b c
-  show "lcm a b = lcm b a"
-    by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
-  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
-    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
-    by (auto intro: lcm_least
-      dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
-      dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
-      dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
-      dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
-  then show "lcm (lcm a b) c = lcm a (lcm b c)"
-    by (rule associated_eqI) simp_all
-qed
-
-sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
-proof
-  show "lcm a a = normalize a" for a
-  proof -
-    have "lcm a a dvd a"
-      by (rule lcm_least) simp_all
-    then show ?thesis
-      by (auto intro: associated_eqI)
-  qed
-  show "lcm (normalize a) b = lcm a b" for a b
-    using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
-    by (auto intro: associated_eqI)
-  show "lcm 1 a = normalize a" for a
-    by (rule associated_eqI) simp_all
-qed simp_all
-
-lemma lcm_self: "lcm a a = normalize a"
-  by (fact lcm.idem_normalize)
-
-lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
-  by (fact lcm.left_idem)
-
-lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
-  by (fact lcm.right_idem)
-
-lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
-  by (simp add: lcm_gcd normalize_mult)
-
-lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
-  using gcd_mult_lcm [of a b] by (simp add: ac_simps)
-
-lemma gcd_lcm:
-  assumes "a \<noteq> 0" and "b \<noteq> 0"
-  shows "gcd a b = normalize (a * b) div lcm a b"
-proof -
-  from assms have "lcm a b \<noteq> 0"
-    by (simp add: lcm_eq_0_iff)
-  have "gcd a b * lcm a b = normalize a * normalize b"
-    by simp
-  then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
-    by (simp_all add: normalize_mult)
-  with \<open>lcm a b \<noteq> 0\<close> show ?thesis
-    using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
-qed
-
-lemma lcm_1_left: "lcm 1 a = normalize a"
-  by (fact lcm.top_left_normalize)
-
-lemma lcm_1_right: "lcm a 1 = normalize a"
-  by (fact lcm.top_right_normalize)
-
-lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
-  by (cases "c = 0")
-    (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
-      simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
-
-lemma lcm_mult_right: "lcm (a * c) (b * c) = lcm b a * normalize c"
-  using lcm_mult_left [of c a b] by (simp add: ac_simps)
-
-lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
-  by (simp add: lcm_mult_left mult.assoc [symmetric])
-
-lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
-  using mult_lcm_left [of c a b] by (simp add: ac_simps)
-
 lemma gcdI:
   assumes "c dvd a" and "c dvd b"
     and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
@@ -520,21 +315,199 @@
 lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
   using gcd_proj1_iff [of n m] by (simp add: ac_simps)
 
-lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
-  by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
-
-lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
-proof-
-  have "normalize k * gcd a b = gcd (k * a) (k * b)"
-    by (simp add: gcd_mult_distrib')
-  then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
+lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize (c * gcd a b)"
+proof (cases "c = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have *: "c * gcd a b dvd gcd (c * a) (c * b)"
+    by (auto intro: gcd_greatest)
+  moreover from False * have "gcd (c * a) (c * b) dvd c * gcd a b"
+    by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
+  ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
+    by (auto intro: associated_eqI)
+  then show ?thesis
+    by (simp add: normalize_mult)
+qed
+
+lemma gcd_mult_right: "gcd (a * c) (b * c) = normalize (gcd b a * c)"
+  using gcd_mult_left [of c a b] by (simp add: ac_simps)
+
+lemma dvd_lcm1 [iff]: "a dvd lcm a b"
+  by (metis div_mult_swap dvd_mult2 dvd_normalize_iff dvd_refl gcd_dvd2 lcm_gcd)
+
+lemma dvd_lcm2 [iff]: "b dvd lcm a b"
+  by (metis dvd_div_mult dvd_mult dvd_normalize_iff dvd_refl gcd_dvd1 lcm_gcd)
+
+lemma dvd_lcmI1: "a dvd b \<Longrightarrow> a dvd lcm b c"
+  by (rule dvd_trans) (assumption, blast)
+
+lemma dvd_lcmI2: "a dvd c \<Longrightarrow> a dvd lcm b c"
+  by (rule dvd_trans) (assumption, blast)
+
+lemma lcm_dvdD1: "lcm a b dvd c \<Longrightarrow> a dvd c"
+  using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
+
+lemma lcm_dvdD2: "lcm a b dvd c \<Longrightarrow> b dvd c"
+  using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
+
+lemma lcm_least:
+  assumes "a dvd c" and "b dvd c"
+  shows "lcm a b dvd c"
+proof (cases "c = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have *: "is_unit (unit_factor c)"
+    by simp
+  show ?thesis
+  proof (cases "gcd a b = 0")
+    case True
+    with assms show ?thesis by simp
+  next
+    case False
+    have "a * b dvd normalize (c * gcd a b)"
+      using assms by (subst gcd_mult_left [symmetric]) (auto intro!: gcd_greatest simp: mult_ac)
+    with False have "(a * b div gcd a b) dvd c"
+      by (subst div_dvd_iff_mult) auto
+    thus ?thesis by (simp add: lcm_gcd)
+  qed
+qed
+
+lemma lcm_least_iff [simp]: "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
+  by (blast intro!: lcm_least intro: dvd_trans)
+
+lemma normalize_lcm [simp]: "normalize (lcm a b) = lcm a b"
+  by (simp add: lcm_gcd dvd_normalize_div)
+
+lemma lcm_0_left [simp]: "lcm 0 a = 0"
+  by (simp add: lcm_gcd)
+
+lemma lcm_0_right [simp]: "lcm a 0 = 0"
+  by (simp add: lcm_gcd)
+
+lemma lcm_eq_0_iff: "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+  (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then have "0 dvd lcm a b"
+    by simp
+  also have "lcm a b dvd (a * b)"
     by simp
-  then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
-    by (simp only: ac_simps)
+  finally show ?Q
+    by auto
+next
+  assume ?Q
+  then show ?P
+    by auto
+qed
+
+lemma zero_eq_lcm_iff: "0 = lcm a b \<longleftrightarrow> a = 0 \<or> b = 0"
+  using lcm_eq_0_iff[of a b] by auto
+
+lemma lcm_eq_1_iff [simp]: "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
+  by (auto intro: associated_eqI)
+
+lemma unit_factor_lcm: "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
+  using lcm_eq_0_iff[of a b] by (cases "lcm a b = 0") (auto simp: lcm_gcd)
+
+sublocale lcm: abel_semigroup lcm
+proof
+  fix a b c
+  show "lcm a b = lcm b a"
+    by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
+  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
+    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
+    by (auto intro: lcm_least
+      dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
+      dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
+      dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
+      dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
+  then show "lcm (lcm a b) c = lcm a (lcm b c)"
+    by (rule associated_eqI) simp_all
+qed
+
+sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
+proof
+  show "lcm a a = normalize a" for a
+  proof -
+    have "lcm a a dvd a"
+      by (rule lcm_least) simp_all
+    then show ?thesis
+      by (auto intro: associated_eqI)
+  qed
+  show "lcm (normalize a) b = lcm a b" for a b
+    using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
+    by (auto intro: associated_eqI)
+  show "lcm 1 a = normalize a" for a
+    by (rule associated_eqI) simp_all
+qed simp_all
+
+lemma lcm_self: "lcm a a = normalize a"
+  by (fact lcm.idem_normalize)
+
+lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
+  by (fact lcm.left_idem)
+
+lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
+  by (fact lcm.right_idem)
+
+lemma gcd_lcm:
+  assumes "a \<noteq> 0" and "b \<noteq> 0"
+  shows "gcd a b = normalize (a * b div lcm a b)"
+proof -
+  from assms have [simp]: "a * b div gcd a b \<noteq> 0"
+    by (subst dvd_div_eq_0_iff) auto
+  let ?u = "unit_factor (a * b div gcd a b)"
+  have "gcd a b * normalize (a * b div gcd a b) =
+          gcd a b * ((a * b div gcd a b) * (1 div ?u))"
+    by simp
+  also have "\<dots> = a * b div ?u"
+    by (subst mult.assoc [symmetric]) auto
+  also have "\<dots> dvd a * b"
+    by (subst div_unit_dvd_iff) auto
+  finally have "gcd a b dvd ((a * b) div lcm a b)"
+    by (intro dvd_mult_imp_div) (auto simp: lcm_gcd)
+  moreover have "a * b div lcm a b dvd a" and "a * b div lcm a b dvd b"
+    using assms by (subst div_dvd_iff_mult; simp add: lcm_eq_0_iff mult.commute[of b "lcm a b"])+
+  ultimately have "normalize (gcd a b) = normalize (a * b div lcm a b)"
+    apply -
+    apply (rule associated_eqI)
+    using assms
+    apply (auto simp: div_dvd_iff_mult zero_eq_lcm_iff)
+    done
+  thus ?thesis by simp
+qed
+
+lemma lcm_1_left: "lcm 1 a = normalize a"
+  by (fact lcm.top_left_normalize)
+
+lemma lcm_1_right: "lcm a 1 = normalize a"
+  by (fact lcm.top_right_normalize)
+
+lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize (c * lcm a b)"
+proof (cases "c = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have *: "lcm (c * a) (c * b) dvd c * lcm a b"
+    by (auto intro: lcm_least)
+  moreover have "lcm a b dvd lcm (c * a) (c * b) div c"
+    by (intro lcm_least) (auto intro!: dvd_mult_imp_div simp: mult_ac)
+  hence "c * lcm a b dvd lcm (c * a) (c * b)"
+    using False by (subst (asm) dvd_div_iff_mult) (auto simp: mult_ac intro: dvd_lcmI1)
+  ultimately have "normalize (lcm (c * a) (c * b)) = normalize (c * lcm a b)"
+    by (auto intro: associated_eqI)
   then show ?thesis
-    by simp
+    by (simp add: normalize_mult)
 qed
 
+lemma lcm_mult_right: "lcm (a * c) (b * c) = normalize (lcm b a * c)"
+  using lcm_mult_left [of c a b] by (simp add: ac_simps)
+
 lemma lcm_mult_unit1: "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
   by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
 
@@ -554,30 +527,6 @@
 lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
   by (fact lcm.normalize_right_idem)
 
-lemma gcd_mult_unit1: 
-  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
-proof -
-  have "gcd (b * a) c dvd b"
-    using assms local.dvd_mult_unit_iff by blast
-  then show ?thesis
-    by (rule gcdI) simp_all
-qed
-
-lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
-  using gcd.commute gcd_mult_unit1 by auto
-
-lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
-  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
-
-lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
-  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
-
-lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
-  by (fact gcd.normalize_left_idem)
-
-lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
-  by (fact gcd.normalize_right_idem)
-
 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   by standard (simp_all add: fun_eq_iff ac_simps)
 
@@ -605,18 +554,6 @@
     by (rule dvd_trans)
 qed
 
-lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
-  by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
-
-lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
-  using gcd_add1 [of n m] by (simp add: ac_simps)
-
-lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
-  by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
-
-lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
-  by (simp add: lcm_gcd)
-
 declare unit_factor_lcm [simp]
 
 lemma lcmI:
@@ -636,11 +573,11 @@
 
 lemma lcm_proj1_if_dvd:
   assumes "b dvd a" shows "lcm a b = normalize a"
-proof (cases "a = 0")
-  case False
-  then show ?thesis
-    using assms gcd_proj2_if_dvd lcm_mult_gcd local.lcm_gcd by auto
-qed auto
+proof -
+  have "normalize (lcm a b) = normalize a"
+    by (rule associatedI) (use assms in auto)
+  thus ?thesis by simp
+qed
 
 lemma lcm_proj2_if_dvd: "a dvd b \<Longrightarrow> lcm a b = normalize b"
   using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
@@ -667,21 +604,6 @@
 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 lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
-  by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
-
-lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
-proof-
-  have "normalize k * lcm a b = lcm (k * a) (k * b)"
-    by (simp add: lcm_mult_distrib')
-  then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
-    by simp
-  then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
-    by (simp only: ac_simps)
-  then show ?thesis
-    by simp
-qed
-
 lemma gcd_mono: "a dvd c \<Longrightarrow> b dvd d \<Longrightarrow> gcd a b dvd gcd c d"
   by (simp add: gcd_dvdI1 gcd_dvdI2)
 
@@ -701,12 +623,45 @@
   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)
+  hence "p dvd b * gcd a p" by (subst (asm) gcd_mult_left) auto
   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
 
+lemma gcd_mult_unit1: 
+  assumes "is_unit a" shows "gcd (b * a) c = gcd b c"
+proof -
+  have "gcd (b * a) c dvd b"
+    using assms dvd_mult_unit_iff by blast
+  then show ?thesis
+    by (rule gcdI) simp_all
+qed
+
+lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
+  using gcd.commute gcd_mult_unit1 by auto
+
+lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
+  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
+
+lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
+  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
+
+lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
+  by (fact gcd.normalize_left_idem)
+
+lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
+  by (fact gcd.normalize_right_idem)
+
+lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
+  by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
+
+lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
+  using gcd_add1 [of n m] by (simp add: ac_simps)
+
+lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
+  by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
+
 end
 
 class ring_gcd = comm_ring_1 + semiring_gcd
@@ -831,9 +786,9 @@
 lemma Lcm_Un: "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
 proof -
   have "\<And>d. \<lbrakk>Lcm A dvd d; Lcm B dvd d\<rbrakk> \<Longrightarrow> Lcm (A \<union> B) dvd d"
-    by (meson UnE local.Lcm_least local.dvd_Lcm local.dvd_trans)
+    by (meson UnE Lcm_least dvd_Lcm dvd_trans)
   then show ?thesis
-    by (meson Lcm_subset local.lcm_unique local.normalize_Lcm sup.cobounded1 sup.cobounded2)
+    by (meson Lcm_subset lcm_unique normalize_Lcm sup.cobounded1 sup.cobounded2)
 qed
 
 lemma Gcd_0_iff [simp]: "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
@@ -982,7 +937,7 @@
 lemma dvd_Gcd_iff: "x dvd Gcd A \<longleftrightarrow> (\<forall>y\<in>A. x dvd y)"
   by (blast dest: dvd_GcdD intro: Gcd_greatest)
 
-lemma Gcd_mult: "Gcd ((*) c ` A) = normalize c * Gcd A"
+lemma Gcd_mult: "Gcd ((*) c ` A) = normalize (c * Gcd A)"
 proof (cases "c = 0")
   case True
   then show ?thesis by auto
@@ -993,17 +948,11 @@
        (auto intro!: Gcd_greatest Gcd_dvd simp: mult.commute[of _ c])
   then have "Gcd ((*) c ` A) dvd c * Gcd A"
     by (subst (asm) div_dvd_iff_mult) (auto intro: Gcd_greatest simp: mult_ac)
-  also have "c * Gcd A = (normalize c * Gcd A) * unit_factor c"
-    by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "Gcd ((*) c ` A) dvd \<dots> \<longleftrightarrow> Gcd ((*) c ` A) dvd normalize c * Gcd A"
-    by (simp add: dvd_mult_unit_iff)
-  finally have "Gcd ((*) c ` A) dvd normalize c * Gcd A" .
-  moreover have "normalize c * Gcd A dvd Gcd ((*) c ` A)"
+  moreover have "c * Gcd A dvd Gcd ((*) c ` A)"
     by (intro Gcd_greatest) (auto intro: mult_dvd_mono Gcd_dvd)
-  ultimately have "normalize (Gcd ((*) c ` A)) = normalize (normalize c * Gcd A)"
+  ultimately have "normalize (Gcd ((*) c ` A)) = normalize (c * Gcd A)"
     by (rule associatedI)
-  then show ?thesis
-    by (simp add: normalize_mult)
+  then show ?thesis by simp    
 qed
 
 lemma Lcm_eqI:
@@ -1021,7 +970,7 @@
 
 lemma Lcm_mult:
   assumes "A \<noteq> {}"
-  shows "Lcm ((*) c ` A) = normalize c * Lcm A"
+  shows "Lcm ((*) c ` A) = normalize (c * Lcm A)"
 proof (cases "c = 0")
   case True
   with assms have "(*) c ` A = {0}"
@@ -1041,17 +990,11 @@
       (auto intro!: Lcm_least dvd_Lcm simp: mult.commute[of _ c])
   ultimately have "c * Lcm A dvd Lcm ((*) c ` A)"
     by auto
-  also have "c * Lcm A = (normalize c * Lcm A) * unit_factor c"
-    by (subst unit_factor_mult_normalize [symmetric]) (simp only: mult_ac)
-  also have "\<dots> dvd Lcm ((*) c ` A) \<longleftrightarrow> normalize c * Lcm A dvd Lcm ((*) c ` A)"
-    by (simp add: mult_unit_dvd_iff)
-  finally have "normalize c * Lcm A dvd Lcm ((*) c ` A)" .
-  moreover have "Lcm ((*) c ` A) dvd normalize c * Lcm A"
+  moreover have "Lcm ((*) c ` A) dvd c * Lcm A"
     by (intro Lcm_least) (auto intro: mult_dvd_mono dvd_Lcm)
-  ultimately have "normalize (normalize c * Lcm A) = normalize (Lcm ((*) c ` A))"
+  ultimately have "normalize (c * Lcm A) = normalize (Lcm ((*) c ` A))"
     by (rule associatedI)
-  then show ?thesis
-    by (simp add: normalize_mult)
+  then show ?thesis by simp
 qed
 
 lemma Lcm_no_units: "Lcm A = Lcm (A - {a. is_unit a})"
@@ -1175,23 +1118,11 @@
   by (simp add: Lcm_fin_dvd_iff)
 
 lemma Gcd_fin_mult:
-  "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
-using that proof induct
-  case empty
-  then show ?case
-    by simp
-next
-  case (insert a A)
-  have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
-    by simp
-  also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
-    by (simp add: normalize_mult)
-  finally show ?case
-    using insert by (simp add: gcd_mult_distrib')
-qed
+  "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A)" if "finite A"
+  using that by induction (auto simp: gcd_mult_left)
 
 lemma Lcm_fin_mult:
-  "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
+  "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A)" if "A \<noteq> {}"
 proof (cases "b = 0")
   case True
   moreover from that have "times 0 ` A = {0}"
@@ -1210,19 +1141,8 @@
       by simp
   next
     case True
-    then show ?thesis using that proof (induct A rule: finite_ne_induct)
-      case (singleton a)
-      then show ?case
-        by (simp add: normalize_mult)
-    next
-      case (insert a A)
-      have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
-        by simp
-      also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
-        by (simp add: normalize_mult)
-      finally show ?case
-        using insert by (simp add: lcm_mult_distrib')
-    qed
+    then show ?thesis using that
+      by (induct A rule: finite_ne_induct) (auto simp: lcm_mult_left)
   qed
 qed
 
@@ -1413,9 +1333,9 @@
     case False
     then have unit: "is_unit (unit_factor b)"
       by simp
-    from \<open>coprime a c\<close> mult_gcd_left [of b a c]
+    from \<open>coprime a c\<close>
     have "gcd (b * a) (b * c) * unit_factor b = b"
-      by (simp add: ac_simps)
+      by (subst gcd_mult_left) (simp add: ac_simps)
     moreover from \<open>a dvd b * c\<close>
     have "a dvd gcd (b * a) (b * c) * unit_factor b"
       by (simp add: dvd_mult_unit_iff unit)
@@ -1479,9 +1399,9 @@
     by simp
   with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
   also from assms have "a div gcd a b = a'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
+    using dvd_div_eq_mult gcd_dvd1 by blast
   also from assms have "b div gcd a b = b'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
+    using dvd_div_eq_mult gcd_dvd1 by blast
   finally show ?thesis .
 qed
 
@@ -1574,24 +1494,6 @@
   ultimately show ?rhs ..
 qed
 
-lemma coprime_crossproduct':
-  fixes a b c d
-  assumes "b \<noteq> 0"
-  assumes unit_factors: "unit_factor b = unit_factor d"
-  assumes coprime: "coprime a b" "coprime c d"
-  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
-  assume eq: "a * d = b * c"
-  hence "normalize a * normalize d = normalize c * normalize b"
-    by (simp only: normalize_mult [symmetric] mult_ac)
-  with coprime have "normalize b = normalize d"
-    by (subst (asm) coprime_crossproduct) simp_all
-  from this and unit_factors show "b = d"
-    by (rule normalize_unit_factor_eqI)
-  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
-  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
 lemma gcd_mult_left_left_cancel:
   "gcd (c * a) b = gcd a b" if "coprime b c"
 proof -
@@ -1619,8 +1521,8 @@
   using that gcd_mult_right_left_cancel [of a c b]
   by (simp add: ac_simps)
 
-lemma gcd_exp [simp]:
-  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+lemma gcd_exp_weak:
+  "gcd (a ^ n) (b ^ n) = normalize (gcd a b ^ n)"
 proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
   case True
   then show ?thesis
@@ -1633,11 +1535,10 @@
     by simp
   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
     by simp
-  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+  then have "normalize (gcd a b ^ n) = normalize (gcd a b ^ n * \<dots>)"
     by simp
-  also note gcd_mult_distrib
-  also have "unit_factor (gcd a b ^ n) = 1"
-    using False by (auto simp: unit_factor_power unit_factor_gcd)
+  also have "\<dots> = gcd (gcd a b ^ n * (a div gcd a b) ^ n) (gcd a b ^ n * (b div gcd a b) ^ n)"
+    by (rule gcd_mult_left [symmetric])
   also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
     by (simp add: ac_simps div_power dvd_power_same)
   also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
@@ -1737,6 +1638,87 @@
 end
 
 
+subsection \<open>GCD and LCM for multiplicative normalisation functions\<close>
+
+class semiring_gcd_mult_normalize = semiring_gcd + normalization_semidom_multiplicative
+begin
+
+lemma mult_gcd_left: "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
+  by (simp add: gcd_mult_left normalize_mult mult.assoc [symmetric])
+
+lemma mult_gcd_right: "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
+  using mult_gcd_left [of c a b] by (simp add: ac_simps)
+
+lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
+  by (subst gcd_mult_left) (simp_all add: normalize_mult)
+
+lemma gcd_mult_distrib: "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
+proof-
+  have "normalize k * gcd a b = gcd (k * a) (k * b)"
+    by (simp add: gcd_mult_distrib')
+  then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
+    by simp
+  then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
+    by (simp only: ac_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
+  by (simp add: lcm_gcd normalize_mult dvd_normalize_div)
+
+lemma lcm_mult_gcd [simp]: "lcm a b * gcd a b = normalize a * normalize b"
+  using gcd_mult_lcm [of a b] by (simp add: ac_simps)
+
+lemma mult_lcm_left: "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
+  by (simp add: lcm_mult_left mult.assoc [symmetric] normalize_mult)
+
+lemma mult_lcm_right: "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
+  using mult_lcm_left [of c a b] by (simp add: ac_simps)
+
+lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
+  by (simp add: lcm_gcd dvd_normalize_div normalize_mult)
+
+lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
+  by (subst lcm_mult_left) (simp add: normalize_mult)
+
+lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+proof-
+  have "normalize k * lcm a b = lcm (k * a) (k * b)"
+    by (simp add: lcm_mult_distrib')
+  then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
+    by simp
+  then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
+    by (simp only: ac_simps)
+  then show ?thesis
+    by simp
+qed
+
+lemma coprime_crossproduct':
+  fixes a b c d
+  assumes "b \<noteq> 0"
+  assumes unit_factors: "unit_factor b = unit_factor d"
+  assumes coprime: "coprime a b" "coprime c d"
+  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+  assume eq: "a * d = b * c"
+  hence "normalize a * normalize d = normalize c * normalize b"
+    by (simp only: normalize_mult [symmetric] mult_ac)
+  with coprime have "normalize b = normalize d"
+    by (subst (asm) coprime_crossproduct) simp_all
+  from this and unit_factors show "b = d"
+    by (rule normalize_unit_factor_eqI)
+  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
+lemma gcd_exp [simp]:
+  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+  using gcd_exp_weak[of a n b] by (simp add: normalize_power)
+
+end
+
+
 subsection \<open>GCD and LCM on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close>
 
 instantiation nat :: gcd
@@ -1946,13 +1928,13 @@
 instance int :: ring_gcd
 proof
   fix k l r :: int
-  show "gcd k l dvd k" "gcd k l dvd l"
+  show [simp]: "gcd k l dvd k" "gcd k l dvd l"
     using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
       gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
     by simp_all
-  show "lcm k l = normalize (k * l) div gcd k l"
+  show "lcm k l = normalize (k * l div gcd k l)"
     using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
-    by (simp add: nat_eq_iff of_nat_div abs_mult)
+    by (simp add: nat_eq_iff of_nat_div abs_mult abs_div)
   assume "r dvd k" "r dvd l"
   then show "r dvd gcd k l"
     using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
@@ -2010,15 +1992,11 @@
 lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
   for k m n :: nat
   \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
-proof (induct m n rule: gcd_nat_induct)
-  case (step m n)
-  then show ?case
-    by (metis gcd_mult_distrib' gcd_red_nat)
-qed auto
+  by (simp add: gcd_mult_left)
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   for k m n :: int
-  using gcd_mult_distrib' [of k m n] by simp
+  by (simp add: gcd_mult_left abs_mult)
 
 text \<open>\medskip Addition laws.\<close>
 
@@ -2400,15 +2378,15 @@
 
 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   for a b :: int
-  by (simp add: abs_mult lcm_gcd)
+  by (simp add: abs_mult lcm_gcd abs_div)
   
 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
   for m n :: nat
-  by simp
+  by (simp add: lcm_gcd)
 
 lemma prod_gcd_lcm_int: "\<bar>m\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   for m n :: int
-  by simp
+  by (simp add: lcm_gcd abs_div abs_mult)
 
 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
   for m n :: nat
@@ -2553,6 +2531,9 @@
   for N :: "nat set"
   by (rule Gcd_eq_1_I) auto
 
+instance nat :: semiring_gcd_mult_normalize
+  by intro_classes (auto simp: unit_factor_nat_def)
+
 
 text \<open>Alternative characterizations of Gcd:\<close>
 
@@ -2695,7 +2676,10 @@
       by (rule Lcm_least) (use that in auto)
     then show ?thesis by simp
   qed
-qed simp_all
+qed (simp_all add: sgn_mult)
+
+instance int :: semiring_gcd_mult_normalize
+  by intro_classes (auto simp: sgn_mult)
 
 
 subsection \<open>GCD and LCM on \<^typ>\<open>integer\<close>\<close>
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -2495,15 +2495,26 @@
   shows "prod_mset (A - {#a#}) = prod_mset A div a"
   using assms prod_mset_diff [of "{#a#}" A] by auto
 
+lemma (in normalization_semidom) normalize_prod_mset_normalize:
+  "normalize (prod_mset (image_mset normalize A)) = normalize (prod_mset A)"
+proof (induction A)
+  case (add x A)
+  have "normalize (prod_mset (image_mset normalize (add_mset x A))) =
+          normalize (x * normalize (prod_mset (image_mset normalize A)))"
+    by simp
+  also note add.IH
+  finally show ?case by simp
+qed 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:
+lemma (in normalization_semidom_multiplicative) 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:
+lemma (in normalization_semidom_multiplicative) normalized_prod_msetI:
   assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
   shows "normalize (prod_mset A) = prod_mset A"
 proof -
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Number_Theory/Prime_Powers.thy
--- a/src/HOL/Number_Theory/Prime_Powers.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Number_Theory/Prime_Powers.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -95,6 +95,7 @@
   by (auto simp: primepow_def aprimedivisor_prime_power prime_factorization_prime_power)
 
 lemma primepow_decompose:
+  fixes n :: "'a :: factorial_semiring_multiplicative"
   assumes "primepow n"
   shows   "aprimedivisor n ^ multiplicity (aprimedivisor n) n = n"
 proof -
@@ -133,11 +134,13 @@
 lemma primepow_gt_0_nat: "primepow n \<Longrightarrow> n > (0::nat)"
   using primepow_gt_Suc_0[of n] by simp
 
-lemma unit_factor_primepow: "primepow p \<Longrightarrow> unit_factor p = 1"
+lemma unit_factor_primepow:
+  fixes p :: "'a :: factorial_semiring_multiplicative"
+  shows "primepow p \<Longrightarrow> unit_factor p = 1"
   by (auto simp: primepow_def unit_factor_power)
 
 lemma aprimedivisor_primepow:
-  assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring)"
+  assumes "prime p" "p dvd n" "primepow (n :: 'a :: factorial_semiring_multiplicative)"
   shows   "aprimedivisor (p * n) = p" "aprimedivisor n = p"
 proof -
   from assms have [simp]: "n \<noteq> 0" by auto
@@ -187,8 +190,9 @@
   
 
 lemma primepow_power_iff:
+  fixes p :: "'a :: factorial_semiring_multiplicative"
   assumes "unit_factor p = 1"
-  shows   "primepow (p ^ n) \<longleftrightarrow> primepow (p :: 'a :: factorial_semiring) \<and> n > 0"
+  shows   "primepow (p ^ n) \<longleftrightarrow> primepow p \<and> n > 0"
 proof safe
   assume "primepow (p ^ n)"
   hence n: "n \<noteq> 0" by (auto intro!: Nat.gr0I)
@@ -218,11 +222,11 @@
   by (auto simp: primepow_def intro!: exI[of _ n] exI[of _ "1::nat"])
 
 lemma primepow_prime_power [simp]: 
-    "prime (p :: 'a :: factorial_semiring) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
+    "prime (p :: 'a :: factorial_semiring_multiplicative) \<Longrightarrow> primepow (p ^ n) \<longleftrightarrow> n > 0"
   by (subst primepow_power_iff) auto
 
 lemma aprimedivisor_vimage:
-  assumes "prime (p :: 'a :: factorial_semiring)"
+  assumes "prime (p :: 'a :: factorial_semiring_multiplicative)"
   shows   "aprimedivisor -` {p} \<inter> primepow_factors n = {p ^ k |k. k > 0 \<and> p ^ k dvd n}"
 proof safe
   fix q assume q: "q \<in> primepow_factors n"
@@ -267,7 +271,7 @@
 qed
 
 lemma bij_betw_primepows: 
-  "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring) 
+  "bij_betw (\<lambda>(p,k). p ^ Suc k :: 'a :: factorial_semiring_multiplicative) 
      (Collect prime \<times> UNIV) (Collect primepow)"
 proof (rule bij_betwI [where ?g = "(\<lambda>n. (aprimedivisor n, multiplicity (aprimedivisor n) n - 1))"], 
        goal_cases)
@@ -310,14 +314,14 @@
 qed
 
 lemma primepow_mult_aprimedivisorI:
-  assumes "primepow (n :: 'a :: factorial_semiring)"
+  assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
   shows   "primepow (aprimedivisor n * n)"
   by (subst (2) primepow_decompose[OF assms, symmetric], subst power_Suc [symmetric],
       subst primepow_prime_power) 
      (insert assms, auto intro!: prime_aprimedivisor' dest: primepow_gt_Suc_0)
  
 lemma primepow_factors_altdef:
-  fixes x :: "'a :: factorial_semiring"
+  fixes x :: "'a :: factorial_semiring_multiplicative"
   assumes "x \<noteq> 0"
   shows "primepow_factors x = {p ^ k |p k. p \<in> prime_factors x \<and> k \<in> {0<.. multiplicity p x}}"
 proof (intro equalityI subsetI)
@@ -330,7 +334,7 @@
 qed (auto simp: primepow_factors_def prime_factors_multiplicity multiplicity_dvd')
 
 lemma finite_primepow_factors:
-  assumes "x \<noteq> (0 :: 'a :: factorial_semiring)"
+  assumes "x \<noteq> (0 :: 'a :: factorial_semiring_multiplicative)"
   shows   "finite (primepow_factors x)"
 proof -
   have "finite (SIGMA p:prime_factors x. {0<..multiplicity p x})"
@@ -342,7 +346,7 @@
 qed
 
 lemma aprimedivisor_primepow_factors_conv_prime_factorization:
-  assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring)"
+  assumes [simp]: "n \<noteq> (0 :: 'a :: factorial_semiring_multiplicative)"
   shows   "image_mset aprimedivisor (mset_set (primepow_factors n)) = prime_factorization n" 
           (is "?lhs = ?rhs")
 proof (intro multiset_eqI)
@@ -403,6 +407,7 @@
   using assms by (auto simp: primepow_def dest!: prime_dvd_power[rotated] dest: primes_dvd_imp_eq)
 
 lemma sum_prime_factorization_conv_sum_primepow_factors:
+  fixes n :: "'a :: factorial_semiring_multiplicative"
   assumes "n \<noteq> 0"
   shows "(\<Sum>q\<in>primepow_factors n. f (aprimedivisor q)) = (\<Sum>p\<in>#prime_factorization n. f p)"
 proof -
@@ -414,7 +419,7 @@
 qed    
 
 lemma multiplicity_aprimedivisor_Suc_0_iff:
-  assumes "primepow (n :: 'a :: factorial_semiring)"
+  assumes "primepow (n :: 'a :: factorial_semiring_multiplicative)"
   shows   "multiplicity (aprimedivisor n) n = Suc 0 \<longleftrightarrow> prime n"
   by (subst (3) primepow_decompose [OF assms, symmetric])
      (insert assms, auto simp add: prime_power_iff intro!: prime_aprimedivisor')
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Power.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -377,7 +377,7 @@
 
 end
 
-context normalization_semidom
+context normalization_semidom_multiplicative
 begin
 
 lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"
diff -r a77a3506548d -r 58ddd7c5c84e src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Jan 22 14:37:23 2020 +0100
+++ b/src/HOL/Rings.thy	Wed Jan 22 15:23:42 2020 +0100
@@ -1290,9 +1290,17 @@
   assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
     and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
     and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
-    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+    and unit_factor_mult_unit_left: "a dvd 1 \<Longrightarrow> unit_factor (a * b) = a * unit_factor b"
   \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
-  
+begin
+
+lemma unit_factor_mult_unit_right: "a dvd 1 \<Longrightarrow> unit_factor (b * a) = unit_factor b * a"
+  using unit_factor_mult_unit_left[of a b] by (simp add: mult_ac)
+
+lemmas [simp] = unit_factor_mult_unit_left unit_factor_mult_unit_right
+
+end
+
 class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
   fixes normalize :: "'a \<Rightarrow> 'a"
   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
@@ -1434,47 +1442,41 @@
   then show ?lhs by simp
 qed
 
-lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
-proof (cases "a = 0 \<or> b = 0")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  have "unit_factor (a * b) * normalize (a * b) = a * b"
-    by (rule unit_factor_mult_normalize)
-  then have "normalize (a * b) = a * b div unit_factor (a * b)"
-    by simp
-  also have "\<dots> = a * b div unit_factor (b * a)"
-    by (simp add: ac_simps)
-  also have "\<dots> = a * b div unit_factor b div unit_factor a"
-    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
-  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
-    using False by (subst unit_div_mult_swap) simp_all
-  also have "\<dots> = normalize a * normalize b"
-    using False
-    by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
-  finally show ?thesis .
-qed
-
 lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a"
   by (cases "a = 0") (auto intro: is_unit_unit_factor)
 
 lemma normalize_unit_factor [simp]: "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
   by (rule is_unit_normalize) simp
 
+lemma normalize_mult_unit_left [simp]:
+  assumes "a dvd 1"
+  shows   "normalize (a * b) = normalize b"
+proof (cases "b = 0")
+  case False
+  have "a * unit_factor b * normalize (a * b) = unit_factor (a * b) * normalize (a * b)"
+    using assms by (subst unit_factor_mult_unit_left) auto
+  also have "\<dots> = a * b" by simp
+  also have "b = unit_factor b * normalize b" by simp
+  hence "a * b = a * unit_factor b * normalize b"
+    by (simp only: mult_ac)
+  finally show ?thesis
+    using assms False by auto
+qed auto
+
+lemma normalize_mult_unit_right [simp]:
+  assumes "b dvd 1"
+  shows   "normalize (a * b) = normalize a"
+  using assms by (subst mult.commute) auto
+
 lemma normalize_idem [simp]: "normalize (normalize a) = normalize a"
 proof (cases "a = 0")
-  case True
-  then show ?thesis by simp
-next
   case False
   have "normalize a = normalize (unit_factor a * normalize a)"
     by simp
-  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
-    by (simp only: normalize_mult)
-  finally show ?thesis
-    using False by simp_all
-qed
+  also from False have "\<dots> = normalize (normalize a)"
+    by (subst normalize_mult_unit_left) auto
+  finally show ?thesis ..
+qed auto
 
 lemma unit_factor_normalize [simp]:
   assumes "a \<noteq> 0"
@@ -1492,30 +1494,6 @@
     by simp
 qed
 
-lemma dvd_unit_factor_div:
-  assumes "b dvd a"
-  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
-proof -
-  from assms have "a = a div b * b"
-    by simp
-  then have "unit_factor a = unit_factor (a div b * b)"
-    by simp
-  then show ?thesis
-    by (cases "b = 0") (simp_all add: unit_factor_mult)
-qed
-
-lemma dvd_normalize_div:
-  assumes "b dvd a"
-  shows "normalize (a div b) = normalize a div normalize b"
-proof -
-  from assms have "a = a div b * b"
-    by simp
-  then have "normalize a = normalize (a div b * b)"
-    by simp
-  then show ?thesis
-    by (cases "b = 0") (simp_all add: normalize_mult)
-qed
-
 lemma normalize_dvd_iff [simp]: "normalize a dvd b \<longleftrightarrow> a dvd b"
 proof -
   have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
@@ -1582,7 +1560,7 @@
   then have "is_unit c" and "is_unit d"
     by auto
   with a b show ?thesis
-    by (simp add: normalize_mult is_unit_normalize)
+    by (simp add: is_unit_normalize)
 qed
 
 lemma associatedD1: "normalize a = normalize b \<Longrightarrow> a dvd b"
@@ -1643,9 +1621,70 @@
     by simp
 qed
 
+lemma normalize_mult_normalize_left [simp]: "normalize (normalize a * b) = normalize (a * b)"
+  by (rule associated_eqI) (auto intro!: mult_dvd_mono)
+
+lemma normalize_mult_normalize_right [simp]: "normalize (a * normalize b) = normalize (a * b)"
+  by (rule associated_eqI) (auto intro!: mult_dvd_mono)
+
 end
 
 
+class normalization_semidom_multiplicative = normalization_semidom +
+  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+begin
+
+lemma normalize_mult: "normalize (a * b) = normalize a * normalize b"
+proof (cases "a = 0 \<or> b = 0")
+  case True
+  then show ?thesis by auto
+next
+  case False
+  have "unit_factor (a * b) * normalize (a * b) = a * b"
+    by (rule unit_factor_mult_normalize)
+  then have "normalize (a * b) = a * b div unit_factor (a * b)"
+    by simp
+  also have "\<dots> = a * b div unit_factor (b * a)"
+    by (simp add: ac_simps)
+  also have "\<dots> = a * b div unit_factor b div unit_factor a"
+    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
+  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
+    using False by (subst unit_div_mult_swap) simp_all
+  also have "\<dots> = normalize a * normalize b"
+    using False
+    by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
+  finally show ?thesis .
+qed
+
+lemma dvd_unit_factor_div:
+  assumes "b dvd a"
+  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
+proof -
+  from assms have "a = a div b * b"
+    by simp
+  then have "unit_factor a = unit_factor (a div b * b)"
+    by simp
+  then show ?thesis
+    by (cases "b = 0") (simp_all add: unit_factor_mult)
+qed
+
+lemma dvd_normalize_div:
+  assumes "b dvd a"
+  shows "normalize (a div b) = normalize a div normalize b"
+proof -
+  from assms have "a = a div b * b"
+    by simp
+  then have "normalize a = normalize (a div b * b)"
+    by simp
+  then show ?thesis
+    by (cases "b = 0") (simp_all add: normalize_mult)
+qed
+
+end
+
+
+
+
 text \<open>Syntactic division remainder operator\<close>
 
 class modulo = dvd + divide +