author  paulson 
Thu, 29 Jul 2004 16:14:42 +0200  
changeset 15085  5693a977a767 
parent 15082  6c3276a2735b 
child 15102  04b0e943fcc9 
permissions  rwrr 
10751  1 
(* Title : SEQ.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 1998 University of Cambridge 

4 
Description : Convergence of sequences and series 

15082  5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
6 
*) 

10751  7 

15082  8 
theory SEQ = NatStar + HyperPow: 
10751  9 

10 
constdefs 

11 

15082  12 
LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ > (_))" [60, 60] 60) 
13 
{*Standard definition of convergence of sequence*} 

14 
"X > L == (\<forall>r. 0 < r > (\<exists>no. \<forall>n. no \<le> n > \<bar>X n + L\<bar> < r))" 

10751  15 

15082  16 
NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ NS> (_))" [60, 60] 60) 
17 
{*Nonstandard definition of convergence of sequence*} 

18 
"X NS> L == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)" 

19 

20 
lim :: "(nat => real) => real" 

21 
{*Standard definition of limit using choice operator*} 

10751  22 
"lim X == (@L. (X > L))" 
23 

15082  24 
nslim :: "(nat => real) => real" 
25 
{*Nonstandard definition of limit using choice operator*} 

10751  26 
"nslim X == (@L. (X NS> L))" 
27 

15082  28 
convergent :: "(nat => real) => bool" 
29 
{*Standard definition of convergence*} 

30 
"convergent X == (\<exists>L. (X > L))" 

10751  31 

15082  32 
NSconvergent :: "(nat => real) => bool" 
33 
{*Nonstandard definition of convergence*} 

34 
"NSconvergent X == (\<exists>L. (X NS> L))" 

35 

36 
Bseq :: "(nat => real) => bool" 

37 
{*Standard definition for bounded sequence*} 

38 
"Bseq X == (\<exists>K. (0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)))" 

10751  39 

15082  40 
NSBseq :: "(nat=>real) => bool" 
41 
{*Nonstandard definition for bounded sequence*} 

42 
"NSBseq X == (\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite)" 

43 

44 
monoseq :: "(nat=>real)=>bool" 

45 
{*Definition for monotonicity*} 

46 
"monoseq X == ((\<forall>(m::nat) n. m \<le> n > X m \<le> X n)  

47 
(\<forall>m n. m \<le> n > X n \<le> X m))" 

10751  48 

15082  49 
subseq :: "(nat => nat) => bool" 
50 
{*Definition of subsequence*} 

51 
"subseq f == (\<forall>m n. m < n > (f m) < (f n))" 

10751  52 

15082  53 
Cauchy :: "(nat => real) => bool" 
54 
{*Standard definition of the Cauchy condition*} 

55 
"Cauchy X == (\<forall>e. (0 < e > 

56 
(\<exists>M. (\<forall>m n. M \<le> m & M \<le> n 

10751  57 
> abs((X m) + (X n)) < e))))" 
58 

15082  59 
NSCauchy :: "(nat => real) => bool" 
60 
{*Nonstandard definition*} 

61 
"NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. 

62 
( *fNat* X) M \<approx> ( *fNat* X) N)" 

63 

64 

65 

66 
text{* Example of an hypersequence (i.e. an extended standard sequence) 

67 
whose term with an hypernatural suffix is an infinitesimal i.e. 

68 
the whn'nth term of the hypersequence is a member of Infinitesimal*} 

69 

70 
lemma SEQ_Infinitesimal: 

71 
"( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal" 

72 
apply (simp add: hypnat_omega_def Infinitesimal_FreeUltrafilterNat_iff starfunNat) 

73 
apply (rule bexI, rule_tac [2] lemma_hyprel_refl) 

74 
apply (simp add: real_of_nat_Suc_gt_zero abs_eqI2 FreeUltrafilterNat_inverse_real_of_posnat) 

75 
done 

76 

77 

78 
subsection{*LIMSEQ and NSLIMSEQ*} 

79 

80 
lemma LIMSEQ_iff: 

81 
"(X > L) = 

82 
(\<forall>r. 0 <r > (\<exists>no. \<forall>n. no \<le> n > \<bar>X n + L\<bar> < r))" 

83 
by (simp add: LIMSEQ_def) 

84 

85 
lemma NSLIMSEQ_iff: 

86 
"(X NS> L) = (\<forall>N \<in> HNatInfinite. ( *fNat* X) N \<approx> hypreal_of_real L)" 

87 
by (simp add: NSLIMSEQ_def) 

88 

89 

90 
text{*LIMSEQ ==> NSLIMSEQ*} 

91 

92 
lemma LIMSEQ_NSLIMSEQ: 

93 
"X > L ==> X NS> L" 

94 
apply (simp add: LIMSEQ_def NSLIMSEQ_def) 

95 
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) 

96 
apply (rule_tac z = N in eq_Abs_hypnat) 

97 
apply (rule approx_minus_iff [THEN iffD2]) 

98 
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def 

99 
hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) 

100 
apply (rule bexI [OF _ lemma_hyprel_refl], safe) 

101 
apply (drule_tac x = u in spec, safe) 

102 
apply (drule_tac x = no in spec, fuf) 

103 
apply (blast dest: less_imp_le) 

104 
done 

105 

106 

107 
text{*NSLIMSEQ ==> LIMSEQ*} 

108 

109 
lemma lemma_NSLIMSEQ1: "!!(f::nat=>nat). \<forall>n. n \<le> f n 

110 
==> {n. f n = 0} = {0}  {n. f n = 0} = {}" 

111 
apply auto 

112 
apply (drule_tac x = xa in spec) 

113 
apply (drule_tac [2] x = x in spec, auto) 

114 
done 

115 

116 
lemma lemma_NSLIMSEQ2: "{n. f n \<le> Suc u} = {n. f n \<le> u} Un {n. f n = Suc u}" 

117 
by (auto simp add: le_Suc_eq) 

118 

119 
lemma lemma_NSLIMSEQ3: 

120 
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. f n = Suc u} \<le> {n. n \<le> Suc u}" 

121 
apply auto 

122 
apply (drule_tac x = x in spec, auto) 

123 
done 

124 

125 
text{* the following sequence @{term "f(n)"} defines a hypernatural *} 

126 
lemma NSLIMSEQ_finite_set: 

127 
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}" 

128 
apply (induct u) 

129 
apply (auto simp add: lemma_NSLIMSEQ2) 

130 
apply (auto intro: lemma_NSLIMSEQ3 [THEN finite_subset] finite_atMost [unfolded atMost_def]) 

131 
apply (drule lemma_NSLIMSEQ1, safe) 

132 
apply (simp_all (no_asm_simp)) 

133 
done 

134 

135 
lemma Compl_less_set: " {n. u < (f::nat=>nat) n} = {n. f n \<le> u}" 

136 
by (auto dest: less_le_trans simp add: le_def) 

137 

138 
text{* the index set is in the free ultrafilter *} 

139 
lemma FreeUltrafilterNat_NSLIMSEQ: 

140 
"!!(f::nat=>nat). \<forall>n. n \<le> f n ==> {n. u < f n} : FreeUltrafilterNat" 

141 
apply (rule FreeUltrafilterNat_Compl_iff2 [THEN iffD2]) 

142 
apply (rule FreeUltrafilterNat_finite) 

143 
apply (auto dest: NSLIMSEQ_finite_set simp add: Compl_less_set) 

144 
done 

145 

146 
text{* thus, the sequence defines an infinite hypernatural! *} 

147 
lemma HNatInfinite_NSLIMSEQ: "\<forall>n. n \<le> f n 

148 
==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite" 

149 
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) 

150 
apply (rule bexI [OF _ lemma_hypnatrel_refl], safe) 

151 
apply (erule FreeUltrafilterNat_NSLIMSEQ) 

152 
done 

153 

154 
lemma lemmaLIM: 

155 
"{n. X (f n) +  L = Y n} Int {n. \<bar>Y n\<bar> < r} \<le> 

156 
{n. \<bar>X (f n) +  L\<bar> < r}" 

157 
by auto 

158 

