author  wenzelm 
Thu, 16 Oct 1997 15:33:06 +0200  
changeset 3906  5ae0e1324c56 
parent 3840  e0baea4d485a 
child 3940  1d5bee4d047f 
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) 
43 
if :: [o, i, i] => i 

0  44 

45 
(* Finite Sets *) 

46 

1401  47 
Upair, cons :: [i, i] => i 
48 
succ :: i => i 

0  49 

615  50 
(* Ordered Pairing *) 
0  51 

1401  52 
Pair :: [i, i] => i 
53 
fst, snd :: i => i 

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

0  55 

56 
(* Sigma and Pi Operators *) 

57 

1401  58 
Sigma, Pi :: [i, i => i] => i 
0  59 

60 
(* Relations and Functions *) 

61 

1401  62 
domain :: i => i 
63 
range :: i => i 

64 
field :: i => i 

65 
converse :: i => i 

1478  66 
function :: i => o (*is a relation a function?*) 
1401  67 
Lambda :: [i, i => i] => i 
68 
restrict :: [i, i] => i 

0  69 

70 
(* Infixes in order of decreasing precedence *) 

71 

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

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

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

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

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

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

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

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

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

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

0  83 

84 

615  85 
types 
86 
is 

3692  87 
patterns 
615  88 

89 
syntax 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

107 

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

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

109 

3692  110 
"@pattern" :: patterns => pttrn ("<_>") 
111 
"" :: pttrn => patterns ("_") 

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

615  113 

0  114 
translations 
615  115 
"x ~: y" == "~ (x : y)" 
0  116 
"{x, xs}" == "cons(x, {xs})" 
117 
"{x}" == "cons(x, 0)" 

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

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

615  120 
"{b. x:A}" == "RepFun(A, %x. b)" 
0  121 
"INT x:A. B" == "Inter({B. x:A})" 
122 
"UN x:A. B" == "Union({B. x:A})" 

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

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

49  125 
"A > B" => "Pi(A, _K(B))" 
126 
"A * B" => "Sigma(A, _K(B))" 

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

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

37  130 

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

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

132 
"<x, y>" == "Pair(x, y)" 
2286  133 
"%<x,y,zs>.b" == "split(%x <y,zs>.b)" 
3840  134 
"%<x,y>.b" == "split(%x y. b)" 
2286  135 

0  136 

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

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

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

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

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

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

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

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

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

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

148 
"@INTER" :: [pttrn, i, i] => i ("(3\\<Inter> _\\<in>_./ _)" 10) 

149 
"@UNION" :: [pttrn, i, i] => i ("(3\\<Union> _\\<in>_./ _)" 10) 

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

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

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

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

3068
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3065
diff
changeset

154 
(* 
3065  155 
"@Tuple" :: [i, is] => i ("\\<langle>(_,/ _)\\<rangle>") 
3692  156 
"@pattern" :: patterns => pttrn ("\\<langle>_\\<rangle>") 
3068
b7562e452816
deactivated new symbols (not yet printable on xterm, emacs);
wenzelm
parents:
3065
diff
changeset

157 
*) 
2540  158 

159 

690  160 
defs 
0  161 

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

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

690  165 

615  166 
subset_def "A <= B == ALL x:A. x:B" 
690  167 
succ_def "succ(i) == cons(i, i)" 
168 

3906  169 

170 
path ZF 

171 

690  172 
rules 
0  173 

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

176 
uniqueness is derivable using extensionality. *) 

0  177 

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

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

0  181 

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

0  184 

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

0  187 

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

615  191 

690  192 
defs 
193 

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

196 
PrimReplace, but the rules are simpler. *) 

0  197 

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

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

0  201 

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

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

0  206 

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

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

0  211 

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

214 

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

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

216 

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

217 
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

218 
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

219 
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

220 
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

221 

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

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

223 

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

224 
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

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

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

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

229 
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

230 
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

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

615  234 
(* Operations on relations *) 
0  235 

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

0  238 

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

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

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

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

0  246 

615  247 
(* Abstraction, application and Cartesian product of a family of sets *) 
0  248 

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

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

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

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

256 
end 

257 

258 

259 
ML 

260 

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

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

262 

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

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

265 
("Pi", dependent_tr' ("@PROD", "op >")), 
632  266 
("Sigma", dependent_tr' ("@SUM", "op *"))]; 
2469  267 