Theory HML_Spectrum

section ‹Equivalence Spectrum through HML›

theory HML_Spectrum
imports
  Hennessy_Milner_Logic
  Strong_Equivalences
begin

lemma relation_currying: ‹(R1 = R2) ⟷ (∀p q. R1 p q ⟷ R2 p q)›
  by auto

context lts
begin

interpretation hml: lts_semantics where satisfies = satisfies
  by unfold_locales
interpretation hml_conj: lts_semantics where satisfies = satisfies_conj
  by unfold_locales

subsection ‹Traces›

inductive observations_traces ::
  ‹('a, 'i) hml_formula ⇒ bool›
where
  ‹observations_traces HML_true›
| ‹observations_traces φ ⟹ observations_traces (⟨α⟩φ)›

primrec observation_trace_to_trace :: ‹('a, 'i) hml_formula ⇒ 'a list›
  where
  ‹observation_trace_to_trace HML_true = []›
| ‹observation_trace_to_trace (⟨α⟩φ) = α # (observation_trace_to_trace φ)›
| ‹observation_trace_to_trace (HML_conj _ _) = []›

lemma observations_correspond_to_traces:
  assumes
    ‹observations_traces φ›
  shows
    ‹p ⊨ φ ⟷ (observation_trace_to_trace φ ∈ traces p)›
  using assms
proof (induct arbitrary: p)
  case 1
  then show ?case
    using empty_trace_trivial by force
next
  case (2 φ α)
  show ?case
  proof
    assume ‹p ⊨ ⟨α⟩φ›
    thus ‹observation_trace_to_trace (⟨α⟩φ) ∈ traces p›
      using sstep 2 by fastforce
  next
    assume ‹observation_trace_to_trace (⟨α⟩φ) ∈ traces p›
    thus ‹p ⊨ ⟨α⟩φ›
      using 2 step_sequence.cases by fastforce
  qed
qed

primrec trace_to_observation_trace :: ‹'a list ⇒ ('a, 'i) hml_formula›
  where
  ‹trace_to_observation_trace [] = HML_true›
