--- 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";