Theory Seq

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Burkhart Wolff, Safouan Taha.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : A Combined CSP Theory
 *
 * Copyright (c) 2009 Université Paris-Sud, 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.
 ******************************************************************************›
(*>*)

section‹The Sequence Operator›

theory  Seq
  imports Process 
begin 

subsection‹Definition›
abbreviation "div_seq P Q   ≡ {t1 @ t2 |t1 t2. t1 ∈ 𝒟 P ∧ tickFree t1 ∧ front_tickFree t2}
                            ∪ {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}"

lift_definition  Seq :: "['a process,'a process] ⇒ 'a process"  (infixl  ‹❙;› 74)  
is       "λP Q. ({(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪
                 {(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
                 {(t, X). t ∈ div_seq P Q},
                 div_seq P Q)"
proof -
  show "is_process ({(t, X). (t, X ∪ {tick}) ∈ ℱ (P :: 'a process) ∧ tickFree t} ∪
                    {(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
                    {(t, X). t ∈ div_seq P Q},
                    div_seq P Q)"
   (is "is_process(?f, ?d)") for P Q
    unfolding is_process_def FAILURES_def DIVERGENCES_def
  proof (simp only: fst_conv snd_conv, intro conjI)
    show "([], {}) ∈ ?f" 
      apply(cases "[tick] ∈ 𝒯 P", simp_all add: is_processT1)
      using F_T is_processT5_S6 by blast        
  next
    show " ∀s X. (s, X) ∈ ?f ⟶ front_tickFree s"
      by (auto simp:is_processT2 append_T_imp_tickFree front_tickFree_append D_imp_front_tickFree)   
  next
    show "∀s t. (s @ t, {}) ∈ ?f ⟶ (s, {}) ∈ ?f"       
      apply auto
            apply (metis F_T append_Nil2 is_processT is_processT3_SR is_processT5_S3)
           apply(simp add:append_eq_append_conv2) 
           apply (metis T_F_spec append_Nil2 is_processT is_processT5_S4)
          apply (metis append_self_conv front_tickFree_append front_tickFree_mono is_processT2_TR 
                no_Trace_implies_no_Failure non_tickFree_implies_nonMt non_tickFree_tick)
         apply (metis (mono_tags, lifting) F_T append_Nil2 is_processT5_S3 process_charn)
        apply (metis front_tickFree_append front_tickFree_mono self_append_conv)
       apply(simp add:append_eq_append_conv2)
       apply (metis T_F_spec append_Nil2 is_processT is_processT5_S4)
      by (metis D_imp_front_tickFree append_T_imp_tickFree front_tickFree_append 
                 front_tickFree_mono not_Cons_self2 self_append_conv)
  next
    show "∀s X Y. (s, Y) ∈ ?f ∧ X ⊆ Y ⟶ (s, X) ∈ ?f" 
      apply auto
         apply (metis insert_mono is_processT4_S1 prod.sel(1) prod.sel(2))
        apply (metis is_processT4)
       apply (simp add: append_T_imp_tickFree)
      by (metis process_charn)
  next
    { fix sa X Y
      have "(sa, X ∪ {tick}) ∈ ℱ P ⟹
              tickFree sa ⟹
              ∀c. c ∈ Y ∧ c ≠ tick ⟶ (sa @ [c], {}) ∉ ℱ P ⟹ 
              (sa, X ∪ Y ∪ {tick}) ∈ ℱ P ∧ tickFree sa"
      apply(rule_tac t="X ∪ Y ∪ {tick}" and s="X ∪ {tick} ∪ (Y-{tick})" in subst,auto)
      by   (metis DiffE Un_insert_left is_processT5 singletonI)
    } note is_processT5_SEQH3 = this
    have is_processT5_SEQH4 : 
         "⋀ sa X Y. (sa, X ∪ {tick}) ∈ ℱ P 
                     ⟹ tickFree sa 
                     ⟹ ∀c. c ∈ Y ⟶ (sa@[c],{tick}) ∉ ℱ P ∨ ¬ tickFree(sa@[c]) 
                     ⟹ ∀c. c ∈ Y ⟶ (∀t1 t2. sa@[c]≠t1@t2 ∨ t1@[tick]∉𝒯 P ∨ (t2,{})∉ℱ Q) 
                     ⟹ (sa, X ∪ Y ∪ {tick}) ∈ ℱ P ∧ tickFree sa"
      by (metis append_Nil2 is_processT1 is_processT5_S3 is_processT5_SEQH3 
                           no_Trace_implies_no_Failure tickFree_Cons tickFree_append)
    let ?f1 = "{(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪ 
               {(t, X). ∃t1 t2. t = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q}"
    have is_processT5_SEQ2: "⋀ sa X Y. (sa, X) ∈ ?f1 
                                        ⟹ (∀c. c ∈ Y ⟶ (sa@[c], {})∉?f) 
                                        ⟹ (sa, X∪Y) ∈ ?f1"
      apply (clarsimp,rule is_processT5_SEQH4[simplified])
      by (auto simp: is_processT5)
    show "∀s X Y. (s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f) ⟶ (s, X ∪ Y) ∈ ?f"
      apply(intro allI impI, elim conjE UnE)
        apply(rule rev_subsetD)
         apply(rule is_processT5_SEQ2)
          apply auto
        using is_processT5_S1 apply force
       apply (simp add: append_T_imp_tickFree)
      using is_processT5[rule_format, OF conjI] by force
  next  
    show "∀s X. (s @ [tick], {}) ∈ ?f ⟶ (s, X - {tick}) ∈ ?f" 
      apply auto
          apply (metis (no_types, lifting) append_T_imp_tickFree butlast_append 
                       butlast_snoc is_processT2 is_processT6 nonTickFree_n_frontTickFree 
                       non_tickFree_tick tickFree_append)
         apply (metis append_T_imp_tickFree front_tickFree_append front_tickFree_mono 
                      is_processT2 non_tickFree_implies_nonMt non_tickFree_tick)
        apply (metis process_charn)
       apply (metis front_tickFree_append front_tickFree_implies_tickFree)
      apply (metis D_T T_nonTickFree_imp_decomp append_T_imp_tickFree append_assoc 
                   append_same_eq non_tickFree_implies_nonMt non_tickFree_tick process_charn 
                   tickFree_append)
      by    (metis D_imp_front_tickFree append_T_imp_tickFree front_tickFree_append 
                      front_tickFree_mono non_tickFree_implies_nonMt non_tickFree_tick)
  next
    show "∀s t. s ∈ ?d ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ ?d"
      apply auto 
       using front_tickFree_append apply blast     
      by (metis process_charn)
  next  
    show "∀s X. s ∈ ?d ⟶  (s, X) ∈ ?f"
      by blast
  next  
    show "∀s. s @ [tick] ∈ ?d ⟶ s ∈ ?d"
      apply auto      
       apply (metis append_Nil2 front_tickFree_implies_tickFree process_charn)
      by (metis append1_eq_conv append_assoc front_tickFree_implies_tickFree is_processT2_TR 
                  nonTickFree_n_frontTickFree non_tickFree_tick process_charn tickFree_append)
  qed
qed


subsection‹The Projections›

lemma F_Seq: ‹ℱ (P ❙; Q) = {(t, X). (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪ 
                          {(t1 @ t2, X) |t1 t2 X. t1 @ [tick] ∈ 𝒯 P ∧ (t2, X) ∈ ℱ Q} ∪
                          {(t1, X) |t1 X. t1 ∈ 𝒟 P}›
  apply (subst Failures.rep_eq, auto simp add: Seq.rep_eq FAILURES_def)
  using is_processT7 is_processT apply (blast+)[5]
  by (meson is_processT)
     (metis front_tickFree_implies_tickFree front_tickFree_single
            is_processT nonTickFree_n_frontTickFree)

 
lemma D_Seq: ‹𝒟 (P ❙; Q) = 𝒟 P ∪ {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒟 Q}›
  apply (subst Divergences.rep_eq, auto simp add: Seq.rep_eq DIVERGENCES_def)
  by (simp add: is_processT7_S)
     (metis elem_min_elems front_tickFree_mono is_processT min_elems_charn 
            nonTickFree_n_frontTickFree non_tickFree_tick tickFree_Nil tickFree_append)


lemma T_Seq: ‹𝒯 (P ❙; Q) = {t. ∃X. (t, X ∪ {tick}) ∈ ℱ P ∧ tickFree t} ∪ 
                          {t1 @ t2 |t1 t2. t1 @ [tick] ∈ 𝒯 P ∧ t2 ∈ 𝒯 Q} ∪
                          𝒟 P›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Seq)
   

subsection‹ Continuity Rule ›

lemma mono_Seq_D11:  
"P ⊑ Q ⟹ 𝒟 (Q ❙; S) ⊆ 𝒟 (P ❙; S)"
  apply(auto simp: D_Seq)
   using le_approx1 apply blast
  using le_approx_lemma_T by blast

lemma mono_Seq_D12: 
assumes ordered: "P ⊑ Q"
shows   "(∀ s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (P ❙; S) s = Ra (Q ❙; S) s)"
proof -
  have mono_SEQI2a:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (Q ❙; S) s ⊆ Ra (P ❙; S) s"
    apply(simp add: Ra_def D_Seq F_Seq)
    apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q], auto) 
    using le_approx1 by blast+
  have mono_SEQI2b:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (P ❙; S) ⟶ Ra (P ❙; S) s ⊆ Ra (Q ❙; S) s"
    apply(simp add: Ra_def D_Seq F_Seq)
    apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q] 
          le_approx1[of P Q] le_approx2T[of P Q], auto) 
      using le_approx2 apply fastforce
     apply (metis front_tickFree_implies_tickFree is_processT2_TR process_charn)
    apply (simp add: append_T_imp_tickFree) 
    by (metis front_tickFree_implies_tickFree is_processT2_TR process_charn)
  show ?thesis 
    using ordered mono_SEQI2a mono_SEQI2b by(blast)
