summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Deriv.thy

changeset 29169 | 6a5f1d8d7344 |

parent 29166 | c23b2d108612 |

child 29470 | 1851088a1f87 |

--- a/src/HOL/Deriv.thy Wed Dec 24 09:26:18 2008 -0800 +++ b/src/HOL/Deriv.thy Wed Dec 24 11:17:37 2008 -0800 @@ -20,12 +20,6 @@ ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" -definition - differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" - (infixl "differentiable" 60) where - "f differentiable x = (\<exists>D. DERIV f x :> D)" - - consts Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" primrec @@ -316,63 +310,104 @@ subsection {* Differentiability predicate *} +definition + differentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool" + (infixl "differentiable" 60) where + "f differentiable x = (\<exists>D. DERIV f x :> D)" + +lemma differentiableE [elim?]: + assumes "f differentiable x" + obtains df where "DERIV f x :> df" + using prems unfolding differentiable_def .. + lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D" by (simp add: differentiable_def) lemma differentiableI: "DERIV f x :> D ==> f differentiable x" by (force simp add: differentiable_def) -lemma differentiable_const: "(\<lambda>z. a) differentiable x" - apply (unfold differentiable_def) - apply (rule_tac x=0 in exI) - apply simp - done +lemma differentiable_ident [simp]: "(\<lambda>x. x) differentiable x" + by (rule DERIV_ident [THEN differentiableI]) + +lemma differentiable_const [simp]: "(\<lambda>z. a) differentiable x" + by (rule DERIV_const [THEN differentiableI]) -lemma differentiable_sum: +lemma differentiable_compose: + assumes f: "f differentiable (g x)" + assumes g: "g differentiable x" + shows "(\<lambda>x. f (g x)) differentiable x" +proof - + from `f differentiable (g x)` obtain df where "DERIV f (g x) :> df" .. + moreover + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. + ultimately + have "DERIV (\<lambda>x. f (g x)) x :> df * dg" by (rule DERIV_chain2) + thus ?thesis by (rule differentiableI) +qed + +lemma differentiable_sum [simp]: assumes "f differentiable x" and "g differentiable x" shows "(\<lambda>x. f x + g x) differentiable x" proof - - from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) - then obtain df where "DERIV f x :> df" .. - moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - ultimately have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add) - hence "\<exists>D. DERIV (\<lambda>x. f x + g x) x :> D" by auto - thus ?thesis by (fold differentiable_def) + from `f differentiable x` obtain df where "DERIV f x :> df" .. + moreover + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. + ultimately + have "DERIV (\<lambda>x. f x + g x) x :> df + dg" by (rule DERIV_add) + thus ?thesis by (rule differentiableI) +qed + +lemma differentiable_minus [simp]: + assumes "f differentiable x" + shows "(\<lambda>x. - f x) differentiable x" +proof - + from `f differentiable x` obtain df where "DERIV f x :> df" .. + hence "DERIV (\<lambda>x. - f x) x :> - df" by (rule DERIV_minus) + thus ?thesis by (rule differentiableI) qed -lemma differentiable_diff: +lemma differentiable_diff [simp]: assumes "f differentiable x" - and "g differentiable x" + assumes "g differentiable x" shows "(\<lambda>x. f x - g x) differentiable x" + unfolding diff_minus using prems by simp + +lemma differentiable_mult [simp]: + assumes "f differentiable x" + assumes "g differentiable x" + shows "(\<lambda>x. f x * g x) differentiable x" proof - - from prems have "f differentiable x" by simp + from `f differentiable x` obtain df where "DERIV f x :> df" .. moreover - from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - then have "DERIV (\<lambda>x. - g x) x :> -dg" by (rule DERIV_minus) - hence "\<exists>D. DERIV (\<lambda>x. - g x) x :> D" by auto - hence "(\<lambda>x. - g x) differentiable x" by (fold differentiable_def) - ultimately - show ?thesis - by (auto simp: diff_def dest: differentiable_sum) + from `g differentiable x` obtain dg where "DERIV g x :> dg" .. + ultimately + have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (rule DERIV_mult) + thus ?thesis by (rule differentiableI) qed -lemma differentiable_mult: - assumes "f differentiable x" - and "g differentiable x" - shows "(\<lambda>x. f x * g x) differentiable x" +lemma differentiable_inverse [simp]: + assumes "f differentiable x" and "f x \<noteq> 0" + shows "(\<lambda>x. inverse (f x)) differentiable x" proof - - from prems have "\<exists>D. DERIV f x :> D" by (unfold differentiable_def) - then obtain df where "DERIV f x :> df" .. - moreover from prems have "\<exists>D. DERIV g x :> D" by (unfold differentiable_def) - then obtain dg where "DERIV g x :> dg" .. - ultimately have "DERIV (\<lambda>x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult) - hence "\<exists>D. DERIV (\<lambda>x. f x * g x) x :> D" by auto - thus ?thesis by (fold differentiable_def) + from `f differentiable x` obtain df where "DERIV f x :> df" .. + hence "DERIV (\<lambda>x. inverse (f x)) x :> - (inverse (f x) * df * inverse (f x))" + using `f x \<noteq> 0` by (rule DERIV_inverse') + thus ?thesis by (rule differentiableI) qed +lemma differentiable_divide [simp]: + assumes "f differentiable x" + assumes "g differentiable x" and "g x \<noteq> 0" + shows "(\<lambda>x. f x / g x) differentiable x" + unfolding divide_inverse using prems by simp + +lemma differentiable_power [simp]: + fixes f :: "'a::{recpower,real_normed_field} \<Rightarrow> 'a" + assumes "f differentiable x" + shows "(\<lambda>x. f x ^ n) differentiable x" + by (induct n, simp, simp add: power_Suc prems) + subsection {* Nested Intervals and Bisection *}