Changeset 2043


Ignore:
Timestamp:
Jun 8, 2012, 11:41:58 PM (5 years ago)
Author:
sacerdot
Message:

Broken code commented out.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_blocks.ma

    r1999 r2043  
    114114  ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
    115115
     116(*
    116117lemma m_pred
    117118
     
    119120  ∀f : X → monad M Y.m_pred MP P … m →
    120121  ! x ← m ; f x = ! x ← 
     122*)
    121123
    122124definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
     
    161163lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
    162164#O #I #X #m elim m // qed.
     165
     166(*
    163167lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
    164168#X #m elim m // qed.
    165 
     169*)
     170
     171(*
    166172lemma never_calls_no_init : ∀p,globals,ge,s.
    167173  never_calls p globals ge s →
     
    213219[ * #lbl * | #id #fd #args #dest ] #st * %
    214220qed.
     221*)
    215222
    216223lemma seq_list_labels_append : ∀p,globals,b1,b2.
     
    224231qed.
    225232
     233(*
    226234lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
    227235  eval_seq_list globals p ge st (b1@b2) =
     
    302310#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
    303311qed.
    304 
     312*)
    305313lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
    306314  block_cont_labels p globals ty (b1 @ b2) =
     
    313321>associative_append %
    314322qed.
    315 
     323(*
    316324lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
    317325  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
     
    375383[1,2: >m_return_bind normalize nodelta % | % ]
    376384qed.
    377 
     385*)
    378386
    379387
     
    514522>EQ1 >m_return_bind >EQ3 %
    515523qed.
    516 
     524(*
    517525lemma eval_seq_list_in_code :
    518526  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
     
    706714    match following with
    707715    [ Some l ⇒ succ_pc p p
     716*)
Note: See TracChangeset for help on using the changeset viewer.