1open HolKernel Parse boolLib bossLib binderLib
2open nomsetTheory
3
4local open stringTheory in end
5
6fun Store_thm (n,t,tac) = store_thm(n,t,tac) before export_rewrites [n]
7
8val _ = new_theory "MPlambda"
9
10val _ = Hol_datatype `MPterm = Var of string
11                             | Parameter of string
12                             | App of MPterm => MPterm
13                             | Abs of string => MPterm`;
14
15val psub_def = Define`
16  (psub a p (Var s) = Var s) /\
17  (psub a p (Parameter q) = if p = q then a else Parameter q) /\
18  (psub a p (App t1 t2) = App (psub a p t1) (psub a p t2)) /\
19  (psub a p (Abs v t) = Abs v (psub a p t))
20`;
21val _ = export_rewrites ["psub_def"]
22
23val params_def = Define`
24  (params (Var s) = {}) /\
25  (params (Parameter p) = {p}) /\
26  (params (App t1 t2) = params t1 UNION params t2) /\
27  (params (Abs v t) = params t)
28`;
29val _ = export_rewrites ["params_def"]
30
31val vsub_def = Define`
32  (vsub a v (Var u) = if u = v then a else Var u) /\
33  (vsub a v (Parameter p) = Parameter p) /\
34  (vsub a v (App t1 t2) = App (vsub a v t1) (vsub a v t2)) /\
35  (vsub a v (Abs u t) = if u = v then Abs u t
36                        else Abs u (vsub a v t))
37`;
38val _ = export_rewrites ["vsub_def"]
39
40val allvars_def = Define`
41  (allvars (Parameter p) = {}) /\
42  (allvars (Var v) = {v}) /\
43  (allvars (App t1 t2) = allvars t1 UNION allvars t2) /\
44  (allvars (Abs v t) = v INSERT allvars t)
45`;
46val _= export_rewrites ["allvars_def"]
47
48val FINITE_allvars = Store_thm(
49  "FINITE_allvars",
50  ``!t. FINITE (allvars t)``,
51  Induct THEN SRW_TAC [][]);
52
53val vsub_14a = Store_thm(
54  "vsub_14a",
55  ``~(v IN allvars t) ==> (vsub N v t = t)``,
56  Induct_on `t` THEN SRW_TAC [][]);
57
58val pvsub_vsub_collapse = store_thm(
59  "pvsub_vsub_collapse",
60  ``!M p v1 v2. ~(v2 IN allvars M) ==>
61                (vsub (Parameter p) v2 (vsub (Var v2) v1 M) =
62                 vsub (Parameter p) v1 M)``,
63  Induct THEN SRW_TAC [][]);
64
65val params_vvsub = Store_thm(
66  "params_vvsub",
67  ``params (vsub (Var v1) v2 M) = params M``,
68  Induct_on `M` THEN SRW_TAC [][]);
69
70val shape_lemma = store_thm(
71  "shape_lemma",
72  ``!M p. ?v M'. (M = vsub (Parameter p) v M') /\ ~(p IN params M')``,
73  Induct THEN ASM_SIMP_TAC (srw_ss()) []THENL [
74    Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN
75    Q_TAC (NEW_TAC "z") `{s}` THEN
76    MAP_EVERY Q.EXISTS_TAC [`z`, `Var s`] THEN SRW_TAC [][],
77
78    Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN
79    Cases_on `s = p` THENL [
80      MAP_EVERY Q.EXISTS_TAC [`x`, `Var x`] THEN SRW_TAC [][],
81      MAP_EVERY Q.EXISTS_TAC [`x`, `Parameter s`] THEN SRW_TAC [][]
82    ],
83
84    GEN_TAC THEN
85    `?v1 M1. (M = vsub (Parameter p) v1 M1) /\ ~(p IN params M1)`
86       by METIS_TAC [] THEN
87    `?v2 M2. (M' = vsub (Parameter p) v2 M2) /\ ~(p IN params M2)`
88       by METIS_TAC [] THEN
89    Q_TAC (NEW_TAC "z") `allvars M1 UNION allvars M2 UNION {v1;v2}` THEN
90    `(M = vsub (Parameter p) z (vsub (Var z) v1 M1)) /\
91     (M' = vsub (Parameter p) z (vsub (Var z) v2 M2))`
92       by METIS_TAC [pvsub_vsub_collapse] THEN
93    MAP_EVERY Q.EXISTS_TAC
94              [`z`, `App (vsub (Var z) v1 M1) (vsub (Var z) v2 M2)`] THEN
95    SRW_TAC [][pvsub_vsub_collapse],
96
97    Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN
98    FIRST_X_ASSUM (Q.SPEC_THEN `p` STRIP_ASSUME_TAC) THEN
99    REVERSE (Cases_on `s = v`) THEN1
100      (MAP_EVERY Q.EXISTS_TAC [`v`, `Abs s M'`] THEN SRW_TAC [][]) THEN
101    SRW_TAC [][] THEN
102    Q_TAC (NEW_TAC "z") `s INSERT allvars M'` THEN
103    MAP_EVERY Q.EXISTS_TAC [`z`, `Abs s (vsub (Var z) s M')`] THEN
104    SRW_TAC [][pvsub_vsub_collapse]
105  ]);
106
107val (vclosed_rules, vclosed_ind, vclosed_cases) = Hol_reln`
108  (!p. vclosed (Parameter p)) /\
109  (!p v t. vclosed (vsub (Parameter p) v t) ==>
110           vclosed (Abs v t)) /\
111  (!t1 t2. vclosed t1 /\ vclosed t2 ==> vclosed (App t1 t2))
112`;
113
114val FINITE_params = Store_thm(
115  "FINITE_params",
116  ``!t. FINITE (params t)``,
117  Induct THEN SRW_TAC [][]);
118
119val psub_14a = Store_thm(
120  "psub_14a",
121  ``!M p N. ~(p IN params M) ==> (psub N p M = M)``,
122  Induct THEN SRW_TAC [][]);
123
124
125val vsub_is_psub_alpha = store_thm(
126  "vsub_is_psub_alpha",
127  ``!M p N v. ~(p IN params M) ==>
128              (psub N p (vsub (Parameter p) v M) = vsub N v M)``,
129  Induct THEN SRW_TAC [][]);
130
131val vars_def = Define`
132  (vars (Var u) = {u}) /\
133  (vars (Parameter p) = {}) /\
134  (vars (App t1 t2) = vars t1 UNION vars t2) /\
135  (vars (Abs v t) = vars t DIFF {v})
136`;
137val _ = export_rewrites ["vars_def"]
138
139val vsub_14a = Store_thm(
140  "vsub_14a",
141  ``!M v N. ~(v IN vars M) ==> (vsub N v M = M)``,
142  Induct THEN SRW_TAC [][]);
143
144
145val raw_MPpm_def = Define`
146  (raw_MPpm pi (Parameter s) = Parameter (lswapstr pi s)) /\
147  (raw_MPpm pi (Var v) = Var v) /\
148  (raw_MPpm pi (App t1 t2) = App (raw_MPpm pi t1) (raw_MPpm pi t2)) /\
149  (raw_MPpm pi (Abs v t) = Abs v (raw_MPpm pi t))
150`;
151val _ = export_rewrites ["raw_MPpm_def"]
152
153val _ = overload_on("MP_pmact",``mk_pmact raw_MPpm``);
154val _ = overload_on("MPpm", ``pmact MP_pmact``);
155
156val MPpm_raw = store_thm(
157  "MPpm_raw",
158  ``MPpm = raw_MPpm``,
159  SRW_TAC [][GSYM pmact_bijections] THEN
160  SRW_TAC [][is_pmact_def] THENL [
161    Induct_on `x` THEN SRW_TAC [][],
162    Induct_on `x` THEN SRW_TAC [][pmact_decompose],
163    FULL_SIMP_TAC (srw_ss()) [permeq_thm, FUN_EQ_THM] THEN
164    Induct THEN SRW_TAC [][]
165  ]);
166
167val MPpm_thm = save_thm(
168"MPpm_thm",
169raw_MPpm_def |> SUBS [GSYM MPpm_raw]);
170val _ = export_rewrites["MPpm_thm"];
171
172val MPpm_fresh = Store_thm(
173  "MPpm_fresh",
174  ``!M x y. ~(x IN params M) /\ ~(y IN params M) ==>
175            (MPpm [(x,y)] M = M)``,
176  Induct THEN SRW_TAC [][]);
177
178val MPpm_NIL = Store_thm(
179  "MPpm_NIL",
180  ``MPpm [] t = t``,
181  Induct_on `t` THEN SRW_TAC [][]);
182
183val supp_MPpm = Store_thm(
184  "supp_MPpm",
185  ``supp MP_pmact = params``,
186  ONCE_REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN
187  MATCH_MP_TAC supp_unique_apart THEN SRW_TAC [][support_def] THEN
188  Induct_on `x` THEN SRW_TAC [][] THEN METIS_TAC []);
189
190val MPpm_vsub = store_thm(
191  "MPpm_vsub",
192  ``!M v pi N. MPpm pi (vsub M v N) = vsub (MPpm pi M) v (MPpm pi N)``,
193  Induct_on `N` THEN SRW_TAC [][]);
194
195val vclosed_MPpm = store_thm(
196  "vclosed_MPpm",
197  ``!M. vclosed M ==> !pi. vclosed (MPpm pi M)``,
198  HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vclosed_rules, MPpm_vsub] THEN
199  METIS_TAC [vclosed_rules]);
200
201val vars_pvsub = store_thm(
202  "vars_pvsub",
203  ``!p v M. vars (vsub (Parameter p) v M) = vars M DELETE v``,
204  Induct_on `M` THEN SRW_TAC [][] THEN
205  SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []);
206
207
208val vclosed_empty_vars = store_thm(
209  "vclosed_empty_vars",
210  ``!t. vclosed t ==> (vars t = {})``,
211  HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vars_pvsub] THEN
212  FULL_SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION]);
213
214
215val vclosed_var = Store_thm(
216  "vclosed_var",
217  ``!v. ~(vclosed (Var v))``,
218  ONCE_REWRITE_TAC [vclosed_cases] THEN SRW_TAC [][]);
219
220val vclosed_parameter = Store_thm(
221  "vclosed_parameter",
222  ``vclosed (Parameter p)``,
223  ONCE_REWRITE_TAC [vclosed_cases] THEN SRW_TAC [][]);
224
225val _ = set_fixity "=" (Infix(NONASSOC, 100))
226
227val vclosed_app = Store_thm(
228  "vclosed_app",
229  ``vclosed (App t1 t2) = vclosed t1 /\ vclosed t2``,
230  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [vclosed_cases])) THEN
231  SRW_TAC [][]);
232
233val vclosed_abs = store_thm(
234  "vclosed_abs",
235  ``vclosed (Abs v t) = ?p. vclosed (vsub (Parameter p) v t)``,
236  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [vclosed_cases])) THEN
237  SRW_TAC [][]);
238
239val pvsub_eq_app = prove(
240  ``(vsub (Parameter p) v M = App t1 t2) =
241      ?M1 M2. (M = App M1 M2) /\ (vsub (Parameter p) v M1 = t1) /\
242              (vsub (Parameter p) v M2 = t2)``,
243  Cases_on `M` THEN SRW_TAC [][]);
244
245val pvsub_eq_param = prove(
246  ``(vsub (Parameter p1) v M = Parameter p2) =
247       (M = Var v) /\ (p1 = p2) \/
248       (M = Parameter p2)``,
249  Cases_on `M` THEN SRW_TAC [][]);
250
251val pvsub_eq_abs = prove(
252  ``(vsub (Parameter p) v M = Abs s t) =
253       (?M0. ~(s = v) /\ (M = Abs s M0) /\ (vsub (Parameter p) v M0 = t)) \/
254       (v = s) /\ (M = Abs s t)``,
255  Cases_on `M` THEN SRW_TAC [][] THEN METIS_TAC []);
256
257val independent_pvsub = prove(
258  ``!p1 p2 v1 v2 M.
259      ~(v1 = v2) ==> (vsub (Parameter p1) v1 (vsub (Parameter p2) v2 M) =
260                      vsub (Parameter p2) v2 (vsub (Parameter p1) v1 M))``,
261  Induct_on `M` THEN SRW_TAC [][])
262
263val IN_params_MPpm = store_thm(
264  "IN_params_MPpm",
265  ``x IN params (MPpm pi M) = lswapstr (REVERSE pi) x IN params M``,
266  Induct_on `M` THEN SRW_TAC [][pmact_eql]);
267
268val independent_psub_vsub = prove(
269  ``!M v p1 p2 p3.
270      ~(p2 = p3) ==>
271      (psub (Parameter p1) p2 (vsub (Parameter p3) v M) =
272       vsub (Parameter p3) v (psub (Parameter p1) p2 M))``,
273  Induct THEN SRW_TAC [][]);
274
275val (cvclosed_rules, cvclosed_ind, cvclosed_cases) = Hol_reln`
276  (!p. cvclosed (Parameter p)) /\
277  (!M N. cvclosed M /\ cvclosed N ==> cvclosed (App M N)) /\
278  (!v p M. ~(p IN params M) /\ cvclosed (vsub (Parameter p) v M) ==>
279           cvclosed (Abs v M))
280`;
281
282val cvclosed_eqns = prove(
283  ``cvclosed (Parameter p) /\
284    (cvclosed (App M N) = cvclosed M /\ cvclosed N) /\
285    (cvclosed (Abs v M) = ?p. ~(p IN params M) /\
286                              cvclosed (vsub (Parameter p) v M))``,
287  REPEAT CONJ_TAC THEN1
288    (ONCE_REWRITE_TAC [cvclosed_cases] THEN SRW_TAC [][]) THEN
289  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [cvclosed_cases])) THEN
290  SRW_TAC [][]);
291
292val cvclosed_strongctxt_ind = prove(
293  ``!P f. (!x. FINITE (f x)) /\
294          (!p x. P (Parameter p) x) /\
295          (!M N y. (!x. P M x)  /\ (!x. P N x) ==> P (App M N) y) /\
296          (!v p M y. ~(p IN f y) /\ ~(p IN params M) /\
297                     (!x. P (vsub (Parameter p) v M) x) ==>
298                     P (Abs v M) y)
299        ==>
300          !M. cvclosed M ==> !x. P M x``,
301  REPEAT GEN_TAC THEN STRIP_TAC THEN
302  Q_TAC SUFF_TAC `!M. cvclosed M ==> !pi x. P (MPpm pi M) x`
303        THEN1 METIS_TAC [MPpm_NIL] THEN
304  HO_MATCH_MP_TAC cvclosed_ind THEN
305  SRW_TAC [][] THEN
306  FIRST_X_ASSUM MATCH_MP_TAC THEN
307  FULL_SIMP_TAC (srw_ss()) [MPpm_vsub] THEN
308  Q_TAC (NEW_TAC "z") `f x UNION params (MPpm pi M)` THEN
309  Q.EXISTS_TAC `z` THEN SRW_TAC [][] THEN
310  FIRST_X_ASSUM (Q.SPECL_THEN [`(stringpm pi p, z) :: pi`, `x'`] MP_TAC) THEN
311  ASM_SIMP_TAC (srw_ss()) [] THEN
312  `MPpm [(stringpm pi p, z)] (MPpm pi M) = MPpm pi M`
313    by SRW_TAC [][MPpm_fresh, IN_params_MPpm, stringpm_raw] THEN
314  FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose]);
315
316val cvclosed_strong_ind =
317(Q.GEN `P` o Q.GEN `X` o
318 SIMP_RULE (srw_ss()) [] o
319 Q.SPECL [`\t u. P t`, `\u. X`] o
320 INST_TYPE [alpha |-> ``:one``]) cvclosed_strongctxt_ind
321
322val notin_pvsub_I = prove(
323  ``~(p1 = p2) /\ ~(p1 IN params M) ==>
324    ~(p1 IN params (vsub (Parameter p2) v M))``,
325  Induct_on `M` THEN SRW_TAC [][]);
326
327val cvclosed_p_indep = prove(
328  ``!t. cvclosed t ==>
329        !pp't0 v p p' t0.
330            ((p, p', t0) = pp't0) /\ (t = vsub (Parameter p) v t0) ==>
331            cvclosed (vsub (Parameter p') v t0)``,
332  HO_MATCH_MP_TAC cvclosed_strongctxt_ind THEN
333  Q.EXISTS_TAC `\(p,p',t0). {p;p'} UNION params t0` THEN
334  SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
335  SRW_TAC [][cvclosed_eqns, pvsub_eq_abs, pvsub_eq_param, pvsub_eq_app] THEN
336  SRW_TAC [][cvclosed_eqns] THENL [
337    METIS_TAC [],
338    METIS_TAC [],
339    FULL_SIMP_TAC (srw_ss()) [] THEN
340    Q.EXISTS_TAC `p` THEN CONJ_TAC THENL [
341      MATCH_MP_TAC notin_pvsub_I THEN SRW_TAC [][],
342      METIS_TAC [independent_pvsub]
343    ],
344    METIS_TAC []
345  ]);
346
347val cvclosed_pickany = save_thm(
348  "cvclosed_pickany",
349  SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] cvclosed_p_indep);
350
351val cvclosed_vclosed = prove(
352  ``!t. cvclosed t ==> vclosed t``,
353  HO_MATCH_MP_TAC cvclosed_ind THEN SRW_TAC [][vclosed_rules] THEN
354  METIS_TAC [vclosed_rules]);
355
356val vclosed_cvclosed = prove(
357  ``!t. vclosed t ==> cvclosed t``,
358  HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][cvclosed_rules] THEN
359  MATCH_MP_TAC (last (CONJUNCTS cvclosed_rules)) THEN
360  Q_TAC (NEW_TAC "z") `params t` THEN
361  METIS_TAC [cvclosed_pickany]);
362
363val cv_eq_vclosed = store_thm(
364  "cv_eq_vclosed",
365  ``cvclosed = vclosed``,
366  SRW_TAC [] [FUN_EQ_THM, vclosed_cvclosed, cvclosed_vclosed, EQ_IMP_THM]);
367
368val vclosed_strong_ind = save_thm(
369  "vclosed_strong_ind",
370  REWRITE_RULE [cv_eq_vclosed] cvclosed_strong_ind)
371
372val double_pvsub = Store_thm(
373  "double_pvsub",
374  ``vsub (Parameter p1) v (vsub (Parameter p2) v t) =
375    vsub (Parameter p2) v t``,
376  Induct_on `t` THEN SRW_TAC [][]);
377
378val vclosed_pvsub = store_thm(
379  "vclosed_pvsub",
380  ``!t. vclosed t ==> !p v. vclosed (vsub (Parameter p) v t)``,
381  HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vclosed_rules] THEN
382  METIS_TAC [vclosed_rules, double_pvsub, independent_pvsub]);
383
384val cofin_vclosed_ind = store_thm(
385  "cofin_vclosed_ind",
386  ``!P. (!p. P (Parameter p)) /\
387        (!v t X. FINITE X /\
388                 (!p. ~(p IN X) ==> P (vsub (Parameter p) v t)) ==>
389                 P (Abs v t)) /\
390        (!t1 t2. P t1 /\ P t2 ==> P (App t1 t2)) ==>
391        !t. vclosed t ==> P t``,
392  GEN_TAC THEN STRIP_TAC THEN
393  Q_TAC SUFF_TAC `!t. vclosed t ==> !pi. P (MPpm pi t)`
394        THEN1 METIS_TAC [MPpm_NIL] THEN
395  HO_MATCH_MP_TAC vclosed_strong_ind THEN
396  Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN
397  FIRST_X_ASSUM MATCH_MP_TAC THEN
398  Q.EXISTS_TAC `params (MPpm pi t)` THEN
399  FULL_SIMP_TAC (srw_ss()) [MPpm_vsub] THEN
400  Q.X_GEN_TAC `p1` THEN STRIP_TAC THEN
401  FIRST_X_ASSUM (Q.SPEC_THEN `[(p1,stringpm pi p)] ++ pi` MP_TAC) THEN
402  ASM_SIMP_TAC (srw_ss()) [] THEN
403  Q_TAC SUFF_TAC `MPpm ((p1,stringpm pi p)::pi) t = MPpm pi t`
404        THEN1 SRW_TAC [][] THEN
405  `MPpm [(p1,stringpm pi p)] (MPpm pi t) = MPpm pi t`
406     by SRW_TAC [][MPpm_fresh, IN_params_MPpm, stringpm_raw] THEN
407  FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose]);
408
409val (avclosed_rules, avclosed_ind, avclosed_cases) = Hol_reln`
410  (!p. avclosed (Parameter p)) /\
411  (!t1 t2. avclosed t1 /\ avclosed t2 ==> avclosed (App t1 t2)) /\
412  (!v t. (!p. avclosed (vsub (Parameter p) v t)) ==>
413         avclosed (Abs v t))
414`;
415
416val avclosed_pickany = prove(
417  ``!t. avclosed t ==>
418        !v p p' t0. (t = vsub (Parameter p) v t0) ==>
419                    avclosed (vsub (Parameter p') v t0)``,
420  HO_MATCH_MP_TAC avclosed_ind THEN
421  SRW_TAC [][pvsub_eq_app, pvsub_eq_param, pvsub_eq_abs] THEN
422  SRW_TAC [][avclosed_rules] THENL [
423    METIS_TAC [avclosed_rules],
424    MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN
425    METIS_TAC [independent_pvsub],
426    MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN
427    METIS_TAC []
428  ]);
429
430(* page 12 *)
431val avclosed_alpha = store_thm(
432  "avclosed_alpha",
433  ``avclosed (vsub (Parameter p) v t) ==>
434    !q. avclosed (vsub (Parameter q) v t)``,
435  METIS_TAC [avclosed_pickany]);
436
437val vclosed_avclosed = store_thm(
438  "vclosed_avclosed",
439  ``!t. vclosed t ==> avclosed t``,
440  HO_MATCH_MP_TAC vclosed_strong_ind THEN
441  SRW_TAC [][avclosed_rules] THEN
442  Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN
443  MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN SRW_TAC [][] THEN
444  METIS_TAC [avclosed_pickany]);
445
446val avclosed_vclosed = prove(
447  ``!t. avclosed t ==> vclosed t``,
448  HO_MATCH_MP_TAC avclosed_ind THEN SRW_TAC [][vclosed_abs]);
449
450val avclosed_eq_vclosed = prove(
451  ``avclosed = vclosed``,
452  SRW_TAC [][FUN_EQ_THM, EQ_IMP_THM, vclosed_avclosed, avclosed_vclosed]);
453
454val vclosed_avclosed_ind = save_thm(
455  "vclosed_avclosed_ind",
456  REWRITE_RULE [avclosed_eq_vclosed] avclosed_ind);
457
458val sub = ``\t (p,v). vsub (Parameter p) v t``
459val FOLDL_Parameter = prove(
460  ``!l. FOLDL ^sub (Parameter p) l = Parameter p``,
461  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
462val FOLDL_Var = prove(
463  ``!l. (?p. FOLDL ^sub (Var s) l = Parameter p) \/
464        (FOLDL ^sub (Var s) l = Var s)``,
465  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
466  FULL_SIMP_TAC (srw_ss()) [] THEN
467  SRW_TAC [][FOLDL_Parameter]);
468
469val FOLDL_App = prove(
470  ``!l t1 t2. FOLDL ^sub (App t1 t2) l =
471              App (FOLDL ^sub t1 l) (FOLDL ^sub t2 l)``,
472  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
473
474val FOLDL_Abs = prove(
475  ``!l v t. FOLDL ^sub (Abs v t) l =
476            Abs v (FOLDL ^sub t (FILTER (\ (p,u). ~(u = v)) l))``,
477  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
478  SRW_TAC [][]);
479
480val vsub_FOLDL = prove(
481  ``!l t p s. vsub (Parameter p) s (FOLDL ^sub t l) =
482              FOLDL ^sub t (l ++ [(p,s)])``,
483  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
484
485val vars_pvsub = prove(
486  ``vars (vsub (Parameter p) v t) = vars t DELETE v``,
487  SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN
488  Induct_on `t` THEN SRW_TAC [][] THEN
489  METIS_TAC []);
490
491
492val vars_FOLDL = prove(
493  ``!l t. vars (FOLDL ^sub t l) = vars t DIFF set (MAP SND l)``,
494  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, vars_pvsub] THEN
495  SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []);
496
497val empty_vars_vclosed = store_thm(
498  "empty_vars_vclosed",
499  ``!t. (vars t = {}) ==> vclosed t``,
500  Q_TAC SUFF_TAC
501    `!t l. (vars (FOLDL (\t (p,v). vsub (Parameter p) v t) t l) = {}) ==>
502           vclosed (FOLDL (\t (p,v). vsub (Parameter p) v t) t l)`
503    THEN1 METIS_TAC [listTheory.FOLDL] THEN
504  Induct THEN
505  ASM_SIMP_TAC (srw_ss()) [FOLDL_App, FOLDL_Parameter, FOLDL_Abs] THENL [
506    MAP_EVERY Q.X_GEN_TAC [`s`,`l`] THEN
507    Q.SPEC_THEN `l` STRIP_ASSUME_TAC FOLDL_Var THEN
508    FULL_SIMP_TAC (srw_ss()) [],
509    SRW_TAC [][] THEN
510    MATCH_MP_TAC (List.nth(CONJUNCTS vclosed_rules, 1)) THEN
511    SRW_TAC [][vsub_FOLDL] THEN Q.EXISTS_TAC `p` THEN
512    FIRST_X_ASSUM MATCH_MP_TAC THEN
513    FULL_SIMP_TAC (srw_ss()) [vars_FOLDL, pred_setTheory.EXTENSION] THEN
514    METIS_TAC []
515  ]);
516
517val (mpbeta_rules, mpbeta_ind, mpbeta_cases) = Hol_reln`
518  (!M N M'. mpbeta M M' ==> mpbeta (App M N) (App M' N)) /\
519  (!M N N'. mpbeta N N' ==> mpbeta (App M N) (App M N')) /\
520  (!u v M N p. ~(p IN params M) /\ ~(p IN params N) /\
521               mpbeta (vsub (Parameter p) u M) (vsub (Parameter p) v N) ==>
522               mpbeta (Abs u M) (Abs v N)) /\
523  (!x M N. vclosed (Abs x M) /\ vclosed N ==>
524           mpbeta (App (Abs x M) N) (vsub N x M))
525`;
526
527open chap3Theory
528val (convert_rules, convert_ind, convert_cases) = Hol_reln`
529  (!p. convert (Parameter p) (VAR p)) /\
530  (!t1 t2 M N. convert t1 M /\ convert t2 N ==>
531               convert (App t1 t2) (M @@ N)) /\
532  (!u v t M. ~(u IN params t) /\ convert (vsub (Parameter u) v t) M ==>
533             convert (Abs v t) (LAM u M))
534`;
535
536val convert_param = Store_thm(
537  "convert_param",
538  ``convert (Parameter p) t = (t = VAR p)``,
539  ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][]);
540
541val convert_app = store_thm(
542  "convert_app",
543  ``convert (App M N) t = ?t0 t1. convert M t0 /\ convert N t1 /\
544                                  (t = t0 @@ t1)``,
545  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN
546  SRW_TAC [][] THEN METIS_TAC []);
547
548val convert_abs = save_thm(
549  "convert_abs",
550  (SIMP_RULE (srw_ss()) [] o Q.SPEC `Abs v M`) convert_cases)
551
552val UNION_DELETE = prove(
553  ``(s UNION t) DELETE e = (s DELETE e) UNION (t DELETE e)``,
554  SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []);
555
556val params_vsub = store_thm(
557  "params_vsub",
558  ``!t p v. ~(p IN params t) ==>
559            (params (vsub (Parameter p) v t) DELETE p = params t)``,
560  Induct THEN SRW_TAC [][UNION_DELETE] THEN
561  SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []);
562
563val convert_MPpm = prove(
564  ``!t M. convert t M ==> !pi. convert (MPpm pi t) (tpm pi M)``,
565  HO_MATCH_MP_TAC convert_ind THEN
566  SRW_TAC [][convert_rules, MPpm_vsub] THEN
567  MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN
568  SRW_TAC [][IN_params_MPpm]);
569
570val convert_MPpm_E = Store_thm(
571  "convert_MPpm_E",
572  ``convert (MPpm pi t) (tpm pi M) = convert t M``,
573  METIS_TAC [convert_MPpm, pmact_inverse]);
574
575val convert_strong_ind = store_thm(
576  "convert_strong_ind",
577  ``!P f. (!x. FINITE (f x)) /\
578          (!p c. P (Parameter p) (VAR p) c) /\
579          (!t1 t2 M N c.
580               (!d1. P t1 M d1) /\ convert t1 M /\
581               (!d2. P t2 N d2) /\ convert t2 N ==>
582               P (App t1 t2) (M @@ N) c) /\
583          (!u v t M c. ~(u IN params t) /\ ~(u IN f c) /\
584                       convert (vsub (Parameter u) v t) M /\
585                       (!d. P (vsub (Parameter u) v t) M d) ==>
586                       P (Abs v t) (LAM u M) c)
587        ==>
588          !t M. convert t M ==> !c. P t M c``,
589  REPEAT GEN_TAC THEN STRIP_TAC THEN
590  Q_TAC SUFF_TAC `!t M. convert t M ==>
591                        convert t M /\
592                        !c pi. P (MPpm pi t) (tpm pi M) c`
593        THEN1 METIS_TAC [pmact_nil] THEN
594  HO_MATCH_MP_TAC convert_ind THEN
595  SRW_TAC [][convert_rules, MPpm_vsub] THEN
596  Q_TAC (NEW_TAC "z") `FV (tpm pi M) UNION f c UNION params (MPpm pi t)` THEN
597  `LAM (lswapstr pi u) (tpm pi M) = LAM z (tpm [(z, lswapstr pi u)] (tpm pi M))`
598     by SRW_TAC [][termTheory.tpm_ALPHA] THEN
599  SRW_TAC [][] THEN
600  `MPpm ((z,lswapstr pi u)::pi) t = MPpm [(z,lswapstr pi u)] (MPpm pi t)`
601     by SRW_TAC [][GSYM pmact_decompose] THEN
602  ` _ = MPpm pi t`
603     by SRW_TAC [][MPpm_fresh, IN_params_MPpm] THEN
604  FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][]
605    THEN1 (`convert (MPpm ((z,lswapstr pi u)::pi) (vsub (Parameter u) v t))
606                    (tpm ((z,lswapstr pi u)::pi) M)`
607              by METIS_TAC [convert_MPpm_E] THEN
608           POP_ASSUM MP_TAC THEN
609           ASM_SIMP_TAC bool_ss [MPpm_vsub] THEN
610           SRW_TAC [][GSYM pmact_decompose]) THEN
611  FIRST_X_ASSUM (Q.SPECL_THEN [`d`, `((z,lswapstr pi u)::pi)`] MP_TAC) THEN
612  SRW_TAC [][GSYM pmact_decompose]);
613
614val convert_params = store_thm(
615  "convert_params",
616  ``!t M. convert t M ==> (params t = FV M)``,
617  HO_MATCH_MP_TAC convert_ind THEN
618  SRW_TAC [][] THEN METIS_TAC [params_vsub]);
619
620val vclosed_convert = store_thm(
621  "vclosed_convert",
622  ``!t. vclosed t ==> ?M. convert t M``,
623  HO_MATCH_MP_TAC vclosed_strong_ind THEN Q.EXISTS_TAC `{}` THEN
624  SRW_TAC [][] THEN METIS_TAC [convert_rules]);
625
626val convert_vclosed = store_thm(
627  "convert_vclosed",
628  ``!t M. convert t M ==> vclosed t``,
629  HO_MATCH_MP_TAC convert_ind THEN SRW_TAC [][vclosed_abs] THEN
630  METIS_TAC []);
631
632val convert_vsub = prove(
633  ``!t M. convert t M ==>
634          !t0p1p2 v p1 p2 t0.
635              (t0p1p2 = (t0,p1,p2)) /\
636              (vsub (Parameter p1) v t0 = t) /\
637              ~(p1 IN params t0) /\ ~(p2 IN params t0) ==>
638              convert (vsub (Parameter p2) v t0) (tpm [(p1,p2)] M)``,
639  HO_MATCH_MP_TAC convert_strong_ind THEN
640  Q.EXISTS_TAC `\ (t0,p1,p2). {p1;p2} UNION params t0` THEN
641  SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
642  REPEAT CONJ_TAC THENL [
643    (* parameter case *)
644    SRW_TAC [][pvsub_eq_param] THEN
645    FULL_SIMP_TAC (srw_ss()) [convert_rules],
646
647    (* App case *)
648    SRW_TAC [][pvsub_eq_app] THEN
649    FULL_SIMP_TAC (srw_ss()) [convert_rules],
650
651    (* Abs case *)
652    MAP_EVERY Q.X_GEN_TAC [`u`, `v`, `t`, `M`, `t0`, `p1`, `p2`] THEN
653    STRIP_TAC THEN Q.X_GEN_TAC `v'` THEN STRIP_TAC THEN
654    FULL_SIMP_TAC (srw_ss()) [pvsub_eq_abs] THENL [
655      SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
656      MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN
657      SRW_TAC [][notin_pvsub_I] THEN
658      METIS_TAC [independent_pvsub, notin_pvsub_I],
659
660      MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN
661      SRW_TAC [][] THEN
662      FULL_SIMP_TAC (srw_ss()) [] THEN
663      `convert (MPpm [(p1,p2)] (vsub (Parameter u) v t))
664               (tpm [(p1,p2)] M)`
665         by SRW_TAC [][] THEN
666      Q_TAC SUFF_TAC `MPpm [(p1,p2)] (vsub (Parameter u) v t) =
667                      vsub (Parameter u) v t`
668            THEN1 METIS_TAC [] THEN
669      SRW_TAC [][MPpm_vsub]
670    ]
671  ]);
672
673val convert_vsub_thm = save_thm(
674  "convert_vsub_thm",
675  SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] convert_vsub)
676
677val convert_unique = store_thm(
678  "convert_unique",
679  ``!t M. convert t M ==> !N. convert t N ==> (M = N)``,
680  HO_MATCH_MP_TAC convert_ind THEN REPEAT CONJ_TAC THENL [
681    ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][],
682    REPEAT GEN_TAC THEN STRIP_TAC THEN
683    ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][] THEN
684    SRW_TAC [][],
685    REPEAT GEN_TAC THEN STRIP_TAC THEN
686    ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][] THEN
687    SRW_TAC [][termTheory.LAM_eq_thm] THEN
688    Cases_on `u = u'` THEN1 METIS_TAC [] THEN
689    ASM_SIMP_TAC (srw_ss()) [] THEN
690    `FV M' = params (vsub (Parameter u') v t)`
691      by METIS_TAC [convert_params] THEN
692    SRW_TAC [][notin_pvsub_I] THEN
693    METIS_TAC [convert_vsub_thm, pmact_flip_args]
694  ]);
695
696val convert_onto = store_thm(
697  "convert_onto",
698  ``!M. ?t. convert t M``,
699  HO_MATCH_MP_TAC termTheory.simple_induction THEN REPEAT STRIP_TAC THENL [
700    Q.EXISTS_TAC `Parameter s` THEN SRW_TAC [][convert_rules],
701    Q.EXISTS_TAC `App t t'` THEN SRW_TAC [][convert_rules],
702    Q.SPECL_THEN [`t`, `v`]
703                 (Q.X_CHOOSE_THEN `u` (Q.X_CHOOSE_THEN `t0` STRIP_ASSUME_TAC))
704                 shape_lemma THEN
705    SRW_TAC [][] THEN
706    Q.EXISTS_TAC `Abs u t0` THEN METIS_TAC [convert_rules]
707  ])
708
709val params_vsub_upperbound = prove(
710  ``p IN params (vsub N v M) ==> p IN params N \/ p IN params M``,
711  Induct_on `M` THEN SRW_TAC [][] THEN METIS_TAC []);
712
713val params_vsub_lowerbound = prove(
714  ``p IN params M ==> p IN params (vsub N v M)``,
715  Induct_on `M` THEN SRW_TAC [][] THEN METIS_TAC []);
716
717val mpbeta_params = store_thm(
718  "mpbeta_params",
719  ``!t u. mpbeta t u ==> !p. p IN params u ==> p IN params t``,
720  HO_MATCH_MP_TAC mpbeta_ind THEN SRW_TAC [][] THENL [
721    METIS_TAC [],
722    METIS_TAC [],
723    METIS_TAC [],
724    METIS_TAC [],
725    `p' IN params (Parameter p) \/ p' IN params M`
726       by METIS_TAC [params_vsub_lowerbound, params_vsub_upperbound] THEN
727    FULL_SIMP_TAC (srw_ss()) [],
728    METIS_TAC [params_vsub_upperbound]
729  ]);
730
731val vsub_vclosed = store_thm(
732  "vsub_vclosed",
733  ``!t. vclosed t ==> (vsub t' v t = t)``,
734  REPEAT STRIP_TAC THEN IMP_RES_TAC vclosed_empty_vars THEN
735  SRW_TAC [][vsub_14a]);
736
737val general_vsub_commute = store_thm(
738  "general_vsub_commute",
739  ``vclosed t1 /\ vclosed t2 /\ ~(v1 = v2) ==>
740    (vsub t1 v1 (vsub t2 v2 t) = vsub t2 v2 (vsub t1 v1 t))``,
741  Induct_on `t` THEN SRW_TAC [][vsub_vclosed] THEN METIS_TAC []);
742
743val convert_sub = store_thm(
744  "convert_sub",
745  ``~(p IN params t1) /\
746    convert (vsub (Parameter p) v t1) M /\
747    convert t2 N ==>
748    convert (vsub t2 v t1) ([N/p] M)``,
749  Q_TAC SUFF_TAC
750        `!t M. convert t M ==>
751               !t1pt2 t1 t2 p v N.
752                  (t1pt2 = (t1,p,t2)) /\
753                  ~(p IN params t1) /\
754                  (vsub (Parameter p) v t1 = t) /\
755                  convert t2 N ==>
756                  convert (vsub t2 v t1) ([N/p] M)`
757        THEN1 SRW_TAC [][] THEN
758  HO_MATCH_MP_TAC convert_strong_ind THEN
759  Q.EXISTS_TAC `\ (t1,p,t2). {p} UNION params t1 UNION params t2` THEN
760  ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
761  SRW_TAC [][pvsub_eq_param, pvsub_eq_app, pvsub_eq_abs] THEN
762  FULL_SIMP_TAC (srw_ss()) [termTheory.SUB_THM, convert_rules] THENL [
763    `FV N = params p_2` by SRW_TAC [][convert_params] THEN
764    SRW_TAC [][termTheory.SUB_THM] THEN
765    MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN
766    `~(u IN params (vsub p_2 v' M0))`
767      by METIS_TAC [params_vsub_upperbound] THEN
768    SRW_TAC [][] THEN
769    `vclosed p_2` by METIS_TAC [convert_vclosed] THEN
770    `vsub (Parameter u) v (vsub p_2 v' M0) =
771     vsub p_2 v' (vsub (Parameter u) v M0)`
772       by SRW_TAC [][general_vsub_commute] THEN
773    SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
774    SRW_TAC [][general_vsub_commute, notin_pvsub_I],
775
776    `FV N = params p_2` by SRW_TAC [][convert_params] THEN
777    SRW_TAC [][termTheory.SUB_THM] THEN
778    MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN
779    Q_TAC SUFF_TAC `~(p_1' IN FV M)` THEN1 SRW_TAC [][termTheory.lemma14b] THEN
780    `FV M = params (vsub (Parameter u) v t)`
781       by SRW_TAC [][convert_params] THEN
782    SRW_TAC [][notin_pvsub_I]
783  ]);
784
785
786val mpbeta_MPpm = prove(
787  ``!t u. mpbeta t u ==> !pi. mpbeta (MPpm pi t) (MPpm pi u)``,
788  HO_MATCH_MP_TAC mpbeta_ind THEN
789  SRW_TAC [][mpbeta_rules, MPpm_vsub] THENL [
790    MATCH_MP_TAC (List.nth(CONJUNCTS mpbeta_rules, 2)) THEN
791    Q.EXISTS_TAC `stringpm pi p` THEN SRW_TAC [][IN_params_MPpm],
792    MATCH_MP_TAC (last (CONJUNCTS mpbeta_rules)) THEN
793    `MPpm pi (Abs x M) = Abs x (MPpm pi M)` by SRW_TAC [][] THEN
794    METIS_TAC [vclosed_MPpm]
795  ]);
796
797val mpbeta_strong_ind =
798    IndDefLib.derive_strong_induction(mpbeta_rules, mpbeta_ind)
799
800val mpbeta_ccbeta = store_thm(
801  "mpbeta_ccbeta",
802  ``!t u. mpbeta t u ==>
803          !M N. convert t M /\ convert u N ==> compat_closure beta M N``,
804  HO_MATCH_MP_TAC mpbeta_strong_ind THEN
805  SRW_TAC [][compat_closure_rules, convert_abs, convert_app] THENL [
806    METIS_TAC [compat_closure_rules, convert_unique],
807    METIS_TAC [compat_closure_rules, convert_unique],
808    SRW_TAC [boolSimps.DNF_ss][cc_beta_thm, termTheory.LAM_eq_thm,
809                               termTheory.tpm_eqr] THEN
810    Cases_on `u' = u''` THEN ASM_SIMP_TAC (srw_ss()) [] THENL [
811      SRW_TAC [][] THEN
812      `convert (vsub (Parameter p) u M) (tpm [(p,u')] M'') /\
813       convert (vsub (Parameter p) v N) (tpm [(p,u')] M''')`
814         by METIS_TAC [convert_vsub_thm, pmact_flip_args] THEN
815      METIS_TAC [cc_beta_tpm_eqn, pmact_inverse],
816      `~(u' IN FV M''')`
817        by (`FV M''' = params (vsub (Parameter u'') v N)`
818               by SRW_TAC [][convert_params] THEN
819            SRW_TAC [][] THEN
820            Cases_on `u' = p` THEN1 SRW_TAC [][notin_pvsub_I] THEN
821            `mpbeta (MPpm [(u'',p)] (vsub (Parameter p) u M))
822                    (MPpm [(u'',p)] (vsub (Parameter p) v N))`
823               by SRW_TAC [][mpbeta_MPpm] THEN
824            POP_ASSUM MP_TAC THEN
825            SRW_TAC [][MPpm_vsub, MPpm_fresh] THEN
826            Q_TAC SUFF_TAC
827                  `~(u' IN params (vsub (Parameter u'') u (MPpm [(u'',p)] M)))`
828                  THEN1 METIS_TAC [mpbeta_params] THEN
829            SRW_TAC [][notin_pvsub_I, IN_params_MPpm]) THEN
830      `convert (vsub (Parameter p) u M) (tpm [(u',p)] M'') /\
831       convert (vsub (Parameter p) v N) (tpm [(u'',p)] M''')`
832         by METIS_TAC [convert_vsub_thm] THEN
833      `compat_closure beta (tpm [(u',p)] M'') (tpm [(u'',p)] M''')`
834         by METIS_TAC [] THEN
835      `compat_closure beta M'' (tpm [(u',p)] (tpm [(u'',p)] M'''))`
836         by METIS_TAC [cc_beta_tpm, pmact_sing_inv] THEN
837      Q_TAC SUFF_TAC `tpm [(u',p)] (tpm [(u'',p)] M''') = tpm [(u'',u')] M'''`
838            THEN1 METIS_TAC [] THEN
839      Cases_on `p = u'` THEN1 SRW_TAC [][] THEN
840      Cases_on `p = u''` THEN1 SRW_TAC [][pmact_flip_args] THEN
841      ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN
842      SRW_TAC [][] THEN
843      `~(p IN FV M''') /\ ~(u' IN FV M''')`
844        by METIS_TAC [convert_params, notin_pvsub_I] THEN
845      SRW_TAC [][termTheory.tpm_fresh]
846    ],
847
848    `N' = [t1/u]M''` by METIS_TAC [convert_sub, convert_unique] THEN
849    SRW_TAC [][cc_beta_thm] THEN METIS_TAC []
850  ]);
851
852
853val alpha_def = Define`alpha t1 t2 = ?M. convert t1 M /\ convert t2 M`
854
855val alpha_trans = store_thm(
856  "alpha_trans",
857  ``alpha t1 t2 /\ alpha t2 t3 ==> alpha t1 t3``,
858  SRW_TAC [][alpha_def] THEN METIS_TAC [convert_unique]);
859
860val alpha_sym = store_thm(
861  "alpha_sym",
862  ``alpha t1 t2 ==> alpha t2 t1``,
863  SRW_TAC [][alpha_def] THEN METIS_TAC []);
864
865val alpha_prefl = store_thm(
866  "alpha_prefl",
867  ``alpha t t = vclosed t``,
868  SRW_TAC [][alpha_def] THEN METIS_TAC [convert_vclosed, vclosed_convert]);
869
870val convert_to_app = prove(
871  ``convert t (M1 @@ M2) = ?t1 t2. (t = App t1 t2) /\ convert t1 M1 /\
872                                   convert t2 M2``,
873  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN
874  SRW_TAC [][]);
875
876val convert_to_lam = prove(
877  ``convert t (LAM v M) = ?u t0. (t = Abs u t0) /\ ~(v IN params t0) /\
878                                 convert (vsub (Parameter v) u t0) M``,
879  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN
880  SRW_TAC [boolSimps.DNF_ss][termTheory.LAM_eq_thm, termTheory.tpm_eqr] THEN
881  SRW_TAC [][EQ_IMP_THM] THEN
882  Q_TAC SUFF_TAC `~(v IN params t')`
883        THEN1 METIS_TAC [convert_vsub_thm, pmact_flip_args,
884                         pmact_sing_inv] THEN
885  `~(v IN FV (tpm [(v,u)] M))` by SRW_TAC [][] THEN
886  `~(v IN params (vsub (Parameter u) v' t'))`
887    by METIS_TAC [convert_params] THEN
888  METIS_TAC [params_vsub_lowerbound]);
889
890val alpha_app = prove(
891  ``alpha (App t1 t2) t = ?t1' t2'. (t = App t1' t2') /\
892                                    alpha t1 t1' /\ alpha t2 t2'``,
893  SRW_TAC [boolSimps.DNF_ss][alpha_def, convert_app, convert_to_app] THEN
894  METIS_TAC []);
895
896(* Curiously, only need to alpha-convert after a reduction, and not
897   before. *)
898val ccbeta_beta = store_thm(
899  "ccbeta_beta",
900  ``!M N. compat_closure beta M N ==>
901          !t u. convert t M /\ convert u N ==>
902                (alpha O mpbeta) t u``,
903  HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN
904  SRW_TAC [][relationTheory.O_DEF, convert_to_app, convert_to_lam] THENL [
905    IMP_RES_TAC convert_vclosed THEN
906    Q.EXISTS_TAC `vsub t2 u' t0` THEN CONJ_TAC THENL [
907      MATCH_MP_TAC (last (CONJUNCTS mpbeta_rules)) THEN
908      SRW_TAC [][vclosed_abs] THEN METIS_TAC [],
909      SRW_TAC [][alpha_def] THEN METIS_TAC [convert_sub]
910    ],
911
912    `?y. mpbeta t1 y /\ alpha y t1'` by METIS_TAC [] THEN
913    Q.EXISTS_TAC `App y t2` THEN
914    IMP_RES_TAC convert_vclosed THEN
915    SRW_TAC [][alpha_app, alpha_prefl] THEN
916    SRW_TAC [][mpbeta_rules, alpha_app, alpha_prefl] THEN
917    SRW_TAC [][alpha_def] THEN METIS_TAC [],
918
919    `?y. mpbeta t2 y /\ alpha y t2'` by METIS_TAC [] THEN
920    Q.EXISTS_TAC `App t1 y` THEN
921    IMP_RES_TAC convert_vclosed THEN
922    SRW_TAC [][alpha_app, alpha_prefl] THEN
923    SRW_TAC [][mpbeta_rules, alpha_app, alpha_prefl] THEN
924    SRW_TAC [][alpha_def] THEN METIS_TAC [],
925
926    `?y. mpbeta (vsub (Parameter v) u' t0) y /\
927         alpha y (vsub (Parameter v) u'' t0')`
928       by METIS_TAC [] THEN
929    `?v1 t1. (y = vsub (Parameter v) v1 t1) /\ ~(v IN params t1)`
930       by METIS_TAC [shape_lemma] THEN
931    Q.EXISTS_TAC `Abs v1 t1` THEN CONJ_TAC THENL [
932       MATCH_MP_TAC (List.nth(CONJUNCTS mpbeta_rules, 2)) THEN
933       Q.EXISTS_TAC `v` THEN SRW_TAC [][],
934       ALL_TAC
935    ] THEN
936    SRW_TAC [boolSimps.DNF_ss][alpha_def, convert_abs] THEN
937    MAP_EVERY Q.EXISTS_TAC [`v`, `N`, `v`, `N`] THEN
938    FULL_SIMP_TAC (srw_ss()) [alpha_def] THEN METIS_TAC [convert_unique]
939  ]);
940
941
942val _ = export_theory()
943