source: LTS/Simulation.ma @ 3553

Last change on this file since 3553 was 3549, checked in by piccolo, 5 years ago

added paolo's trick

File size: 22.4 KB
RevLine 
[3387]1include "Traces.ma".
[3524]2include "basics/jmeq.ma".
[3382]3
[3524]4discriminator option.
5
[3549]6record relations (p : label_params) (S1,S2 : abstract_status p) : Type[0] ≝
[3504]7 { Srel: S1 → S2 → Prop
8 ; Crel: S1 → S2 → Prop
[3383]9 }.
[3382]10
[3549]11definition Rrel ≝ λp.λS1,S2 : abstract_status p.λrel : relations … S1 S2.λs,s'.
12 ∀s1,s1'. as_syntactical_succ … S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ … S2 s1' s'.
[3383]13
[3549]14record simulation_conditions (p : label_params) (S1,S2 : abstract_status p)
15(rel : relations …S1 S2) : Prop ≝
[3394]16 { initial_is_initial :
[3504]17   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
[3394]18 ; final_is_final :
[3504]19   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
[3531]20 ; io_is_io :
21   ∀s1,s2.Srel … rel s1 s2 → as_classify … s2 = cl_io → as_classify … s1 = cl_io
[3394]22 ; simulate_tau:
[3504]23     ∀s1:S1.∀s2:S2.∀s1':S1.
[3549]24      as_execute … (cost_act … (None ?))  s1 s1'→
[3391]25      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3549]26      ∃s2'. ∃t: raw_trace … S2 s2 s2'.
[3388]27        Srel … rel s1' s2' ∧ silent_trace … t
[3383]28 ; simulate_label:
[3504]29     ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
[3549]30      as_execute … S1 (cost_act … (Some ? l)) s1 s1' →
[3391]31      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]32      Srel … rel s1 s2 →
[3383]33      ∃s2',s2'',s2'''.
[3549]34       ∃t1: raw_trace … S2 s2 s2'.
35       as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
[3504]36       ∃t3: raw_trace … s2'' s2'''.
[3394]37        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]38 ; simulate_call_pl:
[3504]39     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
[3387]40      is_call_post_label … s1 →
[3549]41      as_execute … (call_act … f l) s1 s1' →
[3391]42      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]43      Srel … rel s1 s2 →
[3383]44      ∃s2',s2'',s2'''.
[3549]45       ∃t1: raw_trace … S2 s2 s2'.
46       as_execute … (call_act … f l) s2' s2'' ∧
[3388]47       bool_to_Prop(is_call_post_label … s2') ∧
[3549]48       ∃t3: raw_trace … S2 s2'' s2'''.
[3394]49        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]50 ; simulate_ret_l:
[3504]51     ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
[3549]52      as_execute … S1 (ret_act … (Some ? l)) s1 s1' →
[3391]53      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]54      Srel  … rel s1 s2 →
[3383]55      ∃s2',s2'',s2'''.
[3549]56       ∃t1: raw_trace … S2 s2 s2'.
57       as_execute p S2 (ret_act p (Some ? l)) s2' s2'' ∧
58       ∃t3: raw_trace … S2 s2'' s2'''.
[3394]59        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]60 ; simulate_call_n:
[3504]61     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
[3549]62      as_execute … (call_act … f l) s1 s1' →
[3387]63      ¬ is_call_post_label … s1 →
[3391]64      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]65      Srel … rel s1 s2 →
[3383]66      ∃s2',s2'',s2'''.
[3549]67       ∃t1: raw_trace … S2 s2 s2'.
[3389]68       bool_to_Prop (¬ is_call_post_label … s2') ∧
[3549]69       as_execute … (call_act … f l) s2' s2'' ∧
70       ∃t3: raw_trace … S2 s2'' s2'''.
[3394]71        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3387]72        ∧ Crel … rel s1 s2'
[3383]73 ; simulate_ret_n:
[3504]74     ∀s1:S1.∀s2:S2.∀s1':S1.
[3549]75      as_execute … (ret_act … (None ?)) s1 s1' →
[3391]76      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
77      Srel … rel s1 s2 →
[3504]78      ∃s2',s2'',s2''': S2.
[3549]79       ∃t1: raw_trace … S2 s2 s2'.
80       as_execute … (ret_act … (None ?)) s2' s2''  ∧
81       ∃t3: raw_trace … S2 s2'' s2'''.
[3394]82        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
[3389]83        ∧ Rrel … rel s1' s2''
[3394]84 ; simulate_io_in :
[3504]85   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
[3394]86   as_execute … (cost_act … (Some ? l)) s1 s1' →
87   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
88   Srel … rel s1 s2 →
[3504]89   ∃s2',s2''.∃t: raw_trace … s2 s2'.
[3394]90   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
91   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
92; simulate_io_out :
[3504]93   ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
[3394]94   as_execute … (cost_act … (Some ? l)) s1 s1' →
95   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
96   Srel … rel s1 s2 →
[3504]97   ∃s2',s2''.∃t : raw_trace … s2' s2''.
[3394]98   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
99   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
[3383]100 }.
[3531]101 
102lemma io_state_case : ∀P : status_class → Prop.∀s.
103(s = cl_io → P s) → (s ≠ cl_io → P s) → P s.
104#P * #H1 #H2 [2: @H1 %] @H2 % #EQ destruct
105qed.
[3383]106
[3549]107lemma simulate_labelled_action : ∀p.∀S1,S2 : abstract_status p.
108∀rel : relations … S1 S2.
[3531]109∀s1,s2 : S1.∀s1' : S2.
[3549]110∀l : ActionLabel p.
[3531]111simulation_conditions … rel →
[3549]112is_costlabelled_act … l →
113(is_call_act … l → is_call_post_label … s1) →
[3531]114as_execute … l s1 s2 →
115Srel … rel s1 s1' →
116¬ (as_classify … s1 = cl_io ∧ as_classify … s2 = cl_io) →
117∃pre_em,post_em,s2' : S2.
118∃t_pre : raw_trace … s1' pre_em.
119∃t_post : raw_trace … post_em s2'.
120silent_trace … t_pre ∧ silent_trace … t_post ∧
121as_execute … l pre_em post_em ∧
[3549]122(is_call_act … l → is_call_post_label … pre_em) ∧
[3531]123Srel … rel s2 s2'.
[3549]124#p #S1 #S2 #rel #s1 #s2 #s1' *
[3531]125[ #f #c | * [|#lbl] | * [|#lbl]]
126#sim * #Hcall #prf #REL * #Hio
127[ cases(simulate_call_pl … sim … prf … REL)
128  [2: @Hcall %{f} %{c} %
129  |3: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
130  |4: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
131  ]
132  #pre_em * #post_em * #s2' * #t_pre ** #prf' #call * #t_post ** #REL' #sil_tpre #sil_tpost
133  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % // % // % // %1 //
134| cases(simulate_ret_l … sim … prf … REL)
135  [2: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
136  |3: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
137  ]
138  #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
139  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
140  % // % // %1 //
141| @(io_state_case … (as_classify … s1)) @(io_state_case … (as_classify … s2))
142  #class_s2 #class_s1
143  [ cases(Hio ?) /2/
144  | cases(simulate_io_out … sim … prf … REL) //
145    #post_em * #s2' * #t_post *** #sil_tpost #prf' #Hclass #REL'
146    %{s1'} %{post_em} %{s2'} %{(t_base …)} %{t_post} % // % [2: * #f * #c #EQ destruct]
147    % // % [%2 %*] % assumption
148  | cases(simulate_io_in … sim … prf … REL) //
149    #pre_em * #s2' * #t_pre *** #sil_tpre #prf' #Hclass #REL'
150    %{pre_em} %{s2'} %{s2'} %{t_pre} %{(t_base …)} % // % [2: * #f * #c #EQ destruct]
151    % // % [% assumption]  %2 % *
152  | cases(simulate_label … sim … prf … REL) //
153    #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
154    %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
155    % // % // %1 //
156  ]
157]
158qed. 
159   
160 
161 
162(* silente simula in silente *)
[3388]163
[3531]164
[3549]165theorem simulates_pre_mesurable: ∀p.
166 ∀S1,S2 : abstract_status p.∀rel : relations … S1 S2.
167 ∀s1,s1' : S1. ∀t1: raw_trace … S1 s1 s1'.
[3504]168  simulation_conditions … rel →
[3382]169  pre_measurable_trace … t1 →
[3504]170  ∀s2 : S2.
[3391]171 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
[3388]172  ∃s2'. ∃t2: raw_trace … s2 s2'.
[3387]173    pre_measurable_trace … t2 ∧
174    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
[3524]175    Srel … rel s1' s2' ∧
176    (measurable_suffix … t1 → measurable_suffix … t2) ∧
177    (silent_trace … t1 → silent_trace … t2).
[3549]178#p #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
[3524]179[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
180 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
181  * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
182 | #_ %2 % *
183 ]
184| #st1 #st2 #st3 #l #prf #tl #Hclass **
185  [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
186    cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
187    #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
188    [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
189        #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
190    #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
191    cut(? : Prop)
192      [3: #Hpre %
193         [ %
194             [ %
195                 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
196                 | assumption
197                 ]
198             |  #meas_suff cases(Hm ?)
199                [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
200                  destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
201                  %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
202                | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
203                  [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
204                    ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
205                  | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
206                    * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
207                    %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
208                  ]
209                ]
210             ]
211        | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
212          #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
213          /4 by append_silent,or_introl/
214        ]
215     |
216     ]
217    @append_premeasurable_silent //
218  | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
219    cases(simulate_label … sim … prf … REL)
[3391]220    [2,3: /2/]
221    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
[3394]222    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
[3524]223    #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
224    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
225    [2: * [ #H inversion H
226            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
227            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
228            ]
229          | * #H cases(H I)
230          ]
231     ]
232    %
233    [ % [2: assumption] %
234      [ @append_premeasurable_silent // %2 /2 by ex_intro/
[3394]235       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
236         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
237         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
238         cases H47 #ABS @⊥ @ABS % ]
239       @append_premeasurable_silent // % //
[3388]240    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
[3391]241      [2: assumption] whd in ⊢ (???%);
242      >get_cost_label_invariant_for_append_silent_trace_l //
[3524]243    ] % assumption
244    | #Hsuff cases(measurable_suffix_tind … Hsuff)
245      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
[3549]246      % [ /3 by or_introl, append_silent/ ] %{(cost_act … (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
247      | #H @measurable_suffix_append change with ((t_ind ??????? t_s2'''')@t_s3) in ⊢ (?????%);
[3524]248        @measurable_suffix_append /2/
249      ]
[3388]250  ]
[3524]251  ]
[3388]252| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
[3524]253  #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
254  cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
[3391]255  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
256  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
[3394]257  [2: @(pre_silent_io … sil_t2) assumption]
[3524]258  #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
259  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
260  [2: * [ #H inversion H
261            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
262            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
263            ]
264          | * #H cases(H I)
265          ]
266  ]
267  %
268    [ % [2: assumption]
269      % [2: whd in ⊢ (??%?);
[3391]270        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
[3388]271        whd in ⊢ (???%);
[3394]272        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
[3388]273        @eq_f assumption ]
[3394]274  @append_premeasurable_silent [2: //] %3
275  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
276  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
277  [ #H49 #H50 #H51 #H52 #H53 destruct //]
278  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
279  #ABS @⊥ @ABS %
[3524]280 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
281      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
[3549]282      % [ /3 by or_introl, append_silent/ ] %{(ret_act … (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
283      | #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%);
[3524]284        @measurable_suffix_append /2/
285      ]
286  ]
[3391]287| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
288  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
[3524]289   cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
[3391]290   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
291   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
292   cases(IH  … REL)
[3394]293   [2: /2 by pre_silent_io/ ]
[3524]294   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
295   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
296   [2: * [ #H inversion H
297            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
298            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
299            ]
300          | * #H cases(H I)
301          ]
302  ]
303  %
304   [ % [2: assumption] %
[3388]305   [2: whd in ⊢ (??%?);
[3391]306        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
[3388]307        whd in ⊢ (???%);
[3394]308        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
[3388]309        @eq_f assumption ]
[3391]310   @append_premeasurable_silent try assumption
[3388]311     %4 try assumption
[3394]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 %
[3388]315     | whd %{f} %{lab} %
[3394]316     | @append_premeasurable_silent // % assumption
[3388]317     ]
[3524]318   | #Hsuff cases(measurable_suffix_tind … Hsuff)
319      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
[3549]320      % [ /3 by or_introl, append_silent/ ] %{(call_act … f lab)} %{(exe_s2'')} % // % //
321      | #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%);
[3524]322        @measurable_suffix_append /2/
323      ]
324  ]
325|  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
[3389]326  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
[3524]327  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
[3391]328  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
[3389]329  #sil_tr2 #call_rel cases(IH1 … REL1)
[3394]330  [2: /2 by pre_silent_io/ ]
[3524]331  #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
332  cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
[3391]333  #st3'' * #st4' * #st4'' *
[3394]334  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
[3524]335  #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
[3389]336  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
[3524]337  %
338  [2: * [ #H inversion H
339            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
340            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
341            ]
342          | * #H cases(H I)
343          ]
344  ]
345  %
346  [ % [2: assumption] %
[3391]347  [ @append_premeasurable_silent try assumption %5
[3394]348       [1,2: /2 by pre_silent_io/
349             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
350             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
351             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
352             cases H107 #ABS @⊥ @ABS %
[3389]353       | whd %{f} %{l} %
354       | assumption
[3394]355       | @append_premeasurable_silent try assumption [2: % //]
356         @append_silent_premeasurable // % //
[3391]357       | @append_premeasurable_silent try assumption
[3389]358       | @(RET_REL … call_rel) assumption
359       | %
360       ]
[3391]361  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
[3389]362    whd in ⊢ (??%%); @eq_f >append_associative
363    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]364    [2: % // ] >append_associative
[3389]365    >get_cost_label_append in ⊢ (???%);
366    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]367    [2: % //] normalize
[3389]368    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]369    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
[3389]370    assumption
371  ]
[3394]372  % //
[3524]373 | #Hsuff cases(measurable_suffix_tind … Hsuff)
374   [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
375     * #ex_em ** inversion t_pre in ⊢ ?;
376     [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
377         #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
378         -Hsuff -e0 -EQ #H inversion H
379         [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
380         #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
381     ]
382     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
383     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
[3549]384   | #Hsuff @measurable_suffix_append change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append
385     change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append @Hm2
[3524]386     cases(measurable_suffix_append_case … Hsuff)
387     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
388       [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
389         -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
390         #st2 #_ #EQ destruct(EQ)
391       | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
392       ]
393     | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
394       [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
395         lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
396       | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
397         * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
398         %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
399       ]
400     ]
401   ]
402 ]
[3388]403]
[3389]404qed.
[3383]405
[3549]406lemma silent_in_silent : ∀p.∀S1,S2 : abstract_status p.∀rel : relations … S1 S2.
407 ∀s1,s1' : S1. ∀t1: raw_trace … S1 s1 s1'.
[3531]408  simulation_conditions … rel →
409  ∀s2 : S2.Srel … rel s1 s2 →
410  silent_trace … t1 →
411  ∃s2'. ∃t2: raw_trace … s2 s2'.
412    silent_trace … t2 ∧
413    Srel … rel s1' s2'.
[3549]414    #p
[3531]415#S1 #S2 #rel #s1 #s1' #t1 #sim #s2 #REL *
416[ #pre_sil_ti0 cases(simulates_pre_mesurable … sim … (pre_silent_is_premeasurable … pre_sil_ti0) … REL)
417  [2: % #H
418      lapply(head_of_premeasurable_is_not_io … (pre_silent_is_premeasurable … pre_sil_ti0))
419      >(io_is_io … sim … H) // * /2/
420  ]
421  #s2' * #t2 *** * #H1 #H2 #H3 #H4 #H5 %{s2'} %{t2} % /3 by or_introl/
422| cases t1 in REL; [ #st #H #_ %{s2} %{(t_base …)} % [%2 % * ] // ]
423  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 cases H14 #H cases(H I)
424]
425qed.
426
[3549]427lemma tail_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p.
[3531]428∀s1,s2 : S.∀t : raw_trace … s1 s2.
429pre_measurable_trace … t →
[3549]430as_classify … s2 ≠ cl_io. #p
[3531]431#S #s1 #s2 #t #H elim H //
432qed.
433
[3524]434theorem simulates_measurable:
[3549]435 ∀p.
436 ∀S1,S2: abstract_status p.
[3524]437 
[3549]438 ∀rel: relations … S1 S2. simulation_conditions … rel →
[3524]439 
440 ∀si,sn: S1. ∀t: raw_trace … si sn.
441 
442 ∀s1,s2. measurable … s1 s2 … t →
443 
[3531]444 ∀si': S2.
445 (as_classify … si' = cl_io →  as_classify … si = cl_io) → 
[3524]446 
447 Srel … rel si si' →
448 
449 ∃sn'. ∃t': raw_trace … si' sn'.
[3506]450
[3524]451 Srel … rel sn sn' ∧
[3394]452
[3524]453 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
454 
455 ∃s1',s2'. measurable … s1' s2' … t'.
[3549]456#p #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'
[3531]457cases Hmeas -Hmeas #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *******
458#pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init
459cases(silent_in_silent … sim_rel … Rsi_si' sil_ti0)
460#s0' * #ti0' * #sil_ti0' #Rs0_s0'
461cases(simulate_labelled_action … prf1 … Rs0_s0') /2/
462     [2: % * #H1 #H2 lapply(head_of_premeasurable_is_not_io … pre_t12) >H2 * /2/ ]
463#s0'' * #s1'' * #s1' * #t_s0'' * #t_s1'' **** #sil_ts0'' #sil_ts1'' #prf1' #Hcall_init'
464#Rs1_s1'
465cases(simulates_pre_mesurable … sim_rel … pre_t12 … Rs1_s1')
466[2: % #H lapply(head_of_premeasurable_is_not_io … pre_t12) >(io_is_io … sim_rel … H) // * /2/ ]
467#s2' * #t12' **** #pre_t12' #EQcost #Rs2_s2' #_ #_
468cases(simulate_labelled_action … prf2 … Rs2_s2') /2/
469  [2: % * #H1 #H2 lapply(tail_of_premeasurable_is_not_io … pre_t12) >H1 * /2/]
470#s2'' * #s3'' * #s3' * #t_s2'' * #t_s3'' **** #sil_ts2'' #sil_ts3'' #prf2' #Hcall_fin' #Rs3_s3'
471cases(silent_in_silent … sim_rel … Rs3_s3' sil_t3n)
472#sn' * #t_3n' * #sil_t3n' #Rsn_sn' %{sn'}
473%{(ti0'@ t_s0'' @ (t_ind … prf1' (t_s1''@t12' @ t_s2'' @ (t_ind … prf2' (t_s3'' @ t_3n')))))}
[3549]474% [ % // >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0)
475    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0')
476    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts0'')
477    whd in ⊢ (??%%); @eq_f2 //
478    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts1'')
479    >get_cost_label_append >get_cost_label_append in ⊢ (???%); @eq_f2 //
480    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts2'')
481    whd in ⊢ (??%%); @eq_f2 //
482    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts3'')
483    >(get_cost_label_silent_is_empty … sil_t3n') >(get_cost_label_silent_is_empty … sil_t3n) % ]
[3531]484%{s1''} %{s3''} whd %{s0''} %{s2''} %{(ti0' @t_s0'')} %{(t_s1'' @ t12' @ t_s2'')}
485%{(t_s3'' @ t_3n')} %{l1} %{l2} %{prf1'} %{prf2'} % [2: /2/]
486% [2: /2 by append_silent/] % [2: /2 by append_silent/] % [2: /2/] % // % // % //
487@append_premeasurable_silent /2/
[3549]488qed.
[3531]489
490
Note: See TracBrowser for help on using the repository browser.