author | paulson |
Mon, 13 May 2002 13:22:15 +0200 | |
changeset 13144 | c5ae1522fb82 |
parent 13121 | 4888694b2829 |
child 13175 | 81082cfa5618 |
permissions | -rw-r--r-- |
615 | 1 |
(* Title: ZF/ZF.thy |
0 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
13108 | 9 |
ZF = Let + |
0 | 10 |
|
3906 | 11 |
global |
12 |
||
0 | 13 |
types |
615 | 14 |
i |
0 | 15 |
|
16 |
arities |
|
13144 | 17 |
i :: "term" |
0 | 18 |
|
19 |
consts |
|
20 |
||
13144 | 21 |
"0" :: "i" ("0") (*the empty set*) |
22 |
Pow :: "i => i" (*power sets*) |
|
23 |
Inf :: "i" (*infinite set*) |
|
0 | 24 |
|
25 |
(* Bounded Quantifiers *) |
|
26 |
||
13144 | 27 |
Ball, Bex :: "[i, i => o] => o" |
0 | 28 |
|
29 |
(* General Union and Intersection *) |
|
30 |
||
13144 | 31 |
Union,Inter :: "i => i" |
0 | 32 |
|
33 |
(* Variations on Replacement *) |
|
34 |
||
13144 | 35 |
PrimReplace :: "[i, [i, i] => o] => i" |
36 |
Replace :: "[i, [i, i] => o] => i" |
|
37 |
RepFun :: "[i, i => i] => i" |
|
38 |
Collect :: "[i, i => o] => i" |
|
0 | 39 |
|
40 |
(* Descriptions *) |
|
41 |
||
1401 | 42 |
The :: (i => o) => i (binder "THE " 10) |
13144 | 43 |
If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10) |
6068 | 44 |
|
45 |
syntax |
|
13144 | 46 |
old_if :: "[o, i, i] => i" ("if '(_,_,_')") |
0 | 47 |
|
6068 | 48 |
translations |
49 |
"if(P,a,b)" => "If(P,a,b)" |
|
50 |
||
51 |
||
52 |
consts |
|
0 | 53 |
(* Finite Sets *) |
54 |
||
13144 | 55 |
Upair, cons :: "[i, i] => i" |
56 |
succ :: "i => i" |
|
0 | 57 |
|
615 | 58 |
(* Ordered Pairing *) |
0 | 59 |
|
13144 | 60 |
Pair :: "[i, i] => i" |
61 |
fst, snd :: "i => i" |
|
62 |
split :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) |
|
0 | 63 |
|
64 |
(* Sigma and Pi Operators *) |
|
65 |
||
13144 | 66 |
Sigma, Pi :: "[i, i => i] => i" |
0 | 67 |
|
68 |
(* Relations and Functions *) |
|
69 |
||
13144 | 70 |
domain :: "i => i" |
71 |
range :: "i => i" |
|
72 |
field :: "i => i" |
|
73 |
converse :: "i => i" |
|
74 |
relation :: "i => o" (*recognizes sets of pairs*) |
|
75 |
function :: "i => o" (*recognizes functions; can have non-pairs*) |
|
76 |
Lambda :: "[i, i => i] => i" |
|
77 |
restrict :: "[i, i] => i" |
|
0 | 78 |
|
79 |
(* Infixes in order of decreasing precedence *) |
|
80 |
||
13144 | 81 |
"``" :: "[i, i] => i" (infixl 90) (*image*) |
82 |
"-``" :: "[i, i] => i" (infixl 90) (*inverse image*) |
|
83 |
"`" :: "[i, i] => i" (infixl 90) (*function application*) |
|
84 |
(*"*" :: "[i, i] => i" (infixr 80) (*Cartesian product*)*) |
|
85 |
"Int" :: "[i, i] => i" (infixl 70) (*binary intersection*) |
|
86 |
"Un" :: "[i, i] => i" (infixl 65) (*binary union*) |
|
87 |
"-" :: "[i, i] => i" (infixl 65) (*set difference*) |
|
88 |
(*"->" :: "[i, i] => i" (infixr 60) (*function space*)*) |
|
89 |
"<=" :: "[i, i] => o" (infixl 50) (*subset relation*) |
|
90 |
":" :: "[i, i] => o" (infixl 50) (*membership relation*) |
|
91 |
(*"~:" :: "[i, i] => o" (infixl 50) (*negated membership relation*)*) |
|
0 | 92 |
|
93 |
||
615 | 94 |
types |
95 |
is |
|
3692 | 96 |
patterns |
615 | 97 |
|
98 |
syntax |
|
13144 | 99 |
"" :: "i => is" ("_") |
100 |
"@Enum" :: "[i, is] => is" ("_,/ _") |
|
101 |
"~:" :: "[i, i] => o" (infixl 50) |
|
102 |
"@Finset" :: "is => i" ("{(_)}") |
|
103 |
"@Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
|
104 |
"@Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") |
|
105 |
"@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") |
|
106 |
"@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) |
|
107 |
"@INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) |
|
108 |
"@UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) |
|
109 |
"@PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) |
|
110 |
"@SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) |
|
111 |
"->" :: "[i, i] => i" (infixr 60) |
|
112 |
"*" :: "[i, i] => i" (infixr 80) |
|
113 |
"@lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) |
|
114 |
"@Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) |
|
115 |
"@Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
116 |
|
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
117 |
(** Patterns -- extends pre-defined type "pttrn" used in abstractions **) |
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
118 |
|
13144 | 119 |
"@pattern" :: "patterns => pttrn" ("<_>") |
120 |
"" :: "pttrn => patterns" ("_") |
|
121 |
"@patterns" :: "[pttrn, patterns] => patterns" ("_,/_") |
|
615 | 122 |
|
0 | 123 |
translations |
615 | 124 |
"x ~: y" == "~ (x : y)" |
0 | 125 |
"{x, xs}" == "cons(x, {xs})" |
126 |
"{x}" == "cons(x, 0)" |
|
127 |
"{x:A. P}" == "Collect(A, %x. P)" |
|
128 |
"{y. x:A, Q}" == "Replace(A, %x y. Q)" |
|
615 | 129 |
"{b. x:A}" == "RepFun(A, %x. b)" |
0 | 130 |
"INT x:A. B" == "Inter({B. x:A})" |
131 |
"UN x:A. B" == "Union({B. x:A})" |
|
132 |
"PROD x:A. B" => "Pi(A, %x. B)" |
|
133 |
"SUM x:A. B" => "Sigma(A, %x. B)" |
|
49 | 134 |
"A -> B" => "Pi(A, _K(B))" |
135 |
"A * B" => "Sigma(A, _K(B))" |
|
0 | 136 |
"lam x:A. f" == "Lambda(A, %x. f)" |
137 |
"ALL x:A. P" == "Ball(A, %x. P)" |
|
138 |
"EX x:A. P" == "Bex(A, %x. P)" |
|
37 | 139 |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
140 |
"<x, y, z>" == "<x, <y, z>>" |
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
141 |
"<x, y>" == "Pair(x, y)" |
2286 | 142 |
"%<x,y,zs>.b" == "split(%x <y,zs>.b)" |
3840 | 143 |
"%<x,y>.b" == "split(%x y. b)" |
2286 | 144 |
|
0 | 145 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11322
diff
changeset
|
146 |
syntax (xsymbols) |
13144 | 147 |
"op *" :: "[i, i] => i" (infixr "\\<times>" 80) |
148 |
"op Int" :: "[i, i] => i" (infixl "\\<inter>" 70) |
|
149 |
"op Un" :: "[i, i] => i" (infixl "\\<union>" 65) |
|
150 |
"op ->" :: "[i, i] => i" (infixr "\\<rightarrow>" 60) |
|
151 |
"op <=" :: "[i, i] => o" (infixl "\\<subseteq>" 50) |
|
152 |
"op :" :: "[i, i] => o" (infixl "\\<in>" 50) |
|
153 |
"op ~:" :: "[i, i] => o" (infixl "\\<notin>" 50) |
|
154 |
"@Collect" :: "[pttrn, i, o] => i" ("(1{_ \\<in> _ ./ _})") |
|
155 |
"@Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \\<in> _, _})") |
|
156 |
"@RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \\<in> _})" [51,0,51]) |
|
157 |
"@UNION" :: "[pttrn, i, i] => i" ("(3\\<Union>_\\<in>_./ _)" 10) |
|
158 |
"@INTER" :: "[pttrn, i, i] => i" ("(3\\<Inter>_\\<in>_./ _)" 10) |
|
159 |
Union :: "i =>i" ("\\<Union>_" [90] 90) |
|
160 |
Inter :: "i =>i" ("\\<Inter>_" [90] 90) |
|
161 |
"@PROD" :: "[pttrn, i, i] => i" ("(3\\<Pi>_\\<in>_./ _)" 10) |
|
162 |
"@SUM" :: "[pttrn, i, i] => i" ("(3\\<Sigma>_\\<in>_./ _)" 10) |
|
163 |
"@lam" :: "[pttrn, i, i] => i" ("(3\\<lambda>_\\<in>_./ _)" 10) |
|
164 |
"@Ball" :: "[pttrn, i, o] => o" ("(3\\<forall>_\\<in>_./ _)" 10) |
|
165 |
"@Bex" :: "[pttrn, i, o] => o" ("(3\\<exists>_\\<in>_./ _)" 10) |
|
166 |
"@Tuple" :: "[i, is] => i" ("\\<langle>(_,/ _)\\<rangle>") |
|
167 |
"@pattern" :: "patterns => pttrn" ("\\<langle>_\\<rangle>") |
|
2540 | 168 |
|
6340 | 169 |
syntax (HTML output) |
13144 | 170 |
"op *" :: "[i, i] => i" (infixr "\\<times>" 80) |
6340 | 171 |
|
2540 | 172 |
|
690 | 173 |
defs |
0 | 174 |
|
615 | 175 |
(* Bounded Quantifiers *) |
176 |
Ball_def "Ball(A, P) == ALL x. x:A --> P(x)" |
|
177 |
Bex_def "Bex(A, P) == EX x. x:A & P(x)" |
|
690 | 178 |
|
615 | 179 |
subset_def "A <= B == ALL x:A. x:B" |
690 | 180 |
succ_def "succ(i) == cons(i, i)" |
181 |
||
3906 | 182 |
|
3940 | 183 |
local |
3906 | 184 |
|
690 | 185 |
rules |
0 | 186 |
|
615 | 187 |
(* ZF axioms -- see Suppes p.238 |
188 |
Axioms for Union, Pow and Replace state existence only, |
|
189 |
uniqueness is derivable using extensionality. *) |
|
0 | 190 |
|
615 | 191 |
extension "A = B <-> A <= B & B <= A" |
192 |
Union_iff "A : Union(C) <-> (EX B:C. A:B)" |
|
193 |
Pow_iff "A : Pow(B) <-> A <= B" |
|
0 | 194 |
|
615 | 195 |
(*We may name this set, though it is not uniquely defined.*) |
196 |
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)" |
|
0 | 197 |
|
615 | 198 |
(*This formulation facilitates case analysis on A.*) |
199 |
foundation "A=0 | (EX x:A. ALL y:x. y~:A)" |
|
0 | 200 |
|
615 | 201 |
(*Schema axiom since predicate P is a higher-order variable*) |
12762 | 202 |
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) --> y=z) ==> |
1155 | 203 |
b : PrimReplace(A,P) <-> (EX x:A. P(x,b))" |
615 | 204 |
|
690 | 205 |
defs |
206 |
||
615 | 207 |
(* Derived form of replacement, restricting P to its functional part. |
208 |
The resulting set (for functional P) is the same as with |
|
209 |
PrimReplace, but the rules are simpler. *) |
|
0 | 210 |
|
3840 | 211 |
Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" |
615 | 212 |
|
213 |
(* Functional form of replacement -- analgous to ML's map functional *) |
|
0 | 214 |
|
615 | 215 |
RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}" |
0 | 216 |
|
615 | 217 |
(* Separation and Pairing can be derived from the Replacement |
218 |
and Powerset Axioms using the following definitions. *) |
|
0 | 219 |
|
615 | 220 |
Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}" |
0 | 221 |
|
615 | 222 |
(*Unordered pairs (Upair) express binary union/intersection and cons; |
223 |
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) |
|
0 | 224 |
|
615 | 225 |
Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" |
226 |
cons_def "cons(a,A) == Upair(a,a) Un A" |
|
227 |
||
2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
228 |
(* Difference, general intersection, binary union and small intersection *) |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
229 |
|
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
230 |
Diff_def "A - B == { x:A . ~(x:B) }" |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
231 |
Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}" |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
232 |
Un_def "A Un B == Union(Upair(A,B))" |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
233 |
Int_def "A Int B == Inter(Upair(A,B))" |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
234 |
|
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
235 |
(* Definite descriptions -- via Replace over the set "1" *) |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
236 |
|
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
237 |
the_def "The(P) == Union({y . x:{0}, P(y)})" |
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset
|
238 |
if_def "if(P,a,b) == THE z. P & z=a | ~P & z=b" |
0 | 239 |
|
615 | 240 |
(* this "symmetric" definition works better than {{a}, {a,b}} *) |
241 |
Pair_def "<a,b> == {{a,a}, {a,b}}" |
|
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
242 |
fst_def "fst(p) == THE a. EX b. p=<a,b>" |
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
243 |
snd_def "snd(p) == THE b. EX a. p=<a,b>" |
12762 | 244 |
split_def "split(c) == %p. c(fst(p), snd(p))" |
615 | 245 |
Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}" |
0 | 246 |
|
615 | 247 |
(* Operations on relations *) |
0 | 248 |
|
615 | 249 |
(*converse of relation r, inverse of function*) |
250 |
converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}" |
|
0 | 251 |
|
615 | 252 |
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}" |
253 |
range_def "range(r) == domain(converse(r))" |
|
254 |
field_def "field(r) == domain(r) Un range(r)" |
|
13121 | 255 |
relation_def "relation(r) == ALL z:r. EX x y. z = <x,y>" |
256 |
function_def "function(r) == |
|
257 |
ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')" |
|
615 | 258 |
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}" |
259 |
vimage_def "r -`` A == converse(r)``A" |
|
0 | 260 |
|
615 | 261 |
(* Abstraction, application and Cartesian product of a family of sets *) |
0 | 262 |
|
615 | 263 |
lam_def "Lambda(A,b) == {<x,b(x)> . x:A}" |
264 |
apply_def "f`a == THE y. <a,y> : f" |
|
690 | 265 |
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" |
0 | 266 |
|
12891 | 267 |
(* Restrict the relation r to the domain A *) |
268 |
restrict_def "restrict(r,A) == {z : r. EX x:A. EX y. z = <x,y>}" |
|
0 | 269 |
|
270 |
end |
|
271 |
||
272 |
||
273 |
ML |
|
274 |
||
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
275 |
(* Pattern-matching and 'Dependent' type operators *) |
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
276 |
|
12762 | 277 |
val print_translation = |
1116 | 278 |
[(*("split", split_tr'),*) |
1106
62bdb9e5722b
Added pattern-matching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset
|
279 |
("Pi", dependent_tr' ("@PROD", "op ->")), |
632 | 280 |
("Sigma", dependent_tr' ("@SUM", "op *"))]; |