1open HolKernel Parse bossLib boolLib gfgTheory listTheory optionTheory pred_setTheory rich_listTheory arithmeticTheory sortingTheory relationTheory 2 3open sptreeTheory ltlTheory generalHelpersTheory concrRepTheory concrltl2waaTheory buechiATheory 4 5val _ = new_theory "concrGBArep" 6 7val _ = monadsyntax.temp_add_monadsyntax(); 8val _ = overload_on("monad_bind",``OPTION_BIND``); 9 10val _ = Datatype` 11 edgeLabelGBA = <| pos_lab : (�� list) ; 12 neg_lab : (�� list) ; 13 acc_set : (�� ltl_frml) list 14 |>` ; 15 16val _ = Datatype` 17 nodeLabelGBA = <| frmls : (�� ltl_frml) list |>` ; 18 19val _ = Datatype` 20 concrGBA = <| graph : (�� nodeLabelGBA, �� edgeLabelGBA) gfg ; 21 init : (num list) ; 22 all_acc_frmls : (�� ltl_frml) list; 23 atomicProp : �� list 24 |>`; 25 26val gba_trans_concr_def = Define` 27 gba_trans_concr ts_lists = 28 FOLDR d_conj_concr [(concrEdge [] [] [])] ts_lists `; 29 30val GBA_TRANS_LEMM1 = store_thm 31 ("GBA_TRANS_LEMM1", 32 ``!x s. MEM x (gba_trans_concr s) 33 ==> ((!l. MEM l s 34 ==> (?cE. MEM cE l 35 ��� (MEM_SUBSET cE.pos x.pos) 36 ��� (MEM_SUBSET cE.neg x.neg) 37 ��� (MEM_SUBSET cE.sucs x.sucs) 38 )) 39 ��� (?f. let s_with_ind = GENLIST (��n. (EL n s,n)) (LENGTH s) 40 in 41 let x1 = 42 FOLDR 43 (��sF e. 44 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 45 sucs := sF.sucs ��� e.sucs|>) 46 (concrEdge [] [] []) (MAP f s_with_ind) 47 in (cE_equiv x x1) 48 ��� (!q i. MEM (q,i) s_with_ind 49 ==> MEM (f (q,i)) q)) 50 ��� (ALL_DISTINCT x.pos ��� ALL_DISTINCT x.neg 51 ��� ALL_DISTINCT x.sucs))``, 52 Q.HO_MATCH_ABBREV_TAC 53 `!x s. MEM x (gba_trans_concr s) ==> A x s ��� B x s` 54 >> `!x s. MEM x (gba_trans_concr s) ==> A x s ��� (A x s ==> B x s)` 55 suffices_by fs[] 56 >> qunabbrev_tac `A` >> qunabbrev_tac `B` 57 >> Induct_on `s` >> fs[gba_trans_concr_def] >> rpt strip_tac 58 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def]) 59 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def] 60 >> fs[d_conj_concr_def,FOLDR_LEMM4] >> qexists_tac `e1` >> simp[] 61 >> metis_tac[MEM_SUBSET_APPEND,nub_set,MEM_SUBSET_SET_TO_LIST] 62 ) 63 >- (fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def] 64 >> fs[d_conj_concr_def,FOLDR_LEMM4] 65 >> `���cE. 66 MEM cE l ��� MEM_SUBSET cE.pos e2.pos ��� 67 MEM_SUBSET cE.neg e2.neg ��� MEM_SUBSET cE.sucs e2.sucs` 68 by metis_tac[] 69 >> qexists_tac `cE` 70 >> metis_tac[MEM_SUBSET_APPEND,MEM_SUBSET_TRANS,nub_set, 71 MEM_SUBSET_SET_TO_LIST] 72 ) 73 >- (Cases_on `s= []` >> fs[] 74 >- (fs[d_conj_concr_def,FOLDR_CONS,MEM_MAP] 75 >> qexists_tac ` 76 ��(q,i). 77 if (q,i) = (h,0) then e1 else ARB` 78 >> simp[] >> fs[d_conj_concr_def,FOLDR_CONS,MEM_MAP] 79 >> simp[cE_equiv_def,nub_set,MEM_EQUAL_SET] 80 ) 81 >- (fs[d_conj_concr_def,FOLDR_LEMM4] 82 >> first_x_assum (qspec_then `e2` mp_tac) >> simp[] >> strip_tac 83 >> qabbrev_tac `s_ind = (GENLIST (��n. (EL n s,n)) (LENGTH s))` 84 >> `���f. 85 cE_equiv e2 86 (FOLDR 87 (��sF e. 88 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 89 sucs := sF.sucs ��� e.sucs|>) (concrEdge [] [] []) 90 (MAP f s_ind)) 91 ��� (!q i. MEM (q,i) s_ind ==> MEM (f (q,i)) q) 92 ��� ALL_DISTINCT e2.pos ��� ALL_DISTINCT e2.neg 93 ��� ALL_DISTINCT e2.sucs` by metis_tac[] 94 >> qexists_tac ` 95 ��(q,i). 96 if i = 0 97 then e1 98 else f (q,i-1)` >> simp[] 99 >> fs[FOLDR_CONCR_EDGE] >> fs[nub_append] >> rpt strip_tac 100 >> fs[concrEdge_component_equality] 101 >- (qunabbrev_tac `s_ind` >> fs[] 102 >> fs[cE_equiv_def] >> rw[MEM_EQUAL_SET,LIST_TO_SET_FILTER] 103 >> (simp[SET_EQ_SUBSET,SUBSET_DEF] 104 >> strip_tac >> fs[GENLIST] 105 >- (rpt strip_tac 106 >> Q.HO_MATCH_ABBREV_TAC 107 `MEM k (FOLDR (��e pr. (g e) ��� pr) [] L)` 108 >- (`MEM e1 L` 109 suffices_by metis_tac[MEM_SUBSET_SET_TO_LIST, 110 FOLDR_APPEND_LEMM,SUBSET_DEF] 111 >> qunabbrev_tac `L` >> simp[MEM_MAP] 112 >> qexists_tac `(h,0)` >> fs[EL,MEM_GENLIST] 113 >> simp[LENGTH_NOT_NULL,NULL_EQ] 114 ) 115 >- (`?e. MEM e L ��� (MEM k (g e))` 116 suffices_by metis_tac[FOLDR_LEMM6] 117 >> qunabbrev_tac `L` >> simp[MEM_MAP] >> fs[] 118 >> `MEM k 119 (FOLDR (��e pr. g e ��� pr) [] 120 (MAP f (GENLIST (��n. (EL n s,n)) (LENGTH s))))` 121 by metis_tac[MEM_EQUAL_SET] 122 >> fs[FOLDR_LEMM6] >> qexists_tac `a` >> strip_tac 123 >- (fs[MEM_MAP] >> qexists_tac `(FST y,SND y+1)` 124 >> simp[] >> fs[MEM_GENLIST] 125 >> rename [���n + 1 = LENGTH s���, 126 ���EL (LENGTH s) (h::s)���] 127 >> Cases_on `SUC n=LENGTH s` >> fs[] 128 >> metis_tac[EL,TL,DECIDE ``n+1 = SUC n``] 129 ) 130 >- fs[] 131 ) 132 ) 133 >- (rpt strip_tac >> fs[FOLDR_LEMM6,MEM_MAP] 134 >- (rw[] >> fs[] >> Cases_on `s = []` >> fs[] 135 >> disj2_tac >> Q.HO_MATCH_ABBREV_TAC `MEM k (g e2)` 136 >> `MEM k 137 (FOLDR (��e pr. g e ��� pr) [] 138 (MAP f (GENLIST (��n. (EL n s,n)) (LENGTH s))))` 139 suffices_by metis_tac[MEM_EQUAL_SET] 140 >> simp[FOLDR_LEMM6,MEM_GENLIST,MEM_MAP] 141 >> qexists_tac `f (EL (LENGTH s) (h::s),LENGTH s ��� 1)` 142 >> simp[] 143 >> qexists_tac `(EL (LENGTH s) (h::s),LENGTH s ��� 1)` 144 >> fs[] >> `0 < LENGTH s` by (Cases_on `s` >> fs[]) 145 >> rw[] 146 >> `?n. SUC n = LENGTH s` 147 by (Cases_on `LENGTH s` >> simp[]) 148 >> `n = LENGTH s -1` by simp[] >> metis_tac[EL,TL] 149 ) 150 >- (fs[MEM_GENLIST] >> rw[] >> fs[] 151 >> rename [���MEM x (_ (if n = 0 then _ else _))���] 152 >> Cases_on `n = 0` >> fs[] >> disj2_tac 153 >> Q.HO_MATCH_ABBREV_TAC `MEM k (g e2)` 154 >> `MEM k 155 (FOLDR (��e pr. g e ��� pr) [] 156 (MAP f (GENLIST (��n. (EL n s,n)) (LENGTH s))))` 157 suffices_by metis_tac[MEM_EQUAL_SET] 158 >> simp[FOLDR_LEMM6,MEM_GENLIST,MEM_MAP] 159 >> qexists_tac `f (EL n (h::s),n-1)` 160 >> simp[] 161 >> qexists_tac `(EL n (h::s),n ��� 1)` 162 >> fs[] >> `0 < n` by fs[] 163 >> `?p. SUC p = n` 164 by (Cases_on `n` >> simp[]) 165 >> `p = n -1` by simp[] >> metis_tac[EL,TL] 166 ) 167 ) 168 ) 169 ) 170 >> qunabbrev_tac `s_ind` >> fs[] 171 >> Cases_on `i=0` >> fs[MEM_GENLIST] 172 >> `?p. SUC p = i` by (Cases_on `i` >> simp[]) 173 >> rw[] 174 ) 175 ) 176 >- (fs[d_conj_concr_def] >> fs[FOLDR_LEMM4] >> fs[all_distinct_nub]) 177 >- (fs[d_conj_concr_def] >> fs[FOLDR_LEMM4] >> fs[all_distinct_nub]) 178 >- (fs[d_conj_concr_def] >> fs[FOLDR_LEMM4] >> fs[all_distinct_nub]) 179 ); 180 181val GBA_TRANS_LEMM2 = store_thm 182 ("GBA_TRANS_LEMM2", 183 ``!s f. (!q i. ((q = EL i s) ��� i < LENGTH s) 184 ==> MEM (f i) q) 185 ==> ?x. cE_equiv x 186 (FOLDR 187 (��sF e. 188 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 189 sucs := sF.sucs ��� e.sucs|>) 190 (concrEdge [] [] []) (MAP f (COUNT_LIST (LENGTH s)))) 191 ��� MEM x(gba_trans_concr s)``, 192 Induct_on `s` >> fs[gba_trans_concr_def] 193 >> rw[FOLDR_CONCR_EDGE] 194 >- fs[cE_equiv_def,MEM_EQUAL_def,MEM_SUBSET_def,COUNT_LIST_def] 195 >- (first_x_assum (qspec_then `��n. f (n + 1)` mp_tac) 196 >> `!i. i < LENGTH s ==> MEM (f (i + 1)) (EL i s)` by ( 197 rpt strip_tac >> `MEM (f (SUC i)) (EL (SUC i) (h::s))` by fs[] 198 >> fs[EL,TL] >> metis_tac[DECIDE ``i+1=SUC i``] 199 ) 200 >> simp[] 201 >> rpt strip_tac >> simp[d_conj_concr_def] >> rw[FOLDR_LEMM4] 202 >> fs[FOLDR_CONCR_EDGE] 203 >> qexists_tac ` 204 concrEdge 205 (nub ((f 0).pos ++ x.pos)) 206 (nub ((f 0).neg ++ x.neg)) 207 (nub ((f 0).sucs ++ x.sucs))` 208 >> fs[] >> strip_tac 209 >- (fs[cE_equiv_def,MEM_EQUAL_SET] >> rpt strip_tac 210 >> Q.HO_MATCH_ABBREV_TAC ` 211 set (g (f 0)) ��� 212 set 213 (FOLDR (��e pr. (g e) ��� pr) [] 214 (MAP (��n. f (n + 1)) (COUNT_LIST (LENGTH s)))) = 215 set (FOLDR (��e pr. (g e) ��� pr) [] 216 (MAP f (COUNT_LIST (SUC (LENGTH s)))))` 217 >> `MAP f (COUNT_LIST (SUC (LENGTH s))) 218 = f 0 :: MAP (��n. f (n + 1)) (COUNT_LIST (LENGTH s))` by ( 219 simp[COUNT_LIST_def,MAP_MAP_o] 220 >> `(f o SUC) = (��n. f (n + 1))` suffices_by fs[] 221 >> `!n. (f o SUC) n = (��n. f (n + 1)) n` suffices_by metis_tac[] 222 >> fs[SUC_ONE_ADD] 223 ) 224 >> rw[] 225 ) 226 >- (qexists_tac `f 0` >> fs[] 227 >> qexists_tac `x` >> fs[FOLDR_CONCR_EDGE,concrEdge_component_equality] 228 >> `MEM (f 0) (EL 0 (h::s))` 229 by metis_tac[DECIDE ``0 < SUC (LENGTH s)``] 230 >> fs[EL,TL] 231 ) 232 ) 233 ); 234 235val GBA_TRANS_LEMM3 = store_thm 236 ("GBA_TRANS_LEMM3", 237 ``(!s x t. MEM x (gba_trans_concr t) ��� MEM s x.sucs 238 ==> (?l ce. MEM l t ��� MEM ce l ��� MEM s ce.sucs)) 239 ��� (!s x t. MEM x (gba_trans_concr t) ��� MEM s x.pos 240 ==> (?l ce. MEM l t ��� MEM ce l ��� MEM s ce.pos)) 241 ��� (!s x t. MEM x (gba_trans_concr t) ��� MEM s x.neg 242 ==> (?l ce. MEM l t ��� MEM ce l ��� MEM s ce.neg))``, 243 rpt conj_tac 244 >> Induct_on `t` >> rpt strip_tac >> fs[gba_trans_concr_def] 245 >- (fs[concrEdge_component_equality] >> metis_tac[MEMBER_NOT_EMPTY,MEM]) 246 >- (fs[d_conj_concr_def,FOLDR_LEMM4,concrEdge_component_equality] 247 >> `MEM s (nub (e1.sucs ++ e2.sucs))` by metis_tac[] 248 >> fs[nub_append] 249 >> `MEM s (nub (FILTER (��x. ��MEM x e2.sucs) e1.sucs)) 250 \/ MEM s (nub e2.sucs)` by metis_tac[MEM_APPEND] 251 >> metis_tac[] 252 ) 253 >- (fs[concrEdge_component_equality] >> metis_tac[MEMBER_NOT_EMPTY,MEM]) 254 >- (fs[d_conj_concr_def,FOLDR_LEMM4,concrEdge_component_equality] 255 >> `MEM s (nub (e1.pos ++ e2.pos))` by metis_tac[] 256 >> fs[nub_append] 257 >> `MEM s (nub (FILTER (��x. ��MEM x e2.pos) e1.pos)) 258 \/ MEM s (nub e2.pos)` by metis_tac[MEM_APPEND] 259 >> metis_tac[] 260 ) 261 >- (fs[concrEdge_component_equality] >> metis_tac[MEMBER_NOT_EMPTY,MEM]) 262 >- (fs[d_conj_concr_def,FOLDR_LEMM4,concrEdge_component_equality] 263 >> `MEM s (nub (e1.neg ++ e2.neg))` by metis_tac[] 264 >> fs[nub_append] 265 >> `MEM s (nub (FILTER (��x. ��MEM x e2.neg) e1.neg)) 266 \/ MEM s (nub e2.neg)` by metis_tac[MEM_APPEND] 267 >> metis_tac[] 268 ) 269 ); 270 271val GBA_TRANS_LEMM = store_thm 272 ("GBA_TRANS_LEMM", 273 ``!aP trns_concr_list. 274 ALL_DISTINCT (MAP FST trns_concr_list) 275 ==> 276 let concr_edgs_list = MAP SND trns_concr_list 277 in let to_abstr l = MAP (concr2AbstractEdge aP) l 278 in set (to_abstr (gba_trans_concr concr_edgs_list)) 279 = d_conj_set (set (MAP (��(q,d). (q,set (to_abstr d))) 280 trns_concr_list)) (POW aP)``, 281 rpt strip_tac >> fs[] >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 282 >> fs[MEM_MAP] 283 >- (Q.HO_MATCH_ABBREV_TAC `concr2AbstractEdge aP y ��� d_conj_set s A` 284 >> Cases_on `s = {}` 285 >- (qunabbrev_tac `s` >> rw[] >> simp[d_conj_set_def,ITSET_THM] 286 >> fs[gba_trans_concr_def,concr2AbstractEdge_def,transformLabel_def] 287 ) 288 >-( 289 qabbrev_tac `s_ind = 290 GENLIST (��n. (EL n (MAP SND trns_concr_list),n)) 291 (LENGTH (MAP SND trns_concr_list))` 292 >> `?f. cE_equiv y 293 (FOLDR 294 (��sF e. 295 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 296 sucs := sF.sucs ��� e.sucs|>) (concrEdge [] [] []) 297 (MAP f s_ind)) 298 ��� (!q i. MEM (q,i) s_ind ==> MEM (f (q,i)) q)` 299 by metis_tac[GBA_TRANS_LEMM1] 300 >> qabbrev_tac 301 `a_sel = ��q. 302 if ?d i. (q,d) = EL i trns_concr_list 303 ��� i < LENGTH trns_concr_list 304 then (let d = @(x,i). (q,x) = EL i trns_concr_list 305 ��� MEM (x,i) s_ind 306 in transformLabel aP (f d).pos (f d).neg) 307 else ARB` 308 >> qabbrev_tac 309 `e_sel = ��q. 310 if ?d i. (q,d) = EL i trns_concr_list 311 ��� i < LENGTH trns_concr_list 312 then (let d = @(x,i). (q,x) = EL i trns_concr_list 313 ��� MEM (x,i) s_ind 314 in set ((f d).sucs)) 315 else ARB` 316 >> qabbrev_tac `Y = 317 (FOLDR 318 (��sF e. 319 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 320 sucs := sF.sucs ��� e.sucs|>) (concrEdge [] [] []) 321 (MAP f s_ind))` 322 >> `concr2AbstractEdge aP Y ��� d_conj_set s A` 323 suffices_by metis_tac[C2A_EDGE_CE_EQUIV] 324 >> `concr2AbstractEdge aP Y = 325 ((POW aP) ��� BIGINTER {a_sel q | q ��� IMAGE FST s}, 326 BIGUNION {e_sel q | q ��� IMAGE FST s})` by ( 327 qunabbrev_tac `Y` 328 >> simp[concr2AbstractEdge_def,FOLDR_LEMM6] 329 >> rw[FOLDR_CONCR_EDGE] >> simp[concr2AbstractEdge_def] 330 >> rpt strip_tac 331 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 332 >- (qunabbrev_tac `A` >> metis_tac[TRANSFORMLABEL_AP,SUBSET_DEF]) 333 >- (`x ��� a_sel q` suffices_by rw[] 334 >> qunabbrev_tac `s` >> qunabbrev_tac `a_sel` >> fs[] 335 >> `���d i. (FST x',d) = EL i trns_concr_list 336 ��� i < LENGTH trns_concr_list` by ( 337 fs[MEM_ZIP,MEM_EL] 338 >> qexists_tac `SND (EL n' trns_concr_list)` 339 >> qexists_tac `n'` >> fs[LENGTH_MAP,EL_MAP] 340 >> Cases_on `EL n' trns_concr_list` >> fs[] 341 ) 342 >> `x ��� transformLabel aP 343 (f (@(x,i). (FST x',x) = EL i trns_concr_list 344 ��� MEM (x,i) s_ind)).pos 345 (f (@(x,i). (FST x',x) = EL i trns_concr_list 346 ��� MEM (x,i) s_ind)).neg` 347 suffices_by metis_tac[] 348 >> qabbrev_tac `D = (@(x,i). (FST x',x) = EL i trns_concr_list 349 ��� MEM (x,i) s_ind)` 350 >> `(FST x',FST D) = EL (SND D) trns_concr_list 351 ��� MEM D s_ind` by ( 352 `(��k. (FST x',FST k) = EL (SND k) trns_concr_list 353 ��� MEM k s_ind) D` suffices_by fs[] 354 >> qunabbrev_tac `D` >> Q.HO_MATCH_ABBREV_TAC `(J ($@ Q))` 355 >> HO_MATCH_MP_TAC SELECT_ELIM_THM >> qunabbrev_tac `J` 356 >> qunabbrev_tac `Q` >> fs[] >> rpt strip_tac 357 >- (qunabbrev_tac `s_ind` >> simp[MEM_GENLIST,MEM_EL] 358 >> qexists_tac `(d,i)` >> fs[EL_MAP] >> rw[] 359 >> Cases_on `EL i trns_concr_list` >> fs[] 360 ) 361 >- (Cases_on `x''` >> fs[]) 362 >- (Cases_on `x''` >> fs[]) 363 ) 364 >> `MEM (f D) (MAP f s_ind)` by ( 365 simp[MEM_MAP] >> qexists_tac `D` >> fs[] 366 >> qexists_tac `(FST x',D)` >> fs[] 367 ) 368 >> metis_tac[TRANSFORMLABEL_SUBSET,FOLDR_APPEND_LEMM,SUBSET_DEF] 369 ) 370 >- (`!q. MEM q (MAP FST trns_concr_list) ==> x ��� a_sel q` by ( 371 rpt strip_tac >> fs[MEM_MAP] 372 >> first_x_assum (qspec_then `a_sel q` mp_tac) 373 >> simp[] >> Q.HO_MATCH_ABBREV_TAC `(Q ==> B) ==> B` 374 >> `Q` suffices_by fs[] >> qunabbrev_tac `Q` 375 >> qexists_tac `q` >> rw[] 376 >> qunabbrev_tac `s` >> simp[MEM_MAP] 377 >> rename [`MEM k trns_concr_list`] 378 >> qexists_tac 379 `(��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) k` 380 >> simp[] 381 >> Cases_on `k` >> simp[] >> qexists_tac `(q,r)` 382 >> simp[] 383 ) 384 >> `(���e. MEM e (MAP f s_ind) 385 ��� x ��� transformLabel aP e.pos e.neg) ��� x ��� POW aP` 386 suffices_by metis_tac[TRANSFORMLABEL_FOLDR] 387 >> rpt strip_tac >> fs[MEM_MAP] 388 >> qunabbrev_tac `s_ind` >> fs[MEM_GENLIST] 389 >> rename [���n < LENGTH trns_concr_list���, 390 ���(EL n (MAP SND trns_concr_list), n)���] 391 >> `MEM (EL n trns_concr_list) trns_concr_list` 392 by metis_tac[EL_MEM] 393 >> `?q d. EL n trns_concr_list = (q,d)` by ( 394 Cases_on `EL n trns_concr_list` >> fs[] 395 ) 396 >> `MEM (q,d) trns_concr_list ��� FST (q,d) = q` by fs[] 397 >> `x ��� a_sel q` by metis_tac[MEM_EL] 398 >> qunabbrev_tac `a_sel` >> fs[] 399 >> `x ��� 400 transformLabel aP 401 (f (@(x,i). (q,x) = EL i trns_concr_list 402 ��� i < LENGTH trns_concr_list 403 ��� (x = EL i (MAP SND trns_concr_list)))).pos 404 (f (@(x,i). (q,x) = EL i trns_concr_list 405 ��� i < LENGTH trns_concr_list 406 ��� x = EL i (MAP SND trns_concr_list))).neg` by ( 407 `���d i. (q,d) = EL i trns_concr_list 408 ��� (i < LENGTH trns_concr_list)` suffices_by metis_tac[] 409 >> qexists_tac `d` >> fs[] >> metis_tac[MEM_EL] 410 ) 411 >> `(@(x,i). (q,x) = EL i trns_concr_list 412 ��� i < LENGTH trns_concr_list 413 ��� (x = EL i (MAP SND trns_concr_list))) = (d,n)` by ( 414 `(��j. (j = (d,n))) 415 ($@ (��(x,i). (q,x) = EL i trns_concr_list 416 ��� i < LENGTH trns_concr_list 417 ��� (x = EL i (MAP SND trns_concr_list))))` 418 suffices_by fs[] 419 >> Q.HO_MATCH_ABBREV_TAC `Q ($@ M)` 420 >> HO_MATCH_MP_TAC SELECT_ELIM_THM >> qunabbrev_tac `Q` 421 >> rpt strip_tac >> fs[] >> qunabbrev_tac `M` 422 >- (qexists_tac `(d,n)` >> fs[EL_MAP]) 423 >- (Cases_on `x'` >> fs[] >> `r = n` suffices_by fs[EL_MAP] 424 >> `EL n (MAP FST trns_concr_list) = q` by fs[EL_MAP] 425 >> `EL r (MAP FST trns_concr_list) = 426 FST (EL r trns_concr_list)` by metis_tac[EL_MAP] 427 >> rw[] >> Cases_on `EL r trns_concr_list` 428 >> rw[] 429 >> `EL r (MAP FST trns_concr_list) = 430 EL n (MAP FST trns_concr_list)` by fs[] 431 >> metis_tac[ALL_DISTINCT_EL_IMP,LENGTH_MAP] 432 ) 433 ) 434 >> `EL n (MAP SND trns_concr_list) = d` by fs[EL_MAP] 435 >> rw[] >> metis_tac[] 436 ) 437 ) 438 >- (`BIGUNION {e_sel q | ?x. q = FST x ��� x ��� s} = 439 BIGUNION {set d.sucs | MEM d 440 (MAP f s_ind)}` 441 by ( 442 `!q r i. (q,r) = EL i trns_concr_list 443 ��� i < LENGTH trns_concr_list 444 ==> ((?d n. (q,d) = EL n trns_concr_list) 445 ��� ((r,i) = 446 @(x,i). (q,x) = EL i trns_concr_list 447 ��� MEM (x,i) s_ind) 448 ��� ?n. n < LENGTH s_ind ��� (r,i) = EL n s_ind)` by ( 449 rpt strip_tac 450 >- metis_tac[] 451 >- (`(��k. (k = (r,i))) 452 ($@ (��(x,j). (q,x) = EL j trns_concr_list 453 ��� ?n. (n < LENGTH s_ind) 454 ��� (x,j) = EL n s_ind))` 455 suffices_by fs[MEM_EL] 456 >> Q.HO_MATCH_ABBREV_TAC `Q ($@ M)` 457 >> HO_MATCH_MP_TAC SELECT_ELIM_THM >> qunabbrev_tac `Q` 458 >> rpt strip_tac >> fs[] >> qunabbrev_tac `M` 459 >- (qexists_tac `(r,i)` >> fs[] 460 >> qunabbrev_tac `s_ind` >> qexists_tac `i` 461 >> simp[LENGTH_GENLIST,EL_MAP] 462 >> Cases_on `EL i trns_concr_list` >> fs[] 463 ) 464 >- (Cases_on `x` >> fs[] 465 >> `EL i (MAP FST trns_concr_list) = 466 FST (EL i trns_concr_list)` by metis_tac[EL_MAP] 467 >> `MEM (q',r') s_ind` by metis_tac[MEM_EL] 468 >> qunabbrev_tac `s_ind` >> fs[MEM_GENLIST] 469 >> `EL r' (MAP FST trns_concr_list) = 470 FST (EL r' trns_concr_list)` by metis_tac[EL_MAP] 471 >> `r' = i` suffices_by 472 (rw[] >> fs[] >> Cases_on `EL i trns_concr_list` 473 >> fs[]) 474 >> Cases_on `EL i trns_concr_list` 475 >> Cases_on `EL r' trns_concr_list` >> rw[] >> fs[] 476 >> metis_tac[ALL_DISTINCT_EL_IMP,LENGTH_MAP]) 477 ) 478 >- (qunabbrev_tac `s_ind` >> qexists_tac `i` 479 >> simp[LENGTH_GENLIST,EL_MAP] 480 >> Cases_on `EL i trns_concr_list` >> fs[] 481 ) 482 ) 483 >> qunabbrev_tac `e_sel` >> simp[MEM_MAP] >> qunabbrev_tac `s` 484 >> simp[MEM_MAP,SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac 485 >- (rename [`MEM k trns_concr_list`] >> fs[MEM_EL] 486 >> rename[`k = EL i trns_concr_list`] 487 >> Cases_on `k` >> fs[] >> rw[] 488 >> qexists_tac `set (f (r,i)).sucs` >> fs[] 489 >> first_x_assum (qspec_then `q` mp_tac) >> simp[] 490 >> strip_tac 491 >> first_x_assum (qspec_then `r` mp_tac) >> simp[] 492 >> strip_tac 493 >> first_x_assum (qspec_then `i` mp_tac) >> simp[] 494 >> strip_tac >> rpt strip_tac 495 >- metis_tac[] 496 >- (qexists_tac `f (r,i)` >> fs[] >> rpt strip_tac 497 >- metis_tac[MEM_EL] 498 >- metis_tac[MEM_EL] 499 >- (qexists_tac `(r,i)` >> fs[] 500 >> qexists_tac `n''` >> fs[] 501 ) 502 ) 503 ) 504 >- (qunabbrev_tac `s_ind` >> fs[MEM_GENLIST] 505 >> rename [���n < LENGTH trns_concr_list���, 506 ���(EL n (MAP SND trns_concr_list), n)���] 507 >> `MEM (EL n trns_concr_list) trns_concr_list` by fs[EL_MEM] 508 >> `?q r. EL n trns_concr_list = (q,r)` by ( 509 Cases_on `EL n trns_concr_list` >> fs[] 510 ) 511 >> first_x_assum (qspec_then `q` mp_tac) >> simp[] 512 >> strip_tac 513 >> first_x_assum (qspec_then `r` mp_tac) >> simp[] 514 >> strip_tac 515 >> first_x_assum (qspec_then `n` mp_tac) >> simp[] 516 >> rpt strip_tac 517 >> qexists_tac `set (f (r,n)).sucs` >> fs[] 518 >> fs[] >> rpt strip_tac >> rw[] >> fs[] 519 >- fs[EL_MAP] 520 >- (qexists_tac `q`>> fs[] >> rw[] 521 >- metis_tac[] 522 >- metis_tac[] 523 >- (qexists_tac `(q,set (MAP (concr2AbstractEdge aP)r))` 524 >> fs[] >> qexists_tac `(q,r)` >> fs[]) 525 ) 526 ) 527 ) 528 >> metis_tac[FOLDR_APPEND_LEMM,LIST_TO_SET,UNION_EMPTY] 529 ) 530 ) 531 >> `(���q d. (q,d) ��� s ��� (a_sel q,e_sel q) ��� d 532 ��� BIGINTER {a_sel q | q ��� IMAGE FST s} ��� a_sel q) 533 ��� BIGINTER {a_sel q | q ��� IMAGE FST s} ��� A` 534 suffices_by metis_tac[FINITE_LIST_TO_SET,D_CONJ_SET_LEMM3] 535 >> `!q r. (q,r) ��� s 536 ==> (?d i. (q,d) = EL i trns_concr_list 537 ��� (r = set (MAP (concr2AbstractEdge aP) d)) 538 ��� (i < LENGTH trns_concr_list) 539 ��� ((@(x,i). (q,x) = EL i trns_concr_list 540 ��� MEM (x,i) s_ind) = (d,i)))` by ( 541 rpt strip_tac >> qunabbrev_tac `s` >> fs[MEM_MAP] 542 >> Cases_on `y'` >> fs[MEM_EL] 543 >> `(r',n') = 544 (@(x,i). (q',x) = EL i trns_concr_list 545 ��� (MEM (x,i) s_ind))` by ( 546 `(��k. (k = (r',n'))) 547 ($@ (��(x,i). (q',x) = EL i trns_concr_list 548 ��� MEM (x,i) s_ind))` 549 suffices_by fs[] 550 >> Q.HO_MATCH_ABBREV_TAC `Q ($@ M)` 551 >> HO_MATCH_MP_TAC SELECT_ELIM_THM >> qunabbrev_tac `Q` 552 >> rpt strip_tac >> fs[] >> qunabbrev_tac `M` 553 >- (qexists_tac `(r',n')` >> fs[] 554 >> qunabbrev_tac `s_ind` >> simp[MEM_GENLIST,EL_MAP] 555 >> Cases_on `EL n' trns_concr_list` >> fs[]) 556 >- (Cases_on `x'` >> fs[] 557 >> `n' = r''` suffices_by ( 558 Cases_on `EL n' trns_concr_list` 559 >> Cases_on `EL r'' trns_concr_list` >> rw[] >> fs[] 560 ) >> rw[] 561 >> `EL n' (MAP FST trns_concr_list) = 562 FST (EL n' trns_concr_list)` by metis_tac[EL_MAP] 563 >> qunabbrev_tac `s_ind` >> fs[MEM_GENLIST] 564 >> `EL r'' (MAP FST trns_concr_list) = 565 FST (EL r'' trns_concr_list)` by metis_tac[EL_MAP] 566 >> Cases_on `EL n' trns_concr_list` 567 >> Cases_on `EL r'' trns_concr_list` >> rw[] >> fs[] 568 >> metis_tac[ALL_DISTINCT_EL_IMP,LENGTH_MAP] 569 ) 570 ) 571 >> qexists_tac `r'` >> qexists_tac `n'` >> fs[] 572 >> simp[MEM_EL] >> qunabbrev_tac `s_ind` >> simp[MEM_GENLIST,EL_MAP] 573 ) 574 >> rpt strip_tac 575 >- (qunabbrev_tac `a_sel` >> qunabbrev_tac `e_sel` 576 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 577 >> first_x_assum (qspec_then `d` mp_tac) >> simp[] >> strip_tac 578 >> simp[MEM_MAP] 579 >> qabbrev_tac `D = (d',i)` 580 >> qexists_tac `f D` 581 >> `(transformLabel aP (f D).pos (f D).neg, set (f D).sucs) = 582 concr2AbstractEdge aP (f D) ��� MEM (f D) d'` 583 suffices_by metis_tac[] 584 >> Cases_on `f D` >> simp[concr2AbstractEdge_def] 585 >> `MEM (d',i) s_ind` suffices_by metis_tac[] 586 >> qunabbrev_tac `s_ind` >> simp[MEM_GENLIST] 587 >> simp[EL_MAP] 588 >> Cases_on `EL i trns_concr_list` >> fs[] 589 ) 590 >- (HO_MATCH_MP_TAC IN_BIGINTER_SUBSET >> fs[] 591 >> qexists_tac `q` >> fs[] >> qexists_tac `(q,d)` >> fs[] 592 ) 593 >- (HO_MATCH_MP_TAC BIGINTER_SUBSET >> rpt strip_tac 594 >- (fs[] >> Cases_on `x'` >> rw[] 595 >> qunabbrev_tac `a_sel` >> fs[] 596 >> metis_tac[TRANSFORMLABEL_AP] 597 ) 598 >- (`?x. x ��� {a_sel q | q ��� IMAGE FST s}` 599 suffices_by metis_tac[MEMBER_NOT_EMPTY] 600 >> simp[] >> metis_tac[MEMBER_NOT_EMPTY] 601 ) 602 ) 603 ) 604 ) 605 >- ( 606 qabbrev_tac `s = set 607 (MAP (��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) 608 trns_concr_list)` 609 >> Cases_on `s = {}` 610 >- (qunabbrev_tac `s` >> rw[] >> fs[d_conj_set_def,ITSET_THM] 611 >> simp[gba_trans_concr_def,concr2AbstractEdge_def,transformLabel_def] 612 ) 613 >- ( 614 `?a e. x = (a,e)` by (Cases_on `x` >> fs[]) 615 >> `���f_a f_e. 616 ���q d. 617 ((q,d) ��� s ��� 618 (f_a q d,f_e q d) ��� d ��� a ��� f_a q d ��� f_e q d ��� e) 619 ��� ((POW aP) ��� BIGINTER {f_a q d | (q,d) ��� s} = a) 620 ��� (BIGUNION {f_e q d | (q,d) ��� s} = e)` 621 by metis_tac[D_CONJ_SET_LEMM2_STRONG,FINITE_LIST_TO_SET] 622 >> qunabbrev_tac `s` >> fs[MEM_MAP] 623 >> qabbrev_tac `c2a = concr2AbstractEdge aP` >> fs[] 624 >> `?f. !q d d_c i. 625 ((q,d) = (��(q,d). (q,set (MAP c2a d))) (q,d_c)) 626 ��� ((q,d_c) = EL i trns_concr_list 627 ��� i < LENGTH trns_concr_list) 628 ==> (MEM (f i) d_c 629 ��� (c2a (f i) = (f_a q d,f_e q d)))` by ( 630 qabbrev_tac `sel = 631 ��i. 632 if i < LENGTH trns_concr_list 633 then 634 let (q,d_c) = EL i trns_concr_list 635 in let d = 636 set (MAP (concr2AbstractEdge aP) d_c) 637 in @cE. MEM cE d_c 638 ��� concr2AbstractEdge aP cE = (f_a q d,f_e q d) 639 else ARB` 640 >> qexists_tac `sel` >> fs[] >> rpt gen_tac >> strip_tac 641 >> `sel i = 642 @cE. 643 MEM cE d_c 644 ��� concr2AbstractEdge aP cE = 645 (f_a q (set (MAP c2a d_c)), 646 f_e q (set (MAP c2a d_c)))` by ( 647 qunabbrev_tac `sel` >> fs[] >> simp[] 648 >> Cases_on `EL i trns_concr_list` >> fs[] 649 ) 650 >> fs[] 651 >> Q.HO_MATCH_ABBREV_TAC 652 `MEM ($@ P) d_c ��� c2a ($@ P) = (A,E)` 653 >> qabbrev_tac `Q = ��c. MEM c d_c ��� c2a c = (A,E)` 654 >> `Q ($@ P)` suffices_by fs[] >> HO_MATCH_MP_TAC SELECT_ELIM_THM 655 >> qunabbrev_tac `P` >> qunabbrev_tac `Q` >> fs[] 656 >> qabbrev_tac `d = set (MAP c2a d_c)` >> fs[] 657 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 658 >> first_x_assum (qspec_then `d` mp_tac) >> rpt strip_tac 659 >> `(f_a q d,f_e q d) ��� d ��� a ��� f_a q d ��� f_e q d ��� e` by ( 660 `���y. 661 (q,d) = (��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) y 662 ��� MEM y trns_concr_list` suffices_by fs[] 663 >> qexists_tac `(q,d_c)` >> rw[] >> fs[EL_MEM] 664 ) 665 >> qunabbrev_tac `d` 666 >> rw[] >> fs[MEM_MAP] >> metis_tac[] 667 ) 668 >> `!d_c i. d_c = EL i (MAP SND trns_concr_list) 669 ��� i < LENGTH (MAP SND trns_concr_list) 670 ==> MEM (f i) d_c` by ( 671 simp[MEM_MAP,EL_MAP] >> rpt strip_tac 672 >> qabbrev_tac `d_c = SND (EL i trns_concr_list)` 673 >> `?q. MEM (q,d_c) trns_concr_list 674 ��� EL i trns_concr_list = (q,d_c)` by ( 675 `MEM (EL i trns_concr_list) trns_concr_list` by fs[EL_MEM] 676 >> Cases_on `EL i trns_concr_list` >> qunabbrev_tac `d_c` 677 >> fs[] >> metis_tac[] 678 ) 679 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 680 >> first_x_assum (qspec_then `set (MAP c2a d_c)` mp_tac) 681 >> rpt strip_tac 682 >> first_x_assum (qspec_then `d_c` mp_tac) >> rw[] 683 ) 684 >> IMP_RES_TAC GBA_TRANS_LEMM2 685 >> `c2a 686 (FOLDR 687 (��sF e. 688 <|pos := sF.pos ��� e.pos; neg := sF.neg ��� e.neg; 689 sucs := sF.sucs ��� e.sucs|>) (concrEdge [] [] []) 690 (MAP f (COUNT_LIST (LENGTH (MAP SND trns_concr_list))))) = (a,e)` 691 suffices_by metis_tac[C2A_EDGE_CE_EQUIV] 692 >> rw[FOLDR_CONCR_EDGE] >> qunabbrev_tac `c2a` 693 >> simp[concr2AbstractEdge_def] 694 >> `(POW aP ��� BIGINTER 695 {f_a q d | 696 ���y. 697 (q,d) = 698 (��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) y 699 ��� MEM y trns_concr_list} = a) 700 ��� (BIGUNION 701 {f_e q d | 702 ���y. 703 (q,d) = 704 (��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) y 705 ��� MEM y trns_concr_list} = e)` by ( 706 `���q d y. 707 (q,d) = (��(q,d). (q,set (MAP (concr2AbstractEdge aP) d))) y 708 ��� MEM y trns_concr_list` suffices_by (rpt strip_tac >> fs[] >> metis_tac[]) 709 >> `?q d. MEM (q,d) trns_concr_list` by ( 710 Cases_on `trns_concr_list` >> rw[] >> Cases_on `h` >> metis_tac[]) 711 >> qexists_tac `q` >> fs[] 712 >> qexists_tac `set (MAP (concr2AbstractEdge aP) d)` >> fs[] 713 >> qexists_tac `(q,d)` >> fs[] 714 ) 715 >> strip_tac 716 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[] 717 >- (rw[] 718 >- (fs[transformLabel_def] >> metis_tac[FOLDR_INTER,SUBSET_DEF]) 719 >- (`?d_c. y = (q,d_c)` by (Cases_on `y` >> fs[]) 720 >> `?i. (q,d_c) = EL i trns_concr_list 721 ��� i < LENGTH trns_concr_list` by metis_tac[MEM_EL] 722 >> `MEM (f i) d_c 723 ��� concr2AbstractEdge aP (f i) = 724 (f_a q (set (MAP (concr2AbstractEdge aP) d_c)), 725 f_e q (set (MAP (concr2AbstractEdge aP) d_c)))` 726 by metis_tac[] 727 >> `(MEM_SUBSET (f i).pos 728 (FOLDR (��e pr. e.pos ��� pr) 729 [] (MAP f (COUNT_LIST 730 (LENGTH (MAP SND trns_concr_list)))))) 731 ��� (MEM_SUBSET (f i).neg 732 (FOLDR (��e pr. e.neg ��� pr) 733 [] (MAP f (COUNT_LIST 734 (LENGTH (MAP SND trns_concr_list))))))` 735 suffices_by ( 736 Cases_on `f i` >> fs[concr2AbstractEdge_def] 737 >> Cases_on `EL i trns_concr_list` >> fs[] >> rw[] 738 >> metis_tac[TRANSFORMLABEL_SUBSET,SUBSET_DEF] 739 ) 740 >> `MEM (f i) (MAP f (COUNT_LIST (LENGTH trns_concr_list)))` 741 suffices_by (simp[] >> metis_tac[FOLDR_APPEND_LEMM]) 742 >> simp[MEM_MAP] >> qexists_tac `i` >> fs[] 743 >> metis_tac[MEM_COUNT_LIST] 744 ) 745 ) 746 >- (rw[] >> fs[IN_INTER,IN_BIGINTER] 747 >> HO_MATCH_MP_TAC TRANSFORMLABEL_FOLDR >> rpt strip_tac 748 >- (POP_ASSUM mp_tac >> simp[MEM_MAP] >> rpt strip_tac 749 >> `y < LENGTH trns_concr_list` by fs[MEM_COUNT_LIST] 750 >> `MEM (f y) (EL y (MAP SND trns_concr_list))` by metis_tac[] 751 >> qabbrev_tac `d_c = EL y (MAP SND trns_concr_list)` 752 >> `?q. (q,d_c) = EL y trns_concr_list` by ( 753 `MEM (EL y trns_concr_list) trns_concr_list` by fs[EL_MEM] 754 >> qunabbrev_tac `d_c` >> fs[] 755 >> Cases_on `EL y trns_concr_list` >> rw[] >> simp[EL_MAP] 756 ) 757 >> rw[] 758 >> qabbrev_tac `d = set (MAP (concr2AbstractEdge aP) d_c)` 759 >> first_x_assum (qspec_then `f_a q d` mp_tac) 760 >> simp[] >> rpt strip_tac 761 >> `x ��� f_a q d` by ( 762 `(���q' d'. 763 f_a q d = f_a q' d' 764 ��� ���y. 765 (q',d') = (��(q,d). 766 (q,set (MAP (concr2AbstractEdge aP) d))) y 767 ��� MEM y trns_concr_list)` suffices_by metis_tac[] 768 >> qexists_tac `q` >> qexists_tac `d` >> fs[] 769 >> qexists_tac `(q,d_c)` >> fs[EL_MEM] 770 ) 771 >> first_x_assum (qspec_then `q` mp_tac) >> rpt strip_tac 772 >> first_x_assum (qspec_then `d_c` mp_tac) >> simp[] 773 >> rpt strip_tac >> first_x_assum (qspec_then `y` mp_tac) 774 >> simp[] 775 >> Cases_on `f y` >> fs[concr2AbstractEdge_def] 776 ) 777 >- fs[] 778 ) 779 ) 780 >- (rw[] >> Q.HO_MATCH_ABBREV_TAC `S1 = BIGUNION S2` 781 >> `S2 = {set x.sucs | 782 MEM x (MAP f (COUNT_LIST (LENGTH trns_concr_list))) }` 783 suffices_by ( 784 qunabbrev_tac `S1` >> qunabbrev_tac `S2` >> fs[] >> rw[] 785 >> metis_tac[LIST_TO_SET,FOLDR_APPEND_LEMM,UNION_EMPTY] 786 ) 787 >> qunabbrev_tac `S2` >> fs[] >> simp[SET_EQ_SUBSET,SUBSET_DEF] 788 >> rpt strip_tac 789 >- (`?d_c. y = (q,d_c)` by (Cases_on `y` >> fs[]) 790 >> `?i. i < LENGTH trns_concr_list 791 ��� EL i trns_concr_list = (q,d_c)` by metis_tac[MEM_EL] 792 >> `concr2AbstractEdge aP (f i) = 793 (f_a q (set (MAP (concr2AbstractEdge aP) d_c)), 794 f_e q (set (MAP (concr2AbstractEdge aP) d_c)))` 795 by metis_tac[] 796 >> Cases_on `f i` >> fs[concr2AbstractEdge_def] 797 >> qexists_tac `f i` >> rw[] >> simp[MEM_MAP] 798 >> qexists_tac `i` >> fs[] >> metis_tac[MEM_COUNT_LIST] 799 ) 800 >- (fs[MEM_MAP] 801 >> `?j. j = EL y trns_concr_list` by metis_tac[MEM_EL,MEM_COUNT_LIST] 802 >> `?q d_c. j = (q,d_c)` by (Cases_on `j` >> fs[]) 803 >> `y < LENGTH (trns_concr_list)` by fs[MEM_COUNT_LIST] 804 >> `concr2AbstractEdge aP (f y) = 805 (f_a q (set (MAP (concr2AbstractEdge aP) d_c)), 806 f_e q (set (MAP (concr2AbstractEdge aP) d_c)))` 807 by metis_tac[] 808 >> qabbrev_tac `d = set (MAP (concr2AbstractEdge aP) d_c)` 809 >> qexists_tac `q` >> qexists_tac `d` >> fs[] 810 >> Cases_on `f y` >> fs[concr2AbstractEdge_def] 811 >> rw[] >> qexists_tac `(q,d_c)` >> fs[EL_MEM] 812 ) 813 ) 814 ) 815 ) 816 ); 817 818val trns_is_empty_def = Define` 819 trns_is_empty cE = EXISTS (��p. MEM p cE.neg) cE.pos`; 820 821val TRNS_IS_EMPTY_LEMM = store_thm 822 ("TRNS_IS_EMPTY_LEMM", 823 ``!cE ap. ((set cE.pos ��� ap) ��� (set cE.neg ��� ap)) 824 ==> trns_is_empty cE = (transformLabel ap cE.pos cE.neg = {})``, 825 rpt strip_tac >> fs[trns_is_empty_def] 826 >> `(EXISTS (��p. MEM p cE.neg) cE.pos) = ~(set cE.neg ��� set cE.pos = {})` 827 by ( 828 simp[EQ_IMP_THM] >> rpt strip_tac >> fs[EXISTS_MEM] 829 >- (`p ��� set cE.neg ��� set cE.pos` by simp[IN_INTER] 830 >> metis_tac[MEMBER_NOT_EMPTY] 831 ) 832 >- (`?p. p ��� set cE.neg ��� set cE.pos` by metis_tac[MEMBER_NOT_EMPTY] 833 >> metis_tac[IN_INTER] 834 ) 835 ) 836 >> metis_tac[TRANSFORMLABEL_EMPTY,INTER_COMM] 837 ); 838 839val TRANSFORMLABEL_LEMM = store_thm 840 ("TRANSFORMLABEL_LEMM", 841 ``!ce1 ce2 aP. (((~trns_is_empty ce1 ��� ~trns_is_empty ce2) 842 ��� ~(MEM_EQUAL ce1.pos ce2.pos ��� MEM_EQUAL ce1.neg ce2.neg) 843 ��� !x. ((MEM x ce1.pos \/ MEM x ce1.neg \/ MEM x ce2.pos 844 \/ MEM x ce2.neg) ==> MEM x aP)) 845 ==> ~(transformLabel (set aP) ce1.pos ce1.neg = 846 transformLabel (set aP) ce2.pos ce2.neg))``, 847 rpt gen_tac >> strip_tac 848 >> `(set ce1.pos ��� set aP) ��� (set ce2.pos ��� set aP) 849 ��� (set ce1.neg ��� set aP) ��� (set ce2.neg ��� set aP)` by fs[SUBSET_DEF] 850 >> `~(transformLabel (set aP) ce1.pos ce1.neg = {})` by metis_tac[TRNS_IS_EMPTY_LEMM] 851 >> `~(transformLabel (set aP) ce2.pos ce2.neg = {})` by metis_tac[TRNS_IS_EMPTY_LEMM] 852 >> simp[SET_EQ_SUBSET] 853 >> `!l1 l2. ~(set l1 ��� set l2) ==> ~MEM_SUBSET l1 l2` 854 by fs[MEM_SUBSET_SET_TO_LIST] 855 >> fs[MEM_EQUAL_SET] 856 >> IMP_RES_TAC TRANSFORMLABEL_SUBSET2 857 >> metis_tac[SET_EQ_SUBSET,MEM_SUBSET_SET_TO_LIST] 858 ); 859 860val tlg_concr_def = Define` 861 tlg_concr (t1,acc_t1) (t2,acc_t2) = 862 (((MEM_SUBSET t1.pos t2.pos) 863 ��� (MEM_SUBSET t1.neg t2.neg) \/ trns_is_empty t2) 864 ��� (MEM_SUBSET t1.sucs t2.sucs) 865 ��� (MEM_SUBSET acc_t2 acc_t1))`; 866 867val acc_cond_concr_def = Define` 868 acc_cond_concr cE f f_trans = 869 (~(MEM f cE.sucs) 870 \/ (if trns_is_empty cE 871 then (EXISTS (��cE1. 872 MEM_SUBSET cE1.sucs cE.sucs 873 ��� ~(MEM f cE1.sucs)) f_trans) 874 else (EXISTS (��cE1. 875 MEM_SUBSET cE1.pos cE.pos 876 ��� MEM_SUBSET cE1.neg cE.neg 877 ��� MEM_SUBSET cE1.sucs cE.sucs 878 ��� ~(MEM f cE1.sucs)) f_trans)))`; 879 880val concr_extrTrans_def = Define` 881 concr_extrTrans g_AA aa_id = 882 case lookup aa_id g_AA.followers of 883 | NONE => NONE 884 | SOME aa_edges => 885 let aa_edges_with_frmls = 886 CAT_OPTIONS 887 (MAP 888 (��(eL,id). 889 case lookup id g_AA.nodeInfo of 890 | NONE => NONE 891 | SOME n => SOME (eL,n.frml)) 892 aa_edges 893 ) 894 in let aa_edges_grpd = 895 GROUP_BY 896 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp) 897 aa_edges_with_frmls 898 in let concr_edges:(�� concrEdge) list = 899 CAT_OPTIONS 900 (MAP 901 (��grp. case grp of 902 | [] => NONE 903 | ((eL,f)::xs) => 904 SOME 905 (concrEdge eL.pos_lab eL.neg_lab (nub (f::MAP SND xs))) 906 ) aa_edges_grpd) 907 in do node <- lookup aa_id g_AA.nodeInfo ; 908 true_edges <- 909 SOME (MAP 910 (��eL. (concrEdge eL.pos_lab eL.neg_lab [])) 911 node.true_labels) ; 912 SOME (concr_edges ++ true_edges) 913 od`; 914 915val CONCR_EXTRTRANS_NODES = store_thm 916 ("CONCR_EXTRTRANS_NODES", 917 ``!g_AA x l. 918 (concr_extrTrans g_AA x = SOME l) 919 ==> (!ce q. MEM ce l ��� MEM q ce.sucs 920 ==> (MEM q (graphStates g_AA) 921 ��� ALL_DISTINCT ce.sucs))``, 922 rpt strip_tac >> fs[concr_extrTrans_def] 923 >> Cases_on `lookup x g_AA.followers` >> fs[] 924 >> rw[] >> fs[MEM_APPEND,CAT_OPTIONS_MEM,MEM_MAP] 925 >- (Cases_on `grp` >> fs[] >> Cases_on `h` >> fs[] 926 >> fs[concrEdge_component_equality] 927 >> qabbrev_tac `L = 928 CAT_OPTIONS 929 (MAP 930 (��(eL,id). 931 case lookup id g_AA.nodeInfo of 932 NONE => NONE 933 | SOME n => SOME (eL,n.frml)) x')` 934 >> `MEM q (MAP SND (FLAT (GROUP_BY 935 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp) 936 L)))` by ( 937 simp[MEM_MAP,MEM_FLAT] 938 >> `q = r \/ MEM q (MAP SND t)` by metis_tac[MEM,nub_set] 939 >- (qexists_tac `(q',r)` >> fs[] 940 >> qexists_tac `(q',r)::t` >> fs[] 941 ) 942 >- (fs[MEM_MAP] >> qexists_tac `y` >> fs[] 943 >> qexists_tac `(q',r)::t` >> fs[] 944 ) 945 ) 946 >> `MEM q (MAP SND L)` by metis_tac[GROUP_BY_FLAT] 947 >> qunabbrev_tac `L` >> fs[MEM_MAP,CAT_OPTIONS_MEM] 948 >> rename[`MEM y2 trns`, `SOME y1 = _ y2`] 949 >> Cases_on `y2` >> fs[] >> rename[`MEM (eL,id) trns`] 950 >> Cases_on `lookup id g_AA.nodeInfo` >> fs[] 951 >> rename[`lookup id g_AA.nodeInfo = SOME node`] 952 >> simp[graphStates_def,MEM_MAP] >> qexists_tac `(id,node)` 953 >> fs[] >> metis_tac[MEM_toAList] 954 ) 955 >- (fs[concrEdge_component_equality] >> metis_tac[MEM]) 956 >- (Cases_on `grp` >> fs[] >> Cases_on `h` >> fs[] 957 >> fs[all_distinct_nub] 958 ) 959 ); 960 961val CONCR_EXTRTRANS_LEMM = store_thm 962 ("CONCR_EXTRTRANS_LEMM", 963 ``!g_AA id aP. 964 wfg g_AA ��� flws_sorted g_AA ��� unique_node_formula g_AA 965 ==> case lookup id g_AA.followers of 966 | NONE => T 967 | SOME aa_edges => 968 ?n cT. (concr_extrTrans g_AA id = SOME cT) 969 ��� (lookup id g_AA.nodeInfo = SOME n) 970 ��� (set (MAP (concr2AbstractEdge aP) cT) = 971 concrTrans g_AA aP n.frml)``, 972 rpt strip_tac >> fs[] >> Cases_on `lookup id g_AA.followers` >> fs[] 973 >> `?n.lookup id g_AA.nodeInfo = SOME n` by ( 974 fs[wfg_def] >> metis_tac[domain_lookup] 975 ) 976 >> qexists_tac `n` >> fs[] 977 >> `?cT. concr_extrTrans g_AA id = SOME cT` by ( 978 simp[concr_extrTrans_def] 979 ) 980 >> qexists_tac `cT` >> fs[] >> simp[SET_EQ_SUBSET,SUBSET_DEF] 981 >> qabbrev_tac `E = 982 (��((eL1:�� edgeLabelAA),(f1:�� ltl_frml)) 983 ((eL2:�� edgeLabelAA),(f2:�� ltl_frml)). 984 eL1.edge_grp = eL2.edge_grp)` 985 >> qabbrev_tac `P = 986 (��(f1:�� edgeLabelAA # num) 987 (f2:�� edgeLabelAA # num). 988 (FST f2).edge_grp ��� (FST f1).edge_grp)` 989 >> qabbrev_tac `P_c = 990 (��(f1:�� edgeLabelAA # �� ltl_frml) 991 (f2:�� edgeLabelAA # �� ltl_frml). 992 (FST f2).edge_grp ��� (FST f1).edge_grp)` 993 >> `rel_corr E P_c` by ( 994 simp[rel_corr_def] >> qunabbrev_tac `E` 995 >> qunabbrev_tac `P_c` 996 >> simp[EQ_IMP_THM] >> rpt strip_tac 997 >> Cases_on `x'` >> Cases_on `y` >> fs[] 998 ) 999 >> `!l1 l2. (MAP FST l1 = MAP FST l2) 1000 ==> (SORTED P l1 ==> SORTED P_c l2)` by ( 1001 Induct_on `l2` >> fs[] >> rpt strip_tac 1002 >> `transitive P_c` 1003 by (qunabbrev_tac `P_c` >> simp[transitive_def]) 1004 >> simp[SORTED_EQ] >> Cases_on `l1` >> fs[] 1005 >> rename[`SORTED P (h1::t1)`] 1006 >> `SORTED P t1` by metis_tac[SORTED_TL] 1007 >> `SORTED P_c l2` by metis_tac[] >> fs[] 1008 >> rpt strip_tac >> Cases_on `y` 1009 >> `MEM q (MAP FST t1)` by ( 1010 `MEM q (MAP FST l2)` suffices_by metis_tac[] 1011 >> simp[MEM_MAP] >> qexists_tac `(q,r)` >> fs[] 1012 ) 1013 >> fs[MEM_MAP] 1014 >> `transitive P` by (qunabbrev_tac `P` >> simp[transitive_def]) 1015 >> `P h1 y` by metis_tac[SORTED_EQ] 1016 >> qunabbrev_tac `P_c` >> Cases_on `y` >> fs[] 1017 >> Cases_on `h1` >> Cases_on `h` >> fs[] >> rw[] 1018 >> qunabbrev_tac `P` >> fs[] 1019 ) 1020 >> qabbrev_tac `J = 1021 ��(l:((�� edgeLabelAA # num) list)). CAT_OPTIONS 1022 (MAP 1023 (��(eL,id). 1024 case lookup id g_AA.nodeInfo of 1025 NONE => NONE 1026 | SOME n => SOME (eL,n.frml)) l)` 1027 >> `!k. EVERY 1028 (��x. IS_SOME (lookup (SND x) g_AA.nodeInfo)) k 1029 ==> (MAP FST k = MAP FST (J k))` by ( 1030 Induct_on `k` 1031 >- (qunabbrev_tac `J` >> fs[CAT_OPTIONS_def]) 1032 >- (rpt strip_tac 1033 >> `MAP FST k = MAP FST (J k)` 1034 by metis_tac[EVERY_DEF] 1035 >> `(FST h)::(MAP FST (J k)) = MAP FST (J (h::k))` 1036 suffices_by metis_tac[MAP] 1037 >> Cases_on `J (h::k)` >> fs[] 1038 >- (`?n. lookup (SND h) g_AA.nodeInfo = SOME n` 1039 by metis_tac[IS_SOME_EXISTS] 1040 >> `MEM (FST h, n'.frml) (J (h::k))` by ( 1041 qunabbrev_tac `J` >> simp[CAT_OPTIONS_MEM] 1042 >> fs[CAT_OPTIONS_MAP_LEMM] 1043 >> Cases_on `h` >> fs[CAT_OPTIONS_def] 1044 ) 1045 >> fs[] >> rw[] >> metis_tac[MEM] 1046 ) 1047 >- (qunabbrev_tac `J` >> fs[] 1048 >> Cases_on `h` >> fs[CAT_OPTIONS_def] 1049 >> fs[IS_SOME_EXISTS] 1050 >> Cases_on `lookup r g_AA.nodeInfo` >> fs[] 1051 >> fs[CAT_OPTIONS_def] >> rw[] 1052 ) 1053 ) 1054 ) 1055 >> `EVERY (��x. IS_SOME (lookup (SND x) g_AA.nodeInfo)) x` by ( 1056 simp[EVERY_MEM] >> rpt strip_tac 1057 >> rename[`MEM fl fls`] >> Cases_on `fl` 1058 >> rename[`MEM (eL_f,fl_id) fls`] >> fs[wfg_def] 1059 >> fs[wfAdjacency_def] 1060 >> `fl_id ��� domain g_AA.followers` by metis_tac[] 1061 >> metis_tac[IS_SOME_DEF,domain_lookup] 1062 ) 1063 >> `MAP FST x = MAP FST (J x)` by metis_tac[] 1064 >> `transitive P_c` by ( 1065 qunabbrev_tac `P_c` >> simp[transitive_def] 1066 ) 1067 >> `equivalence E` by ( 1068 qunabbrev_tac `E` >> simp[equivalence_def] 1069 >> simp[reflexive_def,symmetric_def,transitive_def] 1070 >> rpt strip_tac 1071 >- (Cases_on `x'` >> fs[]) 1072 >- (Cases_on `x'` >> Cases_on `y` >> fs[]) 1073 >- (Cases_on `x'` >> Cases_on `y` >> Cases_on `z` >> fs[]) 1074 ) 1075 >> rpt strip_tac >> fs[concrTrans_def,extractTrans_def,concr_extrTrans_def] 1076 >> rw[] 1077 >- (Cases_on `lookup id g_AA.followers` >> fs[] 1078 >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM] >> rw[] 1079 >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1080 >- (Cases_on `grp` >> fs[] >> disj1_tac 1081 >> `?eL frml. h = (eL,frml)` by (Cases_on `h` >> fs[]) 1082 >> qexists_tac `(eL.edge_grp, 1083 eL.pos_lab, 1084 eL.neg_lab, 1085 set (frml::(MAP SND t)))` 1086 >> fs[flws_sorted_def] >> first_x_assum (qspec_then `id` mp_tac) 1087 >> `id ��� domain g_AA.nodeInfo` 1088 by (fs[wfg_def] >> metis_tac[domain_lookup]) 1089 >> simp[] >> rpt strip_tac 1090 >- simp[concr2AbstractEdge_def] 1091 >- (qexists_tac `eL` >> simp[] 1092 >> Q.HO_MATCH_ABBREV_TAC ` 1093 (0 < eL.edge_grp) 1094 ��� ~(A = {}) 1095 ��� (frml INSERT set (MAP SND t) 1096 = A)` 1097 >> `0 < eL.edge_grp ��� (frml INSERT set (MAP SND t) = A)` 1098 suffices_by ( 1099 simp[] >> rpt strip_tac >> `frml ��� A` by fs[] 1100 >> metis_tac[MEMBER_NOT_EMPTY] 1101 ) >> rpt strip_tac 1102 >- (`MEM (eL,frml) (FLAT (GROUP_BY E (J x)))` by ( 1103 simp[MEM_FLAT] >> qexists_tac `(eL,frml)::t` >> fs[] 1104 ) 1105 >> `MEM (eL,frml) (J x)` by metis_tac[GROUP_BY_FLAT] 1106 >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1107 >> rename[`MEM edge x`] >> Cases_on `edge` 1108 >> fs[] >> Cases_on `lookup r g_AA.nodeInfo` >> fs[] 1109 >> rw[] >> `0 < (FST (eL,r)).edge_grp` by metis_tac[] 1110 >> fs[] 1111 ) 1112 >- (qabbrev_tac `c_edge_list = (eL,frml)::t` 1113 >> `set (MAP SND c_edge_list) = A` suffices_by ( 1114 qunabbrev_tac `c_edge_list` >> fs[] 1115 ) 1116 >> qunabbrev_tac `A` >> simp[SET_EQ_SUBSET,SUBSET_DEF] 1117 >> qabbrev_tac `L = 1118 CAT_OPTIONS 1119 (MAP 1120 (��(eL,id). 1121 case lookup id g_AA.nodeInfo of 1122 NONE => NONE 1123 | SOME n => SOME (eL,n.frml)) x)` 1124 >> `L = J x` by (qunabbrev_tac `J` >> qunabbrev_tac `L` >> fs[]) 1125 >> `!e f. MEM (e,f) c_edge_list ==> 1126 (MEM (e,f) L 1127 ��� ?id node. MEM (e,id) x 1128 ��� (lookup id g_AA.nodeInfo = SOME node) 1129 ��� (node.frml = f))` by ( 1130 rpt gen_tac >> strip_tac 1131 >> `MEM (e,f) 1132 (FLAT (GROUP_BY 1133 (��(eL1,f1) (eL2,f2). 1134 eL1.edge_grp = eL2.edge_grp) L))` by ( 1135 simp[MEM_FLAT] >> qexists_tac `c_edge_list` >> fs[] 1136 ) 1137 >> `!R. FLAT (GROUP_BY R L) = L` 1138 by metis_tac[GROUP_BY_FLAT] 1139 >> `MEM (e,f) L` by metis_tac[] 1140 >> qunabbrev_tac `L` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1141 >> rename[`MEM y2 x`] 1142 >> `?y_id. y2 = (e,y_id)` by ( 1143 Cases_on `y2` >> Cases_on `lookup r g_AA.nodeInfo` 1144 >> fs[] 1145 ) >> fs[] >> strip_tac 1146 >- (qexists_tac `(e,y_id)` >> simp[]) 1147 >- (qexists_tac `y_id` >> rw[] >> fs[] 1148 >> `?node. lookup y_id g_AA.nodeInfo = SOME node` 1149 by (Cases_on `lookup y_id g_AA.nodeInfo` >> fs[]) 1150 >> qexists_tac `node` >> fs[] 1151 ) 1152 ) 1153 >> `���l_sub. 1154 MEM l_sub (GROUP_BY E L) ��� 1155 (���x y. MEM x l_sub ��� MEM y l_sub ��� E x y) ��� 1156 ���x y. MEM x l_sub ��� MEM y L ��� E x y ��� MEM y l_sub` by ( 1157 HO_MATCH_MP_TAC SORTED_GROUP_BY 1158 >> qexists_tac `P_c` >> fs[] >> metis_tac[] 1159 ) 1160 >> rpt strip_tac 1161 >- (rename[`MEM frml1 (MAP SND c_edge_list)`] 1162 >> `?eL1. MEM (eL1,frml1) c_edge_list` by ( 1163 fs[MEM_MAP] >> rename[`MEM y1 c_edge_list`] 1164 >> qexists_tac `FST y1` >> fs[] 1165 ) 1166 >> `MEM (eL,frml) L ��� 1167 ���id node. 1168 MEM (eL,id) x ��� lookup id g_AA.nodeInfo = SOME node 1169 ��� node.frml = frml` by ( 1170 `MEM (eL,frml) c_edge_list` suffices_by metis_tac[] 1171 >> qunabbrev_tac `c_edge_list` >> fs[] 1172 ) 1173 >> `MEM (eL1,frml1) L ��� 1174 ���id1 node1. 1175 MEM (eL1,id1) x ��� lookup id1 g_AA.nodeInfo = SOME node1 1176 ��� node1.frml = frml1` by metis_tac[] 1177 >> fs[] >> rw[] 1178 >> first_x_assum (qspec_then `c_edge_list` mp_tac) >> simp[] 1179 >> rpt strip_tac >> rw[] 1180 >> `eL1 = eL` by ( 1181 `eL1.edge_grp = eL.edge_grp` by ( 1182 `MEM (eL,node.frml) c_edge_list` by ( 1183 qunabbrev_tac `c_edge_list` >> fs[] 1184 ) 1185 >> `E (eL,node.frml) (eL1,node1.frml)` by metis_tac[] 1186 >> qunabbrev_tac `E` >> fs[] 1187 ) 1188 >> `(FST (eL,id')).edge_grp = 1189 (FST (eL1,id1)).edge_grp` by fs[] 1190 >> `FST (eL,id') = FST (eL1,id1)` by metis_tac[] 1191 >> fs[] 1192 ) 1193 >> rw[] 1194 >> qexists_tac `node1` >> fs[] >> qexists_tac `id1` 1195 >> simp[OPTION_TO_LIST_MEM] >> qexists_tac `x` >> fs[] 1196 >> qexists_tac `(id,n)` >> fs[] 1197 >> metis_tac[UNIQUE_NODE_FIND_LEMM] 1198 ) 1199 >- (simp[MEM_MAP] >> fs[OPTION_TO_LIST_MEM] 1200 >> rename[`findNode _ g_AA = SOME x2`] 1201 >> `x2 = (id,n)` by metis_tac[UNIQUE_NODE_FIND_LEMM,SOME_11] 1202 >> rw[] >> fs[] >> rw[] >> qexists_tac `(eL,suc.frml)` 1203 >> fs[] 1204 >> `MEM (eL,suc.frml) (J l)` by ( 1205 qunabbrev_tac `J` >> simp[CAT_OPTIONS_MEM,MEM_MAP] 1206 >> qexists_tac `(eL,sucId)` >> fs[] 1207 >> Cases_on `lookup sucId g_AA.nodeInfo` >> fs[] 1208 ) 1209 >> `MEM c_edge_list (GROUP_BY E (J l))` by fs[] 1210 >> `MEM (eL,suc.frml) (FLAT (GROUP_BY E (J l)))` by ( 1211 metis_tac[GROUP_BY_FLAT] 1212 ) 1213 >> fs[MEM_FLAT] >> rename[`MEM c_e_list2 (GROUP_BY E (J l))`] 1214 >> first_x_assum (qspec_then `c_edge_list` mp_tac) >> simp[] 1215 >> rpt strip_tac 1216 >> first_x_assum (qspec_then `(eL,frml)` mp_tac) 1217 >> `MEM (eL,frml) c_edge_list` by 1218 (qunabbrev_tac `c_edge_list` >> fs[]) 1219 >> simp[] >> rpt strip_tac 1220 >> `E (eL,frml) (eL,suc.frml)` suffices_by metis_tac[] 1221 >> qunabbrev_tac `E` >> simp[] 1222 ) 1223 ) 1224 ) 1225 ) 1226 >- (disj2_tac >> qexists_tac `(0,eL.pos_lab,eL.neg_lab,{})` 1227 >> simp[concr2AbstractEdge_def] >> qexists_tac `eL` 1228 >> simp[OPTION_TO_LIST_MEM] >> qexists_tac `n.true_labels` 1229 >> simp[] >> qexists_tac `(id,n)` >> fs[] 1230 >> metis_tac[UNIQUE_NODE_FIND_LEMM] 1231 ) 1232 ) 1233 >- (Cases_on `lookup id g_AA.followers` >> fs[] 1234 >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM] >> rw[] 1235 >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1236 >> Q.HO_MATCH_ABBREV_TAC ` 1237 ?y. (transformLabel aP label.pos_lab label.neg_lab, 1238 SUCS) = concr2AbstractEdge aP y 1239 ��� ((?grp. 1240 SOME y = CE grp 1241 ��� MEM grp CONCR_TRNS) \/ A y)` 1242 >> `?grp cE. (SOME cE = CE grp) ��� (MEM grp CONCR_TRNS) 1243 ��� (set cE.sucs = SUCS) 1244 ��� ((cE.pos = label.pos_lab) ��� (cE.neg = label.neg_lab))` by ( 1245 `?f. f ��� SUCS` by metis_tac[MEMBER_NOT_EMPTY] 1246 >> qunabbrev_tac `SUCS` >> fs[OPTION_TO_LIST_MEM] 1247 >> rename[`findNode _ g_AA = SOME node`] 1248 >> `node = (id,n)` by metis_tac[SOME_11,UNIQUE_NODE_FIND_LEMM] 1249 >> rw[] >> fs[] >> rw[] 1250 >> rename[`lookup id g_AA.followers = SOME fls`] 1251 >> `FLAT CONCR_TRNS = J fls` by ( 1252 qunabbrev_tac `CONCR_TRNS` >> fs[] >> metis_tac[GROUP_BY_FLAT] 1253 ) 1254 >> `MEM (label,suc.frml) (J fls)` by ( 1255 qunabbrev_tac `J` >> simp[CAT_OPTIONS_MEM,MEM_MAP] 1256 >> qexists_tac `(label,sucId)` >> simp[] 1257 >> Cases_on `lookup sucId g_AA.nodeInfo` >> fs[] 1258 ) 1259 >> `?grp. MEM grp CONCR_TRNS ��� MEM (label,suc.frml) grp` 1260 by metis_tac[MEM_FLAT] 1261 >> qexists_tac `grp` 1262 >> `?cE. CE grp = SOME cE` by ( 1263 qunabbrev_tac `CE` >> simp[] >> Cases_on `grp` >> fs[] 1264 >> Cases_on `h` >> fs[] 1265 ) 1266 >> qexists_tac `cE` >> simp[SET_EQ_SUBSET,SUBSET_DEF] 1267 >> strip_tac 1268 >- (rpt strip_tac 1269 >- (`!lab f. MEM (lab,f) grp ==> (lab = label)` by ( 1270 rpt strip_tac 1271 >> `SORTED P fls 1272 ��� ���x y. 1273 (MEM x fls ��� MEM y fls ��� (FST x).edge_grp = (FST y).edge_grp) 1274 ��� (FST x = FST y)` by ( 1275 fs[flws_sorted_def] >> metis_tac[domain_lookup] 1276 ) 1277 >> `���l_sub. 1278 MEM l_sub (GROUP_BY E (J fls)) ��� 1279 (���x y. MEM x l_sub ��� MEM y l_sub ��� E x y) ��� 1280 ���x y. MEM x l_sub ��� MEM y (J fls) ��� E x y 1281 ��� MEM y l_sub` by ( 1282 HO_MATCH_MP_TAC SORTED_GROUP_BY 1283 >> qexists_tac `P_c` >> fs[] >> metis_tac[] 1284 ) 1285 >> first_x_assum (qspec_then `grp` mp_tac) >> simp[] 1286 >> rpt strip_tac 1287 >> `MEM (lab,f) (J fls)` by ( 1288 `MEM (lab,f) (FLAT CONCR_TRNS)` by ( 1289 fs[MEM_FLAT] >> qexists_tac `grp` >> simp[] 1290 ) 1291 >> metis_tac[] 1292 ) 1293 >> `E (label,suc.frml) (lab,f)` by metis_tac[] 1294 >> first_x_assum (qspec_then `(label,sucId)` mp_tac) 1295 >> simp[] >> rpt strip_tac 1296 >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1297 >> rename[`MEM y2 fls`,`SOME (lab,x) = _ y2`] 1298 >> Cases_on `y2` >> fs[] 1299 >> first_x_assum (qspec_then `(lab,r)` mp_tac) 1300 >> Cases_on `lookup r g_AA.nodeInfo` >> fs[] 1301 >> rw[] >> qunabbrev_tac `E` >> fs[] 1302 ) 1303 >> qunabbrev_tac `CE` >> Cases_on `grp` >> fs[] >> Cases_on `h` 1304 >> fs[concrEdge_component_equality] >> rw[] 1305 >- (Cases_on `x = suc.frml` 1306 >- (qexists_tac `suc` >> simp[] >> qexists_tac `sucId` 1307 >> simp[] 1308 ) 1309 >- (`MEM x (MAP SND t)` by metis_tac[MEM,nub_set] 1310 >> fs[MEM_MAP] >> rename[`MEM edge t`] 1311 >> `edge = (label,x)` 1312 by (Cases_on `edge` >> fs[] >> metis_tac[]) 1313 >> rw[] 1314 >> `MEM (label,x) (J fls)` by ( 1315 `MEM (label,x) (FLAT CONCR_TRNS)` by ( 1316 simp[MEM_FLAT] 1317 >> qexists_tac `(label,suc.frml)::t` >> simp[] 1318 ) 1319 >> metis_tac[] 1320 ) 1321 >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1322 >> rename[`MEM edge fls`] >> Cases_on `edge` 1323 >> rename[`MEM (e_f,e_id) fls`] 1324 >> Cases_on `lookup e_id g_AA.nodeInfo` >> fs[] 1325 >> rename[`lookup _ _ = SOME node`] 1326 >> qexists_tac `node` >> fs[] >> qexists_tac `e_id` 1327 >> fs[] 1328 ) 1329 ) 1330 >- (Cases_on `x = suc.frml` 1331 >- (qexists_tac `suc` >> simp[] >> qexists_tac `sucId` 1332 >> simp[] 1333 ) 1334 >- (`MEM x (r::MAP SND t)` by metis_tac[nub_set] 1335 >> `MEM x (MAP SND ((label,r)::t))` by fs[MEM] 1336 >- (`MEM (label,x) (J fls)` by ( 1337 `MEM (label,x) (FLAT CONCR_TRNS)` by ( 1338 simp[MEM_FLAT] 1339 >> qexists_tac `(label,r)::t` >> simp[] 1340 >> fs[MEM_MAP] >> Cases_on `y` >> fs[] 1341 >> rw[] >> metis_tac[] 1342 ) 1343 >> metis_tac[] 1344 ) 1345 >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1346 >> rename[`MEM edge fls`] >> Cases_on `edge` 1347 >> rename[`MEM (e_f,e_id) fls`] 1348 >> Cases_on `lookup e_id g_AA.nodeInfo` >> fs[] 1349 >> rename[`lookup _ _ = SOME node`] 1350 >> qexists_tac `node` >> fs[] >> qexists_tac `e_id` 1351 >> fs[]) 1352 (* >- ( *) 1353 (* rename[`MEM edge t`] *) 1354 (* >> `edge = (label,x)` *) 1355 (* by (Cases_on `edge` >> fs[] >> metis_tac[]) *) 1356 (* >> rw[] *) 1357 (* >> `MEM (label,x) (J fls)` by ( *) 1358 (* `MEM (label,x) (FLAT CONCR_TRNS)` by ( *) 1359 (* simp[MEM_FLAT] *) 1360 (* >> qexists_tac `(label,r)::t` >> simp[] *) 1361 (* >> rw[] >> fs[] >> metis_tac[] *) 1362 (* ) *) 1363 (* >> metis_tac[] *) 1364 (* ) *) 1365 (* >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] *) 1366 (* >> rename[`MEM edge fls`] >> Cases_on `edge` *) 1367 (* >> rename[`MEM (e_f,e_id) fls`] *) 1368 (* >> Cases_on `lookup e_id g_AA.nodeInfo` >> fs[] *) 1369 (* >> rename[`lookup _ _ = SOME node`] *) 1370 (* >> qexists_tac `node` >> fs[] >> qexists_tac `e_id` *) 1371 (* >> fs[] *) 1372 (* ) *) 1373 ) 1374 ) 1375 ) 1376 >- (rename[`MEM (label,sucId1) fls`, 1377 `SOME suc1 = lookup sucId1 g_AA.nodeInfo`] 1378 >> `MEM (label,suc1.frml) grp` by ( 1379 `SORTED P fls 1380 ��� ���x y. 1381 (MEM x fls ��� MEM y fls ��� (FST x).edge_grp = (FST y).edge_grp) 1382 ��� (FST x = FST y)` by ( 1383 fs[flws_sorted_def] >> metis_tac[domain_lookup] 1384 ) 1385 >> `���l_sub. 1386 MEM l_sub (GROUP_BY E (J fls)) ��� 1387 (���x y. MEM x l_sub ��� MEM y l_sub ��� E x y) ��� 1388 ���x y. MEM x l_sub ��� MEM y (J fls) ��� E x y 1389 ��� MEM y l_sub` by ( 1390 HO_MATCH_MP_TAC SORTED_GROUP_BY 1391 >> qexists_tac `P_c` >> fs[] >> metis_tac[] 1392 ) 1393 >> first_x_assum (qspec_then `grp` mp_tac) >> simp[] 1394 >> rpt strip_tac 1395 >> `MEM (label,suc1.frml) (J fls)` by ( 1396 qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1397 >> qexists_tac `(label,sucId1)` >> simp[] 1398 >> Cases_on `lookup sucId1 g_AA.nodeInfo` >> fs[] 1399 ) 1400 >> `E (label,suc.frml) (label,suc1.frml)` by ( 1401 qunabbrev_tac `E` >> fs[] 1402 ) 1403 >> metis_tac[] 1404 ) 1405 >> qunabbrev_tac `CE` >> fs[] >> Cases_on `grp` >> fs[] 1406 >> Cases_on `h` >> fs[concrEdge_component_equality] 1407 >- (rw[] >> fs[MEM] >> metis_tac[MEM,nub_set]) 1408 >- (rw[] >> fs[MEM] 1409 >> `MEM suc1.frml (MAP SND t)` by ( 1410 fs[MEM_MAP] >> qexists_tac `(label,suc1.frml)` >> simp[] 1411 ) 1412 >> metis_tac[MEM,nub_set] 1413 ) 1414 >- (rw[] >> fs[MEM] >> metis_tac[MEM,nub_set]) 1415 >- (rw[] >> fs[MEM] 1416 >> `MEM suc1.frml (MAP SND t)` by ( 1417 fs[MEM_MAP] >> qexists_tac `(label,suc1.frml)` >> simp[] 1418 ) 1419 >> metis_tac[MEM,nub_set] 1420 ) 1421 ) 1422 ) 1423 >- (qunabbrev_tac `CE` >> Cases_on `grp` >> fs[] >> Cases_on `h` 1424 >> fs[concrEdge_component_equality] 1425 >> `q = label` by ( 1426 `SORTED P fls 1427 ��� ���x y. 1428 (MEM x fls ��� MEM y fls ��� (FST x).edge_grp = (FST y).edge_grp) 1429 ��� (FST x = FST y)` by ( 1430 fs[flws_sorted_def] >> metis_tac[domain_lookup] 1431 ) 1432 >> `���l_sub. 1433 MEM l_sub (GROUP_BY E (J fls)) ��� 1434 (���x y. MEM x l_sub ��� MEM y l_sub ��� E x y) ��� 1435 ���x y. MEM x l_sub ��� MEM y (J fls) ��� E x y 1436 ��� MEM y l_sub` by ( 1437 HO_MATCH_MP_TAC SORTED_GROUP_BY 1438 >> qexists_tac `P_c` >> fs[] >> metis_tac[] 1439 ) 1440 >> first_x_assum (qspec_then `(q,r)::t` mp_tac) >> simp[] 1441 >> rpt strip_tac 1442 >> `MEM (q,r) (J fls)` by ( 1443 `MEM (q,r) (FLAT CONCR_TRNS)` suffices_by metis_tac[] 1444 >> simp[MEM_FLAT] >> qexists_tac `((q,r)::t)` >> simp[] 1445 ) 1446 >> `E (q,r) (label,suc.frml)` by metis_tac[] 1447 >> qunabbrev_tac `J` >> fs[CAT_OPTIONS_MEM,MEM_MAP] 1448 >> rename[`MEM edge fls`] >> Cases_on `edge` >> fs[] 1449 >> rename[`MEM (e_lab,e_id) fls`] 1450 >> Cases_on `lookup e_id g_AA.nodeInfo` >> fs[] 1451 >> first_x_assum (qspec_then `(e_lab,e_id)` mp_tac) >> simp[] 1452 >> rpt strip_tac 1453 >> first_x_assum (qspec_then `(label,sucId)` mp_tac) 1454 >> qunabbrev_tac `E` >> fs[] >> rw[] 1455 ) 1456 >> rw[] 1457 ) 1458 ) 1459 >> qexists_tac `cE` >> Cases_on `cE` >> simp[concr2AbstractEdge_def] 1460 >> rw[] 1461 >- fs[concrEdge_component_equality] 1462 >- (disj1_tac >> metis_tac[]) 1463 ) 1464 >- (Cases_on `lookup id g_AA.followers` >> fs[] >> simp[MEM_MAP] 1465 >> fs[OPTION_TO_LIST_MEM] 1466 >> rename[`findNode _ g_AA = SOME x2`,`_ x2 = SOME el_list`] 1467 >> `x2 = (id,node)` by metis_tac[UNIQUE_NODE_FIND_LEMM,SOME_11] 1468 >> rw[] >> fs[] >> rename[`lookup id g_AA.followers = SOME fls`] 1469 >> qexists_tac `concrEdge l.pos_lab l.neg_lab []` 1470 >> simp[concr2AbstractEdge_def,CAT_OPTIONS_MEM,MEM_MAP] >> disj2_tac 1471 >> metis_tac[] 1472 ) 1473 ); 1474 1475val suff_wfg_def = Define 1476`suff_wfg g = !n. (g.next <= n) ==> ~(n ��� domain g.nodeInfo)`; 1477 1478val WF_IMP_SUFFWFG = store_thm 1479 ("WF_IMP_SUFFWFG", 1480 ``!g. wfg g ==> suff_wfg g``, 1481 rpt strip_tac >> fs[suff_wfg_def,wfg_def] 1482 ) 1483 1484val inGBA_def = Define` 1485 inGBA g qs = 1486 let gbaNodes = MAP SND (toAList g.nodeInfo) 1487 in EXISTS (��n. MEM_EQUAL n.frmls qs) gbaNodes`; 1488 1489val IN_GBA_MEM_EQUAL = store_thm 1490 ("IN_GBA_MEM_EQUAL", 1491 ``!G x y. MEM_EQUAL x y ==> (inGBA G x = inGBA G y)``, 1492 gen_tac 1493 >> `!x y. MEM_EQUAL x y ==> (inGBA G x ==> inGBA G y)` 1494 suffices_by metis_tac[MEM_EQUAL_SET] 1495 >> simp[EQ_IMP_THM] >> rpt strip_tac 1496 >> fs[inGBA_def] 1497 >> `(��n. MEM_EQUAL n.frmls x) = (��n. MEM_EQUAL n.frmls y)` by ( 1498 Q.HO_MATCH_ABBREV_TAC `A = B` 1499 >> `!x. A x = B x` suffices_by metis_tac[] 1500 >> rpt strip_tac >> qunabbrev_tac `A` 1501 >> qunabbrev_tac `B` >> fs[] 1502 >> fs[MEM_EQUAL_SET] 1503 ) 1504 >> fs[] 1505 ); 1506 1507val addNodeToGBA_def = Define` 1508 addNodeToGBA g qs = 1509 if inGBA g qs 1510 then g 1511 else addNode (nodeLabelGBA qs) g`; 1512 1513 1514val ADDNODE_GBA_WFG = store_thm 1515 ("ADDNODE_GBA_WFG", 1516 ``!g qs. wfg g ==> wfg (addNodeToGBA g qs)``, 1517 rpt strip_tac >> simp[addNodeToGBA_def] >> Cases_on `inGBA g qs` >> fs[] 1518 ); 1519 1520val ADDNODE_GBA_WFG_FOLDR = store_thm 1521 ("ADDNODE_GBA_WFG_FOLDR", 1522 ``!G l. wfg G ==> 1523 (let G_WITH_IDS = 1524 FOLDR 1525 (��n (ids,g). 1526 if inGBA g n then (ids,g) 1527 else (g.next::ids,addNodeToGBA g n)) ([],G) l 1528 in wfg (SND G_WITH_IDS))``, 1529 gen_tac >> Induct_on `l` >> rpt strip_tac >> fs[] 1530 >> Cases_on `FOLDR 1531 (��n (ids,g). 1532 if inGBA g n then (ids,g) 1533 else (g.next::ids,addNodeToGBA g n)) ([],G) l` 1534 >> fs[] >> Cases_on `inGBA r h` >> fs[ADDNODE_GBA_WFG] 1535 ); 1536 1537val ADDNODE_GBA_DOM_FOLDR = store_thm 1538 ("ADDNODE_GBA_DOM_FOLDR", 1539 ``!G l. wfg G ==> 1540 (let G_WITH_IDS = 1541 FOLDR 1542 (��n (ids,g). 1543 if inGBA g n then (ids,g) 1544 else (g.next::ids,addNodeToGBA g n)) ([],G) l 1545 in ((set (FST (G_WITH_IDS))) ��� domain G.nodeInfo = 1546 domain (SND G_WITH_IDS).nodeInfo) 1547 ��� (G.next <= (SND G_WITH_IDS).next))``, 1548 gen_tac >> Induct_on `l` >> rpt strip_tac >> fs[] 1549 >> Cases_on `FOLDR 1550 (��n (ids,g). 1551 if inGBA g n then (ids,g) 1552 else (g.next::ids,addNodeToGBA g n)) ([],G) l` 1553 >> fs[] >> Cases_on `inGBA r h` >> fs[] 1554 >> simp[SUBSET_DEF] >> rpt strip_tac >> fs[] 1555 >> simp[addNodeToGBA_def,addNode_def] 1556 >> fs[SUBSET_DEF,INSERT_UNION] >> Cases_on `r.next ��� domain G.nodeInfo` 1557 >> fs[wfg_def] >> metis_tac[] 1558 ); 1559 1560(* val ADDNODE_GBA_DOM_FOLDR2 = store_thm *) 1561(* ("ADDNODE_GBA_DOM_FOLDR2", *) 1562 1563(* ) *) 1564 1565 1566val ADDNODE_GBA_LEMM = store_thm 1567 ("ADDNODE_GBA_LEMM", 1568 ``!g qs. suff_wfg g ==> 1569 ({ set x | inGBA (addNodeToGBA g qs) x } = 1570 { set x | inGBA g x } ��� {set qs})``, 1571 rpt strip_tac 1572 >> `{set x | inGBA (addNodeToGBA g qs) x} ��� {set x | inGBA g x} ��� {set qs} 1573 ��� {set x | inGBA g x} ��� {set qs} ��� {set x | inGBA (addNodeToGBA g qs) x}` 1574 suffices_by metis_tac[SET_EQ_SUBSET] 1575 >> simp[SUBSET_DEF] >> rpt strip_tac 1576 >> fs[addNodeToGBA_def] >> Cases_on `inGBA g qs` 1577 >> fs[] >> fs[inGBA_def] 1578 >- (fs[EXISTS_MEM,MEM_MAP] >> `?i. y = (i,n)` by (Cases_on `y` >> fs[]) 1579 >> Cases_on `set x' = set qs` >> fs[] >> rw[] >> qexists_tac `n.frmls` 1580 >> fs[MEM_EQUAL_SET] >> qexists_tac `n` >> fs[] >> qexists_tac `(i,n)` 1581 >> fs[]) 1582 >- (fs[EXISTS_MEM,MEM_MAP] >> `?i. y = (i,n)` by (Cases_on `y` >> fs[]) 1583 >> Cases_on `set x' = set qs` >> fs[] 1584 >> `SOME n = lookup i (addNode (nodeLabelGBA qs) g).nodeInfo` 1585 by metis_tac[MEM_toAList] 1586 >> fs[addNode_def,lookup_insert] >> Cases_on `i = g.next` 1587 >> fs[MEM_toAList] >> fs[EVERY_MEM] >> rw[] >> fs[MEM_EQUAL_SET] 1588 >> qexists_tac `n.frmls` >> fs[] >> qexists_tac `n` >> fs[] 1589 >> qexists_tac `(i,n)` >> fs[MEM_toAList] 1590 ) 1591 >- metis_tac[] 1592 >- (fs[EXISTS_MEM] >> qexists_tac `n.frmls` >> fs[MEM_EQUAL_SET] 1593 >> simp[addNode_def] >> qexists_tac `n` >> fs[] 1594 >> fs[MEM_MAP] >> qexists_tac `y` 1595 >> `?i. (i,n) = y` by (Cases_on `y` >> fs[]) 1596 >> `~(i = g.next)` by ( 1597 fs[suff_wfg_def] >> CCONTR_TAC >> `~(i ��� domain g.nodeInfo)` by fs[] 1598 >> rw[] >> metis_tac[MEM_toAList,domain_lookup] 1599 ) 1600 >> rw[] >> metis_tac[lookup_insert,MEM_toAList] 1601 ) 1602 >- metis_tac[] 1603 >- (qexists_tac `qs` >> fs[EXISTS_MEM] >> qexists_tac `nodeLabelGBA qs` 1604 >> fs[MEM_EQUAL_SET,MEM_MAP] >> qexists_tac `(g.next,nodeLabelGBA qs)` 1605 >> fs[] >> simp[MEM_toAList] >> simp[addNode_def,lookup_insert] 1606 ) 1607 ); 1608 1609val frml_ad_def = Define` 1610 frml_ad g = 1611 !i n. i ��� (domain g.nodeInfo) ��� (lookup i g.nodeInfo = SOME n) 1612 ==> ALL_DISTINCT n.frmls`; 1613 1614val FRML_AD_NODEINFO = store_thm 1615 ("FRML_AD_NODEINFO", 1616 ``!g1 g2. (g1.nodeInfo = g2.nodeInfo) ==> (frml_ad g1 = frml_ad g2)``, 1617 rpt strip_tac >> simp[frml_ad_def] 1618 ); 1619 1620val ADDNODE_GBA_FOLDR = store_thm 1621 ("ADDNODE_GBA_FOLDR", 1622 ``!G l. suff_wfg G ==> 1623 (let G_WITH_IDS = 1624 FOLDR 1625 (��n (ids,g). 1626 if inGBA g n then (ids,g) 1627 else (g.next::ids,addNodeToGBA g n)) ([],G) l 1628 in 1629 (suff_wfg (SND G_WITH_IDS) 1630 ��� ({ set x | inGBA (SND G_WITH_IDS) x } = 1631 { set x | inGBA G x } ��� set (MAP set l)) 1632 ��� (!i. i ��� domain G.nodeInfo 1633 ==> (lookup i G.nodeInfo = lookup i (SND G_WITH_IDS).nodeInfo) 1634 ��� (lookup i G.followers = lookup i (SND G_WITH_IDS).followers) 1635 ) 1636 ��� (G.next <= (SND G_WITH_IDS).next) 1637 ��� (domain G.nodeInfo ��� domain (SND G_WITH_IDS).nodeInfo) 1638 ��� (!i. MEM i (FST G_WITH_IDS) 1639 ==> ?n. (lookup i (SND G_WITH_IDS).nodeInfo = SOME n) 1640 ��� (MEM n.frmls l) 1641 ��� lookup i (SND G_WITH_IDS).followers = SOME [] 1642 ��� (G.next <= i) 1643 ) 1644 ��� (frml_ad G ��� (!x. MEM x l ==> ALL_DISTINCT x) 1645 ==> frml_ad (SND G_WITH_IDS)) 1646 ))``, 1647 gen_tac >> Induct_on `l` >> rpt strip_tac >> fs[] 1648 >> Q.HO_MATCH_ABBREV_TAC `suff_wfg G2 ��� A = B 1649 ��� (!i. i ��� domain G.nodeInfo 1650 ==> (lookup i G1.nodeInfo 1651 = lookup i G2.nodeInfo) 1652 ��� (lookup i G1.followers 1653 = lookup i G2.followers) 1654 ) 1655 ��� (G.next <= G2.next) 1656 ��� (domain G.nodeInfo ��� domain G2.nodeInfo) 1657 ��� C` 1658 >> Cases_on `FOLDR 1659 (��n (ids,g). 1660 if inGBA g n then (ids,g) 1661 else (g.next::ids,addNodeToGBA g n)) ([],G) l` 1662 >> fs[] 1663 >> `suff_wfg G2 ��� (A = B) 1664 ��� (���i. 1665 (i ��� domain G.nodeInfo) ��� 1666 (lookup i G1.nodeInfo = lookup i G2.nodeInfo) 1667 ��� (lookup i G1.followers = lookup i G2.followers) 1668 ) 1669 ��� G.next ��� G2.next 1670 ��� domain G.nodeInfo ��� domain G2.nodeInfo 1671 ��� ((A = B) 1672 ��� (���i. 1673 (i ��� domain G.nodeInfo) ��� 1674 (lookup i G1.nodeInfo = lookup i G2.nodeInfo) 1675 ��� (lookup i G1.followers = lookup i G2.followers)) ==> C)` 1676 suffices_by fs[] 1677 >> rw[] 1678 >- (qunabbrev_tac `G1` 1679 >> Cases_on `inGBA r h` >> fs[] >> qunabbrev_tac `G2` 1680 >> fs[addNodeToGBA_def,suff_wfg_def] >> rpt strip_tac 1681 >> fs[addNode_def] 1682 >> metis_tac[DECIDE ``SUC r.next <= n ==> r.next <= n``] 1683 ) 1684 >- (qunabbrev_tac `G1` 1685 >> simp[SET_EQ_SUBSET,SUBSET_DEF] >> qunabbrev_tac `A` 1686 >> qunabbrev_tac `B` 1687 >> fs[] >> rpt strip_tac >> qunabbrev_tac `G2` 1688 >- (Cases_on `inGBA r h` >> fs[] 1689 >- (`x ��� {set x | inGBA r x}` by (fs[] >> metis_tac[]) 1690 >> `x ��� {set x | inGBA G x} ��� set (MAP set l)` 1691 by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] 1692 >> fs[UNION_DEF] >> metis_tac[] 1693 ) 1694 >- (`x ��� {set a | inGBA (addNodeToGBA r h) a}` by (fs[] >> metis_tac[]) 1695 >> `x ��� {set a | inGBA r a} ��� {set h}` by metis_tac[ADDNODE_GBA_LEMM] 1696 >> fs[UNION_DEF] 1697 >- (`x ��� {set x | inGBA r x}` by (fs[] >> metis_tac[]) 1698 >> `x ��� {x'' | (���x. x'' = set x ��� inGBA G x) 1699 ��� MEM x'' (MAP set l)}` 1700 by metis_tac[SET_EQ_SUBSET,SUBSET_DEF] 1701 >> fs[] >> metis_tac[] 1702 ) 1703 >- metis_tac[] 1704 ) 1705 ) 1706 >- (Cases_on `inGBA r h` >> fs[] 1707 >- (`x ��� {set x | inGBA G x}` by (fs[] >> metis_tac[]) 1708 >> `x ��� {set x | inGBA r x}` by metis_tac[IN_UNION] 1709 >> fs[] >> metis_tac[] 1710 ) 1711 >- (`x ��� {set x | inGBA G x}` by (fs[] >> metis_tac[]) 1712 >> `x ��� {set x | inGBA r x}` by metis_tac[IN_UNION] 1713 >> `x ��� {set x | inGBA (addNodeToGBA r h) x}` 1714 by metis_tac[IN_UNION,ADDNODE_GBA_LEMM] 1715 >> fs[] >> metis_tac[] 1716 ) 1717 ) 1718 >- (qexists_tac `h` >> Cases_on `inGBA r h` >> fs[] 1719 >> `x ��� {set h}` by fs[] 1720 >> `x ��� {set x | inGBA (addNodeToGBA r h) x}` 1721 by metis_tac[IN_UNION,ADDNODE_GBA_LEMM] 1722 >> fs[inGBA_def,EXISTS_MEM] >> metis_tac[MEM_EQUAL_SET] 1723 ) 1724 >- (`x ��� {set x | inGBA r x}` by metis_tac[IN_UNION] 1725 >> Cases_on `inGBA r h` >> fs[] 1726 >- metis_tac[] 1727 >- (`x ��� {set x | inGBA r x}` by metis_tac[IN_UNION] 1728 >> `x ��� {set x | inGBA (addNodeToGBA r h) x}` 1729 by metis_tac[IN_UNION,ADDNODE_GBA_LEMM] 1730 >> fs[] >> metis_tac[] 1731 ) 1732 ) 1733 ) 1734 >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[] 1735 >> simp[addNodeToGBA_def,addNode_def] 1736 >> `~(i = G1.next)` by ( 1737 fs[suff_wfg_def] >> `~(G1.next <= i)` by metis_tac[SUBSET_DEF] 1738 >> fs[] 1739 ) 1740 >> metis_tac[lookup_insert] 1741 ) 1742 >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[] 1743 >> simp[addNodeToGBA_def,addNode_def] 1744 >> `~(i = G1.next)` by ( 1745 fs[suff_wfg_def] >> `~(G1.next <= i)` by metis_tac[SUBSET_DEF] 1746 >> fs[] 1747 ) 1748 >> metis_tac[lookup_insert] 1749 ) 1750 >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[] 1751 >> simp[addNodeToGBA_def,addNode_def]) 1752 >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[] 1753 >> simp[addNodeToGBA_def,addNode_def,SUBSET_DEF] >> rpt strip_tac 1754 >> metis_tac[SUBSET_DEF] 1755 ) 1756 >- (qunabbrev_tac `C` >> fs[] >> rpt strip_tac >> Cases_on `inGBA G1 h` 1757 >> fs[] 1758 >- metis_tac[] 1759 >- (qunabbrev_tac `G2` >> rw[] >> fs[addNodeToGBA_def,addNode_def]) 1760 >- (qunabbrev_tac `G2` >> rw[] >> fs[addNodeToGBA_def,addNode_def] 1761 >> `~(i = G1.next)` by ( 1762 fs[suff_wfg_def] 1763 >> `~(G1.next <= i)` by metis_tac[domain_lookup] 1764 >> fs[] 1765 ) 1766 >> metis_tac[lookup_insert] 1767 ) 1768 >- (fs[frml_ad_def] >> rpt strip_tac 1769 >> qunabbrev_tac `G2` >> fs[addNodeToGBA_def] 1770 >> Cases_on `inGBA G1 h` >> fs[addNode_def] 1771 >- (`n = nodeLabelGBA h` by metis_tac[lookup_insert,SOME_11] 1772 >> fs[] 1773 ) 1774 >- (fs[suff_wfg_def] >> `~(G1.next <= i)` by metis_tac[] 1775 >> `~(G1.next = i)` by fs[] 1776 >> `lookup i G1.nodeInfo = SOME n` 1777 by metis_tac[lookup_insert,SOME_11] 1778 >> metis_tac[] 1779 ) 1780 ) 1781 ) 1782 ); 1783 1784val addEdgeToGBA_def = Define` 1785 addEdgeToGBA g id eL suc = 1786 case findNode (��(i,q). MEM_EQUAL q.frmls suc) g of 1787 | SOME (i,q) => addEdge id (eL,i) g 1788 | NONE => NONE`; 1789 1790val ADDEDGE_GBA_LEMM = store_thm 1791 ("ADDEDGE_GBA_LEMM", 1792 ``!g id eL suc. 1793 wfg g ��� (id ��� domain g.nodeInfo) ��� (inGBA g suc) 1794 ==> (?g2. (addEdgeToGBA g id eL suc = SOME g2) 1795 ��� (g.nodeInfo = g2.nodeInfo) 1796 ��� wfg g2)``, 1797 rpt strip_tac >> simp[addEdgeToGBA_def] 1798 >> Cases_on `findNode (��(i,q). MEM_EQUAL q.frmls suc) g` >> fs[] 1799 >- ( 1800 fs[inGBA_def,EXISTS_MEM,findNode_def,MEM_MAP] 1801 >> `(��(i,q). MEM_EQUAL q.frmls suc) y` by (Cases_on `y` >> fs[] >> rw[]) 1802 >> metis_tac[FIND_LEMM,NOT_SOME_NONE] 1803 ) 1804 >- ( 1805 Cases_on `x` >> fs[] >> simp[addEdge_def] 1806 >> `?fl_old. lookup id g.followers = SOME fl_old` 1807 by metis_tac[wfg_def,domain_lookup] 1808 >> qexists_tac `g with followers updated_by insert id ((eL,q)::fl_old)` 1809 >> fs[findNode_def] 1810 >> `MEM (q,r) (toAList g.nodeInfo)` by metis_tac[FIND_LEMM2] 1811 >> `q ��� domain g.nodeInfo` by metis_tac[MEM_toAList,domain_lookup] 1812 >> fs[wfg_def,INSERT_DEF] >> strip_tac >> fs[wfAdjacency_def] 1813 >- (simp[SET_EQ_SUBSET,SUBSET_DEF] >> rpt strip_tac >> fs[]) 1814 >- (rpt strip_tac >> Cases_on `n = id` >> fs[] 1815 >> Cases_on `k = id` >> fs[] 1816 >- (rw[] >> fs[] >> metis_tac[]) 1817 >- (rw[] >> metis_tac[lookup_insert]) 1818 ) 1819 ) 1820 ); 1821 1822val ADDEDGE_GBA_FOLDR_LEMM = store_thm 1823 ("ADDEDGE_GBA_FOLDR_LEMM", 1824 ``!g id ls. 1825 wfg g ��� (id ��� domain g.nodeInfo) ��� (!x. MEM x (MAP SND ls) ==> inGBA g x) 1826 ==> 1827 ?g2. 1828 (FOLDR 1829 (��(eL,suc) g_opt. 1830 do g <- g_opt; addEdgeToGBA g id eL suc od) 1831 (SOME g) ls = SOME g2) 1832 ��� (g.nodeInfo = g2.nodeInfo) ��� wfg g2``, 1833 gen_tac >> gen_tac >> Induct_on `ls` >> fs[] >> rpt strip_tac >> fs[] 1834 >> Cases_on `h` >> fs[] >> HO_MATCH_MP_TAC ADDEDGE_GBA_LEMM 1835 >> fs[] >> rw[] 1836 >- metis_tac[] 1837 >- (`inGBA g r` by fs[] 1838 >> fs[inGBA_def] >> metis_tac[] 1839 ) 1840 ); 1841 1842val extractGBATrans_def = Define` 1843 extractGBATrans aP g q = 1844 (set o OPTION_TO_LIST) 1845 (do (id,n) <- findNode (��(i,n). ((set n.frmls) = q)) g ; 1846 fls <- lookup id g.followers ; 1847 SOME ( 1848 (CAT_OPTIONS 1849 (MAP (��(eL,i). 1850 do nL <- lookup i g.nodeInfo ; 1851 SOME ( 1852 (transformLabel aP eL.pos_lab eL.neg_lab, 1853 set nL.frmls) 1854 ) 1855 od 1856 ) fls 1857 ) 1858 ) 1859 ) 1860 od) `; 1861 1862val concr2AbstrGBA_final_def = Define` 1863 concr2AbstrGBA_final final_forms graph aP = 1864 { {(set q1.frmls, transformLabel aP eL.pos_lab eL.neg_lab, set q2.frmls) | 1865 ?id1 id2 fls. 1866 (lookup id1 graph.nodeInfo = SOME q1) 1867 ��� (lookup id1 graph.followers = SOME fls) 1868 ��� (MEM (eL,id2) fls) ��� (MEM f eL.acc_set) 1869 ��� (lookup id2 graph.nodeInfo = SOME q2) 1870 } | f | (f ��� final_forms) 1871 }`; 1872 1873val concr2AbstrGBA_states_def = Define` 1874 concr2AbstrGBA_states graph = 1875 { set x.frmls | SOME x ��� 1876 (IMAGE (\n. lookup n graph.nodeInfo) 1877 (domain graph.nodeInfo))}`; 1878 1879val concr2AbstrGBA_init_def = Define` 1880 concr2AbstrGBA_init concrInit graph = 1881 set (CAT_OPTIONS (MAP (\i. do n <- lookup i graph.nodeInfo ; 1882 SOME (set n.frmls) 1883 od ) concrInit))`; 1884 1885val concr2AbstrGBA_def = Define ` 1886 concr2AbstrGBA (concrGBA graph init all_acc_frmls aP) = 1887 GBA 1888 (concr2AbstrGBA_states graph) 1889 (concr2AbstrGBA_init init graph) 1890 (extractGBATrans (set aP) graph) 1891 (concr2AbstrGBA_final (set all_acc_frmls) graph (set aP)) 1892 (POW (set aP))`; 1893 1894val _ = export_theory(); 1895