Theory Poly_Ring

section ‹The Polynomial Ring ‹R[X]› (Carrier-Set Construction)›

theory Poly_Ring
  imports Ring_Theory Finite_Composite
begin

text ‹❙‹Note on notation.› ‹Ring_Theory› frees ‹+›/‹-› for the ring operations, while
  ‹FiniteProduct› (via ‹Main›) keeps HOL's arithmetic notation; the theory merge admits
  ∗‹both›.  This is exactly what the convolution needs --- ring operations on coefficients
  (type ‹'a›) and ordinary arithmetic on the ‹nat› indices ‹k - i›.›

text ‹
  We construct the polynomial ring over a carrier-set ring ‹R› using the
  ∗‹finite-support function› representation: a polynomial is a function
  @{typ "nat ⇒ 'a"} that is eventually zero, with all coefficients drawn from the
  carrier ‹R›.  This mirrors HOL's own ‹'a poly› type (which is ‹Abs_poly›
  over a finite-support function), so the bridge to the type-class world is near
  definitional, and there is no leading-zero normalisation invariant to maintain.

  Coefficient ‹i› of a polynomial ‹p› is simply ‹p i›.  Addition is
  pointwise; multiplication is the convolution ‹(p ⊗ q) k = (∑i≤k. p i ⋅ q (k - i))›,
  computed with the additive ‹fincomp› operator of ‹R›.
›

context Ring
begin

subsection ‹Carrier, coefficients, and support›

text ‹The set of polynomials over @{term R}: finite support, coefficients in @{term R}.›
definition poly_carrier :: "(nat ⇒ 'a) set"
  where "poly_carrier ≡ {p. finite {i. p i ≠ 𝟬} ∧ (∀i. p i ∈ R)}"

lemma poly_carrierI:
  "⟦ finite {i. p i ≠ 𝟬}; ⋀i. p i ∈ R ⟧ ⟹ p ∈ poly_carrier"
  unfolding poly_carrier_def by blast

lemma poly_carrier_finite: "p ∈ poly_carrier ⟹ finite {i. p i ≠ 𝟬}"
  unfolding poly_carrier_def by blast

lemma poly_carrier_coeff_closed: "p ∈ poly_carrier ⟹ p i ∈ R"
  unfolding poly_carrier_def by blast


subsection ‹Zero and one›

definition poly_zero :: "nat ⇒ 'a"  (‹𝟬⇩P›)
  where "poly_zero ≡ (λi. 𝟬)"

definition poly_one :: "nat ⇒ 'a"  (‹𝟭⇩P›)
  where "poly_one ≡ (λi. if i = 0 then 𝟭 else 𝟬)"


subsection ‹Addition›

definition poly_add :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"  (infixl ‹⊕⇩P› 65)
  where "poly_add p q ≡ (λi. p i + q i)"

definition poly_neg :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a)"  (‹⊖⇩P _› [66] 65)
  where "poly_neg p ≡ (λi. - p i)"


subsection ‹Multiplication (convolution)›

definition poly_mult :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"  (infixl ‹⊗⇩P› 70)
  where "poly_mult p q ≡ (λk. additive.fincomp (λi. p i ⋅ q (k - i)) {..k})"

text ‹A polynomial is a ∗‹unit› when it has a two-sided multiplicative inverse in the
  polynomial ring.  (Stated directly on the carrier-set operations, since the ambient
  @{text multiplicative} monoid acts on the coefficient type, not on polynomials.)›
definition poly_unit :: "(nat ⇒ 'a) ⇒ bool"
  where "poly_unit p ≡ p ∈ poly_carrier
            ∧ (∃q. q ∈ poly_carrier ∧ p ⊗⇩P q = 𝟭⇩P ∧ q ⊗⇩P p = 𝟭⇩P)"

lemma poly_unitI:
  "⟦ p ∈ poly_carrier; q ∈ poly_carrier; p ⊗⇩P q = 𝟭⇩P; q ⊗⇩P p = 𝟭⇩P ⟧ ⟹ poly_unit p"
  unfolding poly_unit_def by blast

lemma poly_unit_closed: "poly_unit p ⟹ p ∈ poly_carrier"
  unfolding poly_unit_def by blast


subsection ‹Closure under the operations›

lemma poly_zero_closed: "𝟬⇩P ∈ poly_carrier"
  by (rule poly_carrierI) (auto simp: poly_zero_def)

lemma poly_one_closed: "𝟭⇩P ∈ poly_carrier"
  by (simp add: poly_carrierI poly_one_def)

lemma poly_add_closed:
  assumes "p ∈ poly_carrier" "q ∈ poly_carrier"
  shows "p ⊕⇩P q ∈ poly_carrier"
proof (rule poly_carrierI)
  have "{i. (p ⊕⇩P q) i ≠ 𝟬} ⊆ {i. p i ≠ 𝟬} ∪ {i. q i ≠ 𝟬}"
    using additive.right_unit poly_add_def by force
  moreover have "finite ({i. p i ≠ 𝟬} ∪ {i. q i ≠ 𝟬})"
    using assms by (simp add: poly_carrier_finite)
  ultimately show "finite {i. (p ⊕⇩P q) i ≠ 𝟬}" by (rule finite_subset)
  show "⋀i. (p ⊕⇩P q) i ∈ R"
    using assms by (simp add: poly_add_def poly_carrier_coeff_closed)
qed

text ‹Each coefficient of a product is a finite sum of products of carrier elements.›
lemma poly_mult_coeff_closed:
  assumes "p ∈ poly_carrier" "q ∈ poly_carrier"
  shows "(p ⊗⇩P q) k ∈ R"
  by (simp add: assms(1,2) poly_carrier_coeff_closed poly_mult_def)

text ‹A product coefficient vanishes beyond the sum of the two top degrees, so the product has
  finite support.›
lemma poly_mult_support_bound:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier"
    and k: "k > (if {i. p i ≠ 𝟬} = {} then 0 else Max {i. p i ≠ 𝟬})
              + (if {i. q i ≠ 𝟬} = {} then 0 else Max {i. q i ≠ 𝟬})"
  shows "(p ⊗⇩P q) k = 𝟬"
proof -
  define Np where "Np = (if {i. p i ≠ 𝟬} = {} then 0 else Max {i. p i ≠ 𝟬})"
  define Nq where "Nq = (if {i. q i ≠ 𝟬} = {} then 0 else Max {i. q i ≠ 𝟬})"
  have finP: "finite {i. p i ≠ 𝟬}" using p by (rule poly_carrier_finite)
  have finQ: "finite {i. q i ≠ 𝟬}" using q by (rule poly_carrier_finite)
  have pNp: "⋀i. p i ≠ 𝟬 ⟹ i ≤ Np"
    using finP unfolding Np_def by (auto simp: Max_ge)
  have qNq: "⋀i. q i ≠ 𝟬 ⟹ i ≤ Nq"
    using finQ unfolding Nq_def by (auto simp: Max_ge)
  have kgt: "k > Np + Nq" using k unfolding Np_def Nq_def by simp
  have "p i ⋅ q (k - i) = 𝟬" if "i ∈ {..k}" for i
  proof (cases "p i = 𝟬")
    case True then show ?thesis using p q by (simp add: poly_carrier_coeff_closed)
  next
    case False 
    then show ?thesis using p q kgt pNp qNq 
      using poly_carrier_coeff_closed Ring.right_zero Ring_axioms order.strict_trans
      by fastforce
  qed
  then show ?thesis
    unfolding poly_mult_def by (rule additive.fincomp_unit_eqI)
qed

lemma poly_mult_closed:
  assumes "p ∈ poly_carrier" "q ∈ poly_carrier"
  shows "p ⊗⇩P q ∈ poly_carrier"
proof (rule poly_carrierI)
  let ?B = "(if {i. p i ≠ 𝟬} = {} then 0 else Max {i. p i ≠ 𝟬})
          + (if {i. q i ≠ 𝟬} = {} then 0 else Max {i. q i ≠ 𝟬})"
  have "{i. (p ⊗⇩P q) i ≠ 𝟬} ⊆ {..?B}"
    by (fastforce simp: intro: poly_mult_support_bound[OF assms])
  then show "finite {i. (p ⊗⇩P q) i ≠ 𝟬}" by (rule finite_subset) simp
  show "⋀i. (p ⊗⇩P q) i ∈ R" using assms by (rule poly_mult_coeff_closed)
qed

subsection ‹Distribution of multiplication over finite additive sums›

text ‹A fixed factor distributes over an additive finite sum (left and right versions).›
lemma fincomp_mult_distrib_left:
  assumes "a ∈ R" and "g ∈ A → R"
  shows "a ⋅ additive.fincomp g A = additive.fincomp (λi. a ⋅ g i) A"
proof (cases "finite A")
  case True
  then show ?thesis using assms
  proof (induct A rule: finite_induct)
    case empty then show ?case by simp
  next
    case (insert x A)
    then have "a ⋅ additive.fincomp g (insert x A) = a ⋅ g x + additive.fincomp (λi. a ⋅ g i) A"
      by (simp add: distributive)
    also have "… = additive.fincomp (λi. a ⋅ g i) (insert x A)"
      using insert assms by (simp add: additive.fincomp_insert Pi_iff)
    finally show ?case .
  qed
next
  case False
  then show ?thesis using assms by (simp add: additive.fincomp_infinite)
qed

lemma fincomp_mult_distrib_right:
  assumes "a ∈ R" and "g ∈ A → R"
  shows "additive.fincomp g A ⋅ a = additive.fincomp (λi. g i ⋅ a) A"
proof (cases "finite A")
  case True
  then show ?thesis using assms
  proof (induct A rule: finite_induct)
    case empty then show ?case by simp
  next
    case (insert x A)
    then have "additive.fincomp g (insert x A) ⋅ a = g x ⋅ a + additive.fincomp (λi. g i ⋅ a) A"
      by (simp add: distributive)
    also have "… = additive.fincomp (λi. g i ⋅ a) (insert x A)"
      using insert assms by (simp add: Pi_iff additive.fincomp_insert)
    finally show ?case .
  qed
next
  case False
  then show ?thesis using assms by (simp add: additive.fincomp_infinite)
qed


subsection ‹Pointwise additive structure›

lemma poly_add_assoc:
  "⟦ p ∈ poly_carrier; q ∈ poly_carrier; r ∈ poly_carrier ⟧
     ⟹ (p ⊕⇩P q) ⊕⇩P r = p ⊕⇩P (q ⊕⇩P r)"
  by (auto simp: poly_add_def additive.associative poly_carrier_coeff_closed)

lemma poly_add_comm:
  "⟦ p ∈ poly_carrier; q ∈ poly_carrier ⟧ ⟹ p ⊕⇩P q = q ⊕⇩P p"
  by (auto simp: poly_add_def additive.commutative poly_carrier_coeff_closed)

lemma poly_add_zero: "p ∈ poly_carrier ⟹ 𝟬⇩P ⊕⇩P p = p"
  by (auto simp: poly_add_def poly_zero_def poly_carrier_coeff_closed)

lemma poly_neg_closed: "p ∈ poly_carrier ⟹ ⊖⇩P p ∈ poly_carrier"
proof (rule poly_carrierI)
  assume p: "p ∈ poly_carrier"
  have "{i. (⊖⇩P p) i ≠ 𝟬} ⊆ {i. p i ≠ 𝟬}"
    using additive.inverse_unit poly_neg_def by force
  then show "finite {i. (⊖⇩P p) i ≠ 𝟬}"
    using p poly_carrier_finite finite_subset by blast 
  show "⋀i. (⊖⇩P p) i ∈ R" using p by (simp add: poly_neg_def poly_carrier_coeff_closed)
qed

lemma poly_add_neg: "p ∈ poly_carrier ⟹ (⊖⇩P p) ⊕⇩P p = 𝟬⇩P"
  by (auto simp: poly_add_def poly_neg_def poly_zero_def poly_carrier_coeff_closed)

lemma poly_add_neg_right: "p ∈ poly_carrier ⟹ p ⊕⇩P (⊖⇩P p) = 𝟬⇩P"
  using poly_add_comm poly_add_neg poly_neg_closed by force

text ‹Additive cancellation: @{text "x ⊕ (a ⊕ ⊖x) = a"} for carrier polynomials.›
lemma poly_add_minus_cancel:
  assumes "x ∈ poly_carrier" "a ∈ poly_carrier"
  shows "x ⊕⇩P (a ⊕⇩P (⊖⇩P x)) = a"
  by (metis assms poly_add_assoc poly_add_comm poly_add_neg_right poly_add_zero poly_neg_closed)

text ‹Left cancellation for polynomial addition.›
lemma poly_add_left_cancel:
  assumes x: "x ∈ poly_carrier" and a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
    and eq: "x ⊕⇩P a = x ⊕⇩P b"
  shows "a = b"
  by (metis a b eq poly_add_assoc poly_add_minus_cancel poly_neg_closed x)

text ‹The negation is the unique additive inverse.›
lemma poly_minus_unique:
  assumes x: "x ∈ poly_carrier" and y: "y ∈ poly_carrier" and z: "x ⊕⇩P y = 𝟬⇩P"
  shows "y = ⊖⇩P x"
  using poly_add_left_cancel poly_add_neg_right poly_neg_closed x y z by presburger

text ‹Double negation.›
lemma poly_neg_neg:
  assumes x: "x ∈ poly_carrier" shows "⊖⇩P (⊖⇩P x) = x"
  using poly_add_neg poly_minus_unique poly_neg_closed x by presburger

text ‹Reassociation: ‹(u ⊕ a) ⊕ c = (u ⊕ c) ⊕ a› in the abelian group.›
lemma poly_add_swap_right:
  assumes u: "u ∈ poly_carrier" and a: "a ∈ poly_carrier" and c: "c ∈ poly_carrier"
  shows "(u ⊕⇩P a) ⊕⇩P c = (u ⊕⇩P c) ⊕⇩P a"
  by (metis a c poly_add_assoc poly_add_comm u)

text ‹Subtracting one equation from another: if ‹u ⊕ a = v ⊕ b› then
  ‹u ⊕ ⊖v = b ⊕ ⊖a›.›
lemma poly_sub_shift:
  assumes u: "u ∈ poly_carrier" and v: "v ∈ poly_carrier"
    and a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
    and eq: "u ⊕⇩P a = v ⊕⇩P b"
  shows "u ⊕⇩P (⊖⇩P v) = b ⊕⇩P (⊖⇩P a)"
proof -
  have nv: "⊖⇩P v ∈ poly_carrier" and na: "⊖⇩P a ∈ poly_carrier"
    using u v a b by (auto simp: poly_neg_closed)
  ― ‹Add ‹⊖v› and ‹⊖a› to both sides of ‹u ⊕ a = v ⊕ b›.›
  have "(u ⊕⇩P a) ⊕⇩P ((⊖⇩P v) ⊕⇩P (⊖⇩P a)) = (v ⊕⇩P b) ⊕⇩P ((⊖⇩P v) ⊕⇩P (⊖⇩P a))"
    using eq by simp
  ― ‹LHS reduces to ‹u ⊕ ⊖v›, RHS to ‹b ⊕ ⊖a›.›
  moreover have "(u ⊕⇩P a) ⊕⇩P ((⊖⇩P v) ⊕⇩P (⊖⇩P a)) = u ⊕⇩P (⊖⇩P v)"
    by (simp add: a na nv poly_add_assoc poly_add_closed poly_add_minus_cancel u)
  moreover have "(v ⊕⇩P b) ⊕⇩P ((⊖⇩P v) ⊕⇩P (⊖⇩P a)) = b ⊕⇩P (⊖⇩P a)"
    by (metis b na nv poly_add_assoc poly_add_closed poly_add_minus_cancel v)
  ultimately show ?thesis by simp
qed

text ‹If ‹x ⊕ ⊖y = 𝟬› then @{term "x = y"}.›
lemma poly_diff_zero_eq:
  assumes "x ∈ poly_carrier" and "y ∈ poly_carrier" and "x ⊕⇩P (⊖⇩P y) = 𝟬⇩P"
  shows "x = y"
  by (metis poly_add_comm poly_add_minus_cancel poly_add_zero poly_zero_closed assms)


subsection ‹Multiplicative unit›

lemma poly_mult_one_left:
  assumes p: "p ∈ poly_carrier"
  shows "𝟭⇩P ⊗⇩P p = p"
