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