--- a/src/CCL/ex/List.thy Sat Sep 17 14:02:31 2005 +0200
+++ b/src/CCL/ex/List.thy Sat Sep 17 17:35:26 2005 +0200
@@ -1,12 +1,14 @@
-(* Title: CCL/ex/list.thy
+(* Title: CCL/ex/List.thy
ID: $Id$
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
-Programs defined over lists.
*)
-List = Nat +
+header {* Programs defined over lists *}
+
+theory List
+imports Nat
+begin
consts
map :: "[i=>i,i]=>i"
@@ -20,25 +22,27 @@
isort :: "i=>i"
qsort :: "i=>i"
-rules
+axioms
- map_def "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
- comp_def "f o g == (%x. f(g(x)))"
- append_def "l @ m == lrec(l,m,%x xs g. x$g)"
- mem_def "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
- filter_def "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
- flat_def "flat(l) == lrec(l,[],%h t g. h @ g)"
+ map_def: "map(f,l) == lrec(l,[],%x xs g. f(x)$g)"
+ comp_def: "f o g == (%x. f(g(x)))"
+ append_def: "l @ m == lrec(l,m,%x xs g. x$g)"
+ mem_def: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+ filter_def: "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
+ flat_def: "flat(l) == lrec(l,[],%h t g. h @ g)"
- insert_def "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
- isort_def "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
+ insert_def: "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+ isort_def: "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
- partition_def
+ partition_def:
"partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
- if f`x then part(xs,x$a,b) else part(xs,a,x$b))
+ if f`x then part(xs,x$a,b) else part(xs,a,x$b))
in part(l,[],[])"
- qsort_def "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
- let p be partition(f`h,t)
- in split(p,%x y. qsortx(x) @ h$qsortx(y)))
+ qsort_def: "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t.
+ let p be partition(f`h,t)
+ in split(p,%x y. qsortx(x) @ h$qsortx(y)))
in qsortx(l)"
+ML {* use_legacy_bindings (the_context ()) *}
+
end