author  clasohm 
Tue, 06 Feb 1996 12:27:17 +0100  
changeset 1478  2b8c2a7547ab 
parent 1401  0c439768f45c 
child 2286  c2f76a5bad65 
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 

11 
types 

615  12 
i 
0  13 

14 
arities 

15 
i :: term 

16 

17 
consts 

18 

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

21 
Inf :: i (*infinite set*) 

0  22 

23 
(* Bounded Quantifiers *) 

24 

1401  25 
Ball, Bex :: [i, i => o] => o 
0  26 

27 
(* General Union and Intersection *) 

28 

1401  29 
Union,Inter :: i => i 
0  30 

31 
(* Variations on Replacement *) 

32 

1401  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 

1401  40 
The :: (i => o) => i (binder "THE " 10) 
41 
if :: [o, i, i] => i 

0  42 

43 
(* Finite Sets *) 

44 

1401  45 
Upair, cons :: [i, i] => i 
46 
succ :: i => i 

0  47 

615  48 
(* Ordered Pairing *) 
0  49 

1401  50 
Pair :: [i, i] => i 
51 
fst, snd :: i => i 

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

0  53 

54 
(* Sigma and Pi Operators *) 

55 

1401  56 
Sigma, Pi :: [i, i => i] => i 
0  57 

58 
(* Relations and Functions *) 

59 

1401  60 
domain :: i => i 
61 
range :: i => i 

62 
field :: i => i 

63 
converse :: i => i 

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

0  67 

68 
(* Infixes in order of decreasing precedence *) 

69 

1401  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 

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

85 
pttrns 
615  86 

87 
syntax 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

105 

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

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

107 

1401  108 
"@pttrn" :: pttrns => pttrn ("<_>") 
109 
"" :: pttrn => pttrns ("_") 

110 
"@pttrns" :: [pttrn,pttrns] => pttrns ("_,/_") 

615  111 

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

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

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

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

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

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

49  123 
"A > B" => "Pi(A, _K(B))" 
124 
"A * B" => "Sigma(A, _K(B))" 

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

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

37  128 

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

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

130 
"<x, y>" == "Pair(x, y)" 
1116  131 
"%<x,y,zs>.b" == "split(%x <y,zs>.b)" 
132 
"%<x,y>.b" == "split(%x y.b)" 

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

133 
(* The <= direction fails if split has more than one argument because 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

134 
astmatching fails. Otherwise it would work fine *) 
0  135 

690  136 
defs 
0  137 

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

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

690  141 

615  142 
subset_def "A <= B == ALL x:A. x:B" 
690  143 
succ_def "succ(i) == cons(i, i)" 
144 

145 
rules 

0  146 

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

149 
uniqueness is derivable using extensionality. *) 

0  150 

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

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

0  154 

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

0  157 

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

0  160 

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

615  164 

690  165 
defs 
166 

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

169 
PrimReplace, but the rules are simpler. *) 

0  170 

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

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

0  174 

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

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

0  179 

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

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

0  184 

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

187 

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

0  189 

615  190 
Diff_def "A  B == { x:A . ~(x:B) }" 
191 
Inter_def "Inter(A) == { x:Union(A) . ALL y:A. x:y}" 

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

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

0  194 

615  195 
(* Definite descriptions  via Replace over the set "1" *) 
0  196 

615  197 
the_def "The(P) == Union({y . x:{0}, P(y)})" 
198 
if_def "if(P,a,b) == THE z. P & z=a  ~P & z=b" 

0  199 

615  200 
(* Ordered pairs and disjoint union of a family of sets *) 
0  201 

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

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

204 
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

205 
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

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

615  209 
(* Operations on relations *) 
0  210 

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

0  213 

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

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

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

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

0  221 

615  222 
(* Abstraction, application and Cartesian product of a family of sets *) 
0  223 

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

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

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

615  229 
restrict_def "restrict(f,A) == lam x:A.f`x" 
0  230 

231 
end 

232 

233 

234 
ML 

235 

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

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

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

239 

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

240 
fun pttrn s = const"@pttrn" $ s; 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

241 
fun pttrns s t = const"@pttrns" $ s $ t; 
0  242 

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

243 
fun split2(Abs(x,T,t)) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

244 
let val (pats,u) = split1 t 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

245 
in (pttrns (Free(x,T)) pats, subst_bounds([free x],u)) end 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

246 
 split2(Const("split",_) $ r) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

247 
let val (pats,s) = split2(r) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

248 
val (pats2,t) = split1(s) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

249 
in (pttrns (pttrn pats) pats2, t) end 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

250 
and split1(Abs(x,T,t)) = (Free(x,T), subst_bounds([free x],t)) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

251 
 split1(Const("split",_)$t) = split2(t); 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

252 

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

253 
fun split_tr'(t::args) = 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

254 
let val (pats,ft) = split2(t) 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

255 
in list_comb(const"_lambda" $ pttrn pats $ ft, args) end; 
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

256 

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

257 
in 
1116  258 
*) 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

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

261 
("Pi", dependent_tr' ("@PROD", "op >")), 
632  262 
("Sigma", dependent_tr' ("@SUM", "op *"))]; 
1116  263 
(* 
1106
62bdb9e5722b
Added patternmatching code from CHOL/Prod.thy. Changed
lcp
parents:
690
diff
changeset

264 
end; 
1116  265 
*) 