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

src/HOL/List.ML

author | wenzelm |

Thu Feb 12 17:53:05 1998 +0100 (1998-02-12) | |

changeset 4628 | 0c7e97836e3c |

parent 4605 | 579e0ef2df6b |

child 4643 | 1b40fcac5a09 |

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

*** empty log message ***

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) = (length xs) - 1";

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];

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

354 by (induct_tac "xs" 1);

355 by (ALLGOALS Asm_simp_tac);

356 qed "set_map";

357 Addsimps [set_map];

359 goal thy "(x : set(filter P xs)) = (x : set xs & P x)";

360 by (induct_tac "xs" 1);

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

362 by(Blast_tac 1);

363 qed "in_set_filter";

364 Addsimps [in_set_filter];

367 (** list_all **)

369 section "list_all";

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

372 by (induct_tac "xs" 1);

373 by (ALLGOALS Asm_simp_tac);

374 qed "list_all_True";

375 Addsimps [list_all_True];

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

378 by (induct_tac "xs" 1);

379 by (ALLGOALS Asm_simp_tac);

380 qed "list_all_append";

381 Addsimps [list_all_append];

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

384 by (induct_tac "xs" 1);

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

386 by (Blast_tac 1);

387 qed "list_all_mem_conv";

390 (** filter **)

392 section "filter";

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

395 by (induct_tac "xs" 1);

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

397 qed "filter_append";

398 Addsimps [filter_append];

400 goal thy "filter (%x. True) xs = xs";

401 by (induct_tac "xs" 1);

402 by (ALLGOALS Asm_simp_tac);

403 qed "filter_True";

404 Addsimps [filter_True];

406 goal thy "filter (%x. False) xs = []";

407 by (induct_tac "xs" 1);

408 by (ALLGOALS Asm_simp_tac);

409 qed "filter_False";

410 Addsimps [filter_False];

412 goal thy "length (filter P xs) <= length xs";

413 by (induct_tac "xs" 1);

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

415 qed "length_filter";

418 (** concat **)

420 section "concat";

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

423 by (induct_tac "xs" 1);

424 by (ALLGOALS Asm_simp_tac);

425 qed"concat_append";

426 Addsimps [concat_append];

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

429 by (induct_tac "xss" 1);

430 by (ALLGOALS Asm_simp_tac);

431 qed "concat_eq_Nil_conv";

432 AddIffs [concat_eq_Nil_conv];

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

435 by (induct_tac "xss" 1);

436 by (ALLGOALS Asm_simp_tac);

437 qed "Nil_eq_concat_conv";

438 AddIffs [Nil_eq_concat_conv];

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

441 by (induct_tac "xs" 1);

442 by (ALLGOALS Asm_simp_tac);

443 qed"set_concat";

444 Addsimps [set_concat];

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

447 by (induct_tac "xs" 1);

448 by (ALLGOALS Asm_simp_tac);

449 qed "map_concat";

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

452 by (induct_tac "xs" 1);

453 by (ALLGOALS Asm_simp_tac);

454 qed"filter_concat";

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

457 by (induct_tac "xs" 1);

458 by (ALLGOALS Asm_simp_tac);

459 qed "rev_concat";

461 (** nth **)

463 section "nth";

465 goal thy

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

467 by (nat_ind_tac "n" 1);

468 by (Asm_simp_tac 1);

469 by (rtac allI 1);

470 by (exhaust_tac "xs" 1);

471 by (ALLGOALS Asm_simp_tac);

472 by (rtac allI 1);

473 by (exhaust_tac "xs" 1);

474 by (ALLGOALS Asm_simp_tac);

475 qed_spec_mp "nth_append";

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

478 by (induct_tac "xs" 1);

479 (* case [] *)

480 by (Asm_full_simp_tac 1);

