author  paulson 
Wed, 15 Aug 2007 12:52:56 +0200  
changeset 24286  7619080e49f0 
parent 24219  e558fe311376 
child 24308  700e745994c1 
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" 
23554  11 
("Tools/function_package/lexicographic_order.ML") 
12 
("Tools/function_package/fundef_datatype.ML") 

15131  13 
begin 
923  14 

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

923  18 

15392  19 
subsection{*Basic list processing functions*} 
15302  20 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

43 
remove1 :: "'a => 'a list => 'a list" 
13366  44 
"distinct":: "'a list => bool" 
45 
replicate :: "nat => 'a => 'a list" 

19390  46 
splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 
22830  47 
allpairs :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" 
15302  48 

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

50 
upto:: "nat => nat => nat list" ("(1[_../_])") where 
19363  51 
"[i..j] == [i..<(Suc j)]" 
19302  52 

923  53 

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

55 

923  56 
syntax 
13366  57 
 {* list Enumeration *} 
58 
"@list" :: "args => 'a list" ("[(_)]") 

923  59 

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

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

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

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

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

67 
"_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

68 

923  69 
translations 
13366  70 
"[x, xs]" == "x#[xs]" 
71 
"[x]" == "x#[]" 

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

72 
"[x<xs . P]"== "filter (%x. P) xs" 
923  73 

13366  74 
"_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs" 
75 
"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

76 

5427  77 

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

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

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

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

82 

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

83 

13142  84 
text {* 
14589  85 
Function @{text size} is overloaded for all datatypes. Users may 
13366  86 
refer to the list version as @{text length}. *} 
13142  87 

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

89 
length :: "'a list => nat" where 
19363  90 
"length == size" 
15302  91 

5183  92 
primrec 
15307  93 
"hd(x#xs) = x" 
94 

5183  95 
primrec 
15307  96 
"tl([]) = []" 
97 
"tl(x#xs) = xs" 

98 

5183  99 
primrec 
15307  100 
"last(x#xs) = (if xs=[] then x else last xs)" 
101 

5183  102 
primrec 
15307  103 
"butlast []= []" 
104 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 

105 

5183  106 
primrec 
15307  107 
"set [] = {}" 
108 
"set (x#xs) = insert x (set xs)" 

109 

5183  110 
primrec 
15307  111 
"map f [] = []" 
112 
"map f (x#xs) = f(x)#map f xs" 

113 

23235  114 
function (*authentic syntax for append  revert to primrec 
115 
as soon as "authentic" primrec is available*) 

116 
append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) 

117 
where 

118 
append_Nil: "[] @ ys = ys" 

119 
 append_Cons: "(x # xs) @ ys = x # (xs @ ys)" 

120 
by (auto, case_tac a, auto) 

121 
termination by (relation "measure (size o fst)") auto 

15307  122 

5183  123 
primrec 
15307  124 
"rev([]) = []" 
125 
"rev(x#xs) = rev(xs) @ [x]" 

126 

5183  127 
primrec 
15307  128 
"filter P [] = []" 
129 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 

130 

5183  131 
primrec 
15307  132 
foldl_Nil:"foldl f a [] = a" 
133 
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" 

134 

8000  135 
primrec 
15307  136 
"foldr f [] a = a" 
137 
"foldr f (x#xs) a = f x (foldr f xs a)" 

138 

5183  139 
primrec 
15307  140 
"concat([]) = []" 
141 
"concat(x#xs) = x @ concat(xs)" 

142 

5183  143 
primrec 
23096  144 
"listsum [] = 0" 
145 
"listsum (x # xs) = x + listsum xs" 

146 

147 
primrec 

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

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

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

152 

5183  153 
primrec 
15307  154 
take_Nil:"take n [] = []" 
155 
take_Cons: "take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs)" 

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

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

158 

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

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

163 

5183  164 
primrec 
15307  165 
"[][i:=v] = []" 
166 
"(x#xs)[i:=v] = (case i of 0 => v # xs  Suc j => x # xs[j:=v])" 

167 

168 
primrec 

169 
"takeWhile P [] = []" 

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

171 

5183  172 
primrec 
15307  173 
"dropWhile P [] = []" 
174 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 

175 

5183  176 
primrec 
15307  177 
"zip xs [] = []" 
178 
zip_Cons: "zip xs (y#ys) = (case xs of [] => []  z#zs => (z,y)#zip zs ys)" 

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

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

181 

5427  182 
primrec 
15425  183 
upt_0: "[i..<0] = []" 
184 
upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

15307  185 

5183  186 
primrec 
15307  187 
"distinct [] = True" 
188 
"distinct (x#xs) = (x ~: set xs \<and> distinct xs)" 

