1open HolKernel Parse boolLib bossLib;
2
3open numpairTheory primrecfnsTheory nlistTheory arithmeticTheory listTheory
4     recursivefnsTheory
5
6val _ = new_theory "unary_recfns";
7
8val _ = monadsyntax.enable_monadsyntax()
9val _ = monadsyntax.enable_monad "option"
10
11Definition pr1_pr_def:
12  pr1_pr b s n =
13   if nfst n = 0 then b (nsnd n)
14   else
15     s ((nfst n - 1) ��� pr1_pr b s ((nfst n - 1) ��� nsnd n) ��� nsnd n)
16Termination
17  WF_REL_TAC ���measure (��(b,s,n). nfst n)��� >> simp[]
18End
19
20Theorem pr1_pr_thm[simp]:
21  pr1_pr b s (0 ��� v) = b v ���
22  pr1_pr b s (SUC n ��� v) = s (n ��� pr1_pr b s (n ��� v) ��� v) ���
23  pr1_pr b s ((n + 1) ��� v) = s (n ��� pr1_pr b s (n ��� v) ��� v)
24Proof
25  csimp[GSYM ADD1] >> conj_tac >>
26  simp[Once pr1_pr_def, SimpLHS]
27QED
28
29
30Inductive primrec1:
31  primrec1 (K 0) ���
32  primrec1 SUC ���
33  primrec1 nfst ���
34  primrec1 nsnd ���
35  (���f g. primrec1 f ��� primrec1 g ��� primrec1 (��n. f n ��� g n)) ���
36  (���f g. primrec1 f ��� primrec1 g ��� primrec1 (f o g)) ���
37  (���b s. primrec1 b ��� primrec1 s ��� primrec1 (pr1_pr b s))
38End
39
40Theorem primrec1_I[simp]:
41  primrec1 I ��� primrec1 (��x. x)
42Proof
43  ���I = (��x:num. x)��� by simp[FUN_EQ_THM] >> simp[] >>
44  ���primrec1 (��n. nfst n ��� nsnd n)��� by metis_tac[primrec1_rules] >>
45  fs[]
46QED
47
48Theorem primrec1_add:
49  primrec1 (��n. nfst n + nsnd n)
50Proof
51  ���primrec1 (SUC o nfst o nfst)��� by metis_tac[primrec1_rules] >>
52  qabbrev_tac ���ADD = pr1_pr I (SUC o nfst o nsnd)��� >>
53  ���primrec1 ADD��� by metis_tac[primrec1_rules, primrec1_I] >>
54  ���ADD = (��n. nfst n + nsnd n)��� suffices_by (rw[] >> fs[]) >>
55  simp[FUN_EQ_THM, Abbr���ADD���] >> gen_tac >>
56  ������x y. n = x ��� y��� by metis_tac[npair_cases] >> rw[] >> Induct_on ���x��� >>
57  simp[]
58QED
59
60Theorem primrec_Cn = List.nth (CONJUNCTS primrec_rules, 3)
61
62Theorem primrec1_primrec:
63  ���f. primrec1 f ��� ���g. primrec g 1 ��� ���n. g [n] = f n
64Proof
65  Induct_on ���primrec1��� >> rw[]
66  >- (qexists_tac ���zerof��� >> simp[])
67  >- (qexists_tac ���succ��� >> simp[primrec_rules])
68  >- (qexists_tac ���pr1 nfst��� >> simp[primrec_nfst])
69  >- (qexists_tac ���pr1 nsnd��� >> simp[primrec_nsnd])
70  >- (rename [���f1 _ ��� f2 _���, ���g1 [_] = f1 _���, ���g2 [_] = f2 _���] >>
71      qexists_tac ���Cn (pr2 npair) [g1; g2]��� >> simp[primrec_rules])
72  >- (rename [���f1 (f2 _)���, ���g1 [_] = f1 _���, ���g2 [_] = f2 _���] >>
73      qexists_tac ���Cn g1 [g2]���>> simp[primrec_rules]) >>
74  rename [���pr1_pr b1 s1���, ���b [_] = b1 _���, ���s [_] = s1 _���] >>
75  qexists_tac
76    ���Cn (Pr b (Cn s [Cn (pr2 npair) [proj 0; Cn (pr2 npair) [proj 1; proj 2]]]))
77        [pr1 nfst; pr1 nsnd]��� >>
78  conj_tac
79  >- (irule primrec_Cn >> simp[] >> irule alt_Pr_rule >> simp[primrec_rules]) >>
80  gen_tac >>
81  ������x y. n = x ��� y��� by metis_tac[npair_cases] >> rw[] >> Induct_on ���x��� >>
82  simp[]
83QED
84
85Definition unfold_def[simp]:
86  unfold 0 m = [] ���
87  unfold (SUC n) m = if n = 0 then [m]
88                     else nfst m :: unfold n (nsnd m)
89End
90
91Theorem unfold1[simp]:
92  unfold 1 n = [n]
93Proof
94  simp_tac bool_ss [ONE, unfold_def]
95QED
96
97Theorem unfold_LENGTH[simp]:
98  ���m n. LENGTH (unfold m n) = m
99Proof
100  Induct_on ���m��� >> rw[]
101QED
102
103Theorem unfold_EQ_NIL[simp]:
104  unfold a n = [] ��� a = 0
105Proof
106  Cases_on ���a��� >> rw[]
107QED
108
109Definition fold_def[simp]:
110  fold [] = 0 ���
111  fold [x] = x ���
112  fold (x::xs) = x ��� fold xs
113End
114
115Theorem fold_unfold[simp]:
116  ���a n. 0 < a ��� fold (unfold a n) = n
117Proof
118  Induct >> rw[] >>
119  Cases_on ���unfold a (nsnd n)��� >> fs[] >>
120  pop_assum (assume_tac o SYM) >> simp[]
121QED
122
123Theorem unfold_fold[simp]:
124  ���l. unfold (LENGTH l) (fold l) = l
125Proof
126  Induct_on ���l��� >> simp[] >> rw[] >> Cases_on ���l��� >> fs[]
127QED
128
129Theorem unfold_fold_alt:
130  n = LENGTH l ��� unfold n (fold l) = l
131Proof
132  simp[]
133QED
134
135Triviality FUNPOW_o:
136  FUNPOW f 0 = I ���
137  FUNPOW f (SUC n) = f o FUNPOW f n
138Proof
139  simp[FUN_EQ_THM, FUNPOW_SUC]
140QED
141
142Definition foldfs_def[simp]:
143  foldfs [f] n = f n ���
144  foldfs (f::fs) n = f n ��� foldfs fs n
145End
146
147Theorem foldfs_as_function:
148  foldfs [f] = f ���
149  foldfs (f::g::fs) = ��n. f n ��� foldfs (g::fs) n
150Proof
151  simp[FUN_EQ_THM]
152QED
153
154Theorem primrec1_foldfs:
155  fs ��� [] ��� (���f. MEM f fs ��� primrec1 f) ��� primrec1 (foldfs fs)
156Proof
157  Induct_on ���fs��� >> simp[DISJ_IMP_THM, FORALL_AND_THM] >> qx_gen_tac ���f��� >>
158  Cases_on ���fs��� >> fs[foldfs_as_function, DISJ_IMP_THM, FORALL_AND_THM] >>
159  metis_tac[primrec1_rules]
160QED
161
162Theorem unfold_foldfs:
163  ���a fs n. 0 < a ��� LENGTH fs = a ��� unfold a (foldfs fs n) = MAP (��f. f n) fs
164Proof
165  Induct_on ���fs��� >> simp[] >> fs[] >> rw[]
166  >- (Cases_on ���fs��� >> fs[]) >>
167  Cases_on ���fs��� >> fs[]
168QED
169
170Theorem MAP_CONG' = REWRITE_RULE [GSYM AND_IMP_INTRO] MAP_CONG
171
172Theorem primrec_primrec1:
173  ���f a. primrec f a ��� ���g. primrec1 g ��� ���n. g n = f (unfold a n)
174Proof
175  Induct_on ���primrec��� >> rw[]
176  >- (qexists_tac ���K 0��� >> simp[primrec1_rules])
177  >- (qexists_tac ���SUC��� >> simp[primrec1_rules])
178  >- (rename [���proj i (unfold a _)���] >>
179      qexists_tac ���(if i + 1 = a then I else nfst) o FUNPOW nsnd i��� >> conj_tac
180      >- (pop_assum (K ALL_TAC) >>
181          ���primrec1 (FUNPOW nsnd i)���
182            suffices_by metis_tac[primrec1_rules, primrec1_I] >>
183          Induct_on ���i��� >> simp[FUNPOW_o, primrec1_rules]) >>
184      pop_assum mp_tac >> qid_spec_tac ���a��� >>
185      ONCE_REWRITE_TAC [EQ_SYM_EQ] >>
186      Induct_on ���i��� >> simp[]
187      >- (rw[] >> simp[] >> Cases_on ���a��� >> simp[]) >>
188      rw[]
189      >- (simp_tac bool_ss [GSYM ADD1, Once unfold_def] >>
190          simp[Excl "unfold_def"] >> simp[FUNPOW]) >>
191      ������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >> fs[FUNPOW])
192  >- (fs[listTheory.EVERY_MEM, PULL_EXISTS, GSYM RIGHT_EXISTS_IMP_THM] >>
193      fs[SKOLEM_THM] >> rename [���primrec1 (mk1 _)���] >>
194      rename [���f1 _ = f (unfold (LENGTH gs) _)���] >>
195      qexists_tac ���f1 o foldfs (MAP mk1 gs)��� >>
196      ���gs ��� []��� by (strip_tac >> fs[] >> drule primrec_nzero >> simp[]) >>
197      conj_tac
198      >- simp[primrec1_foldfs, primrec1_rules, MEM_MAP, PULL_EXISTS] >>
199      ���0 < LENGTH gs��� by (CCONTR_TAC >> fs[]) >>
200      simp[Cn_def, unfold_foldfs, MAP_MAP_o, combinTheory.o_ABS_L,
201           Cong MAP_CONG']) >>
202  rename [���b1 _ = b (unfold a _)���, ���s1 _ = s (unfold (a + 2) _)���] >>
203  ���0 < a��� by metis_tac[primrec_nzero] >>
204  qexists_tac ���pr1_pr b1 s1��� >> simp[primrec1_rules] >>
205  simp[GSYM ADD1] >>
206  qx_gen_tac ���N��� >>
207  ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >>
208  Induct_on ���x��� >> simp[] >> ������n. n + 2 = SUC (SUC n)��� by simp[] >> simp[]
209QED
210
211Theorem primrec_primrec1_fold:
212  ���f a. primrec f a ��� ���g. primrec1 g ��� ���l. LENGTH l = a ��� f l = g (fold l)
213Proof
214  rw[] >> drule_then (qx_choose_then ���G��� strip_assume_tac) primrec_primrec1 >>
215  qexists_tac ���G��� >> rw[] >> rw[unfold_fold]
216QED
217
218Definition recpair_def:
219  recpair f g (n:num) = do i <- f n; j <- g n; return (i ��� j); od
220End
221
222Definition recCn1_def:
223  recCn1 (f:num->num option) g (n:num) = do x <- g n ; f x; od
224End
225
226Definition recPr1_def:
227  recPr1 b s n = if nfst n = 0 then b (nsnd n)
228                 else do
229                        r <- recPr1 b s ((nfst n - 1) ��� nsnd n) ;
230                        s ((nfst n - 1) ��� r ��� nsnd n)
231                      od
232Termination
233  WF_REL_TAC ���measure (��(b,s,n). nfst n)��� >> simp[]
234End
235
236Theorem recPr1_thm[simp]:
237  recPr1 b s (0 ��� m) = b m ���
238  recPr1 b s (SUC n ��� m) = do r <- recPr1 b s (n ��� m) ;
239                              s (n ��� r ��� m) ;
240                           od
241Proof
242  conj_tac >> simp[Once recPr1_def, SimpLHS]
243QED
244
245Definition recMin1_def:
246  recMin1 f m =
247    OLEAST n. f (n ��� m) = SOME 0 ��� ���i. i < n ��� ���r. f (i ��� m) = SOME r
248End
249
250Inductive recfn1:
251  recfn1 (SOME o K 0) ���
252  recfn1 (SOME o SUC) ���
253  recfn1 (SOME o nfst) ���
254  recfn1 (SOME o nsnd) ���
255  (���f g. recfn1 f ��� recfn1 g ��� recfn1 (recpair f g)) ���
256  (���f g. recfn1 f ��� recfn1 g ��� recfn1 (recCn1 f g)) ���
257  (���b s. recfn1 b ��� recfn1 s ��� recfn1 (recPr1 b s)) ���
258  (���f. recfn1 f ��� recfn1 (recMin1 f))
259End
260
261Theorem primrec1_recfn1:
262  ���f. primrec1 f ��� recfn1 (SOME o f)
263Proof
264  Induct_on ���primrec1��� >> rw[recfn1_rules]
265  >- (rename [���f1 _ ��� f2 _���] >>
266      ���recfn1 (recpair (SOME o f1)(SOME o f2))��� by simp[recfn1_rules] >>
267      pop_assum mp_tac >>
268      qmatch_abbrev_tac ���recfn1 F1 ��� recfn1 F2��� >>
269      ���F1 = F2��� suffices_by simp[] >>
270      simp[recpair_def, Abbr���F1���, Abbr���F2���, FUN_EQ_THM])
271  >- (rename [���SOME o f o g���] >>
272      ���recCn1 (SOME o f) (SOME o g) = SOME o f o g���
273        suffices_by metis_tac[recfn1_rules] >>
274      simp[FUN_EQ_THM, recCn1_def])
275  >- (rename [���SOME o pr1_pr b s���] >>
276      ���recPr1 (SOME o b) (SOME o s) = SOME o pr1_pr b s���
277        suffices_by metis_tac[recfn1_rules] >>
278      simp[FUN_EQ_THM] >> qx_gen_tac ���N��� >>
279      ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >>
280      Induct_on ���x��� >> simp[])
281QED
282
283Theorem recfn1_recfn:
284  ���f. recfn1 f ��� recfn (rec1 f) 1
285Proof
286  Induct_on ���recfn1��� >> rw[] >> irule recfn_rec1
287  >- (qexists_tac ���K (SOME 0)��� >> simp[])
288  >- (qexists_tac ���SOME o succ��� >> simp[recfn_rules])
289  >- (qexists_tac ���SOME o pr1 nfst��� >> simp[] >>
290      irule primrec_recfn >> simp[])
291  >- (qexists_tac ���SOME o pr1 nsnd��� >> simp[] >>
292      irule primrec_recfn >> simp[])
293  >- (rename [���recpair f1 f2���] >>
294      qexists_tac ���recCn (SOME o pr2 npair) [rec1 f1; rec1 f2]��� >>
295      simp[recCn_def, recpair_def, rec1_def] >> conj_tac
296      >- (irule recfnCn >> simp[] >> irule primrec_recfn >> simp[]) >>
297      qx_gen_tac ���N��� >> Cases_on ���f1 N��� >> simp[] >> Cases_on ���f2 N��� >> simp[])
298  >- (rename [���recCn1 f g _���] >>
299      qexists_tac ���recCn (rec1 f) [rec1 g]��� >> simp[recfn_rules] >>
300      simp[recCn_def, recCn1_def, rec1_def] >> qx_gen_tac ���N��� >>
301      Cases_on ���g N��� >> simp[])
302  >- (rename [���recPr1 b s _���] >>
303      qexists_tac
304        ���recCn (recPr (rec1 b)
305                      (recCn (rec1 s) [
306                          SOME o Cn (pr2 npair) [
307                            proj 0;
308                            Cn (pr2 npair) [proj 1; proj 2]
309                          ]
310                       ]))
311               [SOME o pr1 nfst; SOME o pr1 nsnd]��� >>
312      conj_tac
313      >- (irule recfnCn >> simp[primrec_recfn] >>
314          irule recfnPr >> simp[] >> irule recfnCn >> simp[] >>
315          irule primrec_recfn >> irule primrec_Cn >>
316          simp[primrec_rules]) >>
317      qx_gen_tac ���N��� >> ������x y. N = x ��� y��� by metis_tac[npair_cases] >>
318      rw[recCn_def] >> Induct_on ���x��� >> simp[Once recPr_def, rec1_def] >>
319      Cases_on ���recPr1 b s (x ��� y)��� >> simp[recCn_def, rec1_def]) >>
320  rename [���recMin1 f���] >>
321  qexists_tac
322    ���minimise (recCn (rec1 f) [SOME o Cn (pr2 $*,) [proj 0; proj 1]])��� >>
323  conj_tac
324  >- (irule (last (CONJUNCTS recfn_rules)) >> simp[] >> irule recfnCn >>
325      simp[] >> irule primrec_recfn >> simp[primrec_rules]) >>
326  simp[minimise_def, recMin1_def, recCn_def, rec1_def] >> qx_gen_tac ���N��� >>
327  rw[]
328  >- (simp[whileTheory.OLEAST_EQ_SOME] >> SELECT_ELIM_TAC >> conj_tac
329      >- metis_tac[] >>
330      simp[] >> rw[] >- metis_tac[] >>
331      first_x_assum drule >> simp[PULL_EXISTS]) >>
332  fs[] >> rename [���f (A ��� B) = SOME 0���] >>
333  Cases_on ���f (A ��� B) = SOME 0��� >> simp[] >>
334  qspec_then �����n. f (n ��� B) = SOME 0��� mp_tac WOP >> simp[] >> impl_tac
335  >- metis_tac[] >>
336  disch_then (qx_choose_then ���A0��� strip_assume_tac) >>
337  ���A0 ��� A��� by metis_tac[DECIDE �����(x < y) ��� y ��� x���] >>
338  ������i0. i0 < A0 ��� ���m. f (i0 ��� B) = SOME m ��� m = 0��� by metis_tac[] >>
339  metis_tac[DECIDE ���x < y ��� y ��� z ��� x < z���]
340QED
341
342(* basically, expanding def'n of rec1 *)
343Theorem recfn1_recfn_alt:
344  recfn1 f ��� ���g. recfn g 1 ��� ���n. g [n] = f n
345Proof
346  strip_tac >> drule_then strip_assume_tac recfn1_recfn >>
347  qexists_tac ���rec1 f��� >> simp[rec1_def]
348QED
349
350Definition ofoldfs_def:
351  ofoldfs [f] (n:num) = f n ���
352  ofoldfs (f::fs) n = do r1 <- f n ;
353                         rs <- ofoldfs fs n ;
354                         return (r1 ��� rs) ;
355                      od
356End
357
358Theorem ofoldfs_thm[simp]:
359  ofoldfs [f] = f ���
360  ofoldfs (f1::f2::fs) = recpair f1 (ofoldfs (f2::fs))
361Proof
362  simp[FUN_EQ_THM, recpair_def, ofoldfs_def]
363QED
364
365Theorem ofoldfs_EQ_NONE[simp]:
366  fs ��� [] ���
367  (ofoldfs fs n = NONE ��� ���f. MEM f fs ��� f n = NONE)
368Proof
369  Induct_on ���fs��� >> simp[] >> Cases_on ���fs��� >>
370  simp[recpair_def, PULL_EXISTS] >>
371  metis_tac[TypeBase.distinct_of ���:�� option���, TypeBase.nchotomy_of ���:�� option���]
372QED
373
374
375Theorem recfn1_ofoldfs:
376  fs ��� [] ��� (���f. MEM f fs ��� recfn1 f) ��� recfn1 (ofoldfs fs)
377Proof
378  Induct_on ���fs��� >> fs[DISJ_IMP_THM, FORALL_AND_THM] >>
379  qx_gen_tac ���f��� >> Cases_on���fs��� >>
380  fs[DISJ_IMP_THM, FORALL_AND_THM, recfn1_rules]
381QED
382
383Theorem ofoldfs_EQ_SOME:
384  fs ��� [] ���
385  ���l. ofoldfs fs n = SOME l ��� l = fold (MAP (��f. THE (f n)) fs)
386Proof
387  Induct_on ���fs��� >> simp[] >> Cases_on ���fs��� >> fs[] >>
388  simp[recpair_def, PULL_EXISTS]
389QED
390
391Theorem recfn_recfn1:
392  ���f a. recfn f a ��� ���g. recfn1 g ��� ���n. g n = f (unfold a n)
393Proof
394  Induct_on ���recfn��� >> rw[]
395  >- (qexists_tac ���SOME o K 0��� >> simp[recfn1_rules])
396  >- (qexists_tac ���SOME o SUC��� >> simp[recfn1_rules])
397  >- (���primrec (proj i) a��� by simp[primrec_rules] >>
398      drule_then (qx_choose_then ���G��� strip_assume_tac) primrec_primrec1 >>
399      qexists_tac ���SOME o G��� >> simp[] >> simp[primrec1_recfn1])
400  >- (fs[EVERY_MEM, GSYM RIGHT_EXISTS_IMP_THM, PULL_EXISTS, SKOLEM_THM] >>
401      rename [���mk1 _ _ = _ (unfold _ _)���] >>
402      rename [���f1 _ = f (unfold (LENGTH gs) _)���] >>
403      qexists_tac ���recCn1 f1 (ofoldfs (MAP mk1 gs))��� >>
404      ���gs ��� []��� by (strip_tac >> fs[] >> drule recfn_nzero >> simp[]) >>
405      conj_tac
406      >- simp[recfn1_ofoldfs, recfn1_rules, MEM_MAP, PULL_EXISTS] >>
407      ���0 < LENGTH gs��� by (CCONTR_TAC >> fs[]) >>
408      simp[recCn_def, MAP_MAP_o, recCn1_def, EVERY_MEM, MEM_MAP,
409           combinTheory.o_ABS_R] >> qx_gen_tac ���N��� >>
410      Cases_on���ofoldfs (MAP mk1 gs) N��� >> simp[]
411      >- (rfs[MEM_MAP] >> rw[] >> qpat_x_assum ���mk1 _ N = NONE��� mp_tac >>
412          simp[] >> metis_tac[]) >>
413      ������g. NONE ��� g (unfold a N) ��� ��MEM g gs���
414         by (CCONTR_TAC >> fs[] >> rename [���MEM G gs���] >>
415             ���NONE = mk1 G N��� by metis_tac[] >>
416             metis_tac[MEM_MAP, ofoldfs_EQ_NONE, MAP_EQ_NIL,
417                       TypeBase.distinct_of ���:�� option���]) >>
418      simp[] >>
419      ���MAP mk1 gs ��� []��� by simp[] >>
420      drule_all ofoldfs_EQ_SOME >>
421      rw[MAP_MAP_o, combinTheory.o_ABS_L, unfold_fold_alt] >>
422      simp[Cong MAP_CONG'] >> fs[] >> metis_tac[])
423  >- (rename [���b1 _ = b (unfold (a-1) _)���, ���s1 _ = s (unfold (a + 1) _)���] >>
424      ���0 < a-1��� by metis_tac[recfn_nzero] >>
425      qexists_tac ���recPr1 b1 s1��� >> simp[recfn1_rules] >>
426      qx_gen_tac ���N��� >>
427      ������x y. N = x ��� y��� by metis_tac[npair_cases] >> rw[] >>
428      Induct_on ���x��� >> simp[]
429      >- (������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >>
430          simp[unfold_def, Once recPr_def]) >>
431      ������a0. a = SUC a0��� by (Cases_on ���a��� >> fs[]) >> simp[unfold_def] >>
432      simp[SimpRHS, Once recPr_def] >> simp[GSYM ADD1] >>
433      Cases_on���recPr b s (x::unfold a0 y)��� >> simp[])
434  >- (rename [���f1 _ = f (unfold _ _)���] >>
435      qexists_tac ���recMin1 f1��� >> simp[recfn1_rules] >>
436      simp[recMin1_def, minimise_def, GSYM ADD1] >> qx_gen_tac ���N��� >>
437      rw[] >> fs[]
438      >- (simp[whileTheory.OLEAST_EQ_SOME] >> SELECT_ELIM_TAC >>
439          conj_tac >- metis_tac[] >>
440          rw[] >- metis_tac[] >>
441          first_x_assum (drule_then strip_assume_tac) >> simp[]) >>
442      rename [���f (n::unfold a N) = SOME 0���] >>
443      Cases_on ���f (n::unfold a N) = SOME 0��� >> simp[] >>
444      qspec_then �����i. f (i::unfold a N) = SOME 0��� mp_tac WOP >>
445      impl_tac >- metis_tac[] >> simp[] >>
446      disch_then (qx_choose_then ���n0��� strip_assume_tac) >>
447      ���n0 ��� n��� by metis_tac[DECIDE �����(x < y) ��� y ��� x���] >>
448      ������i. i < n0 ��� ���m. f (i :: unfold a N) = SOME m ��� m = 0��� by metis_tac[] >>
449      qexists_tac ���i��� >> simp[] >> metis_tac[])
450QED
451
452Theorem recfn_recfn1_alt:
453  recfn f a ��� ���g. recfn1 g ��� ���l. LENGTH l = a ��� f l = g (fold l)
454Proof
455  metis_tac[unfold_fold, recfn_recfn1]
456QED
457
458val _ = export_theory();
459