# HG changeset patch
# User huffman
# Date 1166055567 -3600
# Node ID 3d8ab65450498aa01b4957b655b55b87c78597af
# Parent  1701f05aa1b09c1ed17f9ad5e9b573a0b7ca889d
remove references to star_n and FreeUltrafilterNat; new proof of NSBseq_Bseq

diff -r 1701f05aa1b0 -r 3d8ab6545049 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Dec 13 23:15:39 2006 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Dec 14 01:19:27 2006 +0100
@@ -235,10 +235,14 @@
 
 lemma HFinite_exp [simp]:
      "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
-by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
-         simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
-                   convergent_NSconvergent_iff [symmetric] 
-                   summable_convergent_sumr_iff [symmetric] summable_exp)
+unfolding sumhr_app
+apply (simp only: star_zero_def starfun2_star_of)
+apply (rule NSBseqD2)
+apply (rule NSconvergent_NSBseq)
+apply (rule convergent_NSconvergent_iff [THEN iffD1])
+apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_exp)
+done
 
 lemma exphr_zero [simp]: "exphr 0 = 1"
 apply (simp add: exphr_def sumhr_split_add
@@ -438,10 +442,12 @@
      "sumhr (0, whn, %n. (if even(n) then 0 else  
               ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
               \<in> HFinite"
-apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
-            simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
-                      convergent_NSconvergent_iff [symmetric] 
-                      summable_convergent_sumr_iff [symmetric])
+unfolding sumhr_app
+apply (simp only: star_zero_def starfun2_star_of)
+apply (rule NSBseqD2)
+apply (rule NSconvergent_NSBseq)
+apply (rule convergent_NSconvergent_iff [THEN iffD1])
+apply (rule summable_convergent_sumr_iff [THEN iffD1])
 apply (simp only: One_nat_def summable_sin)
 done
 
@@ -462,10 +468,14 @@
      "sumhr (0, whn, %n. (if even(n) then  
             ((- 1) ^ (n div 2))/(real (fact n)) else  
             0) * x ^ n) \<in> HFinite"
-by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
-         simp add: starfunNat_sumr [symmetric] starfun hypnat_omega_def
-                   convergent_NSconvergent_iff [symmetric] 
-                   summable_convergent_sumr_iff [symmetric] summable_cos)
+unfolding sumhr_app
+apply (simp only: star_zero_def starfun2_star_of)
+apply (rule NSBseqD2)
+apply (rule NSconvergent_NSBseq)
+apply (rule convergent_NSconvergent_iff [THEN iffD1])
+apply (rule summable_convergent_sumr_iff [THEN iffD1])
+apply (rule summable_cos)
+done
 
 lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
 by transfer (rule cos_zero)
diff -r 1701f05aa1b0 -r 3d8ab6545049 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Dec 13 23:15:39 2006 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Thu Dec 14 01:19:27 2006 +0100
@@ -480,6 +480,16 @@
 lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
 by (simp add: NSBseq_def)
 
+lemma Standard_subset_HFinite: "Standard \<subseteq> HFinite"
+unfolding Standard_def by auto
+
+lemma NSBseqD2: "NSBseq X \<Longrightarrow> ( *f* X) N \<in> HFinite"
+apply (cases "N \<in> HNatInfinite")
+apply (erule (1) NSBseqD)
+apply (rule subsetD [OF Standard_subset_HFinite])
+apply (simp add: HNatInfinite_def Nats_eq_Standard)
+done
+
 lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
 by (simp add: NSBseq_def)
 
@@ -502,76 +512,34 @@
 
 text{*The nonstandard definition implies the standard definition*}
 
-(* similar to NSLIM proof in REALTOPOS *)
-
-text{* We need to get rid of the real variable and do so by proving the
-   following, which relies on the Archimedean property of the reals.
-   When we skolemize we then get the required function @{term "f::nat=>nat"}.
-   Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"}
-   which woulid be useless.*}
-
-lemma lemmaNSBseq:
-     "\<forall>K > 0. \<exists>n. K < norm (X n)
-      ==> \<forall>N. \<exists>n. real(Suc N) < norm (X n)"
-apply safe
-apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast)
-done
-
-lemma lemmaNSBseq2: "\<forall>K > 0. \<exists>n::nat. K < norm (X n)
-                     ==> \<exists>f. \<forall>N. real(Suc N) < norm (X (f N))"
-apply (drule lemmaNSBseq)
-apply (drule no_choice, blast)
-done
-
-lemma real_seq_to_hypreal_HInfinite:
-     "\<forall>N. real(Suc N) < norm (X (f N))
-      ==>  star_n (X o f) : HInfinite"
-apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def)
-apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real)
-apply (drule FreeUltrafilterNat_all)
-apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
-apply (auto simp add: real_of_nat_Suc)
+lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
+apply (insert HInfinite_omega)
+apply (simp add: HInfinite_def)
+apply (simp add: order_less_imp_le)
 done
 
