src/HOL/Bali/TypeSafe.thy

  "error_free (check_field_access G accC statDeclC fn stat a s)
  \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
 apply (cases s)
 apply (auto simp add: check_field_access_def Let_def error_free_def 
                       abrupt_if_def 
-            split: split_if_asm)
+            split: if_split_asm)
 done
 
 lemma error_free_check_method_access_eq:
 "error_free (check_method_access G accC statT mode sig a' s)
  \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"

 prefer 26 
   apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
             check_field_access_def check_method_access_def Let_def
- split del: split_if_asm split add: sum3.split)
+ split del: if_split_asm split add: sum3.split)
 (* 6 subgoals *)
 apply force+
 done
 
 lemma evar_gext_f: 

 apply (drule eval_gext)
 apply auto
 done
 
 lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
-apply (erule eval_cases , auto split del: split_if_asm)
+apply (erule eval_cases , auto split del: if_split_asm)
 apply (case_tac "inited C (globs s1)")
-apply  (clarsimp split del: split_if_asm)+
+apply  (clarsimp split del: if_split_asm)+
 apply (drule eval_gext')+
 apply (drule init_class_obj_inited)
 apply (erule inited_gext)
 apply (simp (no_asm_use))
 done

   show ?thesis
     by (cases a) auto
 qed
 
 declare split_paired_All [simp del] split_paired_Ex [simp del] 
-declare split_if     [split del] split_if_asm     [split del] 
+declare if_split     [split del] if_split_asm     [split del] 
         option.split [split del] option.split_asm [split del]
 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
 setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
 
 lemma FVar_lemma: 

 apply   (force elim!: conforms_upd_gobj)
 
 apply   (blast intro: FVar_lemma2)
 done
 declare split_paired_All [simp] split_paired_Ex [simp] 
-declare split_if     [split] split_if_asm     [split] 
+declare if_split     [split] if_split_asm     [split] 
         option.split [split] option.split_asm [split]
 setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
 
 

 
 lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
 by (auto simp add: abrupt_if_def)
 
 declare split_paired_All [simp del] split_paired_Ex [simp del] 
-declare split_if     [split del] split_if_asm     [split del] 
+declare if_split     [split del] if_split_asm     [split del] 
         option.split [split del] option.split_asm [split del]
 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
 setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
 
 lemma conforms_init_lvars: 

                                | Res \<Rightarrow> Some (resTy (mthd dm)))
                  | This \<Rightarrow> if (is_static (mthd sm)) 
                               then None else Some (Class declC)))"
 apply (simp add: init_lvars_def2)
 apply (rule conforms_set_locals)
-apply  (simp (no_asm_simp) split add: split_if)
+apply  (simp (no_asm_simp) split add: if_split)
 apply (drule  (4) DynT_conf)
 apply clarsimp
 (* apply intro *)
 apply (drule (3) conforms_init_lvars_lemma 
                  [where ?lvars="(lcls (mbody (mthd dm)))"])

 apply   (case_tac "is_static sm")
 apply     simp
 apply     (simp add: np_no_jump)
 done
 declare split_paired_All [simp] split_paired_Ex [simp] 
-declare split_if     [split] split_if_asm     [split] 
+declare if_split     [split] if_split_asm     [split] 
         option.split [split] option.split_asm [split]
 setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
 setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>