Theory After_Operator

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : The After operator with a locale
 *
 * Copyright (c) 2025 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_Operator
  imports Initials
begin
  (*>*)


text ‹Now that we have defined term‹P0›, 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‹a → P›.›

text ‹The intuitive way of doing so is to only keep the tails of the traces
      beginning by term‹ev a› (and similar for failures and divergences).
      However we have an issue if term‹ev a ∉ P0› i.e. if no trace of
      term‹P› begins with term‹ev a›: the result would no longer verify the 
      invariant const‹is_process› because its trace set would be empty.
      We must therefore distinguish this case.›

text ‹In the previous version, we agreed to get const‹STOP› after an event term‹ev a› 
      that was not in the const‹initials› of term‹P›.
      But even if its repercussions were minimal, this choice seemed a little artificial
      and arbitrary.
      In this new version we use a placeholder instead: term‹Ψ›.
      When term‹ev a ∈ P0› we use our intuitive definition, and
      term‹ev a ∉ P0› we define term‹P› after term‹a› being equal to term‹Ψ P a›.›

text ‹For the moment we have no additional assumption on term‹Ψ›.›

locale After = 
  fixes Ψ :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
begin


lift_definition After :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick› (infixl ‹after› 86)
  is ‹λP a.   if ev a ∈ P0
            then ({(t, X). (ev a # t, X) ∈ ℱ P},
                  { t    .  ev a # t     ∈ 𝒟 P})
            else (ℱ (Ψ P a), 𝒟 (Ψ P a))›
proof -
  show ‹?thesis P a› (is ‹is_process (if _ then (?f, ?d) else _)›) for P a
  proof (split if_split, intro conjI impI)
    show ‹is_process (ℱ (Ψ P a), 𝒟 (Ψ P a))›
      by (metis CollectD Divergences.rep_eq Failures.rep_eq process0_of_process process_surj_pair)
  next
    show ‹is_process (?f, ?d)› if ‹ev a ∈ P0›
      unfolding is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv
    proof (intro conjI impI allI)
      from ‹ev a ∈ P0› show ‹([], {}) ∈ ?f› by (simp add: initials_memD T_F_spec)
    next
      show ‹(t, X) ∈ ?f ⟹ ftF t› for t X
        by simp (metis front_tickFree_Cons_iff front_tickFree_Nil is_processT2)
    next
      show ‹(t @ u, {}) ∈ ?f ⟹ (t, {}) ∈ ?f› for t u by (simp add: is_processT3)
    next
      from is_processT4 show ‹(t, Y) ∈ ?f ∧ X ⊆ Y ⟹ (t, X) ∈ ?f› for t X Y by blast
    next
      from ‹ev a ∈ P0› show ‹(t, X) ∈ ?f ∧ (∀e. e ∈ Y ⟶ (t @ [e], {}) ∉ ?f)
                             ⟹ (t, X ∪ Y) ∈ ?f› for t X Y
        by (simp add: initials_memD is_processT5)
    next
      show ‹(t @ [✓(r)], {}) ∈ ?f ⟹ (t, X - {✓(r)}) ∈ ?f› for t r X
        by (simp add: is_processT6)
    next
      from is_processT7 show ‹t ∈ ?d ∧ tF t ∧ ftF u ⟹ t @ u ∈ ?d› for t u by force
    next
      from D_F show ‹t ∈ ?d ⟹ (t, X) ∈ ?f› for t X by blast
    next
      show ‹t @ [✓(r)] ∈ ?d ⟹ t ∈ ?d› for t r
        by simp (metis append_Cons process_charn)
    qed
  qed
qed



section ‹Projections›

lemma F_After :
  ‹ℱ (P after a) = (if ev a ∈ P0 then {(t, X). (ev a # t, X) ∈ ℱ P} else ℱ (Ψ P a))›
  by (simp add: Failures_def After.rep_eq FAILURES_def)

lemma D_After :
  ‹𝒟 (P after a) = (if ev a ∈ P0 then {s. ev a # s ∈ 𝒟 P} else 𝒟 (Ψ P a))› 
  by (simp add: Divergences_def After.rep_eq DIVERGENCES_def)

lemma T_After :
  ‹𝒯 (P after a) = (if ev a ∈ P0 then {s. ev a # s ∈ 𝒯 P} else 𝒯 (Ψ P a))›
  by (auto simp add: T_F_spec[symmetric] F_After)

lemmas After_projs = F_After D_After T_After


lemma not_initial_After : ‹ev a ∉ P0 ⟹ P after a = Ψ P a›
  by (simp add: After.abs_eq Process_spec)

lemma initials_After :
  ‹(P after a)0 = (if ev a ∈ P0 then {e. ev a # [e] ∈ 𝒯 P} else (Ψ P a)0)›
  by (simp add: T_After initials_def)



section ‹Monotony›

lemma mono_After : ‹P after a ⊑ Q after a›
  if ‹P ⊑ Q› and ‹ev a ∉ Q0 ⟹ Ψ P a ⊑ Ψ Q a›
proof (subst le_approx_def, safe)
  from that(1)[THEN anti_mono_initials] that(1)[THEN le_approx2T] that[THEN le_approx1]
  show ‹t ∈ 𝒟 (Q after a) ⟹ t ∈ 𝒟 (P after a)› for t
    by (simp add: D_After initials_def subset_iff split: if_split_asm)
      (metis D_imp_front_tickFree append_Cons append_Nil butlast.simps(2) eventptick.disc(1)
        is_processT7 last.simps tickFree_Nil tickFree_butlast)
next
  from that(1)[THEN anti_mono_initials] that(2)[THEN le_approx2] that(1)[THEN proc_ord2a]
  show ‹t ∉ 𝒟 (P after a) ⟹ X ∈ ℛa (P after a) t ⟹ X ∈ ℛa (Q after a) t› for t X
    by (simp add: Refusals_after_def After_projs initials_def subset_iff split: if_split_asm)
      (metis initials_memI F_T initials_def mem_Collect_eq, blast)
next
  from that(1)[THEN anti_mono_initials] that[THEN le_approx2] that(1)[THEN le_approx2T]
  show ‹t ∉ 𝒟 (P after a) ⟹ X ∈ ℛa (Q after a) t ⟹ X ∈ ℛa (P after a) t› for t X
    by (simp add: Refusals_after_def After_projs initials_def subset_iff split: if_split_asm)
      (metis F_imp_front_tickFree append_Cons append_Nil butlast.simps(2)
        eventptick.disc(1) is_processT7 last.simps tickFree_Nil tickFree_butlast)
next
  show ‹t ∈ min_elems (𝒟 (P after a)) ⟹ t ∈ 𝒯 (Q after a)› for t 
  proof (cases ‹P = ⊥›)
    assume ‹t ∈ min_elems (𝒟 (P after a))› and ‹P = ⊥›
    hence ‹t = []›
      by (simp add: BOT_iff_Nil_D D_After D_BOT min_elems_def)
        (metis append_butlast_last_id front_tickFree_single nil_less2)
    thus ‹t ∈ 𝒯 (Q after a)› by simp
  next
    from that(1)[THEN anti_mono_initials] that(1)[THEN le_approx2T]
      that(2)[THEN le_approx3] min_elems6[OF _ _ that(1)]
    show ‹t ∈ min_elems (𝒟 (P after a)) ⟹ P ≠ ⊥ ⟹ t ∈ 𝒯 (Q after a)›
      apply (auto simp add: min_elems_def After_projs BOT_iff_Nil_D split: if_split_asm)
      by (metis T_F_spec append_butlast_last_id butlast.simps(2) less_self)
        (metis (mono_tags, lifting) T_F_spec append_Nil initials_def mem_Collect_eq)
  qed
qed


lemma mono_After_T  : ‹P ⊑T Q  ⟹ P after a ⊑T Q after a›
  and mono_After_F  : ‹P ⊑F Q  ⟹ P after a ⊑F Q after a›
  and mono_After_D  : ‹P ⊑D Q  ⟹ P after a ⊑D Q after a›
  and mono_After_FD : ‹P ⊑FD Q ⟹ P after a ⊑FD Q after a›
  and mono_After_DT : ‹P ⊑DT Q ⟹ P after a ⊑DT Q after a›
  if ‹ev a ∈ Q0›
  using that F_subset_imp_T_subset[of Q P] D_T[of ‹ev a # _› P]
  unfolding failure_divergence_refine_def trace_divergence_refine_def
    failure_refine_def divergence_refine_def trace_refine_def
  by (auto simp add: After_projs initials_def)
    (metis initials_memI in_mono mem_Collect_eq initials_def)

lemmas monos_After = mono_After mono_After_FD mono_After_DT
  mono_After_F mono_After_D mono_After_T



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

lemma After_STOP : ‹STOP after a = Ψ STOP a›
  by (simp add: Process_eq_spec After_projs)

lemma After_SKIP : ‹SKIP r after a = Ψ (SKIP r) a›
  by (simp add: Process_eq_spec After_projs)

lemma After_BOT : ‹⊥ after a = ⊥›
  by (force simp add: BOT_iff_Nil_D D_After D_BOT)

lemma After_is_BOT_iff :
  ‹P after a = ⊥ ⟷ (if ev a ∈ P0 then [ev a] ∈ 𝒟 P else Ψ P a = ⊥)›
  using hd_Cons_tl by (force simp add: BOT_iff_Nil_D D_After initials_def D_T)



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

text ‹In future theories, we will need to know how @{const [source] After}
      behaves with other operators of CSP.
      More specifically, we want to know how @{const [source] After} can be "distributed"
      over a sequential composition, a synchronization, etc.›

text ‹In some way, we are looking for reversing the "step-laws"
      (laws of distributivity of const‹Mprefix› over other operators).
      Given the difficulty in establishing these results in session‹HOL-CSP›
      and session‹HOL-CSPM›, one can easily imagine that proving
      @{const [source] After} versions will require a lot of work.›



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 ⟹ (□a ∈ A → P a) after a = (⊓a ∈ A → P a) after a›
  by (auto simp add: Process_eq_spec initials_Mprefix initials_Mndetprefix
      After_projs Mprefix_projs Mndetprefix_projs)

lemma After_Det_is_After_Ndet :
  ‹ev a ∈ P0 ∪ Q0 ⟹ (P □ Q) after a = (P ⊓ Q) after a›
  by (auto simp add: Process_eq_spec initials_Det initials_Ndet
      After_projs Det_projs Ndet_projs)

lemma After_Sliding_is_After_Ndet :
  ‹ev a ∈ P0 ∪ Q0 ⟹ (P ⊳ Q) after a = (P ⊓ Q) after a›
  by (auto simp add: Process_eq_spec initials_Sliding initials_Ndet
      After_projs Sliding_projs Ndet_projs)


lemma After_Ndet: 
  ‹(P ⊓ Q) after a = 
   (  if ev a ∈ P0 ∩ Q0 then P after a ⊓ Q after a
    else   if ev a ∈ P0 then P after a
         else   if ev a ∈ Q0 then Q after a
              else Ψ (P ⊓ Q) a)› for P Q :: ‹('a, 'r) processptick›
proof -
  { fix P Q :: ‹('a, 'r) processptick›
    assume ‹ev a ∈ P0› ‹ev a ∉ Q0›
    hence ‹(P ⊓ Q) after a = P after a›
      by (simp add: Process_eq_spec After_projs Ndet_projs initials_Ndet)
        (meson initials_memI D_T F_T)
  }
  moreover have ‹ev a ∉ P0 ∪ Q0 ⟹ (P ⊓ Q) after a = Ψ (P ⊓ Q) a›
    by (simp add: Process_eq_spec After_projs initials_Ndet)
  moreover have ‹ev a ∈ P0 ∩ Q0 ⟹  (P ⊓ Q) after a = P after a ⊓ Q after a›
    by (auto simp add: Process_eq_spec After_projs Ndet_projs initials_Ndet)
  ultimately show ?thesis by (metis Int_iff Ndet_commute Un_iff)
qed

lemma After_Det: 
  ‹(P □ Q) after a = 
   (  if ev a ∈ P0 ∩ Q0 then P after a ⊓ Q after a
    else   if ev a ∈ P0 then P after a
         else   if ev a ∈ Q0 then Q after a
              else Ψ (P □ Q) a)›
  by (simp add: After_Det_is_After_Ndet After_Ndet not_initial_After initials_Det)

lemma After_Sliding:
  ‹(P ⊳ Q) after a = 
   (  if ev a ∈ P0 ∩ Q0 then P after a ⊓ Q after a
    else   if ev a ∈ P0 then P after a
         else   if ev a ∈ Q0 then Q after a
              else Ψ (P ⊳ Q) a)›
  by (simp add: After_Ndet After_Sliding_is_After_Ndet initials_Sliding not_initial_After)


lemma After_Mprefix:
  ‹(□ a ∈ A → P a) after a = (if a ∈ A then P a else Ψ (□ a ∈ A → P a) a)›
  by (simp add: Process_eq_spec After_projs initials_Mprefix
      Mprefix_projs image_iff)

lemma After_Mndetprefix:
  ‹(⊓ a ∈ A → P a) after a = (if a ∈ A then P a else Ψ (⊓ a ∈ A → P a) a)›
  by (metis (full_types) After_Mprefix After_Mprefix_is_After_Mndetprefix
      eventptick.inject(1) imageE not_initial_After initials_Mndetprefix)

corollary After_write0 : ‹(a → P) after b = (if b = a then P else Ψ (a → P) b)›
  by (simp add: write0_def After_Mprefix)

lemma ‹(a → P) after a = P› by (simp add: After_write0)

text ‹This result justifies seeing term‹P after a› as the reciprocal operator of the 
      prefix term‹a → P›.

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

lemma ‹∃P. a → P after a ≠ P›
proof (intro exI)
  show ‹a → SKIP undefined after a ≠ SKIP undefined› by simp
qed

lemma ‹∃P. ev a ∈ P0 ∧ a → P after a ≠ P›
  by (metis UNIV_I initials_BOT write0_neq_BOT)

lemma ‹∃P. ev a ∈ P0 ∧ P ≠ ⊥ ∧ a → P after a ≠ P›
proof (intro exI)
  define P :: ‹('a, 'r) processptick› where P_def: ‹P = (a → STOP) □ SKIP undefined›
  have * : ‹ev a ∈ P0› by (simp add: P_def initials_Det initials_write0)
  moreover have ‹P ≠ ⊥› by (simp add: Det_is_BOT_iff P_def)
  moreover have ‹a → P after a = a → STOP›
    by (rule arg_cong[where f = ‹λP. a → P›])
      (simp add: P_def After_Det initials_write0 After_write0)
  moreover have ‹a → STOP ≠ P›
    by (rule contrapos_nn[of ‹(a → STOP)0 = P0› ‹a → STOP = P›])
      (auto simp add: P_def initials_Det initials_write0)
  ultimately show ‹ev a ∈ P0 ∧ P ≠ ⊥ ∧ a → P after a ≠ P› by presburger
qed


corollary After_write : ‹(c!a → P) after b = (if b = c a then P else Ψ (c!a → P) b)›
  by (simp add: write_def After_Mprefix)

corollary After_read :
  ‹(c?a∈A → P a) after b = (if b ∈ c ` A then P (inv_into A c b) else Ψ (c?a∈A → P a) b)›
  by (simp add: read_def After_Mprefix)

corollary After_ndet_write :
  ‹(c!!a∈A → P a) after b = (if b ∈ c ` A then P (inv_into A c b) else Ψ (c!!a∈A → P a) b)›
  by (simp add: ndet_write_def After_Mndetprefix)



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

text ‹The first goal is to obtain an equivalent of 
      @{thm Mprefix_Seq[of ‹{a}› ‹λ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‹✓(r) ∈ P0› in the sequential composition term‹P ; Q›.›

lemma not_skippable_or_not_initialR_After_Seq:
  ‹(P ; Q) after a = (if ev a ∈ P0 then P after a ; Q else Ψ (P ; Q) a)›
  if ‹range tick ∩ P0 = {} ∨ (∀r. ✓(r) ∈ P0 ⟶ ev a ∉ Q0)›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹
        (P ; Q) after a =
        (if ev a ∈ P0 then P after a ; Q else Ψ (P ; Q) a)›
    by (simp add: After_BOT)
next
  assume non_BOT: ‹P ≠ ⊥›
  with that have $ : ‹ev a ∈ (P ; Q)0 ⟷ ev a ∈ P0›
    by (auto simp add: initials_Seq)
  show ‹(P ; Q) after a =
        (if ev a ∈ P0 then P after a ; Q else Ψ (P ; Q) a)›
  proof (split if_split, intro conjI impI)
    from "$" show ‹ev a ∉ P0 ⟹ (P ; Q) after a = Ψ (P ; Q) a›
      by (simp add: not_initial_After)
  next
    assume initial_P : ‹ev a ∈ P0›
    show ‹(P ; Q) after a = P after a ; Q›
    proof (subst Process_eq_spec_optimized, safe)
      fix s
      assume ‹s ∈ 𝒟 ((P ; Q) after a)›
      hence * : ‹ev a # s ∈ 𝒟 (P ; Q)›
        by (simp add: D_After "$" initial_P split: if_split_asm)
      then consider ‹ev a # s ∈ 𝒟 P› 
        | t1 t2 r where ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
        by (simp add: D_Seq) blast
      thus ‹s ∈ 𝒟 (P after a ; Q)›
      proof cases
        show ‹ev a # s ∈ 𝒟 P ⟹ s ∈ 𝒟 (P after a ; Q)›
          by (simp add: D_Seq D_After initial_P)
      next
        fix t1 t2 r assume ** : ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
        have ‹t1 ≠ []› by (metis "**" initials_memI D_T
              append_self_conv2 disjoint_iff rangeI that)
        with "**"(1) obtain t1'
          where ‹t1 = ev a # t1'› ‹s = t1' @ t2› by (metis Cons_eq_append_conv)
        with "**"(2, 3) show ‹s ∈ 𝒟 (P after a ; Q)›
          by (simp add: D_Seq T_After) (blast intro: initial_P)
      qed
    next
      fix s
      assume ‹s ∈ 𝒟 (P after a; Q)›
      hence ‹ev a # s ∈ 𝒟 P ∨ (∃t1 t2 r. s = t1 @ t2 ∧ ev a # t1 @ [✓(r)] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q)›
        by (simp add: D_Seq After_projs initial_P)
      hence ‹ev a # s ∈ 𝒟 (P ; Q)›
        by (elim disjE; simp add: D_Seq) (metis append_Cons)
      thus ‹s ∈ 𝒟 ((P ; Q) after a)›
        by (simp add: D_After "$" initial_P)
    next
      fix s X
      assume same_div : ‹𝒟 ((P ; Q) after a) = 𝒟 (P after a ; Q)›
      assume ‹(s, X) ∈ ℱ ((P ; Q) after a)›
      then consider ‹ev a ∈ (P ; Q)0› ‹(ev a # s, X) ∈ ℱ (P ; Q)›
        | ‹ev a ∉ (P ; Q)0› ‹s = []› by (simp add: F_After "$" initial_P)
      thus ‹(s, X) ∈ ℱ (P after a ; Q)›
      proof cases
        assume assms : ‹ev a ∈ (P ; Q)0› ‹(ev a # s, X) ∈ ℱ (P ; Q)›
        from assms(2) consider ‹ev a # s ∈ 𝒟 (P ; Q)›
          | ‹(ev a # s, X ∪ range tick) ∈ ℱ P› ‹tF s›
          | t1 t2 r where ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q›
          by (simp add: F_Seq D_Seq) blast
        thus ‹(s, X) ∈ ℱ (P after a ; Q)›
        proof cases
          assume ‹ev a # s ∈ 𝒟 (P ; Q)›
          hence ‹s ∈ 𝒟 ((P ; Q) after a)›
            by (simp add: D_After assms(1))
          with same_div D_F show ‹(s, X) ∈ ℱ (P after a ; Q)› by blast
        next
          show ‹(ev a # s, X ∪ range tick) ∈ ℱ P ⟹ tF s ⟹ (s, X) ∈ ℱ (P after a ; Q)›
            by (simp add: F_Seq F_After initial_P)
        next
          fix t1 t2 r assume * : ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q›
          have ‹t1 ≠ []› by (metis "*" initials_memI F_T
                disjoint_iff rangeI self_append_conv2 that)
          with "*"(1) obtain t1'
            where ‹t1 = ev a # t1'› ‹s = t1' @ t2› by (metis Cons_eq_append_conv)
          with "*"(2, 3) show ‹(s, X) ∈ ℱ (P after a ; Q)›
            by (simp add: F_Seq T_After) (blast intro: initial_P)
        qed
      next
        show ‹ev a ∉ (P ; Q)0 ⟹ s = [] ⟹ (s, X) ∈ ℱ (P after a ; Q)›
          by (simp add: F_Seq F_After "$" initial_P)
      qed
    next
      fix s X
      assume same_div : ‹𝒟 ((P ; Q) after a) = 𝒟 (P after a ; Q)›
      assume ‹(s, X) ∈ ℱ (P after a ; Q)›
      then consider ‹s ∈ 𝒟 (P after a ; Q)›
        | ‹(s, X ∪ range tick) ∈ ℱ (P after a)› ‹tF s›
        | t1 t2 r where ‹s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 (P after a)› ‹(t2, X) ∈ ℱ Q›
        by (simp add: F_Seq D_Seq) blast
      thus ‹(s, X) ∈ ℱ ((P ; Q) after a)›
      proof cases
        from same_div D_F show ‹s ∈ 𝒟 (P after a ; Q) ⟹ (s, X) ∈ ℱ ((P ; Q) after a)› by blast
      next
        show ‹(s, X ∪ range tick) ∈ ℱ (P after a) ⟹ tF s ⟹ (s, X) ∈ ℱ ((P ; Q) after a)›
          by (simp add: F_After "$" initial_P F_Seq)
      next
        fix t1 t2 r assume * : ‹s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 (P after a)› ‹(t2, X) ∈ ℱ Q›
        from "*"(2) have ‹ev a # t1 @ [✓(r)] ∈ 𝒯 P› by (simp add: T_After initial_P)
        with "*"(1, 3) show ‹(s, X) ∈ ℱ ((P ; Q) after a)›
          by (simp add: F_After "$" initial_P F_Seq) (metis append_Cons)
      qed
    qed
  qed
qed


lemma skippable_not_initialL_After_Seq:
  ‹(P ; Q) after a = (  if (∃r. ✓(r) ∈ P0) ∧ ev a ∈ Q0
                      then Q after a else Ψ (P ; Q) a)›
  (is ‹(P ; Q) after a = (if ?prem then ?rhs else _)›) if ‹ev a ∉ P0›
proof -
  from initials_BOT ‹ev a ∉ P0› have non_BOT : ‹P ≠ ⊥› by blast
  with ‹ev a ∉ P0› have $ : ‹ev a ∈ (P ; Q)0 ⟷ ?prem›
    by (auto simp add: initials_Seq)
  show ‹(P ; Q) after a = (if ?prem then ?rhs else Ψ (P ; Q) a)›
  proof (split if_split, intro conjI impI)
    show ‹¬ ?prem ⟹ (P ; Q) after a = Ψ (P ; Q) a›
      by (rule not_initial_After, use "$" in blast)
  next
    show ‹(P ; Q) after a = ?rhs› if ?prem
    proof (subst Process_eq_spec, safe)
      fix t
      assume ‹t ∈ 𝒟 ((P ; Q) after a)›
      with ‹?prem› have ‹ev a # t ∈ 𝒟 (P ; Q)› by (simp add: D_After "$")
      with ‹ev a ∉ P0› obtain t1 t2 r where * : ‹ev a # t = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
        by (simp add: D_Seq) (meson initials_memI D_T)
      from "*"(1, 2) ‹ev a ∉ P0› initials_memI have ‹t1 = []›
        by (cases t1; simp) blast
      with "*" show ‹t ∈ 𝒟 ?rhs›
        by (auto simp add: D_After intro: initials_memI D_T)
    next
      from ‹?prem› show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ((P ; Q) after a)› for s
        by (simp add: D_After "$" D_Seq split: if_split_asm)
          (metis append_Nil initials_memD)
    next
      fix t X
      assume ‹(t, X) ∈ ℱ ((P ; Q) after a)›
      hence ‹ev a ∈ (P ; Q)0› ‹(ev a # t, X) ∈ ℱ (P ; Q)›
        by (simp_all add: F_After "$" split: if_split_asm) (use ‹?prem› in blast)+
      thus ‹(t, X) ∈ ℱ ?rhs›
        by (simp add: F_After F_Seq "$")
          (metis (no_types, lifting) initials_memI D_T F_T Nil_is_append_conv
            append_self_conv2 hd_append2 list.exhaust_sel list.sel(1) ‹ev a ∉ P0›)
    next
      show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ((P ; Q) after a)› for s X
        by (simp add: F_After "$" F_Seq split: if_split_asm)
          (metis append_Nil initials_memD ‹?prem›, use ‹?prem› in blast)
    qed
  qed
qed


lemma skippable_initialL_initialR_After_Seq:
  ‹(P ; Q) after a = (P after a ; Q) ⊓ Q after a›
  (is ‹(P ; Q) after a = (P after a ; Q) ⊓ ?rhs›)
  if assms : ‹(∃r. ✓(r) ∈ P0) ∧ ev a ∈ Q0› ‹ev a ∈ P0›
proof (cases ‹P = ⊥›)
  show ‹P = ⊥ ⟹ (P ; Q) after a = (P after a ; Q) ⊓ ?rhs›
    by (simp add: After_BOT)
next
  show ‹(P ; Q) after a = (P after a ; Q) ⊓ ?rhs› if ‹P ≠ ⊥›
  proof (subst Process_eq_spec_optimized, safe)
    fix s
    assume ‹s ∈ 𝒟 ((P ; Q) after a)›
    hence ‹ev a # s ∈ 𝒟 (P ; Q)›
      by (simp add: D_After initials_Seq ‹P ≠ ⊥› ‹ev a ∈ P0› image_iff)
    then consider ‹ev a # s ∈ 𝒟 P›
      | t1 t2 r where ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
      by (simp add: D_Seq) blast
    thus ‹s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
    proof cases
      show ‹ev a # s ∈ 𝒟 P ⟹ s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
        by (simp add: D_After D_Seq D_Ndet ‹P ≠ ⊥› assms(2))
    next
      fix t1 t2 r assume * : ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹t2 ∈ 𝒟 Q›
      show ‹s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
      proof (cases ‹t1 = []›)
        from "*"(1, 3) assms(1) show ‹t1 = [] ⟹ s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
          by (simp add: D_After D_Ndet)
      next
        assume ‹t1 ≠ []›
        with "*"(1, 3) obtain t1' where ‹t1 = ev a # t1'› by (cases t1; simp)
        with "*" show ‹s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
          by (simp add: T_After D_Seq D_Ndet assms(2)) blast
      qed
    qed
  next
    fix s
    assume ‹s ∈ 𝒟 ((P after a ; Q) ⊓ ?rhs)›
    then consider ‹s ∈ 𝒟 (P after a ; Q)› | ‹s ∈ 𝒟 ?rhs›
      by (simp add: D_Ndet) blast
    thus ‹s ∈ 𝒟 ((P ; Q) after a)›
    proof cases
      show ‹s ∈ 𝒟 (P after a ; Q) ⟹ s ∈ 𝒟 ((P ; Q) after a)›
        by (simp add: After_projs D_Seq initials_Seq ‹P ≠ ⊥› assms(2) image_iff)
          (metis append_Cons)
    next
      from assms show ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ((P ; Q) after a)›
        by (simp add: D_After D_Seq initials_Seq ‹P ≠ ⊥› split: if_split_asm)
          (metis append_Nil initials_def mem_Collect_eq)
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ((P ; Q) after a) = 𝒟 ((P after a ; Q) ⊓ ?rhs)›
    assume ‹(s, X) ∈ ℱ ((P ; Q) after a)›
    hence ‹(ev a # s, X) ∈ ℱ (P ; Q)›
      by (simp add: F_After initials_Seq ‹P ≠ ⊥› assms(2) image_iff)
    then consider ‹ev a # s ∈ 𝒟 P›
      | ‹(ev a # s, X ∪ range tick) ∈ ℱ P› ‹tF s›
      | t1 t2 r where ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q›
      by (simp add: F_Seq D_Seq) blast
    thus ‹(s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
    proof cases
      assume ‹ev a # s ∈ 𝒟 P›
      hence ‹s ∈ 𝒟 (P after a ; Q)› 
        by (simp add: D_After D_Seq assms(2))
      with same_div D_Ndet D_F show ‹(s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)› by blast
    next
      show ‹(ev a # s, X ∪ range tick) ∈ ℱ P ⟹ tF s ⟹
            (s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
        by (simp add: F_Ndet F_Seq F_After assms(2))
    next
      fix t1 t2 r assume * : ‹ev a # s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 P› ‹(t2, X) ∈ ℱ Q›
      show ‹(s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
      proof (cases ‹t1 = []›)
        from "*"(1, 3) assms show ‹t1 = [] ⟹ (s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
          by (simp add: F_Ndet F_Seq F_After assms(2))
      next
        assume ‹t1 ≠ []›
        with "*"(1, 3) obtain t1' where ‹t1 = ev a # t1'› by (cases t1; simp)
        with "*" show ‹(s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
          by (simp add: F_Ndet F_Seq F_After T_After assms(2)) blast
      qed
    qed
  next
    fix s X
    assume same_div : ‹𝒟 ((P ; Q) after a) = 𝒟 ((P after a ; Q) ⊓ ?rhs)›
    assume ‹(s, X) ∈ ℱ ((P after a ; Q) ⊓ ?rhs)›
    then consider ‹(s, X) ∈ ℱ (P after a ; Q)› | ‹(s, X) ∈ ℱ ?rhs›
      by (simp add: F_Ndet) blast
    thus ‹(s, X) ∈ ℱ ((P ; Q) after a)›
    proof cases
      assume ‹(s, X) ∈ ℱ (P after a ; Q)›
      then consider ‹s ∈ 𝒟 (P after a ; Q)›
        | ‹(s, X ∪ range tick) ∈ ℱ (P after a)› ‹tF s›
        | t1 t2 r where ‹s = t1 @ t2› ‹t1 @ [✓(r)] ∈ 𝒯 (P after a)› ‹(t2, X) ∈ ℱ Q›
        by (simp add: F_Seq D_Seq) blast
      thus ‹(s, X) ∈ ℱ ((P ; Q) after a)›
      proof cases
        show ‹s ∈ 𝒟 (P after a ; Q) ⟹ (s, X) ∈ ℱ ((P ; Q) after a)›
          using same_div D_Ndet D_F by blast
      next
        show ‹(s, X ∪ range tick) ∈ ℱ (P after a) ⟹ tF s ⟹ (s, X) ∈ ℱ ((P ; Q) after a)›
          by (simp add: F_After F_Seq initials_Seq assms(2) image_iff)
      next
        show ‹s = t1 @ t2 ⟹ t1 @ [✓(r)] ∈ 𝒯 (P after a) ⟹ (t2, X) ∈ ℱ Q
              ⟹ (s, X) ∈ ℱ ((P ; Q) after a)› for t1 t2 r
          by (simp add: F_After T_After F_Seq initials_Seq
              assms(2) image_iff ‹P ≠ ⊥›) (metis Cons_eq_appendI)
      qed
    next
      from assms(1) ‹P ≠ ⊥› show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ((P ; Q) after a)›
        by (simp add: F_GlobalNdet F_After F_Seq initials_Seq image_iff split: if_split_asm)
          (simp add: initials_def, metis append_Nil)
    qed
  qed
qed


lemma not_initialL_not_skippable_or_not_initialR_After_Seq:
  ‹ev a ∉ P0 ⟹ range tick ∩ P0 = {} ∨ (∀r. tick r ∈ P0 ⟶ ev a ∉ Q0) ⟹ 
   (P ; Q) after a = Ψ (P ; Q) a› 
  by (simp add: not_skippable_or_not_initialR_After_Seq not_initial_After)


lemma After_Seq:
  ‹(P ; Q) after a =
   (  if range tick ∩ P0 = {} ∨ (∀r. ✓(r) ∈ P0 ⟶ ev a ∉ Q0)
    then   if ev a ∈ P0 then P after a ; Q else Ψ (P ; Q) a
    else   if ev a ∈ P0
         then (P after a ; Q) ⊓ Q after a
         else Q after a)›
  by (simp add: not_skippable_or_not_initialR_After_Seq
      skippable_initialL_initialR_After_Seq skippable_not_initialL_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_Mprefix}

      We will also divide the task.›

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

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

lemma initialL_not_initialR_not_in_After_Sync:
  ‹(P ⟦S⟧ Q) after a = P after a ⟦S⟧ Q›
  if initial_hyps: ‹ev a ∈ P0› ‹ev a ∉ Q0› and notin: ‹a ∉ S›
proof (subst Process_eq_spec_optimized, safe)
  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
      and same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q)›
    have ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)›
    proof (cases ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›)
      case True
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a)›
        by (force simp add: D_After initials_Sync initial_hyps(1) assms(1, 2) notin)
      with D_F same_div show ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)› 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 a # s) setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_Sync D_Sync) blast
      have ** : ‹s_P ≠ [] ∧ hd s_P = ev a ∧ s setinterleaves ((tl s_P, s_Q), range tick ∪ ev ` S)›
        using *(3) apply (cases s_P; cases s_Q; simp add: notin image_iff split: if_split_asm)
        using "*"(2) initials_memI F_T initial_hyps(2) by blast+
      hence ‹(tl s_P, X_P) ∈ ℱ (P after a) ∧ (s_Q, X_Q) ∈ ℱ Q ∧
             s setinterleaves ((tl s_P, s_Q), range tick ∪ ev ` S) ∧
             X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_After "**" initial_hyps(1))
          (metis "*"(1) "*"(2) "*"(4) "**" list.exhaust_sel)
      thus ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    qed
  } note * = this

  show ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q) ⟹
        (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a) ⟹ (s, X) ∈ ℱ (P after a ⟦S⟧ Q)› for s X
    by (simp add: "*" F_After initials_Sync initial_hyps notin image_iff split: if_split_asm)
      (metis After_BOT BOT_Sync CollectI D_BOT F_imp_front_tickFree Sync_BOT
        front_tickFree_Cons_iff front_tickFree_Nil is_processT8)
next

  fix s X
  assume same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q)›
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)›
    from assms(3) consider
      ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ (P after a) ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                          s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S) ∧ 
                          X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
      by (simp add: F_Sync D_Sync) blast
    hence ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q
        where * : ‹(ev a # s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q› 
          ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        by (simp add: F_After initial_hyps(1)) blast
      have ‹(s_Q, X_Q) ∈ ℱ Q ∧ 
            (ev a # s) setinterleaves ((ev a # s_P, s_Q), range tick ∪ ev ` S) ∧
             X = (X_P ∪ X_Q) ∩ (range tick ∪ 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 a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    next
      case 2
      from "2"[simplified same_div[symmetric]]
      have ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)› 
        by (simp add: D_After initial_hyps(1) initials_Sync assms(1, 2) image_iff notin)
      with D_F show ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)› by blast
    qed
  }
  thus ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a)› 
    by (simp add: F_After initials_Sync initial_hyps After_BOT F_BOT image_iff
        notin F_imp_front_tickFree front_tickFree_Cons_iff)
next

  { fix s
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
    from assms(3) obtain t u r v
      where * : ‹ftF v› ‹tF  r ∨ v = []› ‹ev a # s = r @ v›
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by (simp add: D_Sync) blast
    have ** : ‹r ≠ [] ∧ hd r = ev a›
      by (metis "*"(3, 4, 5) BOT_iff_Nil_D assms(1, 2) empty_setinterleaving hd_append list.sel(1))
    hence *** : ‹(t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ⟶ t ≠ [] ∧ hd t = ev a ∧ 
                              tl r setinterleaves ((tl t, u), range tick ∪ ev ` S)) ∧ 
                 (t ∈ 𝒟 Q ∧ u ∈ 𝒯 P ⟶ u ≠ [] ∧ hd u = ev a ∧ 
                              tl r setinterleaves ((t, tl u), range tick ∪ ev ` S))›
      using *(4) assms(1, 2)[simplified BOT_iff_Nil_D] initial_hyps[simplified initials_def] notin
      by (cases t; cases u; simp split: if_split_asm)
        (metis [[metis_verbose = false]] initials_memI D_T 
          list.sel(1) list.sel(3) initial_hyps(2))+
    from *(5) have ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
      hence ‹ftF v ∧ (tF  (tl r) ∨ v = []) ∧ s = tl r @ v ∧
             tl r setinterleaves ((tl t, u), range tick ∪ ev ` S) ∧
             tl t ∈ 𝒟 (P after a) ∧ u ∈ 𝒯 Q›
        by (simp add: D_After initial_hyps(1))
          (metis "*"(1, 2, 3) "**" "***" list.collapse list.sel(3) 
            tickFree_tl tl_append2)
      thus ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)› by (simp add: D_Sync) blast
    next
      assume ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
      hence ‹ftF v ∧ (tF  (tl r) ∨ v = []) ∧ s = tl r @ v ∧
             tl r setinterleaves ((t, tl u), range tick ∪ ev ` S) ∧
             t ∈ 𝒟 Q ∧ tl u ∈ 𝒯 (P after a)›
        by (simp add: T_After initial_hyps(1))
          (metis "*"(1, 2, 3) "**" "***" list.collapse
            list.sel(3) tickFree_tl tl_append2)
      thus ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
        by (simp add: D_Sync) blast
    qed
  } note * = this

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a) ⟹ s ∈ 𝒟 (P after a ⟦S⟧ Q)› for s
    by (simp add: D_After initials_Sync initial_hyps notin image_iff "*"
        split: if_split_asm)
      (elim disjE;
        simp add: After_BOT D_BOT, metis front_tickFree_Cons_iff front_tickFree_Nil)
next 

  fix s
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
    from assms(3) obtain t u r v
      where * : ‹ftF v› ‹tF  r ∨ v = []› ‹s = r @ v› 
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)› 
        ‹t ∈ 𝒟 (P after a) ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 (P after a)›
      by (simp add: D_Sync) blast
    from "*"(5) have ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P after a) ∧ u ∈ 𝒯 Q›
      with "*"(1, 2, 3, 4) initial_hyps(1)
      have ** : ‹ftF v ∧ (tF  (ev a # r) ∨ v = []) ∧ s = r @ v ∧
                 (ev a # r) setinterleaves ((ev a # t, u), range tick ∪ ev ` S) ∧
                 ev a # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
        by (cases u; simp add: D_After notin image_iff)
      show ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync) (metis "**" Cons_eq_appendI)
    next
      assume ‹t ∈ 𝒟 Q ∧ u ∈ 𝒯 (P after a)›
      with "*"(1, 2, 3, 4) initial_hyps(1)
      have ** : ‹ftF v ∧ (tF  (ev a # r) ∨ v = []) ∧ s = r @ v ∧
                 (ev a # r) setinterleaves ((t, ev a # u), range tick ∪ ev ` S) ∧
                 t ∈ 𝒟 Q ∧ ev a # u ∈ 𝒯 P›
        by (cases t; simp add: T_After notin image_iff)
      show ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync) (metis "**" Cons_eq_appendI)
    qed
  }
  thus ‹s ∈ 𝒟 (P after a ⟦S⟧ Q) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after a)›
    by (simp add: D_After initials_Sync initial_hyps After_BOT D_BOT
        notin image_iff D_imp_front_tickFree front_tickFree_Cons_iff)
qed



lemma not_initialL_in_After_Sync:
  ‹ev a ∉ P0 ⟹ a ∈ S ⟹ 
   (P ⟦S⟧ Q) after a = (if Q = ⊥ then ⊥ else Ψ (P ⟦S⟧ Q) a)›
  by (simp add: After_BOT, intro impI)
    (subst not_initial_After, auto simp add: After_BOT initials_Sync)



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

lemma initialL_initialR_in_After_Sync:
  ‹(P ⟦S⟧ Q) after a = P after a ⟦S⟧ Q after a› 
  if initial_hyps: ‹ev a ∈ P0› ‹ev a ∈ Q0› and inside: ‹a ∈ S›
proof (subst Process_eq_spec_optimized, safe)

  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)› 
      and same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q after a)›
    from assms(3) consider
      ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                         (ev a # s) setinterleaves ((s_P, s_Q), range tick ∪ ev ` S) ∧ 
                         X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› |
      ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: F_Sync D_Sync) blast
    hence ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q after a)›
    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 a # s) setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› by blast
      from *(3) have ‹s_P ≠ [] ∧ hd s_P = ev a ∧ s_Q ≠ [] ∧ hd s_Q = ev a ∧
                      s setinterleaves ((tl s_P, tl s_Q), range tick ∪ 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 a) ∧ (tl s_Q, X_Q) ∈ ℱ (Q after a) ∧
            s setinterleaves ((tl s_P, tl s_Q), range tick ∪ ev ` S) ∧
            X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
        using "*"(1, 2, 4) initial_hyps by (simp add: F_After) (metis list.exhaust_sel)
      thus ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q after a)›
        by (simp add: F_Sync) blast
    next
      assume ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a)› 
        by (force simp add: D_After initials_Sync initial_hyps assms(1, 2))
      from this[simplified same_div] D_F
      show ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q after a)› by blast
    qed
  } note * = this

  show ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q after a) ⟹
        (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a) ⟹ (s, X) ∈ ℱ (P after a ⟦S⟧ Q after a)› for s X
    by (simp add: "*" F_After initials_Sync initial_hyps image_iff split: if_split_asm)
      (metis After_BOT BOT_Sync BOT_iff_Nil_D CollectI D_BOT F_imp_front_tickFree
        Sync_BOT front_tickFree_Cons_iff is_processT8)
next

  fix s X
  assume same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 (P after a ⟦S⟧ Q after a)›
  { assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q after a)›
    from assms(3) consider 
      ‹∃s_P s_Q X_P X_Q. (ev a # s_P, X_P) ∈ ℱ P ∧ (ev a # s_Q, X_Q) ∈ ℱ Q ∧
                         s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S) ∧ 
                         X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 (P after a ⟦S⟧ Q after a)›
      by (simp add: F_Sync D_Sync F_After initial_hyps) blast
    hence ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      case 1
      then obtain s_P s_Q X_P X_Q 
        where * : ‹(ev a # s_P, X_P) ∈ ℱ P› ‹(ev a # s_Q, X_Q) ∈ ℱ Q› 
          ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› by blast
      have ** : ‹(ev a # s) setinterleaves ((ev a # s_P, ev a # s_Q), range tick ∪ ev ` S)›
        by (simp add: inside "*"(3))
      show ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        apply (simp add: F_Sync)
        using "*"(1, 2, 4) "**" by blast
    next
      assume ‹s ∈ 𝒟 (P after a ⟦S⟧ Q after a)›
      with same_div[symmetric] have ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_After initial_hyps initials_Sync assms(1, 2) image_iff)
      with D_F show ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)› by blast
    qed
  }
  thus ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q after a) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a)›
    by (simp add: F_After initials_Sync initial_hyps F_BOT image_iff
        F_imp_front_tickFree front_tickFree_Cons_iff)
next

  { fix s
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)› 
    from assms(3) obtain t u r v
      where * : ‹ftF v› ‹tF  r ∨ v = []› ‹ev a # s = r @ v›
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)› 
        ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P› by (simp add: D_Sync) blast
    have ** : ‹r ≠ [] ∧ hd r = ev a ∧ t ≠ [] ∧ hd t = ev a ∧ u ≠ [] ∧ hd u = ev a ∧
               tl r setinterleaves ((tl t, tl u), range tick ∪ ev ` S)›
      using *(3, 4, 5) inside assms(1, 2)[simplified BOT_iff_Nil_D]
      by (cases t; cases u) (auto simp add: image_iff split: if_split_asm)
    have ‹(tF  (tl r) ∨ v = []) ∧ s = tl r @ v ∧
          (tl t ∈ 𝒟 (P after a) ∧ tl u ∈ 𝒯 (Q after a) ∨ 
           tl t ∈ 𝒟 (Q after a) ∧ tl u ∈ 𝒯 (P after a))›
      using "*"(2, 3, 5) "**" apply (simp add: D_After initial_hyps T_After)
      by (metis list.collapse list.sel(3) tickFree_tl tl_append2)
    with "*"(1) "**" have ‹s ∈ 𝒟 (P after a ⟦S⟧ Q after a)› by (simp add: D_Sync) blast
  } note * = this

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a) ⟹ s ∈ 𝒟 (P after a ⟦S⟧ Q after a)› for s
    by (simp add: "*" D_After initials_Sync initial_hyps image_iff split: if_split_asm)
      (metis After_BOT BOT_Sync BOT_iff_Nil_D D_BOT Sync_BOT front_tickFree_Cons_iff mem_Collect_eq)
next

  fix s
  { assume ‹s ∈ 𝒟 (P after a ⟦S⟧ Q after a)›
    from this obtain t u r v
      where * : ‹ftF v› ‹tF  r ∨ v = []› ‹s = r @ v›
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)› 
        ‹ev a # t ∈ 𝒟 P ∧ ev a # u ∈ 𝒯 Q ∨ ev a # t ∈ 𝒟 Q ∧ ev a # u ∈ 𝒯 P› 
      by (simp add: D_Sync After_projs initial_hyps) blast
    have ** : ‹(ev a # r) setinterleaves ((ev a # t, ev a # u), range tick ∪ ev ` S)›
      by (simp add: inside "*"(4))
    have ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
      by (simp add: D_Sync inside)
        (metis "*"(1, 2, 3, 5) "**" Cons_eq_appendI eventptick.disc(1) tickFree_Cons_iff)
  }
  thus ‹s ∈ 𝒟 (P after a ⟦S⟧ Q after a) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after a)›
    by (simp add: D_After initials_Sync initial_hyps After_BOT D_BOT inside)
qed



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

lemma initialL_initialR_not_in_After_Sync: 
  ‹(P ⟦S⟧ Q) after a = (P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)›
  if initial_hyps: ‹ev a ∈ P0› ‹ev a ∈ Q0› and notin: ‹a ∉ S› for P Q :: ‹('a, 'r) processptick›
proof (subst Process_eq_spec_optimized, safe)

  { fix P Q :: ‹('a, 'r) processptick› and 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) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
      ‹s_P ≠ []› ‹hd s_P = ev a›
      ‹s setinterleaves ((tl s_P, s_Q), range tick ∪ ev ` S)›
      ‹ev a ∈ P0›
    from assms(1, 4, 5, 7) have ‹(tl s_P, X_P) ∈ ℱ (P after a)›
      by (simp add: F_After) (metis list.exhaust_sel)
    with assms(2, 3, 6) have ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)›
      by (simp add: F_Sync) blast
  } note * = this

  { fix s X
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
      and same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))›
    from assms(3) consider
      ‹∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                          (ev a # s) setinterleaves ((s_P, s_Q), range tick ∪ ev ` S) ∧ 
                          X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› |
      ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a)›
      by (simp add: F_Sync D_After D_Sync initials_Sync assms(1, 2) initial_hyps image_iff) blast
    hence ‹(s, X) ∈ ℱ ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))›
    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 a # s) setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q› by blast
      have ‹s_P ≠ [] ∧ hd s_P = ev a ∧ s setinterleaves ((tl s_P, s_Q), range tick ∪ ev ` S) ∨
            s_Q ≠ [] ∧ hd s_Q = ev a ∧ s setinterleaves ((s_P, tl s_Q), range tick ∪ 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 a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))›
        apply (elim disjE; simp add: F_Ndet)
        using "*" "**"(1, 2, 4) initial_hyps(1) apply blast
        apply (rule disjI2, subst Sync_commute, rule *[OF **(2, 1)])
        by (simp_all add: "**"(4) Int_commute Un_commute Sync_commute
            setinterleaving_sym initial_hyps(2))
    next
      assume ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a)›
      from this[simplified same_div] D_F
      show ‹(s, X) ∈ ℱ ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))› by blast
    qed
  } note ** = this

  show ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)) ⟹
        (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a) ⟹ (s, X) ∈ ℱ ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))› for s X
    by (simp add: "**" F_After initials_Sync initial_hyps image_iff split: if_split_asm)
      (metis After_BOT BOT_Sync BOT_iff_Nil_D D_BOT F_imp_front_tickFree Sync_commute
        front_tickFree_Cons_iff is_processT8 mem_Collect_eq)
next

  { fix s X P Q
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹(s, X) ∈ ℱ (P after a ⟦S⟧ Q)› ‹ev a ∈ P0›
      and same_div : ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))›
    from assms(3)[simplified F_Sync, simplified] consider
      s_P s_Q X_P X_Q where ‹(ev a # s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
      ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
      ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
    | ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
      by (simp add: F_Sync F_After assms(4) D_Sync) blast
    hence ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
    proof cases
      fix s_P s_Q X_P X_Q
      assume * : ‹(ev a # s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
        ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` S)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` S) ∪ X_P ∩ X_Q›
      have ‹(ev a # s) setinterleaves ((ev a # s_P, s_Q), range tick ∪ ev ` S)›
        using "*"(3) by (cases s_Q; simp add: notin image_iff)
      with "*"(1, 2, 4) show ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)›
        by (simp add: F_Sync) blast
    next
      assume ‹s ∈ 𝒟 (P after a ⟦S⟧ Q)›
      hence ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a)› using same_div[simplified D_Ndet] by fast
      hence ‹(s, X) ∈ ℱ ((P ⟦S⟧ Q) after a)› by (simp add: is_processT8)
      thus ‹(ev a # s, X) ∈ ℱ (P ⟦S⟧ Q)› 
        by (simp add: F_After initials_Sync assms(1, 2, 4) notin image_iff)
    qed
  } note * = this

  show ‹𝒟 ((P ⟦S⟧ Q) after a) = 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)) ⟹
        (s, X) ∈ ℱ ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)) ⟹ (s, X) ∈ ℱ ((P ⟦S⟧ Q) after a)› for s X
    apply (simp add: F_After initials_Sync initial_hyps F_BOT image_iff
        F_imp_front_tickFree front_tickFree_Cons_iff)
    apply (rule impI, simp add: F_Ndet, elim disjE conjE)
    by (simp add: "*" initial_hyps(1))
      (metis "*" Ndet_commute Sync_commute initial_hyps(2))
