summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/List.ML

author | nipkow |

Tue Dec 30 11:14:09 1997 +0100 (1997-12-30) | |

changeset 4502 | 337c073de95e |

parent 4423 | a129b817b58a |

child 4605 | 579e0ef2df6b |

permissions | -rw-r--r-- |

nth -> !

1 (* Title: HOL/List

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 1994 TU Muenchen

6 List lemmas

7 *)

9 open List;

11 goal thy "!x. xs ~= x#xs";

12 by (induct_tac "xs" 1);

13 by (ALLGOALS Asm_simp_tac);

14 qed_spec_mp "not_Cons_self";

15 bind_thm("not_Cons_self2",not_Cons_self RS not_sym);

16 Addsimps [not_Cons_self,not_Cons_self2];

18 goal thy "(xs ~= []) = (? y ys. xs = y#ys)";

19 by (induct_tac "xs" 1);

20 by (Simp_tac 1);

21 by (Asm_simp_tac 1);

22 qed "neq_Nil_conv";

25 (** "lists": the list-forming operator over sets **)

27 goalw thy lists.defs "!!A B. A<=B ==> lists A <= lists B";

28 by (rtac lfp_mono 1);

29 by (REPEAT (ares_tac basic_monos 1));

30 qed "lists_mono";

32 val listsE = lists.mk_cases list.simps "x#l : lists A";

33 AddSEs [listsE];

34 AddSIs lists.intrs;

36 goal thy "!!l. l: lists A ==> l: lists B --> l: lists (A Int B)";

37 by (etac lists.induct 1);

38 by (ALLGOALS Blast_tac);

39 qed_spec_mp "lists_IntI";

41 goal thy "lists (A Int B) = lists A Int lists B";

42 by (rtac (mono_Int RS equalityI) 1);

43 by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);

44 by (blast_tac (claset() addSIs [lists_IntI]) 1);

45 qed "lists_Int_eq";

46 Addsimps [lists_Int_eq];

49 (** list_case **)

51 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";

52 by (induct_tac "xs" 1);

53 by (REPEAT(resolve_tac prems 1));

54 qed "list_cases";

56 goal thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";

57 by (induct_tac "xs" 1);

58 by (Blast_tac 1);

59 by (Blast_tac 1);

60 bind_thm("list_eq_cases",

61 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));

64 (** length **)

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

67 section "length";

69 goal thy "length(xs@ys) = length(xs)+length(ys)";

70 by (induct_tac "xs" 1);

71 by (ALLGOALS Asm_simp_tac);

72 qed"length_append";

73 Addsimps [length_append];

75 goal thy "length (map f l) = length l";

76 by (induct_tac "l" 1);

77 by (ALLGOALS Simp_tac);

78 qed "length_map";

79 Addsimps [length_map];

81 goal thy "length(rev xs) = length(xs)";

82 by (induct_tac "xs" 1);

83 by (ALLGOALS Asm_simp_tac);

84 qed "length_rev";

85 Addsimps [length_rev];

87 goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";

88 by (exhaust_tac "xs" 1);

89 by (ALLGOALS Asm_full_simp_tac);

90 qed "length_tl";

91 Addsimps [length_tl];

93 goal thy "(length xs = 0) = (xs = [])";

94 by (induct_tac "xs" 1);

95 by (ALLGOALS Asm_simp_tac);

96 qed "length_0_conv";

97 AddIffs [length_0_conv];

99 goal thy "(0 = length xs) = (xs = [])";

100 by (induct_tac "xs" 1);

101 by (ALLGOALS Asm_simp_tac);

102 qed "zero_length_conv";

103 AddIffs [zero_length_conv];

105 goal thy "(0 < length xs) = (xs ~= [])";

106 by (induct_tac "xs" 1);

107 by (ALLGOALS Asm_simp_tac);

108 qed "length_greater_0_conv";

109 AddIffs [length_greater_0_conv];

111 (** @ - append **)

113 section "@ - append";

115 goal thy "(xs@ys)@zs = xs@(ys@zs)";

116 by (induct_tac "xs" 1);

117 by (ALLGOALS Asm_simp_tac);

118 qed "append_assoc";

119 Addsimps [append_assoc];

121 goal thy "xs @ [] = xs";

