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

src/HOL/List.ML

author | nipkow |

Mon Jun 30 12:08:19 1997 +0200 (1997-06-30) | |

changeset 3467 | a0797ba03dfe |

parent 3465 | e85c24717cad |

child 3468 | 1f972dc8eafb |

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

More concat lemmas.

1 (* Title: HOL/List

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 1994 TU Muenchen

6 List lemmas

7 *)

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

10 by (induct_tac "xs" 1);

11 by (ALLGOALS Asm_simp_tac);

12 qed_spec_mp "not_Cons_self";

13 Addsimps [not_Cons_self];

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

16 by (induct_tac "xs" 1);

17 by (Simp_tac 1);

18 by (Asm_simp_tac 1);

19 qed "neq_Nil_conv";

22 (** List operator over sets **)

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

25 by (rtac lfp_mono 1);

26 by (REPEAT (ares_tac basic_monos 1));

27 qed "lists_mono";

30 (** list_case **)

32 goal thy

33 "P(list_case a f xs) = ((xs=[] --> P(a)) & \

34 \ (!y ys. xs=y#ys --> P(f y ys)))";

35 by (induct_tac "xs" 1);

36 by (ALLGOALS Asm_simp_tac);

37 by (Blast_tac 1);

38 qed "expand_list_case";

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

41 by (induct_tac "xs" 1);

42 by (REPEAT(resolve_tac prems 1));

43 qed "list_cases";

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

46 by (induct_tac "xs" 1);

47 by (Blast_tac 1);

48 by (Blast_tac 1);

49 bind_thm("list_eq_cases",

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

53 (** @ - append **)

55 section "@ - append";

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

58 by (induct_tac "xs" 1);

59 by (ALLGOALS Asm_simp_tac);

60 qed "append_assoc";

61 Addsimps [append_assoc];

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

64 by (induct_tac "xs" 1);

65 by (ALLGOALS Asm_simp_tac);

66 qed "append_Nil2";

67 Addsimps [append_Nil2];

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

70 by (induct_tac "xs" 1);

71 by (ALLGOALS Asm_simp_tac);

72 qed "append_is_Nil_conv";

73 AddIffs [append_is_Nil_conv];

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

76 by (induct_tac "xs" 1);

77 by (ALLGOALS Asm_simp_tac);

78 by (Blast_tac 1);

79 qed "Nil_is_append_conv";

80 AddIffs [Nil_is_append_conv];

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

83 by (induct_tac "xs" 1);

84 by (ALLGOALS Asm_simp_tac);

85 qed "same_append_eq";

86 AddIffs [same_append_eq];

88 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)";

89 by (induct_tac "xs" 1);

90 by (rtac allI 1);

91 by (induct_tac "ys" 1);

92 by (ALLGOALS Asm_simp_tac);

93 by (rtac allI 1);

94 by (induct_tac "ys" 1);

95 by (ALLGOALS Asm_simp_tac);

96 qed_spec_mp "append1_eq_conv";

97 AddIffs [append1_eq_conv];

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

100 by (induct_tac "xs" 1);

101 by (ALLGOALS Asm_simp_tac);

102 qed_spec_mp "hd_Cons_tl";

103 Addsimps [hd_Cons_tl];

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

106 by (induct_tac "xs" 1);

107 by (ALLGOALS Asm_simp_tac);

108 qed "hd_append";

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

111 by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);

112 qed "tl_append";

114 (** map **)

116 section "map";

118 goal thy

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

120 by (induct_tac "xs" 1);

121 by (ALLGOALS Asm_simp_tac);

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

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

125 by (rtac ext 1);

126 by (induct_tac "xs" 1);

127 by (ALLGOALS Asm_simp_tac);

128 qed "map_ident";

129 Addsimps[map_ident];

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

132 by (induct_tac "xs" 1);

133 by (ALLGOALS Asm_simp_tac);

134 qed "map_append";

135 Addsimps[map_append];

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

138 by (induct_tac "xs" 1);

