Theory S_Transform

theory S_Transform
imports
Bisimilarity_Implies_Equivalence
Equivalence_Implies_Bisimilarity
Weak_Bisimilarity_Implies_Equivalence
Weak_Equivalence_Implies_Bisimilarity
Weak_Expressive_Completeness
begin

section ‹\texorpdfstring{$S$}{S}-Transform: State Predicates as Actions›

subsection ‹Actions and binding names›

datatype ('act,'pred) S_action =
Act 'act
| Pred 'pred

instantiation S_action :: (pt,pt) pt
begin

fun permute_S_action :: "perm ⇒ ('a,'b) S_action ⇒ ('a,'b) S_action" where
"p ∙ (Act α) = Act (p ∙ α)"
| "p ∙ (Pred φ) = Pred (p ∙ φ)"

instance
proof
fix x :: "('a,'b) S_action"
show "0 ∙ x = x" by (cases x, simp_all)
next
fix p q and x :: "('a,'b) S_action"
show "(p + q) ∙ x = p ∙ q ∙ x" by (cases x, simp_all)
qed

end

declare permute_S_action.simps [eqvt]

lemma supp_Act [simp]: "supp (Act α) = supp α"
unfolding supp_def by simp

lemma supp_Pred [simp]: "supp (Pred φ) = supp φ"
unfolding supp_def by simp

instantiation S_action :: (fs,fs) fs
begin

instance
proof
fix x :: "('a,'b) S_action"
show "finite (supp x)"
by (cases x) (simp add: finite_supp)+
qed

end

instantiation S_action :: (bn,fs) bn
begin

fun bn_S_action :: "('a,'b) S_action ⇒ atom set" where
"bn_S_action (Act α) = bn α"
| "bn_S_action (Pred _) = {}"

instance
proof
fix p and α :: "('a,'b) S_action"
show "p ∙ bn α = bn (p ∙ α)"
by (cases α) (simp add: bn_eqvt, simp)
next
fix α :: "('a,'b) S_action"
show "finite (bn α)"
by (cases α) (simp add: bn_finite, simp)
qed

end

subsection ‹Satisfaction›

context nominal_ts
begin

text ‹Here our formalization differs from the informal presentation, where the $S$-transform does
not have any predicates. In Isabelle/HOL, there are no empty types; we use type @{typ unit}
instead. However, it is clear from the following definition of the satisfaction relation that the
single element of this type is not actually used in any meaningful way.›

definition S_satisfies :: "'state ⇒ unit ⇒ bool" (infix "⊢⇩S" 70) where
"P ⊢⇩S φ ⟷ False"

lemma S_satisfies_eqvt: assumes "P ⊢⇩S φ" shows "(p ∙ P) ⊢⇩S (p ∙ φ)"
using assms by (simp add: S_satisfies_def)

end

subsection ‹Transitions›

context nominal_ts
begin

inductive S_transition :: "'state ⇒ (('act,'pred) S_action, 'state) residual ⇒ bool" (infix "→⇩S" 70) where
Act: "P → ⟨α,P'⟩ ⟹ P →⇩S ⟨Act α,P'⟩"
| Pred: "P ⊢ φ ⟹ P →⇩S ⟨Pred φ,P⟩"

