src/HOL/List.ML
changeset 5316 7a8975451a89
parent 5296 bdef7d349d27
child 5318 72bf8039b53f
     1.1 --- a/src/HOL/List.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -8,14 +8,14 @@
     1.4  
     1.5  Goal "!x. xs ~= x#xs";
     1.6  by (induct_tac "xs" 1);
     1.7 -by (Auto_tac);
     1.8 +by Auto_tac;
     1.9  qed_spec_mp "not_Cons_self";
    1.10  bind_thm("not_Cons_self2",not_Cons_self RS not_sym);
    1.11  Addsimps [not_Cons_self,not_Cons_self2];
    1.12  
    1.13  Goal "(xs ~= []) = (? y ys. xs = y#ys)";
    1.14  by (induct_tac "xs" 1);
    1.15 -by (Auto_tac);
    1.16 +by Auto_tac;
    1.17  qed "neq_Nil_conv";
    1.18  
    1.19  (* Induction over the length of a list: *)
    1.20 @@ -71,43 +71,43 @@
    1.21  
    1.22  Goal "length(xs@ys) = length(xs)+length(ys)";
    1.23  by (induct_tac "xs" 1);
    1.24 -by (Auto_tac);
    1.25 +by Auto_tac;
    1.26  qed"length_append";
    1.27  Addsimps [length_append];
    1.28  
    1.29  Goal "length (map f xs) = length xs";
    1.30  by (induct_tac "xs" 1);
    1.31 -by (Auto_tac);
    1.32 +by Auto_tac;
    1.33  qed "length_map";
    1.34  Addsimps [length_map];
    1.35  
    1.36  Goal "length(rev xs) = length(xs)";
    1.37  by (induct_tac "xs" 1);
    1.38 -by (Auto_tac);
    1.39 +by Auto_tac;
    1.40  qed "length_rev";
    1.41  Addsimps [length_rev];
    1.42  
    1.43  Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
    1.44  by (exhaust_tac "xs" 1);
    1.45 -by (Auto_tac);
    1.46 +by Auto_tac;
    1.47  qed "length_tl";
    1.48  Addsimps [length_tl];
    1.49  
    1.50  Goal "(length xs = 0) = (xs = [])";
    1.51  by (induct_tac "xs" 1);
    1.52 -by (Auto_tac);
    1.53 +by Auto_tac;
    1.54  qed "length_0_conv";
    1.55  AddIffs [length_0_conv];
    1.56  
    1.57  Goal "(0 = length xs) = (xs = [])";
    1.58  by (induct_tac "xs" 1);
    1.59 -by (Auto_tac);
    1.60 +by Auto_tac;
    1.61  qed "zero_length_conv";
    1.62  AddIffs [zero_length_conv];
    1.63  
    1.64  Goal "(0 < length xs) = (xs ~= [])";
    1.65  by (induct_tac "xs" 1);
    1.66 -by (Auto_tac);
    1.67 +by Auto_tac;
    1.68  qed "length_greater_0_conv";
    1.69  AddIffs [length_greater_0_conv];
    1.70  
    1.71 @@ -123,36 +123,36 @@
    1.72  
    1.73  Goal "(xs@ys)@zs = xs@(ys@zs)";
    1.74  by (induct_tac "xs" 1);
    1.75 -by (Auto_tac);
    1.76 +by Auto_tac;
    1.77  qed "append_assoc";
    1.78  Addsimps [append_assoc];
    1.79  
    1.80  Goal "xs @ [] = xs";
    1.81  by (induct_tac "xs" 1);
    1.82 -by (Auto_tac);
    1.83 +by Auto_tac;
    1.84  qed "append_Nil2";
    1.85  Addsimps [append_Nil2];
    1.86  
    1.87  Goal "(xs@ys = []) = (xs=[] & ys=[])";
    1.88  by (induct_tac "xs" 1);
    1.89 -by (Auto_tac);
    1.90 +by Auto_tac;
    1.91  qed "append_is_Nil_conv";
    1.92  AddIffs [append_is_Nil_conv];
    1.93  
    1.94  Goal "([] = xs@ys) = (xs=[] & ys=[])";
    1.95  by (induct_tac "xs" 1);
    1.96 -by (Auto_tac);
    1.97 +by Auto_tac;
    1.98  qed "Nil_is_append_conv";
    1.99  AddIffs [Nil_is_append_conv];
   1.100  
   1.101  Goal "(xs @ ys = xs) = (ys=[])";
   1.102  by (induct_tac "xs" 1);
   1.103 -by (Auto_tac);
   1.104 +by Auto_tac;
   1.105  qed "append_self_conv";
   1.106  
   1.107  Goal "(xs = xs @ ys) = (ys=[])";
   1.108  by (induct_tac "xs" 1);
   1.109 -by (Auto_tac);
   1.110 +by Auto_tac;
   1.111  qed "self_append_conv";
   1.112  AddIffs [append_self_conv,self_append_conv];
   1.113  
   1.114 @@ -192,7 +192,7 @@
   1.115  
   1.116  Goal "(xs @ ys = ys) = (xs=[])";
   1.117  by (cut_inst_tac [("zs","[]")] append_same_eq 1);
   1.118 -by (Auto_tac);
   1.119 +by Auto_tac;
   1.120  qed "append_self_conv2";
   1.121  
   1.122  Goal "(ys = xs @ ys) = (xs=[])";
   1.123 @@ -204,13 +204,13 @@
   1.124  
   1.125  Goal "xs ~= [] --> hd xs # tl xs = xs";
   1.126  by (induct_tac "xs" 1);
   1.127 -by (Auto_tac);
   1.128 +by Auto_tac;
   1.129  qed_spec_mp "hd_Cons_tl";
   1.130  Addsimps [hd_Cons_tl];
   1.131  
   1.132  Goal "hd(xs@ys) = (if xs=[] then hd ys else hd xs)";
   1.133  by (induct_tac "xs" 1);
   1.134 -by (Auto_tac);
   1.135 +by Auto_tac;
   1.136  qed "hd_append";
   1.137  
   1.138  Goal "xs ~= [] ==> hd(xs @ ys) = hd xs";
   1.139 @@ -252,31 +252,31 @@
   1.140  
   1.141  Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
   1.142  by (induct_tac "xs" 1);
   1.143 -by (Auto_tac);
   1.144 +by Auto_tac;
   1.145  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
   1.146  
   1.147  Goal "map (%x. x) = (%xs. xs)";
   1.148  by (rtac ext 1);
   1.149  by (induct_tac "xs" 1);
   1.150 -by (Auto_tac);
   1.151 +by Auto_tac;
   1.152  qed "map_ident";
   1.153  Addsimps[map_ident];
   1.154  
   1.155  Goal "map f (xs@ys) = map f xs @ map f ys";
   1.156  by (induct_tac "xs" 1);
   1.157 -by (Auto_tac);
   1.158 +by Auto_tac;
   1.159  qed "map_append";
   1.160  Addsimps[map_append];
   1.161  
   1.162  Goalw [o_def] "map (f o g) xs = map f (map g xs)";
   1.163  by (induct_tac "xs" 1);
   1.164 -by (Auto_tac);
   1.165 +by Auto_tac;
   1.166  qed "map_compose";
   1.167  Addsimps[map_compose];
   1.168  
   1.169  Goal "rev(map f xs) = map f (rev xs)";
   1.170  by (induct_tac "xs" 1);
   1.171 -by (Auto_tac);
   1.172 +by Auto_tac;
   1.173  qed "rev_map";
   1.174  
   1.175  (* a congruence rule for map: *)
   1.176 @@ -284,19 +284,19 @@
   1.177  by (rtac impI 1);
   1.178  by (hyp_subst_tac 1);
   1.179  by (induct_tac "ys" 1);
   1.180 -by (Auto_tac);
   1.181 +by Auto_tac;
   1.182  val lemma = result();
   1.183  bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
   1.184  
   1.185  Goal "(map f xs = []) = (xs = [])";
   1.186  by (induct_tac "xs" 1);
   1.187 -by (Auto_tac);
   1.188 +by Auto_tac;
   1.189  qed "map_is_Nil_conv";
   1.190  AddIffs [map_is_Nil_conv];
   1.191  
   1.192  Goal "([] = map f xs) = (xs = [])";
   1.193  by (induct_tac "xs" 1);
   1.194 -by (Auto_tac);
   1.195 +by Auto_tac;
   1.196  qed "Nil_is_map_conv";
   1.197  AddIffs [Nil_is_map_conv];
   1.198  
   1.199 @@ -307,25 +307,25 @@
   1.200  
   1.201  Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
   1.202  by (induct_tac "xs" 1);
   1.203 -by (Auto_tac);
   1.204 +by Auto_tac;
   1.205  qed "rev_append";
   1.206  Addsimps[rev_append];
   1.207  
   1.208  Goal "rev(rev l) = l";
   1.209  by (induct_tac "l" 1);
   1.210 -by (Auto_tac);
   1.211 +by Auto_tac;
   1.212  qed "rev_rev_ident";
   1.213  Addsimps[rev_rev_ident];
   1.214  
   1.215  Goal "(rev xs = []) = (xs = [])";
   1.216  by (induct_tac "xs" 1);
   1.217 -by (Auto_tac);
   1.218 +by Auto_tac;
   1.219  qed "rev_is_Nil_conv";
   1.220  AddIffs [rev_is_Nil_conv];
   1.221  
   1.222  Goal "([] = rev xs) = (xs = [])";
   1.223  by (induct_tac "xs" 1);
   1.224 -by (Auto_tac);
   1.225 +by Auto_tac;
   1.226  qed "Nil_is_rev_conv";
   1.227  AddIffs [Nil_is_rev_conv];
   1.228  
   1.229 @@ -341,7 +341,7 @@
   1.230  
   1.231  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
   1.232  by (res_inst_tac [("xs","xs")] rev_induct 1);
   1.233 -by (Auto_tac);
   1.234 +by Auto_tac;
   1.235  bind_thm ("rev_exhaust",
   1.236    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
   1.237  
   1.238 @@ -352,13 +352,13 @@
   1.239  
   1.240  Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
   1.241  by (induct_tac "xs" 1);
   1.242 -by (Auto_tac);
   1.243 +by Auto_tac;
   1.244  qed "mem_append";
   1.245  Addsimps[mem_append];
   1.246  
   1.247  Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
   1.248  by (induct_tac "xs" 1);
   1.249 -by (Auto_tac);
   1.250 +by Auto_tac;
   1.251  qed "mem_filter";
   1.252  Addsimps[mem_filter];
   1.253  
   1.254 @@ -373,40 +373,40 @@
   1.255  
   1.256  Goal "set (xs@ys) = (set xs Un set ys)";
   1.257  by (induct_tac "xs" 1);
   1.258 -by (Auto_tac);
   1.259 +by Auto_tac;
   1.260  qed "set_append";
   1.261  Addsimps[set_append];
   1.262  
   1.263  Goal "(x mem xs) = (x: set xs)";
   1.264  by (induct_tac "xs" 1);
   1.265 -by (Auto_tac);
   1.266 +by Auto_tac;
   1.267  qed "set_mem_eq";
   1.268  
   1.269  Goal "set l <= set (x#l)";
   1.270 -by (Auto_tac);
   1.271 +by Auto_tac;
   1.272  qed "set_subset_Cons";
   1.273  
   1.274  Goal "(set xs = {}) = (xs = [])";
   1.275  by (induct_tac "xs" 1);
   1.276 -by (Auto_tac);
   1.277 +by Auto_tac;
   1.278  qed "set_empty";
   1.279  Addsimps [set_empty];
   1.280  
   1.281  Goal "set(rev xs) = set(xs)";
   1.282  by (induct_tac "xs" 1);
   1.283 -by (Auto_tac);
   1.284 +by Auto_tac;
   1.285  qed "set_rev";
   1.286  Addsimps [set_rev];
   1.287  
   1.288  Goal "set(map f xs) = f``(set xs)";
   1.289  by (induct_tac "xs" 1);
   1.290 -by (Auto_tac);
   1.291 +by Auto_tac;
   1.292  qed "set_map";
   1.293  Addsimps [set_map];
   1.294  
   1.295  Goal "(x : set(filter P xs)) = (x : set xs & P x)";
   1.296  by (induct_tac "xs" 1);
   1.297 -by (Auto_tac);
   1.298 +by Auto_tac;
   1.299  qed "in_set_filter";
   1.300  Addsimps [in_set_filter];
   1.301  
   1.302 @@ -418,14 +418,14 @@
   1.303  by(blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
   1.304  by(REPEAT(etac exE 1));
   1.305  by(exhaust_tac "ys" 1);
   1.306 -by(Auto_tac);
   1.307 +by Auto_tac;
   1.308  qed "in_set_conv_decomp";
   1.309  
   1.310  (* eliminate `lists' in favour of `set' *)
   1.311  
   1.312  Goal "(xs : lists A) = (!x : set xs. x : A)";
   1.313  by(induct_tac "xs" 1);
   1.314 -by(Auto_tac);
   1.315 +by Auto_tac;
   1.316  qed "in_lists_conv_set";
   1.317  
   1.318  bind_thm("in_listsD",in_lists_conv_set RS iffD1);
   1.319 @@ -439,19 +439,19 @@
   1.320  
   1.321  Goal "list_all (%x. True) xs = True";
   1.322  by (induct_tac "xs" 1);
   1.323 -by (Auto_tac);
   1.324 +by Auto_tac;
   1.325  qed "list_all_True";
   1.326  Addsimps [list_all_True];
   1.327  
   1.328  Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
   1.329  by (induct_tac "xs" 1);
   1.330 -by (Auto_tac);
   1.331 +by Auto_tac;
   1.332  qed "list_all_append";
   1.333  Addsimps [list_all_append];
   1.334  
   1.335  Goal "list_all P xs = (!x. x mem xs --> P(x))";
   1.336  by (induct_tac "xs" 1);
   1.337 -by (Auto_tac);
   1.338 +by Auto_tac;
   1.339  qed "list_all_mem_conv";
   1.340  
   1.341  
   1.342 @@ -461,25 +461,25 @@
   1.343  
   1.344  Goal "filter P (xs@ys) = filter P xs @ filter P ys";
   1.345  by (induct_tac "xs" 1);
   1.346 -by (Auto_tac);
   1.347 +by Auto_tac;
   1.348  qed "filter_append";
   1.349  Addsimps [filter_append];
   1.350  
   1.351  Goal "filter (%x. True) xs = xs";
   1.352  by (induct_tac "xs" 1);
   1.353 -by (Auto_tac);
   1.354 +by Auto_tac;
   1.355  qed "filter_True";
   1.356  Addsimps [filter_True];
   1.357  
   1.358  Goal "filter (%x. False) xs = []";
   1.359  by (induct_tac "xs" 1);
   1.360 -by (Auto_tac);
   1.361 +by Auto_tac;
   1.362  qed "filter_False";
   1.363  Addsimps [filter_False];
   1.364  
   1.365  Goal "length (filter P xs) <= length xs";
   1.366  by (induct_tac "xs" 1);
   1.367 -by (Auto_tac);
   1.368 +by Auto_tac;
   1.369  qed "length_filter";
   1.370  
   1.371  
   1.372 @@ -489,41 +489,41 @@
   1.373  
   1.374  Goal  "concat(xs@ys) = concat(xs)@concat(ys)";
   1.375  by (induct_tac "xs" 1);
   1.376 -by (Auto_tac);
   1.377 +by Auto_tac;
   1.378  qed"concat_append";
   1.379  Addsimps [concat_append];
   1.380  
   1.381  Goal "(concat xss = []) = (!xs:set xss. xs=[])";
   1.382  by (induct_tac "xss" 1);
   1.383 -by (Auto_tac);
   1.384 +by Auto_tac;
   1.385  qed "concat_eq_Nil_conv";
   1.386  AddIffs [concat_eq_Nil_conv];
   1.387  
   1.388  Goal "([] = concat xss) = (!xs:set xss. xs=[])";
   1.389  by (induct_tac "xss" 1);
   1.390 -by (Auto_tac);
   1.391 +by Auto_tac;
   1.392  qed "Nil_eq_concat_conv";
   1.393  AddIffs [Nil_eq_concat_conv];
   1.394  
   1.395  Goal  "set(concat xs) = Union(set `` set xs)";
   1.396  by (induct_tac "xs" 1);
   1.397 -by (Auto_tac);
   1.398 +by Auto_tac;
   1.399  qed"set_concat";
   1.400  Addsimps [set_concat];
   1.401  
   1.402  Goal "map f (concat xs) = concat (map (map f) xs)"; 
   1.403  by (induct_tac "xs" 1);
   1.404 -by (Auto_tac);
   1.405 +by Auto_tac;
   1.406  qed "map_concat";
   1.407  
   1.408  Goal "filter p (concat xs) = concat (map (filter p) xs)"; 
   1.409  by (induct_tac "xs" 1);
   1.410 -by (Auto_tac);
   1.411 +by Auto_tac;
   1.412  qed"filter_concat"; 
   1.413  
   1.414  Goal "rev(concat xs) = concat (map rev (rev xs))";
   1.415  by (induct_tac "xs" 1);
   1.416 -by (Auto_tac);
   1.417 +by Auto_tac;
   1.418  qed "rev_concat";
   1.419  
   1.420  (** nth **)
   1.421 @@ -535,7 +535,7 @@
   1.422   by (Asm_simp_tac 1);
   1.423   by (rtac allI 1);
   1.424   by (exhaust_tac "xs" 1);
   1.425 -  by (Auto_tac);
   1.426 +  by Auto_tac;
   1.427  qed_spec_mp "nth_append";
   1.428  
   1.429  Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
   1.430 @@ -545,7 +545,7 @@
   1.431  (* case x#xl *)
   1.432  by (rtac allI 1);
   1.433  by (induct_tac "n" 1);
   1.434 -by (Auto_tac);
   1.435 +by Auto_tac;
   1.436  qed_spec_mp "nth_map";
   1.437  Addsimps [nth_map];
   1.438  
   1.439 @@ -556,7 +556,7 @@
   1.440  (* case x#xl *)
   1.441  by (rtac allI 1);
   1.442  by (induct_tac "n" 1);
   1.443 -by (Auto_tac);
   1.444 +by Auto_tac;
   1.445  qed_spec_mp "list_all_nth";
   1.446  
   1.447  Goal "!n. n < length xs --> xs!n mem xs";
   1.448 @@ -589,30 +589,30 @@
   1.449  
   1.450  Goal "last(xs@[x]) = x";
   1.451  by (induct_tac "xs" 1);
   1.452 -by (Auto_tac);
   1.453 +by Auto_tac;
   1.454  qed "last_snoc";
   1.455  Addsimps [last_snoc];
   1.456  
   1.457  Goal "butlast(xs@[x]) = xs";
   1.458  by (induct_tac "xs" 1);
   1.459 -by (Auto_tac);
   1.460 +by Auto_tac;
   1.461  qed "butlast_snoc";
   1.462  Addsimps [butlast_snoc];
   1.463  
   1.464  Goal "length(butlast xs) = length xs - 1";
   1.465  by (res_inst_tac [("xs","xs")] rev_induct 1);
   1.466 -by (Auto_tac);
   1.467 +by Auto_tac;
   1.468  qed "length_butlast";
   1.469  Addsimps [length_butlast];
   1.470  
   1.471  Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   1.472  by (induct_tac "xs" 1);
   1.473 -by (Auto_tac);
   1.474 +by Auto_tac;
   1.475  qed_spec_mp "butlast_append";
   1.476  
   1.477  Goal "x:set(butlast xs) --> x:set xs";
   1.478  by (induct_tac "xs" 1);
   1.479 -by (Auto_tac);
   1.480 +by Auto_tac;
   1.481  qed_spec_mp "in_set_butlastD";
   1.482  
   1.483  Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   1.484 @@ -631,12 +631,12 @@
   1.485  
   1.486  Goal "take 0 xs = []";
   1.487  by (induct_tac "xs" 1);
   1.488 -by (Auto_tac);
   1.489 +by Auto_tac;
   1.490  qed "take_0";
   1.491  
   1.492  Goal "drop 0 xs = xs";
   1.493  by (induct_tac "xs" 1);
   1.494 -by (Auto_tac);
   1.495 +by Auto_tac;
   1.496  qed "drop_0";
   1.497  
   1.498  Goal "take (Suc n) (x#xs) = x # take n xs";
   1.499 @@ -652,102 +652,102 @@
   1.500  
   1.501  Goal "!xs. length(take n xs) = min (length xs) n";
   1.502  by (induct_tac "n" 1);
   1.503 - by (Auto_tac);
   1.504 + by Auto_tac;
   1.505  by (exhaust_tac "xs" 1);
   1.506 - by (Auto_tac);
   1.507 + by Auto_tac;
   1.508  qed_spec_mp "length_take";
   1.509  Addsimps [length_take];
   1.510  
   1.511  Goal "!xs. length(drop n xs) = (length xs - n)";
   1.512  by (induct_tac "n" 1);
   1.513 - by (Auto_tac);
   1.514 + by Auto_tac;
   1.515  by (exhaust_tac "xs" 1);
   1.516 - by (Auto_tac);
   1.517 + by Auto_tac;
   1.518  qed_spec_mp "length_drop";
   1.519  Addsimps [length_drop];
   1.520  
   1.521  Goal "!xs. length xs <= n --> take n xs = xs";
   1.522  by (induct_tac "n" 1);
   1.523 - by (Auto_tac);
   1.524 + by Auto_tac;
   1.525  by (exhaust_tac "xs" 1);
   1.526 - by (Auto_tac);
   1.527 + by Auto_tac;
   1.528  qed_spec_mp "take_all";
   1.529  
   1.530  Goal "!xs. length xs <= n --> drop n xs = []";
   1.531  by (induct_tac "n" 1);
   1.532 - by (Auto_tac);
   1.533 + by Auto_tac;
   1.534  by (exhaust_tac "xs" 1);
   1.535 - by (Auto_tac);
   1.536 + by Auto_tac;
   1.537  qed_spec_mp "drop_all";
   1.538  
   1.539  Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   1.540  by (induct_tac "n" 1);
   1.541 - by (Auto_tac);
   1.542 + by Auto_tac;
   1.543  by (exhaust_tac "xs" 1);
   1.544 - by (Auto_tac);
   1.545 + by Auto_tac;
   1.546  qed_spec_mp "take_append";
   1.547  Addsimps [take_append];
   1.548  
   1.549  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   1.550  by (induct_tac "n" 1);
   1.551 - by (Auto_tac);
   1.552 + by Auto_tac;
   1.553  by (exhaust_tac "xs" 1);
   1.554 - by (Auto_tac);
   1.555 + by Auto_tac;
   1.556  qed_spec_mp "drop_append";
   1.557  Addsimps [drop_append];
   1.558  
   1.559  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
   1.560  by (induct_tac "m" 1);
   1.561 - by (Auto_tac);
   1.562 + by Auto_tac;
   1.563  by (exhaust_tac "xs" 1);
   1.564 - by (Auto_tac);
   1.565 + by Auto_tac;
   1.566  by (exhaust_tac "na" 1);
   1.567 - by (Auto_tac);
   1.568 + by Auto_tac;
   1.569  qed_spec_mp "take_take";
   1.570  
   1.571  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   1.572  by (induct_tac "m" 1);
   1.573 - by (Auto_tac);
   1.574 + by Auto_tac;
   1.575  by (exhaust_tac "xs" 1);
   1.576 - by (Auto_tac);
   1.577 + by Auto_tac;
   1.578  qed_spec_mp "drop_drop";
   1.579  
   1.580  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   1.581  by (induct_tac "m" 1);
   1.582 - by (Auto_tac);
   1.583 + by Auto_tac;
   1.584  by (exhaust_tac "xs" 1);
   1.585 - by (Auto_tac);
   1.586 + by Auto_tac;
   1.587  qed_spec_mp "take_drop";
   1.588  
   1.589  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
   1.590  by (induct_tac "n" 1);
   1.591 - by (Auto_tac);
   1.592 + by Auto_tac;
   1.593  by (exhaust_tac "xs" 1);
   1.594 - by (Auto_tac);
   1.595 + by Auto_tac;
   1.596  qed_spec_mp "take_map"; 
   1.597  
   1.598  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
   1.599  by (induct_tac "n" 1);
   1.600 - by (Auto_tac);
   1.601 + by Auto_tac;
   1.602  by (exhaust_tac "xs" 1);
   1.603 - by (Auto_tac);
   1.604 + by Auto_tac;
   1.605  qed_spec_mp "drop_map";
   1.606  
   1.607  Goal "!n i. i < n --> (take n xs)!i = xs!i";
   1.608  by (induct_tac "xs" 1);
   1.609 - by (Auto_tac);
   1.610 + by Auto_tac;
   1.611  by (exhaust_tac "n" 1);
   1.612   by (Blast_tac 1);
   1.613  by (exhaust_tac "i" 1);
   1.614 - by (Auto_tac);
   1.615 + by Auto_tac;
   1.616  qed_spec_mp "nth_take";
   1.617  Addsimps [nth_take];
   1.618  
   1.619  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
   1.620  by (induct_tac "n" 1);
   1.621 - by (Auto_tac);
   1.622 + by Auto_tac;
   1.623  by (exhaust_tac "xs" 1);
   1.624 - by (Auto_tac);
   1.625 + by Auto_tac;
   1.626  qed_spec_mp "nth_drop";
   1.627  Addsimps [nth_drop];
   1.628  
   1.629 @@ -757,37 +757,37 @@
   1.630  
   1.631  Goal "takeWhile P xs @ dropWhile P xs = xs";
   1.632  by (induct_tac "xs" 1);
   1.633 -by (Auto_tac);
   1.634 +by Auto_tac;
   1.635  qed "takeWhile_dropWhile_id";
   1.636  Addsimps [takeWhile_dropWhile_id];
   1.637  
   1.638  Goal  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   1.639  by (induct_tac "xs" 1);
   1.640 -by (Auto_tac);
   1.641 +by Auto_tac;
   1.642  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   1.643  Addsimps [takeWhile_append1];
   1.644  
   1.645  Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   1.646  by (induct_tac "xs" 1);
   1.647 -by (Auto_tac);
   1.648 +by Auto_tac;
   1.649  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   1.650  Addsimps [takeWhile_append2];
   1.651  
   1.652  Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   1.653  by (induct_tac "xs" 1);
   1.654 -by (Auto_tac);
   1.655 +by Auto_tac;
   1.656  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   1.657  Addsimps [dropWhile_append1];
   1.658  
   1.659  Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   1.660  by (induct_tac "xs" 1);
   1.661 -by (Auto_tac);
   1.662 +by Auto_tac;
   1.663  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   1.664  Addsimps [dropWhile_append2];
   1.665  
   1.666  Goal "x:set(takeWhile P xs) --> x:set xs & P x";
   1.667  by (induct_tac "xs" 1);
   1.668 -by (Auto_tac);
   1.669 +by Auto_tac;
   1.670  qed_spec_mp"set_take_whileD";
   1.671  
   1.672  qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
   1.673 @@ -800,7 +800,7 @@
   1.674  
   1.675  Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
   1.676  by(induct_tac "xs" 1);
   1.677 -by(Auto_tac);
   1.678 +by Auto_tac;
   1.679  qed_spec_mp "foldl_append";
   1.680  Addsimps [foldl_append];
   1.681  
   1.682 @@ -821,7 +821,7 @@
   1.683  
   1.684  Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
   1.685  by(induct_tac "ns" 1);
   1.686 -by(Auto_tac);
   1.687 +by Auto_tac;
   1.688  qed_spec_mp "sum_eq_0_conv";
   1.689  AddIffs [sum_eq_0_conv];
   1.690  
   1.691 @@ -838,12 +838,12 @@
   1.692  
   1.693  Goal "nodups(remdups xs)";
   1.694  by (induct_tac "xs" 1);
   1.695 -by (Auto_tac);
   1.696 +by Auto_tac;
   1.697  qed "nodups_remdups";
   1.698  
   1.699  Goal "nodups xs --> nodups (filter P xs)";
   1.700  by (induct_tac "xs" 1);
   1.701 -by (Auto_tac);
   1.702 +by Auto_tac;
   1.703  qed_spec_mp "nodups_filter";
   1.704  
   1.705  (** replicate **)
   1.706 @@ -851,7 +851,7 @@
   1.707  
   1.708  Goal "set(replicate (Suc n) x) = {x}";
   1.709  by (induct_tac "n" 1);
   1.710 -by (Auto_tac);
   1.711 +by Auto_tac;
   1.712  val lemma = result();
   1.713  
   1.714  Goal "n ~= 0 ==> set(replicate n x) = {x}";