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