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 "p ∙ distinguishing_weak_formula P Q = distinguishing_weak_formula (p ∙ P) (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
    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 "supp (distinguishing_weak_formula P Q) ⊆ 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}"

    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 "P ⊨ distinguishing_weak_formula P Q"
      using valid_distinguishing_formula by blast

    moreover have "¬ Q ⊨ distinguishing_weak_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_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 "?B ⊆ (distinguishing_weak_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_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 "x = distinguishing_weak_formula P Q" 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]:
    "p ∙ characteristic_weak_formula P = characteristic_weak_formula (p ∙ 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
    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: "x = distinguishing_weak_formula P Q" 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]:
    "p ∙ characteristic_weak_formula = characteristic_weak_formula"
    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 *: "Q ⊨ characteristic_weak_formula P"
      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 "P ⊨ characteristic_weak_formula P"
        using distinguishing_weak_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto
      ultimately show "Q ⊨ characteristic_weak_formula P"
        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 = "characteristic_weak_formula ` S"

    have "?B ⊆ characteristic_weak_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_weak_formula"
      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 "eqvt Formula.Not"
      by (simp add: eqvtI)
    with supp_B and ‹eqvt image› 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