src/HOL/Lim.thy
 changeset 36661 0a5b7b818d65 parent 32650 34bfa2492298 child 36662 621122eeb138
```--- a/src/HOL/Lim.thy	Tue May 04 10:06:05 2010 -0700
+++ b/src/HOL/Lim.thy	Tue May 04 10:42:47 2010 -0700
@@ -12,12 +12,10 @@

text{*Standard Definitions*}

-definition
+abbreviation
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 & dist x a < s
-        --> dist (f x) L < r)"
+  "f -- a --> L \<equiv> (f ---> L) (at a)"

definition
isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
@@ -29,8 +27,10 @@

subsection {* Limits of Functions *}

-lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
-unfolding LIM_def tendsto_iff eventually_at ..
+lemma LIM_def: "f -- a --> L =
+     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
+        --> dist (f x) L < r)"
+unfolding tendsto_iff eventually_at ..

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)
@@ -82,7 +82,7 @@
by (drule_tac k="- a" in LIM_offset, simp)

lemma LIM_const [simp]: "(%x. k) -- x --> k"
+by (rule tendsto_const)

lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp

@@ -90,22 +90,17 @@
fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes f: "f -- a --> L" and g: "g -- a --> M"
shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
-using assms unfolding LIM_conv_tendsto by (rule tendsto_add)

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"

-lemma minus_diff_minus:
-  fixes a b :: "'a::ab_group_add"
-  shows "(- a) - (- b) = - (a - b)"
-by simp
-
lemma LIM_minus:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
-unfolding LIM_conv_tendsto by (rule tendsto_minus)
+by (rule tendsto_minus)

(* TODO: delete *)
@@ -116,7 +111,7 @@
lemma LIM_diff:
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"
-unfolding LIM_conv_tendsto by (rule tendsto_diff)
+by (rule tendsto_diff)

lemma LIM_zero:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
@@ -156,7 +151,7 @@
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"
-unfolding LIM_conv_tendsto by (rule tendsto_norm)
+by (rule tendsto_norm)

lemma LIM_norm_zero:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
@@ -221,7 +216,7 @@
done

lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
+by (rule tendsto_ident_at)

text{*Limits are equal for functions equal except at limit point*}
lemma LIM_equal:
@@ -349,7 +344,7 @@

lemma (in bounded_linear) LIM:
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
-unfolding LIM_conv_tendsto by (rule tendsto)
+by (rule tendsto)

lemma (in bounded_linear) cont: "f -- a --> f a"
by (rule LIM [OF LIM_ident])
@@ -362,7 +357,7 @@

lemma (in bounded_bilinear) LIM:
"\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
-unfolding LIM_conv_tendsto by (rule tendsto)
+by (rule tendsto)

lemma (in bounded_bilinear) LIM_prod_zero:
fixes a :: "'d::metric_space"
@@ -402,7 +397,6 @@
lemma LIM_inverse:
fixes L :: "'a::real_normed_div_algebra"
shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
-unfolding LIM_conv_tendsto
by (rule tendsto_inverse)

lemma LIM_inverse_fun:```