author  nipkow 
Mon, 31 Oct 2005 01:43:22 +0100  
changeset 18049  156bba334c12 
parent 17956  369e2af8ee45 
child 18336  1a2e30b37ed3 
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 
15140  9 
imports PreList 
15131  10 
begin 
923  11 

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

923  15 

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

923  18 
consts 
13366  19 
"@" :: "'a list => 'a list => 'a list" (infixr 65) 
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 
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" 

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

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 
null:: "'a list => bool" 
43 
"distinct":: "'a list => bool" 

44 
replicate :: "nat => 'a => 'a list" 

15302  45 
rotate1 :: "'a list \<Rightarrow> 'a list" 
46 
rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" 

47 
sublist :: "'a list => nat set => 'a list" 

17086  48 
(* For efficiency *) 
49 
mem :: "'a => 'a list => bool" (infixl 55) 

50 
list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 

51 
list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" 

52 
list_all:: "('a => bool) => ('a list => bool)" 

53 
itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" 

54 
filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" 

55 
map_filter :: "('a => 'b) => ('a => bool) => 'a list => 'b list" 

15302  56 

923  57 

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

59 

923  60 
syntax 
13366  61 
 {* list Enumeration *} 
62 
"@list" :: "args => 'a list" ("[(_)]") 

923  63 

13366  64 
 {* Special syntax for filter *} 
65 
"@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_:_./ _])") 

923  66 

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

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

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

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

72 

13366  73 
upto:: "nat => nat => nat list" ("(1[_../_])") 
5427  74 

923  75 
translations 
13366  76 
"[x, xs]" == "x#[xs]" 
77 
"[x]" == "x#[]" 

78 
"[x:xs . P]"== "filter (%x. P) xs" 

923  79 

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

82 

15425  83 
"[i..j]" == "[i..<(Suc j)]" 
5427  84 

85 

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

86 
syntax (xsymbols) 
13366  87 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])") 
14565  88 
syntax (HTML output) 
89 
"@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<in>_ ./ _])") 

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

90 

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

91 

13142  92 
text {* 
14589  93 
Function @{text size} is overloaded for all datatypes. Users may 
13366  94 
refer to the list version as @{text length}. *} 
13142  95 

96 
syntax length :: "'a list => nat" 

97 
translations "length" => "size :: _ list => nat" 

13114  98 

13142  99 
typed_print_translation {* 
13366  100 
let 
101 
fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] = 

102 
Syntax.const "length" $ t 

103 
 size_tr' _ _ _ = raise Match; 

104 
in [("size", size_tr')] end 

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

106 

15302  107 

5183  108 
primrec 
15307  109 
"hd(x#xs) = x" 
110 

5183  111 
primrec 
15307  112 
"tl([]) = []" 
113 
"tl(x#xs) = xs" 

114 

5183  115 
primrec 
15307  116 
"null([]) = True" 
117 
"null(x#xs) = False" 

118 

8972  119 
primrec 
15307  120 
"last(x#xs) = (if xs=[] then x else last xs)" 
121 

5183  122 
primrec 
15307  123 
"butlast []= []" 
124 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 

125 

5183  126 
primrec 
15307  127 
"set [] = {}" 
128 
"set (x#xs) = insert x (set xs)" 

129 

5183  130 
primrec 
15307  131 
"map f [] = []" 
132 
"map f (x#xs) = f(x)#map f xs" 

133 

5183  134 
primrec 
15307  135 
append_Nil:"[]@ys = ys" 
136 
append_Cons: "(x#xs)@ys = x#(xs@ys)" 

137 

5183  138 
primrec 
15307  139 
"rev([]) = []" 
140 
"rev(x#xs) = rev(xs) @ [x]" 

141 

5183  142 
primrec 
15307  143 
"filter P [] = []" 
144 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 

145 

5183  146 
primrec 
15307  147 
foldl_Nil:"foldl f a [] = a" 
148 
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" 

149 

8000  150 
primrec 
15307  151 
"foldr f [] a = a" 
152 
"foldr f (x#xs) a = f x (foldr f xs a)" 

153 

5183  154 
primrec 
15307  155 
"concat([]) = []" 
156 
"concat(x#xs) = x @ concat(xs)" 

157 

5183  158 
primrec 
15307  159 
drop_Nil:"drop n [] = []" 
160 
drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs  Suc(m) => drop m xs)" 

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 
take_Nil:"take n [] = []" 
166 
take_Cons: "take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs)" 

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

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

169 

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

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

174 

5183  175 
primrec 
15307  176 
"[][i:=v] = []" 
177 
"(x#xs)[i:=v] = (case i of 0 => v # xs  Suc j => x # xs[j:=v])" 

178 

179 
primrec 

180 
"takeWhile P [] = []" 

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

182 

5183  183 
primrec 
15307  184 
"dropWhile P [] = []" 
185 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 

186 

5183  187 
primrec 
15307  188 
"zip xs [] = []" 
189 
zip_Cons: "zip xs (y#ys) = (case xs of [] => []  z#zs => (z,y)#zip zs ys)" 

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

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

192 

5427  193 
primrec 
15425  194 
upt_0: "[i..<0] = []" 
195 
upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])" 

