# Theory HOL-Algebra.Polynomials

(*  Title:      HOL/Algebra/Polynomials.thy
Author:     Paulo Emílio de Vilhena
*)

theory Polynomials
imports Ring Ring_Divisibility Subrings

begin

section ‹Polynomials›

subsection ‹Definitions›

abbreviation lead_coeff :: "'a list  'a"

abbreviation degree :: "'a list  nat"
where "degree p  length p - 1"

definition polynomial :: "_  'a set  'a list  bool" ("polynomialı")
where "polynomialRK p  p = []  (set p  K  lead_coeff p  𝟬R)"

definition (in ring) monom :: "'a  nat  'a list"
where "monom a n = a # (replicate n 𝟬R)"

fun (in ring) eval :: "'a list  'a  'a"
where
"eval [] = (λ_. 𝟬)"
| "eval p = (λx. ((lead_coeff p)  (x [^] (degree p)))  (eval (tl p) x))"

fun (in ring) coeff :: "'a list  nat  'a"
where
"coeff [] = (λ_. 𝟬)"
| "coeff p = (λi. if i = degree p then lead_coeff p else (coeff (tl p)) i)"

fun (in ring) normalize :: "'a list  'a list"
where
"normalize [] = []"
| "normalize p = (if lead_coeff p  𝟬 then p else normalize (tl p))"

fun (in ring) poly_add :: "'a list  'a list  'a list"
(if length p1  length p2
then normalize (map2 (⊕) p1 ((replicate (length p1 - length p2) 𝟬) @ p2))

fun (in ring) poly_mult :: "'a list  'a list  'a list"
where
"poly_mult [] p2 = []"
| "poly_mult p1 p2 =
poly_add ((map (λa. lead_coeff p1  a) p2) @ (replicate (degree p1) 𝟬)) (poly_mult (tl p1) p2)"

fun (in ring) dense_repr :: "'a list  ('a × nat) list"
where
"dense_repr [] = []"
| "dense_repr p = (if lead_coeff p  𝟬
then (lead_coeff p, degree p) # (dense_repr (tl p))
else (dense_repr (tl p)))"

fun (in ring) poly_of_dense :: "('a × nat) list  'a list"
where "poly_of_dense dl = foldr (λ(a, n) l. poly_add (monom a n) l) dl []"

definition (in ring) poly_of_const :: "'a  'a list"
where "poly_of_const = (λk. normalize [ k ])"

subsection ‹Basic Properties›

context ring
begin

lemma polynomialI [intro]: " set p  K; lead_coeff p  𝟬   polynomial K p"
unfolding polynomial_def by auto

lemma polynomial_incl: "polynomial K p  set p  K"
unfolding polynomial_def by auto

lemma monom_in_carrier [intro]: "a  carrier R  set (monom a n)  carrier R"
unfolding monom_def by auto

lemma lead_coeff_not_zero: "polynomial K (a # p)  a  K - { 𝟬 }"
unfolding polynomial_def by simp

lemma zero_is_polynomial [intro]: "polynomial K []"
unfolding polynomial_def by simp

lemma const_is_polynomial [intro]: "a  K - { 𝟬 }  polynomial K [ a ]"
unfolding polynomial_def by auto

lemma normalize_gives_polynomial: "set p  K  polynomial K (normalize p)"
by (induction p) (auto simp add: polynomial_def)

lemma normalize_in_carrier: "set p  carrier R  set (normalize p)  carrier R"
by (induction p) (auto)

lemma normalize_polynomial: "polynomial K p  normalize p = p"
unfolding polynomial_def by (cases p) (auto)

lemma normalize_idem: "normalize ((normalize p) @ q) = normalize (p @ q)"
by (induct p) (auto)

lemma normalize_length_le: "length (normalize p)  length p"
by (induction p) (auto)

lemma eval_in_carrier: " set p  carrier R; x  carrier R   (eval p) x  carrier R"
by (induction p) (auto)

lemma coeff_in_carrier [simp]: "set p  carrier R  (coeff p) i  carrier R"
by (induction p) (auto)

lemma lead_coeff_simp [simp]: "p  []  (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)]) =
a # (map (coeff p) (rev [0..<length p]))"
by auto
also have " ... = a # p"
using Cons by simp
finally show ?case .
qed

lemma coeff_nth: "i < length p  (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"
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  coeff p1 = coeff p2"
proof
show "p1 = p2  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: "i. i  length p  (coeff p) i = 𝟬"
by (induction p) (auto)

lemma coeff_degree: "i. i > degree p  (coeff p) i = 𝟬"
using coeff_length by (simp)

lemma replicate_zero_coeff [simp]: "coeff (replicate n 𝟬) = (λ_. 𝟬)"
by (induction n) (auto)

lemma scalar_coeff: "a  carrier R  coeff (map (λb. a  b) p) = (λi. a  (coeff p) i)"
by (induction p) (auto)

lemma monom_coeff: "coeff (monom a n) = (λi. if i = n then a else 𝟬)"
unfolding monom_def by (induction n) (auto)

lemma coeff_img:
"(coeff p) ` {..< length p} = set p"
"(coeff p) ` { length p ..} = { 𝟬 }"
"(coeff p) ` UNIV = (set p)  { 𝟬 }"
using coeff_img_restrict
proof (simp)
show coeff_img_up: "(coeff p) ` { length p ..} = { 𝟬 }"
using coeff_length[of p] by force
from coeff_img_up and coeff_img_restrict[of p]
show "(coeff p) ` UNIV = (set p)  { 𝟬 }"
by force
qed

