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 


9 
ZF = FOL +


10 


11 
types

615

12 
i

0

13 


14 
arities


15 
i :: term


16 


17 
consts


18 

615

19 
"0" :: "i" ("0") (*the empty set*)


20 
Pow :: "i => i" (*power sets*)


21 
Inf :: "i" (*infinite set*)

0

22 


23 
(* Bounded Quantifiers *)


24 

615

25 
Ball, Bex :: "[i, i => o] => o"

0

26 


27 
(* General Union and Intersection *)


28 

80

29 
Union, Inter :: "i => i"

0

30 


31 
(* Variations on Replacement *)


32 

80

33 
PrimReplace :: "[i, [i, i] => o] => i"


34 
Replace :: "[i, [i, i] => o] => i"


35 
RepFun :: "[i, i => i] => i"


36 
Collect :: "[i, i => o] => i"

0

37 


38 
(* Descriptions *)


39 

615

40 
The :: "(i => o) => i" (binder "THE " 10)

80

41 
if :: "[o, i, i] => i"

0

42 


43 
(* Finite Sets *)


44 

80

45 
Upair, cons :: "[i, i] => i"


46 
succ :: "i => i"

0

47 

615

48 
(* Ordered Pairing *)

0

49 

80

50 
Pair :: "[i, i] => i"


51 
fst, snd :: "i => i"


52 
split :: "[[i, i] => i, i] => i"


53 
fsplit :: "[[i, i] => o, i] => o"

0

54 


55 
(* Sigma and Pi Operators *)


56 

615

57 
Sigma, Pi :: "[i, i => i] => i"

0

58 


59 
(* Relations and Functions *)


60 

80

61 
domain :: "i => i"


62 
range :: "i => i"


63 
field :: "i => i"


64 
converse :: "i => i"


65 
Lambda :: "[i, i => i] => i"


66 
restrict :: "[i, i] => i"

0

67 


68 
(* Infixes in order of decreasing precedence *)


69 

615

70 
"``" :: "[i, i] => i" (infixl 90) (*image*)


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


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


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


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


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


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


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


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


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


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

0

81 


82 

615

83 
types


84 
is


85 


86 
syntax


87 
"" :: "i => is" ("_")


88 
"@Enum" :: "[i, is] => is" ("_,/ _")


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


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


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


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


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


94 
"@RepFun" :: "[i, idt, i] => i" ("(1{_ ./ _: _})")


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


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


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


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


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


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


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


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


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


104 

0

105 
translations

615

106 
"x ~: y" == "~ (x : y)"

0

107 
"{x, xs}" == "cons(x, {xs})"


108 
"{x}" == "cons(x, 0)"

49

109 
"<x, y, z>" == "<x, <y, z>>"


110 
"<x, y>" == "Pair(x, y)"

0

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


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

615

113 
"{b. x:A}" == "RepFun(A, %x. b)"

0

114 
"INT x:A. B" == "Inter({B. x:A})"


115 
"UN x:A. B" == "Union({B. x:A})"


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


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

49

118 
"A > B" => "Pi(A, _K(B))"


119 
"A * B" => "Sigma(A, _K(B))"

0

120 
"lam x:A. f" == "Lambda(A, %x. f)"


121 
"ALL x:A. P" == "Ball(A, %x. P)"


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

37

123 

0

124 


125 
rules


126 

615

127 
(* Bounded Quantifiers *)


128 


129 
Ball_def "Ball(A, P) == ALL x. x:A > P(x)"


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


131 
subset_def "A <= B == ALL x:A. x:B"

0

132 

615

133 
(* ZF axioms  see Suppes p.238


134 
Axioms for Union, Pow and Replace state existence only,


135 
uniqueness is derivable using extensionality. *)

0

136 

615

137 
extension "A = B <> A <= B & B <= A"


138 
Union_iff "A : Union(C) <> (EX B:C. A:B)"


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


140 
succ_def "succ(i) == cons(i, i)"

0

141 

615

