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

src/HOL/List.ML

author | nipkow |

Sun Jul 18 11:06:08 1999 +0200 (1999-07-18) | |

changeset 7028 | 6ea3b385e731 |

parent 6831 | 799859f2e657 |

child 7032 | d6efb3b8e669 |

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

Modifid length_tl

1 (* Title: HOL/List

2 ID: $Id$

3 Author: Tobias Nipkow

4 Copyright 1994 TU Muenchen

6 List lemmas

7 *)

9 Goal "!x. xs ~= x#xs";

10 by (induct_tac "xs" 1);

11 by Auto_tac;

12 qed_spec_mp "not_Cons_self";

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

14 Addsimps [not_Cons_self,not_Cons_self2];

16 Goal "(xs ~= []) = (? y ys. xs = y#ys)";

17 by (induct_tac "xs" 1);

18 by Auto_tac;

19 qed "neq_Nil_conv";

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

22 val [prem] = Goal

23 "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";

24 by (rtac measure_induct 1 THEN etac prem 1);

25 qed "length_induct";

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

30 Goalw lists.defs "A<=B ==> lists A <= lists B";

31 by (rtac lfp_mono 1);

32 by (REPEAT (ares_tac basic_monos 1));

33 qed "lists_mono";

35 val listsE = lists.mk_cases "x#l : lists A";

36 AddSEs [listsE];

37 AddSIs lists.intrs;

39 Goal "l: lists A ==> l: lists B --> l: lists (A Int B)";

40 by (etac lists.induct 1);

41 by (ALLGOALS Blast_tac);

42 qed_spec_mp "lists_IntI";

44 Goal "lists (A Int B) = lists A Int lists B";

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

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

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

48 qed "lists_Int_eq";

49 Addsimps [lists_Int_eq];

52 (** Case analysis **)

53 section "Case analysis";

55 val prems = Goal "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";

56 by (induct_tac "xs" 1);

57 by (REPEAT(resolve_tac prems 1));

58 qed "list_cases";

60 Goal "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";

61 by (induct_tac "xs" 1);

62 by (Blast_tac 1);

63 by (Blast_tac 1);

64 bind_thm("list_eq_cases",

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

67 (** length **)

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

70 section "length";

72 Goal "length(xs@ys) = length(xs)+length(ys)";

73 by (induct_tac "xs" 1);

74 by Auto_tac;

75 qed"length_append";

76 Addsimps [length_append];

78 Goal "length (map f xs) = length xs";

79 by (induct_tac "xs" 1);

80 by Auto_tac;

81 qed "length_map";

82 Addsimps [length_map];

84 Goal "length(rev xs) = length(xs)";

85 by (induct_tac "xs" 1);

86 by Auto_tac;

87 qed "length_rev";

88 Addsimps [length_rev];

90 Goal "length(tl xs) = (length xs) - 1";

91 by (exhaust_tac "xs" 1);

92 by Auto_tac;

93 qed "length_tl";

94 Addsimps [length_tl];

96 Goal "(length xs = 0) = (xs = [])";

97 by (induct_tac "xs" 1);

98 by Auto_tac;

99 qed "length_0_conv";

100 AddIffs [length_0_conv];

102 Goal "(0 = length xs) = (xs = [])";

103 by (induct_tac "xs" 1);

104 by Auto_tac;

105 qed "zero_length_conv";

106 AddIffs [zero_length_conv];

108 Goal "(0 < length xs) = (xs ~= [])";

109 by (induct_tac "xs" 1);

110 by Auto_tac;

111 qed "length_greater_0_conv";

112 AddIffs [length_greater_0_conv];

114 Goal "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)";

115 by (induct_tac "xs" 1);

116 by Auto_tac;

117 qed "length_Suc_conv";

119 (** @ - append **)

121 section "@ - append";

123 Goal "(xs@ys)@zs = xs@(ys@zs)";

124 by (induct_tac "xs" 1);

125 by Auto_tac;

126 qed "append_assoc";

127 Addsimps [append_assoc];

129 Goal "xs @ [] = xs";

130 by (induct_tac "xs" 1);

131 by Auto_tac;

132 qed "append_Nil2";

133 Addsimps [append_Nil2];

135 Goal "(xs@ys = []) = (xs=[] & ys=[])";

136 by (induct_tac "xs" 1);

137 by Auto_tac;

138 qed "append_is_Nil_conv";

139 AddIffs [append_is_Nil_conv];

141 Goal "([] = xs@ys) = (xs=[] & ys=[])";

142 by (induct_tac "xs" 1);

143 by Auto_tac;

144 qed "Nil_is_append_conv";

145 AddIffs [Nil_is_append_conv];

147 Goal "(xs @ ys = xs) = (ys=[])";

148 by (induct_tac "xs" 1);

149 by Auto_tac;

150 qed "append_self_conv";

152 Goal "(xs = xs @ ys) = (ys=[])";

153 by (induct_tac "xs" 1);

154 by Auto_tac;

155 qed "self_append_conv";

156 AddIffs [append_self_conv,self_append_conv];

158 Goal "!ys. length xs = length ys | length us = length vs \

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

160 by (induct_tac "xs" 1);

161 by (rtac allI 1);

162 by (exhaust_tac "ys" 1);

163 by (Asm_simp_tac 1);

164 by (Force_tac 1);

165 by (rtac allI 1);

166 by (exhaust_tac "ys" 1);

167 by (Force_tac 1);

168 by (Asm_simp_tac 1);

169 qed_spec_mp "append_eq_append_conv";

170 Addsimps [append_eq_append_conv];

172 Goal "(xs @ ys = xs @ zs) = (ys=zs)";

173 by (Simp_tac 1);

174 qed "same_append_eq";

176 Goal "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)";

177 by (Simp_tac 1);

178 qed "append1_eq_conv";

180 Goal "(ys @ xs = zs @ xs) = (ys=zs)";

181 by (Simp_tac 1);

182 qed "append_same_eq";

184 AddSIs

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

186 AddSDs

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

189 Goal "(xs @ ys = ys) = (xs=[])";

190 by (cut_inst_tac [("zs","[]")] append_same_eq 1);

191 by Auto_tac;

192 qed "append_self_conv2";

194 Goal "(ys = xs @ ys) = (xs=[])";

195 by (simp_tac (simpset() addsimps

196 [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);

197 by (Blast_tac 1);

198 qed "self_append_conv2";

199 AddIffs [append_self_conv2,self_append_conv2];

201 Goal "xs ~= [] --> hd xs # tl xs = xs";

202 by (induct_tac "xs" 1);

203 by Auto_tac;

204 qed_spec_mp "hd_Cons_tl";

205 Addsimps [hd_Cons_tl];

207 Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";

208 by (induct_tac "xs" 1);

209 by Auto_tac;

210 qed "hd_append";

212 Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";

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

214 addsplits [list.split]) 1);

215 qed "hd_append2";

216 Addsimps [hd_append2];

218 Goal "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";

219 by (simp_tac (simpset() addsplits [list.split]) 1);

220 qed "tl_append";

222 Goal "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";

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

224 addsplits [list.split]) 1);