15307  196 

5183  197 
primrec 
15307  198 
"distinct [] = True" 
199 
"distinct (x#xs) = (x ~: set xs \<and> distinct xs)" 

200 

5183  201 
primrec 
15307  202 
"remdups [] = []" 
203 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

204 

5183  205 
primrec 
15307  206 
"remove1 x [] = []" 
207 
"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)" 

208 

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

209 
primrec 
15307  210 
replicate_0: "replicate 0 x = []" 
211 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

212 

8115  213 
defs 
15302  214 
rotate1_def: "rotate1 xs == (case xs of [] \<Rightarrow> []  x#xs \<Rightarrow> xs @ [x])" 
215 
rotate_def: "rotate n == rotate1 ^ n" 

216 

217 
list_all2_def: 

218 
"list_all2 P xs ys == 

219 
length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" 

220 

221 
sublist_def: 

15425  222 
"sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..<size xs]))" 
5281  223 

17086  224 
primrec 
225 
"x mem [] = False" 

226 
"x mem (y#ys) = (if y=x then True else x mem ys)" 

227 

228 
primrec 

229 
"list_inter [] bs = []" 

230 
"list_inter (a#as) bs = 

231 
(if a \<in> set bs then a#(list_inter as bs) else list_inter as bs)" 

232 

233 
primrec 

234 
"list_all P [] = True" 

235 
"list_all P (x#xs) = (P(x) \<and> list_all P xs)" 

236 

237 
primrec 

238 
"list_ex P [] = False" 

239 
"list_ex P (x#xs) = (P x \<or> list_ex P xs)" 

240 

241 
primrec 

242 
"filtermap f [] = []" 

243 
"filtermap f (x#xs) = 

244 
(case f x of None \<Rightarrow> filtermap f xs 

245 
 Some y \<Rightarrow> y # (filtermap f xs))" 

246 

247 
primrec 

248 
"map_filter f P [] = []" 

249 
"map_filter f P (x#xs) = (if P x then f x # map_filter f P xs else 

250 
map_filter f P xs)" 

251 

252 
primrec 

253 
"itrev [] ys = ys" 

254 
"itrev (x#xs) ys = itrev xs (x#ys)" 

255 

13114  256 

13142  257 
lemma not_Cons_self [simp]: "xs \<noteq> x # xs" 
13145  258 
by (induct xs) auto 
13114  259 

13142  260 
lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric] 
13114  261 

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

13142  265 
lemma length_induct: 
13145  266 
"(!!xs. \<forall>ys. length ys < length xs > P ys ==> P xs) ==> P xs" 
17589  267 
by (rule measure_induct [of length]) iprover 
13114  268 

269 

15392  270 
subsubsection {* @{text length} *} 
13114  271 

13142  272 
text {* 
13145  273 
Needs to come before @{text "@"} because of theorem @{text 
274 
append_eq_append_conv}. 

13142  275 
*} 
13114  276 

13142  277 
lemma length_append [simp]: "length (xs @ ys) = length xs + length ys" 
13145  278 
by (induct xs) auto 
13114  279 

13142  280 
lemma length_map [simp]: "length (map f xs) = length xs" 
13145  281 
by (induct xs) auto 
13114  282 

13142  283 
lemma length_rev [simp]: "length (rev xs) = length xs" 
13145  284 
by (induct xs) auto 
13114  285 

13142  286 
lemma length_tl [simp]: "length (tl xs) = length xs  1" 
13145  287 
by (cases xs) auto 
13114  288 

13142  289 
lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])" 
13145  290 
by (induct xs) auto 
13114  291 

13142  292 
lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" 
13145  293 
by (induct xs) auto 
13114  294 

295 
lemma length_Suc_conv: 

