# HG changeset patch
# User nipkow
# Date 1251483513 -7200
# Node ID 16464c3f86bd23afd53525ce1961e055bdc0bcb8
# Parent  87d98857d1545ac8d4835666d320fcb1b91fbbf6
tuned proofs

diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/BV/BVNoTypeError.thy
--- 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"
diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/BV/Effect.thy
--- 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 
diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/BV/LBVSpec.thy
--- 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"
diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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)+