--- a/src/HOL/Arith.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Arith.ML Mon Mar 13 12:51:10 2000 +0100
@@ -106,24 +106,24 @@
(** Reasoning about m+0=0, etc. **)
Goal "(m+n = 0) = (m=0 & n=0)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (Auto_tac);
qed "add_is_0";
AddIffs [add_is_0];
Goal "(0 = m+n) = (m=0 & n=0)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (Auto_tac);
qed "zero_is_add";
AddIffs [zero_is_add];
Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (Auto_tac);
qed "add_is_1";
Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (Auto_tac);
qed "one_is_add";
@@ -134,7 +134,7 @@
(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
Goal "0<n ==> m + (n-1) = (m+n)-1";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
addsplits [nat.split])));
qed "add_pred";
@@ -404,7 +404,7 @@
Addsimps [Suc_diff_diff];
Goal "0<n ==> n - Suc i < n";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Safe_tac;
by (asm_simp_tac (simpset() addsimps le_simps) 1);
qed "diff_Suc_less";
@@ -1161,16 +1161,16 @@
(** Lemmas for ex/Factorization **)
Goal "[| 1<n; 1<m |] ==> 1<m*n";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by Auto_tac;
qed "one_less_mult";
Goal "[| 1<n; 1<m |] ==> n<m*n";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by Auto_tac;
qed "n_less_m_mult_n";
Goal "[| 1<n; 1<m |] ==> n<n*m";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by Auto_tac;
qed "n_less_n_mult_m";
--- a/src/HOL/BCV/DFAimpl.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/DFAimpl.ML Mon Mar 13 12:51:10 2000 +0100
@@ -60,7 +60,7 @@
by (Force_tac 2);
by (assume_tac 2);
by (assume_tac 2);
- by (exhaust_tac "xs!p" 1);
+ by (cases_tac "xs!p" 1);
by (asm_full_simp_tac (simpset() addsimps [list_update_le_conv]) 1);
by (asm_full_simp_tac (simpset() addsimps
[list_update_le_conv,listsn_optionE_in]) 1);
@@ -147,7 +147,7 @@
\ step p s = Some(t) & merges t (succs p) sos = sos))";
by (rtac iffI 1);
by (asm_simp_tac (simpset() addsimps [next_Some1]) 1);
-by (exhaust_tac "next step succs sos" 1);
+by (cases_tac "next step succs sos" 1);
by (best_tac (claset() addSDs [next_None] addss simpset()) 1);
by (rename_tac "sos'" 1);
by (case_tac "sos' = sos" 1);
@@ -172,7 +172,7 @@
\ step_pres_type step n A; succs_bounded succs n;\
\ sos : listsn n (option A) |] ==> \
\ next step succs sos : option (listsn n (option A))";
-by (exhaust_tac "next step succs sos" 1);
+by (cases_tac "next step succs sos" 1);
by (ALLGOALS Asm_simp_tac);
by (rename_tac "sos'" 1);
by (case_tac "sos' = sos" 1);
@@ -256,7 +256,7 @@
by (subgoal_tac
"!p<n. !s. sos!p = Some s --> (? u. \
\ step p s = Some(u) & (!q:set(succs p). Some u<=tos!q))" 1);
- by (exhaust_tac "next step succs sos" 1);
+ by (cases_tac "next step succs sos" 1);
by (dtac next_None 1);
by (assume_tac 1);
by (assume_tac 1);
@@ -279,12 +279,12 @@
by (blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1);
by (REPEAT(atac 1));
by (Clarify_tac 1);
-by (exhaust_tac "tos!p" 1);
+by (cases_tac "tos!p" 1);
by (force_tac (claset() addDs [le_listD],simpset()) 1);
by (rename_tac "t" 1);
by (subgoal_tac "s <= t" 1);
by (force_tac (claset() addDs [le_listD],simpset()) 2);
-by (exhaust_tac "step p s" 1);
+by (cases_tac "step p s" 1);
by (dtac step_mono_NoneD 1);
by (assume_tac 4);
by (blast_tac (claset() addIs [listsn_optionE_in]) 1);
--- a/src/HOL/BCV/Machine.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Machine.ML Mon Mar 13 12:51:10 2000 +0100
@@ -68,15 +68,15 @@
by (Blast_tac 2);
by (etac thin_rl 1);
by (asm_full_simp_tac (simpset() addsimps [le_typ])1);
-by (exhaust_tac "t!nat1" 1);
+by (cases_tac "t!nat1" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "s!nat1" 1);
+by (cases_tac "s!nat1" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "t!nat2" 1);
+by (cases_tac "t!nat2" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "exec_mono_None";
--- a/src/HOL/BCV/Orders.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Orders.ML Mon Mar 13 12:51:10 2000 +0100
@@ -37,7 +37,7 @@
by (case_tac "? a. Some a : Q" 1);
by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1);
by (Blast_tac 1);
-by (exhaust_tac "x" 1);
+by (cases_tac "x" 1);
by (Fast_tac 1);
by (Blast_tac 1);
qed "acc_option";
@@ -70,18 +70,18 @@
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "Cons_le_Cons";
AddIffs [Cons_le_Cons];
Goal "(x#xs <= ys) = (? z zs. ys = z#zs & x <= z & xs <= zs)";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (ALLGOALS Asm_simp_tac);
qed "Cons_le_iff";
Goal "(xs <= y#ys) = (? z zs. xs = z#zs & z <= y & zs <= ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "le_Cons_iff";
@@ -120,7 +120,7 @@
Goalw [listsn_def]
"(xs : listsn (Suc n) A) = (? y:A. ? ys:listsn n A. xs = y#ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Auto_tac);
qed "in_listsn_Suc_iff";
--- a/src/HOL/BCV/Orders0.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Orders0.ML Mon Mar 13 12:51:10 2000 +0100
@@ -58,11 +58,11 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (rtac allI 1);
-by (exhaust_tac "zs" 1);
+by (cases_tac "zs" 1);
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (hyp_subst_tac 1);
@@ -87,7 +87,7 @@
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (rtac allI 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (hyp_subst_tac 1);
by (Simp_tac 1);
by (hyp_subst_tac 1);
--- a/src/HOL/BCV/SemiLattice.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/SemiLattice.ML Mon Mar 13 12:51:10 2000 +0100
@@ -87,9 +87,9 @@
by (induct_tac "n" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Asm_full_simp_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
qed_spec_mp "nth_plus";
@@ -123,9 +123,9 @@
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (Asm_full_simp_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [semilat_plus]) 1);
--- a/src/HOL/BCV/Types0.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/BCV/Types0.ML Mon Mar 13 12:51:10 2000 +0100
@@ -23,7 +23,7 @@
Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}";
by (Auto_tac);
by (rename_tac "t" 1);
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
by (Auto_tac);
qed "UNIV_typ_enum";
--- a/src/HOL/Finite.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Finite.ML Mon Mar 13 12:51:10 2000 +0100
@@ -248,7 +248,7 @@
Goal "[| x ~: A; insert x A = {f i|i. i<n} |] \
\ ==> ? m::nat. m<n & (? g. A = {g i|i. i<m})";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
by (rename_tac "m" 1);
--- a/src/HOL/Hoare/Examples.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Hoare/Examples.ML Mon Mar 13 12:51:10 2000 +0100
@@ -50,7 +50,7 @@
\ OD \
\ {c = A^B}";
by (hoare_tac (Asm_full_simp_tac) 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mult_assoc]) 1);
@@ -67,7 +67,7 @@
\ {b = fac A}";
by (hoare_tac Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
--- a/src/HOL/IMP/Transition.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/IMP/Transition.ML Mon Mar 13 12:51:10 2000 +0100
@@ -220,7 +220,7 @@
by (Clarify_tac 1);
by (etac rel_pow_E2 1);
by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
-by (exhaust_tac "c" 1);
+by (cases_tac "c" 1);
by (fast_tac (claset() addSDs [hlemma]) 1);
by (Blast_tac 1);
by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
--- a/src/HOL/IOA/IOA.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/IOA/IOA.ML Mon Mar 13 12:51:10 2000 +0100
@@ -30,7 +30,7 @@
Goal "filter_oseq p (filter_oseq p s) = filter_oseq p s";
by (simp_tac (simpset() addsimps [filter_oseq_def]) 1);
by (rtac ext 1);
- by (exhaust_tac "s(i)" 1);
+ by (cases_tac "s(i)" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "filter_oseq_idemp";
@@ -41,7 +41,7 @@
\ & \
\ (mk_trace A s n = Some(a)) = \
\ (s(n)=Some(a) & a : externals(asig_of(A)))";
- by (exhaust_tac "s(n)" 1);
+ by (cases_tac "s(n)" 1);
by (ALLGOALS Asm_simp_tac);
by (Fast_tac 1);
qed "mk_trace_thm";
@@ -86,7 +86,7 @@
by (induct_tac "n" 1);
by (fast_tac (claset() addIs [p1,reachable_0]) 1);
by (eres_inst_tac[("x","na")] allE 1);
- by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
+ by (cases_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
by Safe_tac;
by (etac (p2 RS mp) 1);
by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
--- a/src/HOL/Induct/LList.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Induct/LList.ML Mon Mar 13 12:51:10 2000 +0100
@@ -76,7 +76,7 @@
"LList_corec a f <= \
\ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
by (rtac UN_least 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono,
UNIV_I RS UN_upper] 1));
@@ -132,10 +132,10 @@
by (safe_tac (claset() delrules [equalityI]));
by (etac LListD.elim 1);
by (safe_tac (claset() delrules [equalityI]));
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Asm_simp_tac 1);
by (rename_tac "n'" 1);
-by (exhaust_tac "n'" 1);
+by (cases_tac "n'" 1);
by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
qed "LListD_implies_ntrunc_equality";
@@ -295,9 +295,9 @@
by (stac prem2 1);
by (Simp_tac 1);
by (strip_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (rename_tac "m" 2);
-by (exhaust_tac "m" 2);
+by (cases_tac "m" 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
result();
@@ -598,7 +598,7 @@
"llist_corec a f = \
\ (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
by (stac LList_corec 1);
-by (exhaust_tac "f a" 1);
+by (cases_tac "f a" 1);
by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
qed "llist_corec";
--- a/src/HOL/Integ/Int.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Integ/Int.ML Mon Mar 13 12:51:10 2000 +0100
@@ -90,7 +90,7 @@
by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
by (cut_inst_tac [("m","n")] int_Suc_int_1 1);
by (Asm_full_simp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
by (full_simp_tac (simpset() addsimps zadd_ac) 1);
--- a/src/HOL/Integ/NatBin.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Integ/NatBin.ML Mon Mar 13 12:51:10 2000 +0100
@@ -319,17 +319,17 @@
(* These two can be useful when m = number_of... *)
Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "add_eq_if";
Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "mult_eq_if";
Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (ALLGOALS (asm_simp_tac numeral_ss));
qed "power_eq_if";
--- a/src/HOL/Lambda/Eta.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/Eta.ML Mon Mar 13 12:51:10 2000 +0100
@@ -166,7 +166,7 @@
by (rtac notE 1);
by (assume_tac 2);
by (etac thin_rl 1);
- by (exhaust_tac "t" 1);
+ by (cases_tac "t" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
@@ -181,7 +181,7 @@
by (Asm_simp_tac 1);
by (etac exE 1);
by (etac rev_mp 1);
- by (exhaust_tac "t" 1);
+ by (cases_tac "t" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
@@ -195,7 +195,7 @@
by (Asm_simp_tac 1);
by (etac exE 1);
by (etac rev_mp 1);
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
--- a/src/HOL/Lambda/InductTermi.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/InductTermi.ML Mon Mar 13 12:51:10 2000 +0100
@@ -86,7 +86,7 @@
by (eres_inst_tac [("x","Var n $$ us")] allE 1);
by (Force_tac 1);
by (rename_tac "u ts" 1);
-by (exhaust_tac "ts" 1);
+by (cases_tac "ts" 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs IT.intrs) 1);
by (rename_tac "s ss" 1);
--- a/src/HOL/Lambda/ListBeta.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/ListBeta.ML Mon Mar 13 12:51:10 2000 +0100
@@ -29,7 +29,7 @@
\ (? s t ts. r = Abs s & rs = t#ts & u' = s[t/0]$$ts))";
by (etac beta.induct 1);
by (clarify_tac (claset() delrules [disjCI]) 1);
- by (exhaust_tac "r" 1);
+ by (cases_tac "r" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [App_eq_foldl_conv]) 1);
by (split_asm_tac [split_if_asm] 1);
--- a/src/HOL/Lambda/ListOrder.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lambda/ListOrder.ML Mon Mar 13 12:51:10 2000 +0100
@@ -30,7 +30,7 @@
by (rtac iffI 1);
by (etac exE 1);
by (rename_tac "ts" 1);
- by (exhaust_tac "ts" 1);
+ by (cases_tac "ts" 1);
by (Force_tac 1);
by (Force_tac 1);
by (etac disjE 1);
@@ -51,7 +51,7 @@
\ !y. ys = y#xs --> (y,x) : r --> R; \
\ !zs. ys = x#zs --> (zs,xs) : step1 r --> R \
\ |] ==> R";
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (asm_full_simp_tac (simpset() addsimps [step1_def]) 1);
by (Blast_tac 1);
val lemma = result();
--- a/src/HOL/Lex/MaxPrefix.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/MaxPrefix.ML Mon Mar 13 12:51:10 2000 +0100
@@ -26,7 +26,7 @@
by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
by (Asm_simp_tac 1);
by (Clarify_tac 1);
- by (exhaust_tac "us" 1);
+ by (cases_tac "us" 1);
by (rtac iffI 1);
by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
by (Blast_tac 1);
--- a/src/HOL/Lex/NAe.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/NAe.ML Mon Mar 13 12:51:10 2000 +0100
@@ -5,7 +5,7 @@
*)
Goal "steps A w O (eps A)^* = steps A w";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
qed_spec_mp "steps_epsclosure";
Addsimps [steps_epsclosure];
--- a/src/HOL/Lex/Prefix.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/Prefix.ML Mon Mar 13 12:51:10 2000 +0100
@@ -76,7 +76,7 @@
Goalw [prefix_def]
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed "prefix_Cons";
@@ -92,7 +92,7 @@
Goalw [prefix_def]
"[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
by (auto_tac(claset(), simpset() addsimps [nth_append]));
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by Auto_tac;
qed "append_one_prefix";
--- a/src/HOL/Lex/RegExp2NA.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML Mon Mar 13 12:51:10 2000 +0100
@@ -112,7 +112,7 @@
\ ( (w = [] & q = start(union L R)) | \
\ (w ~= [] & (? p. q = True # p & (start L,p) : steps L w | \
\ q = False # p & (start R,p) : steps R w)))";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
by (Asm_simp_tac 1);
@@ -273,7 +273,7 @@
by (Simp_tac 1);
by (Blast_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
by (Asm_full_simp_tac 1);
@@ -336,7 +336,7 @@
Goal
"[| (start A,q) : steps A u; u ~= []; fin A p |] \
\ ==> (p,q) : steps (plus A) u";
-by (exhaust_tac "u" 1);
+by (cases_tac "u" 1);
by (Blast_tac 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addIs [steps_plusI]) 1);
@@ -360,7 +360,7 @@
by (res_inst_tac [("x","us")] exI 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
by (res_inst_tac [("x","us")] exI 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","us@[v]")] exI 1);
--- a/src/HOL/Lex/RegExp2NAe.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegExp2NAe.ML Mon Mar 13 12:51:10 2000 +0100
@@ -191,7 +191,7 @@
\ ( (w = [] & q = start(union L R)) | \
\ (? p. q = True # p & (start L,p) : steps L w | \
\ q = False # p & (start R,p) : steps R w) )";
-by (exhaust_tac "w" 1);
+by (cases_tac "w" 1);
by (Asm_simp_tac 1);
by (Blast_tac 1);
by (Asm_simp_tac 1);
@@ -568,7 +568,7 @@
"(start(star A),r) : steps (star A) w = \
\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
by (rtac iffI 1);
- by (exhaust_tac "w" 1);
+ by (cases_tac "w" 1);
by (asm_full_simp_tac (simpset() addsimps
[epsclosure_start_step_star]) 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML Mon Mar 13 12:51:10 2000 +0100
@@ -11,7 +11,7 @@
(* Lists *)
Goal "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "butlast_empty";
AddIffs [butlast_empty];
@@ -103,14 +103,14 @@
Addsimps [trace_concat];
Goal "!i. (trace d i xs = []) = (xs = [])";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "trace_is_Nil";
Addsimps [trace_is_Nil];
Goal "(trace d i xs = n#ns) = \
\ (case xs of [] => False | y#ys => n = d y i & ns = trace d n ys)";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed_spec_mp "trace_is_Cons_conv";
--- 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'";
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Mar 13 12:51:10 2000 +0100
@@ -68,7 +68,7 @@
be widen.induct 1;
by(Auto_tac);
by(rename_tac "R" 1);
-by(exhaust_tac "R" 1);
+by(cases_tac "R" 1);
by(Auto_tac);
val lemma = result();
@@ -100,7 +100,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "ls_com" 1);
+by (cases_tac "ls_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
qed "LS_correct";
@@ -119,7 +119,7 @@
by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
by (ALLGOALS (fast_tac (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
qed "Cast_conf2";
@@ -149,7 +149,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "ch_com" 1);
+by (cases_tac "ch_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
qed "CH_correct";
@@ -223,7 +223,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "mo_com" 1);
+by (cases_tac "mo_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
qed "MO_correct";
@@ -263,7 +263,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "co_com" 1);
+by (cases_tac "co_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
qed "CO_correct";
@@ -282,7 +282,7 @@
by(etac exE 1);
by(asm_full_simp_tac (simpset() addsimps defs1) 1);
by(Clarify_tac 1);
-by(exhaust_tac "X\\<noteq>NT" 1);
+by(case_tac "X\\<noteq>NT" 1);
by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1
addsplits [option.split]) 1);
by (Clarify_tac 1);
@@ -360,7 +360,7 @@
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
-by (exhaust_tac "mi_com" 1);
+by (cases_tac "mi_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
qed "MI_correct";
@@ -401,7 +401,7 @@
by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
ba 1;
ba 1;
-by (exhaust_tac "mr" 1);
+by (cases_tac "mr" 1);
by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
qed "MR_correct";
@@ -442,7 +442,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "br_com" 1);
+by (cases_tac "br_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
qed "BR_correct";
@@ -521,7 +521,7 @@
ba 1;
ba 1;
by(rewtac wt_jvm_prog_def);
-by (exhaust_tac "os_com" 1);
+by (cases_tac "os_com" 1);
by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct])));
qed "OS_correct";
@@ -539,15 +539,15 @@
\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by(split_all_tac 1);
by(rename_tac "xp hp frs" 1);
-by (exhaust_tac "xp" 1);
- by (exhaust_tac "frs" 1);
+by (cases_tac "xp" 1);
+ by (cases_tac "frs" 1);
by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
by(split_all_tac 1);
by(hyp_subst_tac 1);
by(forward_tac [correct_state_impl_Some_method] 1);
by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
BR_correct], simpset() addsplits [split_if_asm,instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
-by (exhaust_tac "frs" 1);
+by (cases_tac "frs" 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.rules)));
qed_spec_mp "BV_correct_1";
--- a/src/HOL/MicroJava/BV/Convert.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML Mon Mar 13 12:51:10 2000 +0100
@@ -6,7 +6,7 @@
Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
-by (exhaust_tac "t" 1);
+by (cases_tac "t" 1);
by Auto_tac;
qed "sup_ty_opt_refl";
Addsimps [sup_ty_opt_refl];
@@ -66,7 +66,7 @@
by (induct_tac "a" 1);
by (Simp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","nat")] allE 1);
by (smp_tac 1 1);
@@ -89,7 +89,7 @@
by (induct_tac "a" 1);
by (Clarsimp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
qed_spec_mp "sup_loc_append";
@@ -112,7 +112,7 @@
by (Clarsimp_tac 1);
by Safe_tac;
by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 2);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
bd sup_loc_length 1;
by (Clarsimp_tac 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 1);
@@ -129,7 +129,7 @@
qed "sup_state_rev_fst";
Goal "map x a = Y # YT \\<longrightarrow> map x (tl a) = YT \\<and> x (hd a) = Y \\<and> (\\<exists> y yt. a = y#yt)";
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
by Auto_tac;
qed_spec_mp "map_hd_tl";
@@ -159,15 +159,15 @@
Goalw[sup_ty_opt_def]
"\\<lbrakk>G \\<turnstile> a <=o b; G \\<turnstile> b <=o c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=o c";
-by (exhaust_tac "c" 1);
+by (cases_tac "c" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
by (Clarsimp_tac 1);
- by (exhaust_tac "b" 1);
+ by (cases_tac "b" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
be widen_trans 1;
@@ -190,7 +190,7 @@
by (induct_tac "a" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "b=[]" 1);
+by (case_tac "b=[]" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
@@ -230,7 +230,7 @@
qed "sup_state_trans";
Goalw[sup_ty_opt_def] "G \\<turnstile> a <=o Some b \\<Longrightarrow> \\<exists> x. a = Some x";
-by (exhaust_tac "a" 1);
+by (cases_tac "a" 1);
by Auto_tac;
qed "sup_ty_opt_some";
@@ -240,7 +240,7 @@
by (induct_tac "x" 1);
by (Simp_tac 1);
by (clarsimp_tac ((claset(), simpset()) addIffs [sup_loc_Cons2]) 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
qed_spec_mp "sup_loc_update";
--- a/src/HOL/MicroJava/BV/Correct.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML Mon Mar 13 12:51:10 2000 +0100
@@ -40,7 +40,7 @@
Goal
"\\<lbrakk> wf_prog wt G \\<rbrakk> \
\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
-by (exhaust_tac "T" 1);
+by (cases_tac "T" 1);
by (Asm_simp_tac 1);
by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
qed_spec_mp "approx_val_imp_approx_val_assConvertible";
@@ -56,7 +56,7 @@
Goal
"\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
\\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
-by (exhaust_tac "v" 1);
+by (cases_tac "v" 1);
by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
qed_spec_mp "approx_val_imp_approx_val_heap_update";
@@ -97,7 +97,7 @@
Goalw [approx_loc_def,list_all2_def]
"\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
-by (exhaust_tac "lt" 1);
+by (cases_tac "lt" 1);
by (Asm_simp_tac 1);
by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
simpset() addsimps [neq_Nil_conv]) 1);
--- a/src/HOL/MicroJava/BV/LBVComplete.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.ML Mon Mar 13 12:51:10 2000 +0100
@@ -7,14 +7,14 @@
by (induct_tac "a" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "P n" 1);
+by (case_tac "P n" 1);
by (Clarsimp_tac 1);
- by (exhaust_tac "na" 1);
+ by (cases_tac "na" 1);
by (Clarsimp_tac 1);
by (clarsimp_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
by (Force_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "na" 1);
+by (cases_tac "na" 1);
by (Clarsimp_tac 1);
by (force_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
qed_spec_mp "is_approx_option_filter_n";
@@ -28,7 +28,7 @@
by (induct_tac "l" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
qed_spec_mp "option_filter_n_Some";
@@ -90,7 +90,7 @@
by (induct_tac "x" 1);
by (Simp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
by (smp_tac 1 1);
@@ -114,13 +114,13 @@
Goal "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
-by (exhaust_tac "b" 1);
- by (exhaust_tac "ref_ty" 2);
+by (cases_tac "b" 1);
+ by (cases_tac "ref_ty" 2);
by Auto_tac;
qed "widen_NT";
Goal "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
by Auto_tac;
qed "widen_Class";
@@ -129,7 +129,7 @@
by (induct_tac "a" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "b" 1);
+by (cases_tac "b" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
qed_spec_mp "all_widen_is_sup_loc";
@@ -139,7 +139,7 @@
\ G \\<turnstile> (x, y) <=s s1; wtl_inst i G rT s1 s1' cert mpc pc\\<rbrakk> \
\ \\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
\ ((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))";
-by (exhaust_tac "meth_inv" 1);
+by (cases_tac "meth_inv" 1);
by (Clarsimp_tac 1);
by (cut_inst_tac [("x","x"),("n","length apTs")] rev_append_cons 1);
by (asm_full_simp_tac (simpset() addsimps [sup_state_length_fst]) 1);
@@ -150,7 +150,7 @@
back();
back();
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_rev_fst,sup_state_Cons1]) 1);
-by (exhaust_tac "X = NT" 1);
+by (case_tac "X = NT" 1);
by (Clarsimp_tac 1);
by (res_inst_tac [("x","a")] exI 1);
by (res_inst_tac [("x","b")] exI 1);
@@ -161,7 +161,7 @@
by (strip_tac1 1);
by (forward_tac [widen_Class] 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "r" 1);
+by (cases_tac "r" 1);
by (Clarsimp_tac 1);
by (res_inst_tac [("x","a")] exI 1);
by (res_inst_tac [("x","b")] exI 1);
@@ -198,7 +198,7 @@
by (induct_tac "b" 1);
by (Simp_tac 1);
by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (asm_full_simp_tac (simpset() addsimps [sup_ty_opt_some]) 1);
by (smp_tac 1 1);
by (Asm_full_simp_tac 1);
@@ -224,7 +224,7 @@
Goal "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
by Safe_tac;
-by (exhaust_tac "xb" 1);
+by (cases_tac "xb" 1);
by Auto_tac;
bd widen_RefT 1;
by Auto_tac;
@@ -237,8 +237,8 @@
\ (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
by (cut_inst_tac [("z","s2")] surj_pair 1);
by (Clarify_tac 1);
-by (exhaust_tac "ins!pc" 1);
- by (exhaust_tac "load_and_store" 1);
+by (cases_tac "ins!pc" 1);
+ by (cases_tac "load_and_store" 1);
by (Clarsimp_tac 1);
by (datac mono_load 2 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_length_snd]) 1);
@@ -247,9 +247,9 @@
by (Clarsimp_tac 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1);
- by (exhaust_tac "create_object" 1);
+ by (cases_tac "create_object" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1);
- by (exhaust_tac "manipulate_object" 1);
+ by (cases_tac "manipulate_object" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
be widen_trans 1;
ba 1;
@@ -259,7 +259,7 @@
ba 1;
be widen_trans 1;
ba 1;
- by (exhaust_tac "check_object" 1);
+ by (cases_tac "check_object" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
be widen_RefT2 1;
br method_inv_pseudo_mono 1;
@@ -270,7 +270,7 @@
ba 1;
ba 1;
ba 1;
- by (exhaust_tac "meth_ret" 1);
+ by (cases_tac "meth_ret" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
br conjI 1;
be widen_trans 1;
@@ -278,13 +278,13 @@
by (cut_inst_tac [("z","s1'")] surj_pair 1);
by (strip_tac1 1);
by (Clarsimp_tac 1);
- by (exhaust_tac "op_stack" 1);
+ by (cases_tac "op_stack" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
-by (exhaust_tac "branch" 1);
+by (cases_tac "branch" 1);
by (Clarsimp_tac 1);
bd sup_state_trans 1;
ba 1;
@@ -298,10 +298,10 @@
ba 2;
ba 2;
by (Clarsimp_tac 1);
-by (exhaust_tac "xa" 1);
+by (cases_tac "xa" 1);
by (clarsimp_tac (claset(), simpset() addsimps [PrimT_PrimT]) 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "xb" 1);
+by (cases_tac "xb" 1);
by Auto_tac;
bd widen_RefT 1;
by Auto_tac;
@@ -310,15 +310,15 @@
Goal "\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
\ \\<exists>s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
-by (exhaust_tac "i" 1);
-by (exhaust_tac "branch" 8);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "meth_ret" 6);
-by (exhaust_tac "meth_inv" 5);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+by (cases_tac "branch" 8);
+by (cases_tac "op_stack" 7);
+by (cases_tac "meth_ret" 6);
+by (cases_tac "meth_inv" 5);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
by (TRYALL Asm_full_simp_tac);
by (pair_tac "s1'" 1);
by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
@@ -335,7 +335,7 @@
Goalw [wtl_inst_option_def]
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; Suc pc = mpc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow> \
\ \\<exists>s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
by (Clarsimp_tac 1);
bd wtl_inst_last_mono 1;
ba 1;
@@ -355,18 +355,18 @@
\ \\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
by (cut_inst_tac [("z","phi!pc")] surj_pair 1);
by (strip_tac1 1);
-by (exhaust_tac "ins!pc" 1);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "ins!pc" 1);
+by (cases_tac "op_stack" 7);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
by (TRYALL (Asm_full_simp_tac THEN_MAYBE' Force_tac));
- by (exhaust_tac "meth_inv" 1);
+ by (cases_tac "meth_inv" 1);
by (cut_inst_tac [("z","phi!(Suc pc)")] surj_pair 1);
by (strip_tac1 1);
by (Clarsimp_tac 1);
- by (exhaust_tac "X = NT" 1);
+ by (case_tac "X = NT" 1);
by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
by (smp_tac 1 1);
by (Clarsimp_tac 1);
@@ -378,12 +378,12 @@
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","apTs")] exI 1);
by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
- by (exhaust_tac "meth_ret" 1);
+ by (cases_tac "meth_ret" 1);
by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def]) 1);
by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
by (strip_tac1 1);
by (Clarsimp_tac 1);
-by (exhaust_tac "branch" 1);
+by (cases_tac "branch" 1);
by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def, contains_targets_def]) 1);
by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
by (Force_tac 1);
@@ -395,7 +395,7 @@
"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; \
\ max_pc = length ins\\<rbrakk> \\<Longrightarrow> \
\ \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
by (Clarsimp_tac 1);
bd wt_instr_imp_wtl_inst 1;
ba 1;
@@ -417,14 +417,14 @@
\ ins \\<noteq> []; G \\<turnstile> s <=s s0; \
\ s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \
\ wtl_inst_list ins G rT s s' cert max_pc pc";
-by (exhaust_tac "ins" 1);
+by (cases_tac "ins" 1);
by (Clarify_tac 1);
by (Clarify_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "list = []" 1);
+by (case_tac "list = []" 1);
by (Asm_full_simp_tac 1);
- by (exhaust_tac "s = s0" 1);
+ by (case_tac "s = s0" 1);
by (Force_tac 1);
by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
@@ -434,7 +434,7 @@
Goal "\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; \
\ ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \
\ wtl_inst_list ins G rT s s' cert max_pc pc";
-by (exhaust_tac "ins" 1);
+by (cases_tac "ins" 1);
by (Clarify_tac 1);
by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
qed "wtl_inst_list_cert";
@@ -446,7 +446,7 @@
\ G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow> \
\ \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> \
\ (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
by (Asm_full_simp_tac 1);
by (datac wtl_inst_pseudo_mono 4 1);
by (Clarsimp_tac 1);
@@ -495,7 +495,7 @@
by (Simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
by (Clarify_tac 1);
-by (exhaust_tac "list = []" 1);
+by (case_tac "list = []" 1);
by (Clarsimp_tac 1);
bd wtl_option_last_mono 1;
br refl 1;
@@ -512,7 +512,7 @@
ba 1;
by (simp_tac (simpset() addsimps [append_cons_length_nth]) 1);
by (clarsimp_tac (claset(), simpset() addsimps [append_cons_length_nth]) 1);
-by (exhaust_tac "cert ! Suc (length l)" 1);
+by (cases_tac "cert ! Suc (length l)" 1);
by (Clarsimp_tac 1);
by (dres_inst_tac [("a","(ac,bb)")] sup_state_trans 1);
ba 1;
@@ -529,7 +529,7 @@
by (clarsimp_tac (claset(), simpset() addsimps [fits_def, is_approx_def]) 1);
by (eres_inst_tac [("x","Suc (length l)")] allE 1);
be impE 1;
- by (exhaust_tac "length list" 1);
+ by (cases_tac "length list" 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
by (Clarsimp_tac 1);
--- a/src/HOL/MicroJava/BV/LBVCorrect.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.ML Mon Mar 13 12:51:10 2000 +0100
@@ -25,11 +25,11 @@
by (eres_inst_tac [("x","Suc pc")] allE 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "cert ! pc" 1);
+by (cases_tac "cert ! pc" 1);
by (res_inst_tac [("x","phi[pc:=(aa, b)]")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
by (Clarify_tac 1);
- by (exhaust_tac "ac" 1);
+ by (cases_tac "ac" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
@@ -46,7 +46,7 @@
by (res_inst_tac [("x","phi[pc:=ac]")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
by (Clarify_tac 1);
-by (exhaust_tac "ad" 1);
+by (cases_tac "ad" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
@@ -94,13 +94,13 @@
by (forward_tac [wtl_append] 1);
ba 1;
ba 1;
-by (exhaust_tac "b=[]" 1);
+by (case_tac "b=[]" 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
by (Clarify_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
-by (exhaust_tac "cert!(Suc (length a))" 1);
+by (cases_tac "cert!(Suc (length a))" 1);
by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
by (eres_inst_tac [("x","a@[i]")] allE 1);
by (eres_inst_tac [("x","ys")] allE 1);
@@ -161,46 +161,46 @@
by (TRYALL atac);
by (forward_tac [fits_lemma1] 1);
ba 1;
-by (exhaust_tac "cert!(length i1)" 1);
+by (cases_tac "cert!(length i1)" 1);
by (forward_tac [fits_lemma2] 1);
by (TRYALL atac);
- by (exhaust_tac "i" 1);
- by (exhaust_tac "check_object" 4);
- by (exhaust_tac "manipulate_object" 3);
- by (exhaust_tac "create_object" 2);
- by (exhaust_tac "load_and_store" 1);
+ by (cases_tac "i" 1);
+ by (cases_tac "check_object" 4);
+ by (cases_tac "manipulate_object" 3);
+ by (cases_tac "create_object" 2);
+ by (cases_tac "load_and_store" 1);
by (GOALS (force_tac (claset(),
simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
- by (exhaust_tac "meth_inv" 1);
+ by (cases_tac "meth_inv" 1);
by (thin_tac "\\<forall>pc t.\
\ pc < length (i1 @ i # i2) \\<longrightarrow> \
\ cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
by (pair_tac "s1" 1);
by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
by (Force_tac 1);
- by (exhaust_tac "meth_ret" 1);
+ by (cases_tac "meth_ret" 1);
by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
- by (exhaust_tac "branch" 2);
- by (exhaust_tac "op_stack" 1);
+ by (cases_tac "branch" 2);
+ by (cases_tac "op_stack" 1);
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
THEN_MAYBE' Force_tac) 1 7);
by (forw_inst_tac [("x","length i1")] spec 1);
by (eres_inst_tac [("x","a")] allE 1);
-by (exhaust_tac "i" 1);
- by (exhaust_tac "check_object" 4);
- by (exhaust_tac "manipulate_object" 3);
- by (exhaust_tac "create_object" 2);
- by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+ by (cases_tac "check_object" 4);
+ by (cases_tac "manipulate_object" 3);
+ by (cases_tac "create_object" 2);
+ by (cases_tac "load_and_store" 1);
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
THEN' Force_tac) 1 8);
- by (exhaust_tac "meth_inv" 1);
+ by (cases_tac "meth_inv" 1);
by (thin_tac "\\<forall>pc t.\
\ pc < length (i1 @ i # i2) \\<longrightarrow> \
\ cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
by (force_tac (claset(), simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
- by (exhaust_tac "branch" 3);
- by (exhaust_tac "op_stack" 2);
- by (exhaust_tac "meth_ret" 1);
+ by (cases_tac "branch" 3);
+ by (cases_tac "op_stack" 2);
+ by (cases_tac "meth_ret" 1);
by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def])
THEN_MAYBE' Force_tac) 1 8);
qed "wtl_lemma";
@@ -242,7 +242,7 @@
by (Asm_full_simp_tac 1);
be impE 1;
by (Force_tac 1);
-by (exhaust_tac "cert ! 0" 1);
+by (cases_tac "cert ! 0" 1);
by (auto_tac (claset(), simpset() addsimps [wtl_inst_option_def]));
qed "fits_first";
--- a/src/HOL/MicroJava/BV/LBVSpec.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.ML Mon Mar 13 12:51:10 2000 +0100
@@ -11,15 +11,15 @@
Goal "\\<lbrakk>wtl_inst i G rT s0 s1 cert max_pc pc; \
\ wtl_inst i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
-by (exhaust_tac "i" 1);
-by (exhaust_tac "branch" 8);
-by (exhaust_tac "op_stack" 7);
-by (exhaust_tac "meth_ret" 6);
-by (exhaust_tac "meth_inv" 5);
-by (exhaust_tac "check_object" 4);
-by (exhaust_tac "manipulate_object" 3);
-by (exhaust_tac "create_object" 2);
-by (exhaust_tac "load_and_store" 1);
+by (cases_tac "i" 1);
+by (cases_tac "branch" 8);
+by (cases_tac "op_stack" 7);
+by (cases_tac "meth_ret" 6);
+by (cases_tac "meth_inv" 5);
+by (cases_tac "check_object" 4);
+by (cases_tac "manipulate_object" 3);
+by (cases_tac "create_object" 2);
+by (cases_tac "load_and_store" 1);
by Auto_tac;
by (ALLGOALS (dtac rev_eq));
by (TRYALL atac);
@@ -29,7 +29,7 @@
Goal "\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; \
\ wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
-by (exhaust_tac "cert!pc" 1);
+by (cases_tac "cert!pc" 1);
by (auto_tac (claset(), simpset() addsimps [wtl_inst_unique, wtl_inst_option_def]));
qed "wtl_inst_option_unique";
@@ -49,12 +49,12 @@
\ wtl_inst_list b G rT s1 s' cert mpc (pc+length a))";
by(induct_tac "is" 1);
by Auto_tac;
-by (exhaust_tac "pc'" 1);
+by (cases_tac "pc'" 1);
by (dres_inst_tac [("x","pc'")] spec 1);
by (smp_tac 3 1);
by (res_inst_tac [("x","[]")] exI 1);
by (Asm_full_simp_tac 1);
- by (exhaust_tac "cert!pc" 1);
+ by (cases_tac "cert!pc" 1);
by (Force_tac 1);
by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
by (dres_inst_tac [("x","nat")] spec 1);
--- a/src/HOL/MicroJava/J/JBasis.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML Mon Mar 13 12:51:10 2000 +0100
@@ -83,7 +83,7 @@
eresolve_tac prems 1]);
fun option_case_tac2 s i = EVERY [
- exhaust_tac s i,
+ cases_tac s i,
rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Mon Mar 13 12:51:10 2000 +0100
@@ -284,7 +284,7 @@
(* Level 45 *)
(* 1 Call *)
-by( exhaust_tac "x" 1);
+by( cases_tac "x" 1);
by( Clarsimp_tac 2);
by( dtac exec_xcpt 2);
by( Asm_full_simp_tac 2);
--- a/src/HOL/MicroJava/J/Type.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/MicroJava/J/Type.ML Mon Mar 13 12:51:10 2000 +0100
@@ -5,6 +5,6 @@
*)
Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
-by(exhaust_tac "T" 1);
+by(cases_tac "T" 1);
by Auto_tac;
qed "non_PrimT";
--- a/src/HOL/Nat.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Nat.ML Mon Mar 13 12:51:10 2000 +0100
@@ -22,23 +22,23 @@
val [nat_case_0, nat_case_Suc] = nat.cases;
Goal "n ~= 0 ==> EX m. n = Suc m";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (REPEAT (Blast_tac 1));
qed "not0_implies_Suc";
Goal "m<n ==> n ~= 0";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "gr_implies_not0";
Goal "(n ~= 0) = (0 < n)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
qed "neq0_conv";
AddIffs [neq0_conv];
Goal "(0 ~= n) = (0 < n)";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
qed "zero_neq_conv";
AddIffs [zero_neq_conv];
@@ -64,7 +64,7 @@
(*Useful in certain inductive arguments*)
Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by Auto_tac;
qed "less_Suc_eq_0_disj";
@@ -74,11 +74,11 @@
by (fold_goals_tac [Least_nat_def]);
by (safe_tac (claset() addSEs [LeastI]));
by (rename_tac "j" 1);
-by (exhaust_tac "j" 1);
+by (cases_tac "j" 1);
by (Blast_tac 1);
by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
by (rename_tac "k n" 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by (Blast_tac 1);
by (hyp_subst_tac 1);
by (rewtac Least_nat_def);
@@ -90,8 +90,8 @@
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
by (rtac less_induct 1);
-by (exhaust_tac "n" 1);
-by (exhaust_tac "nat" 2);
+by (cases_tac "n" 1);
+by (cases_tac "nat" 2);
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
qed "nat_induct2";
--- a/src/HOL/Option.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Option.ML Mon Mar 13 12:51:10 2000 +0100
@@ -82,13 +82,13 @@
Goal "x : o2s xo = (xo = Some x)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
by Auto_tac;
qed "elem_o2s";
AddIffs [elem_o2s];
Goal "(o2s xo = {}) = (xo = None)";
-by (exhaust_tac "xo" 1);
+by (cases_tac "xo" 1);
by Auto_tac;
qed "o2s_empty_eq";
--- a/src/HOL/Power.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Power.ML Mon Mar 13 12:51:10 2000 +0100
@@ -48,7 +48,7 @@
(*** Binomial Coefficients, following Andy Gordon and Florian Kammueller ***)
Goal "(n choose 0) = 1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (ALLGOALS Asm_simp_tac);
qed "binomial_n_0";
@@ -99,7 +99,7 @@
by (induct_tac "n" 1);
by (simp_tac (simpset() addsimps [binomial_0]) 1);
by (Clarify_tac 1);
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by (auto_tac (claset(),
simpset() addsimps [add_mult_distrib, add_mult_distrib2,
le_Suc_eq, binomial_eq_0]));
--- a/src/HOL/Real/RealPow.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Mon Mar 13 12:51:10 2000 +0100
@@ -234,7 +234,7 @@
qed_spec_mp "realpow_Suc_le";
Goal "0r <= 0r ^ n";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (Auto_tac);
qed "realpow_zero_le";
Addsimps [realpow_zero_le];
--- a/src/HOL/RelPow.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/RelPow.ML Mon Mar 13 12:51:10 2000 +0100
@@ -43,7 +43,7 @@
\ !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P \
\ |] ==> P";
by (cut_facts_tac [p1] 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
by (Asm_full_simp_tac 1);
by (etac compEpair 1);
@@ -70,7 +70,7 @@
\ !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P \
\ |] ==> P";
by (cut_facts_tac [p1] 1);
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
by (Asm_full_simp_tac 1);
by (etac compEpair 1);
--- a/src/HOL/TLA/Inc/Inc.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML Mon Mar 13 12:51:10 2000 +0100
@@ -165,7 +165,7 @@
(fn _ => [auto_tac (Inc_css addsimps2 Init_defs
addSIs2 [(temp_use N2_leadsto_a)
RSN(2, (temp_use leadsto_init))]),
- exhaust_tac "pc2 (st1 sigma)" 1,
+ cases_tac "pc2 (st1 sigma)" 1,
Auto_tac
]);
@@ -212,7 +212,7 @@
(fn _ => [auto_tac (Inc_css addsimps2 Init_defs
addSIs2 [(temp_use N1_leadsto_b)
RSN(2, temp_use leadsto_init)]),
- exhaust_tac "pc1 (st1 sigma)" 1,
+ cases_tac "pc1 (st1 sigma)" 1,
Auto_tac
]);
--- a/src/HOL/TLA/Memory/Memory.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/TLA/Memory/Memory.ML Mon Mar 13 12:51:10 2000 +0100
@@ -123,7 +123,7 @@
\ --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" (K [
auto_tac (mem_css addsimps2 [enabled_disj]
addSIs2 [RWRNext_enabled]),
- exhaust_tac "arg(ch w p)" 1,
+ cases_tac "arg(ch w p)" 1,
action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
[ReadInner_enabled,exI] [] 1,
force_tac (mem_css addDs2 [base_pair]) 1,
--- a/src/HOL/UNITY/GenPrefix.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML Mon Mar 13 12:51:10 2000 +0100
@@ -129,7 +129,7 @@
Goal "((xs, y#ys) : genPrefix r) = \
\ (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by Auto_tac;
qed "genPrefix_Cons";
@@ -183,7 +183,7 @@
\ --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r";
by (induct_tac "xs" 1);
by Auto_tac;
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by Auto_tac;
qed_spec_mp "genPrefix_imp_nth";
@@ -194,7 +194,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj,
all_conj_distrib])));
by (Clarify_tac 1);
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
by (ALLGOALS Force_tac);
qed_spec_mp "nth_imp_genPrefix";
--- a/src/HOL/UNITY/Lift_prog.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Mon Mar 13 12:51:10 2000 +0100
@@ -16,7 +16,7 @@
Goal "(insert_map i x (delete_map i g)) = g(i:=x)";
by (rtac ext 1);
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-by (exhaust_tac "d" 1);
+by (cases_tac "d" 1);
by (ALLGOALS Asm_simp_tac);
qed "insert_map_delete_map_eq";
--- a/src/HOL/UNITY/TimerArray.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/TimerArray.ML Mon Mar 13 12:51:10 2000 +0100
@@ -15,7 +15,7 @@
Goal "Timer : UNIV leadsTo {s. count s = 0}";
by (res_inst_tac [("f", "count")] lessThan_induct 1);
by (Simp_tac 1);
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
by (ensures_tac "decr" 1);
qed "Timer_leadsTo_zero";
@@ -36,7 +36,7 @@
by (constrains_tac 2);
(*Progress property for the array of Timers*)
by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
(*Annoying need to massage the conditions to have the form (... Times UNIV)*)
by (auto_tac (claset() addIs [subset_imp_leadsTo],
simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
--- a/src/HOL/UNITY/Token.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/UNITY/Token.ML Mon Mar 13 12:51:10 2000 +0100
@@ -16,7 +16,7 @@
Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
by (Simp_tac 1);
-by (exhaust_tac "proc s i" 1);
+by (cases_tac "proc s i" 1);
by Auto_tac;
qed "not_E_eq";
--- a/src/HOL/ex/BinEx.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/BinEx.ML Mon Mar 13 12:51:10 2000 +0100
@@ -323,13 +323,13 @@
Goal "w: normal ==> bin_succ w : normal";
by (etac normal.induct 1);
-by (exhaust_tac "w" 4);
+by (cases_tac "w" 4);
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
qed "bin_succ_normal";
Goal "w: normal ==> bin_pred w : normal";
by (etac normal.induct 1);
-by (exhaust_tac "w" 3);
+by (cases_tac "w" 3);
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
qed "bin_pred_normal";
--- a/src/HOL/ex/Factorization.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Factorization.ML Mon Mar 13 12:51:10 2000 +0100
@@ -10,12 +10,12 @@
(* --- Arithmetic --- *)
Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m";
-by (exhaust_tac "m" 1);
+by (cases_tac "m" 1);
by Auto_tac;
qed "one_less_m";
Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by Auto_tac;
qed "one_less_k";
@@ -24,7 +24,7 @@
qed "mult_left_cancel";
Goal "[| 0<m; m*n = m |] ==> n=1";
-by (exhaust_tac "n" 1);
+by (cases_tac "n" 1);
by Auto_tac;
qed "mn_eq_m_one";
@@ -55,7 +55,7 @@
Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
by Auto_tac;
-by (exhaust_tac "k" 1);
+by (cases_tac "k" 1);
by Auto_tac;
qed "prime_nd_one";
@@ -78,7 +78,7 @@
qed "primes_eq";
Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (ALLGOALS Asm_full_simp_tac);
qed "primel_one_empty";
@@ -105,7 +105,7 @@
Goal "nondec xs --> nondec (oinsert x xs)";
by (induct_tac "xs" 1);
-by (exhaust_tac "list" 2);
+by (cases_tac "list" 2);
by (ALLGOALS (Asm_full_simp_tac));
qed_spec_mp "nondec_oinsert";
@@ -123,9 +123,9 @@
by (induct_tac "xs" 1);
by Safe_tac;
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "list" 1);
+by (cases_tac "list" 1);
by (ALLGOALS Asm_full_simp_tac);
-by (exhaust_tac "list" 1);
+by (cases_tac "list" 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1);
by (ALLGOALS Asm_full_simp_tac);
@@ -269,7 +269,7 @@
\ --> xs <~~> ys)";
by (res_inst_tac [("n","n")] less_induct 1);
by Safe_tac;
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
by (rtac (perm_primel_ex RS exE) 1);
by (ALLGOALS Asm_full_simp_tac);
--- a/src/HOL/ex/Primrec.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Primrec.ML Mon Mar 13 12:51:10 2000 +0100
@@ -185,7 +185,7 @@
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
by (rtac allI 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [less_le_trans]
@@ -223,7 +223,7 @@
"[| ALL l. f l + list_add l < ack(kf, list_add l); \
\ ALL l. g l + list_add l < ack(kg, list_add l) \
\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
-by (exhaust_tac "l" 1);
+by (cases_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [less_trans]) 1);
by (etac ssubst 1); (*get rid of the needless assumption*)
--- a/src/HOL/ex/Puzzle.ML Mon Mar 13 12:42:41 2000 +0100
+++ b/src/HOL/ex/Puzzle.ML Mon Mar 13 12:51:10 2000 +0100
@@ -14,7 +14,7 @@
by (res_inst_tac [("n","k")] less_induct 1);
by (rtac allI 1);
by (rename_tac "i" 1);
-by (exhaust_tac "i" 1);
+by (cases_tac "i" 1);
by (Asm_simp_tac 1);
by (blast_tac (claset() addSIs [Suc_leI] addIs [le_less_trans]) 1);
val lemma = result() RS spec RS mp;