src/HOL/Hyperreal/SEQ.thy
 author nipkow Mon Oct 11 07:42:22 2004 +0200 (2004-10-11) changeset 15236 f289e8ba2bb3 parent 15229 1eb23f805c06 child 15241 a3949068537e permissions -rw-r--r--
Proofs needed to be updated because induction now preserves name of
induction variable.
 paulson@10751 1 (* Title : SEQ.thy paulson@10751 2 Author : Jacques D. Fleuriot paulson@10751 3 Copyright : 1998 University of Cambridge paulson@10751 4 Description : Convergence of sequences and series paulson@15082 5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 paulson@15082 6 *) paulson@10751 7 nipkow@15131 8 theory SEQ nipkow@15236 9 imports NatStar nipkow@15131 10 begin paulson@10751 11 paulson@10751 12 constdefs paulson@10751 13 paulson@15082 14 LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60) paulson@15082 15 --{*Standard definition of convergence of sequence*} paulson@15082 16 "X ----> L == (\r. 0 < r --> (\no. \n. no \ n --> \X n + -L\ < r))" paulson@10751 17 paulson@15082 18 NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60) paulson@15082 19 --{*Nonstandard definition of convergence of sequence*} paulson@15082 20 "X ----NS> L == (\N \ HNatInfinite. ( *fNat* X) N \ hypreal_of_real L)" paulson@15082 21 paulson@15082 22 lim :: "(nat => real) => real" paulson@15082 23 --{*Standard definition of limit using choice operator*} paulson@10751 24 "lim X == (@L. (X ----> L))" paulson@10751 25 paulson@15082 26 nslim :: "(nat => real) => real" paulson@15082 27 --{*Nonstandard definition of limit using choice operator*} paulson@10751 28 "nslim X == (@L. (X ----NS> L))" paulson@10751 29 paulson@15082 30 convergent :: "(nat => real) => bool" paulson@15082 31 --{*Standard definition of convergence*} paulson@15082 32 "convergent X == (\L. (X ----> L))" paulson@10751 33 paulson@15082 34 NSconvergent :: "(nat => real) => bool" paulson@15082 35 --{*Nonstandard definition of convergence*} paulson@15082 36 "NSconvergent X == (\L. (X ----NS> L))" paulson@15082 37 paulson@15082 38 Bseq :: "(nat => real) => bool" paulson@15082 39 --{*Standard definition for bounded sequence*} paulson@15082 40 "Bseq X == (\K. (0 < K & (\n. \X n\ \ K)))" paulson@10751 41 paulson@15082 42 NSBseq :: "(nat=>real) => bool" paulson@15082 43 --{*Nonstandard definition for bounded sequence*} paulson@15082 44 "NSBseq X == (\N \ HNatInfinite. ( *fNat* X) N : HFinite)" paulson@15082 45 paulson@15082 46 monoseq :: "(nat=>real)=>bool" paulson@15082 47 --{*Definition for monotonicity*} paulson@15082 48 "monoseq X == ((\(m::nat) n. m \ n --> X m \ X n) | paulson@15082 49 (\m n. m \ n --> X n \ X m))" paulson@10751 50 paulson@15082 51 subseq :: "(nat => nat) => bool" paulson@15082 52 --{*Definition of subsequence*} paulson@15082 53 "subseq f == (\m n. m < n --> (f m) < (f n))" paulson@10751 54 paulson@15082 55 Cauchy :: "(nat => real) => bool" paulson@15082 56 --{*Standard definition of the Cauchy condition*} paulson@15082 57 "Cauchy X == (\e. (0 < e --> paulson@15082 58 (\M. (\m n. M \ m & M \ n paulson@10751 59 --> abs((X m) + -(X n)) < e))))" paulson@10751 60 paulson@15082 61 NSCauchy :: "(nat => real) => bool" paulson@15082 62 --{*Nonstandard definition*} paulson@15082 63 "NSCauchy X == (\M \ HNatInfinite. \N \ HNatInfinite. paulson@15082 64 ( *fNat* X) M \ ( *fNat* X) N)" paulson@15082 65 paulson@15082 66 paulson@15082 67 paulson@15082 68 text{* Example of an hypersequence (i.e. an extended standard sequence) paulson@15082 69 whose term with an hypernatural suffix is an infinitesimal i.e. paulson@15082 70 the whn'nth term of the hypersequence is a member of Infinitesimal*} paulson@15082 71 paulson@15082 72 lemma SEQ_Infinitesimal: paulson@15082 73 "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" paulson@15082 74 apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat) paulson@15082 75 apply (rule bexI, rule_tac [2] lemma_hyprel_refl) paulson@15229 76 apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat) paulson@15082 77 done paulson@15082 78 paulson@15082 79 paulson@15082 80 subsection{*LIMSEQ and NSLIMSEQ*} paulson@15082 81 paulson@15082 82 lemma LIMSEQ_iff: paulson@15082 83 "(X ----> L) = paulson@15082 84 (\r. 0 (\no. \n. no \ n --> \X n + -L\ < r))" paulson@15082 85 by (simp add: LIMSEQ_def) paulson@15082 86 paulson@15082 87 lemma NSLIMSEQ_iff: paulson@15082 88 "(X ----NS> L) = (\N \ HNatInfinite. ( *fNat* X) N \ hypreal_of_real L)" paulson@15082 89 by (simp add: NSLIMSEQ_def) paulson@15082 90 paulson@15082 91 paulson@15082 92 text{*LIMSEQ ==> NSLIMSEQ*} paulson@15082 93 paulson@15082 94 lemma LIMSEQ_NSLIMSEQ: paulson@15082 95 "X ----> L ==> X ----NS> L" paulson@15082 96 apply (simp add: LIMSEQ_def NSLIMSEQ_def) paulson@15082 97 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) paulson@15082 98 apply (rule_tac z = N in eq_Abs_hypnat) paulson@15082 99 apply (rule approx_minus_iff [THEN iffD2]) paulson@15082 100 apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def paulson@15082 101 hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) paulson@15082 102 apply (rule bexI [OF _ lemma_hyprel_refl], safe) paulson@15082 103 apply (drule_tac x = u in spec, safe) paulson@15082 104 apply (drule_tac x = no in spec, fuf) paulson@15082 105 apply (blast dest: less_imp_le) paulson@15082 106 done paulson@15082 107 paulson@15082 108 paulson@15082 109 text{*NSLIMSEQ ==> LIMSEQ*} paulson@15082 110 paulson@15082 111 lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \n. n \ f n paulson@15082 112 ==> {n. f n = 0} = {0} | {n. f n = 0} = {}" paulson@15082 113 apply auto paulson@15082 114 apply (drule_tac x = xa in spec) paulson@15082 115 apply (drule_tac [2] x = x in spec, auto) paulson@15082 116 done paulson@15082 117 paulson@15082 118 lemma lemma_NSLIMSEQ2: "{n. f n \ Suc u} = {n. f n \ u} Un {n. f n = Suc u}" paulson@15082 119 by (auto simp add: le_Suc_eq) paulson@15082 120 paulson@15082 121 lemma lemma_NSLIMSEQ3: paulson@15082 122 "!!(f::nat=>nat). \n. n \ f n ==> {n. f n = Suc u} \ {n. n \ Suc u}" paulson@15082 123 apply auto paulson@15082 124 apply (drule_tac x = x in spec, auto) paulson@15082 125 done paulson@15082 126 paulson@15082 127 text{* the following sequence @{term "f(n)"} defines a hypernatural *} paulson@15082 128 lemma NSLIMSEQ_finite_set: paulson@15082 129 "!!(f::nat=>nat). \n. n \ f n ==> finite {n. f n \ u}" paulson@15082 130 apply (induct u) paulson@15082 131 apply (auto simp add: lemma_NSLIMSEQ2) paulson@15082 132 apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def]) paulson@15082 133 apply (drule lemma_NSLIMSEQ1, safe) paulson@15082 134 apply (simp_all (no_asm_simp)) paulson@15082 135 done paulson@15082 136 paulson@15082 137 lemma Compl_less_set: "- {n. u < (f::nat=>nat) n} = {n. f n \ u}" paulson@15082 138 by (auto dest: less_le_trans simp add: le_def) paulson@15082 139 paulson@15082 140 text{* the index set is in the free ultrafilter *} paulson@15082 141 lemma FreeUltrafilterNat_NSLIMSEQ: paulson@15082 142 "!!(f::nat=>nat). \n. n \ f n ==> {n. u < f n} : FreeUltrafilterNat" paulson@15082 143 apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2]) paulson@15082 144 apply (rule FreeUltrafilterNat_finite) paulson@15082 145 apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set) paulson@15082 146 done paulson@15082 147 paulson@15082 148 text{* thus, the sequence defines an infinite hypernatural! *} paulson@15082 149 lemma HNatInfinite_NSLIMSEQ: "\n. n \ f n paulson@15082 150 ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite" paulson@15082 151 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) paulson@15082 152 apply (rule bexI [OF _ lemma_hypnatrel_refl], safe) paulson@15082 153 apply (erule FreeUltrafilterNat_NSLIMSEQ) paulson@15082 154 done paulson@15082 155 paulson@15082 156 lemma lemmaLIM: paulson@15082 157 "{n. X (f n) + - L = Y n} Int {n. \Y n\ < r} \ paulson@15082 158 {n. \X (f n) + - L\ < r}" paulson@15082 159 by auto paulson@15082 160 paulson@15082 161 lemma lemmaLIM2: paulson@15082 162 "{n. \X (f n) + - L\ < r} Int {n. r \ abs (X (f n) + - (L::real))} = {}" paulson@15082 163 by auto paulson@15082 164 paulson@15082 165 lemma lemmaLIM3: "[| 0 < r; \n. r \ \X (f n) + - L\; paulson@15082 166 ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + paulson@15082 167 - hypreal_of_real L \ 0 |] ==> False" paulson@15082 168 apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) paulson@15082 169 apply (rename_tac "Y") paulson@15082 170 apply (drule_tac x = r in spec, safe) paulson@15082 171 apply (drule FreeUltrafilterNat_Int, assumption) paulson@15082 172 apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset]) paulson@15082 173 apply (drule FreeUltrafilterNat_all) paulson@15082 174 apply (erule_tac V = "{n. \Y n\ < r} : FreeUltrafilterNat" in thin_rl) paulson@15082 175 apply (drule FreeUltrafilterNat_Int, assumption) paulson@15082 176 apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty) paulson@15082 177 done paulson@15082 178 paulson@15082 179 lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L" paulson@15082 180 apply (simp add: LIMSEQ_def NSLIMSEQ_def) paulson@15082 181 apply (rule ccontr, simp, safe) paulson@15082 182 txt{* skolemization step *} paulson@15082 183 apply (drule choice, safe) paulson@15082 184 apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec) paulson@15082 185 apply (drule_tac [2] approx_minus_iff [THEN iffD1]) paulson@15082 186 apply (simp_all add: linorder_not_less) paulson@15082 187 apply (blast intro: HNatInfinite_NSLIMSEQ) paulson@15082 188 apply (blast intro: lemmaLIM3) paulson@15082 189 done paulson@15082 190 paulson@15082 191 text{* Now, the all-important result is trivially proved! *} paulson@15082 192 theorem LIMSEQ_NSLIMSEQ_iff: "(f ----> L) = (f ----NS> L)" paulson@15082 193 by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) paulson@15082 194 paulson@15082 195 paulson@15082 196 subsection{*Theorems About Sequences*} paulson@15082 197 paulson@15082 198 lemma NSLIMSEQ_const: "(%n. k) ----NS> k" paulson@15082 199 by (simp add: NSLIMSEQ_def) paulson@15082 200 paulson@15082 201 lemma LIMSEQ_const: "(%n. k) ----> k" paulson@15082 202 by (simp add: LIMSEQ_def) paulson@15082 203 paulson@15082 204 lemma NSLIMSEQ_add: paulson@15082 205 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b" paulson@15082 206 by (auto intro: approx_add simp add: NSLIMSEQ_def starfunNat_add [symmetric]) paulson@15082 207 paulson@15082 208 lemma LIMSEQ_add: "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b" paulson@15082 209 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add) paulson@15082 210 paulson@15082 211 lemma NSLIMSEQ_mult: paulson@15082 212 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b" paulson@15082 213 by (auto intro!: approx_mult_HFinite paulson@15082 214 simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric]) paulson@15082 215 paulson@15082 216 lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" paulson@15082 217 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult) paulson@15082 218 paulson@15082 219 lemma NSLIMSEQ_minus: "X ----NS> a ==> (%n. -(X n)) ----NS> -a" paulson@15082 220 by (auto simp add: NSLIMSEQ_def starfunNat_minus [symmetric]) paulson@15082 221 paulson@15082 222 lemma LIMSEQ_minus: "X ----> a ==> (%n. -(X n)) ----> -a" paulson@15082 223 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus) paulson@15082 224 paulson@15082 225 lemma LIMSEQ_minus_cancel: "(%n. -(X n)) ----> -a ==> X ----> a" paulson@15082 226 by (drule LIMSEQ_minus, simp) paulson@15082 227 paulson@15082 228 lemma NSLIMSEQ_minus_cancel: "(%n. -(X n)) ----NS> -a ==> X ----NS> a" paulson@15082 229 by (drule NSLIMSEQ_minus, simp) paulson@15082 230 paulson@15082 231 lemma NSLIMSEQ_add_minus: paulson@15082 232 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + -Y n) ----NS> a + -b" paulson@15082 233 by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y]) paulson@15082 234 paulson@15082 235 lemma LIMSEQ_add_minus: paulson@15082 236 "[| X ----> a; Y ----> b |] ==> (%n. X n + -Y n) ----> a + -b" paulson@15082 237 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus) paulson@15082 238 paulson@15082 239 lemma LIMSEQ_diff: "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b" paulson@15082 240 apply (simp add: diff_minus) paulson@15082 241 apply (blast intro: LIMSEQ_add_minus) paulson@15082 242 done paulson@15082 243 paulson@15082 244 lemma NSLIMSEQ_diff: paulson@15082 245 "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b" paulson@15082 246 apply (simp add: diff_minus) paulson@15082 247 apply (blast intro: NSLIMSEQ_add_minus) paulson@15082 248 done paulson@15082 249 paulson@15082 250 text{*Proof is like that of @{text NSLIM_inverse}.*} paulson@15082 251 lemma NSLIMSEQ_inverse: paulson@15082 252 "[| X ----NS> a; a ~= 0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)" paulson@15082 253 by (simp add: NSLIMSEQ_def starfunNat_inverse [symmetric] paulson@15082 254 hypreal_of_real_approx_inverse) paulson@15082 255 paulson@15082 256 paulson@15082 257 text{*Standard version of theorem*} paulson@15082 258 lemma LIMSEQ_inverse: paulson@15082 259 "[| X ----> a; a ~= 0 |] ==> (%n. inverse(X n)) ----> inverse(a)" paulson@15082 260 by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff) paulson@15082 261 paulson@15082 262 lemma NSLIMSEQ_mult_inverse: paulson@15082 263 "[| X ----NS> a; Y ----NS> b; b ~= 0 |] ==> (%n. X n / Y n) ----NS> a/b" paulson@15082 264 by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) paulson@15082 265 paulson@15082 266 lemma LIMSEQ_divide: paulson@15082 267 "[| X ----> a; Y ----> b; b ~= 0 |] ==> (%n. X n / Y n) ----> a/b" paulson@15082 268 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) paulson@15082 269 paulson@15082 270 text{*Uniqueness of limit*} paulson@15082 271 lemma NSLIMSEQ_unique: "[| X ----NS> a; X ----NS> b |] ==> a = b" paulson@15082 272 apply (simp add: NSLIMSEQ_def) paulson@15082 273 apply (drule HNatInfinite_whn [THEN [2] bspec])+ paulson@15082 274 apply (auto dest: approx_trans3) paulson@15082 275 done paulson@15082 276 paulson@15082 277 lemma LIMSEQ_unique: "[| X ----> a; X ----> b |] ==> a = b" paulson@15082 278 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique) paulson@15082 279 paulson@15082 280 paulson@15082 281 subsection{*Nslim and Lim*} paulson@15082 282 paulson@15082 283 lemma limI: "X ----> L ==> lim X = L" paulson@15082 284 apply (simp add: lim_def) paulson@15082 285 apply (blast intro: LIMSEQ_unique) paulson@15082 286 done paulson@15082 287 paulson@15082 288 lemma nslimI: "X ----NS> L ==> nslim X = L" paulson@15082 289 apply (simp add: nslim_def) paulson@15082 290 apply (blast intro: NSLIMSEQ_unique) paulson@15082 291 done paulson@15082 292 paulson@15082 293 lemma lim_nslim_iff: "lim X = nslim X" paulson@15082 294 by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff) paulson@15082 295 paulson@15082 296 paulson@15082 297 subsection{*Convergence*} paulson@15082 298 paulson@15082 299 lemma convergentD: "convergent X ==> \L. (X ----> L)" paulson@15082 300 by (simp add: convergent_def) paulson@15082 301 paulson@15082 302 lemma convergentI: "(X ----> L) ==> convergent X" paulson@15082 303 by (auto simp add: convergent_def) paulson@15082 304 paulson@15082 305 lemma NSconvergentD: "NSconvergent X ==> \L. (X ----NS> L)" paulson@15082 306 by (simp add: NSconvergent_def) paulson@15082 307 paulson@15082 308 lemma NSconvergentI: "(X ----NS> L) ==> NSconvergent X" paulson@15082 309 by (auto simp add: NSconvergent_def) paulson@15082 310 paulson@15082 311 lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X" paulson@15082 312 by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff) paulson@15082 313 paulson@15082 314 lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X ----NS> nslim X)" paulson@15082 315 by (auto intro: someI simp add: NSconvergent_def nslim_def) paulson@15082 316 paulson@15082 317 lemma convergent_LIMSEQ_iff: "convergent X = (X ----> lim X)" paulson@15082 318 by (auto intro: someI simp add: convergent_def lim_def) paulson@15082 319 paulson@15082 320 text{*Subsequence (alternative definition, (e.g. Hoskins)*} paulson@15082 321 paulson@15082 322 lemma subseq_Suc_iff: "subseq f = (\n. (f n) < (f (Suc n)))" paulson@15082 323 apply (simp add: subseq_def) paulson@15082 324 apply (auto dest!: less_imp_Suc_add) paulson@15082 325 apply (induct_tac k) paulson@15082 326 apply (auto intro: less_trans) paulson@15082 327 done paulson@15082 328 paulson@15082 329 paulson@15082 330 subsection{*Monotonicity*} paulson@15082 331 paulson@15082 332 lemma monoseq_Suc: paulson@15082 333 "monoseq X = ((\n. X n \ X (Suc n)) paulson@15082 334 | (\n. X (Suc n) \ X n))" paulson@15082 335 apply (simp add: monoseq_def) paulson@15082 336 apply (auto dest!: le_imp_less_or_eq) paulson@15082 337 apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) paulson@15082 338 apply (induct_tac "ka") paulson@15082 339 apply (auto intro: order_trans) paulson@15082 340 apply (erule swap) paulson@15082 341 apply (induct_tac "k") paulson@15082 342 apply (auto intro: order_trans) paulson@15082 343 done paulson@15082 344 paulson@15082 345 lemma monoI1: "\m n. m \ n --> X m \ X n ==> monoseq X" paulson@15082 346 by (simp add: monoseq_def) paulson@15082 347 paulson@15082 348 lemma monoI2: "\m n. m \ n --> X n \ X m ==> monoseq X" paulson@15082 349 by (simp add: monoseq_def) paulson@15082 350 paulson@15082 351 lemma mono_SucI1: "\n. X n \ X (Suc n) ==> monoseq X" paulson@15082 352 by (simp add: monoseq_Suc) paulson@15082 353 paulson@15082 354 lemma mono_SucI2: "\n. X (Suc n) \ X n ==> monoseq X" paulson@15082 355 by (simp add: monoseq_Suc) paulson@15082 356 paulson@15082 357 paulson@15082 358 subsection{*Bounded Sequence*} paulson@15082 359 paulson@15082 360 lemma BseqD: "Bseq X ==> \K. 0 < K & (\n. \X n\ \ K)" paulson@15082 361 by (simp add: Bseq_def) paulson@15082 362 paulson@15082 363 lemma BseqI: "[| 0 < K; \n. \X n\ \ K |] ==> Bseq X" paulson@15082 364 by (auto simp add: Bseq_def) paulson@15082 365 paulson@15082 366 lemma lemma_NBseq_def: paulson@15082 367 "(\K. 0 < K & (\n. \X n\ \ K)) = paulson@15082 368 (\N. \n. \X n\ \ real(Suc N))" paulson@15082 369 apply auto paulson@15082 370 prefer 2 apply force paulson@15082 371 apply (cut_tac x = K in reals_Archimedean2, clarify) paulson@15082 372 apply (rule_tac x = n in exI, clarify) paulson@15082 373 apply (drule_tac x = na in spec) paulson@15082 374 apply (auto simp add: real_of_nat_Suc) paulson@15082 375 done paulson@15082 376 paulson@15082 377 text{* alternative definition for Bseq *} paulson@15082 378 lemma Bseq_iff: "Bseq X = (\N. \n. \X n\ \ real(Suc N))" paulson@15082 379 apply (simp add: Bseq_def) paulson@15082 380 apply (simp (no_asm) add: lemma_NBseq_def) paulson@15082 381 done paulson@15082 382 paulson@15082 383 lemma lemma_NBseq_def2: paulson@15082 384 "(\K. 0 < K & (\n. \X n\ \ K)) = paulson@15082 385 (\N. \n. \X n\ < real(Suc N))" paulson@15082 386 apply (subst lemma_NBseq_def, auto) paulson@15082 387 apply (rule_tac x = "Suc N" in exI) paulson@15082 388 apply (rule_tac [2] x = N in exI) paulson@15082 389 apply (auto simp add: real_of_nat_Suc) paulson@15082 390 prefer 2 apply (blast intro: order_less_imp_le) paulson@15082 391 apply (drule_tac x = n in spec, simp) paulson@15082 392 done paulson@15082 393 paulson@15082 394 (* yet another definition for Bseq *) paulson@15082 395 lemma Bseq_iff1a: "Bseq X = (\N. \n. \X n\ < real(Suc N))" paulson@15082 396 by (simp add: Bseq_def lemma_NBseq_def2) paulson@15082 397 paulson@15082 398 lemma NSBseqD: "[| NSBseq X; N: HNatInfinite |] ==> ( *fNat* X) N : HFinite" paulson@15082 399 by (simp add: NSBseq_def) paulson@15082 400 paulson@15082 401 lemma NSBseqI: "\N \ HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X" paulson@15082 402 by (simp add: NSBseq_def) paulson@15082 403 paulson@15082 404 text{*The standard definition implies the nonstandard definition*} paulson@15082 405 paulson@15082 406 lemma lemma_Bseq: "\n. \X n\ \ K ==> \n. abs(X((f::nat=>nat) n)) \ K" paulson@15082 407 by auto paulson@15082 408 paulson@15082 409 lemma Bseq_NSBseq: "Bseq X ==> NSBseq X" paulson@15082 410 apply (simp add: Bseq_def NSBseq_def, safe) paulson@15082 411 apply (rule_tac z = N in eq_Abs_hypnat) paulson@15082 412 apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff paulson@15082 413 HNatInfinite_FreeUltrafilterNat_iff) paulson@15082 414 apply (rule bexI [OF _ lemma_hyprel_refl]) paulson@15082 415 apply (drule_tac f = Xa in lemma_Bseq) paulson@15082 416 apply (rule_tac x = "K+1" in exI) paulson@15082 417 apply (drule_tac P="%n. ?f n \ K" in FreeUltrafilterNat_all, ultra) paulson@15082 418 done paulson@15082 419 paulson@15082 420 text{*The nonstandard definition implies the standard definition*} paulson@15082 421 paulson@15082 422 (* similar to NSLIM proof in REALTOPOS *) paulson@15082 423 paulson@15082 424 text{* We need to get rid of the real variable and do so by proving the paulson@15082 425 following, which relies on the Archimedean property of the reals. paulson@15082 426 When we skolemize we then get the required function @{term "f::nat=>nat"}. paulson@15082 427 Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"} paulson@15082 428 which woulid be useless.*} paulson@15082 429 paulson@15082 430 lemma lemmaNSBseq: paulson@15082 431 "\K. 0 < K --> (\n. K < \X n\) paulson@15082 432 ==> \N. \n. real(Suc N) < \X n\" paulson@15082 433 apply safe paulson@15082 434 apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast) paulson@15082 435 done paulson@15082 436 paulson@15082 437 lemma lemmaNSBseq2: "\K. 0 < K --> (\n. K < \X n\) paulson@15082 438 ==> \f. \N. real(Suc N) < \X (f N)\" paulson@15082 439 apply (drule lemmaNSBseq) paulson@15082 440 apply (drule choice, blast) paulson@15082 441 done paulson@15082 442 paulson@15082 443 lemma real_seq_to_hypreal_HInfinite: paulson@15082 444 "\N. real(Suc N) < \X (f N)\ paulson@15082 445 ==> Abs_hypreal(hyprel``{X o f}) : HInfinite" paulson@15082 446 apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def) paulson@15082 447 apply (rule bexI [OF _ lemma_hyprel_refl], clarify) paulson@15082 448 apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real) paulson@15082 449 apply (drule FreeUltrafilterNat_all) paulson@15082 450 apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset]) paulson@15082 451 apply (auto simp add: real_of_nat_Suc) paulson@15082 452 done paulson@15082 453 paulson@15082 454 text{* Now prove that we can get out an infinite hypernatural as well paulson@15082 455 defined using the skolem function @{term "f::nat=>nat"} above*} paulson@15082 456 paulson@15082 457 lemma lemma_finite_NSBseq: paulson@15082 458 "{n. f n \ Suc u & real(Suc n) < \X (f n)\} \ paulson@15082 459 {n. f n \ u & real(Suc n) < \X (f n)\} Un paulson@15082 460 {n. real(Suc n) < \X (Suc u)\}" paulson@15082 461 by (auto dest!: le_imp_less_or_eq) paulson@15082 462 paulson@15082 463 lemma lemma_finite_NSBseq2: paulson@15082 464 "finite {n. f n \ (u::nat) & real(Suc n) < \X(f n)\}" paulson@15082 465 apply (induct_tac "u") paulson@15082 466 apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset]) paulson@15082 467 apply (rule_tac B = "{n. real (Suc n) < \X 0\ }" in finite_subset) paulson@15082 468 apply (auto intro: finite_real_of_nat_less_real paulson@15082 469 simp add: real_of_nat_Suc less_diff_eq [symmetric]) paulson@15082 470 done paulson@15082 471 paulson@15082 472 lemma HNatInfinite_skolem_f: paulson@15082 473 "\N. real(Suc N) < \X (f N)\ paulson@15082 474 ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite" paulson@15082 475 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) paulson@15082 476 apply (rule bexI [OF _ lemma_hypnatrel_refl], safe) paulson@15082 477 apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem) paulson@15082 478 apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) paulson@15082 479 apply (subgoal_tac "{n. f n \ u & real (Suc n) < \X (f n)\} = paulson@15082 480 {n. f n \ u} \ {N. real (Suc N) < \X (f N)\}") paulson@15082 481 apply (erule ssubst) paulson@15082 482 apply (auto simp add: linorder_not_less Compl_def) paulson@15082 483 done paulson@15082 484 paulson@15082 485 lemma NSBseq_Bseq: "NSBseq X ==> Bseq X" paulson@15082 486 apply (simp add: Bseq_def NSBseq_def) paulson@15082 487 apply (rule ccontr) paulson@15082 488 apply (auto simp add: linorder_not_less [symmetric]) paulson@15082 489 apply (drule lemmaNSBseq2, safe) paulson@15082 490 apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite) paulson@15082 491 apply (drule HNatInfinite_skolem_f [THEN [2] bspec]) paulson@15082 492 apply (auto simp add: starfunNat o_def HFinite_HInfinite_iff) paulson@15082 493 done paulson@15082 494 paulson@15082 495 text{* Equivalence of nonstandard and standard definitions paulson@15082 496 for a bounded sequence*} paulson@15082 497 lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)" paulson@15082 498 by (blast intro!: NSBseq_Bseq Bseq_NSBseq) paulson@15082 499 paulson@15082 500 text{*A convergent sequence is bounded: paulson@15082 501 Boundedness as a necessary condition for convergence. paulson@15082 502 The nonstandard version has no existential, as usual *} paulson@15082 503 paulson@15082 504 lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X" paulson@15082 505 apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def) paulson@15082 506 apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite) paulson@15082 507 done paulson@15082 508 paulson@15082 509 text{*Standard Version: easily now proved using equivalence of NS and paulson@15082 510 standard definitions *} paulson@15082 511 lemma convergent_Bseq: "convergent X ==> Bseq X" paulson@15082 512 by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff) paulson@15082 513 paulson@15082 514 paulson@15082 515 subsection{*Upper Bounds and Lubs of Bounded Sequences*} paulson@15082 516 paulson@15082 517 lemma Bseq_isUb: paulson@15082 518 "!!(X::nat=>real). Bseq X ==> \U. isUb (UNIV::real set) {x. \n. X n = x} U" paulson@15082 519 by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff) paulson@15082 520 paulson@15082 521 paulson@15082 522 text{* Use completeness of reals (supremum property) paulson@15082 523 to show that any bounded sequence has a least upper bound*} paulson@15082 524 paulson@15082 525 lemma Bseq_isLub: paulson@15082 526 "!!(X::nat=>real). Bseq X ==> paulson@15082 527 \U. isLub (UNIV::real set) {x. \n. X n = x} U" paulson@15082 528 by (blast intro: reals_complete Bseq_isUb) paulson@15082 529 paulson@15082 530 lemma NSBseq_isUb: "NSBseq X ==> \U. isUb UNIV {x. \n. X n = x} U" paulson@15082 531 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb) paulson@15082 532 paulson@15082 533 lemma NSBseq_isLub: "NSBseq X ==> \U. isLub UNIV {x. \n. X n = x} U" paulson@15082 534 by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub) paulson@15082 535 paulson@15082 536 paulson@15082 537 subsection{*A Bounded and Monotonic Sequence Converges*} paulson@15082 538 paulson@15082 539 lemma lemma_converg1: paulson@15082 540 "!!(X::nat=>real). [| \m n. m \ n --> X m \ X n; paulson@15082 541 isLub (UNIV::real set) {x. \n. X n = x} (X ma) paulson@15082 542 |] ==> \n. ma \ n --> X n = X ma" paulson@15082 543 apply safe paulson@15082 544 apply (drule_tac y = "X n" in isLubD2) paulson@15082 545 apply (blast dest: order_antisym)+ paulson@15082 546 done paulson@15082 547 paulson@15082 548 text{* The best of both worlds: Easier to prove this result as a standard paulson@15082 549 theorem and then use equivalence to "transfer" it into the paulson@15082 550 equivalent nonstandard form if needed!*} paulson@15082 551 paulson@15082 552 lemma Bmonoseq_LIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----> L)" paulson@15082 553 apply (simp add: LIMSEQ_def) paulson@15082 554 apply (rule_tac x = "X m" in exI, safe) paulson@15082 555 apply (rule_tac x = m in exI, safe) paulson@15082 556 apply (drule spec, erule impE, auto) paulson@15082 557 done paulson@15082 558 paulson@15082 559 text{*Now, the same theorem in terms of NS limit *} paulson@15082 560 lemma Bmonoseq_NSLIMSEQ: "\n. m \ n --> X n = X m ==> \L. (X ----NS> L)" paulson@15082 561 by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff) paulson@15082 562 paulson@15082 563 lemma lemma_converg2: paulson@15082 564 "!!(X::nat=>real). paulson@15082 565 [| \m. X m ~= U; isLub UNIV {x. \n. X n = x} U |] ==> \m. X m < U" paulson@15082 566 apply safe paulson@15082 567 apply (drule_tac y = "X m" in isLubD2) paulson@15082 568 apply (auto dest!: order_le_imp_less_or_eq) paulson@15082 569 done paulson@15082 570 paulson@15082 571 lemma lemma_converg3: "!!(X ::nat=>real). \m. X m \ U ==> isUb UNIV {x. \n. X n = x} U" paulson@15082 572 by (rule setleI [THEN isUbI], auto) paulson@15082 573 paulson@15082 574 text{* FIXME: @{term "U - T < U"} is redundant *} paulson@15082 575 lemma lemma_converg4: "!!(X::nat=> real). paulson@15082 576 [| \m. X m ~= U; paulson@15082 577 isLub UNIV {x. \n. X n = x} U; paulson@15082 578 0 < T; paulson@15082 579 U + - T < U paulson@15082 580 |] ==> \m. U + -T < X m & X m < U" paulson@15082 581 apply (drule lemma_converg2, assumption) paulson@15082 582 apply (rule ccontr, simp) paulson@15082 583 apply (simp add: linorder_not_less) paulson@15082 584 apply (drule lemma_converg3) paulson@15082 585 apply (drule isLub_le_isUb, assumption) paulson@15082 586 apply (auto dest: order_less_le_trans) paulson@15082 587 done paulson@15082 588 paulson@15082 589 text{*A standard proof of the theorem for monotone increasing sequence*} paulson@15082 590 paulson@15082 591 lemma Bseq_mono_convergent: paulson@15082 592 "[| Bseq X; \m n. m \ n --> X m \ X n |] ==> convergent X" paulson@15082 593 apply (simp add: convergent_def) paulson@15082 594 apply (frule Bseq_isLub, safe) paulson@15082 595 apply (case_tac "\m. X m = U", auto) paulson@15082 596 apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) paulson@15082 597 (* second case *) paulson@15082 598 apply (rule_tac x = U in exI) paulson@15082 599 apply (subst LIMSEQ_iff, safe) paulson@15082 600 apply (frule lemma_converg2, assumption) paulson@15082 601 apply (drule lemma_converg4, auto) paulson@15082 602 apply (rule_tac x = m in exI, safe) paulson@15082 603 apply (subgoal_tac "X m \ X n") paulson@15082 604 prefer 2 apply blast paulson@15082 605 apply (drule_tac x=n and P="%m. X m < U" in spec, arith) paulson@15082 606 done paulson@15082 607 paulson@15082 608 text{*Nonstandard version of the theorem*} paulson@15082 609 paulson@15082 610 lemma NSBseq_mono_NSconvergent: paulson@15082 611 "[| NSBseq X; \m n. m \ n --> X m \ X n |] ==> NSconvergent X" paulson@15082 612 by (auto intro: Bseq_mono_convergent paulson@15082 613 simp add: convergent_NSconvergent_iff [symmetric] paulson@15082 614 Bseq_NSBseq_iff [symmetric]) paulson@15082 615 paulson@15082 616 lemma convergent_minus_iff: "(convergent X) = (convergent (%n. -(X n)))" paulson@15082 617 apply (simp add: convergent_def) paulson@15082 618 apply (auto dest: LIMSEQ_minus) paulson@15082 619 apply (drule LIMSEQ_minus, auto) paulson@15082 620 done paulson@15082 621 paulson@15082 622 lemma Bseq_minus_iff: "Bseq (%n. -(X n)) = Bseq X" paulson@15082 623 by (simp add: Bseq_def) paulson@15082 624 paulson@15082 625 text{*Main monotonicity theorem*} paulson@15082 626 lemma Bseq_monoseq_convergent: "[| Bseq X; monoseq X |] ==> convergent X" paulson@15082 627 apply (simp add: monoseq_def, safe) paulson@15082 628 apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) paulson@15082 629 apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) paulson@15082 630 apply (auto intro!: Bseq_mono_convergent) paulson@15082 631 done paulson@15082 632 paulson@15082 633 paulson@15082 634 subsection{*A Few More Equivalence Theorems for Boundedness*} paulson@15082 635 paulson@15082 636 text{*alternative formulation for boundedness*} paulson@15082 637 lemma Bseq_iff2: "Bseq X = (\k x. 0 < k & (\n. \X(n) + -x\ \ k))" paulson@15082 638 apply (unfold Bseq_def, safe) paulson@15082 639 apply (rule_tac [2] x = "k + \x\ " in exI) paulson@15082 640 apply (rule_tac x = K in exI) paulson@15221 641 apply (rule exI [where x = 0], auto) paulson@15221 642 apply (drule_tac x=n in spec, arith)+ paulson@15082 643 done paulson@15082 644 paulson@15082 645 text{*alternative formulation for boundedness*} paulson@15082 646 lemma Bseq_iff3: "Bseq X = (\k N. 0 < k & (\n. abs(X(n) + -X(N)) \ k))" paulson@15082 647 apply safe paulson@15082 648 apply (simp add: Bseq_def, safe) paulson@15082 649 apply (rule_tac x = "K + \X N\ " in exI) paulson@15082 650 apply auto paulson@15082 651 apply arith paulson@15082 652 apply (rule_tac x = N in exI, safe) paulson@15082 653 apply (drule_tac x = n in spec, arith) paulson@15082 654 apply (auto simp add: Bseq_iff2) paulson@15082 655 done paulson@15082 656 paulson@15082 657 lemma BseqI2: "(\n. k \ f n & f n \ K) ==> Bseq f" paulson@15082 658 apply (simp add: Bseq_def) paulson@15221 659 apply (rule_tac x = " (\k\ + \K\) + 1" in exI, auto) paulson@15082 660 apply (drule_tac [2] x = n in spec, arith+) paulson@15082 661 done paulson@15082 662 paulson@15082 663 paulson@15082 664 subsection{*Equivalence Between NS and Standard Cauchy Sequences*} paulson@15082 665 paulson@15082 666 subsubsection{*Standard Implies Nonstandard*} paulson@15082 667 paulson@15082 668 lemma lemmaCauchy1: paulson@15082 669 "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite paulson@15082 670 ==> {n. M \ x n} : FreeUltrafilterNat" paulson@15082 671 apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) paulson@15082 672 apply (drule_tac x = M in spec, ultra) paulson@15082 673 done paulson@15082 674 paulson@15082 675 lemma lemmaCauchy2: paulson@15082 676 "{n. \m n. M \ m & M \ (n::nat) --> \X m + - X n\ < u} Int paulson@15082 677 {n. M \ xa n} Int {n. M \ x n} \ paulson@15082 678 {n. abs (X (xa n) + - X (x n)) < u}" paulson@15082 679 by blast paulson@15082 680 paulson@15082 681 lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X" paulson@15082 682 apply (simp add: Cauchy_def NSCauchy_def, safe) paulson@15082 683 apply (rule_tac z = M in eq_Abs_hypnat) paulson@15082 684 apply (rule_tac z = N in eq_Abs_hypnat) paulson@15082 685 apply (rule approx_minus_iff [THEN iffD2]) paulson@15082 686 apply (rule mem_infmal_iff [THEN iffD1]) paulson@15082 687 apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) paulson@15082 688 apply (rule bexI, auto) paulson@15082 689 apply (drule spec, auto) paulson@15082 690 apply (drule_tac M = M in lemmaCauchy1) paulson@15082 691 apply (drule_tac M = M in lemmaCauchy1) paulson@15082 692 apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset]) paulson@15082 693 apply (rule FreeUltrafilterNat_Int) paulson@15082 694 apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set) paulson@15082 695 done paulson@15082 696 paulson@15082 697 subsubsection{*Nonstandard Implies Standard*} paulson@15082 698 paulson@15082 699 lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X" paulson@15082 700 apply (auto simp add: Cauchy_def NSCauchy_def) paulson@15082 701 apply (rule ccontr, simp) paulson@15082 702 apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib) paulson@15082 703 apply (drule bspec, assumption) paulson@15082 704 apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); paulson@15082 705 apply (auto simp add: starfunNat) paulson@15082 706 apply (drule approx_minus_iff [THEN iffD1]) paulson@15082 707 apply (drule mem_infmal_iff [THEN iffD2]) paulson@15082 708 apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) paulson@15082 709 apply (rename_tac "Y") paulson@15082 710 apply (drule_tac x = e in spec, auto) paulson@15082 711 apply (drule FreeUltrafilterNat_Int, assumption) paulson@15082 712 apply (subgoal_tac "{n. \X (f n) + - X (fa n)\ < e} \ \") paulson@15082 713 prefer 2 apply (erule FreeUltrafilterNat_subset, force) paulson@15082 714 apply (rule FreeUltrafilterNat_empty [THEN notE]) paulson@15082 715 apply (subgoal_tac paulson@15082 716 "{n. abs (X (f n) + - X (fa n)) < e} Int paulson@15082 717 {M. ~ abs (X (f M) + - X (fa M)) < e} = {}") paulson@15082 718 apply auto paulson@15082 719 done paulson@15082 720 paulson@15082 721 paulson@15082 722 theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X" paulson@15082 723 by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy) paulson@15082 724 paulson@15082 725 text{*A Cauchy sequence is bounded -- this is the standard paulson@15082 726 proof mechanization rather than the nonstandard proof*} paulson@15082 727 paulson@15082 728 lemma lemmaCauchy: "\n. M \ n --> \X M + - X n\ < (1::real) paulson@15082 729 ==> \n. M \ n --> \X n\ < 1 + \X M\" paulson@15082 730 apply safe paulson@15082 731 apply (drule spec, auto, arith) paulson@15082 732 done paulson@15082 733 paulson@15082 734 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \ M)" paulson@15082 735 by auto paulson@15082 736 paulson@15082 737 text{* FIXME: Long. Maximal element in subsequence *} paulson@15082 738 lemma SUP_rabs_subseq: paulson@15082 739 "\m. m \ M & (\n. n \ M --> \(X::nat=> real) n\ \ \X m\)" paulson@15082 740 apply (induct M) paulson@15082 741 apply (rule_tac x = 0 in exI, simp, safe) nipkow@15236 742 apply (cut_tac x = "\X (Suc M)\" and y = "\X m\ " in linorder_less_linear) paulson@15082 743 apply safe paulson@15082 744 apply (rule_tac x = m in exI) paulson@15082 745 apply (rule_tac [2] x = m in exI) nipkow@15236 746 apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe) nipkow@15236 747 apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE]) paulson@15082 748 apply (simp_all add: less_Suc_cancel_iff) paulson@15082 749 apply (blast intro: order_le_less_trans [THEN order_less_imp_le]) paulson@15082 750 done paulson@15082 751 paulson@15082 752 lemma lemma_Nat_covered: paulson@15082 753 "[| \m::nat. m \ M --> P M m; paulson@15082 754 \m. M \ m --> P M m |] paulson@15082 755 ==> \m. P M m" paulson@15082 756 by (auto elim: less_asym simp add: le_def) paulson@15082 757 paulson@15082 758 paulson@15082 759 lemma lemma_trans1: paulson@15082 760 "[| \n. n \ M --> \(X::nat=>real) n\ \ a; a < b |] paulson@15082 761 ==> \n. n \ M --> \X n\ \ b" paulson@15082 762 by (blast intro: order_le_less_trans [THEN order_less_imp_le]) paulson@15082 763 paulson@15082 764 lemma lemma_trans2: paulson@15082 765 "[| \n. M \ n --> \(X::nat=>real) n\ < a; a < b |] paulson@15082 766 ==> \n. M \ n --> \X n\\ b" paulson@15082 767 by (blast intro: order_less_trans [THEN order_less_imp_le]) paulson@15082 768 paulson@15082 769 lemma lemma_trans3: paulson@15082 770 "[| \n. n \ M --> \X n\ \ a; a = b |] paulson@15082 771 ==> \n. n \ M --> \X n\ \ b" paulson@15082 772 by auto paulson@15082 773 paulson@15082 774 lemma lemma_trans4: "\n. M \ n --> \(X::nat=>real) n\ < a paulson@15082 775 ==> \n. M \ n --> \X n\ \ a" paulson@15082 776 by (blast intro: order_less_imp_le) paulson@15082 777 paulson@15082 778 paulson@15082 779 text{*Proof is more involved than outlines sketched by various authors paulson@15082 780 would suggest*} paulson@15082 781 paulson@15082 782 lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" paulson@15082 783 apply (simp add: Cauchy_def Bseq_def) paulson@15082 784 apply (drule_tac x = 1 in spec) paulson@15082 785 apply (erule zero_less_one [THEN [2] impE], safe) paulson@15082 786 apply (drule_tac x = M in spec, simp) paulson@15082 787 apply (drule lemmaCauchy) paulson@15082 788 apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe) paulson@15082 789 apply (cut_tac x = "\X m\ " and y = "1 + \X M\ " in linorder_less_linear) paulson@15082 790 apply safe paulson@15082 791 apply (drule lemma_trans1, assumption) paulson@15082 792 apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl) paulson@15082 793 apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl) paulson@15082 794 apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans]) paulson@15082 795 apply (drule lemma_trans4) paulson@15082 796 apply (drule_tac [2] lemma_trans4) paulson@15082 797 apply (rule_tac x = "1 + \X M\ " in exI) paulson@15082 798 apply (rule_tac [2] x = "1 + \X M\ " in exI) paulson@15082 799 apply (rule_tac [3] x = "\X m\ " in exI) paulson@15085 800 apply (auto elim!: lemma_Nat_covered) paulson@15082 801 done paulson@15082 802 paulson@15082 803 text{*A Cauchy sequence is bounded -- nonstandard version*} paulson@15082 804 paulson@15082 805 lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X" paulson@15082 806 by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff) paulson@15082 807 paulson@15082 808 paulson@15082 809 text{*Equivalence of Cauchy criterion and convergence: paulson@15082 810 We will prove this using our NS formulation which provides a paulson@15082 811 much easier proof than using the standard definition. We do not paulson@15082 812 need to use properties of subsequences such as boundedness, paulson@15082 813 monotonicity etc... Compare with Harrison's corresponding proof paulson@15082 814 in HOL which is much longer and more complicated. Of course, we do paulson@15082 815 not have problems which he encountered with guessing the right paulson@15082 816 instantiations for his 'espsilon-delta' proof(s) in this case paulson@15082 817 since the NS formulations do not involve existential quantifiers.*} paulson@15082 818 paulson@15082 819 lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X" paulson@15082 820 apply (simp add: NSconvergent_def NSLIMSEQ_def, safe) paulson@15082 821 apply (frule NSCauchy_NSBseq) paulson@15082 822 apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def) paulson@15082 823 apply (drule HNatInfinite_whn [THEN [2] bspec]) paulson@15082 824 apply (drule HNatInfinite_whn [THEN [2] bspec]) paulson@15082 825 apply (auto dest!: st_part_Ex simp add: SReal_iff) paulson@15082 826 apply (blast intro: approx_trans3) paulson@15082 827 done paulson@15082 828 paulson@15082 829 text{*Standard proof for free*} paulson@15082 830 lemma Cauchy_convergent_iff: "Cauchy X = convergent X" paulson@15082 831 by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff) paulson@15082 832 paulson@15082 833 paulson@15082 834 text{*We can now try and derive a few properties of sequences, paulson@15082 835 starting with the limit comparison property for sequences.*} paulson@15082 836 paulson@15082 837 lemma NSLIMSEQ_le: paulson@15082 838 "[| f ----NS> l; g ----NS> m; paulson@15082 839 \N. \n. N \ n --> f(n) \ g(n) paulson@15082 840 |] ==> l \ m" paulson@15082 841 apply (simp add: NSLIMSEQ_def, safe) paulson@15082 842 apply (drule starfun_le_mono) paulson@15082 843 apply (drule HNatInfinite_whn [THEN [2] bspec])+ paulson@15082 844 apply (drule_tac x = whn in spec) paulson@15082 845 apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ paulson@15082 846 apply clarify paulson@15082 847 apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2) paulson@15082 848 done paulson@15082 849 paulson@15082 850 (* standard version *) paulson@15082 851 lemma LIMSEQ_le: paulson@15082 852 "[| f ----> l; g ----> m; \N. \n. N \ n --> f(n) \ g(n) |] paulson@15082 853 ==> l \ m" paulson@15082 854 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le) paulson@15082 855 paulson@15082 856 lemma LIMSEQ_le_const: "[| X ----> r; \n. a \ X n |] ==> a \ r" paulson@15082 857 apply (rule LIMSEQ_le) paulson@15082 858 apply (rule LIMSEQ_const, auto) paulson@15082 859 done paulson@15082 860 paulson@15082 861 lemma NSLIMSEQ_le_const: "[| X ----NS> r; \n. a \ X n |] ==> a \ r" paulson@15082 862 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const) paulson@15082 863 paulson@15082 864 lemma LIMSEQ_le_const2: "[| X ----> r; \n. X n \ a |] ==> r \ a" paulson@15082 865 apply (rule LIMSEQ_le) paulson@15082 866 apply (rule_tac [2] LIMSEQ_const, auto) paulson@15082 867 done paulson@15082 868 paulson@15082 869 lemma NSLIMSEQ_le_const2: "[| X ----NS> r; \n. X n \ a |] ==> r \ a" paulson@15082 870 by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2) paulson@15082 871 paulson@15082 872 text{*Shift a convergent series by 1: paulson@15082 873 By the equivalence between Cauchiness and convergence and because paulson@15082 874 the successor of an infinite hypernatural is also infinite.*} paulson@15082 875 paulson@15082 876 lemma NSLIMSEQ_Suc: "f ----NS> l ==> (%n. f(Suc n)) ----NS> l" paulson@15082 877 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]]) paulson@15082 878 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one) paulson@15082 879 apply (drule bspec, assumption) paulson@15082 880 apply (drule bspec, assumption) paulson@15082 881 apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add]) paulson@15082 882 apply (blast intro: approx_trans3) paulson@15082 883 done paulson@15082 884 paulson@15082 885 text{* standard version *} paulson@15082 886 lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l" paulson@15082 887 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc) paulson@15082 888 paulson@15082 889 lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) ----NS> l ==> f ----NS> l" paulson@15082 890 apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]]) paulson@15082 891 apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one) paulson@15082 892 apply (drule bspec, assumption) paulson@15082 893 apply (drule bspec, assumption) paulson@15082 894 apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff]) paulson@15082 895 apply (drule_tac x="N - 1" in bspec) paulson@15082 896 apply (auto intro: approx_trans3) paulson@15082 897 done paulson@15082 898 paulson@15082 899 lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l" paulson@15082 900 apply (simp add: LIMSEQ_NSLIMSEQ_iff) paulson@15082 901 apply (erule NSLIMSEQ_imp_Suc) paulson@15082 902 done paulson@15082 903 paulson@15082 904 lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)" paulson@15082 905 by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) paulson@15082 906 paulson@15082 907 lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)" paulson@15082 908 by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) paulson@15082 909 paulson@15082 910 text{*A sequence tends to zero iff its abs does*} paulson@15082 911 lemma LIMSEQ_rabs_zero: "((%n. \f n\) ----> 0) = (f ----> 0)" paulson@15082 912 by (simp add: LIMSEQ_def) paulson@15082 913 paulson@15082 914 text{*We prove the NS version from the standard one, since the NS proof paulson@15082 915 seems more complicated than the standard one above!*} paulson@15082 916 lemma NSLIMSEQ_rabs_zero: "((%n. \f n\) ----NS> 0) = (f ----NS> 0)" paulson@15082 917 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero) paulson@15082 918 paulson@15082 919 text{*Generalization to other limits*} paulson@15082 920 lemma NSLIMSEQ_imp_rabs: "f ----NS> l ==> (%n. \f n\) ----NS> \l\" paulson@15082 921 apply (simp add: NSLIMSEQ_def) paulson@15082 922 apply (auto intro: approx_hrabs paulson@15082 923 simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric]) paulson@15082 924 done paulson@15082 925 paulson@15082 926 text{* standard version *} paulson@15082 927 lemma LIMSEQ_imp_rabs: "f ----> l ==> (%n. \f n\) ----> \l\" paulson@15082 928 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs) paulson@15082 929 paulson@15082 930 text{*An unbounded sequence's inverse tends to 0*} paulson@15082 931 paulson@15082 932 text{* standard proof seems easier *} paulson@15082 933 lemma LIMSEQ_inverse_zero: paulson@15082 934 "\y. \N. \n. N \ n --> y < f(n) ==> (%n. inverse(f n)) ----> 0" paulson@15082 935 apply (simp add: LIMSEQ_def, safe) paulson@15082 936 apply (drule_tac x = "inverse r" in spec, safe) paulson@15082 937 apply (rule_tac x = N in exI, safe) paulson@15082 938 apply (drule spec, auto) paulson@15082 939 apply (frule positive_imp_inverse_positive) paulson@15082 940 apply (frule order_less_trans, assumption) paulson@15082 941 apply (frule_tac a = "f n" in positive_imp_inverse_positive) paulson@15082 942 apply (simp add: abs_if) paulson@15082 943 apply (rule_tac t = r in inverse_inverse_eq [THEN subst]) paulson@15082 944 apply (auto intro: inverse_less_iff_less [THEN iffD2] paulson@15082 945 simp del: inverse_inverse_eq) paulson@15082 946 done paulson@15082 947 paulson@15082 948 lemma NSLIMSEQ_inverse_zero: paulson@15082 949 "\y. \N. \n. N \ n --> y < f(n) paulson@15082 950 ==> (%n. inverse(f n)) ----NS> 0" paulson@15082 951 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) paulson@15082 952 paulson@15082 953 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} paulson@15082 954 paulson@15082 955 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0" paulson@15082 956 apply (rule LIMSEQ_inverse_zero, safe) paulson@15082 957 apply (cut_tac x = y in reals_Archimedean2) paulson@15082 958 apply (safe, rule_tac x = n in exI) paulson@15082 959 apply (auto simp add: real_of_nat_Suc) paulson@15082 960 done paulson@15082 961 paulson@15082 962 lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0" paulson@15082 963 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat) paulson@15082 964 paulson@15082 965 text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to paulson@15082 966 infinity is now easily proved*} paulson@15082 967 paulson@15082 968 lemma LIMSEQ_inverse_real_of_nat_add: paulson@15082 969 "(%n. r + inverse(real(Suc n))) ----> r" paulson@15082 970 by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) paulson@15082 971 paulson@15082 972 lemma NSLIMSEQ_inverse_real_of_nat_add: paulson@15082 973 "(%n. r + inverse(real(Suc n))) ----NS> r" paulson@15082 974 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add) paulson@15082 975 paulson@15082 976 lemma LIMSEQ_inverse_real_of_nat_add_minus: paulson@15082 977 "(%n. r + -inverse(real(Suc n))) ----> r" paulson@15082 978 by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) paulson@15082 979 paulson@15082 980 lemma NSLIMSEQ_inverse_real_of_nat_add_minus: paulson@15082 981 "(%n. r + -inverse(real(Suc n))) ----NS> r" paulson@15082 982 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus) paulson@15082 983 paulson@15082 984 lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: paulson@15082 985 "(%n. r*( 1 + -inverse(real(Suc n)))) ----> r" paulson@15082 986 by (cut_tac b=1 in paulson@15082 987 LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) paulson@15082 988 paulson@15082 989 lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: paulson@15082 990 "(%n. r*( 1 + -inverse(real(Suc n)))) ----NS> r" paulson@15082 991 by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult) paulson@15082 992 paulson@15082 993 paulson@15082 994 text{* Real Powers*} paulson@15082 995 paulson@15082 996 lemma NSLIMSEQ_pow [rule_format]: paulson@15082 997 "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)" paulson@15082 998 apply (induct_tac "m") paulson@15082 999 apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const) paulson@15082 1000 done paulson@15082 1001 paulson@15082 1002 lemma LIMSEQ_pow: "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m" paulson@15082 1003 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow) paulson@15082 1004 paulson@15082 1005 text{*The sequence @{term "x^n"} tends to 0 if @{term "0\x"} and @{term paulson@15082 1006 "x<1"}. Proof will use (NS) Cauchy equivalence for convergence and paulson@15082 1007 also fact that bounded and monotonic sequence converges.*} paulson@15082 1008 paulson@15082 1009 lemma Bseq_realpow: "[| 0 \ x; x \ 1 |] ==> Bseq (%n. x ^ n)" paulson@15082 1010 apply (simp add: Bseq_def) paulson@15082 1011 apply (rule_tac x = 1 in exI) paulson@15082 1012 apply (simp add: power_abs) paulson@15082 1013 apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if) paulson@15082 1014 done paulson@15082 1015 paulson@15082 1016 lemma monoseq_realpow: "[| 0 \ x; x \ 1 |] ==> monoseq (%n. x ^ n)" paulson@15082 1017 apply (clarify intro!: mono_SucI2) paulson@15082 1018 apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) paulson@15082 1019 done paulson@15082 1020 paulson@15082 1021 lemma convergent_realpow: "[| 0 \ x; x \ 1 |] ==> convergent (%n. x ^ n)" paulson@15082 1022 by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) paulson@15082 1023 paulson@15082 1024 text{* We now use NS criterion to bring proof of theorem through *} paulson@15082 1025 paulson@15082 1026 lemma NSLIMSEQ_realpow_zero: "[| 0 \ x; x < 1 |] ==> (%n. x ^ n) ----NS> 0" paulson@15082 1027 apply (simp add: NSLIMSEQ_def) paulson@15082 1028 apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff) paulson@15082 1029 apply (frule NSconvergentD) paulson@15082 1030 apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow) paulson@15082 1031 apply (frule HNatInfinite_add_one) paulson@15082 1032 apply (drule bspec, assumption) paulson@15082 1033 apply (drule bspec, assumption) paulson@15082 1034 apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption) paulson@15082 1035 apply (simp add: hyperpow_add) paulson@15082 1036 apply (drule approx_mult_subst_SReal, assumption) paulson@15082 1037 apply (drule approx_trans3, assumption) paulson@15082 1038 apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric]) paulson@15082 1039 done paulson@15082 1040 paulson@15082 1041 text{* standard version *} paulson@15082 1042 lemma LIMSEQ_realpow_zero: "[| 0 \ x; x < 1 |] ==> (%n. x ^ n) ----> 0" paulson@15082 1043 by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff) paulson@15082 1044 paulson@15082 1045 lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) ----> 0" paulson@15082 1046 apply (cut_tac a = a and x1 = "inverse x" in paulson@15082 1047 LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero]) paulson@15082 1048 apply (auto simp add: divide_inverse power_inverse) paulson@15082 1049 apply (simp add: inverse_eq_divide pos_divide_less_eq) paulson@15082 1050 done paulson@15082 1051 paulson@15102 1052 text{*Limit of @{term "c^n"} for @{term"\c\ < 1"}*} paulson@15082 1053 paulson@15082 1054 lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 ==> (%n. \c\ ^ n) ----> 0" paulson@15082 1055 by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero) paulson@15082 1056 paulson@15082 1057 lemma NSLIMSEQ_rabs_realpow_zero: "\c\ < 1 ==> (%n. \c\ ^ n) ----NS> 0" paulson@15082 1058 by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric]) paulson@15082 1059 paulson@15082 1060 lemma LIMSEQ_rabs_realpow_zero2: "\c\ < 1 ==> (%n. c ^ n) ----> 0" paulson@15082 1061 apply (rule LIMSEQ_rabs_zero [THEN iffD1]) paulson@15082 1062 apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) paulson@15082 1063 done paulson@15082 1064 paulson@15082 1065 lemma NSLIMSEQ_rabs_realpow_zero2: "\c\ < 1 ==> (%n. c ^ n) ----NS> 0" paulson@15082 1066 by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric]) paulson@15082 1067 paulson@15082 1068 subsection{*Hyperreals and Sequences*} paulson@15082 1069 paulson@15082 1070 text{*A bounded sequence is a finite hyperreal*} paulson@15082 1071 lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite" paulson@15082 1072 by (auto intro!: bexI lemma_hyprel_refl paulson@15082 1073 intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset] paulson@15082 1074 simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric] paulson@15082 1075 Bseq_iff1a) paulson@15082 1076 paulson@15082 1077 text{*A sequence converging to zero defines an infinitesimal*} paulson@15082 1078 lemma NSLIMSEQ_zero_Infinitesimal_hypreal: paulson@15082 1079 "X ----NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal" paulson@15082 1080 apply (simp add: NSLIMSEQ_def) paulson@15082 1081 apply (drule_tac x = whn in bspec) paulson@15082 1082 apply (simp add: HNatInfinite_whn) paulson@15082 1083 apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat) paulson@15082 1084 done paulson@15082 1085 paulson@15082 1086 (***--------------------------------------------------------------- paulson@15082 1087 Theorems proved by Harrison in HOL that we do not need paulson@15082 1088 in order to prove equivalence between Cauchy criterion paulson@15082 1089 and convergence: paulson@15082 1090 -- Show that every sequence contains a monotonic subsequence paulson@15082 1091 Goal "\f. subseq f & monoseq (%n. s (f n))" paulson@15082 1092 -- Show that a subsequence of a bounded sequence is bounded paulson@15082 1093 Goal "Bseq X ==> Bseq (%n. X (f n))"; paulson@15082 1094 -- Show we can take subsequential terms arbitrarily far paulson@15082 1095 up a sequence paulson@15082 1096 Goal "subseq f ==> n \ f(n)"; paulson@15082 1097 Goal "subseq f ==> \n. N1 \ n & N2 \ f(n)"; paulson@15082 1098 ---------------------------------------------------------------***) paulson@15082 1099 paulson@15082 1100 ML paulson@15082 1101 {* paulson@15082 1102 val Cauchy_def = thm"Cauchy_def"; paulson@15082 1103 val SEQ_Infinitesimal = thm "SEQ_Infinitesimal"; paulson@15082 1104 val LIMSEQ_iff = thm "LIMSEQ_iff"; paulson@15082 1105 val NSLIMSEQ_iff = thm "NSLIMSEQ_iff"; paulson@15082 1106 val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ"; paulson@15082 1107 val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set"; paulson@15082 1108 val Compl_less_set = thm "Compl_less_set"; paulson@15082 1109 val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ"; paulson@15082 1110 val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ"; paulson@15082 1111 val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ"; paulson@15082 1112 val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff"; paulson@15082 1113 val NSLIMSEQ_const = thm "NSLIMSEQ_const"; paulson@15082 1114 val LIMSEQ_const = thm "LIMSEQ_const"; paulson@15082 1115 val NSLIMSEQ_add = thm "NSLIMSEQ_add"; paulson@15082 1116 val LIMSEQ_add = thm "LIMSEQ_add"; paulson@15082 1117 val NSLIMSEQ_mult = thm "NSLIMSEQ_mult"; paulson@15082 1118 val LIMSEQ_mult = thm "LIMSEQ_mult"; paulson@15082 1119 val NSLIMSEQ_minus = thm "NSLIMSEQ_minus"; paulson@15082 1120 val LIMSEQ_minus = thm "LIMSEQ_minus"; paulson@15082 1121 val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel"; paulson@15082 1122 val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel"; paulson@15082 1123 val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus"; paulson@15082 1124 val LIMSEQ_add_minus = thm "LIMSEQ_add_minus"; paulson@15082 1125 val LIMSEQ_diff = thm "LIMSEQ_diff"; paulson@15082 1126 val NSLIMSEQ_diff = thm "NSLIMSEQ_diff"; paulson@15082 1127 val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse"; paulson@15082 1128 val LIMSEQ_inverse = thm "LIMSEQ_inverse"; paulson@15082 1129 val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse"; paulson@15082 1130 val LIMSEQ_divide = thm "LIMSEQ_divide"; paulson@15082 1131 val NSLIMSEQ_unique = thm "NSLIMSEQ_unique"; paulson@15082 1132 val LIMSEQ_unique = thm "LIMSEQ_unique"; paulson@15082 1133 val limI = thm "limI"; paulson@15082 1134 val nslimI = thm "nslimI"; paulson@15082 1135 val lim_nslim_iff = thm "lim_nslim_iff"; paulson@15082 1136 val convergentD = thm "convergentD"; paulson@15082 1137 val convergentI = thm "convergentI"; paulson@15082 1138 val NSconvergentD = thm "NSconvergentD"; paulson@15082 1139 val NSconvergentI = thm "NSconvergentI"; paulson@15082 1140 val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff"; paulson@15082 1141 val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff"; paulson@15082 1142 val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff"; paulson@15082 1143 val subseq_Suc_iff = thm "subseq_Suc_iff"; paulson@15082 1144 val monoseq_Suc = thm "monoseq_Suc"; paulson@15082 1145 val monoI1 = thm "monoI1"; paulson@15082 1146 val monoI2 = thm "monoI2"; paulson@15082 1147 val mono_SucI1 = thm "mono_SucI1"; paulson@15082 1148 val mono_SucI2 = thm "mono_SucI2"; paulson@15082 1149 val BseqD = thm "BseqD"; paulson@15082 1150 val BseqI = thm "BseqI"; paulson@15082 1151 val Bseq_iff = thm "Bseq_iff"; paulson@15082 1152 val Bseq_iff1a = thm "Bseq_iff1a"; paulson@15082 1153 val NSBseqD = thm "NSBseqD"; paulson@15082 1154 val NSBseqI = thm "NSBseqI"; paulson@15082 1155 val Bseq_NSBseq = thm "Bseq_NSBseq"; paulson@15082 1156 val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite"; paulson@15082 1157 val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f"; paulson@15082 1158 val NSBseq_Bseq = thm "NSBseq_Bseq"; paulson@15082 1159 val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff"; paulson@15082 1160 val NSconvergent_NSBseq = thm "NSconvergent_NSBseq"; paulson@15082 1161 val convergent_Bseq = thm "convergent_Bseq"; paulson@15082 1162 val Bseq_isUb = thm "Bseq_isUb"; paulson@15082 1163 val Bseq_isLub = thm "Bseq_isLub"; paulson@15082 1164 val NSBseq_isUb = thm "NSBseq_isUb"; paulson@15082 1165 val NSBseq_isLub = thm "NSBseq_isLub"; paulson@15082 1166 val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ"; paulson@15082 1167 val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ"; paulson@15082 1168 val Bseq_mono_convergent = thm "Bseq_mono_convergent"; paulson@15082 1169 val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent"; paulson@15082 1170 val convergent_minus_iff = thm "convergent_minus_iff"; paulson@15082 1171 val Bseq_minus_iff = thm "Bseq_minus_iff"; paulson@15082 1172 val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent"; paulson@15082 1173 val Bseq_iff2 = thm "Bseq_iff2"; paulson@15082 1174 val Bseq_iff3 = thm "Bseq_iff3"; paulson@15082 1175 val BseqI2 = thm "BseqI2"; paulson@15082 1176 val Cauchy_NSCauchy = thm "Cauchy_NSCauchy"; paulson@15082 1177 val NSCauchy_Cauchy = thm "NSCauchy_Cauchy"; paulson@15082 1178 val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff"; paulson@15082 1179 val less_Suc_cancel_iff = thm "less_Suc_cancel_iff"; paulson@15082 1180 val SUP_rabs_subseq = thm "SUP_rabs_subseq"; paulson@15082 1181 val Cauchy_Bseq = thm "Cauchy_Bseq"; paulson@15082 1182 val NSCauchy_NSBseq = thm "NSCauchy_NSBseq"; paulson@15082 1183 val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff"; paulson@15082 1184 val Cauchy_convergent_iff = thm "Cauchy_convergent_iff"; paulson@15082 1185 val NSLIMSEQ_le = thm "NSLIMSEQ_le"; paulson@15082 1186 val LIMSEQ_le = thm "LIMSEQ_le"; paulson@15082 1187 val LIMSEQ_le_const = thm "LIMSEQ_le_const"; paulson@15082 1188 val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const"; paulson@15082 1189 val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2"; paulson@15082 1190 val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2"; paulson@15082 1191 val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc"; paulson@15082 1192 val LIMSEQ_Suc = thm "LIMSEQ_Suc"; paulson@15082 1193 val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc"; paulson@15082 1194 val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc"; paulson@15082 1195 val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff"; paulson@15082 1196 val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff"; paulson@15082 1197 val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero"; paulson@15082 1198 val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero"; paulson@15082 1199 val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs"; paulson@15082 1200 val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs"; paulson@15082 1201 val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero"; paulson@15082 1202 val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero"; paulson@15082 1203 val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat"; paulson@15082 1204 val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat"; paulson@15082 1205 val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add"; paulson@15082 1206 val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add"; paulson@15082 1207 val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus"; paulson@15082 1208 val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus"; paulson@15082 1209 val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult"; paulson@15082 1210 val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult"; paulson@15082 1211 val NSLIMSEQ_pow = thm "NSLIMSEQ_pow"; paulson@15082 1212 val LIMSEQ_pow = thm "LIMSEQ_pow"; paulson@15082 1213 val Bseq_realpow = thm "Bseq_realpow"; paulson@15082 1214 val monoseq_realpow = thm "monoseq_realpow"; paulson@15082 1215 val convergent_realpow = thm "convergent_realpow"; paulson@15082 1216 val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero"; paulson@15082 1217 val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero"; paulson@15082 1218 val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero"; paulson@15082 1219 val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero"; paulson@15082 1220 val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero"; paulson@15082 1221 val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2"; paulson@15082 1222 val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2"; paulson@15082 1223 val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal"; paulson@15082 1224 val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal"; paulson@15082 1225 *} paulson@15082 1226 paulson@10751 1227 end paulson@10751 1228