-text{* Now prove that we can get out an infinite hypernatural as well
-     defined using the skolem function  @{term "f::nat=>nat"} above*}
-
-lemma lemma_finite_NSBseq:
-     "{n. f n \<le> Suc u & real(Suc n) < norm (X (f n))} \<le>
-      {n. f n \<le> u & real(Suc n) < norm (X (f n))} Un
-      {n. real(Suc n) < norm (X (Suc u))}"
-by (auto dest!: le_imp_less_or_eq)
-
-lemma lemma_finite_NSBseq2:
-     "finite {n. f n \<le> (u::nat) &  real(Suc n) < norm (X(f n))}"
-apply (induct "u")
-apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset])
-apply (rule_tac B = "{n. real (Suc n) < norm (X 0) }" in finite_subset)
-apply (auto intro: finite_real_of_nat_less_real 
-            simp add: real_of_nat_Suc less_diff_eq [symmetric])
-done
-
-lemma HNatInfinite_skolem_f:
-     "\<forall>N. real(Suc N) < norm (X (f N))
-      ==> star_n f : HNatInfinite"
-apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff)
-apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem)
-apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 
-apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < norm (X (f n))} =
-                    {n. f n \<le> u} \<inter> {N. real (Suc N) < norm (X (f N))}")
-apply (erule ssubst) 
- apply (auto simp add: linorder_not_less Compl_def)
-done
-
-lemma NSBseq_Bseq: "NSBseq X ==> Bseq X"
-apply (simp add: Bseq_def NSBseq_def)
-apply (rule ccontr)
-apply (auto simp add: linorder_not_less [symmetric])
-apply (drule lemmaNSBseq2, safe)
-apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite)
-apply (drule HNatInfinite_skolem_f [THEN [2] bspec])
-apply (auto simp add: starfun o_def HFinite_HInfinite_iff)
-done
+lemma NSBseq_Bseq: "NSBseq X \<Longrightarrow> Bseq X"
+proof (rule ccontr)
+  let ?n = "\<lambda>K. LEAST n. K < norm (X n)"
+  assume "NSBseq X"
+  hence finite: "( *f* X) (( *f* ?n) \<omega>) \<in> HFinite"
+    by (rule NSBseqD2)
+  assume "\<not> Bseq X"
+  hence "\<forall>K>0. \<exists>n. K < norm (X n)"
+    by (simp add: Bseq_def linorder_not_le)
+  hence "\<forall>K>0. K < norm (X (?n K))"
+    by (auto intro: LeastI_ex)
+  hence "\<forall>K>0. K < hnorm (( *f* X) (( *f* ?n) K))"
+    by transfer
+  hence "\<omega> < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+    by simp
+  hence "\<forall>r\<in>\<real>. r < hnorm (( *f* X) (( *f* ?n) \<omega>))"
+    by (simp add: order_less_trans [OF SReal_less_omega])
+  hence "( *f* X) (( *f* ?n) \<omega>) \<in> HInfinite"
+    by (simp add: HInfinite_def)
+  with finite show "False"
+    by (simp add: HFinite_HInfinite_iff)
+qed
 
 text{* Equivalence of nonstandard and standard definitions
   for a bounded sequence*}
@@ -1155,24 +1123,6 @@
 lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < (1::real) ==> (%n. c ^ n) ----NS> 0"
 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric])
 
-subsection{*Hyperreals and Sequences*}
-
-text{*A bounded sequence is a finite hyperreal*}
-lemma NSBseq_HFinite_hypreal: "NSBseq X ==> star_n X : HFinite"
-by (auto intro!: bexI lemma_starrel_refl 
-            intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset]
-            simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric]
-                      Bseq_iff1a)
-
-text{*A sequence converging to zero defines an infinitesimal*}
-lemma NSLIMSEQ_zero_Infinitesimal_hypreal:
-      "X ----NS> 0 ==> star_n X : Infinitesimal"
-apply (simp add: NSLIMSEQ_def)
-apply (drule_tac x = whn in bspec)
-apply (simp add: HNatInfinite_whn)
-apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfun)
-done
-
 (***---------------------------------------------------------------
     Theorems proved by Harrison in HOL that we do not need
     in order to prove equivalence between Cauchy criterion