Theory After

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : The After operator
 *
 * Copyright (c) 2023 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

chapter ‹ Construction of the After Operator ›

theory  After
  imports ReadySet
begin


text ‹Now that we have defined \<^term>‹ready_set P›, we can talk about what
      happens to \<^term>‹P› after an event belonging to this set.›

section ‹Definition›

text ‹We want to define a new operator on a process \<^term>‹P› which would in
      some way be the reciprocal of the prefix operator \<^term>‹e → P›.›

text ‹The intuitive way of doing so is to only keep the tails of the traces
      beginning by \<^term>‹ev e› (and similar for failures and divergences).
      However we have an issue if \<^term>‹ev e ∉ ready_set P› i.e. if no trace of
      \<^term>‹P› begins with \<^term>‹ev e›: the result would no longer verify the 
      invariant \<^const>‹is_process› because its trace set would be empty.
      We must therefore distinguish this case and we agree to then obtain \<^const>‹STOP›.
      This convention is not really decisive since we will only use this operator
      when \<^term>‹ev e ∈ ready_set P› to define operational semantics.›


lift_definition After :: ‹['α process, 'α] ⇒ 'α process› (infixl ‹after› 77)
  is ‹λP e.   if ev e ∈ ready_set P
            then ({(tl s, X)| s X. (s, X) ∈ ℱ P ∧ s ≠ [] ∧ hd s = ev e},
                  { tl s    | s  .  s     ∈ 𝒟 P ∧ s ≠ [] ∧ hd s = ev e})
            else ({(s, X). s = []}, {})›
