src/HOL/Lim.thy

 imports SEQ
 begin
 
 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
   "isCont f a = (f -- a --> (f a))"
 

   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 *}
 
-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)
     \<Longrightarrow> f -- a --> L"
 by (simp add: LIM_def)

   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)
+by (rule tendsto_const)
 
 lemma LIM_cong_limit: "\<lbrakk> f -- x --> L ; K = L \<rbrakk> \<Longrightarrow> f -- x --> K" by simp
 
 lemma LIM_add:
   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)
+using assms by (rule tendsto_add)
 
 lemma LIM_add_zero:
   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:
-  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 *)
 lemma LIM_add_minus:
   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:
   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"
   shows "f -- a --> l \<Longrightarrow> (\<lambda>x. f x - l) -- a --> 0"
 by (simp add: LIM_def dist_norm)

 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"
-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"
   shows "f -- a --> 0 \<Longrightarrow> (\<lambda>x. norm (f x)) -- a --> 0"
 by (drule LIM_norm, simp)

 apply (subst dist_commute, rule dist_triangle)
 apply simp
 done
 
 lemma LIM_ident [simp]: "(\<lambda>x. x) -- a --> a"
-by (auto simp add: LIM_def)
+by (rule tendsto_ident_at)
 
 text{*Limits are equal for functions equal except at limit point*}
 lemma LIM_equal:
      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --> l) = (g -- a --> l)"
 by (simp add: LIM_def)

 
 text {* Bounded Linear Operators *}
 
 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])
 
 lemma (in bounded_linear) LIM_zero:

 
 text {* Bounded Bilinear Operators *}
 
 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"
   assumes f: "f -- a --> 0"
   assumes g: "g -- a --> 0"

 subsubsection {* Derived theorems about @{term LIM} *}
 
 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:
   assumes a: "a \<noteq> (0::'a::real_normed_div_algebra)"
   shows "inverse -- a --> inverse a"