159 
lemma lemmaLIM2: 

160 
"{n. \<bar>X (f n) +  L\<bar> < r} Int {n. r \<le> abs (X (f n) +  (L::real))} = {}" 

161 
by auto 

162 

163 
lemma lemmaLIM3: "[ 0 < r; \<forall>n. r \<le> \<bar>X (f n) +  L\<bar>; 

164 
( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + 

165 
 hypreal_of_real L \<approx> 0 ] ==> False" 

166 
apply (auto simp add: starfunNat mem_infmal_iff [symmetric] hypreal_of_real_def hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) 

167 
apply (rename_tac "Y") 

168 
apply (drule_tac x = r in spec, safe) 

169 
apply (drule FreeUltrafilterNat_Int, assumption) 

170 
apply (drule lemmaLIM [THEN [2] FreeUltrafilterNat_subset]) 

171 
apply (drule FreeUltrafilterNat_all) 

172 
apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl) 

173 
apply (drule FreeUltrafilterNat_Int, assumption) 

174 
apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty) 

175 
done 

176 

177 
lemma NSLIMSEQ_LIMSEQ: "X NS> L ==> X > L" 

178 
apply (simp add: LIMSEQ_def NSLIMSEQ_def) 

179 
apply (rule ccontr, simp, safe) 

180 
txt{* skolemization step *} 

181 
apply (drule choice, safe) 

182 
apply (drule_tac x = "Abs_hypnat (hypnatrel``{f}) " in bspec) 

183 
apply (drule_tac [2] approx_minus_iff [THEN iffD1]) 

184 
apply (simp_all add: linorder_not_less) 

185 
apply (blast intro: HNatInfinite_NSLIMSEQ) 

186 
apply (blast intro: lemmaLIM3) 

187 
done 

188 

189 
text{* Now, the allimportant result is trivially proved! *} 

190 
theorem LIMSEQ_NSLIMSEQ_iff: "(f > L) = (f NS> L)" 

191 
by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ) 

192 

193 

194 
subsection{*Theorems About Sequences*} 

195 

196 
lemma NSLIMSEQ_const: "(%n. k) NS> k" 

197 
by (simp add: NSLIMSEQ_def) 

198 

199 
lemma LIMSEQ_const: "(%n. k) > k" 

200 
by (simp add: LIMSEQ_def) 

201 

202 
lemma NSLIMSEQ_add: 

203 
"[ X NS> a; Y NS> b ] ==> (%n. X n + Y n) NS> a + b" 

204 
by (auto intro: approx_add simp add: NSLIMSEQ_def starfunNat_add [symmetric]) 

205 

206 
lemma LIMSEQ_add: "[ X > a; Y > b ] ==> (%n. X n + Y n) > a + b" 

207 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add) 

208 

209 
lemma NSLIMSEQ_mult: 

210 
"[ X NS> a; Y NS> b ] ==> (%n. X n * Y n) NS> a * b" 

211 
by (auto intro!: approx_mult_HFinite 

212 
simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric]) 

213 

214 
lemma LIMSEQ_mult: "[ X > a; Y > b ] ==> (%n. X n * Y n) > a * b" 

215 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult) 

216 

217 
lemma NSLIMSEQ_minus: "X NS> a ==> (%n. (X n)) NS> a" 

218 
by (auto simp add: NSLIMSEQ_def starfunNat_minus [symmetric]) 

219 

220 
lemma LIMSEQ_minus: "X > a ==> (%n. (X n)) > a" 

221 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_minus) 

222 

223 
lemma LIMSEQ_minus_cancel: "(%n. (X n)) > a ==> X > a" 

224 
by (drule LIMSEQ_minus, simp) 

225 

226 
lemma NSLIMSEQ_minus_cancel: "(%n. (X n)) NS> a ==> X NS> a" 

227 
by (drule NSLIMSEQ_minus, simp) 

228 

229 
lemma NSLIMSEQ_add_minus: 

230 
"[ X NS> a; Y NS> b ] ==> (%n. X n + Y n) NS> a + b" 

231 
by (simp add: NSLIMSEQ_add NSLIMSEQ_minus [of Y]) 

232 

233 
lemma LIMSEQ_add_minus: 

234 
"[ X > a; Y > b ] ==> (%n. X n + Y n) > a + b" 

235 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_add_minus) 

236 

237 
lemma LIMSEQ_diff: "[ X > a; Y > b ] ==> (%n. X n  Y n) > a  b" 

238 
apply (simp add: diff_minus) 

239 
apply (blast intro: LIMSEQ_add_minus) 

240 
done 

241 

242 
lemma NSLIMSEQ_diff: 

243 
"[ X NS> a; Y NS> b ] ==> (%n. X n  Y n) NS> a  b" 

244 
apply (simp add: diff_minus) 

245 
apply (blast intro: NSLIMSEQ_add_minus) 

246 
done 

247 

248 
text{*Proof is like that of @{text NSLIM_inverse}.*} 

249 
lemma NSLIMSEQ_inverse: 

250 
"[ X NS> a; a ~= 0 ] ==> (%n. inverse(X n)) NS> inverse(a)" 

251 
by (simp add: NSLIMSEQ_def starfunNat_inverse [symmetric] 

252 
hypreal_of_real_approx_inverse) 

253 

254 

255 
text{*Standard version of theorem*} 

256 
lemma LIMSEQ_inverse: 

257 
"[ X > a; a ~= 0 ] ==> (%n. inverse(X n)) > inverse(a)" 

258 
by (simp add: NSLIMSEQ_inverse LIMSEQ_NSLIMSEQ_iff) 

259 

260 
lemma NSLIMSEQ_mult_inverse: 

261 
"[ X NS> a; Y NS> b; b ~= 0 ] ==> (%n. X n / Y n) NS> a/b" 

262 
by (simp add: NSLIMSEQ_mult NSLIMSEQ_inverse divide_inverse) 

263 

264 
lemma LIMSEQ_divide: 

265 
"[ X > a; Y > b; b ~= 0 ] ==> (%n. X n / Y n) > a/b" 

266 
by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse) 

267 

268 
text{*Uniqueness of limit*} 

269 
lemma NSLIMSEQ_unique: "[ X NS> a; X NS> b ] ==> a = b" 

270 
apply (simp add: NSLIMSEQ_def) 

271 
apply (drule HNatInfinite_whn [THEN [2] bspec])+ 

272 
apply (auto dest: approx_trans3) 

273 
done 

274 

275 
lemma LIMSEQ_unique: "[ X > a; X > b ] ==> a = b" 

276 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_unique) 

277 

278 

279 
subsection{*Nslim and Lim*} 

280 

281 
lemma limI: "X > L ==> lim X = L" 

282 
apply (simp add: lim_def) 

283 
apply (blast intro: LIMSEQ_unique) 

284 
done 

285 

286 
lemma nslimI: "X NS> L ==> nslim X = L" 

287 
apply (simp add: nslim_def) 

288 
apply (blast intro: NSLIMSEQ_unique) 

289 
done 

290 

291 
lemma lim_nslim_iff: "lim X = nslim X" 

292 
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff) 

293 

294 

295 
subsection{*Convergence*} 

296 

297 
lemma convergentD: "convergent X ==> \<exists>L. (X > L)" 

298 
by (simp add: convergent_def) 

299 

300 
lemma convergentI: "(X > L) ==> convergent X" 

301 
by (auto simp add: convergent_def) 

302 

303 
lemma NSconvergentD: "NSconvergent X ==> \<exists>L. (X NS> L)" 

304 
by (simp add: NSconvergent_def) 

305 

306 
lemma NSconvergentI: "(X NS> L) ==> NSconvergent X" 

307 
by (auto simp add: NSconvergent_def) 

308 

309 
lemma convergent_NSconvergent_iff: "convergent X = NSconvergent X" 

310 
by (simp add: convergent_def NSconvergent_def LIMSEQ_NSLIMSEQ_iff) 

311 

312 
lemma NSconvergent_NSLIMSEQ_iff: "NSconvergent X = (X NS> nslim X)" 

313 
by (auto intro: someI simp add: NSconvergent_def nslim_def) 