13145  296 
"(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" 
297 
by (induct xs) auto 

13142  298 

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

14208  301 
apply (induct xs, simp, simp) 
14025  302 
apply blast 
303 
done 

304 

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

14208  307 
apply (induct xs, auto) 
14099  308 
done 
309 

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

312 
P [] []; 

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

314 
\<Longrightarrow> P xs ys" 

315 
apply(induct xs) 

316 
apply simp 

317 
apply(case_tac ys) 

318 
apply simp 

319 
apply(simp) 

320 
done 

13114  321 

15392  322 
subsubsection {* @{text "@"}  append *} 
13114  323 

13142  324 
lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" 
13145  325 
by (induct xs) auto 
13114  326 

13142  327 
lemma append_Nil2 [simp]: "xs @ [] = xs" 
13145  328 
by (induct xs) auto 
3507  329 

13142  330 
lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" 
13145  331 
by (induct xs) auto 
13114  332 

13142  333 
lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" 
13145  334 
by (induct xs) auto 
13114  335 

13142  336 
lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" 
13145  337 
by (induct xs) auto 
13114  338 

13142  339 
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" 
13145  340 
by (induct xs) auto 
13114  341 

13883
0451e0fb3f22
Restructured some proofs in order to get rid of rule_format attribute.
berghofe
parents:
13863
diff
changeset

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

343 
"!!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

344 
==> (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

345 
apply (induct xs) 
14208  346 
apply (case_tac ys, simp, force) 
347 
apply (case_tac ys, force, simp) 

13145  348 
done 
13142  349 

14495  350 
lemma append_eq_append_conv2: "!!ys zs ts. 
351 
(xs @ ys = zs @ ts) = 

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

353 
apply (induct xs) 

354 
apply fastsimp 

355 
apply(case_tac zs) 

356 
apply simp 

357 
apply fastsimp 

358 
done 

359 

13142  360 
lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)" 
13145  361 
by simp 
13142  362 

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

13145  364 
by simp 
13114  365 

13142  366 
lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)" 
13145  367 
by simp 
13114  368 

13142  369 
lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" 
13145  370 
using append_same_eq [of _ _ "[]"] by auto 
3507  371 

13142  372 
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" 
13145  373 
using append_same_eq [of "[]"] by auto 
13114  374 

13142  375 
lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs" 
13145  376 
by (induct xs) auto 
13114  377 

13142  378 
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)" 
13145  379 
by (induct xs) auto 
13114  380 

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

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

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

390 

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

393 
by(cases ys) auto 

394 

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

397 
by(cases ys) auto 

398 

14300  399 

13142  400 
text {* Trivial rules for solving @{text "@"}equations automatically. *} 
13114  401 

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

13145  403 
by simp 
13114  404 

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

13114  408 

13142  409 
lemma append_eq_appendI: 
13145  410 
"[ xs @ xs1 = zs; ys = xs1 @ us ] ==> xs @ ys = zs @ us" 
411 
by (drule sym) simp 

13114  412 

413 

13142  414 
text {* 
13145  415 
Simplification procedure for all list equalities. 
416 
Currently only tries to rearrange @{text "@"} to see if 

417 
 both lists end in a singleton list, 

418 
 or both lists end in the same list. 

13142  419 
*} 
420 

421 
ML_setup {* 

3507  422 
local 
423 

13122  424 
val append_assoc = thm "append_assoc"; 
425 
val append_Nil = thm "append_Nil"; 

426 
val append_Cons = thm "append_Cons"; 

427 
val append1_eq_conv = thm "append1_eq_conv"; 

428 
val append_same_eq = thm "append_same_eq"; 

429 

13114  430 
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = 
13462  431 
(case xs of Const("List.list.Nil",_) => cons  _ => last xs) 
432 
 last (Const("List.op @",_) $ _ $ ys) = last ys 

433 
 last t = t; 

13114  434 

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

13462  436 
 list1 _ = false; 
13114  437 

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

13462  439 
(case xs of Const("List.list.Nil",_) => xs  _ => cons $ butlast xs) 
440 
 butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys 

441 
 butlast xs = Const("List.list.Nil",fastype_of xs); 

13114  442 

16973  443 
val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]; 
444 

445 
fun list_eq sg ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) = 

13462  446 
let 
447 
val lastl = last lhs and lastr = last rhs; 

448 
fun rearr conv = 

449 
let 

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

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

452 
val appT = [listT,listT] > listT 

453 
val app = Const("List.op @",appT) 

