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