# 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') \ G \ X \ 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 \ 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 \ 0 < length (drop (length fpTs) a)" (is "?a \ ?l") by auto hence "?a \ ?l \ length (rev (take (length fpTs) a)) = length fpTs" - by (auto simp add: min_def) + by (auto) hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ 0 < length ST" by blast hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ ST \ []" @@ -391,7 +391,7 @@ with Pair have "?app s \ ?P s" by (simp only:) moreover - have "?P s \ ?app s" by (unfold app_def) (clarsimp simp add: min_def) + have "?P s \ ?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) \ \" 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 \ *) 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: "\is_class cG cname \ \ 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 @@ \ 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 @@ \ bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)" apply (subgoal_tac "\ 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 @@ \ bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)" apply (subgoal_tac "\ 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 @@ \ bc_mt_corresp [Load i] (\(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 \ ... *) apply (rule surj_pair)+