Lines Matching refs:unfold
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[] >>