1474
|
1 |
(* Title: CCL/ex/list.thy
|
0
|
2 |
ID: $Id$
|
1474
|
3 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
0
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
|
6 |
Programs defined over lists.
|
|
7 |
*)
|
|
8 |
|
|
9 |
List = Nat +
|
|
10 |
|
|
11 |
consts
|
|
12 |
map :: "[i=>i,i]=>i"
|
|
13 |
"o" :: "[i=>i,i=>i]=>i=>i" (infixr 55)
|
|
14 |
"@" :: "[i,i]=>i" (infixr 55)
|
|
15 |
mem :: "[i,i]=>i" (infixr 55)
|
|
16 |
filter :: "[i,i]=>i"
|
|
17 |
flat :: "i=>i"
|
|
18 |
partition :: "[i,i]=>i"
|
|
19 |
insert :: "[i,i,i]=>i"
|
|
20 |
isort :: "i=>i"
|
|
21 |
qsort :: "i=>i"
|
|
22 |
|
|
23 |
rules
|
|
24 |
|
3837
|
25 |
map_def "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
|
|
26 |
comp_def "f o g == (%x. f(g(x)))"
|
|
27 |
append_def "l @ m == lrec(l,m,%x xs g. x$g)"
|
|
28 |
mem_def "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
|
|
29 |
filter_def "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
|
|
30 |
flat_def "flat(l) == lrec(l,[],%h t g. h @ g)"
|
0
|
31 |
|
3837
|
32 |
insert_def "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
|
|
33 |
isort_def "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
|
0
|
34 |
|
|
35 |
partition_def
|
1149
|
36 |
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
|
|
37 |
if f`x then part(xs,x$a,b) else part(xs,a,x$b))
|
|
38 |
in part(l,[],[])"
|
|
39 |
qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
|
|
40 |
let p be partition(f`h,t)
|
3837
|
41 |
in split(p,%x y. qsortx(x) @ h$qsortx(y)))
|
1149
|
42 |
in qsortx(l)"
|
0
|
43 |
|
|
44 |
end
|