src/HOL/List.ML
changeset 8442 96023903c2df
parent 8423 3c19160b6432
child 8741 61bc5ed22b62
     1.1 --- a/src/HOL/List.ML	Mon Mar 13 15:42:19 2000 +0100
     1.2 +++ b/src/HOL/List.ML	Mon Mar 13 16:23:34 2000 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4  Addsimps [length_rev];
     1.5  
     1.6  Goal "length(tl xs) = (length xs) - 1";
     1.7 -by (cases_tac "xs" 1);
     1.8 +by (case_tac "xs" 1);
     1.9  by Auto_tac;
    1.10  qed "length_tl";
    1.11  Addsimps [length_tl];
    1.12 @@ -159,11 +159,11 @@
    1.13  \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
    1.14  by (induct_tac "xs" 1);
    1.15   by (rtac allI 1);
    1.16 - by (cases_tac "ys" 1);
    1.17 + by (case_tac "ys" 1);
    1.18    by (Asm_simp_tac 1);
    1.19   by (Force_tac 1);
    1.20  by (rtac allI 1);
    1.21 -by (cases_tac "ys" 1);
    1.22 +by (case_tac "ys" 1);
    1.23  by (Force_tac 1);
    1.24  by (Asm_simp_tac 1);
    1.25  qed_spec_mp "append_eq_append_conv";
    1.26 @@ -340,19 +340,19 @@
    1.27  bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
    1.28  
    1.29  Goal "(map f xs = []) = (xs = [])";
    1.30 -by (cases_tac "xs" 1);
    1.31 +by (case_tac "xs" 1);
    1.32  by Auto_tac;
    1.33  qed "map_is_Nil_conv";
    1.34  AddIffs [map_is_Nil_conv];
    1.35  
    1.36  Goal "([] = map f xs) = (xs = [])";
    1.37 -by (cases_tac "xs" 1);
    1.38 +by (case_tac "xs" 1);
    1.39  by Auto_tac;
    1.40  qed "Nil_is_map_conv";
    1.41  AddIffs [Nil_is_map_conv];
    1.42  
    1.43  Goal "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)";
    1.44 -by (cases_tac "xs" 1);
    1.45 +by (case_tac "xs" 1);
    1.46  by (ALLGOALS Asm_simp_tac);
    1.47  qed "map_eq_Cons";
    1.48  
    1.49 @@ -411,7 +411,7 @@
    1.50  by (induct_tac "xs" 1);
    1.51   by (Force_tac 1);
    1.52  by (rtac allI 1);
    1.53 -by (cases_tac "ys" 1);
    1.54 +by (case_tac "ys" 1);
    1.55   by (Asm_simp_tac 1);
    1.56  by (Force_tac 1);
    1.57  qed_spec_mp "rev_is_rev_conv";
    1.58 @@ -492,7 +492,7 @@
    1.59  by (rtac iffI 1);
    1.60  by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
    1.61  by (REPEAT(etac exE 1));
    1.62 -by (cases_tac "ys" 1);
    1.63 +by (case_tac "ys" 1);
    1.64  by Auto_tac;
    1.65  qed "in_set_conv_decomp";
    1.66  
    1.67 @@ -630,7 +630,7 @@
    1.68  by (induct_tac "xs" 1);
    1.69   by (Asm_simp_tac 1);
    1.70   by (rtac allI 1);
    1.71 - by (cases_tac "n" 1);
    1.72 + by (case_tac "n" 1);
    1.73    by Auto_tac;
    1.74  qed_spec_mp "nth_append";
    1.75  
    1.76 @@ -652,7 +652,7 @@
    1.77    by (Simp_tac 1);
    1.78   by (res_inst_tac [("x","Suc i")] exI 1);
    1.79   by (Asm_simp_tac 1);
    1.80 -by (cases_tac "i" 1);
    1.81 +by (case_tac "i" 1);
    1.82   by (Asm_full_simp_tac 1);
    1.83  by (rename_tac "j" 1);
    1.84   by (res_inst_tac [("x","j")] exI 1);
    1.85 @@ -728,7 +728,7 @@
    1.86  \     (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])";
    1.87  by (induct_tac "ys" 1);
    1.88   by Auto_tac;
    1.89 -by (cases_tac "xs" 1);
    1.90 +by (case_tac "xs" 1);
    1.91   by (auto_tac (claset(), simpset() addsplits [nat.split]));
    1.92  qed_spec_mp "update_zip";
    1.93  
    1.94 @@ -813,7 +813,7 @@
    1.95  Goal "!xs. length(take n xs) = min (length xs) n";
    1.96  by (induct_tac "n" 1);
    1.97   by Auto_tac;
    1.98 -by (cases_tac "xs" 1);
    1.99 +by (case_tac "xs" 1);
   1.100   by Auto_tac;
   1.101  qed_spec_mp "length_take";
   1.102  Addsimps [length_take];
   1.103 @@ -821,7 +821,7 @@
   1.104  Goal "!xs. length(drop n xs) = (length xs - n)";
   1.105  by (induct_tac "n" 1);
   1.106   by Auto_tac;
   1.107 -by (cases_tac "xs" 1);
   1.108 +by (case_tac "xs" 1);
   1.109   by Auto_tac;
   1.110  qed_spec_mp "length_drop";
   1.111  Addsimps [length_drop];
   1.112 @@ -829,7 +829,7 @@
   1.113  Goal "!xs. length xs <= n --> take n xs = xs";
   1.114  by (induct_tac "n" 1);
   1.115   by Auto_tac;
   1.116 -by (cases_tac "xs" 1);
   1.117 +by (case_tac "xs" 1);
   1.118   by Auto_tac;
   1.119  qed_spec_mp "take_all";
   1.120  Addsimps [take_all];
   1.121 @@ -837,7 +837,7 @@
   1.122  Goal "!xs. length xs <= n --> drop n xs = []";
   1.123  by (induct_tac "n" 1);
   1.124   by Auto_tac;
   1.125 -by (cases_tac "xs" 1);
   1.126 +by (case_tac "xs" 1);
   1.127   by Auto_tac;
   1.128  qed_spec_mp "drop_all";
   1.129  Addsimps [drop_all];
   1.130 @@ -845,7 +845,7 @@
   1.131  Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   1.132  by (induct_tac "n" 1);
   1.133   by Auto_tac;
   1.134 -by (cases_tac "xs" 1);
   1.135 +by (case_tac "xs" 1);
   1.136   by Auto_tac;
   1.137  qed_spec_mp "take_append";
   1.138  Addsimps [take_append];
   1.139 @@ -853,7 +853,7 @@
   1.140  Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   1.141  by (induct_tac "n" 1);
   1.142   by Auto_tac;
   1.143 -by (cases_tac "xs" 1);
   1.144 +by (case_tac "xs" 1);
   1.145   by Auto_tac;
   1.146  qed_spec_mp "drop_append";
   1.147  Addsimps [drop_append];
   1.148 @@ -861,9 +861,9 @@
   1.149  Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
   1.150  by (induct_tac "m" 1);
   1.151   by Auto_tac;
   1.152 -by (cases_tac "xs" 1);
   1.153 +by (case_tac "xs" 1);
   1.154   by Auto_tac;
   1.155 -by (cases_tac "na" 1);
   1.156 +by (case_tac "na" 1);
   1.157   by Auto_tac;
   1.158  qed_spec_mp "take_take";
   1.159  Addsimps [take_take];
   1.160 @@ -871,7 +871,7 @@
   1.161  Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   1.162  by (induct_tac "m" 1);
   1.163   by Auto_tac;
   1.164 -by (cases_tac "xs" 1);
   1.165 +by (case_tac "xs" 1);
   1.166   by Auto_tac;
   1.167  qed_spec_mp "drop_drop";
   1.168  Addsimps [drop_drop];
   1.169 @@ -879,14 +879,14 @@
   1.170  Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   1.171  by (induct_tac "m" 1);
   1.172   by Auto_tac;
   1.173 -by (cases_tac "xs" 1);
   1.174 +by (case_tac "xs" 1);
   1.175   by Auto_tac;
   1.176  qed_spec_mp "take_drop";
   1.177  
   1.178  Goal "!xs. take n xs @ drop n xs = xs";
   1.179  by (induct_tac "n" 1);
   1.180   by Auto_tac;
   1.181 -by (cases_tac "xs" 1);
   1.182 +by (case_tac "xs" 1);
   1.183   by Auto_tac;
   1.184  qed_spec_mp "append_take_drop_id";
   1.185  Addsimps [append_take_drop_id];
   1.186 @@ -894,23 +894,23 @@
   1.187  Goal "!xs. take n (map f xs) = map f (take n xs)"; 
   1.188  by (induct_tac "n" 1);
   1.189   by Auto_tac;
   1.190 -by (cases_tac "xs" 1);
   1.191 +by (case_tac "xs" 1);
   1.192   by Auto_tac;
   1.193  qed_spec_mp "take_map"; 
   1.194  
   1.195  Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
   1.196  by (induct_tac "n" 1);
   1.197   by Auto_tac;
   1.198 -by (cases_tac "xs" 1);
   1.199 +by (case_tac "xs" 1);
   1.200   by Auto_tac;
   1.201  qed_spec_mp "drop_map";
   1.202  
   1.203  Goal "!n i. i < n --> (take n xs)!i = xs!i";
   1.204  by (induct_tac "xs" 1);
   1.205   by Auto_tac;
   1.206 -by (cases_tac "n" 1);
   1.207 +by (case_tac "n" 1);
   1.208   by (Blast_tac 1);
   1.209 -by (cases_tac "i" 1);
   1.210 +by (case_tac "i" 1);
   1.211   by Auto_tac;
   1.212  qed_spec_mp "nth_take";
   1.213  Addsimps [nth_take];
   1.214 @@ -918,7 +918,7 @@
   1.215  Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
   1.216  by (induct_tac "n" 1);
   1.217   by Auto_tac;
   1.218 -by (cases_tac "xs" 1);
   1.219 +by (case_tac "xs" 1);
   1.220   by Auto_tac;
   1.221  qed_spec_mp "nth_drop";
   1.222  Addsimps [nth_drop];
   1.223 @@ -930,7 +930,7 @@
   1.224   by (Simp_tac 1);
   1.225  by (Asm_full_simp_tac 1);
   1.226  by (Clarify_tac 1);
   1.227 -by (cases_tac "zs" 1);
   1.228 +by (case_tac "zs" 1);
   1.229  by (Auto_tac);
   1.230  qed_spec_mp "append_eq_conv_conj";
   1.231  
   1.232 @@ -993,7 +993,7 @@
   1.233  by (induct_tac "ys" 1);
   1.234   by (Simp_tac 1);
   1.235  by (Clarify_tac 1);
   1.236 -by (cases_tac "xs" 1);
   1.237 +by (case_tac "xs" 1);
   1.238   by (Auto_tac);
   1.239  qed_spec_mp "length_zip";
   1.240  Addsimps [length_zip];
   1.241 @@ -1004,7 +1004,7 @@
   1.242  by (induct_tac "zs" 1);
   1.243   by (Simp_tac 1);
   1.244  by (Clarify_tac 1);
   1.245 -by (cases_tac "xs" 1);
   1.246 +by (case_tac "xs" 1);
   1.247   by (Asm_simp_tac 1);
   1.248  by (Asm_simp_tac 1);
   1.249  qed_spec_mp "zip_append1";
   1.250 @@ -1015,7 +1015,7 @@
   1.251  by (induct_tac "xs" 1);
   1.252   by (Simp_tac 1);
   1.253  by (Clarify_tac 1);
   1.254 -by (cases_tac "ys" 1);
   1.255 +by (case_tac "ys" 1);
   1.256   by (Asm_simp_tac 1);
   1.257  by (Asm_simp_tac 1);
   1.258  qed_spec_mp "zip_append2";
   1.259 @@ -1032,7 +1032,7 @@
   1.260   by (Asm_full_simp_tac 1);
   1.261  by (Asm_full_simp_tac 1);
   1.262  by (Clarify_tac 1);
   1.263 -by (cases_tac "xs" 1);
   1.264 +by (case_tac "xs" 1);
   1.265   by (Auto_tac);
   1.266  qed_spec_mp "zip_rev";
   1.267  
   1.268 @@ -1042,7 +1042,7 @@
   1.269  by (induct_tac "ys" 1);
   1.270   by (Simp_tac 1);
   1.271  by (Clarify_tac 1);
   1.272 -by (cases_tac "xs" 1);
   1.273 +by (case_tac "xs" 1);
   1.274   by (Auto_tac);
   1.275  by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
   1.276  qed_spec_mp "nth_zip";
   1.277 @@ -1061,7 +1061,7 @@
   1.278  Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
   1.279  by (induct_tac "i" 1);
   1.280   by (Auto_tac);
   1.281 -by (cases_tac "j" 1);
   1.282 +by (case_tac "j" 1);
   1.283   by (Auto_tac);
   1.284  qed "zip_replicate";
   1.285  Addsimps [zip_replicate];
   1.286 @@ -1091,13 +1091,13 @@
   1.287  
   1.288  Goalw [list_all2_def]
   1.289   "list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)";
   1.290 -by (cases_tac "ys" 1);
   1.291 +by (case_tac "ys" 1);
   1.292  by (Auto_tac);
   1.293  qed "list_all2_Cons1";
   1.294  
   1.295  Goalw [list_all2_def]
   1.296   "list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)";
   1.297 -by (cases_tac "xs" 1);
   1.298 +by (case_tac "xs" 1);
   1.299  by (Auto_tac);
   1.300  qed "list_all2_Cons2";
   1.301  
   1.302 @@ -1249,8 +1249,8 @@
   1.303  						all_conj_distrib])));
   1.304  by (Clarify_tac 1);
   1.305  (*Both lists must be non-empty*)
   1.306 -by (cases_tac "xs" 1);
   1.307 -by (cases_tac "ys" 2);
   1.308 +by (case_tac "xs" 1);
   1.309 +by (case_tac "ys" 2);
   1.310  by (ALLGOALS Clarify_tac);
   1.311  (*prenexing's needed, not miniscoping*)
   1.312  by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])  
   1.313 @@ -1412,7 +1412,7 @@
   1.314   by (rename_tac "a xys x xs' y ys'" 1);
   1.315   by (res_inst_tac [("x","a#xys")] exI 1);
   1.316   by (Simp_tac 1);
   1.317 -by (cases_tac "xys" 1);
   1.318 +by (case_tac "xys" 1);
   1.319   by (ALLGOALS (asm_full_simp_tac (simpset())));
   1.320  by (Blast_tac 1);
   1.321  qed "lexn_conv";
   1.322 @@ -1452,7 +1452,7 @@
   1.323  by (rtac iffI 1);
   1.324   by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
   1.325  by (REPEAT(eresolve_tac [conjE, exE] 1));
   1.326 -by (cases_tac "xys" 1);
   1.327 +by (case_tac "xys" 1);
   1.328  by (Asm_full_simp_tac 1);
   1.329  by (Asm_full_simp_tac 1);
   1.330  by (Blast_tac 1);
   1.331 @@ -1467,19 +1467,19 @@
   1.332  	   sum_eq_0_conv]);
   1.333  
   1.334  Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
   1.335 -by (cases_tac "n" 1);
   1.336 +by (case_tac "n" 1);
   1.337  by (ALLGOALS 
   1.338      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
   1.339  qed "take_Cons'";
   1.340  
   1.341  Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
   1.342 -by (cases_tac "n" 1);
   1.343 +by (case_tac "n" 1);
   1.344  by (ALLGOALS
   1.345      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
   1.346  qed "drop_Cons'";
   1.347  
   1.348  Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
   1.349 -by (cases_tac "n" 1);
   1.350 +by (case_tac "n" 1);
   1.351  by (ALLGOALS
   1.352      (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
   1.353  qed "nth_Cons'";