src/HOL/Hyperreal/SEQ.thy

separation of HOL-Hyperreal from HOL-Real

(*  Title       : SEQ.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Convergence of sequences and series
*) 

SEQ = NatStar + HyperPow + 

constdefs

  (* Standard definition of convergence of sequence *)           
  LIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----> (_))" [60, 60] 60)
  "X ----> L == (ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs (X n + -L) < r))"
  
  (* Nonstandard definition of convergence of sequence *)
  NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
  "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"

  (* define value of limit using choice operator*)
  lim :: (nat => real) => real
  "lim X == (@L. (X ----> L))"

  nslim :: (nat => real) => real
  "nslim X == (@L. (X ----NS> L))"

  (* Standard definition of convergence *)
  convergent :: (nat => real) => bool
  "convergent X == (EX L. (X ----> L))"

  (* Nonstandard definition of convergence *)
  NSconvergent :: (nat => real) => bool
  "NSconvergent X == (EX L. (X ----NS> L))"

  (* Standard definition for bounded sequence *)
  Bseq :: (nat => real) => bool
  "Bseq X == (EX K. (#0 < K & (ALL n. abs(X n) <= K)))"
 
  (* Nonstandard definition for bounded sequence *)
  NSBseq :: (nat=>real) => bool
  "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)" 

  (* Definition for monotonicity *)
  monoseq :: (nat=>real)=>bool
  "monoseq X == ((ALL (m::nat) n. m <= n --> X m <= X n) |
                 (ALL m n. m <= n --> X n <= X m))"   

  (* Definition of subsequence *)
  subseq :: (nat => nat) => bool
  "subseq f == (ALL m n. m < n --> (f m) < (f n))"

  (** Cauchy condition **)

  (* Standard definition *)
  Cauchy :: (nat => real) => bool
  "Cauchy X == (ALL e. (#0 < e -->
                       (EX M. (ALL m n. M <= m & M <= n 
                             --> abs((X m) + -(X n)) < e))))"

  NSCauchy :: (nat => real) => bool
  "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
                      (*fNat* X) M @= (*fNat* X) N)"
end