225 qed "tl_append2";

226 Addsimps [tl_append2];

228 (* trivial rules for solving @-equations automatically *)

230 Goal "xs = ys ==> xs = [] @ ys";

231 by (Asm_simp_tac 1);

232 qed "eq_Nil_appendI";

234 Goal "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs";

235 by (dtac sym 1);

236 by (Asm_simp_tac 1);

237 qed "Cons_eq_appendI";

239 Goal "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us";

240 by (dtac sym 1);

241 by (Asm_simp_tac 1);

242 qed "append_eq_appendI";

245 (***

246 Simplification procedure for all list equalities.

247 Currently only tries to rearranges @ to see if

248 - both lists end in a singleton list,

249 - or both lists end in the same list.

250 ***)

251 local

253 val list_eq_pattern =

254 Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);

256 fun last (cons as Const("List.list.op #",_) $ _ $ xs) =

257 (case xs of Const("List.list.[]",_) => cons | _ => last xs)

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

259 | last t = t;

261 fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true

262 | list1 _ = false;

264 fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =

265 (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)

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

267 | butlast xs = Const("List.list.[]",fastype_of xs);

269 val rearr_tac =

270 simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);

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

273 let

274 val lastl = last lhs and lastr = last rhs

275 fun rearr conv =

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

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

278 val appT = [listT,listT] ---> listT

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

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

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

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

283 handle ERROR =>

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

285 string_of_cterm ct)

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

288 in if list1 lastl andalso list1 lastr

289 then rearr append1_eq_conv

290 else

291 if lastl aconv lastr

292 then rearr append_same_eq

293 else None

294 end;

295 in

296 val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;

297 end;

299 Addsimprocs [list_eq_simproc];

302 (** map **)

304 section "map";

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

307 by (induct_tac "xs" 1);

308 by Auto_tac;

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

311 Goal "map (%x. x) = (%xs. xs)";

312 by (rtac ext 1);

313 by (induct_tac "xs" 1);

314 by Auto_tac;

315 qed "map_ident";

316 Addsimps[map_ident];

318 Goal "map f (xs@ys) = map f xs @ map f ys";

319 by (induct_tac "xs" 1);

320 by Auto_tac;

321 qed "map_append";

322 Addsimps[map_append];

324 Goalw [o_def] "map (f o g) xs = map f (map g xs)";

325 by (induct_tac "xs" 1);

326 by Auto_tac;

327 qed "map_compose";

328 Addsimps[map_compose];

330 Goal "rev(map f xs) = map f (rev xs)";

331 by (induct_tac "xs" 1);

332 by Auto_tac;

333 qed "rev_map";

335 (* a congruence rule for map: *)

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

337 by (hyp_subst_tac 1);

338 by (induct_tac "ys" 1);

339 by Auto_tac;

340 bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));

342 Goal "(map f xs = []) = (xs = [])";

343 by (induct_tac "xs" 1);

344 by Auto_tac;

345 qed "map_is_Nil_conv";

346 AddIffs [map_is_Nil_conv];

