Theory Weak_Traces

section ‹Weak Traces \label{appndx:weakTraces}›
theory Weak_Traces
  imports Main HML_SRBB Expressiveness_Price
begin

text ‹The inductive @{term ‹is_trace_formula›} represents the modal-logical characterization of weak traces HML$_{WT}$.
In particular:
\begin{itemize}
  \item $\top \in$ HML$_{WT}$ encoded by  @{term ‹is_trace_formula›} ‹TT›, @{term ‹is_trace_formula›} @{term ‹(ImmConj I ψs)›} if ‹I = {}› and @{term ‹is_trace_formula›} @{term ‹(Conj I ψs)›} if ‹I = {}.›.
  \item ‹⟨ε⟩χ› $\in$ HML$_{WT}$ if ‹φ› $\in$ HML$_{WT}$ encoded by @{term ‹is_trace_formula›} @{term ‹(Internal χ)›} if @{term ‹is_trace_formula›} ‹χ›.
  \item ‹(α)φ› $\in$ HML$_{WT}$ if ‹φ› $\in$ HML$_{WT}$ encoded by @{term ‹is_trace_formula›} @{term ‹(Obs α φ)›} if @{term ‹is_trace_formula›} ‹φ›.
  \item ‹⋀{(α)φ} ∪ Ψ› $\in$ HML$_{WT}$ if ‹φ› $\in$ HML$_{WT}$ and ‹Ψ = {}› encoded by @{term ‹is_trace_formula›} @{term ‹(BranchConj α φ I ψs)›} if @{term ‹is_trace_formula›} ‹φ› and ‹I = {}›.
\end{itemize}›

inductive
      is_trace_formula :: ‹('act, 'i) hml_srbb ⇒ bool›
  and is_trace_formula_inner :: ‹('act, 'i) hml_srbb_inner ⇒ bool› where
  ‹is_trace_formula TT› |
  ‹is_trace_formula (Internal χ)› if ‹is_trace_formula_inner χ› |
  ‹is_trace_formula (ImmConj I ψs)› if ‹I = {}› |

  ‹is_trace_formula_inner (Obs α φ)› if ‹is_trace_formula φ› |
  ‹is_trace_formula_inner (Conj I ψs)› if ‹I = {}›

text ‹We define a function that translates a (weak) trace ‹tr› to a formula ‹φ› such that a state ‹p› models ‹φ›, ‹p ⊨ φ› if and only if ‹tr› is a (weak) trace of ‹p›.›
fun wtrace_to_srbb :: ‹'act list ⇒ ('act, 'i) hml_srbb›
  and wtrace_to_inner :: ‹'act list ⇒ ('act, 'i) hml_srbb_inner›
  and wtrace_to_conjunct :: ‹'act list ⇒ ('act, 'i) hml_srbb_conjunct› where
  ‹wtrace_to_srbb [] = TT› |
  ‹wtrace_to_srbb tr = (Internal (wtrace_to_inner tr))› |

  ‹wtrace_to_inner [] = (Conj {} (λ_. undefined))› | ― ‹ Should never happen›
  ‹wtrace_to_inner (α # tr) = (Obs α (wtrace_to_srbb tr))› |

  ‹wtrace_to_conjunct tr = Pos (wtrace_to_inner tr)› ― ‹Should never happen›

text ‹@{term ‹wtrace_to_srbb trace›} is in our modal-logical characterization of weak traces.›
lemma trace_to_srbb_is_trace_formula:
  ‹is_trace_formula (wtrace_to_srbb trace)›
  by (induct trace,
      auto simp add: is_trace_formula.simps is_trace_formula_is_trace_formula_inner.intros(1,4))

text ‹The following three lemmas show that the modal-logical characterization of HML$_{WT}$ corresponds to the sublanguage of HML$_\text{SRBB}$, obtain by the energy coordinates ‹(∞, 0, 0, 0, 0, 0, 0, 0)›.›

lemma trace_formula_to_expressiveness:
  fixes φ :: ‹('act, 'i) hml_srbb›
  fixes χ :: ‹('act, 'i) hml_srbb_inner›
  shows  ‹(is_trace_formula φ       ⟶ (φ ∈ 𝒪       (E ∞ 0 0 0 0 0 0 0)))
        ∧ (is_trace_formula_inner χ ⟶ (χ ∈ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)))›
  by (rule is_trace_formula_is_trace_formula_inner.induct) (simp add: Sup_enat_def 𝒪_def 𝒪_inner_def)+

