Theory Equivalence_Implies_Bisimilarity

theory Equivalence_Implies_Bisimilarity
imports
  Logical_Equivalence
begin

section ‹Logical Equivalence Implies Bisimilarity›

context indexed_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 (*[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) valid_eqvt)

  lemma equivalent_iff_not_distinguished: "(P =⋅ Q) ⟷ ¬(∃x. x distinguishes P from Q)"
  by (metis (full_types) is_distinguishing_formula_def logically_equivalent_def valid_Not)

  text ‹There exists a distinguishing formula for~@{term P} and~@{term Q} whose support is contained
  in~@{term "supp P"}.›

  lemma distinguished_bounded_support:
    assumes "x distinguishes P from Q"
    obtains y where "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"
    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 equivalence_is_bisimulation: "is_bisimulation logically_equivalent"
  proof -
    have "symp logically_equivalent"
      by (metis logically_equivalent_def sympI)
    moreover
    {
      fix P Q φ assume "P =⋅ Q" then have "P ⊢ φ ⟶ Q ⊢ φ"
        by (metis logically_equivalent_def valid_Pred)
    }
    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. x distinguishes P' from Q'"
              by (metis equivalent_iff_not_distinguished)
            then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. 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'. 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|"
              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 "P ⊨ Act α ?y"
              unfolding valid_Act proof (standard+)
                show "P → ⟨α,P'⟩" by fact
              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 ⊨ Act α ?y"
              proof
                assume "Q ⊨ Act α ?y"
                then obtain Q' where 1: "Q → ⟨α,Q'⟩" and 2: "Q' ⊨ ?y"
                  using ‹bn α ♯* Q› by (metis valid_Act_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› logically_equivalent_def)
          }
          then show ?thesis by auto
        qed
    }
    ultimately show ?thesis
      unfolding is_bisimulation_def by metis
  qed

  theorem equivalence_implies_bisimilarity: assumes "P =⋅ Q" shows "P ∼⋅ Q"
  using assms by (metis bisimilar_def equivalence_is_bisimulation)

end

end