Changeset 379 for Csemantics/Events.ma
 Timestamp:
 Dec 6, 2010, 4:03:36 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Events.ma
r175 r379 131 131 repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. 132 132 *) 133 134 (* Ported from CompCert 1.7.1 >>> *) 135 136 (* * An alternate presentation of infinite traces as 137 infinite concatenations of nonempty finite traces. *) 138 139 ncoinductive traceinf': Type ≝ 140  Econsinf': ∀t: trace. ∀T: traceinf'. t ≠ E0 → traceinf'. 141 142 ndefinition split_traceinf' : ∀t:trace. traceinf' → t ≠ E0 → event × traceinf' ≝ 143 λt,T. 144 match t return λt0.t0 ≠ E0 → ? with 145 [ nil ⇒ ? 146  cons e t' ⇒ λ_. 147 (match t' return λt0. t' = t0 → ? with 148 [ nil ⇒ λ_.〈e, T〉 149  cons e' t'' ⇒ λE.〈e, Econsinf' t' T ?〉 150 ]) (refl ? t') 151 ]. 152 ##[ *; #NE; napply False_rect_Type0; napply NE; napply refl; 153 ## @; #E'; nrewrite > E' in E; #E; nwhd in E:(??%%); ndestruct (E); 154 ##] nqed. 155 156 nlet corec traceinf_of_traceinf' (T': traceinf') : traceinf ≝ 157 match T' with 158 [ Econsinf' t T'' NOTEMPTY ⇒ 159 match split_traceinf' t T'' NOTEMPTY with [ mk_pair e tl ⇒ 160 Econsinf e (traceinf_of_traceinf' tl) ] 161 ]. 162 163 nremark unroll_traceinf': 164 ∀T. T = match T with [ Econsinf' t T' NE ⇒ Econsinf' t T' NE ]. 165 #T; ncases T; //; nqed. 166 167 nremark unroll_traceinf: 168 ∀T. T = match T with [ Econsinf t T' ⇒ Econsinf t T' ]. 169 #T; ncases T; //; 170 nqed. 171 172 nlemma traceinf_traceinfp_app: 173 ∀t,T,NE. 174 traceinf_of_traceinf' (Econsinf' t T NE) = t ⧻ traceinf_of_traceinf' T. 175 #t; nelim t; 176 ##[ #T NE; ncases NE; #NE'; napply False_ind; napply NE'; napply refl; 177 ## #h t'; ncases t'; ##[ ##2: #h' t''; ##] #IH T NE; 178 nrewrite > (unroll_traceinf (traceinf_of_traceinf' ?)); 179 nwhd in ⊢ (??%?); //; nrewrite > (IH …); napply refl; 180 ##] nqed. 181 182 (* <<< *) 183 133 184 (* * The predicate [event_match ef vargs t vres] expresses that 134 185 the event [t] is generated when invoking external function [ef]
Note: See TracChangeset
for help on using the changeset viewer.