1open HolKernel Parse boolLib bossLib
2
3open listTheory rich_listTheory
4open primrecfnsTheory
5
6open lcsymtacs
7
8val _ = new_theory "recursivefns"
9
10val minimise_def = Define`
11  minimise f l =
12    if (���n. (f (n::l) = SOME 0) ��� ���i. i < n ��� ���m. 0 < m ��� (f (i::l) = SOME m))
13    then
14      SOME (@n. (f (n :: l) = SOME 0) ���
15                ���i. i < n ��� ���m. 0 < m ��� (f (i::l) = SOME m))
16    else NONE
17`;
18
19val recCn_def = Define`
20  recCn (f:num list -> num option) gs l =
21         let results = MAP (��g : num list -> num option. g l) gs
22         in
23           if EVERY (��r. r ��� NONE) results then f (MAP THE results)
24           else NONE
25`;
26
27val recPr_def = Define`
28  recPr zf sf l =
29    case l of
30      [] => zf []
31    | 0::t => zf t
32    | SUC n::t => case recPr zf sf (n :: t) of
33                    NONE => NONE
34                  | SOME r => sf (n::r::t)
35`;
36
37val (recfn_rules, recfn_ind, recfn_cases) = Hol_reln`
38  recfn (SOME o K 0) 1 ���
39  recfn (SOME o succ) 1 ���
40  (���i n. i < n ��� recfn (SOME o proj i) n) ���
41  (���f gs m. recfn f (LENGTH gs) ��� EVERY (��g. recfn g m) gs ���
42            recfn (recCn f gs) m) ���
43  (���zf sf n. recfn zf (n - 1) ��� recfn sf (n + 1) ��� recfn (recPr zf sf) n) ���
44  (���f n. 0 < n ��� recfn f (n + 1) ��� recfn (minimise f) n)
45`;
46
47val recfn_rulesl = CONJUNCTS recfn_rules
48val recfnCn = save_thm("recfnCn", List.nth(recfn_rulesl, 3))
49val recfnPr = save_thm("recfnPr", List.nth(recfn_rulesl, 4))
50
51val primrec_recfn = store_thm(
52  "primrec_recfn",
53  ``���f n. primrec f n ��� recfn (SOME o f) n``,
54  Induct_on ���primrec��� >> SRW_TAC [][recfn_rules] THENL [
55    `SOME o Cn f gs = recCn (SOME o f) (MAP (��g. SOME o g) gs)`
56       by SRW_TAC [][FUN_EQ_THM, recCn_def, LET_THM, MAP_MAP_o,
57                     combinTheory.o_ABS_R, EVERY_MAP, Cn_def] THEN
58    SRW_TAC [][] THEN MATCH_MP_TAC recfnCn THEN
59    SRW_TAC [][EVERY_MAP] THEN FULL_SIMP_TAC (srw_ss()) [EVERY_MEM],
60
61    `SOME o Pr f f' = recPr (SOME o f) (SOME o f')`
62       by (SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN Q.X_GEN_TAC `list` THEN
63           `(list = []) ��� ���m ms. list = m :: ms`
64              by (Cases_on `list` THEN SRW_TAC [][])
65             THEN1 SRW_TAC [][Once recPr_def, Once Pr_def] THEN
66           SRW_TAC [][] THEN
67           Induct_on `m` THEN SRW_TAC [][Once recPr_def] THEN
68           POP_ASSUM (SUBST1_TAC o SYM) THEN SRW_TAC [][]) THEN
69    SRW_TAC [][] THEN MATCH_MP_TAC recfnPr THEN SRW_TAC [ARITH_ss][]
70  ]);
71
72val minimise_thm = Q.store_thm(
73  "minimise_thm",
74  `minimise f l =
75     some n. (f (n::l) = SOME 0) ��� (���i. i<n ��� ���m. 0<m ��� (f (i::l) = SOME m))`,
76  simp[minimise_def] >> DEEP_INTRO_TAC optionTheory.some_intro >> rw[]
77  >- metis_tac[] >>
78  SELECT_ELIM_TAC >> rw[] >>
79  metis_tac[arithmeticTheory.LESS_LESS_CASES, prim_recTheory.LESS_REFL,
80            optionTheory.SOME_11]);
81
82val totalrec_def = Define`
83  totalrec f n = recfn f n ��� ���l. (LENGTH l = n) ��� ���m. f l = SOME m
84`;
85
86val rec1_def = Define`
87  (rec1 f [] = f 0 : num option) ���
88  (rec1 f (x::t) = f x)
89`;
90
91val rec2_def = Define`
92  (rec2 f [] = f 0 0 : num option) ���
93  (rec2 f [x] = f x 0) ���
94  (rec2 f (x::y::t) = f x y)
95`;
96val _ = export_rewrites ["rec2_def"]
97
98val recfn_K = store_thm(
99  "recfn_K[simp]",
100  ``recfn (K (SOME i)) 1``,
101  `recfn (SOME o K i) 1` by simp[primrec_recfn] >> fs[]);
102
103val MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG
104
105val recfn_short_extended = Q.store_thm(
106  "recfn_short_extended",
107  `���f n. recfn f n ���
108         ���xs. LENGTH xs ��� n ���
109              (f (xs ++ GENLIST (K 0) (n - LENGTH xs)) = f xs)`,
110  Induct_on `recfn` >> simp[] >> rpt strip_tac
111  >- (Cases_on `xs` >> simp[succ_def])
112  >- (qid_spec_tac`xs` >> Induct_on `n` >> simp[proj_def] >> rw[] >>
113      simp[EL_APPEND_EQN])
114  >- (simp[recCn_def] >> fs[EVERY_MEM] >> COND_CASES_TAC >> fs[MEM_MAP]
115      >- (COND_CASES_TAC >- simp[Cong MAP_CONG'] >> fs[] >> metis_tac[])
116      >- metis_tac[])
117  >- (Cases_on `xs` >> simp_tac (srw_ss ())[]
118      >- (ONCE_REWRITE_TAC[recPr_def] >> Cases_on `n` >> simp[GENLIST_CONS] >>
119          last_x_assum (qspec_then `[]` mp_tac) >> simp[])
120      >- (fs[] >> Induct_on`h` >> simp[]
121          >- (ONCE_REWRITE_TAC[recPr_def] >>
122              last_x_assum (qspec_then `t` mp_tac) >>
123              simp[arithmeticTheory.ADD1]) >>
124          ONCE_REWRITE_TAC[recPr_def] >> simp[] >>
125          rename [���option_CASE (recPr f g (h::t))���] >>
126          Cases_on`recPr f g (h::t)` >> simp[] >>
127          rename [���g (h1::h2::(t ++ GENLIST _ _))���] >>
128          first_x_assum(qspec_then `h1::h2::t`mp_tac) >>
129          simp[arithmeticTheory.ADD1]))
130  >- (simp[minimise_thm] >> rename [���_ (xs ++ GENLIST (K 0) _)���] >>
131      first_x_assum(qspec_then`j::xs` (mp_tac o Q.GEN`j`)) >>
132      simp[arithmeticTheory.ADD1]))
133
134val recfn_nonzero = Q.store_thm(
135  "recfn_nonzero",
136  ������f n. recfn f n ��� n ��� 0���,
137  Induct_on ���recfn��� >> rw[] >> rename [���gs ��� []���] >>
138  Cases_on ���gs��� >> fs[]);
139
140val recfn_long_truncated = Q.store_thm(
141  "recfn_long_truncated",
142  `���f n. recfn f n ��� ���l. n ��� LENGTH l ��� (f (TAKE n l) = f l)`,
143  Induct_on`recfn` >> simp[] >> rpt strip_tac
144  >- (Cases_on `l` >> fs[succ_def])
145  >- (simp[proj_def,EL_TAKE])
146  >- (simp[recCn_def] >> fs[EVERY_MEM] >> COND_CASES_TAC >> fs[MEM_MAP]
147      >- (COND_CASES_TAC >-(simp[Cong MAP_CONG']) >> fs[] >> metis_tac[])
148      >- metis_tac[])
149  >- (rename [���recfn f (n - 1)���, ���recfn g (n + 1)���, ���TAKE n l���] >>
150      ���n - 1 ��� 0��� by metis_tac[recfn_nonzero] >> ���2 ��� n��� by simp[] >>
151      ������h t. l = h::t��� by (Cases_on ���l��� >> fs[]) >> rw[] >> fs[] >>
152      Induct_on ���h��� >> ONCE_REWRITE_TAC [recPr_def] >> simp[] >>
153      Cases_on ���recPr f g (h::t)��� >> simp[] >>
154      first_x_assum
155        (qspec_then ���h1::h2::t���
156            (irule o
157             SIMP_RULE (srw_ss() ++ ARITH_ss)
158                       [listTheory.TAKE_def, ASSUME ���2 ��� n���] o
159             Q.GENL [���h1���, ���h2���])) >> simp[])
160  >- (simp[minimise_thm] >> rename [���f (TAKE (n + 1) _)���, ���n ��� LENGTH xs���] >>
161      first_x_assum(qspec_then`j::xs` (mp_tac o Q.GEN`j`)) >>
162      simp[arithmeticTheory.ADD1]));
163
164val unary_recfn_eq = Q.store_thm(
165  "unary_recfn_eq",
166  `recfn f 1 ��� (���n. f [n] = g n) ��� (f = rec1 g)`,
167  strip_tac >> simp[FUN_EQ_THM] >> Cases >> simp[rec1_def]
168  >- (drule_then (qspec_then `[]` mp_tac) recfn_short_extended >> simp[])
169  >- (drule_then (qspec_then ���h::t��� mp_tac) recfn_long_truncated >> simp[]))
170
171val recfn_rec1 = Q.store_thm(
172  "recfn_rec1",
173  `(���g. recfn g 1 ��� ���n. g [n] = f n) ��� recfn (rec1 f) 1`,
174  metis_tac[unary_recfn_eq]);
175
176val _ = export_theory()
177