Ignore:
Timestamp:
Mar 31, 2013, 10:01:42 PM (6 years ago)
Author:
campbell
Message:

Switch removal and labelling combined.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SwitchAndLabel.ma

    r3046 r3047  
    22include "Clight/labelSimulation.ma".
    33
    4 axiom switch_final_related : ∀ge1,s1,s2.
    5   switch_state_sim ge1 s1 s2 →
    6   is_final s1 = is_final s2.
    74
    85lemma after_aux_result : ∀avs,n,s,tr,P.
     
    9087
    9188lemma interactive_switch_step : ∀ge,ge'.
    92   switch_removal_globals ? fundef_switch_removal ge ge' →
     89  related_globals … fundef_switch_removal ge ge' →
    9390  ∀s1,s1',o,k.
    9491  exec_step ge s1 = Interact … o k →
     
    144141let corec build_exec
    145142  (ge1,ge2,ge3:genv)
    146   (SRG:switch_removal_globals ? fundef_switch_removal ge1 ge2)
     143  (SRG:related_globals … fundef_switch_removal ge1 ge2)
    147144  (RG:related_globals_gen … label_fundef ge2 ge3)
    148145  (s1,s2,s3:state)
     
    212209  ]
    213210] qed.
     211
     212theorem 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
     219cases (not_wrong_init clight_fullexec p NW)
     220whd in ⊢ (% → ??%? → ?); #s1 #I1
     221cases (initial_state_in_switch_simulation … I1)
     222#s' * * change with p' in match (program_switch_removal p); #I' #RG' #S'
     223cases (initial_state_in_simulation … I')
     224#s2 * #I2
     225
     226whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
     227letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
     228change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
     229>I1
     230
     231whd in match (exec_inf ????);
     232letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p')))
     233change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p')));
     234>I2
     235
     236whd in ⊢ (??% → ? → ?%%);
     237>exec_inf_aux_unfold
     238>exec_inf_aux_unfold
     239whd in ⊢ (??% → ? → ?%%);
     240whd in match (is_final ?????);
     241>(initial_state_is_not_final … I1)
     242whd in match (is_final ?????);
     243>(initial_state_is_not_final … I2)
     244whd 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.