more algebra

--- a/src/HOL/Algebra/Algebra.thy	Mon Jul 02 21:45:35 2018 +0100
+++ b/src/HOL/Algebra/Algebra.thy	Mon Jul 02 22:40:25 2018 +0100
@@ -2,7 +2,6 @@
 
 theory Algebra
   imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields
-     Divisibility Embedded_Algebras IntRing Sym_Groups
-(*Frobenius Exact_Sequence Polynomials*)
+     Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials
 begin
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Exact_Sequence.thy	Mon Jul 02 22:40:25 2018 +0100
@@ -0,0 +1,179 @@
+(* ************************************************************************** *)
+(* Title:      Exact_Sequence.thy                                             *)
+(* Author:     Martin Baillon                                                 *)
+(* ************************************************************************** *)
+
+theory Exact_Sequence
+  imports Group Coset Solvable_Groups
+    
+begin
+
+section \<open>Exact Sequences\<close>
+
+
+subsection \<open>Definitions\<close>
+
+inductive exact_seq :: "'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow> bool"  where
+unity:     " group_hom G1 G2 f \<Longrightarrow> exact_seq ([G2, G1], [f])" |
+extension: "\<lbrakk> exact_seq ((G # K # l), (g # q)); group H ; h \<in> hom G H ;
+              kernel G H h = image g (carrier K) \<rbrakk> \<Longrightarrow> exact_seq (H # G # K # l, h # g # q)"
+
+abbreviation exact_seq_arrow ::
+  "('a \<Rightarrow> 'a) \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list \<Rightarrow>  'a monoid \<Rightarrow> 'a monoid list \<times> ('a \<Rightarrow> 'a) list"
+  ("(3_ / \<longlongrightarrow>\<index> _)" [1000, 60])
+  where "exact_seq_arrow  f t G \<equiv> (G # (fst t), f # (snd t))"
+
+
+subsection \<open>Basic Properties\<close>
+
+lemma exact_seq_length1: "exact_seq t \<Longrightarrow> length (fst t) = Suc (length (snd t))"
+  by (induct t rule: exact_seq.induct) auto
+
+lemma exact_seq_length2: "exact_seq t \<Longrightarrow> length (snd t) \<ge> Suc 0"
+  by (induct t rule: exact_seq.induct) auto
+
+lemma dropped_seq_is_exact_seq:
+  assumes "exact_seq (G, F)" and "(i :: nat) < length F"
+  shows "exact_seq (drop i G, drop i F)"
+proof-
+  { fix t i assume "exact_seq t" "i < length (snd t)"
+    hence "exact_seq (drop i (fst t), drop i (snd t))"
+    proof (induction arbitrary: i)
+      case (unity G1 G2 f) thus ?case
+        by (simp add: exact_seq.unity)
+    next
+      case (extension G K l g q H h) show ?case
+      proof (cases)
+        assume "i = 0" thus ?case
+          using exact_seq.extension[OF extension.hyps] by simp
+      next
+        assume "i \<noteq> 0" hence "i \<ge> Suc 0" by simp
+        then obtain k where "k < length (snd (G # K # l, g # q))" "i = Suc k"
+          using Suc_le_D extension.prems by auto
+        thus ?thesis using extension.IH by simp 
+      qed
+    qed }
+
+  thus ?thesis using assms by auto
+qed
+
+lemma truncated_seq_is_exact_seq:
+  assumes "exact_seq (l, q)" and "length l \<ge> 3"
+  shows "exact_seq (tl l, tl q)"
+  using exact_seq_length1[OF assms(1)] dropped_seq_is_exact_seq[OF assms(1), of "Suc 0"]
+        exact_seq_length2[OF assms(1)] assms(2) by (simp add: drop_Suc)
+
+lemma exact_seq_imp_exact_hom:
+   assumes "exact_seq (G1 # l,q) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
+   shows "g1 ` (carrier G1) = kernel G2 G3 g2"
+proof-
+  { fix t assume "exact_seq t" and "length (fst t) \<ge> 3 \<and> length (snd t) \<ge> 2"
+    hence "(hd (tl (snd t))) ` (carrier (hd (tl (tl (fst t))))) =
+            kernel (hd (tl (fst t))) (hd (fst t)) (hd (snd t))"
+    proof (induction)
+      case (unity G1 G2 f)
+      then show ?case by auto
+    next
+      case (extension G l g q H h)
+      then show ?case by auto
+    qed }
+  thus ?thesis using assms by fastforce
+qed
+
+lemma exact_seq_imp_exact_hom_arbitrary:
+   assumes "exact_seq (G, F)"
+     and "Suc i < length F"
+   shows "(F ! (Suc i)) ` (carrier (G ! (Suc (Suc i)))) = kernel (G ! (Suc i)) (G ! i) (F ! i)"
+proof -
+  have "length (drop i F) \<ge> 2" "length (drop i G) \<ge> 3"
+    using assms(2) exact_seq_length1[OF assms(1)] by auto
+  then obtain l q
+    where "drop i G = (G ! i) # (G ! (Suc i)) # (G ! (Suc (Suc i))) # l"
+     and  "drop i F = (F ! i) # (F ! (Suc i)) # q"
+    by (metis Cons_nth_drop_Suc Suc_less_eq assms exact_seq_length1 fst_conv
+        le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
+  thus ?thesis
+  using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
+        exact_seq_imp_exact_hom[of "G ! i" "G ! (Suc i)" "G ! (Suc (Suc i))" l q] by auto
+qed
+
+lemma exact_seq_imp_group_hom :
+  assumes "exact_seq ((G # l, q)) \<longlongrightarrow>\<^bsub>g\<^esub> H"
+  shows "group_hom G H g"
+proof-
+  { fix t assume "exact_seq t"
+    hence "group_hom (hd (tl (fst t))) (hd (fst t)) (hd(snd t))"
+    proof (induction)
+      case (unity G1 G2 f)
+      then show ?case by auto
+    next
+      case (extension G l g q H h)
+      then show ?case unfolding group_hom_def group_hom_axioms_def by auto
+    qed }
+  note aux_lemma = this
+  show ?thesis using aux_lemma[OF assms]
+    by simp
+qed
+
+lemma exact_seq_imp_group_hom_arbitrary:
+  assumes "exact_seq (G, F)" and "(i :: nat) < length F"
+  shows "group_hom (G ! (Suc i)) (G ! i) (F ! i)"
+proof -
+  have "length (drop i F) \<ge> 1" "length (drop i G) \<ge> 2"
+    using assms(2) exact_seq_length1[OF assms(1)] by auto
+  then obtain l q
+    where "drop i G = (G ! i) # (G ! (Suc i)) # l"
+     and  "drop i F = (F ! i) # q"
+    by (metis Cons_nth_drop_Suc Suc_leI assms exact_seq_length1 fst_conv
+        le_eq_less_or_eq le_imp_less_Suc prod.sel(2))
+  thus ?thesis
+  using dropped_seq_is_exact_seq[OF assms(1), of i] assms(2)
+        exact_seq_imp_group_hom[of "G ! i" "G ! (Suc i)" l q "F ! i"] by simp
+qed
+
+
+subsection \<open>Link Between Exact Sequences and Solvable Conditions\<close>
+
+lemma exact_seq_solvable_imp :
+  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
+    and "inj_on g1 (carrier G1)"
+    and "g2 ` (carrier G2) = carrier G3"
+  shows "solvable G2 \<Longrightarrow> (solvable G1) \<and> (solvable G3)"
+proof -
+  assume G2: "solvable G2"
+  have "group_hom G1 G2 g1"
+    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"] by simp
+  hence "solvable G1"
+    using group_hom.inj_hom_imp_solvable[of G1 G2 g1] assms(2) G2 by simp
+  moreover have "group_hom G2 G3 g2"
+    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by simp
+  hence "solvable G3"
+    using group_hom.surj_hom_imp_solvable[of G2 G3 g2] assms(3) G2 by simp
+  ultimately show ?thesis by simp
+qed
+
+lemma exact_seq_solvable_recip :
+  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
+    and "inj_on g1 (carrier G1)"
+    and "g2 ` (carrier G2) = carrier G3"
+  shows "(solvable G1) \<and> (solvable G3) \<Longrightarrow> solvable G2"
+proof -
+  assume "(solvable G1) \<and> (solvable G3)"
+  hence G1: "solvable G1" and G3: "solvable G3" by auto
+  have g1: "group_hom G1 G2 g1" and g2: "group_hom G2 G3 g2"
+    using exact_seq_imp_group_hom_arbitrary[OF assms(1), of "Suc 0"]
+          exact_seq_imp_group_hom_arbitrary[OF assms(1), of 0] by auto
+  show ?thesis
+    using solvable_condition[OF g1 g2 assms(3)]
+          exact_seq_imp_exact_hom[OF assms(1)] G1 G3 by auto
+qed
+
+proposition exact_seq_solvable_iff :
+  assumes "exact_seq ([G1],[]) \<longlongrightarrow>\<^bsub>g1\<^esub> G2 \<longlongrightarrow>\<^bsub>g2\<^esub> G3"
+    and "inj_on g1 (carrier G1)"
+    and "g2 ` (carrier G2) = carrier G3"
+  shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow>  solvable G2"
+  using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast
+
+end
+         
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Polynomials.thy	Mon Jul 02 22:40:25 2018 +0100
@@ -0,0 +1,1855 @@
+(* ************************************************************************** *)
+(* Title:      Polynomials.thy                                                *)
+(* Author:     Paulo Emílio de Vilhena                                        *)
+(* ************************************************************************** *)
+
+theory Polynomials
+  imports Ring Ring_Divisibility Subrings
+
+begin
+
+section \<open>Polynomials\<close>
+
+subsection \<open>Definitions\<close>
+
+abbreviation lead_coeff :: "'a list \<Rightarrow> 'a"
+  where "lead_coeff \<equiv> hd"
+
+definition degree :: "'a list \<Rightarrow> nat"
+  where "degree p = length p - 1"
+
+definition polynomial :: "_ \<Rightarrow> 'a list \<Rightarrow> bool"
+  where "polynomial R p \<longleftrightarrow> p = [] \<or> (set p \<subseteq> carrier R \<and> lead_coeff p \<noteq> \<zero>\<^bsub>R\<^esub>)"
+
+definition (in ring) monon :: "'a \<Rightarrow> nat \<Rightarrow> 'a list"
+  where "monon a n = a # (replicate n \<zero>\<^bsub>R\<^esub>)"
+
+fun (in ring) eval :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a"
+  where
+    "eval [] = (\<lambda>_. \<zero>)"
+  | "eval p = (\<lambda>x. ((lead_coeff p) \<otimes> (x [^] (degree p))) \<oplus> (eval (tl p) x))"
+
+fun (in ring) coeff :: "'a list \<Rightarrow> nat \<Rightarrow> 'a"
+  where
+    "coeff [] = (\<lambda>_. \<zero>)"
+  | "coeff p = (\<lambda>i. if i = degree p then lead_coeff p else (coeff (tl p)) i)"
+
+fun (in ring) normalize :: "'a list \<Rightarrow> 'a list"
+  where
+    "normalize [] = []"
+  | "normalize p = (if lead_coeff p \<noteq> \<zero> then p else normalize (tl p))"
+
+fun (in ring) poly_add :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  where "poly_add p1 p2 =
+           (if length p1 \<ge> length p2
+            then normalize (map2 (\<oplus>) p1 ((replicate (length p1 - length p2) \<zero>) @ p2))
+            else poly_add p2 p1)"
+
+fun (in ring) poly_mult :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  where
+    "poly_mult [] p2 = []"
+  | "poly_mult p1 p2 =
+       poly_add ((map (\<lambda>a. lead_coeff p1 \<otimes> a) p2) @ (replicate (degree p1) \<zero>)) (poly_mult (tl p1) p2)"
+
+fun (in ring) dense_repr :: "'a list \<Rightarrow> ('a \<times> nat) list"
+  where
+    "dense_repr [] = []"
+  | "dense_repr p = (if lead_coeff p \<noteq> \<zero>
+                     then (lead_coeff p, degree p) # (dense_repr (tl p))
+                     else (dense_repr (tl p)))"
+
+fun (in ring) of_dense :: "('a \<times> nat) list \<Rightarrow> 'a list"
+  where "of_dense dl = foldr (\<lambda>(a, n) l. poly_add (monon a n) l) dl []"
+
+
+subsection \<open>Basic Properties\<close>
+
+context ring
+begin
+
+lemma polynomialI [intro]: "\<lbrakk> set p \<subseteq> carrier R; lead_coeff p \<noteq> \<zero> \<rbrakk> \<Longrightarrow> polynomial R p"
+  unfolding polynomial_def by auto
+
+lemma polynomial_in_carrier [intro]: "polynomial R p \<Longrightarrow> set p \<subseteq> carrier R"
+  unfolding polynomial_def by auto
+
+lemma lead_coeff_not_zero [intro]: "polynomial R (a # p) \<Longrightarrow> a \<in> carrier R - { \<zero> }"
+  unfolding polynomial_def by simp
+
+lemma zero_is_polynomial [intro]: "polynomial R []"
+  unfolding polynomial_def by simp
+
+lemma const_is_polynomial [intro]: "a \<in> carrier R - { \<zero> } \<Longrightarrow> polynomial R [ a ]"
+  unfolding polynomial_def by auto
+
+lemma monon_is_polynomial [intro]: "a \<in> carrier R - { \<zero> } \<Longrightarrow> polynomial R (monon a n)"
+  unfolding polynomial_def monon_def by auto
+
+lemma monon_in_carrier [intro]: "a \<in> carrier R \<Longrightarrow> set (monon a n) \<subseteq> carrier R"
+  unfolding monon_def by auto
+
+lemma normalize_gives_polynomial: "set p \<subseteq> carrier R \<Longrightarrow> polynomial R (normalize p)"
+  by (induction p) (auto simp add: polynomial_def)
+
+lemma normalize_in_carrier: "set p \<subseteq> carrier R \<Longrightarrow> set (normalize p) \<subseteq> carrier R"
+  using normalize_gives_polynomial polynomial_in_carrier by simp
+
+lemma normalize_idem: "polynomial R p \<Longrightarrow> normalize p = p"
+  unfolding polynomial_def by (cases p) (auto)
+
+lemma normalize_length_le: "length (normalize p) \<le> length p"
+  by (induction p) (auto)
+
+lemma eval_in_carrier: "\<lbrakk> set p \<subseteq> carrier R; x \<in> carrier R \<rbrakk> \<Longrightarrow> (eval p) x \<in> carrier R"
+  by (induction p) (auto)
+
+lemma eval_poly_in_carrier: "\<lbrakk> polynomial R p; x \<in> carrier R \<rbrakk> \<Longrightarrow> (eval p) x \<in> carrier R"
+  using eval_in_carrier unfolding polynomial_def by auto
+
+lemma coeff_in_carrier [simp]: "set p \<subseteq> carrier R \<Longrightarrow> (coeff p) i \<in> carrier R"
+  by (induction p) (auto)
+
+lemma poly_coeff_in_carrier [simp]: "polynomial R p \<Longrightarrow> coeff p i \<in> carrier R"
+  using coeff_in_carrier unfolding polynomial_def by auto
+
+lemma lead_coeff_simp [simp]: "p \<noteq> [] \<Longrightarrow> (coeff p) (degree p) = lead_coeff p"
+  by (metis coeff.simps(2) list.exhaust_sel)
+
+lemma coeff_list: "map (coeff p) (rev [0..< length p]) = p"
+proof (induction p)
+  case Nil thus ?case by simp
+next
+  case (Cons a p)
+  have "map (coeff (a # p)) (rev [0..<length (a # p)]) =
+        map (coeff (a # p)) ((length p) # (rev [0..<length p]))"
+    by simp
+  also have " ... = a # (map (coeff p) (rev [0..<length p]))"
+    using degree_def[of "a # p"] by auto
+  also have " ... = a # p"
+    using Cons by simp
+  finally show ?case . 
+qed
+
+lemma coeff_nth: "i < length p \<Longrightarrow> (coeff p) i = p ! (length p - 1 - i)"
+proof -
+  assume i_lt: "i < length p"
+  hence "(coeff p) i = (map (coeff p) [0..< length p]) ! i"
+    by simp
+  also have " ... = (rev (map (coeff p) (rev [0..< length p]))) ! i"
+    by (simp add: rev_map)
+  also have " ... = (map (coeff p) (rev [0..< length p])) ! (length p - 1 - i)"
+    using coeff_list i_lt rev_nth by auto
+  also have " ... = p ! (length p - 1 - i)"
+    using coeff_list[of p] by simp
+  finally show "(coeff p) i = p ! (length p - 1 - i)" .
+qed
+
+lemma coeff_iff_length_cond:
+  assumes "length p1 = length p2"
+  shows "p1 = p2 \<longleftrightarrow> coeff p1 = coeff p2"
+proof
+  show "p1 = p2 \<Longrightarrow> coeff p1 = coeff p2"
+    by simp
+next
+  assume A: "coeff p1 = coeff p2"
+  have "p1 = map (coeff p1) (rev [0..< length p1])"
+    using coeff_list[of p1] by simp
+  also have " ... = map (coeff p2) (rev [0..< length p2])"
+    using A assms by simp
+  also have " ... = p2"
+    using coeff_list[of p2] by simp
+  finally show "p1 = p2" .
+qed
+
+lemma coeff_img_restrict: "(coeff p) ` {..< length p} = set p"
+  using coeff_list[of p] by (metis atLeast_upt image_set set_rev)
+
+lemma coeff_length: "\<And>i. i \<ge> length p \<Longrightarrow> (coeff p) i = \<zero>"
+  by (induction p) (auto simp add: degree_def)
+
+lemma coeff_degree: "\<And>i. i > degree p \<Longrightarrow> (coeff p) i = \<zero>"
+  using coeff_length by (simp add: degree_def)
+
+lemma replicate_zero_coeff [simp]: "coeff (replicate n \<zero>) = (\<lambda>_. \<zero>)"
+  by (induction n) (auto)
+
+lemma scalar_coeff: "a \<in> carrier R \<Longrightarrow> coeff (map (\<lambda>b. a \<otimes> b) p) = (\<lambda>i. a \<otimes> (coeff p) i)"
+  by (induction p) (auto simp add:degree_def)
+
+lemma monon_coeff: "coeff (monon a n) = (\<lambda>i. if i = n then a else \<zero>)"
+  unfolding monon_def by (induction n) (auto simp add: degree_def)
+
+lemma coeff_img:
+  "(coeff p) ` {..< length p} = set p"
+  "(coeff p) ` { length p ..} = { \<zero> }"
+  "(coeff p) ` UNIV = (set p) \<union> { \<zero> }"
+  using coeff_img_restrict
+proof (simp)
+  show coeff_img_up: "(coeff p) ` { length p ..} = { \<zero> }"
+    using coeff_length[of p] unfolding degree_def by force
+  from coeff_img_up and coeff_img_restrict[of p]
+  show "(coeff p) ` UNIV = (set p) \<union> { \<zero> }"
+    by force
+qed
+
+lemma degree_def':
+  assumes "polynomial R p"
+  shows "degree p = (LEAST n. \<forall>i. i > n \<longrightarrow> (coeff p) i = \<zero>)"
+proof (cases p)
+  case Nil thus ?thesis
+    unfolding degree_def by auto
+next
+  define P where "P = (\<lambda>n. \<forall>i. i > n \<longrightarrow> (coeff p) i = \<zero>)"
+
+  case (Cons a ps)
+  hence "(coeff p) (degree p) \<noteq> \<zero>"
+    using assms unfolding polynomial_def by auto
+  hence "\<And>n. n < degree p \<Longrightarrow> \<not> P n"
+    unfolding P_def by auto
+  moreover have "P (degree p)"
+    unfolding P_def using coeff_degree[of p] by simp
+  ultimately have "degree p = (LEAST n. P n)"
+    by (meson LeastI nat_neq_iff not_less_Least)
+  thus ?thesis unfolding P_def .
+qed
+
+lemma coeff_iff_polynomial_cond:
+  assumes "polynomial R p1" and "polynomial R p2"
+  shows "p1 = p2 \<longleftrightarrow> coeff p1 = coeff p2"
+proof
+  show "p1 = p2 \<Longrightarrow> coeff p1 = coeff p2"
+    by simp
+next
+  assume coeff_eq: "coeff p1 = coeff p2"
+  hence deg_eq: "degree p1 = degree p2"
+    using degree_def'[OF assms(1)] degree_def'[OF assms(2)] by auto
+  thus "p1 = p2"
+  proof (cases)
+    assume "p1 \<noteq> [] \<and> p2 \<noteq> []"
+    hence "length p1 = length p2"
+      using deg_eq unfolding degree_def
+      by (simp add: Nitpick.size_list_simp(2)) 
+    thus ?thesis
+      using coeff_iff_length_cond[of p1 p2] coeff_eq by simp
+  next
+    { fix p1 p2 assume A: "p1 = []" "coeff p1 = coeff p2" "polynomial R p2"
+      have "p2 = []"
+      proof (rule ccontr)
+        assume "p2 \<noteq> []"
+        hence "(coeff p2) (degree p2) \<noteq> \<zero>"
+          using A(3) unfolding polynomial_def
+          by (metis coeff.simps(2) list.collapse)
+        moreover have "(coeff p1) ` UNIV = { \<zero> }"
+          using A(1) by auto
+        hence "(coeff p2) ` UNIV = { \<zero> }"
+          using A(2) by simp
+        ultimately show False
+          by blast
+      qed } note aux_lemma = this
+    assume "\<not> (p1 \<noteq> [] \<and> p2 \<noteq> [])"
+    hence "p1 = [] \<or> p2 = []" by simp
+    thus ?thesis
+      using assms coeff_eq aux_lemma[of p1 p2] aux_lemma[of p2 p1] by auto
+  qed
+qed
+
+lemma normalize_lead_coeff:
+  assumes "length (normalize p) < length p"
+  shows "lead_coeff p = \<zero>"
+proof (cases p)
+  case Nil thus ?thesis
+    using assms by simp
+next
+  case (Cons a ps) thus ?thesis
+    using assms by (cases "a = \<zero>") (auto)
+qed
+
+lemma normalize_length_lt:
+  assumes "lead_coeff p = \<zero>" and "length p > 0"
+  shows "length (normalize p) < length p"
+proof (cases p)
+  case Nil thus ?thesis
+    using assms by simp
+next
+  case (Cons a ps) thus ?thesis
+    using normalize_length_le[of ps] assms by simp
+qed
+
+lemma normalize_length_eq:
+  assumes "lead_coeff p \<noteq> \<zero>"
+  shows "length (normalize p) = length p"
+  using normalize_length_le[of p] assms nat_less_le normalize_lead_coeff by auto
+
+lemma normalize_replicate_zero: "normalize ((replicate n \<zero>) @ p) = normalize p"
+  by (induction n) (auto)
+
+lemma normalize_def':
+  shows   "p = (replicate (length p - length (normalize p)) \<zero>) @
+                    (drop (length p - length (normalize p)) p)" (is ?statement1)
+  and "normalize p = drop (length p - length (normalize p)) p"  (is ?statement2)
+proof -
+  show ?statement1
+  proof (induction p)
+    case Nil thus ?case by simp
+  next
+    case (Cons a p) thus ?case
+    proof (cases "a = \<zero>")
+      assume "a \<noteq> \<zero>" thus ?case
+        using Cons by simp
+    next
+      assume eq_zero: "a = \<zero>"
+      hence len_eq:
+        "Suc (length p - length (normalize p)) = length (a # p) - length (normalize (a # p))"
+        by (simp add: Suc_diff_le normalize_length_le)
+      have "a # p = \<zero> # (replicate (length p - length (normalize p)) \<zero> @
+                              drop (length p - length (normalize p)) p)"
+        using eq_zero Cons by simp
+      also have " ... = (replicate (Suc (length p - length (normalize p))) \<zero> @
+                              drop (Suc (length p - length (normalize p))) (a # p))"
+        by simp
+      also have " ... = (replicate (length (a # p) - length (normalize (a # p))) \<zero> @
+                              drop (length (a # p) - length (normalize (a # p))) (a # p))"
+        using len_eq by simp
+      finally show ?case .
+    qed
+  qed
+next
+  show ?statement2
+  proof -
+    have "\<exists>m. normalize p = drop m p"
+    proof (induction p)
+      case Nil thus ?case by simp
+    next
+      case (Cons a p) thus ?case
+        apply (cases "a = \<zero>")
+        apply (auto)
+        apply (metis drop_Suc_Cons)
+        apply (metis drop0)
+        done
+    qed
+    then obtain m where m: "normalize p = drop m p" by auto
+    hence "length (normalize p) = length p - m" by simp
+    thus ?thesis
+      using m by (metis rev_drop rev_rev_ident take_rev)
+  qed
+qed
+
+lemma normalize_coeff: "coeff p = coeff (normalize p)"
+proof (induction p)
+  case Nil thus ?case by simp
+next
+  case (Cons a p)
+  have "coeff (normalize p) (length p) = \<zero>"
+    using normalize_length_le[of p] coeff_degree[of "normalize p"] unfolding degree_def
+    by (metis One_nat_def coeff.simps(1) diff_less length_0_conv
+        less_imp_diff_less nat_neq_iff neq0_conv not_le zero_less_Suc)
+  then show ?case
+    using Cons by (cases "a = \<zero>") (auto simp add: degree_def)
+qed
+
+lemma append_coeff:
+  "coeff (p @ q) = (\<lambda>i. if i < length q then (coeff q) i else (coeff p) (i - length q))"
+proof (induction p)
+  case Nil thus ?case
+    using coeff_length[of q] by auto
+next
+  case (Cons a p)
+  have "coeff ((a # p) @ q) = (\<lambda>i. if i = length p + length q then a else (coeff (p @ q)) i)"
+    by (auto simp add: degree_def)
+  also have " ... = (\<lambda>i. if i = length p + length q then a
+                         else if i < length q then (coeff q) i
+                         else (coeff p) (i - length q))"
+    using Cons by auto
+  also have " ... = (\<lambda>i. if i < length q then (coeff q) i
+                         else if i = length p + length q then a else (coeff p) (i - length q))"
+    by auto
+  also have " ... = (\<lambda>i. if i < length q then (coeff q) i
+                         else if i - length q = length p then a else (coeff p) (i - length q))"
+    by fastforce
+  also have " ... = (\<lambda>i. if i < length q then (coeff q) i else (coeff (a # p)) (i - length q))"
+    by (auto simp add: degree_def)
+  finally show ?case .
+qed
+
+lemma prefix_replicate_zero_coeff: "coeff p = coeff ((replicate n \<zero>) @ p)"
+  using append_coeff[of "replicate n \<zero>" p] replicate_zero_coeff[of n] coeff_length[of p] by auto
+
+end
+
+
+subsection \<open>Poly_Add\<close>
+
+context ring
+begin
+
+lemma poly_add_is_polynomial:
+  assumes "set p1 \<subseteq> carrier R" and "set p2 \<subseteq> carrier R"
+  shows "polynomial R (poly_add p1 p2)"
+proof -
+  { fix p1 p2 assume A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "length p1 \<ge> length p2"
+    hence "polynomial R (poly_add p1 p2)"
+    proof -
+      define p2' where "p2' = (replicate (length p1 - length p2) \<zero>) @ p2"
+      hence set_p2': "set p2' \<subseteq> carrier R"
+        using A(2) by auto
+      have "set (map (\<lambda>(a, b). a \<oplus> b) (zip p1 p2')) \<subseteq> carrier R"
+      proof
+        fix c assume "c \<in> set (map (\<lambda>(a, b). a \<oplus> b) (zip p1 p2'))"
+        then obtain t where "t \<in> set (zip p1 p2')" and c: "c = fst t \<oplus> snd t"
+          by auto
+        then obtain a b where "a \<in> set p1"  "a = fst t"
+                          and "b \<in> set p2'" "b = snd t"
+          by (metis set_zip_leftD set_zip_rightD surjective_pairing)
+        thus "c \<in> carrier R"
+          using A(1) set_p2' c by auto
+      qed
+      thus ?thesis
+        unfolding p2'_def using normalize_gives_polynomial A(3) by simp
+    qed }
+  thus ?thesis
+    using assms by simp
+qed
+
+lemma poly_add_in_carrier:
+  "\<lbrakk> set p1 \<subseteq> carrier R; set p2 \<subseteq> carrier R \<rbrakk> \<Longrightarrow> set (poly_add p1 p2) \<subseteq> carrier R"
+  using poly_add_is_polynomial polynomial_in_carrier by simp
+
+lemma poly_add_closed: "\<lbrakk> polynomial R p1; polynomial R p2 \<rbrakk> \<Longrightarrow> polynomial R (poly_add p1 p2)"
+  using poly_add_is_polynomial polynomial_in_carrier by auto
+
+lemma poly_add_length_le: "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+proof -
+  { fix p1 p2 :: "'a list" assume A: "length p1 \<ge> length p2"
+    hence "length (poly_add p1 p2) \<le> max (length p1) (length p2)"
+    proof -
+      let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+      have "length (map2 (\<oplus>) p1 ?p2) = length p1"
+        using A by auto
+      thus ?thesis
+        using normalize_length_le[of "map2 (\<oplus>) p1 ?p2"] A by auto
+    qed }
+  thus ?thesis
+    by (metis le_cases max.commute poly_add.simps)
+qed
+
+lemma poly_add_length_eq:
+  assumes "polynomial R p1" "polynomial R p2" and "length p1 \<noteq> length p2"
+  shows "length (poly_add p1 p2) = max (length p1) (length p2)"
+proof -
+  { fix p1 p2 assume A: "polynomial R p1" "polynomial R p2" "length p1 > length p2"
+    hence "length (poly_add p1 p2) = max (length p1) (length p2)"
+    proof -
+      let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+      have p1: "p1 \<noteq> []" and p2: "?p2 \<noteq> []"
+        using A(3) by auto
+      hence "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1 \<oplus> lead_coeff ?p2"
+        by (smt case_prod_conv list.exhaust_sel list.map(2) list.sel(1) zip_Cons_Cons)
+      moreover have "lead_coeff p1 \<in> carrier R"
+        using p1 A(1) unfolding polynomial_def by auto
+      ultimately have "lead_coeff (map2 (\<oplus>) p1 ?p2) = lead_coeff p1"
+        using A(3) by auto
+      moreover have "lead_coeff p1 \<noteq> \<zero>"
+        using p1 A(1) unfolding polynomial_def by simp
+      ultimately have "length (normalize (map2 (\<oplus>) p1 ?p2)) = length p1"
+        using normalize_length_eq by auto
+      thus ?thesis
+        using A(3) by auto
+    qed }
+  thus ?thesis
+    using assms by auto
+qed
+
+lemma poly_add_degree: "degree (poly_add p1 p2) \<le> max (degree p1) (degree p2)"
+  unfolding degree_def using poly_add_length_le
+  by (meson diff_le_mono le_max_iff_disj)
+
+lemma poly_add_degree_eq:
+  assumes "polynomial R p1" "polynomial R p2" and "degree p1 \<noteq> degree p2"
+  shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)"
+  using poly_add_length_eq[of p1 p2] assms
+  by (smt degree_def diff_le_mono le_cases max.absorb1 max_def)
+
+lemma poly_add_coeff_aux:
+  assumes "length p1 \<ge> length p2"
+  shows "coeff (poly_add p1 p2) = (\<lambda>i. ((coeff p1) i) \<oplus> ((coeff p2) i))"
+proof
+  fix i
+  have "i < length p1 \<Longrightarrow> (coeff (poly_add p1 p2)) i = ((coeff p1) i) \<oplus> ((coeff p2) i)"
+  proof -
+    let ?p2 = "(replicate (length p1 - length p2) \<zero>) @ p2"
+    have len_eqs: "length p1 = length ?p2" "length (map2 (\<oplus>) p1 ?p2) = length p1"
+      using assms by auto
+    assume i_lt: "i < length p1"
+    have "(coeff (poly_add p1 p2)) i = (coeff (map2 (\<oplus>) p1 ?p2)) i"
+      using normalize_coeff[of "map2 (\<oplus>) p1 ?p2"] assms by auto
+    also have " ... = (map2 (\<oplus>) p1 ?p2) ! (length p1 - 1 - i)"
+      using coeff_nth[of i "map2 (\<oplus>) p1 ?p2"] len_eqs(2) i_lt by auto
+    also have " ... = (p1 ! (length p1 - 1 - i)) \<oplus> (?p2 ! (length ?p2 - 1 - i))"
+      using len_eqs i_lt by auto
+    also have " ... = ((coeff p1) i) \<oplus> ((coeff ?p2) i)"
+      using coeff_nth[of i p1] coeff_nth[of i ?p2] i_lt len_eqs(1) by auto
+    also have " ... = ((coeff p1) i) \<oplus> ((coeff p2) i)"
+      using prefix_replicate_zero_coeff by simp
+    finally show "(coeff (poly_add p1 p2)) i = ((coeff p1) i) \<oplus> ((coeff p2) i)" .
+  qed
+  moreover
+  have "i \<ge> length p1 \<Longrightarrow> (coeff (poly_add p1 p2)) i = ((coeff p1) i) \<oplus> ((coeff p2) i)"
+    using coeff_length[of "poly_add p1 p2"] coeff_length[of p1] coeff_length[of p2]
+          poly_add_length_le[of p1 p2] assms by auto
+  ultimately show "(coeff (poly_add p1 p2)) i = ((coeff p1) i) \<oplus> ((coeff p2) i)"
+    using not_le by blast
+qed
+
+lemma poly_add_coeff:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "coeff (poly_add p1 p2) = (\<lambda>i. ((coeff p1) i) \<oplus> ((coeff p2) i))"
+proof -
+  have "length p1 \<ge> length p2 \<or> length p2 > length p1"
+    by auto
+  thus ?thesis
+  proof
+    assume "length p1 \<ge> length p2" thus ?thesis
+      using poly_add_coeff_aux by simp
+  next
+    assume "length p2 > length p1"
+    hence "coeff (poly_add p1 p2) = (\<lambda>i. ((coeff p2) i) \<oplus> ((coeff p1) i))"
+      using poly_add_coeff_aux by simp
+    thus ?thesis
+      using assms by (simp add: add.m_comm)
+  qed
+qed
+
+lemma poly_add_comm:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_add p1 p2 = poly_add p2 p1"
+proof -
+  have "coeff (poly_add p1 p2) = coeff (poly_add p2 p1)"
+    using poly_add_coeff[OF assms] poly_add_coeff[OF assms(2) assms(1)]
+          coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] add.m_comm by auto
+  thus ?thesis
+    using coeff_iff_polynomial_cond poly_add_is_polynomial assms by auto
+qed
+
+lemma poly_add_monon:
+  assumes "set p \<subseteq> carrier R" and "a \<in> carrier R - { \<zero> }"
+  shows "poly_add (monon a (length p)) p = a # p"
+  unfolding monon_def using assms by (induction p) (auto)
+
+lemma poly_add_normalize_aux:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_add p1 p2 = poly_add (normalize p1) p2"
+proof -
+  { fix n p1 p2 assume "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+    hence "poly_add p1 p2 = poly_add ((replicate n \<zero>) @ p1) p2"
+    proof (induction n)
+      case 0 thus ?case by simp
+    next
+      { fix p1 p2 :: "'a list"
+        assume in_carrier: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+        have "poly_add p1 p2 = poly_add (\<zero> # p1) p2"
+        proof -
+          have "length p1 \<ge> length p2 \<Longrightarrow> ?thesis"
+          proof -
+            assume A: "length p1 \<ge> length p2"
+            let ?p2 = "\<lambda>n. (replicate n \<zero>) @ p2"
+            have "poly_add p1 p2 = normalize (map2 (\<oplus>) (\<zero> # p1) (\<zero> # ?p2 (length p1 - length p2)))"
+              using A by simp
+            also have " ... = normalize (map2 (\<oplus>) (\<zero> # p1) (?p2 (length (\<zero> # p1) - length p2)))"
+              by (simp add: A Suc_diff_le)
+            also have " ... = poly_add (\<zero> # p1) p2"
+              using A by simp
+            finally show ?thesis .
+          qed
+
+          moreover have "length p2 > length p1 \<Longrightarrow> ?thesis"
+          proof -
+            assume A: "length p2 > length p1"
+            let ?f = "\<lambda>n p. (replicate n \<zero>) @ p"
+            have "poly_add p1 p2 = poly_add p2 p1"
+              using A by simp
+            also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - length p1) p1))"
+              using A by simp
+            also have " ... = normalize (map2 (\<oplus>) p2 (?f (length p2 - Suc (length p1)) (\<zero> # p1)))"
+              by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
+            also have " ... = poly_add p2 (\<zero> # p1)"
+              using A by simp
+            also have " ... = poly_add (\<zero> # p1) p2"
+              using poly_add_comm[of p2 "\<zero> # p1"] in_carrier by auto
+            finally show ?thesis .
+          qed
+
+          ultimately show ?thesis by auto
+        qed } note aux_lemma = this
+
+      case (Suc n)
+      hence in_carrier: "set (replicate n \<zero> @ p1) \<subseteq> carrier R"
+        by auto
+      have "poly_add p1 p2 = poly_add (replicate n \<zero> @ p1) p2"
+        using Suc by simp
+      also have " ... = poly_add (replicate (Suc n) \<zero> @ p1) p2"
+        using aux_lemma[OF in_carrier Suc(3)] by simp
+      finally show ?case .
+    qed } note aux_lemma = this
+
+  have "poly_add p1 p2 =
+        poly_add ((replicate (length p1 - length (normalize p1)) \<zero>) @ normalize p1) p2"
+    using normalize_def'[of p1] by simp
+  also have " ... = poly_add (normalize p1) p2"
+    using aux_lemma[OF
+          polynomial_in_carrier[OF normalize_gives_polynomial[OF assms(1)]] assms(2)] by simp
+  finally show ?thesis .
+qed
+
+lemma poly_add_normalize:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_add p1 p2 = poly_add (normalize p1) p2"
+    and "poly_add p1 p2 = poly_add p1 (normalize p2)"
+    and "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)"
+proof -
+  show "poly_add p1 p2 = poly_add p1 (normalize p2)"
+    using poly_add_normalize_aux[OF assms(2) assms(1)] poly_add_comm
+      polynomial_in_carrier normalize_gives_polynomial assms by auto
+next
+  show "poly_add p1 p2 = poly_add (normalize p1) p2"
+    using poly_add_normalize_aux[OF assms] by simp
+  also have " ... = poly_add p2 (normalize p1)"
+    using poly_add_comm polynomial_in_carrier normalize_gives_polynomial assms by auto
+  also have " ... = poly_add (normalize p2) (normalize p1)"
+    using poly_add_normalize_aux polynomial_in_carrier normalize_gives_polynomial assms by auto
+  also have " ... = poly_add (normalize p1) (normalize p2)"
+    using poly_add_comm polynomial_in_carrier normalize_gives_polynomial assms by auto
+  finally show "poly_add p1 p2 = poly_add (normalize p1) (normalize p2)" .
+qed
+
+lemma poly_add_zero':
+  assumes "set p \<subseteq> carrier R"
+  shows "poly_add p [] = normalize p" and "poly_add [] p = normalize p"
+proof -
+  show "poly_add p [] = normalize p" using assms
+  proof (induction p)
+    case Nil thus ?case by simp
+  next
+    { fix p assume A: "set p \<subseteq> carrier R" "lead_coeff p \<noteq> \<zero>"
+      hence "polynomial R p"
+        unfolding polynomial_def by simp
+      moreover have "coeff (poly_add p []) = coeff p"
+        using poly_add_coeff[of p "[]"] A(1) by simp
+      ultimately have "poly_add p [] = p"
+        using coeff_iff_polynomial_cond[OF
+              poly_add_is_polynomial[OF A(1), of "[]"], of p] by simp }
+    note aux_lemma = this
+    case (Cons a p) thus ?case
+      using aux_lemma[of "a # p"] by auto
+  qed
+  thus "poly_add [] p = normalize p"
+    using poly_add_comm[OF assms, of "[]"] by simp
+qed
+
+lemma poly_add_zero:
+  assumes "polynomial R p"
+  shows "poly_add p [] = p" and "poly_add [] p = p"
+  using poly_add_zero' normalize_idem polynomial_in_carrier assms by auto
+
+lemma poly_add_replicate_zero':
+  assumes "set p \<subseteq> carrier R"
+  shows "poly_add p (replicate n \<zero>) = normalize p" and "poly_add (replicate n \<zero>) p = normalize p"
+proof -
+  have "poly_add p (replicate n \<zero>) = poly_add p []"
+    using poly_add_normalize(2)[OF assms, of "replicate n \<zero>"]
+          normalize_replicate_zero[of n "[]"] by force
+  also have " ... = normalize p"
+    using poly_add_zero'[OF assms] by simp
+  finally show "poly_add p (replicate n \<zero>) = normalize p" .
+  thus "poly_add (replicate n \<zero>) p = normalize p"
+    using poly_add_comm[OF assms, of "replicate n \<zero>"] by force
+qed
+
+lemma poly_add_replicate_zero:
+  assumes "polynomial R p"
+  shows "poly_add p (replicate n \<zero>) = p" and "poly_add (replicate n \<zero>) p = p"
+  using poly_add_replicate_zero' normalize_idem polynomial_in_carrier assms by auto
+
+
+subsection \<open>Dense Representation\<close>
+
+lemma dense_repr_replicate_zero: "dense_repr ((replicate n \<zero>) @ p) = dense_repr p"
+  by (induction n) (auto)
+
+lemma polynomial_dense_repr:
+  assumes "polynomial R p" and "p \<noteq> []"
+  shows "dense_repr p = (lead_coeff p, degree p) # dense_repr (normalize (tl p))"
+proof -
+  let ?len = length and ?norm = normalize
+  obtain a p' where p: "p = a # p'"
+    using assms(2) list.exhaust_sel by blast 
+  hence a: "a \<in> carrier R - { \<zero> }" and p': "set p' \<subseteq> carrier R"
+    using assms(1) unfolding p by (auto simp add: polynomial_def)
+  hence "dense_repr p = (lead_coeff p, degree p) # dense_repr p'"
+    unfolding p by simp
+  also have " ... =
+    (lead_coeff p, degree p) # dense_repr ((replicate (?len p' - ?len (?norm p')) \<zero>) @ ?norm p')"
+    using normalize_def' dense_repr_replicate_zero by simp
+  also have " ... = (lead_coeff p, degree p) # dense_repr (?norm p')"
+    using dense_repr_replicate_zero by simp
+  finally show ?thesis
+    unfolding p by simp
+qed
+
+lemma monon_decomp:
+  assumes "polynomial R p"
+  shows "p = of_dense (dense_repr p)"
+  using assms
+proof (induct "length p" arbitrary: p rule: less_induct)
+  case less thus ?case
+  proof (cases p)
+    case Nil thus ?thesis by simp
+  next
+    case (Cons a l)
+    hence a: "a \<in> carrier R - { \<zero> }" and l: "set l \<subseteq> carrier R"
+      using less(2) by (auto simp add: polynomial_def)
+    hence "a # l = poly_add (monon a (degree (a # l))) l"
+      using poly_add_monon by (simp add: degree_def)
+    also have " ... = poly_add (monon a (degree (a # l))) (normalize l)"
+      using poly_add_normalize(2)[of "monon a (degree (a # l))", OF _ l] a
+      unfolding monon_def by force
+    also have " ... = poly_add (monon a (degree (a # l))) (of_dense (dense_repr (normalize l)))"
+      using less(1)[of "normalize l"] normalize_length_le normalize_gives_polynomial[OF l]
+      unfolding Cons by (simp add: le_imp_less_Suc)
+    also have " ... = of_dense ((a, degree (a # l)) # dense_repr (normalize l))"
+      by simp
+    also have " ... = of_dense (dense_repr (a # l))"
+      using polynomial_dense_repr[OF less(2)] unfolding Cons by simp
+    finally show ?thesis
+      unfolding Cons by simp
+  qed
+qed
+
+end
+
+
+subsection \<open>Poly_Mult\<close>
+
+context ring
+begin
+
+lemma poly_mult_is_polynomial:
+  assumes "set p1 \<subseteq> carrier R" and "set p2 \<subseteq> carrier R"
+  shows "polynomial R (poly_mult p1 p2)"
+  using assms
+proof (induction p1)
+  case Nil thus ?case
+    by (simp add: polynomial_def)
+next
+  case (Cons a p1)
+  let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
+  
+  have "set (poly_mult p1 p2) \<subseteq> carrier R"
+    using Cons unfolding polynomial_def by auto
+
+  moreover have "set ?a_p2 \<subseteq> carrier R"
+  proof -
+    have "set (map (\<lambda>b. a \<otimes> b) p2) \<subseteq> carrier R"
+    proof
+      fix c assume "c \<in> set (map (\<lambda>b. a \<otimes> b) p2)"
+      then obtain b where "b \<in> set p2" "c = a \<otimes> b"
+        by auto
+      thus "c \<in> carrier R"
+        using Cons(2-3) by auto
+    qed
+    thus ?thesis
+      unfolding degree_def by auto
+  qed
+
+  ultimately have "polynomial R (poly_add ?a_p2 (poly_mult p1 p2))"
+    using poly_add_is_polynomial by blast
+  thus ?case by simp
+qed
+
+lemma poly_mult_in_carrier:
+  "\<lbrakk> set p1 \<subseteq> carrier R; set p2 \<subseteq> carrier R \<rbrakk> \<Longrightarrow> set (poly_mult p1 p2) \<subseteq> carrier R"
+  using poly_mult_is_polynomial polynomial_in_carrier by simp
+
+lemma poly_mult_closed: "\<lbrakk> polynomial R p1; polynomial R p2 \<rbrakk> \<Longrightarrow> polynomial R (poly_mult p1 p2)"
+  using poly_mult_is_polynomial polynomial_in_carrier by simp
+
+lemma poly_mult_coeff:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "coeff (poly_mult p1 p2) = (\<lambda>i. \<Oplus> k \<in> {..i}. (coeff p1) k \<otimes> (coeff p2) (i - k))"
+  using assms(1) 
+proof (induction p1)
+  case Nil thus ?case using assms(2) by auto
+next
+  case (Cons a p1)
+  hence in_carrier:
+    "a \<in> carrier R" "\<And>i. (coeff p1) i \<in> carrier R" "\<And>i. (coeff p2) i \<in> carrier R"
+    using coeff_in_carrier assms(2) by auto
+
+  let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
+  have "coeff  (replicate (degree (a # p1)) \<zero>) = (\<lambda>_. \<zero>)"
+   and "length (replicate (degree (a # p1)) \<zero>) = length p1"
+    using prefix_replicate_zero_coeff[of "[]" "length p1"] unfolding degree_def by auto
+  hence "coeff ?a_p2 = (\<lambda>i. if i < length p1 then \<zero> else (coeff (map (\<lambda>b. a \<otimes> b) p2)) (i - length p1))"
+    using append_coeff[of "map (\<lambda>b. a \<otimes> b) p2" "replicate (length p1) \<zero>"] unfolding degree_def by auto
+  also have " ... = (\<lambda>i. if i < length p1 then \<zero> else a \<otimes> ((coeff p2) (i - length p1)))"
+  proof -
+    have "\<And>i. i < length p2 \<Longrightarrow> (coeff (map (\<lambda>b. a \<otimes> b) p2)) i = a \<otimes> ((coeff p2) i)"
+    proof -
+      fix i assume i_lt: "i < length p2"
+      hence "(coeff (map (\<lambda>b. a \<otimes> b) p2)) i = (map (\<lambda>b. a \<otimes> b) p2) ! (length p2 - 1 - i)"
+        using coeff_nth[of i "map (\<lambda>b. a \<otimes> b) p2"] by auto
+      also have " ... = a \<otimes> (p2 ! (length p2 - 1 - i))"
+        using i_lt by auto
+      also have " ... = a \<otimes> ((coeff p2) i)"
+        using coeff_nth[OF i_lt] by simp
+      finally show "(coeff (map (\<lambda>b. a \<otimes> b) p2)) i = a \<otimes> ((coeff p2) i)" .
+    qed
+    moreover have "\<And>i. i \<ge> length p2 \<Longrightarrow> (coeff (map (\<lambda>b. a \<otimes> b) p2)) i = a \<otimes> ((coeff p2) i)"
+      using coeff_length[of p2] coeff_length[of "map (\<lambda>b. a \<otimes> b) p2"] in_carrier by auto
+    ultimately show ?thesis by (meson not_le)
+  qed
+  also have " ... = (\<lambda>i. \<Oplus> k \<in> {..i}. (if k = length p1 then a else \<zero>) \<otimes> (coeff p2) (i - k))"
+  (is "?f1 = (\<lambda>i. (\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)))")
+  proof
+    fix i
+    have "\<And>k. k \<in> {..i} \<Longrightarrow> ?f2 k \<otimes> ?f3 (i - k) = \<zero>" if "i < length p1"
+      using in_carrier that by auto
+    hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) = \<zero>" if "i < length p1"
+      using that in_carrier
+            add.finprod_cong'[of "{..i}" "{..i}" "\<lambda>k. ?f2 k \<otimes> ?f3 (i - k)" "\<lambda>i. \<zero>"]
+      by auto
+    hence eq_lt: "?f1 i = (\<lambda>i. (\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k))) i" if "i < length p1"
+      using that by auto
+
+    have "\<And>k. k \<in> {..i} \<Longrightarrow>
+              ?f2 k \<otimes>\<^bsub>R\<^esub> ?f3 (i - k) = (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>)"
+      using in_carrier by auto
+    hence "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) = 
+           (\<Oplus> k \<in> {..i}. (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>))"
+      using in_carrier
+            add.finprod_cong'[of "{..i}" "{..i}" "\<lambda>k. ?f2 k \<otimes> ?f3 (i - k)"
+                             "\<lambda>k. (if length p1 = k then a \<otimes> coeff p2 (i - k) else \<zero>)"]
+      by fastforce
+    also have " ... = a \<otimes> (coeff p2) (i - length p1)" if "i \<ge> length p1"
+      using add.finprod_singleton[of "length p1" "{..i}" "\<lambda>j. a \<otimes> (coeff p2) (i - j)"]
+            in_carrier that by auto
+    finally
+    have "(\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k)) =  a \<otimes> (coeff p2) (i - length p1)" if "i \<ge> length p1"
+      using that by simp
+    hence eq_ge: "?f1 i = (\<lambda>i. (\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k))) i" if "i \<ge> length p1"
+      using that by auto
+
+    from eq_lt eq_ge show "?f1 i = (\<lambda>i. (\<Oplus> k \<in> {..i}. ?f2 k \<otimes> ?f3 (i - k))) i" by auto
+  qed
+
+  finally have coeff_a_p2:
+    "coeff ?a_p2 = (\<lambda>i. \<Oplus> k \<in> {..i}. (if k = length p1 then a else \<zero>) \<otimes> (coeff p2) (i - k))" .
+
+  have "set ?a_p2 \<subseteq> carrier R"
+    using in_carrier(1) assms(2) by auto
+
+  moreover have "set (poly_mult p1 p2) \<subseteq> carrier R"
+    using poly_mult_is_polynomial[of p1 p2] polynomial_in_carrier assms(2) Cons(2) by auto 
+
+  ultimately
+  have "coeff (poly_mult (a # p1) p2) = (\<lambda>i. ((coeff ?a_p2) i) \<oplus> ((coeff (poly_mult p1 p2)) i))"
+    using poly_add_coeff[of ?a_p2 "poly_mult p1 p2"] by simp
+  also have " ... = (\<lambda>i. (\<Oplus> k \<in> {..i}. (if k = length p1 then a else \<zero>) \<otimes> (coeff p2) (i - k)) \<oplus>
+                         (\<Oplus> k \<in> {..i}. (coeff p1) k \<otimes> (coeff p2) (i - k)))"
+    using Cons  coeff_a_p2 by simp
+  also have " ... = (\<lambda>i. (\<Oplus> k \<in> {..i}. ((if k = length p1 then a else \<zero>) \<otimes> (coeff p2) (i - k)) \<oplus>
+                                                            ((coeff p1) k \<otimes> (coeff p2) (i - k))))"
+    using add.finprod_multf in_carrier by auto
+  also have " ... = (\<lambda>i. (\<Oplus> k \<in> {..i}. (coeff (a # p1) k) \<otimes> (coeff p2) (i - k)))"
+   (is "(\<lambda>i. (\<Oplus> k \<in> {..i}. ?f i k)) = (\<lambda>i. (\<Oplus> k \<in> {..i}. ?g i k))")
+  proof
+    fix i
+    have "\<And>k. ?f i k = ?g i k"
+      using in_carrier coeff_length[of p1] by (auto simp add: degree_def)
+    thus "(\<Oplus> k \<in> {..i}. ?f i k) = (\<Oplus> k \<in> {..i}. ?g i k)" by simp
+  qed
+  finally show ?case .
+qed
+
+lemma poly_mult_zero:
+  assumes "polynomial R p"
+  shows "poly_mult [] p = []" and "poly_mult p [] = []"
+proof -
+  show "poly_mult [] p = []" by simp
+next
+  have "coeff (poly_mult p []) = (\<lambda>_. \<zero>)"
+    using poly_mult_coeff[OF polynomial_in_carrier[OF assms], of "[]"]
+          poly_coeff_in_carrier[OF assms] by auto
+  thus "poly_mult p [] = []"
+    using coeff_iff_polynomial_cond[OF poly_mult_closed[OF assms, of "[]"]] zero_is_polynomial by auto
+qed
+
+lemma poly_mult_l_distr':
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "set p3 \<subseteq> carrier R"
+  shows "poly_mult (poly_add p1 p2) p3 = poly_add (poly_mult p1 p3) (poly_mult p2 p3)"
+proof -
+  let ?c1 = "coeff p1" and ?c2 = "coeff p2" and ?c3 = "coeff p3"
+  have in_carrier:
+    "\<And>i. ?c1 i \<in> carrier R" "\<And>i. ?c2 i \<in> carrier R" "\<And>i. ?c3 i \<in> carrier R"
+    using assms coeff_in_carrier by auto
+
+  have "coeff (poly_mult (poly_add p1 p2) p3) = (\<lambda>n. \<Oplus>i \<in> {..n}. (?c1 i \<oplus> ?c2 i) \<otimes> ?c3 (n - i))"
+    using poly_mult_coeff[of "poly_add p1 p2" p3]  poly_add_coeff[OF assms(1-2)]
+          poly_add_in_carrier[OF assms(1-2)] assms by auto
+  also have " ... = (\<lambda>n. \<Oplus>i \<in> {..n}. (?c1 i \<otimes> ?c3 (n - i)) \<oplus> (?c2 i \<otimes> ?c3 (n - i)))"
+    using in_carrier l_distr by auto
+  also
+  have " ... = (\<lambda>n. (\<Oplus>i \<in> {..n}. (?c1 i \<otimes> ?c3 (n - i))) \<oplus> (\<Oplus>i \<in> {..n}. (?c2 i \<otimes> ?c3 (n - i))))"
+    using add.finprod_multf in_carrier by auto
+  also have " ... = coeff (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
+    using poly_mult_coeff[OF assms(1) assms(3)] poly_mult_coeff[OF assms(2-3)]
+          poly_add_coeff[OF poly_mult_in_carrier[OF assms(1) assms(3)]]
+                            poly_mult_in_carrier[OF assms(2-3)] by simp
+  finally have "coeff (poly_mult (poly_add p1 p2) p3) =
+                coeff (poly_add (poly_mult p1 p3) (poly_mult p2 p3))" .
+  moreover have "polynomial R (poly_mult (poly_add p1 p2) p3)"
+            and "polynomial R (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
+    using assms poly_add_is_polynomial poly_mult_is_polynomial polynomial_in_carrier by auto
+  ultimately show ?thesis
+    using coeff_iff_polynomial_cond by auto 
+qed
+
+lemma poly_mult_l_distr:
+  assumes "polynomial R p1" "polynomial R p2" "polynomial R p3"
+  shows "poly_mult (poly_add p1 p2) p3 = poly_add (poly_mult p1 p3) (poly_mult p2 p3)"
+  using poly_mult_l_distr' polynomial_in_carrier assms by auto
+
+lemma poly_mult_append_replicate_zero:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_mult p1 p2 = poly_mult ((replicate n \<zero>) @ p1) p2"
+proof -
+  { fix p1 p2 assume A: "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+    hence "poly_mult p1 p2 = poly_mult (\<zero> # p1) p2"
+    proof -
+      let ?a_p2 = "(map ((\<otimes>) \<zero>) p2) @ (replicate (length p1) \<zero>)"
+      have "?a_p2 = replicate (length p2 + length p1) \<zero>"
+        using A(2) by (induction p2) (auto)
+      hence "poly_mult (\<zero> # p1) p2 = poly_add (replicate (length p2 + length p1) \<zero>) (poly_mult p1 p2)"
+        by (simp add: degree_def)
+      also have " ... = poly_add (normalize (replicate (length p2 + length p1) \<zero>)) (poly_mult p1 p2)"
+        using poly_add_normalize(1)[of "replicate (length p2 + length p1) \<zero>" "poly_mult p1 p2"]
+              poly_mult_in_carrier[OF A] by force
+      also have " ... = poly_mult p1 p2"
+        using poly_add_zero(2)[OF poly_mult_is_polynomial[OF A]]
+              normalize_replicate_zero[of "length p2 + length p1" "[]"] by auto
+      finally show ?thesis by auto
+    qed } note aux_lemma = this
+  
+  from assms show ?thesis
+  proof (induction n)
+    case 0 thus ?case by simp
+  next
+    case (Suc n) thus ?case
+      using aux_lemma[of "replicate n \<zero> @ p1" p2] by force
+  qed
+qed
+
+lemma poly_mult_normalize:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_mult p1 p2 = poly_mult (normalize p1) p2"
+proof -
+  let ?replicate = "replicate (length p1 - length (normalize p1)) \<zero>"
+  have "poly_mult p1 p2 = poly_mult (?replicate @ (normalize p1)) p2"
+    using normalize_def'[of p1] by simp
+  also have " ... = poly_mult (normalize p1) p2"
+    using poly_mult_append_replicate_zero polynomial_in_carrier
+          normalize_gives_polynomial assms by auto
+  finally show ?thesis .
+qed
+
+end
+
+
+subsection \<open>Properties Within a Domain\<close>
+
+context domain
+begin
+
+lemma one_is_polynomial [intro]: "polynomial R [ \<one> ]"
+  unfolding polynomial_def by auto
+
+lemma poly_mult_comm:
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R"
+  shows "poly_mult p1 p2 = poly_mult p2 p1"
+proof -
+  let ?c1 = "coeff p1" and ?c2 = "coeff p2"
+  have "\<And>i. (\<Oplus>k \<in> {..i}. ?c1 k \<otimes> ?c2 (i - k)) = (\<Oplus>k \<in> {..i}. ?c2 k \<otimes> ?c1 (i - k))"
+  proof -
+    fix i :: nat
+    let ?f = "\<lambda>k. ?c1 k \<otimes> ?c2 (i - k)"
+    have in_carrier: "\<And>i. ?c1 i \<in> carrier R" "\<And>i. ?c2 i \<in> carrier R"
+      using coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] by auto
+
+    have reindex_inj: "inj_on (\<lambda>k. i - k) {..i}"
+      using inj_on_def by force
+    moreover have "(\<lambda>k. i - k) ` {..i} \<subseteq> {..i}" by auto
+    hence "(\<lambda>k. i - k) ` {..i} = {..i}"
+      using reindex_inj endo_inj_surj[of "{..i}" "\<lambda>k. i - k"] by simp 
+    ultimately have "(\<Oplus>k \<in> {..i}. ?f k) = (\<Oplus>k \<in> {..i}. ?f (i - k))"
+      using add.finprod_reindex[of ?f "\<lambda>k. i - k" "{..i}"] in_carrier by auto
+
+    moreover have "\<And>k. k \<in> {..i} \<Longrightarrow> ?f (i - k) = ?c2 k \<otimes> ?c1 (i - k)"
+      using in_carrier m_comm by auto
+    hence "(\<Oplus>k \<in> {..i}. ?f (i - k)) = (\<Oplus>k \<in> {..i}. ?c2 k \<otimes> ?c1 (i - k))"
+      using add.finprod_cong'[of "{..i}" "{..i}"] in_carrier by auto
+    ultimately show "(\<Oplus>k \<in> {..i}. ?f k) = (\<Oplus>k \<in> {..i}. ?c2 k \<otimes> ?c1 (i - k))"
+      by simp
+  qed
+  hence "coeff (poly_mult p1 p2) = coeff (poly_mult p2 p1)"
+    using poly_mult_coeff[OF assms] poly_mult_coeff[OF assms(2) assms(1)] by simp
+  thus ?thesis
+    using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF assms]
+                                       poly_mult_is_polynomial[OF assms(2) assms(1)]] by simp
+qed
+
+lemma poly_mult_r_distr':
+  assumes "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "set p3 \<subseteq> carrier R"
+  shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)"
+  using poly_mult_comm[OF assms(1-2)] poly_mult_l_distr'[OF assms(2-3) assms(1)]
+        poly_mult_comm[OF assms(1) assms(3)] poly_add_is_polynomial[OF assms(2-3)]
+        polynomial_in_carrier poly_mult_comm[OF assms(1), of "poly_add p2 p3"] by simp
+
+lemma poly_mult_r_distr:
+  assumes "polynomial R p1" "polynomial R p2" "polynomial R p3"
+  shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)"
+  using poly_mult_r_distr' polynomial_in_carrier assms by auto
+
+lemma poly_mult_replicate_zero:
+  assumes "set p \<subseteq> carrier R"
+  shows "poly_mult (replicate n \<zero>) p = []"
+    and "poly_mult p (replicate n \<zero>) = []"
+proof -
+  have in_carrier: "\<And>n. set (replicate n \<zero>) \<subseteq> carrier R" by auto
+  show "poly_mult (replicate n \<zero>) p = []" using assms
+  proof (induction n)
+    case 0 thus ?case by simp
+  next
+    case (Suc n)
+    hence "poly_mult (replicate (Suc n) \<zero>) p = poly_mult (\<zero> # (replicate n \<zero>)) p"
+      by simp
+    also have " ... = poly_add ((map (\<lambda>a. \<zero> \<otimes> a) p) @ (replicate n \<zero>)) []"
+      using Suc by (simp add: degree_def)
+    also have " ... = poly_add ((map (\<lambda>a. \<zero>) p) @ (replicate n \<zero>)) []"
+      using Suc(2) by (smt map_eq_conv ring_simprules(24) subset_code(1))
+    also have " ... = poly_add (replicate (length p + n) \<zero>) []"
+      by (simp add: map_replicate_const replicate_add)
+    also have " ... = poly_add [] []"
+      using poly_add_normalize(1)[of "replicate (length p + n) \<zero>" "[]"]
+            normalize_replicate_zero[of "length p + n" "[]"] by auto
+    also have " ... = []" by simp
+    finally show ?case . 
+  qed
+  thus "poly_mult p (replicate n \<zero>) = []"
+    using poly_mult_comm[OF assms in_carrier] by simp
+qed
+
+lemma poly_mult_const:
+  assumes "polynomial R p" "a \<in> carrier R - { \<zero> }"
+  shows "poly_mult [ a ] p = map (\<lambda>b. a \<otimes> b) p" and "poly_mult p [ a ] = map (\<lambda>b. a \<otimes> b) p"
+proof -
+  show "poly_mult [ a ] p = map (\<lambda>b. a \<otimes> b) p"
+  proof -
+    have "poly_mult [ a ] p = poly_add (map (\<lambda>b. a \<otimes> b) p) []"
+      by (simp add: degree_def)
+    moreover have "polynomial R (map (\<lambda>b. a \<otimes> b) p)"
+    proof (cases p)
+      case Nil thus ?thesis by (simp add: polynomial_def)
+    next
+      case (Cons b ps)
+      hence "a \<otimes> lead_coeff p \<noteq> \<zero>"
+        using assms integral[of a "lead_coeff p"] unfolding polynomial_def by auto 
+      thus ?thesis
+        using Cons polynomial_in_carrier[OF assms(1)] assms(2) unfolding polynomial_def by auto 
+    qed
+    ultimately show ?thesis
+      using poly_add_zero(1)[of "map (\<lambda>b. a \<otimes> b) p"] by simp
+  qed
+  thus "poly_mult p [ a ] = map (\<lambda>b. a \<otimes> b) p"
+    using poly_mult_comm[of "[ a ]" p] polynomial_in_carrier[OF assms(1)] assms(2) by auto
+qed
+
+lemma poly_mult_monon:
+  assumes "polynomial R p" "a \<in> carrier R - { \<zero> }"
+  shows "poly_mult (monon a n) p =
+           (if p = [] then [] else (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
+proof (cases p)
+  case Nil thus ?thesis
+    using poly_mult_zero(2)[OF monon_is_polynomial[OF assms(2)]] by simp
+next
+  case (Cons b ps)
+  hence "lead_coeff ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) = a \<otimes> b"
+    by simp
+  hence "lead_coeff ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<noteq> \<zero>"
+    using Cons assms integral[of a b] unfolding polynomial_def by auto
+  moreover have "set ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) \<subseteq> carrier R"
+    using polynomial_in_carrier[OF assms(1)] assms(2) DiffD1 by auto 
+  ultimately have is_polynomial: "polynomial R ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
+    using Cons unfolding polynomial_def by auto
+
+  have "poly_mult (a # replicate n \<zero>) p =
+        poly_add ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) (poly_mult (replicate n \<zero>) p)"
+    by (simp add: degree_def)
+  also have " ... = poly_add ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) []"
+    using poly_mult_replicate_zero(1)[OF polynomial_in_carrier[OF assms(1)]] by simp
+  also have " ... = (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)"
+    using poly_add_zero(1)[OF is_polynomial] .
+  also have " ... = (if p = [] then [] else (map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>))"
+    using Cons by auto
+  finally show ?thesis unfolding monon_def .
+qed
+
+lemma poly_mult_one:
+  assumes "polynomial R p"
+  shows "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
+proof -
+  have "map (\<lambda>a. \<one> \<otimes> a) p = p"
+    using polynomial_in_carrier[OF assms] by (meson assms l_one map_idI  subsetCE) 
+  thus "poly_mult [ \<one> ] p = p" and "poly_mult p [ \<one> ] = p"
+    using poly_mult_const[OF assms, of \<one>] by auto
+qed
+
+lemma poly_mult_lead_coeff_aux:
+  assumes "polynomial R p1" "polynomial R p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
+  shows "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
+proof -
+  have p1: "lead_coeff p1 \<in> carrier R - { \<zero> }" and p2: "lead_coeff p2 \<in> carrier R - { \<zero> }"
+    using assms unfolding polynomial_def by auto
+
+  have "(coeff (poly_mult p1 p2)) (degree p1 + degree p2) = 
+        (\<Oplus> k \<in> {..((degree p1) + (degree p2))}.
+          (coeff p1) k \<otimes> (coeff p2) ((degree p1) + (degree p2) - k))"
+    using poly_mult_coeff assms(1-2) polynomial_in_carrier by auto
+  also have " ... = (lead_coeff p1) \<otimes> (lead_coeff p2)"
+  proof -
+    let ?f = "\<lambda>i. (coeff p1) i \<otimes> (coeff p2) ((degree p1) + (degree p2) - i)"
+    have in_carrier: "\<And>i. (coeff p1) i \<in> carrier R" "\<And>i. (coeff p2) i \<in> carrier R"
+      using coeff_in_carrier assms by auto
+    have "\<And>i. i < degree p1 \<Longrightarrow> ?f i = \<zero>"
+      using coeff_degree[of p2] in_carrier by auto
+    moreover have "\<And>i. i > degree p1 \<Longrightarrow> ?f i = \<zero>"
+      using coeff_degree[of p1] in_carrier by auto
+    moreover have "?f (degree p1) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
+      using assms(3-4) by simp
+    ultimately have "?f = (\<lambda>i. if degree p1 = i then (lead_coeff p1) \<otimes> (lead_coeff p2) else \<zero>)"
+      using nat_neq_iff by auto
+    thus ?thesis
+      using add.finprod_singleton[of "degree p1" "{..((degree p1) + (degree p2))}"
+                                     "\<lambda>i. (lead_coeff p1) \<otimes> (lead_coeff p2)"] p1 p2 by auto
+  qed
+  finally show ?thesis .
+qed
+
+lemma poly_mult_degree_eq:
+  assumes "polynomial R p1" "polynomial R p2"
+  shows "degree (poly_mult p1 p2) = (if p1 = [] \<or> p2 = [] then 0 else (degree p1) + (degree p2))"
+proof (cases p1)
+  case Nil thus ?thesis by (simp add: degree_def)
+next
+  case (Cons a p1') note p1 = Cons
+  show ?thesis
+  proof (cases p2)
+    case Nil thus ?thesis
+      using poly_mult_zero(2)[OF assms(1)] by (simp add: degree_def)
+  next
+    case (Cons b p2') note p2 = Cons
+    have a: "a \<in> carrier R" and b: "b \<in> carrier R"
+      using p1 p2 polynomial_in_carrier[OF assms(1)] polynomial_in_carrier[OF assms(2)] by auto
+    have "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) = a \<otimes> b"
+      using poly_mult_lead_coeff_aux[OF assms] p1 p2 by simp
+    hence "(coeff (poly_mult p1 p2)) ((degree p1) + (degree p2)) \<noteq> \<zero>"
+      using assms p1 p2 integral[of a b] unfolding polynomial_def by auto
+    moreover have "\<And>i. i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
+    proof -
+      have aux_lemma: "degree (poly_mult p1 p2) \<le> (degree p1) + (degree p2)"
+      proof (induct p1)
+        case Nil
+        then show ?case by simp
+      next
+        case (Cons a p1)
+        let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (degree (a # p1)) \<zero>)"
+        have "poly_mult (a # p1) p2 = poly_add ?a_p2 (poly_mult p1 p2)" by simp
+        hence "degree (poly_mult (a # p1) p2) \<le> max (degree ?a_p2) (degree (poly_mult p1 p2))"
+          using poly_add_degree[of ?a_p2 "poly_mult p1 p2"] by simp
+        also have " ... \<le> max ((degree (a # p1)) + (degree p2)) (degree (poly_mult p1 p2))"
+          unfolding degree_def by auto
+        also have " ... \<le> max ((degree (a # p1)) + (degree p2)) ((degree p1) + (degree p2))"
+          using Cons by simp
+        also have " ... \<le> (degree (a # p1)) + (degree p2)"
+          unfolding degree_def by auto
+        finally show ?case .
+      qed
+      fix i show "i > (degree p1) + (degree p2) \<Longrightarrow> (coeff (poly_mult p1 p2)) i = \<zero>"
+        using coeff_degree aux_lemma by simp
+    qed
+    ultimately have "degree (poly_mult p1 p2) = degree p1 + degree p2"
+      using degree_def'[OF poly_mult_closed[OF assms]]
+      by (smt coeff_degree linorder_cases not_less_Least)
+    thus ?thesis
+      using p1 p2 by auto
+  qed
+qed
+
+lemma poly_mult_integral:
+  assumes "polynomial R p1" "polynomial R p2"
+  shows "poly_mult p1 p2 = [] \<Longrightarrow> p1 = [] \<or> p2 = []"
+proof (rule ccontr)
+  assume A: "poly_mult p1 p2 = []" "\<not> (p1 = [] \<or> p2 = [])"
+  hence "degree (poly_mult p1 p2) = degree p1 + degree p2"
+    using poly_mult_degree_eq[OF assms] by simp
+  hence "length p1 = 1 \<and> length p2 = 1"
+    unfolding degree_def using A Suc_diff_Suc by fastforce
+  then obtain a b where p1: "p1 = [ a ]" and p2: "p2 = [ b ]"
+    by (metis One_nat_def length_0_conv length_Suc_conv)
+  hence "a \<in> carrier R - { \<zero> }" and "b \<in> carrier R - { \<zero> }"
+    using assms unfolding polynomial_def by auto
+  hence "poly_mult [ a ] [ b ] = [ a \<otimes> b ]"
+    using A assms(2) poly_mult_const(1) p1 by fastforce
+  thus False using A(1) p1 p2 by simp
+qed
+
+lemma poly_mult_lead_coeff:
+  assumes "polynomial R p1" "polynomial R p2" and "p1 \<noteq> []" and "p2 \<noteq> []"
+  shows "lead_coeff (poly_mult p1 p2) = (lead_coeff p1) \<otimes> (lead_coeff p2)"
+proof -
+  have "poly_mult p1 p2 \<noteq> []"
+    using poly_mult_integral[OF assms(1-2)] assms(3-4) by auto
+  hence "lead_coeff (poly_mult p1 p2) = (coeff (poly_mult p1 p2)) (degree p1 + degree p2)"
+    using poly_mult_degree_eq[OF assms(1-2)] assms(3-4) by (metis coeff.simps(2) list.collapse)
+  thus ?thesis
+    using poly_mult_lead_coeff_aux[OF assms] by simp
+qed
+
+end
+
+
+subsection \<open>Algebraic Structure of Polynomials\<close>
+
+definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow> ('a list) ring"
+  where "univ_poly R =
+           \<lparr> carrier = { p. polynomial R p },
+         monoid.mult = ring.poly_mult R,
+                 one = [ \<one>\<^bsub>R\<^esub> ],
+                zero = [],
+                 add = ring.poly_add R \<rparr>"
+
+context domain
+begin
+
+lemma poly_mult_assoc_aux:
+  assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
+    shows "poly_mult ((map (\<lambda>b. a \<otimes> b) p) @ (replicate n \<zero>)) q =
+           poly_mult (monon a n) (poly_mult p q)"
+proof -
+  let ?len = "n"
+  let ?a_p = "(map (\<lambda>b. a \<otimes> b) p) @ (replicate ?len \<zero>)"
+  let ?c2 = "coeff p" and ?c3 = "coeff q"
+  have coeff_a_p:
+    "coeff ?a_p = (\<lambda>i. if i < ?len then \<zero> else a \<otimes> ?c2 (i - ?len))" (is
+    "coeff ?a_p = (\<lambda>i. ?f i)")
+    using append_coeff[of "map ((\<otimes>) a) p" "replicate ?len \<zero>"]
+          replicate_zero_coeff[of ?len] scalar_coeff[OF assms(3), of p] by auto
+  have in_carrier:
+    "set ?a_p \<subseteq> carrier R" "\<And>i. ?c2 i \<in> carrier R" "\<And>i. ?c3 i \<in> carrier R"
+    "\<And>i. coeff (poly_mult p q) i \<in> carrier R"
+    using assms poly_mult_in_carrier by auto
+  have "coeff (poly_mult ?a_p q) = (\<lambda>n. (\<Oplus>i \<in> {..n}. (coeff ?a_p) i \<otimes> ?c3 (n - i)))"
+    using poly_mult_coeff[OF in_carrier(1) assms(2)] .
+  also have " ... = (\<lambda>n. (\<Oplus>i \<in> {..n}. (?f i) \<otimes> ?c3 (n - i)))"
+    using coeff_a_p by simp
+  also have " ... = (\<lambda>n. (\<Oplus>i \<in> {..n}. (if i = ?len then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i)))"
+    (is "(\<lambda>n. (\<Oplus>i \<in> {..n}. ?side1 n i)) = (\<lambda>n. (\<Oplus>i \<in> {..n}. ?side2 n i))")
+  proof
+    fix n
+    have in_carrier': "\<And>i. ?side1 n i \<in> carrier R" "\<And>i. ?side2 n i \<in> carrier R"
+      using in_carrier assms coeff_in_carrier poly_mult_in_carrier by auto
+    show "(\<Oplus>i \<in> {..n}. ?side1 n i) = (\<Oplus>i \<in> {..n}. ?side2 n i)"
+    proof (cases "n < ?len")
+      assume "n < ?len"
+      hence "\<And>i. i \<le> n \<Longrightarrow> ?side1 n i = ?side2 n i"
+        using in_carrier assms coeff_in_carrier poly_mult_in_carrier by simp
+      thus ?thesis
+        using add.finprod_cong'[of "{..n}" "{..n}" "?side1 n" "?side2 n"] in_carrier'
+        by (metis (no_types, lifting) Pi_I' atMost_iff)
+    next
+      assume "\<not> n < ?len"
+      hence n_ge: "n \<ge> ?len" by simp
+      define h where "h = (\<lambda>i. if i < ?len then \<zero> else (a \<otimes> ?c2 (i - ?len)) \<otimes> ?c3 (n - i))"
+      hence h_in_carrier: "\<And>i. h i \<in> carrier R"
+        using assms(3) in_carrier by auto
+      have "\<And>i. (?f i) \<otimes> ?c3 (n - i) = h i"
+        using in_carrier(2-3) assms(3) h_def by auto
+      hence "(\<Oplus>i \<in> {..n}. ?side1 n i) = (\<Oplus>i \<in> {..n}. h i)"
+        by simp
+      also have " ... = (\<Oplus>i \<in> {..<?len}. h i) \<oplus> (\<Oplus>i \<in> {?len..n}. h i)"
+        using add.finprod_Un_disjoint[of "{..<?len}" "{?len..n}" h] h_in_carrier n_ge
+        by (simp add: ivl_disj_int_one(4) ivl_disj_un_one(4))
+      also have " ... = (\<Oplus>i \<in> {..<?len}. \<zero>) \<oplus> (\<Oplus>i \<in> {?len..n}. h i)"
+        using add.finprod_cong'[of "{..<?len}" "{..<?len}" h "\<lambda>_. \<zero>"] h_in_carrier
+        unfolding h_def by auto
+      also have " ... = (\<Oplus>i \<in> {?len..n}. h i)"
+        using add.finprod_one h_in_carrier by simp
+      also have " ... = (\<Oplus>i \<in> (\<lambda>i. i + ?len) ` {..n - ?len}. h i)"
+        using n_ge atLeast0AtMost image_add_atLeastAtMost'[of ?len 0 "n - ?len"] by auto
+      also have " ... = (\<Oplus>i \<in> {..n - ?len}. h (i + ?len))"
+        using add.finprod_reindex[of h "\<lambda>i. i + ?len" "{..n - ?len}"] h_in_carrier by simp
+      also have " ... = (\<Oplus>i \<in> {..n - ?len}. (a \<otimes> ?c2 i) \<otimes> ?c3 (n - (i + ?len)))"
+        unfolding h_def by simp
+      also have " ... = (\<Oplus>i \<in> {..n - ?len}. a \<otimes> (?c2 i \<otimes> ?c3 (n - (i + ?len))))"
+        using in_carrier assms(3) by (simp add: m_assoc) 
+      also have " ... = a \<otimes> (\<Oplus>i \<in> {..n - ?len}. ?c2 i \<otimes> ?c3 (n - (i + ?len)))"
+        using finsum_rdistr[of "{..n - ?len}" a "\<lambda>i. ?c2 i \<otimes> ?c3 (n - (i + ?len))"]
+              in_carrier(2-3) assms(3) by simp
+      also have " ... = a \<otimes> (coeff (poly_mult p q)) (n - ?len)"
+        using poly_mult_coeff[OF assms(1-2)] n_ge by (simp add: add.commute)
+      also have " ... =
+        (\<Oplus>i \<in> {..n}. if ?len = i then a \<otimes> (coeff (poly_mult p q)) (n - i) else \<zero>)"
+        using add.finprod_singleton[of ?len "{..n}" "\<lambda>i. a \<otimes> (coeff (poly_mult p q)) (n - i)"]
+              n_ge in_carrier(2-4) assms by simp
+      also have " ... = (\<Oplus>i \<in> {..n}. (if ?len = i then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i))"
+        using in_carrier(2-4) assms(3) add.finprod_cong'[of "{..n}" "{..n}"] by simp
+      also have " ... = (\<Oplus>i \<in> {..n}. ?side2 n i)"
+      proof -
+        have "(\<lambda>i. (if ?len = i then a else \<zero>) \<otimes> (coeff (poly_mult p q)) (n - i)) = ?side2 n" by auto
+        thus ?thesis by simp
+      qed
+      finally show ?thesis .
+    qed
+  qed
+  also have " ... = coeff (poly_mult (monon a n) (poly_mult p q))"
+    using monon_coeff[of a "n"] poly_mult_coeff[of "monon a n" "poly_mult p q"]
+          poly_mult_in_carrier[OF assms(1-2)] assms(3) unfolding monon_def by force
+  finally
+  have "coeff (poly_mult ?a_p q) = coeff (poly_mult (monon a n) (poly_mult p q))" .
+  moreover have "polynomial R (poly_mult ?a_p q)"
+    using poly_mult_is_polynomial[OF in_carrier(1) assms(2)] by simp
+  moreover have "polynomial R (poly_mult (monon a n) (poly_mult p q))"
+    using poly_mult_is_polynomial[of "monon a n" "poly_mult p q"]
+          poly_mult_in_carrier[OF assms(1-2)] assms(3) unfolding monon_def
+    using in_carrier(1) by auto
+  ultimately show ?thesis
+    using coeff_iff_polynomial_cond by simp
+qed
+
+lemma univ_poly_is_monoid: "monoid (univ_poly R)"
+  unfolding univ_poly_def using poly_mult_one
+proof (auto simp add: poly_add_closed poly_mult_closed one_is_polynomial monoid_def)
+  fix p1 p2 p3
+  let ?P = "poly_mult (poly_mult p1 p2) p3 = poly_mult p1 (poly_mult p2 p3)"
+
+  assume A: "polynomial R p1" "polynomial R p2" "polynomial R p3"
+  show ?P using polynomial_in_carrier[OF A(1)]
+  proof (induction p1)
+    case Nil thus ?case by simp
+  next
+    case (Cons a p1) thus ?case
+    proof (cases "a = \<zero>")
+      assume eq_zero: "a = \<zero>"
+      have p1: "set p1 \<subseteq> carrier R"
+        using Cons(2) by simp
+      have "poly_mult (poly_mult (a # p1) p2) p3 = poly_mult (poly_mult p1 p2) p3"
+        using poly_mult_append_replicate_zero[OF p1 polynomial_in_carrier[OF A(2)], of "Suc 0"]
+              eq_zero by simp
+      also have " ... = poly_mult p1 (poly_mult p2 p3)"
+        using p1[THEN Cons(1)] by simp
+      also have " ... = poly_mult (a # p1) (poly_mult p2 p3)"
+        using poly_mult_append_replicate_zero[OF p1
+              poly_mult_in_carrier[OF A(2-3)[THEN polynomial_in_carrier]], of "Suc 0"] eq_zero by simp
+      finally show ?thesis .
+    next
+      assume "a \<noteq> \<zero>" hence in_carrier:
+        "set p1 \<subseteq> carrier R" "set p2 \<subseteq> carrier R" "set p3 \<subseteq> carrier R" "a \<in> carrier R - { \<zero> }"
+        using A(2-3) polynomial_in_carrier Cons by auto
+
+      let ?a_p2 = "(map (\<lambda>b. a \<otimes> b) p2) @ (replicate (length p1) \<zero>)"
+      have a_p2_in_carrier: "set ?a_p2 \<subseteq> carrier R"
+        using in_carrier by auto
+
+      have "poly_mult (poly_mult (a # p1) p2) p3 = poly_mult (poly_add ?a_p2 (poly_mult p1 p2)) p3"
+        by (simp add: degree_def)
+      also have " ... = poly_add (poly_mult ?a_p2 p3) (poly_mult (poly_mult p1 p2) p3)"
+        using poly_mult_l_distr'[OF a_p2_in_carrier poly_mult_in_carrier[OF in_carrier(1-2)] in_carrier(3)] .
+      also have " ... = poly_add (poly_mult ?a_p2 p3) (poly_mult p1 (poly_mult p2 p3))"
+        using Cons(1)[OF in_carrier(1)] by simp
+      also have " ... = poly_add (poly_mult (a # (replicate (length p1) \<zero>)) (poly_mult p2 p3))
+                                 (poly_mult p1 (poly_mult p2 p3))"
+        using poly_mult_assoc_aux[of p2 p3 a "length p1"] in_carrier unfolding monon_def by simp
+      also have " ... = poly_mult (poly_add (a # (replicate (length p1) \<zero>)) p1) (poly_mult p2 p3)"
+        using poly_mult_l_distr'[of "a # (replicate (length p1) \<zero>)" p1 "poly_mult p2 p3"]
+              poly_mult_in_carrier[OF in_carrier(2-3)] in_carrier by force
+      also have " ... = poly_mult (a # p1) (poly_mult p2 p3)"
+        using poly_add_monon[OF in_carrier(1) in_carrier(4)] unfolding monon_def by simp
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+declare poly_add.simps[simp del]
+
+lemma univ_poly_is_abelian_monoid: "abelian_monoid (univ_poly R)"
+  unfolding univ_poly_def
+  using poly_add_closed poly_add_zero zero_is_polynomial
+proof (auto simp add: abelian_monoid_def comm_monoid_def monoid_def comm_monoid_axioms_def)
+  fix p1 p2 p3
+  let ?c = "\<lambda>p. coeff p"
+  assume A: "polynomial R p1" "polynomial R p2" "polynomial R p3"
+  hence
+    p1: "\<And>i. (?c p1) i \<in> carrier R" "set p1 \<subseteq> carrier R" and
+    p2: "\<And>i. (?c p2) i \<in> carrier R" "set p2 \<subseteq> carrier R" and
+    p3: "\<And>i. (?c p3) i \<in> carrier R" "set p3 \<subseteq> carrier R"
+    using polynomial_in_carrier by auto
+  have "?c (poly_add (poly_add p1 p2) p3) = (\<lambda>i. (?c p1 i \<oplus> ?c p2 i) \<oplus> (?c p3 i))"
+    using poly_add_coeff[OF poly_add_in_carrier[OF p1(2) p2(2)] p3(2)]
+          poly_add_coeff[OF p1(2) p2(2)] by simp
+  also have " ... = (\<lambda>i. (?c p1 i) \<oplus> ((?c p2 i) \<oplus> (?c p3 i)))"
+    using p1 p2 p3 add.m_assoc by simp
+  also have " ... = ?c (poly_add p1 (poly_add p2 p3))"
+    using poly_add_coeff[OF p1(2) poly_add_in_carrier[OF p2(2) p3(2)]]
+          poly_add_coeff[OF p2(2) p3(2)] by simp
+  finally have "?c (poly_add (poly_add p1 p2) p3) = ?c (poly_add p1 (poly_add p2 p3))" .
+  thus "poly_add (poly_add p1 p2) p3 = poly_add p1 (poly_add p2 p3)"
+    using coeff_iff_polynomial_cond poly_add_closed A by auto
+  show "poly_add p1 p2 = poly_add p2 p1"
+    using poly_add_comm[OF p1(2) p2(2)] .
+qed
+
+lemma univ_poly_is_abelian_group: "abelian_group (univ_poly R)"
+proof -
+  interpret abelian_monoid "univ_poly R"
+    using univ_poly_is_abelian_monoid .
+  show ?thesis
+  proof (unfold_locales)
+    show "carrier (add_monoid (univ_poly R)) \<subseteq> Units (add_monoid (univ_poly R))"
+      unfolding univ_poly_def Units_def
+    proof (auto)
+      fix p assume p: "polynomial R p"
+      have "polynomial R [ \<ominus> \<one> ]"
+        unfolding polynomial_def using r_neg by fastforce 
+      hence cond0: "polynomial R (poly_mult [ \<ominus> \<one> ] p)"
+        using poly_mult_closed[of "[ \<ominus> \<one> ]" p] p by simp
+      
+      have "poly_add p (poly_mult [ \<ominus> \<one> ] p) = poly_add (poly_mult [ \<one> ] p) (poly_mult [ \<ominus> \<one> ] p)"
+        using poly_mult_one[OF p] by simp
+      also have " ... = poly_mult (poly_add [ \<one> ] [ \<ominus> \<one> ]) p"
+        using poly_mult_l_distr' polynomial_in_carrier[OF p] by auto
+      also have " ... = poly_mult [] p"
+        using poly_add.simps[of "[ \<one> ]" "[ \<ominus> \<one> ]"]
+        by (simp add: case_prod_unfold r_neg)
+      also have " ... = []" by simp
+      finally have cond1: "poly_add p (poly_mult [ \<ominus> \<one> ] p) = []" .
+
+      have "poly_add (poly_mult [ \<ominus> \<one> ] p) p = poly_add (poly_mult [ \<ominus> \<one> ] p) (poly_mult [ \<one> ] p)"
+        using poly_mult_one[OF p] by simp
+      also have " ... = poly_mult (poly_add [ \<ominus>  \<one> ] [ \<one> ]) p"
+        using poly_mult_l_distr' polynomial_in_carrier[OF p] by auto
+      also have " ... = poly_mult [] p"
+        using \<open>poly_mult (poly_add [\<one>] [\<ominus> \<one>]) p = poly_mult [] p\<close> poly_add_comm by auto
+      also have " ... = []" by simp
+      finally have cond2: "poly_add (poly_mult [ \<ominus> \<one> ] p) p = []" .
+
+      from cond0 cond1 cond2 show "\<exists>q. polynomial R q \<and> poly_add q p = [] \<and> poly_add p q = []"
+        by auto
+    qed
+  qed
+qed
+
+declare poly_add.simps[simp]
+
+end
+
+lemma univ_poly_is_ring:
+  assumes "domain R"
+  shows "ring (univ_poly R)"
+proof -
+  interpret abelian_group "univ_poly R" + monoid "univ_poly R"
+    using domain.univ_poly_is_abelian_group[OF assms] domain.univ_poly_is_monoid[OF assms] .
+  have R: "ring R"
+    using assms unfolding domain_def cring_def by simp
+  show ?thesis
+    apply unfold_locales
+    apply (auto simp add: univ_poly_def assms domain.poly_mult_r_distr ring.poly_mult_l_distr[OF R])
+    done
+qed
+
+lemma univ_poly_is_cring:
+  assumes "domain R"
+  shows "cring (univ_poly R)"
+proof -
+  interpret ring "univ_poly R"
+    using univ_poly_is_ring[OF assms] by simp
+  have "\<And>p q. \<lbrakk> p \<in> carrier (univ_poly R); q \<in> carrier (univ_poly R) \<rbrakk> \<Longrightarrow>
+                p \<otimes>\<^bsub>univ_poly R\<^esub> q = q \<otimes>\<^bsub>univ_poly R\<^esub> p"
+    unfolding univ_poly_def polynomial_def using domain.poly_mult_comm[OF assms] by auto
+  thus ?thesis
+    by unfold_locales auto
+qed
+
+lemma univ_poly_is_domain:
+  assumes "domain R"
+  shows "domain (univ_poly R)"
+proof -
+  interpret cring "univ_poly R"
+    using univ_poly_is_cring[OF assms] by simp
+  show ?thesis
+    by unfold_locales
+      (auto simp add: univ_poly_def domain.poly_mult_integral[OF assms])
+qed
+
+
+subsection \<open>Long Division Theorem\<close>
+
+lemma (in domain) long_division_theorem:
+  assumes "polynomial R p" "polynomial R b" and "b \<noteq> []" and "lead_coeff b \<in> Units R"
+  shows "\<exists>q r. polynomial R q \<and> polynomial R r \<and>
+               p = poly_add (poly_mult b q) r \<and> (r = [] \<or> degree r < degree b)"
+    (is "\<exists>q r. ?long_division p q r")
+  using assms
+proof (induct "length p" arbitrary: p rule: less_induct)
+  case less thus ?case
+  proof (cases p)
+    case Nil
+    hence "?long_division p [] []"
+      using zero_is_polynomial poly_mult_zero[OF less(3)] by (simp add: degree_def)
+    thus ?thesis by blast
+  next
+    case (Cons a p') thus ?thesis
+    proof (cases "length b > length p")
+      assume "length b > length p"
+      hence "p = [] \<or> degree p < degree b" unfolding degree_def
+        by (meson diff_less_mono length_0_conv less_one not_le) 
+      hence "?long_division p [] p"
+        using poly_add_zero[OF less(2)] less(2) zero_is_polynomial
+              poly_mult_zero[OF less(3)] by simp
+      thus ?thesis by blast
+    next
+      interpret UP: cring "univ_poly R"
+        using univ_poly_is_cring[OF is_domain] .
+
+      assume "\<not> length b > length p"
+      hence len_ge: "length p \<ge> length b" by simp
+      obtain c b' where b: "b = c # b'"
+        using less(4) list.exhaust_sel by blast
+      hence c: "c \<in> Units R" "c \<in> carrier R - { \<zero> }" and a: "a \<in> carrier R - { \<zero> }"
+        using assms(4) less(2-3) Cons unfolding polynomial_def by auto
+      hence "(\<ominus> a) \<in> carrier R - { \<zero> }"
+        using r_neg by force
+      hence in_carrier: "(\<ominus> a) \<otimes> inv c \<in> carrier R - { \<zero> }"
+        using a c(2) Units_inv_closed[OF c(1)] Units_l_inv[OF c(1)]
+             empty_iff insert_iff integral_iff m_closed
+        by (metis Diff_iff zero_not_one)
+
+      let ?len = "length"
+      define s where "s = poly_mult (monon ((\<ominus> a) \<otimes> inv c) (?len p - ?len b)) b"
+      hence s_coeff: "lead_coeff s = (\<ominus> a)"
+        using poly_mult_lead_coeff[OF monon_is_polynomial[OF in_carrier] less(3)] a c
+        unfolding monon_def s_def b using m_assoc by force
+      
+      have "degree s = degree (monon ((\<ominus> a) \<otimes> inv c) (?len p - ?len b)) + degree b"
+        using poly_mult_degree_eq[OF monon_is_polynomial[OF in_carrier] less(3)]
+        unfolding s_def b monon_def by auto
+      hence "?len s - 1 = ?len p - 1"
+        using len_ge unfolding b Cons by (simp add: monon_def degree_def)
+      moreover have "s \<noteq> []"
+        using poly_mult_integral[OF monon_is_polynomial[OF in_carrier] less(3)]
+        unfolding s_def monon_def b by blast
+      hence "?len s > 0" by simp
+      ultimately have len_eq: "?len s  = ?len p"
+        by (simp add: Nitpick.size_list_simp(2) local.Cons)
+
+      obtain s' where s: "s = (\<ominus> a) # s'"
+        using s_coeff len_eq by (metis \<open>s \<noteq> []\<close> hd_Cons_tl) 
+
+      define p_diff where "p_diff = poly_add p s"
+      hence "?len p_diff < ?len p"
+        using len_eq s_coeff in_carrier a c unfolding s Cons apply simp
+        by (metis le_imp_less_Suc length_map map_fst_zip normalize_length_le r_neg)
+      moreover have "polynomial R p_diff" unfolding p_diff_def s_def
+        using poly_mult_closed[OF monon_is_polynomial[OF in_carrier(1)] less(3)]
+              poly_add_closed[OF less(2)] by simp
+      ultimately
+      obtain q' r' where l_div: "?long_division p_diff q' r'"
+        using less(1)[of p_diff] less(3-5) by blast
+      hence r': "polynomial R r'" and q': "polynomial R q'" by auto
+
+      obtain m where m: "polynomial R m" "s = poly_mult m b"
+        using s_def monon_is_polynomial[OF in_carrier(1)] by auto
+      have in_univ_carrier:
+         "p \<in> carrier (univ_poly R)"  "m \<in> carrier (univ_poly R)" "b \<in> carrier (univ_poly R)"
+        "r' \<in> carrier (univ_poly R)" "q' \<in> carrier (univ_poly R)" 
+        using r' q' less(2-3) m(1) unfolding univ_poly_def by auto
+
+      hence "poly_add p (poly_mult m b) = poly_add (poly_mult b q') r'"
+        using m l_div unfolding p_diff_def by simp
+      hence "p \<oplus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b) = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> q') \<oplus>\<^bsub>(univ_poly R)\<^esub> r'"
+        unfolding univ_poly_def by auto
+      hence
+        "(p \<oplus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)) \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b) =
+        ((b \<otimes>\<^bsub>(univ_poly R)\<^esub>q') \<oplus>\<^bsub>(univ_poly R)\<^esub> r') \<ominus>\<^bsub>(univ_poly R)\<^esub> (m \<otimes>\<^bsub>(univ_poly R)\<^esub> b)"
+        by simp
+      hence "p = (b \<otimes>\<^bsub>(univ_poly R)\<^esub> (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) \<oplus>\<^bsub>(univ_poly R)\<^esub> r'" 
+        using in_univ_carrier by algebra
+      hence "p = poly_add (poly_mult b (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)) r'"
+        unfolding univ_poly_def by simp
+      moreover have "q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m \<in> carrier (univ_poly R)"
+        using UP.ring_simprules in_univ_carrier by simp
+      hence "polynomial R (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m)"
+        unfolding univ_poly_def by simp
+      ultimately have "?long_division p (q' \<ominus>\<^bsub>(univ_poly R)\<^esub> m) r'"
+        using l_div r' by simp
+      thus ?thesis by blast
+    qed
+  qed
+qed
+
+lemma (in field) field_long_division_theorem:
+  assumes "polynomial R p" "polynomial R b" and "b \<noteq> []"
+  shows "\<exists>q r. polynomial R q \<and> polynomial R r \<and>
+               p = poly_add (poly_mult b q) r \<and> (r = [] \<or> degree r < degree b)"
+  using long_division_theorem[OF assms] assms lead_coeff_not_zero[of "hd b" "tl b"]
+  by (simp add: field_Units)
+
+lemma univ_poly_is_euclidean_domain:
+  assumes "field R"
+  shows "euclidean_domain (univ_poly R) degree"
+proof -
+  interpret domain "univ_poly R"
+    using univ_poly_is_domain assms field_def by blast
+  show ?thesis
+    apply (rule euclidean_domainI)
+    unfolding univ_poly_def
+    using field.field_long_division_theorem[OF assms] by auto
+qed
+
+
+subsection \<open>Consistency Rules\<close>
+
+lemma (in ring) subring_is_ring: (* <- Move to Subrings.thy *)
+  assumes "subring K R" shows "ring (R \<lparr> carrier := K \<rparr>)"
+  using assms unfolding subring_iff[OF subringE(1)[OF assms]] .
+
+lemma (in ring) eval_consistent [simp]:
+  assumes "subring K R" shows "ring.eval (R \<lparr> carrier := K \<rparr>) = eval"
+proof
+  fix p show "ring.eval (R \<lparr> carrier := K \<rparr>) p = eval p"
+    using nat_pow_consistent ring.eval.simps[OF subring_is_ring[OF assms]] by (induct p) (auto)
+qed
+
+lemma (in ring) coeff_consistent [simp]:
+  assumes "subring K R" shows "ring.coeff (R \<lparr> carrier := K \<rparr>) = coeff"
+proof
+  fix p show "ring.coeff (R \<lparr> carrier := K \<rparr>) p = coeff p"
+    using ring.coeff.simps[OF subring_is_ring[OF assms]] by (induct p) (auto)
+qed
+
+lemma (in ring) normalize_consistent [simp]:
+  assumes "subring K R" shows "ring.normalize (R \<lparr> carrier := K \<rparr>) = normalize"
+proof
+  fix p show "ring.normalize (R \<lparr> carrier := K \<rparr>) p = normalize p"
+    using ring.normalize.simps[OF subring_is_ring[OF assms]] by (induct p) (auto)
+qed
+
+lemma (in ring) poly_add_consistent [simp]:
+  assumes "subring K R" shows "ring.poly_add (R \<lparr> carrier := K \<rparr>) = poly_add" 
+proof -
+  have "\<And>p q. ring.poly_add (R \<lparr> carrier := K \<rparr>) p q = poly_add p q"
+  proof -
+    fix p q show "ring.poly_add (R \<lparr> carrier := K \<rparr>) p q = poly_add p q"
+    using ring.poly_add.simps[OF subring_is_ring[OF assms]] normalize_consistent[OF assms] by auto
+  qed
+  thus ?thesis by (auto simp del: poly_add.simps)
+qed
+
+lemma (in ring) poly_mult_consistent [simp]:
+  assumes "subring K R" shows "ring.poly_mult (R \<lparr> carrier := K \<rparr>) = poly_mult"
+proof -
+  have "\<And>p q. ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
+  proof - 
+    fix p q show "ring.poly_mult (R \<lparr> carrier := K \<rparr>) p q = poly_mult p q"
+      using ring.poly_mult.simps[OF subring_is_ring[OF assms]] poly_add_consistent[OF assms]
+      by (induct p) (auto)
+  qed
+  thus ?thesis by auto
+qed
+
+lemma (in ring) univ_poly_carrier_change_def':
+  assumes "subring K R"
+  shows "univ_poly (R \<lparr> carrier := K \<rparr>) = (univ_poly R) \<lparr> carrier := { p. polynomial R p \<and> set p \<subseteq> K } \<rparr>"
+  unfolding univ_poly_def polynomial_def
+  using poly_add_consistent[OF assms]
+        poly_mult_consistent[OF assms]
+        subringE(1)[OF assms]
+  by auto
+
+
+subsection \<open>The Evaluation Homomorphism\<close>
+
+lemma (in ring) eval_replicate:
+  assumes "set p \<subseteq> carrier R" "a \<in> carrier R"
+  shows "eval ((replicate n \<zero>) @ p) a = eval p a"
+  using assms eval_in_carrier by (induct n) (auto)
+
+lemma (in ring) eval_normalize:
+  assumes "set p \<subseteq> carrier R" "a \<in> carrier R"
+  shows "eval (normalize p) a = eval p a"
+  using eval_replicate[OF normalize_in_carrier] normalize_def'[of p] assms by metis
+
+lemma (in ring) eval_poly_add_aux:
+  assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "length p = length q" and "a \<in> carrier R"
+  shows "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+proof -
+  have "eval (map2 (\<oplus>) p q) a = (eval p a) \<oplus> (eval q a)"
+    using assms
+  proof (induct p arbitrary: q)
+    case Nil
+    then show ?case by simp
+  next
+    case (Cons b1 p')
+    then obtain b2 q' where q: "q = b2 # q'"
+      by (metis length_Cons list.exhaust list.size(3) nat.simps(3))
+    show ?case
+      using eval_in_carrier[OF _ Cons(5), of q']
+            eval_in_carrier[OF _ Cons(5), of p'] Cons unfolding q
+      by (auto simp add: degree_def ring_simprules(7,13,22))
+  qed
+  moreover have "set (map2 (\<oplus>) p q) \<subseteq> carrier R"
+    using assms(1-2)
+    by (induct p arbitrary: q) (auto, metis add.m_closed in_set_zipE set_ConsD subsetCE)
+  ultimately show ?thesis
+    using assms(3) eval_normalize[OF _ assms(4), of "map2 (\<oplus>) p q"] by auto
+qed
+
+lemma (in ring) eval_poly_add:
+  assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
+  shows "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+proof -
+  { fix p q assume A: "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" "length p \<ge> length q"
+    hence "eval (poly_add p ((replicate (length p - length q) \<zero>) @ q)) a =
+         (eval p a) \<oplus> (eval ((replicate (length p - length q) \<zero>) @ q) a)"
+      using eval_poly_add_aux[OF A(1) _ _ assms(3), of "(replicate (length p - length q) \<zero>) @ q"] by force
+    hence "eval (poly_add p q) a = (eval p a) \<oplus> (eval q a)"
+      using eval_replicate[OF A(2) assms(3)] A(3) by auto }
+  note aux_lemma = this
+
+  have ?thesis if "length q \<ge> length p"
+    using assms(1-2)[THEN eval_in_carrier[OF _ assms(3)]] poly_add_comm[OF assms(1-2)]
+          aux_lemma[OF assms(2,1) that]
+    by (auto simp del: poly_add.simps simp add: add.m_comm)
+  moreover have ?thesis if "length p \<ge> length q"
+    using aux_lemma[OF assms(1-2) that] .
+  ultimately show ?thesis by auto
+qed
+
+lemma (in ring) eval_append_aux:
+  assumes "set p \<subseteq> carrier R" and "b \<in> carrier R" and "a \<in> carrier R"
+  shows "eval (p @ [ b ]) a = ((eval p a) \<otimes> a) \<oplus> b"
+  using assms(1)
+proof (induct p)
+  case Nil thus ?case by (auto simp add: degree_def assms(2-3))
+next
+  case (Cons l q)
+  have "a [^] length q \<in> carrier R" "eval q a \<in> carrier R"
+    using eval_in_carrier Cons(2) assms(2-3) by auto
+  thus ?case
+    using Cons assms(2-3) by (auto simp add: degree_def, algebra)
+qed
+
+lemma (in ring) eval_append:
+  assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
+  shows "eval (p @ q) a = ((eval p a) \<otimes> (a [^] (length q))) \<oplus> (eval q a)"
+  using assms(2)
+proof (induct "length q" arbitrary: q)
+  case 0 thus ?case
+    using eval_in_carrier[OF assms(1,3)] by auto
+next
+  case (Suc n)
+  then obtain b q' where q: "q = q' @ [ b ]"
+    by (metis length_Suc_conv list.simps(3) rev_exhaust)
+  hence in_carrier: "eval p a \<in> carrier R" "eval q' a \<in> carrier R"
+                    "a [^] (length q') \<in> carrier R" "b \<in> carrier R"
+    using assms(1,3) Suc(3) eval_in_carrier[OF _ assms(3)] by auto
+
+  have "eval (p @ q) a = ((eval (p @ q') a) \<otimes> a) \<oplus> b"
+    using eval_append_aux[OF _ _ assms(3), of "p @ q'" b] assms(1) Suc(3) unfolding q by auto
+  also have " ... = ((((eval p a) \<otimes> (a [^] (length q'))) \<oplus> (eval q' a)) \<otimes> a) \<oplus> b"
+    using Suc unfolding q by auto
+  also have " ... = (((eval p a) \<otimes> ((a [^] (length q')) \<otimes> a))) \<oplus> (((eval q' a) \<otimes> a) \<oplus> b)"
+    using assms(3) in_carrier by algebra
+  also have " ... = (eval p a) \<otimes> (a [^] (length q)) \<oplus> (eval q a)"
+    using eval_append_aux[OF _ in_carrier(4) assms(3), of q'] Suc(3) unfolding q by auto
+  finally show ?case .
+qed
+
+lemma (in ring) eval_monon:
+  assumes "b \<in> carrier R" and "a \<in> carrier R"
+  shows "eval (monon b n) a = b \<otimes> (a [^] n)"
+proof (induct n)
+  case 0 thus ?case
+    using assms unfolding monon_def by (auto simp add: degree_def)
+next
+  case (Suc n)
+  have "monon b (Suc n) = (monon b n) @ [ \<zero> ]"
+    unfolding monon_def by (simp add: replicate_append_same)
+  hence "eval (monon b (Suc n)) a = ((eval (monon b n) a) \<otimes> a) \<oplus> \<zero>"
+    using eval_append_aux[OF monon_in_carrier[OF assms(1)] zero_closed assms(2), of n] by simp
+  also have " ... =  b \<otimes> (a [^] (Suc n))"
+    using Suc assms m_assoc by auto
+  finally show ?case .
+qed
+
+lemma (in cring) eval_poly_mult:
+  assumes "set p \<subseteq> carrier R" "set q \<subseteq> carrier R" and "a \<in> carrier R"
+  shows "eval (poly_mult p q) a = (eval p a) \<otimes> (eval q a)"
+  using assms(1)
+proof (induct p)
+  case Nil thus ?case
+    using eval_in_carrier[OF assms(2-3)] by simp
+next
+  { fix n b assume b: "b \<in> carrier R"
+    hence "set (map ((\<otimes>) b) q) \<subseteq> carrier R" and "set (replicate n \<zero>) \<subseteq> carrier R"
+      using assms(2) by (induct q) (auto)
+    hence "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval ((map ((\<otimes>) b) q)) a) \<otimes> (a [^] n) \<oplus> \<zero>"
+      using eval_append[OF _ _ assms(3), of "map ((\<otimes>) b) q" "replicate n \<zero>"] 
+            eval_replicate[OF _ assms(3), of "[]"] by auto
+    moreover have "eval (map ((\<otimes>) b) q) a = b \<otimes> eval q a"
+      using assms(2-3) eval_in_carrier b by(induct q) (auto simp add: degree_def m_assoc r_distr)
+    ultimately have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (b \<otimes> eval q a) \<otimes> (a [^] n) \<oplus> \<zero>"
+      by simp
+    also have " ... = (b \<otimes> (a [^] n)) \<otimes> (eval q a)"
+      using eval_in_carrier[OF assms(2-3)] b assms(3) m_assoc m_comm by auto
+    finally have "eval ((map ((\<otimes>) b) q) @ (replicate n \<zero>)) a = (eval (monon b n) a) \<otimes> (eval q a)"
+      using eval_monon[OF b assms(3)] by simp }
+  note aux_lemma = this
+
+  case (Cons b p)
+  hence in_carrier:
+    "eval (monon b (length p)) a \<in> carrier R" "eval p a \<in> carrier R" "eval q a \<in> carrier R" "b \<in> carrier R"
+    using eval_in_carrier monon_in_carrier assms by auto
+  have set_map: "set ((map ((\<otimes>) b) q) @ (replicate (length p) \<zero>)) \<subseteq> carrier R"
+    using in_carrier(4) assms(2) by (induct q) (auto)
+  have set_poly: "set (poly_mult p q) \<subseteq> carrier R"
+    using poly_mult_in_carrier[OF _ assms(2), of p] Cons(2) by auto
+  have "eval (poly_mult (b # p) q) a =
+      ((eval (monon b (length p)) a) \<otimes> (eval q a)) \<oplus> ((eval p a) \<otimes> (eval q a))"
+    using eval_poly_add[OF set_map set_poly assms(3)] aux_lemma[OF in_carrier(4), of "length p"] Cons
+    by (auto simp del: poly_add.simps simp add: degree_def)
+  also have " ... = ((eval (monon b (length p)) a) \<oplus> (eval p a)) \<otimes> (eval q a)"
+    using l_distr[OF in_carrier(1-3)] by simp
+  also have " ... = (eval (b # p) a) \<otimes> (eval q a)"
+    unfolding eval_monon[OF in_carrier(4) assms(3), of "length p"] by (auto simp add: degree_def)
+  finally show ?case .
+qed
+
+proposition (in cring) eval_is_hom:
+  assumes "subring K R" and "a \<in> carrier R"
+  shows "(\<lambda>p. (eval p) a) \<in> ring_hom (univ_poly (R \<lparr> carrier := K \<rparr>)) R"
+  unfolding univ_poly_carrier_change_def'[OF assms(1)]
+  using polynomial_in_carrier eval_in_carrier eval_poly_add eval_poly_mult assms(2)
+  by (auto intro!: ring_hom_memI
+         simp add: univ_poly_def degree_def
+         simp del: poly_add.simps poly_mult.simps)
+
+
+end
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/Ring_Divisibility.thy	Mon Jul 02 22:40:25 2018 +0100
@@ -0,0 +1,806 @@
+(* ************************************************************************** *)
+(* Title:      Ring_Divisibility.thy                                          *)
+(* Author:     Paulo Emílio de Vilhena                                        *)
+(* ************************************************************************** *)
+
+theory Ring_Divisibility
+imports Ideal Divisibility QuotRing
+
+begin
+
+section \<open>Definitions ported from Multiplicative_Group.thy\<close>
+
+definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
+  "mult_of R \<equiv> \<lparr> carrier = carrier R - { \<zero>\<^bsub>R\<^esub> }, mult = mult R, one = \<one>\<^bsub>R\<^esub> \<rparr>"
+
+lemma carrier_mult_of [simp]: "carrier (mult_of R) = carrier R - { \<zero>\<^bsub>R\<^esub> }"
+  by (simp add: mult_of_def)
+
+lemma mult_mult_of [simp]: "mult (mult_of R) = mult R"
+ by (simp add: mult_of_def)
+
+lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
+  by (simp add: mult_of_def fun_eq_iff nat_pow_def)
+
+lemma one_mult_of [simp]: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
+  by (simp add: mult_of_def)
+
+lemmas mult_of_simps = carrier_mult_of mult_mult_of nat_pow_mult_of one_mult_of
+
+
+section \<open>The Arithmetic of Rings\<close>
+
+text \<open>In this section we study the links between the divisibility theory and that of rings\<close>
+
+
+subsection \<open>Definitions\<close>
+
+locale factorial_domain = domain + factorial_monoid "mult_of R"
+
+locale noetherian_ring = ring +
+  assumes finetely_gen: "ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+
+locale noetherian_domain = noetherian_ring + domain
+
+locale principal_domain = domain +
+  assumes principal_I: "ideal I R \<Longrightarrow> principalideal I R"
+
+locale euclidean_domain = R?: domain R for R (structure) + fixes \<phi> :: "'a \<Rightarrow> nat"
+  assumes euclidean_function:
+  " \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+   \<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
+
+lemma (in domain) mult_of_is_comm_monoid: "comm_monoid (mult_of R)"
+  apply (rule comm_monoidI)
+  apply (auto simp add: integral_iff m_assoc)
+  apply (simp add: m_comm)
+  done
+
+lemma (in domain) cancel_property: "comm_monoid_cancel (mult_of R)"
+  by (rule comm_monoid_cancelI) (auto simp add: mult_of_is_comm_monoid m_rcancel)
+
+sublocale domain < mult_of: comm_monoid_cancel "(mult_of R)"
+  rewrites "mult (mult_of R) = mult R"
+       and "one  (mult_of R) = one R"
+  using cancel_property by auto
+
+sublocale noetherian_domain \<subseteq> domain ..
+
+sublocale principal_domain \<subseteq> domain ..
+
+sublocale euclidean_domain \<subseteq> domain ..
+
+lemma (in factorial_monoid) is_factorial_monoid: "factorial_monoid G" ..
+
+sublocale factorial_domain < mult_of: factorial_monoid "mult_of R"
+  rewrites "mult (mult_of R) = mult R"
+       and "one  (mult_of R) = one R"
+  using factorial_monoid_axioms by auto
+
+lemma (in domain) factorial_domainI:
+  assumes "\<And>a. a \<in> carrier (mult_of R) \<Longrightarrow>
+               \<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs a"
+      and "\<And>a fs fs'. \<lbrakk> a \<in> carrier (mult_of R);
+                        set fs \<subseteq> carrier (mult_of R);
+                        set fs' \<subseteq> carrier (mult_of R);
+                        wfactors (mult_of R) fs a;
+                        wfactors (mult_of R) fs' a \<rbrakk> \<Longrightarrow>
+                        essentially_equal (mult_of R) fs fs'"
+    shows "factorial_domain R"
+  unfolding factorial_domain_def using mult_of.factorial_monoidI assms domain_axioms by auto
+
+lemma (in domain) is_domain: "domain R" ..
+
+lemma (in ring) noetherian_ringI:
+  assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+  shows "noetherian_ring R"
+  unfolding noetherian_ring_def noetherian_ring_axioms_def using assms is_ring by simp
+
+lemma (in domain) noetherian_domainI:
+  assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> I = Idl A"
+  shows "noetherian_domain R"
+  unfolding noetherian_domain_def noetherian_ring_def noetherian_ring_axioms_def
+  using assms is_ring is_domain by simp
+
+lemma (in domain) principal_domainI:
+  assumes "\<And>I. ideal I R \<Longrightarrow> principalideal I R"
+  shows "principal_domain R"
+  unfolding principal_domain_def principal_domain_axioms_def using is_domain assms by auto
+
+lemma (in domain) principal_domainI2:
+  assumes "\<And>I. ideal I R \<Longrightarrow> \<exists>a \<in> carrier R. I = PIdl a"
+  shows "principal_domain R"
+  unfolding principal_domain_def principal_domain_axioms_def
+  using is_domain assms principalidealI cgenideal_eq_genideal by auto
+
+lemma (in domain) euclidean_domainI:
+  assumes "\<And>a b. \<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+           \<exists>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = (b \<otimes> q) \<oplus> r \<and> ((r = \<zero>) \<or> (\<phi> r < \<phi> b))"
+  shows "euclidean_domain R \<phi>"
+  using assms by unfold_locales auto
+
+
+subsection \<open>Basic Properties\<close>
+
+text \<open>Links between domains and commutative cancellative monoids\<close>
+
+lemma (in cring) to_contain_is_to_divide:
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "(PIdl b \<subseteq> PIdl a) = (a divides b)"
+proof 
+  show "PIdl b \<subseteq> PIdl a \<Longrightarrow> a divides b"
+  proof -
+    assume "PIdl b \<subseteq> PIdl a"
+    hence "b \<in> PIdl a"
+      by (meson assms(2) local.ring_axioms ring.cgenideal_self subsetCE)
+    thus ?thesis
+      unfolding factor_def cgenideal_def using m_comm assms(1) by blast  
+  qed
+  show "a divides b \<Longrightarrow> PIdl b \<subseteq> PIdl a"
+  proof -
+    assume "a divides b" then obtain c where c: "c \<in> carrier R" "b = c \<otimes> a"
+      unfolding factor_def using m_comm[OF assms(1)] by blast
+    show "PIdl b \<subseteq> PIdl a"
+    proof
+      fix x assume "x \<in> PIdl b"
+      then obtain d where d: "d \<in> carrier R" "x = d \<otimes> b"
+        unfolding cgenideal_def by blast
+      hence "x = (d \<otimes> c) \<otimes> a"
+        using c d m_assoc assms by simp
+      thus "x \<in> PIdl a"
+        unfolding cgenideal_def using m_assoc assms c d by blast
+    qed
+  qed
+qed
+
+lemma (in cring) associated_iff_same_ideal:
+  assumes "a \<in> carrier R" "b \<in> carrier R"
+  shows "(a \<sim> b) = (PIdl a = PIdl b)"
+  unfolding associated_def
+  using to_contain_is_to_divide[OF assms]
+        to_contain_is_to_divide[OF assms(2) assms(1)] by auto
+
+lemma divides_mult_imp_divides [simp]: "a divides\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a divides\<^bsub>R\<^esub> b"
+  unfolding factor_def by auto
+
+lemma (in domain) divides_imp_divides_mult [simp]:
+  "\<lbrakk> a \<in> carrier R; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+     a divides\<^bsub>R\<^esub> b \<Longrightarrow> a divides\<^bsub>(mult_of R)\<^esub> b"
+  unfolding factor_def using integral_iff by auto 
+
+lemma assoc_mult_imp_assoc [simp]: "a \<sim>\<^bsub>(mult_of R)\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>R\<^esub> b"
+  unfolding associated_def by simp
+
+lemma (in domain) assoc_imp_assoc_mult [simp]:
+  "\<lbrakk> a \<in> carrier R - { \<zero> } ; b \<in> carrier R - { \<zero> } \<rbrakk> \<Longrightarrow>
+     a \<sim>\<^bsub>R\<^esub> b \<Longrightarrow> a \<sim>\<^bsub>(mult_of R)\<^esub> b"
+  unfolding associated_def by simp
+
+lemma (in domain) Units_mult_eq_Units [simp]: "Units (mult_of R) = Units R"
+  unfolding Units_def using insert_Diff integral_iff by auto
+
+lemma (in domain) properfactor_mult_imp_properfactor:
+  "\<lbrakk> a \<in> carrier R; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor (mult_of R) b a \<Longrightarrow> properfactor R b a"
+proof -
+  assume A: "a \<in> carrier R" "b \<in> carrier R" "properfactor (mult_of R) b a"
+  then obtain c where c: "c \<in> carrier (mult_of R)" "a = b \<otimes> c"
+    unfolding properfactor_def factor_def by auto
+  have "a \<noteq> \<zero>"
+  proof (rule ccontr)
+    assume a: "\<not> a \<noteq> \<zero>"
+    hence "b = \<zero>" using c A integral[of b c] by auto
+    hence "b = a \<otimes> \<one>" using a A by simp
+    hence "a divides\<^bsub>(mult_of R)\<^esub> b"
+      unfolding factor_def by auto
+    thus False using A unfolding properfactor_def by simp
+  qed
+  hence "b \<noteq> \<zero>"
+    using c A integral_iff by auto
+  thus "properfactor R b a"
+    using A divides_imp_divides_mult[of a b] unfolding properfactor_def
+    by (meson DiffI divides_mult_imp_divides empty_iff insert_iff) 
+qed
+
+lemma (in domain) properfactor_imp_properfactor_mult:
+  "\<lbrakk> a \<in> carrier R - { \<zero> }; b \<in> carrier R \<rbrakk> \<Longrightarrow> properfactor R b a \<Longrightarrow> properfactor (mult_of R) b a"
+  unfolding properfactor_def factor_def by auto
+
+lemma (in domain) primeideal_iff_prime:
+  assumes "p \<in> carrier (mult_of R)"
+  shows "(primeideal (PIdl p) R) = (prime (mult_of R) p)"
+proof
+  show "prime (mult_of R) p \<Longrightarrow> primeideal (PIdl p) R"
+  proof (rule primeidealI)
+    assume A: "prime (mult_of R) p"
+    show "ideal (PIdl p) R" and "cring R"
+      using assms is_cring by (auto simp add: cgenideal_ideal)
+    show "carrier R \<noteq> PIdl p"
+    proof (rule ccontr)
+      assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp
+      then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>"
+        unfolding cgenideal_def using one_closed by (smt mem_Collect_eq)
+      hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto
+      thus False using A unfolding prime_def by simp
+    qed
+    fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> PIdl p"
+    thus "a \<in> PIdl p \<or> b \<in> PIdl p"
+    proof (cases "a = \<zero> \<or> b = \<zero>")
+      case True thus "a \<in> PIdl p \<or> b \<in> PIdl p" using ab a b by auto
+    next
+      { fix a assume "a \<in> carrier R" "p divides\<^bsub>mult_of R\<^esub> a"
+        then obtain c where "c \<in> carrier R" "a = p \<otimes> c"
+          unfolding factor_def by auto
+        hence "a \<in> PIdl p" unfolding cgenideal_def using assms m_comm by auto }
+      note aux_lemma = this
+
+      case False hence "a \<noteq> \<zero> \<and> b \<noteq> \<zero>" by simp
+      hence diff_zero: "a \<otimes> b \<noteq> \<zero>" using a b integral by blast
+      then obtain c where c: "c \<in> carrier R" "a \<otimes> b = p \<otimes> c"
+        using assms ab m_comm unfolding cgenideal_def by auto
+      hence "c \<noteq> \<zero>" using c assms diff_zero by auto
+      hence "p divides\<^bsub>(mult_of R)\<^esub> (a \<otimes> b)"
+        unfolding factor_def using ab c by auto
+      hence "p divides\<^bsub>(mult_of R)\<^esub> a \<or> p divides\<^bsub>(mult_of R)\<^esub> b"
+        using A a b False unfolding prime_def by auto
+      thus "a \<in> PIdl p \<or> b \<in> PIdl p" using a b aux_lemma by blast
+    qed
+  qed
+next
+  show "primeideal (PIdl p) R \<Longrightarrow> prime (mult_of R) p"
+  proof -
+    assume A: "primeideal (PIdl p) R" show "prime (mult_of R) p"
+    proof (rule primeI)
+      show "p \<notin> Units (mult_of R)"
+      proof (rule ccontr)
+        assume "\<not> p \<notin> Units (mult_of R)"
+        hence p: "p \<in> Units (mult_of R)" by simp
+        then obtain q where q: "q \<in> carrier R - { \<zero> }" "p \<otimes> q = \<one>" "q \<otimes> p = \<one>"
+          unfolding Units_def apply simp by blast
+        have "PIdl p = carrier R"
+        proof
+          show "PIdl p \<subseteq> carrier R"
+            by (simp add: assms A additive_subgroup.a_subset ideal.axioms(1) primeideal.axioms(1))
+        next
+          show "carrier R \<subseteq> PIdl p"
+          proof
+            fix r assume r: "r \<in> carrier R" hence "r = (r \<otimes> q) \<otimes> p"
+              using p q m_assoc unfolding Units_def by simp
+            thus "r \<in> PIdl p" unfolding cgenideal_def using q r m_closed by blast
+          qed
+        qed
+        moreover have "PIdl p \<noteq> carrier R" using A primeideal.I_notcarr by auto
+        ultimately show False by simp 
+      qed
+    next
+      { fix a assume "a \<in> PIdl p" and a: "a \<noteq> \<zero>"
+        then obtain c where c: "c \<in> carrier R" "a = p \<otimes> c"
+          unfolding cgenideal_def using m_comm assms by auto
+        hence "c \<noteq> \<zero>" using assms a by auto
+        hence "p divides\<^bsub>mult_of R\<^esub> a" unfolding factor_def using c by auto }
+      note aux_lemma = this
+
+      fix a b
+      assume a: "a \<in> carrier (mult_of R)" and b: "b \<in> carrier (mult_of R)"
+         and p: "p divides\<^bsub>mult_of R\<^esub> a \<otimes>\<^bsub>mult_of R\<^esub> b"
+      then obtain c where "c \<in> carrier R" "a \<otimes> b = c \<otimes> p"
+        unfolding factor_def using m_comm assms by auto
+      hence "a \<otimes> b \<in> PIdl p" unfolding cgenideal_def by blast
+      hence "a \<in> PIdl p \<or> b \<in> PIdl p" using A primeideal.I_prime[OF A] a b by auto
+      thus "p divides\<^bsub>mult_of R\<^esub> a \<or> p divides\<^bsub>mult_of R\<^esub> b"
+        using a b aux_lemma by auto
+    qed
+  qed
+qed
+
+
+subsection \<open>Noetherian Rings\<close>
+
+lemma (in noetherian_ring) trivial_ideal_seq:
+  assumes "\<And>i :: nat. ideal (I i) R"
+    and "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+  shows "\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n"
+proof -
+  have "ideal (\<Union>i. I i) R"
+  proof
+    show "(\<Union>i. I i) \<subseteq> carrier (add_monoid R)"
+      using additive_subgroup.a_subset assms(1) ideal.axioms(1) by fastforce
+    have "\<one>\<^bsub>add_monoid R\<^esub> \<in> I 0"
+      by (simp add: additive_subgroup.zero_closed assms(1) ideal.axioms(1))
+    thus "\<one>\<^bsub>add_monoid R\<^esub> \<in> (\<Union>i. I i)" by blast
+  next
+    fix x y assume x: "x \<in> (\<Union>i. I i)" and y: "y \<in> (\<Union>i. I i)"
+    then obtain i j where i: "x \<in> I i" and j: "y \<in> I j" by blast
+    hence "inv\<^bsub>add_monoid R\<^esub> x \<in> I i"
+      by (simp add: additive_subgroup.a_subgroup assms(1) ideal.axioms(1) subgroup.m_inv_closed)
+    thus "inv\<^bsub>add_monoid R\<^esub> x \<in> (\<Union>i. I i)" by blast
+    have "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> I (max i j)"
+      by (metis add.subgroupE(4) additive_subgroup.a_subgroup assms(1-2) i j ideal.axioms(1)
+          max.cobounded1 max.cobounded2 monoid.select_convs(1) rev_subsetD)
+    thus "x \<otimes>\<^bsub>add_monoid R\<^esub> y \<in> (\<Union>i. I i)" by blast
+  next
+    fix x a assume x: "x \<in> carrier R" and a: "a \<in> (\<Union>i. I i)"
+    then obtain i where i: "a \<in> I i" by blast
+    hence "x \<otimes> a \<in> I i" and "a \<otimes> x \<in> I i"
+      by (simp_all add: assms(1) ideal.I_l_closed ideal.I_r_closed x)
+    thus "x \<otimes> a \<in> (\<Union>i. I i)"
+     and "a \<otimes> x \<in> (\<Union>i. I i)" by blast+
+  qed
+
+  then obtain S where S: "S \<subseteq> carrier R" "finite S" "(\<Union>i. I i) = Idl S"
+    by (meson finetely_gen)
+  hence "S \<subseteq> (\<Union>i. I i)"
+    by (simp add: genideal_self)
+
+  from \<open>finite S\<close> and \<open>S \<subseteq> (\<Union>i. I i)\<close> have "\<exists>n. S \<subseteq> I n"
+  proof (induct S set: "finite")
+    case empty thus ?case by simp 
+  next
+    case (insert x S')
+    then obtain n m where m: "S' \<subseteq> I m" and n: "x \<in> I n" by blast
+    hence "insert x S' \<subseteq> I (max m n)"
+      by (meson assms(2) insert_subsetI max.cobounded1 max.cobounded2 rev_subsetD subset_trans) 
+    thus ?case by blast
+  qed
+  then obtain n where "S \<subseteq> I n" by blast
+  hence "I n = (\<Union>i. I i)"
+    by (metis S(3) Sup_upper assms(1) genideal_minimal range_eqI subset_antisym)
+  thus ?thesis
+    by (metis (full_types) Sup_upper assms(2) range_eqI subset_antisym)
+qed
+
+lemma increasing_set_seq_iff:
+  "(\<And>i. I i \<subseteq> I (Suc i)) == (\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j)"
+proof
+  fix i j :: "nat"
+  assume A: "\<And>i. I i \<subseteq> I (Suc i)" and "i \<le> j"
+  then obtain k where k: "j = i + k"
+    using le_Suc_ex by blast
+  have "I i \<subseteq> I (i + k)"
+    by (induction k) (simp_all add: A lift_Suc_mono_le)
+  thus "I i \<subseteq> I j" using k by simp
+next
+  fix i assume "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+  thus "I i \<subseteq> I (Suc i)" by simp
+qed
+
+
+text \<open>Helper definition for the lemma: trivial_ideal_seq_imp_noetherian\<close>
+fun S_builder :: "_ \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set" where
+  "S_builder R J 0 = {}" |
+  "S_builder R J (Suc n) =
+     (let diff = (J - Idl\<^bsub>R\<^esub> (S_builder R J n)) in
+        (if diff \<noteq> {} then insert (SOME x. x \<in> diff) (S_builder R J n) else (S_builder R J n)))"
+
+lemma S_builder_incl: "S_builder R J n \<subseteq> J"
+  by (induction n) (simp_all, (metis (no_types, lifting) some_eq_ex subsetI))
+
+lemma (in ring) S_builder_const1:
+  assumes "ideal J R" "S_builder R J (Suc n) = S_builder R J n"
+  shows "J = Idl (S_builder R J n)"
+proof -
+  have "J - Idl (S_builder R J n) = {}"
+  proof (rule ccontr)
+    assume "J - Idl (S_builder R J n) \<noteq> {}"
+    hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)"
+      by simp
+    moreover have "(S_builder R J n) \<subseteq> Idl (S_builder R J n)"
+      using S_builder_incl assms(1)
+      by (metis additive_subgroup.a_subset dual_order.trans genideal_self ideal.axioms(1))
+    ultimately have "S_builder R J (Suc n) \<noteq> S_builder R J n"
+      by (metis Diff_iff \<open>J - Idl S_builder R J n \<noteq> {}\<close> insert_subset some_in_eq)
+    thus False using assms(2) by simp
+  qed
+  thus "J = Idl (S_builder R J n)"
+    by (meson S_builder_incl[of R J n] Diff_eq_empty_iff assms(1) genideal_minimal subset_antisym)
+qed
+
+lemma (in ring) S_builder_const2:
+  assumes "ideal J R" "Idl (S_builder R J (Suc n)) = Idl (S_builder R J n)"
+  shows "S_builder R J (Suc n) = S_builder R J n"
+proof (rule ccontr)
+  assume "S_builder R J (Suc n) \<noteq> S_builder R J n"
+  hence A: "J - Idl (S_builder R J n) \<noteq> {}" by auto
+  hence "S_builder R J (Suc n) = insert (SOME x. x \<in> (J - Idl (S_builder R J n))) (S_builder R J n)" by simp
+  then obtain x where x: "x \<in> (J - Idl (S_builder R J n))"
+                  and S: "S_builder R J (Suc n) = insert x (S_builder R J n)"
+    using A some_in_eq by blast
+  have "x \<notin> Idl (S_builder R J n)" using x by blast
+  moreover have "x \<in> Idl (S_builder R J (Suc n))"
+    by (metis (full_types) S S_builder_incl additive_subgroup.a_subset
+        assms(1) dual_order.trans genideal_self ideal.axioms(1) insert_subset)
+  ultimately show False using assms(2) by blast
+qed
+
+lemma (in ring) trivial_ideal_seq_imp_noetherian:
+  assumes "\<And>I. \<lbrakk> \<And>i :: nat. ideal (I i) R; \<And>i j. i \<le> j \<Longrightarrow> (I i) \<subseteq> (I j) \<rbrakk> \<Longrightarrow>
+                 (\<exists>n. \<forall>k. k \<ge> n \<longrightarrow> I k = I n)"
+  shows "noetherian_ring R"
+proof -
+  have "\<And>J. ideal J R \<Longrightarrow> \<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
+  proof -
+    fix J assume J: "ideal J R"
+    define S and I where "S = (\<lambda>i. S_builder R J i)" and "I = (\<lambda>i. Idl (S i))"
+    hence "\<And>i. ideal (I i) R"
+      by (meson J S_builder_incl additive_subgroup.a_subset genideal_ideal ideal.axioms(1) subset_trans)
+    moreover have "\<And>n. S n \<subseteq> S (Suc n)" using S_def by auto
+    hence "\<And>n. I n \<subseteq> I (Suc n)"
+      using S_builder_incl[of R J] J S_def I_def
+      by (meson additive_subgroup.a_subset dual_order.trans ideal.axioms(1) subset_Idl_subset)
+    ultimately obtain n where "\<And>k. k \<ge> n \<Longrightarrow> I k = I n"
+      using assms increasing_set_seq_iff[of I] by (metis lift_Suc_mono_le) 
+    hence "J = Idl (S_builder R J n)"
+      using S_builder_const1[OF J, of n] S_builder_const2[OF J, of n] I_def S_def
+      by (meson Suc_n_not_le_n le_cases)
+    moreover have "finite (S_builder R J n)" by (induction n) (simp_all)
+    ultimately show "\<exists>A. A \<subseteq> carrier R \<and> finite A \<and> J = Idl A"
+      by (meson J S_builder_incl ideal.Icarr set_rev_mp subsetI)
+  qed
+  thus ?thesis
+    by (simp add: local.ring_axioms noetherian_ring_axioms_def noetherian_ring_def) 
+qed
+
+lemma (in noetherian_domain) wfactors_exists:
+  assumes "x \<in> carrier (mult_of R)"
+  shows "\<exists>fs. set fs \<subseteq> carrier (mult_of R) \<and> wfactors (mult_of R) fs x" (is "?P x")
+proof (rule ccontr)
+  { fix x
+    assume A: "x \<in> carrier (mult_of R)" "\<not> ?P x"
+    have "\<exists>a. a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a"
+    proof -
+      have "\<not> irreducible (mult_of R) x"
+      proof (rule ccontr)
+        assume "\<not> (\<not> irreducible (mult_of R) x)" hence "irreducible (mult_of R) x" by simp
+        hence "wfactors (mult_of R) [ x ] x" unfolding wfactors_def using A by auto 
+        thus False using A by auto
+      qed
+      moreover have  "\<not> x \<in> Units (mult_of R)"
+        using A monoid.unit_wfactors[OF mult_of.monoid_axioms, of x] by auto
+      ultimately
+      obtain a where a: "a \<in> carrier (mult_of R)" "properfactor (mult_of R) a x" "a \<notin> Units (mult_of R)"
+        unfolding irreducible_def by blast
+      then obtain b where b: "b \<in> carrier (mult_of R)" "x = a \<otimes> b"
+        unfolding properfactor_def by auto
+      hence b_properfactor: "properfactor (mult_of R) b x"
+        using A a mult_of.m_comm mult_of.properfactorI3 by blast
+      have "\<not> ?P a \<or> \<not> ?P b"
+      proof (rule ccontr)
+        assume "\<not> (\<not> ?P a \<or> \<not> ?P b)"
+        then obtain fs_a fs_b
+          where fs_a: "wfactors (mult_of R) fs_a a" "set fs_a \<subseteq> carrier (mult_of R)"
+            and fs_b: "wfactors (mult_of R) fs_b b" "set fs_b \<subseteq> carrier (mult_of R)" by blast
+        hence "wfactors (mult_of R) (fs_a @ fs_b) x"
+          using fs_a fs_b a b mult_of.wfactors_mult by simp
+        moreover have "set (fs_a @ fs_b) \<subseteq> carrier (mult_of R)"
+          using fs_a fs_b by auto
+        ultimately show False using A by blast 
+      qed
+      thus ?thesis using a b b_properfactor mult_of.m_comm by blast
+    qed } note aux_lemma = this
+  
+  assume A: "\<not> ?P x"
+
+  define f :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+    where "f = (\<lambda>a x. (a \<in> carrier (mult_of R) \<and> properfactor (mult_of R) a x \<and> \<not> ?P a))"
+  define factor_seq :: "nat \<Rightarrow> 'a"
+    where "factor_seq = rec_nat x (\<lambda>n y. (SOME a. f a y))"
+  define I where "I = (\<lambda>i. PIdl (factor_seq i))"
+  have factor_seq_props:
+    "\<And>n. properfactor (mult_of R) (factor_seq (Suc n)) (factor_seq n) \<and> 
+         (factor_seq n) \<in> carrier (mult_of R) \<and> \<not> ?P (factor_seq n)" (is "\<And>n. ?Q n")
+  proof -
+    fix n show "?Q n"
+    proof (induct n)
+      case 0
+      have x: "factor_seq 0 = x"
+        using factor_seq_def by simp
+      hence "factor_seq (Suc 0) = (SOME a. f a x)"
+        by (simp add: factor_seq_def)
+      moreover have "\<exists>a. f a x"
+        using aux_lemma[OF assms] A f_def by blast
+      ultimately have "f (factor_seq (Suc 0)) x"
+        using tfl_some by metis
+      thus ?case using f_def A assms x by simp
+    next
+      case (Suc n)
+      have "factor_seq (Suc n) = (SOME a. f a (factor_seq n))"
+        by (simp add: factor_seq_def)
+      moreover have "\<exists>a. f a (factor_seq n)"
+        using aux_lemma f_def Suc.hyps by blast
+      ultimately have Step0: "f (factor_seq (Suc n)) (factor_seq n)"
+        using tfl_some by metis
+      hence "\<exists>a. f a (factor_seq (Suc n))"
+        using aux_lemma f_def by blast
+      moreover have "factor_seq (Suc (Suc n)) = (SOME a. f a (factor_seq (Suc n)))"
+        by (simp add: factor_seq_def)
+      ultimately have Step1: "f (factor_seq (Suc (Suc n))) (factor_seq (Suc n))"
+        using tfl_some by metis
+      show ?case using Step0 Step1 f_def by simp
+    qed
+  qed
+
+  have in_carrier: "\<And>i. factor_seq i \<in> carrier R"
+    using factor_seq_props by simp 
+  hence "\<And>i. ideal (I i) R"
+    using I_def by (simp add: cgenideal_ideal)
+
+  moreover
+  have "\<And>i. factor_seq (Suc i) divides factor_seq i"
+    using factor_seq_props unfolding properfactor_def by auto
+  hence "\<And>i. PIdl (factor_seq i) \<subseteq> PIdl (factor_seq (Suc i))"
+    using in_carrier to_contain_is_to_divide by simp
+  hence "\<And>i j. i \<le> j \<Longrightarrow> I i \<subseteq> I j"
+    using increasing_set_seq_iff[of I] unfolding I_def by auto
+
+  ultimately obtain n where "\<And>k. n \<le> k \<Longrightarrow> I n = I k"
+    by (metis trivial_ideal_seq)
+  hence "I (Suc n) \<subseteq> I n" by (simp add: equalityD2)
+  hence "factor_seq n divides factor_seq (Suc n)"
+    using in_carrier I_def to_contain_is_to_divide by simp
+  moreover have "\<not> factor_seq n divides\<^bsub>(mult_of R)\<^esub> factor_seq (Suc n)"
+    using factor_seq_props[of n] unfolding properfactor_def by simp
+  hence "\<not> factor_seq n divides factor_seq (Suc n)"
+    using divides_imp_divides_mult[of "factor_seq n" "factor_seq (Suc n)"]
+          in_carrier[of n] factor_seq_props[of "Suc n"] by auto
+  ultimately show False by simp
+qed
+
+
+subsection \<open>Principal Domains\<close>
+
+sublocale principal_domain \<subseteq> noetherian_domain
+proof
+  fix I assume "ideal I R"
+  then obtain i where "i \<in> carrier R" "I = Idl { i }"
+    using principal_I principalideal.generate by blast
+  thus "\<exists>A \<subseteq> carrier R. finite A \<and> I = Idl A" by blast
+qed
+
+lemma (in principal_domain) irreducible_imp_maximalideal:
+  assumes "p \<in> carrier (mult_of R)"
+    and "irreducible (mult_of R) p"
+  shows "maximalideal (PIdl p) R"
+proof (rule maximalidealI)
+  show "ideal (PIdl p) R"
+    using assms(1) by (simp add: cgenideal_ideal)
+next
+  show "carrier R \<noteq> PIdl p"
+  proof (rule ccontr)
+    assume "\<not> carrier R \<noteq> PIdl p"
+    hence "carrier R = PIdl p" by simp
+    then obtain c where "c \<in> carrier R" "\<one> = c \<otimes> p"
+      unfolding cgenideal_def using one_closed by auto
+    hence "p \<in> Units R"
+      unfolding Units_def using assms(1) m_comm by auto
+    thus False
+      using assms unfolding irreducible_def by auto
+  qed
+next
+  fix J assume J: "ideal J R" "PIdl p \<subseteq> J" "J \<subseteq> carrier R"
+  then obtain q where q: "q \<in> carrier R" "J = PIdl q"
+    using principal_I[OF J(1)] cgenideal_eq_rcos is_cring
+          principalideal.rcos_generate by (metis contra_subsetD)
+  hence "q divides p"
+    using to_contain_is_to_divide[of q p] using assms(1) J(1-2) by simp
+  hence q_div_p: "q divides\<^bsub>(mult_of R)\<^esub> p"
+    using assms(1) divides_imp_divides_mult[OF q(1), of p] by (simp add: \<open>q divides p\<close>) 
+  show "J = PIdl p \<or> J = carrier R"
+  proof (cases "q \<in> Units R")
+    case True thus ?thesis
+      by (metis J(1) Units_r_inv_ex cgenideal_self ideal.I_r_closed ideal.one_imp_carrier q(1) q(2))
+  next
+    case False
+    have q_in_carr: "q \<in> carrier (mult_of R)"
+      using q_div_p unfolding factor_def using assms(1) q(1) by auto
+    hence "p divides\<^bsub>(mult_of R)\<^esub> q"
+      using q_div_p False assms(2) unfolding irreducible_def properfactor_def by auto
+    hence "p \<sim> q" using q_div_p
+      unfolding associated_def by simp
+    thus ?thesis using associated_iff_same_ideal[of p q] assms(1) q_in_carr q by simp
+  qed
+qed
+
+corollary (in principal_domain) primeness_condition:
+  assumes "p \<in> carrier (mult_of R)"
+  shows "(irreducible (mult_of R) p) \<longleftrightarrow> (prime (mult_of R) p)"
+proof
+  show "irreducible (mult_of R) p \<Longrightarrow> prime (mult_of R) p"
+    using irreducible_imp_maximalideal maximalideal_prime primeideal_iff_prime assms by auto
+next
+  show "prime (mult_of R) p \<Longrightarrow> irreducible (mult_of R) p"
+    using mult_of.prime_irreducible by simp
+qed
+
+lemma (in principal_domain) domain_iff_prime:
+  assumes "a \<in> carrier R - { \<zero> }"
+  shows "domain (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+  using quot_domain_iff_primeideal[of "PIdl a"] primeideal_iff_prime[of a]
+        cgenideal_ideal[of a] assms by auto
+
+lemma (in principal_domain) field_iff_prime:
+  assumes "a \<in> carrier R - { \<zero> }"
+  shows "field (R Quot (PIdl a)) \<longleftrightarrow> prime (mult_of R) a"
+proof
+  show "prime (mult_of R) a \<Longrightarrow> field  (R Quot (PIdl a))"
+    using  primeness_condition[of a] irreducible_imp_maximalideal[of a]
+           maximalideal.quotient_is_field[of "PIdl a" R] is_cring assms by auto
+next
+  show "field  (R Quot (PIdl a)) \<Longrightarrow> prime (mult_of R) a"
+    unfolding field_def using domain_iff_prime[of a] assms by auto
+qed
+
+sublocale principal_domain < mult_of: primeness_condition_monoid "(mult_of R)"
+  rewrites "mult (mult_of R) = mult R"
+       and "one  (mult_of R) = one R"
+  unfolding primeness_condition_monoid_def
+            primeness_condition_monoid_axioms_def
+  using mult_of.is_comm_monoid_cancel primeness_condition by auto
+
+sublocale principal_domain < mult_of: factorial_monoid "(mult_of R)"
+  rewrites "mult (mult_of R) = mult R"
+       and "one  (mult_of R) = one R"
+  apply (rule mult_of.factorial_monoidI)
+  using mult_of.wfactors_unique wfactors_exists mult_of.is_comm_monoid_cancel by auto
+
+sublocale principal_domain \<subseteq> factorial_domain
+  unfolding factorial_domain_def using is_domain mult_of.is_factorial_monoid by simp
+
+lemma (in principal_domain) ideal_sum_iff_gcd:
+  assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)" "d \<in> carrier (mult_of R)"
+  shows "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)) \<longleftrightarrow> (d gcdof\<^bsub>(mult_of R)\<^esub> a b)"
+proof
+  assume A: "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl d)" show "d gcdof\<^bsub>(mult_of R)\<^esub> a b"
+  proof -
+    have "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
+    using assms
+      by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal local.ring_axioms
+          ring.genideal_self ring.oneideal ring.union_genideal A)
+    hence "d divides a \<and> d divides b"
+      using assms apply simp
+      using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] by auto
+    hence "d divides\<^bsub>(mult_of R)\<^esub> a \<and> d divides\<^bsub>(mult_of R)\<^esub> b"
+      using assms by simp
+
+    moreover
+    have "\<And>c. \<lbrakk> c \<in> carrier (mult_of R); c divides\<^bsub>(mult_of R)\<^esub> a; c divides\<^bsub>(mult_of R)\<^esub> b \<rbrakk> \<Longrightarrow>
+                c divides\<^bsub>(mult_of R)\<^esub> d"
+    proof -
+      fix c assume c: "c \<in> carrier (mult_of R)"
+               and "c divides\<^bsub>(mult_of R)\<^esub> a" "c divides\<^bsub>(mult_of R)\<^esub> b"
+      hence "c divides a" "c divides b" by auto
+      hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)"
+        using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] c assms by simp
+      hence "((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) \<subseteq> (PIdl c)"
+        using assms c
+        by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+                        Idl_subset_ideal oneideal union_genideal)
+      hence incl: "(PIdl d) \<subseteq> (PIdl c)" using A by simp
+      hence "c divides d"
+        using c assms(3) apply simp
+        using to_contain_is_to_divide[of c d] by blast
+      thus "c divides\<^bsub>(mult_of R)\<^esub> d" using c assms(3) by simp
+    qed
+
+    ultimately show ?thesis unfolding isgcd_def by simp
+  qed
+next
+  assume A:"d gcdof\<^bsub>mult_of R\<^esub> a b" show "PIdl a <+>\<^bsub>R\<^esub> PIdl b = PIdl d"
+  proof
+    have "d divides a" "d divides b"
+      using A unfolding isgcd_def by auto
+    hence "(PIdl a) \<subseteq> (PIdl d) \<and> (PIdl b) \<subseteq> (PIdl d)"
+      using to_contain_is_to_divide[of d a] to_contain_is_to_divide[of d b] assms by simp
+    thus "PIdl a <+>\<^bsub>R\<^esub> PIdl b \<subseteq> PIdl d" using assms
+      by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+                      Idl_subset_ideal oneideal union_genideal)
+  next
+    have "ideal ((PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)) R"
+      using assms by (simp add: cgenideal_ideal local.ring_axioms ring.add_ideals)
+    then obtain c where c: "c \<in> carrier R" "(PIdl c) = (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
+      using cgenideal_eq_genideal principal_I principalideal.generate by force
+    hence "(PIdl a) \<subseteq> (PIdl c) \<and> (PIdl b) \<subseteq> (PIdl c)" using assms
+      by (simp, metis Un_subset_iff cgenideal_ideal cgenideal_minimal
+                      genideal_self oneideal union_genideal)
+    hence "c divides a \<and> c divides b" using c(1) assms apply simp
+      using to_contain_is_to_divide[of c a] to_contain_is_to_divide[of c b] by blast
+    hence "c divides\<^bsub>(mult_of R)\<^esub> a \<and> c divides\<^bsub>(mult_of R)\<^esub> b"
+      using assms(1-2) c(1) by simp
+
+    moreover have neq_zero: "c \<noteq> \<zero>"
+    proof (rule ccontr)
+      assume "\<not> c \<noteq> \<zero>" hence "PIdl c = { \<zero> }"
+        using cgenideal_eq_genideal genideal_zero by auto
+      moreover have "\<one> \<otimes> a \<in> PIdl a \<and> \<zero> \<otimes> b \<in> PIdl b"
+        unfolding cgenideal_def using assms one_closed zero_closed by blast
+      hence "(\<one> \<otimes> a) \<oplus> (\<zero> \<otimes> b) \<in> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b)"
+        unfolding set_add_def' by auto
+      hence "a \<in> PIdl c"
+        using c assms by simp
+      ultimately show False
+        using assms(1) by simp
+    qed
+
+    ultimately have "c divides\<^bsub>(mult_of R)\<^esub> d"
+      using A c(1) unfolding isgcd_def by simp
+    hence "(PIdl d) \<subseteq> (PIdl c)"
+      using to_contain_is_to_divide[of c d] c(1) assms(3) by simp
+    thus "PIdl d \<subseteq> PIdl a <+>\<^bsub>R\<^esub> PIdl b" using c by simp
+  qed
+qed
+
+lemma (in principal_domain) bezout_identity:
+  assumes "a \<in> carrier (mult_of R)" "b \<in> carrier (mult_of R)"
+  shows "(PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl (somegcd (mult_of R) a b))"
+proof -
+  have "(somegcd (mult_of R) a b) \<in> carrier (mult_of R)"
+    using mult_of.gcd_exists[OF assms] by simp
+  hence "\<And>x. x = somegcd (mult_of R) a b \<Longrightarrow> (PIdl a) <+>\<^bsub>R\<^esub> (PIdl b) = (PIdl x)"
+    using mult_of.gcd_isgcd[OF assms] ideal_sum_iff_gcd[OF assms] by simp
+  thus ?thesis
+    using mult_of.gcd_exists[OF assms] by blast
+qed
+
+
+subsection \<open>Euclidean Domains\<close>
+
+sublocale euclidean_domain \<subseteq> principal_domain
+  unfolding principal_domain_def principal_domain_axioms_def
+proof (auto)
+  show "domain R" by (simp add: domain_axioms)
+next
+  fix I assume I: "ideal I R" show "principalideal I R"
+  proof (cases "I = { \<zero> }")
+    case True thus ?thesis by (simp add: zeropideal) 
+  next
+    case False hence A: "I - { \<zero> } \<noteq> {}"
+      using I additive_subgroup.zero_closed ideal.axioms(1) by auto 
+    define phi_img :: "nat set" where "phi_img = (\<phi> ` (I - { \<zero> }))"
+    hence "phi_img \<noteq> {}" using A by simp 
+    then obtain m where "m \<in> phi_img" "\<And>k. k \<in> phi_img \<Longrightarrow> m \<le> k"
+      using exists_least_iff[of "\<lambda>n. n \<in> phi_img"] not_less by force
+    then obtain a where a: "a \<in> I - { \<zero> }" "\<And>b. b \<in> I - { \<zero> } \<Longrightarrow> \<phi> a \<le> \<phi> b"
+      using phi_img_def by blast
+    have "I = PIdl a"
+    proof (rule ccontr)
+      assume "I \<noteq> PIdl a"
+      then obtain b where b: "b \<in> I" "b \<notin> PIdl a"
+        using I \<open>a \<in> I - {\<zero>}\<close> cgenideal_minimal by auto
+      hence "b \<noteq> \<zero>"
+        by (metis DiffD1 I a(1) additive_subgroup.zero_closed cgenideal_ideal ideal.Icarr ideal.axioms(1))
+      then obtain q r
+        where eucl_div: "q \<in> carrier R" "r \<in> carrier R" "b = (a \<otimes> q) \<oplus> r" "r = \<zero> \<or> \<phi> r < \<phi> a"
+        using euclidean_function[of b a] a(1) b(1) ideal.Icarr[OF I] by auto
+      hence "r = \<zero> \<Longrightarrow> b \<in> PIdl a"
+        unfolding cgenideal_def using m_comm[of a] ideal.Icarr[OF I] a(1) by auto
+      hence 1: "\<phi> r < \<phi> a \<and> r \<noteq> \<zero>"
+        using eucl_div(4) b(2) by auto
+ 
+      have "r = (\<ominus> (a \<otimes> q)) \<oplus> b"
+        using eucl_div(1-3) a(1) b(1) ideal.Icarr[OF I] r_neg1 by auto
+      moreover have "\<ominus> (a \<otimes> q) \<in> I"
+        using eucl_div(1) a(1) I
+        by (meson DiffD1 additive_subgroup.a_inv_closed ideal.I_r_closed ideal.axioms(1))
+      ultimately have 2: "r \<in> I"
+        using b(1) additive_subgroup.a_closed[OF ideal.axioms(1)[OF I]] by auto
+
+      from 1 and 2 show False
+        using a(2) by fastforce
+    qed
+    thus ?thesis
+      by (meson DiffD1 I cgenideal_is_principalideal ideal.Icarr local.a(1))
+  qed
+qed
+
+sublocale field \<subseteq> euclidean_domain R "\<lambda>_. 0"
+proof (rule euclidean_domainI)
+  fix a b
+  let ?eucl_div = "\<lambda>q r. q \<in> carrier R \<and> r \<in> carrier R \<and> a = b \<otimes> q \<oplus> r \<and> (r = \<zero> \<or> 0 < 0)"
+  assume a: "a \<in> carrier R - { \<zero> }" and b: "b \<in> carrier R - { \<zero> }"
+  hence "a = b \<otimes> ((inv b) \<otimes> a) \<oplus> \<zero>"
+    by (metis DiffD1 Units_inv_closed Units_r_inv field_Units l_one m_assoc r_zero)
+  hence "?eucl_div _ ((inv b) \<otimes> a) \<zero>"
+    using a b field_Units by auto
+  thus "\<exists>q r. ?eucl_div _ q r"
+    by blast
+qed
+
+end
\ No newline at end of file