src/ZF/List.thy

bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.

(*  Title:      ZF/List
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1994  University of Cambridge

Lists in Zermelo-Fraenkel Set Theory 

map is a binding operator -- it applies to meta-level functions, not 
object-level functions.  This simplifies the final form of term_rec_conv,
although complicating its derivation.
*)

List = Datatype + ArithSimp +

consts
  list       :: "i=>i"
  
datatype
  "list(A)" = Nil | Cons ("a:A", "l: list(A)")


syntax
 "[]"        :: i                                       ("[]")
 "@List"     :: "is => i"                                 ("[(_)]")

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


consts
  length :: "i=>i"
  hd      :: "i=>i"
  tl      :: "i=>i"

primrec
  "length([]) = 0"
  "length(Cons(a,l)) = succ(length(l))"
  
primrec
  "hd(Cons(a,l)) = a"

primrec
  "tl([]) = []"
  "tl(Cons(a,l)) = l"


consts
  map        :: "[i=>i, i] => i"
  set_of_list :: "i=>i"
  "@"        :: "[i,i]=>i"                        (infixr 60)
  
primrec
  "map(f,[]) = []"
  "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
 
primrec
  "set_of_list([]) = 0"
  "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
   
primrec
  "[] @ ys = ys"
  "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
  

consts
  rev :: "i=>i"
  flat       :: "i=>i"
  list_add   :: "i=>i"

primrec
  "rev([]) = []"
  "rev(Cons(a,l)) = rev(l) @ [a]"

primrec
  "flat([]) = []"
  "flat(Cons(l,ls)) = l @ flat(ls)"
   
primrec
  "list_add([]) = 0"
  "list_add(Cons(a,l)) = a #+ list_add(l)"
       
consts
  drop       :: "[i,i]=>i"

primrec
  drop_0    "drop(0,l) = l"
  drop_SUCC "drop(succ(i), l) = tl (drop(i,l))"


(*** Thanks to Sidi Ehmety for the following ***)

constdefs
(* Function `take' returns the first n elements of a list *)
  take     :: "[i,i]=>i"
  "take(n, as) == list_rec(lam n:nat. [],
		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
  
(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
  nth :: "[i, i]=>i"
  "nth(n, as) == list_rec(lam n:nat. 0,
		%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"

  list_update :: "[i, i, i]=>i"
  "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
      %u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"

consts
  filter :: "[i=>o, i] => i"
  zip :: "[i, i]=>i"
  ziprel :: "[i,i]=>i"
  upt :: "[i, i] =>i"
  
inductive domains "ziprel(A, B)" <= "list(A)*list(B)*list(A*B)"
intrs   
  ziprel_Nil1  "ys:list(B) ==><Nil, ys, Nil>:ziprel(A, B)"
  ziprel_Nil2  "xs:list(A) ==><xs, Nil, Nil>:ziprel(A, B)"
  ziprel_Cons "[| <xs, ys, zs>:ziprel(A, B); x:A; y:B |]==>
	         <Cons(x, xs), Cons(y, ys), Cons(<x, y>, zs)>:ziprel(A,B)"
  type_intrs  "list.intrs"
  
defs
  zip_def "zip(xs, ys) ==
	      THE zs. <xs, ys, zs>:ziprel(set_of_list(xs),set_of_list(ys))"

primrec
  "filter(P, Nil) = Nil"
  "filter(P, Cons(x, xs)) =
     (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"

primrec
  "upt(i, 0) = Nil"
  "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"

constdefs
  sublist :: "[i, i] => i"
    "sublist(xs, A)== 
     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"

  min :: "[i,i] =>i"
    "min(x, y) == (if x le y then x else y)"
  
  max :: "[i, i] =>i"
    "max(x, y) == (if x le y then y else x)"

end