Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3507 r3508 1138 1138 qed. 1139 1139 1140 include "Simulation.ma". 1141 1142 lemma sub_trace_premeasurable_l1 : ∀p,p',prog. 1143 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semantics p p' prog) … s1 s2. 1144 ∀t2 : raw_trace (asm_operational_semantics p p' prog) … s2 s3. 1145 pre_measurable_trace … (t1 @ t2) → 1146 pre_measurable_trace … t1. 1147 #p #p' #prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t1 1148 [ #st #st3 #t2 whd in ⊢ (????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ] 1149 #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; 1150 [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct 1151  #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1152 whd in EQ3 : (??%?%); destruct %2 // @IH // 1153  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct 1154 whd in H13 : (??%?%); destruct %3 // @IH // 1155  #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 1156 destruct whd in H29 : (??%?%); destruct %4 // @IH // 1157  #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 1158 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46 1159 ] 1160 qed. 1161 1162 lemma sub_trace_premeasurable_l2 : ∀p,p',prog. 1163 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semantics p p' prog) … s1 s2. 1164 ∀t2 : raw_trace (asm_operational_semantics p p' prog) … s2 s3. 1165 pre_measurable_trace … (t1 @ t2) → 1166 pre_measurable_trace … t2. 1167 #p #p' #prog #s1 #s2 #s3 #t1 lapply s3 s3 elim t1 1168 [ #st #st3 #t2 whd in ⊢ (????% → ?); #H @H ] 1169 #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; 1170 [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct 1171  #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct 1172 whd in EQ3 : (??%?%); destruct @IH // 1173  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct 1174 whd in H13 : (??%?%); destruct @IH // 1175  #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 1176 destruct whd in H29 : (??%?%); destruct @IH // 1177  #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 1178 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46 1179 ] 1180 qed. 1181 1182 1183 1140 1184 theorem static_dynamic : 1141 1185 (* Given an assembly program *) … … 1184 1228 >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?); 1185 1229 >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?); 1186 whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); [2: cases daemon] % 3: 1230 whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); 1231 [2: cases(actionlabel_ok … Hl2) #x #EQx >EQx cases (get_costlabels_of_trace ????) 1232 [2: #z #zs] normalize % #EQ destruct] % 3: 1187 1233 ] 1188 1234 whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2 … … 1191 1237 @(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR) 1192 1238 [ /6 width=6 by conj, ex_intro/ 1193  cases daemon (* true *) 1239  lapply(sub_trace_premeasurable_l2 … premeas) 1240 change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?); 1241 change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?); 1242 change with ((t_ind ???????)@?) in ⊢ (????(?????%?) → ?); 1243 >append_associative #H lapply(sub_trace_premeasurable_l2 … H) H 1244 change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?); 1245 change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?); 1246 <append_associative #H @(sub_trace_premeasurable_l1 … H) 1194 1247  cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] * 1195 1248 [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %);
Note: See TracChangeset
for help on using the changeset viewer.