proof -
  show ‹?thesis P e› (is ‹is_process (if ev e ∈ ready_set P then (?f, ?d) 
                                      else ({(s, X). s = []}, {}))›) for P e
  proof (split if_split, intro conjI impI)
    show ‹is_process ({(s, X). s = []}, {})› by (metis STOP.rsp eq_onp_def)
  next
    assume ready: ‹ev e ∈ ready_set P›
    show ‹is_process (?f, ?d)›
      unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
    proof (intro conjI impI allI)
      show ‹([], {}) ∈ ?f›
        using ready[unfolded ready_set_def T_F_spec[symmetric]] by force
    next
      show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
        by simp (metis butlast_rev butlast_tl front_tickFree_def is_processT2 tickFree_butlast)
    next
      show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
        by simp (metis (no_types, opaque_lifting) append_Cons is_processT3 
                                                  list.sel(1, 3) neq_Nil_conv)
    next
      show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
        using is_processT4 by simp blast
    next
      show ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟹ (s, X ∪ Y) ∈ ?f› for s X Y
        using ready[unfolded ready_set_def T_F_spec[symmetric]]
        by auto (metis Nil_is_append_conv hd_append2 is_processT5 tl_append2)
    next
      show ‹(s @ [✓], {}) ∈ ?f ⟹ (s, X - {✓}) ∈ ?f› for s X
        by simp (metis (no_types, lifting) Cons_eq_appendI is_processT6 list.collapse 
                                           list.distinct(1) list.sel(1, 3))
    next
      fix s t :: ‹'α trace›
      assume ‹s ∈ ?d ∧ tickFree s ∧ front_tickFree t›
      hence ‹s @ t = tl (ev e # s @ t) ∧ ev e # s @ t ∈ 𝒟 P ∧ 
             ev e # s @ t ≠ [] ∧ hd (ev e # s @ t) = ev e›
        by simp (metis append_Cons event.distinct(1) is_processT7_S
                       list.sel(1, 3) neq_Nil_conv tickFree_Cons)
      show ‹s @ t ∈ ?d›
        apply simp 
        using ‹?this› by blast
    next
      show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X
        using NF_ND by blast
    next
      show ‹s @ [✓] ∈ ?d ⟹ s ∈ ?d› for s
        by auto (metis Cons_eq_appendI is_processT9_S_swap list.sel(1, 3) neq_Nil_conv)
    qed
  qed
qed




section ‹Projections›

lemma F_After:
  ‹ℱ (P after e) = (   if ev e ∈ ready_set P
                     then {(tl s, X)| s X. (s, X) ∈ ℱ P ∧ s ≠ [] ∧ hd s = ev e}
                     else {(s, X). s = []})›
  by (simp add: Failures_def After.rep_eq FAILURES_def)
  (* by (simp add: Failures.rep_eq After.rep_eq FAILURES_def) *)

lemma D_After:
  ‹𝒟 (P after e) = (   if ev e ∈ ready_set P
                     then {tl s| s. s ∈ 𝒟 P ∧ s ≠ [] ∧ hd s = ev e}
                     else {})› 
  by (simp add: Divergences_def After.rep_eq DIVERGENCES_def)
  (* by (simp add: Divergences.rep_eq After.rep_eq DIVERGENCES_def) *)


lemma T_After:
  ‹𝒯 (P after e) = (   if ev e ∈ ready_set P
                     then {tl s| s. s ∈ 𝒯 P ∧ s ≠ [] ∧ hd s = ev e}
                     else {[]})›
  by (auto simp add: T_F_spec[symmetric] F_After)


lemma not_ready_After: ‹ev e ∉ ready_set P ⟹ P after e = STOP›
  by (simp add: STOP_iff_T T_After)

lemma ready_set_After: ‹ready_set (P after e) = {a. ev e # [a] ∈ 𝒯 P}›
  apply (simp add: T_After ready_set_def, safe)
    apply (metis list.exhaust_sel)
   apply (metis list.discI list.sel(1, 3))
  by (simp add: is_processT3_ST_pref le_list_def)



section ‹Monotony›

lemma mono_After : ‹P after e ⊑ Q after e› if ‹P ⊑ Q›
proof (subst le_approx_def, safe)
  from that[THEN anti_mono_ready_set] that[THEN le_approx1]
  show ‹s ∈ 𝒟 (Q after e) ⟹ s ∈ 𝒟 (P after e)› for s
    by (simp add: D_After ready_set_def subset_iff split: if_split_asm) blast
next
  from that[THEN anti_mono_ready_set] that[THEN le_approx2]
  show ‹s ∉ 𝒟 (P after e) ⟹ X ∈ ℛ⇩a (P after e) s ⟹ X ∈ ℛ⇩a (Q after e) s› for s X
  (* show ‹∀s. s ∉ 𝒟 (P after e) ⟶ ℛ⇩a (P after e) s = ℛ⇩a (Q after e) s› *)
    apply (simp add: Ra_def D_After F_After ready_set_def subset_iff split: if_split_asm)
    by (metis F_T append_Cons append_Nil is_processT3_ST list.exhaust_sel) blast
next
  from that[THEN anti_mono_ready_set] that[THEN le_approx2]
  show ‹s ∉ 𝒟 (P after e) ⟹ X ∈ ℛ⇩a (Q after e) s ⟹ X ∈ ℛ⇩a (P after e) s› for s X
    apply (simp add: Ra_def D_After F_After ready_set_def subset_iff split: if_split_asm)
    by blast (metis T_F_spec list.distinct(1) list.sel(1, 3))
next
  show ‹s ∈ min_elems (𝒟 (P after e)) ⟹ s ∈ 𝒯 (Q after e)› for s 
  proof (cases ‹P = ⊥›)
    assume ‹s ∈ min_elems (𝒟 (P after e))› and ‹P = ⊥›
    hence ‹s = []›
      by (simp add: BOT_iff_D D_After ready_set_BOT D_UU min_elems_def)
         (metis front_tickFree_single less_list_def list.distinct(1) list.sel(1, 3) nil_le)
    thus ‹s ∈ 𝒯 (Q after e)› by (simp add: Nil_elem_T)
  next
    assume assms : ‹P ≠ ⊥› ‹s ∈ min_elems (𝒟 (P after e))›
    from assms(2)[THEN elem_min_elems] have * : ‹ev e # s ∈ 𝒟 P› 
      by (simp add: D_After split: if_split_asm) (metis list.collapse)
    { assume ‹ev e # s ∉ min_elems (𝒟 P)›
      with assms(1) "*" obtain a t where ‹a # t ∈ 𝒟 P› ‹a # t < ev e # s›
        by (simp add: BOT_iff_D min_elems_def) (metis list.exhaust)
      hence ‹a = ev e ∧ t < s ∧ t ∈ 𝒟 (P after e)›
        by (simp add: le_list_def less_list_def D_After) 
           (metis Cons_in_T_imp_elem_ready_set D_T list.discI list.sel(1, 3))
      hence False by (metis assms(2) less_list_def min_elems_no)
    }
    hence ‹ev e # s ∈ min_elems (𝒟 P)› by blast
    with le_approx3 that have ‹ev e # s ∈ 𝒯 Q› by blast
    thus ‹s ∈ 𝒯 (Q after e)›
      by (simp add: T_After)
         (metis Cons_in_T_imp_elem_ready_set list.discI list.sel(1, 3))
  qed
qed


lemma mono_After_T : ‹P ⊑⇩T Q ⟹ P after e ⊑⇩T Q after e›
  by (auto simp add: trace_refine_def T_After ready_set_def)
     (metis list.distinct(1) list.sel(1, 3))

lemma mono_After_F :
  ‹P ⊑⇩F Q ⟹ ev e ∉ ready_set P ∨ ev e ∈ ready_set Q ⟹
   P after e ⊑⇩F Q after e›
  using F_subset_imp_T_subset 
  by (auto simp add: failure_refine_def F_After ready_set_def)

lemma mono_After_D : ‹P ⊑⇩D Q ⟹ P after e ⊑⇩D Q after e›
  by (auto simp add: divergence_refine_def D_After ready_set_def)
     (metis Cons_eq_appendI NT_ND append_self_conv2 is_processT3_ST list.collapse subset_iff)

lemma mono_After_FD :
  ‹P ⊑⇩F⇩D Q ⟹ ev e ∉ ready_set P ∨ ev e ∈ ready_set Q ⟹ 
   P after e ⊑⇩F⇩D Q after e›
  using F_subset_imp_T_subset
  by (simp add: failure_divergence_refine_def le_ref_def F_After D_After ready_set_def) blast

lemma mono_After_DT : ‹P ⊑⇩D⇩T Q ⟹ P after e ⊑⇩D⇩T Q after e›
  by (simp add: mono_After_D mono_After_T trace_divergence_refine_def)


  


section ‹Behaviour of @{const [source] After} with \<^const>‹STOP›, \<^const>‹SKIP› and \<^term>‹⊥››

lemma After_STOP: ‹STOP after e = STOP›
  by (simp add: STOP_iff_T T_After ready_set_STOP)

lemma After_is_STOP_iff:
  ‹P after e = STOP ⟷ (∀s. ev e # s ∈ 𝒯 P ⟶ s = [])›
  apply (simp add: STOP_iff_T T_After ready_set_def, safe)
     apply fastforce
    apply (metis list.collapse) 
  using is_processT3_ST by force+
  

lemma After_SKIP: ‹SKIP after e = STOP›
  by (simp add: STOP_iff_T T_After ready_set_SKIP)

 
lemma After_BOT: ‹⊥ after e = ⊥›
  by (force simp add: BOT_iff_D D_After ready_set_BOT D_UU)

lemma After_is_BOT_iff: ‹P after e = ⊥ ⟷ [ev e] ∈ 𝒟 P›
  using hd_Cons_tl by (force simp add: BOT_iff_D D_After ready_set_def D_T)




section ‹Behaviour of @{const [source] After} with Operators of \<^session>‹HOL-CSP››

subsection ‹Loss of Determinism›

text ‹A first interesting observation is that the @{const [source] After} 
      operator leads to the loss of determinism.›

lemma After_Mprefix_is_After_Mndetprefix:
  ‹(□a ∈ A → P a) after e = (⊓a ∈ A → P a) after e›
  by (subst Process_eq_spec)
     (force simp add: ready_set_Mprefix ready_set_Mndetprefix F_After D_After 
                      F_Mprefix D_Mprefix F_Mndetprefix D_Mndetprefix write0_def)

lemma After_Det_is_After_Ndet: ‹P □ Q after e = P ⊓ Q after e›
  by (subst Process_eq_spec)
     (auto simp add: ready_set_Det ready_set_Ndet F_After D_After F_Det F_Ndet D_Det D_Ndet)


lemma After_Ndet: 
  ‹P ⊓ Q after e = 
   (     if ev e ∉ ready_set P ∧ ev e ∉ ready_set Q then STOP 
    else if ev e ∈ ready_set P ∧ ev e ∈ ready_set Q then (P after e) ⊓ (Q after e)
    else if ev e ∈ ready_set P then P after e else Q after e)›
  (is ‹P ⊓ Q after e =
       (if ?c1 then STOP else if ?c2 then (P after e) ⊓ (Q after e) else
        if ?c3 then P after e else Q after e)›)
proof -
  have ‹?c1 ⟹ P ⊓ Q after e = STOP›
    by (simp add: Process_eq_spec F_After D_After ready_set_Ndet F_STOP D_STOP)
  moreover have ‹?c2 ⟹ P ⊓ Q after e = (P after e) ⊓ (Q after e)›
    by (auto simp add: Process_eq_spec F_After D_After F_Ndet D_Ndet ready_set_Ndet)
  moreover have ‹¬ ?c2 ⟹ ?c3 ⟹ P ⊓ Q after e = P after e›
            and ‹¬ ?c2 ⟹ ¬ ?c3 ⟹ P ⊓ Q after e = Q after e›
    by (auto simp add: Process_eq_spec F_After D_After F_Ndet D_Ndet ready_set_Ndet)
       (metis Cons_in_T_imp_elem_ready_set F_T list.collapse,
        metis Cons_in_T_imp_elem_ready_set D_T list.collapse)+
  ultimately show ?thesis by presburger
qed
  

lemma After_Mprefix: ‹(□ a ∈ A → P a) after e = (if e ∈ A then P e else STOP)›
  by (subst Process_eq_spec, auto simp add: F_After D_After ready_set_Mprefix
                                            F_Mprefix D_Mprefix F_STOP D_STOP)
     (metis image_eqI list.distinct(1) list.sel(1, 3))+


lemmas After_Det = After_Ndet[folded After_Det_is_After_Ndet]
   and After_Mndetprefix = After_Mprefix[unfolded After_Mprefix_is_After_Mndetprefix]
   and After_prefix = After_Mprefix[of ‹{a}› ‹λa. P›, folded write0_def, simplified] for a P


lemma ‹(e → P) after e = P› by (simp add: After_prefix) 

text ‹This result justifies seeing \<^term>‹P after e› as the reciprocal operator of the 
      prefix \<^term>‹e → P›.

      However, we lose information with @{const [source] After}: in general,
      \<^term>‹e → (P after e) ≠ P› (even when \<^term>‹ev e ∈ ready_set P› and \<^term>‹P ≠ ⊥›).›

lemma ‹∃P. (e → (P after e) ≠ P)›
proof (intro exI)
  show ‹e → (SKIP after e) ≠ SKIP›
    by (metis Par_SKIP_SKIP SKIP_Neq_STOP prefix_Par_SKIP)
qed

lemma ‹∃P. ev e ∈ ready_set P ∧ (e → (P after e) ≠ P)›
proof (intro exI)
  show ‹ev e ∈ ready_set ⊥ ∧ (e → (⊥ after e) ≠ ⊥)›
    by (simp add: ready_set_BOT Mprefix_neq_BOT write0_def)
qed

lemma ‹∃P. ev e ∈ ready_set P ∧ P ≠ ⊥ ∧ (e → (P after e) ≠ P)›
proof (intro exI)
  define P where P_def: ‹P = (e → STOP) □ SKIP›
  have * : ‹ev e ∈ ready_set P› by (simp add: P_def ready_set_Det ready_set_prefix)
  moreover have ‹P ≠ ⊥› 
    by (simp add: Det_is_BOT_iff Mprefix_neq_BOT P_def SKIP_neq_BOT write0_def)
  moreover have ‹e → (P after e) = (e → STOP)›
    by (rule arg_cong[where f = ‹λP. (e → P)›])
       (simp add: P_def After_Det ready_set_SKIP ready_set_prefix After_prefix)
  moreover have ‹e → STOP ≠ P›
    apply (rule contrapos_nn[of ‹ready_set (e → STOP) = ready_set P› ‹e → STOP = P›])
    by (simp add: P_def ready_set_Det ready_set_prefix ready_set_SKIP)
       (erule arg_cong)
  ultimately show ‹ev e ∈ ready_set P ∧ P ≠ ⊥ ∧ (e → (P after e) ≠ P)› by presburger
qed



subsection ‹@{const [source] After} Sequential Composition›

text ‹The first goal is to obtain an equivalent of 
      @{thm Mprefix_Seq[of ‹{e}› ‹λa. P› Q, folded write0_def]}.
      But in order to be exhaustive we also have to consider the possibility of \<^term>‹Q› taking
      the lead when \<^term>‹✓ ∈ ready_set P› in the sequential composition \<^term>‹P ❙; Q›.›

lemma not_skippable_or_not_readyR_After_Seq: ‹(P ❙; Q) after e = P after e ❙; Q›
  if ‹✓ ∉ ready_set P ∨ ev e ∉ ready_set Q›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ (P ❙; Q) after e = P after e ❙; Q›
    by (simp add: BOT_Seq After_BOT)
next
  assume non_BOT: ‹P ≠ ⊥›
  show ‹(P ❙; Q) after e = P after e ❙; Q›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ((P ❙; Q) after e)›
    hence * : ‹ev e # s ∈ 𝒟 (P ❙; Q)›
      by (simp add: D_After split: if_split_asm) (metis list.exhaust_sel)
    then consider ‹ev e # s ∈ 𝒟 P› 
      | ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q›
      by (simp add: D_Seq) blast
    thus ‹s ∈ 𝒟 (P after e ❙; Q)›
    proof cases
      show ‹ev e # s ∈ 𝒟 P ⟹ s ∈ 𝒟 (P after e ❙; Q)›
        by (simp add: D_Seq D_After)
           (metis Cons_in_T_imp_elem_ready_set D_T list.discI list.sel(1, 3))
    next
      assume ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q›
      then obtain t1 t2 where ** : ‹ev e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q› by blast
      have ‹t1 ≠ []› by (metis "**" Cons_in_T_imp_elem_ready_set D_T self_append_conv2 that)
      with "**"(1) obtain t1'
        where ‹t1 = ev e # t1'› ‹s = t1' @ t2› by (metis Cons_eq_append_conv)
      with "**"(2, 3) show ‹s ∈ 𝒟 (P after e ❙; Q)›
        by (simp add: D_Seq T_After)
           (metis Cons_in_T_imp_elem_ready_set list.distinct(1) list.sel(1, 3))
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 (P after e ❙; Q)›
    hence ‹ev e # s ∈ 𝒟 P ∨ (∃t1 t2. s = t1 @ t2 ∧ ev e # t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q)›
      by (simp add: D_Seq D_After T_After split: if_split_asm) (metis list.collapse)
    hence ‹ev e # s ∈ 𝒟 (P ❙; Q)›
      by (elim disjE; simp add: D_Seq) (metis append_Cons)
    thus ‹s ∈ 𝒟 ((P ❙; Q) after e)›
      by (simp add: D_After)
         (metis Cons_in_T_imp_elem_ready_set D_T list.discI list.sel(1, 3))
  next
    fix s X
    assume same_div : ‹𝒟 ((P ❙; Q) after e) = 𝒟 (P after e ❙; Q)›
    assume ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
    then consider ‹ev e ∈ ready_set (P ❙; Q)› ‹(ev e # s, X) ∈ ℱ (P ❙; Q)›
      | ‹ev e ∉ ready_set (P ❙; Q)› ‹s = []›
      by (simp add: F_After split: if_split_asm) (metis list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ (P after e ❙; Q)›
    proof cases
      assume assms : ‹ev e ∈ ready_set (P ❙; Q)› ‹(ev e # s, X) ∈ ℱ (P ❙; Q)›
      from assms(2) consider ‹ev e # s ∈ 𝒟 (P ❙; Q)›
        | ‹(ev e # s, insert ✓ X) ∈ ℱ P› ‹tickFree s›
        | ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q›
        by (simp add: F_Seq D_Seq) blast
      thus ‹(s, X) ∈ ℱ (P after e ❙; Q)›
      proof cases
        assume ‹ev e # s ∈ 𝒟 (P ❙; Q)›
        hence ‹s ∈ 𝒟 ((P ❙; Q) after e)›
          by (simp add: D_After assms(1)) (metis list.distinct(1) list.sel(1, 3))
        with same_div D_F show ‹(s, X) ∈ ℱ (P after e ❙; Q)› by blast
      next
        show ‹(ev e # s, insert ✓ X) ∈ ℱ P ⟹ tickFree s ⟹ (s, X) ∈ ℱ (P after e ❙; Q)›
          by (simp add: F_Seq F_After)
             (metis Cons_in_T_imp_elem_ready_set F_T list.distinct(1) list.sel(1, 3))
      next
        assume ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q›
        then obtain t1 t2 where * : ‹ev e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q› by blast
        have ‹t1 ≠ []› by (metis "*" Cons_in_T_imp_elem_ready_set F_T self_append_conv2 that)
        with "*"(1) obtain t1'
          where ‹t1 = ev e # t1'› ‹s = t1' @ t2› by (metis Cons_eq_append_conv)
        with "*"(2, 3) show ‹(s, X) ∈ ℱ (P after e ❙; Q)›
          by (simp add: F_Seq T_After)
             (metis Cons_in_T_imp_elem_ready_set list.distinct(1) list.sel(1, 3))
      qed
    next
      show ‹ev e ∉ ready_set (P ❙; Q) ⟹ s = [] ⟹ (s, X) ∈ ℱ (P after e ❙; Q)›
        by (simp add: F_Seq F_After non_BOT ready_set_Seq)
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ((P ❙; Q) after e) = 𝒟 (P after e ❙; Q)›
    assume ‹(s, X) ∈ ℱ (P after e ❙; Q)›
    then consider ‹s ∈ 𝒟 (P after e ❙; Q)›
      | ‹(s, insert ✓ X) ∈ ℱ (P after e)› ‹tickFree s›
      | ‹∃t1 t2. s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 (P after e) ∧ (t2, X) ∈ ℱ Q›
      by (simp add: F_Seq D_Seq) blast
    thus ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
    proof cases
      from same_div D_F show ‹s ∈ 𝒟 (P after e ❙; Q) ⟹ (s, X) ∈ ℱ ((P ❙; Q) after e)› by blast
    next
      from that show ‹(s, insert ✓ X) ∈ ℱ (P after e) ⟹ tickFree s ⟹
                      (s, X) ∈ ℱ ((P ❙; Q) after e)›
        by (simp add: F_After ready_set_Seq F_Seq non_BOT split: if_split_asm)
           (metis event.distinct(1) list.collapse tickFree_Cons)
    next
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 (P after e) ∧ (t2, X) ∈ ℱ Q›
      then obtain t1 t2
        where * : ‹s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 (P after e)› ‹(t2, X) ∈ ℱ Q› by blast
      from "*"(2) have ‹ev e # t1 @ [✓] ∈ 𝒯 P›
        by (simp add: T_After split: if_split_asm) (metis list.exhaust_sel)
      with "*"(1, 3) show ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
        by (simp add: F_After F_Seq ready_set_Seq non_BOT)
           (metis Cons_in_T_imp_elem_ready_set append_Cons list.distinct(1) list.sel(1, 3))
    qed
  qed
qed


lemma ‹(P ❙; STOP) after e = P after e ❙; STOP›
  by (simp add: not_skippable_or_not_readyR_After_Seq ready_set_STOP)


lemma skippable_not_readyL_After_Seq: ‹(P ❙; Q) after e = Q after e› 
  if ‹✓ ∈ ready_set P› and ‹ev e ∉ ready_set P›
proof (cases ‹P = ⊥›)
  from that(2) ready_set_BOT show ‹P = ⊥ ⟹ (P ❙; Q) after e = Q after e› by blast
next
  assume non_BOT : ‹P ≠ ⊥›
  show ‹(P ❙; Q) after e = Q after e›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ((P ❙; Q) after e)›
    hence ‹ev e # s ∈ 𝒟 (P ❙; Q)›
      by (simp add: D_After split: if_split_asm) (metis list.exhaust_sel)
    with that(2) obtain t1 t2 where * : ‹ev e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
      by (simp add: D_Seq) (meson Cons_in_T_imp_elem_ready_set NT_ND)
    from "*"(1, 2) that(2) Cons_in_T_imp_elem_ready_set have ‹t1 = []›
      by (cases t1; simp) blast
    with "*" show ‹s ∈ 𝒟 (Q after e)›
      by (simp add: D_After)
         (metis Cons_in_T_imp_elem_ready_set D_T list.discI list.sel(1, 3))
  next
    show ‹s ∈ 𝒟 (Q after e) ⟹ s ∈ 𝒟 ((P ❙; Q) after e)› for s
      by (simp add: D_After D_Seq ready_set_Seq non_BOT that split: if_split_asm)
         (metis append_Nil mem_Collect_eq ready_set_def that(1))
  next
    fix s X
    assume same_div : ‹𝒟 ((P ❙; Q) after e) = 𝒟 (Q after e)›
    assume ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
    then consider ‹ev e ∈ ready_set (P ❙; Q)› ‹(ev e # s, X) ∈ ℱ (P ❙; Q)›
      | ‹ev e ∉ ready_set (P ❙; Q)› ‹s = []›
      by (simp add: F_After split: if_split_asm) (metis list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ (Q after e)›
    proof cases
      show ‹ev e ∈ ready_set (P ❙; Q) ⟹ (ev e # s, X) ∈ ℱ (P ❙; Q) ⟹
            (s, X) ∈ ℱ (Q after e)›
        by (simp add: F_After F_Seq)
           (metis Cons_in_T_imp_elem_ready_set D_T F_T append_Nil hd_append2 
                  is_processT3_ST list.exhaust_sel list.sel(1, 3) that(2))
    next
      show ‹ev e ∉ ready_set (P ❙; Q) ⟹ s = [] ⟹ (s, X) ∈ ℱ (Q after e)›
        by (simp add: F_After ready_set_Seq non_BOT that)
    qed
  next
    show ‹(s, X) ∈ ℱ (Q after e) ⟹ (s, X) ∈ ℱ ((P ❙; Q) after e)› for s X
      by (simp add: F_After F_Seq ready_set_Seq non_BOT that split: if_split_asm)
         (metis append_Nil mem_Collect_eq ready_set_def that(1))
  qed
qed


lemma skippable_readyL_readyR_After_Seq: ‹(P ❙; Q) after e = (P after e ❙; Q) ⊓ (Q after e)›
  if ‹✓ ∈ ready_set P› ‹ev e ∈ ready_set P› ‹ev e ∈ ready_set Q›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ (P ❙; Q) after e = (P after e ❙; Q) ⊓ (Q after e)›
    by (simp add: BOT_Seq After_BOT Ndet_commute[of ⊥, simplified Ndet_BOT])
next
  assume non_BOT : ‹P ≠ ⊥›
  show ‹(P ❙; Q) after e = (P after e ❙; Q) ⊓ (Q after e)›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ((P ❙; Q) after e)›
    hence ‹ev e # s ∈ 𝒟 (P ❙; Q)›
      by (simp add: D_After ready_set_Seq non_BOT that(2)) (metis list.exhaust_sel)
    then consider ‹ev e # s ∈ 𝒟 P›
      | ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q›
      by (simp add: D_Seq) blast
    thus ‹s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
    proof cases
      show ‹ev e # s ∈ 𝒟 P ⟹ s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
        by (simp add: D_After D_Seq D_Ndet non_BOT that)
           (metis list.distinct(1) list.sel(1, 3))
    next
      assume ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q›
      then obtain t1 t2 where * : ‹ev e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q› by blast
      show ‹s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
      proof (cases ‹t1 = []›)
        from "*"(1, 3) show ‹t1 = [] ⟹ s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
          by (simp add: D_After D_Ndet that(3))
             (metis list.distinct(1) list.sel(1, 3))
      next
        assume ‹t1 ≠ []›
        with "*"(1, 3) obtain t1' where ‹t1 = ev e # t1'› by (cases t1; simp)
        with "*" show ‹s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
          by (simp add: T_After D_Seq D_Ndet that(2))
             (metis list.distinct(1) list.sel(1, 3))
      qed
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
    then consider ‹s ∈ 𝒟 (P after e ❙; Q)› | ‹s ∈ 𝒟 (Q after e)›
      by (simp add: D_Ndet) blast
    thus ‹s ∈ 𝒟 ((P ❙; Q) after e)›
    proof cases
      show ‹s ∈ 𝒟 (P after e ❙; Q) ⟹ s ∈ 𝒟 ((P ❙; Q) after e)›
        apply (simp add: D_After T_After D_Seq ready_set_Seq non_BOT that(2), elim disjE)
        by blast (metis append_Cons list.distinct(1) list.exhaust_sel list.sel(1, 3))
    next
      from that show ‹s ∈ 𝒟 (Q after e) ⟹ s ∈ 𝒟 ((P ❙; Q) after e)›
        by (simp add: D_After D_Seq ready_set_Seq non_BOT)
           (metis append_Nil mem_Collect_eq ready_set_def)
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ((P ❙; Q) after e) = 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
    assume ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
    hence ‹(ev e # s, X) ∈ ℱ (P ❙; Q)›
      by (simp add: F_After ready_set_Seq non_BOT that(2)) (metis list.exhaust_sel)
    then consider ‹ev e # s ∈ 𝒟 P›
      | ‹(ev e # s, insert ✓ X) ∈ ℱ P› ‹tickFree s›
      | ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q›
      by (simp add: F_Seq D_Seq) blast
    thus ‹(s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
    proof cases
      assume ‹ev e # s ∈ 𝒟 P›
      hence ‹s ∈ 𝒟 (P after e ❙; Q)› 
        by (simp add: D_After D_Seq that(2)) (metis list.distinct(1) list.sel(1, 3))
      with same_div D_Ndet D_F show ‹(s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))› by blast
    next
      show ‹(ev e # s, insert ✓ X) ∈ ℱ P ⟹ tickFree s ⟹
            (s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
        by (simp add: F_Ndet F_Seq F_After that(2))
           (metis list.distinct(1) list.sel(1, 3))
    next
      assume ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q›
      then obtain t1 t2
        where * : ‹ev e # s = t1 @ t2› ‹t1 @ [✓] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q› by blast
      show ‹(s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
      proof (cases ‹t1 = []›)
        from "*"(1, 3) show ‹t1 = [] ⟹ (s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
          by (simp add: F_Ndet F_Seq F_After that(2, 3))
             (metis list.distinct(1) list.sel(1, 3))
      next
        assume ‹t1 ≠ []›
        with "*"(1, 3) obtain t1' where ‹t1 = ev e # t1'› by (cases t1; simp)
        with "*" show ‹(s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
          by (simp add: F_Ndet F_Seq F_After T_After that(2))
             (metis list.distinct(1) list.sel(1, 3))
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ((P ❙; Q) after e) = 𝒟 ((P after e ❙; Q) ⊓ (Q after e))›
    assume ‹(s, X) ∈ ℱ ((P after e ❙; Q) ⊓ (Q after e))›
    then consider ‹(s, X) ∈ ℱ (P after e ❙; Q)› | ‹(s, X) ∈ ℱ (Q after e)›
      by (simp add: F_Ndet) blast
    thus ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
    proof cases
      assume ‹(s, X) ∈ ℱ (P after e ❙; Q)›
      then consider ‹s ∈ 𝒟 (P after e ❙; Q)›
        | ‹(s, insert ✓ X) ∈ ℱ (P after e)› ‹tickFree s›
        | ‹∃t1 t2. s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 (P after e) ∧ (t2, X) ∈ ℱ Q›
        by (simp add: F_Seq D_Seq) blast
      thus ‹(s, X) ∈ ℱ ((P ❙; Q) after e)›
      proof cases
        show ‹s ∈ 𝒟 (P after e ❙; Q) ⟹ (s, X) ∈ ℱ ((P ❙; Q) after e)›
          using same_div D_Ndet D_F by blast
      next
        show ‹(s, insert ✓ X) ∈ ℱ (P after e) ⟹ tickFree s ⟹ (s, X) ∈ ℱ ((P ❙; Q) after e)›
          by (simp add: F_After F_Seq ready_set_Seq that(2))
             (metis event.distinct(1) list.collapse tickFree_Cons)
      next
        show ‹∃t1 t2. s = t1 @ t2 ∧ t1 @ [✓] ∈ 𝒯 (P after e) ∧ (t2, X) ∈ ℱ Q ⟹
                      (s, X) ∈ ℱ ((P ❙; Q) after e)›
          by (simp add: F_After T_After F_Seq ready_set_Seq non_BOT that(2))
             (metis append_Cons list.distinct(1) list.exhaust_sel list.sel(1, 3))
      qed
    next
      show ‹(s, X) ∈ ℱ (Q after e) ⟹ (s, X) ∈ ℱ ((P ❙; Q) after e)›
        by (simp add: F_After F_Seq ready_set_Seq that(3))
           (metis append_Nil mem_Collect_eq ready_set_def that(1))
    qed
  qed
qed


lemma not_readyL_not_skippable_or_not_readyR_After_Seq:
  ‹ev e ∉ ready_set P ⟹ ✓ ∉ ready_set P ∨ ev e ∉ ready_set Q ⟹ 
   (P ❙; Q) after e = STOP› 
  by (simp add: not_skippable_or_not_readyR_After_Seq STOP_Seq not_ready_After)
 

lemma After_Seq:
  ‹(P ❙; Q) after e = 
   (     if ev e ∉ ready_set P ∧ ev e ∉ ready_set Q then STOP
    else if ev e ∉ ready_set Q then P after e ❙; Q
    else if ev e ∉ ready_set P then if ✓ ∈ ready_set P then Q after e else STOP
    else if  ✓   ∈ ready_set P then (P after e ❙; Q) ⊓ (Q after e) else P after e ❙; Q)›
  by (simp add: STOP_Seq not_ready_After not_skippable_or_not_readyR_After_Seq 
                skippable_not_readyL_After_Seq skippable_readyL_readyR_After_Seq)


subsection ‹@{const [source] After} Synchronization›

text ‹Now let's focus on \<^const>‹Sync›.
      We want to obtain an equivalent of

      @{thm Mprefix_Sync_distr}

      We will also divide the task.›

text ‹@{const [source] After} version of

      @{thm Mprefix_Sync_distr_left
      [of ‹{e}› _ _ ‹λa. P›, folded write0_def, simplified]}.›

lemma tickFree_tl: ‹tickFree s ⟹ tickFree(tl s)›
  ―‹Remove this lemma, already in future versions of \<^session>‹HOL-CSP›.›
  by (metis Nil_tl tickFree_tl)

lemma readyL_not_readyR_not_in_After_Sync:
  ‹(P ⟦S⟧ Q) after e = P after e ⟦S⟧ Q›
  if ready_hyps: ‹ev e ∈ ready_set P› ‹ev e ∉ ready_set Q› and notin: ‹e ∉ S›
proof (subst Process_eq_spec_optimized, safe)

  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
       and same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q)›
    have ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)›
    proof (cases ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›)
      case True
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e)›
        by (force simp add: D_After ready_set_Sync ready_hyps(1) assms(1, 2) notin)
      thus ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)› using NF_ND same_div by blast
    next
      case False
      with assms(3) obtain s_P s_Q X_P X_Q 
        where * : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q› 
                  ‹(ev e # s) setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_Sync D_Sync) blast
      have ** : ‹s_P ≠ [] ∧ hd s_P = ev e ∧ s setinterleaves ((tl s_P, s_Q), insert ✓ (ev ` S))›
        using *(3) by (cases s_P; cases s_Q, auto split: if_split_asm)
                      (metis *(2) After_is_STOP_iff CollectI F_T not_ready_After
                             ready_set_def ready_hyps(2))+
      hence ‹(tl s_P, X_P) ∈ ℱ (P after e) ∧ (s_Q, X_Q) ∈ ℱ Q ∧
             s setinterleaves ((tl s_P, s_Q), insert ✓ (ev ` S)) ∧
             X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
        apply (simp add: F_After "**" ready_hyps(1))
        using "*"(1, 2, 4) "**" by blast
      thus ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    qed
  } note * = this

  show ‹(s, X) ∈ ℱ ((P ⟦S⟧ Q) after e) ⟹ (s, X) ∈ ℱ (P after e ⟦S⟧ Q)› 
      if same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q)› for s X
    apply (simp add: F_After ready_set_Sync ready_hyps notin image_iff 
              split: if_split_asm)
     apply (erule disjE; 
            simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT F_UU,
            metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "*" list.exhaust_sel same_div)
next

  fix s X
  assume same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q)›
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)›
    from assms(3) consider
      ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ (P after e) ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                          s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S)) ∧ 
                          X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
      by (simp add: F_Sync D_Sync) blast
    hence ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q
        where * : ‹(ev e # s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q› 
                  ‹s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_After ready_hyps(1)) (metis list.collapse)
      have ‹(s_Q, X_Q) ∈ ℱ Q ∧ 
            (ev e # s) setinterleaves ((ev e # s_P, s_Q), insert ✓ (ev ` S)) ∧
             X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
        apply (simp add: *(2, 4))
        using *(3) by (cases s_Q; simp add: notin image_iff)
      with "*"(1) show ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    next
      case 2
      from "2"[simplified same_div[symmetric]]
      have ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)› 
        by (simp add: D_After ready_hyps(1) ready_set_Sync 
                      assms(1, 2) notin image_iff, metis list.collapse)
      thus ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)› using NF_ND by blast
    qed
  }
  thus ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after e)› 
    by (simp add: F_After ready_set_Sync ready_hyps After_BOT F_UU image_iff
                     Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT notin)
       (metis butlast.simps(2) event.distinct(1) front_tickFree_butlast front_tickFree_single
              list.distinct(1) list.sel(1, 3) process_charn tickFree_Cons)
next

  { fix s
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
    from assms(3) obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹ev e # s = r @ v› 
                ‹r setinterleaves ((t, u), insert ✓ (ev ` S))›
                ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by (simp add: D_Sync) blast
    have ** : ‹r ≠ [] ∧ hd r = ev e›
      by (metis "*"(3, 4, 5) BOT_iff_D assms(1, 2) empty_setinterleaving hd_append list.sel(1))
    hence *** : ‹(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ⟶ t ≠ [] ∧ hd t = ev e ∧ 
                              tl r setinterleaves ((tl t, u), insert ✓ (ev ` S))) ∧ 
                 (t ∈ 𝒟 Q ∧ u ∈ 𝒯 P ⟶ u ≠ [] ∧ hd u = ev e ∧ 
                              tl r setinterleaves ((t, tl u), insert ✓ (ev ` S)))›
      using *(4) assms(1, 2)[simplified BOT_iff_D] ready_hyps[simplified ready_set_def]
      apply (cases t; cases u; simp split: if_split_asm)
      by (safe; simp; metis [[metis_verbose = false]] After_is_STOP_iff D_T 
                            not_ready_After ready_hyps(2))+
    from *(5) have ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
      hence ‹front_tickFree v ∧ (tickFree (tl r) ∨ v = []) ∧ s = tl r @ v ∧
             tl r setinterleaves ((tl t, u), insert ✓ (ev ` S)) ∧
             tl t ∈ 𝒟 (P after e) ∧ u ∈ 𝒯 Q›
        by (simp add: D_After ready_hyps,
            metis "*"(1, 2, 3) "**" "***" list.sel(3) tickFree_tl tl_append2)
      thus ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)› by (simp add: D_Sync) blast
    next
      assume ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
      hence ‹front_tickFree v ∧ (tickFree (tl r) ∨ v = []) ∧ s = tl r @ v ∧
             tl r setinterleaves ((t, tl u), insert ✓ (ev ` S)) ∧
             t ∈ 𝒟 Q ∧ tl u ∈ 𝒯 (P after e)›
        by (simp add: D_After T_After ready_hyps,
            metis "*"(1, 2, 3) "**" "***" list.sel(3) tickFree_tl tl_append2)
      thus ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
        by (simp add: D_Sync) blast
    qed
  } note * = this

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e) ⟹ s ∈ 𝒟 (P after e ⟦S⟧ Q)› for s
    apply (simp add: D_After ready_set_Sync ready_hyps notin image_iff 
              split: if_split_asm)
     apply (erule disjE;
            simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT D_UU,
            metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "*" list.collapse)
next 

  fix s
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
    from assms(3) obtain t u r v
        where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v› 
                  ‹r setinterleaves ((t, u), insert ✓ (ev ` S))› 
                  ‹t ∈ 𝒟 (P after e) ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 (P after e)›
      by (simp add: D_Sync) blast
    from "*"(5) have ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P after e) ∧ u ∈ 𝒯 Q›
      with "*"(1, 2, 3, 4) ready_hyps(1)
      have ** : ‹front_tickFree v ∧ (tickFree (ev e # r) ∨ v = []) ∧ s = r @ v ∧
                 (ev e # r) setinterleaves ((ev e # t, u), insert ✓ (ev ` S)) ∧
                 ev e # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
        by (cases u; simp add: D_After notin image_iff, metis list.collapse)
      show ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync) (metis "**" Cons_eq_appendI)
    next
      assume ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 (P after e)›
      with "*"(1, 2, 3, 4) ready_hyps(1)
      have ** : ‹front_tickFree v ∧ (tickFree (ev e # r) ∨ v = []) ∧ s = r @ v ∧
                 (ev e # r) setinterleaves ((t, ev e # u), insert ✓ (ev ` S)) ∧
                 t ∈ 𝒟 Q ∧ ev e # u ∈ 𝒯 P›
        by (cases t; simp add: T_After notin image_iff, metis list.collapse)
      show ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync) (metis "**" Cons_eq_appendI)
    qed
  }
  thus ‹s ∈ 𝒟 (P after e ⟦S⟧ Q) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after e)›
    by (simp add: D_After ready_set_Sync ready_hyps After_BOT D_UU
                     Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT notin image_iff)
       (metis D_imp_front_tickFree butlast.simps(2) event.distinct(1) front_tickFree_butlast 
              list.discI list.sel(1, 3) tickFree_Cons tickFree_butlast)
qed



lemma not_readyL_in_After_Sync:
  ‹ev e ∉ ready_set P ⟹ e ∈ S ⟹ 
   (P ⟦S⟧ Q) after e = (if Q = ⊥ then ⊥ else STOP)› 
  apply (simp, intro conjI impI)
  by (simp add: BOT_iff_D D_After Sync_BOT ready_set_BOT D_UU,
      metis front_tickFree_single list.sel(1) list.sel(3) not_Cons_self)
     (auto simp add: STOP_iff_T T_After ready_set_BOT ready_set_Sync)


text ‹@{const [source] After} version of @{thm Mprefix_Sync_distr_subset
      [of ‹{e}› _ ‹{e}› ‹λa. P› ‹λa. Q›, simplified, folded write0_def]}.›

lemma readyL_readyR_in_After_Sync:
  ‹(P ⟦S⟧ Q) after e = P after e ⟦S⟧ Q after e› 
  if ready_hyps: ‹ev e ∈ ready_set P› ‹ev e ∈ ready_set Q› and inside: ‹e ∈ S›
proof (subst Process_eq_spec_optimized, safe)

  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)› 
       and same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q after e)›
    from assms(3) consider
      ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                         (ev e # s) setinterleaves ((s_P, s_Q), insert ✓ (ev ` S)) ∧ 
                         X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› |
      ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: F_Sync D_Sync) blast
    hence ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q after e)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q
        where * : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
                  ‹(ev e # s) setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› by blast
      from *(3) have ‹s_P ≠ [] ∧ hd s_P = ev e ∧ s_Q ≠ [] ∧ hd s_Q = ev e ∧
                      s setinterleaves ((tl s_P, tl s_Q), insert ✓ (ev ` S))›
        using inside by (cases s_P; cases s_Q, auto simp add: split: if_split_asm)
      hence ‹(tl s_P, X_P) ∈ ℱ (P after e) ∧ (tl s_Q, X_Q) ∈ ℱ (Q after e) ∧
            s setinterleaves ((tl s_P, tl s_Q), insert ✓ (ev ` S)) ∧
            X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
        using "*"(1, 2, 4) ready_hyps by (simp add: F_After) blast
      thus ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q after e)›
        by (simp add: F_Sync) blast
    next
      assume ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e)› 
        by (force simp add: D_After ready_set_Sync ready_hyps assms(1, 2))
      from this[simplified same_div]
      show ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q after e)› using NF_ND by blast
    qed
  } note * = this

  show ‹(s, X) ∈ ℱ ((P ⟦S⟧ Q) after e) ⟹ (s, X) ∈ ℱ (P after e ⟦S⟧ Q after e)›
    if same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q after e)› for s X
    apply (simp add: F_After ready_set_Sync ready_hyps split: if_split_asm)
      apply (erule disjE; 
             simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT F_UU,
             metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "*" list.exhaust_sel same_div)
