1(* Playing around with what is really Morse-Kelley set theory *)
2
3open HolKernel boolLib bossLib Parse
4open boolSimps
5
6val _ = new_theory "vbgset"
7val _ = ParseExtras.temp_loose_equality()
8
9(* hide constants from the existing (typed) set theory *)
10val _ = app (ignore o hide) ["UNION", "IN", "SUBSET", "EMPTY", "INSERT",
11                             "CROSS", "INTER", "BIGINTER", "BIGUNION"]
12
13(* create a new type (of VBG classes) *)
14val _ = new_type("vbgc", 0)
15
16(* with this call, the syntax with ��� is enabled as well. *)
17val _ = new_constant ("IN", ``:vbgc -> vbgc -> bool``)
18
19(* similarly, this abbreviation also allows for ��� *)
20val _ = overload_on ("NOTIN", ``��x y. ~(x ��� y)``)
21
22val SET_def = Define` SET(x) = ���w. x ��� w `
23val SUBSET_def = Define`x ��� y <=> ���u. u ��� x ��� u ��� y`
24
25val EXTENSION = new_axiom ("EXTENSION", ``(a = b) <=> (���x. x ��� a <=> x ��� b)``)
26
27val SPECIFICATION = new_axiom(
28  "SPECIFICATION",
29  ``���(P : vbgc -> bool). ���w. ���x. x ��� w <=> SET(x) ��� P(x)``);
30
31val SPEC0 = new_specification(
32  "SPEC0",
33  ["SPEC0"],
34  CONV_RULE SKOLEM_CONV SPECIFICATION);
35val _ = export_rewrites ["SPEC0"]
36
37val EMPTY_def = Define`EMPTY = SPEC0 (��x. F)`
38
39val NOT_IN_EMPTY = store_thm(
40  "NOT_IN_EMPTY",
41  ``x ��� {}``,
42  SRW_TAC [][EMPTY_def]);
43val _ = export_rewrites ["NOT_IN_EMPTY"]
44
45val EMPTY_UNIQUE = store_thm(
46  "EMPTY_UNIQUE",
47  ``(���x. x ��� u) ��� (u = {})``,
48  SRW_TAC [][EXTENSION]);
49
50val INFINITY = new_axiom(
51  "INFINITY",
52  ``���w. SET w ��� (���u. u ��� w ��� ���x. x ��� u) ���
53        ���x. x ��� w ��� ���y. y ��� w ��� ���u. u ��� y <=> u ��� x ��� (u = x)``);
54
55val EMPTY_SET = store_thm(
56  "EMPTY_SET",
57  ``SET {}``,
58  STRIP_ASSUME_TAC INFINITY THEN
59  `u = {}` by SRW_TAC [][EMPTY_UNIQUE] THEN
60  `SET u` by METIS_TAC [SET_def] THEN
61  METIS_TAC []);
62val _ = export_rewrites ["EMPTY_SET"]
63
64val EMPTY_SUBSET = store_thm(
65  "EMPTY_SUBSET",
66  ``{} ��� A ��� (A ��� {} <=> (A = {}))``,
67  SRW_TAC [][SUBSET_def] THEN METIS_TAC [EMPTY_UNIQUE, NOT_IN_EMPTY]);
68val _ = export_rewrites ["EMPTY_SUBSET"]
69
70val SUBSET_REFL = store_thm(
71  "SUBSET_REFL",
72  ``A ��� A``,
73  SRW_TAC [][SUBSET_def]);
74val _ = export_rewrites ["SUBSET_REFL"]
75
76val SUBSET_ANTISYM = store_thm(
77  "SUBSET_ANTISYM",
78  ``(x = y) <=> x ��� y ��� y ��� x``,
79  SRW_TAC [][EXTENSION, SUBSET_def] THEN METIS_TAC []);
80
81val SUBSET_TRANS = store_thm(
82  "SUBSET_TRANS",
83  ``x ��� y ��� y ��� z ��� x ��� z``,
84  SRW_TAC [][SUBSET_def])
85
86val Sets_def = Define`Sets = SPEC0 (��x. T)`
87
88val SET_Sets = store_thm(
89  "SET_Sets",
90  ``x ��� Sets <=> SET x``,
91  SRW_TAC [][Sets_def]);
92
93val SUBSET_Sets = store_thm(
94  "SUBSET_Sets",
95  ``x ��� Sets``,
96  SRW_TAC [][SUBSET_def, SET_Sets, SET_def] THEN METIS_TAC []);
97
98val RUS_def = Define`
99  RUS = SPEC0 (\x. x ��� x)
100`;
101
102(* gives result
103     ��� RUS ��� RUS ��� SET RUS ��� RUS ��� RUS
104*)
105val RUSlemma =
106``RUS ��� RUS``
107    |> (SIMP_CONV bool_ss [RUS_def, Once SPEC0] THENC
108        SIMP_CONV bool_ss [GSYM RUS_def])
109
110val RUS_not_SET = store_thm(
111  "RUS_not_SET",
112  ``�� SET RUS``,
113  METIS_TAC [RUSlemma]);
114
115val POW_def = Define`POW A = SPEC0 (��x. x ��� A)`
116val IN_POW = store_thm(
117  "IN_POW",
118  ``x ��� POW A ��� SET x ��� x ��� A``,
119  SRW_TAC [][POW_def]);
120val _ = export_rewrites ["IN_POW"]
121
122val POWERSET = new_axiom(
123  "POWERSET",
124  ``SET a ��� ���w. SET w ��� ���x. x ��� a ��� x ��� w``);
125
126val SUBSETS_ARE_SETS = store_thm(
127  "SUBSETS_ARE_SETS",
128  ``���A B. SET A ��� B ��� A ��� SET B``,
129  REPEAT STRIP_TAC THEN IMP_RES_TAC POWERSET THEN
130  `B ��� w` by METIS_TAC [] THEN
131  METIS_TAC [SET_def]);
132
133val POW_SET_CLOSED = store_thm(
134  "POW_SET_CLOSED",
135  ``���a. SET a ��� SET (POW a)``,
136  REPEAT STRIP_TAC THEN IMP_RES_TAC POWERSET THEN
137  MATCH_MP_TAC SUBSETS_ARE_SETS THEN
138  Q.EXISTS_TAC `w` THEN SRW_TAC [][Once SUBSET_def]);
139
140
141val SINGC_def = Define`
142  SINGC a = SPEC0 (��x. x = a)
143`
144
145
146val PCLASS_SINGC_EMPTY = store_thm(
147  "PCLASS_SINGC_EMPTY",
148  ``��SET a ��� (SINGC a = {})``,
149  SRW_TAC [][SINGC_def, Once EXTENSION]);
150
151val SET_IN_SINGC = store_thm(
152  "SET_IN_SINGC",
153  ``SET a ��� (x ��� SINGC a ��� (x = a))``,
154  SRW_TAC [CONJ_ss][SINGC_def]);
155
156val SINGC_11 = store_thm(
157  "SINGC_11",
158  ``SET x ��� SET y ��� ((SINGC x = SINGC y) = (x = y))``,
159  SRW_TAC [][Once EXTENSION, SimpLHS] THEN
160  SRW_TAC [][SET_IN_SINGC] THEN METIS_TAC []);
161val _ = export_rewrites ["SINGC_11"]
162
163
164val PAIRC_def = Define`PAIRC a b = SPEC0 (��x. (x = a) ��� (x = b))`
165
166val SINGC_PAIRC = store_thm(
167  "SINGC_PAIRC",
168  ``SINGC a = PAIRC a a``,
169  SRW_TAC [][SINGC_def, PAIRC_def]);
170
171val PCLASS_PAIRC_EMPTY = store_thm(
172  "PCLASS_PAIRC_EMPTY",
173  ``��SET a ��� ��SET b ��� (PAIRC a b = {})``,
174  SRW_TAC [][PAIRC_def, Once EXTENSION] THEN
175  Cases_on `x = a` THEN SRW_TAC [][] THEN
176  Cases_on `x = b` THEN SRW_TAC [][]);
177
178val SET_IN_PAIRC = store_thm(
179  "SET_IN_PAIRC",
180  ``SET a ��� SET b ��� (���x. x ��� PAIRC a b ��� (x = a) ��� (x = b))``,
181  SRW_TAC [CONJ_ss, DNF_ss][PAIRC_def]);
182
183val UNORDERED_PAIRS = new_axiom(
184  "UNORDERED_PAIRS",
185  ``SET a ��� SET b ��� ���w. SET w ��� a ��� w ��� b ��� w``);
186
187val PAIRC_SET_CLOSED = store_thm(
188  "PAIRC_SET_CLOSED",
189  ``SET a ��� SET b ��� SET (PAIRC a b)``,
190  DISCH_THEN (fn th => STRIP_ASSUME_TAC (MATCH_MP UNORDERED_PAIRS th) THEN
191                       STRIP_ASSUME_TAC th) THEN
192  MATCH_MP_TAC SUBSETS_ARE_SETS THEN Q.EXISTS_TAC `w` THEN
193  SRW_TAC [][SUBSET_def, SET_IN_PAIRC] THEN SRW_TAC [][]);
194
195val SINGC_SET = store_thm(
196  "SINGC_SET",
197  ``SET (SINGC a)``,
198  Cases_on `SET a` THEN1 SRW_TAC [][SINGC_PAIRC, PAIRC_SET_CLOSED] THEN
199  SRW_TAC [][PCLASS_SINGC_EMPTY]);
200val _ = export_rewrites ["SINGC_SET"]
201
202(* UNION ish operations *)
203
204val UNION_def = Define`a ��� b = SPEC0 (��x. x ��� a ��� x ��� b)`
205
206val IN_UNION = store_thm(
207  "IN_UNION",
208  ``x ��� A ��� B ��� x ��� A ��� x ��� B``,
209  SRW_TAC [][UNION_def] THEN METIS_TAC [SET_def]);
210val _ = export_rewrites ["IN_UNION"]
211
212val BIGUNION_def = Define`BIGUNION A = SPEC0 (��x. ���y. y ��� A ��� x ��� y)`
213val IN_BIGUNION = store_thm(
214  "IN_BIGUNION",
215  ``x ��� BIGUNION A ��� ���y. y ��� A ��� x ��� y``,
216  SRW_TAC [][BIGUNION_def] THEN METIS_TAC [SET_def]);
217val _ = export_rewrites ["IN_BIGUNION"]
218
219val EMPTY_UNION = store_thm(
220  "EMPTY_UNION",
221  ``({} ��� A = A) ��� (A ��� {} = A)``,
222  SRW_TAC [][EXTENSION]);
223val _ = export_rewrites ["EMPTY_UNION"]
224
225val UNIONS = new_axiom(
226  "UNIONS",
227  ``SET a ��� ���w. SET w ��� ���x y. x ��� y ��� y ��� a ��� x ��� w``);
228
229val UNION_SET_CLOSED = store_thm(
230  "UNION_SET_CLOSED",
231  ``SET (A ��� B) ��� SET A ��� SET B``,
232  Tactical.REVERSE EQ_TAC >| [
233    STRIP_TAC THEN
234    `SET (PAIRC A B)` by METIS_TAC [PAIRC_SET_CLOSED] THEN
235    POP_ASSUM (STRIP_ASSUME_TAC o MATCH_MP UNIONS) THEN
236    POP_ASSUM MP_TAC THEN
237    ASM_SIMP_TAC (srw_ss() ++ DNF_ss)[SET_IN_PAIRC] THEN
238    STRIP_TAC THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN Q.EXISTS_TAC `w` THEN
239    SRW_TAC [][SUBSET_def] THEN SRW_TAC [][],
240    strip_tac >> conj_tac >> match_mp_tac SUBSETS_ARE_SETS >>
241    qexists_tac `A ��� B` >> srw_tac [][SUBSET_def]
242  ]);
243val _ = export_rewrites ["UNION_SET_CLOSED"]
244
245val BIGUNION_SET_CLOSED = store_thm(
246  "BIGUNION_SET_CLOSED",
247  ``SET A ��� SET (BIGUNION A)``,
248  STRIP_TAC THEN IMP_RES_TAC UNIONS THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN
249  Q.EXISTS_TAC `w` THEN ASM_SIMP_TAC (srw_ss()) [SUBSET_def] THEN
250  METIS_TAC []);
251
252(* intersections *)
253val INTER_def = Define`
254  s1 INTER s2 = SPEC0 (��e. e ��� s1 ��� e ��� s2)
255`;
256
257val IN_INTER = store_thm(
258  "IN_INTER",
259  ``e ��� s1 ��� s2 ��� SET e ��� e ��� s1 ��� e ��� s2``,
260  rw [INTER_def]);
261val _ = export_rewrites ["IN_INTER"]
262
263val INTER_SET_CLOSED = store_thm(
264  "INTER_SET_CLOSED",
265  ``(SET s1 ��� SET (s1 ��� s2)) ��� (SET s2 ��� SET (s1 ��� s2))``,
266  rpt strip_tac >> match_mp_tac SUBSETS_ARE_SETS >| [
267    qexists_tac `s1`,
268    qexists_tac `s2`
269  ] >> rw[SUBSET_def]);
270val _ = export_rewrites ["INTER_SET_CLOSED"]
271
272val INSERT_def = Define`x INSERT y = SINGC x ��� y`
273
274val IN_INSERT = store_thm(
275  "IN_INSERT",
276  ``x ��� a INSERT A ��� SET a ��� (x = a) ��� x ��� A``,
277  SRW_TAC [][INSERT_def] THEN Cases_on `SET a` THEN
278  SRW_TAC [][SET_IN_SINGC, PCLASS_SINGC_EMPTY]);
279val _ = export_rewrites ["IN_INSERT"]
280
281val SET_INSERT = store_thm(
282  "SET_INSERT",
283  ``SET (x INSERT b) = SET b``,
284  SRW_TAC [][INSERT_def])
285val _ = export_rewrites ["SET_INSERT"]
286
287val INSERT_IDEM = store_thm(
288  "INSERT_IDEM",
289  ``a INSERT a INSERT s = a INSERT s``,
290  SRW_TAC [][Once EXTENSION] THEN METIS_TAC []);
291val _ = export_rewrites ["INSERT_IDEM"]
292
293val SUBSET_SING = store_thm(
294  "SUBSET_SING",
295  ``x ��� {a} ��� SET a ��� (x = {a}) ��� (x = {})``,
296  SRW_TAC [][SUBSET_def] THEN EQ_TAC THENL [
297    Cases_on `SET a` THEN SRW_TAC [][] THENL [
298      Cases_on `x = {}` THEN SRW_TAC [][] THEN
299      SRW_TAC [][Once EXTENSION] THEN
300      `���b. b ��� x` by METIS_TAC [EMPTY_UNIQUE] THEN
301      METIS_TAC [],
302      METIS_TAC [EMPTY_UNIQUE]
303    ],
304    SIMP_TAC (srw_ss()) [DISJ_IMP_THM]
305  ]);
306val _ = export_rewrites ["SUBSET_SING"]
307
308val BIGUNION_EMPTY = store_thm(
309  "BIGUNION_EMPTY",
310  ``(BIGUNION {} = {}) ��� (BIGUNION {{}} = {})``,
311  CONJ_TAC THEN SRW_TAC [][Once EXTENSION]);
312val _ = export_rewrites ["BIGUNION_EMPTY"]
313
314val BIGUNION_SING = store_thm(
315  "BIGUNION_SING",
316  ``SET a ��� (BIGUNION {a} = a)``,
317  SRW_TAC [][Once EXTENSION]);
318
319val BIGUNION_UNION = store_thm(
320  "BIGUNION_UNION",
321  ``SET a ��� SET b ��� (BIGUNION {a;b} = a ��� b)``,
322  SRW_TAC [DNF_ss][Once EXTENSION]);
323
324val POW_EMPTY = store_thm(
325  "POW_EMPTY",
326  ``POW {} = {{}}``,
327  SRW_TAC [][Once EXTENSION] THEN SRW_TAC [CONJ_ss][]);
328
329val POW_SING = store_thm(
330  "POW_SING",
331  ``SET a ��� (POW {a} = {{}; {a}})``,
332  SRW_TAC [][Once EXTENSION] THEN
333  ASM_SIMP_TAC (srw_ss() ++ CONJ_ss ++ DNF_ss) [] THEN
334  METIS_TAC []);
335
336(* "primitive ordered pair" *)
337val POPAIR_def = Define`POPAIR a b = {{a}; {a;b}}`
338
339val POPAIR_SET = store_thm(
340  "POPAIR_SET",
341  ``SET (POPAIR a b)``,
342  SRW_TAC [][POPAIR_def]);
343val _ = export_rewrites ["POPAIR_SET"]
344
345val SING_11 = store_thm(
346  "SING_11",
347  ``SET a ��� SET b ��� (({a} = {b}) = (a = b))``,
348  STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [SimpLHS, Once EXTENSION] THEN
349  SRW_TAC [][] THEN METIS_TAC []);
350
351val SING_EQ_PAIR = store_thm(
352  "SING_EQ_PAIR",
353  ``SET a ��� SET b ��� SET c ��� (({a;b} = {c}) = (a = b) ��� (b = c))``,
354  STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [SimpLHS, Once EXTENSION] THEN
355  SRW_TAC [][] THEN METIS_TAC []);
356
357val PAIR_EQ_PAIR = store_thm(
358  "PAIR_EQ_PAIR",
359  ``SET a ��� SET b ��� SET c ��� SET d ���
360    (({a;b} = {c;d}) ��� (a = c) ��� (b = d) ��� (a = d) ��� (b = c))``,
361  STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [Once EXTENSION, SimpLHS] THEN
362  SRW_TAC [][] THEN METIS_TAC []);
363
364val POPAIR_INJ = store_thm(
365  "POPAIR_INJ",
366  ``SET a ��� SET b ��� SET c ��� SET d ���
367    ((POPAIR a b = POPAIR c d) ��� (a = c) ��� (b = d))``,
368  STRIP_TAC THEN SRW_TAC [][SimpLHS, Once EXTENSION] THEN
369  SRW_TAC [][POPAIR_def] THEN REVERSE EQ_TAC THEN1 SRW_TAC [][] THEN
370  METIS_TAC [SING_11, SING_EQ_PAIR, PAIR_EQ_PAIR]);
371
372(* ordered pairs that work when classes are involved *)
373val OPAIR_def = Define`
374  OPAIR a b = SPEC0 (��x. ���y. y ��� a ��� (x = POPAIR {} y)) ���
375              SPEC0 (��x. ���y. y ��� b ��� (x = POPAIR {{}} y))
376`;
377
378val SET_OPAIR = store_thm(
379  "SET_OPAIR",
380  ``SET a ��� SET b ��� SET (OPAIR a b)``,
381  SRW_TAC [][OPAIR_def] THENL[
382    SRW_TAC [][POPAIR_def] THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN
383    SRW_TAC [DNF_ss][SUBSET_def] THEN
384    Q.EXISTS_TAC `POW (POW (a ��� {{}}))` THEN
385    SRW_TAC [][POW_SET_CLOSED] THEN
386    ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUBSET_def],
387    SRW_TAC [][POPAIR_def] THEN MATCH_MP_TAC SUBSETS_ARE_SETS THEN
388    SRW_TAC [DNF_ss][SUBSET_def] THEN
389    Q.EXISTS_TAC `POW (POW (b ��� {{{}}}))` THEN
390    SRW_TAC [][POW_SET_CLOSED] THEN
391    ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUBSET_def]
392  ]);
393val _ = export_rewrites ["SET_OPAIR"]
394
395val ZERO_NEQ_ONE = store_thm(
396  "ZERO_NEQ_ONE",
397  ``{} ��� {{}}``,
398  SRW_TAC [][EXTENSION] THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][]);
399val _ = export_rewrites ["ZERO_NEQ_ONE"]
400
401val POPAIR_01 = store_thm(
402  "POPAIR_01",
403  ``POPAIR {} x ��� POPAIR {{}} y``,
404  SRW_TAC [][POPAIR_def] THEN SRW_TAC [][Once EXTENSION] THEN
405  Q.EXISTS_TAC `{{}}` THEN SRW_TAC [][SING_11] THEN
406  SRW_TAC [][Once EXTENSION] THEN Q.EXISTS_TAC `{{}}` THEN
407  SRW_TAC [][]);
408
409val OPAIR_11 = store_thm(
410  "OPAIR_11",
411  ``((OPAIR a b = OPAIR c d) ��� (a = c) ��� (b = d))``,
412  SRW_TAC [][Once EXTENSION, SimpLHS] THEN
413  SRW_TAC [][OPAIR_def] THEN
414  REVERSE EQ_TAC THEN1 SRW_TAC [][] THEN
415  REPEAT STRIP_TAC THENL [
416    SIMP_TAC (srw_ss()) [EXTENSION, EQ_IMP_THM] THEN
417    Q.X_GEN_TAC `e` THEN REPEAT STRIP_TAC THEN
418    `SET e` by METIS_TAC [SET_def] THEN
419    FIRST_X_ASSUM (Q.SPEC_THEN `POPAIR {} e` MP_TAC) THEN
420    ASM_SIMP_TAC (srw_ss()) [POPAIR_01] THENL [
421      DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #1 o
422                  EQ_IMP_RULE),
423      DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #2 o
424                  EQ_IMP_RULE)
425    ] THEN
426    DISCH_THEN (Q.SPEC_THEN `e` MP_TAC) THEN SRW_TAC [][] THEN
427    POP_ASSUM MP_TAC THEN
428    `SET y` by METIS_TAC [SET_def] THEN
429    SRW_TAC [][POPAIR_INJ],
430
431    SIMP_TAC (srw_ss()) [EXTENSION, EQ_IMP_THM] THEN
432    Q.X_GEN_TAC `e` THEN REPEAT STRIP_TAC THEN
433    `SET e` by METIS_TAC [SET_def] THEN
434    FIRST_X_ASSUM (Q.SPEC_THEN `POPAIR {{}} e` MP_TAC) THEN
435    ASM_SIMP_TAC (srw_ss()) [POPAIR_01] THENL [
436      DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #1 o
437                  EQ_IMP_RULE),
438      DISCH_THEN (MP_TAC o CONV_RULE LEFT_IMP_EXISTS_CONV o #2 o
439                  EQ_IMP_RULE)
440    ] THEN
441    DISCH_THEN (Q.SPEC_THEN `e` MP_TAC) THEN SRW_TAC [][] THEN
442    POP_ASSUM MP_TAC THEN
443    `SET y` by METIS_TAC [SET_def] THEN
444    SRW_TAC [][POPAIR_INJ]
445  ]);
446val _ = export_rewrites ["OPAIR_11"]
447
448val _ = add_rule { fixity = Closefix,
449                   term_name = "OPAIR",
450                   block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
451                   paren_style = OnlyIfNecessary,
452                   pp_elements = [TOK "���", TM, HardSpace 1,
453                                  TOK "��", BreakSpace(1,2),
454                                  TM, TOK "���"]}
455
456val CROSS_def = Define`
457  s1 CROSS s2 = SPEC0 (��x. ���a b. a ��� s1 ��� b ��� s2 ��� (x = ���a �� b���))
458`;
459
460val FunSpace_def = Define`
461  FunSpace A B = SPEC0 (��f. f ��� A �� B ��� ���a. a ��� A ��� ���!b. ���a �� b��� ��� f)
462`
463
464val id_def = Define`
465  id A = SPEC0 (��x. ���a. a ��� A ��� (x = ���a��a���))
466`;
467
468(*
469val apply_def = new_specification("apply_def",
470  ["apply"],
471  CONV_RULE SKOLEM_CONV
472            (prove(``���f x A B. f ��� FunSpace A B ��� x ��� A ���
473                               ���y. y ��� B ��� ���x��y��� ��� f``,
474                   SRW_TAC [][FunSpace_def, SPEC0, CROSS_def] THEN
475                   RES_TAC THEN
476                   FULL_SIMP_TAC (srw_ss()) [EXISTS_UNIQUE_THM] THEN
477                   Q.EXISTS_TAC `b` THEN SRW_TAC [][] THEN
478                   FULL_SIMP_TAC (srw_ss()) [SUBSET_def, SPEC0] THEN
479                   RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [OPAIR_11])
480*)
481
482
483(*
484val FORMATION = new_axiom(
485
486*)
487
488val FOUNDATION = new_axiom(
489  "FOUNDATION",
490  ``(���a. SET a ��� a ��� w ��� a ��� w) ��� ���a. SET a ��� a ��� w``);
491
492val IN_INDUCTION = store_thm(
493  "IN_INDUCTION",
494  ``(���a. SET a ��� (���x. x ��� a ��� P x) ��� P a) ��� ���a. SET a ��� P a``,
495  rpt strip_tac >>
496  MP_TAC (INST [``w:vbgc`` |-> ``SPEC0 (��x. P x)``] FOUNDATION) >>
497  rw[SUBSET_def]);
498val _ = IndDefLib.export_rule_induction "IN_INDUCTION"
499
500val IN_REFL = store_thm(
501  "IN_REFL",
502  ``x ��� x``,
503  Cases_on `SET x` >| [
504    pop_assum mp_tac >> qid_spec_tac `x` >>
505    ho_match_mp_tac IN_INDUCTION >> metis_tac [],
506    fs[SET_def]
507  ]);
508val _ = export_rewrites ["IN_REFL"]
509
510val IN_ANTISYM = store_thm(
511  "IN_ANTISYM",
512  ``x ��� y ��� y ��� x ��� F``,
513  qsuff_tac `���x. SET x ��� ���y. y ��� x ��� x ��� y` >- metis_tac [SET_def] >>
514  Induct_on `SET x` >> metis_tac []);
515
516val IN3_ANTISYM = store_thm(
517  "IN3_ANTISYM",
518  ``x ��� y ��� y ��� z ��� z ��� x ��� F``,
519  qsuff_tac `���x. SET x ��� ���y z. y ��� z ��� z ��� x ��� x ��� y` >- metis_tac [SET_def] >>
520  Induct_on `SET x` >> metis_tac []);
521
522val FORMATION = new_axiom(
523  "FORMATION",
524  ``SET a ��� (���x. x ��� a ��� ���!y. P x y) ��� (���x y. x ��� a ��� P x y ��� SET y) ���
525    ���w. SET w ��� ���y. y ��� w ��� ���x. x ��� a ��� P x y``);
526
527val bad_def = with_flag (computeLib.auto_import_definitions, false) Define`
528  bad f a = SET a ��� (���i. SET (f i)) ��� (f 0 = {a}) ���
529            (���i x. x ��� f i ��� x ��� f (i + 1) ��� {})
530`;
531
532val FOUNDATION2 = store_thm(
533  "FOUNDATION2",
534  ``�����f:num -> vbgc.
535       (���i. SET (f i)) ��� (���e. SET e ��� (f 0 = {e})) ���
536       (���i x. x ��� f i ��� x ��� f (i + 1) ��� {})``,
537  qsuff_tac `���a. SET a ��� �����f. bad f a`
538    >- (rw[bad_def] >>
539        Tactical.REVERSE (Cases_on `���i. SET (f i)`) >- metis_tac [] >>
540        rw[] >> Cases_on `���e. f 0 = {e}` >> fs[] >>
541        Tactical.REVERSE (Cases_on `SET e`)
542          >- (DISJ1_TAC >> rw[Once EXTENSION]) >>
543        DISJ2_TAC >>
544        first_x_assum (qspec_then `e` mp_tac) >> rw[] >>
545        metis_tac []) >>
546  Induct_on `SET a` >> qx_gen_tac `a` >> Cases_on `SET a` >> simp[] >>
547  CONV_TAC CONTRAPOS_CONV >> rw[] >>
548  `a ��� f 0` by metis_tac [IN_INSERT, bad_def] >>
549  `a ��� f 1 ��� {}` by metis_tac [bad_def, DECIDE ``0 + 1 = 1``] >>
550  `���b. b ��� a ��� f 1` by metis_tac [EMPTY_UNIQUE] >>
551  qabbrev_tac `
552    poor = ��p. (���i. p i ��� f (i + 1)) ��� b ��� p 0 ���
553               (���i x. x ��� p i ��� x ��� f (i + 2) ��� p (i + 1))
554  ` >>
555  qabbrev_tac `P = ��n. f (n + 1)` >>
556  `poor P`
557     by (srw_tac[ARITH_ss][Abbr`P`,Abbr`poor`] >> fs[] >>
558         rw[SUBSET_def]) >>
559  qabbrev_tac `N = ��n. SPEC0 (��x. ���p. poor p ��� x ��� p n)` >>
560  `b ��� N 0`
561     by (rw[Abbr`N`] >- metis_tac [SET_def] >> fs[Abbr`poor`]) >>
562  `poor N`
563     by (qpat_assum `Abbrev(poor = X)`
564                    (fn th => ASSUME_TAC th THEN MP_TAC th) >>
565         disch_then (SUBST1_TAC o REWRITE_RULE [markerTheory.Abbrev_def]) >>
566         BETA_TAC >> ASM_REWRITE_TAC[] >> rpt strip_tac >| [
567           qsuff_tac `N i ��� P i` >- metis_tac [SUBSET_def] >>
568           rw[Abbr`N`, SUBSET_def],
569           `���p. poor p ��� x ��� f(i + 2) ��� p (i + 1)`
570              by (rpt strip_tac >>
571                  `x ��� p i` by fs[Abbr`N`, Abbr`poor`] >>
572                  metis_tac []) >>
573           rw[Abbr`N`, SUBSET_def] >> metis_tac [SUBSET_def, IN_INTER]
574         ]) >>
575  qexists_tac `b` >> fs[] >>
576  `���p. poor p ��� ���n. SET (p n)`
577     by (rw[Abbr`poor`] >> match_mp_tac SUBSETS_ARE_SETS  >>
578         qexists_tac `f (n + 1)` >> fs[bad_def]) >>
579  qexists_tac `N` >> rw[bad_def] >|[
580    rw[Once EXTENSION, EQ_IMP_THM] >>
581    spose_not_then assume_tac >>
582    qpat_assum `x ��� N 0` mp_tac >>
583    qpat_assum `Abbrev(N = X)`
584      (fn th => ASSUME_TAC th >>
585                MP_TAC (REWRITE_RULE [markerTheory.Abbrev_def] th)) >>
586    disch_then SUBST1_TAC >> BETA_TAC >> rw[] >> DISJ2_TAC >>
587    qexists_tac `��n. if n = 0 then SPEC0 (��y. y ��� N 0 ��� y ��� x) else N n` >>
588    rw[] >>
589    qpat_assum `Abbrev(poor = X)`
590      (fn th => assume_tac th >>
591                SUBST1_TAC (REWRITE_RULE [markerTheory.Abbrev_def] th)) >>
592    BETA_TAC >> ASM_REWRITE_TAC [] THEN BETA_TAC >> simp[] >> conj_tac
593      >- (rw[SUBSET_def] >>
594          qpat_assum `poor N` mp_tac >>
595          rw[Abbr`poor`] >> metis_tac [SUBSET_def, DECIDE ``0 + 1 = 1``]) >>
596    map_every qx_gen_tac [`i`, `y`] >>
597    rw[] >> metis_tac [DECIDE ``(0 + 1 = 1) ��� (0 + 2 = 2)``],
598    `x ��� f (i + 1)` by metis_tac[SUBSET_def] >>
599    `x ��� f(i + 2) ��� N (i + 1)` by metis_tac [] >>
600    `x ��� f(i + 2) ��� {}` by metis_tac [bad_def, DECIDE ``i + 1 + 1 = i + 2``] >>
601    simp[EXTENSION] >> metis_tac[SET_def, EMPTY_UNIQUE, IN_INTER, SUBSET_def]
602  ])
603
604val lemma0 = prove(
605  ``SET ss ��� SET ss ��� ���x. x ��� ss ��� SET (x ��� a)``,
606  rw[] >> match_mp_tac SUBSETS_ARE_SETS >> qexists_tac `x` >>
607  rw[SUBSET_def] >> metis_tac [SET_def])
608val formlemma =
609    FORMATION |> Q.INST [`a` |-> `ss`,
610                         `P` |-> `��x y. (y = x ��� a)`]
611              |> SIMP_RULE (srw_ss()) []
612              |> C MP (UNDISCH lemma0)
613
614val FOUNDATION3 = store_thm(
615  "FOUNDATION3",
616  ``���a. a ��� {} ��� ���x. x ��� a ��� (x ��� a = {})``,
617  spose_not_then strip_assume_tac >>
618  `���b. b ��� a` by metis_tac [EMPTY_UNIQUE] >>
619  qabbrev_tac `
620     m = PRIM_REC {b} (��s n. BIGUNION (SPEC0 (��y. ���x. x ��� s ��� (y = x ��� a))))
621  ` >>
622  `���i. m i ��� a`
623     by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM, SUBSET_def] >>
624         fs[]) >>
625  `���i. SET (m i)`
626     by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>
627         match_mp_tac BIGUNION_SET_CLOSED >>
628         qpat_assum `SET sss` mp_tac >>
629         qmatch_abbrev_tac `SET ss ��� SET sss` >>
630         qunabbrev_tac `sss` >> strip_tac >>
631         strip_assume_tac formlemma >>
632         qsuff_tac `SPEC0 (��y. ���x. x ��� ss ��� (y = x ��� a)) = w` >- rw[] >>
633         simp[Once EXTENSION, EQ_IMP_THM] >>
634         asm_simp_tac (srw_ss() ++ DNF_ss) [] >> qx_gen_tac `y` >> strip_tac >>
635         match_mp_tac SUBSETS_ARE_SETS >> qexists_tac `y` >>
636         metis_tac [SUBSET_def, SET_def, IN_INTER]) >>
637  `bad m b`
638     by (rw[bad_def]
639            >- metis_tac [SET_def]
640            >- rw[Abbr`m`, prim_recTheory.PRIM_REC_THM]
641            >- (`x ��� a` by metis_tac [SUBSET_def] >>
642                `x ��� a ��� {}` by metis_tac [] >>
643                `���y. y ��� x ��� a` by metis_tac [EMPTY_UNIQUE] >>
644                `y ��� m (SUC i)`
645                   by (rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>
646                       srw_tac [DNF_ss][] >>
647                       qexists_tac `x` >> rw[]
648                         >- (match_mp_tac SUBSETS_ARE_SETS >>
649                             qexists_tac `x` >>
650                             metis_tac [SUBSET_def, IN_INTER, SET_def])
651                         >- metis_tac [SET_def]
652                         >> fs[]) >>
653                fs[arithmeticTheory.ADD1] >>
654                rw[Once EXTENSION] >> metis_tac [SET_def])) >>
655  MP_TAC (FOUNDATION2 |> SIMP_RULE bool_ss []
656                      |> Q.SPEC `m`) >>
657  simp[] >> conj_tac
658     >- (qexists_tac `b` >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>
659         metis_tac [SET_def]) >>
660  metis_tac [bad_def])
661
662val _ = delete_const "bad"
663
664val _ = export_theory()
665