lemma S_transition_eqvt: assumes "P →⇩S α⇩SP'" shows "(p ∙ P) →⇩S (p ∙ α⇩SP')"
using assms by cases (simp add: S_transition.Act transition_eqvt', simp add: S_transition.Pred satisfies_eqvt)

text ‹If there is an $S$-transition, there is an ordinary transition with the same residual---it
is not necessary to consider alpha-variants.›

lemma S_transition_cases [case_names Act Pred, consumes 1]: assumes "P →⇩S ⟨α⇩S,P'⟩"
and "⋀α. α⇩S = Act α ⟹ P → ⟨α,P'⟩ ⟹ R"
and "⋀φ. α⇩S = Pred φ ⟹ P' = P ⟹ P ⊢ φ ⟹ R"
shows R
using assms proof (cases rule: S_transition.cases)
case (Act α' P'')
let ?Act = "Act :: 'act ⇒ ('act,'pred) S_action"
from ‹⟨α⇩S,P'⟩ = ⟨Act α',P''⟩› obtain α where "α⇩S = Act α"
by (meson bn_S_action.elims residual_empty_bn_eq_iff)
with ‹⟨α⇩S,P'⟩ = ⟨Act α',P''⟩› obtain p where "supp (?Act α, P') - bn (?Act α) = supp (?Act α', P'') - bn (?Act α')"
and "(supp (?Act α, P') - bn (?Act α)) ♯* p" and "p ∙ (?Act α, P') = (?Act α', P'')" and "p ∙ bn (?Act α) = bn (?Act α')"
then have "supp (α, P') - bn α = supp (α', P'') - bn α'" and "(supp (α, P') - bn α) ♯* p"
and "p ∙ (α, P') = (α', P'')" and "p ∙ bn α = bn α'"
then have "⟨α,P'⟩ = ⟨α',P''⟩"
by (metis residual_eq_iff_perm)
with ‹α⇩S = Act α› and ‹P → ⟨α',P''⟩› show R
using ‹⋀α. α⇩S = Act α ⟹ P → ⟨α,P'⟩ ⟹ R› by metis
next
case (Pred φ)
from ‹⟨α⇩S,P'⟩ = ⟨Pred φ,P⟩› have "α⇩S = Pred φ" and "P' = P"
by (metis bn_S_action.simps(2) residual_empty_bn_eq_iff)+
with ‹P ⊢ φ› show R
using ‹⋀φ. α⇩S = Pred φ ⟹ P' = P ⟹ P ⊢ φ ⟹ R› by metis
qed

lemma S_transition_Act_iff: "P →⇩S ⟨Act α,P'⟩ ⟷ P → ⟨α,P'⟩"
using S_transition.Act S_transition_cases by fastforce

lemma S_transition_Pred_iff: "P →⇩S ⟨Pred φ,P'⟩ ⟷ P' = P ∧ P ⊢ φ"
using S_transition.Pred S_transition_cases by fastforce

end

subsection ‹Strong Bisimilarity in the \texorpdfstring{$S$}{S}-transform›

context nominal_ts
begin

interpretation S_transform: nominal_ts "(⊢⇩S)" "(→⇩S)"
by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt)

no_notation S_satisfies (infix "⊢⇩S" 70) ― ‹denotes @{const S_transform.S_satisfies} instead›

notation S_transform.bisimilar (infix "∼⋅⇩S" 100)

text ‹Bisimilarity is equivalent to bisimilarity in the $S$-transform.›

lemma bisimilar_is_S_transform_bisimulation: "S_transform.is_bisimulation bisimilar"
unfolding S_transform.is_bisimulation_def
proof
show "symp bisimilar"
by (fact bisimilar_symp)
next
have "∀P Q. P ∼⋅ Q ⟶ (∀φ. P ⊢⇩S φ ⟶ Q ⊢⇩S φ)" (is ?S)
moreover have "∀P Q. P ∼⋅ Q ⟶ (∀α⇩S P'. bn α⇩S ♯* Q ⟶ P →⇩S ⟨α⇩S,P'⟩ ⟶ (∃Q'. Q →⇩S ⟨α⇩S,Q'⟩ ∧ P' ∼⋅ Q'))" (is ?T)
proof (clarify)
fix P Q α⇩S P'
assume bisim: "P ∼⋅ Q" and fresh⇩S: "bn α⇩S ♯* Q" and trans⇩S: "P →⇩S ⟨α⇩S,P'⟩"
obtain Q' where "Q →⇩S ⟨α⇩S,Q'⟩" and "P' ∼⋅ Q'"
using trans⇩S proof (cases rule: S_transition_cases)
case (Act α)
from ‹α⇩S = Act α› and fresh⇩S have "bn α ♯* Q"
by simp
with bisim and ‹P → ⟨α,P'⟩› obtain Q' where transQ: "Q → ⟨α,Q'⟩" and bisim': "P' ∼⋅ Q'"
by (metis bisimilar_simulation_step)
from ‹α⇩S = Act α› and transQ have "Q →⇩S ⟨α⇩S,Q'⟩"
with bisim' show "thesis"
using ‹⋀Q'. Q →⇩S ⟨α⇩S,Q'⟩ ⟹ P' ∼⋅ Q' ⟹ thesis› by blast
next
case (Pred φ)
from bisim and ‹P ⊢ φ› have "Q ⊢ φ"
by (metis is_bisimulation_def bisimilar_is_bisimulation)
with ‹α⇩S = Pred φ› have "Q →⇩S ⟨α⇩S,Q⟩"
with bisim and ‹P' = P› show "thesis"
using ‹⋀Q'. Q →⇩S ⟨α⇩S,Q'⟩ ⟹ P' ∼⋅ Q' ⟹ thesis› by blast
qed
then show "∃Q'. Q →⇩S ⟨α⇩S,Q'⟩ ∧ P' ∼⋅ Q'"
by auto
qed
ultimately show "?S ∧ ?T"
by metis
qed

lemma S_transform_bisimilar_is_bisimulation: "is_bisimulation S_transform.bisimilar"
unfolding is_bisimulation_def
proof
show "symp S_transform.bisimilar"
by (fact S_transform.bisimilar_symp)
next
have "∀P Q. P ∼⋅⇩S Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" (is ?S)
proof (clarify)
fix P Q φ
assume bisim: "P ∼⋅⇩S Q" and valid: "P ⊢ φ"
from valid have "P →⇩S ⟨Pred φ,P⟩"
by (fact S_transition.Pred)
moreover have "bn (Pred φ) ♯* Q"
ultimately obtain Q' where trans': "Q →⇩S ⟨Pred φ,Q'⟩"
using bisim by (metis S_transform.bisimilar_simulation_step)
from trans' show "Q ⊢ φ"
using S_transition_Pred_iff by blast
qed
moreover have "∀P Q. P ∼⋅⇩S Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅⇩S Q'))" (is ?T)
proof (clarify)
fix P Q α P'
assume bisim: "P ∼⋅⇩S Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
from trans have "P →⇩S ⟨Act α,P'⟩"
by (fact S_transition.Act)
with bisim and fresh obtain Q' where trans': "Q →⇩S ⟨Act α,Q'⟩" and bisim': "P' ∼⋅⇩S Q'"
by (metis S_transform.bisimilar_simulation_step bn_S_action.simps(1))
from trans' have "Q → ⟨α,Q'⟩"
by (metis S_transition_Act_iff)
with bisim' show "∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅⇩S Q'"
by metis
qed
ultimately show "?S ∧ ?T"
by metis
qed

theorem S_transform_bisimilar_iff: "P ∼⋅⇩S Q ⟷ P ∼⋅ Q"
proof
assume "P ∼⋅⇩S Q"
then show "P ∼⋅ Q"
by (metis S_transform_bisimilar_is_bisimulation bisimilar_def)
next
assume "P ∼⋅ Q"
then show "P ∼⋅⇩S Q"
by (metis S_transform.bisimilar_def bisimilar_is_S_transform_bisimulation)
qed

end

subsection ‹Weak Bisimilarity in the \texorpdfstring{$S$}{S}-transform›

context weak_nominal_ts
begin

lemma weakly_bisimilar_tau_transition_weakly_bisimilar:
assumes "P ≈⋅ R" and "P ⇒ Q" and "Q ⇒ R"
shows "Q ≈⋅ R"
proof -
let ?bisim = "λS T. S ≈⋅ T ∨ {S,T} = {Q,R}"
have "is_weak_bisimulation ?bisim"
unfolding is_weak_bisimulation_def
proof
show "symp ?bisim"
using weakly_bisimilar_symp by (simp add: insert_commute symp_def)
next
have "∀S T φ. ?bisim S T ∧ S ⊢ φ ⟶ (∃T'. T ⇒ T' ∧ ?bisim S T' ∧ T' ⊢ φ)" (is ?S)
proof (clarify)
fix S T φ
assume bisim: "?bisim S T" and valid: "S ⊢ φ"
from bisim show "∃T'. T ⇒ T' ∧ ?bisim S T' ∧ T' ⊢ φ"
proof
assume "S ≈⋅ T"
with valid show ?thesis
by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
next
assume "{S, T} = {Q, R}"
then have "S = Q ∧ T = R ∨ T = Q ∧ S = R"
by (metis doubleton_eq_iff)
then show ?thesis
proof
assume "S = Q ∧ T = R"
with ‹P ⇒ Q› and ‹P ≈⋅ R› and valid show ?thesis
by (metis is_weak_bisimulation_def tau_transition_trans weakly_bisimilar_is_weak_bisimulation weakly_bisimilar_tau_simulation_step)
next
assume "T = Q ∧ S = R"
with ‹Q ⇒ R› and valid show ?thesis
by (meson reflpE weakly_bisimilar_reflp)
qed
qed
qed
moreover have "∀S T. ?bisim S T ⟶ (∀α S'. bn α ♯* T ⟶ S → ⟨α,S'⟩ ⟶ (∃T'. T ⇒⟨α⟩ T' ∧ ?bisim S' T'))" (is ?T)
proof (clarify)
fix S T α S'
assume bisim: "?bisim S T" and fresh: "bn α ♯* T" and trans: "S → ⟨α,S'⟩"
from bisim show "∃T'. T ⇒⟨α⟩ T' ∧ ?bisim S' T'"
proof
assume "S ≈⋅ T"
with fresh and trans show ?thesis
by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
next
assume "{S, T} = {Q, R}"
then have "S = Q ∧ T = R ∨ T = Q ∧ S = R"
by (metis doubleton_eq_iff)
then show ?thesis
proof
assume "S = Q ∧ T = R"
with ‹P ⇒ Q› and ‹P ≈⋅ R› and fresh and trans show ?thesis
using observable_transition_stepI tau_refl weak_transition_stepI weak_transition_weakI weakly_bisimilar_weak_simulation_step by blast
next
assume "T = Q ∧ S = R"
with ‹Q ⇒ R› and trans show ?thesis
by (metis observable_transition_stepI reflpE tau_refl weak_transition_stepI weak_transition_weakI weakly_bisimilar_reflp)
qed
qed
qed
ultimately show "?S ∧ ?T"
by metis
qed
then show ?thesis
using weakly_bisimilar_def by blast
qed

notation S_satisfies (infix "⊢⇩S" 70)

interpretation S_transform: weak_nominal_ts "(⊢⇩S)" "(→⇩S)" "Act τ"
by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, simp add: tau_eqvt)

