|
0
|
1 |
(* Title: ZF/ex/llist-fn.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1993 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Functions for Lazy Lists in Zermelo-Fraenkel Set Theory
|
|
120
|
7 |
|
|
|
8 |
STILL NEEDS:
|
|
|
9 |
co_recursion for defining lconst, flip, etc.
|
|
|
10 |
a typing rule for it, based on some notion of "productivity..."
|
|
0
|
11 |
*)
|
|
|
12 |
|
|
120
|
13 |
LListFn = LList + LList_Eq +
|
|
0
|
14 |
consts
|
|
|
15 |
lconst :: "i => i"
|
|
120
|
16 |
flip :: "i => i"
|
|
0
|
17 |
|
|
|
18 |
rules
|
|
|
19 |
lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
|
|
|
20 |
|
|
120
|
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 |
|
|
0
|
26 |
end
|