481 (* case x#xl *)

482 by (rtac allI 1);

483 by (nat_ind_tac "n" 1);

484 by (ALLGOALS Asm_full_simp_tac);

485 qed_spec_mp "nth_map";

486 Addsimps [nth_map];

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

489 by (induct_tac "xs" 1);

490 (* case [] *)

491 by (Simp_tac 1);

492 (* case x#xl *)

493 by (rtac allI 1);

494 by (nat_ind_tac "n" 1);

495 by (ALLGOALS Asm_full_simp_tac);

496 qed_spec_mp "list_all_nth";

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

499 by (induct_tac "xs" 1);

500 (* case [] *)

501 by (Simp_tac 1);

502 (* case x#xl *)

503 by (rtac allI 1);

504 by (nat_ind_tac "n" 1);

505 (* case 0 *)

506 by (Asm_full_simp_tac 1);

507 (* case Suc x *)

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

509 qed_spec_mp "nth_mem";

510 Addsimps [nth_mem];

512 (** last & butlast **)

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

515 by (induct_tac "xs" 1);

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

517 qed "last_snoc";

518 Addsimps [last_snoc];

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

521 by (induct_tac "xs" 1);

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

523 qed "butlast_snoc";

524 Addsimps [butlast_snoc];

526 goal thy

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

528 by (induct_tac "xs" 1);

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

530 qed_spec_mp "butlast_append";

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

533 by (induct_tac "xs" 1);

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

535 qed_spec_mp "in_set_butlastD";

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

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

539 addsplits [expand_if]) 1);

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

541 qed "in_set_butlast_appendI1";

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

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

545 addsplits [expand_if]) 1);

546 by (Clarify_tac 1);

547 by (Full_simp_tac 1);

548 qed "in_set_butlast_appendI2";

550 (** take & drop **)

551 section "take & drop";

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

554 by (induct_tac "xs" 1);

555 by (ALLGOALS Asm_simp_tac);

556 qed "take_0";

558 goal thy "drop 0 xs = xs";

559 by (induct_tac "xs" 1);

560 by (ALLGOALS Asm_simp_tac);

561 qed "drop_0";

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

564 by (Simp_tac 1);

565 qed "take_Suc_Cons";

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

568 by (Simp_tac 1);

569 qed "drop_Suc_Cons";

571 Delsimps [take_Cons,drop_Cons];

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

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

575 by (nat_ind_tac "n" 1);

576 by (ALLGOALS Asm_simp_tac);

577 by (rtac allI 1);

578 by (exhaust_tac "xs" 1);

579 by (ALLGOALS Asm_simp_tac);

580 qed_spec_mp "length_take";

581 Addsimps [length_take];

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

584 by (nat_ind_tac "n" 1);

585 by (ALLGOALS Asm_simp_tac);

586 by (rtac allI 1);

587 by (exhaust_tac "xs" 1);

588 by (ALLGOALS Asm_simp_tac);

589 qed_spec_mp "length_drop";

590 Addsimps [length_drop];

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

593 by (nat_ind_tac "n" 1);

594 by (ALLGOALS Asm_simp_tac);

595 by (rtac allI 1);

596 by (exhaust_tac "xs" 1);

597 by (ALLGOALS Asm_simp_tac);

598 qed_spec_mp "take_all";

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

601 by (nat_ind_tac "n" 1);

602 by (ALLGOALS Asm_simp_tac);

603 by (rtac allI 1);

604 by (exhaust_tac "xs" 1);

605 by (ALLGOALS Asm_simp_tac);

606 qed_spec_mp "drop_all";

608 goal thy

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

610 by (nat_ind_tac "n" 1);

611 by (ALLGOALS Asm_simp_tac);

612 by (rtac allI 1);

613 by (exhaust_tac "xs" 1);

614 by (ALLGOALS Asm_simp_tac);

615 qed_spec_mp "take_append";

616 Addsimps [take_append];

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

619 by (nat_ind_tac "n" 1);

620 by (ALLGOALS Asm_simp_tac);

621 by (rtac allI 1);

622 by (exhaust_tac "xs" 1);

623 by (ALLGOALS Asm_simp_tac);

624 qed_spec_mp "drop_append";

625 Addsimps [drop_append];

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

628 by (nat_ind_tac "m" 1);

629 by (ALLGOALS Asm_simp_tac);

630 by (rtac allI 1);

631 by (exhaust_tac "xs" 1);

632 by (ALLGOALS Asm_simp_tac);

633 by (rtac allI 1);

634 by (exhaust_tac "n" 1);

