Changeset 2299 for src/common


Ignore:
Timestamp:
Aug 21, 2012, 7:00:42 PM (7 years ago)
Author:
campbell
Message:

Soundly labelled RTLabs structured traces are "unrepeating".

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2186 r2299  
    3232definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
    3333  λa_s,st.as_label ? st ≠ None ?.
     34
     35lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) ∨ (¬as_costed S s).
     36#S #s whd in match (as_costed S s);
     37cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
     38qed.
    3439
    3540definition as_label_safe : ∀a_s : abstract_status.
     
    181186qed.
    182187
     188lemma not_costed_no_label : ∀S,st.
     189  ¬as_costed S st →
     190  as_label_of_pc S (as_pc_of S st) = None ?.
     191#S #st * normalize cases (as_label_of_pc S ?)
     192[ // | #l #H cases (H ?) % #E destruct ]
     193qed.
     194
     195lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
     196  ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
     197#S #fl0 #s10 #s20 *
     198[ #s1 #s2 #EX #CL #CS
     199| #s1 #s2 #EX #CL
     200| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     201| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
     202| #fl #s1 #s2 #s3 #EX #tal #CL #CS
     203] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     204qed.
     205
     206let rec tal_tail_not_costed S fl st1 st2 tal
     207  (H:Not (as_costed S st1)) on tal :
     208  All ? (λl. as_label_of_pc S l = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
     209cases tal in H ⊢ %;
     210[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
     211| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
     212| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     213| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
     214  cases (tal_pc_list_start … tal')
     215  #hd #E >E
     216  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
     217| #fl' #pre #init #end #EX #tal' #CL #CS #CS'
     218  cases (tal_pc_list_start … tal')
     219  #hd #E >E
     220  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
     221] qed.
     222
     223
    183224inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
    184225  | tac_base:
Note: See TracChangeset for help on using the changeset viewer.