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

src/HOL/List.ML

author | nipkow |

Mon Mar 08 13:49:14 1999 +0100 (1999-03-08) | |

changeset 6306 | 81e7fbf61db2 |

parent 6162 | 484adda70b65 |

child 6394 | 3d9fd50fcc43 |

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

modified zip

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 "xs ~= [] ==> 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 read_cterm (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 (rtac impI 1);

338 by (hyp_subst_tac 1);

339 by (induct_tac "ys" 1);

340 by Auto_tac;

341 val lemma = result();

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

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

345 by (induct_tac "xs" 1);

346 by Auto_tac;

347 qed "map_is_Nil_conv";

348 AddIffs [map_is_Nil_conv];

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

351 by (induct_tac "xs" 1);

352 by Auto_tac;

353 qed "Nil_is_map_conv";

354 AddIffs [Nil_is_map_conv];

357 (** rev **)

359 section "rev";

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

362 by (induct_tac "xs" 1);

363 by Auto_tac;

364 qed "rev_append";

365 Addsimps[rev_append];

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

368 by (induct_tac "l" 1);

369 by Auto_tac;

370 qed "rev_rev_ident";

371 Addsimps[rev_rev_ident];

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

374 by (induct_tac "xs" 1);

375 by Auto_tac;

376 qed "rev_is_Nil_conv";

377 AddIffs [rev_is_Nil_conv];

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

380 by (induct_tac "xs" 1);

381 by Auto_tac;

382 qed "Nil_is_rev_conv";

383 AddIffs [Nil_is_rev_conv];

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

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

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

388 by (ALLGOALS Simp_tac);

389 by (resolve_tac prems 1);

390 by (eresolve_tac prems 1);

391 qed "rev_induct";

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

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

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

397 by Auto_tac;

