logic/ltl/concrGBArepScript.sml

102             >> fs[cE_equiv_def] >> rw[MEM_EQUAL_SET,LIST_TO_SET_FILTER]
134                   >- (rw[] >> fs[] >> Cases_on `s = []` >> fs[]
145                       >> rw[]
150                   >- (fs[MEM_GENLIST] >> rw[] >> fs[]
173        >> rw[]
193    >> rw[FOLDR_CONCR_EDGE]
201        >> rpt strip_tac >> simp[d_conj_concr_def] >> rw[FOLDR_LEMM4]
224            >> rw[]
285        >- (qunabbrev_tac `s` >> rw[] >> simp[d_conj_set_def,ITSET_THM]
329             >> rw[FOLDR_CONCR_EDGE] >> simp[concr2AbstractEdge_def]
333              >- (`x ��� a_sel q` suffices_by rw[]
358                        >> qexists_tac `(d,i)` >> fs[EL_MAP] >> rw[]
375                    >> qexists_tac `q` >> rw[]
427                         >> rw[] >> Cases_on `EL r trns_concr_list`
428                         >> rw[]
435                 >> rw[] >> metis_tac[]
472                                   (rw[] >> fs[] >> Cases_on `EL i trns_concr_list`
475                              >> Cases_on `EL r' trns_concr_list` >> rw[] >> fs[]
487                              >> Cases_on `k` >> fs[] >> rw[]
518                       >> fs[] >> rpt strip_tac >> rw[] >> fs[]
520                       >- (qexists_tac `q`>> fs[] >> rw[]
559                          >> Cases_on `EL r'' trns_concr_list` >> rw[] >> fs[]
560                      ) >> rw[]
567                     >> Cases_on `EL r'' trns_concr_list` >> rw[] >> fs[]
594            >- (fs[] >> Cases_on `x'` >> rw[]
610     >- (qunabbrev_tac `s` >> rw[] >> fs[d_conj_set_def,ITSET_THM]
663            >> qexists_tac `(q,d_c)` >> rw[] >> fs[EL_MEM]
666          >> rw[] >> fs[MEM_MAP] >> metis_tac[]
682          >> first_x_assum (qspec_then `d_c` mp_tac) >> rw[]
692      >> rw[FOLDR_CONCR_EDGE] >> qunabbrev_tac `c2a`
710            Cases_on `trns_concr_list` >> rw[] >> Cases_on `h` >> metis_tac[])
717       >- (rw[]
737                 >> Cases_on `EL i trns_concr_list` >> fs[] >> rw[]
746       >- (rw[] >> fs[IN_INTER,IN_BIGINTER]
755                    >> Cases_on `EL y trns_concr_list` >> rw[] >> simp[EL_MAP]
757               >> rw[]
780      >- (rw[] >> Q.HO_MATCH_ABBREV_TAC `S1 = BIGUNION S2`
784             qunabbrev_tac `S1` >> qunabbrev_tac `S2` >> fs[] >> rw[]
797              >> qexists_tac `f i` >> rw[] >> simp[MEM_MAP]
811              >> rw[] >> qexists_tac `(q,d_c)` >> fs[EL_MEM]
924    >> rw[] >> fs[MEM_APPEND,CAT_OPTIONS_MEM,MEM_MAP]
1017        >> Cases_on `h1` >> Cases_on `h` >> fs[] >> rw[]
1045                >> fs[] >> rw[] >> metis_tac[MEM]
1051                >> fs[CAT_OPTIONS_def] >> rw[]
1076    >> rw[]
1078        >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM] >> rw[]
1109                 >> rw[] >> `0 < (FST (eL,r)).edge_grp` by metis_tac[]
1147                         >- (qexists_tac `y_id` >> rw[] >> fs[]
1177                     >> fs[] >> rw[]
1179                     >> rpt strip_tac >> rw[]
1193                     >> rw[]
1202                     >> rw[] >> fs[] >> rw[] >> qexists_tac `(eL,suc.frml)`
1234        >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM] >> rw[]
1249          >> rw[] >> fs[] >> rw[]
1301                >> rw[] >> qunabbrev_tac `E` >> fs[]
1304              >> fs[concrEdge_component_equality] >> rw[]
1313                      >> rw[]
1341                               >> rw[] >> metis_tac[]
1356                     (*    >> rw[] *)
1361                     (*          >> rw[] >> fs[] >> metis_tac[] *)
1407              >- (rw[] >> fs[MEM] >> metis_tac[MEM,nub_set])
1408              >- (rw[] >> fs[MEM]
1414              >- (rw[] >> fs[MEM] >> metis_tac[MEM,nub_set])
1415              >- (rw[] >> fs[MEM]
1454                 >> qunabbrev_tac `E` >> fs[] >> rw[]
1456              >> rw[]
1460        >> rw[]
1468        >> rw[] >> fs[] >> rename[`lookup id g_AA.followers = SOME fls`]
1579        >> Cases_on `set x' = set qs` >> fs[] >> rw[] >> qexists_tac `n.frmls`
1587        >> fs[MEM_toAList] >> fs[EVERY_MEM] >> rw[] >> fs[MEM_EQUAL_SET]
1598             >> rw[] >> metis_tac[MEM_toAList,domain_lookup]
1600        >> rw[] >> metis_tac[lookup_insert,MEM_toAList]
1677    >> rw[]
1734    >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[]
1742    >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[]
1750    >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[]
1752    >- (fs[] >> rw[] >> Cases_on `inGBA G1 h` >> qunabbrev_tac `G2` >> fs[]
1759        >- (qunabbrev_tac `G2` >> rw[] >> fs[addNodeToGBA_def,addNode_def])
1760        >- (qunabbrev_tac `G2` >> rw[] >> fs[addNodeToGBA_def,addNode_def]
1801     >> `(��(i,q). MEM_EQUAL q.frmls suc) y` by (Cases_on `y` >> fs[] >> rw[])
1816         >- (rw[] >> fs[] >> metis_tac[])
1817         >- (rw[] >> metis_tac[lookup_insert])
1835    >> fs[] >> rw[]