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  

     2.1 --- a/src/HOL/NthRoot.thy	Tue Jun 30 15:58:12 2009 +0200
     2.2 +++ b/src/HOL/NthRoot.thy	Tue Jun 30 18:16:22 2009 +0200
     2.3 @@ -372,6 +372,41 @@
     2.4      using odd_pos [OF n] by (rule isCont_real_root)
     2.5  qed
     2.6  
     2.7 +lemma DERIV_even_real_root:
     2.8 +  assumes n: "0 < n" and "even n"
     2.9 +  assumes x: "x < 0"
    2.10 +  shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
    2.11 +proof (rule DERIV_inverse_function)
    2.12 +  show "x - 1 < x" by simp
    2.13 +  show "x < 0" using x .
    2.14 +next
    2.15 +  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
    2.16 +  proof (rule allI, rule impI, erule conjE)
    2.17 +    fix y assume "x - 1 < y" and "y < 0"
    2.18 +    hence "root n (-y) ^ n = -y" using `0 < n` by simp
    2.19 +    with real_root_minus[OF `0 < n`] and `even n`
    2.20 +    show "- (root n y ^ n) = y" by simp
    2.21 +  qed
    2.22 +next
    2.23 +  show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
    2.24 +    by  (auto intro!: DERIV_intros)
    2.25 +  show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
    2.26 +    using n x by simp
    2.27 +  show "isCont (root n) x"
    2.28 +    using n by (rule isCont_real_root)
    2.29 +qed
    2.30 +
    2.31 +lemma DERIV_real_root_generic:
    2.32 +  assumes "0 < n" and "x \<noteq> 0"
    2.33 +  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    2.34 +  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
    2.35 +  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
    2.36 +  shows "DERIV (root n) x :> D"
    2.37 +using assms by (cases "even n", cases "0 < x",
    2.38 +  auto intro: DERIV_real_root[THEN DERIV_cong]
    2.39 +              DERIV_odd_real_root[THEN DERIV_cong]
    2.40 +              DERIV_even_real_root[THEN DERIV_cong])
    2.41 +
    2.42  subsection {* Square Root *}
    2.43  
    2.44  definition
    2.45 @@ -456,9 +491,21 @@
    2.46  lemma isCont_real_sqrt: "isCont sqrt x"
    2.47  unfolding sqrt_def by (rule isCont_real_root [OF pos2])
    2.48  
    2.49 +lemma DERIV_real_sqrt_generic:
    2.50 +  assumes "x \<noteq> 0"
    2.51 +  assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
    2.52 +  assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
    2.53 +  shows "DERIV sqrt x :> D"
    2.54 +  using assms unfolding sqrt_def
    2.55 +  by (auto intro!: DERIV_real_root_generic)
    2.56 +
    2.57  lemma DERIV_real_sqrt:
    2.58    "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
    2.59 -unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
    2.60 +  using DERIV_real_sqrt_generic by simp
    2.61 +
    2.62 +declare
    2.63 +  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    2.64 +  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    2.65  
    2.66  lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
    2.67  apply auto

     3.1 --- a/src/HOL/Transcendental.thy	Tue Jun 30 15:58:12 2009 +0200
     3.2 +++ b/src/HOL/Transcendental.thy	Tue Jun 30 18:16:22 2009 +0200
     3.3 @@ -1362,6 +1362,12 @@
     3.4  by (rule DERIV_cos [THEN DERIV_isCont])
     3.5  
     3.6  
     3.7 +declare
     3.8 +  DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
     3.9 +  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.10 +  DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.11 +  DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.12 +
    3.13  subsection {* Properties of Sine and Cosine *}
    3.14  
    3.15  lemma sin_zero [simp]: "sin 0 = 0"
    3.16 @@ -1513,12 +1519,6 @@
    3.17  apply (rule DERIV_cos, auto)
    3.18  done
    3.19  
    3.20 -lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
    3.21 -                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
    3.22 -                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
    3.23 -                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
    3.24 -                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
    3.25 -
    3.26  (* lemma *)
    3.27  lemma lemma_DERIV_sin_cos_add:
    3.28       "\<forall>x.  
    3.29 @@ -1722,7 +1722,7 @@
    3.30  apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
    3.31  apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
    3.32  done
    3.33 -    
    3.34 +
    3.35  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    3.36  by (simp add: pi_def)
    3.37  
    3.38 @@ -2500,6 +2500,11 @@
    3.39  apply (simp, simp, simp, rule isCont_arctan)
    3.40  done
    3.41  
    3.42 +declare
    3.43 +  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.44 +  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.45 +  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
    3.46 +
    3.47  subsection {* More Theorems about Sin and Cos *}
    3.48  
    3.49  lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"