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