# Theory FL_Transition_System

theory FL_Transition_System
imports
Transition_System FS_Set
begin

section ‹Nominal Transition Systems with Effects and \texorpdfstring{$F/L$}{F/L}-Bisimilarity›

subsection ‹Nominal transition systems with effects›

text ‹The paper defines an effect as a finitely supported function from states to states. It then
fixes an equivariant set~@{term ℱ} of effects. In our formalization, we avoid working with such a
(carrier) set, and instead introduce a type of (finitely supported) effects together with an
(equivariant) application operator for effects and states.

Equivariance (of the type of effects) is implicitly guaranteed (by the type of~@{const permute}).

\emph{First} represents the (finitely supported) set of effects that must be observed before
following a transition.›

type_synonym 'eff first = "'eff fs_set"

text ‹\emph{Later} is a function that represents how the set~$F$ (for \emph{first}) changes
depending on the action of a transition and the chosen effect.›

type_synonym ('a,'eff) later = "'a × 'eff first × 'eff ⇒ 'eff first"

locale effect_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 effect_apply :: "'effect::fs ⇒ 'state ⇒ 'state" ("⟨_⟩_" [0,101] 100)
and L :: "('act,'effect) later"
assumes effect_apply_eqvt: "eqvt effect_apply"  (* using [eqvt] here generates an error message *)
and L_eqvt: "eqvt L"  ― ‹@{term L} is assumed to be equivariant.›
(* using [eqvt] here generates an error message *)
begin

lemma effect_apply_eqvt_aux [simp]: "p ∙ effect_apply = effect_apply"
by (metis effect_apply_eqvt eqvt_def)

lemma effect_apply_eqvt' [eqvt]: "p ∙ ⟨f⟩P = ⟨p ∙ f⟩(p ∙ P)"
by simp

lemma L_eqvt_aux [simp]: "p ∙ L = L"
by (metis L_eqvt eqvt_def)

lemma L_eqvt' [eqvt]: "p ∙ L (α, P, f) = L (p ∙ α, p ∙ P, p ∙ f)"
by simp

end

subsection ‹\texorpdfstring{$L$}{L}-bisimulations and \texorpdfstring{$F/L$}{F/L}-bisimilarity›

context effect_nominal_ts
begin

definition is_L_bisimulation:: "('effect first ⇒ 'state ⇒ 'state ⇒ bool) ⇒ bool" where
"is_L_bisimulation R ≡
∀F. symp (R F) ∧
(∀P Q. R F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))) ∧
(∀P Q. R F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ R (L (α,F,f)) P' Q'))))"

definition FL_bisimilar :: "'effect first ⇒ 'state ⇒ 'state ⇒ bool" where
"FL_bisimilar F P Q ≡ ∃R. is_L_bisimulation R ∧ (R F) P Q"

abbreviation FL_bisimilar' ("_ ∼⋅[_] _" [51,0,51] 50) where
"P ∼⋅[F] Q ≡ FL_bisimilar F P Q"

text ‹@{term "FL_bisimilar"} is an equivariant relation, and (for every~@{term F}) an
equivalence.›

