Changeset 3508


Ignore:
Timestamp:
Sep 26, 2014, 6:06:05 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3507 r3508  
    11381138qed.
    11391139
     1140include "Simulation.ma".
     1141
     1142lemma 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.
     1145pre_measurable_trace … (t1 @ t2) →
     1146pre_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]
     1160qed.
     1161
     1162lemma 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.
     1165pre_measurable_trace … (t1 @ t2) →
     1166pre_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]
     1180qed.
     1181
     1182
     1183
    11401184theorem static_dynamic :
    11411185(* Given an assembly program *)
     
    11841228     >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?);
    11851229     >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:
    11871233 ]
    11881234 whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2
     
    11911237@(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR)
    11921238  [ /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)
    11941247  | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] *
    11951248    [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.