Theory Weak_Bisimilarity_Implies_Equivalence

theory Weak_Bisimilarity_Implies_Equivalence
imports
  Weak_Logical_Equivalence
begin

section ‹Weak Bisimilarity Implies Weak Logical Equivalence›

context indexed_weak_nominal_ts
begin

  lemma weak_bisimilarity_implies_weak_equivalence_Act:
    assumes "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
    and "P ≈⋅ Q"
    ― ‹not needed: and @{prop "weak_formula x"}›
    and "P ⊨ ⟨⟨α⟩⟩x"
    shows "Q ⊨ ⟨⟨α⟩⟩x"
  proof -
    have "finite (supp Q)"
      by (fact finite_supp)
    with ‹P ⊨ ⟨⟨α⟩⟩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_weak_action_modality_strong)

    from ‹P ≈⋅ Q› and fresh and trans obtain Q' where trans': "Q ⇒⟨α'⟩ Q'" and bisim': "P' ≈⋅ Q'"
      by (metis weakly_bisimilar_weak_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 weakly_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 ⊨ ⟨⟨α⟩⟩x"
      unfolding valid_weak_action_modality by metis
  qed

  lemma weak_bisimilarity_implies_weak_equivalence_Pred:
    assumes "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
    and "P ≈⋅ Q"
    ― ‹not needed: and @{prop "weak_formula x"}›
    and "P ⊨ ⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton x)))"
    shows "Q ⊨ ⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton x)))"
  proof -
    let ?c = "Conj (binsert (Pred φ) (bsingleton x))"

    from ‹P ⊨ ⟨⟨τ⟩⟩?c› obtain P' where trans: "P ⇒ P'" and valid: "P' ⊨ ?c"
      using valid_weak_action_modality by auto

    have "bn τ  ♯* Q"
      by (simp add: fresh_star_def)
    with ‹P ≈⋅ Q› and trans obtain Q' where trans': "Q ⇒ Q'" and bisim': "P' ≈⋅ Q'"
      by (metis weakly_bisimilar_weak_simulation_step weak_transition_tau_iff)

    from valid have *: "P' ⊢ φ" and **: "P' ⊨ x"
      by (simp add: binsert.rep_eq)+

    from bisim' and * obtain Q'' where trans'': "Q' ⇒ Q''" and bisim'': "P' ≈⋅ Q''" and ***: "Q'' ⊢ φ"
      by (metis is_weak_bisimulation_def weakly_bisimilar_is_weak_bisimulation)

    from bisim'' and ** have "Q'' ⊨ x"
      using ‹⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis
    with *** have "Q'' ⊨ ?c"
      by (simp add: binsert.rep_eq)

    moreover from trans' and trans'' have "Q ⇒⟨τ⟩ Q''"
      by (metis tau_transition_trans weak_transition_tau_iff)

    ultimately show "Q ⊨ ⟨⟨τ⟩⟩?c"
      unfolding valid_weak_action_modality by metis
  qed

  theorem weak_bisimilarity_implies_weak_equivalence: assumes "P ≈⋅ Q" shows "P ≡⋅ Q"
  proof -
  {
    fix x :: "('idx, 'pred, 'act) formula"
    assume "weak_formula x"
      then have "⋀P Q. P ≈⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x"
    proof (induct rule: weak_formula.induct)
      case (wf_Conj xset) then show ?case
        by simp
    next
      case (wf_Not x) then show ?case
        by simp
    next
      case (wf_Act x α) then show ?case
        by (metis weakly_bisimilar_symp weak_bisimilarity_implies_weak_equivalence_Act sympE)
    next
      case (wf_Pred x φ) then show ?case
        by (metis weakly_bisimilar_symp weak_bisimilarity_implies_weak_equivalence_Pred sympE)
      qed
    }
    with assms show ?thesis
      unfolding weakly_logically_equivalent_def by simp
  qed

end

end