next

  fix s X
  assume same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 (P after e ⟦S⟧ Q after e)›
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q after e)›
    from assms(3) consider 
      ‹∃s_P s_Q X_P X_Q. (ev e # s_P, X_P) ∈ ℱ P ∧ (ev e # s_Q, X_Q) ∈ ℱ Q ∧
                         s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S)) ∧ 
                         X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 (P after e ⟦S⟧ Q after e)›
      by (auto simp add: F_Sync D_Sync F_After ready_hyps) (metis list.collapse)
    hence ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q 
        where * : ‹(ev e # s_P, X_P) ∈ ℱ P› ‹(ev e # s_Q, X_Q) ∈ ℱ Q› 
                  ‹s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› by blast
      have ** : ‹(ev e # s) setinterleaves ((ev e # s_P, ev e # s_Q), insert ✓ (ev ` S))›
        by (simp add: inside "*"(3))
      show ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        apply (simp add: F_Sync)
        using "*"(1, 2, 4) "**" by blast
    next
      assume ‹s ∈ 𝒟 (P after e ⟦S⟧ Q after e)›
      with same_div[symmetric] have ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_After ready_hyps ready_set_Sync assms(1, 2)) (metis list.collapse)
      with D_F show ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)› by blast
    qed
  }
  thus ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q after e) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after e)›
    by (simp add: F_After ready_set_Sync ready_hyps After_BOT F_UU
                  Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT)
       (metis butlast.simps(2) event.distinct(1) front_tickFree_butlast is_processT2 
              list.distinct(1) list.sel(1, 3) tickFree_Cons tickFree_butlast)
