Changeset 3496 for LTS


Ignore:
Timestamp:
Sep 25, 2014, 2:43:26 PM (5 years ago)
Author:
sacerdot
Message:

Termination hypothesis greatly simplified.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3495 r3496  
    660660definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
    661661λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
    662 ∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧
    663    (is_call_act l → bool_to_Prop (is_call_post_label … s2))).
     662∧ is_costlabelled_act l.
    664663
    665664definition big_op: ∀M: monoid. list M → M ≝
     
    871870#S #st1 #st2 #st3 * // qed.
    872871
    873 lemma actionlabel_ok : ∀l : ActionLabel.
    874 (is_costlabelled_act l ∨ is_labelled_ret_act l) → ∃c.actionlabel_to_costlabel l = [c].
    875 * /2 by refl, ex_intro/
    876 [ * /2/ ** #x #EQ destruct | * /2/ ** #x #EQ destruct]
     872lemma actionlabel_ok :
     873 ∀l : ActionLabel.
     874  is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c].
     875* /2/ * /2/ *
    877876qed.
    878877
     
    901900]
    902901#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct
    903 * #Hlabelled
    904 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
     902#Hlabelled >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
    905903[2: >get_cost_label_append  >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled)
    906904   #c #EQc >EQc //
    907905]   
    908906lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
    909 [ * [3: #st] #l #prf #H1 #H2 #k #_ whd in ⊢ (??%? → ?);
     907[ * [3: #st] #l #prf #H1 #H2 #k whd in ⊢ (??%? → ?);
    910908  [3: cases prf
    911909  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
     
    945943      ]
    946944    ]
    947     whd in ⊢ (??%% → ?); #EQ destruct
    948     [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
     945    whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ]
    949946    >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    950947    #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r
     
    968965    ]
    969966  ]
    970   #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #l1_lab1 #k #pre_meas whd in ⊢ (??%? → ?);
     967  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #k #pre_meas whd in ⊢ (??%? → ?);
    971968  >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ]
    972969  >dependent_map_append
Note: See TracChangeset for help on using the changeset viewer.