Theory Bisimulation

section ‹Proof Infrastructure›
subsection ‹Bisimulation›

theory Bisimulation
imports
  Stuttering
begin

(* WIP strong bisimilar
fun strongly_bisimilar :: "
(IRGraph × ID × MapState × FieldRefHeap) rel
⇒ (IRGraph × ID × MapState × FieldRefHeap)
⇒ (IRGraph × ID × MapState × FieldRefHeap)
⇒ bool"
  where
  "strongly_bisimilar ℛ (g1, nid1, m1, h1) (g2, nid2, m2, h2) =
    ((((g1, nid1, m1, h1), (g2, nid2, m2, h2)) ∈ ℛ) ⟶
    ((∀P'. (g1 ⊢ (nid1, m1, h1) → P') ⟶ (∃Q' . (g2 ⊢ (nid2, m2, h2) → Q') ∧ ((g1,P'), (g2,Q')) ∈ ℛ)) ∧
    (∀Q'. (g2 ⊢ (nid2, m2, h2) → Q') ⟶ (∃P' . (g1 ⊢ (nid1, m1, h1) → P') ∧ ((g1,P'), (g2,Q')) ∈ ℛ))))"
*)

inductive weak_bisimilar :: "ID ⇒ IRGraph ⇒ IRGraph ⇒ bool"
  ("_ . _ ∼ _") for nid where
  "⟦∀P'. (g m p h ⊢ nid ↝ P') ⟶ (∃Q' . (g' m p h ⊢ nid ↝ Q') ∧ P' = Q');
    ∀Q'. (g' m p h ⊢ nid ↝ Q') ⟶ (∃P' . (g m p h ⊢ nid ↝ P') ∧ P' = Q')⟧
  ⟹ nid . g ∼ g'"

text ‹A strong bisimilution between no-op transitions›
inductive strong_noop_bisimilar :: "ID ⇒ IRGraph ⇒ IRGraph ⇒ bool"
  ("_ | _ ∼ _") for nid where
  "⟦∀P'. (g, p ⊢ (nid, m, h) → P') ⟶ (∃Q' . (g', p ⊢ (nid, m, h) → Q') ∧ P' = Q');
    ∀Q'. (g', p ⊢ (nid, m, h) → Q') ⟶ (∃P' . (g, p ⊢ (nid, m, h) → P') ∧ P' = Q')⟧
  ⟹ nid | g ∼ g'"

lemma lockstep_strong_bisimilulation:
  assumes "g' = replace_node nid node g"
  assumes "g, p ⊢ (nid, m, h) → (nid', m, h)"
  assumes "g', p ⊢ (nid, m, h) → (nid', m, h)"
  shows "nid | g ∼ g'"
  by (metis strong_noop_bisimilar.simps stepDet assms(2,3))

lemma no_step_bisimulation:
  assumes "∀m p h nid' m' h'. ¬(g, p ⊢ (nid, m, h) → (nid', m', h'))"
  assumes "∀m p h nid' m' h'. ¬(g', p ⊢ (nid, m, h) → (nid', m', h'))"
  shows "nid | g ∼ g'"
  by (simp add: assms(1,2) strong_noop_bisimilar.intros)

end