no_notation S_satisfies (infix "⊢⇩S" 70) ― ‹denotes @{const S_transform.S_satisfies} instead›

notation S_transform.tau_transition (infix "⇒⇩S" 70)
notation S_transform.observable_transition ("_/ ⇒{_}⇩S/ _" [70, 70, 71] 71)
notation S_transform.weak_transition ("_/ ⇒⟨_⟩⇩S/ _" [70, 70, 71] 71)
notation S_transform.weakly_bisimilar (infix "≈⋅⇩S" 100)

lemma S_transform_tau_transition_iff: "P ⇒⇩S P' ⟷ P ⇒ P'"
proof
assume "P ⇒⇩S P'"
then show "P ⇒ P'"
by induct (simp, metis S_transition_Act_iff tau_step)
next
assume "P ⇒ P'"
then show "P ⇒⇩S P'"
by induct (simp, metis S_transform.tau_transition.simps S_transition.Act)
qed

lemma S_transform_observable_transition_iff: "P ⇒{Act α}⇩S P' ⟷ P ⇒{α} P'"
unfolding S_transform.observable_transition_def observable_transition_def
by (metis S_transform_tau_transition_iff S_transition_Act_iff)

lemma S_transform_weak_transition_iff: "P ⇒⟨Act α⟩⇩S P' ⟷ P ⇒⟨α⟩ P'"
by (simp add: S_transform_observable_transition_iff S_transform_tau_transition_iff weak_transition_def)

