Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCastsMeasurable.ma

    r3063 r3081  
    22include "common/FEMeasurable.ma".
    33include "Clight/Clight_classified_system.ma".
    4 
    5 (* TODO: move *)
    6 lemma step_not_final : ∀ge,s,tr,s'.
    7   exec_step ge s = Value … 〈tr,s'〉 →
    8   is_final s = None ?.
    9 #ge * //
    10 #r #tr #s' #ST whd in ST:(??%?); destruct
    11 qed.
    124
    135lemma state_cast_labelled : ∀s,s'.
     
    3527  ]
    3628] qed.
     29
     30(* Put cast simplification simulation into form that FEMeasurable needs.
     31   Note that sim_call_label is just sticking together two normal steps - we
     32   never add extra steps here, so we don't need to worry about moving cost
     33   labels to the start of the function. *)
    3734
    3835definition simplify_measurable_sim : meas_sim ≝
     
    8683  cases (cast_correction … RG … S1 ST)
    8784  #s2' * #ST' #S2 %{1} whd
    88   whd in match (is_final … s1'); >(step_not_final … ST')
     85  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    8986  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    9087  whd % [ % | assumption ]
     
    9390  cases (cast_correction … RG … S1 ST)
    9491  #s2' * #ST' #S2 %{0} whd
    95   whd in match (is_final … s1'); >(step_not_final … ST')
     92  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    9693  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    9794  whd % [ % | assumption ]
     
    103100  #s3' * #ST2' #S3
    104101  %{1} whd
    105   whd in match (is_final … s1'); >(step_not_final … ST1')
     102  whd in match (is_final … s1'); >(cl_step_not_final … ST1')
    106103  whd whd in match (step … Clight_pcs ge' s1'); >ST1'
    107104  whd % [ % [ % | change with (Clight_labelled s2') in ⊢ (?%); <(state_cast_labelled … S2) assumption ] ]
    108   whd whd in match (is_final … s2'); >(step_not_final … ST2')
     105  whd whd in match (is_final … s2'); >(cl_step_not_final … ST2')
    109106  whd whd in match (step … Clight_pcs ge' s2'); >ST2'
    110107  whd % [ % | assumption ]
     
    114111  #s2' * #ST' #S2 %{0} % [ @(return_E0 … ST) assumption ]
    115112  whd
    116   whd in match (is_final … s1'); >(step_not_final … ST')
     113  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    117114  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    118115  whd % [ >(return_E0 … ST) // assumption | assumption ]
     
    121118  cases (cast_correction … RG … S1 ST)
    122119  #s2' * #ST' #S2 whd
    123   whd in match (is_final … s1'); >(step_not_final … ST')
     120  whd in match (is_final … s1'); >(cl_step_not_final … ST')
    124121  whd whd in match (step … Clight_pcs ge' s1'); >ST'
    125122  whd % [ % | assumption ]
Note: See TracChangeset for help on using the changeset viewer.