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 termready_set P, we can talk about what
      happens to termP after an event belonging to this set.›

section ‹Definition›

text ‹We want to define a new operator on a process termP which would in
      some way be the reciprocal of the prefix operator terme  P.›

text ‹The intuitive way of doing so is to only keep the tails of the traces
      beginning by termev e (and similar for failures and divergences).
      However we have an issue if termev e  ready_set P i.e. if no trace of
      termP begins with termev e: the result would no longer verify the 
      invariant constis_process because its trace set would be empty.
      We must therefore distinguish this case and we agree to then obtain constSTOP.
      This convention is not really decisive since we will only use this operator
      when termev 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 FD Q  ev e  ready_set P  ev e  ready_set Q  
   P after e FD 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 DT Q  P after e DT Q after e
  by (simp add: mono_After_D mono_After_T trace_divergence_refine_def)


  


section ‹Behaviour of @{const [source] After} with constSTOP, constSKIP 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 sessionHOL-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 termP after e as the reciprocal operator of the 
      prefix terme  P.

      However, we lose information with @{const [source] After}: in general,
      terme  (P after e)  P (even when termev e  ready_set P and termP  ).›

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 termQ taking
      the lead when term  ready_set P in the sequential composition termP ; 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 constSync.
      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 sessionHOL-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 termP \ A is harder to deal with, we will only obtain refinements results.›

lemma Hiding_FD_Hiding_After_if_ready_inside:
      e  B  (P \ B) FD (P after e \ B)
  and After_Hiding_FD_Hiding_After_if_ready_notin:
      e  B  (P \ B) after e FD (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) FD (P after e \ B)
   and e  B  (P \ B) after e FD (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) DT (P after e \ B)
  and After_Hiding_DT_Hiding_After_if_ready_notin: 
  ev e  ready_set P  e  B  (P \ B) after e DT (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 termP =  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 sessionHOL-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 sessionHOL-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 constSliding 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 FD 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 FD 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 FD (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 FD (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) FD (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_DFSKIP:
  DFSKIP A after e = (if e  A then DFSKIP A else STOP)
  by (subst DFSKIP_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_CHAOSSKIP:
  CHAOSSKIP A after e = (if e  A then CHAOSSKIP A else STOP)
  by (subst CHAOSSKIP_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 FD P after e
  if DF A FD P and ev e  ready_set P
proof -
  have DF A after e FD 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 FD P after e by (subst (asm) After_DF, simp split: if_splits)
qed


lemma DFSKIP_FD_After: DFSKIP A FD P after e
  if DFSKIP A FD P and ev e  ready_set P
proof -
  have DFSKIP A after e FD 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_DFSKIP that by fastforce
    
  ultimately show DFSKIP A FD P after e by (subst (asm) After_DFSKIP, simp split: if_splits)
qed
 

text ‹We have corollaries on constdeadlock_free and constdeadlock_freeSKIP.›

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_freeSKIP_After:
  deadlock_freeSKIP P  
   deadlock_freeSKIP (P after e)  (if ev e  ready_set P then True else False)
  apply (simp add: non_deadlock_freeSKIP_STOP not_ready_After)
  unfolding deadlock_freeSKIP_FD by (intro impI DFSKIP_FD_After)


end