# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1468417612 -7200
# Node ID a3fe3250d05d9c9292ecc7407e1533e03510e66f
# Parent  58ccbc73a172c722f96934947d5c46e7d288ea72
Reformed factorial rings

diff -r 58ccbc73a172 -r a3fe3250d05d src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/Library/Polynomial.thy	Wed Jul 13 15:46:52 2016 +0200
@@ -880,21 +880,21 @@
   by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
 
 lemma degree_smult_eq [simp]:
-  fixes a :: "'a::idom"
+  fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
   shows "degree (smult a p) = (if a = 0 then 0 else degree p)"
   by (cases "a = 0", simp, simp add: degree_def)
 
 lemma smult_eq_0_iff [simp]:
-  fixes a :: "'a::idom"
+  fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
   shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0"
   by (simp add: poly_eq_iff)
   
 lemma coeffs_smult [code abstract]:
-  fixes p :: "'a::idom poly"
+  fixes p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
   by (rule coeffs_eqI)
     (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq)
-
+   
 instantiation poly :: (comm_semiring_0) comm_semiring_0
 begin
 
@@ -947,6 +947,24 @@
 
 end
 
+lemma coeff_mult_degree_sum:
+  "coeff (p * q) (degree p + degree q) =
+   coeff p (degree p) * coeff q (degree q)"
+  by (induct p, simp, simp add: coeff_eq_0)
+
+instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors
+proof
+  fix p q :: "'a poly"
+  assume "p \<noteq> 0" and "q \<noteq> 0"
+  have "coeff (p * q) (degree p + degree q) =
+        coeff p (degree p) * coeff q (degree q)"
+    by (rule coeff_mult_degree_sum)
+  also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
+    using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp
+  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
+  thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
+qed
+
 instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
 
 lemma coeff_mult:
@@ -984,10 +1002,14 @@
 
 end
 
+instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
+
 instance poly :: (comm_ring) comm_ring ..
 
 instance poly :: (comm_ring_1) comm_ring_1 ..
 
+instance poly :: (comm_ring_1) comm_semiring_1_cancel ..
+
 lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
   unfolding one_poly_def
   by (simp add: coeff_pCons split: nat.split)
@@ -1106,56 +1128,67 @@
 
 subsection \<open>Polynomials form an integral domain\<close>
 
-lemma coeff_mult_degree_sum:
-  "coeff (p * q) (degree p + degree q) =
-   coeff p (degree p) * coeff q (degree q)"
-  by (induct p, simp, simp add: coeff_eq_0)
-
-instance poly :: (idom) idom
-proof
-  fix p q :: "'a poly"
-  assume "p \<noteq> 0" and "q \<noteq> 0"
-  have "coeff (p * q) (degree p + degree q) =
-        coeff p (degree p) * coeff q (degree q)"
-    by (rule coeff_mult_degree_sum)
-  also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
-    using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp
-  finally have "\<exists>n. coeff (p * q) n \<noteq> 0" ..
-  thus "p * q \<noteq> 0" by (simp add: poly_eq_iff)
-qed
+instance poly :: (idom) idom ..
 
 lemma degree_mult_eq:
-  fixes p q :: "'a::semidom poly"
+  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   shows "\<lbrakk>p \<noteq> 0; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree (p * q) = degree p + degree q"
 apply (rule order_antisym [OF degree_mult_le le_degree])
 apply (simp add: coeff_mult_degree_sum)
 done
 
 lemma degree_mult_right_le:
-  fixes p q :: "'a::semidom poly"
+  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   assumes "q \<noteq> 0"
   shows "degree p \<le> degree (p * q)"
   using assms by (cases "p = 0") (simp_all add: degree_mult_eq)
 
 lemma coeff_degree_mult:
-  fixes p q :: "'a::semidom poly"
+  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   shows "coeff (p * q) (degree (p * q)) =
     coeff q (degree q) * coeff p (degree p)"
   by (cases "p = 0 \<or> q = 0") (auto simp add: degree_mult_eq coeff_mult_degree_sum mult_ac)
 
 lemma dvd_imp_degree_le:
-  fixes p q :: "'a::semidom poly"
+  fixes p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
   shows "\<lbrakk>p dvd q; q \<noteq> 0\<rbrakk> \<Longrightarrow> degree p \<le> degree q"
   by (erule dvdE, hypsubst, subst degree_mult_eq) auto
 
 lemma divides_degree:
-  assumes pq: "p dvd (q :: 'a :: semidom poly)"
+  assumes pq: "p dvd (q :: 'a ::{comm_semiring_1,semiring_no_zero_divisors} poly)"
   shows "degree p \<le> degree q \<or> q = 0"
   by (metis dvd_imp_degree_le pq)
+  
+lemma const_poly_dvd_iff:
+  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
+  shows "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
+proof (cases "c = 0 \<or> p = 0")
+  case False
+  show ?thesis
+  proof
+    assume "[:c:] dvd p"
+    thus "\<forall>n. c dvd coeff p n" by (auto elim!: dvdE simp: coeffs_def)
+  next
+    assume *: "\<forall>n. c dvd coeff p n"
+    define mydiv where "mydiv = (\<lambda>x y :: 'a. SOME z. x = y * z)"
+    have mydiv: "x = y * mydiv x y" if "y dvd x" for x y
+      using that unfolding mydiv_def dvd_def by (rule someI_ex)
+    define q where "q = Poly (map (\<lambda>a. mydiv a c) (coeffs p))"
+    from False * have "p = q * [:c:]"
+      by (intro poly_eqI) (auto simp: q_def nth_default_def not_less length_coeffs_degree
+                             coeffs_nth intro!: coeff_eq_0 mydiv)
+    thus "[:c:] dvd p" by (simp only: dvd_triv_right)
+  qed
+qed (auto intro!: poly_eqI)
+
+lemma const_poly_dvd_const_poly_iff [simp]:
+  "[:a::'a::{comm_semiring_1,semiring_no_zero_divisors}:] dvd [:b:] \<longleftrightarrow> a dvd b"
+  by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)
+
 
 subsection \<open>Polynomials form an ordered integral domain\<close>
 
-definition pos_poly :: "'a::linordered_idom poly \<Rightarrow> bool"
+definition pos_poly :: "'a::linordered_semidom poly \<Rightarrow> bool"
 where
   "pos_poly p \<longleftrightarrow> 0 < coeff p (degree p)"
 
@@ -1178,7 +1211,7 @@
   apply auto
   done
 
-lemma pos_poly_total: "p = 0 \<or> pos_poly p \<or> pos_poly (- p)"
+lemma pos_poly_total: "(p :: 'a :: linordered_idom poly) = 0 \<or> pos_poly p \<or> pos_poly (- p)"
 by (induct p) (auto simp add: pos_poly_pCons)
 
 lemma last_coeffs_eq_coeff_degree:
@@ -1321,7 +1354,7 @@
   by (simp add: algebra_simps)
 
 lemma poly_eq_0_iff_dvd:
-  fixes c :: "'a::idom"
+  fixes c :: "'a::{comm_ring_1}"
   shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
 proof
   assume "poly p c = 0"
@@ -1335,12 +1368,12 @@
 qed
 
 lemma dvd_iff_poly_eq_0:
-  fixes c :: "'a::idom"
+  fixes c :: "'a::{comm_ring_1}"
   shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0"
   by (simp add: poly_eq_0_iff_dvd)
 
 lemma poly_roots_finite:
-  fixes p :: "'a::idom poly"
+  fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly"
   shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}"
 proof (induct n \<equiv> "degree p" arbitrary: p)
   case (0 p)
@@ -1370,12 +1403,12 @@
 qed
 
 lemma poly_eq_poly_eq_iff:
-  fixes p q :: "'a::{idom,ring_char_0} poly"
+  fixes p q :: "'a::{comm_ring_1,ring_no_zero_divisors,ring_char_0} poly"
   shows "poly p = poly q \<longleftrightarrow> p = q" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?Q then show ?P by simp
 next
-  { fix p :: "'a::{idom,ring_char_0} poly"
+  { fix p :: "'a poly"
     have "poly p = poly 0 \<longleftrightarrow> p = 0"
       apply (cases "p = 0", simp_all)
       apply (drule poly_roots_finite)
@@ -1387,7 +1420,7 @@
 qed
 
 lemma poly_all_0_iff_0:
-  fixes p :: "'a::{ring_char_0, idom} poly"
+  fixes p :: "'a::{ring_char_0, comm_ring_1,ring_no_zero_divisors} poly"
   shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0"
   by (auto simp add: poly_eq_poly_eq_iff [symmetric])
 
@@ -1616,7 +1649,8 @@
   "snd (pseudo_divmod_main lc q r d dr n) = snd (pseudo_divmod_main lc q' r d dr n)"
 by (induct n arbitrary: q q' lc r d dr; simp add: Let_def)
 
-definition pseudo_mod :: "'a :: idom poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+definition pseudo_mod 
+    :: "'a :: {comm_ring_1,semiring_1_no_zero_divisors} poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   "pseudo_mod f g = snd (pseudo_divmod f g)"
   
 lemma pseudo_mod:
@@ -1802,6 +1836,10 @@
 end
 
 
+instance poly :: (idom_divide) algebraic_semidom ..
+
+
+
 subsubsection\<open>Division in Field Polynomials\<close>
 
 text\<open>
@@ -1950,7 +1988,7 @@
   using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
 
 lemma is_unit_iff_degree:
-  assumes "p \<noteq> 0"
+  assumes "p \<noteq> (0 :: _ :: field poly)"
   shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
 proof
   assume ?Q
@@ -1967,7 +2005,7 @@
 qed
 
 lemma is_unit_pCons_iff:
-  "is_unit (pCons a p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0" (is "?P \<longleftrightarrow> ?Q")
+  "is_unit (pCons (a::_::field) p) \<longleftrightarrow> p = 0 \<and> a \<noteq> 0"
   by (cases "p = 0") (auto simp add: is_unit_triv is_unit_iff_degree)
 
 lemma is_unit_monom_trival:
@@ -1977,7 +2015,7 @@
   using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
 
 lemma is_unit_polyE:
-  assumes "is_unit p"
+  assumes "is_unit (p::_::field poly)"
   obtains a where "p = monom a 0" and "a \<noteq> 0"
 proof -
   obtain a q where "p = pCons a q" by (cases p)
@@ -1986,69 +2024,6 @@
   with that show thesis by (simp add: monom_0)
 qed
 
-instantiation poly :: (field) normalization_semidom
-begin
-
-definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "normalize_poly p = smult (inverse (coeff p (degree p))) p"
-
-definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
-
-instance
-proof
-  fix p :: "'a poly"
-  show "unit_factor p * normalize p = p"
-    by (cases "p = 0")
-      (simp_all add: normalize_poly_def unit_factor_poly_def,
-      simp only: mult_smult_left [symmetric] smult_monom, simp)
-next
-  show "normalize 0 = (0::'a poly)"
-    by (simp add: normalize_poly_def)
-next
-  show "unit_factor 0 = (0::'a poly)"
-    by (simp add: unit_factor_poly_def)
-next
-  fix p :: "'a poly"
-  assume "is_unit p"
-  then obtain a where "p = monom a 0" and "a \<noteq> 0"
-    by (rule is_unit_polyE)
-  then show "normalize p = 1"
-    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
-next
-  fix p q :: "'a poly"
-  assume "q \<noteq> 0"
-  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
-    by (auto intro: is_unit_monom_0)
-  then show "is_unit (unit_factor q)"
-    by (simp add: unit_factor_poly_def)
-next
-  fix p q :: "'a poly"
-  have "monom (coeff (p * q) (degree (p * q))) 0 =
-    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
-    by (simp add: monom_0 coeff_degree_mult)
-  then show "unit_factor (p * q) =
-    unit_factor p * unit_factor q"
-    by (simp add: unit_factor_poly_def)
-qed
-
-end
-
-lemma unit_factor_monom [simp]:
-  "unit_factor (monom a n) =
-     (if a = 0 then 0 else monom a 0)"
-  by (simp add: unit_factor_poly_def degree_monom_eq)
-
-lemma unit_factor_pCons [simp]:
-  "unit_factor (pCons a p) =
-     (if p = 0 then monom a 0 else unit_factor p)"
-  by (simp add: unit_factor_poly_def)
-
-lemma normalize_monom [simp]:
-  "normalize (monom a n) =
-     (if a = 0 then 0 else monom 1 n)"
-  by (simp add: normalize_poly_def degree_monom_eq smult_monom)
-
 lemma degree_mod_less:
   "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   using pdivmod_rel [of x y]
@@ -2883,7 +2858,7 @@
 (* The remainder of this section and the next were contributed by Wenda Li *)
 
 lemma degree_mult_eq_0:
-  fixes p q:: "'a :: semidom poly"
+  fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
 by (auto simp add:degree_mult_eq)
 
@@ -2893,7 +2868,7 @@
   by (induct p) (auto simp add:pcompose_pCons)
 
 lemma degree_pcompose:
-  fixes p q:: "'a::semidom poly"
+  fixes p q:: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   shows "degree (pcompose p q) = degree p * degree q"
 proof (induct p)
   case 0
@@ -2940,7 +2915,7 @@
 qed
 
 lemma pcompose_eq_0:
-  fixes p q:: "'a :: semidom poly"
+  fixes p q:: "'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
   assumes "pcompose p q = 0" "degree q > 0" 
   shows "p = 0"
 proof -
@@ -2972,7 +2947,7 @@
   by (induction n) (simp_all add: coeff_mult)
 
 lemma lead_coeff_mult:
-   fixes p q::"'a ::idom poly"
+   fixes p q::"'a :: {comm_semiring_0,semiring_no_zero_divisors} poly"
    shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
 by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq)
 
@@ -2986,9 +2961,20 @@
   "lead_coeff (-p) = - lead_coeff p"
 by (metis coeff_minus degree_minus lead_coeff_def)
 
+lemma lead_coeff_smult:
+  "lead_coeff (smult c p :: 'a :: {comm_semiring_0,semiring_no_zero_divisors} poly) = c * lead_coeff p"
+proof -
+  have "smult c p = [:c:] * p" by simp
+  also have "lead_coeff \<dots> = c * lead_coeff p"
+    by (subst lead_coeff_mult) simp_all
+  finally show ?thesis .
+qed
+
+lemma lead_coeff_eq_zero_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
+  by (simp add: lead_coeff_def)
 
 lemma lead_coeff_comp:
-  fixes p q:: "'a::idom poly"
+  fixes p q:: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
   assumes "degree q > 0" 
   shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)"
 proof (induct p)
@@ -3011,21 +2997,12 @@
       also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)"
         using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
       also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"
-        by auto
+        by (auto simp: mult_ac)
       finally show ?thesis by auto
     qed
   ultimately show ?case by blast
 qed
 
-lemma lead_coeff_smult: 
-  "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"
-proof -
-  have "smult c p = [:c:] * p" by simp
-  also have "lead_coeff \<dots> = c * lead_coeff p" 
-    by (subst lead_coeff_mult) simp_all
-  finally show ?thesis .
-qed
-
 lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
   by (simp add: lead_coeff_def)
 
@@ -3039,7 +3016,7 @@
   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
 
 lemma lead_coeff_power: 
-  "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"
+  "lead_coeff (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = lead_coeff p ^ n"
   by (induction n) (simp_all add: lead_coeff_mult)
 
 lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
@@ -3180,9 +3157,10 @@
 lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
   by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)
   
-(* TODO: does this work for non-idom as well? *)
+(* TODO: does this work with zero divisors as well? Probably not. *)
 lemma reflect_poly_mult:
-  "reflect_poly (p * q) = reflect_poly p * reflect_poly (q :: _ :: idom poly)"
+  "reflect_poly (p * q) = 
+     reflect_poly p * reflect_poly (q :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly)"
 proof (cases "p = 0 \<or> q = 0")
   case False
   hence [simp]: "p \<noteq> 0" "q \<noteq> 0" by auto
@@ -3216,19 +3194,23 @@
 qed auto
 
 lemma reflect_poly_smult: 
-  "reflect_poly (Polynomial.smult (c::'a::idom) p) = Polynomial.smult c (reflect_poly p)"
+  "reflect_poly (Polynomial.smult (c::'a::{comm_semiring_0,semiring_no_zero_divisors}) p) = 
+     Polynomial.smult c (reflect_poly p)"
   using reflect_poly_mult[of "[:c:]" p] by simp
 
 lemma reflect_poly_power:
-    "reflect_poly (p ^ n :: 'a :: idom poly) = reflect_poly p ^ n"
+    "reflect_poly (p ^ n :: 'a :: {comm_semiring_1,semiring_no_zero_divisors} poly) = 
+       reflect_poly p ^ n"
   by (induction n) (simp_all add: reflect_poly_mult)
 
 lemma reflect_poly_setprod:
-  "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: idom poly) A) = setprod (\<lambda>x. reflect_poly (f x)) A"
+  "reflect_poly (setprod (f :: _ \<Rightarrow> _ :: {comm_semiring_0,semiring_no_zero_divisors} poly) A) = 
+     setprod (\<lambda>x. reflect_poly (f x)) A"
   by (cases "finite A", induction rule: finite_induct) (simp_all add: reflect_poly_mult)
 
 lemma reflect_poly_listprod:
-  "reflect_poly (listprod (xs :: _ :: idom poly list)) = listprod (map reflect_poly xs)"
+  "reflect_poly (listprod (xs :: _ :: {comm_semiring_0,semiring_no_zero_divisors} poly list)) = 
+     listprod (map reflect_poly xs)"
   by (induction xs) (simp_all add: reflect_poly_mult)
 
 lemma reflect_poly_Poly_nz: 
@@ -3242,7 +3224,7 @@
 
 subsection \<open>Derivatives of univariate polynomials\<close>
 
-function pderiv :: "('a :: semidom) poly \<Rightarrow> 'a poly"
+function pderiv :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) poly \<Rightarrow> 'a poly"
 where
   "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
   by (auto intro: pCons_cases)
