1open HolKernel Parse boolLib bossLib
2
3open chap3Theory pred_setTheory termTheory boolSimps
4open nomsetTheory binderLib
5
6val _ = new_theory "head_reduction"
7
8val _ = ParseExtras.temp_loose_equality()
9
10fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
11
12val _ = set_trace "Unicode" 1
13
14val (hreduce1_rules, hreduce1_ind, hreduce1_cases) = Hol_reln`
15  (���v M N. hreduce1 (LAM v M @@ N) ([N/v]M)) ���
16  (���v M1 M2. hreduce1 M1 M2 ��� hreduce1 (LAM v M1) (LAM v M2)) ���
17  (���M1 M2 N. hreduce1 M1 M2 ��� ��is_abs M1 ��� hreduce1 (M1 @@ N) (M2 @@ N))
18`;
19
20val _ = set_fixity "-h->" (Infix(NONASSOC, 450))
21val _ = overload_on ("-h->", ``hreduce1``)
22
23val _ = set_fixity "-h->*" (Infix(NONASSOC, 450))
24val _ = overload_on ("-h->*", ``hreduce1^*``)
25
26val hreduce_ccbeta = store_thm(
27  "hreduce_ccbeta",
28  ``���M N. M -h-> N ��� M -��-> N``,
29  HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][cc_beta_thm] THEN
30  METIS_TAC []);
31
32val hreduce1_FV = store_thm(
33  "hreduce1_FV",
34  ``���M N. M -h-> N ��� ���v. v ��� FV N ��� v ��� FV M``,
35  METIS_TAC [SUBSET_DEF, hreduce_ccbeta, cc_beta_FV_SUBSET]);
36
37
38val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT,2)),
39                       fixity = Infix(NONASSOC, 950),
40                       paren_style = OnlyIfNecessary,
41                       pp_elements = [TOK "��", BreakSpace(0,0)],
42                       term_name = "apply_perm"}
43val _ = temp_overload_on ("apply_perm", ``��p M. tpm [p] M``)
44val _ = temp_overload_on ("apply_perm", ``tpm``)
45val _ = temp_overload_on ("#", ``��v t. v ��� FV t``)
46val _ = temp_set_fixity "#" (Infix(NONASSOC, 450))
47
48val tpm_hreduce_I = store_thm(
49  "tpm_hreduce_I",
50  ``���M N. M -h-> N ��� �����. ����M -h-> ����N``,
51  HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][tpm_subst, hreduce1_rules]);
52
53val tpm_hreduce = store_thm(
54  "tpm_hreduce",
55  ``���M N ��. ����M -h-> ����N ��� M -h-> N``,
56  METIS_TAC [pmact_inverse, tpm_hreduce_I]);
57
58val hreduce1_rwts = store_thm(
59  "hreduce1_rwts",
60  ``(VAR s -h-> M ��� F) ���
61    (��is_abs M ��� (M @@ N -h-> P ��� ���M'. (P = M' @@ N) ��� M -h-> M')) ���
62    (LAM v M -h-> N ��� ���M'. (N = LAM v M') ��� M -h-> M') ���
63    (LAM v M @@ N -h-> P ��� (P = [N/v]M))``,
64  REPEAT STRIP_TAC THENL [
65    SRW_TAC [][Once hreduce1_cases],
66    CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [hreduce1_cases])) THEN
67    SRW_TAC [][] THEN
68    Q_TAC SUFF_TAC `���v N. M ��� LAM v N` THEN1 METIS_TAC [] THEN
69    SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
70    FULL_SIMP_TAC (srw_ss()) [],
71    CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [hreduce1_cases])) THEN
72    SRW_TAC [DNF_ss][LAM_eq_thm, tpm_eqr] THEN EQ_TAC THEN
73    SRW_TAC [][] THEN1 SRW_TAC [][] THEN
74    Q.EXISTS_TAC `(v,v')��M2` THEN
75    SRW_TAC [][] THENL [
76      `v # (v,v')��M` by SRW_TAC [][] THEN
77      `v # M2` by METIS_TAC [hreduce1_FV] THEN
78      SRW_TAC [][GSYM tpm_ALPHA],
79
80      METIS_TAC [pmact_sing_inv, tpm_hreduce_I]
81    ],
82
83    SRW_TAC [DNF_ss][Once hreduce1_cases, LAM_eq_thm] THEN
84    SRW_TAC [][EQ_IMP_THM, tpm_eqr] THEN
85    METIS_TAC [lemma15a, pmact_flip_args, fresh_tpm_subst]
86  ]);
87
88val hnf_def = Define`hnf M = ���N. ��(M -h-> N)`;
89val hnf_thm = Store_thm(
90  "hnf_thm",
91  ``(hnf (VAR s) ��� T) ���
92    (hnf (M @@ N) ��� hnf M ��� ��is_abs M) ���
93    (hnf (LAM v M) ��� hnf M)``,
94  SRW_TAC [][hnf_def, hreduce1_rwts] THEN
95  Cases_on `is_abs M` THEN SRW_TAC [][hreduce1_rwts] THEN
96  Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
97  FULL_SIMP_TAC (srw_ss()) [hreduce1_rwts]);
98
99val hnf_tpm = Store_thm(
100  "hnf_tpm",
101  ``���M ��. hnf (����M) = hnf M``,
102  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]);
103
104val hreduce1_unique = store_thm(
105  "hreduce1_unique",
106  ``���M N1 N2. M -h-> N1 ��� M -h-> N2 ��� (N1 = N2)``,
107  Q_TAC SUFF_TAC `���M N. M -h-> N ��� ���P. M -h-> P ��� (N = P)`
108        THEN1 METIS_TAC [] THEN
109  HO_MATCH_MP_TAC hreduce1_ind THEN
110  SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]);
111
112val strong_cc_ind = IndDefLib.derive_strong_induction (compat_closure_rules,
113                                                       compat_closure_ind)
114
115val hnf_ccbeta_preserved = store_thm(
116  "hnf_ccbeta_preserved",
117  ``���M N. compat_closure beta M N ��� hnf M ��� hnf N``,
118  Q_TAC SUFF_TAC
119        `���M N. compat_closure beta M N ��� hnf M ��� hnf N`
120        THEN1 METIS_TAC [] THEN
121  HO_MATCH_MP_TAC strong_cc_ind THEN SRW_TAC [][] THENL [
122    FULL_SIMP_TAC (srw_ss()) [beta_def] THEN
123    SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [],
124
125    Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
126    FULL_SIMP_TAC (srw_ss()) [cc_beta_thm] THEN
127    SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []
128  ]);
129
130val (weak_head_rules, weak_head_ind, weak_head_cases) = Hol_reln`
131  (���v M N. weak_head (LAM v M @@ N) ([N/v]M)) ���
132  (���M��� M��� N. weak_head M��� M��� ��� weak_head (M��� @@ N) (M��� @@ N))
133`;
134val _ = set_fixity "-w->" (Infix(NONASSOC, 450))
135val _ = overload_on ("-w->", ``weak_head``)
136
137val strong_weak_ind = IndDefLib.derive_strong_induction(weak_head_rules,
138                                                        weak_head_ind)
139
140val wh_is_abs = store_thm(
141  "wh_is_abs",
142  ``���M N. M -w-> N ��� ��is_abs M``,
143  HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][]);
144
145val wh_lam = Store_thm(
146  "wh_lam",
147  ``���v M N. ��(LAM v M -w-> N)``,
148  ONCE_REWRITE_TAC [weak_head_cases] THEN SRW_TAC [][]);
149
150val wh_head = store_thm(
151  "wh_head",
152  ``���M N. M -w-> N ��� M -h-> N``,
153  HO_MATCH_MP_TAC strong_weak_ind THEN METIS_TAC [wh_is_abs, hreduce1_rules]);
154
155
156
157val _ = set_fixity "-w->*" (Infix(NONASSOC, 450))
158val _ = overload_on ("-w->*", ``RTC (-w->)``)
159
160val whead_FV = store_thm(
161  "whead_FV",
162  ``���M N. M -w-> N ��� v ��� FV N ��� v ��� FV M``,
163  HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][FV_SUB] THEN
164  METIS_TAC []);
165val whstar_FV = store_thm(
166  "whstar_FV",
167  ``���M N. M -w->* N ��� v ��� FV N ��� v ��� FV M``,
168  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN
169  METIS_TAC [relationTheory.RTC_RULES, whead_FV]);
170
171
172val _ = reveal "Y"
173val whY1 = store_thm(
174  "whY1",
175  ``Y @@ f -w-> Yf f``,
176  SRW_TAC [][chap2Theory.Y_def, chap2Theory.Yf_def, LET_THM,
177             Once weak_head_cases] THEN
178  NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN
179  SRW_TAC [DNF_ss][LAM_eq_thm] THEN DISJ1_TAC THEN
180  SRW_TAC [][chap2Theory.SUB_LAM_RWT, LET_THM] THEN NEW_ELIM_TAC THEN
181  SRW_TAC [][LAM_eq_thm, tpm_fresh]);
182
183val whY2 = store_thm(
184  "whY2",
185  ``Yf f -w-> f @@ Yf f``,
186  SRW_TAC [][chap2Theory.Yf_def, LET_THM, Once weak_head_cases] THEN
187  NEW_ELIM_TAC THEN SRW_TAC [DNF_ss][LAM_eq_thm, lemma14b]);
188
189val wh_unique = store_thm(
190  "wh_unique",
191  ``M -w-> N��� ��� M -w-> N��� ��� (N��� = N���)``,
192  METIS_TAC [hreduce1_unique, wh_head]);
193
194val whnf_def = Define`
195  whnf M = ���N. ��(M -w-> N)
196`;
197
198val hnf_whnf = store_thm(
199  "hnf_whnf",
200  ``hnf M ��� whnf M``,
201  METIS_TAC [hnf_def, whnf_def, wh_head]);
202
203val bnf_hnf = store_thm(
204  "bnf_hnf",
205  ``bnf M ��� hnf M``,
206  METIS_TAC [hnf_def, beta_normal_form_bnf, corollary3_2_1, hreduce_ccbeta]);
207
208val bnf_whnf = store_thm(
209  "bnf_whnf",
210  ``bnf M ��� whnf M``,
211  METIS_TAC [hnf_whnf, bnf_hnf]);
212
213val whnf_thm = Store_thm(
214  "whnf_thm",
215  ``whnf (VAR s) ���
216    (whnf (M @@ N) ��� ��is_abs M ��� whnf M) ���
217    whnf (LAM v M)``,
218  REPEAT CONJ_TAC THEN SRW_TAC [][whnf_def, Once weak_head_cases] THEN
219  EQ_TAC THEN SRW_TAC [][FORALL_AND_THM] THENL [
220    Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN SRW_TAC [][] THEN
221    METIS_TAC [],
222    Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN
223    FULL_SIMP_TAC (srw_ss()) []
224  ]);
225
226val wh_weaken_cong = store_thm(
227  "wh_weaken_cong",
228  ``whnf N ��� M��� -w->* M��� ��� (M��� -w->* N = M��� -w->* N)``,
229  SIMP_TAC (srw_ss()) [EQ_IMP_THM, IMP_CONJ_THM] THEN CONJ_TAC THENL [
230    Q_TAC SUFF_TAC `���M N. M -w->* N ��� ���N'. M -w->* N' ��� whnf N' ��� N -w->* N'`
231          THEN1 METIS_TAC [] THEN
232    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
233    METIS_TAC [relationTheory.RTC_CASES1, whnf_def, wh_unique],
234
235    METIS_TAC [relationTheory.RTC_CASES_RTC_TWICE]
236  ]);
237
238val wh_app_congL = store_thm(
239  "wh_app_congL",
240  ``M -w->* M' ==> M @@ N -w->* M' @@ N``,
241  STRIP_TAC THEN Q.ID_SPEC_TAC `N` THEN POP_ASSUM MP_TAC THEN
242  MAP_EVERY Q.ID_SPEC_TAC [`M'`, `M`] THEN
243  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
244  METIS_TAC [relationTheory.RTC_RULES, weak_head_rules]);
245
246val tpm_whead_I = store_thm(
247  "tpm_whead_I",
248  ``���M N. M -w-> N ��� ����M -w-> ����N``,
249  HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][weak_head_rules, tpm_subst]);
250
251val whead_gen_bvc_ind = store_thm(
252  "whead_gen_bvc_ind",
253  ``���P f. (���x. FINITE (f x)) ���
254          (���v M N x. v ��� f x ��� P (LAM v M @@ N) ([N/v]M) x) ���
255          (���M��� M��� N x. (���z. P M��� M��� z) ��� P (M��� @@ N) (M��� @@ N) x)
256        ���
257          ���M N. M -w-> N ��� ���x. P M N x``,
258  REPEAT GEN_TAC THEN STRIP_TAC THEN
259  Q_TAC SUFF_TAC `���M N. M -w-> N ��� ����� x. P (����M) (����N) x`
260        THEN1 METIS_TAC [pmact_nil] THEN
261  HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][tpm_subst] THEN
262  Q_TAC (NEW_TAC "z") `{lswapstr �� v} ��� FV (����M) ��� FV (����N) ��� f x` THEN
263  `LAM (lswapstr �� v) (����M) = LAM z ([VAR z/lswapstr �� v](����M))`
264     by SRW_TAC [][SIMPLE_ALPHA] THEN
265  `[����N/lswapstr �� v](����M) = [����N/z] ([VAR z/lswapstr �� v](����M))`
266     by SRW_TAC [][lemma15a] THEN
267  SRW_TAC [][]);
268
269val whead_bvcX_ind = save_thm(
270  "whead_bvcX_ind",
271  whead_gen_bvc_ind |> Q.SPECL [`��M N x. P' M N`, `��x. X`]
272                    |> SIMP_RULE (srw_ss()) []
273                    |> Q.INST [`P'` |-> `P`]
274                    |> Q.GEN `X` |> Q.GEN `P`);
275
276val wh_substitutive = store_thm(
277  "wh_substitutive",
278  ``���M N. M -w-> N ��� [P/v]M -w-> [P/v]N``,
279  HO_MATCH_MP_TAC whead_bvcX_ind THEN Q.EXISTS_TAC `FV P ��� {v}` THEN
280  SRW_TAC [][weak_head_rules] THEN
281  METIS_TAC [chap2Theory.substitution_lemma, weak_head_rules]);
282
283val whstar_substitutive = store_thm(
284  "whstar_substitutive",
285  ``���M N. M -w->* N ��� [P/v]M -w->* [P/v]N``,
286  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
287  METIS_TAC [relationTheory.RTC_RULES, wh_substitutive]);
288
289val whstar_betastar = store_thm(
290  "whstar_betastar",
291  ``���M N. M -w->* N ��� M -��->* N``,
292  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN
293  METIS_TAC [relationTheory.RTC_RULES, wh_head, hreduce_ccbeta]);
294
295val whstar_lameq = store_thm(
296  "whstar_lameq",
297  ``M -w->* N ��� M == N``,
298  METIS_TAC [betastar_lameq, whstar_betastar]);
299
300val whstar_abs = Store_thm(
301  "whstar_abs",
302  ``LAM v M -w->* N ��� (N = LAM v M)``,
303  SRW_TAC [][EQ_IMP_THM] THEN
304  FULL_SIMP_TAC (srw_ss()) [Once relationTheory.RTC_CASES1,
305                            Once weak_head_cases]);
306
307(* ----------------------------------------------------------------------
308    has_whnf
309   ---------------------------------------------------------------------- *)
310
311(* definition of has_hnf in standardisationScript has == rather than -h->*
312   as the relation on the RHS.  This means that has_bnf automatically implies
313   has_hnf, but makes the corollary to the standardisation theorem interesting
314   to prove... *)
315val has_whnf_def = Define`
316  has_whnf M = ���N. M -w->* N ��� whnf N
317`;
318
319val has_whnf_APP_E = store_thm(
320  "has_whnf_APP_E",
321  ``has_whnf (M @@ N) ��� has_whnf M``,
322  simp_tac (srw_ss())[has_whnf_def] >>
323  Q_TAC SUFF_TAC
324     `���M N. M -w->* N ��� ���M0 M1. (M = M0 @@ M1) ��� whnf N ���
325                                 ���N'. M0 -w->* N' ��� whnf N'`
326     >- metis_tac [] >>
327  ho_match_mp_tac relationTheory.RTC_INDUCT >> conj_tac
328    >- (simp_tac (srw_ss()) [] >> metis_tac [relationTheory.RTC_RULES]) >>
329  srw_tac [][] >> Cases_on `is_abs M0`
330    >- (Q.SPEC_THEN `M0` FULL_STRUCT_CASES_TAC term_CASES >>
331        full_simp_tac (srw_ss()) [] >>
332        metis_tac [relationTheory.RTC_RULES, whnf_thm]) >>
333  full_simp_tac (srw_ss()) [Once weak_head_cases] >>
334  metis_tac [relationTheory.RTC_RULES])
335
336val hreduce_weak_or_strong = store_thm(
337  "hreduce_weak_or_strong",
338  ``���M N. M -h-> N ��� whnf M ��� M -w-> N``,
339  ho_match_mp_tac simple_induction >> simp_tac (srw_ss()) [] >>
340  rpt gen_tac >> strip_tac >> rpt gen_tac >>
341  simp_tac (srw_ss()) [Once hreduce1_cases] >>
342  simp_tac (srw_ss() ++ DNF_ss) [] >> conj_tac
343    >- metis_tac [weak_head_rules] >>
344  srw_tac [][] >> metis_tac [weak_head_rules]);
345
346val head_reductions_have_weak_prefixes = store_thm(
347  "head_reductions_have_weak_prefixes",
348  ``���M N. M -h->* N ��� hnf N ���
349          ���N0. M -w->* N0 ��� whnf N0 ��� N0 -h->* N``,
350   ho_match_mp_tac relationTheory.RTC_STRONG_INDUCT >> conj_tac
351     >- metis_tac [hnf_whnf, relationTheory.RTC_RULES] >>
352   metis_tac [relationTheory.RTC_RULES, hreduce_weak_or_strong]);
353
354val _ = export_theory()
355