author haftmann Sun Oct 08 22:28:19 2017 +0200 (19 months ago) changeset 66799 7ba45c30250c parent 66798 39bb2462e681 child 66800 128e9ed9f63c
tuned
```     1.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:19 2017 +0200
1.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:19 2017 +0200
1.3 @@ -596,6 +596,10 @@
1.4  lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
1.5    by (cases "c = 0") (simp_all add: degree_monom_eq)
1.6
1.7 +lemma last_coeffs_eq_coeff_degree:
1.8 +  "last (coeffs p) = lead_coeff p" if "p \<noteq> 0"
1.9 +  using that by (simp add: coeffs_def)
1.10 +
1.11
1.12  subsection \<open>Addition and subtraction\<close>
1.13
1.14 @@ -1110,7 +1114,7 @@
1.15    also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k - i) else 0))"
1.16      by (intro sum.cong) simp_all
1.17    also have "\<dots> = (if k < n then 0 else c * coeff p (k - n))"
1.18 -    by (simp add: sum.delta')
1.19 +    by simp
1.20    finally show ?thesis .
1.21  qed
1.22
1.23 @@ -1162,8 +1166,9 @@
1.24  lemma coeffs_map_poly':
1.25    assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0"
1.26    shows "coeffs (map_poly f p) = map f (coeffs p)"
1.27 -  using assms by (simp add: coeffs_map_poly no_trailing_map strip_while_idem_iff)
1.28 -    (metis comp_def no_leading_def no_trailing_coeffs)
1.29 +  using assms
1.30 +  by (auto simp add: coeffs_map_poly strip_while_idem_iff
1.31 +    last_coeffs_eq_coeff_degree no_trailing_unfold last_map)
1.32
1.33  lemma set_coeffs_map_poly:
1.34    "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)"
1.35 @@ -1494,9 +1499,6 @@
1.36    for p :: "'a::linordered_idom poly"
1.37    by (induct p) (auto simp: pos_poly_pCons)
1.38
1.39 -lemma last_coeffs_eq_coeff_degree: "p \<noteq> 0 \<Longrightarrow> last (coeffs p) = coeff p (degree p)"
1.40 -  by (simp add: coeffs_def)
1.41 -
1.42  lemma pos_poly_coeffs [code]: "pos_poly p \<longleftrightarrow> (let as = coeffs p in as \<noteq> [] \<and> last as > 0)"
1.43    (is "?lhs \<longleftrightarrow> ?rhs")
1.44  proof
```