author  kleing 
Mon, 05 Nov 2007 22:49:28 +0100  
changeset 25296  c187b7422156 
parent 25287  094dab519ff5 
child 25502  9200b36280c0 
permissions  rwrr 
13462  1 
(* Title: HOL/List.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

923  4 
*) 
5 

13114  6 
header {* The datatype of finite lists *} 
13122  7 

15131  8 
theory List 
22844  9 
imports PreList 
21754
6316163ae934
moved char/string syntax to Tools/string_syntax.ML;
wenzelm
parents:
21548
diff
changeset

10 
uses "Tools/string_syntax.ML" 
15131  11 
begin 
923  12 

13142  13 
datatype 'a list = 
13366  14 
Nil ("[]") 
15 
 Cons 'a "'a list" (infixr "#" 65) 

923  16 

15392  17 
subsection{*Basic list processing functions*} 
15302  18 

923  19 
consts 
13366  20 
filter:: "('a => bool) => 'a list => 'a list" 
21 
concat:: "'a list list => 'a list" 

22 
foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b" 

23 
foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b" 

24 
hd:: "'a list => 'a" 

25 
tl:: "'a list => 'a list" 

26 
last:: "'a list => 'a" 

27 
butlast :: "'a list => 'a list" 

28 
set :: "'a list => 'a set" 

29 
map :: "('a=>'b) => ('a list => 'b list)" 

23096  30 
listsum :: "'a list => 'a::monoid_add" 
13366  31 
nth :: "'a list => nat => 'a" (infixl "!" 100) 
32 
list_update :: "'a list => nat => 'a => 'a list" 

33 
take:: "nat => 'a list => 'a list" 

34 
drop:: "nat => 'a list => 'a list" 

35 
takeWhile :: "('a => bool) => 'a list => 'a list" 

36 
dropWhile :: "('a => bool) => 'a list => 'a list" 

37 
rev :: "'a list => 'a list" 

38 
zip :: "'a list => 'b list => ('a * 'b) list" 

15425  39 
upt :: "nat => nat => nat list" ("(1[_..</_'])") 
13366  40 
remdups :: "'a list => 'a list" 
15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

41 
remove1 :: "'a => 'a list => 'a list" 
13366  42 
"distinct":: "'a list => bool" 
43 
replicate :: "nat => 'a => 'a list" 

19390  44 
splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
15302  45 

923  46 

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

48 

923  49 
syntax 
13366  50 
 {* list Enumeration *} 
51 
"@list" :: "args => 'a list" ("[(_)]") 

923  52 

13366  53 
 {* Special syntax for filter *} 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

54 
"@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<_./ _])") 
923  55 

13366  56 
 {* list update *} 
57 
"_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)") 

58 
"" :: "lupdbind => lupdbinds" ("_") 

59 
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _") 

60 
"_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900) 

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

61 

923  62 
translations 
13366  63 
"[x, xs]" == "x#[xs]" 
64 
"[x]" == "x#[]" 

23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

65 
"[x<xs . P]"== "filter (%x. P) xs" 
923  66 

13366  67 
"_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs" 
68 
"xs[i:=x]" == "list_update xs i x" 

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

69 

5427  70 

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

71 
syntax (xsymbols) 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

72 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
14565  73 
syntax (HTML output) 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

74 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") 
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

75 

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

76 

13142  77 
text {* 
14589  78 
Function @{text size} is overloaded for all datatypes. Users may 
13366  79 
refer to the list version as @{text length}. *} 
13142  80 

19363  81 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

82 
length :: "'a list => nat" where 
19363  83 
"length == size" 
15302  84 

5183  85 
primrec 
15307  86 
"hd(x#xs) = x" 
87 

5183  88 
primrec 
15307  89 
"tl([]) = []" 
90 
"tl(x#xs) = xs" 

91 

5183  92 
primrec 
15307  93 
"last(x#xs) = (if xs=[] then x else last xs)" 
94 

5183  95 
primrec 
15307  96 
"butlast []= []" 
97 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 

98 

5183  99 
primrec 
15307  100 
"set [] = {}" 
101 
"set (x#xs) = insert x (set xs)" 

102 

5183  103 
primrec 
15307  104 
"map f [] = []" 
105 
"map f (x#xs) = f(x)#map f xs" 

106 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

107 
setup {* snd o Sign.declare_const [] (*authentic syntax*) 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

108 
("append", @{typ "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"}, InfixrName ("@", 65)) *} 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

109 
primrec 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

110 
append_Nil:"[]@ys = ys" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

111 
append_Cons: "(x#xs)@ys = x#(xs@ys)" 
15307  112 

5183  113 
primrec 
15307  114 
"rev([]) = []" 
115 
"rev(x#xs) = rev(xs) @ [x]" 

116 

5183  117 
primrec 
15307  118 
"filter P [] = []" 
119 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 

120 

5183  121 
primrec 
15307  122 
foldl_Nil:"foldl f a [] = a" 
123 
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" 

124 

8000  125 
primrec 
15307  126 
"foldr f [] a = a" 
127 
"foldr f (x#xs) a = f x (foldr f xs a)" 

128 

5183  129 
primrec 
15307  130 
"concat([]) = []" 
131 
"concat(x#xs) = x @ concat(xs)" 

132 

5183  133 
primrec 
23096  134 
"listsum [] = 0" 
135 
"listsum (x # xs) = x + listsum xs" 

136 

137 
primrec 

15307  138 
drop_Nil:"drop n [] = []" 
139 
drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs  Suc(m) => drop m xs)" 

