src/ZF/ListFn.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/list-fn
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Functions for 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 ListFn = List +
    14 consts
    15   "@"	     :: "[i,i]=>i"      			(infixr 60)
    16   list_rec   :: "[i, i, [i,i,i]=>i] => i"
    17   map 	     :: "[i=>i, i] => i"
    18   length,rev :: "i=>i"
    19   flat       :: "i=>i"
    20   list_add   :: "i=>i"
    21 
    22  (* List Enumeration *)
    23  "[]"        :: "i" 	                           	("[]")
    24  "@List"     :: "args => i" 	                   	("[(_)]")
    25 
    26 
    27 translations
    28   "[x, xs]"     == "Cons(x, [xs])"
    29   "[x]"         == "Cons(x, [])"
    30   "[]"          == "Nil"
    31 
    32 
    33 rules
    34   list_rec_def
    35       "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
    36 
    37   map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
    38   length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
    39   app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
    40   rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
    41   flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
    42   list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
    43 
    44 end