--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Fri Aug 28 20:18:33 2009 +0200
@@ -145,7 +145,7 @@
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
(is "?app ST LT = ?P ST LT")
proof
- assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
+ assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
next
assume app: "?app ST LT"
hence l: "length fpTs < length ST" by simp
@@ -153,7 +153,7 @@
proof -
have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
moreover from l have "length (take (length fpTs) ST) = length fpTs"
- by (simp add: min_def)
+ by simp
ultimately show ?thesis ..
qed
obtain apTs where
@@ -168,11 +168,11 @@
have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
with app
show "?P ST LT"
- apply (clarsimp simp add: list_all2_def min_def)
+ apply (clarsimp simp add: list_all2_def)
apply ((rule exI)+, (rule conjI)?)+
apply auto
done
-qed
+qed
lemma approx_loc_len [simp]:
"approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
--- a/src/HOL/MicroJava/BV/Effect.thy Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy Fri Aug 28 20:18:33 2009 +0200
@@ -375,7 +375,7 @@
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
by auto
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
- by (auto simp add: min_def)
+ by (auto)
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST"
by blast
hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []"
@@ -391,7 +391,7 @@
with Pair
have "?app s \<Longrightarrow> ?P s" by (simp only:)
moreover
- have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)
+ have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
ultimately
show ?thesis by (rule iffI)
qed
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Fri Aug 28 20:18:33 2009 +0200
@@ -293,7 +293,7 @@
shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
proof -
from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
- with suc wtl show ?thesis by (simp add: min_def)
+ with suc wtl show ?thesis by (simp)
qed
lemma (in lbv) wtl_all:
@@ -308,7 +308,7 @@
with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp
from pc have "is!pc = drop pc is ! 0" by simp
with Cons have "is!pc = i" by simp
- with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
+ with take pc show ?thesis by (auto)
qed
section "preserves-type"
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Aug 28 20:18:33 2009 +0200
@@ -959,7 +959,7 @@
apply simp
apply (simp (no_asm_simp))+
apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
+apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
(* show check_type \<dots> *)
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -973,7 +973,7 @@
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_of_list_def ssize_sto_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
apply (simp (no_asm_simp))+
done
@@ -988,7 +988,7 @@
apply (drule_tac x=sttp in spec, erule exE)
apply simp
apply (rule check_type_mono, assumption)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split: prod.split)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
done
(* ********************************************************************** *)
@@ -1058,8 +1058,7 @@
lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1081,7 +1080,7 @@
\<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
apply (erule exE)+
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length STo)" in exI)
@@ -1093,8 +1092,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1113,8 +1111,7 @@
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1130,8 +1127,7 @@
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1180,8 +1176,7 @@
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1194,8 +1189,7 @@
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
- max_ssize_def max_of_list_def ssize_sto_def max_def
- eff_def norm_eff_def)
+ max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
@@ -1211,7 +1205,7 @@
bc_mt_corresp [IAdd] (replST 2 (PrimT Integer))
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
@@ -1252,7 +1246,7 @@
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
- apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+ apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
@@ -1303,7 +1297,7 @@
apply (simp add: max_spec_preserves_length [THEN sym])
-- "@{text check_type}"
-apply (simp add: max_ssize_def ssize_sto_def max_def)
+apply (simp add: max_ssize_def ssize_sto_def)
apply (simp add: max_of_list_def)
apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
apply simp
@@ -1314,7 +1308,7 @@
apply (simp only: comp_is_type)
apply (frule method_wf_mdecl) apply assumption apply assumption
apply (simp add: wf_mdecl_def wf_mhead_def)
-apply (simp add: max_def)
+apply (simp)
done
@@ -1471,7 +1465,7 @@
apply (case_tac "sttp1", simp)
apply (rule check_type_lower) apply assumption
apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
-apply (simp (no_asm_simp) add: max_of_list_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def)
(* subgoals \<exists> ... *)
apply (rule surj_pair)+