140 
 {*Warning: simpset does not contain this definition, but separate 

141 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

142 

5183  143 
primrec 
15307  144 
take_Nil:"take n [] = []" 
145 
take_Cons: "take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs)" 

146 
 {*Warning: simpset does not contain this definition, but separate 

147 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

148 

13142  149 
primrec 
15307  150 
nth_Cons:"(x#xs)!n = (case n of 0 => x  (Suc k) => xs!k)" 
151 
 {*Warning: simpset does not contain this definition, but separate 

152 
theorems for @{text "n = 0"} and @{text "n = Suc k"} *} 

153 

5183  154 
primrec 
15307  155 
"[][i:=v] = []" 
156 
"(x#xs)[i:=v] = (case i of 0 => v # xs  Suc j => x # xs[j:=v])" 

157 

158 
primrec 

159 
"takeWhile P [] = []" 

160 
"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" 

161 

5183  162 
primrec 
15307  163 
"dropWhile P [] = []" 
164 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 

165 

5183  166 
primrec 
15307  167 
"zip xs [] = []" 
168 
zip_Cons: "zip xs (y#ys) = (case xs of [] => []  z#zs => (z,y)#zip zs ys)" 

169 
 {*Warning: simpset does not contain this definition, but separate 

170 
theorems for @{text "xs = []"} and @{text "xs = z # zs"} *} 

171 

5427  172 
primrec 
15425  173 
upt_0: "[i..<0] = []" 
174 
upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

15307  175 

5183  176 
primrec 
15307  177 
"distinct [] = True" 
178 
"distinct (x#xs) = (x ~: set xs \<and> distinct xs)" 

179 

5183  180 
primrec 
15307  181 
"remdups [] = []" 
182 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

183 

5183  184 
primrec 
15307  185 
"remove1 x [] = []" 
186 
"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" 

187 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

188 
primrec 
15307  189 
replicate_0: "replicate 0 x = []" 
190 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

191 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

192 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

193 
rotate1 :: "'a list \<Rightarrow> 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

194 
"rotate1 xs = (case xs of [] \<Rightarrow> []  x#xs \<Rightarrow> xs @ [x])" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

195 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

196 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

197 
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

198 
"rotate n = rotate1 ^ n" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

199 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

200 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

201 
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

202 
"list_all2 P xs ys = 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

203 
(length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

204 

eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

205 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

206 
sublist :: "'a list => nat set => 'a list" where 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21211
diff
changeset

207 
"sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))" 
17086  208 

209 
primrec 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

210 
"splice [] ys = ys" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

211 
"splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

212 
 {*Warning: simpset does not contain the second eqn but a derived one. *} 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

213 

24616  214 
text{* The following simple sort functions are intended for proofs, 
215 
not for efficient implementations. *} 

216 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

217 
context linorder 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

218 
begin 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

219 

5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

220 
fun sorted :: "'a list \<Rightarrow> bool" where 
24697  221 
"sorted [] \<longleftrightarrow> True"  
222 
"sorted [x] \<longleftrightarrow> True"  

25062  223 
"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)" 
24697  224 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

225 
fun insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
24697  226 
"insort x [] = [x]"  
25062  227 
"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))" 
24697  228 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

229 
fun sort :: "'a list \<Rightarrow> 'a list" where 
24697  230 
"sort [] = []"  
231 
"sort (x#xs) = insort x (sort xs)" 

24616  232 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

233 
end 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

234 

24616  235 

23388  236 
subsubsection {* List comprehension *} 
23192  237 

24349  238 
text{* Input syntax for Haskelllike list comprehension notation. 
239 
Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, 

240 
the list of all pairs of distinct elements from @{text xs} and @{text ys}. 

241 
The syntax is as in Haskell, except that @{text""} becomes a dot 

242 
(like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than 

243 
\verb![e x < xs, ...]!. 

244 

245 
The qualifiers after the dot are 

246 
\begin{description} 

247 
\item[generators] @{text"p \<leftarrow> xs"}, 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

248 
where @{text p} is a pattern and @{text xs} an expression of list type, or 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

249 
\item[guards] @{text"b"}, where @{text b} is a boolean expression. 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

250 
%\item[local bindings] @ {text"let x = e"}. 
24349  251 
\end{description} 
23240  252 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

253 
Just like in Haskell, list comprehension is just a shorthand. To avoid 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

254 
misunderstandings, the translation into desugared form is not reversed 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

255 
upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

256 
optmized to @{term"map (%x. e) xs"}. 
23240  257 

24349  258 
It is easy to write short list comprehensions which stand for complex 
259 
expressions. During proofs, they may become unreadable (and 

260 
mangled). In such cases it can be advisable to introduce separate 

261 
definitions for the list comprehensions in question. *} 

262 

23209  263 
(* 
23240  264 
Proper theorem proving support would be nice. For example, if 
23192  265 
@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"} 
266 
produced something like 

23209  267 
@{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}. 
268 
*) 

269 

23240  270 
nonterminals lc_qual lc_quals 
23192  271 

272 
syntax 

23240  273 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
24349  274 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 
23240  275 
"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

276 
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*) 
23240  277 
"_lc_end" :: "lc_quals" ("]") 
278 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

24349  279 
"_lc_abs" :: "'a => 'b list => 'b list" 
23192  280 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

281 
(* These are easier than ML code but cannot express the optimized 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

282 
translation of [e. p<xs] 
23192  283 
translations 
24349  284 
"[e. p<xs]" => "concat(map (_lc_abs p [e]) xs)" 
23240  285 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
24349  286 
=> "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)" 
23240  287 
"[e. P]" => "if P then [e] else []" 
288 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

289 
=> "if P then (_listcompr e Q Qs) else []" 

24349  290 
"_listcompr e (_lc_let b) (_lc_quals Q Qs)" 
291 
=> "_Let b (_listcompr e Q Qs)" 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

292 
*) 
23240  293 

23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

294 
syntax (xsymbols) 
24349  295 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

296 
syntax (HTML output) 
24349  297 
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") 
298 

299 
parse_translation (advanced) {* 

300 
let 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

301 
val NilC = Syntax.const @{const_name Nil}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

302 
val ConsC = Syntax.const @{const_name Cons}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

303 
val mapC = Syntax.const @{const_name map}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

304 
val concatC = Syntax.const @{const_name concat}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

305 
val IfC = Syntax.const @{const_name If}; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

306 
fun singl x = ConsC $ x $ NilC; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

307 

f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

308 
fun pat_tr ctxt p e opti = (* %x. case x of p => e  _ => [] *) 
24349  309 
let 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

310 
val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT); 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

311 
val e = if opti then singl e else e; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

312 
val case1 = Syntax.const "_case1" $ p $ e; 
24349  313 
val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

314 
$ NilC; 
24349  315 
val cs = Syntax.const "_case2" $ case1 $ case2 
316 
val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr 

317 
ctxt [x, cs] 

318 
in lambda x ft end; 

319 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

320 
fun abs_tr ctxt (p as Free(s,T)) e opti = 
24349  321 
let val thy = ProofContext.theory_of ctxt; 
322 
val s' = Sign.intern_const thy s 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

323 
in if Sign.declared_const thy s' 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

324 
then (pat_tr ctxt p e opti, false) 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

325 
else (lambda p e, true) 
24349  326 
end 
24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

327 
 abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false); 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

328 

f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

329 
fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

330 
let val res = case qs of Const("_lc_end",_) => singl e 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

331 
 Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs]; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

332 
in IfC $ b $ res $ NilC end 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

333 
 lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

334 
(case abs_tr ctxt p e true of 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

335 
(f,true) => mapC $ f $ es 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

336 
 (f, false) => concatC $ (mapC $ f $ es)) 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

337 
 lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] = 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