454 
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

455 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2)); 
17956  456 
val thm = Goal.prove sg [] [] eq 
17877
67d5ab1cb0d8
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
wenzelm
parents:
17830
diff
changeset

457 
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1)); 
15531  458 
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end; 
13114  459 

13462  460 
in 
461 
if list1 lastl andalso list1 lastr then rearr append1_eq_conv 

462 
else if lastl aconv lastr then rearr append_same_eq 

15531  463 
else NONE 
13462  464 
end; 
465 

13114  466 
in 
13462  467 

468 
val list_eq_simproc = 

469 
Simplifier.simproc (Theory.sign_of (the_context ())) "list_eq" ["(xs::'a list) = ys"] list_eq; 

470 

13114  471 
end; 
472 

473 
Addsimprocs [list_eq_simproc]; 

474 
*} 

475 

476 

15392  477 
subsubsection {* @{text map} *} 
13114  478 

13142  479 
lemma map_ext: "(!!x. x : set xs > f x = g x) ==> map f xs = map g xs" 
13145  480 
by (induct xs) simp_all 
13114  481 

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

13142  485 
lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" 
13145  486 
by (induct xs) auto 
13114  487 

13142  488 
lemma map_compose: "map (f o g) xs = map f (map g xs)" 
13145  489 
by (induct xs) (auto simp add: o_def) 
13114  490 

13142  491 
lemma rev_map: "rev (map f xs) = map f (rev xs)" 
13145  492 
by (induct xs) auto 
13114  493 

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

496 

13366  497 
lemma map_cong [recdef_cong]: 
13145  498 
"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys" 
499 
 {* a congruence rule for @{text map} *} 

13737  500 
by simp 
13114  501 

13142  502 
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" 
13145  503 
by (cases xs) auto 
13114  504 

13142  505 
lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" 
13145  506 
by (cases xs) auto 
13114  507 

14025  508 
lemma map_eq_Cons_conv[iff]: 
509 
"(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" 

13145  510 
by (cases xs) auto 
13114  511 

14025  512 
lemma Cons_eq_map_conv[iff]: 
513 
"(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" 

514 
by (cases ys) auto 

515 

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

518 
by(induct ys, auto) 

519 

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

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

521 
"!!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

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

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

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

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

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

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

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

529 

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

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

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

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

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

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

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

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

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

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

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

540 

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

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

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

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

544 

13114  545 
lemma map_injective: 
14338  546 
"!!xs. map f xs = map f ys ==> inj f ==> xs = ys" 
547 
by (induct ys) (auto dest!:injD) 

13114  548 

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

551 

13114  552 
lemma inj_mapI: "inj f ==> inj (map f)" 
17589  553 
by (iprover dest: map_injective injD intro: inj_onI) 
13114  554 

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

14208  556 
apply (unfold inj_on_def, clarify) 
13145  557 
apply (erule_tac x = "[x]" in ballE) 
14208  558 
apply (erule_tac x = "[y]" in ballE, simp, blast) 
13145  559 
apply blast 
560 
done 

13114  561 

14339  562 
lemma inj_map[iff]: "inj (map f) = inj f" 
13145  563 
by (blast dest: inj_mapD intro: inj_mapI) 
13114  564 

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

567 
apply(erule map_inj_on) 

568 
apply(blast intro:inj_onI dest:inj_onD) 

569 
done 

570 

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

13114  573 

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

574 
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

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

576 

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

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

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

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

580 

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

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

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

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

584 

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

585 

15392  586 
subsubsection {* @{text rev} *} 
13114  587 

13142  588 
lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs" 
13145  589 
by (induct xs) auto 
13114  590 

13142  591 
lemma rev_rev_ident [simp]: "rev (rev xs) = xs" 
13145  592 
by (induct xs) auto 
13114  593 

15870  594 
lemma rev_swap: "(rev xs = ys) = (xs = rev ys)" 
595 
by auto 

596 

13142  597 
lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" 
13145  598 
by (induct xs) auto 
13114  599 

13142  600 
lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" 
13145  601 
by (induct xs) auto 
13114  602 

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

605 

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

607 
by (cases xs) auto 

608 

13142  609 
lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)" 
14208  610 
apply (induct xs, force) 
611 
apply (case_tac ys, simp, force) 

13145  612 
done 
13114  613 

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

616 

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

619 
apply(simplesubst rev_rev_ident[symmetric]) 
13145  620 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 
621 
done 

13114  622 

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

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

