--- a/src/HOL/List.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/List.ML Mon Mar 13 12:51:10 2000 +0100
@@ -88,7 +88,7 @@
Addsimps [length_rev];
Goal "length(tl xs) = (length xs) - 1";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed "length_tl";
Addsimps [length_tl];
@@ -159,11 +159,11 @@
\ --> (xs@us = ys@vs) = (xs=ys & us=vs)";
by (induct_tac "xs" 1);
by (rtac allI 1);
- by (exhaust_tac "ys" 1);
+ by (cases_tac "ys" 1);
by (Asm_simp_tac 1);
by (Force_tac 1);
by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Force_tac 1);
by (Asm_simp_tac 1);
qed_spec_mp "append_eq_append_conv";
@@ -340,19 +340,19 @@
bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
Goal "(map f xs = []) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed "map_is_Nil_conv";
AddIffs [map_is_Nil_conv];
Goal "([] = map f xs) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed "Nil_is_map_conv";
AddIffs [Nil_is_map_conv];
Goal "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_eq_Cons";
@@ -411,7 +411,7 @@
by (induct_tac "xs" 1);
by (Force_tac 1);
by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Asm_simp_tac 1);
by (Force_tac 1);
qed_spec_mp "rev_is_rev_conv";
@@ -492,7 +492,7 @@
by (rtac iffI 1);
by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
by (REPEAT(etac exE 1));
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by Auto_tac;
qed "in_set_conv_decomp";
@@ -630,7 +630,7 @@
by (induct_tac "xs" 1);
by (Asm_simp_tac 1);
by (rtac allI 1);
- by (exhaust_tac "n" 1);
+ by (cases_tac "n" 1);
by Auto_tac;
qed_spec_mp "nth_append";
@@ -652,7 +652,7 @@
by (Simp_tac 1);
by (res_inst_tac [("x","Suc i")] exI 1);
by (Asm_simp_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by (Asm_full_simp_tac 1);
by (rename_tac "j" 1);
by (res_inst_tac [("x","j")] exI 1);
@@ -728,7 +728,7 @@
\ (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])";
by (induct_tac "ys" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (auto_tac (claset(), simpset() addsplits [nat.split]));
qed_spec_mp "update_zip";
@@ -813,7 +813,7 @@
Goal "!xs. length(take n xs) = min (length xs) n";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "length_take";
Addsimps [length_take];
@@ -821,7 +821,7 @@
Goal "!xs. length(drop n xs) = (length xs - n)";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "length_drop";
Addsimps [length_drop];
@@ -829,7 +829,7 @@
Goal "!xs. length xs <= n --> take n xs = xs";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "take_all";
Addsimps [take_all];
@@ -837,7 +837,7 @@
Goal "!xs. length xs <= n --> drop n xs = []";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "drop_all";
Addsimps [drop_all];
@@ -845,7 +845,7 @@
Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "take_append";
Addsimps [take_append];
@@ -853,7 +853,7 @@
Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "drop_append";
Addsimps [drop_append];
@@ -861,9 +861,9 @@
Goal "!xs n. take n (take m xs) = take (min n m) xs";
by (induct_tac "m" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
-by (exhaust_tac "na" 1);
+by (cases_tac "na" 1);
by Auto_tac;
qed_spec_mp "take_take";
Addsimps [take_take];
@@ -871,7 +871,7 @@
Goal "!xs. drop n (drop m xs) = drop (n + m) xs";
by (induct_tac "m" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "drop_drop";
Addsimps [drop_drop];
@@ -879,14 +879,14 @@
Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
by (induct_tac "m" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "take_drop";
Goal "!xs. take n xs @ drop n xs = xs";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "append_take_drop_id";
Addsimps [append_take_drop_id];
@@ -894,23 +894,23 @@
Goal "!xs. take n (map f xs) = map f (take n xs)";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "take_map";
Goal "!xs. drop n (map f xs) = map f (drop n xs)";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "drop_map";
Goal "!n i. i < n --> (take n xs)!i = xs!i";
by (induct_tac "xs" 1);
by Auto_tac;
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Blast_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by Auto_tac;
qed_spec_mp "nth_take";
Addsimps [nth_take];
@@ -918,7 +918,7 @@
Goal "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
by (induct_tac "n" 1);
by Auto_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed_spec_mp "nth_drop";
Addsimps [nth_drop];
@@ -930,7 +930,7 @@
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "zs" 1);
+by (cases_tac "zs" 1);
by (Auto_tac);
qed_spec_mp "append_eq_conv_conj";
@@ -993,7 +993,7 @@
by (induct_tac "ys" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "length_zip";
Addsimps [length_zip];
@@ -1004,7 +1004,7 @@
by (induct_tac "zs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed_spec_mp "zip_append1";
@@ -1015,7 +1015,7 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed_spec_mp "zip_append2";
@@ -1032,7 +1032,7 @@
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Auto_tac);
qed_spec_mp "zip_rev";
@@ -1042,7 +1042,7 @@
by (induct_tac "ys" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Auto_tac);
by (asm_full_simp_tac (simpset() addsimps (thms"nth.simps") addsplits [nat.split]) 1);
qed_spec_mp "nth_zip";
@@ -1061,7 +1061,7 @@
Goal "!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)";
by (induct_tac "i" 1);
by (Auto_tac);
-by (exhaust_tac "j" 1);
+by (cases_tac "j" 1);
by (Auto_tac);
qed "zip_replicate";
Addsimps [zip_replicate];
@@ -1091,13 +1091,13 @@
Goalw [list_all2_def]
"list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Auto_tac);
qed "list_all2_Cons1";
Goalw [list_all2_def]
"list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Auto_tac);
qed "list_all2_Cons2";
@@ -1249,8 +1249,8 @@
all_conj_distrib])));
by (Clarify_tac 1);
(*Both lists must be non-empty*)
-by (exhaust_tac "xs" 1);
-by (exhaust_tac "ys" 2);
+by (cases_tac "xs" 1);
+by (cases_tac "ys" 2);
by (ALLGOALS Clarify_tac);
(*prenexing's needed, not miniscoping*)
by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [sym])
@@ -1412,7 +1412,7 @@
by (rename_tac "a xys x xs' y ys'" 1);
by (res_inst_tac [("x","a#xys")] exI 1);
by (Simp_tac 1);
-by (exhaust_tac "xys" 1);
+by (cases_tac "xys" 1);
by (ALLGOALS (asm_full_simp_tac (simpset())));
by (Blast_tac 1);
qed "lexn_conv";
@@ -1452,7 +1452,7 @@
by (rtac iffI 1);
by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
by (REPEAT(eresolve_tac [conjE, exE] 1));
-by (exhaust_tac "xys" 1);
+by (cases_tac "xys" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
@@ -1467,19 +1467,19 @@
sum_eq_0_conv]);
Goal "take n (x#xs) = (if n = #0 then [] else x # take (n-#1) xs)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
qed "take_Cons'";
Goal "drop n (x#xs) = (if n = #0 then x#xs else drop (n-#1) xs)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
qed "drop_Cons'";
Goal "(x#xs)!n = (if n = #0 then x else xs!(n-#1))";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1])));
qed "nth_Cons'";