Lines Matching refs:rw
345 (* >- (rw[] *)
367 (* rw[]) *)
450 (* >> `neg1 = []` by fs[MEM_SUBSET_SET_TO_LIST] >> rw[] *)
498 >> rw[FOLDR_LEMM5]
628 by (fs[MEM_MAP] >> qexists_tac `y` >> Cases_on `y` >> fs[] >> rw[])
686 >> `id = id2` by (rw[] >> metis_tac[])
687 >> rw[] >> metis_tac[MEM_toAList,SOME_11]
731 >> rw[] >> metis_tac[MEM_toAList,SOME_11]
763 >> fs[MEM_toAList,domain_lookup] >> rw[]
817 >- (fs[addFrmlToGraph_def] >> rw[]
825 >> fs[MEM_toAList] >> rw[] >> metis_tac[])
832 >> rw[] >> metis_tac[]
922 >> rw[] >> Cases_on `l'` >> fs[]
998 >> fs[addNode_def,lookup_insert] >> rw[]
1000 >> rw[] >> first_x_assum (qspec_then `x_id` mp_tac) >> rpt strip_tac
1045 >> Cases_on `y` >> rw[MEM_toAList]
1048 >> rw[] >> fs[MEM_toAList])
1054 >- (Cases_on `f` >> simp[addFrmlToGraph_def] >> rw[]
1063 >- (Cases_on `f` >> simp[addFrmlToGraph_def] >> rw[]
1080 >> Cases_on `node.frml` >> rw[] >> fs[]
1114 >> qexists_tac `y` >> Cases_on `y` >> fs[] >> rw[]
1132 >> fs[MEM_MAP] >> rw[]
1135 >> rw[]
1137 >> simp[] >> Cases_on `y'` >> fs[] >> rw[]
1169 >> Cases_on `y'` >> fs[] >> rw[]
1172 >> rpt strip_tac >> Cases_on `y'` >> fs[] >> rw[]
1179 >> Cases_on `y` >> fs[] >> rw[] >> CCONTR_TAC
1189 >> rw[] >> fs[lookup_insert,theorem "nodeLabelAA_component_equality"]
1191 >> rw[] >> fs[]
1254 >- (rw[]
1271 strip_tac >> rw[] >> CCONTR_TAC >> fs[]
1273 >> rw[]
1278 rw[] >> Cases_on `r.frml` >> fs[addFrmlToGraph_def,addNode_def]
1287 >> rw[]
1297 >> Cases_on `x'` >> fs[] >> rw[]
1299 strip_tac >> rw[] >> fs[] >> rw[] >> fs[]
1305 >> CCONTR_TAC >> rw[]
1327 >> rw[]
1330 CCONTR_TAC >> rw[]
1341 >> rw[] >> fs[MEM_toAList] >> rw[]
1352 >> rw[] >> `MEM x (graphStates g1)` by (CCONTR_TAC >> fs[])
1364 >- (rw[]
1378 >> fs[unique_node_formula_def] >> rw[]
1379 >> `q' = q` by metis_tac[] >> rw[]
1380 >> `r' = r` by metis_tac[MEM_toAList,SOME_11] >> rw[]
1398 >> fs[unique_node_formula_def] >> rw[]
1399 >> `q' = q` by metis_tac[] >> rw[]
1400 >> `r' = r` by metis_tac[MEM_toAList,SOME_11] >> rw[]
1403 >> rw[]
1411 >> fs[OPTION_TO_LIST_MEM] >> rw[]
1424 >> rw[]
1506 >> Cases_on `q` >> simp[addFrmlToGraph_def] >> rw[]
1525 >> rw[]
1530 >> rw[] >> fs[theorem "nodeLabelAA_component_equality"]
1535 >- (rw[] >> Cases_on `MEM f fs`
1603 >> fs[gfg_component_equality] >> rw[]
1606 >> rw[] >> metis_tac[]
1612 >> fs[gfg_component_equality] >> rw[]
1619 >> fs[gfg_component_equality] >> rw[]
1625 >> fs[gfg_component_equality] >> rw[])
1628 >> fs[gfg_component_equality] >> rw[]
1658 >> Cases_on `y` >> Cases_on `y'` >> fs[] >> rw[]
1700 >> rw[] >> `?nId nL. node = (nId,nL)` by (Cases_on `node` >> fs[])
1701 >> rw[] >> fs[]
1749 >> fs[] >> rpt strip_tac >> rw[] >> fs[]
1777 >> rw[]
1804 >> rpt strip_tac >> rw[]
1805 >> Cases_on `x_id = q` >> rw[]
1811 >> rw[] >> fs[] >> rw[]
1824 >- (rw[]
1827 >> rw[] >> fs[]
1830 >> rw[] >> Cases_on `y` >> fs[]
1839 >> rw[] >> Cases_on `x` >> fs[]
1842 >> Cases_on `h'` >> fs[] >> rw[])
1853 >- (rw[]
1856 >> rw[] >> fs[]
1870 >> rw[] >> fs[]
1874 >> rw[] >> fs[]
1878 >> rw[] >> fs[]
1882 >> rw[] >> fs[]
1886 >> rw[] >> fs[]
1891 >> rw[] >> fs[]
1917 >> Cases_on `q = id` >> rw[]
1998 >> Cases_on `q = nId` >> fs[findNode_def] >> rw[]
2006 >> `r' = frml` by metis_tac[SOME_11] >> rw[]
2007 >> rw[MEM_toAList] >> fs[gfg_component_equality] >> rw[]
2011 >> rw[] >> metis_tac[lookup_insert])
2063 >- (rw[] >> POP_ASSUM mp_tac >> POP_ASSUM mp_tac
2109 >> rw[]
2110 >> Cases_on `sucId = nId` >> fs[] >> rw[]
2125 >> Cases_on `y1` >> Cases_on `y2` >> fs[] >> rw[]
2128 >> rw[] >> qexists_tac `nId` >> fs[]
2141 >> rw[]
2158 fs[OPTION_TO_LIST_MEM] >> fs[] >> rw[] >> fs[]
2159 >> qunabbrev_tac `NEW_LAB` >> fs[] >> rw[]
2167 >> rpt strip_tac >> Cases_on `sucId = nId` >> rw[]
2223 >> `NEW_LAB = suc` by metis_tac[MEM_toAList,SOME_11] >> rw[]
2232 fs[OPTION_TO_LIST_MEM] >> fs[] >> rw[] >> fs[]
2285 >> rw[]
2287 CCONTR_TAC >> fs[findNode_def] >> rw[]
2325 >- (Cases_on `sucId = nId` >> fs[] >> rw[]
2340 >> Cases_on `sucId' = nId` >> fs[] >> rw[]
2374 >- (Cases_on `sucId = nId` >> fs[] >> rw[]
2385 >> Cases_on `sucId' = nId` >> fs[] >> rw[]
2459 >> fs[] >> rw[] >> fs[] >> qunabbrev_tac `LABEL`
2460 >> fs[theorem "edgeLabelAA_component_equality"] >> rw[]
2462 >> fs[first_flw_has_max_counter_def] >> rw[]
2528 >> fs[gfg_component_equality] >> rw[]
2538 >> rw[] >> fs[]
2560 >> rw[] >> fs[theorem "edgeLabelAA_component_equality"]
2567 >> Cases_on `n` >> rw[] >> fs[]
2633 >- (rw[] >> fs[] >> metis_tac[])
2635 >- (rw[] >> fs[] >> metis_tac[])
2667 >> rw[] >> fs[]
2726 >> CCONTR_TAC >> rw[] >> fs[MEM_toAList]
2768 >> `q1 = id` by (rw[] >> metis_tac[])
2769 >> rw[] >> fs[graphStatesWithId_def,MEM_MAP]
2779 >> rw[]
2839 >> rw[] >> fs[]
2840 >> fs[gfg_component_equality] >> rw[] >> fs[]
2845 >- (first_x_assum (qspec_then `a` mp_tac) >> simp[] >> rw[]
2874 >> qunabbrev_tac `LABEL` >> rw[]
2875 >> fs[theorem "edgeLabelAA_component_equality"] >> rw[]
2886 >> rw[] >> fs[gfg_component_equality]
2887 >> rw[] >> fs[]
2906 qunabbrev_tac `LABEL` >> rw[]
2929 >- (qunabbrev_tac `LABEL` >> rw[]
2938 (fs[findNode_def] >> rw[] >> fs[])
2939 >> rw[] >> fs[] >> rw[]
2942 >- (rw[]
2974 (fs[findNode_def] >> rw[] >> fs[])
2979 >> rpt strip_tac >> rw[]
2983 ) >> rw[]
2990 >> fs[OPTION_TO_LIST_MEM] >> rw[] >> fs[]
2992 >> rw[] >> fs[] >> rw[] >> metis_tac[]
2996 >> rw[] >> fs[]
3009 >> fs[OPTION_TO_LIST_MEM] >> rw[] >> fs[]
3011 >> rw[] >> fs[] >> rw[] >> metis_tac[]
3037 >> rw[] >> fs[] >> rw[]
3039 >> fs[gfg_component_equality] >> rw[]
3040 >- (qexists_tac `followers_old` >> fs[] >> rw[]
3046 >> fs[] >> rw[]
3050 >> qexists_tac `(nId,frml)` >> fs[] >> rw[]
3059 >> rw[] >> fs[] >> rw[] >> qexists_tac `(nId,frml)`
3065 >> fs[IN_UNION] >> Cases_on `x` >> rw[] >> fs[]
3083 >> rw[] >> fs[] >> rw[]
3087 >> rw[] >> qexists_tac `(LABEL,id)::followers_old`
3088 >> fs[] >> rw[]
3094 >> rw[] >> qexists_tac `followers_old`
3095 >> fs[] >> rw[]
3099 >- (fs[] >> rw[] >> fs[])
3106 >> rw[] >> fs[] >> rw[] >> qexists_tac `(nId,frml)`
3175 >> CCONTR_TAC >> rw[] >> fs[MEM_toAList]
3198 >> fs[MEM_MAP,CAT_OPTIONS_MAP_LEMM,CAT_OPTIONS_MEM] >> rw[]
3281 >- (rw[] >> first_x_assum (qspec_then `f` mp_tac) >> simp[] >> rpt strip_tac
3286 >> rw[IMAGE_UNION]