text ‹Weak bisimilarity is equivalent to weak bisimilarity in the $S$-transform.›

lemma weakly_bisimilar_is_S_transform_weak_bisimulation: "S_transform.is_weak_bisimulation weakly_bisimilar"
unfolding S_transform.is_weak_bisimulation_def
proof
show "symp weakly_bisimilar"
by (fact weakly_bisimilar_symp)
next
have "∀P Q φ. P ≈⋅ Q ∧ P ⊢⇩S φ ⟶ (∃Q'. Q ⇒⇩S Q' ∧ P ≈⋅ Q' ∧ Q' ⊢⇩S φ)" (is ?S)
moreover have "∀P Q. P ≈⋅ Q ⟶ (∀α⇩S P'. bn α⇩S ♯* Q ⟶ P →⇩S ⟨α⇩S,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⇩S⟩⇩S Q' ∧ P' ≈⋅ Q'))" (is ?T)
proof (clarify)
fix P Q α⇩S P'
assume bisim: "P ≈⋅ Q" and fresh⇩S: "bn α⇩S ♯* Q" and trans⇩S: "P →⇩S ⟨α⇩S,P'⟩"
obtain Q' where "Q ⇒⟨α⇩S⟩⇩S Q'" and "P' ≈⋅ Q'"
using trans⇩S proof (cases rule: S_transition_cases)
case (Act α)
from ‹α⇩S = Act α› and fresh⇩S have "bn α ♯* Q"
by simp
with bisim and ‹P → ⟨α,P'⟩› obtain Q' where transQ: "Q ⇒⟨α⟩ Q'" and bisim': "P' ≈⋅ Q'"
by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
from ‹α⇩S = Act α› and transQ have "Q ⇒⟨α⇩S⟩⇩S Q'"
by (metis S_transform_weak_transition_iff)
with bisim' show "thesis"
using ‹⋀Q'. Q ⇒⟨α⇩S⟩⇩S Q' ⟹ P' ≈⋅ Q' ⟹ thesis› by blast
next
case (Pred φ)
from bisim and ‹P ⊢ φ› obtain Q' where "Q ⇒ Q'" and "P ≈⋅ Q'" and "Q' ⊢ φ"
by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)
from ‹Q ⇒ Q'› have "Q ⇒⇩S Q'"
by (metis S_transform_tau_transition_iff)
moreover from ‹Q' ⊢ φ› have "Q' →⇩S ⟨Pred φ,Q'⟩"
ultimately have "Q ⇒⟨α⇩S⟩⇩S Q'"
using ‹α⇩S = Pred φ› by (metis S_transform.observable_transitionI S_transform.tau_refl S_transform.weak_transition_stepI)
with ‹P' = P› and ‹P ≈⋅ Q'› show "thesis"
using ‹⋀Q'. Q ⇒⟨α⇩S⟩⇩S Q' ⟹ P' ≈⋅ Q' ⟹ thesis› by blast
qed
then show "∃Q'. Q ⇒⟨α⇩S⟩⇩S Q' ∧ P' ≈⋅ Q'"
by auto
qed
ultimately show "?S ∧ ?T"
by metis
qed

lemma S_transform_weakly_bisimilar_is_weak_bisimulation: "is_weak_bisimulation S_transform.weakly_bisimilar"
unfolding is_weak_bisimulation_def
proof
show "symp S_transform.weakly_bisimilar"
by (fact S_transform.weakly_bisimilar_symp)
next
have "∀P Q φ. P ≈⋅⇩S Q ∧ P ⊢ φ ⟶ (∃Q'. Q ⇒ Q' ∧ P ≈⋅⇩S Q' ∧ Q' ⊢ φ)" (is ?S)
proof (clarify)
fix P Q φ
assume bisim: "P ≈⋅⇩S Q" and valid: "P ⊢ φ"
from valid have "P ⇒⟨Pred φ⟩⇩S P"
moreover have "bn (Pred φ) ♯* Q"
ultimately obtain Q'' where trans': "Q ⇒⟨Pred φ⟩⇩S Q''" and bisim': "P ≈⋅⇩S Q''"
using bisim by (metis S_transform.weakly_bisimilar_weak_simulation_step)