@@ -3271,11 +3253,13 @@
   by (induct p arbitrary: n) 
      (auto simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
 
-fun pderiv_coeffs_code :: "('a :: semidom) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+fun pderiv_coeffs_code 
+      :: "('a :: {comm_semiring_1,semiring_no_zero_divisors}) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   "pderiv_coeffs_code f (x # xs) = cCons (f * x) (pderiv_coeffs_code (f+1) xs)"
 | "pderiv_coeffs_code f [] = []"
 
-definition pderiv_coeffs :: "('a :: semidom) list \<Rightarrow> 'a list" where
+definition pderiv_coeffs :: 
+    "'a :: {comm_semiring_1,semiring_no_zero_divisors} list \<Rightarrow> 'a list" where
   "pderiv_coeffs xs = pderiv_coeffs_code 1 (tl xs)"
 
 (* Efficient code for pderiv contributed by René Thiemann and Akihisa Yamada *)
@@ -3340,7 +3324,7 @@
 qed
 
 context
-  assumes "SORT_CONSTRAINT('a::{semidom, semiring_char_0})"
+  assumes "SORT_CONSTRAINT('a::{comm_semiring_1,semiring_no_zero_divisors, semiring_char_0})"
 begin
 
 lemma pderiv_eq_0_iff: 
@@ -3385,7 +3369,7 @@
 lemma pderiv_minus: "pderiv (- p :: 'a :: idom poly) = - pderiv p"
 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
 
-lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
+lemma pderiv_diff: "pderiv ((p :: _ :: idom poly) - q) = pderiv p - pderiv q"
 by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
 
 lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
diff -r 58ccbc73a172 -r a3fe3250d05d src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 13 15:46:52 2016 +0200
@@ -3,7 +3,7 @@
 section \<open>Abstract euclidean algorithm\<close>
 
 theory Euclidean_Algorithm
-imports "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
+imports "~~/src/HOL/GCD" Factorial_Ring
 begin
 
 text \<open>
@@ -54,6 +54,81 @@
   ultimately show False using size_eq by simp
 qed
 
+lemma size_mult_mono': "b \<noteq> 0 \<Longrightarrow> euclidean_size a \<le> euclidean_size (b * a)"
+  by (subst mult.commute) (rule size_mult_mono)
+
+lemma euclidean_size_times_unit:
+  assumes "is_unit a"
+  shows   "euclidean_size (a * b) = euclidean_size b"
+proof (rule antisym)
+  from assms have [simp]: "a \<noteq> 0" by auto
+  thus "euclidean_size (a * b) \<ge> euclidean_size b" by (rule size_mult_mono')
+  from assms have "is_unit (1 div a)" by simp
+  hence "1 div a \<noteq> 0" by (intro notI) simp_all
+  hence "euclidean_size (a * b) \<le> euclidean_size ((1 div a) * (a * b))"
+    by (rule size_mult_mono')
+  also from assms have "(1 div a) * (a * b) = b"
+    by (simp add: algebra_simps unit_div_mult_swap)
+  finally show "euclidean_size (a * b) \<le> euclidean_size b" .
+qed
+
+lemma euclidean_size_unit: "is_unit x \<Longrightarrow> euclidean_size x = euclidean_size 1"
+  using euclidean_size_times_unit[of x 1] by simp
+
+lemma unit_iff_euclidean_size: 
+  "is_unit x \<longleftrightarrow> euclidean_size x = euclidean_size 1 \<and> x \<noteq> 0"
+proof safe
+  assume A: "x \<noteq> 0" and B: "euclidean_size x = euclidean_size 1"
+  show "is_unit x" by (rule dvd_euclidean_size_eq_imp_dvd[OF A _ B]) simp_all
+qed (auto intro: euclidean_size_unit)
+
+lemma euclidean_size_times_nonunit:
+  assumes "a \<noteq> 0" "b \<noteq> 0" "\<not>is_unit a"
+  shows   "euclidean_size b < euclidean_size (a * b)"
+proof (rule ccontr)
+  assume "\<not>euclidean_size b < euclidean_size (a * b)"
+  with size_mult_mono'[OF assms(1), of b] 
+    have eq: "euclidean_size (a * b) = euclidean_size b" by simp
+  have "a * b dvd b"
+    by (rule dvd_euclidean_size_eq_imp_dvd[OF _ _ eq]) (insert assms, simp_all)
+  hence "a * b dvd 1 * b" by simp
+  with \<open>b \<noteq> 0\<close> have "is_unit a" by (subst (asm) dvd_times_right_cancel_iff)
+  with assms(3) show False by contradiction
+qed
+
+lemma dvd_imp_size_le:
+  assumes "x dvd y" "y \<noteq> 0" 
+  shows   "euclidean_size x \<le> euclidean_size y"
+  using assms by (auto elim!: dvdE simp: size_mult_mono)
+
+lemma dvd_proper_imp_size_less:
+  assumes "x dvd y" "\<not>y dvd x" "y \<noteq> 0" 
+  shows   "euclidean_size x < euclidean_size y"
+proof -
+  from assms(1) obtain z where "y = x * z" by (erule dvdE)
+  hence z: "y = z * x" by (simp add: mult.commute)
+  from z assms have "\<not>is_unit z" by (auto simp: mult.commute mult_unit_dvd_iff)
+  with z assms show ?thesis
+    by (auto intro!: euclidean_size_times_nonunit simp: )
+qed
+
+lemma irreducible_normalized_divisors:
+  assumes "irreducible x" "y dvd x" "normalize y = y"
+  shows   "y = 1 \<or> y = normalize x"
+proof -
+  from assms have "is_unit y \<or> x dvd y" by (auto simp: irreducible_altdef)
+  thus ?thesis
+  proof (elim disjE)
+    assume "is_unit y"
+    hence "normalize y = 1" by (simp add: is_unit_normalize)
+    with assms show ?thesis by simp
+  next
+    assume "x dvd y"
+    with \<open>y dvd x\<close> have "normalize y = normalize x" by (rule associatedI)
+    with assms show ?thesis by simp
+  qed
+qed
+
 function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 where
   "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
@@ -133,6 +208,13 @@
     by (simp add: gcd_eucl_non_0 dvd_mod_iff)
 qed
 
+lemma gcd_euclI:
+  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  assumes "d dvd a" "d dvd b" "normalize d = d"
+          "\<And>k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd d"
+  shows   "gcd_eucl a b = d"
+  by (rule associated_eqI) (simp_all add: gcd_eucl_greatest assms)
+
 lemma eq_gcd_euclI:
   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   assumes "\<And>a b. gcd a b dvd a" "\<And>a b. gcd a b dvd b" "\<And>a b. normalize (gcd a b) = gcd a b"
@@ -211,7 +293,7 @@
   {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast}
   from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast
 qed
-  
+
 lemma normalize_Lcm_eucl [simp]:
   "normalize (Lcm_eucl A) = Lcm_eucl A"
 proof (cases "Lcm_eucl A = 0")
@@ -229,6 +311,125 @@
           "\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl"
   by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least)  
 
+lemma Gcd_eucl_dvd: "x \<in> A \<Longrightarrow> Gcd_eucl A dvd x"
+  unfolding Gcd_eucl_def by (auto intro: Lcm_eucl_least)
+
+lemma Gcd_eucl_greatest: "(\<And>x. x \<in> A \<Longrightarrow> d dvd x) \<Longrightarrow> d dvd Gcd_eucl A"
+  unfolding Gcd_eucl_def by auto
+
+lemma normalize_Gcd_eucl [simp]: "normalize (Gcd_eucl A) = Gcd_eucl A"
+  by (simp add: Gcd_eucl_def)
+
+lemma Lcm_euclI:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> x dvd d" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> x dvd d') \<Longrightarrow> d dvd d'" "normalize d = d"
+  shows   "Lcm_eucl A = d"
+proof -
+  have "normalize (Lcm_eucl A) = normalize d"
+    by (intro associatedI) (auto intro: dvd_Lcm_eucl Lcm_eucl_least assms)
+  thus ?thesis by (simp add: assms)
+qed
+
+lemma Gcd_euclI:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> d dvd x" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> d' dvd x) \<Longrightarrow> d' dvd d" "normalize d = d"
+  shows   "Gcd_eucl A = d"
+proof -
+  have "normalize (Gcd_eucl A) = normalize d"
+    by (intro associatedI) (auto intro: Gcd_eucl_dvd Gcd_eucl_greatest assms)
+  thus ?thesis by (simp add: assms)
+qed
+  
+lemmas lcm_gcd_eucl_facts = 
+  gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest normalize_gcd_eucl lcm_eucl_def
+  Gcd_eucl_def Gcd_eucl_dvd Gcd_eucl_greatest normalize_Gcd_eucl
+  dvd_Lcm_eucl Lcm_eucl_least normalize_Lcm_eucl
+
+lemma 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})"
+proof safe
+  fix p assume p: "p dvd a * b" "normalize p = p"
+  interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
+    by standard (rule lcm_gcd_eucl_facts; assumption)+
+  from dvd_productE[OF p(1)] guess x y . note xy = this
+  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)
+
+
+subclass factorial_semiring
+proof (standard, rule factorial_semiring_altI_aux)
+  fix x assume "x \<noteq> 0"
+  thus "finite {p. p dvd x \<and> normalize p = p}"
+  proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
+    case (less x)
+    show ?case
+    proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y")
+      case False
+      have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}"
+      proof
+        fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}"
+        with False have "is_unit p \<or> x dvd p" by blast
+        thus "p \<in> {1, normalize x}"
+        proof (elim disjE)
+          assume "is_unit p"
+          hence "normalize p = 1" by (simp add: is_unit_normalize)
+          with p show ?thesis by simp
+        next
+          assume "x dvd p"
+          with p have "normalize p = normalize x" by (intro associatedI) simp_all
+          with p show ?thesis by simp
+        qed
+      qed
+      moreover have "finite \<dots>" by simp
+      ultimately show ?thesis by (rule finite_subset)
+      
+    next
+      case True
+      then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast
+      define z where "z = x div y"
+      let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}"
+      from y have x: "x = y * z" by (simp add: z_def)
+      with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
+      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)"
+        by (subst x) (rule normalized_factors_product)
+      also 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))"
+        by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
+           (auto simp: x)
+      finally show ?thesis .
+    qed
+  qed
+next
+  interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
+    by standard (rule lcm_gcd_eucl_facts; assumption)+
+  fix p assume p: "irreducible p"
+  thus "is_prime_elem p" by (rule irreducible_imp_prime_gcd)
+qed
+
+lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial"
+  by (intro ext gcd_euclI gcd_lcm_factorial)
+
+lemma lcm_eucl_eq_lcm_factorial: "lcm_eucl = lcm_factorial"
+  by (intro ext) (simp add: lcm_eucl_def lcm_factorial_gcd_factorial gcd_eucl_eq_gcd_factorial)
+
+lemma Gcd_eucl_eq_Gcd_factorial: "Gcd_eucl = Gcd_factorial"
+  by (intro ext Gcd_euclI gcd_lcm_factorial)
+
+lemma Lcm_eucl_eq_Lcm_factorial: "Lcm_eucl = Lcm_factorial"
+  by (intro ext Lcm_euclI gcd_lcm_factorial)
+
+lemmas eucl_eq_factorial = 
+  gcd_eucl_eq_gcd_factorial lcm_eucl_eq_lcm_factorial 
+  Gcd_eucl_eq_Gcd_factorial Lcm_eucl_eq_Lcm_factorial
+  
 end
 
 class euclidean_ring = euclidean_semiring + idom
@@ -336,7 +537,22 @@
 
 subclass semiring_Gcd
   by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least)
-  
+
+subclass factorial_semiring_gcd
+proof
+  fix a b
+  show "gcd a b = gcd_factorial a b"
+    by (rule sym, rule gcdI) (rule gcd_lcm_factorial; assumption)+
+  thus "lcm a b = lcm_factorial a b"
+    by (simp add: lcm_factorial_gcd_factorial lcm_gcd)
+next
+  fix A 
+  show "Gcd A = Gcd_factorial A"
+    by (rule sym, rule GcdI) (rule gcd_lcm_factorial; assumption)+
+  show "Lcm A = Lcm_factorial A"
+    by (rule sym, rule LcmI) (rule gcd_lcm_factorial; assumption)+
+qed
+
 lemma gcd_non_0:
   "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
@@ -427,6 +643,7 @@
 
 end
 
+
 text \<open>
   A Euclidean ring is a Euclidean semiring with additive inverses. It provides a 
   few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
@@ -437,6 +654,7 @@
 
 subclass euclidean_ring ..
 subclass ring_gcd ..
+subclass factorial_ring_gcd ..
 
 lemma euclid_ext_gcd [simp]:
   "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
@@ -470,8 +688,7 @@
 definition [simp]:
   "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
 
-instance proof
-qed simp_all
+instance by standard simp_all
 
 end
 
@@ -482,46 +699,10 @@
 definition [simp]:
   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
 
-instance
-by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
+instance by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
 
 end
 
-
-instantiation poly :: (field) euclidean_ring
-begin
-
-definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
-  where "euclidean_size p = (if p = 0 then 0 else 2 ^ degree p)"
-
-lemma euclidean_size_poly_0 [simp]:
-  "euclidean_size (0::'a poly) = 0"
-  by (simp add: euclidean_size_poly_def)
-
-lemma euclidean_size_poly_not_0 [simp]:
-  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = 2 ^ degree p"
-  by (simp add: euclidean_size_poly_def)
-
-instance
-proof
-  fix p q :: "'a poly"
-  assume "q \<noteq> 0"
-  then have "p mod q = 0 \<or> degree (p mod q) < degree q"
-    by (rule degree_mod_less [of q p])  
-  with \<open>q \<noteq> 0\<close> show "euclidean_size (p mod q) < euclidean_size q"
-    by (cases "p mod q = 0") simp_all
-next
-  fix p q :: "'a poly"
-  assume "q \<noteq> 0"
-  from \<open>q \<noteq> 0\<close> have "degree p \<le> degree (p * q)"
-    by (rule degree_mult_right_le)
-  with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
-    by (cases "p = 0") simp_all
-qed simp
-
-end
-
-
 instance nat :: euclidean_semiring_gcd
 proof
   show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"
@@ -539,60 +720,4 @@
           semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
 qed
 