next

  { fix s
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)› 
    from assms(3) obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹ev e # s = r @ v›
                ‹r setinterleaves ((t, u), insert ✓ (ev ` S))› 
                ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by (simp add: D_Sync) blast
    have ** : ‹r ≠ [] ∧ hd r = ev e ∧ t ≠ [] ∧ hd t = ev e ∧ u ≠ [] ∧ hd u = ev e ∧
               tl r setinterleaves ((tl t, tl u), insert ✓ (ev ` S))›
      using *(3, 4, 5) inside assms(1, 2)[simplified BOT_iff_D] 
      by (cases t; cases u; force split: if_split_asm)
    have ‹(tickFree (tl r) ∨ v = []) ∧ s = tl r @ v ∧
          (tl t ∈ 𝒟 (P after e) ∧ tl u ∈ 𝒯 (Q after e) ∨ 
           tl t ∈ 𝒟 (Q after e) ∧ tl u ∈ 𝒯 (P after e))›
      using "*"(2, 3, 5) "**" apply (simp add: D_After ready_hyps T_After)
      by (metis tickFree_tl list.sel(3) tl_append2)
    with "*"(1) "**" have ‹s ∈ 𝒟 (P after e ⟦S⟧ Q after e)› by (simp add: D_Sync) blast
  } note * = this

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e) ⟹ s ∈ 𝒟 (P after e ⟦S⟧ Q after e)› for s
    apply (simp add: D_After ready_set_Sync ready_hyps After_BOT D_UU
              split: if_split_asm)
     apply (erule disjE; 
            simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT D_UU,
            metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "*" list.exhaust_sel)
next
  
  fix s
  { assume ‹s ∈ 𝒟 (P after e ⟦S⟧ Q after e)›
    from this obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v›
                ‹r setinterleaves ((t, u), insert ✓ (ev ` S))› 
                ‹ev e # t ∈ 𝒟 P ∧ ev e # u ∈ 𝒯 Q ∨ ev e # t ∈ 𝒟 Q ∧ ev e # u ∈ 𝒯 P› 
      by (simp add: D_Sync D_After T_After ready_hyps) (metis list.collapse)
    have ** : ‹(ev e # r) setinterleaves ((ev e # t, ev e # u), insert ✓ (ev ` S))›
      by (simp add: inside "*"(4))
    have ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Sync inside)
         (metis "*"(1, 2, 3, 5) "**" append_Cons event.distinct(1) tickFree_Cons)
  }
  thus ‹s ∈ 𝒟 (P after e ⟦S⟧ Q after e) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after e)›
    by (simp add: D_After ready_set_Sync ready_hyps After_BOT D_UU
                  Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT inside)
       (metis D_imp_front_tickFree list.distinct(1) list.sel(1, 3))
qed


text ‹@{const [source] After} version of
     
      @{thm Mprefix_Sync_distr_indep
      [of ‹{e}› _ ‹{e}› ‹λa. P› ‹λa. Q›, simplified, folded write0_def]}.›

lemma readyL_readyR_not_in_After_Sync: 
  ‹(P ⟦S⟧ Q) after e = (P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e)›
  if ready_hyps: ‹ev e ∈ ready_set P› ‹ev e ∈ ready_set Q› and notin: ‹e ∉ S›
proof (subst Process_eq_spec_optimized, safe)

  { fix P Q s X s_P s_Q X_P X_Q
    assume assms : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q› 
                   ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q›
                   ‹s_P ≠ []› ‹hd s_P = ev e›
                   ‹s setinterleaves ((tl s_P, s_Q), insert ✓ (ev ` S))›
                   ‹ev e ∈ ready_set P›
    from assms(1, 4, 5, 7) have ‹(tl s_P, X_P) ∈ ℱ (P after e)›
      by (simp add: F_After) blast
    with assms(2, 3, 6) have ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)›
      by (simp add: F_Sync) blast
  } note * = this
  
  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
       and same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
    from assms(3) consider
       ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                          (ev e # s) setinterleaves ((s_P, s_Q), insert ✓ (ev ` S)) ∧ 
                          X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› |
        ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e)›
      by (simp add: F_Sync D_After D_Sync ready_set_Sync assms(1, 2) ready_hyps)
         (metis (no_types, opaque_lifting) list.distinct(1) list.sel(1, 3))
    hence ‹(s, X) ∈ ℱ ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q
        where ** : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q› 
                   ‹(ev e # s) setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                   ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› by blast
      have ‹s_P ≠ [] ∧ hd s_P = ev e ∧ s setinterleaves ((tl s_P, s_Q), insert ✓ (ev ` S)) ∨
            s_Q ≠ [] ∧ hd s_Q = ev e ∧ s setinterleaves ((s_P, tl s_Q), insert ✓ (ev ` S))›
        using **(3) by (cases s_P; cases s_Q; simp add: notin image_iff split: if_split_asm) blast
      thus ‹(s, X) ∈ ℱ ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
        apply (elim disjE; simp add: F_Ndet)
        subgoal using "*" "**"(1, 2, 4) ready_hyps(1) by blast
        apply (rule disjI2, subst Sync_commute, rule *[OF **(2, 1)])
        by (simp_all add: "**"(4) Int_commute Un_commute Sync_commute Sync.sym ready_hyps(2))
    next
      assume ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e)›
      from this[simplified same_div]
      show ‹(s, X) ∈ ℱ ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))› using NF_ND by blast
    qed
  } note ** = this
    
  show ‹(s, X) ∈ ℱ ((P ⟦S⟧ Q) after e) ⟹ (s, X) ∈ ℱ ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))› 
    if same_div: ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))› for s X
    apply (simp add: F_After ready_set_Sync ready_hyps split: if_split_asm)
     apply (erule disjE;
            simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT F_UU Ndet_id,
            metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "**" same_div list.exhaust_sel)