314 

315 
lemma convergent_LIMSEQ_iff: "convergent X = (X > lim X)" 

316 
by (auto intro: someI simp add: convergent_def lim_def) 

317 

318 
text{*Subsequence (alternative definition, (e.g. Hoskins)*} 

319 

320 
lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))" 

321 
apply (simp add: subseq_def) 

322 
apply (auto dest!: less_imp_Suc_add) 

323 
apply (induct_tac k) 

324 
apply (auto intro: less_trans) 

325 
done 

326 

327 

328 
subsection{*Monotonicity*} 

329 

330 
lemma monoseq_Suc: 

331 
"monoseq X = ((\<forall>n. X n \<le> X (Suc n)) 

332 
 (\<forall>n. X (Suc n) \<le> X n))" 

333 
apply (simp add: monoseq_def) 

334 
apply (auto dest!: le_imp_less_or_eq) 

335 
apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add) 

336 
apply (induct_tac "ka") 

337 
apply (auto intro: order_trans) 

338 
apply (erule swap) 

339 
apply (induct_tac "k") 

340 
apply (auto intro: order_trans) 

341 
done 

342 

343 
lemma monoI1: "\<forall>m n. m \<le> n > X m \<le> X n ==> monoseq X" 

344 
by (simp add: monoseq_def) 

345 

346 
lemma monoI2: "\<forall>m n. m \<le> n > X n \<le> X m ==> monoseq X" 

347 
by (simp add: monoseq_def) 

348 

349 
lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X" 

350 
by (simp add: monoseq_Suc) 

351 

352 
lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X" 

353 
by (simp add: monoseq_Suc) 

354 

355 

356 
subsection{*Bounded Sequence*} 

357 

358 
lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)" 

359 
by (simp add: Bseq_def) 

360 

361 
lemma BseqI: "[ 0 < K; \<forall>n. \<bar>X n\<bar> \<le> K ] ==> Bseq X" 

362 
by (auto simp add: Bseq_def) 

363 

364 
lemma lemma_NBseq_def: 

365 
"(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) = 

366 
(\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))" 

367 
apply auto 

368 
prefer 2 apply force 

369 
apply (cut_tac x = K in reals_Archimedean2, clarify) 

370 
apply (rule_tac x = n in exI, clarify) 

371 
apply (drule_tac x = na in spec) 

372 
apply (auto simp add: real_of_nat_Suc) 

373 
done 

374 

375 
text{* alternative definition for Bseq *} 

376 
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> \<le> real(Suc N))" 

377 
apply (simp add: Bseq_def) 

378 
apply (simp (no_asm) add: lemma_NBseq_def) 

379 
done 

380 

381 
lemma lemma_NBseq_def2: 

382 
"(\<exists>K. 0 < K & (\<forall>n. \<bar>X n\<bar> \<le> K)) = 

383 
(\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))" 

384 
apply (subst lemma_NBseq_def, auto) 

385 
apply (rule_tac x = "Suc N" in exI) 

386 
apply (rule_tac [2] x = N in exI) 

387 
apply (auto simp add: real_of_nat_Suc) 

388 
prefer 2 apply (blast intro: order_less_imp_le) 

389 
apply (drule_tac x = n in spec, simp) 

390 
done 

391 

392 
(* yet another definition for Bseq *) 

393 
lemma Bseq_iff1a: "Bseq X = (\<exists>N. \<forall>n. \<bar>X n\<bar> < real(Suc N))" 

394 
by (simp add: Bseq_def lemma_NBseq_def2) 

395 

396 
lemma NSBseqD: "[ NSBseq X; N: HNatInfinite ] ==> ( *fNat* X) N : HFinite" 

397 
by (simp add: NSBseq_def) 

398 

399 
lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X" 

400 
by (simp add: NSBseq_def) 

401 

402 
text{*The standard definition implies the nonstandard definition*} 

403 

404 
lemma lemma_Bseq: "\<forall>n. \<bar>X n\<bar> \<le> K ==> \<forall>n. abs(X((f::nat=>nat) n)) \<le> K" 

405 
by auto 

406 

407 
lemma Bseq_NSBseq: "Bseq X ==> NSBseq X" 

408 
apply (simp add: Bseq_def NSBseq_def, safe) 

409 
apply (rule_tac z = N in eq_Abs_hypnat) 

410 
apply (auto simp add: starfunNat HFinite_FreeUltrafilterNat_iff 

411 
HNatInfinite_FreeUltrafilterNat_iff) 

412 
apply (rule bexI [OF _ lemma_hyprel_refl]) 

413 
apply (drule_tac f = Xa in lemma_Bseq) 

414 
apply (rule_tac x = "K+1" in exI) 

415 
apply (drule_tac P="%n. ?f n \<le> K" in FreeUltrafilterNat_all, ultra) 

416 
done 

417 

418 
text{*The nonstandard definition implies the standard definition*} 

419 

420 
(* similar to NSLIM proof in REALTOPOS *) 

421 

422 
text{* We need to get rid of the real variable and do so by proving the 

423 
following, which relies on the Archimedean property of the reals. 

424 
When we skolemize we then get the required function @{term "f::nat=>nat"}. 

425 
Otherwise, we would be stuck with a skolem function @{term "f::real=>nat"} 

426 
which woulid be useless.*} 

427 

428 
lemma lemmaNSBseq: 

429 
"\<forall>K. 0 < K > (\<exists>n. K < \<bar>X n\<bar>) 

430 
==> \<forall>N. \<exists>n. real(Suc N) < \<bar>X n\<bar>" 

431 
apply safe 

432 
apply (cut_tac n = N in real_of_nat_Suc_gt_zero, blast) 

433 
done 

434 

435 
lemma lemmaNSBseq2: "\<forall>K. 0 < K > (\<exists>n. K < \<bar>X n\<bar>) 

436 
==> \<exists>f. \<forall>N. real(Suc N) < \<bar>X (f N)\<bar>" 

437 
apply (drule lemmaNSBseq) 

438 
apply (drule choice, blast) 

439 
done 

440 

441 
lemma real_seq_to_hypreal_HInfinite: 

442 
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar> 

443 
==> Abs_hypreal(hyprel``{X o f}) : HInfinite" 

444 
apply (auto simp add: HInfinite_FreeUltrafilterNat_iff o_def) 

445 
apply (rule bexI [OF _ lemma_hyprel_refl], clarify) 

446 
apply (cut_tac u = u in FreeUltrafilterNat_nat_gt_real) 

447 
apply (drule FreeUltrafilterNat_all) 

448 
apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset]) 

449 
apply (auto simp add: real_of_nat_Suc) 

450 
done 

451 

452 
text{* Now prove that we can get out an infinite hypernatural as well 

453 
defined using the skolem function @{term "f::nat=>nat"} above*} 

454 

455 
lemma lemma_finite_NSBseq: 

456 
"{n. f n \<le> Suc u & real(Suc n) < \<bar>X (f n)\<bar>} \<le> 

457 
{n. f n \<le> u & real(Suc n) < \<bar>X (f n)\<bar>} Un 

458 
{n. real(Suc n) < \<bar>X (Suc u)\<bar>}" 

459 
by (auto dest!: le_imp_less_or_eq) 

460 

461 
lemma lemma_finite_NSBseq2: 

462 
"finite {n. f n \<le> (u::nat) & real(Suc n) < \<bar>X(f n)\<bar>}" 

463 
apply (induct_tac "u") 

464 
apply (rule_tac [2] lemma_finite_NSBseq [THEN finite_subset]) 

465 
apply (rule_tac B = "{n. real (Suc n) < \<bar>X 0\<bar> }" in finite_subset) 

466 
apply (auto intro: finite_real_of_nat_less_real 

467 
simp add: real_of_nat_Suc less_diff_eq [symmetric]) 

468 
done 

469 

470 
lemma HNatInfinite_skolem_f: 

471 
"\<forall>N. real(Suc N) < \<bar>X (f N)\<bar> 

472 
==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite" 

473 
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) 

474 
apply (rule bexI [OF _ lemma_hypnatrel_refl], safe) 

475 
apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem) 

