Theory Reduction_of_Satisfaction

(*<*)
theory Reduction_of_Satisfaction
  imports
    Mapping_for_Formulas
begin
(*>*)

section ‹Reduction of Formula Satisfaction›
text ‹\label{sec:reduction_satisfaction}›

text ‹We will show that, for a process $p$ of an \LTSt{} and a formula $\varphi$ of \HMLt{}, we have $p \vDash \varphi \iff \vartheta(p) \vDash \sigma(\varphi)$ and $p \vDash_X \varphi \iff \vartheta_X(p) \vDash \sigma(\varphi)$. The proof is rather straightforward: we use induction over \HMLt{} formulas and show that, for each case, the semantics given by van~Glabbeek's satisfaction relations and those given by the mappings $\sigma$ and $\vartheta$/$\vartheta_X$ coincide. Due to the relative complexity of the mapping and the satisfaction relations, the proof is quite tedious, however.
\vspace{-.3cm}›


subsection ‹Isabelle›

text ‹\vspace{-.4cm}
Similarly to the formalisations in \cref{sec:reduction_bisimilarity}, we begin by interpreting our transition mapping ‹tran_theta› as an ‹lts› and reassigning notation appropriately (we only care about HML formula satisfaction for $\mathbb{T}_\vartheta$, not $\mathbb{T}$).›

context lts_timeout_mappable begin

interpretation lts_theta: lts tran_theta .
no_notation local.HML_sat ("_ ⊨ _" [50, 50] 50)
notation lts_theta.HML_sat ("_ ⊨ _" [50, 50] 50)

text ‹We show ‹p ⊫?[XoN] φ  ⟺  θ?[XoN](p) ⊨ σ(φ)› by induction over ‹φ›. By using those terms for formula satisfaction and process mappings that handle both triggered and stable environments, we can handle both situations simultaneously, which is required due to the interdependence of $\vDash$ and $\vDash_X$. However, this requires us to consider four cases (each combination of ‹⊫?[XoN⇩1]› and ‹θ?[XoN⇩2]› for ‹XoN⇩1, XoN⇩2 ∈ {None, Some X}›%
\footnote{Once again, we only consider cases where ‹X ⊆ visible_actions›.}%
) per inductive case for ‹φ›. Together with the many disjunctive clauses in the mapping, a large number of cases needs to be considered, leading to a proof spanning roughly 350 lines of Isabelle code.›