338 
let val e' = lc_tr ctxt [e,q,qs]; 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

339 
in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

340 

f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

341 
in [("_listcompr", lc_tr)] end 
24349  342 
*} 
23279
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

343 

23240  344 
(* 
345 
term "[(x,y,z). b]" 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

346 
term "[(x,y,z). x\<leftarrow>xs]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

347 
term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

348 
term "[(x,y,z). x<a, x>b]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

349 
term "[(x,y,z). x\<leftarrow>xs, x>b]" 
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

350 
term "[(x,y,z). x<a, x\<leftarrow>xs]" 
24349  351 
term "[(x,y). Cons True x \<leftarrow> xs]" 
352 
term "[(x,y,z). Cons x [] \<leftarrow> xs]" 

23240  353 
term "[(x,y,z). x<a, x>b, x=d]" 
354 
term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]" 

355 
term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]" 

356 
term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]" 

357 
term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]" 

358 
term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]" 

359 
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]" 

360 
term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]" 

24349  361 
term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]" 
23192  362 
*) 
363 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

364 
subsubsection {* @{const Nil} and @{const Cons} *} 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

365 

580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

366 
lemma not_Cons_self [simp]: 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

367 
"xs \<noteq> x # xs" 
13145  368 
by (induct xs) auto 
13114  369 

13142  370 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  371 

13142  372 
lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)" 
13145  373 
by (induct xs) auto 
13114  374 

13142  375 
lemma length_induct: 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

376 
"(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" 
17589  377 
by (rule measure_induct [of length]) iprover 
13114  378 

379 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

380 
subsubsection {* @{const length} *} 
13114  381 

13142  382 
text {* 
21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

383 
Needs to come before @{text "@"} because of theorem @{text 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

384 
append_eq_append_conv}. 
13142  385 
*} 
13114  386 

13142  387 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  388 
by (induct xs) auto 
13114  389 

13142  390 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  391 
by (induct xs) auto 
13114  392 

13142  393 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  394 
by (induct xs) auto 
13114  395 

13142  396 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  397 
by (cases xs) auto 
13114  398 

13142  399 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  400 
by (induct xs) auto 
13114  401 

13142  402 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  403 
by (induct xs) auto 
13114  404 

23479  405 
lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0" 
406 
by auto 

407 

13114  408 
lemma length_Suc_conv: 
13145  409 
"(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 
410 
by (induct xs) auto 

13142  411 

14025  412 
lemma Suc_length_conv: 
413 
"(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 

14208  414 
apply (induct xs, simp, simp) 
14025  415 
apply blast 
416 
done 

417 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

418 
lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

419 
by (induct xs) auto 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

420 

5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

421 
lemma list_induct2 [consumes 1]: 
24526  422 
"\<lbrakk> length xs = length ys; 
14247  423 
P [] []; 
424 
\<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> 

425 
\<Longrightarrow> P xs ys" 

24526  426 
apply(induct xs arbitrary: ys) 
14247  427 
apply simp 
428 
apply(case_tac ys) 

429 
apply simp 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

430 
apply simp 
14247  431 
done 
13114  432 

22493
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

433 
lemma list_induct2': 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

434 
"\<lbrakk> P [] []; 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

435 
\<And>x xs. P (x#xs) []; 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

436 
\<And>y ys. P [] (y#ys); 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

437 
\<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

438 
\<Longrightarrow> P xs ys" 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

439 
by (induct xs arbitrary: ys) (case_tac x, auto)+ 
db930e490fe5
added another rule for simultaneous induction, and lemmas for zip
krauss
parents:
22422
diff
changeset

440 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

441 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24349  442 
by (rule Eq_FalseI) auto 
24037  443 

444 
simproc_setup list_neq ("(xs::'a list) = ys") = {* 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

445 
(* 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

446 
Reduces xs=ys to False if xs and ys cannot be of the same length. 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

447 
This is the case if the atomic sublists of one are a submultiset 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

448 
of those of the other list and there are fewer Cons's in one than the other. 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

449 
*) 
24037  450 

451 
let 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

452 

cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

453 
fun len (Const("List.list.Nil",_)) acc = acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

454 
 len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1) 
23029  455 
 len (Const("List.append",_) $ xs $ ys) acc = len xs (len ys acc) 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

456 
 len (Const("List.rev",_) $ xs) acc = len xs acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

457 
 len (Const("List.map",_) $ _ $ xs) acc = len xs acc 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

458 
 len t (ts,n) = (t::ts,n); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

459 

24037  460 
fun list_neq _ ss ct = 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

461 
let 
24037  462 
val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

463 
val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

464 
fun prove_neq() = 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

465 
let 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

466 
val Type(_,listT::_) = eqT; 
22994  467 
val size = HOLogic.size_const listT; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

468 
val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

469 
val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

470 
val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len 
22633  471 
(K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1)); 
472 
in SOME (thm RS @{thm neq_if_length_neq}) end 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

473 
in 
23214  474 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
475 
n < m andalso submultiset (op aconv) (rs,ls) 

22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

476 
then prove_neq() else NONE 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

477 
end; 
24037  478 
in list_neq end; 
22143
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

479 
*} 
cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

480 

cf58486ca11b
Added simproc list_neq (prompted by an application)
nipkow
parents:
21911
diff
changeset

481 

15392  482 
subsubsection {* @{text "@"}  append *} 
13114  483 

13142  484 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  485 
by (induct xs) auto 
13114  486 

13142  487 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  488 
by (induct xs) auto 
3507  489 

24449  490 
interpretation semigroup_append: semigroup_add ["op @"] 
491 
by unfold_locales simp 

