73 \ List_case(Rep_LList(l), c, %x y. d(Inv(Leaf,x), Abs_LList(y)))" |
73 \ List_case(Rep_LList(l), c, %x y. d(Inv(Leaf,x), Abs_LList(y)))" |
74 |
74 |
75 LList_corec_fun_def |
75 LList_corec_fun_def |
76 "LList_corec_fun(k,f) == \ |
76 "LList_corec_fun(k,f) == \ |
77 \ nat_rec(k, %x. {}, \ |
77 \ nat_rec(k, %x. {}, \ |
78 \ %j r x. case(f(x), %u.NIL, \ |
78 \ %j r x. sum_case(f(x), %u.NIL, \ |
79 \ %v. split(v, %z w. CONS(z, r(w)))))" |
79 \ %v. split(v, %z w. CONS(z, r(w)))))" |
80 |
80 |
81 LList_corec_def |
81 LList_corec_def |
82 "LList_corec(a,f) == UN k. LList_corec_fun(k,f,a)" |
82 "LList_corec(a,f) == UN k. LList_corec_fun(k,f,a)" |
83 |
83 |
84 llist_corec_def |
84 llist_corec_def |
85 "llist_corec(a,f) == \ |
85 "llist_corec(a,f) == \ |
86 \ Abs_LList(LList_corec(a, %z.case(f(z), %x.Inl(x), \ |
86 \ Abs_LList(LList_corec(a, %z.sum_case(f(z), %x.Inl(x), \ |
87 \ %y.split(y, %v w. Inr(<Leaf(v), w>)))))" |
87 \ %y.split(y, %v w. Inr(<Leaf(v), w>)))))" |
88 |
88 |
89 llistD_Fun_def |
89 llistD_Fun_def |
90 "llistD_Fun(r) == \ |
90 "llistD_Fun(r) == \ |
91 \ prod_fun(Abs_LList,Abs_LList) `` \ |
91 \ prod_fun(Abs_LList,Abs_LList) `` \ |