122 by (induct_tac "xs" 1);

123 by (ALLGOALS Asm_simp_tac);

124 qed "append_Nil2";

125 Addsimps [append_Nil2];

127 goal thy "(xs@ys = []) = (xs=[] & ys=[])";

128 by (induct_tac "xs" 1);

129 by (ALLGOALS Asm_simp_tac);

130 qed "append_is_Nil_conv";

131 AddIffs [append_is_Nil_conv];

133 goal thy "([] = xs@ys) = (xs=[] & ys=[])";

134 by (induct_tac "xs" 1);

135 by (ALLGOALS Asm_simp_tac);

136 by (Blast_tac 1);

137 qed "Nil_is_append_conv";

138 AddIffs [Nil_is_append_conv];

140 goal thy "(xs @ ys = xs) = (ys=[])";

141 by (induct_tac "xs" 1);

142 by (ALLGOALS Asm_simp_tac);

143 qed "append_self_conv";

145 goal thy "(xs = xs @ ys) = (ys=[])";

146 by (induct_tac "xs" 1);

147 by (ALLGOALS Asm_simp_tac);

148 by (Blast_tac 1);

149 qed "self_append_conv";

150 AddIffs [append_self_conv,self_append_conv];

152 goal thy "!ys. length xs = length ys | length us = length vs \

153 \ --> (xs@us = ys@vs) = (xs=ys & us=vs)";

154 by (induct_tac "xs" 1);

155 by (rtac allI 1);

156 by (exhaust_tac "ys" 1);

157 by (Asm_simp_tac 1);

158 by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()

159 addEs [less_not_refl2 RSN (2,rev_notE)]) 1);

160 by (rtac allI 1);

161 by (exhaust_tac "ys" 1);

162 by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()

163 addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);

164 by (Asm_simp_tac 1);

165 qed_spec_mp "append_eq_append_conv";

166 Addsimps [append_eq_append_conv];

168 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";

169 by (Simp_tac 1);

170 qed "same_append_eq";

172 goal thy "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)";

173 by (Simp_tac 1);

174 qed "append1_eq_conv";

176 goal thy "(ys @ xs = zs @ xs) = (ys=zs)";

177 by (Simp_tac 1);

178 qed "append_same_eq";

180 AddSIs

181 [same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];

182 AddSDs

183 [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];

185 goal thy "xs ~= [] --> hd xs # tl xs = xs";

186 by (induct_tac "xs" 1);

187 by (ALLGOALS Asm_simp_tac);

188 qed_spec_mp "hd_Cons_tl";

189 Addsimps [hd_Cons_tl];

191 goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";

192 by (induct_tac "xs" 1);

193 by (ALLGOALS Asm_simp_tac);

194 qed "hd_append";

196 goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";

197 by (asm_simp_tac (simpset() addsimps [hd_append]

198 addsplits [split_list_case]) 1);

199 qed "hd_append2";

200 Addsimps [hd_append2];

202 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";

203 by (simp_tac (simpset() addsplits [split_list_case]) 1);

204 qed "tl_append";

206 goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";

207 by (asm_simp_tac (simpset() addsimps [tl_append]

208 addsplits [split_list_case]) 1);

209 qed "tl_append2";

210 Addsimps [tl_append2];

212 (** map **)

214 section "map";

216 goal thy

217 "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";

218 by (induct_tac "xs" 1);

219 by (ALLGOALS Asm_simp_tac);

220 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));

222 goal thy "map (%x. x) = (%xs. xs)";

223 by (rtac ext 1);

224 by (induct_tac "xs" 1);

225 by (ALLGOALS Asm_simp_tac);

226 qed "map_ident";

227 Addsimps[map_ident];

229 goal thy "map f (xs@ys) = map f xs @ map f ys";

230 by (induct_tac "xs" 1);

231 by (ALLGOALS Asm_simp_tac);

232 qed "map_append";

233 Addsimps[map_append];

235 goalw thy [o_def] "map (f o g) xs = map f (map g xs)";

236 by (induct_tac "xs" 1);

237 by (ALLGOALS Asm_simp_tac);

238 qed "map_compose";

239 Addsimps[map_compose];

241 goal thy "rev(map f xs) = map f (rev xs)";