348 Goal "([] = map f xs) = (xs = [])";

349 by (induct_tac "xs" 1);

350 by Auto_tac;

351 qed "Nil_is_map_conv";

352 AddIffs [Nil_is_map_conv];

355 (** rev **)

357 section "rev";

359 Goal "rev(xs@ys) = rev(ys) @ rev(xs)";

360 by (induct_tac "xs" 1);

361 by Auto_tac;

362 qed "rev_append";

363 Addsimps[rev_append];

365 Goal "rev(rev l) = l";

366 by (induct_tac "l" 1);

367 by Auto_tac;

368 qed "rev_rev_ident";

369 Addsimps[rev_rev_ident];

371 Goal "(rev xs = []) = (xs = [])";

372 by (induct_tac "xs" 1);

373 by Auto_tac;

374 qed "rev_is_Nil_conv";

375 AddIffs [rev_is_Nil_conv];

377 Goal "([] = rev xs) = (xs = [])";

378 by (induct_tac "xs" 1);

379 by Auto_tac;

380 qed "Nil_is_rev_conv";

381 AddIffs [Nil_is_rev_conv];

383 Goal "!ys. (rev xs = rev ys) = (xs = ys)";

384 by (induct_tac "xs" 1);

385 by (Force_tac 1);

386 by (rtac allI 1);

387 by (exhaust_tac "ys" 1);

388 by (Asm_simp_tac 1);

389 by (Force_tac 1);

390 qed_spec_mp "rev_is_rev_conv";

391 AddIffs [rev_is_rev_conv];

393 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";

394 by (stac (rev_rev_ident RS sym) 1);

395 by (res_inst_tac [("list", "rev xs")] list.induct 1);

396 by (ALLGOALS Simp_tac);

397 by (resolve_tac prems 1);

398 by (eresolve_tac prems 1);

399 qed "rev_induct";

401 fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;

403 Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";

404 by (res_inst_tac [("xs","xs")] rev_induct 1);

405 by Auto_tac;

406 bind_thm ("rev_exhaust",

407 impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));

410 (** set **)

412 section "set";

414 qed_goal "finite_set" thy "finite (set xs)"

415 (K [induct_tac "xs" 1, Auto_tac]);

416 Addsimps[finite_set];

417 AddSIs[finite_set];

419 Goal "set (xs@ys) = (set xs Un set ys)";

420 by (induct_tac "xs" 1);

421 by Auto_tac;

422 qed "set_append";

423 Addsimps[set_append];

425 Goal "set l <= set (x#l)";

426 by Auto_tac;

427 qed "set_subset_Cons";

429 Goal "(set xs = {}) = (xs = [])";

430 by (induct_tac "xs" 1);

431 by Auto_tac;

432 qed "set_empty";

433 Addsimps [set_empty];

435 Goal "set(rev xs) = set(xs)";

436 by (induct_tac "xs" 1);

437 by Auto_tac;

438 qed "set_rev";

439 Addsimps [set_rev];

441 Goal "set(map f xs) = f``(set xs)";

442 by (induct_tac "xs" 1);

443 by Auto_tac;

444 qed "set_map";

445 Addsimps [set_map];

447 Goal "set(filter P xs) = {x. x : set xs & P x}";

448 by (induct_tac "xs" 1);

449 by Auto_tac;

450 qed "set_filter";

451 Addsimps [set_filter];

452 (*

453 Goal "(x : set (filter P xs)) = (x : set xs & P x)";

454 by (induct_tac "xs" 1);

455 by Auto_tac;

456 qed "in_set_filter";

457 Addsimps [in_set_filter];

458 *)

459 Goal "set[i..j(] = {k. i <= k & k < j}";

460 by (induct_tac "j" 1);

461 by Auto_tac;

462 by (arith_tac 1);

463 qed "set_upt";

464 Addsimps [set_upt];

466 Goal "!i < size xs. set(xs[i := x]) <= insert x (set xs)";

467 by (induct_tac "xs" 1);

468 by (Simp_tac 1);

469 by (asm_simp_tac (simpset() addsplits [nat.split]) 1);

470 by (Blast_tac 1);

471 qed_spec_mp "set_list_update_subset";

473 Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";

474 by (induct_tac "xs" 1);

475 by (Simp_tac 1);

476 by (Asm_simp_tac 1);

477 by (rtac iffI 1);

478 by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);

479 by (REPEAT(etac exE 1));

480 by (exhaust_tac "ys" 1);

481 by Auto_tac;

482 qed "in_set_conv_decomp";

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

486 Goal "(xs : lists A) = (!x : set xs. x : A)";

487 by (induct_tac "xs" 1);

488 by Auto_tac;

489 qed "in_lists_conv_set";

491 bind_thm("in_listsD",in_lists_conv_set RS iffD1);

492 AddSDs [in_listsD];

493 bind_thm("in_listsI",in_lists_conv_set RS iffD2);

494 AddSIs [in_listsI];

496 (** mem **)

498 section "mem";

500 Goal "(x mem xs) = (x: set xs)";

