src/HOL/Bali/TypeSafe.thy
changeset 62390 842917225d56
parent 62042 6c6ccf573479
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4  apply (cases s)
     1.5  apply (auto simp add: check_field_access_def Let_def error_free_def 
     1.6                        abrupt_if_def 
     1.7 -            split: split_if_asm)
     1.8 +            split: if_split_asm)
     1.9  done
    1.10  
    1.11  lemma error_free_check_method_access_eq:
    1.12 @@ -213,7 +213,7 @@
    1.13  apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
    1.14   simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
    1.15              check_field_access_def check_method_access_def Let_def
    1.16 - split del: split_if_asm split add: sum3.split)
    1.17 + split del: if_split_asm split add: sum3.split)
    1.18  (* 6 subgoals *)
    1.19  apply force+
    1.20  done
    1.21 @@ -232,9 +232,9 @@
    1.22  done
    1.23  
    1.24  lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
    1.25 -apply (erule eval_cases , auto split del: split_if_asm)
    1.26 +apply (erule eval_cases , auto split del: if_split_asm)
    1.27  apply (case_tac "inited C (globs s1)")
    1.28 -apply  (clarsimp split del: split_if_asm)+
    1.29 +apply  (clarsimp split del: if_split_asm)+
    1.30  apply (drule eval_gext')+
    1.31  apply (drule init_class_obj_inited)
    1.32  apply (erule inited_gext)
    1.33 @@ -724,7 +724,7 @@
    1.34  qed
    1.35  
    1.36  declare split_paired_All [simp del] split_paired_Ex [simp del] 
    1.37 -declare split_if     [split del] split_if_asm     [split del] 
    1.38 +declare if_split     [split del] if_split_asm     [split del] 
    1.39          option.split [split del] option.split_asm [split del]
    1.40  setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
    1.41  setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
    1.42 @@ -753,7 +753,7 @@
    1.43  apply   (blast intro: FVar_lemma2)
    1.44  done
    1.45  declare split_paired_All [simp] split_paired_Ex [simp] 
    1.46 -declare split_if     [split] split_if_asm     [split] 
    1.47 +declare if_split     [split] if_split_asm     [split] 
    1.48          option.split [split] option.split_asm [split]
    1.49  setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
    1.50  setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
    1.51 @@ -869,7 +869,7 @@
    1.52  by (auto simp add: abrupt_if_def)
    1.53  
    1.54  declare split_paired_All [simp del] split_paired_Ex [simp del] 
    1.55 -declare split_if     [split del] split_if_asm     [split del] 
    1.56 +declare if_split     [split del] if_split_asm     [split del] 
    1.57          option.split [split del] option.split_asm [split del]
    1.58  setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
    1.59  setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
    1.60 @@ -902,7 +902,7 @@
    1.61                                then None else Some (Class declC)))"
    1.62  apply (simp add: init_lvars_def2)
    1.63  apply (rule conforms_set_locals)
    1.64 -apply  (simp (no_asm_simp) split add: split_if)
    1.65 +apply  (simp (no_asm_simp) split add: if_split)
    1.66  apply (drule  (4) DynT_conf)
    1.67  apply clarsimp
    1.68  (* apply intro *)
    1.69 @@ -922,7 +922,7 @@
    1.70  apply     (simp add: np_no_jump)
    1.71  done
    1.72  declare split_paired_All [simp] split_paired_Ex [simp] 
    1.73 -declare split_if     [split] split_if_asm     [split] 
    1.74 +declare if_split     [split] if_split_asm     [split] 
    1.75          option.split [split] option.split_asm [split]
    1.76  setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close>
    1.77  setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>