1 (* Title: ZF/ZF.thy |
1 (* Title: ZF/ZF.thy |
2 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
2 Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section\<open>Zermelo-Fraenkel Set Theory\<close> |
6 section \<open>Zermelo-Fraenkel Set Theory\<close> |
7 |
7 |
8 theory ZF |
8 theory ZF |
9 imports "~~/src/FOL/FOL" |
9 imports "~~/src/FOL/FOL" |
10 begin |
10 begin |
11 |
11 |
|
12 subsection \<open>Signature\<close> |
|
13 |
12 declare [[eta_contract = false]] |
14 declare [[eta_contract = false]] |
13 |
15 |
14 typedecl i |
16 typedecl i |
15 instance i :: "term" .. |
17 instance i :: "term" .. |
16 |
18 |
|
19 axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl "\<in>" 50) \<comment> \<open>membership relation\<close> |
|
20 and zero :: "i" ("0") \<comment> \<open>the empty set\<close> |
|
21 and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close> |
|
22 and Inf :: "i" \<comment> \<open>infinite set\<close> |
|
23 and Union :: "i \<Rightarrow> i" ("\<Union>_" [90] 90) |
|
24 and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
|
25 |
|
26 abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl "\<notin>" 50) \<comment> \<open>negated membership relation\<close> |
|
27 where "x \<notin> y \<equiv> \<not> (x \<in> y)" |
|
28 |
|
29 |
|
30 subsection \<open>Bounded Quantifiers\<close> |
|
31 |
|
32 definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
|
33 where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)" |
|
34 |
|
35 definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o" |
|
36 where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)" |
|
37 |
|
38 syntax |
|
39 "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<forall>_\<in>_./ _)" 10) |
|
40 "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<exists>_\<in>_./ _)" 10) |
|
41 translations |
|
42 "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)" |
|
43 "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)" |
|
44 |
|
45 |
|
46 subsection \<open>Variations on Replacement\<close> |
|
47 |
|
48 (* Derived form of replacement, restricting P to its functional part. |
|
49 The resulting set (for functional P) is the same as with |
|
50 PrimReplace, but the rules are simpler. *) |
|
51 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i" |
|
52 where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" |
|
53 |
|
54 syntax |
|
55 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") |
|
56 translations |
|
57 "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)" |
|
58 |
|
59 |
|
60 (* Functional form of replacement -- analgous to ML's map functional *) |
|
61 |
|
62 definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
63 where "RepFun(A,f) == {y . x\<in>A, y=f(x)}" |
|
64 |
|
65 syntax |
|
66 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) |
|
67 translations |
|
68 "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)" |
|
69 |
|
70 |
|
71 (* Separation and Pairing can be derived from the Replacement |
|
72 and Powerset Axioms using the following definitions. *) |
|
73 definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i" |
|
74 where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" |
|
75 |
|
76 syntax |
|
77 "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" ("(1{_ \<in> _ ./ _})") |
|
78 translations |
|
79 "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)" |
|
80 |
|
81 |
|
82 subsection \<open>General union and intersection\<close> |
|
83 |
|
84 definition Inter :: "i => i" ("\<Inter>_" [90] 90) |
|
85 where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" |
|
86 |
|
87 syntax |
|
88 "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) |
|
89 "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) |
|
90 translations |
|
91 "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})" |
|
92 "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})" |
|
93 |
|
94 |
|
95 subsection \<open>Finite sets and binary operations\<close> |
|
96 |
|
97 (*Unordered pairs (Upair) express binary union/intersection and cons; |
|
98 set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) |
|
99 |
|
100 definition Upair :: "[i, i] => i" |
|
101 where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" |
|
102 |
|
103 definition Subset :: "[i, i] \<Rightarrow> o" (infixl "\<subseteq>" 50) \<comment> \<open>subset relation\<close> |
|
104 where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B" |
|
105 |
|
106 definition Diff :: "[i, i] \<Rightarrow> i" (infixl "-" 65) \<comment> \<open>set difference\<close> |
|
107 where "A - B == { x\<in>A . ~(x\<in>B) }" |
|
108 |
|
109 definition Un :: "[i, i] \<Rightarrow> i" (infixl "\<union>" 65) \<comment> \<open>binary union\<close> |
|
110 where "A \<union> B == \<Union>(Upair(A,B))" |
|
111 |
|
112 definition Int :: "[i, i] \<Rightarrow> i" (infixl "\<inter>" 70) \<comment> \<open>binary intersection\<close> |
|
113 where "A \<inter> B == \<Inter>(Upair(A,B))" |
|
114 |
|
115 definition cons :: "[i, i] => i" |
|
116 where "cons(a,A) == Upair(a,a) \<union> A" |
|
117 |
|
118 definition succ :: "i => i" |
|
119 where "succ(i) == cons(i, i)" |
|
120 |
|
121 nonterminal "is" |
|
122 syntax |
|
123 "" :: "i \<Rightarrow> is" ("_") |
|
124 "_Enum" :: "[i, is] \<Rightarrow> is" ("_,/ _") |
|
125 "_Finset" :: "is \<Rightarrow> i" ("{(_)}") |
|
126 translations |
|
127 "{x, xs}" == "CONST cons(x, {xs})" |
|
128 "{x}" == "CONST cons(x, 0)" |
|
129 |
|
130 |
|
131 subsection \<open>Axioms\<close> |
|
132 |
|
133 (* ZF axioms -- see Suppes p.238 |
|
134 Axioms for Union, Pow and Replace state existence only, |
|
135 uniqueness is derivable using extensionality. *) |
|
136 |
17 axiomatization |
137 axiomatization |
18 zero :: "i" ("0") \<comment>\<open>the empty set\<close> and |
138 where |
19 Pow :: "i => i" \<comment>\<open>power sets\<close> and |
139 extension: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and |
20 Inf :: "i" \<comment>\<open>infinite set\<close> |
140 Union_iff: "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and |
21 |
141 Pow_iff: "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and |
22 text \<open>Bounded Quantifiers\<close> |
142 |
23 consts |
143 (*We may name this set, though it is not uniquely defined.*) |
24 Ball :: "[i, i => o] => o" |
144 infinity: "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and |
25 Bex :: "[i, i => o] => o" |
145 |
26 |
146 (*This formulation facilitates case analysis on A.*) |
27 text \<open>General Union and Intersection\<close> |
147 foundation: "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and |
28 axiomatization Union :: "i => i" ("\<Union>_" [90] 90) |
148 |
29 consts Inter :: "i => i" ("\<Inter>_" [90] 90) |
149 (*Schema axiom since predicate P is a higher-order variable*) |
30 |
150 replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow> |
31 text \<open>Variations on Replacement\<close> |
151 b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))" |
32 axiomatization PrimReplace :: "[i, [i, i] => o] => i" |
152 |
33 consts |
153 |
34 Replace :: "[i, [i, i] => o] => i" |
154 subsection \<open>Definite descriptions -- via Replace over the set "1"\<close> |
35 RepFun :: "[i, i => i] => i" |
155 |
36 Collect :: "[i, i => o] => i" |
156 definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder "THE " 10) |
37 |
157 where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" |
38 text\<open>Definite descriptions -- via Replace over the set "1"\<close> |
158 |
39 consts |
159 definition If :: "[o, i, i] \<Rightarrow> i" ("(if (_)/ then (_)/ else (_))" [10] 10) |
40 The :: "(i => o) => i" (binder "THE " 10) |
160 where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b" |
41 If :: "[o, i, i] => i" ("(if (_)/ then (_)/ else (_))" [10] 10) |
|
42 |
161 |
43 abbreviation (input) |
162 abbreviation (input) |
44 old_if :: "[o, i, i] => i" ("if '(_,_,_')") where |
163 old_if :: "[o, i, i] => i" ("if '(_,_,_')") |
45 "if(P,a,b) == If(P,a,b)" |
164 where "if(P,a,b) == If(P,a,b)" |
46 |
165 |
47 |
166 |
48 text \<open>Finite Sets\<close> |
167 subsection \<open>Ordered Pairing\<close> |
49 consts |
168 |
50 Upair :: "[i, i] => i" |
169 (* this "symmetric" definition works better than {{a}, {a,b}} *) |
51 cons :: "[i, i] => i" |
170 definition Pair :: "[i, i] => i" |
52 succ :: "i => i" |
171 where "Pair(a,b) == {{a,a}, {a,b}}" |
53 |
172 |
54 text \<open>Ordered Pairing\<close> |
173 definition fst :: "i \<Rightarrow> i" |
55 consts |
174 where "fst(p) == THE a. \<exists>b. p = Pair(a, b)" |
56 Pair :: "[i, i] => i" |
175 |
57 fst :: "i => i" |
176 definition snd :: "i \<Rightarrow> i" |
58 snd :: "i => i" |
177 where "snd(p) == THE b. \<exists>a. p = Pair(a, b)" |
59 split :: "[[i, i] => 'a, i] => 'a::{}" \<comment>\<open>for pattern-matching\<close> |
178 |
60 |
179 definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}" \<comment> \<open>for pattern-matching\<close> |
61 text \<open>Sigma and Pi Operators\<close> |
180 where "split(c) == \<lambda>p. c(fst(p), snd(p))" |
62 consts |
181 |
63 Sigma :: "[i, i => i] => i" |
182 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *) |
64 Pi :: "[i, i => i] => i" |
183 nonterminal patterns |
65 |
184 syntax |
66 text \<open>Relations and Functions\<close> |
|
67 consts |
|
68 "domain" :: "i => i" |
|
69 range :: "i => i" |
|
70 field :: "i => i" |
|
71 converse :: "i => i" |
|
72 relation :: "i => o" \<comment>\<open>recognizes sets of pairs\<close> |
|
73 "function" :: "i => o" \<comment>\<open>recognizes functions; can have non-pairs\<close> |
|
74 Lambda :: "[i, i => i] => i" |
|
75 restrict :: "[i, i] => i" |
|
76 |
|
77 text \<open>Infixes in order of decreasing precedence\<close> |
|
78 consts |
|
79 Image :: "[i, i] => i" (infixl "``" 90) \<comment>\<open>image\<close> |
|
80 vimage :: "[i, i] => i" (infixl "-``" 90) \<comment>\<open>inverse image\<close> |
|
81 "apply" :: "[i, i] => i" (infixl "`" 90) \<comment>\<open>function application\<close> |
|
82 "Int" :: "[i, i] => i" (infixl "\<inter>" 70) \<comment>\<open>binary intersection\<close> |
|
83 "Un" :: "[i, i] => i" (infixl "\<union>" 65) \<comment>\<open>binary union\<close> |
|
84 Diff :: "[i, i] => i" (infixl "-" 65) \<comment>\<open>set difference\<close> |
|
85 Subset :: "[i, i] => o" (infixl "\<subseteq>" 50) \<comment>\<open>subset relation\<close> |
|
86 |
|
87 axiomatization |
|
88 mem :: "[i, i] => o" (infixl "\<in>" 50) \<comment>\<open>membership relation\<close> |
|
89 |
|
90 abbreviation |
|
91 not_mem :: "[i, i] => o" (infixl "\<notin>" 50) \<comment>\<open>negated membership relation\<close> |
|
92 where "x \<notin> y \<equiv> \<not> (x \<in> y)" |
|
93 |
|
94 abbreviation |
|
95 cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment>\<open>Cartesian product\<close> |
|
96 where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)" |
|
97 |
|
98 abbreviation |
|
99 function_space :: "[i, i] => i" (infixr "->" 60) \<comment>\<open>function space\<close> |
|
100 where "A -> B \<equiv> Pi(A, \<lambda>_. B)" |
|
101 |
|
102 |
|
103 nonterminal "is" and patterns |
|
104 |
|
105 syntax |
|
106 "" :: "i => is" ("_") |
|
107 "_Enum" :: "[i, is] => is" ("_,/ _") |
|
108 |
|
109 "_Finset" :: "is => i" ("{(_)}") |
|
110 "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") |
|
111 "_Collect" :: "[pttrn, i, o] => i" ("(1{_ \<in> _ ./ _})") |
|
112 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})") |
|
113 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51]) |
|
114 "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10) |
|
115 "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10) |
|
116 "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10) |
|
117 "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10) |
|
118 "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) |
|
119 "_Ball" :: "[pttrn, i, o] => o" ("(3\<forall>_\<in>_./ _)" 10) |
|
120 "_Bex" :: "[pttrn, i, o] => o" ("(3\<exists>_\<in>_./ _)" 10) |
|
121 |
|
122 (** Patterns -- extends pre-defined type "pttrn" used in abstractions **) |
|
123 |
|
124 "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") |
185 "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>") |
125 "" :: "pttrn => patterns" ("_") |
186 "" :: "pttrn => patterns" ("_") |
126 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") |
187 "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") |
127 |
188 "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>") |
128 translations |
189 translations |
129 "{x, xs}" == "CONST cons(x, {xs})" |
|
130 "{x}" == "CONST cons(x, 0)" |
|
131 "{x\<in>A. P}" == "CONST Collect(A, \<lambda>x. P)" |
|
132 "{y. x\<in>A, Q}" == "CONST Replace(A, \<lambda>x y. Q)" |
|
133 "{b. x\<in>A}" == "CONST RepFun(A, \<lambda>x. b)" |
|
134 "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})" |
|
135 "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})" |
|
136 "\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)" |
|
137 "\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)" |
|
138 "\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)" |
|
139 "\<forall>x\<in>A. P" == "CONST Ball(A, \<lambda>x. P)" |
|
140 "\<exists>x\<in>A. P" == "CONST Bex(A, \<lambda>x. P)" |
|
141 |
|
142 "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>" |
190 "\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>" |
143 "\<langle>x, y\<rangle>" == "CONST Pair(x, y)" |
191 "\<langle>x, y\<rangle>" == "CONST Pair(x, y)" |
144 "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)" |
192 "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)" |
145 "\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)" |
193 "\<lambda>\<langle>x,y\<rangle>.b" == "CONST split(\<lambda>x y. b)" |
146 |
194 |
|
195 definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
196 where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}" |
|
197 |
|
198 abbreviation cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment> \<open>Cartesian product\<close> |
|
199 where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)" |
|
200 |
|
201 |
|
202 subsection \<open>Relations and Functions\<close> |
|
203 |
|
204 (*converse of relation r, inverse of function*) |
|
205 definition converse :: "i \<Rightarrow> i" |
|
206 where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}" |
|
207 |
|
208 definition domain :: "i \<Rightarrow> i" |
|
209 where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}" |
|
210 |
|
211 definition range :: "i \<Rightarrow> i" |
|
212 where "range(r) == domain(converse(r))" |
|
213 |
|
214 definition field :: "i \<Rightarrow> i" |
|
215 where "field(r) == domain(r) \<union> range(r)" |
|
216 |
|
217 definition relation :: "i \<Rightarrow> o" \<comment> \<open>recognizes sets of pairs\<close> |
|
218 where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>" |
|
219 |
|
220 definition function :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close> |
|
221 where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')" |
|
222 |
|
223 definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close> |
|
224 where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}" |
|
225 |
|
226 definition vimage :: "[i, i] \<Rightarrow> i" (infixl "-``" 90) \<comment> \<open>inverse image\<close> |
|
227 where vimage_def: "r -`` A == converse(r)``A" |
|
228 |
|
229 (* Restrict the relation r to the domain A *) |
|
230 definition restrict :: "[i, i] \<Rightarrow> i" |
|
231 where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}" |
|
232 |
|
233 |
|
234 (* Abstraction, application and Cartesian product of a family of sets *) |
|
235 |
|
236 definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
237 where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}" |
|
238 |
|
239 definition "apply" :: "[i, i] \<Rightarrow> i" (infixl "`" 90) \<comment> \<open>function application\<close> |
|
240 where "f`a == \<Union>(f``{a})" |
|
241 |
|
242 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i" |
|
243 where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}" |
|
244 |
|
245 abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr "->" 60) \<comment> \<open>function space\<close> |
|
246 where "A -> B \<equiv> Pi(A, \<lambda>_. B)" |
|
247 |
|
248 |
|
249 (* binder syntax *) |
|
250 |
|
251 syntax |
|
252 "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10) |
|
253 "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10) |
|
254 "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10) |
|
255 translations |
|
256 "\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)" |
|
257 "\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)" |
|
258 "\<lambda>x\<in>A. f" == "CONST Lambda(A, \<lambda>x. f)" |
|
259 |
|
260 |
|
261 subsection \<open>ASCII syntax\<close> |
147 |
262 |
148 notation (ASCII) |
263 notation (ASCII) |
149 cart_prod (infixr "*" 80) and |
264 cart_prod (infixr "*" 80) and |
150 Int (infixl "Int" 70) and |
265 Int (infixl "Int" 70) and |
151 Un (infixl "Un" 65) and |
266 Un (infixl "Un" 65) and |
153 Subset (infixl "<=" 50) and |
268 Subset (infixl "<=" 50) and |
154 mem (infixl ":" 50) and |
269 mem (infixl ":" 50) and |
155 not_mem (infixl "~:" 50) |
270 not_mem (infixl "~:" 50) |
156 |
271 |
157 syntax (ASCII) |
272 syntax (ASCII) |
|
273 "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) |
|
274 "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) |
158 "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") |
275 "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})") |
159 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") |
276 "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})") |
160 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) |
277 "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51]) |
161 "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) |
278 "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10) |
162 "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) |
279 "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10) |
163 "_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) |
280 "_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10) |
164 "_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) |
281 "_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10) |
165 "_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) |
282 "_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10) |
166 "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10) |
|
167 "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10) |
|
168 "_Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
283 "_Tuple" :: "[i, is] => i" ("<(_,/ _)>") |
169 "_pattern" :: "patterns => pttrn" ("<_>") |
284 "_pattern" :: "patterns => pttrn" ("<_>") |
170 |
|
171 defs (* Bounded Quantifiers *) |
|
172 Ball_def: "Ball(A, P) == \<forall>x. x\<in>A \<longrightarrow> P(x)" |
|
173 Bex_def: "Bex(A, P) == \<exists>x. x\<in>A & P(x)" |
|
174 |
|
175 subset_def: "A \<subseteq> B == \<forall>x\<in>A. x\<in>B" |
|
176 |
|
177 |
|
178 axiomatization where |
|
179 |
|
180 (* ZF axioms -- see Suppes p.238 |
|
181 Axioms for Union, Pow and Replace state existence only, |
|
182 uniqueness is derivable using extensionality. *) |
|
183 |
|
184 extension: "A = B <-> A \<subseteq> B & B \<subseteq> A" and |
|
185 Union_iff: "A \<in> \<Union>(C) <-> (\<exists>B\<in>C. A\<in>B)" and |
|
186 Pow_iff: "A \<in> Pow(B) <-> A \<subseteq> B" and |
|
187 |
|
188 (*We may name this set, though it is not uniquely defined.*) |
|
189 infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and |
|
190 |
|
191 (*This formulation facilitates case analysis on A.*) |
|
192 foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and |
|
193 |
|
194 (*Schema axiom since predicate P is a higher-order variable*) |
|
195 replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) \<longrightarrow> y=z) ==> |
|
196 b \<in> PrimReplace(A,P) <-> (\<exists>x\<in>A. P(x,b))" |
|
197 |
|
198 |
|
199 defs |
|
200 |
|
201 (* Derived form of replacement, restricting P to its functional part. |
|
202 The resulting set (for functional P) is the same as with |
|
203 PrimReplace, but the rules are simpler. *) |
|
204 |
|
205 Replace_def: "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))" |
|
206 |
|
207 (* Functional form of replacement -- analgous to ML's map functional *) |
|
208 |
|
209 RepFun_def: "RepFun(A,f) == {y . x\<in>A, y=f(x)}" |
|
210 |
|
211 (* Separation and Pairing can be derived from the Replacement |
|
212 and Powerset Axioms using the following definitions. *) |
|
213 |
|
214 Collect_def: "Collect(A,P) == {y . x\<in>A, x=y & P(x)}" |
|
215 |
|
216 (*Unordered pairs (Upair) express binary union/intersection and cons; |
|
217 set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) |
|
218 |
|
219 Upair_def: "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" |
|
220 cons_def: "cons(a,A) == Upair(a,a) \<union> A" |
|
221 succ_def: "succ(i) == cons(i, i)" |
|
222 |
|
223 (* Difference, general intersection, binary union and small intersection *) |
|
224 |
|
225 Diff_def: "A - B == { x\<in>A . ~(x\<in>B) }" |
|
226 Inter_def: "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}" |
|
227 Un_def: "A \<union> B == \<Union>(Upair(A,B))" |
|
228 Int_def: "A \<inter> B == \<Inter>(Upair(A,B))" |
|
229 |
|
230 (* definite descriptions *) |
|
231 the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})" |
|
232 if_def: "if(P,a,b) == THE z. P & z=a | ~P & z=b" |
|
233 |
|
234 (* this "symmetric" definition works better than {{a}, {a,b}} *) |
|
235 Pair_def: "<a,b> == {{a,a}, {a,b}}" |
|
236 fst_def: "fst(p) == THE a. \<exists>b. p=<a,b>" |
|
237 snd_def: "snd(p) == THE b. \<exists>a. p=<a,b>" |
|
238 split_def: "split(c) == %p. c(fst(p), snd(p))" |
|
239 Sigma_def: "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x,y>}" |
|
240 |
|
241 (* Operations on relations *) |
|
242 |
|
243 (*converse of relation r, inverse of function*) |
|
244 converse_def: "converse(r) == {z. w\<in>r, \<exists>x y. w=<x,y> & z=<y,x>}" |
|
245 |
|
246 domain_def: "domain(r) == {x. w\<in>r, \<exists>y. w=<x,y>}" |
|
247 range_def: "range(r) == domain(converse(r))" |
|
248 field_def: "field(r) == domain(r) \<union> range(r)" |
|
249 relation_def: "relation(r) == \<forall>z\<in>r. \<exists>x y. z = <x,y>" |
|
250 function_def: "function(r) == |
|
251 \<forall>x y. <x,y>:r \<longrightarrow> (\<forall>y'. <x,y'>:r \<longrightarrow> y=y')" |
|
252 image_def: "r `` A == {y \<in> range(r) . \<exists>x\<in>A. <x,y> \<in> r}" |
|
253 vimage_def: "r -`` A == converse(r)``A" |
|
254 |
|
255 (* Abstraction, application and Cartesian product of a family of sets *) |
|
256 |
|
257 lam_def: "Lambda(A,b) == {<x,b(x)> . x\<in>A}" |
|
258 apply_def: "f`a == \<Union>(f``{a})" |
|
259 Pi_def: "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A<=domain(f) & function(f)}" |
|
260 |
|
261 (* Restrict the relation r to the domain A *) |
|
262 restrict_def: "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = <x,y>}" |
|
263 |
285 |
264 |
286 |
265 subsection \<open>Substitution\<close> |
287 subsection \<open>Substitution\<close> |
266 |
288 |
267 (*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
289 (*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |