# HG changeset patch
# User wenzelm
# Date 1326650127 -3600
# Node ID e88e980ed73578acffafc254db5b9a69484eb1cc
# Parent  9cb98d34f593bf4f0565d352de5604f08cbadcec
tuned proofs;

diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -294,8 +294,7 @@
       }
       ultimately show ?thesis using Getfield field "class" stk hconf wf
         apply clarsimp
-        apply (fastforce intro: wf_prog_ws_prog
-          dest!: hconfD widen_cfs_fields oconf_objD)
+        apply (fastforce dest!: hconfD widen_cfs_fields oconf_objD)
         done
     next
       case (Putfield F C)
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -112,11 +112,11 @@
   from phi' have l: "size phi' = size bs" by simp  
   with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp
   with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0"
-    by (clarsimp simp add: not_Err_eq)  
+    by auto
 
   from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def)
   also from w have "phi' = map OK (map ok_val phi')" 
-    by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI)
+    by (auto simp add: wt_step_def intro!: nth_equalityI)
   finally 
   have check_types:
     "check_types G maxs maxr (map OK (map ok_val phi'))" .
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -71,7 +71,7 @@
   apply (simp add: eff_def xcpt_eff_def norm_eff_def)
   apply (case_tac "bs!p")
 
-  apply (clarsimp simp add: not_Err_eq)
+  apply clarsimp
   apply (drule listE_nth_in, assumption)
   apply fastforce
 
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -474,14 +474,13 @@
 (* to avoid automatic pair splits *)
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
 
 lemma distinct_method: "\<lbrakk> wf_java_prog G; is_class G C; 
   method (G, C) S = Some (D, rT, pns, lvars, blk, res) \<rbrakk> \<Longrightarrow> 
   distinct (gjmb_plns (gmb G C S))"
 apply (frule method_wf_mdecl [THEN conjunct2],  assumption, assumption)
 apply (case_tac S)
-apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs distinct_append)
+apply (simp add: wf_mdecl_def wf_java_mdecl_def galldefs)
 apply (simp add: unique_def map_of_in_set)
 apply blast
 done
@@ -809,7 +808,7 @@
 (* case LAss *)
 apply (intro allI impI)
 apply (frule wtpd_expr_lass, erule conjE, erule conjE)
-apply (simp add: compExpr_compExprs.simps)
+apply simp
 
 apply (rule_tac ?instrs0.0 = "(compExpr (gmb G CL S) e)" in progression_transitive, rule HOL.refl)
 apply blast
@@ -884,7 +883,7 @@
 apply simp
 
 (* case Nil *)
-apply (simp add: compExpr_compExprs.simps)
+apply simp
 apply (intro strip)
 apply (rule progression_refl)
 
@@ -1261,7 +1260,6 @@
 
 (* reinstall pair splits *)
 declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 declare wf_prog_ws_prog [simp del]
 
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -955,20 +955,20 @@
 apply simp
 apply (simp (no_asm_simp))+
 apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
+apply (simp add: max_ssize_def) apply (simp (no_asm_simp))
 
   (* show check_type \<dots> *)
 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
 apply (simp only:)
 apply (rule check_type_mono) apply assumption
-apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
+apply (simp (no_asm_simp) add: max_ssize_def max_ac)
 apply (simp add: nth_append)
 
 apply (erule conjE)+
 apply (case_tac sttp1)
 apply (simp add: check_type_def)
 apply (rule states_lower, assumption)
-apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
+apply (simp (no_asm_simp) add: max_ssize_def)
 apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
 apply (simp (no_asm_simp))+
 done
@@ -1742,7 +1742,7 @@
   and ?f3.0 = "popST (Suc 0) \<box> pushST [PrimT Boolean]"
   in bc_mt_corresp_comb_inside)
   apply (simp (no_asm_simp))+
-  apply (simp add: compTpExpr_LT_ST_rewr popST_def)
+  apply simp
   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
   apply (simp (no_asm_simp) add: length_compTpExpr)
   apply (simp (no_asm_simp))
@@ -1775,7 +1775,7 @@
   and ?f3.0 = "comb_nil" 
   in bc_mt_corresp_comb_inside)
   apply (simp (no_asm_simp))+
-  apply (simp add: compTpExpr_LT_ST_rewr popST_def) 
+  apply simp
   apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
   apply (simp (no_asm_simp) add: length_compTpExpr)
   apply (simp (no_asm_simp) add: start_sttp_resp_def)
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -35,7 +35,7 @@
 apply (subgoal_tac "vn \<noteq> This")
 apply simp
 apply (subgoal_tac "\<forall> x \<in> set pns. (\<lambda>z. z \<noteq> vn) x")
