1open HolKernel Parse bossLib boolLib gfgTheory listTheory optionTheory pred_setTheory rich_listTheory sortingTheory relationTheory 2 3open alterATheory sptreeTheory ltlTheory generalHelpersTheory 4 5val _ = new_theory "concrRep"; 6 7val _ = monadsyntax.temp_add_monadsyntax(); 8val _ = overload_on("monad_bind",``OPTION_BIND``); 9 10val _ = Datatype` 11 edgeLabelAA = <| edge_grp : num ; 12 pos_lab : (�� list) ; 13 neg_lab : (�� list) 14 |>`; 15 16val _ = Datatype` 17 nodeLabelAA = <| frml : �� ltl_frml ; 18 is_final : bool ; 19 true_labels : (�� edgeLabelAA) list 20 |>`; 21 22val _ = Datatype` 23 concrAA = <| graph : (�� nodeLabelAA, �� edgeLabelAA) gfg ; 24 init : (num list) list ; 25 atomicProp : �� list 26 |>`; 27 28val concr2Abstr_states_def = Define` 29 concr2Abstr_states graph = 30 { x.frml | SOME x ��� 31 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo))}`; 32 33val concr2Abstr_init_def = Define` 34 concr2Abstr_init concrInit graph = 35 LIST_TO_SET 36 (MAP 37 (\l. {x.frml | 38 MEM x (CAT_OPTIONS (MAP (\n. lookup n graph.nodeInfo) l)) }) 39 concrInit)`; 40 41val concr2Abstr_final_def = Define` 42 concr2Abstr_final graph = 43 {x.frml | SOME x ��� 44 (IMAGE (\n. lookup n graph.nodeInfo) (domain graph.nodeInfo)) 45 ��� x.is_final}`; 46 47val _ = Datatype` 48 concrEdge = <| pos : (�� list) ; 49 neg : (�� list) ; 50 sucs : (�� ltl_frml) list |>`; 51 52val cE_equiv_def = Define ` 53 cE_equiv cE1 cE2 = 54 ((MEM_EQUAL cE1.pos cE2.pos) 55 ��� (MEM_EQUAL cE1.neg cE2.neg) 56 ��� (MEM_EQUAL cE1.sucs cE2.sucs))`; 57 58val transformLabel_def = Define` 59 transformLabel aP pos neg = 60 FOLDR (\a sofar. (char (POW aP) a) ��� sofar) 61 (FOLDR (\a sofar. (char_neg (POW aP) a) ��� sofar) (POW aP) neg) pos`; 62 63val TRANSFORMLABEL_AP = store_thm 64 ("TRANSFORMLABEL_AP", 65 ``!aP pos neg. transformLabel aP pos neg ��� POW aP``, 66 simp[transformLabel_def]>> Induct_on `neg` 67 >- (Induct_on `pos` >> fs[] >> rpt strip_tac 68 >> fs[char_def] 69 >> `{a | a ��� POW aP ��� h ��� a} ��� POW aP` 70 suffices_by metis_tac[INTER_SUBSET,SUBSET_TRANS] 71 >> simp[SUBSET_DEF] >> rpt strip_tac >> fs[] 72 ) 73 >- (Induct_on `pos` >> fs[] >> rpt strip_tac 74 >> `char_neg (POW aP) h ��� POW aP` suffices_by 75 metis_tac[INTER_SUBSET,SUBSET_TRANS,INTER_ASSOC] 76 >> simp[char_neg_def] 77 ) 78 ); 79 80val TRANSFORMLABEL_SUBSET = store_thm 81 ("TRANSFORMLABEL_SUBSET", 82 ``!aP pos1 neg1 pos2 neg2. 83 MEM_SUBSET pos1 pos2 ��� MEM_SUBSET neg1 neg2 84 ==> 85 (transformLabel aP pos2 neg2 ��� transformLabel aP pos1 neg1)``, 86 simp[transformLabel_def] >> Induct_on `pos1` 87 >- (Induct_on `neg1` >> fs[MEM_SUBSET_def] >> rpt strip_tac 88 >- metis_tac[TRANSFORMLABEL_AP,transformLabel_def] 89 >- metis_tac[FOLDR_INTER,SUBSET_TRANS] 90 ) 91 >- (rpt strip_tac >> fs[MEM_SUBSET_def] 92 >> metis_tac[FOLDR_INTER,SUBSET_TRANS] 93 ) 94 ); 95 96val TRANSFORMLABEL_POS = store_thm 97 ("TRANSFORMLABEL_POS", 98 ``!aP s p x. (s ��� POW aP) ==> 99 ((set p) ��� aP ��� (set p ��� x) ��� x ��� s) 100 = (x ��� FOLDR (��a sofar. char (POW aP) a ��� sofar) s p)``, 101 gen_tac >> Induct_on `p` >> fs[IN_POW] >> rpt strip_tac >> fs[] 102 >> fs[char_def,IN_POW,EQ_IMP_THM] >> rpt strip_tac 103 >> metis_tac[SUBSET_DEF,IN_POW] 104 ); 105 106val TRANSFORMLABEL_NEG = store_thm 107 ("TRANSFORMLABEL_NEG", 108 ``!aP n x. ((set n) ��� aP) ==> 109 (((x ��� (aP DIFF set n)) ��� x ��� aP) 110 = (x ��� FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) n))``, 111 gen_tac >> Induct_on `n` >> fs[IN_POW] >> rpt strip_tac >> fs[] 112 >> fs[char_neg_def,char_def,IN_POW,EQ_IMP_THM] >> rpt strip_tac 113 >- (fs[DIFF_DEF,SUBSET_DEF] >> metis_tac[]) 114 >- (`x ��� aP DIFF set n ��� x ��� aP` by fs[DIFF_DEF,SUBSET_DEF] 115 >> fs[char_neg_def,char_def] 116 >> first_x_assum (qspec_then `x` mp_tac) >> simp[IN_POW] 117 ) 118 >- (first_x_assum (qspec_then `x` mp_tac) >> simp[] 119 >> rpt strip_tac >> simp[DIFF_DEF,INSERT_DEF,SUBSET_DEF] 120 >> rpt strip_tac 121 >- metis_tac[SUBSET_DEF] 122 >- metis_tac[SUBSET_DEF] 123 >- (fs[SUBSET_DEF,DIFF_DEF] >> metis_tac[]) 124 ) 125 ); 126 127val TRANSFORMLABEL_EMPTY = store_thm 128 ("TRANSFORMLABEL_EMPTY", 129 ``!aP pos neg. (set pos) ��� aP ��� (set neg) ��� aP 130 ==> 131 ~((set pos) ��� (set neg) = {}) 132 = (transformLabel aP pos neg = {})``, 133 rpt strip_tac >> simp[EQ_IMP_THM] >> rpt strip_tac 134 >- (simp[transformLabel_def] >> CCONTR_TAC 135 >> `?x. x ��� (FOLDR (��a sofar. char (POW aP) a ��� sofar) 136 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) 137 (POW aP) neg) pos)` 138 by metis_tac[MEMBER_NOT_EMPTY] 139 >> `(set pos ��� aP) ��� (set pos ��� x) 140 ��� (x ��� (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg))` 141 by metis_tac[FOLDR_INTER,TRANSFORMLABEL_POS] 142 >> `x ��� aP DIFF set neg` by metis_tac[TRANSFORMLABEL_NEG] 143 >> `set pos ��� aP DIFF set neg` by metis_tac[SUBSET_TRANS] 144 >> POP_ASSUM mp_tac >> simp[SUBSET_DEF,DIFF_DEF] 145 >> `?v. v ��� (set pos ��� set neg)` by metis_tac[MEMBER_NOT_EMPTY] 146 >> qexists_tac `v` >> fs[] 147 ) 148 >- (fs[transformLabel_def] 149 >> `(aP DIFF set neg) ��� 150 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg)` by ( 151 `(aP DIFF set neg ��� aP DIFF set neg) ��� (aP DIFF set neg) ��� aP` 152 suffices_by metis_tac[TRANSFORMLABEL_NEG] 153 >> simp[DIFF_DEF,SUBSET_DEF] 154 ) 155 >> `set pos ��� aP DIFF set neg` 156 suffices_by metis_tac[FOLDR_INTER,TRANSFORMLABEL_POS, 157 MEMBER_NOT_EMPTY] 158 >> simp[DIFF_DEF,SUBSET_DEF] >> rpt strip_tac 159 >- metis_tac[SUBSET_DEF] 160 >- (`x ��� (set pos ��� set neg)` by fs[IN_INTER] 161 >> metis_tac[MEMBER_NOT_EMPTY] 162 ) 163 ) 164 ); 165 166val TRANSFORMLABEL_SUBSET2 = store_thm 167 ("TRANSFORMLABEL_SUBSET2", 168 ``!aP pos1 neg1 pos2 neg2. 169 (!x. (MEM x pos1 \/ MEM x pos2 \/ MEM x neg1 \/ MEM x neg2) 170 ==> x ��� aP 171 ) 172 ��� ~(transformLabel aP pos2 neg2 = {}) 173 ��� (transformLabel aP pos2 neg2 ��� transformLabel aP pos1 neg1) 174 ==> MEM_SUBSET pos1 pos2 ��� MEM_SUBSET neg1 neg2``, 175 rpt strip_tac >> CCONTR_TAC 176 >> `set pos2 ��� aP ��� set neg2 ��� aP` 177 by (fs[SUBSET_DEF] >> rpt strip_tac >> metis_tac[MEM]) 178 >> `?a. a ��� transformLabel aP pos2 neg2` by metis_tac[MEMBER_NOT_EMPTY] 179 >> `a ��� transformLabel aP pos1 neg1` by fs[SUBSET_DEF] 180 >> `set pos2 ��� set neg2 = {}` by metis_tac[TRANSFORMLABEL_EMPTY] 181 >> fs[transformLabel_def] 182 >- (`?x. MEM x pos1 ��� ~MEM x pos2` by ( 183 fs[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] >> metis_tac[] 184 ) 185 >> `a DELETE x ��� 186 FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2` by ( 187 `(a DELETE x) ��� aP DIFF set neg2 ��� (a DELETE x) ��� aP` 188 suffices_by metis_tac[TRANSFORMLABEL_NEG] 189 >> `a ��� aP DIFF set neg2` 190 by metis_tac[TRANSFORMLABEL_NEG,TRANSFORMLABEL_POS,FOLDR_INTER] 191 >> fs[DELETE_DEF,DIFF_DEF,SUBSET_DEF] >> rpt strip_tac 192 ) 193 >> `a DELETE x ��� 194 FOLDR (��a sofar. char (POW aP) a ��� sofar) 195 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2) 196 pos2` by ( 197 `set pos2 ��� aP ��� set pos2 ��� (a DELETE x)` 198 suffices_by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 199 >> `set pos2 ��� a` by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 200 >> fs[DELETE_DEF,SUBSET_DEF] 201 ) 202 >> `~(a DELETE x ��� 203 FOLDR (��a sofar. char (POW aP) a ��� sofar) 204 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg1) 205 pos1)` by ( 206 `~(set pos1 ��� a DELETE x)` 207 suffices_by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 208 >> simp[DELETE_DEF,SUBSET_DEF] >> metis_tac[MEM] 209 ) 210 >> metis_tac[SUBSET_DEF] 211 ) 212 >- (`?x. MEM x neg1 ��� ~MEM x neg2` by ( 213 fs[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] >> metis_tac[] 214 ) 215 >> `x INSERT a ��� 216 FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2` by ( 217 `(x INSERT a) ��� aP DIFF set neg2 ��� (x INSERT a) ��� aP` 218 suffices_by metis_tac[TRANSFORMLABEL_NEG] 219 >> `a ��� aP DIFF set neg2` 220 by metis_tac[TRANSFORMLABEL_NEG,TRANSFORMLABEL_POS,FOLDR_INTER] 221 >> fs[INSERT_DEF,DIFF_DEF,SUBSET_DEF] >> rpt strip_tac 222 ) 223 >> `x INSERT a ��� 224 FOLDR (��a sofar. char (POW aP) a ��� sofar) 225 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2) 226 pos2` by ( 227 `set pos2 ��� aP ��� set pos2 ��� (x INSERT a)` 228 suffices_by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 229 >> `set pos2 ��� a` by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 230 >> fs[INSERT_DEF,SUBSET_DEF] 231 ) 232 >> `~(x INSERT a ��� 233 FOLDR (��a sofar. char (POW aP) a ��� sofar) 234 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg1) 235 pos1)` by ( 236 CCONTR_TAC >> fs[] 237 >> `x INSERT a ��� 238 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg1)` 239 by metis_tac[TRANSFORMLABEL_POS,FOLDR_INTER] 240 >> `set neg1 ��� aP` by (fs[SUBSET_DEF] >> metis_tac[MEM]) 241 >> `(x INSERT a ��� (aP DIFF set neg1))` 242 by metis_tac[TRANSFORMLABEL_NEG,FOLDR_INTER] 243 >> fs[INSERT_DEF,SUBSET_DEF,DIFF_DEF] 244 ) 245 >> metis_tac[SUBSET_DEF] 246 ) 247 ); 248 249 250(* val TRANSFORM_LABEL_POS = store_thm *) 251(* ("TRANSFORM_LABEL_POS", *) 252(* ``!aP neg a pos. a ��� aP ==> *) 253(* (MEM a pos = !m. m ��� transformLabel aP pos neg ==> a ��� m) *) 254(* ��� (MEM a neg = !m. m ��� transformLabel aP pos neg ==> ~(a ��� m))``, *) 255(* gen_tac >> gen_tac >> gen_tac >> Induct_on `pos` >> fs[] >> rpt strip_tac *) 256(* >- (fs[transformLabel_def] *) 257(* >> `!n. {} ��� FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) n` *) 258(* by (Induct_on `n` >> fs[IN_POW,char_neg_def,char_def]) *) 259(* >> metis_tac[NOT_IN_EMPTY] *) 260(* ) *) 261(* >- (fs[transformLabel_def] >> simp[EQ_IMP_THM] >> rpt strip_tac >> fs[] *) 262(* >- (`m ��� char_neg (POW aP) a` by metis_tac[SUBSET_DEF,FOLDR_INTER] *) 263(* >> fs[char_neg_def,char_def] >> metis_tac[] *) 264(* ) *) 265(* >- (Induct_on `neg` >> fs[] *) 266(* >- (qexists_tac `{a}` >> fs[IN_POW]) *) 267(* >- (rpt strip_tac >> fs[] >> Cases_on `MEM a neg` >> fs[] *) 268(* >> Cases_on `MEM h neg` >> fs[] *) 269(* >- (first_x_assum (qspec_then `m` mp_tac) >> simp[] *) 270(* >> `m ��� char_neg (POW aP) h` *) 271(* by metis_tac[FOLDR_INTER,SUBSET_DEF] *) 272(* >> metis_tac[] *) 273(* ) *) 274(* >- (first_x_assum (qspec_then `(a INSERT m) DELETE h` mp_tac) *) 275(* >> simp[] *) 276(* >> `(a INSERT m) DELETE h ��� char_neg (POW aP) h` by ( *) 277(* simp[char_neg_def,char_def] *) 278(* >> `m ��� aP` by metis_tac[FOLDR_INTER,IN_POW,SUBSET_DEF] *) 279(* >> PURE_REWRITE_TAC[INSERT_DEF,DELETE_DEF] *) 280(* >> simp[DIFF_DEF,IN_POW,SUBSET_DEF] >> rpt strip_tac *) 281(* >> metis_tac[SUBSET_DEF] *) 282(* ) *) 283(* >> simp[] *) 284(* >> `(a INSERT m) DELETE h ��� *) 285(* FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg` *) 286(* by ( *) 287(* Induct_on `neg` >> fs[] >> rpt strip_tac *) 288(* >- (PURE_REWRITE_TAC[INSERT_DEF,DELETE_DEF] *) 289(* >> simp[DIFF_DEF,IN_POW,SUBSET_DEF] >> rpt strip_tac *) 290(* >> metis_tac[IN_POW,SUBSET_DEF] *) 291(* ) *) 292(* >- (fs[] >> PURE_REWRITE_TAC[INSERT_DEF,DELETE_DEF] *) 293(* >> simp[DIFF_DEF,IN_POW,SUBSET_DEF] >> rpt strip_tac *) 294(* >> simp[char_neg_def,char_def,IN_POW,SUBSET_DEF] *) 295(* >> rpt strip_tac *) 296(* >- metis_tac[] *) 297(* >- (`m ��� aP` by metis_tac[FOLDR_INTER,IN_POW,SUBSET_DEF] *) 298(* >> metis_tac[SUBSET_DEF] *) 299(* ) *) 300(* >- (disj2_tac >> fs[char_neg_def,char_def] *) 301(* >> metis_tac[]) *) 302(* ) *) 303(* >> fs[] *) 304(* ) *) 305(* >> fs[] *) 306(* ) *) 307(* ) *) 308(* ) *) 309(* >- (Cases_on `a = h` >> fs[] *) 310(* >- (fs[transformLabel_def,char_def] >> metis_tac[]) *) 311(* >- (simp[EQ_IMP_THM] >> rpt strip_tac >> fs[] *) 312(* >- (fs[transformLabel_def,char_def] >> metis_tac[]) *) 313(* >- (Cases_on `MEM a pos` >> fs[] *) 314(* >> Cases_on `MEM a neg` >> fs[] *) 315(* >- (`transformLabel aP (h::pos) neg = {}` by ( *) 316(* fs[transformLabel_def] *) 317(* >> PURE_REWRITE_TAC[SET_EQ_SUBSET,SUBSET_DEF] *) 318(* >> simp[] >> rpt strip_tac >> CCONTR_TAC *) 319(* >> fs[] >> metis_tac[] *) 320(* ) *) 321(* >> fs[transformLabel_def] >> Cases_on `m' ��� char (POW aP) h` *) 322(* >- (`m' ��� {}` by metis_tac[IN_INTER,SET_EQ_SUBSET] >> fs[]) *) 323(* >- (`m' ��� char_neg fs[char_def] >> *) 324 325 326(* >- metis_tac[FOLDR_INTER,SUBSET_DEF,IN_POW] *) 327(* >- *) 328(* ) *) 329(* ) *) 330 331 332 333(* >> `!b p n. MEM b p ��� MEM b n ==> transformLabel aP p n = {}` by ( *) 334(* gen_tac >> Induct_on `p` >> Induct_on `n` *) 335(* >> fs[transformLabel_def] >> rpt strip_tac >> fs[] *) 336(* >- (PURE_REWRITE_TAC[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac *) 337(* >- (`x ��� char (POW aP) b ��� x ��� char_neg (POW aP) b` by ( *) 338(* metis_tac[FOLDR_INTER,SUBSET_DEF,IN_INTER] *) 339(* ) *) 340(* >> fs[char_def,char_neg_def] *) 341(* >> metis_tac[] *) 342(* ) *) 343(* >- metis_tac[MEMBER_NOT_EMPTY] *) 344(* ) *) 345(* >- (rw[] *) 346(* >> `char (POW aP) b ��� *) 347(* (FOLDR (��a sofar. char (POW aP) a ��� sofar) *) 348(* (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) n) *) 349(* p) = {}` by metis_tac[] *) 350(* >> *) 351 352 353 354(* metis_tac[FOLDR_INTER,SUBSET_EMPTY,INTER_EMPTY,SUBSET_TRANS]) *) 355 356 357(* `char (POW aP) b ��� char_neg (POW aP) b = {}` suffices_by ( *) 358(* metis_tac[FOLDR_INTER,INTER_SUBSET] *) 359(* ) *) 360 361 362(* FOLDR (��a sofar. char (POW aP) a ��� sofar) *) 363(* (char_neg (POW aP) b ��� *) 364(* FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) n) p` *) 365 366 367(* rw[]) *) 368 369(* ) *) 370 371 372(* >> `h INSERT m' ��� transformLabel aP (h::pos) neg` by ( *) 373(* fs[transformLabel_def] *) 374(* ) *) 375 376 377 378(* `m ��� transformLabel aP (h::pos) neg` by ( *) 379(* `MEM_SUBSET pos (h::pos)` by ( *) 380(* fs[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] *) 381(* ) *) 382(* >> metis_tac[TRANSFORMLABEL_SUBSET,SUBSET_DEF,MEM_SUBSET_REFL] *) 383(* fs[TRANSFORMLABEL_SUBSET,SUBSET_DEF,MEM] *) 384 385 386(* )) *) 387 388 389(* >- (`!q n p. (���m. m ��� transformLabel aP (q::p) n ��� a ��� m) *) 390(* ��� ~(q = a) ==> (���m. m ��� transformLabel aP p n ��� a ��� m)` by ( *) 391(* gen_tac >> Induct_on `n` >> Induct_on `p` >> fs[transformLabel_def] *) 392(* >> rpt strip_tac *) 393(* >- (fs[char_def] >> ) *) 394(* ) *) 395(* ) *) 396 397(* ) *) 398 399 400 401 402 403(* a pos neg. MEM a pos ��� a ��� aP *) 404(* ==> !m. m ��� transformLabel aP pos neg ==> a ��� m) *) 405(* ��� (!aP a pos neg. ~MEM a pos ��� a ��� aP *) 406(* ==> ?m. m ��� transformLabel aP ��� *) 407(* ) *) 408 409(* ``, *) 410(* gen_tac >> gen_tac >> Induct_on `pos` >> fs[] >> rpt strip_tac *) 411(* >> fs[transformLabel_def,char_def] >> metis_tac[] *) 412(* ); *) 413 414(* val TRANSFORM_LABEL_NEG = store_thm *) 415(* ("TRANSFORM_LABEL_NEG", *) 416(* ``!aP a pos neg. MEM a neg ��� a ��� aP *) 417(* ==> !m. m ��� transformLabel aP pos neg ==> ~(a ��� m)``, *) 418(* gen_tac >> gen_tac >> Induct_on `neg` >> fs[] >> rpt strip_tac *) 419(* >> fs[transformLabel_def] *) 420(* >- (`m ��� char_neg (POW aP) h` *) 421(* by metis_tac[FOLDR_INTER,SUBSET_DEF,IN_INTER] *) 422(* >> fs[char_neg_def,char_def] *) 423(* >> metis_tac[] *) 424(* ) *) 425(* >- (`!l x q p. *) 426(* x ��� (FOLDR (��a sofar. char (POW aP) a ��� sofar) (q ��� l) p) *) 427(* ==> x ��� (FOLDR (��a sofar. char (POW aP) a ��� sofar) l p)` by ( *) 428(* Induct_on `p` >> fs[] >> rpt strip_tac >> fs[] *) 429(* >> metis_tac[] *) 430(* ) *) 431(* >> metis_tac[] *) 432(* ) *) 433(* ); *) 434 435 436 437 438(* gen_tac >> Induct_on `pos2` >> fs[] *) 439(* >- (Induct_on `pos1` >> fs[MEM_SUBSET_def] *) 440(* >- (Induct_on `neg2` >> fs[transformLabel_def] *) 441(* >- (Induct_on `neg1` >> fs[MEM_SUBSET_def] >> rpt strip_tac *) 442(* >> Cases_on `POW aP ��� *) 443(* FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) *) 444(* (POW aP) neg1` >> fs[] *) 445(* >> Cases_on `(���x. (x = h ��� MEM x neg1) ��� x ��� aP)` >> fs[] *) 446(* >- metis_tac[] *) 447(* >- metis_tac[] *) 448(* >- (disj2_tac >> `MEM_SUBSET neg1 []` by metis_tac[] *) 449(* >> simp[char_neg_def] *) 450(* >> `neg1 = []` by fs[MEM_SUBSET_SET_TO_LIST] >> rw[] *) 451(* >> fs[] >> simp[char_def] >> CCONTR_TAC *) 452(* >> fs[] >> `{h} ��� POW aP` by fs[IN_POW] *) 453(* >> `{h} ��� POW aP DIFF {a | a ��� POW aP ��� h ��� a}` *) 454(* by metis_tac[SUBSET_DEF] *) 455(* >> fs[IN_DIFF,IN_POW] *) 456(* ) *) 457(* >- (rpt strip_tac >> first_x_assum (qspec_then `h::neg1` mp_tac) *) 458(* >> simp[] *) 459(* >> `(���x. (x = h ��� MEM x neg1) ��� MEM x neg2 ��� x ��� aP) *) 460(* ��� FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2 ��� *) 461(* char_neg (POW aP) h *) 462(* ��� (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg2 ��� *) 463(* FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) neg1)` *) 464(* by ( *) 465(* rpt strip_tac >> fs[] *) 466(* >- *) 467(* ) *) 468(* ) *) 469(* ) *) 470 471(* ) *) 472(* >- () *) 473(* ) *) 474 475 476(* ) *) 477 478 479val TRANSFORMLABEL_FOLDR = store_thm 480 ("TRANSFORMLABEL_FOLDR", 481 ``!aP l x. 482 (!e. MEM e l ==> x ��� transformLabel aP e.pos e.neg) 483 ��� (x ��� (POW aP)) 484 ==> x ��� 485 transformLabel aP 486 (FOLDR (��e pr. e.pos ++ pr) [] l) 487 (FOLDR (��e pr. e.neg ++ pr) [] l)``, 488 Induct_on `l` >> fs[transformLabel_def] >> rpt strip_tac 489 >> `x ��� 490 FOLDR (��a sofar. char (POW aP) a ��� sofar) 491 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) h.neg) 492 h.pos` by metis_tac[] 493 >> `x ��� 494 FOLDR (��a sofar. char (POW aP) a ��� sofar) 495 (FOLDR (��a sofar. char_neg (POW aP) a ��� sofar) (POW aP) 496 (FOLDR (��e pr. e.neg ��� pr) [] l)) 497 (FOLDR (��e pr. e.pos ��� pr) [] l)` by metis_tac[] 498 >> rw[FOLDR_LEMM5] 499 ); 500 501val concr2AbstractEdge_def = Define` 502 concr2AbstractEdge aP (concrEdge pos neg sucs) = 503 (transformLabel aP pos neg, set sucs)`; 504 505val C2A_EDGE_CE_EQUIV = store_thm 506 ("C2A_EDGE_CE_EQUIV", 507 ``!aP cE1 cE2. cE_equiv cE1 cE2 508 ==> (concr2AbstractEdge aP cE1 = concr2AbstractEdge aP cE2)``, 509 rpt strip_tac >> Cases_on `cE1` >> Cases_on `cE2` >> fs[cE_equiv_def] 510 >> simp[concr2AbstractEdge_def] >> strip_tac >> fs[MEM_EQUAL_SET] 511 >> simp[transformLabel_def] 512 >> metis_tac[FOLDR_INTER_MEMEQUAL] 513 ); 514 515val extractTrans_def = Define` 516 extractTrans graph s = 517 let sucs = 518 OPTION_TO_LIST 519 (do (nId,nodeLabel) <- findNode (��(n,l). l.frml = s) graph ; 520 lookup nId graph.followers 521 od 522 ) 523 in let trueLabels = 524 OPTION_TO_LIST 525 (do (nId, nodeLabel) <- findNode (��(n,l). l.frml = s) graph ; 526 SOME nodeLabel.true_labels 527 od 528 ) 529 in { edge | ?label labelSucs. 0 < label.edge_grp 530 ��� labelSucs = 531 { suc.frml 532 | ?sucId. MEM (label,sucId) sucs 533 ��� SOME suc = lookup sucId graph.nodeInfo 534 } 535 ��� ~(labelSucs = {}) 536 ��� edge = (label.edge_grp, label.pos_lab, 537 label.neg_lab, labelSucs) } 538 ��� { (0,l.pos_lab,l.neg_lab,{}) | MEM l trueLabels }`; 539 540val concrTrans_def = Define ` 541 concrTrans g prop f = 542 IMAGE (��(i,p,n,e). (transformLabel prop p n,e)) (extractTrans g f)`; 543 544val concr2AbstrAA_def = Define` 545 concr2AbstrAA (concrAA g init prop) = 546 ALTER_A 547 (concr2Abstr_states g) 548 (POW (LIST_TO_SET prop)) 549 (concrTrans g (set prop)) 550 (concr2Abstr_init init g) 551 (concr2Abstr_final g)`; 552 553val graphStatesWithId_def = Define` 554 graphStatesWithId g = 555 MAP (��(id,label). (id, label.frml)) (toAList g.nodeInfo)`; 556 557val GRAPH_STATES_WITH_ID_LEMM = store_thm 558 ("GRAPH_STATES_WITH_ID_LEMM", 559 ``!g id q. MEM (id,q) (toAList g.nodeInfo) 560 ==> MEM (id,q.frml) (graphStatesWithId g)``, 561 rpt strip_tac >> fs[graphStatesWithId_def,MEM_MAP] 562 >> qexists_tac `(id,q)` >> fs[] 563 ); 564 565val GRAPHSTATES_WITH_ID_EMPTY = store_thm 566 ("GRAPHSTATES_WITH_ID_EMPTY", 567 ``graphStatesWithId empty = []``, 568 simp[graphStatesWithId_def,toAList_def,empty_def,foldi_def] 569 ); 570 571val unique_node_formula_def = Define` 572 unique_node_formula g = 573 ���id h. 574 MEM (id,h) (graphStatesWithId g) ��� 575 ���oId. MEM (oId,h) (graphStatesWithId g) ��� (id = oId)`; 576 577val UNIQUE_NODE_FORM_EMPTY = store_thm 578 ("UNIQUE_NODE_FORM_EMPTY", 579 ``unique_node_formula empty``, 580 fs[unique_node_formula_def] >> rpt strip_tac 581 >> fs[GRAPHSTATES_WITH_ID_EMPTY] 582 ); 583 584val UNIQUE_NODE_FORM_LEMM = store_thm 585 ("UNIQUE_NODE_FORM_LEMM", 586 ``!g f. unique_node_formula g 587 ==> (OPTION_MAP (��(id,label). (id,label.frml)) 588 (findNode (��(n,l). l.frml = f) g) 589 = FIND (��a. SND a = f) (graphStatesWithId g))``, 590 rpt strip_tac >> fs[findNode_def,graphStatesWithId_def] 591 >> Cases_on 592 `FIND (��a. SND a = f) 593 (MAP (��(id,label). (id,label.frml)) 594 (toAList g.nodeInfo))` 595 >- (fs[] 596 >> `!x. MEM x (MAP (��(id,label). (id,label.frml)) (toAList g.nodeInfo)) 597 ==> ~((��a. SND a = f) x)` by ( 598 Q.HO_MATCH_ABBREV_TAC `!x. MEM x L ==> ~P x` 599 >> rpt strip_tac 600 >> `?z. FIND P L = SOME z` by metis_tac[FIND_LEMM] 601 >> fs[] 602 ) 603 >> Q.HO_MATCH_ABBREV_TAC `FIND P L = NONE` 604 >> `!x. MEM x L ==> ~P x` by ( 605 rpt strip_tac 606 >> first_x_assum 607 (qspec_then `(��(id,label). (id,label.frml)) x` mp_tac) 608 >> fs[MEM_MAP] >> rpt strip_tac 609 >- (qunabbrev_tac `P` >> fs[] >> metis_tac[]) 610 >- (qunabbrev_tac `P` >> Cases_on `x` >> fs[]) 611 ) 612 >> `!x. ~(FIND P L = SOME x)` by ( 613 rpt strip_tac >> metis_tac[FIND_LEMM2] 614 ) 615 >> Cases_on `FIND P L` >> fs[] 616 ) 617 >- (`MEM x (MAP 618 (��(id,label). (id,label.frml)) 619 (toAList g.nodeInfo)) 620 ��� (��a. SND a = f) x` 621 by (Q.HO_MATCH_ABBREV_TAC `MEM x L ��� P x` >> metis_tac[FIND_LEMM2]) 622 >> `?y.(FIND (��(n,l). l.frml = f) (toAList g.nodeInfo)) = SOME y 623 ��� (��(id,label). (id,label.frml)) y = x` suffices_by ( 624 fs[] >> rpt strip_tac >> fs[] 625 ) 626 >> fs[unique_node_formula_def,graphStatesWithId_def] 627 >> `?z. MEM z (toAList g.nodeInfo) ��� (��(n,l). l.frml = f) z` 628 by (fs[MEM_MAP] >> qexists_tac `y` >> Cases_on `y` >> fs[] >> rw[]) 629 >> `?a. FIND (��(n,l). l.frml = f) (toAList g.nodeInfo) = SOME a` 630 by metis_tac[FIND_LEMM] 631 >> qexists_tac `a` >> fs[] >> Cases_on `a` >> Cases_on `x` 632 >> fs[] >> first_x_assum (qspec_then `q'` mp_tac) >> strip_tac 633 >> first_x_assum (qspec_then `f` mp_tac) >> simp[] >> strip_tac 634 >> first_x_assum (qspec_then `q` mp_tac) >> strip_tac 635 >> `MEM (q,r) (toAList g.nodeInfo) ��� (��(n,l). l.frml = f) (q,r)` 636 by metis_tac[FIND_LEMM2] >> fs[] 637 >> `MEM (q,f) 638 (MAP (��(id,label). (id,label.frml)) (toAList g.nodeInfo))` by ( 639 simp[MEM_MAP] >> qexists_tac `(q,r)` >> fs[] 640 ) 641 >> metis_tac[] 642 ) 643 ); 644 645val UNIQUE_NODE_FORM_LEMM2 = store_thm 646 ("UNIQUE_NODE_FORM_LEMM2", 647 ``!g. unique_node_formula g 648 ==> (!f x. (SND x = f) ��� MEM x (graphStatesWithId g) 649 ==> !y. (SND y = f) ��� MEM y (graphStatesWithId g) 650 ==> (x = y))``, 651 rpt strip_tac >> fs[graphStatesWithId_def,unique_node_formula_def] 652 >> Cases_on `x` >> Cases_on `y` 653 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 654 >> first_x_assum (qspec_then `f` mp_tac) 655 >> `MEM (q,f) 656 (MAP (��(id,label). (id,label.frml)) (toAList g.nodeInfo))` 657 by (fs[MEM_MAP] >> qexists_tac `y` >> Cases_on `y` >> fs[]) 658 >> simp[] >> strip_tac 659 >> first_x_assum (qspec_then `q'` mp_tac) 660 >> `MEM (q',f) (MAP (��(id,label). (id,label.frml)) (toAList g.nodeInfo))` 661 by (fs[MEM_MAP] >> qexists_tac `y'` >> Cases_on `y'` >> fs[]) 662 >> simp[] >> fs[] 663 ); 664 665val UNIQUE_NODE_FIND_LEMM = store_thm 666 ("UNIQUE_NODE_FIND_LEMM", 667 ``!g id node f. unique_node_formula g ��� (lookup id g.nodeInfo = SOME node) 668 ==> (findNode (��(n,l). l.frml = node.frml) g = SOME (id,node))``, 669 rpt strip_tac >> fs[unique_node_formula_def,findNode_def] 670 >> `?x. FIND (��(n,l). l.frml = node.frml) (toAList g.nodeInfo) = SOME x` by ( 671 `?x. MEM x (toAList g.nodeInfo) ��� (��(n,l). l.frml = node.frml) x` 672 suffices_by metis_tac[FIND_LEMM] 673 >> qexists_tac `(id,node)` >> fs[MEM_toAList] 674 ) 675 >> `?id2 node2. x = (id2,node2)` by (Cases_on `x` >> fs[]) 676 >> `node2.frml = node.frml ��� MEM x (toAList g.nodeInfo)` by ( 677 strip_tac 678 >- (`(��(n,l). l.frml = node.frml) (id2,node2)` suffices_by fs[] 679 >> metis_tac[FIND_LEMM2]) 680 >- metis_tac[FIND_LEMM2] 681 ) 682 >> `MEM (id2,node2.frml) (graphStatesWithId g)` 683 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 684 >> `MEM (id,node.frml) (graphStatesWithId g)` 685 by metis_tac[GRAPH_STATES_WITH_ID_LEMM,MEM_toAList] 686 >> `id = id2` by (rw[] >> metis_tac[]) 687 >> rw[] >> metis_tac[MEM_toAList,SOME_11] 688 ); 689 690 691val EXTR_TRANS_LEMM = store_thm 692 ("EXTR_TRANS_LEMM", 693 ``!g sucId suc id label fls q. 694 (lookup id g.nodeInfo = SOME q) 695 ��� (lookup id g.followers = SOME fls) 696 ��� (lookup sucId g.nodeInfo = SOME suc) 697 ��� (MEM (label,sucId) fls) 698 ��� (unique_node_formula g) 699 ��� (0 < label.edge_grp) 700 ==> (?s. (label.edge_grp,label.pos_lab,label.neg_lab,s) 701 ��� extractTrans g q.frml 702 ��� (suc.frml ��� s))``, 703 rpt strip_tac >> simp[extractTrans_def] >> CCONTR_TAC 704 >> fs[] 705 >> qabbrev_tac `P = ��label:�� edgeLabelAA. 706 {suc.frml | 707 ���sucId. 708 MEM (label,sucId) 709 (OPTION_TO_LIST 710 do 711 (nId,nodeLabel) <- 712 findNode (��(n,l). l.frml = q.frml) g; 713 lookup nId g.followers 714 od) ��� SOME suc = lookup sucId g.nodeInfo}` 715 >> `findNode (��(n,l). l.frml = q.frml) g = SOME (id,q)` by ( 716 `?x. findNode (��(n,l). l.frml = q.frml) g = SOME x` by ( 717 fs[findNode_def] 718 >> `(��(n,l). l.frml = q.frml) (id,q)` by fs[] 719 >> metis_tac[FIND_LEMM,MEM_toAList] 720 ) 721 >> Cases_on `x` >> fs[] 722 >> `(��(n,l). l.frml = q.frml) (id,q) 723 ��� (MEM (id,q) (toAList g.nodeInfo))` by fs[MEM_toAList] 724 >> `(��(n,l). l.frml = q.frml) (q',r) 725 ��� (MEM (q',r) (toAList g.nodeInfo))` 726 by metis_tac[FIND_LEMM2,findNode_def] 727 >> `q' = id` by ( 728 fs[unique_node_formula_def] 729 >> metis_tac[GRAPH_STATES_WITH_ID_LEMM] 730 ) 731 >> rw[] >> metis_tac[MEM_toAList,SOME_11] 732 ) 733 >> `~(P label = {})` by ( 734 `?n. n ��� P label` suffices_by metis_tac[MEMBER_NOT_EMPTY] 735 >> qunabbrev_tac `P` >> fs[] >> qexists_tac `suc` >> qexists_tac `sucId` 736 >> simp[OPTION_TO_LIST_MEM] >> qexists_tac `fls` >> fs[] 737 >> qexists_tac `(id,q)` >> fs[] 738 ) 739 >> first_x_assum (qspec_then `P label` mp_tac) >> simp[] 740 >> rpt strip_tac >> fs[] 741 >- (qexists_tac `label` >> fs[]) 742 >- (qunabbrev_tac `P` >> fs[] >> qexists_tac `suc` >> fs[] 743 >> qexists_tac `sucId` >> fs[OPTION_TO_LIST_MEM] 744 >> qexists_tac `fls` >> fs[] 745 ) 746 ); 747 748val graphStates_def = Define 749 `graphStates g = MAP ((\l. l.frml) o SND) (toAList g.nodeInfo)`; 750 751val GRAPHSTATES_EMPTY = store_thm 752 ("GRAPHSTATES_EMPTY", 753 ``graphStates empty = []``, 754 simp[graphStates_def,toAList_def,empty_def,foldi_def] 755 ); 756 757val GRAPHSTATES_CONCR_LEMM = store_thm 758 ("GRAPHSTATES_CONCR_LEMM", 759 ``!g. set (graphStates g) = concr2Abstr_states g``, 760 rpt strip_tac >> simp[graphStates_def,concr2Abstr_states_def] 761 >> simp[SET_EQ_SUBSET,SUBSET_DEF,MEM_MAP] >> rpt strip_tac 762 >- (qexists_tac `SND y` >> simp[] 763 >> fs[MEM_toAList,domain_lookup] >> rw[] 764 >> Cases_on `y` >> fs[MEM_toAList] >> metis_tac[] 765 ) 766 >- (qexists_tac `(n,x')` >> simp[] >> simp[MEM_toAList]) 767 ); 768 769val GRAPH_STATES_ID_IMP_GRAPH_STATES = store_thm 770 ("GRAPH_STATES_ID_IMP_GRAPH_STATES", 771 ``!g1 g2. 772 set (graphStatesWithId g1) = set (graphStatesWithId g2) 773 ==> (set (graphStates g1) = set (graphStates g2))``, 774 rpt strip_tac >> fs[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 775 >> fs[graphStates_def,MEM_MAP] >> Cases_on `y` 776 >- (`MEM (q,r.frml) (graphStatesWithId g2)` 777 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 778 >> POP_ASSUM mp_tac >> simp[graphStatesWithId_def,MEM_MAP] 779 >> rpt strip_tac >> qexists_tac `y` >> Cases_on `y` >> fs[] 780 ) 781 >- (`MEM (q,r.frml) (graphStatesWithId g1)` 782 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 783 >> POP_ASSUM mp_tac >> simp[graphStatesWithId_def,MEM_MAP] 784 >> rpt strip_tac >> qexists_tac `y` >> Cases_on `y` >> fs[] 785 ) 786 ); 787 788val autoStates_def = Define` 789 autoStates (concrAA g i aP) = graphStates g`; 790 791val inAuto_def = Define` 792 inAuto aut f = MEM f (autoStates aut)`; 793 794val IN_AUTO_FINITE = store_thm 795 ("IN_AUTO_FINITE", 796 ``!aut. FINITE (LIST_TO_SET (autoStates aut))``, 797 rpt strip_tac >> metis_tac[FINITE_LIST_TO_SET] 798 ); 799 800val addFrmlToGraph_def = Define` 801 (addFrmlToGraph g (U f1 f2) = 802 if MEM (U f1 f2) (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo)) 803 then g 804 else addNode <| frml := (U f1 f2); is_final := T 805 ; true_labels := [] |> g) 806 ��� (addFrmlToGraph g f = 807 if MEM f (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo)) 808 then g 809 else addNode <| frml := f; is_final := F ; true_labels := []|> g)`; 810 811val ADDFRML_LEMM = store_thm 812 ("ADDFRML_LEMM", 813 ``!g f. MEM f (graphStates (addFrmlToGraph g f))``, 814 rpt strip_tac >> Cases_on `MEM f (graphStates g)` 815 >- (Cases_on `f` >> fs[addFrmlToGraph_def,graphStates_def]) 816 >- (Cases_on `?f1 f2. f = U f1 f2` 817 >- (fs[addFrmlToGraph_def] >> rw[] 818 >> fs[graphStates_def,MEM_MAP] 819 >> Cases_on `���y. U f1 f2 = (SND y).frml 820 ��� MEM y (toAList g.nodeInfo)` >> fs[] 821 >- metis_tac[] 822 >- (fs[addNode_def,MEM_toAList] 823 >> qexists_tac `(g.next,<|frml := U f1 f2; 824 is_final := T ; true_labels := []|>)` 825 >> fs[MEM_toAList] >> rw[] >> metis_tac[]) 826 ) 827 >- (qabbrev_tac `el = (g.next,<|frml := f; is_final := F; 828 true_labels := []|>)` 829 >> Cases_on `f` >> fs[addFrmlToGraph_def, graphStates_def,MEM_MAP] 830 >> fs[addNode_def,MEM_toAList] 831 >> qexists_tac `el` >> qunabbrev_tac `el` >> fs[MEM_toAList] 832 >> rw[] >> metis_tac[] 833 ) 834 ) 835 ); 836 837val ADDFRML_LEMM_AUT = store_thm 838 ("ADDFRML_LEMM_AUT", 839 ``!g i aP f. inAuto (concrAA (addFrmlToGraph g f) i aP) f``, 840 metis_tac[inAuto_def,autoStates_def,ADDFRML_LEMM] 841 ); 842 843val addEdgeToGraph_def = Define` 844 addEdgeToGraph f (concrEdge pos neg sucs) g = 845 if sucs = [] 846 then do (nodeId,nodeLabel) <- findNode (��(n,l). l.frml = f) g; 847 newlabel <- SOME (nodeLabelAA 848 nodeLabel.frml 849 nodeLabel.is_final 850 ((edgeLabelAA 0 pos neg) 851 :: nodeLabel.true_labels)) ; 852 updateNode nodeId newlabel g 853 od 854 else 855 let sucIds = MAP FST 856 (CAT_OPTIONS (MAP (\s. findNode (��(n,l). l.frml = s) g) sucs)) 857 in do (nodeId,nodeLabel) <- findNode (��(n,l). l.frml = f) g; 858 oldSucPairs <- lookup nodeId g.followers ; 859 oldSucs <- SOME (MAP FST oldSucPairs); 860 lstGrpId <- SOME (if oldSucs = [] then 1 else (HD oldSucs).edge_grp) ; 861 unfolded_edges <- SOME 862 (MAP (\i. (<| edge_grp := lstGrpId + 1; 863 pos_lab := pos ; 864 neg_lab := neg ; |>,i)) sucIds); 865 FOLDR (\e g_opt. do g_int <- g_opt ; 866 newGraph <- addEdge nodeId e g_int; 867 SOME newGraph 868 od) 869 (SOME g) unfolded_edges 870 od`; 871 872val empty_followers_def = Define` 873 empty_followers g f = 874 !id node. (lookup id g.nodeInfo = SOME node 875 ��� node.frml = f) 876 ==> (lookup id g.followers = SOME [] 877 ��� node.true_labels = [])`; 878 879val EMPTY_FLWS_GRAPHSTATES = store_thm 880 ("EMPTY_FLWS_GRAPHSTATES", 881 ``!g x. ~(MEM x (graphStates g)) ==> empty_followers g x``, 882 rpt strip_tac >> fs[graphStates_def,empty_followers_def] >> rpt strip_tac 883 >> fs[MEM_MAP] 884 >> `MEM (id,node) (toAList g.nodeInfo)` 885 by metis_tac[MEM_toAList] 886 >> `(SND (id,node)).frml = x` by fs[] 887 >> metis_tac[] 888 ); 889 890val EMPTY_FLWS_LEMM = store_thm 891 ("EMPTY_FLWS_LEMM", 892 ``!f g. empty_followers g f ==> extractTrans g f = {}``, 893 rpt strip_tac >> fs[empty_followers_def] 894 >> `!x. ~(x ��� extractTrans g f)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 895 >> simp[extractTrans_def] >> rpt strip_tac 896 >- (disj2_tac >> disj1_tac >> Q.HO_MATCH_ABBREV_TAC `A = {}` 897 >> `!x. ~(x ��� A)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 898 >> qunabbrev_tac `A` >> rpt strip_tac >> fs[OPTION_TO_LIST_MEM] 899 >> Cases_on `x'` >> fs[] >> first_x_assum (qspec_then `q` mp_tac) 900 >> rpt strip_tac 901 >> `l = []` by ( 902 first_x_assum (qspec_then `r` mp_tac) 903 >> simp[] 904 >> `lookup q (g.nodeInfo) = SOME r ��� (��(n,l). l.frml = f) (q,r)` 905 by metis_tac[findNode_def,FIND_LEMM2,MEM_toAList] 906 >> fs[] 907 ) 908 >> fs[] 909 ) 910 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] >> rpt strip_tac 911 >> Cases_on `MEM l l'` >> fs[] >> rpt strip_tac 912 >> Cases_on `findNode (��(n,l). l.frml = f) g ��� SOME x` >> fs[] 913 >> Cases_on `x` >> fs[] 914 >> `lookup q (g.nodeInfo) = SOME r ��� (��(n,l). l.frml = f) (q,r)` 915 by metis_tac[findNode_def,FIND_LEMM2,MEM_toAList] 916 >> fs[] 917 >> `r.true_labels = []` by ( 918 first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 919 >> first_x_assum (qspec_then `r` mp_tac) >> simp[] 920 >> fs[] 921 ) 922 >> rw[] >> Cases_on `l'` >> fs[] 923 ) 924 ); 925 926val flws_sorted_def = Define ` 927 flws_sorted g = 928 (!x_id fls. x_id ��� domain g.nodeInfo 929 ��� (lookup x_id g.followers = SOME fls) 930 ==> (SORTED (��f1 f2. (FST f2).edge_grp <= (FST f1).edge_grp) fls 931 ��� (!x y. (MEM x fls ��� MEM y fls ��� ((FST x).edge_grp = (FST y).edge_grp)) 932 ==> (FST x = FST y)) 933 ��� (!x. MEM x fls ==> (0 < (FST x).edge_grp))))`; 934 935val FLWS_SORTED_EMPTY = store_thm 936 ("FLWS_SORTED_EMPTY", 937 ``flws_sorted empty``, 938 fs[flws_sorted_def] >> rpt strip_tac >> fs[empty_def,domain_def,foldi_def] 939 ); 940 941val first_flw_has_max_counter_def = Define` 942 first_flw_has_max_counter g = 943 (!x_id fls fl. x_id ��� domain g.nodeInfo 944 ��� (lookup x_id g.followers = SOME (fl::fls)) 945 ==> (!y. MEM y fls 946 ==> ((FST y).edge_grp <= (FST fl).edge_grp)))`; 947 948val FLWS_SORTED_IMP_FFHMC = store_thm 949 ("FLWS_SORTED_IMP_FFHMC", 950 ``!g. flws_sorted g ==> first_flw_has_max_counter g``, 951 fs[flws_sorted_def,first_flw_has_max_counter_def] >> rpt strip_tac 952 >> first_x_assum (qspec_then `x_id` mp_tac) >> simp[] >> rpt strip_tac 953 >> qabbrev_tac `P = 954 (��(f1:�� edgeLabelAA # num) (f2:�� edgeLabelAA # num). 955 (FST f2).edge_grp ��� (FST f1).edge_grp)` 956 >> `transitive P` by (qunabbrev_tac `P` >> simp[transitive_def]) 957 >> `!y. MEM y fls ==> P fl y` by metis_tac[SORTED_EQ] 958 >> `P fl y` by metis_tac[] >> qunabbrev_tac `P` >> fs[] 959 ); 960 961val FIRST_FLW_EMPTY = store_thm 962 ("FIRST_FLW_EMPTY", 963 ``first_flw_has_max_counter empty``, 964 fs[first_flw_has_max_counter_def] >> rpt strip_tac 965 >> fs[empty_def,domain_def,foldi_def] 966 ); 967 968val FIRST_FLW_LEMM = store_thm 969 ("FIRST_FLW_LEMM", 970 ``!g g2. (g.followers = g2.followers) 971 ��� (domain g.nodeInfo = domain g2.nodeInfo) 972 ==> (first_flw_has_max_counter g 973 = first_flw_has_max_counter g2)``, 974 simp[first_flw_has_max_counter_def,EQ_IMP_THM] >> rpt strip_tac 975 >> metis_tac[] 976 ); 977 978val ADDFRML_WFG = store_thm 979 ("ADDFRML_WFG", 980 ``!g f. wfg g ==> wfg (addFrmlToGraph g f)``, 981 rpt strip_tac >> Cases_on `MEM f (graphStates g)` 982 >> Cases_on `f` >> fs[addFrmlToGraph_def,graphStates_def] 983 ); 984 985val ADDFRML_FLW_LEMM = store_thm 986 ("ADDFRML_FLW_LEMM", 987 ``!g f. wfg g 988 ��� flws_sorted g 989 ==> flws_sorted (addFrmlToGraph g f)``, 990 rpt strip_tac >> fs[flws_sorted_def] >> rpt strip_tac 991 >> `wfg (addFrmlToGraph g f)` by metis_tac[ADDFRML_WFG] 992 >> Cases_on `fls` >> fs[SORTED_NIL] 993 >> `lookup x_id g.followers = SOME (h::t) 994 ��� (x_id ��� domain g.nodeInfo)` by ( 995 Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo))` 996 >> Cases_on `f` >> fs[addFrmlToGraph_def] 997 >> Cases_on `x_id = g.next` 998 >> fs[addNode_def,lookup_insert] >> rw[] 999 ) 1000 >> rw[] >> first_x_assum (qspec_then `x_id` mp_tac) >> rpt strip_tac 1001 >> first_x_assum (qspec_then `(h::t)` mp_tac) >> simp[] 1002 ); 1003 1004val until_iff_final_def = Define` 1005 until_iff_final g = 1006 !id node. (lookup id g.nodeInfo = SOME node) 1007 ==> ((?f1 f2. node.frml = U f1 f2) = node.is_final)`; 1008 1009val ADDFRML_LEMM2 = store_thm 1010 ("ADDFRML_LEMM2", 1011 ``!g f. wfg g ==> 1012 (set (graphStates (addFrmlToGraph g f)) = set (graphStates g) ��� {f} 1013 ��� (!id. IS_SOME (lookup id g.nodeInfo) 1014 ==> ((lookup id g.nodeInfo 1015 = lookup id (addFrmlToGraph g f).nodeInfo) 1016 ��� (lookup id g.followers 1017 = lookup id (addFrmlToGraph g f).followers)) 1018 ) 1019 ��� (until_iff_final g ==> until_iff_final (addFrmlToGraph g f)))``, 1020 simp[SET_EQ_SUBSET] >> rpt strip_tac 1021 >- (simp[SUBSET_DEF,UNION_DEF] >> rpt strip_tac 1022 >> Cases_on `MEM x (graphStates g)` >> fs[] 1023 >> `!q b. MEM q 1024 (graphStates (addNode <|frml := f; is_final := b ; 1025 true_labels := []|> g)) 1026 ==> ((q = f) \/ MEM q (graphStates g))` by ( 1027 rpt strip_tac >> fs[graphStates_def,MEM_MAP] >> Cases_on `y'` 1028 >> fs[MEM_toAList] >> Cases_on `r.frml = f` >> fs[] 1029 >> qexists_tac `(q',r)` 1030 >> simp[] >> fs[MEM_toAList,addNode_def] 1031 >> fs[lookup_insert] >> Cases_on `q' = g.next` >> fs[] 1032 >> fs[theorem "nodeLabelAA_component_equality"] 1033 ) 1034 >> Cases_on `MEM f (graphStates g)` >> fs[] 1035 >> Cases_on `f` >> fs[addFrmlToGraph_def,inAuto_def] 1036 >> metis_tac[] 1037 ) 1038 >- (simp[SUBSET_DEF] >> rpt strip_tac >> Cases_on `MEM f (graphStates g)` 1039 >- (Cases_on `f` >> fs[addFrmlToGraph_def,graphStates_def]) 1040 >- (Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def,graphStates_def] 1041 >> `~(g.next ��� domain g.nodeInfo)` by ( 1042 fs[wfg_def] >> metis_tac[] 1043 ) 1044 >> fs[insert_def,MEM_MAP] >> qexists_tac `y` >> simp[] 1045 >> Cases_on `y` >> rw[MEM_toAList] 1046 >> Cases_on `q = g.next` >> fs[lookup_insert,MEM_toAList] 1047 >> (`lookup q g.nodeInfo = NONE` by metis_tac[lookup_NONE_domain] 1048 >> rw[] >> fs[MEM_toAList]) 1049 ) 1050 ) 1051 >- (`wfg (addFrmlToGraph g f)` by metis_tac[ADDFRML_WFG] 1052 >> metis_tac[ADDFRML_LEMM] 1053 ) 1054 >- (Cases_on `f` >> simp[addFrmlToGraph_def] >> rw[] 1055 >> `?node. lookup id g.nodeInfo = SOME node` by fs[IS_SOME_EXISTS] 1056 >> `id ��� domain g.nodeInfo` by fs[domain_lookup] 1057 >> simp[addNode_def,lookup_insert] >> fs[wfg_def] 1058 >> `~ (id = g.next)` by ( 1059 first_x_assum (qspec_then `id` mp_tac) >> simp[] 1060 ) 1061 >> fs[] 1062 ) 1063 >- (Cases_on `f` >> simp[addFrmlToGraph_def] >> rw[] 1064 >> `?node. lookup id g.nodeInfo = SOME node` by fs[IS_SOME_EXISTS] 1065 >> `id ��� domain g.nodeInfo` by fs[domain_lookup] 1066 >> simp[addNode_def,lookup_insert] >> fs[wfg_def] 1067 >> `~ (id = g.next)` by ( 1068 first_x_assum (qspec_then `id` mp_tac) >> simp[] 1069 ) 1070 >> fs[] 1071 ) 1072 >- (fs[until_iff_final_def] >> rpt strip_tac 1073 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo))` 1074 >- (Cases_on `f` 1075 >> fs[addFrmlToGraph_def] >> metis_tac[] 1076 ) 1077 >- (Cases_on `id = g.next` 1078 >- (Cases_on `f` 1079 >> fs[addFrmlToGraph_def,addNode_def,lookup_insert] 1080 >> Cases_on `node.frml` >> rw[] >> fs[] 1081 ) 1082 >- (Cases_on `f` 1083 >> fs[addFrmlToGraph_def,addNode_def,lookup_insert] 1084 >> metis_tac[] 1085 ) 1086 ) 1087 ) 1088 ); 1089 1090val ADDFRML_UNIQUENODE_LEMM = store_thm 1091 ("ADDFRML_UNIQUENODE_LEMM", 1092 ``!g g2 f. (wfg g ��� unique_node_formula g ��� (addFrmlToGraph g f = g2)) 1093 ==> (unique_node_formula g2)``, 1094 fs[unique_node_formula_def] >> rpt strip_tac 1095 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g.nodeInfo))` 1096 >- (Cases_on `f` >> fs[addFrmlToGraph_def] >> metis_tac[]) 1097 >- (`!i. i < g.next 1098 ==> (lookup i (addFrmlToGraph g f).nodeInfo 1099 = lookup i g.nodeInfo)` by ( 1100 rpt strip_tac >> fs[] 1101 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) 1102 (toAList g.nodeInfo))` 1103 >- (Cases_on `f` >> simp[addFrmlToGraph_def]) 1104 >- (Cases_on `f` >> simp[addFrmlToGraph_def,addNode_def] 1105 >> metis_tac[lookup_insert, 1106 DECIDE ``i < g.next ==> ~(i = g.next)``] 1107 ) 1108 ) 1109 >> `!i a. i < g.next 1110 ==> ((MEM (i,a) (graphStatesWithId (addFrmlToGraph g f))) 1111 = (MEM (i,a) (graphStatesWithId g)))` by ( 1112 rpt strip_tac >> simp[graphStatesWithId_def,MEM_MAP] 1113 >> simp[EQ_IMP_THM] >> rpt strip_tac 1114 >> qexists_tac `y` >> Cases_on `y` >> fs[] >> rw[] 1115 >> metis_tac[MEM_toAList] 1116 ) 1117 >> `wfg (addFrmlToGraph g f)` by metis_tac[ADDFRML_WFG] 1118 >> `(addFrmlToGraph g f).next = g.next + 1` by ( 1119 Cases_on `f` >> simp[addFrmlToGraph_def] 1120 >> simp[addNode_def] 1121 ) 1122 >> Cases_on `id = g.next` >> fs[] 1123 >- (fs[graphStatesWithId_def] 1124 >> `?r. MEM (g.next,r) (toAList (addFrmlToGraph g f).nodeInfo)` 1125 by (fs[MEM_MAP] >> Cases_on `y` >> fs[] >> metis_tac[]) 1126 >> `r.frml = f` by ( 1127 Cases_on `f` >> fs[addFrmlToGraph_def] 1128 >> fs[] >> POP_ASSUM mp_tac >> simp[addNode_def] 1129 >> simp[MEM_toAList,lookup_insert,SOME_11] 1130 >> fs[theorem "nodeLabelAA_component_equality"] 1131 ) 1132 >> fs[MEM_MAP] >> rw[] 1133 >> `h = r.frml` 1134 by (Cases_on `y` >> fs[] >> metis_tac[MEM_toAList,SOME_11]) 1135 >> rw[] 1136 >> Cases_on `oId < g.next` >> first_x_assum (qspec_then `oId` mp_tac) 1137 >> simp[] >> Cases_on `y'` >> fs[] >> rw[] 1138 >- (`~(lookup oId g.nodeInfo = SOME r')` 1139 suffices_by metis_tac[SOME_11,MEM_toAList] 1140 >> first_x_assum (qspec_then `(oId,r')` mp_tac) >> fs[] 1141 >> metis_tac[MEM_toAList] 1142 ) 1143 >- (Cases_on `g.next < oId` >> fs[] 1144 >> `~(oId ��� domain (addFrmlToGraph g r.frml).nodeInfo)` by ( 1145 `(g.next + 1) <= oId` by simp[] 1146 >> metis_tac[wfg_def] 1147 ) 1148 >> metis_tac[MEM_toAList,domain_lookup] 1149 ) 1150 ) 1151 >- (Cases_on `g.next < id` >> fs[] 1152 >- (`~(id ��� domain (addFrmlToGraph g f).nodeInfo)` by ( 1153 `(g.next + 1) <= id` by simp[] 1154 >> metis_tac[wfg_def] 1155 ) 1156 >> fs[MEM_MAP,graphStatesWithId_def] 1157 >> Cases_on `y` >> fs[] 1158 >> metis_tac[MEM_toAList,domain_lookup] 1159 ) 1160 >- (`id < g.next` by simp[] 1161 >> first_assum (qspec_then `id` mp_tac) >> rpt strip_tac 1162 >> first_x_assum (qspec_then `h` mp_tac) >> rpt strip_tac 1163 >> `MEM (id,h) (graphStatesWithId (addFrmlToGraph g f))` 1164 by metis_tac[] 1165 >> `~(h = f)` by ( 1166 fs[graphStatesWithId_def,MEM_MAP] 1167 >> `y' = (id,SND y')` 1168 by (Cases_on `y'` >> fs[]) 1169 >> Cases_on `y'` >> fs[] >> rw[] 1170 >> `~(r.frml = f)` by ( 1171 POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> simp[] 1172 >> rpt strip_tac >> Cases_on `y'` >> fs[] >> rw[] 1173 >> first_x_assum (qspec_then `(id,r')` mp_tac) >> simp[] 1174 ) 1175 >> Cases_on `y''` >> Cases_on `y'` >> fs[] 1176 ) 1177 >> `oId < g.next` by ( 1178 fs[graphStatesWithId_def,MEM_MAP] 1179 >> Cases_on `y` >> fs[] >> rw[] >> CCONTR_TAC 1180 >> Cases_on `oId = g.next` 1181 >- (`lookup oId (addFrmlToGraph g f).nodeInfo = SOME r` by ( 1182 metis_tac[MEM_toAList] 1183 ) 1184 >> `r.frml = f` by ( 1185 `~(MEM f (MAP ((��l. l.frml) ��� SND) 1186 (toAList g.nodeInfo)))` by fs[MEM_MAP] 1187 >> Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def] 1188 >> fs[gfg_component_equality] 1189 >> rw[] >> fs[lookup_insert,theorem "nodeLabelAA_component_equality"] 1190 ) 1191 >> rw[] >> fs[] 1192 ) 1193 >- (`~(oId ��� domain (addFrmlToGraph g f).nodeInfo)` by ( 1194 `(g.next + 1) <= oId` by simp[] 1195 >> metis_tac[wfg_def] 1196 ) 1197 >> fs[MEM_MAP,graphStatesWithId_def] 1198 >> metis_tac[MEM_toAList,domain_lookup] 1199 ) 1200 ) 1201 >> metis_tac[] 1202 ) 1203 ) 1204 ) 1205 ); 1206 1207val ADDFRML_EXTRTRANS_LEMM = store_thm 1208 ("ADDFRML_EXTRTRANS_LEMM", 1209 ``!g1 g2 f props. (wfg g1 1210 ��� addFrmlToGraph g1 f = g2 1211 ��� unique_node_formula g1) 1212 ==> !x. extractTrans g1 x = extractTrans g2 x``, 1213 rpt strip_tac 1214 >> `!id. (IS_SOME (lookup id g1.nodeInfo)) 1215 ==> (lookup id g2.followers = lookup id g1.followers)` by ( 1216 rpt strip_tac 1217 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo))` 1218 >> Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def] 1219 >> fs[gfg_component_equality] 1220 >> `~(id = g1.next)` by ( 1221 CCONTR_TAC >> fs[wfg_def,domain_lookup] 1222 >> `!v. ~(lookup g1.next g1.nodeInfo = SOME v)` by fs[] 1223 >> metis_tac[IS_SOME_EXISTS,NOT_SOME_NONE] 1224 ) 1225 >> metis_tac[lookup_insert] 1226 ) 1227 >> `!q g. ~(MEM q (graphStates g)) ==> (extractTrans g q = {})` by ( 1228 rpt strip_tac 1229 >> `findNode (��(n,l). l.frml = q) g = NONE` by ( 1230 CCONTR_TAC 1231 >> Cases_on `findNode (��(n,l). l.frml = q) g` >> fs[] 1232 >> fs[findNode_def,graphStates_def] >> Cases_on `x` >> fs[MEM_MAP] 1233 >> `(��(n,l). l.frml = q) (q',r) ��� MEM (q',r) (toAList g.nodeInfo)` 1234 by metis_tac[FIND_LEMM2] 1235 >> fs[] >> first_x_assum (qspec_then `(q',r)` mp_tac) >> simp[] 1236 ) 1237 >> simp[extractTrans_def] >> rpt strip_tac 1238 >- (Q.HO_MATCH_ABBREV_TAC ` 1239 {edge | ?label. A label ��� ~(B label = {}) ��� edge = (C label)} = {}` 1240 >> `!l. B l = {}` suffices_by ( 1241 rpt strip_tac >> CCONTR_TAC 1242 >> `?a. a ��� {edge | ���label. A label 1243 ��� B label ��� ��� ��� edge = C label}` 1244 by metis_tac[MEMBER_NOT_EMPTY] 1245 >> fs[] >> metis_tac[] 1246 ) 1247 >> `!l x. ~(x ��� B l)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 1248 >> qunabbrev_tac `B` >> rpt strip_tac >> fs[OPTION_TO_LIST_MEM] 1249 ) 1250 >- fs[OPTION_TO_LIST_MEM] 1251 ) 1252 >> Cases_on `MEM x (graphStates g2)` >> fs[] 1253 >- (Cases_on `x = f` 1254 >- (rw[] 1255 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo))` 1256 >- (Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def]) 1257 >- (fs[graphStates_def] >> fs[MEM_MAP] >> Cases_on `y` >> fs[] 1258 >> `q = g1.next` by ( 1259 CCONTR_TAC 1260 >> `~(MEM f (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo)))` 1261 by (fs[MEM_MAP] >> metis_tac[]) 1262 >> `q ��� domain (addFrmlToGraph g1 f).nodeInfo` by ( 1263 metis_tac[MEM_toAList,domain_lookup] 1264 ) 1265 >> `q <= g1.next` by ( 1266 `wfg (addFrmlToGraph g1 f)` by metis_tac[ADDFRML_WFG] 1267 >> POP_ASSUM mp_tac >> simp[wfg_def] 1268 >> rpt strip_tac 1269 >> `(addFrmlToGraph g1 r.frml).next = g1.next +1` 1270 suffices_by ( 1271 strip_tac >> rw[] >> CCONTR_TAC >> fs[] 1272 ) 1273 >> rw[] 1274 >> Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def] 1275 >> fs[gfg_component_equality] 1276 ) 1277 >> `MEM (q,r) (toAList g1.nodeInfo)` by ( 1278 rw[] >> Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def] 1279 >> fs[gfg_component_equality] 1280 >> metis_tac[MEM_toAList,lookup_insert] 1281 ) 1282 >> first_x_assum (qspec_then `(q,r)` mp_tac) >> simp[] 1283 ) 1284 >> `lookup q (addFrmlToGraph g1 f).followers = SOME []` by ( 1285 `~(MEM f (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo)))` 1286 by (fs[MEM_MAP] >> metis_tac[]) 1287 >> rw[] 1288 >> Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def] 1289 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 1290 ) 1291 >> `!x. ~(x ��� extractTrans (addFrmlToGraph g1 r.frml) r.frml)` 1292 suffices_by metis_tac[MEMBER_NOT_EMPTY] 1293 >> simp[extractTrans_def] >> rpt strip_tac 1294 >- (disj2_tac >> disj1_tac >> Q.HO_MATCH_ABBREV_TAC `A = {}` 1295 >> `!x. ~(x ��� A)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 1296 >> qunabbrev_tac `A` >> rpt strip_tac >> fs[OPTION_TO_LIST_MEM] 1297 >> Cases_on `x'` >> fs[] >> rw[] 1298 >> `q' = g1.next` suffices_by ( 1299 strip_tac >> rw[] >> fs[] >> rw[] >> fs[] 1300 ) 1301 >> `(��(n,l). l.frml = r.frml) (q',r') 1302 ��� MEM (q',r') (toAList (addFrmlToGraph g1 r.frml).nodeInfo)` 1303 by metis_tac[FIND_LEMM2,findNode_def] 1304 >> fs[] 1305 >> CCONTR_TAC >> rw[] 1306 >> `~(MEM r.frml (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo)))` 1307 by (fs[MEM_MAP] >> metis_tac[]) 1308 >> fs[MEM_toAList] 1309 >> `lookup q' g1.nodeInfo = SOME r'` by ( 1310 Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def] 1311 >> fs[gfg_component_equality,lookup_insert,MEM_toAList] 1312 ) 1313 >> first_x_assum (qspec_then `(q',r')` mp_tac) >> simp[] 1314 >> metis_tac[MEM_toAList] 1315 ) 1316 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] >> rpt strip_tac 1317 >> Q.HO_MATCH_ABBREV_TAC `A \/ B` 1318 >> `~B ==> A` suffices_by metis_tac[] >> qunabbrev_tac `A` 1319 >> qunabbrev_tac `B` 1320 >> rpt strip_tac >> Q.HO_MATCH_ABBREV_TAC `A \/ B` 1321 >> `~A ==> B` suffices_by metis_tac[] >> rpt strip_tac 1322 >> qunabbrev_tac `A` >> qunabbrev_tac `B` >> fs[findNode_def] 1323 >> `(��(n,l). l.frml = r.frml) x 1324 ��� MEM x (toAList (addFrmlToGraph g1 r.frml).nodeInfo)` 1325 by metis_tac[FIND_LEMM2] 1326 >> `?id node. x = (id,node)` by (Cases_on `x` >> fs[]) 1327 >> rw[] 1328 >> `node.true_labels = []` suffices_by (Cases_on `l'` >>fs[]) 1329 >> `id = g1.next` by ( 1330 CCONTR_TAC >> rw[] 1331 >> `~(MEM r.frml (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo)))` 1332 by (fs[MEM_MAP] >> metis_tac[]) 1333 >> fs[MEM_toAList] 1334 >> `lookup id g1.nodeInfo = SOME node` by ( 1335 Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def] 1336 >> fs[gfg_component_equality,lookup_insert,MEM_toAList] 1337 ) 1338 >> first_x_assum (qspec_then `(id,node)` mp_tac) >> simp[] 1339 >> metis_tac[MEM_toAList] 1340 ) 1341 >> rw[] >> fs[MEM_toAList] >> rw[] 1342 >> `~(MEM node.frml (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo)))` 1343 by (fs[MEM_MAP] >> metis_tac[]) 1344 >> Cases_on `node.frml` >> fs[addFrmlToGraph_def,addNode_def] 1345 >> fs[gfg_component_equality,lookup_insert,MEM_toAList, 1346 theorem "nodeLabelAA_component_equality"] 1347 ) 1348 ) 1349 ) 1350 >- (`set (graphStates (addFrmlToGraph g1 f)) 1351 = set (graphStates g1) ��� {f}` by metis_tac[ADDFRML_LEMM2] 1352 >> rw[] >> `MEM x (graphStates g1)` by (CCONTR_TAC >> fs[]) 1353 >> POP_ASSUM mp_tac 1354 >> simp[graphStates_def,MEM_MAP] >> rpt strip_tac 1355 >> `���id. 1356 IS_SOME (lookup id g1.nodeInfo) ��� 1357 lookup id g1.nodeInfo = lookup id (addFrmlToGraph g1 f).nodeInfo` 1358 by metis_tac[ADDFRML_LEMM2] 1359 >> Cases_on `y` >> fs[MEM_toAList] 1360 >> first_assum (qspec_then `q` mp_tac) >> simp[] >> rpt strip_tac 1361 >> `lookup q (addFrmlToGraph g1 f).followers = 1362 lookup q g1.followers` by metis_tac[IS_SOME_DEF] 1363 >> Cases_on `MEM f (MAP ((��l. l.frml) ��� SND) (toAList g1.nodeInfo))` 1364 >- (rw[] 1365 >> Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def] 1366 >> fs[gfg_component_equality]) 1367 >- (`findNode (��(n,l). l.frml = r.frml) g1 = SOME (q,r) ` by ( 1368 simp[findNode_def] >> `(��(n,l). l.frml = r.frml) (q,r)` by fs[] 1369 >> `?x1. findNode (��(n,l). l.frml = r.frml) g1 = SOME x1 1370 ��� (��(n,l). l.frml = r.frml) x1 1371 ��� (MEM x1 (toAList g1.nodeInfo))` 1372 by metis_tac[FIND_LEMM,findNode_def,MEM_toAList,FIND_LEMM2] 1373 >> Cases_on `x1` 1374 >> `MEM (q',r'.frml) (graphStatesWithId g1)` 1375 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 1376 >> `MEM (q,r.frml) (graphStatesWithId g1)` 1377 by metis_tac[GRAPH_STATES_WITH_ID_LEMM,MEM_toAList] 1378 >> fs[unique_node_formula_def] >> rw[] 1379 >> `q' = q` by metis_tac[] >> rw[] 1380 >> `r' = r` by metis_tac[MEM_toAList,SOME_11] >> rw[] 1381 >> fs[findNode_def] 1382 ) 1383 >> `findNode (��(n,l). l.frml = r.frml) (addFrmlToGraph g1 f) 1384 = SOME (q,r)` by ( 1385 `unique_node_formula (addFrmlToGraph g1 f)` 1386 by metis_tac[ADDFRML_UNIQUENODE_LEMM] 1387 >> simp[findNode_def] >> `(��(n,l). l.frml = r.frml) (q,r)` by fs[] 1388 >> `?x1. findNode (��(n,l). l.frml = r.frml) (addFrmlToGraph g1 f) 1389 = SOME x1 1390 ��� (��(n,l). l.frml = r.frml) x1 1391 ��� (MEM x1 (toAList (addFrmlToGraph g1 f).nodeInfo))` 1392 by metis_tac[FIND_LEMM,findNode_def,MEM_toAList,FIND_LEMM2] 1393 >> Cases_on `x1` 1394 >> `MEM (q',r'.frml) (graphStatesWithId (addFrmlToGraph g1 f))` 1395 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 1396 >> `MEM (q,r.frml) (graphStatesWithId (addFrmlToGraph g1 f))` 1397 by metis_tac[GRAPH_STATES_WITH_ID_LEMM,MEM_toAList] 1398 >> fs[unique_node_formula_def] >> rw[] 1399 >> `q' = q` by metis_tac[] >> rw[] 1400 >> `r' = r` by metis_tac[MEM_toAList,SOME_11] >> rw[] 1401 >> fs[findNode_def] 1402 ) 1403 >> rw[] 1404 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1405 >> (POP_ASSUM mp_tac >> simp[extractTrans_def] >> rpt strip_tac 1406 >- (disj1_tac >> qexists_tac `label` >> fs[] 1407 >> Q.HO_MATCH_ABBREV_TAC `~(A = {}) ��� B = A` 1408 >> `A = B` suffices_by metis_tac[] 1409 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1410 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 1411 >> fs[OPTION_TO_LIST_MEM] >> rw[] 1412 >> `sucId ��� domain g1.nodeInfo` 1413 by metis_tac[MEM_toAList,wfg_def,wfAdjacency_def] 1414 >> fs[domain_lookup] 1415 >> first_x_assum (qspec_then `sucId` mp_tac) >> simp[] 1416 >> metis_tac[] 1417 ) 1418 >- metis_tac[]) 1419 ) 1420 ) 1421 ) 1422 >- (`set (graphStates (addFrmlToGraph g1 f)) = set (graphStates g1) ��� {f}` 1423 by metis_tac[ADDFRML_LEMM2] 1424 >> rw[] 1425 >> `~(MEM x (graphStates g1))` by ( 1426 CCONTR_TAC >> fs[] 1427 ) 1428 >> metis_tac[] 1429 ) 1430 ); 1431 1432val ADDFRML_FOLDR_LEMM = store_thm 1433 ("ADDFRML_FOLDR_LEMM", 1434 ``!g fs. wfg g ==> 1435 (set (graphStates g) ��� set fs = 1436 set (graphStates (FOLDR (\f g. addFrmlToGraph g f) g fs)) 1437 ��� wfg (FOLDR (\f g. addFrmlToGraph g f) g fs) 1438 ��� (!id. IS_SOME (lookup id g.nodeInfo) 1439 ==> ((lookup id g.nodeInfo 1440 = lookup id 1441 (FOLDR (\f g. addFrmlToGraph g f) g fs).nodeInfo) 1442 ��� (lookup id g.followers 1443 = lookup id 1444 (FOLDR (\f g. addFrmlToGraph g f) g fs).followers)) 1445 ) 1446 ��� (until_iff_final g 1447 ==> until_iff_final (FOLDR (\f g. addFrmlToGraph g f) g fs)) 1448 ��� (unique_node_formula g 1449 ==> unique_node_formula 1450 (FOLDR (\f g. addFrmlToGraph g f) g fs)) 1451 ��� (flws_sorted g 1452 ==> flws_sorted 1453 (FOLDR (\f g. addFrmlToGraph g f) g fs)) 1454 ��� (wfg g ��� unique_node_formula g ==> 1455 (!x. extractTrans g x = 1456 extractTrans (FOLDR (\f g. addFrmlToGraph g f) g fs) x)) 1457 )``, 1458 gen_tac >> Induct_on `fs` >> rpt strip_tac 1459 >> fs[FOLDR] 1460 >- (`set (graphStates 1461 (addFrmlToGraph (FOLDR (��f g. addFrmlToGraph g f) g fs) h)) 1462 = set (graphStates ((FOLDR (��f g. addFrmlToGraph g f) g fs))) ��� {h}` 1463 by metis_tac[ADDFRML_LEMM2] 1464 >> `set (graphStates g) ��� (h INSERT (set fs)) 1465 = set (graphStates g) ��� set fs ��� {h}` suffices_by metis_tac[] 1466 >> fs[INSERT_DEF,UNION_DEF] >> simp[SET_EQ_SUBSET,SUBSET_DEF] 1467 >> rpt strip_tac >> metis_tac[] 1468 ) 1469 >- metis_tac[ADDFRML_WFG] 1470 >- metis_tac[ADDFRML_LEMM2] 1471 >- metis_tac[ADDFRML_LEMM2] 1472 >- metis_tac[ADDFRML_LEMM2] 1473 >- metis_tac[ADDFRML_UNIQUENODE_LEMM] 1474 >- metis_tac[ADDFRML_FLW_LEMM] 1475 >- metis_tac[ADDFRML_EXTRTRANS_LEMM] 1476 ); 1477 1478val ADDFRML_EMPTYFLW_LEMM = store_thm 1479 ("ADDFRML_EMPTYFLW_LEMM", 1480 ``!(g:(�� nodeLabelAA, �� edgeLabelAA) gfg) fs f. 1481 wfg g ��� MEM f fs 1482 ��� (~MEM f (graphStates g) \/ empty_followers g f) 1483 ==> empty_followers (FOLDR (\f g. addFrmlToGraph g f) g fs) f``, 1484 `!(g:(�� nodeLabelAA, �� edgeLabelAA) gfg) fs f. 1485 wfg g ��� MEM f fs 1486 ��� (~MEM f (graphStates g) 1487 \/ (empty_followers g f ��� MEM f (graphStates g))) 1488 ==> empty_followers (FOLDR (\f g. addFrmlToGraph g f) g fs) f` 1489 suffices_by metis_tac[] 1490 >> gen_tac >> Induct_on `fs` >> fs[] >> strip_tac >> strip_tac 1491 >> `!q f. wfg g ==> 1492 ((MEM q fs \/ MEM q (graphStates g)) ==> 1493 addFrmlToGraph (FOLDR (��f g. addFrmlToGraph g f) g fs) q = 1494 FOLDR (��f g. addFrmlToGraph g f) g fs)` by ( 1495 rpt strip_tac 1496 >> `MEM q (graphStates (FOLDR (��f g. addFrmlToGraph g f) g fs))` by ( 1497 `(set (graphStates g)) ��� (set fs) = 1498 set (graphStates (FOLDR (��f g. addFrmlToGraph g f) g fs))` 1499 by metis_tac[ADDFRML_FOLDR_LEMM] 1500 >> fs[SET_EQ_SUBSET,SUBSET_DEF] >> metis_tac[] 1501 ) 1502 >> `MEM q (MAP ((��l. l.frml) ��� SND) 1503 (toAList ((FOLDR (��f g. addFrmlToGraph g f) g fs)).nodeInfo))` by ( 1504 fs[MEM_MAP,graphStates_def] >> metis_tac[] 1505 ) 1506 >> Cases_on `q` >> simp[addFrmlToGraph_def] >> rw[] 1507 ) 1508 >> `!ks q i n. 1509 (~MEM q ks) 1510 ��� (lookup i (FOLDR (��f g. addFrmlToGraph g f) g ks).nodeInfo 1511 = SOME n ��� (n.frml = q)) 1512 ==> (lookup i g.nodeInfo = SOME n) 1513 ��� (lookup i g.followers = 1514 lookup i (FOLDR (��f g. addFrmlToGraph g f) g ks).followers)` 1515 by ( 1516 Induct_on `ks` >> fs[] >> rpt gen_tac >> strip_tac 1517 >> qabbrev_tac `G_K = (FOLDR (��f g. addFrmlToGraph g f) g ks)` 1518 >> Cases_on 1519 `MEM h (MAP ((��l. l.frml) ��� SND) 1520 (toAList G_K.nodeInfo))` 1521 >- (Cases_on `h` >> fs[addFrmlToGraph_def]) 1522 >- (`~(i = G_K.next)` by ( 1523 CCONTR_TAC >> Cases_on `h` 1524 >> fs[addFrmlToGraph_def,addNode_def,gfg_component_equality] 1525 >> rw[] 1526 >> fs[theorem "nodeLabelAA_component_equality"] >> metis_tac[lookup_insert] 1527 ) 1528 >> Cases_on `h` 1529 >> fs[addFrmlToGraph_def,addNode_def,gfg_component_equality] 1530 >> rw[] >> fs[theorem "nodeLabelAA_component_equality"] 1531 >> metis_tac[lookup_insert] 1532 ) 1533 ) 1534 >> Cases_on `h=f` >> fs[] 1535 >- (rw[] >> Cases_on `MEM f fs` 1536 >- metis_tac[] 1537 >- (simp[empty_followers_def] >> rpt strip_tac 1538 >> qabbrev_tac `G0 = FOLDR (��f g. addFrmlToGraph g f) g fs` 1539 >> `(set (graphStates g)) ��� (set fs) = 1540 set (graphStates (G0))` 1541 by metis_tac[ADDFRML_FOLDR_LEMM] 1542 >> `~(MEM f (MAP ((��l. l.frml) ��� SND) (toAList G0.nodeInfo)))` 1543 by (fs[MEM_MAP] >> rpt strip_tac 1544 >> Cases_on `f = (SND y).frml` >> fs[] 1545 >> `~(MEM f (graphStates G0))` by ( 1546 fs[UNION_DEF,SET_EQ_SUBSET,SUBSET_DEF] 1547 >> metis_tac[] 1548 ) 1549 >> POP_ASSUM mp_tac >> simp[graphStates_def,MEM_MAP] 1550 >> rpt strip_tac >> metis_tac[] 1551 ) 1552 >> `id = G0.next` by ( 1553 CCONTR_TAC 1554 >> `lookup id G0.nodeInfo = SOME node` by ( 1555 Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def] 1556 >> fs[gfg_component_equality] 1557 >> metis_tac[MEM_toAList,lookup_insert] 1558 ) 1559 >> `MEM node.frml (graphStates G0)` by ( 1560 PURE_REWRITE_TAC[MEM_MAP,graphStates_def] 1561 >> `MEM (id,node) (toAList G0.nodeInfo)` 1562 by metis_tac[MEM_toAList] 1563 >> qexists_tac `(id,node)` >> fs[] 1564 ) 1565 >> fs[UNION_DEF,SET_EQ_SUBSET,SUBSET_DEF] >> metis_tac[] 1566 ) 1567 >> Cases_on `f` >> fs[addFrmlToGraph_def,addNode_def] 1568 >> fs[gfg_component_equality] 1569 >> fs[theorem "nodeLabelAA_component_equality"] 1570 ) 1571 >- metis_tac[] 1572 >- (fs[empty_followers_def] >> rpt gen_tac >> strip_tac 1573 >> qabbrev_tac `G0 = FOLDR (��f g. addFrmlToGraph g f) g fs` 1574 >> `(set (graphStates g)) ��� (set fs) = 1575 set (graphStates (G0))` 1576 by metis_tac[ADDFRML_FOLDR_LEMM] 1577 >> metis_tac[] 1578 ) 1579 ) 1580 >- (Cases_on `MEM h fs` 1581 >- metis_tac[] 1582 >- (Cases_on `MEM h (graphStates g)` 1583 >- metis_tac[] 1584 >- (Cases_on `MEM f (graphStates g)` 1585 >> (simp[empty_followers_def] >> rpt strip_tac 1586 >> qabbrev_tac `G0 = FOLDR (��f g. addFrmlToGraph g f) g fs` 1587 >> `(set (graphStates g)) ��� (set fs) = 1588 set (graphStates (G0))` 1589 by metis_tac[ADDFRML_FOLDR_LEMM] 1590 >> `~(MEM h (MAP ((��l. l.frml) ��� SND) (toAList G0.nodeInfo)))` 1591 by (fs[MEM_MAP] >> rpt strip_tac 1592 >> Cases_on `h = (SND y).frml` >> fs[] 1593 >> `~(MEM h (graphStates G0))` by ( 1594 fs[UNION_DEF,SET_EQ_SUBSET,SUBSET_DEF] 1595 >> metis_tac[] 1596 ) 1597 >> POP_ASSUM mp_tac >> simp[graphStates_def,MEM_MAP] 1598 >> rpt strip_tac >> metis_tac[] 1599 ) 1600 >> Cases_on `id = G0.next` 1601 >- (`node.frml = h` by ( 1602 Cases_on `h` >> fs[addFrmlToGraph_def,addNode_def] 1603 >> fs[gfg_component_equality] >> rw[] 1604 >> fs[theorem "nodeLabelAA_component_equality"] 1605 ) 1606 >> rw[] >> metis_tac[] 1607 ) 1608 >- (`empty_followers G0 f` by metis_tac[empty_followers_def] 1609 >> `lookup id G0.followers = 1610 lookup id (addFrmlToGraph G0 h).followers` by ( 1611 Cases_on `h` >> fs[addFrmlToGraph_def,addNode_def] 1612 >> fs[gfg_component_equality] >> rw[] 1613 >> metis_tac[lookup_insert] 1614 ) 1615 >> fs[empty_followers_def] 1616 >> first_x_assum (qspec_then `id` mp_tac) >> rpt strip_tac 1617 >> `lookup id G0.nodeInfo = SOME node` by ( 1618 Cases_on `h` >> fs[addFrmlToGraph_def,addNode_def] 1619 >> fs[gfg_component_equality] >> rw[] 1620 >> metis_tac[lookup_insert] 1621 ) 1622 >> first_x_assum (qspec_then `node` mp_tac) >> simp[] 1623 ) 1624 >- (Cases_on `h` >> fs[addFrmlToGraph_def,addNode_def] 1625 >> fs[gfg_component_equality] >> rw[]) 1626 >- (`lookup id G0.nodeInfo = SOME node` by ( 1627 Cases_on `h` >> fs[addFrmlToGraph_def,addNode_def] 1628 >> fs[gfg_component_equality] >> rw[] 1629 >> metis_tac[lookup_insert] 1630 ) 1631 >> `empty_followers G0 f` by metis_tac[empty_followers_def] 1632 >> POP_ASSUM mp_tac >> PURE_REWRITE_TAC[empty_followers_def] 1633 >> rpt strip_tac >> metis_tac[] 1634 ) 1635 ) 1636 ) 1637 ) 1638 ) 1639 ); 1640 1641val ADD_0EDGE_LEMM = store_thm 1642 ("ADD_0EDGE_LEMM", 1643 ``!g g2 nId lab edge. 1644 let NEW_LAB = 1645 nodeLabelAA lab.frml lab.is_final (edge::lab.true_labels) 1646 in 1647 (lookup nId g.nodeInfo = SOME lab) 1648 ��� unique_node_formula g 1649 ��� (updateNode nId NEW_LAB g = SOME g2) 1650 ==> unique_node_formula g2``, 1651 fs[unique_node_formula_def,updateNode_def,graphStatesWithId_def] 1652 >> rpt strip_tac >> fs[MEM_MAP] 1653 >> first_x_assum (qspec_then `id` mp_tac) >> rpt strip_tac 1654 >> qabbrev_tac `nodeInfo2 = 1655 insert nId 1656 (nodeLabelAA lab.frml lab.is_final 1657 (edge::lab.true_labels)) g.nodeInfo` 1658 >> Cases_on `y` >> Cases_on `y'` >> fs[] >> rw[] 1659 >> first_x_assum (qspec_then `r.frml` mp_tac) >> simp[] >> rpt strip_tac 1660 >> `(lookup id nodeInfo2 = SOME r) ��� (lookup oId nodeInfo2 = SOME r')` 1661 by metis_tac[MEM_toAList] 1662 >> `?z1. (lookup id g.nodeInfo = SOME z1) ��� (z1.frml = r.frml)` by ( 1663 qunabbrev_tac `nodeInfo2` >> Cases_on `id = nId` 1664 >> fs[lookup_insert] >> Cases_on `r` >> fs[] 1665 ) 1666 >> `?z2. (lookup oId g.nodeInfo = SOME z2) ��� (z2.frml = r.frml)` by ( 1667 qunabbrev_tac `nodeInfo2` >> Cases_on `oId = nId` 1668 >> fs[lookup_insert] >> Cases_on `r'` >> fs[] 1669 ) 1670 >> `���y. 1671 (id,r.frml) = (��(id,label). (id,label.frml)) y 1672 ��� MEM y (toAList g.nodeInfo)` by ( 1673 qexists_tac `(id,z1)` >> fs[MEM_toAList] 1674 ) 1675 >> `���oId'. 1676 (���y. 1677 (oId',r.frml) = (��(id,label). (id,label.frml)) y 1678 ��� MEM y (toAList g.nodeInfo)) ��� (id = oId')` by metis_tac[] 1679 >> first_x_assum (qspec_then `oId` mp_tac) >> simp[] 1680 >> `���y. 1681 (oId,r.frml) = (��(id,label). (id,label.frml)) y 1682 ��� MEM y (toAList g.nodeInfo)` by ( 1683 qexists_tac `(oId,z2)` >> fs[MEM_toAList] 1684 ) >> metis_tac[] 1685 ); 1686 1687Theorem ADDEDGE_COUNTER_LEMM: 1688 ���g e f g2. 1689 addEdgeToGraph f e g = SOME g2 ��� flws_sorted g ��� wfg g ==> 1690 flws_sorted g2 1691Proof 1692 rpt strip_tac >> Cases_on `e` 1693 >> fs[addEdgeToGraph_def] 1694 >> Cases_on `l1 = []` >> rpt strip_tac >> fs[] 1695 >- (fs[flws_sorted_def] >> rpt strip_tac 1696 >- (Cases_on `x` >> fs[] 1697 >> metis_tac[updateNode_preserves_domain, updateNode_preserves_edges] 1698 ) 1699 >- (rename[`findNode _ g = SOME node`] 1700 >> rw[] >> `?nId nL. node = (nId,nL)` by (Cases_on `node` >> fs[]) 1701 >> rw[] >> fs[] 1702 >> `(lookup x_id g.followers = SOME fls) 1703 ��� (x_id ��� domain g.nodeInfo)` 1704 by metis_tac[updateNode_preserves_edges,updateNode_preserves_domain] 1705 >> metis_tac[] 1706 ) 1707 >- (Cases_on `x` >> fs[] 1708 >> metis_tac[updateNode_preserves_domain, updateNode_preserves_edges] 1709 ) 1710 ) 1711 >- ( 1712 Cases_on `x` >> fs[] 1713 >> qabbrev_tac `LABEL = 1714 <|edge_grp := 1715 (if oldSucPairs = [] then 1n 1716 else (HD (MAP FST oldSucPairs)).edge_grp) + 1; 1717 pos_lab := l; neg_lab := l0|>` 1718 >> qabbrev_tac `addSingleEdge = 1719 (��e:(�� edgeLabelAA # num) 1720 g_opt:((�� nodeLabelAA, �� edgeLabelAA) gfg) option. 1721 do g_int <- g_opt; 1722 newGraph <- addEdge q e g_int; 1723 SOME newGraph 1724 od)` 1725 >> qabbrev_tac `TO_LABELS = ��l. 1726 (MAP (��i. (LABEL,i)) 1727 (MAP FST 1728 (CAT_OPTIONS 1729 (MAP (��s. findNode (��(n,l). l.frml = s) g) l))))` 1730 >> `!ls. ?m. (FOLDR addSingleEdge (SOME g) (TO_LABELS ls) = SOME m) 1731 ��� (flws_sorted m) 1732 ��� (!fl fls. lookup q m.followers = SOME (fl::fls) 1733 ==> ((FST fl).edge_grp <= LABEL.edge_grp 1734 ��� (!x. MEM x (fl::fls) 1735 ��� ((FST x).edge_grp = LABEL.edge_grp) 1736 ==> (FST x = LABEL))) 1737 ) 1738 ��� (!id. ~(id = q) 1739 ==> (lookup id m.followers = lookup id g.followers)) 1740 ��� (g.nodeInfo = m.nodeInfo) 1741 ��� wfg m` by ( 1742 fs[flws_sorted_def] >> Induct_on `ls` 1743 >- (`TO_LABELS [] = []` by ( 1744 qunabbrev_tac `TO_LABELS` >> fs[CAT_OPTIONS_def] 1745 ) 1746 >> fs[] >> strip_tac 1747 >- metis_tac[flws_sorted_def] 1748 >- (Cases_on `oldSucPairs` >> fs[] >> qunabbrev_tac `LABEL` 1749 >> fs[] >> rpt strip_tac >> rw[] >> fs[] 1750 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 1751 >> first_x_assum (qspec_then `(h::t)` mp_tac) >> simp[] 1752 >> `q ��� domain g.nodeInfo` 1753 by (fs[wfg_def] >> metis_tac[domain_lookup]) 1754 >> simp[] >> rpt strip_tac 1755 >> qabbrev_tac `P = 1756 (��f1:(�� edgeLabelAA # num) 1757 f2:(�� edgeLabelAA # num). 1758 (FST f2).edge_grp ��� (FST f1).edge_grp)` 1759 >> `transitive P` 1760 by (qunabbrev_tac `P` >> simp[transitive_def]) 1761 >> `���y. MEM y t ��� P h y` by metis_tac[SORTED_EQ] 1762 >> `P h x` by fs[] >> qunabbrev_tac `P` >> fs[] 1763 ) 1764 ) 1765 >- (fs[flws_sorted_def] >> gen_tac 1766 >> Cases_on `findNode (��(n,l). l.frml = h) g` 1767 >- (fs[] 1768 >> `TO_LABELS (h::ls) = TO_LABELS ls` by ( 1769 qunabbrev_tac `TO_LABELS` >> fs[CAT_OPTIONS_def] 1770 ) 1771 >> qexists_tac `m` >> fs[] >> metis_tac[] 1772 ) 1773 >- (Cases_on `x` 1774 >> `TO_LABELS (h::ls) = (LABEL,q')::(TO_LABELS ls)` by ( 1775 qunabbrev_tac `TO_LABELS` >> fs[CAT_OPTIONS_def] 1776 ) 1777 >> rw[] 1778 >> `?k. addSingleEdge (LABEL,q') (SOME m) = SOME k 1779 ��� (k.nodeInfo = m.nodeInfo) 1780 ��� wfg k` by ( 1781 qunabbrev_tac `addSingleEdge` >> fs[] 1782 >> `���k. addEdge q (LABEL,q') m = SOME k` 1783 suffices_by metis_tac[addEdge_preserves_nodeInfo, 1784 addEdge_preserves_wfg] 1785 >> simp[addEdge_def] 1786 >> `q ��� domain g.nodeInfo ��� q' ��� domain g.nodeInfo` by ( 1787 fs[findNode_def] 1788 >> `MEM (q,r) (toAList g.nodeInfo) 1789 ��� MEM (q',r') (toAList g.nodeInfo)` 1790 by metis_tac[FIND_LEMM2] 1791 >> metis_tac[MEM_toAList,domain_lookup] 1792 ) 1793 >> Q.HO_MATCH_ABBREV_TAC `?k. A ��� ?j. B j k` 1794 >> `A ��� ?j k. B j k` suffices_by metis_tac[] 1795 >> qunabbrev_tac `A` >> qunabbrev_tac `B` >> fs[] 1796 >> `���j. lookup q m.followers = SOME j` by ( 1797 fs[wfg_def] >> metis_tac[domain_lookup] 1798 ) 1799 >> metis_tac[wfg_def, domain_lookup] 1800 ) 1801 >> qexists_tac `k` >> fs[] 1802 >> qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 1803 >> fs[gfg_component_equality,flws_sorted_def] 1804 >> rpt strip_tac >> rw[] 1805 >> Cases_on `x_id = q` >> rw[] 1806 >- (Q.HO_MATCH_ABBREV_TAC `SORTED P fls` 1807 >> `transitive P` 1808 by (qunabbrev_tac `P` >> simp[transitive_def]) 1809 >> `fls = (LABEL,q')::followers_old` 1810 by metis_tac[lookup_insert,SOME_11] 1811 >> rw[] >> fs[] >> rw[] 1812 >> `SORTED 1813 P 1814 followers_old` by metis_tac[] 1815 >> qunabbrev_tac `P` >> Cases_on `followers_old` >> fs[] 1816 >> simp[SORTED_DEF] >> qunabbrev_tac `P` >> fs[] 1817 ) 1818 >- (`lookup x_id m.followers = SOME fls` 1819 by metis_tac[lookup_insert] 1820 >> `x_id ��� domain m.nodeInfo` 1821 by metis_tac[domain_lookup,wfg_def] 1822 >> metis_tac[] 1823 ) 1824 >- (rw[] 1825 >> `fls = (LABEL,q')::followers_old` 1826 by metis_tac[lookup_insert,SOME_11] 1827 >> rw[] >> fs[] 1828 >- (`(FST x).edge_grp = LABEL.edge_grp` 1829 by (Cases_on `x` >> fs[]) 1830 >> rw[] >> Cases_on `y` >> fs[] 1831 >> Cases_on `followers_old` >> fs[] 1832 >- (first_x_assum (qspec_then `h'` mp_tac) >> simp[] 1833 >> Cases_on `h'` >> fs[]) 1834 >- (first_x_assum (qspec_then `(q'',r'')` mp_tac) 1835 >> simp[]) 1836 ) 1837 >- (`(FST x).edge_grp = LABEL.edge_grp` 1838 by (Cases_on `x` >> fs[]) 1839 >> rw[] >> Cases_on `x` >> fs[] 1840 >> Cases_on `followers_old` >> fs[] 1841 >- (first_x_assum (qspec_then `h'` mp_tac) >> simp[] 1842 >> Cases_on `h'` >> fs[] >> rw[]) 1843 >- (first_x_assum (qspec_then `(q'',r'')` mp_tac) 1844 >> simp[]) 1845 ) 1846 >- metis_tac[] 1847 ) 1848 >- (`lookup x_id m.followers = SOME fls` 1849 by metis_tac[lookup_insert] 1850 >> `x_id ��� domain m.nodeInfo` 1851 by metis_tac[domain_lookup,wfg_def] 1852 >> metis_tac[]) 1853 >- (rw[] 1854 >> `fls = (LABEL,q')::followers_old` 1855 by metis_tac[lookup_insert,SOME_11] 1856 >> rw[] >> fs[] 1857 >- (`(FST x).edge_grp = LABEL.edge_grp` 1858 by (Cases_on `x` >> fs[]) 1859 >> qunabbrev_tac `LABEL` >> fs[] 1860 >> Cases_on `oldSucPairs = []` >> fs[] 1861 ) 1862 >- metis_tac[] 1863 ) 1864 >- (`lookup x_id m.followers = SOME fls` 1865 by metis_tac[lookup_insert,SOME_11] 1866 >> metis_tac[] 1867 ) 1868 >- (`(fl::fls) = (LABEL,q')::followers_old` 1869 by metis_tac[lookup_insert,SOME_11] 1870 >> rw[] >> fs[] 1871 ) 1872 >- (`(fl::fls) = (LABEL,q')::followers_old` 1873 by metis_tac[lookup_insert,SOME_11] 1874 >> rw[] >> fs[] 1875 ) 1876 >- (`(fl::fls) = (LABEL,q')::followers_old` 1877 by metis_tac[lookup_insert,SOME_11] 1878 >> rw[] >> fs[] 1879 ) 1880 >- (`(fl::fls) = (LABEL,q')::followers_old` 1881 by metis_tac[lookup_insert,SOME_11] 1882 >> rw[] >> fs[] 1883 ) 1884 >- (`(fl::fls) = (LABEL,q')::followers_old` 1885 by metis_tac[lookup_insert,SOME_11] 1886 >> rw[] >> fs[] 1887 >> Cases_on `fls` >> fs[] 1888 ) 1889 >- (`(fl::fls) = (LABEL,q')::followers_old` 1890 by metis_tac[lookup_insert,SOME_11] 1891 >> rw[] >> fs[] 1892 >> Cases_on `fls` >> fs[] 1893 ) 1894 >- metis_tac[lookup_insert] 1895 >- metis_tac[lookup_insert] 1896 ) 1897 ) 1898 ) 1899 >> first_x_assum (qspec_then `l1` mp_tac) 1900 >> qunabbrev_tac `TO_LABELS` >> simp[] >> rpt strip_tac 1901 >> fs[flws_sorted_def] >> metis_tac[] 1902 ) 1903QED 1904 1905val ADDEDGE_FINAL_LEMM = store_thm 1906 ("ADDEDGE_FINAL_LEMM", 1907 ``!g g2 f e. (wfg g ��� (addEdgeToGraph f e g = SOME g2) 1908 ��� until_iff_final g) 1909 ==> until_iff_final g2``, 1910 rpt strip_tac >> Cases_on `e` >> fs[addEdgeToGraph_def] 1911 >> Cases_on `l1` >> fs[] 1912 >> Cases_on `x` >> fs[updateNode_def] 1913 >- (fs[gfg_component_equality] >> fs[until_iff_final_def,findNode_def] 1914 >> rpt strip_tac 1915 >> `lookup q g.nodeInfo = SOME r` 1916 by metis_tac[MEM_toAList,FIND_LEMM2,SOME_11] 1917 >> Cases_on `q = id` >> rw[] 1918 >- (`node = nodeLabelAA r.frml r.is_final 1919 (edgeLabelAA 0 l l0::r.true_labels)` 1920 by metis_tac[lookup_insert,SOME_11] 1921 >> first_x_assum (qspec_then `id` mp_tac) >> simp[] 1922 ) 1923 >- (`lookup id g.nodeInfo = SOME node` 1924 by metis_tac[lookup_insert,SOME_11] 1925 >> first_x_assum (qspec_then `id` mp_tac) >> simp[] 1926 ) 1927 ) 1928 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac 1929 >> Q.HO_MATCH_ABBREV_TAC ` 1930 (FOLDR addSingleEdge (SOME g) L = SOME g2) 1931 ==> A` 1932 >> rpt strip_tac 1933 >> `!x x1 ls. FOLDR addSingleEdge (SOME x) ls = SOME x1 1934 ==> (x.nodeInfo = x1.nodeInfo)` by ( 1935 Induct_on `ls` >> fs[] >> rpt strip_tac 1936 >> qunabbrev_tac `addSingleEdge` >> fs[] 1937 >> `g_int.nodeInfo = x.nodeInfo` by metis_tac[] 1938 >> Cases_on `h'` >> metis_tac[addEdge_preserves_nodeInfo] 1939 ) 1940 >> qunabbrev_tac `A` >> rpt strip_tac 1941 >> `g.nodeInfo = g2.nodeInfo` by metis_tac[] 1942 >> fs[until_iff_final_def] >> rpt strip_tac 1943 >> metis_tac[] 1944 ) 1945 ); 1946 1947val _ = set_trace "BasicProvers.var_eq_old" 1 1948val _ = diminish_srw_ss ["ABBREV"] 1949Theorem ADDEDGE_LEMM: 1950 !g f e aP. wfg g ��� MEM f (graphStates g) 1951 ��� unique_node_formula g 1952 ��� (!x. MEM x e.sucs ==> MEM x (graphStates g)) 1953 ��� (flws_sorted g) 1954 ==> (?g2. (addEdgeToGraph f e g = SOME g2) ��� wfg g2 1955 ��� (set (graphStatesWithId g) = set (graphStatesWithId g2)) 1956 ��� (unique_node_formula g2) 1957 ��� (!h. 1958 if h = f 1959 then ?i. extractTrans g2 h 1960 = extractTrans g h ��� { (i, e.pos,e.neg,set e.sucs) } 1961 else extractTrans g2 h = extractTrans g h)) 1962Proof 1963 rpt strip_tac >> Cases_on `e` >> fs[addEdgeToGraph_def] 1964 >> fs[graphStates_def,MEM_MAP] 1965 >> `l1 = [] \/ ?h t. l1 = SNOC h t` by metis_tac[SNOC_CASES] 1966 >> `?q. (findNode (��(n,l). l.frml = (SND y).frml) g = SOME q) 1967 ��� ((��(n,l). l.frml = (SND y).frml) q)` by ( 1968 simp[findNode_def] 1969 >> qabbrev_tac `P = (��(n:num,l). l.frml = (SND y).frml)` 1970 >> `P y` by (qunabbrev_tac `P` >> Cases_on `y` >> fs[]) 1971 >> metis_tac[FIND_LEMM] 1972 ) 1973 >- ( 1974 Cases_on `q` >> fs[] >> rename[`_ = SOME (nId,frml)`] 1975 >> Q.HO_MATCH_ABBREV_TAC 1976 `?g2. updateNode nId NEW_LAB g = SOME g2 ��� Q g2` 1977 >> `���x. updateNode nId NEW_LAB g = SOME x` by ( 1978 simp[updateNode_def] >> fs[findNode_def] 1979 >> `MEM (nId, frml) (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 1980 >> fs[MEM_toAList] >> metis_tac[domain_lookup] 1981 ) 1982 >> `g.followers = x.followers` 1983 by fs[updateNode_def,gfg_component_equality] 1984 >> qexists_tac `x` >> qunabbrev_tac `Q` >> simp[] 1985 >> Q.HO_MATCH_ABBREV_TAC `A ��� B ��� C` 1986 >> `A ��� B ��� (A ��� B ==> C)` suffices_by metis_tac[] 1987 >> qunabbrev_tac `A` >> qunabbrev_tac `B` >> qunabbrev_tac `C` 1988 >> `lookup nId g.nodeInfo = SOME frml` by ( 1989 fs[unique_node_formula_def,graphStatesWithId_def,findNode_def] 1990 >> `MEM (nId,frml) (toAList g.nodeInfo) 1991 ��� (��(n,l). l.frml = (SND y).frml) (nId,frml)` 1992 by metis_tac[FIND_LEMM2] 1993 >> metis_tac[MEM_toAList] 1994 ) 1995 >> `unique_node_formula x` by metis_tac[ADD_0EDGE_LEMM] 1996 >> rpt strip_tac 1997 >- metis_tac[updateNode_preserves_wfg] 1998 >- (simp[graphStatesWithId_def,SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1999 >> fs[MEM_MAP,updateNode_def] >> Cases_on `x'` >> Cases_on `y'` 2000 >> Cases_on `q = nId` >> fs[findNode_def] >> rw[] 2001 >- (qexists_tac `(nId, NEW_LAB)` >> qunabbrev_tac `NEW_LAB` >> fs[] 2002 >> qabbrev_tac `P = (��(n:num,l). l.frml = (SND y).frml)` 2003 >> `P (nId,frml) ��� MEM (nId,frml) (toAList g.nodeInfo)` 2004 by metis_tac[FIND_LEMM2] 2005 >> qunabbrev_tac `P` >> fs[] 2006 >> `lookup nId g.nodeInfo = SOME r'` by metis_tac[MEM_toAList] 2007 >> `lookup nId g.nodeInfo = SOME frml` by metis_tac[MEM_toAList] 2008 >> `r' = frml` by metis_tac[SOME_11] >> rw[] 2009 >> rw[MEM_toAList] >> fs[gfg_component_equality] >> rw[] 2010 >> metis_tac[lookup_insert] 2011 ) 2012 >- (qexists_tac `(q,r')` >> fs[MEM_toAList,gfg_component_equality] 2013 >> rw[] >> metis_tac[lookup_insert]) 2014 >- (qexists_tac `(nId,frml)` >> fs[] 2015 >> qabbrev_tac `P = (��(n:num,l). l.frml = (SND y).frml)` 2016 >> `P (nId,frml) ��� MEM (nId,frml) (toAList g.nodeInfo)` 2017 by metis_tac[FIND_LEMM2] 2018 >> qunabbrev_tac `P` >> fs[] 2019 >> `lookup nId g.nodeInfo = SOME frml` by metis_tac[MEM_toAList] 2020 >> fs[gfg_component_equality] 2021 >> `lookup nId (insert nId NEW_LAB g.nodeInfo) = SOME r'` 2022 by metis_tac[MEM_toAList] 2023 >> fs[lookup_insert] >> qunabbrev_tac `r'` >> fs[] 2024 ) 2025 >- (qexists_tac `(q,r')` >> fs[MEM_toAList,gfg_component_equality] 2026 >> metis_tac[lookup_insert]) 2027 ) 2028 >- fs[] 2029 >- (`?z. findNode (��(n,l). l.frml = (SND y).frml) x 2030 = SOME (nId,NEW_LAB)` by ( 2031 `MEM (nId,frml) (toAList g.nodeInfo)` by metis_tac[MEM_toAList] 2032 >> fs[graphStatesWithId_def] 2033 >> `MEM ((��(id,label). (id,label.frml)) (nId,frml)) 2034 (MAP (��(id,label). (id,label.frml)) (toAList x.nodeInfo))` 2035 by metis_tac[MEM_MAP] 2036 >> fs[MEM_MAP] >> Cases_on `y'` 2037 >> `(��(n,l). l.frml = (SND y).frml) (q,r)` by fs[] 2038 >> `?z. (FIND (��(n,l). l.frml = (SND y).frml) 2039 (toAList x.nodeInfo) = SOME z) 2040 ��� (��(n,l). l.frml = (SND y).frml) z` by metis_tac[FIND_LEMM] 2041 >> Cases_on `z` >> fs[] >> simp[findNode_def] 2042 >> `MEM (q,r.frml) (graphStatesWithId x)` by ( 2043 simp[graphStatesWithId_def,MEM_MAP] 2044 >> qexists_tac `(q,r)` >> fs[] 2045 ) 2046 >> `MEM (q',r'.frml) (graphStatesWithId x)` by ( 2047 simp[graphStatesWithId_def,MEM_MAP] 2048 >> qexists_tac `(q',r')` >> fs[] 2049 >> metis_tac[FIND_LEMM2] 2050 ) 2051 >> fs[unique_node_formula_def] 2052 >> `q' = q` by metis_tac[] 2053 >> `MEM (q,r') (toAList x.nodeInfo)` by metis_tac[FIND_LEMM2] 2054 >> fs[MEM_toAList,updateNode_def,gfg_component_equality] 2055 >> `lookup q (insert q NEW_LAB g.nodeInfo) = SOME r` by metis_tac[] 2056 >> metis_tac[lookup_insert,SOME_11] 2057 ) 2058 >> Cases_on `h = f` >> fs[] 2059 >- ( 2060 qexists_tac `0` >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2061 >> fs[extractTrans_def] 2062 >- ( 2063 qexists_tac `label` >> fs[] >> rpt strip_tac 2064 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2065 >- (rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2066 >> simp[MEMBER_NOT_EMPTY] >> rpt strip_tac 2067 >> `?a. a ��� {suc.frml | ���sucId. 2068 MEM (label,sucId) 2069 (OPTION_TO_LIST (lookup nId x.followers)) 2070 ��� SOME suc = lookup sucId x.nodeInfo}` 2071 by metis_tac[MEMBER_NOT_EMPTY] 2072 >> fs[OPTION_TO_LIST_MEM] 2073 >> `MEM (sucId,suc.frml) (graphStatesWithId g)` by ( 2074 simp[graphStatesWithId_def,MEM_MAP] 2075 >> qexists_tac `(sucId,suc)` >> fs[] 2076 >> metis_tac[MEM_toAList] 2077 ) 2078 >> `?a. a ��� {suc.frml | 2079 ���sucId. 2080 (���l. lookup nId x.followers = SOME l 2081 ��� MEM (label,sucId) l) 2082 ��� SOME suc = lookup sucId g.nodeInfo}` by ( 2083 qexists_tac `suc.frml` >> fs[] 2084 >> fs[graphStatesWithId_def,MEM_MAP] 2085 >> Cases_on `y'` >> qexists_tac `r` >> fs[] 2086 >> qexists_tac `q` >> metis_tac[MEM_toAList] 2087 ) >> metis_tac[MEMBER_NOT_EMPTY] 2088 ) 2089 >- ( 2090 fs[OPTION_TO_LIST_MEM] 2091 >> rename[`findNode _ x = SOME x1`] 2092 >> `SOME ((��(id,label). (id,label.frml)) x1) 2093 = FIND (��a. SND a = (SND y).frml) (graphStatesWithId x)` 2094 by metis_tac[OPTION_MAP_DEF,UNIQUE_NODE_FORM_LEMM] 2095 >> Cases_on `x1` >> fs[] 2096 >> `MEM (q,r.frml) (graphStatesWithId x) 2097 ��� ((��a. SND a = (SND y).frml) (q,r.frml))` 2098 by (Q.HO_MATCH_ABBREV_TAC `MEM A L ��� P A` 2099 >> metis_tac[FIND_LEMM2]) 2100 >> `MEM (q,r.frml) (graphStatesWithId g)` by metis_tac[MEM] 2101 >> `MEM (nId,frml.frml) (graphStatesWithId g)` by ( 2102 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2103 >> qexists_tac `(nId,frml)` >> fs[] 2104 >> metis_tac[MEM_toAList] 2105 ) 2106 >> `q = nId` by ( 2107 `SND (q,r.frml) = f` by fs[] 2108 >> `SND (nId,r.frml) = f` by fs[] 2109 >> IMP_RES_TAC UNIQUE_NODE_FORM_LEMM2 >> fs[] 2110 ) 2111 >> rw[] 2112 >> Cases_on `sucId = nId` >> fs[] >> rw[] 2113 >- (qexists_tac `frml` >> fs[] 2114 >> `MEM (nId,suc) (toAList x.nodeInfo)` 2115 by metis_tac[MEM_toAList] 2116 >> `MEM (nId,suc.frml) (graphStatesWithId x)` by ( 2117 simp[graphStatesWithId_def,MEM_MAP] 2118 >> qexists_tac `(nId,suc)` >> fs[] 2119 ) 2120 >> `MEM (nId,suc.frml) (graphStatesWithId g)` by fs[] 2121 >> `suc.frml = frml.frml` by ( 2122 fs[graphStatesWithId_def,MEM_MAP] 2123 >> rename[`(nId,suc.frml) = _ y1`] 2124 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2125 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2126 >> rename[`(nId,suc.frml) = _ y2`] >> rpt strip_tac 2127 >> Cases_on `y1` >> Cases_on `y2` >> fs[] >> rw[] 2128 >> metis_tac[MEM_toAList,SOME_11] 2129 ) 2130 >> rw[] >> qexists_tac `nId` >> fs[] 2131 >> metis_tac[] 2132 ) 2133 >- ( 2134 qexists_tac `suc` >> fs[] >> qexists_tac `sucId` 2135 >> `���l. lookup nId g.followers = SOME l ��� MEM (label,sucId) l` 2136 by metis_tac[] 2137 >> rpt strip_tac >> fs[updateNode_def] >> Cases_on `g` 2138 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 2139 ) 2140 ) 2141 >- ( 2142 fs[OPTION_TO_LIST_MEM] >> Cases_on `sucId = nId` >> fs[] 2143 >> rw[] 2144 >- ( 2145 `suc = frml` by metis_tac[SOME_11] 2146 >> qexists_tac `NEW_LAB` >> fs[] >> rpt strip_tac 2147 >- (qunabbrev_tac `NEW_LAB` >> fs[]) 2148 >- (qexists_tac `nId` 2149 >> fs[updateNode_def,gfg_component_equality] 2150 >> metis_tac[lookup_insert] 2151 ) 2152 ) 2153 >- (qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 2154 >> fs[updateNode_def,gfg_component_equality] 2155 >> metis_tac[lookup_insert] 2156 ) 2157 ) 2158 ) 2159 >- (`MEM l' (edgeLabelAA 0 l l0::frml.true_labels)` by ( 2160 fs[OPTION_TO_LIST_MEM] >> fs[] >> rw[] >> fs[] 2161 >> qunabbrev_tac `NEW_LAB` >> fs[] >> rw[] 2162 >> fs[] 2163 ) 2164 >> fs[] >> disj1_tac >> fs[] >> disj2_tac 2165 >> qexists_tac `l'` >> simp[OPTION_TO_LIST_MEM] 2166 ) 2167 >- (qexists_tac `label` >> fs[] >> rpt strip_tac 2168 >> simp[SET_EQ_SUBSET,SUBSET_DEF] 2169 >> rpt strip_tac >> Cases_on `sucId = nId` >> rw[] 2170 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2171 >> simp[MEMBER_NOT_EMPTY] 2172 >> Q.HO_MATCH_ABBREV_TAC `~(A = {}) ==> ~(B = {})` 2173 >> rpt strip_tac 2174 >> `?a. a ��� A` by metis_tac[MEMBER_NOT_EMPTY] 2175 >> `?b. b ��� B` suffices_by metis_tac[MEMBER_NOT_EMPTY] 2176 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 2177 >> fs[OPTION_TO_LIST_MEM] 2178 >> `MEM (sucId,suc.frml) (graphStatesWithId g)` by ( 2179 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2180 >> qexists_tac `(sucId,suc)` >> fs[] 2181 >> metis_tac[MEM_toAList] 2182 ) 2183 >> `MEM (sucId,suc.frml) (graphStatesWithId x)` 2184 by metis_tac[] 2185 >> fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y''` 2186 >> fs[] >> metis_tac[MEM_toAList,SOME_11] 2187 ) 2188 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2189 >> simp[MEMBER_NOT_EMPTY] 2190 >> Q.HO_MATCH_ABBREV_TAC `~(A = {}) ==> (B = {}) ==> C` 2191 >> rpt strip_tac 2192 >> `?a. a ��� A` by metis_tac[MEMBER_NOT_EMPTY] 2193 >> `?b. b ��� B` suffices_by metis_tac[MEMBER_NOT_EMPTY] 2194 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 2195 >> fs[OPTION_TO_LIST_MEM] 2196 >> `MEM (sucId',suc.frml) (graphStatesWithId g)` by ( 2197 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2198 >> qexists_tac `(sucId',suc)` >> fs[] 2199 >> metis_tac[MEM_toAList] 2200 ) 2201 >> `MEM (sucId',suc.frml) (graphStatesWithId x)` 2202 by metis_tac[] 2203 >> fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y''` 2204 >> fs[] >> metis_tac[MEM_toAList,SOME_11] 2205 ) 2206 >- (qexists_tac `NEW_LAB` >> fs[findNode_def] 2207 >> `MEM (nId,NEW_LAB) (toAList x.nodeInfo)` 2208 by metis_tac[FIND_LEMM2] 2209 >> `MEM (nId,frml) (toAList g.nodeInfo)` 2210 by metis_tac[FIND_LEMM2] 2211 >> `suc = frml` by metis_tac[SOME_11,MEM_toAList] 2212 >> `suc.frml = NEW_LAB.frml` by ( 2213 qunabbrev_tac `NEW_LAB` >> fs[] 2214 ) 2215 >> fs[] >> qexists_tac `nId` >> fs[updateNode_def] 2216 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 2217 ) 2218 >- (qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 2219 >> fs[updateNode_def,gfg_component_equality] 2220 >> metis_tac[lookup_insert] 2221 ) 2222 >- (qexists_tac `frml` >> fs[findNode_def] 2223 >> `MEM (nId,NEW_LAB) (toAList x.nodeInfo)` 2224 by metis_tac[FIND_LEMM2] 2225 >> `NEW_LAB = suc` by metis_tac[MEM_toAList,SOME_11] >> rw[] 2226 >- (qunabbrev_tac `NEW_LAB` >> fs[]) 2227 >- (qexists_tac `nId` >> fs[OPTION_TO_LIST_MEM]) 2228 ) 2229 >- (qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 2230 >> fs[updateNode_def,gfg_component_equality] 2231 >> metis_tac[lookup_insert]) 2232 ) 2233 >- (`MEM l' frml.true_labels` by ( 2234 fs[OPTION_TO_LIST_MEM] >> fs[] >> rw[] >> fs[] 2235 ) 2236 >> disj2_tac >> qunabbrev_tac `NEW_LAB` >> qexists_tac `l'` 2237 >> fs[OPTION_TO_LIST_MEM] 2238 ) 2239 >- (disj2_tac >> qexists_tac `edgeLabelAA 0 l l0` >> fs[] 2240 >> qunabbrev_tac `NEW_LAB` >> fs[OPTION_TO_LIST_MEM] 2241 ) 2242 ) 2243 >- ( 2244 Cases_on `h = (SND y).frml` >> fs[extractTrans_def] 2245 >> `findNode (��(n,l). l.frml = h) x 2246 = findNode (��(n,l). l.frml = h) g` by ( 2247 simp[findNode_def] 2248 >> Cases_on `?a b. MEM (a,b) (toAList g.nodeInfo) 2249 ��� b.frml = h` >> fs[] 2250 >- ( 2251 `MEM (a,h) (graphStatesWithId g)` by ( 2252 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2253 >> qexists_tac `(a,b)` >> fs[] 2254 ) 2255 >> `MEM (a,h) (graphStatesWithId x)` by metis_tac[] 2256 >> `?z. FIND (��(n,l). l.frml = h) (toAList x.nodeInfo) = SOME z` 2257 by ( 2258 fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y''` >> fs[] 2259 >> `(��(n,l). l.frml = r.frml) (q,r)` by fs[] 2260 >> metis_tac[FIND_LEMM] 2261 ) 2262 >> `?z2. FIND (��(n,l). l.frml = h) (toAList g.nodeInfo) 2263 = SOME z2` by ( 2264 fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y'` >> fs[] 2265 >> Cases_on `y''` >> fs[] 2266 >> `(��(n,l). l.frml = r.frml) (q,r)` by fs[] 2267 >> metis_tac[FIND_LEMM] 2268 ) 2269 >> Cases_on `z` >> Cases_on `z2` 2270 >> `lookup q x.nodeInfo = SOME r ��� (��(n,l). l.frml = h) (q,r) 2271 ��� lookup q' g.nodeInfo = SOME r' 2272 ��� (��(n,l). l.frml = h) (q',r')` 2273 by metis_tac[FIND_LEMM2,MEM_toAList] 2274 >> fs[updateNode_def,gfg_component_equality] 2275 >> `q = a ��� q' = a` by ( 2276 fs[unique_node_formula_def] 2277 >> `MEM (q,h) (graphStatesWithId x)` by ( 2278 fs[graphStatesWithId_def,MEM_MAP] 2279 >> qexists_tac `(q,r)` >> fs[MEM_toAList] 2280 ) 2281 >> `MEM (q',h) (graphStatesWithId g)` by ( 2282 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2283 >> qexists_tac `(q',r')` >> fs[MEM_toAList] 2284 ) 2285 >> metis_tac[] 2286 ) 2287 >> rw[] 2288 >> `~(a = nId)` by ( 2289 CCONTR_TAC >> fs[findNode_def] >> rw[] 2290 >> fs[] 2291 ) 2292 >> metis_tac[lookup_insert,SOME_11] 2293 ) 2294 >- ( 2295 fs[] 2296 >> `���a b. ��MEM (a,b) (toAList g.nodeInfo) 2297 ��� ~((��(n,l). l.frml = h) (a,b))` by fs[] 2298 >> `!a. ~(FIND (��(n,l). l.frml = h) (toAList g.nodeInfo) 2299 = SOME a)` by ( 2300 rpt strip_tac >> Cases_on `a` 2301 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 2302 >> first_x_assum (qspec_then `r` mp_tac) >> rpt strip_tac 2303 >> metis_tac[FIND_LEMM2] 2304 ) 2305 >> Cases_on `FIND (��(n,l). l.frml = h) (toAList g.nodeInfo)` 2306 >> fs[] 2307 >> `���a b. ��MEM (a,b) (toAList x.nodeInfo) ��� b.frml ��� h` by ( 2308 CCONTR_TAC >> fs[] 2309 >> `MEM (a,h) (graphStatesWithId x)` by ( 2310 PURE_REWRITE_TAC[graphStatesWithId_def,MEM_MAP] 2311 >> qexists_tac `(a,b)` >> fs[MEM_toAList] 2312 ) 2313 >> `MEM (a,h) (graphStatesWithId g)` by metis_tac[] 2314 >> fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y''` 2315 >> fs[] >> metis_tac[] 2316 ) 2317 >> Cases_on `FIND (��(n,l). l.frml = h) (toAList x.nodeInfo)` 2318 >> fs[] >> Cases_on `x'` 2319 >> `MEM (q,r) (toAList x.nodeInfo) ��� (��(n,l). l.frml = h) (q,r)` 2320 by metis_tac[FIND_LEMM2] 2321 >> fs[] >> metis_tac[] 2322 ) 2323 ) >> rpt strip_tac 2324 >> PURE_REWRITE_TAC[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2325 >> fs[] 2326 >- (qexists_tac `label` >> fs[] >> rpt strip_tac 2327 >- (Cases_on `sucId = nId` >> fs[] >> rw[] 2328 >- (qexists_tac `frml` >> qexists_tac `nId` 2329 >> fs[OPTION_TO_LIST_MEM] >> qexists_tac `l'` >> fs[] 2330 >> qexists_tac `x'` >> fs[] 2331 ) 2332 >- (qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 2333 >> fs[OPTION_TO_LIST_MEM] 2334 >> `lookup sucId x.nodeInfo = lookup sucId g.nodeInfo` by ( 2335 fs[updateNode_def,gfg_component_equality] 2336 >> metis_tac[lookup_insert] 2337 ) 2338 >> fs[] >> qexists_tac `l'` >> fs[] >> qexists_tac `x'` >> fs[] 2339 ) 2340 ) 2341 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 2342 >> Cases_on `sucId' = nId` >> fs[] >> rw[] 2343 >- (qexists_tac `frml` >> fs[] 2344 >> `suc' = NEW_LAB` by ( 2345 fs[updateNode_def,gfg_component_equality] 2346 >> metis_tac[lookup_insert,SOME_11] 2347 ) 2348 >> qunabbrev_tac `NEW_LAB` >> fs[gfg_component_equality] 2349 >> qexists_tac `nId` >> fs[OPTION_TO_LIST_MEM] 2350 ) 2351 >- (qexists_tac `suc'` >> fs[] >> qexists_tac `sucId'` >> fs[] 2352 >> fs[updateNode_def,gfg_component_equality] 2353 >> metis_tac[lookup_insert] 2354 ) 2355 >- (qexists_tac `NEW_LAB` >> fs[] 2356 >> `suc' = frml` by ( 2357 fs[updateNode_def,gfg_component_equality] 2358 >> metis_tac[lookup_insert,SOME_11] 2359 ) 2360 >> `suc'.frml = NEW_LAB.frml` by ( 2361 qunabbrev_tac `NEW_LAB` >> fs[] 2362 ) 2363 >> fs[] >> qexists_tac `nId` >> fs[updateNode_def] 2364 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 2365 ) 2366 >- (qexists_tac `suc'` >> fs[] >> qexists_tac `sucId'` >> fs[] 2367 >> fs[updateNode_def,gfg_component_equality] 2368 >> metis_tac[lookup_insert] 2369 ) 2370 ) 2371 ) 2372 >- (disj2_tac >> fs[] >> qexists_tac `l'` >> fs[OPTION_TO_LIST_MEM] 2373 >> metis_tac[] 2374 ) 2375 >- (qexists_tac `label` >> fs[] >> rpt strip_tac 2376 >- (Cases_on `sucId = nId` >> fs[] >> rw[] 2377 >- (qexists_tac `NEW_LAB` >> qexists_tac `nId` 2378 >> fs[OPTION_TO_LIST_MEM,updateNode_def,gfg_component_equality] 2379 >> metis_tac[lookup_insert] 2380 ) 2381 >- (qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 2382 >> fs[OPTION_TO_LIST_MEM,updateNode_def,gfg_component_equality] 2383 >> metis_tac[lookup_insert] 2384 ) 2385 ) 2386 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 2387 >> Cases_on `sucId' = nId` >> fs[] >> rw[] 2388 >- (qexists_tac `NEW_LAB` >> fs[] 2389 >> `suc' = frml` by ( 2390 fs[updateNode_def,gfg_component_equality] 2391 >> metis_tac[lookup_insert,SOME_11] 2392 ) 2393 >> `suc'.frml = NEW_LAB.frml` by ( 2394 qunabbrev_tac `NEW_LAB` >> fs[] 2395 ) 2396 >> fs[] >> qexists_tac `nId` >> fs[updateNode_def] 2397 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 2398 ) 2399 >- (qexists_tac `suc'` >> fs[] >> qexists_tac `sucId'` >> fs[] 2400 >> fs[updateNode_def,gfg_component_equality] 2401 >> metis_tac[lookup_insert] 2402 ) 2403 >- (qexists_tac `frml` >> fs[] 2404 >> `suc' = NEW_LAB` by ( 2405 fs[updateNode_def,gfg_component_equality] 2406 >> metis_tac[lookup_insert,SOME_11] 2407 ) 2408 >> qunabbrev_tac `NEW_LAB` >> fs[gfg_component_equality] 2409 >> qexists_tac `nId` >> fs[OPTION_TO_LIST_MEM] 2410 ) 2411 >- (qexists_tac `suc'` >> fs[] >> qexists_tac `sucId'` >> fs[] 2412 >> fs[updateNode_def,gfg_component_equality] 2413 >> metis_tac[lookup_insert] 2414 ) 2415 ) 2416 ) 2417 >- (disj2_tac >> fs[] >> qexists_tac `l'` >> fs[]) 2418 ) 2419 ) 2420 ) 2421 >- ( 2422 fs[] >> Cases_on `q` >> fs[] >> rename[`_ = SOME (nId,frml)`] 2423 >> `nId ��� domain g.followers` by ( 2424 `nId ��� domain g.nodeInfo` suffices_by metis_tac[wfg_def] 2425 >> fs[findNode_def] 2426 >> `MEM (nId, frml) (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 2427 >> fs[MEM_toAList] >> metis_tac[domain_lookup] 2428 ) 2429 >> fs[domain_lookup] 2430 >> Q.HO_MATCH_ABBREV_TAC 2431 `?x. FOLDR addSingleEdge a_init ls = SOME x ��� Q x` 2432 >> `!lab x. MEM (lab,x) ls ==> ?h. MEM (x,h) (toAList g.nodeInfo)` by ( 2433 rpt strip_tac >> qunabbrev_tac `ls` >> fs[MEM_MAP] 2434 >> fs[CAT_OPTIONS_MEM,findNode_def,MEM_MAP] 2435 >> `MEM y' (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 2436 >> Cases_on `y'` >> fs[] >> metis_tac[] 2437 ) 2438 >> qabbrev_tac `LABEL = 2439 <|edge_grp := (if v = [] then 1 else (HD (MAP FST v)).edge_grp) + 1; 2440 pos_lab := l; 2441 neg_lab := l0|>` 2442 >> qabbrev_tac ` 2443 TO_LABELS = ��l. 2444 MAP (��i. (LABEL,i)) 2445 (MAP FST 2446 (CAT_OPTIONS 2447 ((MAP (��s. findNode (��(n,l). l.frml = s) g) l) 2448 ++ [findNode (��(n,l). l.frml = h) g])))` 2449 >> `ls = TO_LABELS t` by (qunabbrev_tac `TO_LABELS` >> simp[]) 2450 >> `?n. findNode (��(n,l). l.frml = h) g = SOME n` by ( 2451 `���y. h = (SND y).frml ��� MEM y (toAList g.nodeInfo)` by metis_tac[] 2452 >> simp[findNode_def] 2453 >> `(��(n,l). l.frml = (SND y').frml) y'` by (Cases_on `y'` >> fs[]) 2454 >> metis_tac[FIND_LEMM] 2455 ) 2456 >> `!i p n s. (i,p,n,s) ��� extractTrans g (SND y).frml 2457 ==> i < LABEL.edge_grp` by ( 2458 simp[extractTrans_def] >> rpt strip_tac 2459 >- (Cases_on `v` >> fs[OPTION_TO_LIST_MEM] 2460 >> `?s_fr. s_fr ��� s` by fs[MEMBER_NOT_EMPTY] 2461 >> fs[] >> rw[] >> fs[] >> qunabbrev_tac `LABEL` 2462 >> fs[theorem "edgeLabelAA_component_equality"] >> rw[] 2463 >> `first_flw_has_max_counter g` by metis_tac[FLWS_SORTED_IMP_FFHMC] 2464 >> fs[first_flw_has_max_counter_def] >> rw[] 2465 >> `���y. MEM y t' ��� (FST y).edge_grp ��� (FST h').edge_grp` 2466 by ( 2467 `nId ��� domain g.nodeInfo` suffices_by metis_tac[] 2468 >> metis_tac[domain_lookup,wfg_def] 2469 ) 2470 >> first_x_assum (qspec_then `(label,sucId)` mp_tac) >> simp[] 2471 ) 2472 >- (qunabbrev_tac `LABEL` >> simp[] 2473 >> metis_tac[DECIDE``!x. 0 < x + 1``] 2474 ) 2475 ) 2476 >> `!fs qs. ((!lab x. MEM (lab,x) qs 2477 ==> (?h. MEM (x,h) (toAList g.nodeInfo) 2478 ��� (lab = LABEL))) 2479 ��� (qs = TO_LABELS fs) 2480 ��� (!x. MEM x fs 2481 ==> ���y. x = (SND y).frml ��� MEM y (toAList g.nodeInfo))) 2482 ==> ?m. (FOLDR addSingleEdge a_init qs = SOME m) 2483 ��� (g.nodeInfo = m.nodeInfo) 2484 ��� (wfg m) 2485 ��� (!a. 2486 if a = f 2487 then extractTrans m a 2488 = (extractTrans g a 2489 ��� { (LABEL.edge_grp,l,l0,h INSERT set fs)}) 2490 else extractTrans m a = extractTrans g a) 2491 ��� (!x id fls q r. 2492 findNode (��(n,l). l.frml = f) m = SOME (q,r) 2493 ��� (lookup q m.followers = SOME fls) 2494 ==> ((!f. MEM f fls 2495 ==> (FST f).edge_grp <= LABEL.edge_grp) 2496 ��� !o_id. ~(o_id = q) 2497 ==> (lookup o_id m.nodeInfo 2498 = lookup o_id g.nodeInfo)))` by ( 2499 Induct_on `fs` >> fs[] 2500 >- ( 2501 qunabbrev_tac `a_init` >> rpt strip_tac 2502 >> `TO_LABELS [] = [(LABEL,FST n)]` by ( 2503 qunabbrev_tac `TO_LABELS` >> fs[CAT_OPTIONS_def] 2504 ) 2505 >> fs[] 2506 >> `?k. addSingleEdge (LABEL,FST n) (SOME g) = SOME k 2507 ��� (g.nodeInfo = k.nodeInfo) ��� (wfg k)` by ( 2508 qunabbrev_tac `addSingleEdge` >> fs[] 2509 >> `?k. addEdge nId (LABEL,FST n) g = SOME k` suffices_by ( 2510 metis_tac[addEdge_preserves_wfg,addEdge_preserves_nodeInfo] 2511 ) 2512 >> simp[addEdge_def] >> fs[findNode_def] >> dsimp[] 2513 >> `MEM (nId,frml) (toAList g.nodeInfo) 2514 ��� MEM (FST n,h') (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 2515 >> metis_tac[MEM_toAList,domain_lookup, wfg_def] 2516 ) 2517 >> qexists_tac `k` 2518 >> `���fls q r. 2519 findNode (��(n,l). l.frml = (SND y).frml) k = SOME (q,r) 2520 ��� lookup q k.followers = SOME fls 2521 ==> (���f. MEM f fls ��� (FST f).edge_grp ��� LABEL.edge_grp 2522 ��� ���o_id. o_id ��� q 2523 ��� lookup o_id k.nodeInfo = lookup o_id g.nodeInfo)` 2524 by ( 2525 qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 2526 >> `first_flw_has_max_counter g` by metis_tac[FLWS_SORTED_IMP_FFHMC] 2527 >> simp[first_flw_has_max_counter_def] >> rpt strip_tac 2528 >> `(q,r) = (nId,frml)` by fs[findNode_def] 2529 >> Cases_on `followers_old` >> fs[first_flw_has_max_counter_def] 2530 >> fs[gfg_component_equality] >> rw[] 2531 >- (`fls = [(LABEL,FST n)]` by metis_tac[lookup_insert,SOME_11] 2532 >> fs[] 2533 ) 2534 >-(`(FST h'').edge_grp <= LABEL.edge_grp` by ( 2535 qunabbrev_tac `LABEL` 2536 >> fs[theorem "edgeLabelAA_component_equality"] 2537 ) 2538 >> `fls = (LABEL,FST n)::h''::t'` 2539 by metis_tac[lookup_insert,SOME_11] 2540 >> rw[] >> fs[] 2541 >> metis_tac[DECIDE``!x y z. x <= y ��� y <= z ==> x <= z``]) 2542 ) 2543 >> fs[] >> rpt strip_tac >> fs[] 2544 >> Cases_on `(SND y).frml = a` >> fs[] 2545 >- ( 2546 `findNode (��(n,l). l.frml = a) k = SOME (nId,frml)` 2547 by fs[findNode_def] 2548 >> `!id. lookup id k.followers = 2549 if id = nId then SOME ((LABEL,FST n)::v) 2550 else lookup id g.followers` by ( 2551 qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 2552 >> rpt strip_tac >> Cases_on `id = nId` >> fs[gfg_component_equality] 2553 >> metis_tac[lookup_insert] 2554 ) 2555 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 2556 >- (Cases_on `x = (LABEL.edge_grp,l,l0,{h})` >> fs[] 2557 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2558 >> simp[extractTrans_def] >> rpt strip_tac 2559 >- (disj1_tac >> fs[] >> qexists_tac `label` >> fs[] 2560 >> `~(LABEL = label)` by ( 2561 qunabbrev_tac `LABEL` >> Cases_on `x` >> fs[] 2562 >> rw[] >> fs[theorem "edgeLabelAA_component_equality"] 2563 >> POP_ASSUM mp_tac 2564 >> Q.HO_MATCH_ABBREV_TAC `~(H = {h}) ==> A` 2565 >> `~A ==> H = {h}` suffices_by metis_tac[] 2566 >> qunabbrev_tac `A` >> qunabbrev_tac `H` 2567 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2568 >> fs[OPTION_TO_LIST_MEM,findNode_def] 2569 >> Cases_on `n` >> rw[] >> fs[] 2570 >> rename[`FIND (��(n,l). l.frml = h) _ = SOME (id,node)`, 2571 `MEM (id,h') (toAList k.nodeInfo)`] 2572 >> `first_flw_has_max_counter g` by metis_tac[FLWS_SORTED_IMP_FFHMC] 2573 >- (`(suc = node) ��� (��(n,l). l.frml = h) (id,node)` 2574 by metis_tac[FIND_LEMM2,MEM_toAList,SOME_11] 2575 >> fs[] 2576 ) 2577 >- (qexists_tac `node` 2578 >> `(��(n,l). l.frml = h) (id,node)` 2579 by metis_tac[FIND_LEMM2] 2580 >> fs[theorem "edgeLabelAA_component_equality"] 2581 >> metis_tac[MEM_toAList,FIND_LEMM2] 2582 ) 2583 >- (`suc = node ��� (��(n,l). l.frml = h) (id,node)` 2584 by metis_tac[FIND_LEMM2,MEM_toAList,SOME_11] 2585 >> fs[] 2586 ) 2587 >- (Cases_on `v` >> fs[first_flw_has_max_counter_def] 2588 >- (Cases_on `label` >> Cases_on `h''` 2589 >> fs[theorem "edgeLabelAA_component_equality"]) 2590 >- (`���y. MEM y t' 2591 ��� (FST y).edge_grp ��� (FST h'').edge_grp` 2592 by ( 2593 `nId ��� domain g.nodeInfo` 2594 suffices_by metis_tac[wfg_def,domain_lookup] 2595 >> metis_tac[domain_lookup,wfg_def] 2596 ) 2597 >> first_x_assum (qspec_then `(label,sucId)` mp_tac) 2598 >> simp[] 2599 ) 2600 ) 2601 >- (qexists_tac `node` 2602 >> `(��(n,l). l.frml = h) (id,node)` 2603 by metis_tac[FIND_LEMM2] 2604 >> fs[theorem "edgeLabelAA_component_equality"] 2605 >> metis_tac[MEM_toAList,FIND_LEMM2] 2606 ) 2607 ) 2608 >> rpt strip_tac >> simp[SET_EQ_SUBSET,SUBSET_DEF] 2609 >> fs[OPTION_TO_LIST_MEM] 2610 ) 2611 >- metis_tac[] 2612 ) 2613 >- (`FST x < LABEL.edge_grp` by ( 2614 Cases_on `x` >> Cases_on `r` >> Cases_on `r'` 2615 >> fs[] >> metis_tac[] 2616 ) 2617 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2618 >> simp[extractTrans_def] >> rpt strip_tac 2619 >- (disj1_tac >> qexists_tac `label` >> fs[] 2620 >> rpt strip_tac >> simp[SET_EQ_SUBSET,SUBSET_DEF] 2621 >- (fs[OPTION_TO_LIST_MEM] >> POP_ASSUM mp_tac 2622 >> dsimp[] 2623 >> Q.HO_MATCH_ABBREV_TAC `~(A = {})` 2624 >> `?a. a ��� A` suffices_by metis_tac[MEMBER_NOT_EMPTY] 2625 >> qunabbrev_tac `A` >> fs[] 2626 >> `?a. a ��� 2627 {suc.frml | 2628 ���sucId. 2629 MEM (label,sucId) v 2630 ��� SOME suc = lookup sucId k.nodeInfo}` 2631 by metis_tac[MEMBER_NOT_EMPTY] 2632 >> fs[] >> metis_tac[] 2633 ) 2634 >- (rpt strip_tac >> fs[OPTION_TO_LIST_MEM] 2635 >- (rw[] >> fs[] >> metis_tac[]) 2636 >- (Cases_on `x` >> fs[]) 2637 >- (rw[] >> fs[] >> metis_tac[]) 2638 ) 2639 ) 2640 >- (disj2_tac >> fs[] >> metis_tac[]) 2641 ) 2642 >- (simp[extractTrans_def] >> qexists_tac `LABEL` >> fs[] 2643 >> rpt strip_tac 2644 >- (qunabbrev_tac `LABEL` >> fs[] 2645 >> metis_tac[DECIDE ``!x. 0 < x + 1``] 2646 ) 2647 >- (POP_ASSUM mp_tac >> simp[] >> Q.HO_MATCH_ABBREV_TAC `~(A = {})` 2648 >> `?a. a ��� A` suffices_by metis_tac[MEMBER_NOT_EMPTY] 2649 >> qunabbrev_tac `A` >> Cases_on `n` >> qexists_tac `r.frml` 2650 >> fs[] >> qexists_tac `r` >> fs[OPTION_TO_LIST_MEM] 2651 >> metis_tac[findNode_def,FIND_LEMM2,MEM_toAList] 2652 ) 2653 >- (qunabbrev_tac `LABEL` >> fs[]) 2654 >- (qunabbrev_tac `LABEL` >> fs[]) 2655 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2656 >- (Cases_on `n` >> fs[] >> qexists_tac `r` 2657 >> fs[findNode_def] 2658 >> `(��(n,l). l.frml = h) (q,r) 2659 ��� MEM (q,r) (toAList k.nodeInfo)` 2660 by metis_tac[FIND_LEMM2] 2661 >> fs[] >> qexists_tac `q` >> fs[OPTION_TO_LIST_MEM] 2662 >> metis_tac[MEM_toAList] 2663 ) 2664 >- (fs[OPTION_TO_LIST_MEM] >> Cases_on `n` >> fs[] 2665 >> fs[findNode_def] 2666 >> `(��(n,l). l.frml = h) (q,r) 2667 ��� MEM (q,r) (toAList k.nodeInfo)` 2668 by metis_tac[FIND_LEMM2] 2669 >> rw[] >> fs[] 2670 >- (`suc = r` by metis_tac[MEM_toAList,SOME_11] 2671 >> fs[]) 2672 >- (qunabbrev_tac `LABEL` >> fs[] >> Cases_on `v` 2673 >> fs[] >> Cases_on `h''` 2674 >> fs[theorem "edgeLabelAA_component_equality"] 2675 >> `first_flw_has_max_counter g` by metis_tac[FLWS_SORTED_IMP_FFHMC] 2676 >> fs[first_flw_has_max_counter_def] 2677 >> `���y. MEM y t' 2678 ��� (FST y).edge_grp ��� (FST (q',r')).edge_grp` 2679 by ( 2680 `nId ��� domain g.nodeInfo` suffices_by metis_tac[] 2681 >> metis_tac[domain_lookup,wfg_def] 2682 ) 2683 >> `q'.edge_grp + 1 <= q'.edge_grp` by ( 2684 first_x_assum (qspec_then ` 2685 (<|edge_grp := q'.edge_grp + 1; pos_lab := l; 2686 neg_lab := l0|>,sucId)` mp_tac) >> simp[] 2687 ) 2688 >> fs[] 2689 ) 2690 ) 2691 ) 2692 ) 2693 ) 2694 >- (`findNode (��(n,l). l.frml = a) g 2695 = findNode (��(n,l). l.frml = a) k` by fs[findNode_def] 2696 >> Cases_on `findNode (��(n,l). l.frml = a) g` >> fs[] 2697 >- ( 2698 `!x b. (findNode (��(n,l). l.frml = b) x = NONE) 2699 ==> (extractTrans x b = {})` by ( 2700 rpt strip_tac 2701 >> `!q. ~ (q ��� extractTrans x b)` 2702 suffices_by metis_tac[MEMBER_NOT_EMPTY] 2703 >> simp[extractTrans_def] >> rpt strip_tac 2704 >> fs[] 2705 >- (disj2_tac >> disj1_tac 2706 >> Q.HO_MATCH_ABBREV_TAC `A = {}` 2707 >> `!x. ~(x ��� A)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 2708 >> rpt strip_tac >> qunabbrev_tac `A` >> fs[OPTION_TO_LIST_MEM] 2709 >> metis_tac[NOT_SOME_NONE] 2710 ) 2711 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] 2712 >> metis_tac[NOT_SOME_NONE]) 2713 ) 2714 >> metis_tac[] 2715 ) 2716 >- ( 2717 Cases_on `x` 2718 >> `lookup q k.followers = lookup q g.followers` by ( 2719 qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 2720 >> `~(q = nId)` by ( 2721 fs[findNode_def] 2722 >> `(��(n,l). l.frml = a) (q,r) 2723 ��� MEM (q,r) (toAList g.nodeInfo)` 2724 by metis_tac[FIND_LEMM2] 2725 >> `(��(n,l). l.frml = (SND y).frml) (nId,frml) 2726 ��� MEM (nId,frml) (toAList g.nodeInfo)` 2727 by metis_tac[FIND_LEMM2] 2728 >> CCONTR_TAC >> rw[] >> fs[MEM_toAList] 2729 >> metis_tac[] 2730 ) 2731 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 2732 ) 2733 >> `!x1 x2 b id n. 2734 (findNode (��(n,l). l.frml = b) x1 = SOME (id,n)) 2735 ��� (findNode (��(n,l). l.frml = b) x2 = SOME (id,n)) 2736 ��� (lookup id x1.followers = lookup id x2.followers) 2737 ��� (x1.nodeInfo = x2.nodeInfo) 2738 ==> (extractTrans x1 b ��� extractTrans x2 b)` by ( 2739 simp[extractTrans_def,SUBSET_DEF] >> rpt strip_tac 2740 ) 2741 >> metis_tac[SET_EQ_SUBSET] 2742 ) 2743 ) 2744 ) 2745 >- (rpt strip_tac 2746 >> first_assum (qspec_then `h'` mp_tac) >> rpt strip_tac >> fs[] 2747 >> rename[`x_new = (SND nodeIdPair).frml`] 2748 >> Cases_on `nodeIdPair` >> fs[] 2749 >> rename [`MEM (id,node) (toAList g.nodeInfo)`] 2750 >> `findNode (��(n,l). l.frml = x_new) g = SOME (id,node)` by ( 2751 `?q1 r1. findNode (��(n,l). l.frml = x_new) g = SOME (q1,r1)` by ( 2752 `(��(n,l). l.frml = x_new) (id,node)` by fs[] 2753 >> simp[findNode_def] 2754 >> IMP_RES_TAC FIND_LEMM >> fs[] 2755 >> Cases_on `y'` >> fs[] 2756 ) 2757 >> fs[unique_node_formula_def, findNode_def] 2758 >> `MEM (q1,r1.frml) (graphStatesWithId g)` by( 2759 fs[MEM_MAP,graphStatesWithId_def] 2760 >> qexists_tac `(q1,r1)` >> fs[] 2761 >> metis_tac[FIND_LEMM2] 2762 ) 2763 >> `MEM (id,node.frml) (graphStatesWithId g)` by( 2764 fs[MEM_MAP,graphStatesWithId_def] 2765 >> qexists_tac `(id,node)` >> fs[] 2766 >> metis_tac[FIND_LEMM2] 2767 ) 2768 >> `(��(n,l). l.frml = x_new) (q1,r1)` by metis_tac[FIND_LEMM2] 2769 >> fs[] 2770 >> `q1 = id` by (rw[] >> metis_tac[]) 2771 >> rw[] >> fs[graphStatesWithId_def,MEM_MAP] 2772 >> `MEM (id,r1) (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 2773 >> `MEM (id,node) (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 2774 >> metis_tac[MEM_toAList,SOME_11] 2775 ) 2776 >> `TO_LABELS (x_new::fs) = (LABEL,id)::(TO_LABELS fs)` by ( 2777 qunabbrev_tac `TO_LABELS` 2778 >> fs[CAT_OPTIONS_def,CAT_OPTIONS_MAP_LEMM,CAT_OPTIONS_MEM, 2779 MEM_MAP,CAT_OPTIONS_APPEND] 2780 ) 2781 >> rw[] 2782 >> `���lab x. 2783 MEM (lab,x) (TO_LABELS fs) ��� 2784 ���h. MEM (x,h) (toAList g.nodeInfo) ��� lab = LABEL` 2785 by (rpt strip_tac 2786 >> `MEM (lab,x) (TO_LABELS (node.frml::fs))` by ( 2787 qunabbrev_tac `TO_LABELS` 2788 >> fs[CAT_OPTIONS_MAP_LEMM,CAT_OPTIONS_MEM,MEM_MAP] 2789 >> dsimp[] >> metis_tac[] 2790 ) 2791 >> metis_tac[] 2792 ) 2793 >> `���m. 2794 FOLDR addSingleEdge a_init (TO_LABELS fs) = SOME m 2795 ��� g.nodeInfo = m.nodeInfo ��� wfg m 2796 ��� (���a. 2797 if a = (SND y).frml then 2798 extractTrans m (SND y).frml = 2799 extractTrans g (SND y).frml 2800 ��� {(LABEL.edge_grp,l,l0,h INSERT set fs)} 2801 else extractTrans m a = extractTrans g a) 2802 ��� (���fls q r. 2803 findNode (��(n,l). l.frml = (SND y).frml) m = SOME (q,r) 2804 ��� lookup q m.followers = SOME fls 2805 ==> (���f. MEM f fls ��� (FST f).edge_grp ��� LABEL.edge_grp 2806 ��� (���o_id. o_id ��� q 2807 ��� lookup o_id m.nodeInfo = lookup o_id g.nodeInfo)))` 2808 by metis_tac[] 2809 >> qabbrev_tac `A = FOLDR addSingleEdge a_init (TO_LABELS fs)` 2810 >> `?m1. addSingleEdge (LABEL,id) A = SOME m1 2811 ��� wfg m1 ��� (m1.nodeInfo = m.nodeInfo) 2812 ��� (���fls q r. 2813 findNode (��(n,l). l.frml = (SND y).frml) m1 = SOME (q,r) 2814 ��� lookup q m1.followers = SOME fls 2815 ==> (���f. MEM f fls ��� (FST f).edge_grp ��� LABEL.edge_grp 2816 ��� (���o_id. o_id ��� q 2817 ��� lookup o_id m1.nodeInfo = lookup o_id g.nodeInfo)))` 2818 by ( 2819 qunabbrev_tac `addSingleEdge` >> fs[] 2820 >> Q.HO_MATCH_ABBREV_TAC ` 2821 ?m1. addEdge nId (LABEL,id) m = SOME m1 ��� wfg m1 2822 ��� m1.nodeInfo = m.nodeInfo ��� B m1` 2823 >> `?m1. addEdge nId (LABEL,id) m = SOME m1 2824 ��� (m1.nodeInfo = m.nodeInfo ==> B m1)` 2825 suffices_by metis_tac[addEdge_preserves_nodeInfo, 2826 addEdge_preserves_wfg] 2827 >> simp[addEdge_def] >> fs[] 2828 >> `nId ��� domain m.nodeInfo ��� id ��� domain m.nodeInfo` by ( 2829 fs[findNode_def] 2830 >> metis_tac[MEM_toAList,domain_lookup,FIND_LEMM2] 2831 ) 2832 >> fs[] 2833 >> dsimp[] 2834 >> `���followers_old preds_old. 2835 lookup nId m.followers = SOME followers_old ��� 2836 lookup id m.preds = SOME preds_old` 2837 by metis_tac[domain_lookup,wfg_def] >> simp[] 2838 >> qunabbrev_tac `B` >> rpt strip_tac >> fs[] >> rpt strip_tac 2839 >- (`(q,r) = (nId,frml)` by fs[findNode_def] 2840 >> rw[] >> fs[] 2841 >> fs[gfg_component_equality] >> rw[] >> fs[] 2842 >> metis_tac[findNode_def,SOME_11]) 2843 ) 2844 >> qexists_tac `m1` >> fs[] >> rpt strip_tac 2845 >> Cases_on `a = (SND y).frml` >> fs[] 2846 >- (first_x_assum (qspec_then `a` mp_tac) >> simp[] >> rw[] 2847 >> Q.HO_MATCH_ABBREV_TAC `M1 = G ��� {N}` 2848 >> `!x. ((x ��� M1 ��� ((FST x) = LABEL.edge_grp)) 2849 ==> (x = N)) 2850 ��� (x ��� M1 ��� ~((FST x) = LABEL.edge_grp) 2851 ==> x ��� G) 2852 ��� ((!y. (y ��� M1 ��� ((FST y) = LABEL.edge_grp)) 2853 ==> (y = N)) 2854 ==> (x ��� G \/ x = N ==> x ��� M1))` suffices_by ( 2855 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2856 >> metis_tac[IN_SING] 2857 ) 2858 >> rpt strip_tac >> qunabbrev_tac `M1` >> qunabbrev_tac `G` 2859 >> qunabbrev_tac `N` 2860 >- (qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 2861 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2862 >> simp[extractTrans_def] >> rpt strip_tac >> fs[] 2863 >- ( 2864 POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2865 >> Q.HO_MATCH_ABBREV_TAC `~(B = {}) ==> C` >> rpt strip_tac 2866 >> `?b. b ��� B` by metis_tac[MEMBER_NOT_EMPTY] 2867 >> first_x_assum (qspec_then `followers_old` mp_tac) 2868 >> rpt strip_tac >> fs[] 2869 >> `(label.edge_grp = LABEL.edge_grp) 2870 ==> (LABEL = label 2871 ��� ((LABEL = label) 2872 ==> (B = h INSERT node.frml INSERT set fs)))` 2873 suffices_by ( 2874 qunabbrev_tac `C` >> rpt strip_tac 2875 >> qunabbrev_tac `LABEL` >> rw[] 2876 >> fs[theorem "edgeLabelAA_component_equality"] >> rw[] 2877 ) 2878 >> rpt strip_tac 2879 >- (qunabbrev_tac `B` >> fs[OPTION_TO_LIST_MEM] 2880 >> `unique_node_formula m` by ( 2881 fs[unique_node_formula_def,graphStatesWithId_def] 2882 >> metis_tac[] 2883 ) 2884 >> `findNode (��(n,l). l.frml = (SND y).frml) m = SOME x'` 2885 by (fs[findNode_def] >> metis_tac[SOME_11]) 2886 >> Cases_on `x'` >> fs[] >> Cases_on `nId = q` 2887 >> rw[] >> fs[gfg_component_equality] 2888 >> rw[] >> fs[] 2889 >-(`���s. 2890 (label.edge_grp,label.pos_lab,label.neg_lab,s) 2891 ��� extractTrans m (SND y).frml ��� suc.frml ��� s` by ( 2892 `r.frml = (SND y).frml` by fs[findNode_def,FIND_LEMM] 2893 >> `lookup nId m.nodeInfo = SOME r` by ( 2894 metis_tac[FIND_LEMM2,findNode_def,MEM_toAList,SOME_11] 2895 ) 2896 >> metis_tac[EXTR_TRANS_LEMM] 2897 ) 2898 >> `(label.edge_grp,label.pos_lab,label.neg_lab,s) 2899 ��� extractTrans g (SND y).frml ��� 2900 {(LABEL.edge_grp,l,l0,h INSERT set fs)}` 2901 by metis_tac[] 2902 >> fs[IN_UNION] 2903 >- ( 2904 `label.edge_grp < LABEL.edge_grp` by metis_tac[] 2905 >> fs[]) 2906 >- ( 2907 qunabbrev_tac `LABEL` >> rw[] 2908 >> fs[theorem "edgeLabelAA_component_equality"] 2909 ) 2910 ) 2911 >- ( 2912 `lookup q m.followers = SOME l'` 2913 by metis_tac[lookup_insert] 2914 >> `���s. 2915 (label.edge_grp,label.pos_lab,label.neg_lab,s) 2916 ��� extractTrans m (SND y).frml ��� suc.frml ��� s` by ( 2917 `r.frml = (SND y).frml` by fs[findNode_def,FIND_LEMM] 2918 >> `lookup q m.nodeInfo = SOME r` by ( 2919 metis_tac[FIND_LEMM2,findNode_def,MEM_toAList] 2920 ) 2921 >> metis_tac[EXTR_TRANS_LEMM] 2922 ) 2923 >> `(label.edge_grp,label.pos_lab,label.neg_lab,s) 2924 ��� extractTrans g (SND y).frml ��� 2925 {(LABEL.edge_grp,l,l0,h INSERT set fs)}` 2926 by metis_tac[] 2927 >> fs[IN_UNION] 2928 >- (`label.edge_grp < LABEL.edge_grp` by metis_tac[] 2929 >> fs[]) 2930 >- (qunabbrev_tac `LABEL` >> rw[] 2931 >> fs[theorem "edgeLabelAA_component_equality"] 2932 ) 2933 ) 2934 ) 2935 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> conj_tac 2936 >> qunabbrev_tac `B` >> fs[OPTION_TO_LIST_MEM] 2937 >- (rpt strip_tac >> rename[`_ x1 = SOME l1`] 2938 >> `x1 = (nId,frml)` by 2939 (fs[findNode_def] >> rw[] >> fs[]) 2940 >> rw[] >> fs[] >> rw[] 2941 >> `(LABEL,sucId') = (LABEL,id) 2942 \/ (MEM (LABEL,sucId') followers_old)` by fs[] 2943 >- (rw[] 2944 >> `suc' = node` 2945 by metis_tac[findNode_def,FIND_LEMM2, 2946 MEM_toAList,SOME_11] 2947 >> fs[] 2948 ) 2949 >- ( 2950 `���s. 2951 (LABEL.edge_grp,LABEL.pos_lab,LABEL.neg_lab,s) 2952 ��� extractTrans m (SND y).frml ��� suc'.frml ��� s` by ( 2953 `unique_node_formula m` by ( 2954 fs[unique_node_formula_def,graphStatesWithId_def] 2955 >> metis_tac[] 2956 ) 2957 >> `lookup nId m.nodeInfo = SOME frml` 2958 by metis_tac[findNode_def,FIND_LEMM2, 2959 MEM_toAList,SOME_11] 2960 >> `frml.frml = (SND y).frml` by fs[] 2961 >> metis_tac[EXTR_TRANS_LEMM] 2962 ) 2963 >> `(LABEL.edge_grp,LABEL.pos_lab,LABEL.neg_lab,s) 2964 ��� extractTrans g (SND y).frml ��� 2965 {(LABEL.edge_grp,l,l0,h INSERT set fs)}` 2966 by metis_tac[] 2967 >> fs[IN_UNION] >> fs[] 2968 >> `LABEL.edge_grp < LABEL.edge_grp` by metis_tac[] 2969 >> fs[] 2970 ) 2971 ) 2972 >- ( 2973 rename[`_ x1 = SOME l1`] 2974 >> `x1 = (nId,frml)` by 2975 (fs[findNode_def] >> rw[] >> fs[]) 2976 >> `(LABEL.edge_grp,l,l0,h INSERT set fs) 2977 ��� extractTrans m (SND y).frml` by fs[] 2978 >> POP_ASSUM mp_tac 2979 >> PURE_REWRITE_TAC[extractTrans_def] >> fs[] 2980 >> rpt strip_tac >> rw[] 2981 >> `LABEL = label'` by ( 2982 qunabbrev_tac `LABEL` 2983 >> fs[theorem "edgeLabelAA_component_equality"] 2984 ) >> rw[] 2985 >- ( 2986 POP_ASSUM mp_tac >> POP_ASSUM mp_tac 2987 >> Q.HO_MATCH_ABBREV_TAC ` 2988 h INSERT set fs = A ==> B` 2989 >> strip_tac >> `h ��� A` by metis_tac[IN_INSERT] 2990 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 2991 >> fs[OPTION_TO_LIST_MEM] >> rw[] >> fs[] 2992 >> `x' = (nId,frml)` by fs[findNode_def] 2993 >> rw[] >> fs[] >> rw[] >> metis_tac[] 2994 ) 2995 >- ( 2996 qexists_tac `node` >> fs[] >> qexists_tac `id` >> fs[] 2997 >> rw[] >> fs[] 2998 >> metis_tac[MEM_toAList,SOME_11] 2999 ) 3000 >- ( 3001 POP_ASSUM mp_tac >> POP_ASSUM mp_tac 3002 >> POP_ASSUM mp_tac 3003 >> Q.HO_MATCH_ABBREV_TAC ` 3004 h INSERT set fs = A ==> MEM x' fs ==> B` 3005 >> strip_tac >> strip_tac 3006 >> `set fs ��� A` 3007 by metis_tac[INSERT_SING_UNION,SUBSET_UNION] 3008 >> `x' ��� A` by metis_tac[SUBSET_DEF,MEM] 3009 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 3010 >> fs[OPTION_TO_LIST_MEM] >> rw[] >> fs[] 3011 >> `x'' = (nId,frml)` by fs[findNode_def] 3012 >> rw[] >> fs[] >> rw[] >> metis_tac[] 3013 ) 3014 ) 3015 ) 3016 ) 3017 >- (qunabbrev_tac `LABEL` 3018 >> fs[theorem "edgeLabelAA_component_equality"] 3019 >> `FST x = 0` by (Cases_on `x` >> fs[]) 3020 >> fs[] 3021 ) 3022 ) 3023 >- (`x ��� extractTrans m (SND y).frml` by ( 3024 POP_ASSUM mp_tac >> POP_ASSUM mp_tac 3025 >> PURE_REWRITE_TAC[extractTrans_def] >> simp[] 3026 >> fs[] 3027 >> rpt strip_tac 3028 >- ( 3029 disj1_tac >> qexists_tac `label` >> fs[] 3030 >> Q.HO_MATCH_ABBREV_TAC `~(A = {}) ��� B = A` 3031 >> `B = A` suffices_by metis_tac[] 3032 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 3033 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 3034 >> fs[OPTION_TO_LIST_MEM] 3035 >> qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 3036 >> `x'' = (nId,frml)` 3037 by metis_tac[findNode_def,SOME_11] 3038 >> rw[] >> fs[] >> rw[] 3039 >> qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 3040 >> fs[gfg_component_equality] >> rw[] 3041 >- (qexists_tac `followers_old` >> fs[] >> rw[] 3042 >- (qexists_tac `(nId,frml)` >> fs[] 3043 >> metis_tac[findNode_def,SOME_11] 3044 ) 3045 >- (`l' = (LABEL,id)::followers_old` 3046 by metis_tac[lookup_insert,SOME_11] 3047 >> fs[] >> rw[] 3048 ) 3049 ) 3050 >- (qexists_tac `(LABEL,id)::l'` >> fs[] 3051 >> qexists_tac `(nId,frml)` >> fs[] >> rw[] 3052 >- metis_tac[findNode_def,SOME_11] 3053 >- metis_tac[lookup_insert,SOME_11] 3054 ) 3055 ) 3056 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] >> qexists_tac `l'` 3057 >> fs[] >> qexists_tac `l''` >> fs[] 3058 >> `x' = (nId,frml)` 3059 by metis_tac[findNode_def,SOME_11] 3060 >> rw[] >> fs[] >> rw[] >> qexists_tac `(nId,frml)` 3061 >> fs[] >> fs[findNode_def] 3062 ) 3063 ) 3064 >> `x ��� extractTrans g (SND y).frml ��� 3065 {(LABEL.edge_grp,l,l0,h INSERT set fs)}` by metis_tac[] 3066 >> fs[IN_UNION] >> Cases_on `x` >> rw[] >> fs[] 3067 ) 3068 >- (`x ��� extractTrans m (SND y).frml` 3069 by metis_tac[UNION_SUBSET,SUBSET_DEF] 3070 >> `FST x < LABEL.edge_grp` by ( 3071 Cases_on `x` >> Cases_on `r` >> Cases_on `r'` >> fs[] 3072 >> metis_tac[] 3073 ) 3074 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 3075 >> PURE_REWRITE_TAC[extractTrans_def] >> fs[] >> rpt strip_tac 3076 >- (disj1_tac >> qexists_tac `label` >> fs[] 3077 >> Q.HO_MATCH_ABBREV_TAC `~(A = {}) ��� B = A` 3078 >> `B = A` suffices_by metis_tac[] 3079 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 3080 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 3081 >> fs[OPTION_TO_LIST_MEM] 3082 >> qexists_tac `suc` >> fs[] >> qexists_tac `sucId` >> fs[] 3083 >> qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 3084 >> rw[] >> fs[] >> rw[] 3085 >- ( 3086 `x'' = (nId,frml)` 3087 by metis_tac[findNode_def,SOME_11] 3088 >> rw[] >> qexists_tac `(LABEL,id)::followers_old` 3089 >> fs[] >> rw[] 3090 >> qexists_tac `(nId,frml)` >> fs[gfg_component_equality] 3091 >> simp[findNode_def] >> metis_tac[findNode_def] 3092 ) 3093 >- (`x'' = (nId,frml)` 3094 by (Cases_on `x''` >> fs[findNode_def]) 3095 >> rw[] >> qexists_tac `followers_old` 3096 >> fs[] >> rw[] 3097 >- (qexists_tac `(nId,frml)` 3098 >> fs[gfg_component_equality] 3099 >> simp[findNode_def] >> metis_tac[findNode_def]) 3100 >- (fs[] >> rw[] >> fs[]) 3101 ) 3102 ) 3103 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] >> qexists_tac `l'` 3104 >> fs[] >> qexists_tac `l''` >> fs[] 3105 >> `x' = (nId,frml)` 3106 by metis_tac[findNode_def,SOME_11] 3107 >> rw[] >> fs[] >> rw[] >> qexists_tac `(nId,frml)` 3108 >> fs[] >> fs[findNode_def]>> fs[] 3109 ) 3110 ) 3111 >- (qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 3112 >> `unique_node_formula m1` by ( 3113 fs[unique_node_formula_def,graphStatesWithId_def] 3114 >> metis_tac[] 3115 ) 3116 >> `?suc. lookup id m1.nodeInfo = SOME suc` 3117 by metis_tac[domain_lookup] 3118 >> `MEM (LABEL,id) ((LABEL,id)::followers_old)` by fs[] 3119 >> `0 < LABEL.edge_grp` by ( 3120 qunabbrev_tac `LABEL` 3121 >> fs[theorem "edgeLabelAA_component_equality"] 3122 >> Cases_on `v` >> fs[] 3123 ) 3124 >> `lookup nId m1.followers = SOME ((LABEL,id)::followers_old)` 3125 by (fs[gfg_component_equality] >> metis_tac[lookup_insert]) 3126 >> `?suc. lookup id m1.nodeInfo = SOME suc` 3127 by metis_tac[domain_lookup] 3128 >> `lookup nId m1.nodeInfo = SOME frml` 3129 by metis_tac[findNode_def,MEM_toAList,SOME_11,FIND_LEMM2] 3130 >> `���s. 3131 (LABEL.edge_grp,LABEL.pos_lab,LABEL.neg_lab,s) ��� 3132 extractTrans m1 (SND y).frml ��� suc'.frml ��� s` 3133 by metis_tac[EXTR_TRANS_LEMM] 3134 >> first_x_assum 3135 (qspec_then `(LABEL.edge_grp,LABEL.pos_lab,LABEL.neg_lab,s)` 3136 mp_tac) 3137 >> simp[] >> qunabbrev_tac `LABEL` >> rpt strip_tac 3138 >> fs[theorem "edgeLabelAA_component_equality"] 3139 ) 3140 ) 3141 >- (`extractTrans m1 a = extractTrans m a` suffices_by metis_tac[] 3142 >> `findNode (��(n,l). l.frml = a) m1 3143 = findNode (��(n,l). l.frml = a) m` by fs[findNode_def] 3144 >> Cases_on `findNode (��(n,l). l.frml = a) m` >> fs[] 3145 >- ( 3146 `!x b. (findNode (��(n,l). l.frml = b) x = NONE) 3147 ==> (extractTrans x b = {})` by ( 3148 rpt strip_tac 3149 >> `!q. ~ (q ��� extractTrans x b)` 3150 suffices_by metis_tac[MEMBER_NOT_EMPTY] 3151 >> simp[extractTrans_def] >> rpt strip_tac 3152 >> fs[] 3153 >- (disj2_tac >> disj1_tac 3154 >> Q.HO_MATCH_ABBREV_TAC `B = {}` 3155 >> `!x. ~(x ��� B)` suffices_by metis_tac[MEMBER_NOT_EMPTY] 3156 >> rpt strip_tac >> qunabbrev_tac `B` >> fs[OPTION_TO_LIST_MEM] 3157 >> metis_tac[NOT_SOME_NONE] 3158 ) 3159 >- (disj2_tac >> fs[OPTION_TO_LIST_MEM] 3160 >> metis_tac[NOT_SOME_NONE]) 3161 ) 3162 >> metis_tac[] 3163 ) 3164 >- ( 3165 Cases_on `x` 3166 >> `lookup q m1.followers = lookup q m.followers` by ( 3167 qunabbrev_tac `addSingleEdge` >> fs[addEdge_def] 3168 >> `~(q = nId)` by ( 3169 fs[findNode_def] 3170 >> `(��(n,l). l.frml = a) (q,r) 3171 ��� MEM (q,r) (toAList m.nodeInfo)` 3172 by metis_tac[FIND_LEMM2] 3173 >> `(��(n,l). l.frml = (SND y).frml) (nId,frml) 3174 ��� MEM (nId,frml) (toAList m.nodeInfo)` 3175 by metis_tac[FIND_LEMM2] 3176 >> CCONTR_TAC >> rw[] >> fs[MEM_toAList] 3177 >> metis_tac[] 3178 ) 3179 >> fs[gfg_component_equality] >> metis_tac[lookup_insert] 3180 ) 3181 >> `!x1 x2 b id n. 3182 (findNode (��(n,l). l.frml = b) x1 = SOME (id,n)) 3183 ��� (findNode (��(n,l). l.frml = b) x2 = SOME (id,n)) 3184 ��� (lookup id x1.followers = lookup id x2.followers) 3185 ��� (x1.nodeInfo = x2.nodeInfo) 3186 ==> (extractTrans x1 b ��� extractTrans x2 b)` by ( 3187 simp[extractTrans_def,SUBSET_DEF] >> rpt strip_tac 3188 ) 3189 >> metis_tac[SET_EQ_SUBSET] 3190 ) 3191 ) 3192 ) 3193 ) 3194 >> first_x_assum (qspec_then `t` mp_tac) >> simp[] 3195 >> `���lab x. 3196 MEM (lab,x) (TO_LABELS t) ��� 3197 ���h. MEM (x,h) (toAList g.nodeInfo) ��� lab = LABEL` by ( 3198 rpt strip_tac >> fs[] >> qunabbrev_tac `TO_LABELS` >> fs[] 3199 >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM,CAT_OPTIONS_MEM] >> rw[] 3200 >> Cases_on `y'` >> metis_tac[FIND_LEMM2] 3201 ) 3202 >> simp[] >> rpt strip_tac >> qexists_tac `m` >> qunabbrev_tac `Q` 3203 >> fs[] 3204 >> Q.HO_MATCH_ABBREV_TAC `A ��� B ��� C` 3205 >> `A ��� (A ==> B) ��� C` suffices_by fs[] 3206 >> qunabbrev_tac `A` >> qunabbrev_tac `B` >> qunabbrev_tac `C` 3207 >> fs[] >> rpt strip_tac 3208 >- simp[graphStatesWithId_def,MEM_MAP] 3209 >- (fs[unique_node_formula_def] >> metis_tac[]) 3210 >- (first_x_assum (qspec_then `h'` mp_tac) >> fs[] 3211 >> Cases_on `h' = (SND y).frml` >> fs[] >> rpt strip_tac 3212 >> qexists_tac `LABEL.edge_grp` 3213 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 3214 ) 3215 ) 3216QED 3217 3218val ADDEDGE_FOLDR_LEMM = store_thm 3219 ("ADDEDGE_FOLDR_LEMM", 3220 ``!g1 f. MEM f (graphStates g1) 3221 ��� wfg g1 3222 ��� unique_node_formula g1 3223 ��� flws_sorted g1 3224 ==> 3225 (!ls. ?g2. 3226 (!e suc. MEM e ls ��� MEM suc e.sucs 3227 ==> MEM suc (graphStates g1)) 3228 ==> ((FOLDR (��e g_opt. monad_bind g_opt (addEdgeToGraph f e)) 3229 (SOME g1) ls = SOME g2) 3230 ��� (wfg g2) 3231 ��� flws_sorted g2 3232 ��� (unique_node_formula g2) 3233 ��� (set (graphStatesWithId g1) 3234 = set (graphStatesWithId g2))) 3235 ��� (!h. if h = f 3236 then IMAGE SND (extractTrans g2 h) = 3237 IMAGE SND (extractTrans g1 h) 3238 ��� { (e.pos,e.neg,set e.sucs) | MEM e ls} 3239 else extractTrans g2 h = extractTrans g1 h))``, 3240 strip_tac >> strip_tac >> strip_tac 3241 >> Induct_on `ls` >> fs[] >> strip_tac 3242 >> Q.HO_MATCH_ABBREV_TAC `?g. A ==> ((?x. B g x) ��� C g) ��� D g` 3243 >> `A ==> ?x g. B g x ��� C g ��� D g` suffices_by metis_tac[] 3244 >> rpt strip_tac >> qunabbrev_tac `A` 3245 >> `FOLDR (��e g_opt. monad_bind g_opt (addEdgeToGraph f e)) 3246 (SOME g1) ls = SOME g2 ��� wfg g2 3247 ��� (set (graphStatesWithId g1) 3248 = set (graphStatesWithId g2)) 3249 ��� unique_node_formula g2 3250 ��� flws_sorted g2 3251 ��� ���h. 3252 if h = f then 3253 IMAGE SND (extractTrans g2 f) = 3254 IMAGE SND (extractTrans g1 f) ��� 3255 {(e.pos,e.neg,set e.sucs) | MEM e ls} 3256 else extractTrans g2 h = extractTrans g1 h` by metis_tac[] 3257 >> qunabbrev_tac `B` >> qunabbrev_tac `C` >> qunabbrev_tac `D` >> fs[] 3258 >> `MEM f (graphStates g2)` by ( 3259 fs[graphStates_def,MEM_MAP] >> Cases_on `y` 3260 >> `MEM (q,r.frml) (graphStatesWithId g1)` 3261 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 3262 >> POP_ASSUM mp_tac >> simp[graphStatesWithId_def,MEM_MAP] 3263 >> rpt strip_tac >> qexists_tac `y` >> Cases_on `y` >> fs[] 3264 ) 3265 >> `set (graphStates g1) = set (graphStates g2)` 3266 by metis_tac[GRAPH_STATES_ID_IMP_GRAPH_STATES] 3267 >> `!x. MEM x h.sucs ==> MEM x (graphStates g2)` 3268 by metis_tac[] 3269 >> `���g3. 3270 addEdgeToGraph f h g2 = SOME g3 ��� wfg g3 ��� 3271 set (graphStatesWithId g2) = set (graphStatesWithId g3) ��� 3272 unique_node_formula g3 ��� 3273 (���x. 3274 if x = f then 3275 ���i. 3276 extractTrans g3 x = 3277 extractTrans g2 x ��� {(i,h.pos,h.neg,set h.sucs)} 3278 else extractTrans g3 x = extractTrans g2 x)` 3279 by metis_tac[ADDEDGE_LEMM] 3280 >> `flws_sorted g3` by metis_tac[ADDEDGE_COUNTER_LEMM] 3281 >> qexists_tac `g3` >> fs[] >> rpt strip_tac >> Cases_on `h' = f` >> fs[] 3282 >- (rw[] >> first_x_assum (qspec_then `f` mp_tac) >> simp[] >> rpt strip_tac 3283 >> `IMAGE SND (extractTrans g2 f ��� {(i,h.pos,h.neg,set h.sucs)}) 3284 = IMAGE SND (extractTrans g1 f) ��� 3285 {(e.pos,e.neg,set e.sucs) | e = h ��� MEM e ls}` 3286 suffices_by metis_tac[] 3287 >> rw[IMAGE_UNION] 3288 >> `IMAGE SND (extractTrans g1 f) ��� 3289 {(e.pos,e.neg,set e.sucs) | MEM e ls} ��� {(h.pos,h.neg,set h.sucs)} 3290 = IMAGE SND (extractTrans g1 f) ��� 3291 {(e.pos,e.neg,set e.sucs) | e = h ��� MEM e ls}` 3292 suffices_by metis_tac[] 3293 >> PURE_REWRITE_TAC[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 3294 >- (Cases_on `x ��� IMAGE SND (extractTrans g1 f)` 3295 >- metis_tac[IN_UNION] 3296 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> PURE_REWRITE_TAC[IN_UNION] 3297 >> dsimp[] 3298 ) 3299 ) 3300 >- (Cases_on `x ��� IMAGE SND (extractTrans g1 f)` 3301 >- metis_tac[IN_UNION] 3302 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> PURE_REWRITE_TAC[IN_UNION] 3303 >> dsimp[] >> rpt strip_tac >> fs[] 3304 >> metis_tac[]) 3305 ) 3306 ) 3307 >- metis_tac[] 3308 ); 3309 3310val _ = export_theory (); 3311