492 
interpretation monoid_append: monoid_add ["[]" "op @"] 

493 
by unfold_locales (simp+) 

494 

13142  495 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  496 
by (induct xs) auto 
13114  497 

13142  498 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  499 
by (induct xs) auto 
13114  500 

13142  501 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  502 
by (induct xs) auto 
13114  503 

13142  504 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  505 
by (induct xs) auto 
13114  506 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

507 
lemma append_eq_append_conv [simp, noatp]: 
24526  508 
"length xs = length ys \<or> length us = length vs 
13883
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

509 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
24526  510 
apply (induct xs arbitrary: ys) 
14208  511 
apply (case_tac ys, simp, force) 
512 
apply (case_tac ys, force, simp) 

13145  513 
done 
13142  514 

24526  515 
lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) = 
516 
(EX us. xs = zs @ us & us @ ys = ts  xs @ us = zs & ys = us@ ts)" 

517 
apply (induct xs arbitrary: ys zs ts) 

14495  518 
apply fastsimp 
519 
apply(case_tac zs) 

520 
apply simp 

521 
apply fastsimp 

522 
done 

523 

13142  524 
lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  525 
by simp 
13142  526 

527 
lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)" 

13145  528 
by simp 
13114  529 

13142  530 
lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  531 
by simp 
13114  532 

13142  533 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  534 
using append_same_eq [of _ _ "[]"] by auto 
3507  535 

13142  536 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  537 
using append_same_eq [of "[]"] by auto 
13114  538 

24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24219
diff
changeset

539 
lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  540 
by (induct xs) auto 
13114  541 

13142  542 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  543 
by (induct xs) auto 
13114  544 

13142  545 
lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs" 
13145  546 
by (simp add: hd_append split: list.split) 
13114  547 

13142  548 
lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys  z#zs => zs @ ys)" 
13145  549 
by (simp split: list.split) 
13114  550 

13142  551 
lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys" 
13145  552 
by (simp add: tl_append split: list.split) 
13114  553 

554 

14300  555 
lemma Cons_eq_append_conv: "x#xs = ys@zs = 
556 
(ys = [] & x#xs = zs  (EX ys'. x#ys' = ys & xs = ys'@zs))" 

557 
by(cases ys) auto 

558 

15281  559 
lemma append_eq_Cons_conv: "(ys@zs = x#xs) = 
560 
(ys = [] & zs = x#xs  (EX ys'. ys = x#ys' & ys'@zs = xs))" 

561 
by(cases ys) auto 

562 

14300  563 

13142  564 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  565 

566 
lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys" 

13145  567 
by simp 
13114  568 

13142  569 
lemma Cons_eq_appendI: 
13145  570 
"[ x # xs1 = ys; xs = xs1 @ zs ] ==> x # xs = ys @ zs" 
571 
by (drule sym) simp 

13114  572 

13142  573 
lemma append_eq_appendI: 
13145  574 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
575 
by (drule sym) simp 

13114  576 

577 

13142  578 
text {* 
13145  579 
Simplification procedure for all list equalities. 
580 
Currently only tries to rearrange @{text "@"} to see if 

581 
 both lists end in a singleton list, 

582 
 or both lists end in the same list. 

13142  583 
*} 
584 

585 
ML_setup {* 

3507  586 
local 
587 

13114  588 
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = 
13462  589 
(case xs of Const("List.list.Nil",_) => cons  _ => last xs) 
23029  590 
 last (Const("List.append",_) $ _ $ ys) = last ys 
13462  591 
 last t = t; 
13114  592 

593 
fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true 

13462  594 
 list1 _ = false; 
13114  595 

596 
fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) = 

13462  597 
(case xs of Const("List.list.Nil",_) => xs  _ => cons $ butlast xs) 
23029  598 
 butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys 
13462  599 
 butlast xs = Const("List.list.Nil",fastype_of xs); 
13114  600 

22633  601 
val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc}, 
602 
@{thm append_Nil}, @{thm append_Cons}]; 

16973  603 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19890
diff
changeset

604 
fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 
13462  605 
let 
606 
val lastl = last lhs and lastr = last rhs; 

607 
fun rearr conv = 

608 
let 

609 
val lhs1 = butlast lhs and rhs1 = butlast rhs; 

610 
val Type(_,listT::_) = eqT 

611 
val appT = [listT,listT] > listT 

23029  612 
val app = Const("List.append",appT) 
13462  613 
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) 
13480
bb72bd43c6c3
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
wenzelm
parents:
13462
diff
changeset

614 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2)); 
20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19890
diff
changeset

615 
val thm = Goal.prove (Simplifier.the_context ss) [] [] eq 
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
17830
diff
changeset

616 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  617 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  618 

13462  619 
in 
22633  620 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
621 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  622 
else NONE 
13462  623 
end; 
624 

13114  625 
in 
13462  626 

627 
val list_eq_simproc = 

22633  628 
Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq); 
13462  629 

13114  630 
end; 
631 

632 
Addsimprocs [list_eq_simproc]; 

633 
*} 

634 

635 

15392  636 
subsubsection {* @{text map} *} 
13114  637 

13142  638 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  639 
by (induct xs) simp_all 
13114  640 

13142  641 
lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)" 
13145  642 
by (rule ext, induct_tac xs) auto 
13114  643 

13142  644 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  645 
by (induct xs) auto 
13114  646 

13142  647 
lemma map_compose: "map (f o g) xs = map f (map g xs)" 
13145  648 
by (induct xs) (auto simp add: o_def) 
13114  649 

13142  650 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  651 
by (induct xs) auto 
13114  652 

13737  653 
lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)" 
654 
by (induct xs) auto 

655 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19623
diff
changeset

656 
lemma map_cong [fundef_cong, recdef_cong]: 
13145  657 
"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys" 
658 
 {* a congruence rule for @{text map} *} 

13737  659 
by simp 
13114  660 

13142  661 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  662 
by (cases xs) auto 
13114  663 

13142  664 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  665 
by (cases xs) auto 
13114  666 

18447  667 
lemma map_eq_Cons_conv: 
14025  668 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  669 
by (cases xs) auto 
13114  670 

18447  671 
lemma Cons_eq_map_conv: 
14025  672 
"(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" 
673 
by (cases ys) auto 

674 

18447  675 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
676 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