501 by (induct_tac "xs" 1);

502 by Auto_tac;

503 qed "set_mem_eq";

506 (** list_all **)

508 section "list_all";

510 Goal "list_all P xs = (!x:set xs. P x)";

511 by (induct_tac "xs" 1);

512 by Auto_tac;

513 qed "list_all_conv";

515 Goal "list_all P (xs@ys) = (list_all P xs & list_all P ys)";

516 by (induct_tac "xs" 1);

517 by Auto_tac;

518 qed "list_all_append";

519 Addsimps [list_all_append];

522 (** filter **)

524 section "filter";

526 Goal "filter P (xs@ys) = filter P xs @ filter P ys";

527 by (induct_tac "xs" 1);

528 by Auto_tac;

529 qed "filter_append";

530 Addsimps [filter_append];

532 Goal "filter (%x. True) xs = xs";

533 by (induct_tac "xs" 1);

534 by Auto_tac;

535 qed "filter_True";

536 Addsimps [filter_True];

538 Goal "filter (%x. False) xs = []";

539 by (induct_tac "xs" 1);

540 by Auto_tac;

541 qed "filter_False";

542 Addsimps [filter_False];

544 Goal "length (filter P xs) <= length xs";

545 by (induct_tac "xs" 1);

546 by Auto_tac;

547 qed "length_filter";

548 Addsimps[length_filter];

550 Goal "set (filter P xs) <= set xs";

551 by Auto_tac;

552 qed "filter_is_subset";

553 Addsimps [filter_is_subset];

556 section "concat";

558 Goal "concat(xs@ys) = concat(xs)@concat(ys)";

559 by (induct_tac "xs" 1);

560 by Auto_tac;

561 qed"concat_append";

562 Addsimps [concat_append];

564 Goal "(concat xss = []) = (!xs:set xss. xs=[])";

565 by (induct_tac "xss" 1);

566 by Auto_tac;

567 qed "concat_eq_Nil_conv";

568 AddIffs [concat_eq_Nil_conv];

570 Goal "([] = concat xss) = (!xs:set xss. xs=[])";

571 by (induct_tac "xss" 1);

572 by Auto_tac;

573 qed "Nil_eq_concat_conv";

574 AddIffs [Nil_eq_concat_conv];

576 Goal "set(concat xs) = Union(set `` set xs)";

577 by (induct_tac "xs" 1);

578 by Auto_tac;

579 qed"set_concat";

580 Addsimps [set_concat];

582 Goal "map f (concat xs) = concat (map (map f) xs)";

583 by (induct_tac "xs" 1);

584 by Auto_tac;

585 qed "map_concat";

587 Goal "filter p (concat xs) = concat (map (filter p) xs)";

588 by (induct_tac "xs" 1);

589 by Auto_tac;

590 qed"filter_concat";

592 Goal "rev(concat xs) = concat (map rev (rev xs))";

593 by (induct_tac "xs" 1);

594 by Auto_tac;

595 qed "rev_concat";

597 (** nth **)

599 section "nth";

601 Goal "(x#xs)!0 = x";

602 by Auto_tac;

603 qed "nth_Cons_0";

604 Addsimps [nth_Cons_0];

606 Goal "(x#xs)!(Suc n) = xs!n";

607 by Auto_tac;

608 qed "nth_Cons_Suc";

609 Addsimps [nth_Cons_Suc];

611 Delsimps (thms "nth.simps");

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

614 by (induct_tac "xs" 1);

615 by (Asm_simp_tac 1);

616 by (rtac allI 1);

617 by (exhaust_tac "n" 1);

618 by Auto_tac;

619 qed_spec_mp "nth_append";

621 Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";

622 by (induct_tac "xs" 1);

623 (* case [] *)

624 by (Asm_full_simp_tac 1);

625 (* case x#xl *)

626 by (rtac allI 1);

627 by (induct_tac "n" 1);

628 by Auto_tac;

629 qed_spec_mp "nth_map";

630 Addsimps [nth_map];

632 Goal "!n. n < length xs --> Ball (set xs) P --> P(xs!n)";

633 by (induct_tac "xs" 1);

634 (* case [] *)

635 by (Simp_tac 1);

636 (* case x#xl *)

637 by (rtac allI 1);

638 by (induct_tac "n" 1);

639 by Auto_tac;

640 qed_spec_mp "list_ball_nth";

642 Goal "!n. n < length xs --> xs!n : set xs";

643 by (induct_tac "xs" 1);

644 (* case [] *)

645 by (Simp_tac 1);

646 (* case x#xl *)

647 by (rtac allI 1);

648 by (induct_tac "n" 1);

649 (* case 0 *)

650 by (Asm_full_simp_tac 1);

651 (* case Suc x *)

652 by (Asm_full_simp_tac 1);

653 qed_spec_mp "nth_mem";

654 Addsimps [nth_mem];

657 (** list update **)

659 section "list update";

661 Goal "!i. length(xs[i:=x]) = length xs";

662 by (induct_tac "xs" 1);

663 by (Simp_tac 1);

664 by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);

665 qed_spec_mp "length_list_update";

666 Addsimps [length_list_update];

668 Goal "!i j. i < length xs --> (xs[i:=x])!j = (if i=j then x else xs!j)";

669 by (induct_tac "xs" 1);

670 by (Simp_tac 1);

671 by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));

