src/CCL/ex/list.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 290 37d580c16af5
permissions -rw-r--r--
tidying
     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