17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
18 foldr :: [['a,'b] => 'b, 'a list, 'b] => 'b |
18 foldr :: [['a,'b] => 'b, 'a list, 'b] => 'b |
19 hd, last :: 'a list => 'a |
19 hd, last :: 'a list => 'a |
20 set :: 'a list => 'a set |
20 set :: 'a list => 'a set |
21 list_all :: ('a => bool) => ('a list => bool) |
21 list_all :: ('a => bool) => ('a list => bool) |
|
22 list_all2 :: ('a => 'b => bool) => 'a list => 'b list => bool |
22 map :: ('a=>'b) => ('a list => 'b list) |
23 map :: ('a=>'b) => ('a list => 'b list) |
23 mem :: ['a, 'a list] => bool (infixl 55) |
24 mem :: ['a, 'a list] => bool (infixl 55) |
24 nth :: ['a list, nat] => 'a (infixl "!" 100) |
25 nth :: ['a list, nat] => 'a (infixl "!" 100) |
25 list_update :: 'a list => nat => 'a => 'a list |
26 list_update :: 'a list => nat => 'a => 'a list |
26 take, drop :: [nat, 'a list] => 'a list |
27 take, drop :: [nat, 'a list] => 'a list |
162 "remdups [] = []" |
163 "remdups [] = []" |
163 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
164 "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" |
164 primrec |
165 primrec |
165 replicate_0 "replicate 0 x = []" |
166 replicate_0 "replicate 0 x = []" |
166 replicate_Suc "replicate (Suc n) x = x # replicate n x" |
167 replicate_Suc "replicate (Suc n) x = x # replicate n x" |
|
168 defs |
|
169 list_all2_def |
|
170 "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)" |
|
171 |
167 |
172 |
168 (** Lexicographic orderings on lists **) |
173 (** Lexicographic orderings on lists **) |
169 |
174 |
170 consts |
175 consts |
171 lexn :: "('a * 'a)set => nat => ('a list * 'a list)set" |
176 lexn :: "('a * 'a)set => nat => ('a list * 'a list)set" |