src/HOL/List.ML
author nipkow
Thu Oct 30 09:45:03 1997 +0100 (1997-10-30)
changeset 4032 4b1c69d8b767
parent 3919 c036caebfc75
child 4069 d6d06a03a2e9
permissions -rw-r--r--
For each datatype `t' there is now a theorem `split_t_case' of the form

P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))&
...
(!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn)))


The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x
to (..t.. & ..t..) --> P t
(and similarly for t=x).
     1 (*  Title:      HOL/List
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 List lemmas
     7 *)
     8 
     9 open List;
    10 
    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];
    17 
    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";
    23 
    24 
    25 (** "lists": the list-forming operator over sets **)
    26 
    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";
    31 
    32 val listsE = lists.mk_cases list.simps  "x#l : lists A";
    33 AddSEs [listsE];
    34 AddSIs lists.intrs;
    35 
    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";
    40 
    41 goal thy "lists (A Int B) = lists A Int lists B";
    42 br (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];
    47 
    48 
    49 (** list_case **)
    50 
    51 val expand_list_case = split_list_case;
    52 
    53 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    54 by (induct_tac "xs" 1);
    55 by (REPEAT(resolve_tac prems 1));
    56 qed "list_cases";
    57 
    58 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    59 by (induct_tac "xs" 1);
    60 by (Blast_tac 1);
    61 by (Blast_tac 1);
    62 bind_thm("list_eq_cases",
    63   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    64 
    65 
    66 (** length **)
    67 (* needs to come before "@" because of thm append_eq_append_conv *)
    68 
    69 section "length";
    70 
    71 goal thy "length(xs@ys) = length(xs)+length(ys)";
    72 by (induct_tac "xs" 1);
    73 by (ALLGOALS Asm_simp_tac);
    74 qed"length_append";
    75 Addsimps [length_append];
    76 
    77 goal thy "length (map f l) = length l";
    78 by (induct_tac "l" 1);
    79 by (ALLGOALS Simp_tac);
    80 qed "length_map";
    81 Addsimps [length_map];
    82 
    83 goal thy "length(rev xs) = length(xs)";
    84 by (induct_tac "xs" 1);
    85 by (ALLGOALS Asm_simp_tac);
    86 qed "length_rev";
    87 Addsimps [length_rev];
    88 
    89 goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
    90 by(exhaust_tac "xs" 1);
    91 by(ALLGOALS Asm_full_simp_tac);
    92 qed "length_tl";
    93 Addsimps [length_tl];
    94 
    95 goal thy "(length xs = 0) = (xs = [])";
    96 by (induct_tac "xs" 1);
    97 by (ALLGOALS Asm_simp_tac);
    98 qed "length_0_conv";
    99 AddIffs [length_0_conv];
   100 
   101 goal thy "(0 = length xs) = (xs = [])";
   102 by (induct_tac "xs" 1);
   103 by (ALLGOALS Asm_simp_tac);
   104 qed "zero_length_conv";
   105 AddIffs [zero_length_conv];
   106 
   107 goal thy "(0 < length xs) = (xs ~= [])";
   108 by (induct_tac "xs" 1);
   109 by (ALLGOALS Asm_simp_tac);
   110 qed "length_greater_0_conv";
   111 AddIffs [length_greater_0_conv];
   112 
   113 (** @ - append **)
   114 
   115 section "@ - append";
   116 
   117 goal thy "(xs@ys)@zs = xs@(ys@zs)";
   118 by (induct_tac "xs" 1);
   119 by (ALLGOALS Asm_simp_tac);
   120 qed "append_assoc";
   121 Addsimps [append_assoc];
   122 
   123 goal thy "xs @ [] = xs";
   124 by (induct_tac "xs" 1);
   125 by (ALLGOALS Asm_simp_tac);
   126 qed "append_Nil2";
   127 Addsimps [append_Nil2];
   128 
   129 goal thy "(xs@ys = []) = (xs=[] & ys=[])";
   130 by (induct_tac "xs" 1);
   131 by (ALLGOALS Asm_simp_tac);
   132 qed "append_is_Nil_conv";
   133 AddIffs [append_is_Nil_conv];
   134 
   135 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
   136 by (induct_tac "xs" 1);
   137 by (ALLGOALS Asm_simp_tac);
   138 by (Blast_tac 1);
   139 qed "Nil_is_append_conv";
   140 AddIffs [Nil_is_append_conv];
   141 
   142 goal thy "(xs @ ys = xs) = (ys=[])";
   143 by (induct_tac "xs" 1);
   144 by (ALLGOALS Asm_simp_tac);
   145 qed "append_self_conv";
   146 
   147 goal thy "(xs = xs @ ys) = (ys=[])";
   148 by (induct_tac "xs" 1);
   149 by (ALLGOALS Asm_simp_tac);
   150 by (Blast_tac 1);
   151 qed "self_append_conv";
   152 AddIffs [append_self_conv,self_append_conv];
   153 
   154 goal thy "!ys. length xs = length ys | length us = length vs \
   155 \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
   156 by(induct_tac "xs" 1);
   157  by(rtac allI 1);
   158  by(exhaust_tac "ys" 1);
   159   by(Asm_simp_tac 1);
   160  by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
   161                       addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
   162 by(rtac allI 1);
   163 by(exhaust_tac "ys" 1);
   164  by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
   165                       addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
   166 by(Asm_simp_tac 1);
   167 qed_spec_mp "append_eq_append_conv";
   168 Addsimps [append_eq_append_conv];
   169 
   170 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
   171 by (Simp_tac 1);
   172 qed "same_append_eq";
   173 
   174 goal thy "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
   175 by (Simp_tac 1);
   176 qed "append1_eq_conv";
   177 
   178 goal thy "(ys @ xs = zs @ xs) = (ys=zs)";
   179 by (Simp_tac 1);
   180 qed "append_same_eq";
   181 
   182 AddSIs
   183  [same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];
   184 AddSDs
   185  [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
   186 
   187 goal thy "xs ~= [] --> hd xs # tl xs = xs";
   188 by (induct_tac "xs" 1);
   189 by (ALLGOALS Asm_simp_tac);
   190 qed_spec_mp "hd_Cons_tl";
   191 Addsimps [hd_Cons_tl];
   192 
   193 goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
   194 by (induct_tac "xs" 1);
   195 by (ALLGOALS Asm_simp_tac);
   196 qed "hd_append";
   197 
   198 goal thy "!!xs. xs ~= [] ==> hd(xs @ ys) = hd xs";
   199 by (asm_simp_tac (!simpset addsimps [hd_append]
   200                            addsplits [expand_list_case]) 1);
   201 qed "hd_append2";
   202 Addsimps [hd_append2];
   203 
   204 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
   205 by (simp_tac (!simpset addsplits [expand_list_case]) 1);
   206 qed "tl_append";
   207 
   208 goal thy "!!xs. xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys";
   209 by (asm_simp_tac (!simpset addsimps [tl_append]
   210                            addsplits [expand_list_case]) 1);
   211 qed "tl_append2";
   212 Addsimps [tl_append2];
   213 
   214 (** map **)
   215 
   216 section "map";
   217 
   218 goal thy
   219   "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
   220 by (induct_tac "xs" 1);
   221 by (ALLGOALS Asm_simp_tac);
   222 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   223 
   224 goal thy "map (%x. x) = (%xs. xs)";
   225 by (rtac ext 1);
   226 by (induct_tac "xs" 1);
   227 by (ALLGOALS Asm_simp_tac);
   228 qed "map_ident";
   229 Addsimps[map_ident];
   230 
   231 goal thy "map f (xs@ys) = map f xs @ map f ys";
   232 by (induct_tac "xs" 1);
   233 by (ALLGOALS Asm_simp_tac);
   234 qed "map_append";
   235 Addsimps[map_append];
   236 
   237 goalw thy [o_def] "map (f o g) xs = map f (map g xs)";
   238 by (induct_tac "xs" 1);
   239 by (ALLGOALS Asm_simp_tac);
   240 qed "map_compose";
   241 Addsimps[map_compose];
   242 
   243 goal thy "rev(map f xs) = map f (rev xs)";
   244 by (induct_tac "xs" 1);
   245 by (ALLGOALS Asm_simp_tac);
   246 qed "rev_map";
   247 
   248 (* a congruence rule for map: *)
   249 goal thy
   250  "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
   251 by(rtac impI 1);
   252 by(hyp_subst_tac 1);
   253 by(induct_tac "ys" 1);
   254 by(ALLGOALS Asm_simp_tac);
   255 val lemma = result();
   256 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
   257 
   258 goal List.thy "(map f xs = []) = (xs = [])";
   259 by(induct_tac "xs" 1);
   260 by(ALLGOALS Asm_simp_tac);
   261 qed "map_is_Nil_conv";
   262 AddIffs [map_is_Nil_conv];
   263 
   264 goal List.thy "([] = map f xs) = (xs = [])";
   265 by(induct_tac "xs" 1);
   266 by(ALLGOALS Asm_simp_tac);
   267 qed "Nil_is_map_conv";
   268 AddIffs [Nil_is_map_conv];
   269 
   270 
   271 (** rev **)
   272 
   273 section "rev";
   274 
   275 goal thy "rev(xs@ys) = rev(ys) @ rev(xs)";
   276 by (induct_tac "xs" 1);
   277 by (ALLGOALS Asm_simp_tac);
   278 qed "rev_append";
   279 Addsimps[rev_append];
   280 
   281 goal thy "rev(rev l) = l";
   282 by (induct_tac "l" 1);
   283 by (ALLGOALS Asm_simp_tac);
   284 qed "rev_rev_ident";
   285 Addsimps[rev_rev_ident];
   286 
   287 goal thy "(rev xs = []) = (xs = [])";
   288 by(induct_tac "xs" 1);
   289 by(ALLGOALS Asm_simp_tac);
   290 qed "rev_is_Nil_conv";
   291 AddIffs [rev_is_Nil_conv];
   292 
   293 goal thy "([] = rev xs) = (xs = [])";
   294 by(induct_tac "xs" 1);
   295 by(ALLGOALS Asm_simp_tac);
   296 qed "Nil_is_rev_conv";
   297 AddIffs [Nil_is_rev_conv];
   298 
   299 
   300 (** mem **)
   301 
   302 section "mem";
   303 
   304 goal thy "x mem (xs@ys) = (x mem xs | x mem ys)";
   305 by (induct_tac "xs" 1);
   306 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   307 qed "mem_append";
   308 Addsimps[mem_append];
   309 
   310 goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   311 by (induct_tac "xs" 1);
   312 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   313 qed "mem_filter";
   314 Addsimps[mem_filter];
   315 
   316 (** set **)
   317 
   318 section "set";
   319 
   320 goal thy "set (xs@ys) = (set xs Un set ys)";
   321 by (induct_tac "xs" 1);
   322 by (ALLGOALS Asm_simp_tac);
   323 qed "set_append";
   324 Addsimps[set_append];
   325 
   326 goal thy "(x mem xs) = (x: set xs)";
   327 by (induct_tac "xs" 1);
   328 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   329 by (Blast_tac 1);
   330 qed "set_mem_eq";
   331 
   332 goal thy "set l <= set (x#l)";
   333 by (Simp_tac 1);
   334 by (Blast_tac 1);
   335 qed "set_subset_Cons";
   336 
   337 goal thy "(set xs = {}) = (xs = [])";
   338 by (induct_tac "xs" 1);
   339 by (ALLGOALS Asm_simp_tac);
   340 qed "set_empty";
   341 Addsimps [set_empty];
   342 
   343 goal thy "set(rev xs) = set(xs)";
   344 by (induct_tac "xs" 1);
   345 by (ALLGOALS Asm_simp_tac);
   346 qed "set_rev";
   347 Addsimps [set_rev];
   348 
   349 goal thy "set(map f xs) = f``(set xs)";
   350 by (induct_tac "xs" 1);
   351 by (ALLGOALS Asm_simp_tac);
   352 qed "set_map";
   353 Addsimps [set_map];
   354 
   355 
   356 (** list_all **)
   357 
   358 section "list_all";
   359 
   360 goal thy "list_all (%x. True) xs = True";
   361 by (induct_tac "xs" 1);
   362 by (ALLGOALS Asm_simp_tac);
   363 qed "list_all_True";
   364 Addsimps [list_all_True];
   365 
   366 goal thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
   367 by (induct_tac "xs" 1);
   368 by (ALLGOALS Asm_simp_tac);
   369 qed "list_all_append";
   370 Addsimps [list_all_append];
   371 
   372 goal thy "list_all P xs = (!x. x mem xs --> P(x))";
   373 by (induct_tac "xs" 1);
   374 by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   375 by (Blast_tac 1);
   376 qed "list_all_mem_conv";
   377 
   378 
   379 (** filter **)
   380 
   381 section "filter";
   382 
   383 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
   384 by (induct_tac "xs" 1);
   385  by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   386 qed "filter_append";
   387 Addsimps [filter_append];
   388 
   389 goal thy "size (filter P xs) <= size xs";
   390 by (induct_tac "xs" 1);
   391  by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   392 qed "filter_size";
   393 
   394 
   395 (** concat **)
   396 
   397 section "concat";
   398 
   399 goal thy  "concat(xs@ys) = concat(xs)@concat(ys)";
   400 by (induct_tac "xs" 1);
   401 by (ALLGOALS Asm_simp_tac);
   402 qed"concat_append";
   403 Addsimps [concat_append];
   404 
   405 goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
   406 by(induct_tac "xss" 1);
   407 by(ALLGOALS Asm_simp_tac);
   408 qed "concat_eq_Nil_conv";
   409 AddIffs [concat_eq_Nil_conv];
   410 
   411 goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
   412 by(induct_tac "xss" 1);
   413 by(ALLGOALS Asm_simp_tac);
   414 qed "Nil_eq_concat_conv";
   415 AddIffs [Nil_eq_concat_conv];
   416 
   417 goal thy  "set(concat xs) = Union(set `` set xs)";
   418 by (induct_tac "xs" 1);
   419 by (ALLGOALS Asm_simp_tac);
   420 qed"set_concat";
   421 Addsimps [set_concat];
   422 
   423 goal thy "map f (concat xs) = concat (map (map f) xs)"; 
   424 by (induct_tac "xs" 1);
   425 by (ALLGOALS Asm_simp_tac);
   426 qed "map_concat";
   427 
   428 goal thy "filter p (concat xs) = concat (map (filter p) xs)"; 
   429 by (induct_tac "xs" 1);
   430 by (ALLGOALS Asm_simp_tac);
   431 qed"filter_concat"; 
   432 
   433 goal thy "rev(concat xs) = concat (map rev (rev xs))";
   434 by (induct_tac "xs" 1);
   435 by (ALLGOALS Asm_simp_tac);
   436 qed "rev_concat";
   437 
   438 (** nth **)
   439 
   440 section "nth";
   441 
   442 goal thy
   443   "!xs. nth n (xs@ys) = \
   444 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
   445 by (nat_ind_tac "n" 1);
   446  by (Asm_simp_tac 1);
   447  by (rtac allI 1);
   448  by (exhaust_tac "xs" 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 "nth_append";
   454 
   455 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
   456 by (induct_tac "xs" 1);
   457 (* case [] *)
   458 by (Asm_full_simp_tac 1);
   459 (* case x#xl *)
   460 by (rtac allI 1);
   461 by (nat_ind_tac "n" 1);
   462 by (ALLGOALS Asm_full_simp_tac);
   463 qed_spec_mp "nth_map";
   464 Addsimps [nth_map];
   465 
   466 goal thy "!n. n < length xs --> list_all P xs --> P(nth n xs)";
   467 by (induct_tac "xs" 1);
   468 (* case [] *)
   469 by (Simp_tac 1);
   470 (* case x#xl *)
   471 by (rtac allI 1);
   472 by (nat_ind_tac "n" 1);
   473 by (ALLGOALS Asm_full_simp_tac);
   474 qed_spec_mp "list_all_nth";
   475 
   476 goal thy "!n. n < length xs --> (nth n xs) mem xs";
   477 by (induct_tac "xs" 1);
   478 (* case [] *)
   479 by (Simp_tac 1);
   480 (* case x#xl *)
   481 by (rtac allI 1);
   482 by (nat_ind_tac "n" 1);
   483 (* case 0 *)
   484 by (Asm_full_simp_tac 1);
   485 (* case Suc x *)
   486 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   487 qed_spec_mp "nth_mem";
   488 Addsimps [nth_mem];
   489 
   490 (** last & butlast **)
   491 
   492 goal thy "last(xs@[x]) = x";
   493 by(induct_tac "xs" 1);
   494 by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   495 qed "last_snoc";
   496 Addsimps [last_snoc];
   497 
   498 goal thy "butlast(xs@[x]) = xs";
   499 by(induct_tac "xs" 1);
   500 by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   501 qed "butlast_snoc";
   502 Addsimps [butlast_snoc];
   503 
   504 goal thy
   505   "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   506 by(induct_tac "xs" 1);
   507 by(ALLGOALS(asm_simp_tac (!simpset addsplits [expand_if])));
   508 qed_spec_mp "butlast_append";
   509 
   510 goal thy "x:set(butlast xs) --> x:set xs";
   511 by(induct_tac "xs" 1);
   512 by(ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
   513 qed_spec_mp "in_set_butlastD";
   514 
   515 goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   516 by(asm_simp_tac (!simpset addsimps [butlast_append]
   517                           addsplits [expand_if]) 1);
   518 by(blast_tac (!claset addDs [in_set_butlastD]) 1);
   519 qed "in_set_butlast_appendI1";
   520 
   521 goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
   522 by(asm_simp_tac (!simpset addsimps [butlast_append]
   523                           addsplits [expand_if]) 1);
   524 by(Clarify_tac 1);
   525 by(Full_simp_tac 1);
   526 qed "in_set_butlast_appendI2";
   527 
   528 (** take  & drop **)
   529 section "take & drop";
   530 
   531 goal thy "take 0 xs = []";
   532 by (induct_tac "xs" 1);
   533 by (ALLGOALS Asm_simp_tac);
   534 qed "take_0";
   535 
   536 goal thy "drop 0 xs = xs";
   537 by (induct_tac "xs" 1);
   538 by (ALLGOALS Asm_simp_tac);
   539 qed "drop_0";
   540 
   541 goal thy "take (Suc n) (x#xs) = x # take n xs";
   542 by (Simp_tac 1);
   543 qed "take_Suc_Cons";
   544 
   545 goal thy "drop (Suc n) (x#xs) = drop n xs";
   546 by (Simp_tac 1);
   547 qed "drop_Suc_Cons";
   548 
   549 Delsimps [take_Cons,drop_Cons];
   550 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
   551 
   552 goal thy "!xs. length(take n xs) = min (length xs) n";
   553 by (nat_ind_tac "n" 1);
   554  by (ALLGOALS Asm_simp_tac);
   555 by (rtac allI 1);
   556 by (exhaust_tac "xs" 1);
   557  by (ALLGOALS Asm_simp_tac);
   558 qed_spec_mp "length_take";
   559 Addsimps [length_take];
   560 
   561 goal thy "!xs. length(drop n xs) = (length xs - n)";
   562 by (nat_ind_tac "n" 1);
   563  by (ALLGOALS Asm_simp_tac);
   564 by (rtac allI 1);
   565 by (exhaust_tac "xs" 1);
   566  by (ALLGOALS Asm_simp_tac);
   567 qed_spec_mp "length_drop";
   568 Addsimps [length_drop];
   569 
   570 goal thy "!xs. length xs <= n --> take n xs = xs";
   571 by (nat_ind_tac "n" 1);
   572  by (ALLGOALS Asm_simp_tac);
   573 by (rtac allI 1);
   574 by (exhaust_tac "xs" 1);
   575  by (ALLGOALS Asm_simp_tac);
   576 qed_spec_mp "take_all";
   577 
   578 goal thy "!xs. length xs <= n --> drop n xs = []";
   579 by (nat_ind_tac "n" 1);
   580  by (ALLGOALS Asm_simp_tac);
   581 by (rtac allI 1);
   582 by (exhaust_tac "xs" 1);
   583  by (ALLGOALS Asm_simp_tac);
   584 qed_spec_mp "drop_all";
   585 
   586 goal thy 
   587   "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   588 by (nat_ind_tac "n" 1);
   589  by (ALLGOALS Asm_simp_tac);
   590 by (rtac allI 1);
   591 by (exhaust_tac "xs" 1);
   592  by (ALLGOALS Asm_simp_tac);
   593 qed_spec_mp "take_append";
   594 Addsimps [take_append];
   595 
   596 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   597 by (nat_ind_tac "n" 1);
   598  by (ALLGOALS Asm_simp_tac);
   599 by (rtac allI 1);
   600 by (exhaust_tac "xs" 1);
   601  by (ALLGOALS Asm_simp_tac);
   602 qed_spec_mp "drop_append";
   603 Addsimps [drop_append];
   604 
   605 goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
   606 by (nat_ind_tac "m" 1);
   607  by (ALLGOALS Asm_simp_tac);
   608 by (rtac allI 1);
   609 by (exhaust_tac "xs" 1);
   610  by (ALLGOALS Asm_simp_tac);
   611 by (rtac allI 1);
   612 by (exhaust_tac "n" 1);
   613  by (ALLGOALS Asm_simp_tac);
   614 qed_spec_mp "take_take";
   615 
   616 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   617 by (nat_ind_tac "m" 1);
   618  by (ALLGOALS Asm_simp_tac);
   619 by (rtac allI 1);
   620 by (exhaust_tac "xs" 1);
   621  by (ALLGOALS Asm_simp_tac);
   622 qed_spec_mp "drop_drop";
   623 
   624 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   625 by (nat_ind_tac "m" 1);
   626  by (ALLGOALS Asm_simp_tac);
   627 by (rtac allI 1);
   628 by (exhaust_tac "xs" 1);
   629  by (ALLGOALS Asm_simp_tac);
   630 qed_spec_mp "take_drop";
   631 
   632 goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
   633 by (nat_ind_tac "n" 1);
   634 by (ALLGOALS Asm_simp_tac);
   635 by (rtac allI 1);
   636 by (exhaust_tac "xs" 1);
   637 by (ALLGOALS Asm_simp_tac);
   638 qed_spec_mp "take_map"; 
   639 
   640 goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
   641 by (nat_ind_tac "n" 1);
   642 by (ALLGOALS Asm_simp_tac);
   643 by (rtac allI 1);
   644 by (exhaust_tac "xs" 1);
   645 by (ALLGOALS Asm_simp_tac);
   646 qed_spec_mp "drop_map";
   647 
   648 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
   649 by (induct_tac "xs" 1);
   650  by (ALLGOALS Asm_simp_tac);
   651 by (Clarify_tac 1);
   652 by (exhaust_tac "n" 1);
   653  by (Blast_tac 1);
   654 by (exhaust_tac "i" 1);
   655 by (ALLGOALS Asm_full_simp_tac);
   656 qed_spec_mp "nth_take";
   657 Addsimps [nth_take];
   658 
   659 goal thy  "!xs i. n + i <= length xs --> nth i (drop n xs) = nth (n + i) xs";
   660 by (nat_ind_tac "n" 1);
   661  by (ALLGOALS Asm_simp_tac);
   662 by (rtac allI 1);
   663 by (exhaust_tac "xs" 1);
   664  by (ALLGOALS Asm_simp_tac);
   665 qed_spec_mp "nth_drop";
   666 Addsimps [nth_drop];
   667 
   668 (** takeWhile & dropWhile **)
   669 
   670 section "takeWhile & dropWhile";
   671 
   672 goal thy "takeWhile P xs @ dropWhile P xs = xs";
   673 by (induct_tac "xs" 1);
   674  by (Simp_tac 1);
   675 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   676 qed "takeWhile_dropWhile_id";
   677 Addsimps [takeWhile_dropWhile_id];
   678 
   679 goal thy  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   680 by (induct_tac "xs" 1);
   681  by (Simp_tac 1);
   682 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   683 by (Blast_tac 1);
   684 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   685 Addsimps [takeWhile_append1];
   686 
   687 goal thy
   688   "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   689 by (induct_tac "xs" 1);
   690  by (Simp_tac 1);
   691 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   692 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   693 Addsimps [takeWhile_append2];
   694 
   695 goal thy
   696   "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   697 by (induct_tac "xs" 1);
   698  by (Simp_tac 1);
   699 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   700 by (Blast_tac 1);
   701 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   702 Addsimps [dropWhile_append1];
   703 
   704 goal thy
   705   "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   706 by (induct_tac "xs" 1);
   707  by (Simp_tac 1);
   708 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   709 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   710 Addsimps [dropWhile_append2];
   711 
   712 goal thy "x:set(takeWhile P xs) --> x:set xs & P x";
   713 by (induct_tac "xs" 1);
   714  by (Simp_tac 1);
   715 by (asm_full_simp_tac (!simpset addsplits [expand_if]) 1);
   716 qed_spec_mp"set_take_whileD";
   717 
   718 (** replicate **)
   719 section "replicate";
   720 
   721 goal thy "set(replicate (Suc n) x) = {x}";
   722 by(induct_tac "n" 1);
   723 by(ALLGOALS Asm_full_simp_tac);
   724 val lemma = result();
   725 
   726 goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
   727 by(fast_tac (!claset addSDs [not0_implies_Suc] addSIs [lemma]) 1);
   728 qed "set_replicate";
   729 Addsimps [set_replicate];