lemma is_L_bisimulation_eqvt [eqvt]:
assumes "is_L_bisimulation R" shows "is_L_bisimulation (p ∙ R)"
unfolding is_L_bisimulation_def
proof (clarify)
fix F
have "symp ((p ∙ R) F)" (is ?S)
using assms unfolding is_L_bisimulation_def by (metis eqvt_lambda symp_eqvt)
moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?T)
proof (clarify)
fix P Q f φ
assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩f⇩s F" and satisfies: "⟨f⟩P ⊢ φ"
from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
moreover have "(-p ∙ f) ∈⇩f⇩s (-p ∙ F)"
using effect by simp
moreover have "⟨-p ∙ f⟩(-p ∙ P) ⊢ -p ∙ φ"
using satisfies by (metis effect_apply_eqvt' satisfies_eqvt)
ultimately have "⟨-p ∙ f⟩(-p ∙ Q) ⊢ -p ∙ φ"
using assms unfolding is_L_bisimulation_def by auto
then show "⟨f⟩Q ⊢ φ"
by (metis (full_types) effect_apply_eqvt' permute_minus_cancel(1) satisfies_eqvt)
qed
moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α, F, f)) P' Q')))" (is ?U)
proof (clarify)
fix P Q f α P'
assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩f⇩s F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩"
from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)"
by (simp add: eqvt_lambda permute_bool_def unpermute_def)
moreover have "(-p ∙ f) ∈⇩f⇩s (-p ∙ F)"
using effect by simp
moreover have "bn (-p ∙ α) ♯* (⟨-p ∙ f⟩(-p ∙ Q), -p ∙ F, -p ∙ f)"
using fresh by (metis (full_types) effect_apply_eqvt' bn_eqvt fresh_star_Pair fresh_star_permute_iff)
moreover have "⟨-p ∙ f⟩(-p ∙ P) → ⟨-p ∙ α, -p ∙ P'⟩"
using trans by (metis effect_apply_eqvt' transition_eqvt')
ultimately obtain Q' where T: "⟨-p ∙ f⟩(-p ∙ Q) → ⟨-p ∙ α,Q'⟩" and R: "R (L (-p ∙ α, -p ∙ F, -p ∙ f)) (-p ∙ P') Q'"
using assms unfolding is_L_bisimulation_def by meson
from T have "⟨f⟩Q → ⟨α, p ∙ Q'⟩"
by (metis (no_types, lifting) effect_apply_eqvt' abs_residual_pair_eqvt permute_minus_cancel(1) transition_eqvt)
moreover from R have "(p ∙ R) (p ∙ L (-p ∙ α, -p ∙ F, -p ∙ f)) (p ∙ -p ∙ P') (p ∙ Q')"
by (metis permute_boolI permute_fun_def permute_minus_cancel(2))
then have "(p ∙ R) (L (α,F,f)) P' (p ∙ Q')"
ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α,F,f)) P' Q'"
by metis
qed
ultimately show "?S ∧ ?T ∧ ?U" by simp
qed

lemma FL_bisimilar_eqvt:
assumes "P ∼⋅[F] Q" shows "(p ∙ P) ∼⋅[p ∙ F] (p ∙ Q)"
using assms
by (metis eqvt_apply permute_boolI is_L_bisimulation_eqvt FL_bisimilar_def)

lemma FL_bisimilar_reflp: "reflp (FL_bisimilar F)"
proof (rule reflpI)
fix x
have "is_L_bisimulation (λ_. (=))"
unfolding is_L_bisimulation_def by (simp add: symp_def)
then show "x ∼⋅[F] x"
unfolding FL_bisimilar_def by auto
qed

lemma FL_bisimilar_symp: "symp (FL_bisimilar F)"
proof (rule sympI)
fix P Q
assume "P ∼⋅[F] Q"
then obtain R where *: "is_L_bisimulation R ∧ R F P Q"
unfolding FL_bisimilar_def ..
then have "R F Q P"
unfolding is_L_bisimulation_def by (simp add: symp_def)
with "*" show "Q ∼⋅[F] P"
unfolding FL_bisimilar_def by auto
qed

lemma FL_bisimilar_is_L_bisimulation: "is_L_bisimulation FL_bisimilar"
unfolding is_L_bisimulation_def proof
fix F
have "symp (FL_bisimilar F)" (is ?R)
by (fact FL_bisimilar_symp)
moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?S)
by (auto simp add: is_L_bisimulation_def FL_bisimilar_def)
moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ P' ∼⋅[L (α, F, f)] Q')))" (is ?T)
by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) blast
ultimately show "?R ∧ ?S ∧ ?T"
by metis
qed

lemma FL_bisimilar_simulation_step:
assumes "P ∼⋅[F] Q" and "f ∈⇩f⇩s F" and "bn α ♯* (⟨f⟩Q, F, f)" and "⟨f⟩P → ⟨α,P'⟩"
obtains Q' where "⟨f⟩Q → ⟨α,Q'⟩" and "P' ∼⋅[L (α,F,f)] Q'"
using assms by (metis (poly_guards_query) FL_bisimilar_is_L_bisimulation is_L_bisimulation_def)