672 qed_spec_mp "nth_list_update";

674 Goal "!i. i < size xs --> xs[i:=x, i:=y] = xs[i:=y]";

675 by (induct_tac "xs" 1);

676 by (Simp_tac 1);

677 by (asm_simp_tac (simpset() addsplits [nat.split]) 1);

678 qed_spec_mp "list_update_overwrite";

679 Addsimps [list_update_overwrite];

681 Goal "!i < length xs. (xs[i := x] = xs) = (xs!i = x)";

682 by (induct_tac "xs" 1);

683 by (Simp_tac 1);

684 by (simp_tac (simpset() addsplits [nat.split]) 1);

685 by (Blast_tac 1);

686 qed_spec_mp "list_update_same_conv";

689 (** last & butlast **)

691 section "last / butlast";

693 Goal "last(xs@[x]) = x";

694 by (induct_tac "xs" 1);

695 by Auto_tac;

696 qed "last_snoc";

697 Addsimps [last_snoc];

699 Goal "butlast(xs@[x]) = xs";

700 by (induct_tac "xs" 1);

701 by Auto_tac;

702 qed "butlast_snoc";

703 Addsimps [butlast_snoc];

705 Goal "length(butlast xs) = length xs - 1";

706 by (res_inst_tac [("xs","xs")] rev_induct 1);

707 by Auto_tac;

708 qed "length_butlast";

709 Addsimps [length_butlast];

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

712 by (induct_tac "xs" 1);

713 by Auto_tac;

714 qed_spec_mp "butlast_append";

716 Goal "x:set(butlast xs) --> x:set xs";

717 by (induct_tac "xs" 1);

718 by Auto_tac;

719 qed_spec_mp "in_set_butlastD";

721 Goal "x:set(butlast xs) | x:set(butlast ys) ==> x:set(butlast(xs@ys))";

722 by (auto_tac (claset() addDs [in_set_butlastD],

723 simpset() addsimps [butlast_append]));

724 qed "in_set_butlast_appendI";

726 (** take & drop **)

727 section "take & drop";

729 Goal "take 0 xs = []";

730 by (induct_tac "xs" 1);

731 by Auto_tac;

732 qed "take_0";

734 Goal "drop 0 xs = xs";

735 by (induct_tac "xs" 1);

736 by Auto_tac;

737 qed "drop_0";

739 Goal "take (Suc n) (x#xs) = x # take n xs";

740 by (Simp_tac 1);

741 qed "take_Suc_Cons";

743 Goal "drop (Suc n) (x#xs) = drop n xs";

744 by (Simp_tac 1);

745 qed "drop_Suc_Cons";

747 Delsimps [take_Cons,drop_Cons];

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

750 Goal "!xs. length(take n xs) = min (length xs) n";

751 by (induct_tac "n" 1);

752 by Auto_tac;

753 by (exhaust_tac "xs" 1);

754 by Auto_tac;

755 qed_spec_mp "length_take";

756 Addsimps [length_take];

758 Goal "!xs. length(drop n xs) = (length xs - n)";

759 by (induct_tac "n" 1);

760 by Auto_tac;

761 by (exhaust_tac "xs" 1);

762 by Auto_tac;

763 qed_spec_mp "length_drop";

764 Addsimps [length_drop];

766 Goal "!xs. length xs <= n --> take n xs = xs";

767 by (induct_tac "n" 1);

768 by Auto_tac;

769 by (exhaust_tac "xs" 1);

770 by Auto_tac;

771 qed_spec_mp "take_all";

773 Goal "!xs. length xs <= n --> drop n xs = []";

774 by (induct_tac "n" 1);

775 by Auto_tac;

776 by (exhaust_tac "xs" 1);

777 by Auto_tac;

778 qed_spec_mp "drop_all";

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

781 by (induct_tac "n" 1);

782 by Auto_tac;

783 by (exhaust_tac "xs" 1);

784 by Auto_tac;

785 qed_spec_mp "take_append";

786 Addsimps [take_append];

788 Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";

789 by (induct_tac "n" 1);

790 by Auto_tac;

791 by (exhaust_tac "xs" 1);

792 by Auto_tac;

793 qed_spec_mp "drop_append";

794 Addsimps [drop_append];

796 Goal "!xs n. take n (take m xs) = take (min n m) xs";

797 by (induct_tac "m" 1);

798 by Auto_tac;

799 by (exhaust_tac "xs" 1);

800 by Auto_tac;

801 by (exhaust_tac "na" 1);

802 by Auto_tac;

803 qed_spec_mp "take_take";

805 Goal "!xs. drop n (drop m xs) = drop (n + m) xs";

806 by (induct_tac "m" 1);

807 by Auto_tac;

808 by (exhaust_tac "xs" 1);

809 by Auto_tac;

810 qed_spec_mp "drop_drop";

812 Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";

