Theory FL_Bisimilarity_Implies_Equivalence

```theory FL_Bisimilarity_Implies_Equivalence
imports
FL_Logical_Equivalence
begin

section ‹\texorpdfstring{\$F/L\$}{F/L}-Bisimilarity Implies Logical Equivalence›

context indexed_effect_nominal_ts
begin

lemma FL_bisimilarity_implies_equivalence_Act:
assumes "f ∈⇩f⇩s F"
and "bn α ♯* (F, f)"
and "x ∈ 𝒜[L (α, F, f)]"
and "⋀P Q. P ∼⋅[L (α, F, f)] Q ⟹ P ⊨ x ⟷ Q ⊨ x"
and "P ∼⋅[F] Q"
and "P ⊨ Act f α x"
shows "Q ⊨ Act f α x"
proof -
have "finite (supp (⟨f⟩Q, F, f))"
by (fact finite_supp)
with ‹P ⊨ Act f α x› obtain α' x' P' where eq: "Act f α x = Act f α' x'" and trans: "⟨f⟩P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* (⟨f⟩Q, F, f)"
by (metis FL_valid_Act_strong)

from ‹P ∼⋅[F] Q› and ‹f ∈⇩f⇩s F› and fresh and trans obtain Q' where trans': "⟨f⟩Q → ⟨α',Q'⟩" and bisim': "P' ∼⋅[L (α',F,f)] Q'"
by (metis FL_bisimilar_simulation_step)

from eq obtain p where p_α: "α' = p ∙ α" and p_x: "x' = p ∙ x"
and fresh_p: "(supp x - bn α) ♯* p ∧ (supp α - bn α) ♯* p"
and supp_p: "supp p ⊆ bn α ∪ p ∙ bn α"
by (metis Act_eq_iff_perm_renaming)

from valid and p_x have "-p ∙ P' ⊨ x"
by (metis permute_minus_cancel(2) FL_valid_eqvt)

moreover from fresh and p_α have "(p ∙ bn α) ♯* (F, f)"
with ‹bn α ♯* (F, f)› and supp_p have "supp (F, f) ♯* p"
by (meson UnE fresh_def fresh_star_def subsetCE)
then have "supp F ♯* p" and "supp f ♯* p"

with bisim' and p_α have "(-p ∙ P') ∼⋅[L (α, F, f)] (-p ∙ Q')"
by (metis FL_bisimilar_eqvt L_eqvt' permute_minus_cancel(2) supp_perm_eq)

ultimately have "-p ∙ Q' ⊨ x"
using ‹⋀P Q. P ∼⋅[L (α, F, f)] Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis

with p_x have "Q' ⊨ x'"
by (metis permute_minus_cancel(1) FL_valid_eqvt)

with eq and trans' show "Q ⊨ Act f α x"
unfolding FL_valid_Act by metis
qed

theorem FL_bisimilarity_implies_equivalence: assumes "P ∼⋅[F] Q" shows "FL_logically_equivalent F P Q"
unfolding FL_logically_equivalent_def proof
fix x :: "('idx, 'pred, 'act, 'effect) formula"
show "x ∈ 𝒜[F] ⟶ P ⊨ x ⟷ Q ⊨ x"
proof
assume "x ∈ 𝒜[F]" then show "P ⊨ x ⟷ Q ⊨ x"
using assms proof (induction x arbitrary: P Q)
case Conj then show ?case
by simp
next
case Not then show ?case
by simp
next
case Pred then show ?case
by (metis FL_bisimilar_is_L_bisimulation is_L_bisimulation_def symp_def FL_valid_Pred)
next
case Act then show ?case
by (metis FL_bisimilar_symp FL_bisimilarity_implies_equivalence_Act sympE)
qed
qed
qed

end

end
```