src/ZF/List.thy
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1478 2b8c2a7547ab
child 1806 12708740f58d
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/List
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     2
    ID:         $Id$
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     4
    Copyright   1994  University of Cambridge
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     5
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     6
Lists in Zermelo-Fraenkel Set Theory 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     7
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     8
map is a binding operator -- it applies to meta-level functions, not 
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
     9
object-level functions.  This simplifies the final form of term_rec_conv,
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    10
although complicating its derivation.
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    11
*)
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    12
810
91c68f74f458 removed quotes around "Datatype",
lcp
parents: 753
diff changeset
    13
List = Datatype + 
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    14
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    15
consts
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    16
  "@"        :: [i,i]=>i                        (infixr 60)
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    17
  list_rec   :: [i, i, [i,i,i]=>i] => i
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    18
  map        :: [i=>i, i] => i
1401
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    19
  length,rev :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    20
  flat       :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    21
  list_add   :: i=>i
0c439768f45c removed quotes from consts and syntax sections
clasohm
parents: 810
diff changeset
    22
  hd,tl      :: i=>i
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    23
  drop       :: [i,i]=>i
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    24
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    25
 (* List Enumeration *)
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    26
 "[]"        :: i                                       ("[]")
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    27
 "@List"     :: is => i                                 ("[(_)]")
124
858ab9a9b047 made pseudo theories for all ML files;
clasohm
parents:
diff changeset
    28
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    29
  list       :: i=>i
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    30
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    31
  
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    32
datatype
581
465075fd257b removal of needless quotes
lcp
parents: 516
diff changeset
    33
  "list(A)" = Nil | Cons ("a:A", "l: list(A)")
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    34
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    35
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    36
translations
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    37
  "[x, xs]"     == "Cons(x, [xs])"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    38
  "[x]"         == "Cons(x, [])"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    39
  "[]"          == "Nil"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    40
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    41
753
ec86863e87c8 replaced "rules" by "defs"
lcp
parents: 581
diff changeset
    42
defs
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    43
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    44
  hd_def        "hd(l)       == list_case(0, %x xs.x, l)"
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    45
  tl_def        "tl(l)       == list_case(Nil, %x xs.xs, l)"
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    46
  drop_def      "drop(i,l)   == rec(i, l, %j r. tl(r))"
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    47
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    48
  list_rec_def
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    49
      "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    50
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    51
  map_def       "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    52
  length_def    "length(l)   == list_rec(l,  0,  %x xs r. succ(r))"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    53
  app_def       "xs@ys       == list_rec(xs, ys, %x xs r. Cons(x,r))"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    54
  rev_def       "rev(l)      == list_rec(l,  Nil,  %x xs r. r @ [x])"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    55
  flat_def      "flat(ls)    == list_rec(ls, Nil,  %l ls r. l @ r)"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    56
  list_add_def  "list_add(l) == list_rec(l, 0,  %x xs r. x#+r)"
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 435
diff changeset
    57
end