Lines Matching refs:collapse
29 collapse e_1 -->_\beta collapse e_2
35 (Where collapse is written graphically in the paper as the "round
41 The collapse function below has the important property that
43 EQC alpha x y = (collapse x = collapse y)
45 I.e., two raw syntax terms are alpha-equivalent iff they collapse
148 (collapse (var s) = VAR s) /\
149 (collapse (app t u) = collapse t @@ collapse u) /\
150 (collapse (lam v t) = LAM v (collapse t))`;
156 ``!e. FV (collapse e) = fv e``,
173 (collapse (subst (var y) x e) = [VAR y/x] (collapse e))``,
185 `~(x IN FV (collapse e))` by SRW_TAC [][] THEN
186 `~(x IN FV (LAM y (collapse e)))` by SRW_TAC [][] THEN
195 (collapse (subst u v t) = [collapse u/v] (collapse t))``,
311 ``!t u. EQC alpha t u ==> (collapse t = collapse u)``,
314 Q_TAC SUFF_TAC `!y t u. ialpha y t u ==> (collapse t = collapse u)`
384 ``!t u. (collapse t = collapse u) ==> EQC alpha t u``,
391 (!u. (collapse t = collapse u) ==> EQC alpha t u) /\
392 (LAM s (collapse t) = LAM s' (collapse t')) ==>
398 `collapse t = [VAR s/s'] (collapse t')`
400 `~(s IN FV (collapse t')) /\ ~(s' IN FV (collapse t))`
405 `collapse t' = collapse t2` by PROVE_TAC [alpha_collapse] THEN
408 `[VAR s/s'] (collapse t2) = collapse (subst (var s) s' t2)`
426 ``EQC alpha t u = (collapse t = collapse u)``,
431 ``!M. ?t. collapse t = M``,
436 ``!t u. beta t u ==> compat_closure beta (collapse t) (collapse u)``,
444 ``!t u. beta (collapse t) (collapse u) ==>
465 `collapse t0 = collapse t1` by PROVE_TAC [alpha_collapse] THEN
468 `M = [VAR v/w] (collapse t1)` by METIS_TAC [INJECTIVITY_LEMMA1] THEN
469 `~(v IN FV (collapse t1))` by METIS_TAC [LAM_INJ_ALPHA_FV] THEN
475 ?t u. (M = collapse t) /\ (N = collapse u) /\
478 `?m n. (collapse m = M) /\ (collapse n = N)`
488 `?n. collapse n = N'` by METIS_TAC [collapse_ONTO] THEN
491 `?m. collapse m = M` by METIS_TAC [collapse_ONTO] THEN
500 !t u. (M = collapse t) /\ (N = collapse u) ==>
505 `?z1 m. (t = app z1 m) /\ (collapse z1 = z) /\ (collapse m = M)`
507 `?z2 n. (u = app z2 n) /\ (collapse z2 = z) /\ (collapse n = N)`
515 `?z1 m. (t = app m z1) /\ (collapse z1 = z) /\ (collapse m = M)`
517 `?z2 n. (u = app n z2) /\ (collapse z2 = z) /\ (collapse n = N)`
535 `collapse v' = collapse w` by PROVE_TAC [EQC_alpha_collapse_EQ] THEN
536 `M = [VAR v/s] (collapse w)` by PROVE_TAC [INJECTIVITY_LEMMA1] THEN
537 `M = collapse (subst (var v) s w)` by PROVE_TAC [collapse_vsubst] THEN
543 `collapse v'' = collapse z` by PROVE_TAC [EQC_alpha_collapse_EQ] THEN
544 `N = [VAR v/s'] (collapse z)` by PROVE_TAC [INJECTIVITY_LEMMA1] THEN
545 `N = collapse (subst (var v) s' z)` by PROVE_TAC [collapse_vsubst] THEN
555 Q_TAC SUFF_TAC `~(v IN FV (collapse v'))` THEN1
580 ``compat_closure beta (collapse t) (collapse u) ==>
586 ``compat_closure beta (collapse t) (collapse u) =
604 ``onto collapse``,
609 ``kSound alpha collapse``,
615 ``kCompl alpha collapse``,
621 ``Pres collapse beta (compat_closure beta)``,
627 ``sRefl collapse beta (compat_closure beta)``,
629 `(?a1. b1 = collapse a1) /\ (?a2. b2 = collapse a2)`
648 ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta)) =
649 sRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
653 ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
660 ``Pres collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
668 MATCH_MP_TAC diagram_preservation THEN Q.EXISTS_TAC `collapse` THEN