Theory Sequential_Composition

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Sequential composition
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * 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 ‹The Sequential Composition›

(*<*)
theory  Sequential_Composition
  imports Process
begin 
  (*>*)

section‹Definition›

lift_definition  Seq :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k› (infixl ‹❙;› 74)
  is ‹λP Q. ({(t, X) |t X. (t, X ∪ range tick) ∈ ℱ P ∧ tF t} ∪
             {(t @ u, X) |t u r X. t @ [✓(r)] ∈ 𝒯 P ∧ (u, X) ∈ ℱ Q} ∪
             {(t, X). t ∈ 𝒟 P},
             𝒟 P ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒟 Q})›
proof -
  show ‹?thesis P Q› (is ‹is_process(?f, ?d)›) for P and Q
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
    show ‹([], {}) ∈ ?f›
      by simp (metis (no_types, opaque_lifting) T_F_spec append_Nil f_inv_into_f
          is_processT1 is_processT5_S7)
  next
    show ‹(s, X) ∈ ?f ⟹ front_tickFree s› for s X
      by (auto simp: is_processT2 append_T_imp_tickFree front_tickFree_append D_imp_front_tickFree)   
  next
    show ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s t
    proof (induct t arbitrary: s)
      show ‹(s @ [], {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s by simp
    next
      fix s e t assume prem : ‹(s @ e # t, {}) ∈ ?f›
      assume hyp : ‹(s @ t, {}) ∈ ?f ⟹ (s, {}) ∈ ?f› for s
      from prem have ‹((s @ [e]) @ t, {}) ∈ ?f› by simp
      with hyp have ‹(s @ [e], {}) ∈ ?f› by presburger
      then consider (F_P) ‹(s @ [e], range tick) ∈ ℱ P› ‹tF s›
        | (F_Q) t u r where ‹s @ [e] = t @ u› ‹t @ [✓(r)] ∈ 𝒯 P› ‹(u, {}) ∈ ℱ Q›
        by (auto intro: is_processT8)
          (meson F_T append_T_imp_tickFree is_processT8 not_Cons_self2)
      thus ‹(s, {}) ∈ ?f›
      proof cases
        case F_P
        from F_P(1) is_processT3 is_processT4_empty have ‹(s, {}) ∈ ℱ P› by blast
        with F_P(2) show ‹(s, {}) ∈ ?f›
          by (elim trace_tick_continuation_or_all_tick_failuresE)
            (simp_all, metis append.right_neutral is_processT1)
      next
        case F_Q
        show ‹(s, {}) ∈ ?f›
        proof (cases u rule: rev_cases)
          assume ‹u = []›
          with F_Q(1) have ‹s @ [e] = t› by simp
          with F_Q(2) T_F is_processT3 have ‹(s, {}) ∈ ℱ P› by blast
          with F_Q(2) ‹s @ [e] = t› show ‹(s, {}) ∈ ?f›
            by (elim trace_tick_continuation_or_all_tick_failuresE, simp_all)
              (metis append.right_neutral is_processT1,
                metis append_T_imp_tickFree not_Cons_self2 tickFree_append_iff)
        next
          from F_Q show ‹u = u' @ [e'] ⟹ (s, {}) ∈ ?f› for u' e'
            by simp (metis is_processT3)
        qed
      qed
    qed
  next
    show ‹(s, Y) ∈ ?f ∧ X ⊆ Y ⟹ (s, X) ∈ ?f› for s X Y
      by simp (metis Un_mono image_mono is_processT4 top.extremum_unique)
  next
    fix s X Y assume * : ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)›
    from "*" consider ‹s ∈ ?d›
      | (F_P) ‹(s, X ∪ range tick) ∈ ℱ P› ‹tickFree s›
      | (F_Q) t u r where ‹s = t @ u› ‹t @ [✓(r)] ∈ 𝒯 P› ‹(u, X) ∈ ℱ Q› by fast
    thus ‹(s, X ∪ Y) ∈ ?f›
    proof cases
      from is_processT8 show ‹s ∈ ?d ⟹ (s, X ∪ Y) ∈ ?f› by simp blast
    next
      case F_P
      let ?Y_evs = ‹Y - range tick›
      have ‹(s, X ∪ range tick ∪ ?Y_evs) ∈ ℱ P›
      proof (intro is_processT5[OF F_P(1)] allI impI)
        fix c assume ‹c ∈ ?Y_evs›
        then obtain r where ‹c = ev r› ‹ev r ∈ Y›
          by (metis Diff_iff event⇩p⇩t⇩i⇩c⇩k.exhaust rangeI)
        from "*"[THEN conjunct2, rule_format, OF ‹ev r ∈ Y›]
        show ‹(s @ [c], {}) ∉ ℱ P›
          by (simp add: ‹c = ev r› ‹tickFree s› image_iff)
            (metis append_Nil2 is_processT1 trace_tick_continuation_or_all_tick_failuresE)
      qed
      also have ‹X ∪ range tick ∪ ?Y_evs = X ∪ Y ∪ range tick› by fast
      finally have ‹(s, X ∪ Y ∪ range tick) ∈ ℱ P› .
      with F_P(2) show ‹(s, X ∪ Y) ∈ ?f› by simp
    next
      case F_Q
      from "*" have ‹∀c. c ∈ Y ⟶ (u @ [c], {}) ∉ ℱ Q›
        by (simp add: F_Q(1)) (metis F_Q(2))
      with F_Q(3) have ‹(u, X ∪ Y) ∈ ℱ Q› by (simp add: is_processT5)
      with F_Q(1, 2) show ‹(s, X ∪ Y) ∈ ?f› by auto
    qed
  next
    show ‹s ∈ ?d ∧ tF s ∧ ftF t ⟹ s @ t ∈ ?d› for s t
      by (simp, elim conjE disjE exE)
        (metis is_processT7, meson append_assoc is_processT7 tickFree_append_iff)
  next  
    from is_processT8 show ‹s ∈ ?d ⟹ (s, X) ∈ ?f› for s X by simp blast
  next
    show ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d› for s r
      by (simp, elim conjE disjE exE)
        (meson is_processT9,
          metis (no_types) D_T T_nonTickFree_imp_decomp append.assoc append_T_imp_tickFree
          butlast_snoc is_processT9 non_tickFree_tick not_Cons_self2 tickFree_append_iff)
    fix s r X assume ‹(s @ [✓(r)], {}) ∈ ?f›
    then consider ‹s @ [✓(r)] ∈ ?d›
      | (F_Q) t u r' where ‹s @ [✓(r)] = t @ u› ‹t @ [✓(r')] ∈ 𝒯 P› ‹(u, X) ∈ ℱ Q›
      by (auto simp add: is_processT8)
        (metis F_T append_T_imp_tickFree is_processT5_S7
          non_tickFree_tick not_Cons_self2 tickFree_append_iff)
    thus ‹(s, X - {✓(r)}) ∈ ?f›
    proof cases
      assume ‹s @ [✓(r)] ∈ ?d›
      hence ‹s ∈ ?d› by (fact ‹s @ [✓(r)] ∈ ?d ⟹ s ∈ ?d›)
      with is_processT8 show ‹(s, X - {✓(r)}) ∈ ?f› by simp blast
    next
      case F_Q
      from F_Q(1, 2) obtain u' where ‹u = u' @ [✓(r)]›
        by (cases u rule: rev_cases, simp_all)
          (meson append_T_imp_tickFree non_tickFree_tick not_Cons_self2 tickFree_append_iff)
      with F_Q(3) have ‹(u', X - {✓(r)}) ∈ ℱ Q› by (simp add: F_T is_processT6_TR)
      with F_Q(1, 2) ‹u = u' @ [✓(r)]› show ‹(s, X - {✓(r)}) ∈ ?f› by auto
    qed
  qed
qed



section‹The Projections›

lemma F_Seq : ‹ℱ (P ❙; Q) = {(t, X) |t X. (t, X ∪ range tick) ∈ ℱ P ∧ tF t} ∪
                           {(t @ u, X) |t u r X. t @ [✓(r)] ∈ 𝒯 P ∧ (u, X) ∈ ℱ Q} ∪
                           {(t, X). t ∈ 𝒟 P}›
  by (simp add: Failures.rep_eq FAILURES_def Seq.rep_eq)


lemma D_Seq : ‹𝒟 (P ❙; Q) = 𝒟 P ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒟 Q}›
  by (simp add: Divergences.rep_eq DIVERGENCES_def Seq.rep_eq)