13145  627 
by (induct xs rule: rev_induct) auto 
13114  628 

13366  629 
lemmas rev_cases = rev_exhaust 
630 

13114  631 

15392  632 
subsubsection {* @{text set} *} 
13114  633 

13142  634 
lemma finite_set [iff]: "finite (set xs)" 
13145  635 
by (induct xs) auto 
13114  636 

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

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

14099  642 

13142  643 
lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)" 
13145  644 
by auto 
13114  645 

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

648 

13142  649 
lemma set_empty [iff]: "(set xs = {}) = (xs = [])" 
13145  650 
by (induct xs) auto 
13114  651 

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

654 

13142  655 
lemma set_rev [simp]: "set (rev xs) = set xs" 
13145  656 
by (induct xs) auto 
13114  657 

13142  658 
lemma set_map [simp]: "set (map f xs) = f`(set xs)" 
13145  659 
by (induct xs) auto 
13114  660 

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

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

13145  667 
done 
13114  668 

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

672 
case (Cons a xs) 

673 
show ?case 

674 
proof 

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

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

677 
by (simp, blast intro: Cons_eq_appendI) 

678 
next 

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

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

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

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

683 
qed 

684 
qed 

13142  685 

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

688 
proof (induct xs) 

689 
case Nil show ?case by simp 

690 
next 

691 
case (Cons a xs) 

692 
show ?case 

693 
proof cases 

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

695 
next 

696 
assume "x \<noteq> a" 

697 
show ?case 

698 
proof 

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

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

701 
by(fastsimp intro!: Cons_eq_appendI) 

702 
next 

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

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

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

706 
qed 

707 
qed 

708 
qed 

709 

710 
lemmas split_list = in_set_conv_decomp[THEN iffD1, standard] 

711 
lemmas split_list_first = in_set_conv_decomp_first[THEN iffD1, standard] 

712 

713 

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

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

717 
done 

718 

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

13114  721 

15168  722 

15392  723 
subsubsection {* @{text filter} *} 
13114  724 

13142  725 
lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" 
13145  726 
by (induct xs) auto 
13114  727 

15305  728 
lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" 
729 
by (induct xs) simp_all 

730 

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

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

736 

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

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

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

745 

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

747 
apply (induct xs) 

748 
apply auto 

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

750 
apply simp 

751 
done 

13114  752 

16965  753 
lemma filter_map: 
754 
"filter P (map f xs) = map f (filter (P o f) xs)" 

755 
by (induct xs) simp_all 

756 

757 
lemma length_filter_map[simp]: 

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

759 
by (simp add:filter_map) 

760 

13142  761 
lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs" 
13145  762 
by auto 
13114  763 

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

766 
proof (induct xs) 

767 
case Nil thus ?case by simp 

768 
next 

769 
case (Cons x xs) thus ?case 

770 
apply (auto split:split_if_asm) 

771 
using length_filter_le[of P xs] apply arith 

772 
done 

773 
qed 

13114  774 

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

777 
proof (induct xs) 

778 
case Nil thus ?case by simp 

779 
next 

780 
case (Cons x xs) 

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

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

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

784 
proof (cases) 

785 
assume "p x" 

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

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

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

789 
using Cons by simp 

790 
also have "\<dots> = Suc(card(Suc ` ?S))" using fin 

791 
by (simp add: card_image inj_Suc) 

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

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

794 
finally show ?thesis . 

795 
next 

796 
assume "\<not> p x" 

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

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

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

800 
using Cons by simp 

801 
also have "\<dots> = card(Suc ` ?S)" using fin 

802 
by (simp add: card_image inj_Suc) 

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

804 
by (simp add:card_insert_if) 

805 
finally show ?thesis . 

806 
qed 

807 
qed 

808 

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

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

812 
(concl is "\<exists>us vs. ?P ys us vs") 

813 
proof(induct ys) 

814 
case Nil thus ?case by simp 

815 
next 

816 
case (Cons y ys) 

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

818 
proof cases 

819 
assume Py: "P y" 

820 
show ?thesis 

821 
proof cases 

822 
assume xy: "x = y" 

823 
show ?thesis 

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

825 
next 

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

827 
qed 

828 
next 

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

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

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

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

833 
qed 

834 
qed 

835 

836 
lemma filter_eq_ConsD: 

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

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

839 
by(rule Cons_eq_filterD) simp 

840 

841 
lemma filter_eq_Cons_iff: 

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

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

844 
by(auto dest:filter_eq_ConsD) 

