1open HolKernel boolLib Parse bossLib BasicProvers
2
3open pred_setTheory
4
5open binderLib
6
7open nomsetTheory labelledTermsTheory termTheory chap3Theory
8
9val _ = new_theory "chap11_1";
10
11fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n]
12
13(* ----------------------------------------------------------------------
14    phi function for reducing all labelled redexes
15   ---------------------------------------------------------------------- *)
16
17val (phi_thm, _) =
18    define_recursive_term_function'
19      (SIMP_CONV (srw_ss()) [tpm_subst, fresh_tpm_subst, GSYM SIMPLE_ALPHA,
20                             lemma15a])
21      `(phi (VAR s) = VAR s : term) /\
22       (phi (M @@ N) = phi M @@ phi N) /\
23       (phi (LAM v M) = LAM v (phi M)) /\
24       (phi (LAMi n v M N) = [phi N/v] (phi M))`
25val _ = export_rewrites ["phi_thm"]
26
27val FV_phi = store_thm(
28  "FV_phi",
29  ``!M. v IN FV (phi M) ==> v IN FV M``,
30  HO_MATCH_MP_TAC lterm_bvc_induction THEN
31  Q.EXISTS_TAC `{v}` THEN SRW_TAC [][] THENL [
32    METIS_TAC [],
33    METIS_TAC [],
34    FULL_SIMP_TAC (srw_ss()) [FV_SUB] THEN METIS_TAC [IN_UNION, IN_DELETE]
35  ]);
36
37val NOT_IN_lSUB_I = Store_Thm(
38  "NOT_IN_lSUB_I",
39  ``���M:lterm. v ��� FV N ��� v ��� u ��� v ��� FV M ==> v ��� FV ([N/u]M)``,
40  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `FV N ��� {u;v}` THEN
41  SRW_TAC [][lSUB_VAR]);
42
43val phi_vsubst_commutes = store_thm(
44  "phi_vsubst_commutes",
45  ``!M. phi ([VAR v/u] M) = [VAR v/u] (phi M)``,
46  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `{u;v}` THEN
47  SRW_TAC [][SUB_THM, SUB_VAR] THEN
48  SRW_TAC [][chap2Theory.substitution_lemma]);
49
50
51(* ----------------------------------------------------------------------
52    strip_label : removing all labels and dropping into :term
53   ---------------------------------------------------------------------- *)
54
55val _ = augment_srw_ss [
56  simpLib.name_ss "alphas" (rewrites [GSYM tpm_ALPHA, GSYM ltpm_ALPHA])
57]
58
59val (strip_label_thm,_) = define_recursive_term_function
60  `(strip_label (VAR s) = VAR s : term) /\
61   (strip_label (M @@ N) = strip_label M @@ strip_label N) /\
62   (strip_label (LAM v M) = LAM v (strip_label M)) /\
63   (strip_label (LAMi n v M N) = (LAM v (strip_label M) @@ strip_label N))`
64val _ = export_rewrites ["strip_label_thm"]
65
66val FV_strip_label = Store_Thm(
67  "FV_strip_label",
68  ``!M. FV (strip_label M) = FV M``,
69  HO_MATCH_MP_TAC simple_lterm_induction THEN SRW_TAC [][]);
70
71val strip_label_vsubst_commutes = store_thm(
72  "strip_label_vsubst_commutes",
73  ``!M. [VAR u/v] (strip_label M) = strip_label ([VAR u/v] M)``,
74  HO_MATCH_MP_TAC lterm_bvc_induction THEN
75  Q.EXISTS_TAC `{u;v}` THEN SRW_TAC [][SUB_THM, SUB_VAR]);
76
77val strip_label_eq_lam = store_thm(
78  "strip_label_eq_lam",
79  ``(strip_label M = LAM v t) =
80        ?t'. (M = LAM v t') /\ (strip_label t' = t)``,
81  Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN
82  SRW_TAC [][LAM_eq_thm, lLAM_eq_thm, EQ_IMP_THM,
83             tpm_eqr, ltpm_eqr] THEN
84  FULL_SIMP_TAC (srw_ss()) [tpm_eqr, ltpm_eqr]);
85
86val strip_label_eq_redex = store_thm(
87  "strip_label_eq_redex",
88  ``(strip_label M = LAM v t @@ u) <=>
89         (?t' u'. (M = LAM v t' @@ u') /\ (strip_label t' = t) /\
90                  (strip_label u' = u)) \/
91         (?n t' u'. (M = LAMi n v t' u') /\
92                    (strip_label t' = t) /\
93                    (strip_label u' = u))``,
94  Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN
95  SRW_TAC [][strip_label_eq_lam] THENL [
96    METIS_TAC [],
97    SRW_TAC [][lLAMi_eq_thm, EQ_IMP_THM, LAM_eq_thm] THENL [
98      FULL_SIMP_TAC (srw_ss()) [ltpm_eqr, tpm_eqr] THEN
99      SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [],
100      SRW_TAC [][tpm_eqr]
101    ]
102  ]);
103
104val strip_label_subst = store_thm(
105  "strip_label_subst",
106  ``!M. strip_label ([N/v] M) = [strip_label N/v] (strip_label M)``,
107  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `v INSERT FV N` THEN
108  SRW_TAC [][SUB_THM, SUB_VAR]);
109
110(* ----------------------------------------------------------------------
111    null_labelling, from :term  to  :lterm
112   ---------------------------------------------------------------------- *)
113
114val (null_labelling_thm,_) = define_recursive_term_function`
115  (null_labelling (VAR s : term) = VAR s : lterm) /\
116  (null_labelling (M @@ N) = null_labelling M @@ null_labelling N) /\
117  (null_labelling (LAM v M) = LAM v (null_labelling M))`
118val _ = export_rewrites ["null_labelling_thm"]
119
120val _ = diminish_srw_ss ["alphas"]
121
122val FV_null_labelling = Store_Thm(
123  "FV_null_labelling",
124  ``!M. FV (null_labelling M) = FV M``,
125  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
126
127val null_labelling_subst = store_thm(
128  "null_labelling_subst",
129  ``!M. null_labelling ([N/v] M) = [null_labelling N/v] (null_labelling M)``,
130  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN
131  SRW_TAC [][SUB_THM, SUB_VAR]);
132
133val strip_null_labelling = Store_Thm(
134  "strip_null_labelling",
135  ``!M. strip_label (null_labelling M) = M``,
136  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
137
138val phi_null_labelling = Store_Thm(
139  "phi_null_labelling",
140  ``!M. phi (null_labelling M) = M``,
141  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
142
143(* ----------------------------------------------------------------------
144    substitution lemma
145   ---------------------------------------------------------------------- *)
146
147val christians_lemma = prove(
148  ``!L: lterm. ~(x IN FV L) /\ ~(x IN FV N) ==> ~(x IN FV ([N/v] L))``,
149  HO_MATCH_MP_TAC lterm_bvc_induction THEN
150  Q.EXISTS_TAC `{x;v} UNION FV N` THEN
151  SRW_TAC [][lSUB_VAR]);
152
153
154val lSUBSTITUTION_LEMMA = store_thm(
155  "lSUBSTITUTION_LEMMA",
156  ``!M:lterm. ~(v = x) /\ ~(v IN FV L) ==>
157              ([L/x] ([N/v] M) = [[L/x] N/v] ([L/x] M))``,
158  HO_MATCH_MP_TAC lterm_bvc_induction THEN
159  Q.EXISTS_TAC `{v;x} UNION FV L UNION FV N` THEN
160  SRW_TAC [][lSUB_VAR, l14b, FV_SUB, christians_lemma]);
161
162val ltpm_subst = store_thm(
163  "ltpm_subst",
164  ``!M. ltpm p ([N/v]M) = [ltpm p N/lswapstr p v] (ltpm p M)``,
165  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `v INSERT FV N` THEN
166  SRW_TAC [][lSUB_VAR]);
167
168val l14c = store_thm(
169  "l14c",
170  ``!M:lterm. x IN FV M ==> (FV ([N/x]M) = FV N UNION (FV M DELETE x))``,
171  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `x INSERT FV N` THEN
172  SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
173    Cases_on `x IN FV M'` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN
174    SRW_TAC [][] THEN METIS_TAC [],
175    Cases_on `x IN FV M` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN
176    SRW_TAC [][] THEN METIS_TAC [],
177    SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] THEN METIS_TAC [],
178    Cases_on `x IN FV M'` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN
179    SRW_TAC [][] THEN METIS_TAC [],
180    Cases_on `x IN FV M` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN
181    SRW_TAC [][] THEN METIS_TAC []
182  ]);
183
184val lFV_SUB = store_thm(
185  "lFV_SUB",
186  ``FV ([N/v]M:lterm) = if v IN FV M then FV N UNION (FV M DELETE v)
187                        else FV M``,
188  METIS_TAC [l14c, l14b]);
189
190
191(* ----------------------------------------------------------------------
192    compatible closure for labelled terms
193   ---------------------------------------------------------------------- *)
194
195val (lcompat_closure_rules, lcompat_closure_ind, lcompat_closure_cases) =
196    Hol_reln`(!x y. R x y ==> lcompat_closure R x y) /\
197             (!z x y. lcompat_closure R x y ==>
198                      lcompat_closure R (z @@ x) (z @@ y)) /\
199             (!z x y. lcompat_closure R x y ==>
200                      lcompat_closure R (x @@ z) (y @@ z)) /\
201             (!v x y. lcompat_closure R x y ==>
202                      lcompat_closure R (LAM v x) (LAM v y)) /\
203             (!v n z x y.
204                      lcompat_closure R x y ==>
205                      lcompat_closure R (LAMi n v x z) (LAMi n v y z)) /\
206             (!v n z x y.
207                      lcompat_closure R x y ==>
208                      lcompat_closure R (LAMi n v z x) (LAMi n v z y))`;
209
210(* reduction on lterms *)
211val beta0_def =
212    Define`beta0 M N = ?n v t u. (M = LAMi n v t u) /\ (N = [u/v]t)`;
213
214val beta1_def =
215    Define`beta1 (M: lterm) N =
216              ?v t u. (M = (LAM v t) @@ u) /\ (N = [u/v]t)`;
217
218val lcc_beta_bvc_ind = store_thm(
219  "lcc_beta_bvc_ind",
220  ``!P X. FINITE X /\
221          (!v M N. ~(v IN FV N) /\ ~(v IN X) ==>
222                   P (LAM v M @@ N) ([N/v]M)) /\
223          (!n v M N. ~(v IN FV N) /\ ~(v IN X) ==>
224                     P (LAMi n v M N) ([N/v]M)) /\
225          (!M M' N. P M M' ==> P (M @@ N) (M' @@ N)) /\
226          (!M N N'. P N N' ==> P (M @@ N) (M @@ N')) /\
227          (!v M M'. ~(v IN X) /\ P M M' ==> P (LAM v M) (LAM v M')) /\
228          (!n v M M' N. ~(v IN X) /\ ~(v IN FV N) /\ P M M' ==>
229                        P (LAMi n v M N) (LAMi n v M' N)) /\
230          (!n v M N N'.
231               ~(v IN X) /\ ~(v IN FV N) /\ ~(v IN FV N') /\ P N N' ==>
232               P (LAMi n v M N) (LAMi n v M N'))
233       ==>
234          !M N. lcompat_closure (beta0 RUNION beta1) M N ==> P M N``,
235  REPEAT GEN_TAC THEN STRIP_TAC THEN
236  Q_TAC SUFF_TAC `!M N. lcompat_closure(beta0 RUNION beta1) M N ==>
237                        !p. P (ltpm p M) (ltpm p N)`
238        THEN1 METIS_TAC [pmact_nil] THEN
239  HO_MATCH_MP_TAC lcompat_closure_ind THEN
240  SRW_TAC [][relationTheory.RUNION, beta0_def, beta1_def] THENL [
241    (* beta0 reduction *)
242    SRW_TAC [][ltpm_subst] THEN
243    Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p t) UNION FV (ltpm p u)` THEN
244    `LAMi n (lswapstr p v) (ltpm p t) (ltpm p u) =
245     LAMi n z (ltpm [(z,lswapstr p v)] (ltpm p t)) (ltpm p u)`
246       by SRW_TAC [][ltpm_ALPHAi] THEN
247    `[ltpm p u/lswapstr p v] (ltpm p t) =
248     [ltpm p u/z] (ltpm [(z,lswapstr p v)] (ltpm p t))`
249       by SRW_TAC [][fresh_ltpm_subst, l15a] THEN
250    SRW_TAC [][],
251    (* beta1 reduction *)
252    SRW_TAC [][ltpm_subst] THEN
253    Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p t) UNION FV (ltpm p u)` THEN
254    `LAM (lswapstr p v) (ltpm p t) =
255       LAM z (ltpm [(z,lswapstr p v)] (ltpm p t))`
256      by SRW_TAC [][ltpm_ALPHA] THEN
257    `[ltpm p u/lswapstr p v] (ltpm p t) =
258        [ltpm p u/z] (ltpm [(z,lswapstr p v)] (ltpm p t))`
259      by SRW_TAC [][fresh_ltpm_subst, l15a] THEN
260    SRW_TAC [][],
261
262    Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p M) UNION FV (ltpm p N)` THEN
263    Q_TAC SUFF_TAC `(LAM (lswapstr p v) (ltpm p M) =
264                         LAM z (ltpm [(z,lswapstr p v)] (ltpm p M))) /\
265                    (LAM (lswapstr p v) (ltpm p N) =
266                         LAM z (ltpm [(z,lswapstr p v)] (ltpm p N)))`
267          THEN1 SRW_TAC [][GSYM pmact_decompose] THEN
268    SRW_TAC [][ltpm_ALPHA],
269
270    Q_TAC (NEW_TAC "w")
271          `X UNION FV (ltpm p M) UNION FV (ltpm p N) UNION FV (ltpm p z)` THEN
272    `(LAMi n (lswapstr p v) (ltpm p M) (ltpm p z) =
273        LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p M)) (ltpm p z)) /\
274     (LAMi n (lswapstr p v) (ltpm p N) (ltpm p z) =
275        LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p N)) (ltpm p z))`
276      by SRW_TAC [][ltpm_ALPHAi] THEN
277    SRW_TAC [][GSYM pmact_decompose],
278
279    Q_TAC (NEW_TAC "w")
280          `X UNION FV (ltpm p z) UNION FV (ltpm p M) UNION FV (ltpm p N)` THEN
281    `!N. LAMi n (lswapstr p v) (ltpm p z) N =
282         LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p z)) N`
283      by SRW_TAC [][ltpm_ALPHAi] THEN
284    SRW_TAC [][GSYM pmact_decompose]
285  ]);
286
287open boolSimps
288val beta_matched = store_thm(
289  "beta_matched",
290  ``!M' N. beta (strip_label M') N ==>
291           ?N'. (beta0 RUNION beta1) M' N' /\ (N = strip_label N')``,
292  SIMP_TAC (srw_ss()) [beta_def] THEN
293  REPEAT GEN_TAC THEN
294  Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN
295  SRW_TAC [][] THENL [
296    FULL_SIMP_TAC (srw_ss()) [strip_label_eq_lam] THEN
297    SRW_TAC [DNF_ss][strip_label_subst, beta1_def, beta0_def,
298                     relationTheory.RUNION, lLAM_eq_thm] THEN METIS_TAC [],
299    FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm, relationTheory.RUNION, beta0_def,
300                              beta1_def] THEN
301    SRW_TAC [DNF_ss][lLAMi_eq_thm, strip_label_subst,
302                     fresh_tpm_subst, lemma15a]
303  ]);
304
305val lcc_beta_FV = store_thm(
306  "lcc_beta_FV",
307  ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==>
308          !x. x IN FV N ==> x IN FV M``,
309  HO_MATCH_MP_TAC lcompat_closure_ind THEN
310  SRW_TAC [][relationTheory.RUNION, beta0_def, beta1_def] THEN
311  TRY (PROVE_TAC []) THEN
312  FULL_SIMP_TAC (srw_ss() ++ boolSimps.COND_elim_ss) [lFV_SUB] THEN
313  PROVE_TAC []);
314
315val lcc_beta_subst = store_thm(
316  "lcc_beta_subst",
317  ``!M N P v. lcompat_closure (beta0 RUNION beta1) M N ==>
318              lcompat_closure (beta0 RUNION beta1) ([P/v]M) ([P/v]N)``,
319  REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`N`, `M`] THEN
320  HO_MATCH_MP_TAC lcc_beta_bvc_ind THEN
321  Q.EXISTS_TAC `v INSERT FV P` THEN SRW_TAC [][lcompat_closure_rules] THENL [
322    Q_TAC SUFF_TAC `beta1 (LAM v' ([P/v]M) @@ [P/v] N) ([P/v]([N/v']M))`
323          THEN1 METIS_TAC [lcompat_closure_rules, relationTheory.RUNION] THEN
324    SRW_TAC [][beta1_def] THEN
325    MAP_EVERY Q.EXISTS_TAC [`v'`, `[P/v]M`] THEN
326    SRW_TAC [][lSUBSTITUTION_LEMMA],
327    Q_TAC SUFF_TAC `beta0 (LAMi n v' ([P/v]M) ([P/v]N)) ([P/v]([N/v']M))`
328          THEN1 METIS_TAC [lcompat_closure_rules, relationTheory.RUNION] THEN
329    SRW_TAC [][beta0_def] THEN
330    MAP_EVERY Q.EXISTS_TAC [`n`,`v'`, `[P/v]M`, `[P/v]N`] THEN
331    SRW_TAC [][lSUBSTITUTION_LEMMA]
332  ]);
333
334val lcc_beta_ltpm_imp = store_thm(
335  "lcc_beta_ltpm_imp",
336  ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==>
337          !pi. lcompat_closure (beta0 RUNION beta1) (ltpm pi M) (ltpm pi N)``,
338  HO_MATCH_MP_TAC lcompat_closure_ind THEN
339  SRW_TAC [][lcompat_closure_rules] THEN
340  FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION] THEN
341  SRW_TAC [][ltpm_subst] THEN
342  METIS_TAC [relationTheory.RUNION, beta0_def, beta1_def,
343             lcompat_closure_rules]);
344
345val lcc_beta_ltpm_eqn = store_thm(
346  "lcc_beta_ltpm_eqn",
347  ``lcompat_closure (beta0 RUNION beta1) (ltpm pi M) N =
348    lcompat_closure (beta0 RUNION beta1) M (ltpm (REVERSE pi) N)``,
349  METIS_TAC [lcc_beta_ltpm_imp, pmact_inverse]);
350
351val lcc_beta_LAM = store_thm(
352  "lcc_beta_LAM",
353  ``!v t N. lcompat_closure (beta0 RUNION beta1) (LAM v t) N =
354            ?N0. (N = LAM v N0) /\
355                 lcompat_closure (beta0 RUNION beta1) t N0``,
356  REPEAT GEN_TAC THEN
357  CONV_TAC (LAND_CONV (REWR_CONV lcompat_closure_cases)) THEN
358  SRW_TAC [][beta0_def, beta1_def, relationTheory.RUNION] THEN EQ_TAC THEN
359  STRIP_TAC THENL [
360    FULL_SIMP_TAC (srw_ss()) [lLAM_eq_thm] THEN
361    SRW_TAC [][ltpm_eqr, lcc_beta_ltpm_eqn, pmact_flip_args] THEN
362    METIS_TAC [lcc_beta_FV],
363    METIS_TAC []
364  ]);
365
366val cc_beta_matched = store_thm(
367  "cc_beta_matched",
368  ``!M N. compat_closure beta M N ==>
369          !M'. (M = strip_label M') ==>
370               ?N'. lcompat_closure (beta0 RUNION beta1) M' N' /\
371                    (N = strip_label N')``,
372  HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT CONJ_TAC THENL [
373    SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss)
374             [beta_def, strip_label_eq_redex] THEN
375    SRW_TAC [][] THEN
376    Q.EXISTS_TAC `[u'/x]t'` THEN SRW_TAC [][strip_label_subst] THENL [
377      METIS_TAC [lcompat_closure_rules, beta1_def, relationTheory.RUNION],
378      METIS_TAC [lcompat_closure_rules, beta0_def, relationTheory.RUNION]
379    ],
380    REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
381    `(���s. M' = VAR s) ��� (���t1 t2. M' = t1 @@ t2) ��� (���v t. M' = LAM v t) ���
382     (���n v t1 t2. M' = LAMi n v t1 t2)`
383       by (Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN
384           METIS_TAC []) THEN
385    SRW_TAC [][] THENL [
386      FIRST_X_ASSUM (Q.SPEC_THEN `t2` MP_TAC) THEN SRW_TAC [][] THEN
387      Q.EXISTS_TAC `t1 @@ N'` THEN SRW_TAC [][lcompat_closure_rules],
388      FIRST_X_ASSUM (Q.SPEC_THEN `t2` MP_TAC) THEN SRW_TAC [][] THEN
389      Q.EXISTS_TAC `LAMi n v t1 N'` THEN SRW_TAC [][lcompat_closure_rules]
390    ],
391    REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN
392    `(���s. M' = VAR s) ��� (���t1 t2. M' = t1 @@ t2) ��� (���v t. M' = LAM v t) ���
393     (���n v t1 t2. M' = LAMi n v t1 t2)`
394       by (Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN
395           METIS_TAC []) THEN
396    SRW_TAC [][] THENL [
397      FIRST_X_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN SRW_TAC [][] THEN
398      Q.EXISTS_TAC `N' @@ t2` THEN SRW_TAC [][lcompat_closure_rules],
399      FIRST_X_ASSUM (Q.SPEC_THEN `LAM v t1` MP_TAC) THEN
400      SRW_TAC [][lcc_beta_LAM] THEN
401      Q.EXISTS_TAC `LAMi n v N0 t2` THEN SRW_TAC [][lcompat_closure_rules]
402    ],
403    SRW_TAC [][strip_label_eq_lam] THEN
404    FIRST_X_ASSUM (Q.SPEC_THEN `t'` MP_TAC) THEN SRW_TAC [][] THEN
405    Q.EXISTS_TAC `LAM v N'` THEN SRW_TAC [][lcompat_closure_rules] THEN
406    METIS_TAC []
407  ]);
408
409val lemma11_1_6i = store_thm(
410  "lemma11_1_6i",
411  ``!M' N. reduction beta (strip_label M') N ==>
412           ?N'. RTC (lcompat_closure (beta0 RUNION beta1)) M' N' /\
413                (N = strip_label N')``,
414  SIMP_TAC (srw_ss()) [] THEN
415  Q_TAC SUFF_TAC
416        `!M N. RTC (compat_closure beta) M N ==>
417               !M'. (M = strip_label M') ==>
418                    ?N'. RTC (lcompat_closure (beta0 RUNION beta1)) M' N' /\
419                         (N = strip_label N')` THEN1 PROVE_TAC [] THEN
420  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN CONJ_TAC THEN
421  PROVE_TAC [relationTheory.RTC_RULES, cc_beta_matched]);
422
423val lcc_beta_matching_beta = store_thm(
424  "lcc_beta_matching_beta",
425  ``!M' N'. lcompat_closure (beta0 RUNION beta1) M' N' ==>
426            compat_closure beta (strip_label M') (strip_label N')``,
427  HO_MATCH_MP_TAC lcompat_closure_ind THEN
428  SRW_TAC [][strip_label_thm] THEN1
429    (Q_TAC SUFF_TAC `beta (strip_label M') (strip_label N')` THEN1
430        PROVE_TAC [compat_closure_rules] THEN
431     FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION,
432                               strip_label_thm, beta_def,
433                               strip_label_subst] THEN PROVE_TAC []) THEN
434  PROVE_TAC [compat_closure_rules]);
435
436val lemma11_1_6ii = store_thm(
437  "lemma11_1_6ii",
438  ``!M' N'.
439      RTC (lcompat_closure (beta0 RUNION beta1)) M' N' ==>
440      reduction beta (strip_label M') (strip_label N')``,
441  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
442  PROVE_TAC [reduction_rules, lcc_beta_matching_beta]);
443
444val coFV_phi = prove(
445  ``~(v IN FV M) ==> ~(v IN FV (phi M))``,
446  METIS_TAC [FV_phi]);
447
448val lemma11_1_7i = store_thm(
449  "lemma11_1_7i",
450  ``!M. phi ([N/x]M) = [phi N/x] (phi M)``,
451  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `x INSERT FV N` THEN
452  SRW_TAC [][SUB_THM, coFV_phi, lSUB_VAR, SUB_VAR] THEN
453  SRW_TAC [][chap2Theory.substitution_lemma, coFV_phi]);
454
455val lcc_beta_phi_matched = store_thm(
456  "lcc_beta_phi_matched",
457  ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==>
458          reduction beta (phi M) (phi N)``,
459  HO_MATCH_MP_TAC lcompat_closure_ind THEN
460  SRW_TAC [][] THENL [
461    FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION]
462    THENL [
463      SRW_TAC [][lemma11_1_7i, reduction_rules],
464      Q_TAC SUFF_TAC `beta (LAM v (phi t) @@ phi u) (phi ([u/v] t))` THEN1
465        PROVE_TAC [reduction_rules] THEN
466      SRW_TAC [][lemma11_1_7i, beta_def] THEN PROVE_TAC []
467    ],
468
469    PROVE_TAC [reduction_rules],
470    PROVE_TAC [reduction_rules],
471    PROVE_TAC [reduction_beta_subst],
472    PROVE_TAC [lemma3_8]
473  ]);
474
475val lemma11_1_7ii = store_thm(
476  "lemma11_1_7ii",
477  ``!M N. RTC (lcompat_closure (beta0 RUNION beta1)) M N ==>
478          reduction beta (phi M) (phi N)``,
479  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
480  PROVE_TAC [reduction_rules, lcc_beta_phi_matched]);
481
482val lemma11_1_8 = store_thm(
483  "lemma11_1_8",
484  ``!M. reduction beta (strip_label M) (phi M)``,
485  HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `{}` THEN
486  SIMP_TAC (srw_ss()) [strip_label_thm, reduction_rules] THEN CONJ_TAC THENL [
487    PROVE_TAC [reduction_rules],
488    MAP_EVERY Q.X_GEN_TAC [`s`, `M`, `M'`] THEN STRIP_TAC THEN
489    `beta (LAM s (strip_label M) @@ strip_label M')
490          ([strip_label M'/s] (strip_label M))` by PROVE_TAC [beta_def] THEN
491    `reduction beta ([strip_label M'/s] (strip_label M))
492                    ([phi M'/s] (strip_label M))` by PROVE_TAC [lemma3_8] THEN
493    `reduction beta ([phi M'/s] (strip_label M))
494                    ([phi M'/s] (phi M))` by
495        PROVE_TAC [reduction_beta_subst, l14a] THEN
496    PROVE_TAC [reduction_rules]
497  ]);
498
499val can_index_redex = store_thm(
500  "can_index_redex",
501  ``!M N. compat_closure beta M N ==>
502          ?M'. (strip_label M' = M) /\ (phi M' = N)``,
503  HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT CONJ_TAC THENL [
504    MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN
505    SIMP_TAC (srw_ss()) [beta_def, GSYM LEFT_FORALL_IMP_THM] THEN
506    MAP_EVERY Q.X_GEN_TAC [`x`,`body`,`arg`] THEN SRW_TAC [][] THEN
507    Q.EXISTS_TAC `LAMi 0 x (null_labelling body) (null_labelling arg)` THEN
508    SIMP_TAC (srw_ss()) [],
509    MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`z`] THEN SRW_TAC [][] THEN
510    Q.EXISTS_TAC `null_labelling z @@ M'` THEN SRW_TAC [][],
511    MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`z`] THEN SRW_TAC [][] THEN
512    Q.EXISTS_TAC `M' @@ null_labelling z` THEN SRW_TAC [][],
513    MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`v`] THEN SRW_TAC [][] THEN
514    Q.EXISTS_TAC `LAM v M'` THEN
515    ASM_SIMP_TAC (srw_ss()) []
516  ]);
517
518val strip_lemma = store_thm(
519  "strip_lemma",
520  ``!M M' N. compat_closure beta M M' /\
521             reduction beta M N ==>
522             ?N'. reduction beta M' N' /\ reduction beta N N'``,
523  REPEAT STRIP_TAC THEN
524  `?Mtilde. (strip_label Mtilde = M) /\ (phi Mtilde = M')` by
525     PROVE_TAC [can_index_redex] THEN
526  `?Ntilde. (N = strip_label Ntilde) /\
527            RTC (lcompat_closure (beta0 RUNION beta1)) Mtilde Ntilde` by
528     PROVE_TAC [lemma11_1_6i] THEN
529  `reduction beta M' (phi Ntilde)` by PROVE_TAC [lemma11_1_7ii] THEN
530  `reduction beta N (phi Ntilde)` by PROVE_TAC [lemma11_1_8] THEN
531  PROVE_TAC []);
532
533val beta_CR_2 = store_thm(
534  "beta_CR_2",
535  ``CR beta``,
536  SIMP_TAC (srw_ss())[CR_def, diamond_property_def] THEN
537  Q_TAC SUFF_TAC
538        `!M M1. RTC (compat_closure beta) M M1 ==>
539                !M2. reduction beta M M2 ==>
540                     ?M3. reduction beta M1 M3 /\ reduction beta M2 M3`
541        THEN1 PROVE_TAC [] THEN
542  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
543  PROVE_TAC [reduction_rules, strip_lemma]);
544
545val _ = export_theory()
546