author  nipkow 
Thu, 14 Feb 2002 11:50:52 +0100  
changeset 12887  d25b43743e10 
parent 12114  a8e860c86252 
child 13114  f2b00262bdfc 
permissions  rwrr 
923  1 
(* Title: HOL/List.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1994 TU Muenchen 

5 

2512  6 
The datatype of finite lists. 
923  7 
*) 
8 

8490  9 
List = PreList + 
923  10 

7224  11 
datatype 'a list = Nil ("[]")  Cons 'a ('a list) (infixr "#" 65) 
923  12 

13 
consts 

1908  14 
"@" :: ['a list, 'a list] => 'a list (infixr 65) 
15 
filter :: ['a => bool, 'a list] => 'a list 

2608  16 
concat :: 'a list list => 'a list 
1908  17 
foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b 
8000  18 
foldr :: [['a,'b] => 'b, 'a list, 'b] => 'b 
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset

19 
hd, last :: 'a list => 'a 
3465  20 
set :: 'a list => 'a set 
5518  21 
list_all :: ('a => bool) => ('a list => bool) 
8115  22 
list_all2 :: ('a => 'b => bool) => 'a list => 'b list => bool 
1908  23 
map :: ('a=>'b) => ('a list => 'b list) 
5518  24 
mem :: ['a, 'a list] => bool (infixl 55) 
4502  25 
nth :: ['a list, nat] => 'a (infixl "!" 100) 
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

26 
list_update :: 'a list => nat => 'a => 'a list 
2608  27 
take, drop :: [nat, 'a list] => 'a list 
28 
takeWhile, 

29 
dropWhile :: ('a => bool) => 'a list => 'a list 

3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset

30 
tl, butlast :: 'a list => 'a list 
1908  31 
rev :: 'a list => 'a list 
4132  32 
zip :: "'a list => 'b list => ('a * 'b) list" 
5427  33 
upt :: nat => nat => nat list ("(1[_../_'(])") 
12887  34 
remdups :: "'a list => 'a list" 
35 
null, "distinct" :: "'a list => bool" 

3589
244daa75f890
Added function `replicate' and lemmas map_cong and set_replicate.
nipkow
parents:
3584
diff
changeset

36 
replicate :: nat => 'a => 'a list 
923  37 

5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

38 
nonterminals 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

39 
lupdbinds lupdbind 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

40 

923  41 
syntax 
42 
(* list Enumeration *) 

2262  43 
"@list" :: args => 'a list ("[(_)]") 
923  44 

2512  45 
(* Special syntax for filter *) 
9341  46 
"@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_:_./ _])") 
923  47 

5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

48 
(* list update *) 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

49 
"_lupdbind" :: ['a, 'a] => lupdbind ("(2_ :=/ _)") 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

50 
"" :: lupdbind => lupdbinds ("_") 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

51 
"_lupdbinds" :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _") 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

52 
"_LUpdate" :: ['a, lupdbinds] => 'a ("_/[(_)]" [900,0] 900) 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

53 

5427  54 
upto :: nat => nat => nat list ("(1[_../_])") 
55 

923  56 
translations 
57 
"[x, xs]" == "x#[xs]" 

58 
"[x]" == "x#[]" 

3842  59 
"[x:xs . P]" == "filter (%x. P) xs" 
923  60 

5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

61 
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs" 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

62 
"xs[i:=x]" == "list_update xs i x" 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

63 

5427  64 
"[i..j]" == "[i..(Suc j)(]" 
65 

66 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10832
diff
changeset

67 
syntax (xsymbols) 
5295  68 
"@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])") 
2262  69 

70 

3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

71 
consts 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

72 
lists :: 'a set => 'a list set 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

73 

ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

74 
inductive "lists A" 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

75 
intrs 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

76 
Nil "[]: lists A" 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

77 
Cons "[ a: A; l: lists A ] ==> a#l : lists A" 
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

78 

ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

79 

3437
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the builtin
paulson
parents:
3401
diff
changeset

80 
(*Function "size" is overloaded for all datatypes. Users may refer to the 
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the builtin
paulson
parents:
3401
diff
changeset

81 
list version as "length".*) 
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the builtin
paulson
parents:
3401
diff
changeset

82 
syntax length :: 'a list => nat 
3507  83 
translations "length" => "size:: _ list => nat" 
3437
bea2faf1641d
Replacing the primrec definition of "length" by a translation to the builtin
paulson
parents:
3401
diff
changeset

84 

5183  85 
primrec 
1898  86 
"hd(x#xs) = x" 
5183  87 
primrec 
8972  88 
"tl([]) = []" 
1898  89 
"tl(x#xs) = xs" 
5183  90 
primrec 
8972  91 
"null([]) = True" 
92 
"null(x#xs) = False" 

93 
primrec 

3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset

94 
"last(x#xs) = (if xs=[] then x else last xs)" 
5183  95 
primrec 
8972  96 
"butlast [] = []" 
3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset

97 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 
5183  98 
primrec 
8972  99 
"x mem [] = False" 
5518  100 
"x mem (y#ys) = (if y=x then True else x mem ys)" 
101 
primrec 

3465  102 
"set [] = {}" 
103 
"set (x#xs) = insert x (set xs)" 

5183  104 
primrec 
5518  105 
list_all_Nil "list_all P [] = True" 
106 
list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" 

107 
primrec 

8972  108 
"map f [] = []" 
1898  109 
"map f (x#xs) = f(x)#map f xs" 
5183  110 
primrec 
111 
append_Nil "[] @ys = ys" 

112 
append_Cons "(x#xs)@ys = x#(xs@ys)" 

113 
primrec 

8972  114 
"rev([]) = []" 
1898  115 
"rev(x#xs) = rev(xs) @ [x]" 
5183  116 
primrec 
8972  117 
"filter P [] = []" 
1898  118 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 
5183  119 
primrec 
6141  120 
foldl_Nil "foldl f a [] = a" 
121 
foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" 

5183  122 
primrec 
8972  123 
"foldr f [] a = a" 
8000  124 
"foldr f (x#xs) a = f x (foldr f xs a)" 
125 
primrec 

8972  126 
"concat([]) = []" 
2608  127 
"concat(x#xs) = x @ concat(xs)" 
5183  128 
primrec 
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1370
diff
changeset

129 
drop_Nil "drop n [] = []" 
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1370
diff
changeset

130 
drop_Cons "drop n (x#xs) = (case n of 0 => x#xs  Suc(m) => drop m xs)" 
6408  131 
(* Warning: simpset does not contain this definition but separate theorems 
132 
for n=0 / n=Suc k*) 

5183  133 
primrec 
1419
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1370
diff
changeset

134 
take_Nil "take n [] = []" 
a6a034a47a71
defined take/drop by induction over list rather than nat.
nipkow
parents:
1370
diff
changeset

135 
take_Cons "take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs)" 
6408  136 
(* Warning: simpset does not contain this definition but separate theorems 
137 
for n=0 / n=Suc k*) 

138 
primrec 

139 
nth_Cons "(x#xs)!n = (case n of 0 => x  (Suc k) => xs!k)" 

140 
(* Warning: simpset does not contain this definition but separate theorems 

141 
for n=0 / n=Suc k*) 

5183  142 
primrec 
5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

143 
" [][i:=v] = []" 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

144 
"(x#xs)[i:=v] = (case i of 0 => v # xs 
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
4643
diff
changeset

145 
 Suc j => x # xs[j:=v])" 
5183  146 
primrec 
8972  147 
"takeWhile P [] = []" 
2608  148 
"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" 
5183  149 
primrec 
8972  150 
"dropWhile P [] = []" 
3584
8f9ee0f79d9a
Corected bug in def of dropWhile (also present in Haskell lib!)
nipkow
parents:
3507
diff
changeset

151 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 
5183  152 
primrec 
4132  153 
"zip xs [] = []" 
6306  154 
"zip xs (y#ys) = (case xs of [] => []  z#zs => (z,y)#zip zs ys)" 
6408  155 
(* Warning: simpset does not contain this definition but separate theorems 
156 
for xs=[] / xs=z#zs *) 

5427  157 
primrec 
8983  158 
upt_0 "[i..0(] = []" 
159 
upt_Suc "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])" 

5183  160 
primrec 
12887  161 
"distinct [] = True" 
162 
"distinct (x#xs) = (x ~: set xs & distinct xs)" 

5183  163 
primrec 
4605  164 
"remdups [] = []" 
165 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

5183  166 
primrec 
5443
e2459d18ff47
changed constants mem and list_all to mere translations
oheimb
parents:
5427
diff
changeset

167 
replicate_0 "replicate 0 x = []" 
5183  168 
replicate_Suc "replicate (Suc n) x = x # replicate n x" 
8115  169 
defs 
170 
list_all2_def 

171 
"list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)" 

172 

3196  173 

6408  174 
(** Lexicographic orderings on lists **) 
5281  175 

176 
consts 

177 
lexn :: "('a * 'a)set => nat => ('a list * 'a list)set" 

178 
primrec 

179 
"lexn r 0 = {}" 

10832  180 
"lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int 
5281  181 
{(xs,ys). length xs = Suc n & length ys = Suc n}" 
182 

183 
constdefs 

9336  184 
lex :: "('a * 'a)set => ('a list * 'a list)set" 
185 
"lex r == UN n. lexn r n" 

5281  186 

9336  187 
lexico :: "('a * 'a)set => ('a list * 'a list)set" 
188 
"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))" 

189 

190 
sublist :: "['a list, nat set] => 'a list" 

191 
"sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))" 

5281  192 

923  193 
end 
3507  194 

195 
ML 

196 

197 
local 

198 

199 
(* translating size::list > length *) 

200 

4151  201 
fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] = 
3507  202 
Syntax.const "length" $ t 
4151  203 
 size_tr' _ _ _ = raise Match; 
3507  204 

205 
in 

206 

207 
val typed_print_translation = [("size", size_tr')]; 

208 

209 
end; 