476 
apply (rule lemma_finite_NSBseq2 [THEN FreeUltrafilterNat_finite, THEN notE]) 

477 
apply (subgoal_tac "{n. f n \<le> u & real (Suc n) < \<bar>X (f n)\<bar>} = 

478 
{n. f n \<le> u} \<inter> {N. real (Suc N) < \<bar>X (f N)\<bar>}") 

479 
apply (erule ssubst) 

480 
apply (auto simp add: linorder_not_less Compl_def) 

481 
done 

482 

483 
lemma NSBseq_Bseq: "NSBseq X ==> Bseq X" 

484 
apply (simp add: Bseq_def NSBseq_def) 

485 
apply (rule ccontr) 

486 
apply (auto simp add: linorder_not_less [symmetric]) 

487 
apply (drule lemmaNSBseq2, safe) 

488 
apply (frule_tac X = X and f = f in real_seq_to_hypreal_HInfinite) 

489 
apply (drule HNatInfinite_skolem_f [THEN [2] bspec]) 

490 
apply (auto simp add: starfunNat o_def HFinite_HInfinite_iff) 

491 
done 

492 

493 
text{* Equivalence of nonstandard and standard definitions 

494 
for a bounded sequence*} 

495 
lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)" 

496 
by (blast intro!: NSBseq_Bseq Bseq_NSBseq) 

497 

498 
text{*A convergent sequence is bounded: 

499 
Boundedness as a necessary condition for convergence. 

500 
The nonstandard version has no existential, as usual *} 

501 

502 
lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X" 

503 
apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def) 

504 
apply (blast intro: HFinite_hypreal_of_real approx_sym approx_HFinite) 

505 
done 

506 

507 
text{*Standard Version: easily now proved using equivalence of NS and 

508 
standard definitions *} 

509 
lemma convergent_Bseq: "convergent X ==> Bseq X" 

510 
by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff) 

511 

512 

513 
subsection{*Upper Bounds and Lubs of Bounded Sequences*} 

514 

515 
lemma Bseq_isUb: 

516 
"!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U" 

517 
by (auto intro: isUbI setleI simp add: Bseq_def abs_le_interval_iff) 

518 

519 

520 
text{* Use completeness of reals (supremum property) 

521 
to show that any bounded sequence has a least upper bound*} 

522 

523 
lemma Bseq_isLub: 

524 
"!!(X::nat=>real). Bseq X ==> 

525 
\<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U" 

526 
by (blast intro: reals_complete Bseq_isUb) 

527 

528 
lemma NSBseq_isUb: "NSBseq X ==> \<exists>U. isUb UNIV {x. \<exists>n. X n = x} U" 

529 
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb) 

530 

531 
lemma NSBseq_isLub: "NSBseq X ==> \<exists>U. isLub UNIV {x. \<exists>n. X n = x} U" 

532 
by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub) 

533 

534 

535 
subsection{*A Bounded and Monotonic Sequence Converges*} 

536 

537 
lemma lemma_converg1: 

538 
"!!(X::nat=>real). [ \<forall>m n. m \<le> n > X m \<le> X n; 

539 
isLub (UNIV::real set) {x. \<exists>n. X n = x} (X ma) 

540 
] ==> \<forall>n. ma \<le> n > X n = X ma" 

541 
apply safe 

542 
apply (drule_tac y = "X n" in isLubD2) 

543 
apply (blast dest: order_antisym)+ 

544 
done 

545 

546 
text{* The best of both worlds: Easier to prove this result as a standard 

547 
theorem and then use equivalence to "transfer" it into the 

548 
equivalent nonstandard form if needed!*} 

549 

550 
lemma Bmonoseq_LIMSEQ: "\<forall>n. m \<le> n > X n = X m ==> \<exists>L. (X > L)" 

551 
apply (simp add: LIMSEQ_def) 

552 
apply (rule_tac x = "X m" in exI, safe) 

553 
apply (rule_tac x = m in exI, safe) 

554 
apply (drule spec, erule impE, auto) 

555 
done 

556 

557 
text{*Now, the same theorem in terms of NS limit *} 

558 
lemma Bmonoseq_NSLIMSEQ: "\<forall>n. m \<le> n > X n = X m ==> \<exists>L. (X NS> L)" 

559 
by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff) 

560 

561 
lemma lemma_converg2: 

562 
"!!(X::nat=>real). 

563 
[ \<forall>m. X m ~= U; isLub UNIV {x. \<exists>n. X n = x} U ] ==> \<forall>m. X m < U" 

564 
apply safe 

565 
apply (drule_tac y = "X m" in isLubD2) 

566 
apply (auto dest!: order_le_imp_less_or_eq) 

567 
done 

568 

569 
lemma lemma_converg3: "!!(X ::nat=>real). \<forall>m. X m \<le> U ==> isUb UNIV {x. \<exists>n. X n = x} U" 

570 
by (rule setleI [THEN isUbI], auto) 

571 

572 
text{* FIXME: @{term "U  T < U"} is redundant *} 

573 
lemma lemma_converg4: "!!(X::nat=> real). 

574 
[ \<forall>m. X m ~= U; 

575 
isLub UNIV {x. \<exists>n. X n = x} U; 

576 
0 < T; 

577 
U +  T < U 

578 
] ==> \<exists>m. U + T < X m & X m < U" 

579 
apply (drule lemma_converg2, assumption) 

580 
apply (rule ccontr, simp) 

581 
apply (simp add: linorder_not_less) 

582 
apply (drule lemma_converg3) 

583 
apply (drule isLub_le_isUb, assumption) 

584 
apply (auto dest: order_less_le_trans) 

585 
done 

586 

587 
text{*A standard proof of the theorem for monotone increasing sequence*} 

588 

589 
lemma Bseq_mono_convergent: 

590 
"[ Bseq X; \<forall>m n. m \<le> n > X m \<le> X n ] ==> convergent X" 

591 
apply (simp add: convergent_def) 

592 
apply (frule Bseq_isLub, safe) 

593 
apply (case_tac "\<exists>m. X m = U", auto) 

594 
apply (blast dest: lemma_converg1 Bmonoseq_LIMSEQ) 

595 
(* second case *) 

596 
apply (rule_tac x = U in exI) 

597 
apply (subst LIMSEQ_iff, safe) 

598 
apply (frule lemma_converg2, assumption) 

599 
apply (drule lemma_converg4, auto) 

600 
apply (rule_tac x = m in exI, safe) 

601 
apply (subgoal_tac "X m \<le> X n") 

602 
prefer 2 apply blast 

603 
apply (drule_tac x=n and P="%m. X m < U" in spec, arith) 

604 
done 

605 

606 
text{*Nonstandard version of the theorem*} 

607 

608 
lemma NSBseq_mono_NSconvergent: 

609 
"[ NSBseq X; \<forall>m n. m \<le> n > X m \<le> X n ] ==> NSconvergent X" 

610 
by (auto intro: Bseq_mono_convergent 

611 
simp add: convergent_NSconvergent_iff [symmetric] 

612 
Bseq_NSBseq_iff [symmetric]) 

613 

614 
lemma convergent_minus_iff: "(convergent X) = (convergent (%n. (X n)))" 

615 
apply (simp add: convergent_def) 

616 
apply (auto dest: LIMSEQ_minus) 

617 
apply (drule LIMSEQ_minus, auto) 

618 
done 

619 

620 
lemma Bseq_minus_iff: "Bseq (%n. (X n)) = Bseq X" 

621 
by (simp add: Bseq_def) 

622 

623 
text{*Main monotonicity theorem*} 

624 
lemma Bseq_monoseq_convergent: "[ Bseq X; monoseq X ] ==> convergent X" 

625 
apply (simp add: monoseq_def, safe) 

626 
apply (rule_tac [2] convergent_minus_iff [THEN ssubst]) 

627 
apply (drule_tac [2] Bseq_minus_iff [THEN ssubst]) 

628 
apply (auto intro!: Bseq_mono_convergent) 

629 
done 

630 

631 

632 
subsection{*A Few More Equivalence Theorems for Boundedness*} 

633 

634 
text{*alternative formulation for boundedness*} 

