1 (* ========================================================================= *)
2 (* Set-theoretic hierarchy for modelling HOL inside itself. *)
3 (* ========================================================================= *)
6 (`(!x y. (f x = f y) ==> (x = y)) <=> (!x y. (f x = f y) <=> (x = y))`,
9 (* ------------------------------------------------------------------------- *)
10 (* Useful to have a niceish "function update" notation. *)
11 (* ------------------------------------------------------------------------- *)
13 parse_as_infix("|->",(12,"right"));;
15 let valmod = new_definition
16 `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
19 (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
20 REWRITE_TAC[valmod]);;
22 let VALMOD_BASIC = prove
23 (`!v x y. (x |-> y) v x = y`,
24 REWRITE_TAC[valmod]);;
26 let VALMOD_VALMOD_BASIC = prove
27 (`!v a b x. (x |-> a) ((x |-> b) v) = (x |-> a) v`,
28 REWRITE_TAC[valmod; FUN_EQ_THM] THEN
29 REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
31 let VALMOD_REPEAT = prove
32 (`!v x. (x |-> v(x)) v = v`,
33 REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
35 let FORALL_VALMOD = prove
36 (`!x. (!v a. P((x |-> a) v)) = (!v. P v)`,
37 MESON_TAC[VALMOD_REPEAT]);;
39 let VALMOD_SWAP = prove
41 ~(x = y) ==> ((x |-> a) ((y |-> b) v) = (y |-> b) ((x |-> a) v))`,
42 REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
44 (* ------------------------------------------------------------------------- *)
45 (* A dummy finite type inadequately modelling ":ind". *)
46 (* ------------------------------------------------------------------------- *)
48 let ind_model_tybij_th =
49 prove(`?x. x IN @s:num->bool. ~(s = {}) /\ FINITE s`,
50 MESON_TAC[MEMBER_NOT_EMPTY; IN_SING; FINITE_RULES]);;
53 new_type_definition "ind_model" ("mk_ind","dest_ind") ind_model_tybij_th;;
55 (* ------------------------------------------------------------------------- *)
56 (* Introduce a type whose universe is "inaccessible" starting from *)
57 (* "ind_model". Since "ind_model" is finite, we can just use any *)
58 (* infinite set. In order to make "ind_model" infinite, we would need *)
59 (* a new axiom. In order to keep things generic we try to deduce *)
60 (* everything from this one uniform "axiom". Note that even in the *)
61 (* infinite case, this can still be a small set in ZF terms, not a real *)
62 (* inaccessible cardinal. *)
63 (* ------------------------------------------------------------------------- *)
65 (****** Here's what we'd do in the infinite case
69 let I_AXIOM = new_axiom
70 `UNIV:ind_model->bool <_c UNIV:I->bool /\
71 (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`;;
75 let inacc_tybij_th = prove
76 (`?x:num. x IN UNIV`,REWRITE_TAC[IN_UNIV]);;
79 new_type_definition "I" ("mk_I","dest_I") inacc_tybij_th;;
82 (`UNIV:ind_model->bool <_c UNIV:I->bool /\
83 (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`,
85 (`!s. s <_c UNIV:I->bool <=> FINITE s`,
86 GEN_TAC THEN REWRITE_TAC[FINITE_CARD_LT] THEN
87 MATCH_MP_TAC CARD_LT_CONG THEN REWRITE_TAC[CARD_EQ_REFL] THEN
88 REWRITE_TAC[GSYM CARD_LE_ANTISYM; le_c; IN_UNIV] THEN
89 MESON_TAC[inacc_tybij; IN_UNIV]) in
90 REWRITE_TAC[lemma; FINITE_POWERSET] THEN
91 SUBGOAL_THEN `UNIV = IMAGE mk_ind (@s. ~(s = {}) /\ FINITE s)`
93 [MESON_TAC[EXTENSION; IN_IMAGE; IN_UNIV; ind_model_tybij];
94 MESON_TAC[FINITE_IMAGE; NOT_INSERT_EMPTY; FINITE_RULES]]);;
96 (* ------------------------------------------------------------------------- *)
97 (* I is infinite and therefore admits an injective pairing. *)
98 (* ------------------------------------------------------------------------- *)
100 let I_INFINITE = prove
101 (`INFINITE(UNIV:I->bool)`,
102 REWRITE_TAC[INFINITE] THEN DISCH_TAC THEN
103 MP_TAC(ISPEC `{n | n < CARD(UNIV:I->bool) - 1}` (CONJUNCT2 I_AXIOM)) THEN
104 ASM_SIMP_TAC[CARD_LT_CARD; FINITE_NUMSEG_LT; FINITE_POWERSET] THEN
105 SIMP_TAC[CARD_NUMSEG_LT; CARD_POWERSET; FINITE_NUMSEG_LT] THEN
106 SUBGOAL_THEN `~(CARD(UNIV:I->bool) = 0)` MP_TAC THENL
107 [ASM_SIMP_TAC[CARD_EQ_0; GSYM MEMBER_NOT_EMPTY; IN_UNIV]; ALL_TAC] THEN
108 SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 < n`; NOT_LT] THEN
109 MATCH_MP_TAC(ARITH_RULE `a - 1 < b ==> ~(a = 0) ==> a <= b`) THEN
110 SPEC_TAC(`CARD(UNIV:I->bool) - 1`,`n:num`) THEN POP_ASSUM(K ALL_TAC) THEN
111 INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN POP_ASSUM MP_TAC THEN
114 let I_PAIR_EXISTS = prove
115 (`?f:I#I->I. !x y. (f x = f y) ==> (x = y)`,
116 SUBGOAL_THEN `UNIV:I#I->bool <=_c UNIV:I->bool` MP_TAC THENL
117 [ALL_TAC; REWRITE_TAC[le_c; IN_UNIV]] THEN
118 MATCH_MP_TAC CARD_EQ_IMP_LE THEN
119 MP_TAC(MATCH_MP CARD_SQUARE_INFINITE I_INFINITE) THEN
120 MATCH_MP_TAC(TAUT `(a = b) ==> a ==> b`) THEN
121 AP_THM_TAC THEN AP_TERM_TAC THEN
122 REWRITE_TAC[EXTENSION; mul_c; IN_ELIM_THM; IN_UNIV] THEN MESON_TAC[PAIR]);;
124 let I_PAIR = REWRITE_RULE[INJ_LEMMA]
125 (new_specification ["I_PAIR"] I_PAIR_EXISTS);;
127 (* ------------------------------------------------------------------------- *)
128 (* It also admits injections from "bool" and "ind_model". *)
129 (* ------------------------------------------------------------------------- *)
131 let CARD_BOOL_LT_I = prove
132 (`UNIV:bool->bool <_c UNIV:I->bool`,
133 REWRITE_TAC[GSYM CARD_NOT_LE] THEN
134 DISCH_TAC THEN MP_TAC I_INFINITE THEN REWRITE_TAC[INFINITE] THEN
135 SUBGOAL_THEN `FINITE(UNIV:bool->bool)`
136 (fun th -> ASM_MESON_TAC[th; CARD_LE_FINITE]) THEN
137 SUBGOAL_THEN `UNIV:bool->bool = {F,T}` SUBST1_TAC THENL
138 [REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT] THEN MESON_TAC[];
139 SIMP_TAC[FINITE_RULES]]);;
141 let I_BOOL_EXISTS = prove
142 (`?f:bool->I. !x y. (f x = f y) ==> (x = y)`,
143 MP_TAC(MATCH_MP CARD_LT_IMP_LE CARD_BOOL_LT_I) THEN
144 SIMP_TAC[lt_c; le_c; IN_UNIV]);;
146 let I_BOOL = REWRITE_RULE[INJ_LEMMA]
147 (new_specification ["I_BOOL"] I_BOOL_EXISTS);;
149 let I_IND_EXISTS = prove
150 (`?f:ind_model->I. !x y. (f x = f y) ==> (x = y)`,
151 MP_TAC(CONJUNCT1 I_AXIOM) THEN SIMP_TAC[lt_c; le_c; IN_UNIV]);;
153 let I_IND = REWRITE_RULE[INJ_LEMMA]
154 (new_specification ["I_IND"] I_IND_EXISTS);;
156 (* ------------------------------------------------------------------------- *)
157 (* And the injection from powerset of any accessible set. *)
158 (* ------------------------------------------------------------------------- *)
160 let I_SET_EXISTS = prove
163 ==> ?f:(I->bool)->I. !t u. t SUBSET s /\ u SUBSET s /\ (f t = f u)
165 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP(CONJUNCT2 I_AXIOM)) THEN
166 DISCH_THEN(MP_TAC o MATCH_MP CARD_LT_IMP_LE) THEN
167 REWRITE_TAC[le_c; IN_UNIV; IN_ELIM_THM]);;
169 let I_SET = new_specification ["I_SET"]
170 (REWRITE_RULE[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] I_SET_EXISTS);;
172 (* ------------------------------------------------------------------------- *)
173 (* Define a type for "levels" of our set theory. *)
174 (* ------------------------------------------------------------------------- *)
176 let setlevel_INDUCT,setlevel_RECURSION = define_type
180 | Cartprod setlevel setlevel";;
182 let setlevel_DISTINCT = distinctness "setlevel";;
183 let setlevel_INJ = injectivity "setlevel";;
185 (* ------------------------------------------------------------------------- *)
186 (* Now define a subset of I corresponding to each. *)
187 (* ------------------------------------------------------------------------- *)
189 let setlevel = new_recursive_definition setlevel_RECURSION
190 `(setlevel Ur_bool = IMAGE I_BOOL UNIV) /\
191 (setlevel Ur_ind = IMAGE I_IND UNIV) /\
192 (setlevel (Cartprod l1 l2) =
193 IMAGE I_PAIR {x,y | x IN setlevel l1 /\ y IN setlevel l2}) /\
194 (setlevel (Powerset l) = IMAGE (I_SET (setlevel l))
195 {s | s SUBSET (setlevel l)})`;;
197 (* ------------------------------------------------------------------------- *)
198 (* Show they all satisfy the cardinal limits. *)
199 (* ------------------------------------------------------------------------- *)
201 let SETLEVEL_CARD = prove
202 (`!l. setlevel l <_c UNIV:I->bool`,
203 MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel] THEN
204 REPEAT CONJ_TAC THENL
205 [TRANS_TAC CARD_LET_TRANS `UNIV:bool->bool` THEN
206 REWRITE_TAC[CARD_LE_IMAGE; CARD_BOOL_LT_I];
207 TRANS_TAC CARD_LET_TRANS `UNIV:ind_model->bool` THEN
208 REWRITE_TAC[CARD_LE_IMAGE; I_AXIOM];
209 X_GEN_TAC `l:setlevel` THEN DISCH_TAC THEN
210 TRANS_TAC CARD_LET_TRANS `{s | s SUBSET (setlevel l)}` THEN
211 ASM_SIMP_TAC[I_AXIOM; CARD_LE_IMAGE];
213 MAP_EVERY X_GEN_TAC [`l1:setlevel`; `l2:setlevel`] THEN STRIP_TAC THEN
214 TRANS_TAC CARD_LET_TRANS `setlevel l1 *_c setlevel l2` THEN
215 ASM_SIMP_TAC[CARD_MUL_LT_INFINITE; I_INFINITE; GSYM mul_c; CARD_LE_IMAGE]);;
217 (* ------------------------------------------------------------------------- *)
218 (* Hence the injectivity of the mapping from powerset. *)
219 (* ------------------------------------------------------------------------- *)
221 let I_SET_SETLEVEL = prove
222 (`!l s t. s SUBSET setlevel l /\ t SUBSET setlevel l /\
223 (I_SET (setlevel l) s = I_SET (setlevel l) t)
225 MESON_TAC[SETLEVEL_CARD; I_SET]);;
227 (* ------------------------------------------------------------------------- *)
228 (* Now our universe of sets and (ur)elements. *)
229 (* ------------------------------------------------------------------------- *)
231 let universe = new_definition
232 `universe = {(t,x) | x IN setlevel t}`;;
234 (* ------------------------------------------------------------------------- *)
235 (* Define an actual type V. *)
237 (* This satisfies a suitable number of the ZF axioms. It isn't extensional *)
238 (* but we could then construct a quotient structure if desired. Anyway it's *)
239 (* only empty sets that aren't. A more significant difference is that we *)
240 (* have urelements and the hierarchy levels are all distinct rather than *)
241 (* being cumulative. *)
242 (* ------------------------------------------------------------------------- *)
244 let v_tybij_th = prove
245 (`?a. a IN universe`,
246 EXISTS_TAC `Ur_bool,I_BOOL T` THEN
247 REWRITE_TAC[universe; IN_ELIM_THM; PAIR_EQ; CONJ_ASSOC;
248 ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1;
249 setlevel; IN_IMAGE; IN_UNIV] THEN
253 new_type_definition "V" ("mk_V","dest_V") v_tybij_th;;
256 (`!l e. e IN setlevel l <=> (dest_V(mk_V(l,e)) = (l,e))`,
257 REWRITE_TAC[GSYM(CONJUNCT2 v_tybij)] THEN
258 REWRITE_TAC[IN_ELIM_THM; universe; FORALL_PAIR_THM; PAIR_EQ] THEN
261 (* ------------------------------------------------------------------------- *)
262 (* Drop a level; test if something is a set. *)
263 (* ------------------------------------------------------------------------- *)
265 let droplevel = new_recursive_definition setlevel_RECURSION
266 `droplevel(Powerset l) = l`;;
268 let isasetlevel = new_recursive_definition setlevel_RECURSION
269 `(isasetlevel Ur_bool = F) /\
270 (isasetlevel Ur_ind = F) /\
271 (isasetlevel (Cartprod l1 l2) = F) /\
272 (isasetlevel (Powerset l) = T)`;;
274 (* ------------------------------------------------------------------------- *)
275 (* Define some useful inversions. *)
276 (* ------------------------------------------------------------------------- *)
278 let level = new_definition
279 `level x = FST(dest_V x)`;;
281 let element = new_definition
282 `element x = SND(dest_V x)`;;
284 let ELEMENT_IN_LEVEL = prove
285 (`!x. (element x) IN setlevel(level x)`,
286 REWRITE_TAC[V_TYBIJ; v_tybij; level; element; PAIR]);;
289 (`!x. mk_V(level x,element x) = x`,
290 REWRITE_TAC[level; element; PAIR; v_tybij]);;
292 let set = new_definition
293 `set x = @s. s SUBSET (setlevel(droplevel(level x))) /\
294 (I_SET (setlevel(droplevel(level x))) s = element x)`;;
296 let isaset = new_definition
297 `isaset x <=> ?l. level x = Powerset l`;;
299 (* ------------------------------------------------------------------------- *)
300 (* Now all the critical relations. *)
301 (* ------------------------------------------------------------------------- *)
303 parse_as_infix("<:",(11,"right"));;
305 let inset = new_definition
306 `x <: s <=> (level s = Powerset(level x)) /\ (element x) IN (set s)`;;
308 parse_as_infix("<=:",(12,"right"));;
310 let subset_def = new_definition
311 `s <=: t <=> (level s = level t) /\ !x. x <: s ==> x <: t`;;
313 (* ------------------------------------------------------------------------- *)
314 (* If something has members, it's a set. *)
315 (* ------------------------------------------------------------------------- *)
317 let MEMBERS_ISASET = prove
318 (`!x s. x <: s ==> isaset s`,
319 REWRITE_TAC[inset; isaset] THEN MESON_TAC[]);;
321 (* ------------------------------------------------------------------------- *)
322 (* Each level is nonempty. *)
323 (* ------------------------------------------------------------------------- *)
325 let LEVEL_NONEMPTY = prove
326 (`!l. ?x. x IN setlevel l`,
327 REWRITE_TAC[MEMBER_NOT_EMPTY] THEN
328 MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel; IMAGE_EQ_EMPTY] THEN
329 REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIV] THEN
330 REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_THM] THEN
331 MESON_TAC[EMPTY_SUBSET]);;
333 let LEVEL_SET_EXISTS = prove
334 (`!l. ?s. level s = l`,
335 MP_TAC LEVEL_NONEMPTY THEN MATCH_MP_TAC MONO_FORALL THEN
336 REWRITE_TAC[level] THEN MESON_TAC[FST; PAIR; V_TYBIJ]);;
338 (* ------------------------------------------------------------------------- *)
339 (* Empty sets (or non-sets, of course) exist at all set levels. *)
340 (* ------------------------------------------------------------------------- *)
342 let MK_V_CLAUSES = prove
344 ==> (level(mk_V(l,e)) = l) /\ (element(mk_V(l,e)) = e)`,
345 REWRITE_TAC[level; element; PAIR; GSYM PAIR_EQ; V_TYBIJ]);;
348 (`s SUBSET setlevel l
349 ==> (set(mk_V(Powerset l,I_SET (setlevel l) s)) = s) /\
350 (level(mk_V(Powerset l,I_SET (setlevel l) s)) = Powerset l) /\
351 (element(mk_V(Powerset l,I_SET (setlevel l) s)) = I_SET (setlevel l) s)`,
352 REPEAT GEN_TAC THEN DISCH_TAC THEN
353 SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
354 [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
356 ASM_SIMP_TAC[MK_V_CLAUSES; set] THEN
357 SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
358 [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
360 ASM_SIMP_TAC[MK_V_CLAUSES; droplevel] THEN
361 MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN
362 ASM_MESON_TAC[I_SET_SETLEVEL]);;
364 let EMPTY_EXISTS = prove
365 (`!l. ?s. (level s = l) /\ !x. ~(x <: s)`,
366 MATCH_MP_TAC setlevel_INDUCT THEN
367 REPEAT CONJ_TAC THENL
369 X_GEN_TAC `l:setlevel` THEN DISCH_THEN(K ALL_TAC) THEN
370 EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) {})` THEN
371 SIMP_TAC[inset; MK_V_CLAUSES; MK_V_SET; EMPTY_SUBSET; NOT_IN_EMPTY];
373 MESON_TAC[LEVEL_SET_EXISTS; MEMBERS_ISASET; isaset;
374 setlevel_DISTINCT]);;
376 let EMPTY_SET = new_specification ["emptyset"]
377 (REWRITE_RULE[SKOLEM_THM] EMPTY_EXISTS);;
379 (* ------------------------------------------------------------------------- *)
380 (* Comprehension principle, with no change of levels. *)
381 (* ------------------------------------------------------------------------- *)
383 let COMPREHENSION_EXISTS = prove
384 (`!s p. ?t. (level t = level s) /\ !x. x <: t <=> x <: s /\ p x`,
385 REPEAT GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
386 [ALL_TAC; ASM_MESON_TAC[MEMBERS_ISASET]] THEN
387 POP_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
388 MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
389 ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
390 DISCH_THEN(X_CHOOSE_THEN `u:I->bool` STRIP_ASSUME_TAC) THEN
391 EXISTS_TAC `mk_V(Powerset l,
393 {i | i IN u /\ p(mk_V(l,i))})` THEN
394 SUBGOAL_THEN `{i | i IN u /\ p (mk_V (l,i))} SUBSET (setlevel l)`
396 [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[SUBSET];
398 ASM_SIMP_TAC[MK_V_SET; inset] THEN X_GEN_TAC `x:V` THEN
399 REWRITE_TAC[setlevel_INJ] THEN
400 REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[SET; MK_V_SET]);;
402 parse_as_infix("suchthat",(21,"left"));;
404 let SUCHTHAT = new_specification ["suchthat"]
405 (REWRITE_RULE[SKOLEM_THM] COMPREHENSION_EXISTS);;
407 (* ------------------------------------------------------------------------- *)
408 (* Each setlevel exists as a set. *)
409 (* ------------------------------------------------------------------------- *)
411 let SETLEVEL_EXISTS = prove
412 (`!l. ?s. (level s = Powerset l) /\
413 !x. x <: s <=> (level x = l) /\ element(x) IN setlevel l`,
415 EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) (setlevel l))` THEN
416 SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; setlevel_INJ] THEN MESON_TAC[]);;
418 (* ------------------------------------------------------------------------- *)
419 (* Conversely, set(s) belongs in the appropriate level. *)
420 (* ------------------------------------------------------------------------- *)
422 let SET_DECOMP = prove
424 ==> (set s) SUBSET (setlevel(droplevel(level s))) /\
425 (I_SET (setlevel(droplevel(level s))) (set s) = element s)`,
426 REPEAT GEN_TAC THEN REWRITE_TAC[isaset] THEN
427 DISCH_THEN(X_CHOOSE_TAC `l:setlevel`) THEN
428 REWRITE_TAC[set] THEN CONV_TAC SELECT_CONV THEN
429 ASM_REWRITE_TAC[setlevel; droplevel] THEN
430 MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
431 ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
434 let SET_SUBSET_SETLEVEL = prove
435 (`!s. isaset s ==> set(s) SUBSET setlevel(droplevel(level s))`,
436 MESON_TAC[SET_DECOMP]);;
438 (* ------------------------------------------------------------------------- *)
439 (* Power set exists. *)
440 (* ------------------------------------------------------------------------- *)
442 let POWERSET_EXISTS = prove
443 (`!s. ?t. (level t = Powerset(level s)) /\ !x. x <: t <=> x <=: s`,
444 GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
445 [FIRST_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
446 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [isaset]) THEN
447 DISCH_THEN(X_CHOOSE_THEN `l:setlevel` STRIP_ASSUME_TAC) THEN
448 ASM_REWRITE_TAC[droplevel] THEN STRIP_TAC THEN
449 X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC
450 (SPEC `Powerset l` SETLEVEL_EXISTS) THEN
451 MP_TAC(SPECL [`t:V`; `\v. !x. x <: v ==> x <: s`]
452 COMPREHENSION_EXISTS) THEN
453 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:V` THEN
454 STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
455 ASM_MESON_TAC[ELEMENT_IN_LEVEL];
456 MP_TAC(SPEC `level s` SETLEVEL_EXISTS) THEN
457 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:V` THEN
458 STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
459 ASM_MESON_TAC[ELEMENT_IN_LEVEL; MEMBERS_ISASET; isaset]]);;
461 let POWERSET = new_specification ["powerset"]
462 (REWRITE_RULE[SKOLEM_THM] POWERSET_EXISTS);;
464 (* ------------------------------------------------------------------------- *)
465 (* Pairing operation. *)
466 (* ------------------------------------------------------------------------- *)
468 let pair = new_definition
470 mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))`;;
472 let PAIR_IN_LEVEL = prove
473 (`!x y l m. x IN setlevel l /\ y IN setlevel m
474 ==> I_PAIR(x,y) IN setlevel (Cartprod l m)`,
475 REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);;
477 let DEST_MK_PAIR = prove
478 (`dest_V(mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))) =
479 Cartprod (level x) (level y),I_PAIR(element x,element y)`,
480 REWRITE_TAC[GSYM V_TYBIJ] THEN SIMP_TAC[PAIR_IN_LEVEL; ELEMENT_IN_LEVEL]);;
483 (`!x1 y1 x2 y2. (pair x1 y1 = pair x2 y2) <=> (x1 = x2) /\ (y1 = y2)`,
484 REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
485 REWRITE_TAC[pair] THEN
486 DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN REWRITE_TAC[DEST_MK_PAIR] THEN
487 REWRITE_TAC[setlevel_INJ; PAIR_EQ; I_PAIR] THEN
488 REWRITE_TAC[level; element] THEN MESON_TAC[PAIR; CONJUNCT1 v_tybij]);;
490 let LEVEL_PAIR = prove
491 (`!x y. level(pair x y) = Cartprod (level x) (level y)`,
493 REWRITE_RULE[DEST_MK_PAIR] (AP_TERM `dest_V` (SPEC_ALL pair))]);;
495 (* ------------------------------------------------------------------------- *)
496 (* Decomposition functions. *)
497 (* ------------------------------------------------------------------------- *)
499 let fst_def = new_definition
500 `fst p = @x. ?y. p = pair x y`;;
502 let snd_def = new_definition
503 `snd p = @y. ?x. p = pair x y`;;
505 let PAIR_CLAUSES = prove
506 (`!x y. (fst(pair x y) = x) /\ (snd(pair x y) = y)`,
507 REWRITE_TAC[fst_def; snd_def] THEN MESON_TAC[PAIR_INJ]);;
509 (* ------------------------------------------------------------------------- *)
510 (* And the Cartesian product space. *)
511 (* ------------------------------------------------------------------------- *)
513 let CARTESIAN_EXISTS = prove
514 (`!s t. ?u. (level u =
515 Powerset(Cartprod (droplevel(level s))
516 (droplevel(level t)))) /\
517 !z. z <: u <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
519 ASM_CASES_TAC `isaset s` THENL
520 [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
521 SUBGOAL_THEN `?l. (level s = Powerset l)` CHOOSE_TAC THENL
522 [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
523 ASM_CASES_TAC `isaset t` THENL
524 [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
525 SUBGOAL_THEN `?m. (level t = Powerset m)` CHOOSE_TAC THENL
526 [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
527 MP_TAC(SPEC `Cartprod l m` SETLEVEL_EXISTS) THEN
528 ASM_REWRITE_TAC[droplevel] THEN
529 DISCH_THEN(X_CHOOSE_THEN `u:V` STRIP_ASSUME_TAC) THEN
530 MP_TAC(SPECL [`u:V`; `\z. ?x y. (z = pair x y) /\ x <: s /\ y <: t`]
531 COMPREHENSION_EXISTS) THEN
532 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `w:V` THEN
533 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
535 MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> a) ==> ((a /\ b) /\ c <=> c)`) THEN
536 CONJ_TAC THENL [MESON_TAC[ELEMENT_IN_LEVEL]; ALL_TAC] THEN
537 STRIP_TAC THEN ASM_REWRITE_TAC[LEVEL_PAIR] THEN BINOP_TAC THEN
538 ASM_MESON_TAC[inset; setlevel_INJ]);;
540 let PRODUCT = new_specification ["product"]
541 (REWRITE_RULE[SKOLEM_THM] CARTESIAN_EXISTS);;
543 (* ------------------------------------------------------------------------- *)
544 (* Extensionality for sets at the same level. *)
545 (* ------------------------------------------------------------------------- *)
547 let IN_SET_ELEMENT = prove
548 (`!s. isaset s /\ e IN set(s)
549 ==> ?x. (e = element x) /\ (level s = Powerset(level x)) /\ x <: s`,
550 REPEAT STRIP_TAC THEN
551 FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
552 EXISTS_TAC `mk_V(l,e)` THEN REWRITE_TAC[inset] THEN
553 SUBGOAL_THEN `e IN setlevel l` (fun t -> ASM_SIMP_TAC[t; MK_V_CLAUSES]) THEN
554 ASM_MESON_TAC[SET_SUBSET_SETLEVEL; SUBSET; droplevel]);;
556 let SUBSET_ALT = prove
557 (`isaset s /\ isaset t
558 ==> (s <=: t <=> (level s = level t) /\ set(s) SUBSET set(t))`,
559 REPEAT GEN_TAC THEN REWRITE_TAC[subset_def; inset] THEN
560 ASM_CASES_TAC `level s = level t` THEN ASM_REWRITE_TAC[SUBSET] THEN
561 STRIP_TAC THEN EQ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
562 ASM_MESON_TAC[IN_SET_ELEMENT]);;
564 let SUBSET_ANTISYM_LEVEL = prove
565 (`!s t. isaset s /\ isaset t /\ s <=: t /\ t <=: s ==> (s = t)`,
567 REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
568 ASM_SIMP_TAC[SUBSET_ALT] THEN
569 EVERY_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
570 REPEAT STRIP_TAC THEN
571 MP_TAC(SPEC `s:V` SET) THEN MP_TAC(SPEC `t:V` SET) THEN
572 REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
573 AP_TERM_TAC THEN BINOP_TAC THEN ASM_MESON_TAC[SUBSET_ANTISYM]);;
575 let EXTENSIONALITY_LEVEL = prove
576 (`!s t. isaset s /\ isaset t /\ (level s = level t) /\ (!x. x <: s <=> x <: t)
578 MESON_TAC[SUBSET_ANTISYM_LEVEL; subset_def]);;
580 (* ------------------------------------------------------------------------- *)
581 (* And hence for any nonempty sets. *)
582 (* ------------------------------------------------------------------------- *)
584 let EXTENSIONALITY_NONEMPTY = prove
585 (`!s t. (?x. x <: s) /\ (?x. x <: t) /\ (!x. x <: s <=> x <: t)
587 REPEAT STRIP_TAC THEN MATCH_MP_TAC EXTENSIONALITY_LEVEL THEN
588 ASM_MESON_TAC[MEMBERS_ISASET; inset]);;
590 (* ------------------------------------------------------------------------- *)
591 (* Union set exists. I don't need this but if might be a sanity check. *)
592 (* ------------------------------------------------------------------------- *)
594 let UNION_EXISTS = prove
595 (`!s. ?t. (level t = droplevel(level s)) /\
596 !x. x <: t <=> ?u. x <: u /\ u <: s`,
597 GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
599 MP_TAC(SPEC `droplevel(level s)` EMPTY_EXISTS) THEN
600 MATCH_MP_TAC MONO_EXISTS THEN ASM_MESON_TAC[MEMBERS_ISASET]] THEN
601 FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
602 ASM_REWRITE_TAC[droplevel] THEN ASM_CASES_TAC `?m. l = Powerset m` THENL
604 MP_TAC(SPEC `l:setlevel` EMPTY_EXISTS) THEN MATCH_MP_TAC MONO_EXISTS THEN
605 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[inset] THEN
606 ASM_MESON_TAC[setlevel_INJ]] THEN
607 FIRST_X_ASSUM(X_CHOOSE_THEN `m:setlevel` SUBST_ALL_TAC) THEN
608 MP_TAC(SPEC `m:setlevel` SETLEVEL_EXISTS) THEN
609 ASM_REWRITE_TAC[droplevel] THEN
610 DISCH_THEN(X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC) THEN
611 MP_TAC(SPECL [`t:V`; `\x. ?u. x <: u /\ u <: s`]
612 COMPREHENSION_EXISTS) THEN
613 MATCH_MP_TAC MONO_EXISTS THEN
614 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
615 ASM_MESON_TAC[inset; ELEMENT_IN_LEVEL; setlevel_INJ]);;
617 let SETUNION = new_specification ["setunion"]
618 (REWRITE_RULE[SKOLEM_THM] UNION_EXISTS);;
620 (* ------------------------------------------------------------------------- *)
622 (* ------------------------------------------------------------------------- *)
624 let true_def = new_definition
625 `true = mk_V(Ur_bool,I_BOOL T)`;;
627 let false_def = new_definition
628 `false = mk_V(Ur_bool,I_BOOL F)`;;
630 let boolset = new_definition
632 mk_V(Powerset Ur_bool,I_SET (setlevel Ur_bool) (setlevel Ur_bool))`;;
635 (`!x. x <: boolset <=> (x = true) \/ (x = false)`,
636 REWRITE_TAC[inset; boolset; true_def; false_def] THEN
637 SIMP_TAC[MK_V_SET; SUBSET_REFL] THEN
638 REWRITE_TAC[setlevel_INJ; setlevel] THEN
639 SUBGOAL_THEN `IMAGE I_BOOL UNIV = {I_BOOL F,I_BOOL T}` SUBST1_TAC THENL
640 [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
644 GEN_REWRITE_TAC (RAND_CONV o BINOP_CONV o LAND_CONV) [GSYM SET] THEN
645 REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
646 SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
647 [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
648 ASM_MESON_TAC[V_TYBIJ; ELEMENT_IN_LEVEL; PAIR_EQ]]);;
650 let TRUE_NE_FALSE = prove
652 REWRITE_TAC[true_def; false_def] THEN
653 DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN
654 SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
655 [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
656 ASM_MESON_TAC[V_TYBIJ; I_BOOL; PAIR_EQ]]);;
658 let BOOLEAN_EQ = prove
659 (`!x y. x <: boolset /\ y <: boolset /\
660 ((x = true) <=> (y = true))
662 MESON_TAC[TRUE_NE_FALSE; IN_BOOL]);;
664 (* ------------------------------------------------------------------------- *)
666 (* ------------------------------------------------------------------------- *)
668 let indset = new_definition
669 `indset = mk_V(Powerset Ur_ind,I_SET (setlevel Ur_ind) (setlevel Ur_ind))`;;
671 let INDSET_IND_MODEL = prove
672 (`?f. (!i:ind_model. f(i) <: indset) /\ (!i j. (f i = f j) ==> (i = j))`,
673 EXISTS_TAC `\i. mk_V(Ur_ind,I_IND i)` THEN REWRITE_TAC[] THEN
674 SUBGOAL_THEN `!i. (I_IND i) IN setlevel Ur_ind` ASSUME_TAC THENL
675 [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[]; ALL_TAC] THEN
676 ASM_SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; indset; MK_V_CLAUSES] THEN
677 ASM_MESON_TAC[V_TYBIJ; I_IND; ELEMENT_IN_LEVEL; PAIR_EQ]);;
679 let INDSET_INHABITED = prove
681 MESON_TAC[INDSET_IND_MODEL]);;
683 (* ------------------------------------------------------------------------- *)
684 (* Axiom of choice (this is trivially so in HOL anyway, but...) *)
685 (* ------------------------------------------------------------------------- *)
689 (`?ch. !s. (?x. x <: s) ==> ch(s) <: s`,
690 REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[]) in
691 new_specification ["ch"] th;;
693 (* ------------------------------------------------------------------------- *)
694 (* Sanity check lemmas. *)
695 (* ------------------------------------------------------------------------- *)
697 let IN_POWERSET = prove
698 (`!x s. x <: powerset s <=> x <=: s`,
699 MESON_TAC[POWERSET]);;
701 let IN_PRODUCT = prove
702 (`!z s t. z <: product s t <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
703 MESON_TAC[PRODUCT]);;
705 let IN_COMPREHENSION = prove
706 (`!p s x. x <: s suchthat p <=> x <: s /\ p x`,
707 MESON_TAC[SUCHTHAT]);;
709 let PRODUCT_INHABITED = prove
710 (`(?x. x <: s) /\ (?y. y <: t) ==> ?z. z <: product s t`,
711 MESON_TAC[IN_PRODUCT]);;
713 (* ------------------------------------------------------------------------- *)
714 (* Definition of function space. *)
715 (* ------------------------------------------------------------------------- *)
717 let funspace = new_definition
719 powerset(product s t) suchthat
720 (\u. !x. x <: s ==> ?!y. pair x y <: u)`;;
722 let apply_def = new_definition
723 `apply f x = @y. pair x y <: f`;;
725 let abstract = new_definition
727 (product s t) suchthat (\z. !x y. (pair x y = z) ==> (y = f x))`;;
729 let APPLY_ABSTRACT = prove
730 (`!x s t. x <: s /\ f(x) <: t ==> (apply(abstract s t f) x = f(x))`,
731 REPEAT STRIP_TAC THEN
732 REWRITE_TAC[apply_def; abstract; IN_PRODUCT; SUCHTHAT] THEN
733 MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[PAIR_INJ] THEN
736 let APPLY_IN_RANSPACE = prove
737 (`!f x s t. x <: s /\ f <: funspace s t ==> apply f x <: t`,
738 REWRITE_TAC[funspace; SUCHTHAT; IN_POWERSET; IN_PRODUCT; subset_def] THEN
739 REWRITE_TAC[apply_def] THEN MESON_TAC[PAIR_INJ]);;
741 let ABSTRACT_IN_FUNSPACE = prove
742 (`!f x s t. (!x. x <: s ==> f(x) <: t)
743 ==> abstract s t f <: funspace s t`,
744 REWRITE_TAC[funspace; abstract; SUCHTHAT; IN_POWERSET; IN_PRODUCT;
745 subset_def; PAIR_INJ] THEN
746 SIMP_TAC[LEFT_FORALL_IMP_THM; GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
747 REWRITE_TAC[UNWIND_THM1; EXISTS_REFL] THEN MESON_TAC[]);;
749 let FUNSPACE_INHABITED = prove
750 (`!s t. ((?x. x <: s) ==> (?y. y <: t)) ==> ?f. f <: funspace s t`,
751 REPEAT STRIP_TAC THEN
752 EXISTS_TAC `abstract s t (\x. @y. y <: t)` THEN
753 MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN ASM_MESON_TAC[]);;
755 let ABSTRACT_EQ = prove
758 (!x. x <: s ==> f(x) <: t1 /\ g(x) <: t2 /\ (f x = g x))
759 ==> (abstract s t1 f = abstract s t2 g)`,
760 REWRITE_TAC[abstract] THEN REPEAT STRIP_TAC THEN
761 MATCH_MP_TAC EXTENSIONALITY_NONEMPTY THEN
762 REWRITE_TAC[SUCHTHAT; IN_PRODUCT] THEN REPEAT CONJ_TAC THEN
763 REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
764 SIMP_TAC[TAUT `(a /\ b /\ c) /\ d <=> ~(a ==> b /\ c ==> ~d)`] THEN
765 REWRITE_TAC[PAIR_INJ] THEN SIMP_TAC[LEFT_FORALL_IMP_THM] THENL
766 [ASM_MESON_TAC[]; ASM_MESON_TAC[]; ALL_TAC] THEN
767 ASM_REWRITE_TAC[PAIR_INJ] THEN
768 REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
769 REWRITE_TAC[NOT_IMP] THEN GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
770 ASM_REWRITE_TAC[PAIR_INJ] THEN ASM_MESON_TAC[]);;
772 (* ------------------------------------------------------------------------- *)
773 (* Special case of treating a Boolean function as a set. *)
774 (* ------------------------------------------------------------------------- *)
776 let boolean = new_definition
777 `boolean b = if b then true else false`;;
779 let holds = new_definition
780 `holds s x <=> (apply s x = true)`;;
782 let BOOLEAN_IN_BOOLSET = prove
783 (`!b. boolean b <: boolset`,
784 REWRITE_TAC[boolean] THEN MESON_TAC[IN_BOOL]);;
786 let BOOLEAN_EQ_TRUE = prove
787 (`!b. (boolean b = true) <=> b`,
788 REWRITE_TAC[boolean] THEN MESON_TAC[TRUE_NE_FALSE]);;