src/HOL/Deriv.thy
 changeset 31880 6fb86c61747c parent 31404 05d2eddc5d41 child 31899 1a7ade46061b
```     1.1 --- a/src/HOL/Deriv.thy	Tue Jun 30 15:58:12 2009 +0200
1.2 +++ b/src/HOL/Deriv.thy	Tue Jun 30 18:16:22 2009 +0200
1.3 @@ -115,12 +115,16 @@
1.4
1.5  text{*Differentiation of finite sum*}
1.6
1.7 +lemma DERIV_setsum:
1.8 +  assumes "finite S"
1.9 +  and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
1.10 +  shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
1.11 +  using assms by induct (auto intro!: DERIV_add)
1.12 +
1.13  lemma DERIV_sumr [rule_format (no_asm)]:
1.14       "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
1.15        --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
1.16 -apply (induct "n")
1.18 -done
1.19 +  by (auto intro: DERIV_setsum)
1.20
1.21  text{*Alternative definition for differentiability*}
1.22
1.23 @@ -216,7 +220,6 @@
1.24    shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
1.25  by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
1.26
1.27 -
1.28  text {* Caratheodory formulation of derivative at a point *}
1.29
1.30  lemma CARAT_DERIV:
1.31 @@ -308,6 +311,30 @@
1.32  lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
1.33  by auto
1.34
1.35 +text {* DERIV_intros *}
1.36 +
1.37 +ML{*
1.38 +structure DerivIntros =
1.39 +  NamedThmsFun(val name = "DERIV_intros"
1.40 +               val description = "DERIV introduction rules");
1.41 +*}
1.42 +setup DerivIntros.setup
1.43 +
1.44 +lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
1.45 +  by simp
1.46 +
1.47 +declare
1.48 +  DERIV_const[THEN DERIV_cong, DERIV_intros]
1.49 +  DERIV_ident[THEN DERIV_cong, DERIV_intros]