813 by (induct_tac "m" 1);

814 by Auto_tac;

815 by (exhaust_tac "xs" 1);

816 by Auto_tac;

817 qed_spec_mp "take_drop";

819 Goal "!xs. take n xs @ drop n xs = xs";

820 by (induct_tac "n" 1);

821 by Auto_tac;

822 by (exhaust_tac "xs" 1);

823 by Auto_tac;

824 qed_spec_mp "append_take_drop_id";

826 Goal "!xs. take n (map f xs) = map f (take n xs)";

827 by (induct_tac "n" 1);

828 by Auto_tac;

829 by (exhaust_tac "xs" 1);

830 by Auto_tac;

831 qed_spec_mp "take_map";

833 Goal "!xs. drop n (map f xs) = map f (drop n xs)";

834 by (induct_tac "n" 1);

835 by Auto_tac;

836 by (exhaust_tac "xs" 1);

837 by Auto_tac;

838 qed_spec_mp "drop_map";

840 Goal "!n i. i < n --> (take n xs)!i = xs!i";

841 by (induct_tac "xs" 1);

842 by Auto_tac;

843 by (exhaust_tac "n" 1);

844 by (Blast_tac 1);

845 by (exhaust_tac "i" 1);

846 by Auto_tac;

847 qed_spec_mp "nth_take";

848 Addsimps [nth_take];

850 Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";

851 by (induct_tac "n" 1);

852 by Auto_tac;

853 by (exhaust_tac "xs" 1);

854 by Auto_tac;

855 qed_spec_mp "nth_drop";

856 Addsimps [nth_drop];

858 (** takeWhile & dropWhile **)

860 section "takeWhile & dropWhile";

862 Goal "takeWhile P xs @ dropWhile P xs = xs";

863 by (induct_tac "xs" 1);

864 by Auto_tac;

865 qed "takeWhile_dropWhile_id";

866 Addsimps [takeWhile_dropWhile_id];

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

869 by (induct_tac "xs" 1);

870 by Auto_tac;

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

872 Addsimps [takeWhile_append1];

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

875 by (induct_tac "xs" 1);

876 by Auto_tac;

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

878 Addsimps [takeWhile_append2];

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

881 by (induct_tac "xs" 1);

882 by Auto_tac;

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

884 Addsimps [dropWhile_append1];

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

887 by (induct_tac "xs" 1);

888 by Auto_tac;

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

890 Addsimps [dropWhile_append2];

892 Goal "x:set(takeWhile P xs) --> x:set xs & P x";

893 by (induct_tac "xs" 1);

894 by Auto_tac;

895 qed_spec_mp"set_take_whileD";

897 (** zip **)

898 section "zip";

900 Goal "zip [] ys = []";

901 by (induct_tac "ys" 1);

902 by Auto_tac;

903 qed "zip_Nil";

904 Addsimps [zip_Nil];

906 Goal "zip (x#xs) (y#ys) = (x,y)#zip xs ys";

907 by (Simp_tac 1);

908 qed "zip_Cons_Cons";

909 Addsimps [zip_Cons_Cons];

911 Delsimps(tl (thms"zip.simps"));

914 (** foldl **)

915 section "foldl";

917 Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";

918 by (induct_tac "xs" 1);

919 by Auto_tac;

920 qed_spec_mp "foldl_append";

921 Addsimps [foldl_append];

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

924 because it requires an additional transitivity step

925 *)

926 Goal "!n::nat. m <= n --> m <= foldl op+ n ns";

927 by (induct_tac "ns" 1);

928 by Auto_tac;

929 qed_spec_mp "start_le_sum";

931 Goal "n : set ns ==> n <= foldl op+ 0 ns";

932 by (force_tac (claset() addIs [start_le_sum],

933 simpset() addsimps [in_set_conv_decomp]) 1);

934 qed "elem_le_sum";

936 Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";

937 by (induct_tac "ns" 1);

938 by Auto_tac;

939 qed_spec_mp "sum_eq_0_conv";

940 AddIffs [sum_eq_0_conv];

942 (** upto **)

944 (* Does not terminate! *)

945 Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";

946 by (induct_tac "j" 1);

947 by Auto_tac;

948 qed "upt_rec";

950 Goal "j<=i ==> [i..j(] = []";

951 by (stac upt_rec 1);

952 by (Asm_simp_tac 1);

953 qed "upt_conv_Nil";

954 Addsimps [upt_conv_Nil];

956 Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";

957 by (Asm_simp_tac 1);

958 qed "upt_Suc";

960 Goal "i<j ==> [i..j(] = i#[Suc i..j(]";

961 by (rtac trans 1);

962 by (stac upt_rec 1);

963 by (rtac refl 2);

964 by (Asm_simp_tac 1);

965 qed "upt_conv_Cons";

967 Goal "length [i..j(] = j-i";

968 by (induct_tac "j" 1);

969 by (Simp_tac 1);

970 by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);

971 qed "length_upt";

972 Addsimps [length_upt];

974 Goal "i+k < j --> [i..j(] ! k = i+k";

975 by (induct_tac "j" 1);

