Theory Synchronization_Product

(*<*)
―‹ ********************************************************************
 * 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       : Synchronization product
 *
 * 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 Synchronization Product ›

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

section‹Basic Concepts›

fun setinterleaving :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k × ('a, 'r) refusal⇩p⇩t⇩i⇩c⇩k × ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k set›
  where

si_empty1: ‹setinterleaving ([], X, []) = {[]}›
| si_empty2: ‹setinterleaving ([], X, y # t) = 
               (if y ∈ X
                then {} 
                else {z. ∃u. z = y # u ∧ u ∈ setinterleaving ([], X, t)})›
| si_empty3: ‹setinterleaving ((x # s), X, []) = 
               (if x ∈ X 
                then {} 
                else {z. ∃ u. z = x # u ∧ u ∈ setinterleaving (s, X, [])})›

| si_neq   : ‹setinterleaving (x # s, X, y # t) = 
               (if x ∈ X 
                then if y ∈ X
                     then if x = y
                          then {z. ∃u. z = x # u ∧ u ∈ setinterleaving (s, X, t)}
                          else {}
                     else {z. ∃u. z = y # u ∧ u ∈ setinterleaving (x # s, X, t)}
                else if y ∉ X
                     then {z. ∃u. z = x # u ∧ u ∈ setinterleaving (s, X, y # t)} ∪
                          {z. ∃u. z = y # u ∧ u ∈ setinterleaving (x # s, X, t)} 
                     else {z. ∃u. z = x # u ∧ u ∈ setinterleaving (s, X, y # t)})›

fun setinterleavingList :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k × ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set × ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k list›
  where

si_empty1l: ‹setinterleavingList ([], X, []) = [[]]›
| si_empty2l: ‹setinterleavingList ([], X, (y # t)) = 
               (if y ∈ X
                then [] 
                else [y # z. z ← setinterleavingList ([], X, t)])›
| si_empty3l: ‹setinterleavingList (x # s, X, []) = 
               (if x ∈ X
                then [] 
                else [x # z. z ← setinterleavingList (s, X, [])])›

| si_neql   : ‹setinterleavingList ((x # s), X, (y # t)) = 
               (if x ∈ X 
                then if y ∈ X
                     then if x = y
                          then [x # z. z ← setinterleavingList (s, X, t)]
                          else []
                     else [y # z. z ← setinterleavingList (x # s, X, t)]
                else if y ∉ X
                     then [x # z. z ← setinterleavingList (s, X, y # t)] @
                          [y # z. z ← setinterleavingList (x # s, X, t)]
                     else [x # z. z ← setinterleavingList (s, X, y # t)])›


lemma finiteSetinterleavingList: "finite (set (setinterleavingList (s, X, t)))" 
  by auto

lemma setinterleaving_sym : ‹setinterleaving (s, X, t) = setinterleaving(t, X, s)›
  by (rule setinterleaving.induct[of ‹λ(s, X, t). setinterleaving (s, X, t) =
           setinterleaving (t, X, s)› ‹(s, X, t)›, simplified]) auto



abbreviation "setinterleaves_syntax"  ("_ setinterleaves '(()'(_, _')(), _')" [60,0,0,0]70)
  where      "u setinterleaves ((s, t), X) == (u ∈ setinterleaving(s, X, t))"


section‹Consequences›

lemma emptyLeftProperty: ‹s setinterleaves (([], t :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k), A) ⟹ s = t›
  by (induct ‹([] :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k, A, t)› arbitrary: s t rule: setinterleaving.induct)
    (auto split: if_split_asm)

lemma emptyRightProperty: ‹s setinterleaves ((t, []), A) ⟹ s = t›
  by (simp add: setinterleaving_sym emptyLeftProperty)

lemma emptyLeftSelf: ‹∀t1. t1 ∈ set t ⟶ t1 ∉ A ⟹ t setinterleaves (([], t), A)›
  by (induct t) auto

lemma empty_setinterleaving : "[] setinterleaves ((t, u), A) ⟹ t = []"  
  by (cases t; cases u) (simp_all split: if_split_asm) 


lemma emptyLeftNonSync: ‹s setinterleaves (([], t), A) ⟹ ∀a ∈ set t. a ∉ A›
proof (induct t arbitrary: s)
  case Nil
  show ?case by simp
next
  case (Cons a t)
  thus ?case by (cases s; simp split: if_split_asm)
qed


lemma ftf_Sync1: ‹⟦a ∉ set u; a ∉ set t; s setinterleaves ((t, u), A)⟧ ⟹ a ∉ set s›
  by (induct ‹(t, A, u)› arbitrary: s t u rule: setinterleaving.induct)
    (auto intro: emptyLeftProperty emptyRightProperty split: if_split_asm)


lemma addNonSync:
  ‹sa setinterleaves ((t, u), A) ⟹ y1 ∉ A ⟹
   (sa @ [y1]) setinterleaves ((t @ [y1], u), A) ∧ (sa @ [y1]) setinterleaves ((t, u @ [y1]), A)›
  by (induct ‹(t, A, u)› arbitrary: sa t u rule: setinterleaving.induct)
    (auto split: if_split_asm)


lemma addSync:‹sa setinterleaves ((t, u), A) ⟹ y1 ∈ A ⟹
               (sa @ [y1]) setinterleaves ((t @ [y1], u @ [y1]), A)›
  by (induct ‹(t, A, u)› arbitrary: sa t u rule: setinterleaving.induct)
    (auto split: if_split_asm)


lemma doubleReverse: ‹s1 setinterleaves ((t, u), A) ⟹ rev s1 setinterleaves ((rev t, rev u), A)›
  by (induct ‹(t, A, u)› arbitrary: s1 t u rule: setinterleaving.induct; simp split: if_split_asm)
    (metis [[metis_verbose = false]] addNonSync addSync rev.simps(2))+


(* from CSP_Laws, better to have it here ? *)
lemma SyncTlEmpty: ‹a setinterleaves (([], u), A) ⟹ tl a setinterleaves (([], tl u), A)›
  by (cases u; cases a) (simp_all split: if_splits)

lemma SyncHd_Tl: 
  ‹a setinterleaves ((t, u), A) ⟹ hd t ∈ A ⟹ hd u ∉ A
    ⟹ hd a = hd u ∧ tl a setinterleaves ((t, tl u), A)›
  by (cases u; cases t) (auto split: if_split_asm)

lemma SyncHdAddEmpty: 
  "(tl a) setinterleaves (([], u), A) ⟹ hd a ∉ A ⟹ a ≠ []
    ⟹ a setinterleaves (([], hd a # u), A)"
  by (cases a) simp_all

lemma SyncHdAdd: 
  "(tl a) setinterleaves ((t, u), A) ⟹ hd a ∉ A ⟹ hd t ∈ A ⟹ a ≠ []
   ⟹ a setinterleaves ((t, hd a # u), A)" 
  by (cases a, simp, cases t, auto) 

lemmas SyncHdAdd1 = SyncHdAdd[of "a # r", simplified] for a r

lemma SyncSameHdTl:
  "a setinterleaves ((t, u), A) ⟹ hd t ∈ A ⟹ hd u ∈ A
   ⟹ hd t = hd u ∧ hd a = hd t ∧ (tl a) setinterleaves ((tl t, tl u), A)"
  by (cases u) (cases t, auto split:if_splits)+

lemma SyncSingleHeadAdd: 
  "a setinterleaves ((t, u), A) ⟹ h ∉ A
    ⟹ (h # a) setinterleaves ((h # t, u), A)"
  by (cases u, auto split:if_splits)

lemma TickLeftSync:
  ‹⟦tick r ∈ A; front_tickFree t; s setinterleaves (([tick r], t :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k), A)⟧ ⟹ s = t ∧ last t = tick r›
  apply (induct ‹([tick r] :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k, A, t)› arbitrary: s t rule: setinterleaving.induct)
   apply (simp_all add: front_tickFree_Cons_iff split: if_split_asm)
  by force (metis distinct.simps(1) distinct_length_2_or_more emptyRightProperty front_tickFree_Nil)


lemma EmptyLeftSync: ‹s setinterleaves (([], t), A) ⟹ s = t ∧ set t ∩ A = {}›
  by (meson Int_emptyI emptyLeftNonSync emptyLeftProperty)

lemma EmptyRightSync: ‹s setinterleaves ((t, []), A) ⟹ s = t ∧ set t ∩ A = {}›
  by (simp add: EmptyLeftSync setinterleaving_sym)


(* lemma event_set: ‹(e::('a, 'r) event⇩p⇩t⇩i⇩c⇩k) ∈ range tick ∪ range ev›
  by (metis UnCI event.exhaust rangeI) *)






lemma ftf_Sync21: ‹a ∈ set u ∧ a ∉ set t ∨ a ∈ set t ∧ a ∉ set u ⟹ a ∈ A ⟹
                   setinterleaving (u, A, t) = {}›
  by (induct ‹(t, A, u)› arbitrary: t u rule: setinterleaving.induct)
    (auto split: if_split_asm)


lemma ftf_Sync32:
  assumes ‹t = t1 @ [tick r]› and ‹u = u1 @ [tick r]› 
    and ‹s setinterleaves ((t, u), range tick ∪ ev ` A)›
  shows ‹∃s1. s1 setinterleaves ((t1, u1), range tick ∪ ev ` A) ∧ s = s1 @ [tick r]›
proof -
  from assms(1) have b : ‹rev t = tick r # rev t1› by auto
  from assms(2) have a : ‹rev u = tick r # rev u1› by auto
  from assms have ab: ‹(rev s) setinterleaves ((tick r # rev t1, tick r # rev u1), range tick ∪ ev ` A)›
    using doubleReverse by fastforce
  from ab have c: ‹tl (rev s) setinterleaves ((rev t1, rev u1), range tick ∪ ev ` A)› by auto 
  hence d: ‹(rev (tl (rev s))) setinterleaves ((t1,  u1), range tick ∪ ev ` A)›
    using doubleReverse by fastforce
  from ab append_Cons_eq_iff c have ‹rev s = tick r # tl (rev s)› by auto
  with d show ?thesis by blast
qed


lemma SyncWithTick_imp_NTF:
  assumes ‹(s @ [tick r]) setinterleaves ((t, u), range tick ∪ ev ` A)›
    and ‹front_tickFree t› and ‹front_tickFree u›
  shows ‹∃t1 u1. t = t1 @ [tick r] ∧ u = u1 @ [tick r] ∧ s setinterleaves ((t1, u1), range tick ∪ ev ` A)›
proof-
  from assms(1) have a: ‹(tick r # rev s) setinterleaves ((rev t, rev u), range tick ∪ ev ` A)›
    using doubleReverse by fastforce
  from assms(1)[THEN doubleReverse] obtain tt uu where b: ‹t = tt @ [tick r]› ‹u = uu @ [tick r]›
    apply (cases t rule: rev_cases; cases u rule: rev_cases; simp add: image_iff)
    by ((split if_split_asm, safe)+, auto)+ (* ??? *)
  from ftf_Sync32[OF this assms(1)] have ‹s setinterleaves ((tt, uu), range tick ∪ ev ` A)› by blast
  with b show ?thesis by blast
qed 



lemma suffix_tick_le_ftf_imp_eq: ‹front_tickFree t ⟹ s @ [tick r] ≤ t ⟹ s @ [tick r] = t›
  by (metis prefixE append_Nil2 front_tickFree_nonempty_append_imp non_tickFree_tick tickFree_append_iff)




lemma synPrefix: ‹(s @ t) setinterleaves ((ta, u), A) ⟹ ∃t1 u1. t1 ≤ ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)›
proof (induct ‹(ta, A, u)› arbitrary: s t ta u rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  { case (2 y u)
    thus ?case
      by (cases s; simp split: if_split_asm)
        (metis si_empty1 insertI1 nil_le,
          metis (no_types) "2.prems" emptyLeftNonSync emptyLeftProperty
          emptyLeftSelf less_eq_list_def prefix_def set_ConsD)
  } note * = this

  case (3 x ta)
  thus ?case by (metis (full_types) "*" setinterleaving_sym)
next
  case (4 x ta y u)
  show ?case
  proof (cases s)
    show ‹s = [] ⟹ ?case› by (metis si_empty1 insertI1 nil_le)
  next
    fix a s'
    assume ‹s = a # s'›
    consider ‹x ∈ A› ‹y ∈ A› | ‹x ∈ A› ‹y ∉ A› | ‹x ∉ A› ‹y ∈ A› | ‹x ∉ A› ‹y ∉ A› by blast
    thus ?case
    proof cases
      assume ‹x ∈ A› ‹y ∈ A›
      with "4.prems" have ‹x = y› ‹a = y› ‹(s' @ t) setinterleaves ((ta, u), A)›
        by (simp_all add: ‹s = a # s'› split: if_split_asm)
      from "4.hyps"(1)[OF ‹x ∈ A› ‹y ∈ A› ‹x = y› this(3)] obtain t1 u1
        where ‹t1 ≤ ta› ‹u1 ≤ u ∧ s' setinterleaves ((t1, u1), A)› by blast
      hence ‹x # t1 ≤ x # ta ∧ y # u1 ≤ y # u ∧ s setinterleaves ((x # t1, y # u1), A)›
        by (simp add: ‹s = a # s'› ‹x ∈ A› ‹y ∈ A› ‹x = y› ‹a = y›)
      thus ?case by blast
    next
      { fix x y ta u s a s'
        assume ‹x ∈ A› ‹y ∉ A› ‹s = a # s'›
          and prems: ‹(s @ t) setinterleaves ((x # ta, y # u), A)›
        assume hyps: ‹x ∈ A ⟹ y ∉ A ⟹ (s @ t) setinterleaves ((x # ta, u), A) ⟹
                      ∃t1 u1. t1 ≤ x # ta ∧ u1 ≤ u ∧ s setinterleaves ((t1, u1), A)› for s t
        from ‹x ∈ A› ‹y ∉ A› ‹s = a # s'› prems
        have ‹a = y› ‹(s' @ t) setinterleaves ((x # ta, u), A)›
          by (simp_all add: ‹s = a # s'› split: if_split_asm)
        from hyps[OF ‹x ∈ A› ‹y ∉ A› this(2)] obtain t1 u1
          where ‹t1 ≤ x # ta› ‹u1 ≤ u› ‹s' setinterleaves ((t1, u1), A)› by blast
        hence ‹t1 ≤ x # ta ∧ y # u1 ≤ y # u ∧ s setinterleaves ((t1, y # u1), A)›
          by (cases t1; simp add: ‹s = a # s'› ‹y ∉ A› ‹a = y›)
        hence ‹∃t1 u1. t1 ≤ x # ta ∧ u1 ≤ y # u ∧ s setinterleaves ((t1, u1), A)› by blast
      } note * = this

      show ‹?case› if ‹x ∈ A› and ‹y ∉ A›
        using "*"[OF ‹x ∈ A› ‹y ∉ A› ‹s = a # s'› "4.prems" "4.hyps"(2)] by simp

      show ‹?case› if ‹x ∉ A› and ‹y ∈ A›
        by (metis "*"[OF ‹y ∈ A› ‹x ∉ A› ‹s = a # s'›, of u ta]
            "4.hyps"(5) "4.prems" setinterleaving_sym)
    next
      assume ‹x ∉ A› and ‹y ∉ A›
      with "4.prems" have ‹a = x ∧ (s' @ t) setinterleaves ((ta, y # u), A) ∨
                           a = y ∧ (s' @ t) setinterleaves ((x # ta, u), A)› (is ‹?c ∨ _›)
        by (simp add: ‹s = a # s'› split: if_split_asm)
      thus ?case 
      proof (elim disjE conjE)
        assume ‹a = x› ‹(s' @ t) setinterleaves ((ta, y # u), A)›
        from "4.hyps"(3)[OF ‹x ∉ A› ‹y ∉ A› this(2)] obtain t1 u1
          where ‹t1 ≤ ta› ‹u1 ≤ y # u› ‹s' setinterleaves ((t1, u1), A)› by blast
        hence ‹x # t1 ≤ x # ta ∧ u1 ≤ y # u ∧ s setinterleaves ((x # t1, u1), A)›
          by (cases u1; simp add: ‹s = a # s'› ‹a = x› ‹x ∉ A›)
        thus ?case by blast
      next
        assume ‹a = y› ‹(s' @ t) setinterleaves ((x # ta, u), A)›
        from "4.hyps"(4)[OF ‹x ∉ A› ‹y ∉ A› this(2)] obtain t1 u1
          where ‹t1 ≤ x # ta› ‹u1 ≤ u› ‹s' setinterleaves ((t1, u1), A)› by blast
        hence ‹t1 ≤ x # ta ∧ y # u1 ≤ y # u ∧ s setinterleaves ((t1, y # u1), A)›
          by (cases t1; simp add: ‹s = a # s'› ‹a = y› ‹y ∉ A›)
        thus ?case by blast
      qed
    qed
  qed
qed


lemma interleave_less_left :
  ‹s setinterleaves ((t, u), A) ⟹ t1 < t ⟹
   ∃u1 s1. u1 ≤ u ∧ s1 < s ∧ s1 setinterleaves ((t1, u1), A)›
proof (induct ‹(t, A, u)› arbitrary: s t u t1 rule: setinterleaving.induct)
  case 1
  thus ?case by simp
next
  case (2 y u)
  hence False by simp
  thus ?case by simp
next
  case (3 x t)
  thus ?case by (metis (no_types, lifting) emptyRightProperty less_eq_list_def prefix_def
        nil_le2 order_less_imp_le synPrefix)
next
  case (4 x t y u)
  show ?case
  proof (cases ‹t1 = []›)
    show ‹t1 = [] ⟹ ?case›
      by (metis "4.prems"(1) si_empty1 empty_setinterleaving insertI1
          list.distinct(1) nil_le order_le_imp_less_or_eq)
  next
    assume ‹t1 ≠ []›
    with ‹t1 < x # t› obtain t1' where ‹t1 = x # t1'› ‹t1' < t›
      by (metis hd_append2 less_eq_list_def prefix_def less_list_def less_tail list.exhaust_sel list.sel(1, 3))
    consider ‹x ∈ A› ‹y ∈ A› | ‹x ∈ A› ‹y ∉ A› | ‹x ∉ A› ‹y ∈ A› | ‹x ∉ A› ‹y ∉ A› by blast
    thus ?case
    proof cases
      assume ‹x ∈ A› ‹y ∈ A›
      with "4.prems"(1) obtain s' where ‹x = y› ‹s = y # s'› ‹s' setinterleaves ((t, u), A)›
        by (simp split: if_split_asm) blast
      from "4.hyps"(1)[OF ‹x ∈ A› ‹y ∈ A› ‹x = y› this(3) ‹t1' < t›]
      obtain u1 s1 where ‹u1 ≤ u› ‹s1 < s'› ‹s1 setinterleaves ((t1', u1), A)› by blast
      hence ‹y # u1 ≤ y # u ∧ y # s1 < s ∧ (y # s1) setinterleaves ((t1, y # u1), A)›
        by (simp add: ‹t1 = x # t1'› ‹x = y› ‹y ∈ A› ‹s = y # s'›)
      thus ?case by blast
    next
      assume ‹x ∈ A› ‹y ∉ A›
      with "4.prems"(1) obtain s' where ‹s = y # s'› ‹s' setinterleaves ((x # t, u), A)›
        by (simp split: if_split_asm) blast
      from "4.hyps"(2)[OF ‹x ∈ A› ‹y ∉ A› this(2) less_cons[THEN iffD2, OF ‹t1' < t›]]
      obtain u1 s1 where ‹u1 ≤ u› ‹s1 < s'› ‹s1 setinterleaves ((x # t1', u1), A)› by blast
      hence ‹y # u1 ≤ y # u ∧ y # s1 < s ∧ (y # s1) setinterleaves ((t1, y # u1), A)›
        by (simp add: ‹t1 = x # t1'› ‹y ∉ A› ‹s = y # s'›)
      thus ?case by blast
    next
      assume ‹x ∉ A› ‹y ∈ A›
      with "4.prems"(1) obtain s' where ‹s = x # s'› ‹s' setinterleaves ((t, y # u), A)›
        by (simp split: if_split_asm) blast
      from "4.hyps"(5)[OF ‹x ∉ A› _ this(2) ‹t1' < t›] ‹y ∈ A›
      obtain u1 s1 where ‹u1 ≤ y # u› ‹s1 < s'› ‹s1 setinterleaves ((t1', u1), A)› by blast
      hence ‹u1 ≤ y # u ∧ x # s1 < s ∧ (x # s1) setinterleaves ((t1, u1), A)›
        by (cases u1; simp add: ‹t1 = x # t1'› ‹x ∉ A› ‹s = x # s'›)
      thus ?case by blast
    next
      assume ‹x ∉ A› ‹y ∉ A›
      with "4.prems"(1) obtain s'
        where ‹s = x # s' ∧ s' setinterleaves ((t, y # u), A) ∨
               s = y # s' ∧ s' setinterleaves ((x # t, u), A)›
        by (simp split: if_split_asm) blast
      thus ?case
      proof (elim disjE conjE)
        assume ‹s = x # s'› ‹s' setinterleaves ((t, y # u), A)› 
        from "4.hyps"(3)[OF ‹x ∉ A› ‹y ∉ A› this(2) ‹t1' < t›]
        obtain u1 s1 where ‹u1 ≤ y # u› ‹s1 < s'› ‹s1 setinterleaves ((t1', u1), A)› by blast
        hence ‹u1 ≤ y # u ∧ x # s1 < s ∧ (x # s1) setinterleaves ((t1, u1), A)›
          by (cases u1; simp add: ‹t1 = x # t1'› ‹x ∉ A› ‹s = x # s'›)
        thus ?case by blast
      next
        assume ‹s = y # s'› ‹s' setinterleaves ((x # t, u), A)› 
        from "4.hyps"(4)[OF ‹x ∉ A› ‹y ∉ A› this(2) less_cons[THEN iffD2, OF ‹t1' < t›]]
        obtain u1 s1 where ‹u1 ≤ u› ‹s1 < s'› ‹s1 setinterleaves ((x # t1', u1), A)› by blast
        hence ‹y # u1 ≤ y # u ∧ y # s1 < s ∧ (y # s1) setinterleaves ((t1, y # u1), A)›
          by (simp add: ‹t1 = x # t1'› ‹y ∉ A› ‹s = y # s'›)
        thus ?case by blast
      qed
    qed
  qed
qed

lemma interleave_less_right :
  ‹s setinterleaves ((t, u), A) ⟹ u1 < u ⟹
   ∃t1 s1. t1 ≤ t ∧ s1 < s ∧ s1 setinterleaves ((t1, u1), A)›
  by (metis (no_types) interleave_less_left setinterleaving_sym)


lemma interleave_le_left :
  ‹s setinterleaves ((t, u), A) ⟹ t1 ≤ t ⟹
   ∃u1 s1. u1 ≤ u ∧ s1 ≤ s ∧ s1 setinterleaves ((t1, u1), A)›
  by (metis interleave_less_left order_le_less)

lemma interleave_le_right :
  ‹s setinterleaves ((t, u), A) ⟹ u1 ≤ u ⟹
   ∃t1 s1. t1 ≤ t ∧ s1 ≤ s ∧ s1 setinterleaves ((t1, u1), A)›
  by (metis (no_types) interleave_le_left setinterleaving_sym)

(*   assumes ‹(s @ [tick r]) setinterleaves ((t, u), range tick ∪ ev ` A)›
      and ‹t ∈ 𝒯 P› and ‹u ∈ 𝒯 Q›
    shows ‹∃t_P t_Q X_P X_Q. (t_P, X_P) ∈ ℱ P ∧ (t_Q, X_Q) ∈ ℱ Q ∧
                             s setinterleaves ((t_P, t_Q), range tick ∪ ev ` A) ∧
                             X_P - {tick r} = (X_P ∪ X_Q) ∩ range tick ∪ ev ` A ∪ X_P ∩ X_Q›
 *)


lemma SyncWithTick_imp_NTF1:
  assumes ‹(s @ [tick r]) setinterleaves ((t, u), range tick ∪ ev ` A)›
    and ‹t ∈ 𝒯 P› and ‹u ∈ 𝒯 Q›
  shows ‹∃t u X_P X_Q. (t, X_P) ∈ ℱ P ∧ (u, X_Q) ∈ ℱ Q ∧
                         s setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                         X - {tick r} = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
proof -
  from SyncWithTick_imp_NTF[OF assms(1)] assms(2, 3) is_processT2_TR
  obtain t1 u1 
    where * : ‹t = t1 @ [tick r]› ‹u = u1 @ [tick r]›
      ‹s setinterleaves ((t1, u1), range tick ∪ ev ` A)› by blast
  from "*"(1, 2) assms(2, 3) have E: ‹(t1, X - {tick r}) ∈ ℱ P› ‹(u1, X - {tick r}) ∈ ℱ Q›
    by (simp_all add: T_F process_charn)
  with "*"(3) show ?thesis by blast
qed


lemma interleave_size: 
  ‹s setinterleaves ((t, u), C) ⟹ length s = length t + length u - length (filter (λx. x ∈ C) t)›
  apply (induct ‹(t, C, u)› arbitrary: t u s rule: setinterleaving.induct)
     apply (simp; fail)
    apply (metis add_diff_cancel_left' emptyLeftProperty filter.simps(1))
   apply (metis add_diff_cancel_right' emptyLeftNonSync
      emptyRightProperty filter_False setinterleaving_sym)
  by (simp split: if_split_asm;
      metis (no_types) [[metis_verbose = false]] Suc_diff_le add_Suc_right
      length_Cons length_filter_le trans_le_add1)

lemma interleave_eq_size: 
  ‹s setinterleaves ((t, u), C) ⟹ s' setinterleaves ((t, u), C) ⟹ length s = length s'›
  by (simp add: interleave_size)


lemma ftf_Sync:
  assumes ‹front_tickFree t› and ‹front_tickFree u›
    and ‹s setinterleaves ((t, u), range tick ∪ ev ` A)›
  shows ‹front_tickFree s›
proof (cases ‹tickFree s›)
  show ‹tickFree s ⟹ front_tickFree s› by (fact tickFree_imp_front_tickFree)
next
  assume ‹¬ tickFree s›
  hence ‹∃s1 s2 r. tickFree s1 ∧ s = (s1 @ [tick r]) @ s2›
  proof (induct s rule: rev_induct)
    case Nil thus ?case by simp
  next
    case (snoc a s)
    from ‹¬ tickFree (s @ [a])› consider r where ‹tickFree s› ‹a = tick r› | ‹¬ tickFree s›
      by (auto simp add: tickFree_def)
    thus ?case
    proof cases
      show ‹tickFree s ⟹ a = tick r ⟹
            ∃s1 s2 r. tickFree s1 ∧ s @ [a] = (s1 @ [tick r]) @ s2› for r by blast
    next
      assume ‹¬ tickFree s›
      with snoc.hyps obtain s1 s2 r where ‹tickFree s1› ‹s = (s1 @ [tick r]) @ s2› by blast
      hence ‹tickFree s1 ∧ s @ [a] = (s1 @ [tick r]) @ (s2 @ [a])› by simp
      thus ?case by blast
    qed
  qed
  then obtain s1 s2 r where ‹tickFree s1› ‹s = (s1 @ [tick r]) @ s2› by blast
  from synPrefix[of ‹s1 @ [tick r]› s2, folded ‹s = (s1 @ [tick r]) @ s2›, OF assms(3)]
  obtain t1 u1
    where * : ‹t1 ≤ t› ‹u1 ≤ u›
      ‹(s1 @ [tick r]) setinterleaves ((t1, u1), range tick ∪ ev ` A)› by blast
  from "*"(1, 2) assms(1, 2) have ‹front_tickFree t1› ‹front_tickFree u1›
    by (metis prefixE front_tickFree_dw_closed)+
  from SyncWithTick_imp_NTF[OF "*"(3) this]
  obtain t2 u2 where ‹t1 = t2 @ [tick r]› ‹u1 = u2 @ [tick r]›
    ‹s1 setinterleaves ((t2, u2), range tick ∪ ev ` A)› by blast
  from ‹t1 ≤ t› ‹t1 = t2 @ [tick r]› assms(1) suffix_tick_le_ftf_imp_eq have ‹t = t1› by metis
  from ‹u1 ≤ u› ‹u1 = u2 @ [tick r]› assms(2) suffix_tick_le_ftf_imp_eq have ‹u = u1› by metis
  have ‹(s1 @ [tick r]) setinterleaves ((t, u), range tick ∪ ev ` A)›
    by (simp add: "*"(3) ‹t = t1› ‹u = u1›)
  with assms(3) interleave_eq_size have ‹length s = length (s1 @ [tick r])› by blast
  with ‹s = (s1 @ [tick r]) @ s2› have ‹s = s1 @ [tick r]› by simp
  thus ‹front_tickFree s› by (simp add: ‹tickFree s1› front_tickFree_append)
qed



section‹The Sync Operator Definition›

lift_definition Sync :: ‹[('a, 'r) process⇩p⇩t⇩i⇩c⇩k, 'a set, ('a, 'r) process⇩p⇩t⇩i⇩c⇩k] ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  (‹(3(_ ⟦_⟧/ _))› [70, 0, 71] 70)
  is ‹λP A Q. ({(s, R). ∃t u X Y. (t, X) ∈ ℱ P ∧ (u, Y) ∈ ℱ Q ∧
                                  s setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                                  R = (X ∪ Y) ∩ (range tick ∪ ev ` A) ∪ X ∩ Y} ∪
               {(s, R). ∃t u r v. ftF v ∧ (tF r ∨ v = []) ∧ s = r @ v ∧
                                  r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                                  (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)},
               {s. ∃t u r v. ftF v ∧ (tF r ∨ v = []) ∧ s = r @ v ∧
                             r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                             (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)})›
proof -
  show ‹?thesis P A Q› (is ‹is_process(?f, ?d P Q)›) for P Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and A
  proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI impI allI)
    show ‹([], {}) ∈ ?f›
      by simp (metis Int_commute Int_empty_right si_empty1
          Un_empty insert_iff is_processT1) 
  next 
    show ‹(s, X) ∈ ?f ⟹ ftF s› for s X
      apply (simp, elim disjE)
      using F_imp_front_tickFree ftf_Sync apply blast
      by (metis D_imp_front_tickFree T_imp_front_tickFree append.right_neutral front_tickFree_append ftf_Sync)

  next
    fix s t assume ‹(s @ t, {}) ∈ ?f›
    then consider (fail) t_P t_Q X_P X_Q where 
      ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
      ‹(s @ t) setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
      ‹(X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q = {}›
    | (div) t' u r v where ‹ftF v› ‹tF r ∨ v = []› ‹s @ t = r @ v›
      ‹r setinterleaves ((t', u), range tick ∪ ev ` A)›
      ‹t' ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t' ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
      (* TODO: break this smt *)
      by (smt (verit, ccfv_SIG) Un_iff case_prod_conv mem_Collect_eq)
    thus ‹(s, {}) ∈ ?f›
    proof cases
      case fail
      from fail(3)[THEN synPrefix] show ‹(s, {}) ∈ ?f›
        apply (elim exE conjE)
        apply (drule fail(1, 2)[THEN F_T, THEN is_processT3_TR])+
        by simp (metis Int_empty_left T_F Un_absorb)
    next
      case div
      show ‹(s, {}) ∈ ?f›
      proof (cases ‹length r ≤ length s›)
        assume ‹length r ≤ length s›
        with div have ‹front_tickFree (take (length s - length r) v) ∧
                       (tickFree r ∨ take (length s - length r) v = []) ∧
                       s = r @ take (length s - length r) v›
          by simp (metis append_eq_conv_conj append_take_drop_id
              front_tickFree_dw_closed take_all_iff take_append)
        show ‹(s, {}) ∈ ?f› by simp (use ‹?this› div in blast)
      next
        assume ‹¬ length r ≤ length s›
        with div obtain r' where ‹r = s @ r'›
          by (metis append_eq_append_conv_if append_take_drop_id)
        from div ‹r = s @ r'› synPrefix obtain t1 u1
          where ** : ‹t1 ≤ t'› ‹u1 ≤ u›
            ‹s setinterleaves ((t1, u1), range tick ∪ ev ` A)› by metis
        from div "**"(1, 2) D_T is_processT3_TR
        have ‹t1 ∈ 𝒯 P ∧ u1 ∈ 𝒯 Q ∨ t1 ∈ 𝒯 Q ∧ u1 ∈ 𝒯 P› by blast
        thus ‹(s, {}) ∈ ?f›
          by simp (metis "**"(3) Int_Un_eq(1) T_F setinterleaving_sym sup_bot.right_neutral)
      qed
    qed
  next
    fix s X Y
    assume ‹(s, Y) ∈ ?f ∧ X ⊆ Y›
    then consider ‹s ∈ ?d P Q›
      | (fail) s_P s_Q X_P X_Q
      where ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
        ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` A)›
        ‹Y = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
      by simp blast
    thus ‹(s, X) ∈ ?f›
    proof cases
      show ‹s ∈ ?d P Q ⟹ (s, X) ∈ ?f› by blast
    next
      case fail
      have ‹(s_P, X_P ∩ X) ∈ ℱ P› using fail(1) by (meson inf_le1 process_charn)
      moreover have ‹(s_Q, X_Q ∩ X) ∈ ℱ Q› using fail(2) by (meson inf_le1 process_charn)
      moreover have ‹X = (X_P ∩ X ∪ X_Q ∩ X) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X ∩ (X_Q ∩ X)›
        by (subst ‹(s, Y) ∈ ?f ∧ X ⊆ Y›[THEN conjunct2, THEN Int_absorb1, symmetric])
          (use fail(4) in blast)
      ultimately show ‹(s, X) ∈ ?f› using fail(3) by simp blast
    qed
  next
    fix s X Y
    assume ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)›
    then consider ‹s ∈ ?d P Q› | ‹(s, X) ∈ ?f ∧ s ∉ ?d P Q› by linarith
    thus ‹(s, X ∪ Y) ∈ ?f›
    proof cases
      show ‹s ∈ ?d P Q ⟹ (s, X ∪ Y) ∈ ?f› by blast
    next
      assume ‹(s, X) ∈ ?f ∧ s ∉ ?d P Q›
      then obtain s_P X_P s_Q X_Q
        where assms : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
          ‹s setinterleaves ((s_P, s_Q), range tick ∪ ev ` A)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
        by simp blast
      have assms4 : ‹c ∈ Y ⟹ ((s @ [c]) setinterleaves ((t1, u1), range tick ∪ ev ` A) ⟹
                     ((t1, {}) ∈ ℱ P ⟶ (u1, {}) ∉ ℱ Q) ∧
                     ((t1, {}) ∈ ℱ Q ⟶ (u1, {}) ∉ ℱ P))› for c t1 u1
        using ‹(s, X) ∈ ?f ∧ s ∉ ?d P Q›
          ‹(s, X) ∈ ?f ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ?f)› 
        by simp (metis (no_types, lifting) Int_empty_left setinterleaving_sym sup_bot.right_neutral)
      show ‹(s, X ∪ Y) ∈ ?f›
      proof-
        define Y1 Y2 where Y1_def: ‹Y1 ≡ Y ∩ (range tick ∪ ev ` A)›
          and Y2_def: ‹Y2 ≡ Y - (range tick ∪ ev ` A)›
        hence ‹Y1 ∪ Y2 = Y› by blast
        have $ : ‹∀z∈Y1. (s_P @ [z], {}) ∉ ℱ P ∨ (s_Q @ [z], {}) ∉ ℱ Q›
        proof (rule ccontr)
          assume ‹¬ (∀z∈Y1. (s_P @ [z], {}) ∉ ℱ P ∨ (s_Q @ [z], {}) ∉ ℱ Q)›
          then obtain z1 where * : ‹z1 ∈ Y1› ‹(s_P @ [z1], {}) ∈ ℱ P› ‹(s_Q @ [z1], {}) ∈ ℱ Q› by blast
          have ‹(s @ [z1]) setinterleaves ((s_P @ [z1], s_Q @ [z1]), range tick ∪ ev ` A)›
            by (metis "*"(1) IntD2 Y1_def addSync assms(3))
          with "*" assms4 show False by (metis IntD1 Y1_def)
        qed
        define Z1 Z2 where Z1_def: ‹Z1 ≡ Y1 ∩ {z. (s_P @ [z], {}) ∉ ℱ P}›
          and Z2_def: ‹Z2 ≡ Y1 - {z. (s_P @ [z], {}) ∉ ℱ P}›
        hence ‹Y1 = Z1 ∪ Z2› by blast
        have $$ : ‹∀y∈Y2. (s_P @ [y], {}) ∉ ℱ P ∧ (s_Q @ [y], {}) ∉ ℱ Q›
        proof (rule ccontr)
          assume ‹¬ (∀y∈Y2. (s_P @ [y], {}) ∉ ℱ P ∧ (s_Q @ [y], {}) ∉ ℱ Q)›
          then obtain y1 where * : ‹y1 ∈ Y2› ‹((s_P @ [y1], {}) ∈ ℱ P ∨ (s_Q @ [y1], {}) ∈ ℱ Q)› by blast
          hence ‹(s @ [y1]) setinterleaves ((s_P @ [y1], s_Q), range tick ∪ ev ` A) ∨
                 (s @ [y1]) setinterleaves ((s_P, s_Q @ [y1]), range tick ∪ ev ` A)›
            by (simp add: Y2_def addNonSync assms(3))
          with "*" assms show False
            by (metis DiffD1 DiffD2 Y2_def addNonSync assms(1, 2, 3) assms4 is_processT4_empty)
        qed

        define X_P' where ‹X_P' = X_P ∪ Z1 ∪ Y2›
        hence f1: ‹(s_P, X_P') ∈ ℱ P› by (simp add: "$$" Z1_def assms(1) process_charn)
        define X_Q' where ‹X_Q' = X_Q ∪ Z2 ∪ Y2›
        hence f2: ‹(s_Q, X_Q') ∈ ℱ Q› using "$" "$$" by (simp add: Z2_def assms(2) is_processT5)
        have ‹(X_P ∪ X_Q ∪ Y1 ∪ Y2) ∩ range tick ∪ ev ` A =
              (X_P ∪ X_Q) ∩ range tick ∪ ev ` A ∪ Y1›
          unfolding Y1_def Y2_def by auto
        hence ‹(X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q ∪ Y =
               (X_P' ∪ X_Q') ∩ (range tick ∪ ev ` A) ∪ X_P' ∩ X_Q'›
          using X_P'_def X_Q'_def ‹Y1 = Z1 ∪ Z2› ‹Y1 ∪ Y2 = Y› by blast
        thus ‹(s, X ∪ Y) ∈ ?f› by simp (use f1 f2 assms(3, 4) in blast)
      qed
    qed
  next
    show processT9: ‹s @ [✓(res)] ∈ ?d P Q ⟹ s ∈ ?d P Q› for s res
    proof -
      { fix s t u r v and res :: 'r and P Q
        assume assms : ‹front_tickFree v› ‹tickFree r ∨ v = []› ‹s @ [✓(res)] = r @ v›
          ‹r setinterleaves ((t, u), range tick ∪ ev ` A)› ‹t ∈ 𝒟 P› ‹u ∈ 𝒯 Q›
        from assms(2) have ‹s ∈ ?d P Q›
        proof (elim disjE)
          assume ‹tickFree r›
          with assms(1, 3) have ‹s @ [✓(res)] = r @ (butlast v @ [✓(res)])›
            by (cases v rule: rev_cases) auto
          with ‹tickFree r› assms(1, 4, 5, 6) show ‹s ∈ ?d P Q›
            by simp (use front_tickFree_iff_tickFree_butlast tickFree_imp_front_tickFree in blast)
        next
          assume ‹v = []›
          with assms(3) obtain r' where ‹r = r' @ [✓(res)]› ‹s = r'› by auto
          with D_imp_front_tickFree SyncWithTick_imp_NTF assms(4, 5, 6) is_processT2_TR
          obtain t1 u1 where ‹t = t1 @ [✓(res)]› ‹u = u1 @ [✓(res)]›
            ‹r' setinterleaves ((t1, u1), range tick ∪ ev ` A)› by metis
          with assms(5, 6) show ‹s ∈ ?d P Q›
            apply (simp add: ‹s = r'›)
            by (metis prefixI ‹v = []› append.right_neutral assms(1) is_processT3_TR is_processT9)
        qed
      }
      thus ‹s @ [✓(res)] ∈ ?d P Q ⟹ s ∈ ?d P Q› for s by simp blast
    qed    

    fix s X res
    assume ‹(s @ [✓(res)], {}) ∈ ?f›
    hence ‹s @ [✓(res)] ∈ ?d P Q ∨
           (∃s_P s_Q X_P X_Q. (s_P, X_P) ∈ ℱ P ∧ (s_Q, X_Q) ∈ ℱ Q ∧
                              (s @ [✓(res)]) setinterleaves ((s_P, s_Q), range tick ∪ ev ` A) ∧
                              {} = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q)› by auto
    thus ‹(s, X - {✓(res)}) ∈ ?f›
    proof (elim disjE exE conjE)
      from processT9 show ‹s @ [✓(res)] ∈ ?d P Q ⟹ (s, X - {✓(res)}) ∈ ?f› by blast
    next
      fix s_P s_Q X_P X_Q res
      assume * : ‹(s_P, X_P) ∈ ℱ P› ‹(s_Q, X_Q) ∈ ℱ Q›
        ‹(s @ [✓(res)]) setinterleaves ((s_P, s_Q), range tick ∪ ev ` A)›
        ‹{} = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
      from SyncWithTick_imp_NTF1[OF "*"(3) "*"(1, 2)[THEN F_T]]
      show ‹(s, X - {✓(res)}) ∈ ?f› by simp
    qed
  next
    show ‹s ∈ ?d P Q ∧ tickFree s ∧ front_tickFree t ⟹ s @ t ∈ ?d P Q› for s t
      using front_tickFree_append by fastforce
  next  
    show ‹s ∈ ?d P Q ⟹ (s, X) ∈ ?f› for s X by blast
  qed
qed



section‹The Projections›

lemma F_Sync :
  ‹ℱ (P ⟦ A ⟧ Q) = 
   {(s, R). ∃t u X Y. (t, X) ∈ ℱ P ∧ (u, Y) ∈ ℱ Q ∧
                  s setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                      R = (X ∪ Y) ∩ (range tick ∪ ev ` A) ∪ X ∩ Y} ∪
   {(s, R). ∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ s = r @ v ∧
                      r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                      (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}›
  by (simp add: Failures.rep_eq Sync.rep_eq FAILURES_def)   

lemma D_Sync :
  ‹𝒟 (P ⟦ A ⟧ Q) = 
   {s. ∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ s = r @ v ∧
                 r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                 (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}›
  by (simp add: Divergences.rep_eq Sync.rep_eq DIVERGENCES_def)   

lemma T_Sync :
  ‹𝒯 (P ⟦ A ⟧ Q) =
   {s. ∃t u. t ∈ 𝒯 P ∧ u ∈ 𝒯 Q ∧ s setinterleaves ((t, u), range tick ∪ ev ` A)} ∪
   {s. ∃t u r v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧
                 s = r @ v ∧ r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                 (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}›
  by (simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_Sync) blast

lemmas Sync_projs = F_Sync D_Sync T_Sync


section‹Syntax for Interleave and Parallel Operator ›

abbreviation Inter_syntax  ("(_ ||| _)" [72,73] 72)
  where "P ||| Q ≡ (P ⟦ {} ⟧ Q)"

abbreviation Par_syntax  ("(_ || _)" [74,75] 74)
  where "P || Q  ≡ (P ⟦ UNIV ⟧ Q)"


lemma setinterleaving_UNIV_iff : ‹s setinterleaves ((t, u), UNIV) ⟷ s = t ∧ s = u›
  for s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
  by (induct ‹(u, UNIV :: ('a, 'r) event⇩p⇩t⇩i⇩c⇩k set, t)›
      arbitrary: s t u rule: setinterleaving.induct) auto

lemma F_Par :
  ‹ℱ (P || Q) = {(s, R). ∃X Y. (s, X) ∈ ℱ P ∧ (s, Y) ∈ ℱ Q ∧ R = X ∪ Y ∪ X ∩ Y} ∪
                 {(s, R). ∃t v. ftF v ∧ (tF t ∨ v = []) ∧ s = t @ v ∧
                                (t ∈ 𝒟 P ∧ t ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ t ∈ 𝒯 P)}›
  by (auto simp add: F_Sync setinterleaving_UNIV_iff)

lemma D_Par :
  ‹𝒟 (P || Q) = {s. ∃t v. ftF v ∧ (tF t ∨ v = []) ∧ s = t @ v ∧
                          (t ∈ 𝒟 P ∧ t ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ t ∈ 𝒯 P)}›
  by (simp add: D_Sync setinterleaving_UNIV_iff)

lemma T_Par :
  ‹𝒯 (P || Q) = 𝒯 P ∩ 𝒯 Q ∪ {t @ v| t v. ftF v ∧ (tF t ∨ v = []) ∧
                                          t ∈ 𝒟 P ∩ 𝒯 Q ∪ 𝒟 Q ∩ 𝒯 P}›
  by (simp add: set_eq_iff T_Sync setinterleaving_UNIV_iff) blast

lemmas Par_projs = F_Par D_Par T_Par


lemma superset_T_Inter : ‹{t. tF t ∧ t ∈ 𝒯 P ∪ 𝒯 Q} ⊆ 𝒯 (P ||| Q)›
proof (rule subsetI, clarify)
  fix t assume ‹tF t› ‹t ∈ 𝒯 P ∪ 𝒯 Q›
  from ‹tF t› have ‹t setinterleaves ((t, []), range tick)›
    by (metis disjoint_iff emptyLeftSelf setinterleaving_sym tickFree_def)
  with ‹t ∈ 𝒯 P ∪ 𝒯 Q› show ‹t ∈ 𝒯 (P ||| Q)›
    by (simp add: T_Sync) (use Nil_elem_T setinterleaving_sym in blast)
qed

lemma superset_D_Inter : ‹𝒟 P ∪ 𝒟 Q ⊆ 𝒟 (P ||| Q)›
proof (rule subsetI)
  fix t assume ‹t ∈ 𝒟 P ∪ 𝒟 Q›
  define t' where ‹t' ≡ if tF t then t else butlast t›
  from ‹t ∈ 𝒟 P ∪ 𝒟 Q› D_imp_front_tickFree front_tickFree_iff_tickFree_butlast
  have ‹tF t'› unfolding t'_def by auto
  with ‹t ∈ 𝒟 P ∪ 𝒟 Q› have ‹t' ∈ 𝒟 P ∪ 𝒟 Q›
    by (metis t'_def D_imp_front_tickFree Un_iff butlast_snoc
        is_processT9 nonTickFree_n_frontTickFree)
  from ‹tF t'› have ‹t' setinterleaves ((t', []), range tick)›
    by (metis disjoint_iff emptyLeftSelf setinterleaving_sym tickFree_def)
  with ‹t' ∈ 𝒟 P ∪ 𝒟 Q› have ‹t' ∈ 𝒟 (P ||| Q)›
    by (simp add: D_Sync) (use front_tickFree_Nil Nil_elem_T in blast)
  thus ‹t ∈ 𝒟 (P ||| Q)›
    by (metis ‹tF t'› butlast_snoc front_tickFree_iff_tickFree_butlast
        front_tickFree_single is_processT7 nonTickFree_n_frontTickFree t'_def)
qed



section‹ Continuity Rule ›

lemma Sync_commute: ‹P ⟦S⟧ Q = Q ⟦S⟧ P›
  ―‹This will simplify the following proofs.›
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 (P ⟦S⟧ Q) ⟹ s ∈ 𝒟 (Q ⟦S⟧ P)› for s by (simp add: D_Sync) blast
next
  show ‹s ∈ 𝒟 (Q ⟦S⟧ P) ⟹ s ∈ 𝒟 (P ⟦S⟧ Q)› for s by (simp add: D_Sync) blast
next
  show ‹(s, X) ∈ ℱ (P ⟦S⟧ Q) ⟹ (s, X) ∈ ℱ (Q ⟦S⟧ P)› for s X
    by (simp add: F_Sync, elim disjE exE)
      (metis (no_types) Int_commute Un_commute setinterleaving_sym, blast)
next
  show ‹(s, X) ∈ ℱ (Q ⟦S⟧ P) ⟹ (s, X) ∈ ℱ (P ⟦S⟧ Q)› for s X
    by (simp add: F_Sync, elim disjE exE)
      (metis (no_types) Int_commute Un_commute setinterleaving_sym, blast)
qed


(* TODO: declare this simp ? *)
lemma mono_Sync : ‹P ⊑ P' ⟹ Q ⊑ Q' ⟹ P ⟦A⟧ Q ⊑ P' ⟦A⟧ Q'›
  for P :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
proof -
  have ‹P ⟦A⟧ S ⊑ Q ⟦A⟧ S› if ‹P ⊑ Q› for P S Q :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  proof (unfold le_approx_def, safe)
    from le_approx1[OF ‹P ⊑ Q›] le_approx_lemma_T[OF ‹P ⊑ Q›]
    show ‹s ∈ 𝒟 (Q ⟦A⟧ S) ⟹ s ∈ 𝒟 (P ⟦A⟧ S)› for s by (simp add: D_Sync) blast
  next
    show ‹s ∉ 𝒟 (P ⟦A⟧ S) ⟹ X ∈ ℛ⇩a (P ⟦A⟧ S) s ⟹ X ∈ ℛ⇩a (Q ⟦A⟧ S) s› for s X
      by (simp add: D_Sync Refusals_after_def F_Sync, elim disjE)
        (metis F_T front_tickFree_Nil proc_ord2a[OF that] self_append_conv, blast)
  next
    show ‹s ∉ 𝒟 (P ⟦A⟧ S) ⟹ X ∈ ℛ⇩a (Q ⟦A⟧ S) s ⟹ X ∈ ℛ⇩a (P ⟦A⟧ S) s› for s X
      apply (simp add: D_Sync Refusals_after_def F_Sync, elim disjE)
      using le_approx_lemma_F that apply blast
        (* TODO: break this smt *)
      by (smt (verit, ccfv_SIG) in_mono le_approx1 le_approx_lemma_T that)
  next
    fix s
    assume ‹s ∈ min_elems (𝒟 (P ⟦A⟧ S))›
    hence ‹s ∈ 𝒟 (P ⟦A⟧ S)› by (simp add: elem_min_elems)
    then obtain t u r
      where * : ‹r ≤ s› ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 S ∨ t ∈ 𝒟 S ∧ u ∈ 𝒯 P›
        ‹r setinterleaves ((t, u), range tick ∪ ev ` A)›
      by (simp add: D_Sync less_eq_list_def prefix_def) blast

    have ‹∃t u r. r ≤ s ∧ r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                  (t ∈ min_elems (𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems (𝒟 S) ∧ u ∈ 𝒯 P)›
    proof (rule ccontr)
      assume assm : ‹∄t u r1. r1 ≤ s ∧ r1 setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                              (t ∈ min_elems (𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems (𝒟 S) ∧ u ∈ 𝒯 P)›

      obtain tm1 tm2 where $: ‹t ∈ 𝒟 P ⟹ tm1 ≤ t ∧ tm1 ∈ min_elems (𝒟 P)›
        ‹t ∈ 𝒟 S ⟹ tm2 ≤ t ∧ tm2 ∈ min_elems (𝒟 S)›
        by (metis min_elems5)
      hence $$ : ‹t ∈ 𝒟 P ⟹ u ∈ 𝒯 S ⟹ tm1 < t› ‹t ∈ 𝒟 S ⟹ u ∈ 𝒯 P ⟹ tm2 < t›
        by (metis "*"(1, 3) assm order_neq_le_trans)+
      then obtain um1 rm1 um2 rm2 where
        ‹t ∈ 𝒟 P ⟹ u ∈ 𝒯 S ⟹ um1 ≤ u ∧ rm1 setinterleaves ((tm1, um1), range tick ∪ ev ` A)›
        ‹t ∈ 𝒟 S ⟹ u ∈ 𝒯 P ⟹ um2 ≤ u ∧ rm2 setinterleaves ((tm2, um2), range tick ∪ ev ` A)›
        by (metis "*"(3) interleave_less_left)
      moreover have ‹t ∈ 𝒟 P ⟹ u ∈ 𝒯 S ⟹ rm1 < s ∧ rm1 ∈ 𝒟 (P ⟦A⟧ S)›
        ‹t ∈ 𝒟 S ⟹ u ∈ 𝒯 P ⟹ rm2 < s ∧ rm2 ∈ 𝒟 (P ⟦A⟧ S)›
        by (meson assm "$"(1, 2) "$$"(1, 2) "*"(1) "*"(3)
            interleave_le_left is_processT3_TR order_trans)+
      ultimately show False by (metis "*"(2) ‹s ∈ min_elems (𝒟 (P ⟦A⟧ S))› less_list_def min_elems_no)
    qed

―‹We override.›
    then obtain t u r
      where * : ‹r ≤ s› ‹r setinterleaves ((t, u), range tick ∪ ev ` A)›
        ‹t ∈ min_elems (𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems (𝒟 S) ∧ u ∈ 𝒯 P› by blast

    from "*"(2, 3) have ‹r ∈ 𝒟 (P ⟦A⟧ S)›
      by (simp add: D_Sync) (use elem_min_elems front_tickFree_Nil in blast)
    with "*"(1) ‹s ∈ min_elems (𝒟 (P ⟦A⟧ S))› min_elems_no have ‹s = r› by blast

    have ‹t ∈ 𝒟 S ⟹ u ∈ 𝒯 P ⟹ u ∈ 𝒯 P - (𝒟 P - min_elems (𝒟 P))›
    proof (rule ccontr)
      assume assms : ‹t ∈ 𝒟 S› ‹u ∈ 𝒯 P› ‹u ∉ 𝒯 P - (𝒟 P - min_elems (𝒟 P))›
      from assms(2, 3) have ‹u ∈ 𝒟 P› ‹u ∉ min_elems (𝒟 P)› by simp_all
      then obtain u1 where ‹u1 < u› ‹u1 ∈ min_elems (𝒟 P)› 
        by (metis min_elems5 order_neq_le_trans)

      obtain t1 r1 where ‹t1 ≤ t› ‹r1 setinterleaves ((t1, u1), range tick ∪ ev ` A)› ‹r1 < r›
        by (metis (no_types, lifting) "*"(2) ‹u1 < u› interleave_less_left setinterleaving_sym)
      from ‹t1 ≤ t› ‹u1 ∈ min_elems (𝒟 P)› assms(1) have ‹u1 ∈ 𝒟 P ∧ t1 ∈ 𝒯 S›
        using D_T elem_min_elems is_processT3_TR by blast
      moreover have ‹r1 ∈ 𝒟 (P ⟦A⟧ S)›
        by (simp add: D_Sync)  
          (use ‹r1 setinterleaves ((t1, u1), range tick ∪ ev ` A)›
            ‹u1 ∈ 𝒟 P ∧ t1 ∈ 𝒯 S› front_tickFree_Nil setinterleaving_sym in blast)
      ultimately show False
        by (metis ‹r1 < r› ‹s = r› ‹s ∈ min_elems (𝒟 (P ⟦A⟧ S))› less_list_def min_elems_no)
    qed

    hence ‹∃t u. s setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                (t ∈ min_elems (𝒟 P) ∧ u ∈ 𝒯 S ∨ t ∈ min_elems (𝒟 S) ∧
                u ∈ 𝒯 P ∧ u ∈ 𝒯 P - (𝒟 P - min_elems (𝒟 P)))›
      using "*"(2, 3) ‹s = r› elem_min_elems by blast
    thus ‹s ∈ 𝒯 (Q ⟦A⟧ S)›
      by (simp add: T_Sync)
        (metis (no_types) append.right_neutral elem_min_elems front_tickFree_Nil
          le_approx2T[OF ‹P ⊑ Q›] ‹P ⊑ Q›[unfolded le_approx_def] in_mono)
  qed
  thus ‹P ⊑ P' ⟹ Q ⊑ Q' ⟹ P ⟦A⟧ Q ⊑ P' ⟦A⟧ Q'›
    by (metis Sync_commute below_trans)
qed



lemma chain_Sync_left  : ‹chain Y ⟹ chain (λi. Y i ⟦A⟧ S)›
  and chain_Sync_right : ‹chain Y ⟹ chain (λi. S ⟦A⟧ Y i)›
  by (simp_all add: chain_def mono_Sync) 




lemma finite_interleaves: ‹finite {(t, u). (s :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k) setinterleaves ((t, u), A)}›
proof (induction ‹length s› arbitrary: s rule: nat_less_induct)
  fix s :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
  assume hyp : ‹∀m < length s. ∀s. m = length s ⟶ finite {(t, u). s setinterleaves ((t, u), A)}›
  show ‹finite {(t, u). s setinterleaves ((t, u), A)}›
  proof (cases s)
    have ‹[] setinterleaves ((t, u), A) ⟹ t = [] ∧ u = []› for t u
      using EmptyLeftSync empty_setinterleaving by blast
    hence ‹{(t, u). [] setinterleaves ((t, u), A)} = {([], [])}› by auto
    thus ‹s = [] ⟹ finite {(t, u). s setinterleaves ((t, u), A)}› by simp
  next
    fix x s'
    assume ‹s = x # s'›
    define S where ‹S ≡ {(t, u). s' setinterleaves ((t, u), A)}›
    with hyp ‹s = x # s'› have ‹finite S› by auto
    have ‹s setinterleaves ((t, u), A) ⟹
          t ≠ [] ∧ hd t = x ∧ s' setinterleaves ((tl t,    u), A) ∨
          u ≠ [] ∧ hd u = x ∧ s' setinterleaves ((   t, tl u), A) ∨
          t ≠ [] ∧ hd t = x ∧ u ≠ [] ∧ hd u = x ∧
          s' setinterleaves ((tl t, tl u), A)› for t u
      by (cases t; cases u; simp add: ‹s = x # s'› split: if_split_asm) blast
    hence * : ‹{(t, u). s setinterleaves ((t, u), A)} ⊆
               {(t, u). t ≠ [] ∧ hd t = x ∧ s' setinterleaves ((tl t,    u), A)} ∪
               {(t, u). u ≠ [] ∧ hd u = x ∧ s' setinterleaves ((   t, tl u), A)} ∪
               {(t, u). t ≠ [] ∧ hd t = x ∧ u ≠ [] ∧ hd u = x ∧
                         s' setinterleaves ((tl t, tl u), A)}›
      (is ‹{(t, u). s setinterleaves ((t, u), A)} ⊆ ?S1 ∪ ?S2 ∪ ?S3›) by blast

    have ‹?S1 = {(x # t, u)| t u. s' setinterleaves ((t, u), A)}› by force
    also have ‹… = (λ(t, u). (x # t, u)) ` S› unfolding S_def by auto
    finally have ‹finite ?S1› by (simp add: ‹finite S›)

    have ‹?S2 = {(t, x # u)| t u. s' setinterleaves ((t, u), A)}› by force
    also have ‹… = (λ(t, u). (t, x # u)) ` S› unfolding S_def by auto
    finally have ‹finite ?S2› by (simp add: ‹finite S›)

    have ‹?S3 = {(x # t, x # u)| t u. s' setinterleaves ((t, u), A)}›
      by (simp add: set_eq_iff) (metis list.collapse list.distinct(1) list.sel(1, 3))
    also have ‹… = (λ(t, u). (x # t, x # u)) ` S› unfolding S_def by auto
    finally have ‹finite ?S3› by (simp add: ‹finite S›)

    from "*" ‹finite ?S1› ‹finite ?S2› ‹finite ?S3› finite_subset
    show ‹finite {(t, u). s setinterleaves ((t, u), A)}› by blast
  qed
qed


lemma finite_interleaves_Sync:
  ‹finite {(t, u, r). r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                      (∃v. s = r @ v ∧ front_tickFree v ∧ (tickFree r ∨ v = []))}›
  (is ‹finite ?A›)
proof -
  have ‹?A ⊆ (⋃r∈{r. r ≤ s}. {(t, u, r) |t u. r setinterleaves ((t, u), range tick ∪ ev ` A)})›
    (is ‹?A ⊆ (⋃r ∈ {r. r ≤ s}. ?P r)›)
    unfolding less_eq_list_def prefix_def by blast

  have ‹?P r ⊆ (λ(t, u). (t, u, r)) `
                {(t, u). r setinterleaves ((t, u), range tick ∪ ev ` A)}› for r by auto
  hence ‹finite (?P r)› for r by (rule finite_subset) (simp add: finite_interleaves)

  have ‹{r. ∃v. s = r @ v} = {r. ∃v. r @ v = s}› by blast
  hence ‹finite {r. r ≤ s}›
    by (fold prefix_def less_eq_list_def)
      (use prefixes_fin[of s, simplified Let_def] in presburger)

  show ?thesis
    by (rule finite_subset[OF ‹?A ⊆ (⋃r ∈ {r. r ≤ s}. ?P r)›]) 
      (rule finite_UN_I[OF ‹finite {r. r ≤ s}› ‹⋀r. finite (?P r)›])
qed



lemma Cont_Sync_prem:
  ‹(⨆ i. Y i) ⟦A⟧ Q = (⨆ i. Y i ⟦A⟧ Q)› if chain: ‹chain Y›
proof (subst Process_eq_spec_optimized, safe)
  show ‹s ∈ 𝒟 ((⨆ i. Y i) ⟦A⟧ Q) ⟹ s ∈ 𝒟 (⨆i. Y i ⟦A⟧ Q)› for s
    by (simp add: limproc_is_thelub chain chain_Sync_left D_Sync D_LUB T_LUB) blast
next
  show ‹(s, X) ∈ ℱ ((⨆ i. Y i) ⟦A⟧ Q) ⟹ (s, X) ∈ ℱ (⨆i. Y i ⟦A⟧ Q)› for s X
    by (simp add: limproc_is_thelub chain chain_Sync_left F_Sync D_LUB T_LUB F_LUB) blast
next
  fix s
  assume ‹s ∈ 𝒟 (⨆i. Y i ⟦A⟧ Q)›
  define S 
    where ‹S i ≡ {(t, u, r). ∃v. front_tickFree v ∧ (tickFree r ∨ v = []) ∧ s = r @ v ∧
                                   r setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                                   (t ∈ 𝒟 (Y i) ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 (Y i))}› for i
  have ‹(⋂i. S i) ≠ {}› 
    apply (rule Inter_nonempty_finite_chained_sets, unfold S_def)
      apply (use ‹s ∈ 𝒟 (⨆i. Y i ⟦A⟧ Q)› in
        ‹simp add: limproc_is_thelub chain chain_Sync_left D_Sync T_LUB D_LUB, blast›)
     apply (rule finite_subset[OF _ finite_interleaves_Sync]; auto)
    using D_T le_approx1[OF po_class.chainE[OF chain]]
      le_approx2T[OF po_class.chainE[OF chain]] by blast
  then obtain t u r where ‹(t, u, r) ∈ (⋂i. S i)› by auto
  hence ‹front_tickFree (drop (length r) s) ∧ (tickFree r ∨ drop (length r) s = []) ∧
           s = r @ drop (length r) s ∧ r setinterleaves ((t, u), range tick ∪ ev ` A) ∧ 
           ((∀i. t ∈ 𝒟 (Y i)) ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ (∀i. u ∈ 𝒯 (Y i)))›
    by (auto simp add: S_def) (meson chain_lemma le_approx1 le_approx_lemma_T subsetD chain)

  show ‹s ∈ 𝒟 ((⨆ i. Y i) ⟦A⟧ Q)›
    by (simp add: limproc_is_thelub chain chain_Sync_left D_Sync T_LUB D_LUB)
      (use ‹?this› in blast)
next
  assume same_div : ‹𝒟 ((⨆ i. Y i) ⟦A⟧ Q) = 𝒟 (⨆ i. Y i ⟦A⟧ Q)›
  fix s X assume ‹(s, X) ∈ ℱ (⨆i. Y i ⟦A⟧ Q)›
  show ‹(s, X) ∈ ℱ ((⨆ i. Y i) ⟦A⟧ Q)›
  proof (cases ‹s ∈ 𝒟 (⨆ i. Y i ⟦A⟧ Q)›)
    show ‹s ∈ 𝒟 (⨆i. Y i ⟦A⟧ Q) ⟹ (s, X) ∈ ℱ ((⨆i. Y i) ⟦A⟧ Q)›
      by (simp add: is_processT8 same_div)
  next
    assume ‹s ∉ 𝒟 (⨆i. Y i ⟦A⟧ Q)›
    then obtain j where ‹s ∉ 𝒟 (Y j ⟦A⟧ Q)›
      by (auto simp add: limproc_is_thelub chain_Sync_left ‹chain Y› D_LUB)
    moreover from ‹(s, X) ∈ ℱ (⨆i. Y i ⟦A⟧ Q)› have ‹(s, X) ∈ ℱ (Y j ⟦A⟧ Q)›
      by (simp add: limproc_is_thelub chain_Sync_left ‹chain Y› F_LUB)
    ultimately show ‹(s, X) ∈ ℱ ((⨆ i. Y i) ⟦A⟧ Q)›
      by (fact le_approx2[OF mono_Sync[OF is_ub_thelub[OF ‹chain Y›] below_refl], THEN iffD2])
  qed
qed



lemma Sync_cont[simp]: ‹cont (λx. f x ⟦A⟧ g x)› if ‹cont f› ‹cont g›
proof (rule cont_apply[where f = ‹λx y. y ⟦A⟧ g x›])
  from ‹cont f› show ‹cont f› .
next
  show ‹cont (λy. y ⟦A⟧ g x)› for x
  proof (rule contI2)
    show ‹monofun (λy. y ⟦A⟧ g x)› by (simp add: monofunI mono_Sync)
  next
    show ‹chain Y ⟹ (⨆i. Y i) ⟦A⟧ g x ⊑ (⨆i. Y i ⟦A⟧ g x)› for Y
      by (simp add: Cont_Sync_prem)
  qed
next
  show ‹cont (λx. y ⟦A⟧ g x)› for y
  proof (rule cont_compose[of ‹λx. y ⟦A⟧ x›])
    show ‹cont (Sync y A)› 
    proof (rule contI2)
      show ‹monofun (Sync y A)› by (simp add: monofunI mono_Sync)
    next
      show ‹chain Y ⟹ y ⟦A⟧ (⨆i. Y i) ⊑ (⨆i. y ⟦A⟧ Y i)› for Y
        by (subst (1 2) Sync_commute) (simp add: Cont_Sync_prem)
    qed
  next
    from ‹cont g› show ‹cont g› .
  qed
qed


(*<*)
end
  (*>*)