# Theory Weak_Transition_System

```theory Weak_Transition_System
imports
Transition_System
begin

section ‹Nominal Transition Systems and Bisimulations with Unobservable Transitions›

subsection ‹Nominal transition systems with unobservable transitions›

locale weak_nominal_ts = nominal_ts satisfies transition
for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70)
and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) +
fixes τ :: 'act
assumes tau_eqvt [eqvt]: "p ∙ τ = τ"
begin

lemma bn_tau_empty [simp]: "bn τ = {}"
using bn_eqvt bn_finite tau_eqvt by (metis eqvt_def supp_finite_atom_set supp_fun_eqvt)

lemma bn_tau_fresh [simp]: "bn τ ♯* P"

inductive tau_transition :: "'state ⇒ 'state ⇒ bool" (infix "⇒" 70) where
tau_refl [simp]: "P ⇒ P"
| tau_step: "⟦ P → ⟨τ, P'⟩; P' ⇒ P'' ⟧ ⟹ P ⇒ P''"

definition observable_transition :: "'state ⇒ 'act ⇒ 'state ⇒ bool" ("_/ ⇒{_}/ _" [70, 70, 71] 71) where
"P ⇒{α} P' ≡ ∃Q Q'. P ⇒ Q ∧ Q → ⟨α, Q'⟩ ∧ Q' ⇒ P'"

definition weak_transition :: "'state ⇒ 'act ⇒ 'state ⇒ bool" ("_/ ⇒⟨_⟩/ _" [70, 70, 71] 71) where
"P ⇒⟨α⟩ P' ≡ if α = τ then P ⇒ P' else P ⇒{α} P'"

text ‹The transition relations defined above are equivariant.›

lemma tau_transition_eqvt (*[eqvt]*):
assumes "P ⇒ P'" shows "p ∙ P ⇒ p ∙ P'"
using assms proof (induction)
case (tau_refl P) show ?case
by (fact tau_transition.tau_refl)
next
case (tau_step P P' P'')
from ‹P → ⟨τ,P'⟩› have "p ∙ P → ⟨τ,p ∙ P'⟩"
using tau_eqvt transition_eqvt' by fastforce
with ‹p ∙ P' ⇒ p ∙ P''› show ?case
using tau_transition.tau_step by blast
qed

lemma observable_transition_eqvt (*[eqvt]*):
assumes "P ⇒{α} P'" shows "p ∙ P ⇒{p ∙ α} p ∙ P'"
using assms unfolding observable_transition_def by (metis transition_eqvt' tau_transition_eqvt)

lemma weak_transition_eqvt (*[eqvt]*):
assumes "P ⇒⟨α⟩ P'" shows "p ∙ P ⇒⟨p ∙ α⟩ p ∙ P'"
using assms unfolding weak_transition_def by (metis (full_types) observable_transition_eqvt permute_minus_cancel(2) tau_eqvt tau_transition_eqvt)

@{const weak_transition}.›

lemma tau_transition_trans:
assumes "P ⇒ Q" and "Q ⇒ R"
shows "P ⇒ R"
using assms by (induction, auto simp add: tau_step)

lemma observable_transitionI:
assumes "P ⇒ Q" and "Q → ⟨α, Q'⟩" and "Q' ⇒ P'"
shows "P ⇒{α} P'"
using assms observable_transition_def by blast

lemma observable_transition_stepI [simp]:
assumes "P → ⟨α, P'⟩"
shows "P ⇒{α} P'"
using assms observable_transitionI tau_refl by blast

lemma observable_tau_transition:
assumes "P ⇒{τ} P'"
shows "P ⇒ P'"
proof -
from ‹P ⇒{τ} P'› obtain Q Q' where "P ⇒ Q" and "Q → ⟨τ, Q'⟩" and "Q' ⇒ P'"
unfolding observable_transition_def by blast
then show ?thesis
by (metis tau_step tau_transition_trans)
qed

lemma weak_transition_tau_iff [simp]:
"P ⇒⟨τ⟩ P' ⟷ P ⇒ P'"

lemma weak_transition_not_tau_iff [simp]:
assumes "α ≠ τ"
shows "P ⇒⟨α⟩ P' ⟷ P ⇒{α} P'"
using assms by (simp add: weak_transition_def)

lemma weak_transition_stepI [simp]:
assumes "P ⇒{α} P'"
shows "P ⇒⟨α⟩ P'"
using assms by (cases "α = τ", simp_all add: observable_tau_transition)

lemma weak_transition_weakI:
assumes "P ⇒ Q" and "Q ⇒⟨α⟩ Q'" and "Q' ⇒ P'"
shows "P ⇒⟨α⟩ P'"
proof (cases "α = τ")
case True with assms show ?thesis
by (metis tau_transition_trans weak_transition_tau_iff)
next
case False with assms show ?thesis
using observable_transition_def tau_transition_trans weak_transition_not_tau_iff by blast
qed

end

subsection ‹Weak bisimulations›

context weak_nominal_ts
begin

definition is_weak_bisimulation :: "('state ⇒ 'state ⇒ bool) ⇒ bool" where
"is_weak_bisimulation R ≡
symp R ∧
― ‹weak static implication›
(∀P Q φ. R P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ R P Q' ∧ Q' ⊢ φ)) ∧
― ‹weak simulation›
(∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ R P' Q')))"

definition weakly_bisimilar :: "'state ⇒ 'state ⇒ bool"  (infix "≈⋅" 100) where
"P ≈⋅ Q ≡ ∃R. is_weak_bisimulation R ∧ R P Q"

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

lemma is_weak_bisimulation_eqvt (*[eqvt]*):
assumes "is_weak_bisimulation R" shows "is_weak_bisimulation (p ∙ R)"
using assms unfolding is_weak_bisimulation_def
proof (clarify)
assume 1: "symp R"
assume 2: "∀P Q φ. R P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ R P Q' ∧ 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'. Q ⇒ Q' ∧ (p ∙ R) P Q' ∧ Q' ⊢ φ)" (is ?T)
proof (clarify)
fix P Q φ
assume pR: "(p ∙ R) P Q" and phi: "P ⊢ φ"
from pR have "R (-p ∙ P) (-p ∙ Q)"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
moreover from phi have "(-p ∙ P) ⊢ (-p ∙ φ)"
by (metis satisfies_eqvt)
ultimately obtain Q' where *: "-p ∙ Q ⇒ Q'" and **: "R (-p ∙ P) Q'" and ***: "Q' ⊢ (-p ∙ φ)"
using 2 by blast
from * have "Q ⇒ p ∙ Q'"
by (metis permute_minus_cancel(1) tau_transition_eqvt)
moreover from ** have "(p ∙ R) P (p ∙ Q')"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
moreover from *** have "p ∙ Q' ⊢ φ"
by (metis permute_minus_cancel(1) satisfies_eqvt)
ultimately show "∃Q'. Q ⇒ Q' ∧ (p ∙ R) P Q' ∧ Q' ⊢ φ"
by metis
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) weak_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 weakly_bisimilar_eqvt (*[eqvt]*):
assumes "P ≈⋅ Q" shows "(p ∙ P) ≈⋅ (p ∙ Q)"
proof -
from assms obtain R where *: "is_weak_bisimulation R ∧ R P Q"
unfolding weakly_bisimilar_def ..
then have "is_weak_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 weakly_bisimilar_def by auto
qed

lemma weakly_bisimilar_reflp: "reflp weakly_bisimilar"
proof (rule reflpI)
fix x
have "is_weak_bisimulation (=)"
unfolding is_weak_bisimulation_def by (simp add: symp_def)
then show "x ≈⋅ x"
unfolding weakly_bisimilar_def by auto
qed

lemma weakly_bisimilar_symp: "symp weakly_bisimilar"
proof (rule sympI)
fix P Q
assume "P ≈⋅ Q"
then obtain R where *: "is_weak_bisimulation R ∧ R P Q"
unfolding weakly_bisimilar_def ..
then have "R Q P"
unfolding is_weak_bisimulation_def by (simp add: symp_def)
with "*" show "Q ≈⋅ P"
unfolding weakly_bisimilar_def by auto
qed

lemma weakly_bisimilar_is_weak_bisimulation: "is_weak_bisimulation weakly_bisimilar"
unfolding is_weak_bisimulation_def proof
show "symp (≈⋅)"
by (fact weakly_bisimilar_symp)
next
show "(∀P Q φ. P ≈⋅ Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ P ≈⋅ Q' ∧ Q' ⊢ φ)) ∧
(∀P Q. P ≈⋅ Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅ Q')))"
by (auto simp add: is_weak_bisimulation_def weakly_bisimilar_def) blast+
qed

lemma weakly_bisimilar_tau_simulation_step:
assumes "P ≈⋅ Q" and "P ⇒ P'"
obtains Q' where "Q ⇒ Q'" and "P' ≈⋅ Q'"
using ‹P ⇒ P'› ‹P ≈⋅ Q› proof (induct arbitrary: Q)
case (tau_refl P) then show ?case
by (metis tau_transition.tau_refl)
next
case (tau_step P P'' P')
from ‹P → ⟨τ,P''⟩› and ‹P ≈⋅ Q› obtain Q'' where "Q ⇒ Q''" and "P'' ≈⋅ Q''"
by (metis bn_tau_fresh is_weak_bisimulation_def weak_transition_def weakly_bisimilar_is_weak_bisimulation)
then show ?case
using tau_step.hyps(3) tau_step.prems(1) by (metis tau_transition_trans)
qed

lemma weakly_bisimilar_weak_simulation_step:
assumes "P ≈⋅ Q" and "bn α ♯* Q" and "P ⇒⟨α⟩ P'"
obtains Q' where "Q ⇒⟨α⟩ Q'" and "P' ≈⋅ Q'"
proof (cases "α = τ")
case True with ‹P ≈⋅ Q› and ‹P ⇒⟨α⟩ P'› and that show ?thesis
using weak_transition_tau_iff weakly_bisimilar_tau_simulation_step by force
next
case False with ‹P ⇒⟨α⟩ P'› have "P ⇒{α} P'"
by simp
then obtain P1 P2 where tauP: "P ⇒ P1" and trans: "P1 → ⟨α,P2⟩" and tauP2: "P2 ⇒ P'"
using observable_transition_def by blast
from ‹P ≈⋅ Q› and tauP obtain Q1 where tauQ: "Q ⇒ Q1" and P1Q1: "P1 ≈⋅ Q1"
by (metis weakly_bisimilar_tau_simulation_step)

― ‹rename~@{term "⟨α,P2⟩"} to avoid~@{term Q1}, without touching~@{term Q}›
obtain p where 1: "(p ∙ bn α) ♯* Q1" and 2: "supp (⟨α,P2⟩, Q) ♯* p"
proof (rule at_set_avoiding2[of "bn α" Q1 "(⟨α,P2⟩, Q)", THEN exE])
show "finite (bn α)" by (fact bn_finite)
next
show "finite (supp Q1)" by (fact finite_supp)
next
show "finite (supp (⟨α,P2⟩, Q))" by (simp add: finite_supp supp_Pair)
next
show "bn α ♯* (⟨α,P2⟩, Q)" using ‹bn α ♯* Q› by (simp add: fresh_star_Pair)
qed metis
from 2 have 3: "supp ⟨α,P2⟩ ♯* p" and 4: "supp Q ♯* p"
from 3 have "⟨p ∙ α, p ∙ P2⟩ = ⟨α,P2⟩"
using supp_perm_eq by fastforce
then obtain Q2 where trans': "Q1 ⇒⟨p ∙ α⟩ Q2" and P2Q2: "(p ∙ P2) ≈⋅ Q2"
using P1Q1 trans 1 by (metis (mono_tags, lifting) weakly_bisimilar_is_weak_bisimulation bn_eqvt is_weak_bisimulation_def)

from tauP2 have "p ∙ P2 ⇒ p ∙ P'"
by (fact tau_transition_eqvt)
with P2Q2 obtain Q' where tauQ2: "Q2 ⇒ Q'" and P'Q': "(p ∙ P') ≈⋅ Q'"
by (metis weakly_bisimilar_tau_simulation_step)

from tauQ and trans' and tauQ2 have "Q ⇒⟨p ∙ α⟩ Q'"
by (rule weak_transition_weakI)
with 4 have "Q ⇒⟨α⟩ (-p ∙ Q')"
by (metis permute_minus_cancel(2) supp_perm_eq weak_transition_eqvt)
moreover from P'Q' have "P' ≈⋅ (-p ∙ Q')"
by (metis permute_minus_cancel(2) weakly_bisimilar_eqvt)
ultimately show ?thesis ..
qed

lemma weakly_bisimilar_transp: "transp weakly_bisimilar"
proof (rule transpI)
fix P Q R
assume PQ: "P ≈⋅ Q" and QR: "Q ≈⋅ R"
let ?bisim = "weakly_bisimilar OO weakly_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 weakly_bisimilar_symp sympE)+
then show "?bisim R P"
by blast
qed
moreover have "∀P Q φ. ?bisim P Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ ?bisim P Q' ∧ Q' ⊢ φ)"
proof (clarify)
fix P Q φ R
assume phi: "P ⊢ φ" and PR: "P ≈⋅ R" and RQ: "R ≈⋅ Q"
from PR and phi obtain R' where "R ⇒ R'" and "P ≈⋅ R'" and *: "R' ⊢ φ"
using weakly_bisimilar_is_weak_bisimulation is_weak_bisimulation_def by force
from RQ and ‹R ⇒ R'› obtain Q' where "Q ⇒ Q'" and "R' ≈⋅ Q'"
by (metis weakly_bisimilar_tau_simulation_step)
from ‹R' ≈⋅ Q'› and * obtain Q'' where "Q' ⇒ Q''" and "R' ≈⋅ Q''" and **: "Q'' ⊢ φ"
using weakly_bisimilar_is_weak_bisimulation is_weak_bisimulation_def by force
from ‹Q ⇒ Q'› and ‹Q' ⇒ Q''› have "Q ⇒ Q''"
by (fact tau_transition_trans)
moreover from ‹P ≈⋅ R'› and ‹R' ≈⋅ Q''› have "?bisim P Q''"
by blast
ultimately show "∃Q'. Q ⇒ Q' ∧ ?bisim P Q' ∧ Q' ⊢ φ"
using ** by metis
qed
moreover have "∀P Q. ?bisim P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ ?bisim P' Q'))"
proof (clarify)
fix P Q R α 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
with trans obtain pR' where 5: "R ⇒⟨p ∙ α⟩ pR'" and 6: "(p ∙ P') ≈⋅ pR'"
using PR 1 by (metis bn_eqvt weakly_bisimilar_is_weak_bisimulation is_weak_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 weakly_bisimilar_weak_simulation_step)
from 7 have "Q ⇒⟨α⟩ (-p ∙ pQ')"
using 4 by (metis permute_minus_cancel(2) supp_perm_eq weak_transition_eqvt)
moreover from 6 and 8 have "?bisim P' (-p ∙ pQ')"
by (metis (no_types, opaque_lifting) weakly_bisimilar_eqvt permute_minus_cancel(2) relcompp.simps)
ultimately show "∃Q'. Q ⇒⟨α⟩ Q' ∧ ?bisim P' Q'"
by metis
qed
ultimately have "is_weak_bisimulation ?bisim"
unfolding is_weak_bisimulation_def by metis
moreover have "?bisim P R"
using PQ QR by blast
ultimately show "P ≈⋅ R"
unfolding weakly_bisimilar_def by meson
qed

lemma weakly_bisimilar_equivp: "equivp weakly_bisimilar"
by (metis weakly_bisimilar_reflp weakly_bisimilar_symp weakly_bisimilar_transp equivp_reflp_symp_transp)

end

end
```