677 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

678 

14111  679 
lemma ex_map_conv: 
680 
"(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)" 

18447  681 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  682 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

683 
lemma map_eq_imp_length_eq: 
24526  684 
"map f xs = map f ys ==> length xs = length ys" 
685 
apply (induct ys arbitrary: xs) 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

686 
apply simp 
24632  687 
apply (metis Suc_length_conv length_map) 
15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

688 
done 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

689 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

690 
lemma map_inj_on: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

691 
"[ map f xs = map f ys; inj_on f (set xs Un set ys) ] 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

692 
==> xs = ys" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

693 
apply(frule map_eq_imp_length_eq) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

694 
apply(rotate_tac 1) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

695 
apply(induct rule:list_induct2) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

696 
apply simp 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

697 
apply(simp) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

698 
apply (blast intro:sym) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

699 
done 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

700 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

701 
lemma inj_on_map_eq_map: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

702 
"inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

703 
by(blast dest:map_inj_on) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

704 

13114  705 
lemma map_injective: 
24526  706 
"map f xs = map f ys ==> inj f ==> xs = ys" 
707 
by (induct ys arbitrary: xs) (auto dest!:injD) 

13114  708 

14339  709 
lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)" 
710 
by(blast dest:map_injective) 

711 

13114  712 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  713 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  714 

715 
lemma inj_mapD: "inj (map f) ==> inj f" 

14208  716 
apply (unfold inj_on_def, clarify) 
13145  717 
apply (erule_tac x = "[x]" in ballE) 
14208  718 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  719 
apply blast 
720 
done 

13114  721 

14339  722 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  723 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  724 

15303  725 
lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A" 
726 
apply(rule inj_onI) 

727 
apply(erule map_inj_on) 

728 
apply(blast intro:inj_onI dest:inj_onD) 

729 
done 

730 

14343  731 
lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs" 
732 
by (induct xs, auto) 

13114  733 

14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

734 
lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs" 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

735 
by (induct xs) auto 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

736 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

737 
lemma map_fst_zip[simp]: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

738 
"length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

739 
by (induct rule:list_induct2, simp_all) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

740 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

741 
lemma map_snd_zip[simp]: 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

742 
"length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

743 
by (induct rule:list_induct2, simp_all) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

744 

78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

745 

15392  746 
subsubsection {* @{text rev} *} 
13114  747 

13142  748 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  749 
by (induct xs) auto 
13114  750 

13142  751 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  752 
by (induct xs) auto 
13114  753 

15870  754 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
755 
by auto 

756 

13142  757 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  758 
by (induct xs) auto 
13114  759 

13142  760 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  761 
by (induct xs) auto 
13114  762 

15870  763 
lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])" 
764 
by (cases xs) auto 

765 

766 
lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])" 

767 
by (cases xs) auto 

768 

21061
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

769 
lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)" 
580dfc999ef6
added normal post setup; cleaned up "execution" constants
haftmann
parents:
21046
diff
changeset

770 
apply (induct xs arbitrary: ys, force) 
14208  771 
apply (case_tac ys, simp, force) 
13145  772 
done 
13114  773 

15439  774 
lemma inj_on_rev[iff]: "inj_on rev A" 
775 
by(simp add:inj_on_def) 

776 

13366  777 
lemma rev_induct [case_names Nil snoc]: 
778 
"[ P []; !!x xs. P xs ==> P (xs @ [x]) ] ==> P xs" 

15489
d136af442665
Replaced application of subst by simplesubst in proof of rev_induct
berghofe
parents:
15439
diff
changeset

779 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  780 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
781 
done 

13114  782 

13366  783 
lemma rev_exhaust [case_names Nil snoc]: 
784 
"(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P" 

13145  785 
by (induct xs rule: rev_induct) auto 
13114  786 

13366  787 
lemmas rev_cases = rev_exhaust 
788 

18423  789 
lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" 
790 
by(rule rev_cases[of xs]) auto 

791 

13114  792 

15392  793 
subsubsection {* @{text set} *} 
13114  794 

13142  795 
lemma finite_set [iff]: "finite (set xs)" 
13145  796 
by (induct xs) auto 
13114  797 

13142  798 
lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)" 
13145  799 
by (induct xs) auto 
13114  800 

17830  801 
lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs" 
802 
by(cases xs) auto 

14099  803 

13142  804 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  805 
by auto 
13114  806 

14099  807 
lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
808 
by auto 

809 

13142  810 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  811 
by (induct xs) auto 
13114  812 

15245  813 
lemma set_empty2[iff]: "({} = set xs) = (xs = [])" 
814 
by(induct xs) auto 

815 

13142  816 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  817 
by (induct xs) auto 
13114  818 

13142  819 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  820 
by (induct xs) auto 
13114  821 

13142  822 
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}" 
13145  823 
by (induct xs) auto 
13114  824 

15425  825 
lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}" 
14208  826 
apply (induct j, simp_all) 
827 
apply (erule ssubst, auto) 

13145  828 
done 
13114  829 

13142  830 
lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)" 
15113  831 
proof (induct xs) 
832 
case Nil show ?case by simp 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

833 
next 
15113  834 
case (Cons a xs) 
835 
show ?case 

836 
proof 

837 
assume "x \<in> set (a # xs)" 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

838 
with Cons show "\<exists>ys zs. a # xs = ys @ x # zs" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

839 
by (auto intro: Cons_eq_appendI) 
15113  840 
next 
841 
assume "\<exists>ys zs. a # xs = ys @ x # zs" 

842 
then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast 

843 
show "x \<in> set (a # xs)" 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

844 
by (cases ys) (auto simp add: eq) 
15113  845 
qed 
846 
qed 

13142  847 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

848 
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

849 
by (rule in_set_conv_decomp [THEN iffD1]) 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

850 

18049  851 
lemma in_set_conv_decomp_first: 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

852 
"(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)" 
18049  853 
proof (induct xs) 
854 
case Nil show ?case by simp 

855 
next 

856 
case (Cons a xs) 

857 
show ?case 

858 
proof cases 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

859 
assume "x = a" thus ?case using Cons by fastsimp 
18049  860 
next 
861 
assume "x \<noteq> a" 

862 
show ?case 

863 
proof 

864 
assume "x \<in> set (a # xs)" 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

865 
with Cons and `x \<noteq> a` show "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

