src/HOL/SEQ.thy
changeset 32064 53ca12ff305d
parent 31588 2651f172c38b
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/SEQ.thy	Mon Jul 13 08:25:43 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Tue Jul 14 15:54:19 2009 +0200
     1.3 @@ -113,8 +113,8 @@
     1.4  lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
     1.5  unfolding Bfun_def eventually_sequentially
     1.6  apply (rule iffI)
     1.7 -apply (simp add: Bseq_def, fast)
     1.8 -apply (fast intro: BseqI2')
     1.9 +apply (simp add: Bseq_def)
    1.10 +apply (auto intro: BseqI2')
    1.11  done
    1.12  
    1.13  
    1.14 @@ -762,13 +762,25 @@
    1.15  lemma lemma_NBseq_def:
    1.16       "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
    1.17        (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.18 -apply auto
    1.19 - prefer 2 apply force
    1.20 -apply (cut_tac x = K in reals_Archimedean2, clarify)
    1.21 -apply (rule_tac x = n in exI, clarify)
    1.22 -apply (drule_tac x = na in spec)
    1.23 -apply (auto simp add: real_of_nat_Suc)
    1.24 -done
    1.25 +proof auto
    1.26 +  fix K :: real
    1.27 +  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
    1.28 +  then have "K \<le> real (Suc n)" by auto
    1.29 +  assume "\<forall>m. norm (X m) \<le> K"
    1.30 +  have "\<forall>m. norm (X m) \<le> real (Suc n)"
    1.31 +  proof
    1.32 +    fix m :: 'a
    1.33 +    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
    1.34 +    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
    1.35 +  qed
    1.36 +  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
    1.37 +next
    1.38 +  fix N :: nat
    1.39 +  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
    1.40 +  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
    1.41 +  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
    1.42 +qed
    1.43 +
    1.44  
    1.45  text{* alternative definition for Bseq *}
    1.46  lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    1.47 @@ -1105,7 +1117,7 @@
    1.48  lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
    1.49  proof (rule reals_complete)
    1.50    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
    1.51 -    using CauchyD [OF X zero_less_one] by fast
    1.52 +    using CauchyD [OF X zero_less_one] by auto
    1.53    hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
    1.54    show "\<exists>x. x \<in> S"
    1.55    proof
    1.56 @@ -1129,7 +1141,7 @@
    1.57    fix r::real assume "0 < r"
    1.58    hence r: "0 < r/2" by simp
    1.59    obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
    1.60 -    using CauchyD [OF X r] by fast
    1.61 +    using CauchyD [OF X r] by auto
    1.62    hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
    1.63    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
    1.64      by (simp only: real_norm_def real_abs_diff_less_iff)