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