| ‹trace_to_observation_trace (α # rest) = (⟨α⟩ (trace_to_observation_trace rest))›

lemma trace_to_observation_trace_sound:
  ‹observations_traces (trace_to_observation_trace tr)›
  by (induct tr, auto simp add: observations_traces.intros)

lemma traces_correspond_to_observations_1:
  assumes
    ‹p ⟼$ tr p'›
  shows
    ‹p ⊨ trace_to_observation_trace tr›
  using assms
proof (induct tr arbitrary: p)
  case Nil
  then show ?case by simp
next
  case (Cons a tr)
  then show ?case
    by (metis list.discI list.inject satisfies.simps(3) step_sequence.cases trace_to_observation_trace.simps(2))
qed

lemma traces_correspond_to_observations_2:
  assumes
    ‹p ⊨ trace_to_observation_trace tr›
  shows
    ‹tr ∈ traces p›
  using assms
proof (induct tr arbitrary: p)
  case Nil
  show ?case using empty_trace_trivial .
next
  case (Cons a tr)
  then show ?case
    using sstep by fastforce
qed
 
lemma trace_preorder_implies_observations_preorder:
  assumes
    ‹p ≲T q›
  shows
    ‹hml.preordered (Collect observations_traces) p q›
  unfolding hml.preordered_no_distinction
proof safe
  fix φ
  assume ‹observations_traces φ› ‹p ⊨ φ› ‹¬ q ⊨ φ›
  hence ‹observation_trace_to_trace φ ∈ traces p›
    using observations_correspond_to_traces by blast
  hence ‹observation_trace_to_trace φ ∈ traces q›
    using assms unfolding trace_preordered_def ..
  thus False
    using ‹¬ q ⊨ φ› observations_correspond_to_traces[OF ‹observations_traces φ›] by blast
qed

lemma trace_observations_preorder_implies_trace_preorder:
  assumes
    ‹hml.preordered (Collect observations_traces) p q›
  shows
    ‹p ≲T q›
  unfolding trace_preordered_def
proof
  fix tr
  assume ‹tr ∈ traces p›
  hence ‹p ⊨ trace_to_observation_trace tr›
    using traces_correspond_to_observations_1 by auto
  hence ‹q ⊨ trace_to_observation_trace tr›
    using trace_to_observation_trace_sound assms  by blast
  thus ‹tr ∈ traces q›
    using traces_correspond_to_observations_2 by auto
qed

theorem observations_traces_characterizes_trace_preorder:
  ‹(≲T) = hml.preordered (Collect observations_traces)›
  using trace_preorder_implies_observations_preorder
    trace_observations_preorder_implies_trace_preorder
  unfolding relation_currying
  by blast

subsection ‹Simulation›

inductive
  observations_simulation :: ‹('a, 's) hml_formula ⇒ bool› and
  observations_simulation_conj ::‹('a, 's) hml_conjunct ⇒ bool›
where
  ‹observations_simulation HML_true›
| ‹observations_simulation φ ⟹ observations_simulation (⟨α⟩φ)›
| ‹I ≠ {} ⟹ (⋀i. i ∈ I ⟹ observations_simulation_conj (F i)) ⟹ observations_simulation (AND I F)›
| ‹observations_simulation φ ⟹ observations_simulation_conj (HML_pos (⟨α⟩φ))›

inductive
  observations_simulation_game :: ‹('a, 's) hml_formula ⇒ bool› and
  observations_simulation_game_conj ::‹('a, 's) hml_conjunct ⇒ bool›
  where
  ‹observations_simulation_game (⟨α⟩HML_true)›
| ‹I ≠ {} ⟹ (⋀i. i ∈ I ⟹ observations_simulation_game_conj (F i)) ⟹ observations_simulation_game (⟨α⟩(AND I F))›
| ‹φ ≠ HML_true ⟹ observations_simulation_game φ ⟹ observations_simulation_game_conj (HML_pos (φ))›

lemma observations_simulation_sim:
  shows ‹simulation (hml.preordered (Collect observations_simulation_game))›
  unfolding simulation_def
proof (safe, rule ccontr)
  fix p q a p'
  assume assm:
    ‹p ⟼a p'›
    ‹hml.preordered (Collect observations_simulation_game) p q›
    ‹∄q'. q ⟼a q' ∧ hml.preordered (Collect observations_simulation_game) p' q'›
  show False
  proof (cases ‹derivatives q a = {}›)
    case True
    hence ‹(p ⊨ ⟨a⟩HML_true) ∧ ¬(q ⊨ ⟨a⟩HML_true)›
      using assm(1) by auto
    moreover have ‹observations_simulation_game (⟨a⟩HML_true)›
      using lts.observations_simulation_game.simps by blast
    ultimately show False using assm by blast
  next
    case False
    define φd where ‹φd ≡ AND (derivatives q a) (λq'. HML_pos
      (SOME φ. φ ∈ Collect observations_simulation_game ∧ hml.distinguishes φ p' q'))›
    from assm have distinctions: ‹∀q' ∈ derivatives q a.
        ∃φ. φ ∈ Collect observations_simulation_game ∧ hml.distinguishes φ p' q'›
      using hml.preordered_no_distinction by blast
    hence ‹p' ⊨ φd ∧ (∀q' ∈ derivatives q a. ¬ q' ⊨ φd)›
      unfolding φd_def by auto (smt (verit, best) someI2_ex)+
    with ‹p ⟼a p'› have ‹hml.distinguishes (⟨a⟩φd) p q› by auto
    from distinctions have
        ‹∀q'. q' ∈ derivatives q a ⟶ observations_simulation_game
      (SOME φ. φ ∈ Collect observations_simulation_game ∧ hml.distinguishes φ p' q')›
      by auto (smt (verit, best) someI2_ex)+
    hence
        ‹∀q'. q' ∈ derivatives q a ⟶ observations_simulation_game_conj
      (+ (SOME φ. φ ∈ Collect observations_simulation_game ∧ hml.distinguishes φ p' q'))›
      using lts.observations_simulation_game.simps observations_simulation_game_conj.simps by force
    thus ‹False› using assm(2)
      using ‹hml.distinguishes (⟨a⟩φd) p q› False assm(2)
      unfolding φd_def
      by (metis (no_types, lifting) mem_Collect_eq observations_simulation_game_observations_simulation_game_conj.intros(2))
  qed
qed

lemma observations_simulation_game_invariant:
  ‹(observations_simulation_game φ ⟶ (∀p q. p ≲S q ⟶ p ⊨ φ ⟶ q ⊨ φ)) ∧
   (observations_simulation_game_conj ψ ⟶ (∀p q. p ≲S q ⟶ satisfies_conj p ψ ⟶ satisfies_conj q ψ))›
proof (induct rule: observations_simulation_game_observations_simulation_game_conj.induct)
  case (1 α)
  then show ?case
    by (meson lts.observations_correspond_to_traces lts.observations_traces.intros(1) lts.trace_preordered_def observations_traces.intros(2) sim_implies_trace_preord subsetD)
next
  case (2 I Ψ α)
  then show ?case
    by (smt (verit, ccfv_threshold) satisfies.simps(2) satisfies.simps(3) simulated_by_def simulation_def) 
next
  case (3 φ)
  then show ?case
    by auto
qed

theorem observations_simulation_game_characterize_simulation_preorder:
  shows ‹(≲S) = hml.preordered (Collect observations_simulation_game)›
  using observations_simulation_sim observations_simulation_game_invariant
    hml.preordered_no_distinction simulated_by_def
  unfolding relation_currying
  by (smt (verit, best) mem_Collect_eq)

thm observations_simulation_game_observations_simulation_game_conj.induct

lemma observations_simulation_game_are_positive:
  shows ‹(Collect observations_simulation_game) ⊆ (Collect observations_simulation) ∧
    (Collect observations_simulation_game_conj) ⊆ (Collect observations_simulation_conj)›
proof -
  have ‹⋀φ ψ. (observations_simulation_game φ ⟶ observations_simulation φ) ∧
      (observations_simulation_game_conj ψ ⟶ observations_simulation_conj ψ)›
  proof -
    fix φ::‹('a, 's) hml_formula› and ψ::‹('a, 's) hml_conjunct›
    show ‹(observations_simulation_game φ ⟶ observations_simulation φ) ∧
      (observations_simulation_game_conj ψ ⟶ observations_simulation_conj ψ)›
    proof (induct rule: observations_simulation_game_observations_simulation_game_conj.induct)
      case (1 α)
      then show ?case
        by (simp add: observations_simulation_observations_simulation_conj.intros)
    next
      case (2 I F α)
      then show ?case
        using observations_simulation_observations_simulation_conj.intros by blast
    next
      case (3 φ)
      then show ?case
        by (metis hml_formula.distinct(5) observations_simulation.simps observations_simulation_game.cases observations_simulation_observations_simulation_conj.intros(4))
    qed
  qed
  thus ?thesis by blast
qed

lemma observations_simulation_matches_observations_simulation_game:
  shows ‹hml.leq_distinctive (Collect observations_simulation) (Collect observations_simulation_game)›
proof -
  have ‹⋀φ ψ.
    (observations_simulation φ ⟶ (∀p q. hml.distinguishes φ p q
      ⟶ (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p q))) ∧
    (observations_simulation_conj ψ ⟶ (∀p q. hml_conj.distinguishes ψ p q
      ⟶ (∃ψ'. observations_simulation_game_conj ψ' ∧ hml_conj.distinguishes ψ' p q)))›
  proof -
    fix φ::‹('a, 's) hml_formula› and ψ::‹('a, 's) hml_conjunct›
    show
      ‹(observations_simulation φ ⟶ (∀p q. hml.distinguishes φ p q
        ⟶ (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p q))) ∧
      (observations_simulation_conj ψ ⟶ (∀p q. hml_conj.distinguishes ψ p q
        ⟶ (∃ψ'. observations_simulation_game_conj ψ' ∧ hml_conj.distinguishes ψ' p q)))›
    proof (induct rule: observations_simulation_observations_simulation_conj.induct)
      case 1
      then show ?case by simp
    next
      case (2 φ α)
      then show ?case
      proof safe
        fix p q
        assume case_assms: ‹observations_simulation φ›
           ‹∀p q. hml.distinguishes φ p q ⟶ (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p q)›
           ‹p ⊨ ⟨α⟩φ› ‹¬ q ⊨ ⟨α⟩φ›
        from case_assms(3,4) obtain p' where p'_spec: ‹p ⟼ α p'› ‹p' ⊨ φ› ‹∀q' ∈ derivatives q  α. ¬q' ⊨ φ› by auto
        thus ‹∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p q›
        proof (cases ‹derivatives q α = {}›)
          case True
          hence ‹hml.distinguishes (⟨α⟩HML_true) p q› using case_assms by auto
          moreover have ‹observations_simulation_game (⟨α⟩HML_true)›
            by (simp add: observations_simulation_game.simps
                  observations_simulation_game_observations_simulation_game_conj.intros(3))
          ultimately show ?thesis by blast
        next
          case False
          define φd where ‹φd ≡
            AND (derivatives q α) (λq'. +(SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q'))›
          have ‹∀q' ∈ derivatives q  α. hml.distinguishes φ p' q'›
            using p'_spec by auto
          then have distinctions: ‹∀q' ∈ derivatives q α.
            (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using case_assms by blast
          then have main_distinction: ‹∀q' ∈ derivatives q  α.
            (hml.distinguishes φd p' q')›
            unfolding φd_def by auto (smt (verit, best) someI2_ex)+
          from distinctions have
            ‹∀q' ∈ derivatives q  α. observations_simulation_game
              (SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using someI2_ex by smt
          hence ‹∀q' ∈ derivatives q  α. observations_simulation_game_conj
              (+(SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q'))›
            by (metis (no_types, lifting) hml_formula.distinct(3) observations_simulation_game.cases
                observations_simulation_game_observations_simulation_game_conj.intros(3))
          hence ‹observations_simulation_game (⟨α⟩φd)›
            unfolding φd_def
            by (metis (no_types, lifting) False observations_simulation_game_observations_simulation_game_conj.intros(2))
          moreover have ‹hml.distinguishes (⟨α⟩φd) p q›
            using main_distinction φd_def p'_spec(1) by auto
          ultimately show ?thesis
            using observations_simulation_game_observations_simulation_game_conj.intros(3)
              satisfies_conj.simps(1) by blast
        qed
      qed
    next
      case (3 I F)
      then show ?case
        by (smt (verit, best) mem_Collect_eq observations_simulation_game_characterize_simulation_preorder observations_simulation_game_invariant satisfies.simps(2))
    next
      case (4 φ α)
      then show ?case
      proof safe
        fix p q
        assume case_assms: ‹observations_simulation φ›
           ‹∀p q. hml.distinguishes φ p q ⟶ (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p q)›
           ‹satisfies_conj p (+⟨α⟩φ)› ‹¬ satisfies_conj q (+⟨α⟩φ)›
        from case_assms(3,4) obtain p' where p'_spec: ‹p ⟼ α p'› ‹p' ⊨ φ› ‹∀q' ∈ derivatives q  α. ¬q' ⊨ φ› by auto
        thus ‹∃ψ'. observations_simulation_game_conj ψ' ∧ hml_conj.distinguishes ψ' p q›
        proof (cases ‹derivatives q α = {}›)
          case True
          hence ‹hml_conj.distinguishes (+⟨α⟩HML_true) p q› using case_assms by auto
          moreover have ‹observations_simulation_game_conj (+⟨α⟩HML_true)›
            by (simp add: observations_simulation_game.simps
                  observations_simulation_game_observations_simulation_game_conj.intros(3))
          ultimately show ?thesis by blast
        next
          case False
          define φd where ‹φd ≡
            AND (derivatives q α) (λq'. +(SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q'))›
          have ‹∀q' ∈ derivatives q  α. hml.distinguishes φ p' q'›
            using p'_spec by auto
          then have distinctions: ‹∀q' ∈ derivatives q α.
            (∃φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using case_assms by blast
          then have main_distinction: ‹∀q' ∈ derivatives q  α.
            (hml.distinguishes φd p' q')›
            unfolding φd_def by auto (smt (verit, best) someI2_ex)+
          from distinctions have
            ‹∀q' ∈ derivatives q  α. observations_simulation_game
              (SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using someI2_ex by smt
          hence ‹∀q' ∈ derivatives q  α. observations_simulation_game_conj
              (+(SOME φ'. observations_simulation_game φ' ∧ hml.distinguishes φ' p' q'))›
            by (metis (no_types, lifting) hml_formula.distinct(3) observations_simulation_game.cases
                observations_simulation_game_observations_simulation_game_conj.intros(3))
          hence ‹observations_simulation_game (⟨α⟩φd)›
            unfolding φd_def
            by (metis (no_types, lifting) False observations_simulation_game_observations_simulation_game_conj.intros(2))
          moreover have ‹hml.distinguishes (⟨α⟩φd) p q›
            using main_distinction φd_def p'_spec(1) by auto
          ultimately show ?thesis
            using observations_simulation_game_observations_simulation_game_conj.intros(3)
              satisfies_conj.simps(1) by blast
        qed
      qed
    qed
  qed
  thus ?thesis
    unfolding hml.leq_distinctive_def by simp
qed

theorem observations_simulation_characterize_simulation_preorder:
  ‹(≲S) = hml.preordered (Collect observations_simulation)›
  using
    observations_simulation_game_characterize_simulation_preorder
    hml.preorder_distinctiveness_contraposition
    observations_simulation_game_are_positive
    observations_simulation_matches_observations_simulation_game
    hml.subset_distinctiveness
  unfolding relation_currying
  by meson

subsection ‹Hennessy–Milner Theorem of Modal Logic and Bisimilarity›

lemma hml_equiv_sim:
  shows ‹simulation (hml.equivalent UNIV)›
  unfolding simulation_def 
proof (safe, rule ccontr)
  fix p q a p'
  define φd where ‹φd ≡ AND (derivatives q a) (λq'. HML_pos (SOME φ. hml.distinguishes φ p' q'))›
  assume assm:
    ‹p ⟼a p'›
    ‹hml.equivalent UNIV p q›
    ‹∄q'. q ⟼a q' ∧ hml.equivalent UNIV p' q'›
  hence distinctions: ‹∀q' ∈ derivatives q a. ∃φ. hml.distinguishes φ p' q'›
    using hml_distinctions by blast
  hence ‹p' ⊨ φd ∧ (∀q' ∈ derivatives q a. ¬ q' ⊨ φd)›
    unfolding φd_def by auto (smt (verit, best) someI2_ex)+
  with ‹p ⟼a p'› have ‹(p ⊨ ⟨a⟩φd) ∧ ¬(q ⊨ ⟨a⟩φd)› by auto
  thus ‹False› using ‹hml.equivalent UNIV p q›
    unfolding hml.equivalent_def by blast
qed

lemma hml_bisim_invariant:
  ‹⋀p q. p ≃B q ⟹ p ⊨ φ ⟹ q ⊨ φ›
  ‹⋀p q. p ≃B q ⟹ satisfies_conj p ψ ⟹ satisfies_conj q ψ›
proof (induct φ and ψ)
  case HML_true
  then show ?case by auto
next
  case (HML_conj I F)
  then show ?case by auto
next
  case (HML_obs α φ)
  then obtain p' q' where ‹p ⟼α p'› ‹p' ⊨ φ› ‹q ⟼α q'› ‹bisimilar p' q'›
    using bisim_sim unfolding simulation_def by (meson satisfies.simps(3))
  then show ?case using HML_obs by auto
next
  case (HML_pos φ)
  hence ‹bisimilar q p› unfolding bisimilar_def symp_def by blast
  then show ?case using HML_pos by auto
next
  case (HML_neg φ)
  hence ‹bisimilar q p› unfolding bisimilar_def symp_def by blast
  then show ?case using HML_neg by auto
qed

theorem Hennessy_Milner_theorem:
  shows ‹(≃B) = hml.equivalent UNIV›
  using hml_bisim_invariant hml_equiv_sim hml_distinctions distinguishes_invertible
    equivp_reflp_symp_transp hml.equivalent_equiv
  unfolding relation_currying bisimilar_def
  by meson

inductive
  observations_bisimulation_game :: ‹('a, 's) hml_formula ⇒ bool› and
  observations_bisimulation_game_conj ::‹('a, 's) hml_conjunct ⇒ bool›
  where
  ‹observations_bisimulation_game (⟨α⟩HML_true)›
| ‹I ≠ {} ⟹ (⋀i. i ∈ I ⟹ observations_bisimulation_game_conj (F i)) ⟹ observations_bisimulation_game (⟨α⟩(AND I F))›
| ‹φ ≠ HML_true ⟹ observations_bisimulation_game φ ⟹ observations_bisimulation_game_conj (HML_pos φ)›
| ‹φ ≠ HML_true ⟹ observations_bisimulation_game φ ⟹ observations_bisimulation_game_conj (HML_neg φ)›
| ‹observations_bisimulation_game φ ⟹ observations_bisimulation_game (HML_conj_neg φ)›

lemma observations_bisimulation_game_conj_neg:
  assumes ‹observations_bisimulation_game_conj (HML_neg φ)›
  shows ‹observations_bisimulation_game φ›
  using assms observations_bisimulation_game_conj.cases by auto

lemma observations_bisimulation_game_conj_pos:
  assumes ‹observations_bisimulation_game_conj (HML_pos φ)›
  shows ‹observations_bisimulation_game φ›
  using assms observations_bisimulation_game_conj.cases by auto

lemma observations_bisimulation_game_match_hml:
  shows ‹hml.leq_distinctive (UNIV) (Collect observations_bisimulation_game)›
proof -
  have ‹⋀φ ψ.
    (∀p q. hml.distinguishes φ p q
      ⟶ (∃φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p q)) ∧
    (∀p q. hml_conj.distinguishes ψ p q
      ⟶ (∃ψ'. observations_bisimulation_game_conj ψ' ∧ hml_conj.distinguishes ψ' p q))›
  proof -
    fix φ::‹('a, 's) hml_formula› and ψ::‹('a, 's) hml_conjunct›
    show ‹(∀p q. hml.distinguishes φ p q
        ⟶ (∃φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p q)) ∧
      (∀p q. hml_conj.distinguishes ψ p q
        ⟶ (∃ψ'. observations_bisimulation_game_conj ψ' ∧ hml_conj.distinguishes ψ' p q))›
    proof (induct rule: hml_formula_hml_conjunct.induct)
      case HML_true
      then show ?case by auto
    next
      case (HML_conj I Ψ)
      show ?case
      proof safe
        fix p q
        assume ‹p ⊨ AND I Ψ› ‹¬ q ⊨ AND I Ψ›
        then obtain i where i_spec: ‹i∈I› ‹hml_conj.distinguishes (Ψ i) p q› by auto
        with HML_conj obtain ψ' where ψ'_spec:
          ‹observations_bisimulation_game_conj ψ'› ‹hml_conj.distinguishes ψ' p q› by blast
        show ‹∃φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p q›
        proof (cases ψ')
          case (HML_pos φ')
          thus ?thesis
            using ψ'_spec observations_bisimulation_game_conj_pos by auto
        next
          case (HML_neg φ')
          hence ‹observations_bisimulation_game φ' ∧ hml.distinguishes φ' q p›
            using ψ'_spec observations_bisimulation_game_conj_neg by auto
          hence ‹observations_bisimulation_game (HML_conj_neg φ')›
            ‹hml.distinguishes (HML_conj_neg φ') p q›
            using lts.observations_bisimulation_game.simps by fastforce+
          then show ?thesis by blast
        qed
      qed
    next
      case (HML_obs α φ)
      show ?case
      proof safe
        fix p q
        assume case_assms: ‹p ⊨ ⟨α⟩φ› ‹¬ q ⊨ ⟨α⟩φ›
        then obtain p' where p'_spec:
          ‹p ⟼ α p'› ‹p' ⊨ φ› ‹∀q'. q ⟼ α q' ⟶ hml.distinguishes φ p' q'› by auto
        thus ‹∃φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p q›
        proof (cases ‹derivatives q α = {}›)
          case True
          hence ‹hml.distinguishes (⟨α⟩HML_true) p q› using case_assms by auto
          moreover have ‹observations_bisimulation_game (⟨α⟩HML_true)›
            by (simp add: observations_bisimulation_game_observations_bisimulation_game_conj.intros(1))
          ultimately show ?thesis by blast
        next
          case False
          define φd where ‹φd ≡
            AND (derivatives q α) (λq'. +(SOME φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p' q'))›
          have ‹∀q' ∈ derivatives q  α. hml.distinguishes φ p' q'›
            using p'_spec by auto
          then have distinctions: ‹∀q' ∈ derivatives q α.
            (∃φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using HML_obs by blast
          then have main_distinction: ‹∀q' ∈ derivatives q α.
            (hml.distinguishes φd p' q')›
            unfolding φd_def by auto (smt (verit, best) someI2_ex)+
          from distinctions have
            ‹∀q' ∈ derivatives q  α. observations_bisimulation_game
              (SOME φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p' q')›
            using someI2_ex by smt
          hence ‹∀q' ∈ derivatives q  α. observations_bisimulation_game_conj
              (+(SOME φ'. observations_bisimulation_game φ' ∧ hml.distinguishes φ' p' q'))›
            using lts.observations_bisimulation_game.cases lts.observations_bisimulation_game_conj.simps by fastforce
          hence ‹observations_bisimulation_game (⟨α⟩φd)›
            unfolding φd_def
            by (meson False observations_bisimulation_game_observations_bisimulation_game_conj.intros(2))
          moreover have ‹hml.distinguishes (⟨α⟩φd) p q›
            using main_distinction φd_def p'_spec(1) by auto
          ultimately show ?thesis
            using observations_simulation_game_observations_simulation_game_conj.intros(3)
              satisfies_conj.simps(1) by blast
        qed
      qed
    next
      case (HML_pos φ)
      then show ?case
        by (metis observations_bisimulation_game_conj.simps satisfies.simps(1) satisfies_conj.simps(1))
    next
      case (HML_neg φ)
      then show ?case
        by (metis lts.observations_bisimulation_game_observations_bisimulation_game_conj.intros(4) satisfies.simps(1) satisfies_conj.simps(2))
    qed
  qed
  thus ?thesis unfolding hml.leq_distinctive_def by blast
qed

theorem hml_and_bisimulation_game_observations_equally_expressive:
  ‹hml.eq_distinctive (UNIV) (Collect observations_bisimulation_game)›
  using observations_bisimulation_game_match_hml hml.subset_distinctiveness by auto

end

end