242 by (induct_tac "xs" 1);

243 by (ALLGOALS Asm_simp_tac);

244 qed "rev_map";

246 (* a congruence rule for map: *)

247 goal thy

248 "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";

249 by (rtac impI 1);

250 by (hyp_subst_tac 1);

251 by (induct_tac "ys" 1);

252 by (ALLGOALS Asm_simp_tac);

253 val lemma = result();

254 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));

256 goal List.thy "(map f xs = []) = (xs = [])";

257 by (induct_tac "xs" 1);

258 by (ALLGOALS Asm_simp_tac);

259 qed "map_is_Nil_conv";

260 AddIffs [map_is_Nil_conv];

262 goal List.thy "([] = map f xs) = (xs = [])";

263 by (induct_tac "xs" 1);

264 by (ALLGOALS Asm_simp_tac);

265 qed "Nil_is_map_conv";

266 AddIffs [Nil_is_map_conv];

269 (** rev **)

271 section "rev";

273 goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";

274 by (induct_tac "xs" 1);

275 by (ALLGOALS Asm_simp_tac);

276 qed "rev_append";

277 Addsimps[rev_append];

279 goal thy "rev(rev l) = l";

280 by (induct_tac "l" 1);

281 by (ALLGOALS Asm_simp_tac);

282 qed "rev_rev_ident";

283 Addsimps[rev_rev_ident];

285 goal thy "(rev xs = []) = (xs = [])";

286 by (induct_tac "xs" 1);

287 by (ALLGOALS Asm_simp_tac);

288 qed "rev_is_Nil_conv";

289 AddIffs [rev_is_Nil_conv];

291 goal thy "([] = rev xs) = (xs = [])";

292 by (induct_tac "xs" 1);

293 by (ALLGOALS Asm_simp_tac);

294 qed "Nil_is_rev_conv";

295 AddIffs [Nil_is_rev_conv];

298 (** mem **)

300 section "mem";

302 goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";

303 by (induct_tac "xs" 1);

304 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

305 qed "mem_append";

306 Addsimps[mem_append];

308 goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";

309 by (induct_tac "xs" 1);

310 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

311 qed "mem_filter";

312 Addsimps[mem_filter];

314 (** set **)

316 section "set";

318 goal thy "set (xs@ys) = (set xs Un set ys)";

319 by (induct_tac "xs" 1);

320 by (ALLGOALS Asm_simp_tac);

321 qed "set_append";

322 Addsimps[set_append];

324 goal thy "(x mem xs) = (x: set xs)";

325 by (induct_tac "xs" 1);

326 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

327 by (Blast_tac 1);

328 qed "set_mem_eq";

330 goal thy "set l <= set (x#l)";

331 by (Simp_tac 1);

332 by (Blast_tac 1);

333 qed "set_subset_Cons";

335 goal thy "(set xs = {}) = (xs = [])";

336 by (induct_tac "xs" 1);

337 by (ALLGOALS Asm_simp_tac);

338 qed "set_empty";

339 Addsimps [set_empty];

341 goal thy "set(rev xs) = set(xs)";

342 by (induct_tac "xs" 1);

343 by (ALLGOALS Asm_simp_tac);

344 qed "set_rev";

345 Addsimps [set_rev];

347 goal thy "set(map f xs) = f``(set xs)";

348 by (induct_tac "xs" 1);

349 by (ALLGOALS Asm_simp_tac);

350 qed "set_map";

351 Addsimps [set_map];

354 (** list_all **)

356 section "list_all";

358 goal thy "list_all (%x. True) xs = True";

359 by (induct_tac "xs" 1);

360 by (ALLGOALS Asm_simp_tac);

361 qed "list_all_True";

362 Addsimps [list_all_True];

364 goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";

365 by (induct_tac "xs" 1);

366 by (ALLGOALS Asm_simp_tac);

367 qed "list_all_append";

368 Addsimps [list_all_append];

370 goal thy "list_all P xs = (!x. x mem xs --> P(x))";

371 by (induct_tac "xs" 1);

372 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

373 by (Blast_tac 1);

374 qed "list_all_mem_conv";

377 (** filter **)

379 section "filter";

381 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";

382 by (induct_tac "xs" 1);