189 

5183  190 
primrec 
15307  191 
"remdups [] = []" 
192 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

193 

5183  194 
primrec 
15307  195 
"remove1 x [] = []" 
196 
"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" 

197 

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

198 
primrec 
15307  199 
replicate_0: "replicate 0 x = []" 
200 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

201 

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

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

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

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

205 

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

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

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

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

209 

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

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

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

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

213 
(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

214 

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

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

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

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

219 
primrec 

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

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

221 
"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

222 
 {*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

223 

22828  224 
primrec 
22830  225 
"allpairs f [] ys = []" 
226 
"allpairs f (x # xs) ys = map (f x) ys @ allpairs f xs ys" 

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

227 

23388  228 
subsubsection {* List comprehension *} 
23192  229 

23209  230 
text{* Input syntax for Haskelllike list comprehension 
231 
notation. Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"}, the list of all pairs of distinct elements from @{text xs} and @{text ys}. 

232 

23240  233 
There are two differences to Haskell. The general synatx is 
234 
@{text"[e. p \<leftarrow> xs, \<dots>]"} rather than \verb![x x < xs, ...]!. Patterns in 

235 
generators can only be tuples (at the moment). 

236 

237 
To avoid misunderstandings, the translation is not reversed upon 

238 
output. You can add the inverse translations in your own theory if you 

239 
desire. 

240 

241 
Hint: formulae containing complex list comprehensions may become quite 

242 
unreadable after the simplifier has finished with them. It can be 

243 
helpful to introduce definitions for such list comprehensions and 

244 
treat them separately in suitable lemmas. 

23209  245 
*} 
246 
(* 

23240  247 
Proper theorem proving support would be nice. For example, if 
23192  248 
@{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"} 
249 
produced something like 

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

252 

23240  253 
nonterminals lc_qual lc_quals 
23192  254 

255 
syntax 

23240  256 
"_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __") 
257 
"_lc_gen" :: "pttrn \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ < _") 

258 
"_lc_test" :: "bool \<Rightarrow> lc_qual" ("_") 

259 
"_lc_end" :: "lc_quals" ("]") 

260 
"_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __") 

23192  261 

262 
translations 

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

263 
"[e. p<xs]" => "map (%p. e) xs" 
23240  264 
"_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)" 
265 
=> "concat (map (%p. _listcompr e Q Qs) xs)" 

266 
"[e. P]" => "if P then [e] else []" 

267 
"_listcompr e (_lc_test P) (_lc_quals Q Qs)" 

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

269 

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

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

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

272 
syntax (HTML output) 
e39dd93161d9
tuned list comprehension, changed filter syntax from : to <
nipkow
parents:
23246
diff
changeset

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

274 

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

275 

23240  276 
(* 
277 
term "[(x,y,z). b]" 

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

279 
term "[(x,y,z). x<a, x>b]" 

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

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

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

283 
term "[(x,y,z). x<a, x>b, x=d]" 

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

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

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

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

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

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

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

23192  291 
*) 
292 

23240  293 

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

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

295 

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

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

297 
"xs \<noteq> x # xs" 
13145  298 
by (induct xs) auto 
13114  299 

13142  300 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  301 

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

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

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

309 

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

310 
subsubsection {* @{const length} *} 
13114  311 

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

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

314 
append_eq_append_conv}. 
13142  315 
*} 
13114  316 

13142  317 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  318 
by (induct xs) auto 
13114  319 

13142  320 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  321 
by (induct xs) auto 
13114  322 

13142  323 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  324 
by (induct xs) auto 
13114  325 

13142  326 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  327 
by (cases xs) auto 
13114  328 

22828  329 
lemma length_allpairs[simp]: 
22830  330 
"length(allpairs f xs ys) = length xs * length ys" 
22828  331 
by(induct xs) auto 
332 

13142  333 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  334 
by (induct xs) auto 
13114  335 

13142  336 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  337 
by (induct xs) auto 
13114  338 

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

341 

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

13142  345 

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

14208  348 
apply (induct xs, simp, simp) 
14025  349 
apply blast 
350 
done 

351 

14099  352 
lemma impossible_Cons [rule_format]: 
353 
"length xs <= length ys > xs = x # ys = False" 

20503  354 
apply (induct xs) 
355 
apply auto 

14099  356 
done 
357 

14247  358 
lemma list_induct2[consumes 1]: "\<And>ys. 
359 
\<lbrakk> length xs = length ys; 

360 
P [] []; 

361 
\<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> 

362 
\<Longrightarrow> P xs ys" 

