src/HOL/Lim.thy
 changeset 36661 0a5b7b818d65 parent 32650 34bfa2492298 child 36662 621122eeb138
```     1.1 --- a/src/HOL/Lim.thy	Tue May 04 10:06:05 2010 -0700
1.2 +++ b/src/HOL/Lim.thy	Tue May 04 10:42:47 2010 -0700
1.3 @@ -12,12 +12,10 @@
1.4
1.5  text{*Standard Definitions*}
1.6
1.7 -definition
1.8 +abbreviation
1.9    LIM :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a, 'b] \<Rightarrow> bool"
1.10          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
1.11 -  [code del]: "f -- a --> L =
1.12 -     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
1.13 -        --> dist (f x) L < r)"
1.14 +  "f -- a --> L \<equiv> (f ---> L) (at a)"
1.15
1.16  definition
1.17    isCont :: "['a::metric_space \<Rightarrow> 'b::metric_space, 'a] \<Rightarrow> bool" where
1.18 @@ -29,8 +27,10 @@
1.19
1.20  subsection {* Limits of Functions *}
1.21
1.22 -lemma LIM_conv_tendsto: "(f -- a --> L) \<longleftrightarrow> (f ---> L) (at a)"
1.23 -unfolding LIM_def tendsto_iff eventually_at ..
1.24 +lemma LIM_def: "f -- a --> L =
1.25 +     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
1.26 +        --> dist (f x) L < r)"
1.27 +unfolding tendsto_iff eventually_at ..
1.28
1.29  lemma metric_LIM_I:
1.30    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
1.31 @@ -82,7 +82,7 @@
1.32  by (drule_tac k="- a" in LIM_offset, simp)
1.33
1.34  lemma LIM_const [simp]: "(%x. k) -- x --> k"
1.35 -by (simp add: LIM_def)
1.36 +by (rule tendsto_const)
1.37
1.38  lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
1.39
1.40 @@ -90,22 +90,17 @@
1.41    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.42    assumes f: "f -- a --> L" and g: "g -- a --> M"
1.43    shows "(\<lambda>x. f x + g x) -- a --> (L + M)"
1.44 -using assms unfolding LIM_conv_tendsto by (rule tendsto_add)
1.45 +using assms by (rule tendsto_add)
1.46
1.48    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.49    shows "\<lbrakk>f -- a --> 0; g -- a --> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. f x + g x) -- a --> 0"
1.50  by (drule (1) LIM_add, simp)
1.51
1.52 -lemma minus_diff_minus:
1.53 -  fixes a b :: "'a::ab_group_add"
1.54 -  shows "(- a) - (- b) = - (a - b)"
1.55 -by simp
1.56 -
1.57  lemma LIM_minus:
1.58    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.59    shows "f -- a --> L \<Longrightarrow> (\<lambda>x. - f x) -- a --> - L"
1.60 -unfolding LIM_conv_tendsto by (rule tendsto_minus)
1.61 +by (rule tendsto_minus)
1.62
1.63  (* TODO: delete *)
1.65 @@ -116,7 +111,7 @@
1.66  lemma LIM_diff:
1.67    fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.68    shows "\<lbrakk>f -- x --> l; g -- x --> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --> l - m"
1.69 -unfolding LIM_conv_tendsto by (rule tendsto_diff)
1.70 +by (rule tendsto_diff)
1.71
1.72  lemma LIM_zero:
1.73    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.74 @@ -156,7 +151,7 @@
1.75  lemma LIM_norm:
1.76    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.77    shows "f -- a --> l \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> norm l"
1.78 -unfolding LIM_conv_tendsto by (rule tendsto_norm)
1.79 +by (rule tendsto_norm)
1.80
1.81  lemma LIM_norm_zero:
1.82    fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
1.83 @@ -221,7 +216,7 @@
1.84  done
1.85
1.86  lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
1.87 -by (auto simp add: LIM_def)
1.88 +by (rule tendsto_ident_at)
1.89
1.90  text{*Limits are equal for functions equal except at limit point*}
1.91  lemma LIM_equal:
1.92 @@ -349,7 +344,7 @@
1.93
1.94  lemma (in bounded_linear) LIM:
1.95    "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
1.96 -unfolding LIM_conv_tendsto by (rule tendsto)
1.97 +by (rule tendsto)
1.98
1.99  lemma (in bounded_linear) cont: "f -- a --> f a"
1.100  by (rule LIM [OF LIM_ident])
1.101 @@ -362,7 +357,7 @@
1.102
1.103  lemma (in bounded_bilinear) LIM:
1.104    "\<lbrakk>f -- a --> L; g -- a --> M\<rbrakk> \<Longrightarrow> (\<lambda>x. f x ** g x) -- a --> L ** M"
1.105 -unfolding LIM_conv_tendsto by (rule tendsto)
1.106 +by (rule tendsto)
1.107
1.108  lemma (in bounded_bilinear) LIM_prod_zero:
1.109    fixes a :: "'d::metric_space"
1.110 @@ -402,7 +397,6 @@
1.111  lemma LIM_inverse:
1.112    fixes L :: "'a::real_normed_div_algebra"
1.113    shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
1.114 -unfolding LIM_conv_tendsto
1.115  by (rule tendsto_inverse)
1.116
1.117  lemma LIM_inverse_fun:
```