Ignore:
Timestamp:
Mar 14, 2013, 3:40:01 PM (8 years ago)
Author:
tranquil
Message:

some reorganization of definitions, and a new taaf_append_taaf

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2799 r2869  
    5353                 call_rel ?? R s1_pre s2_pre →
    5454                 as_after_return S2 s2_pre s2_ret.
    55 
    56 (* the equivalent of a collapsable trace_any_label where we do not force
    57    costedness of the lookahead status *)
    58 inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
    59 | taaf_base : ∀s.trace_any_any_free S s s
    60 | taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
    61   as_classifier S s2 cl_other →
    62   trace_any_any_free S s1 s3
    63 | taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
    64   as_classifier S s2 cl_jump →
    65   as_costed S s3 →
    66   trace_any_any_free S s1 s3.
    67 
    68 definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
    69 match taaf with
    70 [ taaf_base _ ⇒ false
    71 | _ ⇒ true
    72 ].
    7355
    7456(* the base property we ask for simulation to work depends on the status_class
     
    172154(* some useful lemmas *)
    173155
    174 let rec taa_append_taa S st1 st2 st3
    175   (taa : trace_any_any S st1 st2) on taa :
    176   trace_any_any S st2 st3 →
    177   trace_any_any S st1 st3 ≝
    178   match taa
    179   with
    180   [ taa_base st1' ⇒ λst3,taa2.taa2
    181   | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
    182     taa_step ???? H I J (taa_append_taa … tl taa2)
    183   ] st3.
    184 
    185 definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
    186 if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
    187 trace_any_any S s1 s2 ≝
    188 λS,s1,s2,taaf.
    189 match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
    190   trace_any_any S s1 s2 with
    191 [ taaf_base s ⇒ λ_.taa_base …
    192 | taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
    193   taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
    194 | taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
    195 ].
    196 
    197 lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
    198   ∀taa1 : trace_any_any S s1 s2.
    199   ∀taa2 : trace_any_any S s2 s3.
    200   ∀tal : trace_any_label S fl s3 s4.
    201   (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
    202 #S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
    203 [ #s1 #taa2 #tal %
    204 | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
    205   normalize >IH %
    206 ]
    207 qed.
    208 
    209 lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
    210   ∀taa1 : trace_any_any S s1 s2.
    211   ∀taa2 : trace_any_any S s2 s3.
    212   ∀taa3 : trace_any_any S s3 s4.
    213   taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
    214   taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
    215 #S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
    216 [ #s1 #taa2 #tal %
    217 | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
    218   normalize >IH %
    219 ]
    220 qed.
    221 
    222156let rec taa_append_tal_rel S1 fl1 st1 st1'
    223157  (tal1 : trace_any_label S1 fl1 st1 st1')
     
    343277%[|%[|%[|%[|%[| % ]]]]]
    344278qed.
    345 
    346 definition taaf_append_tal : ∀S,st1,fl,st2,st3.
    347   ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
    348   trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
    349   match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
    350   trace_any_label S fl st1 st3 with
    351   [ taaf_base s ⇒ λ_.λtal.tal
    352   | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
    353   | taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J)
    354   ]. 
    355279
    356280lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
Note: See TracChangeset for help on using the changeset viewer.