# HG changeset patch
# User haftmann
# Date 1507494501 -7200
# Node ID 274b4edca85954b0f5ffcdb14276747dc1eb835a
# Parent  3f9bb52082c414903e547f10922d33533dc9d8e0
Polynomial_Factorial does not depend on Field_as_Ring as such

diff -r 3f9bb52082c4 -r 274b4edca859 NEWS
--- a/NEWS	Sun Oct 08 22:28:20 2017 +0200
+++ b/NEWS	Sun Oct 08 22:28:21 2017 +0200
@@ -44,6 +44,11 @@
     higher-order quantifiers. An 'smt_explicit_application' option has been
     added to control this. INCOMPATIBILITY.
 
+* Theory HOL-Computational_Algebra.Polynomial_Factorial does not
+provide instances of rat, real, complex as factorial rings etc.
+Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of
+need. INCOMPATIBILITY.
+
 * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
 with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
 
diff -r 3f9bb52082c4 -r 274b4edca859 src/HOL/Computational_Algebra/Computational_Algebra.thy
--- a/src/HOL/Computational_Algebra/Computational_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -12,6 +12,7 @@
   Nth_Powers
   Polynomial_FPS
   Polynomial
+  Polynomial_Factorial
   Primes
   Squarefree
 begin
diff -r 3f9bb52082c4 -r 274b4edca859 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -12,6 +12,7 @@
   HOL.Deriv
   "HOL-Library.More_List"
   "HOL-Library.Infinite_Set"
+  Factorial_Ring
 begin
 
 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
@@ -2881,167 +2882,6 @@
 qed
 
 