866 
by (fastsimp intro!: Cons_eq_appendI) 
18049  867 
next 
868 
assume "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys" 

869 
then obtain ys zs where eq: "a # xs = ys @ x # zs" by blast 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

870 
show "x \<in> set (a # xs)" by (cases ys) (auto simp add: eq) 
18049  871 
qed 
872 
qed 

873 
qed 

874 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

875 
lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

876 
by (rule in_set_conv_decomp_first [THEN iffD1]) 
18049  877 

878 

13508  879 
lemma finite_list: "finite A ==> EX l. set l = A" 
880 
apply (erule finite_induct, auto) 

881 
apply (rule_tac x="x#l" in exI, auto) 

882 
done 

883 

14388  884 
lemma card_length: "card (set xs) \<le> length xs" 
885 
by (induct xs) (auto simp add: card_insert_if) 

13114  886 

15168  887 

15392  888 
subsubsection {* @{text filter} *} 
13114  889 

13142  890 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  891 
by (induct xs) auto 
13114  892 

15305  893 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
894 
by (induct xs) simp_all 

895 

13142  896 
lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs" 
13145  897 
by (induct xs) auto 
13114  898 

16998  899 
lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" 
900 
by (induct xs) (auto simp add: le_SucI) 

901 

18423  902 
lemma sum_length_filter_compl: 
903 
"length(filter P xs) + length(filter (%x. ~P x) xs) = length xs" 

904 
by(induct xs) simp_all 

905 

13142  906 
lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs" 
13145  907 
by (induct xs) auto 
13114  908 

13142  909 
lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []" 
13145  910 
by (induct xs) auto 
13114  911 

16998  912 
lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
24349  913 
by (induct xs) simp_all 
16998  914 

915 
lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)" 

916 
apply (induct xs) 

917 
apply auto 

918 
apply(cut_tac P=P and xs=xs in length_filter_le) 

919 
apply simp 

920 
done 

13114  921 

16965  922 
lemma filter_map: 
923 
"filter P (map f xs) = map f (filter (P o f) xs)" 

924 
by (induct xs) simp_all 

925 

926 
lemma length_filter_map[simp]: 

927 
"length (filter P (map f xs)) = length(filter (P o f) xs)" 

928 
by (simp add:filter_map) 

929 

13142  930 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  931 
by auto 
13114  932 

15246  933 
lemma length_filter_less: 
934 
"\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs" 

935 
proof (induct xs) 

936 
case Nil thus ?case by simp 

937 
next 

938 
case (Cons x xs) thus ?case 

939 
apply (auto split:split_if_asm) 

940 
using length_filter_le[of P xs] apply arith 

941 
done 

942 
qed 

13114  943 

15281  944 
lemma length_filter_conv_card: 
945 
"length(filter p xs) = card{i. i < length xs & p(xs!i)}" 

946 
proof (induct xs) 

947 
case Nil thus ?case by simp 

948 
next 

949 
case (Cons x xs) 

950 
let ?S = "{i. i < length xs & p(xs!i)}" 

951 
have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite) 

952 
show ?case (is "?l = card ?S'") 

953 
proof (cases) 

954 
assume "p x" 

955 
hence eq: "?S' = insert 0 (Suc ` ?S)" 

25162  956 
by(auto simp: image_def split:nat.split dest:gr0_implies_Suc) 
15281  957 
have "length (filter p (x # xs)) = Suc(card ?S)" 
23388  958 
using Cons `p x` by simp 
15281  959 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 
960 
by (simp add: card_image inj_Suc) 

961 
also have "\<dots> = card ?S'" using eq fin 

962 
by (simp add:card_insert_if) (simp add:image_def) 

963 
finally show ?thesis . 

964 
next 

965 
assume "\<not> p x" 

966 
hence eq: "?S' = Suc ` ?S" 

25162  967 
by(auto simp add: image_def split:nat.split elim:lessE) 
15281  968 
have "length (filter p (x # xs)) = card ?S" 
23388  969 
using Cons `\<not> p x` by simp 
15281  970 
also have "\<dots> = card(Suc ` ?S)" using fin 
971 
by (simp add: card_image inj_Suc) 

972 
also have "\<dots> = card ?S'" using eq fin 

973 
by (simp add:card_insert_if) 

974 
finally show ?thesis . 

975 
qed 

976 
qed 

977 

17629  978 
lemma Cons_eq_filterD: 
979 
"x#xs = filter P ys \<Longrightarrow> 

980 
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs" 

19585  981 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  982 
proof(induct ys) 
983 
case Nil thus ?case by simp 

984 
next 

985 
case (Cons y ys) 

986 
show ?case (is "\<exists>x. ?Q x") 

987 
proof cases 

988 
assume Py: "P y" 

989 
show ?thesis 

990 
proof cases 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

991 
assume "x = y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

992 
with Py Cons.prems have "?Q []" by simp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

993 
then show ?thesis .. 
17629  994 
next 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

995 
assume "x \<noteq> y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

996 
with Py Cons.prems show ?thesis by simp 
17629  997 
qed 
998 
next 

25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

999 
assume "\<not> P y" 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1000 
with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1001 
then have "?Q (y#us)" by simp 
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1002 
then show ?thesis .. 
17629  1003 
qed 
1004 
qed 

1005 

1006 
lemma filter_eq_ConsD: 

1007 
"filter P ys = x#xs \<Longrightarrow> 

1008 
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs" 

1009 
by(rule Cons_eq_filterD) simp 

1010 

1011 
lemma filter_eq_Cons_iff: 

1012 
"(filter P ys = x#xs) = 

1013 
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" 

1014 
by(auto dest:filter_eq_ConsD) 

1015 

1016 
lemma Cons_eq_filter_iff: 

1017 
"(x#xs = filter P ys) = 

1018 
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" 

1019 
by(auto dest:Cons_eq_filterD) 

1020 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19623
diff
changeset

1021 
lemma filter_cong[fundef_cong, recdef_cong]: 
17501  1022 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys" 
1023 
apply simp 

1024 
apply(erule thin_rl) 

1025 
by (induct ys) simp_all 

1026 

15281  1027 

15392  1028 
subsubsection {* @{text concat} *} 
13114  1029 

13142  1030 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  1031 
by (induct xs) auto 
13114  1032 

