author  nipkow 
Wed, 08 May 2002 13:01:40 +0200  
changeset 13124  6e1decd8a7a9 
parent 13122  c63612ffb186 
child 13142  1ebd8ed5a1a0 
permissions  rwrr 
923  1 
(* Title: HOL/List.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1994 TU Muenchen 

5 
*) 

6 

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

9 
theory List = PreList: 

923  10 

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

13 
consts 

13114  14 
"@" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr 65) 
15 
filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" 

16 
concat :: "'a list list \<Rightarrow> 'a list" 

17 
foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" 

18 
foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" 

19 
hd :: "'a list \<Rightarrow> 'a" 

20 
tl :: "'a list \<Rightarrow> 'a list" 

21 
last :: "'a list \<Rightarrow> 'a" 

22 
butlast :: "'a list \<Rightarrow> 'a list" 

23 
set :: "'a list \<Rightarrow> 'a set" 

24 
list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)" 

25 
list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" 

26 
map :: "('a\<Rightarrow>'b) \<Rightarrow> ('a list \<Rightarrow> 'b list)" 

27 
mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl 55) 

28 
nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) 

29 
list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" 

30 
take :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" 

31 
drop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" 

32 
takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" 

33 
dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" 

34 
rev :: "'a list \<Rightarrow> 'a list" 

35 
zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list" 

36 
upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_../_'(])") 

37 
remdups :: "'a list \<Rightarrow> 'a list" 

38 
null :: "'a list \<Rightarrow> bool" 

39 
"distinct" :: "'a list \<Rightarrow> bool" 

40 
replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" 

923  41 

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

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

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

44 

923  45 
syntax 
46 
(* list Enumeration *) 

13114  47 
"@list" :: "args \<Rightarrow> 'a list" ("[(_)]") 
923  48 

2512  49 
(* Special syntax for filter *) 
13114  50 
"@filter" :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list" ("(1[_:_./ _])") 
923  51 

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

52 
(* list update *) 
13114  53 
"_lupdbind" :: "['a, 'a] \<Rightarrow> lupdbind" ("(2_ :=/ _)") 
54 
"" :: "lupdbind \<Rightarrow> lupdbinds" ("_") 

55 
"_lupdbinds" :: "[lupdbind, lupdbinds] \<Rightarrow> lupdbinds" ("_,/ _") 

56 
"_LUpdate" :: "['a, lupdbinds] \<Rightarrow> '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

57 

13114  58 
upto :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_../_])") 
5427  59 

923  60 
translations 
61 
"[x, xs]" == "x#[xs]" 

62 
"[x]" == "x#[]" 

3842  63 
"[x:xs . P]" == "filter (%x. P) xs" 
923  64 

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

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

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

67 

5427  68 
"[i..j]" == "[i..(Suc j)(]" 
69 

70 

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

71 
syntax (xsymbols) 
13114  72 
"@filter" :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list" ("(1[_\<in>_ ./ _])") 
2262  73 

74 

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

75 
consts 
13114  76 
lists :: "'a set \<Rightarrow> 'a list set" 
3342
ec3b55fcb165
New operator "lists" for formalizing sets of lists
paulson
parents:
3320
diff
changeset

77 

13114  78 
inductive "lists A" 
79 
intros 

80 
Nil: "[]: lists A" 

81 
Cons: "\<lbrakk> a: A; l: lists A \<rbrakk> \<Longrightarrow> a#l : lists A" 

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 

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

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

85 
list version as "length".*) 
13114  86 
syntax length :: "'a list \<Rightarrow> nat" 
87 
translations "length" => "size:: _ list \<Rightarrow> nat" 

88 

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

90 
typed_print_translation 

91 
{* 

92 
let 

93 
fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] = 

94 
Syntax.const "length" $ t 

95 
 size_tr' _ _ _ = raise Match; 

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

97 
*} 

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

98 

5183  99 
primrec 
1898  100 
"hd(x#xs) = x" 
5183  101 
primrec 
8972  102 
"tl([]) = []" 
1898  103 
"tl(x#xs) = xs" 
5183  104 
primrec 
8972  105 
"null([]) = True" 
106 
"null(x#xs) = False" 

107 
primrec 

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

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

111 
"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)" 
5183  112 
primrec 
8972  113 
"x mem [] = False" 
5518  114 
"x mem (y#ys) = (if y=x then True else x mem ys)" 
115 
primrec 

3465  116 
"set [] = {}" 
117 
"set (x#xs) = insert x (set xs)" 

5183  118 
primrec 
13114  119 
list_all_Nil: "list_all P [] = True" 
120 
list_all_Cons: "list_all P (x#xs) = (P(x) & list_all P xs)" 

5518  121 
primrec 
8972  122 
"map f [] = []" 
1898  123 
"map f (x#xs) = f(x)#map f xs" 
5183  124 
primrec 
13114  125 
append_Nil: "[] @ys = ys" 
126 
append_Cons: "(x#xs)@ys = x#(xs@ys)" 

5183  127 
primrec 
8972  128 
"rev([]) = []" 
1898  129 
"rev(x#xs) = rev(xs) @ [x]" 
5183  130 
primrec 
8972  131 
"filter P [] = []" 
1898  132 
"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" 
5183  133 
primrec 
13114  134 
foldl_Nil: "foldl f a [] = a" 
135 
foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs" 

5183  136 
primrec 
8972  137 
"foldr f [] a = a" 
8000  138 
"foldr f (x#xs) a = f x (foldr f xs a)" 
139 
primrec 

8972  140 
"concat([]) = []" 
2608  141 
"concat(x#xs) = x @ concat(xs)" 
5183  142 
primrec 
13114  143 
drop_Nil: "drop n [] = []" 
144 
drop_Cons: "drop n (x#xs) = (case n of 0 \<Rightarrow> x#xs  Suc(m) \<Rightarrow> drop m xs)" 

6408  145 
(* Warning: simpset does not contain this definition but separate theorems 
146 
for n=0 / n=Suc k*) 

5183  147 
primrec 
13114  148 
take_Nil: "take n [] = []" 
149 
take_Cons: "take n (x#xs) = (case n of 0 \<Rightarrow> []  Suc(m) \<Rightarrow> x # take m xs)" 

6408  150 
(* Warning: simpset does not contain this definition but separate theorems 
151 
for n=0 / n=Suc k*) 

152 
primrec 

13114  153 
nth_Cons: "(x#xs)!n = (case n of 0 \<Rightarrow> x  (Suc k) \<Rightarrow> xs!k)" 
6408  154 
(* Warning: simpset does not contain this definition but separate theorems 
155 
for n=0 / n=Suc k*) 

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

157 
" [][i:=v] = []" 
13114  158 
"(x#xs)[i:=v] = (case i of 0 \<Rightarrow> v # xs 
159 
 Suc j \<Rightarrow> x # xs[j:=v])" 

5183  160 
primrec 
8972  161 
"takeWhile P [] = []" 
2608  162 
"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" 
5183  163 
primrec 
8972  164 
"dropWhile P [] = []" 
3584
8f9ee0f79d9a
Corected bug in def of dropWhile (also present in Haskell lib!)
nipkow
parents:
3507
diff
changeset