845 

846 
lemma Cons_eq_filter_iff: 

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

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

849 
by(auto dest:Cons_eq_filterD) 

850 

17501  851 
lemma filter_cong: 
852 
"xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys" 

853 
apply simp 

854 
apply(erule thin_rl) 

855 
by (induct ys) simp_all 

856 

15281  857 

15392  858 
subsubsection {* @{text concat} *} 
13114  859 

13142  860 
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" 
13145  861 
by (induct xs) auto 
13114  862 

13142  863 
lemma concat_eq_Nil_conv [iff]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" 
13145  864 
by (induct xss) auto 
13114  865 

13142  866 
lemma Nil_eq_concat_conv [iff]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" 
13145  867 
by (induct xss) auto 
13114  868 

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

13142  872 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
13145  873 
by (induct xs) auto 
13114  874 

13142  875 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
13145  876 
by (induct xs) auto 
13114  877 

13142  878 
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" 
13145  879 
by (induct xs) auto 
13114  880 

881 

15392  882 
subsubsection {* @{text nth} *} 
13114  883 

13142  884 
lemma nth_Cons_0 [simp]: "(x # xs)!0 = x" 
13145  885 
by auto 
13114  886 

13142  887 
lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n" 
13145  888 
by auto 
13114  889 

13142  890 
declare nth.simps [simp del] 
13114  891 

892 
lemma nth_append: 

13145  893 
"!!n. (xs @ ys)!n = (if n < length xs then xs!n else ys!(n  length xs))" 
14208  894 
apply (induct "xs", simp) 
895 
apply (case_tac n, auto) 

13145  896 
done 
13114  897 

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

898 
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

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

900 

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

901 
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

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

903 

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

13145  907 
done 
13114  908 

18049  909 

910 
lemma list_eq_iff_nth_eq: 

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

912 
apply(induct xs) 

913 
apply simp apply blast 

914 
apply(case_tac ys) 

915 
apply simp 

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

917 
done 

918 

13142  919 
lemma set_conv_nth: "set xs = {xs!i  i. i < length xs}" 
15251  920 
apply (induct xs, simp, simp) 
13145  921 
apply safe 
14208  922 
apply (rule_tac x = 0 in exI, simp) 
923 
apply (rule_tac x = "Suc i" in exI, simp) 

924 
apply (case_tac i, simp) 

13145  925 
apply (rename_tac j) 
14208  926 
apply (rule_tac x = j in exI, simp) 
13145  927 
done 
13114  928 

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

931 

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

13114  934 

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

938 
lemma all_nth_imp_all_set: 

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

13114  941 

942 
lemma all_set_conv_all_nth: 

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

13114  945 

946 

15392  947 
subsubsection {* @{text list_update} *} 
13114  948 

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

952 
lemma nth_list_update: 

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

13114  955 

13142  956 
lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x" 
13145  957 
by (simp add: nth_list_update) 
13114  958 

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

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

13114  965 

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

966 
lemma list_update_id[simp]: "!!i. i < length xs ==> xs[i := xs!i] = xs" 
14208  967 
apply (induct xs, simp) 
14187  968 
apply(simp split:nat.splits) 
969 
done 

970 

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

973 
apply simp 

974 
apply (case_tac i) 

975 
apply simp_all 

976 
done 

977 

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

13114  981 

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

14208  984 
apply (induct xs, simp) 
14187  985 
apply(simp split:nat.split) 
986 
done 

987 

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

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

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

992 

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

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

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

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

996 

13114  997 
lemma update_zip: 
13145  998 
"!!i xy xs. length xs = length ys ==> 
999 
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" 

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

13114  1001 

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

13145  1003 
by (induct xs) (auto split: nat.split) 
13114  1004 

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

13145  1006 
by (blast dest!: set_update_subset_insert [THEN subsetD]) 
13114  1007 

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

1010 

13114  1011 

15392  1012 
subsubsection {* @{text last} and @{text butlast} *} 
13114  1013 

13142  1014 
lemma last_snoc [simp]: "last (xs @ [x]) = x" 
13145  1015 
by (induct xs) auto 
13114  1016 

13142  1017 
lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs" 
13145  1018 
by (induct xs) auto 
13114  1019 

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

1022 

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

1024 
by(simp add:last.simps) 

1025 

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

1027 
by (induct xs) (auto) 

1028 

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

1030 
by(simp add:last_append) 

1031 

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

1033 
by(simp add:last_append) 

1034 

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

1037 

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

