--- 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)
--- 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)
--- 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
--- 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 ..
--- 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)
--- 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
--- 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