src/HOL/MicroJava/BV/BVSpecTypeSafe.thy

       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
 apply (unfold correct_state_def Let_def correct_frame_def)
 apply simp
 apply (blast intro: wt_jvm_prog_impl_wt_instr)
-.
+done
 
 lemma Load_correct:
 "\<lbrakk> wf_prog wt G;
    method (G,C) sig = Some (C,rT,maxl,ins); 
    ins!pc = Load idx; 

 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (rule approx_loc_imp_approx_val_sup)
  apply simp+
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
-.
+done
 
 lemma Store_correct:
 "\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins);
   ins!pc = Store idx;

 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (blast intro: approx_stk_imp_approx_stk_sup)
 apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
-.
+done
 
 
 lemma conf_Intg_Integer [iff]:
   "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
 by (simp add: conf_def)

   method (G,C) sig = Some (C,rT,maxl,ins); 
   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>";
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
-.
+done
 
 lemma NT_subtype_conv:
   "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
 proof -
   have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
     apply (erule widen.induct)
     apply auto
     apply (case_tac R)
     apply auto
-    .
+    done
   note l = this
 
   show ?thesis 
     by (force intro: null dest: l)
 qed

   method (G,C) sig = Some (C,rT,maxl,ins); 
   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>";
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (rule conjI)
  apply (force simp add: approx_val_Null NT_subtype_conv)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
-.
+done
 
 
 lemma Cast_conf2:
   "\<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"

 apply (elim exE disjE)
  apply (simp add: null)
 apply (clarsimp simp add: conf_def obj_ty_def)
 apply (cases v)
 apply (auto intro: null rtrancl_trans)
-.
+done
 
 
 lemma Checkcast_correct:
 "\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 

   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>"
 apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
-.
+done
 
 
 lemma Getfield_correct:
 "\<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>";
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
 apply (frule conf_widen)
 apply assumption+
 apply (drule conf_RefTD)
 apply (clarsimp simp add: defs1 approx_val_def)
 apply (rule conjI)
  apply (drule widen_cfs_fields)
  apply assumption+
  apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
-.
+done
 
 lemma Putfield_correct:
 "\<lbrakk> wf_prog wt G;
   method (G,C) sig = Some (C,rT,maxl,ins); 
   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>";
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
 apply (clarsimp simp add: approx_val_def)
 apply (frule conf_widen)
 prefer 2
 apply assumption
 apply assumption
 apply (drule conf_RefTD)
 apply clarsimp
-apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
-		approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
-		hconf_imp_hconf_field_update
-		correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
-.
+apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap
+  approx_stk_imp_approx_stk_sup
+  approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
+  hconf_imp_hconf_field_update
+  correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
+done
 
 lemma collapse_paired_All:
   "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
   by fast
 

                    approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
                    hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
                    correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
 		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
        split: option.split)
-.
+done
 
 
 (****** Method Invocation ******)
 
 lemmas [simp del] = split_paired_Ex

   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>"
 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
 apply (frule wt_jvm_prog_impl_wt_instr)
-apply (tactic "EVERY1[atac, etac Suc_lessD]")
+apply (assumption, erule Suc_lessD)
 apply (unfold wt_jvm_prog_def)
-apply (tactic {* fast_tac (claset()
- addDs [thm "subcls_widen_methd"]
- addEs [rotate_prems 1 widen_trans]
- addIs [conf_widen]
- addss (simpset() addsimps [thm "approx_val_def",thm "append_eq_conv_conj", map_eq_Cons]@thms "defs1")) 1 *})
-.
+apply (fastsimp
+  dest: subcls_widen_methd
+  elim: widen_trans [COMP swap_prems_rl]
+  intro: conf_widen
+  simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
+done
 
 lemmas [simp] = map_append
 
 lemma Goto_correct:
 "\<lbrakk> wf_prog wt G; 

   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>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
-.
+done
 
 
 lemma Ifcmpeq_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 

   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>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
-.
+done
 
 lemma Pop_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Pop;

   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>"
 apply (clarsimp simp add: defs1)
 apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
-.
+done
 
 lemma Dup_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup;

   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
-.
+done
 
 lemma Dup_x1_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup_x1;

   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
-.
+done
 
 lemma Dup_x2_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Dup_x2;

   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
-.
+done
 
 lemma Swap_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = Swap;

   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs1 map_eq_Cons)
 apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
              simp add: defs1 map_eq_Cons)
-.
+done
 
 lemma IAdd_correct:
 "\<lbrakk> wf_prog wt G; 
   method (G,C) sig = Some (C,rT,maxl,ins); 
   ins ! pc = IAdd; 

   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>"
 apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
 apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
-.
+done
 
 
 (** instr correct **)
 
 lemma instr_correct:

 apply (unfold wt_jvm_prog_def)
 apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
        Checkcast_correct Getfield_correct Putfield_correct New_correct 
        Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
        Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
-.
+done
 
 
 (** Main **)
 
 lemma correct_state_impl_Some_method:

 by (auto simp add: correct_state_def Let_def)
 
 
 lemma BV_correct_1 [rulify]:
 "\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
- \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
-apply (tactic "split_all_tac 1")
+ \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (simp only: split_tupled_all)
 apply (rename_tac xp hp frs)
 apply (case_tac xp)
  apply (case_tac frs)
   apply simp
- apply (tactic "split_all_tac 1")
- apply (tactic "hyp_subst_tac 1")
+ apply (simp only: split_tupled_all)
+ apply hypsubst
  apply (frule correct_state_impl_Some_method)
  apply (force intro: instr_correct)
 apply (case_tac frs)
-apply simp+
-.
+apply simp_all
+done
 
 
 lemma L0:
   "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
 by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)

   "\<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>"
 apply (drule L0)
 apply assumption
 apply (fast intro: BV_correct_1)
-.
+done
 
 
 theorem BV_correct [rulify]:
 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
 apply (unfold exec_all_def)
 apply (erule rtrancl_induct)
  apply simp
 apply (auto intro: BV_correct_1)
-.
+done
 
 
 theorem BV_correct_initial:
 "\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
  \<Longrightarrow>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
 apply (drule BV_correct)
 apply assumption+
 apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
-.
+done
 
 end