Changeset 2202 for src/Clight/labelSimulation.ma
- Timestamp:
- Jul 17, 2012, 6:57:39 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSimulation.ma
r2176 r2202 1189 1189 1190 1190 lemma not_wrong_init : ∀p. 1191 not_wrong (exec_inf … clight_fullexec p) →1191 not_wrong state (exec_inf … clight_fullexec p) → 1192 1192 ∃s. make_initial_state … p = OK ? s. 1193 #p whd in ⊢ (? % → ?); change with (make_initial_state p) in match (make_initial_state ??? p);1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p); 1194 1194 cases (make_initial_state p) 1195 1195 [ /2/ … … 1225 1225 plus ge s tr s' → 1226 1226 is_final s' = None ? → 1227 steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s')). 1227 steps state tr 1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1229 (exec_inf_aux … clight_fullexec ge (exec_step ge s')). 1229 1230 #ge #s0 #tr0 #s0' #P elim P 1230 1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold 1231 whd in ⊢ (?? %?);1232 whd in ⊢ (???%?); 1232 1233 whd in match (is_final ?????); >NF 1233 1234 %2 1234 1235 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF 1235 1236 >exec_inf_aux_unfold >EX1 1236 whd in ⊢ (?? %?);1237 whd in ⊢ (???%?); 1237 1238 whd in match (is_final ?????); >(plus_not_final … P2) 1238 1239 %3 @IH // … … 1242 1243 plus ge s tr s' → 1243 1244 is_final s' = Some ? r → 1244 ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1245 (e_stop … tr' r s'). 1245 ∃tr'. steps state tr 1246 (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1247 (e_stop … tr' r s'). 1246 1248 #ge #s0 #tr0 #s0' #r #P elim P 1247 1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold 1248 %{tr} whd in ⊢ (?? %?);1250 %{tr} whd in ⊢ (???%?); 1249 1251 whd in match (is_final ?????); >F 1250 1252 %1 … … 1253 1255 #tr' #S' %{tr'} 1254 1256 >exec_inf_aux_unfold >EX1 1255 whd in ⊢ (?? %?);1257 whd in ⊢ (???%?); 1256 1258 whd in match (is_final ?????); >(plus_not_final … P2) 1257 1259 %3 @S' … … 1263 1265 (s1,s2:state) 1264 1266 (S:state_with_labels s1 s2) 1265 (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))1267 (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))) 1266 1268 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 1267 1269 match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with … … 1299 1301 #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S' 1300 1302 lapply (NWk i) 1301 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (? % → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])1303 @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?]) 1302 1304 @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????); 1303 1305 cases (is_final s2') 1304 [ whd in ⊢ (? % → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //1306 [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec // 1305 1307 inversion NW' 1306 1308 [ #H1 #H2 #H3 #H4 #H5 destruct … … 1308 1310 | #H14 #H15 #H16 #H17 #H18 destruct 1309 1311 ] 1310 | #r whd in ⊢ (? % → ?%%); #NW' @(swl_stop … (steps_stop …)) //1312 | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) // 1311 1313 ] 1312 1314 ] qed. … … 1343 1345 >I2 1344 1346 1345 whd in ⊢ (? % → ? → ?%%);1347 whd in ⊢ (??% → ? → ?%%); 1346 1348 >exec_inf_aux_unfold 1347 1349 >exec_inf_aux_unfold 1348 whd in ⊢ (? % → ? → ?%%);1350 whd in ⊢ (??% → ? → ?%%); 1349 1351 whd in match (is_final ?????); 1350 1352 >(initial_state_is_not_final … I1) 1351 1353 whd in match (is_final ?????); 1352 1354 >(initial_state_is_not_final … I2) 1353 whd in ⊢ (? % → ? → ?%%);1355 whd in ⊢ (??% → ? → ?%%); 1354 1356 1355 1357 #NW #S
Note: See TracChangeset
for help on using the changeset viewer.