383 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

384 qed "filter_append";

385 Addsimps [filter_append];

387 goal thy "size (filter P xs) <= size xs";

388 by (induct_tac "xs" 1);

389 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

390 qed "filter_size";

393 (** concat **)

395 section "concat";

397 goal thy "concat(xs@ys) = concat(xs)@concat(ys)";

398 by (induct_tac "xs" 1);

399 by (ALLGOALS Asm_simp_tac);

400 qed"concat_append";

401 Addsimps [concat_append];

403 goal thy "(concat xss = []) = (!xs:set xss. xs=[])";

404 by (induct_tac "xss" 1);

405 by (ALLGOALS Asm_simp_tac);

406 qed "concat_eq_Nil_conv";

407 AddIffs [concat_eq_Nil_conv];

409 goal thy "([] = concat xss) = (!xs:set xss. xs=[])";

410 by (induct_tac "xss" 1);

411 by (ALLGOALS Asm_simp_tac);

412 qed "Nil_eq_concat_conv";

413 AddIffs [Nil_eq_concat_conv];

415 goal thy "set(concat xs) = Union(set `` set xs)";

416 by (induct_tac "xs" 1);

417 by (ALLGOALS Asm_simp_tac);

418 qed"set_concat";

419 Addsimps [set_concat];

421 goal thy "map f (concat xs) = concat (map (map f) xs)";

422 by (induct_tac "xs" 1);

423 by (ALLGOALS Asm_simp_tac);

424 qed "map_concat";

426 goal thy "filter p (concat xs) = concat (map (filter p) xs)";

427 by (induct_tac "xs" 1);

428 by (ALLGOALS Asm_simp_tac);

429 qed"filter_concat";

431 goal thy "rev(concat xs) = concat (map rev (rev xs))";

432 by (induct_tac "xs" 1);

433 by (ALLGOALS Asm_simp_tac);

434 qed "rev_concat";

436 (** nth **)

438 section "nth";

440 goal thy

441 "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";

442 by (nat_ind_tac "n" 1);

443 by (Asm_simp_tac 1);

444 by (rtac allI 1);

445 by (exhaust_tac "xs" 1);

446 by (ALLGOALS Asm_simp_tac);

447 by (rtac allI 1);

448 by (exhaust_tac "xs" 1);

449 by (ALLGOALS Asm_simp_tac);

450 qed_spec_mp "nth_append";

452 goal thy "!n. n < length xs --> (map f xs)!n = f(xs!n)";

453 by (induct_tac "xs" 1);

454 (* case [] *)

455 by (Asm_full_simp_tac 1);

456 (* case x#xl *)

457 by (rtac allI 1);

458 by (nat_ind_tac "n" 1);

459 by (ALLGOALS Asm_full_simp_tac);

460 qed_spec_mp "nth_map";

461 Addsimps [nth_map];

463 goal thy "!n. n < length xs --> list_all P xs --> P(xs!n)";

464 by (induct_tac "xs" 1);

465 (* case [] *)

466 by (Simp_tac 1);

467 (* case x#xl *)

468 by (rtac allI 1);

469 by (nat_ind_tac "n" 1);

470 by (ALLGOALS Asm_full_simp_tac);

471 qed_spec_mp "list_all_nth";

473 goal thy "!n. n < length xs --> xs!n mem xs";

474 by (induct_tac "xs" 1);

475 (* case [] *)

476 by (Simp_tac 1);

477 (* case x#xl *)

478 by (rtac allI 1);

479 by (nat_ind_tac "n" 1);

480 (* case 0 *)

481 by (Asm_full_simp_tac 1);

482 (* case Suc x *)

483 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

484 qed_spec_mp "nth_mem";

485 Addsimps [nth_mem];

487 (** last & butlast **)

489 goal thy "last(xs@[x]) = x";

490 by (induct_tac "xs" 1);

491 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

492 qed "last_snoc";

493 Addsimps [last_snoc];

495 goal thy "butlast(xs@[x]) = xs";

496 by (induct_tac "xs" 1);

497 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

498 qed "butlast_snoc";

499 Addsimps [butlast_snoc];

501 goal thy

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

503 by (induct_tac "xs" 1);

504 by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));

505 qed_spec_mp "butlast_append";

507 goal thy "x:set(butlast xs) --> x:set xs";

508 by (induct_tac "xs" 1);

509 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));

