--- /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