List.thy

Initial revision

(*  Title:      HOL/list
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Definition of type 'a list by a least fixed point

We use          List(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
and not         List    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
so that List can serve as a "functor" for defining other recursive types
*)

List = Sexp +

types
  list 1

arities
  list :: (term) term


consts

  List_Fun      :: "['a node set set, 'a node set set] => 'a node set set"
  List          :: "'a node set set => 'a node set set"
  Rep_List      :: "'a list => 'a node set"
  Abs_List      :: "'a node set => 'a list"
  NIL           :: "'a node set"
  CONS          :: "['a node set, 'a node set] => 'a node set"
  Nil           :: "'a list"
  Cons          :: "['a, 'a list] => 'a list"
  List_case     :: "['a node set, 'b, ['a node set, 'a node set]=>'b] => 'b"
  List_rec      :: "['a node set, 'b, ['a node set, 'a node set, 'b]=>'b] => 'b"
  list_rec      :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
  Rep_map       :: "('b => 'a node set) => ('b list => 'a node set)"
  Abs_map       :: "('a node set => 'b) => 'a node set => 'b list"
  null          :: "'a list => bool"
  hd            :: "'a list => 'a"
  tl            :: "'a list => 'a list"
  list_all      :: "('a => bool) => ('a list => bool)"
  map           :: "('a=>'b) => ('a list => 'b list)"
  list_case     :: "['a list, 'b, ['a, 'a list]=>'b] => 'b"

  (* List Enumeration *)

  "[]"          :: "'a list"                            ("[]")
  "@List"       :: "args => 'a list"                    ("[(_)]")


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


rules

  List_Fun_def  "List_Fun(A) == (%Z. {Numb(0)} <+> A <*> Z)"
  List_def      "List(A) == lfp(List_Fun(A))"

  (* Faking a Type Definition ... *)

  Rep_List          "Rep_List(xs): List(range(Leaf))"
  Rep_List_inverse  "Abs_List(Rep_List(xs)) = xs"
  Abs_List_inverse  "M: List(range(Leaf)) ==> Rep_List(Abs_List(M)) = M"

  (* Defining the Concrete Constructors *)

  NIL_def       "NIL == In0(Numb(0))"
  CONS_def      "CONS(M, N) == In1(M . N)"

  (* Defining the Abstract Constructors *)

  Nil_def       "Nil == Abs_List(NIL)"
  Cons_def      "Cons(x, xs) == Abs_List(CONS(Leaf(x), Rep_List(xs)))"

  List_case_def "List_case(M, c, d) == Case(M, %x.c, %u. Split(u, %x y.d(x, y)))"

  (* List Recursion -- the trancl is Essential; see list.ML *)

  List_rec_def
   "List_rec(M, c, d) == wfrec(trancl(pred_Sexp), M, \
\                         %z g. List_case(z, c, %x y. d(x, y, g(y))))"

  list_rec_def
   "list_rec(l, c, d) == \
\   List_rec(Rep_List(l), c, %x y r. d(Inv(Leaf, x), Abs_List(y), r))"

  (* Generalized Map Functionals *)

  Rep_map_def
   "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))"
  Abs_map_def
   "Abs_map(g, M) == List_rec(M, Nil, %N L r. Cons(g(N), r))"

  null_def      "null(xs)            == list_rec(xs, True, %x xs r.False)"
  hd_def        "hd(xs)              == list_rec(xs, @x.True, %x xs r.x)"
  tl_def        "tl(xs)              == list_rec(xs, @xs.True, %x xs r.xs)"
  list_all_def  "list_all(P, xs)     == list_rec(xs, True, %x l r. P(x) & r)"
  map_def       "map(f, xs)          == list_rec(xs, Nil, %x l r. Cons(f(x), r))"
  list_case_def "list_case(xs, a, f) == list_rec(xs, a, %x xs r.f(x, xs))"

end