author  wenzelm 
Fri, 15 Sep 2000 00:19:52 +0200  
changeset 9965  1971c8dd0971 
parent 9683  f87c8c449018 
child 11233  34c81a796ee3 
permissions  rwrr 
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 
ZermeloFraenkel Set Theory 

7 
*) 

8 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

9 
ZF = FOL + Let + 
0  10 

3906  11 
global 
12 

0  13 
types 
615  14 
i 
0  15 

16 
arities 

17 
i :: term 

18 

19 
consts 

20 

1401  21 
"0" :: i ("0") (*the empty set*) 
22 
Pow :: i => i (*power sets*) 

23 
Inf :: i (*infinite set*) 

0  24 

25 
(* Bounded Quantifiers *) 

26 

1401  27 
Ball, Bex :: [i, i => o] => o 
0  28 

29 
(* General Union and Intersection *) 

30 

1401  31 
Union,Inter :: i => i 
0  32 

33 
(* Variations on Replacement *) 

34 

1401  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) 
6068  43 
If :: [o, i, i] => i ("(if (_)/ then (_)/ else (_))" [10] 10) 
44 

45 
syntax 

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 

1401  55 
Upair, cons :: [i, i] => i 
56 
succ :: i => i 

0  57 

615  58 
(* Ordered Pairing *) 
0  59 

1401  60 
Pair :: [i, i] => i 
61 
fst, snd :: i => i 

62 
split :: [[i, i] => 'a, i] => 'a::logic (*for patternmatching*) 

0  63 

64 
(* Sigma and Pi Operators *) 

65 

1401  66 
Sigma, Pi :: [i, i => i] => i 
0  67 

68 
(* Relations and Functions *) 

69 

1401  70 
domain :: i => i 
71 
range :: i => i 

72 
field :: i => i 

73 
converse :: i => i 

1478  74 
function :: i => o (*is a relation a function?*) 
1401  75 
Lambda :: [i, i => i] => i 
76 
restrict :: [i, i] => i 

0  77 

78 
(* Infixes in order of decreasing precedence *) 

79 

1401  80 
"``" :: [i, i] => i (infixl 90) (*image*) 
81 
"``" :: [i, i] => i (infixl 90) (*inverse image*) 

82 
"`" :: [i, i] => i (infixl 90) (*function application*) 

83 
(*"*" :: [i, i] => i (infixr 80) (*Cartesian product*)*) 

84 
"Int" :: [i, i] => i (infixl 70) (*binary intersection*) 

85 
"Un" :: [i, i] => i (infixl 65) (*binary union*) 

86 
"" :: [i, i] => i (infixl 65) (*set difference*) 

87 
(*">" :: [i, i] => i (infixr 60) (*function space*)*) 

88 
"<=" :: [i, i] => o (infixl 50) (*subset relation*) 

89 
":" :: [i, i] => o (infixl 50) (*membership relation*) 

90 
(*"~:" :: [i, i] => o (infixl 50) (*negated membership relation*)*) 

0  91 

92 

615  93 
types 
94 
is 

3692  95 
patterns 
615  96 

97 
syntax 

1401  98 
"" :: i => is ("_") 
99 
"@Enum" :: [i, is] => is ("_,/ _") 

100 
"~:" :: [i, i] => o (infixl 50) 

101 
"@Finset" :: is => i ("{(_)}") 

102 
"@Tuple" :: [i, is] => i ("<(_,/ _)>") 

103 
"@Collect" :: [pttrn, i, o] => i ("(1{_: _ ./ _})") 

104 
"@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})") 

105 
"@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _: _})" [51,0,51]) 

106 
"@INTER" :: [pttrn, i, i] => i ("(3INT _:_./ _)" 10) 

107 
"@UNION" :: [pttrn, i, i] => i ("(3UN _:_./ _)" 10) 

108 
"@PROD" :: [pttrn, i, i] => i ("(3PROD _:_./ _)" 10) 

109 
"@SUM" :: [pttrn, i, i] => i ("(3SUM _:_./ _)" 10) 

110 
">" :: [i, i] => i (infixr 60) 

111 
"*" :: [i, i] => i (infixr 80) 

112 
"@lam" :: [pttrn, i, i] => i ("(3lam _:_./ _)" 10) 

