src/HOL/MicroJava/BV/BVSpecTypeSafe.thy

 \<close>
 lemma exec_instr_xcpt:
   "(fst (exec_instr i G hp stk vars Cl sig pc frs) = Some xcp)
   = (\<exists>stk'. exec_instr i G hp stk vars Cl sig pc frs = 
             (Some xcp, hp, (stk', vars, Cl, sig, pc)#frs))"
-  by (cases i, auto simp add: split_beta split: split_if_asm)
+  by (cases i, auto simp add: split_beta split: if_split_asm)
 
 
 text \<open>
   Relates \<open>match_any\<close> from the Bytecode Verifier with 
   \<open>match_exception_table\<close> from the operational semantics:

 lemma match_et_imp_match:
   "match_exception_table G (Xcpt X) pc et = Some handler
   \<Longrightarrow> match G X pc et = [Xcpt X]"
   apply (simp add: match_some_entry)
   apply (induct et)
-  apply (auto split: split_if_asm)
+  apply (auto split: if_split_asm)
   done
 
 text \<open>
   We can prove separately that the recursive search for exception
   handlers (\<open>find_handler\<close>) in the frame stack results in 

        G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
   \<Longrightarrow> \<exists>adr T. xcp = Addr adr \<and> hp adr = Some T" 
   (is "\<lbrakk> ?xcpt; ?wt; ?correct \<rbrakk> \<Longrightarrow> ?thesis")
 proof -
   note [simp] = split_beta raise_system_xcpt_def
-  note [split] = split_if_asm option.split_asm 
+  note [split] = if_split_asm option.split_asm 
   
   assume wt: ?wt ?correct
   hence pre: "preallocated hp" by (simp add: correct_state_def)
 
   assume xcpt: ?xcpt with pre show ?thesis 

     
     from some_handler xp'
     have state': 
       "state' = (None, hp, ([xcp], loc, C, sig, handler)#frs)"
       by (cases "ins!pc") (auto simp add: raise_system_xcpt_def split_beta 
-                               split: split_if_asm) (* takes long! *)
+                               split: if_split_asm) (* takes long! *)
 
     let ?f' = "([xcp], loc, C, sig, handler)"
     from eff
     obtain ST' LT' where
       phi_pc': "phi C sig ! handler = Some (ST', LT')" and
       frame': "correct_frame G hp (ST',LT') maxl ins ?f'" 
     proof (cases "ins!pc")
       case Return \<comment> "can't generate exceptions:"
-      with xp' have False by (simp add: split_beta split: split_if_asm)
+      with xp' have False by (simp add: split_beta split: if_split_asm)
       thus ?thesis ..
     next
       case New
       with some_handler xp'
       have xcp: "xcp = Addr (XcptRef OutOfMemory)"

       show ?thesis by (rule that)
     next 
       case Getfield
       with some_handler xp'
       have xcp: "xcp = Addr (XcptRef NullPointer)"
-        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+        by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
       with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
       with Getfield some_handler phi_pc eff 
       obtain ST' LT' where
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and

       show ?thesis by (rule that)
     next
       case Putfield
       with some_handler xp'
       have xcp: "xcp = Addr (XcptRef NullPointer)"
-        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+        by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
       with prehp have "cname_of hp xcp = Xcpt NullPointer" ..
       with Putfield some_handler phi_pc eff 
       obtain ST' LT' where
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and

       show ?thesis by (rule that)
     next
       case Checkcast
       with some_handler xp'
       have xcp: "xcp = Addr (XcptRef ClassCast)"
-        by (simp add: raise_system_xcpt_def split_beta split: split_if_asm)
+        by (simp add: raise_system_xcpt_def split_beta split: if_split_asm)
       with prehp have "cname_of hp xcp = Xcpt ClassCast" ..
       with Checkcast some_handler phi_pc eff 
       obtain ST' LT' where
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and

     wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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>;
     fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 wt_jvm_prog_def split: split_if_asm)
+apply (clarsimp simp add: defs2 wt_jvm_prog_def split: if_split_asm)
 apply (blast intro: Cast_conf2)
 done
 
 
 lemma Getfield_correct:

   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>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: defs2 wt_jvm_prog_def split_beta
-                split: option.split split_if_asm)
+                split: option.split if_split_asm)
 apply (frule conf_widen)
 apply assumption+
 apply (drule conf_RefTD)
 apply (clarsimp simp add: defs2)
 apply (rule conjI)

   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et 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>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split if_split_asm)
 apply (frule conf_widen)
 prefer 2
   apply assumption
  apply assumption
 apply (drule conf_RefTD)

 lemma 
   fixes G :: jvm_prog ("\<Gamma>")
   assumes wf: "wf_prog wf_mb \<Gamma>"
   shows hconf_start: "\<Gamma> \<turnstile>h (start_heap \<Gamma>) \<surd>"
   apply (unfold hconf_def start_heap_def)
-  apply (auto simp add: fun_upd_apply blank_def oconf_def split: split_if_asm)
+  apply (auto simp add: fun_upd_apply blank_def oconf_def split: if_split_asm)
   apply (simp add: fields_is_type 
           [OF _ wf [THEN wf_prog_ws_prog] 
                 is_class_xcpt [OF wf [THEN wf_prog_ws_prog]]])+
   done