Theory Bisimilarity_Implies_Equivalence

theory Bisimilarity_Implies_Equivalence
imports
  Logical_Equivalence
begin

section ‹Bisimilarity Implies Logical Equivalence›

context indexed_nominal_ts
begin

  lemma bisimilarity_implies_equivalence_Act:
    assumes "⋀P Q. P ∼⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
    and "P ∼⋅ Q"
    and "P ⊨ Act α x"
    shows "Q ⊨ Act α x"
  proof -
    have "finite (supp Q)"
      by (fact finite_supp)
    with ‹P ⊨ Act α x› obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* Q"
      by (metis valid_Act_strong)

    from ‹P ∼⋅ Q› and fresh and trans obtain Q' where trans': "Q → ⟨α',Q'⟩" and bisim': "P' ∼⋅ Q'"
      by (metis bisimilar_simulation_step)

    from eq obtain p where px: "x' = p ∙ x"
      by (metis Act_eq_iff_perm)

    with valid have "-p ∙ P' ⊨ x"
      by (metis permute_minus_cancel(1) valid_eqvt)
    moreover from bisim' have "(-p ∙ P') ∼⋅ (-p ∙ Q')"
      by (metis bisimilar_eqvt)
    ultimately have "-p ∙ Q' ⊨ x"
      using ‹⋀P Q. P ∼⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis
    with px have "Q' ⊨ x'"
      by (metis permute_minus_cancel(1) valid_eqvt)

    with eq and trans' show "Q ⊨ Act α x"
      unfolding valid_Act by metis
  qed

  theorem bisimilarity_implies_equivalence: assumes "P ∼⋅ Q" shows "P =⋅ Q"
  unfolding logically_equivalent_def proof
    fix x :: "('idx, 'pred, 'act) formula"
    from assms show "P ⊨ x ⟷ Q ⊨ x"
    proof (induction x arbitrary: P Q)
      case (Conj xset) then show ?case
        by simp
    next
      case Not then show ?case
        by simp
    next
      case Pred then show ?case
        by (metis bisimilar_is_bisimulation is_bisimulation_def symp_def valid_Pred)
    next
      case (Act α x) then show ?case
        by (metis bisimilar_symp bisimilarity_implies_equivalence_Act sympE)
    qed
  qed

end

end