# HG changeset patch
# User haftmann
# Date 1481984533 -3600
# Node ID 240a39af9ec4d73738d5d2ec08380617fd8dc412
# Parent  6621d91d3c8a87bb99ccd39e2a81b38f781eb2aa
restructured matter on polynomials and normalized fractions

diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fields.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -506,6 +506,21 @@
   "y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y"
   by (simp add: add_divide_distrib add.commute)
 
+lemma dvd_field_iff:
+  "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
+proof (cases "a = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "b = a * (b / a)"
+    by (simp add: field_simps)
+  then have "a dvd b" ..
+  with False show ?thesis
+    by simp
+qed
+
 end
 
 class field_char_0 = field + ring_char_0
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -278,6 +278,16 @@
   done
 
 
+subsection \<open>Yet another induction principle on the natural numbers\<close>
+
+lemma nat_descend_induct [case_names base descend]:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes H1: "\<And>k. k > n \<Longrightarrow> P k"
+  assumes H2: "\<And>k. 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"])+
+
+
 subsection \<open>Tool setup\<close>
 
 ML_file "Tools/Function/termination.ML"
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/GCD.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -639,7 +639,6 @@
     using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
 qed
 
-
 lemma divides_mult:
   assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   shows "a * b dvd c"
@@ -695,6 +694,10 @@
   using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
   by blast
 
+lemma coprime_mul_eq':
+  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
+  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
+
 lemma gcd_coprime:
   assumes c: "gcd a b \<noteq> 0"
     and a: "a = a' * gcd a b"
@@ -958,6 +961,24 @@
   ultimately show ?thesis by (rule that)
 qed
 
+lemma coprime_crossproduct':
+  fixes a b c d
+  assumes "b \<noteq> 0"
+  assumes unit_factors: "unit_factor b = unit_factor d"
+  assumes coprime: "coprime a b" "coprime c d"
+  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+  assume eq: "a * d = b * c"
+  hence "normalize a * normalize d = normalize c * normalize b"
+    by (simp only: normalize_mult [symmetric] mult_ac)
+  with coprime have "normalize b = normalize d"
+    by (subst (asm) coprime_crossproduct) simp_all
+  from this and unit_factors show "b = d"
+    by (rule normalize_unit_factor_eqI)
+  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
 end
 
 class ring_gcd = comm_ring_1 + semiring_gcd
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -657,6 +657,12 @@
   for x :: nat
   unfolding Greatest_def by (rule GreatestM_nat_le) auto
 
+lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
+  apply (erule exE)
+  apply (rule GreatestI)
+   apply assumption+
+  done
+
 
 subsection \<open>An aside: bounded accessible part\<close>
 
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Library/Field_as_Ring.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Field_as_Ring.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -0,0 +1,108 @@
+(*  Title:      HOL/Library/Field_as_Ring.thy
+    Author:     Manuel Eberl
+*)
+
+theory Field_as_Ring
+imports 
+  Complex_Main
+  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
+begin
+
+context field
+begin
+
+subclass idom_divide ..
+
+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]: "modulo_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]: "modulo_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]: "modulo_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
+
+end
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -1738,6 +1738,10 @@
   "(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}"
   by (metis image_mset_cong split_cong)
 
+lemma image_mset_const_eq:
+  "{#c. a \<in># M#} = replicate_mset (size M) c"
+  by (induct M) simp_all
+
 
 subsection \<open>Further conversions\<close>
 
@@ -2310,6 +2314,9 @@
 translations
   "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST prod_mset (CONST image_mset (\<lambda>i. b) A)"
 
+lemma prod_mset_constant [simp]: "(\<Prod>_\<in>#A. c) = c ^ size A"
+  by (simp add: image_mset_const_eq)
+
 lemma (in comm_monoid_mult) prod_mset_subset_imp_dvd:
   assumes "A \<subseteq># B"
   shows   "prod_mset A dvd prod_mset B"
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Library/Normalized_Fraction.thy
--- a/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Normalized_Fraction.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -1,3 +1,7 @@
+(*  Title:      HOL/Library/Normalized_Fraction.thy
+    Author:     Manuel Eberl
+*)
+
 theory Normalized_Fraction
 imports 
   Main 
@@ -5,75 +9,6 @@
   "~~/src/HOL/Library/Fraction_Field"
 begin
 
