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.17 -apply (auto intro: DERIV_add)
    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]
    1.50 +  DERIV_add[THEN DERIV_cong, DERIV_intros]
    1.51 +  DERIV_minus[THEN DERIV_cong, DERIV_intros]
    1.52 +  DERIV_mult[THEN DERIV_cong, DERIV_intros]
    1.53 +  DERIV_diff[THEN DERIV_cong, DERIV_intros]
    1.54 +  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
    1.55 +  DERIV_divide[THEN DERIV_cong, DERIV_intros]
    1.56 +  DERIV_power[where 'a=real, THEN DERIV_cong,
    1.57 +              unfolded real_of_nat_def[symmetric], DERIV_intros]
    1.58 +  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
    1.59  
    1.60  subsection {* Differentiability predicate *}
    1.61