examples/computability/unary_recfnsScript.sml

86   unfold 0 m = [] ���
87   unfold (SUC n) m = if n = 0 then [m]
88                      else nfst m :: unfold n (nsnd m)
92   unfold 1 n = [n]
98   ���m n. LENGTH (unfold m n) = m
104   unfold a n = [] ��� a = 0
116   ���a n. 0 < a ��� fold (unfold a n) = n
119   Cases_on ���unfold a (nsnd n)��� >> fs[] >>
124   ���l. unfold (LENGTH l) (fold l) = l
130   n = LENGTH l ��� unfold n (fold l) = l
163   ���a fs n. 0 < a ��� LENGTH fs = a ��� unfold a (foldfs fs n) = MAP (��f. f n) fs
173   ���f a. primrec f a ��� ���g. primrec1 g ��� ���n. g n = f (unfold a n)
178   >- (rename [���proj i (unfold a _)���] >>
194       rename [���f1 _ = f (unfold (LENGTH gs) _)���] >>
202   rename [���b1 _ = b (unfold a _)���, ���s1 _ = s (unfold (a + 2) _)���] >>
392   ���f a. recfn f a ��� ���g. recfn1 g ��� ���n. g n = f (unfold a n)
401       rename [���mk1 _ _ = _ (unfold _ _)���] >>
402       rename [���f1 _ = f (unfold (LENGTH gs) _)���] >>
413       ������g. NONE ��� g (unfold a N) ��� ��MEM g gs���
423   >- (rename [���b1 _ = b (unfold (a-1) _)���, ���s1 _ = s (unfold (a + 1) _)���] >>
433       Cases_on���recPr b s (x::unfold a0 y)��� >> simp[])
434   >- (rename [���f1 _ = f (unfold _ _)���] >>
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 >>
448       ������i. i < n0 ��� ���m. f (i :: unfold a N) = SOME m ��� m = 0��� by metis_tac[] >>