--- a/List.thy Fri Dec 02 16:09:49 1994 +0100
+++ b/List.thy Fri Dec 02 16:13:34 1994 +0100
@@ -1,52 +1,32 @@
-(* Title: HOL/list
+(* Title: HOL/List.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
-Definition of type 'a list by a least fixed point
+Definition of type 'a list as a datatype. This allows primrec to work.
-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 +
+List = Arith +
-types
- 'a list
-
-arities
- list :: (term) term
-
+datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65)
consts
- list :: "'a item set => 'a item set"
- Rep_list :: "'a list => 'a item"
- Abs_list :: "'a item => 'a list"
- NIL :: "'a item"
- CONS :: "['a item, 'a item] => 'a item"
- Nil :: "'a list"
- "#" :: "['a, 'a list] => 'a list" (infixr 65)
- List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
- List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
- list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
- list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
- Rep_map :: "('b => 'a item) => ('b list => 'a item)"
- Abs_map :: "('a item => 'b) => 'a item => 'b list"
null :: "'a list => bool"
hd :: "'a list => 'a"
tl,ttl :: "'a list => 'a list"
- mem :: "['a, 'a list] => bool" (infixl 55)
+ mem :: "['a, 'a list] => bool" (infixl 55)
list_all :: "('a => bool) => ('a list => bool)"
map :: "('a=>'b) => ('a list => 'b list)"
- "@" :: "['a list, 'a list] => 'a list" (infixr 65)
+ "@" :: "['a list, 'a list] => 'a list" (infixr 65)
filter :: "['a => bool, 'a list] => 'a list"
+ foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
+ length :: "'a list => nat"
+syntax
(* list Enumeration *)
-
- "[]" :: "'a list" ("[]")
- "@list" :: "args => 'a list" ("[(_)]")
+ "@list" :: "args => 'a list" ("[(_)]")
(* Special syntax for list_all and filter *)
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
@@ -55,66 +35,42 @@
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
- "[]" == "Nil"
-
- "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys.b, xs)"
"[x:xs . P]" == "filter(%x.P,xs)"
"Alls x:xs.P" == "list_all(%x.P,xs)"
-defs
- (* Defining the Concrete Constructors *)
- NIL_def "NIL == In0(Numb(0))"
- CONS_def "CONS(M, N) == In1(M $ N)"
-
-inductive "list(A)"
- intrs
- NIL_I "NIL: list(A)"
- CONS_I "[| a: A; M: list(A) |] ==> CONS(a,M) : list(A)"
-
-rules
- (* 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"
-
-
-defs
- (* Defining the Abstract Constructors *)
- Nil_def "Nil == Abs_list(NIL)"
- Cons_def "x#xs == Abs_list(CONS(Leaf(x), Rep_list(xs)))"
-
- List_case_def "List_case(c, d) == Case(%x.c, Split(d))"
-
- (* list Recursion -- the trancl is Essential; see list.ML *)
-
- List_rec_def
- "List_rec(M, c, d) == wfrec(trancl(pred_sexp), M, \
-\ List_case(%g.c, %x y g. 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. 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)"
- (* a total version of tl: *)
- ttl_def "ttl(xs) == list_rec(xs, [], %x xs r.xs)"
-
- mem_def "x mem xs == \
-\ list_rec(xs, False, %y ys r. if(y=x, True, r))"
- 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, [], %x l r. f(x)#r)"
- append_def "xs@ys == list_rec(xs, ys, %x l r. x#r)"
- filter_def "filter(P,xs) == \
-\ list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
-
- list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
-
+primrec null list
+ null_Nil "null([]) = True"
+ null_Cons "null(x#xs) = False"
+primrec hd list
+ hd_Nil "hd([]) = (@x.False)"
+ hd_Cons "hd(x#xs) = x"
+primrec tl list
+ tl_Nil "tl([]) = (@x.False)"
+ tl_Cons "tl(x#xs) = xs"
+primrec ttl list
+ (* a "total" version of tl: *)
+ ttl_Nil "ttl([]) = []"
+ ttl_Cons "ttl(x#xs) = xs"
+primrec "op mem" list
+ mem_Nil "x mem [] = False"
+ mem_Cons "x mem (y#ys) = if(y=x, True, x mem ys)"
+primrec list_all list
+ list_all_Nil "list_all(P,[]) = True"
+ list_all_Cons "list_all(P,x#xs) = (P(x) & list_all(P,xs))"
+primrec map list
+ map_Nil "map(f,[]) = []"
+ map_Cons "map(f,x#xs) = f(x)#map(f,xs)"
+primrec "op @" list
+ append_Nil "[] @ ys = ys"
+ append_Cons "(x#xs)@ys = x#(xs@ys)"
+primrec filter list
+ filter_Nil "filter(P,[]) = []"
+ filter_Cons "filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))"
+primrec foldl list
+ foldl_Nil "foldl(f,a,[]) = a"
+ foldl_Cons "foldl(f,a,x#xs) = foldl(f, f(a,x), xs)"
+primrec length list
+ length_Nil "length([]) = 0"
+ length_Cons "length(x#xs) = Suc(length(xs))"
end