113 
"@Ball" :: [pttrn, i, o] => o ("(3ALL _:_./ _)" 10) 

114 
"@Bex" :: [pttrn, i, o] => o ("(3EX _:_./ _)" 10) 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

115 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

116 
(** Patterns  extends predefined type "pttrn" used in abstractions **) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

117 

3692  118 
"@pattern" :: patterns => pttrn ("<_>") 
119 
"" :: pttrn => patterns ("_") 

120 
"@patterns" :: [pttrn, patterns] => patterns ("_,/_") 

615  121 

0  122 
translations 
615  123 
"x ~: y" == "~ (x : y)" 
0  124 
"{x, xs}" == "cons(x, {xs})" 
125 
"{x}" == "cons(x, 0)" 

126 
"{x:A. P}" == "Collect(A, %x. P)" 

127 
"{y. x:A, Q}" == "Replace(A, %x y. Q)" 

615  128 
"{b. x:A}" == "RepFun(A, %x. b)" 
0  129 
"INT x:A. B" == "Inter({B. x:A})" 
130 
"UN x:A. B" == "Union({B. x:A})" 

131 
"PROD x:A. B" => "Pi(A, %x. B)" 

132 
"SUM x:A. B" => "Sigma(A, %x. B)" 

49  133 
"A > B" => "Pi(A, _K(B))" 
134 
"A * B" => "Sigma(A, _K(B))" 

0  135 
"lam x:A. f" == "Lambda(A, %x. f)" 
136 
"ALL x:A. P" == "Ball(A, %x. P)" 

137 
"EX x:A. P" == "Bex(A, %x. P)" 

37  138 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

139 
"<x, y, z>" == "<x, <y, z>>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

140 
"<x, y>" == "Pair(x, y)" 
2286  141 
"%<x,y,zs>.b" == "split(%x <y,zs>.b)" 
3840  142 
"%<x,y>.b" == "split(%x y. b)" 
2286  143 

0  144 

2540  145 
syntax (symbols) 
146 
"op *" :: [i, i] => i (infixr "\\<times>" 80) 

147 
"op Int" :: [i, i] => i (infixl "\\<inter>" 70) 

148 
"op Un" :: [i, i] => i (infixl "\\<union>" 65) 

149 
"op >" :: [i, i] => i (infixr "\\<rightarrow>" 60) 

150 
"op <=" :: [i, i] => o (infixl "\\<subseteq>" 50) 

151 
"op :" :: [i, i] => o (infixl "\\<in>" 50) 

152 
"op ~:" :: [i, i] => o (infixl "\\<notin>" 50) 

153 
"@Collect" :: [pttrn, i, o] => i ("(1{_\\<in> _ ./ _})") 

154 
"@Replace" :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _\\<in> _, _})") 

155 
"@RepFun" :: [i, pttrn, i] => i ("(1{_ ./ _\\<in> _})" [51,0,51]) 

9965  156 
"@INTER" :: [pttrn, i, i] => i ("(3\\<Inter>_\\<in>_./ _)" 10) 
157 
"@UNION" :: [pttrn, i, i] => i ("(3\\<Union>_\\<in>_./ _)" 10) 

158 
"@PROD" :: [pttrn, i, i] => i ("(3\\<Pi>_\\<in>_./ _)" 10) 

159 
"@SUM" :: [pttrn, i, i] => i ("(3\\<Sigma>_\\<in>_./ _)" 10) 

160 
"@lam" :: [pttrn, i, i] => i ("(3\\<lambda>_:_./ _)" 10) 

161 
"@Ball" :: [pttrn, i, o] => o ("(3\\<forall>_\\<in>_./ _)" 10) 

162 
"@Bex" :: [pttrn, i, o] => o ("(3\\<exists>_\\<in>_./ _)" 10) 

163 

164 
syntax (xsymbols) 

3065  165 
"@Tuple" :: [i, is] => i ("\\<langle>(_,/ _)\\<rangle>") 
3692  166 
"@pattern" :: patterns => pttrn ("\\<langle>_\\<rangle>") 
2540  167 

6340  168 
syntax (HTML output) 
169 
"op *" :: [i, i] => i (infixr "\\<times>" 80) 

170 

2540  171 

690  172 
defs 
0  173 

