Changeset 3531


Ignore:
Timestamp:
Mar 13, 2015, 6:42:58 PM (5 years ago)
Author:
piccolo
Message:

new notion of measurable: some lemmas are still broken

Location:
LTS
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3524 r3531  
    91916. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
    9292*)
     93
     94(* TO SAY
     951) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
     96inizia/termina in un IO solo se vuota
     972) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
     98aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
     99*)
  • LTS/Language.ma

    r3527 r3531  
    17041704qed.
    17051705   
    1706 
    17071706lemma correctness_lemma : ∀p,p',prog.
    17081707no_duplicates_labels … prog →
     
    17121711pre_measurable_trace … t →
    17131712state_rel … m keep abs_top abs_tail s1 s1' →
    1714 ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
    1715 state_rel  … m keep abs_top' abs_tail' s2 s2' ∧
     1713∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     1714state_rel  … m keep abs_top' abs_tail s2 s2' ∧
    17161715is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
    1717                  (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
     1716                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail) ∧
    17181717 len … t = len … t' ∧
    17191718 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
    17201719 cont … s1 = k @ cont … s2 →
    17211720∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
    1722 ∧ pre_measurable_trace … t'.
     1721∧ pre_measurable_trace … t' ∧
     1722(pre_silent_trace … t → pre_silent_trace … t').
    17231723#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
    17241724#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
    17251725-abs_tail lapply s1' -s1' elim Hpre
    1726 [ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
    1727   %
     1726[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{s1'} %{(t_base …)}
     1727  cut(? : Prop)
     1728  [3: #Hpre' %
    17281729  [ %
     1730   [ %
    17291731    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    17301732      @is_permutation_eq
    17311733    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
    17321734    ]
    1733   | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
     1735  | @Hpre'
     1736  ]
     1737 | #_ %1 /2 by head_of_premeasurable_is_not_io/
     1738 ]
     1739 | skip
     1740 ]
     1741   %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
    17341742    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
    17351743    inversion(code ??) normalize nodelta
     
    17401748    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    17411749    normalize in Hst; <e1 in Hst; normalize nodelta //
    1742   ]   
    17431750| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    17441751  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
     
    17891796         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
    17901797         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1791       #abs_top' * #abs_tail' * #st3' * #t' ****
    1792       #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t'
    1793       %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
     1798      #abs_top' * #st3' * #t' *****
     1799      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' #Hsil
     1800      %{abs_top'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    17941801      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    17951802        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1796       %
     1803      % [ %
    17971804      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
    17981805      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
     
    18021809      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
    18031810      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
    1804       normalize in class_st11; >EQcode11 in class_st11; //
     1811      normalize in class_st11; >EQcode11 in class_st11; // ]
     1812      #H inversion H in ⊢ ?;
     1813      [ #H1 #H2 #H3 #H4 #H5 #H6 destruct ] #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
     1814      destruct %2
     1815      [ % whd in ⊢ (??%% → ?); >EQcodes1' normalize nodelta <EQio11 inversion(io_info … H8)
     1816        normalize nodelta [2: #_ #EQ destruct] #ABS lapply class_st11 whd in match (as_classify ??);
     1817        >EQcode11 normalize nodelta >ABS normalize nodelta * /2/
     1818      ]
     1819      @Hsil //
    18051820    | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
    18061821      #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     
    18391854           ]
    18401855      ]
    1841       #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
     1856      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore1 #EQio #EQ destruct(EQ)
    18421857      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
    18431858      [2: whd whd in match check_continuations; normalize nodelta
     
    18451860         >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
    18461861         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
    1847       #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety
    1848       #pre_t'
    1849       %{abs_top'} %{abs_tail'} %{st3'}
     1862      #abs_top' * #st3' * #t' ***** #Hst3st3' #EQcost #EQlen #stack_safety
     1863      #pre_t' #Hsil
     1864      %{abs_top'} %{st3'}
    18501865      %{(t_ind … (cost_act (Some ? lbl)) … t')}
    18511866      [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    18521867        [3: assumption |4: assumption |*:] /3 by nmk/ ]
    1853       %
     1868     cut(? : Prop)
     1869     [3: #Hpre' %
     1870      [ %
    18541871      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
    18551872          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
    18561873          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
    1857           @is_permutation_cons assumption
     1874          @is_permutation_cons @EQcost
    18581875        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
    18591876          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
     
    18621879          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
    18631880        ]]
     1881      @Hpre' ]
     1882      #h inversion h in ⊢ ?; [ #H21 #H22 #H23 #H24 #H25 #H26 destruct]
     1883      #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
     1884      |skip |
    18641885      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
    18651886      normalize in class_st11; >EQcode11 in class_st11; //
    1866     ]
     1887    ]]
    18671888  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
    18681889    #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11
     
    19141935    |2,5:
    19151936    ]
    1916     #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    1917     #pre_t' %{abs_top1}
    1918     %{abs_tail1} %{s2'} %{(t_ind … t')}
     1937    #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
     1938    #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
    19191939    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
    19201940    |2,5:
    19211941    ]
    1922     % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption]
     1942    cut(? : Prop)
     1943    [3,6: #Hpre'
     1944       %
     1945   
     1946    [1,3: % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f @EQlen ] %{Hst3_s2'} [2: @EQcosts]
    19231947        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
    19241948        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
    1925         assumption
     1949        @EQcosts
    19261950      |*: #k #i #EQcont_st3 >EQcont #EQ
    19271951          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
    19281952      ]]
     1953      @Hpre'
     1954      |*: #h inversion h in ⊢ ?;
     1955          [1,3: #H41 #H42 #H43 #H44 #H45 #H46 destruct
     1956          |*: #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
     1957              %2 [ /2 by head_of_premeasurable_is_not_io/ ] @Hsil //
     1958          ]
     1959          ] |1,4:]
    19291960    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
    1930   | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
     1961    ]
     1962  |*: cases daemon
     1963  ] cases daemon
     1964qed.
     1965
     1966(*
     1967  |
     1968   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
    19311969    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
    19321970    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
     
    19742012        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    19752013        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    1976     ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
    1977       #stack_safety #pre_t' %{abs_top1} %{abs_tail1}
     2014    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen
     2015      #stack_safety #pre_t' %{abs_top1}
    19782016    %{s2'} %{(t_ind … t')}
    19792017    [ @hide_prf @(cond_true … EQcode_s1') //
     
    20372075        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
    20382076        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
    2039     ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
     2077    ] #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety
    20402078    #pre_t'
    2041     %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2079    %{abs_top1} %{s2'} %{(t_ind … t')}
    20422080    [ @hide_prf @(cond_false … EQcode_s1') //
    20432081    |
     
    21022140       % //
    21032141   ]
    2104    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2105    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2142   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2143   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    21062144   [ @hide_prf @(loop_true … EQcode_s1') // |]
    21072145   % [ %
     
    21622200        % // % // % // % [2: %] //
    21632201   ]
    2164    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2165    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2202   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2203   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    21662204   [ @hide_prf @(loop_false … EQcode_s1') // |]
    21672205   % [ %
     
    22192257       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
    22202258   ]
    2221    #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2222    #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2259   #abs_cont1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2260   #pre_t' %{abs_cont1} %{s2'} %{(t_ind … t')}
    22232261   [ @hide_prf @(io_in … EQcode_s1') // |]
    22242262   % [ %
     
    23062344  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
    23072345  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
    2308   #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
    2309   #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')}
     2346  #abs_top1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety
     2347  #pre_t' %{abs_top1} %{s2'} %{(t_ind … t')}
    23102348  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
    23112349  | ]
     
    23992437            ]
    24002438          ]
    2401           #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
     2439          #abs_top''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety
    24022440          #pre_t' %{abs_top'''}
    2403           %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
     2441          %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    24042442          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ]
    24052443          % [ %
     
    25182556          ]
    25192557     ]
    2520      #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
     2558     #abs_top''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1
    25212559     #pre_t1'
    25222560     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
     
    25762614     ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
    25772615     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
    2578      #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
     2616     #EQ1 >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
    25792617     #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ)
    25802618     cases(IH2
     
    25822620             abs_tail_cont abs_top'''')
    25832621     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
    2584      #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
    2585      #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
     2622     #abs_top_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts'
     2623     #EQlen'  #stack_safety2 #pre_t2' %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
    25862624     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
    25872625     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
     
    26172655]
    26182656qed.
     2657
     2658*)
     2659
     2660lemma silent_in_silent : ∀p,p',prog.
     2661no_duplicates_labels … prog →
     2662let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     2663∀s1,s2,s1' : state p.∀abs_top,abs_tail.
     2664∀t : raw_trace (operational_semantics … p' prog) s1 s2.
     2665silent_trace … t →
     2666state_rel … m keep abs_top abs_tail s1 s1' →
     2667∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     2668state_rel  … m keep abs_top' abs_tail s2 s2' ∧
     2669silent_trace … t'.
     2670#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
     2671#s1 #s2 #s1' #abs_top #abs_tail #t *
     2672[2: cases t -s1 -s2 [2: #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 cases H87 #H cases(H I)]
     2673#st #_ #H %{abs_top} %{s1'} %{(t_base …)} % // %2 % * ]
     2674#H #H1 lapply(correctness_lemma p p' prog no_dup) >EQt_prog normalize nodelta #H2
     2675cases(H2 … (pre_silent_is_premeasurable … H) … H1)  -H2 #abs_top' * #s2' * #t' ***** #REL'
     2676#_ #_ #_ #_ #H2 %{abs_top'} %{s2'} %{t'} %{REL'} % @H2 //
     2677qed.
  • LTS/Simulation.ma

    r3524 r3531  
    1717 ; final_is_final :
    1818   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
     19 ; io_is_io :
     20   ∀s1,s2.Srel … rel s1 s2 → as_classify … s2 = cl_io → as_classify … s1 = cl_io
    1921 ; simulate_tau:
    2022     ∀s1:S1.∀s2:S2.∀s1':S1.
     
    9698   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
    9799 }.
     100 
     101lemma io_state_case : ∀P : status_class → Prop.∀s.
     102(s = cl_io → P s) → (s ≠ cl_io → P s) → P s.
     103#P * #H1 #H2 [2: @H1 %] @H2 % #EQ destruct
     104qed.
     105
     106lemma simulate_labelled_action : ∀S1,S2 : abstract_status.
     107∀rel : relations S1 S2.
     108∀s1,s2 : S1.∀s1' : S2.
     109∀l : ActionLabel.
     110simulation_conditions … rel →
     111is_costlabelled_act l →
     112(is_call_act l → is_call_post_label … s1) →
     113as_execute … l s1 s2 →
     114Srel … rel s1 s1' →
     115¬ (as_classify … s1 = cl_io ∧ as_classify … s2 = cl_io) →
     116∃pre_em,post_em,s2' : S2.
     117∃t_pre : raw_trace … s1' pre_em.
     118∃t_post : raw_trace … post_em s2'.
     119silent_trace … t_pre ∧ silent_trace … t_post ∧
     120as_execute … l pre_em post_em ∧
     121(is_call_act l → is_call_post_label … pre_em) ∧
     122Srel … rel s2 s2'.
     123#S1 #S2 #rel #s1 #s2 #s1' *
     124[ #f #c | * [|#lbl] | * [|#lbl]]
     125#sim * #Hcall #prf #REL * #Hio
     126[ cases(simulate_call_pl … sim … prf … REL)
     127  [2: @Hcall %{f} %{c} %
     128  |3: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
     129  |4: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
     130  ]
     131  #pre_em * #post_em * #s2' * #t_pre ** #prf' #call * #t_post ** #REL' #sil_tpre #sil_tpost
     132  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % // % // % // %1 //
     133| cases(simulate_ret_l … sim … prf … REL)
     134  [2: % #ABS lapply(io_exiting … S1 … ABS … prf) * #lbl #EQ destruct
     135  |3: % #ABS lapply(io_entering … S1 … ABS … prf) * #lbl #EQ destruct
     136  ]
     137  #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
     138  %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
     139  % // % // %1 //
     140| @(io_state_case … (as_classify … s1)) @(io_state_case … (as_classify … s2))
     141  #class_s2 #class_s1
     142  [ cases(Hio ?) /2/
     143  | cases(simulate_io_out … sim … prf … REL) //
     144    #post_em * #s2' * #t_post *** #sil_tpost #prf' #Hclass #REL'
     145    %{s1'} %{post_em} %{s2'} %{(t_base …)} %{t_post} % // % [2: * #f * #c #EQ destruct]
     146    % // % [%2 %*] % assumption
     147  | cases(simulate_io_in … sim … prf … REL) //
     148    #pre_em * #s2' * #t_pre *** #sil_tpre #prf' #Hclass #REL'
     149    %{pre_em} %{s2'} %{s2'} %{t_pre} %{(t_base …)} % // % [2: * #f * #c #EQ destruct]
     150    % // % [% assumption]  %2 % *
     151  | cases(simulate_label … sim … prf … REL) //
     152    #pre_em * #post_em * #s2' * #t_pre * #prf' * #t_post ** #REL' #sil_tpre #sil_tpost
     153    %{pre_em} %{post_em} %{s2'} %{t_pre} %{t_post} % // % [2: * #f * #c #EQ destruct]
     154    % // % // %1 //
     155  ]
     156]
     157qed. 
     158   
     159 
     160 
     161(* silente simula in silente *)
    98162
    99163
     
    339403qed.
    340404
     405lemma silent_in_silent : ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     406 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     407  simulation_conditions … rel →
     408  ∀s2 : S2.Srel … rel s1 s2 →
     409  silent_trace … t1 →
     410  ∃s2'. ∃t2: raw_trace … s2 s2'.
     411    silent_trace … t2 ∧
     412    Srel … rel s1' s2'.
     413#S1 #S2 #rel #s1 #s1' #t1 #sim #s2 #REL *
     414[ #pre_sil_ti0 cases(simulates_pre_mesurable … sim … (pre_silent_is_premeasurable … pre_sil_ti0) … REL)
     415  [2: % #H
     416      lapply(head_of_premeasurable_is_not_io … (pre_silent_is_premeasurable … pre_sil_ti0))
     417      >(io_is_io … sim … H) // * /2/
     418  ]
     419  #s2' * #t2 *** * #H1 #H2 #H3 #H4 #H5 %{s2'} %{t2} % /3 by or_introl/
     420| cases t1 in REL; [ #st #H #_ %{s2} %{(t_base …)} % [%2 % * ] // ]
     421  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 cases H14 #H cases(H I)
     422]
     423qed.
     424
     425lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
     426∀s1,s2 : S.∀t : raw_trace … s1 s2.
     427pre_measurable_trace … t →
     428as_classify … s2 ≠ cl_io.
     429#S #s1 #s2 #t #H elim H //
     430qed.
     431
    341432theorem simulates_measurable:
    342433 ∀S1,S2: abstract_status.
     
    348439 ∀s1,s2. measurable … s1 s2 … t →
    349440 
    350  ∀si': S2. as_classify … si' ≠ cl_io →
     441 ∀si': S2.
     442 (as_classify … si' = cl_io →  as_classify … si = cl_io) → 
    351443 
    352444 Srel … rel si si' →
     
    359451 
    360452 ∃s1',s2'. measurable … s1' s2' … t'.
    361 #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
    362 cases(simulates_pre_mesurable … rel … t … Rsi_si') //
    363 [2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
    364 #Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
    365 <EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
    366 #H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
    367  >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
    368 qed.
     453#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'
     454cases Hmeas -Hmeas #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *******
     455#pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init
     456cases(silent_in_silent … sim_rel … Rsi_si' sil_ti0)
     457#s0' * #ti0' * #sil_ti0' #Rs0_s0'
     458cases(simulate_labelled_action … prf1 … Rs0_s0') /2/
     459     [2: % * #H1 #H2 lapply(head_of_premeasurable_is_not_io … pre_t12) >H2 * /2/ ]
     460#s0'' * #s1'' * #s1' * #t_s0'' * #t_s1'' **** #sil_ts0'' #sil_ts1'' #prf1' #Hcall_init'
     461#Rs1_s1'
     462cases(simulates_pre_mesurable … sim_rel … pre_t12 … Rs1_s1')
     463[2: % #H lapply(head_of_premeasurable_is_not_io … pre_t12) >(io_is_io … sim_rel … H) // * /2/ ]
     464#s2' * #t12' **** #pre_t12' #EQcost #Rs2_s2' #_ #_
     465cases(simulate_labelled_action … prf2 … Rs2_s2') /2/
     466  [2: % * #H1 #H2 lapply(tail_of_premeasurable_is_not_io … pre_t12) >H1 * /2/]
     467#s2'' * #s3'' * #s3' * #t_s2'' * #t_s3'' **** #sil_ts2'' #sil_ts3'' #prf2' #Hcall_fin' #Rs3_s3'
     468cases(silent_in_silent … sim_rel … Rs3_s3' sil_t3n)
     469#sn' * #t_3n' * #sil_t3n' #Rsn_sn' %{sn'}
     470%{(ti0'@ t_s0'' @ (t_ind … prf1' (t_s1''@t12' @ t_s2'' @ (t_ind … prf2' (t_s3'' @ t_3n')))))}
     471% [ % // cases daemon (*TODO*) ]
     472%{s1''} %{s3''} whd %{s0''} %{s2''} %{(ti0' @t_s0'')} %{(t_s1'' @ t12' @ t_s2'')}
     473%{(t_s3'' @ t_3n')} %{l1} %{l2} %{prf1'} %{prf2'} % [2: /2/]
     474% [2: /2 by append_silent/] % [2: /2 by append_silent/] % [2: /2/] % // % // % //
     475@append_premeasurable_silent /2/
     476qed.
     477
     478
  • LTS/Traces.ma

    r3524 r3531  
    638638 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
    639639λS,si,s1,s3,sn,t.
    640  pre_measurable_trace … t ∧
    641640 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
    642641 ∃l1,l2,prf1,prf2.
     642 pre_measurable_trace … t12 ∧
    643643  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
    644644 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
    645  ∧ silent_trace … ti0 ∧ silent_trace … t3n.
     645 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
    646646
    647647 
     
    791791lemma measurable_is_measurable_suffix : ∀S : abstract_status.
    792792∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
    793 #S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *****
     793#S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
    794794#EQ destruct /11 width=20 by conj,ex_intro/
    795795qed.
     
    863863qed.
    864864
     865(*
     866
    865867lemma measurable_suffix_is_measurable:
    866868∀S : abstract_status.
     
    881883  /20 width=20 by conj,ex_intro/
    882884]
    883 qed.
     885qed.*)
Note: See TracChangeset for help on using the changeset viewer.