--- 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 *}
--- 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
--- 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"