Theory Tau_Sinks

section ‹Reductions and ‹τ›-sinks›

text ‹
  Checking trace inclusion can be reduced to contrasimulation checking,
  as can weak simulation checking to coupled simulation checking.
  The trick is to add a ‹τ›-sink to the transition system, that is, a state that is reachable
  by ‹τ›-steps from every other state, and cannot be left.
  An illustration of such an extension is given in Figure~\ref{fig:sink-illustration}.
  Intuitively, the extension means that the model is allowed to just stop progressing at any point.

  We here prove that, on systems with a ‹τ›-sink, weak similarity equals coupled similarity and 
  weak trace inclusion equals contrasimilarity.
  We also prove that adding a ‹τ›-sink to a system does not change weak similarity nor weak trace
  inclusion relationships within the system.
  As adding the ‹τ›-sink only has negligible effect on the system sizes, these facts establish the
  reducibility relationships.
›

text_raw ‹
  \begin{figure}
    \centering
    \begin{tikzpicture}[scale=1, auto]
  
      \node (p0) [circle, draw=black] at (0,0)                    {};
      \node (p1) [circle, draw=black, below right= 1cm of p0]                {};
      \node (p2) [circle, draw=black, below left= 1.5cm and 2mm of p1]          {};
      \node (p3) [circle, draw=black, above left= 1cm of p2]           {};
      %\node (p5) [circle, draw=black, below left= 5mm and 8mm of p0]           {};
      
      \node (bot) [circle, draw= red, right= 2cm of p1] {\Large$\color{red}{\bot}$};
      
      \path[->]
        (p0)         edge[swap, bend left = 15]         node    {}         (p1)
        (p0)         edge[swap, bend right = 15]         node    {}         (p3)
        (p1)         edge[bend left = 15]               node    {}         (p2)
        (p2)         edge[loop below]   node    {}         (p2)
        (p3)         edge[bend left = 15]    node    {}         (p1)
        (p3)         edge[bend right = 15]   node    {}         (p2)
        (p1)         edge[bend left = 15]   node    {}         (p3)
        ;
       
      %Contrasim_ undirected
      \path[->, draw=red,  every node/.style={color=red}]
        (p0)         edge[bend left = 25]         node    {$\tau$}       (bot)
        (p1)         edge[bend left = 10]         node    {$\tau$}    (bot)
        (p2)         edge[swap,bend right = 25]   node    {$\tau$}         (bot)
        (p3)         edge[bend right = 0, out = -35, in=-168]   node    {$\tau$}         (bot)
        (bot)         edge[loop below]   node    {$\tau$}         (bot)
       ;
    ;
    \end{tikzpicture}
    \caption{Example of a $\tau$-sink extension with the original transition system in black and
      the extension in red.}
      \label{fig:sink-illustration}
  \end{figure}
›

theory Tau_Sinks
imports
  Coupled_Simulation
begin

subsection ‹‹τ›-Sink Properties›

context lts_tau
begin

definition tau_sink ::
  ‹'s ⇒ bool›
