src/ZF/ListFn.thy
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 15 6c6d2f6e3185
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/list-fn
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Functions for Lists in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
map is a binding operator -- it applies to meta-level functions, not 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
object-level functions.  This simplifies the final form of term_rec_conv,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
although complicating its derivation.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
ListFn = List +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  "@"	     :: "[i,i]=>i"      			(infixr 60)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  list_rec   :: "[i, i, [i,i,i]=>i] => i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  map 	     :: "[i=>i, i] => i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  length,rev :: "i=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  flat       :: "i=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  list_add   :: "i=>i"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
 (* List Enumeration *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
 "[]"        :: "i" 	                           	("[]")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
 "@List"     :: "args => i" 	                   	("[(_)]")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
translations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  "[x, xs]"     == "Cons(x, [xs])"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  "[x]"         == "Cons(x, [])"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  "[]"          == "Nil"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  list_rec_def
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
      "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
  map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
  length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
  flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
end