1open HolKernel Parse bossLib boolLib pred_setTheory relationTheory set_relationTheory arithmeticTheory pairTheory listTheory optionTheory prim_recTheory whileTheory rich_listTheory sortingTheory 2 3(* open relationTheoryHelperTheory *) 4 5val _ = new_theory "generalHelpers" 6 7val NONEMPTY_LEMM = store_thm 8 ("NONEMPTY_LEMM", 9 ``!s. ~(s = {}) ==> ?e s'. (s = {e} ��� s') /\ ~(e ��� s')``, 10 rpt strip_tac >> fs[] >> qexists_tac `CHOICE s` 11 >> qexists_tac `s DIFF {CHOICE s}` >> strip_tac 12 >- (`(s ��� {CHOICE s} ��� (s DIFF {CHOICE s})) 13 /\ ({CHOICE s} ��� (s DIFF {CHOICE s}) ��� s)` 14 suffices_by metis_tac[SET_EQ_SUBSET] 15 >> strip_tac >> (fs[SUBSET_DEF,CHOICE_DEF])) 16 >- simp[DIFF_DEF] 17 ); 18 19val RRESTRICT_TRANS = store_thm 20 ("RRESTRICT_TRANS", 21 ``!s r. transitive r ==> transitive (rrestrict r s)``, 22 rpt strip_tac >> fs[transitive_def, rrestrict_def] 23 >> rpt strip_tac >> metis_tac[] 24 ); 25 26val RRESTRICT_ANTISYM = store_thm 27 ("RRESTRICT_ANTISYM", 28 ``!s r. antisym r ==> antisym (rrestrict r s)``, 29 rpt strip_tac >> fs[antisym_def, in_rrestrict] 30 ); 31 32val ADD_N_INJ_LEMM = store_thm 33 ("ADD_N_INJ_LEMM", 34 ``!n x y. ((\x. x+n ) x = (\x. x+n) y) ==> (x = y)``, 35 rpt strip_tac >> Induct_on `n` >> fs[] 36 >> rw[ADD_SUC] 37 ); 38 39val ADD_N_IMAGE_LEMM = store_thm 40 ("ADD_N_IMAGE_LEMM", 41 ``!n. IMAGE (\x. x+n) ����(:num) = { x | x >= n }``, 42 strip_tac >> fs[IMAGE_DEF] 43 >> `({n + x | x | T} ��� {x | x ��� n}) /\ ({x | x ��� n} ��� {n + x | x | T})` 44 suffices_by metis_tac[SET_EQ_SUBSET] 45 >> rpt strip_tac >> fs[SUBSET_DEF] 46 >> rpt strip_tac 47 >> qexists_tac `x - n` >> simp[] 48 ); 49 50val SUBS_UNION_LEMM = store_thm 51 ("SUBS_UNION_LEMM", 52 ``!s s1 s2. (s = s1) \/ (s = s2) ==> (s ��� s1 ��� s2)``, 53 rpt strip_tac >> metis_tac[SUBSET_UNION] 54 ); 55 56val SUBS_UNION_LEMM2 = store_thm 57 ("SUBS_UNION_LEMM2", 58 ``!s s1 s2 s3. s ��� s1 ��� s2 /\ s1 ��� s3 ==> s ��� s3 ��� s2``, 59 fs[UNION_DEF, SUBSET_DEF] >> rpt strip_tac 60 >> `x ��� s1 \/ x ��� s2` by metis_tac[] 61 >> metis_tac[] 62 ); 63 64val INFINITE_DIFF_FINITE = store_thm 65 ("INFINITE_DIFF_FINITE", 66 ``!s t. INFINITE s ��� FINITE t ==> INFINITE (s DIFF t)``, 67 rpt strip_tac >> metis_tac[FINITE_DIFF_down] 68 ); 69 70val INSERT_LEMM = store_thm 71 ("INSERT_LEMM", 72 ``!f q e s. {f q | q ��� e INSERT s } = f e INSERT {f q | q ��� s }``, 73 fs[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac 74 >> metis_tac[] 75 ); 76 77val POW_11 = store_thm 78 ("POW_11", 79 ``!s1 s2. (POW s1 = POW s2) = (s1 = s2)``, 80 simp[EQ_IMP_THM] >> fs[] 81 >> `���s1 s2. (POW s1 = POW s2) ��� s1 ��� s2` suffices_by metis_tac[SET_EQ_SUBSET] 82 >> fs[SET_EQ_SUBSET,SUBSET_DEF,POW_DEF] >> rpt strip_tac 83 >> `(���x'. x' ��� {x} ��� x' ��� s1) ��� ���x'. x' ��� {x} ��� x' ��� s2` by metis_tac[] 84 >> `���x'. x' ��� {x} ��� x' ��� s2` by ( 85 `(���x'. x' ��� {x} ��� x' ��� s1)` suffices_by metis_tac[] 86 >> simp[] 87 ) 88 >> fs[] 89 ); 90 91val IN_BIGINTER_SUBSET = store_thm 92 ("IN_BIGINTER_SUBSET", 93 ``!x P. (x ��� P) ==> (BIGINTER P ��� x)``, 94 rpt strip_tac 95 >> `x INSERT P = P` by simp[SET_EQ_SUBSET,SUBSET_DEF] 96 >> `x ��� BIGINTER P = BIGINTER P` by metis_tac[BIGINTER_INSERT] 97 >> metis_tac[INTER_SUBSET] 98 ); 99 100val NO_BOUNDS_INFINITE = store_thm 101 ("NO_BOUNDS_INFINITE", 102 ``!f. (!i. i <= f i) 103 ==> INFINITE { f i | i ��� ����(:num) }``, 104 rpt strip_tac >> fs[FINITE_WEAK_ENUMERATE] 105 >> `linear_order (rrestrict (rel_to_reln $<=) {f' n | n < b }) {f' n | n < b }` 106 by (fs[linear_order_def,rrestrict_def,rel_to_reln_def] >> rpt strip_tac 107 >- (fs[domain_def, SUBSET_DEF] >> rpt strip_tac 108 >> metis_tac[] 109 ) 110 >- (fs[range_def, SUBSET_DEF] >> rpt strip_tac 111 >> metis_tac[]) 112 >- (fs[transitive_def, SUBSET_DEF] >> rpt strip_tac 113 >> metis_tac[]) 114 >- (fs[antisym_def, SUBSET_DEF] >> rpt strip_tac 115 >> metis_tac[]) 116 ) 117 >> `FINITE {f' n | n < b }` by ( 118 `FINITE {f' n | n ��� count b }` suffices_by fs[IN_ABS,count_def] 119 >> metis_tac[IMAGE_DEF,FINITE_COUNT,IMAGE_FINITE] 120 ) 121 >> Cases_on `b = 0` 122 >- (`~ !e. (?i. e = f i)` by fs[] 123 >> fs[]) 124 >- (`~({f' n | n < b} = {})` by ( 125 `?x. x ��� {f' n | n < b}` suffices_by fs[MEMBER_NOT_EMPTY] 126 >> fs[] >> `b-1 < b` by simp[] >> metis_tac[] 127 ) 128 >> `?x. x ��� maximal_elements {f' n | n < b } 129 (rrestrict (rel_to_reln $<=) {f' n | n < b })` 130 by metis_tac[finite_linear_order_has_maximal] 131 >> `(���i. f (SUC x) = f i) ��� ���n. n < b ��� (f (SUC x) = f' n)` by fs[] 132 >> `(���i. f (SUC x) = f i)` by metis_tac[] 133 >> `~?n. n < b ��� (f (SUC x) = f' n)` suffices_by metis_tac[] 134 >> fs[] >> rpt strip_tac 135 >> CCONTR_TAC >> fs[] 136 >> `SUC x <= f (SUC x)` by fs[] 137 >> `f' n <= x` by ( 138 fs[maximal_elements_def, rrestrict_def, rel_to_reln_def] 139 >> first_x_assum (qspec_then `f' n` mp_tac) 140 >> rpt strip_tac >> fs[] 141 >> CCONTR_TAC 142 >> `x < f' n` by metis_tac[DECIDE ``~(f' n <= f' n') = (f' n' < f' n)``] 143 >> `x = f' n` by metis_tac[DECIDE ``x < f' n ==> x <= f' n``] 144 >> fs[] 145 ) 146 >> fs[] 147 ) 148 ); 149 150val FIXPOINT_EXISTS = store_thm 151 ("FIXPOINT_EXISTS", 152 ``!Rel f. WF Rel /\ (!y. (RC Rel) (f y) y) 153 ==> (!x. ?n. !m. (m >= n) ==> (FUNPOW f m x = FUNPOW f n x))``, 154 rpt gen_tac >> strip_tac 155 >> IMP_RES_THEN ho_match_mp_tac WF_INDUCTION_THM 156 >> rpt strip_tac 157 >> `Rel (f x) x \/ (f x = x)` by metis_tac[RC_DEF] 158 >- (`���n. ���m. m ��� n ��� (FUNPOW f m (f x) = FUNPOW f n (f x))` by metis_tac[] 159 >> qexists_tac `SUC n` >> simp[FUNPOW] >> rpt strip_tac 160 >> qabbrev_tac `FIX = FUNPOW f n (f x)` 161 >> first_x_assum (qspec_then `SUC n` mp_tac) >> simp[FUNPOW_SUC] 162 >> strip_tac >> Induct_on `m` >> simp[] >> strip_tac 163 >> simp[FUNPOW_SUC] 164 >> Cases_on `m = n` 165 >- (rw[] >> metis_tac[FUNPOW, FUNPOW_SUC]) 166 >- (`m >= SUC n` by simp[] >> metis_tac[]) 167 ) 168 >- (exists_tac ``0`` >> simp[FUNPOW] >> Induct_on `m` >> simp[FUNPOW]) 169 ); 170 171val char_def = Define `char �� p = { a | (a ��� ��) /\ (p ��� a)}`; 172 173val char_neg_def = Define `char_neg �� p = �� DIFF (char �� p)`; 174 175val CHAR_LEMM = store_thm 176 ("CHAR_LEMM", 177 ``!�� x. char �� x ��� ��``, 178 fs[char_def,SUBSET_DEF] >> rpt strip_tac 179 ); 180 181val CHAR_NEG_LEMM = store_thm 182 ("CHAR_NEG_LEMM", 183 ``!�� x. char_neg �� x ��� ��``, 184 fs[char_neg_def,DIFF_SUBSET] 185 ); 186 187val d_conj_def = Define 188 `d_conj d1 d2 = { (a1 ��� a2, e1 ��� e2) | ((a1,e1) ��� d1) /\ ((a2,e2) ��� d2)}`; 189 190val d_conj_set_def = Define` 191 d_conj_set ts �� = ITSET (d_conj o SND) ts {(��, {})}`; 192 193val D_CONJ_UNION_DISTR = store_thm 194 ("D_CONJ_UNION_DISTR", 195 ``!s t d. d_conj s (t ��� d) = (d_conj s t) ��� (d_conj s d)``, 196 rpt strip_tac >> fs[d_conj_def] >> rw[SET_EQ_SUBSET] 197 >> fs[SUBSET_DEF] >> rpt strip_tac >> metis_tac[] 198 ); 199val D_CONJ_FINITE = store_thm 200 ("D_CONJ_FINITE", 201 ``!s d. FINITE s ��� FINITE d ==> FINITE (d_conj s d)``, 202 rpt gen_tac 203 >> `d_conj s d = {(a1 ��� a2, e1 ��� e2) | ((a1,e1),a2,e2) ��� s �� d}` 204 by fs[CROSS_DEF, FST, SND, d_conj_def] 205 >> rpt strip_tac 206 >> qabbrev_tac `f = (��((a1,e1),(a2,e2)). (a1 ��� a2, e1 ��� e2))` 207 >> `d_conj s d = {f ((a1,e1),a2,e2) | ((a1,e1),a2,e2) ��� s �� d}` by ( 208 qunabbrev_tac `f` >> fs[SET_EQ_SUBSET, SUBSET_DEF] >> rpt strip_tac 209 >> fs[] >> metis_tac[] 210 ) 211 >> `FINITE (s �� d)` by metis_tac[FINITE_CROSS] 212 >> `d_conj s d = IMAGE f (s �� d)` by ( 213 fs[IMAGE_DEF] >> fs[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 214 >- metis_tac[FST,SND] 215 >- (Cases_on `x'` >> Cases_on `q` >> Cases_on `r` 216 >> qunabbrev_tac `f` 217 >> qexists_tac `q'` >> qexists_tac `q` >> qexists_tac `r'` 218 >> qexists_tac `r''` >> fs[] 219 ) 220 ) 221 >> metis_tac[IMAGE_FINITE] 222 ); 223 224val D_CONJ_ASSOC = store_thm 225 ("D_CONJ_ASSOC", 226 ``!s d t. d_conj s (d_conj d t) = d_conj (d_conj s d) t``, 227 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[d_conj_def] 228 >> metis_tac[INTER_ASSOC,UNION_ASSOC] 229 ); 230 231val D_CONJ_COMMUTES = store_thm 232 ("D_CONJ_COMMUTES", 233 ``!s d t. d_conj s (d_conj d t) = d_conj d (d_conj s t)``, 234 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[d_conj_def] 235 >- (qexists_tac `a1'` >> qexists_tac `a1 ��� a2'` 236 >> qexists_tac `e1'` >> qexists_tac `e1 ��� e2'` 237 >> rpt strip_tac 238 >- metis_tac[INTER_COMM, INTER_ASSOC] 239 >- metis_tac[UNION_COMM, UNION_ASSOC] 240 >- metis_tac[] 241 >- metis_tac[] 242 ) 243 >- (qexists_tac `a1'` >> qexists_tac `a1 ��� a2'` 244 >> qexists_tac `e1'` >> qexists_tac `e1 ��� e2'` 245 >> rpt strip_tac 246 >- metis_tac[INTER_COMM, INTER_ASSOC] 247 >- metis_tac[UNION_COMM, UNION_ASSOC] 248 >- metis_tac[] 249 >- metis_tac[] 250 ) 251 ); 252 253val D_CONJ_SND_COMMUTES = store_thm 254 ("D_CONJ_SND_COMMUTES", 255 ``!s d t. (d_conj o SND) s ((d_conj o SND) d t) 256 = (d_conj o SND) d ((d_conj o SND) s t)``, 257 rpt strip_tac >> fs[SND] >> metis_tac[D_CONJ_COMMUTES] 258 ); 259 260val D_CONJ_SET_RECURSES = store_thm 261 ("D_CONJ_SET_RECURSES", 262 ``!s. FINITE s ==> 263 ���e b. ITSET (d_conj o SND) (e INSERT s) b = 264 (d_conj o SND) e (ITSET (d_conj o SND) (s DELETE e) b)``, 265 rpt strip_tac 266 >> HO_MATCH_MP_TAC COMMUTING_ITSET_RECURSES 267 >> metis_tac[D_CONJ_SND_COMMUTES] 268 ); 269 270(* val D_CONJ_SET_SND = store_thm *) 271(* ("D_CONJ_SET_SND", *) 272(* ``!aP s1. FINITE s1 ==> *) 273(* !s2. FINITE s2 ==> *) 274(* ((IMAGE SND s1 = IMAGE SND s2) ��� FINITE s1 ��� FINITE s2 *) 275(* ==> (d_conj_set s1 aP = d_conj_set s2 aP))``, *) 276(* gen_tac >> Induct_on `s1` >> fs[] >> rpt strip_tac *) 277(* >- (`s2 = {}` by metis_tac[IMAGE_EQ_EMPTY] >> fs[d_conj_set_def,ITSET_THM]) *) 278(* >- (`IMAGE SND s1 ��� IMAGE SND s2` by ( *) 279(* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 280(* >> simp[INSERT_DEF] >> rpt strip_tac >> simp[SUBSET_DEF] *) 281(* >> rpt strip_tac *) 282(* >> `x ��� {y | y = SND e ��� ���x. y = SND x ��� x ��� s1}` by ( *) 283(* fs[] >> disj2_tac >> metis_tac[] *) 284(* ) *) 285(* >> `x ��� IMAGE SND s2` by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] *) 286(* >> fs[IMAGE_DEF] >> metis_tac[] *) 287(* ) *) 288(* >> `IMAGE SND s2 ��� IMAGE SND s1 ��� {SND e}` by ( *) 289(* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 290(* >> PURE_REWRITE_TAC[INSERT_DEF] >> rpt strip_tac *) 291(* >> simp[SUBSET_DEF] >> rpt strip_tac *) 292(* >> `x ��� IMAGE SND s2` by (simp[] >> metis_tac[]) *) 293(* >> `x ��� {y | y = SND e ��� y ��� IMAGE SND s1}` *) 294(* by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] *) 295(* >> fs[] >> disj1_tac >> metis_tac[] *) 296(* ) *) 297(* >> fs[d_conj_set_def] >> simp[D_CONJ_SET_RECURSES] *) 298(* >> Cases_on `SND e ��� IMAGE SND s1` *) 299(* >- ( *) 300(* `IMAGE SND s1 = IMAGE SND s2` by ( *) 301(* simp[IMAGE_DEF] *) 302(* >> `{SND x | x ��� s1} ��� {SND x | x ��� s2} *) 303(* ��� {SND x | x ��� s2} ��� {SND x | x ��� s1}` *) 304(* suffices_by metis_tac[SET_EQ_SUBSET] *) 305(* >> simp[SUBSET_DEF] >> rpt strip_tac *) 306(* >- (`x ��� IMAGE SND s1` by (simp[] >> metis_tac[]) *) 307(* >> `x ��� IMAGE SND s2` by metis_tac[SUBSET_DEF] *) 308(* >> fs[] >> metis_tac[] *) 309(* ) *) 310(* >- (`x ��� IMAGE SND s2` by (simp[] >> metis_tac[]) *) 311(* >> `x ��� IMAGE SND s1 ��� {SND e}` by metis_tac[SUBSET_DEF] *) 312(* >> fs[UNION_DEF] >> metis_tac[] *) 313(* ) *) 314(* ) *) 315(* >> `?x. x ��� s1 ��� SND x = SND e ��� ~(x = e)` by ( *) 316(* fs[IMAGE_DEF] >> metis_tac[] *) 317(* ) *) 318(* >> `IMAGE SND (s1 DELETE e) = IMAGE SND s1` by ( *) 319(* simp[IMAGE_DEF] *) 320(* ) *) 321(* >> *) 322(* >> `(IMAGE SND s2) DELETE (SND e) = IMAGE SND s1` by ( *) 323(* simp[DELETE_DEF] *) 324(* >> `IMAGE SND s2 DIFF {SND e} ��� IMAGE SND s1 *) 325(* ��� IMAGE SND s1 ��� IMAGE SND s2 DIFF {SND e}` *) 326(* suffices_by fs[SET_EQ_SUBSET] *) 327(* >> simp[SUBSET_DEF] >> rpt strip_tac *) 328(* >- (rw[] *) 329(* >> `SND x' ��� IMAGE SND s1` by ( *) 330(* `IMAGE SND s2 ��� SND e INSERT IMAGE SND s1` *) 331(* by metis_tac[SET_EQ_SUBSET] *) 332(* >> `SND x' ��� IMAGE SND s2` by simp[IMAGE_DEF] *) 333(* >> `SND x' ��� SND e INSERT IMAGE SND s1` *) 334(* by metis_tac[SUBSET_DEF] *) 335(* >> `~(SND x' = SND e)` by fs[] *) 336(* >> POP_ASSUM mp_tac >> simp[INSERT_DEF] *) 337(* ) *) 338(* >> fs[IMAGE_DEF] >> metis_tac[] *) 339(* ) *) 340(* >- (`IMAGE SND s1 ��� IMAGE SND s2` by ( *) 341(* rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac *) 342(* >> simp[INSERT_DEF] >> rpt strip_tac >> simp[SUBSET_DEF] *) 343(* >> rpt strip_tac *) 344(* >> `x ��� {y | y = SND e ��� ���x. y = SND x ��� x ��� s1}` by ( *) 345(* fs[] >> disj2_tac >> metis_tac[] *) 346(* ) *) 347(* >> `x ��� IMAGE SND s2` by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] *) 348(* >> fs[IMAGE_DEF] >> metis_tac[] *) 349(* ) *) 350(* >> `x ��� IMAGE SND s1` by (simp[IMAGE_DEF] >> metis_tac[]) *) 351(* >> `x ��� IMAGE SND s2` by metis_tac[SUBSET_DEF] *) 352(* >> fs[IMAGE_DEF] >> metis_tac[] *) 353(* ) *) 354(* >- (rw[] >> ) *) 355 356 357 358(* ) *) 359 360 361 362val D_CONJ_SET_LEMM = store_thm 363 ("D_CONJ_SET_LEMM", 364 ``!A s. FINITE s ==> !a e.(a,e) ��� d_conj_set s A 365 ==> (!q d. (q,d) ��� s ==> ?a' e'. (a',e') ��� d ��� a ��� a' ��� e' ��� e)``, 366 gen_tac >> Induct_on `s` >> rpt strip_tac >> fs[NOT_IN_EMPTY] 367 >> `(a,e') ��� (d_conj o SND) e (d_conj_set s A)` by ( 368 fs[d_conj_set_def, DELETE_NON_ELEMENT] 369 >> `(a,e') ��� (d_conj o SND) e (ITSET (d_conj ��� SND) s {(A,���)})` suffices_by fs[] 370 >> metis_tac[D_CONJ_SET_RECURSES] 371 ) 372 >- (fs[d_conj_def] >> first_x_assum (qspec_then `a2` mp_tac) 373 >> rpt strip_tac >> first_x_assum (qspec_then `e2` mp_tac) 374 >> rpt strip_tac >> fs[] 375 >> `���q d. (q,d) ��� s ��� ���a' e'. (a',e') ��� d ��� a2 ��� a' ��� e' ��� e2` by ( 376 rpt strip_tac >> metis_tac[] 377 ) 378 >> qexists_tac `a1` >> qexists_tac `e1` >> fs[SND] >> metis_tac[SND] 379 ) 380 >- (fs[d_conj_def] 381 >> `���a' e'. (a',e') ��� d ��� a2 ��� a' ��� e' ��� e2` by metis_tac[] 382 >> qexists_tac `a'` >> qexists_tac `e''` 383 >> metis_tac[SUBSET_DEF,IN_INTER,IN_UNION] 384 ) 385 ); 386 387val D_CONJ_SET_LEMM2 = store_thm 388 ("D_CONJ_SET_LEMM2", 389 ``!A s a e. FINITE s ��� (a,e) ��� d_conj_set s A 390 ==> (!q d. (q,d) ��� s ==> ?a' e'. (a',e') ��� d ��� a ��� a' ��� e' ��� e)``, 391 rpt strip_tac >> metis_tac[D_CONJ_SET_LEMM] 392 ); 393 394val D_CONJ_SET_LEMM2_STRONG = store_thm 395 ("D_CONJ_SET_LEMM2_STRONG", 396 ``!A s. FINITE s 397 ==> !a e. (a,e) ��� d_conj_set s A 398 ==> (?f_a f_e. !q d. 399 ((q,d) ��� s ==> (f_a q d,f_e q d) ��� d ��� a ��� f_a q d ��� f_e q d ��� e) 400 ��� (A ��� BIGINTER {f_a q d | (q,d) ��� s } = a) 401 ��� (BIGUNION {f_e q d | (q,d) ��� s } = e))``, 402 gen_tac >> Induct_on `s` >> rpt strip_tac 403 >- (fs[NOT_IN_EMPTY,d_conj_set_def,ITSET_THM]) 404 >- (rename[`(a,e1) ��� d_conj_set (e INSERT s) A`] 405 >> fs[d_conj_set_def] 406 >> `s DELETE e = s` by (simp[SET_EQ_SUBSET,SUBSET_DEF]) 407 >> `(a,e1) ��� 408 (d_conj ��� SND) e (ITSET (d_conj ��� SND) (s DELETE e) {A,{}})` 409 by metis_tac[D_CONJ_SET_RECURSES] 410 >> fs[d_conj_def] >> rw[] 411 >> first_x_assum (qspec_then `a2` mp_tac) >> rpt strip_tac 412 >> first_x_assum (qspec_then `e2` mp_tac) 413 >> `(a2,e2) ��� ITSET (d_conj ��� SND) s {(A,���)}` by metis_tac[] 414 >> simp[] >> rpt strip_tac 415 >> qabbrev_tac `f_a2 = 416 ��q d. if (q,d) = e then a1 else f_a q d` 417 >> qabbrev_tac `f_e2 = 418 ��q d. if (q,d) = e then e1' else f_e q d` 419 >> qexists_tac `f_a2` >> qexists_tac `f_e2` >> fs[] >> rpt strip_tac 420 >> qunabbrev_tac `f_a2` >> qunabbrev_tac `f_e2` >> rw[] >> fs[] 421 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 422 >> first_x_assum (qspec_then `d` mp_tac) >> simp[] >> rpt strip_tac 423 >> fs[] >> rw[] 424 >- metis_tac[INTER_SUBSET,INTER_ASSOC,SUBSET_TRANS] 425 >- metis_tac[SUBSET_UNION,SUBSET_TRANS] 426 >- (`{if (q,d) = e 427 then a1 428 else f_a q d | (q,d) | ((q,d) = e) ��� ((q,d) ��� s)} = 429 {f_a q d | (q,d) ��� s} ��� {a1}` by ( 430 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 431 >- metis_tac[] 432 >- metis_tac[] 433 >- (qexists_tac `FST e` >> qexists_tac `SND e` >> fs[]) 434 ) 435 >> rw[] >> metis_tac[INTER_ASSOC,INTER_COMM] 436 ) 437 >- (`{if (q,d) = e 438 then e1' 439 else f_e q d | (q,d) | ((q,d) = e) ��� ((q,d) ��� s)} = 440 {f_e q d | (q,d) ��� s} ��� {e1'}` by ( 441 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 442 >- metis_tac[] 443 >- metis_tac[] 444 >- (qexists_tac `FST e` >> qexists_tac `SND e` >> fs[]) 445 ) 446 >> rw[] >> metis_tac[UNION_COMM] 447 ) 448 ) 449 ); 450 451val D_CONJ_SET_LEMM3 = store_thm 452 ("D_CONJ_SET_LEMM3", 453 ``!s A a a' e'. FINITE s 454 ��� (!q d. (q,d) ��� s ==> (a' q,e' q) ��� d ��� a ��� a' q) 455 ��� (a ��� A) 456 ==> (A ��� BIGINTER {a' q | q ��� IMAGE FST s }, 457 BIGUNION {e' q | q ��� IMAGE FST s}) 458 ��� d_conj_set s A``, 459 `!s. FINITE (s:�� # ((�� -> bool) # (�� -> bool) -> bool) -> bool) 460 ==> 461 (!A a a' e'. (!q d. (q,d) ��� s ==> (a' q,e' q) ��� d ��� a ��� a' q) 462 ��� (a ��� A) 463 ==> (A ��� BIGINTER {a' q | q ��� IMAGE FST s }, 464 BIGUNION {e' q | q ��� IMAGE FST s}) ��� d_conj_set s A)` 465 suffices_by metis_tac[] 466 >> Induct_on `s` >> rpt strip_tac >> fs[] 467 >- fs[d_conj_set_def,ITSET_THM] 468 >- (`(A ��� BIGINTER {a' q | ?x. (q = FST x) ��� x ��� s}, 469 BIGUNION {e' q | ?x. (q = FST x) ��� x ��� s}) ��� d_conj_set s A` 470 by metis_tac[] 471 >> simp[d_conj_set_def] 472 >> `s DELETE e = s` by fs[DELETE_NON_ELEMENT_RWT] 473 >> imp_res_tac D_CONJ_SET_RECURSES 474 >> first_x_assum (qspec_then `e` mp_tac) >> rpt strip_tac 475 >> first_x_assum (qspec_then `{(A,{})}` mp_tac) 476 >> rpt strip_tac >> fs[] >> fs[d_conj_set_def] 477 >> simp[d_conj_def] >> qexists_tac `a' (FST e)` 478 >> qexists_tac `A ��� BIGINTER {a' q | q ��� IMAGE FST s }` 479 >> qexists_tac `e' (FST e)` 480 >> qexists_tac `BIGUNION {e' q | q ��� IMAGE FST s }` 481 >> rpt strip_tac 482 >> simp[IN_IMAGE] >> dsimp[] >> simp[SET_EQ_SUBSET,SUBSET_DEF,IN_BIGINTER] 483 >> rpt strip_tac >> metis_tac[] 484 ) 485 ); 486 487val MEM_SUBSET_def = Define` 488 (MEM_SUBSET [] l = T) 489 ��� (MEM_SUBSET (h::ls) l = (MEM h l ��� MEM_SUBSET ls l))`; 490 491val MEM_SUBSET_SET_TO_LIST = store_thm 492 ("MEM_SUBSET_SET_TO_LIST", 493 ``!l1 l2. MEM_SUBSET l1 l2 = (set l1 ��� set l2)``, 494 Induct_on `l1` >> fs[MEM_SUBSET_def] >> rpt strip_tac 495 ); 496 497val MEM_SUBSET_REFL = store_thm 498 ("MEM_SUBSET_REFL", 499 ``!l. MEM_SUBSET l l``, 500 Induct_on `l` >> fs[MEM_SUBSET_def] >> rpt strip_tac 501 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF,MEM] 502 ); 503 504val MEM_SUBSET_APPEND = store_thm 505 ("MEM_SUBSET_APPEND", 506 ``!l1 l2. MEM_SUBSET l1 (l1++l2) 507 ��� MEM_SUBSET l2 (l1++l2)``, 508 rpt strip_tac 509 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF,MEM,MEM_APPEND] 510 ); 511 512val MEM_SUBSET_TRANS = store_thm 513 ("MEM_SUBSET_TRANS", 514 ``!l1 l2 l3. MEM_SUBSET l1 l2 ��� MEM_SUBSET l2 l3 ==> MEM_SUBSET l1 l3``, 515 metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_TRANS] 516 ); 517 518val MEM_EQUAL_def = Define` 519 (MEM_EQUAL l1 l2 = (MEM_SUBSET l1 l2 ��� MEM_SUBSET l2 l1))`; 520 521val MEM_EQUAL_SET = store_thm 522 ("MEM_EQUAL_SET", 523 ``!l1 l2. MEM_EQUAL l1 l2 = (set l1 = set l2)``, 524 metis_tac[MEM_SUBSET_SET_TO_LIST,SET_EQ_SUBSET,MEM_EQUAL_def] 525 ); 526 527val SET_OF_SUBLISTS_FINITE = store_thm 528 ("SET_OF_SUBLISTS_FINITE", 529 ``!l. FINITE {qs | MEM_SUBSET qs l ��� ALL_DISTINCT qs }``, 530 Induct_on `l` 531 >- (`{qs | MEM_SUBSET qs [] ��� ALL_DISTINCT qs} = {[]}` by ( 532 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 533 >> fs[MEM_EQUAL_def,MEM_SUBSET_def,MEM_SUBSET_SET_TO_LIST] 534 ) >> rw[] 535 ) 536 >- (rpt strip_tac >> fs[MEM_SUBSET_SET_TO_LIST] 537 >> `!k s. k ��� s ==> (k INSERT s = s)` by ( 538 rpt strip_tac >> simp[INSERT_DEF,SET_EQ_SUBSET,SUBSET_DEF] 539 ) 540 >> Cases_on `MEM h l` >> fs[] 541 >> qabbrev_tac `A = {qs | set qs ��� set l ��� ALL_DISTINCT qs}` 542 >> Q.HO_MATCH_ABBREV_TAC `FINITE B` 543 >> `B = A ��� {l1 ++ [h] ++ l2 | (l1++l2) ��� A }` by ( 544 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 545 >> qunabbrev_tac `A` >> qunabbrev_tac `B` >> fs[] 546 >- (Cases_on `set x ��� set l` >> fs[] 547 >> `!k a. MEM a k ��� ALL_DISTINCT k 548 ==> ?k1 k2. (k = k1 ++ [a] ++ k2) 549 ��� ~MEM a k1 ��� ~MEM a k2` by ( 550 Induct_on `k` >> fs[] >> rpt strip_tac 551 >- (rw[] >> qexists_tac `[]` >> fs[]) 552 >- (rw[] >> first_x_assum (qspec_then `a` mp_tac) 553 >> simp[] >> rpt strip_tac 554 >> qexists_tac `h'::k1` >> fs[] 555 ) 556 ) 557 >> `MEM h x` by ( 558 `?k. k ��� set x ��� ~(k ��� set l)` by metis_tac[SUBSET_DEF] 559 >> fs[SUBSET_DEF] >> metis_tac[] 560 ) 561 >> first_x_assum (qspec_then `x` mp_tac) >> rpt strip_tac 562 >> first_x_assum (qspec_then `h` mp_tac) >> simp[] 563 >> rpt strip_tac >> qexists_tac `k1` >> qexists_tac `k2` 564 >> fs[ALL_DISTINCT_APPEND] >> fs[SUBSET_DEF] >> metis_tac[] 565 ) 566 >- fs[SUBSET_DEF] 567 >- (fs[ALL_DISTINCT_APPEND] >> rpt strip_tac >> fs[SUBSET_DEF] 568 >> metis_tac[] 569 ) 570 ) 571 >> `!P. FINITE P ==> FINITE {l1 ��� [h] ��� l2 | l1 ��� l2 ��� P}` by ( 572 HO_MATCH_MP_TAC FINITE_INDUCT >> rpt strip_tac >> fs[] 573 >> `!k. FINITE {l1 ++ [h] ++ l2 | l1 ++ l2 = k }` by ( 574 Induct_on `k` >> fs[] 575 >- (`{l1 ++ [h] ++ l2 | (l1 = []) ��� (l2 = []) } = { [h] }` by ( 576 simp[SET_EQ_SUBSET,SUBSET_DEF] 577 ) 578 >> rw[] 579 ) 580 >- (rpt strip_tac 581 >> `{l1 ��� [h] ��� l2 | l1 ��� l2 = h'::k} = 582 (h::h'::k) INSERT 583 {h'::a | a ��� 584 {l1 ��� [h] ��� l2 | l1 ��� l2 = k}}` 585 by (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 586 >- (Cases_on `l1` >> fs[] >> disj2_tac 587 >> metis_tac[]) 588 >- (qexists_tac `[]` >> fs[]) 589 >- (rw[] >> qexists_tac `h'::l1` >> fs[]) 590 ) 591 >> `FINITE {h'::a | a ��� {l1 ��� [h] ��� l2 | l1 ��� l2 = k}}` 592 suffices_by metis_tac[FINITE_INSERT] 593 >> `{h'::a | a ��� {l1 ��� [h] ��� l2 | l1 ��� l2 = k}} 594 = IMAGE (��x. h'::x) {l1 ��� [h] ��� l2 | l1 ��� l2 = k}` 595 by fs[IMAGE_DEF] 596 >> metis_tac[IMAGE_FINITE] 597 ) 598 ) 599 >> `{l1 ��� [h] ��� l2 | (l1 ��� l2 = e) ��� l1 ��� l2 ��� P} 600 = {l1 ��� [h] ��� l2 | (l1 ��� l2 = e)} 601 ��� {l1 ��� [h] ��� l2 | l1 ��� l2 ��� P}` by ( 602 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 603 >> metis_tac[] 604 ) 605 >> metis_tac[FINITE_UNION] 606 ) 607 >> metis_tac[FINITE_UNION] 608 ) 609 ); 610 611val NUB_NUB = store_thm 612 ("NUB_NUB", 613 ``!l. nub (nub l) = nub l``, 614 Induct_on `l` >> fs[nub_def] >> rpt strip_tac 615 >> Cases_on `MEM h l` >> fs[nub_def] 616 ); 617 618val ALL_DISTINCT_SAME_NUB = store_thm 619 ("ALL_DISTINCT_SAME_NUB", 620 ``!l. ALL_DISTINCT l ==> (l = nub l)``, 621 Induct_on `l` >> fs[nub_def] 622 ); 623 624val ALL_DISTINCT_PAIRS_LEMM = store_thm 625 ("ALL_DISTINCT_PAIRS_LEMM", 626 ``(!x y1 y2 l. 627 (ALL_DISTINCT (MAP FST l) ��� (MEM (x,y1) l) ��� (MEM (x,y2) l) 628 ==> (y1 = y2))) 629 ��� (!x y1 y2 l. 630 (ALL_DISTINCT (MAP SND l) ��� (MEM (y1,x) l) ��� (MEM (y2,x) l) 631 ==> (y1 = y2)))``, 632 strip_tac >> Induct_on `l` >> fs[ALL_DISTINCT] >> rpt strip_tac 633 >- (Cases_on `h` >> fs[]) 634 >- (fs[MEM_MAP] >> Cases_on `h` >> fs[] >> rw[] 635 >> first_x_assum (qspec_then `(q,y2)` mp_tac) >> fs[]) 636 >- (fs[MEM_MAP] >> Cases_on `h` >> fs[] >> rw[] 637 >> first_x_assum (qspec_then `(q,y1)` mp_tac) >> fs[]) 638 >- metis_tac[] 639 >- (Cases_on `h` >> fs[]) 640 >- (fs[MEM_MAP] >> Cases_on `h` >> fs[] >> rw[] 641 >> first_x_assum (qspec_then `(y2,r)` mp_tac) >> fs[]) 642 >- (fs[MEM_MAP] >> Cases_on `h` >> fs[] >> rw[] 643 >> first_x_assum (qspec_then `(y1,r)` mp_tac) >> fs[]) 644 >- metis_tac[] 645 ); 646 647val FOLDR_INTER = store_thm 648 ("FOLDR_INTER", 649 ``!f A l. 650 (!x. MEM x l 651 ==> (FOLDR (��a sofar. f a ��� sofar) A l 652 ��� f x)) 653 ��� (FOLDR (��a sofar. f a ��� sofar) A l 654 ��� A)``, 655 Induct_on `l` >> rpt strip_tac >> fs[] 656 >> metis_tac[INTER_SUBSET,SUBSET_TRANS] 657 ); 658 659val FOLDR_APPEND_LEMM = store_thm 660 ("FOLDR_APPEND_LEMM", 661 ``!f A l. 662 (!x. MEM x l 663 ==> MEM_SUBSET (f x) (FOLDR (��a sofar. f a ++ sofar) A l)) 664 ��� (MEM_SUBSET A (FOLDR (��a sofar. f a ++ sofar) A l)) 665 ��� (set (FOLDR (��a sofar. f a ++ sofar) A l) = 666 set A ��� BIGUNION {set (f a) | MEM a l })``, 667 Induct_on `l` >> rpt strip_tac >> fs[] 668 >- fs[MEM_SUBSET_REFL] 669 >- fs[MEM_SUBSET_APPEND] 670 >- metis_tac[MEM_SUBSET_APPEND,MEM_SUBSET_TRANS] 671 >- metis_tac[MEM_SUBSET_APPEND,MEM_SUBSET_TRANS] 672 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 673 >> metis_tac[] 674 ) 675 ); 676 677val FOLDR_LEMM5 = store_thm 678 ("FOLDR_LEMM5", 679 ``!l1 l2 l3 l4 f1 f2 s. 680 (FOLDR (��a sofar. f1 a ��� sofar) 681 (FOLDR (��a sofar. f2 a ��� sofar) s (l1++l2)) (l3++l4)) 682 = ((FOLDR (��a sofar. f1 a ��� sofar) 683 (FOLDR (��a sofar. f2 a ��� sofar) s l1) l3) 684 ��� ((FOLDR (��a sofar. f1 a ��� sofar) 685 (FOLDR (��a sofar. f2 a ��� sofar) s l2) l4)))``, 686 Induct_on `l3` >> simp[SET_EQ_SUBSET,SUBSET_DEF] 687 >> rpt strip_tac >> fs[] 688 >> Induct_on `l4` 689 >> Induct_on `l1` >> fs[] >> Induct_on `l2` >> fs[] 690 ); 691 692val FOLDR_INTER_MEMEQUAL = store_thm 693 ("FOLDR_INTER_MEMEQUAL", 694 ``!l1 l2 s f. (set l1 = set l2) 695 ==> (FOLDR (��a sofar. f a ��� sofar) s l1 = 696 FOLDR (��a sofar. f a ��� sofar) s l2)``, 697 `!l1 l2 s f. (MEM_SUBSET l1 l2) 698 ==> (FOLDR (��a sofar. f a ��� sofar) s l2 699 ��� FOLDR (��a sofar. f a ��� sofar) s l1)` 700 suffices_by metis_tac[SET_EQ_SUBSET,SUBSET_DEF,MEM_SUBSET_SET_TO_LIST] 701 >> Induct_on `l1` 702 >- (rpt strip_tac >> fs[MEM_SUBSET_def,FOLDR_INTER]) 703 >- (rpt strip_tac >> simp[FOLDR] >> fs[MEM_SUBSET_def] 704 >> metis_tac[FOLDR_INTER] 705 ) 706 ); 707 708val ZIP_MAP = store_thm 709 ("ZIP_MAP", 710 ``!l. ZIP (MAP FST l, MAP SND l) = l``, 711 Induct_on `l` >> fs[ZIP] 712 ); 713 714val MAP_LEMM = store_thm 715 ("MAP_LEMM", 716 ``!l f h a. ~MEM h l 717 ==> (MAP (��q. if q = h then a else f q) l = MAP f l)``, 718 Induct_on `l` >> rpt strip_tac >> fs[] 719 ); 720 721val CAT_OPTIONS_def = Define` 722 (CAT_OPTIONS [] = []) 723 ��� (CAT_OPTIONS (SOME v::ls) = v::(CAT_OPTIONS ls)) 724 ��� (CAT_OPTIONS (NONE::ls) = CAT_OPTIONS ls)`; 725 726val CAT_OPTIONS_MEM = store_thm 727 ("CAT_OPTIONS_MEM", 728 ``!x l. (MEM x (CAT_OPTIONS l)) = (?y. (SOME x = y) ��� MEM y l)``, 729 Induct_on `l` >> rpt strip_tac >> fs[CAT_OPTIONS_def] 730 >> Cases_on `h` >> fs[CAT_OPTIONS_def] 731 ); 732 733val CAT_OPTIONS_MAP_LEMM = store_thm 734 ("CAT_OPTIONS_MAP_LEMM", 735 ``!i f ls. MEM i (CAT_OPTIONS (MAP f ls)) 736 = ?x. MEM x ls ��� (SOME i = f x)``, 737 Induct_on `ls` >> fs[CAT_OPTIONS_def,MAP] 738 >> rpt strip_tac >> Cases_on `f h` >> simp[EQ_IMP_THM] 739 >> rw[] >> fs[CAT_OPTIONS_def] >> metis_tac[SOME_11,NOT_SOME_NONE] 740 ); 741 742val CAT_OPTIONS_APPEND = store_thm 743 ("CAT_OPTIONS_APPEND", 744 ``!l1 l2. CAT_OPTIONS (l1 ++ l2) = CAT_OPTIONS l1 ++ CAT_OPTIONS l2``, 745 Induct_on `l1` >> fs[CAT_OPTIONS_def] >> rpt strip_tac 746 >> Cases_on `h` >> fs[CAT_OPTIONS_def] 747 ); 748 749val CAT_OPTIONS_LENGTH = store_thm 750 ("CAT_OPTIONS_LENGTH", 751 ``!l. (EVERY IS_SOME l = (LENGTH (CAT_OPTIONS l) = LENGTH l)) 752 ��� (LENGTH (CAT_OPTIONS l) <= LENGTH l)``, 753 Induct_on `l` >> fs[CAT_OPTIONS_def] >> rpt strip_tac 754 >> Cases_on `h` >> fs[IS_SOME_DEF,CAT_OPTIONS_def] 755 ); 756 757val CAT_OPTIONS_EL = store_thm 758 ("CAT_OPTIONS_EL", 759 ``!l. EVERY IS_SOME l 760 ==> !i. (i < LENGTH l) 761 ==> (SOME (EL i (CAT_OPTIONS l)) = EL i l)``, 762 Induct_on `l` >> fs[CAT_OPTIONS_def] >> rpt strip_tac 763 >> Cases_on `h` >> fs[IS_SOME_DEF,CAT_OPTIONS_def] 764 >> Cases_on `i` >> fs[EL] 765 ); 766 767val OPTION_TO_LIST_def = Define` 768 (OPTION_TO_LIST NONE = []) 769 ��� (OPTION_TO_LIST (SOME l) = l)`; 770 771val OPTION_TO_LIST_MEM = store_thm 772 ("OPTION_TO_LIST_MEM", 773 ``!x o_l. MEM x (OPTION_TO_LIST o_l) 774 = ?l. (o_l = SOME l) ��� (MEM x l)``, 775 rpt strip_tac >> Cases_on `o_l` >> fs[OPTION_TO_LIST_def] 776 ); 777 778val LIST_INTER_def = Define` 779 (LIST_INTER [] ls = []) 780 ��� (LIST_INTER (x::xs) ls = if MEM x ls 781 then x::(LIST_INTER xs ls) 782 else LIST_INTER xs ls)`; 783 784(* val GROUP_BY_def = tDefine "GROUP_BY" *) 785(* `(GROUP_BY P [] = []) *) 786(* ��� (GROUP_BY P (x::xs) = *) 787(* (FILTER (P x) (x::xs))::(GROUP_BY P (FILTER ($~ o (P x)) xs)) *) 788(* )` *) 789(* (WF_REL_TAC `measure (LENGTH o SND)` >> rpt strip_tac >> fs[] *) 790(* >> Q.HO_MATCH_ABBREV_TAC `A < SUC B` >> `A <= B ` suffices_by simp[] *) 791(* >> metis_tac[LENGTH_FILTER_LEQ] *) 792(* ); *) 793 794(* val GROUP_BY_SET_LEMM = store_thm *) 795(* ("GROUP_BY_SET_LEMM", *) 796(* ``!P l. (!x. P x x) ==> set l = (set (FLAT (GROUP_BY P l)))``, *) 797(* Induct_on `l` >> fs[GROUP_BY_def] >> rpt strip_tac *) 798(* >> Cases_on `P h h` >> fs[] *) 799(* >- () *) 800 801(* ) *) 802 803val SPAN_def = Define` 804 (SPAN R [] = ([],[])) 805 ��� (SPAN R (x::xs) = 806 if R x 807 then (let (ys,rs) = SPAN R xs 808 in (x::ys,rs)) 809 else ([],x::xs) 810 )`; 811 812val SPAN_APPEND = store_thm 813 ("SPAN_APPEND", 814 ``!R l l1 l2. (SPAN R l = (l1,l2)) ==> (l1 ++ l2 = l)``, 815 gen_tac >> Induct_on `l` >> fs[SPAN_def] >> rpt strip_tac 816 >> Cases_on `R h` >> fs[] 817 >> Cases_on `SPAN R l` >> rw[] >> fs[] 818 ); 819 820val SPAN_EQ = store_thm 821 ("SPAN_EQ", 822 ``!R x y t. equivalence R ��� R x y ==> (SPAN (R x) t = SPAN (R y) t)``, 823 gen_tac >> Induct_on `t` >> fs[SPAN_def] >> rpt strip_tac 824 >> `SPAN (R x) t = SPAN (R y) t` by metis_tac[] 825 >> `R x h = R y h` by ( 826 metis_tac[equivalence_def,relationTheory.transitive_def, 827 relationTheory.reflexive_def, 828 relationTheory.symmetric_def] 829 ) 830 >> Cases_on `R x h` >> fs[] 831 ); 832 833val SPAN_FST_LEMM = store_thm 834 ("SPAN_FST_LEMM", 835 ``!x R l. MEM x (FST (SPAN R l)) ==> R x``, 836 Induct_on `l` >> fs[SPAN_def] >> rpt strip_tac 837 >> Cases_on `R h` >> fs[] >> Cases_on `x = h` >> fs[] 838 >> Cases_on `SPAN R l` >> fs[] 839 ); 840 841val GROUP_BY_def = tDefine "GROUP_BY" 842 `(GROUP_BY P [] = []) 843 ��� (GROUP_BY P (x::xs) = 844 let (ys,rs) = SPAN (P x) (xs) 845 in (x::ys)::(GROUP_BY P rs) 846 )` 847 (WF_REL_TAC `measure (LENGTH o SND)` >> rpt strip_tac 848 >> `ys ++ rs = xs` by metis_tac[SPAN_APPEND] 849 >> `LENGTH ys + LENGTH rs = LENGTH xs` by metis_tac[LENGTH_APPEND] 850 >> fs[] 851 ); 852 853val GROUP_BY_FLAT = store_thm 854 ("GROUP_BY_FLAT", 855 ``!P l. (FLAT (GROUP_BY P l)) = l``, 856 gen_tac 857 >> `!l1 l2 l. (l1 ++ l2 = l) 858 ==> ((FLAT (GROUP_BY P l2)) = l2)` by ( 859 Induct_on `l` >> fs[GROUP_BY_def] >> rpt strip_tac 860 >> Cases_on `l1` 861 >- (fs[] >> simp[GROUP_BY_def] >> Cases_on `SPAN (P h) l` 862 >> `q ++ r = l` by metis_tac[SPAN_APPEND] 863 >> fs[] >> `(FLAT (GROUP_BY P r)) = r` by metis_tac[] 864 >> rw[LIST_TO_SET_APPEND] 865 ) 866 >- (Cases_on `l2` >> fs[GROUP_BY_def] >> rw[] 867 >> Cases_on `SPAN (P h'') t'` >> fs[] 868 >> `q++r = t'` by metis_tac[SPAN_APPEND] 869 >> first_x_assum (qspec_then `t ++ [h''] ++ q` mp_tac) >> simp[] 870 >> rpt strip_tac >> rw[LIST_TO_SET_APPEND] 871 ) 872 ) 873 >> strip_tac >> `[] ++ l = l` by simp[] >> metis_tac[] 874 ); 875 876val rel_corr_def = Define ` 877 rel_corr R P = 878 !x y. R x y = (P x y ��� P y x)`; 879 880val REL_CORR_GROUP_BY = store_thm 881 ("REL_CORR_GROUP_BY", 882 ``!R P. rel_corr R P 883 ��� equivalence R ��� transitive P 884 ==> !k_hd k_tl l. 885 (GROUP_BY R l = (k_hd::k_tl)) 886 ��� (SORTED P l) 887 ==> (!x y k. (MEM x k_hd) 888 ��� (MEM k k_tl) 889 ��� (MEM y k) 890 ==> ~R x y)``, 891 gen_tac >> gen_tac >> strip_tac >> Induct_on `l` >> fs[GROUP_BY_def,SPAN_def] 892 >> (rpt strip_tac >> rename[`SORTED P (H::l)`] 893 >> Cases_on `SPAN (R H) l` 894 >> Cases_on `l` 895 >- (fs[GROUP_BY_def,SPAN_def] >> rw[] >> fs[GROUP_BY_def]) 896 >- (fs[GROUP_BY_def,SPAN_def] >> rename[`SORTED P (H::h2::t1)`] 897 >> Cases_on `R H h2` >> fs[] 898 >- (first_x_assum (qspec_then `q` mp_tac) 899 >> rpt strip_tac 900 >> first_x_assum (qspec_then `GROUP_BY R r` mp_tac) 901 >> simp[GROUP_BY_def] >> fs[SORTED_DEF] 902 >> strip_tac 903 >> `SPAN (R h2) t1 = SPAN (R H) t1` 904 by metis_tac[SPAN_EQ] 905 >> rw[] >> Cases_on `SPAN (R H) t1` >> fs[] 906 >- (rw[] >> metis_tac[equivalence_def, 907 relationTheory.symmetric_def,relationTheory.transitive_def]) 908 >- (rw[] >> qexists_tac `x` >> simp[] >> fs[] >> rw[] 909 >> metis_tac[equivalence_def,relationTheory.symmetric_def, 910 relationTheory.transitive_def] 911 ) 912 ) 913 >- (rw[] >> Cases_on `GROUP_BY R (h2::t1)` >> fs[] 914 >> rw[] >> fs[SORTED_DEF] 915 >> rename[`GROUP_BY R (h3::t2) = h4::t3`] 916 >- (`R h3 y` by ( 917 fs[GROUP_BY_def,SPAN_def] 918 >> Cases_on `SPAN (R h3) t2` >> fs[] 919 >> `!x. MEM x (FST (q,r)) ==> (R h3 x)` 920 by metis_tac[SPAN_FST_LEMM] 921 >> Cases_on `y = h3` >> fs[] 922 >> `MEM y q` by (rw[] >> fs[]) 923 >> metis_tac[] 924 ) 925 >> metis_tac[equivalence_def,relationTheory.symmetric_def,relationTheory.transitive_def] 926 ) 927 >- (`P h3 H` by ( 928 Cases_on `y = h3` >> rw[] 929 >- metis_tac[equivalence_def, relationTheory.reflexive_def] 930 >- ( 931 `MEM y t2` by ( 932 `FLAT (GROUP_BY R (h3::t2)) = h3::t2` 933 by metis_tac[GROUP_BY_FLAT] 934 >> `MEM y (FLAT (GROUP_BY R (h3::t2)))` by ( 935 simp[MEM_FLAT] >> metis_tac[] 936 ) 937 >> `MEM y (h3::t2)` by metis_tac[] 938 >> fs[] >> metis_tac[] 939 ) 940 >> `P h3 y` by metis_tac[SORTED_EQ] 941 >> fs[rel_corr_def] 942 >> metis_tac[equivalence_def,relationTheory.symmetric_def,relationTheory.transitive_def] 943 ) 944 ) 945 >> metis_tac[rel_corr_def] 946 ) 947 ) 948 ) 949 ) 950 ); 951 952val _ = Cond_rewr.stack_limit := 1 953 954val SORTED_GROUP_BY = store_thm 955 ("SORTED_GROUP_BY", 956 ``!R P l. SORTED P l ��� transitive P ��� equivalence R 957 ��� rel_corr R P 958 ==> (!l_sub. MEM l_sub (GROUP_BY R l) 959 ==> ((!x y. MEM x l_sub ��� MEM y l_sub ==> R x y) 960 ��� (!x y. MEM x l_sub ��� MEM y l ��� R x y ==> MEM y l_sub)))``, 961 gen_tac >> gen_tac >> Induct_on `l` 962 >- (rpt strip_tac >> fs[GROUP_BY_def]) 963 >- ( 964 simp[] >> gen_tac >> strip_tac >> strip_tac >> strip_tac 965 >> Cases_on `l` >> fs[] 966 >- (rpt strip_tac >> fs[GROUP_BY_def,SPAN_def,equivalence_def] >> rw[] 967 >> fs[] >> rw[] >> metis_tac[relationTheory.reflexive_def] 968 ) 969 >- (fs[SORTED_DEF] >> Cases_on `GROUP_BY R (h'::t)` >> fs[] 970 >- (fs[GROUP_BY_def,SPAN_def] >> Cases_on `R h h'` >> fs[] 971 >> Cases_on `SPAN (R h) t` >> Cases_on `SPAN (R h') t` 972 >> fs[SPAN_EQ] 973 ) 974 >- (Cases_on `R h h'` 975 >- (Cases_on `GROUP_BY R (h::h'::t)` >> fs[] 976 >> `h''' = h::h''` by ( 977 fs[GROUP_BY_def,SPAN_def] >> Cases_on `R h h'` >> fs[] 978 >> `SPAN (R h) t = SPAN (R h') t` by metis_tac[SPAN_EQ] 979 >> rw[] >> Cases_on `SPAN (R h') t` >> fs[] >> rw[] 980 ) 981 >> `t' = t''` by ( 982 fs[GROUP_BY_def,SPAN_def] >> Cases_on `R h h'` >> fs[] 983 >> `SPAN (R h) t = SPAN (R h') t` by metis_tac[SPAN_EQ] 984 >> rw[] >> Cases_on `SPAN (R h') t` >> fs[] >> rw[] 985 ) 986 >> strip_tac 987 >- (rw[] >> fs[] 988 >> first_x_assum (qspec_then `h''` mp_tac) >> simp[] 989 >> rpt strip_tac >> fs[HD] >> rw[] >> rpt strip_tac 990 >- metis_tac[equivalence_def,relationTheory.reflexive_def] 991 >- (rw[] 992 >> `MEM h' h''` by ( 993 fs[GROUP_BY_def,SPAN_def] 994 >> rw[] >> Cases_on `R h h'` >> fs[] 995 >> Cases_on `SPAN (R h) t` >> Cases_on `SPAN (R h') t` 996 >> fs[SPAN_EQ] >> rw[] 997 ) 998 >> metis_tac[equivalence_def,relationTheory.transitive_def] 999 ) 1000 >- (rw[] 1001 >> `MEM h' h''` by ( 1002 fs[GROUP_BY_def,SPAN_def] 1003 >> rw[] >> Cases_on `R h h'` >> fs[] 1004 >> Cases_on `SPAN (R h) t` >> Cases_on `SPAN (R h') t` 1005 >> fs[SPAN_EQ] >> rw[] 1006 ) 1007 >> metis_tac[equivalence_def,relationTheory.transitive_def, 1008 relationTheory.symmetric_def] 1009 ) 1010 ) 1011 >- (first_x_assum (qspec_then `h''` mp_tac) >> simp[] 1012 >> rpt strip_tac >> rw[] 1013 >> fs[GROUP_BY_def,SPAN_def] >> Cases_on `R h h'` >> fs[] 1014 >> `SPAN (R h) t = SPAN (R h') t` by metis_tac[SPAN_EQ] 1015 >> rw[] >> Cases_on `SPAN (R h') t` >> fs[] >> rw[] 1016 >> Cases_on `y = h` >> Cases_on `y = h'` >> fs[] 1017 >> metis_tac[equivalence_def,relationTheory.transitive_def, 1018 relationTheory.reflexive_def, 1019 relationTheory.symmetric_def] 1020 ) 1021 >- (first_x_assum (qspec_then `l_sub` mp_tac) >> simp[]) 1022 >- (first_x_assum (qspec_then `l_sub` mp_tac) >> simp[] 1023 >> rpt strip_tac >> rw[] 1024 >- (fs[SORTED_EQ] 1025 >> `FLAT (h''::t') = h'::t` 1026 by metis_tac[GROUP_BY_FLAT] 1027 >> `MEM x (FLAT (h''::t'))` by (simp[MEM_FLAT] >> metis_tac[]) 1028 >> `MEM x (h'::t)` by metis_tac[] 1029 >> Cases_on `x = h'` 1030 >> rw[] 1031 >> `SORTED P (h::h'::t)` by ( 1032 simp[SORTED_EQ] >> rpt strip_tac >> fs[] 1033 >> metis_tac[relationTheory.transitive_def] 1034 ) 1035 >> `!k_hd k_tl l. 1036 (GROUP_BY R l = k_hd::k_tl) ��� SORTED P l 1037 ==> ���x y k. MEM x k_hd ��� MEM k k_tl ��� MEM y k ��� ��R x y` 1038 by (HO_MATCH_MP_TAC REL_CORR_GROUP_BY >> metis_tac[]) 1039 >> first_x_assum (qspec_then `h::h''` mp_tac) 1040 >> rpt strip_tac 1041 >> first_x_assum (qspec_then `t'` mp_tac) 1042 >> rpt strip_tac 1043 >> first_x_assum (qspec_then `h::h'::t` mp_tac) >> simp[] 1044 >> rpt strip_tac 1045 >> (fs[] 1046 >- metis_tac[] 1047 >- (fs[MEM_FLAT] >> `~R h x` by metis_tac[] 1048 >> metis_tac[equivalence_def,relationTheory.symmetric_def] 1049 )) 1050 ) 1051 >- metis_tac[] 1052 >- metis_tac[] 1053 ) 1054 ) 1055 >- (`(l_sub = [h]) \/ (l_sub = h'') \/ (MEM l_sub t')` by ( 1056 fs[GROUP_BY_def,SPAN_def] 1057 ) 1058 >- (rpt strip_tac >> rw[] 1059 >- (`(x = h) ��� (y = h)` by fs[] 1060 >> metis_tac[equivalence_def,relationTheory.reflexive_def] 1061 ) 1062 >- (`x = h` by fs[] >> metis_tac[]) 1063 >- (`x = h` by fs[] >> rw[] 1064 >> `SORTED P (h::h'::t)` by ( 1065 simp[SORTED_EQ] >> rpt strip_tac >> fs[SORTED_EQ] 1066 >> metis_tac[relationTheory.transitive_def] 1067 ) 1068 >> `FLAT (GROUP_BY R (h::h'::t)) = h::h'::t` 1069 by fs[GROUP_BY_FLAT] 1070 >> `!k_hd k_tl l. 1071 (GROUP_BY R l = k_hd::k_tl) ��� SORTED P l 1072 ==> ���x y k. MEM x k_hd ��� MEM k k_tl ��� MEM y k ��� ��R x y` 1073 by (HO_MATCH_MP_TAC REL_CORR_GROUP_BY >> metis_tac[]) 1074 >> Cases_on `GROUP_BY R (h::h'::t)` 1075 >- fs[FLAT] 1076 >- ( 1077 rename[`GROUP_BY R (h::h1::t) = h3::t2`] 1078 >> first_x_assum (qspec_then `h3` mp_tac) 1079 >> rpt strip_tac 1080 >> first_x_assum (qspec_then `t2` mp_tac) 1081 >> rpt strip_tac 1082 >> first_x_assum (qspec_then `h::h1::t` mp_tac) >> simp[] 1083 >> rpt strip_tac >> fs[GROUP_BY_def] 1084 >> Cases_on `SPAN (R h) (h1::t)` >> fs[] 1085 >> fs[SPAN_def] >> Cases_on `R h h1` >> fs[] 1086 >> rw[] >> Cases_on `SPAN (R h1) t` >> fs[] 1087 >> rw[] >> `MEM y (FLAT (GROUP_BY R (h1::t)))` by fs[] 1088 >> fs[MEM_FLAT] 1089 ) 1090 ) 1091 ) 1092 >- (rpt strip_tac >> rw[] 1093 >- (first_x_assum (qspec_then `h''` mp_tac) >> simp[] 1094 >> rpt strip_tac >> rw[] 1095 >> `FLAT (h''::t') = h'::t` by metis_tac[GROUP_BY_FLAT] 1096 >> `MEM h' h''` by (Cases_on `h''` >> fs[FLAT]) 1097 >> metis_tac[equivalence_def,relationTheory.symmetric_def, 1098 relationTheory.transitive_def] 1099 ) 1100 >- (first_x_assum (qspec_then `h''` mp_tac) >> simp[] 1101 >> rpt strip_tac >> rw[] 1102 >> `SORTED P (h::h'::t)` by ( 1103 simp[SORTED_EQ] >> rpt strip_tac >> fs[SORTED_EQ] 1104 >> metis_tac[relationTheory.transitive_def] 1105 ) 1106 >> `FLAT (GROUP_BY R (h::h'::t)) = h::h'::t` 1107 by fs[GROUP_BY_FLAT] 1108 >> `!k_hd k_tl l. 1109 (GROUP_BY R l = k_hd::k_tl) ��� SORTED P l 1110 ==> ���x y k. MEM x k_hd ��� MEM k k_tl ��� MEM y k ��� ��R x y` 1111 by (HO_MATCH_MP_TAC REL_CORR_GROUP_BY >> metis_tac[]) 1112 >> Cases_on `GROUP_BY R (h::h'::t)` 1113 >- fs[FLAT] 1114 >- (rename[`GROUP_BY R (h::h1::t) = h3::t2`] 1115 >> first_x_assum (qspec_then `h3` mp_tac) 1116 >> rpt strip_tac 1117 >> first_x_assum (qspec_then `t2` mp_tac) 1118 >> rpt strip_tac 1119 >> first_x_assum (qspec_then `h::h1::t` mp_tac) >> simp[] 1120 >> rpt strip_tac >> fs[GROUP_BY_def] 1121 >- (Cases_on `SPAN (R h) (h1::t)` >> fs[] 1122 >> fs[SPAN_def] >> Cases_on `R h h1` >> fs[] 1123 >> rw[] >> Cases_on `SPAN (R h1) t` >> fs[] 1124 >> rw[] >> `MEM y (FLAT (GROUP_BY R (h1::t)))` by fs[]) 1125 >- (Cases_on `SPAN (R h) (h1::t)` >> fs[] 1126 >> fs[SPAN_def] >> Cases_on `R h h1` >> fs[] 1127 >> rw[] >> Cases_on `SPAN (R h1) t` >> fs[] 1128 >> metis_tac[equivalence_def,relationTheory.symmetric_def] 1129 ) 1130 ) 1131 ) 1132 >- metis_tac[] 1133 ) 1134 >- (rpt strip_tac >> rw[] 1135 >- metis_tac[] 1136 >- (first_x_assum (qspec_then `l_sub` mp_tac) >> simp[] 1137 >> rpt strip_tac >> `SORTED P (h::h'::t)` by ( 1138 simp[SORTED_EQ] >> rpt strip_tac >> fs[SORTED_EQ] 1139 >> metis_tac[relationTheory.transitive_def] 1140 ) 1141 >> `FLAT (GROUP_BY R (h::h'::t)) = h::h'::t` 1142 by fs[GROUP_BY_FLAT] 1143 >> `!k_hd k_tl l. 1144 (GROUP_BY R l = k_hd::k_tl) ��� SORTED P l 1145 ==> ���x y k. MEM x k_hd ��� MEM k k_tl ��� MEM y k ��� ��R x y` 1146 by (HO_MATCH_MP_TAC REL_CORR_GROUP_BY >> metis_tac[]) 1147 >> Cases_on `GROUP_BY R (h::h'::t)` 1148 >- fs[FLAT] 1149 >- (rename[`GROUP_BY R (h::h1::t) = h3::t2`] 1150 >> first_x_assum (qspec_then `h3` mp_tac) 1151 >> rpt strip_tac 1152 >> first_x_assum (qspec_then `t2` mp_tac) 1153 >> rpt strip_tac 1154 >> first_x_assum (qspec_then `h::h1::t` mp_tac) >> simp[] 1155 >> rpt strip_tac >> fs[GROUP_BY_def] 1156 >- (Cases_on `SPAN (R h) (h1::t)` >> fs[] 1157 >> fs[SPAN_def] >> Cases_on `R h h1` >> fs[] 1158 >> rw[] >> Cases_on `SPAN (R h1) t` >> fs[] 1159 >> rw[] >> `MEM y (FLAT (GROUP_BY R (h1::t)))` by fs[]) 1160 >- (Cases_on `SPAN (R h) (h1::t)` >> fs[] 1161 >> fs[SPAN_def] >> Cases_on `R h h1` >> fs[] 1162 >> rw[] >> Cases_on `SPAN (R h1) t` >> fs[] 1163 >> metis_tac[equivalence_def,relationTheory.symmetric_def] 1164 ) 1165 ) 1166 ) 1167 >- metis_tac[] 1168 >- metis_tac[] 1169 ) 1170 ) 1171 ) 1172 ) 1173 ) 1174 ); 1175 1176val ONLY_MINIMAL_def = Define` 1177 ONLY_MINIMAL P l = 1178 FILTER (��a. ~EXISTS (��x. P x a ��� ~(x = a)) l) l`; 1179 1180 1181 (* (ONLY_MINIMAL P [] = []) *) 1182 (* ��� (ONLY_MINIMAL P (x::xs) = *) 1183 (* (* if EXISTS (��x1. P x1 x) xs *) *) 1184 (* (* then ONLY_MINIMAL P xs *) *) 1185 (* x::(FILTER (��a. ~P a x) (ONLY_MINIMAL P xs)) *) 1186 (* )`; *) 1187 1188val ONLY_MINIMAL_SUBSET = store_thm 1189 ("ONLY_MINIMAL_SUBSET", 1190 ``!P l. MEM_SUBSET (ONLY_MINIMAL P l) l``, 1191 gen_tac >> Induct_on `l` >> fs[ONLY_MINIMAL_def,MEM_SUBSET_def] 1192 >> rpt strip_tac >> fs[MEM_SUBSET_SET_TO_LIST] 1193 >> Cases_on `EVERY ($~ ��� (��x. P x h ��� x ��� h)) l` 1194 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[MEM_FILTER,EVERY_MEM] 1195 ); 1196 1197val ONLY_MINIMAL_MEM = store_thm 1198 ("ONLY_MINIMAL_MEM", 1199 ``!P l x. 1200 (MEM x (ONLY_MINIMAL P l) = 1201 (MEM x l ��� (!y. MEM y l ��� ~(x = y) ==> ~P y x)))``, 1202 simp[EQ_IMP_THM] >> rpt strip_tac 1203 >- metis_tac[MEM_SUBSET_SET_TO_LIST,ONLY_MINIMAL_SUBSET,MEM,SUBSET_DEF] 1204 >- (fs[ONLY_MINIMAL_def,MEM_FILTER,EVERY_MEM] >> metis_tac[]) 1205 >- (simp[ONLY_MINIMAL_def,MEM_FILTER,EVERY_MEM] >> rpt strip_tac 1206 >> metis_tac[] 1207 ) 1208 ); 1209 1210val INDEX_FIND_LEMM = store_thm 1211 ("INDEX_FIND_LEMM", 1212 ``!P i ls. OPTION_MAP SND (INDEX_FIND i P ls) 1213 = OPTION_MAP SND (INDEX_FIND (SUC i) P ls)``, 1214 gen_tac >> Induct_on `ls` >> fs[OPTION_MAP_DEF,INDEX_FIND_def] 1215 >> Cases_on `P h` 1216 >- fs[OPTION_MAP_DEF,INDEX_FIND_def] 1217 >- metis_tac[] 1218 ); 1219 1220val FIND_LEMM = store_thm 1221 ("FIND_LEMM", 1222 ``!P x l. MEM x l ��� P x 1223 ==> ?y. (FIND P l = SOME y) ��� (P y)``, 1224 gen_tac >> Induct_on `l` >> rpt strip_tac >> fs[] 1225 >- (rw[] >> simp[FIND_def,INDEX_FIND_def]) 1226 >- (rw[] 1227 >> `?y. (OPTION_MAP SND (INDEX_FIND 0 P (h::l)) = SOME y) 1228 ��� (P y)` suffices_by fs[FIND_def] 1229 >> first_x_assum (qspec_then `x` mp_tac) 1230 >> rpt strip_tac 1231 >> `?y. (OPTION_MAP SND (INDEX_FIND 0 P l) = SOME y) 1232 ��� (P y)` by fs[FIND_def] 1233 >> Cases_on `P h` 1234 >- fs[INDEX_FIND_def] 1235 >- (`���y. (OPTION_MAP SND (INDEX_FIND 1 P l) = SOME y) ��� P y` 1236 suffices_by fs[INDEX_FIND_def] 1237 >> qexists_tac `y` >> rpt strip_tac 1238 >> metis_tac[INDEX_FIND_LEMM,DECIDE ``SUC 0 = 1``]) 1239 ) 1240 ); 1241 1242val FIND_LEMM2 = store_thm 1243 ("FIND_LEMM2", 1244 ``!P x l. (FIND P l = SOME x) ==> (MEM x l ��� P x)``, 1245 gen_tac >> Induct_on `l` >> fs[FIND_def,INDEX_FIND_def] 1246 >> rpt strip_tac >> Cases_on `P h` >> fs[] >> Cases_on `z` 1247 >> fs[] 1248 >> `OPTION_MAP SND (INDEX_FIND 0 P l) = 1249 OPTION_MAP SND (INDEX_FIND 1 P l)` 1250 by metis_tac[INDEX_FIND_LEMM,DECIDE ``SUC 0 = 1``] 1251 >> rw[] 1252 >> `OPTION_MAP SND (INDEX_FIND 0 P l) = SOME r` by ( 1253 `OPTION_MAP SND (INDEX_FIND 1 P l) = SOME r` by fs[] 1254 >> metis_tac[] 1255 ) 1256 >> fs[] 1257 ); 1258 1259val FIND_UNIQUE = store_thm 1260 ("FIND_UNIQUE", 1261 ``!P x l. P x ��� (!y. MEM y l ��� P y ==> (y = x)) ��� MEM x l 1262 ==> (FIND P l = SOME x)``, 1263 gen_tac >> Induct_on `l` >> rpt strip_tac 1264 >- fs[] 1265 >- (Cases_on `P h` 1266 >- (`x = h` by fs[] >> rw[] 1267 >> fs[FIND_def,INDEX_FIND_def] 1268 ) 1269 >- (fs[FIND_def] >> rw[] >> fs[] 1270 >> fs[INDEX_FIND_def] 1271 >> `���z. (INDEX_FIND 0 P l = SOME z) ��� (x = SND z)` 1272 by metis_tac[] 1273 >> Cases_on `z` 1274 >> `OPTION_MAP SND (INDEX_FIND 0 P l) 1275 = OPTION_MAP SND (INDEX_FIND (SUC 0) P l)` 1276 by metis_tac[INDEX_FIND_LEMM] 1277 >> `OPTION_MAP SND (INDEX_FIND 0 P l) = SOME r` 1278 by fs[OPTION_MAP_DEF] >> fs[] 1279 >> `OPTION_MAP SND (INDEX_FIND 1 P l) = SOME r` 1280 by fs[OPTION_MAP_DEF] >> fs[] 1281 >> metis_tac[] 1282 ) 1283 ) 1284 ); 1285 1286 1287val PSUBSET_WF = store_thm 1288 ("PSUBSET_WF", 1289 ``!d. FINITE d ==> WF (\s t. s ��� t ��� s ��� d ��� t ��� d)``, 1290 rpt strip_tac 1291 >> qabbrev_tac `r_reln = rel_to_reln (\s t. s ��� t ��� s ��� d ��� t ��� d)` 1292 >> `transitive r_reln` by ( 1293 simp[transitive_def] >> rpt strip_tac >> qunabbrev_tac `r_reln` 1294 >> fs[rel_to_reln_def] >> metis_tac[PSUBSET_TRANS] 1295 ) 1296 >> `acyclic r_reln` by ( 1297 fs[acyclic_def] >> rpt strip_tac 1298 >> `(x,x) ��� r_reln` by metis_tac[transitive_tc] 1299 >> qunabbrev_tac `r_reln` >> fs[rel_to_reln_def] 1300 ) 1301 >> `domain r_reln ��� (POW d)` by ( 1302 qunabbrev_tac `r_reln` >> fs[domain_def,rel_to_reln_def] 1303 >> simp[SUBSET_DEF] >> rpt strip_tac 1304 >> metis_tac[SUBSET_DEF,IN_POW] 1305 ) 1306 >> `range r_reln ��� (POW d)` by ( 1307 qunabbrev_tac `r_reln` >> fs[range_def,rel_to_reln_def] 1308 >> simp[SUBSET_DEF] >> rpt strip_tac 1309 >> metis_tac[SUBSET_DEF,IN_POW] 1310 ) 1311 >> `(��s t. s ��� t ��� s ��� d ��� t ��� d) = reln_to_rel r_reln` by ( 1312 qunabbrev_tac `r_reln` >> fs[rel_to_reln_inv]) 1313 >> `FINITE (POW d)` by metis_tac[FINITE_POW] 1314 >> `WF (reln_to_rel r_reln)` suffices_by fs[] 1315 >> metis_tac[acyclic_WF] 1316 ); 1317 1318val BOUNDED_INCR_WF_LEMM = store_thm 1319 ("BOUNDED_INCR_WF_LEMM", 1320 ``!b m n. WF (��(i,j) (i1,j1). 1321 (b (i,j) = b (i1,j1)) 1322 ��� (i1 < i) ��� (i <= b (i,j)))``, 1323 rpt strip_tac >> rw[WF_IFF_WELLFOUNDED] >> simp[wellfounded_def] 1324 >> rpt strip_tac >> CCONTR_TAC >> fs[] 1325 >> `!n. b (FST (f n), SND (f n)) = b (FST (f 0), SND (f 0))` by ( 1326 Induct_on `n` >> first_x_assum (qspec_then `n` mp_tac) >> rpt strip_tac 1327 >> fs[] >> Cases_on `f n` >> Cases_on `f (SUC n)` 1328 >> fs[] 1329 ) 1330 >> qabbrev_tac `B = b (FST (f 0),SND (f 0))` 1331 >> `!n. (��(i,j) (i1,j1). i1 < i ��� i <= B) (f (SUC n)) (f n)` by ( 1332 rpt strip_tac >> rpt (first_x_assum (qspec_then `n` mp_tac)) 1333 >> rpt strip_tac >> Cases_on `f n` >> Cases_on `f (SUC n)` 1334 >> fs[] 1335 ) 1336 >> `!k. ?n. (FST (f n) > k)` by ( 1337 Induct_on `k` 1338 >- (Cases_on `FST (f 0)` >> fs[] 1339 >- (first_x_assum (qspec_then `0` mp_tac) >> rpt strip_tac 1340 >> qexists_tac `SUC 0` >> Cases_on `f (SUC 0)` >> Cases_on `f 0` 1341 >> fs[] 1342 ) 1343 >- (qexists_tac `0` >> fs[]) 1344 ) 1345 >- (fs[] >> Cases_on `FST (f n) = SUC k` 1346 >- (first_x_assum (qspec_then `n` mp_tac) >> rpt strip_tac 1347 >> Cases_on `f (SUC n)` >> Cases_on `f n` >> fs[] 1348 >> qexists_tac `SUC n` >> fs[] 1349 ) 1350 >- (qexists_tac `n` >> fs[]) 1351 ) 1352 ) 1353 >> first_x_assum (qspec_then `B` mp_tac) >> rpt strip_tac 1354 >> first_x_assum (qspec_then `n` mp_tac) >> rpt strip_tac 1355 >> Cases_on `f (SUC n)` >> Cases_on `f n` >> fs[] 1356 ); 1357 1358val WF_LEMM = store_thm 1359 ("WF_LEMM", 1360 ``!P A b. (!k. A k ==> WF (P k)) 1361 ==> ((!k. A (b k)) ==> WF (��a a2. (b a = b a2) ��� P (b a) a a2))``, 1362 rpt strip_tac >> rw[WF_IFF_WELLFOUNDED] >> simp[wellfounded_def] 1363 >> rpt strip_tac >> CCONTR_TAC >> fs[] 1364 >> `���n. b (f (SUC n)) = b (f n)` by metis_tac[] 1365 >> `!n. b (f (SUC n)) = b (f 0)` by (Induct_on `n` >> fs[]) 1366 >> `!n. P (b (f (SUC n))) (f (SUC n)) (f n)` by metis_tac[] 1367 >> `!n. P (b (f 0)) (f (SUC n)) (f n)` by metis_tac[] 1368 >> `!n. P (b (f 0)) (f (SUC n)) (f n)` by metis_tac[] 1369 >> `~wellfounded (P (b (f 0)))` by metis_tac[wellfounded_def] 1370 >> metis_tac[WF_IFF_WELLFOUNDED] 1371 ); 1372 1373val NoNodeProcessedTwice_def = Define` 1374 NoNodeProcessedTwice g m (a,ns) (a2,ns2) = 1375 ((g DIFF (m a) ��� g DIFF (m a2)) 1376 \/ ((g DIFF (m a) = g DIFF (m a2)) 1377 ��� (LENGTH ns) < (LENGTH ns2)))`; 1378 1379val NNPT_WF = store_thm 1380 ("NNPT_WF", 1381 ``!g m. FINITE g ==> WF (NoNodeProcessedTwice g m)``, 1382 rpt strip_tac 1383 >> `WF (��s t. s ��� t 1384 ��� s ��� g ��� t ��� g)` by metis_tac[PSUBSET_WF] 1385 >> `WF ($<)` by metis_tac[WF_LESS] 1386 >> `WF (�� (x:�� list) y. 1387 LENGTH x < LENGTH y)` by ( 1388 `inv_image ($<) (LENGTH:(�� list -> num)) 1389 = (��x y. 1390 LENGTH x < LENGTH y)` by simp[inv_image_def] 1391 >> `WF (inv_image ($<) (LENGTH:(�� list -> num)))` suffices_by fs[] 1392 >> metis_tac[WF_inv_image] 1393 ) 1394 >> qabbrev_tac `P = (��s t. s ��� t ��� s ��� g ��� t ��� g)` 1395 >> qabbrev_tac `Q = (��(x:�� list) (y:�� list). LENGTH x < LENGTH y)` 1396 >> qabbrev_tac `f = �� a. g DIFF (m a)` 1397 >> `inv_image P f = �� a a2. 1398 (g DIFF (m a) 1399 ��� g DIFF (m a2))` by ( 1400 qunabbrev_tac `P` 1401 >> fs[inv_image_def] 1402 >> `(\x y. f x ��� f y) = (��a a2. f a ��� f a2)` 1403 suffices_by ( 1404 fs[] >> qunabbrev_tac `f` >> simp[inv_image_def] 1405 ) 1406 >> metis_tac[] 1407 ) 1408 >> `WF (inv_image P f)` by metis_tac[WF_inv_image] 1409 >> `WF (P LEX Q)` by metis_tac[WF_LEX] 1410 >> qabbrev_tac 1411 `j = ��(a,l:(�� list)). (g DIFF (m a),l)` 1412 >> `WF (inv_image (P LEX Q) j)` by metis_tac[WF_inv_image] 1413 >> `!x y. (NoNodeProcessedTwice g m) x y ==> (inv_image (P LEX Q) j) x y` by ( 1414 fs[inv_image_def,LEX_DEF] >> rpt strip_tac 1415 >> Cases_on `x` >> Cases_on `y` >> fs[NoNodeProcessedTwice_def] 1416 >> qunabbrev_tac `f` >> qunabbrev_tac `P` >> qunabbrev_tac `Q` 1417 >> simp[] >> simp[EQ_IMP_THM] >> rpt strip_tac 1418 >> (qunabbrev_tac `j` >> simp[]) 1419 ) 1420 >> metis_tac[WF_SUBSET] 1421 ); 1422 1423val P_DIVIDED_WF_LEMM = store_thm 1424 ("P_DIVIDED_WF_LEMM", 1425 ``!P R1 R2. 1426 WF (��x y. ~P x ��� ~P y ��� R1 x y) ��� WF R2 1427 ��� (!x y. P y ��� R2 x y ==> P x) 1428 ==> WF (��x y. ((~P y ��� ~P x) ==> R1 x y) ��� (P y ==> R2 x y))``, 1429 rpt strip_tac >> rw[WF_IFF_WELLFOUNDED] >> simp[wellfounded_def] 1430 >> rpt strip_tac 1431 >> `!k. P (f k) 1432 ==> ?j. k <= j ��� (P (f j) ��� ~R2 (f (SUC j)) (f j))` by ( 1433 rpt strip_tac 1434 >> `�����f. ���n. R2 (f (SUC n)) (f n)` 1435 by metis_tac[WF_IFF_WELLFOUNDED,wellfounded_def] >> fs[] 1436 >> qabbrev_tac `f_k = ��n. f (n + k)` 1437 >> qabbrev_tac `N = $LEAST (��k. ~R2 (f_k (SUC k)) (f_k k))` 1438 >> `(��k. ~R2 (f_k (SUC k)) (f_k k)) N 1439 ��� !n. n < N ==> ~(��k. ~R2 (f_k (SUC k)) (f_k k)) n` by ( 1440 qunabbrev_tac `N` 1441 >> Q.HO_MATCH_ABBREV_TAC ` 1442 Q ($LEAST Q) 1443 ��� !n. n < ($LEAST Q) ==> ~Q n` 1444 >> HO_MATCH_MP_TAC LEAST_EXISTS_IMP >> fs[] 1445 >> qunabbrev_tac `Q` >> fs[] 1446 ) 1447 >> `!a. a <= N ==> P (f_k a)` by ( 1448 Induct_on `a` >> fs[] 1449 >- (qunabbrev_tac `f_k` >> fs[]) 1450 >- (strip_tac >> `a < N` by fs[] 1451 >> metis_tac[DECIDE ``a < N ==> a <= N``] 1452 ) 1453 ) 1454 >> qexists_tac `N+k` >> qunabbrev_tac `f_k` >> fs[] 1455 >> metis_tac[DECIDE ``SUC (N + k) = k + SUC N``] 1456 ) 1457 >> Cases_on `?a. P (f a)` >> fs[] 1458 >- metis_tac[] 1459 >- (`?k. P (f k) \/ (~P (f k) ��� ~R1 (f (SUC k)) (f k))` by ( 1460 `?n. P (f (SUC n)) ��� P (f n) ��� (��R1 (f (SUC n)) (f n) ��� ~P (f n))` 1461 by (fs[WF_IFF_WELLFOUNDED, wellfounded_def] 1462 >> metis_tac[]) 1463 >> metis_tac[] 1464 ) 1465 >> metis_tac[] 1466 ) 1467 ); 1468 1469val MOD_LEMM = store_thm 1470 ("MOD_LEMM", 1471 ``!x n. (0 < n) ==> ((x - (x MOD n)) MOD n = 0)``, 1472 rpt strip_tac 1473 >> `((x - (x MOD n) + (x MOD n)) MOD n = ((0 + (x MOD n)) MOD n))` by ( 1474 `(x MOD n) <= x` by simp[MOD_LESS_EQ] 1475 >> `x - (x MOD n) + (x MOD n) = x` by simp[] 1476 >> fs[] 1477 ) 1478 >> metis_tac[ADD_MOD,MOD_EQ_0,DECIDE ``0 * n = 0``] 1479 ); 1480 1481val MOD_GEQ_2_INCREASES = store_thm 1482 ("MOD_GEQ_2_INCREASES", 1483 ``!N x. 2 <= N ==> ~((x + 1) MOD N = x MOD N)``, 1484 rpt strip_tac >> simp[] >> `0 < N` by simp[] 1485 >> `(x + 1 + (N - (x MOD N))) MOD N = (x + (N - (x MOD N))) MOD N` 1486 by metis_tac[ADD_MOD] 1487 >> `x MOD N < N` by metis_tac[MOD_LESS] >> fs[] 1488 >> `0 < N` by simp[] >> `x MOD N <= x` by metis_tac[MOD_LESS_EQ] 1489 >> `(N + ((x + 1) ��� (x MOD N))) MOD N = (N + (x ��� (x MOD N))) MOD N` by fs[] 1490 >> `(x + 1 - (x MOD N)) MOD N = (x - (x MOD N)) MOD N` 1491 by metis_tac[ADD_MODULUS] 1492 >> `(x - (x MOD N)) MOD N = 0` by metis_tac[MOD_LEMM] 1493 >> rw[] >> `((x - (x MOD N)) +1) MOD N = 1` suffices_by fs[] 1494 >> `(x - (x MOD N)) MOD N = 0 MOD N` by simp[] 1495 >> `1 MOD N = 1` by simp[] >> metis_tac[ADD_MOD,DECIDE ``0 + 1 = 1``] 1496 ); 1497 1498val INCREASING_MOD_CYCLES = store_thm 1499 ("INCREASING_MOD_CYCLES", 1500 ``!f N. (!j. (f (SUC j) = f j) \/ ((f (SUC j)) = ((f j + 1) MOD N))) 1501 ��� (!i. ?k. (i <= k) ��� ~(f (SUC k) = f k)) 1502 ��� (f 0 = 0) ��� (0 < N) 1503 ==> (!n. (n < N) ==> !i. ?k. (i <= k) ��� (f k = n))``, 1504 strip_tac >> strip_tac >> strip_tac 1505 >> `!a. f a < N` by ( 1506 Induct_on `a` >> fs[] 1507 >> `(f (SUC a) = f a) ��� (f (SUC a) = (f a + 1) MOD N)` by simp[] >> fs[] 1508 ) 1509 >> rpt strip_tac >> CCONTR_TAC 1510 >> qabbrev_tac `U = { u | u < N ��� !k. i <= k ==> ~(f k = u)}` 1511 >> `U ��� (count N)` by ( 1512 qunabbrev_tac `U` >> simp[count_def,SUBSET_DEF] 1513 >> rpt strip_tac >> fs[] 1514 ) 1515 >> `CARD U <= N` by metis_tac[CARD_COUNT,CARD_SUBSET,FINITE_COUNT] 1516 >> Cases_on `CARD U < N` 1517 >- (`0 < CARD U` by ( 1518 `~(U = {})` suffices_by metis_tac[CARD_EQ_0,FINITE_COUNT,PSUBSET_DEF, 1519 PSUBSET_FINITE, 1520 DECIDE ``0 < CARD U = ~(CARD U = 0)`` 1521 ] 1522 >> `?u. u ��� U` suffices_by metis_tac[MEMBER_NOT_EMPTY] 1523 >> qexists_tac `n` >> qunabbrev_tac `U` >> fs[] >> rpt strip_tac 1524 >> metis_tac[] 1525 ) 1526 >> `!a. ~((f i + a) MOD N ��� U)` by ( 1527 Induct_on `a` >> fs[] >> rpt strip_tac 1528 >- (qunabbrev_tac `U` >> fs[] >> metis_tac[DECIDE ``i <= i``]) 1529 >- (qunabbrev_tac `U` >> fs[] 1530 >> qabbrev_tac `P = \p. k <= p ��� ~(f (SUC p) = f p)` 1531 >> qabbrev_tac `p0 = $LEAST P` 1532 >> `P p0 ��� !n. n < p0 ==> ~P n` by ( 1533 `?p. P p` suffices_by metis_tac[LEAST_EXISTS] 1534 >> qunabbrev_tac `P` >> fs[] 1535 ) 1536 >> qunabbrev_tac `P` >> fs[] 1537 >> `!l. k <= l ��� l <= p0 ==> (f k = f l)` by ( 1538 Induct_on `l` >> fs[] >> rpt strip_tac 1539 >- metis_tac[] 1540 >- (first_x_assum (qspec_then `l` mp_tac) >> simp[] 1541 >> Cases_on `k = SUC l` >> fs[] >> rw[] 1542 ) 1543 ) 1544 >> `f p0 = f k` by fs[] >> rw[] 1545 >> `(f (SUC p0) = (f p0 + 1) MOD N)` by metis_tac[] 1546 >> `i <= SUC p0` by simp[] 1547 >> `(f p0 + 1) MOD N = (f i + SUC a) MOD N` suffices_by metis_tac[] 1548 >> rw[] >> metis_tac[DECIDE ``a + (f i + 1) = f i + SUC a``] 1549 ) 1550 ) 1551 >> `?k. (f i + k) MOD N = n` by ( 1552 `{a | ?k. a = (f i + k) MOD N } = count N` by ( 1553 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1554 >- metis_tac[MOD_LESS] 1555 >- (qexists_tac `N -(f i MOD N) + (x MOD N)` >> simp[] 1556 >> `f i < N` by metis_tac[] >> simp[] 1557 ) 1558 ) 1559 >> `n ��� count N` by simp[count_def] 1560 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 1561 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1562 >> metis_tac[] 1563 ) 1564 >> `n ��� U` suffices_by metis_tac[] 1565 >> qunabbrev_tac `U` >> fs[] >> metis_tac[] 1566 ) 1567 >- (`CARD U = N` by fs[] 1568 >> `U = count N` 1569 by metis_tac[FINITE_COUNT,PSUBSET_FINITE, 1570 PSUBSET_DEF,SUBSET_EQ_CARD,CARD_COUNT] 1571 >> `f i ��� U` 1572 by (`f i ��� count N` suffices_by metis_tac[] >> fs[count_def]) 1573 >> qunabbrev_tac `U` >> fs[] >> metis_tac[DECIDE ``i <= i``] 1574 ) 1575 ); 1576 1577 1578 1579val _ = export_theory(); 1580