Theory Stuttering

subsection ‹Stuttering›

theory Stuttering
  imports
    Semantics.IRStepThms
begin

inductive stutter:: "IRGraph ⇒ MapState ⇒ Params ⇒ FieldRefHeap ⇒ ID ⇒ ID ⇒ bool" ("_ _ _ _ ⊢ _ ↝ _" 55)
  for g m p h where

  StutterStep:
  "⟦g, p ⊢ (nid,m,h) → (nid',m,h)⟧
   ⟹ g m p h ⊢ nid ↝ nid'" |

  Transitive:
  "⟦g, p ⊢ (nid,m,h) → (nid'',m,h);
    g m p h ⊢ nid'' ↝ nid'⟧
   ⟹ g m p h ⊢ nid ↝ nid'"

lemma stuttering_successor:
  assumes "(g, p ⊢ (nid, m, h) → (nid', m, h))"
  shows "{P'. (g m p h ⊢ nid ↝ P')} = {nid'} ∪ {nid''. (g m p h ⊢ nid' ↝ nid'')}"
proof -
  have nextin: "nid' ∈ {P'. (g m p h ⊢ nid ↝ P')}"
    using assms StutterStep by fast
  have nextsubset: "{nid''. (g m p h ⊢ nid' ↝ nid'')} ⊆ {P'. (g m p h ⊢ nid ↝ P')}"
    by (metis Collect_mono assms stutter.Transitive)
  have "∀n ∈ {P'. (g m p h ⊢ nid ↝ P')} . n = nid' ∨ n ∈ {nid''. (g m p h ⊢ nid' ↝ nid'')}"
    by (metis (no_types, lifting) Pair_inject assms mem_Collect_eq stutter.simps stepDet)
  then show ?thesis
    using nextin nextsubset by (auto simp add: mk_disjoint_insert)
qed

end