src/HOL/SEQ.thy
 changeset 32707 836ec9d0a0c8 parent 32436 10cd49e0c067 child 32877 6f09346c7c08
```     1.1 --- a/src/HOL/SEQ.thy	Wed Sep 23 11:06:32 2009 +0100
1.2 +++ b/src/HOL/SEQ.thy	Fri Sep 25 13:47:28 2009 +0100
1.3 @@ -500,6 +500,28 @@
1.4  apply (drule LIMSEQ_minus, auto)
1.5  done
1.6
1.7 +lemma lim_le:
1.8 +  fixes x :: real
1.9 +  assumes f: "convergent f" and fn_le: "!!n. f n \<le> x"
1.10 +  shows "lim f \<le> x"
1.11 +proof (rule classical)
1.12 +  assume "\<not> lim f \<le> x"
1.13 +  hence 0: "0 < lim f - x" by arith
1.14 +  have 1: "f----> lim f"
1.15 +    by (metis convergent_LIMSEQ_iff f)
1.16 +  thus ?thesis
1.17 +    proof (simp add: LIMSEQ_iff)
1.18 +      assume "\<forall>r>0. \<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < r"
1.19 +      hence "\<exists>no. \<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
1.20 +	by (metis 0)
1.21 +      from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
1.22 +	by blast
1.23 +      thus "lim f \<le> x"
1.25 +                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le)
1.26 +    qed
1.27 +qed
1.28 +
1.29  text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
1.30
1.31  lemma nat_function_unique: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
1.32 @@ -1082,10 +1104,6 @@
1.33  lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
1.34  by (simp add: isUbI setleI)
1.35
1.36 -lemma real_abs_diff_less_iff:
1.37 -  "(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
1.38 -by auto
1.39 -
1.40  locale real_Cauchy =
1.41    fixes X :: "nat \<Rightarrow> real"
1.42    assumes X: "Cauchy X"
1.43 @@ -1122,13 +1140,13 @@
1.44    show "\<exists>x. x \<in> S"
1.45    proof
1.46      from N have "\<forall>n\<ge>N. X N - 1 < X n"
1.47 -      by (simp add: real_abs_diff_less_iff)
1.48 +      by (simp add: abs_diff_less_iff)
1.49      thus "X N - 1 \<in> S" by (rule mem_S)
1.50    qed
1.51    show "\<exists>u. isUb UNIV S u"
1.52    proof
1.53      from N have "\<forall>n\<ge>N. X n < X N + 1"
1.54 -      by (simp add: real_abs_diff_less_iff)
1.55 +      by (simp add: abs_diff_less_iff)
1.56      thus "isUb UNIV S (X N + 1)"
1.57        by (rule bound_isUb)
1.58    qed
1.59 @@ -1144,7 +1162,7 @@
1.60      using CauchyD [OF X r] by auto
1.61    hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
1.62    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
1.63 -    by (simp only: real_norm_def real_abs_diff_less_iff)
1.64 +    by (simp only: real_norm_def abs_diff_less_iff)
1.65
1.66    from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
1.67    hence "X N - r/2 \<in> S" by (rule mem_S)
1.68 @@ -1159,7 +1177,7 @@
1.69      fix n assume n: "N \<le> n"
1.70      from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
1.71      thus "norm (X n - x) < r" using 1 2
1.72 -      by (simp add: real_abs_diff_less_iff)
1.73 +      by (simp add: abs_diff_less_iff)
1.74    qed
1.75  qed
1.76
```