diff -r d3d170a2887f -r 155263089e7b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Mar 26 12:20:58 2013 +0100
+++ b/src/HOL/Limits.thy	Tue Mar 26 12:20:58 2013 +0100
@@ -1,13 +1,23 @@
-(*  Title       : Limits.thy
-    Author      : Brian Huffman
+(*  Title:      Limits.thy
+    Author:     Brian Huffman
+    Author:     Jacques D. Fleuriot, University of Cambridge
+    Author:     Lawrence C Paulson
+    Author:     Jeremy Avigad
+
 *)
 
-header {* Filters and Limits *}
+header {* Limits on Real Vector Spaces *}
 
 theory Limits
 imports Real_Vector_Spaces
 begin
 
+(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
+   Hence it was references as Limits.eventually_within, but now it is Basic_Topology.eventually_within *)
+lemmas eventually_within = eventually_within
+
+subsection {* Filter going to infinity norm *}
+
 definition at_infinity :: "'a::real_normed_vector filter" where
   "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
 
@@ -1027,9 +1037,616 @@
 qed simp
 
 
-(* Unfortunately eventually_within was overwritten by Multivariate_Analysis.
-   Hence it was references as Limits.within, but now it is Basic_Topology.eventually_within *)
-lemmas eventually_within = eventually_within
+subsection {* Limits of Sequences *}
+
+lemma [trans]: "X=Y ==> Y ----> z ==> X ----> z"
+  by simp
+
+lemma LIMSEQ_iff:
+  fixes L :: "'a::real_normed_vector"
+  shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
+unfolding LIMSEQ_def dist_norm ..
+
+lemma LIMSEQ_I:
+  fixes L :: "'a::real_normed_vector"
+  shows "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r) \<Longrightarrow> X ----> L"
+by (simp add: LIMSEQ_iff)
+
+lemma LIMSEQ_D:
+  fixes L :: "'a::real_normed_vector"
+  shows "\<lbrakk>X ----> L; 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (X n - L) < r"
+by (simp add: LIMSEQ_iff)
+
+lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
+  unfolding tendsto_def eventually_sequentially
+  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
+
+lemma Bseq_inverse_lemma:
+  fixes x :: "'a::real_normed_div_algebra"
+  shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
+apply (subst nonzero_norm_inverse, clarsimp)
+apply (erule (1) le_imp_inverse_le)
+done
+
+lemma Bseq_inverse:
+  fixes a :: "'a::real_normed_div_algebra"
+  shows "\<lbrakk>X ----> a; a \<noteq> 0\<rbrakk> \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
+  by (rule Bfun_inverse)
+
+lemma LIMSEQ_diff_approach_zero:
+  fixes L :: "'a::real_normed_vector"
+  shows "g ----> L ==> (%x. f x - g x) ----> 0 ==> f ----> L"
+  by (drule (1) tendsto_add, simp)
+
+lemma LIMSEQ_diff_approach_zero2:
+  fixes L :: "'a::real_normed_vector"
+  shows "f ----> L ==> (%x. f x - g x) ----> 0 ==> g ----> L"
+  by (drule (1) tendsto_diff, simp)
+
+text{*An unbounded sequence's inverse tends to 0*}
+
+lemma LIMSEQ_inverse_zero:
+  "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
+  apply (rule filterlim_compose[OF tendsto_inverse_0])
+  apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
+  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
+  done
+
+text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
+
+lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
+  by (metis filterlim_compose tendsto_inverse_0 filterlim_mono order_refl filterlim_Suc
+            filterlim_compose[OF filterlim_real_sequentially] at_top_le_at_infinity)
+
+text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to
+infinity is now easily proved*}
+
+lemma LIMSEQ_inverse_real_of_nat_add:
+     "(%n. r + inverse(real(Suc n))) ----> r"
+  using tendsto_add [OF tendsto_const LIMSEQ_inverse_real_of_nat] by auto
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus:
+     "(%n. r + -inverse(real(Suc n))) ----> r"
+  using tendsto_add [OF tendsto_const tendsto_minus [OF LIMSEQ_inverse_real_of_nat]]
+  by auto
+
+lemma LIMSEQ_inverse_real_of_nat_add_minus_mult:
+     "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r"
+  using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
+  by auto
+
+subsection {* Convergence on sequences *}
+
+lemma convergent_add:
+  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes "convergent (\<lambda>n. X n)"
+  assumes "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n + Y n)"
+  using assms unfolding convergent_def by (fast intro: tendsto_add)
+
+lemma convergent_setsum:
+  fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> convergent (\<lambda>n. X i n)"
+  shows "convergent (\<lambda>n. \<Sum>i\<in>A. X i n)"
+proof (cases "finite A")
+  case True from this and assms show ?thesis
+    by (induct A set: finite) (simp_all add: convergent_const convergent_add)
+qed (simp add: convergent_const)
+
+lemma (in bounded_linear) convergent:
+  assumes "convergent (\<lambda>n. X n)"
+  shows "convergent (\<lambda>n. f (X n))"
+  using assms unfolding convergent_def by (fast intro: tendsto)
+
+lemma (in bounded_bilinear) convergent:
+  assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n ** Y n)"
+  using assms unfolding convergent_def by (fast intro: tendsto)
+
+lemma convergent_minus_iff:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
+apply (simp add: convergent_def)
+apply (auto dest: tendsto_minus)
+apply (drule tendsto_minus, auto)
+done
+
+subsection {* Bounded Monotonic Sequences *}
+
+subsubsection {* Bounded Sequences *}
+
+lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
+  by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
+  by (intro BfunI) (auto simp: eventually_sequentially)
+
+lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
+  unfolding Bfun_def eventually_sequentially
+proof safe
+  fix N K assume "0 < K" "\<forall>n\<ge>N. norm (X n) \<le> K"
+  then show "\<exists>K>0. \<forall>n. norm (X n) \<le> K"
+    by (intro exI[of _ "max (Max (norm ` X ` {..N})) K"] min_max.less_supI2)
+       (auto intro!: imageI not_less[where 'a=nat, THEN iffD1] Max_ge simp: le_max_iff_disj)
+qed auto
+
+lemma BseqE: "\<lbrakk>Bseq X; \<And>K. \<lbrakk>0 < K; \<forall>n. norm (X n) \<le> K\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+unfolding Bseq_def by auto
+
+lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"
+by (simp add: Bseq_def)
+
+lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
+by (auto simp add: Bseq_def)
+
+lemma lemma_NBseq_def:
+  "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
+proof safe
+  fix K :: real
+  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+  then have "K \<le> real (Suc n)" by auto
+  moreover assume "\<forall>m. norm (X m) \<le> K"
+  ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
+    by (blast intro: order_trans)
+  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+qed (force simp add: real_of_nat_Suc)
+
+text{* alternative definition for Bseq *}
+lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
+apply (simp add: Bseq_def)
+apply (simp (no_asm) add: lemma_NBseq_def)
+done
+
+lemma lemma_NBseq_def2:
+     "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
+apply (subst lemma_NBseq_def, auto)
+apply (rule_tac x = "Suc N" in exI)
+apply (rule_tac [2] x = N in exI)
+apply (auto simp add: real_of_nat_Suc)
+ prefer 2 apply (blast intro: order_less_imp_le)
+apply (drule_tac x = n in spec, simp)
+done
+
+(* yet another definition for Bseq *)
+lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. norm (X n) < real(Suc N))"
+by (simp add: Bseq_def lemma_NBseq_def2)
+
+subsubsection{*A Few More Equivalence Theorems for Boundedness*}
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff2: "Bseq X = (\<exists>k > 0. \<exists>x. \<forall>n. norm (X(n) + -x) \<le> k)"
+apply (unfold Bseq_def, safe)
+apply (rule_tac [2] x = "k + norm x" in exI)
+apply (rule_tac x = K in exI, simp)
+apply (rule exI [where x = 0], auto)
+apply (erule order_less_le_trans, simp)
+apply (drule_tac x=n in spec, fold diff_minus)
+apply (drule order_trans [OF norm_triangle_ineq2])
+apply simp
+done
+
+text{*alternative formulation for boundedness*}
+lemma Bseq_iff3: "Bseq X = (\<exists>k > 0. \<exists>N. \<forall>n. norm(X(n) + -X(N)) \<le> k)"
+apply safe
+apply (simp add: Bseq_def, safe)
+apply (rule_tac x = "K + norm (X N)" in exI)
+apply auto
+apply (erule order_less_le_trans, simp)
+apply (rule_tac x = N in exI, safe)
+apply (drule_tac x = n in spec)
+apply (rule order_trans [OF norm_triangle_ineq], simp)
+apply (auto simp add: Bseq_iff2)
+done
+
+lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> (K::real)) ==> Bseq f"
+apply (simp add: Bseq_def)
+apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
+apply (drule_tac x = n in spec, arith)
+done
+
+subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
+
+lemma Bseq_isUb:
+  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
+
+text{* Use completeness of reals (supremum property)
+   to show that any bounded sequence has a least upper bound*}
+
+lemma Bseq_isLub:
+  "!!(X::nat=>real). Bseq X ==>
+   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
+by (blast intro: reals_complete Bseq_isUb)
+
+subsubsection{*A Bounded and Monotonic Sequence Converges*}
+
+(* TODO: delete *)
+(* FIXME: one use in NSA/HSEQ.thy *)
+lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n --> X n = X m ==> \<exists>L. (X ----> L)"
+  apply (rule_tac x="X m" in exI)
+  apply (rule filterlim_cong[THEN iffD2, OF refl refl _ tendsto_const])
+  unfolding eventually_sequentially
+  apply blast
+  done
+
+text {* A monotone sequence converges to its least upper bound. *}
+
+lemma isLub_mono_imp_LIMSEQ:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+  shows "X ----> u"
+proof (rule LIMSEQ_I)
+  have 1: "\<forall>n. X n \<le> u"
+    using isLubD2 [OF u] by auto
+  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
+    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
+  hence 2: "\<forall>y<u. \<exists>n. y < X n"
+    by (metis not_le)
+  fix r :: real assume "0 < r"
+  hence "u - r < u" by simp
+  hence "\<exists>m. u - r < X m" using 2 by simp
+  then obtain m where "u - r < X m" ..
+  with X have "\<forall>n\<ge>m. u - r < X n"
+    by (fast intro: less_le_trans)
+  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
+  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
+    using 1 by (simp add: diff_less_eq add_commute)
+qed
+
+text{*A standard proof of the theorem for monotone increasing sequence*}
+
+lemma Bseq_mono_convergent:
+   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
+  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
+
+lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
+  by (simp add: Bseq_def)
+
+text{*Main monotonicity theorem*}
+
+lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
+  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
+            Bseq_mono_convergent)
+
+lemma Cauchy_iff:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
+  unfolding Cauchy_def dist_norm ..
+
+lemma CauchyI:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e) \<Longrightarrow> Cauchy X"
+by (simp add: Cauchy_iff)
+
+lemma CauchyD:
+  fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "\<lbrakk>Cauchy X; 0 < e\<rbrakk> \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e"
+by (simp add: Cauchy_iff)
+
+lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
+  apply (simp add: subset_eq)
+  apply (rule BseqI'[where K="max (norm a) (norm b)"])
+  apply (erule_tac x=n in allE)
+  apply auto
+  done
+
+lemma incseq_bounded: "incseq X \<Longrightarrow> \<forall>i. X i \<le> (B::real) \<Longrightarrow> Bseq X"
+  by (intro Bseq_eq_bounded[of X "X 0" B]) (auto simp: incseq_def)
+
+lemma decseq_bounded: "decseq X \<Longrightarrow> \<forall>i. (B::real) \<le> X i \<Longrightarrow> Bseq X"
+  by (intro Bseq_eq_bounded[of X B "X 0"]) (auto simp: decseq_def)
+
+lemma incseq_convergent:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes "incseq X" and "\<forall>i. X i \<le> B"
+  obtains L where "X ----> L" "\<forall>i. X i \<le> L"
+proof atomize_elim
+  from incseq_bounded[OF assms] `incseq X` Bseq_monoseq_convergent[of X]
+  obtain L where "X ----> L"
+    by (auto simp: convergent_def monoseq_def incseq_def)
+  with `incseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. X i \<le> L)"
+    by (auto intro!: exI[of _ L] incseq_le)
+qed
+
+lemma decseq_convergent:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes "decseq X" and "\<forall>i. B \<le> X i"
+  obtains L where "X ----> L" "\<forall>i. L \<le> X i"
+proof atomize_elim
+  from decseq_bounded[OF assms] `decseq X` Bseq_monoseq_convergent[of X]
+  obtain L where "X ----> L"
+    by (auto simp: convergent_def monoseq_def decseq_def)
+  with `decseq X` show "\<exists>L. X ----> L \<and> (\<forall>i. L \<le> X i)"
+    by (auto intro!: exI[of _ L] decseq_le)
+qed
+
+subsubsection {* Cauchy Sequences are Bounded *}
+
+text{*A Cauchy sequence is bounded -- this is the standard
+  proof mechanization rather than the nonstandard proof*}
+
+lemma lemmaCauchy: "\<forall>n \<ge> M. norm (X M - X n) < (1::real)
+          ==>  \<forall>n \<ge> M. norm (X n :: 'a::real_normed_vector) < 1 + norm (X M)"
+apply (clarify, drule spec, drule (1) mp)
+apply (simp only: norm_minus_commute)
+apply (drule order_le_less_trans [OF norm_triangle_ineq2])
+apply simp
+done
+
+class banach = real_normed_vector + complete_space
+
+instance real :: banach by default
+
+subsection {* Power Sequences *}
+
+text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
+"x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
+  also fact that bounded and monotonic sequence converges.*}
+
+lemma Bseq_realpow: "[| 0 \<le> (x::real); x \<le> 1 |] ==> Bseq (%n. x ^ n)"
+apply (simp add: Bseq_def)
+apply (rule_tac x = 1 in exI)
+apply (simp add: power_abs)
+apply (auto dest: power_mono)
+done
+
+lemma monoseq_realpow: fixes x :: real shows "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
+apply (clarify intro!: mono_SucI2)
+apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto)
+done
+
+lemma convergent_realpow:
+  "[| 0 \<le> (x::real); x \<le> 1 |] ==> convergent (%n. x ^ n)"
+by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow)
+
+lemma LIMSEQ_inverse_realpow_zero: "1 < (x::real) \<Longrightarrow> (\<lambda>n. inverse (x ^ n)) ----> 0"
+  by (rule filterlim_compose[OF tendsto_inverse_0 filterlim_realpow_sequentially_gt1]) simp
+
+lemma LIMSEQ_realpow_zero:
+  "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+proof cases
+  assume "0 \<le> x" and "x \<noteq> 0"
+  hence x0: "0 < x" by simp
+  assume x1: "x < 1"
+  from x0 x1 have "1 < inverse x"
+    by (rule one_less_inverse)
+  hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
+    by (rule LIMSEQ_inverse_realpow_zero)
+  thus ?thesis by (simp add: power_inverse)
+qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
+
+lemma LIMSEQ_power_zero:
+  fixes x :: "'a::{real_normed_algebra_1}"
+  shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
+apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
+apply (simp add: power_abs norm_power_ineq)
+done
+
+lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) ----> 0"
+  by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
+
+text{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*}
+
+lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) ----> 0"
+  by (rule LIMSEQ_realpow_zero [OF abs_ge_zero])
+
+lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. c ^ n :: real) ----> 0"
+  by (rule LIMSEQ_power_zero) simp
+
+
+subsection {* Limits of Functions *}
+
+lemma LIM_eq:
+  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 dist_norm)
+
+lemma LIM_I:
+  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:
+  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:
+  fixes a :: "'a::real_normed_vector"
+  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+apply (rule topological_tendstoI)
+apply (drule (2) topological_tendstoD)
+apply (simp only: eventually_at dist_norm)
+apply (clarify, rule_tac x=d in exI, safe)
+apply (drule_tac x="x + k" in spec)
+apply (simp add: algebra_simps)
+done
+
+lemma LIM_offset_zero:
+  fixes a :: "'a::real_normed_vector"
+  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:
+  fixes a :: "'a::real_normed_vector"
+  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+by (drule_tac k="- a" in LIM_offset, simp)
+
+lemma LIM_zero:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  shows "(f ---> l) F \<Longrightarrow> ((\<lambda>x. f x - l) ---> 0) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_zero_cancel:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  shows "((\<lambda>x. f x - l) ---> 0) F \<Longrightarrow> (f ---> l) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_zero_iff:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  shows "((\<lambda>x. f x - l) ---> 0) F = (f ---> l) F"
+unfolding tendsto_iff dist_norm by simp
+
+lemma LIM_imp_LIM:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  fixes g :: "'a::topological_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"
+  by (rule metric_LIM_imp_LIM [OF f],
+    simp add: dist_norm le)
+
+lemma LIM_equal2:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_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"
+by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
+
+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"
+by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
+
+lemma real_LIM_sandwich_zero:
+  fixes f g :: "'a::topological_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"
+  shows "g -- a --> 0"
+proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
+  fix x assume x: "x \<noteq> a"
+  have "norm (g x - 0) = g x" by (simp add: 1 x)
+  also have "g x \<le> f x" by (rule 2 [OF x])
+  also have "f x \<le> \<bar>f x\<bar>" by (rule abs_ge_self)
+  also have "\<bar>f x\<bar> = norm (f x - 0)" by simp
+  finally show "norm (g x - 0) \<le> norm (f x - 0)" .
+qed
+
+
+subsection {* Continuity *}
+
+lemma LIM_isCont_iff:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_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:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
+  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+by (simp add: isCont_def LIM_isCont_iff)
+
+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"
+  shows "(\<lambda>x. g (f x)) -- a --> l"
+by (rule LIM_compose2 [OF f g inj])
+
+
+lemma isCont_norm [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+  by (fact continuous_norm)
+
+lemma isCont_rabs [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> real"
+  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
+  by (fact continuous_rabs)
+
+lemma isCont_add [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
+  by (fact continuous_add)
+
+lemma isCont_minus [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
+  by (fact continuous_minus)
+
+lemma isCont_diff [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
+  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
+  by (fact continuous_diff)
+
+lemma isCont_mult [simp]:
+  fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_algebra"
+  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
+  by (fact continuous_mult)
+
+lemma (in bounded_linear) isCont:
+  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
+  by (fact continuous)
+
+lemma (in bounded_bilinear) isCont:
+  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
+  by (fact continuous)
+
+lemmas isCont_scaleR [simp] = 
+  bounded_bilinear.isCont [OF bounded_bilinear_scaleR]
+
+lemmas isCont_of_real [simp] =
+  bounded_linear.isCont [OF bounded_linear_of_real]
+
+lemma isCont_power [simp]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
+  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
+  by (fact continuous_power)
+
+lemma isCont_setsum [simp]:
+  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
+  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
+  by (auto intro: continuous_setsum)
+
+lemmas isCont_intros =
+  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
+  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
+  isCont_of_real isCont_power isCont_sgn isCont_setsum
+
+subsection {* Uniform Continuity *}
+
+lemma (in bounded_linear) isUCont: "isUCont f"
+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"
+    using pos_bounded by fast
+  show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
+  proof (rule exI, safe)
+    from r K show "0 < r / K" by (rule divide_pos_pos)
+  next
+    fix x y :: 'a
+    assume xy: "norm (x - y) < r / K"
+    have "norm (f x - f y) = norm (f (x - y))" by (simp only: diff)
+    also have "\<dots> \<le> norm (x - y) * K" by (rule norm_le)
+    also from K xy have "\<dots> < r" by (simp only: pos_less_divide_eq)
+    finally show "norm (f x - f y) < r" .
+  qed
+qed
+
+lemma (in bounded_linear) Cauchy: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
+by (rule isUCont [THEN isUCont_Cauchy])
+
+
+lemma LIM_less_bound: 
+  fixes f :: "real \<Rightarrow> real"
+  assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
+  shows "0 \<le> f x"
+proof (rule tendsto_le_const)
+  show "(f ---> f x) (at_left x)"
+    using `isCont f x` by (simp add: filterlim_at_split isCont_def)
+  show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
+    using ev by (auto simp: eventually_within_less dist_real_def intro!: exI[of _ "x - b"])
+qed simp
 
 end