-
-instantiation poly :: (field) euclidean_ring_gcd
-begin
-
-definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
-  "gcd_poly = gcd_eucl"
-  
-definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
-  "lcm_poly = lcm_eucl"
-  
-definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
-  "Gcd_poly = Gcd_eucl"
-  
-definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
-  "Lcm_poly = Lcm_eucl"
-
-instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
-end
-
-lemma poly_gcd_monic:
-  "lead_coeff (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)"
-  using unit_factor_gcd[of x y]
-  by (simp add: unit_factor_poly_def monom_0 one_poly_def lead_coeff_def split: if_split_asm)
-
-lemma poly_dvd_antisym:
-  fixes p q :: "'a::idom poly"
-  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
-  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
-proof (cases "p = 0")
-  case True with coeff show "p = q" by simp
-next
-  case False with coeff have "q \<noteq> 0" by auto
-  have degree: "degree p = degree q"
-    using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
-    by (intro order_antisym dvd_imp_degree_le)
-
-  from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
-  with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
-  with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"
-    by (simp add: degree_mult_eq)
-  with coeff a show "p = q"
-    by (cases a, auto split: if_splits)
-qed
-
-lemma poly_gcd_unique:
-  fixes d x y :: "_ poly"
-  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
-    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
-    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
-  shows "d = gcd x y"
-  using assms by (intro gcdI) (auto simp: normalize_poly_def split: if_split_asm)
-
-lemma poly_gcd_code [code]:
-  "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
-  by (simp add: gcd_0 gcd_non_0)
-
-end
+end
\ No newline at end of file
diff -r 58ccbc73a172 -r a3fe3250d05d src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Jul 13 15:46:52 2016 +0200
@@ -1,3 +1,4 @@
+
 (*  Title:      HOL/Number_Theory/Factorial_Ring.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
@@ -5,50 +6,174 @@
 section \<open>Factorial (semi)rings\<close>
 
 theory Factorial_Ring
-imports Main Primes "~~/src/HOL/Library/Multiset"
+imports 
+  Main 
+  "~~/src/HOL/Number_Theory/Primes"
+  "~~/src/HOL/Library/Multiset"
+begin
+
+lemma (in semiring_gcd) dvd_productE:
+  assumes "p dvd (a * b)"
+  obtains x y where "p = x * y" "x dvd a" "y dvd b"
+proof (cases "a = 0")
+  case True
+  thus ?thesis by (intro that[of p 1]) simp_all
+next
+  case False
+  define x y where "x = gcd a p" and "y = p div x"
+  have "p = x * y" by (simp add: x_def y_def)
+  moreover have "x dvd a" by (simp add: x_def)
+  moreover from assms have "p dvd gcd (b * a) (b * p)"
+    by (intro gcd_greatest) (simp_all add: mult.commute)
+  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
+  with False have "y dvd b" 
+    by (simp add: x_def y_def div_dvd_iff_mult assms)
+  ultimately show ?thesis by (rule that)
+qed
+
+
+context comm_semiring_1
 begin
 
+definition irreducible :: "'a \<Rightarrow> bool" where
+  "irreducible p \<longleftrightarrow> p \<noteq> 0 \<and> \<not>p dvd 1 \<and> (\<forall>a b. p = a * b \<longrightarrow> a dvd 1 \<or> b dvd 1)"
+
+lemma not_irreducible_zero [simp]: "\<not>irreducible 0"
+  by (simp add: irreducible_def)
+
+lemma irreducible_not_unit: "irreducible p \<Longrightarrow> \<not>p dvd 1"
+  by (simp add: irreducible_def)
+
+lemma not_irreducible_one [simp]: "\<not>irreducible 1"
+  by (simp add: irreducible_def)
+
+lemma irreducibleI:
+  "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1) \<Longrightarrow> irreducible p"
+  by (simp add: irreducible_def)
+
+lemma irreducibleD: "irreducible p \<Longrightarrow> p = a * b \<Longrightarrow> a dvd 1 \<or> b dvd 1"
+  by (simp add: irreducible_def)
+
+definition is_prime_elem :: "'a \<Rightarrow> bool" where
+  "is_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)"
+
+lemma not_is_prime_elem_zero [simp]: "\<not>is_prime_elem 0"
+  by (simp add: is_prime_elem_def)
+
+lemma is_prime_elem_not_unit: "is_prime_elem p \<Longrightarrow> \<not>p dvd 1"
+  by (simp add: is_prime_elem_def)
+
+lemma is_prime_elemI:
+    "p \<noteq> 0 \<Longrightarrow> \<not>p dvd 1 \<Longrightarrow> (\<And>a b. p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b) \<Longrightarrow> is_prime_elem p"
+  by (simp add: is_prime_elem_def)
+
+lemma prime_divides_productD:
+    "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<Longrightarrow> p dvd a \<or> p dvd b"
+  by (simp add: is_prime_elem_def)
+
+lemma prime_dvd_mult_iff:
+  "is_prime_elem p \<Longrightarrow> p dvd (a * b) \<longleftrightarrow> p dvd a \<or> p dvd b"
+  by (auto simp: is_prime_elem_def)
+
+lemma not_is_prime_elem_one [simp]:
+  "\<not> is_prime_elem 1"
+  by (auto dest: is_prime_elem_not_unit)
+
+lemma is_prime_elem_not_zeroI:
+  assumes "is_prime_elem p"
+  shows "p \<noteq> 0"
+  using assms by (auto intro: ccontr)
+
+lemma is_prime_elem_imp_nonzero [simp]:
+  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 0"
+  unfolding ASSUMPTION_def by (rule is_prime_elem_not_zeroI)
+
+lemma is_prime_elem_imp_not_one [simp]:
+  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> x \<noteq> 1"
+  unfolding ASSUMPTION_def by auto
+
+end
+
+lemma (in algebraic_semidom) mult_unit_dvd_iff': "is_unit a \<Longrightarrow> (a * b) dvd c \<longleftrightarrow> b dvd c"
+  by (subst mult.commute) (rule mult_unit_dvd_iff)
+
 context algebraic_semidom
 begin
 
-lemma dvd_mult_imp_div:
-  assumes "a * c dvd b"
-  shows "a dvd b div c"
-proof (cases "c = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from \<open>a * c dvd b\<close> obtain d where "b = a * c * d" ..
-  with False show ?thesis by (simp add: mult.commute [of a] mult.assoc)
+lemma prime_imp_irreducible:
+  assumes "is_prime_elem p"
+  shows   "irreducible p"
+proof (rule irreducibleI)
+  fix a b
+  assume p_eq: "p = a * b"
+  with assms have nz: "a \<noteq> 0" "b \<noteq> 0" by auto
+  from p_eq have "p dvd a * b" by simp
+  with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
+  with \<open>p = a * b\<close> have "a * b dvd 1 * b \<or> a * b dvd a * 1" by auto
+  thus "a dvd 1 \<or> b dvd 1"
+    by (simp only: dvd_times_left_cancel_iff[OF nz(1)] dvd_times_right_cancel_iff[OF nz(2)])
+qed (insert assms, simp_all add: is_prime_elem_def)
+
+lemma is_prime_elem_mono:
+  assumes "is_prime_elem p" "\<not>q dvd 1" "q dvd p"
+  shows   "is_prime_elem q"
+proof -
+  from \<open>q dvd p\<close> obtain r where r: "p = q * r" by (elim dvdE)
+  hence "p dvd q * r" by simp
+  with \<open>is_prime_elem p\<close> have "p dvd q \<or> p dvd r" by (rule prime_divides_productD)
+  hence "p dvd q"
+  proof
+    assume "p dvd r"
+    then obtain s where s: "r = p * s" by (elim dvdE)
+    from r have "p * 1 = p * (q * s)" by (subst (asm) s) (simp add: mult_ac)
+    with \<open>is_prime_elem p\<close> have "q dvd 1"
+      by (subst (asm) mult_cancel_left) auto
+    with \<open>\<not>q dvd 1\<close> show ?thesis by contradiction
+  qed
+
+  show ?thesis
+  proof (rule is_prime_elemI)
+    fix a b assume "q dvd (a * b)"
+    with \<open>p dvd q\<close> have "p dvd (a * b)" by (rule dvd_trans)
+    with \<open>is_prime_elem p\<close> have "p dvd a \<or> p dvd b" by (rule prime_divides_productD)
+    with \<open>q dvd p\<close> show "q dvd a \<or> q dvd b" by (blast intro: dvd_trans)
+  qed (insert assms, auto)
 qed
 
-end
-
-class factorial_semiring = normalization_semidom +
-  assumes finite_divisors: "a \<noteq> 0 \<Longrightarrow> finite {b. b dvd a \<and> normalize b = b}"
-  fixes is_prime :: "'a \<Rightarrow> bool"
-  assumes not_is_prime_zero [simp]: "\<not> is_prime 0"
-    and is_prime_not_unit: "is_prime p \<Longrightarrow> \<not> is_unit p"
-    and no_prime_divisorsI2: "(\<And>b. b dvd a \<Longrightarrow> \<not> is_prime b) \<Longrightarrow> is_unit a"
-  assumes is_primeI: "p \<noteq> 0 \<Longrightarrow> \<not> is_unit p \<Longrightarrow> (\<And>a. a dvd p \<Longrightarrow> \<not> is_unit a \<Longrightarrow> p dvd a) \<Longrightarrow> is_prime p"
-    and is_primeD: "is_prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
-begin
+lemma irreducibleD':
+  assumes "irreducible a" "b dvd a"
+  shows   "a dvd b \<or> is_unit b"
+proof -
+  from assms obtain c where c: "a = b * c" by (elim dvdE)
+  from irreducibleD[OF assms(1) this] have "is_unit b \<or> is_unit c" .
+  thus ?thesis by (auto simp: c mult_unit_dvd_iff)
+qed
 
-lemma not_is_prime_one [simp]:
-  "\<not> is_prime 1"
-  by (auto dest: is_prime_not_unit)
+lemma irreducibleI':
+  assumes "a \<noteq> 0" "\<not>is_unit a" "\<And>b. b dvd a \<Longrightarrow> a dvd b \<or> is_unit b"
+  shows   "irreducible a"
+proof (rule irreducibleI)
+  fix b c assume a_eq: "a = b * c"
+  hence "a dvd b \<or> is_unit b" by (intro assms) simp_all
+  thus "is_unit b \<or> is_unit c"
+  proof
+    assume "a dvd b"
+    hence "b * c dvd b * 1" by (simp add: a_eq)
+    moreover from \<open>a \<noteq> 0\<close> a_eq have "b \<noteq> 0" by auto
+    ultimately show ?thesis by (subst (asm) dvd_times_left_cancel_iff) auto
+  qed blast
+qed (simp_all add: assms(1,2))
 
-lemma is_prime_not_zeroI:
-  assumes "is_prime p"
-  shows "p \<noteq> 0"
-  using assms by (auto intro: ccontr)
+lemma irreducible_altdef:
+  "irreducible x \<longleftrightarrow> x \<noteq> 0 \<and> \<not>is_unit x \<and> (\<forall>b. b dvd x \<longrightarrow> x dvd b \<or> is_unit b)"
+  using irreducibleI'[of x] irreducibleD'[of x] irreducible_not_unit[of x] by auto
 
-lemma is_prime_multD:
-  assumes "is_prime (a * b)"
+lemma is_prime_elem_multD:
+  assumes "is_prime_elem (a * b)"
   shows "is_unit a \<or> is_unit b"
 proof -
-  from assms have "a \<noteq> 0" "b \<noteq> 0" by auto
-  moreover from assms is_primeD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
+  from assms have "a \<noteq> 0" "b \<noteq> 0" by (auto dest!: is_prime_elem_not_zeroI)
+  moreover from assms prime_divides_productD [of "a * b"] have "a * b dvd a \<or> a * b dvd b"
     by auto
   ultimately show ?thesis
     using dvd_times_left_cancel_iff [of a b 1]
@@ -56,120 +181,112 @@
     by auto
 qed
 
-lemma is_primeD2:
-  assumes "is_prime p" and "a dvd p" and "\<not> is_unit a"
+lemma is_prime_elemD2:
+  assumes "is_prime_elem p" and "a dvd p" and "\<not> is_unit a"
   shows "p dvd a"
 proof -
   from \<open>a dvd p\<close> obtain b where "p = a * b" ..
-  with \<open>is_prime p\<close> is_prime_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
+  with \<open>is_prime_elem p\<close> is_prime_elem_multD \<open>\<not> is_unit a\<close> have "is_unit b" by auto
   with \<open>p = a * b\<close> show ?thesis
     by (auto simp add: mult_unit_dvd_iff)
 qed
 
-lemma is_prime_mult_unit_left:
-  assumes "is_prime p"
-    and "is_unit a"
-  shows "is_prime (a * p)"
-proof (rule is_primeI)
-  from assms show "a * p \<noteq> 0" "\<not> is_unit (a * p)"
-    by (auto simp add: is_unit_mult_iff is_prime_not_unit)
-  show "a * p dvd b" if "b dvd a * p" "\<not> is_unit b" for b
-  proof -
-    from that \<open>is_unit a\<close> have "b dvd p"
-      using dvd_mult_unit_iff [of a b p] by (simp add: ac_simps)
-    with \<open>is_prime p\<close> \<open>\<not> is_unit b\<close> have "p dvd b" 
-      using is_primeD2 [of p b] by auto
-    with \<open>is_unit a\<close> show ?thesis
-      using mult_unit_dvd_iff [of a p b] by (simp add: ac_simps)
-  qed
-qed
+lemma irreducible_mult_unit_left:
+  "is_unit a \<Longrightarrow> irreducible (a * p) \<longleftrightarrow> irreducible p"
+  by (auto simp: irreducible_altdef mult.commute[of a] is_unit_mult_iff
+        mult_unit_dvd_iff dvd_mult_unit_iff)
+
+lemma is_prime_elem_mult_unit_left:
+  "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
+  by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
+
+end
+
+context normalization_semidom
+begin
+
+lemma irreducible_normalize_iff [simp]: "irreducible (normalize x) = irreducible x"
+  using irreducible_mult_unit_left[of "1 div unit_factor x" x]
+  by (cases "x = 0") (simp_all add: unit_div_commute)
+
+lemma is_prime_elem_normalize_iff [simp]: "is_prime_elem (normalize x) = is_prime_elem x"
+  using is_prime_elem_mult_unit_left[of "1 div unit_factor x" x]
+  by (cases "x = 0") (simp_all add: unit_div_commute)
+
+definition is_prime :: "'a \<Rightarrow> bool" where
+  "is_prime p \<longleftrightarrow> is_prime_elem p \<and> normalize p = p"
+
+lemma not_is_prime_0 [simp]: "\<not>is_prime 0" by (simp add: is_prime_def)
+
+lemma not_is_prime_unit: "is_unit x \<Longrightarrow> \<not>is_prime x"
+  using is_prime_elem_not_unit[of x] by (auto simp add: is_prime_def)
+
+lemma not_is_prime_1 [simp]: "\<not>is_prime 1" by (simp add: not_is_prime_unit)
+
+lemma is_primeI: "is_prime_elem x \<Longrightarrow> normalize x = x \<Longrightarrow> is_prime x"
+  by (simp add: is_prime_def)
+
+lemma prime_imp_prime_elem [dest]: "is_prime p \<Longrightarrow> is_prime_elem p"
+  by (simp add: is_prime_def)
 
-lemma is_primeI2:
-  assumes "p \<noteq> 0"
-  assumes "\<not> is_unit p"
-  assumes P: "\<And>a b. p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
-  shows "is_prime p"
-using \<open>p \<noteq> 0\<close> \<open>\<not> is_unit p\<close> proof (rule is_primeI)
-  fix a
-  assume "a dvd p"
-  then obtain b where "p = a * b" ..
-  with \<open>p \<noteq> 0\<close> have "b \<noteq> 0" by simp
-  moreover from \<open>p = a * b\<close> P have "p dvd a \<or> p dvd b" by auto
-  moreover assume "\<not> is_unit a"
-  ultimately show "p dvd a"
-    using dvd_times_right_cancel_iff [of b a 1] \<open>p = a * b\<close> by auto
-qed    
+lemma normalize_is_prime: "is_prime p \<Longrightarrow> normalize p = p"
+  by (simp add: is_prime_def)
+
+lemma is_prime_normalize_iff [simp]: "is_prime (normalize p) \<longleftrightarrow> is_prime_elem p"
+  by (auto simp add: is_prime_def)
+
+lemma is_prime_elem_not_unit' [simp]:
+  "ASSUMPTION (is_prime_elem x) \<Longrightarrow> \<not>is_unit x"
+  unfolding ASSUMPTION_def by (rule is_prime_elem_not_unit)
+
+lemma is_prime_imp_nonzero [simp]:
+  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 0"
+  unfolding ASSUMPTION_def is_prime_def by auto
+
+lemma is_prime_imp_not_one [simp]:
+  "ASSUMPTION (is_prime x) \<Longrightarrow> x \<noteq> 1"
+  unfolding ASSUMPTION_def by auto
 
-lemma not_is_prime_divisorE:
-  assumes "a \<noteq> 0" and "\<not> is_unit a" and "\<not> is_prime a"
-  obtains b where "b dvd a" and "\<not> is_unit b" and "\<not> a dvd b"
-proof -
-  from assms have "\<exists>b. b dvd a \<and> \<not> is_unit b \<and> \<not> a dvd b"
-    by (auto intro: is_primeI)
-  with that show thesis by blast
+lemma is_prime_not_unit' [simp]:
+  "ASSUMPTION (is_prime x) \<Longrightarrow> \<not>is_unit x"
+  unfolding ASSUMPTION_def is_prime_def by auto
+
+lemma is_prime_normalize' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> normalize x = x"
+  unfolding ASSUMPTION_def is_prime_def by simp
+
+lemma unit_factor_is_prime: "is_prime x \<Longrightarrow> unit_factor x = 1"
+  using unit_factor_normalize[of x] unfolding is_prime_def by auto
+
+lemma unit_factor_is_prime' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> unit_factor x = 1"
+  unfolding ASSUMPTION_def by (rule unit_factor_is_prime)
+
+lemma prime_imp_prime_elem' [simp]: "ASSUMPTION (is_prime x) \<Longrightarrow> is_prime_elem x"
+  by (simp add: is_prime_def ASSUMPTION_def)
+
+ lemma is_prime_elem_associated:
+  assumes "is_prime_elem p" and "is_prime_elem q" and "q dvd p"
+  shows "normalize q = normalize p"
+using \<open>q dvd p\<close> proof (rule associatedI)
+  from \<open>is_prime_elem q\<close> have "\<not> is_unit q"
+    by (simp add: is_prime_elem_not_unit)
+  with \<open>is_prime_elem p\<close> \<open>q dvd p\<close> show "p dvd q"
+    by (blast intro: is_prime_elemD2)
 qed
 
-lemma is_prime_normalize_iff [simp]:
-  "is_prime (normalize p) \<longleftrightarrow> is_prime p" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?Q show ?P
-    by (rule is_primeI) (insert \<open>?Q\<close>, simp_all add: is_prime_not_zeroI is_prime_not_unit is_primeD2)
-next
-  assume ?P show ?Q
-    by (rule is_primeI)
-      (insert is_prime_not_zeroI [of "normalize p"] is_prime_not_unit [of "normalize p"] is_primeD2 [of "normalize p"] \<open>?P\<close>, simp_all)
-qed  
-
-lemma no_prime_divisorsI:
-  assumes "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime b"
-  shows "is_unit a"
-proof (rule no_prime_divisorsI2)
-  fix b
-  assume "b dvd a"
-  then have "normalize b dvd a"
-    by simp
-  moreover have "normalize (normalize b) = normalize b"
-    by simp
-  ultimately have "\<not> is_prime (normalize b)"
-    by (rule assms)
-  then show "\<not> is_prime b"
-    by simp
-qed
-
-lemma prime_divisorE:
-  assumes "a \<noteq> 0" and "\<not> is_unit a" 
-  obtains p where "is_prime p" and "p dvd a"
-  using assms no_prime_divisorsI [of a] by blast
-
-lemma is_prime_associated:
-  assumes "is_prime p" and "is_prime q" and "q dvd p"
-  shows "normalize q = normalize p"
-using \<open>q dvd p\<close> proof (rule associatedI)
-  from \<open>is_prime q\<close> have "\<not> is_unit q"
-    by (simp add: is_prime_not_unit)
-  with \<open>is_prime p\<close> \<open>q dvd p\<close> show "p dvd q"
-    by (blast intro: is_primeD2)
-qed
-
-lemma prime_dvd_mult_iff:  
-  assumes "is_prime p"
-  shows "p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
-  using assms by (auto dest: is_primeD)
-
-lemma prime_dvd_msetprod:
-  assumes "is_prime p"
+lemma prime_dvd_msetprodE:
+  assumes "is_prime_elem p"
   assumes dvd: "p dvd msetprod A"
   obtains a where "a \<in># A" and "p dvd a"
 proof -
   from dvd have "\<exists>a. a \<in># A \<and> p dvd a"
   proof (induct A)
     case empty then show ?case
-    using \<open>is_prime p\<close> by (simp add: is_prime_not_unit)
+    using \<open>is_prime_elem p\<close> by (simp add: is_prime_elem_not_unit)
   next
     case (add A a)
     then have "p dvd msetprod A * a" by simp
-    with \<open>is_prime p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
-      by (blast dest: is_primeD)
+    with \<open>is_prime_elem p\<close> consider (A) "p dvd msetprod A" | (B) "p dvd a"
+      by (blast dest: prime_divides_productD)
     then show ?case proof cases
       case B then show ?thesis by auto
     next
@@ -182,64 +299,78 @@
   with that show thesis by blast
 qed
 
-lemma msetprod_eq_iff:
-  assumes "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p" and "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
-  shows "msetprod P = msetprod Q \<longleftrightarrow> P = Q" (is "?R \<longleftrightarrow> ?S")
-proof
-  assume ?S then show ?R by simp
-next
-  assume ?R then show ?S using assms proof (induct P arbitrary: Q)
-    case empty then have Q: "msetprod Q = 1" by simp
-    have "Q = {#}"
-    proof (rule ccontr)
-      assume "Q \<noteq> {#}"
-      then obtain r R where "Q = R + {#r#}"
-        using multi_nonempty_split by blast 
-      moreover with empty have "is_prime r" by simp
-      ultimately have "msetprod Q = msetprod R * r"
-        by simp
-      with Q have "msetprod R * r = 1"
-        by simp
-      then have "is_unit r"
-        by (metis local.dvd_triv_right)
-      with \<open>is_prime r\<close> show False by (simp add: is_prime_not_unit)
-    qed
-    then show ?case by simp
-  next
-    case (add P p)
-    then have "is_prime p" and "normalize p = p"
-      and "msetprod Q = msetprod P * p" and "p dvd msetprod Q"
-      by auto (metis local.dvd_triv_right)
-    with prime_dvd_msetprod
-      obtain q where "q \<in># Q" and "p dvd q"
-      by blast
-    with add.prems have "is_prime q" and "normalize q = q"
-      by simp_all
-    from \<open>is_prime p\<close> have "p \<noteq> 0"
-      by auto 
-    from \<open>is_prime q\<close> \<open>is_prime p\<close> \<open>p dvd q\<close>
-      have "normalize p = normalize q"
-      by (rule is_prime_associated)
-    from \<open>normalize p = p\<close> \<open>normalize q = q\<close> have "p = q"
-      unfolding \<open>normalize p = normalize q\<close> by simp
-    with \<open>q \<in># Q\<close> have "p \<in># Q" by simp
-    have "msetprod P = msetprod (Q - {#p#})"
-      using \<open>p \<in># Q\<close> \<open>p \<noteq> 0\<close> \<open>msetprod Q = msetprod P * p\<close>
-      by (simp add: msetprod_minus)
-    then have "P = Q - {#p#}"
-      using add.prems(2-3)
-      by (auto intro: add.hyps dest: in_diffD)
-    with \<open>p \<in># Q\<close> show ?case by simp
-  qed
+lemma msetprod_subset_imp_dvd:
+  assumes "A \<subseteq># B"
+  shows   "msetprod A dvd msetprod B"
+proof -
+  from assms have "B = (B - A) + A" by (simp add: subset_mset.diff_add)
+  also have "msetprod \<dots> = msetprod (B - A) * msetprod A" by simp
+  also have "msetprod A dvd \<dots>" by simp
+  finally show ?thesis .
+qed
+
+lemma prime_dvd_msetprod_iff: "is_prime p \<Longrightarrow> p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)"
+  by (induction A) (simp_all add: prime_dvd_mult_iff prime_imp_prime_elem, blast+)
+
+lemma primes_dvd_imp_eq:
+  assumes "is_prime p" "is_prime q" "p dvd q"
+  shows   "p = q"
+proof -
+  from assms have "irreducible q" by (simp add: prime_imp_irreducible is_prime_def)
+  from irreducibleD'[OF this \<open>p dvd q\<close>] assms have "q dvd p" by simp
+  with \<open>p dvd q\<close> have "normalize p = normalize q" by (rule associatedI)
+  with assms show "p = q" by simp
+qed
+
+lemma prime_dvd_msetprod_primes_iff:
+  assumes "is_prime p" "\<And>q. q \<in># A \<Longrightarrow> is_prime q"
+  shows   "p dvd msetprod A \<longleftrightarrow> p \<in># A"
+proof -
+  from assms(1) have "p dvd msetprod A \<longleftrightarrow> (\<exists>x. x \<in># A \<and> p dvd x)" by (rule prime_dvd_msetprod_iff)
+  also from assms have "\<dots> \<longleftrightarrow> p \<in># A" by (auto dest: primes_dvd_imp_eq)
+  finally show ?thesis .
 qed
 
+lemma msetprod_primes_dvd_imp_subset:
+  assumes "msetprod A dvd msetprod B" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># B \<Longrightarrow> is_prime p"
+  shows   "A \<subseteq># B"
+using assms
+proof (induction A arbitrary: B)
+  case empty
+  thus ?case by simp
+next
+  case (add A p B)
+  hence p: "is_prime p" by simp
+  define B' where "B' = B - {#p#}"
+  from add.prems have "p dvd msetprod B" by (simp add: dvd_mult_right)
+  with add.prems have "p \<in># B"
+    by (subst (asm) (2) prime_dvd_msetprod_primes_iff) simp_all
+  hence B: "B = B' + {#p#}" by (simp add: B'_def)
+  from add.prems p have "A \<subseteq># B'" by (intro add.IH) (simp_all add: B)
+  thus ?case by (simp add: B)
+qed
+
+lemma normalize_msetprod_primes:
+  "(\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> normalize (msetprod A) = msetprod A"
+proof (induction A)
+  case (add A p)
+  hence "is_prime p" by simp
+  hence "normalize p = p" by simp
+  with add show ?case by (simp add: normalize_mult)
+qed simp_all
+
+lemma msetprod_dvd_msetprod_primes_iff:
+  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
+  shows   "msetprod A dvd msetprod B \<longleftrightarrow> A \<subseteq># B"
+  using assms by (auto intro: msetprod_subset_imp_dvd msetprod_primes_dvd_imp_subset)
+
 lemma prime_dvd_power_iff:
-  assumes "is_prime p"
+  assumes "is_prime_elem p"
   shows "p dvd a ^ n \<longleftrightarrow> p dvd a \<and> n > 0"
-  using assms by (induct n) (auto dest: is_prime_not_unit is_primeD)
+  using assms by (induct n) (auto dest: is_prime_elem_not_unit prime_divides_productD)
 
 lemma prime_power_dvd_multD:
-  assumes "is_prime p"
+  assumes "is_prime_elem p"
   assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   shows "p ^ n dvd b"
 using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> proof (induct n arbitrary: b)
@@ -247,16 +378,16 @@
 next
   case (Suc n) show ?case
   proof (cases "n = 0")
-    case True with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> show ?thesis
+    case True with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> show ?thesis
       by (simp add: prime_dvd_mult_iff)
   next
     case False then have "n > 0" by simp
-    from \<open>is_prime p\<close> have "p \<noteq> 0" by auto
+    from \<open>is_prime_elem p\<close> have "p \<noteq> 0" by auto
     from Suc.prems have *: "p * p ^ n dvd a * b"
       by simp
     then have "p dvd a * b"
       by (rule dvd_mult_left)
-    with Suc \<open>is_prime p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
+    with Suc \<open>is_prime_elem p\<close> \<open>\<not> p dvd a\<close> have "p dvd b"
       by (simp add: prime_dvd_mult_iff)
     moreover define c where "c = b div p"
     ultimately have b: "b = p * c" by simp
@@ -271,497 +402,1065 @@
   qed
 qed
 
-lemma is_prime_inj_power:
-  assumes "is_prime p"
-  shows "inj (op ^ p)"
-proof (rule injI, rule ccontr)
-  fix m n :: nat
-  have [simp]: "p ^ q = 1 \<longleftrightarrow> q = 0" (is "?P \<longleftrightarrow> ?Q") for q
-  proof
-    assume ?Q then show ?P by simp
-  next
-    assume ?P then have "is_unit (p ^ q)" by simp
-    with assms show ?Q by (auto simp add: is_unit_power_iff is_prime_not_unit)
+lemma is_unit_msetprod_iff:
+  "is_unit (msetprod A) \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> is_unit x)"
+  by (induction A) (auto simp: is_unit_mult_iff)
+
+lemma multiset_emptyI: "(\<And>x. x \<notin># A) \<Longrightarrow> A = {#}"
+  by (intro multiset_eqI) (simp_all add: count_eq_zero_iff)
+
+lemma is_unit_msetprod_primes_iff:
+  assumes "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
+  shows   "is_unit (msetprod A) \<longleftrightarrow> A = {#}"
+proof
+  assume unit: "is_unit (msetprod A)"
+  show "A = {#}"
+  proof (intro multiset_emptyI notI)
+    fix x assume "x \<in># A"
+    with unit have "is_unit x" by (subst (asm) is_unit_msetprod_iff) blast
+    moreover from \<open>x \<in># A\<close> have "is_prime x" by (rule assms)
+    ultimately show False by simp
+  qed
+qed simp_all
+
+lemma msetprod_primes_irreducible_imp_prime:
+  assumes irred: "irreducible (msetprod A)"
+  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
+  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
+  assumes C: "\<And>x. x \<in># C \<Longrightarrow> is_prime x"
+  assumes dvd: "msetprod A dvd msetprod B * msetprod C"
+  shows   "msetprod A dvd msetprod B \<or> msetprod A dvd msetprod C"
+proof -
+  from dvd have "msetprod A dvd msetprod (B + C)"
+    by simp
+  with A B C have subset: "A \<subseteq># B + C"
+    by (subst (asm) msetprod_dvd_msetprod_primes_iff) auto
+  define A1 and A2 where "A1 = A #\<inter> B" and "A2 = A - A1"
+  have "A = A1 + A2" unfolding A1_def A2_def
+    by (rule sym, intro subset_mset.add_diff_inverse) simp_all
+  from subset have "A1 \<subseteq># B" "A2 \<subseteq># C"
+    by (auto simp: A1_def A2_def Multiset.subset_eq_diff_conv Multiset.union_commute)
+  from \<open>A = A1 + A2\<close> have "msetprod A = msetprod A1 * msetprod A2" by simp
+  from irred and this have "is_unit (msetprod A1) \<or> is_unit (msetprod A2)"
+    by (rule irreducibleD)
+  with A have "A1 = {#} \<or> A2 = {#}" unfolding A1_def A2_def
+    by (subst (asm) (1 2) is_unit_msetprod_primes_iff) (auto dest: Multiset.in_diffD)
+  with dvd \<open>A = A1 + A2\<close> \<open>A1 \<subseteq># B\<close> \<open>A2 \<subseteq># C\<close> show ?thesis
+    by (auto intro: msetprod_subset_imp_dvd)
+qed
+
+lemma multiset_nonemptyE [elim]:
+  assumes "A \<noteq> {#}"
+  obtains x where "x \<in># A"
+proof -
+  have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto)
+  with that show ?thesis by blast
+qed
+
+lemma msetprod_primes_finite_divisor_powers:
+  assumes A: "\<And>x. x \<in># A \<Longrightarrow> is_prime x"
+  assumes B: "\<And>x. x \<in># B \<Longrightarrow> is_prime x"
+  assumes "A \<noteq> {#}"
+  shows   "finite {n. msetprod A ^ n dvd msetprod B}"
+proof -
+  from \<open>A \<noteq> {#}\<close> obtain x where x: "x \<in># A" by blast
+  define m where "m = count B x"
+  have "{n. msetprod A ^ n dvd msetprod B} \<subseteq> {..m}"
+  proof safe
+    fix n assume dvd: "msetprod A ^ n dvd msetprod B"
+    from x have "x ^ n dvd msetprod A ^ n" by (intro dvd_power_same dvd_msetprod)
+    also note dvd
+    also have "x ^ n = msetprod (replicate_mset n x)" by simp
+    finally have "replicate_mset n x \<subseteq># B"
+      by (rule msetprod_primes_dvd_imp_subset) (insert A B x, simp_all split: if_splits)
+    thus "n \<le> m" by (simp add: count_le_replicate_mset_subset_eq m_def)
   qed
-  have *: False if "p ^ m = p ^ n" and "m > n" for m n
-  proof -
-    from assms have "p \<noteq> 0"
-      by (rule is_prime_not_zeroI)
-    then have "p ^ n \<noteq> 0"
-      by (induct n) simp_all
-    from that have "m = n + (m - n)" and "m - n > 0" by arith+
-    then obtain q where "m = n + q" and "q > 0" ..
-    with that have "p ^ n * p ^ q = p ^ n * 1" by (simp add: power_add)
-    with \<open>p ^ n \<noteq> 0\<close> have "p ^ q = 1"
-      using mult_left_cancel [of "p ^ n" "p ^ q" 1] by simp
-    with \<open>q > 0\<close> show ?thesis by simp
-  qed 
-  assume "m \<noteq> n"
-  then have "m > n \<or> m < n" by arith
-  moreover assume "p ^ m = p ^ n"
-  ultimately show False using * [of m n] * [of n m] by auto
+  moreover have "finite {..m}" by simp
+  ultimately show ?thesis by (rule finite_subset)
+qed
+
+lemma normalize_msetprod:
+  "normalize (msetprod A) = msetprod (image_mset normalize A)"
+  by (induction A) (simp_all add: normalize_mult mult_ac)
+
+end
+
+context semiring_gcd
+begin
+
+lemma irreducible_imp_prime_gcd:
+  assumes "irreducible x"
+  shows   "is_prime_elem x"
+proof (rule is_prime_elemI)
+  fix a b assume "x dvd a * b"
+  from dvd_productE[OF this] obtain y z where yz: "x = y * z" "y dvd a" "z dvd b" .
+  from \<open>irreducible x\<close> and \<open>x = y * z\<close> have "is_unit y \<or> is_unit z" by (rule irreducibleD)
+  with yz show "x dvd a \<or> x dvd b"
+    by (auto simp: mult_unit_dvd_iff mult_unit_dvd_iff')
+qed (insert assms, auto simp: irreducible_not_unit)
+
+end
+
+
+class factorial_semiring = normalization_semidom +
+  assumes prime_factorization_exists:
+            "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
+begin
+
+lemma prime_factorization_exists':
+  assumes "x \<noteq> 0"
+  obtains A where "\<And>x. x \<in># A \<Longrightarrow> is_prime x" "msetprod A = normalize x"
+proof -
+  from prime_factorization_exists[OF assms] obtain A
+    where A: "\<And>x. x \<in># A \<Longrightarrow> is_prime_elem x" "msetprod A = normalize x" by blast
+  define A' where "A' = image_mset normalize A"
+  have "msetprod A' = normalize (msetprod A)"
+    by (simp add: A'_def normalize_msetprod)
+  also note A(2)
+  finally have "msetprod A' = normalize x" by simp
+  moreover from A(1) have "\<forall>x. x \<in># A' \<longrightarrow> is_prime x" by (auto simp: is_prime_def A'_def)
+  ultimately show ?thesis by (intro that[of A']) blast
+qed
+
+lemma irreducible_imp_prime:
+  assumes "irreducible x"
+  shows   "is_prime_elem x"
+proof (rule is_prime_elemI)
+  fix a b assume dvd: "x dvd a * b"
+  from assms have "x \<noteq> 0" by auto
+  show "x dvd a \<or> x dvd b"
+  proof (cases "a = 0 \<or> b = 0")
+    case False
+    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 (msetprod A)" by simp
+    from dvd msetprod_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])
+  qed auto
+qed (insert assms, simp_all add: irreducible_def)
+
+lemma finite_divisor_powers:
+  assumes "y \<noteq> 0" "\<not>is_unit x"
+  shows   "finite {n. x ^ n dvd y}"
+proof (cases "x = 0")
+  case True
+  with assms have "{n. x ^ n dvd y} = {0}" by (auto simp: power_0_left)
+  thus ?thesis by simp
+next
+  case False
+  note nz = this \<open>y \<noteq> 0\<close>
+  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) msetprod_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
+    show ?thesis by (simp add: normalize_power [symmetric])
+qed
+
+lemma finite_prime_divisors:
+  assumes "x \<noteq> 0"
+  shows   "finite {p. is_prime p \<and> p dvd x}"
+proof -
+  from prime_factorization_exists'[OF assms] guess A . note A = this
+  have "{p. is_prime p \<and> p dvd x} \<subseteq> set_mset A"
+  proof safe
+    fix p assume p: "is_prime p" and dvd: "p dvd x"
+    from dvd have "p dvd normalize x" by simp
+    also from A have "normalize x = msetprod A" by simp
+    finally show "p \<in># A" using p A by (subst (asm) prime_dvd_msetprod_primes_iff)
+  qed
+  moreover have "finite (set_mset A)" by simp
+  ultimately show ?thesis by (rule finite_subset)
 qed
 
-definition factorization :: "'a \<Rightarrow> 'a multiset option"
-  where "factorization a = (if a = 0 then None
-    else Some (setsum (\<lambda>p. replicate_mset (Max {n. p ^ n dvd a}) p)
-      {p. p dvd a \<and> is_prime p \<and> normalize p = p}))"
+lemma prime_iff_irreducible: "is_prime_elem x \<longleftrightarrow> irreducible x"
+  by (blast intro: irreducible_imp_prime prime_imp_irreducible)
 
-lemma factorization_normalize [simp]:
-  "factorization (normalize a) = factorization a"
-  by (simp add: factorization_def)
-
-lemma factorization_0 [simp]:
-  "factorization 0 = None"
-  by (simp add: factorization_def)
-
-lemma factorization_eq_None_iff [simp]:
-  "factorization a = None \<longleftrightarrow> a = 0"
-  by (simp add: factorization_def)
+lemma prime_divisor_exists:
+  assumes "a \<noteq> 0" "\<not>is_unit a"
+  shows   "\<exists>b. b dvd a \<and> is_prime b"
+proof -
+  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 msetprod A" "is_prime x" by (auto simp: dvd_msetprod)
+  moreover from this A have "x dvd a" by simp
+  ultimately show ?thesis by blast
+qed
 
-lemma factorization_eq_Some_iff:
-  "factorization a = Some P \<longleftrightarrow>
-   normalize a = msetprod P \<and> 0 \<notin># P \<and> (\<forall>p \<in> set_mset P. is_prime p \<and> normalize p = p)"
-proof (cases "a = 0")
-  have [simp]: "0 = msetprod P \<longleftrightarrow> 0 \<in># P"
-    using msetprod_zero_iff [of P] by blast
-  case True
-  then show ?thesis by auto
-next
-  case False    
-  let ?prime_factors = "\<lambda>a. {p. p dvd a \<and> is_prime p \<and> normalize p = p}"
-  have "?prime_factors a \<subseteq> {b. b dvd a \<and> normalize b = b}"
-    by auto
-  moreover from \<open>a \<noteq> 0\<close> have "finite {b. b dvd a \<and> normalize b = b}"
-    by (rule finite_divisors)
-  ultimately have "finite (?prime_factors a)"
-    by (rule finite_subset)
-  then show ?thesis using \<open>a \<noteq> 0\<close>
-  proof (induct "?prime_factors a" arbitrary: a P)
-    case empty then have
-      *: "{p. p dvd a \<and> is_prime p \<and> normalize p = p} = {}"
-        and "a \<noteq> 0"
-      by auto
-    from \<open>a \<noteq> 0\<close> have "factorization a = Some {#}"
-      by (simp only: factorization_def *) simp
-    from * have "normalize a = 1"
-      by (auto intro: is_unit_normalize no_prime_divisorsI)
-    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
-      assume ?lhs with \<open>factorization a = Some {#}\<close> \<open>normalize a = 1\<close>
-      show ?rhs by simp
-    next
-      assume ?rhs have "P = {#}"
-      proof (rule ccontr)
-        assume "P \<noteq> {#}"
-        then obtain q Q where "P = Q + {#q#}"
-          using multi_nonempty_split by blast
-        with \<open>?rhs\<close> \<open>normalize a = 1\<close>
-        have "1 = q * msetprod Q" and "is_prime q"
-          by (simp_all add: ac_simps)
-        then have "is_unit q" by (auto intro: dvdI)
-        with \<open>is_prime q\<close> show False
-          using is_prime_not_unit by blast
-      qed
-      with \<open>factorization a = Some {#}\<close> show ?lhs by simp
-    qed
-  next
-    case (insert p F)
-    from \<open>insert p F = ?prime_factors a\<close>
-    have "?prime_factors a = insert p F"
-      by simp
-    then have "p dvd a" and "is_prime p" and "normalize p = p" and "p \<noteq> 0"
-      by (auto intro!: is_prime_not_zeroI)
-    define n where "n = Max {n. p ^ n dvd a}"
-    then have "n > 0" and "p ^ n dvd a" and "\<not> p ^ Suc n dvd a" 
-    proof -
-      define N where "N = {n. p ^ n dvd a}"
-      then have n_M: "n = Max N" by (simp add: n_def)
-      from is_prime_inj_power \<open>is_prime p\<close> have "inj (op ^ p)" .
-      then have "inj_on (op ^ p) U" for U
-        by (rule subset_inj_on) simp
-      moreover have "op ^ p ` N \<subseteq> {b. b dvd a \<and> normalize b = b}"
-        by (auto simp add: normalize_power \<open>normalize p = p\<close> N_def)
-      ultimately have "finite N"
-        by (rule inj_on_finite) (simp add: finite_divisors \<open>a \<noteq> 0\<close>)
-      from N_def \<open>a \<noteq> 0\<close> have "0 \<in> N" by (simp add: N_def)
-      then have "N \<noteq> {}" by blast
-      note * = \<open>finite N\<close> \<open>N \<noteq> {}\<close>
-      from N_def \<open>p dvd a\<close> have "1 \<in> N" by simp
-      with * have "Max N > 0"
-        by (auto simp add: Max_gr_iff)
-      then show "n > 0" by (simp add: n_M)
-      from * have "Max N \<in> N" by (rule Max_in)
-      then have "p ^ Max N dvd a" by (simp add: N_def)
-      then show "p ^ n dvd a" by (simp add: n_M)
-      from * have "\<forall>n\<in>N. n \<le> Max N"
-        by (simp add: Max_le_iff [symmetric])
-      then have "p ^ Suc (Max N) dvd a \<Longrightarrow> Suc (Max N) \<le> Max N"
-        by (rule bspec) (simp add: N_def)
-      then have "\<not> p ^ Suc (Max N) dvd a"
-        by auto
-      then show "\<not> p ^ Suc n dvd a"
-        by (simp add: n_M)
-    qed
-    define b where "b = a div p ^ n"
-    with \<open>p ^ n dvd a\<close> have a: "a = p ^ n * b"
-      by simp
-    with \<open>\<not> p ^ Suc n dvd a\<close> have "\<not> p dvd b" and "b \<noteq> 0"
-      by (auto elim: dvdE simp add: ac_simps)
-    have "?prime_factors a = insert p (?prime_factors b)"
-    proof (rule set_eqI)
-      fix q
-      show "q \<in> ?prime_factors a \<longleftrightarrow> q \<in> insert p (?prime_factors b)"
-      using \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close>
-        by (auto simp add: a prime_dvd_mult_iff prime_dvd_power_iff)
-          (auto dest: is_prime_associated)
-    qed
-    with \<open>\<not> p dvd b\<close> have "?prime_factors a - {p} = ?prime_factors b"
-      by auto
-    with insert.hyps have "F = ?prime_factors b"
-      by auto
-    then have "?prime_factors b = F"
-      by simp
-    with \<open>?prime_factors a = insert p (?prime_factors b)\<close> have "?prime_factors a = insert p F"
-      by simp
-    have equiv: "(\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p) =
-      (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p)"
-    using refl proof (rule Groups_Big.setsum.cong)
-      fix q
-      assume "q \<in> F"
-      have "{n. q ^ n dvd a} = {n. q ^ n dvd b}"
-      proof -
-        have "q ^ m dvd a \<longleftrightarrow> q ^ m dvd b" (is "?R \<longleftrightarrow> ?S")
-          for m
-        proof (cases "m = 0")
-          case True then show ?thesis by simp
-        next
-          case False then have "m > 0" by simp
-          show ?thesis
-          proof
-            assume ?S then show ?R by (simp add: a)
-          next
-            assume ?R
-            then have *: "q ^ m dvd p ^ n * b" by (simp add: a)
-            from insert.hyps \<open>q \<in> F\<close>
-            have "is_prime q" "normalize q = q" "p \<noteq> q" "q dvd p ^ n * b"
-              by (auto simp add: a)
-            from \<open>is_prime q\<close> * \<open>m > 0\<close> show ?S
-            proof (rule prime_power_dvd_multD)
-              have "\<not> q dvd p"
-              proof
-                assume "q dvd p"
-                with \<open>is_prime q\<close> \<open>is_prime p\<close> have "normalize q = normalize p"
-                  by (blast intro: is_prime_associated)
-                with \<open>normalize p = p\<close> \<open>normalize q = q\<close> \<open>p \<noteq> q\<close> show False
-                  by simp
-              qed
-              with \<open>is_prime q\<close> show "\<not> q dvd p ^ n"
-                by (simp add: prime_dvd_power_iff)
-            qed
-          qed
-        qed
-        then show ?thesis by auto
-      qed
-      then show
-        "replicate_mset (Max {n. q ^ n dvd a}) q = replicate_mset (Max {n. q ^ n dvd b}) q"
-        by simp
-    qed
-    define Q where "Q = the (factorization b)"
-    with \<open>b \<noteq> 0\<close> have [simp]: "factorization b = Some Q"
-      by simp
-    from \<open>a \<noteq> 0\<close> have "factorization a =
-      Some (\<Sum>p\<in>?prime_factors a. replicate_mset (Max {n. p ^ n dvd a}) p)"
-      by (simp add: factorization_def)
-    also have "\<dots> =
-      Some (\<Sum>p\<in>insert p F. replicate_mset (Max {n. p ^ n dvd a}) p)"
-      by (simp add: \<open>?prime_factors a = insert p F\<close>)
-    also have "\<dots> =
-      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd a}) p))"
-      using \<open>finite F\<close> \<open>p \<notin> F\<close> n_def by simp
-    also have "\<dots> =
-      Some (replicate_mset n p + (\<Sum>p\<in>F. replicate_mset (Max {n. p ^ n dvd b}) p))"
-      using equiv by simp
-    also have "\<dots> = Some (replicate_mset n p + the (factorization b))"
-      using \<open>b \<noteq> 0\<close> by (simp add: factorization_def \<open>?prime_factors a = insert p F\<close> \<open>?prime_factors b = F\<close>)
-    finally have fact_a: "factorization a = 
-      Some (replicate_mset n p + Q)"
-      by simp
-    moreover have "factorization b = Some Q \<longleftrightarrow>
-      normalize b = msetprod Q \<and>
-      0 \<notin># Q \<and>
-      (\<forall>p\<in>#Q. is_prime p \<and> normalize p = p)"
-      using \<open>F = ?prime_factors b\<close> \<open>b \<noteq> 0\<close> by (rule insert.hyps)
-    ultimately have
-      norm_a: "normalize a = msetprod (replicate_mset n p + Q)" and
-      prime_Q: "\<forall>p\<in>set_mset Q. is_prime p \<and> normalize p = p"
-      by (simp_all add: a normalize_mult normalize_power \<open>normalize p = p\<close>)
-    show ?case (is "?lhs \<longleftrightarrow> ?rhs") proof
-      assume ?lhs with fact_a
-      have "P = replicate_mset n p + Q" by simp
-      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> prime_Q
-        show ?rhs by (auto simp add: norm_a dest: is_prime_not_zeroI)
-    next
-      assume ?rhs
-      with \<open>n > 0\<close> \<open>is_prime p\<close> \<open>normalize p = p\<close> \<open>n > 0\<close> prime_Q
-      have "msetprod P = msetprod (replicate_mset n p + Q)"
-        and "\<forall>p\<in>set_mset P. is_prime p \<and> normalize p = p"
-        and "\<forall>p\<in>set_mset (replicate_mset n p + Q). is_prime p \<and> normalize p = p"
-        by (simp_all add: norm_a)
-      then have "P = replicate_mset n p + Q"
-        by (simp only: msetprod_eq_iff)
-      then show ?lhs
-        by (simp add: fact_a)
-    qed
-  qed
+lemma prime_divisors_induct [case_names zero unit factor]:
+  assumes "P 0" "\<And>x. is_unit x \<Longrightarrow> P x" "\<And>p x. is_prime p \<Longrightarrow> P x \<Longrightarrow> P (p * x)"
+  shows   "P x"
+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 * msetprod A)"
+  proof (induction A)
+    case (add A p)
+    from add.prems have "is_prime p" by simp
+    moreover from add.prems have "P (unit_factor x * msetprod A)" by (intro add.IH) simp_all
+    ultimately have "P (p * (unit_factor x * msetprod 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(1))
+
+lemma no_prime_divisors_imp_unit:
+  assumes "a \<noteq> 0" "\<And>b. b dvd a \<Longrightarrow> normalize b = b \<Longrightarrow> \<not> is_prime_elem b"
+  shows "is_unit a"
+proof (rule ccontr)
+  assume "\<not>is_unit a"
+  from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
+  with assms(2)[of b] show False by (simp add: is_prime_def)
 qed
 
-lemma factorization_cases [case_names 0 factorization]:
-  assumes "0": "a = 0 \<Longrightarrow> P"
-  assumes factorization: "\<And>A. a \<noteq> 0 \<Longrightarrow> factorization a = Some A \<Longrightarrow> msetprod A = normalize a
-    \<Longrightarrow> 0 \<notin># A \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> normalize p = p) \<Longrightarrow> (\<And>p. p \<in># A \<Longrightarrow> is_prime p) \<Longrightarrow> P"
-  shows P
-proof (cases "a = 0")
-  case True with 0 show P .
-next
-  case False
-  then have "factorization a \<noteq> None" by simp
-  then obtain A where "factorization a = Some A" by blast
-  moreover from this have "msetprod A = normalize a"
-    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
-    by (auto simp add: factorization_eq_Some_iff)
-  ultimately show P using \<open>a \<noteq> 0\<close> factorization by blast
+lemma prime_divisorE:
+  assumes "a \<noteq> 0" and "\<not> is_unit a"
+  obtains p where "is_prime p" and "p dvd a"
+  using assms no_prime_divisors_imp_unit unfolding is_prime_def by blast
+
+definition multiplicity :: "'a \<Rightarrow> 'a \<Rightarrow> nat" where
+  "multiplicity p x = (if finite {n. p ^ n dvd x} then Max {n. p ^ n dvd x} else 0)"
+
+lemma multiplicity_dvd: "p ^ multiplicity p x dvd x"
+proof (cases "finite {n. p ^ n dvd x}")
+  case True
+  hence "multiplicity p x = Max {n. p ^ n dvd x}"
+    by (simp add: multiplicity_def)
+  also have "\<dots> \<in> {n. p ^ n dvd x}"
+    by (rule Max_in) (auto intro!: True exI[of _ "0::nat"])
+  finally show ?thesis by simp
+qed (simp add: multiplicity_def)
+
+lemma multiplicity_dvd': "n \<le> multiplicity p x \<Longrightarrow> p ^ n dvd x"
+  by (rule dvd_trans[OF le_imp_power_dvd multiplicity_dvd])
+
+lemma dvd_power_iff:
+  assumes "x \<noteq> 0"
+  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
+proof
+  assume *: "x ^ m dvd x ^ n"
+  {
+    assume "m > n"
+    note *
+    also have "x ^ n = x ^ n * 1" by simp
+    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
+    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
+    finally have "x ^ (m - n) dvd 1"
+      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
+    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
+  }
+  thus "is_unit x \<or> m \<le> n" by force
+qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
+
+context
+  fixes x p :: 'a
+  assumes xp: "x \<noteq> 0" "\<not>is_unit p"
+begin
+
+lemma multiplicity_eq_Max: "multiplicity p x = Max {n. p ^ n dvd x}"
+  using finite_divisor_powers[OF xp] by (simp add: multiplicity_def)
+
+lemma multiplicity_geI:
+  assumes "p ^ n dvd x"
+  shows   "multiplicity p x \<ge> n"
+proof -
+  from assms have "n \<le> Max {n. p ^ n dvd x}"
+    by (intro Max_ge finite_divisor_powers xp) simp_all
+  thus ?thesis by (subst multiplicity_eq_Max)
+qed
+
+lemma multiplicity_lessI:
+  assumes "\<not>p ^ n dvd x"
+  shows   "multiplicity p x < n"
+proof (rule ccontr)
+  assume "\<not>(n > multiplicity p x)"
+  hence "p ^ n dvd x" by (intro multiplicity_dvd') simp
+  with assms show False by contradiction
 qed
 
-lemma factorizationE:
-  assumes "a \<noteq> 0"
-  obtains A u where "factorization a = Some A" "normalize a = msetprod A"
-    "0 \<notin># A" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
-  using assms by (cases a rule: factorization_cases) simp_all
+lemma power_dvd_iff_le_multiplicity:
+  "p ^ n dvd x \<longleftrightarrow> n \<le> multiplicity p x"
+  using multiplicity_geI[of n] multiplicity_lessI[of n] by (cases "p ^ n dvd x") auto
+
+lemma multiplicity_eq_zero_iff:
+  assumes "x \<noteq> 0" "\<not>is_unit p"
+  shows   "multiplicity p x = 0 \<longleftrightarrow> \<not>p dvd x"
+  using power_dvd_iff_le_multiplicity[of 1] by auto
+
+lemma multiplicity_gt_zero_iff:
+  assumes "x \<noteq> 0" "\<not>is_unit p"
+  shows   "multiplicity p x > 0 \<longleftrightarrow> p dvd x"
+  using power_dvd_iff_le_multiplicity[of 1] by auto
+
+lemma multiplicity_decompose:
+  "\<not>p dvd (x div p ^ multiplicity p x)"
+proof
+  assume *: "p dvd x div p ^ multiplicity p x"
+  have "x = x div p ^ multiplicity p x * (p ^ multiplicity p x)"
+    using multiplicity_dvd[of p x] by simp
+  also from * have "x div p ^ multiplicity p x = (x div p ^ multiplicity p x div p) * p" by simp
+  also have "x div p ^ multiplicity p x div p * p * p ^ multiplicity p x =
+               x div p ^ multiplicity p x div p * p ^ Suc (multiplicity p x)"
+    by (simp add: mult_assoc)
+  also have "p ^ Suc (multiplicity p x) dvd \<dots>" by (rule dvd_triv_right)
+  finally show False by (subst (asm) power_dvd_iff_le_multiplicity) simp
+qed
+
+lemma multiplicity_decompose':
+  obtains y where "x = p ^ multiplicity p x * y" "\<not>p dvd y"
+  using that[of "x div p ^ multiplicity p x"]
+  by (simp add: multiplicity_decompose multiplicity_dvd)
+
+end
+
+lemma multiplicity_zero [simp]: "multiplicity p 0 = 0"
+  by (simp add: multiplicity_def)
+
+lemma multiplicity_unit_left: "is_unit p \<Longrightarrow> multiplicity p x = 0"
+  by (simp add: multiplicity_def is_unit_power_iff unit_imp_dvd)
 
-lemma prime_dvd_mset_prod_iff:
-  assumes "is_prime p" "normalize p = p" "\<And>p. p \<in># A \<Longrightarrow> is_prime p" "\<And>p. p \<in># A \<Longrightarrow> normalize p = p"
-  shows "p dvd msetprod A \<longleftrightarrow> p \<in># A"
-using assms proof (induct A)
-  case empty then show ?case by (auto dest: is_prime_not_unit)
-next
-  case (add A q) then show ?case
-    using is_prime_associated [of q p]
-    by (simp_all add: prime_dvd_mult_iff, safe, simp_all)
+lemma multiplicity_unit_right:
+  assumes "is_unit x"
+  shows   "multiplicity p x = 0"
+proof (cases "is_unit p \<or> x = 0")
+  case False
+  with multiplicity_lessI[of x p 1] this assms
+    show ?thesis by (auto dest: dvd_unit_imp_unit)
+qed (auto simp: multiplicity_unit_left)
+
+lemma multiplicity_one [simp]: "multiplicity p 1 = 0"
+  by (rule multiplicity_unit_right) simp_all
+
+lemma multiplicity_eqI:
+  assumes "p ^ n dvd x" "\<not>p ^ Suc n dvd x"
+  shows   "multiplicity p x = n"
+proof -
+  consider "x = 0" | "is_unit p" | "x \<noteq> 0" "\<not>is_unit p" by blast
+  thus ?thesis
+  proof cases
+    assume xp: "x \<noteq> 0" "\<not>is_unit p"
+    from xp assms(1) have "multiplicity p x \<ge> n" by (intro multiplicity_geI)
+    moreover from assms(2) xp have "multiplicity p x < Suc n" by (intro multiplicity_lessI)
+    ultimately show ?thesis by simp
+  next
+    assume "is_unit p"
+    hence "is_unit (p ^ Suc n)" by (simp add: is_unit_power_iff del: power_Suc)
+    hence "p ^ Suc n dvd x" by (rule unit_imp_dvd)
+    with \<open>\<not>p ^ Suc n dvd x\<close> show ?thesis by contradiction
+  qed (insert assms, simp_all)
+qed
+
+
+context
+  fixes x p :: 'a
+  assumes xp: "x \<noteq> 0" "\<not>is_unit p"
+begin
+
+lemma multiplicity_times_same:
+  assumes "p \<noteq> 0"
+  shows   "multiplicity p (p * x) = Suc (multiplicity p x)"
+proof (rule multiplicity_eqI)
+  show "p ^ Suc (multiplicity p x) dvd p * x"
+    by (auto intro!: mult_dvd_mono multiplicity_dvd)
+  from xp assms show "\<not> p ^ Suc (Suc (multiplicity p x)) dvd p * x"
+    using power_dvd_iff_le_multiplicity[OF xp, of "Suc (multiplicity p x)"] by simp
 qed
 
 end
 
-class factorial_semiring_gcd = factorial_semiring + gcd +
-  assumes gcd_unfold: "gcd a b =
-    (if a = 0 then normalize b
-     else if b = 0 then normalize a
-     else msetprod (the (factorization a) #\<inter> the (factorization b)))"
-  and lcm_unfold: "lcm a b =
-    (if a = 0 \<or> b = 0 then 0
-     else msetprod (the (factorization a) #\<union> the (factorization b)))"
-begin
+lemma multiplicity_same_power': "multiplicity p (p ^ n) = (if p = 0 \<or> is_unit p then 0 else n)"
+proof -
+  consider "p = 0" | "is_unit p" |"p \<noteq> 0" "\<not>is_unit p" by blast
+  thus ?thesis
+  proof cases
+    assume "p \<noteq> 0" "\<not>is_unit p"
+    thus ?thesis by (induction n) (simp_all add: multiplicity_times_same)
+  qed (simp_all add: power_0_left multiplicity_unit_left)
+qed
 
-subclass semiring_gcd
-proof
-  fix a b
-  have comm: "gcd a b = gcd b a" for a b
-   by (simp add: gcd_unfold ac_simps)
-  have "gcd a b dvd a" for a b
-  proof (cases a rule: factorization_cases)
-    case 0 then show ?thesis by simp
+lemma multiplicity_same_power:
+  "p \<noteq> 0 \<Longrightarrow> \<not>is_unit p \<Longrightarrow> multiplicity p (p ^ n) = n"
+  by (simp add: multiplicity_same_power')
+
+lemma multiplicity_prime_times_other:
+  assumes "is_prime_elem p" "\<not>p dvd q"
+  shows   "multiplicity p (q * x) = multiplicity p x"
+proof (cases "x = 0")
+  case False
+  show ?thesis
+  proof (rule multiplicity_eqI)
+    have "1 * p ^ multiplicity p x dvd q * x"
+      by (intro mult_dvd_mono multiplicity_dvd) simp_all
+    thus "p ^ multiplicity p x dvd q * x" by simp
   next
-    case (factorization A) note fact_A = this
-    then have non_zero: "\<And>p. p \<in>#A \<Longrightarrow> p \<noteq> 0"
-      using normalize_0 not_is_prime_zero by blast
-    show ?thesis
-    proof (cases b rule: factorization_cases)
-      case 0 then show ?thesis by (simp add: gcd_unfold)
-    next
-      case (factorization B) note fact_B = this
-      have "msetprod (A #\<inter> B) dvd msetprod A"
-      using non_zero proof (induct B arbitrary: A)
-        case empty show ?case by simp
-      next
-        case (add B p) show ?case
-        proof (cases "p \<in># A")
-          case True then obtain C where "A = C + {#p#}"
-            by (metis insert_DiffM2)
-          moreover with True add have "p \<noteq> 0" and "\<And>p. p \<in># C \<Longrightarrow> p \<noteq> 0"
-            by auto
-          ultimately show ?thesis
-            using True add.hyps [of C]
-            by (simp add: inter_union_distrib_left [symmetric])
-        next
-          case False with add.prems add.hyps [of A] show ?thesis
-            by (simp add: inter_add_right1)
-        qed
-      qed
-      with fact_A fact_B show ?thesis by (simp add: gcd_unfold)
-    qed
+    define n where "n = multiplicity p x"
+    from assms have "\<not>is_unit p" by simp
+    from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
+    from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
+    also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
+    also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_dvd_mult_iff) fact+
+    also from assms y have "\<dots> \<longleftrightarrow> False" by simp
+    finally show "\<not>(p ^ Suc n dvd q * x)" by blast
   qed
-  then have "gcd a b dvd a" and "gcd b a dvd b"
-    by simp_all
-  then show "gcd a b dvd a" and "gcd a b dvd b"
-    by (simp_all add: comm)
-  show "c dvd gcd a b" if "c dvd a" and "c dvd b" for c
-  proof (cases "a = 0 \<or> b = 0 \<or> c = 0")
-    case True with that show ?thesis by (auto simp add: gcd_unfold)
-  next
-    case False then have "a \<noteq> 0" and "b \<noteq> 0" and "c \<noteq> 0"
-      by simp_all
-    then obtain A B C
-    where fact: "factorization a = Some A" "factorization b = Some B" "factorization c = Some C"
-      and norm: "normalize a = msetprod A" "normalize b = msetprod B" "normalize c = msetprod C"
-      and A: "0 \<notin># A" "p \<in># A \<Longrightarrow> normalize p = p" "p \<in># A \<Longrightarrow> is_prime p"
-      and B: "0 \<notin># B" "p \<in># B \<Longrightarrow> normalize p = p" "p \<in># B \<Longrightarrow> is_prime p"
-      and C: "0 \<notin># C" "p \<in># C \<Longrightarrow> normalize p = p" "p \<in># C \<Longrightarrow> is_prime p"
-      for p
-      by (blast elim!: factorizationE)
-    moreover from that have "normalize c dvd normalize a" and "normalize c dvd normalize b"
-      by simp_all
-    ultimately have "msetprod C dvd msetprod A" and "msetprod C dvd msetprod B"
-      by simp_all
-    with A B C have "msetprod C dvd msetprod (A #\<inter> B)"
-    proof (induct C arbitrary: A B)
-      case empty then show ?case by simp
-    next
-      case add: (add C p)
-      from add.prems
-        have p: "p \<noteq> 0" "is_prime p" "normalize p = p" by auto
-      from add.prems have prems: "msetprod C * p dvd msetprod A" "msetprod C * p dvd msetprod B"
-        by simp_all
-      then have "p dvd msetprod A" "p dvd msetprod B"
-        by (auto dest: dvd_mult_imp_div dvd_mult_right)
-      with p add.prems have "p \<in># A" "p \<in># B"
-        by (simp_all add: prime_dvd_mset_prod_iff)
-      then obtain A' B' where ABp: "A = {#p#} + A'" "B = {#p#} + B'"
-        by (auto dest!: multi_member_split simp add: ac_simps)
-      with add.prems prems p have "msetprod C dvd msetprod (A' #\<inter> B')"
-        by (auto intro: add.hyps simp add: ac_simps)
-      with p have "msetprod ({#p#} + C) dvd msetprod (({#p#} + A') #\<inter> ({#p#} + B'))"
-        by (simp add: inter_union_distrib_right [symmetric])
-      then show ?case by (simp add: ABp ac_simps)
-    qed
-    with \<open>a \<noteq> 0\<close> \<open>b \<noteq> 0\<close> that fact have "normalize c dvd gcd a b"
-      by (simp add: norm [symmetric] gcd_unfold fact)
-    then show ?thesis by simp
-  qed
-  show "normalize (gcd a b) = gcd a b"
-    apply (simp add: gcd_unfold)
-    apply safe
-    apply (rule normalized_msetprodI)
-    apply (auto elim: factorizationE)
-    done
-  show "lcm a b = normalize (a * b) div gcd a b"
-    by (auto elim!: factorizationE simp add: gcd_unfold lcm_unfold normalize_mult
-      union_diff_inter_eq_sup [symmetric] msetprod_diff inter_subset_eq_union)
+qed simp_all
+
+lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
+  "\<lambda>x p. if is_prime p then multiplicity p x else 0"
+  unfolding multiset_def
+proof clarify
+  fix x :: 'a
+  show "finite {p. 0 < (if is_prime p then multiplicity p x else 0)}" (is "finite ?A")
+  proof (cases "x = 0")
+    case False
+    from False have "?A \<subseteq> {p. is_prime p \<and> p dvd x}"
+      by (auto simp: multiplicity_gt_zero_iff)
+    moreover from False have "finite {p. is_prime p \<and> p dvd x}"
+      by (rule finite_prime_divisors)
+    ultimately show ?thesis by (rule finite_subset)
+  qed simp_all
+qed
+
+lemma count_prime_factorization_nonprime:
+  "\<not>is_prime p \<Longrightarrow> count (prime_factorization x) p = 0"
+  by transfer simp
+
+lemma count_prime_factorization_prime:
+  "is_prime p \<Longrightarrow> count (prime_factorization x) p = multiplicity p x"
+  by transfer simp
+
+lemma count_prime_factorization:
+  "count (prime_factorization x) p = (if is_prime p then multiplicity p x else 0)"
+  by transfer simp
+
+lemma unit_imp_no_irreducible_divisors:
+  assumes "is_unit x" "irreducible p"
+  shows   "\<not>p dvd x"
+  using assms dvd_unit_imp_unit irreducible_not_unit by blast
+
+lemma unit_imp_no_prime_divisors:
+  assumes "is_unit x" "is_prime_elem p"
+  shows   "\<not>p dvd x"
+  using unit_imp_no_irreducible_divisors[OF assms(1) prime_imp_irreducible[OF assms(2)]] .
+
+lemma prime_factorization_0 [simp]: "prime_factorization 0 = {#}"
+  by (simp add: multiset_eq_iff count_prime_factorization)
+
+lemma prime_factorization_empty_iff:
+  "prime_factorization x = {#} \<longleftrightarrow> x = 0 \<or> is_unit x"
+proof
+  assume *: "prime_factorization x = {#}"
+  {
+    assume x: "x \<noteq> 0" "\<not>is_unit x"
+    {
+      fix p assume p: "is_prime p"
+      have "count (prime_factorization x) p = 0" by (simp add: *)
+      also from p have "count (prime_factorization x) p = multiplicity p x"
+        by (rule count_prime_factorization_prime)
+      also from x p have "\<dots> = 0 \<longleftrightarrow> \<not>p dvd x" by (simp add: multiplicity_eq_zero_iff)
+      finally have "\<not>p dvd x" .
+    }
+    with prime_divisor_exists[OF x] have False by blast
+  }
+  thus "x = 0 \<or> is_unit x" by blast
+next
+  assume "x = 0 \<or> is_unit x"
+  thus "prime_factorization x = {#}"
+  proof
+    assume x: "is_unit x"
+    {
+      fix p assume p: "is_prime p"
+      from p x have "multiplicity p x = 0"
+        by (subst multiplicity_eq_zero_iff)
+           (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
+    }
+    thus ?thesis by (simp add: multiset_eq_iff count_prime_factorization)
+  qed simp_all
+qed
+
+lemma prime_factorization_unit:
+  assumes "is_unit x"
+  shows   "prime_factorization x = {#}"
+proof (rule multiset_eqI)
+  fix p :: 'a
+  show "count (prime_factorization x) p = count {#} p"
+  proof (cases "is_prime p")
+    case True
+    with assms have "multiplicity p x = 0"
+      by (subst multiplicity_eq_zero_iff)
+         (auto simp: multiplicity_eq_zero_iff dest: unit_imp_no_prime_divisors)
+    with True show ?thesis by (simp add: count_prime_factorization_prime)
+  qed (simp_all add: count_prime_factorization_nonprime)
+qed
+
+lemma prime_factorization_1 [simp]: "prime_factorization 1 = {#}"
+  by (simp add: prime_factorization_unit)
+
+lemma prime_factorization_times_prime:
+  assumes "x \<noteq> 0" "is_prime p"
+  shows   "prime_factorization (p * x) = {#p#} + prime_factorization x"
+proof (rule multiset_eqI)
+  fix q :: 'a
+  consider "\<not>is_prime q" | "p = q" | "is_prime q" "p \<noteq> q" by blast
+  thus "count (prime_factorization (p * x)) q = count ({#p#} + prime_factorization x) q"
+  proof cases
+    assume q: "is_prime q" "p \<noteq> q"
+    with assms primes_dvd_imp_eq[of q p] have "\<not>q dvd p" by auto
+    with q assms show ?thesis
+      by (simp add: multiplicity_prime_times_other count_prime_factorization)
+  qed (insert assms, auto simp: count_prime_factorization multiplicity_times_same)
+qed
+
+lemma msetprod_prime_factorization:
+  assumes "x \<noteq> 0"
+  shows   "msetprod (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 in_prime_factorization_iff:
+  "p \<in># prime_factorization x \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
+proof -
+  have "p \<in># prime_factorization x \<longleftrightarrow> count (prime_factorization x) p > 0" by simp
+  also have "\<dots> \<longleftrightarrow> x \<noteq> 0 \<and> p dvd x \<and> is_prime p"
+   by (subst count_prime_factorization, cases "x = 0")
+      (auto simp: multiplicity_eq_zero_iff multiplicity_gt_zero_iff)
+  finally show ?thesis .
+qed
+
+lemma in_prime_factorization_imp_prime:
+  "p \<in># prime_factorization x \<Longrightarrow> is_prime p"
+  by (simp add: in_prime_factorization_iff)
+
+lemma in_prime_factorization_imp_dvd:
+  "p \<in># prime_factorization x \<Longrightarrow> p dvd x"
+  by (simp add: in_prime_factorization_iff)
+
+lemma multiplicity_self:
+  assumes "p \<noteq> 0" "\<not>is_unit p"
+  shows   "multiplicity p p = 1"
+proof -
+  from assms have "multiplicity p p = Max {n. p ^ n dvd p}"
+    by (simp add: multiplicity_eq_Max)
+  also from assms have "p ^ n dvd p \<longleftrightarrow> n \<le> 1" for n
+    using dvd_power_iff[of p n 1] by auto
+  hence "{n. p ^ n dvd p} = {..1}" by auto
+  also have "\<dots> = {0,1}" by auto
+  finally show ?thesis by simp
+qed
+
+lemma prime_factorization_prime:
+  assumes "is_prime p"
+  shows   "prime_factorization p = {#p#}"
+proof (rule multiset_eqI)
+  fix q :: 'a
+  consider "\<not>is_prime q" | "q = p" | "is_prime q" "q \<noteq> p" by blast
+  thus "count (prime_factorization p) q = count {#p#} q"
+    by cases (insert assms, auto dest: primes_dvd_imp_eq
+                simp: count_prime_factorization multiplicity_self multiplicity_eq_zero_iff)
+qed
+
+lemma prime_factorization_msetprod_primes:
+  assumes "\<And>p. p \<in># A \<Longrightarrow> is_prime p"
+  shows   "prime_factorization (msetprod A) = A"
+  using assms
+proof (induction A)
+  case (add A p)
+  from add.prems[of 0] have "0 \<notin># A" by auto
+  hence "msetprod A \<noteq> 0" by auto
+  with add show ?case
+    by (simp_all add: mult_ac prime_factorization_times_prime Multiset.union_commute)
+qed simp_all
+
+lemma multiplicity_times_unit_left:
+  assumes "is_unit c"
+  shows   "multiplicity (c * p) x = multiplicity p x"
+proof -
+  from assms have "{n. (c * p) ^ n dvd x} = {n. p ^ n dvd x}"
+    by (subst mult.commute) (simp add: mult_unit_dvd_iff power_mult_distrib is_unit_power_iff)
+  thus ?thesis by (simp add: multiplicity_def)
+qed
+
+lemma multiplicity_times_unit_right:
+  assumes "is_unit c"
+  shows   "multiplicity p (c * x) = multiplicity p x"
+proof -
+  from assms have "{n. p ^ n dvd c * x} = {n. p ^ n dvd x}"
+    by (subst mult.commute) (simp add: dvd_mult_unit_iff)
+  thus ?thesis by (simp add: multiplicity_def)
+qed
+
+lemma multiplicity_normalize_left [simp]: "multiplicity (normalize p) x = multiplicity p x"
+proof (cases "p = 0")
+  case [simp]: False
+  have "normalize p = (1 div unit_factor p) * p"
+    by (simp add: unit_div_commute is_unit_unit_factor)
+  also have "multiplicity \<dots> x = multiplicity p x"
+    by (rule multiplicity_times_unit_left) (simp add: is_unit_unit_factor)
+  finally show ?thesis .
+qed simp_all
+
+lemma multiplicity_normalize_right [simp]: "multiplicity p (normalize x) = multiplicity p x"
+proof (cases "x = 0")
+  case [simp]: False
+  have "normalize x = (1 div unit_factor x) * x"
+    by (simp add: unit_div_commute is_unit_unit_factor)
+  also have "multiplicity p \<dots> = multiplicity p x"
+    by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
+  finally show ?thesis .
+qed simp_all
+
+lemma prime_factorization_cong:
+  "normalize x = normalize y \<Longrightarrow> prime_factorization x = prime_factorization y"
+  by (simp add: multiset_eq_iff count_prime_factorization
+                multiplicity_normalize_right [of _ x, symmetric]
+                multiplicity_normalize_right [of _ y, symmetric]
+           del:  multiplicity_normalize_right)
+
+lemma prime_factorization_unique:
+  assumes "x \<noteq> 0" "y \<noteq> 0"
+  shows   "prime_factorization x = prime_factorization y \<longleftrightarrow> normalize x = normalize y"
+proof
+  assume "prime_factorization x = prime_factorization y"
+  hence "msetprod (prime_factorization x) = msetprod (prime_factorization y)" by simp
+  with assms show "normalize x = normalize y" by (simp add: msetprod_prime_factorization)
+qed (rule prime_factorization_cong)
+
+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 (msetprod (prime_factorization (x * y))) =
+          prime_factorization (msetprod (prime_factorization x + prime_factorization y))"
+    by (simp add: msetprod_prime_factorization assms normalize_mult)
+  also have "prime_factorization (msetprod (prime_factorization (x * y))) =
+               prime_factorization (x * y)"
+    by (rule prime_factorization_msetprod_primes) (simp_all add: in_prime_factorization_imp_prime)
+  also have "prime_factorization (msetprod (prime_factorization x + prime_factorization y)) =
+               prime_factorization x + prime_factorization y"
+    by (rule prime_factorization_msetprod_primes) (auto simp: in_prime_factorization_imp_prime)
+  finally show ?thesis .
 qed
 
+lemma prime_factorization_prime_power:
+  "is_prime p \<Longrightarrow> prime_factorization (p ^ n) = replicate_mset n p"
+  by (induction n)
+     (simp_all add: prime_factorization_mult prime_factorization_prime Multiset.union_commute)
+
+lemma prime_decomposition: "unit_factor x * msetprod (prime_factorization x) = x"
+  by (cases "x = 0") (simp_all add: msetprod_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> msetprod (prime_factorization x) dvd msetprod (prime_factorization y)"
+    by (simp add: msetprod_prime_factorization)
+  also have "\<dots> \<longleftrightarrow> prime_factorization x \<subseteq># prime_factorization y"
+    by (auto intro!: msetprod_primes_dvd_imp_subset msetprod_subset_imp_dvd
+                     in_prime_factorization_imp_prime)
+  finally show ?thesis ..
+qed
+
+lemma prime_factorization_divide:
+  assumes "b dvd a"
+  shows   "prime_factorization (a div b) = prime_factorization a - prime_factorization b"
+proof (cases "a = 0")
+  case [simp]: False
+  from assms have [simp]: "b \<noteq> 0" by auto
+  have "prime_factorization ((a div b) * b) = prime_factorization (a div b) + prime_factorization b"
+    by (intro prime_factorization_mult) (insert assms, auto elim!: dvdE)
+  with assms show ?thesis by simp
+qed simp_all
+
+lemma zero_not_in_prime_factorization [simp]: "0 \<notin># prime_factorization x"
+  by (auto dest: in_prime_factorization_imp_prime)
+
+
+definition "gcd_factorial a b = (if a = 0 then normalize b
+     else if b = 0 then normalize a
+     else msetprod (prime_factorization a #\<inter> prime_factorization b))"
+
+definition "lcm_factorial a b = (if a = 0 \<or> b = 0 then 0
+     else msetprod (prime_factorization a #\<union> prime_factorization b))"
+
+definition "Gcd_factorial A =
+  (if A \<subseteq> {0} then 0 else msetprod (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
+     msetprod (Sup (prime_factorization ` A))
+   else
+     0)"
+
+lemma prime_factorization_gcd_factorial:
+  assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
+  shows   "prime_factorization (gcd_factorial a b) = prime_factorization a #\<inter> prime_factorization b"
+proof -
+  have "prime_factorization (gcd_factorial a b) =
+          prime_factorization (msetprod (prime_factorization a #\<inter> prime_factorization b))"
+    by (simp add: gcd_factorial_def)
+  also have "\<dots> = prime_factorization a #\<inter> prime_factorization b"
+    by (subst prime_factorization_msetprod_primes) (auto simp add: in_prime_factorization_imp_prime)
+  finally show ?thesis .
+qed
+
+lemma prime_factorization_lcm_factorial:
+  assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
+  shows   "prime_factorization (lcm_factorial a b) = prime_factorization a #\<union> prime_factorization b"
+proof -
+  have "prime_factorization (lcm_factorial a b) =
+          prime_factorization (msetprod (prime_factorization a #\<union> prime_factorization b))"
+    by (simp add: lcm_factorial_def)
+  also have "\<dots> = prime_factorization a #\<union> prime_factorization b"
+    by (subst prime_factorization_msetprod_primes) (auto simp add: in_prime_factorization_imp_prime)
+  finally show ?thesis .
+qed
+
+lemma prime_factorization_Gcd_factorial:
+  assumes "\<not>A \<subseteq> {0}"
+  shows   "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
+proof -
+  from assms obtain x where x: "x \<in> A - {0}" by auto
+  hence "Inf (prime_factorization ` (A - {0})) \<subseteq># prime_factorization x"
+    by (intro subset_mset.cInf_lower) simp_all
+  hence "\<forall>y. y \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> y \<in># prime_factorization x"
+    by (auto dest: mset_subset_eqD)
+  with in_prime_factorization_imp_prime[of _ x]
+    have "\<forall>p. p \<in># Inf (prime_factorization ` (A - {0})) \<longrightarrow> is_prime p" by blast
+  with assms show ?thesis
+    by (simp add: Gcd_factorial_def prime_factorization_msetprod_primes)
+qed
+
+lemma prime_factorization_Lcm_factorial:
+  assumes "0 \<notin> A" "subset_mset.bdd_above (prime_factorization ` A)"
+  shows   "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
+proof (cases "A = {}")
+  case True
+  hence "prime_factorization ` A = {}" by auto
+  also have "Sup \<dots> = {#}" by (simp add: Sup_multiset_empty)
+  finally show ?thesis by (simp add: Lcm_factorial_def)
+next
+  case False
+  have "\<forall>y. y \<in># Sup (prime_factorization ` A) \<longrightarrow> is_prime y"
+    by (auto simp: in_Sup_multiset_iff assms in_prime_factorization_imp_prime)
+  with assms False show ?thesis
+    by (simp add: Lcm_factorial_def prime_factorization_msetprod_primes)
+qed
+
+lemma gcd_factorial_commute: "gcd_factorial a b = gcd_factorial b a"
+  by (simp add: gcd_factorial_def multiset_inter_commute)
+
+lemma gcd_factorial_dvd1: "gcd_factorial a b dvd a"
+proof (cases "a = 0 \<or> b = 0")
+  case False
+  hence "gcd_factorial a b \<noteq> 0" by (auto simp: gcd_factorial_def)
+  with False show ?thesis
+    by (subst prime_factorization_subset_iff_dvd [symmetric])
+       (auto simp: prime_factorization_gcd_factorial)
+qed (auto simp: gcd_factorial_def)
+
+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 (msetprod (prime_factorization a #\<inter> prime_factorization b)) =
+          msetprod (prime_factorization a #\<inter> prime_factorization b)"
+    by (intro normalize_msetprod_primes) (auto simp: in_prime_factorization_imp_prime)
+  thus ?thesis by (simp add: gcd_factorial_def)
+qed
+
+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")
+  case False
+  with that have [simp]: "c \<noteq> 0" by auto
+  let ?p = "prime_factorization"
+  from that False have "?p c \<subseteq># ?p a" "?p c \<subseteq># ?p b"
+    by (simp_all add: prime_factorization_subset_iff_dvd)
+  hence "prime_factorization c \<subseteq>#
+           prime_factorization (msetprod (prime_factorization a #\<inter> prime_factorization b))"
+    using False by (subst prime_factorization_msetprod_primes)
+                   (auto simp: in_prime_factorization_imp_prime)
+  with False show ?thesis
+    by (auto simp: gcd_factorial_def prime_factorization_subset_iff_dvd [symmetric])
+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
+proof (cases "a = 0 \<or> b = 0")
+  case False
+  let ?p = "prime_factorization"
+  from False have "msetprod (?p (a * b)) div gcd_factorial a b =
+                     msetprod (?p a + ?p b - ?p a #\<inter> ?p b)"
+    by (subst msetprod_diff) (auto simp: lcm_factorial_def gcd_factorial_def
+                                prime_factorization_mult subset_mset.le_infI1)
+  also from False have "msetprod (?p (a * b)) = normalize (a * b)"
+    by (intro msetprod_prime_factorization) simp_all
+  also from False have "msetprod (?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 ..
+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 "is_prime p" if "p \<in># Inf (prime_factorization ` (A - {0}))" for p
+    using that by (auto dest: mset_subset_eqD intro: in_prime_factorization_imp_prime)
+  with False show ?thesis
+    by (auto simp add: Gcd_factorial_def normalize_msetprod_primes)
+qed (simp_all add: Gcd_factorial_def)
+
+lemma Gcd_factorial_eq_0_iff:
+  "Gcd_factorial A = 0 \<longleftrightarrow> A \<subseteq> {0}"
+  by (auto simp: Gcd_factorial_def in_Inf_multiset_iff split: if_splits)
+
+lemma Gcd_factorial_dvd:
+  assumes "x \<in> A"
+  shows   "Gcd_factorial A dvd x"
+proof (cases "x = 0")
+  case False
+  with assms have "prime_factorization (Gcd_factorial A) = Inf (prime_factorization ` (A - {0}))"
+    by (intro prime_factorization_Gcd_factorial) auto
+  also from False assms have "\<dots> \<subseteq># prime_factorization x"
+    by (intro subset_mset.cInf_lower) auto
+  finally show ?thesis
+    by (subst (asm) prime_factorization_subset_iff_dvd)
+       (insert assms False, auto simp: Gcd_factorial_eq_0_iff)
+qed simp_all
+
+lemma Gcd_factorial_greatest:
+  assumes "\<And>y. y \<in> A \<Longrightarrow> x dvd y"
+  shows   "x dvd Gcd_factorial A"
+proof (cases "A \<subseteq> {0}")
+  case False
+  from False obtain y where "y \<in> A" "y \<noteq> 0" by auto
+  with assms[of y] have nz: "x \<noteq> 0" by auto
+  from nz assms have "prime_factorization x \<subseteq># prime_factorization y" if "y \<in> A - {0}" for y
+    using that by (subst prime_factorization_subset_iff_dvd) auto
+  with False have "prime_factorization x \<subseteq># Inf (prime_factorization ` (A - {0}))"
+    by (intro subset_mset.cInf_greatest) auto
+  also from False have "\<dots> = prime_factorization (Gcd_factorial A)"
+    by (rule prime_factorization_Gcd_factorial [symmetric])
+  finally show ?thesis
+    by (subst (asm) prime_factorization_subset_iff_dvd)
+       (insert nz False, auto simp: Gcd_factorial_eq_0_iff)
+qed (simp_all add: Gcd_factorial_def)
+
+
+lemma normalize_Lcm_factorial:
+  "normalize (Lcm_factorial A) = Lcm_factorial A"
+proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
+  case True
+  hence "normalize (msetprod (Sup (prime_factorization ` A))) =
+           msetprod (Sup (prime_factorization ` A))"
+    by (intro normalize_msetprod_primes)
+       (auto simp: in_Sup_multiset_iff in_prime_factorization_imp_prime)
+  with True show ?thesis by (simp add: Lcm_factorial_def)
+qed (auto simp: 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)"
+  by (auto simp: Lcm_factorial_def in_Sup_multiset_iff)
+
+lemma dvd_Lcm_factorial:
+  assumes "x \<in> A"
+  shows   "x dvd Lcm_factorial A"
+proof (cases "0 \<notin> A \<and> subset_mset.bdd_above (prime_factorization ` A)")
+  case True
+  with assms have [simp]: "0 \<notin> A" "x \<noteq> 0" "A \<noteq> {}" by auto
+  from assms True have "prime_factorization x \<subseteq># Sup (prime_factorization ` A)"
+    by (intro subset_mset.cSup_upper) auto
+  also have "\<dots> = prime_factorization (Lcm_factorial A)"
+    by (rule prime_factorization_Lcm_factorial [symmetric]) (insert True, simp_all)
+  finally show ?thesis
+    by (subst (asm) prime_factorization_subset_iff_dvd)
+       (insert True, auto simp: Lcm_factorial_eq_0_iff)
+qed (insert assms, auto simp: Lcm_factorial_def)
+
+lemma Lcm_factorial_least:
+  assumes "\<And>y. y \<in> A \<Longrightarrow> y dvd x"
+  shows   "Lcm_factorial A dvd x"
+proof -
+  consider "A = {}" | "0 \<in> A" | "x = 0" | "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0" by blast
+  thus ?thesis
+  proof cases
+    assume *: "A \<noteq> {}" "0 \<notin> A" "x \<noteq> 0"
+    hence nz: "x \<noteq> 0" if "x \<in> A" for x using that by auto
+    from * have bdd: "subset_mset.bdd_above (prime_factorization ` A)"
+      by (intro subset_mset.bdd_aboveI[of _ "prime_factorization x"])
+         (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
+    have "prime_factorization (Lcm_factorial A) = Sup (prime_factorization ` A)"
+      by (rule prime_factorization_Lcm_factorial) fact+
+    also from * have "\<dots> \<subseteq># prime_factorization x"
+      by (intro subset_mset.cSup_least)
+         (auto simp: prime_factorization_subset_iff_dvd nz dest: assms)
+    finally show ?thesis
+      by (subst (asm) prime_factorization_subset_iff_dvd)
+         (insert * bdd, auto simp: Lcm_factorial_eq_0_iff)
+  qed (auto simp: Lcm_factorial_def dest: assms)
+qed
+
+lemmas gcd_lcm_factorial =
+  gcd_factorial_dvd1 gcd_factorial_dvd2 gcd_factorial_greatest
+  normalize_gcd_factorial lcm_factorial_gcd_factorial
+  normalize_Gcd_factorial Gcd_factorial_dvd Gcd_factorial_greatest
+  normalize_Lcm_factorial dvd_Lcm_factorial Lcm_factorial_least
+
 end
 
-instantiation nat :: factorial_semiring
+lemma (in normalization_semidom) factorial_semiring_altI_aux:
+  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
+  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
+  assumes "(x::'a) \<noteq> 0"
+  shows   "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize x"
+using \<open>x \<noteq> 0\<close>
+proof (induction "card {b. b dvd x \<and> normalize b = b}" arbitrary: x rule: less_induct)
+  case (less a)
+  let ?fctrs = "\<lambda>a. {b. b dvd a \<and> normalize b = b}"
+  show ?case
+  proof (cases "is_unit a")
+    case True
+    thus ?thesis by (intro exI[of _ "{#}"]) (auto simp: is_unit_normalize)
+  next
+    case False
+    show ?thesis
+    proof (cases "\<exists>b. b dvd a \<and> \<not>is_unit b \<and> \<not>a dvd b")
+      case False
+      with \<open>\<not>is_unit a\<close> less.prems have "irreducible a" by (auto simp: irreducible_altdef)
+      hence "is_prime_elem a" by (rule irreducible_imp_prime)
+      thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
+    next
+      case True
+      then guess b by (elim exE conjE) note b = this
+
+      from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
+      moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
+      hence "?fctrs b \<noteq> ?fctrs a" by blast
+      ultimately have "?fctrs b \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
+      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs b) < card (?fctrs a)"
+        by (rule psubset_card_mono)
+      moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
+      ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize b"
+        by (intro less) auto
+      then guess A .. note A = this
+
+      define c where "c = a div b"
+      from b have c: "a = b * c" by (simp add: c_def)
+      from less.prems c have "c \<noteq> 0" by auto
+      from b c have "?fctrs c \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
+      moreover have "normalize a \<notin> ?fctrs c"
+      proof safe
+        assume "normalize a dvd c"
+        hence "b * c dvd 1 * c" by (simp add: c)
+        hence "b dvd 1" by (subst (asm) dvd_times_right_cancel_iff) fact+
+        with b show False by simp
+      qed
+      with \<open>normalize a \<in> ?fctrs a\<close> have "?fctrs a \<noteq> ?fctrs c" by blast
+      ultimately have "?fctrs c \<subset> ?fctrs a" by (subst subset_not_subset_eq) blast
+      with finite_divisors[OF \<open>a \<noteq> 0\<close>] have "card (?fctrs c) < card (?fctrs a)"
+        by (rule psubset_card_mono)
+      with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> is_prime_elem x) \<and> msetprod A = normalize c"
+        by (intro less) auto
+      then guess B .. note B = this
+
+      from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
+    qed
+  qed
+qed 
+
+lemma factorial_semiring_altI:
+  assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
+  assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> is_prime_elem x"
+  shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
+  by intro_classes (rule factorial_semiring_altI_aux[OF assms])
+
+
+class factorial_semiring_gcd = factorial_semiring + gcd + Gcd +
+  assumes gcd_eq_gcd_factorial: "gcd a b = gcd_factorial a b"
+  and     lcm_eq_lcm_factorial: "lcm a b = lcm_factorial a b"
+  and     Gcd_eq_Gcd_factorial: "Gcd A = Gcd_factorial A"
+  and     Lcm_eq_Lcm_factorial: "Lcm A = Lcm_factorial A"
 begin
 
-definition is_prime_nat :: "nat \<Rightarrow> bool"
-where
-  "is_prime_nat p \<longleftrightarrow> (1 < p \<and> (\<forall>n. n dvd p \<longrightarrow> n = 1 \<or> n = p))"
+lemma prime_factorization_gcd:
+  assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
+  shows   "prime_factorization (gcd a b) = prime_factorization a #\<inter> prime_factorization b"
+  by (simp add: gcd_eq_gcd_factorial prime_factorization_gcd_factorial)
 
-lemma is_prime_eq_prime:
-  "is_prime = prime"
-  by (simp add: fun_eq_iff prime_def is_prime_nat_def)
+lemma prime_factorization_lcm:
+  assumes [simp]: "a \<noteq> 0" "b \<noteq> 0"
+  shows   "prime_factorization (lcm a b) = prime_factorization a #\<union> prime_factorization b"
+  by (simp add: lcm_eq_lcm_factorial prime_factorization_lcm_factorial)
 
-instance proof
-  show "\<not> is_prime (0::nat)" by (simp add: is_prime_nat_def)
-  show "\<not> is_unit p" if "is_prime p" for p :: nat
-    using that by (simp add: is_prime_nat_def)
-next
-  fix p :: nat
-  assume "p \<noteq> 0" and "\<not> is_unit p"
-  then have "p > 1" by simp
-  assume P: "\<And>n. n dvd p \<Longrightarrow> \<not> is_unit n \<Longrightarrow> p dvd n"
-  have "n = 1" if "n dvd p" "n \<noteq> p" for n
-  proof (rule ccontr)
-    assume "n \<noteq> 1"
-    with that P have "p dvd n" by auto
-    with \<open>n dvd p\<close> have "n = p" by (rule dvd_antisym)
-    with that show False by simp
-  qed
-  with \<open>p > 1\<close> show "is_prime p" by (auto simp add: is_prime_nat_def)
-next
-  fix p m n :: nat
-  assume "is_prime p"
-  then have "prime p" by (simp add: is_prime_eq_prime)
-  moreover assume "p dvd m * n"
-  ultimately show "p dvd m \<or> p dvd n"
-    by (rule prime_dvd_mult_nat)
-next
-  fix n :: nat
-  show "is_unit n" if "\<And>m. m dvd n \<Longrightarrow> \<not> is_prime m"
-    using that prime_factor_nat by (auto simp add: is_prime_eq_prime)
-qed simp
+lemma prime_factorization_Gcd:
+  assumes "Gcd A \<noteq> 0"
+  shows   "prime_factorization (Gcd A) = Inf (prime_factorization ` (A - {0}))"
+  using assms
+  by (simp add: prime_factorization_Gcd_factorial Gcd_eq_Gcd_factorial Gcd_factorial_eq_0_iff)
+
+lemma prime_factorization_Lcm:
+  assumes "Lcm A \<noteq> 0"
+  shows   "prime_factorization (Lcm A) = Sup (prime_factorization ` A)"
+  using assms
+  by (simp add: prime_factorization_Lcm_factorial Lcm_eq_Lcm_factorial Lcm_factorial_eq_0_iff)
+
+subclass semiring_gcd
+  by (standard, unfold gcd_eq_gcd_factorial lcm_eq_lcm_factorial)
+     (rule gcd_lcm_factorial; assumption)+
+
+subclass semiring_Gcd
+  by (standard, unfold Gcd_eq_Gcd_factorial Lcm_eq_Lcm_factorial)
+     (rule gcd_lcm_factorial; assumption)+
 
 end
 
-instantiation int :: factorial_semiring
+
+class factorial_ring_gcd = factorial_semiring_gcd + idom
 begin
 
-definition is_prime_int :: "int \<Rightarrow> bool"
-where
-  "is_prime_int p \<longleftrightarrow> is_prime (nat \<bar>p\<bar>)"
-
-lemma is_prime_int_iff [simp]:
-  "is_prime (int n) \<longleftrightarrow> is_prime n"
-  by (simp add: is_prime_int_def)
-
-lemma is_prime_nat_abs_iff [simp]:
-  "is_prime (nat \<bar>k\<bar>) \<longleftrightarrow> is_prime k"
-  by (simp add: is_prime_int_def)
+subclass ring_gcd ..
 
-instance proof
-  show "\<not> is_prime (0::int)" by (simp add: is_prime_int_def)
-  show "\<not> is_unit p" if "is_prime p" for p :: int
-    using that is_prime_not_unit [of "nat \<bar>p\<bar>"] by simp
-next
-  fix p :: int
-  assume P: "\<And>k. k dvd p \<Longrightarrow> \<not> is_unit k \<Longrightarrow> p dvd k"
-  have "nat \<bar>p\<bar> dvd n" if "n dvd nat \<bar>p\<bar>" and "n \<noteq> Suc 0" for n :: nat
-  proof -
-    from that have "int n dvd p" by (simp add: int_dvd_iff)
-    moreover from that have "\<not> is_unit (int n)" by simp
-    ultimately have "p dvd int n" by (rule P)
-    with that have "p dvd int n" by auto
-    then show ?thesis by (simp add: dvd_int_iff)
-  qed
-  moreover assume "p \<noteq> 0" and "\<not> is_unit p"
-  ultimately have "is_prime (nat \<bar>p\<bar>)" by (intro is_primeI) auto
-  then show "is_prime p" by simp
-next
-  fix p k l :: int
-  assume "is_prime p"
-  then have *: "is_prime (nat \<bar>p\<bar>)" by simp
-  assume "p dvd k * l"
-  then have "nat \<bar>p\<bar> dvd nat \<bar>k * l\<bar>"
-    by (simp add: dvd_int_unfold_dvd_nat)
-  then have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> * nat \<bar>l\<bar>"
-    by (simp add: abs_mult nat_mult_distrib)
-  with * have "nat \<bar>p\<bar> dvd nat \<bar>k\<bar> \<or> nat \<bar>p\<bar> dvd nat \<bar>l\<bar>"
-    using is_primeD [of "nat \<bar>p\<bar>"] by auto
-  then show "p dvd k \<or> p dvd l"
-    by (simp add: dvd_int_unfold_dvd_nat)
-next
-  fix k :: int
-  assume P: "\<And>l. l dvd k \<Longrightarrow> \<not> is_prime l"
-  have "is_unit (nat \<bar>k\<bar>)"
-  proof (rule no_prime_divisorsI)
-    fix m
-    assume "m dvd nat \<bar>k\<bar>"
-    then have "int m dvd k" by (simp add: int_dvd_iff)
-    then have "\<not> is_prime (int m)" by (rule P)
-    then show "\<not> is_prime m" by simp
-  qed
-  then show "is_unit k" by simp
-qed simp
+subclass idom_divide ..
 
 end
 
+
+lemma is_prime_elem_nat: "is_prime_elem (n::nat) \<longleftrightarrow> prime n"
+proof
+  assume *: "is_prime_elem n"
+  show "prime n" unfolding prime_def
+  proof safe
+    from * have "n \<noteq> 0" "n \<noteq> 1" by (intro notI, simp del: One_nat_def)+
+    thus "n > 1" by (cases n) simp_all
+  next
+    fix m assume m: "m dvd n" "m \<noteq> n"
+    from * \<open>m dvd n\<close> have "n dvd m \<or> is_unit m"
+      by (intro irreducibleD' prime_imp_irreducible)
+    with m show "m = 1" by (auto dest: dvd_antisym)
+  qed
+qed (auto simp: is_prime_elem_def prime_gt_0_nat)
+
+lemma is_prime_nat: "is_prime (n::nat) \<longleftrightarrow> prime n"
+  by (simp add: is_prime_def is_prime_elem_nat)
+
+lemma is_prime_elem_int: "is_prime_elem (n::int) \<longleftrightarrow> prime (nat (abs n))"
+proof (subst is_prime_elem_nat [symmetric], rule iffI)
+  assume "is_prime_elem n"
+  thus "is_prime_elem (nat (abs n))" by (auto simp: is_prime_elem_def nat_dvd_iff)
+next
+  assume "is_prime_elem (nat (abs n))"
+  thus "is_prime_elem n"
+    by (auto simp: dvd_int_unfold_dvd_nat is_prime_elem_def abs_mult nat_mult_distrib)
+qed
+
+lemma is_prime_int: "is_prime (n::int) \<longleftrightarrow> prime n \<and> n \<ge> 0"
+  by (simp add: is_prime_def is_prime_elem_int)
+
 end
+
diff -r 58ccbc73a172 -r a3fe3250d05d src/HOL/Number_Theory/Polynomial_Factorial.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Polynomial_Factorial.thy	Wed Jul 13 15:46:52 2016 +0200
@@ -0,0 +1,1468 @@
+theory Polynomial_Factorial
+imports 
+  Complex_Main
+  Euclidean_Algorithm 
+  "~~/src/HOL/Library/Fraction_Field" 
+  "~~/src/HOL/Library/Polynomial"
+  "/home/manuel/hg/Linear_Recurrences/Normalized_Fraction"
+begin
+
+subsection \<open>Prelude\<close>
+
+lemma msetprod_mult: 
+  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
+  by (induction A) (simp_all add: mult_ac)
+  
+lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
+  by (induction A) (simp_all add: mult_ac)
+  
+lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
+proof safe
+  assume "x \<noteq> 0"
+  hence "y = x * (y / x)" by (simp add: field_simps)
+  thus "x dvd y" by (rule dvdI)
+qed auto
+
+lemma nat_descend_induct [case_names base descend]:
+  assumes "\<And>k::nat. k > n \<Longrightarrow> P k"
+  assumes "\<And>k::nat. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
+  shows   "P m"
+  using assms by induction_schema (force intro!: wf_measure[of "\<lambda>k. Suc n - k"])+
+
+lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
+  by (metis GreatestI)
+
+
+context field
+begin
+
+subclass idom_divide ..
+
+end
+
+context field
+begin
+
+definition normalize_field :: "'a \<Rightarrow> 'a" 
+  where [simp]: "normalize_field x = (if x = 0 then 0 else 1)"
+definition unit_factor_field :: "'a \<Rightarrow> 'a" 
+  where [simp]: "unit_factor_field x = x"
+definition euclidean_size_field :: "'a \<Rightarrow> nat" 
+  where [simp]: "euclidean_size_field x = (if x = 0 then 0 else 1)"
+definition mod_field :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  where [simp]: "mod_field x y = (if y = 0 then x else 0)"
+
+end
+
+instantiation real :: euclidean_ring
+begin
+
+definition [simp]: "normalize_real = (normalize_field :: real \<Rightarrow> _)"
+definition [simp]: "unit_factor_real = (unit_factor_field :: real \<Rightarrow> _)"
+definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
+definition [simp]: "mod_real = (mod_field :: real \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation real :: euclidean_ring_gcd
+begin
+
+definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
+  "gcd_real = gcd_eucl"
+definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
+  "lcm_real = lcm_eucl"
+definition Gcd_real :: "real set \<Rightarrow> real" where
+ "Gcd_real = Gcd_eucl"
+definition Lcm_real :: "real set \<Rightarrow> real" where
+ "Lcm_real = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
+
+end
+
+instantiation rat :: euclidean_ring
+begin
+
+definition [simp]: "normalize_rat = (normalize_field :: rat \<Rightarrow> _)"
+definition [simp]: "unit_factor_rat = (unit_factor_field :: rat \<Rightarrow> _)"
+definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
+definition [simp]: "mod_rat = (mod_field :: rat \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation rat :: euclidean_ring_gcd
+begin
+
+definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
+  "gcd_rat = gcd_eucl"
+definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
+  "lcm_rat = lcm_eucl"
+definition Gcd_rat :: "rat set \<Rightarrow> rat" where
+ "Gcd_rat = Gcd_eucl"
+definition Lcm_rat :: "rat set \<Rightarrow> rat" where
+ "Lcm_rat = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
+
+end
+
+instantiation complex :: euclidean_ring
+begin
+
+definition [simp]: "normalize_complex = (normalize_field :: complex \<Rightarrow> _)"
+definition [simp]: "unit_factor_complex = (unit_factor_field :: complex \<Rightarrow> _)"
+definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
+definition [simp]: "mod_complex = (mod_field :: complex \<Rightarrow> _)"
+
+instance by standard (simp_all add: dvd_field_iff divide_simps)
+end
+
+instantiation complex :: euclidean_ring_gcd
+begin
+
+definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
+  "gcd_complex = gcd_eucl"
+definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
+  "lcm_complex = lcm_eucl"
+definition Gcd_complex :: "complex set \<Rightarrow> complex" where
+ "Gcd_complex = Gcd_eucl"
+definition Lcm_complex :: "complex set \<Rightarrow> complex" where
+ "Lcm_complex = Lcm_eucl"
+
+instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
+
+end
+
+
+
+subsection \<open>Lifting elements into the field of fractions\<close>
+
+definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
+
+lemma to_fract_0 [simp]: "to_fract 0 = 0"
+  by (simp add: to_fract_def eq_fract Zero_fract_def)
+
+lemma to_fract_1 [simp]: "to_fract 1 = 1"
+  by (simp add: to_fract_def eq_fract One_fract_def)
+
+lemma to_fract_add [simp]: "to_fract (x + y) = to_fract x + to_fract y"
+  by (simp add: to_fract_def)
+
+lemma to_fract_diff [simp]: "to_fract (x - y) = to_fract x - to_fract y"
+  by (simp add: to_fract_def)
+  
+lemma to_fract_uminus [simp]: "to_fract (-x) = -to_fract x"
+  by (simp add: to_fract_def)
+  
+lemma to_fract_mult [simp]: "to_fract (x * y) = to_fract x * to_fract y"
+  by (simp add: to_fract_def)
+
+lemma to_fract_eq_iff [simp]: "to_fract x = to_fract y \<longleftrightarrow> x = y"
+  by (simp add: to_fract_def eq_fract)
+  
+lemma to_fract_eq_0_iff [simp]: "to_fract x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: to_fract_def Zero_fract_def eq_fract)
+
+lemma snd_quot_of_fract_nonzero [simp]: "snd (quot_of_fract x) \<noteq> 0"
+  by transfer simp
+
+lemma Fract_quot_of_fract [simp]: "Fract (fst (quot_of_fract x)) (snd (quot_of_fract x)) = x"
+  by transfer (simp del: fractrel_iff, subst fractrel_normalize_quot_left, simp)
+
+lemma to_fract_quot_of_fract:
+  assumes "snd (quot_of_fract x) = 1"
+  shows   "to_fract (fst (quot_of_fract x)) = x"
+proof -
+  have "x = Fract (fst (quot_of_fract x)) (snd (quot_of_fract x))" by simp
+  also note assms
+  finally show ?thesis by (simp add: to_fract_def)
+qed
+
+lemma snd_quot_of_fract_Fract_whole:
+  assumes "y dvd x"
+  shows   "snd (quot_of_fract (Fract x y)) = 1"
+  using assms by transfer (auto simp: normalize_quot_def Let_def gcd_proj2_if_dvd)
+  
+lemma Fract_conv_to_fract: "Fract a b = to_fract a / to_fract b"
+  by (simp add: to_fract_def)
+
+lemma quot_of_fract_to_fract [simp]: "quot_of_fract (to_fract x) = (x, 1)"
+  unfolding to_fract_def by transfer (simp add: normalize_quot_def)
+
+lemma fst_quot_of_fract_eq_0_iff [simp]: "fst (quot_of_fract x) = 0 \<longleftrightarrow> x = 0"
+  by transfer simp
+ 
+lemma snd_quot_of_fract_to_fract [simp]: "snd (quot_of_fract (to_fract x)) = 1"
+  unfolding to_fract_def by (rule snd_quot_of_fract_Fract_whole) simp_all
+
+lemma coprime_quot_of_fract:
+  "coprime (fst (quot_of_fract x)) (snd (quot_of_fract x))"
+  by transfer (simp add: coprime_normalize_quot)
+
+lemma unit_factor_snd_quot_of_fract: "unit_factor (snd (quot_of_fract x)) = 1"
+  using quot_of_fract_in_normalized_fracts[of x] 
+  by (simp add: normalized_fracts_def case_prod_unfold)  
+
+lemma unit_factor_1_imp_normalized: "unit_factor x = 1 \<Longrightarrow> normalize x = x"
+  by (subst (2) normalize_mult_unit_factor [symmetric, of x])
+     (simp del: normalize_mult_unit_factor)
+  
+lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
+  by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
+
+  
+subsection \<open>Mapping polynomials\<close>
+
+definition map_poly 
+     :: "('a :: comm_semiring_0 \<Rightarrow> 'b :: comm_semiring_0) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where
+  "map_poly f p = Poly (map f (coeffs p))"
+
+lemma map_poly_0 [simp]: "map_poly f 0 = 0"
+  by (simp add: map_poly_def)
+
+lemma map_poly_1: "map_poly f 1 = [:f 1:]"
+  by (simp add: map_poly_def)
+
+lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
+  by (simp add: map_poly_def one_poly_def)
+
+lemma coeff_map_poly:
+  assumes "f 0 = 0"
+  shows   "coeff (map_poly f p) n = f (coeff p n)"
+  by (auto simp: map_poly_def nth_default_def coeffs_def assms
+        not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc)
+
+lemma coeffs_map_poly [code abstract]: 
+    "coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))"
+  by (simp add: map_poly_def)
+
+lemma set_coeffs_map_poly:
+  "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
+  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0)
+
+lemma coeffs_map_poly': 
+  assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)"
+  shows   "coeffs (map_poly f p) = map f (coeffs p)"
+  by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
+                           intro!: strip_while_not_last split: if_splits)
+
+lemma degree_map_poly:
+  assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
+  shows   "degree (map_poly f p) = degree p"
+  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)
+
+lemma map_poly_eq_0_iff:
+  assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
+  shows   "map_poly f p = 0 \<longleftrightarrow> p = 0"
+proof -
+  {
+    fix n :: nat
+    have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms)
+    also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0"
+    proof (cases "n < length (coeffs p)")
+      case True
+      hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc)
+      with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto
+    qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
+    finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" .
+  }
+  thus ?thesis by (auto simp: poly_eq_iff)
+qed
+
+lemma map_poly_smult:
+  assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x"
+  shows   "map_poly f (smult c p) = smult (f c) (map_poly f p)"
+  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)
+
+lemma map_poly_pCons:
+  assumes "f 0 = 0"
+  shows   "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
+  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)
+
+lemma map_poly_map_poly:
+  assumes "f 0 = 0" "g 0 = 0"
+  shows   "map_poly f (map_poly g p) = map_poly (f \<circ> g) p"
+  by (intro poly_eqI) (simp add: coeff_map_poly assms)
+
+lemma map_poly_id [simp]: "map_poly id p = p"
+  by (simp add: map_poly_def)
+
+lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p"
+  by (simp add: map_poly_def)
+
+lemma map_poly_cong: 
+  assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)"
+  shows   "map_poly f p = map_poly g p"
+proof -
+  from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all
+  thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly)
+qed
+
+lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n"
+  by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+lemma map_poly_idI:
+  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
+  shows   "map_poly f p = p"
+  using map_poly_cong[OF assms, of _ id] by simp
+
+lemma map_poly_idI':
+  assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x"
+  shows   "p = map_poly f p"
+  using map_poly_cong[OF assms, of _ id] by simp
+
+lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p"
+  by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+lemma div_const_poly_conv_map_poly: 
+  assumes "[:c:] dvd p"
+  shows   "p div [:c:] = map_poly (\<lambda>x. x div c) p"
+proof (cases "c = 0")
+  case False
+  from assms obtain q where p: "p = [:c:] * q" by (erule dvdE)
+  moreover {
+    have "smult c q = [:c:] * q" by simp
+    also have "\<dots> div [:c:] = q" by (rule nonzero_mult_divide_cancel_left) (insert False, auto)
+    finally have "smult c q div [:c:] = q" .
+  }
+  ultimately show ?thesis by (intro poly_eqI) (auto simp: coeff_map_poly False)
+qed (auto intro!: poly_eqI simp: coeff_map_poly)
+
+
+
+subsection \<open>Various facts about polynomials\<close>
+
+lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
+  by (induction A) (simp_all add: one_poly_def mult_ac)
+
+lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
+  using degree_mod_less[of b a] by auto
+  
+lemma is_unit_const_poly_iff: 
+    "[:c :: 'a :: {comm_semiring_1,semiring_no_zero_divisors}:] dvd 1 \<longleftrightarrow> c dvd 1"
+  by (auto simp: one_poly_def)
+
+lemma is_unit_poly_iff:
+  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
+  shows "p dvd 1 \<longleftrightarrow> (\<exists>c. p = [:c:] \<and> c dvd 1)"
+proof safe
+  assume "p dvd 1"
+  then obtain q where pq: "1 = p * q" by (erule dvdE)
+  hence "degree 1 = degree (p * q)" by simp
+  also from pq have "\<dots> = degree p + degree q" by (intro degree_mult_eq) auto
+  finally have "degree p = 0" by simp
+  from degree_eq_zeroE[OF this] obtain c where c: "p = [:c:]" .
+  with \<open>p dvd 1\<close> show "\<exists>c. p = [:c:] \<and> c dvd 1"
+    by (auto simp: is_unit_const_poly_iff)
+qed (auto simp: is_unit_const_poly_iff)
+
+lemma is_unit_polyE:
+  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
+  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
+  using assms by (subst (asm) is_unit_poly_iff) blast
+
+lemma smult_eq_iff:
+  assumes "(b :: 'a :: field) \<noteq> 0"
+  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
+proof
+  assume "smult a p = smult b q"
+  also from assms have "smult (inverse b) \<dots> = q" by simp
+  finally show "smult (a / b) p = q" by (simp add: field_simps)
+qed (insert assms, auto)
+
+lemma irreducible_const_poly_iff:
+  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
+  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
+proof
+  assume A: "irreducible c"
+  show "irreducible [:c:]"
+  proof (rule irreducibleI)
+    fix a b assume ab: "[:c:] = a * b"
+    hence "degree [:c:] = degree (a * b)" by (simp only: )
+    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
+    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
+    finally have "degree a = 0" "degree b = 0" by auto
+    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
+    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
+    hence "c = a' * b'" by (simp add: ab' mult_ac)
+    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
+    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
+  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
+next
+  assume A: "irreducible [:c:]"
+  show "irreducible c"
+  proof (rule irreducibleI)
+    fix a b assume ab: "c = a * b"
+    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
+    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
+    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
+  qed (insert A, auto simp: irreducible_def one_poly_def)
+qed
+
+lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
+  by (cases "c = 0") (simp_all add: lead_coeff_def degree_monom_eq)
+
+  
+subsection \<open>Normalisation of polynomials\<close>
+
+instantiation poly :: ("{normalization_semidom,idom_divide}") normalization_semidom
+begin
+
+definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
+  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
+
+definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
+  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+
+lemma normalize_poly_altdef:
+  "normalize p = p div [:unit_factor (lead_coeff p):]"
+proof (cases "p = 0")
+  case False
+  thus ?thesis
+    by (subst div_const_poly_conv_map_poly)
+       (auto simp: normalize_poly_def const_poly_dvd_iff lead_coeff_def )
+qed (auto simp: normalize_poly_def)
+
+instance
+proof
+  fix p :: "'a poly"
+  show "unit_factor p * normalize p = p"
+    by (cases "p = 0")
+       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
+          smult_conv_map_poly map_poly_map_poly o_def)
+next
+  fix p :: "'a poly"
+  assume "is_unit p"
+  then obtain c where p: "p = [:c:]" "is_unit c" by (auto simp: is_unit_poly_iff)
+  thus "normalize p = 1"
+    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
+next
+  fix p :: "'a poly" assume "p \<noteq> 0"
+  thus "is_unit (unit_factor p)"
+    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
+qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
+
+end
+
+lemma unit_factor_pCons:
+  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
+  by (simp add: unit_factor_poly_def)
+
+lemma normalize_monom [simp]:
+  "normalize (monom a n) = monom (normalize a) n"
+  by (simp add: map_poly_monom normalize_poly_def)
+
+lemma unit_factor_monom [simp]:
+  "unit_factor (monom a n) = monom (unit_factor a) 0"
+  by (simp add: unit_factor_poly_def )
+
+lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
+  by (simp add: normalize_poly_def map_poly_pCons)
+
+lemma normalize_smult: "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)"
+    by (subst normalize_mult) (simp add: normalize_const_poly)
+  finally show ?thesis .
+qed
+
+lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
+proof -
+  have "smult c p = [:c:] * p" by simp
+  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
+  proof safe
+    assume A: "[:c:] * p dvd 1"
+    thus "p dvd 1" by (rule dvd_mult_right)
+    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
+    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
+    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
+    also note B [symmetric]
+    finally show "c dvd 1" by simp
+  next
+    assume "c dvd 1" "p dvd 1"
+    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
+    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
+    hence "[:c:] dvd 1" by (rule dvdI)
+    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
+  qed
+  finally show ?thesis .
+qed
+
+
+subsection \<open>Content and primitive part of a polynomial\<close>
+
+definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
+  "content p = Gcd (set (coeffs p))"
+
+lemma content_0 [simp]: "content 0 = 0"
+  by (simp add: content_def)
+
+lemma content_1 [simp]: "content 1 = 1"
+  by (simp add: content_def)
+
+lemma content_const [simp]: "content [:c:] = normalize c"
+  by (simp add: content_def cCons_def)
+
+lemma const_poly_dvd_iff_dvd_content:
+  fixes c :: "'a :: semiring_Gcd"
+  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
+proof (cases "p = 0")
+  case [simp]: False
+  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
+  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
+  proof safe
+    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
+    thus "c dvd coeff p n"
+      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
+  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
+  also have "\<dots> \<longleftrightarrow> c dvd content p"
+    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
+          dvd_mult_unit_iff lead_coeff_nonzero)
+  finally show ?thesis .
+qed simp_all
+
+lemma content_dvd [simp]: "[:content p:] dvd p"
+  by (subst const_poly_dvd_iff_dvd_content) simp_all
+  
+lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
+  by (cases "n \<le> degree p") 
+     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
+
+lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
+  by (simp add: content_def Gcd_dvd)
+
+lemma normalize_content [simp]: "normalize (content p) = content p"
+  by (simp add: content_def)
+
+lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
+proof
+  assume "is_unit (content p)"
+  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
+  thus "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_mult)
+
+lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
+  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
+
+definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
+  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
+  
+lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
+  by (simp add: primitive_part_def)
+
+lemma content_times_primitive_part [simp]:
+  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
+  shows "smult (content p) (primitive_part p) = p"
+proof (cases "p = 0")
+  case False
+  thus ?thesis
+  unfolding primitive_part_def
+  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
+           intro: map_poly_idI)
+qed simp_all
+
+lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
+proof (cases "p = 0")
+  case False
+  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
+    by (simp add:  primitive_part_def)
+  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
+    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
+  finally show ?thesis using False by simp
+qed simp
+
+lemma content_primitive_part [simp]:
+  assumes "p \<noteq> 0"
+  shows   "content (primitive_part p) = 1"
+proof -
+  have "p = smult (content p) (primitive_part p)" by simp
+  also have "content \<dots> = content p * content (primitive_part p)" 
+    by (simp del: content_times_primitive_part)
+  finally show ?thesis using assms by simp
+qed
+
+lemma content_decompose:
+  fixes p :: "'a :: semiring_Gcd poly"
+  obtains p' where "p = smult (content p) p'" "content p' = 1"
+proof (cases "p = 0")
+  case True
+  thus ?thesis by (intro that[of 1]) simp_all
+next
+  case False
+  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
+  have "content p * 1 = content p * content r" by (subst r) simp
+  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
+  with r show ?thesis by (intro that[of r]) simp_all
+qed
+
+lemma smult_content_normalize_primitive_part [simp]:
+  "smult (content p) (normalize (primitive_part p)) = normalize p"
+proof -
+  have "smult (content p) (normalize (primitive_part p)) = 
+          normalize ([:content p:] * primitive_part p)" 
+    by (subst normalize_mult) (simp_all add: normalize_const_poly)
+  also have "[:content p:] * primitive_part p = p" by simp
+  finally show ?thesis .
+qed
+
+lemma content_dvd_contentI [intro]:
+  "p dvd q \<Longrightarrow> content p dvd content q"
+  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
+  
+lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
+  by (simp add: primitive_part_def map_poly_pCons)
+ 
+lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
+  by (auto simp: primitive_part_def)
+  
+lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
+proof (cases "p = 0")
+  case False
+  have "p = smult (content p) (primitive_part p)" by simp
+  also from False have "degree \<dots> = degree (primitive_part p)"
+    by (subst degree_smult_eq) simp_all
+  finally show ?thesis ..
+qed simp_all
+
+
+subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
+
+abbreviation (input) fract_poly 
+  where "fract_poly \<equiv> map_poly to_fract"
+
+abbreviation (input) unfract_poly 
+  where "unfract_poly \<equiv> map_poly (fst \<circ> quot_of_fract)"
+  
+lemma fract_poly_smult [simp]: "fract_poly (smult c p) = smult (to_fract c) (fract_poly p)"
+  by (simp add: smult_conv_map_poly map_poly_map_poly o_def)
+
+lemma fract_poly_0 [simp]: "fract_poly 0 = 0"
+  by (simp add: poly_eqI coeff_map_poly)
+
+lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
+  by (simp add: one_poly_def map_poly_pCons)
+
+lemma fract_poly_add [simp]:
+  "fract_poly (p + q) = fract_poly p + fract_poly q"
+  by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+lemma fract_poly_diff [simp]:
+  "fract_poly (p - q) = fract_poly p - fract_poly q"
+  by (intro poly_eqI) (simp_all add: coeff_map_poly)
+
+lemma to_fract_setsum [simp]: "to_fract (setsum f A) = setsum (\<lambda>x. to_fract (f x)) A"
+  by (cases "finite A", induction A rule: finite_induct) simp_all 
+
+lemma fract_poly_mult [simp]:
+  "fract_poly (p * q) = fract_poly p * fract_poly q"
+  by (intro poly_eqI) (simp_all add: coeff_map_poly coeff_mult)
+
+lemma fract_poly_eq_iff [simp]: "fract_poly p = fract_poly q \<longleftrightarrow> p = q"
+  by (auto simp: poly_eq_iff coeff_map_poly)
+
+lemma fract_poly_eq_0_iff [simp]: "fract_poly p = 0 \<longleftrightarrow> p = 0"
+  using fract_poly_eq_iff[of p 0] by (simp del: fract_poly_eq_iff)
+
+lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
+  by (auto elim!: dvdE)
+
+lemma msetprod_fract_poly: 
+  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
+  by (induction A) (simp_all add: mult_ac)
+  
+lemma is_unit_fract_poly_iff:
+  "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
+proof safe
+  assume A: "p dvd 1"
+  with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
+  from A show "content p = 1"
+    by (auto simp: is_unit_poly_iff normalize_1_iff)
+next
+  assume A: "fract_poly p dvd 1" and B: "content p = 1"
+  from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
+  {
+    fix n :: nat assume "n > 0"
+    have "to_fract (coeff p n) = coeff (fract_poly p) n" by (simp add: coeff_map_poly)
+    also note c
+    also from \<open>n > 0\<close> have "coeff [:c:] n = 0" by (simp add: coeff_pCons split: nat.splits)
+    finally have "coeff p n = 0" by simp
+  }
+  hence "degree p \<le> 0" by (intro degree_le) simp_all
+  with B show "p dvd 1" by (auto simp: is_unit_poly_iff normalize_1_iff elim!: degree_eq_zeroE)
+qed
+  
+lemma fract_poly_is_unit: "p dvd 1 \<Longrightarrow> fract_poly p dvd 1"
+  using fract_poly_dvd[of p 1] by simp
+
+lemma fract_poly_smult_eqE:
+  fixes c :: "'a :: {idom_divide,ring_gcd} 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"
+proof -
+  define a b where "a = fst (quot_of_fract c)" and "b = snd (quot_of_fract c)"
+  have "smult (to_fract a) (fract_poly q) = smult (to_fract b) (fract_poly p)"
+    by (subst smult_eq_iff) (simp_all add: a_def b_def Fract_conv_to_fract [symmetric] assms)
+  hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
+  hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
+  moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
+    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
+          normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
+  ultimately show ?thesis by (intro that[of a b])
+qed
+
+
+subsection \<open>Fractional content\<close>
+
+abbreviation (input) Lcm_coeff_denoms 
+    :: "'a :: {semiring_Gcd,idom_divide,ring_gcd} 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
+  "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
+  "primitive_part_fract p = 
+     primitive_part (unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p))"
+
+lemma primitive_part_fract_0 [simp]: "primitive_part_fract 0 = 0"
+  by (simp add: primitive_part_fract_def)
+
+lemma fract_content_eq_0_iff [simp]:
+  "fract_content p = 0 \<longleftrightarrow> p = 0"
+  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"
+  unfolding primitive_part_fract_def
+  by (rule content_primitive_part)
+     (auto simp: primitive_part_fract_def map_poly_eq_0_iff Lcm_0_iff)  
+
+lemma content_times_primitive_part_fract:
+  "smult (fract_content p) (fract_poly (primitive_part_fract p)) = p"
+proof -
+  define p' where "p' = unfract_poly (smult (to_fract (Lcm_coeff_denoms p)) p)"
+  have "fract_poly p' = 
+          map_poly (to_fract \<circ> fst \<circ> quot_of_fract) (smult (to_fract (Lcm_coeff_denoms p)) p)"
+    unfolding primitive_part_fract_def p'_def 
+    by (subst map_poly_map_poly) (simp_all add: o_assoc)
+  also have "\<dots> = smult (to_fract (Lcm_coeff_denoms p)) p"
+  proof (intro map_poly_idI, unfold o_apply)
+    fix c assume "c \<in> set (coeffs (smult (to_fract (Lcm_coeff_denoms p)) p))"
+    then obtain c' where c: "c' \<in> set (coeffs p)" "c = to_fract (Lcm_coeff_denoms p) * c'"
+      by (auto simp add: Lcm_0_iff coeffs_smult split: if_splits)
+    note c(2)
+    also have "c' = Fract (fst (quot_of_fract c')) (snd (quot_of_fract c'))"
+      by simp
+    also have "to_fract (Lcm_coeff_denoms p) * \<dots> = 
+                 Fract (Lcm_coeff_denoms p * fst (quot_of_fract c')) (snd (quot_of_fract c'))"
+      unfolding to_fract_def by (subst mult_fract) simp_all
+    also have "snd (quot_of_fract \<dots>) = 1"
+      by (intro snd_quot_of_fract_Fract_whole dvd_mult2 dvd_Lcm) (insert c(1), auto)
+    finally show "to_fract (fst (quot_of_fract c)) = c"
+      by (rule to_fract_quot_of_fract)
+  qed
+  also have "p' = smult (content p') (primitive_part p')" 
+    by (rule content_times_primitive_part [symmetric])
+  also have "primitive_part p' = primitive_part_fract p"
+    by (simp add: primitive_part_fract_def p'_def)
+  also have "fract_poly (smult (content p') (primitive_part_fract p)) = 
+               smult (to_fract (content p')) (fract_poly (primitive_part_fract p))" by simp
+  finally have "smult (to_fract (content p')) (fract_poly (primitive_part_fract p)) =
+                      smult (to_fract (Lcm_coeff_denoms p)) p" .
+  thus ?thesis
+    by (subst (asm) smult_eq_iff)
+       (auto simp add: Let_def p'_def Fract_conv_to_fract field_simps Lcm_0_iff fract_content_def)
+qed
+
+lemma fract_content_fract_poly [simp]: "fract_content (fract_poly p) = to_fract (content p)"
+proof -
+  have "Lcm_coeff_denoms (fract_poly p) = 1"
+    by (auto simp: Lcm_1_iff set_coeffs_map_poly)
+  hence "fract_content (fract_poly p) = 
+           to_fract (content (map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p))"
+    by (simp add: fract_content_def to_fract_def fract_collapse map_poly_map_poly del: Lcm_1_iff)
+  also have "map_poly (fst \<circ> quot_of_fract \<circ> to_fract) p = p"
+    by (intro map_poly_idI) simp_all
+  finally show ?thesis .
+qed
+
+lemma content_decompose_fract:
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} fract poly"
+  obtains c p' where "p = smult c (map_poly to_fract p')" "content p' = 1"
+proof (cases "p = 0")
+  case True
+  hence "p = smult 0 (map_poly to_fract 1)" "content 1 = 1" by simp_all
+  thus ?thesis ..
+next
+  case False
+  thus ?thesis
+    by (rule that[OF content_times_primitive_part_fract [symmetric] content_primitive_part_fract])
+qed
+
+
+subsection \<open>More properties of content and primitive part\<close>
+
+lemma lift_prime_elem_poly:
+  assumes "is_prime_elem (c :: 'a :: semidom)"
+  shows   "is_prime_elem [:c:]"
+proof (rule is_prime_elemI)
+  fix a b assume *: "[:c:] dvd a * b"
+  from * have dvd: "c dvd coeff (a * b) n" for n
+    by (subst (asm) const_poly_dvd_iff) blast
+  {
+    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
+    assume "\<not>[:c:] dvd b"
+    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
+    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
+      by (auto intro: le_degree simp: less_Suc_eq_le)
+    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
+    have "i \<le> m" if "\<not>c dvd coeff b i" for i
+      unfolding m_def by (rule Greatest_le[OF that B])
+    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
+
+    have "c dvd coeff a i" for i
+    proof (induction i rule: nat_descend_induct[of "degree a"])
+      case (base i)
+      thus ?case by (simp add: coeff_eq_0)
+    next
+      case (descend i)
+      let ?A = "{..i+m} - {i}"
+      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
+      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
+        by (simp add: coeff_mult)
+      also have "{..i+m} = insert i ?A" by auto
+      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
+                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
+        (is "_ = _ + ?S")
+        by (subst setsum.insert) simp_all
+      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
+      moreover have "c dvd ?S"
+      proof (rule dvd_setsum)
+        fix k assume k: "k \<in> {..i+m} - {i}"
+        show "c dvd coeff a k * coeff b (i + m - k)"
+        proof (cases "k < i")
+          case False
+          with k have "c dvd coeff a k" by (intro descend.IH) simp
+          thus ?thesis by simp
+        next
+          case True
+          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
+          thus ?thesis by simp
+        qed
+      qed
+      ultimately have "c dvd coeff a i * coeff b m"
+        by (simp add: dvd_add_left_iff)
+      with assms coeff_m show "c dvd coeff a i"
+        by (simp add: prime_dvd_mult_iff)
+    qed
+    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
+  }
+  thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
+qed (insert assms, simp_all add: is_prime_elem_def one_poly_def)
+
+lemma prime_elem_const_poly_iff:
+  fixes c :: "'a :: semidom"
+  shows   "is_prime_elem [:c:] \<longleftrightarrow> is_prime_elem c"
+proof
+  assume A: "is_prime_elem [:c:]"
+  show "is_prime_elem c"
+  proof (rule is_prime_elemI)
+    fix a b assume "c dvd a * b"
+    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
+    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_divides_productD)
+    thus "c dvd a \<or> c dvd b" by simp
+  qed (insert A, auto simp: is_prime_elem_def is_unit_poly_iff)
+qed (auto intro: lift_prime_elem_poly)
+
+context
+begin
+
+private lemma content_1_mult:
+  fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly"
+  assumes "content f = 1" "content g = 1"
+  shows   "content (f * g) = 1"
+proof (cases "f * g = 0")
+  case False
+  from assms have "f \<noteq> 0" "g \<noteq> 0" by auto
+
+  hence "f * g \<noteq> 0" by auto
+  {
+    assume "\<not>is_unit (content (f * g))"
+    with False have "\<exists>p. p dvd content (f * g) \<and> is_prime p"
+      by (intro prime_divisor_exists) simp_all
+    then obtain p where "p dvd content (f * g)" "is_prime p" by blast
+    from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g"
+      by (simp add: const_poly_dvd_iff_dvd_content)
+    moreover from \<open>is_prime p\<close> have "is_prime_elem [:p:]" by (simp add: lift_prime_elem_poly)
+    ultimately have "[:p:] dvd f \<or> [:p:] dvd g"
+      by (simp add: prime_dvd_mult_iff)
+    with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content)
+    with \<open>is_prime p\<close> have False by simp
+  }
+  hence "is_unit (content (f * g))" by blast
+  hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content)
+  thus ?thesis by simp
+qed (insert assms, auto)
+
+lemma content_mult:
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
+  shows "content (p * q) = content p * content q"
+proof -
+  from content_decompose[of p] guess p' . note p = this
+  from content_decompose[of q] guess q' . note q = this
+  have "content (p * q) = content p * content q * content (p' * q')"
+    by (subst p, subst q) (simp add: mult_ac normalize_mult)
+  also from p q have "content (p' * q') = 1" by (intro content_1_mult)
+  finally show ?thesis by simp
+qed
+
+lemma primitive_part_mult:
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
+proof -
+  have "primitive_part (p * q) = p * q div [:content (p * q):]"
+    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
+  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
+    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
+  also have "\<dots> = primitive_part p * primitive_part q"
+    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
+  finally show ?thesis .
+qed
+
+lemma primitive_part_smult:
+  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
+proof -
+  have "smult a p = [:a:] * p" by simp
+  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
+    by (subst primitive_part_mult) simp_all
+  finally show ?thesis .
+qed  
+
+lemma primitive_part_dvd_primitive_partI [intro]:
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
+  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
+  by (auto elim!: dvdE simp: primitive_part_mult)
+
+lemma content_msetprod: 
+  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
+  shows "content (msetprod A) = msetprod (image_mset content A)"
+  by (induction A) (simp_all add: content_mult mult_ac)
+
+lemma fract_poly_dvdD:
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  assumes "fract_poly p dvd fract_poly q" "content p = 1"
+  shows   "p dvd q"
+proof -
+  from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
+  from content_decompose_fract[of r] guess c r' . note r' = this
+  from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp  
+  from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+  have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
+  hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
+  have "1 = gcd a (normalize b)" by (simp add: ab)
+  also note eq'
+  also have "gcd a (a * content q) = a" by (simp add: gcd_proj1_if_dvd ab(4))
+  finally have [simp]: "a = 1" by simp
+  from eq ab have "q = p * ([:b:] * r')" by simp
+  thus ?thesis by (rule dvdI)
+qed
+
+lemma content_prod_eq_1_iff: 
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
+  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
+proof safe
+  assume A: "content (p * q) = 1"
+  {
+    fix p q :: "'a poly" assume "content p * content q = 1"
+    hence "1 = content p * content q" by simp
+    hence "content p dvd 1" by (rule dvdI)
+    hence "content p = 1" by simp
+  } note B = this
+  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
+    by (simp_all add: content_mult mult_ac)
+qed (auto simp: content_mult)
+
+end
+
+
+subsection \<open>Polynomials over a field are a Euclidean ring\<close>
+
+context
+begin
+
+private definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
+  "unit_factor_field_poly p = [:lead_coeff p:]"
+
+private definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
+  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
+
+private definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
+  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
+
+private lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
+    by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
+
+interpretation field_poly: 
+  euclidean_ring "op div" "op *" "op mod" "op +" "op -" 0 "1 :: 'a :: field poly" 
+    normalize_field_poly unit_factor_field_poly euclidean_size_field_poly uminus
+proof (standard, unfold dvd_field_poly)
+  fix p :: "'a poly"
+  show "unit_factor_field_poly p * normalize_field_poly p = p"
+    by (cases "p = 0") 
+       (simp_all add: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_nonzero)
+next
+  fix p :: "'a poly" assume "is_unit p"
+  thus "normalize_field_poly p = 1"
+    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
+next
+  fix p :: "'a poly" assume "p \<noteq> 0"
+  thus "is_unit (unit_factor_field_poly p)"
+    by (simp add: unit_factor_field_poly_def lead_coeff_nonzero is_unit_pCons_iff)
+qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
+       euclidean_size_field_poly_def intro!: degree_mod_less' degree_mult_right_le)
+
+private lemma field_poly_irreducible_imp_prime:
+  assumes "irreducible (p :: 'a :: field poly)"
+  shows   "is_prime_elem p"
+proof -
+  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
+  from field_poly.irreducible_imp_prime[of p] assms
+    show ?thesis unfolding irreducible_def is_prime_elem_def dvd_field_poly
+      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.is_prime_elem_def[OF A] by blast
+qed
+
+private lemma field_poly_msetprod_prime_factorization:
+  assumes "(x :: 'a :: field poly) \<noteq> 0"
+  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
+proof -
+  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
+  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
+    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
+  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
+qed
+
+private lemma field_poly_in_prime_factorization_imp_prime:
+  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
+  shows   "is_prime_elem p"
+proof -
+  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
+  have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
+             normalize_field_poly unit_factor_field_poly" ..
+  from field_poly.in_prime_factorization_imp_prime[of p x] assms
+    show ?thesis unfolding is_prime_elem_def dvd_field_poly
+      comm_semiring_1.is_prime_elem_def[OF A] normalization_semidom.is_prime_def[OF B] by blast
+qed
+
+
+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"
+  assumes "degree p \<noteq> 0"
+  shows   "irreducible p \<longleftrightarrow> irreducible (fract_poly p) \<and> content p = 1"
+proof safe
+  assume p: "irreducible p"
+
+  from content_decompose[of p] guess p' . note p' = this
+  hence "p = [:content p:] * p'" by simp
+  from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
+  moreover have "\<not>p' dvd 1"
+  proof
+    assume "p' dvd 1"
+    hence "degree p = 0" by (subst p') (auto simp: is_unit_poly_iff)
+    with assms show False by contradiction
+  qed
+  ultimately show [simp]: "content p = 1" by (simp add: is_unit_const_poly_iff)
+  
+  show "irreducible (map_poly to_fract p)"
+  proof (rule irreducibleI)
+    have "fract_poly p = 0 \<longleftrightarrow> p = 0" by (intro map_poly_eq_0_iff) auto
+    with assms show "map_poly to_fract p \<noteq> 0" by auto
+  next
+    show "\<not>is_unit (fract_poly p)"
+    proof
+      assume "is_unit (map_poly to_fract p)"
+      hence "degree (map_poly to_fract p) = 0"
+        by (auto simp: is_unit_poly_iff)
+      hence "degree p = 0" by (simp add: degree_map_poly)
+      with assms show False by contradiction
+   qed
+ next
+   fix q r assume qr: "fract_poly p = q * r"
+   from content_decompose_fract[of q] guess cg q' . note q = this
+   from content_decompose_fract[of r] guess cr r' . note r = this
+   from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
+   from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
+     by (simp add: q r)
+   from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+   hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
+   with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
+   hence "normalize b = gcd a b" by simp
+   also from ab(3) have "\<dots> = 1" .
+   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
+   
+   note eq
+   also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
+   also have "smult \<dots> (fract_poly (q' * r')) = fract_poly (smult b (q' * r'))" by simp
+   finally have "p = ([:b:] * q') * r'" by (simp del: fract_poly_smult)
+   from p and this have "([:b:] * q') dvd 1 \<or> r' dvd 1" by (rule irreducibleD)
+   hence "q' dvd 1 \<or> r' dvd 1" by (auto dest: dvd_mult_right simp del: mult_pCons_left)
+   hence "fract_poly q' dvd 1 \<or> fract_poly r' dvd 1" by (auto simp: fract_poly_is_unit)
+   with q r show "is_unit q \<or> is_unit r"
+     by (auto simp add: is_unit_smult_iff dvd_field_iff nz)
+ qed
+
+next
+
+  assume irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
+  show "irreducible p"
+  proof (rule irreducibleI)
+    from irred show "p \<noteq> 0" by auto
+  next
+    from irred show "\<not>p dvd 1"
+      by (auto simp: irreducible_def dest: fract_poly_is_unit)
+  next
+    fix q r assume qr: "p = q * r"
+    hence "fract_poly p = fract_poly q * fract_poly r" by simp
+    from irred and this have "fract_poly q dvd 1 \<or> fract_poly r dvd 1" 
+      by (rule irreducibleD)
+    with primitive qr show "q dvd 1 \<or> r dvd 1"
+      by (auto simp:  content_prod_eq_1_iff is_unit_fract_poly_iff)
+  qed
+qed
+
+private lemma irreducible_imp_prime_poly:
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  assumes "irreducible p"
+  shows   "is_prime_elem p"
+proof (cases "degree p = 0")
+  case True
+  with assms show ?thesis
+    by (auto simp: prime_elem_const_poly_iff irreducible_const_poly_iff
+             intro!: irreducible_imp_prime elim!: degree_eq_zeroE)
+next
+  case False
+  from assms False have irred: "irreducible (fract_poly p)" and primitive: "content p = 1"
+    by (simp_all add: nonconst_poly_irreducible_iff)
+  from irred have prime: "is_prime_elem (fract_poly p)" by (rule field_poly_irreducible_imp_prime)
+  show ?thesis
+  proof (rule is_prime_elemI)
+    fix q r assume "p dvd q * r"
+    hence "fract_poly p dvd fract_poly (q * r)" by (rule fract_poly_dvd)
+    hence "fract_poly p dvd fract_poly q * fract_poly r" by simp
+    from prime and this have "fract_poly p dvd fract_poly q \<or> fract_poly p dvd fract_poly r"
+      by (rule prime_divides_productD)
+    with primitive show "p dvd q \<or> p dvd r" by (auto dest: fract_poly_dvdD)
+  qed (insert assms, auto simp: irreducible_def)
+qed
+
+
+lemma degree_primitive_part_fract [simp]:
+  "degree (primitive_part_fract p) = degree p"
+proof -
+  have "p = smult (fract_content p) (fract_poly (primitive_part_fract p))"
+    by (simp add: content_times_primitive_part_fract)
+  also have "degree \<dots> = degree (primitive_part_fract p)"
+    by (auto simp: degree_map_poly)
+  finally show ?thesis ..
+qed
+
+lemma irreducible_primitive_part_fract:
+  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+  assumes "irreducible p"
+  shows   "irreducible (primitive_part_fract p)"
+proof -
+  from assms have deg: "degree (primitive_part_fract p) \<noteq> 0"
+    by (intro notI) 
+       (auto elim!: degree_eq_zeroE simp: irreducible_def is_unit_poly_iff dvd_field_iff)
+  hence [simp]: "p \<noteq> 0" by auto
+
+  note \<open>irreducible p\<close>
+  also have "p = [:fract_content p:] * fract_poly (primitive_part_fract p)" 
+    by (simp add: content_times_primitive_part_fract)
+  also have "irreducible \<dots> \<longleftrightarrow> irreducible (fract_poly (primitive_part_fract p))"
+    by (intro irreducible_mult_unit_left) (simp_all add: is_unit_poly_iff dvd_field_iff)
+  finally show ?thesis using deg
+    by (simp add: nonconst_poly_irreducible_iff)
+qed
+
+lemma is_prime_elem_primitive_part_fract:
+  fixes p :: "'a :: {idom_divide, ring_gcd, factorial_semiring, semiring_Gcd} fract poly"
+  shows "irreducible p \<Longrightarrow> is_prime_elem (primitive_part_fract p)"
+  by (intro irreducible_imp_prime_poly irreducible_primitive_part_fract)
+
+lemma irreducible_linear_field_poly:
+  fixes a b :: "'a::field"
+  assumes "b \<noteq> 0"
+  shows "irreducible [:a,b:]"
+proof (rule irreducibleI)
+  fix p q assume pq: "[:a,b:] = p * q"
+  also from this assms have "degree \<dots> = degree p + degree q" 
+    by (intro degree_mult_eq) auto
+  finally have "degree p = 0 \<or> degree q = 0" using assms by auto
+  with assms pq show "is_unit p \<or> is_unit q"
+    by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
+qed (insert assms, auto simp: is_unit_poly_iff)
+
+lemma is_prime_elem_linear_field_poly:
+  "(b :: 'a :: field) \<noteq> 0 \<Longrightarrow> is_prime_elem [:a,b:]"
+  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}"
+  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 is_prime_elem_linear_poly:
+  fixes a b :: "'a::{idom_divide,ring_gcd,factorial_semiring,semiring_Gcd}"
+  shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> is_prime_elem [:a,b:]"
+  by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
+
+  
+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"
+  assumes "p \<noteq> 0" "content p = 1"
+  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod A = normalize p"
+proof -
+  let ?P = "field_poly.prime_factorization (fract_poly p)"
+  define c where "c = msetprod (image_mset fract_content ?P)"
+  define c' where "c' = c * to_fract (lead_coeff p)"
+  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
+  define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
+  have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
+                      content (primitive_part_fract x))"
+    by (simp add: e_def content_msetprod multiset.map_comp o_def)
+  also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
+    by (intro image_mset_cong content_primitive_part_fract) auto
+  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
+  
+  have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
+          normalize_field_poly (fract_poly p)" by simp
+  also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
+    by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
+  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
+    by (subst field_poly_msetprod_prime_factorization) simp_all
+  also have "\<dots> = msetprod (image_mset id ?P)" by simp
+  also have "image_mset id ?P = 
+               image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
+    by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
+  also have "msetprod \<dots> = smult c (fract_poly e)"
+    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
+  also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
+    by (simp add: c'_def)
+  finally have eq: "fract_poly p = smult c' (fract_poly e)" .
+  also obtain b where b: "c' = to_fract b" "is_unit b"
+  proof -
+    from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
+    from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
+    with assms content_e have "a = normalize b" by (simp add: ab(4))
+    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
+    with ab ab' have "c' = to_fract b" by auto
+    from this and \<open>is_unit b\<close> show ?thesis by (rule that)
+  qed
+  hence "smult c' (fract_poly e) = fract_poly (smult b e)" by simp
+  finally have "p = smult b e" by (simp only: fract_poly_eq_iff)
+  hence "p = [:b:] * e" by simp
+  with b have "normalize p = normalize e" 
+    by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
+  also have "normalize e = msetprod A"
+    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
+  finally have "msetprod A = normalize p" ..
+  
+  have "is_prime_elem p" if "p \<in># A" for p
+    using that by (auto simp: A_def is_prime_elem_primitive_part_fract prime_imp_irreducible 
+                        dest!: field_poly_in_prime_factorization_imp_prime )
+  from this and \<open>msetprod A = normalize p\<close> show ?thesis
+    by (intro exI[of _ A]) blast
+qed
+
+lemma poly_prime_factorization_exists:
+  fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
+  assumes "p \<noteq> 0"
+  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> is_prime_elem p) \<and> msetprod 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> is_prime_elem p) \<and> msetprod 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 "msetprod B = [:content p:]"
+    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
+  moreover have "\<forall>p. p \<in># B \<longrightarrow> is_prime_elem p"
+    by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
+  ultimately show ?thesis by (intro exI[of _ "B + A"]) auto
+qed
+
+end
+
+
+subsection \<open>Typeclass instances\<close>
+
+instance poly :: (factorial_ring_gcd) factorial_semiring
+  by standard (rule poly_prime_factorization_exists)  
+
+instantiation poly :: (factorial_ring_gcd) factorial_ring_gcd
+begin
+
+definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  [code del]: "gcd_poly = gcd_factorial"
+
+definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  [code del]: "lcm_poly = lcm_factorial"
+  
+definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
+ [code del]: "Gcd_poly = Gcd_factorial"
+
+definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
+ [code del]: "Lcm_poly = Lcm_factorial"
+ 
+instance by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
+
+end
+
+instantiation poly :: ("{field,factorial_ring_gcd}") euclidean_ring
+begin
+
+definition euclidean_size_poly :: "'a poly \<Rightarrow> nat" where
+  "euclidean_size_poly p = (if p = 0 then 0 else 2 ^ degree p)"
+
+instance 
+  by standard (auto simp: euclidean_size_poly_def intro!: degree_mod_less' degree_mult_right_le)
+end
+
+instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
+  by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
+
+  
+subsection \<open>Polynomial GCD\<close>
+
+lemma gcd_poly_decompose:
+  fixes p q :: "'a :: factorial_ring_gcd poly"
+  shows "gcd p q = 
+           smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
+proof (rule sym, rule gcdI)
+  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
+          [:content p:] * primitive_part p" by (intro mult_dvd_mono) simp_all
+  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd p"
+    by simp
+next
+  have "[:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q) dvd
+          [:content q:] * primitive_part q" by (intro mult_dvd_mono) simp_all
+  thus "smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q)) dvd q"
+    by simp
+next
+  fix d assume "d dvd p" "d dvd q"
+  hence "[:content d:] * primitive_part d dvd 
+           [:gcd (content p) (content q):] * gcd (primitive_part p) (primitive_part q)"
+    by (intro mult_dvd_mono) auto
+  thus "d dvd smult (gcd (content p) (content q)) (gcd (primitive_part p) (primitive_part q))"
+    by simp
+qed (auto simp: normalize_smult)
+  
+
+lemma gcd_poly_pseudo_mod:
+  fixes p q :: "'a :: factorial_ring_gcd 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 -
+  define r s where "r = fst (pseudo_divmod p q)" and "s = snd (pseudo_divmod p q)"
+  define a where "a = [:coeff q (degree q) ^ (Suc (degree p) - degree q):]"
+  have [simp]: "primitive_part a = unit_factor a"
+    by (simp add: a_def unit_factor_poly_def unit_factor_power monom_0)
+  from nz have [simp]: "a \<noteq> 0" by (auto simp: a_def)
+  
+  have rs: "pseudo_divmod p q = (r, s)" by (simp add: r_def s_def)
+  have "gcd (q * r + s) q = gcd q s"
+    using gcd_add_mult[of q r s] by (simp add: gcd.commute add_ac mult_ac)
+  with pseudo_divmod(1)[OF nz rs]
+    have "gcd (p * a) q = gcd q s" by (simp add: a_def)
+  also from prim have "gcd (p * a) q = gcd p q"
+    by (subst gcd_poly_decompose)
+       (auto simp: primitive_part_mult gcd_mult_unit1 primitive_part_prim 
+             simp del: mult_pCons_right )
+  also from prim have "gcd q s = gcd q (primitive_part s)"
+    by (subst gcd_poly_decompose) (simp_all add: primitive_part_prim)
+  also have "s = pseudo_mod p q" by (simp add: s_def pseudo_mod_def)
+  finally show ?thesis .
+qed
+
+lemma degree_pseudo_mod_less:
+  assumes "q \<noteq> 0" "pseudo_mod p q \<noteq> 0"
+  shows   "degree (pseudo_mod p q) < degree q"
+  using pseudo_mod(2)[of q p] assms by auto
+
+function gcd_poly_code_aux :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  "gcd_poly_code_aux p q = 
+     (if q = 0 then normalize p else gcd_poly_code_aux q (primitive_part (pseudo_mod p q)))" 
+by auto
+termination
+  by (relation "measure ((\<lambda>p. if p = 0 then 0 else Suc (degree p)) \<circ> snd)")
+     (auto simp: degree_primitive_part degree_pseudo_mod_less)
+
+declare gcd_poly_code_aux.simps [simp del]
+
+lemma gcd_poly_code_aux_correct:
+  assumes "content p = 1" "q = 0 \<or> content q = 1"
+  shows   "gcd_poly_code_aux p q = gcd p q"
+  using assms
+proof (induction p q rule: gcd_poly_code_aux.induct)
+  case (1 p q)
+  show ?case
+  proof (cases "q = 0")
+    case True
+    thus ?thesis by (subst gcd_poly_code_aux.simps) auto
+  next
+    case False
+    hence "gcd_poly_code_aux p q = gcd_poly_code_aux q (primitive_part (pseudo_mod p q))"
+      by (subst gcd_poly_code_aux.simps) simp_all
+    also from "1.prems" False 
+      have "primitive_part (pseudo_mod p q) = 0 \<or> 
+              content (primitive_part (pseudo_mod p q)) = 1"
+      by (cases "pseudo_mod p q = 0") auto
+    with "1.prems" False 
+      have "gcd_poly_code_aux q (primitive_part (pseudo_mod p q)) = 
+              gcd q (primitive_part (pseudo_mod p q))"
+      by (intro 1) simp_all
+    also from "1.prems" False 
+      have "\<dots> = gcd p q" by (intro gcd_poly_pseudo_mod [symmetric]) auto
+    finally show ?thesis .
+  qed
+qed
+
+definition gcd_poly_code 
+    :: "'a :: factorial_ring_gcd poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
+  where "gcd_poly_code p q = 
+           (if p = 0 then normalize q else if q = 0 then normalize p else
+              smult (gcd (content p) (content q)) 
+                (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
+
+lemma lcm_poly_code [code]: 
+  fixes p q :: "'a :: factorial_ring_gcd poly"
+  shows "lcm p q = normalize (p * q) div gcd p q"
+  by (rule lcm_gcd)
+
+lemma gcd_poly_code [code]: "gcd p q = gcd_poly_code p q"
+  by (simp add: gcd_poly_code_def gcd_poly_code_aux_correct gcd_poly_decompose [symmetric])
+
+declare Gcd_set
+  [where ?'a = "'a :: factorial_ring_gcd poly", code]
+
+declare Lcm_set
+  [where ?'a = "'a :: factorial_ring_gcd poly", code]
+  
+value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
+
+end
diff -r 58ccbc73a172 -r a3fe3250d05d src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 14 12:21:12 2016 +0200
+++ b/src/HOL/ROOT	Wed Jul 13 15:46:52 2016 +0200
@@ -39,7 +39,6 @@
     Product_Lexorder
     Product_Order
     Finite_Lattice
-    Polynomial_GCD_euclidean
     (*data refinements and dependent applications*)
     AList_Mapping
     Code_Binary_Nat