1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -1425,9 +1425,6 @@
     1.4    @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
     1.5  *}
     1.6  
     1.7 -lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
     1.8 -by (simp add: isUbI setleI)
     1.9 -
    1.10  lemma increasing_LIMSEQ:
    1.11    fixes f :: "nat \<Rightarrow> real"
    1.12    assumes inc: "\<And>n. f n \<le> f (Suc n)"
    1.13 @@ -1454,40 +1451,33 @@
    1.14    then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
    1.15  
    1.16    { fix N x assume N: "\<forall>n\<ge>N. X n < x"
    1.17 -  have "isUb UNIV S x"
    1.18 -  proof (rule isUb_UNIV_I)
    1.19    fix y::real assume "y \<in> S"
    1.20    hence "\<exists>M. \<forall>n\<ge>M. y < X n"
    1.21      by (simp add: S_def)
    1.22    then obtain M where "\<forall>n\<ge>M. y < X n" ..
    1.23    hence "y < X (max M N)" by simp
    1.24    also have "\<dots> < x" using N by simp
    1.25 -  finally show "y \<le> x"
    1.26 -    by (rule order_less_imp_le)
    1.27 -  qed }
    1.28 +  finally have "y \<le> x"
    1.29 +    by (rule order_less_imp_le) }
    1.30    note bound_isUb = this 
    1.31  
    1.32 -  have "\<exists>u. isLub UNIV S u"
    1.33 -  proof (rule reals_complete)
    1.34    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
    1.35      using X[THEN metric_CauchyD, OF zero_less_one] by auto
    1.36    hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
    1.37 -  show "\<exists>x. x \<in> S"
    1.38 -  proof
    1.39 +  have [simp]: "S \<noteq> {}"
    1.40 +  proof (intro exI ex_in_conv[THEN iffD1])
    1.41      from N have "\<forall>n\<ge>N. X N - 1 < X n"
    1.42        by (simp add: abs_diff_less_iff dist_real_def)
    1.43      thus "X N - 1 \<in> S" by (rule mem_S)
    1.44    qed
    1.45 -  show "\<exists>u. isUb UNIV S u"
    1.46 +  have [simp]: "bdd_above S"
    1.47    proof
    1.48      from N have "\<forall>n\<ge>N. X n < X N + 1"
    1.49        by (simp add: abs_diff_less_iff dist_real_def)
    1.50 -    thus "isUb UNIV S (X N + 1)"
    1.51 +    thus "\<And>s. s \<in> S \<Longrightarrow>  s \<le> X N + 1"
    1.52        by (rule bound_isUb)
    1.53    qed
    1.54 -  qed
    1.55 -  then obtain x where x: "isLub UNIV S x" ..
    1.56 -  have "X ----> x"
    1.57 +  have "X ----> Sup S"
    1.58    proof (rule metric_LIMSEQ_I)
    1.59    fix r::real assume "0 < r"
    1.60    hence r: "0 < r/2" by simp
    1.61 @@ -1499,17 +1489,18 @@
    1.62  
    1.63    from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
    1.64    hence "X N - r/2 \<in> S" by (rule mem_S)
    1.65 -  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
    1.66 +  hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
    1.67  
    1.68    from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
    1.69 -  hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
    1.70 -  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
    1.71 +  from bound_isUb[OF this]
    1.72 +  have 2: "Sup S \<le> X N + r/2"
    1.73 +    by (intro cSup_least) simp_all
    1.74  
    1.75 -  show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
    1.76 +  show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r"
    1.77    proof (intro exI allI impI)
    1.78      fix n assume n: "N \<le> n"
    1.79      from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
    1.80 -    thus "dist (X n) x < r" using 1 2
    1.81 +    thus "dist (X n) (Sup S) < r" using 1 2
    1.82        by (simp add: abs_diff_less_iff dist_real_def)
    1.83    qed
    1.84    qed