# HG changeset patch
# User huffman
# Date 1230146257 28800
# Node ID 6a5f1d8d7344f3cf2ccaeb9617d7996f00f016f8
# Parent  ff13de554ed0337f5c45e2f3648e8e4a67c26334
more proofs about differentiable

diff -r ff13de554ed0 -r 6a5f1d8d7344 src/HOL/Deriv.thy
--- 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 *}