source: LTS/Traces.ma @ 3506

Last change on this file since 3506 was 3506, checked in by sacerdot, 5 years ago

Refactoring.

File size: 19.9 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20inductive FunctionName : Type[0] ≝
21 | a_function_id : ℕ → FunctionName.
22 
23inductive CallCostLabel : Type[0] ≝
24 | a_call_label : ℕ → CallCostLabel.
25 
26inductive ReturnPostCostLabel : Type[0] ≝
27 | a_return_cost_label : ℕ → ReturnPostCostLabel.
28 
29inductive NonFunctionalLabel : Type[0] ≝
30 | a_non_functional_label : ℕ → NonFunctionalLabel.
31 
32inductive CostLabel : Type[0] ≝
33 | a_call : CallCostLabel → CostLabel
34 | a_return_post : ReturnPostCostLabel → CostLabel
35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37coercion a_call.
38coercion a_return_post.
39coercion a_non_functional_label.
40
41(*
42definition ret_act_label_to_cost_label :
43(ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
44λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b].
45
46coercion ret_act_label_to_cost_label.
47
48definition call_act_label_to_cost_label :
49(CallCostLabel + NonFunctionalLabel) → CostLabel ≝
50λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
51
52coercion call_act_label_to_cost_label.
53*)
54
55definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
56λx,y.match x with [ a_non_functional_label n ⇒
57                    match y with [a_non_functional_label m ⇒ eqb n m ] ].
58
59lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
60(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
61#P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
62
63definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
64#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
65assumption
66qed.
67
68unification hint  0 ≔ ;
69    X ≟ DEQNonFunctionalLabel
70(* ---------------------------------------- *) ⊢
71    NonFunctionalLabel ≡ carr X.
72
73unification hint  0 ≔ p1,p2;
74    X ≟ DEQNonFunctionalLabel
75(* ---------------------------------------- *) ⊢
76    eq_nf_label p1 p2 ≡ eqb X p1 p2.
77
78definition eq_function_name : FunctionName → FunctionName → bool ≝
79λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].
80
81lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
82(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
83#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.
84
85definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
86#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
87assumption
88qed.
89
90unification hint  0 ≔ ;
91    X ≟ DEQFunctionName
92(* ---------------------------------------- *) ⊢
93    FunctionName ≡ carr X.
94
95unification hint  0 ≔ p1,p2;
96    X ≟ DEQFunctionName
97(* ---------------------------------------- *) ⊢
98    eq_function_name p1 p2 ≡ eqb X p1 p2.
99
100definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
101λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
102
103lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
104(c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
105#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
106
107definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
108#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
109assumption
110qed.
111
112unification hint  0 ≔ ;
113    X ≟ DEQReturnPostCostLabel
114(* ---------------------------------------- *) ⊢
115    ReturnPostCostLabel ≡ carr X.
116
117unification hint  0 ≔ p1,p2;
118    X ≟ DEQReturnPostCostLabel
119(* ---------------------------------------- *) ⊢
120    eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
121
122definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
123λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
124
125lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
126(c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
127#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
128
129definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
130#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
131assumption
132qed.
133
134unification hint  0 ≔ ;
135    X ≟ DEQCallCostLabel
136(* ---------------------------------------- *) ⊢
137    CallCostLabel ≡ carr X.
138
139unification hint  0 ≔ p1,p2;
140    X ≟ DEQCallCostLabel
141(* ---------------------------------------- *) ⊢
142    eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
143
144definition eq_costlabel : CostLabel → CostLabel → bool ≝
145λc1.match c1 with
146  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
147  | a_return_post x1 ⇒
148      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
149  | a_non_functional_label x1 ⇒
150     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
151  ].
152
153lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
154(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
155#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
156try (@H2 % #EQ destruct)
157[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
158  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
159| change with (eq_return_cost_lab ??) in ⊢ (?%);
160   @eq_return_cost_lab_elim
161   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
162| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
163  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
164]
165qed.
166
167
168definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
169#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
170assumption
171qed.
172
173unification hint  0 ≔ ;
174    X ≟ DEQCostLabel
175(* ---------------------------------------- *) ⊢
176    CostLabel ≡ carr X.
177
178unification hint  0 ≔ p1,p2;
179    X ≟ DEQCostLabel
180(* ---------------------------------------- *) ⊢
181    eq_costlabel p1 p2 ≡ eqb X p1 p2.
182
183   
184
185
186inductive ActionLabel : Type[0] ≝
187 | call_act : FunctionName → CallCostLabel → ActionLabel
188 | ret_act : option(ReturnPostCostLabel) → ActionLabel
189 | cost_act : option NonFunctionalLabel → ActionLabel.
190 
191definition is_cost_label : ActionLabel → Prop ≝
192λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
193
194inductive status_class : Type[0] ≝
195 | cl_jump : status_class
196 | cl_io : status_class
197 | cl_other : status_class.
198
199definition is_non_silent_cost_act : ActionLabel → Prop ≝
200λact. ∃l. act = cost_act (Some ? l).
201
202record abstract_status : Type[2] ≝
203 { as_status :> Type[0]
204 ; as_execute : ActionLabel → relation as_status
205 ; as_syntactical_succ : relation as_status
206 ; as_classify : as_status → status_class
207 ; is_call_post_label : as_status → bool
208 ; as_initial : as_status → bool
209 ; as_final : as_status → bool
210 ; jump_emits : ∀s1,s2,l.
211      as_classify … s1 = cl_jump →
212      as_execute l s1 s2 → is_non_silent_cost_act l
213 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
214      as_execute l s1 s2 → is_non_silent_cost_act l
215 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
216     as_execute l s1 s2 → is_non_silent_cost_act l
217 }.
218 (*
219definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
220λS,l.match l with
221[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
222| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
223                                                   | inr c' ⇒ is_io_entering S c']
224                           | None ⇒ false
225                           ]
226| cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
227| init_act ⇒ false
228].
229
230definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
231λS,l.match l with
232[ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
233| ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
234                                                   | inr c' ⇒ is_io_exiting S c']
235                           | None ⇒ false
236                           ]
237| cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
238| init_act ⇒ false
239].
240*)
241
242inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
243  | t_base : ∀st : S.raw_trace S st st
244  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
245             as_execute S l st1 st2 → raw_trace S st2 st3 →
246             raw_trace S st1 st3.
247
248definition is_cost_act : ActionLabel → Prop ≝
249λact.∃l.act = cost_act l.
250
251definition is_call_act : ActionLabel → Prop ≝
252λact.∃f,l.act = call_act f l.
253
254definition is_labelled_ret_act : ActionLabel → Prop ≝
255λact.∃l.act = ret_act (Some ? l).
256
257definition is_unlabelled_ret_act : ActionLabel → Prop ≝
258λact.act = ret_act (None ?).
259
260definition is_costlabelled_act : ActionLabel → Prop ≝
261λact.match act with [ call_act _ _ ⇒ True
262                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
263                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
264                    ].
265(*
266lemma well_formed_trace_inv :
267∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
268well_formed_trace … t →
269(st1 = st2 ∧ t ≃ t_base S st1) ∨
270(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
271well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
272t ≃ t_ind … prf … tl) ∨
273(∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
274 well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
275(∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
276 well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
277 is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
278#S #st1 #st2 #t #H inversion H
279[ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
280| #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
281  %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
282| #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
283  %{l} %{prf} %{tl} % // % //
284(*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
285  destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
286]
287qed.
288
289*)
290
291let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
292(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
293match t1
294return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
295with
296[ t_base st ⇒ λt2.t2
297| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
298].
299
300interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
301
302lemma append_associative : ∀S,st1,st2,st3,st4.
303∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
304∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
305#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
306[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
307qed.
308
309definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
310raw_trace … st1 st3 → Prop≝
311λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
312
313definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
314raw_trace … st1 st3 → Prop≝
315λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
316
317inductive pre_silent_trace (S : abstract_status) :
318∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
319| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
320| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
321                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
322                pre_silent_trace … (t_ind … prf … tl).
323               
324definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
325raw_trace S st1 st2 → bool ≝
326λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
327
328definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
329raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
330¬ (bool_to_Prop (is_trace_non_empty … t)).
331
332lemma pre_silent_io : ∀S : abstract_status.
333∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
334as_classify … s2 ≠ cl_io.
335#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
336#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
337#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
338#EQ destruct #_ @IH assumption
339qed.
340
341(*
342definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
343raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
344well_formed_trace … t.
345
346lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
347∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
348#S #st1 #st2 #t * //
349qed. *)
350(* elim t -t
351[ #st #_ %]
352#st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
353[2: >cl % #EQ destruct]
354@IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
355#st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
356% [ assumption | #_ assumption]
357qed.*)
358
359inductive pre_measurable_trace (S : abstract_status) :
360∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
361 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
362 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
363                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
364                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
365                      pre_measurable_trace … (t_ind … prf … tl)
366 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
367                      as_classify … st1 ≠ cl_io →
368                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
369                      is_labelled_ret_act l → pre_measurable_trace … tl →
370                      pre_measurable_trace … (t_ind … prf … tl)
371 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
372                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
373                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
374                      pre_measurable_trace … tl →
375                      pre_measurable_trace … (t_ind … prf … tl)
376 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
377                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
378                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
379                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
380                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
381                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
382                      as_syntactical_succ S st1 st4 →
383                      is_unlabelled_ret_act l2 →
384                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
385                     
386lemma pre_measurable_trace_inv : ∀S : abstract_status.
387∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
388(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
389(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
390 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
391 pre_measurable_trace … tl) ∨
392(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
393 t = t_ind … prf … tl ∧
394 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
395(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
396 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
397 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
398(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
399 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
400 ∃prf' : as_execute S l2 st1'' st1'''.
401 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
402 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
403 bool_to_Prop (¬ is_call_post_label … st1) ∧
404 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
405 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
406#S #st1 #st2 #t #H inversion H
407[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
408| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
409  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
410| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
411  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
412| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
413  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
414| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
415  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
416  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
417  %{prf'} /12 by conj/
418]
419qed.
420
421definition measurable :
422 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
423λS,si,s1,s3,sn,t.
424 pre_measurable_trace … t ∧
425 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
426 ∃l1,l2,prf1,prf2.
427  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
428 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
429
430let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
431(t : raw_trace S st1 st2) on t : list CostLabel ≝
432match t with
433[ t_base st ⇒ [ ]
434| t_ind st1' st2' st3' l prf t' ⇒
435    let tl ≝ get_costlabels_of_trace … t' in
436    match l with
437    [ call_act f c ⇒ [ c ]
438    | ret_act x ⇒ match x with
439                  [ Some c ⇒ [ a_return_post c ]
440                  | None ⇒ []
441                  ]
442    | cost_act x ⇒ match x with
443                  [ Some c ⇒ [ a_non_functional_label c ]
444                  | None ⇒ []
445                  ]
446   ] @ tl
447].
448
449lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
450∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
451#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
452#H inversion H
453[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
454destruct #_ @IH % assumption
455qed.
456
457lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
458∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
459get_costlabels_of_trace … (t1 @ t2) =
460 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
461#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
462[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
463qed.
464 
Note: See TracBrowser for help on using the repository browser.