1open HolKernel Parse boolLib bossLib metisLib basic_swapTheory
2     relationTheory
3
4val _ = new_theory "chap3";
5
6local open pred_setLib in end;
7
8open binderLib BasicProvers
9open nomsetTheory termTheory chap2Theory
10
11fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
12
13val SUBSET_DEF = pred_setTheory.SUBSET_DEF
14
15val compatible_def =
16    Define`compatible R = !x y c. R x y /\ one_hole_context c ==>
17                                  R (c x) (c y)`;
18
19val congruence_def = Define`congruence R <=> equivalence R /\ compatible R`;
20
21val is_reduction_def =
22    Define`is_reduction R <=> compatible R /\ transitive R /\ reflexive R`;
23
24val (compat_closure_rules, compat_closure_ind, compat_closure_cases) =
25    Hol_reln`(!x y. R x y ==> compat_closure R x y) /\
26             (!x y z. compat_closure R x y ==>
27                      compat_closure R (z @@ x) (z @@ y)) /\
28             (!x y z. compat_closure R x y ==>
29                      compat_closure R (x @@ z) (y @@ z)) /\
30             (!x y v. compat_closure R x y ==>
31                 compat_closure R (LAM v x) (LAM v y))`
32
33(* Barendregt definition 3.1.14 *)
34val substitutive_def = Define`
35  substitutive R = !M M'. R M M' ==> !N v. R ([N/v]M) ([N/v]M')
36`;
37
38val permutative_def = Define`
39  permutative R = !M M'. R M M' ==> !p. R (tpm p M) (tpm p M')
40`;
41
42val cc_gen_ind = store_thm(
43  "cc_gen_ind",
44  ``!R fv. (!M N p. R M N ==> R (tpm p M) (tpm p N)) /\
45           (!M N x. R M N ==> P M N x) /\
46           (!M M' N x. (!y. P M M' y) ==> P (M @@ N) (M' @@ N) x) /\
47           (!M N N' x. (!y. P N N' y) ==> P (M @@ N) (M @@ N') x) /\
48           (!v M M' x. ~(v IN fv x) /\ (!y. P M M' y) ==>
49                       P (LAM v M) (LAM v M') x) /\
50           (!x. FINITE (fv x)) ==>
51           !M N. compat_closure R M N ==> !x. P M N x``,
52  REPEAT GEN_TAC THEN STRIP_TAC THEN
53  Q_TAC SUFF_TAC `!M N. compat_closure R M N ==>
54                        !x p. P (tpm p M) (tpm p N) x`
55        THEN1 METIS_TAC [pmact_nil] THEN
56  HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THEN
57  Q_TAC (NEW_TAC "z") `fv x UNION {lswapstr p v} UNION FV (tpm p M) UNION
58                       FV (tpm p N)` THEN
59  `LAM (lswapstr p v) (tpm p M) = LAM z (tpm ([(z,lswapstr p v)] ++ p) M)`
60     by SRW_TAC [][tpm_ALPHA, pmact_decompose] THEN
61  `LAM (lswapstr p v) (tpm p N) = LAM z (tpm ([(z,lswapstr p v)] ++ p) N)`
62     by SRW_TAC [][tpm_ALPHA, pmact_decompose] THEN
63  SRW_TAC [][]);
64
65val cc_ind = save_thm(
66  "cc_ind",
67  (Q.GEN `P` o Q.GEN `X` o Q.GEN `R` o
68   Q.INST [`P'` |-> `P`] o
69   SIMP_RULE (srw_ss()) [] o
70   Q.INST [`P` |-> `\M N x. P' M N`, `fv` |-> `\x. X`] o
71   SPEC_ALL) cc_gen_ind);
72
73val compat_closure_permutative = store_thm(
74  "compat_closure_permutative",
75  ``permutative R ==> permutative (compat_closure R)``,
76  STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [permutative_def] THEN
77  HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THEN
78  METIS_TAC [permutative_def, compat_closure_rules]);
79
80val permutative_compat_closure_eqn = store_thm(
81  "permutative_compat_closure_eqn",
82  ``permutative R ==>
83    (compat_closure R (tpm p M) (tpm p N) = compat_closure R M N)``,
84  STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
85    `permutative (compat_closure R)`
86       by METIS_TAC [compat_closure_permutative] THEN
87    `compat_closure R (tpm (REVERSE p) (tpm p M))
88                      (tpm (REVERSE p) (tpm p N))`
89       by METIS_TAC [permutative_def] THEN
90    FULL_SIMP_TAC (srw_ss()) [],
91    METIS_TAC [permutative_def, compat_closure_permutative]
92  ]);
93val _ = export_rewrites ["permutative_compat_closure_eqn"]
94
95val swap_eq_3substs = store_thm(
96  "swap_eq_3substs",
97  ``~(z IN FV M) /\ ~(x = z) /\ ~(y = z) ==>
98    (tpm [(x, y)] M = [VAR y/z] ([VAR x/y] ([VAR z/x] M)))``,
99  SRW_TAC [][GSYM fresh_tpm_subst] THEN
100  `tpm [(x,y)] (tpm [(z,x)] M) =
101       tpm [(swapstr x y z, swapstr x y x)] (tpm [(x,y)] M)`
102     by (SRW_TAC [][Once (GSYM pmact_sing_to_back), SimpLHS] THEN
103         SRW_TAC [][]) THEN
104  POP_ASSUM SUBST_ALL_TAC THEN
105  SRW_TAC [][pmact_flip_args]);
106
107val substitutive_implies_permutative = store_thm(
108  "substitutive_implies_permutative",
109  ``substitutive R ==> permutative R``,
110  SRW_TAC [][substitutive_def, permutative_def] THEN
111  Induct_on `p` THEN SRW_TAC [][] THEN
112  `?x y. h = (x,y)` by METIS_TAC [pairTheory.pair_CASES] THEN
113  SRW_TAC [][] THEN
114  Q_TAC (NEW_TAC "z") `{x; y} UNION FV (tpm p M) UNION FV (tpm p M')` THEN
115  `(tpm ((x,y)::p) M = [VAR y/z] ([VAR x/y] ([VAR z/x] (tpm p M)))) /\
116   (tpm ((x,y)::p) M'= [VAR y/z] ([VAR x/y] ([VAR z/x] (tpm p M'))))`
117      by (ONCE_REWRITE_TAC [tpm_CONS] THEN
118          SRW_TAC [][swap_eq_3substs]) THEN
119  ASM_SIMP_TAC (srw_ss()) []);
120
121val compat_closure_substitutive = store_thm(
122  "compat_closure_substitutive",
123  ``substitutive R ==> substitutive (compat_closure R)``,
124  STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN
125  REPEAT STRIP_TAC THEN
126  Q.UNDISCH_THEN `compat_closure R M M'` MP_TAC THEN
127  MAP_EVERY Q.ID_SPEC_TAC [`M'`, `M`] THEN
128  HO_MATCH_MP_TAC cc_ind THEN Q.EXISTS_TAC `v INSERT FV N` THEN
129  SRW_TAC [][SUB_THM] THENL [
130    PROVE_TAC [substitutive_implies_permutative, permutative_def],
131    PROVE_TAC [compat_closure_rules, substitutive_def],
132    SRW_TAC [][compat_closure_rules],
133    SRW_TAC [][compat_closure_rules],
134    SRW_TAC [][compat_closure_rules]
135  ]);
136
137val _ = overload_on ("equiv_closure", ``relation$EQC``)
138val _ = overload_on ("EQC", ``relation$EQC``)
139local
140  open relationTheory
141in
142  val equiv_closure_rules = LIST_CONJ [EQC_R, EQC_REFL, EQC_SYM, EQC_TRANS]
143  val equiv_closure_ind = EQC_INDUCTION
144end
145
146val equiv_closure_substitutive = store_thm(
147  "equiv_closure_substitutive",
148  ``substitutive R ==> substitutive (equiv_closure R)``,
149  STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN
150  HO_MATCH_MP_TAC equiv_closure_ind THEN SRW_TAC [][] THEN
151  METIS_TAC [substitutive_def, equiv_closure_rules]);
152
153val _ = overload_on ("conversion", ``\R. equiv_closure (compat_closure R)``)
154
155val conversion_substitutive = store_thm(
156  "conversion_substitutive",
157  ``substitutive R ==> substitutive (conversion R)``,
158  METIS_TAC [compat_closure_substitutive, equiv_closure_substitutive]);
159
160val RTC_substitutive = store_thm(
161  "RTC_substitutive",
162  ``substitutive R ==> substitutive (RTC R)``,
163  STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN
164  HO_MATCH_MP_TAC RTC_INDUCT THEN
165  METIS_TAC [RTC_RULES, substitutive_def]);
166
167val _ = overload_on ("reduction", ``\R. RTC (compat_closure R)``)
168
169val reduction_substitutive = store_thm(
170  "reduction_substitutive",
171  ``substitutive R ==> substitutive (reduction R)``,
172  METIS_TAC [compat_closure_substitutive, RTC_substitutive]);
173
174val conversion_rules = store_thm(
175  "conversion_rules",
176  ``!R. (!x. conversion R x x) /\
177        (!x y. conversion R x y ==> conversion R y x) /\
178        (!x y z. conversion R x y /\ conversion R y z ==> conversion R x z) /\
179        (!x y. R x y ==> conversion R x y) /\
180        (!x y. reduction R x y ==> conversion R x y) /\
181        (!x y. compat_closure R x y ==> conversion R x y)``,
182  SRW_TAC [][equiv_closure_rules] THENL [
183    PROVE_TAC [equiv_closure_rules],
184    PROVE_TAC [equiv_closure_rules, compat_closure_rules],
185    POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [] THEN
186    MAP_EVERY Q.ID_SPEC_TAC [`y`,`x`] THEN
187    HO_MATCH_MP_TAC RTC_INDUCT THEN
188    PROVE_TAC [equiv_closure_rules]
189  ]);
190
191val compat_closure_compatible = store_thm(
192  "compat_closure_compatible",
193  ``!R. compatible (compat_closure R)``,
194  GEN_TAC THEN
195  Q_TAC SUFF_TAC `!c. one_hole_context c ==>
196                      !x y. compat_closure R x y ==>
197                            compat_closure R (c x) (c y)` THEN1
198     SRW_TAC [][compatible_def] THEN
199  HO_MATCH_MP_TAC one_hole_context_ind THEN SRW_TAC [][] THEN
200  PROVE_TAC [compat_closure_rules]);
201
202val reduction_compatible = store_thm(
203  "reduction_compatible",
204  ``!R. compatible (reduction R)``,
205  GEN_TAC THEN
206  Q_TAC SUFF_TAC `!x y. RTC (compat_closure R) x y ==>
207                        !c. one_hole_context c ==>
208                            RTC (compat_closure R) (c x) (c y)` THEN1
209    SRW_TAC [][compatible_def] THEN
210  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
211  PROVE_TAC [compatible_def, compat_closure_compatible,
212             RTC_RULES]);
213
214val reduction_rules = store_thm(
215  "reduction_rules",
216  ``(!x. reduction R x x) /\
217    (!x y. R x y ==> reduction R x y) /\
218    (!x y. compat_closure R x y ==> reduction R x y) /\
219    (!x y z. reduction R x y /\ reduction R y z ==>
220             reduction R x z) /\
221    (!x y z. reduction R x y ==> reduction R (z @@ x) (z @@ y)) /\
222    (!x y z. reduction R x y ==> reduction R (x @@ z) (y @@ z)) /\
223    (!x y v. reduction R x y ==> reduction R (LAM v x) (LAM v y))``,
224  REPEAT STRIP_TAC THENL [
225    PROVE_TAC [RTC_RULES],
226    PROVE_TAC [RTC_RULES, compat_closure_rules],
227    PROVE_TAC [RTC_RULES],
228    PROVE_TAC [RTC_RTC],
229    PROVE_TAC [leftctxt, compatible_def, reduction_compatible],
230    PROVE_TAC [rightctxt_thm, rightctxt, compatible_def, reduction_compatible],
231    PROVE_TAC [absctxt, compatible_def, reduction_compatible]
232  ]);
233
234val conversion_compatible = store_thm(
235  "conversion_compatible",
236  ``!R. compatible (conversion R)``,
237  GEN_TAC THEN
238  Q_TAC SUFF_TAC `!x y. equiv_closure (compat_closure R) x y ==>
239                        !c. one_hole_context c ==>
240                            equiv_closure (compat_closure R) (c x) (c y)` THEN1
241    SRW_TAC [][compatible_def] THEN
242  HO_MATCH_MP_TAC equiv_closure_ind THEN SRW_TAC [][] THEN
243  PROVE_TAC [compatible_def, equiv_closure_rules, compat_closure_compatible]);
244
245(* "Follows from an induction on the structure of M, and the
246    compatibility of reduction R" *)
247val lemma3_8 = store_thm(
248  "lemma3_8",
249  ``!M. reduction R N N' ==> reduction R ([N/x] M) ([N'/x] M)``,
250  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
251  Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN
252  SRW_TAC [][SUB_THM, SUB_VAR] THEN PROVE_TAC [reduction_rules]);
253
254val redex_def = Define`redex (R:'a -> 'a -> bool) t = ?u. R t u`;
255
256val (can_reduce_rules, can_reduce_ind, can_reduce_cases) =
257  Hol_reln`(!t. redex R t ==> can_reduce R t) /\
258           (!M N. can_reduce R M ==> can_reduce R (M @@ N)) /\
259           (!M N. can_reduce R M ==> can_reduce R (N @@ M)) /\
260           (!v M. can_reduce R M ==> can_reduce R (LAM v M))`
261
262val can_reduce_reduces = store_thm(
263  "can_reduce_reduces",
264  ``!R t. can_reduce R t ==> ?u. compat_closure R t u``,
265  GEN_TAC THEN HO_MATCH_MP_TAC can_reduce_ind THEN SRW_TAC [][redex_def] THEN
266  PROVE_TAC [compat_closure_rules]);
267
268val normal_form_def = Define`normal_form R t = ~can_reduce R t`;
269
270(* definition from p30 *)
271val beta_def = Define`beta M N = ?x body arg. (M = LAM x body @@ arg) /\
272                                              (N = [arg/x]body)`;
273val _ = Unicode.unicode_version {u = UnicodeChars.beta, tmnm = "beta"}
274
275val beta_alt = store_thm(
276  "beta_alt",
277  ``!X M N. FINITE X ==>
278            (beta M N = ?x body arg. (M = LAM x body @@ arg) /\
279                                     (N = [arg/x] body) /\
280                                     ~(x IN X))``,
281  SRW_TAC [][beta_def, EQ_IMP_THM] THENL [
282    SRW_TAC [][LAM_eq_thm] THEN
283    Q_TAC (NEW_TAC "z") `x INSERT FV body UNION X` THEN
284    MAP_EVERY Q.EXISTS_TAC [`z`, `tpm [(x,z)] body`] THEN
285    SRW_TAC [][] THEN
286    Q_TAC SUFF_TAC `tpm [(x,z)] body = [VAR z/x]body`
287          THEN1 SRW_TAC [][lemma15a] THEN
288    SRW_TAC [][GSYM fresh_tpm_subst, pmact_flip_args],
289    METIS_TAC []
290  ]);
291
292val strong_bvc_term_ind = store_thm(
293  "strong_bvc_term_ind",
294  ``!P fv. (!s x. P (VAR s) x) /\
295           (!M N x. (!x. P M x) /\ (!x. P N x) ==> P (M @@ N) x) /\
296           (!v x M. ~(v IN fv x) /\ (!x. P M x) ==> P (LAM v M) x) /\
297           (!x. FINITE (fv x)) ==>
298           !t x. P t x``,
299  REPEAT GEN_TAC THEN STRIP_TAC THEN
300  Q_TAC SUFF_TAC `!t p x. P (tpm p t) x` THEN1 METIS_TAC [pmact_nil] THEN
301  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN
302  Q.ABBREV_TAC `u = lswapstr p v` THEN
303  Q.ABBREV_TAC `M = tpm p t` THEN
304  Q_TAC (NEW_TAC "z") `u INSERT FV M UNION fv x` THEN
305  `LAM u M = LAM z (tpm [(z, u)] M)` by SRW_TAC [][tpm_ALPHA] THEN
306  `tpm [(z,u)] M = tpm ((z,u)::p) t`
307     by SRW_TAC [][Abbr`M`, GSYM pmact_decompose] THEN
308  SRW_TAC [][])
309
310val _ = set_fixity "-b->" (Infix(NONASSOC, 450))
311val _ = overload_on("-b->", ``compat_closure beta``)
312val _ = set_fixity "-b->*" (Infix(NONASSOC, 450))
313val _ = overload_on ("-b->*", ``RTC (-b->)``)
314
315val ubeta_arrow = "-" ^ UnicodeChars.beta ^ "->"
316val _ = Unicode.unicode_version {u = ubeta_arrow, tmnm = "-b->"}
317val _ = Unicode.unicode_version {u = ubeta_arrow^"*", tmnm = "-b->*"}
318
319val ccbeta_gen_ind = store_thm(
320  "ccbeta_gen_ind",
321  ``(!v M N X. v NOTIN FV N /\ v NOTIN fv X ==>
322               P ((LAM v M) @@ N) ([N/v]M) X) /\
323    (!M1 M2 N X. (!X. P M1 M2 X) ==> P (M1 @@ N) (M2 @@ N) X) /\
324    (!M N1 N2 X. (!X. P N1 N2 X) ==> P (M @@ N1) (M @@ N2) X) /\
325    (!v M1 M2 X. v NOTIN fv X /\ (!X. P M1 M2 X) ==>
326                 P (LAM v M1) (LAM v M2) X) /\
327    (!X. FINITE (fv X)) ==>
328    !M N. M -b-> N ==> !X. P M N X``,
329  STRIP_TAC THEN
330  Q_TAC SUFF_TAC `!M N. M -b-> N ==>
331                        !X p. P (tpm p M) (tpm p N) X`
332        THEN1 METIS_TAC [pmact_nil] THEN
333  HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT STRIP_TAC THENL [
334    FULL_SIMP_TAC (srw_ss()) [beta_def, tpm_subst] THEN
335    Q.ABBREV_TAC `v = lswapstr p x` THEN
336    Q.ABBREV_TAC `N' = tpm p arg` THEN
337    Q.ABBREV_TAC `M' = tpm p body` THEN
338    Q_TAC (NEW_TAC "z") `v INSERT FV M' UNION FV N' UNION fv X` THEN
339    `LAM v M' = LAM z ([VAR z/v] M')` by SRW_TAC [][SIMPLE_ALPHA] THEN
340    Q_TAC SUFF_TAC `[N'/v]M' = [N'/z]([VAR z/v]M')` THEN1 SRW_TAC [][] THEN
341    SRW_TAC [][lemma15a],
342    SRW_TAC [][],
343    SRW_TAC [][],
344    SRW_TAC [][] THEN
345    Q.ABBREV_TAC `x = lswapstr p v` THEN
346    Q.ABBREV_TAC `M' = tpm p M` THEN
347    Q.ABBREV_TAC `N' = tpm p N` THEN
348    Q_TAC (NEW_TAC "z") `x INSERT FV M' UNION FV N' UNION fv X` THEN
349    `(LAM x M' = LAM z (tpm [(z,x)] M')) /\ (LAM x N' = LAM z (tpm[(z,x)] N'))`
350       by SRW_TAC [][tpm_ALPHA] THEN
351    SRW_TAC [][] THEN
352    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
353    `(tpm [(z,x)] M' = tpm ((z,x)::p) M) /\
354     (tpm [(z,x)] N' = tpm ((z,x)::p) N)`
355       by SRW_TAC [][Abbr`M'`, Abbr`N'`, GSYM pmact_decompose] THEN
356    SRW_TAC [][]
357  ]);
358
359val ccbeta_ind = save_thm(
360  "ccbeta_ind",
361  (Q.GEN `P` o Q.GEN `X` o
362   SIMP_RULE (srw_ss()) [] o
363   Q.INST [`P'` |-> `P`] o
364   Q.INST [`fv` |-> `\x. X`, `P` |-> `\M N X. P' M N`] o
365   SPEC_ALL) ccbeta_gen_ind);
366
367val beta_substitutive = store_thm(
368  "beta_substitutive",
369  ``substitutive beta``,
370  SRW_TAC [][substitutive_def] THEN
371  Q.SPEC_THEN `v INSERT FV N` ASSUME_TAC beta_alt THEN
372  FULL_SIMP_TAC (srw_ss()) [] THEN
373  Q.EXISTS_TAC `x` THEN SRW_TAC [][SUB_THM, GSYM substitution_lemma]);
374
375val cc_beta_subst = store_thm(
376  "cc_beta_subst",
377  ``!M N. M -b-> N ==> !P v. [P/v]M -b-> [P/v]N``,
378  METIS_TAC [beta_substitutive, compat_closure_substitutive,
379             substitutive_def]);
380
381val reduction_beta_subst = store_thm(
382  "reduction_beta_subst",
383  ``!M N. M -b->* N ==> !P v. [P/v]M -b->* [P/v]N``,
384  METIS_TAC [beta_substitutive, reduction_substitutive, substitutive_def]);
385
386val cc_beta_FV_SUBSET = store_thm(
387  "cc_beta_FV_SUBSET",
388  ``!M N. M -b-> N ==> FV N SUBSET FV M``,
389  HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN
390  SRW_TAC [][SUBSET_DEF, FV_SUB] THEN PROVE_TAC []);
391
392val cc_beta_tpm = store_thm(
393  "cc_beta_tpm",
394  ``!M N. M -b-> N ==> !p. tpm p M -b-> tpm p N``,
395  HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THENL [
396    FULL_SIMP_TAC (srw_ss()) [beta_def, tpm_subst] THEN
397    METIS_TAC [compat_closure_rules, beta_def],
398    METIS_TAC [compat_closure_rules],
399    METIS_TAC [compat_closure_rules],
400    METIS_TAC [compat_closure_rules]
401  ]);
402
403val cc_beta_tpm_eqn = store_thm(
404  "cc_beta_tpm_eqn",
405  ``tpm pi M -b-> N <=> M -b-> tpm (REVERSE pi) N``,
406  METIS_TAC [pmact_inverse, cc_beta_tpm]);
407
408val cc_beta_thm = store_thm(
409  "cc_beta_thm",
410  ``(!s t. VAR s -b-> t <=> F) /\
411    (!M N P. M @@ N -b-> P <=>
412               (?v M0. (M = LAM v M0) /\ (P = [N/v]M0)) \/
413               (?M'. (P = M' @@ N) /\ M -b-> M') \/
414               (?N'. (P = M @@ N') /\ N -b-> N')) /\
415    (!v M N. LAM v M -b-> N <=> ?N0. (N = LAM v N0) /\ M -b-> N0)``,
416  REPEAT CONJ_TAC THEN
417  SIMP_TAC (srw_ss()) [beta_def, SimpLHS, Once compat_closure_cases] THEN
418  REPEAT STRIP_TAC THEN EQ_TAC THEN
419  SRW_TAC [][] THEN SRW_TAC [][] THENL [
420    PROVE_TAC [],
421    PROVE_TAC [],
422    REPEAT (POP_ASSUM MP_TAC) THEN
423    Q_TAC SUFF_TAC
424          `!v w M N P.
425                 (LAM v M = LAM w N) ==>
426                 compat_closure beta N P ==>
427                 ?M0. (LAM w P = LAM v M0) /\
428                      compat_closure beta M M0` THEN1 PROVE_TAC [] THEN
429    SRW_TAC [][LAM_eq_thm] THEN Q.EXISTS_TAC `tpm [(v,w)] P` THEN
430    SRW_TAC [][pmact_flip_args, cc_beta_tpm_eqn] THEN
431    METIS_TAC [cc_beta_FV_SUBSET, SUBSET_DEF],
432    PROVE_TAC []
433  ]);
434
435val ccbeta_rwt = store_thm(
436  "ccbeta_rwt",
437  ``(VAR s -b-> N <=> F) /\
438    (LAM x M -b-> N <=> ?N0. (N = LAM x N0) /\ M -b-> N0) /\
439    (LAM x M @@ N -b-> P <=>
440       (?M'. (P = LAM x M' @@ N) /\ M -b-> M') \/
441       (?N'. (P = LAM x M @@ N') /\ N -b-> N') \/
442       (P = [N/x]M)) /\
443    (~is_abs M ==>
444      (M @@ N -b-> P <=>
445        (?M'. (P = M' @@ N) /\ M -b-> M') \/
446        (?N'. (P = M @@ N') /\ N -b-> N')))``,
447  SRW_TAC [][cc_beta_thm] THENL [
448    SRW_TAC [][EQ_IMP_THM, LAM_eq_thm] THEN SRW_TAC [][] THENL [
449      METIS_TAC [fresh_tpm_subst, lemma15a],
450      SRW_TAC [boolSimps.DNF_ss][tpm_eqr]
451    ],
452    Q_TAC SUFF_TAC `!v M'. M <> LAM v M'` THEN1 METIS_TAC[] THEN
453    Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
454    FULL_SIMP_TAC (srw_ss()) []
455  ]);
456
457val beta_normal_form_bnf = store_thm(
458  "beta_normal_form_bnf",
459  ``normal_form beta = bnf``,
460  SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, normal_form_def,
461                       FORALL_AND_THM] THEN
462  CONJ_TAC THENL [
463    Q_TAC SUFF_TAC `!t. ~bnf t ==> can_reduce beta t` THEN1 PROVE_TAC [] THEN
464    HO_MATCH_MP_TAC nc_INDUCTION2 THEN
465    Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THENL [
466      PROVE_TAC [can_reduce_rules],
467      PROVE_TAC [can_reduce_rules],
468      Q_TAC SUFF_TAC `redex beta (t @@ t')` THEN1
469            PROVE_TAC [can_reduce_rules] THEN
470      SRW_TAC [][redex_def, beta_def] THEN PROVE_TAC [is_abs_thm, term_CASES],
471      PROVE_TAC [lemma14a, can_reduce_rules]
472    ],
473    Q_TAC SUFF_TAC `!t. can_reduce beta t ==> ~bnf t` THEN1 PROVE_TAC [] THEN
474    HO_MATCH_MP_TAC can_reduce_ind THEN SRW_TAC [][redex_def, beta_def] THEN
475    SRW_TAC [][]
476  ]);
477
478val nf_of_def = Define`nf_of R M N <=> normal_form R N /\ conversion R M N`;
479
480val prop3_10 = store_thm(
481  "prop3_10",
482  ``!R M N.
483       compat_closure R M N = ?P Q c. one_hole_context c /\ (M = c P) /\
484                                      (N = c Q) /\ R P Q``,
485  GEN_TAC THEN SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN
486  CONJ_TAC THENL [
487    HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THENL [
488      MAP_EVERY Q.EXISTS_TAC [`M`,`N`,`\x.x`] THEN
489      SRW_TAC [][one_hole_context_rules],
490      MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. z @@ c t`] THEN
491      SRW_TAC [][one_hole_context_rules],
492      MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. c t @@ z`] THEN
493      SRW_TAC [][one_hole_context_rules],
494      MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. LAM v (c t)`] THEN
495      SRW_TAC [][one_hole_context_rules]
496    ],
497    PROVE_TAC [compat_closure_compatible, compatible_def,
498               compat_closure_rules]
499  ]);
500
501val corollary3_2_1 = store_thm(
502  "corollary3_2_1",
503  ``!R M. normal_form R M ==> (!N. ~compat_closure R M N) /\
504                              (!N. reduction R M N ==> (M = N))``,
505  SIMP_TAC (srw_ss()) [normal_form_def] THEN REPEAT GEN_TAC THEN
506  STRIP_TAC THEN
507  Q.SUBGOAL_THEN `!N. ~compat_closure R M N` ASSUME_TAC THENL [
508    GEN_TAC THEN POP_ASSUM MP_TAC THEN
509    CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC (srw_ss())[] THEN
510    MAP_EVERY Q.ID_SPEC_TAC [`N`, `M`] THEN
511    HO_MATCH_MP_TAC compat_closure_ind THEN
512    PROVE_TAC [can_reduce_rules, redex_def],
513    ALL_TAC
514  ] THEN ASM_SIMP_TAC (srw_ss()) [] THEN
515  PROVE_TAC [RTC_CASES1]);
516
517val bnf_reduction_to_self = store_thm(
518  "bnf_reduction_to_self",
519  ``bnf M ==> (M -b->* N <=> (N = M))``,
520  METIS_TAC [corollary3_2_1, beta_normal_form_bnf, RTC_RULES]);
521
522local open relationTheory
523in
524val diamond_property_def = save_thm("diamond_property_def", diamond_def)
525end
526val _ = overload_on("diamond_property", ``relation$diamond``)
527
528(* This is not the same CR as appears in   There
529     CR R = diamond (RTC R)
530   Here,
531     CR R = diamond (RTC (compat_closure R))
532   In other words, this formulation allows us to write
533     CR beta
534   rather than having to write
535     CR (compat_closure beta)
536*)
537val CR_def = Define`CR R = diamond_property (reduction R)`;
538
539val theorem3_13 = store_thm(
540  "theorem3_13",
541  ``!R. CR R ==>
542        !M N. conversion R M N ==> ?Z. reduction R M Z /\ reduction R N Z``,
543  GEN_TAC THEN STRIP_TAC THEN SIMP_TAC (srw_ss()) [] THEN
544  HO_MATCH_MP_TAC equiv_closure_ind THEN REVERSE (SRW_TAC [][]) THEN1
545    (`?Z2. reduction R Z Z2 /\ reduction R Z' Z2` by
546        PROVE_TAC [CR_def, diamond_property_def] THEN
547     PROVE_TAC [reduction_rules]) THEN
548  PROVE_TAC [reduction_rules]);
549
550val corollary3_3_1 = store_thm(
551  "corollary3_3_1",
552  ``!R. CR R ==> (!M N. nf_of R M N ==> reduction R M N) /\
553                 (!M N1 N2. nf_of R M N1 /\ nf_of R M N2 ==> (N1 = N2))``,
554  SRW_TAC [][nf_of_def] THENL [
555    PROVE_TAC [corollary3_2_1, theorem3_13],
556    `conversion R N1 N2` by
557       (FULL_SIMP_TAC (srw_ss()) [] THEN
558        PROVE_TAC [equiv_closure_rules]) THEN
559    `?Z. reduction R N1 Z /\ reduction R N2 Z` by
560       PROVE_TAC [theorem3_13] THEN
561    PROVE_TAC [corollary3_2_1]
562  ]);
563
564
565val diamond_TC = diamond_TC_diamond
566
567val bvc_cases = store_thm(
568  "bvc_cases",
569  ``!X. FINITE X ==>
570        !t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/
571            (?v t0. ~(v IN X) /\ (t = LAM v t0))``,
572  SRW_TAC [][] THEN
573  Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN
574  SRW_TAC [][LAM_eq_thm] THEN
575  SRW_TAC [boolSimps.DNF_ss][] THEN
576  SRW_TAC [][Once tpm_eqr] THEN
577  Q_TAC (NEW_TAC "z") `v INSERT X UNION FV t0` THEN
578  METIS_TAC []);
579
580val (grandbeta_rules, grandbeta_ind, grandbeta_cases) =
581    Hol_reln`(!M. grandbeta M M) /\
582             (!M M' x. grandbeta M M' ==> grandbeta (LAM x M) (LAM x M')) /\
583             (!M N M' N'. grandbeta M M' /\ grandbeta N N' ==>
584                          grandbeta (M @@ N) (M' @@ N')) /\
585             (!M N M' N' x. grandbeta M M' /\ grandbeta N N' ==>
586                            grandbeta ((LAM x M) @@ N) ([N'/x] M'))`;
587val _ = set_fixity "=b=>" (Infix(NONASSOC,450))
588val _ = overload_on ("=b=>", ``grandbeta``)
589val _ = set_fixity "=b=>*" (Infix(NONASSOC,450))
590val _ = overload_on ("=b=>*", ``RTC grandbeta``)
591
592val gbarrow = "=" ^ UnicodeChars.beta ^ "=>"
593val _ = Unicode.unicode_version {u = gbarrow, tmnm = "=b=>"}
594val _ = Unicode.unicode_version {u = gbarrow ^ "*", tmnm = "=b=>*"}
595
596val grandbeta_bvc_gen_ind = store_thm(
597  "grandbeta_bvc_gen_ind",
598  ``!P fv.
599        (!M x. P M M x) /\
600        (!v M1 M2 x. v NOTIN fv x /\ (!x. P M1 M2 x) ==>
601                     P (LAM v M1) (LAM v M2) x) /\
602        (!M1 M2 N1 N2 x. (!x. P M1 M2 x) /\ (!x. P N1 N2 x) ==>
603                         P (M1 @@ N1) (M2 @@ N2) x) /\
604        (!M1 M2 N1 N2 v x.
605                  v NOTIN fv x /\ v NOTIN FV N1 /\ v NOTIN FV N2 /\
606                  (!x. P M1 M2 x) /\ (!x. P N1 N2 x) ==>
607                  P ((LAM v M1) @@ N1) ([N2/v]M2) x) /\
608        (!x. FINITE (fv x)) ==>
609        !M N. M =b=> N ==> !x. P M N x``,
610  REPEAT GEN_TAC THEN STRIP_TAC THEN
611  Q_TAC SUFF_TAC `!M N. grandbeta M N ==> !p x. P (tpm p M) (tpm p N) x`
612        THEN1 METIS_TAC [pmact_nil] THEN
613  HO_MATCH_MP_TAC grandbeta_ind THEN SRW_TAC [][] THENL [
614    Q.ABBREV_TAC `M' = tpm p M` THEN
615    Q.ABBREV_TAC `N' = tpm p N` THEN
616    Q.ABBREV_TAC `v = lswapstr p x` THEN
617    Q_TAC (NEW_TAC "z") `v INSERT fv x' UNION FV M' UNION FV N'` THEN
618    `(LAM v M' = LAM z (tpm ((z,v)::p) M)) /\
619     (LAM v N' = LAM z (tpm ((z,v)::p) N))`
620       by (ONCE_REWRITE_TAC [tpm_CONS] THEN
621           SRW_TAC [][Abbr`M'`, Abbr`N'`, tpm_ALPHA]) THEN
622    SRW_TAC [][],
623    Q.MATCH_ABBREV_TAC `P (LAM (lswapstr p v0) (tpm p ML) @@ tpm p MR)
624                          (tpm p ([NR/v0] NL)) ctx`  THEN
625    markerLib.RM_ALL_ABBREVS_TAC THEN
626    SRW_TAC [][tpm_subst] THEN
627    Q.ABBREV_TAC `v = lswapstr p v0` THEN
628    Q.ABBREV_TAC `M1 = tpm p ML` THEN
629    Q.ABBREV_TAC `N1 = tpm p MR` THEN
630    Q.ABBREV_TAC `M2 = tpm p NL` THEN
631    Q.ABBREV_TAC `N2 = tpm p NR` THEN
632    Q_TAC (NEW_TAC "z")
633          `v INSERT fv ctx UNION FV N1 UNION FV N2 UNION FV M1 UNION
634           FV M2` THEN
635    `LAM v M1 = LAM z (tpm [(z,v)] M1)` by SRW_TAC [][tpm_ALPHA] THEN
636    `[N2/v]M2 = [N2/z](tpm [(z,v)] M2)`
637       by SRW_TAC [][fresh_tpm_subst, lemma15a] THEN
638    SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
639    SRW_TAC [][Abbr`N1`,Abbr`N2`] THEN
640    `(tpm [(z,v)] M1 = tpm ((z,v)::p) ML) /\
641     (tpm [(z,v)] M2 = tpm ((z,v)::p) NL)`
642        by SRW_TAC [][GSYM pmact_decompose, Abbr`M1`,Abbr`M2`] THEN
643    SRW_TAC [][]
644  ]);
645
646val grandbeta_bvc_ind = save_thm(
647  "grandbeta_bvc_ind",
648  (Q.GEN `P` o Q.GEN `X` o
649   SIMP_RULE bool_ss [] o
650   SPECL [``(\M:term N:term x:'a. P M N:bool)``, ``\x:'a. X:string -> bool``])
651  grandbeta_bvc_gen_ind);
652
653val exercise3_3_1 = store_thm(
654  "exercise3_3_1",
655  ``!M N. M -b-> N ==> M =b=> N``,
656  HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][beta_def] THEN
657  PROVE_TAC [grandbeta_rules]);
658
659val app_grandbeta = store_thm(  (* property 3 on p. 37 *)
660  "app_grandbeta",
661  ``!M N L. M @@ N =b=> L <=>
662               (?M' N'. M =b=> M' /\ N =b=> N' /\ (L = M' @@ N')) \/
663               (?x P P' N'. (M = LAM x P) /\ P =b=> P' /\
664                            N =b=> N' /\ (L = [N'/x]P'))``,
665  REPEAT GEN_TAC THEN EQ_TAC THENL [
666    SIMP_TAC (srw_ss()) [SimpL ``(==>)``, Once grandbeta_cases] THEN
667    SIMP_TAC (srw_ss()) [DISJ_IMP_THM, GSYM LEFT_FORALL_IMP_THM,
668                         grandbeta_rules] THEN PROVE_TAC [],
669    SRW_TAC [][] THEN PROVE_TAC [grandbeta_rules]
670  ]);
671
672val grandbeta_permutative = store_thm(
673  "grandbeta_permutative",
674  ``!M N. M =b=> N ==> !pi. tpm pi M =b=> tpm pi N``,
675  HO_MATCH_MP_TAC grandbeta_ind THEN SRW_TAC [][tpm_subst] THEN
676  METIS_TAC [grandbeta_rules]);
677
678val grandbeta_permutative_eqn = store_thm(
679  "grandbeta_permutative_eqn",
680  ``tpm pi M =b=> tpm pi N  <=>  M =b=> N``,
681  METIS_TAC [pmact_inverse, grandbeta_permutative]);
682val _ = export_rewrites ["grandbeta_permutative_eqn"]
683
684val grandbeta_substitutive = store_thm(
685  "grandbeta_substitutive",
686  ``!M N. M =b=> N ==> [P/x]M =b=> [P/x]N``,
687  HO_MATCH_MP_TAC grandbeta_bvc_ind THEN
688  Q.EXISTS_TAC `x INSERT FV P` THEN
689  SRW_TAC [][SUB_THM, grandbeta_rules] THEN
690  SRW_TAC [][lemma2_11, grandbeta_rules]);
691
692val grandbeta_FV = store_thm(
693  "grandbeta_FV",
694  ``!M N. M =b=> N ==> FV N SUBSET FV M``,
695  HO_MATCH_MP_TAC grandbeta_ind THEN
696  SRW_TAC [][SUBSET_DEF, FV_SUB] THEN
697  PROVE_TAC []);
698
699val abs_grandbeta = store_thm(
700  "abs_grandbeta",
701  ``!M N v. LAM v M =b=> N <=> ���N0. N = LAM v N0 /\ M =b=> N0``,
702  REPEAT GEN_TAC THEN EQ_TAC THENL [
703    SIMP_TAC (srw_ss()) [Once grandbeta_cases, SimpL ``(==>)``] THEN
704    SIMP_TAC (srw_ss()) [DISJ_IMP_THM, grandbeta_rules] THEN
705    SRW_TAC [][LAM_eq_thm] THENL [
706      PROVE_TAC [],
707      SRW_TAC [][LAM_eq_thm, tpm_eqr, pmact_flip_args] THEN
708      PROVE_TAC [SUBSET_DEF, grandbeta_FV]
709    ],
710    PROVE_TAC [grandbeta_rules]
711  ]);
712
713val lemma3_15 = save_thm("lemma3_15", abs_grandbeta);
714
715val redex_grandbeta = store_thm(
716  "redex_grandbeta",
717  ``LAM v M @@ N =b=> L <=>
718        (���M' N'. M =b=> M' /\ N =b=> N' /\
719                 (L = LAM v M' @@ N')) \/
720        (���M' N'. M =b=> M' /\ N =b=> N' /\ (L = [N'/v]M'))``,
721  SRW_TAC [][app_grandbeta, EQ_IMP_THM] THENL [
722    PROVE_TAC [abs_grandbeta],
723    FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm] THEN DISJ2_TAC THENL [
724      METIS_TAC [],
725      SRW_TAC [][] THEN
726      MAP_EVERY Q.EXISTS_TAC [`tpm [(v,x)] P'`, `N'`] THEN
727      SRW_TAC [][] THEN
728      `v NOTIN FV P'`
729        by METIS_TAC [grandbeta_FV, SUBSET_DEF] THEN
730      SRW_TAC [][fresh_tpm_subst, lemma15a]
731    ],
732    METIS_TAC [grandbeta_rules],
733    METIS_TAC []
734  ]);
735
736val var_grandbeta = store_thm(
737  "var_grandbeta",
738  ``!v N. VAR v =b=> N <=> (N = VAR v)``,
739  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [grandbeta_cases] THEN
740  SRW_TAC [][]);
741
742val grandbeta_cosubstitutive = store_thm(
743  "grandbeta_cosubstitutive",
744  ``!M. N =b=> N' ==> [N/x] M =b=> [N'/x] M``,
745  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
746  Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN
747  SRW_TAC [][grandbeta_rules, SUB_VAR]);
748
749(* property 1 on p37, and Barendregt's lemma 3.2.4 *)
750val grandbeta_subst = store_thm(
751  "grandbeta_subst",
752  ``M =b=> M' /\ N =b=> N' ==> [N/x]M =b=> [N'/x]M'``,
753  Q_TAC SUFF_TAC
754        `!M M'. M =b=> M' ==> N =b=> N' ==>
755                [N/x] M =b=> [N'/x]M'` THEN1
756        METIS_TAC [] THEN
757  HO_MATCH_MP_TAC grandbeta_bvc_ind THEN
758  Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN
759  SRW_TAC [][SUB_THM, grandbeta_rules] THENL [
760    METIS_TAC [grandbeta_cosubstitutive],
761    RES_TAC THEN
762    SRW_TAC [][lemma2_11, grandbeta_rules]
763  ]);
764
765val strong_grandbeta_ind =
766    IndDefLib.derive_strong_induction (grandbeta_rules, grandbeta_ind)
767
768val strong_grandbeta_bvc_gen_ind =
769    (GEN_ALL o
770     SIMP_RULE (srw_ss()) [grandbeta_rules, FORALL_AND_THM,
771                           GSYM CONJ_ASSOC] o
772     Q.SPEC `\M N x. P M N x /\ grandbeta M N`)
773    grandbeta_bvc_gen_ind
774
775val lemma3_16 = store_thm( (* p. 37 *)
776  "lemma3_16",
777  ``diamond_property grandbeta``,
778  Q_TAC SUFF_TAC `!M M1. M =b=> M1 ==>
779                         !M2. M =b=> M2 ==>
780                              ?M3. M1 =b=> M3 /\ M2 =b=> M3` THEN1
781    PROVE_TAC [diamond_property_def] THEN
782  HO_MATCH_MP_TAC strong_grandbeta_bvc_gen_ind THEN Q.EXISTS_TAC `FV` THEN
783  SIMP_TAC (srw_ss()) [] THEN REPEAT CONJ_TAC THENL [
784    (* reflexive case *)
785    PROVE_TAC [grandbeta_rules],
786    (* lambda case *)
787    MAP_EVERY Q.X_GEN_TAC [`v`, `M`,`M1`, `M2`] THEN REPEAT STRIP_TAC THEN
788    `?P. (M2 = LAM v P) /\ M =b=> P` by PROVE_TAC [abs_grandbeta] THEN
789    SRW_TAC [][] THEN PROVE_TAC [grandbeta_rules],
790    (* app case *)
791    MAP_EVERY Q.X_GEN_TAC [`f`,`g`,`x`,`y`, `fx'`] THEN STRIP_TAC THEN
792    STRIP_TAC THEN
793    `(?f' x'. (fx' = f' @@ x') /\ f =b=> f' /\ x =b=> x') \/
794     (?v P P' x'. (f = LAM v P) /\ P =b=> P' /\ x =b=> x' /\
795                  (fx' = [x'/v]P'))` by
796        (FULL_SIMP_TAC (srw_ss()) [app_grandbeta] THEN PROVE_TAC [])
797    THENL [
798      METIS_TAC [grandbeta_rules],
799      `?P2. (g = LAM v P2) /\ P =b=> P2` by
800          PROVE_TAC [abs_grandbeta] THEN
801      SRW_TAC [][] THEN
802      `?ff. LAM v P2 =b=> ff /\ LAM v P' =b=> ff` by
803         PROVE_TAC [grandbeta_rules] THEN
804      `?xx. y =b=> xx /\ x' =b=> xx` by PROVE_TAC [] THEN
805      `?PP. P' =b=> PP /\ (ff = LAM v PP)` by
806         PROVE_TAC [abs_grandbeta] THEN
807      SRW_TAC [][] THEN
808      `P2 =b=> PP` by PROVE_TAC [abs_grandbeta, term_11] THEN
809      PROVE_TAC [grandbeta_rules, grandbeta_subst]
810    ],
811    (* beta-redex case *)
812    MAP_EVERY Q.X_GEN_TAC [`M`, `M'`, `N`, `N'`, `x`, `M2`] THEN
813    SRW_TAC [][redex_grandbeta] THENL [
814      (* other reduction didn't beta-reduce *)
815      `?Mfin. M' =b=> Mfin /\ M'' =b=> Mfin` by METIS_TAC [] THEN
816      `?Nfin. N' =b=> Nfin /\ N'' =b=> Nfin` by METIS_TAC [] THEN
817      Q.EXISTS_TAC `[Nfin/x]Mfin` THEN
818      METIS_TAC [grandbeta_rules, grandbeta_subst],
819      (* other reduction also beta-reduced *)
820      `?Mfin. M' =b=> Mfin /\ M'' =b=> Mfin` by METIS_TAC [] THEN
821      `?Nfin. N' =b=> Nfin /\ N'' =b=> Nfin` by METIS_TAC [] THEN
822      Q.EXISTS_TAC `[Nfin/x]Mfin` THEN
823      METIS_TAC [grandbeta_rules, grandbeta_subst]
824    ]
825  ]);
826
827val theorem3_17 = store_thm(
828  "theorem3_17",
829  ``TC grandbeta = reduction beta``,
830  Q_TAC SUFF_TAC
831    `(!M N. TC grandbeta M N ==> reduction beta M N) /\
832     (!M N. RTC (compat_closure beta) M N ==> TC grandbeta M N)`
833    THEN1 SRW_TAC [] [FUN_EQ_THM, EQ_IMP_THM] THEN
834  CONJ_TAC THENL [
835    Q_TAC SUFF_TAC `!M N. grandbeta M N ==> reduction beta M N`
836      THEN1 (PROVE_TAC [TC_IDEM, TC_RC_EQNS,
837                        TC_MONOTONE]) THEN
838    HO_MATCH_MP_TAC grandbeta_ind THEN PROVE_TAC [reduction_rules, beta_def],
839
840    Q_TAC SUFF_TAC `!M N. RC (compat_closure beta) M N ==> grandbeta M N`
841      THEN1 PROVE_TAC [TC_MONOTONE,
842                       TC_RC_EQNS] THEN
843    Q_TAC SUFF_TAC `!M N. compat_closure beta M N ==> grandbeta M N`
844      THEN1 PROVE_TAC [RC_DEF, grandbeta_rules] THEN
845    PROVE_TAC [exercise3_3_1]
846  ]);
847
848val beta_CR = store_thm(
849  "beta_CR",
850  ``CR beta``,
851  PROVE_TAC [CR_def, lemma3_16, theorem3_17, diamond_TC]);
852
853val betaCR_square = store_thm(
854  "betaCR_square",
855  ``M -b->* N1 /\ M -b->* N2 ==> ?N. N1 -b->* N /\ N2 -b->* N``,
856  METIS_TAC [beta_CR, diamond_property_def, CR_def]);
857
858val bnf_triangle = store_thm(
859  "bnf_triangle",
860  ``M -b->* N /\ M -b->* N' /\ bnf N ==> N' -b->* N``,
861  METIS_TAC [betaCR_square, bnf_reduction_to_self]);
862
863val Omega_starloops = Store_thm(
864  "Omega_starloops",
865  ``Omega -b->* N <=> (N = Omega)``,
866  Q_TAC SUFF_TAC `!M N. M -b->* N ==> (M = Omega) ==> (N = Omega)`
867     THEN1 METIS_TAC [RTC_RULES] THEN
868  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
869  FULL_SIMP_TAC (srw_ss()) [ccbeta_rwt, Omega_def]);
870
871val lameq_betaconversion = store_thm(
872  "lameq_betaconversion",
873  ``!M N. M == N <=> conversion beta M N``,
874  SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
875    HO_MATCH_MP_TAC lameq_ind THEN REPEAT STRIP_TAC THENL [
876      Q_TAC SUFF_TAC `beta (LAM x M @@ N) ([N/x] M)` THEN1
877        PROVE_TAC [conversion_rules] THEN
878      SRW_TAC [][beta_def] THEN PROVE_TAC [],
879      PROVE_TAC [conversion_rules],
880      PROVE_TAC [conversion_rules],
881      PROVE_TAC [conversion_rules],
882      PROVE_TAC [conversion_compatible, compatible_def, rightctxt,
883                 rightctxt_thm],
884      PROVE_TAC [conversion_compatible, compatible_def, leftctxt],
885      PROVE_TAC [conversion_compatible, compatible_def, absctxt]
886    ],
887    SIMP_TAC (srw_ss()) [] THEN
888    HO_MATCH_MP_TAC equiv_closure_ind THEN REPEAT CONJ_TAC THEN1
889      (HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][beta_def] THEN
890       PROVE_TAC [lameq_rules]) THEN
891    PROVE_TAC [lameq_rules]
892  ]);
893
894val prop3_18 = save_thm("prop3_18", lameq_betaconversion);
895
896val ccbeta_lameq = store_thm(
897  "ccbeta_lameq",
898  ``!M N. M -b-> N ==> M == N``,
899  SRW_TAC [][lameq_betaconversion, EQC_R]);
900val betastar_lameq = store_thm(
901  "betastar_lameq",
902  ``!M N. M -b->* N ==> M == N``,
903  SRW_TAC [][lameq_betaconversion, RTC_EQC]);
904
905val betastar_lameq_bnf = store_thm(
906  "betastar_lameq_bnf",
907  ``bnf N ==> (M -b->* N <=> M == N)``,
908  METIS_TAC [theorem3_13, beta_CR, betastar_lameq, bnf_reduction_to_self,
909             lameq_betaconversion]);
910
911val lameq_consistent = store_thm(
912  "lameq_consistent",
913  ``consistent $==``,
914  SRW_TAC [][consistent_def] THEN
915  MAP_EVERY Q.EXISTS_TAC [`S`,`K`] THEN STRIP_TAC THEN
916  `conversion beta S K` by PROVE_TAC [prop3_18] THEN
917  `?Z. reduction beta S Z /\ reduction beta K Z` by
918     PROVE_TAC [theorem3_13, beta_CR] THEN
919  `normal_form beta S` by PROVE_TAC [S_beta_normal, beta_normal_form_bnf] THEN
920  `normal_form beta K` by PROVE_TAC [K_beta_normal, beta_normal_form_bnf] THEN
921  `S = K` by PROVE_TAC [corollary3_2_1] THEN
922  FULL_SIMP_TAC (srw_ss()) [S_def, K_def]);
923
924val has_bnf_thm = store_thm(
925  "has_bnf_thm",
926  ``has_bnf M <=> ?N. M -b->* N /\ bnf N``,
927  EQ_TAC THENL [
928    METIS_TAC [lameq_betaconversion, chap2Theory.has_bnf_def, theorem3_13,
929               beta_CR, beta_normal_form_bnf, corollary3_2_1],
930    SRW_TAC [][chap2Theory.has_bnf_def, lameq_betaconversion] THEN
931    METIS_TAC [RTC_EQC]
932  ]);
933
934val Omega_reachable_no_bnf = store_thm(
935  "Omega_reachable_no_bnf",
936  ``M -b->* Omega ==> ~has_bnf M``,
937  REPEAT STRIP_TAC THEN
938  FULL_SIMP_TAC (srw_ss()) [has_bnf_thm] THEN
939  `Omega -b->* N` by METIS_TAC [bnf_triangle] THEN
940  `N = Omega` by FULL_SIMP_TAC (srw_ss()) [] THEN
941  FULL_SIMP_TAC (srw_ss()) []);
942
943val weak_diamond_def =
944    save_thm("weak_diamond_def", WCR_def)
945val _ = overload_on("weak_diamond", ``relation$WCR``)
946
947(* likewise, these definitions of WCR and SN, differ from those in
948   relation by wrapping the argument in a call to compat_closure
949*)
950val WCR_def = (* definition 3.20, p39 *) Define`
951  WCR R = weak_diamond (compat_closure R)
952`;
953
954val SN_def = Define`SN R = relation$SN (compat_closure R)`;
955
956val newmans_lemma = store_thm( (* lemma3_22, p39 *)
957  "newmans_lemma",
958  ``!R. SN R /\ WCR R ==> CR R``,
959  SIMP_TAC (srw_ss()) [SN_def, WCR_def, Newmans_lemma,
960                       CR_def,
961                       GSYM relationTheory.diamond_def,
962                       GSYM relationTheory.CR_def]);
963
964val commute_def =  (* p43 *)
965    Define`commute R1 R2 = !x x1 x2. R1 x x1 /\ R2 x x2 ==>
966                                     ?x3. R2 x1 x3 /\ R1 x2 x3`;
967
968val commute_COMM = store_thm(
969  "commute_COMM",
970  ``commute R1 R2 = commute R2 R1``,
971  PROVE_TAC [commute_def]);
972
973val diamond_RC = diamond_RC_diamond
974  (* |- !R. diamond_property R ==> diamond_property (RC R) *)
975
976val diamond_RTC = store_thm(
977  "diamond_RTC",
978  ``!R. diamond_property R ==> diamond_property (RTC R)``,
979  PROVE_TAC [diamond_TC, diamond_RC, TC_RC_EQNS]);
980
981val hr_lemma0 = prove(
982  ``!R1 R2. diamond_property R1 /\ diamond_property R2 /\ commute R1 R2 ==>
983            diamond_property (RTC (R1 RUNION R2))``,
984  REPEAT STRIP_TAC THEN
985  Q_TAC SUFF_TAC `diamond_property (R1 RUNION R2)` THEN1
986        PROVE_TAC [diamond_RTC] THEN
987  FULL_SIMP_TAC (srw_ss()) [diamond_property_def, commute_def,
988                            RUNION] THEN
989  PROVE_TAC []);
990
991val RUNION_RTC_MONOTONE = store_thm(
992  "RUNION_RTC_MONOTONE",
993  ``!R1 x y. RTC R1 x y ==> !R2. RTC (R1 RUNION R2) x y``,
994  GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN
995  PROVE_TAC [RTC_RULES, RUNION]);
996
997val RTC_OUT = store_thm(
998  "RTC_OUT",
999  ``!R1 R2. RTC (RTC R1 RUNION RTC R2) = RTC (R1 RUNION R2)``,
1000  REPEAT GEN_TAC THEN
1001  Q_TAC SUFF_TAC
1002    `(!x y. RTC (RTC R1 RUNION RTC R2) x y ==> RTC (R1 RUNION R2) x y) /\
1003     (!x y. RTC (R1 RUNION R2) x y ==> RTC (RTC R1 RUNION RTC R2) x y)` THEN1
1004    (SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
1005     PROVE_TAC []) THEN CONJ_TAC
1006  THEN HO_MATCH_MP_TAC RTC_INDUCT THENL [
1007    CONJ_TAC THENL [
1008      PROVE_TAC [RTC_RULES],
1009      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
1010      `RTC R1 x y \/ RTC R2 x y` by PROVE_TAC [RUNION] THEN
1011      PROVE_TAC [RUNION_RTC_MONOTONE, RTC_RTC, RUNION_COMM]
1012    ],
1013    CONJ_TAC THENL [
1014      PROVE_TAC [RTC_RULES],
1015      MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
1016      `R1 x y \/ R2 x y` by PROVE_TAC [RUNION] THEN
1017      PROVE_TAC [RTC_RULES, RUNION]
1018    ]
1019  ]);
1020
1021
1022val CC_RUNION_MONOTONE = store_thm(
1023  "CC_RUNION_MONOTONE",
1024  ``!R1 x y. compat_closure R1 x y ==> compat_closure (R1 RUNION R2) x y``,
1025  GEN_TAC THEN HO_MATCH_MP_TAC compat_closure_ind THEN
1026  PROVE_TAC [compat_closure_rules, RUNION]);
1027
1028val CC_RUNION_DISTRIB = store_thm(
1029  "CC_RUNION_DISTRIB",
1030  ``!R1 R2. compat_closure (R1 RUNION R2) =
1031            compat_closure R1 RUNION compat_closure R2``,
1032  REPEAT GEN_TAC THEN
1033  Q_TAC SUFF_TAC
1034     `(!x y. compat_closure (R1 RUNION R2) x y ==>
1035             (compat_closure R1 RUNION compat_closure R2) x y) /\
1036      (!x y. (compat_closure R1 RUNION compat_closure R2) x y ==>
1037             compat_closure (R1 RUNION R2) x y)` THEN1
1038     SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
1039  CONJ_TAC THENL [
1040    HO_MATCH_MP_TAC compat_closure_ind THEN
1041    PROVE_TAC [compat_closure_rules, RUNION],
1042    SRW_TAC [][RUNION] THEN
1043    PROVE_TAC [RUNION_COMM, CC_RUNION_MONOTONE]
1044  ]);
1045
1046val hindley_rosen_lemma = store_thm( (* p43 *)
1047  "hindley_rosen_lemma",
1048  ``(!R1 R2. diamond_property R1 /\ diamond_property R2 /\ commute R1 R2 ==>
1049             diamond_property (RTC (R1 RUNION R2))) /\
1050    (!R1 R2. CR R1 /\ CR R2 /\ commute (reduction R1) (reduction R2) ==>
1051             CR (R1 RUNION R2))``,
1052  CONJ_TAC THENL [
1053    MATCH_ACCEPT_TAC hr_lemma0,
1054    SRW_TAC [][CR_def] THEN
1055    `diamond_property (RTC (RTC (compat_closure R1) RUNION
1056                            RTC (compat_closure R2)))`
1057        by PROVE_TAC [hr_lemma0] THEN
1058    FULL_SIMP_TAC (srw_ss()) [RTC_OUT, CC_RUNION_DISTRIB]
1059  ]);
1060
1061val eta_def =
1062    Define`eta M N <=> ���v. M = LAM v (N @@ VAR v) ��� v ��� FV N`;
1063
1064val _ = Unicode.unicode_version {u = UnicodeChars.eta, tmnm = "eta"}
1065
1066val eta_normal_form_enf = store_thm(
1067  "eta_normal_form_enf",
1068  ``normal_form eta = enf``,
1069  Q_TAC SUFF_TAC `(!x. ~enf x ==> can_reduce eta x) /\
1070                  (!x. can_reduce eta x ==> ~enf x)` THEN1
1071    (SIMP_TAC (srw_ss())[normal_form_def, FUN_EQ_THM, EQ_IMP_THM,
1072                         FORALL_AND_THM] THEN PROVE_TAC []) THEN
1073  CONJ_TAC THENL [
1074    HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{}` THEN
1075    SRW_TAC [][] THENL [
1076      PROVE_TAC [can_reduce_rules],
1077      PROVE_TAC [can_reduce_rules],
1078      PROVE_TAC [can_reduce_rules, lemma14a],
1079      Q_TAC SUFF_TAC `?u. eta (LAM y x) u` THEN1
1080            PROVE_TAC [can_reduce_rules, redex_def] THEN
1081      FULL_SIMP_TAC (srw_ss()) [is_comb_APP_EXISTS, eta_def] THEN
1082      SRW_TAC [][] THEN
1083      FULL_SIMP_TAC (srw_ss()) [rand_thm, rator_thm] THEN PROVE_TAC []
1084    ],
1085    HO_MATCH_MP_TAC can_reduce_ind THEN
1086    SRW_TAC [][redex_def, eta_def] THEN
1087    SRW_TAC [][]
1088  ]);
1089
1090val no_eta_thm = store_thm(
1091  "no_eta_thm",
1092  ``(!s t. ~(eta (VAR s) t)) /\
1093    (!t u v. ~(eta (t @@ u) v))``,
1094  SRW_TAC [][eta_def]);
1095
1096val cc_eta_thm = store_thm(
1097  "cc_eta_thm",
1098  ``(!s t. compat_closure eta (VAR s) t <=> F) /\
1099    (!t u v. compat_closure eta (t @@ u) v <=>
1100             (?t'. (v = t' @@ u) /\ compat_closure eta t t') \/
1101             (?u'. (v = t @@ u') /\ compat_closure eta u u'))``,
1102  REPEAT CONJ_TAC THEN
1103  SIMP_TAC (srw_ss()) [SimpLHS, Once compat_closure_cases] THEN
1104  SIMP_TAC (srw_ss()) [no_eta_thm, EQ_IMP_THM, DISJ_IMP_THM,
1105                       GSYM LEFT_FORALL_IMP_THM, RIGHT_AND_OVER_OR,
1106                       LEFT_AND_OVER_OR, FORALL_AND_THM,
1107                       is_comb_APP_EXISTS, GSYM LEFT_EXISTS_AND_THM]);
1108
1109val eta_substitutive = store_thm(
1110  "eta_substitutive",
1111  ``substitutive eta``,
1112  SRW_TAC [][substitutive_def, eta_def] THEN
1113  Q_TAC (NEW_TAC "z") `{v;v'} UNION FV M' UNION FV N` THEN
1114  `LAM v (M' @@ VAR v) = LAM z ([VAR z/v] (M' @@ VAR v))`
1115     by SRW_TAC [][SIMPLE_ALPHA] THEN
1116  ` _ = LAM z ([VAR z/v] M' @@ VAR z)` by SRW_TAC [][SUB_THM] THEN
1117  ASM_SIMP_TAC (srw_ss()) [SUB_THM, lemma14b] THEN
1118  Q.EXISTS_TAC `z` THEN SRW_TAC [][FV_SUB]);
1119
1120val cc_eta_subst = store_thm(
1121  "cc_eta_subst",
1122  ``!M N. compat_closure eta M N ==>
1123          !P v. compat_closure eta ([P/v] M) ([P/v] N)``,
1124  METIS_TAC [eta_substitutive, compat_closure_substitutive, substitutive_def]);
1125
1126val cc_eta_tpm = store_thm(
1127  "cc_eta_tpm",
1128  ``!M N. compat_closure eta M N ==>
1129          compat_closure eta (tpm pi M) (tpm pi N)``,
1130  METIS_TAC [compat_closure_permutative, substitutive_implies_permutative,
1131             eta_substitutive, permutative_def])
1132val cc_eta_tpm_eqn = store_thm(
1133  "cc_eta_tpm_eqn",
1134  ``compat_closure eta (tpm pi M) N =
1135    compat_closure eta M (tpm (REVERSE pi) N)``,
1136  METIS_TAC [cc_eta_tpm, pmact_inverse]);
1137
1138val eta_deterministic = store_thm(
1139  "eta_deterministic",
1140  ``!M N1 N2. eta M N1 /\ eta M N2 ==> (N1 = N2)``,
1141  SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [eta_def, LAM_eq_thm, tpm_fresh]);
1142
1143val cc_eta_FV_SUBSET = store_thm(
1144  "cc_eta_FV_SUBSET",
1145  ``!M N. compat_closure eta M N ==> FV N SUBSET FV M``,
1146  HO_MATCH_MP_TAC compat_closure_ind THEN
1147  SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
1148  Q_TAC SUFF_TAC `!M N. eta M N ==> !s. s IN FV N ==> s IN FV M` THEN1
1149        PROVE_TAC [] THEN
1150  SIMP_TAC (srw_ss()) [eta_def, GSYM LEFT_FORALL_IMP_THM]);
1151
1152val cc_eta_LAM = store_thm(
1153  "cc_eta_LAM",
1154  ``!t v u. compat_closure eta (LAM v t) u <=>
1155            (?t'. (u = LAM v t') /\ compat_closure eta t t') \/
1156            eta (LAM v t) u``,
1157  SIMP_TAC (srw_ss()) [Once compat_closure_cases, SimpLHS] THEN
1158  SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss)[LAM_eq_thm, EQ_IMP_THM, tpm_eqr,
1159                                          cc_eta_tpm_eqn, pmact_flip_args] THEN
1160  REPEAT STRIP_TAC THEN DISJ1_TAC THEN
1161  Q_TAC SUFF_TAC `~(v' IN FV (tpm [(v,v')] y))` THEN1 SRW_TAC [][] THEN
1162  METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF]);
1163
1164val eta_LAM = store_thm(
1165  "eta_LAM",
1166  ``!v t u. eta (LAM v t) u <=> t = u @@ VAR v ��� v ��� FV u``,
1167  SRW_TAC [][eta_def, LAM_eq_thm, EQ_IMP_THM] THEN SRW_TAC [][tpm_fresh] THEN
1168  SRW_TAC [boolSimps.DNF_ss][]);
1169
1170val CR_eta_lemma = prove(
1171  ``!M M1 M2. eta M M1 /\ compat_closure eta M M2 /\ ~(M1 = M2) ==>
1172              ?M3. compat_closure eta M1 M3 /\ compat_closure eta M2 M3``,
1173  REPEAT STRIP_TAC THEN
1174  `?v. (M = LAM v (M1 @@ VAR v)) /\ ~(v IN FV M1)` by PROVE_TAC [eta_def] THEN
1175  FULL_SIMP_TAC (srw_ss()) [cc_eta_LAM, cc_eta_thm] THENL [
1176    Q.EXISTS_TAC `rator t'` THEN
1177    SRW_TAC [][eta_LAM] THEN
1178    METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF],
1179    FULL_SIMP_TAC (srw_ss()) [eta_LAM]
1180  ]);
1181
1182val cc_strong_ind =
1183    IndDefLib.derive_strong_induction (compat_closure_rules, compat_closure_ind)
1184
1185val eta_diamond = prove(
1186  ``!M M1. compat_closure eta M M1 ==>
1187           !M2. compat_closure eta M M2 /\ ~(M1 = M2) ==>
1188                ?M3. compat_closure eta M1 M3 /\
1189                     compat_closure eta M2 M3``,
1190  HO_MATCH_MP_TAC cc_strong_ind THEN REPEAT CONJ_TAC THENL [
1191    PROVE_TAC [CR_eta_lemma],
1192
1193    SRW_TAC [][cc_eta_thm] THEN
1194    FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_thm],
1195
1196    SRW_TAC [][cc_eta_thm] THEN
1197    FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_thm],
1198
1199    SRW_TAC [][cc_eta_LAM, eta_LAM] THEN
1200    FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_LAM, cc_eta_thm] THEN
1201    METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF]
1202  ]);
1203
1204val eta_CR = store_thm(
1205  "eta_CR",
1206  ``CR eta``,
1207  Q_TAC SUFF_TAC `diamond_property (RC (compat_closure eta))` THEN1
1208        (SRW_TAC [][CR_def] THEN
1209         PROVE_TAC [TC_RC_EQNS, diamond_TC]) THEN
1210  SIMP_TAC (srw_ss()) [diamond_property_def, RC_DEF,
1211                       RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM,
1212                       DISJ_IMP_THM, FORALL_AND_THM] THEN
1213  PROVE_TAC [eta_diamond]);
1214
1215val wonky_diamond_commutes = store_thm( (* Barendregt, lemma 3.3.6 *)
1216  "wonky_diamond_commutes",
1217  ``!R1 R2.
1218        (!x y z. R1 x y /\ R2 x z ==> ?w. RTC R1 z w /\ RC R2 y w) ==>
1219        commute (RTC R1) (RTC R2)``,
1220  REPEAT STRIP_TAC THEN
1221  `!x y. RTC R1 x y ==> !z. R2 x z ==> ?w. RTC R1 z w /\ RTC R2 y w` by
1222      (HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN
1223       CONJ_TAC THENL [
1224         PROVE_TAC [RTC_RULES],
1225         MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN
1226         `?w. RC R2 y w /\ RTC R1 z' w` by PROVE_TAC [] THEN
1227         FULL_SIMP_TAC (srw_ss()) [RC_DEF] THEN
1228         PROVE_TAC [RTC_RTC, RTC_RULES]
1229       ]) THEN
1230  Q_TAC SUFF_TAC
1231        `!x y. RTC R2 x y ==> !z. RTC R1 x z ==>
1232                                  ?w. RTC R2 z w /\ RTC R1 y w` THEN1
1233        (SRW_TAC [][commute_def] THEN PROVE_TAC []) THEN
1234  HO_MATCH_MP_TAC RTC_INDUCT THEN
1235  PROVE_TAC [RTC_RULES, RTC_RTC]);
1236
1237val eta_cosubstitutive = store_thm(
1238  "eta_cosubstitutive",
1239  ``!P M N x. compat_closure eta M N ==> reduction eta ([M/x] P) ([N/x] P)``,
1240  REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `P` THEN
1241  HO_MATCH_MP_TAC nc_INDUCTION2 THEN
1242  Q.EXISTS_TAC `x INSERT FV M UNION FV N` THEN
1243  SRW_TAC [][SUB_THM, SUB_VAR] THEN
1244  PROVE_TAC [reduction_rules]);
1245
1246val ccredex = prove(
1247  ``compat_closure beta (LAM v M @@ N) ([N/v]M)``,
1248  SRW_TAC [][cc_beta_thm] THEN METIS_TAC [])
1249
1250val strong_ccbeta_gen_ind = save_thm(
1251  "strong_ccbeta_gen_ind",
1252    (GEN_ALL o
1253     SIMP_RULE (srw_ss() ++ SatisfySimps.SATISFY_ss)
1254               [compat_closure_rules, FORALL_AND_THM, ccredex,
1255                GSYM CONJ_ASSOC] o
1256     Q.INST [`P` |-> `\M N x. P M N x /\ compat_closure beta M N`])
1257    ccbeta_gen_ind)
1258
1259val eta_beta_commute = store_thm(
1260  "eta_beta_commute",
1261  ``commute (reduction eta) (reduction beta)``,
1262  SIMP_TAC (srw_ss()) [] THEN
1263  MATCH_MP_TAC wonky_diamond_commutes THEN
1264  Q_TAC SUFF_TAC
1265        `!M P. M -b-> P ==>
1266               !N. compat_closure eta M N ==>
1267                   ?Q. reduction eta P Q /\ RC (-b->) N Q`
1268        THEN1 PROVE_TAC [] THEN
1269  HO_MATCH_MP_TAC strong_ccbeta_gen_ind THEN
1270  Q.EXISTS_TAC `FV` THEN SRW_TAC [][] THENL [
1271    FULL_SIMP_TAC (srw_ss()) [cc_eta_thm, cc_eta_LAM] THENL [
1272      Q.EXISTS_TAC `[P/v]t''` THEN
1273      `compat_closure eta ([P/v]M) ([P/v]t'')`
1274         by METIS_TAC [cc_eta_subst] THEN
1275      `compat_closure beta (LAM v t'' @@ P) ([P/v]t'')`
1276         by METIS_TAC [beta_def, compat_closure_rules] THEN
1277      METIS_TAC [RC_DEF, reduction_rules],
1278      FULL_SIMP_TAC (srw_ss()) [eta_LAM, SUB_THM, lemma14b] THEN
1279      Q.EXISTS_TAC `t' @@ P` THEN
1280      METIS_TAC [reduction_rules, RC_DEF],
1281      Q.EXISTS_TAC `[u'/v]M` THEN
1282      METIS_TAC [RC_DEF, eta_cosubstitutive, beta_def,
1283                 compat_closure_rules]
1284    ],
1285
1286    FULL_SIMP_TAC (srw_ss()) [cc_eta_thm] THEN
1287    METIS_TAC [compat_closure_rules, RC_DEF,
1288               reduction_rules],
1289    FULL_SIMP_TAC (srw_ss()) [cc_eta_thm] THEN
1290    METIS_TAC [compat_closure_rules, RC_DEF,
1291               reduction_rules],
1292
1293    FULL_SIMP_TAC (srw_ss()) [cc_eta_LAM, eta_LAM] THENL [
1294      METIS_TAC [compat_closure_rules, RC_DEF,
1295                 reduction_rules],
1296      FULL_SIMP_TAC (srw_ss()) [cc_beta_thm] THENL [
1297        SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1298        Cases_on `v = v'` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
1299          METIS_TAC [reduction_rules, RC_DEF],
1300          `LAM v ([VAR v/v'] M0) = LAM v' M0`
1301             by METIS_TAC [SIMPLE_ALPHA] THEN
1302          METIS_TAC [reduction_rules, RC_DEF]
1303        ],
1304        `v NOTIN FV M'` by METIS_TAC [cc_beta_FV_SUBSET, SUBSET_DEF] THEN
1305        `compat_closure eta (LAM v (M' @@ VAR v)) M'`
1306           by SRW_TAC [][cc_eta_LAM, eta_LAM] THEN
1307        METIS_TAC [RC_DEF, reduction_rules]
1308      ]
1309    ]
1310  ])
1311
1312val beta_eta_CR = store_thm(
1313  "beta_eta_CR",
1314  ``CR (beta RUNION eta)``,
1315  MATCH_MP_TAC (CONJUNCT2 hindley_rosen_lemma) THEN
1316  PROVE_TAC [beta_CR, eta_CR, eta_beta_commute, commute_COMM]);
1317
1318val beta_eta_lameta = store_thm(
1319  "beta_eta_lameta",
1320  ``conversion (beta RUNION eta) = lameta``,
1321  SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN
1322  CONJ_TAC THENL [
1323    SIMP_TAC (srw_ss()) [] THEN
1324    HO_MATCH_MP_TAC equiv_closure_ind THEN
1325    REPEAT CONJ_TAC THEN1
1326      (HO_MATCH_MP_TAC compat_closure_ind THEN
1327       REPEAT CONJ_TAC THEN1
1328          (SRW_TAC [][beta_def, eta_def, RUNION] THEN
1329           PROVE_TAC [lameta_rules]) THEN
1330       PROVE_TAC [lameta_rules]) THEN
1331    PROVE_TAC [lameta_rules],
1332    CONV_TAC (RENAME_VARS_CONV ["M", "N"]) THEN HO_MATCH_MP_TAC lameta_ind THEN
1333    REPEAT STRIP_TAC THENL [
1334      `(beta RUNION eta) (LAM x M @@ N) ([N/x]M)` by
1335         (SRW_TAC [][beta_def, RUNION] THEN PROVE_TAC []) THEN
1336      PROVE_TAC [conversion_rules],
1337      PROVE_TAC [conversion_rules],
1338      PROVE_TAC [conversion_rules],
1339      PROVE_TAC [conversion_rules],
1340      PROVE_TAC [conversion_compatible, compatible_def, rightctxt,
1341                 rightctxt_thm],
1342      PROVE_TAC [conversion_compatible, compatible_def, leftctxt],
1343      PROVE_TAC [conversion_compatible, compatible_def, absctxt],
1344      `(beta RUNION eta) (LAM x (N @@ VAR x)) N` by
1345         (SRW_TAC [][eta_def, RUNION] THEN PROVE_TAC []) THEN
1346      PROVE_TAC [conversion_rules]
1347    ]
1348  ]);
1349
1350val beta_eta_normal_form_benf = store_thm(
1351  "beta_eta_normal_form_benf",
1352  ``normal_form (beta RUNION eta) = benf``,
1353  SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, benf_def, FORALL_AND_THM,
1354                       normal_form_def] THEN CONJ_TAC
1355  THENL [
1356    Q_TAC SUFF_TAC `!M. ~bnf M \/ ~enf M ==> can_reduce (beta RUNION eta) M`
1357          THEN1 PROVE_TAC [] THEN
1358    HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [
1359      SRW_TAC [][bnf_thm, enf_thm], (* var case *)
1360      MAP_EVERY Q.X_GEN_TAC [`f`, `x`] THEN (* app case *)
1361      SRW_TAC [][bnf_thm, enf_thm] THENL [
1362        PROVE_TAC [can_reduce_rules],
1363        PROVE_TAC [can_reduce_rules],
1364        `redex (beta RUNION eta) (f @@ x)` by
1365         (SRW_TAC [][redex_def, RUNION, beta_def,
1366                     EXISTS_OR_THM] THEN
1367          PROVE_TAC [is_abs_thm, term_CASES]) THEN
1368        PROVE_TAC [can_reduce_rules],
1369        PROVE_TAC [can_reduce_rules],
1370        PROVE_TAC [can_reduce_rules]
1371      ],
1372
1373      MAP_EVERY Q.X_GEN_TAC [`x`, `M`] THEN
1374      SRW_TAC [][bnf_thm, enf_thm] THENL [
1375        PROVE_TAC [can_reduce_rules, lemma14a],
1376        PROVE_TAC [can_reduce_rules, lemma14a],
1377        Q_TAC SUFF_TAC `redex (beta RUNION eta) (LAM x M)` THEN1
1378            PROVE_TAC [can_reduce_rules] THEN
1379        SRW_TAC [][redex_def, RUNION, eta_def] THEN
1380        PROVE_TAC [is_comb_rator_rand]
1381      ]
1382    ],
1383    Q_TAC SUFF_TAC `!x. can_reduce (beta RUNION eta) x ==> ~bnf x \/ ~enf x`
1384          THEN1 PROVE_TAC [] THEN
1385    HO_MATCH_MP_TAC can_reduce_ind THEN
1386    SIMP_TAC (srw_ss()) [bnf_thm, enf_thm, DISJ_IMP_THM, redex_def,
1387                         RUNION, GSYM LEFT_FORALL_IMP_THM,
1388                         beta_def, eta_def]
1389  ]);
1390
1391val lameta_consistent = store_thm(
1392  "lameta_consistent",
1393  ``consistent lameta``,
1394  SIMP_TAC (srw_ss()) [consistent_def, GSYM beta_eta_lameta] THEN
1395  MAP_EVERY Q.EXISTS_TAC [`S`, `K`] THEN STRIP_TAC THEN
1396  `?Z. reduction (beta RUNION eta) S Z /\ reduction (beta RUNION eta) K Z` by
1397     PROVE_TAC [theorem3_13, beta_eta_CR] THEN
1398  `normal_form (beta RUNION eta) S` by
1399       SRW_TAC [][beta_eta_normal_form_benf, benf_def, bnf_thm, enf_thm,
1400                  S_def] THEN
1401  `normal_form (beta RUNION eta) K` by
1402       SRW_TAC [][beta_eta_normal_form_benf, benf_def, bnf_thm, enf_thm,
1403                  K_def] THEN
1404  `S = K` by PROVE_TAC [corollary3_2_1] THEN
1405  FULL_SIMP_TAC (srw_ss()) [S_def, K_def]);
1406
1407val is_comb_subst = store_thm(
1408  "is_comb_subst",
1409  ``!t u v. is_comb t ==> is_comb ([u/v]t)``,
1410  SIMP_TAC (srw_ss()) [SUB_THM, is_comb_APP_EXISTS,
1411                       GSYM LEFT_FORALL_IMP_THM]);
1412
1413val rator_isub_commutes = store_thm(
1414  "rator_isub_commutes",
1415  ``!R t. is_comb t ==> (rator (t ISUB R) = rator t ISUB R)``,
1416  Induct THEN
1417  ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD,
1418                           rator_subst_commutes, is_comb_subst]);
1419
1420(* ----------------------------------------------------------------------
1421    Congruence and rewrite rules for -b-> and -b->*
1422   ---------------------------------------------------------------------- *)
1423
1424open boolSimps
1425val RTC1_step = CONJUNCT2 (SPEC_ALL RTC_RULES)
1426
1427val betastar_LAM = store_thm(
1428  "betastar_LAM",
1429  ``!M N. LAM x M -b->* LAM x N  <=>  M -b->* N``,
1430  SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
1431    Q_TAC SUFF_TAC `!M N. M -b->* N ==>
1432                          !v M0 N0. (M = LAM v M0) /\ (N = LAM v N0) ==>
1433                                    M0 -b->* N0` THEN1 METIS_TAC [] THEN
1434    HO_MATCH_MP_TAC RTC_INDUCT THEN
1435    SIMP_TAC (srw_ss() ++ DNF_ss) [ccbeta_rwt] THEN
1436    METIS_TAC [RTC_RULES],
1437
1438    HO_MATCH_MP_TAC RTC_INDUCT THEN
1439    SRW_TAC [][] THEN
1440    METIS_TAC [compat_closure_rules, RTC_RULES]
1441  ]);
1442val _ = export_rewrites ["betastar_LAM"]
1443
1444val betastar_LAM_I = store_thm(
1445  "betastar_LAM_I",
1446  ``!v M N. M -b->* N ==> LAM v M -b->* LAM v N``,
1447  METIS_TAC [betastar_LAM]);
1448
1449val betastar_APPr = store_thm(
1450  "betastar_APPr",
1451  ``!M N. M -b->* N ==> P @@ M -b->* P @@ N``,
1452  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
1453  METIS_TAC [RTC1_step, compat_closure_rules]);
1454
1455val betastar_APPl = store_thm(
1456  "betastar_APPl",
1457  ``!M N. M -b->* N ==> M @@ P -b->* N @@ P``,
1458  HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN
1459  METIS_TAC [RTC1_step, compat_closure_rules]);
1460
1461val betastar_APPlr = store_thm(
1462  "betastar_APPlr",
1463  ``M -b->* M' ==> N -b->* N' ==> M @@ N -b->* M' @@ N'``,
1464  METIS_TAC [RTC_CASES_RTC_TWICE, betastar_APPl, betastar_APPr]);
1465
1466val beta_betastar = store_thm(
1467  "beta_betastar",
1468  ``LAM v M @@ N -b->* [N/v]M``,
1469  SRW_TAC [][ccbeta_rwt, RTC_SINGLE]);
1470
1471val betastar_eq_cong = store_thm(
1472  "betastar_eq_cong",
1473  ``bnf N ==> M -b->* M' ==> (M -b->* N  <=> M' -b->* N)``,
1474  METIS_TAC [bnf_triangle, RTC_CASES_RTC_TWICE]);
1475
1476val _ = export_theory();
1477
1478