# HG changeset patch
# User hoelzl
# Date 1246378582 -7200
# Node ID 6fb86c61747c6944728903979dba09a0c53d38dc
# Parent  39bff8d9b032c861818cd3606739d910ce349ec4
Added DERIV_intros

diff -r 39bff8d9b032 -r 6fb86c61747c src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Jun 30 15:58:12 2009 +0200
+++ b/src/HOL/Deriv.thy	Tue Jun 30 18:16:22 2009 +0200
@@ -115,12 +115,16 @@
 
 text{*Differentiation of finite sum*}
 
+lemma DERIV_setsum:
+  assumes "finite S"
+  and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
+  shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
+  using assms by induct (auto intro!: DERIV_add)
+
 lemma DERIV_sumr [rule_format (no_asm)]:
      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
+  by (auto intro: DERIV_setsum)
 
 text{*Alternative definition for differentiability*}
 
@@ -216,7 +220,6 @@
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
 
-
 text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV:
@@ -308,6 +311,30 @@
 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
 by auto
 
+text {* DERIV_intros *}
+
+ML{*
+structure DerivIntros =
+  NamedThmsFun(val name = "DERIV_intros"
+               val description = "DERIV introduction rules");
+*}
+setup DerivIntros.setup
+
+lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
+  by simp
+
+declare
+  DERIV_const[THEN DERIV_cong, DERIV_intros]
+  DERIV_ident[THEN DERIV_cong, DERIV_intros]
+  DERIV_add[THEN DERIV_cong, DERIV_intros]
+  DERIV_minus[THEN DERIV_cong, DERIV_intros]
+  DERIV_mult[THEN DERIV_cong, DERIV_intros]
+  DERIV_diff[THEN DERIV_cong, DERIV_intros]
+  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+  DERIV_divide[THEN DERIV_cong, DERIV_intros]
+  DERIV_power[where 'a=real, THEN DERIV_cong,
+              unfolded real_of_nat_def[symmetric], DERIV_intros]
+  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
 
 subsection {* Differentiability predicate *}
 
diff -r 39bff8d9b032 -r 6fb86c61747c src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Jun 30 15:58:12 2009 +0200
+++ b/src/HOL/NthRoot.thy	Tue Jun 30 18:16:22 2009 +0200
@@ -372,6 +372,41 @@
     using odd_pos [OF n] by (rule isCont_real_root)
 qed
 
+lemma DERIV_even_real_root:
+  assumes n: "0 < n" and "even n"
+  assumes x: "x < 0"
+  shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
+proof (rule DERIV_inverse_function)
+  show "x - 1 < x" by simp
+  show "x < 0" using x .
+next
+  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
+  proof (rule allI, rule impI, erule conjE)
+    fix y assume "x - 1 < y" and "y < 0"
+    hence "root n (-y) ^ n = -y" using `0 < n` by simp
+    with real_root_minus[OF `0 < n`] and `even n`
+    show "- (root n y ^ n) = y" by simp
+  qed
+next
+  show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
+    by  (auto intro!: DERIV_intros)
+  show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
+    using n x by simp
+  show "isCont (root n) x"
+    using n by (rule isCont_real_root)
+qed
+
+lemma DERIV_real_root_generic:
+  assumes "0 < n" and "x \<noteq> 0"
+  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  shows "DERIV (root n) x :> D"
+using assms by (cases "even n", cases "0 < x",
+  auto intro: DERIV_real_root[THEN DERIV_cong]
+              DERIV_odd_real_root[THEN DERIV_cong]
+              DERIV_even_real_root[THEN DERIV_cong])
+
 subsection {* Square Root *}
 
 definition
@@ -456,9 +491,21 @@
 lemma isCont_real_sqrt: "isCont sqrt x"
 unfolding sqrt_def by (rule isCont_real_root [OF pos2])
 
+lemma DERIV_real_sqrt_generic:
+  assumes "x \<noteq> 0"
+  assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
+  assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
+  shows "DERIV sqrt x :> D"
+  using assms unfolding sqrt_def
+  by (auto intro!: DERIV_real_root_generic)
+
 lemma DERIV_real_sqrt:
   "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
-unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
+  using DERIV_real_sqrt_generic by simp
+
+declare
+  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
 
 lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
 apply auto
diff -r 39bff8d9b032 -r 6fb86c61747c src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jun 30 15:58:12 2009 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jun 30 18:16:22 2009 +0200
@@ -1362,6 +1362,12 @@
 by (rule DERIV_cos [THEN DERIV_isCont])
 
 
+declare
+  DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* Properties of Sine and Cosine *}
 
 lemma sin_zero [simp]: "sin 0 = 0"
@@ -1513,12 +1519,6 @@
 apply (rule DERIV_cos, auto)
 done
 
-lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
-                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
-                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
-                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
-                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
-
 (* lemma *)
 lemma lemma_DERIV_sin_cos_add:
      "\<forall>x.  
@@ -1722,7 +1722,7 @@
 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
 done
-    
+
 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
 by (simp add: pi_def)
 
@@ -2500,6 +2500,11 @@
 apply (simp, simp, simp, rule isCont_arctan)
 done
 
+declare
+  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* More Theorems about Sin and Cos *}
 
 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"