next

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

  show ‹s ∈ 𝒟 ((P ⟦S⟧ Q) after a) ⟹ s ∈ 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a))› for s
    by (simp add: "*" D_After initials_Sync initial_hyps image_iff split: if_split_asm)
      (metis D_BOT Ndet_is_BOT_iff Sync_is_BOT_iff
        front_tickFree_Cons_iff front_tickFree_Nil mem_Collect_eq)
next

  { fix s P Q
    assume assms : ‹P ≠ ⊥› ‹Q ≠ ⊥› ‹s ∈ 𝒟 ((P after a ⟦S⟧ Q))› ‹ev a ∈ P0›
    from assms(3)[simplified D_Sync, simplified] obtain t u r v
      where * : ‹ftF v› ‹tF  r ∨ v = []› ‹s = r @ v› 
        ‹r setinterleaves ((t, u), range tick ∪ ev ` S)›
        ‹ev a # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ ev a # u ∈ 𝒯 P›
      by (simp add: D_Sync After_projs assms(4)) blast
    from "*"(5) have ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
    proof (elim disjE)
      assume ** : ‹ev a # t ∈ 𝒟 P ∧ u ∈ 𝒯 Q›
      have *** : ‹(ev a # r) setinterleaves ((ev a # t, u), range tick ∪ ev ` S)›
        using "*"(4) by (cases u; simp add: notin image_iff "*"(1, 2, 3))
      show ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync)
          (metis "*"(1, 2, 3) "**" "***" append_Cons eventptick.disc(1) tickFree_Cons_iff)
    next
      assume ** : ‹t ∈ 𝒟 Q ∧ ev a # u ∈ 𝒯 P›
      have *** : ‹(ev a # r) setinterleaves ((t, ev a # u), range tick ∪ ev ` S)›
        using "*"(4) by (cases t; simp add: notin image_iff "*"(1, 2, 3))
      show ‹ev a # s ∈ 𝒟 (P ⟦S⟧ Q)›
        by (simp add: D_Sync)
          (metis "*"(1, 2, 3) "**" "***" append_Cons eventptick.disc(1) tickFree_Cons_iff)
    qed
  } note * = this 

  show ‹s ∈ 𝒟 ((P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)) ⟹ s ∈ 𝒟 ((P ⟦S⟧ Q) after a)› for s
    by (simp add: D_After initials_Sync D_BOT image_iff notin)
      (metis "*" D_Ndet D_imp_front_tickFree Sync_commute
        UnE eventptick.disc(1) front_tickFree_Cons_iff initial_hyps)