next

  { fix s X P Q
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after e ⟦S⟧ Q)› ‹ev e ∈ ready_set P›
       and same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
    from assms(3)[simplified F_Sync, simplified] consider
      ‹∃s_P s_Q X_P X_Q. (ev e # s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                         s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S)) ∧ 
                         X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
      by (simp add: F_Sync F_After assms(4) D_Sync)
         (metis (no_types, opaque_lifting) list.exhaust_sel)
    hence ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q
        where * : ‹(ev e # s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
                  ‹s setinterleaves ((s_P, s_Q), insert ✓ (ev ` S))›
                  ‹X = (X_P ∪ X_Q) ∩ insert ✓ (ev ` S) ∪ X_P ∩ X_Q› by blast
      have ‹(ev e # s) setinterleaves ((ev e # s_P, s_Q), insert ✓ (ev ` S))›
        using "*"(3) by (cases s_Q; simp add: notin image_iff)
      with "*"(1, 2, 4) show ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    next
      assume ‹s ∈ 𝒟 (P after e ⟦S⟧ Q)›
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e)› using same_div[simplified D_Ndet] by fast
      hence ‹(s, X) ∈ ℱ ((P ⟦S⟧ Q) after e)› using process_charn by blast
      thus ‹(ev e # s, X) ∈ ℱ (P ⟦S⟧ Q)› 
        by (simp add: F_After ready_set_Sync assms(1, 2, 4) notin image_iff)
           (metis list.collapse)
    qed
  } note * = this

  show ‹(s, X) ∈ ℱ ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e)) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after e)› 
    if same_div : ‹𝒟 ((P ⟦S⟧ Q) after e) = 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))› for s X
    apply (simp add: F_After ready_set_Sync ready_hyps After_BOT F_UU
                     Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT Ndet_id)
    apply (intro conjI impI)
      apply ((metis butlast.simps(2) event.simps(3) front_tickFree_butlast tickFree_Cons
                    front_tickFree_single is_processT2 list.distinct(1) list.sel(1, 3))+)[2]
    by (simp add: F_Ndet)
       (metis "*" Ndet_commute Sync_commute list.distinct(1) list.sel(1, 3) ready_hyps same_div)
next

  { fix s
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
    from assms(3) obtain t u r v
      where ** : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹ev e # s = r @ v›
                 ‹r setinterleaves ((t, u), insert ✓ (ev ` S))›
                 ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by (simp add: D_Sync) blast
    have *** : ‹r ≠ []› using "**"(4, 5) BOT_iff_D assms(1, 2) empty_setinterleaving by blast
    have ‹t ≠ [] ∧ hd t = ev e ∧ tl r setinterleaves ((tl t, u), insert ✓ (ev ` S)) ∨
          u ≠ [] ∧ hd u = ev e ∧ tl r setinterleaves ((t, tl u), insert ✓ (ev ` S))›
      using **(3, 4) by (cases t; cases u, auto simp add: *** notin split: if_split_asm)
    with "**"(5) have ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
    proof (elim disjE)
      assume * : ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
                 ‹t ≠ [] ∧ hd t = ev e ∧ tl r setinterleaves ((tl t, u), insert ✓ (ev ` S))›
      hence ‹s = tl r @ v ∧ tl t ∈ 𝒟 (P after e) ∧ u ∈ 𝒯 Q›
        using "**"(3) "***" ready_hyps(1) apply (simp add: D_After, intro conjI)
          by (metis list.sel(3) tl_append2) blast
      thus ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
        using "*"(2) "**"(1, 2) tickFree_tl by (simp add: D_Ndet D_Sync) blast
    next
      assume * : ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
                 ‹u ≠ [] ∧ hd u = ev e ∧ tl r setinterleaves ((t, tl u), insert ✓ (ev ` S))›
      hence ‹s = tl r @ v ∧ t ∈ 𝒟 P ∧ tl u ∈ 𝒯 (Q after e)›
        using "**"(3) ready_hyps(2) "***" apply (simp add: T_After, intro conjI)
        by (metis list.sel(3) tl_append2) blast
      thus ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
        using "*"(2) "**"(1, 2) tickFree_tl by (simp add: D_Ndet D_Sync) blast
    next
      assume * : ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
                 ‹t ≠ [] ∧ hd t = ev e ∧ tl r setinterleaves ((tl t, u), insert ✓ (ev ` S))›
      hence ‹s = tl r @ v ∧ tl t ∈ 𝒟 (Q after e) ∧ u ∈ 𝒯 P›
        using "**"(1, 2, 3) ready_hyps apply (simp add: D_After, intro conjI)
        by (metis "***" list.sel(3) tl_append2) blast
      thus ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
        using "*"(2) "**"(1, 2) tickFree_tl by (simp add: D_Ndet D_Sync) blast
    next
      assume * : ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
                 ‹u ≠ [] ∧ hd u = ev e ∧ tl r setinterleaves ((t, tl u), insert ✓ (ev ` S))›
      hence ‹s = tl r @ v ∧ t ∈ 𝒟 Q ∧ tl u ∈ 𝒯 (P after e)›
        using "**"(1, 2, 3) ready_hyps apply (simp add: T_After, intro conjI)
        by (metis "***" list.sel(3) tl_append2) blast
      thus ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))›
        using "*"(2) "**"(1, 2) tickFree_tl by (simp add: D_Ndet D_Sync) blast
    qed
  } note * = this

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after e) ⟹ s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e))› for s
     apply (simp add: D_After ready_set_Sync ready_hyps After_BOT D_UU
              split: if_split_asm)
     apply (erule disjE;
            simp add: After_BOT Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT Ndet_id D_UU,
            metis butlast_tl front_tickFree_butlast tickFree_tl)
    by (metis "*" list.collapse)
next

  { fix s P Q
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q))› ‹ev e ∈ ready_set P›
    from assms(3)[simplified D_Sync, simplified] obtain t u r v
      where * : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s = r @ v› 
                ‹r setinterleaves ((t, u), insert ✓ (ev ` S))›
                ‹ev e # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ ev e # u ∈ 𝒯 P›
      by (simp add: D_Sync D_After T_After assms(4)) (metis list.collapse)
    from "*"(5) have ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
    proof (elim disjE)
      assume ** : ‹ev e # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
      have *** : ‹(ev e # r) setinterleaves ((ev e # t, u), insert ✓ (ev ` S))›
        using "*"(4) by (cases u; simp add: notin image_iff "*"(1, 2, 3))
      show ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync)
           (metis "*"(1, 2, 3) "**" "***" Cons_eq_appendI event.distinct(1) tickFree_Cons)
    next
      assume ** : ‹t ∈ 𝒟 Q ∧ ev e # u ∈ 𝒯 P›
      have *** : ‹(ev e # r) setinterleaves ((t, ev e # u), insert ✓ (ev ` S))›
        using "*"(4) by (cases t; simp add: notin image_iff "*"(1, 2, 3))
      show ‹ev e # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync)
           (metis "*"(1, 2, 3) "**" "***" Cons_eq_appendI event.distinct(1) tickFree_Cons)
    qed
  } note * = this 

  show ‹s ∈ 𝒟 ((P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e)) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after e)› for s
    apply (simp add: D_After ready_set_Sync ready_hyps After_BOT D_UU
                     Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT notin Ndet_id)
    apply (intro conjI impI)
      apply ((metis D_imp_front_tickFree butlast.simps(2) event.distinct(1) tickFree_Cons
                    front_tickFree_single list.discI list.sel(1, 3) front_tickFree_butlast)+)[2]
    by (simp add: D_Ndet)
       (metis "*" list.distinct(1) list.sel(1, 3) mono_D_Sync ready_hyps)
qed


lemma not_readyL_not_readyR_After_Sync: ‹(P ⟦S⟧ Q) after e = STOP› 
  if ready_hyps: ‹ev e ∉ ready_set P› ‹ev e ∉ ready_set Q›
  apply (subst not_ready_After, simp add: ready_set_Sync)
  using ready_set_BOT ready_hyps by auto


text ‹Finally, the monster theorem !›

theorem After_Sync: 
  ‹(P ⟦S⟧ Q) after e =
   (        if P = ⊥ ∨ Q = ⊥ then ⊥ 
     else   if ev e ∈ ready_set P ∧ ev e ∈ ready_set Q
          then   if e ∈ S then P after e ⟦S⟧ Q after e 
               else (P after e ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after e)
     else   if e ∈ S then STOP
     else   if ev e ∈ ready_set P then P after e ⟦S⟧ Q
     else   if ev e ∈ ready_set Q then P ⟦S⟧ Q after e
     else STOP)›
  by (simp add: Sync_commute[of ⊥, simplified Sync_BOT] Sync_BOT After_BOT
                readyL_readyR_in_After_Sync readyL_readyR_not_in_After_Sync
                not_readyL_in_After_Sync readyL_not_readyR_not_in_After_Sync 
                not_readyL_not_readyR_After_Sync)
     (metis Sync_commute not_readyL_in_After_Sync readyL_not_readyR_not_in_After_Sync)



subsection ‹@{const [source] After} Hiding Operator›

text ‹\<^term>‹P \ A› is harder to deal with, we will only obtain refinements results.›

lemma Hiding_FD_Hiding_After_if_ready_inside:
      ‹e ∈ B ⟹ (P \ B) ⊑⇩F⇩D (P after e \ B)›
  and After_Hiding_FD_Hiding_After_if_ready_notin:
      ‹e ∉ B ⟹ (P \ B) after e ⊑⇩F⇩D (P after e \ B)›
  if ready: ‹ev e ∈ ready_set P›
  supply ready' = ready_notin_imp_ready_Hiding[OF ready]
