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