139 by (ALLGOALS Asm_simp_tac);

140 qed "map_compose";

141 Addsimps[map_compose];

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

144 by (induct_tac "xs" 1);

145 by (ALLGOALS Asm_simp_tac);

146 qed "rev_map";

148 (** rev **)

150 section "rev";

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

153 by (induct_tac "xs" 1);

154 by (ALLGOALS Asm_simp_tac);

155 qed "rev_append";

156 Addsimps[rev_append];

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

159 by (induct_tac "l" 1);

160 by (ALLGOALS Asm_simp_tac);

161 qed "rev_rev_ident";

162 Addsimps[rev_rev_ident];

165 (** mem **)

167 section "mem";

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

170 by (induct_tac "xs" 1);

171 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

172 qed "mem_append";

173 Addsimps[mem_append];

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

176 by (induct_tac "xs" 1);

177 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

178 qed "mem_filter";

179 Addsimps[mem_filter];

181 (** set **)

183 section "set";

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

186 by (induct_tac "xs" 1);

187 by (ALLGOALS Asm_simp_tac);

188 qed "set_of_list_append";

189 Addsimps[set_of_list_append];

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

192 by (induct_tac "xs" 1);

193 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

194 by (Blast_tac 1);

195 qed "set_of_list_mem_eq";

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

198 by (Simp_tac 1);

199 by (Blast_tac 1);

200 qed "set_of_list_subset_Cons";

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

203 by (induct_tac "xs" 1);

204 by (ALLGOALS Asm_simp_tac);

205 qed "set_of_list_empty";

206 Addsimps [set_of_list_empty];

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

209 by (induct_tac "xs" 1);

210 by (ALLGOALS Asm_simp_tac);

211 qed "set_of_list_rev";

212 Addsimps [set_of_list_rev];

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

215 by (induct_tac "xs" 1);

216 by (ALLGOALS Asm_simp_tac);

217 qed "set_of_list_map";

218 Addsimps [set_of_list_map];

221 (** list_all **)

223 section "list_all";

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

226 by (induct_tac "xs" 1);

227 by (ALLGOALS Asm_simp_tac);

228 qed "list_all_True";

229 Addsimps [list_all_True];

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

232 by (induct_tac "xs" 1);

233 by (ALLGOALS Asm_simp_tac);

234 qed "list_all_append";

235 Addsimps [list_all_append];

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

238 by (induct_tac "xs" 1);

239 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

240 by (Blast_tac 1);

241 qed "list_all_mem_conv";

244 (** filter **)

246 section "filter";

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

249 by (induct_tac "xs" 1);

250 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

251 qed "filter_append";

252 Addsimps [filter_append];

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

255 by (induct_tac "xs" 1);

256 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));

257 qed "filter_size";

260 (** concat **)

262 section "concat";

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

265 by (induct_tac "xs" 1);

266 by (ALLGOALS Asm_simp_tac);

267 qed"concat_append";

268 Addsimps [concat_append];

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

271 by (induct_tac "xs" 1);

272 by (ALLGOALS Asm_simp_tac);

273 qed"set_of_list_concat";

274 Addsimps [set_of_list_concat];

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

277 by (induct_tac "xs" 1);

278 by (ALLGOALS Asm_simp_tac);

279 qed "map_concat";

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

282 by (induct_tac "xs" 1);

283 by (ALLGOALS Asm_simp_tac);

284 qed"filter_concat";

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

287 by (induct_tac "xs" 1);

288 by (ALLGOALS Asm_simp_tac);

289 qed "rev_concat";

291 (** length **)

293 section "length";

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

296 by (induct_tac "xs" 1);

297 by (ALLGOALS Asm_simp_tac);

298 qed"length_append";

299 Addsimps [length_append];

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

302 by (induct_tac "l" 1);

303 by (ALLGOALS Simp_tac);

304 qed "length_map";

305 Addsimps [length_map];

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

308 by (induct_tac "xs" 1);

309 by (ALLGOALS Asm_simp_tac);

