Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1964 r1976  
    632632for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    633633
    634 definition as_cost_of_trace_any_label :
    635   ∀S : abstract_status.
    636   ∀fl, start, end.
    637   as_cost_map S →
    638   trace_any_label S fl start end → ℕ ≝
    639   λS,fl,start,end,m,the_trace.
    640   Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig).
    641 
    642 definition as_cost_of_trace_label_label :
    643   ∀S : abstract_status.
    644   ∀fl, start, end.
    645   as_cost_map S →
    646   trace_label_label S fl start end → ℕ ≝
    647   λS,fl,start,end,m,the_trace.
    648   Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig).
    649 
    650 definition as_cost_of_trace_label_return :
    651   ∀S : abstract_status.
    652   ∀start, end.
    653   as_cost_map S →
    654   trace_label_return S start end → ℕ ≝
    655   λS,start,end,m,the_trace.
    656   Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig).
    657 
    658634lemma lift_cost_map_same_cost :
    659635  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     
    680656  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
    681657  tal_rel … the_trace_in the_trace_out →
    682   as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    683     as_cost_of_trace_any_label … m_out the_trace_out.
     658  (Σ_{l ∈ flatten_trace_any_label … the_trace_in}
     659    (lift_cost_map_id … dec m_out l)) =
     660  (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)).
    684661#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    685662#tal_in #tal_out #H_tal
     
    692669  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
    693670  tll_rel … the_trace_in the_trace_out →
    694   as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    695     as_cost_of_trace_label_label … m_out the_trace_out.
     671  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
     672    (lift_cost_map_id … dec m_out l)) =
     673  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
    696674#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    697675#tll_in #tll_out #H_tll
     
    704682  ∀the_trace_out : trace_label_return S_out start_out end_out.
    705683  tlr_rel … the_trace_in the_trace_out →
    706   as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    707     as_cost_of_trace_label_return … m_out the_trace_out.
     684  (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
     685    (lift_cost_map_id … dec m_out l)) =
     686  (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
    708687#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    709688#tlr_in #tlr_out #H_tlr
Note: See TracChangeset for help on using the changeset viewer.