Removed unnecessary primrec equations of hd and last involving arbitrary.
4 Copyright 1994 TU Muenchen
6 The datatype of finite lists.
11 datatype 'a list = Nil ("[]") | Cons '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 foldr :: [['a,'b] => 'b, 'a list, 'b] => 'b
19 hd, last :: 'a list => 'a
20 set :: 'a list => 'a set
21 list_all :: ('a => bool) => ('a list => bool)
22 list_all2 :: ('a => 'b => bool) => 'a list => 'b list => bool
23 map :: ('a=>'b) => ('a list => 'b list)
24 mem :: ['a, 'a list] => bool (infixl 55)
25 nth :: ['a list, nat] => 'a (infixl "!" 100)
26 list_update :: 'a list => nat => 'a => 'a list
27 take, drop :: [nat, 'a list] => 'a list
29 dropWhile :: ('a => bool) => 'a list => 'a list
30 tl, butlast :: 'a list => 'a list
31 rev :: 'a list => 'a list
32 zip :: "'a list => 'b list => ('a * 'b) list"
33 upt :: nat => nat => nat list ("(1[_../_'(])")
34 remdups :: 'a list => 'a list
35 nodups :: "'a list => bool"
36 replicate :: nat => 'a => 'a list
42 (* list Enumeration *)
43 "@list" :: args => 'a list ("[(_)]")
45 (* Special syntax for filter *)
46 "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
49 "_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)")
50 "" :: lupdbind => lupdbinds ("_")
51 "_lupdbinds" :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _")
52 "_LUpdate" :: ['a, lupdbinds] => 'a ("_/[(_)]" [900,0] 900)
54 upto :: nat => nat => nat list ("(1[_../_])")
59 "[x:xs . P]" == "filter (%x. P) xs"
61 "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
62 "xs[i:=x]" == "list_update xs i x"
64 "[i..j]" == "[i..(Suc j)(]"
68 "@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
72 lists :: 'a set => 'a list set
77 Cons "[| a: A; l: lists A |] ==> a#l : lists A"
80 (*Function "size" is overloaded for all datatypes. Users may refer to the
81 list version as "length".*)
82 syntax length :: 'a list => nat
83 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)"
117 foldl_Nil "foldl f a [] = a"
118 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs"
121 "foldr f (x#xs) a = f x (foldr f xs a)"
124 "concat(x#xs) = x @ concat(xs)"
126 drop_Nil "drop n [] = []"
127 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
128 (* Warning: simpset does not contain this definition but separate theorems
131 take_Nil "take n [] = []"
132 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
133 (* Warning: simpset does not contain this definition but separate theorems
136 nth_Cons "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
137 (* Warning: simpset does not contain this definition but separate theorems
141 "(x#xs)[i:=v] = (case i of 0 => v # xs
142 | Suc j => x # xs[j:=v])"
144 "takeWhile P [] = []"
145 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
147 "dropWhile P [] = []"
148 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
151 "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
152 (* Warning: simpset does not contain this definition but separate theorems
153 for xs=[] / xs=z#zs *)
156 "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
159 "nodups (x#xs) = (x ~: set xs & nodups xs)"
162 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
164 replicate_0 "replicate 0 x = []"
165 replicate_Suc "replicate (Suc n) x = x # replicate n x"
168 "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)"
171 (** Lexicographic orderings on lists **)
174 lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
177 "lexn r (Suc n) = (prod_fun (split op#) (split op#) `` (r <*lex*> lexn r n)) Int
178 {(xs,ys). length xs = Suc n & length ys = Suc n}"
181 lex :: "('a * 'a)set => ('a list * 'a list)set"
182 "lex r == UN n. lexn r n"
184 lexico :: "('a * 'a)set => ('a list * 'a list)set"
185 "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
193 (* translating size::list -> length *)
195 fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
196 Syntax.const "length" $ t
197 | size_tr' _ _ _ = raise Match;
201 val typed_print_translation = [("size", size_tr')];