Lines Matching refs:rw
36 >> fs[MEM_EQUAL_SET] >> rw[]
58 >- (Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (f,f_trns) acc`]
139 >> Cases_on `y` >> fs[] >> rw[]
168 >> rw[]
244 >> rw[] >> rename[`(��,sucs) ��� aa_red.trans n.frml`]
252 >> `a ��� ��` by rw[]
263 >> rw[]
352 >> rw[] >> fs[MEM_SUBSET_SET_TO_LIST]
366 >> rw[] >> fs[findNode_def]
378 >> fs[] >> simp[acc_cond_concr_def] >> rw[]
381 >- (Cases_on `ce2` >> fs[concr2AbstractEdge_def] >> rw[]
389 >> fs[concr2AbstractEdge_def] >> rw[]
398 >> rw[] >> fs[concr2AbstrAA_def] >> rw[]
421 >> `cT = f_trns` by metis_tac[SOME_11] >> rw[]
426 >> fs[MEM_MAP] >> rename[`MEM ce cT`] >> rw[]
446 >> fs[] >> rw[] >> metis_tac[]
455 >> Cases_on `ce2` >> fs[concr2AbstractEdge_def] >> rw[]
505 ) >> rw[]
527 >> rw[] >> metis_tac[SET_OF_SUBLISTS_FINITE,IMAGE_FINITE]
584 Induct_on `a` >> fs[] >> rw[]
642 >> rw[]
644 >> rw[] >> fs[maximal_elements_def] >> rw[] >> fs[] >> rw[]
766 >- (fs[addEdge_def] >> rw[])
784 >> fs[] >> Cases_on `inGBA r h` >> fs[] >> rw[]
838 >> rw[] >> fs[]
840 >> rw[]
855 >> fs[] >> Cases_on `inGBA r h` >> fs[] >> rw[]
878 >> fs[EXISTS_MEM,MEM_MAP] >> Cases_on `y` >> fs[] >> rw[]
933 >> qunabbrev_tac `M` >> fs[] >> rw[]
955 >> rw[] >> `new_ids = []` by fs[]
962 >> rw[]
1253 >> rw[]
1300 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[])
1444 >> rw[]
1500 >> qunabbrev_tac `ce_lists` >> rw[]
1525 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[]
1553 >> rw[]
1593 >> rw[]
1625 >> rw[]
1694 >> rw[]
1741 >> fs[] >> rw[]
1757 >> `l = cT` by metis_tac[SOME_11] >> rw[]
1763 >> rw[]
1766 by (rw[] >> metis_tac[domain_lookup])
1771 >> rw[] >> simp[graphStates_def,MEM_MAP]
1777 >> fs[concr2AbstractEdge_def] >> rw[]
1819 >> rw[]
1821 >- (rw[] >> Cases_on `cE` >> Cases_on `ce2`
1854 >> first_x_assum (qspec_then `nL` mp_tac) >> rw[]
1868 >> rw[] >> POP_ASSUM mp_tac >> simp[reachableFromSetGBA_def]
1869 >> rpt strip_tac >> fs[] >> rw[]
1980 >- (fs[one_step_closed_def] >> rpt strip_tac >> fs[expandGBA_def] >> rw[]
1982 >> Cases_on `y` >> fs[] >> rw[]
2031 >> rw[]
2078 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[])
2166 >- (rw[]
2247 >> rw[]
2270 >> rw[]
2281 >> qunabbrev_tac `ce_lists` >> rw[]
2306 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[]
2334 >> rw[]
2374 >> rw[]
2406 >> rw[]
2475 >> fs[] >> rw[]
2491 >> `l = cT` by metis_tac[SOME_11] >> rw[]
2497 >> rw[]
2500 by (rw[] >> metis_tac[domain_lookup])
2505 >> rw[] >> simp[graphStates_def,MEM_MAP]
2511 >> fs[concr2AbstractEdge_def] >> rw[]
2532 >> rw[] >> metis_tac[]
2540 >> rw[]
2565 >> rw[]
2585 >> Cases_on `y` >> rw[]
2723 >> rw[]
2770 by (rpt strip_tac >> rw[] >> fs[] >> metis_tac[])
2852 >- (rw[]
2856 >- (rw[]
2863 >> rw[] >> fs[MEM_EQUAL_SET]
3007 >> rw[]
3031 >> rw[]
3042 >> qunabbrev_tac `ce_lists` >> rw[]
3067 >> rw[] >> `EL ind_q (CAT_OPTIONS L) = q_i` by fs[]
3095 >> rw[]
3135 >> rw[]
3167 >> rw[]
3220 >> fs[] >> rw[]
3236 >> `l = cT` by metis_tac[SOME_11] >> rw[]
3242 >> rw[]
3245 by (rw[] >> metis_tac[domain_lookup])
3250 >> rw[] >> simp[graphStates_def,MEM_MAP]
3256 >> fs[concr2AbstractEdge_def] >> rw[]
3292 >> rw[]
3304 >> fs[] >> rw[] >> metis_tac[MEM_EQUAL_SET]
3326 >> rw[] >> Cases_on `cE` >> simp[concr2AbstractEdge_def]
3363 >> rw[] >> Cases_on `cE` >> simp[concr2AbstractEdge_def]
3380 >- (rw[] >> metis_tac[all_acc_cond_def])
3394 >- (rw[] >> Cases_on `cE` >> Cases_on `ce2`
3410 >> rename[`(a,sucs) ��� d_conj_set _ _`] >> rw[]
3452 rw[] >> fs[] >> CCONTR_TAC >> rw[]
3464 >> rw[] >> metis_tac[]
3479 >> rw[] >> metis_tac[MEM_EQUAL_SET]
3512 (fs[concr_min_rel_def] >> rw[])
3632 >> rw[] >> qunabbrev_tac `TRNS`
3646 >> rw[] >> fs[] >> rw[] >> fs[]
3745 >> fs[] >> rw[]
3891 >> rw[] >> fs[MEM_MAP]
3948 >> Q.HO_MATCH_ABBREV_TAC `GOAL` >> rw[]
3968 >> Cases_on `lookup id g_AA.nodeInfo` >> fs[] >> rw[]
4001 >> fs[] >> rw[] >> rename[`MEM (id,nL) (toAList g_AA.nodeInfo)`]
4103 >> fs[] >> rw[] >> fs[]
4108 >> fs[] >> rw[] >> fs[]
4132 >> fs[] >> rw[] >> fs[]
4141 qunabbrev_tac `INIT` >> rw[] >> simp[vwaa2gba_def,GBA_component_equality]
4143 >> Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (id,n) _`]
4159 rpt strip_tac >> qunabbrev_tac `INIT` >> rw[]
4162 >> Cases_on `y` >> fs[] >> rw[] >> rename[`MEM (id,n) _`]
4280 qunabbrev_tac `abstrAA` >> simp[vwaa2gba_def] >> rw[]
4322 >> Cases_on `y` >> fs[] >> qexists_tac `r` >> rw[]
4423 >> Cases_on `y` >> fs[] >> rw[]
4425 >> rw[]
4446 >> rw[] >> Cases_on `y'` >> fs[]
4459 >> rw[] >> metis_tac[MEM_toAList,MEM_EQUAL_SET]
4466 >- (qunabbrev_tac `NEW_L` >> fs[] >> rw[]
4475 >- (rw[] >> `MEM x''.frml NEW_L` suffices_by fs[]
4486 >> strip_tac >> Cases_on `y` >> rw[]
4530 >> Cases_on `y` >> fs[] >> rw[]
4532 >> rw[] >> qexists_tac `i` >> fs[]
4547 >- (fs[expandAuto_init_def] >> rw[] >> fs[MEM_MAP,CAT_OPTIONS_MEM]
4548 >> rw[] >> fs[MEM_MAP, CAT_OPTIONS_MEM]
4614 >> Cases_on `x1` >> fs[] >> rw[]
4784 >> simp[] >> rw[]
5097 >> simp[] >> rw[]