363 
apply(induct xs) 

364 
apply simp 

365 
apply(case_tac ys) 

366 
apply simp 

367 
apply(simp) 

368 
done 

13114  369 

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

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

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

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

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

374 
\<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

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

376 
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

377 

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

378 
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" 
24037  379 
by (rule Eq_FalseI) auto 
380 

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

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

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

383 
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

384 
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

385 
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

386 
*) 
24037  387 

388 
let 

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

389 

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

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

391 
 len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1) 
23029  392 
 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

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

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

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

396 

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

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

400 
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

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

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

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

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

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

407 
val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len 
22633  408 
(K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1)); 
409 
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

410 
in 
23214  411 
if m < n andalso submultiset (op aconv) (ls,rs) orelse 
412 
n < m andalso submultiset (op aconv) (rs,ls) 

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

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

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

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

417 

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

418 

15392  419 
subsubsection {* @{text "@"}  append *} 
13114  420 

13142  421 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  422 
by (induct xs) auto 
13114  423 

13142  424 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  425 
by (induct xs) auto 
3507  426 

13142  427 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  428 
by (induct xs) auto 
13114  429 

13142  430 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  431 
by (induct xs) auto 
13114  432 

13142  433 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  434 
by (induct xs) auto 
13114  435 

13142  436 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  437 
by (induct xs) auto 
13114  438 

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

439 
lemma append_eq_append_conv [simp,noatp]: 
13883
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

440 
"!!ys. length xs = length ys \<or> length us = length vs 
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

441 
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)" 
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

442 
apply (induct xs) 
14208  443 
apply (case_tac ys, simp, force) 
444 
apply (case_tac ys, force, simp) 

13145  445 
done 
13142  446 

14495  447 
lemma append_eq_append_conv2: "!!ys zs ts. 
448 
(xs @ ys = zs @ ts) = 

449 
(EX us. xs = zs @ us & us @ ys = ts  xs @ us = zs & ys = us@ ts)" 

450 
apply (induct xs) 

451 
apply fastsimp 

452 
apply(case_tac zs) 

453 
apply simp 

454 
apply fastsimp 

455 
done 

456 

13142  457 
lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  458 
by simp 
13142  459 

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

13145  461 
by simp 
13114  462 

13142  463 
lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  464 
by simp 
13114  465 

13142  466 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  467 
using append_same_eq [of _ _ "[]"] by auto 
3507  468 

13142  469 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  470 
using append_same_eq [of "[]"] by auto 
13114  471 

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

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

13142  475 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  476 
by (induct xs) auto 
13114  477 

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

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

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

487 

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

490 
by(cases ys) auto 

491 

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

494 
by(cases ys) auto 

495 

14300  496 

13142  497 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  498 

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

13145  500 
by simp 
13114  501 

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

13114  505 

13142  506 
lemma append_eq_appendI: 
13145  507 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
508 
by (drule sym) simp 

13114  509 

510 

13142  511 
text {* 
13145  512 
Simplification procedure for all list equalities. 
513 
Currently only tries to rearrange @{text "@"} to see if 

514 
 both lists end in a singleton list, 

515 
 or both lists end in the same list. 

13142  516 
*} 
517 

518 
ML_setup {* 

3507  519 
local 
520 

13114  521 
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = 
13462  522 
(case xs of Const("List.list.Nil",_) => cons  _ => last xs) 
23029  523 
 last (Const("List.append",_) $ _ $ ys) = last ys 
13462  524 
 last t = t; 
13114  525 

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

13462  527 
 list1 _ = false; 
13114  528 

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

13462  530 
(case xs of Const("List.list.Nil",_) => xs  _ => cons $ butlast xs) 
23029  531 
 butlast ((app as Const("List.append",_) $ xs) $ ys) = app $ butlast ys 
13462  532 
 butlast xs = Const("List.list.Nil",fastype_of xs); 
13114  533 

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

16973  536 

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

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

540 
fun rearr conv = 

541 
let 

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

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

544 
val appT = [listT,listT] > listT 

23029  545 
val app = Const("List.append",appT) 
13462  546 
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

547 
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

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

549 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  550 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  551 

13462  552 
in 
22633  553 
if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv} 
554 
else if lastl aconv lastr then rearr @{thm append_same_eq} 

15531  555 
else NONE 
13462  556 
end; 
557 

13114  558 
in 
13462  559 

560 
val list_eq_simproc = 

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

13114  563 
end; 
564 

565 
Addsimprocs [list_eq_simproc]; 

566 
*} 

567 

568 

15392  569 
subsubsection {* @{text map} *} 
13114  570 

