source: LTS/Simulation.ma @ 3484

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

Simulation generalized to two different abstract_status.

File size: 37.5 KB
Line 
1include "Traces.ma".
2
3record relations (S1,S2 : abstract_status) : Type[0] ≝
4 { Srel: S1 → S2 → Prop
5 ; Crel: S1 → S2 → Prop
6 }.
7
8definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'.
9 ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'.
10
11record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝
12 { initial_is_initial :
13   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
14 ; final_is_final :
15   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
16 ; simulate_tau:
17     ∀s1:S1.∀s2:S2.∀s1':S1.
18      as_execute … (cost_act (None ?))  s1 s1'→
19      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
20      ∃s2'. ∃t: raw_trace S2 s2 s2'.
21        Srel … rel s1' s2' ∧ silent_trace … t
22 ; simulate_label:
23     ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
24      as_execute S1 (cost_act (Some ? l)) s1 s1' →
25      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
26      Srel … rel s1 s2 →
27      ∃s2',s2'',s2'''.
28       ∃t1: raw_trace S2 s2 s2'.
29       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
30       ∃t3: raw_trace … s2'' s2'''.
31        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
32 ; simulate_call_pl:
33     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
34      is_call_post_label … s1 →
35      as_execute … (call_act f l) s1 s1' →
36      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
37      Srel … rel s1 s2 →
38      ∃s2',s2'',s2'''.
39       ∃t1: raw_trace S2 s2 s2'.
40       as_execute … (call_act f l) s2' s2'' ∧
41       bool_to_Prop(is_call_post_label … s2') ∧
42       ∃t3: raw_trace S2 s2'' s2'''.
43        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
44 ; simulate_ret_l:
45     ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
46      as_execute S1 (ret_act (Some ? l)) s1 s1' →
47      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
48      Srel  … rel s1 s2 →
49      ∃s2',s2'',s2'''.
50       ∃t1: raw_trace S2 s2 s2'.
51       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
52       ∃t3: raw_trace S2 s2'' s2'''.
53        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
54 ; simulate_call_n:
55     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
56      as_execute … (call_act f l) s1 s1' →
57      ¬ is_call_post_label … s1 →
58      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
59      Srel … rel s1 s2 →
60      ∃s2',s2'',s2'''.
61       ∃t1: raw_trace S2 s2 s2'.
62       bool_to_Prop (¬ is_call_post_label … s2') ∧
63       as_execute … (call_act f l) s2' s2'' ∧
64       ∃t3: raw_trace S2 s2'' s2'''.
65        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
66        ∧ Crel … rel s1 s2'
67 ; simulate_ret_n:
68     ∀s1:S1.∀s2:S2.∀s1':S1.
69      as_execute … (ret_act (None ?)) s1 s1' →
70      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
71      Srel … rel s1 s2 →
72      ∃s2',s2'',s2''': S2.
73       ∃t1: raw_trace S2 s2 s2'.
74       as_execute … (ret_act (None ?)) s2' s2''  ∧
75       ∃t3: raw_trace S2 s2'' s2'''.
76        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
77        ∧ Rrel … rel s1' s2''
78 ; simulate_io_in :
79   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
80   as_execute … (cost_act … (Some ? l)) s1 s1' →
81   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
82   Srel … rel s1 s2 →
83   ∃s2',s2''.∃t: raw_trace … s2 s2'.
84   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
85   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
86; simulate_io_out :
87   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
88   as_execute … (cost_act … (Some ? l)) s1 s1' →
89   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
90   Srel … rel s1 s2 →
91   ∃s2',s2''.∃t : raw_trace … s2' s2''.
92   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
93   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
94 }.
95
96let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
97(t : raw_trace S st1 st2) on t : list CostLabel ≝
98match t with
99[ t_base st ⇒ [ ]
100| t_ind st1' st2' st3' l prf t' ⇒
101    let tl ≝ get_costlabels_of_trace … t' in
102    match l with
103    [ call_act f c ⇒ [ c ]
104    | ret_act x ⇒ match x with
105                  [ Some c ⇒ [ a_return_post c ]
106                  | None ⇒ []
107                  ]
108    | cost_act x ⇒ match x with
109                  [ Some c ⇒ [ a_non_functional_label c ]
110                  | None ⇒ []
111                  ]
112
113   ] @ tl
114].
115
116
117lemma append_premeasurable_silent : ∀S : abstract_status.
118∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
119pre_measurable_trace … t → silent_trace … t' → 
120pre_measurable_trace … (t' @ t).
121#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
122[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
123#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
124[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
125#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
126destruct #_ whd in ⊢ (????%); %2
127[ assumption
128| %{(None ?)} %
129| @IH try assumption
130]
131% assumption
132qed.
133
134lemma pre_silent_is_premeasurable : ∀S : abstract_status.
135∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
136→ pre_measurable_trace … t.
137#S #st1 #st2 #t elim t
138[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
139#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
140-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
141[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
142#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
143@IH assumption
144qed.
145
146lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
147    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
148    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
149#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
150
151lemma append_silent_premeasurable : ∀S : abstract_status.
152∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
153pre_measurable_trace … t' → silent_trace … t →
154pre_measurable_trace … (t' @ t).
155#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
156[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
157  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
158  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
159  %1 assumption
160|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
161  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
162  try ( %{x} %) try @IH try assumption % ]
163#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
164#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
165#r #pre_r normalize
166>append_tind_commute >append_tind_commute >append_associative
167<append_tind_commute in ⊢ (????(??????%)); %5
168try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
169qed.
170
171(*
172lemma append_well_formed_silent : ∀S : abstract_status.
173∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
174well_formed_trace … t → pre_silent_trace … t' →
175(is_trace_non_empty … t' → as_classify … st) →
176well_formed_trace … (t' @ t).
177#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
178[ #st #t #H #_ #_ assumption ]
179#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
180inversion H in ⊢ ?;
181[ #st #EQ1 #EQ2 #EQ3 destruct]
182#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
183#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
184[2: >(Hclass1 I) % #EQ destruct]
185@IH try assumption #_ assumption
186qed.*)
187
188(*
189lemma well_formed_append : ∀S : abstract_status.
190∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
191well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
192#S #st1 #st2 #st3 #t1 #t2 #H %
193[ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
194#H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
195#st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
196#EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
197[ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
198]
199lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
200#s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
201[ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
202#s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
203#_ @IH assumption
204qed.
205
206
207lemma append_well_formed : ∀S : abstract_status.
208∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
209well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
210#S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
211[ #st #r #H1 @H1 ]
212#s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
213try @IH assumption
214qed.
215(*
216lemma silent_is_well_formed : ∀S : abstract_status.
217∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
218#S #st1 #st2 #t elim t [ #st #_ %]
219#s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
220#s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
221[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
222qed.
223*)
224*)
225lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
226∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
227silent_trace … t1 →
228get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
229#S #st1 #st2 #st3 #t1 elim t1
230[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
231[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
232#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
233#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
234#_ whd in ⊢ (??%?); >IH [%] %1 assumption
235qed.
236
237lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
238∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
239get_costlabels_of_trace … (t1 @ t2) =
240 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
241#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
242[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
243qed.
244 
245(*
246lemma raw_trace_ind_r : ∀S : abstract_status.
247∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
248(∀st : S.P … (t_base … st)) →
249(∀st1,st2,st3,l.
250 ∀prf : as_execute S l st2 st3.
251 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
252∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
253#S #P #base #ind #st1 #st2 #t elim t [ assumption]
254#st1 #st2 #st3 #l #prf #raw #IH
255*)
256
257lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
258∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
259as_classify … st1 ≠ cl_io.
260#S #st1 #st2 #t #H inversion H //
261qed.
262
263theorem simulates_pre_mesurable:
264 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
265 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
266  simulation_conditions … rel →
267  pre_measurable_trace … t1 →
268  ∀s2 : S2.
269 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
270  ∃s2'. ∃t2: raw_trace … s2 s2'.
271    pre_measurable_trace … t2 ∧
272    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
273    Srel … rel s1' s2'.
274#S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
275[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
276  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
277| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
278  #pre_measurable_tl #IH #s2 #classify_s2 #REL
279  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
280    #silent_ts2'' cases(IH … RELst2s2'')
281    [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
282        [ #x #EQ1 #EQ2 #EQ3 destruct // ]
283        #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
284    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
285    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
286    whd in ⊢ (??%?); /2/
287  | cases(simulate_label … good … execute … REL)
288    [2,3: /2/]
289    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
290    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
291    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
292    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
293    %
294    [ @append_premeasurable_silent // %2 /2 by ex_intro/
295       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
296         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
297         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
298         cases H47 #ABS @⊥ @ABS % ]
299       @append_premeasurable_silent // % //
300    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
301      [2: assumption] whd in ⊢ (???%);
302      >get_cost_label_invariant_for_append_silent_trace_l //
303    ]
304  ]
305  % assumption
306| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
307  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
308  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
309  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
310  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
311  [2: @(pre_silent_io … sil_t2) assumption]
312  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
313  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
314  % [2: whd in ⊢ (??%?);
315        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
316        whd in ⊢ (???%);
317        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
318        @eq_f assumption ]
319  @append_premeasurable_silent [2: //] %3
320  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
321  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
322  [ #H49 #H50 #H51 #H52 #H53 destruct //]
323  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
324  #ABS @⊥ @ABS %
325| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
326  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
327   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
328   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
329   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
330   cases(IH  … REL)
331   [2: /2 by pre_silent_io/ ]
332   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
333   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
334   [2: whd in ⊢ (??%?);
335        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
336        whd in ⊢ (???%);
337        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
338        @eq_f assumption ]
339   @append_premeasurable_silent try assumption
340     %4 try assumption
341     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
342       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
343       #ABS @⊥ @ABS %
344     | whd %{f} %{lab} %
345     | @append_premeasurable_silent // % assumption
346     ]
347| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
348  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
349  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
350  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
351  #sil_tr2 #call_rel cases(IH1 … REL1)
352  [2: /2 by pre_silent_io/ ]
353  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
354  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
355  #st3'' * #st4' * #st4'' *
356  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
357  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
358  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
359  % [2: assumption] %
360  [ @append_premeasurable_silent try assumption %5
361       [1,2: /2 by pre_silent_io/
362             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
363             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
364             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
365             cases H107 #ABS @⊥ @ABS %
366       | whd %{f} %{l} %
367       | assumption
368       | @append_premeasurable_silent try assumption [2: % //]
369         @append_silent_premeasurable // % //
370       | @append_premeasurable_silent try assumption
371       | @(RET_REL … call_rel) assumption
372       | %
373       ]
374  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
375    whd in ⊢ (??%%); @eq_f >append_associative
376    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
377    [2: % // ] >append_associative
378    >get_cost_label_append in ⊢ (???%);
379    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
380    [2: % //] normalize
381    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
382    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
383    assumption
384  ]
385  % //
386]
387qed.
388
389
390(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
391   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
392   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
393
394(* measurable fattorizzata sotto come measurable'
395definition measurable ≝
396 λL,s1,s2.λt: raw_trace … s1 s2.
397  ∃L',s0,so. as_execute … s0 s1 L ∧
398  pre_measurable_trace … t ∧
399  well_formed_trace … t ∧
400  as_execute … s2 so L'. *)
401
402record measurable_trace (S : abstract_status) : Type[0] ≝
403 { L_label: option ActionLabel
404 ; R_label : option ActionLabel
405 ; L_pre_state : option S
406 ; L_s1 : S
407 ; R_s2: S
408 ; R_post_state : option S
409 ; trace : raw_trace S L_s1 R_s2
410 ; pre_meas : pre_measurable_trace … trace
411 ; L_init_ok : match L_pre_state with
412               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
413               | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
414                          as_execute … l s L_s1
415               ]
416 ; R_fin_ok : match R_label with
417               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
418               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
419                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
420                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
421               ]
422}.
423
424lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
425#P #H1 #H2 * // @H2 % #EQ destruct qed.
426
427lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
428* [2: %%] %2 % #EQ destruct qed.
429
430lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
431∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
432as_classify … st2 ≠ cl_io.
433#S #st1 #st2 #t #H elim H //
434qed.
435
436lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
437∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
438#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
439#H inversion H
440[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
441destruct #_ @IH % assumption
442qed.
443
444lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
445∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
446silent_trace … t2 →
447get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
448#S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
449>(get_cost_label_silent_is_empty … H) //
450qed.
451
452lemma instr_execute_commute : ∀S1,S2 :abstract_status.
453∀rel : relations S1 S2.
454simulation_conditions … rel →
455∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
456(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
457∀s2.
458Srel … rel s1 s2 →
459∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧
460∃s2'' : S2.as_execute … l s2' s2'' ∧ ∃s2''' : S2.
461∃tr' : raw_trace … s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
462(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
463(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
464#S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
465[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
466  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
467  cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
468  #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
469  %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
470  [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
471     assumption ] % [  %//  % // ] * #f * #l #EQ destruct
472| #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
473  [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
474    cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
475    *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
476    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
477     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
478  | #Hclass_s1' cases l in prf l_notau;
479    [ #f #l #prf #_ inversion(is_call_post_label … s1)
480      [ #Hpost cases(simulate_call_pl … good … prf … REL)
481        [2: >Hpost % |3,4: assumption]
482        #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
483        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
484        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
485        % [ /4 by or_introl, conj/ ] /3 by /
486     | #Hpost cases(simulate_call_n … good … prf … REL)
487       [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
488       *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
489       %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
490       % [2: #_ *] % //
491     ]
492   | *
493     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
494       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
495       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
496       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
497       % [ % // % // ] * #f * #l #EQ destruct
498     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
499       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
500       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
501       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
502       % [ % // % //] * #f * #l #EQ destruct
503    ]
504  | * [ #_ * #H @⊥ @H % ] #lab #prf #_
505    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
506    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
507    %{s2'''} %{t3} %
508    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
509    % [% // % //] * #f * #l #EQ destruct
510  ]
511  % //
512]
513qed.
514
515theorem simulate_LR_trace :
516∀S1,S2 : abstract_status.
517∀t : measurable_trace S1.
518∀rel : relations S1 S2.
519simulation_conditions … rel →
520∀s2 : S2.
521match L_pre_state … t with
522[ None ⇒
523   as_classify … s2 ≠ cl_io ∧
524   Srel … rel (L_s1 … t) s2 
525| Some s1 ⇒ Srel … rel s1 s2 ] →
526∃t' : measurable_trace S2.
527 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
528 get_costlabels_of_trace … (trace … t) =
529  get_costlabels_of_trace … (trace … t') ∧
530match L_pre_state … t with
531[ None ⇒ L_s1 … t' = s2
532| Some s1 ⇒
533         ∃ pre_state : S2.
534         L_pre_state … t' = Some ? pre_state ∧
535         ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i
536] ∧
537match R_post_state … t with         
538[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
539| Some s1' ⇒
540          ∃s2' : S2. Srel … rel s1' s2' ∧
541          ∃ post_state : S2.
542          R_post_state … t' = Some ? post_state ∧
543          ∃tr : raw_trace … post_state s2'. silent_trace … tr
544].
545#S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
546[2: #REL_pre
547    cut
548     (∃pre_state.∃ l.
549      ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i ∧
550      ∃middle_state.L_label … t = Some ? l ∧
551       as_execute … l pre_state middle_state ∧
552      ∃final_state.
553      ∃tr_i2: raw_trace … middle_state final_state. silent_trace … tr_i2 ∧
554       as_classify … final_state ≠ cl_io ∧
555       Srel … rel (L_s1 … t) final_state)
556      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
557      cases(instr_execute_commute … good … l … exe … REL_pre)
558      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
559      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
560      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
561      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
562      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
563      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
564      #H @⊥ @H %]
565    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
566    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
567| #REL
568  cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?)
569      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
570        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
571]
572cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
573#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
574[2,4: #post_s2] #EQpost normalize nodelta
575[3,4: cut (match R_label … t in option return λ_:(option ActionLabel).Prop with 
576 [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2
577 |Some (l:ActionLabel)⇒
578  (is_costlabelled_act l∨is_unlabelled_ret_act l)
579  ∧(is_call_act l→is_call_post_label … fin_s2)
580  ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')])
581  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
582      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
583      |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
584      ]
585  ] #R_label_fin
586|*: cut(∃l.(R_label … t) = Some ? l)
587    [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
588          #a #_ %{a} % ] * #final_label #EQfinal_label
589     cut
590      (∃middle_state.
591       ∃tr : raw_trace … fin_s2 middle_state. silent_trace … tr ∧
592       ∃post_state.
593       as_execute … final_label middle_state post_state ∧
594       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
595       ∃final_state.
596       ∃tr_f2: raw_trace … post_state final_state. silent_trace … tr_f2 ∧
597       Srel … rel post_s2 final_state)
598     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
599         * >EQpost #EQ destruct #exe
600          cases(instr_execute_commute … good … final_label … exe … REL')
601          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
602          |3,6: %1 @tail_of_premeasurable_is_not_io //
603          ]
604          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
605          #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
606          % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
607     #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
608]
609[2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
610     normalize nodelta /5 by conj/
611|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
612    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
613      #EQ destruct //
614    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
615    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
616        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
617        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
618        /2 by refl, pair_destruct_1/
619    | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
620      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
621    ]
622| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
623  normalize nodelta
624  [ assumption
625  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
626  | /4 by append_premeasurable_silent/
627  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
628    >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
629  ]
630| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
631  normalize nodelta
632 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
633      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
634 | /2/
635 | /3 by append_silent_premeasurable/
636 | % [2: %{final_state'} /5 by ex_intro, conj/
637 | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
638   // ]
639 ]   
640]
641qed.   
642(*
643xxxxxxxxxxxxxxxxxxxx
644 
645theorem simulate_LR_trace :
646∀S : abstract_status.
647∀t : measurable_trace S.
648∀rel : relations S.
649simulation_conditions … rel →
650∀s2 : S.
651match L_pre_state … t with
652[ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
653         ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
654         L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
655         get_costlabels_of_trace … (trace … t) =
656                      get_costlabels_of_trace … (trace … t') ∧
657         match R_post_state … t with
658         [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
659         | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
660                      ∃post_state : S.
661                      ∃tr : raw_trace S (opt_safe … prf) post_state.
662                      silent_trace … tr ∧ Srel … rel s2' post_state
663         ]
664| Some s1 ⇒ Srel … rel s1 s2 →
665            ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
666            silent_trace … tr_i ∧
667            ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
668            L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
669            get_costlabels_of_trace … (trace … t) =
670                      get_costlabels_of_trace … (trace … t') ∧
671            match R_post_state … t with         
672            [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
673            | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
674                         ∃post_state : S.
675                         ∃tr : raw_trace S (opt_safe … prf) post_state.
676                         silent_trace … tr ∧ Srel … rel s2' post_state
677            ]
678].
679#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
680#REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
681[1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
682     #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
683     [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
684         [ inversion(R_label … t) normalize nodelta
685           [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
686             >EQnone normalize nodelta * //
687           | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
688             >EQpost #EQ destruct
689           ]
690         | normalize nodelta %
691           [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
692           >EQpre normalize nodelta * //
693         | /6 by conj/
694         ]
695     | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
696       #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
697       #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
698       [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
699         * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
700         [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
701         ** #sil_t1 #exe' #Hx2 #REL1
702         %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
703         [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
704           @notb_Prop % #ABS @(as_final_ok … ABS exe')
705         | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
706           -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
707         | /3 by append_silent_premeasurable/
708         | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
709           [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
710         ]
711       | (*go by cases on the instruction executed TODO *) cases daemon
712       ]
713    ]
714|*: cases daemon (*TODO*)
715]
716qed.
717
718
719
720
721#L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
722normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
723* [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
724
725
726whd in ⊢ (% → ?);
727
728
729
730
731(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
732  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
733  il teorema sotto sembra suggerire il merge *)
734
735definition unmovable_entry_label ≝
736λS : abstract_status.λl.
737match l with
738[ call_act _ _ ⇒ false
739| ret_act _ ⇒ false
740| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
741                            | None ⇒ false
742                            ]
743].
744 
745definition unmovable_exit_label ≝
746λS : abstract_status.λl.
747match l with
748[ call_act _ _ ⇒ false
749| ret_act _ ⇒ false
750| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
751                            | None ⇒ false
752                            ]
753].
754
755theorem simulates_LR_raw_trace :
756∀S : abstract_status.
757∀t : LR_raw_trace S.
758∀rel : relations S.
759simulation_conditions … rel →
760measurable S t →
761∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
762∃ t' : LR_raw_trace S.
763measurable S t' ∧
764if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
765   LR_s1 … t' = s1'
766else
767   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
768∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
769if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
770   LR_s2 … t' = s1''
771else
772  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
773
774get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
775#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
776cases(simulates_pre_mesurable … (LR_t … t) … REL)
777[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
778#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
779inversion(as_initial … (LR_s1 … t)) #Has_initial
780inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
781inversion(as_final … (LR_s2 … t)) #Has_final
782inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
783normalize nodelta
784[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
785
786
787
788qed.
789
790xxxx
791
792theorem simulates_L_raw_trace:
793 ∀t: L_raw_trace.
794  pre_measurable_trace … (L_t t1) →
795  well_formed_trace … (L_t t1) →
796 ∀s1'.
797   S (L_s1 t) s1' →
798   s1' -flat-→ (L_s1 t2) →
799   ∃s2',t2: L_raw_trace.
800    pre_mesurable_trace … (L_t t2) ∧
801    well_formed_trace … (L_t t2) ∧
802    |t1| = |t2| ∧
803    S (L_s2 t1) s2' ∧
804    (L_s2 t2) -flat-→ s2'.
805 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
806       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
807
808
809(*********************************************************************)
810
811(* quello che segue tentava di permettere di evitare l'emissione di label
812   associate a codice morto *)
813
814replace_last x : weak_trace → weak_trace
815   [] ⇒ [], Some x
816 | l::t ⇒
817     let 〈t',x'〉 ≝ replace_last x t in
818     match x' with
819     [ None ⇒ l::t', None
820     | Some x'' ⇒ [], Some x''
821
822theorem simulates:
823 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
824  pre_measurable_trace … t1 →
825  well_formed_trace … t1.
826 ∀l1: option NonFunctionalLabel.
827 ∀s1'.
828   S s1 s1' →
829   ∃dead_labels.
830   ∃s2'. ∃t2: raw_trace … s1' s2'.
831    pre_mesurable_trace … t2 ∧
832    well_formed_trace … t2.
833   ∃l2: option NonFunctionalLabel.
834    match l1 with
835    [ None ⇒
836       match l2 with
837       [ None ⇒ |t1| = |t2|
838       | Some l2' ⇒ |t1| = l2'::|t2| ]
839    | Some l1' ⇒
840       match l2 with
841       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
842       | Some l2' ⇒
843          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
844          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
845       ]
846    ]
847    *)
Note: See TracBrowser for help on using the repository browser.