Changeset 2529 for src/joint/semanticsUtils.ma

Timestamp:

Dec 4, 2012, 6:16:25 PM (8 years ago)

Author:

tranquil

Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:

• src/joint/semanticsUtils.ma (modified) (3 diffs)

src/joint/semanticsUtils.ma

@@ -75 +75 @@
   mk_sem_params
     g_pars
-    (mk_more_sem_params
-      g_pars
-      (spars ?)
-      (word_of_identifier ?)
-      (an_identifier ?)
-      ? (refl …)
-    ).
+    (spars ?)
+    (word_of_identifier ?)
+    (an_identifier ?)
+    ? (refl …).
 * #p % qed.
 
@@ -89 +86 @@
 @pos_elim [%]
 #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
-
 
 definition make_sem_lin_params :
@@ -99 +95 @@
   mk_sem_params
     lin_pars
-    (mk_more_sem_params
-      lin_pars
-      (spars ?)
-      succ_pos_of_nat
-      (λp.pred (nat_of_pos p))
-      ??
-    ).
-[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
-| #n >nat_succ_pos %
+    (spars ?)
+    succ_pos_of_nat
+    (λp.pred (nat_of_pos p))
+    ??.
+[ #n >nat_succ_pos %
+| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
 ] qed.
+
+
+
+
+lemma fetch_statement_eq : ∀p:sem_params.∀g.
+  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
+  ∀i,fn,s.
+  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
+  let pt ≝ point_of_pc … ptr in
+  stmt_at … (joint_if_code … fn) pt = Some ? s →
+  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
+#p #g #ge #ptr #i #f #s #EQ1 #EQ2
+whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
+>EQ2 %
+qed.
+
+lemma fetch_statement_inv : ∀p:sem_params.∀g.
+  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
+  ∀i,fn,s.
+  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
+  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
+  let pt ≝ point_of_pc p ptr in
+  stmt_at … (joint_if_code … fn) pt = Some ? s.
+#p #g #ge #ptr #i #fn #s #H
+elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
+elim (bind_inversion ????? H) #s' * #H
+lapply (opt_eq_from_res ???? H) -H #EQ2
+whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
+qed.
+