1open HolKernel boolLib bossLib Parse
2
3open normal_orderTheory
4open reductionEval
5
6fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n]
7
8val _ = new_theory "steps"
9
10val steps_def = Define`
11  (steps 0 t = t) ���
12  (steps (SUC n) t = if bnf t then t else steps n (THE (noreduct t)))
13`;
14val _ = export_rewrites ["steps_def"]
15
16val bnf_steps = store_thm(
17  "bnf_steps",
18  ``(bnf_of t = SOME u) ��� ���n. (steps n t = u) ��� bnf u``,
19  SRW_TAC [][EQ_IMP_THM] THENL [
20    IMP_RES_TAC bnf_of_SOME THEN SRW_TAC [][] THEN
21    Q.PAT_ASSUM `t -n->* u` MP_TAC THEN
22    MAP_EVERY Q.ID_SPEC_TAC [`u`, `t`] THEN
23    HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN1
24      (Q.EXISTS_TAC `0` THEN SRW_TAC[][]) THEN
25    Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][] THEN1
26      (METIS_TAC [normorder_bnf]) THEN
27    FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation],
28
29    POP_ASSUM MP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`,`n`] THEN
30    Induct THEN SRW_TAC [][] THENL [
31      MATCH_MP_TAC nstar_bnf_of_SOME_I THEN SRW_TAC [][],
32      MATCH_MP_TAC nstar_bnf_of_SOME_I THEN SRW_TAC [][],
33      SRW_TAC [][Once bnf_of_thm]
34    ]
35  ]);
36
37val RTC_L1_I = CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES)
38
39val steps_nstar = store_thm(
40  "steps_nstar",
41  ``���n t. t -n->* steps n t``,
42  Induct THEN SRW_TAC [][] THEN MATCH_MP_TAC RTC_L1_I THEN
43  Q.EXISTS_TAC `THE (noreduct t)` THEN SRW_TAC [][] THEN
44  `���u. t -n-> u` by METIS_TAC [normorder_bnf] THEN
45  `noreduct t = SOME u` by METIS_TAC [noreduct_characterisation] THEN
46  SRW_TAC [][]);
47
48val bnf_steps_upwards_closed = store_thm(
49  "bnf_steps_upwards_closed",
50  ``���n m t. bnf (steps n t) ��� n < m ��� (steps m t = steps n t)``,
51  Induct_on `n` THEN SRW_TAC [][] THENL [
52    Cases_on `m` THEN SRW_TAC [][],
53    Cases_on `m` THEN SRW_TAC [][],
54    Cases_on `m` THEN FULL_SIMP_TAC (srw_ss()) []
55  ]);
56
57val nstar_steps = store_thm(
58  "nstar_steps",
59  ``���M N. M -n->* N ��� ���n. N = steps n M``,
60  HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN1
61    (Q.EXISTS_TAC `0` THEN SRW_TAC [][]) THEN
62  FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation] THEN
63  Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][] THEN
64  FULL_SIMP_TAC (srw_ss()) [SYM noreduct_bnf]);
65
66val steps_noreduct = store_thm(
67  "steps_noreduct",
68  ``���t. ��bnf (steps n t) ���
69        (steps n (THE (noreduct t)) = THE (noreduct (steps n t)))``,
70  Induct_on `n` THEN SRW_TAC [][] THEN
71  POP_ASSUM MP_TAC THEN Cases_on `n` THEN SRW_TAC [][]);
72
73val steps_plus = store_thm(
74  "steps_plus",
75  ``���t. steps (m + n) t = steps m (steps n t)``,
76  Induct_on `m` THEN SRW_TAC [][arithmeticTheory.ADD_CLAUSES] THENL [
77    Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [],
78    POP_ASSUM MP_TAC THEN Cases_on `n` THEN SRW_TAC [][],
79    `steps n (THE (noreduct t)) = steps n t`
80      by METIS_TAC [bnf_steps_upwards_closed, steps_def,
81                    DECIDE ``n < SUC n``] THEN
82    Cases_on `m` THEN SRW_TAC [][],
83    SRW_TAC [][steps_noreduct]
84  ]);
85
86val bnf_steps_fixpoint = store_thm(
87  "bnf_steps_fixpoint",
88  ``bnf M ��� (steps n M = M)``,
89  METIS_TAC [bnf_steps_upwards_closed, DECIDE ``0 < n ��� (n = 0)``, steps_def]);
90
91val _ = export_theory ()
92