# Theory Expressive_Completeness

theory Expressive_Completeness
imports
Bisimilarity_Implies_Equivalence
Equivalence_Implies_Bisimilarity
Disjunction
begin

section ‹Expressive Completeness›

context indexed_nominal_ts
begin

subsection ‹Distinguishing formulas›

text ‹Lemma \emph{distinguished\_bounded\_support} only shows the existence of a distinguishing
formula, without stating what this formula looks like. We now define an explicit function that
returns a distinguishing formula, in a way that this function is equivariant (on pairs of
non-equivalent states).

Note that this definition uses Hilbert's choice operator~$\varepsilon$, which is not necessarily
equivariant. This is immediately remedied by a hull construction.›

definition distinguishing_formula :: "'state ⇒ 'state ⇒ ('idx, 'pred, 'act) formula" where
"distinguishing_formula P Q ≡ Conj (Abs_bset {-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True})"

― ‹just an auxiliary lemma that will be useful further below›
lemma distinguishing_formula_card_aux:
"|{-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True}| <o natLeq +c |UNIV :: 'idx set|"
proof -
let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))"
let ?B = "{-p ∙ ?some p|p. True}"

have "?B ⊆ (λp. -p ∙ ?some p)  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 show ?thesis .
qed

― ‹just an auxiliary lemma that will be useful further below›
lemma distinguishing_formula_supp_aux:
assumes "¬ (P =⋅ Q)"
shows "supp (Abs_bset {-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True} :: _ set['idx]) ⊆ supp P"
proof -
let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))"
let ?B = "{-p ∙ ?some p|p. True}"

{
fix p
from assms have "¬ (p ∙ P =⋅ p ∙ Q)"
by (metis logically_equivalent_eqvt permute_minus_cancel(2))
then have "supp (?some p) ⊆ supp (p ∙ P)"
using distinguished_bounded_support by (metis (mono_tags, lifting) equivalent_iff_not_distinguished someI_ex)
}
note supp_some = this

{
fix x
assume "x ∈ ?B"
then obtain p where "x = -p ∙ ?some p"
by blast
with supp_some have "supp (p ∙ x) ⊆ supp (p ∙ P)"
by simp
then have "supp x ⊆ supp P"
by (metis (full_types) permute_boolE subset_eqvt supp_eqvt)
}
note "*" = this
have supp_B: "supp ?B ⊆ supp P"
by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)

from supp_B and distinguishing_formula_card_aux show ?thesis
using supp_Abs_bset by blast
qed

lemma distinguishing_formula_eqvt [simp]:
assumes "¬ (P =⋅ Q)"
shows "p ∙ distinguishing_formula P Q = distinguishing_formula (p ∙ P) (p ∙ Q)"
proof -
let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))"
let ?B = "{-p ∙ ?some p|p. True}"

from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P"
by (rule distinguishing_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with distinguishing_formula_card_aux have *: "p ∙ Conj (Abs_bset ?B) = Conj (Abs_bset (p ∙ ?B))"
by simp

let ?some' = "λp'. (ϵx. supp x ⊆ supp (p' ∙ p ∙ P) ∧ x distinguishes (p' ∙ p ∙ P) from (p' ∙ p ∙ Q))"
let ?B' = "{-p' ∙ ?some' p'|p'. True}"

have "p ∙ ?B = ?B'"
proof
{
fix px
assume "px ∈ p ∙ ?B"
then obtain x where 1: "px = p ∙ x" and 2: "x ∈ ?B"
by (metis (no_types, lifting) image_iff permute_set_eq_image)
from 2 obtain p' where 3: "x = -p' ∙ ?some p'"
by blast
from 1 and 3 have "px = -(p' - p) ∙ ?some' (p' - p)"
by simp
then have "px ∈ ?B'"
by blast
}
then show "p ∙ ?B ⊆ ?B'"
by blast
next
{
fix x
assume "x ∈ ?B'"
then obtain p' where "x = -p' ∙ ?some' p'"
by blast
then have "x = p ∙ -(p' + p) ∙ ?some (p' + p)"
then have "x ∈ p ∙ ?B"
using mem_permute_iff by blast
}
then show "?B' ⊆ p ∙ ?B"
by blast
qed

with "*" show ?thesis
unfolding distinguishing_formula_def by simp
qed

lemma supp_distinguishing_formula:
assumes "¬ (P =⋅ Q)"
shows "supp (distinguishing_formula P Q) ⊆ supp P"
proof -
let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))"
let ?B = "{- p ∙ ?some p|p. True}"

from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P"
by (rule distinguishing_formula_supp_aux)
moreover from this have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
ultimately show ?thesis
unfolding distinguishing_formula_def by simp
qed

lemma distinguishing_formula_distinguishes:
assumes "¬ (P =⋅ Q)"
shows "(distinguishing_formula P Q) distinguishes P from Q"
proof -
let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))"
let ?B = "{- p ∙ ?some p|p. True}"