where
  ‹tau_sink p ≡ 
    (∀a p'. p ⟼a p' ⟶ a = τ ∧ p = p') ∧
    (∀p0. p0 ⟼τ p)›

text ‹The tau sink is a supremum for the weak transition relation.›

lemma tau_sink_maximal:
  assumes ‹tau_sink sink›
  shows
    ‹tau_max sink›
    ‹(p ⟼* tau sink)›
  using assms steps_loop step_weak_step_tau tau_tau unfolding tau_sink_def by metis+

lemma sink_has_no_word_transitions: 
  assumes 
    ‹tau_sink sink›
    ‹A ≠ []›
    ‹∀ a ∈ set(A). a ≠ τ›
  shows ‹∄s'. sink ⇒$A s'›
proof - 
  obtain a where ‹∃B. A = a#B› using assms(2) list.exhaust_sel by auto
  hence ‹∄s' . sink ⇒^a s'›
    by (metis assms(1,3) list.set_intros(1) lts_tau.tau_def steps_loop tau_sink_def)
  thus ?thesis using ‹∃B. A = a#B› by fastforce
qed

subsection ‹Contrasimulation Equals Weak Simulation on ‹τ›-Sink Systems›

lemma sink_coupled_simulates_all_states:
  assumes
    ‹⋀ p . (p ⟼* tau sink)›
  shows 
    ‹sink ⊑cs p› 
  by (simp add: assms coupledsim_refl coupledsim_step)

theorem coupledsim_weaksim_equiv_on_sink_expansion:
  assumes
    ‹⋀ p . (p ⟼* tau sink)›
  shows
    ‹p ⊑ws q ⟷ p ⊑cs q›
  using assms 
  using coupled_simulation_weak_simulation weak_sim_tau_step weaksim_greatest by auto

subsection ‹Contrasimulation Equals Weak Trace Inclusion on ‹τ›-Sink Systems›
  
lemma sink_contrasimulates_all_states:
fixes A :: " 'a list"
  assumes 
    ‹tau_sink sink›
    ‹⋀ p . (p ⟼* tau sink)›
  shows 
    ‹∀ p. sink ⊑c p›
proof (cases A)
  case Nil
  hence empty_word: ‹sink ⇒$A sink› by (simp add: steps.refl)
  have ‹∀p. p ⇒$A sink› using assms(2) Nil by auto
  have ‹sink ⊑c sink› using contrasim_tau_step empty_word Nil by auto 
  show ?thesis using assms(2) contrasim_tau_step by auto 
next
  case Cons
  hence ‹∄s'. (∀ a ∈ set(A). a ≠ τ) ∧ sink ⇒$A s'›
    using assms(1) sink_has_no_word_transitions by fastforce
  show ?thesis using assms(2) contrasim_tau_step by auto 
qed

lemma sink_trace_includes_all_states:
  assumes 
    ‹⋀ p . (p ⟼* tau sink)›
  shows 
    ‹sink ⊑T p›
  by (metis assms contrasim_tau_step lts_tau.contrasim_implies_trace_incl) 

lemma trace_incl_with_sink_is_contrasim:
  assumes
    ‹⋀ p . (p ⟼* tau sink)›
    ‹⋀ p . R sink p›
    ‹trace_inclusion R›
  shows
    ‹contrasimulation R›
 unfolding contrasimulation_def
proof clarify
  fix p q p' A
  assume ‹R p q› ‹p ⇒$A  p'› ‹∀ a ∈ set(A). a ≠ τ›
  hence ‹∃q'. q ⇒$A  q'›
    using assms(3) unfolding trace_inclusion_def by blast
  hence ‹q ⇒$A  sink›
    using assms(1) tau_tau word_tau_concat by blast
  thus ‹∃q'. q ⇒$ A  q' ∧ R q' p'›
    using assms(2) by auto
qed

theorem contrasim_trace_incl_equiv_on_sink_expansion_R:
  assumes
    ‹⋀ p . (p ⟼* tau sink)›
    ‹⋀ p . R sink p›
  shows 
    ‹contrasimulation R = trace_inclusion R›
proof
  assume ‹contrasimulation R›
  thus ‹trace_inclusion R› by (simp add: contrasim_implies_trace_incl)
next
  assume ‹trace_inclusion R›
  thus ‹contrasimulation R›  by (meson assms lts_tau.trace_incl_with_sink_is_contrasim)
qed

theorem contrasim_trace_incl_equiv_on_sink_expansion:
  assumes
    ‹⋀ p . (p ⟼* tau sink)›
  shows
    ‹p ⊑T q ⟷ p ⊑c q›
  using assms weak_trace_inlcusion_greatest
    contrasim_tau_step contrasim_trace_incl_equiv_on_sink_expansion_R contrasim_implies_trace_incl
  by (metis (no_types, lifting))

end

subsection ‹Weak Simulation Invariant under ‹τ›-Sink Extension›

lemma simulation_tau_sink_1:
  fixes
    step sink R τ
  defines
    ‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a = τ ∧ p2 = sink) ∨ step p1 a p2›
  assumes
    ‹⋀ a p . ¬ step sink a p›
    ‹lts_tau.weak_simulation step τ R›
  shows
    ‹lts_tau.weak_simulation step2 τ (λ p q. p = sink ∨ R p q)›