165 
"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)" 
5183  166 
primrec 
4132  167 
"zip xs [] = []" 
13114  168 
zip_Cons: 
169 
"zip xs (y#ys) = (case xs of [] \<Rightarrow> []  z#zs \<Rightarrow> (z,y)#zip zs ys)" 

6408  170 
(* Warning: simpset does not contain this definition but separate theorems 
171 
for xs=[] / xs=z#zs *) 

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

5183  175 
primrec 
12887  176 
"distinct [] = True" 
177 
"distinct (x#xs) = (x ~: set xs & distinct xs)" 

5183  178 
primrec 
4605  179 
"remdups [] = []" 
180 
"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)" 

5183  181 
primrec 
13114  182 
replicate_0: "replicate 0 x = []" 
183 
replicate_Suc: "replicate (Suc n) x = x # replicate n x" 

8115  184 
defs 
13114  185 
list_all2_def: 
8115  186 
"list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)" 
187 

3196  188 

6408  189 
(** Lexicographic orderings on lists **) 
5281  190 

191 
consts 

13114  192 
lexn :: "('a * 'a)set \<Rightarrow> nat \<Rightarrow> ('a list * 'a list)set" 
5281  193 
primrec 
194 
"lexn r 0 = {}" 

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

198 
constdefs 

13114  199 
lex :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set" 
9336  200 
"lex r == UN n. lexn r n" 
5281  201 

13114  202 
lexico :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set" 
9336  203 
"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))" 
204 

13114  205 
sublist :: "['a list, nat set] \<Rightarrow> 'a list" 
9336  206 
"sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))" 
5281  207 

13114  208 

209 
lemma not_Cons_self[simp]: "\<And>x. xs ~= x#xs" 

210 
by(induct_tac "xs", auto) 

211 

212 
lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym] 

213 

13122  214 
lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)" 
13114  215 
by(induct_tac "xs", auto) 
216 

217 
(* Induction over the length of a list: *) 

218 
(* "(!!xs. (!ys. length ys < length xs > P ys) ==> P xs) ==> P(xs)" *) 

219 
lemmas length_induct = measure_induct[of length] 

220 

221 

222 
(** "lists": the listforming operator over sets **) 

223 

224 
lemma lists_mono: "A<=B ==> lists A <= lists B" 

225 
apply(unfold lists.defs) 

226 
apply(blast intro!:lfp_mono) 

227 
done 

228 

229 
inductive_cases listsE[elim!]: "x#l : lists A" 

230 
declare lists.intros[intro!] 

231 

232 
lemma lists_IntI[rule_format]: 

13122  233 
"l: lists A ==> l: lists B > l: lists (A Int B)" 
13114  234 
apply(erule lists.induct) 
235 
apply blast+ 

236 
done 

237 

238 
lemma lists_Int_eq[simp]: "lists (A Int B) = lists A Int lists B" 

239 
apply(rule mono_Int[THEN equalityI]) 

240 
apply(simp add:mono_def lists_mono) 

241 
apply(blast intro!: lists_IntI) 

242 
done 

243 

244 
lemma append_in_lists_conv[iff]: 

245 
"(xs@ys : lists A) = (xs : lists A & ys : lists A)" 

246 
by(induct_tac "xs", auto) 

247 

248 
(** length **) 

249 
(* needs to come before "@" because of thm append_eq_append_conv *) 

250 

251 
section "length" 

252 

253 
lemma length_append[simp]: "length(xs@ys) = length(xs)+length(ys)" 

254 
by(induct_tac "xs", auto) 

255 

256 
lemma length_map[simp]: "length (map f xs) = length xs" 

257 
by(induct_tac "xs", auto) 

258 

259 
lemma length_rev[simp]: "length(rev xs) = length(xs)" 

260 
by(induct_tac "xs", auto) 

261 

262 
lemma length_tl[simp]: "length(tl xs) = (length xs)  1" 

263 
by(case_tac "xs", auto) 

264 

265 
lemma length_0_conv[iff]: "(length xs = 0) = (xs = [])" 

266 
by(induct_tac "xs", auto) 

267 

268 
lemma length_greater_0_conv[iff]: "(0 < length xs) = (xs ~= [])" 

269 
by(induct_tac xs, auto) 

270 

271 
lemma length_Suc_conv: 

272 
"(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)" 

273 
by(induct_tac "xs", auto) 

274 

275 
(** @  append **) 

276 

277 
section "@  append" 

278 

279 
lemma append_assoc[simp]: "(xs@ys)@zs = xs@(ys@zs)" 

280 
by(induct_tac "xs", auto) 

3507  281 

13114  282 
lemma append_Nil2[simp]: "xs @ [] = xs" 
283 
by(induct_tac "xs", auto) 

284 

285 
lemma append_is_Nil_conv[iff]: "(xs@ys = []) = (xs=[] & ys=[])" 

286 
by(induct_tac "xs", auto) 

287 

288 
lemma Nil_is_append_conv[iff]: "([] = xs@ys) = (xs=[] & ys=[])" 

289 
by(induct_tac "xs", auto) 

290 

291 
lemma append_self_conv[iff]: "(xs @ ys = xs) = (ys=[])" 

292 
by(induct_tac "xs", auto) 

293 

294 
lemma self_append_conv[iff]: "(xs = xs @ ys) = (ys=[])" 

295 
by(induct_tac "xs", auto) 

296 

297 
lemma append_eq_append_conv[rule_format,simp]: 

298 
"!ys. length xs = length ys  length us = length vs 

299 
> (xs@us = ys@vs) = (xs=ys & us=vs)" 

300 
apply(induct_tac "xs") 

301 
apply(rule allI) 

302 
apply(case_tac "ys") 

303 
apply simp 

304 
apply force 

305 
apply(rule allI) 

306 
apply(case_tac "ys") 

307 
apply force 

308 
apply simp 

309 
done 

310 

311 
lemma same_append_eq[iff]: "(xs @ ys = xs @ zs) = (ys=zs)" 

312 
by simp 

313 

314 
lemma append1_eq_conv[iff]: "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)" 

315 
by simp 

316 

317 
lemma append_same_eq[iff]: "(ys @ xs = zs @ xs) = (ys=zs)" 

318 
by simp 

3507  319 

13114  320 
lemma append_self_conv2[iff]: "(xs @ ys = ys) = (xs=[])" 
321 
by(insert append_same_eq[of _ _ "[]"], auto) 

322 

323 
lemma self_append_conv2[iff]: "(ys = xs @ ys) = (xs=[])" 

324 
by(auto simp add: append_same_eq[of "[]", simplified]) 

325 

326 
lemma hd_Cons_tl[rule_format,simp]: "xs ~= [] > hd xs # tl xs = xs" 

327 
by(induct_tac "xs", auto) 

328 

329 
lemma hd_append: "hd(xs@ys) = (if xs=[] then hd ys else hd xs)" 

