lambda/other-models/raw_syntaxScript.sml

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