src/HOL/SEQ.thy

   shows "convergent X \<longleftrightarrow> convergent (\<lambda>n. - X n)"
 apply (simp add: convergent_def)
 apply (auto dest: LIMSEQ_minus)
 apply (drule LIMSEQ_minus, auto)
 done
+
+lemma lim_le:
+  fixes x :: real
+  assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
+  shows "lim f \<le> x"
+proof (rule classical)
+  assume "\<not> lim f \<le> x"
+  hence 0: "0 < lim f - x" by arith
+  have 1: "f----> lim f"
+    by (metis convergent_LIMSEQ_iff f) 
+  thus ?thesis
+    proof (simp add: LIMSEQ_iff)
+      assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
+      hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
+	by (metis 0)
+      from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
+	by blast
+      thus "lim f \<le> x"
+	by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
+                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
+    qed
+qed
 
 text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
 
 lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   unfolding Ex1_def

 *}
 
 lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
 by (simp add: isUbI setleI)
 
-lemma real_abs_diff_less_iff:
-  "(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
-by auto
-
 locale real_Cauchy =
   fixes X :: "nat \<Rightarrow> real"
   assumes X: "Cauchy X"
   fixes S :: "real set"
   defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"

     using CauchyD [OF X zero_less_one] by auto
   hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
   show "\<exists>x. x \<in> S"
   proof
     from N have "\<forall>n\<ge>N. X N - 1 < X n"
-      by (simp add: real_abs_diff_less_iff)
+      by (simp add: abs_diff_less_iff)
     thus "X N - 1 \<in> S" by (rule mem_S)
   qed
   show "\<exists>u. isUb UNIV S u"
   proof
     from N have "\<forall>n\<ge>N. X n < X N + 1"
-      by (simp add: real_abs_diff_less_iff)
+      by (simp add: abs_diff_less_iff)
     thus "isUb UNIV S (X N + 1)"
       by (rule bound_isUb)
   qed
 qed
 

   hence r: "0 < r/2" by simp
   obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
     using CauchyD [OF X r] by auto
   hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
   hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
-    by (simp only: real_norm_def real_abs_diff_less_iff)
+    by (simp only: real_norm_def abs_diff_less_iff)
 
   from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   hence "X N - r/2 \<in> S" by (rule mem_S)
   hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
 

   show "\<exists>N. \<forall>n\<ge>N. norm (X n - x) < r"
   proof (intro exI allI impI)
     fix n assume n: "N \<le> n"
     from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
     thus "norm (X n - x) < r" using 1 2
-      by (simp add: real_abs_diff_less_iff)
+      by (simp add: abs_diff_less_iff)
   qed
 qed
 
 lemma (in real_Cauchy) LIMSEQ_ex: "\<exists>x. X ----> x"
 proof -