330 
by(induct_tac "xs", auto) 

331 

332 
lemma hd_append2[simp]: "xs ~= [] ==> hd(xs @ ys) = hd xs" 

333 
by(simp add: hd_append split: list.split) 

334 

335 
lemma tl_append: "tl(xs@ys) = (case xs of [] => tl(ys)  z#zs => zs@ys)" 

336 
by(simp split: list.split) 

337 

338 
lemma tl_append2[simp]: "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys" 

339 
by(simp add: tl_append split: list.split) 

340 

341 
(* trivial rules for solving @equations automatically *) 

342 

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

344 
by simp 

345 

346 
lemma Cons_eq_appendI: "[ x#xs1 = ys; xs = xs1 @ zs ] ==> x#xs = ys@zs" 

347 
by(drule sym, simp) 

348 

349 
lemma append_eq_appendI: "[ xs@xs1 = zs; ys = xs1 @ us ] ==> xs@ys = zs@us" 

350 
by(drule sym, simp) 

351 

352 

353 
(*** 

354 
Simplification procedure for all list equalities. 

355 
Currently only tries to rearrange @ to see if 

356 
 both lists end in a singleton list, 

357 
 or both lists end in the same list. 

358 
***) 

359 
ML_setup{* 

3507  360 
local 
361 

13122  362 
val append_assoc = thm "append_assoc"; 
363 
val append_Nil = thm "append_Nil"; 

364 
val append_Cons = thm "append_Cons"; 

365 
val append1_eq_conv = thm "append1_eq_conv"; 

366 
val append_same_eq = thm "append_same_eq"; 

367 

13114  368 
val list_eq_pattern = 
369 
Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT) 

370 

371 
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = 

372 
(case xs of Const("List.list.Nil",_) => cons  _ => last xs) 

373 
 last (Const("List.op @",_) $ _ $ ys) = last ys 

374 
 last t = t 

375 

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

377 
 list1 _ = false 

378 

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

380 
(case xs of Const("List.list.Nil",_) => xs  _ => cons $ butlast xs) 

381 
 butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys 

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

383 

384 
val rearr_tac = 

385 
simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]) 

386 

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

388 
let 

389 
val lastl = last lhs and lastr = last rhs 

390 
fun rearr conv = 

391 
let val lhs1 = butlast lhs and rhs1 = butlast rhs 

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

393 
val appT = [listT,listT] > listT 

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

395 
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr) 

396 
val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2))) 

397 
val thm = prove_goalw_cterm [] ct (K [rearr_tac 1]) 

398 
handle ERROR => 

399 
error("The error(s) above occurred while trying to prove " ^ 

400 
string_of_cterm ct) 

401 
in Some((conv RS (thm RS trans)) RS eq_reflection) end 

402 

403 
in if list1 lastl andalso list1 lastr 

404 
then rearr append1_eq_conv 

405 
else 

406 
if lastl aconv lastr 

407 
then rearr append_same_eq 

408 
else None 

409 
end 

410 
in 

411 
val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq 

412 
end; 

413 

414 
Addsimprocs [list_eq_simproc]; 

415 
*} 

416 

417 

418 
(** map **) 

419 

420 
section "map" 

421 

422 
lemma map_ext: "(\<And>x. x : set xs \<longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g xs" 

423 
by (induct xs, simp_all) 

424 

425 
lemma map_ident[simp]: "map (%x. x) = (%xs. xs)" 

426 
by(rule ext, induct_tac "xs", auto) 

427 

428 
lemma map_append[simp]: "map f (xs@ys) = map f xs @ map f ys" 

429 
by(induct_tac "xs", auto) 

430 

431 
lemma map_compose(*[simp]*): "map (f o g) xs = map f (map g xs)" 

432 
by(unfold o_def, induct_tac "xs", auto) 

433 

434 
lemma rev_map: "rev(map f xs) = map f (rev xs)" 

435 
by(induct_tac xs, auto) 

436 

437 
(* a congruence rule for map: *) 

438 
lemma map_cong: 

439 
"xs=ys ==> (!!x. x : set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys" 

440 
by (clarify, induct ys, auto) 

441 

442 
lemma map_is_Nil_conv[iff]: "(map f xs = []) = (xs = [])" 

443 
by(case_tac xs, auto) 

444 

445 
lemma Nil_is_map_conv[iff]: "([] = map f xs) = (xs = [])" 

446 
by(case_tac xs, auto) 

447 

448 
lemma map_eq_Cons: 

449 
"(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)" 

450 
by(case_tac xs, auto) 

451 

452 
lemma map_injective: 

453 
"\<And>xs. map f xs = map f ys \<Longrightarrow> (!x y. f x = f y > x=y) \<Longrightarrow> xs=ys" 

454 
by(induct "ys", simp, fastsimp simp add:map_eq_Cons) 

455 

456 
lemma inj_mapI: "inj f ==> inj (map f)" 

457 
by(blast dest:map_injective injD intro:injI) 

458 

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

460 
apply(unfold inj_on_def) 

461 
apply clarify 

462 
apply(erule_tac x = "[x]" in ballE) 

463 
apply(erule_tac x = "[y]" in ballE) 

464 
apply simp 

465 
apply blast 

466 
apply blast 

467 
done 

468 

469 
lemma inj_map: "inj (map f) = inj f" 

470 
by(blast dest:inj_mapD intro:inj_mapI) 

471 

472 
(** rev **) 

473 

474 
section "rev" 

475 

476 
lemma rev_append[simp]: "rev(xs@ys) = rev(ys) @ rev(xs)" 

477 
by(induct_tac xs, auto) 

478 

479 
lemma rev_rev_ident[simp]: "rev(rev xs) = xs" 

480 
by(induct_tac xs, auto) 

481 

482 
lemma rev_is_Nil_conv[iff]: "(rev xs = []) = (xs = [])" 

483 
by(induct_tac xs, auto) 

484 

485 
lemma Nil_is_rev_conv[iff]: "([] = rev xs) = (xs = [])" 

486 
by(induct_tac xs, auto) 

487 

488 
lemma rev_is_rev_conv[iff]: "!!ys. (rev xs = rev ys) = (xs = ys)" 

489 
apply(induct "xs" ) 

490 
apply force 

491 
apply(case_tac ys) 

492 
apply simp 

493 
apply force 

494 
done 

495 

496 
lemma rev_induct: "[ P []; !!x xs. P xs ==> P(xs@[x]) ] ==> P xs" 

497 
apply(subst rev_rev_ident[symmetric]) 

498 
apply(rule_tac list = "rev xs" in list.induct, simp_all) 

499 
done 

500 

501 
(* Instead of (rev_induct_tac xs) use (induct_tac xs rule: rev_induct) *) 

502 

503 
lemma rev_exhaust: "(xs = [] \<Longrightarrow> P) \<Longrightarrow> (!!ys y. xs = ys@[y] \<Longrightarrow> P) \<Longrightarrow> P" 

504 
by(induct xs rule: rev_induct, auto) 

505 

506 

507 
(** set **) 

