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