tuned
authorhaftmann
Sun Oct 08 22:28:19 2017 +0200 (19 months ago)
changeset 667997ba45c30250c
parent 66798 39bb2462e681
child 66800 128e9ed9f63c
tuned
src/HOL/Computational_Algebra/Polynomial.thy
     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