635 
lemma Bseq_iff2: "Bseq X = (\<exists>k x. 0 < k & (\<forall>n. \<bar>X(n) + x\<bar> \<le> k))" 

636 
apply (unfold Bseq_def, safe) 

637 
apply (rule_tac [2] x = "k + \<bar>x\<bar> " in exI) 

638 
apply (rule_tac x = K in exI) 

639 
apply (rule_tac x = 0 in exI, auto) 

640 
apply (drule_tac [!] x=n in spec, arith+) 

641 
done 

642 

643 
text{*alternative formulation for boundedness*} 

644 
lemma Bseq_iff3: "Bseq X = (\<exists>k N. 0 < k & (\<forall>n. abs(X(n) + X(N)) \<le> k))" 

645 
apply safe 

646 
apply (simp add: Bseq_def, safe) 

647 
apply (rule_tac x = "K + \<bar>X N\<bar> " in exI) 

648 
apply auto 

649 
apply arith 

650 
apply (rule_tac x = N in exI, safe) 

651 
apply (drule_tac x = n in spec, arith) 

652 
apply (auto simp add: Bseq_iff2) 

653 
done 

654 

655 
lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f" 

656 
apply (simp add: Bseq_def) 

657 
apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI) 

658 
apply auto 

659 
apply (drule_tac [2] x = n in spec, arith+) 

660 
done 

661 

662 

663 
subsection{*Equivalence Between NS and Standard Cauchy Sequences*} 

664 

665 
subsubsection{*Standard Implies Nonstandard*} 

666 

667 
lemma lemmaCauchy1: 

668 
"Abs_hypnat (hypnatrel `` {x}) : HNatInfinite 

669 
==> {n. M \<le> x n} : FreeUltrafilterNat" 

670 
apply (auto simp add: HNatInfinite_FreeUltrafilterNat_iff) 

671 
apply (drule_tac x = M in spec, ultra) 

672 
done 

673 

674 
lemma lemmaCauchy2: 

675 
"{n. \<forall>m n. M \<le> m & M \<le> (n::nat) > \<bar>X m +  X n\<bar> < u} Int 

676 
{n. M \<le> xa n} Int {n. M \<le> x n} \<le> 

677 
{n. abs (X (xa n) +  X (x n)) < u}" 

678 
by blast 

679 

680 
lemma Cauchy_NSCauchy: "Cauchy X ==> NSCauchy X" 

681 
apply (simp add: Cauchy_def NSCauchy_def, safe) 

682 
apply (rule_tac z = M in eq_Abs_hypnat) 

683 
apply (rule_tac z = N in eq_Abs_hypnat) 

684 
apply (rule approx_minus_iff [THEN iffD2]) 

685 
apply (rule mem_infmal_iff [THEN iffD1]) 

686 
apply (auto simp add: starfunNat hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) 

687 
apply (rule bexI, auto) 

688 
apply (drule spec, auto) 

689 
apply (drule_tac M = M in lemmaCauchy1) 

690 
apply (drule_tac M = M in lemmaCauchy1) 

691 
apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset]) 

692 
apply (rule FreeUltrafilterNat_Int) 

693 
apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set) 

694 
done 

695 

696 
subsubsection{*Nonstandard Implies Standard*} 

697 

698 
lemma NSCauchy_Cauchy: "NSCauchy X ==> Cauchy X" 

699 
apply (auto simp add: Cauchy_def NSCauchy_def) 

700 
apply (rule ccontr, simp) 

701 
apply (auto dest!: choice HNatInfinite_NSLIMSEQ simp add: all_conj_distrib) 

702 
apply (drule bspec, assumption) 

703 
apply (drule_tac x = "Abs_hypnat (hypnatrel `` {fa}) " in bspec); 

704 
apply (auto simp add: starfunNat) 

705 
apply (drule approx_minus_iff [THEN iffD1]) 

706 
apply (drule mem_infmal_iff [THEN iffD2]) 

707 
apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff) 

708 
apply (rename_tac "Y") 

709 
apply (drule_tac x = e in spec, auto) 

710 
apply (drule FreeUltrafilterNat_Int, assumption) 

711 
apply (subgoal_tac "{n. \<bar>X (f n) +  X (fa n)\<bar> < e} \<in> \<U>") 

712 
prefer 2 apply (erule FreeUltrafilterNat_subset, force) 

713 
apply (rule FreeUltrafilterNat_empty [THEN notE]) 

714 
apply (subgoal_tac 

715 
"{n. abs (X (f n) +  X (fa n)) < e} Int 

716 
{M. ~ abs (X (f M) +  X (fa M)) < e} = {}") 

717 
apply auto 

718 
done 

719 

720 

721 
theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X" 

722 
by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy) 

723 

724 
text{*A Cauchy sequence is bounded  this is the standard 

725 
proof mechanization rather than the nonstandard proof*} 

726 

727 
lemma lemmaCauchy: "\<forall>n. M \<le> n > \<bar>X M +  X n\<bar> < (1::real) 

728 
==> \<forall>n. M \<le> n > \<bar>X n\<bar> < 1 + \<bar>X M\<bar>" 

729 
apply safe 

730 
apply (drule spec, auto, arith) 

731 
done 

732 

733 
lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)" 

734 
by auto 

735 

736 
text{* FIXME: Long. Maximal element in subsequence *} 

737 
lemma SUP_rabs_subseq: 

738 
"\<exists>m. m \<le> M & (\<forall>n. n \<le> M > \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)" 

739 
apply (induct M) 

740 
apply (rule_tac x = 0 in exI, simp, safe) 

741 
apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear) 

742 
apply safe 

743 
apply (rule_tac x = m in exI) 

744 
apply (rule_tac [2] x = m in exI) 

745 
apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe) 

746 
apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) 

747 
apply (simp_all add: less_Suc_cancel_iff) 

748 
apply (blast intro: order_le_less_trans [THEN order_less_imp_le]) 

749 
done 

750 

751 
lemma lemma_Nat_covered: 

752 
"[ \<forall>m::nat. m \<le> M > P M m; 

753 
\<forall>m. M \<le> m > P M m ] 

754 
==> \<forall>m. P M m" 

755 
by (auto elim: less_asym simp add: le_def) 

756 

757 

758 
lemma lemma_trans1: 

759 
"[ \<forall>n. n \<le> M > \<bar>(X::nat=>real) n\<bar> \<le> a; a < b ] 

760 
==> \<forall>n. n \<le> M > \<bar>X n\<bar> \<le> b" 

761 
by (blast intro: order_le_less_trans [THEN order_less_imp_le]) 

762 

763 
lemma lemma_trans2: 

764 
"[ \<forall>n. M \<le> n > \<bar>(X::nat=>real) n\<bar> < a; a < b ] 

765 
==> \<forall>n. M \<le> n > \<bar>X n\<bar>\<le> b" 

766 
by (blast intro: order_less_trans [THEN order_less_imp_le]) 

767 

768 
lemma lemma_trans3: 

769 
"[ \<forall>n. n \<le> M > \<bar>X n\<bar> \<le> a; a = b ] 

770 
==> \<forall>n. n \<le> M > \<bar>X n\<bar> \<le> b" 

771 
by auto 

772 

773 
lemma lemma_trans4: "\<forall>n. M \<le> n > \<bar>(X::nat=>real) n\<bar> < a 

774 
==> \<forall>n. M \<le> n > \<bar>X n\<bar> \<le> a" 

775 
by (blast intro: order_less_imp_le) 

776 

777 

778 
text{*Proof is more involved than outlines sketched by various authors 

779 
would suggest*} 

780 

781 
lemma Cauchy_Bseq: "Cauchy X ==> Bseq X" 

782 
apply (simp add: Cauchy_def Bseq_def) 

783 
apply (drule_tac x = 1 in spec) 

784 
apply (erule zero_less_one [THEN [2] impE], safe) 

785 
apply (drule_tac x = M in spec, simp) 

786 
apply (drule lemmaCauchy) 

787 
apply (cut_tac M = M and X = X in SUP_rabs_subseq, safe) 