(* These lemmas are not important for the thesis document. *)
(*<*)
lemma✐‹tag (proof) unimportant› sat_poss_alpha_not_special:
  assumes 
    ‹no_special_action α›
    ‹P ⊨ φ'›
    ‹φ' ∈ {HML_poss α σ(φ), 
          HML_poss (ε[visible_actions]) (HML_poss α σ(φ)),
          HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))}› (is ‹φ' ∈ ?disj›)
  shows
    ‹P ⊨ σ(HMLt_poss α φ)›
proof -
  from assms(3) have ‹cin φ' (acset ?disj)› 
    by (simp add: cin.abs_eq eq_onp_same_args)
  with assms(2) have ‹P ⊨ (HML_disj (acset ?disj))› using HML_sat_disj by auto
  with HMt_mapping.simps(4)[OF assms(1)] show ?thesis by simp
qed

lemma✐‹tag (proof) unimportant› sat_time_forward:
  assumes 
    ‹X ⊆ visible_actions›
    ‹P ⊨ φ'›
    ‹φ' ∈ {HML_poss (ε[X]) (HML_poss t σ(φ)),
          HML_poss t_ε (HML_poss (ε[X]) (HML_poss t σ(φ)))}› (is ‹φ' ∈ ?disj›)
  shows
    ‹P ⊨ σ(HMLt_time X φ)›
proof -
  from assms(3) have ‹cin φ' (acset ?disj)› 
    by (simp add: cin.abs_eq eq_onp_same_args)
  with assms(2) have ‹P ⊨ (HML_disj (acset ?disj))› using HML_sat_disj by auto
  with HMt_mapping.simps(6)[OF assms(1)] show ?thesis by simp
qed

lemma✐‹tag (proof) unimportant› sat_time_backward:
  assumes 
    ‹θ?[XoN](p) ⊨ σ(HMLt_time Y φ)›
  shows 
    ‹Y ⊆ visible_actions ∧ (θ?[XoN](p) ⊨ HML_poss (ε[Y]) (HML_poss t σ(φ)) ∨
    θ?[XoN](p) ⊨ HML_poss t_ε (HML_poss (ε[Y]) (HML_poss t σ(φ))))›
proof -
  have ‹Y ⊆ visible_actions›
  proof (rule ccontr)
    assume ‹¬ Y ⊆ visible_actions›
    with assms have ‹θ?[XoN](p) ⊨ HML_false› by simp
    thus False using lts_theta.HML_sat_false by fast
  qed
  let ?disj = ‹{HML_poss (ε[Y]) (HML_poss t σ(φ)), 
    HML_poss t_ε (HML_poss (ε[Y]) (HML_poss t σ(φ)))}›
  from assms have ‹θ?[XoN](p) ⊨ HML_disj (acset ?disj)› 
    using HMt_mapping.simps(6)[OF ‹Y ⊆ visible_actions›] by simp
  then obtain φ' where ‹cin φ' (acset ?disj)› ‹θ?[XoN](p) ⊨ φ'› 
    using lts_theta.HML_sat_disj by blast
  from ‹cin φ' (acset ?disj)› have ‹φ' ∈ ?disj›
    by (simp add: cin.abs_eq eq_onp_same_args)
  with ‹θ?[XoN](p) ⊨ φ'› ‹Y ⊆ visible_actions› show ?thesis
    by fastforce
qed

lemma✐‹tag (proof) unimportant› triggered_env_cannot_timeout: 
  ‹⋀ φ. ¬ θ(p) ⊨ HML_poss t_ε φ› using generation_triggered_transitions
  using distinctness_special_actions(2,6) by force

lemma✐‹tag (proof) unimportant› stable_env_cannot_stabilise: 
  ‹⋀ φ. ¬ θ[X](p) ⊨ HML_poss (ε[Y]) φ›
  using generation_stable_transitions distinctness_special_actions(6) 
    no_epsilon_in_tran(1) lts_theta.HML_sat.simps(3) by meson
(*>*)

lemma HMLt_sat_iff_HML_sat:
  assumes ‹XoN = None ∨ (XoN = (Some X) ∧ X ⊆ visible_actions)›
  shows ‹p ⊫?[XoN] φ  ⟺  θ?[XoN](p) ⊨ σ(φ)›
  using assms
proof (induct φ arbitrary: p XoN X)
  case (HMLt_conj Φ)
  from HMLt_conj.prems show ?case 
  proof safe
    assume ‹p ⊫ HMLt_conj Φ›
    hence ‹∀φ. φ ∈⇩c Φ ⟶ p ⊫ φ› by simp
    with HMLt_conj.hyps have ‹∀φ. φ ∈⇩c Φ ⟶ θ(p) ⊨ σ(φ)› by (simp add: cin.rep_eq)
    thus ‹θ(p) ⊨ σ(HMLt_conj Φ)› by fastforce
  next
    assume ‹θ(p) ⊨ σ(HMLt_conj Φ)›
    hence ‹θ(p) ⊨ HML_conj (cimage (λ φ. σ(φ)) Φ)› by simp
    hence ‹∀φ. cin φ (cimage (λ φ. σ(φ)) Φ) ⟶ θ(p) ⊨ φ› by simp
    hence ‹∀φ. φ ∈⇩c Φ ⟶ θ(p) ⊨ σ(φ)› by blast
    with HMLt_conj.hyps have ‹∀φ. φ ∈⇩c Φ ⟶ p ⊫ φ› by (simp add: cin.rep_eq)
    thus ‹p ⊫ HMLt_conj Φ› by fastforce
  next
    fix X
    assume ‹X ⊆ visible_actions›
    assume ‹p ⊫[X] HMLt_conj Φ›
    hence ‹(∀φ. φ ∈⇩c Φ ⟶ p ⊫[X] φ)› by simp
    with HMLt_conj.hyps ‹X ⊆ visible_actions› have ‹∀φ. φ ∈⇩c Φ ⟶ θ[X](p) ⊨ σ(φ)› 
      by (simp add: cin.rep_eq)
    thus ‹θ[X](p) ⊨ (σ(HMLt_conj Φ))› by auto
  next
    fix X
    assume ‹X ⊆ visible_actions›
    assume ‹θ[X](p) ⊨ σ(HMLt_conj Φ)›
    hence ‹θ[X](p) ⊨ HML_conj (cimage (λ φ. σ(φ)) Φ)› by simp
    hence ‹∀φ. cin φ (cimage (λ φ. σ(φ)) Φ) ⟶ θ[X](p) ⊨ φ› by simp
    hence ‹∀φ. φ ∈⇩c Φ ⟶ θ[X](p) ⊨ σ(φ)› by blast
    with HMLt_conj.hyps ‹X ⊆ visible_actions› have ‹∀φ. φ ∈⇩c Φ ⟶ p ⊫[X] φ› by (simp add: cin.rep_eq)
    with ‹X ⊆ visible_actions› show ‹p ⊫[X] HMLt_conj Φ› by simp
  qed
next
  case (HMLt_neg φ)
  thus ?case by auto
next
  case (HMLt_poss α φ)
  from HMLt_poss.prems show ?case
  proof safe
    assume ‹p ⊫ HMLt_poss α φ›
    hence ‹∃ p'. p ⟼α p' ∧ p' ⊫ φ› ‹α = τ ∨ α ∈ visible_actions› by auto
    then obtain p' where ‹p ⟼α p' ∧ p' ⊫ φ› by blast
    with HMLt_poss.hyps have ‹θ(p') ⊨ σ(φ)› by blast

    from ‹α = τ ∨ α ∈ visible_actions› 
    show ‹θ(p) ⊨ σ(HMLt_poss α φ)›
    proof safe
      assume ‹α = τ›
      with ‹p ⟼α p' ∧ p' ⊫ φ› have ‹θ(p) ⟼⇧θτ θ(p')› using triggered_tau by simp
      with ‹θ(p') ⊨ σ(φ)› have ‹θ(p) ⊨ HML_poss τ σ(φ)› by auto
      thus ‹θ(p) ⊨ σ(HMLt_poss τ φ)› by simp
    next
      assume ‹α ∈ visible_actions›
      hence ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])› 
        using no_epsilon_in_tran visible_actions_def by auto
      have ‹θ(p) ⟼⇧θε[visible_actions] θ[visible_actions](p)› using env_stabilise by auto
      moreover from ‹α ∈ visible_actions› ‹p ⟼α p' ∧ p' ⊫ φ› 
      have ‹θ[visible_actions](p) ⟼⇧θα θ(p')› using tran_visible by auto
      moreover note ‹θ(p') ⊨ σ(φ)› 
      ultimately have ‹θ(p) ⊨ HML_poss (ε[visible_actions]) (HML_poss α σ(φ))› by auto
      with  ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])› show ‹θ(p) ⊨ σ(HMLt_poss α φ)›
        using sat_poss_alpha_not_special visible_actions_def by blast
    qed
  next
    assume ‹θ(p) ⊨ σ(HMLt_poss α φ)›
    have ‹α = τ ⟹ p ⊫ HMLt_poss α φ› proof -
      assume ‹α = τ›
      with ‹θ(p) ⊨ σ(HMLt_poss α φ)› have ‹θ(p) ⊨ HML_poss τ σ(φ)› by simp
      then obtain p' where ‹θ(p) ⟼⇧θτ θ(p')› ‹p ⟼τ p'›  ‹θ(p') ⊨ σ(φ)›
        using generation_triggered_tau lts_theta.HML_sat.simps(3) by blast
      from HMLt_poss.hyps ‹θ(p') ⊨ σ(φ)› have ‹p' ⊫ φ› by auto
      with ‹p ⟼τ p'› ‹α = τ› show ‹p ⊫ HMLt_poss α φ› by auto
    qed
    moreover have ‹α = t ∨ α = t_ε ∨ (∃ X. α = ε[X]) ⟹ p ⊫ HMLt_poss α φ› proof -
      assume ‹α = t ∨ α = t_ε ∨ (∃ X. α = ε[X])›
      with ‹θ(p) ⊨ σ(HMLt_poss α φ)› have ‹θ(p) ⊨ HML_false› using HMt_mapping.simps(5) by metis 
      with lts_theta.HML_sat_false have False by simp
      thus ‹p ⊫ HMLt_poss α φ› by simp
    qed
    moreover have ‹no_special_action α ⟹ p ⊫ HMLt_poss α φ› proof -
      let ?disj = ‹{HML_poss α σ(φ), 
                  HML_poss (ε[visible_actions]) (HML_poss α σ(φ)),
                  HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))}›
      have ‹countable ?disj› by auto
      assume ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])›
      with ‹θ(p) ⊨ σ(HMLt_poss α φ)› have ‹θ(p) ⊨ HML_disj (acset ?disj)› by simp
      hence ‹∃ φ' ∈ ?disj. θ(p) ⊨ φ'› using lts_theta.HML_sat_disj ‹countable ?disj›
        by (smt (z3) cin.abs_eq eq_onp_same_args)
      thus ‹p ⊫ HMLt_poss α φ› proof safe
        assume ‹θ(p) ⊨ HML_poss α σ(φ)›
        then obtain P' where ‹θ(p) ⟼⇧θα P'› by auto
        hence ‹α = τ ∨ (∃ X. α = ε[X])› using generation_triggered_transitions by blast
        with ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])› have False by auto
        thus ‹p ⊫ HMLt_poss α φ› by simp
      next
        assume ‹θ(p) ⊨ HML_poss (ε[visible_actions]) (HML_poss α σ(φ))›
        hence ‹θ[visible_actions](p) ⊨ HML_poss α σ(φ)›
          using generation_env_stabilise injectivity_theta(2) lts_theta.HML_sat.simps(3) by blast
        then obtain P' where ‹θ[visible_actions](p) ⟼⇧θα P'› ‹P' ⊨ σ(φ)› by auto
        with ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])› have ‹α ∈ visible_actions›
          using generation_stable_transitions by blast
        with ‹θ[visible_actions](p) ⟼⇧θα P'›
        obtain p' where ‹P' = θ(p')› ‹p ⟼α p'› using generation_tran_visible by blast
        from ‹P' ⊨ σ(φ)› ‹P' = θ(p')› have ‹p' ⊫ φ› using HMLt_poss.hyps by blast

        with ‹p ⟼α p'› ‹α ∈ visible_actions› show ‹p ⊫ HMLt_poss α φ› by auto
      next
        assume ‹θ(p) ⊨ HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))›
        then obtain P' where ‹θ(p) ⟼⇧θt_ε P'› by auto
        hence False using generation_triggered_transitions distinctness_special_actions by blast
        thus ‹p ⊫ HMLt_poss α φ› by simp
      qed
    qed
    ultimately show ‹p ⊫ HMLt_poss α φ› by blast
  next
    assume ‹X ⊆ visible_actions›
    assume ‹p ⊫[X] HMLt_poss α φ›
    hence ‹α ∈ X ∧ (∃p'. p ⟼α p' ∧ p' ⊫ φ) 
      ∨ α = τ ∧ (∃p'. p ⟼τ  p' ∧ p' ⊫[X] φ) 
      ∨ idle p X ∧ p ⊫ HMLt_poss α φ› 
      by simp
    thus ‹θ[X](p) ⊨ σ(HMLt_poss α φ)›
    proof (elim disjE)
      assume ‹α ∈ X ∧ (∃p'. p ⟼α p' ∧ p' ⊫ φ)›
      hence ‹α ∈ X› ‹∃p'. p ⟼α p' ∧ p' ⊫ φ› by auto

      from ‹α ∈ X› ‹X ⊆ visible_actions› have ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X])›
        using no_epsilon_in_tran visible_actions_def by auto

      from ‹∃p'. p ⟼α p' ∧ p' ⊫ φ› obtain p' where ‹p ⟼α p'› ‹p' ⊫ φ› by blast
      with ‹α ∈ X› ‹X ⊆ visible_actions› have ‹θ[X](p) ⟼⇧θα θ(p')› using tran_visible by auto
      moreover from ‹p' ⊫ φ› have ‹θ(p') ⊨ σ(φ)› using HMLt_poss.hyps by auto
      ultimately have ‹θ[X](p) ⊨ HML_poss α σ(φ)› by auto
      thus ‹θ[X](p) ⊨ σ(HMLt_poss α φ)› using ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X])›
        by (metis insertCI sat_poss_alpha_not_special)
    next
      assume ‹α = τ ∧ (∃p'. p ⟼τ  p' ∧ p' ⊫[X] φ)›
      hence ‹α = τ› ‹∃p'. p ⟼τ  p' ∧ p' ⊫[X] φ› by auto
      then obtain p' where ‹p ⟼τ  p'› ‹p' ⊫[X] φ› by blast
      with ‹X ⊆ visible_actions› have ‹θ[X](p) ⟼⇧θτ θ[X](p')› using stable_tau by auto
      moreover from ‹p' ⊫[X] φ› ‹X ⊆ visible_actions› have ‹θ[X](p') ⊨ σ(φ)› using HMLt_poss.hyps by auto
      ultimately have ‹θ[X](p) ⊨ HML_poss τ σ(φ)› by auto
      thus ‹θ[X](p) ⊨ σ(HMLt_poss α φ)› using ‹α = τ› HMt_mapping.simps(3) by auto
    next
      assume ‹idle p X ∧ p ⊫ HMLt_poss α φ›
      hence ‹idle p X› ‹p ⊫ HMLt_poss α φ› by blast+

      from ‹idle p X› ‹X ⊆ visible_actions› have ‹θ[X](p) ⟼⇧θt_ε θ(p)›
        using env_timeout by simp
      have ‹θ(p) ⟼⇧θε[visible_actions] θ[visible_actions](p)›
        using env_stabilise by simp

      from ‹p ⊫ HMLt_poss α φ› have ‹α ∈ visible_actions ∨ α = τ› ‹∃p'. p ⟼α p' ∧ p' ⊫ φ›
        by auto
      from ‹∃p'. p ⟼α p' ∧ p' ⊫ φ› obtain p' where ‹p ⟼α p'› ‹p' ⊫ φ› by blast
      from ‹α ∈ visible_actions ∨ α = τ› ‹idle p X› ‹p ⟼α p'› have ‹α ∈ visible_actions› 
        using initial_actions_def by auto
      from ‹α ∈ visible_actions›
      have ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X])›
        using no_epsilon_in_tran visible_actions_def by auto

      from ‹p ⟼α p'› ‹α ∈ visible_actions› have ‹θ[visible_actions](p) ⟼⇧θα θ(p')› using tran_visible by auto
      moreover from ‹p' ⊫ φ› have ‹θ(p') ⊨ σ(φ)› using HMLt_poss.hyps by auto
      ultimately have ‹θ[visible_actions](p) ⊨ HML_poss α σ(φ)› by auto

      with ‹θ(p) ⟼⇧θε[visible_actions] θ[visible_actions](p)›
      have ‹θ(p) ⊨ HML_poss (ε[visible_actions]) (HML_poss α σ(φ))› by auto

      with ‹θ[X](p) ⟼⇧θt_ε θ(p)›
      have ‹θ[X](p) ⊨ HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))› by auto

      thus ‹θ[X](p) ⊨ σ(HMLt_poss α φ)› using ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X])›
        by (metis insertCI sat_poss_alpha_not_special)
    qed
  next
    assume ‹X ⊆ visible_actions›
    assume prem: ‹θ[X](p) ⊨ σ(HMLt_poss α φ)›

    have ‹α = τ ⟹ p ⊫[X] HMLt_poss α φ› proof -
      assume ‹α = τ›
      with prem have ‹θ[X](p) ⊨ HML_poss τ σ(φ)› by auto
      hence ‹∃ P'. θ[X](p) ⟼⇧θτ P' ∧ P' ⊨ σ(φ)› by auto
      then obtain p' where ‹p ⟼τ p'› ‹θ[X](p') ⊨ σ(φ)›
        using generation_stable_tau by blast
      from ‹θ[X](p') ⊨ σ(φ)› have ‹p' ⊫[X] φ› 
        using HMLt_poss.hyps ‹X ⊆ visible_actions› by blast
      with ‹p ⟼τ p'› ‹α = τ› ‹X ⊆ visible_actions› show ‹p ⊫[X] HMLt_poss α φ› by auto
    qed
    moreover have ‹α = t ∨ α = t_ε ∨ (∃ X. α = ε[X]) ⟹ p ⊫[X] HMLt_poss α φ› proof -
      assume ‹α = t ∨ α = t_ε ∨ (∃ X. α = ε[X])›
      with prem have ‹θ[X](p) ⊨ HML_false› using HMt_mapping.simps(5) by metis
      with lts_theta.HML_sat_false have False by simp
      thus ‹p ⊫[X] HMLt_poss α φ› by simp
    qed
    moreover have ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X]) ⟹ p ⊫[X] HMLt_poss α φ› proof -
      let ?disj = ‹{HML_poss α σ(φ), 
        HML_poss (ε[visible_actions]) (HML_poss α σ(φ)),
        HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))}›
      have ‹countable ?disj› by auto
      assume α_not_special: ‹α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀X. α ≠ ε[X])›
      with prem have ‹θ[X](p) ⊨ HML_disj (acset ?disj)› using HMt_mapping.simps(5) by auto
      hence ‹∃ φ' ∈ ?disj. θ[X](p) ⊨ φ'› using lts_theta.HML_sat_disj ‹countable ?disj›
        by (smt (z3) cin.abs_eq eq_onp_same_args)
      thus ‹p ⊫[X] HMLt_poss α φ› proof (safe)
        assume ‹θ[X](p) ⊨ HML_poss α σ(φ)›
        then obtain P' where ‹θ[X](p) ⟼⇧θα P'› ‹P' ⊨ σ(φ)› by auto
        hence ‹α ∈ X› using generation_stable_transitions α_not_special by blast
        with ‹X ⊆ visible_actions› ‹θ[X](p) ⟼⇧θα P'› obtain p' where ‹P' = θ(p')› ‹p ⟼α p'›
          using generation_tran_visible by blast
        
        from ‹P' ⊨ σ(φ)› ‹P' = θ(p')› have ‹p' ⊫ φ›
          using HMLt_poss.hyps by auto

        from ‹α ∈ X› ‹p ⟼α p'› ‹p' ⊫ φ› show ‹p ⊫[X] HMLt_poss α φ›
          using ‹X ⊆ visible_actions› by auto
      next
        assume ‹θ[X](p) ⊨ HML_poss (ε[visible_actions]) (HML_poss α σ(φ))›
        then obtain P' where ‹θ[X](p) ⟼⇧θε[visible_actions] P'› by auto
        with generation_env_stabilise injectivity_theta(1) have False by metis
        thus ‹p ⊫[X] HMLt_poss α φ› by simp
      next
        assume ‹θ[X](p) ⊨ HML_poss t_ε (HML_poss (ε[visible_actions]) (HML_poss α σ(φ)))›
        hence ‹θ(p) ⊨ HML_poss (ε[visible_actions]) (HML_poss α σ(φ))› ‹idle p X›
          using generation_env_timeout by auto
        hence ‹θ[visible_actions](p) ⊨ HML_poss α σ(φ)›
          using generation_env_stabilise by (metis injectivity_theta(2) lts_theta.HML_sat.simps(3))
        then obtain P' where ‹θ[visible_actions](p) ⟼⇧θα P'› ‹P' ⊨ σ(φ)› by auto
        with α_not_special have ‹α ∈ visible_actions› using generation_stable_transitions by blast
        with ‹θ[visible_actions](p) ⟼⇧θα P'› obtain p' where ‹P' = θ(p')› ‹p ⟼α p'›
          using generation_tran_visible by blast

        from ‹P' = θ(p')› ‹P' ⊨ σ(φ)› have ‹p' ⊫ φ›
          using HMLt_poss.hyps by auto
        with ‹p ⟼α p'› have ‹p ⊫ HMLt_poss α φ› using ‹α ∈ visible_actions› by auto
        with ‹idle p X› ‹X ⊆ visible_actions› show ‹p ⊫[X] HMLt_poss α φ› by auto
      qed
    qed
    ultimately show ‹p ⊫[X] HMLt_poss α φ› by blast
  qed