18447  1033 
lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" 
13145  1034 
by (induct xss) auto 
13114  1035 

18447  1036 
lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" 
13145  1037 
by (induct xss) auto 
13114  1038 

24308  1039 
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)" 
13145  1040 
by (induct xs) auto 
13114  1041 

24476
f7ad9fbbeeaa
turned list comprehension translations into ML to optimize base case
nipkow
parents:
24471
diff
changeset

1042 
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" 
24349  1043 
by (induct xs) auto 
1044 

13142  1045 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  1046 
by (induct xs) auto 
13114  1047 

13142  1048 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  1049 
by (induct xs) auto 
13114  1050 

13142  1051 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  1052 
by (induct xs) auto 
13114  1053 

1054 

15392  1055 
subsubsection {* @{text nth} *} 
13114  1056 

13142  1057 
lemma nth_Cons_0 [simp]: "(x # xs)!0 = x" 
13145  1058 
by auto 
13114  1059 

13142  1060 
lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n" 
13145  1061 
by auto 
13114  1062 

13142  1063 
declare nth.simps [simp del] 
13114  1064 

1065 
lemma nth_append: 

24526  1066 
"(xs @ ys)!n = (if n < length xs then xs!n else ys!(n  length xs))" 
1067 
apply (induct xs arbitrary: n, simp) 

14208  1068 
apply (case_tac n, auto) 
13145  1069 
done 
13114  1070 

14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1071 
lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x" 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1072 
by (induct xs) auto 
14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1073 

4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1074 
lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n" 
25221
5ded95dda5df
append/member: more lightweight way to declare authentic syntax;
wenzelm
parents:
25215
diff
changeset

1075 
by (induct xs) auto 
14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1076 

24526  1077 
lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)" 
1078 
apply (induct xs arbitrary: n, simp) 

14208  1079 
apply (case_tac n, auto) 
13145  1080 
done 
13114  1081 

18423  1082 
lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0" 
1083 
by(cases xs) simp_all 

1084 

18049  1085 

1086 
lemma list_eq_iff_nth_eq: 

24526  1087 
"(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))" 
1088 
apply(induct xs arbitrary: ys) 

24632  1089 
apply force 
18049  1090 
apply(case_tac ys) 
1091 
apply simp 

1092 
apply(simp add:nth_Cons split:nat.split)apply blast 

1093 
done 

1094 

13142  1095 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1096 
apply (induct xs, simp, simp) 
13145  1097 
apply safe 
24632  1098 
apply (metis nat_case_0 nth.simps zero_less_Suc) 
1099 
apply (metis less_Suc_eq_0_disj nth_Cons_Suc) 

14208  1100 
apply (case_tac i, simp) 
24632  1101 
apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff) 
13145  1102 
done 
13114  1103 

17501  1104 
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)" 
1105 
by(auto simp:set_conv_nth) 

1106 

13145  1107 
lemma list_ball_nth: "[ n < length xs; !x : set xs. P x] ==> P(xs!n)" 
1108 
by (auto simp add: set_conv_nth) 

13114  1109 

13142  1110 
lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs" 
13145  1111 
by (auto simp add: set_conv_nth) 
13114  1112 

1113 
lemma all_nth_imp_all_set: 

13145  1114 
"[ !i < length xs. P(xs!i); x : set xs] ==> P x" 
1115 
by (auto simp add: set_conv_nth) 

13114  1116 

1117 
lemma all_set_conv_all_nth: 

13145  1118 
"(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs > P (xs ! i))" 
1119 
by (auto simp add: set_conv_nth) 

13114  1120 

25296  1121 
lemma rev_nth: 
1122 
"n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs  Suc n)" 

1123 
proof (induct xs arbitrary: n) 

1124 
case Nil thus ?case by simp 

1125 
next 

1126 
case (Cons x xs) 

1127 
hence n: "n < Suc (length xs)" by simp 

1128 
moreover 

1129 
{ assume "n < length xs" 

1130 
with n obtain n' where "length xs  n = Suc n'" 

1131 
by (cases "length xs  n", auto) 

1132 
moreover 

1133 
then have "length xs  Suc n = n'" by simp 

1134 
ultimately 

1135 
have "xs ! (length xs  Suc n) = (x # xs) ! (length xs  n)" by simp 

1136 
} 

1137 
ultimately 

1138 
show ?case by (clarsimp simp add: Cons nth_append) 

1139 
qed 

13114  1140 

15392  1141 
subsubsection {* @{text list_update} *} 
13114  1142 

24526  1143 
lemma length_list_update [simp]: "length(xs[i:=x]) = length xs" 
1144 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1145 

1146 
lemma nth_list_update: 

24526  1147 
"i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)" 
1148 
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split) 

13114  1149 

13142  1150 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  1151 
by (simp add: nth_list_update) 
13114  1152 

24526  1153 
lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j" 
1154 
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split) 

13114  1155 

13142  1156 
lemma list_update_overwrite [simp]: 
24526  1157 
"i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]" 
1158 
by (induct xs arbitrary: i) (auto split: nat.split) 

1159 

1160 
lemma list_update_id[simp]: "xs[i := xs!i] = xs" 

1161 
by (induct xs arbitrary: i) (simp_all split:nat.splits) 

1162 

1163 
lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs" 

1164 
apply (induct xs arbitrary: i) 

17501  1165 
apply simp 
1166 
apply (case_tac i) 

1167 
apply simp_all 

1168 
done 

1169 

13114  1170 
lemma list_update_same_conv: 
24526  1171 
"i < length xs ==> (xs[i := x] = xs) = (xs!i = x)" 
1172 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1173 

14187  1174 
lemma list_update_append1: 
24526  1175 
"i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys" 
1176 
apply (induct xs arbitrary: i, simp) 

14187  1177 
apply(simp split:nat.split) 
1178 
done 

1179 

15868  1180 
lemma list_update_append: 
24526  1181 
"(xs @ ys) [n:= x] = 
15868  1182 
(if n < length xs then xs[n:= x] @ ys else xs @ (ys [nlength xs:= x]))" 
24526  1183 
by (induct xs arbitrary: n) (auto split:nat.splits) 
15868  1184 

14402
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1185 
lemma list_update_length [simp]: 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1186 
"(xs @ x # ys)[length xs := y] = (xs @ y # ys)" 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1187 
by (induct xs, auto) 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