lemma degree_def':
assumes "polynomial K p"
shows "degree p = (LEAST n. i. i > n  (coeff p) i = 𝟬)"
proof (cases p)
case Nil thus ?thesis by auto
next
define P where "P = (λn. i. i > n  (coeff p) i = 𝟬)"

case (Cons a ps)
hence "(coeff p) (degree p)  𝟬"
using assms unfolding polynomial_def by auto
hence "n. n < degree p  ¬ 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 K p1" and "polynomial K p2"
shows "p1 = p2  coeff p1 = coeff p2"
proof
show "p1 = p2  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  []  p2  []"
hence "length p1 = length p2"
using deg_eq 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 K p2"
have "p2 = []"
proof (rule ccontr)
assume "p2  []"
hence "(coeff p2) (degree p2)  𝟬"
using A(3) unfolding polynomial_def
by (metis coeff.simps(2) list.collapse)
moreover have "(coeff p1) ` UNIV = { 𝟬 }"
using A(1) by auto
hence "(coeff p2) ` UNIV = { 𝟬 }"
using A(2) by simp
ultimately show False
by blast
qed } note aux_lemma = this
assume "¬ (p1  []  p2  [])"
hence "p1 = []  p2 = []" by simp
thus ?thesis
using assms coeff_eq aux_lemma[of p1 p2] aux_lemma[of p2 p1] by auto
qed
qed

assumes "length (normalize p) < length p"
proof (cases p)
case Nil thus ?thesis
using assms by simp
next
case (Cons a ps) thus ?thesis
using assms by (cases "a = 𝟬") (auto)
qed

lemma normalize_length_lt:
assumes "lead_coeff p = 𝟬" 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:
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 𝟬) @ p) = normalize p"
by (induction n) (auto)

lemma normalize_def':
shows   "p = (replicate (length p - length (normalize p)) 𝟬) @
(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 = 𝟬")
assume "a  𝟬" thus ?case
using Cons by simp
next
assume eq_zero: "a = 𝟬"
hence len_eq:
"Suc (length p - length (normalize p)) = length (a # p) - length (normalize (a # p))"
have "a # p = 𝟬 # (replicate (length p - length (normalize p)) 𝟬 @
drop (length p - length (normalize p)) p)"
using eq_zero Cons by simp
also have " ... = (replicate (Suc (length p - length (normalize p))) 𝟬 @
drop (Suc (length p - length (normalize p))) (a # p))"
by simp
also have " ... = (replicate (length (a # p) - length (normalize (a # p))) 𝟬 @
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 "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 = 𝟬")
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

corollary normalize_trick:
shows "p = (replicate (length p - length (normalize p)) 𝟬) @ (normalize p)"
using normalize_def'(1)[of p] unfolding sym[OF normalize_def'(2)] .

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) = 𝟬"
using normalize_length_le[of p] coeff_degree[of "normalize p"] coeff_length by blast
then show ?case
using Cons by (cases "a = 𝟬") (auto)
qed

