Changeset 3390 for LTS/Simulation.ma
 Timestamp:
 Oct 10, 2013, 2:53:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3389 r3390 112 112 [ assumption 113 113  %{(None ?)} % 114  @IH try assumption >Hclass % #EQ destruct114  @IH try assumption 115 115 ] 116 116 qed. … … 125 125 [ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl' 126 126 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption  whd %{(None ?)} % ] 127 @IH [ >Hst2' % #EQ destruct  assumption]127 @IH assumption 128 128 qed. 129 129 … … 158 158 λS,st1,st2,t.match t with [ t_base _ ⇒ false  _ ⇒ true ]. 159 159 160 (* 160 161 lemma append_well_formed_silent : ∀S : abstract_status. 161 162 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. 162 163 well_formed_trace … t → pre_silent_trace … t' → 163 (is_trace_non_empty … t' → as_classify … st 1' = cl_other) →164 (is_trace_non_empty … t' → as_classify … st) → 164 165 well_formed_trace … (t' @ t). 165 166 #S #st1' #st1 #st2 #t #t' lapply t t elim t' … … 172 173 [2: >(Hclass1 I) % #EQ destruct] 173 174 @IH try assumption #_ assumption 174 qed. 175 qed.*) 175 176 176 177 lemma well_formed_append : ∀S : abstract_status. … … 200 201 try @IH assumption 201 202 qed. 202 203 (* 203 204 lemma silent_is_well_formed : ∀S : abstract_status. 204 205 ∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t. … … 208 209 [ @IH % [2: #_ ] assumption  >(H1 I) % #EQ destruct] 209 210 qed. 210 211 *) 211 212 212 213 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. … … 260 261 #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL 261 262 [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2'' 262 * #silent_ts2'' #Hclass_s2cases(IH … RELst2s2'')263 ** #silent_ts2'' #Hclass_s2 #wf_ts2'' cases(IH … RELst2s2'') 263 264 [2: cases(well_formed_trace_inv … well_formed) 264 265 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ … … 276 277 [ % 277 278 [ @append_premeasurable_silent assumption 278  @append_well_formed _silentassumption279  @append_well_formed assumption 279 280 ] 280 281  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l … … 291 292 ] 292 293 #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2'''' 293 * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')294 ** #sil_ts2'' #Hclass_s2 #wf_ts2'' ** #sil_t_s2'''' #Hclass_s2''' #wf_ts2'''' cases(IH … RELst2_s2'''') 294 295 [2: cases(well_formed_trace_inv … well_formed) 295 296 [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ … … 312 313 ] 313 314 @append_premeasurable_silent assumption 314  @append_well_formed _silenttry assumption inversion(as_classify … s2'')315  @append_well_formed try assumption inversion(as_classify … s2'') 315 316 #Hclass 316 317 [ %3 [2: %{c} %] 317 318 *: %2 [2,4: >Hclass % #EQ destruct] 318 319 ] 319 @append_well_formed _silentassumption320 @append_well_formed assumption 320 321 ] 321 322  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l … … 341 342 #sil_t1 #sil_t2 342 343 cases(IH … wf_tl' … rel_s2_s2''') 343 [2: @(silent_io … (proj1 … sil_t2)) assumption]344 [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption] 344 345 #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL 345 346 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] 346 347 % [2: whd in ⊢ (??%?); 347 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))348 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1))) 348 349 whd in ⊢ (???%); 349 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))350 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2))) 350 351 @eq_f assumption ] 351 352 % 352 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]353 [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))] 353 354 %3 354 [ @(silent_io … (proj1 … sil_t1)) assumption355 [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption 355 356  whd %{ret_lab} % 356  @append_premeasurable_silent try assumption @(proj1 … sil_t2)357  @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2)) 357 358 ] 358  @append_well_formed_silent 359 [ %2 try assumption @append_well_formed_silent try assumption 360 [ @(proj1 … sil_t2) 361  @(proj2 … sil_t2) 362 ] 363  @(proj1 … sil_t1) 364  @(proj2 … sil_t1) 365 ] 359  @append_well_formed 360 [ @(proj2 … sil_t1)] 361 %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2) 366 362 ] 367 363  #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct … … 379 375 #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2 380 376 cases(IH … wf_tl' … REL) 381 [2: @(silent_io … (proj1 … sil_t2)) assumption ]377 [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption ] 382 378 #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin} 383 379 %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % 384 380 [2: whd in ⊢ (??%?); 385 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))381 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1))) 386 382 whd in ⊢ (???%); 387 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))383 >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2))) 388 384 @eq_f assumption ] 389 385 % 390 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]386 [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))] 391 387 %4 try assumption 392 [ @(silent_io … (proj1 … sil_t1)) assumption388 [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption 393 389  whd %{f} %{lab} % 394  @append_premeasurable_silent try assumption @(proj1 … sil_t2)390  @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2)) 395 391 ] 396  @append_well_formed_silent 397 [ %2 try assumption @append_well_formed_silent try assumption 398 [ @(proj1 … sil_t2) 399  @(proj2 … sil_t2) 400 ] 401  @(proj1 … sil_t1) 402  @(proj2 … sil_t1) 403 ] 392  @append_well_formed [ @(proj2 … sil_t1) ] 393 %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2) 404 394 ] 405 395  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * … … 412 402 #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1  * #y1 #EQ destruct(EQ) ] #_ 413 403 #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl)) 414 3: @(silent_io … (proj1 … sil_tr2)) assumption404 3: @(silent_io … (proj1 … (proj1 … sil_tr2))) assumption 415 405 ] 416 406 #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2 … … 423 413 #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1  * #w1 #EQ destruct(EQ)] #_ 424 414 #EQ1 #EQ2 #EQ3 destruct #_ assumption 425 3: @(silent_io … (proj1 … sil_tr5)) assumption415 3: @(silent_io … (proj1 … (proj1 … sil_tr5))) assumption 426 416 ] 427 417 #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'} … … 429 419 % [2: assumption] % 430 420 [ % 431 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ]421 [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr1)) ] 432 422 %5 433 [ @(silent_io … (proj1 … sil_tr1)) assumption434  @(silent_io … (proj1 … sil_tr4)) assumption423 [ @(silent_io … (proj1 … (proj1 … sil_tr1))) assumption 424  @(silent_io … (proj1 … (proj1 … sil_tr4))) assumption 435 425  whd %{f} %{l} % 436 426  assumption 437  @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr2)]438 @append_silent_premeasurable try assumption @(proj1 … sil_tr4)439  @append_premeasurable_silent try assumption @(proj1 … sil_tr5)427  @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr2))] 428 @append_silent_premeasurable try assumption @(proj1 … (proj1 … sil_tr4)) 429  @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_tr5)) 440 430  @(RET_REL … call_rel) assumption 441 431  % 442 432 ] 443  @append_well_formed _silent [2: @(proj1 … sil_tr1) 3:@(proj2 … sil_tr1) ]444 %2 [2: assumption] >append_associative @append_well_formed _silent445 [ 2: @(proj1 … sil_tr2) 3: @(proj2 … sil_tr2) ]@append_well_formed433  @append_well_formed [ @(proj2 … sil_tr1) ] 434 %2 [2: assumption] >append_associative @append_well_formed 435 [ @(proj2 … sil_tr2) ] @append_well_formed 446 436 [ @append_well_formed try assumption @silent_is_well_formed assumption ] 447 437 %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed 448 438 assumption 449 439 ] 450  >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ]440  >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … (proj1 … sil_tr1)) ] 451 441 whd in ⊢ (??%%); @eq_f >append_associative 452 442 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 453 [2: @(proj1 … sil_tr2) ] >append_associative443 [2: @(proj1 … (proj1 … sil_tr2)) ] >append_associative 454 444 >get_cost_label_append in ⊢ (???%); 455 445 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 456 [2: @(proj1 … sil_tr4) ] normalize446 [2: @(proj1 … (proj1 … sil_tr4)) ] normalize 457 447 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 458 [2: @(proj1 … sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2448 [2: @(proj1 … (proj1 … sil_tr5)) ] >get_cost_label_append in ⊢ (??%?); @eq_f2 459 449 assumption 460 450 ] … … 462 452 qed. 463 453 464 xxxxx454 sxxxxx 465 455 466 456
Note: See TracChangeset
for help on using the changeset viewer.