-subsection \<open>Content and primitive part of a polynomial\<close>
-
-definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
-  where "content p = gcd_list (coeffs p)"
-
-lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
-  by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
-
-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: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
-  for c :: "'a::semiring_gcd"
-proof (cases "p = 0")
-  case True
-  then show ?thesis by simp
-next
-  case 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"
-    then show "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_fin_iff dvd_mult_unit_iff)
-  finally show ?thesis .
-qed
-
-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"
-proof (cases "p = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then show ?thesis
-    by (cases "n \<le> degree p")
-      (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd)
-qed
-
-lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
-  by (simp add: content_def Gcd_fin_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)"
-  then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
-  then show "content p = 1" by simp
-qed auto
-
-lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
-  by (simp add: content_def coeffs_smult Gcd_fin_mult)
-
-lemma content_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 poly \<Rightarrow> 'a poly"
-  where "primitive_part p = 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]: "smult (content p) (primitive_part p) = p"
-  for p :: "'a :: semiring_gcd poly"
-proof (cases "p = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then show ?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
-
-lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
-proof (cases "p = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have "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
-
-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 (primitive_part p) * content p"
-    by (simp del: content_times_primitive_part add: ac_simps)
-  finally have "1 * content p = content (primitive_part p) * content p"
-    by simp
-  then have "1 * content p div content p = content (primitive_part p) * content p div content p"
-    by simp
-  with assms show ?thesis
-    by simp
-qed
-
-lemma content_decompose:
-  obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
-proof (cases "p = 0")
-  case True
-  then show ?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 (rule 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 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 True
-  then show ?thesis by simp
-next
-  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
-
-
 subsection \<open>Division of polynomials\<close>
 
 subsubsection \<open>Division in general\<close>
@@ -3649,16 +3489,6 @@
   finally show ?thesis .
 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
-
 inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
   where
     eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
@@ -4502,6 +4332,387 @@
   qed
 qed
 
+
+subsection \<open>Primality and irreducibility in polynomial rings\<close>
+
+lemma prod_mset_const_poly: "(\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
+  by (induct A) (simp_all add: ac_simps)
+
+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 add: is_unit_const_poly_iff)
+  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
+next
+  assume A: "irreducible [:c:]"
+  then have "c \<noteq> 0" and "\<not> c dvd 1"
+    by (auto simp add: irreducible_def is_unit_const_poly_iff)
+  then 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)
+    then show "a dvd 1 \<or> b dvd 1"
+      by (auto simp add: is_unit_const_poly_iff)
+  qed
+qed
+
+lemma lift_prime_elem_poly:
+  assumes "prime_elem (c :: 'a :: semidom)"
+  shows   "prime_elem [:c:]"
+proof (rule 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 \<le> degree b"
+      by (auto intro: le_degree)
+    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
+    have "i \<le> m" if "\<not>c dvd coeff b i" for i
+      unfolding m_def by (rule Greatest_le_nat[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 sum.insert) simp_all
+      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
+      moreover have "c dvd ?S"
+      proof (rule dvd_sum)
+        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_elem_dvd_mult_iff)
+    qed
+    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
+  }
+  then show "[:c:] dvd a \<or> [:c:] dvd b" by blast
+next
+  from assms show "[:c:] \<noteq> 0" and "\<not> [:c:] dvd 1"
+    by (simp_all add: prime_elem_def is_unit_const_poly_iff)
+qed
+
+lemma prime_elem_const_poly_iff:
+  fixes c :: "'a :: semidom"
+  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
+proof
+  assume A: "prime_elem [:c:]"
+  show "prime_elem c"
+  proof (rule 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_elem_dvd_multD)
+    thus "c dvd a \<or> c dvd b" by simp
+  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
+qed (auto intro: lift_prime_elem_poly)
+
+
+subsection \<open>Content and primitive part of a polynomial\<close>
+
+definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
+  where "content p = gcd_list (coeffs p)"
+
+lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
+  by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
+
+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: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
+  for c :: "'a::semiring_gcd"
+proof (cases "p = 0")
+  case True
+  then show ?thesis by simp
+next
+  case 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"
+    then show "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_fin_iff dvd_mult_unit_iff)
+  finally show ?thesis .
+qed
+
+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"
+proof (cases "p = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then show ?thesis
+    by (cases "n \<le> degree p")
+      (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd)
+qed
+
+lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
+  by (simp add: content_def Gcd_fin_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)"
+  then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
+  then show "content p = 1" by simp
+qed auto
+
+lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
+  by (simp add: content_def coeffs_smult Gcd_fin_mult)
+
+lemma content_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 poly \<Rightarrow> 'a poly"
+  where "primitive_part p = 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]: "smult (content p) (primitive_part p) = p"
+  for p :: "'a :: semiring_gcd poly"
+proof (cases "p = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then show ?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
+
+lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
+proof (cases "p = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have "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
+
+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 (primitive_part p) * content p"
+    by (simp del: content_times_primitive_part add: ac_simps)
+  finally have "1 * content p = content (primitive_part p) * content p"
+    by simp
+  then have "1 * content p div content p = content (primitive_part p) * content p div content p"
+    by simp
+  with assms show ?thesis
+    by simp
+qed
+
+lemma content_decompose:
+  obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
+proof (cases "p = 0")
+  case True
+  then show ?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 (rule 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 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 True
+  then show ?thesis by simp
+next
+  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
+
+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_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 have "content (p' * q') = 1"
+  proof (cases "p' * q' = 0")
+    case True
+    with \<open>content p' = 1\<close> \<open>content q' = 1\<close> show ?thesis
+      by auto
+  next  
+    case False
+    from \<open>content p' = 1\<close> \<open>content q' = 1\<close>
+    have "p' \<noteq> 0" "q' \<noteq> 0"
+      by auto
+    then have "p' * q' \<noteq> 0"
+      by auto
+    have "is_unit (content (p' * q'))"
+    proof (rule ccontr)      
+      assume "\<not> is_unit (content (p' * q'))"
+      with False have "\<exists>p. p dvd content (p' * q') \<and> prime p"
+        by (intro prime_divisor_exists) simp_all
+      then obtain p where "p dvd content (p' * q')" "prime p"
+        by blast
+      from \<open>p dvd content (p' * q')\<close> have "[:p:] dvd p' * q'"
+        by (simp add: const_poly_dvd_iff_dvd_content)
+      moreover from \<open>prime p\<close> have "prime_elem [:p:]"
+        by (simp add: lift_prime_elem_poly)
+      ultimately have "[:p:] dvd p' \<or> [:p:] dvd q'"
+        by (simp add: prime_elem_dvd_mult_iff)
+      with \<open>content p' = 1\<close> \<open>content q' = 1\<close> have "is_unit p"
+        by (simp add: const_poly_dvd_iff_dvd_content)
+      with \<open>prime p\<close> show False
+        by simp
+    qed    
+    then have "normalize (content (p' * q')) = 1"
+      by (simp add: is_unit_normalize del: normalize_content)
+    then show ?thesis
+      by simp
+  qed
+  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_prod_mset: 
+  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
+  shows "content (prod_mset A) = prod_mset (image_mset content A)"
+  by (induction A) (simp_all add: content_mult mult_ac)
+
+lemma content_prod_eq_1_iff: 
+  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
+  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)
+
+
 no_notation cCons (infixr "##" 65)
 
 end
diff -r 3f9bb52082c4 -r 274b4edca859 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -1,61 +1,20 @@
 (*  Title:      HOL/Computational_Algebra/Polynomial_Factorial.thy
-    Author:     Brian Huffman
-    Author:     Clemens Ballarin
-    Author:     Amine Chaieb
-    Author:     Florian Haftmann
     Author:     Manuel Eberl
 *)
 
+section \<open>Polynomials, fractions and rings\<close>
+
 theory Polynomial_Factorial
 imports 
   Complex_Main
   Polynomial
   Normalized_Fraction
-  Field_as_Ring
 begin
 
-subsection \<open>Various facts about polynomials\<close>
-
-lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
-  by (induct A) (simp_all add: ac_simps)
-
-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 add: is_unit_const_poly_iff)
-  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
-next
-  assume A: "irreducible [:c:]"
-  then have "c \<noteq> 0" and "\<not> c dvd 1"
-    by (auto simp add: irreducible_def is_unit_const_poly_iff)
-  then 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)
-    then show "a dvd 1 \<or> b dvd 1"
-      by (auto simp add: is_unit_const_poly_iff)
-  qed
-qed
-
-
 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"
+definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
+  where "to_fract x = Fract x 1"
   \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
 
 lemma to_fract_0 [simp]: "to_fract 0 = 0"
@@ -429,39 +388,6 @@
   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_prod_mset: 
-  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
-  shows "content (prod_mset A) = prod_mset (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"
@@ -481,104 +407,80 @@
   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>
 
-definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
-  "unit_factor_field_poly p = [:lead_coeff p:]"
-
-definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
-  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
-
-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)" 
-
-lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
-  by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
+context
+begin
 
 interpretation field_poly: 
   unique_euclidean_ring where zero = "0 :: 'a :: field poly"
-    and one = 1 and plus = plus and uminus = uminus and minus = minus
+    and one = 1 and plus = plus
+    and uminus = uminus and minus = minus
     and times = times
-    and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
-    and euclidean_size = euclidean_size_field_poly
+    and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
+    and unit_factor = "\<lambda>p. [:lead_coeff p:]"
+    and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
     and uniqueness_constraint = top
     and divide = divide and modulo = modulo
-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)
-next
-  fix p :: "'a poly" assume "is_unit p"
-  then show "unit_factor_field_poly p = p"
-    by (elim is_unit_polyE) (auto simp: unit_factor_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 is_unit_pCons_iff)
-next
-  fix p q s :: "'a poly" assume "s \<noteq> 0"
-  moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q"
-  ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)"
-    by (auto simp add: euclidean_size_field_poly_def degree_mult_eq)
-next
-  fix p q r :: "'a poly" assume "p \<noteq> 0"
-  moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p"
-  ultimately show "(q * p + r) div p = q"
-    by (cases "r = 0")
-      (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less)
-qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
-       euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
+  rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
+    and "comm_monoid_mult.prod_mset times 1 = prod_mset"
+    and "comm_semiring_1.irreducible times 1 0 = irreducible"
+    and "comm_semiring_1.prime_elem times 1 0 = prime_elem"
+proof -
+  show "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
+    by (simp add: dvd_dict)
+  show "comm_monoid_mult.prod_mset times 1 = prod_mset"
+    by (simp add: prod_mset_dict)
+  show "comm_semiring_1.irreducible times 1 0 = irreducible"
+    by (simp add: irreducible_dict)
+  show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
+    by (simp add: prime_elem_dict)
+  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
+    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
+    (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
+  proof (standard, fold dvd_dict)
+    fix p :: "'a poly"
+    show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
+      by (cases "p = 0") simp_all
+  next
+    fix p :: "'a poly" assume "is_unit p"
+    then show "[:lead_coeff p:] = p"
+      by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps)
+  next
+    fix p :: "'a poly" assume "p \<noteq> 0"
+    then show "is_unit [:lead_coeff p:]"
+      by (simp add: is_unit_pCons_iff)
+  next
+    fix p q s :: "'a poly" assume "s \<noteq> 0"
+    moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)"
+    ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
+      by (auto simp add: degree_mult_eq)
+  next
+    fix p q r :: "'a poly" assume "p \<noteq> 0"
+    moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
+    < (if p = 0 then 0 else 2 ^ degree p)"
+    ultimately show "(q * p + r) div p = q"
+      by (cases "r = 0") (auto simp add: div_poly_less)
+  qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
+qed
 
 lemma field_poly_irreducible_imp_prime:
