 Timestamp:
 Jun 8, 2012, 11:41:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics_blocks.ma
r1999 r2043 114 114 ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed. 115 115 116 (* 116 117 lemma m_pred 117 118 … … 119 120 ∀f : X → monad M Y.m_pred MP P … m → 120 121 ! x ← m ; f x = ! x ← 122 *) 121 123 122 124 definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝ … … 161 163 lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m. 162 164 #O #I #X #m elim m // qed. 165 166 (* 163 167 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m. 164 168 #X #m elim m // qed. 165 169 *) 170 171 (* 166 172 lemma never_calls_no_init : ∀p,globals,ge,s. 167 173 never_calls p globals ge s → … … 213 219 [ * #lbl *  #id #fd #args #dest ] #st * % 214 220 qed. 221 *) 215 222 216 223 lemma seq_list_labels_append : ∀p,globals,b1,b2. … … 224 231 qed. 225 232 233 (* 226 234 lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2. 227 235 eval_seq_list globals p ge st (b1@b2) = … … 302 310 #y * #EQ <EQ y * @rel_io_eq normalize nodelta % 303 311 qed. 304 312 *) 305 313 lemma block_cont_labels_append : ∀p,globals,ty,b1,b2. 306 314 block_cont_labels p globals ty (b1 @ b2) = … … 313 321 >associative_append % 314 322 qed. 315 323 (* 316 324 lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st. 317 325 ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty. … … 375 383 [1,2: >m_return_bind normalize nodelta %  % ] 376 384 qed. 377 385 *) 378 386 379 387 … … 514 522 >EQ1 >m_return_bind >EQ3 % 515 523 qed. 516 524 (* 517 525 lemma eval_seq_list_in_code : 518 526 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst. … … 706 714 match following with 707 715 [ Some l ⇒ succ_pc p p 716 *)
Note: See TracChangeset
for help on using the changeset viewer.