Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.ML
changeset 3457 a8ab7c64817c
parent 3383 7707cb7a5054
child 3465 e85c24717cad
equal deleted inserted replaced
3456:fdb1768ebd3e 3457:a8ab7c64817c 
    36 by (ALLGOALS Asm_simp_tac);
 
    36 by (ALLGOALS Asm_simp_tac);
 
    37 by (Blast_tac 1);
 
    37 by (Blast_tac 1);
 
    38 qed "expand_list_case";
 
    38 qed "expand_list_case";
 
    39 
    39 
    40 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
 
    40 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
 
    41 by(induct_tac "xs" 1);
 
    41 by (induct_tac "xs" 1);
 
    42 by(REPEAT(resolve_tac prems 1));
 
    42 by (REPEAT(resolve_tac prems 1));
 
    43 qed "list_cases";
 
    43 qed "list_cases";
 
    44 
    44 
    45 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
 
    45 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
 
    46 by (induct_tac "xs" 1);
 
    46 by (induct_tac "xs" 1);
 
    47 by (Blast_tac 1);
 
    47 by (Blast_tac 1);
 
    71 AddIffs [append_is_Nil_conv];
 
    71 AddIffs [append_is_Nil_conv];
 
    72 
    72 
    73 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
 
    73 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
 
    74 by (induct_tac "xs" 1);
 
    74 by (induct_tac "xs" 1);
 
    75 by (ALLGOALS Asm_simp_tac);
 
    75 by (ALLGOALS Asm_simp_tac);
 
    76 by(Blast_tac 1);
 
    76 by (Blast_tac 1);
 
    77 qed "Nil_is_append_conv";
 
    77 qed "Nil_is_append_conv";
 
    78 AddIffs [Nil_is_append_conv];
 
    78 AddIffs [Nil_is_append_conv];
 
    79 
    79 
    80 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
 
    80 goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
 
    81 by (induct_tac "xs" 1);
 
    81 by (induct_tac "xs" 1);
 
    82 by (ALLGOALS Asm_simp_tac);
 
    82 by (ALLGOALS Asm_simp_tac);
 
    83 qed "same_append_eq";
 
    83 qed "same_append_eq";
 
    84 AddIffs [same_append_eq];
 
    84 AddIffs [same_append_eq];
 
    85 
    85 
    86 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    86 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    87 by(induct_tac "xs" 1);
 
    87 by (induct_tac "xs" 1);
 
    88  br allI 1;
 
    88  by (rtac allI 1);
 
    89  by(induct_tac "ys" 1);
 
    89  by (induct_tac "ys" 1);
 
    90   by(ALLGOALS Asm_simp_tac);
 
    90   by (ALLGOALS Asm_simp_tac);
 
    91 br allI 1;
 
    91 by (rtac allI 1);
 
    92 by(induct_tac "ys" 1);
 
    92 by (induct_tac "ys" 1);
 
    93  by(ALLGOALS Asm_simp_tac);
 
    93  by (ALLGOALS Asm_simp_tac);
 
    94 qed_spec_mp "append1_eq_conv";
 
    94 qed_spec_mp "append1_eq_conv";
 
    95 AddIffs [append1_eq_conv];
 
    95 AddIffs [append1_eq_conv];
 
    96 
    96 
    97 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 
    97 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 
    98 by(induct_tac "xs" 1);
 
    98 by (induct_tac "xs" 1);
 
    99 by(ALLGOALS Asm_simp_tac);
 
    99 by (ALLGOALS Asm_simp_tac);
 
   100 qed_spec_mp "hd_Cons_tl";
 
   100 qed_spec_mp "hd_Cons_tl";
 
   101 Addsimps [hd_Cons_tl];
 
   101 Addsimps [hd_Cons_tl];
 
   102 
   102 
   103 goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
 
   103 goal thy "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
 
   104 by (induct_tac "xs" 1);
 
   104 by (induct_tac "xs" 1);
 
   105 by (ALLGOALS Asm_simp_tac);
 
   105 by (ALLGOALS Asm_simp_tac);
 
   106 qed "hd_append";
 
   106 qed "hd_append";
 
   107 
   107 
   108 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
 
   108 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
 
   109 by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
 
   109 by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
 
   110 qed "tl_append";
 
   110 qed "tl_append";
 
   111 
   111 
   112 (** map **)
 
   112 (** map **)
 
   113 
   113 
   114 goal thy
 
   114 goal thy
 
   115   "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
 
   115   "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
 
   116 by(induct_tac "xs" 1);
 
   116 by (induct_tac "xs" 1);
 
   117 by(ALLGOALS Asm_simp_tac);
 
   117 by (ALLGOALS Asm_simp_tac);
 
   118 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
   118 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
   119 
   119 
   120 goal thy "map (%x.x) = (%xs.xs)";
 
   120 goal thy "map (%x.x) = (%xs.xs)";
 
   121 by (rtac ext 1);
 
   121 by (rtac ext 1);
 
   122 by (induct_tac "xs" 1);
 
   122 by (induct_tac "xs" 1);
 
   188 by (Simp_tac 1);
 
   188 by (Simp_tac 1);
 
   189 by (Blast_tac 1);
 
   189 by (Blast_tac 1);
 
   190 qed "set_of_list_subset_Cons";
 
   190 qed "set_of_list_subset_Cons";
 
   191 
   191 
   192 goal thy "(set_of_list xs = {}) = (xs = [])";
 
   192 goal thy "(set_of_list xs = {}) = (xs = [])";
 
   193 by(induct_tac "xs" 1);
 
   193 by (induct_tac "xs" 1);
 
   194 by(ALLGOALS Asm_simp_tac);
 
   194 by (ALLGOALS Asm_simp_tac);
 
   195 qed "set_of_list_empty";
 
   195 qed "set_of_list_empty";
 
   196 Addsimps [set_of_list_empty];
 
   196 Addsimps [set_of_list_empty];
 
   197 
   197 
   198 goal thy "set_of_list(rev xs) = set_of_list(xs)";
 
   198 goal thy "set_of_list(rev xs) = set_of_list(xs)";
 
   199 by(induct_tac "xs" 1);
 
   199 by (induct_tac "xs" 1);
 
   200 by(ALLGOALS Asm_simp_tac);
 
   200 by (ALLGOALS Asm_simp_tac);
 
   201 qed "set_of_list_rev";
 
   201 qed "set_of_list_rev";
 
   202 Addsimps [set_of_list_rev];
 
   202 Addsimps [set_of_list_rev];
 
   203 
   203 
   204 goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
 
   204 goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
 
   205 by(induct_tac "xs" 1);
 
   205 by (induct_tac "xs" 1);
 
   206 by(ALLGOALS Asm_simp_tac);
 
   206 by (ALLGOALS Asm_simp_tac);
 
   207 qed "set_of_list_map";
 
   207 qed "set_of_list_map";
 
   208 Addsimps [set_of_list_map];
 
   208 Addsimps [set_of_list_map];
 
   209 
   209 
   210 
   210 
   211 (** list_all **)
 
   211 (** list_all **)
 
   230 
   230 
   231 
   231 
   232 (** filter **)
 
   232 (** filter **)
 
   233 
   233 
   234 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
 
   234 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
 
   235 by(induct_tac "xs" 1);
 
   235 by (induct_tac "xs" 1);
 
   236  by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 
   236  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 
   237 qed "filter_append";
 
   237 qed "filter_append";
 
   238 Addsimps [filter_append];
 
   238 Addsimps [filter_append];
 
   239 
   239 
   240 goal thy "size (filter P xs) <= size xs";
 
   240 goal thy "size (filter P xs) <= size xs";
 
   241 by(induct_tac "xs" 1);
 
   241 by (induct_tac "xs" 1);
 
   242  by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 
   242  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 
   243 qed "filter_size";
 
   243 qed "filter_size";
 
   244 
   244 
   245 
   245 
   246 (** concat **)
 
   246 (** concat **)
 
   247 
   247 
   275 by (ALLGOALS Asm_simp_tac);
 
   275 by (ALLGOALS Asm_simp_tac);
 
   276 qed "length_rev";
 
   276 qed "length_rev";
 
   277 Addsimps [length_rev];
 
   277 Addsimps [length_rev];
 
   278 
   278 
   279 goal thy "(length xs = 0) = (xs = [])";
 
   279 goal thy "(length xs = 0) = (xs = [])";
 
   280 by(induct_tac "xs" 1);
 
   280 by (induct_tac "xs" 1);
 
   281 by(ALLGOALS Asm_simp_tac);
 
   281 by (ALLGOALS Asm_simp_tac);
 
   282 qed "length_0_conv";
 
   282 qed "length_0_conv";
 
   283 AddIffs [length_0_conv];
 
   283 AddIffs [length_0_conv];
 
   284 
   284 
   285 goal thy "(0 < length xs) = (xs ~= [])";
 
   285 goal thy "(0 < length xs) = (xs ~= [])";
 
   286 by(induct_tac "xs" 1);
 
   286 by (induct_tac "xs" 1);
 
   287 by(ALLGOALS Asm_simp_tac);
 
   287 by (ALLGOALS Asm_simp_tac);
 
   288 qed "length_greater_0_conv";
 
   288 qed "length_greater_0_conv";
 
   289 AddIffs [length_greater_0_conv];
 
   289 AddIffs [length_greater_0_conv];
 
   290 
   290 
   291 
   291 
   292 (** nth **)
 
   292 (** nth **)
 
   293 
   293 
   294 goal thy
 
   294 goal thy
 
   295   "!xs. nth n (xs@ys) = \
 
   295   "!xs. nth n (xs@ys) = \
 
   296 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
 
   296 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
 
   297 by(nat_ind_tac "n" 1);
 
   297 by (nat_ind_tac "n" 1);
 
   298  by(Asm_simp_tac 1);
 
   298  by (Asm_simp_tac 1);
 
   299  br allI 1;
 
   299  by (rtac allI 1);
 
   300  by(exhaust_tac "xs" 1);
 
   300  by (exhaust_tac "xs" 1);
 
   301   by(ALLGOALS Asm_simp_tac);
 
   301   by (ALLGOALS Asm_simp_tac);
 
   302 br allI 1;
 
   302 by (rtac allI 1);
 
   303 by(exhaust_tac "xs" 1);
 
   303 by (exhaust_tac "xs" 1);
 
   304  by(ALLGOALS Asm_simp_tac);
 
   304  by (ALLGOALS Asm_simp_tac);
 
   305 qed_spec_mp "nth_append";
 
   305 qed_spec_mp "nth_append";
 
   306 
   306 
   307 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
 
   307 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
 
   308 by (induct_tac "xs" 1);
 
   308 by (induct_tac "xs" 1);
 
   309 (* case [] *)
 
   309 (* case [] *)
 
   363 
   363 
   364 Delsimps [take_Cons,drop_Cons];
 
   364 Delsimps [take_Cons,drop_Cons];
 
   365 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
 
   365 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
 
   366 
   366 
   367 goal thy "!xs. length(take n xs) = min (length xs) n";
 
   367 goal thy "!xs. length(take n xs) = min (length xs) n";
 
   368 by(nat_ind_tac "n" 1);
 
   368 by (nat_ind_tac "n" 1);
 
   369  by(ALLGOALS Asm_simp_tac);
 
   369  by (ALLGOALS Asm_simp_tac);
 
   370 br allI 1;
 
   370 by (rtac allI 1);
 
   371 by(exhaust_tac "xs" 1);
 
   371 by (exhaust_tac "xs" 1);
 
   372  by(ALLGOALS Asm_simp_tac);
 
   372  by (ALLGOALS Asm_simp_tac);
 
   373 qed_spec_mp "length_take";
 
   373 qed_spec_mp "length_take";
 
   374 Addsimps [length_take];
 
   374 Addsimps [length_take];
 
   375 
   375 
   376 goal thy "!xs. length(drop n xs) = (length xs - n)";
 
   376 goal thy "!xs. length(drop n xs) = (length xs - n)";
 
   377 by(nat_ind_tac "n" 1);
 
   377 by (nat_ind_tac "n" 1);
 
   378  by(ALLGOALS Asm_simp_tac);
 
   378  by (ALLGOALS Asm_simp_tac);
 
   379 br allI 1;
 
   379 by (rtac allI 1);
 
   380 by(exhaust_tac "xs" 1);
 
   380 by (exhaust_tac "xs" 1);
 
   381  by(ALLGOALS Asm_simp_tac);
 
   381  by (ALLGOALS Asm_simp_tac);
 
   382 qed_spec_mp "length_drop";
 
   382 qed_spec_mp "length_drop";
 
   383 Addsimps [length_drop];
 
   383 Addsimps [length_drop];
 
   384 
   384 
   385 goal thy "!xs. length xs <= n --> take n xs = xs";
 
   385 goal thy "!xs. length xs <= n --> take n xs = xs";
 
   386 by(nat_ind_tac "n" 1);
 
   386 by (nat_ind_tac "n" 1);
 
   387  by(ALLGOALS Asm_simp_tac);
 
   387  by (ALLGOALS Asm_simp_tac);
 
   388 br allI 1;
 
   388 by (rtac allI 1);
 
   389 by(exhaust_tac "xs" 1);
 
   389 by (exhaust_tac "xs" 1);
 
   390  by(ALLGOALS Asm_simp_tac);
 
   390  by (ALLGOALS Asm_simp_tac);
 
   391 qed_spec_mp "take_all";
 
   391 qed_spec_mp "take_all";
 
   392 
   392 
   393 goal thy "!xs. length xs <= n --> drop n xs = []";
 
   393 goal thy "!xs. length xs <= n --> drop n xs = []";
 
   394 by(nat_ind_tac "n" 1);
 
   394 by (nat_ind_tac "n" 1);
 
   395  by(ALLGOALS Asm_simp_tac);
 
   395  by (ALLGOALS Asm_simp_tac);
 
   396 br allI 1;
 
   396 by (rtac allI 1);
 
   397 by(exhaust_tac "xs" 1);
 
   397 by (exhaust_tac "xs" 1);
 
   398  by(ALLGOALS Asm_simp_tac);
 
   398  by (ALLGOALS Asm_simp_tac);
 
   399 qed_spec_mp "drop_all";
 
   399 qed_spec_mp "drop_all";
 
   400 
   400 
   401 goal thy 
   401 goal thy 
   402   "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 
   402   "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 
   403 by(nat_ind_tac "n" 1);
 
   403 by (nat_ind_tac "n" 1);
 
   404  by(ALLGOALS Asm_simp_tac);
 
   404  by (ALLGOALS Asm_simp_tac);
 
   405 br allI 1;
 
   405 by (rtac allI 1);
 
   406 by(exhaust_tac "xs" 1);
 
   406 by (exhaust_tac "xs" 1);
 
   407  by(ALLGOALS Asm_simp_tac);
 
   407  by (ALLGOALS Asm_simp_tac);
 
   408 qed_spec_mp "take_append";
 
   408 qed_spec_mp "take_append";
 
   409 Addsimps [take_append];
 
   409 Addsimps [take_append];
 
   410 
   410 
   411 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   411 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   412 by(nat_ind_tac "n" 1);
 
   412 by (nat_ind_tac "n" 1);
 
   413  by(ALLGOALS Asm_simp_tac);
 
   413  by (ALLGOALS Asm_simp_tac);
 
   414 br allI 1;
 
   414 by (rtac allI 1);
 
   415 by(exhaust_tac "xs" 1);
 
   415 by (exhaust_tac "xs" 1);
 
   416  by(ALLGOALS Asm_simp_tac);
 
   416  by (ALLGOALS Asm_simp_tac);
 
   417 qed_spec_mp "drop_append";
 
   417 qed_spec_mp "drop_append";
 
   418 Addsimps [drop_append];
 
   418 Addsimps [drop_append];
 
   419 
   419 
   420 goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
   420 goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
   421 by(nat_ind_tac "m" 1);
 
   421 by (nat_ind_tac "m" 1);
 
   422  by(ALLGOALS Asm_simp_tac);
 
   422  by (ALLGOALS Asm_simp_tac);
 
   423 br allI 1;
 
   423 by (rtac allI 1);
 
   424 by(exhaust_tac "xs" 1);
 
   424 by (exhaust_tac "xs" 1);
 
   425  by(ALLGOALS Asm_simp_tac);
 
   425  by (ALLGOALS Asm_simp_tac);
 
   426 br allI 1;
 
   426 by (rtac allI 1);
 
   427 by(exhaust_tac "n" 1);
 
   427 by (exhaust_tac "n" 1);
 
   428  by(ALLGOALS Asm_simp_tac);
 
   428  by (ALLGOALS Asm_simp_tac);
 
   429 qed_spec_mp "take_take";
 
   429 qed_spec_mp "take_take";
 
   430 
   430 
   431 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   431 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   432 by(nat_ind_tac "m" 1);
 
   432 by (nat_ind_tac "m" 1);
 
   433  by(ALLGOALS Asm_simp_tac);
 
   433  by (ALLGOALS Asm_simp_tac);
 
   434 br allI 1;
 
   434 by (rtac allI 1);
 
   435 by(exhaust_tac "xs" 1);
 
   435 by (exhaust_tac "xs" 1);
 
   436  by(ALLGOALS Asm_simp_tac);
 
   436  by (ALLGOALS Asm_simp_tac);
 
   437 qed_spec_mp "drop_drop";
 
   437 qed_spec_mp "drop_drop";
 
   438 
   438 
   439 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   439 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   440 by(nat_ind_tac "m" 1);
 
   440 by (nat_ind_tac "m" 1);
 
   441  by(ALLGOALS Asm_simp_tac);
 
   441  by (ALLGOALS Asm_simp_tac);
 
   442 br allI 1;
 
   442 by (rtac allI 1);
 
   443 by(exhaust_tac "xs" 1);
 
   443 by (exhaust_tac "xs" 1);
 
   444  by(ALLGOALS Asm_simp_tac);
 
   444  by (ALLGOALS Asm_simp_tac);
 
   445 qed_spec_mp "take_drop";
 
   445 qed_spec_mp "take_drop";
 
   446 
   446 
   447 goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
   447 goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
   448 by(nat_ind_tac "n" 1);
 
   448 by (nat_ind_tac "n" 1);
 
   449 by(ALLGOALS Asm_simp_tac);
 
   449 by (ALLGOALS Asm_simp_tac);
 
   450 br allI 1;
 
   450 by (rtac allI 1);
 
   451 by(exhaust_tac "xs" 1);
 
   451 by (exhaust_tac "xs" 1);
 
   452 by(ALLGOALS Asm_simp_tac);
 
   452 by (ALLGOALS Asm_simp_tac);
 
   453 qed_spec_mp "take_map"; 
   453 qed_spec_mp "take_map"; 
   454 
   454 
   455 goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
   455 goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
   456 by(nat_ind_tac "n" 1);
 
   456 by (nat_ind_tac "n" 1);
 
   457 by(ALLGOALS Asm_simp_tac);
 
   457 by (ALLGOALS Asm_simp_tac);
 
   458 br allI 1;
 
   458 by (rtac allI 1);
 
   459 by(exhaust_tac "xs" 1);
 
   459 by (exhaust_tac "xs" 1);
 
   460 by(ALLGOALS Asm_simp_tac);
 
   460 by (ALLGOALS Asm_simp_tac);
 
   461 qed_spec_mp "drop_map";
 
   461 qed_spec_mp "drop_map";
 
   462 
   462 
   463 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
 
   463 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
 
   464 by(induct_tac "xs" 1);
 
   464 by (induct_tac "xs" 1);
 
   465  by(ALLGOALS Asm_simp_tac);
 
   465  by (ALLGOALS Asm_simp_tac);
 
   466 by(strip_tac 1);
 
   466 by (strip_tac 1);
 
   467 by(exhaust_tac "n" 1);
 
   467 by (exhaust_tac "n" 1);
 
   468  by(Blast_tac 1);
 
   468  by (Blast_tac 1);
 
   469 by(exhaust_tac "i" 1);
 
   469 by (exhaust_tac "i" 1);
 
   470 by(ALLGOALS Asm_full_simp_tac);
 
   470 by (ALLGOALS Asm_full_simp_tac);
 
   471 qed_spec_mp "nth_take";
 
   471 qed_spec_mp "nth_take";
 
   472 Addsimps [nth_take];
 
   472 Addsimps [nth_take];
 
   473 
   473 
   474 goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
 
   474 goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
 
   475 by(nat_ind_tac "n" 1);
 
   475 by (nat_ind_tac "n" 1);
 
   476  by(ALLGOALS Asm_simp_tac);
 
   476  by (ALLGOALS Asm_simp_tac);
 
   477 br allI 1;
 
   477 by (rtac allI 1);
 
   478 by(exhaust_tac "xs" 1);
 
   478 by (exhaust_tac "xs" 1);
 
   479  by(ALLGOALS Asm_simp_tac);
 
   479  by (ALLGOALS Asm_simp_tac);
 
   480 qed_spec_mp "nth_drop";
 
   480 qed_spec_mp "nth_drop";
 
   481 Addsimps [nth_drop];
 
   481 Addsimps [nth_drop];
 
   482 
   482 
   483 (** takeWhile & dropWhile **)
 
   483 (** takeWhile & dropWhile **)
 
   484 
   484 
   485 goal thy
 
   485 goal thy
 
   486   "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 
   486   "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
 
   487 by(induct_tac "xs" 1);
 
   487 by (induct_tac "xs" 1);
 
   488  by(Simp_tac 1);
 
   488  by (Simp_tac 1);
 
   489 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   489 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   490 by(Blast_tac 1);
 
   490 by (Blast_tac 1);
 
   491 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 
   491 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 
   492 Addsimps [takeWhile_append1];
 
   492 Addsimps [takeWhile_append1];
 
   493 
   493 
   494 goal thy
 
   494 goal thy
 
   495   "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 
   495   "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 
   496 by(induct_tac "xs" 1);
 
   496 by (induct_tac "xs" 1);
 
   497  by(Simp_tac 1);
 
   497  by (Simp_tac 1);
 
   498 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   498 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   499 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 
   499 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 
   500 Addsimps [takeWhile_append2];
 
   500 Addsimps [takeWhile_append2];
 
   501 
   501 
   502 goal thy
 
   502 goal thy
 
   503   "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
 
   503   "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
 
   504 by(induct_tac "xs" 1);
 
   504 by (induct_tac "xs" 1);
 
   505  by(Simp_tac 1);
 
   505  by (Simp_tac 1);
 
   506 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   506 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   507 by(Blast_tac 1);
 
   507 by (Blast_tac 1);
 
   508 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 
   508 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 
   509 Addsimps [dropWhile_append1];
 
   509 Addsimps [dropWhile_append1];
 
   510 
   510 
   511 goal thy
 
   511 goal thy
 
   512   "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 
   512   "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 
   513 by(induct_tac "xs" 1);
 
   513 by (induct_tac "xs" 1);
 
   514  by(Simp_tac 1);
 
   514  by (Simp_tac 1);
 
   515 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   515 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   516 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 
   516 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 
   517 Addsimps [dropWhile_append2];
 
   517 Addsimps [dropWhile_append2];
 
   518 
   518 
   519 goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
 
   519 goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
 
   520 by(induct_tac "xs" 1);
 
   520 by (induct_tac "xs" 1);
 
   521  by(Simp_tac 1);
 
   521  by (Simp_tac 1);
 
   522 by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   522 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 
   523 qed_spec_mp"set_of_list_take_whileD";
 
   523 qed_spec_mp"set_of_list_take_whileD";
 
   524 
   524
isabelle