615  174 
(* Bounded Quantifiers *) 
175 
Ball_def "Ball(A, P) == ALL x. x:A > P(x)" 

176 
Bex_def "Bex(A, P) == EX x. x:A & P(x)" 

690  177 

615  178 
subset_def "A <= B == ALL x:A. x:B" 
690  179 
succ_def "succ(i) == cons(i, i)" 
180 

3906  181 

3940  182 
local 
3906  183 

690  184 
rules 
0  185 

615  186 
(* ZF axioms  see Suppes p.238 
187 
Axioms for Union, Pow and Replace state existence only, 

188 
uniqueness is derivable using extensionality. *) 

0  189 

615  190 
extension "A = B <> A <= B & B <= A" 
191 
Union_iff "A : Union(C) <> (EX B:C. A:B)" 

192 
Pow_iff "A : Pow(B) <> A <= B" 

0  193 

615  194 
(*We may name this set, though it is not uniquely defined.*) 
195 
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)" 

0  196 

615  197 
(*This formulation facilitates case analysis on A.*) 
198 
foundation "A=0  (EX x:A. ALL y:x. y~:A)" 

0  199 

615  200 
(*Schema axiom since predicate P is a higherorder variable*) 
1155  201 
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) > y=z) ==> 
202 
b : PrimReplace(A,P) <> (EX x:A. P(x,b))" 

615  203 

690  204 
defs 
205 

615  206 
(* Derived form of replacement, restricting P to its functional part. 
207 
The resulting set (for functional P) is the same as with 

208 
PrimReplace, but the rules are simpler. *) 

0  209 

3840  210 
Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" 
615  211 

212 
(* Functional form of replacement  analgous to ML's map functional *) 

0  213 

615  214 
RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}" 
0  215 

615  216 
(* Separation and Pairing can be derived from the Replacement 
217 
and Powerset Axioms using the following definitions. *) 

0  218 

615  219 
Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}" 
0  220 

615  221 
(*Unordered pairs (Upair) express binary union/intersection and cons; 
222 
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) 

0  223 

615  224 
Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)}" 
225 
cons_def "cons(a,A) == Upair(a,a) Un A" 

226 

2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

227 
(* 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

228 

ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

229 
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

230 
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

231 
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

232 
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

233 

ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

234 
(* 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

235 

ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2540
diff
changeset

236 
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

237 
if_def "if(P,a,b) == THE z. P & z=a  ~P & z=b" 
0  238 

615  239 
(* this "symmetric" definition works better than {{a}, {a,b}} *) 
240 
Pair_def "<a,b> == {{a,a}, {a,b}}" 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

241 
fst_def "fst(p) == THE a. EX b. p=<a,b>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

242 
snd_def "snd(p) == THE b. EX a. p=<a,b>" 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

243 
split_def "split(c,p) == c(fst(p), snd(p))" 
615  244 
Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}" 
0  245 

615  246 
(* Operations on relations *) 
0  247 

615  248 
(*converse of relation r, inverse of function*) 
249 
converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}" 

0  250 

615  251 
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}" 
252 
range_def "range(r) == domain(converse(r))" 

253 
field_def "field(r) == domain(r) Un range(r)" 

1478  254 
function_def "function(r) == ALL x y. <x,y>:r > 
255 
(ALL y'. <x,y'>:r > y=y')" 

615  256 
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}" 
257 
vimage_def "r `` A == converse(r)``A" 

0  258 

615  259 
(* Abstraction, application and Cartesian product of a family of sets *) 
0  260 

615  261 
lam_def "Lambda(A,b) == {<x,b(x)> . x:A}" 
262 
apply_def "f`a == THE y. <a,y> : f" 

690  263 
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" 
0  264 

265 
(* Restrict the function f to the domain A *) 

3840  266 
restrict_def "restrict(f,A) == lam x:A. f`x" 
0  267 

268 
end 

269 

270 

271 
ML 

272 

1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

273 
(* Patternmatching and 'Dependent' type operators *) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

274 

62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

275 
val print_translation = 
1116  276 
[(*("split", split_tr'),*) 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

277 
("Pi", dependent_tr' ("@PROD", "op >")), 
632  278 
("Sigma", dependent_tr' ("@SUM", "op *"))]; 
2469  279 