# HG changeset patch
# User huffman
# Date 1179623954 -7200
# Node ID a0f26d47369b91fe360d65d82f475807cd643649
# Parent  d329182b59660db453f0f779e12b4e3b7a1f9fef
add lemma DERIV_inverse_function

diff -r d329182b5966 -r a0f26d47369b src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Sun May 20 03:18:50 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Sun May 20 03:19:14 2007 +0200
@@ -1249,6 +1249,47 @@
   qed
 qed
 
+text {* Derivative of inverse function *}
+
+lemma DERIV_inverse_function:
+  fixes f g :: "real \<Rightarrow> real"
+  assumes der: "DERIV f (g x) :> D"
+  assumes neq: "D \<noteq> 0"
+  assumes e: "0 < e"
+  assumes inj: "\<forall>y. \<bar>y - x\<bar> \<le> e \<longrightarrow> f (g y) = y"
+  assumes cont: "isCont g x"
+  shows "DERIV g x :> inverse D"
+unfolding DERIV_iff2
+proof (rule LIM_equal2 [OF e])
+  fix y
+  assume "y \<noteq> x" and "norm (y - x) < e"
+  thus "(g y - g x) / (y - x) =
+        inverse ((f (g y) - x) / (g y - g x))"
+    by (simp add: inj)
+next
+  have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D"
+    by (rule der [unfolded DERIV_iff2])
+  hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D"
+    using inj e by simp
+  have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
+  proof (safe intro!: exI)
+    show "0 < e" using e .
+  next
+    fix y
+    assume y: "norm (y - x) < e"
+    assume "g y = g x"
+    hence "f (g y) = f (g x)" by simp
+    hence "y = x" using inj y by simp
+    also assume "y \<noteq> x"
+    finally show False by simp
+  qed
+  have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D"
+    using cont 1 2 by (rule isCont_LIM_compose2)
+  thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
+        -- x --> inverse D"
+    using neq by (rule LIM_inverse)
+qed
+
 theorem GMVT:
   fixes a b :: real
   assumes alb: "a < b"