1039 
by(cases xs) simp_all 

1040 

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

17762  1043 

13142  1044 
lemma length_butlast [simp]: "length (butlast xs) = length xs  1" 
13145  1045 
by (induct xs rule: rev_induct) auto 
13114  1046 

1047 
lemma butlast_append: 

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

13114  1050 

13142  1051 
lemma append_butlast_last_id [simp]: 
13145  1052 
"xs \<noteq> [] ==> butlast xs @ [last xs] = xs" 
1053 
by (induct xs) auto 

13114  1054 

13142  1055 
lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs" 
13145  1056 
by (induct xs) (auto split: split_if_asm) 
13114  1057 

1058 
lemma in_set_butlast_appendI: 

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

13114  1061 

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

1064 
apply simp 

1065 
apply (auto split:nat.split) 

1066 
done 

1067 

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

1070 

13142  1071 

15392  1072 
subsubsection {* @{text take} and @{text drop} *} 
13114  1073 

13142  1074 
lemma take_0 [simp]: "take 0 xs = []" 
13145  1075 
by (induct xs) auto 
13114  1076 

13142  1077 
lemma drop_0 [simp]: "drop 0 xs = xs" 
13145  1078 
by (induct xs) auto 
13114  1079 

13142  1080 
lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs" 
13145  1081 
by simp 
13114  1082 

13142  1083 
lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs" 
13145  1084 
by simp 
13114  1085 

13142  1086 
declare take_Cons [simp del] and drop_Cons [simp del] 
13114  1087 

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

1088 
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

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

1090 

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

1093 

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

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

1096 

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

14208  1098 
apply (induct xs, simp) 
14187  1099 
apply(simp add:drop_Cons nth_Cons split:nat.splits) 
1100 
done 

1101 

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

14208  1104 
apply (induct xs, simp) 
1105 
apply (case_tac i, auto) 

13913  1106 
done 
1107 

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

1110 
apply (induct xs, simp) 

1111 
apply (case_tac i, auto) 

1112 
done 

1113 

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

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

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

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

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

13114  1129 

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

13114  1133 

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

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

1137 
apply (case_tac n, auto) 
13145  1138 
done 
13114  1139 

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

13145  1143 
done 
13114  1144 

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

14208  1146 
apply (induct m, auto) 
1147 
apply (case_tac xs, auto) 

13145  1148 
done 
13114  1149 

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

1152 
apply simp 

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

1154 
done 

1155 

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

13145  1159 
done 
13114  1160 

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

1161 
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

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

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

1164 
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

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

1166 

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

1167 
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

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

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

1170 
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

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

1172 

13114  1173 
lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)" 
14208  1174 
apply (induct n, auto) 
1175 
apply (case_tac xs, auto) 

13145  1176 
done 
13114  1177 

13142  1178 
lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" 
14208  1179 
apply (induct n, auto) 
1180 
apply (case_tac xs, auto) 

13145  1181 
done 
13114  1182 

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

14208  1184 
apply (induct xs, auto) 
1185 
apply (case_tac i, auto) 

13145  1186 
done 
13114  1187 

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

14208  1189 
apply (induct xs, auto) 
1190 
apply (case_tac i, auto) 

13145  1191 
done 
13114  1192 

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

1196 
apply (case_tac i, auto) 

13145  1197 
done 
13114  1198 

13142  1199 
lemma nth_drop [simp]: 
13145  1200 
"!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" 
14208  1201 
apply (induct n, auto) 
1202 
apply (case_tac xs, auto) 

13145  1203 
done 
3507  1204 

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

1207 

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

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

1210 

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

1213 

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

1215 
using set_drop_subset by fast 

1216 

13114  1217 
lemma append_eq_conv_conj: 
13145  1218 
"!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)" 
14208  1219 
apply (induct xs, simp, clarsimp) 
1220 
apply (case_tac zs, auto) 

13145  1221 
done 
13142  1222 

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

1225 
apply (induct xs, auto) 

1226 
apply (case_tac i, simp_all) 

1227 
done 

1228 

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

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

1232 
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 

1233 
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)" 

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

1235 
apply simp 

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

1237 
apply simp_all 

1238 
done 

1239 

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

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

1241 
"!!n. n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs" 
78b5636eabc7
Added a number of new thms and the new function remove1
nipkow
parents:
15072
diff
changeset

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

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

1244 
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

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

1246 

17501  1247 
lemma id_take_nth_drop: 
1248 
"i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 

1249 
proof  