qed


lemma not_initialL_not_initialR_After_Sync: ‹(P ⟦S⟧ Q) after a = Ψ (P ⟦S⟧ Q) a› 
  if initial_hyps: ‹ev a ∉ P0› ‹ev a ∉ Q0›
  apply (subst not_initial_After, simp add: initials_Sync)
  using initials_BOT initial_hyps by auto


text ‹Finally, the monster theorem !›

theorem After_Sync: 
  ‹(P ⟦S⟧ Q) after a =
   (  if P = ⊥ ∨ Q = ⊥ then ⊥
    else   if ev a ∈ P0 ∩ Q0
         then   if a ∈ S then P after a ⟦S⟧ Q after a
              else (P after a ⟦S⟧ Q) ⊓ (P ⟦S⟧ Q after a)
         else   if ev a ∈ P0 ∧ a ∉ S then P after a ⟦S⟧ Q
              else   if ev a ∈ Q0 ∧ a ∉ S then P ⟦S⟧ Q after a
                   else Ψ (P ⟦S⟧ Q) a)›
  by (simp add: After_BOT initialL_initialR_in_After_Sync initialL_initialR_not_in_After_Sync)
    (metis initialL_not_initialR_not_in_After_Sync Sync_commute
      not_initialL_in_After_Sync not_initialL_not_initialR_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_initial_inside:
  ‹a ∈ A ⟹ P \ A ⊑FD P after a \ A›
  and After_Hiding_FD_Hiding_After_if_initial_notin:
  ‹a ∉ A ⟹ (P \ A) after a ⊑FD P after a \ A›
  if initial: ‹ev a ∈ P0›
   supply initial' = initial_notin_imp_initial_Hiding[OF initial]
proof -
  { fix s
    assume ‹s ∈ 𝒟 (P after a \ A)›
    with D_Hiding obtain t u 
      where * : ‹ftF u› ‹tF t› ‹s = trace_hide t (ev ` A) @ u› 
        ‹t ∈ 𝒟 (P after a) ∨ (∃ f. isInfHiddenRun f (P after a) A ∧ t ∈ range f)› 
      by blast
    from "*"(4) have ‹s ∈ (if a ∈ A then 𝒟 (P \ A) else 𝒟 ((P \ A) after a))›
    proof (elim disjE)
      assume ‹t ∈ 𝒟 (P after a)›
      hence ** : ‹ev a # t ∈ 𝒟 P› by (simp add: D_After initial)
      show  ‹s ∈ (if a ∈ A then 𝒟 (P \ A) else 𝒟 ((P \ A) after a))›
      proof (split if_split, intro conjI impI)
        assume ‹a ∈ A›
        with "*"(3) have *** : ‹s = trace_hide (ev a # t) (ev ` A) @ u› by simp
        show ‹s ∈ 𝒟 (P \ A)›
          by (simp add: D_Hiding)
            (metis "*"(1, 2) "**" "***" eventptick.disc(1) tickFree_Cons_iff)
      next
        assume ‹a ∉ A›
        with "*"(3) have *** : ‹ev a # s = trace_hide (ev a # t) (ev ` A) @ u›
          by (simp add: image_iff)
        have ‹ev a # s ∈ 𝒟 (P \ A)›
          by (simp add: D_Hiding)
            (metis "*"(1, 2) "**" "***" eventptick.disc(1) tickFree_Cons_iff)
        thus ‹s ∈ 𝒟 ((P \ A) after a)› by (simp add: D_After initial' ‹a ∉ A›)
      qed
    next
      assume ‹∃f. isInfHiddenRun f (P after a) A ∧ t ∈ range f›
      then obtain f where ‹isInfHiddenRun f (P after a) A› ‹t ∈ range f› by blast
      hence ** : ‹isInfHiddenRun (λi. ev a # f i) P A ∧
                  ev a # t ∈ range (λi. ev a # f i)›
        by (simp add: monotone_on_def T_After initial) blast
      show ‹s ∈ (if a ∈ A then 𝒟 (P \ A) else 𝒟 ((P \ A) after a))›
      proof (split if_split, intro conjI impI)
        assume ‹a ∈ A›
        with "*"(3) have *** : ‹s = trace_hide (ev a # t) (ev ` A) @ u› by simp
        show ‹s ∈ 𝒟 (P \ A)›
          by (simp add: D_Hiding)
            (metis "*"(1, 2) "**" "***" eventptick.disc(1) tickFree_Cons_iff)
      next
        assume ‹a ∉ A›
        with "*"(3) have *** : ‹ev a # s = trace_hide (ev a # t) (ev ` A) @ u›
          by (simp add: image_iff)
        have ‹ev a # s ∈ 𝒟 (P \ A)›
          by (simp add: D_Hiding)
            (metis "*"(1, 2) "**" "***" eventptick.disc(1) tickFree_Cons_iff)
        thus ‹s ∈ 𝒟 ((P \ A) after a)› by (simp add: D_After initial' ‹a ∉ A›)
      qed
    qed
  } note div_ref = this

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

  show ‹a ∈ A ⟹ P \ A ⊑FD P after a \ A›
    and ‹a ∉ A ⟹ (P \ A) after a ⊑FD P after a \ A›
    unfolding failure_divergence_refine_def failure_refine_def divergence_refine_def
    using div_ref fail_ref by auto
qed


lemmas Hiding_F_Hiding_After_if_initial_inside = 
  Hiding_FD_Hiding_After_if_initial_inside[THEN leFD_imp_leF]
  and After_Hiding_F_Hiding_After_if_initial_notin = 
  After_Hiding_FD_Hiding_After_if_initial_notin[THEN leFD_imp_leF]
  and Hiding_D_Hiding_After_if_initial_inside = 
  Hiding_FD_Hiding_After_if_initial_inside[THEN leFD_imp_leD]
  and After_Hiding_D_Hiding_After_if_initial_notin = 
  After_Hiding_FD_Hiding_After_if_initial_notin[THEN leFD_imp_leD]
  and Hiding_T_Hiding_After_if_initial_inside = 
  Hiding_FD_Hiding_After_if_initial_inside[THEN leFD_imp_leF, THEN leF_imp_leT]   
  and After_Hiding_T_Hiding_After_if_initial_notin = 
  After_Hiding_FD_Hiding_After_if_initial_notin[THEN leFD_imp_leF, THEN leF_imp_leT]

corollary Hiding_DT_Hiding_After_if_initial_inside:
  ‹ev a ∈ P0 ⟹ a ∈ A ⟹ P \ A ⊑DT P after a \ A›
  and After_Hiding_DT_Hiding_After_if_initial_notin: 
  ‹ev a ∈ P0 ⟹ a ∉ A ⟹ (P \ A) after a ⊑DT P after a \ A›
  by (simp add: Hiding_D_Hiding_After_if_initial_inside 
      Hiding_T_Hiding_After_if_initial_inside leD_leT_imp_leDT)
    (simp add: After_Hiding_D_Hiding_After_if_initial_notin 
      After_Hiding_T_Hiding_After_if_initial_notin leD_leT_imp_leDT)

end

(* 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 ∈ P0 ∧ f ∈ B ∧ P \ B ≠ P after f \ B›
          and ‹ev e ∈ P0 ∧ e ∉ B ∧ (P \ B) after e ≠ P after e \ B› 
  unfolding e_def f_def P_def B_def
  apply (simp_all add: initials_Ndet initials_write0)
  apply (simp_all add: After_Ndet initials_write0 After_write0 Hiding_set_SKIP)
  apply (simp_all add: Hiding_Ndet After_Ndet initials_write0 After_write0 Hiding_set_SKIP 
                       Hiding_set_STOP no_Hiding_write0 Hiding_write0)
  by (metis After_write0 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 ‹Renaming is tricky›

text ‹In all generality, const‹Renaming› takes a process
      @{term [show_types, source] ‹P :: ('a, 'r) processptick›}, a function
      @{term [show_types, source ] ‹f :: 'a ⇒ 'b›}, a function
      @{term [show_types, source ] ‹g :: 'r ⇒ 's›}, and returns 
      @{term [show_types, source] ‹Renaming P f g :: ('b, 's) processptick›}.
      But if we try to write and prove a lemma ‹After_Renaming› like we did for
      the other operators, the mechanism of the locale locale‹After› would
      constrain @{term [show_types, source] ‹f :: 'a ⇒ 'a›} and
      @{term [show_types, source] ‹g :: 'r ⇒ 'r›}.›

text ‹We solve this issue with a trick: we duplicate the locale,
      instantiating each one with a different free type.›

locale AfterDuplicated = Afterα : After Ψα + Afterβ : After Ψβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick› 
    and Ψβ :: ‹[('b, 's) processptick, 'b] ⇒ ('b, 's) processptick›
begin

notation Afterα.After (infixl ‹afterα› 86)
notation Afterβ.After (infixl ‹afterβ› 86)

lemma After_Renaming:
  ‹Renaming P f g afterβ b =
  ―‹We highlight the fact that @{term [show_types, source] ‹f :: 'a ⇒ 'b›}›
   (  if P = ⊥ then ⊥
    else   if ∃a. ev a ∈ P0 ∧ f a = b
         then ⊓ a∈{a. ev a ∈ P0 ∧ f a = b}. Renaming (P afterα a) f g
         else Ψβ (Renaming P f g) b)›
  (is ‹?lhs = (if P = ⊥ then ⊥
                else if ∃a. ev a ∈ P0 ∧ f a = b then ?rhs else _)›)

proof (split if_split, intro conjI impI)
  show ‹P = ⊥ ⟹ ?lhs= ⊥› by (simp add: Afterβ.After_BOT)
next
  assume non_BOT: ‹P ≠ ⊥›
  show ‹?lhs = (if ∃a. ev a ∈ P0 ∧ f a = b then ?rhs else Ψβ (Renaming P f g) b)›
  proof (split if_split, intro conjI impI)
    show ‹∄a. ev a ∈ P0 ∧ f a = b ⟹ ?lhs = Ψβ (Renaming P f g) b›
      by (subst Afterβ.not_initial_After)
        (auto simp add: initials_Renaming non_BOT image_iff ev_eq_map_eventptick_iff)
  next
    assume assm : ‹∃a. ev a ∈ P0 ∧ f a = b›
    hence initial: ‹ev b ∈ (Renaming P f g)0›
      by (auto simp add: initials_Renaming image_iff ev_eq_map_eventptick_iff)
    show ‹?lhs = ?rhs›
    proof (subst Process_eq_spec_optimized, safe)
      fix s
      assume ‹s ∈ 𝒟 ?lhs›
      hence * : ‹ev b # s ∈ 𝒟 (Renaming P f g)›
        by (auto simp add: initial Afterβ.D_After split: if_split_asm)
      from "*" obtain t1 t2
        where ** : ‹tF t1› ‹ftF t2›
          ‹ev b # s = map (map_eventptick f g) 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 = b›
        by (cases t1) (auto simp add: BOT_iff_Nil_D ev_eq_map_eventptick_iff)
      have ‹ev a ∈ P0›
        using "**"(4) "***"(1) initials_memI D_T by blast
      also have ‹s ∈ 𝒟 (Renaming (P afterα a) f g)›
        using "**" "***"(1) by (simp add: D_Renaming Afterα.D_After calculation) blast
      ultimately show ‹s ∈ 𝒟 ?rhs›
        using "***"(2) by (simp add: D_GlobalNdet) blast
    next
      fix s
      assume ‹s ∈ 𝒟 ?rhs›
      then obtain a where * : ‹ev a ∈ P0› ‹f a = b›
        ‹s ∈ 𝒟 (Renaming (P afterα a) f g)›
        by (simp add: D_GlobalNdet split: if_split_asm) blast
      from "*"(3) obtain s1 s2 
        where ** : ‹tF s1› ‹ftF s2›
          ‹s = map (map_eventptick f g) s1 @ s2› ‹ev a # s1 ∈ 𝒟 P›
        by (simp add: D_Renaming Afterα.D_After "*"(1)) blast
      have *** : ‹tF (ev a # s1) ∧ ev b # s = map (map_eventptick f g) (ev a # s1) @ s2›
        by (simp add: "**"(1, 3) "*"(2))
      from "**"(2, 4)  show ‹s ∈ 𝒟 ?lhs›
        by (simp add: Afterβ.D_After initial D_Renaming) (use "***" in blast)
    next
      fix s X
      assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
      assume ‹(s, X) ∈ ℱ ?lhs›
      then consider ‹ev b ∉ (Renaming P f g)0› ‹s = []›
        | ‹ev b ∈ (Renaming P f g)0› ‹(ev b # s, X) ∈ ℱ (Renaming P f g)›
        by (simp add: initial Afterβ.F_After split: if_split_asm) 
      thus ‹(s, X) ∈ ℱ ?rhs›
      proof cases
        from initial show ‹ev b ∉ (Renaming P f g)0 ⟹ (s, X) ∈ ℱ ?rhs› by simp
      next
        assume assms : ‹ev b ∈ (Renaming P f g)0›
          ‹(ev b # s, X) ∈ ℱ (Renaming P f g)›
        from assms(2) consider ‹ev b # s ∈ 𝒟 (Renaming P f g)›
          | s1 where ‹(s1, map_eventptick f g -` X) ∈ ℱ P› ‹ev b # s = map (map_eventptick f g) s1›
          by (simp add: F_Renaming D_Renaming) meson
        thus ‹(s, X) ∈ ℱ ?rhs›
        proof cases
          assume ‹ev b # s ∈ 𝒟 (Renaming P f g)›
          hence ‹s ∈ 𝒟 ?lhs› by (force simp add: Afterβ.D_After assms(1))
          with D_F same_div show ‹(s, X) ∈ ℱ ?rhs› by blast
        next
          fix s1 assume * : ‹(s1, map_eventptick f g -` X) ∈ ℱ P›
            ‹ev b # s = map (map_eventptick f g) s1›
          from "*"(2) obtain a s1'
            where ** : ‹s1 = ev a # s1'› ‹f a = b›
            by (cases s1; simp) (metis map_eventptick_eq_ev_iff)
          have ‹ev a ∈ P0›
            using "*"(1) "**"(1) initials_memI F_T by blast
          also have ‹(s, X) ∈ ℱ (Renaming (P afterα a) f g)›
            using "*"(1, 2) "**"(1) by (simp add: F_Renaming Afterα.F_After calculation) blast
          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 ∈ P0 ⟶ f a ≠ b› ‹s = []›
        | a where ‹f a = b› ‹ev a ∈ P0› ‹(s, X) ∈ ℱ (Renaming (P afterα a) f g)›
        by (auto simp add: F_GlobalNdet split: if_split_asm)
      thus ‹(s, X) ∈ ℱ ?lhs›
      proof cases
        from assm show ‹∀a. ev a ∈ P0 ⟶ f a ≠ b ⟹ s = [] ⟹ (s, X) ∈ ℱ ?lhs›
          by (auto simp add: Afterβ.F_After F_Renaming initials_Renaming non_BOT)
      next
        fix a assume * : ‹f a = b› ‹ev a ∈ P0› ‹(s, X) ∈ ℱ (Renaming (P afterα a) f g)›
        from "*"(3) consider ‹s ∈ 𝒟 (Renaming (P afterα a) f g)›
          | s1 where ‹(s1, map_eventptick f g -` X) ∈ ℱ (P afterα a)› ‹s = map (map_eventptick f g) s1›
          by (simp add: F_Renaming D_Renaming) blast
        thus ‹(s, X) ∈ ℱ ?lhs›
        proof cases
          assume ‹s ∈ 𝒟 (Renaming (P afterα a) f g)›
          with "*"(1, 2) have ‹s ∈ 𝒟 ?rhs› by (simp add: D_GlobalNdet) blast
          with D_F same_div show ‹(s, X) ∈ ℱ ?lhs› by blast
        next
          fix s1 assume ** : ‹(s1, map_eventptick f g -` X) ∈ ℱ (P afterα a)›
            ‹s = map (map_eventptick f g) s1›
          from initial "*"(1, 2) "**"
          have ‹(ev a # s1, map_eventptick f g -` X) ∈ ℱ P ∧ ev b # s = map (map_eventptick f g) (ev a # s1)›
            by (simp add: Afterα.F_After "*"(2))
          hence ‹(ev b # s, X) ∈ ℱ (Renaming P f g)›
            by (auto simp add: F_Renaming)
          thus ‹(s, X) ∈ ℱ ?lhs›
            by (simp add: Afterβ.F_After initial)
        qed
      qed
    qed
  qed
qed

no_notation Afterα.After (infixl ‹afterα› 86)
no_notation Afterβ.After (infixl ‹afterβ› 86)

end


text ‹Now we can get back to locale‹After›.›

context After
begin

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

lemma After_GlobalDet_is_After_GlobalNdet: 
  ‹ev a ∈ (⋃a ∈ A. (P a)0) ⟹ (□ a ∈ A. P a) after a = (⊓ a ∈ A. P a) after a›
  by (simp add: Process_eq_spec After_projs initials_GlobalDet
      initials_GlobalNdet GlobalNdet_projs GlobalDet_projs)


lemma After_GlobalNdet:
  ‹(⊓ a ∈ A. P a) after a =  (  if ev a ∈ (⋃a ∈ A. (P a)0)
                              then ⊓ x ∈ {x ∈ A. ev a ∈ (P x)0}. P x after a
                              else Ψ (⊓ a ∈ A. P a) a)›
  (is ‹?lhs = (if ?prem then ?rhs else _)›)
proof (split if_split, intro conjI impI)
  show ‹¬ ?prem ⟹ ?lhs = Ψ (⊓ a ∈ A. P a) a›
    by (simp add: not_initial_After initials_GlobalNdet)
next
  assume ?prem
  then obtain x where ‹x ∈ A› ‹ev a ∈ (P x)0› by blast
  show ‹?lhs = ?rhs›
  proof (subst Process_eq_spec, safe)
    from ‹x ∈ A› ‹ev a ∈ (P x)0› show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: D_After initials_GlobalNdet D_GlobalNdet
          split: if_split_asm intro: D_T initials_memI)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: D_GlobalNdet D_After initials_GlobalNdet)
  next
    from ‹x ∈ A› ‹ev a ∈ (P x)0› show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
      by (auto simp add: F_After initials_GlobalNdet F_GlobalNdet
          split: if_split_asm intro: F_T initials_memI)
  next
    from ‹x ∈ A› ‹ev a ∈ (P x)0› show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (auto simp add: F_GlobalNdet F_After initials_GlobalNdet split: if_split_asm)
  qed
qed


lemma After_GlobalDet:
  ‹(□ a ∈ A. P a) after a =  (  if ev a ∈ (⋃a ∈ A. (P a)0)
                              then ⊓ x ∈ {x ∈ A. ev a ∈ (P x)0}. P x after a
                              else Ψ (□ a ∈ A. P a) a)›
  by (simp add: After_GlobalDet_is_After_GlobalNdet After_GlobalNdet
      initials_GlobalDet not_initial_After)


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



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

lemma After_Throw: 
  ‹(P Θ a ∈ A. Q a) after a = 
   (  if P = ⊥ then ⊥
    else   if ev a ∈ P0 then   if a ∈ A then Q a
                                 else P after a Θ a ∈ A. Q a
         else Ψ (P Θ a ∈ A. Q a) a)›
  (is ‹?lhs = ?rhs›)
proof -
  have ‹?lhs = Q a› if ‹P ≠ ⊥› and ‹ev a ∈ P0› and ‹a ∈ A›
  proof (rule Process_eq_optimizedI)
    fix t
    assume ‹t ∈ 𝒟 ?lhs›
    with ‹ev a ∈ P0› have ‹ev a # t ∈ 𝒟 (P Θ a ∈ A. Q a)›
      by (simp add: D_After initials_Throw)
    with ‹P ≠ ⊥› show ‹t ∈ 𝒟 (Q a)›
      apply (simp add: D_Throw disjoint_iff BOT_iff_Nil_D, elim disjE)
      by (metis hd_append2 hd_in_set image_eqI list.sel(1) ‹a ∈ A›)
        (metis append_self_conv2 eventptick.inject(1) hd_append2
          hd_in_set image_eqI list.sel(1, 3) ‹a ∈ A›)
  next
    have ‹[ev a] ∈ 𝒯 P ∧ a ∈ A› using initials_def ‹ev a ∈ P0› ‹a ∈ A› by blast
    thus ‹t ∈ 𝒟 (Q a) ⟹ t ∈ 𝒟 ((P Θ a ∈ A. Q a) after a)› for t
      by (simp add: D_After initials_Throw ‹ev a ∈ P0› D_Throw)
        (metis append_Nil empty_set inf_bot_left)
  next
    fix t X
    assume ‹(t, X) ∈ ℱ ?lhs›
    with ‹ev a ∈ P0› have ‹(ev a # t, X) ∈ ℱ (P Θ a ∈ A. Q a)›
      by (simp add: F_After initials_Throw)
    with ‹P ≠ ⊥› ‹a ∈ A› show ‹(t, X) ∈ ℱ (Q a)›
      apply (simp add: F_Throw image_iff BOT_iff_Nil_D, elim disjE)
      by (metis disjoint_iff hd_append2 hd_in_set image_eqI list.sel(1))
        (metis append_Nil eventptick.inject(1) hd_append2 imageI insert_disjoint(2) 
          list.exhaust_sel list.sel(1, 3) list.simps(15))
  next
    have ‹[ev a] ∈ 𝒯 P ∧ a ∈ A› using initials_def ‹ev a ∈ P0› ‹a ∈ A› by blast
    thus ‹(t, X) ∈ ℱ (Q a) ⟹ (t, X) ∈ ℱ ?lhs› for t X
      by (simp add: F_After initials_Throw ‹ev a ∈ P0› F_Throw)
        (metis append_Nil empty_set inf_bot_left)
  qed

  also have ‹?lhs = (P after a) Θ a ∈ A. Q a›
    if ‹P ≠ ⊥› and ‹ev a ∈ P0› and ‹a ∉ A›
  proof (rule Process_eq_optimizedI)
    fix t
    assume ‹t ∈ 𝒟 ?lhs›
    with ‹ev a ∈ P0› have ‹ev a # t ∈ 𝒟 (P Θ a ∈ A. Q a)›
      by (simp add: D_After initials_Throw)
    then consider (divL) t1 t2 where ‹ev a # t = t1 @ t2› ‹t1 ∈ 𝒟 P› ‹tF t1›
      ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | (divR) t1 t2 a' where ‹ev a # t = t1 @ ev a' # t2› ‹t1 @ [ev a'] ∈ 𝒯 P›
      ‹set t1 ∩ ev ` A = {}› ‹a' ∈ A› ‹t2 ∈ 𝒟 (Q a')›
      by (simp add: D_Throw) blast
    thus ‹t ∈ 𝒟 ((P after a) Θ a ∈ A. Q a)›
    proof cases
      case divL
      from ‹P ≠ ⊥› divL(1, 2) BOT_iff_Nil_D obtain t1'
        where ‹t1 = ev a # t1'› by (cases t1) auto
      with divL(1-4) have ‹t = t1' @ t2 ∧ t1' ∈ 𝒟 (P after a) ∧
                           tF t1' ∧ set t1' ∩ ev ` A = {}›
        by (simp add: D_After ‹ev a ∈ P0›)
      with divL(5) show ‹t ∈ 𝒟 ((P after a) Θ a ∈ A. Q a)›
        by (auto simp add: D_Throw) 
    next
      case divR
      have ‹a ≠ a'› using divR(4) ‹a ∉ A› by blast
      with divR(1) obtain t1' where ** : ‹t1 = ev a # t1'› by (cases t1) auto
      with divR(2) ‹ev a ∈ P0› have ‹t1' @ [ev a'] ∈ 𝒯 (P after a)›
        by (simp add: T_After)
      with divR(1, 3-5) "**" show ‹t ∈ 𝒟 ((P after a) Θ a ∈ A. Q a)›
        by (simp add: D_Throw) blast
    qed
  next
    fix t
    assume ‹t ∈ 𝒟 ((P after a) Θ a ∈ A. Q a)›
    then consider (divL) t1 t2 where ‹t = t1 @ t2› ‹t1 ∈ 𝒟 (P after a)›
      ‹tF t1› ‹set t1 ∩ ev ` A = {}› ‹ftF t2›
    | (divR) t1 a' t2 where ‹t = t1 @ ev a' # t2› ‹t1 @ [ev a'] ∈ 𝒯 (P after a)›
      ‹set t1 ∩ ev ` A = {}› ‹a' ∈ A› ‹t2 ∈ 𝒟 (Q a')›
      unfolding D_Throw by blast
    thus ‹t ∈ 𝒟 ?lhs›
    proof cases
      case divL
      from divL(2) ‹ev a ∈ P0› have ** : ‹ev a # t1 ∈ 𝒟 P› by (simp add: D_After)
      have *** : ‹tF (ev a # t1) ∧ set (ev a # t1) ∩ ev ` A = {}›
        by (simp add: image_iff divL(3, 4) ‹a ∉ A›)
      show ‹t ∈ 𝒟 ?lhs›
        by (simp add: D_After D_Throw initials_Throw ‹ev a ∈ P0›)
          (metis divL(1, 5) "**" "***" Cons_eq_appendI)
    next
      case divR
      from divR(2) ‹ev a ∈ P0› have ** : ‹ev a # t1 @ [ev a'] ∈ 𝒯 P›
        by (simp add: T_After)
      have *** : ‹set (ev a # t1) ∩ ev ` A = {}›
        by (simp add: image_iff divR(3) ‹a ∉ A›)
      show ‹t ∈ 𝒟 ?lhs›
        by (simp add: D_After D_Throw initials_Throw ‹ev a ∈ P0›) 
          (metis divR(1, 4, 5) "**" "***" Cons_eq_appendI)
    qed
  next
    fix t X assume ‹t ∉ 𝒟 ?lhs›
    assume ‹(t, X) ∈ ℱ ?lhs›
    with ‹ev a ∈ P0› have ‹(ev a # t, X) ∈ ℱ (P Θ a ∈ A. Q a)›
      by (simp add: F_After initials_Throw)
    with ‹t ∉ 𝒟 ?lhs› ‹(t, X) ∈ ℱ ?lhs› consider ‹(ev a # t, X) ∈ ℱ P› ‹set t ∩ ev ` A = {}›
      | (failR) t1 a' t2 where ‹ev a # t = t1 @ ev a' # t2› ‹t1 @ [ev a'] ∈ 𝒯 P›
        ‹set t1 ∩ ev ` A = {}› ‹a' ∈ A› ‹(t2, X) ∈ ℱ (Q a')›
      by (auto simp add: D_After Throw_projs initials_Throw split: if_split_asm)
        (metis D_T initials_memI is_processT7)
    thus ‹(t, X) ∈ ℱ (P after a Θ a∈A. Q a)›
    proof cases
      show ‹(ev a # t, X) ∈ ℱ P ⟹ set t ∩ ev ` A = {} ⟹
            (t, X) ∈ ℱ (P after a Θ a∈A. Q a)›
        by (simp add: F_Throw F_After ‹ev a ∈ P0›)
    next
      case failR
      have ‹a ≠ a'› using failR(4) ‹a ∉ A› by blast
      with failR(1) obtain t1' where ‹t1 = ev a # t1'› by (cases t1) auto
      also have ‹t1' @ [ev a'] ∈ 𝒯 (P after a) ∧ set t1' ∩ ev ` A = {}›
        using failR(2, 3) by (simp add: image_iff T_After ‹ev a ∈ P0› calculation)
      ultimately show ‹(t, X) ∈ ℱ (P after a Θ a ∈ A. Q a)›
        using failR(1, 4, 5) by (simp add: F_Throw) blast
    qed
  next
    fix t X
    assume ‹t ∉ 𝒟 (P after a Θ a∈A. Q a)› and ‹(t, X) ∈ ℱ (P after a Θ a∈A. Q a)›
    then consider (failL) ‹(t, X) ∈ ℱ (P after a)› ‹set t ∩ ev ` A = {}›
      | (failR) t1 a' t2 where ‹t = t1 @ ev a' # t2› ‹t1 @ [ev a'] ∈ 𝒯 (P after a)›
        ‹set t1 ∩ ev ` A = {}› ‹a' ∈ A› ‹(t2, X) ∈ ℱ (Q a')›
      by (auto simp add: Throw_projs D_After ‹ev a ∈ P0›) 
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      case failL
      from failL(2) have * : ‹set (ev a # t) ∩ ev ` A = {}›
        by (simp add: image_iff ‹a ∉ A› failL(2))
      from failL(1) have ‹(ev a # t, X) ∈ ℱ P›
        by (simp add: F_After ‹ev a ∈ P0›)
      with "*" show  ‹(t, X) ∈ ℱ ?lhs›
        by (simp add: F_After F_Throw initials_Throw ‹ev a ∈ P0›)
    next
      case failR
      from failR(2) ‹ev a ∈ P0› have ** : ‹ev a # t1 @ [ev a'] ∈ 𝒯 P›
        by (simp add: T_After)
      have *** : ‹set (ev a # t1) ∩ ev ` A = {}›
        by (simp add: image_iff failR(3) ‹a ∉ A›)
      from failR(1, 4, 5) show ‹(t, X) ∈ ℱ ?lhs›
        by (simp add: F_After F_Throw initials_Throw ‹ev a ∈ P0›) 
          (metis  "**" "***" append_Cons)
    qed
  qed

  ultimately show ‹?lhs = ?rhs›
    by (simp add: After_BOT not_initial_After initials_Throw)
qed



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

theorem After_Interrupt: 
  ‹(P △ Q) after a =
   (   if ev a ∈ P0 ∩ Q0 
     then Q after a ⊓ (P after a △ Q)
     else    if ev a ∈ P0 ∧ ev a ∉ Q0
           then P after a △ Q 
           else   if ev a ∉ P0 ∧ ev a ∈ Q0
                then Q after a
                else Ψ (P △ Q) a)›
proof -
  have ‹(P △ Q) after a ⊑FD Q after a› if initial: ‹ev a ∈ Q0›
  proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
    fix t
    assume ‹t ∈ 𝒟 (Q after a)›
    hence ‹ev a # t ∈ 𝒟 Q›
      by (simp add: D_After initial)
    thus ‹t ∈ 𝒟 ((P △ Q) after a)›
      by (simp add: D_After initial initials_Interrupt D_Interrupt)
        (metis Nil_elem_T append_Nil tickFree_Nil)
  next
    show ‹(t, X) ∈ ℱ (Q after a) ⟹ (t, X) ∈ ℱ ((P △ Q) after a)› for t X
      by (simp add: F_After initials_Interrupt F_Interrupt initial)
        (metis Nil_elem_T append_Nil list.distinct(1) tickFree_Nil)
  qed

  moreover have ‹(P △ Q) after a ⊑FD P after a △ Q› if initial: ‹ev a ∈ P0›
  proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
    show ‹t ∈ 𝒟 (P after a △ Q) ⟹ t ∈ 𝒟 ((P △ Q) after a)› for t
      by (simp add: D_Interrupt D_After initial T_After initials_Interrupt)
        (metis append_Cons eventptick.disc(1) tickFree_Cons_iff)
  next
    show ‹(t, X) ∈ ℱ (P after a △ Q) ⟹ (t, X) ∈ ℱ ((P △ Q) after a)› for t X
      by (simp add: F_Interrupt F_After initial initials_Interrupt T_After D_After, elim disjE)
        (metis [[metis_verbose = false]] Cons_eq_appendI eventptick.disc(1) tickFree_Cons_iff)+ 
  qed

  moreover have ‹Q after a ⊑FD (P △ Q) after a›
    if initial_hyps: ‹ev a ∉ P0› ‹ev a ∈ Q0›
  proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
    show ‹t ∈ 𝒟 ((P △ Q) after a) ⟹ t ∈ 𝒟 (Q after a)› for t
      by (simp add: D_After initials_Interrupt D_Interrupt initial_hyps)
        (metis initials_memI D_T append_Nil hd_append
          list.exhaust_sel list.sel(1) initial_hyps(1))
  next
    from initials_memI[of ‹ev a› _ P, simplified initial_hyps(1)]
    show ‹(t, X) ∈ ℱ ((P △ Q) after a) ⟹ (t, X) ∈ ℱ (Q after a)› for t X
      by (auto simp add: F_After initials_Interrupt F_Interrupt initial_hyps intro: F_T D_T)
        (metis, metis append_eq_Cons_conv, metis append_eq_Cons_conv is_processT8)
  qed

  moreover have ‹P after a △ Q ⊑FD (P △ Q) after a›
    if initial_hyps: ‹ev a ∈ P0› ‹ev a ∉ Q0›
  proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
    from initials_memI[of ‹ev a› _ Q, simplified initial_hyps(2)]
    show ‹t ∈ 𝒟 ((P △ Q) after a) ⟹ t ∈ 𝒟 (P after a △ Q)› for t
      by (simp add: After_projs initials_Interrupt initial_hyps D_Interrupt)
        (metis append_Nil hd_append2 list.exhaust_sel D_T
          list.sel(1, 3) tickFree_Cons_iff tl_append2)
  next
    fix t X
    assume ‹(t, X) ∈ ℱ ((P △ Q) after a)›
    with initial_hyps(1) have ‹(ev a # t, X) ∈ ℱ (P △ Q)›
      by (simp add: F_After initials_Interrupt)
    with initials_memI[of ‹ev a› _ Q, simplified initial_hyps(2)]
    show ‹(t, X) ∈ ℱ (P after a △ Q)›
      by (simp add: F_Interrupt After_projs initial_hyps(1), elim disjE)
        (metis (no_types, opaque_lifting) [[metis_verbose = false]]
          append_self_conv2 eventptick.simps(3) tl_append2 F_T list.exhaust_sel
          list.sel(1, 3) tickFree_Cons_iff D_T hd_append2)+
  qed

  moreover have ‹(Q after a) ⊓ (P after a △ Q) ⊑FD (P △ Q) after a›
    if both_initial: ‹ev a ∈ P0› ‹ev a ∈ Q0›
  proof (unfold failure_divergence_refine_def failure_refine_def divergence_refine_def, safe)
    fix t assume ‹t ∈ 𝒟 ((P △ Q) after a)›
    with both_initial(1) have ‹ev a # t ∈ 𝒟 (P △ Q)›
      by (simp add: D_After initials_Interrupt)
    thus ‹t ∈ 𝒟 ((Q after a) ⊓ (P after a △ Q))›
      by (simp add: D_Interrupt After_projs D_Ndet both_initial)
        (metis tickFree_tl append_Cons append_Nil list.exhaust_sel list.sel(1, 3))
  next
    fix t X assume ‹(t, X) ∈ ℱ ((P △ Q) after a)›
    with both_initial(1) have ‹(ev a # t, X) ∈ ℱ (P △ Q)›
      by (simp add: F_After initials_Interrupt)
    thus ‹(t, X) ∈ ℱ ((Q after a) ⊓ (P after a △ Q))›
      by (simp add: F_Interrupt F_Ndet After_projs both_initial, elim disjE)
        (metis (no_types, opaque_lifting) [[metis_verbose = false]] 
          eventptick.distinct(1) list.sel(1, 3) append_Nil hd_append2
          list.exhaust_sel process_charn tickFree_Cons_iff tl_append2)+
  qed

  ultimately show ?thesis
    by (auto simp add: not_initial_After initials_Interrupt
        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 a = (if a ∈ A then DF A else Ψ (DF A) a)›
  by (simp add: not_initial_After initials_DF image_iff)
    (subst DF_unfold, simp add: After_Mndetprefix)

lemma After_DFSKIPS:
  ‹DFSKIPS A R after a = (if a ∈ A then DFSKIPS A R else Ψ (DFSKIPS A R) a)›
  by (simp add: not_initial_After initials_DFSKIPS image_iff)
    (subst DFSKIPS_unfold,
      simp add: After_Ndet After_Mndetprefix initials_Mndetprefix image_iff)

lemma After_RUN:
  ‹RUN A after a = (if a ∈ A then RUN A else Ψ (RUN A) a)›
  by (simp add: not_initial_After initials_RUN image_iff)
    (subst RUN_unfold, subst After_Mprefix, simp)

lemma After_CHAOS:
  ‹CHAOS A after a = (if a ∈ A then CHAOS A else Ψ (CHAOS A) a)›
  by (simp add: not_initial_After initials_CHAOS image_iff)
    (subst CHAOS_unfold,
      simp add: After_Ndet initials_Mprefix After_Mprefix)

lemma After_CHAOSSKIPS: 
  ‹CHAOSSKIPS A R after a = (if a ∈ A then CHAOSSKIPS A R else Ψ (CHAOSSKIPS A R) a)›
  by (simp add: not_initial_After initials_CHAOSSKIPS image_iff)
    (subst CHAOSSKIPS_unfold,
      simp add: initials_Ndet initials_Mprefix After_Ndet After_Mprefix image_iff)



lemma DF_FD_After: ‹DF A ⊑FD P after a› if ‹ev a ∈ P0› and ‹DF A ⊑FD P›
proof -
  have ‹DF A after a ⊑FD P after a› by (rule mono_After_FD[OF that]) 
  also have ‹a ∈ A›
    using anti_mono_initials_FD[OF that(2), THEN set_mp, OF that(1)]
    by (simp add: initials_DF image_iff)
  ultimately show ‹DF A ⊑FD P after a› by (subst (asm) After_DF, simp split: if_split_asm)
qed


lemma DFSKIPS_FD_After: ‹DFSKIPS A R ⊑FD P after a› if ‹ev a ∈ P0› and ‹DFSKIPS A R ⊑FD P›
proof -
  have ‹DFSKIPS A R after a ⊑FD P after a› by (rule mono_After_FD[OF that]) 
  also have ‹a ∈ A›
    using anti_mono_initials_FD[OF that(2), THEN set_mp, OF that(1)]
    by (simp add: initials_DFSKIPS image_iff)
  ultimately show ‹DFSKIPS A R ⊑FD P after a› by (subst (asm) After_DFSKIPS, simp split: if_split_asm)
qed


text ‹We have corollaries on const‹deadlock_free› and const‹deadlock_freeSKIPS›.›

corollary deadlock_free_After:
  ‹deadlock_free P ⟹
   deadlock_free (P after a) ⟷
   (if ev a ∈ P0 then True else deadlock_free (Ψ P a))›
  by (simp add: not_initial_After deadlock_free_def)
    (intro impI DF_FD_After)

corollary deadlock_freeSKIPS_After:
  ‹deadlock_freeSKIPS P ⟹ 
   deadlock_freeSKIPS (P after a) ⟷
   (if ev a ∈ P0 then True else deadlock_freeSKIPS (Ψ P a))›
  by (simp add: not_initial_After deadlock_freeSKIPS_FD)
    (intro impI DFSKIPS_FD_After)



section ‹Continuity›

text ‹This is a new result whose main consequence will be the admissibility of the event
      transition that is defined later (property that paves the way for point-fixed induction)‹…››

text ‹Of course this result will require an additional assumption of continuity
      on the placeholder term‹Ψ›.›

context begin

(* TODO: do we want this accessible outside ? *)
private lemma mono_Ψ_imp_chain_After:
  ‹(⋀P Q. P ⊑ Q ⟹ Ψ P a ⊑ Ψ Q a) ⟹ chain Y ⟹ chain (λi. Y i after a)›
  by (simp add: mono_After chain_def)

private lemma cont_prem_After :
  ‹(⨆ i. Y i) after a = (⨆ i. Y i after a)› (is ‹?lhs = ?rhs›)
  if cont_Ψ: ‹cont (λP. Ψ P a)› and chain_Y : ‹chain Y›
proof -
  from chain_Y cont2monofunE cont_Ψ mono_Ψ_imp_chain_After
  have chain_After : ‹chain (λi. Y i after a)› by blast
  show ‹?lhs = ?rhs›
  proof (cases ‹ev a ∈ (⨆ i. Y i)0›)
    assume initial : ‹ev a ∈ (⨆ i. Y i)0›
    hence * : ‹∀i. ev a ∈ (Y i)0› by (simp add: initials_LUB chain_Y)
    show ‹?lhs = ?rhs›
    proof (rule Process_eq_optimizedI)
      show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
        by (simp add: D_After initial)
          (simp add: D_After "*" limproc_is_thelub chain_After chain_Y D_LUB)
    next
      fix t
      define S
        where ‹S i ≡ {u. t = u ∧ ev a # u ∈ 𝒟 (Y i)}› for i
      assume ‹t ∈ 𝒟 ?rhs›
      hence ‹t ∈ 𝒟 (Y i after a)› for i
        by (simp add: limproc_is_thelub D_LUB chain_After)
      hence ‹S i ≠ {}› for i by (simp add: S_def D_After "*")
      moreover have ‹finite (S 0)› unfolding S_def by (prove_finite_subset_of_prefixes t)
      moreover have ‹S (Suc i) ⊆ S i› for i
        by (simp add: S_def subset_iff) (metis in_mono le_approx1 po_class.chainE chain_Y)
      ultimately have ‹(⋂i. S i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
      then obtain t1 where ‹∀i. t1 ∈ S i›
        by (meson INT_iff ex_in_conv iso_tuple_UNIV_I)
      thus ‹t ∈ 𝒟 ?lhs› by (simp add: S_def D_After initial "*")
          (simp add: limproc_is_thelub chain_Y D_LUB)
    next
      show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
        by (simp add: F_After initial)
          (simp add: F_After "*" limproc_is_thelub chain_After chain_Y F_LUB)
    next
      fix t X assume ‹t ∉ 𝒟 ?rhs› and ‹(t, X) ∈ ℱ ?rhs›
      from ‹t ∉ 𝒟 ?rhs› obtain j where ‹t ∉ 𝒟 (Y j after a)›
        by (auto simp add: limproc_is_thelub chain_After ‹chain Y› D_LUB)
      moreover from ‹(t, X) ∈ ℱ ?rhs› have ‹(t, X) ∈ ℱ (Y j after a)›
        by (simp add: limproc_is_thelub chain_After ‹chain Y› F_LUB)
      ultimately show ‹(t, X) ∈ ℱ ?lhs›
        using chain_Y initial is_ub_thelub mono_After proc_ord2a by blast
    qed
  next
    assume ‹ev a ∉ (⨆i. Y i)0›
    then obtain k where * : ‹ev a ∉ (Y (i + k))0› for i
      by (simp add: initials_LUB chain_Y)
        (metis add.commute anti_mono_initials chain_Y in_mono le_add1 po_class.chain_mono)
    hence ** : ‹ev a ∉ (⨆i. Y (i + k))0› by (simp add: initials_LUB chain_Y chain_shift)
    have ‹?lhs = (⨆ i. Y (i + k)) after a› by (simp add: chain_Y lub_range_shift)
    also have ‹… = (⨆ i. Y (i + k) after a)›
      by (simp add: not_initial_After "*" "**")
        (fact cont2contlubE[OF cont_Ψ chain_shift[OF chain_Y]]) 
    also from chain_After lub_range_shift have ‹… = ?rhs› by blast
    finally show ‹?lhs = ?rhs› .
  qed
qed


lemma After_cont [simp] : 
  ‹cont (λx. f x after a)› if cont_Ψ : ‹cont (λP. Ψ P a)› and cont_f : ‹cont f›
proof (rule contI2)
  show ‹monofun (λx. f x after a)›
    by (rule monofunI) (metis cont2monofunE cont_Ψ cont_f mono_After)
next
  show ‹chain Y ⟹ f (⨆i. Y i) after a ⊑ (⨆i. f (Y i) after a)› for Y
    by (simp add: ch2ch_cont cont2contlubE cont_Ψ cont_f cont_prem_After)
qed

end

end

(*<*)
end
  (*>*)