13142  571 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  572 
by (induct xs) simp_all 
13114  573 

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

13142  577 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  578 
by (induct xs) auto 
13114  579 

13142  580 
lemma map_compose: "map (f o g) xs = map f (map g xs)" 
13145  581 
by (induct xs) (auto simp add: o_def) 
13114  582 

13142  583 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  584 
by (induct xs) auto 
13114  585 

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

588 

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

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

13737  592 
by simp 
13114  593 

13142  594 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  595 
by (cases xs) auto 
13114  596 

13142  597 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  598 
by (cases xs) auto 
13114  599 

18447  600 
lemma map_eq_Cons_conv: 
14025  601 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 
13145  602 
by (cases xs) auto 
13114  603 

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

607 

18447  608 
lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] 
609 
lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] 

610 
declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!] 

611 

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

18447  614 
by(induct ys, auto simp add: Cons_eq_map_conv) 
14111  615 

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

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

617 
"!!xs. map f xs = map f ys ==> length xs = length ys" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

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

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

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

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

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

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

625 

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

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

627 
"[ 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

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

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

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

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

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

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

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

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

636 

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

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

638 
"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

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

640 

13114  641 
lemma map_injective: 
14338  642 
"!!xs. map f xs = map f ys ==> inj f ==> xs = ys" 
643 
by (induct ys) (auto dest!:injD) 

13114  644 

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

647 

13114  648 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  649 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  650 

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

14208  652 
apply (unfold inj_on_def, clarify) 
13145  653 
apply (erule_tac x = "[x]" in ballE) 
14208  654 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  655 
apply blast 
656 
done 

13114  657 

14339  658 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  659 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  660 

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

663 
apply(erule map_inj_on) 

664 
apply(blast intro:inj_onI dest:inj_onD) 

665 
done 

666 

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

13114  669 

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

670 
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

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

672 

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

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

674 
"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

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

676 

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

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

678 
"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

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

680 

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

681 

15392  682 
subsubsection {* @{text rev} *} 
13114  683 

13142  684 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  685 
by (induct xs) auto 
13114  686 

13142  687 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  688 
by (induct xs) auto 
13114  689 

15870  690 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
691 
by auto 

692 

13142  693 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  694 
by (induct xs) auto 
13114  695 

13142  696 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  697 
by (induct xs) auto 
13114  698 

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

701 

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

703 
by (cases xs) auto 

704 

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

705 
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

706 
apply (induct xs arbitrary: ys, force) 
14208  707 
apply (case_tac ys, simp, force) 
13145  708 
done 
13114  709 

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

712 

13366  713 
lemma rev_induct [case_names Nil snoc]: 
714 
"[ 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

715 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  716 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
717 
done 

13114  718 

13145  719 
ML {* val rev_induct_tac = induct_thm_tac (thm "rev_induct") *} "compatibility" 
13114  720 

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

13145  723 
by (induct xs rule: rev_induct) auto 
13114  724 

13366  725 
lemmas rev_cases = rev_exhaust 
726 

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

729 

13114  730 

15392  731 
subsubsection {* @{text set} *} 
13114  732 

13142  733 
lemma finite_set [iff]: "finite (set xs)" 
13145  734 
by (induct xs) auto 
13114  735 

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

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

14099  741 

13142  742 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  743 
by auto 
13114  744 

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

747 

13142  748 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  749 
by (induct xs) auto 
13114  750 

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

753 

13142  754 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  755 
by (induct xs) auto 
13114  756 

13142  757 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  758 
by (induct xs) auto 
13114  759 

24166  760 
lemma set_allpairs [simp]: 
22830  761 
"set(allpairs f xs ys) = {z. EX x : set xs. EX y : set ys. z = f x y}" 
24166  762 
by (induct xs) auto 
22828  763 

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

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

13145  770 
done 
13114  771 

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

775 
case (Cons a xs) 

776 
show ?case 

777 
proof 

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

779 
with prems show "\<exists>ys zs. a # xs = ys @ x # zs" 

780 
by (simp, blast intro: Cons_eq_appendI) 

781 
next 

782 
assume "\<exists>ys zs. a # xs = ys @ x # zs" 

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

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

785 
by (cases ys, auto simp add: eq) 

786 
qed 

787 
qed 

13142  788 

18049  789 
lemma in_set_conv_decomp_first: 
790 
"(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)" 

791 
proof (induct xs) 

792 
case Nil show ?case by simp 

793 
next 

794 
case (Cons a xs) 

795 
show ?case 

796 
proof cases 

797 
assume "x = a" thus ?case using Cons by force 

798 
next 

799 
assume "x \<noteq> a" 

800 
show ?case 

