Changeset 3047 for src/Clight/SwitchAndLabel.ma
 Timestamp:
 Mar 31, 2013, 10:01:42 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SwitchAndLabel.ma
r3046 r3047 2 2 include "Clight/labelSimulation.ma". 3 3 4 axiom switch_final_related : ∀ge1,s1,s2.5 switch_state_sim ge1 s1 s2 →6 is_final s1 = is_final s2.7 4 8 5 lemma after_aux_result : ∀avs,n,s,tr,P. … … 90 87 91 88 lemma interactive_switch_step : ∀ge,ge'. 92 switch_removal_globals ?fundef_switch_removal ge ge' →89 related_globals … fundef_switch_removal ge ge' → 93 90 ∀s1,s1',o,k. 94 91 exec_step ge s1 = Interact … o k → … … 144 141 let corec build_exec 145 142 (ge1,ge2,ge3:genv) 146 (SRG: switch_removal_globals ?fundef_switch_removal ge1 ge2)143 (SRG:related_globals … fundef_switch_removal ge1 ge2) 147 144 (RG:related_globals_gen … label_fundef ge2 ge3) 148 145 (s1,s2,s3:state) … … 212 209 ] 213 210 ] qed. 211 212 theorem switch_and_labelling_sim : ∀p. 213 let e1 ≝ exec_inf … clight_fullexec p in 214 let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label (program_switch_removal p))) in 215 not_wrong state e1 → 216 sim_with_labels e1 e2. 217 #p letin p' ≝ (program_switch_removal p) 218 #NW 219 cases (not_wrong_init clight_fullexec p NW) 220 whd in ⊢ (% → ??%? → ?); #s1 #I1 221 cases (initial_state_in_switch_simulation … I1) 222 #s' * * change with p' in match (program_switch_removal p); #I' #RG' #S' 223 cases (initial_state_in_simulation … I') 224 #s2 * #I2 225 226 whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %; 227 letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %; 228 change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p); 229 >I1 230 231 whd in match (exec_inf ????); 232 letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p'))) 233 change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p'))); 234 >I2 235 236 whd in ⊢ (??% → ? → ?%%); 237 >exec_inf_aux_unfold 238 >exec_inf_aux_unfold 239 whd in ⊢ (??% → ? → ?%%); 240 whd in match (is_final ?????); 241 >(initial_state_is_not_final … I1) 242 whd in match (is_final ?????); 243 >(initial_state_is_not_final … I2) 244 whd in ⊢ (??% → ? → ?%%); 245 246 #NW #S 247 @(swl_steps E0 E0) 248 [ 2: @steps_step  skip  //  @(build_exec … RG' … S' S) 249 [ whd in match ge2; >unfold_clight_label 250 @transform_program_gen_related 251  inversion NW 252 [ #tr #i #s #E1 #E2 destruct 253  #trX #sX #eX #NWX #E1X #E2X destruct // 254  #H1 #H2 #H3 #H4 #H5 destruct 255 ] 256 ] 257 ] qed. 258 259
Note: See TracChangeset
for help on using the changeset viewer.