proof -
  { fix s
    assume ‹s ∈ 𝒟 (P after e \ B)›
    with D_Hiding obtain t u 
      where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` B) @ u› 
                ‹t ∈ 𝒟 (P after e) ∨ (∃ f. isInfHiddenRun f (P after e) B ∧ t ∈ range f)› 
      by blast
    from "*"(4) have ‹s ∈ (if e ∈ B then 𝒟 (P \ B) else 𝒟 ((P \ B) after e))›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P after e)›
      hence ** : ‹ev e # t ∈ 𝒟 P› by (simp add: D_After ready) (metis list.exhaust_sel)
      show  ‹s ∈ (if e ∈ B then 𝒟 (P \ B) else 𝒟 ((P \ B) after e))›
      proof (split if_split, intro conjI impI)
        assume ‹e ∈ B›
        with "*"(3) have *** : ‹s = trace_hide (ev e # t) (ev ` B) @ u› by simp
        show ‹s ∈ 𝒟 (P \ B)›
          by (simp add: D_Hiding)
             (metis "*"(1, 2) "**" "***" event.distinct(1) tickFree_Cons)
      next
        assume ‹e ∉ B›
        with "*"(3) have *** : ‹ev e # s = trace_hide (ev e # t) (ev ` B) @ u›
          by (simp add: image_iff)
        have ‹ev e # s ∈ 𝒟 (P \ B)›
          by (simp add: D_Hiding)
             (metis "*"(1, 2) "**" "***" event.distinct(1) tickFree_Cons)
        thus ‹s ∈ 𝒟 ((P \ B) after e)›
          by (simp add: D_After ready' ‹e ∉ B›)
             (metis list.distinct(1) list.sel(1, 3))
      qed
    next
      assume ‹∃f. isInfHiddenRun f (P after e) B ∧ t ∈ range f›
      then obtain f where ‹isInfHiddenRun f (P after e) B› ‹t ∈ range f› by blast
      hence ** : ‹isInfHiddenRun (λi. ev e # f i) P B ∧
                  ev e # t ∈ range (λi. ev e # f i)›
        by (simp add: less_cons monotone_on_def T_After ready)
           (metis list.exhaust_sel rangeE rangeI)       
      show ‹s ∈ (if e ∈ B then 𝒟 (P \ B) else 𝒟 ((P \ B) after e))›
      proof (split if_split, intro conjI impI)
        assume ‹e ∈ B›
        with "*"(3) have *** : ‹s = trace_hide (ev e # t) (ev ` B) @ u› by simp
        show ‹s ∈ 𝒟 (P \ B)›
          by (simp add: D_Hiding)
             (metis "*"(1, 2) "**" "***" event.distinct(1) tickFree_Cons)
      next
        assume ‹e ∉ B›
        with "*"(3) have *** : ‹ev e # s = trace_hide (ev e # t) (ev ` B) @ u›
          by (simp add: image_iff)
        have ‹ev e # s ∈ 𝒟 (P \ B)›
          by (simp add: D_Hiding)
             (metis "*"(1, 2) "**" "***" event.distinct(1) tickFree_Cons)
        thus ‹s ∈ 𝒟 ((P \ B) after e)›
          by (simp add: D_After ready' ‹e ∉ B›)
             (metis list.distinct(1) list.sel(1, 3))
      qed
    qed
  } note div_ref = this

  { fix s X
    assume ‹(s, X) ∈ ℱ (P after e \ B)›
    with F_Hiding D_Hiding consider 
        ‹∃t. s = trace_hide t (ev ` B) ∧ (t, X ∪ ev ` B) ∈ ℱ (P after e)› 
      | ‹s ∈ 𝒟 (P after e \ B)› by blast
    hence ‹(s, X) ∈ (if e ∈ B then ℱ (P \ B) else ℱ ((P \ B) after e))›
    proof cases
      assume ‹∃t. s = trace_hide t (ev ` B) ∧ (t, X ∪ ev ` B) ∈ ℱ (P after e)›
      then obtain t where * : ‹s = trace_hide t (ev ` B)› ‹(ev e # t, X ∪ ev ` B) ∈ ℱ P›
        by (simp add: F_After ready) (metis list.exhaust_sel)
      show ‹(s, X) ∈ (if e ∈ B then ℱ (P \ B) else ℱ ((P \ B) after e))›
      proof (split if_split, intro conjI impI)
        from "*" show ‹e ∈ B ⟹ (s, X) ∈ ℱ (P \ B)›
          by (simp add: F_Hiding) (metis filter.simps(2) image_eqI)
      next
        assume ‹e ∉ B›
        with "*"(1) have ** : ‹ev e # s = trace_hide (ev e # t) (ev ` B)›
          by (simp add: image_iff)
        show ‹(s, X) ∈ ℱ ((P \ B) after e)›
          by (simp add: F_After ready' ‹e ∉ B› F_Hiding)
             (metis "*"(2) "**" list.discI list.sel(1, 3)) 
      qed
    next
      show ‹s ∈ 𝒟 (P after e \ B) ⟹ (s, X) ∈ (if e ∈ B then ℱ (P \ B) else ℱ ((P \ B) after e))›
        by (drule div_ref, simp split: if_split_asm; use NF_ND in blast)
    qed 
  } note fail_ref = this

  show ‹e ∈ B ⟹ (P \ B) ⊑⇩F⇩D (P after e \ B)›
   and ‹e ∉ B ⟹ (P \ B) after e ⊑⇩F⇩D (P after e \ B)›
    unfolding failure_divergence_refine_def le_ref_def using div_ref fail_ref by auto
qed


lemmas Hiding_F_Hiding_After_if_ready_inside = 
       Hiding_FD_Hiding_After_if_ready_inside[THEN leFD_imp_leF]
   and After_Hiding_F_Hiding_After_if_ready_notin = 
       After_Hiding_FD_Hiding_After_if_ready_notin[THEN leFD_imp_leF]
   and Hiding_D_Hiding_After_if_ready_inside = 
       Hiding_FD_Hiding_After_if_ready_inside[THEN leFD_imp_leD]
   and After_Hiding_D_Hiding_After_if_ready_notin = 
       After_Hiding_FD_Hiding_After_if_ready_notin[THEN leFD_imp_leD]
   and Hiding_T_Hiding_After_if_ready_inside = 
       Hiding_FD_Hiding_After_if_ready_inside[THEN leFD_imp_leF, THEN leF_imp_leT]   
   and After_Hiding_T_Hiding_After_if_ready_notin = 
       After_Hiding_FD_Hiding_After_if_ready_notin[THEN leFD_imp_leF, THEN leF_imp_leT]

corollary Hiding_DT_Hiding_After_if_ready_inside:
  ‹ev e ∈ ready_set P ⟹ e ∈ B ⟹ (P \ B) ⊑⇩D⇩T (P after e \ B)›
  and After_Hiding_DT_Hiding_After_if_ready_notin: 
  ‹ev e ∈ ready_set P ⟹ e ∉ B ⟹ (P \ B) after e ⊑⇩D⇩T (P after e \ B)›
  by (simp add: Hiding_D_Hiding_After_if_ready_inside 
                Hiding_T_Hiding_After_if_ready_inside leD_leT_imp_leDT)
     (simp add: After_Hiding_D_Hiding_After_if_ready_notin 
                After_Hiding_T_Hiding_After_if_ready_notin leD_leT_imp_leDT)


text ‹This is the best we can obtain: even by restricting ourselves to two events, 
      we can already construct a counterexample.›

lemma defines P_def: ‹P ≡ (Suc 0 → (0 → STOP)) ⊓ (0 → SKIP)› 
          and B_def: ‹B ≡ {Suc 0}› and e_def : ‹e ≡ 0› and f_def: ‹f ≡ Suc 0›
        shows ‹ev e ∈ ready_set P ∧ f ∈ B ∧ P \ B ≠ P after f \ B›
          and ‹ev e ∈ ready_set P ∧ e ∉ B ∧ (P \ B) after e ≠ P after e \ B› 
  unfolding e_def f_def P_def B_def
  apply (simp_all add: ready_set_Ndet ready_set_prefix)
  apply (simp_all add: After_Ndet ready_set_prefix After_prefix Hiding_set_SKIP)
  apply (simp_all add: Hiding_Ndet After_Ndet ready_set_prefix After_prefix Hiding_set_SKIP 
                       Hiding_set_STOP no_Hiding_write0 Hiding_write0)
  by (metis After_prefix Ndet_is_STOP_iff SKIP_Neq_STOP write0_Ndet)
     (metis mono_Ndet_FD_right Ndet_commute SKIP_FD_iff SKIP_Neq_STOP STOP_FD_iff)
  


subsection ‹@{const [source] After} Renaming›

lemma After_Renaming:
  ‹Renaming P f after e = 
   (if P = ⊥ then ⊥ else
    ⊓a ∈ {a. ev a ∈ ready_set P ∧ f a = e}. Renaming (P after a) f)›
   (is ‹?lhs = (if P = ⊥ then ⊥ else ?rhs)›)
  ―‹We treat the case \<^term>‹P = ⊥› separately because the set \<^term>‹{a. f a = e}› may
     be empty, which implies \<^term>‹?rhs = STOP› while \<^term>‹?lhs = ⊥›.›

proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ ?lhs= ⊥›
    by (simp add: Renaming_BOT After_BOT GlobalNdet_id)
next
  assume non_BOT: ‹P ≠ ⊥›
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    hence * : ‹ev e ∈ ready_set (Renaming P f)› ‹ev e # s ∈ 𝒟 (Renaming P f)›
      by (auto simp add: D_After split: if_split_asm) (metis list.exhaust_sel)
    from "*"(2) obtain t1 t2
      where ** : ‹tickFree t1› ‹front_tickFree t2›
                 ‹ev e # s = map (EvExt f) t1 @ t2› ‹t1 ∈ 𝒟 P›
      by (simp add: D_Renaming) blast
    from "**"(1, 3, 4) non_BOT obtain a t1'
      where *** : ‹t1 = ev a # t1'› ‹f a = e›
      by (cases t1; simp add: BOT_iff_D EvExt_def)
         (metis comp_apply event.exhaust event.inject event.simps(4))
    have ‹ev a ∈ ready_set P›
      using "**"(4) "***"(1) Cons_in_T_imp_elem_ready_set D_T by blast
    also have ‹s ∈ 𝒟 (Renaming (P after a) f)›
      using "**" "***"(1) by (simp add: D_Renaming D_After calculation)
                             (metis list.discI list.sel(1, 3))
    ultimately show ‹s ∈ 𝒟 ?rhs›
      using "***"(2) by (simp add: D_GlobalNdet) blast
  next
    show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
      apply (simp add: D_GlobalNdet D_Renaming D_After 
                       ready_set_Renaming non_BOT EvExt_def image_iff
                split: if_split_asm event.split, intro conjI)
      by (metis (no_types, lifting) Nil_is_append_conv event.distinct(1) 
          hd_append2 hd_map_EvExt list.collapse list.map_disc_iff 
          map_tl tickFree_Cons tl_append2) blast
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?lhs›
    then consider ‹ev e ∉ ready_set (Renaming P f)› ‹s = []›
      | ‹ev e ∈ ready_set (Renaming P f)› ‹(ev e # s, X) ∈ ℱ (Renaming P f)›
      by (simp add: F_After split: if_split_asm) (metis list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ ?rhs›
    proof cases
      show ‹ev e ∉ ready_set (Renaming P f) ⟹ s = [] ⟹ (s, X) ∈ ℱ ?rhs›
        by (simp add: ready_set_Renaming non_BOT F_GlobalNdet F_Renaming F_After)
           (metis ev_elem_anteced1 imageI vimage_eq)
    next
      assume assms : ‹ev e ∈ ready_set (Renaming P f)›
                     ‹(ev e # s, X) ∈ ℱ (Renaming P f)›
      from assms(2) consider ‹ev e # s ∈ 𝒟 (Renaming P f)›
        | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ P ∧ ev e # s = map (EvExt f) s1›
        by (simp add: F_Renaming D_Renaming) blast
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        assume ‹ev e # s ∈ 𝒟 (Renaming P f)›
        hence ‹s ∈ 𝒟 ?lhs› by (force simp add: D_After assms(1))
        with D_F same_div show ‹(s, X) ∈ ℱ ?rhs› by blast
      next
        assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ P ∧ ev e # s = map (EvExt f) s1›
        then obtain s1 where * : ‹(s1, EvExt f -` X) ∈ ℱ P›
                                 ‹ev e # s = map (EvExt f) s1› by meson
        from "*"(2) obtain a s1'
          where ** : ‹s1 = ev a # s1'› ‹f a = e›
          by (cases s1; simp; metis "*"(2) EvExt_ev1 event.inject 
                                    hd_map_EvExt list.distinct(1) list.sel(1))
        have ‹ev a ∈ ready_set P›
          using "*"(1) "**"(1) Cons_in_T_imp_elem_ready_set F_T by blast
        also have ‹(s, X) ∈ ℱ (Renaming (P after a) f)›
          using "*"(1, 2) "**"(1) by (simp add: F_Renaming F_After calculation)
                                     (metis list.distinct(1) list.sel(1, 3))
        ultimately show ‹(s, X) ∈ ℱ ?rhs›
          using "**"(2) by (simp add: F_GlobalNdet) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    assume ‹(s, X) ∈ ℱ ?rhs›    
    then consider ‹∀a. ev a ∈ ready_set P ⟶ f a ≠ e› ‹s = []›
      | ‹∃a. f a = e ∧ ev a ∈ ready_set P ∧ (s, X) ∈ ℱ (Renaming (P after a) f)›
      by (auto simp add: F_GlobalNdet split: if_split_asm)
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      show ‹∀a. ev a ∈ ready_set P ⟶ f a ≠ e ⟹ s = [] ⟹ (s, X) ∈ ℱ ?lhs›
        by (auto simp add: F_After F_Renaming ready_set_Renaming non_BOT)
           (metis (no_types, opaque_lifting) EvExt_ev1 event.inject 
                  hd_map_EvExt list.distinct(1) list.sel(1) list.simps(9))
    next
      assume ‹∃a. f a = e ∧ ev a ∈ ready_set P ∧ 
                  (s, X) ∈ ℱ (Renaming (P after a) f)›
      then obtain a 
        where * : ‹f a = e› ‹ev a ∈ ready_set P› 
                  ‹(s, X) ∈ ℱ (Renaming (P after a) f)› by blast
      from "*"(3) consider ‹s ∈ 𝒟 (Renaming (P after a) f)›
        | ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P after a) ∧ s = map (EvExt f) s1›
        by (simp add: F_Renaming D_Renaming) blast
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹s ∈ 𝒟 (Renaming (P after a) f)›
        with "*"(1, 2) have ‹s ∈ 𝒟 ?rhs› by (simp add: D_GlobalNdet) blast
        with D_F same_div show ‹(s, X) ∈ ℱ ?lhs› by blast
      next
        assume ‹∃s1. (s1, EvExt f -` X) ∈ ℱ (P after a) ∧ s = map (EvExt f) s1›
        then obtain s1 where ** : ‹(s1, EvExt f -` X) ∈ ℱ (P after a)›
                                  ‹s = map (EvExt f) s1› by blast
        with "*"(1) have *** : ‹ev e ∉ ready_set (Renaming P f) ⟹ s = []›
          by (simp add: ready_set_Renaming non_BOT image_iff F_After 
                 split: if_split_asm) (metis hd_map hd_map_EvExt)
        { assume ‹ev e ∈ ready_set (Renaming P f)›
          hence ‹(ev a # s1, EvExt f -` X) ∈ ℱ P ∧ ev e # s = map (EvExt f) (ev a # s1)›
            using "*"(1, 2) "**" by (simp add: F_After "*"(2))
                                    (metis hd_map hd_map_EvExt list.collapse)
          hence ‹(ev e # s, X) ∈ ℱ (Renaming P f)›
            by (auto simp add: F_Renaming)
        }
        thus ‹(s, X) ∈ ℱ ?lhs›
          by (simp add: F_After "***") (metis list.discI list.sel(1, 3))
      qed
    qed
  qed
qed



section ‹Behaviour of @{const [source] After} with Operators of \<^session>‹HOL-CSPM››

lemma After_MultiDet_is_After_MultiNdet: 
  ‹finite A ⟹ (❙□ a ∈ A. P a) after e = (⨅ a ∈ A. P a) after e›
  apply (cases ‹A = {}›, simp)
  apply (rotate_tac, induct rule: finite_set_induct_nonempty, simp)
  by (simp add: After_Det_is_After_Ndet After_Ndet 
                ready_set_MultiDet ready_set_MultiNdet)


lemma After_GlobalNdet: ‹(⊓ a ∈ A. P a) after e = 
                         (  if ev e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
                          else (⊓ a ∈ {a ∈ A. ev e ∈ ready_set (P a)}. P a) after e)›
  apply (subst Process_eq_spec, auto simp add: not_ready_After ready_set_GlobalNdet)
     apply (auto simp add: F_After F_GlobalNdet D_After D_GlobalNdet ready_set_GlobalNdet
                    split: if_split_asm, 
            auto simp add: ready_set_def)
  by (metis F_T append_Cons append_Nil is_processT3_ST list.exhaust list.sel(1))
     (metis D_T append_Cons append_Nil hd_Cons_tl is_processT3_ST)


lemma After_MultiNdet: ‹finite A ⟹ (⨅ a ∈ A. P a) after e = 
                        (  if ev e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
                         else (⨅ a ∈ {a ∈ A. ev e ∈ ready_set (P a)}. P a) after e)›
  by (subst (1 2) finite_GlobalNdet_is_MultiNdet[symmetric], simp_all add: After_GlobalNdet)


lemma After_MultiDet: ‹finite A ⟹ 
                       (❙□ a ∈ A. P a) after e = 
                       (  if ev e ∉ (⋃a ∈ A. ready_set (P a)) then STOP
                        else (⨅ a ∈ {a ∈ A. ev e ∈ ready_set (P a)}. P a) after e)›
  by (simp add: After_MultiDet_is_After_MultiNdet After_MultiNdet)


(* TODO: formulate and prove for MultiSync and MultiSeq *)



section ‹Behaviour of @{const [source] After} with Operators of \<^session>‹HOL-CSP_OpSem››

subsection ‹@{const [source] After} Sliding›

lemma After_Sliding:
  ‹P ⊳ Q after e = 
   (  if ev e ∉ ready_set P ∧ ev e ∉ ready_set Q then STOP
    else   if ev e ∈ ready_set P ∧ ev e ∈ ready_set Q then (P after e) ⊓ (Q after e)
         else if ev e ∈ ready_set P then P after e else Q after e)›
  by (simp add: Sliding_def After_Ndet After_Det ready_set_Det Ndet_id Ndet_assoc)

text ‹An interesting corollary is that \<^const>‹Sliding› is also
      concerned by the loss of determinism (see @{thm After_Det_is_After_Ndet}).›

lemma After_Sliding_is_After_Ndet: ‹P ⊳ Q after e = P ⊓ Q after e›
  by (simp add: After_Ndet After_Sliding)



subsection ‹@{const [source] After} Throwing›

lemma After_Throw: 
  ‹(P Θ a ∈ A. Q a) after e = 
   (  if P = ⊥ then ⊥
    else   if ev e ∈ ready_set P then   if e ∈ A then Q e
                                 else (P after e) Θ a ∈ A. Q a
         else STOP)›
  (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = Q e› if ‹P ≠ ⊥› and ‹ev e ∈ ready_set P› and ‹e ∈ A›
  proof (subst Process_eq_spec, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    with that(2) have ‹ev e # s ∈ 𝒟 (P Θ a ∈ A. Q a)›
      by (simp add: D_After ready_set_Throw) (metis list.exhaust_sel)
    with that(1) show ‹s ∈ 𝒟 (Q e)›
      apply (simp add: D_Throw disjoint_iff BOT_iff_D, elim disjE)
      by (metis hd_append2 hd_in_set image_eqI list.sel(1) that(3))
         (metis append_self_conv2 event.inject hd_append2
                hd_in_set image_eqI list.sel(1, 3) that(3))
  next
    have ‹[ev e] ∈ 𝒯 P ∧ e ∈ A› using ready_set_def that(2, 3) by blast
    thus ‹s ∈ 𝒟 (Q e) ⟹ s ∈ 𝒟 ((P Θ a ∈ A. Q a) after e)› for s
      by (simp add: D_After ready_set_Throw that(2) D_Throw)
         (metis append_Nil empty_set inf_bot_left list.distinct(1) list.sel(1, 3))
  next
    fix s X
    assume ‹(s, X) ∈ ℱ ?lhs›
    with that(2) have ‹(ev e # s, X) ∈ ℱ (P Θ a ∈ A. Q a)›
      by (simp add: F_After ready_set_Throw) (metis list.exhaust_sel)
    with that(1, 3) show ‹(s, X) ∈ ℱ (Q e)›
      apply (simp add: F_Throw image_iff BOT_iff_D, elim disjE)
      by (metis disjoint_iff hd_append2 hd_in_set image_eqI list.sel(1))
         (metis append_Nil event.inject hd_append2 imageI insert_disjoint(2) 
                list.exhaust_sel list.sel(1, 3) list.simps(15))
  next
    have ‹[ev e] ∈ 𝒯 P ∧ e ∈ A› using ready_set_def that(2, 3) by blast
    thus ‹(s, X) ∈ ℱ (Q e) ⟹ (s, X) ∈ ℱ ?lhs› for s X
      by (simp add: F_After ready_set_Throw that(2) F_Throw)
         (metis append_Nil empty_set inf_bot_left list.distinct(1) list.sel(1, 3))
  qed

  also have ‹?lhs = (P after e) Θ a ∈ A. Q a›
    if ‹P ≠ ⊥› and ‹ev e ∈ ready_set P› and ‹e ∉ A›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ?lhs›
    with that(2) have ‹ev e # s ∈ 𝒟 (P Θ a ∈ A. Q a)›
      by (simp add: D_After ready_set_Throw) (metis list.exhaust_sel)
    then consider ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 ∈ 𝒟 P ∧ tickFree t1 ∧
                           set t1 ∩ ev ` A = {} ∧ front_tickFree t2›
      | ‹∃t1 a t2. ev e # s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 P ∧ 
                   set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ 𝒟 (Q a)›
      by (simp add: D_Throw) blast
    thus ‹s ∈ 𝒟 ((P after e) Θ a ∈ A. Q a)›
    proof cases
      assume ‹∃t1 t2. ev e # s = t1 @ t2 ∧ t1 ∈ 𝒟 P ∧ tickFree t1 ∧
                      set t1 ∩ ev ` A = {} ∧ front_tickFree t2›
      then obtain t1 t2
        where * : ‹ev e # s = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tickFree t1›
                  ‹set t1 ∩ ev ` A = {}› ‹front_tickFree t2› by blast
      from that(1) "*"(1, 2) BOT_iff_D obtain t1'
        where ‹t1 = ev e # t1'› by (cases t1) auto
      with "*"(1, 2, 3, 4) have ‹s = t1' @ t2 ∧ t1' ∈ 𝒟 (P after e) ∧
                                 tickFree t1' ∧ set t1' ∩ ev ` A = {}›
        by (simp add: D_After that(2)) (metis list.discI list.sel(1, 3))
      with "*"(5) show ‹s ∈ 𝒟 ((P after e) Θ a ∈ A. Q a)›
        by (auto simp add: D_Throw) 
    next
      assume ‹∃t1 a t2. ev e # s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 P ∧
                   set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ 𝒟 (Q a)›
      then obtain t1 a t2
        where * : ‹ev e # s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› 
                  ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a)› by blast
      have ‹e ≠ a› using "*"(4) that(3) by blast
      with "*"(1) obtain t1' where ** : ‹t1 = ev e # t1'› by (cases t1) auto
      with "*"(2) that(2) have ‹t1' @ [ev a] ∈ 𝒯 (P after e)›
        by (simp add: T_After) (metis list.distinct(1) list.sel(1, 3))
      thus ‹s ∈ 𝒟 ((P after e) Θ a ∈ A. Q a)›
        using "*"(1, 3, 4, 5) "**" by (simp add: D_Throw) blast
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 ((P after e) Θ a ∈ A. Q a)›
    then consider ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒟 (P after e) ∧ tickFree t1 ∧
                           set t1 ∩ ev ` A = {} ∧ front_tickFree t2›
      | ‹∃t1 a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 (P after e) ∧
                   set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ 𝒟 (Q a)›
      by (simp add: D_Throw) blast
    thus ‹s ∈ 𝒟 ?lhs›
    proof cases
      assume ‹∃t1 t2. s = t1 @ t2 ∧ t1 ∈ 𝒟 (P after e) ∧ tickFree t1 ∧
                      set t1 ∩ ev ` A = {} ∧ front_tickFree t2›
      then obtain t1 t2 
        where * : ‹s = t1 @ t2› ‹t1 ∈ 𝒟 (P after e)› ‹tickFree t1› 
                  ‹set t1 ∩ ev ` A = {}› ‹front_tickFree t2› by blast
      from "*"(2) that(2) have ** : ‹ev e # t1 ∈ 𝒟 P›
        by (simp add: D_After) (metis list.exhaust_sel)
      have *** : ‹tickFree (ev e # t1) ∧ set (ev e # t1) ∩ ev ` A = {}›
        by (simp add: image_iff "*"(3, 4) that(3))
      show ‹s ∈ 𝒟 ?lhs›
        by (simp add: D_After D_Throw ready_set_Throw that(2))
           (metis "*"(1, 5) "**" "***" Cons_eq_appendI list.discI list.sel(1, 3))
    next
      assume ‹∃t1 a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 (P after e) ∧
                        set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ t2 ∈ 𝒟 (Q a)›
      then obtain t1 a t2
        where * : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P after e)›
                  ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹t2 ∈ 𝒟 (Q a)› by blast
      from "*"(2) that(2) have ** : ‹ev e # t1 @ [ev a] ∈ 𝒯 P›
        by (simp add: T_After) (metis list.exhaust_sel)
      have *** : ‹set (ev e # t1) ∩ ev ` A = {}›
        by (simp add: image_iff "*"(3) that(3))
      show ‹s ∈ 𝒟 ?lhs›
        by (simp add: D_After D_Throw ready_set_Throw that(2)) 
           (metis "*"(1, 4, 5) "**" "***" Cons_eq_appendI list.discI list.sel(1, 3))
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 (Throw (P after e) A Q)›
    assume ‹(s, X) ∈ ℱ ?lhs›
    with that(2) have ‹(ev e # s, X) ∈ ℱ (P Θ a ∈ A. Q a)›
      by (simp add: F_After ready_set_Throw) (metis list.exhaust_sel)
    then consider ‹ev e # s ∈ 𝒟 (P Θ a ∈ A. Q a)›
      | ‹(ev e # s, X) ∈ ℱ P› ‹set s ∩ ev ` A = {}›
      | ‹∃t1 a t2. ev e # s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 P ∧ 
                   set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ ℱ (Q a)›
      by (simp add: F_Throw D_Throw) blast
    thus ‹(s, X) ∈ ℱ ((P after e) Θ a ∈ A. Q a)›
    proof cases
      assume ‹ev e # s ∈ 𝒟 (P Θ a ∈ A. Q a)›
      hence ‹s ∈ 𝒟 ?lhs› by (force simp add: D_After ready_set_Throw that(2))
      with same_div D_F show ‹(s, X) ∈ ℱ ((P after e) Θ a ∈ A. Q a)› by blast
    next
      show ‹(ev e # s, X) ∈ ℱ P ⟹ set s ∩ ev ` A = {} ⟹
            (s, X) ∈ ℱ ((P after e) Θ a ∈ A. Q a)›
        by (simp add: F_Throw F_After that(2))
           (metis list.distinct(1) list.sel(1, 3))
    next
      assume ‹∃t1 a t2. ev e # s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 P ∧
                        set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ ℱ (Q a)›
      then obtain t1 a t2
        where * : ‹ev e # s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 P› 
                  ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)› by blast
      have ‹e ≠ a› using "*"(4) that(3) by blast
      with "*"(1) obtain t1' where ‹t1 = ev e # t1'› by (cases t1) auto
      also have ‹t1' @ [ev a] ∈ 𝒯 (P after e) ∧ set t1' ∩ ev ` A = {}›
        using "*"(2, 3) by (simp add: image_iff T_After that(2) calculation)
                           (metis list.distinct(1) list.sel(1, 3))
      ultimately show ‹(s, X) ∈ ℱ ((P after e) Θ a ∈ A. Q a)›
        using "*"(1, 4, 5) by (simp add: F_Throw) blast
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ?lhs = 𝒟 (Throw (P after e) A Q)›
    assume ‹(s, X) ∈ ℱ ((P after e) Θ a ∈ A. Q a)›
    then consider ‹s ∈ 𝒟 ((P after e) Θ a ∈ A. Q a)›
      | ‹(s, X) ∈ ℱ (P after e)› ‹set s ∩ ev ` A = {}›
      | ‹∃t1 a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 (P after e) ∧
                   set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ ℱ (Q a)›
      by (simp add: F_Throw D_Throw) blast
    thus ‹(s, X) ∈ ℱ ?lhs›
    proof cases
      show ‹s ∈ 𝒟 (Throw (P after e) A Q) ⟹ (s, X) ∈ ℱ ?lhs›
        using same_div D_F by blast
    next
      assume assms : ‹(s, X) ∈ ℱ (P after e)› ‹set s ∩ ev ` A = {}›
      from assms(2) have * : ‹set (ev e # s) ∩ ev ` A = {}›
        by (simp add: image_iff that(3) assms(2))
      from assms(1) have ‹(ev e # s, X) ∈ ℱ P›
        by (simp add: F_After that(2)) (metis list.exhaust_sel)
      thus ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_After F_Throw ready_set_Throw that(2))
           (metis "*" list.discI list.sel(1, 3))
    next
      assume ‹∃t1 a t2. s = t1 @ ev a # t2 ∧ t1 @ [ev a] ∈ 𝒯 (P after e) ∧
                        set t1 ∩ ev ` A = {} ∧ a ∈ A ∧ (t2, X) ∈ ℱ (Q a)›
      then obtain t1 a t2
        where * : ‹s = t1 @ ev a # t2› ‹t1 @ [ev a] ∈ 𝒯 (P after e)›
                  ‹set t1 ∩ ev ` A = {}› ‹a ∈ A› ‹(t2, X) ∈ ℱ (Q a)› by blast
      from "*"(2) that(2) have ** : ‹ev e # t1 @ [ev a] ∈ 𝒯 P›
        by (simp add: T_After) (metis list.exhaust_sel)
      have *** : ‹set (ev e # t1) ∩ ev ` A = {}›
        by (simp add: image_iff "*"(3) that(3))
      from "*"(1, 4, 5) show ‹(s, X) ∈ ℱ ?lhs›
        by (simp add: F_After F_Throw ready_set_Throw that(2)) 
           (metis  "**" "***" append_Cons list.distinct(1) list.sel(1, 3))
    qed
  qed

  ultimately show ‹?lhs = ?rhs›
    by (simp add: Throw_BOT After_BOT STOP_iff_T T_After ready_set_Throw)
qed



subsection ‹@{const [source] After} Interrupting›

theorem After_Interrupt: 
  ‹(P △ Q) after e =
   (   if ev e ∈ ready_set P ∧ ev e ∈ ready_set Q 
     then (Q after e) ⊓ (P after e △ Q)
     else    if ev e ∈ ready_set P ∧ ev e ∉ ready_set Q
           then P after e △ Q 
           else   if ev e ∉ ready_set P ∧ ev e ∈ ready_set Q
                then Q after e
                else STOP)›
proof -
  have ‹(P △ Q) after e ⊑⇩F⇩D Q after e› if ready: ‹ev e ∈ ready_set Q›
  proof (unfold failure_divergence_refine_def le_ref_def, safe)
    fix s
    assume ‹s ∈ 𝒟 (Q after e)›
    hence ‹ev e # s ∈ 𝒟 Q›
      by (simp add: D_After ready) (metis list.exhaust_sel)
    thus ‹s ∈ 𝒟 ((P △ Q) after e)›
      by (simp add: D_After ready ready_set_Interrupt D_Interrupt)
         (metis Nil_elem_T append_Nil list.distinct(1) list.sel(1, 3) tickFree_Nil)
  next
    show ‹(s, X) ∈ ℱ (Q after e) ⟹ (s, X) ∈ ℱ ((P △ Q) after e)› for s X
      by (simp add: F_After ready_set_Interrupt ready F_Interrupt)
         (metis Nil_elem_T append_Nil tickFree_Nil)
  qed

  moreover have ‹(P △ Q) after e ⊑⇩F⇩D P after e △ Q› if ready: ‹ev e ∈ ready_set P›
  proof (unfold failure_divergence_refine_def le_ref_def, safe)
    show ‹s ∈ 𝒟 (P after e △ Q) ⟹ s ∈ 𝒟 ((P △ Q) after e)› for s
      apply (simp add: D_Interrupt D_After ready T_After ready_set_Interrupt,
             elim disjE)
      by blast (metis append_Cons event.simps(3) list.sel(1, 3) neq_Nil_conv tickFree_Cons)
  next
    show ‹(s, X) ∈ ℱ (P after e △ Q) ⟹ (s, X) ∈ ℱ ((P △ Q) after e)› for s X
      apply (simp add: F_Interrupt F_After ready ready_set_Interrupt T_After D_After,
             elim disjE)
      by (metis (no_types, opaque_lifting) [[metis_verbose = false]] 
                append_Cons list.distinct(1) event.distinct(1) 
                list.exhaust_sel list.sel(1, 3) tickFree_Cons)+
  qed

  moreover have ‹Q after e ⊑⇩F⇩D (P △ Q) after e› if not_ready: ‹ev e ∉ ready_set P›
  proof (unfold failure_divergence_refine_def le_ref_def, safe)
    show ‹s ∈ 𝒟 ((P △ Q) after e) ⟹ s ∈ 𝒟 (Q after e)› for s
      by (simp add: D_After not_ready ready_set_Interrupt D_Interrupt
             split: if_split_asm)
         (metis Cons_in_T_imp_elem_ready_set D_T not_ready
                append_Nil hd_append2 list.exhaust_sel)
  next
    show ‹(s, X) ∈ ℱ ((P △ Q) after e) ⟹ (s, X) ∈ ℱ (Q after e)› for s X
      by (simp add: F_After not_ready ready_set_Interrupt F_Interrupt
             split: if_split_asm, elim exE disjE conjE)
         (metis (no_types, opaque_lifting) [[metis_verbose = false]] 
                Cons_in_T_imp_elem_ready_set F_T NF_ND hd_Cons_tl 
                snoc_eq_iff_butlast append_self_conv2 hd_append2 not_ready)+
  qed

  moreover have ‹P after e △ Q ⊑⇩F⇩D (P △ Q) after e›
    if ready_hyps: ‹ev e ∈ ready_set P› ‹ev e ∉ ready_set Q›
  proof (unfold failure_divergence_refine_def le_ref_def, safe)
    show ‹s ∈ 𝒟 ((P △ Q) after e) ⟹ s ∈ 𝒟 (P after e △ Q)› for s
      by (simp add: D_After T_After ready_hyps ready_set_Interrupt D_Interrupt)
         (metis tickFree_tl Cons_in_T_imp_elem_ready_set D_T eq_Nil_appendI
                hd_append list.exhaust_sel ready_hyps(2) tl_append_if)
  next
    fix s X
    assume ‹(s, X) ∈ ℱ ((P △ Q) after e)›
    with ready_hyps(1) have ‹(ev e # s, X) ∈ ℱ (P △ Q)›
      by (simp add: F_After ready_set_Interrupt) (metis list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ (P after e △ Q)›
      by (simp add: F_Interrupt F_After D_After T_After ready_hyps, elim disjE)
         (metis (no_types, opaque_lifting) [[metis_verbose = false]] tickFree_tl
                Cons_in_T_imp_elem_ready_set F_T NT_ND append_self_conv2 hd_append
                event.distinct(1) list.sel(1, 3) list.distinct(1) ready_hyps(2) tl_append2)+
  qed
  
  moreover have ‹(Q after e) ⊓ (P after e △ Q) ⊑⇩F⇩D (P △ Q) after e›
    if both_ready: ‹ev e ∈ ready_set P› ‹ev e ∈ ready_set Q›
  proof (unfold failure_divergence_refine_def le_ref_def, safe)
    fix s
    assume ‹s ∈ 𝒟 ((P △ Q) after e)›
    with both_ready(1) have ‹ev e # s ∈ 𝒟 (P △ Q)›
      by (simp add: D_After ready_set_Interrupt) (metis list.exhaust_sel)
    thus ‹s ∈ 𝒟 ((Q after e) ⊓ (P after e △ Q))›
      by (simp add: D_Interrupt D_After T_After D_Ndet both_ready)
         (metis tickFree_tl append_Cons append_Nil
                list.distinct(1) list.exhaust_sel list.sel(1, 3))
  next
    fix s X
    assume ‹(s, X) ∈ ℱ ((P △ Q) after e)›
    with both_ready(1) have ‹(ev e # s, X) ∈ ℱ (P △ Q)›
      by (simp add: F_After ready_set_Interrupt) (metis list.exhaust_sel)
    thus ‹(s, X) ∈ ℱ ((Q after e) ⊓ (P after e △ Q))›
      by (simp add: F_Interrupt F_After F_Ndet D_After T_After both_ready, elim disjE)
         (metis (no_types, opaque_lifting) [[metis_verbose = false]]
                event.distinct(1) hd_append2 list.distinct(1) list.sel(1, 3)
                process_charn self_append_conv2 tickFree_tl tl_append2)+
  qed

  ultimately show ?thesis
    by (auto simp add: STOP_FD_iff not_ready_After intro: FD_antisym)
       (metis mono_Ndet_FD FD_antisym Ndet_id)
qed
  


section ‹Behaviour of @{const [source] After} with Reference Processes›

lemma After_DF: ‹DF A after e = (if e ∈ A then DF A else STOP)›
  by (subst DF_unfold, subst After_Mndetprefix, simp)

lemma After_DF⇩S⇩K⇩I⇩P:
  ‹DF⇩S⇩K⇩I⇩P A after e = (if e ∈ A then DF⇩S⇩K⇩I⇩P A else STOP)›
  by (subst DF⇩S⇩K⇩I⇩P_unfold)
     (simp add: ready_set_SKIP ready_set_Mndetprefix After_Ndet After_Mndetprefix)

lemma After_RUN: ‹RUN A after e = (if e ∈ A then RUN A else STOP)›
  by (subst RUN_unfold, subst After_Mprefix, simp)

lemma After_CHAOS: ‹CHAOS A after e = (if e ∈ A then CHAOS A else STOP)›
  by (subst CHAOS_unfold)
     (simp add: After_Ndet ready_set_STOP ready_set_Mprefix After_Mprefix)

lemma After_CHAOS⇩S⇩K⇩I⇩P:
  ‹CHAOS⇩S⇩K⇩I⇩P A after e = (if e ∈ A then CHAOS⇩S⇩K⇩I⇩P A else STOP)›
  by (subst CHAOS⇩S⇩K⇩I⇩P_unfold)
     (simp add: ready_set_Ndet ready_set_STOP ready_set_SKIP 
                ready_set_Mprefix After_Ndet After_Mprefix)



lemma DF_FD_After: ‹DF A ⊑⇩F⇩D P after e›
  if ‹DF A ⊑⇩F⇩D P› and ‹ev e ∈ ready_set P›
proof -
  have ‹DF A after e ⊑⇩F⇩D P after e› by (rule mono_After_FD[OF that(1)]) 
                                       (use that(2) in ‹simp add: ready_set_DF image_iff›)
  also have ‹e ∈ A›
    by (metis After_DF DF_Univ_freeness DF_unfold STOP_FD_iff UNIV_I deadlock_free_def empty_iff 
              mono_After_FD mt_Mndetprefix non_deadlock_free_STOP ready_set_STOP that)
  ultimately show ‹DF A ⊑⇩F⇩D P after e› by (subst (asm) After_DF, simp split: if_splits)
qed


lemma DF⇩S⇩K⇩I⇩P_FD_After: ‹DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P after e›
  if ‹DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P› and ‹ev e ∈ ready_set P›
proof -
  have ‹DF⇩S⇩K⇩I⇩P A after e ⊑⇩F⇩D P after e› by (rule mono_After_FD[OF that(1)]) 
                                          (use that(2) in ‹simp add: ready_set_DF image_iff›)
  also have ‹e ∈ A› using anti_mono_ready_set_FD ready_set_DF⇩S⇩K⇩I⇩P that by fastforce
    
  ultimately show ‹DF⇩S⇩K⇩I⇩P A ⊑⇩F⇩D P after e› by (subst (asm) After_DF⇩S⇩K⇩I⇩P, simp split: if_splits)
qed
 

text ‹We have corollaries on \<^const>‹deadlock_free› and \<^const>‹deadlock_free⇩S⇩K⇩I⇩P›.›

corollary deadlock_free_After:
  ‹deadlock_free P ⟹ 
   deadlock_free (P after e) ⟷ (if ev e ∈ ready_set P then True else False)›
  apply (simp add: non_deadlock_free_STOP not_ready_After)
  unfolding deadlock_free_def by (intro impI DF_FD_After)

corollary deadlock_free⇩S⇩K⇩I⇩P_After:
  ‹deadlock_free⇩S⇩K⇩I⇩P P ⟹ 
   deadlock_free⇩S⇩K⇩I⇩P (P after e) ⟷ (if ev e ∈ ready_set P then True else False)›
  apply (simp add: non_deadlock_free⇩S⇩K⇩I⇩P_STOP not_ready_After)
  unfolding deadlock_free⇩S⇩K⇩I⇩P_FD by (intro impI DF⇩S⇩K⇩I⇩P_FD_After)


end