|
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 |
|
97 "S <<= cl" == "S : sublattice ^^ {cl}" |
|
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 |
|
124 f_cl "f : CLF ^^{cl}" |
|
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)" |
|
138 v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1} |
|
139 (| pset=intY1, order=induced intY1 r|)" |
|
140 |
|
141 end |