-lemma dvd_neg_div': "y dvd (x :: 'a :: idom_divide) \<Longrightarrow> -x div y = - (x div y)"
-apply (case_tac "y = 0") apply simp
-apply (auto simp add: dvd_def)
-apply (subgoal_tac "-(y * k) = y * - k")
-apply (simp only:)
-apply (erule nonzero_mult_div_cancel_left)
-apply simp
-done
-
-(* TODO Move *)
-lemma (in semiring_gcd) coprime_mul_eq': "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
-  using coprime_mul_eq[of d a b] by (simp add: gcd.commute)
-
-lemma dvd_div_eq_0_iff:
-  assumes "b dvd (a :: 'a :: semidom_divide)"
-  shows   "a div b = 0 \<longleftrightarrow> a = 0"
-  using assms by (elim dvdE, cases "b = 0") simp_all  
-
-lemma dvd_div_eq_0_iff':
-  assumes "b dvd (a :: 'a :: semiring_div)"
-  shows   "a div b = 0 \<longleftrightarrow> a = 0"
-  using assms by (elim dvdE, cases "b = 0") simp_all
-
-lemma unit_div_eq_0_iff:
-  assumes "is_unit (b :: 'a :: {algebraic_semidom,semidom_divide})"
-  shows   "a div b = 0 \<longleftrightarrow> a = 0"
-  by (rule dvd_div_eq_0_iff) (insert assms, auto)  
-
-lemma unit_div_eq_0_iff':
-  assumes "is_unit (b :: 'a :: semiring_div)"
-  shows   "a div b = 0 \<longleftrightarrow> a = 0"
-  by (rule dvd_div_eq_0_iff) (insert assms, auto)
-
-lemma dvd_div_eq_cancel:
-  "a div c = b div c \<Longrightarrow> (c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
-  by (elim dvdE, cases "c = 0") simp_all
-
-lemma dvd_div_eq_iff:
-  "(c :: 'a :: semiring_div) dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
-  by (elim dvdE, cases "c = 0") simp_all
-
-lemma normalize_imp_eq:
-  "normalize a = normalize b \<Longrightarrow> unit_factor a = unit_factor b \<Longrightarrow> a = b"
-  by (cases "a = 0 \<or> b = 0")
-     (auto simp add: div_unit_factor [symmetric] unit_div_cancel simp del: div_unit_factor)
-    
-lemma coprime_crossproduct':
-  fixes a b c d :: "'a :: semiring_gcd"
-  assumes nz: "b \<noteq> 0"
-  assumes unit_factors: "unit_factor b = unit_factor d"
-  assumes coprime: "coprime a b" "coprime c d"
-  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
-  assume eq: "a * d = b * c"
-  hence "normalize a * normalize d = normalize c * normalize b"
-    by (simp only: normalize_mult [symmetric] mult_ac)
-  with coprime have "normalize b = normalize d"
-    by (subst (asm) coprime_crossproduct) simp_all
-  from this and unit_factors show "b = d" by (rule normalize_imp_eq)
-  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
-  with nz \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-  
-     
-lemma div_mult_unit2: "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
-  by (subst dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
-(* END TODO *)
-
-
 definition quot_to_fract :: "'a :: {idom} \<times> 'a \<Rightarrow> 'a fract" where
   "quot_to_fract = (\<lambda>(a,b). Fraction_Field.Fract a b)"
 
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -877,7 +877,7 @@
   by (induct n, simp add: monom_0, simp add: monom_Suc)
 
 lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)"
-  by (auto simp add: poly_eq_iff coeff_Poly_eq nth_default_def)
+  by (auto simp add: poly_eq_iff nth_default_def)
 
 lemma degree_smult_eq [simp]:
   fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
@@ -1064,6 +1064,111 @@
     by (rule le_trans[OF degree_mult_le], insert insert, auto)
 qed simp
 
+
+subsection \<open>Mapping polynomials\<close>
+
+definition map_poly 
+     :: "('a :: zero \<Rightarrow> 'b :: zero) \<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)
+
+
 subsection \<open>Conversions from natural numbers\<close>
 
 lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
@@ -1086,6 +1191,7 @@
 lemma numeral_poly: "numeral n = [:numeral n:]"
   by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
 
+
 subsection \<open>Lemmas about divisibility\<close>
 
 lemma dvd_smult: "p dvd q \<Longrightarrow> p dvd smult a q"
@@ -1137,6 +1243,11 @@
 apply (simp add: coeff_mult_degree_sum)
 done
 
+lemma degree_mult_eq_0:
+  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)
+
 lemma degree_mult_right_le:
   fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   assumes "q \<noteq> 0"
@@ -1290,6 +1401,75 @@
 text \<open>TODO: Simplification rules for comparisons\<close>
 
 