508 

509 
section "set" 

510 

511 
lemma finite_set[iff]: "finite (set xs)" 

512 
by(induct_tac xs, auto) 

513 

514 
lemma set_append[simp]: "set (xs@ys) = (set xs Un set ys)" 

515 
by(induct_tac xs, auto) 

516 

517 
lemma set_subset_Cons: "set xs \<subseteq> set (x#xs)" 

518 
by auto 

519 

520 
lemma set_empty[iff]: "(set xs = {}) = (xs = [])" 

521 
by(induct_tac xs, auto) 

522 

523 
lemma set_rev[simp]: "set(rev xs) = set(xs)" 

524 
by(induct_tac xs, auto) 

525 

526 
lemma set_map[simp]: "set(map f xs) = f`(set xs)" 

527 
by(induct_tac xs, auto) 

528 

529 
lemma set_filter[simp]: "set(filter P xs) = {x. x : set xs & P x}" 

530 
by(induct_tac xs, auto) 

531 

532 
lemma set_upt[simp]: "set[i..j(] = {k. i <= k & k < j}" 

533 
apply(induct_tac j) 

534 
apply simp_all 

535 
apply(erule ssubst) 

536 
apply auto 

537 
apply arith 

538 
done 

539 

540 
lemma in_set_conv_decomp: "(x : set xs) = (? ys zs. xs = ys@x#zs)" 

541 
apply(induct_tac "xs") 

542 
apply simp 

543 
apply simp 

544 
apply(rule iffI) 

545 
apply(blast intro: eq_Nil_appendI Cons_eq_appendI) 

546 
apply(erule exE)+ 

547 
apply(case_tac "ys") 

548 
apply auto 

549 
done 

550 

551 

552 
(* eliminate `lists' in favour of `set' *) 

553 

554 
lemma in_lists_conv_set: "(xs : lists A) = (!x : set xs. x : A)" 

555 
by(induct_tac xs, auto) 

556 

557 
lemmas in_listsD[dest!] = in_lists_conv_set[THEN iffD1] 

558 
lemmas in_listsI[intro!] = in_lists_conv_set[THEN iffD2] 

559 

560 

561 
(** mem **) 

562 

563 
section "mem" 

564 

565 
lemma set_mem_eq: "(x mem xs) = (x : set xs)" 

566 
by(induct_tac xs, auto) 

567 

568 

569 
(** list_all **) 

570 

571 
section "list_all" 

572 

573 
lemma list_all_conv: "list_all P xs = (!x:set xs. P x)" 

574 
by(induct_tac xs, auto) 

575 

576 
lemma list_all_append[simp]: 

577 
"list_all P (xs@ys) = (list_all P xs & list_all P ys)" 

578 
by(induct_tac xs, auto) 

579 

580 

581 
(** filter **) 

582 

583 
section "filter" 

584 

585 
lemma filter_append[simp]: "filter P (xs@ys) = filter P xs @ filter P ys" 

586 
by(induct_tac xs, auto) 

587 

588 
lemma filter_filter[simp]: "filter P (filter Q xs) = filter (%x. Q x & P x) xs" 

589 
by(induct_tac xs, auto) 

590 

591 
lemma filter_True[simp]: "!x : set xs. P x \<Longrightarrow> filter P xs = xs" 

592 
by(induct xs, auto) 

593 

594 
lemma filter_False[simp]: "!x : set xs. ~P x \<Longrightarrow> filter P xs = []" 

595 
by(induct xs, auto) 

596 

597 
lemma length_filter[simp]: "length (filter P xs) <= length xs" 

598 
by(induct xs, auto simp add: le_SucI) 

599 

600 
lemma filter_is_subset[simp]: "set (filter P xs) <= set xs" 

601 
by auto 

602 

603 

604 
section "concat" 

605 

606 
lemma concat_append[simp]: "concat(xs@ys) = concat(xs)@concat(ys)" 

607 
by(induct xs, auto) 

608 

609 
lemma concat_eq_Nil_conv[iff]: "(concat xss = []) = (!xs:set xss. xs=[])" 

610 
by(induct xss, auto) 

611 

612 
lemma Nil_eq_concat_conv[iff]: "([] = concat xss) = (!xs:set xss. xs=[])" 

613 
by(induct xss, auto) 

614 

615 
lemma set_concat[simp]: "set(concat xs) = Union(set ` set xs)" 

616 
by(induct xs, auto) 

617 

618 
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 

619 
by(induct xs, auto) 

620 

621 
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 

622 
by(induct xs, auto) 

623 

624 
lemma rev_concat: "rev(concat xs) = concat (map rev (rev xs))" 

625 
by(induct xs, auto) 

626 

627 
(** nth **) 

628 

629 
section "nth" 

630 

631 
lemma nth_Cons_0[simp]: "(x#xs)!0 = x" 

632 
by auto 

633 

634 
lemma nth_Cons_Suc[simp]: "(x#xs)!(Suc n) = xs!n" 

635 
by auto 

636 

637 
declare nth.simps[simp del] 

638 

639 
lemma nth_append: 

640 
"!!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n  length xs))" 

641 
apply(induct "xs") 

642 
apply simp 

643 
apply(case_tac "n" ) 

644 
apply auto 

645 
done 

646 

647 
lemma nth_map[simp]: "!!n. n < length xs \<Longrightarrow> (map f xs)!n = f(xs!n)" 

648 
apply(induct "xs" ) 

649 
apply simp 

650 
apply(case_tac "n") 

651 
apply auto 

652 
done 

653 

654 
lemma set_conv_nth: "set xs = {xs!i i. i < length xs}" 

655 
apply(induct_tac "xs") 

656 
apply simp 

657 
apply simp 

658 
apply safe 

659 
apply(rule_tac x = 0 in exI) 

660 
apply simp 

661 
apply(rule_tac x = "Suc i" in exI) 

662 
apply simp 

663 
apply(case_tac "i") 

664 
apply simp 

665 
apply(rename_tac "j") 

666 
apply(rule_tac x = "j" in exI) 

667 
apply simp 

668 
done 

669 

670 
lemma list_ball_nth: "\<lbrakk> n < length xs; !x : set xs. P x \<rbrakk> \<Longrightarrow> P(xs!n)" 

671 
by(simp add:set_conv_nth, blast) 

672 

673 
lemma nth_mem[simp]: "n < length xs ==> xs!n : set xs" 

674 
by(simp add:set_conv_nth, blast) 

675 

676 
lemma all_nth_imp_all_set: 

677 
"\<lbrakk> !i < length xs. P(xs!i); x : set xs \<rbrakk> \<Longrightarrow> P x" 

678 
by(simp add:set_conv_nth, blast) 

679 

680 
lemma all_set_conv_all_nth: 

681 
"(!x : set xs. P x) = (!i. i<length xs > P (xs ! i))" 

682 
by(simp add:set_conv_nth, blast) 

683 

684 

685 
(** list update **) 

686 

687 
section "list update" 

688 

689 
lemma length_list_update[simp]: "!!i. length(xs[i:=x]) = length xs" 

690 
by(induct xs, simp, simp split:nat.split) 

691 

692 
lemma nth_list_update: 

693 
"!!i j. i < length xs \<Longrightarrow> (xs[i:=x])!j = (if i=j then x else xs!j)" 

694 
by(induct xs, simp, auto simp add:nth_Cons split:nat.split) 

695 

696 
lemma nth_list_update_eq[simp]: "i < length xs ==> (xs[i:=x])!i = x" 

697 
by(simp add:nth_list_update) 

698 

699 
lemma nth_list_update_neq[simp]: "!!i j. i ~= j \<Longrightarrow> xs[i:=x]!j = xs!j" 

700 
by(induct xs, simp, auto simp add:nth_Cons split:nat.split) 

701 

702 
lemma list_update_overwrite[simp]: 

703 
"!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]" 

704 
by(induct xs, simp, simp split:nat.split) 

705 

706 
lemma list_update_same_conv: 

707 
"!!i. i < length xs \<Longrightarrow> (xs[i := x] = xs) = (xs!i = x)" 

708 
by(induct xs, simp, simp split:nat.split, blast) 

709 

710 
lemma update_zip: 

711 
"!!i xy xs. length xs = length ys \<Longrightarrow> 

712 
(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])" 

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

