src/HOL/Real/Hyperreal/SEQ.thy
 changeset 10045 c76b73e16711 child 10648 a8c647cfa31f
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Real/Hyperreal/SEQ.thy	Thu Sep 21 12:17:11 2000 +0200
1.3 @@ -0,0 +1,63 @@
1.4 +(*  Title       : SEQ.thy
1.5 +    Author      : Jacques D. Fleuriot
1.6 +    Copyright   : 1998  University of Cambridge
1.7 +    Description : Convergence of sequences and series
1.8 +*)
1.9 +
1.10 +SEQ = NatStar + HyperPow +
1.11 +
1.12 +constdefs
1.13 +
1.14 +  (* Standard definition of convergence of sequence *)
1.15 +  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" 60)
1.16 +  "X ----> L == (ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
1.17 +
1.18 +  (* Nonstandard definition of convergence of sequence *)
1.19 +  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" 60)
1.20 +  "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"
1.21 +
1.22 +  (* define value of limit using choice operator*)
1.23 +  lim :: (nat => real) => real
1.24 +  "lim X == (@L. (X ----> L))"
1.25 +
1.26 +  nslim :: (nat => real) => real
1.27 +  "nslim X == (@L. (X ----NS> L))"
1.28 +
1.29 +  (* Standard definition of convergence *)
1.30 +  convergent :: (nat => real) => bool
1.31 +  "convergent X == (EX L. (X ----> L))"
1.32 +
1.33 +  (* Nonstandard definition of convergence *)
1.34 +  NSconvergent :: (nat => real) => bool
1.35 +  "NSconvergent X == (EX L. (X ----NS> L))"
1.36 +
1.37 +  (* Standard definition for bounded sequence *)
1.38 +  Bseq :: (nat => real) => bool
1.39 +  "Bseq X == (EX K. (#0 < K & (ALL n. abs(X n) <= K)))"
1.40 +
1.41 +  (* Nonstandard definition for bounded sequence *)
1.42 +  NSBseq :: (nat=>real) => bool
1.43 +  "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)"
1.44 +
1.45 +  (* Definition for monotonicity *)
1.46 +  monoseq :: (nat=>real)=>bool
1.47 +  "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) |
1.48 +                 (ALL m n. m <= n --> X n <= X m))"
1.49 +
1.50 +  (* Definition of subsequence *)
1.51 +  subseq :: (nat => nat) => bool
1.52 +  "subseq f == (ALL m n. m < n --> (f m) < (f n))"
1.53 +
1.54 +  (** Cauchy condition **)
1.55 +
1.56 +  (* Standard definition *)
1.57 +  Cauchy :: (nat => real) => bool
1.58 +  "Cauchy X == (ALL e. (#0 < e -->
1.59 +                       (EX M. (ALL m n. M <= m & M <= n
1.60 +                             --> abs((X m) + -(X n)) < e))))"
1.61 +
1.62 +  NSCauchy :: (nat => real) => bool
1.63 +  "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
1.64 +                      (*fNat* X) M @= (*fNat* X) N)"
1.65 +end
1.66 +
```