{
fix p
have "(?some p) distinguishes (p ∙ P) from (p ∙ Q)"
using assms
by (metis (mono_tags, lifting) is_distinguishing_formula_eqvt distinguished_bounded_support equivalent_iff_not_distinguished someI_ex)
}
note some_distinguishes = this

{
fix P'
from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P"
by (rule distinguishing_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with distinguishing_formula_card_aux have "P' ⊨ distinguishing_formula P Q ⟷ (∀x∈?B. P' ⊨ x)"
unfolding distinguishing_formula_def by simp
}
note valid_distinguishing_formula = this

{
fix p
have "P ⊨ -p ∙ ?some p"
by (metis (mono_tags) is_distinguishing_formula_def permute_minus_cancel(2) some_distinguishes valid_eqvt)
}
then have "P ⊨ distinguishing_formula P Q"
using valid_distinguishing_formula by blast

moreover have "¬ Q ⊨ distinguishing_formula P Q"
using valid_distinguishing_formula by (metis (mono_tags, lifting) is_distinguishing_formula_def mem_Collect_eq permute_minus_cancel(1) some_distinguishes valid_eqvt)

ultimately show "(distinguishing_formula P Q) distinguishes P from Q"
using is_distinguishing_formula_def by blast
qed

subsection ‹Characteristic formulas›

text ‹A \emph{characteristic formula} for a state~$P$ is valid for (exactly) those states that are
bisimilar to~$P$.›

definition characteristic_formula :: "'state ⇒ ('idx, 'pred, 'act) formula" where
"characteristic_formula P ≡ Conj (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)})"

― ‹just an auxiliary lemma that will be useful further below›
lemma characteristic_formula_card_aux:
"|{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}| <o natLeq +c |UNIV :: 'idx set|"
proof -
let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

have "?B ⊆ (distinguishing_formula P)  UNIV"
by auto
then have "|?B| ≤o |UNIV :: 'state set|"
by (rule surj_imp_ordLeq)
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 show ?thesis .
qed

― ‹just an auxiliary lemma that will be useful further below›
lemma characteristic_formula_supp_aux:
shows "supp (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)} :: _ set['idx]) ⊆ supp P"
proof -
let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

{
fix x
assume "x ∈ ?B"
then obtain Q where "x = distinguishing_formula P Q" and "¬ (P =⋅ Q)"
by blast
with supp_distinguishing_formula have "supp x ⊆ supp P"
by metis
}
note "*" = this
have supp_B: "supp ?B ⊆ supp P"
by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast)

from supp_B and characteristic_formula_card_aux show ?thesis
using supp_Abs_bset by blast
qed