qed

lemma minSeqInclu: 
  "min_elems(𝒟 (P ❙; S)) 
   ⊆ min_elems(𝒟 P) ∪ {t1@t2|t1 t2. t1@[tick]∈𝒯 P∧t1∉𝒟 P∧t2∈min_elems(𝒟 S)}"
  apply(auto simp: D_Seq min_elems_def)
  by (metis append_single_T_imp_tickFree less_append process_charn)
    

lemma mono_Seq_D13 : 
assumes ordered: "P ⊑ Q"
shows        "min_elems (𝒟 (P ❙; S)) ⊆ 𝒯 (Q ❙; S)"
  apply (insert ordered, frule le_approx3, rule subset_trans [OF minSeqInclu])
  apply (auto simp: F_Seq T_Seq min_elems_def append_T_imp_tickFree)
     apply(rule_tac x="{}" in exI, rule is_processT5_S3)
      apply (metis (no_types, lifting) T_F elem_min_elems le_approx3 less_list_def min_elems5 subset_eq)
     using Nil_elem_T no_Trace_implies_no_Failure apply fastforce
       apply (metis (no_types, lifting) less_self nonTickFree_n_frontTickFree process_charn)  
     apply (metis (no_types, opaque_lifting) D_T le_approx2T process_charn)
  by (metis (no_types, lifting) less_self nonTickFree_n_frontTickFree process_charn)  