801 
proof 

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

803 
from prems show "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys" 

804 
by(fastsimp intro!: Cons_eq_appendI) 

805 
next 

806 
assume "\<exists>ys zs. a # xs = ys @ x # zs \<and> x \<notin> set ys" 

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

808 
show "x \<in> set (a # xs)" by (cases ys, auto simp add: eq) 

809 
qed 

810 
qed 

811 
qed 

812 

813 
lemmas split_list = in_set_conv_decomp[THEN iffD1, standard] 

814 
lemmas split_list_first = in_set_conv_decomp_first[THEN iffD1, standard] 

815 

816 

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

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

820 
done 

821 

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

13114  824 

15168  825 

15392  826 
subsubsection {* @{text filter} *} 
13114  827 

13142  828 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  829 
by (induct xs) auto 
13114  830 

15305  831 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
832 
by (induct xs) simp_all 

833 

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

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

839 

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

842 
by(induct xs) simp_all 

843 

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

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

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

852 

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

854 
apply (induct xs) 

855 
apply auto 

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

857 
apply simp 

858 
done 

13114  859 

16965  860 
lemma filter_map: 
861 
"filter P (map f xs) = map f (filter (P o f) xs)" 

862 
by (induct xs) simp_all 

863 

864 
lemma length_filter_map[simp]: 

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

866 
by (simp add:filter_map) 

867 

13142  868 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  869 
by auto 
13114  870 

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

873 
proof (induct xs) 

874 
case Nil thus ?case by simp 

875 
next 

876 
case (Cons x xs) thus ?case 

877 
apply (auto split:split_if_asm) 

878 
using length_filter_le[of P xs] apply arith 

879 
done 

880 
qed 

13114  881 

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

884 
proof (induct xs) 

885 
case Nil thus ?case by simp 

886 
next 

887 
case (Cons x xs) 

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

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

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

891 
proof (cases) 

892 
assume "p x" 

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

894 
by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) 

895 
have "length (filter p (x # xs)) = Suc(card ?S)" 

23388  896 
using Cons `p x` by simp 
15281  897 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 
898 
by (simp add: card_image inj_Suc) 

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

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

901 
finally show ?thesis . 

902 
next 

903 
assume "\<not> p x" 

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

905 
by(auto simp add: nth_Cons image_def split:nat.split elim:lessE) 

906 
have "length (filter p (x # xs)) = card ?S" 

23388  907 
using Cons `\<not> p x` by simp 
15281  908 
also have "\<dots> = card(Suc ` ?S)" using fin 
909 
by (simp add: card_image inj_Suc) 

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

911 
by (simp add:card_insert_if) 

912 
finally show ?thesis . 

913 
qed 

914 
qed 

915 

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