lemma T_Seq_bis :
  ‹𝒯 (P ❙; Q) = {t. (t, range tick) ∈ ℱ P ∧ tF t} ∪
               {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒯 Q} ∪
               𝒟 P›
  by (auto simp add: Traces.rep_eq TRACES_def F_Seq simp flip: Failures.rep_eq)
    (meson is_processT4 sup_ge2, meson is_processT5_S7', blast)


lemma T_Seq :
  ‹𝒯 (P ❙; Q) = {t ∈ 𝒯 P. tF t} ∪ {t @ u |t u r. t @ [✓(r)] ∈ 𝒯 P ∧ u ∈ 𝒯 Q} ∪ 𝒟 P›
  ―‹Often easier to use›
  by (auto simp add: T_Seq_bis F_T)
    (metis T_F_spec append.right_neutral is_processT1_TR
      trace_tick_continuation_or_all_tick_failuresE)

lemmas Seq_projs = F_Seq D_Seq T_Seq



section‹ Continuity Rule ›

lemma mono_Seq : ‹P ⊑ Q ⟹ R ⊑ S ⟹ P ❙; R ⊑ Q ❙; S› for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof -
  have ‹P ❙; S ⊑ Q ❙; S› if ‹P ⊑ Q› for P Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and S
  proof (unfold le_approx_def, intro conjI allI impI subset_antisym)
    show ‹𝒟 (Q ❙; S) ⊆ 𝒟 (P ❙; S)›
      apply (rule subsetI, simp add: D_Seq, elim disjE exE conjE)
      by (meson in_mono le_approx1 ‹P ⊑ Q›) (metis D_T le_approx2T ‹P ⊑ Q›)
  next
    show ‹s ∉ 𝒟 (P ❙; S) ⟹ ℛ⇩a (P ❙; S) s ⊆ ℛ⇩a (Q ❙; S) s› for s
      apply (auto simp add: D_Seq Refusals_after_def F_Seq set_eq_iff append_T_imp_tickFree)[1]
      by (meson le_approx2 ‹P ⊑ Q›)
        (metis F_imp_front_tickFree append_T_imp_tickFree is_processT7 is_processT9 le_approx2T not_Cons_self2 ‹P ⊑ Q›)+
  next
    show ‹s ∉ 𝒟 (P ❙; S) ⟹ ℛ⇩a (Q ❙; S) s ⊆ ℛ⇩a (P ❙; S) s› for s
      apply (auto simp add: D_Seq Refusals_after_def F_Seq set_eq_iff append_T_imp_tickFree)
          apply (meson le_approx2 ‹P ⊑ Q›)
      by ((metis D_T le_approx2T ‹P ⊑ Q›)+)[2]
        ((meson in_mono le_approx1 ‹P ⊑ Q›)+)[2]
  next
    show ‹min_elems (𝒟 (P ❙; S)) ⊆ 𝒯 (Q ❙; S)›
    proof (rule subset_trans; rule subsetI)
      fix t assume ‹t ∈ min_elems (𝒟 (P ❙; S))›
      hence ‹t ∈ 𝒟 (P ❙; S)› by (meson elem_min_elems)
      then consider ‹t ∈ 𝒟 P› | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹v ∈ 𝒟 S›
        by (simp add: D_Seq)
          (metis D_imp_front_tickFree append_T_imp_tickFree is_processT7 not_Cons_self2)
      thus ‹t ∈ min_elems (𝒟 P) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ v ∈ min_elems (𝒟 S)}›
      proof cases
        assume ‹t ∈ 𝒟 P›
        with ‹t ∈ min_elems (𝒟 (P ❙; S))› have ‹t ∈ min_elems (𝒟 P)›
          by (auto simp add: D_Seq min_elems_def)
        thus ‹t ∈ min_elems (𝒟 P) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ v ∈ min_elems (𝒟 S)}› ..
      next
        fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 P› ‹u ∉ 𝒟 P› ‹v ∈ 𝒟 S›
        with ‹t ∈ min_elems (𝒟 (P ❙; S))›
        have ‹t ∈ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ v ∈ min_elems (𝒟 S)}›
          by (simp add: D_Seq min_elems_def)
            (metis (mono_tags, lifting) Un_iff less_append mem_Collect_eq)
        thus ‹t ∈ min_elems (𝒟 P) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ v ∈ min_elems (𝒟 S)}› ..
      qed
    next
      show ‹t ∈ min_elems (𝒟 P) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 P ∧ u ∉ 𝒟 P ∧ v ∈ min_elems (𝒟 S)}
            ⟹ t ∈ 𝒯 (Q ❙; S)› for t
        by (simp add: T_Seq, elim disjE exE conjE)
          (metis (no_types, lifting) Prefix_Order.prefixI T_nonTickFree_imp_decomp
            elem_min_elems in_mono is_processT9 le_approx3 min_elems_no
            not_Cons_self2 self_append_conv ‹P ⊑ Q›,
            metis D_T elem_min_elems is_processT9 le_approx2T ‹P ⊑ Q›)
    qed
  qed

  moreover have ‹S ❙; P ⊑ S ❙; Q› if ‹P ⊑ Q› for P Q and S :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  proof (unfold le_approx_def, intro conjI allI impI subset_antisym)
    show ‹𝒟 (S ❙; Q) ⊆ 𝒟 (S ❙; P)›
      by (rule subsetI, simp add: D_Seq) (metis in_mono le_approx1 that)
  next
    show ‹s ∉ 𝒟 (S ❙; P) ⟹ ℛ⇩a (S ❙; P) s ⊆ ℛ⇩a (S ❙; Q) s› for s
      apply (auto simp add: D_Seq Refusals_after_def F_Seq append_T_imp_tickFree)
      by (metis proc_ord2a that)+
  next
    show ‹s ∉ 𝒟 (S ❙; P) ⟹ ℛ⇩a (S ❙; Q) s ⊆ ℛ⇩a (S ❙; P) s› for s
      apply (auto simp add: D_Seq Refusals_after_def F_Seq append_T_imp_tickFree)
      by (metis proc_ord2a that)+
  next
    show ‹min_elems (𝒟 (S ❙; P)) ⊆ 𝒯 (S ❙; Q)›
    proof (rule subset_trans; rule subsetI)
      fix t assume ‹t ∈ min_elems (𝒟 (S ❙; P))›
      hence ‹t ∈ 𝒟 (S ❙; P)› by (meson elem_min_elems)
      then consider ‹t ∈ 𝒟 S› | u v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 S› ‹u ∉ 𝒟 S› ‹v ∈ 𝒟 P›
        by (simp add: D_Seq)
          (metis D_imp_front_tickFree append_T_imp_tickFree is_processT7 not_Cons_self2)
      thus ‹t ∈ min_elems (𝒟 S) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 S ∧ u ∉ 𝒟 S ∧ v ∈ min_elems (𝒟 P)}›
      proof cases
        assume ‹t ∈ 𝒟 S›
        with ‹t ∈ min_elems (𝒟 (S ❙; P))› have ‹t ∈ min_elems (𝒟 S)›
          by (auto simp add: D_Seq min_elems_def)
        thus ‹t ∈ min_elems (𝒟 S) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 S ∧ u ∉ 𝒟 S ∧ v ∈ min_elems (𝒟 P)}› ..
      next
        fix u v r assume ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 S› ‹u ∉ 𝒟 S› ‹v ∈ 𝒟 P›
        with ‹t ∈ min_elems (𝒟 (S ❙; P))›
        have ‹t ∈ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 S ∧ u ∉ 𝒟 S ∧ v ∈ min_elems (𝒟 P)}›
          by (simp add: D_Seq min_elems_def)
            (metis (mono_tags, lifting) Un_iff less_append mem_Collect_eq)
        thus ‹t ∈ min_elems (𝒟 S) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 S ∧ u ∉ 𝒟 S ∧ v ∈ min_elems (𝒟 P)}› ..
      qed
    next
      show ‹t ∈ min_elems (𝒟 S) ∪ {u @ v |u v r. u @ [✓(r)] ∈ 𝒯 S ∧ u ∉ 𝒟 S ∧ v ∈ min_elems (𝒟 P)}
            ⟹ t ∈ 𝒯 (S ❙; Q)› for t
        by (simp add:  T_Seq, elim disjE exE conjE)
          (use elem_min_elems in blast,
            metis insert_absorb insert_subset le_approx3 ‹P ⊑ Q›)
    qed
  qed

  ultimately show ‹P ⊑ Q ⟹ R ⊑ S ⟹ P ❙; R ⊑ Q ❙; S› by (meson below_trans)
