# Theory Weak_Bisimilarity_Implies_Equivalence

```theory Weak_Bisimilarity_Implies_Equivalence
imports
Weak_Logical_Equivalence
begin

section ‹Weak Bisimilarity Implies Weak Logical Equivalence›

context indexed_weak_nominal_ts
begin

lemma weak_bisimilarity_implies_weak_equivalence_Act:
assumes "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
and "P ≈⋅ Q"
― ‹not needed: and @{prop "weak_formula x"}›
and "P ⊨ ⟨⟨α⟩⟩x"
shows "Q ⊨ ⟨⟨α⟩⟩x"
proof -
have "finite (supp Q)"
by (fact finite_supp)
with ‹P ⊨ ⟨⟨α⟩⟩x› obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P ⇒⟨α'⟩ P'" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* Q"
by (metis valid_weak_action_modality_strong)

from ‹P ≈⋅ Q› and fresh and trans obtain Q' where trans': "Q ⇒⟨α'⟩ Q'" and bisim': "P' ≈⋅ Q'"
by (metis weakly_bisimilar_weak_simulation_step)

from eq obtain p where px: "x' = p ∙ x"
by (metis Act_eq_iff_perm)

with valid have "-p ∙ P' ⊨ x"
by (metis permute_minus_cancel(1) valid_eqvt)
moreover from bisim' have "(-p ∙ P') ≈⋅ (-p ∙ Q')"
by (metis weakly_bisimilar_eqvt)
ultimately have "-p ∙ Q' ⊨ x"
using ‹⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis
with px have "Q' ⊨ x'"
by (metis permute_minus_cancel(1) valid_eqvt)

with eq and trans' show "Q ⊨ ⟨⟨α⟩⟩x"
unfolding valid_weak_action_modality by metis
qed

lemma weak_bisimilarity_implies_weak_equivalence_Pred:
assumes "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
and "P ≈⋅ Q"
― ‹not needed: and @{prop "weak_formula x"}›
and "P ⊨ ⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton x)))"
shows "Q ⊨ ⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton x)))"
proof -
let ?c = "Conj (binsert (Pred φ) (bsingleton x))"

from ‹P ⊨ ⟨⟨τ⟩⟩?c› obtain P' where trans: "P ⇒ P'" and valid: "P' ⊨ ?c"
using valid_weak_action_modality by auto

have "bn τ  ♯* Q"
with ‹P ≈⋅ Q› and trans obtain Q' where trans': "Q ⇒ Q'" and bisim': "P' ≈⋅ Q'"
by (metis weakly_bisimilar_weak_simulation_step weak_transition_tau_iff)

from valid have *: "P' ⊢ φ" and **: "P' ⊨ x"

from bisim' and * obtain Q'' where trans'': "Q' ⇒ Q''" and bisim'': "P' ≈⋅ Q''" and ***: "Q'' ⊢ φ"
by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)

from bisim'' and ** have "Q'' ⊨ x"
using ‹⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis
with *** have "Q'' ⊨ ?c"

moreover from trans' and trans'' have "Q ⇒⟨τ⟩ Q''"
by (metis tau_transition_trans weak_transition_tau_iff)

ultimately show "Q ⊨ ⟨⟨τ⟩⟩?c"
unfolding valid_weak_action_modality by metis
qed

theorem weak_bisimilarity_implies_weak_equivalence: assumes "P ≈⋅ Q" shows "P ≡⋅ Q"
proof -
{
fix x :: "('idx, 'pred, 'act) formula"
assume "weak_formula x"
then have "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
proof (induct rule: weak_formula.induct)
case (wf_Conj xset) then show ?case
by simp
next
case (wf_Not x) then show ?case
by simp
next
case (wf_Act x α) then show ?case
by (metis weakly_bisimilar_symp weak_bisimilarity_implies_weak_equivalence_Act sympE)
next
case (wf_Pred x φ) then show ?case
by (metis weakly_bisimilar_symp weak_bisimilarity_implies_weak_equivalence_Pred sympE)
qed
}
with assms show ?thesis
unfolding weakly_logically_equivalent_def by simp
qed

end

end
```