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