4 Copyright 1994 TU Muenchen
6 The datatype of finite lists.
9 List = Datatype + WF_Rel +
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
14 "@" :: ['a list, 'a list] => 'a list (infixr 65)
15 filter :: ['a => bool, 'a list] => 'a list
16 concat :: 'a list list => 'a list
17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b
18 hd, last :: 'a list => 'a
19 set :: 'a list => 'a set
20 list_all :: ('a => bool) => ('a list => bool)
21 map :: ('a=>'b) => ('a list => 'b list)
22 mem :: ['a, 'a list] => bool (infixl 55)
23 nth :: ['a list, nat] => 'a (infixl "!" 100)
24 list_update :: 'a list => nat => 'a => 'a list
25 take, drop :: [nat, 'a list] => 'a list
27 dropWhile :: ('a => bool) => 'a list => 'a list
28 tl, butlast :: 'a list => 'a list
29 rev :: 'a list => 'a list
30 zip :: "'a list => 'b list => ('a * 'b) list"
31 upt :: nat => nat => nat list ("(1[_../_'(])")
32 remdups :: 'a list => 'a list
33 nodups :: "'a list => bool"
34 replicate :: nat => 'a => 'a list
40 (* list Enumeration *)
41 "@list" :: args => 'a list ("[(_)]")
43 (* Special syntax for filter *)
44 "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
47 "_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)")
48 "" :: lupdbind => lupdbinds ("_")
49 "_lupdbinds" :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _")
50 "_LUpdate" :: ['a, lupdbinds] => 'a ("_/[(_)]" [900,0] 900)
52 upto :: nat => nat => nat list ("(1[_../_])")
57 "[x:xs . P]" == "filter (%x. P) xs"
59 "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
60 "xs[i:=x]" == "list_update xs i x"
62 "[i..j]" == "[i..(Suc j)(]"
66 "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
70 lists :: 'a set => 'a list set
75 Cons "[| a: A; l: lists A |] ==> a#l : lists A"
78 (*Function "size" is overloaded for all datatypes. Users may refer to the
79 list version as "length".*)
80 syntax length :: 'a list => nat
81 translations "length" => "size:: _ list => nat"
91 "last(x#xs) = (if xs=[] then x else last xs)"
94 "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
97 "x mem (y#ys) = (if y=x then True else x mem ys)"
100 "set (x#xs) = insert x (set xs)"
102 list_all_Nil "list_all P [] = True"
103 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)"
106 "map f (x#xs) = f(x)#map f xs"
108 append_Nil "[] @ys = ys"
109 append_Cons "(x#xs)@ys = x#(xs@ys)"
112 "rev(x#xs) = rev(xs) @ [x]"
115 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
118 "foldl f a (x#xs) = foldl f (f a x) xs"
121 "concat(x#xs) = x @ concat(xs)"
123 drop_Nil "drop n [] = []"
124 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
126 take_Nil "take n [] = []"
127 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
130 "xs!(Suc n) = (tl xs)!n"
133 "(x#xs)[i:=v] = (case i of 0 => v # xs
134 | Suc j => x # xs[j:=v])"
136 "takeWhile P [] = []"
137 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
139 "dropWhile P [] = []"
140 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
143 "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
146 "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
149 "nodups (x#xs) = (x ~: set xs & nodups xs)"
152 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
154 replicate_0 "replicate 0 x = []"
155 replicate_Suc "replicate (Suc n) x = x # replicate n x"
157 (** Lexcicographic orderings on lists **)
160 lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
163 "lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r ** lexn r n)) Int
164 {(xs,ys). length xs = Suc n & length ys = Suc n}"
167 lex :: "('a * 'a)set => ('a list * 'a list)set"
168 "lex r == UN n. lexn r n"
170 lexico :: "('a * 'a)set => ('a list * 'a list)set"
171 "lexico r == inv_image (less_than ** lex r) (%xs. (length xs, xs))"
179 (* translating size::list -> length *)
181 fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
182 Syntax.const "length" $ t
183 | size_tr' _ _ _ = raise Match;
187 val typed_print_translation = [("size", size_tr')];