1open HolKernel Parse boolLib bossLib BasicProvers metisLib
2
3local open stringTheory in end
4
5open pred_setTheory binderLib boolSimps relationTheory
6open chap3Theory
7
8(* ----------------------------------------------------------------------
9
10    This theory demonstrates that the quotiented theory of
11    lambda-calculus in the rest of the development is a good model of
12    the "raw" theory of lambda calculus syntax.
13
14    The raw syntax here and the relations on it are taken from
15
16     "A formalised first-order confluence proof of for the \lambda-calculus
17      using one-sorted variable names"
18
19        by Rene Vestergaard and James Brotherston
20
21     which appeared in Information and Computation, 183:2.
22     (A pre-print of this paper is available at
23       http://www.jaist.ac.jp/~vester/Writings/vestergaard-brotherston-IandC-rta01.ps.gz)
24
25    In this paper, the "real \lambda-calculus" is established by
26    taking a quotient of raw syntax terms, and the notion of
27    beta-reduction in the real type is defined such that
28
29           collapse e_1  -->_\beta collapse e_2
30
31                 = (by defn)
32
33           e1 ==_\alpha ; -->_\beta ; ==_\alpha e2
34
35    (Where collapse is written graphically in the paper as the "round
36     down operator".  Also, in the theory below, the semi-colon is
37     replaced with the relation composition operator O.)
38
39    I show the above is a theorem of the development.
40
41    The collapse function below has the important property that
42
43      EQC alpha x y = (collapse x = collapse y)
44
45    I.e., two raw syntax terms are alpha-equivalent iff they collapse
46    to the same quotiented term.
47
48   ---------------------------------------------------------------------- *)
49
50val _ = new_theory "raw_syntax"
51
52val _ = Hol_datatype `raw_term = var of string
53                               | app of raw_term => raw_term
54                               | lam of string => raw_term`;
55
56val fv_def = Define`
57  (fv (var s) = {s}) /\
58  (fv (app t u) = fv t UNION fv u) /\
59  (fv (lam v t) = fv t DELETE v)`;
60
61val FINITE_fv = store_thm(
62  "FINITE_fv",
63  ``!t. FINITE (fv t)``,
64  Induct THEN SRW_TAC [][fv_def]);
65val _ = export_rewrites ["FINITE_fv"]
66
67val capt_def = Define`
68  (capt x (var y) = {}) /\
69  (capt x (app t u) = capt x t UNION capt x u) /\
70  (capt x (lam y t) = if ~(x = y) /\ x IN fv t then {y} UNION capt x t
71                      else {})
72`
73
74val FINITE_capt = store_thm(
75  "FINITE_capt",
76  ``!t v. FINITE (capt v t)``,
77  Induct THEN SRW_TAC [][capt_def]);
78val _ = export_rewrites ["FINITE_capt"]
79
80val capt_fv = store_thm(
81  "capt_fv",
82  ``!e x. ~(x IN fv e) ==> (capt x e = {})``,
83  Induct THEN SRW_TAC [][capt_def, fv_def]);
84val _ = export_rewrites ["capt_fv"]
85
86val subst_def = Define`
87  (subst x y (var s) = if y = s then x else var s) /\
88  (subst x y (app t u) = app (subst x y t) (subst x y u)) /\
89  (subst x y (lam v t) = if ~(y = v) /\ ~(v IN fv x) then lam v (subst x y t)
90                         else lam v t)
91`;
92
93val (ialpha_rules, ialpha_ind, ialpha_cases) = Hol_reln`
94  (!x y e.  ~(y IN capt x e UNION fv e) ==>
95            ialpha y (lam x e) (lam y (subst (var y) x e))) /\
96  (!e e' x y. ialpha y e e' ==> ialpha y (lam x e) (lam x e')) /\
97  (!e1 e1' e2 y. ialpha y e1 e1' ==> ialpha y (app e1 e2) (app e1' e2)) /\
98  (!e1 e2 e2' y. ialpha y e2 e2' ==> ialpha y (app e1 e2) (app e1 e2'))
99`;
100
101val (beta_rules, beta_ind, beta_cases) = Hol_reln`
102  (!e1 e2 x. (fv e2 INTER capt x e1 = {}) ==>
103             beta (app (lam x e1) e2) (subst e2 x e1)) /\
104  (!e e' x. beta e e' ==> beta (lam x e) (lam x e')) /\
105  (!e1 e1' e2. beta e1 e1' ==> beta (app e1 e2) (app e1' e2)) /\
106  (!e1 e2 e2'. beta e2 e2' ==> beta (app e1 e2) (app e1 e2'))
107`;
108
109val alpha_def = Define`alpha e1 e2 = ?y. ialpha y e1 e2`
110
111val renaming_sanity1 = store_thm(
112  "renaming_sanity1",
113  ``!e x. subst (var x) x e = e``,
114  Induct THEN SRW_TAC [][subst_def]);
115val _ = export_rewrites ["renaming_sanity1"]
116
117val renaming_sanity2 = store_thm(
118  "renaming_sanity2",
119  ``!e x e'. ~(x IN fv e) ==> (subst e' x e = e)``,
120  Induct THEN SRW_TAC [][subst_def, fv_def]);
121val _ = export_rewrites ["renaming_sanity2"]
122
123val RIGHT_INTER_OVER_UNION = prove(
124  ``(x UNION y) INTER z = (x INTER z) UNION (y INTER z)``,
125  SRW_TAC [][EXTENSION] THEN tautLib.TAUT_TAC)
126
127val SING_INTER = prove(
128  ``({x} INTER Y = if x IN Y then {x} else {}) /\
129    (Y INTER {x} = if x IN Y then {x} else {})``,
130  SRW_TAC [][EXTENSION] THEN PROVE_TAC []);
131
132val renaming_sanity3 = store_thm(
133  "renaming_sanity3",
134  ``!e e' x. ~(x IN fv e') /\ (capt x e INTER fv e' = {}) ==>
135             ~(x IN fv (subst e' x e))``,
136  Induct THEN
137  SRW_TAC [][capt_def, fv_def, subst_def,
138             RIGHT_INTER_OVER_UNION, SING_INTER] THEN
139  FULL_SIMP_TAC (srw_ss()) []);
140
141val renaming_sanity4 = store_thm(
142  "renaming_sanity4",
143  ``!e x y. ~(y IN fv e) ==> (subst (var x) y (subst (var y) x e) = e)``,
144  Induct THEN SRW_TAC [][fv_def, subst_def] THEN
145  SRW_TAC [][]);
146
147val collapse_def = Define`
148  (collapse (var s) = VAR s) /\
149  (collapse (app t u) = collapse t @@ collapse u) /\
150  (collapse (lam v t) = LAM v (collapse t))`;
151
152open termTheory
153
154val FV_collapse = store_thm(
155  "FV_collapse",
156  ``!e. FV (collapse e) = fv e``,
157  Induct THEN SRW_TAC [][collapse_def, fv_def]);
158val _ = export_rewrites ["FV_collapse"]
159
160val fv_vsubst = store_thm(
161  "fv_vsubst",
162  ``!e x y. ~(y IN capt x e) ==>
163            (fv (subst (var y) x e) =
164               if x IN fv e then y INSERT (fv e DELETE x)
165               else fv e)``,
166  Induct THEN
167  SRW_TAC [][fv_def, capt_def, subst_def, EXTENSION] THEN
168  FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []);
169
170val collapse_vsubst = store_thm(
171  "collapse_vsubst",
172  ``!e x y. ~(y IN capt x e)  ==>
173            (collapse (subst (var y) x e) = [VAR y/x] (collapse e))``,
174  Induct THEN
175  ASM_SIMP_TAC (srw_ss()) [collapse_def, capt_def, fv_def, subst_def,
176                           SUB_VAR, SUB_THM]
177  THENL [
178    REPEAT GEN_TAC THEN COND_CASES_TAC THEN SRW_TAC [][collapse_def],
179    MAP_EVERY Q.X_GEN_TAC [`s`, `x`, `y`] THEN
180    Cases_on `x = s` THEN ASM_SIMP_TAC (srw_ss()) [collapse_def, SUB_THM] THEN
181    Cases_on `s = y` THEN
182    ASM_SIMP_TAC (srw_ss()) [collapse_def, SUB_THM, lemma14b] THENL [
183      Cases_on `x IN fv e` THEN
184      ASM_SIMP_TAC (srw_ss()) [] THEN
185      `~(x IN FV (collapse e))` by SRW_TAC [][] THEN
186      `~(x IN FV (LAM y (collapse e)))` by SRW_TAC [][] THEN
187      SRW_TAC [][lemma14b],
188      Cases_on `x IN fv e` THEN ASM_SIMP_TAC (srw_ss()) []
189    ]
190  ]);
191
192val collapse_subst = store_thm(
193  "collapse_subst",
194  ``!t u v. (capt v t INTER fv u = {}) ==>
195            (collapse (subst u v t) = [collapse u/v] (collapse t))``,
196  Induct THEN
197  ASM_SIMP_TAC (srw_ss()) [collapse_def, capt_def, fv_def, subst_def,
198                           SUB_VAR, SUB_THM, RIGHT_INTER_OVER_UNION]
199  THENL [
200    REPEAT GEN_TAC THEN SRW_TAC [][collapse_def],
201    REPEAT GEN_TAC THEN SRW_TAC [][collapse_def, RIGHT_INTER_OVER_UNION,
202                                   SUB_THM] THEN
203    FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, SUB_THM, lemma14b]
204  ]);
205
206
207val x_IN_capt_x = store_thm(
208  "x_IN_capt_x",
209  ``!t. ~(x IN capt x t)``,
210  Induct THEN SRW_TAC [][capt_def]);
211
212val capt_subst2 = prove(
213  ``!t.
214       ~(v IN capt x t) /\ ~(v IN fv t) ==>
215       ~(x IN capt v (subst (var v) x t))``,
216  Induct THEN SRW_TAC [][capt_def, subst_def, fv_def, fv_vsubst] THEN
217  FULL_SIMP_TAC (srw_ss()) []);
218
219val ialpha_sym = store_thm(
220  "ialpha_sym",
221  ``!y t1 t2. ialpha y t1 t2 ==> ?z. ialpha z t2 t1``,
222  HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][] THENL [
223    Cases_on `x = y` THENL [
224      SRW_TAC [][renaming_sanity1] THEN
225      Q.EXISTS_TAC `x` THEN
226      Q_TAC SUFF_TAC `~(x IN fv (subst (var x) x e))` THEN
227            METIS_TAC [ialpha_rules, renaming_sanity1,
228                       pred_setTheory.IN_UNION],
229      `~(x IN fv (subst (var y) x e))`
230          by SRW_TAC [][fv_vsubst] THEN
231      Q_TAC SUFF_TAC `~(x IN capt y (subst (var y) x e))`
232            THEN1 METIS_TAC [renaming_sanity4, ialpha_rules,
233                             pred_setTheory.IN_UNION] THEN
234      SRW_TAC [][capt_subst2]
235    ],
236    METIS_TAC [ialpha_rules],
237    METIS_TAC [ialpha_rules],
238    METIS_TAC [ialpha_rules]
239  ]);
240
241val alpha_sym = store_thm(
242  "alpha_sym",
243  ``alpha x y ==> alpha y x``,
244  METIS_TAC [alpha_def, ialpha_sym]);
245
246val alpha_CONG = store_thm(
247  "alpha_CONG",
248  ``!t t'. alpha t t' ==>
249           (!u. alpha (app t u) (app t' u) /\
250                alpha (app u t) (app u t')) /\
251           (!v. alpha (lam v t) (lam v t'))``,
252  SRW_TAC [][alpha_def] THEN PROVE_TAC [ialpha_rules]);
253
254val EQC_alpha_CONG = store_thm(
255  "EQC_alpha_CONG",
256  ``!t t'. EQC alpha t t' ==>
257           (!u. EQC alpha (app t u) (app t' u) /\
258                EQC alpha (app u t) (app u t')) /\
259           (!v. EQC alpha (lam v t) (lam v t'))``,
260  HO_MATCH_MP_TAC relationTheory.EQC_INDUCTION THEN
261  SRW_TAC [][] THEN
262  PROVE_TAC [alpha_CONG, EQC_R, EQC_SYM, EQC_TRANS]);
263
264
265
266val EQC_alpha_CONG2 = store_thm(
267  "EQC_alpha_CONG2",
268  ``!t t' u u'. EQC alpha t t' /\ EQC alpha u u' ==>
269                EQC alpha (app t u) (app t' u')``,
270  METIS_TAC [EQC_alpha_CONG, EQC_TRANS]);
271
272val ialpha_lam_lemma = prove(
273  ``!y t u. ialpha y t u ==>
274            !v t0 s k t1 t2.
275               ((t = lam v t0) ==>
276                ~(u = var s) /\ ~(u = app t1 t2)) /\
277               ((u = lam v t0) ==>
278                ~(t = var s) /\ ~(t = app t1 t2))``,
279  HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][]);
280
281val ialpha_lam_thm = save_thm(
282  "ialpha_lam_thm",
283  SIMP_RULE (srw_ss() ++ DNF_ss) [] ialpha_lam_lemma)
284
285val alpha_lam_thm = store_thm(
286  "alpha_lam_thm",
287  ``(!v t0 s. ~alpha (lam v t0) (var s) /\ ~alpha (var s) (lam v t0)) /\
288    (!v t0 t1 t2.
289        ~alpha (lam v t0) (app t1 t2) /\ ~alpha (app t1 t2) (lam v t0))``,
290  METIS_TAC [alpha_def, ialpha_lam_thm]);
291val _ = export_rewrites ["alpha_lam_thm"]
292
293val EQC_alpha_lam_lemma = prove(
294  ``!t u. EQC alpha t u ==>
295          !v t0 s k t1 t2.
296               ((t = lam v t0) ==>
297                ~(u = var s) /\ ~(u = app t1 t2)) /\
298               ((u = lam v t0) ==>
299                ~(t = var s) /\ ~(t = app t1 t2))``,
300  HO_MATCH_MP_TAC EQC_INDUCTION THEN REPEAT STRIP_TAC THEN SRW_TAC [][] THEN
301  FULL_SIMP_TAC (srw_ss()) [] THEN Cases_on `t'` THEN
302  FULL_SIMP_TAC (srw_ss()) []);
303
304val EQC_alpha_lam_thm = save_thm(
305  "EQC_alpha_lam_thm",
306  SIMP_RULE (srw_ss() ++ DNF_ss) [] EQC_alpha_lam_lemma)
307val _ = export_rewrites ["EQC_alpha_lam_thm"]
308
309val alpha_collapse = store_thm(
310  "alpha_collapse",
311  ``!t u. EQC alpha t u ==> (collapse t = collapse u)``,
312  HO_MATCH_MP_TAC relationTheory.EQC_INDUCTION THEN
313  SIMP_TAC (srw_ss()) [alpha_def] THEN
314  Q_TAC SUFF_TAC `!y t u. ialpha y t u ==> (collapse t = collapse u)`
315     THEN1 PROVE_TAC [] THEN
316  HO_MATCH_MP_TAC ialpha_ind THEN
317  SIMP_TAC (srw_ss()) [collapse_def, collapse_vsubst] THEN REPEAT STRIP_TAC THEN
318  MATCH_MP_TAC SIMPLE_ALPHA THEN SRW_TAC [][]);
319
320val alpha_fv_invariant = store_thm(
321  "alpha_fv_invariant",
322  ``!t u. EQC alpha t u ==> (fv t = fv u)``,
323  HO_MATCH_MP_TAC EQC_INDUCTION THEN SIMP_TAC (srw_ss()) [alpha_def] THEN
324  Q_TAC SUFF_TAC `!y t u. ialpha y t u ==> (fv t = fv u)`
325     THEN1 PROVE_TAC [] THEN
326  HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][fv_def, fv_vsubst] THEN
327  SRW_TAC [][EXTENSION] THEN PROVE_TAC []);
328
329val capt_subst = store_thm(
330  "capt_subst",
331  ``!t x y z. ~(x = y) /\ ~(y IN capt z t) ==>
332              (capt x (subst (var y) z t) =
333                 if x = z then {} else capt x t)``,
334  Induct THEN SRW_TAC [][subst_def, capt_def, fv_def, fv_vsubst] THEN
335  FULL_SIMP_TAC (srw_ss()) []);
336
337val alpha_eq_safe_subst = store_thm(
338  "alpha_eq_safe_subst",
339  ``!t. ?t'. EQC alpha t t' /\ (capt x t' INTER fv u = {})``,
340  Induct THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
341    Q.X_GEN_TAC `s` THEN Q.EXISTS_TAC `var s` THEN SRW_TAC [][capt_def],
342    Q.EXISTS_TAC `app t'' t'''` THEN
343    SRW_TAC [][capt_def, RIGHT_INTER_OVER_UNION] THEN
344    METIS_TAC [EQC_alpha_CONG2],
345    Q.X_GEN_TAC `s` THEN
346    Cases_on `x IN fv t` THENL [
347      Cases_on `s IN fv u` THENL [
348        Q_TAC (NEW_TAC "z")
349              `fv t UNION fv u UNION {s;x} UNION capt s t'` THEN
350        Q.EXISTS_TAC `lam z (subst (var z) s t')` THEN
351        CONJ_TAC THENL [
352          MATCH_MP_TAC EQC_TRANS THEN
353          Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [
354            PROVE_TAC [EQC_alpha_CONG],
355            MATCH_MP_TAC EQC_R THEN
356            SRW_TAC [][alpha_def] THEN Q.EXISTS_TAC `z` THEN
357            MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN
358            SRW_TAC [][] THEN PROVE_TAC [alpha_fv_invariant]
359          ],
360          SRW_TAC [][capt_def, capt_subst, RIGHT_INTER_OVER_UNION, SING_INTER]
361        ],
362        Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [
363          PROVE_TAC [EQC_alpha_CONG],
364          SRW_TAC [][capt_def, RIGHT_INTER_OVER_UNION, SING_INTER]
365        ]
366      ],
367      Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [
368        PROVE_TAC [EQC_alpha_CONG],
369        SRW_TAC [][capt_def] THEN PROVE_TAC [alpha_fv_invariant]
370      ]
371    ]
372  ]);
373
374val LAM_INJ_ALPHA_FV = prove(
375  ``~(v1 = v2) /\ (LAM v1 t1 = LAM v2 t2) ==>
376    ~(v1 IN FV t2) /\ ~(v2 IN FV t1)``,
377  SRW_TAC [][LAM_eq_thm] THEN SRW_TAC [][]);
378val INJECTIVITY_LEMMA1 = prove(
379  ``(LAM v1 t1 = LAM v2 t2) ==> (t1 = [VAR v1/v2]t2)``,
380  SRW_TAC [][LAM_eq_thm] THEN SRW_TAC [][fresh_tpm_subst]);
381
382val collapse_alpha = store_thm(
383  "collapse_alpha",
384  ``!t u. (collapse t = collapse u) ==> EQC alpha t u``,
385  Induct THEN REPEAT GEN_TAC THEN Cases_on `u` THEN
386  SRW_TAC [][collapse_def] THENL [
387    PROVE_TAC [EQC_alpha_CONG2],
388    REPEAT (POP_ASSUM MP_TAC) THEN
389    Q_TAC SUFF_TAC
390      `!t s s' t'.
391          (!u. (collapse t = collapse u) ==> EQC alpha t u) /\
392          (LAM s (collapse t) = LAM s' (collapse t')) ==>
393          EQC alpha (lam s t) (lam s' t')` THEN1 METIS_TAC [] THEN
394    REPEAT STRIP_TAC THEN
395    Cases_on `s = s'` THENL [
396      FULL_SIMP_TAC (srw_ss()) [] THEN
397      METIS_TAC [EQC_alpha_CONG],
398      `collapse t = [VAR s/s'] (collapse t')`
399        by PROVE_TAC [INJECTIVITY_LEMMA1] THEN
400      `~(s IN FV (collapse t')) /\ ~(s' IN FV (collapse t))`
401        by PROVE_TAC [LAM_INJ_ALPHA_FV] THEN
402      MATCH_MP_TAC EQC_TRANS THEN
403      `?t2. EQC alpha t' t2 /\ (capt s' t2 INTER fv (var s) = {})`
404         by PROVE_TAC [alpha_eq_safe_subst] THEN
405      `collapse t' = collapse t2` by PROVE_TAC [alpha_collapse] THEN
406      `~(s IN capt s' t2)`
407          by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] THEN
408      `[VAR s/s'] (collapse t2) = collapse (subst (var s) s' t2)`
409         by METIS_TAC [collapse_vsubst] THEN
410      `EQC alpha t (subst (var s) s' t2)` by METIS_TAC [] THEN
411      `EQC alpha (lam s t) (lam s (subst (var s) s' t2))`
412         by METIS_TAC [EQC_alpha_CONG] THEN
413      `EQC alpha (lam s (subst (var s) s' t2)) (lam s' t2)`
414         by (MATCH_MP_TAC EQC_SYM THEN
415             MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN
416             Q.EXISTS_TAC `s` THEN
417             MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN
418             FULL_SIMP_TAC (srw_ss()) [] THEN
419             PROVE_TAC [alpha_fv_invariant]) THEN
420      PROVE_TAC [EQC_TRANS, EQC_SYM, EQC_alpha_CONG]
421    ]
422  ]);
423
424val EQC_alpha_collapse_EQ = store_thm(
425  "EQC_alpha_collapse_EQ",
426  ``EQC alpha t u = (collapse t = collapse u)``,
427  PROVE_TAC [collapse_alpha, alpha_collapse]);
428
429val collapse_ONTO = store_thm(
430  "collapse_ONTO",
431  ``!M. ?t. collapse t = M``,
432  HO_MATCH_MP_TAC simple_induction THEN METIS_TAC [collapse_def]);
433
434val beta_ccbeta = store_thm(
435  "beta_ccbeta",
436  ``!t u. beta t u ==> compat_closure beta (collapse t) (collapse u)``,
437  HO_MATCH_MP_TAC beta_ind THEN
438  SRW_TAC [][compat_closure_rules, collapse_def] THEN
439  SRW_TAC [][collapse_subst, INTER_COMM] THEN
440  SRW_TAC [][cc_beta_thm] THEN PROVE_TAC []);
441
442val gmbeta_beta = store_thm(
443  "gmbeta_beta",
444  ``!t u. beta (collapse t) (collapse u) ==>
445          (EQC alpha O beta O EQC alpha) t u``,
446  SIMP_TAC (srw_ss()) [beta_def, O_DEF] THEN REPEAT GEN_TAC THEN
447  DISCH_THEN (Q.X_CHOOSE_THEN `v`
448               (Q.X_CHOOSE_THEN `M`
449                 (Q.X_CHOOSE_THEN `N` STRIP_ASSUME_TAC))) THEN
450  `?f x. t = app f x`
451     by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
452  POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN
453  `?w t0. f = lam w t0`
454     by (Cases_on `f` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
455  POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN
456  `?t1. EQC alpha t0 t1 /\ (capt w t1 INTER fv x = {})`
457     by PROVE_TAC [alpha_eq_safe_subst] THEN
458  `EQC alpha (app (lam w t0) x) (app (lam w t1) x)`
459     by METIS_TAC [EQC_alpha_CONG] THEN
460  `beta (app (lam w t1) x) (subst x w t1)`
461     by (MATCH_MP_TAC  (hd (CONJUNCTS beta_rules)) THEN
462         FULL_SIMP_TAC (srw_ss()) [INTER_COMM]) THEN
463  Q_TAC SUFF_TAC `EQC alpha (subst x w t1) u` THEN1 PROVE_TAC [] THEN
464  ASM_SIMP_TAC (srw_ss()) [EQC_alpha_collapse_EQ, collapse_subst] THEN
465  `collapse t0 = collapse t1` by PROVE_TAC [alpha_collapse] THEN
466  POP_ASSUM SUBST_ALL_TAC THEN
467  Cases_on `v = w` THEN1 FULL_SIMP_TAC (srw_ss()) [] 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
470  SRW_TAC [][lemma15a]);
471
472val beta_some_reflected = store_thm(
473  "beta_some_reflected",
474  ``!M N. compat_closure beta M N ==>
475          ?t u. (M = collapse t) /\ (N = collapse u) /\
476                beta t u``,
477  HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THENL [
478    `?m n. (collapse m = M) /\ (collapse n = N)`
479       by METIS_TAC [collapse_ONTO] THEN
480    `?m'. EQC alpha m m' /\ (capt v m' INTER fv n = {})`
481       by METIS_TAC [alpha_eq_safe_subst] THEN
482    MAP_EVERY Q.EXISTS_TAC [`app (lam v m') n`, `subst n v m'`] THEN
483    SRW_TAC [][collapse_def, GSYM EQC_alpha_collapse_EQ, collapse_subst]
484    THENL [
485      METIS_TAC [EQC_alpha_collapse_EQ],
486      METIS_TAC [INTER_COMM, beta_rules]
487    ],
488    `?n. collapse n = N'` by METIS_TAC [collapse_ONTO] THEN
489    MAP_EVERY Q.EXISTS_TAC [`app t n`, `app u n`] THEN
490    SRW_TAC [][collapse_def, beta_rules],
491    `?m. collapse m = M` by METIS_TAC [collapse_ONTO] THEN
492    MAP_EVERY Q.EXISTS_TAC [`app m t`, `app m u`] THEN
493    SRW_TAC [][collapse_def, beta_rules],
494    MAP_EVERY Q.EXISTS_TAC [`lam v t`, `lam v u`] THEN
495    SRW_TAC [][collapse_def, beta_rules]
496  ]);
497
498val ccbeta_beta_lemma = prove(
499  ``!M N. compat_closure beta M N ==>
500          !t u. (M = collapse t) /\ (N = collapse u) ==>
501                (EQC alpha O beta O EQC alpha) t u``,
502  HO_MATCH_MP_TAC compat_closure_ind THEN
503  REPEAT STRIP_TAC THEN1 METIS_TAC [gmbeta_beta] THEN
504  FULL_SIMP_TAC (srw_ss()) [O_DEF] THENL [
505    `?z1 m. (t = app z1 m) /\ (collapse z1 = z) /\ (collapse m = M)`
506       by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
507    `?z2 n. (u = app z2 n) /\ (collapse z2 = z) /\ (collapse n = N)`
508       by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
509    `?y1 y2. EQC alpha m y1 /\ beta y1 y2 /\ EQC alpha y2 n`
510       by METIS_TAC [] THEN
511    `EQC alpha (app z1 m) (app z1 y1)` by METIS_TAC [EQC_alpha_CONG] THEN
512    `beta (app z1 y1) (app z1 y2)` by METIS_TAC [beta_rules] THEN
513    METIS_TAC [EQC_alpha_CONG2, EQC_alpha_collapse_EQ],
514
515    `?z1 m. (t = app m z1) /\ (collapse z1 = z) /\ (collapse m = M)`
516      by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
517    `?z2 n. (u = app n z2) /\ (collapse z2 = z) /\ (collapse n = N)`
518      by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
519    `?y1 y2. EQC alpha m y1 /\ beta y1 y2 /\ EQC alpha y2 n`
520      by METIS_TAC [] THEN
521    `EQC alpha (app m z1) (app y1 z1)` by METIS_TAC [EQC_alpha_CONG] THEN
522    `beta (app y1 z1) (app y2 z1)` by METIS_TAC [beta_rules] THEN
523    METIS_TAC [EQC_alpha_CONG2, EQC_alpha_collapse_EQ],
524
525    `?s v'. (t = lam s v')`
526       by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
527    POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN
528    `?s' v''. (u = lam s' v'')`
529       by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN
530    POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN
531    `?w. EQC alpha v' w /\ (capt s w INTER fv (var v) = {})`
532       by PROVE_TAC [alpha_eq_safe_subst] THEN
533    `~(v IN capt s w)`
534       by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] THEN
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
538
539    `?z. EQC alpha v'' z /\ (capt s' z INTER fv (var v) = {})`
540       by PROVE_TAC [alpha_eq_safe_subst] THEN
541    `~(v IN capt s' z)`
542       by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] 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
546    `?a b. EQC alpha (subst (var v) s w) a /\ beta a b /\
547           EQC alpha b (subst (var v) s' z)` by PROVE_TAC [] THEN
548    `EQC alpha (lam s w) (lam v (subst (var v) s w))`
549        by (Cases_on `s = v` THEN1
550              SRW_TAC [][renaming_sanity1] THEN
551            MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN
552            Q.EXISTS_TAC `v` THEN
553            MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN
554            ASM_SIMP_TAC (srw_ss()) [] THEN
555            Q_TAC SUFF_TAC `~(v IN FV (collapse v'))` THEN1
556                  PROVE_TAC [alpha_fv_invariant, FV_collapse] THEN
557            PROVE_TAC [LAM_INJ_ALPHA_FV]) THEN
558    `EQC alpha (lam s v') (lam s w)` by PROVE_TAC [EQC_alpha_CONG] THEN
559    `EQC alpha (lam v (subst (var v) s w)) (lam v a)`
560       by PROVE_TAC [EQC_alpha_CONG] THEN
561    `EQC alpha (lam s v') (lam v a)` by PROVE_TAC [EQC_TRANS] THEN
562    `beta (lam v a) (lam v b)` by PROVE_TAC [beta_rules] THEN
563    `EQC alpha (lam v b) (lam v (subst (var v) s' z))`
564       by PROVE_TAC [EQC_alpha_CONG] THEN
565    `EQC alpha (lam v (subst (var v) s' z)) (lam s' z)`
566       by (Cases_on `s' = v` THEN1 SRW_TAC [][renaming_sanity1] THEN
567           MATCH_MP_TAC EQC_SYM THEN
568           MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN
569           Q.EXISTS_TAC `v` THEN
570           MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN
571           ASM_SIMP_TAC (srw_ss()) [] THEN
572           PROVE_TAC [LAM_INJ_ALPHA_FV, alpha_fv_invariant, FV_collapse]) THEN
573    `EQC alpha (lam s' z) (lam s' v'')`
574       by PROVE_TAC [EQC_alpha_CONG, EQC_SYM] THEN
575    PROVE_TAC [EQC_TRANS]
576  ]);
577
578val ccbeta_beta = store_thm(
579  "ccbeta_beta",
580  ``compat_closure beta (collapse t) (collapse u) ==>
581    (EQC alpha O beta O EQC alpha) t u``,
582  PROVE_TAC [SIMP_RULE (bool_ss ++ DNF_ss) [] ccbeta_beta_lemma]);
583
584val ccbeta_beta_EQ = store_thm(
585  "ccbeta_beta_EQ",
586  ``compat_closure beta (collapse t) (collapse u) =
587    (EQC alpha O beta O EQC alpha) t u``,
588  EQ_TAC THENL [
589    PROVE_TAC [ccbeta_beta],
590    SRW_TAC [][O_DEF] THEN
591    PROVE_TAC [alpha_collapse, beta_ccbeta]
592  ]);
593
594(* ----------------------------------------------------------------------
595    having established this much, confluence results about the
596    quotiented type can be transferred to the raw type, using the abstract
597    machinery from diagsTheory
598   ---------------------------------------------------------------------- *)
599
600open diagsTheory
601
602val onto_collapse = store_thm(
603  "onto_collapse",
604  ``onto collapse``,
605  SRW_TAC [][onto_def, collapse_ONTO]);
606
607val kSound_collapse = store_thm(
608  "kSound_collapse",
609  ``kSound alpha collapse``,
610  SIMP_TAC (srw_ss()) [kSound_def] THEN
611  METIS_TAC [EQC_alpha_collapse_EQ, EQC_R]);
612
613val kCompl_collapse = store_thm(
614  "kCompl_collapse",
615  ``kCompl alpha collapse``,
616  SRW_TAC [][kCompl_def] THEN
617  METIS_TAC [EQC_alpha_collapse_EQ, EQC_R]);
618
619val Pres_collapse = store_thm(
620  "Pres_collapse",
621  ``Pres collapse beta (compat_closure beta)``,
622  SRW_TAC [][O_DEF, ccbeta_beta_EQ, Pres_def] THEN
623  METIS_TAC [EQC_REFL]);
624
625val sRefl_collapse = store_thm(
626  "sRefl_collapse",
627  ``sRefl collapse beta (compat_closure beta)``,
628  SRW_TAC [][sRefl_def] THEN
629  `(?a1. b1 = collapse a1) /\ (?a2. b2 = collapse a2)`
630    by METIS_TAC [collapse_ONTO] THEN
631  FULL_SIMP_TAC (srw_ss()) [ccbeta_beta_EQ, O_DEF] THEN
632  METIS_TAC [alpha_collapse]);
633
634
635val ofree_alpha = store_thm(
636  "ofree_alpha",
637  ``ofree alpha``,
638  REWRITE_TAC [ofree_def] THEN
639  HO_MATCH_MP_TAC EQC_INDUCTION THEN REPEAT CONJ_TAC THENL [
640    METIS_TAC [RTC_RULES],
641    METIS_TAC [RTC_RULES],
642    METIS_TAC [TC_RC_EQNS, alpha_sym, symmetric_RC, symmetric_TC,
643               symmetric_def],
644    METIS_TAC [RTC_RTC]
645  ]);
646
647val aRefl_eq_sRefl_lambda = prove(
648  ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta)) =
649    sRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
650  METIS_TAC [onto_collapse, kCompl_collapse, ofree_alpha, note_lemma9]);
651
652val aRefl_collapse_RTC = prove(
653  ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
654  REWRITE_TAC [aRefl_eq_sRefl_lambda] THEN
655  METIS_TAC [note_prop10_1, sRefl_collapse, onto_collapse, kCompl_collapse,
656             ofree_alpha]);
657
658val Pres_collapse_RTC = store_thm(
659  "Pres_collapse_RTC",
660  ``Pres collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``,
661  SRW_TAC [][onto_collapse, Pres_structure_RTC, Pres_collapse,
662             kSound_collapse]);
663
664val collapse_preserves_diagrams = store_thm(
665  "collapse_preserves_diagrams",
666  ``!Fa G. eval Fa G (\i. RTC (beta RUNION alpha)) =
667           eval Fa G (\i. RTC (compat_closure beta))``,
668  MATCH_MP_TAC diagram_preservation THEN Q.EXISTS_TAC `collapse` THEN
669  SRW_TAC [][aRefl_collapse_RTC, Pres_collapse_RTC, onto_collapse]);
670
671val raw_diamond = store_thm(
672  "raw_diamond",
673  ``diamond (RTC (beta RUNION alpha))``,
674  SRW_TAC [][GSYM diamond_eval, collapse_preserves_diagrams] THEN
675  SRW_TAC [][diamond_eval] THEN
676  METIS_TAC [chap3Theory.beta_CR, chap3Theory.CR_def]);
677
678val _ = export_theory();
679