# HG changeset patch
# User haftmann
# Date 1507494499 -7200
# Node ID 7ba45c30250cb06024c39224da26c4196596a3e5
# Parent  39bb2462e681216b98edba7279baafc4aad7f90e
tuned

diff -r 39bb2462e681 -r 7ba45c30250c src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:19 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:19 2017 +0200
@@ -596,6 +596,10 @@
 lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
   by (cases "c = 0") (simp_all add: degree_monom_eq)
 
+lemma last_coeffs_eq_coeff_degree:
+  "last (coeffs p) = lead_coeff p" if "p \<noteq> 0"
+  using that by (simp add: coeffs_def)
+  
 
 subsection \<open>Addition and subtraction\<close>
 
@@ -1110,7 +1114,7 @@
   also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
     by (intro sum.cong) simp_all
   also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))"
-    by (simp add: sum.delta')
+    by simp
   finally show ?thesis .
 qed
 
@@ -1162,8 +1166,9 @@
 lemma coeffs_map_poly':
   assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
   shows "coeffs (map_poly f p) = map f (coeffs p)"
-  using assms by (simp add: coeffs_map_poly no_trailing_map strip_while_idem_iff)
-    (metis comp_def no_leading_def no_trailing_coeffs)
+  using assms
+  by (auto simp add: coeffs_map_poly strip_while_idem_iff
+    last_coeffs_eq_coeff_degree no_trailing_unfold last_map)
 
 lemma set_coeffs_map_poly:
   "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
@@ -1494,9 +1499,6 @@
   for p :: "'a::linordered_idom poly"
   by (induct p) (auto simp: pos_poly_pCons)
 
-lemma last_coeffs_eq_coeff_degree: "p \<noteq> 0 \<Longrightarrow> last (coeffs p) = coeff p (degree p)"
-  by (simp add: coeffs_def)
-
 lemma pos_poly_coeffs [code]: "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof