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 +