src/HOL/NthRoot.thy
 changeset 31880 6fb86c61747c parent 31014 79f0858d9d49 child 35216 7641e8d831d2
```     1.1 --- a/src/HOL/NthRoot.thy	Tue Jun 30 15:58:12 2009 +0200
1.2 +++ b/src/HOL/NthRoot.thy	Tue Jun 30 18:16:22 2009 +0200
1.3 @@ -372,6 +372,41 @@
1.4      using odd_pos [OF n] by (rule isCont_real_root)
1.5  qed
1.6
1.7 +lemma DERIV_even_real_root:
1.8 +  assumes n: "0 < n" and "even n"
1.9 +  assumes x: "x < 0"
1.10 +  shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
1.11 +proof (rule DERIV_inverse_function)
1.12 +  show "x - 1 < x" by simp
1.13 +  show "x < 0" using x .
1.14 +next
1.15 +  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
1.16 +  proof (rule allI, rule impI, erule conjE)
1.17 +    fix y assume "x - 1 < y" and "y < 0"
1.18 +    hence "root n (-y) ^ n = -y" using `0 < n` by simp
1.19 +    with real_root_minus[OF `0 < n`] and `even n`
1.20 +    show "- (root n y ^ n) = y" by simp
1.21 +  qed
1.22 +next
1.23 +  show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
1.24 +    by  (auto intro!: DERIV_intros)
1.25 +  show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
1.26 +    using n x by simp
1.27 +  show "isCont (root n) x"
1.28 +    using n by (rule isCont_real_root)
1.29 +qed
1.30 +
1.31 +lemma DERIV_real_root_generic:
1.32 +  assumes "0 < n" and "x \<noteq> 0"
1.33 +  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
1.34 +  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
1.35 +  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
1.36 +  shows "DERIV (root n) x :> D"
1.37 +using assms by (cases "even n", cases "0 < x",
1.38 +  auto intro: DERIV_real_root[THEN DERIV_cong]
1.39 +              DERIV_odd_real_root[THEN DERIV_cong]
1.40 +              DERIV_even_real_root[THEN DERIV_cong])
1.41 +
1.42  subsection {* Square Root *}
1.43
1.44  definition
1.45 @@ -456,9 +491,21 @@
1.46  lemma isCont_real_sqrt: "isCont sqrt x"
1.47  unfolding sqrt_def by (rule isCont_real_root [OF pos2])
1.48
1.49 +lemma DERIV_real_sqrt_generic:
1.50 +  assumes "x \<noteq> 0"
1.51 +  assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
1.52 +  assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
1.53 +  shows "DERIV sqrt x :> D"
1.54 +  using assms unfolding sqrt_def
1.55 +  by (auto intro!: DERIV_real_root_generic)
1.56 +
1.57  lemma DERIV_real_sqrt:
1.58    "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
1.59 -unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
1.60 +  using DERIV_real_sqrt_generic by simp
1.61 +
1.62 +declare
1.63 +  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.64 +  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
1.65
1.66  lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
1.67  apply auto
```