author huffman Sun, 20 May 2007 08:00:48 +0200 changeset 23044 2ad82c359175 parent 23043 5dbfd67516a4 child 23045 95e04f335940
change premises of DERIV_inverse_function lemma
 src/HOL/Hyperreal/Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Hyperreal/NthRoot.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/Deriv.thy	Sun May 20 05:27:45 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Sun May 20 08:00:48 2007 +0200
@@ -1255,14 +1255,19 @@
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 a: "a < x" and b: "x < b"
+  assumes inj: "\<forall>y. a < y \<and> y < b \<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])
+proof (rule LIM_equal2)
+  show "0 < min (x - a) (b - x)"
+    using a b by simp
+next
fix y
-  assume "y \<noteq> x" and "norm (y - x) < e"
+  assume "norm (y - x) < min (x - a) (b - x)"
+  hence "a < y" and "y < b"
thus "(g y - g x) / (y - x) =
inverse ((f (g y) - x) / (g y - g x))"
@@ -1270,16 +1275,19 @@
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
+    using inj a b 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 .
+    show "0 < min (x - a) (b - x)"
+      using a b by simp
next
fix y
-    assume y: "norm (y - x) < e"
+    assume "norm (y - x) < min (x - a) (b - x)"
+    hence y: "a < y" "y < b"
assume "g y = g x"
hence "f (g y) = f (g x)" by simp
-    hence "y = x" using inj y by simp
+    hence "y = x" using inj y a b by simp
also assume "y \<noteq> x"
finally show False by simp
qed```
```--- a/src/HOL/Hyperreal/NthRoot.thy	Sun May 20 05:27:45 2007 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Sun May 20 08:00:48 2007 +0200
@@ -259,9 +259,9 @@
assumes x: "0 < x"
shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))"
proof (rule DERIV_inverse_function)
-  show "0 < x"
-    using x .
-  show "\<forall>y. \<bar>y - x\<bar> \<le> x \<longrightarrow> root n y ^ n = y"
+  show "0 < x" using x .
+  show "x < x + 1" by simp
+  show "\<forall>y. 0 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
using n by simp
show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
by (rule DERIV_pow)```