142 
(*We may name this set, though it is not uniquely defined.*)


143 
infinity "0:Inf & (ALL y:Inf. succ(y): Inf)"

0

144 

615

145 
(*This formulation facilitates case analysis on A.*)


146 
foundation "A=0  (EX x:A. ALL y:x. y~:A)"

0

147 

615

148 
(*Schema axiom since predicate P is a higherorder variable*)


149 
replacement "(ALL x:A. ALL y z. P(x,y) & P(x,z) > y=z) ==> \


150 
\ b : PrimReplace(A,P) <> (EX x:A. P(x,b))"


151 


152 
(* Derived form of replacement, restricting P to its functional part.


153 
The resulting set (for functional P) is the same as with


154 
PrimReplace, but the rules are simpler. *)

0

155 

615

156 
Replace_def "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"


157 


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

0

159 

615

160 
RepFun_def "RepFun(A,f) == {y . x:A, y=f(x)}"

0

161 

615

162 
(* Separation and Pairing can be derived from the Replacement


163 
and Powerset Axioms using the following definitions. *)

0

164 

615

165 
Collect_def "Collect(A,P) == {y . x:A, x=y & P(x)}"

0

166 

615

167 
(*Unordered pairs (Upair) express binary union/intersection and cons;


168 
set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)

0

169 

615

170 
Upair_def "Upair(a,b) == {y. x:Pow(Pow(0)), (x=0 & y=a)  (x=Pow(0) & y=b)}"


171 
cons_def "cons(a,A) == Upair(a,a) Un A"


172 


173 
(* Difference, general intersection, binary union and small intersection *)

0

174 

615

175 
Diff_def "A  B == { x:A . ~(x:B) }"


176 
Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}"


177 
Un_def "A Un B == Union(Upair(A,B))"


178 
Int_def "A Int B == Inter(Upair(A,B))"

0

179 

615

180 
(* Definite descriptions  via Replace over the set "1" *)

0

181 

615

182 
the_def "The(P) == Union({y . x:{0}, P(y)})"


183 
if_def "if(P,a,b) == THE z. P & z=a  ~P & z=b"

0

184 

615

185 
(* Ordered pairs and disjoint union of a family of sets *)

0

186 

615

187 
(* this "symmetric" definition works better than {{a}, {a,b}} *)


188 
Pair_def "<a,b> == {{a,a}, {a,b}}"


189 
fst_def "fst == split(%x y.x)"


190 
snd_def "snd == split(%x y.y)"


191 
split_def "split(c,p) == THE y. EX a b. p=<a,b> & y=c(a,b)"


192 
fsplit_def "fsplit(R,z) == EX x y. z=<x,y> & R(x,y)"


193 
Sigma_def "Sigma(A,B) == UN x:A. UN y:B(x). {<x,y>}"

0

194 

615

195 
(* Operations on relations *)

0

196 

615

197 
(*converse of relation r, inverse of function*)


198 
converse_def "converse(r) == {z. w:r, EX x y. w=<x,y> & z=<y,x>}"

0

199 

615

200 
domain_def "domain(r) == {x. w:r, EX y. w=<x,y>}"


201 
range_def "range(r) == domain(converse(r))"


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


203 
image_def "r `` A == {y : range(r) . EX x:A. <x,y> : r}"


204 
vimage_def "r `` A == converse(r)``A"

0

205 

615

206 
(* Abstraction, application and Cartesian product of a family of sets *)

0

207 

615

208 
lam_def "Lambda(A,b) == {<x,b(x)> . x:A}"


209 
apply_def "f`a == THE y. <a,y> : f"


210 
Pi_def "Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}"

0

211 


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

615

213 
restrict_def "restrict(f,A) == lam x:A.f`x"

0

214 


215 
end


216 


217 


218 
ML


219 


220 
(* 'Dependent' type operators *)


221 


222 
val print_translation =

516

223 
[("Pi", dependent_tr' ("@PROD", ">")),


224 
("Sigma", dependent_tr' ("@SUM", "*"))];
