Theory Eta_Bisimilarity
section ‹‹η›-Bisimilarity and ‹η›-Similarity›
theory Eta_Bisimilarity
imports Expressiveness_Price
begin
text ‹
‹η›-Bisimilarity and ‹η›-Similarity are comparably arcane notions of behavioral equivalence. We show that they are characterized by coordinates \<^term>‹E ∞ ∞ ∞ 0 0 ∞ ∞ ∞› and \<^term>‹E ∞ ∞ ∞ 0 0 ∞ 0 0› as an illustration of how to connect coordinates and relational characterizations of equivalences.
›
subsection ‹Definition and Properties of ‹η›-(Bi-)Similarity›
context lts_tau
begin
text ‹We characterize ‹η›-bisimilarity through symmetric ‹η›-simulations.›
definition eta_simulation :: ‹('s ⇒ 's ⇒ bool) ⇒ bool› where
‹eta_simulation R ≡ ∀p α p' q. R p q ⟶ p ↦ α p' ⟶
(α = τ ∧ R p' q)
∨ (∃q' q'' q'''. q ↠ q' ∧ q' ↦ α q'' ∧ q'' ↠ q''' ∧ R p q' ∧ R p' q''')›
definition eta_bisimulated :: ‹'s ⇒ 's ⇒ bool› (infix ‹~η› 40) where
‹p ~η q ≡ ∃R. eta_simulation R ∧ symp R ∧ R p q›
lemma eta_bisim_sim:
shows ‹eta_simulation (~η)›
unfolding eta_bisimulated_def eta_simulation_def by blast
lemma eta_bisim_sym:
assumes ‹p ~η q›
shows ‹q ~η p›
using assms unfolding eta_bisimulated_def
by (meson sympD)
lemma silence_retains_eta_sim:
assumes
‹eta_simulation R›
‹R p q›
‹p ↠ p'›
shows ‹∃q'. R p' q' ∧ q ↠ q'›
using assms(3,2)
proof (induct arbitrary: q)
case (refl p)
then show ?case
using silent_reachable.refl by blast
next
case (step p p' p'')
then obtain q' where ‹R p' q'› ‹q ↠ q'›
using ‹eta_simulation R› silent_reachable.refl
silent_reachable_append_τ silent_reachable_trans
unfolding eta_simulation_def by blast
then obtain q'' where ‹R p'' q''› ‹q' ↠ q''› using step by blast
then show ?case
using ‹q ↠ q'› silent_reachable_trans by blast
qed
lemma eta_bisimulated_silently_retained:
assumes
‹p ~η q›
‹p ↠ p'›
shows
‹∃q'. q ↠ q' ∧ p' ~η q'› using assms(2,1)
using silence_retains_eta_sim unfolding eta_bisimulated_def by blast
subsection ‹Logical Characterization of ‹η›-Bisimilarity through Expressiveness Price›
lemma logic_eta_bisim_invariant:
assumes
‹p0 ~η q0›
‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹p0 ⊨SRBB φ›
shows ‹q0 ⊨SRBB φ›
proof -
have ‹⋀φ χ ψ.
(∀p q. p ~η q ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
(∀p q. p ~η q ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
(∀p q. p ~η q ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
proof -
fix φ χ ψ
show
‹(∀p q. p ~η q ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
(∀p q. p ~η q ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
(∀p q. p ~η q ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct)
case TT
then show ?case by simp
next
case (Internal χ)
show ?case
proof safe
fix p q
assume case_assms:
‹p ~η q› ‹p ⊨SRBB hml_srbb.Internal χ› ‹Internal χ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
have ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
using case_assms(3) unfolding 𝒪_inner_def 𝒪_def by auto
hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ›
using Internal case_assms(1) p'_spec eta_bisimulated_silently_retained
by (meson silent_reachable_trans)
thus ‹q ⊨SRBB hml_srbb.Internal χ› by auto
qed
next
case (ImmConj I Ψ)
then show ?case unfolding 𝒪_inner_def 𝒪_def by auto
next
case (Obs α φ)
then show ?case
proof (safe)
fix p q
assume case_assms:
‹p ~η q›
‹Obs α φ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹hml_srbb_inner_models p (hml_srbb_inner.Obs α φ)›
hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› unfolding 𝒪_inner_def 𝒪_def by auto
hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
proof (cases φ)
case TT
then show ?thesis by auto
next
case (Internal _)
then show ?thesis
using silent_reachable_trans by auto
next
case (ImmConj _ _)
then show ?thesis using no_imm_conj by auto
qed
from case_assms obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
then obtain q' q'' q''' where ‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''› ‹p' ~η q'''›
using ‹p ~η q› eta_bisim_sim unfolding eta_simulation_def
using silent_reachable.refl by blast
hence ‹q''' ⊨SRBB φ›
using ‹p' ⊨SRBB φ› Obs ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by blast
hence ‹hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
using ‹q' ↦a α q''› ‹q'' ↠ q'''› back_step by auto
thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
using ‹q ↠ q'› by blast
qed
next
case (Conj I Ψ)
show ?case
proof safe
fix p q
assume case_assms:
‹p ~η q›
‹Conj I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹hml_srbb_inner_models p (Conj I Ψ)›
hence conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
unfolding 𝒪_conjunct_def 𝒪_inner_def
by (simp, metis SUP_bot_conv(1) le_zero_eq sup_bot_left sup_ge1)
from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› by auto
hence ‹∀i∈I. hml_srbb_conjunct_models q (Ψ i)›
using Conj ‹p ~η q› conj_price by blast
hence ‹hml_srbb_inner_models q (hml_srbb_inner.Conj I Ψ)› by simp
thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Conj I Ψ)›
using silent_reachable.refl by blast
qed
next
case (StableConj I Ψ)
thus ?case unfolding 𝒪_inner_def 𝒪_def by auto
next
case (BranchConj α φ I Ψ)
show ?case
proof safe
fix p q
assume case_assms:
‹p ~η q›
‹BranchConj α φ I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› unfolding 𝒪_inner_def 𝒪_def
by (simp, metis le_zero_eq sup_ge1)
hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
proof (cases φ)
case TT
then show ?thesis by auto
next
case (Internal _)
then show ?thesis
using silent_reachable_trans by auto
next
case (ImmConj _ _)
then show ?thesis using no_imm_conj by auto
qed
from case_assms have conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
unfolding 𝒪_conjunct_def 𝒪_inner_def
by (simp, metis SUP_bot_conv(1) le_zero_eq sup_bot_left sup_ge1)
from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
‹hml_srbb_inner_models p (Obs α φ)›
using branching_conj_parts branching_conj_obs by blast+
then obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
then obtain q' q'' q''' where q'_q''_spec:
‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''›
‹p ~η q'› ‹p' ~η q'''›
using eta_bisim_sim ‹p ~η q› silent_reachable.refl
unfolding eta_simulation_def by blast
hence ‹q''' ⊨SRBB φ›
using BranchConj.hyps ‹p' ⊨SRBB φ› ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by auto
hence ‹q'' ⊨SRBB φ› using back_step q'_q''_spec by blast
hence ‹hml_srbb_inner_models q' (Obs α φ)› using q'_q''_spec by auto
moreover have ‹∀i∈I. hml_srbb_conjunct_models q' (Ψ i)›
using BranchConj.hyps ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› q'_q''_spec conj_price
by blast
ultimately show ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (BranchConj α φ I Ψ)›
using ‹q ↠ q'› by auto
qed
next
case (Pos χ)
show ?case
proof safe
fix p q
assume case_assms:
‹p ~η q›
‹Pos χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹hml_srbb_conjunct_models p (Pos χ)›
hence ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
unfolding 𝒪_inner_def 𝒪_conjunct_def by simp
from case_assms obtain p' where ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
then obtain q' where ‹q ↠ q'› ‹hml_srbb_inner_models q' χ›
using Pos ‹p ~η q› ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
by (meson eta_bisimulated_silently_retained silent_reachable_trans)
thus ‹hml_srbb_conjunct_models q (Pos χ)› by auto
qed
next
case (Neg χ)
show ?case
proof safe
fix p q
assume case_assms:
‹p ~η q›
‹Neg χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
‹hml_srbb_conjunct_models p (Neg χ)›
hence ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
unfolding 𝒪_inner_def 𝒪_conjunct_def by simp
from case_assms have ‹∀p'. p ↠ p' ⟶ ¬hml_srbb_inner_models p' χ› by simp
moreover have
‹(∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)
⟶ (∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ)›
using Neg eta_bisim_sym[OF ‹p ~η q›] eta_bisimulated_silently_retained
silent_reachable_trans ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by blast
ultimately have ‹∀q'. q ↠ q' ⟶ ¬hml_srbb_inner_models q' χ› by blast
thus ‹hml_srbb_conjunct_models q (Neg χ)› by simp
qed
qed
qed
thus ?thesis using assms by blast
qed
lemma modal_eta_sim_eq: ‹eta_simulation (equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)))›
proof -
have ‹∄p α p' q. (equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞))) p q ∧ p ↦ α p' ∧
(α ≠ τ ∨ ¬(equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞))) p' q) ∧
(∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q'''
⟶ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q'
∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q''')›
proof clarify
fix p α p' q
define Qα where
‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes φ p q' ∨ distinguishes φ q' p))}›
assume contradiction:
‹equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q› ‹p ↦ α p'›
‹∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q'''
⟶ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q'
∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q'''›
‹α ≠ τ ∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q›
hence distinctions: ‹∀q'. q ↠ q' ⟶
(∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p) ∨
(∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p' q''' ∨ distinguishes φ q''' p'))›
unfolding equivalent_no_distinction
by (metis silent_reachable.cases silent_reachable.refl)
hence ‹∀q'' q''' . ∀q'∈Qα. q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
unfolding Qα_def using silent_reachable.refl by fastforce
hence ‹∀q'' q'''. q'' ↠ q''' ⟶ (∃q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'')
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
unfolding Qα_def by blast
hence ‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'' ∧ q'' ↠ q''')
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
by blast
then obtain Φα where Φα_def:
‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'' ∧ q'' ↠ q''')
⟶ (Φα q''') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)
∧ (distinguishes (Φα q''') p' q''' ∨ distinguishes (Φα q''') q''' p')› by metis
hence distinctions_α: ‹∀q'∈Qα. ∀q'' q'''.
q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ distinguishes (Φα q''') p' q''' ∨ distinguishes (Φα q''') q''' p'›
unfolding Qα_def by blast
from distinctions obtain Φη where
‹∀q'. q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)}
⟶ (distinguishes (Φη q') p q' ∨ distinguishes (Φη q') q' p)
∧ (Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
unfolding mem_Collect_eq by moura
hence
‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)}.
(distinguishes (Φη q') p q' ∨ distinguishes (Φη q') q' p)›
‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)}.
(Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
by blast+
from distinction_conjunctification_two_way[OF this(1)]
distinction_conjunctification_two_way_price[OF this]
have ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)}.
hml_srbb_conj.distinguishes (
(if distinguishes (Φη q') p q'
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φη p q') p q'
∧ (if distinguishes (Φη q') p q'
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φη p q' ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
by fastforce
then obtain Ψη where distinctions_η:
‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)}.
hml_srbb_conj.distinguishes (Ψη q') p q'
∧ Ψη q' ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
by auto
have ‹p ↦a α p'› using ‹p ↦ α p'› by simp
from distinction_combination_eta_two_way[OF this, of q Φα] distinctions_α have obs_dist:
‹∀q'∈Qα.
hml_srbb_inner.distinguishes (
Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
q''')))
) p q'›
unfolding Qα_def by fastforce
have ‹Qα ≠ {}›
using Qα_def contradiction(1) silent_reachable.refl by fastforce
hence conjunct_prices: ‹∀q'''∈{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
((if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φα p' q'''
) ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
using distinction_conjunctification_two_way_price[of
‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}›]
using Qα_def Φα_def by auto
have ‹(Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual)
Φα p' q''')) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
proof (cases ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} = {}›)
case True
then show ?thesis
unfolding 𝒪_inner_def 𝒪_conjunct_def
by (auto simp add: True bot_enat_def)
next
case False
then show ?thesis
using conjunct_prices
unfolding 𝒪_inner_def 𝒪_conjunct_def by force
qed
hence obs_price: ‹(Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual
) Φα p' q''')))) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
using distinction_conjunctification_price distinctions_α
unfolding 𝒪_inner_def 𝒪_def by simp
from obs_dist distinctions_η have
‹hml_srbb_inner_models p (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual
) Φα p' q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
using ‹Qα ≠ {}› silent_reachable.refl
unfolding hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def
by (smt (verit) Qα_def empty_Collect_eq hml_srbb_inner_models.simps(1,4) mem_Collect_eq)
moreover have ‹∀q'. q ↠ q' ⟶ ¬ hml_srbb_inner_models q'
(BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φα p'
q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
proof safe
fix q'
assume contradiction: ‹q ↠ q'›
‹hml_srbb_inner_models q' (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φα p'
q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
thus ‹False›
using obs_dist distinctions_η branching_conj_obs branching_conj_parts
unfolding distinguishes_def hml_srbb_conj.distinguishes_def
hml_srbb_inner.distinguishes_def Qα_def
by blast
qed
moreover have branch_price:
‹(BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions
else conjunctify_distinctions_dual) Φα p'
q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)
∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
using distinctions_η obs_price
unfolding Qα_def 𝒪_inner_def 𝒪_def 𝒪_conjunct_def Φα_def
by (simp, metis (mono_tags, lifting) SUP_bot_conv(2) bot_enat_def sup_bot_left)
ultimately have ‹distinguishes (Internal (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)) p q›
unfolding distinguishes_def Qα_def
using silent_reachable.refl hml_srbb_models.simps(2) by blast
moreover have ‹(Internal (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(λq'''. (if distinguishes (Φα q''') p' q'''
then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
q''')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞).
distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη))
∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
using branch_price
unfolding Qα_def 𝒪_def 𝒪_conjunct_def
by (metis (no_types, lifting) 𝒪_inner_def expr_internal_eq mem_Collect_eq)
ultimately show False using contradiction(1) equivalent_no_distinction by blast
qed
thus ?thesis
unfolding eta_simulation_def by blast
qed
theorem eta_bisim_coordinate: ‹(p ~η q) = (p ∼ (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) q)›
using modal_eta_sim_eq logic_eta_bisim_invariant sympD equivalent_no_distinction
unfolding eta_bisimulated_def expr_equiv_def distinguishes_def
by (smt (verit, best) equivalent_equiv equivpE)
subsection ‹‹η›-Similarity›
lemma logic_eta_sim_invariant:
assumes
‹∃R. eta_simulation R ∧ R p0 q0›
‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹p0 ⊨SRBB φ›
shows ‹q0 ⊨SRBB φ›
proof -
have ‹⋀φ χ ψ.
(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
proof -
fix φ χ ψ
show
‹(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
(∀p q. (∃R. eta_simulation R ∧ R p q) ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)
⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct)
case TT
then show ?case by simp
next
case (Internal χ)
show ?case
proof safe
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q› ‹p ⊨SRBB hml_srbb.Internal χ›
‹Internal χ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
have ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using case_assms(4) unfolding 𝒪_inner_def 𝒪_def by auto
hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ›
using Internal case_assms(1,2) p'_spec silence_retains_eta_sim
by (metis silent_reachable_trans)
thus ‹q ⊨SRBB hml_srbb.Internal χ› by auto
qed
next
case (ImmConj I Ψ)
then show ?case unfolding 𝒪_inner_def 𝒪_def by auto
next
case (Obs α φ)
then show ?case
proof (safe)
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q›
‹Obs α φ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹hml_srbb_inner_models p (hml_srbb_inner.Obs α φ)›
hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)› unfolding 𝒪_inner_def 𝒪_def by auto
hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
proof (cases φ)
case TT
then show ?thesis by auto
next
case (Internal _)
then show ?thesis
using silent_reachable_trans by auto
next
case (ImmConj _ _)
then show ?thesis using no_imm_conj by auto
qed
from case_assms obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
then obtain q' q'' q''' where ‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''› ‹R p' q'''›
using ‹eta_simulation R› ‹R p q› unfolding eta_simulation_def
using silent_reachable.refl by blast
hence ‹q''' ⊨SRBB φ› using ‹p' ⊨SRBB φ› Obs ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using case_assms(1) by blast
hence ‹hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
using ‹q' ↦a α q''› ‹q'' ↠ q'''› back_step by auto
thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
using ‹q ↠ q'› by blast
qed
next
case (Conj I Ψ)
show ?case
proof safe
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q›
‹Conj I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹hml_srbb_inner_models p (Conj I Ψ)›
hence conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
unfolding 𝒪_conjunct_def 𝒪_inner_def
by (simp, metis SUP_bot_conv(1) le_zero_eq sup_bot_left sup_ge1)
from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› by auto
hence ‹∀i∈I. hml_srbb_conjunct_models q (Ψ i)›
using Conj ‹eta_simulation R› ‹R p q› conj_price by blast
hence ‹hml_srbb_inner_models q (hml_srbb_inner.Conj I Ψ)› by simp
thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Conj I Ψ)›
using silent_reachable.refl by blast
qed
next
case (StableConj I Ψ)
thus ?case unfolding 𝒪_inner_def 𝒪_def by auto
next
case (BranchConj α φ I Ψ)
show ?case
proof safe
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q›
‹BranchConj α φ I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)› unfolding 𝒪_inner_def 𝒪_def
by (simp, metis le_zero_eq sup_ge1)
hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
proof (cases φ)
case TT
then show ?thesis by auto
next
case (Internal _)
then show ?thesis
using silent_reachable_trans by auto
next
case (ImmConj _ _)
then show ?thesis using no_imm_conj by auto
qed
from case_assms have conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
unfolding 𝒪_conjunct_def 𝒪_inner_def
by (simp, metis SUP_bot_conv(1) bot_enat_def bot_eq_sup_iff)
from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
‹hml_srbb_inner_models p (Obs α φ)›
using branching_conj_parts branching_conj_obs by blast+
then obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
then obtain q' q'' q''' where q'_q''_spec:
‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''›
‹R p q'› ‹R p' q'''›
using ‹eta_simulation R› ‹R p q› silent_reachable.refl
unfolding eta_simulation_def by blast
hence ‹q''' ⊨SRBB φ›
using BranchConj ‹p' ⊨SRBB φ› ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)› case_assms by auto
hence ‹q'' ⊨SRBB φ› using back_step q'_q''_spec by blast
hence ‹hml_srbb_inner_models q' (Obs α φ)› using q'_q''_spec by auto
moreover have ‹∀i∈I. hml_srbb_conjunct_models q' (Ψ i)›
using BranchConj q'_q''_spec conj_price case_assms
‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
by blast
ultimately show ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (BranchConj α φ I Ψ)›
using ‹q ↠ q'› by auto
qed
next
case (Pos χ)
show ?case
proof safe
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q›
‹Pos χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹hml_srbb_conjunct_models p (Pos χ)›
hence ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
unfolding 𝒪_inner_def 𝒪_conjunct_def by simp
from case_assms obtain p' where ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
then obtain q' where ‹q ↠ q'› ‹hml_srbb_inner_models q' χ›
using Pos case_assms ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)› silence_retains_eta_sim
by (smt (verit, ccfv_threshold) silent_reachable_trans)
thus ‹hml_srbb_conjunct_models q (Pos χ)› by auto
qed
next
case (Neg χ)
show ?case
proof safe
fix p q R
assume case_assms:
‹eta_simulation R› ‹R p q›
‹Neg χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
‹hml_srbb_conjunct_models p (Neg χ)›
hence False unfolding 𝒪_conjunct_def by auto
thus ‹hml_srbb_conjunct_models q (Neg χ)› by simp
qed
qed
qed
thus ?thesis using assms by blast
qed
lemma modal_eta_sim: ‹eta_simulation (preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)))›
proof -
have ‹∄p α p' q. (preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0))) p q ∧ p ↦ α p' ∧
(α ≠ τ ∨ ¬(preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0))) p' q) ∧
(∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q'''
⟶ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q'
∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q''')›
proof clarify
have less_obs:
‹modal_depth (E ∞ ∞ ∞ 0 0 ∞ 0 0) ≤ pos_conjuncts (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
by simp
fix p α p' q
define Qα where
‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')}›
assume contradiction:
‹preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q› ‹p ↦ α p'›
‹∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q'''
⟶ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q'
∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q'''›
‹α ≠ τ ∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q›
hence distinctions: ‹∀q'. q ↠ q' ⟶
(∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q') ∨
(∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q'''))›
unfolding preordered_no_distinction
by (metis silent_reachable.cases silent_reachable.refl)
hence ‹∀q'' q''' . ∀q'∈Qα.
q' ↦a α q'' ⟶ q'' ↠ q'''
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
unfolding Qα_def using silent_reachable.refl by fastforce
hence ‹∀q'' q'''. q'' ↠ q''' ⟶
(∃q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')
∧ q' ↦a α q'')
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
unfolding Qα_def by blast
hence ‹∀q'''. (∃q' q''. q ↠ q' ∧
(∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q') ∧ q' ↦a α q''
∧ q'' ↠ q''')
⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
by blast
then obtain Φα where Φα_def:
‹∀q'''. (∃q' q''. q ↠ q' ∧
(∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')
∧ q' ↦a α q'' ∧ q'' ↠ q''')
⟶ (Φα q''') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes (Φα q''') p' q'''›
by metis
hence distinctions_α: ‹∀q'∈Qα. ∀q'' q'''.
q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φα q''') p' q'''›
unfolding Qα_def by blast
from distinctions obtain Φη where
‹∀q'. q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')}
⟶ distinguishes (Φη q') p q' ∧ (Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
unfolding mem_Collect_eq by moura
then obtain Ψη where distinctions_η:
‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')}.
hml_srbb_conj.distinguishes (Ψη q') p q' ∧ (Ψη q')
∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using less_obs distinction_conjunctification distinction_conjunctification_price
by (smt (verit, del_insts))
have ‹p ↦a α p'› using ‹p ↦ α p'› by auto
from distinction_combination_eta[OF this] distinctions_α have obs_dist:
‹∀q'∈Qα. hml_srbb_inner.distinguishes
(Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))) p q'›
unfolding Qα_def by blast
have ‹Qα ≠ {}›
using Qα_def contradiction(1) silent_reachable.refl by fastforce
hence conjunct_prices: ‹∀q'''∈{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
(conjunctify_distinctions Φα p' q''') ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using distinction_conjunctification_price[of
‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}›]
using Qα_def Φα_def by auto
have ‹(Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
proof (cases ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} = {}›)
case True
then show ?thesis
unfolding 𝒪_inner_def 𝒪_conjunct_def
by (auto simp add: True bot_enat_def)
next
case False
then show ?thesis
using conjunct_prices
unfolding 𝒪_inner_def 𝒪_conjunct_def by force
qed
hence obs_price: ‹(Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using distinction_conjunctification_price distinctions_α
unfolding 𝒪_inner_def 𝒪_def by simp
from obs_dist distinctions_η have
‹hml_srbb_inner_models p (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
using contradiction(1) silent_reachable.refl
unfolding Qα_def by force
moreover have ‹∀q'. q ↠ q' ⟶ ¬ hml_srbb_inner_models q'
(BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
proof safe
fix q'
assume contradiction: ‹q ↠ q'›
‹hml_srbb_inner_models q' (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
thus ‹False›
using obs_dist distinctions_η
unfolding distinguishes_def hml_srbb_conj.distinguishes_def
hml_srbb_inner.distinguishes_def Qα_def
by (auto) blast+
qed
moreover have branch_price: ‹(BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)
∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using distinctions_η obs_price
unfolding Qα_def 𝒪_inner_def 𝒪_def 𝒪_conjunct_def Φα_def
by (simp, metis (mono_tags, lifting) SUP_bot_conv(2) bot_enat_def sup_bot_left)
ultimately have ‹distinguishes (Internal (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)) p q›
unfolding distinguishes_def Qα_def
using silent_reachable.refl hml_srbb_models.simps(2) by blast
moreover have ‹(Internal (BranchConj α
(Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
(conjunctify_distinctions Φα p')))
{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη))
∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
using branch_price
unfolding Qα_def 𝒪_def 𝒪_conjunct_def
by (metis (no_types, lifting) 𝒪_inner_def expr_internal_eq mem_Collect_eq)
ultimately show False using contradiction(1) preordered_no_distinction by blast
qed
thus ?thesis
unfolding eta_simulation_def by blast
qed
theorem eta_sim_coordinate:
‹(p ≼ (E ∞ ∞ ∞ 0 0 ∞ 0 0) q) = (∃R. eta_simulation R ∧ R p q)›
using modal_eta_sim logic_eta_sim_invariant unfolding expr_preord_def
by auto
end
end