next
  case (HMLt_time Y φ)

  {
    assume ‹θ(p) ⊨ σ(HMLt_time Y φ)›
    hence ‹θ(p) ⊨ HML_poss (ε[Y]) (HML_poss t σ(φ))› ‹Y ⊆ visible_actions› 
      using sat_time_backward triggered_env_cannot_timeout by blast+
    hence ‹θ[Y](p) ⊨ HML_poss t σ(φ)›
      using generation_env_stabilise injectivity_theta(2) lts_theta.HML_sat.simps(3) by blast
    then obtain P' where ‹θ[Y](p) ⟼⇧θt P'› ‹P' ⊨ σ(φ)› by (simp, blast)
    from ‹θ[Y](p) ⟼⇧θt P'› obtain p' where ‹P' = θ[Y](p')› ‹idle p Y› ‹p ⟼t  p'› 
      using generation_sys_timeout by blast
    moreover from ‹P' = θ[Y](p')› ‹P' ⊨ σ(φ)› have ‹p' ⊫[Y] φ› 
      using HMLt_time.hyps ‹Y ⊆ visible_actions› by blast
    ultimately have ‹p ⊫ HMLt_time Y φ› using ‹Y ⊆ visible_actions› by auto
  }
  note case2 = this

  from HMLt_time.prems show ?case
  proof safe
    assume ‹p ⊫ HMLt_time Y φ›
    hence ‹Y ⊆ visible_actions› ‹idle p Y› ‹∃p'. p ⟼t  p' ∧ p' ⊫[Y] φ› by auto
    then obtain p' where ‹p ⟼t  p'› ‹p' ⊫[Y] φ› by blast
    from ‹p' ⊫[Y] φ› have ‹θ[Y](p') ⊨ σ(φ)› using HMLt_time.hyps ‹Y ⊆ visible_actions› by simp
    moreover have ‹θ[Y](p) ⟼⇧θt θ[Y](p')› 
      using sys_timeout[OF ‹Y ⊆ visible_actions› ‹idle p Y› ‹p ⟼t  p'›] .
    ultimately have ‹θ[Y](p) ⊨ HML_poss t σ(φ)› by auto

    moreover have ‹θ(p) ⟼⇧θε[Y] θ[Y](p)› using env_stabilise[OF ‹Y ⊆ visible_actions›] .
    ultimately have ‹θ(p) ⊨ HML_poss (ε[Y]) (HML_poss t σ(φ))› by auto

    thus ‹θ(p) ⊨ σ(HMLt_time Y φ)› using sat_time_forward[OF ‹Y ⊆ visible_actions›] by blast
  next
    show ‹θ(p) ⊨ σ(HMLt_time Y φ) ⟹ p ⊫ HMLt_time Y φ› using case2 .
  next
    assume ‹X ⊆ visible_actions›
    assume ‹p ⊫[X] HMLt_time Y φ›

    hence ‹idle p X› ‹p ⊫ HMLt_time Y φ› by simp+
    from ‹p ⊫ HMLt_time Y φ› have ‹Y ⊆ visible_actions› ‹idle p Y› ‹∃p'. p ⟼t p' ∧ p' ⊫[Y] φ›
      by auto
    then obtain p' where ‹p ⟼t p'› ‹p' ⊫[Y] φ› by blast

    have ‹θ[X](p) ⟼⇧θt_ε θ(p)› using env_timeout[OF ‹X ⊆ visible_actions› ‹idle p X›] .
    have ‹θ(p) ⟼⇧θε[Y] θ[Y](p)› using env_stabilise[OF ‹Y ⊆ visible_actions›] .

    from ‹p' ⊫[Y] φ› have ‹θ[Y](p') ⊨ σ(φ)› using HMLt_time.hyps ‹Y ⊆ visible_actions› by simp
    moreover from ‹p ⟼t p'› ‹idle p Y› have ‹θ[Y](p) ⟼⇧θt θ[Y](p')› 
      using sys_timeout[OF ‹Y ⊆ visible_actions›] by simp
    ultimately have ‹θ[Y](p) ⊨ HML_poss t σ(φ)› by auto
    with ‹θ(p) ⟼⇧θε[Y] θ[Y](p)› have ‹θ(p) ⊨ HML_poss (ε[Y]) (HML_poss t σ(φ))› by auto
    with ‹θ[X](p) ⟼⇧θt_ε θ(p)› have ‹θ[X](p) ⊨ HML_poss (t_ε) (HML_poss (ε[Y]) (HML_poss t σ(φ)))› by auto

    thus ‹θ[X](p) ⊨ σ(HMLt_time Y φ)› using sat_time_forward[OF ‹Y ⊆ visible_actions›] by blast
  next
    assume ‹X ⊆ visible_actions›
    assume ‹θ[X](p) ⊨ σ(HMLt_time Y φ)›
    hence ‹θ[X](p) ⊨ HML_poss t_ε (HML_poss (ε[Y]) (HML_poss t σ(φ)))› ‹Y ⊆ visible_actions› 
      using sat_time_backward stable_env_cannot_stabilise by blast+
    hence ‹θ(p) ⊨ HML_poss (ε[Y]) (HML_poss t σ(φ))› ‹idle p X› 
      using generation_env_timeout by force+
    hence ‹θ(p) ⊨ σ(HMLt_time Y φ)› using sat_time_forward[OF ‹Y ⊆ visible_actions›] by blast
    from case2[OF this] have ‹p ⊫ HMLt_time Y φ› .

    thus ‹p ⊫[X] HMLt_time Y φ› using ‹X ⊆ visible_actions› ‹idle p X› by auto
  qed
qed

text ‹Theorems using nicer notation are immediate consequences of this lemma.›

theorem✐‹tag (proof) visible› HMLt_sat_triggered_iff_triggered_env_HML_sat:
  shows ‹p ⊫ φ  ⟺  θ(p) ⊨ σ(φ)› 
  using HMLt_sat_iff_HML_sat by blast
theorem✐‹tag (proof) visible› HMLt_sat_stable_iff_stable_env_HML_sat:
  assumes ‹X ⊆ visible_actions›
  shows ‹p ⊫[X] φ  ⟺  θ[X](p) ⊨ σ(φ)› 
  using HMLt_sat_iff_HML_sat assms by blast

end ― ‹of ‹context lts_timeout_mappable››
(*<*)
end ― ‹of ‹theory››
(*>*)