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"

lemma differentiableI: "DERIV f x :> D ==> f differentiable x"

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