[3387] | 1 | include "Traces.ma". |
---|
[3524] | 2 | include "basics/jmeq.ma". |
---|
[3382] | 3 | |
---|
[3524] | 4 | discriminator option. |
---|
| 5 | |
---|
[3549] | 6 | record 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] | 11 | definition 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] | 14 | record 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 | |
---|
| 102 | lemma 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 |
---|
| 105 | qed. |
---|
[3383] | 106 | |
---|
[3549] | 107 | lemma 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] | 111 | simulation_conditions … rel → |
---|
[3549] | 112 | is_costlabelled_act … l → |
---|
| 113 | (is_call_act … l → is_call_post_label … s1) → |
---|
[3531] | 114 | as_execute … l s1 s2 → |
---|
| 115 | Srel … 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'. |
---|
| 120 | silent_trace … t_pre ∧ silent_trace … t_post ∧ |
---|
| 121 | as_execute … l pre_em post_em ∧ |
---|
[3549] | 122 | (is_call_act … l → is_call_post_label … pre_em) ∧ |
---|
[3531] | 123 | Srel … 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 | ] |
---|
| 158 | qed. |
---|
| 159 | |
---|
| 160 | |
---|
| 161 | |
---|
| 162 | (* silente simula in silente *) |
---|
[3388] | 163 | |
---|
[3531] | 164 | |
---|
[3549] | 165 | theorem 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] | 404 | qed. |
---|
[3383] | 405 | |
---|
[3549] | 406 | lemma 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 | ] |
---|
| 425 | qed. |
---|
| 426 | |
---|
[3549] | 427 | lemma tail_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p. |
---|
[3531] | 428 | ∀s1,s2 : S.∀t : raw_trace … s1 s2. |
---|
| 429 | pre_measurable_trace … t → |
---|
[3549] | 430 | as_classify … s2 ≠ cl_io. #p |
---|
[3531] | 431 | #S #s1 #s2 #t #H elim H // |
---|
| 432 | qed. |
---|
| 433 | |
---|
[3524] | 434 | theorem 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] | 457 | cases 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 |
---|
| 459 | cases(silent_in_silent … sim_rel … Rsi_si' sil_ti0) |
---|
| 460 | #s0' * #ti0' * #sil_ti0' #Rs0_s0' |
---|
| 461 | cases(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' |
---|
| 465 | cases(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' #_ #_ |
---|
| 468 | cases(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' |
---|
| 471 | cases(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] | 488 | qed. |
---|
[3531] | 489 | |
---|
| 490 | |
---|