Theory FL_Equivalence_Implies_Bisimilarity
theory FL_Equivalence_Implies_Bisimilarity
imports
FL_Logical_Equivalence
begin
section ‹Logical Equivalence Implies \texorpdfstring{$F/L$}{F/L}-Bisimilarity›
context indexed_effect_nominal_ts
begin
definition is_distinguishing_formula :: "('idx, 'pred, 'act, 'effect) 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 :
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) FL_valid_eqvt)
lemma FL_equivalent_iff_not_distinguished:
"FL_logically_equivalent F P Q ⟷ ¬(∃x. x ∈ 𝒜[F] ∧ x distinguishes P from Q)"
by (meson FL_logically_equivalent_def Not is_distinguishing_formula_def FL_valid_Not)
text ‹There exists a distinguishing formula for~@{term P} and~@{term Q} in~‹𝒜[F]› whose
support is contained in~@{term "supp (F,P)"}.›
lemma FL_distinguished_bounded_support:
assumes "x ∈ 𝒜[F]" and "x distinguishes P from Q"
obtains y where "y ∈ 𝒜[F]" and "supp y ⊆ supp (F,P)" and "y distinguishes P from Q"
proof -
let ?B = "{p ∙ x|p. supp (F,P) ♯* p}"
have "supp (F,P) supports ?B"
unfolding supports_def proof (clarify)
fix a b
assume a: "a ∉ supp (F,P)" and b: "b ∉ supp (F,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 (F,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 (F,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 (F,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 (F,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 (F,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, 'effect) formula"
from finite_supp_B and card_B and supp_B_subset_supp_P have "supp ?y ⊆ supp (F,P)"
by simp
moreover have "?y ∈ 𝒜[F]"
proof
show "finite (supp (Abs_bset ?B :: (_,_,_,_) formula set['idx]))"
using finite_supp_B card_B by simp
next
fix x'
assume "x' ∈ set_bset (Abs_bset ?B :: (_,_,_,_) formula set['idx])"
then obtain p where p_x: "x' = p ∙ x" and fresh_p: "supp (F,P) ♯* p"
using card_B by auto
from fresh_p have "p ∙ F = F"
using fresh_star_Pair fresh_star_supp_conv perm_supp_eq by blast
with ‹x ∈ 𝒜[F]› show "x' ∈ 𝒜[F]"
using p_x by (metis is_FL_formula_eqvt)
qed
moreover have "?y distinguishes P from Q"
unfolding is_distinguishing_formula_def proof
from ‹x distinguishes P from Q› show "P ⊨ ?y"
by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def fresh_star_Un supp_Pair supp_perm_eq FL_valid_eqvt)
next
from ‹x distinguishes P from Q› 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
using that by blast
qed
lemma FL_equivalence_is_L_bisimulation: "is_L_bisimulation FL_logically_equivalent"
proof -
{
fix F have "symp (FL_logically_equivalent F)"
by (rule sympI) (metis FL_logically_equivalent_def)
}
moreover
{
fix F P Q f φ
assume "FL_logically_equivalent F P Q" and "f ∈⇩f⇩s F" and "⟨f⟩P ⊢ φ"
then have "⟨f⟩Q ⊢ φ"
by (metis FL_logically_equivalent_def Pred FL_valid_Pred)
}
moreover
{
fix F P Q f α P'
assume "FL_logically_equivalent F P Q" and "f ∈⇩f⇩s F" and "bn α ♯* (⟨f⟩Q, F, f)" and "⟨f⟩P → ⟨α,P'⟩"
then have "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ FL_logically_equivalent (L (α,F,f)) P' Q'"
proof -
{
let ?Q' = "{Q'. ⟨f⟩Q → ⟨α,Q'⟩}"
assume "∀Q'∈?Q'. ¬ FL_logically_equivalent (L (α,F,f)) P' Q'"
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act, 'effect) formula. x ∈ 𝒜[L (α,F,f)] ∧ x distinguishes P' from Q'"
by (metis FL_equivalent_iff_not_distinguished)
then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act, 'effect) formula. x ∈ 𝒜[L (α,F,f)] ∧ supp x ⊆ supp (L (α,F,f), P') ∧ x distinguishes P' from Q'"
by (metis FL_distinguished_bounded_support)
then obtain g :: "'state ⇒ ('idx, 'pred, 'act, 'effect) formula" where
*: "∀Q'∈?Q'. g Q' ∈ 𝒜[L (α,F,f)] ∧ supp (g Q') ⊆ supp (L (α,F,f), P') ∧ (g Q') distinguishes P' from Q'"
by metis
have "supp (g ` ?Q') ⊆ supp (L (α,F,f), P')"
by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)
then have finite_supp_image: "finite (supp (g ` ?Q'))"
using finite_supp rev_finite_subset by blast
have "|g ` ?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: "|g ` ?Q'| <o natLeq +c |UNIV :: 'idx set|" .
let ?y = "Conj (Abs_bset (g ` ?Q')) :: ('idx, 'pred, 'act, 'effect) formula"
have "Act f α ?y ∈ 𝒜[F]"
proof
from ‹f ∈⇩f⇩s F› show "f ∈⇩f⇩s F" .
next
from ‹bn α ♯* (⟨f⟩Q, F, f)› show "bn α ♯* (F, f)"
using fresh_star_Pair by blast
next
show "Conj (Abs_bset (g ` ?Q')) ∈ 𝒜[L (α, F, f)]"
proof
show "finite (supp (Abs_bset (g ` ?Q') :: (_,_,_,_) formula set['idx]))"
using finite_supp_image card_image by simp
next
fix x'
assume "x' ∈ set_bset (Abs_bset (g ` ?Q') :: (_,_,_,_) formula set['idx])"
then obtain Q' where "x' = g Q'" and "⟨f⟩Q → ⟨α,Q'⟩"
using card_image by auto
with "*" show "x' ∈ 𝒜[L (α, F, f)]"
using mem_Collect_eq by blast
qed
qed
moreover have "P ⊨ Act f α ?y"
unfolding FL_valid_Act proof (standard+)
show "⟨f⟩P → ⟨α,P'⟩" by fact
next
{
fix Q'
assume "⟨f⟩Q → ⟨α,Q'⟩"
with "*" have "P' ⊨ g 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 ⊨ Act f α ?y"
proof
assume "Q ⊨ Act f α ?y"
then obtain Q' where 1: "⟨f⟩Q → ⟨α,Q'⟩" and 2: "Q' ⊨ ?y"
using ‹bn α ♯* (⟨f⟩Q, F, f)› by (metis fresh_star_Pair FL_valid_Act_fresh)
from 2 have "⋀Q''. ⟨f⟩Q → ⟨α,Q''⟩ ⟶ Q' ⊨ g 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 ‹FL_logically_equivalent F P Q› FL_logically_equivalent_def)
}
then show ?thesis by auto
qed
}
ultimately show ?thesis
unfolding is_L_bisimulation_def by metis
qed
theorem FL_equivalence_implies_bisimilarity: assumes "FL_logically_equivalent F P Q" shows "P ∼⋅[F] Q"
using assms by (metis FL_bisimilar_def FL_equivalence_is_L_bisimulation)
end
end