equal
deleted
inserted
replaced
1120 apply (rule_tac x="Suc (length ST)" in exI) |
1120 apply (rule_tac x="Suc (length ST)" in exI) |
1121 apply simp |
1121 apply simp |
1122 apply simp+ |
1122 apply simp+ |
1123 done |
1123 done |
1124 |
1124 |
|
1125 declare not_Err_eq [iff del] |
|
1126 |
1125 lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk> |
1127 lemma bc_mt_corresp_Load: "\<lbrakk> i < length LT; LT ! i \<noteq> Err; mxr = length LT \<rbrakk> |
1126 \<Longrightarrow> bc_mt_corresp [Load i] |
1128 \<Longrightarrow> bc_mt_corresp [Load i] |
1127 (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)" |
1129 (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)" |
1128 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
1130 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def |
1129 max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2) |
1131 max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def min_max.sup_absorb2) |
1136 apply (simp (no_asm_simp)) |
1138 apply (simp (no_asm_simp)) |
1137 apply (simp only: err_def) |
1139 apply (simp only: err_def) |
1138 apply (frule listE_nth_in) apply assumption |
1140 apply (frule listE_nth_in) apply assumption |
1139 apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}") |
1141 apply (subgoal_tac "LT ! i \<in> {x. \<exists>y\<in>types cG. x = OK y}") |
1140 apply (drule CollectD) apply (erule bexE) |
1142 apply (drule CollectD) apply (erule bexE) |
1141 apply (simp (no_asm_simp) ) |
1143 apply (simp (no_asm_simp)) |
1142 apply blast |
1144 apply blast |
1143 apply blast |
1145 apply blast |
1144 done |
1146 done |
1145 |
1147 |
1146 |
1148 |