equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory |
6 Functions for Lazy Lists in Zermelo-Fraenkel Set Theory |
|
7 |
|
8 STILL NEEDS: |
|
9 co_recursion for defining lconst, flip, etc. |
|
10 a typing rule for it, based on some notion of "productivity..." |
7 *) |
11 *) |
8 |
12 |
9 LListFn = LList + |
13 LListFn = LList + LList_Eq + |
10 consts |
14 consts |
11 lconst :: "i => i" |
15 lconst :: "i => i" |
|
16 flip :: "i => i" |
12 |
17 |
13 rules |
18 rules |
14 lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
19 lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))" |
15 |
20 |
|
21 flip_LNil "flip(LNil) = LNil" |
|
22 |
|
23 flip_LCons "[| x:bool; l: llist(bool) |] ==> \ |
|
24 \ flip(LCons(x,l)) = LCons(not(x), flip(l))" |
|
25 |
16 end |
26 end |