510 qed_spec_mp "in_set_butlastD";

512 goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";

513 by (asm_simp_tac (simpset() addsimps [butlast_append]

514 addsplits [expand_if]) 1);

515 by (blast_tac (claset() addDs [in_set_butlastD]) 1);

516 qed "in_set_butlast_appendI1";

518 goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";

519 by (asm_simp_tac (simpset() addsimps [butlast_append]

520 addsplits [expand_if]) 1);

521 by (Clarify_tac 1);

522 by (Full_simp_tac 1);

523 qed "in_set_butlast_appendI2";

525 (** take & drop **)

526 section "take & drop";

528 goal thy "take 0 xs = []";

529 by (induct_tac "xs" 1);

530 by (ALLGOALS Asm_simp_tac);

531 qed "take_0";

533 goal thy "drop 0 xs = xs";

534 by (induct_tac "xs" 1);

535 by (ALLGOALS Asm_simp_tac);

536 qed "drop_0";

538 goal thy "take (Suc n) (x#xs) = x # take n xs";

539 by (Simp_tac 1);

540 qed "take_Suc_Cons";

542 goal thy "drop (Suc n) (x#xs) = drop n xs";

543 by (Simp_tac 1);

544 qed "drop_Suc_Cons";

546 Delsimps [take_Cons,drop_Cons];

547 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];

549 goal thy "!xs. length(take n xs) = min (length xs) n";

550 by (nat_ind_tac "n" 1);

551 by (ALLGOALS Asm_simp_tac);

552 by (rtac allI 1);

553 by (exhaust_tac "xs" 1);

554 by (ALLGOALS Asm_simp_tac);

555 qed_spec_mp "length_take";

556 Addsimps [length_take];

558 goal thy "!xs. length(drop n xs) = (length xs - n)";

559 by (nat_ind_tac "n" 1);

560 by (ALLGOALS Asm_simp_tac);

561 by (rtac allI 1);

562 by (exhaust_tac "xs" 1);

563 by (ALLGOALS Asm_simp_tac);

564 qed_spec_mp "length_drop";

565 Addsimps [length_drop];

567 goal thy "!xs. length xs <= n --> take n xs = xs";

568 by (nat_ind_tac "n" 1);

569 by (ALLGOALS Asm_simp_tac);

570 by (rtac allI 1);

571 by (exhaust_tac "xs" 1);

572 by (ALLGOALS Asm_simp_tac);

573 qed_spec_mp "take_all";

575 goal thy "!xs. length xs <= n --> drop n xs = []";

576 by (nat_ind_tac "n" 1);

577 by (ALLGOALS Asm_simp_tac);

578 by (rtac allI 1);

579 by (exhaust_tac "xs" 1);

580 by (ALLGOALS Asm_simp_tac);

581 qed_spec_mp "drop_all";

583 goal thy

584 "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";

585 by (nat_ind_tac "n" 1);

586 by (ALLGOALS Asm_simp_tac);

587 by (rtac allI 1);

588 by (exhaust_tac "xs" 1);

589 by (ALLGOALS Asm_simp_tac);

590 qed_spec_mp "take_append";

591 Addsimps [take_append];

593 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";

594 by (nat_ind_tac "n" 1);

595 by (ALLGOALS Asm_simp_tac);

596 by (rtac allI 1);

597 by (exhaust_tac "xs" 1);

598 by (ALLGOALS Asm_simp_tac);

599 qed_spec_mp "drop_append";

600 Addsimps [drop_append];

602 goal thy "!xs n. take n (take m xs) = take (min n m) xs";

603 by (nat_ind_tac "m" 1);

604 by (ALLGOALS Asm_simp_tac);

605 by (rtac allI 1);

606 by (exhaust_tac "xs" 1);

607 by (ALLGOALS Asm_simp_tac);

608 by (rtac allI 1);

609 by (exhaust_tac "n" 1);

610 by (ALLGOALS Asm_simp_tac);

611 qed_spec_mp "take_take";

613 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs";

614 by (nat_ind_tac "m" 1);

615 by (ALLGOALS Asm_simp_tac);

