source: LTS/Simulation.ma @ 3482

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

Repaired.

File size: 37.3 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_label: option ActionLabel
405 ; R_label : option ActionLabel
406 ; L_pre_state : option S
407 ; L_s1 : S
408 ; R_s2: S
409 ; R_post_state : option S
410 ; trace : raw_trace S L_s1 R_s2
411 ; pre_meas : pre_measurable_trace … trace
412 ; L_init_ok : match L_pre_state with
413               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?
414               | Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧
415                          as_execute … l s L_s1
416               ]
417 ; R_fin_ok : match R_label with
418               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
419               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
420                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
421                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
422               ]
423}.
424
425lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
426#P #H1 #H2 * // @H2 % #EQ destruct qed.
427
428lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
429* [2: %%] %2 % #EQ destruct qed.
430
431lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
432∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
433as_classify … st2 ≠ cl_io.
434#S #st1 #st2 #t #H elim H //
435qed.
436
437lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
438∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
439#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
440#H inversion H
441[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
442destruct #_ @IH % assumption
443qed.
444
445lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
446∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
447silent_trace … t2 →
448get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
449#S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
450>(get_cost_label_silent_is_empty … H) //
451qed.
452
453lemma instr_execute_commute : ∀S :abstract_status.
454∀rel : relations S.
455simulation_conditions … rel →
456∀s1,s1': S.∀l.l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
457(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
458∀s2.
459Srel … rel s1 s2 →
460∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
461∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
462∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
463(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
464(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
465#S #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
466[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
467  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
468  cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
469  #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
470  %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
471  [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
472     assumption ] % [  %//  % // ] * #f * #l #EQ destruct
473| #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
474  [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
475    cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
476    *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
477    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
478     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
479  | #Hclass_s1' cases l in prf l_notau;
480    [ #f #l #prf #_ inversion(is_call_post_label … s1)
481      [ #Hpost cases(simulate_call_pl … good … prf … REL)
482        [2: >Hpost % |3,4: assumption]
483        #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
484        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
485        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
486        % [ /4 by or_introl, conj/ ] /3 by /
487     | #Hpost cases(simulate_call_n … good … prf … REL)
488       [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
489       *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
490       %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
491       % [2: #_ *] % //
492     ]
493   | *
494     [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
495       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
496       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
497       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
498       % [ % // % // ] * #f * #l #EQ destruct
499     | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
500       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
501       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
502       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
503       % [ % // % //] * #f * #l #EQ destruct
504    ]
505  | * [ #_ * #H @⊥ @H % ] #lab #prf #_
506    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
507    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
508    %{s2'''} %{t3} %
509    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
510    % [% // % //] * #f * #l #EQ destruct
511  ]
512  % //
513]
514qed.
515
516
517theorem simulate_LR_trace :
518∀S : abstract_status.
519∀t : measurable_trace S.
520∀rel : relations S.
521simulation_conditions … rel →
522∀s2 : S.
523match L_pre_state … t with
524[ None ⇒
525   as_classify … s2 ≠ cl_io ∧
526   Srel … rel (L_s1 … t) s2 
527| Some s1 ⇒ Srel … rel s1 s2 ] →
528∃t' : measurable_trace S.
529 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
530 get_costlabels_of_trace … (trace … t) =
531  get_costlabels_of_trace … (trace … t') ∧
532match L_pre_state … t with
533[ None ⇒ L_s1 … t' = s2
534| Some s1 ⇒
535         ∃ pre_state : S.
536         L_pre_state … t' = Some ? pre_state ∧
537         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
538] ∧
539match R_post_state … t with         
540[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
541| Some s1' ⇒
542          ∃s2' : S. Srel … rel s1' s2' ∧
543          ∃ post_state : S.
544          R_post_state … t' = Some ? post_state ∧
545          ∃tr : raw_trace S post_state s2'. silent_trace … tr
546].
547#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
548[2: #REL_pre
549    cut
550     (∃pre_state: S.∃ l.
551      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
552      ∃middle_state: S.L_label … t = Some ? l ∧
553       as_execute … l pre_state middle_state ∧
554      ∃final_state: S.
555      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
556       as_classify … final_state ≠ cl_io ∧
557       Srel … rel (L_s1 … t) final_state)
558      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe   
559      cases(instr_execute_commute … good … l … exe … REL_pre)
560      [2: % #EQ >EQ in Hcost; * |3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
561      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
562      #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % //
563      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
564      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
565      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
566      #H @⊥ @H %]
567    * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle
568    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
569| #REL
570  cut(bool_to_Prop (as_initial S s2)∧L_label S t=None ?)
571      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
572        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
573]
574cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
575#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
576[2,4: #post_s2] #EQpost normalize nodelta
577[3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
578 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
579 |Some (l:ActionLabel)⇒
580  (is_costlabelled_act l∨is_unlabelled_ret_act l)
581  ∧(is_call_act l→is_call_post_label S fin_s2)
582  ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
583  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
584      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
585      |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
586      ]
587  ] #R_label_fin
588|*: cut(∃l.(R_label … t) = Some ? l)
589    [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
590          #a #_ %{a} % ] * #final_label #EQfinal_label
591     cut
592      (∃middle_state: S.
593       ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
594       ∃post_state : S.
595       as_execute … final_label middle_state post_state ∧
596       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
597       ∃final_state: S.
598       ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
599       Srel … rel post_s2 final_state)
600     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
601         * >EQpost #EQ destruct #exe
602          cases(instr_execute_commute … good … final_label … exe … REL')
603          [2,5: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
604          |3,6: %1 @tail_of_premeasurable_is_not_io //
605          ]
606          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
607          #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
608          % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
609     #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
610]
611[2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
612     normalize nodelta /5 by conj/
613|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
614    normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl'
615      #EQ destruct //
616    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
617    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
618        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
619        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
620        /2 by refl, pair_destruct_1/
621    | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
622      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
623    ]
624| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
625  normalize nodelta
626  [ assumption
627  | %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct //
628  | /4 by append_premeasurable_silent/
629  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
630    >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
631  ]
632| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
633  normalize nodelta
634 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
635      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
636 | /2/
637 | /3 by append_silent_premeasurable/
638 | % [2: %{final_state'} /5 by ex_intro, conj/
639 | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
640   // ]
641 ]   
642]
643qed.   
644(*
645xxxxxxxxxxxxxxxxxxxx
646 
647theorem simulate_LR_trace :
648∀S : abstract_status.
649∀t : measurable_trace S.
650∀rel : relations S.
651simulation_conditions … rel →
652∀s2 : S.
653match L_pre_state … t with
654[ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
655         ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
656         L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
657         get_costlabels_of_trace … (trace … t) =
658                      get_costlabels_of_trace … (trace … t') ∧
659         match R_post_state … t with
660         [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
661         | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
662                      ∃post_state : S.
663                      ∃tr : raw_trace S (opt_safe … prf) post_state.
664                      silent_trace … tr ∧ Srel … rel s2' post_state
665         ]
666| Some s1 ⇒ Srel … rel s1 s2 →
667            ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
668            silent_trace … tr_i ∧
669            ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
670            L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
671            get_costlabels_of_trace … (trace … t) =
672                      get_costlabels_of_trace … (trace … t') ∧
673            match R_post_state … t with         
674            [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
675            | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
676                         ∃post_state : S.
677                         ∃tr : raw_trace S (opt_safe … prf) post_state.
678                         silent_trace … tr ∧ Srel … rel s2' post_state
679            ]
680].
681#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
682#REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
683[1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
684     #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
685     [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
686         [ inversion(R_label … t) normalize nodelta
687           [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
688             >EQnone normalize nodelta * //
689           | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
690             >EQpost #EQ destruct
691           ]
692         | normalize nodelta %
693           [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
694           >EQpre normalize nodelta * //
695         | /6 by conj/
696         ]
697     | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
698       #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
699       #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
700       [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
701         * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
702         [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
703         ** #sil_t1 #exe' #Hx2 #REL1
704         %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
705         [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
706           @notb_Prop % #ABS @(as_final_ok … ABS exe')
707         | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
708           -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
709         | /3 by append_silent_premeasurable/
710         | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
711           [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
712         ]
713       | (*go by cases on the instruction executed TODO *) cases daemon
714       ]
715    ]
716|*: cases daemon (*TODO*)
717]
718qed.
719
720
721
722
723#L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
724normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
725* [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
726
727
728whd in ⊢ (% → ?);
729
730
731
732
733(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
734  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
735  il teorema sotto sembra suggerire il merge *)
736
737definition unmovable_entry_label ≝
738λS : abstract_status.λl.
739match l with
740[ call_act _ _ ⇒ false
741| ret_act _ ⇒ false
742| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
743                            | None ⇒ false
744                            ]
745].
746 
747definition unmovable_exit_label ≝
748λS : abstract_status.λl.
749match l with
750[ call_act _ _ ⇒ false
751| ret_act _ ⇒ false
752| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
753                            | None ⇒ false
754                            ]
755].
756
757theorem simulates_LR_raw_trace :
758∀S : abstract_status.
759∀t : LR_raw_trace S.
760∀rel : relations S.
761simulation_conditions … rel →
762measurable S t →
763∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
764∃ t' : LR_raw_trace S.
765measurable S t' ∧
766if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
767   LR_s1 … t' = s1'
768else
769   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
770∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
771if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
772   LR_s2 … t' = s1''
773else
774  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
775
776get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
777#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
778cases(simulates_pre_mesurable … (LR_t … t) … REL)
779[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
780#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
781inversion(as_initial … (LR_s1 … t)) #Has_initial
782inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
783inversion(as_final … (LR_s2 … t)) #Has_final
784inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
785normalize nodelta
786[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
787
788
789
790qed.
791
792xxxx
793
794theorem simulates_L_raw_trace:
795 ∀t: L_raw_trace.
796  pre_measurable_trace … (L_t t1) →
797  well_formed_trace … (L_t t1) →
798 ∀s1'.
799   S (L_s1 t) s1' →
800   s1' -flat-→ (L_s1 t2) →
801   ∃s2',t2: L_raw_trace.
802    pre_mesurable_trace … (L_t t2) ∧
803    well_formed_trace … (L_t t2) ∧
804    |t1| = |t2| ∧
805    S (L_s2 t1) s2' ∧
806    (L_s2 t2) -flat-→ s2'.
807 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
808       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
809
810
811(*********************************************************************)
812
813(* quello che segue tentava di permettere di evitare l'emissione di label
814   associate a codice morto *)
815
816replace_last x : weak_trace → weak_trace
817   [] ⇒ [], Some x
818 | l::t ⇒
819     let 〈t',x'〉 ≝ replace_last x t in
820     match x' with
821     [ None ⇒ l::t', None
822     | Some x'' ⇒ [], Some x''
823
824theorem simulates:
825 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
826  pre_measurable_trace … t1 →
827  well_formed_trace … t1.
828 ∀l1: option NonFunctionalLabel.
829 ∀s1'.
830   S s1 s1' →
831   ∃dead_labels.
832   ∃s2'. ∃t2: raw_trace … s1' s2'.
833    pre_mesurable_trace … t2 ∧
834    well_formed_trace … t2.
835   ∃l2: option NonFunctionalLabel.
836    match l1 with
837    [ None ⇒
838       match l2 with
839       [ None ⇒ |t1| = |t2|
840       | Some l2' ⇒ |t1| = l2'::|t2| ]
841    | Some l1' ⇒
842       match l2 with
843       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
844       | Some l2' ⇒
845          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
846          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
847       ]
848    ]
849    *)
Note: See TracBrowser for help on using the repository browser.