src/ZF/List.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 1806 12708740f58d
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/List
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Lists in Zermelo-Fraenkel Set Theory 
     7 
     8 map is a binding operator -- it applies to meta-level functions, not 
     9 object-level functions.  This simplifies the final form of term_rec_conv,
    10 although complicating its derivation.
    11 *)
    12 
    13 List = Datatype + 
    14 
    15 consts
    16   "@"        :: [i,i]=>i                        (infixr 60)
    17   list_rec   :: [i, i, [i,i,i]=>i] => i
    18   map        :: [i=>i, i] => i
    19   length,rev :: i=>i
    20   flat       :: i=>i
    21   list_add   :: i=>i
    22   hd,tl      :: i=>i
    23   drop       :: [i,i]=>i
    24 
    25  (* List Enumeration *)
    26  "[]"        :: i                                       ("[]")
    27  "@List"     :: is => i                                 ("[(_)]")
    28 
    29   list       :: i=>i
    30 
    31   
    32 datatype
    33   "list(A)" = Nil | Cons ("a:A", "l: list(A)")
    34 
    35 
    36 translations
    37   "[x, xs]"     == "Cons(x, [xs])"
    38   "[x]"         == "Cons(x, [])"
    39   "[]"          == "Nil"
    40 
    41 
    42 defs
    43 
    44   hd_def        "hd(l)       == list_case(0, %x xs.x, l)"
    45   tl_def        "tl(l)       == list_case(Nil, %x xs.xs, l)"
    46   drop_def      "drop(i,l)   == rec(i, l, %j r. tl(r))"
    47 
    48   list_rec_def
    49       "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
    50 
    51   map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
    52   length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
    53   app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
    54   rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
    55   flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
    56   list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
    57 end