lemma expressiveness_to_trace_formula:
  fixes φ :: ‹('act, 'i) hml_srbb›
  fixes χ :: ‹('act, 'i) hml_srbb_inner›
  shows ‹(φ ∈ 𝒪 (E ∞ 0 0 0 0 0 0 0) ⟶ is_trace_formula φ)
       ∧ (χ ∈ 𝒪_inner (E ∞ 0 0 0 0 0 0 0) ⟶ is_trace_formula_inner χ)
       ∧ True›
proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct)
  case TT
  then show ?case
    using is_trace_formula_is_trace_formula_inner.intros(1) by blast
next
  case (Internal x)
  then show ?case
    by (simp add: 𝒪_inner_def 𝒪_def is_trace_formula_is_trace_formula_inner.intros(2))
next
  case (ImmConj x1 x2)
  then show ?case
    using 𝒪_def is_trace_formula_is_trace_formula_inner.intros(3)
    by(auto simp add: 𝒪_def)
next
  case (Obs x1 x2)
  then show ?case by (simp add: 𝒪_def 𝒪_inner_def is_trace_formula_is_trace_formula_inner.intros(4))
next
  case (Conj I ψs)
  show ?case
  proof (rule impI)
    assume ‹Conj I ψs ∈ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)›
    hence ‹I = {}›
      unfolding 𝒪_inner_def
      by (metis bot.extremum_uniqueI bot_enat_def energy.sel(3) expr_pr_inner.simps inst_conj_depth_inner.simps(2) le_iff_add leq_components mem_Collect_eq not_one_le_zero)
    then show ‹is_trace_formula_inner (Conj I ψs)›
      by (simp add: is_trace_formula_is_trace_formula_inner.intros(5))
  qed
next
  case (StableConj I ψs)
  show ?case
  proof (rule impI)
    assume ‹StableConj I ψs ∈ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)›
    have ‹StableConj I ψs ∉ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)›
      by (simp add: 𝒪_inner_def)
    with ‹StableConj I ψs ∈ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)›
    show ‹is_trace_formula_inner (StableConj I ψs)› by contradiction
  qed
next
  case (BranchConj α φ I ψs)
  have ‹expr_pr_inner (BranchConj α φ I ψs) ≥ E 0 1 1 0 0 0 0 0›
    by simp
  hence ‹BranchConj α φ I ψs ∉ 𝒪_inner (E ∞ 0 0 0 0 0 0 0)›
    unfolding 𝒪_inner_def by simp
  thus ?case by blast
next
  case (Pos x)
  then show ?case by auto
next
  case (Neg x)
  then show ?case by auto
qed

lemma modal_depth_only_is_trace_form:
  ‹(is_trace_formula φ) = (φ ∈ 𝒪 (E ∞ 0 0 0 0 0 0 0))›
  using expressiveness_to_trace_formula trace_formula_to_expressiveness by blast

context LTS_Tau
begin

text ‹If a formula ‹φ› is in HML$_{WT}$ and a state ‹p› models ‹φ›, then there exists a weak trace ‹tr› of ‹p› such that @{term ‹wtrace_to_srbb tr›} is equivalent to ‹φ›.›
lemma trace_formula_implies_trace:
  fixes ψ ::‹('a, 's) hml_srbb_conjunct›
  shows
       trace_case: ‹is_trace_formula φ ⟹ p ⊨SRBB φ ⟹ (∃tr ∈ weak_traces p. wtrace_to_srbb tr ⇚srbb⇛ φ)›
    and conj_case: ‹is_trace_formula_inner χ ⟹ hml_srbb_inner_models q χ ⟹ (∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ χ)›
    and            True
