# Theory Transition_System

```theory Transition_System
imports
Residual
begin

section ‹Nominal Transition Systems and Bisimulations›

subsection ‹Basic Lemmas›

lemma symp_on_eqvt [eqvt]:
assumes "symp_on A R" shows "symp_on (p ∙ A) (p ∙ R)"
using assms
by (auto simp: symp_on_def permute_fun_def permute_set_def permute_pure)

lemma symp_eqvt:
assumes "symp R" shows "symp (p ∙ R)"
using assms
by (auto simp: symp_on_def permute_fun_def permute_pure)

subsection ‹Nominal transition systems›

locale nominal_ts =
fixes satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool"                (infix "⊢" 70)
and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool"  (infix "→" 70)
assumes satisfies_eqvt [eqvt]: "P ⊢ φ ⟹ p ∙ P ⊢ p ∙ φ"
and transition_eqvt [eqvt]: "P → αQ ⟹ p ∙ P → p ∙ αQ"
begin

lemma transition_eqvt':
assumes "P → ⟨α,Q⟩" shows "p ∙ P → ⟨p ∙ α, p ∙ Q⟩"
using assms by (metis abs_residual_pair_eqvt transition_eqvt)

end

subsection ‹Bisimulations›

context nominal_ts
begin

definition is_bisimulation :: "('state ⇒ 'state ⇒ bool) ⇒ bool" where
"is_bisimulation R ≡
symp R ∧
(∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧
(∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q')))"

definition bisimilar :: "'state ⇒ 'state ⇒ bool"  (infix "∼⋅" 100) where
"P ∼⋅ Q ≡ ∃R. is_bisimulation R ∧ R P Q"

text ‹@{const bisimilar} is an equivariant equivalence relation.›

lemma is_bisimulation_eqvt (*[eqvt]*):
assumes "is_bisimulation R" shows "is_bisimulation (p ∙ R)"
using assms unfolding is_bisimulation_def
proof (clarify)
assume 1: "symp R"
assume 2: "∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)"
assume 3: "∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q'))"
have "symp (p ∙ R)" (is ?S)
using 1 by (simp add: symp_eqvt)
moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" (is ?T)
proof (clarify)
fix P Q φ
assume *: "(p ∙ R) P Q" and **: "P ⊢ φ"
from * have "R (-p ∙ P) (-p ∙ Q)"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
then show "Q ⊢ φ"
using 2 ** by (metis permute_minus_cancel(1) satisfies_eqvt)
qed
moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'))" (is ?U)
proof (clarify)
fix P Q α P'
assume *: "(p ∙ R) P Q" and **: "bn α ♯* Q" and ***: "P → ⟨α,P'⟩"
from * have "R (-p ∙ P) (-p ∙ Q)"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
moreover have "bn (-p ∙ α) ♯* (-p ∙ Q)"
using ** by (metis bn_eqvt fresh_star_permute_iff)
moreover have "-p ∙ P → ⟨-p ∙ α, -p ∙ P'⟩"
using *** by (metis transition_eqvt')
ultimately obtain Q' where T: "-p ∙ Q → ⟨-p ∙ α,Q'⟩" and R: "R (-p ∙ P') Q'"
using 3 by metis
from T have "Q → ⟨α, p ∙ Q'⟩"
by (metis permute_minus_cancel(1) transition_eqvt')
moreover from R have "(p ∙ R) P' (p ∙ Q')"
by (metis eqvt_apply eqvt_lambda permute_bool_def unpermute_def)
ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'"
by metis
qed
ultimately show "?S ∧ ?T ∧ ?U" by simp
qed

lemma bisimilar_eqvt (*[eqvt]*):
assumes "P ∼⋅ Q" shows "(p ∙ P) ∼⋅ (p ∙ Q)"
proof -
from assms obtain R where *: "is_bisimulation R ∧ R P Q"
unfolding bisimilar_def ..
then have "is_bisimulation (p ∙ R)"
moreover from "*" have "(p ∙ R) (p ∙ P) (p ∙ Q)"
by (metis eqvt_apply permute_boolI)
ultimately show "(p ∙ P) ∼⋅ (p ∙ Q)"
unfolding bisimilar_def by auto
qed

lemma bisimilar_reflp: "reflp bisimilar"
proof (rule reflpI)
fix x
have "is_bisimulation (=)"
unfolding is_bisimulation_def by (simp add: symp_def)
then show "x ∼⋅ x"
unfolding bisimilar_def by auto
qed

lemma bisimilar_symp: "symp bisimilar"
proof (rule sympI)
fix P Q
assume "P ∼⋅ Q"
then obtain R where *: "is_bisimulation R ∧ R P Q"
unfolding bisimilar_def ..
then have "R Q P"
unfolding is_bisimulation_def by (simp add: symp_def)
with "*" show "Q ∼⋅ P"
unfolding bisimilar_def by auto
qed

lemma bisimilar_is_bisimulation: "is_bisimulation bisimilar"
unfolding is_bisimulation_def proof
show "symp (∼⋅)"
by (fact bisimilar_symp)
next
show "(∀P Q. P ∼⋅ Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧
(∀P Q. P ∼⋅ Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅ Q')))"
by (auto simp add: is_bisimulation_def bisimilar_def) blast
qed

lemma bisimilar_transp: "transp bisimilar"
proof (rule transpI)
fix P Q R
assume PQ: "P ∼⋅ Q" and QR: "Q ∼⋅ R"
let ?bisim = "bisimilar OO bisimilar"
have "symp ?bisim"
proof (rule sympI)
fix P R
assume "?bisim P R"
then obtain Q where "P ∼⋅ Q" and "Q ∼⋅ R"
by blast
then have "R ∼⋅ Q" and "Q ∼⋅ P"
by (metis bisimilar_symp sympE)+
then show "?bisim R P"
by blast
qed
moreover have "∀P Q. ?bisim P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)"
using bisimilar_is_bisimulation is_bisimulation_def by auto
moreover have "∀P Q. ?bisim P Q ⟶
(∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'))"
proof (clarify)
fix P R Q α P'
assume PR: "P ∼⋅ R" and RQ: "R ∼⋅ Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term R}, without touching~@{term Q}›
obtain p where 1: "(p ∙ bn α) ♯* R" and 2: "supp (⟨α,P'⟩, Q) ♯* p"
proof (rule at_set_avoiding2[of "bn α" R "(⟨α,P'⟩, Q)", THEN exE])
show "finite (bn α)" by (fact bn_finite)
next
show "finite (supp R)" by (fact finite_supp)
next
show "finite (supp (⟨α,P'⟩, Q))" by (simp add: finite_supp supp_Pair)
next
show "bn α ♯* (⟨α,P'⟩, Q)" by (simp add: fresh fresh_star_Pair)
qed metis
from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp Q ♯* p"
from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩"
using supp_perm_eq by fastforce
then obtain pR' where 5: "R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅ pR'"
using PR trans 1 by (metis (mono_tags, lifting) bisimilar_is_bisimulation bn_eqvt is_bisimulation_def)
from fresh and 4 have "bn (p ∙ α) ♯* Q"
by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
then obtain pQ' where 7: "Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅ pQ'"
using RQ 5 by (metis (full_types) bisimilar_is_bisimulation is_bisimulation_def)
from 7 have "Q → ⟨α, -p ∙ pQ'⟩"
using 4 by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt')
moreover from 6 and 8 have "?bisim P' (-p ∙ pQ')"
by (metis (no_types, opaque_lifting) bisimilar_eqvt permute_minus_cancel(2) relcompp.simps)
ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'"
by metis
qed
ultimately have "is_bisimulation ?bisim"
unfolding is_bisimulation_def by metis
moreover have "?bisim P R"
using PQ QR by blast
ultimately show "P ∼⋅ R"
unfolding bisimilar_def by meson
qed

lemma bisimilar_equivp: "equivp bisimilar"
by (metis bisimilar_reflp bisimilar_symp bisimilar_transp equivp_reflp_symp_transp)

lemma bisimilar_simulation_step:
assumes "P ∼⋅ Q" and "bn α ♯* Q" and "P → ⟨α,P'⟩"
obtains Q' where "Q → ⟨α,Q'⟩" and "P' ∼⋅ Q'"
using assms by (metis (poly_guards_query) bisimilar_is_bisimulation is_bisimulation_def)

end

end
```