788 
apply (cut_tac x = "\<bar>X m\<bar> " and y = "1 + \<bar>X M\<bar> " in linorder_less_linear) 

789 
apply safe 

790 
apply (drule lemma_trans1, assumption) 

791 
apply (drule_tac [3] lemma_trans2, erule_tac [3] asm_rl) 

792 
apply (drule_tac [2] lemma_trans3, erule_tac [2] asm_rl) 

793 
apply (drule_tac [3] abs_add_one_gt_zero [THEN order_less_trans]) 

794 
apply (drule lemma_trans4) 

795 
apply (drule_tac [2] lemma_trans4) 

796 
apply (rule_tac x = "1 + \<bar>X M\<bar> " in exI) 

797 
apply (rule_tac [2] x = "1 + \<bar>X M\<bar> " in exI) 

798 
apply (rule_tac [3] x = "\<bar>X m\<bar> " in exI) 

15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15082
diff
changeset

799 
apply (auto elim!: lemma_Nat_covered) 
15082  800 
done 
801 

802 
text{*A Cauchy sequence is bounded  nonstandard version*} 

803 

804 
lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X" 

805 
by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff) 

806 

807 

808 
text{*Equivalence of Cauchy criterion and convergence: 

809 
We will prove this using our NS formulation which provides a 

810 
much easier proof than using the standard definition. We do not 

811 
need to use properties of subsequences such as boundedness, 

812 
monotonicity etc... Compare with Harrison's corresponding proof 

813 
in HOL which is much longer and more complicated. Of course, we do 

814 
not have problems which he encountered with guessing the right 

815 
instantiations for his 'espsilondelta' proof(s) in this case 

816 
since the NS formulations do not involve existential quantifiers.*} 

817 

818 
lemma NSCauchy_NSconvergent_iff: "NSCauchy X = NSconvergent X" 

819 
apply (simp add: NSconvergent_def NSLIMSEQ_def, safe) 

820 
apply (frule NSCauchy_NSBseq) 

821 
apply (auto intro: approx_trans2 simp add: NSBseq_def NSCauchy_def) 

822 
apply (drule HNatInfinite_whn [THEN [2] bspec]) 

823 
apply (drule HNatInfinite_whn [THEN [2] bspec]) 

824 
apply (auto dest!: st_part_Ex simp add: SReal_iff) 

825 
apply (blast intro: approx_trans3) 

826 
done 

827 

828 
text{*Standard proof for free*} 

829 
lemma Cauchy_convergent_iff: "Cauchy X = convergent X" 

830 
by (simp add: NSCauchy_Cauchy_iff [symmetric] convergent_NSconvergent_iff NSCauchy_NSconvergent_iff) 

831 

832 

833 
text{*We can now try and derive a few properties of sequences, 

834 
starting with the limit comparison property for sequences.*} 

835 

836 
lemma NSLIMSEQ_le: 

837 
"[ f NS> l; g NS> m; 

838 
\<exists>N. \<forall>n. N \<le> n > f(n) \<le> g(n) 

839 
] ==> l \<le> m" 

840 
apply (simp add: NSLIMSEQ_def, safe) 

841 
apply (drule starfun_le_mono) 

842 
apply (drule HNatInfinite_whn [THEN [2] bspec])+ 

843 
apply (drule_tac x = whn in spec) 

844 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ 

845 
apply clarify 

846 
apply (auto intro: hypreal_of_real_le_add_Infininitesimal_cancel2) 

847 
done 

848 

849 
(* standard version *) 

850 
lemma LIMSEQ_le: 

851 
"[ f > l; g > m; \<exists>N. \<forall>n. N \<le> n > f(n) \<le> g(n) ] 

852 
==> l \<le> m" 

853 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le) 

854 

855 
lemma LIMSEQ_le_const: "[ X > r; \<forall>n. a \<le> X n ] ==> a \<le> r" 

856 
apply (rule LIMSEQ_le) 

857 
apply (rule LIMSEQ_const, auto) 

858 
done 

859 

860 
lemma NSLIMSEQ_le_const: "[ X NS> r; \<forall>n. a \<le> X n ] ==> a \<le> r" 

861 
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const) 

862 

863 
lemma LIMSEQ_le_const2: "[ X > r; \<forall>n. X n \<le> a ] ==> r \<le> a" 

864 
apply (rule LIMSEQ_le) 

865 
apply (rule_tac [2] LIMSEQ_const, auto) 

866 
done 

867 

868 
lemma NSLIMSEQ_le_const2: "[ X NS> r; \<forall>n. X n \<le> a ] ==> r \<le> a" 

869 
by (simp add: LIMSEQ_NSLIMSEQ_iff LIMSEQ_le_const2) 

870 

871 
text{*Shift a convergent series by 1: 

872 
By the equivalence between Cauchiness and convergence and because 

873 
the successor of an infinite hypernatural is also infinite.*} 

874 

875 
lemma NSLIMSEQ_Suc: "f NS> l ==> (%n. f(Suc n)) NS> l" 

876 
apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]]) 

877 
apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one) 

878 
apply (drule bspec, assumption) 

879 
apply (drule bspec, assumption) 

880 
apply (drule Nats_1 [THEN [2] HNatInfinite_SHNat_add]) 

881 
apply (blast intro: approx_trans3) 

882 
done 

883 

884 
text{* standard version *} 

885 
lemma LIMSEQ_Suc: "f > l ==> (%n. f(Suc n)) > l" 

886 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc) 

887 

888 
lemma NSLIMSEQ_imp_Suc: "(%n. f(Suc n)) NS> l ==> f NS> l" 

889 
apply (frule NSconvergentI [THEN NSCauchy_NSconvergent_iff [THEN iffD2]]) 

890 
apply (auto simp add: NSCauchy_def NSLIMSEQ_def starfunNat_shift_one) 

891 
apply (drule bspec, assumption) 

892 
apply (drule bspec, assumption) 

893 
apply (frule Nats_1 [THEN [2] HNatInfinite_SHNat_diff]) 

894 
apply (drule_tac x="N  1" in bspec) 

895 
apply (auto intro: approx_trans3) 

896 
done 

897 

898 
lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) > l ==> f > l" 

899 
apply (simp add: LIMSEQ_NSLIMSEQ_iff) 

900 
apply (erule NSLIMSEQ_imp_Suc) 

901 
done 

902 

903 
lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) > l) = (f > l)" 

904 
by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc) 

905 

906 
lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) NS> l) = (f NS> l)" 

907 
by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc) 

908 

909 
text{*A sequence tends to zero iff its abs does*} 

910 
lemma LIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) > 0) = (f > 0)" 

911 
by (simp add: LIMSEQ_def) 

912 

913 
text{*We prove the NS version from the standard one, since the NS proof 

914 
seems more complicated than the standard one above!*} 

915 
lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) NS> 0) = (f NS> 0)" 

916 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_rabs_zero) 

917 

918 
text{*Generalization to other limits*} 

919 
lemma NSLIMSEQ_imp_rabs: "f NS> l ==> (%n. \<bar>f n\<bar>) NS> \<bar>l\<bar>" 

920 
apply (simp add: NSLIMSEQ_def) 

921 
apply (auto intro: approx_hrabs 

922 
simp add: starfunNat_rabs hypreal_of_real_hrabs [symmetric]) 

923 
done 

924 

925 
text{* standard version *} 

926 
lemma LIMSEQ_imp_rabs: "f > l ==> (%n. \<bar>f n\<bar>) > \<bar>l\<bar>" 

927 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_imp_rabs) 

928 

929 
text{*An unbounded sequence's inverse tends to 0*} 

930 

931 
text{* standard proof seems easier *} 

932 
lemma LIMSEQ_inverse_zero: 

933 
"\<forall>y. \<exists>N. \<forall>n. N \<le> n > y < f(n) ==> (%n. inverse(f n)) > 0" 

934 
apply (simp add: LIMSEQ_def, safe) 

935 
apply (drule_tac x = "inverse r" in spec, safe) 

936 
apply (rule_tac x = N in exI, safe) 

937 
apply (drule spec, auto) 

938 
apply (frule positive_imp_inverse_positive) 

939 
apply (frule order_less_trans, assumption) 

940 
apply (frule_tac a = "f n" in positive_imp_inverse_positive) 

941 
apply (simp add: abs_if) 

942 
apply (rule_tac t = r in inverse_inverse_eq [THEN subst]) 

943 
apply (auto intro: inverse_less_iff_less [THEN iffD2] 

944 
simp del: inverse_inverse_eq) 

945 
done 

946 

947 
lemma NSLIMSEQ_inverse_zero: 

948 
"\<forall>y. \<exists>N. \<forall>n. N \<le> n > y < f(n) 

949 
==> (%n. inverse(f n)) NS> 0" 

950 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero) 

