triangular/nominal/nunifPropsScript.sml

48   (a1 ��� a2 ��� fresh fcs a1 t2 ���
49    equiv fcs t1 (apply_pi [(a1,a2)] t2) ���
50    equiv fcs (Tie a1 t1) (Tie a2 t2)) ���
79 Q.PAT_X_ASSUM `a ��� a1` ASSUME_TAC THEN
82 POP_ASSUM (Q.SPEC_THEN `REVERSE [(a1,a2)]` MP_TAC) THEN
119   `equiv fe (apply_pi [(a2,a1)] (apply_pi [(a1,a2)] t2)) (apply_pi [(a2,a1)] t1)`
123   Q.EXISTS_TAC `[(a1,a2)] �� t2` THEN
125   POP_ASSUM (Q.SPEC_THEN `[(a1,a2)]` MP_TAC) THEN
189   Cases_on `a1 = lswapstr pi2 a` THEN SRW_TAC [][] THEN
190   FIRST_X_ASSUM (Q.SPECL_THEN [`pi1 ++ (REVERSE pi2)`,`[(a1,a2)]`,`lswapstr pi2 a`] MP_TAC) THEN
232     Cases_on `lswapstr pi a1 = a1` THEN1 METIS_TAC [fresh_apply_pi] THEN
233     Cases_on `lswapstr (REVERSE pi) a1 = a1` THEN1 (
239     `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi pi t2))`
241     FIRST_X_ASSUM (Q.SPEC_THEN `(a1,a2)::pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN
245   Cases_on `lswapstr pi a2 = a1` THEN
247     `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi [(a2,a1)] (apply_pi pi t2)))`
249     FIRST_X_ASSUM (Q.SPEC_THEN `pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN
252   `fresh fe a1 (apply_pi [(a2,lswapstr pi a2)] (apply_pi pi t2))`
254   `fresh fe (lswapstr (REVERSE [(a2,lswapstr pi a2)]) a1) (apply_pi pi t2)`
256   Q.PAT_X_ASSUM `lswapstr pi a2 ��� a1` ASSUME_TAC THEN
257   Q.PAT_X_ASSUM `a1 ��� a2` ASSUME_TAC THEN
259   FIRST_X_ASSUM (Q.SPEC_THEN `(a1,lswapstr pi a2)::pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN
270   Cases_on `a = a1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
272   Cases_on `a1 = lswapstr pi a` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
322   Cases_on `a2' = a1` THEN ASM_SIMP_TAC (srw_ss()) [] THEN1 (
324     `equiv fe ([(a1,a2)] �� t2) ([(a1,a2)] �� ([(a2,a1)] �� t2'))`
333     `fresh fe (lswapstr [(a2,a3)] a1) (apply_pi [(a2,a3)] t2)`
337   `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi [(a2,a3)] t3))`
339   `dis_set [(a1,a3)] [(a1,a2);(a2,a3)] = {a1;a2}`
341       Cases_on `x = a1` THEN SRW_TAC [][] THEN
345   `equiv fe (apply_pi [(a1,a2);(a2,a3)] t3) (apply_pi [(a1,a3)] t3)`
347   `equiv fe (apply_pi [(a1,a2)] t2)
348             (apply_pi ([(a1,a3)] ++ (REVERSE [(a1,a2);(a2,a3)]))
349                       (apply_pi [(a1,a2);(a2,a3)] t3))` by
1943 `equiv fe (Tie a1 t1) (Tie a2 t2) ��� a1 ��� a2 ���
1944  ���fcs. (term_fcs a1 t2 = SOME fcs) ��� fcs SUBSET fe`,
1946 Cases_on `term_fcs a1 t2` THEN1 (
2180   POP_ASSUM (Q.SPEC_THEN `REVERSE [(a1,a2)]` MP_TAC) THEN
2305   (equiv_fcs (Tie a1 t1) (Tie a2 t2) =
2306      if a1 = a2 then equiv_fcs t1 t2
2307      else OPTION_MAP2 $UNION (term_fcs a1 t2)
2308                              (equiv_fcs t1 (apply_pi [(a1,a2)] t2))) ���
2388   Q.PAT_X_ASSUM `a1 ��� a2` ASSUME_TAC THEN
2557   Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie a1 c1` THEN
2568      Q.INST [`s`|->`sxx`,`t`|->`nwalk* s c2`,`b`|->`a1`,`a`|->`b`,
2681   Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t1 = Tie a1 (nwalk* s c1)` THEN
2683   FIRST_X_ASSUM (Q.SPECL_THEN [`c1`,`apply_pi [(a1,a2)] c2`,`s`] MP_TAC) THEN
2695     MAP_EVERY Q.EXISTS_TAC [`nwalk* s c2`,`a1`] THEN
3098   Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie a1 c1` THEN
3100   Cases_on `a1 = a2` THEN SRW_TAC [][] THEN1 (
3107   `���fe0. term_fcs a1 (nwalk* s c2) = SOME fe0`
3111   `���fe1. nunify (s,fe0) c1 (apply_pi [(a1,a2)] c2) = SOME (sx,fe1)`
3115     POP_ASSUM (Q.SPECL_THEN [`apply_pi [(a1,a2)] c2`,`c1`] STRIP_ASSUME_TAC) THEN
3125     MAP_EVERY Q.EXISTS_TAC [`{}`,`c1`,`apply_pi [(a1,a2)] c2`,`fv`] THEN
3127     `fresh fe2 a1 (nwalk* s2 (nwalk* sx c2))`
3129     `���fcs4. (term_fcs a1 (nwalk* s2 (nwalk* sx c2)) = SOME fcs4) ��� fcs4 ��� fe2` by
3132     `���fcs3. (term_fcs a1 (nwalk* sx (nwalk* s c2)) = SOME fcs3)` by