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