lemma characteristic_formula_eqvt (*[eqvt]*) [simp]:
"p ∙ characteristic_formula P = characteristic_formula (p ∙ P)"
proof -
let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P"
by (fact characteristic_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with characteristic_formula_card_aux have *: "p ∙ Conj (Abs_bset ?B) = Conj (Abs_bset (p ∙ ?B))"
by simp

let ?B' = "{distinguishing_formula (p ∙ P) Q|Q. ¬ ((p ∙ P) =⋅ Q)}"

have "p ∙ ?B = ?B'"
proof
{
fix px
assume "px ∈ p ∙ ?B"
then obtain x where 1: "px = p ∙ x" and 2: "x ∈ ?B"
by (metis (no_types, lifting) image_iff permute_set_eq_image)
from 2 obtain Q where 3: "x = distinguishing_formula P Q" and 4: "¬ (P =⋅ Q)"
by blast
with 1 have "px = distinguishing_formula (p ∙ P) (p ∙ Q)"
by simp
moreover from 4 have "¬ ((p ∙ P) =⋅ (p ∙ Q))"
by (metis logically_equivalent_eqvt permute_minus_cancel(2))
ultimately have "px ∈ ?B'"
by blast
}
then show "p ∙ ?B ⊆ ?B'"
by blast
next
{
fix x
assume "x ∈ ?B'"
then obtain Q where 1: "x = distinguishing_formula (p ∙ P) Q" and 2: "¬ ((p ∙ P) =⋅ Q)"
by blast
from 2 have "¬ (P =⋅ (-p ∙ Q))"
by (metis logically_equivalent_eqvt permute_minus_cancel(1))
moreover from this and 1 have "x = p ∙ distinguishing_formula P (-p ∙ Q)"
by simp
ultimately have "x ∈ p ∙ ?B"
using mem_permute_iff by blast
}
then show "?B' ⊆ p ∙ ?B"
by blast
qed

with "*" show ?thesis
unfolding characteristic_formula_def by simp
qed

lemma characteristic_formula_eqvt_raw [simp]:
"p ∙ characteristic_formula = characteristic_formula"

lemma characteristic_formula_is_characteristic':
"Q ⊨ characteristic_formula P ⟷ P =⋅ Q"
proof -
let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}"

{
fix P'
have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P"
by (fact characteristic_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with characteristic_formula_card_aux have "P' ⊨ characteristic_formula P ⟷ (∀x∈?B. P' ⊨ x)"
unfolding characteristic_formula_def by simp
}
note valid_characteristic_formula = this

show ?thesis
proof
assume *: "Q ⊨ characteristic_formula P"
show "P =⋅ Q"
proof (rule ccontr)
assume "¬ (P =⋅ Q)"
with "*" show False
using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
qed
next
assume "P =⋅ Q"
moreover have "P ⊨ characteristic_formula P"
using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
ultimately show "Q ⊨ characteristic_formula P"
using logically_equivalent_def by blast
qed
qed

lemma characteristic_formula_is_characteristic:
"Q ⊨ characteristic_formula P ⟷ P ∼⋅ Q"
using characteristic_formula_is_characteristic' by (meson bisimilarity_implies_equivalence equivalence_implies_bisimilarity)

subsection ‹Expressive completeness›

text ‹Every finitely supported set of states that is closed under bisimulation can be described by
a formula; namely, by a disjunction of characteristic formulas.›

theorem expressive_completeness:
assumes "finite (supp S)"
and "⋀P Q. P ∈ S ⟹ P ∼⋅ Q ⟹ Q ∈ S"
shows "P ⊨ Disj (Abs_bset (characteristic_formula  S)) ⟷ P ∈ S"
proof -
let ?B = "characteristic_formula  S"

have "?B ⊆ characteristic_formula  UNIV"
by auto
then have "|?B| ≤o |UNIV :: 'state set|"
by (rule surj_imp_ordLeq)
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_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" .

have "eqvt image" and "eqvt characteristic_formula"
then have "supp ?B ⊆ supp S"
using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt by blast
with card_B have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp S"
using supp_Abs_bset by blast
with ‹finite (supp S)› have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with card_B have "P ⊨ Disj (Abs_bset (characteristic_formula  S)) ⟷ (∃x∈?B. P ⊨ x)"
by simp

with ‹⋀P Q. P ∈ S ⟹ P ∼⋅ Q ⟹ Q ∈ S› show ?thesis
using characteristic_formula_is_characteristic characteristic_formula_is_characteristic' logically_equivalent_def by fastforce
qed

end

end