714 

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

716 
by(induct xs, simp, simp split:nat.split, fast) 

717 

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

719 
by(fast dest!:set_update_subset_insert[THEN subsetD]) 

720 

721 

722 
(** last & butlast **) 

723 

724 
section "last / butlast" 

725 

726 
lemma last_snoc[simp]: "last(xs@[x]) = x" 

727 
by(induct xs, auto) 

728 

729 
lemma butlast_snoc[simp]:"butlast(xs@[x]) = xs" 

730 
by(induct xs, auto) 

731 

732 
lemma length_butlast[simp]: "length(butlast xs) = length xs  1" 

733 
by(induct xs rule:rev_induct, auto) 

734 

735 
lemma butlast_append: 

736 
"!!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)" 

737 
by(induct xs, auto) 

738 

739 
lemma append_butlast_last_id[simp]: 

740 
"xs ~= [] > butlast xs @ [last xs] = xs" 

741 
by(induct xs, auto) 

742 

743 
lemma in_set_butlastD: "x:set(butlast xs) ==> x:set xs" 

744 
by(induct xs, auto split:split_if_asm) 

745 

746 
lemma in_set_butlast_appendI: 

747 
"x:set(butlast xs)  x:set(butlast ys) ==> x:set(butlast(xs@ys))" 

748 
by(auto dest:in_set_butlastD simp add:butlast_append) 

749 

750 
(** take & drop **) 

751 
section "take & drop" 

752 

753 
lemma take_0[simp]: "take 0 xs = []" 

754 
by(induct xs, auto) 

755 

756 
lemma drop_0[simp]: "drop 0 xs = xs" 

757 
by(induct xs, auto) 

758 

759 
lemma take_Suc_Cons[simp]: "take (Suc n) (x#xs) = x # take n xs" 

760 
by simp 

761 

762 
lemma drop_Suc_Cons[simp]: "drop (Suc n) (x#xs) = drop n xs" 

763 
by simp 

764 

765 
declare take_Cons[simp del] drop_Cons[simp del] 

766 

767 
lemma length_take[simp]: "!!xs. length(take n xs) = min (length xs) n" 

768 
by(induct n, auto, case_tac xs, auto) 

769 

770 
lemma length_drop[simp]: "!!xs. length(drop n xs) = (length xs  n)" 

771 
by(induct n, auto, case_tac xs, auto) 

772 

773 
lemma take_all[simp]: "!!xs. length xs <= n ==> take n xs = xs" 

774 
by(induct n, auto, case_tac xs, auto) 

775 

776 
lemma drop_all[simp]: "!!xs. length xs <= n ==> drop n xs = []" 

777 
by(induct n, auto, case_tac xs, auto) 

778 

779 
lemma take_append[simp]: 

780 
"!!xs. take n (xs @ ys) = (take n xs @ take (n  length xs) ys)" 

781 
by(induct n, auto, case_tac xs, auto) 

782 

783 
lemma drop_append[simp]: 

784 
"!!xs. drop n (xs@ys) = drop n xs @ drop (n  length xs) ys" 

785 
by(induct n, auto, case_tac xs, auto) 

786 

787 
lemma take_take[simp]: "!!xs n. take n (take m xs) = take (min n m) xs" 

788 
apply(induct m) 

789 
apply auto 

790 
apply(case_tac xs) 

791 
apply auto 

792 
apply(case_tac na) 

793 
apply auto 

794 
done 

795 

796 
lemma drop_drop[simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs" 

797 
apply(induct m) 

798 
apply auto 

799 
apply(case_tac xs) 

800 
apply auto 

801 
done 

802 

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

804 
apply(induct m) 

805 
apply auto 

806 
apply(case_tac xs) 

807 
apply auto 

808 
done 

809 

810 
lemma append_take_drop_id[simp]: "!!xs. take n xs @ drop n xs = xs" 

811 
apply(induct n) 

812 
apply auto 

813 
apply(case_tac xs) 

814 
apply auto 

815 
done 

816 

817 
lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)" 

818 
apply(induct n) 

819 
apply auto 

820 
apply(case_tac xs) 

821 
apply auto 

822 
done 

823 

824 
lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" 

825 
apply(induct n) 

826 
apply auto 

827 
apply(case_tac xs) 

828 
apply auto 

829 
done 

830 

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

832 
apply(induct xs) 

833 
apply auto 

834 
apply(case_tac i) 

835 
apply auto 

836 
done 

837 

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

839 
apply(induct xs) 

840 
apply auto 

841 
apply(case_tac i) 

842 
apply auto 

843 
done 

844 

845 
lemma nth_take[simp]: "!!n i. i < n ==> (take n xs)!i = xs!i" 

846 
apply(induct xs) 

847 
apply auto 

848 
apply(case_tac n) 

849 
apply(blast ) 

850 
apply(case_tac i) 

851 
apply auto 

852 
done 

853 

854 
lemma nth_drop[simp]: "!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n+i)" 

855 
apply(induct n) 

856 
apply auto 

857 
apply(case_tac xs) 

858 
apply auto 

859 
done 

3507  860 

13114  861 
lemma append_eq_conv_conj: 
862 
"!!zs. (xs@ys = zs) = (xs = take (length xs) zs & ys = drop (length xs) zs)" 

863 
apply(induct xs) 

864 
apply simp 

865 
apply clarsimp 

866 
apply(case_tac zs) 

867 
apply auto 

868 
done 

869 

870 
(** takeWhile & dropWhile **) 

871 

872 
section "takeWhile & dropWhile" 

873 

874 
lemma takeWhile_dropWhile_id[simp]: "takeWhile P xs @ dropWhile P xs = xs" 

875 
by(induct xs, auto) 

876 

877 
lemma takeWhile_append1[simp]: 

878 
"\<lbrakk> x:set xs; ~P(x) \<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs" 

