--- a/src/HOL/Deriv.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Deriv.thy Fri May 29 09:22:56 2009 -0700
@@ -76,7 +76,7 @@
hence "(\<lambda>h. f(x+h) - f(x)) -- 0 --> 0"
by (simp cong: LIM_cong)
thus "(\<lambda>h. f(x+h)) -- 0 --> f(x)"
- by (simp add: LIM_def)
+ by (simp add: LIM_def dist_norm)
qed
lemma DERIV_mult_lemma:
@@ -125,6 +125,7 @@
text{*Alternative definition for differentiability*}
lemma DERIV_LIM_iff:
+ fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows
"((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
apply (rule iffI)
@@ -614,7 +615,7 @@
apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> ~ (f (u) \<le> y & y \<le> f (v))" in lemma_BOLZANO2)
apply safe
apply simp_all
-apply (simp add: isCont_iff LIM_def)
+apply (simp add: isCont_iff LIM_eq)
apply (rule ccontr)
apply (subgoal_tac "a \<le> x & x \<le> b")
prefer 2
@@ -675,7 +676,7 @@
apply (case_tac "a \<le> x & x \<le> b")
apply (rule_tac [2] x = 1 in exI)
prefer 2 apply force
-apply (simp add: LIM_def isCont_iff)
+apply (simp add: LIM_eq isCont_iff)
apply (drule_tac x = x in spec, auto)
apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
apply (drule_tac x = 1 in spec, auto)
@@ -1486,7 +1487,7 @@
lemma LIM_fun_gt_zero:
"[| f -- c --> (l::real); 0 < l |]
==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> 0 < f x)"
-apply (auto simp add: LIM_def)
+apply (auto simp add: LIM_eq)
apply (drule_tac x = "l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
apply (auto simp only: abs_less_iff)
@@ -1495,7 +1496,7 @@
lemma LIM_fun_less_zero:
"[| f -- c --> (l::real); l < 0 |]
==> \<exists>r. 0 < r & (\<forall>x::real. x \<noteq> c & \<bar>c - x\<bar> < r --> f x < 0)"
-apply (auto simp add: LIM_def)
+apply (auto simp add: LIM_eq)
apply (drule_tac x = "-l/2" in spec, safe, force)
apply (rule_tac x = s in exI)
apply (auto simp only: abs_less_iff)
--- a/src/HOL/Integration.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Integration.thy Fri May 29 09:22:56 2009 -0700
@@ -272,7 +272,7 @@
fix x :: real assume "a \<le> x" and "x \<le> b"
with f' have "DERIV f x :> f'(x)" by simp
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
- by (simp add: DERIV_iff2 LIM_def)
+ by (simp add: DERIV_iff2 LIM_eq)
with `0 < e` obtain s
where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
by (drule_tac x="e/2" in spec, auto)
--- a/src/HOL/Lim.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Lim.thy Fri May 29 09:22:56 2009 -0700
@@ -13,90 +13,110 @@
text{*Standard Definitions*}
definition
- LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
+ LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
[code del]: "f -- a --> L =
- (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
- --> norm (f x - L) < r)"
+ (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
+ --> dist (f x) L < r)"
definition
- isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
+ isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
"isCont f a = (f -- a --> (f a))"
definition
- isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
- [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
+ isUCont :: "['a::metric_space \<Rightarrow> 'b::metric_space] \<Rightarrow> bool" where
+ [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. dist x y < s \<longrightarrow> dist (f x) (f y) < r)"
subsection {* Limits of Functions *}
-subsubsection {* Purely standard proofs *}
+lemma metric_LIM_I:
+ "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
+ \<Longrightarrow> f -- a --> L"
+by (simp add: LIM_def)
+
+lemma metric_LIM_D:
+ "\<lbrakk>f -- a --> L; 0 < r\<rbrakk>
+ \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
+by (simp add: LIM_def)
lemma LIM_eq:
- "f -- a --> L =
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "f -- a --> L =
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
-by (simp add: LIM_def diff_minus)
+by (simp add: LIM_def dist_norm)
lemma LIM_I:
- "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
==> f -- a --> L"
by (simp add: LIM_eq)
lemma LIM_D:
- "[| f -- a --> L; 0<r |]
+ fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
+ shows "[| f -- a --> L; 0<r |]
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
by (simp add: LIM_eq)
-lemma LIM_offset: "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
-apply (rule LIM_I)
-apply (drule_tac r="r" in LIM_D, safe)
+lemma LIM_offset:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+unfolding LIM_def dist_norm
+apply clarify
+apply (drule_tac x="r" in spec, safe)
apply (rule_tac x="s" in exI, safe)
apply (drule_tac x="x + k" in spec)
apply (simp add: algebra_simps)
done
-lemma LIM_offset_zero: "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+lemma LIM_offset_zero:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
by (drule_tac k="a" in LIM_offset, simp add: add_commute)
-lemma LIM_offset_zero_cancel: "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+lemma LIM_offset_zero_cancel:
+ fixes a :: "'a::real_normed_vector" and L :: "'b::metric_space"
+ shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
by (drule_tac k="- a" in LIM_offset, simp)
lemma LIM_const [simp]: "(%x. k) -- x --> k"
by (simp add: LIM_def)
lemma LIM_add:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes f: "f -- a --> L" and g: "g -- a --> M"
- shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (rule LIM_I)
+ shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
+proof (rule metric_LIM_I)
fix r :: real
assume r: "0 < r"
- from LIM_D [OF f half_gt_zero [OF r]]
+ from metric_LIM_D [OF f half_gt_zero [OF r]]
obtain fs
where fs: "0 < fs"
- and fs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < fs --> norm (f x - L) < r/2"
+ and fs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < fs \<longrightarrow> dist (f x) L < r/2"
by blast
- from LIM_D [OF g half_gt_zero [OF r]]
+ from metric_LIM_D [OF g half_gt_zero [OF r]]
obtain gs
where gs: "0 < gs"
- and gs_lt: "\<forall>x. x \<noteq> a & norm (x-a) < gs --> norm (g x - M) < r/2"
+ and gs_lt: "\<forall>x. x \<noteq> a \<and> dist x a < gs \<longrightarrow> dist (g x) M < r/2"
by blast
- show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (x-a) < s \<longrightarrow> norm (f x + g x - (L + M)) < r"
+ show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x + g x) (L + M) < r"
proof (intro exI conjI strip)
show "0 < min fs gs" by (simp add: fs gs)
fix x :: 'a
- assume "x \<noteq> a \<and> norm (x-a) < min fs gs"
- hence "x \<noteq> a \<and> norm (x-a) < fs \<and> norm (x-a) < gs" by simp
+ assume "x \<noteq> a \<and> dist x a < min fs gs"
+ hence "x \<noteq> a \<and> dist x a < fs \<and> dist x a < gs" by simp
with fs_lt gs_lt
- have "norm (f x - L) < r/2" and "norm (g x - M) < r/2" by blast+
- hence "norm (f x - L) + norm (g x - M) < r" by arith
- thus "norm (f x + g x - (L + M)) < r"
+ have "dist (f x) L < r/2" and "dist (g x) M < r/2" by blast+
+ hence "dist (f x) L + dist (g x) M < r" by arith
+ thus "dist (f x + g x) (L + M) < r"
+ unfolding dist_norm
by (blast intro: norm_diff_triangle_ineq order_le_less_trans)
qed
qed
lemma LIM_add_zero:
- "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
by (drule (1) LIM_add, simp)
lemma minus_diff_minus:
@@ -104,46 +124,75 @@
shows "(- a) - (- b) = - (a - b)"
by simp
-lemma LIM_minus: "f -- a --> L ==> (%x. -f(x)) -- a --> -L"
-by (simp only: LIM_eq minus_diff_minus norm_minus_cancel)
+lemma LIM_minus:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
+by (simp only: LIM_def dist_norm minus_diff_minus norm_minus_cancel)
+(* TODO: delete *)
lemma LIM_add_minus:
- "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + -g(x)) -- x --> (l + -m)"
by (intro LIM_add LIM_minus)
lemma LIM_diff:
- "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) - g(x)) -- x --> l-m"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
by (simp only: diff_minus LIM_add LIM_minus)
-lemma LIM_zero: "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
-by (simp add: LIM_def)
+lemma LIM_zero:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
+by (simp add: LIM_def dist_norm)
-lemma LIM_zero_cancel: "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
-by (simp add: LIM_def)
+lemma LIM_zero_cancel:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. f x - l) -- a --> 0 \<Longrightarrow> f -- a --> l"
+by (simp add: LIM_def dist_norm)
-lemma LIM_zero_iff: "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
-by (simp add: LIM_def)
+lemma LIM_zero_iff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. f x - l) -- a --> 0 = f -- a --> l"
+by (simp add: LIM_def dist_norm)
-lemma LIM_imp_LIM:
+lemma metric_LIM_imp_LIM:
assumes f: "f -- a --> l"
- assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
+ assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
shows "g -- a --> m"
-apply (rule LIM_I, drule LIM_D [OF f], safe)
+apply (rule metric_LIM_I, drule metric_LIM_D [OF f], safe)
apply (rule_tac x="s" in exI, safe)
apply (drule_tac x="x" in spec, safe)
apply (erule (1) order_le_less_trans [OF le])
done
-lemma LIM_norm: "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
+lemma LIM_imp_LIM:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes g :: "'a::metric_space \<Rightarrow> 'c::real_normed_vector"
+ assumes f: "f -- a --> l"
+ assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
+ shows "g -- a --> m"
+apply (rule metric_LIM_imp_LIM [OF f])
+apply (simp add: dist_norm le)
+done
+
+lemma LIM_norm:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
by (erule LIM_imp_LIM, simp add: norm_triangle_ineq3)
-lemma LIM_norm_zero: "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
+lemma LIM_norm_zero:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
by (drule LIM_norm, simp)
-lemma LIM_norm_zero_cancel: "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
+lemma LIM_norm_zero_cancel:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. norm (f x)) -- a --> 0 \<Longrightarrow> f -- a --> 0"
by (erule LIM_imp_LIM, simp)
-lemma LIM_norm_zero_iff: "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
+lemma LIM_norm_zero_iff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "(\<lambda>x. norm (f x)) -- a --> 0 = f -- a --> 0"
by (rule iffI [OF LIM_norm_zero_cancel LIM_norm_zero])
lemma LIM_rabs: "f -- a --> (l::real) \<Longrightarrow> (\<lambda>x. \<bar>f x\<bar>) -- a --> \<bar>l\<bar>"
@@ -161,9 +210,9 @@
lemma LIM_const_not_eq:
fixes a :: "'a::real_normed_algebra_1"
shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
-apply (simp add: LIM_eq)
-apply (rule_tac x="norm (k - L)" in exI, simp, safe)
-apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
+apply (simp add: LIM_def)
+apply (rule_tac x="dist k L" in exI, simp add: zero_less_dist_iff, safe)
+apply (rule_tac x="a + of_real (s/2)" in exI, simp add: dist_norm)
done
lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
@@ -176,10 +225,21 @@
done
lemma LIM_unique:
- fixes a :: "'a::real_normed_algebra_1"
+ fixes a :: "'a::real_normed_algebra_1" -- {* TODO: find a more appropriate class *}
shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
-apply (drule (1) LIM_diff)
-apply (auto dest!: LIM_const_eq)
+apply (rule ccontr)
+apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
+apply (drule_tac r="dist L M / 2" in metric_LIM_D, simp add: zero_less_dist_iff)
+apply (clarify, rename_tac r s)
+apply (subgoal_tac "min r s \<noteq> 0")
+apply (subgoal_tac "dist L M < dist L M / 2 + dist L M / 2", simp)
+apply (subgoal_tac "dist L M \<le> dist (f (a + of_real (min r s / 2))) L +
+ dist (f (a + of_real (min r s / 2))) M")
+apply (erule le_less_trans, rule add_strict_mono)
+apply (drule spec, erule mp, simp add: dist_norm)
+apply (drule spec, erule mp, simp add: dist_norm)
+apply (subst dist_commute, rule dist_triangle)
+apply simp
done
lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
@@ -195,9 +255,9 @@
\<Longrightarrow> ((\<lambda>x. f x) -- a --> l) = ((\<lambda>x. g x) -- b --> m)"
by (simp add: LIM_def)
-lemma LIM_equal2:
+lemma metric_LIM_equal2:
assumes 1: "0 < R"
- assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+ assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
shows "g -- a --> l \<Longrightarrow> f -- a --> l"
apply (unfold LIM_def, safe)
apply (drule_tac x="r" in spec, safe)
@@ -206,9 +266,22 @@
apply (simp add: 2)
done
-text{*Two uses in Hyperreal/Transcendental.ML*}
+lemma LIM_equal2:
+ fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ assumes 1: "0 < R"
+ assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
+ shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+apply (unfold LIM_def dist_norm, safe)
+apply (drule_tac x="r" in spec, safe)
+apply (rule_tac x="min s R" in exI, safe)
+apply (simp add: 1)
+apply (simp add: 2)
+done
+
+text{*Two uses in Transcendental.ML*}
lemma LIM_trans:
- "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "[| (%x. f(x) + -g(x)) -- a --> 0; g -- a --> l |] ==> f -- a --> l"
apply (drule LIM_add, assumption)
apply (auto simp add: add_assoc)
done
@@ -217,62 +290,70 @@
assumes g: "g -- l --> g l"
assumes f: "f -- a --> l"
shows "(\<lambda>x. g (f x)) -- a --> g l"
-proof (rule LIM_I)
+proof (rule metric_LIM_I)
fix r::real assume r: "0 < r"
obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> l; norm (y - l) < s\<rbrakk> \<Longrightarrow> norm (g y - g l) < r"
- using LIM_D [OF g r] by fast
+ and less_r: "\<And>y. \<lbrakk>y \<noteq> l; dist y l < s\<rbrakk> \<Longrightarrow> dist (g y) (g l) < r"
+ using metric_LIM_D [OF g r] by fast
obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - l) < s"
- using LIM_D [OF f s] by fast
+ and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) l < s"
+ using metric_LIM_D [OF f s] by fast
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - g l) < r"
+ show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) (g l) < r"
proof (rule exI, safe)
show "0 < t" using t .
next
- fix x assume "x \<noteq> a" and "norm (x - a) < t"
- hence "norm (f x - l) < s" by (rule less_s)
- thus "norm (g (f x) - g l) < r"
+ fix x assume "x \<noteq> a" and "dist x a < t"
+ hence "dist (f x) l < s" by (rule less_s)
+ thus "dist (g (f x)) (g l) < r"
using r less_r by (case_tac "f x = l", simp_all)
qed
qed
+lemma metric_LIM_compose2:
+ assumes f: "f -- a --> b"
+ assumes g: "g -- b --> c"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
+ shows "(\<lambda>x. g (f x)) -- a --> c"
+proof (rule metric_LIM_I)
+ fix r :: real
+ assume r: "0 < r"
+ obtain s where s: "0 < s"
+ and less_r: "\<And>y. \<lbrakk>y \<noteq> b; dist y b < s\<rbrakk> \<Longrightarrow> dist (g y) c < r"
+ using metric_LIM_D [OF g r] by fast
+ obtain t where t: "0 < t"
+ and less_s: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> dist (f x) b < s"
+ using metric_LIM_D [OF f s] by fast
+ obtain d where d: "0 < d"
+ and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
+ using inj by fast
+
+ show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> dist x a < t \<longrightarrow> dist (g (f x)) c < r"
+ proof (safe intro!: exI)
+ show "0 < min d t" using d t by simp
+ next
+ fix x
+ assume "x \<noteq> a" and "dist x a < min d t"
+ hence "f x \<noteq> b" and "dist (f x) b < s"
+ using neq_b less_s by simp_all
+ thus "dist (g (f x)) c < r"
+ by (rule less_r)
+ qed
+qed
+
lemma LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
assumes f: "f -- a --> b"
assumes g: "g -- b --> c"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
shows "(\<lambda>x. g (f x)) -- a --> c"
-proof (rule LIM_I)
- fix r :: real
- assume r: "0 < r"
- obtain s where s: "0 < s"
- and less_r: "\<And>y. \<lbrakk>y \<noteq> b; norm (y - b) < s\<rbrakk> \<Longrightarrow> norm (g y - c) < r"
- using LIM_D [OF g r] by fast
- obtain t where t: "0 < t"
- and less_s: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (f x - b) < s"
- using LIM_D [OF f s] by fast
- obtain d where d: "0 < d"
- and neq_b: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < d\<rbrakk> \<Longrightarrow> f x \<noteq> b"
- using inj by fast
-
- show "\<exists>t>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < t \<longrightarrow> norm (g (f x) - c) < r"
- proof (safe intro!: exI)
- show "0 < min d t" using d t by simp
- next
- fix x
- assume "x \<noteq> a" and "norm (x - a) < min d t"
- hence "f x \<noteq> b" and "norm (f x - b) < s"
- using neq_b less_s by simp_all
- thus "norm (g (f x) - c) < r"
- by (rule less_r)
- qed
-qed
+by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
unfolding o_def by (rule LIM_compose)
lemma real_LIM_sandwich_zero:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> real"
+ fixes f g :: "'a::metric_space \<Rightarrow> real"
assumes f: "f -- a --> 0"
assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
@@ -316,10 +397,11 @@
text {* Bounded Bilinear Operators *}
lemma (in bounded_bilinear) LIM_prod_zero:
+ fixes a :: "'d::metric_space"
assumes f: "f -- a --> 0"
assumes g: "g -- a --> 0"
shows "(\<lambda>x. f x ** g x) -- a --> 0"
-proof (rule LIM_I)
+proof (rule metric_LIM_I, unfold dist_norm)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K"
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
@@ -327,18 +409,18 @@
from K have K': "0 < inverse K"
by (rule positive_imp_inverse_positive)
obtain s where s: "0 < s"
- and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
- using LIM_D [OF f r] by auto
+ and norm_f: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> norm (f x) < r"
+ using metric_LIM_D [OF f r, unfolded dist_norm] by auto
obtain t where t: "0 < t"
- and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
- using LIM_D [OF g K'] by auto
- show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x ** g x - 0) < r"
+ and norm_g: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < t\<rbrakk> \<Longrightarrow> norm (g x) < inverse K"
+ using metric_LIM_D [OF g K', unfolded dist_norm] by auto
+ show "\<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> norm (f x ** g x - 0) < r"
proof (rule exI, safe)
from s t show "0 < min s t" by simp
next
fix x assume x: "x \<noteq> a"
- assume "norm (x - a) < min s t"
- hence xs: "norm (x - a) < s" and xt: "norm (x - a) < t" by simp_all
+ assume "dist x a < min s t"
+ hence xs: "dist x a < s" and xt: "dist x a < t" by simp_all
from x xs have 1: "norm (f x) < r" by (rule norm_f)
from x xt have 2: "norm (g x) < inverse K" by (rule norm_g)
have "norm (f x ** g x) \<le> norm (f x) * norm (g x) * K" by (rule norm_le)
@@ -383,7 +465,7 @@
lemmas LIM_of_real = of_real.LIM
lemma LIM_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
assumes f: "f -- a --> l"
shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
by (induct n, simp, simp add: LIM_mult f)
@@ -453,19 +535,22 @@
by (rule LIM_inverse_fun [THEN LIM_compose])
lemma LIM_sgn:
- "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>f -- a --> l; l \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. sgn (f x)) -- a --> sgn l"
unfolding sgn_div_norm
by (simp add: LIM_scaleR LIM_inverse LIM_norm)
subsection {* Continuity *}
-subsubsection {* Purely standard proofs *}
-
-lemma LIM_isCont_iff: "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
+lemma LIM_isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
-lemma isCont_iff: "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+lemma isCont_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::metric_space"
+ shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
by (simp add: isCont_def LIM_isCont_iff)
lemma isCont_ident [simp]: "isCont (\<lambda>x. x) a"
@@ -474,28 +559,36 @@
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
unfolding isCont_def by (rule LIM_const)
-lemma isCont_norm: "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+lemma isCont_norm:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
unfolding isCont_def by (rule LIM_norm)
lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
unfolding isCont_def by (rule LIM_rabs)
-lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
+lemma isCont_add:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
unfolding isCont_def by (rule LIM_add)
-lemma isCont_minus: "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
+lemma isCont_minus:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
unfolding isCont_def by (rule LIM_minus)
-lemma isCont_diff: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
+lemma isCont_diff:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
unfolding isCont_def by (rule LIM_diff)
lemma isCont_mult:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_algebra"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)
lemma isCont_inverse:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_div_algebra"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)
@@ -503,7 +596,15 @@
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
unfolding isCont_def by (rule LIM_compose)
+lemma metric_isCont_LIM_compose2:
+ assumes f [unfolded isCont_def]: "isCont f a"
+ assumes g: "g -- f a --> l"
+ assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
+ shows "(\<lambda>x. g (f x)) -- a --> l"
+by (rule metric_LIM_compose2 [OF f g inj])
+
lemma isCont_LIM_compose2:
+ fixes a :: "'a::real_normed_vector"
assumes f [unfolded isCont_def]: "isCont f a"
assumes g: "g -- f a --> l"
assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
@@ -526,22 +627,25 @@
lemmas isCont_scaleR = scaleR.isCont
lemma isCont_of_real:
- "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)) a"
+ "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
unfolding isCont_def by (rule LIM_of_real)
lemma isCont_power:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
lemma isCont_sgn:
- "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
unfolding isCont_def by (rule LIM_sgn)
lemma isCont_abs [simp]: "isCont abs (a::real)"
by (rule isCont_rabs [OF isCont_ident])
-lemma isCont_setsum: fixes A :: "nat set" assumes "finite A"
+lemma isCont_setsum:
+ fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+ fixes A :: "'a set" assumes "finite A"
shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
using `finite A`
proof induct
@@ -578,7 +682,7 @@
hence "f ?x < 0" using `f x < 0` by auto
thus False using `0 \<le> f ?x` by auto
qed
-
+
subsection {* Uniform Continuity *}
@@ -588,14 +692,14 @@
lemma isUCont_Cauchy:
"\<lbrakk>isUCont f; Cauchy X\<rbrakk> \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
unfolding isUCont_def
-apply (rule CauchyI)
+apply (rule metric_CauchyI)
apply (drule_tac x=e in spec, safe)
-apply (drule_tac e=s in CauchyD, safe)
+apply (drule_tac e=s in metric_CauchyD, safe)
apply (rule_tac x=M in exI, simp)
done
lemma (in bounded_linear) isUCont: "isUCont f"
-unfolding isUCont_def
+unfolding isUCont_def dist_norm
proof (intro allI impI)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
@@ -620,44 +724,46 @@
subsection {* Relation of LIM and LIMSEQ *}
lemma LIMSEQ_SEQ_conv1:
- fixes a :: "'a::real_normed_vector"
+ fixes a :: "'a::metric_space"
assumes X: "X -- a --> L"
shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
-proof (safe intro!: LIMSEQ_I)
+proof (safe intro!: metric_LIMSEQ_I)
fix S :: "nat \<Rightarrow> 'a"
fix r :: real
assume rgz: "0 < r"
assume as: "\<forall>n. S n \<noteq> a"
assume S: "S ----> a"
- from LIM_D [OF X rgz] obtain s
+ from metric_LIM_D [OF X rgz] obtain s
where sgz: "0 < s"
- and aux: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (X x - L) < r"
+ and aux: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < s\<rbrakk> \<Longrightarrow> dist (X x) L < r"
by fast
- from LIMSEQ_D [OF S sgz]
- obtain no where "\<forall>n\<ge>no. norm (S n - a) < s" by blast
- hence "\<forall>n\<ge>no. norm (X (S n) - L) < r" by (simp add: aux as)
- thus "\<exists>no. \<forall>n\<ge>no. norm (X (S n) - L) < r" ..
+ from metric_LIMSEQ_D [OF S sgz]
+ obtain no where "\<forall>n\<ge>no. dist (S n) a < s" by blast
+ hence "\<forall>n\<ge>no. dist (X (S n)) L < r" by (simp add: aux as)
+ thus "\<exists>no. \<forall>n\<ge>no. dist (X (S n)) L < r" ..
qed
+
lemma LIMSEQ_SEQ_conv2:
fixes a :: real
assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "X -- a --> L"
proof (rule ccontr)
assume "\<not> (X -- a --> L)"
- hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> norm (X x - L) < r)" by (unfold LIM_def)
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> norm (X x - L) < r)" by simp
- hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r)" by (simp add: linorder_not_less)
- then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> norm (X x - L) \<ge> r))" by auto
+ hence "\<not> (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s --> dist (X x) L < r)"
+ unfolding LIM_def dist_norm .
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. \<not>(x \<noteq> a \<and> \<bar>x - a\<bar> < s --> dist (X x) L < r)" by simp
+ hence "\<exists>r > 0. \<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r)" by (simp add: not_less)
+ then obtain r where rdef: "r > 0 \<and> (\<forall>s > 0. \<exists>x. (x \<noteq> a \<and> \<bar>x - a\<bar> < s \<and> dist (X x) L \<ge> r))" by auto
- let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
- have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> norm (X x - L) \<ge> r"
+ let ?F = "\<lambda>n::nat. SOME x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
+ have "\<And>n. \<exists>x. x\<noteq>a \<and> \<bar>x - a\<bar> < inverse (real (Suc n)) \<and> dist (X x) L \<ge> r"
using rdef by simp
- hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> norm (X (?F n) - L) \<ge> r"
+ hence F: "\<And>n. ?F n \<noteq> a \<and> \<bar>?F n - a\<bar> < inverse (real (Suc n)) \<and> dist (X (?F n)) L \<ge> r"
by (rule someI_ex)
hence F1: "\<And>n. ?F n \<noteq> a"
and F2: "\<And>n. \<bar>?F n - a\<bar> < inverse (real (Suc n))"
- and F3: "\<And>n. norm (X (?F n) - L) \<ge> r"
+ and F3: "\<And>n. dist (X (?F n)) L \<ge> r"
by fast+
have "?F ----> a"
@@ -694,13 +800,13 @@
obtain n where "n = no + 1" by simp
then have nolen: "no \<le> n" by simp
(* We prove this by showing that for any m there is an n\<ge>m such that |X (?F n) - L| \<ge> r *)
- have "norm (X (?F n) - L) \<ge> r"
+ have "dist (X (?F n)) L \<ge> r"
by (rule F3)
- with nolen have "\<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r" by fast
+ with nolen have "\<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r" by fast
}
- then have "(\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> r)" by simp
- with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> norm (X (?F n) - L) \<ge> e)" by auto
- thus ?thesis by (unfold LIMSEQ_iff, auto simp add: linorder_not_less)
+ then have "(\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> r)" by simp
+ with rdef have "\<exists>e>0. (\<forall>no. \<exists>n. no \<le> n \<and> dist (X (?F n)) L \<ge> e)" by auto
+ thus ?thesis by (unfold LIMSEQ_def, auto simp add: not_less)
qed
ultimately show False by simp
qed
--- a/src/HOL/Ln.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Ln.thy Fri May 29 09:22:56 2009 -0700
@@ -343,7 +343,7 @@
done
lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
- apply (unfold deriv_def, unfold LIM_def, clarsimp)
+ apply (unfold deriv_def, unfold LIM_eq, clarsimp)
apply (rule exI)
apply (rule conjI)
prefer 2
--- a/src/HOL/NSA/CLim.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/NSA/CLim.thy Fri May 29 09:22:56 2009 -0700
@@ -45,17 +45,25 @@
hIm_hcomplex_of_complex)
(** get this result easily now **)
-lemma LIM_Re: "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
+lemma LIM_Re:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Re)
-lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
+lemma LIM_Im:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
by (simp add: LIM_NSLIM_iff NSLIM_Im)
-lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
-by (simp add: LIM_def complex_cnj_diff [symmetric])
+lemma LIM_cnj:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
+by (simp add: LIM_eq complex_cnj_diff [symmetric])
-lemma LIM_cnj_iff: "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
-by (simp add: LIM_def complex_cnj_diff [symmetric])
+lemma LIM_cnj_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
+by (simp add: LIM_eq complex_cnj_diff [symmetric])
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
by transfer (rule refl)
@@ -74,8 +82,10 @@
approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
(** much, much easier standard proof **)
-lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
-by (simp add: LIM_def)
+lemma CLIM_CRLIM_iff:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
+by (simp add: LIM_eq)
(* so this is nicer nonstandard proof *)
lemma NSCLIM_NSCRLIM_iff2:
@@ -92,7 +102,8 @@
done
lemma LIM_CRLIM_Re_Im_iff:
- "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
(%x. Im(f x)) -- a --> Im(L))"
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
@@ -113,10 +124,14 @@
lemma isContCR_cmod [simp]: "isCont cmod (a)"
by (simp add: isNSCont_isCont_iff [symmetric])
-lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a"
+lemma isCont_Re:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "isCont f a ==> isCont (%x. Re (f x)) a"
by (simp add: isCont_def LIM_Re)
-lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a"
+lemma isCont_Im:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
+ shows "isCont f a ==> isCont (%x. Im (f x)) a"
by (simp add: isCont_def LIM_Im)
subsection{* Differentiation of Natural Number Powers*}
--- a/src/HOL/NSA/HLim.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/NSA/HLim.thy Fri May 29 09:22:56 2009 -0700
@@ -287,7 +287,7 @@
fix r::real assume r: "0 < r"
with f obtain s where s: "0 < s" and
less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
- by (auto simp add: isUCont_def)
+ by (auto simp add: isUCont_def dist_norm)
from less_r have less_r':
"\<And>x y. hnorm (x - y) < star_of s
\<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
@@ -306,7 +306,7 @@
lemma isNSUCont_isUCont:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes f: "isNSUCont f" shows "isUCont f"
-proof (unfold isUCont_def, safe)
+proof (unfold isUCont_def dist_norm, safe)
fix r::real assume r: "0 < r"
have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
\<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
--- a/src/HOL/Transcendental.thy Thu May 28 23:03:12 2009 -0700
+++ b/src/HOL/Transcendental.thy Fri May 29 09:22:56 2009 -0700
@@ -438,7 +438,7 @@
assumes k: "0 < (k::real)"
assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
shows "f -- 0 --> 0"
-unfolding LIM_def diff_0_right
+unfolding LIM_eq diff_0_right
proof (safe)
let ?h = "of_real (k / 2)::'a"
have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
@@ -2145,7 +2145,7 @@
lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
apply (cut_tac LIM_cos_div_sin)
-apply (simp only: LIM_def)
+apply (simp only: LIM_eq)
apply (drule_tac x = "inverse y" in spec, safe, force)
apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero], safe)
apply (rule_tac x = "(pi/2) - e" in exI)