src/CCL/ex/List.thy

Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML

(*  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 + 

consts
  map       :: "[i=>i,i]=>i"
  "o"       :: "[i=>i,i=>i]=>i=>i"             (infixr 55)
  "@"       :: "[i,i]=>i"             (infixr 55)
  mem       :: "[i,i]=>i"             (infixr 55)
  filter    :: "[i,i]=>i"
  flat      :: "i=>i"
  partition :: "[i,i]=>i"
  insert    :: "[i,i,i]=>i"
  isort     :: "i=>i"
  qsort     :: "i=>i"

rules 

  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))"

  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)) 
                    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))) 
                          in qsortx(l)"

end