-apply (simp add: takeWhile_append2)
+apply simp
 apply (subgoal_tac "length (takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars)) < length (map fst lvars)")
 apply simp
 apply (rule length_takeWhile)
@@ -86,7 +86,7 @@
   \<Longrightarrow> index (pns, zs @ ((xvar, xval) # xys), blk, res) xvar = Suc (length pns + length zs)"
 apply (simp add: index_def)
 apply (subgoal_tac "(\<And>x. ((x \<in> (set pns)) \<Longrightarrow> ((\<lambda>z. (z \<noteq> xvar))x)))")
-apply (simp add: List.takeWhile_append2)
+apply simp
 apply (subgoal_tac "(takeWhile (\<lambda>z. z \<noteq> xvar) (map fst zs @ xvar # map fst xys)) = map fst zs @ (takeWhile (\<lambda>z. z \<noteq> xvar) (xvar # map fst xys))")
 apply simp
 apply (rule List.takeWhile_append2)
@@ -114,7 +114,7 @@
   disjoint_varnames pns (lvars_pre @ (vn, ty) # lvars_post)
   \<Longrightarrow> index (pns, lvars_pre @ (vn, ty) # lvars_post, blk, res) vn =
   Suc (length pns + length lvars_pre)"
-apply (simp add: disjoint_varnames_def index_def unique_def distinct_append)
+apply (simp add: disjoint_varnames_def index_def unique_def)
 apply (subgoal_tac "vn \<noteq> This", simp)
 apply (subgoal_tac
   "takeWhile (\<lambda>z. z \<noteq> vn) (map fst lvars_pre @ vn # map fst lvars_post) =
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -95,7 +95,7 @@
 "(class G C = None) = (class (comp G) C = None)"
 apply (simp add: class_def comp_def compClass_def)
 apply (simp add: map_of_in_set)
-apply (simp add: image_compose [THEN sym] o_def split_beta del: image_compose)
+apply (simp add: image_compose [THEN sym] o_def split_beta)
 done
 
 lemma comp_is_class: "is_class (comp G) C = is_class G C"
@@ -170,7 +170,7 @@
 apply (simp only: image_compose [THEN sym])
 apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
-apply (simp del: image_compose)
+apply simp
 apply (simp add: fun_eq_iff split_beta)
 done
 
@@ -275,9 +275,9 @@
   = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)"
 apply (induct xs)
 apply simp
-apply (simp del: split_paired_All)
+apply simp
 apply (case_tac "k = fst a")
-apply (simp del: split_paired_All)
+apply simp
 apply (subgoal_tac "(inv f (fst a, snd (f a))) = a", simp)
 apply (subgoal_tac "(fst a, snd (f a)) = f a", simp)
 apply (erule conjE)+
@@ -332,7 +332,7 @@
 defer
 
 apply (intro strip)
-apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_Some_iff map_of_map)
 apply (simp add: map_add_def)
 apply (subgoal_tac "inj (\<lambda>(s, m). (s, Ca, m))")
 apply (drule_tac g="(Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca))" and xs=ms
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -320,7 +320,7 @@
     apply (rule sym, assumption)
     defer apply simp
     apply (subgoal_tac "\<forall>q t. \<not>((q, t) \<in> set qs \<and> t +_f ss ! q \<noteq> ss ! q)")
-    apply (blast intro!: psubsetI elim: equalityE)
+    apply (blast elim: equalityE)
     apply clarsimp
     apply (drule bspec, assumption) 
     apply (drule bspec, assumption)
diff -r 9cb98d34f593 -r e88e980ed735 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Jan 15 14:55:30 2012 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Jan 15 18:55:27 2012 +0100
@@ -155,7 +155,7 @@
 lemma (in Semilat) le_iff_plus_unchanged: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (x \<squnion>\<^sub>f y = y)"
 (*<*)
 apply (rule iffI)
- apply (blast intro: antisym_r refl_r lub ub2)
+ apply (blast intro: antisym_r lub ub2)
 apply (erule subst)
 apply simp
 done
@@ -164,7 +164,7 @@
 lemma (in Semilat) le_iff_plus_unchanged2: "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> (x \<sqsubseteq>\<^sub>r y) = (y \<squnion>\<^sub>f x = y)"
 (*<*)
 apply (rule iffI)
- apply (blast intro: order_antisym lub order_refl ub1)
+ apply (blast intro: order_antisym lub ub1)
 apply (erule subst)
 apply simp
 done