proof (induction φ and χ and ψ arbitrary: p and q)
  case TT
  then have ‹[] ∈ weak_traces p›
    using weak_step_sequence.intros(1) silent_reachable.intros(1) by fastforce
  moreover have ‹wtrace_to_srbb [] ⇚srbb⇛ TT›
    unfolding wtrace_to_srbb.simps
    by (simp add: equivp_reflp)
  ultimately show ?case by auto
next
  case (Internal χ)

  from ‹is_trace_formula (Internal χ)›
  have ‹is_trace_formula_inner χ›
    using is_trace_formula.cases by auto

  from ‹p ⊨SRBB Internal χ›
  have ‹∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ›
    unfolding hml_srbb_models.simps.
  then obtain p' where ‹p ↠ p'› and ‹hml_srbb_inner_models p' χ› by auto
  hence ‹hml_srbb_inner_models p' χ› by auto
  with ‹is_trace_formula_inner χ›
  have ‹∃tr∈weak_traces p'. wtrace_to_inner tr ⇚χ⇛ χ›
    using Internal.IH by blast
  then obtain tr where tr_spec:
    ‹tr ∈ weak_traces p'› ‹wtrace_to_inner tr ⇚χ⇛ χ› by auto
  with ‹p ↠ p'› have ‹tr ∈ weak_traces p›
    using silent_prepend_weak_traces by auto

  moreover
  have ‹wtrace_to_srbb tr ⇚srbb⇛ Internal χ›
  proof (cases tr)
    case Nil
    thus ?thesis
      using srbb_TT_is_χTT tr_spec by auto
  next
    case (Cons a tr)
    thus ?thesis
      using tr_spec internal_srbb_cong by auto
  qed

  ultimately show ?case by auto
next
  case (ImmConj I ψs)

  from ‹is_trace_formula (ImmConj I ψs)›
  have ‹I = {}›
    by (simp add: is_trace_formula.simps)

  have ‹[] ∈ weak_traces p›
    using silent_reachable.intros(1) weak_step_sequence.intros(1) by auto

  from srbb_TT_is_empty_conj
   and ‹I = {}›
  have ‹wtrace_to_srbb [] ⇚srbb⇛ ImmConj I ψs›
    unfolding wtrace_to_srbb.simps by auto

  from ‹[] ∈ weak_traces p›
   and ‹wtrace_to_srbb [] ⇚srbb⇛ ImmConj I ψs›
  show ‹∃tr∈weak_traces p. wtrace_to_srbb tr ⇚srbb⇛ ImmConj I ψs› by auto
