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.47  lemma LIM_add_zero:
    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.64  lemma LIM_add_minus:
    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: