author  wenzelm 
Tue, 07 May 2002 19:54:29 +0200  
changeset 13114  f2b00262bdfc 
parent 12887  d25b43743e10 
child 13122  c63612ffb186 
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 *} 
8 
theory List1 = PreList: 

923  9 

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

12 
consts 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

923  40 

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

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

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

43 

923  44 
syntax 
45 
(* list Enumeration *) 

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

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

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

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

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

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

56 

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

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

61 
"[x]" == "x#[]" 

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

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

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

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

66 

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

69 

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

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

73 

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

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

76 

13114  77 
inductive "lists A" 
78 
intros 

79 
Nil: "[]: lists A" 

80 
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

81 

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

82 

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

83 
(*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

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

87 

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

89 
typed_print_translation 

90 
{* 

91 
let 

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

93 
Syntax.const "length" $ t 

94 
 size_tr' _ _ _ = raise Match; 

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

96 
*} 

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

97 

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

106 
primrec 

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

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

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

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

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

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

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

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

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

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

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

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

151 
primrec 

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

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

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

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

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

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

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

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

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

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

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

3196  187 

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

190 
consts 

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

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

197 
constdefs 

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

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

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

13114  207 

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

209 
by(induct_tac "xs", auto) 

210 

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

212 

213 
lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)"; 

214 
by(induct_tac "xs", auto) 

215 

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

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

218 
lemmas length_induct = measure_induct[of length] 

219 

220 

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

222 

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

224 
apply(unfold lists.defs) 

225 
apply(blast intro!:lfp_mono) 

226 
done 

227 

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

229 
declare lists.intros[intro!] 

230 

231 
lemma lists_IntI[rule_format]: 

232 
"l: lists A ==> l: lists B > l: lists (A Int B)"; 

233 
apply(erule lists.induct) 

234 
apply blast+ 

235 
done 

236 

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

238 
apply(rule mono_Int[THEN equalityI]) 

239 
apply(simp add:mono_def lists_mono) 

240 
apply(blast intro!: lists_IntI) 

241 
done 

242 

243 
lemma append_in_lists_conv[iff]: 

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

245 
by(induct_tac "xs", auto) 

246 

247 
(** length **) 

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

249 

250 
section "length" 

251 

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

253 
by(induct_tac "xs", auto) 

254 

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

256 
by(induct_tac "xs", auto) 

257 

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

259 
by(induct_tac "xs", auto) 

260 

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

262 
by(case_tac "xs", auto) 

263 

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

265 
by(induct_tac "xs", auto) 

266 

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

268 
by(induct_tac xs, auto) 

269 

270 
lemma length_Suc_conv: 

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

272 
by(induct_tac "xs", auto) 

273 

274 
(** @  append **) 

275 

276 
section "@  append" 

277 

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

279 
by(induct_tac "xs", auto) 

3507  280 

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

283 

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

285 
by(induct_tac "xs", auto) 

286 

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

288 
by(induct_tac "xs", auto) 

289 

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

291 
by(induct_tac "xs", auto) 

292 

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

294 
by(induct_tac "xs", auto) 

295 

296 
lemma append_eq_append_conv[rule_format,simp]: 

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

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

299 
apply(induct_tac "xs") 

300 
apply(rule allI) 

301 
apply(case_tac "ys") 

302 
apply simp 

303 
apply force 

304 
apply(rule allI) 

305 
apply(case_tac "ys") 

306 
apply force 

307 
apply simp 

308 
done 

309 

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

311 
by simp 

312 

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

314 
by simp 

315 

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

317 
by simp 

3507  318 

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

321 

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

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

324 

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

326 
by(induct_tac "xs", auto) 

327 

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

329 
by(induct_tac "xs", auto) 

330 

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

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

333 

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

335 
by(simp split: list.split) 

336 

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

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

339 

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

341 

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

343 
by simp 

344 

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

346 
by(drule sym, simp) 

347 

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

349 
by(drule sym, simp) 

350 

351 

352 
(*** 

353 
Simplification procedure for all list equalities. 

354 
Currently only tries to rearrange @ to see if 

355 
 both lists end in a singleton list, 

356 
 or both lists end in the same list. 

357 
***) 

358 
ML_setup{* 

3507  359 
local 
360 

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

363 

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

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

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

367 
 last t = t 

368 

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

370 
 list1 _ = false 

371 

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

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

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

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

376 

377 
val rearr_tac = 

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

379 

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

381 
let 

382 
val lastl = last lhs and lastr = last rhs 

383 
fun rearr conv = 

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

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

386 
val appT = [listT,listT] > listT 

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

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

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

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

391 
handle ERROR => 

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

393 
string_of_cterm ct) 

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

395 

396 
in if list1 lastl andalso list1 lastr 

397 
then rearr append1_eq_conv 

398 
else 

399 
if lastl aconv lastr 

400 
then rearr append_same_eq 

401 
else None 

402 
end 

403 
in 

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

405 
end; 

406 

407 
Addsimprocs [list_eq_simproc]; 

408 
*} 

409 

410 

411 
(** map **) 

412 

413 
section "map" 

414 

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

416 
by (induct xs, simp_all) 

417 

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

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

420 

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

422 
by(induct_tac "xs", auto) 

423 

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

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

426 

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

428 
by(induct_tac xs, auto) 

429 

430 
(* a congruence rule for map: *) 

431 
lemma map_cong: 

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

433 
by (clarify, induct ys, auto) 

434 

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

436 
by(case_tac xs, auto) 

437 

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

439 
by(case_tac xs, auto) 

440 

441 
lemma map_eq_Cons: 

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

443 
by(case_tac xs, auto) 

444 

445 
lemma map_injective: 

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

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

448 

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

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

451 

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

453 
apply(unfold inj_on_def) 

454 
apply clarify 

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

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

457 
apply simp 

458 
apply blast 

459 
apply blast 

460 
done 

461 

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

463 
by(blast dest:inj_mapD intro:inj_mapI) 

464 

465 
(** rev **) 

466 

467 
section "rev" 

468 

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

470 
by(induct_tac xs, auto) 

471 

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

473 
by(induct_tac xs, auto) 

474 

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

476 
by(induct_tac xs, auto) 

477 

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

479 
by(induct_tac xs, auto) 

480 

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

482 
apply(induct "xs" ) 

483 
apply force 

484 
apply(case_tac ys) 

485 
apply simp 

486 
apply force 

487 
done 

488 

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

490 
apply(subst rev_rev_ident[symmetric]) 

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

492 
done 

493 

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

495 

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

497 
by(induct xs rule: rev_induct, auto) 

498 

499 

500 
(** set **) 

501 

502 
section "set" 

503 

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

505 
by(induct_tac xs, auto) 

506 

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

508 
by(induct_tac xs, auto) 

509 

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

511 
by auto 

512 

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

514 
by(induct_tac xs, auto) 

515 

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

517 
by(induct_tac xs, auto) 

518 

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

520 
by(induct_tac xs, auto) 

521 

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

523 
by(induct_tac xs, auto) 

524 

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

526 
apply(induct_tac j) 

527 
apply simp_all 

528 
apply(erule ssubst) 

529 
apply auto 

530 
apply arith 

531 
done 

532 

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

534 
apply(induct_tac "xs") 

535 
apply simp 

536 
apply simp 

537 
apply(rule iffI) 

538 
apply(blast intro: eq_Nil_appendI Cons_eq_appendI) 

539 
apply(erule exE)+ 

540 
apply(case_tac "ys") 

541 
apply auto 

542 
done 

543 

544 

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

546 

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

548 
by(induct_tac xs, auto) 

549 

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

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

552 

553 

554 
(** mem **) 

555 

556 
section "mem" 

557 

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

559 
by(induct_tac xs, auto) 

560 

561 

562 
(** list_all **) 

563 

564 
section "list_all" 

565 

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

567 
by(induct_tac xs, auto) 

568 

569 
lemma list_all_append[simp]: 

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

571 
by(induct_tac xs, auto) 

572 

573 

574 
(** filter **) 

575 

576 
section "filter" 

577 

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

579 
by(induct_tac xs, auto) 

580 

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

582 
by(induct_tac xs, auto) 

583 

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

585 
by(induct xs, auto) 

586 

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

588 
by(induct xs, auto) 

589 

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

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

592 

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

594 
by auto 

595 

596 

597 
section "concat" 

598 

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

600 
by(induct xs, auto) 

601 

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

603 
by(induct xss, auto) 

604 

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

606 
by(induct xss, auto) 

607 

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

609 
by(induct xs, auto) 

610 

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

612 
by(induct xs, auto) 

613 

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

615 
by(induct xs, auto) 

616 

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

618 
by(induct xs, auto) 

619 

620 
(** nth **) 

621 

622 
section "nth" 

623 

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

625 
by auto 

626 

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

628 
by auto 

629 

630 
declare nth.simps[simp del] 

631 

632 
lemma nth_append: 

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

634 
apply(induct "xs") 

635 
apply simp 

636 
apply(case_tac "n" ) 

637 
apply auto 

638 
done 

639 

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

641 
apply(induct "xs" ) 

642 
apply simp 

643 
apply(case_tac "n") 

644 
apply auto 

645 
done 

646 

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

648 
apply(induct_tac "xs") 

649 
apply simp 

650 
apply simp 

651 
apply safe 

652 
apply(rule_tac x = 0 in exI) 

653 
apply simp 

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

655 
apply simp 

656 
apply(case_tac "i") 

657 
apply simp 

658 
apply(rename_tac "j") 

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

660 
apply simp 

661 
done 

662 

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

664 
by(simp add:set_conv_nth, blast) 

665 

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

667 
by(simp add:set_conv_nth, blast) 

668 

669 
lemma all_nth_imp_all_set: 

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

671 
by(simp add:set_conv_nth, blast) 

672 

673 
lemma all_set_conv_all_nth: 

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

675 
by(simp add:set_conv_nth, blast) 

676 

677 

678 
(** list update **) 

679 

680 
section "list update" 

681 

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

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

684 

685 
lemma nth_list_update: 

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

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

688 

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

690 
by(simp add:nth_list_update) 

691 

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

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

694 

695 
lemma list_update_overwrite[simp]: 

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

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

698 

699 
lemma list_update_same_conv: 

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

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

702 

703 
lemma update_zip: 

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

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

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

707 

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

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

710 

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

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

713 

714 

715 
(** last & butlast **) 

716 

717 
section "last / butlast" 

718 

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

720 
by(induct xs, auto) 

721 

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

723 
by(induct xs, auto) 

724 

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

726 
by(induct xs rule:rev_induct, auto) 

727 

728 
lemma butlast_append: 

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

730 
by(induct xs, auto) 

731 

732 
lemma append_butlast_last_id[simp]: 

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

734 
by(induct xs, auto) 

735 

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

737 
by(induct xs, auto split:split_if_asm) 

738 

739 
lemma in_set_butlast_appendI: 

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

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

742 

743 
(** take & drop **) 

744 
section "take & drop" 

745 

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

747 
by(induct xs, auto) 

748 

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

750 
by(induct xs, auto) 

751 

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

753 
by simp 

754 

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

756 
by simp 

757 

758 
declare take_Cons[simp del] drop_Cons[simp del] 

759 

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

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

762 

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

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

765 

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

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

768 

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

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

771 

772 
lemma take_append[simp]: 

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

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

775 

776 
lemma drop_append[simp]: 

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

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

779 

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

781 
apply(induct m) 

782 
apply auto 

783 
apply(case_tac xs) 

784 
apply auto 

785 
apply(case_tac na) 

786 
apply auto 

787 
done 

788 

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

790 
apply(induct m) 

791 
apply auto 

792 
apply(case_tac xs) 

793 
apply auto 

794 
done 

795 

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

797 
apply(induct m) 

798 
apply auto 

799 
apply(case_tac xs) 

800 
apply auto 

801 
done 

802 

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

804 
apply(induct n) 

805 
apply auto 

806 
apply(case_tac xs) 

807 
apply auto 

808 
done 

809 

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

811 
apply(induct n) 

812 
apply auto 

813 
apply(case_tac xs) 

814 
apply auto 

815 
done 

816 

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

818 
apply(induct n) 

819 
apply auto 

820 
apply(case_tac xs) 

821 
apply auto 

822 
done 

823 

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

825 
apply(induct xs) 

826 
apply auto 

827 
apply(case_tac i) 

828 
apply auto 

829 
done 

830 

831 
lemma rev_drop: "!!i. rev (drop i xs) = take (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 nth_take[simp]: "!!n i. i < n ==> (take n xs)!i = xs!i" 

839 
apply(induct xs) 

840 
apply auto 

841 
apply(case_tac n) 

842 
apply(blast ) 

843 
apply(case_tac i) 

844 
apply auto 

845 
done 

846 

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

848 
apply(induct n) 

849 
apply auto 

850 
apply(case_tac xs) 

851 
apply auto 

852 
done 

3507  853 

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

856 
apply(induct xs) 

857 
apply simp 

858 
apply clarsimp 

859 
apply(case_tac zs) 

860 
apply auto 

861 
done 

862 

863 
(** takeWhile & dropWhile **) 

864 

865 
section "takeWhile & dropWhile" 

866 

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

868 
by(induct xs, auto) 

869 

870 
lemma takeWhile_append1[simp]: 

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

872 
by(induct xs, auto) 

873 

874 
lemma takeWhile_append2[simp]: 

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

876 
by(induct xs, auto) 

877 

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

879 
by(induct xs, auto) 

880 

881 
lemma dropWhile_append1[simp]: 

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

883 
by(induct xs, auto) 

884 

885 
lemma dropWhile_append2[simp]: 

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

887 
by(induct xs, auto) 

888 

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

890 
by(induct xs, auto split:split_if_asm) 

891 

892 

893 
(** zip **) 

894 
section "zip" 

895 

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

897 
by(induct ys, auto) 

898 

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

900 
by simp 

901 

902 
declare zip_Cons[simp del] 

903 

904 
lemma length_zip[simp]: 

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

906 
apply(induct ys) 

907 
apply simp 

908 
apply(case_tac xs) 

909 
apply auto 

910 
done 

911 

912 
lemma zip_append1: 

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

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

915 
apply(induct zs) 

916 
apply simp 

917 
apply(case_tac xs) 

918 
apply simp_all 

919 
done 

920 

921 
lemma zip_append2: 

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

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

924 
apply(induct xs) 

925 
apply simp 

926 
apply(case_tac ys) 

927 
apply simp_all 

928 
done 

929 

930 
lemma zip_append[simp]: 

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

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

933 
by(simp add: zip_append1) 

934 

935 
lemma zip_rev: 

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

937 
apply(induct ys) 

938 
apply simp 

939 
apply(case_tac xs) 

940 
apply simp_all 

941 
done 

942 

943 
lemma nth_zip[simp]: 

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

945 
apply(induct ys) 

946 
apply simp 

947 
apply(case_tac xs) 

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

949 
done 

950 

951 
lemma set_zip: 

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

953 
by(simp add: set_conv_nth cong: rev_conj_cong) 

954 

955 
lemma zip_update: 

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

957 
by(rule sym, simp add: update_zip) 

958 

959 
lemma zip_replicate[simp]: 

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

961 
apply(induct i) 

962 
apply auto 

963 
apply(case_tac j) 

964 
apply auto 

965 
done 

966 

967 
(** list_all2 **) 

968 
section "list_all2" 

969 

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

971 
by(simp add:list_all2_def) 

972 

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

974 
by(simp add:list_all2_def) 

975 

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

977 
by(simp add:list_all2_def) 

978 

979 
lemma list_all2_Cons[iff]: 

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

981 
by(auto simp add:list_all2_def) 

982 

983 
lemma list_all2_Cons1: 

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

985 
by(case_tac ys, auto) 

986 

987 
lemma list_all2_Cons2: 

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

989 
by(case_tac xs, auto) 

990 

991 
lemma list_all2_rev[iff]: 

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

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

994 

995 
lemma list_all2_append1: 

996 
"list_all2 P (xs@ys) zs = 

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

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

999 
apply(simp add:list_all2_def zip_append1) 

1000 
apply(rule iffI) 

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

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

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

1004 
apply clarify 

1005 
apply(simp add: ball_Un) 

1006 
done 

1007 

1008 
lemma list_all2_append2: 

1009 
"list_all2 P xs (ys@zs) = 

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

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

1012 
apply(simp add:list_all2_def zip_append2) 

1013 
apply(rule iffI) 

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

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

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

1017 
apply clarify 

1018 
apply(simp add: ball_Un) 

1019 
done 

1020 

1021 
lemma list_all2_conv_all_nth: 

1022 
"list_all2 P xs ys = 

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

1024 
by(force simp add:list_all2_def set_zip) 

1025 

1026 
lemma list_all2_trans[rule_format]: 

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

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

1029 
apply(induct_tac as) 

1030 
apply simp 

1031 
apply(rule allI) 

1032 
apply(induct_tac bs) 

1033 
apply simp 

1034 
apply(rule allI) 

1035 
apply(induct_tac cs) 

1036 
apply auto 

1037 
done 

1038 

1039 

1040 
section "foldl" 

1041 

1042 
lemma foldl_append[simp]: 

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

1044 
by(induct xs, auto) 

1045 

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

1047 
because it requires an additional transitivity step 

1048 
*) 

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

1050 
by(induct ns, auto) 

1051 

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

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

1054 

1055 
lemma sum_eq_0_conv[iff]: 

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

1057 
by(induct ns, auto) 

1058 

1059 
(** upto **) 

1060 

1061 
(* Does not terminate! *) 

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

1063 
by(induct j, auto) 

1064 

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

1066 
by(subst upt_rec, simp) 

1067 

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

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

1070 
by simp 

1071 

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

1073 
apply(rule trans) 

1074 
apply(subst upt_rec) 

1075 
prefer 2 apply(rule refl) 

1076 
apply simp 

1077 
done 

1078 

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

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

1081 
by(induct_tac "k", auto) 

1082 

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

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

1085 

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

1087 
apply(induct j) 

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

1089 
done 

1090 

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

1092 
apply(induct m) 

1093 
apply simp 

1094 
apply(subst upt_rec) 

1095 
apply(rule sym) 

1096 
apply(subst upt_rec) 

1097 
apply(simp del: upt.simps) 

1098 
done 

3507  1099 

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

1102 

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

1104 
thm diff_induct 

1105 
apply(induct n m rule: diff_induct) 

1106 
prefer 3 apply(subst map_Suc_upt[symmetric]) 

1107 
apply(auto simp add: less_diff_conv nth_upt) 

1108 
done 

1109 

1110 
lemma nth_take_lemma[rule_format]: 

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

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

1113 
> take k xs = take k ys" 

1114 
apply(induct_tac k) 

1115 
apply(simp_all add: less_Suc_eq_0_disj all_conj_distrib) 

1116 
apply clarify 

1117 
(*Both lists must be nonempty*) 

1118 
apply(case_tac xs) 

1119 
apply simp 

1120 
apply(case_tac ys) 

1121 
apply clarify 

1122 
apply(simp (no_asm_use)) 

1123 
apply clarify 

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

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

1126 
apply blast 

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

1128 
done 

1129 

1130 
lemma nth_equalityI: 

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

1132 
apply(frule nth_take_lemma[OF le_refl eq_imp_le]) 

1133 
apply(simp_all add: take_all) 

1134 
done 

1135 

1136 
(*The famous takelemma*) 

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

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

1139 
apply(simp add: le_max_iff_disj take_all) 

1140 
done 

1141 

1142 

1143 
(** distinct & remdups **) 

1144 
section "distinct & remdups" 

1145 

1146 
lemma distinct_append[simp]: 

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

1148 
by(induct xs, auto) 

1149 

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

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

1152 

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

1154 
by(induct xs, auto) 

1155 

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

1157 
by(induct xs, auto) 

1158 

1159 
(** replicate **) 

1160 
section "replicate" 

1161 

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

1163 
by(induct n, auto) 

1164 

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

1166 
by(induct n, auto) 

1167 

1168 
lemma replicate_app_Cons_same: 

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

1170 
by(induct n, auto) 

1171 

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

1173 
apply(induct n) 

1174 
apply simp 

1175 
apply(simp add: replicate_app_Cons_same) 

1176 
done 

1177 

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

1179 
by(induct n, auto) 

1180 

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

1182 
by(induct n, auto) 

1183 

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

1185 
by(induct n, auto) 

1186 

1187 
lemma last_replicate[rule_format,simp]: 

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

1189 
by(induct_tac n, auto) 

1190 

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

1192 
apply(induct n) 

1193 
apply simp 

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

1195 
done 

1196 

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

1198 
by(induct n, auto) 

1199 

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

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

1202 

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

1204 
by auto 

1205 

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

1207 
by(simp add: set_replicate_conv_if split:split_if_asm) 

1208 

1209 

1210 
(*** Lexcicographic orderings on lists ***) 

1211 
section"Lexcicographic orderings on lists" 

3507  1212 

13114  1213 
lemma wf_lexn: "wf r ==> wf(lexn r n)" 
1214 
apply(induct_tac n) 

1215 
apply simp 

1216 
apply simp 

1217 
apply(rule wf_subset) 

1218 
prefer 2 apply(rule Int_lower1) 

1219 
apply(rule wf_prod_fun_image) 

1220 
prefer 2 apply(rule injI) 

1221 
apply auto 

1222 
done 

1223 

1224 
lemma lexn_length: 

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

1226 
by(induct n, auto) 

1227 

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

1229 
apply(unfold lex_def) 

1230 
apply(rule wf_UN) 

1231 
apply(blast intro: wf_lexn) 

1232 
apply clarify 

1233 
apply(rename_tac m n) 

1234 
apply(subgoal_tac "m ~= n") 

1235 
prefer 2 apply blast 

1236 
apply(blast dest: lexn_length not_sym) 

1237 
done 

1238 

1239 

1240 
lemma lexn_conv: 

1241 
"lexn r n = 

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

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

1244 
apply(induct_tac n) 

1245 
apply simp 

1246 
apply blast 

1247 
apply(simp add: image_Collect lex_prod_def) 

1248 
apply auto 

1249 
apply blast 

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

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

1252 
apply simp 

1253 
apply(case_tac xys) 

1254 
apply simp_all 

1255 
apply blast 

1256 
done 

1257 

1258 
lemma lex_conv: 

1259 
"lex r = 

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

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

1262 
by(force simp add: lex_def lexn_conv) 

1263 

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

1265 
by(unfold lexico_def, blast) 

1266 

1267 
lemma lexico_conv: 

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

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

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

1271 

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

1273 
by(simp add:lex_conv) 

1274 

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

1276 
by(simp add:lex_conv) 

1277 

1278 
lemma Cons_in_lex[iff]: 

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

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

1281 
apply(simp add:lex_conv) 

1282 
apply(rule iffI) 

1283 
prefer 2 apply(blast intro: Cons_eq_appendI) 

1284 
apply clarify 

1285 
apply(case_tac xys) 

1286 
apply simp 

1287 
apply simp 

1288 
apply blast 

1289 
done 

1290 

1291 

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

1293 

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

1295 
by(auto simp add:sublist_def) 

1296 

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

1298 
by(auto simp add:sublist_def) 

1299 

1300 
lemma sublist_shift_lemma: 

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

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

1303 
apply(induct_tac xs rule: rev_induct) 

1304 
apply simp 

1305 
apply(simp add:add_commute) 

1306 
done 

1307 

1308 
lemma sublist_append: 

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

1310 
apply(unfold sublist_def) 

1311 
apply(induct_tac l' rule: rev_induct) 

1312 
apply simp 

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

1314 
apply(simp add:add_commute) 

1315 
done 

1316 

1317 
lemma sublist_Cons: 

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

1319 
apply(induct_tac l rule: rev_induct) 

1320 
apply(simp add:sublist_def) 

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

1322 
done 

1323 

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

1325 
by(simp add:sublist_Cons) 

1326 

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

1328 
apply(induct_tac l rule: rev_induct) 

1329 
apply simp 

1330 
apply(simp split:nat_diff_split add:sublist_append) 

1331 
done 

1332 

1333 

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

1335 
by(case_tac n, simp_all) 

1336 

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

1338 
by(case_tac n, simp_all) 

1339 

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

1341 
by(case_tac n, simp_all) 

1342 

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

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

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

3507  1346 

1347 
end; 