Theory Weak_Traces

(* License: LGPL *)

section ‹Weak Traces›

theory Weak_Traces
  imports Main HML_SRBB Expressiveness_Price
begin

text ‹
  The point of this theory is to prove that the coordinate \<^term>‹(E ∞ 0 0 0 0 0 0 0)› precisely characterizes weak trace preorder and equivalence.
›

subsection ‹Weak Traces as Modal Constructs›

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›

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))

subsection ‹Weak Trace Observations through Coordinates›

text ‹The following three lemmas show that the modal-logical characterization of weak traces 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› and
    χ :: ‹('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› and
    χ :: ‹('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 trace formula ‹φ› is satisfied by a state ‹p› 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
    ‹is_trace_formula φ ⟹ p ⊨SRBB φ
      ⟹ ∃tr ∈ weak_traces p. wtrace_to_srbb tr ⇚srbb⇛ φ›
    ‹is_trace_formula_inner χ ⟹ hml_srbb_inner_models q χ
      ⟹ ∃tr ∈ weak_traces q. wtrace_to_inner tr ⇚χ⇛ χ›
    True
proof (induction φ and χ and ψ arbitrary: p and q)
  case TT
  thus ?case
    using weak_step_sequence.intros(1) silent_reachable.intros(1) by fastforce
next
  case (Internal χ)
  hence ‹is_trace_formula_inner χ›
    using is_trace_formula.cases by blast
  from ‹p ⊨SRBB Internal χ›
    have ‹∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ›
    unfolding hml_srbb_models.simps .
  then obtain p' where ‹p ↠ p'› ‹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 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 (metis wtrace_to_srbb.simps(2))
  qed
  ultimately show ?case by blast
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
  have ‹wtrace_to_srbb [] ⇚srbb⇛ ImmConj I ψs›
    using srbb_TT_is_empty_conj ‹I = {}›
    unfolding wtrace_to_srbb.simps by auto
  thus ‹∃tr∈weak_traces p. wtrace_to_srbb tr ⇚srbb⇛ ImmConj I ψs›
    using ‹[] ∈ weak_traces p› by auto
next
  case (Obs α φ)
  thus ?case
  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'› ‹q' ⊨SRBB φ› by auto
    hence ‹∃tr' ∈ weak_traces q'. wtrace_to_srbb tr' ⇚srbb⇛ φ›
      using ‹is_trace_formula φ› Obs by auto
    then obtain tr' where ‹tr' ∈ weak_traces q'› ‹wtrace_to_srbb tr' ⇚srbb⇛ φ› by auto
    have ‹(α # tr') ∈ weak_traces q›
      using ‹q ↦ α q'› ‹tr' ∈ weak_traces q'› 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)
  from ‹is_trace_formula_inner (Conj I ψs)› have ‹I = {}›
    by (simp add: is_trace_formula_inner.simps)
  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.
  with empty_trace_allways_weak_trace[of q] show ?case by auto
qed (auto simp add: is_trace_formula_inner.simps)

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)
    then 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 ‹wtrace_to_srbb (a # tail) = (Internal (Obs a (wtrace_to_srbb tail)))›
      by simp
    thus ?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
          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
    thus ?case
      using Cons prepend_τ_weak_trace silent_prepend_weak_traces step_prepend_weak_traces
      by fastforce
  qed
qed

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 expressiveness_to_trace_formula trace_equals_trace_to_formula
      trace_formula_implies_trace
    unfolding weakly_trace_preordered_def
    by (metis (no_types, lifting) eq_equality in_mono)
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›).›
theorem weak_traces_coordinate: ‹(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