--- 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)
--- 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'))" .
--- 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
--- 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]
--- 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)
--- 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) =
--- 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
--- 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)
--- 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