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.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.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)