# HG changeset patch
# User wenzelm
# Date 1330360859 -3600
# Node ID a7ca72710dfe6dd8802613d8cbc4265a284b41c5
# Parent  e6e1ec6d5c1c3c66a65f9b5aa894450212fd8a92
tuned proofs;

diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/AxCompl.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -1299,7 +1299,7 @@
         apply -
         apply (rule MGFn_NormalI)
         apply (rule ax_derivs.Jmp [THEN conseq1])
-        apply (auto intro: eval.Jmp simp add: abupd_def2)
+        apply (auto intro: eval.Jmp)
         done
     next
       case (Throw e)
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/AxSound.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -78,8 +78,7 @@
 done
 
 lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
-apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
-done
+by (auto elim!: evaln_elim_cases simp add: triple_valid2_def2)
 
 lemma Methd_triple_valid2_SucI: 
 "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
@@ -992,7 +991,7 @@
       from da obtain V where 
         da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
         by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
-      from eval obtain w upd where
+      from eval obtain upd where
         eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
         using normal_s0 by (fastforce elim: evaln_elim_cases)
       from valid_var P valid_A conf_s0 eval_var wt_var da_var
@@ -1408,7 +1407,7 @@
           by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
         with normal_s1 normal_s2 eval_args 
         have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
-          by (auto dest: eval_gext intro: conf_gext)
+          by (auto dest: eval_gext)
         from evaln_args wt_args da_args' conf_s1 wf
         have conf_args: "list_all2 (conf G (store s2)) vs pTs"
           by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
@@ -1491,7 +1490,7 @@
             apply (rule dynM')
             apply (force dest: ty_expr_is_type)
             apply (rule invC_widen)
-            apply (force intro: conf_gext dest: eval_gext)
+            apply (force dest: eval_gext)
             apply simp
             apply simp
             apply (simp add: invC)
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -2241,7 +2241,7 @@
   \<Longrightarrow> table_of (fields G C) (fn, declclass f) = Some (fld f)"
 apply (simp only: accfield_def Let_def)
 apply (rule table_of_remap_SomeD)
-apply (auto dest: filter_tab_SomeD)
+apply auto
 done
 
 
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/Evaln.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -233,7 +233,6 @@
         "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
         "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
-        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
 
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
@@ -575,7 +574,6 @@
     apply -
     apply (rule evaln.Loop)
     apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
-
     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
     done
   then show ?case ..
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/Example.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -975,7 +975,6 @@
 done
 
 declare mhead_resTy_simp [simp add]
-declare member_is_static_simp [simp add]
 
 lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
 apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -28,7 +28,7 @@
   next
     case New
     then show ?case
-      by (auto split: split_if_asm)
+      by auto
   qed
   with eqs 
   show ?thesis
@@ -68,19 +68,18 @@
  \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
 apply (cases s)
 apply (auto simp add: check_method_access_def Let_def error_free_def 
-                      abrupt_if_def 
-            split: split_if_asm)
+                      abrupt_if_def)
 done
 
 lemma error_free_FVar_lemma: 
      "error_free s 
        \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
-  by (case_tac s) (auto split: split_if) 
+  by (case_tac s) auto
 
 lemma error_free_init_lvars [simp,intro]:
 "error_free s \<Longrightarrow> 
   error_free (init_lvars G C sig mode a pvs s)"
-by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
+by (cases s) (auto simp add: init_lvars_def Let_def)
 
 lemma error_free_LVar_lemma:   
 "error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
@@ -362,12 +361,12 @@
       case CInst
       with modeIntVir obj_props
       show ?thesis 
-        by (auto dest!: widen_Array2 split add: split_if)
+        by (auto dest!: widen_Array2)
     next
       case Arr
-      from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
+      from Arr obtain T where "obj_ty obj = T.[]" by blast
       moreover from Arr have "obj_class obj = Object" 
-        by (blast dest: obj_class_Arr1)
+        by blast
       moreover note modeIntVir obj_props wf 
       ultimately show ?thesis by (auto dest!: widen_Array )
     qed
@@ -411,8 +410,7 @@
                            dynimethd_def dynmethd_C_C 
                     intro: dynmethd_declclass
                     dest!: wf_imethdsD
-                     dest: table_of_map_SomeI
-                    split: split_if_asm)
+                     dest: table_of_map_SomeI)
     next        
       case SuperM
       with not_SuperM show ?thesis ..
@@ -421,8 +419,7 @@
       with wf dynlookup IfaceT invC_prop show ?thesis 
         by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
                            DynT_prop_def
-                    intro: methd_declclass dynmethd_declclass
-                    split: split_if_asm)
+                    intro: methd_declclass dynmethd_declclass)
     qed
   next
     case ClassT
@@ -1851,7 +1848,7 @@
       (*
                 wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
                 wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
-      by (rule wt_elim_cases) (auto split add: split_if)
+      by (rule wt_elim_cases) auto
     from If.prems obtain E C where
       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
                                        \<guillemotright>In1l e\<guillemotright> E" and
@@ -3978,7 +3975,7 @@
     obtain 
               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
-      by (elim wt_elim_cases) (auto split add: split_if)
+      by (elim wt_elim_cases) auto
     from If.prems obtain E C where
       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
                                        \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
diff -r e6e1ec6d5c1c -r a7ca72710dfe src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Mon Feb 27 17:39:34 2012 +0100
+++ b/src/HOL/Bali/WellType.thy	Mon Feb 27 17:40:59 2012 +0100
@@ -546,7 +546,7 @@
     then show ?thesis by blast
   next 
     case False then show ?thesis 
-      by (auto simp add: invmode_def split: split_if_asm)
+      by (auto simp add: invmode_def)
   qed
 qed