source: LTS/Simulation.ma @ 3486

Last change on this file since 3486 was 3486, checked in by piccolo, 5 years ago
File size: 36.6 KB
Line 
1include "Traces.ma".
2
3record relations (S : abstract_status) : Type[0] ≝
4 { Srel: S → S → Prop
5 ; Crel: S → S → Prop
6 }.
7
8definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S.
9 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
10
11record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
12 { initial_is_initial :
13   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
14 ; final_is_final :
15   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
16 ; simulate_tau:
17     ∀s1,s2,s1' : S.
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 S s2 s2'.
21        Srel … rel s1' s2' ∧ silent_trace … t
22 ; simulate_label:
23     ∀s1,s2,l,s1'.
24      as_execute S (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 S s2 s2'.
29       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
30       ∃t3: raw_trace S s2'' s2'''.
31        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
32 ; simulate_call_pl:
33     ∀s1,s2,s1' : S.∀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 S s2 s2'.
40       as_execute … (call_act f l) s2' s2'' ∧
41       bool_to_Prop(is_call_post_label … s2') ∧
42       ∃t3: raw_trace S s2'' s2'''.
43        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
44 ; simulate_ret_l:
45     ∀s1,s2,s1' : S.∀l.
46      as_execute S (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 S s2 s2'.
51       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
52       ∃t3: raw_trace S s2'' s2'''.
53        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
54 ; simulate_call_n:
55     ∀s1,s2,s1' : S.∀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 S s2 s2'.
62       bool_to_Prop (¬ is_call_post_label … s2') ∧
63       as_execute … (call_act f l) s2' s2'' ∧
64       ∃t3: raw_trace S 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,s2,s1' : S.
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'''.
73       ∃t1: raw_trace S s2 s2'.
74       as_execute … (ret_act (None ?)) s2' s2''  ∧
75       ∃t3: raw_trace S 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,s2,s1' : S.∀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'' : S.∃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,s2,s1' : S.∀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'' : S.∃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
263
264theorem simulates_pre_mesurable:
265 ∀S : abstract_status.∀rel : relations S.
266 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
267  simulation_conditions S rel →
268  pre_measurable_trace … t1 →
269  ∀s2 : S.
270 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
271  ∃s2'. ∃t2: raw_trace … s2 s2'.
272    pre_measurable_trace … t2 ∧
273    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
274    Srel … rel s1' s2'.
275#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
276[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
277  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
278| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
279  #pre_measurable_tl #IH #s2 #classify_s2 #REL
280  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
281    #silent_ts2'' cases(IH … RELst2s2'')
282    [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
283        [ #x #EQ1 #EQ2 #EQ3 destruct // ]
284        #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
285    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
286    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
287    whd in ⊢ (??%?); /2/
288  | cases(simulate_label … good … execute … REL)
289    [2,3: /2/]
290    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
291    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
292    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
293    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
294    %
295    [ @append_premeasurable_silent // %2 /2 by ex_intro/
296       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
297         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
298         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
299         cases H47 #ABS @⊥ @ABS % ]
300       @append_premeasurable_silent // % //
301    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
302      [2: assumption] whd in ⊢ (???%);
303      >get_cost_label_invariant_for_append_silent_trace_l //
304    ]
305  ]
306  % assumption
307| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
308  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
309  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
310  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
311  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
312  [2: @(pre_silent_io … sil_t2) assumption]
313  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
314  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
315  % [2: whd in ⊢ (??%?);
316        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
317        whd in ⊢ (???%);
318        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
319        @eq_f assumption ]
320  @append_premeasurable_silent [2: //] %3
321  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
322  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
323  [ #H49 #H50 #H51 #H52 #H53 destruct //]
324  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
325  #ABS @⊥ @ABS %
326| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
327  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
328   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
329   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
330   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
331   cases(IH  … REL)
332   [2: /2 by pre_silent_io/ ]
333   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
334   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
335   [2: whd in ⊢ (??%?);
336        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
337        whd in ⊢ (???%);
338        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
339        @eq_f assumption ]
340   @append_premeasurable_silent try assumption
341     %4 try assumption
342     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
343       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
344       #ABS @⊥ @ABS %
345     | whd %{f} %{lab} %
346     | @append_premeasurable_silent // % assumption
347     ]
348| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
349  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
350  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
351  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
352  #sil_tr2 #call_rel cases(IH1 … REL1)
353  [2: /2 by pre_silent_io/ ]
354  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
355  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
356  #st3'' * #st4' * #st4'' *
357  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
358  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
359  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
360  % [2: assumption] %
361  [ @append_premeasurable_silent try assumption %5
362       [1,2: /2 by pre_silent_io/
363             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
364             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
365             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
366             cases H107 #ABS @⊥ @ABS %
367       | whd %{f} %{l} %
368       | assumption
369       | @append_premeasurable_silent try assumption [2: % //]
370         @append_silent_premeasurable // % //
371       | @append_premeasurable_silent try assumption
372       | @(RET_REL … call_rel) assumption
373       | %
374       ]
375  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
376    whd in ⊢ (??%%); @eq_f >append_associative
377    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
378    [2: % // ] >append_associative
379    >get_cost_label_append in ⊢ (???%);
380    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
381    [2: % //] normalize
382    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
383    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
384    assumption
385  ]
386  % //
387]
388qed.
389
390
391(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
392   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
393   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
394
395(* measurable fattorizzata sotto come measurable'
396definition measurable ≝
397 λL,s1,s2.λt: raw_trace … s1 s2.
398  ∃L',s0,so. as_execute … s0 s1 L ∧
399  pre_measurable_trace … t ∧
400  well_formed_trace … t ∧
401  as_execute … s2 so L'. *)
402
403record measurable_trace (S : abstract_status) : Type[0] ≝
404 { L_s1 : S
405 ; R_s2: S
406 ; trace : raw_trace S L_s1 R_s2
407 ; pre_meas : pre_measurable_trace … trace
408 }.
409
410lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
411#P #H1 #H2 * // @H2 % #EQ destruct qed.
412
413lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
414* [2: %%] %2 % #EQ destruct qed.
415
416lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
417∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
418as_classify … st2 ≠ cl_io.
419#S #st1 #st2 #t #H elim H //
420qed.
421
422lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
423∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
424#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
425#H inversion H
426[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
427destruct #_ @IH % assumption
428qed.
429
430lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
431∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
432silent_trace … t2 →
433get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
434#S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
435>(get_cost_label_silent_is_empty … H) //
436qed.
437
438lemma instr_execute_commute : ∀S :abstract_status.
439∀rel : relations S.
440simulation_conditions … rel →
441∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
442(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
443∀s2.
444Srel … rel s1 s2 →
445∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
446∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
447∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
448(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
449(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
450#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
451[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
452  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
453  cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
454  #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
455  %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
456  [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
457     assumption ] % [  %//  % // ] * #f * #l #EQ destruct
458| #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
459  [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
460    cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
461    *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
462    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
463     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
464  | #Hclass_s1' cases l in prf l_notau;
465    [ #f #l #prf #_ inversion(is_call_post_label … s1)
466      [ #Hpost cases(simulate_call_pl … good … prf … REL)
467        [2: >Hpost % |3,4: assumption]
468        #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
469        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
470        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
471        % [ /4 by or_introl, conj/ ] /3 by /
472     | #Hpost cases(simulate_call_n … good … prf … REL)
473       [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
474       *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
475       %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
476       % [2: #_ *] % //
477     ]
478   | *
479     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
480       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
481       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
482       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
483       % [ % // % // ] * #f * #l #EQ destruct
484     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
485       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
486       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
487       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
488       % [ % // % //] * #f * #l #EQ destruct
489    ]
490  | * [ #_ * #H @⊥ @H % ] #lab #prf #_
491    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
492    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
493    %{s2'''} %{t3} %
494    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
495    % [% // % //] * #f * #l #EQ destruct
496  ]
497  % //
498]
499qed.
500
501(*
502theorem simulate_LR_trace :
503∀S : abstract_status.
504∀t : measurable_trace S.
505∀rel : relations S.
506simulation_conditions … rel →
507∀s2 : S.
508match L_pre_state … t with
509[ None ⇒
510   as_classify … s2 ≠ cl_io ∧
511   Srel … rel (L_s1 … t) s2 
512| Some s1 ⇒ Srel … rel s1 s2 ] →
513∃t' : measurable_trace S.
514 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
515 get_costlabels_of_trace … (trace … t) =
516  get_costlabels_of_trace … (trace … t') ∧
517match L_pre_state … t with
518[ None ⇒ L_s1 … t' = s2
519| Some s1 ⇒
520         ∃ pre_state : S.
521         L_pre_state … t' = Some ? pre_state ∧
522         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
523] ∧
524match R_post_state … t with         
525[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
526| Some s1' ⇒
527          ∃s2' : S. Srel … rel s1' s2' ∧
528          ∃ post_state : S.
529          R_post_state … t' = Some ? post_state ∧
530          ∃tr : raw_trace S post_state s2'. silent_trace … tr
531].
532#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
533[2: #REL_pre
534    cut
535     (∃pre_state: S.∃ l.
536      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
537      ∃middle_state: S.L_label … t = Some ? l ∧
538       as_execute … l pre_state middle_state ∧
539      ∃final_state: S.
540      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
541       as_classify … final_state ≠ cl_io ∧
542       Srel … rel (L_s1 … t) final_state)
543      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
544      cases(instr_execute_commute … good … l … exe … REL_pre)
545      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
546      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
547      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
548      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
549      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
550      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
551      #H @⊥ @H %]
552    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
553    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
554| #REL
555  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
556      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
557        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
558]
559cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
560#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
561[2,4: #post_s2] #EQpost normalize nodelta
562[3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
563 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
564 |Some (l:ActionLabel)⇒
565  (is_costlabelled_act l∨is_unlabelled_ret_act l)
566  ∧(is_call_act l→is_call_post_label S fin_s2)
567  ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
568  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
569      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
570      |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
571      ]
572  ] #R_label_fin
573|*: cut(∃l.(R_label … t) = Some ? l)
574    [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
575          #a #_ %{a} % ] * #final_label #EQfinal_label
576     cut
577      (∃middle_state: S.
578       ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
579       ∃post_state : S.
580       as_execute … final_label middle_state post_state ∧
581       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
582       ∃final_state: S.
583       ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
584       Srel … rel post_s2 final_state)
585     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
586         * >EQpost #EQ destruct #exe
587          cases(instr_execute_commute … good … final_label … exe … REL')
588          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
589          |3,6: %1 @tail_of_premeasurable_is_not_io //
590          ]
591          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
592          #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
593          % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
594     #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
595]
596[2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
597     normalize nodelta /5 by conj/
598|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
599    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
600      #EQ destruct //
601    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
602    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
603        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
604        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
605        /2 by refl, pair_destruct_1/
606    | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
607      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
608    ]
609| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
610  normalize nodelta
611  [ assumption
612  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
613  | /4 by append_premeasurable_silent/
614  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
615    >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
616  ]
617| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
618  normalize nodelta
619 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
620      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
621 | /2/
622 | /3 by append_silent_premeasurable/
623 | % [2: %{final_state'} /5 by ex_intro, conj/
624 | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
625   // ]
626 ]   
627]
628qed.   
629(*
630xxxxxxxxxxxxxxxxxxxx
631 
632theorem simulate_LR_trace :
633∀S : abstract_status.
634∀t : measurable_trace S.
635∀rel : relations S.
636simulation_conditions … rel →
637∀s2 : S.
638match L_pre_state … t with
639[ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
640         ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
641         L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
642         get_costlabels_of_trace … (trace … t) =
643                      get_costlabels_of_trace … (trace … t') ∧
644         match R_post_state … t with
645         [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
646         | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
647                      ∃post_state : S.
648                      ∃tr : raw_trace S (opt_safe … prf) post_state.
649                      silent_trace … tr ∧ Srel … rel s2' post_state
650         ]
651| Some s1 ⇒ Srel … rel s1 s2 →
652            ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
653            silent_trace … tr_i ∧
654            ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
655            L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
656            get_costlabels_of_trace … (trace … t) =
657                      get_costlabels_of_trace … (trace … t') ∧
658            match R_post_state … t with         
659            [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
660            | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
661                         ∃post_state : S.
662                         ∃tr : raw_trace S (opt_safe … prf) post_state.
663                         silent_trace … tr ∧ Srel … rel s2' post_state
664            ]
665].
666#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
667#REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
668[1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
669     #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
670     [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
671         [ inversion(R_label … t) normalize nodelta
672           [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
673             >EQnone normalize nodelta * //
674           | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
675             >EQpost #EQ destruct
676           ]
677         | normalize nodelta %
678           [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
679           >EQpre normalize nodelta * //
680         | /6 by conj/
681         ]
682     | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
683       #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
684       #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
685       [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
686         * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
687         [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
688         ** #sil_t1 #exe' #Hx2 #REL1
689         %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
690         [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
691           @notb_Prop % #ABS @(as_final_ok … ABS exe')
692         | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
693           -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
694         | /3 by append_silent_premeasurable/
695         | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
696           [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
697         ]
698       | (*go by cases on the instruction executed TODO *) cases daemon
699       ]
700    ]
701|*: cases daemon (*TODO*)
702]
703qed.
704
705
706
707
708#L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
709normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
710* [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
711
712
713whd in ⊢ (% → ?);
714
715
716
717
718(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
719  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
720  il teorema sotto sembra suggerire il merge *)
721
722definition unmovable_entry_label ≝
723λS : abstract_status.λl.
724match l with
725[ call_act _ _ ⇒ false
726| ret_act _ ⇒ false
727| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
728                            | None ⇒ false
729                            ]
730].
731 
732definition unmovable_exit_label ≝
733λS : abstract_status.λl.
734match l with
735[ call_act _ _ ⇒ false
736| ret_act _ ⇒ false
737| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
738                            | None ⇒ false
739                            ]
740].
741
742theorem simulates_LR_raw_trace :
743∀S : abstract_status.
744∀t : LR_raw_trace S.
745∀rel : relations S.
746simulation_conditions … rel →
747measurable S t →
748∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
749∃ t' : LR_raw_trace S.
750measurable S t' ∧
751if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
752   LR_s1 … t' = s1'
753else
754   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
755∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
756if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
757   LR_s2 … t' = s1''
758else
759  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
760
761get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
762#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
763cases(simulates_pre_mesurable … (LR_t … t) … REL)
764[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
765#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
766inversion(as_initial … (LR_s1 … t)) #Has_initial
767inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
768inversion(as_final … (LR_s2 … t)) #Has_final
769inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
770normalize nodelta
771[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
772
773
774
775qed.
776
777xxxx
778
779theorem simulates_L_raw_trace:
780 ∀t: L_raw_trace.
781  pre_measurable_trace … (L_t t1) →
782  well_formed_trace … (L_t t1) →
783 ∀s1'.
784   S (L_s1 t) s1' →
785   s1' -flat-→ (L_s1 t2) →
786   ∃s2',t2: L_raw_trace.
787    pre_mesurable_trace … (L_t t2) ∧
788    well_formed_trace … (L_t t2) ∧
789    |t1| = |t2| ∧
790    S (L_s2 t1) s2' ∧
791    (L_s2 t2) -flat-→ s2'.
792 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
793       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
794
795
796(*********************************************************************)
797
798(* quello che segue tentava di permettere di evitare l'emissione di label
799   associate a codice morto *)
800
801replace_last x : weak_trace → weak_trace
802   [] ⇒ [], Some x
803 | l::t ⇒
804     let 〈t',x'〉 ≝ replace_last x t in
805     match x' with
806     [ None ⇒ l::t', None
807     | Some x'' ⇒ [], Some x''
808
809theorem simulates:
810 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
811  pre_measurable_trace … t1 →
812  well_formed_trace … t1.
813 ∀l1: option NonFunctionalLabel.
814 ∀s1'.
815   S s1 s1' →
816   ∃dead_labels.
817   ∃s2'. ∃t2: raw_trace … s1' s2'.
818    pre_mesurable_trace … t2 ∧
819    well_formed_trace … t2.
820   ∃l2: option NonFunctionalLabel.
821    match l1 with
822    [ None ⇒
823       match l2 with
824       [ None ⇒ |t1| = |t2|
825       | Some l2' ⇒ |t1| = l2'::|t2| ]
826    | Some l1' ⇒
827       match l2 with
828       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
829       | Some l2' ⇒
830          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
831          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
832       ]
833    ]
834    *)
835*)
Note: See TracBrowser for help on using the repository browser.