equal
deleted
inserted
replaced
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 The datatype of finite lists. |
6 The datatype of finite lists. |
7 *) |
7 *) |
8 |
8 |
9 List = WF_Rel + Datatype + |
9 List = Datatype + Recdef + |
10 |
10 |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
12 |
12 |
13 consts |
13 consts |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
26 takeWhile, |
26 takeWhile, |
27 dropWhile :: ('a => bool) => 'a list => 'a list |
27 dropWhile :: ('a => bool) => 'a list => 'a list |
28 tl, butlast :: 'a list => 'a list |
28 tl, butlast :: 'a list => 'a list |
29 rev :: 'a list => 'a list |
29 rev :: 'a list => 'a list |
30 zip :: "'a list => 'b list => ('a * 'b) list" |
30 zip :: "'a list => 'b list => ('a * 'b) list" |
|
31 upto :: nat => nat => nat list ("(1[_../_])") |
|
32 paired_upto :: "nat * nat => nat list" |
31 remdups :: 'a list => 'a list |
33 remdups :: 'a list => 'a list |
32 nodups :: "'a list => bool" |
34 nodups :: "'a list => bool" |
33 replicate :: nat => 'a => 'a list |
35 replicate :: nat => 'a => 'a list |
34 |
36 |
35 nonterminals |
37 nonterminals |
133 "dropWhile P [] = []" |
135 "dropWhile P [] = []" |
134 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
136 "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" |
135 primrec |
137 primrec |
136 "zip xs [] = []" |
138 "zip xs [] = []" |
137 "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys" |
139 "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys" |
|
140 recdef paired_upto "measure(%(i,j). (Suc j)-i)" |
|
141 "paired_upto(i,j) = (if j<i then [] else i#paired_upto(Suc i,j))" |
|
142 defs upto_def "[i..j] == paired_upto(i,j)" |
138 primrec |
143 primrec |
139 "nodups [] = True" |
144 "nodups [] = True" |
140 "nodups (x#xs) = (x ~: set xs & nodups xs)" |
145 "nodups (x#xs) = (x ~: set xs & nodups xs)" |
141 primrec |
146 primrec |
142 "remdups [] = []" |
147 "remdups [] = []" |