src/CCL/ex/List.thy
changeset 0 a5a9c433f639
child 290 37d580c16af5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/ex/List.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title: 	CCL/ex/list.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Programs defined over lists.
    1.10 +*)
    1.11 +
    1.12 +List = Nat + 
    1.13 +
    1.14 +consts
    1.15 +  map       :: "[i=>i,i]=>i"
    1.16 +  "o"       :: "[i=>i,i=>i]=>i=>i"             (infixr 55)
    1.17 +  "@"       :: "[i,i]=>i"             (infixr 55)
    1.18 +  mem       :: "[i,i]=>i"             (infixr 55)
    1.19 +  filter    :: "[i,i]=>i"
    1.20 +  flat      :: "i=>i"
    1.21 +  partition :: "[i,i]=>i"
    1.22 +  insert    :: "[i,i,i]=>i"
    1.23 +  isort     :: "i=>i"
    1.24 +  qsort     :: "i=>i"
    1.25 +
    1.26 +rules 
    1.27 +
    1.28 +  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x).g)"
    1.29 +  comp_def    "f o g == (%x.f(g(x)))"
    1.30 +  append_def  "l @ m == lrec(l,m,%x xs g.x.g)"
    1.31 +  mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
    1.32 +  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x.g else g)"
    1.33 +  flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
    1.34 +
    1.35 +  insert_def  "insert(f,a,l) == lrec(l,a.[],%h t g.if f`a`h then a.h.t else h.g)"
    1.36 +  isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
    1.37 +
    1.38 +  partition_def 
    1.39 +  "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.\
    1.40 +\                            if f`x then part(xs,x.a,b) else part(xs,a,x.b)) \
    1.41 +\                    in part(l,[],[])"
    1.42 +  qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. \
    1.43 +\                                   let p be partition(f`h,t) \
    1.44 +\                                   in split(p,%x y.qsortx(x) @ h.qsortx(y))) \
    1.45 +\                          in qsortx(l)"
    1.46 +
    1.47 +end