+subsection \<open>Leading coefficient\<close>
+
+definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
+  "lead_coeff p= coeff p (degree p)"
+
+lemma lead_coeff_pCons[simp]:
+    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
+    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
+unfolding lead_coeff_def by auto
+
+lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
+  unfolding lead_coeff_def by auto
+
+lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
+  by (induction xs) (simp_all add: coeff_mult)
+
+lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
+  by (induction n) (simp_all add: coeff_mult)
+
+lemma lead_coeff_mult:
+   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)
+
+lemma lead_coeff_add_le:
+  assumes "degree p < degree q"
+  shows "lead_coeff (p+q) = lead_coeff q" 
+using assms unfolding lead_coeff_def
+by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
+
+lemma lead_coeff_minus:
+  "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_1 [simp]: "lead_coeff 1 = 1"
+  by (simp add: lead_coeff_def)
+
+lemma lead_coeff_of_nat [simp]:
+  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
+  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
+
+lemma lead_coeff_numeral [simp]: 
+  "lead_coeff (numeral n) = numeral n"
+  unfolding lead_coeff_def
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+lemma lead_coeff_power: 
+  "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"
+  by (simp add: lead_coeff_def)
+
+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>Synthetic division and polynomial roots\<close>
 
 text \<open>
@@ -1555,7 +1735,7 @@
 
 
 
-subsection\<open>Pseudo-Division and Division of Polynomials\<close>
+subsection \<open>Pseudo-Division and Division of Polynomials\<close>
 
 text\<open>This part is by René Thiemann and Akihisa Yamada.\<close>
 
@@ -1838,15 +2018,172 @@
 lemma divide_poly_0: "f div 0 = (0 :: 'a poly)"
   by (simp add: divide_poly_def Let_def divide_poly_main_0)
 
-instance by (standard, auto simp: divide_poly divide_poly_0)
+instance
+  by standard (auto simp: divide_poly divide_poly_0)
+
 end
 
-
 instance poly :: (idom_divide) algebraic_semidom ..
 
-
-
-subsubsection\<open>Division in Field Polynomials\<close>
+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_div_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)
+
+lemma is_unit_monom_0:
+  fixes a :: "'a::field"
+  assumes "a \<noteq> 0"
+  shows "is_unit (monom a 0)"
+proof
+  from assms show "1 = monom a 0 * monom (inverse a) 0"
+    by (simp add: mult_monom)
+qed
+
+lemma is_unit_triv:
+  fixes a :: "'a::field"
+  assumes "a \<noteq> 0"
+  shows "is_unit [:a:]"
+  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
+
+lemma is_unit_iff_degree:
+  assumes "p \<noteq> (0 :: _ :: field poly)"
+  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q
+  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
+  with assms show ?P by (simp add: is_unit_triv)
+next
+  assume ?P
+  then obtain q where "q \<noteq> 0" "p * q = 1" ..
+  then have "degree (p * q) = degree 1"
+    by simp
+  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
+    by (simp add: degree_mult_eq)
+  then show ?Q by simp
+qed
+
+lemma is_unit_pCons_iff:
+  "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:
+  fixes p :: "'a::field poly"
+  assumes "is_unit p"
+  shows "monom (coeff p (degree p)) 0 = p"
+  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
+
+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_polyE:
+  fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"
+  assumes "p dvd 1" obtains c where "p = [:c:]" "c dvd 1"
+proof -
+  from assms obtain q where "1 = p * q"
+    by (rule dvdE)
+  then have "p \<noteq> 0" and "q \<noteq> 0"
+    by auto
+  from \<open>1 = p * q\<close> have "degree 1 = degree (p * q)"
+    by simp
+  also from \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> have "\<dots> = degree p + degree q"
+    by (simp add: degree_mult_eq)
+  finally have "degree p = 0" by simp
+  with degree_eq_zeroE obtain c where c: "p = [:c:]" .
+  moreover with \<open>p dvd 1\<close> have "c dvd 1"
+    by (simp add: is_unit_const_poly_iff)
+  ultimately show thesis
+    by (rule that)
+qed
+
+lemma is_unit_polyE':
+  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)
+  with assms have "p = [:a:]" and "a \<noteq> 0"
+    by (simp_all add: is_unit_pCons_iff)
+  with that show thesis by (simp add: monom_0)
+qed
+
+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)"
+  by (auto elim: is_unit_polyE simp add: is_unit_const_poly_iff)
+
+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"
+
+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 normalize_poly_eq_div:
+  "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)
+
+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
+
+
+subsubsection \<open>Division in Field Polynomials\<close>
 
 text\<open>
  This part connects the above result to the division of field polynomials.
@@ -1978,58 +2315,6 @@
 
 end
 