next
  case (Obs α φ)
  assume IH: ‹⋀p1. is_trace_formula φ ⟹ p1 ⊨SRBB φ ⟹ ∃tr∈weak_traces p1. wtrace_to_srbb tr ⇚srbb⇛ φ›
     and ‹is_trace_formula_inner (Obs α φ)›
     and ‹hml_srbb_inner_models q (Obs α φ)›
  then show ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ›
  proof (cases ‹α = τ›)
    case True

    with ‹hml_srbb_inner_models q (Obs α φ)› have ‹q ⊨SRBB φ›
      using Obs.prems(1) silent_reachable.step empty_conj_trivial(1)
      by (metis (no_types, lifting) hml_srbb_inner.distinct(1) hml_srbb_inner.inject(1)
          hml_srbb_inner_models.simps(1) hml_srbb_models.simps(1,2) is_trace_formula.cases
          is_trace_formula_inner.cases)

    moreover have ‹is_trace_formula φ›
      using ‹is_trace_formula_inner (Obs α φ)› is_trace_formula_inner.cases by auto

    ultimately show ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ›
      using Obs.IH
      by (metis ‹α = τ› obs_srbb_cong prepend_τ_weak_trace wtrace_to_inner.simps(2))
  next
    case False

    from ‹is_trace_formula_inner (Obs α φ)›
    have ‹is_trace_formula φ›
      by (simp add: is_trace_formula_inner.simps)

    from ‹hml_srbb_inner_models q (Obs α φ)› and ‹α ≠ τ›
    have ‹∃q'. q ↦ α q' ∧ q' ⊨SRBB φ› by simp
    then obtain q' where ‹q ↦ α q'› and ‹q' ⊨SRBB φ› by auto

    from ‹is_trace_formula φ›
     and ‹q' ⊨SRBB φ›
     and IH
    have ‹∃tr' ∈ weak_traces q'. wtrace_to_srbb tr' ⇚srbb⇛ φ› by auto
    then obtain tr' where ‹tr' ∈ weak_traces q'› and ‹wtrace_to_srbb tr' ⇚srbb⇛ φ› by auto

    from ‹q ↦ α q'›
     and ‹tr' ∈ weak_traces q'›
    have ‹(α # tr') ∈ weak_traces q›
      using step_prepend_weak_traces by auto

    from ‹wtrace_to_srbb tr' ⇚srbb⇛ φ›
    have ‹Obs α (wtrace_to_srbb tr') ⇚χ⇛ Obs α φ›
      using obs_srbb_cong by auto
    then have ‹wtrace_to_inner (α # tr') ⇚χ⇛ Obs α φ›
      unfolding wtrace_to_inner.simps.

    with ‹(α # tr') ∈ weak_traces q›
    show ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ› by blast
  qed
next
  case (Conj I ψs)
  assume ‹is_trace_formula_inner (Conj I ψs)›
     and ‹hml_srbb_inner_models q (Conj I ψs)›

  from ‹is_trace_formula_inner (Conj I ψs)›
  have ‹I = {}›
    by (simp add: is_trace_formula_inner.simps)

  have ‹[] ∈ weak_traces q› by (rule empty_trace_allways_weak_trace)

  have ‹(Conj {} (λ_. undefined)) ⇚χ⇛ (Conj {} ψs)›
    using srbb_obs_τ_is_χTT by simp
  then have ‹(Conj {} (λ_. undefined)) ⇚χ⇛ (Conj I ψs)›
    using ‹I = {}› by auto
  then have ‹wtrace_to_inner [] ⇚χ⇛ Conj I ψs›
    unfolding wtrace_to_inner.simps.

  from ‹[] ∈ weak_traces q›
   and ‹wtrace_to_inner [] ⇚χ⇛ Conj I ψs›
  show ?case by auto
next
  case (StableConj I ψs)
  have ‹¬is_trace_formula_inner (StableConj I ψs)›
    by (simp add: is_trace_formula_inner.simps)
  with ‹is_trace_formula_inner (StableConj I ψs)›
  show ?case by contradiction
next
  case (BranchConj α φ I ψs)
  assume IH: ‹⋀p1. is_trace_formula φ ⟹ p1 ⊨SRBB φ ⟹ ∃tr∈weak_traces p1. wtrace_to_srbb tr ⇚srbb⇛ φ›
  from ‹is_trace_formula_inner (BranchConj α φ I ψs)›
  have ‹is_trace_formula φ ∧ I = {}›
    by (simp add: is_trace_formula_inner.simps)
  hence ‹is_trace_formula φ› and ‹I = {}› by auto
  from ‹hml_srbb_inner_models q (BranchConj α φ I ψs)›
   and ‹I = {}›
  have ‹hml_srbb_inner_models q (Obs α φ)›
    using srbb_obs_is_empty_branch_conj
    by auto

  have ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ›
  proof (cases ‹α = τ›)
    assume ‹α = τ›

    from ‹hml_srbb_inner_models q (Obs α φ)›
    show ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ›
      using BranchConj.prems(1) is_trace_formula_inner.simps by fastforce
  next
    assume ‹α ≠ τ›

    from ‹hml_srbb_inner_models q (Obs α φ)›
     and ‹α ≠ τ›
    have ‹∃q'. q ↦ α q' ∧ q' ⊨SRBB φ› by auto
    then obtain q' where ‹q ↦ α q'› and ‹q' ⊨SRBB φ› by auto

    from ‹is_trace_formula φ›
     and ‹q' ⊨SRBB φ›
     and IH
    have ‹∃tr' ∈ weak_traces q'. wtrace_to_srbb tr' ⇚srbb⇛ φ› by auto
    then obtain tr' where ‹tr' ∈ weak_traces q'› and ‹wtrace_to_srbb tr' ⇚srbb⇛ φ› by auto

    from ‹q ↦ α q'›
     and ‹tr' ∈ weak_traces q'›
    have ‹(α # tr') ∈ weak_traces q›
      using step_prepend_weak_traces by auto

    from ‹wtrace_to_srbb tr' ⇚srbb⇛ φ›
    have ‹Obs α (wtrace_to_srbb tr') ⇚χ⇛ Obs α φ›
      using obs_srbb_cong by auto
    then have ‹wtrace_to_inner (α # tr') ⇚χ⇛ Obs α φ›
      unfolding wtrace_to_inner.simps.

    with ‹(α # tr') ∈ weak_traces q›
    show ‹∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ Obs α φ› by blast
  qed
  then obtain tr where ‹tr ∈ weak_traces q› and ‹wtrace_to_inner tr ⇚χ⇛ Obs α φ› by auto

  from ‹wtrace_to_inner tr ⇚χ⇛ Obs α φ›
   and ‹I = {}›
  have ‹wtrace_to_inner tr ⇚χ⇛ (BranchConj α φ I ψs)›
    using srbb_obs_is_empty_branch_conj by simp
  with ‹tr ∈ weak_traces q›
  show ?case by blast
next
  case (Pos χ)
  then show ?case by auto
next
  case (Neg χ)
  then show ?case by auto
qed

text ‹‹t› is a weak trace of a state ‹p› if and only if ‹p› models the formula obtained from @{term ‹wtrace_to_srbb t›}.›
lemma trace_equals_trace_to_formula:
  ‹t ∈ weak_traces p = (p ⊨SRBB (wtrace_to_srbb t))›
proof
  assume ‹t ∈ weak_traces p›
  show ‹p ⊨SRBB (wtrace_to_srbb t)›
    using ‹t ∈ weak_traces p›
  proof(induction t arbitrary: p)
    case Nil
    then show ?case
      by simp
  next
    case (Cons a tail)
    from Cons obtain p'' p' where ‹p ↠↦↠ a p''› ‹p'' ↠↦↠$ tail p'› using weak_step_sequence.simps
      by (smt (verit, best) list.discI list.inject mem_Collect_eq)
    with Cons(1) have IS: ‹p'' ⊨SRBB wtrace_to_srbb tail›
      by blast
    from Cons have goal_eq: ‹wtrace_to_srbb (a # tail) = (Internal (Obs a (wtrace_to_srbb tail)))›
      by simp
    show ?case
      by (smt (verit) Cons.IH IS LTS_Tau.hml_srbb_inner_models.simps(1)
          LTS_Tau.silent_reachable_trans ‹p ↠↦↠ a p''› empty_trace_allways_weak_trace goal_eq
          hml_srbb_models.simps(2) weak_step_def wtrace_to_srbb.elims)
  qed
next
  assume ‹p ⊨SRBB wtrace_to_srbb t›
  then show ‹t ∈ weak_traces p›
  proof(induction t arbitrary: p)
    case Nil
    then show ?case
      using weak_step_sequence.intros(1) silent_reachable.intros(1) by auto
  next
    case (Cons a tail)
    hence ‹p ⊨SRBB (Internal (Obs a (wtrace_to_srbb tail)))›
      by simp
    show ?case
      using Cons.IH ‹p ⊨SRBB hml_srbb.Internal (hml_srbb_inner.Obs a (wtrace_to_srbb tail))› prepend_τ_weak_trace silent_prepend_weak_traces step_prepend_weak_traces by fastforce
  qed
qed

text ‹If a state ‹p› weakly trace-pre-orders another state ‹q›, ‹φ› is in our modal-logical characterization HML$_{WT}$, and ‹p› models ‹φ› then ‹q› models ‹φ›.›
lemma aux:
  fixes φ :: ‹('a, 's) hml_srbb›
  fixes χ :: ‹('a, 's) hml_srbb_inner›
  fixes ψ :: ‹('a, 's) hml_srbb_conjunct›
  shows ‹p ≲WT q ⟹ is_trace_formula φ ⟹ p ⊨SRBB φ ⟹ q ⊨SRBB φ›
proof -
  assume φ_trace: ‹is_trace_formula φ› and p_sat_srbb: ‹p ⊨SRBB φ› and assms: ‹p ≲WT q›
  show ‹q ⊨SRBB φ›
  proof-
    from assms have p_trace_implies_q_trace: ‹∀tr p'. (p ↠↦↠$ tr p') ⟶ (∃q'. q ↠↦↠$ tr q')›
      unfolding weakly_trace_preordered_def by auto
    from p_sat_srbb trace_formula_implies_trace obtain tr p' where
      ‹(p ↠↦↠$ tr p')› ‹wtrace_to_srbb tr ⇚srbb⇛ φ›
      using φ_trace by blast
    with p_trace_implies_q_trace obtain q' where ‹q ↠↦↠$ tr q'›
      by blast
    with trace_equals_trace_to_formula show ?thesis
      using ‹wtrace_to_srbb tr ⇚srbb⇛ φ› by auto
  qed
qed

text ‹These are the main lemmas of this theory. They establish that the colloquial, relational notion of of weak trace pre-order/equivalence
has the same distinctive power as the one derived from the coordinate (‹∞, 0, 0, 0, 0, 0, 0, 0›).
\\\\
A state ‹p› weakly trace-pre-orders a state ‹q› iff and only if it also pre-orders ‹q› with respect to the coordinate (‹∞, 0, 0, 0, 0, 0, 0, 0›).›
lemma expr_preorder_characterizes_relational_preorder_traces:
  ‹(p ≲WT q) = (p ≼ (E ∞ 0 0 0 0 0 0 0) q)›
  unfolding expr_preord_def preordered_def
proof
  assume ‹p ≲WT q›
  thus ‹∀φ∈𝒪 (E ∞ 0 0 0 0 0 0 0). p ⊨SRBB φ ⟶ q ⊨SRBB φ›
    using aux expressiveness_to_trace_formula weakly_trace_preordered_def
    by blast+
next
  assume φ_eneg: ‹∀φ∈𝒪 (E ∞ 0 0 0 0 0 0 0). p ⊨SRBB φ ⟶ q ⊨SRBB φ›
  thus ‹p ≲WT q›
    unfolding weakly_trace_preordered_def
    using trace_equals_trace_to_formula trace_formula_to_expressiveness trace_to_srbb_is_trace_formula
    by fastforce
qed

text ‹Two states ‹p› and ‹q› are weakly trace equivalent if and only if they they are equivalent with respect to the coordinate (‹∞, 0, 0, 0, 0, 0, 0, 0›).›
lemma ‹(p ≃WT q) = (p ∼ (E ∞ 0 0 0 0 0 0 0) q)›
  using expr_preorder_characterizes_relational_preorder_traces
  unfolding weakly_trace_equivalent_def expr_equiv_def 𝒪_def expr_preord_def
  by simp

end

end