lemma FL_bisimilar_transp: "transp (FL_bisimilar F)"
proof (rule transpI)
fix P Q R
assume PQ: "P ∼⋅[F] Q" and QR: "Q ∼⋅[F] R"
let ?FL_bisim = "λF. (FL_bisimilar F) OO (FL_bisimilar F)"
have "⋀F. symp (?FL_bisim F)"
proof (rule sympI)
fix F P R
assume "?FL_bisim F P R"
then obtain Q where "P ∼⋅[F] Q" and "Q ∼⋅[F] R"
by blast
then have "R ∼⋅[F] Q" and "Q ∼⋅[F] P"
by (metis FL_bisimilar_symp sympE)+
then show "?FL_bisim F R P"
by blast
qed
moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶ (∀f. f ∈⇩f⇩s F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))"
using FL_bisimilar_is_L_bisimulation is_L_bisimulation_def by auto
moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶
(∀f. f ∈⇩f⇩s F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶
⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q')))"
proof (clarify)
fix F P R Q f α P'
assume PR: "P ∼⋅[F] R" and RQ: "R ∼⋅[F] Q" and effect: "f ∈⇩f⇩s F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩"
― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term "(⟨f⟩R, F)"}, without touching~@{term "(⟨f⟩Q, F, f)"}›
obtain p where 1: "(p ∙ bn α) ♯* (⟨f⟩R, F, f)" and 2: "supp (⟨α,P'⟩, (⟨f⟩Q, F, f)) ♯* p"
proof (rule at_set_avoiding2[of "bn α" "(⟨f⟩R, F, f)" "(⟨α,P'⟩, (⟨f⟩Q, F, f))", THEN exE])
show "finite (bn α)" by (fact bn_finite)
next
show "finite (supp (⟨f⟩R, F, f))" by (fact finite_supp)
next
show "finite (supp (⟨α,P'⟩, (⟨f⟩Q, F, f)))" by (simp add: finite_supp supp_Pair)
next
show "bn α ♯* (⟨α,P'⟩, (⟨f⟩Q, F, f))"
using bn_abs_residual_fresh fresh fresh_star_Pair by blast
qed metis
from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp (⟨f⟩Q, F, f) ♯* p"
from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩"
using supp_perm_eq by fastforce
then obtain pR' where 5: "⟨f⟩R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅[L (p ∙ α,F,f)] pR'"
using PR effect trans 1 by (metis FL_bisimilar_simulation_step bn_eqvt)
from fresh and 4 have "bn (p ∙ α) ♯* (⟨f⟩Q, F, f)"
by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq)
then obtain pQ' where 7: "⟨f⟩Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅[L (p ∙ α,F,f)] pQ'"
using RQ effect 5 by (metis FL_bisimilar_simulation_step)
from 4 have "supp (⟨f⟩Q) ♯* p"
with 7 have "⟨f⟩Q → ⟨α, -p ∙ pQ'⟩"
by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt')
moreover from 6 and 8 have "?FL_bisim (L (p ∙ α, F, f)) (p ∙ P') pQ'"
by (metis relcompp.relcompI)
then have "?FL_bisim (-p ∙ L (p ∙ α, F, f)) (-p ∙ p ∙ P') (-p ∙ pQ')"
using FL_bisimilar_eqvt by blast
then have "?FL_bisim (L (α, -p ∙ F, -p ∙ f)) P' (-p ∙ pQ')"
then have "?FL_bisim (L (α,F,f)) P' (-p ∙ pQ')"
using 4 by (metis fresh_star_Un permute_minus_cancel(2) supp_Pair supp_perm_eq)
ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q'"
by metis
qed
ultimately have "is_L_bisimulation ?FL_bisim"
unfolding is_L_bisimulation_def by metis
moreover have "?FL_bisim F P R"
using PQ QR by blast
ultimately show "P ∼⋅[F] R"
unfolding FL_bisimilar_def by meson
qed

lemma FL_bisimilar_equivp: "equivp (FL_bisimilar F)"
by (metis FL_bisimilar_reflp FL_bisimilar_symp FL_bisimilar_transp equivp_reflp_symp_transp)

end

end