src/HOL/Library/Poly_Deriv.thy
changeset 52380 3cc46b8cca5e
parent 47108 2a1953f0d20d
child 56181 2aa0b19e74f3
     1.1 --- a/src/HOL/Library/Poly_Deriv.thy	Sat Jun 15 17:19:23 2013 +0200
     1.2 +++ b/src/HOL/Library/Poly_Deriv.thy	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -11,26 +11,41 @@
     1.4  
     1.5  subsection {* Derivatives of univariate polynomials *}
     1.6  
     1.7 -definition
     1.8 -  pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly" where
     1.9 -  "pderiv = poly_rec 0 (\<lambda>a p p'. p + pCons 0 p')"
    1.10 +function pderiv :: "'a::real_normed_field poly \<Rightarrow> 'a poly"
    1.11 +where
    1.12 +  [simp del]: "pderiv (pCons a p) = (if p = 0 then 0 else p + pCons 0 (pderiv p))"
    1.13 +  by (auto intro: pCons_cases)
    1.14 +
    1.15 +termination pderiv
    1.16 +  by (relation "measure degree") simp_all
    1.17  
    1.18 -lemma pderiv_0 [simp]: "pderiv 0 = 0"
    1.19 -  unfolding pderiv_def by (simp add: poly_rec_0)
    1.20 +lemma pderiv_0 [simp]:
    1.21 +  "pderiv 0 = 0"
    1.22 +  using pderiv.simps [of 0 0] by simp
    1.23  
    1.24 -lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
    1.25 -  unfolding pderiv_def by (simp add: poly_rec_pCons)
    1.26 +lemma pderiv_pCons:
    1.27 +  "pderiv (pCons a p) = p + pCons 0 (pderiv p)"
    1.28 +  by (simp add: pderiv.simps)
    1.29  
    1.30  lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
    1.31    apply (induct p arbitrary: n, simp)
    1.32    apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
    1.33    done
    1.34  
    1.35 +primrec pderiv_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list"
    1.36 +where
    1.37 +  "pderiv_coeffs [] = []"
    1.38 +| "pderiv_coeffs (x # xs) = plus_coeffs xs (cCons 0 (pderiv_coeffs xs))"
    1.39 +
    1.40 +lemma coeffs_pderiv [code abstract]:
    1.41 +  "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
    1.42 +  by (rule sym, induct p) (simp_all add: pderiv_pCons coeffs_plus_eq_plus_coeffs cCons_def)
    1.43 +
    1.44  lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
    1.45    apply (rule iffI)
    1.46    apply (cases p, simp)
    1.47 -  apply (simp add: expand_poly_eq coeff_pderiv del: of_nat_Suc)
    1.48 -  apply (simp add: expand_poly_eq coeff_pderiv coeff_eq_0)
    1.49 +  apply (simp add: poly_eq_iff coeff_pderiv del: of_nat_Suc)
    1.50 +  apply (simp add: poly_eq_iff coeff_pderiv coeff_eq_0)
    1.51    done
    1.52  
    1.53  lemma degree_pderiv: "degree (pderiv p) = degree p - 1"
    1.54 @@ -47,16 +62,16 @@
    1.55  by (simp add: pderiv_pCons)
    1.56  
    1.57  lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
    1.58 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
    1.59 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
    1.60  
    1.61  lemma pderiv_minus: "pderiv (- p) = - pderiv p"
    1.62 -by (rule poly_ext, simp add: coeff_pderiv)
    1.63 +by (rule poly_eqI, simp add: coeff_pderiv)
    1.64  
    1.65  lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
    1.66 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
    1.67 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
    1.68  
    1.69  lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
    1.70 -by (rule poly_ext, simp add: coeff_pderiv algebra_simps)
    1.71 +by (rule poly_eqI, simp add: coeff_pderiv algebra_simps)
    1.72  
    1.73  lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
    1.74  apply (induct p)
    1.75 @@ -75,6 +90,7 @@
    1.76  apply (simp add: algebra_simps) (* FIXME *)
    1.77  done
    1.78  
    1.79 +
    1.80  lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
    1.81  by (simp add: DERIV_cmult mult_commute [of _ c])
    1.82