1open HolKernel boolLib bossLib Parse
2
3open pure_dBTheory normal_orderTheory
4
5fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
6
7val _ = new_theory "dnoreduct"
8
9val dest_dabs_def = Define`
10  (dest_dabs (dABS t) = t)
11`;
12val _ = export_rewrites ["dest_dabs_def"]
13
14val dnoreduct_def = Define`
15  (dnoreduct (dV i) = NONE) ���
16  (dnoreduct (dAPP t u) =
17     if is_dABS t then SOME (nsub u 0 (dest_dabs t))
18     else if dbnf t then OPTION_MAP (dAPP t) (dnoreduct u)
19     else  SOME (dAPP (THE (dnoreduct t)) u)) ���
20  (dnoreduct (dABS t) = OPTION_MAP dABS (dnoreduct t))
21`;
22val _ = export_rewrites ["dnoreduct_def"]
23
24val notbnf_noreduct = prove(
25  ``��bnf t ��� ���u. noreduct t = SOME u``,
26  Cases_on `noreduct t` THEN1 FULL_SIMP_TAC (srw_ss()) [noreduct_bnf] THEN
27  SRW_TAC [][]);
28
29val notbnf_dnoreduct = store_thm(
30  "notbnf_dnoreduct",
31  ``��dbnf t ��� ���u. dnoreduct t = SOME u``,
32  Induct_on `t` THEN SRW_TAC [][]);
33
34val dnoreduct_dbeta = store_thm(
35  "dnoreduct_dbeta",
36  ``���t u. (dnoreduct t = SOME u) ��� dbeta t u``,
37  Induct_on `t` THEN SRW_TAC [][] THENL [
38    Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
39    METIS_TAC [dbeta_rules],
40    METIS_TAC [dbeta_rules],
41    IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][] THEN
42    METIS_TAC [dbeta_rules],
43    METIS_TAC [dbeta_rules]
44  ]);
45
46val dnoreduct_FV = store_thm(
47  "dnoreduct_FV",
48  ``(dnoreduct t = SOME u) ��� v ��� dFV u ��� v ��� dFV t``,
49  STRIP_TAC THEN IMP_RES_TAC dnoreduct_dbeta THEN
50  FULL_SIMP_TAC (srw_ss()) [dbeta_dbeta'_eqn] THEN
51  `���tt uu. (t = fromTerm tt) ��� (u = fromTerm uu)`
52     by METIS_TAC [fromTerm_onto] THEN
53  FULL_SIMP_TAC (srw_ss()) [IN_dFV, dbeta'_eq_ccbeta] THEN
54  METIS_TAC [chap3Theory.cc_beta_FV_SUBSET, pred_setTheory.SUBSET_DEF]);
55
56val dpm_is_dABS = Store_thm(
57  "dpm_is_dABS",
58  ``is_dABS (dpm �� t) = is_dABS t``,
59  Cases_on `t` THEN SRW_TAC [][]);
60
61val dpm_dbnf = Store_thm(
62  "dpm_dbnf",
63  ``�����. dbnf (dpm �� t) = dbnf t``,
64  Induct_on `t` THEN SRW_TAC [][]);
65
66val dest_dabs_dpm = store_thm(
67  "dest_dabs_dpm",
68  ``is_dABS d ��� (dest_dabs (dpm �� d) = dpm (inc_pm 0 ��) (dest_dabs d))``,
69  Cases_on `d` THEN SRW_TAC [][]);
70
71val dnoreduct_dpm = store_thm(
72  "dnoreduct_dpm",
73  ``���d ��. dnoreduct (dpm �� d) = OPTION_MAP (dpm ��) (dnoreduct d)``,
74  Induct_on `d` THEN
75  SRW_TAC [][dpm_nsub, optionTheory.OPTION_MAP_COMPOSE, combinTheory.o_DEF,
76             dest_dabs_dpm] THEN
77  IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][]);
78
79val dnoreduct_dLAM = Store_thm(
80  "dnoreduct_dLAM",
81  ``dnoreduct (dLAM i t) = OPTION_MAP (dLAM i) (dnoreduct t)``,
82  SRW_TAC [][dLAM_def] THEN
83  `dLAM i = ��t. dLAM i t` by SRW_TAC [][FUN_EQ_THM] THEN
84  POP_ASSUM SUBST1_TAC THEN SRW_TAC [][dLAM_def] THEN
85  Q.ABBREV_TAC `MX = if dFV t = {} then 0 else MAX_SET (dFV t)` THEN
86  `���i. i ��� dFV t ��� i ��� MX`
87      by SRW_TAC [][Abbr`MX`, pred_setTheory.MAX_SET_DEF] THEN
88  Q.ABBREV_TAC `�� = lifting_pm 0 MX` THEN
89  `lift t 0 = dpm �� t`
90     by SRW_TAC [][lifts_are_specific_dpms, Abbr`��`] THEN
91  `0 ��� dFV (lift t 0)` by SRW_TAC [][] THEN
92  `sub (dV 0) (i + 1) (lift t 0) = dpm [(n2s 0, n2s (i + 1))] (lift t 0)`
93     by SRW_TAC [][fresh_dpm_sub] THEN
94  SRW_TAC [][dnoreduct_dpm, optionTheory.OPTION_MAP_COMPOSE] THEN
95  `(dnoreduct t = NONE) ��� ���u. dnoreduct t = SOME u`
96     by (Cases_on `dnoreduct t` THEN SRW_TAC [][]) THEN
97  SRW_TAC [][] THEN
98  `���i. i ��� dFV u ��� i ��� MX` by METIS_TAC [dnoreduct_FV] THEN
99  `lift u 0 = dpm �� u`
100     by SRW_TAC [][lifts_are_specific_dpms, Abbr`��`] THEN
101  `0 ��� dFV (lift u 0)` by SRW_TAC [][] THEN
102  `sub (dV 0) (i + 1) (lift u 0) = dpm [(n2s 0, n2s (i + 1))] (lift u 0)`
103     by SRW_TAC [][fresh_dpm_sub] THEN
104  SRW_TAC [][]);
105
106val dnoreduct_correct = store_thm(
107  "dnoreduct_correct",
108  ``���t. noreduct t = OPTION_MAP toTerm (dnoreduct (fromTerm t))``,
109  HO_MATCH_MP_TAC termTheory.simple_induction THEN
110  SRW_TAC [][noreduct_thm, optionTheory.OPTION_MAP_COMPOSE,
111             combinTheory.o_DEF]
112  THENL [
113    `���v t0. t = LAM v t0`
114       by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC termTheory.term_CASES THEN
115           FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []) THEN
116    ASM_SIMP_TAC (srw_ss()) [noreduct_thm, dLAM_def, GSYM sub_nsub,
117                             GSYM fromTerm_subst],
118
119    `��dbnf (fromTerm t)` by SRW_TAC [][] THEN
120    IMP_RES_TAC notbnf_dnoreduct THEN SRW_TAC [][]
121  ]);
122
123val omap_lemma = prove(``OPTION_MAP (��x. x) y = y``,
124                       Cases_on `y` THEN SRW_TAC [][])
125
126val dnoreduct_thm = Store_thm(
127  "dnoreduct_thm",
128  ``(dnoreduct (fromTerm t) = OPTION_MAP fromTerm (noreduct t)) ���
129    (noreduct (toTerm d) = OPTION_MAP toTerm (dnoreduct d))``,
130  SRW_TAC [][dnoreduct_correct, optionTheory.OPTION_MAP_COMPOSE,
131             combinTheory.o_DEF, omap_lemma]);
132
133val _ = export_theory()
134