1250 
assume si: "i < length xs" 

1251 
hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto 

1252 
moreover 

1253 
from si have "take (Suc i) xs = take i xs @ [xs!i]" 

1254 
apply (rule_tac take_Suc_conv_app_nth) by arith 

1255 
ultimately show ?thesis by auto 

1256 
qed 

1257 

1258 
lemma upd_conv_take_nth_drop: 

1259 
"i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs" 

1260 
proof  

1261 
assume i: "i < length xs" 

1262 
have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]" 

1263 
by(rule arg_cong[OF id_take_nth_drop[OF i]]) 

1264 
also have "\<dots> = take i xs @ a # drop (Suc i) xs" 

1265 
using i by (simp add: list_update_append) 

1266 
finally show ?thesis . 

1267 
qed 

1268 

13114  1269 

15392  1270 
subsubsection {* @{text takeWhile} and @{text dropWhile} *} 
13114  1271 

13142  1272 
lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs" 
13145  1273 
by (induct xs) auto 
13114  1274 

13142  1275 
lemma takeWhile_append1 [simp]: 
13145  1276 
"[ x:set xs; ~P(x)] ==> takeWhile P (xs @ ys) = takeWhile P xs" 
1277 
by (induct xs) auto 

13114  1278 

13142  1279 
lemma takeWhile_append2 [simp]: 
13145  1280 
"(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys" 
1281 
by (induct xs) auto 

13114  1282 

13142  1283 
lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs" 
13145  1284 
by (induct xs) auto 
13114  1285 

13142  1286 
lemma dropWhile_append1 [simp]: 
13145  1287 
"[ x : set xs; ~P(x)] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" 
1288 
by (induct xs) auto 

13114  1289 

13142  1290 
lemma dropWhile_append2 [simp]: 
13145  1291 
"(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" 
1292 
by (induct xs) auto 

13114  1293 

13142  1294 
lemma set_take_whileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x" 
13145  1295 
by (induct xs) (auto split: split_if_asm) 
13114  1296 

13913  1297 
lemma takeWhile_eq_all_conv[simp]: 
1298 
"(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)" 

1299 
by(induct xs, auto) 

1300 

1301 
lemma dropWhile_eq_Nil_conv[simp]: 

1302 
"(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)" 

1303 
by(induct xs, auto) 

1304 

1305 
lemma dropWhile_eq_Cons_conv: 

1306 
"(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)" 

1307 
by(induct xs, auto) 

1308 

17501  1309 
text{* The following two lemmmas could be generalized to an arbitrary 
1310 
property. *} 

1311 

1312 
lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow> 

1313 
takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))" 

1314 
by(induct xs) (auto simp: takeWhile_tail[where l="[]"]) 

1315 

1316 
lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow> 

1317 
dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)" 

1318 
apply(induct xs) 

1319 
apply simp 

1320 
apply auto 

1321 
apply(subst dropWhile_append2) 

1322 
apply auto 

1323 
done 

1324 

13114  1325 

15392  1326 
subsubsection {* @{text zip} *} 
13114  1327 

13142  1328 
lemma zip_Nil [simp]: "zip [] ys = []" 
13145  1329 
by (induct ys) auto 
13114  1330 

13142  1331 
lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys" 
13145  1332 
by simp 
13114  1333 

13142  1334 
declare zip_Cons [simp del] 
13114  1335 

15281  1336 
lemma zip_Cons1: 
1337 
"zip (x#xs) ys = (case ys of [] \<Rightarrow> []  y#ys \<Rightarrow> (x,y)#zip xs ys)" 

1338 
by(auto split:list.split) 

1339 

13142  1340 
lemma length_zip [simp]: 
13145  1341 
"!!xs. length (zip xs ys) = min (length xs) (length ys)" 
14208  1342 
apply (induct ys, simp) 
1343 
apply (case_tac xs, auto) 

13145  1344 
done 
13114  1345 

1346 
lemma zip_append1: 

13145  1347 
"!!xs. zip (xs @ ys) zs = 
1348 
zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" 

14208  1349 
apply (induct zs, simp) 
1350 
apply (case_tac xs, simp_all) 

13145  1351 
done 
13114  1352 

1353 
lemma zip_append2: 

13145  1354 
"!!ys. zip xs (ys @ zs) = 
1355 
zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" 

14208  1356 
apply (induct xs, simp) 
1357 
apply (case_tac ys, simp_all) 

13145  1358 
done 
13114  1359 

13142 