Lines Matching refs:rw
260 rw [INTER_def]);
269 ] >> rw[SUBSET_def]);
497 rw[SUBSET_def]);
538 >- (rw[bad_def] >>
540 rw[] >> Cases_on `���e. f 0 = {e}` >> fs[] >>
542 >- (DISJ1_TAC >> rw[Once EXTENSION]) >>
544 first_x_assum (qspec_then `e` mp_tac) >> rw[] >>
547 CONV_TAC CONTRAPOS_CONV >> rw[] >>
558 rw[SUBSET_def]) >>
561 by (rw[Abbr`N`] >- metis_tac [SET_def] >> fs[Abbr`poor`]) >>
568 rw[Abbr`N`, SUBSET_def],
573 rw[Abbr`N`, SUBSET_def] >> metis_tac [SUBSET_def, IN_INTER]
577 by (rw[Abbr`poor`] >> match_mp_tac SUBSETS_ARE_SETS >>
579 qexists_tac `N` >> rw[bad_def] >|[
580 rw[Once EXTENSION, EQ_IMP_THM] >>
586 disch_then SUBST1_TAC >> BETA_TAC >> rw[] >> DISJ2_TAC >>
588 rw[] >>
593 >- (rw[SUBSET_def] >>
595 rw[Abbr`poor`] >> metis_tac [SUBSET_def, DECIDE ``0 + 1 = 1``]) >>
597 rw[] >> metis_tac [DECIDE ``(0 + 1 = 1) ��� (0 + 2 = 2)``],
606 rw[] >> match_mp_tac SUBSETS_ARE_SETS >> qexists_tac `x` >>
607 rw[SUBSET_def] >> metis_tac [SET_def])
623 by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM, SUBSET_def] >>
626 by (Induct >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>
632 qsuff_tac `SPEC0 (��y. ���x. x ��� ss ��� (y = x ��� a)) = w` >- rw[] >>
638 by (rw[bad_def]
640 >- rw[Abbr`m`, prim_recTheory.PRIM_REC_THM]
645 by (rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>
647 qexists_tac `x` >> rw[]
654 rw[Once EXTENSION] >> metis_tac [SET_def])) >>
658 >- (qexists_tac `b` >> rw[Abbr`m`, prim_recTheory.PRIM_REC_THM] >>