Theory Weak_Equivalence_Implies_Bisimilarity
theory Weak_Equivalence_Implies_Bisimilarity
imports
Weak_Logical_Equivalence
begin
section ‹Weak Logical Equivalence Implies Weak Bisimilarity›
context indexed_weak_nominal_ts
begin
definition is_distinguishing_formula :: "('idx, 'pred, 'act) formula ⇒ 'state ⇒ 'state ⇒ bool"
(‹_ distinguishes _ from _› [100,100,100] 100)
where
"x distinguishes P from Q ≡ P ⊨ x ∧ ¬ Q ⊨ x"
lemma is_distinguishing_formula_eqvt [simp]:
assumes "x distinguishes P from Q" shows "(p ∙ x) distinguishes (p ∙ P) from (p ∙ Q)"
using assms unfolding is_distinguishing_formula_def
by (metis permute_minus_cancel(2) valid_eqvt)
lemma weakly_equivalent_iff_not_distinguished: "(P ≡⋅ Q) ⟷ ¬(∃x. weak_formula x ∧ x distinguishes P from Q)"
by (meson is_distinguishing_formula_def weakly_logically_equivalent_def valid_Not wf_Not)
text ‹There exists a distinguishing weak formula for~@{term P} and~@{term Q} whose support is
contained in~@{term "supp P"}.›
lemma distinguished_bounded_support:
assumes "weak_formula x" and "x distinguishes P from Q"
obtains y where "weak_formula y" and "supp y ⊆ supp P" and "y distinguishes P from Q"
proof -
let ?B = "{p ∙ x|p. supp P ♯* p}"
have "supp P supports ?B"
unfolding supports_def proof (clarify)
fix a b
assume a: "a ∉ supp P" and b: "b ∉ supp P"
have "(a ⇌ b) ∙ ?B ⊆ ?B"
proof
fix x'
assume "x' ∈ (a ⇌ b) ∙ ?B"
then obtain p where 1: "x' = (a ⇌ b) ∙ p ∙ x" and 2: "supp P ♯* p"
by (auto simp add: permute_set_def)
let ?q = "(a ⇌ b) + p"
from 1 have "x' = ?q ∙ x"
by simp
moreover from a and b and 2 have "supp P ♯* ?q"
by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
ultimately show "x' ∈ ?B" by blast
qed
moreover have "?B ⊆ (a ⇌ b) ∙ ?B"
proof
fix x'
assume "x' ∈ ?B"
then obtain p where 1: "x' = p ∙ x" and 2: "supp P ♯* p"
by auto
let ?q = "(a ⇌ b) + p"
from 1 have "x' = (a ⇌ b) ∙ ?q ∙ x"
by simp
moreover from a and b and 2 have "supp P ♯* ?q"
by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3))
ultimately show "x' ∈ (a ⇌ b) ∙ ?B"
using mem_permute_iff by blast
qed
ultimately show "(a ⇌ b) ∙ ?B = ?B" ..
qed
then have supp_B_subset_supp_P: "supp ?B ⊆ supp P"
by (metis (erased, lifting) finite_supp supp_is_subset)
then have finite_supp_B: "finite (supp ?B)"
using finite_supp rev_finite_subset by blast
have "?B ⊆ (λp. p ∙ x) ` UNIV"
by auto
then have "|?B| ≤o |UNIV :: perm set|"
by (rule surj_imp_ordLeq)
also have "|UNIV :: perm set| <o |UNIV :: 'idx set|"
by (metis card_idx_perm)
also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
by (metis Cnotzero_UNIV ordLeq_csum2)
finally have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" .
let ?y = "Conj (Abs_bset ?B) :: ('idx, 'pred, 'act) formula"
have "weak_formula ?y"
proof
show "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp_B card_B by simp
next
fix x' assume "x' ∈ set_bset (Abs_bset ?B :: _ set['idx])"
with card_B obtain p where "x' = p ∙ x"
using Abs_bset_inverse mem_Collect_eq by auto
then show "weak_formula x'"
using ‹weak_formula x› by (metis weak_formula_eqvt)
qed
moreover from finite_supp_B and card_B and supp_B_subset_supp_P have "supp ?y ⊆ supp P"
by simp
moreover have "?y distinguishes P from Q"
unfolding is_distinguishing_formula_def proof
from assms show "P ⊨ ?y"
by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def supp_perm_eq valid_eqvt)
next
from assms show "¬ Q ⊨ ?y"
by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def permute_zero fresh_star_zero)
qed
ultimately show ?thesis ..
qed
lemma weak_equivalence_is_weak_bisimulation: "is_weak_bisimulation weakly_logically_equivalent"
proof -
have "symp weakly_logically_equivalent"
by (metis weakly_logically_equivalent_def sympI)
moreover
{
fix P Q φ assume "P ≡⋅ Q" and "P ⊢ φ"
then have "∃Q'. Q ⇒ Q' ∧ P ≡⋅ Q' ∧ Q' ⊢ φ"
proof -
{
let ?Q' = "{Q'. Q ⇒ Q' ∧ Q' ⊢ φ}"
assume "∀Q'∈?Q'. ¬ P ≡⋅ Q'"
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. weak_formula x ∧ x distinguishes P from Q'"
by (metis weakly_equivalent_iff_not_distinguished)
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. weak_formula x ∧ supp x ⊆ supp P ∧ x distinguishes P from Q'"
by (metis distinguished_bounded_support)
then obtain f :: "'state ⇒ ('idx, 'pred, 'act) formula" where
*: "∀Q'∈?Q'. weak_formula (f Q') ∧ supp (f Q') ⊆ supp P ∧ (f Q') distinguishes P from Q'"
by metis
have "supp (f ` ?Q') ⊆ supp P"
by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)
then have finite_supp_image: "finite (supp (f ` ?Q'))"
using finite_supp rev_finite_subset by blast
have "|f ` ?Q'| ≤o |UNIV :: 'state set|"
using card_of_UNIV card_of_image ordLeq_transitive by blast
also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
by (metis card_idx_state)
also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
by (metis Cnotzero_UNIV ordLeq_csum2)
finally have card_image: "|f ` ?Q'| <o natLeq +c |UNIV :: 'idx set|" .
let ?y = "Conj (Abs_bset (f ` ?Q')) :: ('idx, 'pred, 'act) formula"
have "weak_formula ?y"
proof (standard+)
show "finite (supp (Abs_bset (f ` ?Q') :: _ set['idx]))"
using finite_supp_image card_image by simp
next
fix x assume "x ∈ set_bset (Abs_bset (f ` ?Q') :: _ set['idx])"
with card_image obtain Q' where "Q' ∈ ?Q'" and "x = f Q'"
using Abs_bset_inverse imageE set_bset set_bset_to_set_bset by auto
then show "weak_formula x"
using "*" by metis
qed
let ?z = "⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton ?y)))"
have "weak_formula ?z"
by standard (fact ‹weak_formula ?y›)
moreover have "P ⊨ ?z"
proof -
have "P ⇒⟨τ⟩ P"
by simp
moreover
{
fix Q'
assume "Q ⇒ Q' ∧ Q' ⊢ φ"
with "*" have "P ⊨ f Q'"
by (metis is_distinguishing_formula_def mem_Collect_eq)
}
with ‹P ⊢ φ› have "P ⊨ Conj (binsert (Pred φ) (bsingleton ?y))"
by (simp add: binsert.rep_eq finite_supp_image card_image)
ultimately show ?thesis
using valid_weak_action_modality by blast
qed
moreover have "¬ Q ⊨ ?z"
proof
assume "Q ⊨ ?z"
then obtain Q' where 1: "Q ⇒ Q'" and "Q' ⊨ Conj (binsert (Pred φ) (bsingleton ?y))"
using valid_weak_action_modality by auto
then have 2: "Q' ⊢ φ" and 3: "Q' ⊨ ?y"
by (simp add: binsert.rep_eq finite_supp_image card_image)+
from 3 have "⋀Q''. Q ⇒ Q'' ∧ Q'' ⊢ φ ⟶ Q' ⊨ f Q''"
by (simp add: finite_supp_image card_image)
with 1 and 2 and "*" show False
using is_distinguishing_formula_def by blast
qed
ultimately have False
by (metis ‹P ≡⋅ Q› weakly_logically_equivalent_def)
}
then show ?thesis
by blast
qed
}
moreover
{
fix P Q α P' assume "P ≡⋅ Q" and "bn α ♯* Q" and "P → ⟨α,P'⟩"
then have "∃Q'. Q ⇒⟨α⟩ Q' ∧ P' ≡⋅ Q'"
proof -
{
let ?Q' = "{Q'. Q ⇒⟨α⟩ Q'}"
assume "∀Q'∈?Q'. ¬ P' ≡⋅ Q'"
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. weak_formula x ∧ x distinguishes P' from Q'"
by (metis weakly_equivalent_iff_not_distinguished)
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. weak_formula x ∧ supp x ⊆ supp P' ∧ x distinguishes P' from Q'"
by (metis distinguished_bounded_support)
then obtain f :: "'state ⇒ ('idx, 'pred, 'act) formula" where
*: "∀Q'∈?Q'. weak_formula (f Q') ∧ supp (f Q') ⊆ supp P' ∧ (f Q') distinguishes P' from Q'"
by metis
have "supp P' supports (f ` ?Q')"
unfolding supports_def proof (clarify)
fix a b
assume a: "a ∉ supp P'" and b: "b ∉ supp P'"
have "(a ⇌ b) ∙ (f ` ?Q') ⊆ f ` ?Q'"
proof
fix x
assume "x ∈ (a ⇌ b) ∙ (f ` ?Q')"
then obtain Q' where 1: "x = (a ⇌ b) ∙ f Q'" and 2: "Q ⇒⟨α⟩ Q'"
by auto (metis (no_types, lifting) imageE image_eqvt mem_Collect_eq permute_set_eq_image)
with "*" and a and b have "a ∉ supp (f Q')" and "b ∉ supp (f Q')"
by auto
with 1 have "x = f Q'"
by (metis fresh_perm fresh_star_def supp_perm_eq swap_atom)
with 2 show "x ∈ f ` ?Q'"
by simp
qed
moreover have "f ` ?Q' ⊆ (a ⇌ b) ∙ (f ` ?Q')"
proof
fix x
assume "x ∈ f ` ?Q'"
then obtain Q' where 1: "x = f Q'" and 2: "Q ⇒⟨α⟩ Q'"
by auto
with "*" and a and b have "a ∉ supp (f Q')" and "b ∉ supp (f Q')"
by auto
with 1 have "x = (a ⇌ b) ∙ f Q'"
by (metis fresh_perm fresh_star_def supp_perm_eq swap_atom)
with 2 show "x ∈ (a ⇌ b) ∙ (f ` ?Q')"
using mem_permute_iff by blast
qed
ultimately show "(a ⇌ b) ∙ (f ` ?Q') = f ` ?Q'" ..
qed
then have supp_image_subset_supp_P': "supp (f ` ?Q') ⊆ supp P'"
by (metis (erased, lifting) finite_supp supp_is_subset)
then have finite_supp_image: "finite (supp (f ` ?Q'))"
using finite_supp rev_finite_subset by blast
have "|f ` ?Q'| ≤o |UNIV :: 'state set|"
by (metis card_of_UNIV card_of_image ordLeq_transitive)
also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|"
by (metis card_idx_state)
also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|"
by (metis Cnotzero_UNIV ordLeq_csum2)
finally have card_image: "|f ` ?Q'| <o natLeq +c |UNIV :: 'idx set|" .
let ?y = "Conj (Abs_bset (f ` ?Q')) :: ('idx, 'pred, 'act) formula"
have "weak_formula (⟨⟨α⟩⟩?y)"
proof (standard+)
show "finite (supp (Abs_bset (f ` ?Q') :: _ set['idx]))"
using finite_supp_image card_image by simp
next
fix x assume "x ∈ set_bset (Abs_bset (f ` ?Q') :: _ set['idx])"
with card_image obtain Q' where "Q' ∈ ?Q'" and "x = f Q'"
using Abs_bset_inverse imageE set_bset set_bset_to_set_bset by auto
then show "weak_formula x"
using "*" by metis
qed
moreover have "P ⊨ ⟨⟨α⟩⟩?y"
unfolding valid_weak_action_modality proof (standard+)
from ‹P → ⟨α,P'⟩› show "P ⇒⟨α⟩ P'"
by simp
next
{
fix Q'
assume "Q ⇒⟨α⟩ Q'"
with "*" have "P' ⊨ f Q'"
by (metis is_distinguishing_formula_def mem_Collect_eq)
}
then show "P' ⊨ ?y"
by (simp add: finite_supp_image card_image)
qed
moreover have "¬ Q ⊨ ⟨⟨α⟩⟩?y"
proof
assume "Q ⊨ ⟨⟨α⟩⟩?y"
then obtain Q' where 1: "Q ⇒⟨α⟩ Q'" and 2: "Q' ⊨ ?y"
using ‹bn α ♯* Q› by (metis valid_weak_action_modality_fresh)
from 2 have "⋀Q''. Q ⇒⟨α⟩ Q'' ⟶ Q' ⊨ f Q''"
by (simp add: finite_supp_image card_image)
with 1 and "*" show False
using is_distinguishing_formula_def by blast
qed
ultimately have False
by (metis ‹P ≡⋅ Q› weakly_logically_equivalent_def)
}
then show ?thesis by auto
qed
}
ultimately show ?thesis
unfolding is_weak_bisimulation_def by metis
qed
theorem weak_equivalence_implies_weak_bisimilarity: assumes "P ≡⋅ Q" shows "P ≈⋅ Q"
using assms by (metis weakly_bisimilar_def weak_equivalence_is_weak_bisimulation)
end
end