lemma append_coeff:
"coeff (p @ q) = (λ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) = (λi. if i = length p + length q then a else (coeff (p @ q)) i)"
by auto
also have " ... = (λ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 " ... = (λ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 " ... = (λ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 " ... = (λi. if i < length q then (coeff q) i else (coeff (a # p)) (i - length q))"
by auto
finally show ?case .
qed

lemma prefix_replicate_zero_coeff: "coeff p = coeff ((replicate n 𝟬) @ p)"
using append_coeff[of "replicate n 𝟬" p] replicate_zero_coeff[of n] coeff_length[of p] by auto

(* ========================================================================== *)
context
fixes K :: "'a set" assumes K: "subring K R"
begin

lemma polynomial_in_carrier [intro]: "polynomial K p  set p  carrier R"
unfolding polynomial_def using subringE(1)[OF K] by auto

lemma carrier_polynomial [intro]: "polynomial K p  polynomial (carrier R) p"
unfolding polynomial_def using subringE(1)[OF K] by auto

lemma append_is_polynomial: " polynomial K p; p  []   polynomial K (p @ (replicate n 𝟬))"
unfolding polynomial_def using subringE(2)[OF K] by auto

lemma lead_coeff_in_carrier: "polynomial K (a # p)  a  carrier R - { 𝟬 }"
unfolding polynomial_def using subringE(1)[OF K] by auto

lemma monom_is_polynomial [intro]: "a  K - { 𝟬 }  polynomial K (monom a n)"
unfolding polynomial_def monom_def using subringE(2)[OF K] by auto

lemma eval_poly_in_carrier: " polynomial K p; x  carrier R   (eval p) x  carrier R"
using eval_in_carrier[OF polynomial_in_carrier] .

lemma poly_coeff_in_carrier [simp]: "polynomial K p  coeff p i  carrier R"
using coeff_in_carrier[OF polynomial_in_carrier] .

end (* of fixed K context. *)
(* ========================================================================== *)

(* ========================================================================== *)
context
fixes K :: "'a set" assumes K: "subring K R"
begin

assumes "set p1  K" and "set p2  K"
shows "polynomial K (poly_add p1 p2)"
proof -
{ fix p1 p2 assume A: "set p1  K" "set p2  K" "length p1  length p2"
hence "polynomial K (poly_add p1 p2)"
proof -
define p2' where "p2' = (replicate (length p1 - length p2) 𝟬) @ p2"
hence "set p2'  K" and "length p1 = length p2'"
using A(2-3) subringE(2)[OF K] by auto
hence "set (map2 (⊕) p1 p2')  K"
using A(1) subringE(7)[OF K]
by (induct p1) (auto, metis set_ConsD subsetD set_zip_leftD set_zip_rightD)
thus ?thesis
unfolding p2'_def using normalize_gives_polynomial A(3) by simp
qed }
thus ?thesis
using assms by auto
qed

lemma poly_add_closed: " polynomial K p1; polynomial K p2   polynomial K (poly_add p1 p2)"

assumes "polynomial K p1" "polynomial K p2" and "length p1  length p2"
shows "length (poly_add p1 p2) = max (length p1) (length p2)"
proof -
{ fix p1 p2 assume A: "polynomial K p1" "polynomial K p2" "length p1 > length p2"
hence "length (poly_add p1 p2) = max (length p1) (length p2)"
proof -
let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2"
have p1: "p1  []" and p2: "?p2  []"
using A(3) by auto
then have "zip p1 (replicate (length p1 - length p2) 𝟬 @ p2) = zip (lead_coeff p1 # tl p1) (lead_coeff (replicate (length p1 - length p2) 𝟬 @ p2) # tl (replicate (length p1 - length p2) 𝟬 @ p2))"
by auto
by simp
moreover have "lead_coeff p1  carrier R"
using p1 A(1) lead_coeff_in_carrier[OF K, of "hd p1" "tl p1"] by auto
using A(3) by auto
using p1 A(1) unfolding polynomial_def by simp
ultimately have "length (normalize (map2 (⊕) 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

assumes "polynomial K p1" "polynomial K p2" and "degree p1  degree p2"
shows "degree (poly_add p1 p2) = max (degree p1) (degree p2)"
using poly_add_length_eq[OF assms(1-2)] assms(3) by simp

end (* of fixed K context. *)
(* ========================================================================== *)

" set p1  carrier R; set p2  carrier R   set (poly_add p1 p2)  carrier R"
using polynomial_incl[OF poly_add_is_polynomial[OF carrier_is_subring]] by simp

proof -
{ fix p1 p2 :: "'a list" assume A: "length p1  length p2"
let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2"
have "length (poly_add p1 p2)  max (length p1) (length p2)"
using normalize_length_le[of "map2 (⊕) p1 ?p2"] A by auto }
thus ?thesis
qed

using poly_add_length_le by (meson diff_le_mono le_max_iff_disj)

assumes "length p1  length p2"
shows "coeff (poly_add p1 p2) = (λi. ((coeff p1) i)  ((coeff p2) i))"
proof
fix i
have "i < length p1  (coeff (poly_add p1 p2)) i = ((coeff p1) i)  ((coeff p2) i)"
proof -
let ?p2 = "(replicate (length p1 - length p2) 𝟬) @ p2"
have len_eqs: "length p1 = length ?p2" "length (map2 (⊕) p1 ?p2) = length p1"
using assms by auto
assume i_lt: "i < length p1"
have "(coeff (poly_add p1 p2)) i = (coeff (map2 (⊕) p1 ?p2)) i"
using normalize_coeff[of "map2 (⊕) p1 ?p2"] assms by auto
also have " ... = (map2 (⊕) p1 ?p2) ! (length p1 - 1 - i)"
using coeff_nth[of i "map2 (⊕) p1 ?p2"] len_eqs(2) i_lt by auto
also have " ... = (p1 ! (length p1 - 1 - i))  (?p2 ! (length ?p2 - 1 - i))"
using len_eqs i_lt by auto
also have " ... = ((coeff p1) i)  ((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)  ((coeff p2) i)"
using prefix_replicate_zero_coeff by simp
finally show "(coeff (poly_add p1 p2)) i = ((coeff p1) i)  ((coeff p2) i)" .
qed
moreover
have "i  length p1  (coeff (poly_add p1 p2)) i = ((coeff p1) i)  ((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)  ((coeff p2) i)"
using not_le by blast
qed

assumes "set p1  carrier R" "set p2  carrier R"
shows "coeff (poly_add p1 p2) = (λi. ((coeff p1) i)  ((coeff p2) i))"
proof -
have "length p1  length p2  length p2 > length p1"
by auto
thus ?thesis
proof
assume "length p1  length p2" thus ?thesis
next
assume "length p2 > length p1"
hence "coeff (poly_add p1 p2) = (λi. ((coeff p2) i)  ((coeff p1) i))"
thus ?thesis
qed
qed

assumes "set p1  carrier R" "set p2  carrier R"
proof -
coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] add.m_comm by auto
thus ?thesis
using coeff_iff_polynomial_cond[OF
qed

assumes "set p  carrier R" and "a  carrier R - { 𝟬 }"
shows "poly_add (monom a (length p)) p = a # p"
unfolding monom_def using assms by (induction p) (auto)

assumes "set p  carrier R" "set q  carrier R"
shows "poly_add (p @ (replicate (length q) 𝟬)) q = normalize (p @ q)"
proof -
have "map2 (⊕) (p @ (replicate (length q) 𝟬)) ((replicate (length p) 𝟬) @ q) = p @ q"
using assms by (induct p) (induct q, auto)
thus ?thesis by simp
qed

assumes "set p  carrier R" "set q  carrier R"
shows "poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ]) = normalize ((poly_add p q) @ [ 𝟬 ])"
proof -
have in_carrier: "set (p @ [ 𝟬 ])  carrier R" "set (q @ [ 𝟬 ])  carrier R"
using assms by auto
have "coeff (poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ])) = coeff ((poly_add p q) @ [ 𝟬 ])"
using append_coeff[of p "[ 𝟬 ]"] poly_add_coeff[OF in_carrier]
append_coeff[of q "[ 𝟬 ]"] append_coeff[of "poly_add p q" "[ 𝟬 ]"]
poly_add_coeff[OF assms] assms[THEN coeff_in_carrier] by auto
hence "coeff (poly_add (p @ [ 𝟬 ]) (q @ [ 𝟬 ])) = coeff (normalize ((poly_add p q) @ [ 𝟬 ]))"
using normalize_coeff by simp
moreover have "set ((poly_add p q) @ [ 𝟬 ])  carrier R"
ultimately show ?thesis
normalize_gives_polynomial] by simp
qed

assumes "set p1  carrier R" "set p2  carrier R"
proof -
{ fix n p1 p2 assume "set p1  carrier R" "set p2  carrier R"
hence "poly_add p1 p2 = poly_add ((replicate n 𝟬) @ p1) p2"
proof (induction n)
case 0 thus ?case by simp
next
{ fix p1 p2 :: "'a list"
assume in_carrier: "set p1  carrier R" "set p2  carrier R"
proof -
have "length p1  length p2  ?thesis"
proof -
assume A: "length p1  length p2"
let ?p2 = "λn. (replicate n 𝟬) @ p2"
have "poly_add p1 p2 = normalize (map2 (⊕) (𝟬 # p1) (𝟬 # ?p2 (length p1 - length p2)))"
using A by simp
also have " ... = normalize (map2 (⊕) (𝟬 # p1) (?p2 (length (𝟬 # p1) - length p2)))"
also have " ... = poly_add (𝟬 # p1) p2"
using A by simp
finally show ?thesis .
qed

moreover have "length p2 > length p1  ?thesis"
proof -
assume A: "length p2 > length p1"
let ?f = "λn p. (replicate n 𝟬) @ p"
using A by simp
also have " ... = normalize (map2 (⊕) p2 (?f (length p2 - length p1) p1))"
using A by simp
also have " ... = normalize (map2 (⊕) p2 (?f (length p2 - Suc (length p1)) (𝟬 # p1)))"
by (metis A Suc_diff_Suc append_Cons replicate_Suc replicate_app_Cons_same)
also have " ... = poly_add p2 (𝟬 # p1)"
using A by simp
also have " ... = poly_add (𝟬 # p1) p2"
using poly_add_comm[of p2 "𝟬 # 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 𝟬 @ p1)  carrier R"
by auto
have "poly_add p1 p2 = poly_add (replicate n 𝟬 @ p1) p2"
using Suc by simp
also have " ... = poly_add (replicate (Suc n) 𝟬 @ p1) p2"
using aux_lemma[OF in_carrier Suc(3)] by simp
finally show ?case .
qed } note aux_lemma = this

poly_add ((replicate (length p1 - length (normalize p1)) 𝟬) @ normalize p1) p2"
using normalize_def'[of p1] by simp
also have " ... = poly_add (normalize p1) p2"
using aux_lemma[OF normalize_in_carrier[OF assms(1)] assms(2)] by simp
finally show ?thesis .
qed

assumes "set p1  carrier R" "set p2  carrier R"
proof -
poly_add_comm[OF normalize_in_carrier[OF assms(2)] assms(1)] by simp
next
also have " ... = poly_add (normalize p2) (normalize p1)"
poly_add_normalize_aux[OF assms(2) normalize_in_carrier[OF assms(1)]] by simp
qed

assumes "set p  carrier R"
shows  and
proof -
have "map2 (⊕) p (replicate (length p) 𝟬) = p"
using assms by (induct p) (auto)
thus  and
using poly_add_comm[OF assms, of "[]"] by simp+
qed

assumes "subring K R" "polynomial K p"
shows "poly_add p [] = p" and "poly_add [] p = p"
using poly_add_zero' normalize_polynomial polynomial_in_carrier assms by auto

assumes "set p  carrier R"
shows "poly_add p (replicate n 𝟬) = normalize p" and "poly_add (replicate n 𝟬) p = normalize p"
proof -
have
using poly_add_normalize(2)[OF assms, of "replicate n 𝟬"]
normalize_replicate_zero[of n "[]"] by force
also have " ... = normalize p"
finally show "poly_add p (replicate n 𝟬) = normalize p" .
thus "poly_add (replicate n 𝟬) p = normalize p"
using poly_add_comm[OF assms, of "replicate n 𝟬"] by force
qed

assumes "subring K R" "polynomial K p"
shows "poly_add p (replicate n 𝟬) = p" and "poly_add (replicate n 𝟬) p = p"
using poly_add_replicate_zero' normalize_polynomial polynomial_in_carrier assms by auto

subsection ‹Dense Representation›

lemma dense_repr_replicate_zero: "dense_repr ((replicate n 𝟬) @ p) = dense_repr p"
by (induction n) (auto)

lemma dense_repr_normalize:
by (induct p) (auto)

lemma polynomial_dense_repr:
assumes "polynomial K p" and "p  []"
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  K - { 𝟬 }" and p': "set p'  K"
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')) 𝟬) @ ?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 monom_decomp:
assumes "subring K R" "polynomial K p"
shows "p = poly_of_dense (dense_repr p)"
using assms(2)
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  carrier R - { 𝟬 }" and l: "set l  carrier R"  "set l  K"
using less(2) subringE(1)[OF assms(1)] by (auto simp add: polynomial_def)
hence "a # l = poly_add (monom a (degree (a # l))) l"
using poly_add_monom[of l a] by simp
also have " ... = poly_add (monom a (degree (a # l))) (normalize l)"
using poly_add_normalize(2)[of "monom a (degree (a # l))", OF _ l(1)] a
unfolding monom_def by force
also have " ... = poly_add (monom a (degree (a # l))) (poly_of_dense (dense_repr (normalize l)))"
using less(1)[OF _ normalize_gives_polynomial[OF l(2)]] normalize_length_le[of l]
unfolding Cons by simp
also have " ... = poly_of_dense ((a, degree (a # l)) # dense_repr (normalize l))"
by simp
also have " ... = poly_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

subsection ‹Polynomial Multiplication›

lemma poly_mult_is_polynomial:
assumes "subring K R" "set p1  K" and "set p2  K"
shows "polynomial K (poly_mult p1 p2)"
using assms(2-3)
proof (induction p1)
case Nil thus ?case
next
case (Cons a p1)
let ?a_p2 = "(map (λb. a  b) p2) @ (replicate (degree (a # p1)) 𝟬)"

have "set (poly_mult p1 p2)  K"
using Cons unfolding polynomial_def by auto
moreover have "set ?a_p2  K"
using assms(3) Cons(2) subringE(1-2,6)[OF assms(1)] by(induct p2) (auto)
ultimately have "polynomial K (poly_add ?a_p2 (poly_mult p1 p2))"
thus ?case by simp
qed

lemma poly_mult_closed:
assumes "subring K R"
shows " polynomial K p1; polynomial K p2   polynomial K (poly_mult p1 p2)"
using poly_mult_is_polynomial polynomial_incl assms by simp

lemma poly_mult_in_carrier:
" set p1  carrier R; set p2  carrier R   set (poly_mult p1 p2)  carrier R"
using poly_mult_is_polynomial polynomial_in_carrier carrier_is_subring by simp

lemma poly_mult_coeff:
assumes "set p1  carrier R" "set p2  carrier R"
shows "coeff (poly_mult p1 p2) = (λi.  k  {..i}. (coeff p1) k  (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  carrier R" "i. (coeff p1) i  carrier R" "i. (coeff p2) i  carrier R"
using coeff_in_carrier assms(2) by auto

let ?a_p2 = "(map (λb. a  b) p2) @ (replicate (degree (a # p1)) 𝟬)"
have "coeff  (replicate (degree (a # p1)) 𝟬) = (λ_. 𝟬)"
and "length (replicate (degree (a # p1)) 𝟬) = length p1"
using prefix_replicate_zero_coeff[of "[]" "length p1"] by auto
hence "coeff ?a_p2 = (λi. if i < length p1 then 𝟬 else (coeff (map (λb. a  b) p2)) (i - length p1))"
using append_coeff[of "map (λb. a  b) p2" "replicate (length p1) 𝟬"] by auto
also have " ... = (λi. if i < length p1 then 𝟬 else a  ((coeff p2) (i - length p1)))"
proof -
have "i. i < length p2  (coeff (map (λb. a  b) p2)) i = a  ((coeff p2) i)"
proof -
fix i assume i_lt: "i < length p2"
hence "(coeff (map (λb. a  b) p2)) i = (map (λb. a  b) p2) ! (length p2 - 1 - i)"
using coeff_nth[of i "map (λb. a  b) p2"] by auto
also have " ... = a  (p2 ! (length p2 - 1 - i))"
using i_lt by auto
also have " ... = a  ((coeff p2) i)"
using coeff_nth[OF i_lt] by simp
finally show "(coeff (map (λb. a  b) p2)) i = a  ((coeff p2) i)" .
qed
moreover have "i. i  length p2  (coeff (map (λb. a  b) p2)) i = a  ((coeff p2) i)"
using coeff_length[of p2] coeff_length[of "map (λb. a  b) p2"] in_carrier by auto
ultimately show ?thesis by (meson not_le)
qed
also have " ... = (λi.  k  {..i}. (if k = length p1 then a else 𝟬)  (coeff p2) (i - k))"
(is "?f1 = (λi. ( k  {..i}. ?f2 k  ?f3 (i - k)))")
proof
fix i
have "k. k  {..i}  ?f2 k  ?f3 (i - k) = 𝟬" if "i < length p1"
using in_carrier that by auto
hence "( k  {..i}. ?f2 k  ?f3 (i - k)) = 𝟬" if "i < length p1"
using that in_carrier
add.finprod_cong'[of "{..i}" "{..i}" "λk. ?f2 k  ?f3 (i - k)" "λi. 𝟬"]
by auto
hence eq_lt: "?f1 i = (λi. ( k  {..i}. ?f2 k  ?f3 (i - k))) i" if "i < length p1"
using that by auto

have "k. k  {..i}
?f2 k R?f3 (i - k) = (if length p1 = k then a  coeff p2 (i - k) else 𝟬)"
using in_carrier by auto
hence "( k  {..i}. ?f2 k  ?f3 (i - k)) =
( k  {..i}. (if length p1 = k then a  coeff p2 (i - k) else 𝟬))"
using in_carrier
add.finprod_cong'[of "{..i}" "{..i}" "λk. ?f2 k  ?f3 (i - k)"
"λk. (if length p1 = k then a  coeff p2 (i - k) else 𝟬)"]
by fastforce
also have " ... = a  (coeff p2) (i - length p1)" if "i  length p1"
using add.finprod_singleton[of "length p1" "{..i}" "λj. a  (coeff p2) (i - j)"]
in_carrier that by auto
finally
have "( k  {..i}. ?f2 k  ?f3 (i - k)) =  a  (coeff p2) (i - length p1)" if "i  length p1"
using that by simp
hence eq_ge: "?f1 i = (λi. ( k  {..i}. ?f2 k  ?f3 (i - k))) i" if "i  length p1"
using that by auto

from eq_lt eq_ge show "?f1 i = (λi. ( k  {..i}. ?f2 k  ?f3 (i - k))) i" by auto
qed

finally have coeff_a_p2:
"coeff ?a_p2 = (λi.  k  {..i}. (if k = length p1 then a else 𝟬)  (coeff p2) (i - k))" .

have "set ?a_p2  carrier R"
using in_carrier(1) assms(2) by auto

moreover have "set (poly_mult p1 p2)  carrier R"
using poly_mult_in_carrier[OF _ assms(2)] Cons(2) by simp

ultimately
have "coeff (poly_mult (a # p1) p2) = (λi. ((coeff ?a_p2) i)  ((coeff (poly_mult p1 p2)) i))"
using poly_add_coeff[of ?a_p2 "poly_mult p1 p2"] by simp
also have " ... = (λi. ( k  {..i}. (if k = length p1 then a else 𝟬)  (coeff p2) (i - k))
( k  {..i}. (coeff p1) k  (coeff p2) (i - k)))"
using Cons  coeff_a_p2 by simp
also have " ... = (λi. ( k  {..i}. ((if k = length p1 then a else 𝟬)  (coeff p2) (i - k))
((coeff p1) k  (coeff p2) (i - k))))"
also have " ... = (λi. ( k  {..i}. (coeff (a # p1) k)  (coeff p2) (i - k)))"
(is "(λi. ( k  {..i}. ?f i k)) = (λi. ( k  {..i}. ?g i k))")
proof
fix i
have "k. ?f i k = ?g i k"
using in_carrier coeff_length[of p1] by auto
thus "( k  {..i}. ?f i k) = ( k  {..i}. ?g i k)" by simp
qed
finally show ?case .
qed

lemma poly_mult_zero:
assumes "set p  carrier R"
shows  and
proof (simp)
have "coeff (poly_mult p []) = (λ_. 𝟬)"
using poly_mult_coeff[OF assms, of "[]"] coeff_in_carrier[OF assms] by auto
thus
using coeff_iff_polynomial_cond[OF
poly_mult_is_polynomial[OF carrier_is_subring assms] zero_is_polynomial] by simp
qed

lemma poly_mult_l_distr':
assumes "set p1  carrier R" "set p2  carrier R" "set p3  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:
"i. ?c1 i  carrier R" "i. ?c2 i  carrier R" "i. ?c3 i  carrier R"
using assms coeff_in_carrier by auto

have "coeff (poly_mult (poly_add p1 p2) p3) = (λn. i  {..n}. (?c1 i  ?c2 i)  ?c3 (n - i))"
also have " ... = (λn. i  {..n}. (?c1 i  ?c3 (n - i))  (?c2 i  ?c3 (n - i)))"
using in_carrier l_distr by auto
also
have " ... = (λn. (i  {..n}. (?c1 i  ?c3 (n - i)))  (i  {..n}. (?c2 i  ?c3 (n - i))))"
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_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 (carrier R) (poly_mult (poly_add p1 p2) p3)"
and "polynomial (carrier R) (poly_add (poly_mult p1 p3) (poly_mult p2 p3))"
carrier_is_subring by auto
ultimately show ?thesis
using coeff_iff_polynomial_cond by auto
qed

lemma poly_mult_l_distr:
assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K 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_prepend_replicate_zero:
assumes "set p1  carrier R" "set p2  carrier R"
shows "poly_mult p1 p2 = poly_mult ((replicate n 𝟬) @ p1) p2"
proof -
{ fix p1 p2 assume A: "set p1  carrier R" "set p2  carrier R"
hence "poly_mult p1 p2 = poly_mult (𝟬 # p1) p2"
proof -
let ?a_p2 = "(map ((⊗) 𝟬) p2) @ (replicate (length p1) 𝟬)"
have "?a_p2 = replicate (length p2 + length p1) 𝟬"
using A(2) by (induction p2) (auto)
hence "poly_mult (𝟬 # p1) p2 = poly_add (replicate (length p2 + length p1) 𝟬) (poly_mult p1 p2)"
by simp
also have " ... = poly_add (normalize (replicate (length p2 + length p1) 𝟬)) (poly_mult p1 p2)"
using poly_add_normalize(1)[of "replicate (length p2 + length p1) 𝟬" "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]] carrier_is_subring
normalize_replicate_zero[of "length p2 + length p1" "[]"] by simp
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 𝟬 @ p1" p2] by force
qed
qed

lemma poly_mult_normalize:
assumes "set p1  carrier R" "set p2  carrier R"
shows "poly_mult p1 p2 = poly_mult (normalize p1) p2"
proof -
let ?replicate = "replicate (length p1 - length (normalize p1)) 𝟬"
have "poly_mult p1 p2 = poly_mult (?replicate @ (normalize p1)) p2"
using normalize_def'[of p1] by simp
thus ?thesis
using poly_mult_prepend_replicate_zero normalize_in_carrier assms by auto
qed

lemma poly_mult_append_zero:
assumes "set p  carrier R" "set q  carrier R"
shows "poly_mult (p @ [ 𝟬 ]) q = normalize ((poly_mult p q) @ [ 𝟬 ])"
using assms(1)
proof (induct p)
case Nil thus ?case
using poly_mult_normalize[OF _ assms(2), of "[] @ [ 𝟬 ]"]
poly_mult_zero(1) poly_mult_zero(1)[of "q @ [ 𝟬 ]"] assms(2) by auto
next
case (Cons a p)
let ?q_a = "λn. (map ((⊗) a) q) @ (replicate n 𝟬)"
have set_q_a: "n. set (?q_a n)  carrier R"
using Cons(2) assms(2) by (induct q) (auto)
have set_poly_mult: "set ((poly_mult p q) @ [ 𝟬 ])  carrier R"
using poly_mult_in_carrier[OF _ assms(2)] Cons(2) by auto
have "poly_mult ((a # p) @ [𝟬]) q = poly_add (?q_a (Suc (length p))) (poly_mult (p @ [𝟬]) q)"
by auto
also have " ... = poly_add (?q_a (Suc (length p))) (normalize ((poly_mult p q) @ [ 𝟬 ]))"
using Cons by simp
also have " ... = poly_add ((?q_a (length p)) @ [ 𝟬 ]) ((poly_mult p q) @ [ 𝟬 ])"
using poly_add_normalize(2)[OF set_q_a[of "Suc (length p)"] set_poly_mult]
also have " ... = normalize ((poly_add (?q_a (length p)) (poly_mult p q)) @ [ 𝟬 ])"
using poly_add_append_zero[OF set_q_a[of "length p"] poly_mult_in_carrier[OF _ assms(2)]] Cons(2) by auto
also have " ... = normalize ((poly_mult (a # p) q) @ [ 𝟬 ])"
by auto
finally show ?case .
qed

end (* of ring context. *)

subsection ‹Properties Within a Domain›

context domain
begin

lemma one_is_polynomial [intro]: "subring K R  polynomial K [ 𝟭 ]"
unfolding polynomial_def using subringE(3) by auto

lemma poly_mult_comm:
assumes "set p1  carrier R" "set p2  carrier R"
shows "poly_mult p1 p2 = poly_mult p2 p1"
proof -
let ?c1 = "coeff p1" and ?c2 = "coeff p2"
have "i. (k  {..i}. ?c1 k  ?c2 (i - k)) = (k  {..i}. ?c2 k  ?c1 (i - k))"
proof -
fix i :: nat
let ?f = "λk. ?c1 k  ?c2 (i - k)"
have in_carrier: "i. ?c1 i  carrier R" "i. ?c2 i  carrier R"
using coeff_in_carrier[OF assms(1)] coeff_in_carrier[OF assms(2)] by auto

have reindex_inj: "inj_on (λk. i - k) {..i}"
using inj_on_def by force
moreover have "(λk. i - k) ` {..i}  {..i}" by auto
hence "(λk. i - k) ` {..i} = {..i}"
using reindex_inj endo_inj_surj[of "{..i}" "λk. i - k"] by simp
ultimately have "(k  {..i}. ?f k) = (k  {..i}. ?f (i - k))"
using add.finprod_reindex[of ?f "λk. i - k" "{..i}"] in_carrier by auto

moreover have "k. k  {..i}  ?f (i - k) = ?c2 k  ?c1 (i - k)"
using in_carrier m_comm by auto
hence "(k  {..i}. ?f (i - k)) = (k  {..i}. ?c2 k  ?c1 (i - k))"
using add.finprod_cong'[of "{..i}" "{..i}"] in_carrier by auto
ultimately show "(k  {..i}. ?f k) = (k  {..i}. ?c2 k  ?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,1)] by simp
thus ?thesis
using coeff_iff_polynomial_cond[OF poly_mult_is_polynomial[OF _ assms]
poly_mult_is_polynomial[OF _ assms(2,1)]]
carrier_is_subring by simp
qed

lemma poly_mult_r_distr':
assumes "set p1  carrier R" "set p2  carrier R" "set p3  carrier R"
shows "poly_mult p1 (poly_add p2 p3) = poly_add (poly_mult p1 p2) (poly_mult p1 p3)"
poly_mult_l_distr'[OF assms(2-3,1)] assms(2-3)[THEN poly_mult_comm[OF _ assms(1)]] ..

lemma poly_mult_r_distr:
assumes "subring K R" "polynomial K p1" "polynomial K p2" "polynomial K 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  carrier R"
shows "poly_mult (replicate n 𝟬) p = []"
and "poly_mult p (replicate n 𝟬) = []"
proof -
have in_carrier: "n. set (replicate n 𝟬)  carrier R" by auto
show "poly_mult (replicate n 𝟬) p = []" using assms
proof (induction n)
case 0 thus ?case by simp
next
case (Suc n)
hence "poly_mult (replicate (Suc n) 𝟬) p = poly_mult (𝟬 # (replicate n 𝟬)) p"
by simp
also have " ... = poly_add ((map (λa. 𝟬  a) p) @ (replicate n 𝟬)) []"
using Suc by simp
also have " ... = poly_add ((map (λa. 𝟬) p) @ (replicate n 𝟬)) []"
proof -
have "map ((⊗) 𝟬) p = map (λa. 𝟬) p"
using Suc.prems by auto
then show ?thesis
by presburger
qed
also have " ... = poly_add (replicate (length p + n) 𝟬) []"
also have " ... = poly_add [] []"
using poly_add_normalize(1)[of "replicate (length p + n) 𝟬" "[]"]
normalize_replicate_zero[of "length p + n" "[]"] by auto
also have " ... = []" by simp
finally show ?case .
qed
thus "poly_mult p (replicate n 𝟬) = []"
using poly_mult_comm[OF assms in_carrier] by simp
qed

lemma poly_mult_const':
assumes "set p  carrier R" "a  carrier R"
shows "poly_mult [ a ] p = normalize (map (λb. a  b) p)"
and "poly_mult p [ a ] = normalize (map (λb. a  b) p)"
proof -
have "map2 (⊕) (map ((⊗) a) p) (replicate (length p) 𝟬) = map ((⊗) a) p"
using assms by (induction p) (auto)
thus "poly_mult [ a ] p = normalize (map (λb. a  b) p)" by simp
thus "poly_mult p [ a ] = normalize (map (λb. a  b) p)"
using poly_mult_comm[OF assms(1), of "[ a ]"] assms(2) by auto
qed

lemma poly_mult_const:
assumes "subring K R" "polynomial K p" "a  K - { 𝟬 }"
shows "poly_mult [ a ] p = map (λb. a  b) p"
and "poly_mult p [ a ] = map (λb. a  b) p"
proof -
have in_carrier: "set p  carrier R" "a  carrier R"
using polynomial_in_carrier[OF assms(1-2)] assms(3) subringE(1)[OF assms(1)] by auto

show "poly_mult [ a ] p = map (λb. a  b) p"
proof (cases p)
case Nil thus ?thesis
using poly_mult_const'(1) in_carrier by auto
next
case (Cons b q)
have "lead_coeff (map (λb. a  b) p)  𝟬"
using assms subringE(1)[OF assms(1)] integral[of a b] Cons lead_coeff_in_carrier by auto
hence "normalize (map (λb. a  b) p) = (map (λb. a  b) p)"
unfolding Cons by simp
thus ?thesis
using poly_mult_const'(1) in_carrier by auto
qed
thus "poly_mult p [ a ] = map (λb. a  b) p"
using poly_mult_comm[OF in_carrier(1)] in_carrier(2) by auto
qed

lemma poly_mult_semiassoc:
assumes "set p  carrier R" "set q  carrier R" and "a  carrier R"
shows "poly_mult (poly_mult [ a ] p) q = poly_mult [ a ] (poly_mult p q)"
proof -
let ?cp = "coeff p" and ?cq = "coeff q"
have "coeff (poly_mult [ a ] p) = (λi. (a  ?cp i))"
using poly_mult_const'(1)[OF assms(1,3)] normalize_coeff scalar_coeff[OF assms(3)] by simp

hence "coeff (poly_mult (poly_mult [ a ] p) q) = (λi. (j  {..i}. (a  ?cp j)  ?cq (i - j)))"
using poly_mult_coeff[OF poly_mult_in_carrier[OF _ assms(1)] assms(2), of "[ a ]"] assms(3) by auto
also have " ... = (λi. a  (j  {..i}. ?cp j  ?cq (i - j)))"
proof
fix i show "(j  {..i}. (a  ?cp j)  ?cq (i - j)) = a  (j  {..i}. ?cp j  ?cq (i - j))"
using finsum_rdistr[OF _ assms(3), of _ "λj. ?cp j  ?cq (i - j)"]
assms(1-2)[THEN coeff_in_carrier] by (simp add: assms(3) m_assoc)
qed
also have " ... = coeff (poly_mult [ a ] (poly_mult p q))"
unfolding poly_mult_const'(1)[OF poly_mult_in_carrier[OF assms(1-2)] assms(3)]
using scalar_coeff[OF assms(3), of "poly_mult p q"]
poly_mult_coeff[OF assms(1-2)] normalize_coeff by simp
finally have "coeff (poly_mult (poly_mult [ a ] p) q) = coeff (poly_mult [ a ] (poly_mult p q))" .
moreover have "polynomial (carrier R) (poly_mult (poly_mult [ a ] p) q)"
and "polynomial (carrier R) (poly_mult [ a ] (poly_mult p q))"
using poly_mult_is_polynomial[OF _ poly_mult_in_carrier[OF _ assms(1)] assms(2)]
poly_mult_is_polynomial[OF _ _ poly_mult_in_carrier[OF assms(1-2)]]
carrier_is_subring assms(3) by (auto simp del: poly_mult.simps)
ultimately show ?thesis
using coeff_iff_polynomial_cond by simp
qed

text ‹Note that "polynomial (carrier R) p" and "subring K p; polynomial K p" are "equivalent"
assumptions for any lemma in ring which the result doesn't depend on K, because carrier
is a subring and a polynomial for a subset of the carrier is a carrier polynomial. The
decision between one of them should be based on how the lemma is going to be used and
proved. These are some tips:
(a) Lemmas about the algebraic structure of polynomials should use the latter option.
(b) Also, if the lemma deals with lots of polynomials, then the latter option is preferred.
(c) If the proof is going to be much easier with the first option, do not hesitate. ›

lemma poly_mult_monom':
assumes "set p  carrier R" "a  carrier R"
shows "poly_mult (monom a n) p = normalize ((map ((⊗) a) p) @ (replicate n 𝟬))"
proof -
have set_map: "set ((map ((⊗) a) p) @ (replicate n 𝟬))  carrier R"
using assms by (induct p) (auto)
show ?thesis
using poly_mult_replicate_zero(1)[OF assms(1), of n]
unfolding monom_def by simp
qed

lemma poly_mult_monom:
assumes "polynomial (carrier R) p" "a  carrier R - { 𝟬 }"
shows "poly_mult (monom a n) p =
(if p = [] then [] else (poly_mult [ a ] p) @ (replicate n 𝟬))"
proof (cases p)
case Nil thus ?thesis
using poly_mult_zero(2)[of "monom a n"] assms(2) monom_def by fastforce
next
case (Cons b ps)
hence "lead_coeff ((map (λb. a  b) p) @ (replicate n 𝟬))  𝟬"
using Cons assms integral[of a b] unfolding polynomial_def by auto
thus ?thesis
using poly_mult_monom'[OF polynomial_incl[OF assms(1)<