1 (* Title: CCL/ex/list.thy |
|
2 ID: $Id$ |
|
3 Author: Martin Coen, Cambridge University Computer Laboratory |
|
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 |
|
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)" |
|
31 |
|
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))" |
|
34 |
|
35 partition_def |
|
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) \ |
|
41 \ in split(p,%x y.qsortx(x) @ h$qsortx(y))) \ |
|
42 \ in qsortx(l)" |
|
43 |
|
44 end |
|