879 
by(induct xs, auto) 

880 

881 
lemma takeWhile_append2[simp]: 

882 
"(!!x. x : set xs \<Longrightarrow> P(x)) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys" 

883 
by(induct xs, auto) 

884 

885 
lemma takeWhile_tail: "~P(x) ==> takeWhile P (xs @ (x#l)) = takeWhile P xs" 

886 
by(induct xs, auto) 

887 

888 
lemma dropWhile_append1[simp]: 

889 
"\<lbrakk> x : set xs; ~P(x) \<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" 

890 
by(induct xs, auto) 

891 

892 
lemma dropWhile_append2[simp]: 

893 
"(!!x. x:set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" 

894 
by(induct xs, auto) 

895 

896 
lemma set_take_whileD: "x:set(takeWhile P xs) ==> x:set xs & P x" 

897 
by(induct xs, auto split:split_if_asm) 

898 

899 

900 
(** zip **) 

901 
section "zip" 

902 

903 
lemma zip_Nil[simp]: "zip [] ys = []" 

904 
by(induct ys, auto) 

905 

906 
lemma zip_Cons_Cons[simp]: "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 

907 
by simp 

908 

909 
declare zip_Cons[simp del] 

910 

911 
lemma length_zip[simp]: 

912 
"!!xs. length (zip xs ys) = min (length xs) (length ys)" 

913 
apply(induct ys) 

914 
apply simp 

915 
apply(case_tac xs) 

916 
apply auto 

917 
done 

918 

919 
lemma zip_append1: 

920 
"!!xs. zip (xs@ys) zs = 

921 
zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" 

922 
apply(induct zs) 

923 
apply simp 

924 
apply(case_tac xs) 

925 
apply simp_all 

926 
done 

927 

928 
lemma zip_append2: 

929 
"!!ys. zip xs (ys@zs) = 

930 
zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" 

931 
apply(induct xs) 

932 
apply simp 

933 
apply(case_tac ys) 

934 
apply simp_all 

935 
done 

936 

937 
lemma zip_append[simp]: 

938 
"[ length xs = length us; length ys = length vs ] ==> \ 

939 
\ zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" 

940 
by(simp add: zip_append1) 

941 

942 
lemma zip_rev: 

943 
"!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" 

944 
apply(induct ys) 

945 
apply simp 

946 
apply(case_tac xs) 

947 
apply simp_all 

948 
done 

949 

950 
lemma nth_zip[simp]: 

951 
"!!i xs. \<lbrakk> i < length xs; i < length ys \<rbrakk> \<Longrightarrow> (zip xs ys)!i = (xs!i, ys!i)" 

952 
apply(induct ys) 

953 
apply simp 

954 
apply(case_tac xs) 

955 
apply (simp_all add: nth.simps split:nat.split) 

956 
done 

957 

958 
lemma set_zip: 

959 
"set(zip xs ys) = {(xs!i,ys!i) i. i < min (length xs) (length ys)}" 

960 
by(simp add: set_conv_nth cong: rev_conj_cong) 

961 

962 
lemma zip_update: 

963 
"length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]" 

964 
by(rule sym, simp add: update_zip) 

965 

966 
lemma zip_replicate[simp]: 

967 
"!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)" 

968 
apply(induct i) 

969 
apply auto 

970 
apply(case_tac j) 

971 
apply auto 

972 
done 

973 

974 
(** list_all2 **) 

975 
section "list_all2" 

976 

977 
lemma list_all2_lengthD: "list_all2 P xs ys ==> length xs = length ys" 

978 
by(simp add:list_all2_def) 

979 

980 
lemma list_all2_Nil[iff]: "list_all2 P [] ys = (ys=[])" 

981 
by(simp add:list_all2_def) 

982 

983 
lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs=[])" 

984 
by(simp add:list_all2_def) 

985 

986 
lemma list_all2_Cons[iff]: 

987 
"list_all2 P (x#xs) (y#ys) = (P x y & list_all2 P xs ys)" 

988 
by(auto simp add:list_all2_def) 

989 

990 
lemma list_all2_Cons1: 

991 
"list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)" 

992 
by(case_tac ys, auto) 

993 

994 
lemma list_all2_Cons2: 

995 
"list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)" 

996 
by(case_tac xs, auto) 

997 

998 
lemma list_all2_rev[iff]: 

999 
"list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" 

1000 
by(simp add:list_all2_def zip_rev cong:conj_cong) 

1001 

1002 
lemma list_all2_append1: 

1003 
"list_all2 P (xs@ys) zs = 

1004 
(EX us vs. zs = us@vs & length us = length xs & length vs = length ys & 

1005 
list_all2 P xs us & list_all2 P ys vs)" 

1006 
apply(simp add:list_all2_def zip_append1) 

1007 
apply(rule iffI) 

1008 
apply(rule_tac x = "take (length xs) zs" in exI) 

1009 
apply(rule_tac x = "drop (length xs) zs" in exI) 

1010 
apply(force split: nat_diff_split simp add:min_def) 

1011 
apply clarify 

1012 
apply(simp add: ball_Un) 

1013 
done 

1014 

1015 
lemma list_all2_append2: 

1016 
"list_all2 P xs (ys@zs) = 

1017 
(EX us vs. xs = us@vs & length us = length ys & length vs = length zs & 

1018 
list_all2 P us ys & list_all2 P vs zs)" 

1019 
apply(simp add:list_all2_def zip_append2) 

1020 
apply(rule iffI) 

1021 
apply(rule_tac x = "take (length ys) xs" in exI) 

1022 
apply(rule_tac x = "drop (length ys) xs" in exI) 

1023 
apply(force split: nat_diff_split simp add:min_def) 

1024 
apply clarify 

1025 
apply(simp add: ball_Un) 

1026 
done 

1027 

1028 
lemma list_all2_conv_all_nth: 

1029 
"list_all2 P xs ys = 

1030 
(length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))" 

1031 
by(force simp add:list_all2_def set_zip) 

1032 

1033 
lemma list_all2_trans[rule_format]: 

1034 
"ALL a b c. P1 a b > P2 b c > P3 a c ==> 

1035 
ALL bs cs. list_all2 P1 as bs > list_all2 P2 bs cs > list_all2 P3 as cs" 

1036 
apply(induct_tac as) 

1037 
apply simp 

1038 
apply(rule allI) 

1039 
apply(induct_tac bs) 

1040 
apply simp 

1041 
apply(rule allI) 

1042 
apply(induct_tac cs) 

1043 
apply auto 

1044 
done 

1045 

1046 

1047 
section "foldl" 

1048 

1049 
lemma foldl_append[simp]: 

1050 
"!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" 

1051 
by(induct xs, auto) 

1052 

1053 
(* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use 

1054 
because it requires an additional transitivity step 

1055 
*) 

1056 
lemma start_le_sum: "!!n::nat. m <= n ==> m <= foldl op+ n ns" 

1057 
by(induct ns, auto) 

1058 

1059 
lemma elem_le_sum: "!!n::nat. n : set ns ==> n <= foldl op+ 0 ns" 