-  assumes "irreducible (p :: 'a :: field poly)"
-  shows   "prime_elem p"
-proof -
-  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
-  from field_poly.irreducible_imp_prime_elem[of p] assms
-    show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
-      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
-qed
+  "prime_elem p" if "irreducible p" for p :: "'a :: field poly"
+  using that by (fact field_poly.irreducible_imp_prime_elem)
 
 lemma field_poly_prod_mset_prime_factorization:
-  assumes "(x :: 'a :: field poly) \<noteq> 0"
-  shows   "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x"
-proof -
-  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
-  have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset"
-    by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def)
-  with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp
-qed
+  "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
+  if "p \<noteq> 0" for p :: "'a :: field poly"
+  using that by (fact field_poly.prod_mset_prime_factorization)
 
 lemma field_poly_in_prime_factorization_imp_prime:
-  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
-  shows   "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 
-             unit_factor_field_poly normalize_field_poly" ..
-  from field_poly.in_prime_factors_imp_prime [of p x] assms
-    show ?thesis unfolding prime_elem_def dvd_field_poly
-      comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
-qed
+  "prime_elem p" if "p \<in># field_poly.prime_factorization x"
+  for p :: "'a :: field poly"
+  by (rule field_poly.prime_imp_prime_elem, rule field_poly.in_prime_factors_imp_prime)
+    (fact that)
 
 
 subsection \<open>Primality and irreducibility in polynomial rings\<close>