qed


context begin

private lemma chain_Seq_left: ‹chain Y ⟹ chain (λi. Y i ❙; S)›
  by (simp add: mono_Seq po_class.chain_def)

private lemma chain_Seq_right: ‹chain Y ⟹ chain (λi. S ❙; Y i)›
  by (simp add: mono_Seq po_class.chain_def)


private lemma cont_left_prem_Seq :
  ‹(⨆i. Y i) ❙; S = (⨆i. Y i ❙; S)› (is ‹?lhs = ?rhs›) if ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: D_Seq limproc_is_thelub ‹chain Y› chain_Seq_left LUB_projs)
next
  fix t assume ‹t ∈ 𝒟 ?rhs›
  define T where ‹T i ≡ {u ∈ 𝒟 (Y i). t = u} ∪
                        {u. ∃r v. t = u @ v ∧ u @ [✓(r)] ∈ 𝒯 (Y i) ∧ v ∈ 𝒟 S}› for i
  from ‹t ∈ 𝒟 ?rhs› have ‹T i ≠ {}› for i
    by (auto simp add: T_def D_Seq limproc_is_thelub ‹chain Y› chain_Seq_left D_LUB)
  moreover have ‹finite (T 0)› unfolding T_def by (prove_finite_subset_of_prefixes t)
  moreover have ‹T (Suc i) ⊆ T i› for i
    unfolding T_def apply (intro allI Un_mono subsetI, simp_all)
    by (meson ‹chain Y› in_mono le_approx1 po_class.chainE)
      (metis ‹chain Y› le_approx_lemma_T po_class.chain_def subset_iff)
  ultimately have ‹(⋂i. T i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
  then obtain u where ‹∀i. u ∈ T i› by fast
  show ‹t ∈ 𝒟 ?lhs›
  proof (cases ‹∀i. t ∈ 𝒟 (Y i)›)
    show ‹∀i. t ∈ 𝒟 (Y i) ⟹ t ∈ 𝒟 ?lhs›
      by (simp add: D_Seq limproc_is_thelub D_LUB ‹chain Y›)
  next
    assume ‹¬ (∀i. t ∈ 𝒟 (Y i))›
    with ‹∀i. u ∈ T i› obtain r v j
      where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (Y j)› ‹u ∉ 𝒟 (Y j)› ‹v ∈ 𝒟 S›
      by (simp add: T_def)
        (metis D_imp_front_tickFree append_T_imp_tickFree is_processT7 not_Cons_self2)
    from ‹u ∉ 𝒟 (Y j)› ‹u @ [✓(r)] ∈ 𝒯 (Y j)› have ‹∀i≥j. u @ [✓(r)] ∈ 𝒯 (Y i)›
      by (meson ND_F_dir2' ‹chain Y› ‹u ∉ 𝒟 (Y j)› is_processT9 is_ub_thelub)
    hence ‹u @ [✓(r)] ∈ 𝒯 (⨆i. Y i)›
      by (simp add: limproc_is_thelub T_LUB ‹chain Y›)
        (meson D_T ‹chain Y› le_approx2T nle_le po_class.chain_mono)
    with ‹v ∈ 𝒟 S› show ‹t ∈ 𝒟 ?lhs› by (auto simp add: ‹t = u @ v› D_Seq ‹chain Y›)
  qed
next
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (auto simp add: F_Seq limproc_is_thelub ‹chain Y› chain_Seq_left LUB_projs)
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  fix t X assume ‹(t, X) ∈ ℱ ?rhs›
  then consider ‹∀i. t ∈ 𝒟 (Y i)› 
    | j       where ‹t ∉ 𝒟 (Y j)› ‹(t, X ∪ range tick) ∈ ℱ (Y j)› ‹tF t›
    | j u r v where ‹t ∉ 𝒟 (Y j)› ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (Y j)› ‹(v, X) ∈ ℱ S›
    by (simp add: limproc_is_thelub ‹chain Y› chain_Seq_left F_LUB F_Seq) blast
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    show ‹∀i. t ∈ 𝒟 (Y i) ⟹ (t, X) ∈ ℱ ?lhs›
      by (simp add: D_LUB_2 D_Seq is_processT8 limproc_is_thelub ‹chain Y›)
  next
    fix j assume ‹t ∉ 𝒟 (Y j)› ‹(t, X ∪ range tick) ∈ ℱ (Y j)› ‹tF t›
    hence ‹(t, X ∪ range tick) ∈ ℱ (⨆i. Y i)›
      by (simp add: limproc_is_thelub ‹chain Y› F_LUB)
        (metis is_processT8 nle_le po_class.chain_mono proc_ord2a ‹chain Y›)
    with ‹tF t› show ‹(t, X) ∈ ℱ ?lhs› by (simp add: F_Seq)
  next
    fix j u r v assume ‹t ∉ 𝒟 (Y j)› ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 (Y j)› ‹(v, X) ∈ ℱ S›
    hence ‹u @ [✓(r)] ∈ 𝒯 (⨆i. Y i)›
      by (simp add: limproc_is_thelub ‹chain Y› T_LUB)
        (meson F_imp_front_tickFree ND_F_dir2' T_F_spec append_T_imp_tickFree
          is_processT7 is_ub_thelub min_elems2 not_Cons_self2 ‹chain Y›)
    with ‹(v, X) ∈ ℱ S› show ‹(t, X) ∈ ℱ ?lhs› by (auto simp add: F_Seq ‹t = u @ v›)
  qed
qed


private lemma cont_right_prem_Seq :
  ‹S ❙; (⨆i. Y i) = (⨆i. S ❙; Y i)› (is ‹?lhs = ?rhs›) if ‹chain Y› 
proof (subst Process_eq_spec_optimized, safe)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: D_Seq limproc_is_thelub ‹chain Y› chain_Seq_right D_LUB)
next
  show ‹t ∈ 𝒟 ?lhs› if ‹t ∈ 𝒟 ?rhs› for t
  proof (cases ‹t ∈ 𝒟 S›)
    show ‹t ∈ 𝒟 S ⟹ t ∈ 𝒟 (S ❙; (⨆i. Y i))› by (simp add: D_Seq)
  next
    assume ‹t ∉ 𝒟 S›
    define T where ‹T i ≡ {u. ∃v r. t = u @ v ∧ u @ [✓(r)] ∈ 𝒯 S ∧ v ∈ 𝒟 (Y i)}› for i
    from ‹t ∉ 𝒟 S› ‹t ∈ 𝒟 ?rhs› have ‹T i ≠ {}› for i
      by (simp add: T_def limproc_is_thelub chain_Seq_right ‹chain Y› D_LUB D_Seq)
    moreover have ‹finite (T 0)›
      unfolding T_def by (prove_finite_subset_of_prefixes t)
    moreover have ‹T (Suc i) ⊆ T i› for i
      unfolding T_def apply (intro allI Un_mono subsetI; simp)
      by (metis le_approx1 po_class.chainE subset_iff ‹chain Y›)
    ultimately have ‹(⋂i. T i) ≠ {}› by (rule Inter_nonempty_finite_chained_sets)
    then obtain u where ‹∀i. u ∈ T i› by fast
    then obtain v r where ‹t = u @ v› ‹u @ [✓(r)] ∈ 𝒯 S› ‹∀i. v ∈ 𝒟 (Y i)›
      by (simp add: T_def) blast
    from ‹∀i. v ∈ 𝒟 (Y i)› have ‹v ∈ 𝒟 (⨆i. Y i)›
      by (simp add: D_LUB ‹chain Y› limproc_is_thelub)
    with ‹u @ [✓(r)] ∈ 𝒯 S› show ‹t ∈ 𝒟 ?lhs› by (auto simp add: ‹t = u @ v›  D_Seq)
  qed
next
  show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    by (auto simp add: F_Seq limproc_is_thelub ‹chain Y› chain_Seq_right F_LUB)
next
  assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
  show ‹(t, X) ∈ ℱ ?lhs› if ‹(t, X) ∈ ℱ ?rhs› for t X
  proof (cases ‹t ∈ 𝒟 ?rhs›)
    show ‹t ∈ 𝒟 ?rhs ⟹ (t, X) ∈ ℱ ?lhs›
      by (simp add: is_processT8 same_div)
  next
    assume ‹t ∉ 𝒟 ?rhs›
    then obtain j where ‹t ∉ 𝒟 (S ❙; Y j)›
      by (auto simp add: limproc_is_thelub chain_Seq_right ‹chain Y› D_LUB)
    moreover from ‹(t, X) ∈ ℱ ?rhs› have ‹(t, X) ∈ ℱ (S ❙; Y j)›
      by (simp add: limproc_is_thelub chain_Seq_right ‹chain Y› F_LUB)
    ultimately show ‹(t, X) ∈ ℱ ?lhs›
      by (fact le_approx2[OF mono_Seq[OF below_refl is_ub_thelub[OF ‹chain Y›]], THEN iffD2])
  qed
qed


lemma Seq_cont [simp] : ‹cont (λx. f x ❙; g x)› if ‹cont f› and ‹cont g›
proof (rule cont_apply[where f = ‹λx y. f x ❙; y›])
  show ‹cont g› by (fact ‹cont g›)
next
  show ‹cont ((❙;) (f x))› for x
  proof (rule contI2)
    show ‹monofun ((❙;) (f x))› by (simp add: mono_Seq monofunI)
  next
    show ‹chain Y ⟹ f x ❙; (⨆i. Y i) ⊑ (⨆i. f x ❙; Y i)› for Y
      by (simp add: cont_right_prem_Seq)
  qed
next
  show ‹cont (λx. f x ❙; y)› for y
  proof (rule contI2)
    show ‹monofun (λx. f x ❙; y)› by (simp add: cont2monofunE mono_Seq monofunI ‹cont f›)
  next
    show ‹chain Y ⟹ f (⨆i. Y i) ❙; y ⊑ (⨆i. f (Y i) ❙; y)› for Y
      by (simp add: ch2ch_cont cont2contlubE cont_left_prem_Seq ‹cont f›)
  qed
qed


end

(*<*)
end
  (*>*)