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