616 by (rtac allI 1);

617 by (exhaust_tac "xs" 1);

618 by (ALLGOALS Asm_simp_tac);

619 qed_spec_mp "drop_drop";

621 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";

622 by (nat_ind_tac "m" 1);

623 by (ALLGOALS Asm_simp_tac);

624 by (rtac allI 1);

625 by (exhaust_tac "xs" 1);

626 by (ALLGOALS Asm_simp_tac);

627 qed_spec_mp "take_drop";

629 goal thy "!xs. take n (map f xs) = map f (take n xs)";

630 by (nat_ind_tac "n" 1);

631 by (ALLGOALS Asm_simp_tac);

632 by (rtac allI 1);

633 by (exhaust_tac "xs" 1);

634 by (ALLGOALS Asm_simp_tac);

635 qed_spec_mp "take_map";

637 goal thy "!xs. drop n (map f xs) = map f (drop n xs)";

638 by (nat_ind_tac "n" 1);

639 by (ALLGOALS Asm_simp_tac);

640 by (rtac allI 1);

641 by (exhaust_tac "xs" 1);

642 by (ALLGOALS Asm_simp_tac);

643 qed_spec_mp "drop_map";

645 goal thy "!n i. i < n --> (take n xs)!i = xs!i";

646 by (induct_tac "xs" 1);

647 by (ALLGOALS Asm_simp_tac);

648 by (Clarify_tac 1);

649 by (exhaust_tac "n" 1);

650 by (Blast_tac 1);

651 by (exhaust_tac "i" 1);

652 by (ALLGOALS Asm_full_simp_tac);

653 qed_spec_mp "nth_take";

654 Addsimps [nth_take];

656 goal thy "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";

657 by (nat_ind_tac "n" 1);

658 by (ALLGOALS Asm_simp_tac);

659 by (rtac allI 1);

660 by (exhaust_tac "xs" 1);

661 by (ALLGOALS Asm_simp_tac);

662 qed_spec_mp "nth_drop";

663 Addsimps [nth_drop];

665 (** takeWhile & dropWhile **)

667 section "takeWhile & dropWhile";

669 goal thy "takeWhile P xs @ dropWhile P xs = xs";

670 by (induct_tac "xs" 1);

671 by (Simp_tac 1);

672 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

673 qed "takeWhile_dropWhile_id";

674 Addsimps [takeWhile_dropWhile_id];

676 goal thy "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";

677 by (induct_tac "xs" 1);

678 by (Simp_tac 1);

679 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

680 by (Blast_tac 1);

681 bind_thm("takeWhile_append1", conjI RS (result() RS mp));

682 Addsimps [takeWhile_append1];

684 goal thy

685 "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";

686 by (induct_tac "xs" 1);

687 by (Simp_tac 1);

688 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

689 bind_thm("takeWhile_append2", ballI RS (result() RS mp));

690 Addsimps [takeWhile_append2];

692 goal thy

693 "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";

694 by (induct_tac "xs" 1);

695 by (Simp_tac 1);

696 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

697 by (Blast_tac 1);

698 bind_thm("dropWhile_append1", conjI RS (result() RS mp));

699 Addsimps [dropWhile_append1];

701 goal thy

702 "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";

703 by (induct_tac "xs" 1);

704 by (Simp_tac 1);

705 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

706 bind_thm("dropWhile_append2", ballI RS (result() RS mp));

707 Addsimps [dropWhile_append2];

709 goal thy "x:set(takeWhile P xs) --> x:set xs & P x";

710 by (induct_tac "xs" 1);

711 by (Simp_tac 1);

712 by (asm_full_simp_tac (simpset() addsplits [expand_if]) 1);

713 qed_spec_mp"set_take_whileD";

715 qed_goal "zip_Nil_Nil" thy "zip [] [] = []" (K [Simp_tac 1]);

716 qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys"

717 (K [Simp_tac 1]);

718 (** replicate **)

719 section "replicate";

721 goal thy "set(replicate (Suc n) x) = {x}";

722 by (induct_tac "n" 1);

723 by (ALLGOALS Asm_full_simp_tac);

724 val lemma = result();

726 goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";

727 by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);

728 qed "set_replicate";

729 Addsimps [set_replicate];