author | wenzelm |
Mon, 10 Dec 2001 20:59:43 +0100 | |
changeset 12459 | 6978ab7cac64 |
parent 10834 | a7897aebbffc |
child 13115 | 0a6fbdedcde2 |
permissions | -rw-r--r-- |
7112 | 1 |
(* Title: HOL/ex/Tarski |
2 |
ID: $Id$ |
|
3 |
Author: Florian Kammueller, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Minimal version of lattice theory plus the full theorem of Tarski: |
|
7 |
The fixedpoints of a complete lattice themselves form a complete lattice. |
|
8 |
||
9 |
Illustrates first-class theories, using the Sigma representation of structures |
|
10 |
*) |
|
11 |
||
12 |
Tarski = Main + |
|
13 |
||
14 |
||
15 |
record 'a potype = |
|
16 |
pset :: "'a set" |
|
17 |
order :: "('a * 'a) set" |
|
18 |
||
19 |
syntax |
|
20 |
"@pset" :: "'a potype => 'a set" ("_ .<A>" [90] 90) |
|
21 |
"@order" :: "'a potype => ('a *'a)set" ("_ .<r>" [90] 90) |
|
22 |
||
23 |
translations |
|
24 |
"po.<A>" == "pset po" |
|
25 |
"po.<r>" == "order po" |
|
26 |
||
27 |
constdefs |
|
28 |
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" |
|
29 |
"monotone f A r == ! x: A. ! y: A. (x, y): r --> ((f x), (f y)) : r" |
|
30 |
||
31 |
least :: "['a => bool, 'a potype] => 'a" |
|
32 |
"least P po == @ x. x: po.<A> & P x & |
|
33 |
(! y: po.<A>. P y --> (x,y): po.<r>)" |
|
34 |
||
35 |
greatest :: "['a => bool, 'a potype] => 'a" |
|
36 |
"greatest P po == @ x. x: po.<A> & P x & |
|
37 |
(! y: po.<A>. P y --> (y,x): po.<r>)" |
|
38 |
||
39 |
lub :: "['a set, 'a potype] => 'a" |
|
40 |
"lub S po == least (%x. ! y: S. (y,x): po.<r>) po" |
|
41 |
||
42 |
glb :: "['a set, 'a potype] => 'a" |
|
43 |
"glb S po == greatest (%x. ! y: S. (x,y): po.<r>) po" |
|
44 |
||
45 |
islub :: "['a set, 'a potype, 'a] => bool" |
|
46 |
"islub S po == %L. (L: po.<A> & (! y: S. (y,L): po.<r>) & |
|
47 |
(! z:po.<A>. (! y: S. (y,z): po.<r>) --> (L,z): po.<r>))" |
|
48 |
||
49 |
isglb :: "['a set, 'a potype, 'a] => bool" |
|
50 |
"isglb S po == %G. (G: po.<A> & (! y: S. (G,y): po.<r>) & |
|
51 |
(! z: po.<A>. (! y: S. (z,y): po.<r>) --> (z,G): po.<r>))" |
|
52 |
||
53 |
fix :: "[('a => 'a), 'a set] => 'a set" |
|
54 |
"fix f A == {x. x: A & f x = x}" |
|
55 |
||
56 |
interval :: "[('a*'a) set,'a, 'a ] => 'a set" |
|
57 |
"interval r a b == {x. (a,x): r & (x,b): r}" |
|
58 |
||
59 |
||
60 |
constdefs |
|
61 |
Bot :: "'a potype => 'a" |
|
62 |
"Bot po == least (%x. True) po" |
|
63 |
||
64 |
Top :: "'a potype => 'a" |
|
65 |
"Top po == greatest (%x. True) po" |
|
66 |
||
67 |
PartialOrder :: "('a potype) set" |
|
68 |
"PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) & |
|
69 |
trans (P.<r>)}" |
|
70 |
||
71 |
CompleteLattice :: "('a potype) set" |
|
72 |
"CompleteLattice == {cl. cl: PartialOrder & |
|
73 |
(! S. S <= cl.<A> --> (? L. islub S cl L)) & |
|
74 |
(! S. S <= cl.<A> --> (? G. isglb S cl G))}" |
|
75 |
||
76 |
CLF :: "('a potype * ('a => 'a)) set" |
|
77 |
"CLF == SIGMA cl: CompleteLattice. |
|
78 |
{f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}" |
|
79 |
||
80 |
induced :: "['a set, ('a * 'a) set] => ('a *'a)set" |
|
81 |
"induced A r == {(a,b). a : A & b: A & (a,b): r}" |
|
82 |
||
83 |
||
84 |
||
85 |
||
86 |
constdefs |
|
87 |
sublattice :: "('a potype * 'a set)set" |
|
88 |
"sublattice == |
|
89 |
SIGMA cl: CompleteLattice. |
|
90 |
{S. S <= cl.<A> & |
|
91 |
(| pset = S, order = induced S (cl.<r>) |): CompleteLattice }" |
|
92 |
||
93 |
syntax |
|
94 |
"@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50) |
|
95 |
||
96 |
translations |
|
10834 | 97 |
"S <<= cl" == "S : sublattice `` {cl}" |
7112 | 98 |
|
99 |
constdefs |
|
100 |
dual :: "'a potype => 'a potype" |
|
101 |
"dual po == (| pset = po.<A>, order = converse (po.<r>) |)" |
|
102 |
||
103 |
locale PO = |
|
104 |
fixes |
|
105 |
cl :: "'a potype" |
|
106 |
A :: "'a set" |
|
107 |
r :: "('a * 'a) set" |
|
108 |
assumes |
|
109 |
cl_po "cl : PartialOrder" |
|
110 |
defines |
|
111 |
A_def "A == cl.<A>" |
|
112 |
r_def "r == cl.<r>" |
|
113 |
||
114 |
locale CL = PO + |
|
115 |
fixes |
|
116 |
assumes |
|
117 |
cl_co "cl : CompleteLattice" |
|
118 |
||
119 |
locale CLF = CL + |
|
120 |
fixes |
|
121 |
f :: "'a => 'a" |
|
122 |
P :: "'a set" |
|
123 |
assumes |
|
10834 | 124 |
f_cl "f : CLF``{cl}" |
7112 | 125 |
defines |
126 |
P_def "P == fix f A" |
|
127 |
||
128 |
||
129 |
locale Tarski = CLF + |
|
130 |
fixes |
|
131 |
Y :: "'a set" |
|
132 |
intY1 :: "'a set" |
|
133 |
v :: "'a" |
|
134 |
assumes |
|
135 |
Y_ss "Y <= P" |
|
136 |
defines |
|
137 |
intY1_def "intY1 == interval r (lub Y cl) (Top cl)" |
|
12459
6978ab7cac64
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
wenzelm
parents:
10834
diff
changeset
|
138 |
v_def "v == glb {x. ((%x: intY1. f x) x, x): induced intY1 r & x: intY1} |
7112 | 139 |
(| pset=intY1, order=induced intY1 r|)" |
140 |
||
141 |
end |