--- 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"
+ by (simp_all add: abs_less_iff)
thus "(g y - g x) / (y - x) =
inverse ((f (g y) - x) / (g y - g x))"
by (simp add: inj)
@@ -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"
+ by (simp_all add: abs_less_iff)
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)