Changeset 2118 for src/common

Timestamp:

Jun 27, 2012, 12:04:27 PM (7 years ago)

Author:

campbell

Message:

Labelling preserves behaviour.

File:

• src/common/SmallstepExec.ma (modified) (1 diff)

src/common/SmallstepExec.ma

@@ -80 +80 @@
 *)
 
+lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
+  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
+  step … ge s = Value … 〈tr, s'〉 ∧
+  is_final … s' = Some ? r.
+#O #I #TS #ge #s #s' #tr #r
+>exec_inf_aux_unfold
+cases (step … ge s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  lapply (refl ? (is_final … s''))
+  cases (is_final … s'') in ⊢ (???% → %);
+  [ #_ whd in ⊢ (??%? → ?); #E destruct
+  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
+  ]
+] qed.
+
+lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
+  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
+  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
+#O #I #TS #ge #s #s' #tr #e
+>exec_inf_aux_unfold
+cases (step … s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  cases (is_final … s'')
+  [ #E normalize in E; destruct /2/
+  | #r #E normalize in E; destruct
+  ]
+] qed.
+
+lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
+  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
+  is_final … s' = None ?.
+#O #I #TS #ge #s #s' #tr #e
+>exec_inf_aux_unfold
+cases (step … s)
+[ 1,3: normalize #H1 #H2 try #H3 destruct
+| * #tr' #s''
+  whd in ⊢ (??%? → ?);
+  lapply (refl ? (is_final … s''))
+  cases (is_final … s'') in ⊢ (???% → %);
+  [ #F whd in ⊢ (??%? → ?); #E destruct @F
+  | #r' #_ #E whd in E:(??%?);  destruct
+  ]
+] qed.
+
+
+
 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
 { program : Type[0]