148
|
1 |
(* Title: HOL/LList.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1994 University of Cambridge
|
|
5 |
|
|
6 |
Definition of type 'a llist by a greatest fixed point
|
|
7 |
|
|
8 |
Shares NIL, CONS, List_case with List.thy
|
|
9 |
|
|
10 |
Still needs filter and flatten functions -- hard because they need
|
|
11 |
bounds on the amount of lookahead required.
|
|
12 |
|
|
13 |
Could try (but would it work for the gfp analogue of term?)
|
|
14 |
LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
|
|
15 |
|
|
16 |
A nice but complex example would be [ML for the Working Programmer, page 176]
|
|
17 |
from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
|
|
18 |
|
|
19 |
Previous definition of llistD_Fun was explicit:
|
|
20 |
llistD_Fun_def
|
|
21 |
"llistD_Fun(r) == \
|
|
22 |
\ {<LNil,LNil>} Un \
|
|
23 |
\ (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,l2)>))``r)"
|
|
24 |
*)
|
|
25 |
|
195
|
26 |
LList = Gfp + SList +
|
148
|
27 |
|
|
28 |
types
|
|
29 |
'a llist
|
|
30 |
|
|
31 |
arities
|
|
32 |
llist :: (term)term
|
|
33 |
|
|
34 |
consts
|
|
35 |
list_Fun :: "['a item set, 'a item set] => 'a item set"
|
|
36 |
LListD_Fun ::
|
|
37 |
"[('a item * 'a item)set, ('a item * 'a item)set] => \
|
|
38 |
\ ('a item * 'a item)set"
|
|
39 |
|
|
40 |
llist :: "'a item set => 'a item set"
|
|
41 |
LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
|
|
42 |
llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
|
|
43 |
|
|
44 |
Rep_llist :: "'a llist => 'a item"
|
|
45 |
Abs_llist :: "'a item => 'a llist"
|
|
46 |
LNil :: "'a llist"
|
|
47 |
LCons :: "['a, 'a llist] => 'a llist"
|
|
48 |
|
|
49 |
llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
|
|
50 |
|
|
51 |
LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
|
|
52 |
LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
|
|
53 |
llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
|
|
54 |
|
|
55 |
Lmap :: "('a item => 'b item) => ('a item => 'b item)"
|
|
56 |
lmap :: "('a=>'b) => ('a llist => 'b llist)"
|
|
57 |
|
|
58 |
iterates :: "['a => 'a, 'a] => 'a llist"
|
|
59 |
|
|
60 |
Lconst :: "'a item => 'a item"
|
|
61 |
Lappend :: "['a item, 'a item] => 'a item"
|
|
62 |
lappend :: "['a llist, 'a llist] => 'a llist"
|
|
63 |
|
|
64 |
|
|
65 |
coinductive "llist(A)"
|
|
66 |
intrs
|
|
67 |
NIL_I "NIL: llist(A)"
|
|
68 |
CONS_I "[| a: A; M: llist(A) |] ==> CONS(a,M) : llist(A)"
|
|
69 |
|
|
70 |
coinductive "LListD(r)"
|
|
71 |
intrs
|
|
72 |
NIL_I "<NIL, NIL> : LListD(r)"
|
|
73 |
CONS_I "[| <a,b>: r; <M,N> : LListD(r) \
|
|
74 |
\ |] ==> <CONS(a,M), CONS(b,N)> : LListD(r)"
|
|
75 |
|
|
76 |
defs
|
|
77 |
(*Now used exclusively for abbreviating the coinduction rule*)
|
|
78 |
list_Fun_def "list_Fun(A,X) == \
|
|
79 |
\ {z. z = NIL | (? M a. z = CONS(a, M) & a : A & M : X)}"
|
|
80 |
|
|
81 |
LListD_Fun_def "LListD_Fun(r,X) == \
|
|
82 |
\ {z. z = <NIL, NIL> | \
|
|
83 |
\ (? M N a b. z = <CONS(a, M), CONS(b, N)> & \
|
|
84 |
\ <a, b> : r & <M, N> : X)}"
|
|
85 |
|
|
86 |
(*defining the abstract constructors*)
|
|
87 |
LNil_def "LNil == Abs_llist(NIL)"
|
|
88 |
LCons_def "LCons(x,xs) == Abs_llist(CONS(Leaf(x), Rep_llist(xs)))"
|
|
89 |
|
|
90 |
llist_case_def
|
|
91 |
"llist_case(c,d,l) == \
|
|
92 |
\ List_case(c, %x y. d(Inv(Leaf,x), Abs_llist(y)), Rep_llist(l))"
|
|
93 |
|
|
94 |
LList_corec_fun_def
|
|
95 |
"LList_corec_fun(k,f) == \
|
|
96 |
\ nat_rec(k, %x. {}, \
|
|
97 |
\ %j r x. sum_case(%u.NIL, split(%z w. CONS(z, r(w))), f(x)))"
|
|
98 |
|
|
99 |
LList_corec_def
|
|
100 |
"LList_corec(a,f) == UN k. LList_corec_fun(k,f,a)"
|
|
101 |
|
|
102 |
llist_corec_def
|
|
103 |
"llist_corec(a,f) == \
|
|
104 |
\ Abs_llist(LList_corec(a, %z.sum_case(%x.Inl(x), \
|
|
105 |
\ split(%v w. Inr(<Leaf(v), w>)), f(z))))"
|
|
106 |
|
|
107 |
llistD_Fun_def
|
|
108 |
"llistD_Fun(r) == \
|
|
109 |
\ prod_fun(Abs_llist,Abs_llist) `` \
|
|
110 |
\ LListD_Fun(diag(range(Leaf)), \
|
|
111 |
\ prod_fun(Rep_llist,Rep_llist) `` r)"
|
|
112 |
|
|
113 |
Lconst_def "Lconst(M) == lfp(%N. CONS(M, N))"
|
|
114 |
|
|
115 |
Lmap_def
|
|
116 |
"Lmap(f,M) == LList_corec(M, List_case(Inl(Unity), %x M'. Inr(<f(x), M'>)))"
|
|
117 |
|
|
118 |
lmap_def
|
|
119 |
"lmap(f,l) == llist_corec(l, llist_case(Inl(Unity), %y z. Inr(<f(y), z>)))"
|
|
120 |
|
|
121 |
iterates_def "iterates(f,a) == llist_corec(a, %x. Inr(<x, f(x)>))"
|
|
122 |
|
|
123 |
(*Append generates its result by applying f, where
|
|
124 |
f(<NIL,NIL>) = Inl(Unity)
|
|
125 |
f(<NIL, CONS(N1,N2)>) = Inr(<N1, <NIL,N2>)
|
|
126 |
f(<CONS(M1,M2), N>) = Inr(<M1, <M2,N>)
|
|
127 |
*)
|
|
128 |
|
|
129 |
Lappend_def
|
|
130 |
"Lappend(M,N) == LList_corec(<M,N>, \
|
|
131 |
\ split(List_case(List_case(Inl(Unity), %N1 N2. Inr(<N1, <NIL,N2>>)), \
|
|
132 |
\ %M1 M2 N. Inr(<M1, <M2,N>>))))"
|
|
133 |
|
|
134 |
lappend_def
|
|
135 |
"lappend(l,n) == llist_corec(<l,n>, \
|
|
136 |
\ split(llist_case(llist_case(Inl(Unity), %n1 n2. Inr(<n1, <LNil,n2>>)), \
|
|
137 |
\ %l1 l2 n. Inr(<l1, <l2,n>>))))"
|
|
138 |
|
|
139 |
rules
|
|
140 |
(*faking a type definition...*)
|
|
141 |
Rep_llist "Rep_llist(xs): llist(range(Leaf))"
|
|
142 |
Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
|
|
143 |
Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
|
|
144 |
|
|
145 |
end
|