proof
  fix k
  have "(𝟭⇩P ⊗⇩P p) k = additive.fincomp (λi. 𝟭⇩P i ⋅ p (k - i)) {..k}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp (λj. if j = 0 then (λ_. p k) j else 𝟬) {..k}"
    using p by (intro additive.fincomp_cong') (auto simp: poly_one_def poly_carrier_coeff_closed)
  also have "… = p k"
    using p by (simp add: additive.fincomp_singleton_swap poly_carrier_coeff_closed)
  finally show "(𝟭⇩P ⊗⇩P p) k = p k" .
qed

lemma poly_mult_one_right:
  assumes p: "p ∈ poly_carrier"
  shows "p ⊗⇩P 𝟭⇩P = p"
proof
  fix k
  have "(p ⊗⇩P 𝟭⇩P) k = additive.fincomp (λi. p i ⋅ 𝟭⇩P (k - i)) {..k}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp (λj. if j = k then (λ_. p k) j else 𝟬) {..k}"
    using p by (intro additive.fincomp_cong') (auto simp: poly_one_def poly_carrier_coeff_closed)
  also have "… = p k"
    using p by (simp add: additive.fincomp_singleton_swap poly_carrier_coeff_closed)
  finally show "(p ⊗⇩P 𝟭⇩P) k = p k" .
qed


subsection ‹Distributivity›

lemma poly_mult_add_distrib_left:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
  shows "p ⊗⇩P (q ⊕⇩P r) = (p ⊗⇩P q) ⊕⇩P (p ⊗⇩P r)"
proof
  fix k
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R" and ri: "⋀i. r i ∈ R"
    using p q r by (auto simp: poly_carrier_coeff_closed)
  have "(p ⊗⇩P (q ⊕⇩P r)) k = additive.fincomp (λi. p i ⋅ (q (k - i) + r (k - i))) {..k}"
    by (simp add: poly_mult_def poly_add_def)
  also have "… = additive.fincomp (λi. p i ⋅ q (k - i) + p i ⋅ r (k - i)) {..k}"
    using distributive(1) pi qi ri by presburger
  also have "… = additive.fincomp (λi. p i ⋅ q (k - i)) {..k}
                  + additive.fincomp (λi. p i ⋅ r (k - i)) {..k}"
    by (rule additive.fincomp_comp) (use pi qi ri in auto)
  also have "… = ((p ⊗⇩P q) ⊕⇩P (p ⊗⇩P r)) k"
    by (simp add: poly_mult_def poly_add_def)
  finally show "(p ⊗⇩P (q ⊕⇩P r)) k = ((p ⊗⇩P q) ⊕⇩P (p ⊗⇩P r)) k" .
qed

lemma poly_mult_add_distrib_right:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
  shows "(q ⊕⇩P r) ⊗⇩P p = (q ⊗⇩P p) ⊕⇩P (r ⊗⇩P p)"
proof
  fix k
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R" and ri: "⋀i. r i ∈ R"
    using p q r by (auto simp: poly_carrier_coeff_closed)
  have "((q ⊕⇩P r) ⊗⇩P p) k = additive.fincomp (λi. (q i + r i) ⋅ p (k - i)) {..k}"
    by (simp add: poly_mult_def poly_add_def)
  also have "… = additive.fincomp (λi. q i ⋅ p (k - i) + r i ⋅ p (k - i)) {..k}"
    using distributive(2) pi qi ri by presburger
  also have "… = additive.fincomp (λi. q i ⋅ p (k - i)) {..k}
                  + additive.fincomp (λi. r i ⋅ p (k - i)) {..k}"
    by (rule additive.fincomp_comp) (use pi qi ri in auto)
  also have "… = ((q ⊗⇩P p) ⊕⇩P (r ⊗⇩P p)) k"
    by (simp add: poly_mult_def poly_add_def)
  finally show "((q ⊕⇩P r) ⊗⇩P p) k = ((q ⊗⇩P p) ⊕⇩P (r ⊗⇩P p)) k" .
qed


subsection ‹A Fubini law for the additive finite sum›

text ‹A nested additive sum equals the sum over the dependent product (Sigma) of the index
  sets: ‹∑i∈I. ∑j∈A i. g i j  =  ∑(i,j)∈Sigma I A. g i j›.›
lemma fincomp_Sigma:
  assumes I: "finite I" and A: "⋀i. i ∈ I ⟹ finite (A i)"
    and g: "⋀i j. i ∈ I ⟹ j ∈ A i ⟹ g i j ∈ R"
  shows "additive.fincomp (λi. additive.fincomp (g i) (A i)) I
         = additive.fincomp (λp. g (fst p) (snd p)) (Sigma I A)"
proof -
  have disj: "pairwise (λi j. disjnt ({i} × A i) ({j} × A j)) I"
    by (auto simp: pairwise_def disjnt_def)
  have "additive.fincomp (λp. g (fst p) (snd p)) (Sigma I A)
        = additive.fincomp (λp. g (fst p) (snd p)) (⋃i∈I. {i} × A i)"
    by (simp add: Sigma_def)
  also have "… = additive.fincomp (λi. additive.fincomp (λp. g (fst p) (snd p)) ({i} × A i)) I"
    using A I by (intro additive.fincomp_UN_disjoint disj g) auto
  also have "… = additive.fincomp (λi. additive.fincomp (g i) (A i)) I"
  proof (rule additive.fincomp_cong')
    fix i assume i: "i ∈ I"
    have "{i} × A i = Pair i ` A i" by auto
    then have "additive.fincomp (λp. g (fst p) (snd p)) ({i} × A i)
          = additive.fincomp (λp. g (fst p) (snd p)) (Pair i ` A i)"
      by simp
    also have "… = additive.fincomp (λj. g (fst (Pair i j)) (snd (Pair i j))) (A i)"
    proof (rule additive.fincomp_reindex)
      show "(λp. g (fst p) (snd p)) ∈ Pair i ` A i → R" using i g by auto
      show "inj_on (Pair i) (A i)" by (simp add: inj_on_def)
    qed
    also have "… = additive.fincomp (g i) (A i)" by simp
    finally show "additive.fincomp (λp. g (fst p) (snd p)) ({i} × A i)
                    = additive.fincomp (g i) (A i)" .
  qed (use I A g additive.fincomp_closed in auto)
  finally show ?thesis ..
qed


subsection ‹Associativity of convolution›

lemma poly_mult_assoc:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
  shows "(p ⊗⇩P q) ⊗⇩P r = p ⊗⇩P (q ⊗⇩P r)"
proof
  fix n
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R" and ri: "⋀i. r i ∈ R"
    using p q r by (auto simp: poly_carrier_coeff_closed)
  ― ‹LHS as a sum over the triangle @{text "{(j,i). i ≤ j ≤ n}"}.›
  have "((p ⊗⇩P q) ⊗⇩P r) n
        = additive.fincomp (λj. additive.fincomp (λi. p i ⋅ q (j - i)) {..j} ⋅ r (n - j)) {..n}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp
                    (λj. additive.fincomp (λi. (p i ⋅ q (j - i)) ⋅ r (n - j)) {..j}) {..n}"
    using pi qi ri
    by (intro additive.fincomp_cong' fincomp_mult_distrib_right) auto
  also have "… = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (n - fst x))
                    (Sigma {..n} (λj. {..j}))"
    by (rule fincomp_Sigma) (use pi qi ri in auto)
  finally have LHS: "((p ⊗⇩P q) ⊗⇩P r) n
        = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (n - fst x))
            (Sigma {..n} (λj. {..j}))" .
  ― ‹RHS as a sum over the triangle @{text "{(i,j). j ≤ n - i}"}.›
  have "(p ⊗⇩P (q ⊗⇩P r)) n
        = additive.fincomp (λi. p i ⋅ additive.fincomp (λj. q j ⋅ r (n - i - j)) {..n - i}) {..n}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp
                    (λi. additive.fincomp (λj. p i ⋅ (q j ⋅ r (n - i - j))) {..n - i}) {..n}"
    using pi qi ri
    by (intro additive.fincomp_cong' fincomp_mult_distrib_left) auto
  also have "… = additive.fincomp (λx. p (fst x) ⋅ (q (snd x) ⋅ r (n - fst x - snd x)))
                    (Sigma {..n} (λi. {..n - i}))"
    by (rule fincomp_Sigma) (use pi qi ri in auto)
  finally have RHS: "(p ⊗⇩P (q ⊗⇩P r)) n
        = additive.fincomp (λx. p (fst x) ⋅ (q (snd x) ⋅ r (n - fst x - snd x)))
            (Sigma {..n} (λi. {..n - i}))" .
  ― ‹Reindex the LHS triangle to the RHS triangle by @{text "(j,i) ↦ (i, j - i)"}.›
  let ?h = "λx::nat×nat. (snd x, fst x - snd x)"
  let ?h' = "λx::nat×nat. (fst x + snd x, fst x)"
  have bij: "bij_betw ?h (Sigma {..n} (λj. {..j})) (Sigma {..n} (λi. {..n - i}))"
    by (rule bij_betw_byWitness[where f' = ?h']) auto
  let ?F = "λx. p (fst x) ⋅ (q (snd x) ⋅ r (n - fst x - snd x))"
  have "additive.fincomp ?F (Sigma {..n} (λi. {..n - i}))
        = additive.fincomp ?F (?h ` Sigma {..n} (λj. {..j}))"
    using bij bij_betw_imp_surj_on by fastforce
  also have "… = additive.fincomp (λx. ?F (?h x)) (Sigma {..n} (λj. {..j}))"
  proof (rule additive.fincomp_reindex)
    show "?F ∈ ?h ` Sigma {..n} (λj. {..j}) → R" using pi qi ri by auto
    show "inj_on ?h (Sigma {..n} (λj. {..j}))"
      using bij bij_betw_imp_inj_on by blast
  qed
  also have "… = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ r (n - fst x))
                    (Sigma {..n} (λj. {..j}))"
    using pi qi ri multiplicative.associative
    by (intro additive.fincomp_cong') auto
  finally show "((p ⊗⇩P q) ⊗⇩P r) n = (p ⊗⇩P (q ⊗⇩P r)) n"
    using LHS RHS by simp
qed


subsection ‹Coefficients, degree, monomials, constants, and the variable›

text ‹The coefficient map is just function application (kept as a named operation to mirror
  the HOL-Algebra polynomial interface).›
definition coeff :: "(nat ⇒ 'a) ⇒ nat ⇒ 'a"
  where "coeff p = p"

lemma coeff_eq [simp]: "coeff p i = p i"
  by (simp add: coeff_def)

text ‹The degree is the greatest index with a nonzero coefficient (and @{term 0} for the zero
  polynomial, as is conventional here).›
definition degree :: "(nat ⇒ 'a) ⇒ nat"
  where "degree p ≡ (if {i. p i ≠ 𝟬} = {} then 0 else Max {i. p i ≠ 𝟬})"

lemma degree_zero [simp]: "degree 𝟬⇩P = 0"
  by (simp add: degree_def poly_zero_def)

lemma coeff_gt_degree:
  assumes "p ∈ poly_carrier" and "degree p < i"
  shows "p i = 𝟬"
proof (rule ccontr)
  assume "p i ≠ 𝟬"
  then have §: "{i. p i ≠ 𝟬} ≠ {}" by blast
  moreover have "finite {i. p i ≠ 𝟬}" using assms(1) by (rule poly_carrier_finite)
  ultimately have "i ≤ Max {i. p i ≠ 𝟬}" using ‹p i ≠ 𝟬› by simp
  then show False using assms(2)
    by (metis § degree_def linorder_not_le)
qed

text ‹A degree bound: @{term "degree p ≤ n"} exactly when all coefficients above @{term n}
  vanish (for a polynomial, whose support is finite).›
lemma degree_le_iff:
  assumes "p ∈ poly_carrier"
  shows "degree p ≤ n ⟷ (∀i>n. p i = 𝟬)"
proof
  assume "degree p ≤ n"
  then show "∀i>n. p i = 𝟬" using coeff_gt_degree[OF assms] by force
next
  assume *: "∀i>n. p i = 𝟬"
  show "degree p ≤ n"
    using "*" assms degree_def linorder_le_less_linear poly_carrier_finite by force
qed

lemma degree_leI:
  "⟦ p ∈ poly_carrier; ⋀i. i > n ⟹ p i = 𝟬 ⟧ ⟹ degree p ≤ n"
  by (simp add: degree_le_iff)

text ‹Negation preserves the support, hence the degree (for carrier polynomials).›
lemma degree_neg:
  assumes p: "p ∈ poly_carrier" shows "degree (⊖⇩P p) = degree p"
proof -
  have "⋀x. (⊖⇩P p) x = 𝟬 ⟹ p x = 𝟬"
    by (metis additive.inverse_unit p poly_neg_def poly_neg_neg)
  then have "{i. (⊖⇩P p) i ≠ 𝟬} = {i. p i ≠ 𝟬}"
    by (metis additive.inverse_unit poly_neg_def)
  then show ?thesis by (simp add: degree_def)
qed


subsection ‹Polynomials of bounded degree›

text ‹The polynomials supported on @{text "{..<n}"} --- those of degree below @{term n}, together
  with the zero polynomial.  These are exactly the carrier polynomials whose coefficients vanish
  from index @{term n} on.  When the coefficient ring is finite, there are @{text "¦R¦⇧n"} of them;
  they serve as the canonical representatives of @{text "F[X]/(b)"} for @{term b} of degree
  @{term n}.›
definition low_poly :: "nat ⇒ (nat ⇒ 'a) set"
  where "low_poly n ≡ {p. p ∈ poly_carrier ∧ (∀i≥n. p i = 𝟬)}"

lemma low_polyI:
  "⟦ p ∈ poly_carrier; ⋀i. i ≥ n ⟹ p i = 𝟬 ⟧ ⟹ p ∈ low_poly n"
  unfolding low_poly_def by blast

lemma low_poly_closed: "p ∈ low_poly n ⟹ p ∈ poly_carrier"
  unfolding low_poly_def by blast

lemma low_poly_coeff: "⟦ p ∈ low_poly n; i ≥ n ⟧ ⟹ p i = 𝟬"
  unfolding low_poly_def by blast
― ‹@{thm [source] low_poly_coeff} and @{thm [source] low_poly_closed} must ∗‹not› go into a simpset.›

text ‹The low-degree polynomials form a subgroup of the additive group, and this is immediate
  ∗‹coefficientwise›: the operations are pointwise, so no reasoning about degrees is needed.›

lemma low_poly_zero [simp]: "𝟬⇩P ∈ low_poly n"
  using low_polyI poly_zero_closed poly_zero_def by force

lemma low_poly_add_closed:
  assumes p: "p ∈ low_poly n" and q: "q ∈ low_poly n" shows "p ⊕⇩P q ∈ low_poly n"
proof (rule low_polyI)
  have pc: "p ∈ poly_carrier" and qc: "q ∈ poly_carrier"
    using p q by (blast intro: low_poly_closed)+
  show "p ⊕⇩P q ∈ poly_carrier" using pc qc by (rule poly_add_closed)
next
  fix i assume i: "n ≤ i"
  have "p i = 𝟬" and "q i = 𝟬"
    using low_poly_coeff [OF p i] low_poly_coeff [OF q i] by blast+
  then show "(p ⊕⇩P q) i = 𝟬"
    by (simp add: poly_add_def additive.left_unit)
qed

lemma low_poly_neg_closed:
  assumes p: "p ∈ low_poly n" shows "⊖⇩P p ∈ low_poly n"
  using additive.inverse_unit low_polyI low_poly_closed low_poly_coeff p poly_neg_closed poly_neg_def
  by metis

lemma low_poly_one:
  assumes n: "0 < n" shows "𝟭⇩P ∈ low_poly n"
  using low_polyI n poly_one_closed poly_one_def by force

text ‹Membership of @{const low_poly} in terms of degree: a carrier polynomial lies in
  @{term "low_poly n"} iff it is zero or has degree below @{term n}.›
lemma low_poly_iff_degree:
  assumes p: "p ∈ poly_carrier"
  shows "p ∈ low_poly n ⟷ (p = 𝟬⇩P ∨ degree p < n)"
proof
  assume "p ∈ low_poly n"
  then have z: "⋀i. i ≥ n ⟹ p i = 𝟬" unfolding low_poly_def by blast
  show "p = 𝟬⇩P ∨ degree p < n"
  proof (cases "p = 𝟬⇩P")
    case False
    ― ‹The support is finite and nonempty, so its maximum @{term "degree p"} lies in it.›
    have fin: "finite {i. p i ≠ 𝟬}" using p by (rule poly_carrier_finite)
    have ne: "{i. p i ≠ 𝟬} ≠ {}" using False by (auto simp: poly_zero_def fun_eq_iff)
    then show ?thesis
      by (metis (mono_tags, lifting) Max_in degree_def fin leI mem_Collect_eq z)
  qed simp
next
  assume "p = 𝟬⇩P ∨ degree p < n"
  then show "p ∈ low_poly n"
    using coeff_gt_degree low_polyI poly_zero_def p by auto
qed

text ‹Restricting a low-degree polynomial to @{text "{..<n}"} is a bijection onto the coefficient
  vectors @{text "{..<n} →⇩E R"}; the inverse extends a vector by zero.›
lemma bij_low_poly_PiE:
  "bij_betw (λp. restrict p {..<n}) (low_poly n) ({..<n} →⇩E R)"
proof (rule bij_betw_byWitness[where f' = "λf i. if i < n then f i else 𝟬"])
  show "∀p∈low_poly n. (λi. if i < n then restrict p {..<n} i else 𝟬) = p"
    by (auto simp: low_poly_def not_less)
  show "∀f∈{..<n} →⇩E R. restrict (λi. if i < n then f i else 𝟬) {..<n} = f"
    by (auto simp: restrict_def PiE_def extensional_def fun_eq_iff)
  show "(λp. restrict p {..<n}) ` low_poly n ⊆ {..<n} →⇩E R"
    using low_poly_closed poly_carrier_coeff_closed by force
  show "(λf i. if i < n then f i else 𝟬) ` ({..<n} →⇩E R) ⊆ low_poly n"
  proof
    fix p assume "p ∈ (λf i. if i < n then f i else 𝟬) ` ({..<n} →⇩E R)"
    then obtain f where f: "f ∈ {..<n} →⇩E R" and pf: "p = (λi. if i < n then f i else 𝟬)" by blast
    have "p ∈ poly_carrier"
      using f by (intro poly_carrierI) (auto simp: pf)
    then show "p ∈ low_poly n" using pf by (auto intro!: low_polyI)
  qed
qed

text ‹Hence, over a finite coefficient ring, there are exactly @{text "¦R¦⇧n"} polynomials of
  degree below @{term n}.›
theorem card_low_poly:
  assumes "finite R" shows "card (low_poly n) = card R ^ n"
  using bij_betw_same_card [OF bij_low_poly_PiE] by (simp add: card_PiE)

text ‹The constant polynomial with value @{term a}.›
definition poly_const :: "'a ⇒ (nat ⇒ 'a)"
  where "poly_const a = (λi. if i = 0 then a else 𝟬)"

lemma poly_const_closed: "a ∈ R ⟹ poly_const a ∈ poly_carrier"
  by (simp add: poly_carrier_def poly_const_def)

lemma poly_const_zero [simp]: "poly_const 𝟬 = 𝟬⇩P"
  by (simp add: poly_const_def poly_zero_def)

lemma poly_const_one [simp]: "poly_const 𝟭 = 𝟭⇩P"
  by (simp add: poly_const_def poly_one_def)

text ‹The monomial @{text "a X⇧n"}: the coefficient @{term a} at degree @{term n}.›
definition monom :: "'a ⇒ nat ⇒ (nat ⇒ 'a)"
  where "monom a n = (λi. if i = n then a else 𝟬)"

lemma monom_closed: "a ∈ R ⟹ monom a n ∈ poly_carrier"
  by (simp add: monom_def poly_carrier_def)

lemma monom_0_eq_const: "monom a 0 = poly_const a"
  by (simp add: monom_def poly_const_def)

text ‹The variable @{text X} is the monomial @{text "𝟭 X⇧1"}.›
definition var :: "nat ⇒ 'a"  (‹X⇩P›)
  where "var = monom 𝟭 1"

lemma var_closed: "X⇩P ∈ poly_carrier"
  by (simp add: var_def monom_closed)

lemma coeff_var: "X⇩P i = (if i = 1 then 𝟭 else 𝟬)"
  by (simp add: var_def monom_def)

text ‹Multiplying by a monomial @{text "monom c k"} shifts coefficients up by @{term k} and
  scales by @{term c}: @{text "(monom c k ⊗ b) j = (if k ≤ j then c ⋅ b (j - k) else 𝟬)"}.›
lemma coeff_monom_mult:
  assumes c: "c ∈ R" and b: "b ∈ poly_carrier"
  shows "(monom c k ⊗⇩P b) j = (if k ≤ j then c ⋅ b (j - k) else 𝟬)"
proof -
  have bi: "⋀i. b i ∈ R" using b by (simp add: poly_carrier_coeff_closed)
  have "(monom c k ⊗⇩P b) j = additive.fincomp (λi. monom c k i ⋅ b (j - i)) {..j}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp (λi. if i = k then c ⋅ b (j - k) else 𝟬) {..j}"
    by (rule additive.fincomp_cong') (use c bi in ‹auto simp: monom_def›)
  finally have eq: "(monom c k ⊗⇩P b) j
                    = additive.fincomp (λi. if i = k then c ⋅ b (j - k) else 𝟬) {..j}" .
  show ?thesis
  proof (cases "k ≤ j")
    case True
    then have "k ∈ {..j}" by simp
    have "additive.fincomp (λi. if i = k then (λ_. c ⋅ b (j - k)) i else 𝟬) {..j}
            = (λ_. c ⋅ b (j - k)) k"
      by (rule additive.fincomp_singleton_swap[OF ‹k ∈ {..j}›]) (use c bi in auto)
    then show ?thesis using eq True by simp
  next
    case False
    then have "⋀i. i ∈ {..j} ⟹ (if i = k then c ⋅ b (j - k) else 𝟬) = 𝟬" by auto
    then show ?thesis using eq False
      by (smt (verit) additive.fincomp_unit_eqI)
  qed
qed

text ‹Degrees of the basic polynomials›

text ‹Multiplying a monomial by the variable raises its exponent, and multiplying by a constant
  scales its coefficient.›

lemma var_mult_monom:
  assumes a: "a ∈ R" shows "X⇩P ⊗⇩P monom a k = monom a (Suc k)"
proof
  fix j
  have "(X⇩P ⊗⇩P monom a k) j = (if Suc 0 ≤ j then 𝟭 ⋅ monom a k (j - Suc 0) else 𝟬)"
    by (simp add: var_def coeff_monom_mult [OF _ monom_closed [OF a]])
  then show "(X⇩P ⊗⇩P monom a k) j = monom a (Suc k) j" 
    using a by (auto simp: monom_def)
qed

text ‹A monomial is zero exactly when its coefficient is zero.›
lemma monom_eq_zero_iff [simp]: "monom a n = 𝟬⇩P ⟷ a = 𝟬"
  by (auto simp: monom_def poly_zero_def fun_eq_iff)

lemma degree_monom:
  assumes "a ≠ 𝟬"
  shows "degree (monom a n) = n"
  using assms by (auto simp: monom_def degree_def)

lemma degree_monom_le: "degree (monom a n) ≤ n"
  using degree_monom degree_zero monom_eq_zero_iff by (metis dual_order.refl le0)

lemma degree_poly_const:
  assumes "a ≠ 𝟬"
  shows "degree (poly_const a) = 0"
  using degree_monom[OF assms, of 0] by (simp add: monom_0_eq_const)

lemma degree_const_le: "degree (poly_const a) ≤ 0"
  using degree_monom_le[of a 0] by (simp add: monom_0_eq_const)

lemma degree_one [simp]: "degree 𝟭⇩P = 0"
  using degree_const_le[of 𝟭] by simp

text ‹In a nontrivial coefficient ring, the variable has degree one.  The explicit hypothesis
  keeps this lemma available in the more general @{locale Ring} context above.›
lemma degree_var:
  assumes "𝟭 ≠ 𝟬"
  shows "degree X⇩P = 1"
  by (simp add: assms degree_monom var_def)

text ‹The product of two constants is the constant of the product.›
lemma poly_const_add:
  assumes a: "a ∈ R" and b: "b ∈ R"
  shows "poly_const a ⊕⇩P poly_const b = poly_const (a + b)"
  using poly_add_def poly_const_def by fastforce

lemma poly_const_mult:
  assumes a: "a ∈ R" and b: "b ∈ R"
  shows "poly_const a ⊗⇩P poly_const b = poly_const (a ⋅ b)"
proof
  fix j
  show "(poly_const a ⊗⇩P poly_const b) j = poly_const (a ⋅ b) j" 
    using coeff_monom_mult[OF a poly_const_closed[OF b], of 0] a
    by (simp add: monom_0_eq_const poly_const_def)
qed

text ‹A polynomial of degree @{text 0} is the constant given by its zeroth coefficient.›
lemma degree_zero_imp_const:
  assumes "p ∈ poly_carrier" "degree p = 0"
  shows "p = poly_const (p 0)"
  using assms coeff_gt_degree poly_const_def by auto

lemma degree_add_le:
  assumes "p ∈ poly_carrier" "q ∈ poly_carrier"
  shows "degree (p ⊕⇩P q) ≤ max (degree p) (degree q)"
proof (intro degree_leI poly_add_closed assms)
qed (simp add: assms coeff_gt_degree poly_add_def)


text ‹Multiplication by the zero polynomial.›
lemma
  assumes "p ∈ poly_carrier" 
  shows poly_mult_zero_right: "p ⊗⇩P 𝟬⇩P = 𝟬⇩P"
    and poly_mult_zero_left: "𝟬⇩P ⊗⇩P p = 𝟬⇩P"
  using assms by (simp_all add: poly_mult_def poly_zero_def poly_carrier_coeff_closed)

text ‹The leading coefficient.›
definition lead_coeff :: "(nat ⇒ 'a) ⇒ 'a"
  where "lead_coeff p = p (degree p)"

text ‹The coefficient at the degree is nonzero for a nonzero polynomial.›
lemma coeff_degree_nonzero:
  assumes "p ∈ poly_carrier" and "p ≠ 𝟬⇩P"
  shows "p (degree p) ≠ 𝟬"
  by (metis antisym assms coeff_gt_degree less_not_refl linorder_not_le low_polyI
      low_poly_iff_degree)

lemma lead_coeff_nonzero:
  "⟦ p ∈ poly_carrier; p ≠ 𝟬⇩P ⟧ ⟹ lead_coeff p ≠ 𝟬"
  unfolding lead_coeff_def by (rule coeff_degree_nonzero)

text ‹The coefficient of a product at the sum of the two degrees is the product of the leading
  coefficients: every other term of the convolution vanishes for degree reasons.›
lemma coeff_mult_degree_add:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier"
  shows "(p ⊗⇩P q) (degree p + degree q) = p (degree p) ⋅ q (degree q)"
proof -
  let ?m = "degree p" and ?n = "degree q"
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R"
    using p q by (auto simp: poly_carrier_coeff_closed)
  have "(p ⊗⇩P q) (?m + ?n) = additive.fincomp (λi. p i ⋅ q (?m + ?n - i)) {..?m + ?n}"
    by (simp add: poly_mult_def)
  also have "… = additive.fincomp (λi. if i = ?m then p ?m ⋅ q ?n else 𝟬) {..?m + ?n}"
  proof (rule additive.fincomp_cong')
    fix i assume "i ∈ {..?m + ?n}"
    show "p i ⋅ q (?m + ?n - i) = (if i = ?m then p ?m ⋅ q ?n else 𝟬)"
    proof (cases "i = ?m")
      case False
      have "p i ⋅ q (?m + ?n - i) = 𝟬"
      proof (cases "i > ?m")
        case False
        with pi coeff_gt_degree[OF q] ‹i ≠ ?m› show ?thesis by simp
      qed (simp add: coeff_gt_degree p qi)
      then show ?thesis using False by simp
    qed auto
  qed (use pi qi in auto)
  also have "… = p ?m ⋅ q ?n"
    using additive.fincomp_singleton_swap[of ?m "{..?m + ?n}" "λ_. p ?m ⋅ q ?n"]
    using pi qi by simp
  finally show ?thesis .
qed

text ‹The degree of a product is at most the sum of the degrees.›
lemma degree_mult_le:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier"
  shows "degree (p ⊗⇩P q) ≤ degree p + degree q"
proof (rule degree_leI)
  show "p ⊗⇩P q ∈ poly_carrier" using assms by (rule poly_mult_closed)
  fix i assume i: "i > degree p + degree q"
  have "p j ⋅ q (i - j) = 𝟬" if "j ∈ {..i}" for j
    using i p q coeff_gt_degree
  proof (cases "j > degree p")
    case True
    then show ?thesis using q coeff_gt_degree[OF p]
      by (simp add: poly_carrier_coeff_closed)
  next
    case False
    then show ?thesis using p i coeff_gt_degree[OF q]
      by (simp add: poly_carrier_coeff_closed)
  qed
  then show "(p ⊗⇩P q) i = 𝟬"
    unfolding poly_mult_def by (rule additive.fincomp_unit_eqI)
qed


subsection ‹The ring structure›

theorem poly_ring: "Ring poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
proof -
  have add_grp: "Group poly_carrier (⊕⇩P) 𝟬⇩P"
  proof (rule GroupI)
    show "⋀p. p ∈ poly_carrier ⟹ p ⊕⇩P 𝟬⇩P = p"
      using poly_add_comm poly_add_zero poly_zero_closed by simp
    show "⋀p. p ∈ poly_carrier ⟹ ∃q∈poly_carrier. p ⊕⇩P q = 𝟬⇩P ∧ q ⊕⇩P p = 𝟬⇩P"
      using poly_add_neg poly_add_neg_right poly_neg_closed by blast
  qed (auto simp: poly_add_closed poly_zero_closed poly_add_assoc poly_add_zero)
  interpret add: Group poly_carrier "(⊕⇩P)" "𝟬⇩P" by (rule add_grp)
  interpret add: Abelian_Group poly_carrier "(⊕⇩P)" "𝟬⇩P"
    by unfold_locales (rule poly_add_comm)
  interpret mult: Monoid poly_carrier "(⊗⇩P)" "𝟭⇩P"
  proof 
  qed (auto simp: poly_mult_one_left poly_mult_one_right poly_mult_assoc poly_one_closed poly_mult_closed)
  show ?thesis
  proof qed (use poly_mult_add_distrib_left poly_mult_add_distrib_right in auto)
qed


subsection ‹Evaluation at a point›

text ‹Powers in the (multiplicative monoid of the) ring.  We define them locally rather than
  importing ‹Group_Action›'s ‹Monoid.power›, to keep the polynomial theory's
  dependencies minimal.›
definition rpow :: "'a ⇒ nat ⇒ 'a"
  where "rpow a n = (((⋅) a) ^^ n) 𝟭"

lemma rpow_0 [simp]: "rpow a 0 = 𝟭"
  by (simp add: rpow_def)

lemma rpow_Suc [simp]: "rpow a (Suc n) = a ⋅ rpow a n"
  by (simp add: rpow_def)

lemma rpow_closed [simp]: "a ∈ R ⟹ rpow a n ∈ R"
  by (induct n) auto

text ‹Evaluation of a polynomial at a point @{term a}: the finite sum
  @{text "∑⇘i≤degree p⇙ p i ⋅ a⇧i"}.›
definition eval :: "'a ⇒ (nat ⇒ 'a) ⇒ 'a"
  where "eval a p = additive.fincomp (λi. p i ⋅ rpow a i) {..degree p}"

text ‹Each summand lies in @{term R}, and the sum is closed.›
lemma eval_summand_closed: "⟦ p ∈ poly_carrier; a ∈ R ⟧ ⟹ p i ⋅ rpow a i ∈ R"
  by (simp add: poly_carrier_coeff_closed)

lemma eval_closed [simp]:
  assumes p: "p ∈ poly_carrier" and a: "a ∈ R" shows "eval a p ∈ R"
  unfolding eval_def using p a by (auto intro!: additive.fincomp_closed eval_summand_closed)

text ‹The summation range may be enlarged past the degree: the extra coefficients vanish.›
lemma eval_fincomp_le:
  assumes p: "p ∈ poly_carrier" and a: "a ∈ R" and n: "degree p ≤ n"
  shows "eval a p = additive.fincomp (λi. p i ⋅ rpow a i) {..n}"
proof -
  have fin: "⋀i. p i ⋅ rpow a i ∈ R" using p a by (rule eval_summand_closed)
  have split: "{..n} = {..degree p} ∪ {Suc (degree p)..n}" using n by auto
  have disj: "{..degree p} ∩ {Suc (degree p)..n} = {}" by auto
  have "additive.fincomp (λi. p i ⋅ rpow a i) {..n}
        = additive.fincomp (λi. p i ⋅ rpow a i) {..degree p}
          + additive.fincomp (λi. p i ⋅ rpow a i) {Suc (degree p)..n}"
    using fin by (simp add: split additive.fincomp_Un_disjoint[OF _ _ disj])
  also have "additive.fincomp (λi. p i ⋅ rpow a i) {Suc (degree p)..n} = 𝟬"
    using a coeff_gt_degree[OF p] by (auto intro: additive.fincomp_unit_eqI)
  finally show ?thesis
    unfolding eval_def using fin by (simp add: additive.fincomp_closed)
qed

text ‹Evaluation of the basic polynomials.›
lemma eval_zero [simp]: "a ∈ R ⟹ eval a 𝟬⇩P = 𝟬"
  by (simp add: eval_def poly_zero_def)

lemma eval_const [simp]:
  assumes a: "a ∈ R" and c: "c ∈ R" shows "eval a (poly_const c) = c"
  unfolding eval_def
  by (simp add: degree_def poly_const_def) (use c in ‹simp add: poly_const_def›)

lemma eval_one [simp]: "a ∈ R ⟹ eval a 𝟭⇩P = 𝟭"
  using eval_const[of a 𝟭] by simp

text ‹Evaluation is additive.›
lemma eval_add:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier" and a: "a ∈ R"
  shows "eval a (p ⊕⇩P q) = eval a p + eval a q"
proof -
  define n where "n ≡ max (degree p) (degree q)"
  have pq: "p ⊕⇩P q ∈ poly_carrier" using p q by (rule poly_add_closed)
  have dpq: "degree (p ⊕⇩P q) ≤ n" unfolding n_def using degree_add_le[OF p q] .
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R" using p q by (auto simp: poly_carrier_coeff_closed)
  have "eval a (p ⊕⇩P q) = additive.fincomp (λi. (p i + q i) ⋅ rpow a i) {..n}"
    using eval_fincomp_le[OF pq a dpq] by (simp add: poly_add_closed poly_add_def)
  also have "… = additive.fincomp (λi. p i ⋅ rpow a i) {..n}
                  + additive.fincomp (λi. q i ⋅ rpow a i) {..n}"
    by (simp add: a additive.fincomp_comp distributive(2) pi qi)
  also have "… = eval a p + eval a q"
    by (metis (lifting) a eval_fincomp_le max.cobounded1 max.cobounded2 n_def p q)
  finally show ?thesis .
qed

text ‹Evaluation of a monomial @{term "monom c k"} is @{text "c ⋅ a⇧k"}.›
lemma eval_monom:
  assumes c: "c ∈ R" and a: "a ∈ R"
  shows "eval a (monom c k) = c ⋅ rpow a k"
proof -
  have "eval a (monom c k) = additive.fincomp (λi. monom c k i ⋅ rpow a i) {..k}"
    using a c degree_monom_le eval_fincomp_le monom_closed by blast
  also have "… = additive.fincomp (λi. if i = k then c ⋅ rpow a k else 𝟬) {..k}"
    by (rule additive.fincomp_cong') (use c a in ‹auto simp: monom_def›)
  also have "… = c ⋅ rpow a k"
    using additive.fincomp_singleton_swap[of k "{..k}" "λi. c ⋅ rpow a k"] c a by simp
  finally show ?thesis .
qed

text ‹Evaluation of the variable @{term "X⇩P"} returns the point itself.›
lemma poly_rpow_var: "Ring.rpow (⊗⇩P) 𝟭⇩P X⇩P k = monom 𝟭 k"
proof (induct k)
  case 0
  show ?case
    using Ring.rpow_0 [OF poly_ring, of X⇩P] monom_0_eq_const [of 𝟭] by simp
next
  case (Suc k) then show ?case
    using multiplicative.unit_closed poly_ring var_mult_monom by (metis Ring.rpow_Suc)
qed

lemma poly_const_mult_monom:
  assumes c: "c ∈ R" shows "poly_const c ⊗⇩P monom 𝟭 k = monom c k"
proof
  fix j
  have "(poly_const c ⊗⇩P monom 𝟭 k) j = c ⋅ monom 𝟭 k j"
    using coeff_monom_mult [OF c monom_closed] by (simp flip: monom_0_eq_const)
  then show "(poly_const c ⊗⇩P monom 𝟭 k) j = monom c k j" 
    using c by (simp add: monom_def)
qed

text ‹∗‹Expanding a polynomial into its monomials.›  Sums in the polynomial ring are pointwise, so
  a finite composite may be read coefficientwise, and then only the monomial whose exponent matches
  the coefficient index survives.  This is the univariate counterpart of the closed form
  ‹ieval_ivar› in ‹Indexed_Poly›, and it is what identifies evaluation of a polynomial's
  constant lift at the variable with the polynomial itself.›

lemma poly_add_cmonoid: "commutative_monoid poly_carrier (⊕⇩P) 𝟬⇩P"
  using poly_ring by (meson Abelian_Group_def Ring_def)

lemma poly_fincomp_apply:
  assumes f: "⋀k. f k ∈ poly_carrier"
  shows "commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P f A j
       = additive.fincomp (λk. f k j) A"
proof (cases "finite A")
  case False then show ?thesis
    using commutative_monoid.fincomp_infinite poly_add_cmonoid poly_zero_def by fastforce
next
  case True
  then show ?thesis
  proof (induction A rule: finite_induct)
    case empty
    then show ?case
      using additive.fincomp_empty poly_add_cmonoid poly_zero_def
      by (metis commutative_monoid.fincomp_empty)
  next
    case (insert a A)
    have fA: "f ∈ A → poly_carrier" and fa: "f a ∈ poly_carrier" using f by auto
    have "commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P f (insert a A) j
        = f a j + commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P f A j"
      by (simp add: commutative_monoid.fincomp_insert f insert.hyps poly_add_cmonoid poly_add_def)
    also have "… = f a j + additive.fincomp (λk. f k j) A" using insert.IH by simp
    also have "… = additive.fincomp (λk. f k j) (insert a A)"
      by (simp add: f insert.hyps poly_carrier_coeff_closed)
    finally show ?case .
  qed
qed

lemma poly_sum_monom:
  assumes q: "q ∈ poly_carrier" and n: "degree q ≤ n"
  shows "commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P (λk. monom (q k) k) {..n} = q"
proof 
  fix j
  have cl: "monom (q k) k ∈ poly_carrier" for k
    using q by (simp add: monom_closed poly_carrier_coeff_closed)
  have qjR: "q j ∈ R" by (rule poly_carrier_coeff_closed [OF q])
  have "commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P (λk. monom (q k) k) {..n} j
        = additive.fincomp (λk. monom (q k) k j) {..n}"
    by (rule poly_fincomp_apply [OF cl])
  also have "… = additive.fincomp (λk. if k = j then (λ_. q j) k else 𝟬) {..n}"
    using qjR monom_def by (intro additive.fincomp_cong') auto
  also have "… = q j"
  proof (cases "j ≤ n")
    case True
    with qjR show ?thesis
      by (intro additive.fincomp_singleton_swap) auto
  next
    case False
    have "(if k = j then (λ_. q j) k else 𝟬) = 𝟬" if "k ∈ {..n}" for k
      using False that by auto
    moreover have "q j = 𝟬" using False n by (intro coeff_gt_degree [OF q]) simp
    ultimately show ?thesis
      using additive.fincomp_unit_eqI by fastforce
  qed
  finally show "commutative_monoid.fincomp poly_carrier (⊕⇩P) 𝟬⇩P (λk. monom (q k) k) {..n} j
                = q j" .
qed

text ‹∗‹A polynomial is the value of its own constant lift at the variable.›  Evaluating in the
  polynomial ring itself, with each coefficient embedded as a constant and the point taken to be
  @{term "X⇩P"}, returns the polynomial.  Composing this with the reduction homomorphism is what
  identifies the class of @{term q} with the value of @{term q} at the adjoined root.›
lemma eval_const_lift_at_var:
  assumes q: "q ∈ poly_carrier"
  shows "Ring.eval poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P X⇩P (λk. poly_const (q k)) = q"
proof -
  have coeffR: "q k ∈ R" for k using q by (rule poly_carrier_coeff_closed)
  have supp: "{k. poly_const (q k) ≠ 𝟬⇩P} = {k. q k ≠ 𝟬}"
    by (auto simp: poly_const_def poly_zero_def fun_eq_iff)
  have lift: "(λk. poly_const (q k)) ∈ Ring.poly_carrier poly_carrier 𝟬⇩P"
    using poly_carrier_finite [OF q] supp
    using coeffR poly_const_closed poly_ring by (metis Ring.poly_carrierI) 
  have deg: "Ring.degree 𝟬⇩P (λk. poly_const (q k)) = degree q"
    using Ring.degree_def [OF poly_ring, of "λk. poly_const (q k)"] supp
    by (simp add: degree_def)
  have "poly_const (q k) ⊗⇩P Ring.rpow (⊗⇩P) 𝟭⇩P X⇩P k = monom (q k) k" for k
    using poly_rpow_var [of k] poly_const_mult_monom [OF coeffR, of k] by simp
  then show ?thesis 
    using Ring.eval_def [OF poly_ring] poly_sum_monom [OF q order_refl]
    by (simp add: deg)
qed

lemma eval_var [simp]: "a ∈ R ⟹ eval a X⇩P = a"
  using eval_monom[of 𝟭 a 1] by (simp add: var_def)

text ‹Powers add exponents.›
lemma rpow_add: "a ∈ R ⟹ rpow a (i + j) = rpow a i ⋅ rpow a j"
  by (induct i) (auto simp: multiplicative.associative)

end

subsection ‹Evaluation along a ring homomorphism›

text ‹Evaluating in the target, at the image of the point and with the images of the coefficients,
  gives the image of the evaluation.  Powers transport by induction on the exponent and the sum by
  @{thm [source] fincomp_hom}; the summation range is the only thing that does not come for free, so
  the equality of the two degrees is taken as a hypothesis..›
lemma eval_hom:
  fixes A :: "'b set" and add mult :: "'b ⇒ 'b ⇒ 'b" and z u :: 'b
    and B :: "'c set" and badd bmult :: "'c ⇒ 'c ⇒ 'c" and bz bu :: 'c
    and h :: "'b ⇒ 'c"
  assumes RA: "Ring A add mult z u" and RB: "Ring B badd bmult bz bu"
    and hB: "⋀y. y ∈ A ⟹ h y ∈ B"
    and hz: "h z = bz" and hu: "h u = bu"
    and hadd: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (add y y') = badd (h y) (h y')"
    and hmult: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (mult y y') = bmult (h y) (h y')"
    and x: "x ∈ A" and p: "⋀k. p k ∈ A"
    and deg: "Ring.degree bz (λk. h (p k)) = Ring.degree z p"
  shows "Ring.eval B badd bmult bz bu (h x) (λk. h (p k)) = h (Ring.eval A add mult z u x p)"
proof -
  have cmA: "commutative_monoid A add z" using RA by (simp add: Ring_def Abelian_Group_def)
  have cmB: "commutative_monoid B badd bz" using RB by (simp add: Ring_def Abelian_Group_def)
  have MonM: "Monoid A mult u" using RA by (simp add: Ring_def)
  have rp: "Ring.rpow bmult bu (h x) n = h (Ring.rpow mult u x n)" for n
  proof (induct n)
    case 0
    show ?case using hu by (simp add: Ring.rpow_0 [OF RA] Ring.rpow_0 [OF RB])
  next
    case (Suc n)
    have cl: "Ring.rpow mult u x n ∈ A" by (rule Ring.rpow_closed [OF RA x])
    then show ?case
      using Ring.rpow_Suc [OF RB] RA Suc hmult x by (metis Ring.rpow_Suc)
  qed
  define kf where "kf ≡ (λi. mult (p i) (Ring.rpow mult u x i))"
  have kA: "kf i ∈ A" for i
    unfolding kf_def
    using p Ring.rpow_closed [OF RA x] Monoid.composition_closed [OF MonM] by blast
  have summand: "bmult (h (p i)) (Ring.rpow bmult bu (h x) i) = h (kf i)" for i
    unfolding kf_def using rp hmult [OF p Ring.rpow_closed [OF RA x]] by simp
  have "commutative_monoid.fincomp B badd bz (λi. bmult (h (p i)) (Ring.rpow bmult bu (h x) i))
            {..Ring.degree bz (λk. h (p k))} 
      = commutative_monoid.fincomp B badd bz (λi. h (kf i)) {..Ring.degree z p}"
    using summand deg by simp
  also have "… = h (commutative_monoid.fincomp A add z kf {..Ring.degree z p})"
  proof (rule fincomp_hom [OF cmA cmB, symmetric])
    show "⋀y. y ∈ A ⟹ h y ∈ B" by (rule hB)
    show "h z = bz" by (rule hz)
    show "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (add y y') = badd (h y) (h y')" by (rule hadd)
    show "kf ∈ {..Ring.degree z p} → A" using kA by blast
  qed
  also have "… = h (Ring.eval A add mult z u x p)"
    unfolding kf_def by (simp add: Ring.eval_def [OF RA, symmetric])
  finally show ?thesis 
    using Ring.eval_def [OF RB] by simp
qed

text ‹When the map is injective on the source and the target is exactly the image, the degree
  hypothesis is automatic: an injection sends the zero to the zero and nothing else there, so the two
  coefficient supports are the same set.›
corollary eval_transport:
  fixes A :: "'b set" and add mult :: "'b ⇒ 'b ⇒ 'b" and z u :: 'b
    and h :: "'b ⇒ 'c" and hadd hmult :: "'c ⇒ 'c ⇒ 'c"
  assumes RA: "Ring A add mult z u"
    and RK: "Ring (h ` A) hadd hmult (h z) (h u)"
    and ha: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (add y y') = hadd (h y) (h y')"
    and hm: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (mult y y') = hmult (h y) (h y')"
    and inj: "inj_on h A"
    and x: "x ∈ A" and p: "⋀k. p k ∈ A"
  shows "Ring.eval (h ` A) hadd hmult (h z) (h u) (h x) (λk. h (p k))
       = h (Ring.eval A add mult z u x p)"
proof (rule eval_hom [OF RA RK])
  show "⋀y. y ∈ A ⟹ h y ∈ h ` A" by blast
  show "h z = h z" by rule
  show "h u = h u" by rule
  show "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (add y y') = hadd (h y) (h y')" by (rule ha)
  show "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (mult y y') = hmult (h y) (h y')" by (rule hm)
  show "x ∈ A" by (rule x)
  show "⋀k. p k ∈ A" by (rule p)
  have cmA: "commutative_monoid A add z" using RA by (simp add: Ring_def Abelian_Group_def)
  have MonA: "Monoid A add z" using cmA by (simp add: commutative_monoid_def)
  have zA: "z ∈ A" by (rule Monoid.unit_closed [OF MonA])
  have supp: "{i. h (p i) ≠ h z} = {i. p i ≠ z}"
    using inj_on_eq_iff [OF inj p zA] by blast
  show "Ring.degree (h z) (λk. h (p k)) = Ring.degree z p"
    using Ring.degree_def [OF RK, of "λk. h (p k)"] Ring.degree_def [OF RA, of p] supp
    by simp
qed


section ‹Polynomials over a Commutative Ring (continued): evaluation is multiplicative›

context commutative_ring
begin

text ‹∗‹Evaluation is multiplicative.›  This needs commutativity (the point and the coefficients
  must commute).  The proof mirrors @{thm [source] poly_mult_assoc}: expand both sides to sums 
  over a triangle of index pairs and reindex by @{text "(k,i) ↦ (i, k - i)"}.›
lemma eval_mult:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier" and a: "a ∈ R"
  shows "eval a (p ⊗⇩P q) = eval a p ⋅ eval a q"
proof -
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R" using p q by (auto simp: poly_carrier_coeff_closed)
  have pq: "p ⊗⇩P q ∈ poly_carrier" using p q by (rule poly_mult_closed)
  define N where "N = degree p + degree q"
  have dpq: "degree (p ⊗⇩P q) ≤ N" unfolding N_def using degree_mult_le[OF p q] .
  ― ‹LHS: distribute @{text "a⇧k"} into the convolution and view it over the triangle.›
  have "eval a (p ⊗⇩P q) = additive.fincomp (λk. (p ⊗⇩P q) k ⋅ rpow a k) {..N}"
    using eval_fincomp_le[OF pq a dpq] .
  also have "… = additive.fincomp
                    (λk. additive.fincomp (λi. (p i ⋅ q (k - i)) ⋅ rpow a k) {..k}) {..N}"
    unfolding poly_mult_def
    using pi qi a by (auto intro!: additive.fincomp_cong' fincomp_mult_distrib_right)
  also have "… = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ rpow a (fst x))
                    (Sigma {..N} (λk. {..k}))"
    by (rule fincomp_Sigma) (use pi qi a in auto)
  finally have LHS: "eval a (p ⊗⇩P q)
        = additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ rpow a (fst x))
            (Sigma {..N} (λk. {..k}))" .
  ― ‹RHS: expand the product of the two evaluation sums into a double sum.›
  have "eval a q ∈ R" using q a by (rule eval_closed)
  then have "eval a p ⋅ eval a q = additive.fincomp (λi. (p i ⋅ rpow a i) ⋅ eval a q) {..degree p}"
    using pi a unfolding eval_def by (intro fincomp_mult_distrib_right) auto
  also have "… = additive.fincomp
                    (λi. additive.fincomp (λj. (p i ⋅ rpow a i) ⋅ (q j ⋅ rpow a j)) {..degree q})
                    {..degree p}"
    unfolding eval_def using pi qi a additive.fincomp_closed
    by (auto simp: intro!: additive.fincomp_cong' fincomp_mult_distrib_left)
  also have "… = additive.fincomp
                    (λx. (p (fst x) ⋅ rpow a (fst x)) ⋅ (q (snd x) ⋅ rpow a (snd x)))
                    (Sigma {..degree p} (λi. {..degree q}))"
    by (intro fincomp_Sigma) (use pi qi a in auto)
  finally have RHS: "eval a p ⋅ eval a q
        = additive.fincomp (λx. (p (fst x) ⋅ rpow a (fst x)) ⋅ (q (snd x) ⋅ rpow a (snd x)))
            (Sigma {..degree p} (λi. {..degree q}))" .
  ― ‹Both sides are sums of @{text "p i ⋅ q j ⋅ a⇗i+j⇖"}; identify the index sets.›
  let ?T = "Sigma {..N} (λk. {..k})"
  let ?S = "Sigma {..degree p} (λi. {..degree q})"
  let ?G = "λi j. (p i ⋅ q j) ⋅ rpow a (i + j)"
  ― ‹Rewrite the LHS summand into the symmetric form @{text "?G i j"} with @{text "(i,j) = (snd x, fst x - snd x)"}.›
  have LHS': "additive.fincomp (λx. (p (snd x) ⋅ q (fst x - snd x)) ⋅ rpow a (fst x)) ?T
             = additive.fincomp (λx. ?G (snd x) (fst x - snd x)) ?T"
    by (intro additive.fincomp_cong') (auto simp: a pi qi)
  ― ‹And the RHS summand likewise, with @{text "(i,j) = (fst x, snd x)"}.›
  have RHS': "additive.fincomp (λx. (p (fst x) ⋅ rpow a (fst x)) ⋅ (q (snd x) ⋅ rpow a (snd x))) ?S
             = additive.fincomp (λx. ?G (fst x) (snd x)) ?S"
    by (simp add: a multiplicative.associative multiplicative.left_commute pi qi rpow_add)
  ― ‹The rectangle ‹?S› sits inside the larger triangle ‹?U›; the extra summands of ‹?U›
      vanish, since ‹p i = 𝟬› for ‹i > degree p› and likewise ‹q›.  So the sum over ‹?S›
      equals the sum over ‹?U›.›
  let ?U = "Sigma {..N} (λi. {..N - i})"
  have GR: "⋀i j. ?G i j ∈ R" using pi qi a by simp
  have G_eq_S: "additive.fincomp (λx. ?G (fst x) (snd x)) ?S = additive.fincomp (λx. ?G (fst x) (snd x)) ?U"
  proof -
    have "?G (fst x) (snd x) = 𝟬" if "x ∈ ?U - ?S" for x
    proof -
      have "p (fst x) = 𝟬 ∨ q (snd x) = 𝟬"
        using that coeff_gt_degree[OF p] coeff_gt_degree[OF q] by (auto simp: mem_Times_iff)
      then show ?thesis
        using a left_zero pi qi right_zero rpow_closed by presburger
    qed
    with GR N_def show ?thesis      
      by (intro additive.fincomp_mono_neutral_cong_left) auto
  qed
  ― ‹Reindex the LHS triangle @{term ?T} to @{term ?U} by @{text "(k,i) ↦ (i, k - i)"} --- the
      same bijection used for associativity of convolution.›
  let ?h = "λx::nat×nat. (snd x, fst x - snd x)"
  let ?h' = "λx::nat×nat. (fst x + snd x, fst x)"
  have bij: "bij_betw ?h ?T ?U"
    by (rule bij_betw_byWitness[where f' = ?h']) (auto simp: N_def)
  have "additive.fincomp (λx. ?G (fst x) (snd x)) ?U
        = additive.fincomp (λx. ?G (fst x) (snd x)) (?h ` ?T)"
    using bij bij_betw_imp_surj_on by fastforce
  also have "… = additive.fincomp (λx. ?G (fst (?h x)) (snd (?h x))) ?T"
    using bij bij_betw_def GR by (intro additive.fincomp_reindex) auto
  finally have "additive.fincomp (λx. ?G (fst x) (snd x)) ?S
                = additive.fincomp (λx. ?G (snd x) (fst x - snd x)) ?T"
    using G_eq_S by simp
  then show ?thesis using LHS RHS LHS' RHS' by simp
qed

text ‹Evaluation respects negation, hence is a ring homomorphism @{text "F[X] → F"}.›
lemma eval_neg:
  assumes "p ∈ poly_carrier" and "a ∈ R"
  shows "eval a (⊖⇩P p) = - eval a p"
proof -
  have "eval a p + eval a (⊖⇩P p) = 𝟬"
    using assms eval_add poly_add_neg_right poly_neg_closed by fastforce 
  then show ?thesis
    by (simp add: assms additive.commutative additive.inverse_equality poly_neg_closed)
qed

text ‹The linear polynomial @{text "X - a"} (a root factor).›
definition root_factor :: "'a ⇒ (nat ⇒ 'a)"
  where "root_factor a ≡ X⇩P ⊕⇩P (⊖⇩P poly_const a)"

lemma root_factor_closed: "a ∈ R ⟹ root_factor a ∈ poly_carrier"
  unfolding root_factor_def using var_closed poly_const_closed poly_neg_closed by (simp add: poly_add_closed)

text ‹@{term "root_factor a"} evaluates to @{text 0} at @{term a}.›
lemma eval_root_factor [simp]:
  assumes a: "a ∈ R" shows "eval a (root_factor a) = 𝟬"
  using a poly_const_closed poly_neg_closed
  by (simp add: eval_add eval_neg poly_const_closed root_factor_def var_closed)

end


section ‹Polynomials over a Commutative Ring›

context commutative_ring
begin

text ‹When the coefficient ring is commutative, so is the polynomial ring: the convolution
  @{text "∑i≤k. p i ⋅ q (k - i)"} is symmetric under the reindexing @{text "i ↦ k - i"}.›
lemma poly_mult_comm:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier"
  shows "p ⊗⇩P q = q ⊗⇩P p"
proof
  fix k
  have inj: "inj_on (λi. k - i) {..k::nat}"
    unfolding atMost_iff image_def Ball_def set_eq_iff inj_on_def
    by presburger
  have  inj: "inj_on (λi. k - i) {..k::nat}" and img: "(λi. k - i) ` {..k} = {..k::nat}"
    unfolding inj_on_def atMost_iff image_def Bex_def Ball_def set_eq_iff mem_Collect_eq
    by presburger+
  have pi: "⋀i. p i ∈ R" and qi: "⋀i. q i ∈ R"
    using p q by (auto simp: poly_carrier_coeff_closed)
  have "(p ⊗⇩P q) k = additive.fincomp (λi. q (k - i) ⋅ p i) ((λi. k - i) ` {..k})"
    using img multiplicative.commutative pi poly_mult_def qi by presburger
  also have "… = additive.fincomp (λi. q (k - (k - i)) ⋅ p (k - i)) {..k}"
    using additive.fincomp_reindex[where h = "λi. k - i" and A = "{..k}"] pi qi inj by auto
  also have "… = additive.fincomp (λi. q i ⋅ p (k - i)) {..k}"
    by (rule additive.fincomp_cong') (use pi qi in auto)
  also have "… = (q ⊗⇩P p) k" by (simp add: poly_mult_def)
  finally show "(p ⊗⇩P q) k = (q ⊗⇩P p) k" .
qed

text ‹Hence the polynomial ring over a commutative ring is itself commutative.›
theorem poly_commutative_ring:
  "commutative_ring poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
proof -
  interpret R: Ring poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P" by (rule poly_ring)
  show ?thesis
  proof qed (simp add: poly_mult_comm)
qed

end


section ‹Polynomials over an Integral Domain›

context integral_domain
begin

text‹The leading coefficients are nonzero, and a domain has no zero divisors, so the
      product's coefficient at @{text "degree p + degree q"} is nonzero.›
lemma degree_mult:
  assumes p: "p ∈ poly_carrier" and q: "q ∈ poly_carrier"
    and pnz: "p ≠ 𝟬⇩P" and qnz: "q ≠ 𝟬⇩P"
  shows "degree (p ⊗⇩P q) = degree p + degree q"
proof (rule antisym)
  have "p (degree p) ⋅ q (degree q) ≠ 𝟬"
    by (metis coeff_degree_nonzero local.no_zero_divisors poly_carrier_coeff_closed assms)
  then have "(p ⊗⇩P q) (degree p + degree q) ≠ 𝟬"
    using coeff_mult_degree_add[OF p q] by simp
  then show "degree p + degree q ≤ degree (p ⊗⇩P q)"
    by (meson coeff_gt_degree linorder_not_le p poly_mult_closed q)
qed (simp add: degree_mult_le p q)

text ‹Multiplication by a nonzero monomial shifts the degree by its exponent.›
lemma degree_monom_mult:
  assumes c: "c ∈ R" and b: "b ∈ poly_carrier"
    and cnz: "c ≠ 𝟬" and bnz: "b ≠ 𝟬⇩P"
  shows "degree (monom c n ⊗⇩P b) = n + degree b"
  by (simp add: b bnz c cnz degree_monom degree_mult monom_closed)

text ‹Hence the polynomial ring over an integral domain has no zero divisors.›
lemma poly_no_zero_divisors:
  assumes "p ∈ poly_carrier" and "q ∈ poly_carrier" and "p ⊗⇩P q = 𝟬⇩P"
  shows "p = 𝟬⇩P ∨ q = 𝟬⇩P"
proof (rule ccontr)
  assume "¬ (p = 𝟬⇩P ∨ q = 𝟬⇩P)"
  then obtain "p (degree p) ≠ 𝟬" and "q (degree q) ≠ 𝟬" 
    using assms coeff_degree_nonzero by blast
  then have "(p ⊗⇩P q) (degree p + degree q) ≠ 𝟬"
    by (metis coeff_mult_degree_add no_zero_divisors poly_carrier_coeff_closed assms) 
  then show False using ‹p ⊗⇩P q = 𝟬⇩P› by (simp add: poly_zero_def)
qed


text ‹Hence @{text "R[X]"} is itself an integral domain. .›
theorem poly_integral_domain:
  "integral_domain poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
proof -
  interpret comm: commutative_ring poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P"
    by (rule poly_commutative_ring)
  show ?thesis
  proof
    show nt: "𝟭⇩P ≠ 𝟬⇩P"
      by (metis nontrivial poly_one_def poly_zero_def)
  qed (simp add: poly_no_zero_divisors)
qed

end


section ‹Polynomial Division over a Field›

context Field
begin

subsection ‹Units of ‹F[X]››

text ‹Over a field, multiplication of nonzero polynomials adds degrees, so a polynomial can
  only be a multiplicative unit if it has degree @{text 0}: the units of @{text "F[X]"} are
  exactly the nonzero constants.  This pins down what it means for an irreducible polynomial
  to admit only trivial factorisations.›

text ‹A nonzero constant is a unit, with the constant of the inverse coefficient as inverse.›
lemma poly_const_unit:
  assumes a: "a ∈ R" and anz: "a ≠ 𝟬"
  shows "poly_unit (poly_const a)"
  by (metis poly_unitI field_inverse poly_const_mult assms multiplicative.invertibleE 
      poly_const_closed poly_const_one)

text ‹Conversely, every unit of @{text "F[X]"} is a nonzero constant.  An invertible
  polynomial is nonzero and has degree @{text 0} (degrees add under multiplication), so it is
  the constant of its own (nonzero) leading coefficient.›
lemma poly_unit_imp_const:
  assumes inv: "poly_unit p"
  shows "p ≠ 𝟬⇩P ∧ degree p = 0 ∧ p = poly_const (p 0) ∧ p 0 ≠ 𝟬"
proof -
  have p: "p ∈ poly_carrier" using inv by (rule poly_unit_closed)
  obtain q where q: "q ∈ poly_carrier" and pq: "p ⊗⇩P q = 𝟭⇩P"
    using inv unfolding poly_unit_def by blast
  have pnz: "p ≠ 𝟬⇩P"
    using q poly_mult_zero_left pq eval_zero nontrivial by force
  have qnz: "q ≠ 𝟬⇩P"
    using p pnz poly_mult_one_right poly_mult_zero_right pq by force
  ― ‹Degrees add and the product has degree @{text 0}, so @{term p} has degree @{text 0}.›
  have d0: "degree p = 0"
    by (metis add_eq_0_iff_both_eq_0 degree_mult degree_one p pnz pq q qnz)
  then show ?thesis using pnz d0
    by (metis coeff_degree_nonzero degree_zero_imp_const p)
qed

text ‹A polynomial is ∗‹irreducible› when it is a non-unit, nonzero, and every factorisation
  has a unit factor.  Over a field this excludes the units (the nonzero constants) and the
  zero polynomial, matching the usual notion for @{text "F[X]"}.›
definition poly_irreducible :: "(nat ⇒ 'a) ⇒ bool"
  where "poly_irreducible p ≡ 
           p ∈ poly_carrier ∧ p ≠ 𝟬⇩P ∧ ¬ poly_unit p
              ∧ (∀a b. a ∈ poly_carrier ⟶ b ∈ poly_carrier ⟶ p = a ⊗⇩P b
                       ⟶ poly_unit a ∨ poly_unit b)"

lemma poly_irreducibleD_carrier: "poly_irreducible p ⟹ p ∈ poly_carrier"
  unfolding poly_irreducible_def by blast

lemma poly_irreducibleD_nonzero: "poly_irreducible p ⟹ p ≠ 𝟬⇩P"
  unfolding poly_irreducible_def by blast

lemma poly_irreducibleD_nonunit: "poly_irreducible p ⟹ ¬ poly_unit p"
  unfolding poly_irreducible_def by blast

lemma poly_irreducibleD_factor:
  "⟦ poly_irreducible p; a ∈ poly_carrier; b ∈ poly_carrier; p = a ⊗⇩P b ⟧
     ⟹ poly_unit a ∨ poly_unit b"
  unfolding poly_irreducible_def by blast

text ‹An irreducible polynomial is nonconstant: a nonzero constant is a unit, and the zero
  polynomial is excluded outright.  Needed because the remainders modulo @{term p} contain
  @{term "𝟭⇩P"} only when @{term p} is nonconstant.›
lemma poly_irreducible_degree_pos:
  assumes irr: "poly_irreducible p" shows "0 < degree p"
proof (rule ccontr)
  assume non: "¬ 0 < degree p"
  have pc: "p ∈ poly_carrier" using irr by (rule poly_irreducibleD_carrier)
  have const: "p = poly_const (p 0)"
    using non degree_zero_imp_const pc by blast
  have nz: "p 0 ≠ 𝟬"
    using const irr poly_const_zero poly_irreducibleD_nonzero by force
  have "poly_unit p"
    using const poly_const_unit [OF poly_carrier_coeff_closed [OF pc] nz] by simp
  with poly_irreducibleD_nonunit [OF irr] show False ..
qed

interpretation Ring_R: Ring R "addition" "(⋅)" 𝟬 𝟭 ..

text ‹The reduction step of the division algorithm: when @{term "degree b ≤ degree a"} and both
  are nonzero, subtracting the appropriate monomial multiple of @{term b} cancels the leading
  term of @{term a}, strictly decreasing its degree.›
lemma div_step:
  assumes a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
    and anz: "a ≠ 𝟬⇩P" and bnz: "b ≠ 𝟬⇩P" and ge: "degree b ≤ degree a"
  obtains m where "m ∈ poly_carrier" "degree m = degree a - degree b"
    and "a ⊕⇩P (⊖⇩P (m ⊗⇩P b)) = 𝟬⇩P ∨ degree (a ⊕⇩P (⊖⇩P (m ⊗⇩P b))) < degree a"
proof -
  define c where "c ≡  lead_coeff a ⋅ multiplicative.inverse (lead_coeff b)"
  define k where "k ≡ degree a - degree b"
  have laR: "lead_coeff a ∈ R" and lbR: "lead_coeff b ∈ R"
    using a b by (simp_all add: lead_coeff_def poly_carrier_coeff_closed)
  have invb: "multiplicative.invertible (lead_coeff b)"
    by (simp add: b bnz field_inverse lbR lead_coeff_nonzero)
  have ibR: "multiplicative.inverse (lead_coeff b) ∈ R" using lbR invb by simp
  have ib_nz: "multiplicative.inverse (lead_coeff b) ≠ 𝟬"
    using invb lbR multiplicative.invertible_right_inverse nontrivial right_zero by moura
  have cnz: "c ≠ 𝟬"
    using a anz c_def ibR ib_nz laR lead_coeff_nonzero local.no_zero_divisors by auto
  define m where "m = monom c k"
  have mc: "m ∈ poly_carrier"
    by (simp add: c_def ibR laR m_def monom_closed)
  have mk: "m k ≠ 𝟬" unfolding m_def monom_def using cnz by simp
  ― ‹@{term m} has degree exactly @{term k}.›
  have degm: "degree m = k"
    using coeff_gt_degree degree_monom_le le_neq_implies_less m_def mc mk by blast
  have mbc: "m ⊗⇩P b ∈ poly_carrier" using mc b by (rule poly_mult_closed)
  ― ‹The product @{term "m ⊗⇩P b"} has degree @{term "degree a"} and matching leading term.›
  have degmb: "degree (m ⊗⇩P b) = degree a"
    using b bnz cnz degm degree_mult ge k_def m_def mc by fastforce
  have lead_mb: "(m ⊗⇩P b) (degree a) = lead_coeff a"
    using coeff_mult_degree_add[OF mc b] invb degm ge k_def laR lbR m_def 
    by (force simp: c_def multiplicative.associative lead_coeff_def monom_def)
  define d where "d ≡ a ⊕⇩P (⊖⇩P (m ⊗⇩P b))"
  have dc: "d ∈ poly_carrier" unfolding d_def using a mbc poly_neg_closed poly_add_closed by simp
  ― ‹The difference is zero or has strictly smaller degree, since its top coefficient cancels.›
  have "d = 𝟬⇩P ∨ degree d < degree a"
  proof (cases "d = 𝟬⇩P")
    case True then show ?thesis ..
  next
    case False
    have "degree d ≤ degree a"
      by (intro degree_leI[OF dc]) (simp add: a d_def poly_add_def poly_neg_def coeff_gt_degree degmb mbc)
    moreover have "d (degree a) = 𝟬"
      using Ring.lead_coeff_def Ring_axioms d_def laR lead_mb poly_add_def poly_neg_def
      by fastforce
    ultimately show ?thesis
      using False by (metis coeff_degree_nonzero dc le_neq_implies_less)
  qed
  then show ?thesis using mc degm d_def by (metis k_def that)
qed

text ‹∗‹The division algorithm.›  For any dividend @{term a} and nonzero divisor @{term b}
  there exist a quotient @{term q} and remainder @{term r} with @{text "a = b ⊗ q ⊕ r"} and
  the remainder either zero or of degree below that of @{term b}.  Proved by strong induction
  on @{term "degree a"}, repeatedly applying @{thm [source] div_step}.›
theorem poly_divide:
  assumes a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "∃q r. q ∈ poly_carrier ∧ r ∈ poly_carrier ∧ a = (b ⊗⇩P q) ⊕⇩P r
              ∧ (r = 𝟬⇩P ∨ degree r < degree b)"
  using a
proof (induct "degree a" arbitrary: a rule: less_induct)
  case (less a)
  show ?case
  proof (cases "a = 𝟬⇩P ∨ degree a < degree b")
    case True then show ?thesis
    ― ‹Base case: the quotient is zero and @{term a} is the remainder.›
      by (metis b less.prems poly_zero_closed poly_add_zero poly_mult_zero_right)
  next
    case False
    then have anz: "a ≠ 𝟬⇩P" and ge: "degree b ≤ degree a" by auto
    ― ‹Reduce the leading term, then divide the smaller remainder by the induction hypothesis.›
    obtain m where m: "m ∈ poly_carrier"
      and d: "a ⊕⇩P (⊖⇩P (m ⊗⇩P b)) = 𝟬⇩P ∨ degree (a ⊕⇩P (⊖⇩P (m ⊗⇩P b))) < degree a"
      using div_step[OF less.prems b anz bnz ge] by blast
    define dd where "dd = a ⊕⇩P (⊖⇩P (m ⊗⇩P b))"
    have ddc: "dd ∈ poly_carrier"
      unfolding dd_def using less.prems b m poly_neg_closed poly_mult_closed poly_add_closed
      by simp
    ― ‹@{term a} is recovered: @{text "a = (m ⊗ b) ⊕ dd"}, by additive-group cancellation.›
    have mbc: "m ⊗⇩P b ∈ poly_carrier" using m b by (rule poly_mult_closed)
    have a_eq: "a = (m ⊗⇩P b) ⊕⇩P dd"
      unfolding dd_def using poly_add_minus_cancel[OF mbc less.prems] by simp
    have dd_div: "∃q r. q ∈ poly_carrier ∧ r ∈ poly_carrier ∧ dd = (b ⊗⇩P q) ⊕⇩P r
                       ∧ (r = 𝟬⇩P ∨ degree r < degree b)"
      by (metis b d dd_def ddc less.hyps poly_add_zero poly_mult_zero_right)
    then obtain q r where q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
      and dd_eq: "dd = (b ⊗⇩P q) ⊕⇩P r" and rdeg: "r = 𝟬⇩P ∨ degree r < degree b" by blast
    ― ‹Assemble: @{text "a = (m ⊗ b) ⊕ (b ⊗ q) ⊕ r = b ⊗ (m ⊕ q) ⊕ r"}.›
    have "a = (m ⊗⇩P b) ⊕⇩P ((b ⊗⇩P q) ⊕⇩P r)" using a_eq dd_eq by simp
    also have "… = (b ⊗⇩P (m ⊕⇩P q)) ⊕⇩P r"
      using poly_mult_add_distrib_left[OF b m q]
      by (simp add: b m poly_add_assoc poly_mult_closed poly_mult_comm q r)
    finally have "a = (b ⊗⇩P (m ⊕⇩P q)) ⊕⇩P r" .
    then show ?thesis 
      by (metis r rdeg m poly_add_closed q)
  qed
qed

text ‹∗‹Uniqueness of quotient and remainder.›  If @{term b} is nonzero and two quotient/remainder
  pairs both work --- each remainder of degree below @{term b} --- then they coincide.  For if the
  quotients differed, ‹b ⊗ (q⇩1 ⊕ ⊖q⇩2)› would have degree ‹≥ degree b› (degrees
  add over a domain), yet it equals ‹r⇩2 ⊕ ⊖r⇩1›, of degree below @{term b}.›
text ‹Left cancellation of a nonzero factor: @{text "a ⊗ x = a ⊗ y ⟹ x = y"} (the ring of
  polynomials over a field is a domain).›
lemma poly_mult_left_cancel:
  assumes a: "a ∈ poly_carrier" and anz: "a ≠ 𝟬⇩P"
    and x: "x ∈ poly_carrier" and y: "y ∈ poly_carrier"
    and eq: "a ⊗⇩P x = a ⊗⇩P y"
  shows "x = y"
proof -
  have ny: "⊖⇩P y ∈ poly_carrier" using y by (rule poly_neg_closed)
  have dxyc: "x ⊕⇩P (⊖⇩P y) ∈ poly_carrier" using x ny by (rule poly_add_closed)
  ― ‹@{text "a ⊗ ⊖y = ⊖(a ⊗ y)"}: the two sum to @{text "a ⊗ (y ⊕ ⊖y) = 𝟬"}.›
  have "(a ⊗⇩P y) ⊕⇩P (a ⊗⇩P (⊖⇩P y)) = a ⊗⇩P (y ⊕⇩P (⊖⇩P y))"
    using poly_mult_add_distrib_left[OF a y ny] by simp
  also have "… = 𝟬⇩P" using a
    by (simp add: poly_add_neg_right poly_mult_zero_right y)
  finally have "(a ⊗⇩P y) ⊕⇩P (a ⊗⇩P (⊖⇩P y)) = 𝟬⇩P" .
  then have "a ⊗⇩P (x ⊕⇩P (⊖⇩P y)) = 𝟬⇩P" 
  ― ‹No zero divisors and @{term "a ≠ 𝟬⇩P"} force ‹x ⊕ ⊖y = 𝟬⇩P›, i.e. @{term "x = y"}.›
    by (simp add: a eq ny poly_mult_add_distrib_left x)
  then show ?thesis
    by (meson a anz dxyc poly_diff_zero_eq poly_no_zero_divisors x y)
qed

theorem poly_divide_unique:
  assumes b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
    and q1: "q1 ∈ poly_carrier" and r1: "r1 ∈ poly_carrier"
    and q2: "q2 ∈ poly_carrier" and r2: "r2 ∈ poly_carrier"
    and e1: "a = (b ⊗⇩P q1) ⊕⇩P r1" and d1: "r1 = 𝟬⇩P ∨ degree r1 < degree b"
    and e2: "a = (b ⊗⇩P q2) ⊕⇩P r2" and d2: "r2 = 𝟬⇩P ∨ degree r2 < degree b"
  shows "q1 = q2 ∧ r1 = r2"
proof 
  have bq1: "b ⊗⇩P q1 ∈ poly_carrier" using b q1 by (rule poly_mult_closed)
  have bq2: "b ⊗⇩P q2 ∈ poly_carrier" using b q2 by (rule poly_mult_closed)
  define dq where "dq = q1 ⊕⇩P (⊖⇩P q2)"
  define dr where "dr = r2 ⊕⇩P (⊖⇩P r1)"
  have dqc: "dq ∈ poly_carrier" unfolding dq_def using q1 q2 poly_neg_closed by (simp add: poly_add_closed)
  have drc: "dr ∈ poly_carrier" unfolding dr_def using r1 r2 poly_neg_closed by (simp add: poly_add_closed)
  ― ‹The two equations give @{term "b ⊗⇩P dq = dr"}.›
  have key: "b ⊗⇩P dq = dr"
  proof -
    have "b ⊗⇩P dq = (b ⊗⇩P q1) ⊕⇩P (b ⊗⇩P (⊖⇩P q2))"
      unfolding dq_def using poly_mult_add_distrib_left[OF b q1 poly_neg_closed[OF q2]] .
    also have "b ⊗⇩P (⊖⇩P q2) = ⊖⇩P (b ⊗⇩P q2)"
      using poly_mult_add_distrib_left[OF b q2 poly_neg_closed[OF q2]]
      by (simp add: b poly_add_neg_right poly_minus_unique poly_mult_closed poly_mult_zero_right
          poly_neg_closed q2) 
    finally have "b ⊗⇩P dq = (b ⊗⇩P q1) ⊕⇩P (⊖⇩P (b ⊗⇩P q2))" .
    ― ‹And ‹(b ⊗ q1) ⊕ ⊖(b ⊗ q2) = r2 ⊕ ⊖r1 = dr› from the two division equations.›
    then show ?thesis
      using bq1 bq2 dr_def e1 e2 poly_sub_shift r1 r2 by force
  qed
  ― ‹If @{term dq} were nonzero, @{term "b ⊗⇩P dq"} would have degree @{text "≥ degree b"}.›
  have dqz: "dq = 𝟬⇩P"
  proof (rule ccontr)
    assume dqnz: "dq ≠ 𝟬⇩P"
    have ge: "degree b ≤ degree dr" using key
      using b bnz degree_mult dqc dqnz by force
    ― ‹But @{term dr} has degree below @{term b}.›
    have "dr = 𝟬⇩P ∨ degree dr < degree b"
    proof (cases "dr = 𝟬⇩P")
      case True then show ?thesis ..
    next
      case False
      ― ‹@{term dr} is nonzero, so @{term "degree b > 0"} (else both remainders vanish).›
      have bpos: "degree b > 0"
        using False d1 d2 dr_def poly_add_neg_right r2 by force
      have r1b: "degree r1 < degree b" using d1 bpos by auto
      have r2b: "degree r2 < degree b" using d2 bpos by auto
      have "degree dr ≤ max (degree r2) (degree (⊖⇩P r1))"
        unfolding dr_def by (rule degree_add_le[OF r2 poly_neg_closed[OF r1]])
      then show ?thesis
        using degree_neg r1 r1b r2b by fastforce
    qed
    then show False
      using b bnz dqc dqnz ge key poly_no_zero_divisors by fastforce
  qed
  ― ‹So @{term "q1 = q2"}, and then @{term "r1 = r2"} from either equation.›
  show qeq: "q1 = q2"
    using dq_def dqz poly_diff_zero_eq q1 q2 by blast
  show "r1 = r2"
    using bq1 e1 e2 poly_add_left_cancel qeq r1 r2 by blast 
qed


subsection ‹Remainder modulo a polynomial›

text ‹The remainder of @{term a} on division by @{term b}: the canonical representative of
  @{term a} modulo @{term b}, of degree below that of @{term b}.  Defined by choice from the
  division algorithm, and pinned down uniquely by @{thm [source] poly_divide_unique}.›
definition pmod :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)"
  where "pmod a b = (SOME r. ∃q. q ∈ poly_carrier ∧ r ∈ poly_carrier
                                  ∧ a = (b ⊗⇩P q) ⊕⇩P r ∧ (r = 𝟬⇩P ∨ degree r < degree b))"

text ‹The defining property of @{const pmod}: there is a quotient realising it.›
lemma pmod_spec:
  assumes a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "∃q. q ∈ poly_carrier ∧ pmod a b ∈ poly_carrier
             ∧ a = (b ⊗⇩P q) ⊕⇩P pmod a b ∧ (pmod a b = 𝟬⇩P ∨ degree (pmod a b) < degree b)"
proof -
  let ?P = "λr. ∃q. q ∈ poly_carrier ∧ r ∈ poly_carrier
                     ∧ a = (b ⊗⇩P q) ⊕⇩P r ∧ (r = 𝟬⇩P ∨ degree r < degree b)"
  have "∃r. ?P r" using poly_divide[OF a b bnz] by blast
  then have "?P (SOME r. ?P r)" by (rule someI_ex)
  then show ?thesis unfolding pmod_def .
qed

lemma pmod_closed:
  "⟦ a ∈ poly_carrier; b ∈ poly_carrier; b ≠ 𝟬⇩P ⟧ ⟹ pmod a b ∈ poly_carrier"
  using pmod_spec by blast

lemma pmod_degree:
  "⟦ a ∈ poly_carrier; b ∈ poly_carrier; b ≠ 𝟬⇩P ⟧
     ⟹ pmod a b = 𝟬⇩P ∨ degree (pmod a b) < degree b"
  using pmod_spec by blast

text ‹@{const pmod} is the unique remainder: any low-degree @{term r} congruent to @{term a}
  modulo @{term b} equals @{term "pmod a b"}.›
lemma pmod_unique:
  assumes a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
    and q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
    and eq: "a = (b ⊗⇩P q) ⊕⇩P r" and rd: "r = 𝟬⇩P ∨ degree r < degree b"
  shows "pmod a b = r"
  using pmod_spec[OF a b bnz] poly_divide_unique[OF b bnz]
  by (metis eq q r rd)

text ‹A remainder is a low-degree polynomial --- the form in which the remainders are used as a
  carrier.›
lemma pmod_low_poly:
  assumes a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "pmod a b ∈ low_poly (degree b)"
  using pmod_closed [OF a b bnz] pmod_degree [OF a b bnz]
  by (simp add: low_poly_iff_degree)

text ‹A polynomial of degree below @{term b} is its own remainder.›
lemma pmod_small:
  assumes b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
    and r: "r ∈ poly_carrier" and rd: "r = 𝟬⇩P ∨ degree r < degree b"
  shows "pmod r b = r"
  using pmod_unique[OF r b bnz poly_zero_closed r _ rd]
  using b poly_add_zero poly_mult_zero_right r by force

text ‹Changing @{term a} by a multiple of @{term b} does not change the remainder.  Everything below
  is a consequence of this and @{thm [source] pmod_unique}.›
lemma pmod_shift:
  assumes y: "y ∈ poly_carrier" and c: "c ∈ poly_carrier"
    and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "pmod ((b ⊗⇩P c) ⊕⇩P y) b = pmod y b"
proof -
  obtain q where q: "q ∈ poly_carrier" and yeq: "y = (b ⊗⇩P q) ⊕⇩P pmod y b"
    using pmod_spec [OF y b bnz] by blast
  have r: "pmod y b ∈ poly_carrier" by (rule pmod_closed [OF y b bnz])
  have "(b ⊗⇩P c) ⊕⇩P y = (b ⊗⇩P (c ⊕⇩P q)) ⊕⇩P pmod y b"
    using yeq b c q r
    by (simp add: poly_mult_add_distrib_left poly_add_assoc poly_mult_closed)
  moreover have "(b ⊗⇩P c) ⊕⇩P y ∈ poly_carrier"
    using b c y by (simp add: poly_add_closed poly_mult_closed)
  ultimately show ?thesis
    using pmod_unique [OF _ b bnz _ r _ pmod_degree [OF y b bnz]] c q
    by (simp add: poly_add_closed)
qed

text ‹The remainder is additive outright: a sum of two low-degree remainders is already low-degree,
  so no second reduction is needed.›
lemma pmod_add:
  assumes a: "a ∈ poly_carrier" and a': "a' ∈ poly_carrier"
    and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "pmod (a ⊕⇩P a') b = pmod a b ⊕⇩P pmod a' b"
proof -
  obtain q where q: "q ∈ poly_carrier" and aeq: "a = (b ⊗⇩P q) ⊕⇩P pmod a b"
    using pmod_spec [OF a b bnz] by blast
  obtain q' where q': "q' ∈ poly_carrier" and a'eq: "a' = (b ⊗⇩P q') ⊕⇩P pmod a' b"
    using pmod_spec [OF a' b bnz] by blast
  have r: "pmod a b ∈ poly_carrier" and r': "pmod a' b ∈ poly_carrier"
    using pmod_closed [OF a b bnz] pmod_closed [OF a' b bnz] by blast+
  have rr': "pmod a b ⊕⇩P pmod a' b ∈ poly_carrier" using r r' by (rule poly_add_closed)
  ― ‹The sum of the two remainders is itself low-degree.›
  have low: "pmod a b ⊕⇩P pmod a' b = 𝟬⇩P ∨ degree (pmod a b ⊕⇩P pmod a' b) < degree b"
  proof (cases "pmod a b ⊕⇩P pmod a' b = 𝟬⇩P")
    case False
    ― ‹Not both remainders vanish, so @{term b} has positive degree, and then a vanishing
        remainder has degree below it as well.›
    have dpos: "0 < degree b"
      using pmod_degree [OF _ b bnz] False a a' poly_add_zero poly_zero_closed by fastforce 
    have dr: "degree (pmod a b) < degree b" and dr': "degree (pmod a' b) < degree b"
      using a a' b dpos pmod_spec by fastforce+
    then show ?thesis
      using low_poly_add_closed low_poly_iff_degree r r' rr' by meson
  qed simp
  ― ‹Reduce the left summand, then the right, as ‹pmod_mult› below does for a product; each step
      only moves a multiple of @{term b}.  The sum of the remainders is then its own remainder.›
  have step1: "a ⊕⇩P a' = (b ⊗⇩P q) ⊕⇩P (pmod a b ⊕⇩P a')"
    using a' aeq b poly_add_assoc poly_mult_closed q r by metis
  have "b ⊗⇩P q' ∈ poly_carrier" using b q' by (rule poly_mult_closed)
  then have step2: "pmod a b ⊕⇩P a' = (b ⊗⇩P q') ⊕⇩P (pmod a b ⊕⇩P pmod a' b)"
    using a'eq poly_add_assoc poly_add_comm r r' by metis
  have "pmod (a ⊕⇩P a') b = pmod (pmod a b ⊕⇩P a') b"
    using step1 pmod_shift [OF poly_add_closed [OF r a'] q b bnz] by simp
  also have "… = pmod (pmod a b ⊕⇩P pmod a' b) b"
    using step2 pmod_shift [OF rr' q' b bnz] by simp
  also have "… = pmod a b ⊕⇩P pmod a' b" by (rule pmod_small [OF b bnz rr' low])
  finally show ?thesis .
qed

text ‹The remainder is multiplicative ∗‹after a further reduction›: a product of two low-degree
  remainders need not be low-degree, so the outer @{const pmod} cannot be dropped here as it was for
  the sum.  This is the congruence that makes the remainders a ring.›
lemma pmod_mult:
  assumes a: "a ∈ poly_carrier" and a': "a' ∈ poly_carrier"
    and b: "b ∈ poly_carrier" and bnz: "b ≠ 𝟬⇩P"
  shows "pmod (a ⊗⇩P a') b = pmod (pmod a b ⊗⇩P pmod a' b) b"
proof -
  obtain q where q: "q ∈ poly_carrier" and aeq: "a = (b ⊗⇩P q) ⊕⇩P pmod a b"
    using pmod_spec [OF a b bnz] by blast
  obtain q' where q': "q' ∈ poly_carrier" and a'eq: "a' = (b ⊗⇩P q') ⊕⇩P pmod a' b"
    using pmod_spec [OF a' b bnz] by blast
  have r: "pmod a b ∈ poly_carrier" and r': "pmod a' b ∈ poly_carrier"
    using pmod_closed [OF _ b bnz] a a' by blast+
      ― ‹Reduce the left factor, then the right; each step only moves a multiple of @{term b}.›
  have "a ⊗⇩P a' = ((b ⊗⇩P q) ⊗⇩P a') ⊕⇩P (pmod a b ⊗⇩P a')"
    using aeq poly_mult_add_distrib_right [OF a' poly_mult_closed [OF b q] r] by simp
  then have step1: "a ⊗⇩P a' = (b ⊗⇩P (q ⊗⇩P a')) ⊕⇩P (pmod a b ⊗⇩P a')"
    by (simp add: a' b poly_mult_assoc q)
  have "pmod a b ⊗⇩P a' = (pmod a b ⊗⇩P (b ⊗⇩P q')) ⊕⇩P (pmod a b ⊗⇩P pmod a' b)"
    using a'eq poly_mult_add_distrib_left [OF r poly_mult_closed [OF b q'] r'] by simp
  then have step2: "pmod a b ⊗⇩P a' = (b ⊗⇩P (pmod a b ⊗⇩P q')) ⊕⇩P (pmod a b ⊗⇩P pmod a' b)"
    using b poly_mult_assoc poly_mult_comm q' r by metis
  show ?thesis
    using step1 step2 a' b bnz pmod_shift poly_mult_closed q q' r r' by metis
qed

subsection ‹The factor theorem›

text ‹The root factor @{term "root_factor a"} has degree exactly @{text 1}: its degree-1
  coefficient is @{term 𝟭}, which is nonzero in a (nontrivial) field.›
lemma degree_root_factor:
  assumes a: "a ∈ R" shows "degree (root_factor a) = 1"
proof (rule antisym)
  have rf: "root_factor a ∈ poly_carrier" using a by (rule root_factor_closed)
  ― ‹Coefficients above @{text 1} vanish.›
  show "degree (root_factor a) ≤ 1"
    using a rf unfolding root_factor_def poly_const_def
    by (intro degree_leI) (auto simp: poly_add_def poly_neg_def coeff_var poly_const_def)
  have "root_factor a 1 = 𝟭"
    using a poly_const_def coeff_var poly_add_def poly_neg_def root_factor_def by fastforce
  then show "1 ≤ degree (root_factor a)"
    using degree_le_iff nontrivial rf by fastforce
qed

lemma root_factor_nonzero:
  assumes a: "a ∈ R" shows "root_factor a ≠ 𝟬⇩P"
  using assms degree_root_factor by force

text ‹∗‹The factor theorem.›  A field element @{term a} is a root of @{term p} 
     iff the linear polynomial @{term "root_factor a"} divides @{term p}.›
theorem factor_theorem:
  assumes p: "p ∈ poly_carrier" and a: "a ∈ R"
  shows "eval a p = 𝟬 ⟷ (∃q. q ∈ poly_carrier ∧ p = root_factor a ⊗⇩P q)"
proof
  assume "∃q. q ∈ poly_carrier ∧ p = root_factor a ⊗⇩P q" then show "eval a p = 𝟬"
    using a eval_mult root_factor_closed by force
next
  assume root: "eval a p = 𝟬"
  obtain rf: "root_factor a ∈ poly_carrier" and rfnz: "root_factor a ≠ 𝟬⇩P" 
    using a by (simp add: root_factor_closed root_factor_nonzero)
  ― ‹Divide by the degree-1 factor; the remainder has degree @{text "< 1"}, so is a constant.›
  obtain q r where q: "q ∈ poly_carrier" and r: "r ∈ poly_carrier"
    and peq: "p = (root_factor a ⊗⇩P q) ⊕⇩P r"
    and rdeg: "r = 𝟬⇩P ∨ degree r < degree (root_factor a)"
    using poly_divide[OF p rf rfnz] by blast
  have rconst: "r = poly_const (r 0)"
    using a degree_root_factor degree_zero_imp_const r rdeg by fastforce
  ― ‹Evaluate at @{term a}: the @{term "root_factor a"} term vanishes, leaving the constant.›
  have rqc: "root_factor a ⊗⇩P q ∈ poly_carrier" using rf q 
    by (rule poly_mult_closed)
  have r0: "r 0 ∈ R" 
    using r by (simp add: poly_carrier_coeff_closed)
  have "𝟬 = 𝟬 + r 0"
    using Ring.eval_const Ring_axioms a eval_add eval_mult peq q r r0 rconst rf root rqc
    by fastforce
  then have rz: "r = 𝟬⇩P" using rconst
    using poly_const_zero r by (simp add: poly_carrier_coeff_closed)
  ― ‹So @{term p} is exactly the multiple @{term "root_factor a ⊗⇩P q"}.›
  then show "∃q. q ∈ poly_carrier ∧ p = root_factor a ⊗⇩P q"
    using peq poly_add_comm poly_add_zero poly_zero_closed q rqc by auto 
qed

subsection ‹A nonzero polynomial has at most ‹degree› roots›

text ‹Evaluation of the linear factor @{term "root_factor a"} at an arbitrary point @{term b} is
  ‹b - a›; in particular it is nonzero unless @{term "b = a"}.›
lemma eval_root_factor_apply:
  assumes a: "a ∈ R" and b: "b ∈ R" shows "eval b (root_factor a) = b - a"
proof -
  have nc: "⊖⇩P poly_const a ∈ poly_carrier" 
    using a poly_const_closed poly_neg_closed by simp
  have "eval b (root_factor a) = eval b X⇩P + eval b (⊖⇩P poly_const a)"
    unfolding root_factor_def using var_closed nc b by (rule eval_add)
  also have "… = b - a"
    by (simp add: a b eval_neg poly_const_closed)
  finally show ?thesis .
qed

text ‹The root set @{term "{a ∈ R. eval a p = 𝟬}"} of a nonzero polynomial over a field is finite and
  has at most @{term "degree p"} elements.  By induction on the degree: a root @{term a} lets the factor
  theorem write @{term "p = root_factor a ⊗⇩P q"} with @{term "degree q = degree p - 1"}
  (@{thm [source] degree_mult}, @{thm [source] degree_root_factor}); as a field has no zero divisors,
  every root of @{term p} is @{term a} or a root of @{term q}.›
theorem card_roots_le_degree:
  "p ∈ poly_carrier ⟹ p ≠ 𝟬⇩P
     ⟹ finite {a ∈ R. eval a p = 𝟬} ∧ card {a ∈ R. eval a p = 𝟬} ≤ degree p"
proof (induct "degree p" arbitrary: p rule: less_induct)
  case less
  note p = ‹p ∈ poly_carrier› and pnz = ‹p ≠ 𝟬⇩P›
  show ?case
  proof (cases "∃a ∈ R. eval a p = 𝟬")
    case False
    then have e: "{a ∈ R. eval a p = 𝟬} = {}" by blast
    show ?thesis
      unfolding e by simp
  next
    case True
    then obtain a where aR: "a ∈ R" and aroot: "eval a p = 𝟬" by blast
    obtain q where q: "q ∈ poly_carrier" and peq: "p = root_factor a ⊗⇩P q" and qnz: "q ≠ 𝟬⇩P"
      using factor_theorem[OF p] aroot aR pnz poly_mult_zero_right root_factor_closed by metis
    have rf: "root_factor a ∈ poly_carrier" using aR by (rule root_factor_closed)
    have qnz: "q ≠ 𝟬⇩P" using peq pnz by (metis poly_mult_zero_right rf)
    have degp: "degree p = 1 + degree q"
      by (simp add: aR degree_mult degree_root_factor peq q qnz root_factor_closed
          root_factor_nonzero)
    have IH: "finite {b ∈ R. eval b q = 𝟬} ∧ card {b ∈ R. eval b q = 𝟬} ≤ degree q"
      using degp q qnz by (intro less) simp
    have subset: "{b ∈ R. eval b p = 𝟬} ⊆ insert a {b ∈ R. eval b q = 𝟬}"
    proof
      fix b assume "b ∈ {b ∈ R. eval b p = 𝟬}"
      then have bR: "b ∈ R" and broot: "eval b p = 𝟬" by auto
      have "eval b (root_factor a) ⋅ eval b q = 𝟬"
        using peq eval_mult[OF rf q bR] broot by simp
      then have "eval b (root_factor a) = 𝟬 ∨ eval b q = 𝟬"
        using eval_closed[OF rf bR] by (simp add: bR local.no_zero_divisors q)
      then show "b ∈ insert a {b ∈ R. eval b q = 𝟬}"
      proof
        assume "eval b (root_factor a) = 𝟬"
        then have z: "b + (- a) = 𝟬" using eval_root_factor_apply[OF aR bR] by simp
        then show ?thesis
          using aR additive.inverse_unique additive.invertible_left_inverse bR by blast
      qed (auto simp: bR)
    qed
    have "card {a ∈ R. eval a p = 𝟬} ≤ card (insert a {b ∈ R. eval b q = 𝟬})"
      by (simp add: IH card_mono subset)
    also have "… ≤ degree p"
      using IH degp by (intro card_insert_le_m1) auto
    finally show ?thesis
      using IH finite_subset subset by auto
  qed
qed


subsection ‹Low-degree irreducibility›

text ‹Evaluation of a polynomial of degree @{text "≤ 1"}: @{text "eval α c = c 0 + c 1 ⋅ α"}.›
lemma eval_le1:
  assumes c: "c ∈ poly_carrier" and al: "α ∈ R" and d: "degree c ≤ 1"
  shows "eval α c = c 0 + c 1 ⋅ α"
proof -
  have ci: "⋀i. c i ∈ R" using c by (simp add: poly_carrier_coeff_closed)
  have "additive.fincomp (λi. c i ⋅ rpow α i) {0, 1} = c 0 ⋅ rpow α 0 + c 1 ⋅ rpow α 1"
    using ci al by simp
  then show ?thesis 
    unfolding eval_fincomp_le[OF c al d]
    by (simp add: al atMost_Suc ci insert_commute)
qed

text ‹Every polynomial of degree @{text 1} over a field has a root:  @{text "-(c 0) ⋅ (c 1)¯"}.›
lemma degree1_has_root:
  assumes c: "c ∈ poly_carrier" and d: "degree c = 1"
  shows "∃α∈R. eval α c = 𝟬"
proof -
  have ci: "⋀i. c i ∈ R" using c by (simp add: poly_carrier_coeff_closed)
  have inv: "multiplicative.invertible (c 1)"
    using c ci coeff_degree_nonzero d field_inverse by force
  then have i1: "multiplicative.inverse (c 1) ∈ R" using ci by simp
  have nc0: "- c 0 ∈ R" using ci by simp
  define α where "α ≡ (- c 0) ⋅ multiplicative.inverse (c 1)"
  have aR: "α ∈ R" unfolding α_def using nc0 i1 by simp
  have "c 1 ⋅ α = (c 1 ⋅ multiplicative.inverse (c 1)) ⋅ (- c 0)"
    using α_def ci i1 multiplicative.associative multiplicative.commutative by auto
  then have "eval α c = 𝟬"
    using aR c ci d eval_le1 inv by force
  then show ?thesis using aR by blast
qed

lemma degree_nz: 
  assumes a: "a ∈ poly_carrier" and nua: "¬ poly_unit a" and anz: "a ≠ 𝟬⇩P"
  shows "degree a ≠ 0"
  using degree_zero_imp_const[OF a] coeff_degree_nonzero[OF a anz]
  by (metis a nua poly_carrier_coeff_closed poly_const_unit)

text ‹A degree-1 factor of @{term p} supplies a root of @{term p}: if @{term "p = a ⊗⇩P b"} with
  @{term a} (or @{term b}) of degree @{text 1}, evaluation at the factor's root kills @{term p}.›
lemma degree1_factor_root:
  assumes a: "a ∈ poly_carrier" and "b ∈ poly_carrier" "p = a ⊗⇩P b" "degree a = 1"
  shows "∃α∈R. eval α p = 𝟬"
  using degree1_has_root[OF a] eval_mult assms by force

text ‹∗‹Degree-2, 3 irreducibility criterion.›  A cubic with no root is irreducible: a nontrivial
  factorisation @{term "p = a ⊗⇩P b"} has @{term "degree a + degree b = 2"} or 3 with both factors of
  degree @{text "≥ 1"}, so one of them has degree @{text 1} and hence a root of @{term p}.›
theorem degree23_no_root_irreducible:
  assumes p: "p ∈ poly_carrier" and d: "degree p ∈ {2,3}"
    and noroot: "⋀α. α ∈ R ⟹ eval α p ≠ 𝟬"
  shows "poly_irreducible p"
proof -
  have pnu: "¬ poly_unit p"
    using assms(2) poly_unit_imp_const by fastforce
  have False
    if a: "a ∈ poly_carrier" "¬ poly_unit a" and b: "b ∈ poly_carrier" "¬ poly_unit b" 
      and pab: "p = a ⊗⇩P b" for a b
  proof -
    have anz: "a ≠ 𝟬⇩P" and bnz: "b ≠ 𝟬⇩P"
      using pab d a b poly_mult_zero_left poly_mult_zero_right by auto
    ― ‹Degrees add to @{text 3}; neither factor is a unit, so neither has degree @{text 0}.›
    then have dsum: "degree a + degree b ∈ {2,3}"
      using d degree_mult pab that by force
    obtain "degree a ≠ 0" and "degree b ≠ 0"
      using a anz b bnz degree_nz by presburger
    then have "degree a = 1 ∨ degree b = 1" using dsum by auto
    with noroot a b degree1_factor_root pab poly_mult_comm show False by metis
  qed
  then show ?thesis unfolding poly_irreducible_def using p d pnu by auto
qed

subsection ‹Factorisation into irreducibles›

text ‹The product of a list of polynomials (right fold, empty list giving @{term "𝟭⇩P"}).›
definition poly_prod :: "(nat ⇒ 'a) list ⇒ (nat ⇒ 'a)"
  where "poly_prod fs ≡ foldr (⊗⇩P) fs 𝟭⇩P"

lemma poly_prod_Nil [simp]: "poly_prod [] = 𝟭⇩P"
  by (simp add: poly_prod_def)

lemma poly_prod_Cons [simp]: "poly_prod (f # fs) = f ⊗⇩P poly_prod fs"
  by (simp add: poly_prod_def)

lemma poly_prod_closed:
  "(⋀f. f ∈ set fs ⟹ f ∈ poly_carrier) ⟹ poly_prod fs ∈ poly_carrier"
  by (induct fs) (auto simp: poly_one_closed poly_mult_closed)

lemma poly_prod_append:
  assumes fs: "⋀f. f ∈ set fs ⟹ f ∈ poly_carrier"
    and gs: "⋀g. g ∈ set gs ⟹ g ∈ poly_carrier"
  shows "poly_prod (fs @ gs) = poly_prod fs ⊗⇩P poly_prod gs"
  using fs by (induct fs) (simp_all add: gs poly_mult_one_left poly_mult_assoc poly_prod_closed)

subsection ‹Splitting into linear factors›

text ‹A polynomial ∗‹splits› when it is a constant times a product of root factors, all of whose roots
  lie in the field.  Equivalently it is a product of linear factors: the constant carries the leading
  coefficient.  Taking that constant to range over the whole field, rather than the nonzero elements,
  lets @{term "𝟬⇩P"} split as well (empty list, zero constant), so no polynomial is excluded.›
definition splits :: "(nat ⇒ 'a) ⇒ bool"
  where "splits p ≡ (∃c as. c ∈ R ∧ set as ⊆ R
                            ∧ p = poly_const c ⊗⇩P poly_prod (List.map root_factor as))"

lemma splitsI:
  "⟦ c ∈ R; set as ⊆ R; p = poly_const c ⊗⇩P poly_prod (List.map root_factor as) ⟧
     ⟹ splits p"
  unfolding splits_def by blast

lemma splitsE:
  assumes "splits p"
  obtains c as where "c ∈ R" "set as ⊆ R"
    and "p = poly_const c ⊗⇩P poly_prod (List.map root_factor as)"
  using assms unfolding splits_def by blast

lemma splits_closed: "splits p ⟹ p ∈ poly_carrier"
proof (elim splitsE)
  fix c as assume c: "c ∈ R" and as: "set as ⊆ R"
    and peq: "p = poly_const c ⊗⇩P poly_prod (List.map root_factor as)"
  have "poly_prod (List.map root_factor as) ∈ poly_carrier"
    using as by (intro poly_prod_closed) (auto intro: root_factor_closed)
  then show "p ∈ poly_carrier" using peq poly_const_closed [OF c] by (simp add: poly_mult_closed)
qed

lemma splits_const:
  assumes c: "c ∈ R" shows "splits (poly_const c)"
proof (rule splitsI)
  show "poly_const c = poly_const c ⊗⇩P poly_prod (List.map root_factor [])"
    using poly_mult_one_right [OF poly_const_closed [OF c]] by simp
qed (use c in auto)

lemma splits_zero [simp]: "splits 𝟬⇩P"
  using splits_const [of 𝟬] by simp

lemma splits_root_factor:
  assumes a: "a ∈ R" shows "splits (root_factor a)"
proof (rule splitsI)
  show "root_factor a = poly_const 𝟭 ⊗⇩P poly_prod (List.map root_factor [a])"
    by (simp add: assms poly_mult_one_left poly_mult_one_right root_factor_closed)
qed (use a in auto)

text ‹Splitting is multiplicative: concatenate the root lists and multiply the constants.›
lemma splits_mult:
  assumes p: "splits p" and q: "splits q" shows "splits (p ⊗⇩P q)"
proof -
  obtain c as where c: "c ∈ R" and as: "set as ⊆ R"
    and peq: "p = poly_const c ⊗⇩P poly_prod (List.map root_factor as)"
    using p by (rule splitsE)
  obtain d bs where d: "d ∈ R" and bs: "set bs ⊆ R"
    and qeq: "q = poly_const d ⊗⇩P poly_prod (List.map root_factor bs)"
    using q by (rule splitsE)
  have pab: "poly_prod (List.map root_factor as) ∈ poly_carrier"
            "poly_prod (List.map root_factor bs) ∈ poly_carrier"
    using as bs by (auto intro!: poly_prod_closed root_factor_closed)
  have prod_app: "poly_prod (List.map root_factor (as @ bs))
                  = poly_prod (List.map root_factor as) ⊗⇩P poly_prod (List.map root_factor bs)"
    unfolding List.map_append
    using as bs by (force intro: intro: poly_prod_append root_factor_closed)
  show ?thesis
  proof (rule splitsI)
    show "c ⋅ d ∈ R" using c d by simp
    show "set (as @ bs) ⊆ R" using as bs by simp
    show "p ⊗⇩P q = poly_const (c ⋅ d) ⊗⇩P poly_prod (List.map root_factor (as @ bs))"
    proof -
      have cc: "poly_const c ∈ poly_carrier" using c by (rule poly_const_closed)
      have dc: "poly_const d ∈ poly_carrier" using d by (rule poly_const_closed)
      have "p ⊗⇩P q
            = (poly_const c ⊗⇩P poly_prod (List.map root_factor as))
              ⊗⇩P (poly_const d ⊗⇩P poly_prod (List.map root_factor bs))"
        using peq qeq by simp
      also have "… = (poly_const c ⊗⇩P poly_const d)
                       ⊗⇩P (poly_prod (List.map root_factor as) ⊗⇩P poly_prod (List.map root_factor bs))"
        using cc commutative_ring.mult_ac(3) dc pab poly_commutative_ring poly_mult_assoc
          poly_mult_closed by fastforce
      also have "… = poly_const (c ⋅ d) ⊗⇩P poly_prod (List.map root_factor (as @ bs))"
        using poly_const_mult [OF c d] prod_app by simp
      finally show ?thesis .
    qed
  qed
qed

text ‹∗‹A polynomial of degree one splits.›  Divide by the leading coefficient: the result is
  @{term "root_factor a"} for @{term a} the negated ratio of the two coefficients.  This is the base
  case that makes a factorisation into linear factors out of a factorisation into irreducibles all of
  whose factors have degree one.›
lemma degree_one_splits:
  assumes q: "q ∈ poly_carrier" and d: "degree q = 1"
  shows "splits q"
proof -
  have qnz: "q ≠ 𝟬⇩P" using d by auto
  have c: "q 1 ∈ R" and q0: "q 0 ∈ R" using q by (blast intro: poly_carrier_coeff_closed)+
  have cnz: "q 1 ≠ 𝟬"
    using lead_coeff_nonzero [OF q qnz] d by (simp add: lead_coeff_def)
  have inv: "multiplicative.invertible (q 1)" by (rule field_inverse [OF c cnz])
  define e where "e ≡ multiplicative.inverse (q 1)"
  define a where "a ≡ - (e ⋅ q 0)"
  obtain eR: "e ∈ R" and ce: "q 1 ⋅ e = 𝟭" using c e_def inv by force
  obtain eq0: "e ⋅ q 0 ∈ R" and aR: "a ∈ R" and nega: "- a = e ⋅ q 0" 
    using eR q0 a_def by simp
  have rf: "root_factor a ∈ poly_carrier" using aR by (rule root_factor_closed)
  ― ‹Multiplying by a constant scales each coefficient.›
  have scale: "(poly_const (q 1) ⊗⇩P root_factor a) j = q 1 ⋅ root_factor a j" for j
    using coeff_monom_mult [OF c rf, of 0 j] by (simp add: monom_0_eq_const)
  ― ‹The three coefficients of @{term "root_factor a"}.›
  have rf0: "root_factor a 0 = - a"
    by (simp add: eq0 monom_def nega poly_add_def poly_const_def poly_neg_def root_factor_def var_def)
  have rf1: "root_factor a 1 = 𝟭"
    by (simp add: root_factor_def var_def monom_def poly_const_def poly_add_def poly_neg_def)
  have rfj: "root_factor a j = 𝟬" if "j ≠ 0" "j ≠ 1" for j
    using aR coeff_gt_degree degree_root_factor rf that by auto
  have qeq: "q = poly_const (q 1) ⊗⇩P root_factor a"
  proof (rule ext)
    fix j
    show "q j = (poly_const (q 1) ⊗⇩P root_factor a) j"
    proof (cases "j = 0")
      case True
      then show ?thesis using True scale rf0
        using c ce eR multiplicative.associative multiplicative.left_unit nega q0 by force
    next
      case False
      then show ?thesis
      proof (cases "j = 1")
        case True
        then show ?thesis using scale rf1 c by simp
      next
        case False
        then show ?thesis
          using ‹j ≠ 0› d scale rfj coeff_gt_degree [OF q] c by simp
      qed
    qed
  qed
  show ?thesis
    using aR c qeq splits_const splits_mult splits_root_factor by metis
qed

lemma splits_poly_prod:
  assumes "⋀f. f ∈ set fs ⟹ splits f" shows "splits (poly_prod fs)"
  using assms
  by (induct fs; use splits_const splits_mult in force)


text ‹∗‹Existence of an irreducible factorisation.›  Every nonzero non-unit polynomial over a field
  is a product of a nonempty list of irreducibles.  By strong induction on the degree: an
  irreducible @{term p} is its own singleton factorisation; otherwise @{term "p = a ⊗⇩P b"} with
  both factors non-units --- hence, over a field, of strictly smaller degree --- and the induction
  hypothesis factors each.›
theorem factorization_into_irreducibles:
  assumes "p ∈ poly_carrier" and "p ≠ 𝟬⇩P" and "¬ poly_unit p"
  shows "∃fs. fs ≠ [] ∧ (∀f∈set fs. poly_irreducible f) ∧ p = poly_prod fs"
  using assms
proof (induct "degree p" arbitrary: p rule: less_induct)
  case (less p)
  show ?case
  proof (cases "poly_irreducible p")
    case True
    ― ‹@{term p} is its own factorisation.›
    have "p = poly_prod [p]" using less.prems by (simp add: poly_mult_one_right)
    moreover have "[p] ≠ [] ∧ (∀f∈set [p]. poly_irreducible f)" using True by simp
    ultimately show ?thesis by blast
  next
    case False
    ― ‹A nontrivial factorisation.›
    from less.prems False obtain a b where a: "a ∈ poly_carrier" and b: "b ∈ poly_carrier"
      and pab: "p = a ⊗⇩P b" and nua: "¬ poly_unit a" and nub: "¬ poly_unit b"
      unfolding poly_irreducible_def by blast
    have anz: "a ≠ 𝟬⇩P" and bnz: "b ≠ 𝟬⇩P"
      using pab less.prems(2) a b poly_mult_zero_left poly_mult_zero_right by auto
    have dsum: "degree a + degree b = degree p"
      using degree_mult[OF a b anz bnz] pab by simp
    ― ‹Neither factor has degree @{text 0}, so each has degree strictly below @{term "degree p"}.›
    obtain "degree a ≠ 0" and "degree b ≠ 0" and da: "degree a < degree p" and db: "degree b < degree p"
      using a anz b bnz degree_nz nua nub dsum by fastforce
    then have da: "degree a < degree p" and db: "degree b < degree p" using dsum by auto
    ― ‹Factor each smaller factor by the induction hypothesis, then concatenate.›
    obtain fa where fa: "fa ≠ []" "∀f∈set fa. poly_irreducible f" "a = poly_prod fa"
      using less.hyps[OF da a anz nua] by blast
    obtain fb where fb: "fb ≠ []" "∀f∈set fb. poly_irreducible f" "b = poly_prod fb"
      using less.hyps[OF db b bnz nub] by blast
    have "p = poly_prod (fa @ fb)"
    proof -
      have "poly_prod (fa @ fb) = poly_prod fa ⊗⇩P poly_prod fb"
        using fa(2) fb(2)
      proof (induct fa)
        case Nil
        then show ?case
          using b fb(3) poly_mult_one_left by auto
      next
        case (Cons g gs)
        then obtain gc: "g ∈ poly_carrier" and gsc: "poly_prod gs ∈ poly_carrier"
          by (simp add: Cons.prems(1) poly_irreducibleD_carrier poly_prod_closed)
        then show ?case
          using b fb(3) by (simp add: Cons.hyps Cons.prems gc gsc poly_mult_assoc)
      qed
      then show ?thesis using pab fa(3) fb(3) by simp
    qed
    moreover have "∀f∈set (fa @ fb). poly_irreducible f" using fa(2) fb(2) by auto
    ultimately show ?thesis
      using fa(1) by blast
  qed
qed


subsection ‹Monic polynomials and normalisation›

text ‹A polynomial is ∗‹monic› when it is nonzero with leading coefficient @{term 𝟭}.›
definition poly_monic :: "(nat ⇒ 'a) ⇒ bool"
  where "poly_monic p ≡ p ≠ 𝟬⇩P ∧ lead_coeff p = 𝟭"

text ‹Scaling a nonzero polynomial by a nonzero constant preserves its degree and scales its
  leading coefficient.›
lemma degree_poly_const_mult:
  assumes c: "c ∈ R" and cnz: "c ≠ 𝟬" and p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P"
  shows "degree (poly_const c ⊗⇩P p) = degree p"
  by (simp add: c cnz degree_mult p pnz poly_const_closed poly_const_unit poly_unit_imp_const)

lemma lead_coeff_poly_const_mult:
  assumes c: "c ∈ R" and cnz: "c ≠ 𝟬" and p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P"
  shows "lead_coeff (poly_const c ⊗⇩P p) = c ⋅ lead_coeff p"
proof -
  have cc: "poly_const c ∈ poly_carrier" using c by (rule poly_const_closed)
  have dc0: "degree (poly_const c) = 0" using degree_const_le by simp
  then have "lead_coeff (poly_const c ⊗⇩P p) = poly_const c (degree (poly_const c)) ⋅ p (degree p)"
    using coeff_mult_degree_add c cc cnz degree_poly_const_mult lead_coeff_def p pnz by fastforce
  then show ?thesis
    using dc0 lead_coeff_def poly_const_def by force
qed

text ‹Every nonzero polynomial has a monic associate, obtained by scaling by the inverse of its
  leading coefficient.›
theorem monic_associate_exists:
  assumes p: "p ∈ poly_carrier" and pnz: "p ≠ 𝟬⇩P"
  shows "∃u m. u ∈ R ∧ u ≠ 𝟬 ∧ m ∈ poly_carrier ∧ poly_monic m ∧ p = poly_const u ⊗⇩P m"
proof -
  define c where "c ≡ multiplicative.inverse (lead_coeff p)"
  have lc: "lead_coeff p ∈ R" 
    using p by (simp add: lead_coeff_def poly_carrier_coeff_closed)
  have inv: "multiplicative.invertible (lead_coeff p)"
    by (simp add: field_inverse lc lead_coeff_nonzero p pnz)
  have cR: "c ∈ R" unfolding c_def using lc inv by simp
  have cnz: "c ≠ 𝟬"
    using c_def inv lc multiplicative.invertible_inverse_invertible nontrivial
    by fastforce
  define m where "m ≡ poly_const c ⊗⇩P p"
  have mc: "m ∈ poly_carrier" unfolding m_def
    by (simp add: cR p poly_const_closed poly_mult_closed)
  ― ‹@{term m} is monic: its leading coefficient is @{text "c ⋅ lead_coeff p = 𝟭"}.›
  have cnzp: "poly_const c ≠ 𝟬⇩P" using cnz by (auto simp: poly_const_def poly_zero_def fun_eq_iff)
  have mnz: "m ≠ 𝟬⇩P" unfolding m_def
    using poly_no_zero_divisors[OF _ p] cnzp pnz cR poly_const_closed by force
  have eq1: "multiplicative.inverse (lead_coeff p) ⋅ lead_coeff p = 𝟭"
    using inv lc by simp
  have monic_m: "poly_monic m"
    using cR c_def cnz eq1 lead_coeff_poly_const_mult m_def mnz p pnz poly_monic_def by metis 
  ― ‹Recover @{term p} by scaling @{term m} by @{term "lead_coeff p"}.›
  have "poly_const (lead_coeff p) ⊗⇩P m = poly_const 𝟭 ⊗⇩P p"
    using cR c_def eq1 lc m_def p poly_const_closed poly_const_mult poly_mult_assoc poly_mult_comm
    by metis
   also have "… = p" 
    using p by (simp add: poly_mult_one_left)
  finally have "p = poly_const (lead_coeff p) ⊗⇩P m" ..
  then show ?thesis using lc lead_coeff_nonzero mc monic_m p pnz by blast
qed


subsection ‹The polynomial ring over a field is a principal ideal domain›

text ‹∗‹Every ideal of ‹F[X]› is principal.›  Given an ideal @{term J}, the zero ideal is
  generated by @{term "𝟬⇩P"}; otherwise pick a nonzero @{term b} of ∗‹least degree› in @{term J}.
  Dividing any @{term "a ∈ J"} by @{term b} (the division algorithm @{thm [source] poly_divide})
  leaves a remainder that again lies in @{term J} but has degree below that of @{term b}, so by
  minimality it must be zero: hence @{term a} is a multiple of @{term b}.  This is the structural
  fact behind Kronecker's construction --- it makes ‹(p)› maximal for irreducible @{term p}, and
  so @{text "F[X]/(p)"} a field.›
theorem poly_PID:
  assumes J: "Ideal J poly_carrier (⊕⇩P) (⊗⇩P) 𝟬⇩P 𝟭⇩P"
  shows "∃b. b ∈ poly_carrier ∧ J = {r ⊗⇩P b | r. r ∈ poly_carrier}"
proof -
  interpret J: Ideal J poly_carrier "(⊕⇩P)" "(⊗⇩P)" "𝟬⇩P" "𝟭⇩P" by (rule J)
  show ?thesis
  proof (cases "J = {𝟬⇩P}")
    case True
    then show ?thesis using poly_zero_closed by force
  next
    case False
    ― ‹Otherwise @{term J} contains a nonzero element, hence one of least degree.›
    define hasdeg where "hasdeg n ⟷ (∃a. a ∈ J ∧ a ≠ 𝟬⇩P ∧ degree a = n)" for n
    have "∃n. hasdeg n"
      using False unfolding hasdeg_def by blast
    then obtain b where bJ: "b ∈ J" and bnz: "b ≠ 𝟬⇩P"
      and bLeast: "degree b = (LEAST n. hasdeg n)"
      using hasdeg_def by (metis LeastI_ex)
    have bP: "b ∈ poly_carrier" using bJ J.additive.subset by blast
    ― ‹@{term b} has least degree among the nonzero elements of @{term J}.›
    have minimal: "degree b ≤ degree c" if "c ∈ J" "c ≠ 𝟬⇩P" for c
      by (metis Least_le bLeast hasdeg_def that)
    ― ‹@{term J} is exactly the principal ideal generated by @{term b}.›
    have "J = {r ⊗⇩P b | r. r ∈ poly_carrier}"
    proof (intro antisym subsetI)
      fix a assume aJ: "a ∈ J"
      have aP: "a ∈ poly_carrier" using aJ J.additive.subset by blast
      obtain q rem where q: "q ∈ poly_carrier" and rem: "rem ∈ poly_carrier"
        and aeq: "a = (b ⊗⇩P q) ⊕⇩P rem"
        and remd: "rem = 𝟬⇩P ∨ degree rem < degree b"
        using poly_divide[OF aP bP bnz] by blast
      have bqc: "b ⊗⇩P q ∈ poly_carrier" using bP q by (rule poly_mult_closed)
          ― ‹The multiple @{term "b ⊗⇩P q"} and its negative both lie in @{term J}.›
      have "J.additive.inverse (b ⊗⇩P q) ∈ J"
        by (simp add: J.Ideal(2) bJ q)
      then have negbqJ: "⊖⇩P (b ⊗⇩P q) ∈ J"
        using J.additive.inverse_equality bqc poly_add_neg poly_add_neg_right poly_neg_closed 
        by metis
      have rem_eq: "rem = (⊖⇩P (b ⊗⇩P q)) ⊕⇩P a"
        by (metis aeq bqc poly_add_comm poly_add_minus_cancel poly_neg_closed poly_neg_neg rem)
      then have remJ: "rem ∈ J"
        using negbqJ aJ by blast
      have "rem = 𝟬⇩P"
        using leD minimal remJ remd by auto
      then show "a ∈ {r ⊗⇩P b | r. r ∈ poly_carrier}" 
        using q aeq bP poly_mult_comm by auto
    qed (auto simp: J.Ideal bJ)
    then show ?thesis using bP by blast
  qed
qed

end


section ‹Pushing a Polynomial along a Ring Homomorphism›

text ‹Coefficientwise application of a ring homomorphism commutes with every operation of the
  polynomial ring..›

context
  fixes A :: "'b set" and add mult :: "'b ⇒ 'b ⇒ 'b" and z u :: 'b
    and B :: "'c set" and badd bmult :: "'c ⇒ 'c ⇒ 'c" and bz bu :: 'c
    and h :: "'b ⇒ 'c"
  assumes RA: "Ring A add mult z u" and RB: "Ring B badd bmult bz bu"
    and hB: "⋀y. y ∈ A ⟹ h y ∈ B"
    and hz: "h z = bz" and hu: "h u = bu"
    and hadd: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (add y y') = badd (h y) (h y')"
    and hmult: "⋀y y'. ⟦ y ∈ A; y' ∈ A ⟧ ⟹ h (mult y y') = bmult (h y) (h y')"
begin

lemma cmA: "commutative_monoid A add z"
  using RA by (simp add: Ring_def Abelian_Group_def)

lemma cmB: "commutative_monoid B badd bz"
  using RB by (simp add: Ring_def Abelian_Group_def)

lemma gpA: "Abelian_Group A add z"
  using RA by (simp add: Ring_def)

lemma gpB: "Abelian_Group B badd bz"
  using RB by (simp add: Ring_def)

lemma monA: "Monoid A mult u"
  using RA by (simp add: Ring_def)

lemma poly_zero_hom: "(λk. h (Ring.poly_zero z k)) = Ring.poly_zero bz"
  by (simp add: Ring.poly_zero_def [OF RA] Ring.poly_zero_def [OF RB] hz)

lemma poly_one_hom: "(λk. h (Ring.poly_one z u k)) = Ring.poly_one bz bu"
  by (auto simp add: Ring.poly_one_def [OF RA] Ring.poly_one_def [OF RB] hz hu)

lemma poly_const_hom: "(λk. h (Ring.poly_const z c k)) = Ring.poly_const bz (h c)"
  by (auto simp: Ring.poly_const_def [OF RA] Ring.poly_const_def [OF RB] hz)

lemma var_hom: "(λk. h (Ring.var z u k)) = Ring.var bz bu"
  using RA RB Ring.coeff_var[of A add mult z u] Ring.coeff_var[of B badd bmult bz bu] hu hz
  by auto

text ‹Coefficients of the polynomials named above, needed as closure side conditions below.›

lemma zA: "z ∈ A"
  using cmA by (metis Monoid_def commutative_monoid_def)

lemma uA: "u ∈ A"
  using monA by (metis Monoid_def)

lemma poly_const_coeff_closed: "c ∈ A ⟹ Ring.poly_const z c k ∈ A"
  using zA by (simp add: Ring.poly_const_def [OF RA])

lemma var_coeff_closed: "Ring.var z u k ∈ A"
  using zA uA by (simp add: Ring.var_def [OF RA] Ring.monom_def [OF RA])

lemma poly_add_hom:
  assumes p: "⋀k. p k ∈ A" and q: "⋀k. q k ∈ A"
  shows "(λk. h (Ring.poly_add add p q k)) = Ring.poly_add badd (λk. h (p k)) (λk. h (q k))"
  by (simp add: Ring.poly_add_def [OF RA] Ring.poly_add_def [OF RB] hadd p q)

text ‹The additive inverse is pinned by the equation it solves, so a homomorphism of the additive
  groups carries it along.›
lemma inverse_hom:
  assumes "y ∈ A"
  shows "h (Monoid.inverse A add z y) = Monoid.inverse B badd bz (h y)"
proof -
  interpret GA: Abelian_Group A add z by (rule gpA)
  interpret GB: Abelian_Group B badd bz by (rule gpB)
  have inv: "Monoid.inverse A add z y ∈ A" using assms by simp
  have 1: "badd (h y) (h (Monoid.inverse A add z y)) = bz"
    using GA.invertible GA.invertible_right_inverse hadd hz inv assms by metis
  then have 2: "badd (h (Monoid.inverse A add z y)) (h y) = bz"
    by (simp add: GB.commutative hB assms)
  show ?thesis
    using "1" "2" GB.inverse_equality hB inv assms by presburger
qed

lemma poly_neg_hom:
  assumes p: "⋀k. p k ∈ A"
  shows "(λk. h (Ring.poly_neg A add z p k)) = Ring.poly_neg B badd bz (λk. h (p k))"
  by (simp add: Ring.poly_neg_def [OF RA] Ring.poly_neg_def [OF RB] inverse_hom p)

lemma poly_neg_coeff_closed:
  assumes p: "⋀k. p k ∈ A"
  shows "Ring.poly_neg A add z p k ∈ A"
proof -
  interpret GA: Abelian_Group A add z by (rule gpA)
  show ?thesis using p by (simp add: Ring.poly_neg_def [OF RA])
qed

text ‹Convolution is a finite composite of products, so it pushes along by @{thm [source] fincomp_hom}.
  Only the two monoid premises are supplied: resolving the homomorphism premise inside ‹OF› sends
  unification into higher-order search, as the corresponding step of ‹eval_hom› also avoids.›
lemma poly_mult_hom:
  assumes p: "⋀k. p k ∈ A" and q: "⋀k. q k ∈ A"
  shows "(λk. h (Ring.poly_mult A add mult z p q k))
       = Ring.poly_mult B badd bmult bz (λk. h (p k)) (λk. h (q k))"
proof 
  fix k
  have cl: "(λi. mult (p i) (q (k - i))) ∈ {..k} → A"
    using Monoid.composition_closed monA p q by fastforce
  have "h (Ring.poly_mult A add mult z p q k)
        = commutative_monoid.fincomp B badd bz (λi. h (mult (p i) (q (k - i)))) {..k}"
    by (simp add: Ring.poly_mult_def [OF RA] fincomp_hom [OF cmA cmB] hB hz hadd cl)
  also have "… = Ring.poly_mult B badd bmult bz (λk. h (p k)) (λk. h (q k)) k"
    by (simp add: hmult p q Ring.poly_mult_def [OF RB])
  finally show "h (Ring.poly_mult A add mult z p q k)
              = Ring.poly_mult B badd bmult bz (λk. h (p k)) (λk. h (q k)) k" .
qed

lemma poly_mult_coeff_closed:
  assumes p: "⋀k. p k ∈ A" and q: "⋀k. q k ∈ A"
  shows "Ring.poly_mult A add mult z p q k ∈ A"
proof -
  have "(λi. mult (p i) (q (k - i))) ∈ {..k} → A"
    using Monoid.composition_closed monA p q by fastforce
  then show ?thesis
    by (simp add: Ring.poly_mult_def [OF RA] commutative_monoid.fincomp_closed [OF cmA])
qed

lemma poly_one_coeff_closed: "Ring.poly_one z u k ∈ A"
  using zA uA by (simp add: Ring.poly_one_def [OF RA])

text ‹The linear factor ‹X - a›, the list product, and hence the property of splitting.  The
  stronger structure is taken as an ordinary assumption of each lemma, so that the ring-level facts
  above keep their generality.›

lemma root_factor_coeff_closed:
  assumes "commutative_ring A add mult z u" "a ∈ A"
  shows "commutative_ring.root_factor A add z u a k ∈ A"
  by (meson assms RA Ring.poly_carrier_coeff_closed commutative_ring.root_factor_closed)

lemma root_factor_hom:
  assumes CA: "commutative_ring A add mult z u" and CB: "commutative_ring B badd bmult bz bu"
    and a: "a ∈ A"
  shows "(λk. h (commutative_ring.root_factor A add z u a k)) = commutative_ring.root_factor B badd bz bu (h a)"
proof -
  have cn: "⋀k. Ring.poly_const z a k ∈ A"
    using a by (rule poly_const_coeff_closed)
  have "(λk. h (commutative_ring.root_factor A add z u a k))
        = Ring.poly_add badd (λk. h (Ring.var z u k))
                    (λk. h (Ring.poly_neg A add z (Ring.poly_const z a) k))"
    using CA cn poly_add_hom poly_neg_coeff_closed var_coeff_closed
    by (metis commutative_ring.root_factor_def)
  also have "… = commutative_ring.root_factor B badd bz bu (h a)"
    by (simp add: var_hom poly_neg_hom [OF cn] poly_const_hom commutative_ring.root_factor_def [OF CB])
  finally show ?thesis .
qed

lemma poly_prod_coeff_closed:
  assumes FA: "Field A add mult z u"
    and fs: "⋀f. f ∈ set fs ⟹ (∀k. f k ∈ A)"
  shows "Field.poly_prod A add mult z u fs k ∈ A"
  using fs
proof (induct fs arbitrary: k)
  case Nil
  show ?case
    using poly_one_coeff_closed by (simp add: Field.poly_prod_Nil [OF FA])
next
  case (Cons g gs)
  then show ?case
    by (simp add: FA Field.poly_prod_Cons poly_mult_coeff_closed)
qed

lemma poly_prod_hom:
  assumes FA: "Field A add mult z u" and FB: "Field B badd bmult bz bu"
    and fs: "⋀f. f ∈ set fs ⟹ (∀k. f k ∈ A)"
  shows "(λk. h (Field.poly_prod A add mult z u fs k))
       = Field.poly_prod B badd bmult bz bu (List.map (λf k. h (f k)) fs)"
  using fs
proof (induct fs)
  case Nil
  show ?case
    by (simp add: Field.poly_prod_Nil [OF FA] Field.poly_prod_Nil [OF FB] poly_one_hom)
next
  case (Cons g gs)
  then have g: "⋀k. g k ∈ A" and gs: "⋀f. f ∈ set gs ⟹ (∀k. f k ∈ A)"
    by auto
  have pp: "⋀k. Field.poly_prod A add mult z u gs k ∈ A"
    using FA gs poly_prod_coeff_closed by blast
  have "(λk. h (Field.poly_prod A add mult z u (g # gs) k))
         = Ring.poly_mult B badd bmult bz (λk. h (g k)) (λk. h (Field.poly_prod A add mult z u gs k))"
    by (simp add: Field.poly_prod_Cons [OF FA] poly_mult_hom [OF g pp])
  also have "… = Field.poly_prod B badd bmult bz bu (List.map (λf k. h (f k)) (g # gs))"
    by (simp add: Field.poly_prod_Cons [OF FB] Cons.hyps [OF gs])
  finally show ?case .
qed

text ‹Splitting is preserved: the witnessing constant and root list are simply carried across.
  The steps use ‹simp only› throughout, to keep @{thm [source] map_map} from rewriting the two lists
  into composed form and so out of reach of the transport equations.›
theorem splits_hom:
  assumes FA: "Field A add mult z u" and FB: "Field B badd bmult bz bu"
    and sp: "Field.splits A add mult z u p"
  shows "Field.splits B badd bmult bz bu (λk. h (p k))"
proof -
  have CA: "commutative_ring A add mult z u" using FA by (simp add: Field_def)
  have CB: "commutative_ring B badd bmult bz bu" using FB by (simp add: Field_def)
  interpret B: commutative_ring B badd bmult bz bu
    using CB by auto
  from sp obtain c as where c: "c ∈ A" and as: "set as ⊆ A"
    and peq: "p = Ring.poly_mult A add mult z
                   (Ring.poly_const z c)
                   (Field.poly_prod A add mult z u
                      (List.map (commutative_ring.root_factor A add z u) as))"
    using Field.splits_def [OF FA] by blast
  have rf: "⋀f. f ∈ set (List.map (commutative_ring.root_factor A add z u) as) ⟹ (∀k. f k ∈ A)"
    using as by (auto simp: root_factor_coeff_closed [OF CA])
  then have pp: "⋀k. Field.poly_prod A add mult z u (List.map (commutative_ring.root_factor A add z u) as) k ∈ A"
    using FA poly_prod_coeff_closed by blast
  have mm: "List.map (λf k. h (f k)) (List.map (commutative_ring.root_factor A add z u) as)
            = List.map (commutative_ring.root_factor B badd bz bu) (List.map h as)"
    using as by (induct as) (simp_all add: root_factor_hom [OF CA CB])
  have "(λk. h (p k))
        = Ring.poly_mult B badd bmult bz (Ring.poly_const bz (h c))
            (Field.poly_prod B badd bmult bz bu
               (List.map (λf k. h (f k))
                  (List.map (commutative_ring.root_factor A add z u) as)))"
    using FA FB c poly_const_coeff_closed peq poly_const_hom poly_mult_hom poly_prod_hom pp rf 
    by presburger
  moreover have "set (List.map h as) ⊆ B" using as hB by auto
  ultimately show ?thesis
    using Field.splits_def [OF FB] mm c hB by metis
qed

end

end