Changeset 2134
 Timestamp:
 Jun 28, 2012, 12:37:38 PM (6 years ago)
 Location:
 src/Clight
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2118 r2134 1 1 2 include "Clight/label.ma". 3 include "Clight/Cexec.ma". 2 include "Clight/labelSpecification.ma". 4 3 include "Clight/CexecInd.ma". 5 4 … … 36 35 qed. 37 36 38 (* Formalise the notion of a trace with extra cost labels added. Note that 39 we don't require the left trace to be cost free. *) 40 inductive trace_with_extra_labels : trace → trace → Prop ≝ 41  twel_0 : trace_with_extra_labels E0 E0 42  twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2) 43  twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2). 37 (* Lemmas about trace_with_extra_labels *) 44 38 45 39 lemma twel_refl : ∀tr. trace_with_extra_labels tr tr. … … 53 47 #tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/ 54 48 qed. 49 55 50 56 51 theorem label_expr_ok : ∀ge,ge',en,m. … … 1091 1086 1092 1087 1093 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝1094  steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)1095  steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e1096  steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.1097 1098 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝1099  swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.1100 steps tr2 e2 (e_stop … tr2' r s2) →1101 trace_with_extra_labels tr1 tr2 →1102 sim_with_labels (e_stop … tr1 r s1) e21103  swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.1104 steps tr2 e2 e2' →1105 trace_with_extra_labels tr1 tr2 →1106 sim_with_labels e1 e2' →1107 sim_with_labels (e_step … tr1 s1 e1) e2.1108 1109 coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝1110  nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s)1111  nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e).1112 1088 1113 1089 lemma not_wrong_init : ∀p. … … 1227 1203 1228 1204 1229 theorem labelling_sim : ∀p. 1230 let e1 ≝ exec_inf … clight_fullexec p in 1231 let e2 ≝ exec_inf … clight_fullexec (clight_label p) in 1232 not_wrong_no_io e1 → 1233 sim_with_labels e1 e2. 1205 theorem labelling_sim : labelled_exec_is_equiv. 1206 whd (* let's remind ourselves of the spec *) 1234 1207 #p 1235 1208 #NW … … 1239 1212 #s2 * #I2 1240 1213 1241 whd in match (exec_inf ?? ?p) in NW ⊢ %;1242 letin ge1 ≝ (make_global ?? ?p) in NW ⊢ %;1243 change with (make_initial_state p) in match (make_initial_state ?? ?p);1214 whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %; 1215 letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %; 1216 change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p); 1244 1217 >I1 1245 1218
Note: See TracChangeset
for help on using the changeset viewer.