src/HOL/Hyperreal/SEQ.thy
author nipkow
Fri Feb 07 16:40:23 2003 +0100 (2003-02-07)
changeset 13810 c3fbfd472365
parent 12018 ec054019c910
child 15082 6c3276a2735b
permissions -rw-r--r--
(*f -> ( *f because of new comments
     1 (*  Title       : SEQ.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : Convergence of sequences and series
     5 *) 
     6 
     7 SEQ = NatStar + HyperPow + 
     8 
     9 constdefs
    10 
    11   (* Standard definition of convergence of sequence *)           
    12   LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" [60, 60] 60)
    13   "X ----> L == (ALL r. 0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
    14   
    15   (* Nonstandard definition of convergence of sequence *)
    16   NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
    17   "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"
    18 
    19   (* define value of limit using choice operator*)
    20   lim :: (nat => real) => real
    21   "lim X == (@L. (X ----> L))"
    22 
    23   nslim :: (nat => real) => real
    24   "nslim X == (@L. (X ----NS> L))"
    25 
    26   (* Standard definition of convergence *)
    27   convergent :: (nat => real) => bool
    28   "convergent X == (EX L. (X ----> L))"
    29 
    30   (* Nonstandard definition of convergence *)
    31   NSconvergent :: (nat => real) => bool
    32   "NSconvergent X == (EX L. (X ----NS> L))"
    33 
    34   (* Standard definition for bounded sequence *)
    35   Bseq :: (nat => real) => bool
    36   "Bseq X == (EX K. (0 < K & (ALL n. abs(X n) <= K)))"
    37  
    38   (* Nonstandard definition for bounded sequence *)
    39   NSBseq :: (nat=>real) => bool
    40   "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" 
    41 
    42   (* Definition for monotonicity *)
    43   monoseq :: (nat=>real)=>bool
    44   "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) |
    45                  (ALL m n. m <= n --> X n <= X m))"   
    46 
    47   (* Definition of subsequence *)
    48   subseq :: (nat => nat) => bool
    49   "subseq f == (ALL m n. m < n --> (f m) < (f n))"
    50 
    51   (** Cauchy condition **)
    52 
    53   (* Standard definition *)
    54   Cauchy :: (nat => real) => bool
    55   "Cauchy X == (ALL e. (0 < e -->
    56                        (EX M. (ALL m n. M <= m & M <= n 
    57                              --> abs((X m) + -(X n)) < e))))"
    58 
    59   NSCauchy :: (nat => real) => bool
    60   "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
    61                       ( *fNat* X) M @= ( *fNat* X) N)"
    62 end
    63