1open HolKernel Parse bossLib boolLib gfgTheory listTheory optionTheory pred_setTheory relationTheory pairTheory prim_recTheory set_relationTheory arithmeticTheory rich_listTheory 2 3open sptreeTheory ltlTheory generalHelpersTheory concrGBArepTheory concrRepTheory waa2baTheory buechiATheory gbaSimplTheory alterATheory ltl2waaTheory waaSimplTheory concrltl2waaTheory 4 5val _ = new_theory "concrwaa2gba" 6 7val _ = Cond_rewr.stack_limit := 2 8 9val _ = monadsyntax.temp_add_monadsyntax(); 10val _ = overload_on("monad_bind",``OPTION_BIND``); 11 12 13val get_acc_set_def = Define` 14 get_acc_set acc ce = 15 CAT_OPTIONS (MAP (��(f,f_trans). 16 if acc_cond_concr ce f f_trans 17 then SOME f 18 else NONE 19 ) acc 20 )`; 21 22val GET_ACC_SET_LEMM = store_thm 23 ("GET_ACC_SET_LEMM", 24 ``!acc ce1 ce2. 25 (MEM_EQUAL ce1.pos ce2.pos) 26 ��� (MEM_EQUAL ce1.neg ce2.neg) 27 ��� (MEM_EQUAL ce1.sucs ce2.sucs) 28 ==> (get_acc_set acc ce1 = get_acc_set acc ce2)``, 29 rpt strip_tac >> fs[get_acc_set_def] 30 >> `!f f_tr. acc_cond_concr ce1 f f_tr = acc_cond_concr ce2 f f_tr` 31 suffices_by metis_tac[] 32 >> rpt strip_tac >> Cases_on `ce1` >> Cases_on `ce2` 33 >> simp[acc_cond_concr_def,trns_is_empty_def] 34 >> fs[concrEdge_component_equality] 35 >> simp[MEM_SUBSET_SET_TO_LIST,MEM_EQUAL_SET,EXISTS_MEM] 36 >> fs[MEM_EQUAL_SET] >> rw[] 37 ); 38 39val valid_acc_def = Define` 40 valid_acc aP g_AA acc = 41 ((!f f_trns. MEM (f,f_trns) acc ==> 42 ?id nL. (findNode (��(i,l). l.frml = f) g_AA = SOME (id,nL)) 43 ��� (SOME f_trns = concr_extrTrans g_AA id) 44 ��� (!ce. MEM ce f_trns ==> 45 (set ce.pos ��� set aP ��� set ce.neg ��� set aP) 46 ) 47 ��� is_until f 48 ) 49 ��� (!f. (is_until f ��� MEM f (graphStates g_AA)) 50 ==> ?f_trns. MEM (f,f_trns) acc))`; 51 52val VALID_ACC_LEMM = store_thm 53 ("VALID_ACC_LEMM", 54 ``!aP acc g_AA. valid_acc aP g_AA acc ��� until_iff_final g_AA 55 ==> !f. MEM f (MAP FST acc) ��� f ��� concr2Abstr_final g_AA``, 56 simp[EQ_IMP_THM] >> fs[valid_acc_def,concr2Abstr_final_def] >> rpt strip_tac 57 >> fs[MEM_MAP] 58 >- (Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (f,f_trns) acc`] 59 >> `���id nL. 60 (findNode (��(i,l). l.frml = f) g_AA = SOME (id,nL)) 61 ��� (SOME f_trns = concr_extrTrans g_AA id) 62 ��� (���ce. 63 MEM ce f_trns ��� 64 set ce.pos ��� set aP ��� set ce.neg ��� set aP) 65 ��� is_until f` by metis_tac[] 66 >> qexists_tac `nL` 67 >> `(MEM (id,nL) (toAList g_AA.nodeInfo)) 68 ��� ((��(i,l). l.frml = f) (id,nL))` by metis_tac[FIND_LEMM2,findNode_def] 69 >> fs[until_iff_final_def] 70 >> first_x_assum (qspec_then `id` mp_tac) >> strip_tac 71 >> first_x_assum (qspec_then `nL` mp_tac) 72 >> `lookup id g_AA.nodeInfo = SOME nL` by metis_tac[MEM_toAList,SOME_11] 73 >> simp[] 74 >> `(���f1 f2. f = U f1 f2)` by (Cases_on `f` >> fs[is_until_def]) >> simp[] 75 >> metis_tac[MEM_toAList,domain_lookup] 76 ) 77 >- (`is_until f` by ( 78 simp[is_until_def] >> fs[until_iff_final_def] 79 >> `���f1 f2. x.frml = U f1 f2` by metis_tac[] 80 >> Cases_on `x` >> simp[is_until_def] 81 ) 82 >> `MEM f (graphStates g_AA)` by ( 83 simp[graphStates_def,MEM_MAP] >> qexists_tac `(n,x)` >> fs[] 84 >> metis_tac[MEM_toAList] 85 ) 86 >> first_x_assum (qspec_then `f` mp_tac) >> simp[] >> strip_tac 87 >> metis_tac[FST] 88 ) 89 ); 90 91val CONCR_ACC_SETS = store_thm 92 ("CONCR_ACC_SETS", 93 ``!h g_AA init acc aP abstrAA. 94 (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 95 ��� (abstrAA = removeStatesSimpl (ltl2vwaa h)) 96 ��� valid_acc aP g_AA acc 97 ��� wfg g_AA ��� flws_sorted g_AA ��� unique_node_formula g_AA 98 ==> 99 !ce u aE. 100 (aE = concr2AbstractEdge (set aP) ce) 101 ��� is_until u ��� MEM u (graphStates g_AA) 102 ��� MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP 103 ��� MEM_SUBSET ce.sucs (graphStates g_AA) 104 ==> 105 (!qs2. qs2 ��� POW abstrAA.states 106 ==> (MEM u (get_acc_set acc ce) = 107 ((qs2,FST aE,SND aE) ��� acc_cond abstrAA u)))``, 108 fs[] >> rpt strip_tac >> simp[EQ_IMP_THM] >> rpt strip_tac 109 >> fs[CAT_OPTIONS_MEM,MEM_MAP] 110 >> qabbrev_tac `aa_red = removeStatesSimpl (ltl2vwaa h)` 111 >> `(aa_red).alphabet = POW (set aP)` 112 by fs[concr2AbstrAA_def,ALTER_A_component_equality] 113 >> `isValidAlterA (aa_red)` by ( 114 metis_tac[LTL2WAA_ISVALID,REDUCE_STATE_IS_VALID] 115 ) 116 >- ( 117 simp[acc_cond_def] >> qexists_tac `FST (concr2AbstractEdge (set aP) ce)` 118 >> qexists_tac `SND (concr2AbstractEdge (set aP) ce)` >> fs[] 119 >> rpt strip_tac 120 >- (simp[IN_POW,SUBSET_DEF] >> rpt strip_tac >> fs[] 121 >> Cases_on `ce` >> fs[concr2AbstractEdge_def] 122 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 123 >> fs[concr2Abstr_states_def,graphStates_def] 124 >> `MEM x (MAP ((��l. l.frml) ��� SND) (toAList g_AA.nodeInfo))` 125 by metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 126 >> `x ��� {x.frml | 127 ���n. (SOME x = lookup n g_AA.nodeInfo) 128 ��� (n ��� domain g_AA.nodeInfo)}` suffices_by metis_tac[] 129 >> fs[MEM_MAP] >> qexists_tac `(SND y')` >> fs[] 130 >> Cases_on `y'` >> fs[] 131 >> metis_tac[MEM_toAList,domain_lookup] 132 ) 133 >- (simp[IN_POW,SUBSET_DEF] >> rpt strip_tac 134 >> Cases_on `ce` >> fs[concr2AbstractEdge_def] 135 >> metis_tac[TRANSFORMLABEL_AP,IN_POW,SUBSET_DEF] 136 ) 137 >- (Cases_on `u ��� SND (concr2AbstractEdge (set aP) ce)` 138 >> fs[get_acc_set_def,CAT_OPTIONS_MEM,MEM_MAP] 139 >> Cases_on `y` >> fs[] >> rw[] 140 >> rename[`MEM (f,f_trns) acc`] >> fs[acc_cond_concr_def] 141 >- (Cases_on `ce` >> fs[concr2AbstractEdge_def]) 142 >- (fs[valid_acc_def] 143 >> Cases_on `EXISTS (��p. MEM p ce.neg) ce.pos` >> fs[] 144 >> `���id nL. 145 (findNode (��(i,l). l.frml = f) g_AA = SOME (id,nL)) 146 ��� (SOME f_trns = concr_extrTrans g_AA id)` by metis_tac[] 147 >> `���n cT. 148 (concr_extrTrans g_AA id = SOME cT) 149 ��� (lookup id g_AA.nodeInfo = SOME n) 150 ��� (set (MAP (concr2AbstractEdge (set aP)) cT)) = 151 concrTrans g_AA (set aP) n.frml` by ( 152 `?fls. lookup id g_AA.followers = SOME fls` by ( 153 `id ��� domain g_AA.nodeInfo` by ( 154 fs[findNode_def] 155 >> metis_tac[FIND_LEMM2,MEM_toAList,domain_lookup] 156 ) 157 >> metis_tac[wfg_def,domain_lookup] 158 ) 159 >> IMP_RES_TAC CONCR_EXTRTRANS_LEMM 160 >> first_x_assum (qspec_then `id` mp_tac) >> simp[] 161 ) 162 >> fs[] >> simp[concr2AbstrAA_def] 163 >> `(n = nL) ��� (n.frml = f)` by ( 164 fs[findNode_def] 165 >> `(n = nL) ��� ((��(i,l). l.frml = f) (id,n))` suffices_by fs[] 166 >> metis_tac[FIND_LEMM2,MEM_toAList,SOME_11] 167 ) 168 >> rw[] 169 >- (fs[EXISTS_MEM,trns_is_empty_def] 170 >> `concr2AbstractEdge (set aP) cE1 ��� 171 concrTrans g_AA (set aP) n.frml` by ( 172 metis_tac[MEM_MAP] 173 ) 174 >> Cases_on `concr2AbstractEdge (set aP) cE1` >> fs[] 175 >> rename[`_ = (a,e)`] 176 >> qexists_tac `a` >> qexists_tac `e` >> Cases_on `cE1` 177 >> fs[concr2AbstractEdge_def] >> rpt strip_tac 178 >- (`FST (concr2AbstractEdge (set aP) ce) = {}` suffices_by fs[] 179 >> Cases_on `ce` >> fs[concr2AbstractEdge_def] 180 >> rename[`transformLabel (set aP) pos neg`] 181 >> `set pos ��� set neg ��� ���` 182 suffices_by metis_tac[TRANSFORMLABEL_EMPTY, 183 MEM_SUBSET_SET_TO_LIST] 184 >> `?x. x ��� set pos ��� x ��� set neg` 185 suffices_by metis_tac[IN_INTER,MEMBER_NOT_EMPTY] 186 >> metis_tac[MEM] 187 ) 188 >- (Cases_on `ce` >> fs[concr2AbstractEdge_def] 189 >> metis_tac[MEM_SUBSET_SET_TO_LIST]) 190 ) 191 >- (fs[trns_is_empty_def] 192 >> `EXISTS 193 (��cE1. 194 MEM_SUBSET cE1.pos ce.pos ��� MEM_SUBSET cE1.neg ce.neg ��� 195 MEM_SUBSET cE1.sucs ce.sucs ��� ��MEM n.frml cE1.sucs) cT` 196 by metis_tac[NOT_EXISTS] 197 >> fs[EXISTS_MEM] 198 >> `concr2AbstractEdge (set aP) cE1 ��� 199 concrTrans g_AA (set aP) n.frml` by ( 200 metis_tac[MEM_MAP] 201 ) 202 >> Cases_on `concr2AbstractEdge (set aP) cE1` >> fs[] 203 >> rename[`_ = (a,e)`] >> qexists_tac `a` >> qexists_tac `e` 204 >> fs[] >> rpt strip_tac >> Cases_on `ce` >> Cases_on `cE1` 205 >> fs[concr2AbstractEdge_def] 206 >- metis_tac[TRANSFORMLABEL_SUBSET] 207 >- metis_tac[MEM_SUBSET_SET_TO_LIST] 208 ) 209 ) 210 ) 211 ) 212 >- (simp[get_acc_set_def,CAT_OPTIONS_MEM,MEM_MAP] 213 >> fs[valid_acc_def] 214 >> `?u_trns. MEM (u,u_trns) acc` by metis_tac[] 215 >> qexists_tac `(u,u_trns)` >> fs[] >> simp[acc_cond_concr_def] 216 >> fs[acc_cond_def] 217 >- (disj1_tac >> Cases_on `ce` >> fs[concr2AbstractEdge_def]) 218 >- (Cases_on `MEM u ce.sucs` >> fs[] 219 >> Cases_on `EXISTS (��p. MEM p ce.neg) ce.pos` >> fs[] 220 >> `���id nL. 221 (findNode (��(i,l). l.frml = u) g_AA = SOME (id,nL)) 222 ��� (SOME u_trns = concr_extrTrans g_AA id)` by metis_tac[] 223 >> `���n cT. 224 (concr_extrTrans g_AA id = SOME cT) 225 ��� (lookup id g_AA.nodeInfo = SOME n) 226 ��� (set (MAP (concr2AbstractEdge (set aP)) cT) 227 = concrTrans g_AA (set aP) n.frml)` by ( 228 `?fls. lookup id g_AA.followers = SOME fls` by ( 229 `id ��� domain g_AA.nodeInfo` by ( 230 fs[findNode_def] 231 >> metis_tac[FIND_LEMM2,MEM_toAList,domain_lookup] 232 ) 233 >> metis_tac[wfg_def,domain_lookup] 234 ) 235 >> IMP_RES_TAC CONCR_EXTRTRANS_LEMM 236 >> first_x_assum (qspec_then `id` mp_tac) >> simp[] 237 ) 238 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 239 >> `(n = nL) ��� (n.frml = u)` by ( 240 fs[findNode_def] 241 >> `(n = nL) ��� ((��(i,l). l.frml = u) (id,n))` suffices_by fs[] 242 >> metis_tac[FIND_LEMM2,MEM_toAList,SOME_11] 243 ) 244 >> rw[] >> rename[`(��,sucs) ��� aa_red.trans n.frml`] 245 >> `(��,sucs) ��� set (MAP (concr2AbstractEdge (set aP)) cT)` 246 by metis_tac[] 247 >> POP_ASSUM mp_tac >> simp[MEM_MAP] >> rpt strip_tac 248 >> fs[EXISTS_MEM] 249 >> `set y.pos ��� set aP ��� set y.neg ��� set aP` by metis_tac[] 250 >> qexists_tac `y` >> fs[] >> Cases_on `ce` >> Cases_on `y` 251 >> fs[concr2AbstractEdge_def, MEM_SUBSET_SET_TO_LIST] 252 >> `a ��� ��` by rw[] 253 >> `~(a = {})` by ( 254 fs[trns_is_empty_def,EVERY_MEM] 255 >> `set l ��� set l0 = {}` by ( 256 PURE_REWRITE_TAC[SET_EQ_SUBSET,SUBSET_DEF,IN_INTER] 257 >> rpt strip_tac >> metis_tac[MEMBER_NOT_EMPTY] 258 ) 259 >> metis_tac[TRANSFORMLABEL_EMPTY] 260 ) 261 >> `MEM_SUBSET l' l ��� MEM_SUBSET l0' l0` 262 suffices_by metis_tac[MEM_SUBSET_SET_TO_LIST] 263 >> rw[] 264 >> `���x. MEM x l ��� MEM x l' ��� MEM x l0 ��� MEM x l0' 265 ��� x ��� set aP` suffices_by metis_tac[TRANSFORMLABEL_SUBSET2] 266 >> rpt strip_tac >> metis_tac[SUBSET_DEF,MEM] 267 ) 268 ) 269 ); 270 271val TLG_CONCR_LEMM = store_thm 272 ("TLG_CONCR_LEMM", 273 ``!h g_AA init aP acc qs ce1 ce2 abstrAA. 274 (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 275 ��� (abstrAA = removeStatesSimpl (ltl2vwaa h)) 276 ��� valid_acc aP g_AA acc 277 ��� wfg g_AA ��� flws_sorted g_AA ��� unique_node_formula g_AA 278 ��� (qs ��� POW abstrAA.states) 279 ��� (!id cT. (concr_extrTrans g_AA id = SOME cT) 280 ==> (!ce. MEM ce cT ==> (MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)) 281 ) 282 ==> 283 !e1_lab e1_sucs e2_lab e2_sucs. 284 MEM_SUBSET ce1.pos aP ��� MEM_SUBSET ce1.neg aP 285 ��� MEM_SUBSET ce1.sucs (graphStates g_AA) 286 ��� MEM_SUBSET ce2.pos aP ��� MEM_SUBSET ce2.neg aP 287 ��� MEM_SUBSET ce2.sucs (graphStates g_AA) 288 ��� ((e1_lab,e1_sucs) = concr2AbstractEdge (set aP) ce1) 289 ��� ((e2_lab,e2_sucs) = concr2AbstractEdge (set aP) ce2) 290 ==> 291 ((((e1_lab,e1_sucs),e2_lab,e2_sucs) ��� 292 tr_less_general { acc_cond abstrAA f | MEM f (MAP FST acc) } qs) = 293 (tlg_concr (ce1,get_acc_set acc ce1) (ce2,get_acc_set acc ce2)))``, 294 rpt strip_tac >> fs[] 295 >> simp[EQ_IMP_THM] >> rpt strip_tac 296 >- (fs[tlg_concr_def,tr_less_general_def] 297 >> `MEM_SUBSET ce1.sucs ce2.sucs` by ( 298 Cases_on `ce1` >> Cases_on `ce2` 299 >> fs[concr2AbstractEdge_def] >> metis_tac[MEM_SUBSET_SET_TO_LIST] 300 ) 301 >> fs[] 302 >> `MEM_SUBSET (get_acc_set acc ce2) (get_acc_set acc ce1)` by ( 303 simp[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] >> rpt strip_tac 304 >> `is_until x ��� MEM x (graphStates g_AA)` by ( 305 fs[get_acc_set_def,CAT_OPTIONS_MEM,MEM_MAP] 306 >> Cases_on `y` >> fs[valid_acc_def] 307 >> `?id nL. (findNode (��(i,l). l.frml = x) g_AA = SOME (id,nL)) 308 ��� (is_until x)` 309 by metis_tac[] 310 >> fs[findNode_def] 311 >> `(MEM (id,nL) (toAList g_AA.nodeInfo)) 312 ��� (��(i,l). l.frml = x) (id,nL)` by metis_tac[FIND_LEMM2] 313 >> simp[graphStates_def,MEM_MAP] >> fs[] 314 >> metis_tac[SND] 315 ) 316 >> `(qs,FST (concr2AbstractEdge (set aP) ce2), 317 SND (concr2AbstractEdge (set aP) ce2)) ��� 318 acc_cond (removeStatesSimpl (ltl2vwaa h)) x` 319 by metis_tac[CONCR_ACC_SETS] 320 >> fs[] 321 >> `MEM x (MAP FST acc)` by ( 322 fs[valid_acc_def] >> simp[MEM_MAP] 323 >> first_x_assum (qspec_then `x` mp_tac) >> simp[] 324 >> rpt strip_tac >> qexists_tac `(x,f_trns)` >> simp[] 325 ) 326 >> `(qs,concr2AbstractEdge (set aP) ce1) ��� 327 acc_cond (removeStatesSimpl (ltl2vwaa h)) x` by metis_tac[] 328 >> metis_tac[CONCR_ACC_SETS,FST,SND] 329 ) 330 >> fs[] 331 >> Cases_on `trns_is_empty ce2` >> fs[] 332 >> `~(transformLabel (set aP) ce2.pos ce2.neg = ���)` 333 by metis_tac[TRNS_IS_EMPTY_LEMM,MEM_SUBSET_SET_TO_LIST] 334 >> `���x. MEM x ce1.pos ��� MEM x ce2.pos ��� MEM x ce1.neg ��� MEM x ce2.neg 335 ��� x ��� set aP` suffices_by ( 336 strip_tac 337 >> Cases_on `ce2` >> Cases_on `ce1` >> fs[concr2AbstractEdge_def] 338 >> metis_tac[TRANSFORMLABEL_SUBSET2] 339 ) 340 >> rpt strip_tac >> metis_tac[SUBSET_DEF,MEM_SUBSET_SET_TO_LIST] 341 ) 342 >- (`((MEM_SUBSET ce1.pos ce2.pos ��� MEM_SUBSET ce1.neg ce2.neg 343 ��� ~trns_is_empty ce2) ��� trns_is_empty ce2) 344 ��� MEM_SUBSET ce1.sucs ce2.sucs 345 ��� MEM_SUBSET (get_acc_set acc ce2) (get_acc_set acc ce1)` 346 by metis_tac[tlg_concr_def] 347 >> fs[tr_less_general_def] 348 >> qexists_tac `e1_lab` >> qexists_tac `e1_sucs` 349 >> qexists_tac `e2_lab` >> qexists_tac `e2_sucs` >> fs[] 350 >> `e1_sucs ��� e2_sucs` by ( 351 Cases_on `ce1` >> Cases_on `ce2` >> fs[concr2AbstractEdge_def] 352 >> rw[] >> fs[MEM_SUBSET_SET_TO_LIST] 353 ) 354 >> `���T'. 355 (���f. 356 (T' = acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f) 357 ��� MEM f (MAP FST acc)) ��� 358 ((qs,concr2AbstractEdge (set aP) ce2) ��� T' ��� 359 (qs,concr2AbstractEdge (set aP) ce1) ��� T')` by ( 360 fs[] >> rpt strip_tac 361 >> `is_until f ��� MEM f (graphStates g_AA)` by ( 362 fs[valid_acc_def,MEM_MAP] 363 >> Cases_on `y` >> fs[] 364 >> `?id nL. findNode (��(i,l). l.frml = f) g_AA = SOME (id,nL) 365 ��� is_until f` by metis_tac[FST] 366 >> rw[] >> fs[findNode_def] 367 >> `MEM (id,nL) (toAList g_AA.nodeInfo) 368 ��� (��(i,l). l.frml = f) (id,nL)` by metis_tac[FIND_LEMM2] 369 >> fs[] >> simp[graphStates_def,MEM_MAP] >> qexists_tac `(id,nL)` 370 >> fs[] 371 ) 372 >> `(MEM f (get_acc_set acc ce1) ��� 373 (qs,FST (e1_lab,e1_sucs),SND (e1_lab,e1_sucs)) ��� 374 acc_cond abstrAA f)` by metis_tac[CONCR_ACC_SETS] 375 >> `MEM f (get_acc_set acc ce2)` by ( 376 simp[get_acc_set_def,CAT_OPTIONS_MEM,MEM_MAP] 377 >> fs[MEM_MAP] >> qexists_tac `y` >> fs[] >> Cases_on `y` 378 >> fs[] >> simp[acc_cond_concr_def] >> rw[] 379 >> Cases_on `MEM f ce2.sucs` >> fs[] 380 >> fs[acc_cond_def] 381 >- (Cases_on `ce2` >> fs[concr2AbstractEdge_def] >> rw[] 382 >> metis_tac[] 383 ) 384 >- (simp[EXISTS_MEM] 385 >> `trns_is_empty ce2 \/ 386 ~(transformLabel (set aP) ce2.pos ce2.neg = {})` 387 by metis_tac[TRNS_IS_EMPTY_LEMM,MEM_SUBSET_SET_TO_LIST] 388 >> Cases_on `ce2` 389 >> fs[concr2AbstractEdge_def] >> rw[] 390 >> fs[valid_acc_def] >> rename[`MEM (f,f_trns) acc`] 391 >> `���id nL. 392 (findNode (��(i,l). l.frml = f) g_AA = SOME (id,nL)) 393 ��� (SOME f_trns = concr_extrTrans g_AA id) 394 ��� (���ce. 395 MEM ce f_trns ��� 396 (set ce.pos ��� set aP) ��� (set ce.neg ��� set aP))` 397 by metis_tac[] 398 >> rw[] >> fs[concr2AbstrAA_def] >> rw[] 399 >> `���n cT. 400 (concr_extrTrans g_AA id = SOME cT) 401 ��� (lookup id g_AA.nodeInfo = SOME n) 402 ��� (set (MAP (concr2AbstractEdge (set aP)) cT) = 403 concrTrans g_AA (set aP) n.frml)` by ( 404 `?flws. lookup id g_AA.followers = SOME flws` by ( 405 fs[findNode_def] 406 >> `MEM (id,nL) (toAList g_AA.nodeInfo)` 407 by metis_tac[FIND_LEMM2] 408 >> fs[wfg_def] 409 >> metis_tac[MEM_toAList,domain_lookup] 410 ) 411 >> IMP_RES_TAC CONCR_EXTRTRANS_LEMM 412 >> first_x_assum (qspec_then `id` mp_tac) >> simp[] 413 ) 414 >> `(lookup id g_AA.nodeInfo = SOME nL) 415 ��� (f = n.frml)` by ( 416 fs[findNode_def] 417 >> `n = nL ��� (��(i,l). l.frml = f) (id,nL)` 418 by metis_tac[FIND_LEMM2,MEM_toAList,SOME_11] 419 >> fs[] 420 ) 421 >> `cT = f_trns` by metis_tac[SOME_11] >> rw[] 422 >> rename[`(ce_lab,ce_sucs) ��� concrTrans _ _ _`] 423 >> `MEM (ce_lab,ce_sucs) 424 (MAP (concr2AbstractEdge (set aP)) cT)` 425 by fs[] 426 >> fs[MEM_MAP] >> rename[`MEM ce cT`] >> rw[] 427 >> `MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP` 428 by metis_tac[] 429 >> qexists_tac `ce` >> Cases_on `ce` 430 >> fs[concrEdge_component_equality,concr2AbstractEdge_def] 431 >> rename[`MEM (concrEdge ce_pos ce_neg ce_sucs) cT`] 432 >> `MEM_SUBSET ce_sucs l1` by fs[MEM_SUBSET_SET_TO_LIST] 433 >> fs[] 434 >> `���x. ((MEM x ce_pos) ��� (MEM x l) 435 ��� (MEM x ce_neg) ��� (MEM x l0)) 436 ��� MEM x aP` suffices_by ( 437 strip_tac >> IMP_RES_TAC TRANSFORMLABEL_SUBSET2 438 >> metis_tac[] 439 ) 440 >> rpt strip_tac 441 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 442 ) 443 ) 444 >> `MEM f (get_acc_set acc ce1)` 445 by metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 446 >> fs[] >> rw[] >> metis_tac[] 447 ) 448 >> fs[] 449 >- (Cases_on `ce1` >> Cases_on `ce2` >> fs[concr2AbstractEdge_def] 450 >> metis_tac[TRANSFORMLABEL_SUBSET] 451 ) 452 >- (`e2_lab = {}` by ( 453 `transformLabel (set aP) ce2.pos ce2.neg = {}` 454 by metis_tac[TRNS_IS_EMPTY_LEMM,MEM_SUBSET_SET_TO_LIST] 455 >> Cases_on `ce2` >> fs[concr2AbstractEdge_def] >> rw[] 456 ) 457 >> fs[] 458 ) 459 ) 460 ); 461 462val possibleGBA_states_def = Define` 463 possibleGBA_states g_AA = 464 {set qs | !q. MEM q qs ==> MEM q (graphStates g_AA) ��� ALL_DISTINCT qs }`; 465 466val decr_expGBA_rel_def = Define ` 467 decr_expGBA_rel (g_AA1,acc1,ids1,G1) (g_AA2,acc2,ids2,G2) = 468 let m = 469 ��g. {set x | inGBA g x } ��� possibleGBA_states g_AA1 470 in 471 (g_AA1 = g_AA2) 472 ��� (NoNodeProcessedTwice 473 (possibleGBA_states g_AA1) m (G1,ids1) (G2,ids2))`; 474 475val DECR_EXPGBA_REL_WF = store_thm 476 ("DECR_EXPGBA_REL_WF", 477 ``WF decr_expGBA_rel``, 478 qabbrev_tac ` 479 lifted_NNPT = 480 ��B:((�� ltl_frml -> bool) -> bool) 481 (j:(�� nodeLabelAA, ��) gfg, 482 k:��, 483 l:�� list, 484 m:(�� nodeLabelGBA, ��) gfg) 485 (j2:(�� nodeLabelAA, ��) gfg, 486 k2:��, 487 l2:�� list, 488 m2:(�� nodeLabelGBA, ��) gfg). 489 NoNodeProcessedTwice 490 B 491 (��g. {set x | inGBA g x } ��� B) 492 (m,l) (m2,l2)` 493 >> `!B. FINITE B ==> WF (lifted_NNPT B)` by ( 494 rpt strip_tac 495 >> `lifted_NNPT B = 496 inv_image 497 (NoNodeProcessedTwice B (��g.{set x | inGBA g x} ��� B)) 498 (��(m,n,k,l). (l,k))` by ( 499 Q.HO_MATCH_ABBREV_TAC `Q = P` 500 >> `!x1 x2. Q x1 x2 = P x1 x2` suffices_by metis_tac[] 501 >> rpt strip_tac >> qunabbrev_tac `Q` >> qunabbrev_tac `P` 502 >> fs[inv_image_def] >> qunabbrev_tac `lifted_NNPT` 503 >> Cases_on `x1` >> Cases_on `x2` >> Cases_on `r` >> Cases_on `r'` 504 >> Cases_on `r` >> Cases_on `r''` >> fs[EQ_IMP_THM] 505 ) >> rw[] 506 >> metis_tac[WF_inv_image,NNPT_WF] 507 ) 508 >> IMP_RES_TAC WF_LEMM 509 >> first_x_assum (qspec_then `��(m,n,j,k). possibleGBA_states m` mp_tac) 510 >> Q.HO_MATCH_ABBREV_TAC `(A ==> WF B) ==> WF C` 511 >> `A` by ( 512 qunabbrev_tac `A` 513 >> rpt strip_tac >> Cases_on `k` >> Cases_on `r` >> Cases_on `r'` >> fs[] 514 >> simp[possibleGBA_states_def] 515 >> `{set qs | ���q'. MEM q' qs ��� MEM q' (graphStates q) ��� ALL_DISTINCT qs} = 516 {set qs | MEM_SUBSET qs (graphStates q) ��� ALL_DISTINCT qs}` by ( 517 simp[SET_EQ_SUBSET,SUBSET_DEF,MEM_SUBSET_SET_TO_LIST] 518 >> rpt strip_tac >> Cases_on `x` >> fs[ALL_DISTINCT] 519 >> qexists_tac `qs` >> fs[] >> Cases_on `qs` >> fs[ALL_DISTINCT] 520 >> metis_tac[] 521 ) 522 >> `FINITE (IMAGE 523 set ({qs | MEM_SUBSET qs (graphStates q) 524 ��� ALL_DISTINCT qs}))` suffices_by ( 525 strip_tac >> fs[IMAGE_DEF,MEM_SUBSET_SET_TO_LIST] 526 ) 527 >> rw[] >> metis_tac[SET_OF_SUBLISTS_FINITE,IMAGE_FINITE] 528 ) 529 >> simp[] >> rpt strip_tac 530 >> `!x y. C x y ==> B x y` suffices_by metis_tac[WF_SUBSET] 531 >> qunabbrev_tac `B` >> qunabbrev_tac `C` >> rpt strip_tac >> fs[] 532 >> Cases_on `x` >> Cases_on `y` >> qunabbrev_tac `lifted_NNPT` >> fs[] 533 >> Cases_on `r` >> Cases_on `r'` >> fs[] >> Cases_on `r` >> Cases_on `r''` 534 >> fs[] >> fs[decr_expGBA_rel_def] 535 ); 536 537val towards_suff_wfg_def = Define 538 `towards_suff_wfg (g_AA1,acc1,ids1,G1) (g_AA2,acc2,ids2,G2) = 539 let max_elems = ��d. maximal_elements d (rrestrict (rel_to_reln ($<)) d) 540 in ((max_elems (domain G1.nodeInfo) = 541 max_elems (domain G2.nodeInfo)) 542 ��� ((G1.next > G2.next) \/ 543 (G1.next = G2.next ��� (LENGTH ids1 < LENGTH ids2))))` 544 545val TWDRS_SUFFWFG_WF = store_thm 546 ("TWDRS_SUFFWFG_WF", 547 ``let P = ��(g_AA,acc,ids,G). suff_wfg G 548 in WF (��x y. ~P x ��� ~P y ��� towards_suff_wfg x y)``, 549 fs[] >> simp[WF_IFF_WELLFOUNDED,wellfounded_def] >> rpt strip_tac 550 >> CCONTR_TAC >> fs[towards_suff_wfg_def] 551 >> qabbrev_tac `get_next = 552 ��(g_AA :��),(acc :��),(ids :�� list),(G :(��, ��) gfg). 553 G.next` 554 >> qabbrev_tac `get_ids = 555 ��(g_AA :��),(acc :��),(ids :�� list),(G :(��, ��) gfg). 556 ids` 557 >> qabbrev_tac `get_domain = 558 ��(g_AA :��),(acc :��),(ids :�� list),(G :(��, ��) gfg). 559 domain G.nodeInfo` 560 >> `!k. ?j. k <= j ��� (get_next (f j) < get_next (f (SUC j)))` by ( 561 rpt strip_tac 562 >> CCONTR_TAC >> fs[] 563 >> `!a. k <= a 564 ==> LENGTH (get_ids (f (SUC a))) < LENGTH (get_ids (f a))` by ( 565 rpt strip_tac 566 >> first_x_assum (qspec_then `a` mp_tac) >> simp[] >> rpt strip_tac 567 >> `towards_suff_wfg (f (SUC a)) (f a)` by fs[] 568 >> qunabbrev_tac `get_ids` >> Cases_on `f (SUC a)` >> Cases_on `f a` 569 >> fs[] >> Cases_on `r` >> Cases_on `r'` >> fs[] 570 >> Cases_on `r` >> Cases_on `r''` >> fs[towards_suff_wfg_def] 571 >> qunabbrev_tac `get_next` >> fs[] 572 ) 573 >> `WF (measure (LENGTH o get_ids o f))` by fs[] 574 >> POP_ASSUM mp_tac 575 >> PURE_REWRITE_TAC[WF_IFF_WELLFOUNDED,wellfounded_def] >> fs[] 576 >> qexists_tac `��x. x + k` >> rpt strip_tac >> fs[] 577 >> metis_tac[DECIDE ``k <= k + n``, 578 DECIDE ``k + SUC n = SUC (k + n)``] 579 ) 580 >> qabbrev_tac `D = get_domain (f 0)` 581 >> qabbrev_tac `max_elems = 582 ��d. maximal_elements d (rrestrict (rel_to_reln ($<)) d)` 583 >> `!a. max_elems (get_domain (f a)) = max_elems D` by ( 584 Induct_on `a` >> fs[] >> rw[] 585 >> `towards_suff_wfg (f (SUC a)) (f a)` by fs[] 586 >> qunabbrev_tac `get_domain` >> Cases_on `f (SUC a)` >> Cases_on `f a` 587 >> fs[] >> Cases_on `r` >> Cases_on `r'` >> fs[] 588 >> Cases_on `r` >> Cases_on `r''` >> fs[towards_suff_wfg_def] 589 >> qunabbrev_tac `max_elems` >> fs[] 590 ) 591 >> Cases_on `D = {}` 592 >- ( 593 `��(��(g_AA,acc,ids,G). suff_wfg G) (f 0)` by fs[] 594 >> Cases_on `f 0` >> fs[] >> Cases_on `r` >> fs[] >> Cases_on `r'` >> fs[] 595 >> fs[suff_wfg_def] >> qunabbrev_tac `get_domain` >> fs[] 596 >> metis_tac[MEMBER_NOT_EMPTY] 597 ) 598 >- ( 599 `?x. x ��� maximal_elements D (rrestrict (rel_to_reln ($<)) D)` by ( 600 HO_MATCH_MP_TAC finite_strict_linear_order_has_maximal 601 >> rpt strip_tac >> qunabbrev_tac `D` >> fs[] 602 >- (Cases_on `f 0` >> fs[] >> Cases_on `r` >> fs[] >> Cases_on `r'` 603 >> fs[] >> qunabbrev_tac `get_domain` 604 >> fs[FINITE_domain] 605 ) 606 >- (simp[strict_linear_order_def,rrestrict_def,rel_to_reln_def] 607 >> simp[set_relationTheory.domain_def,range_def,transitive_def,antisym_def] 608 >> simp[SUBSET_DEF] >> rpt strip_tac 609 ) 610 ) 611 >> `!b. ?n. b < get_next (f n)` by ( 612 `!n. get_next (f n) <= get_next (f (SUC n))` by ( 613 rpt strip_tac 614 >> `towards_suff_wfg (f (SUC n)) (f n)` by fs[] 615 >> qunabbrev_tac `get_ids` >> Cases_on `f (SUC n)` >> Cases_on `f n` 616 >> fs[] >> Cases_on `r` >> Cases_on `r'` >> fs[] 617 >> Cases_on `r` >> Cases_on `r''` >> fs[towards_suff_wfg_def] 618 >> qunabbrev_tac `get_next` >> fs[] 619 ) 620 >> Induct_on `b` >> fs[] 621 >- (`���j. get_next (f j) < get_next (f (SUC j))` by metis_tac[] 622 >> qexists_tac `SUC j` >> fs[] 623 ) 624 >- (`!a. (n <= a) ==> (get_next (f n) <= get_next (f a))` by ( 625 Induct_on `a` >> fs[] >> rpt strip_tac >> Cases_on `n = SUC a` 626 >> fs[] >> `get_next (f a) <= get_next (f (SUC a))` by fs[] 627 >> fs[] 628 ) 629 >> `���j. n ��� j ��� get_next (f j) < get_next (f (SUC j))` by metis_tac[] 630 >> qexists_tac `SUC j` >> fs[] 631 >> `get_next (f n) <= get_next (f j)` by fs[] >> fs[] 632 ) 633 ) 634 >> `?n. x < get_next (f n)` by fs[] 635 >> `��(��(g_AA,acc,ids,G). suff_wfg G) (f n)` by metis_tac[] 636 >> `max_elems (get_domain (f n)) = max_elems D` by fs[] 637 >> `x ��� max_elems (get_domain (f n))` by ( 638 qunabbrev_tac `max_elems` >> fs[] 639 ) 640 >> Cases_on `f n` >> fs[] >> Cases_on `r` >> fs[] >> Cases_on `r'` 641 >> fs[suff_wfg_def] >> qunabbrev_tac `get_next` >> fs[] 642 >> rw[] 643 >> qunabbrev_tac `get_domain` >> qunabbrev_tac `max_elems` >> fs[] 644 >> rw[] >> fs[maximal_elements_def] >> rw[] >> fs[] >> rw[] 645 >> `n' ��� domain r.nodeInfo 646 ��� (x,n') ��� rrestrict (rel_to_reln $<) (domain r.nodeInfo) ��� 647 x = n'` by metis_tac[] 648 >> `x = n'` by ( 649 `(x,n') ��� rrestrict (rel_to_reln $<) (domain r.nodeInfo)` 650 suffices_by metis_tac[] 651 >> PURE_REWRITE_TAC[rrestrict_def,rel_to_reln_def] >> simp[] 652 ) 653 >> fs[] 654 ) 655 ); 656 657val decr_expGBA_strong_def = Define ` 658 decr_expGBA_strong (g_AA1,acc1,ids1,G1) (g_AA2,acc2,ids2,G2) = 659 ((decr_expGBA_rel (g_AA1,acc1,ids1,G1) (g_AA2,acc2,ids2,G2)) 660 ��� (suff_wfg G2 ==> suff_wfg G1))`; 661 662val DECR_EXPGBA_STRONG_WF = store_thm 663 ("DECR_EXPGBA_STRONG_WF", 664 ``WF decr_expGBA_strong``, 665 HO_MATCH_MP_TAC WF_SUBSET 666 >> qexists_tac `decr_expGBA_rel` >> rpt strip_tac 667 >- metis_tac[DECR_EXPGBA_REL_WF] 668 >- (Cases_on `x` >> Cases_on `y` >> Cases_on `r` >> Cases_on `r'` 669 >> Cases_on `r` >> Cases_on `r''` >> fs[decr_expGBA_strong_def] 670 ) 671 ); 672 673val concr_min_rel_def = Define` 674 concr_min_rel (t1,acc1) (t2,acc2) = 675 (tlg_concr (t1,acc1) (t2,acc2) 676 ��� ~((MEM_EQUAL t1.pos t2.pos) 677 ��� (MEM_EQUAL t1.neg t2.neg) 678 ��� (MEM_EQUAL t1.sucs t2.sucs)) 679 ��� ~(trns_is_empty t1 ��� trns_is_empty t2 680 ��� MEM_EQUAL t1.sucs t2.sucs))`; 681 682 683val expandGBA_def = tDefine ("expandGBA") 684 `(expandGBA g_AA acc [] G = SOME G) 685 ��� (expandGBA g_AA acc (id::ids) G = 686 case lookup id G.nodeInfo of 687 | NONE => NONE 688 | SOME current_node => 689 let aa_frml_ids = 690 CAT_OPTIONS 691 (MAP (��f. OPTION_MAP FST 692 (findNode (��(i,l). l.frml = f) g_AA) 693 ) 694 current_node.frmls) 695 in let concr_edges = 696 CAT_OPTIONS 697 (MAP (concr_extrTrans g_AA) aa_frml_ids) 698 in let trans_unopt = gba_trans_concr concr_edges 699 in let flws_with_acc_sets = 700 MAP (��cE. (cE,get_acc_set acc cE)) trans_unopt 701 in let trans = 702 ONLY_MINIMAL 703 concr_min_rel 704 flws_with_acc_sets 705 in let new_sucs = 706 FILTER (��qs. ~inGBA G qs) 707 (MAP (��(cE,fs). cE.sucs) trans) 708 in let (new_ids, G1) = 709 FOLDR (��n (ids,g). 710 if inGBA g n 711 then (ids,g) 712 else ((g.next::ids),addNodeToGBA g n)) 713 ([],G) new_sucs 714 in do G2 <- 715 FOLDR 716 (��(eL,suc) g_opt. do g <- g_opt ; 717 addEdgeToGBA g id eL suc 718 od) 719 (SOME G1) 720 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) trans) ; 721 expandGBA g_AA acc (nub (ids ++ new_ids)) G2 722 od 723 )` 724 (qabbrev_tac `P = ��(g_AA:(�� nodeLabelAA, �� edgeLabelAA) gfg, 725 acc:(�� ltl_frml, �� concrEdge list) alist, 726 ids:num list, 727 G:(�� nodeLabelGBA, �� edgeLabelGBA) gfg). suff_wfg G` 728 >> WF_REL_TAC `��x y. (~P y ��� ~P x ==> towards_suff_wfg x y) 729 ��� (P y ==> decr_expGBA_strong x y)` 730 >- (HO_MATCH_MP_TAC P_DIVIDED_WF_LEMM >> rpt strip_tac 731 >- metis_tac[TWDRS_SUFFWFG_WF] 732 >- metis_tac[DECR_EXPGBA_STRONG_WF] 733 >- (Cases_on `x` >> Cases_on `y` >> Cases_on `r` >> Cases_on `r'` 734 >> Cases_on `r` >> Cases_on `r''` 735 >> rename[`P (g_AA1,acc1,ids1,G1)`] 736 >> rename[`decr_expGBA_strong _ (g_AA2,acc2,ids2,G2)`] 737 >> qunabbrev_tac `P` >> fs[decr_expGBA_strong_def,suff_wfg_def] 738 ) 739 ) 740 >- (rpt strip_tac >> fs[] 741 >> simp[decr_expGBA_rel_def,NoNodeProcessedTwice_def] >> fs[] 742 >> qabbrev_tac `t = 743 gba_trans_concr 744 (CAT_OPTIONS 745 (MAP (concr_extrTrans g_AA) 746 (CAT_OPTIONS 747 (MAP 748 (��f. 749 OPTION_MAP FST 750 (findNode (��(i,l). l.frml = f) 751 g_AA)) 752 current_node.frmls))))` 753 >> qabbrev_tac `t_with_acc = MAP (��cE. (cE,get_acc_set acc cE)) t` 754 >> `!l n_G. 755 (FOLDR 756 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 757 (SOME G1) l = SOME n_G) 758 ==> ((G1.nodeInfo = n_G.nodeInfo) ��� (G1.next = n_G.next))` by ( 759 Induct_on `l` >> fs[] >> rpt strip_tac >> fs[] 760 >> Cases_on `h` >> fs[] 761 >> `G1.nodeInfo = g.nodeInfo ��� G1.next = g.next` by metis_tac[] 762 >> fs[addEdgeToGBA_def] 763 >> Cases_on `findNode (��(i,q). MEM_EQUAL q.frmls r) g` >> fs[] 764 >> Cases_on `x` >> fs[] 765 >- metis_tac[addEdge_preserves_nodeInfo] 766 >- (fs[addEdge_def] >> rw[]) 767 ) 768 >> `!l n_ids n_G. 769 (n_ids,n_G) = 770 FOLDR (��n (ids,g). 771 if inGBA g n then (ids,g) 772 else (g.next::ids,addNodeToGBA g n)) ([],G) l 773 ==> ((!n. n ��� domain n_G.nodeInfo 774 ==> ((n ��� domain G.nodeInfo) \/ n < n_G.next)) 775 ��� (!n. n ��� domain G.nodeInfo ==> n ��� domain n_G.nodeInfo) 776 ��� (G.next <= n_G.next) 777 ��� ((G.next = n_G.next) 778 ==> ((G.nodeInfo = n_G.nodeInfo) 779 ��� (n_ids = []))))` by ( 780 Induct_on `l` >> fs[] >> rpt strip_tac 781 >> Cases_on `(FOLDR (��n (ids,g). 782 if inGBA g n then (ids,g) 783 else (g.next::ids,addNodeToGBA g n)) ([],G) l)` 784 >> fs[] >> Cases_on `inGBA r h` >> fs[] >> rw[] 785 >> fs[addNodeToGBA_def] >> fs[addNode_def] 786 >> metis_tac[DECIDE ``n < r.next ==> n < SUC r.next``] 787 ) 788 >- ( 789 simp[towards_suff_wfg_def] >> qunabbrev_tac `P` >> fs[suff_wfg_def] 790 >> strip_tac 791 >- ( 792 `!n. n ��� domain G2.nodeInfo ==> n ��� domain G.nodeInfo \/ n < G2.next` 793 by metis_tac[] 794 >> simp[maximal_elements_def,rrestrict_def,rel_to_reln_def, 795 SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 796 >- (fs[] >> `x ��� domain G.nodeInfo \/ x < G2.next` by metis_tac[] 797 >> first_x_assum (qspec_then `n'` mp_tac) >> fs[] 798 ) 799 >- (fs[] >> `x ��� domain G.nodeInfo \/ x < G2.next` by metis_tac[] 800 >> fs[] 801 >- (Cases_on `x'' ��� domain G.nodeInfo` >> fs[] 802 >> `x'' ��� domain G2.nodeInfo` by metis_tac[] 803 >> metis_tac[] 804 ) 805 >- (metis_tac[]) 806 ) 807 >- metis_tac[] 808 >- (Cases_on `x'' ��� domain G2.nodeInfo` >> fs[] 809 >> `x'' ��� domain G.nodeInfo \/ x'' < G2.next` by metis_tac[] 810 >- (disj1_tac >> fs[] >> metis_tac[]) 811 >- (`x ��� domain G2.nodeInfo` by metis_tac[] >> fs[] 812 >> `x'' ��� domain G.nodeInfo \/ x'' < G2.next` by metis_tac[] 813 >- metis_tac[] 814 >- (`n' ��� domain G.nodeInfo \/ n' < G2.next` by metis_tac[] 815 >- (`~(x < n')` by metis_tac[] 816 >> fs[]) 817 >- fs[] 818 ) 819 ) 820 ) 821 ) 822 >- ( 823 `(���n. 824 n ��� domain G2.nodeInfo ��� 825 n ��� domain G.nodeInfo ��� n < G2.next) 826 ��� (���n. n ��� domain G.nodeInfo ��� n ��� domain G2.nodeInfo) 827 ��� (G.next ��� G2.next) 828 ��� ((G.next = G2.next) 829 ==> ((G.nodeInfo = G2.nodeInfo) 830 ��� (new_ids = [])))` by metis_tac[] 831 >> Cases_on `G2.next > G.next` >> fs[] 832 >> `!(l:num list). LENGTH (nub l) <= LENGTH l` by ( 833 Induct_on `l` >> fs[nub_def] >> rpt strip_tac 834 >> Cases_on `MEM h l` >> fs[] 835 ) 836 >> `G.next = G2.next` by fs[] 837 >> `G.nodeInfo = G2.nodeInfo ��� new_ids = []` by metis_tac[] 838 >> rw[] >> fs[] 839 >> `LENGTH (nub ids) <= LENGTH ids` by metis_tac[] 840 >> rw[] 841 ) 842 ) 843 >- ( 844 `!l n_ids n_G. 845 (n_ids,n_G) = 846 FOLDR (��n (ids,g). 847 if inGBA g n then (ids,g) 848 else (g.next::ids,addNodeToGBA g n)) ([],G) l 849 ==> (!x id. lookup id G.nodeInfo = SOME x 850 ==> lookup id n_G.nodeInfo = SOME x)` by ( 851 Induct_on `l` >> fs[] >> rpt strip_tac 852 >> Cases_on `(FOLDR (��n (ids,g). 853 if inGBA g n then (ids,g) 854 else (g.next::ids,addNodeToGBA g n)) ([],G) l)` 855 >> fs[] >> Cases_on `inGBA r h` >> fs[] >> rw[] 856 >> fs[addNodeToGBA_def] >> fs[addNode_def] 857 >> qunabbrev_tac `P` >> fs[suff_wfg_def] 858 >> `G.next <= r.next` by metis_tac[] 859 >> `lookup id' r.nodeInfo = SOME x` by fs[] 860 >> `~(id' = r.next)` by ( 861 `id' ��� domain G.nodeInfo` by metis_tac[domain_lookup] 862 >> `~(G.next <= id')` by metis_tac[] 863 >> fs[] 864 ) 865 >> metis_tac[lookup_insert] 866 ) 867 >> simp[decr_expGBA_strong_def,decr_expGBA_rel_def] 868 >> simp[NoNodeProcessedTwice_def] >> qunabbrev_tac `P` >> fs[] 869 >> Q.HO_MATCH_ABBREV_TAC 870 `((M G2 ��� M G) \/ (M G2 = M G ��� EQ_LENGTH)) ��� suff_wfg G2` 871 >> `M G2 ��� M G` by ( 872 qunabbrev_tac `M` >> fs[] 873 >> `{x | inGBA G x} ��� {x | inGBA G2 x}` suffices_by ( 874 simp[SUBSET_DEF] >> rpt strip_tac >> fs[] 875 >> metis_tac[] 876 ) 877 >> simp[SUBSET_DEF] >> rpt strip_tac >> fs[inGBA_def] 878 >> fs[EXISTS_MEM,MEM_MAP] >> Cases_on `y` >> fs[] >> rw[] 879 >> rename[`MEM (id,n) (toAList G.nodeInfo)`] 880 >> `lookup id G2.nodeInfo = SOME n` by metis_tac[MEM_toAList] 881 >> qexists_tac `n` >> fs[] >> qexists_tac `(id,n)` >> fs[MEM_toAList] 882 ) 883 >> `suff_wfg G2` by ( 884 `suff_wfg (SND (new_ids,G1))` by metis_tac[ADDNODE_GBA_FOLDR] 885 >> `G1.nodeInfo = G2.nodeInfo ��� G1.next = G2.next` by metis_tac[] 886 >> fs[suff_wfg_def] 887 ) 888 >> Cases_on `M G2 = M G` >> fs[PSUBSET_DEF] 889 >> qabbrev_tac `QS = 890 FILTER (��qs. ��inGBA G qs) 891 (MAP (��(cE,fs). cE.sucs) 892 (ONLY_MINIMAL concr_min_rel t_with_acc))` 893 >> `suff_wfg (SND (new_ids,G1)) 894 ��� {set x | inGBA (SND (new_ids,G1)) x} = 895 {set x | inGBA G x} ��� set (MAP set QS)` 896 by metis_tac[ADDNODE_GBA_FOLDR] 897 >> fs[] 898 >> `{set x | inGBA G1 x} = {set x | inGBA G2 x}` by ( 899 `G1.nodeInfo = G2.nodeInfo` by metis_tac[] 900 >> PURE_REWRITE_TAC[inGBA_def] >> metis_tac[] 901 ) 902 >> `!x. MEM x QS ==> (set x ��� possibleGBA_states g_AA)` by ( 903 rpt strip_tac >> qunabbrev_tac `QS` >> fs[MEM_FILTER,MEM_MAP] 904 >> `MEM y t_with_acc` by metis_tac[ONLY_MINIMAL_SUBSET, 905 MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 906 >> rename[`MEM ce_with_acc t_with_acc`] >> Cases_on `ce_with_acc` 907 >> fs[] 908 >> `MEM q t` by (qunabbrev_tac `t_with_acc` >> fs[MEM_MAP]) 909 >> qunabbrev_tac `t` 910 >> qabbrev_tac `c_trns = 911 CAT_OPTIONS 912 (MAP (concr_extrTrans g_AA) 913 (CAT_OPTIONS 914 (MAP 915 (��f. 916 OPTION_MAP FST 917 (findNode (��(i,l). l.frml = f) g_AA)) 918 current_node.frmls)))` 919 >> `!x. MEM x q.sucs 920 ==> ?l ce. MEM l c_trns ��� MEM ce l ��� MEM x ce.sucs` by ( 921 rpt strip_tac >> metis_tac[GBA_TRANS_LEMM3] 922 ) 923 >> simp[possibleGBA_states_def] >> qexists_tac `q.sucs` >> fs[] 924 >> strip_tac >> strip_tac 925 >> first_x_assum (qspec_then `q'` mp_tac) >> simp[] >> strip_tac 926 >> qunabbrev_tac `c_trns` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 927 >> strip_tac 928 >- metis_tac[CONCR_EXTRTRANS_NODES] 929 >- metis_tac[GBA_TRANS_LEMM1] 930 ) 931 >> `!x. MEM x QS ==> set x ��� {set x | inGBA G x}` by ( 932 qabbrev_tac `PS = possibleGBA_states g_AA` 933 >> qunabbrev_tac `M` >> fs[] >> rw[] 934 >> fs[DIFF_INTER2,DIFF_UNION] >> qexists_tac `x` 935 >> fs[] >> CCONTR_TAC >> `set x ��� PS` by fs[] 936 >> `~(set x ��� (PS DIFF {set x | inGBA G x} DIFF set (MAP set QS)))` 937 by ( 938 simp[IN_DIFF,MEM_MAP] >> rpt strip_tac 939 >> disj2_tac >> metis_tac[] 940 ) 941 >> `set x ��� PS DIFF {set x | inGBA G x}` by ( 942 simp[IN_DIFF] >> rpt strip_tac >> Cases_on `set x = set x'` 943 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 944 ) 945 >> metis_tac[SET_EQ_SUBSET,SUBSET_DEF] 946 ) 947 >> `QS = []` by ( 948 `set QS = {}` suffices_by fs[] 949 >> `!x. ~MEM x QS` suffices_by metis_tac[MEM,MEMBER_NOT_EMPTY] 950 >> rpt strip_tac >> `set x ��� {set x | inGBA G x}` by fs[] 951 >> qunabbrev_tac `QS` >> fs[MEM_FILTER] 952 >> `MEM_EQUAL x' x` by fs[MEM_EQUAL_SET] 953 >> metis_tac[IN_GBA_MEM_EQUAL] 954 ) 955 >> rw[] >> `new_ids = []` by fs[] 956 >> qunabbrev_tac `EQ_LENGTH` >> fs[] 957 >> `!(l:num list). LENGTH (nub l) <= LENGTH l` by ( 958 Induct_on `l` >> fs[nub_def] >> rpt strip_tac 959 >> Cases_on `MEM h l` >> fs[] 960 ) 961 >> `LENGTH (nub ids) <= (LENGTH ids)` by metis_tac[] 962 >> rw[] 963 ) 964 ) 965 ); 966 967val expandGBA_init_def = Define` 968 expandGBA_init (concrAA g_AA initAA props) = 969 let initNodes = MAP (��i_list. 970 let suc_nLabels = MAP (��i. lookup i g_AA.nodeInfo) 971 (nub i_list) 972 in MAP (��l. l.frml) (CAT_OPTIONS suc_nLabels) 973 ) initAA 974 in let G0 = FOLDR (��n g. addNodeToGBA g n) empty initNodes 975 in let initIds = MAP FST (toAList G0.nodeInfo) 976 in let acc_sets = 977 FOLDR (��(id,x) sF. 978 case (is_until x, concr_extrTrans g_AA id) of 979 | (T,SOME c_t) => (x,c_t)::sF 980 | _ => sF 981 ) 982 [] (graphStatesWithId g_AA) 983 in let o_graph = expandGBA g_AA acc_sets initIds G0 984 in case o_graph of 985 | SOME graph => SOME (concrGBA graph initIds (MAP FST acc_sets) props) 986 | NONE => NONE `; 987 988 989val EXPGBA_SOME_WFG = store_thm 990 ("EXPGBA_SOME_WFG", 991 ``!g_AA acc ids G. 992 wfg G 993 ��� (!i. MEM i ids ==> i ��� (domain G.nodeInfo)) 994 ==> (?gba. (expandGBA g_AA acc ids G = SOME gba) 995 ��� wfg gba 996 ��� (!i. i ��� domain G.nodeInfo 997 ==> lookup i G.nodeInfo = lookup i gba.nodeInfo 998 ) 999 ��� (frml_ad G ==> frml_ad gba))``, 1000 HO_MATCH_MP_TAC (theorem "expandGBA_ind") 1001 >> rpt strip_tac >> fs[expandGBA_def] 1002 >> Q.HO_MATCH_ABBREV_TAC 1003 `?gba. ((case lookup id G.nodeInfo of 1004 | NONE => NONE 1005 | SOME current_node => 1006 (��(new_ids,G1). 1007 do G2 <- FOLDR ADDE (SOME G1) (MAP toEL (TRNS current_node)) ; 1008 expandGBA g_AA acc (nub (ids ++ new_ids)) G2 1009 od) 1010 (FOLDR ADDN ([],G) 1011 (FILTER (��qs. ~inGBA G qs) 1012 (MAP (��(cE,fs). cE.sucs) (TRNS current_node))))) = SOME gba) 1013 ��� wfg gba 1014 ��� (���i. 1015 i ��� domain G.nodeInfo 1016 ��� (lookup i G.nodeInfo = lookup i gba.nodeInfo)) 1017 ��� (frml_ad G ==> frml_ad gba)` 1018 >> fs[] 1019 >> `?node. lookup id G.nodeInfo = SOME node` by metis_tac[domain_lookup] 1020 >> Cases_on `lookup id G.nodeInfo` >> fs[] 1021 >> Cases_on 1022 `FOLDR ADDN ([],G) 1023 (FILTER (��qs. ��inGBA G qs) 1024 (MAP (��(cE,fs). cE.sucs) (TRNS node)))` 1025 >> rename[`_ = (new_ids,addedNodesGBA)`] 1026 >> fs[] 1027 >> qabbrev_tac `NEW_NODES = 1028 FILTER (��qs. ��inGBA G qs) 1029 (MAP (��(cE,fs). cE.sucs) (TRNS node))` 1030 >> `wfg addedNodesGBA` by ( 1031 `addedNodesGBA = SND (new_ids,addedNodesGBA)` by fs[] 1032 >> qunabbrev_tac `ADDN` 1033 >> metis_tac[ADDNODE_GBA_WFG_FOLDR] 1034 ) 1035 >> `{set x | inGBA addedNodesGBA x} = 1036 {set x | inGBA G x} ��� set (MAP set NEW_NODES)` by ( 1037 `suff_wfg G` by metis_tac[WF_IMP_SUFFWFG] 1038 >> `addedNodesGBA = SND (new_ids,addedNodesGBA)` by fs[] 1039 >> qunabbrev_tac `ADDN` >> metis_tac[ADDNODE_GBA_FOLDR] 1040 ) 1041 >> `set new_ids ��� domain G.nodeInfo = 1042 domain addedNodesGBA.nodeInfo` by ( 1043 `addedNodesGBA = SND (new_ids,addedNodesGBA)` by fs[] 1044 >> `new_ids = FST (new_ids,addedNodesGBA)` by fs[] 1045 >> qunabbrev_tac `ADDN` 1046 >> metis_tac[ADDNODE_GBA_DOM_FOLDR,SUBSET_DEF,IN_UNION] 1047 ) 1048 >> `!ls. (!suc. MEM suc (MAP SND ls) ==> inGBA addedNodesGBA suc) 1049 ==> (?G2. (FOLDR ADDE (SOME addedNodesGBA) ls = SOME G2) 1050 ��� (addedNodesGBA.nodeInfo = G2.nodeInfo) ��� wfg G2)` by ( 1051 qunabbrev_tac `ADDE` >> rpt strip_tac 1052 >> HO_MATCH_MP_TAC ADDEDGE_GBA_FOLDR_LEMM >> fs[] 1053 >> `addedNodesGBA = SND (new_ids,addedNodesGBA)` by fs[] 1054 >> qunabbrev_tac `ADDN` 1055 >> metis_tac[ADDNODE_GBA_DOM_FOLDR,SUBSET_DEF,IN_UNION] 1056 ) 1057 >> first_x_assum (qspec_then `MAP toEL (TRNS node)` mp_tac) >> fs[] 1058 >> `���suc. 1059 MEM suc (MAP SND (MAP toEL (TRNS node))) ��� 1060 inGBA addedNodesGBA suc` by ( 1061 rpt strip_tac >> fs[MEM_MAP] 1062 >> rename[`MEM trns_cel (TRNS node)`,`trns_el = toEL trns_cel` ] 1063 >> fs[] 1064 >> `(MEM (FST trns_cel).sucs NEW_NODES) 1065 \/ (inGBA G (FST trns_cel).sucs)` by ( 1066 qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER] 1067 >> Cases_on `inGBA G (FST trns_cel).sucs` >> fs[] 1068 >> simp[MEM_MAP] >> Cases_on `trns_cel` >> fs[] 1069 >> qexists_tac `(q,r)` >> fs[] 1070 ) 1071 >- ( 1072 qunabbrev_tac `toEL` >> Cases_on `trns_cel` >> fs[] 1073 >> `MEM (set q.sucs) (MAP set NEW_NODES)` by ( 1074 fs[MEM_MAP] >> metis_tac[] 1075 ) 1076 >> `set (q.sucs) ��� {set x | inGBA addedNodesGBA x}` by ( 1077 metis_tac[IN_UNION] 1078 ) 1079 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 1080 ) 1081 >- ( 1082 qunabbrev_tac `toEL` >> Cases_on `trns_cel` >> fs[] 1083 >> `set q.sucs ��� {set x | inGBA addedNodesGBA x}` by ( 1084 `set q.sucs ��� {set x | inGBA G x}` by (fs[] >> metis_tac[]) 1085 >> metis_tac[IN_UNION] 1086 ) 1087 >> fs[] 1088 >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 1089 ) 1090 ) 1091 >> fs[] >> rpt strip_tac >> first_x_assum (qspec_then `G2` mp_tac) >> fs[] 1092 >> `���i. MEM i ids ��� MEM i new_ids ��� i ��� domain G2.nodeInfo` by ( 1093 rpt strip_tac >> fs[] 1094 >- metis_tac[IN_UNION] 1095 >- metis_tac[IN_UNION,MEM] 1096 ) 1097 >> fs[] >> rpt strip_tac 1098 >> `���gba. expandGBA g_AA acc (nub (ids ��� new_ids)) G2 = SOME gba 1099 ��� wfg gba 1100 ��� (���i. 1101 i ��� domain G2.nodeInfo ��� 1102 lookup i G2.nodeInfo = lookup i gba.nodeInfo) 1103 ��� (frml_ad G2 ==> frml_ad gba)` 1104 by metis_tac[] 1105 >> qexists_tac `gba` >> fs[] >> rpt strip_tac 1106 >- (`i ��� domain G2.nodeInfo` by metis_tac[UNION_SUBSET,SUBSET_DEF] 1107 >> `lookup i addedNodesGBA.nodeInfo = lookup i G.nodeInfo` 1108 suffices_by metis_tac[] 1109 >> `suff_wfg G` by metis_tac[WF_IMP_SUFFWFG] 1110 >> IMP_RES_TAC ADDNODE_GBA_FOLDR 1111 >> first_x_assum (qspec_then `NEW_NODES` mp_tac) >> simp[] 1112 ) 1113 >- (`frml_ad G2` suffices_by metis_tac[] 1114 >> `(���n. MEM n NEW_NODES ��� ALL_DISTINCT n)` suffices_by ( 1115 `suff_wfg G` by metis_tac[WF_IMP_SUFFWFG] 1116 >> IMP_RES_TAC ADDNODE_GBA_FOLDR 1117 >> first_x_assum (qspec_then `NEW_NODES` mp_tac) >> simp[] 1118 >> rpt strip_tac 1119 >> metis_tac[FRML_AD_NODEINFO] 1120 ) 1121 >> rpt strip_tac >> qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER,MEM_MAP] 1122 >> rename[`MEM t (TRNS node)`] >> Cases_on `t` >> fs[] 1123 >> `?s. MEM q (gba_trans_concr s)` by ( 1124 qunabbrev_tac `TRNS` >> fs[ONLY_MINIMAL_MEM,MEM_MAP] 1125 >> metis_tac[] 1126 ) 1127 >> metis_tac[GBA_TRANS_LEMM1] 1128 ) 1129 ); 1130 1131val trns_correct_def = Define ` 1132 trns_correct l abstrAA gba aP = 1133 (!id nL fls. 1134 (lookup id gba.nodeInfo = SOME nL) 1135 ��� (lookup id gba.followers = SOME fls) 1136 ��� (set nL.frmls ��� POW abstrAA.states) 1137 ��� ~(MEM id l) 1138 ==> 1139 (set (CAT_OPTIONS 1140 (MAP 1141 (��(eL,i). 1142 do 1143 s_nL <- lookup i gba.nodeInfo; 1144 SOME 1145 (transformLabel aP eL.pos_lab eL.neg_lab, 1146 set s_nL.frmls) 1147 od) fls)) = 1148 (gba_trans abstrAA (set nL.frmls))) 1149 )`; 1150 1151val final_correct_def = Define ` 1152 final_correct (abstrAA:(�� -> bool, �� ltl_frml) ALTER_A) gba acc = 1153 (!id fls nL eL s_id s_nL. 1154 (lookup id gba.nodeInfo = SOME nL) 1155 ��� (lookup id gba.followers = SOME fls) 1156 ��� (MEM (eL,s_id) fls) 1157 ��� (lookup s_id gba.nodeInfo = SOME s_nL) 1158 ��� (set nL.frmls ��� POW abstrAA.states) 1159 ==> (!u. MEM u eL.acc_set 1160 = MEM u (get_acc_set acc 1161 (concrEdge eL.pos_lab 1162 eL.neg_lab 1163 s_nL.frmls))) 1164 )`; 1165 1166val aP_correct_def = Define ` 1167 aP_correct (abstrAA:(�� -> bool, �� ltl_frml) ALTER_A) gba aP = 1168 (!id fls nL eL s_id. 1169 (lookup id gba.nodeInfo = SOME nL) 1170 ��� (lookup id gba.followers = SOME fls) 1171 ��� (MEM (eL,s_id) fls) 1172 ��� (set nL.frmls ��� POW abstrAA.states) 1173 ==> ((MEM_SUBSET eL.pos_lab aP) 1174 ��� (MEM_SUBSET eL.neg_lab aP)) 1175 )`; 1176 1177val EXPGBA_GRAPH_REACHABLE = store_thm 1178 ("EXPGBA_GRAPH_REACHABLE", 1179 ``!abstrAA f init aP g_AA acc ids g g2. 1180 (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 1181 ��� (abstrAA = removeStatesSimpl (ltl2vwaa f)) 1182 ��� (wfg g_AA) 1183 ��� (until_iff_final g_AA) 1184 ��� (!id cT. (concr_extrTrans g_AA id = SOME cT) 1185 ==> (!ce. MEM ce cT 1186 ==> (MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)) 1187 ) 1188 ��� (valid_acc aP g_AA acc) 1189 ��� (unique_node_formula g_AA) ��� (flws_sorted g_AA) 1190 ��� (!x. inGBA g x 1191 ==> set x ��� reachableFromSetGBA 1192 (vwaa2gba abstrAA) (vwaa2gba abstrAA).initial) 1193 ��� (!i. MEM i ids ==> i ��� domain g.nodeInfo) 1194 ��� (expandGBA g_AA acc ids g = SOME g2) 1195 ��� (wfg g) 1196 ��� (!x. inGBA g x ==> (set x ��� POW abstrAA.states)) 1197 ��� frml_ad g 1198 ==> ((!x. inGBA g2 x 1199 ==> ((set x ��� reachableFromSetGBA (vwaa2gba abstrAA) 1200 (vwaa2gba abstrAA).initial) 1201 ��� (set x ��� (vwaa2gba abstrAA).states))) 1202 )``, 1203 gen_tac >> gen_tac >> gen_tac >> gen_tac 1204 >> HO_MATCH_MP_TAC (theorem "expandGBA_ind") >> strip_tac 1205 >- (fs[] >> rpt strip_tac >> fs[expandGBA_def] 1206 >> first_x_assum (qspec_then `x` mp_tac) >> simp[] >> rpt strip_tac 1207 >> `isVeryWeakAlterA (concr2AbstrAA (concrAA g_AA init aP))` 1208 by metis_tac[REDUCE_STATE_IS_WEAK, LTL2WAA_ISWEAK, 1209 LTL2WAA_ISVALID] 1210 >> fs[vwaa2gba_def] >> first_x_assum (qspec_then `x` mp_tac) >> simp[] 1211 >> metis_tac[] 1212 ) 1213 >- (strip_tac >> strip_tac >> strip_tac >> strip_tac >> strip_tac 1214 >> strip_tac >> strip_tac >> strip_tac >> strip_tac 1215 >> strip_tac 1216 >> fs[] 1217 >> `?node. lookup id g.nodeInfo = SOME node` by metis_tac[domain_lookup] 1218 >> first_x_assum (qspec_then `node` mp_tac) >> simp[] 1219 >> strip_tac 1220 >> qabbrev_tac `TRNS = 1221 ONLY_MINIMAL 1222 concr_min_rel 1223 (MAP (��cE. (cE,get_acc_set acc cE)) 1224 (gba_trans_concr 1225 (CAT_OPTIONS 1226 (MAP (concr_extrTrans g_AA) 1227 (CAT_OPTIONS 1228 (MAP 1229 (��f. 1230 OPTION_MAP FST 1231 (findNode (��(i,l). l.frml = f) 1232 g_AA)) node.frmls))))))` 1233 >> Cases_on `FOLDR 1234 (��n (ids,g). 1235 if inGBA g n then (ids,g) 1236 else (g.next::ids,addNodeToGBA g n)) ([],g) 1237 (FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS))` 1238 >> fs[] >> rename[`_ = (new_ids,G1)`] 1239 >> `wfg G1` by ( 1240 `G1 = SND (new_ids,G1)` by fs[] 1241 >> metis_tac[ADDNODE_GBA_WFG_FOLDR] 1242 ) 1243 >> qabbrev_tac `NEW_NODES = 1244 FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS)` 1245 >> `{set x | inGBA G1 x} = 1246 {set x | inGBA g x} ��� set (MAP set NEW_NODES)` by ( 1247 `G1 = SND (new_ids,G1)` by fs[] 1248 >> metis_tac[ADDNODE_GBA_FOLDR,WF_IMP_SUFFWFG] 1249 ) 1250 >> `���x. MEM x (MAP FST TRNS) ��� inGBA G1 x.sucs` by ( 1251 rpt strip_tac >> rename[`MEM qs (MAP FST TRNS)`] 1252 >> fs[MEM_MAP] >> rename[`MEM t TRNS`] >> Cases_on `t` >> fs[] 1253 >> rw[] 1254 >> `(MEM q.sucs NEW_NODES) \/ (inGBA g q.sucs)` by ( 1255 qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER] 1256 >> Cases_on `inGBA g q.sucs` >> fs[] 1257 >> simp[MEM_MAP] 1258 >> qexists_tac `(q,r)` >> fs[] 1259 ) 1260 >- (`MEM ((set q.sucs) ) (MAP set NEW_NODES)` 1261 by (fs[MEM_MAP] >> metis_tac[]) 1262 >> `(set q.sucs) ��� {set x | inGBA G1 x }` 1263 by metis_tac[IN_UNION] 1264 >> fs[] 1265 >> metis_tac[IN_GBA_MEM_EQUAL,MEM,MEM_EQUAL_SET] 1266 ) 1267 >- (`(set q.sucs) ���{set x | inGBA g x}` 1268 by (fs[MEM_MAP] >> metis_tac[]) 1269 >> `(set q.sucs) ��� {set x | inGBA G1 x}` 1270 by metis_tac[IN_UNION] 1271 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 1272 ) 1273 ) 1274 >> `!x. MEM x 1275 (MAP SND (MAP 1276 (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) 1277 TRNS)) ==> inGBA G1 x` by ( 1278 rpt strip_tac >> fs[MEM_MAP] >> rename[`MEM t TRNS`] 1279 >> Cases_on `t` >> fs[] 1280 >> `FST (q,r) = q` by fs[] >> metis_tac[] 1281 ) 1282 >> `(set new_ids ��� domain g.nodeInfo = domain G1.nodeInfo) 1283 ��� g.next ��� G1.next` by metis_tac[FST,SND,ADDNODE_GBA_DOM_FOLDR] 1284 >> `���g2. 1285 (FOLDR 1286 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 1287 (SOME G1) 1288 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) TRNS) = 1289 SOME g2) ��� G1.nodeInfo = g2.nodeInfo ��� wfg g2` by ( 1290 HO_MATCH_MP_TAC ADDEDGE_GBA_FOLDR_LEMM 1291 >> rpt conj_tac 1292 >- metis_tac[] 1293 >- metis_tac[domain_lookup,IN_UNION] 1294 >- metis_tac[] 1295 ) 1296 >> rename[`wfg G2`] >> first_x_assum (qspec_then `G2` mp_tac) >> fs[] 1297 >> `(���id cT. 1298 (concr_extrTrans g_AA id = SOME cT) ��� 1299 ���ce. MEM ce cT ��� MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)` 1300 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[]) 1301 >> simp[] 1302 >> Q.HO_MATCH_ABBREV_TAC `(!g2. A g2 ==> B g2) ==> C` 1303 >> `B g2 ==> C` by metis_tac[] 1304 >> `A g2` suffices_by fs[] >> qunabbrev_tac `A` >> fs[] 1305 >> qabbrev_tac `abstr_gba = 1306 vwaa2gba (concr2AbstrAA (concrAA g_AA init aP))` 1307 >> `!x. inGBA G1 x = inGBA G2 x` by ( 1308 simp[inGBA_def] 1309 ) 1310 >> `!x. set x ��� reachableFromSetGBA abstr_gba {set q | inGBA g q } 1311 ==> (set x ��� reachableFromSetGBA abstr_gba 1312 {set q | inGBA G2 q })` by ( 1313 simp[reachableFromSetGBA_def] >> rpt strip_tac 1314 >> `set q ��� {set x | inGBA g x}` by (simp[] >> metis_tac[]) 1315 >> `set q ��� {set x | inGBA G1 x}` by metis_tac[IN_UNION] 1316 >> fs[] >> metis_tac[] 1317 ) 1318 >> `(���i. 1319 i ��� domain g.nodeInfo ��� 1320 lookup i g.nodeInfo = lookup i G1.nodeInfo) 1321 ��� (���i. 1322 MEM i new_ids ��� 1323 ���n. 1324 lookup i G1.nodeInfo = SOME n ��� MEM n.frmls NEW_NODES)` 1325 by metis_tac[WF_IMP_SUFFWFG,ADDNODE_GBA_FOLDR,SND,FST] 1326 >> `isVeryWeakAlterA abstrAA ��� isValidAlterA abstrAA 1327 ��� (FINITE abstrAA.states) 1328 ��� (abstrAA.alphabet = POW (set aP))` by ( 1329 fs[] >> rpt strip_tac 1330 >- metis_tac[REDUCE_STATE_IS_WEAK,LTL2WAA_ISWEAK, 1331 LTL2WAA_ISVALID] 1332 >- metis_tac[REDUCE_STATE_IS_VALID,LTL2WAA_ISVALID] 1333 >- (simp[concr2AbstrAA_def,concr2Abstr_states_def] 1334 >> `FINITE {x.frml | ?n. MEM (n,x) (toAList g_AA.nodeInfo)}` 1335 suffices_by ( 1336 Q.HO_MATCH_ABBREV_TAC `FINITE S1 ==> FINITE S2` 1337 >> `S1 = S2` suffices_by fs[] 1338 >> qunabbrev_tac `S1` >> qunabbrev_tac `S2` 1339 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1340 >> metis_tac[MEM_toAList,domain_lookup] 1341 ) 1342 >> `{x.frml | ���n. MEM (n,x) (toAList g_AA.nodeInfo)} = 1343 IMAGE (��(i,n). n.frml) (set (toAList g_AA.nodeInfo))` by ( 1344 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1345 >- (qexists_tac `(n,x'')` >> fs[]) 1346 >- (fs[] >> Cases_on `x''` >> fs[] >> metis_tac[]) 1347 ) 1348 >> metis_tac[FINITE_LIST_TO_SET,IMAGE_FINITE] 1349 ) 1350 >- simp[concr2AbstrAA_def] 1351 ) 1352 >> `!i x. (MEM i ids ��� lookup i G2.nodeInfo = SOME x) ==> 1353 (set x.frmls ��� reachableFromSetGBA abstr_gba {set q | inGBA g q})` 1354 by (rpt strip_tac >> `i ��� domain g.nodeInfo` by fs[] 1355 >> simp[reachableFromSetGBA_def,reachableFromGBA_def] 1356 >> `lookup i g.nodeInfo = lookup i G2.nodeInfo` by fs[] 1357 >> qexists_tac `set (x'.frmls)` >> simp[RTC_REFL] 1358 >> `inGBA g x'.frmls` by ( 1359 simp[inGBA_def,EXISTS_MEM,MEM_MAP] 1360 >> qexists_tac `x'` >> fs[MEM_EQUAL_SET] 1361 >> metis_tac[SND,MEM_toAList] 1362 ) 1363 >> metis_tac[] 1364 ) 1365 >> `(���i x. MEM i new_ids 1366 ��� (lookup i G2.nodeInfo = SOME x) 1367 ��� ((set x.frmls ��� reachableFromSetGBA abstr_gba {set q | inGBA g q}) 1368 ))` 1369 by ( 1370 rpt gen_tac >> strip_tac 1371 >> rename[`lookup i G2.nodeInfo = SOME n`] 1372 >> `MEM n.frmls NEW_NODES` by metis_tac[SOME_11] 1373 >> qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER] 1374 >> qunabbrev_tac `TRNS` >> fs[MEM_MAP,ONLY_MINIMAL_MEM] 1375 >> qabbrev_tac `TRNS = 1376 gba_trans_concr 1377 (CAT_OPTIONS 1378 (MAP (concr_extrTrans g_AA) 1379 (CAT_OPTIONS 1380 (MAP 1381 (��f. 1382 OPTION_MAP FST 1383 (findNode (��(i,l). l.frml = f) 1384 g_AA)) node.frmls))))` 1385 >> qabbrev_tac `TO_SUCS = 1386 ��(cE,f). 1387 (edgeLabelGBA cE.pos cE.neg f,cE.sucs)` 1388 >> qabbrev_tac `W_FINAL = ��cE. (cE,get_acc_set acc cE)` 1389 >> qabbrev_tac `abstr_ce = concr2AbstractEdge (set aP) cE` 1390 >> `abstr_ce ��� 1391 set (MAP (concr2AbstractEdge (set aP)) TRNS)` by ( 1392 simp[MEM_MAP] >> qunabbrev_tac `abstr_ce` >> fs[] 1393 >> metis_tac[] 1394 ) 1395 >> qabbrev_tac `ce_lists = 1396 CAT_OPTIONS 1397 (MAP (concr_extrTrans g_AA) 1398 (CAT_OPTIONS 1399 (MAP 1400 (��f. 1401 OPTION_MAP FST 1402 (findNode (��(i,l). l.frml = f) g_AA)) 1403 node.frmls)))` 1404 >> qabbrev_tac `zpd = ZIP (node.frmls,ce_lists)` 1405 >> qabbrev_tac `L = 1406 MAP 1407 (��f. 1408 OPTION_MAP FST 1409 (findNode (��(i,l). l.frml = f) g_AA)) 1410 node.frmls` 1411 >> `EVERY IS_SOME L` by ( 1412 qunabbrev_tac `L` >> fs[] >> simp[EVERY_MEM] 1413 >> rpt strip_tac >> fs[MEM_MAP] 1414 >> Cases_on `e` >> fs[IS_SOME_DEF] 1415 >> `inGBA g node.frmls` by ( 1416 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `node` 1417 >> simp[MEM_MAP,MEM_EQUAL_SET] 1418 >> metis_tac[MEM_toAList,SND] 1419 ) 1420 >> `set node.frmls ��� 1421 POW (removeStatesSimpl (ltl2vwaa f)).states` 1422 by metis_tac[] 1423 >> fs[concr2AbstrAA_def] 1424 >> `f' ��� (removeStatesSimpl (ltl2vwaa f)).states` 1425 by metis_tac[MEM,IN_POW,SUBSET_DEF] 1426 >> `f' ��� concr2Abstr_states g_AA` 1427 by (fs[ALTER_A_component_equality] >> metis_tac[]) 1428 >> fs[concr2Abstr_states_def,findNode_def] 1429 >> rename[`f1 = x1.frml`,`n1 ��� domain g_AA.nodeInfo`] 1430 >> `(��(i,l). l.frml = f1) (n1,x1)` by fs[] 1431 >> metis_tac[FIND_LEMM,NOT_SOME_NONE,MEM_toAList] 1432 ) 1433 >> `EVERY IS_SOME 1434 (MAP (concr_extrTrans g_AA) (CAT_OPTIONS L))` by ( 1435 simp[EVERY_MEM] >> rpt strip_tac >> fs[MEM_MAP] 1436 >> rename[`MEM some_id (CAT_OPTIONS L)`] 1437 >> simp[concr_extrTrans_def] 1438 >> Cases_on `lookup some_id g_AA.followers` >> fs[] 1439 >-(qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1440 >> fs[findNode_def] 1441 >> `MEM z (toAList g_AA.nodeInfo)` 1442 by metis_tac[FIND_LEMM2] 1443 >> Cases_on `z` >> fs[wfg_def] 1444 >> rw[] 1445 >> metis_tac[MEM_toAList,domain_lookup,wfg_def, 1446 NOT_SOME_NONE] 1447 ) 1448 >- ( 1449 fs[] >> rpt strip_tac 1450 >> Q.HO_MATCH_ABBREV_TAC `IS_SOME H` >> Cases_on `H` 1451 >> fs[IS_SOME_DEF] 1452 >> `some_id ��� (domain g_AA.nodeInfo)` 1453 by metis_tac[domain_lookup,wfg_def] 1454 >> metis_tac[domain_lookup,NOT_SOME_NONE] 1455 ) 1456 ) 1457 >> `LENGTH node.frmls = LENGTH ce_lists` by ( 1458 qunabbrev_tac `ce_lists` 1459 >> qunabbrev_tac `L` 1460 >> metis_tac[LENGTH_MAP,CAT_OPTIONS_LENGTH] 1461 ) 1462 >> `MAP FST zpd = node.frmls` by ( 1463 qunabbrev_tac `zpd` >> fs[] 1464 >> metis_tac[MAP_ZIP] 1465 ) 1466 >> `ALL_DISTINCT (MAP FST zpd)` 1467 by metis_tac[frml_ad_def] 1468 >> `abstr_ce ��� 1469 d_conj_set 1470 (set (MAP (��(q,d). 1471 (q,set (MAP 1472 (concr2AbstractEdge (set aP)) d))) zpd)) 1473 (POW (set aP))` 1474 by metis_tac[MAP_ZIP,LENGTH_COUNT_LIST,GBA_TRANS_LEMM] 1475 >> simp[reachableFromSetGBA_def,reachableFromGBA_def, 1476 stepGBA_def] 1477 >> qunabbrev_tac `abstr_gba` >> simp[vwaa2gba_def] 1478 >> `isVeryWeakAlterA (concr2AbstrAA (concrAA g_AA init aP))` 1479 by metis_tac[] 1480 >> simp[gba_trans_def] 1481 >> simp[d_gen_def,removeStatesSimpl_def] 1482 >> qexists_tac `set node.frmls` >> simp[] >> strip_tac 1483 >- ( 1484 Q.HO_MATCH_ABBREV_TAC `Q^* (set node.frmls) (set cE.sucs)` 1485 >> `Q (set node.frmls) (set cE.sucs)` 1486 suffices_by metis_tac[RTC_SUBSET] 1487 >> qunabbrev_tac `Q` >> simp[] >> qexists_tac `FST abstr_ce` 1488 >> simp[minimal_elements_rrestrict] 1489 >> simp[minimal_elements_def] 1490 >> `!q_i q_nL q q_trns. 1491 (findNode (��(i,l). l.frml = q) g_AA = SOME (q_i,q_nL)) 1492 ��� (q_nL.frml = q) ��� MEM q node.frmls 1493 ��� concr_extrTrans g_AA q_i = SOME q_trns 1494 ==> MEM (q_nL.frml,q_trns) zpd` by ( 1495 qunabbrev_tac `zpd` >> simp[MEM_ZIP] >> rpt strip_tac 1496 >> `?ind_q. EL ind_q node.frmls = q_nL.frml 1497 ��� ind_q < LENGTH node.frmls` 1498 by metis_tac[MEM_EL] 1499 >> qexists_tac `ind_q` >> fs[] 1500 >> qunabbrev_tac `ce_lists` >> rw[] 1501 >> `LENGTH node.frmls = 1502 LENGTH (MAP (concr_extrTrans g_AA) 1503 (CAT_OPTIONS L))` by ( 1504 fs[CAT_OPTIONS_LENGTH] 1505 ) 1506 >> `SOME 1507 (EL ind_q (CAT_OPTIONS (MAP (concr_extrTrans g_AA) 1508 (CAT_OPTIONS L)))) = 1509 (EL ind_q (MAP (concr_extrTrans g_AA) 1510 (CAT_OPTIONS L)))` by 1511 metis_tac[CAT_OPTIONS_EL] 1512 >> `EL ind_q (MAP (concr_extrTrans g_AA) 1513 (CAT_OPTIONS L)) = 1514 (concr_extrTrans g_AA (EL ind_q (CAT_OPTIONS L)))` 1515 by fs[EL_MAP,LENGTH_MAP] 1516 >> `LENGTH L = LENGTH node.frmls` by ( 1517 qunabbrev_tac `L` 1518 >> fs[LENGTH_MAP] 1519 ) 1520 >> `SOME (EL ind_q (CAT_OPTIONS L)) = 1521 EL ind_q L` by metis_tac[CAT_OPTIONS_EL] 1522 >> `EL ind_q L = SOME q_i` by ( 1523 qunabbrev_tac `L` >> simp[EL_MAP] 1524 ) 1525 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[] 1526 >> metis_tac[SOME_11] 1527 ) 1528 >> `{(q,(removeStatesSimpl (ltl2vwaa f)).trans q) | 1529 MEM q node.frmls} = 1530 set 1531 (MAP (��(q,d). 1532 (q,set (MAP (concr2AbstractEdge (set aP)) d))) 1533 zpd)` by ( 1534 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 1535 >- ( 1536 simp[MEM_MAP] 1537 >> `?i nL. findNode (��(i,l). l.frml = q) g_AA = SOME (i,nL)` 1538 by ( 1539 fs[findNode_def,concr2AbstrAA_def, 1540 ALTER_A_component_equality] 1541 >> `inGBA g node.frmls` by ( 1542 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `node` 1543 >> simp[MEM_MAP,MEM_EQUAL_SET] 1544 >> metis_tac[MEM_toAList,SND] 1545 ) 1546 >> `set node.frmls ��� 1547 POW (concr2Abstr_states g_AA)` 1548 by metis_tac[] 1549 >> `q ��� concr2Abstr_states g_AA` 1550 by metis_tac[IN_POW,SUBSET_DEF] 1551 >> fs[concr2Abstr_states_def] 1552 >> rename[`SOME x2 = lookup n1 g_AA.nodeInfo` ] 1553 >> rw[] 1554 >> `(��(i,l). l.frml = x2.frml) (n1,x2)` by fs[] 1555 >> `���y. FIND (��(i,l). l.frml = x2.frml) 1556 (toAList g_AA.nodeInfo) = SOME y` 1557 by metis_tac[FIND_LEMM,MEM_toAList] 1558 >> qexists_tac `FST y` >> qexists_tac `SND y` >> fs[] 1559 ) 1560 >> rename[`findNode _ g_AA = SOME (q_i,q_nL)`] 1561 >> `?q_trns. SOME q_trns = concr_extrTrans g_AA q_i 1562 ��� MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 1563 ��� (q_nL.frml = q)` by ( 1564 fs[findNode_def] 1565 >> `MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 1566 ��� ((��(i,l). l.frml = q) (q_i,q_nL))` 1567 by metis_tac[FIND_LEMM2] 1568 >> `IS_SOME (lookup q_i g_AA.followers)` suffices_by ( 1569 rpt strip_tac >> simp[concr_extrTrans_def] >> fs[] 1570 >> Cases_on `lookup q_i g_AA.followers` 1571 >> fs[IS_SOME_DEF] 1572 >> metis_tac[wfg_def,domain_lookup] 1573 ) 1574 >> Cases_on `lookup q_i g_AA.followers` 1575 >> fs[IS_SOME_DEF] 1576 >> metis_tac[wfg_def,domain_lookup,MEM_toAList, 1577 NOT_SOME_NONE] 1578 ) 1579 >> qexists_tac `(q,q_trns)` >> simp[] 1580 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 1581 >> `?fls. lookup q_i g_AA.followers = SOME fls` by ( 1582 metis_tac[domain_lookup,MEM_toAList,wfg_def,SOME_11] 1583 ) 1584 >> `���n cT. 1585 concr_extrTrans g_AA q_i = SOME cT 1586 ��� lookup q_i g_AA.nodeInfo = SOME n 1587 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 1588 concrTrans g_AA (set aP) n.frml` 1589 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 1590 >> first_x_assum (qspec_then `q_i` mp_tac) 1591 >> simp[]) 1592 >> fs[] >> `q_nL = n'` by metis_tac[MEM_toAList,SOME_11] 1593 >> rw[] 1594 ) 1595 >- ( 1596 rename[`MEM edge _`] >> fs[MEM_MAP] 1597 >> rename[`MEM cE zpd`] >> Cases_on `cE` 1598 >> fs[] >> qunabbrev_tac `zpd` 1599 >> rename[`MEM (q,q_trans) _`] >> POP_ASSUM mp_tac 1600 >> simp[MEM_ZIP] >> rpt strip_tac 1601 >- ( 1602 `inGBA g node.frmls` by ( 1603 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `node` 1604 >> simp[MEM_MAP,MEM_EQUAL_SET] 1605 >> metis_tac[MEM_toAList,SND] 1606 ) 1607 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 1608 >> `set node.frmls ��� 1609 POW (concr2Abstr_states g_AA)` 1610 by metis_tac[] 1611 >> `q ��� concr2Abstr_states g_AA` 1612 by metis_tac[IN_POW,SUBSET_DEF,EL_MEM] 1613 >> fs[concr2Abstr_states_def] 1614 >> rename[`q_i ��� domain _`,`q = q_nL.frml`] 1615 >> `findNode (��(n,l). l.frml = q) g_AA 1616 = SOME (q_i,q_nL)` 1617 by metis_tac[UNIQUE_NODE_FIND_LEMM] 1618 >> `?q_trns. concr_extrTrans g_AA q_i = SOME q_trns` 1619 by ( 1620 simp[concr_extrTrans_def] 1621 >> Cases_on `lookup q_i g_AA.followers` >> fs[] 1622 >- metis_tac[wfg_def,NOT_SOME_NONE,domain_lookup] 1623 >- metis_tac[] 1624 ) 1625 >> rw[] 1626 >> `MEM (q_nL.frml,q_trns) (ZIP (node.frmls,ce_lists))` 1627 by metis_tac[EL_MEM] 1628 >> `���k. k < LENGTH node.frmls 1629 ��� (q_nL.frml,q_trns) = (EL k node.frmls,EL k ce_lists)` 1630 by metis_tac[MEM_ZIP] 1631 >> `EL k node.frmls = q_nL.frml` by fs[] 1632 >> `k = n'` by metis_tac[ALL_DISTINCT_EL_IMP] 1633 >> fs[] 1634 >> `?fls. lookup q_i g_AA.followers = SOME fls` 1635 by metis_tac[wfg_def,domain_lookup] 1636 >> `���n cT. 1637 concr_extrTrans g_AA q_i = SOME cT 1638 ��� lookup q_i g_AA.nodeInfo = SOME n 1639 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 1640 concrTrans g_AA (set aP) n.frml` 1641 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 1642 >> first_x_assum (qspec_then `q_i` mp_tac) 1643 >> simp[] >> rpt strip_tac 1644 >> first_x_assum (qspec_then `set aP` mp_tac) 1645 >> fs[] 1646 ) 1647 >> metis_tac[SOME_11] 1648 ) 1649 >- metis_tac[EL_MEM] 1650 ) 1651 ) 1652 >> `set node.frmls ��� 1653 POW (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 1654 `inGBA g node.frmls` suffices_by ( 1655 fs[vwaa2gba_def,concr2AbstrAA_def,ALTER_A_component_equality] 1656 >> metis_tac[] 1657 ) 1658 >> simp[inGBA_def,EXISTS_MEM,MEM_MAP] 1659 >> qexists_tac `node` >> fs[MEM_EQUAL_SET] 1660 >> qexists_tac `(id,node)` >> fs[] 1661 >> metis_tac[MEM_toAList] 1662 ) 1663 >> fs[] 1664 >> `abstr_ce ��� 1665 d_conj_set 1666 {(q,(concr2AbstrAA (concrAA g_AA init aP)).trans q) | 1667 MEM q node.frmls} (POW (set aP))` by ( 1668 fs[concr2AbstrAA_def,ALTER_A_component_equality] 1669 >> metis_tac[] 1670 ) 1671 >> `(FST abstr_ce,set cE.sucs) = abstr_ce` by ( 1672 qunabbrev_tac `abstr_ce` 1673 >> Cases_on `cE` >> fs[concr2AbstractEdge_def] 1674 ) 1675 >> fs[] 1676 >> `(concr2AbstrAA (concrAA g_AA init aP)).alphabet = 1677 POW (set aP)` by fs[concr2AbstrAA_def] 1678 >> rpt strip_tac >> fs[] >> rename[`abstr_ce = abstr_ce2`] 1679 >> `abstr_ce2 ��� 1680 set (MAP (concr2AbstractEdge (set aP)) TRNS)` by ( 1681 IMP_RES_TAC GBA_TRANS_LEMM 1682 >> first_x_assum (qspec_then `set aP` mp_tac) >> fs[] 1683 >> rpt strip_tac >> qunabbrev_tac `TRNS` >> fs[] 1684 >> metis_tac[MAP_ZIP] 1685 ) 1686 >> POP_ASSUM mp_tac >> simp[MEM_MAP] >> strip_tac 1687 >> rename[`MEM ce2 TRNS`] >> fs[] 1688 >> `ce2 = cE \/ ~concr_min_rel (W_FINAL ce2) y` 1689 by ( 1690 first_x_assum (qspec_then `W_FINAL ce2` mp_tac) 1691 >> strip_tac 1692 >> qunabbrev_tac `W_FINAL` >> fs[] 1693 >> Cases_on `ce2 = cE` >> fs[] >> Cases_on `y` >> fs[] 1694 >> rw[] 1695 ) 1696 >> fs[] 1697 >> `���e1_lab e1_sucs e2_lab e2_sucs. 1698 MEM_SUBSET ce2.pos aP ��� MEM_SUBSET ce2.neg aP ��� 1699 MEM_SUBSET ce2.sucs (graphStates g_AA) ��� MEM_SUBSET cE.pos aP ��� 1700 MEM_SUBSET cE.neg aP ��� MEM_SUBSET cE.sucs (graphStates g_AA) ��� 1701 ((e1_lab,e1_sucs) = concr2AbstractEdge (set aP) ce2) ��� 1702 ((e2_lab,e2_sucs) = concr2AbstractEdge (set aP) cE) 1703 ��� (((e1_lab,e1_sucs),e2_lab,e2_sucs) ��� 1704 tr_less_general {acc_cond abstrAA f | MEM f (MAP FST acc)} (set node.frmls) ��� 1705 tlg_concr (ce2,get_acc_set acc ce2) (cE,get_acc_set acc cE))` by ( 1706 HO_MATCH_MP_TAC TLG_CONCR_LEMM >> qexists_tac `f` 1707 >> qexists_tac `init` >> fs[] >> metis_tac[] 1708 ) 1709 >> fs[] 1710 >> first_x_assum (qspec_then `FST abstr_ce2` mp_tac) 1711 >> rpt strip_tac 1712 >> first_x_assum (qspec_then `SND abstr_ce2` mp_tac) 1713 >> rpt strip_tac 1714 >> first_x_assum (qspec_then `FST abstr_ce` mp_tac) 1715 >> rpt strip_tac 1716 >> first_x_assum (qspec_then `SND abstr_ce` mp_tac) 1717 >> `!ce. MEM ce TRNS ==> 1718 (MEM_SUBSET ce.pos aP 1719 ��� MEM_SUBSET ce.neg aP 1720 ��� MEM_SUBSET ce.sucs (graphStates g_AA))` by ( 1721 qunabbrev_tac `TRNS` >> fs[] >> gen_tac >> strip_tac 1722 >> simp[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 1723 >> rpt strip_tac >> rename[`MEM x _`] 1724 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.pos` 1725 by metis_tac[GBA_TRANS_LEMM3] 1726 >> qunabbrev_tac `ce_lists` 1727 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 1728 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 1729 ) 1730 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.neg` 1731 by metis_tac[GBA_TRANS_LEMM3] 1732 >> qunabbrev_tac `ce_lists` 1733 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 1734 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 1735 ) 1736 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.sucs` 1737 by metis_tac[GBA_TRANS_LEMM3] 1738 >> qunabbrev_tac `ce_lists` 1739 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 1740 >> qunabbrev_tac `L` >> fs[MEM_MAP] >> Cases_on `z` 1741 >> fs[] >> rw[] 1742 >> `MEM (q,r) (toAList g_AA.nodeInfo)` by ( 1743 fs[findNode_def] >> metis_tac[FIND_LEMM2] 1744 ) 1745 >> `?fls. lookup q g_AA.followers = SOME fls` by ( 1746 metis_tac[domain_lookup,MEM_toAList,wfg_def,SOME_11] 1747 ) 1748 >> `���n cT. 1749 (concr_extrTrans g_AA q = SOME cT) 1750 ��� (lookup q g_AA.nodeInfo = SOME n) 1751 ��� (set (MAP (concr2AbstractEdge (set aP)) cT) = 1752 concrTrans g_AA (set aP) n.frml)` 1753 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 1754 >> first_x_assum (qspec_then `q` mp_tac) 1755 >> simp[] 1756 ) 1757 >> `l = cT` by metis_tac[SOME_11] >> rw[] 1758 >> `concr2AbstractEdge (set aP) ce' ��� 1759 concrTrans g_AA (set aP) n'.frml` by ( 1760 metis_tac[MEM_MAP,SET_EQ_SUBSET,SUBSET_DEF] 1761 ) 1762 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 1763 >> rw[] 1764 >> fs[isValidAlterA_def,concr2Abstr_states_def] 1765 >> `n'.frml ��� (removeStatesSimpl (ltl2vwaa f)).states` 1766 by (rw[] >> metis_tac[domain_lookup]) 1767 >> Cases_on `concr2AbstractEdge (set aP) ce'` 1768 >> fs[] 1769 >> `r' ��� (removeStatesSimpl (ltl2vwaa f)).states` 1770 by metis_tac[] 1771 >> rw[] >> simp[graphStates_def,MEM_MAP] 1772 >> `r' ��� 1773 {x.frml | 1774 ���n. (SOME x = lookup n g_AA.nodeInfo) 1775 ��� (n ��� domain g_AA.nodeInfo)}` by metis_tac[] 1776 >> Cases_on `ce'` 1777 >> fs[concr2AbstractEdge_def] >> rw[] 1778 >> `x ��� 1779 {x.frml | 1780 ���n. (SOME x = lookup n g_AA.nodeInfo) 1781 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 1782 >> fs[] >> metis_tac[MEM_toAList,SND,FST] 1783 ) 1784 ) 1785 >> `(MEM_SUBSET ce2.pos aP ��� MEM_SUBSET ce2.neg aP) 1786 ��� (MEM_SUBSET ce2.sucs (graphStates g_AA) ��� MEM_SUBSET cE.pos aP) 1787 ��� (MEM_SUBSET cE.neg aP ��� MEM_SUBSET cE.sucs (graphStates g_AA)) 1788 ��� ((FST abstr_ce2,SND abstr_ce2) = concr2AbstractEdge (set aP) ce2) 1789 ��� ((FST abstr_ce,SND abstr_ce) = concr2AbstractEdge (set aP) cE)` 1790 by (rpt strip_tac >> fs[]) 1791 >> simp[] 1792 >> qunabbrev_tac `W_FINAL` >> fs[all_acc_cond_def] 1793 >> `{acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f' | 1794 MEM f' (MAP FST acc)} = 1795 {acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f | 1796 f | f ��� (concr2AbstrAA (concrAA g_AA init aP)).final}` 1797 by ( 1798 `���f. MEM f (MAP FST acc) ��� f ��� concr2Abstr_final g_AA` 1799 by metis_tac[VALID_ACC_LEMM] 1800 >> simp[SET_EQ_SUBSET,SUBSET_DEF,concr2AbstrAA_def] 1801 >> rpt strip_tac 1802 ) 1803 >> Cases_on `y` >> fs[concr_min_rel_def] 1804 >- metis_tac[] 1805 >- (`abstr_ce2 = abstr_ce` by ( 1806 Cases_on `cE` >> Cases_on `ce2` 1807 >> simp[concr2AbstractEdge_def] 1808 >> fs[concrEdge_component_equality] 1809 >> `!x y. MEM_EQUAL x y ==> 1810 MEM_SUBSET x y ��� MEM_SUBSET y x` 1811 by metis_tac[MEM_EQUAL_SET,MEM_SUBSET_SET_TO_LIST, 1812 SET_EQ_SUBSET] 1813 >> simp[SET_EQ_SUBSET] >> rpt strip_tac 1814 >- metis_tac[TRANSFORMLABEL_SUBSET] 1815 >- metis_tac[TRANSFORMLABEL_SUBSET] 1816 >- metis_tac[MEM_EQUAL_SET,SET_EQ_SUBSET] 1817 >- metis_tac[MEM_EQUAL_SET,SET_EQ_SUBSET] 1818 ) 1819 >> rw[] 1820 ) 1821 >- (rw[] >> Cases_on `cE` >> Cases_on `ce2` 1822 >> simp[concr2AbstractEdge_def] 1823 >> fs[concrEdge_component_equality,MEM_EQUAL_SET] 1824 >> rename[`_ (set aP) pos1 neg1 = _ (set aP) pos2 neg2`] 1825 >> `pos1 = (concrEdge pos1 neg1 l1).pos` by fs[] 1826 >> `neg1 = (concrEdge pos1 neg1 l1).neg` by fs[] 1827 >> `pos2 = (concrEdge pos2 neg2 l1').pos` by fs[] 1828 >> `neg2 = (concrEdge pos2 neg2 l1').neg` by fs[] 1829 >> metis_tac[TRNS_IS_EMPTY_LEMM,MEM_SUBSET_SET_TO_LIST] 1830 ) 1831 ) 1832 >- (qexists_tac `node.frmls` >> simp[inGBA_def,EXISTS_MEM] 1833 >> qexists_tac `node` >> simp[MEM_MAP,MEM_EQUAL_SET] 1834 >> metis_tac[MEM_toAList,SND] 1835 ) 1836 ) 1837 >> rpt conj_tac 1838 >- metis_tac[] 1839 >- (rpt strip_tac >> fs[] >> rename[`set x ��� _`] 1840 >> `set x ��� {set x | inGBA g x} ��� set (MAP set NEW_NODES)` by ( 1841 `set x ��� {set x | inGBA G1 x}` by (simp[] >> metis_tac[]) 1842 >> metis_tac[UNION_DEF] 1843 ) 1844 >> fs[UNION_DEF] 1845 >- metis_tac[] 1846 >- (qunabbrev_tac `NEW_NODES` >> fs[MEM_MAP,MEM_FILTER] 1847 >> `?id nL. (lookup id G2.nodeInfo = SOME nL) 1848 ��� (MEM id new_ids) ��� (set nL.frmls = set x)` by ( 1849 fs[inGBA_def,EXISTS_MEM,MEM_MAP] 1850 >> rename[`MEM y2 (toAList G2.nodeInfo)`] >> Cases_on `y2` 1851 >> rename[`MEM (id,nL) (toAList G2.nodeInfo)`] 1852 >> qexists_tac `id` >> qexists_tac `nL` 1853 >> fs[MEM_EQUAL_SET,MEM_toAList] 1854 >> first_x_assum (qspec_then `nL` mp_tac) >> rw[] 1855 >> rename[`set n1.frmls = set _`] 1856 >> first_x_assum (qspec_then `(id,n1)` mp_tac) 1857 >> simp[] >> rpt strip_tac 1858 >> `id ��� {x | MEM x new_ids ��� x ��� domain g.nodeInfo}` 1859 by metis_tac[domain_lookup] 1860 >> `~(id ��� domain g.nodeInfo)` 1861 by metis_tac[MEM_toAList,domain_lookup] 1862 >> fs[] 1863 ) 1864 >> `set nL.frmls ��� 1865 reachableFromSetGBA abstr_gba {set q | inGBA g q}` 1866 by metis_tac[] 1867 >> rename[`MEM y1 TRNS`, `y = _ y1`] >> Cases_on `y1` >> fs[] 1868 >> rw[] >> POP_ASSUM mp_tac >> simp[reachableFromSetGBA_def] 1869 >> rpt strip_tac >> fs[] >> rw[] 1870 >> rename[`inGBA g q_inter`] 1871 >> `set q_inter ��� reachableFromSetGBA abstr_gba abstr_gba.initial` 1872 by metis_tac[] 1873 >> POP_ASSUM mp_tac >> simp[reachableFromSetGBA_def] 1874 >> rpt strip_tac >> rename[`q_init ��� abstr_gba.initial`] 1875 >> qexists_tac `q_init` >> fs[] >> fs[reachableFromGBA_def] 1876 >> metis_tac[RTC_RTC] 1877 ) 1878 ) 1879 >- (rpt strip_tac 1880 >- (`domain g.nodeInfo ��� domain G2.nodeInfo` by metis_tac[SUBSET_UNION] 1881 >> metis_tac[SUBSET_DEF] 1882 ) 1883 >- metis_tac[domain_lookup] 1884 ) 1885 >- fs[expandGBA_def] 1886 >- (rpt strip_tac >> rename[`set x ��� POW _`] 1887 >> `set x ��� {set x | inGBA g x} ��� set (MAP set NEW_NODES)` by ( 1888 `set x ��� {set x | inGBA G1 x}` by (simp[] >> metis_tac[]) 1889 >> metis_tac[UNION_DEF] 1890 ) 1891 >> fs[UNION_DEF] 1892 >- metis_tac[] 1893 >- (qunabbrev_tac `NEW_NODES` >> qunabbrev_tac `TRNS` 1894 >> fs[MEM_MAP,MEM_FILTER,ONLY_MINIMAL_MEM] 1895 >> qabbrev_tac `L = 1896 CAT_OPTIONS 1897 (MAP (concr_extrTrans g_AA) 1898 (CAT_OPTIONS 1899 (MAP 1900 (��f. 1901 OPTION_MAP FST 1902 (findNode (��(i,l). l.frml = f) g_AA)) 1903 node.frmls)))` 1904 >> `!s. MEM s cE.sucs ==> 1905 ���l ce. MEM l L ��� MEM ce l ��� MEM s ce.sucs` 1906 by metis_tac[GBA_TRANS_LEMM3] 1907 >> simp[IN_POW,SUBSET_DEF] >> rpt strip_tac 1908 >> rename[`MEM s cE.sucs`] 1909 >> `���l ce. MEM l L ��� MEM ce l ��� MEM s ce.sucs` by fs[] 1910 >> qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1911 >> `MEM s (graphStates g_AA) ��� ALL_DISTINCT ce.sucs` 1912 by metis_tac[CONCR_EXTRTRANS_NODES] 1913 >> fs[graphStates_def,MEM_MAP,concr2AbstrAA_def, 1914 concr2Abstr_states_def] 1915 >> rename[`MEM y3 (toAList g_AA.nodeInfo)`] 1916 >> Cases_on `y3` >> fs[] 1917 >> metis_tac[MEM_toAList,domain_lookup] 1918 ) 1919 ) 1920 >- (fs[frml_ad_def] >> rpt strip_tac 1921 >> `i ��� (set new_ids ��� domain g.nodeInfo)` by metis_tac[] 1922 >> fs[UNION_DEF] 1923 >- (`MEM n.frmls NEW_NODES` by metis_tac[SOME_11] 1924 >> qunabbrev_tac `NEW_NODES` >> qunabbrev_tac `TRNS` 1925 >> fs[MEM_MAP,MEM_FILTER,ONLY_MINIMAL_MEM] 1926 >> qabbrev_tac `L = 1927 CAT_OPTIONS 1928 (MAP (concr_extrTrans g_AA) 1929 (CAT_OPTIONS 1930 (MAP 1931 (��f. 1932 OPTION_MAP FST 1933 (findNode (��(i,l). l.frml = f) g_AA)) 1934 node.frmls)))` 1935 >> qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1936 >> metis_tac[GBA_TRANS_LEMM1] 1937 ) 1938 >- metis_tac[] 1939 ) 1940 ) 1941 ); 1942 1943val one_step_closed_apart_l_def = Define` 1944 one_step_closed_apart_l abstrAA g l = 1945 !nL qs i. 1946 (lookup i g.nodeInfo = SOME nL) 1947 ��� (set nL.frmls = qs) 1948 ��� ~(MEM i l) 1949 ==> (!ys. stepGBA (vwaa2gba abstrAA) qs (set ys) 1950 ==> inGBA g ys)`; 1951 1952val one_step_closed_def = Define` 1953 one_step_closed abstrAA g = 1954 (!xs. inGBA g xs 1955 ==> (!ys. stepGBA (vwaa2gba abstrAA) (set xs) (set ys) 1956 ==> inGBA g ys) 1957 )`; 1958 1959val EXPGBA_ALL_REACHABLE = store_thm 1960 ("EXPGBA_ALL_REACHABLE", 1961 ``!abstrAA f init aP g_AA acc ids g g2. 1962 (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 1963 ��� (abstrAA = removeStatesSimpl (ltl2vwaa f)) 1964 ��� (wfg g_AA) 1965 ��� (until_iff_final g_AA) 1966 ��� (!id cT. (concr_extrTrans g_AA id = SOME cT) 1967 ==> (!ce. MEM ce cT 1968 ==> (MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)) 1969 ) 1970 ��� (valid_acc aP g_AA acc) 1971 ��� (unique_node_formula g_AA) ��� (flws_sorted g_AA) 1972 ��� (expandGBA g_AA acc ids g = SOME g2) 1973 ��� (!i. MEM i ids ==> i ��� domain g.nodeInfo) 1974 ��� (wfg g) 1975 ��� frml_ad g 1976 ��� (one_step_closed_apart_l abstrAA g ids) 1977 ==> (one_step_closed abstrAA g2)``, 1978 gen_tac >> gen_tac >> gen_tac >> gen_tac 1979 >> HO_MATCH_MP_TAC (theorem "expandGBA_ind") >> strip_tac 1980 >- (fs[one_step_closed_def] >> rpt strip_tac >> fs[expandGBA_def] >> rw[] 1981 >> fs[one_step_closed_apart_l_def,inGBA_def,EXISTS_MEM,MEM_MAP] 1982 >> Cases_on `y` >> fs[] >> rw[] 1983 >> first_x_assum (qspec_then `n` mp_tac) >> strip_tac 1984 >> first_x_assum (qspec_then `q` mp_tac) 1985 >> `lookup q g.nodeInfo = SOME n` by metis_tac[MEM_toAList] 1986 >> simp[] >> strip_tac 1987 >> first_x_assum (qspec_then `ys` mp_tac) 1988 >> `set xs = set n.frmls` by metis_tac[MEM_EQUAL_SET] 1989 >> fs[] 1990 ) 1991 >- (strip_tac >> strip_tac >> strip_tac >> strip_tac >> strip_tac 1992 >> strip_tac >> strip_tac >> strip_tac 1993 >> fs[] 1994 >> simp[one_step_closed_def] >> strip_tac >> strip_tac >> strip_tac 1995 >> `?node. lookup id g.nodeInfo = SOME node` by metis_tac[domain_lookup] 1996 >> first_x_assum (qspec_then `node` mp_tac) >> simp[] 1997 >> strip_tac 1998 >> qabbrev_tac `TRNS = 1999 ONLY_MINIMAL 2000 concr_min_rel 2001 (MAP (��cE. (cE,get_acc_set acc cE)) 2002 (gba_trans_concr 2003 (CAT_OPTIONS 2004 (MAP (concr_extrTrans g_AA) 2005 (CAT_OPTIONS 2006 (MAP 2007 (��f. 2008 OPTION_MAP FST 2009 (findNode (��(i,l). l.frml = f) 2010 g_AA)) node.frmls))))))` 2011 >> Cases_on `FOLDR 2012 (��n (ids,g). 2013 if inGBA g n then (ids,g) 2014 else (g.next::ids,addNodeToGBA g n)) ([],g) 2015 (FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS))` 2016 >> fs[] >> rename[`_ = (new_ids,G1)`] 2017 >> `wfg G1` by ( 2018 `G1 = SND (new_ids,G1)` by fs[] 2019 >> metis_tac[ADDNODE_GBA_WFG_FOLDR] 2020 ) 2021 >> qabbrev_tac `NEW_NODES = 2022 FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS)` 2023 >> `{set x | inGBA G1 x} = 2024 {set x | inGBA g x} ��� set (MAP set NEW_NODES)` by ( 2025 `G1 = SND (new_ids,G1)` by fs[] 2026 >> metis_tac[ADDNODE_GBA_FOLDR,WF_IMP_SUFFWFG] 2027 ) 2028 >> `���x. MEM x (MAP FST TRNS) ��� inGBA G1 x.sucs` by ( 2029 rpt strip_tac >> rename[`MEM qs (MAP FST TRNS)`] 2030 >> fs[MEM_MAP] >> rename[`MEM t TRNS`] >> Cases_on `t` >> fs[] 2031 >> rw[] 2032 >> `(MEM q.sucs NEW_NODES) \/ (inGBA g q.sucs)` by ( 2033 qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER] 2034 >> Cases_on `inGBA g q.sucs` >> fs[] 2035 >> simp[MEM_MAP] 2036 >> qexists_tac `(q,r)` >> fs[] 2037 ) 2038 >- (`MEM ((set q.sucs) ) (MAP set NEW_NODES)` 2039 by (fs[MEM_MAP] >> metis_tac[]) 2040 >> `(set q.sucs) ��� {set x | inGBA G1 x }` 2041 by metis_tac[IN_UNION] 2042 >> fs[] 2043 >> metis_tac[IN_GBA_MEM_EQUAL,MEM,MEM_EQUAL_SET] 2044 ) 2045 >- (`(set q.sucs) ���{set x | inGBA g x}` 2046 by (fs[MEM_MAP] >> metis_tac[]) 2047 >> `(set q.sucs) ��� {set x | inGBA G1 x}` 2048 by metis_tac[IN_UNION] 2049 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 2050 ) 2051 ) 2052 >> `!x. MEM x 2053 (MAP SND (MAP 2054 (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) 2055 TRNS)) ==> inGBA G1 x` by ( 2056 rpt strip_tac >> fs[MEM_MAP] >> rename[`MEM t TRNS`] 2057 >> Cases_on `t` >> fs[] 2058 >> `FST (q,r) = q` by fs[] >> metis_tac[] 2059 ) 2060 >> `(set new_ids ��� domain g.nodeInfo = domain G1.nodeInfo) 2061 ��� g.next ��� G1.next` by metis_tac[FST,SND,ADDNODE_GBA_DOM_FOLDR] 2062 >> `���g2. 2063 (FOLDR 2064 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 2065 (SOME G1) 2066 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) TRNS) = 2067 SOME g2) ��� G1.nodeInfo = g2.nodeInfo ��� wfg g2` by ( 2068 HO_MATCH_MP_TAC ADDEDGE_GBA_FOLDR_LEMM 2069 >> rpt conj_tac 2070 >- metis_tac[] 2071 >- metis_tac[domain_lookup,IN_UNION] 2072 >- metis_tac[] 2073 ) 2074 >> rename[`wfg G2`] >> first_x_assum (qspec_then `G2` mp_tac) >> fs[] 2075 >> `(���id cT. 2076 (concr_extrTrans g_AA id = SOME cT) ��� 2077 ���ce. MEM ce cT ��� MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)` 2078 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[]) 2079 >> simp[] >> Q.HO_MATCH_ABBREV_TAC `(!g2. A g2 ==> B g2) ==> C` 2080 >> `B g2 ==> C` by ( 2081 qunabbrev_tac `B` >> simp[one_step_closed_def] 2082 >> metis_tac[] 2083 ) 2084 >> `A g2` suffices_by fs[] >> qunabbrev_tac `A` >> fs[] 2085 >> qabbrev_tac `abstr_gba = 2086 vwaa2gba (concr2AbstrAA (concrAA g_AA init aP))` 2087 >> `!x. inGBA G1 x = inGBA G2 x` by simp[inGBA_def] 2088 >> `!x. set x ��� reachableFromSetGBA abstr_gba {set q | inGBA g q } 2089 ==> (set x ��� reachableFromSetGBA abstr_gba 2090 {set q | inGBA G2 q })` by ( 2091 simp[reachableFromSetGBA_def] >> rpt strip_tac 2092 >> `set q ��� {set x | inGBA g x}` by (simp[] >> metis_tac[]) 2093 >> `set q ��� {set x | inGBA G1 x}` by metis_tac[IN_UNION] 2094 >> fs[] >> metis_tac[] 2095 ) 2096 >> `(���i. 2097 i ��� domain g.nodeInfo ��� 2098 lookup i g.nodeInfo = lookup i G1.nodeInfo) 2099 ��� (���i. 2100 MEM i new_ids ��� 2101 ���n. 2102 lookup i G1.nodeInfo = SOME n ��� MEM n.frmls NEW_NODES)` 2103 by metis_tac[WF_IMP_SUFFWFG,ADDNODE_GBA_FOLDR,SND,FST] 2104 >> `isVeryWeakAlterA abstrAA ��� isValidAlterA abstrAA 2105 ��� (FINITE abstrAA.states) 2106 ��� (abstrAA.alphabet = POW (set aP))` by ( 2107 fs[] >> rpt strip_tac 2108 >- metis_tac[REDUCE_STATE_IS_WEAK,LTL2WAA_ISWEAK, 2109 LTL2WAA_ISVALID] 2110 >- metis_tac[REDUCE_STATE_IS_VALID,LTL2WAA_ISVALID] 2111 >- (simp[concr2AbstrAA_def,concr2Abstr_states_def] 2112 >> `FINITE {x.frml | ?n. MEM (n,x) (toAList g_AA.nodeInfo)}` 2113 suffices_by ( 2114 Q.HO_MATCH_ABBREV_TAC `FINITE S1 ==> FINITE S2` 2115 >> `S1 = S2` suffices_by fs[] 2116 >> qunabbrev_tac `S1` >> qunabbrev_tac `S2` 2117 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2118 >> metis_tac[MEM_toAList,domain_lookup] 2119 ) 2120 >> `{x.frml | ���n. MEM (n,x) (toAList g_AA.nodeInfo)} = 2121 IMAGE (��(i,n). n.frml) (set (toAList g_AA.nodeInfo))` by ( 2122 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2123 >- (qexists_tac `(n,x')` >> fs[]) 2124 >- (fs[] >> Cases_on `x'` >> fs[] >> metis_tac[]) 2125 ) 2126 >> metis_tac[FINITE_LIST_TO_SET,IMAGE_FINITE] 2127 ) 2128 >- simp[concr2AbstrAA_def] 2129 ) 2130 >> rpt conj_tac 2131 >- metis_tac[] 2132 >- fs[expandGBA_def] 2133 >- (rpt strip_tac 2134 >- (`domain g.nodeInfo ��� domain G2.nodeInfo` by metis_tac[SUBSET_UNION] 2135 >> metis_tac[SUBSET_DEF] 2136 ) 2137 >- metis_tac[domain_lookup] 2138 ) 2139 >- (fs[frml_ad_def] >> rpt strip_tac 2140 >> `i ��� (set new_ids ��� domain g.nodeInfo)` by metis_tac[] 2141 >> fs[UNION_DEF] 2142 >- (`MEM n.frmls NEW_NODES` by metis_tac[SOME_11] 2143 >> qunabbrev_tac `NEW_NODES` >> qunabbrev_tac `TRNS` 2144 >> fs[MEM_MAP,MEM_FILTER,ONLY_MINIMAL_MEM] 2145 >> qabbrev_tac `L = 2146 CAT_OPTIONS 2147 (MAP (concr_extrTrans g_AA) 2148 (CAT_OPTIONS 2149 (MAP 2150 (��f. 2151 OPTION_MAP FST 2152 (findNode (��(i,l). l.frml = f) g_AA)) 2153 node.frmls)))` 2154 >> qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 2155 >> metis_tac[GBA_TRANS_LEMM1] 2156 ) 2157 >- metis_tac[] 2158 ) 2159 >- (simp[one_step_closed_apart_l_def] >> rpt strip_tac 2160 >> rename[`inGBA G2 ys`] 2161 >> `i ��� domain G2.nodeInfo` by metis_tac[domain_lookup] 2162 >> `i ��� domain g.nodeInfo` by metis_tac[SET_EQ_SUBSET,SUBSET_DEF,IN_UNION] 2163 >> fs[one_step_closed_apart_l_def] 2164 >> `lookup i g.nodeInfo = SOME nL` by metis_tac[SOME_11] 2165 >> Cases_on `i = id` 2166 >- (rw[] 2167 >> fs[stepGBA_def] 2168 >> `?ys1. 2169 MEM_EQUAL ys1 ys 2170 ��� (MEM ys1 2171 (MAP SND 2172 (MAP (��(cE,f). 2173 (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) 2174 TRNS)))` suffices_by ( 2175 rpt strip_tac >> metis_tac[IN_GBA_MEM_EQUAL] 2176 ) 2177 >> fs[stepGBA_def] >> qunabbrev_tac `abstr_gba` 2178 >> fs[vwaa2gba_def] 2179 >> Cases_on `isVeryWeakAlterA 2180 (concr2AbstrAA (concrAA g_AA init aP))` >> fs[] 2181 >- ( 2182 fs[gba_trans_def,d_gen_def,minimal_elements_def] 2183 >> qunabbrev_tac `TRNS` >> fs[MEM_MAP,ONLY_MINIMAL_MEM] 2184 >> qabbrev_tac `TRNS = 2185 gba_trans_concr 2186 (CAT_OPTIONS 2187 (MAP (concr_extrTrans g_AA) 2188 (CAT_OPTIONS 2189 (MAP 2190 (��f. 2191 OPTION_MAP FST 2192 (findNode (��(i,l). l.frml = f) 2193 g_AA)) node.frmls))))` 2194 >> qabbrev_tac `TO_SUCS = 2195 ��(cE,f). 2196 (edgeLabelGBA cE.pos cE.neg f,cE.sucs)` 2197 >> qabbrev_tac `W_FINAL = ��cE. (cE,get_acc_set acc cE)` 2198 >> qabbrev_tac `ce_lists = 2199 CAT_OPTIONS 2200 (MAP (concr_extrTrans g_AA) 2201 (CAT_OPTIONS 2202 (MAP 2203 (��f. 2204 OPTION_MAP FST 2205 (findNode (��(i,l). l.frml = f) g_AA)) 2206 node.frmls)))` 2207 >> qabbrev_tac `zpd = ZIP (node.frmls,ce_lists)` 2208 >> qabbrev_tac `L = 2209 MAP 2210 (��f. 2211 OPTION_MAP FST 2212 (findNode (��(i,l). l.frml = f) g_AA)) 2213 node.frmls` 2214 >> `EVERY IS_SOME L` by ( 2215 qunabbrev_tac `L` >> fs[] >> simp[EVERY_MEM] 2216 >> rpt strip_tac >> fs[MEM_MAP] 2217 >> Cases_on `e` >> fs[IS_SOME_DEF] 2218 >> `inGBA g node.frmls` by ( 2219 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `node` 2220 >> simp[MEM_MAP,MEM_EQUAL_SET] 2221 >> metis_tac[MEM_toAList,SND] 2222 ) 2223 >> `set node.frmls ��� 2224 POW (removeStatesSimpl (ltl2vwaa f)).states` 2225 by metis_tac[] 2226 >> fs[concr2AbstrAA_def] 2227 >> `f' ��� (removeStatesSimpl (ltl2vwaa f)).states` 2228 by metis_tac[MEM,IN_POW,SUBSET_DEF] 2229 >> `f' ��� concr2Abstr_states g_AA` 2230 by (fs[ALTER_A_component_equality] >> metis_tac[]) 2231 >> fs[concr2Abstr_states_def,findNode_def] 2232 >> rename[`f1 = x1.frml`,`n1 ��� domain g_AA.nodeInfo`] 2233 >> `(��(i,l). l.frml = f1) (n1,x1)` by fs[] 2234 >> metis_tac[FIND_LEMM,NOT_SOME_NONE,MEM_toAList] 2235 ) 2236 >> `EVERY IS_SOME 2237 (MAP (concr_extrTrans g_AA) (CAT_OPTIONS L))` by ( 2238 simp[EVERY_MEM] >> rpt strip_tac >> fs[MEM_MAP] 2239 >> rename[`MEM some_id (CAT_OPTIONS L)`] 2240 >> simp[concr_extrTrans_def] 2241 >> Cases_on `lookup some_id g_AA.followers` >> fs[] 2242 >-(qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 2243 >> fs[findNode_def] 2244 >> `MEM z (toAList g_AA.nodeInfo)` 2245 by metis_tac[FIND_LEMM2] 2246 >> Cases_on `z` >> fs[wfg_def] 2247 >> rw[] 2248 >> metis_tac[MEM_toAList,domain_lookup,wfg_def, 2249 NOT_SOME_NONE] 2250 ) 2251 >- ( 2252 fs[] >> rpt strip_tac 2253 >> Q.HO_MATCH_ABBREV_TAC `IS_SOME H` >> Cases_on `H` 2254 >> fs[IS_SOME_DEF] 2255 >> `some_id ��� (domain g_AA.nodeInfo)` 2256 by metis_tac[domain_lookup,wfg_def] 2257 >> metis_tac[domain_lookup,NOT_SOME_NONE] 2258 ) 2259 ) 2260 >> `LENGTH node.frmls = LENGTH ce_lists` by ( 2261 qunabbrev_tac `ce_lists` 2262 >> qunabbrev_tac `L` 2263 >> metis_tac[LENGTH_MAP,CAT_OPTIONS_LENGTH] 2264 ) 2265 >> `MAP FST zpd = node.frmls` by ( 2266 qunabbrev_tac `zpd` >> fs[] 2267 >> metis_tac[MAP_ZIP] 2268 ) 2269 >> `ALL_DISTINCT (MAP FST zpd)` by metis_tac[frml_ad_def] 2270 >> rw[] 2271 >> `!q_i q_nL q q_trns. 2272 (findNode (��(i,l). l.frml = q) g_AA = SOME (q_i,q_nL)) 2273 ��� (q_nL.frml = q) ��� MEM q nL.frmls 2274 ��� concr_extrTrans g_AA q_i = SOME q_trns 2275 ==> MEM (q_nL.frml,q_trns) zpd` by ( 2276 qunabbrev_tac `zpd` >> simp[MEM_ZIP] >> rpt strip_tac 2277 >> `?ind_q. EL ind_q nL.frmls = q_nL.frml 2278 ��� ind_q < LENGTH nL.frmls` 2279 by metis_tac[MEM_EL] 2280 >> qexists_tac `ind_q` >> fs[] 2281 >> qunabbrev_tac `ce_lists` >> rw[] 2282 >> `LENGTH nL.frmls = 2283 LENGTH (MAP (concr_extrTrans g_AA) 2284 (CAT_OPTIONS L))` by ( 2285 fs[CAT_OPTIONS_LENGTH] 2286 ) 2287 >> `SOME 2288 (EL ind_q (CAT_OPTIONS (MAP (concr_extrTrans g_AA) 2289 (CAT_OPTIONS L)))) = 2290 (EL ind_q (MAP (concr_extrTrans g_AA) 2291 (CAT_OPTIONS L)))` by 2292 metis_tac[CAT_OPTIONS_EL] 2293 >> `EL ind_q (MAP (concr_extrTrans g_AA) 2294 (CAT_OPTIONS L)) = 2295 (concr_extrTrans g_AA (EL ind_q (CAT_OPTIONS L)))` 2296 by fs[EL_MAP,LENGTH_MAP] 2297 >> `LENGTH L = LENGTH nL.frmls` by ( 2298 qunabbrev_tac `L` 2299 >> fs[LENGTH_MAP] 2300 ) 2301 >> `SOME (EL ind_q (CAT_OPTIONS L)) = 2302 EL ind_q L` by metis_tac[CAT_OPTIONS_EL] 2303 >> `EL ind_q L = SOME q_i` by ( 2304 qunabbrev_tac `L` >> simp[EL_MAP] 2305 ) 2306 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[] 2307 >> metis_tac[SOME_11] 2308 ) 2309 >> `{(q,(removeStatesSimpl (ltl2vwaa f)).trans q) | 2310 MEM q nL.frmls} = 2311 set 2312 (MAP (��(q,d). 2313 (q,set (MAP (concr2AbstractEdge (set aP)) d))) 2314 zpd)` by ( 2315 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2316 >- ( 2317 simp[MEM_MAP] 2318 >> `?i nL. findNode (��(i,l). l.frml = q) g_AA = SOME (i,nL)` 2319 by ( 2320 fs[findNode_def,concr2AbstrAA_def, 2321 ALTER_A_component_equality] 2322 >> `inGBA g nL.frmls` by ( 2323 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `nL` 2324 >> simp[MEM_MAP,MEM_EQUAL_SET] 2325 >> metis_tac[MEM_toAList,SND] 2326 ) 2327 >> `set nL.frmls ��� 2328 POW (concr2Abstr_states g_AA)` 2329 by metis_tac[] 2330 >> `q ��� concr2Abstr_states g_AA` 2331 by metis_tac[IN_POW,SUBSET_DEF] 2332 >> fs[concr2Abstr_states_def] 2333 >> rename[`SOME x2 = lookup n1 g_AA.nodeInfo` ] 2334 >> rw[] 2335 >> `(��(i,l). l.frml = x2.frml) (n1,x2)` by fs[] 2336 >> `���y. FIND (��(i,l). l.frml = x2.frml) 2337 (toAList g_AA.nodeInfo) = SOME y` 2338 by metis_tac[FIND_LEMM,MEM_toAList] 2339 >> qexists_tac `FST y` >> qexists_tac `SND y` >> fs[] 2340 ) 2341 >> rename[`findNode _ g_AA = SOME (q_i,q_nL)`] 2342 >> `?q_trns. SOME q_trns = concr_extrTrans g_AA q_i 2343 ��� MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 2344 ��� (q_nL.frml = q)` by ( 2345 fs[findNode_def] 2346 >> `MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 2347 ��� ((��(i,l). l.frml = q) (q_i,q_nL))` 2348 by metis_tac[FIND_LEMM2] 2349 >> `IS_SOME (lookup q_i g_AA.followers)` suffices_by ( 2350 rpt strip_tac >> simp[concr_extrTrans_def] >> fs[] 2351 >> Cases_on `lookup q_i g_AA.followers` 2352 >> fs[IS_SOME_DEF] 2353 >> metis_tac[wfg_def,domain_lookup] 2354 ) 2355 >> Cases_on `lookup q_i g_AA.followers` 2356 >> fs[IS_SOME_DEF] 2357 >> metis_tac[wfg_def,domain_lookup,MEM_toAList, 2358 NOT_SOME_NONE] 2359 ) 2360 >> qexists_tac `(q,q_trns)` >> simp[] 2361 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 2362 >> `?fls. lookup q_i g_AA.followers = SOME fls` by ( 2363 metis_tac[domain_lookup,MEM_toAList,wfg_def,SOME_11] 2364 ) 2365 >> `���n cT. 2366 concr_extrTrans g_AA q_i = SOME cT 2367 ��� lookup q_i g_AA.nodeInfo = SOME n 2368 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 2369 concrTrans g_AA (set aP) n.frml` 2370 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 2371 >> first_x_assum (qspec_then `q_i` mp_tac) 2372 >> simp[]) 2373 >> fs[] >> `q_nL = n` by metis_tac[MEM_toAList,SOME_11] 2374 >> rw[] 2375 ) 2376 >- ( 2377 rename[`MEM edge _`] >> fs[MEM_MAP] 2378 >> rename[`MEM cE zpd`] >> Cases_on `cE` 2379 >> fs[] >> qunabbrev_tac `zpd` 2380 >> rename[`MEM (q,q_trans) _`] >> POP_ASSUM mp_tac 2381 >> simp[MEM_ZIP] >> rpt strip_tac 2382 >- ( 2383 `inGBA g nL.frmls` by ( 2384 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `nL` 2385 >> simp[MEM_MAP,MEM_EQUAL_SET] 2386 >> metis_tac[MEM_toAList,SND] 2387 ) 2388 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 2389 >> `set nL.frmls ��� 2390 POW (concr2Abstr_states g_AA)` 2391 by metis_tac[] 2392 >> `q ��� concr2Abstr_states g_AA` 2393 by metis_tac[IN_POW,SUBSET_DEF,EL_MEM] 2394 >> fs[concr2Abstr_states_def] 2395 >> rename[`q_i ��� domain _`,`q = q_nL.frml`] 2396 >> `findNode (��(n,l). l.frml = q) g_AA 2397 = SOME (q_i,q_nL)` 2398 by metis_tac[UNIQUE_NODE_FIND_LEMM] 2399 >> `?q_trns. concr_extrTrans g_AA q_i = SOME q_trns` 2400 by ( 2401 simp[concr_extrTrans_def] 2402 >> Cases_on `lookup q_i g_AA.followers` >> fs[] 2403 >- metis_tac[wfg_def,NOT_SOME_NONE,domain_lookup] 2404 >- metis_tac[] 2405 ) 2406 >> rw[] 2407 >> `MEM (q_nL.frml,q_trns) (ZIP (nL.frmls,ce_lists))` 2408 by metis_tac[EL_MEM] 2409 >> `���k. k < LENGTH nL.frmls 2410 ��� (q_nL.frml,q_trns) = (EL k nL.frmls,EL k ce_lists)` 2411 by metis_tac[MEM_ZIP] 2412 >> `EL k nL.frmls = q_nL.frml` by fs[] 2413 >> `k = n` by metis_tac[ALL_DISTINCT_EL_IMP] 2414 >> fs[] 2415 >> `?fls. lookup q_i g_AA.followers = SOME fls` 2416 by metis_tac[wfg_def,domain_lookup] 2417 >> `���n cT. 2418 concr_extrTrans g_AA q_i = SOME cT 2419 ��� lookup q_i g_AA.nodeInfo = SOME n 2420 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 2421 concrTrans g_AA (set aP) n.frml` 2422 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 2423 >> first_x_assum (qspec_then `q_i` mp_tac) 2424 >> simp[] >> rpt strip_tac 2425 >> first_x_assum (qspec_then `set aP` mp_tac) 2426 >> fs[] 2427 ) 2428 >> metis_tac[SOME_11] 2429 ) 2430 >- metis_tac[EL_MEM] 2431 ) 2432 ) 2433 >> IMP_RES_TAC GBA_TRANS_LEMM 2434 >> first_x_assum (qspec_then `set aP` mp_tac) >> simp[] 2435 >> strip_tac 2436 >> `(a,set ys) ��� 2437 set 2438 (MAP (concr2AbstractEdge (set aP)) 2439 (gba_trans_concr (MAP SND zpd)))` by metis_tac[] 2440 >> fs[MEM_MAP] >> rename[`MEM edge _`] >> Cases_on `edge` 2441 >> rename[`MEM (concrEdge pos neg sucs) _`] 2442 >> fs[concr2AbstractEdge_def] >> qexists_tac `sucs` 2443 >> `MEM_EQUAL sucs ys` by metis_tac[MEM_EQUAL_SET] 2444 >> simp[] >> qabbrev_tac `cE = concrEdge pos neg sucs` 2445 >> qexists_tac ` 2446 (edgeLabelGBA cE.pos cE.neg (get_acc_set acc cE), 2447 cE.sucs)` 2448 >> simp[] >> `sucs = cE.sucs` by (qunabbrev_tac `cE` >> fs[]) 2449 >> simp[] >> qexists_tac `(cE,get_acc_set acc cE)` 2450 >> qunabbrev_tac `TO_SUCS` >> qunabbrev_tac `W_FINAL` >> simp[] 2451 >> `!ce. MEM ce TRNS ==> 2452 (MEM_SUBSET ce.pos aP 2453 ��� MEM_SUBSET ce.neg aP 2454 ��� MEM_SUBSET ce.sucs (graphStates g_AA))` by ( 2455 qunabbrev_tac `TRNS` >> fs[] >> gen_tac >> strip_tac 2456 >> simp[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 2457 >> rpt strip_tac >> rename[`MEM x _`] 2458 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.pos` 2459 by metis_tac[GBA_TRANS_LEMM3] 2460 >> qunabbrev_tac `ce_lists` 2461 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 2462 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 2463 ) 2464 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.neg` 2465 by metis_tac[GBA_TRANS_LEMM3] 2466 >> qunabbrev_tac `ce_lists` 2467 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 2468 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 2469 ) 2470 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.sucs` 2471 by metis_tac[GBA_TRANS_LEMM3] 2472 >> qunabbrev_tac `ce_lists` 2473 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 2474 >> qunabbrev_tac `L` >> fs[MEM_MAP] >> Cases_on `z` 2475 >> fs[] >> rw[] 2476 >> `MEM (q,r) (toAList g_AA.nodeInfo)` by ( 2477 fs[findNode_def] >> metis_tac[FIND_LEMM2] 2478 ) 2479 >> `?fls. lookup q g_AA.followers = SOME fls` 2480 by metis_tac[domain_lookup,MEM_toAList, 2481 wfg_def,SOME_11] 2482 >> `���n cT. 2483 (concr_extrTrans g_AA q = SOME cT) 2484 ��� (lookup q g_AA.nodeInfo = SOME n) 2485 ��� (set (MAP (concr2AbstractEdge (set aP)) cT) = 2486 concrTrans g_AA (set aP) n.frml)` 2487 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 2488 >> first_x_assum (qspec_then `q` mp_tac) 2489 >> simp[] 2490 ) 2491 >> `l = cT` by metis_tac[SOME_11] >> rw[] 2492 >> `concr2AbstractEdge (set aP) ce' ��� 2493 concrTrans g_AA (set aP) n.frml` by ( 2494 metis_tac[MEM_MAP,SET_EQ_SUBSET,SUBSET_DEF] 2495 ) 2496 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 2497 >> rw[] 2498 >> fs[isValidAlterA_def,concr2Abstr_states_def] 2499 >> `n.frml ��� (removeStatesSimpl (ltl2vwaa f)).states` 2500 by (rw[] >> metis_tac[domain_lookup]) 2501 >> Cases_on `concr2AbstractEdge (set aP) ce'` 2502 >> fs[] 2503 >> `r' ��� (removeStatesSimpl (ltl2vwaa f)).states` 2504 by metis_tac[] 2505 >> rw[] >> simp[graphStates_def,MEM_MAP] 2506 >> `r' ��� 2507 {x.frml | 2508 ���n. (SOME x = lookup n g_AA.nodeInfo) 2509 ��� (n ��� domain g_AA.nodeInfo)}` by metis_tac[] 2510 >> Cases_on `ce'` 2511 >> fs[concr2AbstractEdge_def] >> rw[] 2512 >> `x ��� 2513 {x.frml | 2514 ���n. (SOME x = lookup n g_AA.nodeInfo) 2515 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 2516 >> fs[] >> metis_tac[MEM_toAList,SND,FST] 2517 ) 2518 ) 2519 >> qunabbrev_tac `TRNS` >> simp[] 2520 >> `MAP SND zpd = ce_lists` 2521 by (qunabbrev_tac `zpd` >> metis_tac[MAP_ZIP]) 2522 >> fs[] >> rpt strip_tac >> rename[`MEM cE2 _`] 2523 >> first_x_assum 2524 (qspec_then `concr2AbstractEdge (set aP) cE2` mp_tac) 2525 >> Q.HO_MATCH_ABBREV_TAC `(Q1 ==> Q2) ==> F` 2526 >> `Q2 ==> F` by ( 2527 qunabbrev_tac `Q2` >> simp[] >> Cases_on `y` 2528 >> `~(cE = cE2)` by metis_tac[] 2529 >> Cases_on `~MEM_EQUAL q.sucs cE.sucs` 2530 >- (Cases_on `cE2` >> simp[concr2AbstractEdge_def] 2531 >> fs[MEM_EQUAL_SET,concrEdge_component_equality] 2532 >> rw[] >> metis_tac[] 2533 ) 2534 >- (Cases_on `~ trns_is_empty cE ��� ~ trns_is_empty q` 2535 >- (fs[concr_min_rel_def] >> Cases_on `cE2` 2536 >> `!l1 l2. ~(set l1 ��� set l2) ==> ~MEM_SUBSET l1 l2` 2537 by fs[MEM_SUBSET_SET_TO_LIST] 2538 >> fs[MEM_EQUAL_SET,concrEdge_component_equality] 2539 >> simp[concr2AbstractEdge_def] 2540 >> rw[] 2541 >> `(concrEdge q.pos q.neg q.sucs).pos = q.pos 2542 ��� (concrEdge q.pos q.neg q.sucs).neg = q.neg` 2543 by fs[] 2544 >> `���x. MEM x pos ��� MEM x q.pos 2545 ��� MEM x neg ��� MEM x q.neg ��� x ��� set aP` by ( 2546 metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF,MEM] 2547 ) >> CCONTR_TAC 2548 >> fs[] 2549 >> `set cE.pos ��� set aP 2550 ��� set cE.neg ��� set aP 2551 ��� set q.pos ��� set aP 2552 ��� set q.neg ��� set aP` 2553 by metis_tac[SUBSET_DEF] 2554 >> fs[SET_EQ_SUBSET] 2555 >> `~(transformLabel (set aP) pos neg = {})` 2556 by metis_tac[TRNS_IS_EMPTY_LEMM] 2557 >> `~(transformLabel (set aP) q.pos q.neg = {})` 2558 by metis_tac[TRNS_IS_EMPTY_LEMM] 2559 >> IMP_RES_TAC TRANSFORMLABEL_SUBSET2 2560 >> metis_tac[] 2561 ) 2562 >- (fs[concr_min_rel_def] >> Cases_on `cE2` 2563 >> fs[MEM_EQUAL_SET,concrEdge_component_equality] 2564 >> fs[concr2AbstractEdge_def] 2565 >> rw[] 2566 >> `(concrEdge q.pos q.neg q.sucs).pos = q.pos 2567 ��� (concrEdge q.pos q.neg q.sucs).neg = q.neg` 2568 by fs[] 2569 >> `set cE.pos ��� set aP 2570 ��� set cE.neg ��� set aP 2571 ��� set q.pos ��� set aP 2572 ��� set q.neg ��� set aP` 2573 by metis_tac[MEM_SUBSET_SET_TO_LIST] 2574 >> metis_tac[TRNS_IS_EMPTY_LEMM] 2575 ) 2576 ) 2577 ) 2578 >> `Q1` suffices_by metis_tac[] 2579 >> qunabbrev_tac `Q1` >> fs[] 2580 >> conj_tac 2581 >- metis_tac[MEM_MAP] 2582 >- (simp[rrestrict_def] >> conj_tac 2583 >- (`tlg_concr y (cE,get_acc_set acc cE)` by 2584 (Cases_on `y` >> fs[concr_min_rel_def]) 2585 >> Cases_on `y` >> rw[] 2586 >> qabbrev_tac `abstrAA = 2587 concr2AbstrAA (concrAA g_AA init aP)` 2588 >> `���e1_lab e1_sucs e2_lab e2_sucs. 2589 MEM_SUBSET cE2.pos aP ��� MEM_SUBSET cE2.neg aP ��� 2590 MEM_SUBSET cE2.sucs (graphStates g_AA) ��� MEM_SUBSET cE.pos aP ��� 2591 MEM_SUBSET cE.neg aP ��� MEM_SUBSET cE.sucs (graphStates g_AA) ��� 2592 ((e1_lab,e1_sucs) = concr2AbstractEdge (set aP) cE2) ��� 2593 ((e2_lab,e2_sucs) = concr2AbstractEdge (set aP) cE) 2594 ��� (((e1_lab,e1_sucs),e2_lab,e2_sucs) ��� 2595 tr_less_general 2596 {acc_cond abstrAA f | MEM f (MAP FST acc)} 2597 (set nL.frmls) ��� 2598 tlg_concr (cE2,get_acc_set acc cE2) 2599 (cE,get_acc_set acc cE))` by ( 2600 HO_MATCH_MP_TAC TLG_CONCR_LEMM >> qexists_tac `f` 2601 >> qexists_tac `init` >> fs[] >> metis_tac[] 2602 ) 2603 >> fs[] 2604 >> first_x_assum 2605 (qspec_then `transformLabel (set aP) cE2.pos cE2.neg` 2606 mp_tac) 2607 >> simp[] >> strip_tac 2608 >> first_x_assum (qspec_then `set cE2.sucs` mp_tac) 2609 >> simp[] >> strip_tac 2610 >> first_x_assum 2611 (qspec_then `transformLabel (set aP) cE.pos cE.neg` 2612 mp_tac) 2613 >> simp[] >> strip_tac 2614 >> first_x_assum (qspec_then `set cE.sucs` mp_tac) 2615 >> simp[] >> strip_tac 2616 >> fs[all_acc_cond_def] 2617 >> `{acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f' | 2618 MEM f' (MAP FST acc)} = 2619 {acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f | 2620 f | f ��� (concr2AbstrAA (concrAA g_AA init aP)).final}` 2621 by ( 2622 `���f. MEM f (MAP FST acc) ��� f ��� concr2Abstr_final g_AA` 2623 by metis_tac[VALID_ACC_LEMM] 2624 >> simp[SET_EQ_SUBSET,SUBSET_DEF,concr2AbstrAA_def] 2625 >> rpt strip_tac >> qexists_tac `f'` >> simp[] 2626 >> qunabbrev_tac `abstrAA` >> fs[concr2AbstrAA_def] 2627 ) 2628 >> Cases_on `cE` >> Cases_on `cE2` 2629 >> fs[concr2AbstractEdge_def] 2630 >> qunabbrev_tac `abstrAA` >> fs[concr2AbstrAA_def] 2631 >> metis_tac[] 2632 ) 2633 >- (metis_tac[MEM_MAP]) 2634 ) 2635 ) 2636 >- metis_tac[] 2637 ) 2638 >- (`inGBA g ys` by metis_tac[SOME_11] 2639 >> `set ys ��� ({set x | inGBA g x} ��� set (MAP set NEW_NODES))` 2640 by (simp[IN_UNION] >> metis_tac[]) 2641 >> `set ys ��� {set x | inGBA G2 x}` 2642 by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] 2643 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 2644 ) 2645 ) 2646 ) 2647 ); 2648 2649val EXPGBA_TRANS_AND_FINAL = store_thm 2650 ("EXPGBA_TRANS_AND_FINAL", 2651 ``!abstrAA f init aP g_AA acc ids g g2. 2652 (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 2653 ��� (abstrAA = removeStatesSimpl (ltl2vwaa f)) 2654 ��� (wfg g_AA) 2655 ��� (until_iff_final g_AA) 2656 ��� (!id cT. (concr_extrTrans g_AA id = SOME cT) 2657 ==> (!ce. MEM ce cT 2658 ==> (MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)) 2659 ) 2660 ��� (valid_acc aP g_AA acc) 2661 ��� (unique_node_formula g_AA) ��� (flws_sorted g_AA) 2662 ��� (expandGBA g_AA acc ids g = SOME g2) 2663 ��� (!i. MEM i ids ==> i ��� domain g.nodeInfo) 2664 ��� (!i. MEM i ids ==> (lookup i g.followers = SOME [])) 2665 ��� (wfg g) 2666 ��� (aP_correct abstrAA g aP) 2667 ��� (final_correct abstrAA g acc) 2668 ��� (trns_correct ids abstrAA g (set aP)) 2669 ��� (ALL_DISTINCT ids) 2670 ��� frml_ad g 2671 ��� ((!id fls. 2672 (lookup id g.followers = SOME fls) 2673 ==> (!eL s_id. 2674 MEM (eL,s_id) fls 2675 ==> s_id ��� domain g.nodeInfo))) 2676 ==> ((aP_correct abstrAA g2 aP) 2677 ��� (final_correct abstrAA g2 acc) 2678 ��� (trns_correct [] abstrAA g2 (set aP)) 2679 )``, 2680 gen_tac >> gen_tac >> gen_tac >> gen_tac 2681 >> HO_MATCH_MP_TAC (theorem "expandGBA_ind") >> strip_tac 2682 >- (rpt strip_tac >> fs[expandGBA_def] >> metis_tac[]) 2683 >- ( 2684 strip_tac >> strip_tac >> strip_tac >> strip_tac >> strip_tac 2685 >> strip_tac >> strip_tac >> strip_tac 2686 >> fs[] 2687 >> `?node. lookup id g.nodeInfo = SOME node` by metis_tac[domain_lookup] 2688 >> first_x_assum (qspec_then `node` mp_tac) >> simp[] 2689 >> strip_tac >> Q.HO_MATCH_ABBREV_TAC `P g2` 2690 >> qabbrev_tac `TRNS = 2691 ONLY_MINIMAL 2692 concr_min_rel 2693 (MAP (��cE. (cE,get_acc_set acc cE)) 2694 (gba_trans_concr 2695 (CAT_OPTIONS 2696 (MAP (concr_extrTrans g_AA) 2697 (CAT_OPTIONS 2698 (MAP 2699 (��f. 2700 OPTION_MAP FST 2701 (findNode (��(i,l). l.frml = f) 2702 g_AA)) node.frmls))))))` 2703 >> Cases_on `FOLDR 2704 (��n (ids,g). 2705 if inGBA g n then (ids,g) 2706 else (g.next::ids,addNodeToGBA g n)) ([],g) 2707 (FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS))` 2708 >> fs[] >> rename[`_ = (new_ids,G1)`] 2709 >> `wfg G1` by ( 2710 `G1 = SND (new_ids,G1)` by fs[] 2711 >> metis_tac[ADDNODE_GBA_WFG_FOLDR] 2712 ) 2713 >> qabbrev_tac `NEW_NODES = 2714 FILTER (��qs. ��inGBA g qs) (MAP (��(cE,fs). cE.sucs) TRNS)` 2715 >> `{set x | inGBA G1 x} = 2716 {set x | inGBA g x} ��� set (MAP set NEW_NODES)` by ( 2717 `G1 = SND (new_ids,G1)` by fs[] 2718 >> metis_tac[ADDNODE_GBA_FOLDR,WF_IMP_SUFFWFG] 2719 ) 2720 >> `���x. MEM x (MAP FST TRNS) ��� inGBA G1 x.sucs` by ( 2721 rpt strip_tac >> rename[`MEM qs (MAP FST TRNS)`] 2722 >> fs[MEM_MAP] >> rename[`MEM t TRNS`] >> Cases_on `t` >> fs[] 2723 >> rw[] 2724 >> `(MEM q.sucs NEW_NODES) \/ (inGBA g q.sucs)` by ( 2725 qunabbrev_tac `NEW_NODES` >> fs[MEM_FILTER] 2726 >> Cases_on `inGBA g q.sucs` >> fs[] 2727 >> simp[MEM_MAP] 2728 >> qexists_tac `(q,r)` >> fs[] 2729 ) 2730 >- (`MEM ((set q.sucs) ) (MAP set NEW_NODES)` 2731 by (fs[MEM_MAP] >> metis_tac[]) 2732 >> `(set q.sucs) ��� {set x | inGBA G1 x }` 2733 by metis_tac[IN_UNION] 2734 >> fs[] 2735 >> metis_tac[IN_GBA_MEM_EQUAL,MEM,MEM_EQUAL_SET] 2736 ) 2737 >- (`(set q.sucs) ���{set x | inGBA g x}` 2738 by (fs[MEM_MAP] >> metis_tac[]) 2739 >> `(set q.sucs) ��� {set x | inGBA G1 x}` 2740 by metis_tac[IN_UNION] 2741 >> fs[] >> metis_tac[IN_GBA_MEM_EQUAL,MEM_EQUAL_SET] 2742 ) 2743 ) 2744 >> `!x. MEM x 2745 (MAP SND (MAP 2746 (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) 2747 TRNS)) ==> inGBA G1 x` by ( 2748 rpt strip_tac >> fs[MEM_MAP] >> rename[`MEM t TRNS`] 2749 >> Cases_on `t` >> fs[] 2750 >> `FST (q,r) = q` by fs[] >> metis_tac[] 2751 ) 2752 >> `(set new_ids ��� domain g.nodeInfo = domain G1.nodeInfo) 2753 ��� g.next ��� G1.next` by metis_tac[FST,SND,ADDNODE_GBA_DOM_FOLDR] 2754 >> `���g2. 2755 (FOLDR 2756 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 2757 (SOME G1) 2758 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) TRNS) = 2759 SOME g2) ��� G1.nodeInfo = g2.nodeInfo ��� wfg g2` by ( 2760 HO_MATCH_MP_TAC ADDEDGE_GBA_FOLDR_LEMM 2761 >> rpt conj_tac 2762 >- metis_tac[] 2763 >- metis_tac[domain_lookup,IN_UNION] 2764 >- metis_tac[] 2765 ) 2766 >> rename[`wfg G2`] >> first_x_assum (qspec_then `G2` mp_tac) >> fs[] 2767 >> `(���id cT. 2768 (concr_extrTrans g_AA id = SOME cT) ��� 2769 ���ce. MEM ce cT ��� MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)` 2770 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[]) 2771 >> simp[] 2772 >> Q.HO_MATCH_ABBREV_TAC `(!g2. (A g2) ==> B g2) ==> P g2` 2773 >> `B g2 ==> P g2` by ( 2774 qunabbrev_tac `B` >> qunabbrev_tac `P` 2775 >> metis_tac[] 2776 ) 2777 >> `A g2` suffices_by fs[] >> qunabbrev_tac `A` >> fs[] 2778 >> qabbrev_tac `abstr_gba = 2779 vwaa2gba (concr2AbstrAA (concrAA g_AA init aP))` 2780 >> `!x. inGBA G1 x = inGBA G2 x` by simp[inGBA_def] 2781 >> `(���i. 2782 i ��� domain g.nodeInfo ��� 2783 (lookup i g.nodeInfo = lookup i G1.nodeInfo) 2784 ��� (lookup i g.followers = lookup i G1.followers)) 2785 ��� (���i. 2786 MEM i new_ids ��� 2787 ���n. 2788 lookup i G1.nodeInfo = SOME n ��� MEM n.frmls NEW_NODES 2789 ��� (lookup i G1.followers = SOME []) 2790 ��� (g.next <= i))` 2791 by metis_tac[WF_IMP_SUFFWFG,ADDNODE_GBA_FOLDR,SND,FST] 2792 >> `isVeryWeakAlterA abstrAA ��� isValidAlterA abstrAA 2793 ��� (FINITE abstrAA.states) 2794 ��� (abstrAA.alphabet = POW (set aP))` by ( 2795 fs[] >> rpt strip_tac 2796 >- metis_tac[REDUCE_STATE_IS_WEAK,LTL2WAA_ISWEAK, 2797 LTL2WAA_ISVALID] 2798 >- metis_tac[REDUCE_STATE_IS_VALID,LTL2WAA_ISVALID] 2799 >- (simp[concr2AbstrAA_def,concr2Abstr_states_def] 2800 >> `FINITE {x.frml | ?n. MEM (n,x) (toAList g_AA.nodeInfo)}` 2801 suffices_by ( 2802 Q.HO_MATCH_ABBREV_TAC `FINITE S1 ==> FINITE S2` 2803 >> `S1 = S2` suffices_by fs[] 2804 >> qunabbrev_tac `S1` >> qunabbrev_tac `S2` 2805 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2806 >> metis_tac[MEM_toAList,domain_lookup] 2807 ) 2808 >> `{x.frml | ���n. MEM (n,x) (toAList g_AA.nodeInfo)} = 2809 IMAGE (��(i,n). n.frml) (set (toAList g_AA.nodeInfo))` by ( 2810 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 2811 >- (qexists_tac `(n,x')` >> fs[]) 2812 >- (fs[] >> Cases_on `x'` >> fs[] >> metis_tac[]) 2813 ) 2814 >> metis_tac[FINITE_LIST_TO_SET,IMAGE_FINITE] 2815 ) 2816 >- simp[concr2AbstrAA_def] 2817 ) 2818 >> `!ls G fls. (FOLDR 2819 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 2820 (SOME G1) 2821 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) ls) = 2822 SOME G) 2823 ��� (lookup id G.followers = SOME fls) 2824 ==> ((!eL s_id. 2825 MEM (eL,s_id) fls 2826 ==> s_id ��� domain G.nodeInfo) 2827 ��� (!eL qs. 2828 (?s_id s_nL. 2829 MEM (eL,s_id) fls 2830 ��� (lookup s_id G.nodeInfo = SOME s_nL) 2831 ��� MEM_EQUAL s_nL.frmls qs) 2832 = 2833 (?s_list. 2834 MEM_EQUAL s_list qs 2835 ��� (MEM (eL,s_list) 2836 (MAP (��(cE,f). 2837 (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) 2838 ls)))))` by ( 2839 Induct_on `ls` >> fs[] >> strip_tac 2840 >- (strip_tac >> `fls = []` by metis_tac[domain_lookup,SOME_11] 2841 >> fs[] 2842 ) 2843 >- (rpt gen_tac >> strip_tac 2844 >> Cases_on `h` >> fs[] >> rename[`addEdgeToGBA G_int _ _ _ = _ _`] 2845 >> fs[addEdgeToGBA_def] 2846 >> Cases_on `findNode (��(i,q'). MEM_EQUAL q'.frmls q.sucs) G_int` 2847 >> fs[] >> Cases_on `x` >> fs[addEdge_def] 2848 >> fs[gfg_component_equality] 2849 >> `fls = ((edgeLabelGBA q.pos q.neg r,q')::followers_old)` 2850 by metis_tac[lookup_insert,SOME_11] 2851 >> rpt gen_tac >> simp[EQ_IMP_THM] >> strip_tac 2852 >- (rw[] 2853 >- metis_tac[findNode_def,FIND_LEMM2,MEM_toAList,domain_lookup] 2854 >- metis_tac[] 2855 ) 2856 >- (rw[] 2857 >- (qexists_tac `q.sucs` >> fs[] 2858 >> rename[`findNode _ _ = SOME (id1,nL1)`] 2859 >> `(��(i,q'). MEM_EQUAL q'.frmls q.sucs) (id1,nL1) 2860 ��� MEM (id1,nL1) (toAList G_int.nodeInfo)` 2861 by metis_tac[FIND_LEMM2,findNode_def] 2862 >> `s_nL = nL1` by metis_tac[MEM_toAList,SOME_11] 2863 >> rw[] >> fs[MEM_EQUAL_SET] 2864 ) 2865 >- metis_tac[] 2866 >- (rename[`findNode _ _ = SOME (id1,nL1)`] 2867 >> `(��(i,q'). MEM_EQUAL q'.frmls q.sucs) (id1,nL1) 2868 ��� MEM (id1,nL1) (toAList G_int.nodeInfo)` 2869 by metis_tac[FIND_LEMM2,findNode_def] 2870 >> qexists_tac `id1` >> fs[] >> qexists_tac `nL1` >> simp[] 2871 >> metis_tac[MEM_EQUAL_SET,MEM_toAList] 2872 ) 2873 >- metis_tac[] 2874 ) 2875 ) 2876 ) 2877 >> first_x_assum (qspec_then `TRNS` mp_tac) >> simp[] 2878 >> strip_tac 2879 >> `!ls G i. ~(i = id) ==> 2880 (FOLDR 2881 (��(eL,suc) g_opt. do g <- g_opt; addEdgeToGBA g id eL suc od) 2882 (SOME G1) 2883 (MAP (��(cE,f). (edgeLabelGBA cE.pos cE.neg f,cE.sucs)) ls) = 2884 SOME G) 2885 ==> (lookup i G.followers = lookup i G1.followers)` by ( 2886 Induct_on `ls` >> fs[] >> rpt strip_tac 2887 >> Cases_on `h` >> fs[] >> rename[`addEdgeToGBA G_int _ _ _ = _ _`] 2888 >> fs[addEdgeToGBA_def] 2889 >> Cases_on `findNode (��(i,q'). MEM_EQUAL q'.frmls q.sucs) G_int` 2890 >> fs[] >> Cases_on `x` >> fs[] 2891 >> fs[addEdge_def,gfg_component_equality] 2892 >> metis_tac[lookup_insert] 2893 ) 2894 >> first_x_assum (qspec_then `TRNS` mp_tac) >> simp[] >> strip_tac 2895 >> `aP_correct (concr2AbstrAA (concrAA g_AA init aP)) G2 aP 2896 ��� trns_correct (nub (ids ++ new_ids)) 2897 (concr2AbstrAA (concrAA g_AA init aP)) G2 (set aP) 2898 ��� final_correct (concr2AbstrAA (concrAA g_AA init aP)) G2 acc` by ( 2899 `!id fls nL. 2900 (lookup id G2.nodeInfo = SOME nL) 2901 ��� (lookup id G2.followers = SOME fls) 2902 ��� ((set nL.frmls) ��� POW abstrAA.states) 2903 ==> 2904 ((~MEM id (nub (ids ++ new_ids)) 2905 ==> 2906 (set 2907 (CAT_OPTIONS 2908 (MAP 2909 (��(eL,i). 2910 do 2911 s_nL <- lookup i G2.nodeInfo; 2912 SOME 2913 (transformLabel (set aP) eL.pos_lab eL.neg_lab, 2914 set s_nL.frmls) 2915 od) fls)) = gba_trans abstrAA (set nL.frmls) 2916 )) 2917 ��� (!eL s_id. 2918 MEM (eL,s_id) fls ��� 2919 MEM_SUBSET eL.pos_lab aP ��� MEM_SUBSET eL.neg_lab aP 2920 ) 2921 ��� (!eL s_id s_nL. 2922 MEM (eL,s_id) fls 2923 ��� (lookup s_id G2.nodeInfo = SOME s_nL) 2924 ==> ���u. 2925 MEM u eL.acc_set ��� 2926 MEM u 2927 (get_acc_set acc 2928 (concrEdge eL.pos_lab eL.neg_lab s_nL.frmls)))) 2929 ` suffices_by ( 2930 rpt strip_tac >> fs[aP_correct_def,trns_correct_def,final_correct_def] 2931 >> rpt strip_tac >> fs[] 2932 >- metis_tac[] 2933 >- metis_tac[] 2934 >- (first_x_assum(qspec_then `id'` mp_tac) >> simp[] 2935 ) 2936 >- metis_tac[] 2937 ) 2938 >> rpt gen_tac >> strip_tac 2939 >> rename[`lookup id2 G2.nodeInfo = SOME nL`] 2940 >> Cases_on `id = id2` >> fs[] 2941 >- ( 2942 `node = nL` by metis_tac[SOME_11] 2943 >> qunabbrev_tac `TRNS` >> fs[MEM_MAP,ONLY_MINIMAL_MEM] 2944 >> qabbrev_tac `TRNS = 2945 gba_trans_concr 2946 (CAT_OPTIONS 2947 (MAP (concr_extrTrans g_AA) 2948 (CAT_OPTIONS 2949 (MAP 2950 (��f. 2951 OPTION_MAP FST 2952 (findNode (��(i,l). l.frml = f) 2953 g_AA)) nL.frmls))))` 2954 >> qabbrev_tac `TO_SUCS = 2955 ��(cE,f). 2956 (edgeLabelGBA cE.pos cE.neg f,cE.sucs)` 2957 >> qabbrev_tac `W_FINAL = ��cE. (cE,get_acc_set acc cE)` 2958 >> qabbrev_tac `ce_lists = 2959 CAT_OPTIONS 2960 (MAP (concr_extrTrans g_AA) 2961 (CAT_OPTIONS 2962 (MAP 2963 (��f. 2964 OPTION_MAP FST 2965 (findNode (��(i,l). l.frml = f) g_AA)) 2966 nL.frmls)))` 2967 >> qabbrev_tac `zpd = ZIP (nL.frmls,ce_lists)` 2968 >> qabbrev_tac `L = 2969 MAP 2970 (��f. 2971 OPTION_MAP FST 2972 (findNode (��(i,l). l.frml = f) g_AA)) 2973 node.frmls` 2974 >> `EVERY IS_SOME L` by ( 2975 qunabbrev_tac `L` >> fs[] >> simp[EVERY_MEM] 2976 >> rpt strip_tac >> fs[MEM_MAP] 2977 >> Cases_on `e` >> fs[IS_SOME_DEF] 2978 >> `inGBA g node.frmls` by ( 2979 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `node` 2980 >> simp[MEM_MAP,MEM_EQUAL_SET] 2981 >> metis_tac[MEM_toAList,SND] 2982 ) 2983 >> `set node.frmls ��� 2984 POW (removeStatesSimpl (ltl2vwaa f)).states` 2985 by metis_tac[] 2986 >> fs[concr2AbstrAA_def] 2987 >> `f' ��� (removeStatesSimpl (ltl2vwaa f)).states` 2988 by metis_tac[MEM,IN_POW,SUBSET_DEF] 2989 >> `f' ��� concr2Abstr_states g_AA` 2990 by (fs[ALTER_A_component_equality] >> metis_tac[]) 2991 >> fs[concr2Abstr_states_def,findNode_def] 2992 >> rename[`f1 = x1.frml`,`n1 ��� domain g_AA.nodeInfo`] 2993 >> `(��(i,l). l.frml = f1) (n1,x1)` by fs[] 2994 >> metis_tac[FIND_LEMM,NOT_SOME_NONE,MEM_toAList] 2995 ) 2996 >> `EVERY IS_SOME 2997 (MAP (concr_extrTrans g_AA) (CAT_OPTIONS L))` by ( 2998 simp[EVERY_MEM] >> rpt strip_tac >> fs[MEM_MAP] 2999 >> rename[`MEM some_id (CAT_OPTIONS L)`] 3000 >> simp[concr_extrTrans_def] 3001 >> Cases_on `lookup some_id g_AA.followers` >> fs[] 3002 >-(qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 3003 >> fs[findNode_def] 3004 >> `MEM z (toAList g_AA.nodeInfo)` 3005 by metis_tac[FIND_LEMM2] 3006 >> Cases_on `z` >> fs[wfg_def] 3007 >> rw[] 3008 >> metis_tac[MEM_toAList,domain_lookup,wfg_def, 3009 NOT_SOME_NONE] 3010 ) 3011 >- ( 3012 fs[] >> rpt strip_tac 3013 >> Q.HO_MATCH_ABBREV_TAC `IS_SOME H` >> Cases_on `H` 3014 >> fs[IS_SOME_DEF] 3015 >> `some_id ��� (domain g_AA.nodeInfo)` 3016 by metis_tac[domain_lookup,wfg_def] 3017 >> metis_tac[domain_lookup,NOT_SOME_NONE] 3018 ) 3019 ) 3020 >> `LENGTH node.frmls = LENGTH ce_lists` by ( 3021 qunabbrev_tac `ce_lists` 3022 >> qunabbrev_tac `L` 3023 >> metis_tac[LENGTH_MAP,CAT_OPTIONS_LENGTH] 3024 ) 3025 >> `MAP FST zpd = node.frmls` by ( 3026 qunabbrev_tac `zpd` >> fs[] 3027 >> metis_tac[MAP_ZIP] 3028 ) 3029 >> `ALL_DISTINCT (MAP FST zpd)` by metis_tac[frml_ad_def] 3030 >> Q.HO_MATCH_ABBREV_TAC `GOAL` 3031 >> rw[] 3032 >> `!q_i q_nL q q_trns. 3033 (findNode (��(i,l). l.frml = q) g_AA = SOME (q_i,q_nL)) 3034 ��� (q_nL.frml = q) ��� MEM q nL.frmls 3035 ��� concr_extrTrans g_AA q_i = SOME q_trns 3036 ==> MEM (q_nL.frml,q_trns) zpd` by ( 3037 qunabbrev_tac `zpd` >> simp[MEM_ZIP] >> rpt strip_tac 3038 >> `?ind_q. EL ind_q nL.frmls = q_nL.frml 3039 ��� ind_q < LENGTH nL.frmls` 3040 by metis_tac[MEM_EL] 3041 >> qexists_tac `ind_q` >> fs[] 3042 >> qunabbrev_tac `ce_lists` >> rw[] 3043 >> `LENGTH nL.frmls = 3044 LENGTH (MAP (concr_extrTrans g_AA) 3045 (CAT_OPTIONS L))` by ( 3046 fs[CAT_OPTIONS_LENGTH] 3047 ) 3048 >> `SOME 3049 (EL ind_q (CAT_OPTIONS (MAP (concr_extrTrans g_AA) 3050 (CAT_OPTIONS L)))) = 3051 (EL ind_q (MAP (concr_extrTrans g_AA) 3052 (CAT_OPTIONS L)))` by 3053 metis_tac[CAT_OPTIONS_EL] 3054 >> `EL ind_q (MAP (concr_extrTrans g_AA) 3055 (CAT_OPTIONS L)) = 3056 (concr_extrTrans g_AA (EL ind_q (CAT_OPTIONS L)))` 3057 by fs[EL_MAP,LENGTH_MAP] 3058 >> `LENGTH L = LENGTH nL.frmls` by ( 3059 qunabbrev_tac `L` 3060 >> fs[LENGTH_MAP] 3061 ) 3062 >> `SOME (EL ind_q (CAT_OPTIONS L)) = 3063 EL ind_q L` by metis_tac[CAT_OPTIONS_EL] 3064 >> `EL ind_q L = SOME q_i` by ( 3065 qunabbrev_tac `L` >> simp[EL_MAP] 3066 ) 3067 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[] 3068 >> metis_tac[SOME_11] 3069 ) 3070 >> `{(q,(removeStatesSimpl (ltl2vwaa f)).trans q) | 3071 MEM q nL.frmls} = 3072 set 3073 (MAP (��(q,d). 3074 (q,set (MAP (concr2AbstractEdge (set aP)) d))) 3075 zpd)` by ( 3076 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 3077 >- ( 3078 simp[MEM_MAP] 3079 >> `?i nL. findNode (��(i,l). l.frml = q) g_AA = SOME (i,nL)` 3080 by ( 3081 fs[findNode_def,concr2AbstrAA_def, 3082 ALTER_A_component_equality] 3083 >> `inGBA g nL.frmls` by ( 3084 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `nL` 3085 >> simp[MEM_MAP,MEM_EQUAL_SET] 3086 >> metis_tac[MEM_toAList,SND] 3087 ) 3088 >> `set nL.frmls ��� 3089 POW (concr2Abstr_states g_AA)` 3090 by metis_tac[] 3091 >> `q ��� concr2Abstr_states g_AA` 3092 by metis_tac[IN_POW,SUBSET_DEF] 3093 >> fs[concr2Abstr_states_def] 3094 >> rename[`SOME x2 = lookup n1 g_AA.nodeInfo` ] 3095 >> rw[] 3096 >> `(��(i,l). l.frml = x2.frml) (n1,x2)` by fs[] 3097 >> `���y. FIND (��(i,l). l.frml = x2.frml) 3098 (toAList g_AA.nodeInfo) = SOME y` 3099 by metis_tac[FIND_LEMM,MEM_toAList] 3100 >> qexists_tac `FST y` >> qexists_tac `SND y` >> fs[] 3101 ) 3102 >> rename[`findNode _ g_AA = SOME (q_i,q_nL)`] 3103 >> `?q_trns. SOME q_trns = concr_extrTrans g_AA q_i 3104 ��� MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 3105 ��� (q_nL.frml = q)` by ( 3106 fs[findNode_def] 3107 >> `MEM (q_i,q_nL) (toAList g_AA.nodeInfo) 3108 ��� ((��(i,l). l.frml = q) (q_i,q_nL))` 3109 by metis_tac[FIND_LEMM2] 3110 >> `IS_SOME (lookup q_i g_AA.followers)` suffices_by ( 3111 rpt strip_tac >> simp[concr_extrTrans_def] >> fs[] 3112 >> Cases_on `lookup q_i g_AA.followers` 3113 >> fs[IS_SOME_DEF] 3114 >> metis_tac[wfg_def,domain_lookup] 3115 ) 3116 >> Cases_on `lookup q_i g_AA.followers` 3117 >> fs[IS_SOME_DEF] 3118 >> metis_tac[wfg_def,domain_lookup,MEM_toAList, 3119 NOT_SOME_NONE] 3120 ) 3121 >> qexists_tac `(q,q_trns)` >> simp[] 3122 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 3123 >> `?fls. lookup q_i g_AA.followers = SOME fls` by ( 3124 metis_tac[domain_lookup,MEM_toAList,wfg_def,SOME_11] 3125 ) 3126 >> `���n cT. 3127 concr_extrTrans g_AA q_i = SOME cT 3128 ��� lookup q_i g_AA.nodeInfo = SOME n 3129 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 3130 concrTrans g_AA (set aP) n.frml` 3131 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 3132 >> first_x_assum (qspec_then `q_i` mp_tac) 3133 >> simp[]) 3134 >> fs[] >> `q_nL = n` by metis_tac[MEM_toAList,SOME_11] 3135 >> rw[] 3136 ) 3137 >- ( 3138 rename[`MEM edge _`] >> fs[MEM_MAP] 3139 >> rename[`MEM cE zpd`] >> Cases_on `cE` 3140 >> fs[] >> qunabbrev_tac `zpd` 3141 >> rename[`MEM (q,q_trans) _`] >> POP_ASSUM mp_tac 3142 >> simp[MEM_ZIP] >> rpt strip_tac 3143 >- ( 3144 `inGBA g nL.frmls` by ( 3145 simp[inGBA_def,EXISTS_MEM] >> qexists_tac `nL` 3146 >> simp[MEM_MAP,MEM_EQUAL_SET] 3147 >> metis_tac[MEM_toAList,SND] 3148 ) 3149 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 3150 >> `set nL.frmls ��� 3151 POW (concr2Abstr_states g_AA)` 3152 by metis_tac[] 3153 >> `q ��� concr2Abstr_states g_AA` 3154 by metis_tac[IN_POW,SUBSET_DEF,EL_MEM] 3155 >> fs[concr2Abstr_states_def] 3156 >> rename[`q_i ��� domain _`,`q = q_nL.frml`] 3157 >> `findNode (��(n,l). l.frml = q) g_AA 3158 = SOME (q_i,q_nL)` 3159 by metis_tac[UNIQUE_NODE_FIND_LEMM] 3160 >> `?q_trns. concr_extrTrans g_AA q_i = SOME q_trns` 3161 by ( 3162 simp[concr_extrTrans_def] 3163 >> Cases_on `lookup q_i g_AA.followers` >> fs[] 3164 >- metis_tac[wfg_def,NOT_SOME_NONE,domain_lookup] 3165 >- metis_tac[] 3166 ) 3167 >> rw[] 3168 >> `MEM (q_nL.frml,q_trns) (ZIP (nL.frmls,ce_lists))` 3169 by metis_tac[EL_MEM] 3170 >> `���k. k < LENGTH nL.frmls 3171 ��� (q_nL.frml,q_trns) = (EL k nL.frmls,EL k ce_lists)` 3172 by metis_tac[MEM_ZIP] 3173 >> `EL k nL.frmls = q_nL.frml` by fs[] 3174 >> `k = n` by metis_tac[ALL_DISTINCT_EL_IMP] 3175 >> fs[] 3176 >> `?fls. lookup q_i g_AA.followers = SOME fls` 3177 by metis_tac[wfg_def,domain_lookup] 3178 >> `���n cT. 3179 concr_extrTrans g_AA q_i = SOME cT 3180 ��� lookup q_i g_AA.nodeInfo = SOME n 3181 ��� set (MAP (concr2AbstractEdge (set aP)) cT) = 3182 concrTrans g_AA (set aP) n.frml` 3183 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 3184 >> first_x_assum (qspec_then `q_i` mp_tac) 3185 >> simp[] >> rpt strip_tac 3186 >> first_x_assum (qspec_then `set aP` mp_tac) 3187 >> fs[] 3188 ) 3189 >> metis_tac[SOME_11] 3190 ) 3191 >- metis_tac[EL_MEM] 3192 ) 3193 ) 3194 >> IMP_RES_TAC GBA_TRANS_LEMM 3195 >> first_x_assum (qspec_then `set aP` mp_tac) >> simp[] 3196 >> `!ce. MEM ce TRNS ==> 3197 (MEM_SUBSET ce.pos aP 3198 ��� MEM_SUBSET ce.neg aP 3199 ��� MEM_SUBSET ce.sucs (graphStates g_AA))` by ( 3200 qunabbrev_tac `TRNS` >> fs[] >> gen_tac >> strip_tac 3201 >> simp[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 3202 >> rpt strip_tac >> rename[`MEM x _`] 3203 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.pos` 3204 by metis_tac[GBA_TRANS_LEMM3] 3205 >> qunabbrev_tac `ce_lists` 3206 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 3207 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 3208 ) 3209 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.neg` 3210 by metis_tac[GBA_TRANS_LEMM3] 3211 >> qunabbrev_tac `ce_lists` 3212 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 3213 >> metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF] 3214 ) 3215 >- (`���l ce. MEM l ce_lists ��� MEM ce l ��� MEM x ce.sucs` 3216 by metis_tac[GBA_TRANS_LEMM3] 3217 >> qunabbrev_tac `ce_lists` 3218 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 3219 >> qunabbrev_tac `L` >> fs[MEM_MAP] >> Cases_on `z` 3220 >> fs[] >> rw[] 3221 >> `MEM (q,r) (toAList g_AA.nodeInfo)` by ( 3222 fs[findNode_def] >> metis_tac[FIND_LEMM2] 3223 ) 3224 >> `?fls. lookup q g_AA.followers = SOME fls` 3225 by metis_tac[domain_lookup,MEM_toAList, 3226 wfg_def,SOME_11] 3227 >> `���n cT. 3228 (concr_extrTrans g_AA q = SOME cT) 3229 ��� (lookup q g_AA.nodeInfo = SOME n) 3230 ��� (set (MAP (concr2AbstractEdge (set aP)) cT) = 3231 concrTrans g_AA (set aP) n.frml)` 3232 by (IMP_RES_TAC CONCR_EXTRTRANS_LEMM 3233 >> first_x_assum (qspec_then `q` mp_tac) 3234 >> simp[] 3235 ) 3236 >> `l = cT` by metis_tac[SOME_11] >> rw[] 3237 >> `concr2AbstractEdge (set aP) ce' ��� 3238 concrTrans g_AA (set aP) n.frml` by ( 3239 metis_tac[MEM_MAP,SET_EQ_SUBSET,SUBSET_DEF] 3240 ) 3241 >> fs[concr2AbstrAA_def,ALTER_A_component_equality] 3242 >> rw[] 3243 >> fs[isValidAlterA_def,concr2Abstr_states_def] 3244 >> `n.frml ��� (removeStatesSimpl (ltl2vwaa f)).states` 3245 by (rw[] >> metis_tac[domain_lookup]) 3246 >> Cases_on `concr2AbstractEdge (set aP) ce'` 3247 >> fs[] 3248 >> `r' ��� (removeStatesSimpl (ltl2vwaa f)).states` 3249 by metis_tac[] 3250 >> rw[] >> simp[graphStates_def,MEM_MAP] 3251 >> `r' ��� 3252 {x.frml | 3253 ���n. (SOME x = lookup n g_AA.nodeInfo) 3254 ��� (n ��� domain g_AA.nodeInfo)}` by metis_tac[] 3255 >> Cases_on `ce'` 3256 >> fs[concr2AbstractEdge_def] >> rw[] 3257 >> `x ��� 3258 {x.frml | 3259 ���n. (SOME x = lookup n g_AA.nodeInfo) 3260 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 3261 >> fs[] >> metis_tac[MEM_toAList,SND,FST] 3262 ) 3263 ) >> strip_tac 3264 >> qunabbrev_tac `GOAL` >> rpt strip_tac 3265 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> strip_tac 3266 >- ( 3267 rpt strip_tac >> fs[CAT_OPTIONS_MEM,MEM_MAP] 3268 >> Cases_on `y` >> fs[] 3269 >> rename[`MEM (eL, s_id) fls`] 3270 >> simp[gba_trans_def,minimal_elements_def,rrestrict_def] 3271 >> simp[d_gen_def] 3272 >> Cases_on `x` >> fs[] 3273 >> first_x_assum (qspec_then `eL` mp_tac) >> simp[] 3274 >> strip_tac 3275 >> first_x_assum (qspec_then `s_nL.frmls` mp_tac) >> simp[] 3276 >> `(���s_id s_nL'. 3277 MEM (eL,s_id) fls 3278 ��� (lookup s_id G2.nodeInfo = SOME s_nL') 3279 ��� MEM_EQUAL s_nL'.frmls s_nL.frmls)` by ( 3280 qexists_tac `s_id` >> qexists_tac `s_nL` 3281 >> fs[MEM_EQUAL_SET] 3282 ) 3283 >> strip_tac 3284 >> `���s_list. 3285 (MEM_EQUAL s_list s_nL.frmls) 3286 ��� ���y. 3287 ((eL,s_list) = TO_SUCS y) 3288 ��� (���cE. y = W_FINAL cE ��� MEM cE TRNS) 3289 ��� ���y'. 3290 (���cE. y' = W_FINAL cE ��� MEM cE TRNS) ��� y ��� y' ��� 3291 ��concr_min_rel y' y` by metis_tac[EQ_IMP_THM] 3292 >> rw[] 3293 >- ( 3294 `(transformLabel (set aP) eL.pos_lab eL.neg_lab,set s_nL.frmls) ��� 3295 set 3296 (MAP (concr2AbstractEdge (set aP)) 3297 (gba_trans_concr (MAP SND zpd)))` 3298 suffices_by metis_tac[] 3299 >> simp[MEM_MAP] >> qexists_tac `cE` 3300 >> Cases_on `cE` >> fs[concr2AbstractEdge_def] 3301 >> qunabbrev_tac `TRNS` >> qunabbrev_tac `TO_SUCS` 3302 >> qunabbrev_tac `W_FINAL` >> fs[] 3303 >> `MAP SND zpd = ce_lists` by metis_tac[MAP_ZIP] 3304 >> fs[] >> rw[] >> metis_tac[MEM_EQUAL_SET] 3305 ) 3306 >- (rpt strip_tac 3307 >> rename[`_ = abstr_ce2`] 3308 >> `abstr_ce2 ��� 3309 set (MAP (concr2AbstractEdge (set aP)) TRNS)` by ( 3310 IMP_RES_TAC GBA_TRANS_LEMM 3311 >> first_x_assum (qspec_then `set aP` mp_tac) >> fs[] 3312 >> rpt strip_tac >> qunabbrev_tac `TRNS` >> fs[] 3313 >> metis_tac[MAP_ZIP] 3314 ) 3315 >> POP_ASSUM mp_tac >> simp[MEM_MAP] >> strip_tac 3316 >> rename[`MEM ce2 TRNS`] >> fs[] 3317 >> `ce2 = cE \/ ~concr_min_rel (W_FINAL ce2) (W_FINAL cE)` 3318 by ( 3319 first_x_assum (qspec_then `W_FINAL ce2` mp_tac) 3320 >> simp[] 3321 >> strip_tac 3322 >> qunabbrev_tac `W_FINAL` >> fs[] 3323 >> Cases_on `ce2 = cE` >> fs[] 3324 ) 3325 >- (qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` >> fs[] 3326 >> rw[] >> Cases_on `cE` >> simp[concr2AbstractEdge_def] 3327 >> fs[concrEdge_component_equality] 3328 >> metis_tac[MEM_EQUAL_SET] 3329 ) 3330 >- ( 3331 fs[] 3332 >> qabbrev_tac `abstrAA = concr2AbstrAA (concrAA g_AA init aP)` 3333 >> `���e1_lab e1_sucs e2_lab e2_sucs. 3334 MEM_SUBSET ce2.pos aP ��� MEM_SUBSET ce2.neg aP ��� 3335 MEM_SUBSET ce2.sucs (graphStates g_AA) ��� MEM_SUBSET cE.pos aP ��� 3336 MEM_SUBSET cE.neg aP ��� MEM_SUBSET cE.sucs (graphStates g_AA) ��� 3337 ((e1_lab,e1_sucs) = concr2AbstractEdge (set aP) ce2) ��� 3338 ((e2_lab,e2_sucs) = concr2AbstractEdge (set aP) cE) 3339 ��� (((e1_lab,e1_sucs),e2_lab,e2_sucs) ��� 3340 tr_less_general 3341 {acc_cond abstrAA f | MEM f (MAP FST acc)} 3342 (set nL.frmls) ��� 3343 tlg_concr 3344 (ce2,get_acc_set acc ce2) 3345 (cE,get_acc_set acc cE))` by ( 3346 HO_MATCH_MP_TAC TLG_CONCR_LEMM >> qexists_tac `f` 3347 >> qexists_tac `init` >> fs[] >> metis_tac[] 3348 ) 3349 >> fs[] 3350 >> first_x_assum (qspec_then `FST abstr_ce2` mp_tac) 3351 >> rpt strip_tac 3352 >> first_x_assum (qspec_then `SND abstr_ce2` mp_tac) 3353 >> rpt strip_tac 3354 >> first_x_assum 3355 (qspec_then `transformLabel (set aP) eL.pos_lab eL.neg_lab` 3356 mp_tac) 3357 >> rpt strip_tac 3358 >> first_x_assum (qspec_then `set s_nL.frmls` mp_tac) 3359 >> `(transformLabel (set aP) eL.pos_lab eL.neg_lab, 3360 set s_nL.frmls) = 3361 concr2AbstractEdge (set aP) cE` by ( 3362 qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` >> fs[] 3363 >> rw[] >> Cases_on `cE` >> simp[concr2AbstractEdge_def] 3364 >> fs[concrEdge_component_equality] 3365 >> metis_tac[MEM_EQUAL_SET] 3366 ) 3367 >> simp[] >> strip_tac 3368 >> `{acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f' | 3369 MEM f' (MAP FST acc)} = 3370 {acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f | 3371 f | f ��� (concr2AbstrAA (concrAA g_AA init aP)).final}` 3372 by ( 3373 `���f. MEM f (MAP FST acc) ��� f ��� concr2Abstr_final g_AA` 3374 by metis_tac[VALID_ACC_LEMM] 3375 >> qunabbrev_tac `abstrAA` >> fs[] 3376 >> simp[SET_EQ_SUBSET,SUBSET_DEF,concr2AbstrAA_def] 3377 ) 3378 >> qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` 3379 >> fs[concr_min_rel_def] 3380 >- (rw[] >> metis_tac[all_acc_cond_def]) 3381 >- (Cases_on `cE` >> Cases_on `ce2` 3382 >> simp[concr2AbstractEdge_def] 3383 >> fs[concrEdge_component_equality] 3384 >> `!x y. MEM_EQUAL x y ==> 3385 MEM_SUBSET x y ��� MEM_SUBSET y x` 3386 by metis_tac[MEM_EQUAL_SET,MEM_SUBSET_SET_TO_LIST, 3387 SET_EQ_SUBSET] 3388 >> simp[SET_EQ_SUBSET] >> rpt strip_tac 3389 >- metis_tac[TRANSFORMLABEL_SUBSET] 3390 >- metis_tac[TRANSFORMLABEL_SUBSET] 3391 >- metis_tac[MEM_EQUAL_SET,SET_EQ_SUBSET] 3392 >- metis_tac[MEM_EQUAL_SET,SET_EQ_SUBSET] 3393 ) 3394 >- (rw[] >> Cases_on `cE` >> Cases_on `ce2` 3395 >> simp[concr2AbstractEdge_def] 3396 >> fs[concrEdge_component_equality,MEM_EQUAL_SET] 3397 >> rename[`_ (set aP) pos1 neg1 = _ (set aP) pos2 neg2`] 3398 >> `pos1 = (concrEdge pos1 neg1 l1).pos` by fs[] 3399 >> `neg1 = (concrEdge pos1 neg1 l1).neg` by fs[] 3400 >> `pos2 = (concrEdge pos2 neg2 l1').pos` by fs[] 3401 >> `neg2 = (concrEdge pos2 neg2 l1').neg` by fs[] 3402 >> metis_tac[TRNS_IS_EMPTY_LEMM,MEM_SUBSET_SET_TO_LIST] 3403 ) 3404 ) 3405 ) 3406 ) 3407 >- (rpt strip_tac >> simp[CAT_OPTIONS_MEM,MEM_MAP] >> POP_ASSUM mp_tac 3408 >> simp[gba_trans_def,minimal_elements_def,rrestrict_def,d_gen_def] 3409 >> strip_tac 3410 >> rename[`(a,sucs) ��� d_conj_set _ _`] >> rw[] 3411 >> `(a,sucs) ��� 3412 set 3413 (MAP (concr2AbstractEdge (set aP)) 3414 (gba_trans_concr (MAP SND zpd)))` by metis_tac[] 3415 >> POP_ASSUM mp_tac >> simp[MEM_MAP] >> strip_tac 3416 >> rename[`MEM ce (gba_trans_concr _)`] 3417 >> qabbrev_tac `eL = 3418 edgeLabelGBA ce.pos ce.neg (get_acc_set acc ce)` 3419 >> first_x_assum (qspec_then `eL` mp_tac) >> simp[] 3420 >> strip_tac 3421 >> first_x_assum (qspec_then `ce.sucs` mp_tac) >> simp[] 3422 >> strip_tac 3423 >> `���s_list. 3424 MEM_EQUAL s_list ce.sucs 3425 ��� ���y. 3426 ((eL,s_list) = TO_SUCS y) 3427 ��� (���cE. y = W_FINAL cE ��� MEM cE TRNS) 3428 ��� ���y'. 3429 (���cE. y' = W_FINAL cE ��� MEM cE TRNS) ��� y ��� y' ��� 3430 ��concr_min_rel y' y` suffices_by ( 3431 strip_tac 3432 >> `(���s_id s_nL. 3433 (MEM (eL,s_id) fls ��� lookup s_id G2.nodeInfo = SOME s_nL) 3434 ��� MEM_EQUAL s_nL.frmls ce.sucs)` by metis_tac[] 3435 >> qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` >> fs[] 3436 >> qexists_tac `(eL,s_id)` >> simp[] 3437 >> Cases_on `ce` >> simp[concr2AbstractEdge_def] 3438 >> fs[concrEdge_component_equality] 3439 >> `l = cE.pos ��� l0 = cE.neg` by metis_tac[] 3440 >> fs[MEM_EQUAL_SET] 3441 ) 3442 >> qexists_tac `ce.sucs` >> fs[MEM_EQUAL_SET] 3443 >> qexists_tac `(ce,get_acc_set acc ce)` >> fs[] 3444 >> qunabbrev_tac `TO_SUCS` >> qunabbrev_tac `W_FINAL` >> fs[] 3445 >> rpt strip_tac 3446 >- (`MAP SND zpd = ce_lists` by metis_tac[MAP_ZIP] 3447 >> qunabbrev_tac `TRNS` >> fs[] 3448 ) 3449 >- (rename[`MEM cE2 TRNS`] 3450 >> rename[`concr_min_rel y1 (ce,_)`] >> Cases_on `y1` 3451 >> `~(cE2 = ce)` by ( 3452 rw[] >> fs[] >> CCONTR_TAC >> rw[] 3453 ) 3454 >> first_x_assum 3455 (qspec_then `concr2AbstractEdge (set aP) cE2` mp_tac) 3456 >> Q.HO_MATCH_ABBREV_TAC `(Q1 ==> Q2) ==> F` 3457 >> `Q2 ==> F` by ( 3458 qunabbrev_tac `Q2` >> simp[] (* >> Cases_on `y` *) 3459 >> `~(ce = cE2)` by metis_tac[] 3460 >> Cases_on `~MEM_EQUAL cE2.sucs ce.sucs` 3461 >- (Cases_on `ce` >> fs[] 3462 >> Cases_on `cE2` >> simp[concr2AbstractEdge_def] 3463 >> fs[MEM_EQUAL_SET,concrEdge_component_equality] 3464 >> rw[] >> metis_tac[] 3465 ) 3466 >- (Cases_on `~ trns_is_empty ce ��� ~ trns_is_empty cE2` 3467 >- (`MEM ce TRNS` by metis_tac[MAP_ZIP] 3468 >> `���x. MEM x ce.pos ��� MEM x cE2.pos 3469 ��� MEM x ce.neg ��� MEM x cE2.neg ��� x ��� set aP` by ( 3470 metis_tac[MEM_SUBSET_SET_TO_LIST,SUBSET_DEF,MEM] 3471 ) 3472 >> `~(transformLabel (set aP) ce.pos ce.neg = 3473 transformLabel (set aP) cE2.pos cE2.neg)` 3474 suffices_by (Cases_on `ce` >> Cases_on `cE2` 3475 >> simp[concr2AbstractEdge_def] 3476 ) 3477 >> HO_MATCH_MP_TAC TRANSFORMLABEL_LEMM 3478 >> simp[] >> fs[concr_min_rel_def] 3479 >> rw[] >> metis_tac[MEM_EQUAL_SET] 3480 ) 3481 >- (`MEM ce TRNS` by metis_tac[MAP_ZIP] 3482 >> `(concrEdge cE2.pos cE2.neg cE2.sucs).pos = cE2.pos 3483 ��� (concrEdge cE2.pos cE2.neg cE2.sucs).neg = cE2.neg` 3484 by fs[] 3485 >> `set ce.pos ��� set aP 3486 ��� set ce.neg ��� set aP 3487 ��� set cE2.pos ��� set aP 3488 ��� set cE2.neg ��� set aP` 3489 by metis_tac[MEM_SUBSET_SET_TO_LIST] 3490 >> `trns_is_empty ce = ~trns_is_empty cE2` by ( 3491 fs[concr_min_rel_def] >> metis_tac[] 3492 ) 3493 >> `~(transformLabel (set aP) ce.pos ce.neg 3494 = transformLabel (set aP) cE2.pos cE2.neg)` 3495 suffices_by (Cases_on `ce` >> Cases_on `cE2` 3496 >> simp[concr2AbstractEdge_def]) 3497 >> metis_tac[TRNS_IS_EMPTY_LEMM] 3498 ) 3499 ) 3500 ) 3501 >> `Q1` suffices_by metis_tac[] 3502 >> qunabbrev_tac `Q1` >> fs[] 3503 >> (conj_tac 3504 >- (qunabbrev_tac `TRNS` 3505 >> `MAP SND zpd = ce_lists` by metis_tac[MAP_ZIP] 3506 >> metis_tac[MEM_MAP] 3507 ) 3508 >- (conj_tac 3509 >- (`MEM ce TRNS` by metis_tac[MAP_ZIP] 3510 >> `tlg_concr (cE2,get_acc_set acc cE2) 3511 (ce,get_acc_set acc ce)` by 3512 (fs[concr_min_rel_def] >> rw[]) 3513 >> qabbrev_tac `abstrAA = 3514 concr2AbstrAA (concrAA g_AA init aP)` 3515 >> `���e1_lab e1_sucs e2_lab e2_sucs. 3516 MEM_SUBSET cE2.pos aP ��� MEM_SUBSET cE2.neg aP ��� 3517 MEM_SUBSET cE2.sucs (graphStates g_AA) ��� MEM_SUBSET ce.pos aP ��� 3518 MEM_SUBSET ce.neg aP ��� MEM_SUBSET ce.sucs (graphStates g_AA) ��� 3519 ((e1_lab,e1_sucs) = concr2AbstractEdge (set aP) cE2) ��� 3520 ((e2_lab,e2_sucs) = concr2AbstractEdge (set aP) ce) 3521 ��� (((e1_lab,e1_sucs),e2_lab,e2_sucs) ��� 3522 tr_less_general 3523 {acc_cond abstrAA f | MEM f (MAP FST acc)} 3524 (set nL.frmls) ��� 3525 tlg_concr (cE2,get_acc_set acc cE2) 3526 (ce,get_acc_set acc ce))` by ( 3527 HO_MATCH_MP_TAC TLG_CONCR_LEMM >> qexists_tac `f` 3528 >> qexists_tac `init` >> fs[] >> metis_tac[] 3529 ) 3530 >> fs[] 3531 >> first_x_assum 3532 (qspec_then `transformLabel (set aP) cE2.pos cE2.neg` 3533 mp_tac) 3534 >> simp[] >> strip_tac 3535 >> first_x_assum (qspec_then `set cE2.sucs` mp_tac) 3536 >> simp[] >> strip_tac 3537 >> first_x_assum 3538 (qspec_then `transformLabel (set aP) ce.pos ce.neg` 3539 mp_tac) 3540 >> simp[] >> strip_tac 3541 >> first_x_assum (qspec_then `set ce.sucs` mp_tac) 3542 >> simp[] >> strip_tac 3543 >> fs[all_acc_cond_def] 3544 >> `{acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f' | 3545 MEM f' (MAP FST acc)} = 3546 {acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f | 3547 f | f ��� (concr2AbstrAA (concrAA g_AA init aP)).final}` 3548 by ( 3549 `���f. MEM f (MAP FST acc) ��� f ��� concr2Abstr_final g_AA` 3550 by metis_tac[VALID_ACC_LEMM] 3551 >> simp[SET_EQ_SUBSET,SUBSET_DEF,concr2AbstrAA_def] 3552 >> rpt strip_tac >> qexists_tac `f'` >> simp[] 3553 >> qunabbrev_tac `abstrAA` >> fs[concr2AbstrAA_def] 3554 ) 3555 >> Cases_on `ce` >> Cases_on `cE2` 3556 >> fs[concr2AbstractEdge_def] 3557 >> qunabbrev_tac `abstrAA` >> fs[concr2AbstrAA_def] 3558 ) 3559 >- (qunabbrev_tac `TRNS` 3560 >> `MAP SND zpd = ce_lists` by metis_tac[MAP_ZIP] 3561 >> metis_tac[MEM_MAP] 3562 ) 3563 )) 3564 ) 3565 ) 3566 ) 3567 >- (first_x_assum (qspec_then `eL` mp_tac) >> simp[] 3568 >> strip_tac 3569 >> `s_id ��� domain G2.nodeInfo` by metis_tac[] 3570 >> `?s_nL. lookup s_id G2.nodeInfo = SOME s_nL` 3571 by metis_tac[domain_lookup] 3572 >> first_x_assum (qspec_then `s_nL.frmls` mp_tac) >> simp[] 3573 >> strip_tac 3574 >> `���s_id s_nL'. 3575 MEM (eL,s_id) fls 3576 ��� lookup s_id G2.nodeInfo = SOME s_nL' 3577 ��� MEM_EQUAL s_nL'.frmls s_nL.frmls` by ( 3578 metis_tac[MEM_EQUAL_SET] 3579 ) 3580 >> `���s_list. 3581 MEM_EQUAL s_list s_nL.frmls ��� 3582 ���y. 3583 ((eL,s_list) = TO_SUCS y) ��� (���cE. y = W_FINAL cE ��� MEM cE TRNS) 3584 ��� ���y'. 3585 (���cE. y' = W_FINAL cE ��� MEM cE TRNS) ��� y ��� y' ��� 3586 ��concr_min_rel y' y` by metis_tac[] 3587 >> qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` 3588 >> Cases_on `y` >> fs[] 3589 ) 3590 >- (first_x_assum (qspec_then `eL` mp_tac) >> simp[] 3591 >> strip_tac 3592 >> `s_id ��� domain G2.nodeInfo` by metis_tac[] 3593 >> `?s_nL. lookup s_id G2.nodeInfo = SOME s_nL` 3594 by metis_tac[domain_lookup] 3595 >> first_x_assum (qspec_then `s_nL.frmls` mp_tac) >> simp[] 3596 >> strip_tac 3597 >> `���s_id s_nL'. 3598 MEM (eL,s_id) fls 3599 ��� lookup s_id G2.nodeInfo = SOME s_nL' 3600 ��� MEM_EQUAL s_nL'.frmls s_nL.frmls` by ( 3601 metis_tac[MEM_EQUAL_SET] 3602 ) 3603 >> `���s_list. 3604 MEM_EQUAL s_list s_nL.frmls ��� 3605 ���y. 3606 ((eL,s_list) = TO_SUCS y) ��� (���cE. y = W_FINAL cE ��� MEM cE TRNS) 3607 ��� ���y'. 3608 (���cE. y' = W_FINAL cE ��� MEM cE TRNS) ��� y ��� y' ��� 3609 ��concr_min_rel y' y` by metis_tac[] 3610 >> qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` 3611 >> Cases_on `y` >> fs[] 3612 ) 3613 >- (first_x_assum (qspec_then `eL` mp_tac) >> simp[] 3614 >> strip_tac 3615 >> first_x_assum (qspec_then `s_nL.frmls` mp_tac) >> simp[] 3616 >> strip_tac 3617 >> `���s_id s_nL'. 3618 MEM (eL,s_id) fls 3619 ��� (lookup s_id G2.nodeInfo = SOME s_nL') 3620 ��� MEM_EQUAL s_nL'.frmls s_nL.frmls` by ( 3621 metis_tac[MEM_EQUAL_SET] 3622 ) 3623 >> `���s_list. 3624 (MEM_EQUAL s_list s_nL.frmls) ��� 3625 ���y. 3626 ((eL,s_list) = TO_SUCS y) ��� (���cE. y = W_FINAL cE ��� MEM cE TRNS) 3627 ��� ���y'. 3628 (���cE. y' = W_FINAL cE ��� MEM cE TRNS) ��� y ��� y' ��� 3629 ��concr_min_rel y' y` by metis_tac[] 3630 >> qunabbrev_tac `W_FINAL` >> qunabbrev_tac `TO_SUCS` 3631 >> Cases_on `y` >> fs[] 3632 >> rw[] >> qunabbrev_tac `TRNS` 3633 >> `get_acc_set acc cE = 3634 get_acc_set acc (concrEdge cE.pos cE.neg s_nL.frmls)` by ( 3635 HO_MATCH_MP_TAC GET_ACC_SET_LEMM 3636 >> Cases_on `cE` >> simp[concrEdge_component_equality] 3637 >> fs[MEM_EQUAL_SET] 3638 ) 3639 >> metis_tac[] 3640 ) 3641 ) 3642 >- (`id2 ��� domain G2.nodeInfo` by metis_tac[domain_lookup] 3643 >> `id2 ��� (set new_ids ��� domain g.nodeInfo)` by metis_tac[] 3644 >> fs[IN_UNION] 3645 >- (`lookup id2 G2.followers = SOME []` by metis_tac[] 3646 >> rw[] >> fs[] >> rw[] >> fs[] 3647 ) 3648 >- (fs[trns_correct_def,final_correct_def,aP_correct_def] 3649 >> rpt strip_tac 3650 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 3651 >- (fs[CAT_OPTIONS_MEM,MEM_MAP] 3652 >> Cases_on `y` >> fs[] 3653 >> `lookup id2 g.nodeInfo = SOME nL` by metis_tac[] 3654 >> `lookup id2 g.followers = SOME fls` by metis_tac[] 3655 >> `r ��� domain g.nodeInfo` by metis_tac[] 3656 >> `MEM x 3657 (CAT_OPTIONS 3658 (MAP 3659 (��(eL,i). 3660 do 3661 s_nL <- lookup i g.nodeInfo; 3662 SOME 3663 (transformLabel (set aP) eL.pos_lab 3664 eL.neg_lab,set s_nL.frmls) 3665 od) fls))` by ( 3666 simp[CAT_OPTIONS_MEM,MEM_MAP] 3667 >> qexists_tac `(q,r)` >> fs[] 3668 ) 3669 >> metis_tac[] 3670 ) 3671 >- (`MEM x 3672 (CAT_OPTIONS 3673 (MAP 3674 (��(eL,i). 3675 do 3676 s_nL <- lookup i g.nodeInfo; 3677 SOME 3678 (transformLabel (set aP) eL.pos_lab 3679 eL.neg_lab,set s_nL.frmls) 3680 od) fls))` by metis_tac[] 3681 >> fs[CAT_OPTIONS_MEM,MEM_MAP] 3682 >> qexists_tac `y` >> fs[] >> Cases_on `y` >> fs[] 3683 >> `r ��� domain g.nodeInfo` by metis_tac[] 3684 >> metis_tac[domain_lookup] 3685 ) 3686 ) 3687 >- metis_tac[] 3688 >- metis_tac[] 3689 >- metis_tac[] 3690 ) 3691 ) 3692 ) 3693 >> rpt conj_tac 3694 >- metis_tac[] 3695 >- fs[expandGBA_def] 3696 >- (rpt strip_tac 3697 >- (`domain g.nodeInfo ��� domain G2.nodeInfo` by metis_tac[SUBSET_UNION] 3698 >> metis_tac[SUBSET_DEF] 3699 ) 3700 >- metis_tac[domain_lookup] 3701 ) 3702 >- (rpt strip_tac 3703 >- (`~(i = id)` by metis_tac[] 3704 >> metis_tac[] 3705 ) 3706 >- (`id ��� domain g.nodeInfo` by metis_tac[] 3707 >> fs[wfg_def] 3708 >> `~(g.next <= id)` by metis_tac[] 3709 >> `~(id = i)` by metis_tac[] 3710 >> metis_tac[] 3711 ) 3712 ) 3713 >- metis_tac[] 3714 >- metis_tac[] 3715 >- metis_tac[] 3716 >- fs[all_distinct_nub] 3717 >- (fs[frml_ad_def] >> rpt strip_tac 3718 >> `i ��� (set new_ids ��� domain g.nodeInfo)` by metis_tac[] 3719 >> fs[UNION_DEF] 3720 >- (`MEM n.frmls NEW_NODES` by metis_tac[SOME_11] 3721 >> qunabbrev_tac `NEW_NODES` >> qunabbrev_tac `TRNS` 3722 >> fs[MEM_MAP,MEM_FILTER,ONLY_MINIMAL_MEM] 3723 >> qabbrev_tac `L = 3724 CAT_OPTIONS 3725 (MAP (concr_extrTrans g_AA) 3726 (CAT_OPTIONS 3727 (MAP 3728 (��f. 3729 OPTION_MAP FST 3730 (findNode (��(i,l). l.frml = f) g_AA)) 3731 node.frmls)))` 3732 >> qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 3733 >> metis_tac[GBA_TRANS_LEMM1] 3734 ) 3735 >- metis_tac[] 3736 ) 3737 >- (rpt strip_tac >> rename[`lookup id2 _`] 3738 >> Cases_on `id = id2` >> fs[] 3739 >- metis_tac[] 3740 >- (fs[wfg_def] 3741 >> `id2 ��� (set new_ids ��� domain g.nodeInfo)` 3742 by metis_tac[domain_lookup] 3743 >> fs[IN_UNION] 3744 >- (`fls = []` by metis_tac[SOME_11] 3745 >> fs[] >> rw[] 3746 ) 3747 >- (`lookup id2 g.followers = SOME fls` by metis_tac[] 3748 >> `id2 ��� domain g.nodeInfo` by metis_tac[] 3749 >> metis_tac[UNION_SUBSET,SUBSET_DEF] 3750 ) 3751 ) 3752 ) 3753 ) 3754 ); 3755 3756val EXPGBA_CORRECT_LEMM = store_thm 3757 ("EXPGBA_CORRECT_LEMM", 3758 ``!f init aP g_AA abstrAA. 3759 (expandAuto_init f = SOME (concrAA g_AA init aP)) 3760 ��� (abstrAA = concr2AbstrAA (concrAA g_AA init aP)) 3761 ==> 3762 case expandGBA_init (concrAA g_AA init aP) of 3763 | NONE => F 3764 | SOME c_gba => 3765 (concr2AbstrGBA c_gba = 3766 removeStatesSimpl (vwaa2gba abstrAA))``, 3767 fs[] >> rpt strip_tac >> simp[expandGBA_init_def] 3768 >> `(wfg g_AA) ��� (until_iff_final g_AA) ��� (unique_node_formula g_AA) 3769 ��� (flws_sorted g_AA)` by ( 3770 fs[expandAuto_init_def] 3771 >> qabbrev_tac `G = 3772 FOLDR (��s g. addFrmlToGraph g s) 3773 (empty:(�� nodeLabelAA,�� edgeLabelAA) gfg) 3774 (nub (FLAT (tempDNF_concr f)))` 3775 >> qabbrev_tac `FS = nub (FLAT (tempDNF_concr f))` 3776 >> `wfg G 3777 ��� (wfg G 3778 ==> (unique_node_formula G ��� flws_sorted G 3779 ��� (!f. MEM f FS ==> MEM f (graphStates G)))) 3780 ��� (until_iff_final G)` 3781 suffices_by metis_tac[EXP_GRAPH_WFG_AND_SOME,SOME_11] 3782 >> qunabbrev_tac `G` >> rpt strip_tac >> fs[] 3783 >- metis_tac[empty_is_wfg,ADDFRML_FOLDR_LEMM] 3784 >- metis_tac[UNIQUE_NODE_FORM_EMPTY,ADDFRML_FOLDR_LEMM,empty_is_wfg] 3785 >- metis_tac[FLWS_SORTED_EMPTY,ADDFRML_FOLDR_LEMM,empty_is_wfg] 3786 >- (rename[`MEM f _`] 3787 >> Q.HO_MATCH_ABBREV_TAC `MEM f (graphStates G)` 3788 >> `set (graphStates G) = set FS ��� {}` 3789 by metis_tac[ADDFRML_FOLDR_LEMM,empty_is_wfg,GRAPHSTATES_EMPTY, 3790 LIST_TO_SET,UNION_COMM] 3791 >> fs[] 3792 ) 3793 >- (`until_iff_final (empty:(�� nodeLabelAA, �� edgeLabelAA) gfg)` 3794 by ( 3795 simp[empty_def,until_iff_final_def] >> rpt strip_tac 3796 >> metis_tac[lookup_def,NOT_SOME_NONE] 3797 ) 3798 >> metis_tac[ADDFRML_FOLDR_LEMM,empty_is_wfg]) 3799 ) 3800 >> qabbrev_tac `addedInit:(�� nodeLabelGBA, �� edgeLabelGBA) gfg = 3801 FOLDR (��n g. addNodeToGBA g n) empty 3802 (MAP 3803 (��i_list. 3804 MAP (��l. l.frml) 3805 (CAT_OPTIONS 3806 (MAP (��i. lookup i g_AA.nodeInfo) 3807 (nub i_list)))) init)` 3808 >> qabbrev_tac `final_trans = 3809 FOLDR 3810 (��(id,x) sF. 3811 case concr_extrTrans g_AA id of 3812 NONE => sF 3813 | SOME c_t => if is_until x then (x,c_t)::sF else sF) [] 3814 (graphStatesWithId g_AA)` 3815 >> `!i. MEM i (MAP FST (toAList addedInit.nodeInfo)) 3816 ==> (i ��� domain addedInit.nodeInfo)` by ( 3817 rpt strip_tac >> qunabbrev_tac `addedInit` >> fs[MEM_MAP] 3818 >> Cases_on `y` >> fs[] 3819 >> metis_tac[MEM_toAList,domain_lookup] 3820 ) 3821 >> `wfg addedInit` by ( 3822 qunabbrev_tac `addedInit` >> fs[] 3823 >> `!l. wfg (FOLDR (��n g. addNodeToGBA g n) 3824 (empty:(�� nodeLabelGBA, �� edgeLabelGBA) gfg) 3825 l)` by ( 3826 Induct_on `l` >> fs[] >> rpt strip_tac 3827 >> metis_tac[ADDNODE_GBA_WFG] 3828 ) 3829 >> metis_tac[] 3830 ) 3831 >> IMP_RES_TAC EXPGBA_SOME_WFG >> first_x_assum (qspec_then `g_AA` mp_tac) 3832 >> rpt strip_tac >> first_x_assum (qspec_then `final_trans` mp_tac) >> simp[] 3833 >> rpt strip_tac >> fs[] >> simp[concr2AbstrGBA_def,vwaa2gba_def] 3834 >> `frml_ad addedInit` by ( 3835 qunabbrev_tac `addedInit` >> fs[] 3836 >> Q.HO_MATCH_ABBREV_TAC `frml_ad (P init)` 3837 >> `!ls. frml_ad (P ls) ��� wfg (P ls)` by ( 3838 Induct_on `ls` >> fs[] 3839 >- (qunabbrev_tac `P` >> simp[frml_ad_def] >> rpt strip_tac 3840 >> fs[empty_def] 3841 ) 3842 >- (rpt strip_tac 3843 >- ( 3844 qunabbrev_tac `P` >> simp[FOLDR] 3845 >> Q.HO_MATCH_ABBREV_TAC `frml_ad (addNodeToGBA G (p h))` 3846 >> fs[] 3847 >> simp[addNodeToGBA_def] 3848 >> Cases_on `inGBA G (p h)` >> simp[addNode_def] 3849 >> simp[frml_ad_def] >> rpt gen_tac 3850 >> Cases_on `i = G.next` 3851 >- (rpt strip_tac 3852 >> `n = nodeLabelGBA (p h)` by metis_tac[lookup_insert,SOME_11] 3853 >> qunabbrev_tac `p` >> fs[] 3854 >> `!l:(num option) list. 3855 ALL_DISTINCT l 3856 ==> ALL_DISTINCT (CAT_OPTIONS l)` by ( 3857 Induct_on `l` >> fs[CAT_OPTIONS_def] >> rpt strip_tac 3858 >> Cases_on `h'` >> simp[CAT_OPTIONS_def] 3859 >> simp[CAT_OPTIONS_MEM] 3860 ) 3861 >> qabbrev_tac `frml_diff = 3862 ��l. !x1 x2. (MEM x1 l ��� MEM x2 l) 3863 ==> ~(x1 = x2) ==> ~(x1.frml = x2.frml)` 3864 >> `!l. ALL_DISTINCT l ==> 3865 (ALL_DISTINCT 3866 (CAT_OPTIONS 3867 (MAP (��i. lookup i g_AA.nodeInfo) l)) 3868 ��� frml_diff 3869 (CAT_OPTIONS 3870 (MAP (��i. lookup i g_AA.nodeInfo) l)))` by ( 3871 Induct_on `l` >> qunabbrev_tac `frml_diff` 3872 >> fs[ALL_DISTINCT,CAT_OPTIONS_def] 3873 >> gen_tac >> strip_tac 3874 >> rpt strip_tac 3875 >-(rename[`~MEM h l`] 3876 >> Cases_on `lookup h g_AA.nodeInfo` >> fs[CAT_OPTIONS_def] 3877 >> CCONTR_TAC >> fs[CAT_OPTIONS_MEM,MEM_MAP] 3878 >> rename[`SOME x = lookup i g_AA.nodeInfo`] 3879 >> Cases_on `MEM i l` >> fs[unique_node_formula_def] 3880 >> `MEM (h,x.frml) (graphStatesWithId g_AA)` by ( 3881 metis_tac[GRAPH_STATES_WITH_ID_LEMM,MEM_toAList] 3882 ) 3883 >> `MEM (i,x.frml) (graphStatesWithId g_AA)` by ( 3884 metis_tac[GRAPH_STATES_WITH_ID_LEMM,MEM_toAList] 3885 ) 3886 >> metis_tac[] 3887 ) 3888 >- (rename[`~MEM h l`] 3889 >> Cases_on `lookup h g_AA.nodeInfo` >> fs[CAT_OPTIONS_def] 3890 >> fs[CAT_OPTIONS_MEM] 3891 >> rw[] >> fs[MEM_MAP] 3892 >> metis_tac[GRAPH_STATES_WITH_ID_LEMM, 3893 MEM_toAList,unique_node_formula_def] 3894 ) 3895 ) 3896 >> `ALL_DISTINCT 3897 (CAT_OPTIONS 3898 (MAP (��i. lookup i g_AA.nodeInfo) (nub h)))` 3899 by metis_tac[all_distinct_nub] 3900 >> `!s. (ALL_DISTINCT s ��� frml_diff s) 3901 ==> ALL_DISTINCT (MAP (��l. l.frml) s)` by ( 3902 Induct_on `s` >> fs[ALL_DISTINCT] >> rpt strip_tac 3903 >> qunabbrev_tac `frml_diff` >> fs[MEM_MAP] 3904 >> metis_tac[] 3905 ) 3906 >> metis_tac[all_distinct_nub] 3907 ) 3908 >- (rpt strip_tac 3909 >> `lookup i G.nodeInfo = SOME n` by metis_tac[lookup_insert,SOME_11] 3910 >> fs[frml_ad_def] >> metis_tac[] 3911 ) 3912 ) 3913 >- (qunabbrev_tac `P` >> simp[FOLDR] 3914 >> Q.HO_MATCH_ABBREV_TAC `wfg (addNodeToGBA G (p h))` 3915 >> metis_tac[ADDNODE_GBA_WFG] 3916 ) 3917 ) 3918 ) 3919 >> metis_tac[] 3920 ) 3921 >> `removeStatesSimpl (ltl2vwaa f) = 3922 concr2AbstrAA (concrAA g_AA init aP)` by ( 3923 `�����. 3924 case expandAuto_init �� of 3925 NONE => F 3926 | SOME concrA => 3927 concr2AbstrAA concrA = removeStatesSimpl (ltl2vwaa ��)` 3928 by metis_tac[EXP_WAA_CORRECT_LEMM] 3929 >> first_x_assum (qspec_then `f` mp_tac) >> simp[] 3930 ) 3931 >> `isVeryWeakAlterA (concr2AbstrAA (concrAA g_AA init aP))` by ( 3932 metis_tac[REDUCE_STATE_IS_WEAK, LTL2WAA_ISWEAK, 3933 LTL2WAA_ISVALID] 3934 ) 3935 >> simp[gbaSimplTheory.removeStatesSimpl_def,GBA_component_equality] 3936 >> qabbrev_tac `abstrAA = removeStatesSimpl (ltl2vwaa f)` 3937 >> `set aP = props f` by ( 3938 fs[ltl2vwaa_def,ltl2vwaa_free_alph_def,removeStatesSimpl_def] 3939 >> qunabbrev_tac `abstrAA` >> fs[concr2AbstrAA_def] 3940 >> metis_tac[POW_11] 3941 ) 3942 >> `(���id cT. 3943 (concr_extrTrans g_AA id = SOME cT) 3944 ==> ���ce. MEM ce cT ��� MEM_SUBSET ce.pos aP ��� MEM_SUBSET ce.neg aP)` by ( 3945 rpt gen_tac >> simp[concr_extrTrans_def] 3946 >> Cases_on `lookup id g_AA.followers` >> simp[] >> strip_tac 3947 >> strip_tac >> strip_tac 3948 >> Q.HO_MATCH_ABBREV_TAC `GOAL` >> rw[] 3949 >> fs[MEM_APPEND,CAT_OPTIONS_MEM,MEM_MAP] 3950 >- (Cases_on `grp` >> fs[] >> rename[`MEM (edge::sucs) _`] 3951 >> Cases_on `edge` >> fs[] 3952 >> `MEM (q,r) (CAT_OPTIONS 3953 (MAP 3954 (��(eL,id). 3955 case lookup id g_AA.nodeInfo of 3956 NONE => NONE 3957 | SOME n => SOME (eL,n.frml)) x))` by ( 3958 Q.HO_MATCH_ABBREV_TAC `MEM (q,r) L` 3959 >> `MEM (q,r) (FLAT 3960 (GROUP_BY 3961 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp) 3962 L))` suffices_by metis_tac[GROUP_BY_FLAT] 3963 >> simp[MEM_FLAT] >> qexists_tac `((q,r)::sucs)` 3964 >> fs[] 3965 ) 3966 >> fs[CAT_OPTIONS_MEM,MEM_MAP] >> rename[`MEM edge x`] 3967 >> Cases_on `edge` >> fs[] >> rename[`MEM (eL,id) x`] 3968 >> Cases_on `lookup id g_AA.nodeInfo` >> fs[] >> rw[] 3969 >> IMP_RES_TAC EXP_WAA_AP >> qunabbrev_tac `GOAL` 3970 >> fs[domain_lookup] 3971 >> `MEM eL (MAP FST x)` by metis_tac[MEM_MAP,FST] 3972 >> metis_tac[] 3973 ) 3974 >- (IMP_RES_TAC EXP_WAA_AP >> qunabbrev_tac `GOAL` 3975 >> fs[concrEdge_component_equality] 3976 ) 3977 ) 3978 >> Q.HO_MATCH_ABBREV_TAC `STATES ��� INIT ��� TRANS ��� FINAL ��� ALPH` 3979 >> `valid_acc aP g_AA final_trans` by ( 3980 simp[valid_acc_def] >> rpt strip_tac 3981 >- ( 3982 qunabbrev_tac `final_trans` 3983 >> Q.HO_MATCH_ABBREV_TAC `GOAL` 3984 >> `!L. 3985 (!i h. MEM (i,h) L ==> MEM (i,h) (graphStatesWithId g_AA)) 3986 ==> MEM (f',f_trns) ( 3987 FOLDR 3988 (��(id,x) sF. 3989 case concr_extrTrans g_AA id of 3990 NONE => sF 3991 | SOME c_t => if is_until x then (x,c_t)::sF else sF) 3992 [] 3993 L 3994 ) ==> GOAL` by ( 3995 qunabbrev_tac `GOAL` >> Induct_on `L` >> fs[] >> rpt strip_tac 3996 >> Cases_on `h` >> fs[] 3997 >> `MEM (q,r) (graphStatesWithId g_AA)` by fs[] 3998 >> Cases_on `concr_extrTrans g_AA q` >> fs[] 3999 >> Cases_on `is_until r` >> fs[] >> qexists_tac `q` 4000 >> fs[graphStatesWithId_def,MEM_MAP] >> Cases_on `y` 4001 >> fs[] >> rw[] >> rename[`MEM (id,nL) (toAList g_AA.nodeInfo)`] 4002 >> qexists_tac `nL` >> strip_tac 4003 >- metis_tac[UNIQUE_NODE_FIND_LEMM,MEM_toAList,SOME_11] 4004 >- (rpt strip_tac >> metis_tac[MEM_SUBSET_SET_TO_LIST]) 4005 ) 4006 >> qunabbrev_tac `GOAL` >> metis_tac[MEM] 4007 ) 4008 >- ( 4009 qunabbrev_tac `final_trans` >> fs[graphStates_def,MEM_MAP] 4010 >> Cases_on `y` >> rename[`MEM (id,nL) (toAList g_AA.nodeInfo)`] 4011 >> `?f_trns. concr_extrTrans g_AA id = SOME f_trns` by ( 4012 simp[concr_extrTrans_def] 4013 >> `?edgs. lookup id g_AA.followers = SOME edgs` by ( 4014 fs[wfg_def] 4015 >> `id ��� domain g_AA.nodeInfo` 4016 by metis_tac[MEM_toAList,domain_lookup] 4017 >> metis_tac[domain_lookup] 4018 >> fs[] >> metis_tac[MEM_toAList] 4019 ) 4020 >> fs[] >> metis_tac[MEM_toAList,domain_lookup] 4021 ) 4022 >> qexists_tac `f_trns` >> fs[] 4023 >> `!L. (MEM (id,nL.frml) L) 4024 ==> (MEM (nL.frml,f_trns) 4025 (FOLDR 4026 (��(id,x) sF. 4027 case concr_extrTrans g_AA id of 4028 NONE => sF 4029 | SOME c_t => if is_until x 4030 then (x,c_t)::sF 4031 else sF) [] 4032 L))` by ( 4033 Induct_on `L` >> fs[MEM_SUBSET_SET_TO_LIST] 4034 >> rpt strip_tac >> Cases_on `h` >> fs[] 4035 >> Cases_on `concr_extrTrans g_AA q` >> fs[] 4036 >> Cases_on `is_until r` >> fs[] 4037 ) 4038 >> fs[] 4039 >> `MEM (id,nL.frml) (graphStatesWithId g_AA)` 4040 suffices_by metis_tac[] 4041 >> simp[graphStatesWithId_def,MEM_MAP] 4042 >> qexists_tac `(id,nL)` >> fs[] 4043 ) 4044 ) 4045 >> `(set (MAP FST final_trans)) = 4046 {x | is_until x ��� MEM x (graphStates g_AA) }` by ( 4047 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4048 >- (fs[valid_acc_def,MEM_MAP] >> Cases_on `y` 4049 >> metis_tac[FST] 4050 ) 4051 >- (fs[valid_acc_def,MEM_MAP] >> Cases_on `y` 4052 >> `���id nL. 4053 findNode (��(i,l). l.frml = q) g_AA = SOME (id,nL)` 4054 by metis_tac[] 4055 >> simp[graphStates_def,MEM_MAP] 4056 >> `(MEM (id,nL) (toAList g_AA.nodeInfo)) 4057 ��� (��(i,l). l.frml = q) (id,nL)` 4058 by metis_tac[findNode_def,FIND_LEMM2] 4059 >> fs[] >> metis_tac[SND] 4060 ) 4061 >- (fs[valid_acc_def,MEM_MAP] >> metis_tac[FST]) 4062 ) 4063 >> `!l G id. ((FOLDR (��n g. addNodeToGBA g n) 4064 (empty:(�� nodeLabelGBA, �� edgeLabelGBA) gfg) 4065 l) = G) 4066 ��� (id ��� domain G.nodeInfo) 4067 ==> (lookup id G.followers = SOME [])` by ( 4068 Induct_on `l` >> fs[] >> rpt strip_tac 4069 >- fs[empty_def] 4070 >- (qabbrev_tac `G_int = 4071 FOLDR (��n g. addNodeToGBA g n) 4072 (empty:(�� nodeLabelGBA,�� edgeLabelGBA) gfg) 4073 l` 4074 >> simp[addNodeToGBA_def] 4075 >> Cases_on `inGBA G_int h` >> fs[addNodeToGBA_def] 4076 >> fs[addNode_def] 4077 >> Cases_on `id = G_int.next` >> fs[] 4078 >> metis_tac[lookup_insert] 4079 ) 4080 ) 4081 >> first_x_assum (qspec_then 4082 `(MAP 4083 (��i_list. 4084 MAP (��l. l.frml) 4085 (CAT_OPTIONS 4086 (MAP (��i. lookup i g_AA.nodeInfo) (nub i_list)))) 4087 init)` mp_tac) 4088 >> strip_tac 4089 >> first_x_assum (qspec_then `addedInit` mp_tac) >> simp[] 4090 >> strip_tac 4091 >> `(trns_correct (MAP FST (toAList addedInit.nodeInfo)) 4092 abstrAA addedInit) (set aP) 4093 ��� (aP_correct abstrAA addedInit aP) 4094 ��� (final_correct abstrAA addedInit final_trans)` by ( 4095 rpt conj_tac 4096 >- (simp[trns_correct_def] >> rpt strip_tac 4097 >> fs[MEM_MAP] >> first_x_assum (qspec_then `(id,nL)` mp_tac) 4098 >> simp[] >> metis_tac[MEM_toAList] 4099 ) 4100 >- (simp[aP_correct_def] >> rpt strip_tac 4101 >> `lookup id addedInit.followers = SOME []` 4102 by metis_tac[domain_lookup] 4103 >> fs[] >> rw[] >> fs[] 4104 ) 4105 >- (simp[final_correct_def] >> rpt strip_tac 4106 >> `lookup id addedInit.followers = SOME []` 4107 by metis_tac[domain_lookup] 4108 >> fs[] >> rw[] >> fs[] 4109 ) 4110 ) 4111 >> `(INIT ==> STATES) ��� INIT 4112 ��� (STATES ==> TRANS) ��� ((STATES ��� TRANS) ==> FINAL) ��� ALPH` 4113 suffices_by metis_tac[] 4114 >> `aP_correct abstrAA gba aP ��� final_correct abstrAA gba final_trans ��� 4115 trns_correct [] abstrAA gba (set aP)` by ( 4116 HO_MATCH_MP_TAC EXPGBA_TRANS_AND_FINAL >> simp[] 4117 >> qexists_tac `f` >> qexists_tac `init` 4118 >> qexists_tac `g_AA` 4119 >> qexists_tac `(MAP FST (toAList addedInit.nodeInfo))` 4120 >> simp[] >> qexists_tac `addedInit` 4121 >> fs[] >> rpt strip_tac 4122 >- metis_tac[] 4123 >- metis_tac[] 4124 >- metis_tac[] 4125 >- metis_tac[] 4126 >- metis_tac[] 4127 >- metis_tac[ALL_DISTINCT_MAP_FST_toAList] 4128 >- (`id ��� domain addedInit.nodeInfo` 4129 by metis_tac[domain_lookup,wfg_def] 4130 >> `lookup id addedInit.followers = SOME []` 4131 by metis_tac[domain_lookup] 4132 >> fs[] >> rw[] >> fs[] 4133 ) 4134 ) 4135 >> rpt strip_tac 4136 >- (`���x. 4137 inGBA addedInit x ��� 4138 set x ��� 4139 reachableFromSetGBA (vwaa2gba abstrAA) 4140 (vwaa2gba abstrAA).initial` by ( 4141 qunabbrev_tac `INIT` >> rw[] >> simp[vwaa2gba_def,GBA_component_equality] 4142 >> fs[inGBA_def,EXISTS_MEM,MEM_MAP] >> rename[`MEM y _`] 4143 >> Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (id,n) _`] 4144 >> `lookup id gba.nodeInfo = SOME n` by ( 4145 metis_tac[MEM_toAList,domain_lookup] 4146 ) 4147 >> `set x ��� 4148 concr2AbstrGBA_init 4149 (MAP FST (toAList addedInit.nodeInfo)) 4150 gba` suffices_by ( 4151 simp[reachableFromSetGBA_def,reachableFromGBA_def] 4152 >> metis_tac[RTC_REFL] 4153 ) 4154 >> PURE_REWRITE_TAC[concr2AbstrGBA_init_def] 4155 >> simp[CAT_OPTIONS_MEM,MEM_MAP] >> qexists_tac `id` >> fs[] 4156 >> fs[MEM_EQUAL_SET] >> metis_tac[FST] 4157 ) 4158 >> `���x. inGBA addedInit x ��� set x ��� POW abstrAA.states` by ( 4159 rpt strip_tac >> qunabbrev_tac `INIT` >> rw[] 4160 >> simp[vwaa2gba_def,GBA_component_equality] 4161 >> fs[inGBA_def,EXISTS_MEM,MEM_MAP] >> rename[`MEM y _`] 4162 >> Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (id,n) _`] 4163 >> `lookup id gba.nodeInfo = SOME n` by ( 4164 metis_tac[MEM_toAList,domain_lookup] 4165 ) 4166 >> `set x ��� 4167 concr2AbstrGBA_init 4168 (MAP FST (toAList addedInit.nodeInfo)) 4169 gba` by ( 4170 PURE_REWRITE_TAC[concr2AbstrGBA_init_def] 4171 >> simp[CAT_OPTIONS_MEM,MEM_MAP] 4172 >> qexists_tac `id` >> fs[] 4173 >> fs[MEM_EQUAL_SET] >> metis_tac[FST] 4174 ) 4175 >> `isValidAlterA (concr2AbstrAA (concrAA g_AA init aP))` by ( 4176 metis_tac[REDUCE_STATE_IS_VALID,LTL2WAA_ISVALID] 4177 ) 4178 >> POP_ASSUM mp_tac >> simp[isValidAlterA_def] 4179 >> metis_tac[SUBSET_DEF] 4180 ) 4181 >> qunabbrev_tac `STATES` >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> strip_tac 4182 >- (`!x. inGBA gba x 4183 ==> ((set x ��� reachableFromSetGBA (vwaa2gba abstrAA) 4184 (vwaa2gba abstrAA).initial) 4185 ��� (set x ��� (vwaa2gba abstrAA).states))` by ( 4186 HO_MATCH_MP_TAC EXPGBA_GRAPH_REACHABLE 4187 >> simp[] >> qexists_tac `f` >> qexists_tac `init` 4188 >> qexists_tac `aP` >> qexists_tac `g_AA` >> simp[] 4189 >> qexists_tac `final_trans` 4190 >> qexists_tac `MAP FST (toAList addedInit.nodeInfo)` 4191 >> qexists_tac `addedInit` >> simp[] >> rpt strip_tac 4192 >> metis_tac[] 4193 ) 4194 >> rpt strip_tac 4195 >> fs[concr2AbstrGBA_states_def] >> rename[`SOME q = lookup _ _`] 4196 >> `inGBA gba q.frmls` by ( 4197 simp[inGBA_def,EXISTS_MEM,MEM_MAP] >> qexists_tac `q` 4198 >> simp[MEM_EQUAL_SET] >> qexists_tac `(n,q)` 4199 >> metis_tac[SND,MEM_toAList] 4200 ) 4201 >> first_x_assum (qspec_then `q.frmls` mp_tac) 4202 >> simp[vwaa2gba_def] 4203 ) 4204 >- (rpt strip_tac >> fs[reachableFromSetGBA_def,reachableFromGBA_def] 4205 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 4206 >> Q.HO_MATCH_ABBREV_TAC ` 4207 (stepGBA G)^* x1 x2 4208 ==> x1 ��� init_states 4209 ==> x2 ��� concr2AbstrGBA_states gba` 4210 >> `!a b. (stepGBA G)^* a b 4211 ==> a ��� init_states 4212 ==> b ��� concr2AbstrGBA_states gba` suffices_by metis_tac[] 4213 >> HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 >> rpt strip_tac 4214 >- (qunabbrev_tac `init_states` >> fs[] 4215 >> `a ��� 4216 concr2AbstrGBA_init (MAP FST (toAList addedInit.nodeInfo)) 4217 gba` by metis_tac[] 4218 >> POP_ASSUM mp_tac 4219 >> simp[concr2AbstrGBA_init_def,concr2AbstrGBA_states_def] 4220 >> simp[CAT_OPTIONS_MEM,MEM_MAP] >> strip_tac 4221 >> metis_tac[domain_lookup] 4222 ) 4223 >- (`one_step_closed abstrAA gba` by ( 4224 HO_MATCH_MP_TAC EXPGBA_ALL_REACHABLE 4225 >> simp[] >> qexists_tac `f` 4226 >> qexists_tac `init` 4227 >> qexists_tac `aP` >> qexists_tac `g_AA` 4228 >> simp[] >> qexists_tac `final_trans` 4229 >> qexists_tac `MAP FST (toAList addedInit.nodeInfo)` 4230 >> qexists_tac `addedInit` >> simp[] >> conj_tac 4231 >- metis_tac[] 4232 >- ( 4233 simp[one_step_closed_apart_l_def] >> rpt strip_tac 4234 >> fs[MEM_MAP] >> metis_tac[FST,MEM_toAList] 4235 ) 4236 ) 4237 >> fs[one_step_closed_def,concr2AbstrGBA_states_def] 4238 >> rename[`b = set q1.frmls`] 4239 >> `inGBA gba q1.frmls` by ( 4240 simp[inGBA_def,EXISTS_MEM,MEM_MAP] 4241 >> qexists_tac `q1` >> simp[MEM_EQUAL_SET] 4242 >> qexists_tac `(n,q1)` >> simp[] 4243 >> metis_tac[MEM_toAList] 4244 ) 4245 >> first_x_assum (qspec_then `q1.frmls` mp_tac) >> simp[] 4246 >> strip_tac 4247 >> `FINITE b'` by ( 4248 fs[stepGBA_def] >> qunabbrev_tac `G` >> fs[] 4249 >> `(a',b') ��� (vwaa2gba abstrAA).trans b` by ( 4250 fs[vwaa2gba_def] >> metis_tac[] 4251 ) 4252 >> `FINITE 4253 (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 4254 simp[concr2AbstrAA_def,concr2Abstr_states_def] 4255 >> `FINITE {x.frml | 4256 ?n. MEM (n,x) (toAList g_AA.nodeInfo)}` 4257 suffices_by ( 4258 Q.HO_MATCH_ABBREV_TAC `FINITE S1 ==> FINITE S2` 4259 >> `S1 = S2` suffices_by fs[] 4260 >> qunabbrev_tac `S1` >> qunabbrev_tac `S2` 4261 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4262 >> metis_tac[MEM_toAList,domain_lookup] 4263 ) 4264 >> `{x.frml | ���n. MEM (n,x) (toAList g_AA.nodeInfo)} = 4265 IMAGE (��(i,n). n.frml) (set (toAList g_AA.nodeInfo))` 4266 by ( 4267 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4268 >- (qexists_tac `(n',x''')` >> fs[]) 4269 >- (fs[] >> Cases_on `x'''` >> fs[] >> metis_tac[]) 4270 ) 4271 >> metis_tac[FINITE_LIST_TO_SET,IMAGE_FINITE] 4272 ) 4273 >> `isValidGBA (vwaa2gba abstrAA)` by ( 4274 HO_MATCH_MP_TAC WAA2GBA_ISVALID 4275 >> fs[] 4276 >> metis_tac[REDUCE_STATE_IS_VALID,LTL2WAA_ISVALID] 4277 ) 4278 >> fs[isValidGBA_def] 4279 >> `b ��� (vwaa2gba abstrAA).states` by ( 4280 qunabbrev_tac `abstrAA` >> simp[vwaa2gba_def] >> rw[] 4281 ) 4282 >> `b' ��� (vwaa2gba abstrAA).states` by metis_tac[SUBSET_DEF] 4283 >> POP_ASSUM mp_tac >> simp[vwaa2gba_def] 4284 >> simp[concr2AbstrAA_def,concr2Abstr_states_def,IN_POW] 4285 >> strip_tac 4286 >> `FINITE {x.frml | 4287 ?n. MEM (n,x) (toAList g_AA.nodeInfo)}` 4288 suffices_by ( 4289 Q.HO_MATCH_ABBREV_TAC `FINITE S1 ==> FINITE S2` 4290 >> `S2 ��� S1` 4291 suffices_by metis_tac[PSUBSET_DEF,PSUBSET_FINITE] 4292 >> qunabbrev_tac `S1` >> qunabbrev_tac `S2` 4293 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4294 >> fs[SUBSET_DEF] 4295 >> metis_tac[MEM_toAList,domain_lookup,SUBSET_DEF] 4296 ) 4297 >> `{x.frml | ���n. MEM (n,x) (toAList g_AA.nodeInfo)} = 4298 IMAGE (��(i,n). n.frml) (set (toAList g_AA.nodeInfo))` 4299 by ( 4300 simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4301 >- (qexists_tac `(n',x''')` >> fs[]) 4302 >- (fs[] >> Cases_on `x'''` >> fs[] >> metis_tac[]) 4303 ) 4304 >> metis_tac[FINITE_LIST_TO_SET,IMAGE_FINITE] 4305 ) 4306 >> qabbrev_tac `q = nodeLabelGBA (SET_TO_LIST b')` 4307 >> first_x_assum (qspec_then `q.frmls` mp_tac) 4308 >> `G = vwaa2gba (concr2AbstrAA (concrAA g_AA init aP))` by ( 4309 qunabbrev_tac `G` >> fs[] >> simp[vwaa2gba_def] 4310 ) 4311 >> `b' = set q.frmls` by ( 4312 qunabbrev_tac `q` >> simp[] 4313 >> metis_tac[SET_TO_LIST_INV] 4314 ) 4315 >> `stepGBA 4316 (vwaa2gba (concr2AbstrAA (concrAA g_AA init aP))) 4317 (set q1.frmls) 4318 (set q.frmls)` by ( 4319 simp[] >> metis_tac[] 4320 ) 4321 >> simp[] >> simp[inGBA_def,EXISTS_MEM,MEM_MAP] >> strip_tac 4322 >> Cases_on `y` >> fs[] >> qexists_tac `r` >> rw[] 4323 >- fs[MEM_EQUAL_SET] 4324 >- metis_tac[MEM_toAList,domain_lookup] 4325 ) 4326 ) 4327 ) 4328 >- (qunabbrev_tac `INIT` >> simp[concr2AbstrAA_def,concr2Abstr_init_def] 4329 >> qunabbrev_tac `addedInit` 4330 >> Q.HO_MATCH_ABBREV_TAC ` 4331 concr2AbstrGBA_init 4332 (MAP FST 4333 (toAList (G_int init).nodeInfo)) gba = 4334 I_SET init` 4335 >> Q.HO_MATCH_ABBREV_TAC `P init` 4336 >> `!ls. (!l i. MEM l ls ��� MEM i l 4337 ==> i ��� domain g_AA.nodeInfo) 4338 ��� (!i. i ��� domain (G_int ls).nodeInfo 4339 ==> (lookup i (G_int ls).nodeInfo = lookup i gba.nodeInfo) 4340 ) 4341 ��� (!i. i ��� domain (G_int ls).nodeInfo 4342 ==> i ��� domain gba.nodeInfo) 4343 ==> P ls` by ( 4344 qunabbrev_tac `P` >> fs[] >> Induct_on `ls` >> fs[] 4345 >- (qunabbrev_tac `I_SET` >> qunabbrev_tac `G_int` 4346 >> simp[concr2AbstrGBA_init_def,toAList_def,foldi_def,empty_def] 4347 >> simp[CAT_OPTIONS_def]) 4348 >- (rpt strip_tac 4349 >> qunabbrev_tac `G_int` >> qunabbrev_tac `I_SET` 4350 >> simp[] 4351 >> qabbrev_tac 4352 `G_int = 4353 FOLDR (��n g. addNodeToGBA g n) 4354 (empty:(�� nodeLabelGBA, �� edgeLabelGBA) gfg) 4355 (MAP 4356 (��i_list. 4357 MAP (��l. l.frml) 4358 (CAT_OPTIONS 4359 (MAP (��i. lookup i g_AA.nodeInfo) 4360 (nub i_list)))) ls)` 4361 >> qabbrev_tac `NEW_L = 4362 (MAP (��l. l.frml) 4363 (CAT_OPTIONS 4364 (MAP (��i. lookup i g_AA.nodeInfo) (nub h))))` 4365 >> qabbrev_tac `OLD_S = 4366 set 4367 (MAP 4368 (��l. 4369 {x.frml | 4370 MEM x (CAT_OPTIONS (MAP (��n. lookup n g_AA.nodeInfo) l))}) ls)` 4371 >> fs[] 4372 >> `wfg G_int` by ( 4373 qunabbrev_tac `G_int` 4374 >> Q.HO_MATCH_ABBREV_TAC `wfg (A ls)` 4375 >> `!j. wfg (A j)` by ( 4376 Induct_on `j` >> qunabbrev_tac `A` >> fs[] 4377 >> strip_tac >> metis_tac[ADDNODE_GBA_WFG] 4378 ) 4379 >> fs[] 4380 ) 4381 >> `(���i. 4382 i ��� domain G_int.nodeInfo ��� 4383 lookup i G_int.nodeInfo = lookup i gba.nodeInfo) ��� 4384 (���i. i ��� domain G_int.nodeInfo 4385 ��� i ��� domain gba.nodeInfo)` by ( 4386 rpt strip_tac 4387 >- ( 4388 `~(G_int.next <= i)` by metis_tac[wfg_def] 4389 >> `~(G_int.next = i)` by fs[] 4390 >> `i ��� domain (addNodeToGBA G_int NEW_L).nodeInfo` 4391 by ( 4392 PURE_REWRITE_TAC[addNodeToGBA_def] 4393 >> Cases_on `inGBA G_int NEW_L` >> fs[] 4394 >> simp[addNode_def] 4395 ) 4396 >> `lookup i G_int.nodeInfo = 4397 lookup i (addNodeToGBA G_int NEW_L).nodeInfo` 4398 suffices_by metis_tac[] 4399 >> PURE_REWRITE_TAC[addNodeToGBA_def] 4400 >> Cases_on `inGBA G_int NEW_L` >> fs[] 4401 >> simp[addNode_def] 4402 >> metis_tac[lookup_insert] 4403 ) 4404 >- ( 4405 `i ��� domain (addNodeToGBA G_int NEW_L).nodeInfo` 4406 by ( 4407 PURE_REWRITE_TAC[addNodeToGBA_def] 4408 >> Cases_on `inGBA G_int NEW_L` >> fs[] 4409 >> simp[addNode_def] 4410 ) 4411 >> metis_tac[] 4412 ) 4413 ) 4414 >> `concr2AbstrGBA_init 4415 (MAP FST (toAList G_int.nodeInfo)) gba = OLD_S` 4416 by (fs[] >> metis_tac[]) 4417 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4418 >- (fs[concr2AbstrGBA_init_def,CAT_OPTIONS_MEM,MEM_MAP] 4419 >> `{set x | inGBA (addNodeToGBA G_int NEW_L) x} = 4420 {set x | inGBA G_int x} ��� {set NEW_L}` by ( 4421 metis_tac[ADDNODE_GBA_LEMM,WF_IMP_SUFFWFG] 4422 ) 4423 >> Cases_on `y` >> fs[] >> rw[] 4424 >> `n = r` by metis_tac[MEM_toAList,SOME_11,domain_lookup] 4425 >> rw[] 4426 >> `set n.frmls ��� 4427 {set x | inGBA (addNodeToGBA G_int NEW_L) x}` by ( 4428 `inGBA (addNodeToGBA G_int NEW_L) n.frmls` 4429 suffices_by (simp[] >> metis_tac[]) 4430 >> simp[inGBA_def,EXISTS_MEM,MEM_MAP] 4431 >> qexists_tac `n` >> simp[MEM_EQUAL_SET] 4432 >> qexists_tac `(i,n)` >> simp[] 4433 ) 4434 >> `set n.frmls ��� 4435 {set x | inGBA G_int x} ��� {set NEW_L}` by metis_tac[] 4436 >> fs[IN_UNION] 4437 >- (rename[`inGBA G_int x1`] 4438 >> `MEM (set x1) 4439 (CAT_OPTIONS 4440 (MAP 4441 (��i. 4442 do n <- lookup i gba.nodeInfo; SOME (set n.frmls) od) 4443 (MAP FST (toAList G_int.nodeInfo))))` by ( 4444 simp[CAT_OPTIONS_MEM,MEM_MAP] 4445 >> fs[inGBA_def,EXISTS_MEM,MEM_MAP] 4446 >> rw[] >> Cases_on `y'` >> fs[] 4447 >> `q ��� domain G_int.nodeInfo` by ( 4448 metis_tac[MEM_toAList,domain_lookup] 4449 ) 4450 >> `q ��� domain (addNodeToGBA G_int NEW_L).nodeInfo` 4451 by (simp[addNodeToGBA_def] 4452 >> Cases_on `inGBA G_int NEW_L` >> fs[] 4453 >> simp[addNode_def] 4454 ) 4455 >> qexists_tac `q` >> simp[] >> strip_tac 4456 >- (`lookup q (addNodeToGBA G_int NEW_L).nodeInfo = 4457 SOME r` by metis_tac[SOME_11,MEM_toAList] 4458 >> qexists_tac `r` >> fs[] >> Cases_on `y` >> fs[] 4459 >> rw[] >> metis_tac[MEM_toAList,MEM_EQUAL_SET] 4460 ) 4461 >- metis_tac[FST] 4462 ) 4463 >> metis_tac[] 4464 ) 4465 >- (disj1_tac >> fs[] >> rpt strip_tac 4466 >- (qunabbrev_tac `NEW_L` >> fs[] >> rw[] 4467 >> `MEM x' 4468 (MAP (��l. l.frml) 4469 (CAT_OPTIONS 4470 (MAP (��i. lookup i g_AA.nodeInfo) 4471 (nub h))))` by metis_tac[] 4472 >> fs[MEM_MAP,CAT_OPTIONS_MEM] 4473 >> metis_tac[] 4474 ) 4475 >- (rw[] >> `MEM x''.frml NEW_L` suffices_by fs[] 4476 >> qunabbrev_tac `NEW_L` 4477 >> simp[MEM_MAP,CAT_OPTIONS_MEM] >> metis_tac[] 4478 ) 4479 ) 4480 ) 4481 >- (simp[concr2AbstrGBA_init_def,MEM_MAP,CAT_OPTIONS_MEM] 4482 >> Cases_on `inGBA G_int NEW_L` 4483 >- ( 4484 simp[addNodeToGBA_def] 4485 >> POP_ASSUM mp_tac >> simp[inGBA_def,EXISTS_MEM,MEM_MAP] 4486 >> strip_tac >> Cases_on `y` >> rw[] 4487 >> rename[`MEM (id,n) _`] >> fs[] 4488 >> qexists_tac `id` >> simp[] >> strip_tac 4489 >- (qexists_tac `n` >> fs[] >> strip_tac 4490 >- metis_tac[MEM_toAList,SOME_11,domain_lookup] 4491 >- (`set NEW_L = 4492 {x.frml | ���n. SOME x = lookup n g_AA.nodeInfo 4493 ��� MEM n h}` 4494 suffices_by metis_tac[MEM_EQUAL_SET] 4495 >> qunabbrev_tac `NEW_L` 4496 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4497 >> fs[MEM_MAP,CAT_OPTIONS_MEM] >> metis_tac[] 4498 ) 4499 ) 4500 >- metis_tac[FST] 4501 ) 4502 >- (qexists_tac `G_int.next` >> simp[] 4503 >> strip_tac 4504 >- ( 4505 `lookup G_int.next 4506 (addNodeToGBA G_int NEW_L).nodeInfo = 4507 SOME (nodeLabelGBA NEW_L)` by ( 4508 simp[addNodeToGBA_def] 4509 >> PURE_REWRITE_TAC[addNode_def] 4510 >> simp[] 4511 ) 4512 >> qexists_tac `nodeLabelGBA NEW_L` >> simp[] 4513 >> strip_tac 4514 >- metis_tac[SOME_11,domain_lookup] 4515 >- (qunabbrev_tac `NEW_L` 4516 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4517 >> fs[MEM_MAP,CAT_OPTIONS_MEM] >> metis_tac[] 4518 ) 4519 ) 4520 >- (qexists_tac `(G_int.next,nodeLabelGBA NEW_L)` 4521 >> simp[addNodeToGBA_def] 4522 >> PURE_REWRITE_TAC[addNode_def] >> simp[] 4523 >> metis_tac[MEM_toAList,lookup_insert] 4524 ) 4525 ) 4526 ) 4527 >- (`x ��� concr2AbstrGBA_init 4528 (MAP FST (toAList G_int.nodeInfo)) gba` by fs[] 4529 >> fs[concr2AbstrGBA_init_def,CAT_OPTIONS_MEM,MEM_MAP] 4530 >> Cases_on `y` >> fs[] >> rw[] 4531 >> `n = r` by metis_tac[MEM_toAList,domain_lookup,SOME_11] 4532 >> rw[] >> qexists_tac `i` >> fs[] 4533 >> qexists_tac `(i,n)` >> fs[] 4534 >> `i ��� domain (addNodeToGBA G_int NEW_L).nodeInfo` by ( 4535 simp[addNodeToGBA_def] >> PURE_REWRITE_TAC[addNode_def] 4536 >> Cases_on `inGBA G_int NEW_L` >> fs[] 4537 >> metis_tac[MEM_toAList,domain_lookup] 4538 ) 4539 >> metis_tac[MEM_toAList,domain_lookup] 4540 ) 4541 ) 4542 ) 4543 >> first_x_assum (qspec_then `init` mp_tac) >> simp[] 4544 >> fs[] >> Q.HO_MATCH_ABBREV_TAC `(A ==> P init) ==> P init` 4545 >> `A` suffices_by fs[] >> qunabbrev_tac `A` 4546 >> rpt strip_tac 4547 >- (fs[expandAuto_init_def] >> rw[] >> fs[MEM_MAP,CAT_OPTIONS_MEM] 4548 >> rw[] >> fs[MEM_MAP, CAT_OPTIONS_MEM] 4549 >> qabbrev_tac `ADDEDNODES = 4550 (FOLDR (��s g. addFrmlToGraph g s) 4551 (empty: (�� nodeLabelAA, �� edgeLabelAA) gfg) 4552 (nub (FLAT (tempDNF_concr f))))` 4553 >> `(���f'. MEM f' (nub (FLAT (tempDNF_concr f))) 4554 ��� MEM f' (graphStates ADDEDNODES)) 4555 ==> (set (graphStatesWithId ADDEDNODES) 4556 ��� set (graphStatesWithId g_AA))` 4557 by ( 4558 `wfg ADDEDNODES` by metis_tac[ADDFRML_FOLDR_LEMM,empty_is_wfg] 4559 >> `unique_node_formula ADDEDNODES` 4560 by metis_tac[ADDFRML_FOLDR_LEMM,UNIQUE_NODE_FORM_EMPTY, 4561 empty_is_wfg] 4562 >> `flws_sorted ADDEDNODES` 4563 by metis_tac[ADDFRML_FOLDR_LEMM,FLWS_SORTED_EMPTY, 4564 empty_is_wfg] 4565 >> `!g fs. wfg g ��� unique_node_formula g ��� flws_sorted g ��� 4566 (���f. MEM f fs ��� MEM f (graphStates g)) ��� 4567 ���g2. 4568 (expandGraph g fs = SOME g2 ��� wfg g2) 4569 ��� set (graphStatesWithId g) ��� set (graphStatesWithId g2)` 4570 by metis_tac[EXP_GRAPH_WFG_AND_SOME] 4571 >> first_x_assum (qspec_then `ADDEDNODES` mp_tac) 4572 >> simp[] >> strip_tac 4573 >> first_x_assum 4574 (qspec_then `nub (FLAT (tempDNF_concr f))` mp_tac) 4575 >> simp[] >> strip_tac >> strip_tac 4576 ) 4577 >> `���f'. 4578 MEM f' (nub (FLAT (tempDNF_concr f))) ��� 4579 MEM f' (graphStates ADDEDNODES)` by ( 4580 rpt strip_tac 4581 >> `set (graphStates (empty:(�� nodeLabelAA,�� edgeLabelAA) gfg)) 4582 ��� set (nub (FLAT (tempDNF_concr f))) = 4583 set (graphStates ADDEDNODES)` by ( 4584 qunabbrev_tac `ADDEDNODES` 4585 >> metis_tac[ADDFRML_FOLDR_LEMM,empty_is_wfg] 4586 ) 4587 >> fs[GRAPHSTATES_EMPTY] 4588 ) 4589 >> fs[findNode_def] 4590 >> `MEM z (toAList ADDEDNODES.nodeInfo)` by metis_tac[FIND_LEMM2] 4591 >> Cases_on `z` >> fs[] 4592 >> `MEM (q,r.frml) (graphStatesWithId ADDEDNODES)` 4593 by metis_tac[GRAPH_STATES_WITH_ID_LEMM] 4594 >> `MEM (q,r.frml) (graphStatesWithId g_AA)` by fs[SUBSET_DEF] 4595 >> fs[graphStatesWithId_def,MEM_MAP] >> rename[`MEM y2 _`] 4596 >> Cases_on `y2` >> fs[] 4597 >> metis_tac[MEM_toAList,domain_lookup] 4598 ) 4599 >- metis_tac[domain_lookup] 4600 ) 4601 >- (qunabbrev_tac `TRANS` 4602 >> Q.HO_MATCH_ABBREV_TAC ` 4603 extractGBATrans (set aP) gba = 4604 ABS_TRNS` 4605 >> `!q. extractGBATrans (props f) gba q = 4606 ABS_TRNS q` 4607 suffices_by metis_tac[] 4608 >> gen_tac >> simp[SET_EQ_SUBSET,SUBSET_DEF] 4609 >> qunabbrev_tac `ABS_TRNS` >> strip_tac 4610 >- (simp[extractGBATrans_def] >> rpt strip_tac 4611 >> `q ��� concr2AbstrGBA_states gba` by ( 4612 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4613 >> fs[OPTION_TO_LIST_MEM] >> rename[`_ x1 = SOME l`] 4614 >> Cases_on `x1` >> fs[] >> rw[] 4615 >> fs[CAT_OPTIONS_MEM,MEM_MAP] 4616 >> Cases_on `y` >> fs[] 4617 >> qexists_tac `r` >> fs[] 4618 >> `MEM (q',r) (toAList gba.nodeInfo) 4619 ��� (��(i,n). set n.frmls = q) (q',r)` 4620 by metis_tac[findNode_def,FIND_LEMM2] 4621 >> fs[] >> metis_tac[MEM_toAList,domain_lookup] 4622 ) 4623 >> `x ��� gba_trans (concr2AbstrAA (concrAA g_AA init aP)) q` 4624 suffices_by metis_tac[IN_INTER] 4625 >> fs[OPTION_TO_LIST_MEM] >> rename[`findNode _ gba = SOME x1`] 4626 >> Cases_on `x1` >> fs[] 4627 >> `MEM (q',r) (toAList gba.nodeInfo) 4628 ��� (��(i,n). set n.frmls = q) (q',r)` 4629 by metis_tac[findNode_def,FIND_LEMM2] 4630 >> fs[] 4631 >> `q ��� POW abstrAA.states` by metis_tac[IN_INTER] 4632 >> fs[trns_correct_def] 4633 >> first_x_assum (qspec_then `q'` mp_tac) >> strip_tac 4634 >> first_x_assum (qspec_then `r` mp_tac) >> strip_tac 4635 >> first_x_assum (qspec_then `fls` mp_tac) >> simp[] 4636 >> `(lookup q' gba.nodeInfo = SOME r) 4637 ��� (q ��� POW (concr2AbstrAA (concrAA g_AA init aP)).states)` 4638 by metis_tac[MEM_toAList] 4639 >> metis_tac[] 4640 ) 4641 >- (simp[extractGBATrans_def] >> rpt strip_tac 4642 >> `q ��� concr2AbstrGBA_states gba` by ( 4643 metis_tac[MEMBER_NOT_EMPTY,IN_INTER] 4644 ) 4645 >> `x ��� gba_trans (concr2AbstrAA (concrAA g_AA init aP)) q` 4646 by metis_tac[MEMBER_NOT_EMPTY] 4647 >> simp[OPTION_TO_LIST_MEM] 4648 >> Q.HO_MATCH_ABBREV_TAC 4649 `?l. (?x. F1 x ��� (L x = SOME l)) ��� (MEM x l)` 4650 >> `?x. F1 x` by ( 4651 qunabbrev_tac `F1` >> fs[concr2AbstrGBA_states_def] 4652 >> simp[findNode_def] 4653 >> `?x. (MEM x (toAList gba.nodeInfo)) 4654 ��� (��(i,n). set n.frmls = set x'.frmls) x` 4655 suffices_by metis_tac[FIND_LEMM] 4656 >> qexists_tac `(n,x')` >> fs[] 4657 >> metis_tac[MEM_toAList] 4658 ) 4659 >> `?l. L x' = SOME l` by ( 4660 qunabbrev_tac `L` >> qunabbrev_tac `F1` >> fs[] 4661 >> Cases_on `x'` >> simp[] 4662 >> `MEM (q',r) (toAList gba.nodeInfo)` 4663 by metis_tac[findNode_def,FIND_LEMM2] 4664 >> metis_tac[wfg_def,domain_lookup,MEM_toAList] 4665 ) 4666 >> qexists_tac `l` >> fs[] >> conj_tac 4667 >- metis_tac[] 4668 >- ( 4669 qunabbrev_tac `L` >> qunabbrev_tac `F1` >> fs[] 4670 >> fs[trns_correct_def] 4671 >> `q ��� POW abstrAA.states` by metis_tac[IN_INTER] 4672 >> Cases_on `x'` 4673 >> `MEM (q',r) (toAList gba.nodeInfo) 4674 ��� (��(i,n). set n.frmls = q) (q',r)` 4675 by metis_tac[findNode_def,FIND_LEMM2] 4676 >> first_x_assum (qspec_then `q'` mp_tac) >> strip_tac 4677 >> first_x_assum (qspec_then `r` mp_tac) >> strip_tac 4678 >> `?fls. lookup q' gba.followers = SOME fls` 4679 by metis_tac[MEM_toAList,domain_lookup,wfg_def] 4680 >> first_x_assum (qspec_then `fls` mp_tac) >> simp[] 4681 >> `(lookup q' gba.nodeInfo = SOME r) 4682 ��� (q ��� POW (concr2AbstrAA (concrAA g_AA init aP)).states)` 4683 by metis_tac[MEM_toAList] 4684 >> fs[] >> metis_tac[] 4685 ) 4686 ) 4687 ) 4688 >- (`!l u ce. MEM u (get_acc_set l ce) 4689 ==> MEM u (MAP FST l)` by ( 4690 Induct_on `l` >> fs[get_acc_set_def,CAT_OPTIONS_def] 4691 >> rpt strip_tac >> fs[CAT_OPTIONS_MEM] 4692 >> Cases_on `h` >> fs[MEM_MAP] >> Cases_on `y` >> fs[] 4693 >> metis_tac[FST] 4694 ) 4695 >> `!id q. (lookup id gba.nodeInfo = SOME q) 4696 ==> set q.frmls ��� concr2AbstrGBA_states gba` by ( 4697 rpt strip_tac >> fs[] 4698 >> PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4699 >> simp[] >> qexists_tac `q` >> metis_tac[domain_lookup] 4700 ) 4701 >> qunabbrev_tac `FINAL` >> simp[concr2AbstrGBA_final_def] 4702 >> `���ce u aE. 4703 (aE = concr2AbstractEdge (set aP) ce) ��� is_until u 4704 ��� MEM u (graphStates g_AA) ��� MEM_SUBSET ce.pos aP 4705 ��� MEM_SUBSET ce.neg aP ��� MEM_SUBSET ce.sucs (graphStates g_AA) ��� 4706 ���qs2. 4707 qs2 ��� POW abstrAA.states ��� 4708 (MEM u (get_acc_set final_trans ce) ��� 4709 (qs2,FST aE,SND aE) ��� acc_cond abstrAA u)` by ( 4710 HO_MATCH_MP_TAC CONCR_ACC_SETS 4711 >> simp[] >> metis_tac[] 4712 ) 4713 >> fs[final_correct_def] 4714 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 4715 >> qabbrev_tac `realTrans = 4716 {(e,a,e') | (a,e') ��� gba_trans abstrAA e ��� e ��� POW abstrAA.states}` 4717 >- (rename[`MEM u (graphStates g_AA)`] 4718 >> qexists_tac `acc_cond abstrAA u ��� realTrans` 4719 >> rpt strip_tac 4720 >- (rename[`t ��� x`] 4721 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 4722 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 4723 >> first_x_assum (qspec_then `t` mp_tac) 4724 >> Cases_on `t` >> simp[] >> Cases_on `r` >> rpt strip_tac 4725 >> fs[] >> rename[`(e,a,e') ��� x`] >> simp[] 4726 >> rpt strip_tac 4727 >- ( 4728 first_x_assum 4729 (qspec_then `concrEdge eL.pos_lab eL.neg_lab q2.frmls` mp_tac) 4730 >> simp[] >> strip_tac 4731 >> first_x_assum (qspec_then `u` mp_tac) 4732 >> first_x_assum (qspec_then `id1` mp_tac) >> simp[] 4733 >> first_x_assum (qspec_then `id1` mp_tac) >> simp[] >> strip_tac 4734 >> first_x_assum (qspec_then `eL` mp_tac) >> simp[] >> strip_tac 4735 >> first_x_assum (qspec_then `id2` mp_tac) >> simp[] 4736 >> `set q1.frmls ��� 4737 concr2AbstrGBA_states gba` by ( 4738 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4739 >> simp[] >> qexists_tac `q1` 4740 >> metis_tac[MEM_toAList,domain_lookup] 4741 ) 4742 >> `set q1.frmls ��� 4743 POW (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 4744 metis_tac[IN_INTER] 4745 ) 4746 >> simp[] >> strip_tac 4747 >> first_x_assum (qspec_then `u` mp_tac) >> simp[] >> strip_tac 4748 >> `MEM u (MAP FST (final_trans))` by metis_tac[] 4749 >> fs[MEM_MAP] >> Cases_on `y` >> fs[] 4750 >> `���id nL. 4751 (findNode (��(i,l). l.frml = u) g_AA = SOME (id,nL)) 4752 ��� is_until u` by metis_tac[valid_acc_def,FST] 4753 >> `is_until u ��� MEM u (graphStates g_AA)` by ( 4754 simp[graphStates_def,MEM_MAP] 4755 >> `MEM (id,nL) (toAList g_AA.nodeInfo) 4756 ��� (��(i,l). l.frml = u) (id,nL)` 4757 by metis_tac[FIND_LEMM2,findNode_def] 4758 >> fs[] >> qexists_tac `(id,nL)` >> fs[] 4759 ) 4760 >> simp[] 4761 >> `MEM_SUBSET eL.pos_lab aP ��� 4762 MEM_SUBSET eL.neg_lab aP` by metis_tac[aP_correct_def] 4763 >> simp[] 4764 >> `MEM_SUBSET q2.frmls (graphStates g_AA)` by ( 4765 `set q2.frmls ��� concr2AbstrGBA_states gba` by ( 4766 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4767 >> simp[] >> qexists_tac `q2` 4768 >> metis_tac[MEM_toAList,domain_lookup] 4769 ) 4770 >> `set q2.frmls ��� 4771 POW (concr2AbstrAA (concrAA g_AA init aP)).states` 4772 by metis_tac[IN_INTER] 4773 >> fs[concr2AbstrAA_def,concr2Abstr_states_def] 4774 >> fs[IN_POW] >> simp[MEM_SUBSET_SET_TO_LIST] 4775 >> simp[graphStates_def,SUBSET_DEF] >> strip_tac 4776 >> simp[MEM_MAP] >> strip_tac 4777 >> `x' ��� 4778 {x.frml | 4779 ���n. SOME x = lookup n g_AA.nodeInfo 4780 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 4781 >> fs[] >> qexists_tac `(n,x'')` >> simp[] 4782 >> metis_tac[MEM_toAList] 4783 ) 4784 >> simp[] >> rw[] 4785 >> first_x_assum (qspec_then `set q1.frmls` mp_tac) >> simp[] 4786 >> simp[concr2AbstractEdge_def] 4787 ) 4788 >- (qunabbrev_tac `realTrans` >> fs[] 4789 >> `set q1.frmls ��� POW abstrAA.states ��� 4790 (reachableFromSetGBA 4791 (GBA (POW (concr2AbstrAA (concrAA g_AA init aP)).states) 4792 (concr2AbstrAA (concrAA g_AA init aP)).initial 4793 (gba_trans (concr2AbstrAA (concrAA g_AA init aP))) 4794 (gba_accTrans (concr2AbstrAA (concrAA g_AA init aP))) 4795 (concr2AbstrAA (concrAA g_AA init aP)).alphabet) 4796 (concr2AbstrAA (concrAA g_AA init aP)).initial)` by ( 4797 `set q1.frmls ��� concr2AbstrGBA_states gba` 4798 suffices_by metis_tac[IN_INTER] 4799 >> PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4800 >> simp[] >> qexists_tac `q1` 4801 >> metis_tac[MEM_toAList,domain_lookup] 4802 ) 4803 >> fs[] >> conj_tac 4804 >- (fs[trns_correct_def] 4805 >> `set 4806 (CAT_OPTIONS 4807 (MAP 4808 (��(eL,i). 4809 do 4810 s_nL <- lookup i gba.nodeInfo; 4811 SOME 4812 (transformLabel (set aP) eL.pos_lab 4813 eL.neg_lab,set s_nL.frmls) 4814 od) fls)) = gba_trans abstrAA (set q1.frmls)` 4815 by metis_tac[] 4816 >> `MEM (transformLabel (props f) eL.pos_lab eL.neg_lab, 4817 set q2.frmls) 4818 (CAT_OPTIONS 4819 (MAP 4820 (��(eL,i). 4821 do 4822 s_nL <- lookup i gba.nodeInfo; 4823 SOME 4824 (transformLabel (set aP) eL.pos_lab eL.neg_lab, 4825 set s_nL.frmls) 4826 od) fls))` suffices_by metis_tac[] 4827 >> simp[CAT_OPTIONS_MEM,MEM_MAP] 4828 >> qexists_tac `(eL,id2)` >> fs[] 4829 ) 4830 >- metis_tac[] 4831 ) 4832 >- metis_tac[IN_INTER] 4833 ) 4834 >- (fs[trns_correct_def] 4835 >> `e ��� POW abstrAA.states` 4836 by (qunabbrev_tac `realTrans` >> fs[]) 4837 >> `e ��� concr2AbstrGBA_states gba` by metis_tac[IN_INTER] 4838 >> POP_ASSUM mp_tac 4839 >> PURE_REWRITE_TAC[concr2AbstrGBA_states_def] >> simp[] 4840 >> strip_tac 4841 >> `?fls. lookup n gba.followers = SOME fls` 4842 by metis_tac[wfg_def,domain_lookup] 4843 >> `(a,e') ��� gba_trans abstrAA e` 4844 by (qunabbrev_tac `realTrans` >> fs[] >> metis_tac[]) 4845 >> `MEM (a,e') 4846 (CAT_OPTIONS 4847 (MAP 4848 (��(eL,i). 4849 do 4850 s_nL <- lookup i gba.nodeInfo; 4851 SOME 4852 (transformLabel (set aP) eL.pos_lab 4853 eL.neg_lab,set s_nL.frmls) 4854 od) fls))` by metis_tac[] 4855 >> fs[CAT_OPTIONS_MEM,MEM_MAP] >> Cases_on `y` >> fs[] 4856 >> fs[] 4857 >> first_x_assum (qspec_then 4858 `concrEdge q.pos_lab q.neg_lab s_nL.frmls` 4859 mp_tac) 4860 >> strip_tac 4861 >> first_x_assum (qspec_then `u` mp_tac) >> simp[] 4862 >> simp[] 4863 >> `MEM_SUBSET q.pos_lab aP ��� MEM_SUBSET q.neg_lab aP` 4864 by metis_tac[aP_correct_def] 4865 >> simp[] 4866 >> `MEM_SUBSET s_nL.frmls (graphStates g_AA)` by ( 4867 `set s_nL.frmls ��� concr2AbstrGBA_states gba` by ( 4868 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4869 >> simp[] >> qexists_tac `s_nL` 4870 >> metis_tac[MEM_toAList,domain_lookup] 4871 ) 4872 >> `set s_nL.frmls ��� 4873 POW (concr2AbstrAA (concrAA g_AA init aP)).states` 4874 by metis_tac[IN_INTER] 4875 >> fs[concr2AbstrAA_def,concr2Abstr_states_def] 4876 >> fs[IN_POW] >> simp[MEM_SUBSET_SET_TO_LIST] 4877 >> simp[graphStates_def,SUBSET_DEF] >> strip_tac 4878 >> simp[MEM_MAP] >> strip_tac 4879 >> `x''' ��� 4880 {x.frml | 4881 ���n. SOME x = lookup n g_AA.nodeInfo 4882 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 4883 >> fs[] >> qexists_tac `(n',x'''')` >> simp[] 4884 >> metis_tac[MEM_toAList] 4885 ) 4886 >> simp[] >> strip_tac 4887 >> first_x_assum (qspec_then `set x''.frmls` mp_tac) 4888 >> `set x''.frmls ��� 4889 POW (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 4890 `set x''.frmls ��� concr2AbstrGBA_states gba` by ( 4891 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4892 >> simp[] >> qexists_tac `x''` 4893 >> metis_tac[MEM_toAList,domain_lookup] 4894 ) 4895 >> metis_tac[IN_INTER] 4896 ) 4897 >> simp[concr2AbstractEdge_def] >> fs[] >> strip_tac 4898 >> `MEM u 4899 (get_acc_set final_trans 4900 (concrEdge q.pos_lab q.neg_lab s_nL.frmls))` 4901 by metis_tac[concr2AbstrAA_def] 4902 >> first_x_assum (qspec_then `(set x''.frmls,a,e')` mp_tac) 4903 >> simp[] 4904 >> Q.HO_MATCH_ABBREV_TAC `(A ==> B) ==> B` >> `A` suffices_by fs[] 4905 >> qunabbrev_tac `A` >> qexists_tac `x''` >> simp[] 4906 >> qexists_tac `q` >> fs[] >> qexists_tac `s_nL` >> fs[] 4907 >> strip_tac 4908 >- metis_tac[concr2AbstrAA_def] 4909 >- metis_tac[] 4910 ) 4911 >- (simp[gba_accTrans_def] >> qexists_tac `u` >> simp[] 4912 >> qunabbrev_tac `realTrans` >> fs[] 4913 >> simp[concr2AbstrAA_def,concr2Abstr_final_def] 4914 >> fs[graphStates_def,EXISTS_MEM,MEM_MAP] 4915 >> qexists_tac `SND y` >> simp[] 4916 >> fs[] >> Cases_on `y` >> fs[] >> conj_tac 4917 >- metis_tac[MEM_toAList,domain_lookup] 4918 >- (fs[until_iff_final_def,is_until_def] 4919 >> Cases_on `u` 4920 >> metis_tac[MEM_toAList,is_until_def] 4921 ) 4922 ) 4923 ) 4924 >- (fs[gba_accTrans_def] >> rename[`u ��� _.final`] 4925 >> qexists_tac `u` >> fs[] >> rpt strip_tac 4926 >- (POP_ASSUM mp_tac >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 4927 >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac 4928 >> first_x_assum (qspec_then `x'` mp_tac) 4929 >> Cases_on `x' ��� x` >> fs[] >> rpt strip_tac 4930 >> fs[trns_correct_def] 4931 >> `e ��� POW abstrAA.states` 4932 by (qunabbrev_tac `realTrans` >> fs[]) 4933 >> `e ��� concr2AbstrGBA_states gba` by metis_tac[IN_INTER] 4934 >> POP_ASSUM mp_tac 4935 >> PURE_REWRITE_TAC[concr2AbstrGBA_states_def] >> simp[] 4936 >> strip_tac 4937 >> `?fls. lookup n gba.followers = SOME fls` 4938 by metis_tac[wfg_def,domain_lookup] 4939 >> `(a,e') ��� gba_trans abstrAA e` 4940 by (qunabbrev_tac `realTrans` >> fs[] >> metis_tac[]) 4941 >> `MEM (a,e') 4942 (CAT_OPTIONS 4943 (MAP 4944 (��(eL,i). 4945 do 4946 s_nL <- lookup i gba.nodeInfo; 4947 SOME 4948 (transformLabel (set aP) eL.pos_lab 4949 eL.neg_lab,set s_nL.frmls) 4950 od) fls))` by metis_tac[] 4951 >> fs[CAT_OPTIONS_MEM,MEM_MAP] >> Cases_on `y` >> fs[] 4952 >> fs[] 4953 >> first_x_assum (qspec_then 4954 `concrEdge q.pos_lab q.neg_lab s_nL.frmls` 4955 mp_tac) 4956 >> strip_tac 4957 >> first_x_assum (qspec_then `u` mp_tac) >> simp[] 4958 >> `MEM u (graphStates g_AA)` by ( 4959 fs[concr2AbstrAA_def,concr2Abstr_final_def] 4960 >> simp[graphStates_def,EXISTS_MEM,MEM_MAP] 4961 >> metis_tac[SND,MEM_toAList] 4962 ) 4963 >> simp[] 4964 >> `MEM_SUBSET q.pos_lab aP ��� MEM_SUBSET q.neg_lab aP` 4965 by metis_tac[aP_correct_def] 4966 >> simp[] 4967 >> `MEM_SUBSET s_nL.frmls (graphStates g_AA)` by ( 4968 `set s_nL.frmls ��� concr2AbstrGBA_states gba` by ( 4969 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4970 >> simp[] >> qexists_tac `s_nL` 4971 >> metis_tac[MEM_toAList,domain_lookup] 4972 ) 4973 >> `set s_nL.frmls ��� 4974 POW (concr2AbstrAA (concrAA g_AA init aP)).states` 4975 by metis_tac[IN_INTER] 4976 >> fs[concr2AbstrAA_def,concr2Abstr_states_def] 4977 >> fs[IN_POW] >> simp[MEM_SUBSET_SET_TO_LIST] 4978 >> simp[graphStates_def,SUBSET_DEF] >> strip_tac 4979 >> simp[MEM_MAP] >> strip_tac 4980 >> `x''' ��� 4981 {x.frml | 4982 ���n. SOME x = lookup n g_AA.nodeInfo 4983 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 4984 >> fs[] >> qexists_tac `(n',x'''')` >> simp[] 4985 >> metis_tac[MEM_toAList] 4986 ) 4987 >> `is_until u` by ( 4988 fs[concr2AbstrAA_def,concr2Abstr_final_def] 4989 >> Cases_on `u` >> metis_tac[until_iff_final_def,is_until_def] 4990 ) 4991 >> simp[] 4992 >> `set x''.frmls ��� 4993 POW (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 4994 `set x''.frmls ��� concr2AbstrGBA_states gba` by ( 4995 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 4996 >> simp[] >> qexists_tac `x''` 4997 >> metis_tac[MEM_toAList,domain_lookup] 4998 ) 4999 >> metis_tac[IN_INTER] 5000 ) 5001 >> strip_tac 5002 >> first_x_assum (qspec_then `set x''.frmls` mp_tac) 5003 >> simp[concr2AbstractEdge_def] >> fs[] >> strip_tac 5004 >> `MEM u 5005 (get_acc_set final_trans 5006 (concrEdge q.pos_lab q.neg_lab s_nL.frmls))` 5007 by metis_tac[concr2AbstrAA_def] 5008 >> qexists_tac `x''` >> simp[] 5009 >> qexists_tac `q` >> fs[] >> qexists_tac `s_nL` >> fs[] 5010 >> strip_tac 5011 >- metis_tac[concr2AbstrAA_def] 5012 >- metis_tac[] 5013 ) 5014 >- (first_x_assum (qspec_then `x'` mp_tac) >> simp[] 5015 >> Q.HO_MATCH_ABBREV_TAC `(A ==> B) ==> B` 5016 >> `A` suffices_by fs[] >> qunabbrev_tac `A` 5017 >> `set q1.frmls ��� concr2AbstrGBA_states gba` by ( 5018 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 5019 >> simp[] >> qexists_tac `q1` 5020 >> metis_tac[MEM_toAList,domain_lookup] 5021 ) 5022 >> `(set q1.frmls ��� 5023 POW (concr2AbstrAA (concrAA g_AA init aP)).states) 5024 ��� set q1.frmls ��� 5025 reachableFromSetGBA 5026 (GBA (POW (concr2AbstrAA (concrAA g_AA init aP)).states) 5027 (concr2AbstrAA (concrAA g_AA init aP)).initial 5028 (gba_trans (concr2AbstrAA (concrAA g_AA init aP))) 5029 {acc_cond (concr2AbstrAA (concrAA g_AA init aP)) f ��� 5030 {(e,a,e') | 5031 (a,e') ��� 5032 gba_trans (concr2AbstrAA (concrAA g_AA init aP)) e 5033 ��� e ��� 5034 POW (concr2AbstrAA (concrAA g_AA init aP)).states} | 5035 f | 5036 f ��� (concr2AbstrAA (concrAA g_AA init aP)).final} 5037 (concr2AbstrAA (concrAA g_AA init aP)).alphabet) 5038 (concr2AbstrAA (concrAA g_AA init aP)).initial` 5039 by metis_tac[IN_INTER] 5040 >> simp[] 5041 >> first_x_assum 5042 (qspec_then `concrEdge eL.pos_lab eL.neg_lab q2.frmls` mp_tac) 5043 >> simp[] >> strip_tac 5044 >> first_x_assum (qspec_then `u` mp_tac) 5045 >> first_x_assum (qspec_then `id1` mp_tac) >> simp[] 5046 >> first_x_assum (qspec_then `id1` mp_tac) >> simp[] >> strip_tac 5047 >> first_x_assum (qspec_then `eL` mp_tac) >> simp[] >> strip_tac 5048 >> first_x_assum (qspec_then `id2` mp_tac) >> simp[] 5049 >> `set q1.frmls ��� 5050 concr2AbstrGBA_states gba` by ( 5051 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 5052 >> simp[] >> qexists_tac `q1` 5053 >> metis_tac[MEM_toAList,domain_lookup] 5054 ) 5055 >> `set q1.frmls ��� 5056 POW (concr2AbstrAA (concrAA g_AA init aP)).states` by ( 5057 metis_tac[IN_INTER] 5058 ) 5059 >> simp[] >> strip_tac 5060 >> first_x_assum (qspec_then `u` mp_tac) >> simp[] >> strip_tac 5061 >> `MEM u (MAP FST (final_trans))` by metis_tac[] 5062 >> fs[MEM_MAP] >> Cases_on `y` >> fs[] 5063 >> `���id nL. 5064 (findNode (��(i,l). l.frml = u) g_AA = SOME (id,nL)) 5065 ��� is_until u` by metis_tac[valid_acc_def,FST] 5066 >> `is_until u ��� MEM u (graphStates g_AA)` by ( 5067 simp[graphStates_def,MEM_MAP] 5068 >> `MEM (id,nL) (toAList g_AA.nodeInfo) 5069 ��� (��(i,l). l.frml = u) (id,nL)` 5070 by metis_tac[FIND_LEMM2,findNode_def] 5071 >> fs[] >> qexists_tac `(id,nL)` >> fs[] 5072 ) 5073 >> simp[] 5074 >> `MEM_SUBSET eL.pos_lab aP ��� 5075 MEM_SUBSET eL.neg_lab aP` by metis_tac[aP_correct_def] 5076 >> simp[] 5077 >> `MEM_SUBSET q2.frmls (graphStates g_AA)` by ( 5078 `set q2.frmls ��� concr2AbstrGBA_states gba` by ( 5079 PURE_REWRITE_TAC[concr2AbstrGBA_states_def] 5080 >> simp[] >> qexists_tac `q2` 5081 >> metis_tac[MEM_toAList,domain_lookup] 5082 ) 5083 >> `set q2.frmls ��� 5084 POW (concr2AbstrAA (concrAA g_AA init aP)).states` 5085 by metis_tac[IN_INTER] 5086 >> fs[concr2AbstrAA_def,concr2Abstr_states_def] 5087 >> fs[IN_POW] >> simp[MEM_SUBSET_SET_TO_LIST] 5088 >> simp[graphStates_def,SUBSET_DEF] >> strip_tac 5089 >> simp[MEM_MAP] >> strip_tac 5090 >> `x'' ��� 5091 {x.frml | 5092 ���n. SOME x = lookup n g_AA.nodeInfo 5093 ��� n ��� domain g_AA.nodeInfo}` by fs[SUBSET_DEF] 5094 >> fs[] >> qexists_tac `(n,x''')` >> simp[] 5095 >> metis_tac[MEM_toAList] 5096 ) 5097 >> simp[] >> rw[] 5098 >> first_x_assum (qspec_then `set q1.frmls` mp_tac) >> simp[] 5099 >> simp[concr2AbstractEdge_def] 5100 >> strip_tac 5101 >> fs[trns_correct_def] 5102 >> first_x_assum (qspec_then `id1` mp_tac) >> simp[] >> strip_tac 5103 >> `MEM (transformLabel (props f) eL.pos_lab eL.neg_lab, 5104 set q2.frmls) 5105 (CAT_OPTIONS 5106 (MAP 5107 (��(eL',i). 5108 do 5109 s_nL <- lookup i gba.nodeInfo; 5110 SOME 5111 (transformLabel (props f) eL'.pos_lab 5112 eL'.neg_lab,set s_nL.frmls) 5113 od) fls))` suffices_by metis_tac[] 5114 >> simp[CAT_OPTIONS_MEM,MEM_MAP] 5115 >> qexists_tac `(eL,id2)` >> fs[] 5116 ) 5117 >- (fs[concr2AbstrAA_def,concr2Abstr_final_def] 5118 >> Cases_on `u` >> metis_tac[until_iff_final_def,is_until_def] 5119 ) 5120 >- (fs[concr2AbstrAA_def,concr2Abstr_final_def] 5121 >> simp[graphStates_def,MEM_MAP] 5122 >> qexists_tac `(n,x')` >> fs[] >> metis_tac[MEM_toAList] 5123 ) 5124 ) 5125 ) 5126 >- (qunabbrev_tac `ALPH` >> fs[] >> simp[concr2AbstrAA_def]) 5127 ); 5128 5129val EXPGBA_CORRECT = store_thm 5130 ("EXPGBA_CORRECT", 5131 ``!f concr_AA abstrAA. 5132 (expandAuto_init f = SOME concr_AA) 5133 ��� (abstrAA = concr2AbstrAA concr_AA) 5134 ==> ?c_gba. 5135 (expandGBA_init concr_AA = SOME c_gba) 5136 ��� (concr2AbstrGBA c_gba = 5137 removeStatesSimpl (vwaa2gba abstrAA))``, 5138 rpt gen_tac >> strip_tac 5139 >> `case expandGBA_init concr_AA of 5140 NONE => F 5141 | SOME c_gba => 5142 concr2AbstrGBA c_gba = removeStatesSimpl (vwaa2gba abstrAA)` 5143 by (Cases_on `concr_AA` >> fs[] >> metis_tac[EXPGBA_CORRECT_LEMM]) 5144 >> Cases_on `expandGBA_init concr_AA` >> fs[] 5145 ); 5146 5147val _ = export_theory() 5148