310 qed "length_rev";

311 Addsimps [length_rev];

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

314 by (induct_tac "xs" 1);

315 by (ALLGOALS Asm_simp_tac);

316 qed "length_0_conv";

317 AddIffs [length_0_conv];

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

320 by (induct_tac "xs" 1);

321 by (ALLGOALS Asm_simp_tac);

322 qed "length_greater_0_conv";

323 AddIffs [length_greater_0_conv];

326 (** nth **)

328 section "nth";

330 goal thy

331 "!xs. nth n (xs@ys) = \

332 \ (if n < length xs then nth n xs else nth (n - length xs) ys)";

333 by (nat_ind_tac "n" 1);

334 by (Asm_simp_tac 1);

335 by (rtac allI 1);

336 by (exhaust_tac "xs" 1);

337 by (ALLGOALS Asm_simp_tac);

338 by (rtac allI 1);

339 by (exhaust_tac "xs" 1);

340 by (ALLGOALS Asm_simp_tac);

341 qed_spec_mp "nth_append";

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

344 by (induct_tac "xs" 1);

345 (* case [] *)

346 by (Asm_full_simp_tac 1);

347 (* case x#xl *)

348 by (rtac allI 1);

349 by (nat_ind_tac "n" 1);

350 by (ALLGOALS Asm_full_simp_tac);

351 qed_spec_mp "nth_map";

352 Addsimps [nth_map];

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

355 by (induct_tac "xs" 1);

356 (* case [] *)

357 by (Simp_tac 1);

358 (* case x#xl *)

359 by (rtac allI 1);

360 by (nat_ind_tac "n" 1);

361 by (ALLGOALS Asm_full_simp_tac);

362 qed_spec_mp "list_all_nth";

364 goal thy "!n. n < length xs --> (nth n xs) mem xs";

365 by (induct_tac "xs" 1);

366 (* case [] *)

367 by (Simp_tac 1);

368 (* case x#xl *)

369 by (rtac allI 1);

370 by (nat_ind_tac "n" 1);

371 (* case 0 *)

372 by (Asm_full_simp_tac 1);

373 (* case Suc x *)

374 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);

375 qed_spec_mp "nth_mem";

376 Addsimps [nth_mem];

379 (** take & drop **)

380 section "take & drop";

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

383 by (induct_tac "xs" 1);

384 by (ALLGOALS Asm_simp_tac);

385 qed "take_0";

387 goal thy "drop 0 xs = xs";

388 by (induct_tac "xs" 1);

389 by (ALLGOALS Asm_simp_tac);

390 qed "drop_0";

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

393 by (Simp_tac 1);

394 qed "take_Suc_Cons";

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

397 by (Simp_tac 1);

398 qed "drop_Suc_Cons";

400 Delsimps [take_Cons,drop_Cons];

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

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

404 by (nat_ind_tac "n" 1);

405 by (ALLGOALS Asm_simp_tac);

406 by (rtac allI 1);

407 by (exhaust_tac "xs" 1);

408 by (ALLGOALS Asm_simp_tac);

409 qed_spec_mp "length_take";

410 Addsimps [length_take];

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

413 by (nat_ind_tac "n" 1);

414 by (ALLGOALS Asm_simp_tac);

415 by (rtac allI 1);

416 by (exhaust_tac "xs" 1);

417 by (ALLGOALS Asm_simp_tac);

418 qed_spec_mp "length_drop";

419 Addsimps [length_drop];

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

422 by (nat_ind_tac "n" 1);

423 by (ALLGOALS Asm_simp_tac);

424 by (rtac allI 1);

425 by (exhaust_tac "xs" 1);

426 by (ALLGOALS Asm_simp_tac);

427 qed_spec_mp "take_all";

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

430 by (nat_ind_tac "n" 1);

431 by (ALLGOALS Asm_simp_tac);

432 by (rtac allI 1);

433 by (exhaust_tac "xs" 1);

434 by (ALLGOALS Asm_simp_tac);

435 qed_spec_mp "drop_all";

437 goal thy

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

439 by (nat_ind_tac "n" 1);

440 by (ALLGOALS Asm_simp_tac);

441 by (rtac allI 1);

442 by (exhaust_tac "xs" 1);

443 by (ALLGOALS Asm_simp_tac);

444 qed_spec_mp "take_append";

445 Addsimps [take_append];

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

448 by (nat_ind_tac "n" 1);

449 by (ALLGOALS Asm_simp_tac);

450 by (rtac allI 1);

451 by (exhaust_tac "xs" 1);

452 by (ALLGOALS Asm_simp_tac);

453 qed_spec_mp "drop_append";

454 Addsimps [drop_append];

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

457 by (nat_ind_tac "m" 1);

458 by (ALLGOALS Asm_simp_tac);

459 by (rtac allI 1);

460 by (exhaust_tac "xs" 1);

461 by (ALLGOALS Asm_simp_tac);

462 by (rtac allI 1);

463 by (exhaust_tac "n" 1);

464 by (ALLGOALS Asm_simp_tac);

465 qed_spec_mp "take_take";

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

468 by (nat_ind_tac "m" 1);

469 by (ALLGOALS Asm_simp_tac);

470 by (rtac allI 1);

471 by (exhaust_tac "xs" 1);

472 by (ALLGOALS Asm_simp_tac);

473 qed_spec_mp "drop_drop";

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

476 by (nat_ind_tac "m" 1);

477 by (ALLGOALS Asm_simp_tac);

478 by (rtac allI 1);

479 by (exhaust_tac "xs" 1);

480 by (ALLGOALS Asm_simp_tac);

481 qed_spec_mp "take_drop";

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

484 by (nat_ind_tac "n" 1);

485 by (ALLGOALS Asm_simp_tac);

486 by (rtac allI 1);

487 by (exhaust_tac "xs" 1);

488 by (ALLGOALS Asm_simp_tac);

489 qed_spec_mp "take_map";

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

492 by (nat_ind_tac "n" 1);

493 by (ALLGOALS Asm_simp_tac);

494 by (rtac allI 1);

495 by (exhaust_tac "xs" 1);

496 by (ALLGOALS Asm_simp_tac);

497 qed_spec_mp "drop_map";

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

500 by (induct_tac "xs" 1);

501 by (ALLGOALS Asm_simp_tac);

502 by (strip_tac 1);

503 by (exhaust_tac "n" 1);

504 by (Blast_tac 1);

505 by (exhaust_tac "i" 1);

506 by (ALLGOALS Asm_full_simp_tac);

507 qed_spec_mp "nth_take";

508 Addsimps [nth_take];

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

511 by (nat_ind_tac "n" 1);

512 by (ALLGOALS Asm_simp_tac);

513 by (rtac allI 1);

514 by (exhaust_tac "xs" 1);

515 by (ALLGOALS Asm_simp_tac);

516 qed_spec_mp "nth_drop";

517 Addsimps [nth_drop];

519 (** takeWhile & dropWhile **)

521 section "takeWhile & dropWhile";

523 goal thy

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

525 by (induct_tac "xs" 1);

526 by (Simp_tac 1);

527 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);

528 by (Blast_tac 1);

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

530 Addsimps [takeWhile_append1];

532 goal thy

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

534 by (induct_tac "xs" 1);

535 by (Simp_tac 1);

536 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);

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

538 Addsimps [takeWhile_append2];

540 goal thy

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

542 by (induct_tac "xs" 1);

543 by (Simp_tac 1);

544 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);

545 by (Blast_tac 1);

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

547 Addsimps [dropWhile_append1];

549 goal thy

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

551 by (induct_tac "xs" 1);

552 by (Simp_tac 1);

553 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);

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

555 Addsimps [dropWhile_append2];

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

558 by (induct_tac "xs" 1);

559 by (Simp_tac 1);

560 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);

561 qed_spec_mp"set_of_list_take_whileD";