918 
\<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  919 
(is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs") 
17629  920 
proof(induct ys) 
921 
case Nil thus ?case by simp 

922 
next 

923 
case (Cons y ys) 

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

925 
proof cases 

926 
assume Py: "P y" 

927 
show ?thesis 

928 
proof cases 

929 
assume xy: "x = y" 

930 
show ?thesis 

931 
proof from Py xy Cons(2) show "?Q []" by simp qed 

932 
next 

933 
assume "x \<noteq> y" with Py Cons(2) show ?thesis by simp 

934 
qed 

935 
next 

936 
assume Py: "\<not> P y" 

937 
with Cons obtain us vs where 1 : "?P (y#ys) (y#us) vs" by fastsimp 

938 
show ?thesis (is "? us. ?Q us") 

939 
proof show "?Q (y#us)" using 1 by simp qed 

940 
qed 

941 
qed 

942 

943 
lemma filter_eq_ConsD: 

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

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

946 
by(rule Cons_eq_filterD) simp 

947 

948 
lemma filter_eq_Cons_iff: 

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

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

951 
by(auto dest:filter_eq_ConsD) 

952 

953 
lemma Cons_eq_filter_iff: 

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

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

956 
by(auto dest:Cons_eq_filterD) 

957 

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

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

961 
apply(erule thin_rl) 

962 
by (induct ys) simp_all 

963 

15281  964 

15392  965 
subsubsection {* @{text concat} *} 
13114  966 

13142  967 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  968 
by (induct xs) auto 
13114  969 

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

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

13142  976 
lemma set_concat [simp]: "set (concat xs) = \<Union>(set ` set xs)" 
13145  977 
by (induct xs) auto 
13114  978 

23983  979 
lemma set_concat_map: "set(concat(map f xs)) = (UN x:set xs. set(f x))" 
980 
by(auto) 

981 

13142  982 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  983 
by (induct xs) auto 
13114  984 

13142  985 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  986 
by (induct xs) auto 
13114  987 

13142  988 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  989 
by (induct xs) auto 
13114  990 

991 

15392  992 
subsubsection {* @{text nth} *} 
13114  993 

13142  994 
lemma nth_Cons_0 [simp]: "(x # xs)!0 = x" 
13145  995 
by auto 
13114  996 

13142  997 
lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n" 
13145  998 
by auto 
13114  999 

13142  1000 
declare nth.simps [simp del] 
13114  1001 

1002 
lemma nth_append: 

13145  1003 
"!!n. (xs @ ys)!n = (if n < length xs then xs!n else ys!(n  length xs))" 
14208  1004 
apply (induct "xs", simp) 
1005 
apply (case_tac n, auto) 

13145  1006 
done 
13114  1007 

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

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

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

1010 

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

1011 
lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n" 
4201e1916482
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
nipkow
parents:
14395
diff
changeset

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

1013 

13142  1014 
lemma nth_map [simp]: "!!n. n < length xs ==> (map f xs)!n = f(xs!n)" 
14208  1015 
apply (induct xs, simp) 
1016 
apply (case_tac n, auto) 

13145  1017 
done 
13114  1018 

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

1021 

18049  1022 

1023 
lemma list_eq_iff_nth_eq: 

1024 
"!!ys. (xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))" 

1025 
apply(induct xs) 

1026 
apply simp apply blast 

1027 
apply(case_tac ys) 

1028 
apply simp 

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

1030 
done 

1031 

13142  1032 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  1033 
apply (induct xs, simp, simp) 
13145  1034 
apply safe 
14208  1035 
apply (rule_tac x = 0 in exI, simp) 
1036 
apply (rule_tac x = "Suc i" in exI, simp) 

1037 
apply (case_tac i, simp) 

13145  1038 
apply (rename_tac j) 
14208  1039 
apply (rule_tac x = j in exI, simp) 
13145  1040 
done 
13114  1041 

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

1044 

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

13114  1047 

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

1051 
lemma all_nth_imp_all_set: 

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

13114  1054 

1055 
lemma all_set_conv_all_nth: 

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

13114  1058 

1059 

15392  1060 
subsubsection {* @{text list_update} *} 
13114  1061 

13142  1062 
lemma length_list_update [simp]: "!!i. length(xs[i:=x]) = length xs" 
13145  1063 
by (induct xs) (auto split: nat.split) 
13114  1064 

1065 
lemma nth_list_update: 

13145  1066 
"!!i j. i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)" 
1067 
by (induct xs) (auto simp add: nth_Cons split: nat.split) 

13114  1068 

13142  1069 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  1070 
by (simp add: nth_list_update) 
13114  1071 

13142  1072 
lemma nth_list_update_neq [simp]: "!!i j. i \<noteq> j ==> xs[i:=x]!j = xs!j" 
13145  1073 
by (induct xs) (auto simp add: nth_Cons split: nat.split) 
13114  1074 

13142  1075 
lemma list_update_overwrite [simp]: 
13145  1076 
"!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]" 
1077 
by (induct xs) (auto split: nat.split) 

13114  1078 

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

1079 
lemma list_update_id[simp]: "!!i. i < length xs ==> xs[i := xs!i] = xs" 
14208  1080 
apply (induct xs, simp) 
14187  1081 
apply(simp split:nat.splits) 
1082 
done 

1083 

17501  1084 
lemma list_update_beyond[simp]: "\<And>i. length xs \<le> i \<Longrightarrow> xs[i:=x] = xs" 
1085 
apply (induct xs) 

1086 
apply simp 

1087 
apply (case_tac i) 

1088 
apply simp_all 

1089 
done 

1090 

13114  1091 
lemma list_update_same_conv: 
13145  1092 
"!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)" 
1093 
by (induct xs) (auto split: nat.split) 

13114  1094 

14187  1095 
lemma list_update_append1: 
1096 
"!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys" 

14208  1097 
apply (induct xs, simp) 
14187  1098 
apply(simp split:nat.split) 
1099 
done 

1100 

15868  1101 
lemma list_update_append: 
1102 
"!!n. (xs @ ys) [n:= x] = 

1103 
(if n < length xs then xs[n:= x] @ ys else xs @ (ys [nlength xs:= x]))" 

1104 
by (induct xs) (auto split:nat.splits) 

1105 

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

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

1107 
"(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

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

1109 

13114  1110 
lemma update_zip: 
13145  1111 
"!!i xy xs. length xs = length ys ==> 
1112 
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" 

1113 
by (induct ys) (auto, case_tac xs, auto split: nat.split) 

13114  1114 

1115 
lemma set_update_subset_insert: "!!i. set(xs[i:=x]) <= insert x (set xs)" 

13145  1116 
by (induct xs) (auto split: nat.split) 
13114  1117 

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

13145  1119 
by (blast dest!: set_update_subset_insert [THEN subsetD]) 
13114  1120 

15868  1121 
lemma set_update_memI: "!!n. n < length xs \<Longrightarrow> x \<in> set (xs[n := x])" 
1122 
by (induct xs) (auto split:nat.splits) 

1123 

13114  1124 

15392  1125 
subsubsection {* @{text last} and @{text butlast} *} 
13114  1126 

13142  1127 
lemma last_snoc [simp]: "last (xs @ [x]) = x" 
13145  1128 
by (induct xs) auto 
13114  1129 

13142  1130 
lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs" 
13145  1131 
by (induct xs) auto 
13114  1132 

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

1135 

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

1137 
by(simp add:last.simps) 

1138 

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

1140 
by (induct xs) (auto) 

1141 

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

1143 
by(simp add:last_append) 

1144 

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

1146 
by(simp add:last_append) 

1147 

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

1150 

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

1152 
by(cases xs) simp_all 

1153 

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

17762  1156 

13142  1157 
lemma length_butlast [simp]: "length (butlast xs) = length xs  1" 
13145  1158 
by (induct xs rule: rev_induct) auto 
13114  1159 

1160 
lemma butlast_append: 

13145  1161 
"!!ys. butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)" 
1162 
by (induct xs) auto 

13114  1163 

13142  1164 
lemma append_butlast_last_id [simp]: 
13145  1165 
"xs \<noteq> [] ==> butlast xs @ [last xs] = xs" 
1166 
by (induct xs) auto 

13114  1167 

13142  1168 
lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs" 
13145  1169 
by (induct xs) (auto split: split_if_asm) 
13114  1170 

1171 
lemma in_set_butlast_appendI: 

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

13114  1174 

17501  1175 
lemma last_drop[simp]: "!!n. n < length xs \<Longrightarrow> last (drop n xs) = last xs" 
1176 
apply (induct xs) 

1177 
apply simp 

1178 
apply (auto split:nat.split) 

1179 
done 

1180 

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

1183 

15392  1184 
subsubsection {* @{text take} and @{text drop} *} 
13114  1185 

13142  1186 
lemma take_0 [simp]: "take 0 xs = []" 
13145  1187 
by (induct xs) auto 
13114  1188 

13142  1189 
lemma drop_0 [simp]: "drop 0 xs = xs" 
13145  1190 
by (induct xs) auto 
13114  1191 

13142  1192 
lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs" 
13145  1193 
by simp 
13114  1194 

13142  1195 
lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs" 
13145  1196 
by simp 
13114  1197 

13142  1198 
declare take_Cons [simp del] and drop_Cons [simp del] 
13114  1199 

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

1200 
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

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

1202 

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

1205 

1206 
lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)" 

