1open HolKernel Parse boolLib bossLib
2
3open boolSimps pred_setTheory pathTheory binderLib
4open chap3Theory standardisationTheory term_posnsTheory termTheory
5     finite_developmentsTheory appFOLDLTheory nomsetTheory
6
7val _ = new_theory "normal_order"
8
9val _ = set_trace "Unicode" 1
10
11fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
12
13(* ----------------------------------------------------------------------
14    Normal order reduction
15
16    This relation is a bit monstrous really.  In particular, nice
17    properties of ��-reduction don't necessarily translate across.  For
18    example, substitutivity doesn't hold.  This would have that
19
20     M -n-> N ��� [P/v]M -n-> [P/v]N
21
22    but this isn't true because the variable v might be at the head
23    position in M, and P might contain a redex.  Then the reduction
24    that was OK on the left has to be deferred for the reduction in P
25    on the right.
26   ---------------------------------------------------------------------- *)
27
28val (normorder_rules, normorder_ind, normorder_cases) = Hol_reln`
29  (���v M N. normorder (LAM v M @@ N) ([N/v]M)) ���
30  (���v M1 M2. normorder M1 M2 ��� normorder (LAM v M1) (LAM v M2)) ���
31  (���M1 M2 N. normorder M1 M2 ��� ��is_abs M1 ��� normorder (M1 @@ N) (M2 @@ N)) ���
32  (���M N1 N2. normorder N1 N2 ��� bnf M ��� ��is_abs M ���
33              normorder (M @@ N1) (M @@ N2))
34`;
35
36val _ = set_fixity "-n->" (Infix(NONASSOC,450))
37val _ = overload_on ("-n->", ``normorder``)
38val _ = set_fixity "-n->*" (Infix(NONASSOC,450))
39val _ = overload_on ("-n->*", ``RTC normorder``)
40
41val tpm_normorder_I = store_thm(
42  "tpm_normorder_I",
43  ``���M N. M -n-> N ��� ���pi. tpm pi M -n-> tpm pi N``,
44  HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][normorder_rules, tpm_subst]);
45
46val tpm_normorder_eqn = store_thm(
47  "tpm_normorder_eqn",
48  ``tpm pi M -n-> tpm pi N ��� M -n-> N``,
49  METIS_TAC [pmact_inverse, tpm_normorder_I]);
50val _ = export_rewrites ["tpm_normorder_eqn"]
51
52val normorder_bvc_gen_ind = store_thm(
53  "normorder_bvc_gen_ind",
54  ``���P f.
55      (���x. FINITE (f x)) ���
56      (���v M N x. v ��� FV N ��� v ��� f x ��� P (LAM v M @@ N) ([N/v]M) x) ���
57      (���v M N x. v ��� f x ��� (���y. P M N y) ��� P (LAM v M) (LAM v N) x) ���
58      (���M1 M2 N x. (���y. P M1 M2 y) ��� ��is_abs M1 ��� P (M1 @@ N) (M2 @@ N) x) ���
59      (���M N1 N2 x.
60         (���y. P N1 N2 y) ��� bnf M ��� ��is_abs M ��� P (M @@ N1) (M @@ N2) x)
61     ���
62      ���M N. M -n-> N ��� ���x. P M N x``,
63  REPEAT GEN_TAC THEN STRIP_TAC THEN
64  Q_TAC SUFF_TAC
65        `���M N. M -n-> N ��� ����� x. P (tpm �� M) (tpm �� N) x`
66        THEN1 METIS_TAC [pmact_nil] THEN
67  HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][] THENL [
68    SRW_TAC [][tpm_subst] THEN
69    Q_TAC (NEW_TAC "z")
70          `{lswapstr �� v} ��� FV (tpm �� N) ��� f x ��� FV (tpm �� M)` THEN
71    `LAM (lswapstr �� v) (tpm �� M) = LAM z ([VAR z/lswapstr �� v] (tpm �� M))`
72       by SRW_TAC [][SIMPLE_ALPHA] THEN
73    POP_ASSUM SUBST_ALL_TAC THEN
74    `[tpm �� N/lswapstr �� v](tpm �� M) =
75     [tpm �� N/z] ([VAR z/lswapstr �� v](tpm �� M))`
76        by SRW_TAC [][lemma15a] THEN
77    POP_ASSUM SUBST_ALL_TAC THEN
78    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][],
79
80    Q_TAC (NEW_TAC "z")
81          `{lswapstr �� v} ��� FV (tpm �� M) ��� FV (tpm �� N) ��� f x` THEN
82    `(LAM (lswapstr �� v) (tpm �� M) = LAM z (tpm [(z, lswapstr �� v)] (tpm �� M)))
83         ���
84     (LAM (lswapstr �� v) (tpm �� N) = LAM z (tpm [(z, lswapstr �� v)] (tpm �� N)))`
85        by SRW_TAC [][tpm_ALPHA] THEN
86    NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN
87    SRW_TAC [][GSYM pmact_decompose]
88  ]);
89
90infix |> fun x |> f = f x
91val normorder_bvc_ind = save_thm(
92  "normorder_bvc_ind",
93  normorder_bvc_gen_ind |> SPEC_ALL
94                        |> Q.INST [`P` |-> `��M N x. P1 M N`, `f` |-> `��x. X`]
95                        |> SIMP_RULE (srw_ss()) []
96                        |> Q.INST [`P1` |-> `P`]
97                        |> Q.GEN `X` |> Q.GEN `P`);
98
99val normorder_ccbeta = store_thm(
100  "normorder_ccbeta",
101  ``���M N. M -n-> N ��� M -��-> N``,
102  HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][compat_closure_rules] THEN
103  METIS_TAC [compat_closure_rules, beta_def]);
104
105val normorder_lameq = store_thm(
106  "normorder_lameq",
107  ``���M N. M -n-> N ��� M == N``,
108  SRW_TAC [][normorder_ccbeta, ccbeta_lameq]);
109
110val normorder_FV = store_thm(
111  "normorder_FV",
112  ``M -n-> N ��� v ��� FV N ��� v ��� FV M``,
113  METIS_TAC [normorder_ccbeta, cc_beta_FV_SUBSET, SUBSET_DEF]);
114
115val normorder_rwts = store_thm(
116  "normorder_rwts",
117  ``(VAR s -n-> N ��� F) ���
118    (LAM v M -n-> N ��� ���M'. (N = LAM v M') ��� M -n-> M') ���
119    (LAM v M @@ N -n-> P ��� (P = [N/v]M)) ���
120    (��is_abs M ��� (M @@ N -n-> P ���
121                   (bnf M ��� ���N'. (P = M @@ N') ��� N -n-> N') ���
122                   ���M'. (P = M' @@ N) ��� M -n-> M'))``,
123  SRW_TAC [][] THENL [
124    SRW_TAC [][Once normorder_cases],
125
126    CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN
127    SIMP_TAC (srw_ss() ++ DNF_ss) [LAM_eq_thm, tpm_eqr] THEN
128    SRW_TAC [][EQ_IMP_THM] THEN1 SRW_TAC [][] THEN
129    Q.EXISTS_TAC `tpm [(v,v')] M2` THEN
130    `v ��� FV (tpm [(v,v')] M)` by SRW_TAC [][] THEN
131    `v ��� FV M2` by METIS_TAC [normorder_FV] THEN
132    SRW_TAC [][LAM_eq_thm, pmact_flip_args] THEN
133    METIS_TAC [pmact_sing_inv, tpm_normorder_I],
134
135    CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN
136    SIMP_TAC (srw_ss() ++ DNF_ss) [LAM_eq_thm, tpm_eqr] THEN
137    SRW_TAC [][EQ_IMP_THM] THEN
138    METIS_TAC [fresh_tpm_subst, lemma15a, pmact_flip_args],
139
140    CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN
141    SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][] THEN
142    FULL_SIMP_TAC (srw_ss()) []
143  ]);
144
145
146val normorder_bnf = store_thm(
147  "normorder_bnf",
148  ``bnf M ��� ���N. ��(M -n-> N)``,
149  Q.ID_SPEC_TAC `M` THEN HO_MATCH_MP_TAC simple_induction THEN
150  SRW_TAC [][normorder_rwts] THEN
151  SIMP_TAC (srw_ss()) [EQ_IMP_THM, normorder_rwts] THEN
152  Cases_on `is_abs M` THENL [
153    `���v M0. M = LAM v M0`
154      by (Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
155          FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN
156          METIS_TAC []) THEN
157    SRW_TAC [][normorder_rwts],
158
159    SRW_TAC [][normorder_rwts] THEN
160    METIS_TAC [simpLib.SIMP_PROVE (srw_ss()) []
161              ``���M1 M2 N1 N2. (M1 @@ N1:term = M2 @@ N2) ���
162                               (M1 = M2) ��� (N1 = N2)``]
163  ]);
164
165val strong_normorder_ind =
166    IndDefLib.derive_strong_induction (normorder_rules, normorder_ind)
167
168val normorder_det = store_thm(
169  "normorder_det",
170  ``���M N. M -n-> N ��� ���N'. M -n-> N' ��� (N' = N)``,
171  HO_MATCH_MP_TAC strong_normorder_ind THEN
172  SRW_TAC [][normorder_rwts] THEN
173  METIS_TAC [normorder_bnf]);
174
175val noposn_def = define_recursive_term_function`
176  (noposn (VAR s) = NONE) ���
177  (noposn (M @@ N) = if is_abs M then SOME []
178                     else case noposn M of
179                            NONE => OPTION_MAP (CONS Rt) (noposn N)
180                          | SOME p => SOME (Lt::p)) ���
181  (noposn (LAM v M) = OPTION_MAP (CONS In) (noposn M))
182`;
183val _ = export_rewrites ["noposn_def"]
184
185val bnf_noposn = store_thm(
186  "bnf_noposn",
187  ``���M. bnf M ��� (noposn M = NONE)``,
188  HO_MATCH_MP_TAC simple_induction THEN
189  SRW_TAC [][] THEN Cases_on `noposn M` THEN SRW_TAC [][])
190
191val normorder_noposn = store_thm(
192  "normorder_noposn",
193  ``M -n-> N ��� ���p. (noposn M = SOME p) ��� labelled_redn beta M p N``,
194  EQ_TAC THENL [
195    Q_TAC SUFF_TAC
196     `���M N. M -n-> N ��� ���p. (noposn M = SOME p) ��� labelled_redn beta M p N`
197     THEN1 METIS_TAC [] THEN
198    HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][bnf_noposn] THEN
199    SRW_TAC [][labelled_redn_rules] THEN
200    METIS_TAC [labelled_redn_rules, beta_def],
201
202    Q_TAC SUFF_TAC
203      `���M p N. labelled_redn beta M p N ���
204                (noposn M = SOME p) ��� M -n-> N` THEN1 METIS_TAC [] THEN
205    HO_MATCH_MP_TAC labelled_redn_ind THEN
206    SIMP_TAC (srw_ss() ++ DNF_ss) [beta_def, normorder_rules] THEN
207    SRW_TAC [][] THENL [
208      Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [normorder_rules],
209      Cases_on `noposn z` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
210      METIS_TAC [bnf_noposn, normorder_rules]
211    ]
212  ]);
213
214val noposn_least = store_thm(
215  "noposn_least",
216  ``���M p.
217      (noposn M = SOME p) ��� p ��� redex_posns M ���
218                            ���p'. p' ��� redex_posns M ���
219                                 (p' = p) ��� p < p'``,
220  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][redex_posns_def] THENL [
221    Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
222    SRW_TAC [][],
223    Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
224      `���N. labelled_redn beta M x N`
225         by METIS_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns] THEN
226      `bnf M` by METIS_TAC [bnf_noposn] THEN
227      METIS_TAC [labelled_redn_cc, beta_normal_form_bnf, corollary3_2_1],
228      SRW_TAC [][]
229    ],
230
231    Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
232    SRW_TAC [][]
233  ]);
234
235val normorder_reduction_def = Define`
236  normorder_reduction p =
237    okpath (��M r N. (noposn M = SOME r) ��� labelled_redn beta M r N) p
238`
239val normorder_is_standard = store_thm(
240  "normorder_is_standard",
241  ``���p. normorder_reduction p ��� standard_reduction p``,
242  HO_MATCH_MP_TAC standard_coind THEN
243  SRW_TAC [][normorder_reduction_def] THEN
244  METIS_TAC [posn_lt_antisym, posn_lt_irrefl, noposn_least]);
245
246val ihr_noposn = store_thm(
247  "ihr_noposn",
248  ``���r M. r is_head_redex M ��� (noposn M = SOME r)``,
249  HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][]);
250
251val head_is_normorder = store_thm(
252  "head_is_normorder",
253  ``���p. is_head_reduction p ��� normorder_reduction p``,
254  SIMP_TAC (srw_ss()) [normorder_reduction_def] THEN
255  HO_MATCH_MP_TAC okpath_co_ind THEN
256  SRW_TAC [][is_head_reduction_thm, ihr_noposn]);
257
258val ADD1 = arithmeticTheory.ADD1
259
260val last_el = store_thm(
261  "last_el",
262  ``���p. finite p ���
263        (last p = el (THE (length p) - 1) p)``,
264  HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][length_thm] THEN
265  Q_TAC SUFF_TAC `���n. length p = SOME (SUC n)`
266        THEN1 SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [] THEN
267  METIS_TAC [finite_length, length_never_zero, arithmeticTheory.num_CASES]);
268
269val standard_to_bnf_is_normal = store_thm(
270  "standard_to_bnf_is_normal",
271  ``���p. standard_reduction p ��� finite p ��� bnf (last p) ���
272        normorder_reduction p``,
273  SIMP_TAC (srw_ss()) [normorder_reduction_def] THEN
274  HO_MATCH_MP_TAC okpath_co_ind THEN
275  SRW_TAC [][standard_reduction_thm] THEN
276  `���r���. noposn M = SOME r���`
277     by (Cases_on `noposn M` THEN SRW_TAC [][] THEN
278         `bnf M` by METIS_TAC [bnf_noposn] THEN
279         METIS_TAC [labelled_redn_cc, beta_normal_form_bnf,
280                    corollary3_2_1]) THEN
281  `r��� ��� redex_posns M ��� ���r'. r' ��� redex_posns M ��� (r' = r���) ��� r��� < r'`
282     by METIS_TAC [noposn_least] THEN
283  `r ��� redex_posns M` by METIS_TAC [labelled_redn_beta_redex_posn] THEN
284  `(r = r���) ��� r��� < r` by METIS_TAC [] THEN1 SRW_TAC [][] THEN
285  `okpath (labelled_redn beta) p` by METIS_TAC [standard_reductions_ok] THEN
286  `���n. n ��� PL p ��� r��� ��� redex_posns (el n p)`
287     by (Induct THEN SRW_TAC [][] THENL [
288           METIS_TAC [lr_beta_preserves_lefter_redexes],
289           `labelled_redn beta (el n p) (nth_label n p) (el (SUC n) p)`
290               by METIS_TAC [okpath_every_el_relates] THEN
291           `n ��� PL p`
292               by METIS_TAC [PL_downward_closed, DECIDE ``x < SUC x``] THEN
293           METIS_TAC [lr_beta_preserves_lefter_redexes, ADD1, el_def]
294         ]) THEN
295  `���m. 0 < m ��� (length p = SOME m)`
296     by METIS_TAC [finite_length, length_never_zero,
297                   DECIDE ``0 < x ��� x ��� 0``] THEN
298  `last p = el (m - 1) p`
299     by METIS_TAC [last_el, optionTheory.option_CLAUSES] THEN
300  `m - 1 ��� PL p` by SRW_TAC [][PL_def] THEN
301  `r��� ��� redex_posns (last p)` by METIS_TAC [] THEN
302  `���N. labelled_redn beta (last p) r��� N`
303     by METIS_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns] THEN
304  METIS_TAC [labelled_redn_cc, beta_normal_form_bnf, corollary3_2_1]);
305
306val finite_normorder_RTC = store_thm(
307  "finite_normorder_RTC",
308  ``���p. normorder_reduction p ��� finite p ��� first p -n->* last p``,
309  REWRITE_TAC [normorder_reduction_def] THEN
310  HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THEN
311  METIS_TAC [normorder_noposn, relationTheory.RTC_RULES]);
312
313
314val normal_finds_bnf = store_thm(
315  "normal_finds_bnf",
316  ``M -��->* N /\ bnf N ��� M -n->* N``,
317  SRW_TAC [][] THEN
318  `���p. (first p = M) ��� finite p ��� (last p = N) ��� standard_reduction p`
319    by METIS_TAC [standardisation_theorem] THEN
320  METIS_TAC [standard_to_bnf_is_normal, finite_normorder_RTC]);
321
322val nstar_betastar = store_thm(
323  "nstar_betastar",
324  ``���M N. M -n->* N ��� M -��->* N``,
325  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
326  METIS_TAC [relationTheory.RTC_RULES, normorder_ccbeta]);
327
328val nstar_lameq = store_thm(
329  "nstar_lameq",
330  ``���M N. M -n->* N ��� M == N``,
331  SRW_TAC [][nstar_betastar, betastar_lameq]);
332
333val nstar_betastar_bnf = store_thm(
334  "nstar_betastar_bnf",
335  ``bnf N ��� (M -n->* N ��� M -��->* N)``,
336  METIS_TAC [normal_finds_bnf, nstar_betastar]);
337
338
339val nstar_bnf_triangle = store_thm(
340  "nstar_bnf_triangle",
341  ``���M N. M -n->* N ���
342          bnf N ��� ���M'. M -n->* M' ��� M' -n->* N``,
343  HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THENL [
344    METIS_TAC [relationTheory.RTC_RULES, bnf_reduction_to_self,
345               nstar_betastar],
346    POP_ASSUM MP_TAC THEN REWRITE_TAC [Once relationTheory.RTC_CASES1] THEN
347    STRIP_TAC THENL [
348      METIS_TAC [relationTheory.RTC_RULES],
349      METIS_TAC [normorder_det]
350    ]
351  ]);
352
353
354
355val normstar_LAM = store_thm(
356  "normstar_LAM",
357  ``���M N. LAM x M -n->* LAM x N ��� M -n->* N``,
358  SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [
359    Q_TAC SUFF_TAC `���M N. M -n->* N ���
360                          ���v M0 N0. (M = LAM v M0) ��� (N = LAM v N0) ���
361                                    M0 -n->* N0` THEN1 METIS_TAC [] THEN
362    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
363    SIMP_TAC (srw_ss() ++ DNF_ss) [normorder_rwts] THEN
364    METIS_TAC [relationTheory.RTC_RULES],
365
366    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
367    SRW_TAC [][] THEN
368    METIS_TAC [normorder_rules, relationTheory.RTC_RULES]
369  ]);
370val _ = export_rewrites ["normstar_LAM"]
371
372val normstar_APPr = store_thm(
373  "normstar_APPr",
374  ``bnf M ��� ��is_abs M ���
375        (M @@ N -n->* P ��� ���N'. (P = M @@ N') ��� N -n->* N')``,
376  SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN CONJ_TAC THENL [
377    Q_TAC SUFF_TAC `���M��� P. M��� -n->* P ���
378                            ���M N. (M��� = M @@ N) ��� bnf M ��� ��is_abs M ���
379                                   ���N'. (P = M @@ N') ��� N -n->* N'`
380          THEN1 METIS_TAC [] THEN
381    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
382    SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN
383    SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
384      METIS_TAC [relationTheory.RTC_RULES],
385      METIS_TAC [normorder_bnf]
386    ],
387
388    Q_TAC SUFF_TAC `���N N'. N -n->* N' ���
389                           ���M. bnf M ��� ��is_abs M ��� M @@ N -n->* M @@ N'`
390          THEN1 METIS_TAC [] THEN
391    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
392    METIS_TAC [normorder_rules, relationTheory.RTC_RULES]
393  ]);
394
395(* ----------------------------------------------------------------------
396    -n->* congruences
397   ---------------------------------------------------------------------- *)
398
399val nstar_LAM_I = store_thm(
400  "nstar_LAM_I",
401  ``M -n->* N ��� LAM v M -n->* LAM v N``,
402  SRW_TAC [][]);
403
404val normstar_APPr_I = store_thm(
405  "normstar_APPr_I",
406  ``bnf M ��� ��is_abs M ��� N -n->* N' ��� M @@ N -n->* M @@ N'``,
407  SRW_TAC [][normstar_APPr]);
408
409(* ----------------------------------------------------------------------
410    Calculating normal order reducts
411   ---------------------------------------------------------------------- *)
412
413val noreduct_def = Define`
414  noreduct t = if bnf t then NONE else SOME (@t'. t -n-> t')
415`;
416
417val noreduct_thm = store_thm(
418  "noreduct_thm",
419  ``(noreduct (LAM v M) = OPTION_MAP (LAM v) (noreduct M)) ���
420    (noreduct (LAM v M @@ N) = SOME ([N/v]M)) ���
421    (��is_abs M ��� (noreduct (M @@ N) =
422                  if bnf M then OPTION_MAP (APP M) (noreduct N)
423                  else OPTION_MAP (��M'. M' @@ N) (noreduct M))) ���
424    (noreduct (VAR s) = NONE)``,
425  SRW_TAC [][noreduct_def] THENL [
426    SRW_TAC [][normorder_rwts] THEN
427    `���N. M -n-> N` by METIS_TAC [normorder_bnf] THEN
428    `���N'. M -n-> N' ��� (N' = N)` by METIS_TAC [normorder_det] THEN
429    SRW_TAC [][],
430
431    SRW_TAC [][normorder_rwts],
432    FULL_SIMP_TAC (srw_ss()) [],
433
434    SRW_TAC [][normorder_rwts] THEN
435    `(���N. M -n-> N ��� F) ��� ���N'. N -n-> N'` by METIS_TAC [normorder_bnf] THEN
436    SRW_TAC [][] THEN
437    `���N���. N -n-> N��� ��� (N��� = N')` by METIS_TAC [normorder_det] THEN
438    SRW_TAC [][],
439
440    SRW_TAC [][normorder_rwts] THEN
441    `���M'. M -n-> M'` by METIS_TAC [normorder_bnf] THEN
442    `���M���. M -n-> M��� ��� (M��� = M')` by METIS_TAC [normorder_det] THEN
443    SRW_TAC [][]
444  ]);
445
446val noreduct_Yf = Store_thm(
447  "noreduct_Yf",
448  ``(noreduct (Yf f) = SOME (f @@ Yf f)) ���
449    (noreduct (Yf f @@ x) = SOME (f @@ Yf f @@ x))``,
450  Q_TAC (NEW_TAC "z") `FV f` THEN
451  `Yf f = LAM z (f @@ (VAR z @@ VAR z)) @@ LAM z (f @@ (VAR z @@ VAR z))`
452    by SRW_TAC [][chap2Theory.Yf_fresh] THEN
453  SRW_TAC [][noreduct_thm, termTheory.lemma14b]);
454
455val noreduct_characterisation = store_thm(
456  "noreduct_characterisation",
457  ``M -n-> N ��� (noreduct M = SOME N)``,
458  SRW_TAC [][noreduct_def] THEN Cases_on `bnf M` THEN SRW_TAC [][] THENL [
459    METIS_TAC [normorder_bnf],
460    `���N���. M -n-> N���` by METIS_TAC [normorder_bnf] THEN
461    `���N���. M -n-> N��� ��� (N��� = N���)` by METIS_TAC [normorder_det] THEN
462    SRW_TAC [][] THEN METIS_TAC []
463  ]);
464
465val noreduct_bnf = store_thm(
466  "noreduct_bnf",
467  ``(noreduct M = NONE) = bnf M``,
468  SRW_TAC [][noreduct_def]);
469
470
471val noreduct_vsubst = store_thm(
472  "noreduct_vsubst",
473  ``���t. noreduct ([VAR v/u] t) = OPTION_MAP (SUB (VAR v) u) (noreduct t)``,
474  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN
475  SRW_TAC [][noreduct_thm, SUB_VAR] THENL [
476    Cases_on `is_abs t` THENL [
477      `���z t0. (t = LAM z t0) ��� z ��� u ��� z ��� v`
478         by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN
479             FULL_SIMP_TAC (srw_ss()) [] THEN
480             SRW_TAC [boolSimps.DNF_ss][LAM_eq_thm, tpm_eqr] THEN
481             DISJ2_TAC THEN
482             Q_TAC (NEW_TAC "z") `{v';u;v} ��� FV t0` THEN METIS_TAC []) THEN
483      SRW_TAC [][noreduct_thm] THEN
484      SRW_TAC [][GSYM chap2Theory.substitution_lemma],
485
486      SRW_TAC [][noreduct_thm] THENL [
487        Cases_on `noreduct t'` THEN SRW_TAC [][],
488        Cases_on `noreduct t` THEN SRW_TAC [][]
489      ]
490    ],
491
492    Cases_on `noreduct t` THEN SRW_TAC [][]
493  ]);
494
495val noreduct_tpm = store_thm(
496  "noreduct_tpm",
497  ``���t. noreduct (tpm �� t) = OPTION_MAP (tpm ��) (noreduct t)``,
498  HO_MATCH_MP_TAC simple_induction THEN
499  SRW_TAC [][noreduct_thm] THENL [
500    Cases_on `is_abs t` THENL [
501      `���z t0. t = LAM z t0`
502         by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN
503             FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []) THEN
504      SRW_TAC [][noreduct_thm, tpm_subst],
505
506      SRW_TAC [][noreduct_thm] THENL [
507        Cases_on `noreduct t'` THEN SRW_TAC [][],
508        Cases_on `noreduct t` THEN SRW_TAC [][]
509      ]
510    ],
511
512    Cases_on `noreduct t` THEN SRW_TAC [][]
513  ]);
514
515
516val noredAPP' = store_thm(
517  "noredAPP'",
518  ``~is_abs M ==> (noreduct (M @@ N) =
519                     case noreduct M of
520                       NONE => OPTION_MAP (APP M) (noreduct N)
521                     | SOME M' => SOME (M' @@ N))``,
522  SRW_TAC [][noreduct_thm, GSYM noreduct_bnf] THEN
523  Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) []);
524
525val _ = overload_on ("upcons", ``��x y. pcons x () y``)
526
527
528
529val pair_case_unit = prove(
530  ``pair_CASE v (f : unit -> 'a -> 'b) = f () (SND v)``,
531  Cases_on `v` THEN SRW_TAC [][oneTheory.one]);
532
533val option_case_unit = prove(
534  ``option_CASE (OPTION_MAP ($, ()) x) n (f : unit # 'a -> 'b)  =
535    option_CASE x n (��x. f ((), x))``,
536  Cases_on `x` THEN SRW_TAC [][]);
537
538val nopath_def = new_specification(
539  "nopath_def",
540  ["nopath"],
541  path_Axiom |> ISPEC ``��M. (M, OPTION_MAP ((,) ()) (noreduct M))``
542             |> SIMP_RULE (srw_ss()) [oneTheory.one, pair_case_unit,
543                                      option_case_unit]);
544
545val first_nopath = Store_thm(
546  "first_nopath",
547  ``first (nopath M) = M``,
548  ONCE_REWRITE_TAC [nopath_def] THEN Cases_on `noreduct M` THEN
549  SRW_TAC [][]);
550
551val mem_nopath = Store_thm(
552  "mem_nopath",
553  ``mem M (nopath M)``,
554  ONCE_REWRITE_TAC [nopath_def] THEN Cases_on `noreduct M` THEN
555  SRW_TAC [][]);
556
557val mem_nopath_expanded = Store_thm(
558  "mem_nopath_expanded",
559  ``mem M (case v of NONE => stopped_at M
560                   | SOME y => pcons M l (f y))``,
561  Cases_on `v` THEN SRW_TAC [][]);
562
563val nopath_okpath = store_thm(
564  "nopath_okpath",
565  ``okpath (��M u N. M -n-> N) (nopath M)``,
566  Q_TAC SUFF_TAC `���p. (���M. p = nopath M) ��� okpath (��M u N. M -n-> N) p`
567        THEN1 METIS_TAC [] THEN
568  HO_MATCH_MP_TAC okpath_co_ind THEN REPEAT GEN_TAC THEN
569  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [nopath_def])) THEN
570  CONV_TAC LEFT_IMP_EXISTS_CONV THEN GEN_TAC THEN
571  Cases_on `noreduct M'` THEN SRW_TAC [][] THEN
572  METIS_TAC [noreduct_characterisation]);
573
574val option_case_CONG = store_thm(
575  "option_case_CONG",
576  ``(x = x') ��� (option_CASE x n f = option_CASE x' n f)``,
577  SRW_TAC [][]);
578
579val normstar_nopath = store_thm(
580  "normstar_nopath",
581  ``M -n->* N ��� mem N (nopath M)``,
582  EQ_TAC THENL [
583    Q_TAC SUFF_TAC `���M N. M -n->* N ��� mem N (nopath M)` THEN1 METIS_TAC []THEN
584    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
585    FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation,
586                              nopath_def, Cong option_case_CONG],
587
588    SIMP_TAC (srw_ss())[mem_def, GSYM LEFT_FORALL_IMP_THM] THEN
589    Q.ID_SPEC_TAC `N` THEN Q.ID_SPEC_TAC `M` THEN
590    SIMP_TAC (srw_ss()) [] THEN Induct_on`i` THEN SRW_TAC [][] THEN
591    Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN
592    POP_ASSUM SUBST_ALL_TAC THEN
593    Cases_on `noreduct M` THEN
594    FULL_SIMP_TAC (srw_ss()) [] THEN
595    METIS_TAC [relationTheory.RTC_RULES, noreduct_characterisation]
596  ]);
597
598val bnf_posn_is_length = store_thm(
599  "bnf_posn_is_length",
600  ``���i M. i ��� PL (nopath M) ��� bnf (el i (nopath M)) ���
601          (length (nopath M) = SOME (i + 1))``,
602  Induct THEN SRW_TAC [][] THENL [
603    ONCE_REWRITE_TAC [nopath_def] THEN
604    `noreduct M = NONE` by METIS_TAC [noreduct_bnf] THEN
605    SRW_TAC [][length_thm],
606
607    Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN
608    Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
609    `length (nopath x) = SOME (i + 1)` by METIS_TAC [] THEN
610    `finite (nopath x)` by METIS_TAC [finite_length] THEN
611    SRW_TAC [][length_thm, arithmeticTheory.ADD1]
612  ]);
613
614val has_bnf_finite_nopath = store_thm(
615  "has_bnf_finite_nopath",
616  ``has_bnf M ��� finite (nopath M)``,
617  SRW_TAC [][has_bnf_thm, EQ_IMP_THM] THENL [
618    `M -n->* N` by METIS_TAC [nstar_betastar_bnf] THEN
619    `mem N (nopath M)` by METIS_TAC [normstar_nopath] THEN
620    `���i. i ��� PL (nopath M) ��� (el i (nopath M) = N)`
621       by METIS_TAC [mem_def] THEN
622    `length (nopath M) = SOME (i + 1)`
623       by METIS_TAC [bnf_posn_is_length] THEN
624    METIS_TAC [finite_length],
625
626    POP_ASSUM MP_TAC THEN
627    Q_TAC SUFF_TAC
628       `���p. finite p ��� ���M. (p = nopath M) ��� ���N. M -��->* N ��� bnf N`
629       THEN1 METIS_TAC [] THEN
630    HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THENL [
631      Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN
632      Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
633      METIS_TAC [noreduct_bnf, relationTheory.RTC_RULES],
634
635      Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN
636      Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
637      SRW_TAC [][] THEN
638      METIS_TAC [normorder_ccbeta, noreduct_characterisation,
639                 relationTheory.RTC_RULES]
640    ]
641  ]);
642
643val nopath_el = store_thm(
644  "nopath_el",
645  ``���i M. i ��� PL (nopath M) ���
646          (nopath (el i (nopath M)) = drop i (nopath M))``,
647  Induct THEN SRW_TAC [][] THEN
648  POP_ASSUM MP_TAC THEN
649  Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN
650  POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
651  Cases_on `noreduct M` THEN SRW_TAC [][]);
652
653val nopath_smaller = store_thm(
654  "nopath_smaller",
655  ``���M N. M -n->* N ���
656          M ��� N ��� finite (nopath M) ���
657          THE (length (nopath N)) < THE (length (nopath M))``,
658  REPEAT STRIP_TAC THEN
659  `mem N (nopath M)` by METIS_TAC [normstar_nopath] THEN
660  `���i. i ��� PL (nopath M) ��� (N = el i (nopath M))`
661     by METIS_TAC [mem_def] THEN
662  `0 < i`
663     by (SPOSE_NOT_THEN ASSUME_TAC THEN
664         `i = 0` by DECIDE_TAC THEN
665         FULL_SIMP_TAC (srw_ss()) []) THEN
666  Q_TAC SUFF_TAC `nopath N = drop i (nopath M)` THEN1
667     (SRW_TAC [][] THEN
668      `���m. (length (nopath M) = SOME m) ��� m ��� 0`
669         by METIS_TAC [finite_length,
670                       length_never_zero] THEN
671      SRW_TAC [ARITH_ss][length_drop]) THEN
672  SRW_TAC [][nopath_el]);
673
674
675val Omega_def = chap2Theory.Omega_def
676val noreduct_omega = Store_thm(
677  "noreduct_omega",
678  ``noreduct �� = SOME ��``,
679  SRW_TAC [][noreduct_thm, Omega_def]);
680
681val Omega_loops = store_thm(
682  "Omega_loops",
683  ``�� -n-> ��``,
684  SRW_TAC [][noreduct_characterisation] THEN
685  SRW_TAC [][noreduct_thm, Omega_def]);
686
687val Omega_path_infinite = store_thm(
688  "Omega_path_infinite",
689  ``��finite (nopath ��)``,
690  Q_TAC SUFF_TAC `���p. finite p ��� p ��� nopath ��` THEN1 METIS_TAC [] THEN
691  HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THEN
692  ONCE_REWRITE_TAC [nopath_def] THEN SRW_TAC [][]);
693
694
695val Omega_has_no_bnf = Store_thm(
696  "Omega_has_no_bnf",
697  ``��has_bnf ��``,
698  SRW_TAC [][has_bnf_finite_nopath, Omega_path_infinite]);
699
700val last_of_finite_nopath = store_thm(
701  "last_of_finite_nopath",
702  ``finite (nopath M) ��� bnf (last (nopath M))``,
703  Q_TAC SUFF_TAC
704        `���p. finite p ��� ���M. (nopath M = p) ��� bnf (last (nopath M))`
705        THEN1 METIS_TAC [] THEN
706  HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THENL [
707    Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN
708    Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [noreduct_bnf] THEN
709    SRW_TAC [][],
710
711    Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN
712    Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
713    SRW_TAC [][] THEN METIS_TAC []
714  ]);
715
716
717(* ----------------------------------------------------------------------
718    bnf_of : term -> term option
719
720    "Calculating" the ��-normal form of a term (if it exists) with a while
721    loop.
722   ---------------------------------------------------------------------- *)
723
724val bnf_of_def = Define`
725  bnf_of M = OWHILE ((~) o bnf) (THE o noreduct) M
726`;
727
728val lemma1 = prove(
729  ``���p. okpath (��M u N. M -n-> N) p ��� finite p ���
730        bnf (last p) ��� (bnf_of (first p) = SOME (last p))``,
731  HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THENL [
732    SRW_TAC [][Once whileTheory.OWHILE_THM, bnf_of_def],
733    FULL_SIMP_TAC (srw_ss()) [] THEN
734    SRW_TAC [][Once whileTheory.OWHILE_THM, bnf_of_def] THENL [
735      SRW_TAC [][GSYM bnf_of_def] THEN
736      METIS_TAC [noreduct_characterisation, optionTheory.THE_DEF],
737      METIS_TAC [normorder_bnf]
738    ]
739  ]);
740
741val lemma2 = prove(
742  ``���N. (OWHILE ($~ o bnf) (THE o noreduct) M = SOME N) ���
743        M -n->* N``,
744  HO_MATCH_MP_TAC whileTheory.OWHILE_INV_IND THEN SRW_TAC [][] THEN
745  Cases_on `noreduct N` THENL [
746    FULL_SIMP_TAC (srw_ss()) [noreduct_bnf],
747    METIS_TAC [noreduct_characterisation, relationTheory.RTC_RULES_RIGHT1,
748               optionTheory.THE_DEF]
749  ]);
750
751val bnf_of_SOME = store_thm(
752  "bnf_of_SOME",
753  ``(bnf_of M = SOME N) ��� M -n->* N ��� bnf N``,
754  SRW_TAC [][bnf_of_def] THEN
755  IMP_RES_TAC whileTheory.OWHILE_ENDCOND THEN
756  FULL_SIMP_TAC (srw_ss()) [] THEN
757  METIS_TAC [lemma2]);
758
759val has_bnf_of = store_thm(
760  "has_bnf_of",
761  ``has_bnf M ��� ���N. bnf_of M = SOME N``,
762  EQ_TAC THENL [
763    SRW_TAC [][has_bnf_finite_nopath] THEN
764    ASSUME_TAC nopath_okpath THEN
765    METIS_TAC [lemma1, last_of_finite_nopath, first_nopath],
766
767    METIS_TAC [chap2Theory.has_bnf_def, bnf_of_SOME, nstar_lameq]
768  ]);
769
770val bnf_of_NONE = store_thm(
771  "bnf_of_NONE",
772  ``(bnf_of M = NONE) ��� ��has_bnf M``,
773  REWRITE_TAC [has_bnf_of] THEN
774  Cases_on `bnf_of M` THEN SRW_TAC [][]);
775
776val bnf_of_thm = store_thm(
777  "bnf_of_thm",
778  ``bnf_of M = if bnf M then SOME M else bnf_of (THE (noreduct M))``,
779  SRW_TAC [][bnf_of_def] THEN1
780    SRW_TAC [][Once whileTheory.OWHILE_THM] THEN
781  SRW_TAC [][SimpLHS, Once whileTheory.OWHILE_THM]);
782
783val nstar_bnf_of_SOME_I = store_thm(
784  "nstar_bnf_of_SOME_I",
785  ``M -n->* N ��� bnf N ��� (bnf_of M = SOME N)``,
786  Q_TAC SUFF_TAC `���M N. M -n->* N ��� bnf N ��� (bnf_of M = SOME N)`
787        THEN1 METIS_TAC [] THEN
788  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
789  SRW_TAC [][Once bnf_of_thm] THEN1 METIS_TAC [normorder_bnf] THEN
790  FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation]);
791
792val betastar_bnf_of_SOME_I = store_thm(
793  "betastar_bnf_of_SOME_I",
794  ``M -��->* N ��� bnf N ��� (bnf_of M = SOME N)``,
795  METIS_TAC [nstar_bnf_of_SOME_I, normal_finds_bnf]);
796
797val lameq_bnf_of_SOME_I = store_thm(
798  "lameq_bnf_of_SOME_I",
799  ``M == N ��� bnf N ��� (bnf_of M = SOME N)``,
800  METIS_TAC [betastar_bnf_of_SOME_I, betastar_lameq_bnf]);
801
802val lameq_bnf_of_cong = store_thm(
803  "lameq_bnf_of_cong",
804  ``M == N ��� (bnf_of M = bnf_of N)``,
805  Cases_on `bnf_of N` THENL [
806    FULL_SIMP_TAC (srw_ss()) [bnf_of_NONE, chap2Theory.has_bnf_def] THEN
807    METIS_TAC [chap2Theory.lameq_rules],
808    IMP_RES_TAC bnf_of_SOME THEN STRIP_TAC THEN
809    `M == x` by METIS_TAC [chap2Theory.lameq_rules, nstar_lameq] THEN
810    METIS_TAC [lameq_bnf_of_SOME_I]
811  ]);
812
813val lameq_has_bnf_cong = store_thm(
814  "lameq_has_bnf_cong",
815  ``M == N ��� (has_bnf M = has_bnf N)``,
816  SRW_TAC [][has_bnf_of] THEN
817  METIS_TAC [lameq_bnf_of_cong, chap2Theory.lameq_rules]);
818
819val bnf_bnf_of = store_thm(
820  "bnf_bnf_of",
821  ``bnf M ��� (bnf_of M = SOME M)``,
822  SRW_TAC [][Once bnf_of_thm]);
823
824val bnf_of_Omega = Store_thm(
825  "bnf_of_Omega",
826  ``bnf_of �� = NONE``,
827  METIS_TAC [Omega_has_no_bnf, bnf_of_NONE]);
828
829(* ----------------------------------------------------------------------
830    weak head reduction gives a congruence rule for -n->* of sorts
831   ---------------------------------------------------------------------- *)
832
833open head_reductionTheory
834val head_normorder = store_thm(
835  "head_normorder",
836  ``���M N. M -h-> N ��� M -n-> N``,
837  HO_MATCH_MP_TAC hreduce1_ind THEN
838  SRW_TAC [][normorder_rules]);
839
840val whstar_nstar = store_thm(
841  "whstar_nstar",
842  ``���M N. M -w->* N ��� M -n->* N``,
843  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
844  METIS_TAC [relationTheory.RTC_RULES, wh_head, head_normorder]);
845
846val whead_normorder = store_thm(
847  "whead_normorder",
848  ``���M N. M -w-> N ��� M -n-> N``,
849  METIS_TAC [wh_head, head_normorder]);
850
851val whead_norm_congL = store_thm(
852  "whead_norm_congL",
853  ``���M��� M���. M��� -w->* M��� ��� ���N. M��� @@ N -n->* M��� @@ N``,
854  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN
855  MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES_RIGHT1)) THEN
856  Q.EXISTS_TAC `M��� @@ N` THEN SRW_TAC [][] THEN
857  IMP_RES_TAC whead_normorder THEN
858  IMP_RES_TAC wh_is_abs THEN
859  SRW_TAC [][normorder_rules]);
860
861val normwhnf_is_abs_rpreserved = store_thm(
862  "normwhnf_is_abs_rpreserved",
863  ``���M N. M -n-> N ��� whnf M ��� is_abs N ��� is_abs M``,
864  HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][]);
865
866
867val whnf_is_abs_appstr = store_thm(
868  "whnf_is_abs_appstr",
869  ``���t. whnf t ��� is_abs t ��� ���v args. t = VAR v ���� args``,
870  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [
871    MAP_EVERY Q.EXISTS_TAC [`s`, `[]`] THEN SRW_TAC [][],
872    SRW_TAC [][EQ_IMP_THM] THENL [
873      MAP_EVERY Q.EXISTS_TAC [`v`, `args ++ [t']`] THEN
874      SRW_TAC [][rich_listTheory.FOLDL_APPEND],
875
876      FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN
877      Q.SPEC_THEN `VAR v ���� FRONT args` MP_TAC term_CASES THEN
878      STRIP_TAC THEN SRW_TAC [][] THEN
879      FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar],
880
881      FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN METIS_TAC []
882    ]
883  ]);
884
885val normorder_strong_ind =
886    IndDefLib.derive_strong_induction (normorder_rules,normorder_ind)
887
888Theorem bnf_appstar[simp]:
889    ���args f.
890      bnf (f ���� args) ��� bnf f ��� EVERY bnf args ��� (is_abs f ��� (args = []))
891Proof Induct THEN SRW_TAC [][] THEN METIS_TAC []
892QED
893
894val norm_varhead0 = prove(
895  ``���M N. M -n-> N ���
896          ���v Ms. (M = VAR v ���� Ms) ���
897                 ���p s M0 N0.
898                    (Ms = p ++ [M0] ++ s) ���
899                    (N = VAR v ���� (p ++ [N0] ++ s)) ���
900                    EVERY bnf p ���
901                    M0 -n-> N0``,
902  HO_MATCH_MP_TAC normorder_strong_ind THEN
903  SRW_TAC [][lam_eq_appstar, app_eq_varappstar] THENL [
904    FIRST_X_ASSUM (Q.SPECL_THEN [`v`, `FRONT Ms`] MP_TAC) THEN
905    SRW_TAC [][] THEN
906    MAP_EVERY Q.EXISTS_TAC [`p`, `s ++ [LAST Ms]`, `M0`, `N0`] THEN
907    SRW_TAC [][rich_listTheory.FRONT_APPEND, listTheory.FRONT_DEF,
908               rich_listTheory.LAST_APPEND, listTheory.LAST_DEF] THEN
909    IMP_RES_TAC listTheory.APPEND_FRONT_LAST THEN
910    POP_ASSUM (fn th => REWRITE_TAC [Once (GSYM th)]) THEN
911    SRW_TAC [][] THEN
912    REWRITE_TAC [GSYM listTheory.APPEND_ASSOC, listTheory.APPEND],
913
914    MAP_EVERY Q.EXISTS_TAC [`FRONT Ms`, `[]`, `LAST Ms`, `N`] THEN
915    SRW_TAC [][listTheory.APPEND_FRONT_LAST, rich_listTheory.FRONT_APPEND,
916               rich_listTheory.LAST_APPEND] THEN
917    FULL_SIMP_TAC (srw_ss()) []
918  ]);
919
920val norm_varhead = save_thm(
921  "norm_varhead",
922  SIMP_RULE (srw_ss() ++ DNF_ss) [] norm_varhead0);
923
924val normstar_varhead0 = prove(
925  ``���M N. M -n->* N ���
926          ���v Ms. (M = VAR v ���� Ms) ���
927                 ���Ns. (N = VAR v ���� Ns) ��� (LENGTH Ns = LENGTH Ms) ���
928                      ���i. i < LENGTH Ms ��� EL i Ms -n->* EL i Ns``,
929  HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THEN
930  `���p s M0 N0.  (Ms = p ++ [M0] ++ s) ���
931                (M' = VAR v ���� (p ++ [N0] ++ s)) ���
932                M0 -n-> N0`
933      by METIS_TAC [norm_varhead] THEN
934  `���Ns. (N = VAR v ���� Ns) ��� (LENGTH Ns = LENGTH (p ++ [N0] ++ s)) ���
935        ���i. i < LENGTH (p ++ [N0] ++ s) ��� EL i (p ++ [N0] ++ s) -n->* EL i Ns`
936      by METIS_TAC [] THEN
937  Q.EXISTS_TAC `Ns` THEN SRW_TAC [][] THEN
938  Cases_on `i < LENGTH p` THEN1
939    (SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND1] THEN
940     FIRST_X_ASSUM (Q.SPEC_THEN `i` MP_TAC) THEN
941     SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND1]) THEN
942  Cases_on `i = LENGTH p` THENL [
943    FIRST_X_ASSUM (Q.SPEC_THEN `LENGTH p` MP_TAC) THEN
944    SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND2,
945                       rich_listTheory.EL_APPEND1] THEN
946    METIS_TAC [relationTheory.RTC_RULES],
947    FIRST_X_ASSUM (Q.SPEC_THEN `i` MP_TAC) THEN
948    ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [rich_listTheory.EL_APPEND2]
949  ]);
950
951val normstar_varhead = save_thm(
952  "normstar_varhead",
953  SIMP_RULE (srw_ss() ++ DNF_ss) [] normstar_varhead0);
954
955val normstar_to_abs_wstar0 = prove(
956  ``���M N. M -n->* N ���
957          ���v N0. (N = LAM v N0) ��� v ��� FV M ���
958                 ���M0. M -w->* LAM v M0 ��� M0 -n->* N0``,
959  HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THEN
960  Cases_on `whnf M` THENL [
961    Cases_on `is_abs M` THENL [
962      `���M0. M = LAM v M0`
963         by (Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
964             FULL_SIMP_TAC (srw_ss()) [] THEN
965             SRW_TAC [DNF_ss][LAM_eq_thm, tpm_eqr] THEN METIS_TAC []) THEN
966      SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN
967      SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
968      METIS_TAC [relationTheory.RTC_RULES],
969
970      `���var args. LAM v N0 = VAR var ���� args`
971         by METIS_TAC [whnf_is_abs_appstr, normstar_varhead,
972                       norm_varhead] THEN
973      FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar]
974    ],
975
976    `���M���. M -w-> M���` by METIS_TAC [whnf_def] THEN
977    `M��� = M'` by METIS_TAC [wh_head, head_normorder, normorder_det] THEN
978    `v ��� FV M'` by METIS_TAC [normorder_FV] THEN
979    `���M'���. M' -w->* LAM v M'��� ��� M'��� -n->* N0` by METIS_TAC [] THEN
980    METIS_TAC [relationTheory.RTC_RULES]
981  ]);
982
983val normstar_to_abs_wstar = save_thm(
984  "normstar_to_abs_wstar",
985  SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] normstar_to_abs_wstar0);
986
987val varappstar_not_is_abs = store_thm(
988  "varappstar_not_is_abs",
989  ``��is_abs (VAR v ���� a)``,
990  Q.SPEC_THEN `VAR v ���� a` STRIP_ASSUME_TAC term_CASES THEN SRW_TAC [][] THEN
991  FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar]);
992
993val normorder_preserves_is_abs = store_thm(
994  "normorder_preserves_is_abs",
995  ``���M N. M -n-> N ��� is_abs M ��� is_abs N``,
996  HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][]);
997val nstar_preserves_is_abs = store_thm(
998  "nstar_preserves_is_abs",
999  ``���M N. M -n->* N ��� is_abs M ��� is_abs N``,
1000  HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN
1001  METIS_TAC [relationTheory.RTC_RULES, normorder_preserves_is_abs]);
1002
1003
1004val normstar_to_vhead_wstar0 = prove(
1005  ``���M N. M -n->* N ���
1006          ���f Ns. (N = VAR f ���� Ns) ���
1007                 ���Ms. M -w->* VAR f ���� Ms ���
1008                     (LENGTH Ms = LENGTH Ns) ���
1009                     ���i. i < LENGTH Ms ��� EL i Ms -n->* EL i Ns``,
1010  HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THENL [
1011    Q.EXISTS_TAC `Ns` THEN SRW_TAC [][],
1012    FULL_SIMP_TAC (srw_ss()) [] THEN Cases_on `whnf M` THENL [
1013      `is_abs M ��� ���v M0s. M = VAR v ���� M0s`
1014        by METIS_TAC [whnf_is_abs_appstr]
1015      THEN1
1016        METIS_TAC [normorder_preserves_is_abs, nstar_preserves_is_abs,
1017                   varappstar_not_is_abs] THEN
1018      `���Ns'. (VAR f ���� Ns = VAR v ���� Ns') ��� (LENGTH M0s = LENGTH Ns') ���
1019             ���i. i < LENGTH Ns' ��� EL i M0s -n->* EL i Ns'`
1020          by METIS_TAC [normstar_varhead, relationTheory.RTC_RULES] THEN
1021      FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [relationTheory.RTC_RULES],
1022
1023      `���M''. M -w-> M''` by METIS_TAC [whnf_def] THEN
1024      `M'' = M'` by  METIS_TAC [wh_head, head_normorder, normorder_det] THEN
1025      METIS_TAC [relationTheory.RTC_RULES]
1026    ]
1027  ]);
1028
1029val normstar_to_vhead_wstar = save_thm(
1030  "normstar_to_vhead_wstar",
1031  SIMP_RULE (srw_ss() ++ DNF_ss) [] normstar_to_vhead_wstar0);
1032
1033val leneq1 = prove(
1034  ``(LENGTH list = 1) ��� ���e. list = [e]``,
1035  Cases_on `list` THEN SRW_TAC [][listTheory.LENGTH_NIL]);
1036val leneq2 = prove(
1037  ``(LENGTH list = 2) ��� ���e��� e���. list = [e���; e���]``,
1038  Cases_on `list` THEN SRW_TAC [][leneq1]);
1039
1040val normstar_to_vheadnullary_wstar = save_thm(
1041  "normstar_to_vheadnullary_wstar",
1042  normstar_to_vhead_wstar
1043    |> SPEC_ALL |> Q.INST [`Ns` |-> `[]`]
1044    |> SIMP_RULE (srw_ss()) [listTheory.LENGTH_NIL]);
1045
1046val normstar_to_vheadunary_wstar = save_thm(
1047  "normstar_to_vheadunary_wstar",
1048  normstar_to_vhead_wstar
1049    |> SPEC_ALL |> Q.INST [`Ns` |-> `[N]`]
1050    |> SIMP_RULE (srw_ss() ++ DNF_ss) [leneq1, DECIDE ``x < 1 ��� (x = 0)``]);
1051
1052val normstar_to_vheadbinary_wstar = save_thm(
1053  "normstar_to_vheadbinary_wstar",
1054  normstar_to_vhead_wstar
1055    |> SPEC_ALL |> Q.INST [`Ns` |-> `[N���; N���]`]
1056    |> SIMP_RULE (srw_ss() ++ DNF_ss)
1057                 [leneq2, DECIDE ``x < 2 ��� (x = 0) ��� (x = 1)``]);
1058
1059val _ = export_theory()
1060