-lemma is_unit_monom_0:
-  fixes a :: "'a::field"
-  assumes "a \<noteq> 0"
-  shows "is_unit (monom a 0)"
-proof
-  from assms show "1 = monom a 0 * monom (inverse a) 0"
-    by (simp add: mult_monom)
-qed
-
-lemma is_unit_triv:
-  fixes a :: "'a::field"
-  assumes "a \<noteq> 0"
-  shows "is_unit [:a:]"
-  using assms by (simp add: is_unit_monom_0 monom_0 [symmetric])
-
-lemma is_unit_iff_degree:
-  assumes "p \<noteq> (0 :: _ :: field poly)"
-  shows "is_unit p \<longleftrightarrow> degree p = 0" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?Q
-  then obtain a where "p = [:a:]" by (rule degree_eq_zeroE)
-  with assms show ?P by (simp add: is_unit_triv)
-next
-  assume ?P
-  then obtain q where "q \<noteq> 0" "p * q = 1" ..
-  then have "degree (p * q) = degree 1"
-    by simp
-  with \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "degree p + degree q = 0"
-    by (simp add: degree_mult_eq)
-  then show ?Q by simp
-qed
-
-lemma is_unit_pCons_iff:
-  "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:
-  fixes p :: "'a::field poly"
-  assumes "is_unit p"
-  shows "monom (coeff p (degree p)) 0 = p"
-  using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
-
-lemma is_unit_polyE:
-  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)
-  with assms have "p = [:a:]" and "a \<noteq> 0"
-    by (simp_all add: is_unit_pCons_iff)
-  with that show thesis by (simp add: monom_0)
-qed
-
 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]
@@ -2860,18 +3145,11 @@
   by (cases "finite A", induction rule: finite_induct)
      (simp_all add: pcompose_1 pcompose_mult)
 
-
-(* The remainder of this section and the next were contributed by Wenda Li *)
-
-lemma degree_mult_eq_0:
-  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)
-
-lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp) 
+lemma pcompose_const [simp]: "pcompose [:a:] q = [:a:]"
+  by (subst pcompose_pCons) simp
 
 lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]"
-  by (induct p) (auto simp add:pcompose_pCons)
+  by (induct p) (auto simp add: pcompose_pCons)
 
 lemma degree_pcompose:
   fixes p q:: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
@@ -2932,53 +3210,6 @@
   thus ?thesis using \<open>p=[:a:]\<close> by simp
 qed
 
-
-subsection \<open>Leading coefficient\<close>
-
-definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
-  "lead_coeff p= coeff p (degree p)"
-
-lemma lead_coeff_pCons[simp]:
-    "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p"
-    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
-unfolding lead_coeff_def by auto
-
-lemma lead_coeff_0[simp]:"lead_coeff 0 =0" 
-  unfolding lead_coeff_def by auto
-
-lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)"
-  by (induction xs) (simp_all add: coeff_mult)
-
-lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
-  by (induction n) (simp_all add: coeff_mult)
-
-lemma lead_coeff_mult:
-   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)
-
-lemma lead_coeff_add_le:
-  assumes "degree p < degree q"
-  shows "lead_coeff (p+q) = lead_coeff q" 
-using assms unfolding lead_coeff_def
-by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)
-
-lemma lead_coeff_minus:
-  "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::{comm_semiring_1,semiring_no_zero_divisors} poly"
   assumes "degree q > 0" 
@@ -3009,25 +3240,6 @@
   ultimately show ?case by blast
 qed
 
-lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
-  by (simp add: lead_coeff_def)
-
-lemma lead_coeff_of_nat [simp]:
-  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
-  by (induction n) (simp_all add: lead_coeff_def of_nat_poly)
-
-lemma lead_coeff_numeral [simp]: 
-  "lead_coeff (numeral n) = numeral n"
-  unfolding lead_coeff_def
-  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
-
-lemma lead_coeff_power: 
-  "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"
-  by (simp add: lead_coeff_def)
-
 
 subsection \<open>Shifting polynomials\<close>
 
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -9,144 +9,84 @@
 theory Polynomial_Factorial
 imports 
   Complex_Main
-  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
   "~~/src/HOL/Library/Polynomial"
   "~~/src/HOL/Library/Normalized_Fraction"
-begin
-
-subsection \<open>Prelude\<close>
-
-lemma prod_mset_mult: 
-  "prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)"
-  by (induction A) (simp_all add: mult_ac)
-  
-lemma prod_mset_const: "prod_mset (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]: "modulo_real = (mod_field :: real \<Rightarrow> _)"
-
-instance by standard (simp_all add: dvd_field_iff divide_simps)
-end
-
-instantiation real :: euclidean_ring_gcd
+  "~~/src/HOL/Library/Field_as_Ring"
 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"
