Changeset 2869 for src/joint


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

some reorganization of definitions, and a new taaf_append_taaf

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r2817 r2869  
    1414  λp : evaluation_params.λcurr_id.
    1515  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
    16 
    17 definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
    18   as_execute S s1 s2 →
    19   as_classifier … s1 cl_other →
    20   ∀taaf : trace_any_any_free S s2 s3.
    21   (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
    22   trace_any_any_free S s1 s3 ≝
    23 λS,s1,s2,s3,H,I,tl.
    24 match tl return λs2,s3,tl.
    25   as_execute … s1 s2 →
    26   if taaf_non_empty … tl then ¬as_costed … s2 else True →
    27   trace_any_any_free S s1 s3
    28 with
    29 [ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
    30 | taaf_step s2 s3 s4 taa H' I' ⇒
    31   λH,J.taaf_step … (taa_step … H I J taa) H' I'
    32 | taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
    33   λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
    34 ] H.
    35 
    36 lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
    37 bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
    38 #S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
    39 [ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
    40 qed.
    4116
    4217lemma produce_step_trace :
Note: See TracChangeset for help on using the changeset viewer.