1060 
by(force intro: start_le_sum simp add:in_set_conv_decomp) 

1061 

1062 
lemma sum_eq_0_conv[iff]: 

1063 
"!!m::nat. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))" 

1064 
by(induct ns, auto) 

1065 

1066 
(** upto **) 

1067 

1068 
(* Does not terminate! *) 

1069 
lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])" 

1070 
by(induct j, auto) 

1071 

1072 
lemma upt_conv_Nil[simp]: "j<=i ==> [i..j(] = []" 

1073 
by(subst upt_rec, simp) 

1074 

1075 
(*Only needed if upt_Suc is deleted from the simpset*) 

1076 
lemma upt_Suc_append: "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]" 

1077 
by simp 

1078 

1079 
lemma upt_conv_Cons: "i<j ==> [i..j(] = i#[Suc i..j(]" 

1080 
apply(rule trans) 

1081 
apply(subst upt_rec) 

1082 
prefer 2 apply(rule refl) 

1083 
apply simp 

1084 
done 

1085 

1086 
(*LOOPS as a simprule, since j<=j*) 

1087 
lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]" 

1088 
by(induct_tac "k", auto) 

1089 

1090 
lemma length_upt[simp]: "length [i..j(] = ji" 

1091 
by(induct_tac j, simp, simp add: Suc_diff_le) 

1092 

1093 
lemma nth_upt[simp]: "i+k < j ==> [i..j(] ! k = i+k" 

1094 
apply(induct j) 

1095 
apply(auto simp add: less_Suc_eq nth_append split:nat_diff_split) 

1096 
done 

1097 

1098 
lemma take_upt[simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]" 

1099 
apply(induct m) 

1100 
apply simp 

1101 
apply(subst upt_rec) 

1102 
apply(rule sym) 

1103 
apply(subst upt_rec) 

1104 
apply(simp del: upt.simps) 

1105 
done 

3507  1106 

13114  1107 
lemma map_Suc_upt: "map Suc [m..n(] = [Suc m..n]" 
1108 
by(induct n, auto) 

1109 

1110 
lemma nth_map_upt: "!!i. i < nm ==> (map f [m..n(]) ! i = f(m+i)" 

1111 
thm diff_induct 

1112 
apply(induct n m rule: diff_induct) 

1113 
prefer 3 apply(subst map_Suc_upt[symmetric]) 

1114 
apply(auto simp add: less_diff_conv nth_upt) 

1115 
done 

1116 

1117 
lemma nth_take_lemma[rule_format]: 

1118 
"ALL xs ys. k <= length xs > k <= length ys 

1119 
> (ALL i. i < k > xs!i = ys!i) 

1120 
> take k xs = take k ys" 

1121 
apply(induct_tac k) 

1122 
apply(simp_all add: less_Suc_eq_0_disj all_conj_distrib) 

1123 
apply clarify 

1124 
(*Both lists must be nonempty*) 

1125 
apply(case_tac xs) 

1126 
apply simp 

1127 
apply(case_tac ys) 

1128 
apply clarify 

1129 
apply(simp (no_asm_use)) 

1130 
apply clarify 