1207 
by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split) 

1208 

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

14208  1210 
apply (induct xs, simp) 
14187  1211 
apply(simp add:drop_Cons nth_Cons split:nat.splits) 
1212 
done 

1213 

13913  1214 
lemma take_Suc_conv_app_nth: 
1215 
"!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]" 

14208  1216 
apply (induct xs, simp) 
1217 
apply (case_tac i, auto) 

13913  1218 
done 
1219 

14591  1220 
lemma drop_Suc_conv_tl: 
1221 
"!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs" 

1222 
apply (induct xs, simp) 

1223 
apply (case_tac i, auto) 

1224 
done 

1225 

13142  1226 
lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n" 
13145  1227 
by (induct n) (auto, case_tac xs, auto) 
13114  1228 

13142  1229 
lemma length_drop [simp]: "!!xs. length (drop n xs) = (length xs  n)" 
13145  1230 
by (induct n) (auto, case_tac xs, auto) 
13114  1231 

13142  1232 
lemma take_all [simp]: "!!xs. length xs <= n ==> take n xs = xs" 
13145  1233 
by (induct n) (auto, case_tac xs, auto) 
13114  1234 

13142  1235 
lemma drop_all [simp]: "!!xs. length xs <= n ==> drop n xs = []" 
13145  1236 
by (induct n) (auto, case_tac xs, auto) 
13114  1237 

13142  1238 
lemma take_append [simp]: 
13145  1239 
"!!xs. take n (xs @ ys) = (take n xs @ take (n  length xs) ys)" 
1240 
by (induct n) (auto, case_tac xs, auto) 

13114  1241 

