Changeset 2043

Timestamp:

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

Author:

sacerdot

Message:

Broken code commented out.

File:

• src/joint/semantics_blocks.ma (modified) (10 diffs)

src/joint/semantics_blocks.ma

@@ -114 +114 @@
   ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
 
+(*
 lemma m_pred
 
@@ -119 +120 @@
   ∀f : X → monad M Y.m_pred MP P … m →
   ! x ← m ; f x = ! x ←  
+*)
 
 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.
 #O #I #X #m elim m // qed.
+
+(*
 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
 #X #m elim m // qed.
-
+*)
+
+(*
 lemma never_calls_no_init : ∀p,globals,ge,s.
   never_calls p globals ge s →
@@ -213 +219 @@
 [ * #lbl * | #id #fd #args #dest ] #st * %
 qed.
+*)
 
 lemma seq_list_labels_append : ∀p,globals,b1,b2.
@@ -224 +231 @@
 qed.
 
+(*
 lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
   eval_seq_list globals p ge st (b1@b2) =
@@ -302 +310 @@
 #y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
 qed.
-
+*)
 lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
   block_cont_labels p globals ty (b1 @ b2) =
@@ -313 +321 @@
 >associative_append %
 qed.
-
+(*
 lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
   ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
@@ -375 +383 @@
 [1,2: >m_return_bind normalize nodelta % | % ]
 qed.
-
+*)
 
 
@@ -514 +522 @@
 >EQ1 >m_return_bind >EQ3 %
 qed.
-
+(*
 lemma eval_seq_list_in_code :
   ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
@@ -706 +714 @@
     match following with
     [ Some l ⇒ succ_pc p p 
+*)