+subsection \<open>Various facts about polynomials\<close>
 
-instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
-
-end
+lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
+  by (induction A) (simp_all add: one_poly_def mult_ac)
 
-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]: "modulo_rat = (mod_field :: rat \<Rightarrow> _)"
-
-instance by standard (simp_all add: dvd_field_iff divide_simps)
-end
-
-instantiation rat :: euclidean_ring_gcd
-begin
+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
 
-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
+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 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)
 
-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]: "modulo_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
-
+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
 
 
 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"
+  -- \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
 
 lemma to_fract_0 [simp]: "to_fract 0 = 0"
   by (simp add: to_fract_def eq_fract Zero_fract_def)
@@ -219,285 +159,6 @@
 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 :: zero \<Rightarrow> 'b :: zero) \<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_div_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 prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (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>
 
@@ -1243,7 +904,7 @@
 
 end
 
-  
+ 
 subsection \<open>Prime factorisation of polynomials\<close>   
 
 context
@@ -1264,7 +925,8 @@
     by (simp add: e_def content_prod_mset 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: prod_mset_const)    
+  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
@@ -1277,7 +939,7 @@
                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 "prod_mset \<dots> = smult c (fract_poly e)"
-    by (subst prod_mset_mult) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
+    by (subst prod_mset.distrib) (simp_all add: prod_mset_fract_poly prod_mset_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)" .
@@ -1466,20 +1128,22 @@
               smult (gcd (content p) (content q)) 
                 (gcd_poly_code_aux (primitive_part p) (primitive_part q)))"
 
+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])
+
 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])
+  by (fact lcm_gcd)
 
 declare Gcd_set
   [where ?'a = "'a :: factorial_ring_gcd poly", code]
 
 declare Lcm_set
   [where ?'a = "'a :: factorial_ring_gcd poly", code]
+
+text \<open>Example:
+  @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
+\<close>
   
-value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
-
 end
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
@@ -31,10 +31,11 @@
   *}
   theories
     Library
-    Polynomial_Factorial
     (*conflicting type class instantiations and dependent applications*)
+    Field_as_Ring
     Finite_Lattice
     List_lexord
+    Polynomial_Factorial
     Prefix_Order
     Product_Lexorder
     Product_Order
diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Rings.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -713,9 +713,41 @@
 lemma div_by_1 [simp]: "a div 1 = a"
   using nonzero_mult_div_cancel_left [of 1 a] by simp
 
+lemma dvd_div_eq_0_iff:
+  assumes "b dvd a"
+  shows "a div b = 0 \<longleftrightarrow> a = 0"
+  using assms by (elim dvdE, cases "b = 0") simp_all  
+
+lemma dvd_div_eq_cancel:
+  "a div c = b div c \<Longrightarrow> c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a = b"
+  by (elim dvdE, cases "c = 0") simp_all
+
+lemma dvd_div_eq_iff:
+  "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
+  by (elim dvdE, cases "c = 0") simp_all
+
 end
 
 class idom_divide = idom + semidom_divide
+begin
+
+lemma dvd_neg_div':
+  assumes "b dvd a"
+  shows "- a div b = - (a div b)"
+proof (cases "b = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  from assms obtain c where "a = b * c" ..
+  moreover from False have "b * - c div b = - (b * c div b)"
+    using nonzero_mult_div_cancel_left [of b "- c"]
+    by simp
+  ultimately show ?thesis
+    by simp
+qed
+
+end
 
 class algebraic_semidom = semidom_divide
 begin
@@ -1060,6 +1092,15 @@
   shows "a div (b * a) = 1 div b"
   using assms is_unit_div_mult_cancel_left [of a b] by (simp add: ac_simps)
 
+lemma unit_div_eq_0_iff:
+  assumes "is_unit b"
+  shows "a div b = 0 \<longleftrightarrow> a = 0"
+  by (rule dvd_div_eq_0_iff) (insert assms, auto)  
+
+lemma div_mult_unit2:
+  "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
+  by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
+
 end
 
 class normalization_semidom = algebraic_semidom +
@@ -1373,6 +1414,17 @@
     by simp
 qed
 
+lemma normalize_unit_factor_eqI:
+  assumes "normalize a = normalize b"
+    and "unit_factor a = unit_factor b"
+  shows "a = b"
+proof -
+  from assms have "unit_factor a * normalize a = unit_factor b * normalize b"
+    by simp
+  then show ?thesis
+    by simp
+qed
+
 end