398 bind_thm ("rev_exhaust",

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

402 (** set **)

404 section "set";

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

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

408 Addsimps[finite_set];

409 AddSIs[finite_set];

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

412 by (induct_tac "xs" 1);

413 by Auto_tac;

414 qed "set_append";

415 Addsimps[set_append];

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

418 by Auto_tac;

419 qed "set_subset_Cons";

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

422 by (induct_tac "xs" 1);

423 by Auto_tac;

424 qed "set_empty";

425 Addsimps [set_empty];

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

428 by (induct_tac "xs" 1);

429 by Auto_tac;

430 qed "set_rev";

431 Addsimps [set_rev];

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

434 by (induct_tac "xs" 1);

435 by Auto_tac;

436 qed "set_map";

437 Addsimps [set_map];

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

440 by (induct_tac "xs" 1);

441 by Auto_tac;

442 qed "in_set_filter";

443 Addsimps [in_set_filter];

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

446 by (induct_tac "xs" 1);

447 by (Simp_tac 1);

448 by (Asm_simp_tac 1);

449 by (rtac iffI 1);

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

451 by (REPEAT(etac exE 1));

452 by (exhaust_tac "ys" 1);

453 by Auto_tac;

454 qed "in_set_conv_decomp";

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

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

459 by (induct_tac "xs" 1);

460 by Auto_tac;

461 qed "in_lists_conv_set";

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

464 AddSDs [in_listsD];

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

466 AddSIs [in_listsI];

468 (** mem **)

470 section "mem";

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

473 by (induct_tac "xs" 1);

474 by Auto_tac;

475 qed "set_mem_eq";

478 (** list_all **)

480 section "list_all";

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

483 by (induct_tac "xs" 1);

484 by Auto_tac;

485 qed "list_all_conv";

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

488 by (induct_tac "xs" 1);

489 by Auto_tac;

490 qed "list_all_append";

491 Addsimps [list_all_append];

494 (** filter **)

496 section "filter";

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

499 by (induct_tac "xs" 1);

500 by Auto_tac;

501 qed "filter_append";

502 Addsimps [filter_append];

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

505 by (induct_tac "xs" 1);

506 by Auto_tac;

507 qed "filter_True";

508 Addsimps [filter_True];

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

511 by (induct_tac "xs" 1);

512 by Auto_tac;

513 qed "filter_False";

514 Addsimps [filter_False];

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

517 by (induct_tac "xs" 1);

518 by Auto_tac;

519 qed "length_filter";

520 Addsimps[length_filter];

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

523 by Auto_tac;

524 qed "filter_is_subset";

525 Addsimps [filter_is_subset];

528 section "concat";

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

531 by (induct_tac "xs" 1);

532 by Auto_tac;

533 qed"concat_append";

534 Addsimps [concat_append];

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

537 by (induct_tac "xss" 1);

538 by Auto_tac;

539 qed "concat_eq_Nil_conv";

540 AddIffs [concat_eq_Nil_conv];

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

543 by (induct_tac "xss" 1);

544 by Auto_tac;

545 qed "Nil_eq_concat_conv";

546 AddIffs [Nil_eq_concat_conv];

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

549 by (induct_tac "xs" 1);

550 by Auto_tac;

551 qed"set_concat";

552 Addsimps [set_concat];

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

555 by (induct_tac "xs" 1);

556 by Auto_tac;

557 qed "map_concat";

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

560 by (induct_tac "xs" 1);

561 by Auto_tac;

562 qed"filter_concat";

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

565 by (induct_tac "xs" 1);

566 by Auto_tac;

567 qed "rev_concat";

569 (** nth **)

571 section "nth";

573 Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";

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

575 qed "nth_Cons";

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

578 by (induct_tac "n" 1);

579 by (Asm_simp_tac 1);

580 by (rtac allI 1);

581 by (exhaust_tac "xs" 1);

582 by Auto_tac;

583 qed_spec_mp "nth_append";

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

586 by (induct_tac "xs" 1);

587 (* case [] *)

588 by (Asm_full_simp_tac 1);

589 (* case x#xl *)

590 by (rtac allI 1);

591 by (induct_tac "n" 1);

592 by Auto_tac;

593 qed_spec_mp "nth_map";

594 Addsimps [nth_map];

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

597 by (induct_tac "xs" 1);

598 (* case [] *)

599 by (Simp_tac 1);

600 (* case x#xl *)

601 by (rtac allI 1);

602 by (induct_tac "n" 1);

603 by Auto_tac;

604 qed_spec_mp "list_ball_nth";

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

607 by (induct_tac "xs" 1);

608 (* case [] *)

609 by (Simp_tac 1);

610 (* case x#xl *)

611 by (rtac allI 1);

612 by (induct_tac "n" 1);

613 (* case 0 *)

614 by (Asm_full_simp_tac 1);

615 (* case Suc x *)

616 by (Asm_full_simp_tac 1);

617 qed_spec_mp "nth_mem";

618 Addsimps [nth_mem];

621 (** list update **)

623 section "list update";

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

626 by (induct_tac "xs" 1);

627 by (Simp_tac 1);

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

629 qed_spec_mp "length_list_update";

630 Addsimps [length_list_update];

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

633 by (induct_tac "xs" 1);

634 by (Simp_tac 1);

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

636 qed_spec_mp "nth_list_update";

639 (** last & butlast **)

641 section "last / butlast";

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

644 by (induct_tac "xs" 1);

645 by Auto_tac;

646 qed "last_snoc";

647 Addsimps [last_snoc];

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

650 by (induct_tac "xs" 1);

651 by Auto_tac;

652 qed "butlast_snoc";

653 Addsimps [butlast_snoc];

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

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

657 by Auto_tac;

658 qed "length_butlast";

659 Addsimps [length_butlast];

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

662 by (induct_tac "xs" 1);

663 by Auto_tac;

664 qed_spec_mp "butlast_append";

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

667 by (induct_tac "xs" 1);

668 by Auto_tac;

669 qed_spec_mp "in_set_butlastD";

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

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

673 simpset() addsimps [butlast_append]));

674 qed "in_set_butlast_appendI";

676 (** take & drop **)

677 section "take & drop";

679 Goal "take 0 xs = []";

680 by (induct_tac "xs" 1);

681 by Auto_tac;

682 qed "take_0";

684 Goal "drop 0 xs = xs";

685 by (induct_tac "xs" 1);

686 by Auto_tac;

687 qed "drop_0";

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

690 by (Simp_tac 1);

691 qed "take_Suc_Cons";

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

694 by (Simp_tac 1);

695 qed "drop_Suc_Cons";

697 Delsimps [take_Cons,drop_Cons];

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

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

701 by (induct_tac "n" 1);

702 by Auto_tac;

703 by (exhaust_tac "xs" 1);

704 by Auto_tac;

705 qed_spec_mp "length_take";

706 Addsimps [length_take];

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

709 by (induct_tac "n" 1);

710 by Auto_tac;

711 by (exhaust_tac "xs" 1);

712 by Auto_tac;

713 qed_spec_mp "length_drop";

714 Addsimps [length_drop];

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

717 by (induct_tac "n" 1);

718 by Auto_tac;

719 by (exhaust_tac "xs" 1);

720 by Auto_tac;

721 qed_spec_mp "take_all";

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

724 by (induct_tac "n" 1);

725 by Auto_tac;

726 by (exhaust_tac "xs" 1);

727 by Auto_tac;

728 qed_spec_mp "drop_all";

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

731 by (induct_tac "n" 1);

732 by Auto_tac;

733 by (exhaust_tac "xs" 1);

734 by Auto_tac;

735 qed_spec_mp "take_append";

736 Addsimps [take_append];

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

739 by (induct_tac "n" 1);

740 by Auto_tac;

741 by (exhaust_tac "xs" 1);

742 by Auto_tac;

743 qed_spec_mp "drop_append";

744 Addsimps [drop_append];

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

747 by (induct_tac "m" 1);

748 by Auto_tac;

749 by (exhaust_tac "xs" 1);

750 by Auto_tac;

751 by (exhaust_tac "na" 1);

752 by Auto_tac;

753 qed_spec_mp "take_take";

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

756 by (induct_tac "m" 1);

757 by Auto_tac;

758 by (exhaust_tac "xs" 1);

759 by Auto_tac;

760 qed_spec_mp "drop_drop";

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

763 by (induct_tac "m" 1);

764 by Auto_tac;

765 by (exhaust_tac "xs" 1);

766 by Auto_tac;

767 qed_spec_mp "take_drop";

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

770 by (induct_tac "n" 1);

771 by Auto_tac;

772 by (exhaust_tac "xs" 1);

773 by Auto_tac;

774 qed_spec_mp "take_map";

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

777 by (induct_tac "n" 1);

778 by Auto_tac;

779 by (exhaust_tac "xs" 1);

780 by Auto_tac;

781 qed_spec_mp "drop_map";

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

784 by (induct_tac "xs" 1);

785 by Auto_tac;

786 by (exhaust_tac "n" 1);

787 by (Blast_tac 1);

788 by (exhaust_tac "i" 1);

789 by Auto_tac;

790 qed_spec_mp "nth_take";

791 Addsimps [nth_take];

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

794 by (induct_tac "n" 1);

795 by Auto_tac;

796 by (exhaust_tac "xs" 1);

797 by Auto_tac;

798 qed_spec_mp "nth_drop";

799 Addsimps [nth_drop];

801 (** takeWhile & dropWhile **)

803 section "takeWhile & dropWhile";

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

806 by (induct_tac "xs" 1);

807 by Auto_tac;

808 qed "takeWhile_dropWhile_id";

809 Addsimps [takeWhile_dropWhile_id];

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

812 by (induct_tac "xs" 1);

813 by Auto_tac;

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

815 Addsimps [takeWhile_append1];

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

818 by (induct_tac "xs" 1);

819 by Auto_tac;

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

821 Addsimps [takeWhile_append2];

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

824 by (induct_tac "xs" 1);

825 by Auto_tac;

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

827 Addsimps [dropWhile_append1];

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

830 by (induct_tac "xs" 1);

831 by Auto_tac;

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

833 Addsimps [dropWhile_append2];

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

836 by (induct_tac "xs" 1);

837 by Auto_tac;

838 qed_spec_mp"set_take_whileD";

840 (** zip **)

841 section "zip";

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

844 by(induct_tac "ys" 1);

845 by Auto_tac;

846 qed "zip_Nil";

847 Addsimps [zip_Nil];

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

850 by(Simp_tac 1);

851 qed "zip_Cons_Cons";

852 Addsimps [zip_Cons_Cons];

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

857 (** foldl **)

858 section "foldl";

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

861 by (induct_tac "xs" 1);

862 by Auto_tac;

863 qed_spec_mp "foldl_append";

864 Addsimps [foldl_append];

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

867 because it requires an additional transitivity step

868 *)

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

870 by (induct_tac "ns" 1);

871 by Auto_tac;

872 qed_spec_mp "start_le_sum";

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

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

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

877 qed "elem_le_sum";

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

880 by (induct_tac "ns" 1);

881 by Auto_tac;

882 qed_spec_mp "sum_eq_0_conv";

883 AddIffs [sum_eq_0_conv];

885 (** upto **)

887 (* Does not terminate! *)

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

889 by (induct_tac "j" 1);

890 by Auto_tac;

891 qed "upt_rec";

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

894 by (stac upt_rec 1);

895 by (Asm_simp_tac 1);

896 qed "upt_conv_Nil";

897 Addsimps [upt_conv_Nil];

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

900 by (Asm_simp_tac 1);

901 qed "upt_Suc";

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

904 by (rtac trans 1);

905 by (stac upt_rec 1);

906 by (rtac refl 2);

907 by (Asm_simp_tac 1);

908 qed "upt_conv_Cons";

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

911 by (induct_tac "j" 1);

912 by (Simp_tac 1);

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

914 qed "length_upt";

915 Addsimps [length_upt];

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

918 by (induct_tac "j" 1);

919 by (Simp_tac 1);

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

921 by (Clarify_tac 1);

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

923 by (Asm_simp_tac 2);

924 by (Asm_simp_tac 1);

925 qed_spec_mp "nth_upt";

926 Addsimps [nth_upt];

929 (** nodups & remdups **)

930 section "nodups & remdups";

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

933 by (induct_tac "xs" 1);

934 by (Simp_tac 1);

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

936 qed "set_remdups";

937 Addsimps [set_remdups];

939 Goal "nodups(remdups xs)";

940 by (induct_tac "xs" 1);

941 by Auto_tac;

942 qed "nodups_remdups";

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

945 by (induct_tac "xs" 1);

946 by Auto_tac;

947 qed_spec_mp "nodups_filter";

949 (** replicate **)

950 section "replicate";

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

953 by (induct_tac "n" 1);

954 by Auto_tac;

955 val lemma = result();

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

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

959 qed "set_replicate";

960 Addsimps [set_replicate];

963 (*** Lexcicographic orderings on lists ***)

964 section"Lexcicographic orderings on lists";

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

967 by (induct_tac "n" 1);

968 by (Simp_tac 1);

969 by (Simp_tac 1);

970 by (rtac wf_subset 1);

971 by (rtac Int_lower1 2);

972 by (rtac wf_prod_fun_image 1);

973 by (rtac injI 2);

974 by (Auto_tac);

975 qed "wf_lexn";

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

978 by (induct_tac "n" 1);

979 by (Auto_tac);

980 qed_spec_mp "lexn_length";

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

983 by (rtac wf_UN 1);

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

985 by (Clarify_tac 1);

986 by (rename_tac "m n" 1);

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

988 by (Blast_tac 2);

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

990 qed "wf_lex";

991 AddSIs [wf_lex];

993 Goal

994 "lexn r n = \

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

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

997 by (induct_tac "n" 1);

998 by (Simp_tac 1);

999 by (Blast_tac 1);

1000 by (asm_full_simp_tac (simpset()

1001 addsimps [lex_prod_def]) 1);

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

1003 by (Blast_tac 1);

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

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

1006 by (Simp_tac 1);

1007 by (exhaust_tac "xys" 1);

1008 by (ALLGOALS (asm_full_simp_tac (simpset())));

1009 by (Blast_tac 1);

1010 qed "lexn_conv";

1012 Goalw [lex_def]

1013 "lex r = \

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

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

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

1017 qed "lex_conv";

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

1020 by (Blast_tac 1);

1021 qed "wf_lexico";

1022 AddSIs [wf_lexico];

1024 Goalw

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

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

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

1028 by (Simp_tac 1);

1029 qed "lexico_conv";

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

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

1033 qed "Nil_notin_lex";

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

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

1037 qed "Nil2_notin_lex";

1039 AddIffs [Nil_notin_lex,Nil2_notin_lex];

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

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

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

1044 by (rtac iffI 1);

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

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

1047 by (exhaust_tac "xys" 1);

1048 by (Asm_full_simp_tac 1);

1049 by (Asm_full_simp_tac 1);

1050 by (Blast_tac 1);

1051 qed "Cons_in_lex";

1052 AddIffs [Cons_in_lex];