src/HOL/Algebra/Polynomials.thy

more standard headers;
tuned whitespace;

(*  Title:      HOL/Algebra/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>Polynomial addition\<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>Polynomial multiplication\<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