Changeset 2539 for src/common


Ignore:
Timestamp:
Dec 6, 2012, 2:48:40 PM (7 years ago)
Author:
tranquil
Message:

added cl_jump case to trace_any_any_free

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2530 r2539  
    6060| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
    6161  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 →
    6266  trace_any_any_free S s1 s3.
    6367
     
    6569match taaf with
    6670[ taaf_base _ ⇒ false
    67 | taaf_step _ _ _ _ _ _ ⇒ true
     71| _ ⇒ true
    6872].
    6973
     
    316320  [ taaf_base s ⇒ λ_.λtal.tal
    317321  | 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  ]. 
    319324
    320325lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
    321326  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
    322327  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); * ]
    324330#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
    325331change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
     
    486492  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
    487493  #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 *)
    489495    ** whd in ⊢ (%→?); *
    490496    [1,3: #ncost #R' #L' %2 /4 by conj/
    491497    |*: * #ABS elim (ABS K)
    492498    ]
    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: %]]
    498505  ]
    499506| (* tal_base_return *) whd
     
    515522  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
    516523  [ #st2' #tlr2 *****
    517   | #st2_after_ret #st2_after_ret' #st2' #taa2''
    518     #I2 #J2 #tlr2 **** #ncost
     524  |*: #st2_after_ret #st2_after_ret' #st2' #taa2''
     525    #I2 #J2 [2: #K2 ] #tlr2 **** #ncost
    519526  ]
    520527  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
     
    524531      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
    525532    ]
    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/
    529538      ]]]]]]]]]]
    530539    ]
    531540  ]
    532   [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
     541  [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption
    533542  |*: whd <st1_L_st2' assumption
    534543  ]
     
    549558    [4: %{taa2'''} % [ /4 by conj/ ]
    550559      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
    551     ]]] 
     560    ]]]
    552561  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
    553562    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
     
    562571      [3: % [ /2 by conj/ ]
    563572      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
    564     | #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' #ncost
     573    |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost
    565574      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
    566575      *** #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/
    570581        ]]]]]]]]]]
    571582      ]]
    572583    ]
    573584  ]
    574   [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
     585  [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption
    575586  |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 assumption
    577     |*: #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 //
    578589    ]
    579590  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
     
    642653  | taaf_step s1 s2 s3 pre H G ⇒
    643654    λ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)
    644657  ] ft.
    645658
     
    759772#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
    760773[ #st2 #ft >append_nil % ]
    761 #st2 #st3 #st4 #taa #H normalize nodelta #G #ft
     774#st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft
    762775@ft_extend_taa_advance_flat_obs
    763776qed.
     
    798811|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
    799812  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
    800   [1,2: (* jump *)
     813  [1,2: (* other/jump *)
    801814    lapply (sim_execute … ex G')
    802815    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_nil
    809       >ft_extend_taa_obs <L'
    810       >(not_costed_no_label … ncost) >if_eq >S %
    811     | * #st2' * #tal ** #coll
    812       elim (tal_collapsable_split … coll) #st2_mid' * #taa2
    813       * #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_obs
    820       whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    821       <S <L' %
    822     ]
    823   | (* other *)
    824     lapply (sim_execute … ex G')
    825     >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); **)
    826816    #st2' *#taaf ** #ncost #G'' #H''
    827817    %{st2'} %{st2'}
     
    834824    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
    835825    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
    836     [1,3: #st2' #H'' #taa * #ncost
     826    [1,4: #st2' #H'' #taa * #ncost
    837827      >ft_extend_taa_obs <L'
    838828      [1,3: >(not_costed_no_label … ncost) >if_eq >S %
     
    846836        ]
    847837      ]
    848     |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' #_ #taa *
     838    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa *
    849839      whd in ⊢ (???(?????%));
    850840      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
     
    868858    lapply ncost cases taa2' -st2_after_ret -st2'
    869859    [ #st2' * >append_nil
    870     | #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' #ncost
     860    |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost
    871861      >(not_costed_no_label … ncost)
    872862      >if_eq >append_nil
Note: See TracChangeset for help on using the changeset viewer.