Changeset 250 for C-semantics/CexecIOcomplete.ma

Timestamp:

Nov 22, 2010, 2:40:22 PM (9 years ago)

Author:

campbell

Message:

Begin separating soundness from executable semantics.

File:

• C-semantics/CexecIOcomplete.ma (modified) (3 diffs)

C-semantics/CexecIOcomplete.ma

@@ -61 +61 @@
 
 ntheorem the_initial_state:
-  ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.
+  ∀p,s. initial_state p s → yieldsIObare ? (make_initial_state p) s.
 #p s; ncases p; #fns main globs H;
-napply remove_io_sig;
 ninversion H;
 #b f e1 e2 e3;
+nwhd in ⊢ (??%?);
 nrewrite > e1;
 nwhd in ⊢ (??%?);
@@ -84 +84 @@
 
 nlemma cast_complete: ∀m,v,ty,ty',v'.
-  cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.
+  cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'.
 #m v ty ty' v' H;
 nelim H;
@@ -91 +91 @@
 ##| #m i sz sz' sg; napply refl;
 ##| #m f sz sz'; napply refl;
-##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;
+##| #m sp sp' ty ty' b ofs H1 H2 H3;
     nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
     nwhd in ⊢ (??%?);