lemma mono_Seq[simp] : "P ⊑ Q ⟹ (P ❙; S) ⊑ (Q ❙; S)"
by (auto simp: le_approx_def mono_Seq_D11 mono_Seq_D12 mono_Seq_D13)

lemma mono_Seq_D21:  
"P ⊑ Q ⟹ 𝒟 (S ❙; Q) ⊆ 𝒟 (S ❙; P)"
  apply(auto simp: D_Seq)
  using le_approx1 by blast

lemma mono_Seq_D22: 
assumes ordered: "P ⊑ Q"
shows   "(∀ s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; P) s = Ra (S ❙; Q) s)"
proof -
  have mono_SEQI2a:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; Q) s ⊆ Ra (S ❙; P) s"
    apply(simp add: Ra_def D_Seq F_Seq)
    by(use le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q] in auto) 
  have mono_SEQI2b:"P ⊑ Q ⟹ ∀s. s ∉ 𝒟 (S ❙; P) ⟶ Ra (S ❙; P) s ⊆ Ra (S ❙; Q) s"
    apply(simp add: Ra_def D_Seq F_Seq)
    apply(insert le_approx_lemma_F[of P Q] le_approx_lemma_T[of P Q] 
            le_approx1[of P Q] le_approx2T[of P Q], auto) 
    using le_approx2 by fastforce+
  show ?thesis 
    using ordered mono_SEQI2a mono_SEQI2b by(blast)
