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