635 by (ALLGOALS Asm_simp_tac);

636 qed_spec_mp "take_take";

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

639 by (nat_ind_tac "m" 1);

640 by (ALLGOALS Asm_simp_tac);

641 by (rtac allI 1);

642 by (exhaust_tac "xs" 1);

643 by (ALLGOALS Asm_simp_tac);

644 qed_spec_mp "drop_drop";

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

647 by (nat_ind_tac "m" 1);

648 by (ALLGOALS Asm_simp_tac);

649 by (rtac allI 1);

650 by (exhaust_tac "xs" 1);

651 by (ALLGOALS Asm_simp_tac);

652 qed_spec_mp "take_drop";

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

655 by (nat_ind_tac "n" 1);

656 by (ALLGOALS Asm_simp_tac);

657 by (rtac allI 1);

658 by (exhaust_tac "xs" 1);

659 by (ALLGOALS Asm_simp_tac);

660 qed_spec_mp "take_map";

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

663 by (nat_ind_tac "n" 1);

664 by (ALLGOALS Asm_simp_tac);

665 by (rtac allI 1);

666 by (exhaust_tac "xs" 1);

667 by (ALLGOALS Asm_simp_tac);

668 qed_spec_mp "drop_map";

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

671 by (induct_tac "xs" 1);

672 by (ALLGOALS Asm_simp_tac);

673 by (Clarify_tac 1);

674 by (exhaust_tac "n" 1);

675 by (Blast_tac 1);

676 by (exhaust_tac "i" 1);

677 by (ALLGOALS Asm_full_simp_tac);

678 qed_spec_mp "nth_take";

679 Addsimps [nth_take];

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

682 by (nat_ind_tac "n" 1);

683 by (ALLGOALS Asm_simp_tac);

684 by (rtac allI 1);

685 by (exhaust_tac "xs" 1);

686 by (ALLGOALS Asm_simp_tac);

687 qed_spec_mp "nth_drop";

688 Addsimps [nth_drop];

690 (** takeWhile & dropWhile **)

692 section "takeWhile & dropWhile";

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

695 by (induct_tac "xs" 1);

696 by (Simp_tac 1);

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

698 qed "takeWhile_dropWhile_id";

699 Addsimps [takeWhile_dropWhile_id];

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

702 by (induct_tac "xs" 1);

703 by (Simp_tac 1);

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

705 by (Blast_tac 1);

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

707 Addsimps [takeWhile_append1];

709 goal thy

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

711 by (induct_tac "xs" 1);

712 by (Simp_tac 1);

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

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

715 Addsimps [takeWhile_append2];

717 goal thy

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

719 by (induct_tac "xs" 1);

720 by (Simp_tac 1);

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

722 by (Blast_tac 1);

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

724 Addsimps [dropWhile_append1];

726 goal thy

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

728 by (induct_tac "xs" 1);

729 by (Simp_tac 1);

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

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

732 Addsimps [dropWhile_append2];

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

735 by (induct_tac "xs" 1);

736 by (Simp_tac 1);

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

738 qed_spec_mp"set_take_whileD";

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

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

742 (K [Simp_tac 1]);

744 (** nodups & remdups **)

745 section "nodups & remdups";

747 goal thy "set(remdups xs) = set xs";

748 by (induct_tac "xs" 1);

749 by (Simp_tac 1);

750 by (asm_full_simp_tac (simpset() addsimps [insert_absorb]

751 addsplits [expand_if]) 1);

752 qed "set_remdups";

753 Addsimps [set_remdups];

755 goal thy "nodups(remdups xs)";

756 by (induct_tac "xs" 1);

757 by (Simp_tac 1);

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

759 qed "nodups_remdups";

761 goal thy "nodups xs --> nodups (filter P xs)";

762 by (induct_tac "xs" 1);

763 by (Simp_tac 1);

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

765 qed_spec_mp "nodups_filter";

767 (** replicate **)

768 section "replicate";

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

771 by (induct_tac "n" 1);

772 by (ALLGOALS Asm_full_simp_tac);

773 val lemma = result();

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

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

777 qed "set_replicate";

778 Addsimps [set_replicate];