976 by (Simp_tac 1);

977 by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);

978 by (Clarify_tac 1);

979 by (subgoal_tac "n=i+k" 1);

980 by (Asm_simp_tac 2);

981 by (Asm_simp_tac 1);

982 qed_spec_mp "nth_upt";

983 Addsimps [nth_upt];

985 Goal "!i. i+m <= n --> take m [i..n(] = [i..i+m(]";

986 by (induct_tac "m" 1);

987 by (Simp_tac 1);

988 by (Clarify_tac 1);

989 by (stac upt_rec 1);

990 by (rtac sym 1);

991 by (stac upt_rec 1);

992 by (asm_simp_tac (simpset() delsimps (thms"upt.simps")) 1);

993 qed_spec_mp "take_upt";

994 Addsimps [take_upt];

996 Goal "!m i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";

997 by (induct_tac "n" 1);

998 by (Simp_tac 1);

999 by (Clarify_tac 1);

1000 by (subgoal_tac "m < Suc n" 1);

1001 by (arith_tac 2);

1002 by (stac upt_rec 1);

1003 by (asm_simp_tac (simpset() delsplits [split_if]) 1);

1004 by (split_tac [split_if] 1);

1005 by (rtac conjI 1);

1006 by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);

1007 by (simp_tac (simpset() addsimps [nth_append] addsplits [nat.split]) 1);

1008 by (Clarify_tac 1);

1009 by (rtac conjI 1);

1010 by (Clarify_tac 1);

1011 by (subgoal_tac "Suc(m+nat) < n" 1);

1012 by (arith_tac 2);

1013 by (Asm_simp_tac 1);

1014 by (Clarify_tac 1);

1015 by (subgoal_tac "n = Suc(m+nat)" 1);

1016 by (arith_tac 2);

1017 by (Asm_simp_tac 1);

1018 by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);

1019 by (arith_tac 1);

1020 qed_spec_mp "nth_map_upt";

1022 Goal "ALL xs ys. k <= length xs --> k <= length ys --> \

1023 \ (ALL i. i < k --> xs!i = ys!i) \

1024 \ --> take k xs = take k ys";

1025 by (induct_tac "k" 1);

1026 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj,

1027 all_conj_distrib])));

1028 by (Clarify_tac 1);

1029 (*Both lists must be non-empty*)

1030 by (exhaust_tac "xs" 1);

1031 by (exhaust_tac "ys" 2);

1032 by (ALLGOALS Clarify_tac);

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

1034 by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])

1035 delsimps (all_simps))));

1036 by (Blast_tac 1);

1037 qed_spec_mp "nth_take_lemma";

1039 Goal "[| length xs = length ys; \

1040 \ ALL i. i < length xs --> xs!i = ys!i |] \

1041 \ ==> xs = ys";

1042 by (forward_tac [[le_refl, eq_imp_le] MRS nth_take_lemma] 1);

1043 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));

1044 qed_spec_mp "nth_equalityI";

1046 (*The famous take-lemma*)

1047 Goal "(ALL i. take i xs = take i ys) ==> xs = ys";

1048 by (dres_inst_tac [("x", "max (length xs) (length ys)")] spec 1);

1049 by (full_simp_tac (simpset() addsimps [le_max_iff_disj, take_all]) 1);

1050 qed_spec_mp "take_equalityI";

1053 (** nodups & remdups **)

1054 section "nodups & remdups";

1056 Goal "set(remdups xs) = set xs";

1057 by (induct_tac "xs" 1);

1058 by (Simp_tac 1);

1059 by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);

1060 qed "set_remdups";

1061 Addsimps [set_remdups];

1063 Goal "nodups(remdups xs)";

1064 by (induct_tac "xs" 1);

1065 by Auto_tac;

1066 qed "nodups_remdups";

1068 Goal "nodups xs --> nodups (filter P xs)";

1069 by (induct_tac "xs" 1);

1070 by Auto_tac;

1071 qed_spec_mp "nodups_filter";

1073 (** replicate **)

1074 section "replicate";

1076 Goal "length(replicate n x) = n";

1077 by (induct_tac "n" 1);

1078 by Auto_tac;

1079 qed "length_replicate";

1080 Addsimps [length_replicate];

1082 Goal "map f (replicate n x) = replicate n (f x)";

1083 by (induct_tac "n" 1);

1084 by Auto_tac;

1085 qed "map_replicate";

1086 Addsimps [map_replicate];

1088 Goal "(replicate n x) @ (x#xs) = x # replicate n x @ xs";

1089 by (induct_tac "n" 1);

1090 by Auto_tac;

1091 qed "replicate_app_Cons_same";

1093 Goal "rev(replicate n x) = replicate n x";

1094 by (induct_tac "n" 1);

1095 by (Simp_tac 1);

1096 by (asm_simp_tac (simpset() addsimps [replicate_app_Cons_same]) 1);

1097 qed "rev_replicate";

1098 Addsimps [rev_replicate];

1100 Goal"n ~= 0 --> hd(replicate n x) = x";

1101 by (induct_tac "n" 1);

