Theory Weak_Expressive_Completeness

theory Weak_Expressive_Completeness
imports
Weak_Bisimilarity_Implies_Equivalence
Weak_Equivalence_Implies_Bisimilarity
Disjunction
begin

section ‹Weak Expressive Completeness›

context indexed_weak_nominal_ts
begin

subsection ‹Distinguishing weak formulas›

text ‹Lemma \emph{distinguished\_bounded\_support} only shows the existence of a distinguishing
weak formula, without stating what this formula looks like. We now define an explicit function
that returns a distinguishing weak formula, in a way that this function is equivariant (on pairs
of non-weakly-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_weak_formula :: "'state  'state  ('idx, 'pred, 'act) formula" where
"distinguishing_weak_formula P Q  Conj (Abs_bset {-p  (ϵx. weak_formula 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_weak_formula_card_aux:
"|{-p  (ϵx. weak_formula 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. weak_formula 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_weak_formula_supp_aux:
assumes "¬ (P ≡⋅ Q)"
shows "supp (Abs_bset {-p  (ϵx. weak_formula x  supp x  supp (p  P)  x distinguishes (p  P) from (p  Q))|p. True} :: _ set['idx])  supp P"
proof -
let ?some = "λp. (ϵx. weak_formula 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 weakly_logically_equivalent_eqvt permute_minus_cancel(2))
then have "supp (?some p)  supp (p  P)"
using distinguished_bounded_support by (metis (mono_tags, lifting) weakly_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_weak_formula_card_aux show ?thesis
using supp_Abs_bset by blast
qed

lemma distinguishing_weak_formula_eqvt [simp]:
assumes "¬ (P ≡⋅ Q)"
shows
proof -
let ?some = "λp. (ϵx. weak_formula 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_weak_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with distinguishing_weak_formula_card_aux have *: "p  Conj (Abs_bset ?B) = Conj (Abs_bset (p  ?B))"
by simp

let ?some' = "λp'. (ϵx. weak_formula 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)"
by (simp add: add.inverse_distrib_swap)
then have "x  p  ?B"
using mem_permute_iff by blast
}
then show "?B'  p  ?B"
by blast
qed

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

lemma supp_distinguishing_weak_formula:
assumes "¬ (P ≡⋅ Q)"
shows
proof -
let ?some = "λp. (ϵx. weak_formula 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_weak_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_weak_formula_def by simp
qed

lemma distinguishing_weak_formula_distinguishes:
assumes "¬ (P ≡⋅ Q)"
shows "(distinguishing_weak_formula P Q) distinguishes P from Q"
proof -
let ?some = "λp. (ϵx. weak_formula 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 permute_minus_cancel(2) weakly_logically_equivalent_eqvt)
then have "(?some p) distinguishes (p  P) from (p  Q)"
by (metis (mono_tags, lifting) distinguished_bounded_support weakly_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_weak_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with distinguishing_weak_formula_card_aux have "P'  distinguishing_weak_formula P Q  (x?B. P'  x)"
unfolding distinguishing_weak_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
using valid_distinguishing_formula by blast

moreover have
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_weak_formula P Q) distinguishes P from Q"
using is_distinguishing_formula_def by blast
qed

lemma distinguishing_weak_formula_is_weak:
assumes "¬ (P ≡⋅ Q)"
shows "weak_formula (distinguishing_weak_formula P Q)"
proof -
let ?some = "λp. (ϵx. weak_formula 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_weak_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast

moreover have "set_bset (Abs_bset ?B :: _ set['idx]) = ?B"
using distinguishing_weak_formula_card_aux Abs_bset_inverse' by simp

moreover
{
fix x
assume "x  ?B"
then obtain p where "x = -p  ?some p"
by blast
moreover from assms have "¬ (p  P) ≡⋅ (p  Q)"
by (metis permute_minus_cancel(2) weakly_logically_equivalent_eqvt)
then have "weak_formula (?some p)"
by (metis (mono_tags, lifting) distinguished_bounded_support weakly_equivalent_iff_not_distinguished someI_ex)
ultimately have "weak_formula x"
by simp
}

ultimately show ?thesis
unfolding distinguishing_weak_formula_def using wf_Conj by blast
qed

subsection ‹Characteristic weak formulas›

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

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

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

have
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_weak_formula_supp_aux:
shows "supp (Abs_bset {distinguishing_weak_formula P Q|Q. ¬ (P ≡⋅ Q)} :: _ set['idx])  supp P"
proof -
let ?B = "{distinguishing_weak_formula P Q|Q. ¬ (P ≡⋅ Q)}"

{
fix x
assume "x  ?B"
then obtain Q where  and "¬ (P ≡⋅ Q)"
by blast
with supp_distinguishing_weak_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_weak_formula_card_aux show ?thesis
using supp_Abs_bset by blast
qed

lemma characteristic_weak_formula_eqvt (*[eqvt]*) [simp]:

proof -
let ?B = "{distinguishing_weak_formula P Q|Q. ¬ (P ≡⋅ Q)}"

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

let ?B' = "{distinguishing_weak_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:  and 4: "¬ (P ≡⋅ Q)"
by blast
with 1 have "px = distinguishing_weak_formula (p  P) (p  Q)"
by simp
moreover from 4 have "¬ (p  P) ≡⋅ (p  Q)"
by (metis weakly_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_weak_formula (p  P) Q" and 2: "¬ (p  P) ≡⋅ Q"
by blast
from 2 have "¬ P ≡⋅ (-p  Q)"
by (metis weakly_logically_equivalent_eqvt permute_minus_cancel(1))
moreover from this and 1 have "x = p  distinguishing_weak_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_weak_formula_def by simp
qed

lemma characteristic_weak_formula_eqvt_raw [simp]:

by (simp add: permute_fun_def)

lemma characteristic_weak_formula_is_weak:
"weak_formula (characteristic_weak_formula P)"
proof -
let ?B = "{distinguishing_weak_formula P Q|Q. ¬ (P ≡⋅ Q)}"

have "supp (Abs_bset ?B :: _ set['idx])  supp P"
by (fact characteristic_weak_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast

moreover have "set_bset (Abs_bset ?B :: _ set['idx]) = ?B"
using characteristic_weak_formula_card_aux Abs_bset_inverse' by simp

moreover
{
fix x
assume "x  ?B"
then have "weak_formula x"
using distinguishing_weak_formula_is_weak by blast
}

ultimately show ?thesis
unfolding characteristic_weak_formula_def using wf_Conj by presburger
qed

lemma characteristic_weak_formula_is_characteristic':
"Q  characteristic_weak_formula P  P ≡⋅ Q"
proof -
let ?B = "{distinguishing_weak_formula P Q|Q. ¬ (P ≡⋅ Q)}"

{
fix P'
have "supp (Abs_bset ?B :: _ set['idx])  supp P"
by (fact characteristic_weak_formula_supp_aux)
then have "finite (supp (Abs_bset ?B :: _ set['idx]))"
using finite_supp rev_finite_subset by blast
with characteristic_weak_formula_card_aux have "P'  characteristic_weak_formula P  (x?B. P'  x)"
unfolding characteristic_weak_formula_def by simp
}
note valid_characteristic_formula = this

show ?thesis
proof
assume *:
show "P ≡⋅ Q"
proof (rule ccontr)
assume "¬ (P ≡⋅ Q)"
with "*" show False
using distinguishing_weak_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
qed
next
assume "P ≡⋅ Q"
moreover have
using distinguishing_weak_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
ultimately show
using weakly_logically_equivalent_def characteristic_weak_formula_is_weak by blast
qed
qed

lemma characteristic_weak_formula_is_characteristic:
"Q  characteristic_weak_formula P  P ≈⋅ Q"
using characteristic_weak_formula_is_characteristic' by (meson weak_bisimilarity_implies_weak_equivalence weak_equivalence_implies_weak_bisimilarity)

subsection ‹Weak expressive completeness›

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

theorem weak_expressive_completeness:
assumes "finite (supp S)"
and "P Q. P  S  P ≈⋅ Q  Q  S"
shows "P  Disj (Abs_bset (characteristic_weak_formula  S))  P  S"
and "weak_formula (Disj (Abs_bset (characteristic_weak_formula  S)))"
proof -
let ?B =

have
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  and
by (simp add: eqvtI)+
then have supp_B: "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_weak_formula  S))  (x?B. P  x)"
by simp

with P Q. P  S  P ≈⋅ Q  Q  S show "P  Disj (Abs_bset (characteristic_weak_formula  S))  P  S"
using characteristic_weak_formula_is_characteristic characteristic_weak_formula_is_characteristic' weakly_logically_equivalent_def by fastforce

― ‹it remains to show that the disjunction is a weak formula›

have
by (simp add: eqvtI)
with supp_B and  have supp_Not_B: "supp (Formula.Not  ?B)  supp S"
using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt by blast

have "|Formula.Not  ?B| ≤o |?B|"
by simp
also note card_B
finally have card_not_B: "|Formula.Not  ?B| <o natLeq +c |UNIV :: 'idx set|" .

with supp_Not_B have "supp (Abs_bset (Formula.Not  ?B) :: _ set['idx])  supp S"
using supp_Abs_bset by blast
with finite (supp S) have "finite (supp (Abs_bset (Formula.Not  ?B) :: _ set['idx]))"
using finite_supp rev_finite_subset by blast

moreover have "x. x  Formula.Not  ?B  weak_formula x"
using characteristic_weak_formula_is_weak wf_Not by auto

moreover from card_B have *: "map_bset Formula.Not (Abs_bset ?B :: _ set['idx]) = (Abs_bset (Formula.Not  ?B) :: _ set['idx])"
using map_bset.abs_eq[unfolded eq_onp_def] by blast

moreover from card_not_B have "set_bset (Abs_bset (Formula.Not  ?B) :: _ set['idx]) = Formula.Not  ?B"
by simp

ultimately show "weak_formula (Disj (Abs_bset (characteristic_weak_formula ` S)))"
unfolding Disj_def by (metis wf_Conj wf_Not)
qed

end

end