Changeset 3550


Ignore:
Timestamp:
Apr 8, 2015, 7:53:48 PM (6 years ago)
Author:
piccolo
Message:

chiusi dei demoni

File:
1 edited

Legend:

Unmodified
Added
Removed

  • LTS/Lang_meas.ma

    r3549 r3550  
    163163  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
    164164  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
    165 | cases daemon
    166 | cases daemon
     165| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
     166  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
     167  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     168  [1,2,3,4,6,7:
     169    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
     170       | #lin #io #lout #instr #_ ]
     171          #_ whd in ⊢ (??%% → ?);
     172          [ |
     173          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     174          | cases(call_post_clean ?????); normalize nodelta
     175            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     176               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     177                 [| #z cases(?∧?) normalize nodelta
     178                 ]
     179               ]
     180            ]
     181          | cases(call_post_clean ?????) normalize nodelta
     182             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     183                [ cases (?==?) normalize nodelta ]
     184             ]]
     185          | cases(call_post_clean ?????) normalize nodelta
     186             [| #x cases(? ∧ ?) normalize nodelta ]
     187          ]
     188          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     189   ]
     190   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     191   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
     192   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
     193   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     194   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
     195| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
     196  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
     197  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     198  [1,2,3,4,6,7:
     199    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
     200       | #lin #io #lout #instr #_ ]
     201          #_ whd in ⊢ (??%% → ?);
     202          [ |
     203          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     204          | cases(call_post_clean ?????); normalize nodelta
     205            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     206               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     207                 [| #z cases(?∧?) normalize nodelta
     208                 ]
     209               ]
     210            ]
     211          | cases(call_post_clean ?????) normalize nodelta
     212             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     213                [ cases (?==?) normalize nodelta ]
     214             ]]
     215          | cases(call_post_clean ?????) normalize nodelta
     216             [| #x cases(? ∧ ?) normalize nodelta ]
     217          ]
     218          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     219   ]
     220   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     221   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
     222   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
     223   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     224   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
    167225| #s1 #s2 #lin #io #lout #instr #men #EQcode  #EQeval #EQcodes2 #EQcont_s2 #EQ destruct #Hio * whd in match state_rel;
    168226  normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
    169227  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode inversion(code ? s1')
    170   [1,2,3,4,5,6: cases daemon (* ASSURDI*)
     228  [1,2,3,4,5,6:
     229    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     230        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
     231          #_ whd in ⊢ (??%% → ?);
     232          [ |
     233          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     234          | cases(call_post_clean ?????); normalize nodelta
     235            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     236               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     237                 [| #z cases(?∧?) normalize nodelta
     238                 ]
     239               ]
     240            ]
     241          | cases(call_post_clean ?????) normalize nodelta
     242            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     243               [| #y cases(?∧?) normalize nodelta
     244               ]
     245            ]
     246          | cases(call_post_clean ?????) normalize nodelta
     247             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     248                [ cases (?==?) normalize nodelta ]
     249             ]]
     250          ]
     251          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    171252  | #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    172253    [ #EQ destruct] #x
    … …  
    177258  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
    178259  #H1 #a_top #a_tail normalize nodelta #Hcall **** #HH1 >EQcode inversion(code ? s1')
    179   [1,2,3,4,5,7: cases daemon (* ASSURDI*)
     260  [1,2,3,4,5,7:
     261    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     262        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
     263          #_ whd in ⊢ (??%% → ?);
     264          [ |
     265          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     266          | cases(call_post_clean ?????); normalize nodelta
     267            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     268               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     269                 [| #z cases(?∧?) normalize nodelta
     270                 ]
     271               ]
     272            ]
     273          | cases(call_post_clean ?????) normalize nodelta
     274            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     275               [| #y cases(?∧?) normalize nodelta
     276               ]
     277            ]
     278         | cases(call_post_clean ?????) normalize nodelta
     279             [| #x cases(? ∧ ?) normalize nodelta ]
     280         ]
     281         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    180282  |*: #f' #act_p' #lbl' #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    181283    [ #EQ destruct] #x cases lbl' in EQcode_s1'; normalize nodelta [ #_ #EQ destruct] #lbl'' #EQcode_s1'
    … …  
    192294  whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta [ #_ *]
    193295  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode inversion(code … s1')
    194   [1,3,4,5,6,7: cases daemon (*ASSURDI*)
     296  [1,3,4,5,6,7:
     297       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     298        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
     299          #_ whd in ⊢ (??%% → ?);
     300          [
     301          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     302          | cases(call_post_clean ?????); normalize nodelta
     303            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     304               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     305                 [| #z cases(?∧?) normalize nodelta
     306                 ]
     307               ]
     308            ]
     309          | cases(call_post_clean ?????) normalize nodelta
     310            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     311               [| #y cases(?∧?) normalize nodelta
     312               ]
     313            ]
     314         | cases(call_post_clean ?????) normalize nodelta
     315             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     316                [ cases (?==?) normalize nodelta ]
     317             ]]
     318         | cases(call_post_clean ?????) normalize nodelta
     319             [| #x cases(? ∧ ?) normalize nodelta ]
     320         ]
     321         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    195322  | #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct
    196323    >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    … …  
    215342
    216343lemma bool_true : ∀b : bool.b=true → b. * // #EQ destruct qed.
    217 (*
    218 axiom actionlabel_of_cost_is_not_empty : ∀l : ActionLabel.
    219 is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c].
    220 *)
     344
    221345lemma labelled_action_is_correct :
    222346∀p,p',prog.
    … …  
    247371    cases cost_lbl #HH2 #EQ destruct #EQget #EQ_cleaned #EQstore #EQio #EQ destruct
    248372    >EQcode_s1 in EQ_cleaned; inversion(code ? s1')
    249     [2,3,4,5,6,7: cases daemon (*ASSURDI*)] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
     373    [2,3,4,5,6,7: [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     374            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     375          #_ whd in ⊢ (??%% → ?);
     376          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     377          | cases(call_post_clean ?????); normalize nodelta
     378            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     379               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     380                 [| #z cases(?∧?) normalize nodelta
     381                 ]
     382               ]
     383            ]
     384          | cases(call_post_clean ?????) normalize nodelta
     385            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     386               [| #y cases(?∧?) normalize nodelta
     387               ]
     388            ]
     389          | cases(call_post_clean ?????) normalize nodelta
     390             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     391                [ cases (?==?) normalize nodelta ]
     392             ]]
     393          | cases(call_post_clean ?????) normalize nodelta
     394             [| #x cases(? ∧ ?) normalize nodelta ]
     395          ]
     396          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
    250397    %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
    251398    [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %]
    … …  
    256403  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta
    257404  [#_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
    258   [1,2,4,5,6,7: cases daemon (*ASSURDI*)] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     405  [1,2,4,5,6,7: [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     406            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     407          #_ whd in ⊢ (??%% → ?);
     408          [ |
     409          | cases(call_post_clean ?????); normalize nodelta
     410            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     411               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     412                 [| #z cases(?∧?) normalize nodelta
     413                 ]
     414               ]
     415            ]
     416          | cases(call_post_clean ?????) normalize nodelta
     417            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     418               [| #y cases(?∧?) normalize nodelta
     419               ]
     420            ]
     421          | cases(call_post_clean ?????) normalize nodelta
     422             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     423                [ cases (?==?) normalize nodelta ]
     424             ]]
     425          | cases(call_post_clean ?????) normalize nodelta
     426             [| #x cases(? ∧ ?) normalize nodelta ]
     427          ]
     428          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?);
    259429  inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned
    260430  cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget]
    … …  
    271441  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *]
    272442  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
    273   [1,2,3,4,5,6: cases daemon (*ASSURDI*) ]
     443  [1,2,3,4,5,6:  [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     444        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
     445          #_ whd in ⊢ (??%% → ?);
     446          [ |
     447          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     448          | cases(call_post_clean ?????); normalize nodelta
     449            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     450               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     451                 [| #z cases(?∧?) normalize nodelta
     452                 ]
     453               ]
     454            ]
     455          | cases(call_post_clean ?????) normalize nodelta
     456            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     457               [| #y cases(?∧?) normalize nodelta
     458               ]
     459            ]
     460          | cases(call_post_clean ?????) normalize nodelta
     461             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     462                [ cases (?==?) normalize nodelta ]
     463             ]]
     464          ]
     465          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    274466  #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct]
    275467  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
Note: See TracChangeset for help on using the changeset viewer.