13142  1242 
lemma drop_append [simp]: 
13145  1243 
"!!xs. drop n (xs @ ys) = drop n xs @ drop (n  length xs) ys" 
1244 
by (induct n) (auto, case_tac xs, auto) 

13114  1245 

13142  1246 
lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs" 
14208  1247 
apply (induct m, auto) 
1248 
apply (case_tac xs, auto) 

15236
f289e8ba2bb3
Proofs needed to be updated because induction now preserves name of
nipkow
parents:
15176
diff
changeset

1249 
apply (case_tac n, auto) 
13145  1250 
done 
13114  1251 

13142  1252 
lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs" 
14208  1253 
apply (induct m, auto) 
1254 
apply (case_tac xs, auto) 

13145  1255 
done 
13114  1256 

1257 
lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)" 

14208  1258 
apply (induct m, auto) 
1259 
apply (case_tac xs, auto) 

13145  1260 
done 
13114  1261 

14802  1262 
lemma drop_take: "!!m n. drop n (take m xs) = take (mn) (drop n xs)" 
1263 
apply(induct xs) 

1264 
apply simp 

1265 
apply(simp add: take_Cons drop_Cons split:nat.split) 

1266 
done 

1267 

13142  1268 
lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs" 
14208  1269 
apply (induct n, auto) 
1270 
apply (case_tac xs, auto) 

13145  1271 
done 
13114  1272 

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

1273 
lemma take_eq_Nil[simp]: "!!n. (take n xs = []) = (n = 0 \<or> xs = [])" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

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

1276 
apply(simp add:take_Cons split:nat.split) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

1278 

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

1279 
lemma drop_eq_Nil[simp]: "!!n. (drop n xs = []) = (length xs <= n)" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

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

1282 
apply(simp add:drop_Cons split:nat.split) 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

1284 

13114  1285 
lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)" 
14208  1286 
apply (induct n, auto) 
1287 
apply (case_tac xs, auto) 

13145  1288 
done 
13114  1289 

13142  1290 
lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" 
14208  1291 
apply (induct n, auto) 
1292 
apply (case_tac xs, auto) 

13145  1293 
done 
13114  1294 

1295 
lemma rev_take: "!!i. rev (take i xs) = drop (length xs  i) (rev xs)" 

14208  1296 
apply (induct xs, auto) 
1297 
apply (case_tac i, auto) 

13145  1298 
done 
13114  1299 

1300 
lemma rev_drop: "!!i. rev (drop i xs) = take (length xs  i) (rev xs)" 

14208  1301 
apply (induct xs, auto) 
1302 
apply (case_tac i, auto) 

13145  1303 
done 
13114  1304 

13142  1305 
lemma nth_take [simp]: "!!n i. i < n ==> (take n xs)!i = xs!i" 
14208  1306 
apply (induct xs, auto) 
1307 
apply (case_tac n, blast) 

1308 
apply (case_tac i, auto) 

13145  1309 
done 
13114  1310 

13142  1311 
lemma nth_drop [simp]: 
13145  1312 
"!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" 
14208  1313 
apply (induct n, auto) 
1314 
apply (case_tac xs, auto) 

13145  1315 
done 
3507  1316 

18423  1317 
lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n" 
1318 
by(simp add: hd_conv_nth) 

1319 

14025  1320 
lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs" 
1321 
by(induct xs)(auto simp:take_Cons split:nat.split) 

1322 

1323 
lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs" 

1324 
by(induct xs)(auto simp:drop_Cons split:nat.split) 

1325 

14187  1326 
lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs" 
1327 
using set_take_subset by fast 

1328 

1329 
lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs" 

1330 
using set_drop_subset by fast 

1331 

13114  1332 
lemma append_eq_conv_conj: 
13145  1333 
"!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)" 
14208  1334 
apply (induct xs, simp, clarsimp) 
1335 
apply (case_tac zs, auto) 

13145  1336 
done 
13142  1337 

14050  1338 
lemma take_add [rule_format]: 
1339 
"\<forall>i. i+j \<le> length(xs) > take (i+j) xs = take i xs @ take j (drop i xs)" 

1340 
apply (induct xs, auto) 

1341 
apply (case_tac i, simp_all) 

1342 
done 

1343 

14300  1344 
lemma append_eq_append_conv_if: 
1345 
"!! ys\<^isub>1. (xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) = 

1346 
(if size xs\<^isub>1 \<le> size ys\<^isub>1 

1347 
then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2 

1348 
else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)" 

1349 
apply(induct xs\<^isub>1) 

1350 
apply simp 

1351 
apply(case_tac ys\<^isub>1) 
