1(* this is an -*- sml -*- file *)
2(* script file establishing a type of lambda-terms on top of the
3   GM base.  Does this by defining the predicate "const-free" *)
4
5open HolKernel Parse boolLib bossLib BasicProvers boolSimps NEWLib
6open ncTheory swapTheory binderLib
7
8val _ = new_theory "gmterm";
9
10val (constfree_rules, constfree_ind, constfree_cases) = Hol_reln`
11  (!s. constfree (nc$VAR s)) /\
12  (!M N. constfree M /\ constfree N ==> constfree (M @@ N)) /\
13  (!v M. constfree M ==> constfree (LAM v M))
14`;
15
16val constfree_swap_I = prove(
17  ``!M. constfree M ==> !x y. constfree (swap x y M)``,
18  HO_MATCH_MP_TAC constfree_ind THEN SRW_TAC [][constfree_rules]);
19
20val constfree_thm = store_thm(
21  "constfree_thm",
22  ``(constfree (nc$VAR s) = T) /\
23    (constfree (M @@ N) = constfree M /\ constfree N) /\
24    (constfree (LAM v M) = constfree M) /\
25    (constfree (CON k) = F)``,
26  REPEAT CONJ_TAC THEN
27  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [constfree_cases])) THEN
28  SRW_TAC [][] THEN EQ_TAC THENL [
29    SRW_TAC [][LAM_INJ_swap] THEN
30    METIS_TAC [lswap_def, constfree_swap_I],
31    METIS_TAC []
32  ]);
33val _ = export_rewrites ["constfree_thm"]
34
35val lswap_constfree = prove(
36  ``!t. constfree (lswap pi t) = constfree t``,
37  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
38val _ = augment_srw_ss [rewrites [lswap_constfree]]
39
40val swap_constfree = prove(
41  ``constfree (swap x y t) = constfree t``,
42  MP_TAC (Q.INST [`pi` |-> `[(x,y)]`] (SPEC_ALL lswap_constfree)) THEN
43  REWRITE_TAC [lswap_def]);
44val _ = augment_srw_ss [rewrites [swap_constfree]]
45
46val term_ax = new_type_definition(
47  "term",
48  prove(``?t : one nc. constfree t``,
49        Q.EXISTS_TAC `nc$VAR s` THEN SRW_TAC [][]))
50
51val term_bij = define_new_type_bijections
52                 {ABS = "to_term", REP = "from_term",
53                  name = "term_bij", tyax = term_ax}
54
55val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "nc"})
56            ["LAM", "VAR", "CON", "@@", "FV", "SUB", "ABS", "size"]
57
58val VAR_def = Define`VAR s = to_term (nc$VAR s)`
59val APP_def = xDefine "APP"
60                      `M @@ N = to_term (nc$@@ (from_term M) (from_term N))`
61val LAM_def = Define`LAM v t = to_term (nc$LAM v (from_term t))`
62
63val fromto_inverse = prove(
64  ``constfree t ==> (from_term (to_term t) = t)``,
65  METIS_TAC [term_bij]);
66
67val tofrom_inverse = prove(
68  ``to_term (from_term t) = t``,
69  SRW_TAC [][term_bij]);
70val _ = augment_srw_ss [rewrites [tofrom_inverse]]
71
72val constfree_from_term = prove(
73  ``constfree (from_term M)``,
74  SRW_TAC [][term_bij]);
75val _ = augment_srw_ss [rewrites [constfree_from_term]]
76
77val from_term_11 = prove(
78  ``(from_term t = from_term u) = (t = u)``,
79  METIS_TAC [term_bij]);
80
81val term_11 = store_thm(
82  "term_11",
83  ``((VAR s = VAR t) = (s = t)) /\
84    ((M1 @@ N1 = M2 @@ N2) = (M1 = M2) /\ (N1 = N2)) /\
85    ((LAM v M1 = LAM v M2) = (M1 = M2))``,
86  SRW_TAC [][VAR_def, APP_def, LAM_def, EQ_IMP_THM] THEN
87  POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN
88  SRW_TAC [][fromto_inverse] THEN
89  FULL_SIMP_TAC (srw_ss()) [from_term_11]);
90val _ = export_rewrites ["term_11"]
91
92val term_distinct = store_thm(
93  "term_distinct",
94  ``~(VAR s = M @@ N) /\ ~(VAR s = LAM v t) /\ ~(M @@ N = LAM v t)``,
95  SRW_TAC [][VAR_def, APP_def, LAM_def] THEN STRIP_TAC THEN
96  POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN
97  SRW_TAC [][fromto_inverse]);
98val _ = export_rewrites ["term_distinct"]
99
100val simple_induction = store_thm(
101  "simple_induction",
102  ``!P. (!s. P (VAR s)) /\
103        (!M N. P M /\ P N ==> P (M @@ N)) /\
104        (!v M. P M ==> P (LAM v M)) ==>
105        !M. P M``,
106  SIMP_TAC (srw_ss())[VAR_def, APP_def, LAM_def] THEN
107  GEN_TAC THEN STRIP_TAC THEN
108  Q_TAC SUFF_TAC `!M. constfree M ==> P (to_term M)`
109        THEN1 (REPEAT STRIP_TAC THEN
110               `M = to_term (from_term M)` by METIS_TAC [term_bij] THEN
111               POP_ASSUM SUBST1_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
112               SRW_TAC [][term_bij]) THEN
113  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [
114    `(M = from_term (to_term M)) /\ (M' = from_term (to_term M'))`
115      by METIS_TAC [term_bij] THEN
116    NTAC 2 (POP_ASSUM SUBST1_TAC) THEN
117    SRW_TAC [][],
118    `(M = from_term (to_term M))` by METIS_TAC [term_bij] THEN
119    POP_ASSUM SUBST1_TAC THEN SRW_TAC [][]
120  ]);
121
122val tpm_def = Define`tpm pi t = to_term (lswap pi (from_term t))`
123
124
125
126val tpm_thm = store_thm(
127  "tpm_thm",
128  ``(tpm pi (VAR s) = VAR (raw_lswapstr pi s)) /\
129    (tpm pi (M @@ N) = tpm pi M @@ tpm pi N) /\
130    (tpm pi (LAM v M) = LAM (raw_lswapstr pi v) (tpm pi M))``,
131  SRW_TAC [][tpm_def, LAM_def, APP_def, VAR_def, fromto_inverse]);
132val _ = export_rewrites ["tpm_thm"]
133
134val FV_def = Define`FV t = nc$FV (from_term t)`
135
136val FV_thm = store_thm(
137  "FV_thm",
138  ``(FV (VAR s) = {s}) /\
139    (FV (M @@ N) = FV M UNION FV N) /\
140    (FV (LAM v M) = FV M DELETE v)``,
141  SRW_TAC [][FV_def, LAM_def, APP_def, VAR_def, fromto_inverse]);
142val _ = export_rewrites ["FV_thm"]
143
144val FINITE_FV = store_thm(
145  "FINITE_FV",
146  ``FINITE (FV t)``,
147  SRW_TAC [][FV_def]);
148val _ = export_rewrites ["FINITE_FV"]
149
150val constfree_SUB = prove(
151  ``!t. constfree t /\ constfree u ==> constfree (nc$SUB u x t)``,
152  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `x INSERT nc$FV u` THEN
153  SRW_TAC [][SUB_THM, SUB_VAR]);
154val _ = augment_srw_ss [rewrites [constfree_SUB]]
155
156val SUB_def = Define`[N/v] M = to_term (nc$SUB (from_term N) v (from_term M))`;
157
158val SUB_THM = store_thm(
159  "SUB_THM",
160  ``([u/x] (VAR x) = u) /\
161    (~(x = y) ==> ([u/x] (VAR y) = VAR y)) /\
162    ([u/x] (s @@ t) = [u/x]s @@ [u/x] t) /\
163    ([u/x] (LAM x t) = LAM x t) /\
164    (~(x = y) /\ ~(y IN FV u) ==> ([u/x] (LAM y t) = LAM y ([u/x] t)))``,
165  SRW_TAC [][FV_def, SUB_def, LAM_def, VAR_def, APP_def,
166             fromto_inverse, ncTheory.SUB_THM]);
167
168val SUB_VAR = store_thm(
169  "SUB_VAR",
170  ``[t/y] (VAR x) = if x = y then t else VAR x``,
171  SRW_TAC [][VAR_def, SUB_def, fromto_inverse, SUB_VAR]);
172
173val tpm_NIL = store_thm(
174  "tpm_NIL",
175  ``!t. tpm [] t = t``,
176  HO_MATCH_MP_TAC simple_induction THEN
177  SRW_TAC [][]);
178val _ = export_rewrites ["tpm_NIL"]
179
180val LAM_eq_thm = store_thm(
181  "LAM_eq_thm",
182  ``(LAM u M = LAM v N) = ((u = v) /\ (M = N)) \/
183                          (~(u = v) /\ ~(u IN FV N) /\ (M = tpm [(u,v)] N))``,
184  SRW_TAC [][LAM_def, FV_def, tpm_def, EQ_IMP_THM] THENL [
185    POP_ASSUM (MP_TAC o AP_TERM ``from_term``) THEN
186    SRW_TAC [][fromto_inverse, LAM_INJ_swap] THENL [
187      Cases_on `u = v` THEN FULL_SIMP_TAC (srw_ss()) [lswap_def] THEN
188      FIRST_X_ASSUM (MP_TAC o AP_TERM ``to_term``) THEN SRW_TAC [][],
189      FULL_SIMP_TAC (srw_ss()) [from_term_11]
190    ],
191    AP_TERM_TAC THEN SRW_TAC [][fromto_inverse, LAM_INJ_swap,
192                                lswap_def]
193  ]);
194
195val FV_tpm = store_thm(
196  "FV_tpm",
197  ``!t pi v. v IN FV (tpm pi t) = raw_lswapstr (REVERSE pi) v IN FV t``,
198  HO_MATCH_MP_TAC simple_induction THEN
199  SRW_TAC [][basic_swapTheory.raw_lswapstr_eql]);
200val _ = export_rewrites ["FV_tpm"]
201
202val tpm_inverse = store_thm(
203  "tpm_inverse",
204  ``!t pi. (tpm pi (tpm (REVERSE pi) t) = t) /\
205           (tpm (REVERSE pi) (tpm pi t) = t)``,
206  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
207val _ = export_rewrites ["tpm_inverse"]
208
209val tpm_eqr = store_thm(
210  "tpm_eqr",
211  ``(t = tpm pi u) = (tpm (REVERSE pi) t = u)``,
212  METIS_TAC [tpm_inverse]);
213
214val tpm_eql = store_thm(
215  "tpm_eql",
216  ``(tpm pi t = u) = (t = tpm (REVERSE pi) u)``,
217  METIS_TAC [tpm_inverse]);
218
219val tpm_flip_args = store_thm(
220  "tpm_flip_args",
221  ``!t. tpm ((y,x)::rest) t = tpm ((x,y)::rest) t``,
222  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
223
224val tpm_APPEND = store_thm(
225  "tpm_APPEND",
226  ``!t. tpm (p1 ++ p2) t = tpm p1 (tpm p2 t)``,
227  HO_MATCH_MP_TAC simple_induction THEN
228  SRW_TAC [][basic_swapTheory.raw_lswapstr_APPEND]);
229
230val tpm_CONS = store_thm(
231  "tpm_CONS",
232  ``tpm ((x,y)::pi) t = tpm [(x,y)] (tpm pi t)``,
233  SRW_TAC [][GSYM tpm_APPEND]);
234
235val tpm_sing_inv = store_thm(
236  "tpm_sing_inv",
237  ``tpm [h] (tpm [h] t) = t``,
238  ACCEPT_TAC
239    (SIMP_RULE list_ss [] (Q.INST [`pi` |-> `[h]`] (SPEC_ALL tpm_inverse))))
240val _ = export_rewrites ["tpm_sing_inv"]
241
242val nc_INDUCTION2 = store_thm(
243  "nc_INDUCTION2",
244  ``!P X. (!x. P (VAR x)) /\
245          (!t u. P t /\ P u ==> P (t @@ u)) /\
246          (!y u. ~(y IN X) /\ P u ==> P (LAM y u)) /\  FINITE X ==>
247          !u. P u``,
248  REPEAT GEN_TAC THEN STRIP_TAC THEN
249  Q_TAC SUFF_TAC `!u pi. P (tpm pi u)` THEN1 METIS_TAC [tpm_NIL] THEN
250  HO_MATCH_MP_TAC simple_induction THEN
251  SRW_TAC [][] THEN
252  Q_TAC (NEW_TAC "z") `raw_lswapstr pi v INSERT FV (tpm pi u) UNION X` THEN
253  Q_TAC SUFF_TAC `LAM (raw_lswapstr pi v) (tpm pi u) =
254                  LAM z (tpm ((z,raw_lswapstr pi v)::pi) u)`
255        THEN1 SRW_TAC [][] THEN
256  SRW_TAC [][LAM_eq_thm, basic_swapTheory.raw_lswapstr_APPEND] THENL [
257    FULL_SIMP_TAC (srw_ss()) [],
258    SRW_TAC [][tpm_eqr, tpm_flip_args, tpm_APPEND]
259  ]);
260
261val tpm_sing_to_back = store_thm(
262  "tpm_sing_to_back",
263  ``!t. tpm [(raw_lswapstr p u, raw_lswapstr p v)] (tpm p t) = tpm p (tpm [(u,v)] t)``,
264  HO_MATCH_MP_TAC simple_induction THEN
265  SRW_TAC [][basic_swapTheory.raw_lswapstr_sing_to_back]);
266
267val tpm_subst = store_thm(
268  "tpm_subst",
269  ``!N. tpm pi ([M/v] N) = [tpm pi M/raw_lswapstr pi v] (tpm pi N)``,
270  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
271  Q.EXISTS_TAC `v INSERT FV M` THEN
272  SRW_TAC [][SUB_THM, SUB_VAR]);
273
274val tpm_subst_out = store_thm(
275  "tpm_subst_out",
276  ``[M/v] (tpm pi N) =
277       tpm pi ([tpm (REVERSE pi) M/raw_lswapstr (REVERSE pi) v] N)``,
278  SRW_TAC [][tpm_subst])
279
280val tpm_idfront = store_thm(
281  "tpm_idfront",
282  ``!t. tpm ((v,v)::rest) t = tpm rest t``,
283  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
284val _ = export_rewrites ["tpm_idfront"]
285
286val tpm_fresh = store_thm(
287  "tpm_fresh",
288  ``!t. ~(x IN FV t) /\ ~(y IN FV t) ==> (tpm [(x,y)] t = t)``,
289  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN
290  SRW_TAC [][] THEN SRW_TAC [CONJ_ss][LAM_eq_thm, tpm_flip_args] THEN
291  Cases_on `x = v` THEN SRW_TAC [][] THEN
292  Cases_on `y = v` THEN SRW_TAC [][] THEN
293  FULL_SIMP_TAC (srw_ss()) [tpm_flip_args]);
294
295val tpm_apart = store_thm(
296  "tpm_apart",
297  ``!t. x IN FV t /\ ~(y IN FV t) ==> ~(tpm [(x,y)] t = t)``,
298  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [
299    METIS_TAC [],
300    METIS_TAC [],
301    SRW_TAC [][LAM_eq_thm] THEN
302    Cases_on `y = v` THEN SRW_TAC [][],
303    SRW_TAC [][LAM_eq_thm]
304  ]);
305
306val fresh_tpm_subst = store_thm(
307  "fresh_tpm_subst",
308  ``!M. ~(u IN FV M) ==> (tpm [(u,v)] M = [VAR u/v] M)``,
309  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
310  SRW_TAC [][SUB_THM, SUB_VAR]);
311
312val SIMPLE_ALPHA = store_thm(
313  "SIMPLE_ALPHA",
314  ``~(y IN FV u) ==> !x. LAM x u = LAM y ([VAR y/x] u)``,
315  SRW_TAC [][GSYM fresh_tpm_subst] THEN
316  SRW_TAC [CONJ_ss][LAM_eq_thm, tpm_flip_args]);
317
318val tpm_ALPHA = store_thm(
319  "tpm_ALPHA",
320  ``~(v IN FV u) ==> !x. LAM x u = LAM v (tpm [(v,x)] u)``,
321  SRW_TAC [][fresh_tpm_subst, SIMPLE_ALPHA]);
322
323val lemma14a = store_thm(
324  "lemma14a",
325  ``!t. [VAR v/v] t = t``,
326  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v}` THEN
327  SRW_TAC [][SUB_THM, SUB_VAR]);
328val _ = export_rewrites ["lemma14a"]
329
330val lemma14b = store_thm(
331  "lemma14b",
332  ``!M. ~(v IN FV M) ==> ([N/v] M = M)``,
333  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN
334  SRW_TAC [][SUB_THM, SUB_VAR]);
335
336open pred_setTheory
337
338val lemma14c = store_thm(
339  "lemma14c",
340  ``!t x u. x IN FV u ==> (FV ([t/x]u) = FV t UNION (FV u DELETE x))``,
341  NTAC 2 GEN_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN
342  Q.EXISTS_TAC `x INSERT FV t` THEN
343  SRW_TAC [][SUB_THM, SUB_VAR, EXTENSION] THENL [
344    Cases_on `x IN FV u'` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [],
345    Cases_on `x IN FV u` THEN SRW_TAC [][lemma14b] THEN METIS_TAC [],
346    METIS_TAC []
347  ]);
348
349val lemma15a = store_thm(
350  "lemma15a",
351  ``!M. ~(v IN FV M) ==> ([N/v]([VAR v/x]M) = [N/x]M)``,
352  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v} UNION FV N` THEN
353  SRW_TAC [][SUB_THM, SUB_VAR]);
354
355val lemma15b = store_thm(
356  "lemma15b",
357  ``~(v IN FV M) ==> ([VAR u/v]([VAR v/u] M) = M)``,
358  SRW_TAC [][lemma15a]);
359
360val FV_SUB = store_thm(
361  "FV_SUB",
362  ``!t u v. FV ([t/v] u) = if v IN FV u then FV t UNION (FV u DELETE v)
363                           else FV u``,
364  PROVE_TAC [lemma14b, lemma14c]);
365
366(* ----------------------------------------------------------------------
367    iterated substitutions (ugh)
368   ---------------------------------------------------------------------- *)
369
370val ISUB_def =
371 Define
372     `($ISUB t [] = t)
373  /\  ($ISUB t ((s,x)::rst) = $ISUB ([s/x]t) rst)`;
374
375val _ = set_fixity "ISUB" (Infixr 501);
376
377val DOM_DEF =
378 Define
379     `(DOM [] = {})
380  /\  (DOM ((x,y)::rst) = {y} UNION DOM rst)`;
381
382val FVS_DEF =
383 Define
384    `(FVS [] = {})
385 /\  (FVS ((t,x)::rst) = FV t UNION FVS rst)`;
386
387
388val FINITE_DOM = Q.store_thm("FINITE_DOM",
389 `!ss. FINITE (DOM ss)`,
390Induct THENL [ALL_TAC, Cases]
391   THEN RW_TAC std_ss [DOM_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_SING]);
392val _ = export_rewrites ["FINITE_DOM"]
393
394
395val FINITE_FVS = Q.store_thm("FINITE_FVS",
396`!ss. FINITE (FVS ss)`,
397Induct THENL [ALL_TAC, Cases]
398   THEN RW_TAC std_ss [FVS_DEF, FINITE_EMPTY, FINITE_UNION, FINITE_FV]);
399val _ = export_rewrites ["FINITE_FVS"]
400
401val ISUB_LAM = store_thm(
402  "ISUB_LAM",
403  ``!R x. ~(x IN (DOM R UNION FVS R)) ==>
404          !t. (LAM x t) ISUB R = LAM x (t ISUB R)``,
405  Induct THEN
406  ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD,
407                           DOM_DEF, FVS_DEF, SUB_THM]);
408
409(* ----------------------------------------------------------------------
410    size of a term
411   ---------------------------------------------------------------------- *)
412
413val size_def = Define`size t = nc$size (from_term t)`;
414
415val size_thm = store_thm(
416  "size_thm",
417  ``(size (VAR s) = 1) /\
418    (size (t @@ u) = size t + size u + 1) /\
419    (size (LAM v t) = size t + 1)``,
420  SRW_TAC [][size_def, ncTheory.size_thm, fromto_inverse, VAR_def, APP_def,
421             LAM_def]);
422val _ = export_rewrites ["size_thm"]
423
424val size_tpm = store_thm(
425  "size_tpm",
426  ``!t. size (tpm pi t) = size t``,
427  HO_MATCH_MP_TAC simple_induction THEN
428  SRW_TAC [][]);
429val _ = export_rewrites ["size_tpm"]
430
431val size_vsubst = store_thm(
432  "size_vsubst",
433  ``!t. size ([VAR v/u] t) = size t``,
434  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
435  SRW_TAC [][SUB_THM, SUB_VAR]);
436val _ = export_rewrites ["size_vsubst"]
437
438(* ----------------------------------------------------------------------
439    proving a recursion theorem
440   ---------------------------------------------------------------------- *)
441val gm_recursion = prove(
442  ``!var app lam.
443      ?hom : term -> 'b.
444        (!s. hom (VAR s) = var s) /\
445        (!t u. hom (t @@ u) = app (hom t) (hom u) t u) /\
446        !v t. hom (LAM v t) = lam (\y. hom ([VAR y/v] t))
447                                  (\y. [VAR y/v] t)``,
448  REPEAT GEN_TAC THEN
449  Q.SPECL_THEN [`\k. ARB`, `var`,
450                `\rt ru t u. app rt ru (to_term t) (to_term u)`,
451                `\rf tf. lam rf (to_term o tf)`] MP_TAC
452               (INST_TYPE [alpha |-> ``:one``] nc_RECURSION) THEN
453  DISCH_THEN (STRIP_ASSUME_TAC o CONJUNCT1 o CONV_RULE EXISTS_UNIQUE_CONV) THEN
454  Q.EXISTS_TAC `hom o from_term` THEN
455  SRW_TAC [][VAR_def, APP_def, LAM_def, fromto_inverse,
456             combinTheory.o_ABS_R, SUB_def]);
457
458val ABS_def = Define`ABS f = to_term (nc$ABS (from_term o f))`
459
460val ABS_axiom = prove(
461  ``gmterm$ABS (\y. [VAR y/v] t) = LAM v t``,
462  SRW_TAC [][LAM_def, ABS_def, SUB_def, combinTheory.o_ABS_R,
463             fromto_inverse, VAR_def, ncTheory.ABS_DEF]);
464
465
466val fresh_new_subst0 = prove(
467  ``FINITE X ==>
468    ((let v = NEW (FV (LAM x u) UNION X) in f v ([VAR v/x] u)) =
469     (let v = NEW (FV (LAM x u) UNION X) in f v (tpm [(v,x)] u)))``,
470  STRIP_TAC THEN NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN
471  SRW_TAC [][] THEN SRW_TAC [][fresh_tpm_subst]);
472
473val lemma = (SIMP_RULE bool_ss [ABS_axiom, fresh_new_subst0,
474                                ASSUME ``FINITE (X:string set)``]o
475             Q.INST [`lam'` |-> `lam`] o
476             Q.INST [`lam` |->
477                        `\r t. let v = NEW (FV (gmterm$ABS t) UNION X)
478                               in
479                                 lam' (r v) v (t v)`] o
480             INST_TYPE [beta |-> alpha] o
481             SPEC_ALL) gm_recursion
482
483val term_CASES = store_thm(
484  "term_CASES",
485  ``!t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/
486        (?v t0. t = LAM v t0)``,
487  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN METIS_TAC []);
488
489val pvh_induction = prove(
490  ``!P. (!s. P (VAR s)) /\ (!t u. P t /\ P u ==> P (t @@ u)) /\
491        (!v t. (!t'. (size t' = size t) ==> P t') ==> P (LAM v t)) ==>
492        !t. P t``,
493  REPEAT STRIP_TAC THEN measureInduct_on `size t` THEN
494  Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN
495  FULL_SIMP_TAC (srw_ss()) [] THEN
496  POP_ASSUM (fn th => FIRST_X_ASSUM MATCH_MP_TAC THEN ASSUME_TAC th) THEN
497  REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
498  SRW_TAC [numSimps.ARITH_ss][]);
499
500val swap_RECURSION = store_thm(
501  "swap_RECURSION",
502  ``swapping rswap rFV /\ FINITE X /\
503    (!s. rFV (var s) SUBSET s INSERT X) /\
504    (!t' u' t u.
505       rFV t' SUBSET FV t UNION X /\ rFV u' SUBSET FV u UNION X ==>
506       rFV (app t' u' t u) SUBSET FV t UNION FV u UNION X) /\
507    (!t' v t.
508       rFV t' SUBSET FV t UNION X ==>
509       rFV (lam t' v t) SUBSET FV t DELETE v UNION X) /\
510    (!s x y.
511       ~(x IN X) /\ ~(y IN X) ==>
512       (rswap x y (var s) = var (swapstr x y s))) /\
513    (!t t' u u' x y.
514       ~(x IN X) /\ ~(y IN X) ==>
515       (rswap x y (app t' u' t u) =
516        app (rswap x y t') (rswap x y u') (tpm [(x,y)] t) (tpm [(x,y)] u))) /\
517    (!t' t x y v.
518       ~(x IN X) /\ ~(y IN X) ==>
519       (rswap x y (lam t' v t) =
520        lam (rswap x y t') (swapstr x y v) (tpm[(x,y)] t))) ==>
521    ?hom.
522      ((!s. hom (VAR s) = var s) /\
523       (!t u. hom (t @@ u) = app (hom t) (hom u) t u) /\
524       !v t. ~(v IN X) ==> (hom (LAM v t) = lam (hom t) v t)) /\
525      (!t x y.
526         ~(x IN X) /\ ~(y IN X) ==>
527         (hom (tpm [(x,y)] t) = rswap x y (hom t)))``,
528  REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC lemma THEN
529  Q.EXISTS_TAC `hom` THEN ASM_SIMP_TAC bool_ss [] THEN
530  `!t. rFV (hom t) SUBSET FV t UNION X`
531     by (HO_MATCH_MP_TAC pvh_induction THEN ASM_SIMP_TAC (srw_ss()) [] THEN
532         REPEAT CONJ_TAC THENL [
533           ASM_SIMP_TAC (srw_ss()) [INSERT_UNION_EQ],
534           REPEAT STRIP_TAC THEN NEW_ELIM_TAC THEN
535           ASM_SIMP_TAC (srw_ss()) [] THEN Q.X_GEN_TAC `u` THEN
536           REPEAT STRIP_TAC THENL [
537             SRW_TAC [][LET_THM] THEN
538             `FV t DELETE v = FV (LAM v t)`  by SRW_TAC [][] THEN
539             POP_ASSUM SUBST_ALL_TAC THEN
540             `LAM v t = LAM u (tpm [(u,v)] t)` by SRW_TAC [][tpm_ALPHA] THEN
541             POP_ASSUM SUBST1_TAC THEN SRW_TAC [][],
542             SRW_TAC [][LET_THM]
543           ]
544         ]) THEN
545  ASM_REWRITE_TAC [] THEN
546  `!x r. rswap x x r = r` by FULL_SIMP_TAC (srw_ss()) [swapping_def] THEN
547  `!t x y. ~(x IN X) /\ ~(y IN X) ==>
548           (hom (tpm [(x,y)] t) = rswap x y (hom t))`
549     by (HO_MATCH_MP_TAC pvh_induction THEN REPEAT CONJ_TAC THEN
550         TRY (SRW_TAC [][] THEN NO_TAC) THEN
551         REPEAT STRIP_TAC THEN
552         Cases_on `x = y` THEN1 SRW_TAC [][] THEN
553         Q_TAC (NEW_TAC "z") `{x;y;v} UNION FV t UNION X` THEN
554         `LAM v t = LAM z ([VAR z/v] t)` by SRW_TAC [][SIMPLE_ALPHA] THEN
555         Q.ABBREV_TAC `M = [VAR z/v] t` THEN
556         `size t = size M` by SRW_TAC [][Abbr`M`] THEN
557         Q.RM_ABBREV_TAC `M` THEN
558         NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN
559         `hom (tpm [(x,y)] (LAM z M)) = rswap x y (lam (hom M) z M)`
560            by (SRW_TAC [][LET_THM] THEN
561                NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN
562                Q.X_GEN_TAC `a` THEN
563                REVERSE (SRW_TAC [][]) THEN1 SRW_TAC [][] THEN
564                Q.MATCH_ABBREV_TAC
565                  `lam (rswap a z Y) a (tpm [(a,z)] M') = R` THEN
566                Q.UNABBREV_TAC `R` THEN
567                `lam (rswap a z Y) a (tpm [(a,z)] M') =
568                   lam (rswap a z Y) (swapstr a z z) (tpm [(a,z)] M')`
569                  by SRW_TAC [][] THEN
570                ` _ = rswap a z (lam Y z M')`
571                  by POP_ASSUM (fn th => SRW_TAC [][] THEN ASSUME_TAC th) THEN
572                POP_ASSUM SUBST1_TAC THEN
573                MATCH_MP_TAC swapping_implies_identity_swap THEN
574                Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN
575                `rFV (lam Y z M') SUBSET FV M' DELETE z UNION X`
576                   by (FIRST_ASSUM MATCH_MP_TAC THEN
577                       FULL_SIMP_TAC (srw_ss())
578                                     [SUBSET_DEF, Abbr`Y`, Abbr`M'`,
579                                      swapping_def]) THEN
580                Q_TAC SUFF_TAC `~(a IN FV M' DELETE z UNION X) /\
581                                ~(z IN FV M' DELETE z UNION X)`
582                      THEN1 METIS_TAC [SUBSET_DEF] THEN
583                SRW_TAC [][Abbr`M'`]) THEN
584         POP_ASSUM SUBST_ALL_TAC THEN REPEAT AP_TERM_TAC THEN
585         ASM_SIMP_TAC bool_ss [] THEN NEW_ELIM_TAC THEN
586         ASM_REWRITE_TAC [] THEN Q.X_GEN_TAC `a` THEN
587         REVERSE (SRW_TAC [][]) THEN1 SRW_TAC [][] THEN
588         MATCH_MP_TAC EQ_TRANS THEN
589         Q.EXISTS_TAC `rswap a z (lam (hom M) z M)` THEN CONJ_TAC THENL [
590           ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN
591           MATCH_MP_TAC swapping_implies_identity_swap THEN
592           Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN
593           `rFV (lam (hom M) z M) SUBSET FV (LAM z M) UNION X`
594             by SRW_TAC [][] THEN
595           POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
596           METIS_TAC [],
597           SRW_TAC [][]
598         ]) THEN
599  ASM_SIMP_TAC bool_ss [] THEN SRW_TAC [][LET_THM] THEN
600  NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN
601  Q.X_GEN_TAC `u` THEN STRIP_TAC THENL [
602    `lam (rswap u v (hom t)) u (tpm [(u,v)] t) = rswap u v (lam (hom t) v t)`
603       by SRW_TAC [][] THEN
604    POP_ASSUM SUBST_ALL_TAC THEN
605    MATCH_MP_TAC swapping_implies_identity_swap THEN
606    Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN
607    `rFV (lam (hom t) v t) SUBSET FV (LAM v t) UNION X`
608       by SRW_TAC [][] THEN
609    POP_ASSUM MP_TAC THEN REWRITE_TAC [SUBSET_DEF] THEN SRW_TAC [][] THEN
610    METIS_TAC [],
611    SRW_TAC [][]
612  ]);
613
614val term_swapping = store_thm(
615  "term_swapping",
616  ``swapping (\x y t. tpm [(x,y)] t) FV``,
617  SRW_TAC [][swapping_def, tpm_fresh]);
618val _ = export_rewrites ["term_swapping"]
619
620val lam_rFV = prove(
621  ``(!t' v t. rFV (lam t' v t) SUBSET ((rFV t' UNION FV t) DELETE v) UNION X)
622       ==>
623    !t' v t. rFV t' SUBSET FV t UNION X ==>
624             rFV (lam t' v t) SUBSET (FV t DELETE v) UNION X``,
625  SRW_TAC [][] THEN
626  FIRST_X_ASSUM (Q.SPECL_THEN [`t'`, `v`, `t`] ASSUME_TAC) THEN
627  REPEAT (POP_ASSUM MP_TAC) THEN
628  SRW_TAC [][SUBSET_DEF] THEN METIS_TAC [])
629val app_rFV = prove(
630  ``(!t' u' t u. rFV (app t' u' t u) SUBSET
631                 rFV t' UNION rFV u' UNION FV t UNION FV u UNION X) ==>
632    !t' u' t u.
633        rFV t' SUBSET FV t UNION X /\ rFV u' SUBSET FV u UNION X ==>
634        rFV (app t' u' t u) SUBSET FV t UNION FV u UNION X``,
635  SRW_TAC [][] THEN
636  FIRST_X_ASSUM (Q.SPECL_THEN [`t'`, `u'`, `t`, `u`] MP_TAC) THEN
637  REPEAT (POP_ASSUM MP_TAC) THEN
638  SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []);
639
640val swap_RECURSION_improved = save_thm(
641  "swap_RECURSION_improved",
642  REWRITE_RULE [AND_IMP_INTRO]
643               (DISCH_ALL (REWRITE_RULE [UNDISCH lam_rFV, UNDISCH app_rFV]
644                                        swap_RECURSION)))
645
646val swap_RECURSION_nosideset = save_thm(
647  "swap_RECURSION_nosideset",
648  SIMP_RULE (srw_ss()) [] (Q.INST [`X` |-> `{}`] swap_RECURSION_improved))
649
650
651val _ = export_theory();
652