from trans' obtain Q' Q⇩1 where trans⇩1: "Q ⇒⇩S Q'" and trans⇩2: "Q' →⇩S ⟨Pred φ, Q⇩1⟩" and trans⇩3: "Q⇩1 ⇒⇩S Q''"
from trans⇩2 have eq: "Q⇩1 = Q'" and "Q' ⊢ φ"
using S_transition_Pred_iff by blast+
moreover from trans⇩1 and trans⇩3 and eq and bisim and bisim' have "P ≈⋅⇩S Q'"
by (metis S_transform.weakly_bisimilar_equivp S_transform.weakly_bisimilar_tau_transition_weakly_bisimilar equivp_def)
moreover from trans⇩1 have "Q ⇒ Q'"
by (metis S_transform_tau_transition_iff)
ultimately show "∃Q'. Q ⇒ Q' ∧ P ≈⋅⇩S Q' ∧ Q' ⊢ φ"
by metis
qed
moreover have "∀P Q. P ≈⋅⇩S Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅⇩S Q'))" (is ?T)
proof (clarify)
fix P Q α P'
assume bisim: "P ≈⋅⇩S Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩"
from trans have "P →⇩S ⟨Act α,P'⟩"
by (fact S_transition.Act)
with bisim and fresh obtain Q' where trans': "Q ⇒⟨Act α⟩⇩S Q'" and bisim': "P' ≈⋅⇩S Q'"
by (metis S_transform.is_weak_bisimulation_def S_transform.weakly_bisimilar_is_weak_bisimulation bn_S_action.simps(1))
from trans' have "Q ⇒⟨α⟩ Q'"
by (metis S_transform_weak_transition_iff)
with bisim' show "∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≈⋅⇩S Q'"
by metis
qed
ultimately show "?S ∧ ?T"
by metis
qed

theorem S_transform_weakly_bisimilar_iff: "P ≈⋅⇩S Q ⟷ P ≈⋅ Q"
proof
assume "P ≈⋅⇩S Q"
then show "P ≈⋅ Q"
by (metis S_transform_weakly_bisimilar_is_weak_bisimulation weakly_bisimilar_def)
next
assume "P ≈⋅ Q"
then show "P ≈⋅⇩S Q"
by (metis S_transform.weakly_bisimilar_def weakly_bisimilar_is_S_transform_weak_bisimulation)
qed

end

subsection ‹Translation of (strong) formulas into formulas without predicates›

text ‹Since we defined formulas via a manual quotient construction, we also need to define the
$S$-transform via lifting from the underlying type of infinitely branching trees. As before, we
cannot use {\bf nominal\_function} because that generates proof obligations where, for formulas
of the form~@{term "Conj xset"}, the assumption that~@{term xset} has finite support is missing.›

text ‹The following auxiliary function returns trees (modulo $\alpha$-equivalence) rather than
formulas. This allows us to prove equivariance for \emph{all} argument trees, without an assumption
that they are (hereditarily) finitely supported. Further below--after this auxiliary function has
been lifted to (strong) formulas as arguments--we derive a version that returns formulas.›

primrec S_transform_Tree :: "('idx,'pred::fs,'act::bn) Tree ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" where
"S_transform_Tree (tConj tset) = Conj⇩α (map_bset S_transform_Tree tset)"
| "S_transform_Tree (tNot t) = Not⇩α (S_transform_Tree t)"
| "S_transform_Tree (tPred φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
| "S_transform_Tree (tAct α t) = Act⇩α (S_action.Act α) (S_transform_Tree t)"

lemma S_transform_Tree_eqvt [eqvt]: "p ∙ S_transform_Tree t = S_transform_Tree (p ∙ t)"
proof (induct t)
case (tConj tset)
then show ?case
by simp (metis (no_types, opaque_lifting) bset.map_cong0 map_bset_eqvt permute_fun_def permute_minus_cancel(1))
qed simp_all

text ‹@{const S_transform_Tree} respects $\alpha$-equivalence.›

