src/ZF/List.thy
 author paulson Mon, 17 Jun 1996 16:50:08 +0200 changeset 1806 12708740f58d parent 1478 2b8c2a7547ab child 1926 1957ae3f9301 permissions -rw-r--r--
Converted to use constdefs instead of defs
```
(*  Title:      ZF/List
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Lists in Zermelo-Fraenkel Set Theory

map is a binding operator -- it applies to meta-level functions, not
object-level functions.  This simplifies the final form of term_rec_conv,
although complicating its derivation.
*)

List = Datatype +

consts
(* List Enumeration *)
"[]"        :: i                                       ("[]")
"@List"     :: is => i                                 ("[(_)]")

list       :: i=>i

datatype
"list(A)" = Nil | Cons ("a:A", "l: list(A)")

translations
"[x, xs]"     == "Cons(x, [xs])"
"[x]"         == "Cons(x, [])"
"[]"          == "Nil"

constdefs
hd      :: i=>i
"hd(l)       == list_case(0, %x xs.x, l)"

tl      :: i=>i
"tl(l)       == list_case(Nil, %x xs.xs, l)"

drop       :: [i,i]=>i
"drop(i,l)   == rec(i, l, %j r. tl(r))"

list_rec   :: [i, i, [i,i,i]=>i] => i
"list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"

map        :: [i=>i, i] => i
"map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"

length :: i=>i
"length(l)   == list_rec(l,  0,  %x xs r. succ(r))"

consts  (*Cannot use constdefs because @ is not an identifier*)
"@"        :: [i,i]=>i                        (infixr 60)
defs
app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"

constdefs
rev :: i=>i
"rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"

flat       :: i=>i
"flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"