more proofs about differentiable
authorhuffman
Wed Dec 24 11:17:37 2008 -0800 (2008-12-24)
changeset 291696a5f1d8d7344
parent 29168 ff13de554ed0
child 29170 dad3933c88dd
more proofs about differentiable
src/HOL/Deriv.thy
     1.1 --- a/src/HOL/Deriv.thy	Wed Dec 24 09:26:18 2008 -0800
     1.2 +++ b/src/HOL/Deriv.thy	Wed Dec 24 11:17:37 2008 -0800
     1.3 @@ -20,12 +20,6 @@
     1.4            ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
     1.5    "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
     1.6  
     1.7 -definition
     1.8 -  differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
     1.9 -    (infixl "differentiable" 60) where
    1.10 -  "f differentiable x = (\<exists>D. DERIV f x :> D)"
    1.11 -
    1.12 -
    1.13  consts
    1.14    Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
    1.15  primrec
    1.16 @@ -316,63 +310,104 @@
    1.17  
    1.18  subsection {* Differentiability predicate *}
    1.19  
    1.20 +definition
    1.21 +  differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
    1.22 +    (infixl "differentiable" 60) where
    1.23 +  "f differentiable x = (\<exists>D. DERIV f x :> D)"
    1.24 +
    1.25 +lemma differentiableE [elim?]:
    1.26 +  assumes "f differentiable x"
    1.27 +  obtains df where "DERIV f x :> df"
    1.28 +  using prems unfolding differentiable_def ..
    1.29 +
    1.30  lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
    1.31  by (simp add: differentiable_def)
    1.32  
    1.33  lemma differentiableI: "DERIV f x :> D ==> f differentiable x"
    1.34  by (force simp add: differentiable_def)
    1.35  
    1.36 -lemma differentiable_const: "(\<lambda>z. a) differentiable x"
    1.37 -  apply (unfold differentiable_def)
    1.38 -  apply (rule_tac x=0 in exI)
    1.39 -  apply simp
    1.40 -  done
    1.41 +lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x"
    1.42 +  by (rule DERIV_ident [THEN differentiableI])
    1.43 +
    1.44 +lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x"
    1.45 +  by (rule DERIV_const [THEN differentiableI])
    1.46  
    1.47 -lemma differentiable_sum:
    1.48 +lemma differentiable_compose:
    1.49 +  assumes f: "f differentiable (g x)"
    1.50 +  assumes g: "g differentiable x"
    1.51 +  shows "(\<lambda>x. f (g x)) differentiable x"
    1.52 +proof -
    1.53 +  from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" ..
    1.54 +  moreover
    1.55 +  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
    1.56 +  ultimately
    1.57 +  have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2)
    1.58 +  thus ?thesis by (rule differentiableI)
    1.59 +qed
    1.60 +
    1.61 +lemma differentiable_sum [simp]:
    1.62    assumes "f differentiable x"
    1.63    and "g differentiable x"
    1.64    shows "(\<lambda>x. f x + g x) differentiable x"
    1.65  proof -
    1.66 -  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
    1.67 -  then obtain df where "DERIV f x :> df" ..
    1.68 -  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
    1.69 -  then obtain dg where "DERIV g x :> dg" ..
    1.70 -  ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
    1.71 -  hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto
    1.72 -  thus ?thesis by (fold differentiable_def)
    1.73 +  from `f differentiable x` obtain df where "DERIV f x :> df" ..
    1.74 +  moreover
    1.75 +  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
    1.76 +  ultimately
    1.77 +  have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add)
    1.78 +  thus ?thesis by (rule differentiableI)
    1.79 +qed
    1.80 +
    1.81 +lemma differentiable_minus [simp]:
    1.82 +  assumes "f differentiable x"
    1.83 +  shows "(\<lambda>x. - f x) differentiable x"
    1.84 +proof -
    1.85 +  from `f differentiable x` obtain df where "DERIV f x :> df" ..
    1.86 +  hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus)
    1.87 +  thus ?thesis by (rule differentiableI)
    1.88  qed
    1.89  
    1.90 -lemma differentiable_diff:
    1.91 +lemma differentiable_diff [simp]:
    1.92    assumes "f differentiable x"
    1.93 -  and "g differentiable x"
    1.94 +  assumes "g differentiable x"
    1.95    shows "(\<lambda>x. f x - g x) differentiable x"
    1.96 +  unfolding diff_minus using prems by simp
    1.97 +
    1.98 +lemma differentiable_mult [simp]:
    1.99 +  assumes "f differentiable x"
   1.100 +  assumes "g differentiable x"
   1.101 +  shows "(\<lambda>x. f x * g x) differentiable x"
   1.102  proof -
   1.103 -  from prems have "f differentiable x" by simp
   1.104 +  from `f differentiable x` obtain df where "DERIV f x :> df" ..
   1.105    moreover
   1.106 -  from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.107 -  then obtain dg where "DERIV g x :> dg" ..
   1.108 -  then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus)
   1.109 -  hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto
   1.110 -  hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def)
   1.111 -  ultimately 
   1.112 -  show ?thesis
   1.113 -    by (auto simp: diff_def dest: differentiable_sum)
   1.114 +  from `g differentiable x` obtain dg where "DERIV g x :> dg" ..
   1.115 +  ultimately
   1.116 +  have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult)
   1.117 +  thus ?thesis by (rule differentiableI)
   1.118  qed
   1.119  
   1.120 -lemma differentiable_mult:
   1.121 -  assumes "f differentiable x"
   1.122 -  and "g differentiable x"
   1.123 -  shows "(\<lambda>x. f x * g x) differentiable x"
   1.124 +lemma differentiable_inverse [simp]:
   1.125 +  assumes "f differentiable x" and "f x \<noteq> 0"
   1.126 +  shows "(\<lambda>x. inverse (f x)) differentiable x"
   1.127  proof -
   1.128 -  from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def)
   1.129 -  then obtain df where "DERIV f x :> df" ..
   1.130 -  moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def)
   1.131 -  then obtain dg where "DERIV g x :> dg" ..
   1.132 -  ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult)
   1.133 -  hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto
   1.134 -  thus ?thesis by (fold differentiable_def)
   1.135 +  from `f differentiable x` obtain df where "DERIV f x :> df" ..
   1.136 +  hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))"
   1.137 +    using `f x \<noteq> 0` by (rule DERIV_inverse')
   1.138 +  thus ?thesis by (rule differentiableI)
   1.139  qed
   1.140  
   1.141 +lemma differentiable_divide [simp]:
   1.142 +  assumes "f differentiable x"
   1.143 +  assumes "g differentiable x" and "g x \<noteq> 0"
   1.144 +  shows "(\<lambda>x. f x / g x) differentiable x"
   1.145 +  unfolding divide_inverse using prems by simp
   1.146 +
   1.147 +lemma differentiable_power [simp]:
   1.148 +  fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a"
   1.149 +  assumes "f differentiable x"
   1.150 +  shows "(\<lambda>x. f x ^ n) differentiable x"
   1.151 +  by (induct n, simp, simp add: power_Suc prems)
   1.152 +
   1.153  
   1.154  subsection {* Nested Intervals and Bisection *}
   1.155