proof -
  let ?tau = ‹(lts_tau.tau τ)›
  let ?tauEx = ‹τ›
  show ?thesis unfolding lts_tau.weak_simulation_def
  proof safe
    fix p q p' a
    assume ‹step2 sink a p'›
    hence ‹p' = sink› ‹a = τ›
      using assms(2) unfolding step2_def by auto
    thus ‹∃q'. (p' = sink ∨ R p' q') ∧
      (?tau a ⟶ lts.steps step2 q ?tau q') ∧ 
      (¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2 
        ∧ lts.steps step2 pq2 ?tau q'))›
      using lts_tau.step_tau_refl[of τ step2 q] by auto
  next
    fix p q p' a
    assume ‹step2 p a p'› ‹R p q›
    have step_impl_step2: ‹⋀ p1 a p2 . step p1 a p2 ⟹ step2 p1 a p2›
      unfolding step2_def by blast
    have ‹(p ≠ sink ∧ a = ?tauEx ∧ p' = sink) ∨ step p a p'›
      using `step2 p a p'` unfolding step2_def .
    thus ‹∃q'. (p' = sink ∨ R p' q') ∧
      (?tau a ⟶ lts.steps step2 q ?tau q') ∧
      (¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
        ∧ lts.steps step2 pq2 ?tau q'))›
    proof safe
      show ‹∃q'. (sink = sink ∨ R sink q') ∧
           (?tau ?tauEx ⟶ lts.steps step2 q ?tau q') ∧
           (¬ ?tau ?tauEx ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1
            ∧ step2 pq1 ?tauEx pq2 ∧ lts.steps step2 pq2 ?tau q'))›
        using lts.steps.refl[of step2 q ?tau] assms(1) by (meson lts_tau.tau_tau)
    next
      assume ‹step p a p'›
      then obtain q' where q'_def:
        ‹R p' q' ∧
        (?tau a ⟶ lts.steps step q ?tau q') ∧
        (¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step q ?tau pq1 ∧ step pq1 a pq2
          ∧ lts.steps step pq2 ?tau q'))›
        using assms(3) `R p q` unfolding lts_tau.weak_simulation_def by blast
      hence ‹(p' = sink ∨ R p' q') ∧
        (?tau a ⟶ lts.steps step2 q ?tau q') ∧
        (¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
          ∧ lts.steps step2 pq2 ?tau q'))›
        using lts_impl_steps[of step _ _ _ step2] step_impl_step2 by blast
      thus ‹∃q'. (p' = sink ∨ R p' q') ∧
        (?tau a ⟶ lts.steps step2 q ?tau q') ∧
        (¬ ?tau a ⟶ (∃pq1 pq2. lts.steps step2 q ?tau pq1 ∧ step2 pq1 a pq2
          ∧ lts.steps step2 pq2 ?tau q'))›
        by blast
    qed
  qed
qed
  
lemma simulation_tau_sink_2:
  fixes
    step sink R τ
  defines
    ‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a = τ ∧ p2 = sink) ∨ step p1 a p2›
  assumes
    ‹⋀ a p . ¬ step sink a p ∧ ¬ step p a sink›
    ‹lts_tau.weak_simulation step2 τ (λ p q. p = sink ∨ R p q)›
    ‹⋀ p' q' q . (p' = sink ∨ R p' q') 
      ∧ lts.steps step2 q (lts_tau.tau τ) q'  ⟶ (p' = sink ∨ R p' q)›
  shows
    ‹lts_tau.weak_simulation step τ (λ p q. p = sink ∨ R p q)›
proof -
  let ?tau = ‹(lts_tau.tau τ)›
  let ?tauEx = ‹τ›
  let ?steps = ‹lts.steps›
  show ?thesis
    unfolding lts_tau.weak_simulation_def
  proof safe
    fix p q p' a
    assume
      ‹step sink a p'›
    hence False using assms(2) by blast
    thus ‹∃q'. (p' = sink ∨ R p' q') ∧
      (?tau a ⟶ ?steps step q ?tau q') ∧
      (¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
        ∧ ?steps step pq2 ?tau q'))› ..
  next
    fix p q p' a
    assume ‹R p q› ‹step p a p'›
    hence not_sink: ‹p ≠ sink› ‹p' ≠ sink›
      using assms(2)[of a p] assms(2)[of a p'] by auto
    have ‹step2 p a p'› using `step p a p'` unfolding step2_def by blast
    then obtain q' where q'_def:
      ‹p' = sink ∨ R p' q'›
      ‹?tau a ⟶ ?steps step2 q ?tau q'›  
      ‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step2 q ?tau pq1 ∧ step2 pq1 a pq2 
        ∧ ?steps step2 pq2 ?tau q')›
      using assms(3) `R p q` unfolding lts_tau.weak_simulation_def by blast
    hence outer_goal_a: ‹R p' q'› using not_sink by blast
    show ‹∃q'. (p' = sink ∨ R p' q') ∧
      (?tau a ⟶ ?steps step q ?tau q') ∧
      (¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
        ∧ ?steps step pq2 ?tau q'))›
    proof (cases ‹q' = sink›)
      assume ‹q' = sink›
      then obtain q'' where q''_def:
        ‹?tau a ⟶ (?steps step q ?tau q'' ∧ ?steps step2 q'' ?tau q')›
        ‹¬ ?tau a ⟶ (∃pq1. ?steps step2 q ?tau pq1 ∧ step pq1 a q''
          ∧ ?steps step2 q'' ?tau q')›
        using q'_def(2,3) assms(1) step2_def lts_tau.step_tau_refl[of τ]
          lts_tau.tau_tau[of τ] by metis
      hence ‹q'' = sink ⟶ q = sink›
        using assms(2) unfolding step2_def by (metis lts.steps.cases)
      have ‹?steps step2 q'' ?tau q'› using q''_def by auto
      hence ‹p' = sink ∨ R p' q''› using  q'_def(1) assms(4)[of p' q' q''] by blast
      moreover have ‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
        ∧ ?steps step pq2 ?tau q'')›
      proof
        assume ‹¬ ?tau a›
        hence ‹q ≠ sink› using q'_def by (metis assms(2) lts.steps_left step2_def)
        hence ‹q'' ≠ sink› using `q'' = sink ⟶ q = sink` by simp
        obtain pq1 where pq1_def:
            ‹?steps step2 q ?tau pq1› ‹step pq1 a q''› ‹?steps step2 q'' ?tau q'›
          using q''_def(2) `¬ ?tau a` by blast
        hence ‹pq1 ≠ sink› using `q'' ≠ sink` assms(2) by blast
        hence ‹?steps step q ?tau pq1› using `q ≠ sink` `?steps step2 q ?tau pq1`
        proof (induct rule: lts.steps.induct[OF `?steps step2 q ?tau pq1`])
          case (1 p af)
          then show ?case using lts.steps.refl[of step p af] by blast
        next
          case (2 p af q1 a q)
          hence ‹q1 ≠ sink› ‹step q1 a q› using assms(2) unfolding step2_def by auto
          moreover hence ‹?steps step p af q1› using 2 by blast 
          ultimately show ?case using 2(4) by (meson lts.step)
        qed
        thus
          ‹∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2 ∧ ?steps step pq2 ?tau q''›
          using pq1_def(2) lts.steps.refl[of step q'' ?tau] by blast
      qed
      ultimately show ‹∃q''. (p' = sink ∨ R p' q'') ∧
           (?tau a ⟶ ?steps step q ?tau q'') ∧
           (¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
            ∧ ?steps step pq2 ?tau q''))›
        using q''_def(1) q'_def(1) by auto
    next
      assume not_sink_q': ‹q' ≠ sink›
      have outer_goal_b: ‹?tau a ⟶ ?steps step q ?tau q'›
        using q'_def(2) not_sink_q' unfolding step2_def
      proof (safe)
        assume i:
          ‹q' ≠ sink› ‹?tau a›
          ‹?steps (λp1 a p2. p1 ≠ sink ∧ a = ?tauEx ∧ p2 = sink ∨ step p1 a p2) q ?tau q'›
        thus ‹?steps step q ?tau q'›
        proof (induct rule: lts.steps.induct[OF i(3)])
          case (1 p af)
          then show ?case using lts.steps.refl[of _ p af] by auto
        next
          case (2 p af q1 a q)
          hence ‹step q1 a q› by blast
          moreover have ‹?steps step p af q1› using 2 assms(2) by blast
          ultimately show ?case using `af a` lts.step[of step p af q1 a q] by blast
        qed
      qed
      have outer_goal_c:
          ‹¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
          ∧ ?steps step pq2 ?tau q')›
        using q'_def(3)
      proof safe
        fix pq1 pq2
        assume subassms:
          ‹¬ ?tau a›
          ‹?steps step2 q ?tau pq1›
          ‹step2 pq1 a pq2›
          ‹?steps step2 pq2 ?tau q'›
        have ‹pq2 ≠ sink› 
          using subassms(4) assms(2) not_sink_q' lts.steps_loop
          unfolding step2_def by (metis (mono_tags, lifting))
        have  goal_c: ‹?steps step pq2 ?tau q'›
          using subassms(4) not_sink_q' unfolding step2_def
        proof (induct rule:lts.steps.induct[OF subassms(4)])
          case (1 p af) show ?case using lts.steps.refl by assumption
        next
          case (2 p af q1 a q)
          hence ‹step q1 a q› unfolding step2_def by simp
          moreover hence ‹q1 ≠ sink› using assms(2) by blast
          ultimately have ‹?steps step p af q1› using 2 unfolding step2_def by auto
          thus ?case using `step q1 a q` 2(4) lts.step[of step p af q1 a q] by blast
        qed
        have goal_b: ‹step pq1 a pq2›
          using `pq2 ≠ sink` subassms(3) unfolding step2_def by blast
        hence ‹pq1 ≠ sink› using assms(2) by blast
        hence goal_a: ‹?steps step q ?tau pq1›
          using subassms(4) unfolding step2_def
        proof (induct rule:lts.steps.induct[OF subassms(2)])
          case (1 p af) show ?case using lts.steps.refl by assumption
        next
          case (2 p af q1 a q)
          hence ‹step q1 a q› unfolding step2_def by simp
          moreover hence ‹q1 ≠ sink› using assms(2) by blast
          ultimately have ‹?steps step p af q1› using 2 unfolding step2_def by auto
          thus ?case using `step q1 a q` 2(4) lts.step[of step p af q1 a q] by blast
        qed
        thus
          ‹∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2 ∧ ?steps step pq2 ?tau q'›
          using goal_b goal_c by auto
      qed
      thus ‹∃q'. (p' = sink ∨ R p' q') ∧ (?tau a ⟶ ?steps step q ?tau q') ∧
        (¬ ?tau a ⟶ (∃pq1 pq2. ?steps step q ?tau pq1 ∧ step pq1 a pq2
          ∧ ?steps step pq2 ?tau q'))›
        using outer_goal_a outer_goal_b by auto
    qed
  qed
qed

lemma simulation_sink_invariant:
  fixes
    step sink R τ
  defines
    ‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a =  τ ∧ p2 = sink) ∨ step p1 a p2›
  assumes
    ‹⋀ a p . ¬ step sink a p ∧ ¬ step p a sink›
  shows ‹lts_tau.weakly_simulated_by step2 τ p q = lts_tau.weakly_simulated_by step τ p q›
proof (rule)
  have sink_sim_min: ‹lts_tau.weak_simulation step2 τ (λ p q. p = sink)›
    unfolding lts_tau.weak_simulation_def step2_def using assms(2)
    by (meson lts.steps.simps)
  define R where ‹R ≡ lts_tau.weakly_simulated_by step2 τ›
  have weak_sim_R: ‹lts_tau.weak_simulation step2 τ R›
    using lts_tau.weaksim_greatest[of step2 τ] unfolding R_def by blast
  have R_contains_inv_tau_closure:
    ‹R = (λp1 q1. R p1 q1 ∨ lts.steps step2 q1 (lts_tau.tau τ) p1)›
    unfolding R_def using lts_tau.weak_sim_tau_step by fastforce
  assume Rpq: ‹R p q›
  have ‹⋀ p' q' q . R p' q' ∧ lts.steps step2 q (lts_tau.tau τ) q'  ⟶ R p' q›
    using R_contains_inv_tau_closure lts_tau.weak_sim_trans[of step2 ‹τ› _ _ _] R_def assms(2)
    by meson
  hence closed_R:
      ‹⋀ p' q' q . (p' = sink ∨ R p' q') ∧ lts.steps step2 q (lts_tau.tau τ) q'
         ⟶ (p' = sink ∨ R p' q)›
    using weak_sim_R sink_sim_min lts_tau.weak_sim_union_cl by blast
  have ‹lts_tau.weak_simulation step2 τ (λp q. p = sink ∨ R p q)›
    using weak_sim_R sink_sim_min lts_tau.weak_sim_union_cl[of step2 τ] by blast
  hence ‹lts_tau.weak_simulation step τ (λp q. p = sink ∨ R p q)›
    using  simulation_tau_sink_2[of step sink τ R] assms(2) closed_R
    unfolding step2_def by blast
  thus ‹∃R. lts_tau.weak_simulation step τ R ∧ R p q›
    using Rpq weak_sim_R by blast
next
  show ‹∃R. lts_tau.weak_simulation step τ R ∧ R p q ⟹
        ∃R. lts_tau.weak_simulation step2 τ R ∧ R p q›
  proof clarify
    fix R
    assume
      ‹lts_tau.weak_simulation step τ R›
      ‹R p q›
    hence ‹lts_tau.weak_simulation
      (λp1 a p2. p1 ≠ sink ∧ a = τ ∧ p2 = sink ∨ step p1 a p2) τ (λp q. p = sink ∨ R p q)›
      using simulation_tau_sink_1[of step sink τ R] assms(2) unfolding step2_def by auto
    thus ‹∃R. lts_tau.weak_simulation step2 τ R ∧ R p q›
      using `R p q` unfolding step2_def by blast
  qed
qed

subsection ‹Trace Inclusion Invariant under ‹τ›-Sink Extension›

lemma trace_inclusion_sink_invariant:
  fixes
    step sink R τ
  defines
    ‹step2 ≡ λ p1 a p2 . (p1 ≠ sink ∧ a =  τ ∧ p2 = sink) ∨ step p1 a p2›
  assumes
    ‹⋀ a p . ¬ step sink a p ∧ ¬ step p a sink›
  shows
    ‹lts_tau.weakly_trace_included_by step2 τ p q
    = lts_tau.weakly_trace_included_by step τ p q›
proof - 
  let ?tau = ‹(lts_tau.tau τ)›
  let ?weak_step = ‹lts_tau.weak_step_tau step τ›
  let ?weak_step2 = ‹lts_tau.weak_step_tau step2 τ›
  let ?weak_seq = ‹lts_tau.weak_step_seq step τ›
  let ?weak_seq2 = ‹lts_tau.weak_step_seq step2 τ›
  {
    fix A
    have ‹∀p p'. (∀ a ∈ set(A). a ≠ τ)
    ∧ ?weak_seq2 p A p' 
    ⟶ (∃p''. ?weak_seq p A p''
    ∧ ?weak_step2 p'' τ p')›
    proof(clarify, induct A rule: rev_induct)
      case Nil
      hence ‹?weak_step p τ p›
        using lts_tau.step_tau_refl by fastforce
      thus ?case
        by (metis Nil.prems(2) lts_tau.tau_tau lts_tau.weak_step_seq.simps(1)) 
    next
      case (snoc a A)
      hence not_in_set: ‹∀a∈set A. a ≠ τ› by force 
      then obtain p01 where 
        ‹?weak_seq2 p A p01› and
        p01_def2: ‹?weak_step2 p01 a p'›
        using snoc by (metis lts_tau.rev_seq_split) 
      then obtain p02 where p02_def: 
        ‹?weak_seq p A p02› 
        ‹?weak_step2 p02 τ p01›
        using snoc.hyps[of p p01] snoc.prems(1) not_in_set by auto
      hence ‹?weak_step2 p02 a p'› 
        using p01_def2 lts_tau.step_tau_concat lts_tau.tau_tau
        by (smt (verit, del_insts))
      then obtain p03 p04 where 
        tau1: ‹?weak_step2 p02 τ p03› and
        a_step2: ‹step2 p03 a p04› and
        tau2: ‹?weak_step2 p04 τ p'›
        using snoc.prems(1) lts_tau.tau_def 
        by (metis last_in_set snoc_eq_iff_butlast)
      hence ‹p04 ≠ sink› using assms snoc.prems(1) by force
      hence a_step: ‹step p03 a p04› using a_step2 assms by auto
      have notsinkp03: ‹p03 ≠ sink› using a_step2 assms snoc.prems(1) by force
      have ‹lts.steps step2 p02 ?tau p03› using tau1 by (simp add: lts_tau.tau_tau)
      hence ‹lts.steps step p02 ?tau p03› using notsinkp03
      proof (induct rule: lts.steps.induct[OF `lts.steps step2 p02 ?tau  p03`])
        case (1 p A)
        thus ?case by (simp add: lts.refl)
      next
        case (2 p A q1 a q)
        hence ‹q1 ≠ sink› using assms(2) step2_def by blast 
        thus ?case using 2 lts.step step2_def by metis
      qed 
      hence ‹?weak_step p02 τ p03› by (simp add: lts_tau.tau_tau)
      hence ‹?weak_step p02 a p04› using a_step
        by (metis lts.step lts_tau.step_tau_refl lts_tau.tau_tau) 
      hence ‹?weak_seq p (A@[a]) p04›
        using lts_tau.rev_seq_step_concat p02_def(1) by fastforce 
      thus ?case using tau2 by auto
    qed
  }
  hence step2_to_step: ‹∀A p p'. (∀ a ∈ set(A). a ≠ τ)
    ∧ ?weak_seq2 p A p' 
    ⟶ (∃p''. ?weak_seq p A p'')›
    by fastforce

  have step_to_step2:  ‹∀A p p'. (∀ a ∈ set(A). a ≠ τ)
    ∧ ?weak_seq p A p' 
    ⟶ ?weak_seq2 p A p'›
  proof
    fix A
    show ‹∀p p'. (∀ a ∈ set(A). a ≠ τ)
    ∧ ?weak_seq p A p' 
    ⟶ ?weak_seq2 p A p'›
    proof(clarify, induct A rule: list.induct)
      case Nil
      assume ‹?weak_seq p [] p'›
      hence tau_step: ‹?weak_step p τ p'›
        by (simp add: lts_tau.weak_step_seq.simps(1) lts_tau.tau_tau)
      hence ‹?weak_step2 p τ p'›
        using lts_impl_steps step2_def lts_tau.tau_tau  by force 
      thus ?case by (simp add: lts_tau.weak_step_seq.simps(1) lts_tau.tau_tau) 
    next
      case (Cons x xs)
      then obtain p1 where p1_def: ‹?weak_step p x p1› 
      ‹?weak_seq p1 xs p'›
        by (metis (mono_tags, lifting) lts_tau.weak_step_seq.simps(2))
      hence IH: ‹?weak_seq2 p1 xs p'› using Cons by auto
      then obtain p01 p02 where ‹?weak_step p τ p01› and
        strong: ‹step p01 x p02› and
        p02_weak: ‹?weak_step p02 τ p1›
        using Cons.prems(1) p1_def lts_tau.tau_def by (metis list.set_intros(1))
      hence tau1: ‹?weak_step2 p τ p01› 
        using lts_impl_steps step2_def
        by (smt (verit, best))
      have ‹?weak_step2 p02 τ p1› 
        using p02_weak lts_impl_steps step2_def by (smt (verit, best))
      hence ‹?weak_step2 p x p1› 
        using tau1 strong step2_def Cons.prems(1) lts_tau.tau_def
        by (metis list.set_intros(1))  
      thus ‹?weak_seq2 p (x#xs) p'› 
        using IH lts_tau.weak_step_seq_def[of step2 τ] by auto
    qed
  qed
  show ?thesis
  proof (rule)
    assume ‹∃R. lts_tau.trace_inclusion step2 τ R ∧ R p q›
    then obtain R where weak_sim_R: ‹lts_tau.trace_inclusion step2 τ R›
      and Rpq: ‹R p q›
      by blast
    have ‹lts_tau.trace_inclusion step τ R›
      unfolding lts_tau.trace_inclusion_def
    proof clarify
      fix p q p' A
      assume subassms: 
        ‹∀a∈set A. a ≠ τ›
        ‹R p q›
        ‹?weak_seq p A p'›
      hence ‹(∀a∈set A. a ≠ τ) ∧
       ?weak_seq2 p A p' ⟶
       (∃q'. ?weak_seq2 q A q')› 
        using weak_sim_R 
        unfolding lts_tau.trace_inclusion_def by simp
      hence ‹(∀a∈set A. a ≠ τ) ∧
       ?weak_seq p A p' ⟶
       (∃q'. ?weak_seq q A q')›
        using step2_to_step step_to_step2
        by auto
      thus "∃q'. ?weak_seq q A q'"
        by (simp add: subassms)
    qed
    thus ‹∃R. lts_tau.trace_inclusion step τ R ∧ R p q›
      using Rpq by auto
  next 
    assume ‹∃R. lts_tau.trace_inclusion step τ R ∧ R p q›
    then obtain R where weak_sim_R: ‹lts_tau.trace_inclusion step τ R›
      and Rpq: ‹R p q›
      by blast
    have ‹lts_tau.trace_inclusion step2 τ R› 
      unfolding lts_tau.trace_inclusion_def
    proof clarify
      fix p q p' A
      assume subassms: 
        ‹∀a∈set A. a ≠ τ›
        ‹R p q›
        ‹?weak_seq2 p A p'›
      thus ‹∃q'. ?weak_seq2 q A q'›
        using step2_to_step step_to_step2
        by (metis (full_types) lts_tau.trace_inclusion_def weak_sim_R)
    qed
    thus ‹∃R. lts_tau.trace_inclusion step2 τ R ∧ R p q› using Rpq by auto
  qed
qed

end