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.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
```