new proof of Bseq_NSbseq using transfer
Wed, 01 Nov 2006 16:48:58 +0100
changeset 21139 c957e02e7a36
parent 21138 afdd72fc6c4f
child 21140 1c0805003c4f
new proof of Bseq_NSbseq using transfer
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Nov 01 16:11:31 2006 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Nov 01 16:48:58 2006 +0100
@@ -479,14 +479,16 @@
 by auto
 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
-apply (simp add: Bseq_def NSBseq_def, safe)
-apply (rule_tac x = N in star_cases)
-apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff 
-                      HNatInfinite_FreeUltrafilterNat_iff)
-apply (drule_tac f = Xa in lemma_Bseq)
-apply (rule_tac x = "K+1" in exI)
-apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra)
+proof (unfold NSBseq_def, safe)
+  assume X: "Bseq X"
+  fix N assume N: "N \<in> HNatInfinite"
+  from BseqD [OF X] obtain K where "\<forall>n. norm (X n) \<le> K" by fast
+  hence "\<forall>N. hnorm (starfun X N) \<le> star_of K" by transfer
+  hence "hnorm (starfun X N) \<le> star_of K" by simp
+  also have "star_of K < star_of (K + 1)" by simp
+  finally have "\<exists>x\<in>Reals. hnorm (starfun X N) < x" by (rule bexI, simp)
+  thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
 text{*The nonstandard definition implies the standard definition*}