author haftmann Sun, 08 Oct 2017 22:28:19 +0200 changeset 66799 7ba45c30250c parent 66798 39bb2462e681 child 66800 128e9ed9f63c
tuned
```--- 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 @@
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)
+

@@ -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
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)
+  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)"