 Timestamp:
 Dec 6, 2012, 2:48:40 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StatusSimulation.ma
r2530 r2539 60 60  taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 → 61 61 as_classifier S s2 cl_other → 62 trace_any_any_free S s1 s3 63  taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 → 64 as_classifier S s2 cl_jump → 65 as_costed S s3 → 62 66 trace_any_any_free S s1 s3. 63 67 … … 65 69 match taaf with 66 70 [ taaf_base _ ⇒ false 67  taaf_step _ _ _ _ __ ⇒ true71  _ ⇒ true 68 72 ]. 69 73 … … 316 320 [ taaf_base s ⇒ λ_.λtal.tal 317 321  taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J 318 ]. 322  taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J) 323 ]. 319 324 320 325 lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2. 321 326 tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 → 322 327 tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2). 323 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * H7 H8 normalize // 328 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * H7 H8 normalize 329 [ // 3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ] 324 330 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 325 331 change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????); … … 486 492 try >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 487 493 #st2' ** st2 st2' 488 [1, 3: #st2 (* taa2 empty → st1' must be not cost_labelled *)494 [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *) 489 495 ** whd in ⊢ (%→?); * 490 496 [1,3: #ncost #R' #L' %2 /4 by conj/ 491 497 *: * #ABS elim (ABS K) 492 498 ] 493 *: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1 494 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))} 495 [1,3: whd <st1_L_st2' assumption ] 496 % [1,3: /2 by conj/] 497 % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]] 499 *: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ] 500 *** #st1_R_st2' #st1_L_st2' %1 501 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))} 502 [1,4: %1{I2} 7,10: %2{I2} 2,5: assumption 8,11: whd <st1_L_st2' assumption ] 503 % /2 by conj/ 504 % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]] 498 505 ] 499 506  (* tal_base_return *) whd … … 515 522 #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' st2_after_ret st2' 516 523 [ #st2' #tlr2 ***** 517  #st2_after_ret #st2_after_ret' #st2' #taa2''518 #I2 #J2 #tlr2 **** #ncost524 *: #st2_after_ret #st2_after_ret' #st2' #taa2'' 525 #I2 #J2 [2: #K2 ] #tlr2 **** #ncost 519 526 ] 520 527 #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1 … … 524 531 % [%] %[%[ %{EQcall} %[%[%[ %1 %[%[%[ %{S} % ]]]]]]]] 525 532 ] 526  %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 (or_intror ?? J2) ?))} 527 [3: % [ % assumption ] 528 % [%] %[%[ %{EQcall} %[%[%[ %2 %[%[%[%[%[ % [ %{S} % ] /2 by taa_append_collapsable, I/ 533 *: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))} 534 [2: %1{J2} 6: %2{J2} 535 4,8: % try (% assumption) 536 % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: 537 % [1,3: %{S} % ] /2 by taa_append_collapsable, I/ 529 538 ]]]]]]]]]] 530 539 ] 531 540 ] 532 [1,3 : @(st1_Rret_st2' … st1_C_st2) assumption541 [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption 533 542 *: whd <st1_L_st2' assumption 534 543 ] … … 549 558 [4: %{taa2'''} % [ /4 by conj/ ] 550 559 %[%[ %{EQcall} %[%[%[ %2 %[%[%[%[%[ %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]] 551 ]]] 560 ]]] 552 561  *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1 553 562 %[ %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))} … … 562 571 [3: % [ /2 by conj/ ] 563 572 %[%[ %{EQcall} %[%[%[ %1 %{(refl …)} %[%[%[ %{S} %{tl1_coll} % ]]]]]]]]]] 564  #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2'#ncost573 *: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost 565 574 #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S 566 575 *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1 567 %[ %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' (or_intror ?? J2') ?))} 568 [3: % [ /2 by conj/ ] 569 %[%[ %{EQcall} %[%[%[ %2 %[%[%[%[%[ %{S} % [%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/ 576 %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))} 577 [2: %1{J2'} 6: %2{J2'} 578 4,8: % [1,3: /2 by conj/] 579 %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: 580 %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/ 570 581 ]]]]]]]]]] 571 582 ]] 572 583 ] 573 584 ] 574 [1,4,7,9 : @(st1_Rret_st2' … st1_C_st2) assumption585 [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption 575 586 2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' st2_after_ret st2' 576 [1, 3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption577 *: #st2_after_ret #st2_post #st2' #tl2 #K #M #H #_ @H %587 [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption 588 *: normalize nodelta // 578 589 ] 579 590 3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption … … 642 653  taaf_step s1 s2 s3 pre H G ⇒ 643 654 λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G) 655  taaf_step_jump s1 s2 s3 pre H G K ⇒ 656 λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … G) 644 657 ] ft. 645 658 … … 759 772 #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa st2 st3 760 773 [ #st2 #ft >append_nil % ] 761 #st2 #st3 #st4 #taa #H normalize nodelta #G #ft774 #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft 762 775 @ft_extend_taa_advance_flat_obs 763 776 qed. … … 798 811 *: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl 799 812 (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S 800 [1,2: (* jump *)813 [1,2: (* other/jump *) 801 814 lapply (sim_execute … ex G') 802 815 try >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 803 (* [ ** #ncost #G'' #H''804 %{st2_mid} %{st2_mid}805 %[@(ft_extend_taa … taa)806 assumption]807 %{(taa_base …)} % [ %{H'' G''} ]808 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil809 >ft_extend_taa_obs <L'810 >(not_costed_no_label … ncost) >if_eq >S %811  * #st2' * #tal ** #coll812 elim (tal_collapsable_split … coll) #st2_mid' * #taa2813 * #K2 * #J2 *#H2 #EQ #G'' #H''814 %{st2'} %{st2'}815 %[@(ft_advance_flat … K2 J2)816 @(ft_extend_taa … (taa_append_taa … taa taa2))817 assumption]818 %{(taa_base …)} % [ %{H'' G''} ]819 >ft_extend_taa_advance_flat_obs820 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil821 <S <L' %822 ]823  (* other *)824 lapply (sim_execute … ex G')825 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); **)826 816 #st2' *#taaf ** #ncost #G'' #H'' 827 817 %{st2'} %{st2'} … … 834 824 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 835 825 lapply ncost lapply taa lapply H'' cases taaf st2_mid st2' 836 [1, 3: #st2' #H'' #taa * #ncost826 [1,4: #st2' #H'' #taa * #ncost 837 827 >ft_extend_taa_obs <L' 838 828 [1,3: >(not_costed_no_label … ncost) >if_eq >S % … … 846 836 ] 847 837 ] 848 *: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' #_ #taa *838 *: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa * 849 839 whd in ⊢ (???(?????%)); 850 840 >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs … … 868 858 lapply ncost cases taa2' st2_after_ret st2' 869 859 [ #st2' * >append_nil 870  #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl''#ncost860 *: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost 871 861 >(not_costed_no_label … ncost) 872 862 >if_eq >append_nil
Note: See TracChangeset
for help on using the changeset viewer.