source: LTS/Simulation.ma @ 3505

Last change on this file since 3505 was 3504, checked in by sacerdot, 6 years ago

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