1102 by Auto_tac;

1103 qed_spec_mp "hd_replicate";

1104 Addsimps [hd_replicate];

1106 Goal "n ~= 0 --> tl(replicate n x) = replicate (n-1) x";

1107 by (induct_tac "n" 1);

1108 by Auto_tac;

1109 qed_spec_mp "tl_replicate";

1110 Addsimps [tl_replicate];

1112 Goal "n ~= 0 --> last(replicate n x) = x";

1113 by (induct_tac "n" 1);

1114 by Auto_tac;

1115 qed_spec_mp "last_replicate";

1116 Addsimps [last_replicate];

1118 Goal "!i. i<n --> (replicate n x)!i = x";

1119 by (induct_tac "n" 1);

1120 by (Simp_tac 1);

1121 by (asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);

1122 qed_spec_mp "nth_replicate";

1123 Addsimps [nth_replicate];

1125 Goal "set(replicate (Suc n) x) = {x}";

1126 by (induct_tac "n" 1);

1127 by Auto_tac;

1128 val lemma = result();

1130 Goal "n ~= 0 ==> set(replicate n x) = {x}";

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

1132 qed "set_replicate";

1133 Addsimps [set_replicate];

1135 Goal "replicate (n+m) x = replicate n x @ replicate m x";

1136 by (induct_tac "n" 1);

1137 by Auto_tac;

1138 qed "replicate_add";

1140 (*** Lexcicographic orderings on lists ***)

1141 section"Lexcicographic orderings on lists";

1143 Goal "wf r ==> wf(lexn r n)";

1144 by (induct_tac "n" 1);

1145 by (Simp_tac 1);

1146 by (Simp_tac 1);

1147 by (rtac wf_subset 1);

1148 by (rtac Int_lower1 2);

1149 by (rtac wf_prod_fun_image 1);

1150 by (rtac injI 2);

1151 by Auto_tac;

1152 qed "wf_lexn";

1154 Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";

1155 by (induct_tac "n" 1);

1156 by Auto_tac;

1157 qed_spec_mp "lexn_length";

1159 Goalw [lex_def] "wf r ==> wf(lex r)";

1160 by (rtac wf_UN 1);

1161 by (blast_tac (claset() addIs [wf_lexn]) 1);

1162 by (Clarify_tac 1);

1163 by (rename_tac "m n" 1);

1164 by (subgoal_tac "m ~= n" 1);

1165 by (Blast_tac 2);

1166 by (blast_tac (claset() addDs [lexn_length,not_sym]) 1);

1167 qed "wf_lex";

1168 AddSIs [wf_lex];

1170 Goal

1171 "lexn r n = \

1172 \ {(xs,ys). length xs = n & length ys = n & \

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

1174 by (induct_tac "n" 1);

1175 by (Simp_tac 1);

1176 by (Blast_tac 1);

1177 by (asm_full_simp_tac (simpset()

1178 addsimps [lex_prod_def]) 1);

1179 by (auto_tac (claset(), simpset()));

1180 by (Blast_tac 1);

1181 by (rename_tac "a xys x xs' y ys'" 1);

1182 by (res_inst_tac [("x","a#xys")] exI 1);

1183 by (Simp_tac 1);

1184 by (exhaust_tac "xys" 1);

1185 by (ALLGOALS (asm_full_simp_tac (simpset())));

1186 by (Blast_tac 1);

1187 qed "lexn_conv";

1189 Goalw [lex_def]

1190 "lex r = \

1191 \ {(xs,ys). length xs = length ys & \

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

1193 by (force_tac (claset(), simpset() addsimps [lexn_conv]) 1);

1194 qed "lex_conv";

1196 Goalw [lexico_def] "wf r ==> wf(lexico r)";

1197 by (Blast_tac 1);

1198 qed "wf_lexico";

1199 AddSIs [wf_lexico];

1201 Goalw

1202 [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]

1203 "lexico r = {(xs,ys). length xs < length ys | \

1204 \ length xs = length ys & (xs,ys) : lex r}";

1205 by (Simp_tac 1);

1206 qed "lexico_conv";

1208 Goal "([],ys) ~: lex r";

1209 by (simp_tac (simpset() addsimps [lex_conv]) 1);

1210 qed "Nil_notin_lex";

1212 Goal "(xs,[]) ~: lex r";

1213 by (simp_tac (simpset() addsimps [lex_conv]) 1);

1214 qed "Nil2_notin_lex";

1216 AddIffs [Nil_notin_lex,Nil2_notin_lex];

1218 Goal "((x#xs,y#ys) : lex r) = \

1219 \ ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";

1220 by (simp_tac (simpset() addsimps [lex_conv]) 1);

1221 by (rtac iffI 1);

1222 by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);

1223 by (REPEAT(eresolve_tac [conjE, exE] 1));

1224 by (exhaust_tac "xys" 1);

1225 by (Asm_full_simp_tac 1);

1226 by (Asm_full_simp_tac 1);

1227 by (Blast_tac 1);

1228 qed "Cons_in_lex";

1229 AddIffs [Cons_in_lex];