qed

lemma mono_Seq_D23 : 
assumes ordered: "P ⊑ Q"
shows       "min_elems (𝒟 (S ❙; P)) ⊆ 𝒯 (S ❙; Q)"
  apply (insert ordered, frule le_approx3, auto simp: D_Seq T_Seq min_elems_def)
     apply (metis (no_types, lifting) D_imp_front_tickFree Nil_elem_T append.assoc below_refl 
            front_tickFree_charn less_self min_elems2 no_Trace_implies_no_Failure)
   apply (simp add: append_T_imp_tickFree)
  by (metis (no_types, lifting) append.assoc is_processT less_self nonTickFree_n_frontTickFree)

lemma mono_Seq_sym[simp] : "P ⊑ Q ⟹ (S ❙; P) ⊑ (S ❙; Q)"
by (auto simp: le_approx_def mono_Seq_D21 mono_Seq_D22 mono_Seq_D23)

lemma chain_Seq1: "chain Y ⟹ chain (λi. Y i ❙; S)"
  by(simp add: chain_def) 

lemma chain_Seq2: "chain Y ⟹ chain (λi. S ❙; Y i)"
  by(simp add: chain_def)  

lemma limproc_Seq_D1: "chain Y ⟹ 𝒟 (lim_proc (range Y) ❙; S) = 𝒟 (lim_proc (range (λi. Y i ❙; S)))"
  apply(auto simp:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq1)
  by (metis ND_F_dir2' append_single_T_imp_tickFree is_processT is_ub_thelub)
  

lemma limproc_Seq_F1: "chain Y ⟹ ℱ (lim_proc (range Y) ❙; S) = ℱ (lim_proc (range (λi. Y i ❙; S)))"
  apply(auto simp add:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq1)
  proof (auto, goal_cases)
    case (1 a b x y)
    then show ?case
      apply (erule_tac x=x in allE, elim disjE exE, auto simp add: is_processT7 is_processT8_S) 
      apply (erule_tac x=t1 in allE, erule_tac x=t2 in allE) 
      by (metis ND_F_dir2' append_single_T_imp_tickFree is_processT is_ub_thelub)
  next
    case (2 a b x)
    assume A1:"a ∉ 𝒟 (Y x)"
      and  A3:"∀t1 t2. a = t1 @ t2 ⟶ (∃x. t1 @ [tick] ∉ 𝒯 (Y x)) ∨ (t2, b) ∉ ℱ S"
      and  B: "∀x. (a, insert tick b) ∈ ℱ (Y x) ∧ tickFree a ∨ 
                   (∃t1 t2. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y x) ∧ (t2, b) ∈ ℱ S) ∨
                   a ∈ 𝒟 (Y x)"
      and  C:"chain Y" 
    have E:"¬ tickFree a ⟹ False"
      proof -
        assume F:"¬ tickFree a"
        from A obtain f 
          where D:"f = (λt2. {n. ∃t1. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y n) ∧ (t2, b) ∈ ℱ S}
                           ∪ {n. ∃t1. a = t1 @ t2 ∧ t1 ∈ 𝒟 (Y n) ∧ tickFree t1 ∧ front_tickFree t2})"
          by simp
        with B F have "∀n. n ∈ (⋃x∈{t. ∃t1. a = t1 @ t}. f x)"  
                      (is "∀n. n ∈ ?S f") using NF_ND
          by (smt (verit, best) A1 A3 C ND_F_dir2' append_single_T_imp_tickFree is_processT is_ub_thelub) 
        hence "infinite (?S f)" by (simp add: Sup_set_def)
        then obtain t2 where E:"t2∈{t. ∃t1. a = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
        { assume E1:"infinite{n. ∃t1. a = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 (Y n) ∧ (t2, b) ∈ ℱ S}" 
                     (is "infinite ?E1")
          with E obtain t1 where F:"a = t1 @ t2 ∧ (t2, b) ∈ ℱ S" using D not_finite_existsD by blast
          with A3 obtain m where G:"t1@ [tick] ∉ 𝒯 (Y m)" by blast
          with E1 obtain n where "n ≥ m ∧ n ∈ ?E1" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
          with D have "n ≥ m ∧ t1@ [tick] ∈ 𝒯 (Y n)" by (simp add: F)
          with G C have False using le_approx_lemma_T chain_mono by blast
        } note E1 = this
        { assume E2:"infinite{n. ∃t1. a = t1 @ t2 ∧ t1 ∈ 𝒟 (Y n) ∧ tickFree t1 ∧ front_tickFree t2}" 
                    (is "infinite ?E2")
          with E obtain t1 where F:"a = t1 @ t2 ∧ tickFree t1 ∧ front_tickFree t2" 
            using D not_finite_existsD by blast
          with A1 obtain m where G:"t1 ∉ 𝒟 (Y m)" using is_processT7_S by blast
          with E2 obtain n where "n ≥ m ∧ n ∈ ?E2" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
          with D have "n ≥ m ∧ t1 ∈ 𝒟 (Y n)" by (simp add: F)
          with G C have False using le_approx1 chain_mono by blast
        } note E2 = this      
        from D E E1 E2 show False by blast
      qed
    from E show "tickFree a" by blast
  qed

lemma cont_left_D_Seq : "chain Y ⟹ ((⨆ i. Y i) ❙; S) = (⨆ i. (Y i ❙; S))"
  by (simp add: Process_eq_spec chain_Seq1 limproc_Seq_D1 limproc_Seq_F1 limproc_is_thelub)

lemma limproc_Seq_D2: "chain Y ⟹ 𝒟 (S ❙; lim_proc (range Y)) = 𝒟 (lim_proc (range (λi. S ❙; Y i )))"
  apply(auto simp add:Process_eq_spec D_Seq F_Seq F_LUB D_LUB T_LUB chain_Seq2)
proof -
  fix x
  assume B: "∀n. ∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y n)"
  and C: "chain Y"
  from A obtain f where D:"f = (λt2. {n. ∃t1. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ t2 ∈ 𝒟 (Y n)})"
    by simp
  with B have "∀n. n ∈ (⋃x∈{t. ∃t1. x = t1 @ t}. f x)" (is "∀n. n ∈ ?S f") by fastforce
  hence "infinite (?S f)" by (simp add: Sup_set_def)
  then obtain t2 where E:"t2∈{t. ∃t1. x = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
  then obtain t1 where F:"x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S" using D not_finite_existsD by blast
  thus "∃t1 t2. x = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (∀x. t2 ∈ 𝒟 (Y x))" 
    apply (rule_tac x = t1 in exI, rule_tac x = t2 in exI)
  proof (rule ccontr, simp)
    assume ‹∃m. t2 ∉ 𝒟 (Y m)›
    then obtain m where G: ‹t2 ∉ 𝒟 (Y m)› ..
    with E obtain n where "n ≥ m ∧ n ∈ (f t2)" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
    with D have "n ≥ m ∧ t2 ∈ 𝒟 (Y n)" by blast 
    with G C show False using le_approx1 po_class.chain_mono by blast
  qed
qed

      

lemma limproc_Seq_F2: 
  "chain Y ⟹ ℱ (S ❙; lim_proc (range Y)) = ℱ (lim_proc (range (λi. S ❙; Y i )))"
  apply(auto simp:Process_eq_spec D_Seq F_Seq T_Seq F_LUB D_LUB D_LUB_2 T_LUB T_LUB_2 chain_Seq2 del:conjI)
     apply(auto)[3]
proof (goal_cases)
  fix s X
  assume A:"∀t1. t1 @ [tick] ∈ 𝒯 S ⟶ (∀t2. s = t1 @ t2 ⟶ (∃m. (t2, X) ∉ ℱ (Y m)))"
  and B: "∀n. ∃t1 t2. s = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n)"
  and C: "chain Y"
  from B have D:"∀n. (∃t1 t2. s = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n))" by (meson NF_ND)
  from A obtain f where D:"f = (λt2. {n. ∃t1. s = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S ∧ (t2, X) ∈ ℱ (Y n)})"
    by simp
  with D have "∀n. n ∈ (⋃x∈{t. ∃t1. s = t1 @ t}. f x)" using B NF_ND by fastforce
  hence "infinite (⋃x∈{t. ∃t1. s = t1 @ t}. f x)" by (simp add: Sup_set_def)
  then obtain t2 where E:"t2∈{t. ∃t1. s = t1 @ t} ∧ infinite (f t2)" using suffixes_fin by blast
  then obtain t1 where F:"s = t1 @ t2 ∧ t1 @ [tick] ∈ 𝒯 S" using D not_finite_existsD by blast
  from A F obtain m where G:"(t2, X) ∉ ℱ (Y m)" by blast
  with E obtain n where "n ≥ m ∧ n ∈ (f t2)" by (meson finite_nat_set_iff_bounded_le nat_le_linear)
  with D have "n ≥ m ∧ (t2, X) ∈ ℱ (Y n)" by blast
  with G C have False using is_processT8 po_class.chain_mono proc_ord2a by blast
  thus ‹(s, insert tick X) ∈ ℱ S ∧ tickFree s› by simp
qed

lemma cont_right_D_Seq : "chain Y ⟹ (S ❙; (⨆ i. Y i)) = (⨆ i. (S ❙; Y i))"
  by (simp add: Process_eq_spec chain_Seq2 limproc_Seq_D2 limproc_Seq_F2 limproc_is_thelub)

lemma Seq_cont[simp]:
assumes f:"cont f"
and     g:"cont g"
shows     "cont (λx. f x ❙; g x)"
proof -
  have A : "⋀x. cont g ⟹ cont (λy. y ❙; g x)"
    apply (rule contI2, rule monofunI)
     apply (auto)
    by (simp add: cont_left_D_Seq)
  have B : "⋀y. cont g ⟹ cont (λx. y ❙; g x)"
    apply (rule_tac c="(λ x. y ❙; x)" in cont_compose)
     apply (rule contI2,rule monofunI)
    by (auto simp add: chain_Seq2 cont_right_D_Seq)
  show ?thesis using f g 
    apply(rule_tac f="(λx. (λ f. f ❙; g x))" in cont_apply)
      by(auto intro:contI2 monofunI simp:A B)
qed

end