src/HOL/MicroJava/BV/BVSpecTypeSafe.ML

     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
 val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
-		correct_frame_def,wt_instr_def];
+		correct_frame_def];
 
 Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
 "\\<lbrakk> wt_jvm_prog G phi; \
 \   method (G,C) sig = Some (C,rT,maxl,ins); \
 \   G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \

 (******* LS *******)
 
 Goal
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = LS(Load idx); \
+\  ins!pc = Load idx; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,

 qed "Load_correct";
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = LS(Store idx); \
+\  ins!pc = Store idx; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]

 AddIffs [conf_Intg_Integer];
 
 Goal
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = LS(Bipush i); \
+\  ins!pc = Bipush i; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]

 qed "NT_subtype_conv";
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = LS Aconst_null; \
+\  ins!pc =  Aconst_null; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
 	addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1);
 qed "Aconst_null_correct";
 
 
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = LS ls_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "ls_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
-qed "LS_correct";
-
-
-(**** CH ****)
 
 Goalw [cast_ok_def]
  "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
 by (forward_tac [widen_Class] 1);

 qed "Cast_conf2";
 
 Goal
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = CH (Checkcast D); \
+\  ins!pc = Checkcast D; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons,
 		raise_xcpt_def]@defs1 addsplits [option.split]) 1);
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] 
 	addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
 qed "Checkcast_correct";
 
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = CH ch_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "ch_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
-qed "CH_correct";
-
-
-(******* MO *******)
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = MO (Getfield F D); \
+
+Goal
+"\\<lbrakk> wf_prog wt G; \
+\  method (G,C) sig = Some (C,rT,maxl,ins); \
+\  ins!pc = Getfield F D; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);

 
 
 Goal
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = MO (Putfield F D); \
+\  ins!pc = Putfield F D; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);

 		hconf_imp_hconf_field_update,
 		correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
 qed "Putfield_correct";
 
 
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = MO mo_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "mo_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
-qed "MO_correct";
-
-
-(****** CO ******)
-
 Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
 by(Fast_tac 1);
 qed "collapse_paired_All";
 
 Goal
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = CO(New cl_idx); \
+\  ins!pc = New cl_idx; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,

 	addss (simpset() addsimps [NT_subtype_conv,approx_val_def,conf_def,
 		fun_upd_apply,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 
 	addsplits [option.split])) 1);
 qed "New_correct";
 
+
+(****** Method Invocation ******)
+
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = CO co_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "co_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
-qed "CO_correct";
-
-
-(****** MI ******)
-
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = MI(Invoke mn pTs); \
+\  ins ! pc = Invoke mn pTs; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by(forward_tac [wt_jvm_progD] 1);

 by (asm_full_simp_tac (simpset() addsimps [approx_val_def, raise_xcpt_def]) 1);
 bd conf_NullTD 1;
 by (Asm_simp_tac 1);
 qed "Invoke_correct";
 
+
+Delsimps [map_append];
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = MI mi_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by (case_tac "mi_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Invoke_correct])));
-qed "MI_correct";
-
-(****** MR ******)
-
-Delsimps [map_append];
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = MR Return; \
+\  ins ! pc = Return; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (asm_full_simp_tac (simpset() addsimps (neq_Nil_conv::defs1) addsplits [split_if_asm]) 1);

  addIs [conf_widen]
  addss (simpset() addsimps [approx_val_def,append_eq_conv_conj,map_eq_Cons]@defs1)) 1);
 qed "Return_correct";
 Addsimps [map_append];
 
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = MR mr; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by (case_tac "mr" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
-qed "MR_correct";
-
-(****** BR ******)
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = BR(Goto branch); \
+
+Goal 
+"\\<lbrakk> wf_prog wt G; \
+\  method (G,C) sig = Some (C,rT,maxl,ins); \
+\  ins ! pc = Goto branch; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]

 
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = BR(Ifcmpeq branch); \
+\  ins!pc = Ifcmpeq branch; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
 qed "Ifiacmpeq_correct";
 
 
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = BR br_com; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(rewtac wt_jvm_prog_def);
-by (case_tac "br_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
-qed "BR_correct";
-
-
-(****** OS ******)
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS Pop; \
+Goal 
+"\\<lbrakk> wf_prog wt G; \
+\  method (G,C) sig = Some (C,rT,maxl,ins); \
+\  ins ! pc = Pop; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);

 
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS Dup; \
+\  ins ! pc = Dup; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 

 
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS Dup_x1; \
+\  ins ! pc = Dup_x1; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 

 qed "Dup_x1_correct";
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS Dup_x2; \
+\  ins ! pc = Dup_x2; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 

 qed "Dup_x2_correct";
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS Swap; \
+\  ins ! pc = Swap; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 

 
 
 Goal 
 "\\<lbrakk> wf_prog wt G; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = OS IAdd; \
+\  ins ! pc = IAdd; \
 \  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
   addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1);
 qed "IAdd_correct";
 
 
+(** instr correct **)
+
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = OS os_com; \
 \  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
 \  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
   ba 1;
  ba 1;
+by(case_tac "ins!pc" 1);
+by(fast_tac (claset() addIs [Invoke_correct]) 9);
+by(fast_tac (claset() addIs [Return_correct]) 9);
 by(rewtac wt_jvm_prog_def);
-by (case_tac "os_com" 1);
-by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
-qed "OS_correct";
+by (ALLGOALS (fast_tac (claset() addIs 
+      [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct,
+       Checkcast_correct,Getfield_correct,Putfield_correct,New_correct,
+       Goto_correct,Ifiacmpeq_correct,Pop_correct,Dup_correct,
+       Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
+qed "instr_correct";
+
 
 (** Main **)
 
 Goalw [correct_state_def,Let_def]
  "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \

  by (case_tac "frs" 1);
   by (asm_full_simp_tac (simpset() addsimps exec.simps) 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.simps@[split_def]) 1);
+ by (force_tac (claset() addIs [instr_correct], simpset() addsplits [split_if_asm] addsimps exec.simps@[split_def]) 1);
 by (case_tac "frs" 1);
  by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.simps)));
 qed_spec_mp "BV_correct_1";
 
 (*******)
 Goal
 "\\<lbrakk> xp=None; frs\\<noteq>[] \\<rbrakk> \\<Longrightarrow> (\\<exists>state'. exec (G,xp,hp,frs) = Some state')";
-by (fast_tac (claset() addIs [BV_correct_1] 
-	addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1);
+by (auto_tac (claset() addIs [BV_correct_1],
+             (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)));
+by (case_tac "(snd (snd (snd (the (method (G, ab) (ac, b)))))) ! ba" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps defs1)));
 val lemma = result();
 
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
 \ \\<Longrightarrow> \\<exists>state'. exec(G,xp,hp,frs) = Some state' \\<and> G,phi \\<turnstile>JVM state'\\<surd>";