|
515
|
1 |
(* Title: ZF/ex/LList.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1994 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Codatatype definition of Lazy Lists
|
|
|
7 |
|
|
|
8 |
Equality for llist(A) as a greatest fixed point
|
|
|
9 |
|
|
|
10 |
Functions for Lazy Lists
|
|
|
11 |
|
|
|
12 |
STILL NEEDS:
|
|
|
13 |
co_recursion for defining lconst, flip, etc.
|
|
|
14 |
a typing rule for it, based on some notion of "productivity..."
|
|
|
15 |
*)
|
|
|
16 |
|
|
810
|
17 |
LList = Datatype +
|
|
515
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
llist :: "i=>i"
|
|
|
21 |
|
|
|
22 |
codatatype
|
|
|
23 |
"llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
|
|
|
24 |
|
|
|
25 |
|
|
|
26 |
(*Coinductive definition of equality*)
|
|
|
27 |
consts
|
|
|
28 |
lleq :: "i=>i"
|
|
|
29 |
|
|
|
30 |
(*Previously used <*> in the domain and variant pairs as elements. But
|
|
|
31 |
standard pairs work just as well. To use variant pairs, must change prefix
|
|
|
32 |
a q/Q to the Sigma, Pair and converse rules.*)
|
|
|
33 |
coinductive
|
|
|
34 |
domains "lleq(A)" <= "llist(A) * llist(A)"
|
|
|
35 |
intrs
|
|
|
36 |
LNil "<LNil, LNil> : lleq(A)"
|
|
|
37 |
LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
|
|
|
38 |
type_intrs "llist.intrs"
|
|
|
39 |
|
|
|
40 |
|
|
|
41 |
(*Lazy list functions; flip is not definitional!*)
|
|
|
42 |
consts
|
|
|
43 |
lconst :: "i => i"
|
|
|
44 |
flip :: "i => i"
|
|
|
45 |
|
|
753
|
46 |
defs
|
|
515
|
47 |
lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
|
|
|
48 |
|
|
753
|
49 |
rules
|
|
515
|
50 |
flip_LNil "flip(LNil) = LNil"
|
|
|
51 |
|
|
|
52 |
flip_LCons "[| x:bool; l: llist(bool) |] ==> \
|
|
|
53 |
\ flip(LCons(x,l)) = LCons(not(x), flip(l))"
|
|
|
54 |
|
|
|
55 |
end
|
|
|
56 |
|