diff -r 1d0cb3f003d4 -r 76720aeab21e src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Feb 19 14:12:29 2024 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Feb 21 10:46:22 2024 +0000
@@ -464,7 +464,7 @@
   by (simp add: is_zero_def null_def)
 
 
-subsubsection \<open>Reconstructing the polynomial from the list\<close>
+text \<open>Reconstructing the polynomial from the list\<close>
   \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>
 
 definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly"
@@ -1296,6 +1296,15 @@
   "lead_coeff (of_int k) = of_int k"
   by (simp add: of_int_poly)
 
+lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n"
+  by (simp add: of_nat_poly)
+
+lemma poly_of_int [simp]: "poly (of_int n) x = of_int n"
+  by (simp add: of_int_poly) 
+
+lemma poly_numeral [simp]: "poly (numeral n) x = numeral n"
+  by (metis of_nat_numeral poly_of_nat)
+
 lemma numeral_poly: "numeral n = [:numeral n:]"
 proof -
   have "numeral n = of_nat (numeral n)"
@@ -1841,6 +1850,12 @@
     by simp
 qed
 
+lemma order_gt_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p > 0 \<longleftrightarrow> poly p x = 0"
+  by (subst order_root) auto
+
+lemma order_eq_0_iff: "p \<noteq> 0 \<Longrightarrow> order x p = 0 \<longleftrightarrow> poly p x \<noteq> 0"
+  by (subst order_root) auto
+
 text \<open>Next three lemmas contributed by Wenda Li\<close>
 lemma order_1_eq_0 [simp]:"order x 1 = 0"
   by (metis order_root poly_1 zero_neq_one)
@@ -2176,6 +2191,68 @@
   qed
 qed
 
+lemma coeff_pcompose_monom_linear [simp]:
+  fixes p :: "'a :: comm_ring_1 poly"
+  shows "coeff (pcompose p (monom c (Suc 0))) k = c ^ k * coeff p k"
+  by (induction p arbitrary: k)
+     (auto simp: coeff_pCons coeff_monom_mult pcompose_pCons split: nat.splits)
+
+lemma of_nat_mult_conv_smult: "of_nat n * P = smult (of_nat n) P"
+  by (simp add: monom_0 of_nat_monom)
+
+lemma numeral_mult_conv_smult: "numeral n * P = smult (numeral n) P"
+  by (simp add: numeral_poly)
+
+lemma sum_order_le_degree:
+  assumes "p \<noteq> 0"
+  shows   "(\<Sum>x | poly p x = 0. order x p) \<le> degree p"
+  using assms
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  case (less p)
+  show ?case
+  proof (cases "\<exists>x. poly p x = 0")
+    case False
+    thus ?thesis
+      by auto
+  next
+    case True
+    then obtain x where x: "poly p x = 0"
+      by auto
+    have "[:-x, 1:] ^ order x p dvd p"
+      by (simp add: order_1)
+    then obtain q where q: "p = [:-x, 1:] ^ order x p * q"
+      by (elim dvdE)
+    have [simp]: "q \<noteq> 0"
+      using q less.prems by auto
+    have "order x p = order x p + order x q"
+      by (subst q, subst order_mult) (auto simp: order_power_n_n)
+    hence "order x q = 0"
+      by auto
+    hence [simp]: "poly q x \<noteq> 0"
+      by (simp add: order_root)
+    have deg_p: "degree p = degree q + order x p"
+      by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq)
+    moreover have "order x p > 0"
+      using x less.prems by (simp add: order_root)
+    ultimately have "degree q < degree p"
+      by linarith
+    hence "(\<Sum>x | poly q x = 0. order x q) \<le> degree q"
+      by (intro less.hyps) auto
+    hence "order x p + (\<Sum>x | poly q x = 0. order x q) \<le> degree p"
+      by (simp add: deg_p)
+    also have "{y. poly q y = 0} = {y. poly p y = 0} - {x}"
+      by (subst q) auto
+    also have "(\<Sum>y \<in> {y. poly p y = 0} - {x}. order y q) =
+               (\<Sum>y \<in> {y. poly p y = 0} - {x}. order y p)"
+      by (intro sum.cong refl, subst q)
+         (auto simp: order_mult order_power_n_n intro!: order_0I)
+    also have "order x p + \<dots> = (\<Sum>y \<in> insert x ({y. poly p y = 0} - {x}). order y p)"
+      using \<open>p \<noteq> 0\<close> by (subst sum.insert) (auto simp: poly_roots_finite)
+    also have "insert x ({y. poly p y = 0} - {x}) = {y. poly p y = 0}"
+      using \<open>poly p x = 0\<close> by auto
+    finally show ?thesis .
+  qed
+qed
 
 subsection \<open>Closure properties of coefficients\<close>
 
@@ -2858,6 +2935,12 @@
     by (simp add: rsquarefree_def order_root)
 qed
 
+lemma has_field_derivative_poly [derivative_intros]:
+  assumes "(f has_field_derivative f') (at x within A)"
+  shows   "((\<lambda>x. poly p (f x)) has_field_derivative
+             (f' * poly (pderiv p) (f x))) (at x within A)"
+  using DERIV_chain[OF poly_DERIV assms, of p] by (simp add: o_def mult_ac)
+
 
 subsection \<open>Algebraic numbers\<close>
 
@@ -5138,7 +5221,6 @@
     by (simp_all add: content_mult mult_ac)
 qed (auto simp: content_mult)
 
-
 no_notation cCons (infixr "##" 65)
 
 end