lemma alpha_Tree_S_transform_Tree:
assumes "t1 =⇩α t2"
shows "S_transform_Tree t1 = S_transform_Tree t2"
using assms proof (induction t1 t2 rule: alpha_Tree_induct')
case (alpha_tConj tset1 tset2)
then have "rel_bset (=) (map_bset S_transform_Tree tset1) (map_bset S_transform_Tree tset2)"
by (simp add: bset.rel_map(1) bset.rel_map(2) bset.rel_mono_strong)
then show ?case
next
case (alpha_tAct α1 t1 α2 t2)
from ‹tAct α1 t1 =⇩α tAct α2 t2›
obtain p where *: "(bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2)"
and **: "(bn α1, α1) ≈set (=) supp p (bn α2, α2)"
by auto
from * have fresh: "(supp_rel alpha_Tree t1 - bn α1) ♯* p" and alpha: "p ∙ t1 =⇩α t2" and eq: "p ∙ bn α1 = bn α2"
from alpha_tAct.IH(2) have "supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) ⊆ supp_rel alpha_Tree t1"
by (metis (no_types, lifting) infinite_mono alpha_Tree_permute_rep_commute S_transform_Tree_eqvt mem_Collect_eq subsetI supp_rel_def)
with fresh have fresh': "(supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) - bn α1) ♯* p"
by (meson DiffD1 DiffD2 DiffI fresh_star_def subsetCE)
moreover from alpha have alpha': "p ∙ rep_Tree⇩α (S_transform_Tree t1) =⇩α rep_Tree⇩α (S_transform_Tree t2)"
using alpha_tAct.IH(1) by (metis alpha_Tree_permute_rep_commute S_transform_Tree_eqvt)
moreover from fresh' alpha' eq have "supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t1)) - bn α1 = supp_rel alpha_Tree (rep_Tree⇩α (S_transform_Tree t2)) - bn α2"
by (metis (mono_tags) Diff_eqvt alpha_Tree_eqvt' alpha_Tree_eqvt_aux alpha_Tree_supp_rel atom_set_perm_eq)
ultimately have "(bn α1, rep_Tree⇩α (S_transform_Tree t1)) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, rep_Tree⇩α (S_transform_Tree t2))"
using eq by (simp add: alpha_set)
moreover from ** have "(bn α1, S_action.Act α1) ≈set (=) supp p (bn α2, S_action.Act α2)"
by (metis (mono_tags, lifting) S_Transform.supp_Act alpha_set permute_S_action.simps(1))
ultimately have "Act⇩α (S_action.Act α1) (S_transform_Tree t1) = Act⇩α (S_action.Act α2) (S_transform_Tree t2)"
then show ?case
by simp
qed simp_all

text ‹$S$-transform for trees modulo $\alpha$-equivalence.›

lift_definition S_transform_Tree⇩α :: "('idx,'pred::fs,'act::bn) Tree⇩α ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" is
S_transform_Tree
by (fact alpha_Tree_S_transform_Tree)

lemma S_transform_Tree⇩α_eqvt [eqvt]: "p ∙ S_transform_Tree⇩α t⇩α = S_transform_Tree⇩α (p ∙ t⇩α)"
by transfer (simp)

lemma S_transform_Tree⇩α_Conj⇩α [simp]: "S_transform_Tree⇩α (Conj⇩α tset⇩α) = Conj⇩α (map_bset S_transform_Tree⇩α tset⇩α)"
by (simp add: Conj⇩α_def' S_transform_Tree⇩α.abs_eq) (metis (no_types, lifting) S_transform_Tree⇩α.rep_eq bset.map_comp bset.map_cong0 comp_apply)

lemma S_transform_Tree⇩α_Not⇩α [simp]: "S_transform_Tree⇩α (Not⇩α t⇩α) = Not⇩α (S_transform_Tree⇩α t⇩α)"
by transfer simp

lemma S_transform_Tree⇩α_Pred⇩α [simp]: "S_transform_Tree⇩α (Pred⇩α φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
by transfer simp

lemma S_transform_Tree⇩α_Act⇩α [simp]: "S_transform_Tree⇩α (Act⇩α α t⇩α) = Act⇩α (S_action.Act α) (S_transform_Tree⇩α t⇩α)"
by transfer simp

lemma finite_supp_map_bset_S_transform_Tree⇩α [simp]:
assumes "finite (supp tset⇩α)"
shows "finite (supp (map_bset S_transform_Tree⇩α tset⇩α))"
proof -
have "eqvt map_bset" and "eqvt S_transform_Tree⇩α"
then have "supp (map_bset S_transform_Tree⇩α) = {}"
using supp_fun_eqvt supp_fun_app_eqvt by blast
then have "supp (map_bset S_transform_Tree⇩α tset⇩α) ⊆ supp tset⇩α"
using supp_fun_app by blast
with assms show "finite (supp (map_bset S_transform_Tree⇩α tset⇩α))"
by (metis finite_subset)
qed

lemma S_transform_Tree⇩α_preserves_hereditarily_fs:
assumes "hereditarily_fs t⇩α"
shows "hereditarily_fs (S_transform_Tree⇩α t⇩α)"
using assms proof (induct rule: hereditarily_fs.induct)
case (Conj⇩α tset⇩α)
then show ?case
by (auto intro!: hereditarily_fs.Conj⇩α) (metis imageE map_bset.rep_eq)
next
case (Not⇩α t⇩α)
then show ?case
next
case (Pred⇩α φ)
have "finite (supp bempty)"
then show ?case
using hereditarily_fs.Act⇩α finite_supp_implies_hereditarily_fs_Conj⇩α by fastforce
next
case (Act⇩α t⇩α α)
then show ?case
qed

text ‹$S$-transform for (strong) formulas.›

lift_definition S_transform_formula :: "('idx,'pred::fs,'act::bn) formula ⇒ ('idx, unit, ('act,'pred) S_action) Tree⇩α" is
S_transform_Tree⇩α
.

lemma S_transform_formula_eqvt [eqvt]: "p ∙ S_transform_formula x = S_transform_formula (p ∙ x)"
by transfer (simp)

lemma S_transform_formula_Conj [simp]:
assumes "finite (supp xset)"
shows "S_transform_formula (Conj xset) = Conj⇩α (map_bset S_transform_formula xset)"
using assms by (simp add: Conj_def S_transform_formula_def bset.map_comp map_fun_def)

lemma S_transform_formula_Not [simp]: "S_transform_formula (Not x) = Not⇩α (S_transform_formula x)"
by transfer simp

lemma S_transform_formula_Pred [simp]: "S_transform_formula (Formula.Pred φ) = Act⇩α (S_action.Pred φ) (Conj⇩α bempty)"
by transfer simp

lemma S_transform_formula_Act [simp]: "S_transform_formula (Formula.Act α x) = Formula.Act⇩α (S_action.Act α) (S_transform_formula x)"
by transfer simp

lemma S_transform_formula_hereditarily_fs [simp]: "hereditarily_fs (S_transform_formula x)"
by transfer (fact S_transform_Tree⇩α_preserves_hereditarily_fs)

text ‹Finally, we define the proper $S$-transform, which returns formulas instead of trees.›

definition S_transform :: "('idx,'pred::fs,'act::bn) formula ⇒ ('idx, unit, ('act,'pred) S_action) formula" where
"S_transform x = Abs_formula (S_transform_formula x)"

lemma S_transform_eqvt [eqvt]: "p ∙ S_transform x = S_transform (p ∙ x)"
unfolding S_transform_def by simp

lemma finite_supp_map_bset_S_transform [simp]:
assumes "finite (supp xset)"
shows "finite (supp (map_bset S_transform xset))"
proof -
have "eqvt map_bset" and "eqvt S_transform"
then have "supp (map_bset S_transform) = {}"
using supp_fun_eqvt supp_fun_app_eqvt by blast
then have "supp (map_bset S_transform xset) ⊆ supp xset"
using supp_fun_app by blast
with assms show "finite (supp (map_bset S_transform xset))"
by (metis finite_subset)
qed

lemma S_transform_Conj [simp]:
assumes "finite (supp xset)"
shows "S_transform (Conj xset) = Conj (map_bset S_transform xset)"
using assms unfolding S_transform_def by (simp, simp add: Conj_def bset.map_comp o_def)

lemma S_transform_Not [simp]: "S_transform (Not x) = Not (S_transform x)"
unfolding S_transform_def by (simp add: Not.abs_eq eq_onp_same_args)

lemma S_transform_Pred [simp]: "S_transform (Formula.Pred φ) = Formula.Act (S_action.Pred φ) (Conj bempty)"
unfolding S_transform_def by (simp add: Formula.Act_def Conj_rep_eq eqvtI supp_fun_eqvt)

lemma S_transform_Act [simp]: "S_transform (Formula.Act α x) = Formula.Act (S_action.Act α) (S_transform x)"
unfolding S_transform_def by (simp, simp add: Formula.Act_def)

context nominal_ts
begin

lemma valid_Conj_bempty [simp]: "P ⊨ Conj bempty"
by (simp add: bempty.rep_eq eqvtI supp_fun_eqvt)

notation S_satisfies (infix "⊢⇩S" 70)

interpretation S_transform: nominal_ts "(⊢⇩S)" "(→⇩S)"
by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt)

notation S_transform.valid (infix "⊨⇩S" 70)

text ‹The $S$-transform preserves satisfaction of formulas in the following sense:›

theorem valid_iff_valid_S_transform: shows "P ⊨ x ⟷ P ⊨⇩S S_transform x"
proof (induct x arbitrary: P)
case (Conj xset)
then show ?case
by auto (metis imageE map_bset.rep_eq, simp add: map_bset.rep_eq)
next
case (Not x)
then show ?case by simp
next
case (Pred φ)
let ?φ = "Formula.Pred φ :: ('idx, 'pred, ('act,'pred) S_action) formula"
have "bn (S_action.Pred φ :: ('act,'pred) S_action) ♯* P"
then show ?case
by (auto simp add: S_transform.valid_Act_fresh S_transition_Pred_iff)
next
case (Act α x)
show ?case
proof
assume "P ⊨ Formula.Act α x"
then obtain α' x' P' where eq: "Formula.Act α x = Formula.Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'"
by (metis valid_Act)
from eq obtain p where p_x: "p ∙ x = x'" and p_α: "p ∙ α = α'"
by (metis Act_eq_iff_perm)

from valid have "-p ∙ P' ⊨ x"
using p_x by (metis valid_eqvt permute_minus_cancel(2))
then have "-p ∙ P' ⊨⇩S S_transform x"
using Act.hyps(1) by metis
then have "P' ⊨⇩S S_transform x'"
by (metis (no_types, lifting) p_x S_transform.valid_eqvt S_transform_eqvt permute_minus_cancel(1))

with eq and trans show "P ⊨⇩S S_transform (Formula.Act α x)"
using S_transform.valid_Act S_transition.Act by fastforce
next
assume *: "P ⊨⇩S S_transform (Formula.Act α x)"

― ‹rename~@{term "bn α"} to avoid~@{term "P"}, without touching~@{term "Formula.Act α x"}›
obtain p where 1: "(p ∙ bn α) ♯* P" and 2: "supp (Formula.Act α x) ♯* p"
proof (rule at_set_avoiding2[of "bn α" "P" "Formula.Act α x", THEN exE])
show "finite (bn α)" by (fact bn_finite)
next
show "finite (supp P)" by (fact finite_supp)
next
show "finite (supp (Formula.Act α x))" by (fact finite_supp)
next
show "bn α ♯* Formula.Act α x" by simp
qed metis
from 2 have eq: "Formula.Act α x = Formula.Act (p ∙ α) (p ∙ x)"
using supp_perm_eq by fastforce

with * have "P ⊨⇩S Formula.Act (S_action.Act (p ∙ α)) (S_transform (p ∙ x))"
by simp
with 1 obtain P' where trans: "P →⇩S ⟨S_action.Act (p ∙ α),P'⟩" and valid: "P' ⊨⇩S S_transform (p ∙ x)"
by (metis S_transform.valid_Act_fresh bn_S_action.simps(1) bn_eqvt)

from valid have "-p ∙ P' ⊨⇩S S_transform x"
by (metis (no_types, opaque_lifting) S_transform.valid_eqvt S_transform_eqvt permute_minus_cancel(1))
then have "-p ∙ P' ⊨ x"
using Act.hyps(1) by metis
then have "P' ⊨ p ∙ x"
by (metis permute_minus_cancel(1) valid_eqvt)

moreover from trans have "P → ⟨p ∙ α,P'⟩"
using S_transition_Act_iff by blast

ultimately show "P ⊨ Formula.Act α x"
using eq valid_Act by blast
qed
qed

end

context indexed_nominal_ts
begin

text ‹The following (alternative) proof of the $\rightarrow$'' direction of theorem
@{thm S_transform_bisimilar_iff}, namely that bisimilarity in the $S$-transform implies
bisimilarity in the original transition system, uses the fact that the $S$-transform(ation)
preserves satisfaction of formulas, together with the fact that bisimilarity (in the
$S$-transform) implies logical equivalence, and equivalence (in the original transition system)
implies bisimilarity. However, since we proved the latter in the context of indexed nominal
transition systems, this proof requires an indexed nominal transition system.›

interpretation S_transform: indexed_nominal_ts "(⊢⇩S)" "(→⇩S)"
by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, fact card_idx_perm, fact card_idx_state)

notation S_transform.bisimilar (infix "∼⋅⇩S" 100)

theorem "P ∼⋅⇩S Q ⟶ P ∼⋅ Q"
proof
assume "P ∼⋅⇩S Q"
then have "S_transform.logically_equivalent P Q"
by (fact S_transform.bisimilarity_implies_equivalence)
with valid_iff_valid_S_transform have "logically_equivalent P Q"
using logically_equivalent_def S_transform.logically_equivalent_def by blast
then show "P ∼⋅ Q"
by (fact equivalence_implies_bisimilarity)
qed

end

subsection ‹Translation of weak formulas into formulas without predicates›

context indexed_weak_nominal_ts
begin

notation S_satisfies (infix "⊢⇩S" 70)

interpretation S_transform: indexed_weak_nominal_ts "S_action.Act τ" "(⊢⇩S)" "(→⇩S)"
by unfold_locales (fact S_satisfies_eqvt, fact S_transition_eqvt, simp add: tau_eqvt, fact card_idx_perm, fact card_idx_state, fact card_idx_nat)

notation S_transform.valid (infix "⊨⇩S" 70)
notation S_transform.weakly_bisimilar (infix "≈⋅⇩S" 100)

text ‹The $S$-transform of a weak formula is not necessarily a weak formula. However, the image of
all weak formulas under the $S$-transform is adequate for weak bisimilarity.›

corollary "P ≈⋅⇩S Q ⟷ (∀x. weak_formula x ⟶ P ⊨⇩S S_transform x ⟷ Q ⊨⇩S S_transform x)"
by (meson valid_iff_valid_S_transform weak_bisimilarity_implies_weak_equivalence weak_equivalence_implies_weak_bisimilarity S_transform_weakly_bisimilar_iff weakly_logically_equivalent_def)

text ‹For every weak formula, there is an equivalent weak formula over the $S$-transform.›

corollary
assumes "weak_formula x"
obtains y where "S_transform.weak_formula y" and "∀P. P ⊨ x ⟷ P ⊨⇩S y"
proof -
let ?S = "{P. P ⊨ x}"

― ‹@{term ?S} is finitely supported›
have "supp x supports ?S"
unfolding supports_def proof (clarify)
fix a b
assume a: "a ∉ supp x" and b: "b ∉ supp x"
{
fix P
from a and b have "(a ⇌ b) ∙ x = x"
then have "(a ⇌ b) ∙ P ⊨ x ⟷ P ⊨ x"
by (metis permute_swap_cancel valid_eqvt)
}
note * = this
show "(a ⇌ b) ∙ ?S = ?S"
by auto (metis mem_Collect_eq mem_permute_iff permute_swap_cancel "*", simp add: Collect_eqvt permute_fun_def "*")
qed
then have "finite (supp ?S)"
using finite_supp supports_finite by blast

― ‹@{term ?S} is closed under weak bisimilarity›
moreover {
fix P Q
assume "P ∈ ?S" and "P ≈⋅⇩S Q"
with ‹weak_formula x› have "Q ∈ ?S"
using S_transform_weakly_bisimilar_iff weak_bisimilarity_implies_weak_equivalence weakly_logically_equivalent_def by auto
}

ultimately show ?thesis
using S_transform.weak_expressive_completeness that by (metis (no_types, lifting) mem_Collect_eq)
qed

end

end