equal
deleted
inserted
replaced
|
1 (* Title : Filter.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Filters and Ultrafilters |
|
5 *) |
|
6 |
|
7 Filter = Zorn + |
|
8 |
|
9 constdefs |
|
10 |
|
11 is_Filter :: ['a set set,'a set] => bool |
|
12 "is_Filter F S == (F <= Pow(S) & S : F & {} ~: F & |
|
13 (ALL u: F. ALL v: F. u Int v : F) & |
|
14 (ALL u v. u: F & u <= v & v <= S --> v: F))" |
|
15 |
|
16 Filter :: 'a set => 'a set set set |
|
17 "Filter S == {X. is_Filter X S}" |
|
18 |
|
19 (* free filter does not contain any finite set *) |
|
20 |
|
21 Freefilter :: 'a set => 'a set set set |
|
22 "Freefilter S == {X. X: Filter S & (ALL x: X. ~ finite x)}" |
|
23 |
|
24 Ultrafilter :: 'a set => 'a set set set |
|
25 "Ultrafilter S == {X. X: Filter S & (ALL A: Pow(S). A: X | S - A : X)}" |
|
26 |
|
27 FreeUltrafilter :: 'a set => 'a set set set |
|
28 "FreeUltrafilter S == {X. X: Ultrafilter S & (ALL x: X. ~ finite x)}" |
|
29 |
|
30 (* A locale makes proof of Ultrafilter Theorem more modular *) |
|
31 locale UFT = |
|
32 fixes frechet :: "'a set => 'a set set" |
|
33 superfrechet :: "'a set => 'a set set set" |
|
34 |
|
35 assumes not_finite_UNIV "~finite (UNIV :: 'a set)" |
|
36 |
|
37 defines frechet_def "frechet S == {A. finite (S - A)}" |
|
38 superfrechet_def "superfrechet S == |
|
39 {G. G: Filter S & frechet S <= G}" |
|
40 end |
|
41 |
|
42 |
|
43 |
|
44 |