author  paulson 
Mon, 13 May 2002 13:22:15 +0200  
changeset 13144  c5ae1522fb82 
parent 13121  4888694b2829 
child 13175  81082cfa5618 
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 

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 patternmatching*) 

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 nonpairs*) 

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 patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

116 

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

117 
(** Patterns  extends predefined type "pttrn" used in abstractions **) 
62bdb9e5722b
Added patternmatching 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 patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

140 
"<x, y, z>" == "<x, <y, z>>" 
62bdb9e5722b
Added patternmatching 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 higherorder 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 patternmatching 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 patternmatching 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 patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

275 
(* Patternmatching and 'Dependent' type operators *) 
62bdb9e5722b
Added patternmatching 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 patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

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