Lines Matching refs:swap
46 ``!i j. bijection (swap i j)``,
468 (apply (swap i j) s = s)``,
584 \\ Q.EXISTS_TAC `b' o swap i' (k (fresh h))`
587 \\ ASM_SIMP_TAC bool_ss [METIS_PROVE [swap_def] ``!i k. swap i k i = k``]
596 \\ `(MAP b' (MAP (swap i' (k (fresh h))) t) = t2::ts)` by
652 \\ `swap i' (k (fresh h)) o swap i' (k (fresh h)) = I` by METIS_TAC [swap_swap]
654 \\ (ASSUME_TAC o UNDISCH_ALL o Q.SPECL [`swap i' (k (fresh h))`,`swap i' (k (fresh h))`]) apply_INSERT
656 \\ `swap i' (k (fresh h)) (k (fresh h)) = i'` by SIMP_TAC bool_ss [swap_def]
666 \\ `swap i' (k (fresh h)) h' = h'` by FULL_SIMP_TAC bool_ss [swap_def]
667 \\ `swap i' (k (fresh h)) h'' = h''` by FULL_SIMP_TAC bool_ss [swap_def]
689 \\ Q.PAT_X_ASSUM `apply (swap i' (k (fresh h))) xxx (x,y,z,d')`
692 \\ `basic_abs m' (swap i' (k (fresh h)) x,swap i' (k (fresh h)) y,
693 swap i' (k (fresh h)) z,d')` by METIS_TAC []
698 \\ Q.ABBREV_TAC `sx = swap i' (k ff) x`
699 \\ Q.ABBREV_TAC `sy = swap i' (k ff) y`
700 \\ Q.ABBREV_TAC `sz = swap i' (k ff) z`