1131 
(*prenexing's needed, not miniscoping*) 

1132 
apply(simp (no_asm_use) add: all_simps[symmetric] del: all_simps) 

1133 
apply blast 

1134 
(*prenexing's needed, not miniscoping*) 

1135 
done 

1136 

1137 
lemma nth_equalityI: 

1138 
"[ length xs = length ys; ALL i < length xs. xs!i = ys!i ] ==> xs = ys" 

1139 
apply(frule nth_take_lemma[OF le_refl eq_imp_le]) 

1140 
apply(simp_all add: take_all) 

1141 
done 

1142 

1143 
(*The famous takelemma*) 

1144 
lemma take_equalityI: "(ALL i. take i xs = take i ys) ==> xs = ys" 

1145 
apply(drule_tac x = "max (length xs) (length ys)" in spec) 

1146 
apply(simp add: le_max_iff_disj take_all) 

1147 
done 

1148 

1149 

1150 
(** distinct & remdups **) 

1151 
section "distinct & remdups" 

1152 

1153 
lemma distinct_append[simp]: 

1154 
"distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})" 

1155 
by(induct xs, auto) 

1156 

1157 
lemma set_remdups[simp]: "set(remdups xs) = set xs" 

1158 
by(induct xs, simp, simp add:insert_absorb) 

1159 

1160 
lemma distinct_remdups[iff]: "distinct(remdups xs)" 

1161 
by(induct xs, auto) 

1162 

1163 
lemma distinct_filter[simp]: "distinct xs ==> distinct (filter P xs)" 

1164 
by(induct xs, auto) 

1165 

13124  1166 
(* It is best to avoid this indexed version of distinct, 
1167 
but sometimes it is useful *) 

1168 
lemma distinct_conv_nth: 

1169 
"distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)" 

1170 
apply(induct_tac xs) 

1171 
apply simp 

1172 
apply simp 

1173 
apply(rule iffI) 

1174 
apply(clarsimp) 

1175 
apply(case_tac i) 

1176 
apply(case_tac j) 

1177 
apply simp 

1178 
apply(simp add:set_conv_nth) 

1179 
apply(case_tac j) 

1180 
apply(clarsimp simp add:set_conv_nth) 

1181 
apply simp 

1182 
apply(rule conjI) 

1183 
apply(clarsimp simp add:set_conv_nth) 

1184 
apply(erule_tac x = 0 in allE) 

1185 
apply(erule_tac x = "Suc i" in allE) 

1186 
apply simp 

1187 
apply clarsimp 

1188 
apply(erule_tac x = "Suc i" in allE) 

1189 
apply(erule_tac x = "Suc j" in allE) 

1190 
apply simp 

1191 
done 

1192 

13114  1193 
(** replicate **) 
1194 
section "replicate" 

1195 

1196 
lemma length_replicate[simp]: "length(replicate n x) = n" 

1197 
by(induct n, auto) 

1198 

1199 
lemma map_replicate[simp]: "map f (replicate n x) = replicate n (f x)" 

1200 
by(induct n, auto) 

1201 

1202 
lemma replicate_app_Cons_same: 

1203 
"(replicate n x) @ (x#xs) = x # replicate n x @ xs" 

1204 
by(induct n, auto) 

1205 

1206 
lemma rev_replicate[simp]: "rev(replicate n x) = replicate n x" 

1207 
apply(induct n) 

1208 
apply simp 

1209 
apply(simp add: replicate_app_Cons_same) 

1210 
done 

1211 

1212 
lemma replicate_add: "replicate (n+m) x = replicate n x @ replicate m x" 

1213 
by(induct n, auto) 

1214 

1215 
lemma hd_replicate[simp]: "n ~= 0 ==> hd(replicate n x) = x" 

1216 
by(induct n, auto) 

1217 

1218 
lemma tl_replicate[simp]: "n ~= 0 ==> tl(replicate n x) = replicate (n  1) x" 

1219 
by(induct n, auto) 

1220 

1221 
lemma last_replicate[rule_format,simp]: 

1222 
"n ~= 0 > last(replicate n x) = x" 

1223 
by(induct_tac n, auto) 

1224 

1225 
lemma nth_replicate[simp]: "!!i. i<n ==> (replicate n x)!i = x" 

1226 
apply(induct n) 

1227 
apply simp 

1228 
apply(simp add: nth_Cons split:nat.split) 

1229 
done 

1230 

1231 
lemma set_replicate_Suc: "set(replicate (Suc n) x) = {x}" 

1232 
by(induct n, auto) 

1233 

1234 
lemma set_replicate[simp]: "n ~= 0 ==> set(replicate n x) = {x}" 

1235 
by(fast dest!: not0_implies_Suc intro!: set_replicate_Suc) 

1236 

1237 
lemma set_replicate_conv_if: "set(replicate n x) = (if n=0 then {} else {x})" 

1238 
by auto 

1239 

1240 
lemma in_set_replicateD: "x : set(replicate n y) ==> x=y" 

1241 
by(simp add: set_replicate_conv_if split:split_if_asm) 

1242 

1243 

1244 
(*** Lexcicographic orderings on lists ***) 

1245 
section"Lexcicographic orderings on lists" 

3507  1246 

13114  1247 
lemma wf_lexn: "wf r ==> wf(lexn r n)" 
1248 
apply(induct_tac n) 

1249 
apply simp 

1250 
apply simp 

1251 
apply(rule wf_subset) 

1252 
prefer 2 apply(rule Int_lower1) 

1253 
apply(rule wf_prod_fun_image) 

1254 
prefer 2 apply(rule injI) 

1255 
apply auto 

1256 
done 

1257 

1258 
lemma lexn_length: 

1259 
"!!xs ys. (xs,ys) : lexn r n ==> length xs = n & length ys = n" 

1260 
by(induct n, auto) 

1261 

1262 
lemma wf_lex[intro!]: "wf r ==> wf(lex r)" 

1263 
apply(unfold lex_def) 

1264 
apply(rule wf_UN) 

1265 
apply(blast intro: wf_lexn) 

1266 
apply clarify 

1267 
apply(rename_tac m n) 

1268 
apply(subgoal_tac "m ~= n") 

1269 
prefer 2 apply blast 

1270 
apply(blast dest: lexn_length not_sym) 

1271 
done 

1272 

1273 

1274 
lemma lexn_conv: 

1275 
"lexn r n = 

1276 
{(xs,ys). length xs = n & length ys = n & 

1277 
(? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}" 

1278 
apply(induct_tac n) 

1279 
apply simp 

1280 
apply blast 

1281 
apply(simp add: image_Collect lex_prod_def) 

1282 
apply auto 

1283 
apply blast 

1284 
apply(rename_tac a xys x xs' y ys') 

1285 
apply(rule_tac x = "a#xys" in exI) 

1286 
apply simp 

1287 
apply(case_tac xys) 

1288 
apply simp_all 

1289 
apply blast 

1290 
done 

1291 

1292 
lemma lex_conv: 

1293 
"lex r = 

1294 
{(xs,ys). length xs = length ys & 

1295 
(? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}" 

1296 
by(force simp add: lex_def lexn_conv) 

1297 

1298 
lemma wf_lexico[intro!]: "wf r ==> wf(lexico r)" 

1299 
by(unfold lexico_def, blast) 

1300 

1301 
lemma lexico_conv: 

1302 
"lexico r = {(xs,ys). length xs < length ys  

1303 
length xs = length ys & (xs,ys) : lex r}" 

1304 
by(simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def) 

1305 

1306 
lemma Nil_notin_lex[iff]: "([],ys) ~: lex r" 

1307 
by(simp add:lex_conv) 

1308 

1309 
lemma Nil2_notin_lex[iff]: "(xs,[]) ~: lex r" 

1310 
by(simp add:lex_conv) 

1311 

1312 
lemma Cons_in_lex[iff]: 

1313 
"((x#xs,y#ys) : lex r) = 

1314 
((x,y) : r & length xs = length ys  x=y & (xs,ys) : lex r)" 

1315 
apply(simp add:lex_conv) 

1316 
apply(rule iffI) 

1317 
prefer 2 apply(blast intro: Cons_eq_appendI) 

1318 
apply clarify 

1319 
apply(case_tac xys) 

1320 
apply simp 

1321 
apply simp 

1322 
apply blast 

1323 
done 

1324 

1325 

1326 
(*** sublist (a generalization of nth to sets) ***) 

1327 

1328 
lemma sublist_empty[simp]: "sublist xs {} = []" 

1329 
by(auto simp add:sublist_def) 

1330 

1331 
lemma sublist_nil[simp]: "sublist [] A = []" 

1332 
by(auto simp add:sublist_def) 

1333 

1334 
lemma sublist_shift_lemma: 

1335 
"map fst [p:zip xs [i..i + length xs(] . snd p : A] = 

1336 
map fst [p:zip xs [0..length xs(] . snd p + i : A]" 

1337 
apply(induct_tac xs rule: rev_induct) 

1338 
apply simp 

1339 
apply(simp add:add_commute) 

1340 
done 

1341 

1342 
lemma sublist_append: 

1343 
"sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}" 

1344 
apply(unfold sublist_def) 

1345 
apply(induct_tac l' rule: rev_induct) 

1346 
apply simp 

1347 
apply(simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma) 

1348 
apply(simp add:add_commute) 

1349 
done 

1350 

1351 
lemma sublist_Cons: 

1352 
"sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}" 

1353 
apply(induct_tac l rule: rev_induct) 

1354 
apply(simp add:sublist_def) 

1355 
apply(simp del: append_Cons add: append_Cons[symmetric] sublist_append) 

1356 
done 

1357 

1358 
lemma sublist_singleton[simp]: "sublist [x] A = (if 0 : A then [x] else [])" 

1359 
by(simp add:sublist_Cons) 

1360 

1361 
lemma sublist_upt_eq_take[simp]: "sublist l {..n(} = take n l" 

1362 
apply(induct_tac l rule: rev_induct) 

1363 
apply simp 

1364 
apply(simp split:nat_diff_split add:sublist_append) 

1365 
done 

1366 

1367 

1368 
lemma take_Cons': "take n (x#xs) = (if n=0 then [] else x # take (n  1) xs)" 

1369 
by(case_tac n, simp_all) 

1370 

1371 
lemma drop_Cons': "drop n (x#xs) = (if n=0 then x#xs else drop (n  1) xs)" 

1372 
by(case_tac n, simp_all) 

1373 

1374 
lemma nth_Cons': "(x#xs)!n = (if n=0 then x else xs!(n  1))" 

1375 
by(case_tac n, simp_all) 

1376 

1377 
lemmas [simp] = take_Cons'[of "number_of v",standard] 

1378 
drop_Cons'[of "number_of v",standard] 

1379 
nth_Cons'[of "number_of v",standard] 

3507  1380 

13122  1381 
end 