@@ -658,9 +560,6 @@
   qed
 qed
 
-context
-begin
-
 private lemma irreducible_imp_prime_poly:
   fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   assumes "irreducible p"
@@ -686,7 +585,6 @@
   qed (insert assms, auto simp: irreducible_def)
 qed
 
-
 lemma degree_primitive_part_fract [simp]:
   "degree (primitive_part_fract p) = degree p"
 proof -
@@ -749,14 +647,9 @@
   shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
   by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
 
-end
-
  
 subsection \<open>Prime factorisation of polynomials\<close>   
 
-context
-begin 
-
 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"
@@ -775,11 +668,12 @@
   finally have content_e: "content e = 1"
     by simp    
   
-  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 monom_0 degree_map_poly coeff_map_poly)
-  also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
+  from \<open>p \<noteq> 0\<close> have "fract_poly p = [:lead_coeff (fract_poly p):] * 
+    smult (inverse (lead_coeff (fract_poly p))) (fract_poly p)"
+    by simp 
+  also have "[:lead_coeff (fract_poly p):] = [:to_fract (lead_coeff p):]" 
+    by (simp add: monom_0 degree_map_poly coeff_map_poly)
+  also from assms have "smult (inverse (lead_coeff (fract_poly p))) (fract_poly p) = prod_mset ?P" 
     by (subst field_poly_prod_mset_prime_factorization) simp_all
   also have "\<dots> = prod_mset (image_mset id ?P)" by simp
   also have "image_mset id ?P = 
diff -r 3f9bb52082c4 -r 274b4edca859 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Oct 08 22:28:20 2017 +0200
+++ b/src/HOL/ROOT	Sun Oct 08 22:28:21 2017 +0200
@@ -71,7 +71,6 @@
     Computational_Algebra
     (*conflicting type class instantiations and dependent applications*)
     Field_as_Ring
-    Polynomial_Factorial
 
 session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
   description {*