951 

952 
text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*} 

953 

954 
lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) > 0" 

955 
apply (rule LIMSEQ_inverse_zero, safe) 

956 
apply (cut_tac x = y in reals_Archimedean2) 

957 
apply (safe, rule_tac x = n in exI) 

958 
apply (auto simp add: real_of_nat_Suc) 

959 
done 

960 

961 
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) NS> 0" 

962 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat) 

963 

964 
text{*The sequence @{term "r + 1/n"} tends to @{term r} as @{term n} tends to 

965 
infinity is now easily proved*} 

966 

967 
lemma LIMSEQ_inverse_real_of_nat_add: 

968 
"(%n. r + inverse(real(Suc n))) > r" 

969 
by (cut_tac LIMSEQ_add [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) 

970 

971 
lemma NSLIMSEQ_inverse_real_of_nat_add: 

972 
"(%n. r + inverse(real(Suc n))) NS> r" 

973 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add) 

974 

975 
lemma LIMSEQ_inverse_real_of_nat_add_minus: 

976 
"(%n. r + inverse(real(Suc n))) > r" 

977 
by (cut_tac LIMSEQ_add_minus [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat], auto) 

978 

979 
lemma NSLIMSEQ_inverse_real_of_nat_add_minus: 

980 
"(%n. r + inverse(real(Suc n))) NS> r" 

981 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus) 

982 

983 
lemma LIMSEQ_inverse_real_of_nat_add_minus_mult: 

984 
"(%n. r*( 1 + inverse(real(Suc n)))) > r" 

985 
by (cut_tac b=1 in 

986 
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto) 

987 

988 
lemma NSLIMSEQ_inverse_real_of_nat_add_minus_mult: 

989 
"(%n. r*( 1 + inverse(real(Suc n)))) NS> r" 

990 
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add_minus_mult) 

991 

992 

993 
text{* Real Powers*} 

994 

995 
lemma NSLIMSEQ_pow [rule_format]: 

996 
"(X NS> a) > ((%n. (X n) ^ m) NS> a ^ m)" 

997 
apply (induct_tac "m") 

998 
apply (auto intro: NSLIMSEQ_mult NSLIMSEQ_const) 

999 
done 

1000 

1001 
lemma LIMSEQ_pow: "X > a ==> (%n. (X n) ^ m) > a ^ m" 

1002 
by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_pow) 

1003 

1004 
text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term 

1005 
"x<1"}. Proof will use (NS) Cauchy equivalence for convergence and 

1006 
also fact that bounded and monotonic sequence converges.*} 

1007 

1008 
lemma Bseq_realpow: "[ 0 \<le> x; x \<le> 1 ] ==> Bseq (%n. x ^ n)" 

1009 
apply (simp add: Bseq_def) 

1010 
apply (rule_tac x = 1 in exI) 

1011 
apply (simp add: power_abs) 

1012 
apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if) 

1013 
done 

1014 

1015 
lemma monoseq_realpow: "[ 0 \<le> x; x \<le> 1 ] ==> monoseq (%n. x ^ n)" 

1016 
apply (clarify intro!: mono_SucI2) 

1017 
apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing, auto) 

1018 
done 

1019 

1020 
lemma convergent_realpow: "[ 0 \<le> x; x \<le> 1 ] ==> convergent (%n. x ^ n)" 

1021 
by (blast intro!: Bseq_monoseq_convergent Bseq_realpow monoseq_realpow) 

1022 

1023 
text{* We now use NS criterion to bring proof of theorem through *} 

1024 

1025 
lemma NSLIMSEQ_realpow_zero: "[ 0 \<le> x; x < 1 ] ==> (%n. x ^ n) NS> 0" 

1026 
apply (simp add: NSLIMSEQ_def) 

1027 
apply (auto dest!: convergent_realpow simp add: convergent_NSconvergent_iff) 

1028 
apply (frule NSconvergentD) 

1029 
apply (auto simp add: NSLIMSEQ_def NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_pow) 

1030 
apply (frule HNatInfinite_add_one) 

1031 
apply (drule bspec, assumption) 

1032 
apply (drule bspec, assumption) 

1033 
apply (drule_tac x = "N + (1::hypnat) " in bspec, assumption) 

1034 
apply (simp add: hyperpow_add) 

1035 
apply (drule approx_mult_subst_SReal, assumption) 

1036 
apply (drule approx_trans3, assumption) 

1037 
apply (auto simp del: hypreal_of_real_mult simp add: hypreal_of_real_mult [symmetric]) 

1038 
done 

1039 

1040 
text{* standard version *} 

1041 
lemma LIMSEQ_realpow_zero: "[ 0 \<le> x; x < 1 ] ==> (%n. x ^ n) > 0" 

1042 
by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff) 

1043 

1044 
lemma LIMSEQ_divide_realpow_zero: "1 < x ==> (%n. a / (x ^ n)) > 0" 

1045 
apply (cut_tac a = a and x1 = "inverse x" in 

1046 
LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_realpow_zero]) 

1047 
apply (auto simp add: divide_inverse power_inverse) 

1048 
apply (simp add: inverse_eq_divide pos_divide_less_eq) 

1049 
done 

1050 

1051 
subsubsection{*Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}*} 

1052 

1053 
lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) > 0" 

1054 
by (blast intro!: LIMSEQ_realpow_zero abs_ge_zero) 

1055 

1056 
lemma NSLIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 ==> (%n. \<bar>c\<bar> ^ n) NS> 0" 

1057 
by (simp add: LIMSEQ_rabs_realpow_zero LIMSEQ_NSLIMSEQ_iff [symmetric]) 

1058 

1059 
lemma LIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) > 0" 

1060 
apply (rule LIMSEQ_rabs_zero [THEN iffD1]) 

1061 
apply (auto intro: LIMSEQ_rabs_realpow_zero simp add: power_abs) 

1062 
done 

1063 

1064 
lemma NSLIMSEQ_rabs_realpow_zero2: "\<bar>c\<bar> < 1 ==> (%n. c ^ n) NS> 0" 

1065 
by (simp add: LIMSEQ_rabs_realpow_zero2 LIMSEQ_NSLIMSEQ_iff [symmetric]) 

1066 

1067 
subsection{*Hyperreals and Sequences*} 

1068 

1069 
text{*A bounded sequence is a finite hyperreal*} 

1070 
lemma NSBseq_HFinite_hypreal: "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite" 

1071 
by (auto intro!: bexI lemma_hyprel_refl 

1072 
intro: FreeUltrafilterNat_all [THEN FreeUltrafilterNat_subset] 

1073 
simp add: HFinite_FreeUltrafilterNat_iff Bseq_NSBseq_iff [symmetric] 

1074 
Bseq_iff1a) 

1075 

1076 
text{*A sequence converging to zero defines an infinitesimal*} 

1077 
lemma NSLIMSEQ_zero_Infinitesimal_hypreal: 

1078 
"X NS> 0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal" 

1079 
apply (simp add: NSLIMSEQ_def) 

1080 
apply (drule_tac x = whn in bspec) 

1081 
apply (simp add: HNatInfinite_whn) 

1082 
apply (auto simp add: hypnat_omega_def mem_infmal_iff [symmetric] starfunNat) 

1083 
done 

1084 

