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