1188 

13114  1189 
lemma update_zip: 
24526  1190 
"length xs = length ys ==> 
1191 
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" 

1192 
by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split) 

1193 

1194 
lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)" 

1195 
by (induct xs arbitrary: i) (auto split: nat.split) 

13114  1196 

1197 
lemma set_update_subsetI: "[ set xs <= A; x:A ] ==> set(xs[i := x]) <= A" 

13145  1198 
by (blast dest!: set_update_subset_insert [THEN subsetD]) 
13114  1199 

24526  1200 
lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])" 
1201 
by (induct xs arbitrary: n) (auto split:nat.splits) 

15868  1202 

24796  1203 
lemma list_update_overwrite: 
1204 
"xs [i := x, i := y] = xs [i := y]" 

1205 
apply (induct xs arbitrary: i) 

1206 
apply simp 

1207 
apply (case_tac i) 

1208 
apply simp_all 

1209 
done 

1210 

1211 
lemma list_update_swap: 

1212 
"i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]" 

1213 
apply (induct xs arbitrary: i i') 

1214 
apply simp 

1215 
apply (case_tac i, case_tac i') 

1216 
apply auto 

1217 
apply (case_tac i') 

1218 
apply auto 

1219 
done 

1220 

13114  1221 

15392  1222 
subsubsection {* @{text last} and @{text butlast} *} 
13114  1223 

13142  1224 
lemma last_snoc [simp]: "last (xs @ [x]) = x" 
13145  1225 
by (induct xs) auto 
13114  1226 

13142  1227 
lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs" 
13145  1228 
by (induct xs) auto 
13114  1229 

14302  1230 
lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x" 
1231 
by(simp add:last.simps) 

1232 

1233 
lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs" 

1234 
by(simp add:last.simps) 

1235 

1236 
lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)" 

1237 
by (induct xs) (auto) 

1238 

1239 
lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs" 

1240 
by(simp add:last_append) 

1241 

1242 
lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys" 

1243 
by(simp add:last_append) 

1244 

17762  1245 
lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs" 
1246 
by(rule rev_exhaust[of xs]) simp_all 

1247 

1248 
lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs" 

1249 
by(cases xs) simp_all 

1250 

17765  1251 
lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as" 
1252 
by (induct as) auto 

17762  1253 

13142  1254 
lemma length_butlast [simp]: "length (butlast xs) = length xs  1" 
13145  1255 
by (induct xs rule: rev_induct) auto 
13114  1256 

1257 
lemma butlast_append: 

24526  1258 
"butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)" 
1259 
by (induct xs arbitrary: ys) auto 

13114  1260 

13142  1261 
lemma append_butlast_last_id [simp]: 
13145  1262 
"xs \<noteq> [] ==> butlast xs @ [last xs] = xs" 
1263 
by (induct xs) auto 

13114  1264 

13142  1265 
lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs" 
13145  1266 
by (induct xs) (auto split: split_if_asm) 
13114  1267 

1268 
lemma in_set_butlast_appendI: 

13145  1269 
"x : set (butlast xs)  x : set (butlast ys) ==> x : set (butlast (xs @ ys))" 
1270 
by (auto dest: in_set_butlastD simp add: butlast_append) 

13114  1271 

24526  1272 
lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs" 
1273 
apply (induct xs arbitrary: n) 

17501  1274 
apply simp 
1275 
apply (auto split:nat.split) 

1276 
done 

1277 

17589  1278 
lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs  1)" 
1279 
by(induct xs)(auto simp:neq_Nil_conv) 

1280 

24796  1281 

15392  1282 
subsubsection {* @{text take} and @{text drop} *} 
13114  1283 

13142  1284 
lemma take_0 [simp]: "take 0 xs = []" 
13145  1285 
by (induct xs) auto 
13114  1286 

13142  1287 
lemma drop_0 [simp]: "drop 0 xs = xs" 
13145  1288 
by (induct xs) auto 
13114  1289 

13142  1290 
lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs" 
13145  1291 
by simp 
13114  1292 

13142  1293 
lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs" 
13145  1294 
by simp 
13114  1295 

13142  1296 
declare take_Cons [simp del] and drop_Cons [simp del] 
13114  1297 

15110
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

1298 
lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

1299 
by(clarsimp simp add:neq_Nil_conv) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

1300 

14187  1301 
lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)" 
1302 
by(cases xs, simp_all) 

1303 

24526  1304 
lemma drop_tl: "drop n (tl xs) = tl(drop n xs)" 
1305 
by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split) 

1306 

1307 
lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y" 

1308 
apply (induct xs arbitrary: n, simp) 

14187  1309 
apply(simp add:drop_Cons nth_Cons split:nat.splits) 
1310 
done 

1311 

13913  1312 
lemma take_Suc_conv_app_nth: 
24526  1313 
"i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]" 
1314 
apply (induct xs arbitrary: i, simp) 

14208  1315 
apply (case_tac i, auto) 
13913  1316 
done 
1317 

14591  1318 
lemma drop_Suc_conv_tl: 
24526  1319 
"i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs" 
1320 
apply (induct xs arbitrary: i, simp) 

14591  1321 
apply (case_tac i, auto) 
1322 
done 

1323 

24526  1324 
lemma length_take [simp]: "length (take n xs) = min (length xs) n" 
1325 
by (induct n arbitrary: xs) (auto, case_tac xs, auto) 

1326 

1327 
lemma length_drop [simp]: "length (drop n xs) = (length xs  n)" 

1328 
by (induct n arbitrary: xs) (auto, case_tac xs, auto) 

1329 

1330 
lemma take_all [simp]: "length xs <= n ==> take n xs = xs" 

1331 
by (induct n arbitrary: xs) (auto, case_tac xs, auto) 

1332 

1333 
lemma drop_all [simp]: "length xs <= n ==> drop n xs = []" 

1334 
by (induct n arbitrary: xs) (auto, case_tac xs, auto) 

13114  1335 

13142  1336 
lemma take_append [simp]: 
24526  1337 
"take n (xs @ ys) = (take n xs @ take (n  length xs) ys)" 
1338 
by (induct n arbitrary: xs) (auto, case_tac xs, auto) 

13114  1339 

13142  1340 
lemma drop_append [simp]: 
24526 