1open HolKernel boolLib Parse bossLib
2
3open vbgsetTheory vbgnatsTheory
4open boolSimps
5
6val _ = new_theory "ordinal"
7
8val poc_def = Define`
9  poc A R ���
10    (���x. x ��� A ��� R x x) ���
11    (���x y z. x ��� A ��� y ��� A ��� z ��� A ��� R x y ��� R y z ��� R x z) ���
12    (���x y. x ��� A ��� y ��� A ��� R x y ��� R y x ��� (x = y))
13`;
14
15val chain_def = Define`
16  chain A R C ��� C ��� A ��� ���x y. x ��� C ��� y ��� C ��� R x y ��� R y x
17`
18
19val totalR_def = Define`
20  totalR A R ��� poc A R ��� ���x y. x ��� A ��� y ��� A ��� R x y ��� R y x
21`;
22
23val iseg_def = Define`
24  iseg A R x = SPEC0 (��y. y ��� A ��� R y x ��� x ��� y ��� x ��� A)
25`;
26
27val iseg_SUBSET = store_thm(
28  "iseg_SUBSET",
29  ``���x y. x ��� A ��� y ��� A ��� poc A R ��� R x y ��� iseg A R x ��� iseg A R y``,
30  rpt strip_tac >>
31  `���x y z. x ��� A ��� y ��� A ��� z ��� A ��� R x y ��� R y z ��� R x z` by fs[poc_def] >>
32  rw[iseg_def, SUBSET_def, SPEC0] >- metis_tac [] >>
33  `R u y` by metis_tac [] >>
34  strip_tac >> srw_tac [][] >>
35  `���x y. x ��� A ��� y ��� A ��� R x y ��� R y x ��� (x = y)` by fs[poc_def] >>
36  metis_tac[]);
37
38val woclass_def = Define`
39  woclass A R ���
40     totalR A R ���
41     ���B. B ��� A ��� B ��� {} ��� ���e. e ��� B ��� ���d. d ��� B ��� R e d
42`;
43
44val Nats_SETs = prove(``n ��� Nats ��� SET n``, metis_tac [SET_def])
45val _ = augment_srw_ss [rewrites [Nats_SETs]]
46
47val Nats_wo = store_thm(
48  "Nats_wo",
49  ``woclass Nats (��x y. x ��� y)``,
50  rw[woclass_def, totalR_def, poc_def, LE_ANTISYM]
51    >- metis_tac [LE_TRANS]
52    >- metis_tac [LE_TOTAL] >>
53  `���e. e ��� B` by (fs[EXTENSION] >> metis_tac[]) >>
54  metis_tac [Nats_least_element]);
55
56val ordinal_def = Define`
57  ordinal �� ��� SET �� ��� transitive �� ���
58              (���x y. x ��� �� ��� y ��� �� ��� x ��� y ��� y ��� x ��� (x = y))
59`;
60
61val Ord_def = Define`Ord = SPEC0 (��s. ordinal s)`
62
63val _ = clear_overloads_on "<="
64
65val ordle_def = Define`
66  ordle x y ��� x ��� y ��� (x = y)
67`;
68
69val _ = overload_on ("<=", ``ordle``)
70
71val ordle_REFL = store_thm(
72  "ordle_REFL",
73  ``x:vbgc ��� x``,
74  rw[ordle_def])
75val _ = export_rewrites ["ordle_REFL"]
76
77val woclass_thm = store_thm(
78  "woclass_thm",
79  ``woclass A R ��� (���x y. x ��� A ��� y ��� A ��� R x y ��� R y x ��� (x = y)) ���
80                  ���B. B ��� A ��� B ��� {} ��� ���e. e ��� B ��� ���d. d ��� B ��� R e d``,
81  rw[woclass_def, EQ_IMP_THM]
82    >- fs[totalR_def, poc_def] >>
83  rw[totalR_def, poc_def]
84    >- ((* reflexivity *)
85        first_x_assum (qspec_then `{x}` mp_tac) >>
86        `{x} ��� {}`
87           by (rw[Once EXTENSION] >> metis_tac [SET_def]) >>
88        srw_tac [CONJ_ss][SUBSET_def])
89    >- ((* transitivity *)
90        first_x_assum (qspec_then `{x;y;z}` mp_tac) >>
91        `SET x ��� SET y ��� SET z` by metis_tac [SET_def] >>
92        `{x;y;z} ��� {}`
93           by rw[Once EXTENSION, EXISTS_OR_THM] >>
94        srw_tac[CONJ_ss, DNF_ss][SUBSET_def] >> metis_tac [])
95    >- ((* totality *)
96        first_x_assum (qspec_then `{x;y}` mp_tac) >>
97        `SET x ��� SET y` by metis_tac [SET_def] >>
98        `{x;y} ��� {}`
99           by rw[Once EXTENSION, EXISTS_OR_THM] >>
100        srw_tac[CONJ_ss, DNF_ss][SUBSET_def]))
101
102val EMPTY_ordinal = store_thm(
103  "EMPTY_ordinal",
104  ``ordinal {}``,
105  rw[ordinal_def, transitive_def])
106val _ = export_rewrites ["EMPTY_ordinal"]
107
108val ORDINALS_CONTAIN_ORDINALS = store_thm(
109  "ORDINALS_CONTAIN_ORDINALS",
110  ``����� ��. ordinal �� ��� �� ��� �� ��� ordinal ��``,
111  rw[ordinal_def]
112    >- metis_tac [SET_def]
113    >- (fs[transitive_def] >>
114        `���e. e ��� �� ��� e ��� ��` by metis_tac [SUBSET_def] >>
115        qx_gen_tac `x` >> rw[] >>
116        simp[SUBSET_def] >> SPOSE_NOT_THEN MP_TAC >>
117        DISCH_THEN (Q.X_CHOOSE_THEN `u` STRIP_ASSUME_TAC) >>
118        `x ��� ��` by metis_tac [] >>
119        `u ��� ��` by metis_tac [SUBSET_def] >>
120        `u ��� �� ��� �� ��� u ��� (�� = u)` by metis_tac [] >>
121        metis_tac [IN3_ANTISYM, IN_ANTISYM])
122   >- metis_tac [transitive_def, SUBSET_def])
123
124val ORD_INDUCTION = store_thm(
125  "ORD_INDUCTION",
126  ``(���a. ordinal a ��� (���x. x ��� a ��� P x) ��� P a) ��� ���a. ordinal a ��� P a``,
127  strip_tac >>
128  qsuff_tac `���a. SET a ��� ordinal a ��� P a`
129    >- metis_tac [SET_def, ordinal_def] >>
130  Induct_on `SET a` >> rw[] >> metis_tac [ORDINALS_CONTAIN_ORDINALS]);
131val _ = IndDefLib.export_rule_induction "ORD_INDUCTION"
132
133val EMPTY_LE_ORDS = store_thm(
134  "EMPTY_LE_ORDS",
135  ``�����. ordinal �� ��� {} ��� ��``,
136  Induct_on `ordinal ��` >> rw[] >>
137  Cases_on `�� = {}` >> rw[] >>
138  `�����. �� ��� ��` by metis_tac [EMPTY_UNIQUE] >>
139  `{} ��� ��` by metis_tac [] >>
140  fs[ordle_def] >> metis_tac [transitive_ALT, ordinal_def]);
141
142val ords_segs = store_thm(
143  "ords_segs",
144  ``�����. ordinal �� ��� (iseg Ord ordle �� = ��)``,
145  rw[Ord_def, ordinal_def, iseg_def] >> rw[Once EXTENSION] >>
146  rw[EQ_IMP_THM] >| [
147    fs[ordle_def],
148    metis_tac [SET_def],
149    metis_tac [SET_def],
150    metis_tac [SET_def],
151    fs[transitive_ALT] >> metis_tac [IN_REFL, IN_ANTISYM, IN3_ANTISYM],
152    metis_tac [transitive_ALT],
153    rw[ordle_def],
154    metis_tac [IN_REFL]
155  ])
156
157val ords_segs2 = store_thm(
158  "ords_segs2",
159  ``ordinal �� ��� e ��� �� ��� (iseg �� ordle e = e)``,
160  rw[ordinal_def, iseg_def] >> rw[Once EXTENSION] >>
161  EQ_TAC >- srw_tac[CONJ_ss][ordle_def] >>
162  metis_tac [SET_def, ordle_def, IN_REFL, transitive_ALT]);
163
164
165val orderiso_def = Define`
166  orderiso A B R ��� ���f. (���x. x ��� A ��� f x ��� B) ���
167                       (���x1 x2. x1 ��� A ��� x2 ��� A ���
168                                ((f x1 = f x2)  ��� (x1 = x2))) ���
169                       (���y. y ��� B ��� ���x. x ��� A ��� (f x = y)) ���
170                       (���x1 x2. x1 ��� A ��� x2 ��� A ��� R x1 x2 ��� R (f x1) (f x2))
171`;
172
173val ordle_wo = store_thm(
174  "ordle_wo",
175  ``ordinal �� ��� woclass �� ordle``,
176  rw[woclass_thm, Ord_def]
177    >- ((* antisymmetry *)
178        fs[ordinal_def, transitive_def] >>
179        Cases_on `x = y` >- rw[] >>
180        `x ��� y ��� y ��� x` by metis_tac [ordle_def] >>
181        metis_tac [IN_ANTISYM])
182    >- ((* existence of least members *)
183        `���x. x ��� B ��� (x ��� B = {})` by metis_tac [FOUNDATION3] >>
184        qexists_tac `x` >> rw[] >>
185        `d ��� x` by (fs [Once EXTENSION] >> metis_tac [SET_def]) >>
186        metis_tac [ordinal_def, ordle_def, SUBSET_def]));
187
188val wlog_seteq = store_thm(
189  "wlog_seteq",
190  ``(���a b. Q a b ��� Q b a) ��� (���a b. Q a b ��� a ��� b) ���
191    (���a b. Q a b ��� (a = b))``,
192  rpt strip_tac >>
193  qsuff_tac `a ��� b ��� b ��� a` >- metis_tac[SUBSET_def, EXTENSION] >>
194  metis_tac []);
195
196val orderiso_ordinals = store_thm(
197  "orderiso_ordinals",
198  ``����� ��. ordinal �� ��� ordinal �� ��� orderiso �� �� $<= ��� (�� = ��)``,
199  ho_match_mp_tac wlog_seteq >> conj_tac
200    >- (rw[orderiso_def]>>
201        `���a. a ��� �� ��� ���!b. b ��� �� ��� (a = f b)` by metis_tac [] >>
202        qabbrev_tac `g = ��a. @b. b ��� �� ��� (a = f b)` >>
203        qexists_tac `g` >> qunabbrev_tac `g` >> rw[] >| [
204          SELECT_ELIM_TAC >> rw[] >> metis_tac [],
205          SELECT_ELIM_TAC >> conj_tac >- metis_tac [] >> rw[] >>
206          SELECT_ELIM_TAC >> metis_tac [],
207          qexists_tac `f y` >> rw[] >> SELECT_ELIM_TAC >>
208          srw_tac [CONJ_ss][],
209          SELECT_ELIM_TAC >> conj_tac >- metis_tac [] >> rw[] >>
210          SELECT_ELIM_TAC >> conj_tac >- metis_tac[] >>
211          qx_gen_tac `b` >> rw[] >>
212          `x ��� b ��� (x = b) ��� b ��� x` by metis_tac [ordinal_def] >| [
213             rw[ordle_def],
214             rw[ordle_def],
215             `b ��� x` by rw[ordle_def] >>
216             `f b ��� f x` by metis_tac[] >>
217             pop_assum mp_tac >> simp_tac (srw_ss()) [ordle_def] >>
218             rw[] >> fs[ordle_def] >> metis_tac [IN_ANTISYM, IN_REFL]
219          ]
220        ]) >>
221  rpt strip_tac >>
222  spose_not_then assume_tac >>
223  `���x. x ��� �� ��� x ��� ��` by metis_tac [SUBSET_def] >>
224  fs[orderiso_def] >>
225  `f x ��� x` by metis_tac []>>
226  qabbrev_tac `E = SPEC0 (��y. y ��� �� ��� y ��� f y)` >>
227  `E ��� {}` by (rw[Once EXTENSION, Abbr`E`] >> metis_tac[SET_def]) >>
228  `E ��� ��` by rw[SUBSET_def, Abbr`E`] >>
229  `���e. e ��� E ��� ���d. d ��� E ��� e ��� d` by metis_tac [ordle_wo, woclass_def] >>
230  `e ��� �� ��� f e ��� ��` by metis_tac [SUBSET_def] >>
231  `e ��� f e` by fs[Abbr`E`] >>
232  `���d. d ��� e ��� (f d = d)`
233     by (qx_gen_tac `d` >> strip_tac >>
234         `��(e ��� d)` by metis_tac [IN_REFL, IN_ANTISYM, ordle_def] >>
235         `d ��� ��`
236           by metis_tac [SUBSET_def, ordinal_def, transitive_def] >>
237         `d ��� E` by metis_tac [] >>
238         pop_assum mp_tac >> qunabbrev_tac `E` >>
239         simp[] >> metis_tac [SET_def]) >>
240  `ordinal e ��� ordinal (f e)`
241     by metis_tac [ORDINALS_CONTAIN_ORDINALS, SUBSET_def] >>
242  `iseg �� $<= e = SPEC0 (��x. ���y. y ��� iseg �� $<= e ��� (x = f y))`
243     by (rw[iseg_def] >> simp[Once EXTENSION] >>
244         qx_gen_tac `e'` >> EQ_TAC >> rw[] >-
245           (qexists_tac `e'` >> fs[ordle_def]) >>
246         fs[ordle_def]) >>
247  `_ = iseg �� $<= (f e)`
248     by (rw[iseg_def] >> simp[Once EXTENSION] >>
249         qx_gen_tac `b` >> EQ_TAC >>
250         asm_simp_tac (srw_ss() ++ DNF_ss) [] >>
251         strip_tac >>
252         `���b0. b0 ��� �� ��� (f b0 = b)` by metis_tac [] >>
253         qexists_tac `b0` >> simp[] >> BasicProvers.VAR_EQ_TAC >>
254         `SET b0` by metis_tac [SET_def] >>
255         `e ��� ��` by metis_tac [SUBSET_def] >>
256         `e ��� b0` by metis_tac [] >> simp[ordle_def] >>
257         `e ��� b0 ��� b0 ��� e` by metis_tac [ordinal_def] >>
258         `f e ��� f b0` by metis_tac [ordle_def] >>
259         metis_tac [ordle_def, IN_REFL, IN_ANTISYM]) >>
260  `_ = f e` by metis_tac [ords_segs2] >>
261  `iseg �� ordle e = e` by metis_tac [ords_segs2] >>
262  metis_tac [])
263
264
265
266
267val _ = export_theory()
268
269
270
271