Changeset 3505
Legend:
- Unmodified
- Added
- Removed
-
LTS/Vm.ma
r3503 r3505 1126 1126 mem … 〈c1,pc p p' st1〉 1127 1127 (labels_pc … (instructions … prog) (call_label_fun … prog) 1128 (return_label_fun … prog) (in_act … prog) O). 1128 (return_label_fun … prog) (in_act … prog) O). 1129 #p #p' #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H 1130 #H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H) 1131 [ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1; 1132 >EQc1 * #EQ destruct // ] 1133 cases i in Hi; 1134 [ #seq * [|#lbl1] 1135 | #newpc 1136 | #cond #newpc #ltrue #lfalse 1137 | #lin #io #lout 1138 | #f 1139 | 1140 ] 1141 normalize nodelta cases(asm_is_io ??) normalize nodelta 1142 [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct 1143 |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_ 1144 [3: cases x normalize nodelta 1145 |6: #H cases(bind_inversion ????? H) -H #y * #_ 1146 ] 1147 ] 1148 whd in ⊢ (??%% → ?); #EQ destruct try % normalize in EQc1; destruct 1149 qed. 1150 1129 1151 theorem static_dynamic : 1130 1152 (* Given an assembly program *) … … 1190 1212 [ normalize in ⊢ (??%%); >neutral_l @EQact 1191 1213 | 1192 | check nth_opt 1193 1194 cases daemon 1214 | @execute_mem_label_pc // 1215 ] 1216 | #H #EQ destruct #_ whd in match get_pc; normalize nodelta 1217 <(proj1 ?? (static_analisys_ok … EQmap …)) 1218 [ normalize in ⊢ (??%%); >neutral_l @EQact 1219 | 1220 | whd in EQc1 : (??%%); destruct lapply H @eqb_elim [2: #_ #EQ destruct] #EQ >EQ #_ @i_act_in_map 1221 ] 1222 ] 1195 1223 | >rewrite_in_dependent_map 1196 [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?);1197 1198 %1224 [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); 1225 >append_nil in ⊢ (??%?); % |3:] 1226 % 1199 1227 ] 1200 1228 qed.
Note: See TracChangeset
for help on using the changeset viewer.