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
     5 
     6 List lemmas
     7 *)
     8 
     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];
    14 
    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";
    20 
    21 
    22 (** List operator over sets **)
    23 
    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";
    28 
    29 
    30 (** list_case **)
    31 
    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";
    39 
    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";
    44 
    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))))));
    51 
    52 
    53 (** @ - append **)
    54 
    55 section "@ - append";
    56 
    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];
    62 
    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];
    68 
    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];
    74 
    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];
    81 
    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];
    87 
    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];
    98 
    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];
   104 
   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";
   109 
   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";
   113 
   114 (** map **)
   115 
   116 section "map";
   117 
   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)));
   123 
   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];
   130 
   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];
   136 
   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];
   142 
   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";
   147 
   148 (** rev **)
   149 
   150 section "rev";
   151 
   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];
   157 
   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];
   163 
   164 
   165 (** mem **)
   166 
   167 section "mem";
   168 
   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];
   174 
   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];
   180 
   181 (** set **)
   182 
   183 section "set";
   184 
   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];
   190 
   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";
   196 
   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";
   201 
   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];
   207 
   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];
   213 
   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];
   219 
   220 
   221 (** list_all **)
   222 
   223 section "list_all";
   224 
   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];
   230 
   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];
   236 
   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";
   242 
   243 
   244 (** filter **)
   245 
   246 section "filter";
   247 
   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];
   253 
   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";
   258 
   259 
   260 (** concat **)
   261 
   262 section "concat";
   263 
   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];
   269 
   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];
   275 
   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";
   280 
   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"; 
   285 
   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";
   290 
   291 (** length **)
   292 
   293 section "length";
   294 
   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];
   300 
   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];
   306 
   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];
   312 
   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];
   318 
   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];
   324 
   325 
   326 (** nth **)
   327 
   328 section "nth";
   329 
   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";
   342 
   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];
   353 
   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";
   363 
   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];
   377 
   378 
   379 (** take  & drop **)
   380 section "take & drop";
   381 
   382 goal thy "take 0 xs = []";
   383 by (induct_tac "xs" 1);
   384 by (ALLGOALS Asm_simp_tac);
   385 qed "take_0";
   386 
   387 goal thy "drop 0 xs = xs";
   388 by (induct_tac "xs" 1);
   389 by (ALLGOALS Asm_simp_tac);
   390 qed "drop_0";
   391 
   392 goal thy "take (Suc n) (x#xs) = x # take n xs";
   393 by (Simp_tac 1);
   394 qed "take_Suc_Cons";
   395 
   396 goal thy "drop (Suc n) (x#xs) = drop n xs";
   397 by (Simp_tac 1);
   398 qed "drop_Suc_Cons";
   399 
   400 Delsimps [take_Cons,drop_Cons];
   401 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
   402 
   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];
   411 
   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];
   420 
   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";
   428 
   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";
   436 
   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];
   446 
   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];
   455 
   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";
   466 
   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";
   474 
   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";
   482 
   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"; 
   490 
   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";
   498 
   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];
   509 
   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];
   518 
   519 (** takeWhile & dropWhile **)
   520 
   521 section "takeWhile & dropWhile";
   522 
   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];
   531 
   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];
   539 
   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];
   548 
   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];
   556 
   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";
   562