1085 
(*** 

1086 
Theorems proved by Harrison in HOL that we do not need 

1087 
in order to prove equivalence between Cauchy criterion 

1088 
and convergence: 

1089 
 Show that every sequence contains a monotonic subsequence 

1090 
Goal "\<exists>f. subseq f & monoseq (%n. s (f n))" 

1091 
 Show that a subsequence of a bounded sequence is bounded 

1092 
Goal "Bseq X ==> Bseq (%n. X (f n))"; 

1093 
 Show we can take subsequential terms arbitrarily far 

1094 
up a sequence 

1095 
Goal "subseq f ==> n \<le> f(n)"; 

1096 
Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)"; 

1097 
***) 

1098 

1099 
ML 

1100 
{* 

1101 
val Cauchy_def = thm"Cauchy_def"; 

1102 
val SEQ_Infinitesimal = thm "SEQ_Infinitesimal"; 

1103 
val LIMSEQ_iff = thm "LIMSEQ_iff"; 

1104 
val NSLIMSEQ_iff = thm "NSLIMSEQ_iff"; 

1105 
val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ"; 

1106 
val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set"; 

1107 
val Compl_less_set = thm "Compl_less_set"; 

1108 
val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ"; 

1109 
val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ"; 

1110 
val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ"; 

1111 
val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff"; 

1112 
val NSLIMSEQ_const = thm "NSLIMSEQ_const"; 

1113 
val LIMSEQ_const = thm "LIMSEQ_const"; 

1114 
val NSLIMSEQ_add = thm "NSLIMSEQ_add"; 

1115 
val LIMSEQ_add = thm "LIMSEQ_add"; 

1116 
val NSLIMSEQ_mult = thm "NSLIMSEQ_mult"; 

1117 
val LIMSEQ_mult = thm "LIMSEQ_mult"; 

1118 
val NSLIMSEQ_minus = thm "NSLIMSEQ_minus"; 

1119 
val LIMSEQ_minus = thm "LIMSEQ_minus"; 

1120 
val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel"; 

1121 
val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel"; 

1122 
val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus"; 

1123 
val LIMSEQ_add_minus = thm "LIMSEQ_add_minus"; 

1124 
val LIMSEQ_diff = thm "LIMSEQ_diff"; 

1125 
val NSLIMSEQ_diff = thm "NSLIMSEQ_diff"; 

1126 
val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse"; 

1127 
val LIMSEQ_inverse = thm "LIMSEQ_inverse"; 

1128 
val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse"; 

1129 
val LIMSEQ_divide = thm "LIMSEQ_divide"; 

1130 
val NSLIMSEQ_unique = thm "NSLIMSEQ_unique"; 

1131 
val LIMSEQ_unique = thm "LIMSEQ_unique"; 

1132 
val limI = thm "limI"; 

1133 
val nslimI = thm "nslimI"; 

1134 
val lim_nslim_iff = thm "lim_nslim_iff"; 

1135 
val convergentD = thm "convergentD"; 

1136 
val convergentI = thm "convergentI"; 

1137 
val NSconvergentD = thm "NSconvergentD"; 

1138 
val NSconvergentI = thm "NSconvergentI"; 

1139 
val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff"; 

1140 
val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff"; 

1141 
val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff"; 

1142 
val subseq_Suc_iff = thm "subseq_Suc_iff"; 

1143 
val monoseq_Suc = thm "monoseq_Suc"; 

1144 
val monoI1 = thm "monoI1"; 

1145 
val monoI2 = thm "monoI2"; 

1146 
val mono_SucI1 = thm "mono_SucI1"; 

1147 
val mono_SucI2 = thm "mono_SucI2"; 

1148 
val BseqD = thm "BseqD"; 

1149 
val BseqI = thm "BseqI"; 

1150 
val Bseq_iff = thm "Bseq_iff"; 

1151 
val Bseq_iff1a = thm "Bseq_iff1a"; 

1152 
val NSBseqD = thm "NSBseqD"; 

1153 
val NSBseqI = thm "NSBseqI"; 

1154 
val Bseq_NSBseq = thm "Bseq_NSBseq"; 

1155 
val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite"; 

1156 
val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f"; 

1157 
val NSBseq_Bseq = thm "NSBseq_Bseq"; 

1158 
val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff"; 

1159 
val NSconvergent_NSBseq = thm "NSconvergent_NSBseq"; 

1160 
val convergent_Bseq = thm "convergent_Bseq"; 

1161 
val Bseq_isUb = thm "Bseq_isUb"; 

1162 
val Bseq_isLub = thm "Bseq_isLub"; 

1163 
val NSBseq_isUb = thm "NSBseq_isUb"; 

1164 
val NSBseq_isLub = thm "NSBseq_isLub"; 

1165 
val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ"; 

1166 
val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ"; 

1167 
val Bseq_mono_convergent = thm "Bseq_mono_convergent"; 

1168 
val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent"; 

1169 
val convergent_minus_iff = thm "convergent_minus_iff"; 

1170 
val Bseq_minus_iff = thm "Bseq_minus_iff"; 

1171 
val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent"; 

1172 
val Bseq_iff2 = thm "Bseq_iff2"; 

1173 
val Bseq_iff3 = thm "Bseq_iff3"; 

1174 
val BseqI2 = thm "BseqI2"; 

1175 
val Cauchy_NSCauchy = thm "Cauchy_NSCauchy"; 

1176 
val NSCauchy_Cauchy = thm "NSCauchy_Cauchy"; 

1177 
val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff"; 

1178 
val less_Suc_cancel_iff = thm "less_Suc_cancel_iff"; 

1179 
val SUP_rabs_subseq = thm "SUP_rabs_subseq"; 

1180 
val Cauchy_Bseq = thm "Cauchy_Bseq"; 

1181 
val NSCauchy_NSBseq = thm "NSCauchy_NSBseq"; 

1182 
val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff"; 

1183 
val Cauchy_convergent_iff = thm "Cauchy_convergent_iff"; 

1184 
val NSLIMSEQ_le = thm "NSLIMSEQ_le"; 

1185 
val LIMSEQ_le = thm "LIMSEQ_le"; 

1186 
val LIMSEQ_le_const = thm "LIMSEQ_le_const"; 

1187 
val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const"; 

1188 
val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2"; 

1189 
val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2"; 

1190 
val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc"; 

1191 
val LIMSEQ_Suc = thm "LIMSEQ_Suc"; 

1192 
val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc"; 

1193 
val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc"; 

1194 
val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff"; 

1195 
val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff"; 

1196 
val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero"; 

1197 
val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero"; 

1198 
val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs"; 

1199 
val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs"; 

1200 
val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero"; 

1201 
val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero"; 

1202 
val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat"; 

1203 
val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat"; 

1204 
val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add"; 

1205 
val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add"; 

1206 
val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus"; 

1207 
val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus"; 

1208 
val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult"; 

1209 
val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult"; 

1210 
val NSLIMSEQ_pow = thm "NSLIMSEQ_pow"; 

1211 
val LIMSEQ_pow = thm "LIMSEQ_pow"; 

1212 
val Bseq_realpow = thm "Bseq_realpow"; 

1213 
val monoseq_realpow = thm "monoseq_realpow"; 

1214 
val convergent_realpow = thm "convergent_realpow"; 

1215 
val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero"; 

1216 
val LIMSEQ_realpow_zero = thm "LIMSEQ_realpow_zero"; 

1217 
val LIMSEQ_divide_realpow_zero = thm "LIMSEQ_divide_realpow_zero"; 

1218 
val LIMSEQ_rabs_realpow_zero = thm "LIMSEQ_rabs_realpow_zero"; 

1219 
val NSLIMSEQ_rabs_realpow_zero = thm "NSLIMSEQ_rabs_realpow_zero"; 

1220 
val LIMSEQ_rabs_realpow_zero2 = thm "LIMSEQ_rabs_realpow_zero2"; 

1221 
val NSLIMSEQ_rabs_realpow_zero2 = thm "NSLIMSEQ_rabs_realpow_zero2"; 

1222 
val NSBseq_HFinite_hypreal = thm "NSBseq_HFinite_hypreal"; 

1223 
val NSLIMSEQ_zero_Infinitesimal_hypreal = thm "NSLIMSEQ_zero_Infinitesimal_hypreal"; 

1224 
*} 

1225 

10751  1226 
end 
1227 