Changeset 2760 for src/common


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2757 r2760  
    829829].
    830830
     831lemma filter_map_append:
     832 ∀X,Y,f,l1,l2. filter_map X Y f (l1@l2) = filter_map … f l1 @ filter_map … f l2.
     833 #X #Y #f #l1 elim l1 // #hd #tl #IH #l2 normalize >IH //
     834qed.
     835
    831836lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
    832837#X #Y #f #l elim l normalize // qed.
     
    856861λA,P,l.list_distribute_sig_aux … l (pi2 … l).
    857862
     863lemma list_distribute_sig_append:
     864 ∀A,P,l1,l2,prf1,prf2,prf3.
     865  list_distribute_sig A P «l1@l2,prf3» =
     866   list_distribute_sig … «l1,prf1» @ list_distribute_sig … «l2,prf2».
     867 #A #P #l1 whd in match list_distribute_sig; normalize nodelta elim l1 //
     868 #hd #tl #IH normalize #l2 #prf1 #prf2 #prf3 <IH //
     869qed.
     870
    858871let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
    859872match l with
     
    868881    | _ ⇒ λ_.None ?
    869882    ] (pi2 … ev)) (list_distribute_sig … l).
     883
     884axiom costlabels_of_observables_trace_label_return_id_irrelevant:
     885 ∀S,s1,s2,tr,id1,id2.
     886  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id1) =
     887  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id2).
     888
     889lemma costlabels_of_observables_append:
     890 ∀S:abstract_status. ∀tr1,tr2: as_trace S.
     891  costlabels_of_observables S (tr1 @ tr2) =
     892   costlabels_of_observables … tr1 @ costlabels_of_observables … tr2.
     893[ #S #tr1 #tr2 whd in match costlabels_of_observables; normalize nodelta
     894  <filter_map_append <list_distribute_sig_append //
     895| @All_append [ @(pi2 … tr1) | @(pi2 … tr2) ]]
     896qed.
    870897
    871898(* JHM: base case now passes the termination checker *)
     
    10351062  costlabels_of_observables … (observables_trace_label_label … tll dummy).
    10361063
     1064definition flatten_trace_any_label ≝
     1065  λS,flag,st1,st2.λtll : trace_any_label S flag st1 st2.
     1066  (* as cost events do not depend on current function identifier, we
     1067     can use a dummy one *)
     1068  let dummy ≝ an_identifier ? one in
     1069  costlabels_of_observables … (observables_trace_any_label … tll dummy).
     1070
    10371071lemma lift_cost_map_same_cost_tlr :
    10381072  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
Note: See TracChangeset for help on using the changeset viewer.