Theory Synchronization_Product_Generalized_Associativity

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * 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
 *
 * * 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.
 *
 * 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 HOLDER 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.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


section ‹Associativity›

(*<*)
theory Synchronization_Product_Generalized_Associativity
  imports CSP_PTick_Renaming
begin
  (*>*)



subsection ‹Motivation›

text ‹
The classical synchronization product is associative: @{thm Sync_assoc[of P A Q R]}
but in our generalization such a law cannot be obtained in all generality.
We already encountered a similar issue for the commutativity:
we have to find a setup in which the different combinations of the ticks
that we need make sense, and prove the quasi-associativity.
›



subsection ‹Formalization›

locale Syncptick_assoc_locale =
  Syncptick1 : Syncptick_locale ‹(⊗✓1)› +
  Syncptick2 : Syncptick_locale ‹(⊗✓2)› +
  Syncptick3 : Syncptick_locale ‹(⊗✓3)› +
  Syncptick4 : Syncptick_locale ‹(⊗✓4)›
  for tick_join1 :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓1› 100)
    and tick_join2 :: ‹'t ⇒ 'u ⇒ 'v option› (infixl ‹⊗✓2› 100)
    and tick_join3 :: ‹'r ⇒ 'w ⇒ 'x option› (infixl ‹⊗✓3› 100)
    and tick_join4 :: ‹'s ⇒ 'u ⇒ 'w option› (infixl ‹⊗✓4› 100) +
  fixes tick_assoc_ren      :: ‹'v ⇒ 'x› (‹⊗✓2⇒⊗✓3›)
    and tick_assoc_ren_conv :: ‹'x ⇒ 'v› (‹⊗✓3⇒⊗✓2›)
  assumes None_assms_tick_join :
    ‹r ⊗✓1 s = ◇ ⟹ s ⊗✓4 u = ◇ ∨ r ⊗✓3 ⌈s ⊗✓4 u⌉ = ◇›
    ‹r ⊗✓1 s ≠ ◇ ⟹ ⌈r ⊗✓1 s⌉ ⊗✓2 u = ◇ ⟹ s ⊗✓4 u = ◇ ∨ r ⊗✓3 ⌈s ⊗✓4 u⌉ = ◇›
    ‹s ⊗✓4 u = ◇ ⟹ r ⊗✓1 s = ◇ ∨ ⌈r ⊗✓1 s⌉ ⊗✓2 u = ◇›
    ‹s ⊗✓4 u ≠ ◇ ⟹ r ⊗✓3 ⌈s ⊗✓4 u⌉ = ◇ ⟹ r ⊗✓1 s = ◇ ∨ ⌈r ⊗✓1 s⌉ ⊗✓2 u = ◇›
    and tick_assoc_ren_hyp :
    ‹r ⊗✓1 s = ⌊t⌋ ⟹ t ⊗✓2 u = ⌊v⌋ ⟹ ⌈r ⊗✓3 ⌈s ⊗✓4 u⌉⌉ = ⊗✓2⇒⊗✓3 v›
    and tick_assoc_ren_conv_hyp :
    ‹s ⊗✓4 u = ⌊w⌋ ⟹ r ⊗✓3 w = ⌊x⌋ ⟹ ⌈⌈r ⊗✓1 s⌉ ⊗✓2 u⌉ = ⊗✓3⇒⊗✓2 x›
begin


text ‹There is a symmetry over the variables.›

sublocale Syncptick_assoc_locale_sym :
  Syncptick_assoc_locale ‹λu s. s ⊗✓4 u› ‹λw r. r ⊗✓3 w› ‹λu t. t ⊗✓2 u›
  ‹λs r. r ⊗✓1 s› ‹⊗✓3⇒⊗✓2› ‹⊗✓2⇒⊗✓3›
  by unfold_locales
    (fact None_assms_tick_join tick_assoc_ren_hyp tick_assoc_ren_conv_hyp)+

end


subsection ‹First Properties›

lemma (in Syncptick_assoc_locale) tick_assoc_ren_tick_assoc_ren_conv :
  ‹∃r s u w. s ⊗✓4 u = ⌊w⌋ ∧ r ⊗✓3 w = ⌊x⌋ ⟹
   ⊗✓2⇒⊗✓3 (⊗✓3⇒⊗✓2 x) = x›
  by (metis None_assms_tick_join(1,2) option.collapse option.distinct(1)
      option.sel tick_assoc_ren_hyp tick_assoc_ren_conv_hyp)

lemma (in Syncptick_assoc_locale) tick_assoc_ren_conv_tick_assoc_ren :
  ‹∃r s t u. r ⊗✓1 s = ⌊t⌋ ∧ t ⊗✓2 u = ⌊v⌋ ⟹ ⊗✓3⇒⊗✓2 (⊗✓2⇒⊗✓3 v) = v›
  by (metis Syncptick_assoc_locale_sym.tick_assoc_ren_tick_assoc_ren_conv)

lemma (in Syncptick_assoc_locale) inj_on_tick_assoc_ren :
  ‹inj_on ⊗✓2⇒⊗✓3 {v. ∃r s t u. r ⊗✓1 s = ⌊t⌋ ∧ t ⊗✓2 u = ⌊v⌋}›
  by (rule inj_onI, simp) (metis tick_assoc_ren_conv_tick_assoc_ren)

lemma (in Syncptick_assoc_locale) inj_on_tick_assoc_ren_conv :
  ‹inj_on ⊗✓3⇒⊗✓2 {x. ∃r s u w. s ⊗✓4 u = ⌊w⌋ ∧ r ⊗✓3 w = ⌊x⌋}›
  by (rule inj_onI, simp) (metis tick_assoc_ren_tick_assoc_ren_conv)



subsection ‹Associativity for the Traces›

lemma (in Syncptick_assoc_locale) setinterleavesptick_assoc_left : 
  ‹⟦tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts), A);
    tv setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A)⟧ ⟹
    ∃tw. map (map_eventptick id ⊗✓2⇒⊗✓3) tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A) ∧
         tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)›
proof -
  let ?map = ‹λt. map ev (map of_ev t)›
  let ?map_event = ‹λt. map (map_eventptick id ⊗✓2⇒⊗✓3) t›
  show ‹⟦tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts), A);
         tv setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A)⟧ ⟹ ?thesis›
  proof (induct ‹((⊗✓2), tt, A, tu)› arbitrary: tr ts tt tu tv)
    case Nil_setinterleavingptick_Nil
    thus ?case
      by (cases tr; cases ts)
        (auto intro: Nil_setinterleavesptick simp add: setinterleavingptick_simps
          split: if_split_asm eventptick.split_asm option.split_asm)
  next
    case (ev_setinterleavingptick_Nil a tt)
    from ev_setinterleavingptick_Nil.prems(2)
    have ‹a ∉ A› ‹tF tt› ‹set tt ∩ ev ` A = {}› ‹tv = ?map (ev a # tt)›
      and $ : ‹?map tt setinterleaves✓⇘(⊗✓2)⇙ ((tt, []), A)›
      by (auto simp add: setinterleavesptick_NilR_iff split: if_split_asm)
    from ev_setinterleavingptick_Nil.prems(1)
    consider (mv_left) tr' where ‹tr = ev a # tr'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts), A)›
      | (mv_right) ts' where ‹ts = ev a # ts'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts'), A)›
      by (auto simp add: ‹a ∉ A› elim: Cons_ev_setinterleavesptickE)
    thus ?case
    proof cases
      case mv_left
      from ev_setinterleavingptick_Nil.hyps[OF ‹a ∉ A› mv_left(2) "$"]
      obtain tw where * : ‹?map_event (?map tt) setinterleaves✓⇘(⊗✓3)⇙((tr', tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, []), A)› by blast
      from "*"(1) have ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
        by (cases tw, auto simp add: mv_left(1) ‹a ∉ A› ‹tv = ?map (ev a # tt)›
            setinterleavingptick_simps split: eventptick.split)
      with "*"(2) show ?thesis by blast
    next
      case mv_right
      from ev_setinterleavingptick_Nil.hyps[OF ‹a ∉ A› mv_right(2) "$"]
      obtain tw where * : ‹?map_event (?map tt) setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts', []), A)› by blast
      from "*"(2) have ‹ev a # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, []), A)›
        by (simp add: ‹a ∉ A› ‹tv = ?map (ev a # tt)› mv_right(1))
      moreover from "*"(1) 
      have ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev a # tw), A)›
        by (cases tr, auto simp add: ‹a ∉ A› ‹tv = ?map (ev a # tt)› setinterleavingptick_simps
            split: eventptick.split)
      ultimately show ?thesis by blast
    qed
  next
    case (tick_setinterleavingptick_Nil r tt)
    from tick_setinterleavingptick_Nil.prems(2) have False by simp
    thus ?case ..
  next
    case (Nil_setinterleavingptick_ev b tu)
    from Nil_setinterleavingptick_ev.prems(1)[THEN setinterleavesptick_imp_lengthLR_le]
    have ‹tr = []› ‹ts = []› by simp_all
    from Nil_setinterleavingptick_ev.prems(2)
    have ‹b ∉ A› ‹tF tu› ‹set tu ∩ ev ` A = {}› ‹tv = ?map (ev b # tu)›
      and $ : ‹?map tu setinterleaves✓⇘(⊗✓2)⇙ (([], tu), A)›
      by (auto simp add: setinterleavesptick_NilL_iff split: if_split_asm)
    from Nil_setinterleavingptick_ev.hyps[OF ‹b ∉ A› Nil_setinterleavingptick_ev.prems(1) "$"]
    obtain tw where ‹?map_event (?map tu) setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
      ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)› by blast
    hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev b # tw), A) ∧
          ev b # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
      by (simp add: ‹tv = ?map (ev b # tu)› ‹tr = []› ‹ts = []› ‹b ∉ A›)
    thus ?case ..
  next
    case (Nil_setinterleavingptick_tick ru tu)
    from Nil_setinterleavingptick_tick.prems(2) have False by simp
    thus ?case ..
  next
    case (ev_setinterleavingptick_ev a tt b tu)
    from ev_setinterleavingptick_ev.prems(2)
    consider (mv_both) tv' where ‹a ∈ A› ‹b ∈ A› ‹a = b› ‹tv = ev b # tv'› ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A)›
      |      (mvR_inL) tv' where ‹a ∈ A› ‹b ∉ A› ‹tv = ev b # tv'› ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((ev a # tt, tu), A)›
      |      (mvL_inR) tv' where ‹a ∉ A› ‹b ∈ A› ‹tv = ev a # tv'› ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, ev b # tu), A)›
      |      (mvR_notin) tv' where ‹a ∉ A› ‹b ∉ A› ‹tv = ev b # tv'› ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((ev a # tt, tu), A)›
      |      (mvL_notin) tv' where ‹a ∉ A› ‹b ∉ A› ‹tv = ev a # tv'› ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, ev b # tu), A)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      case mv_both
      from ev_setinterleavingptick_ev.prems(1)
      obtain tr' ts' where ‹tr = ev a # tr'› ‹ts = ev a # ts'›
        ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts'), A)›
        by (auto simp add: ‹a ∈ A› elim: Cons_ev_setinterleavesptickE)
      from ev_setinterleavingptick_ev.hyps(1)[OF mv_both(1-3) ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts'), A)› mv_both(5)]
      obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr', tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts', tu), A)› by blast
      hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev a # tw), A) ∧
           ev a # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
        by (simp add: mv_both(2-4) ‹ts = ev a # ts'› ‹tr = ev a # tr'›)
      thus ?thesis ..
    next
      case mvR_inL
      from ev_setinterleavingptick_ev.prems(1)
      obtain tr' ts' where ‹tr = ev a # tr'› ‹ts = ev a # ts'›
        ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts'), A)›
        by (auto simp add: ‹a ∈ A› elim: Cons_ev_setinterleavesptickE)
      from ev_setinterleavingptick_ev.hyps(2)[OF mvR_inL(1, 2) ev_setinterleavingptick_ev.prems(1) mvR_inL(4)]
      obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)› by blast
      hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev b # tw), A) ∧
           ev b # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
        by (simp add: ‹tr = ev a # tr'› ‹ts = ev a # ts'› mvR_inL(1-3))
      thus ?thesis ..
    next
      case mvL_inR
      from ev_setinterleavingptick_ev.prems(1)
      consider (mv_left) tr' where ‹tr = ev a # tr'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts), A)›
        | (mv_right) ts' where ‹ts = ev a # ts'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts'), A)›
        by (auto simp add: ‹a ∉ A› elim: Cons_ev_setinterleavesptickE)
      thus ?thesis
      proof cases
        case mv_left
        from ev_setinterleavingptick_ev.hyps(3)[OF mvL_inR(1, 2) mv_left(2) mvL_inR(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr', tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A) ∧
             tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases tw) (auto simp add: mvL_inR(1-3) mv_left(1)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      next
        case mv_right
        from ev_setinterleavingptick_ev.hyps(3)[OF mvL_inR(1, 2) mv_right(2) mvL_inR(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts', ev b # tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev a # tw), A) ∧
             ev a # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases tr) (auto simp add: mvL_inR(1-3) mv_right(1)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      qed
    next
      case mvR_notin
      from ev_setinterleavingptick_ev.prems(1)
      consider (mv_left) tr' where ‹tr = ev a # tr'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts), A)›
        | (mv_right) ts' where ‹ts = ev a # ts'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts'), A)›
        by (auto simp add: ‹a ∉ A› elim: Cons_ev_setinterleavesptickE)
      thus ?thesis
      proof cases
        case mv_left
        from mv_left(2) have ‹ev a # tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts), A)›
          by (cases ts) (auto simp add: mv_left(1) mvR_notin(1)
              setinterleavingptick_simps split: eventptick.split)
        from ev_setinterleavingptick_ev.hyps(5)[OF mvR_notin(1, 2) this mvR_notin(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev b # tw), A) ∧
             ev b # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases ts) (auto simp add: mvR_notin(1-3) mv_left(1)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      next
        case mv_right
        from mv_right(2) have ‹ev a # tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts), A)›
          by (cases tr) (auto simp add: mv_right(1) mvR_notin(1)
              setinterleavingptick_simps split: eventptick.split)
        from ev_setinterleavingptick_ev.hyps(5)[OF mvR_notin(1, 2) this mvR_notin(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev b # tw), A) ∧
             ev b # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases tr) (auto simp add: mvR_notin(1-3) mv_right(1)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      qed
    next
      case mvL_notin
      from ev_setinterleavingptick_ev.prems(1)
      consider (mv_left) tr' where ‹tr = ev a # tr'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts), A)›
        | (mv_right) ts' where ‹ts = ev a # ts'› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts'), A)›
        by (auto simp add: ‹a ∉ A› elim: Cons_ev_setinterleavesptickE)
      thus ?thesis
      proof cases
        case mv_left
        from ev_setinterleavingptick_ev.hyps(4)[OF mvL_notin(1, 2) mv_left(2) mvL_notin(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr', tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A) ∧
             tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases tw) (auto simp add: mv_left(1) mvL_notin(1, 3)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      next
        case mv_right
        from ev_setinterleavingptick_ev.hyps(4)[OF mvL_notin(1, 2) mv_right(2) mvL_notin(4)]
        obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
          ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts', ev b # tu), A)› by blast
        hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev a # tw), A) ∧
             ev a # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
          by (cases tr) (auto simp add: mv_right(1) mvL_notin(1, 3)
              setinterleavingptick_simps split: eventptick.split)
        thus ?thesis ..
      qed
    qed
  next
    case (ev_setinterleavingptick_tick a tt s tu)
    from ev_setinterleavingptick_tick.prems(2) obtain tv'
      where ‹a ∉ A› ‹tv = ev a # tv'›
        and $ : ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, ✓(s) # tu), A)›
      by (auto split: if_split_asm)
    from ev_setinterleavingptick_tick.prems(1)
    have ‹tr ≠ [] ∧ hd tr = ev a ∧ tt setinterleaves✓⇘(⊗✓1)⇙ ((tl tr, ts), A) ∨
        ts ≠ [] ∧ hd ts = ev a ∧ tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, tl ts), A)›
      by (auto simp add: ‹a ∉ A› elim: Cons_ev_setinterleavesptickE)
    thus ?case
    proof (elim disjE conjE)
      assume ‹tr ≠ []› ‹hd tr = ev a› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tl tr, ts), A)›
      from ev_setinterleavingptick_tick.hyps[OF ‹a ∉ A› this(3) "$"]
      obtain tw where * : ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙((tl tr, tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ✓(s) # tu), A)› by blast
      from "*"(1) have ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
        by (subst list.collapse[OF ‹tr ≠ []›, symmetric])
          (cases tw, auto simp add: ‹a ∉ A› ‹hd tr = ev a› ‹tv = ev a # tv'›
            setinterleavingptick_simps split: eventptick.split)
      with "*"(2) show ?case by blast
    next
      assume ‹ts ≠ []› ‹hd ts = ev a› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, tl ts), A)›
      from ev_setinterleavingptick_tick.hyps[OF ‹a ∉ A› this(3) "$"]
      obtain tw where * : ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
        ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((tl ts, ✓(s) # tu), A)› by blast
      from "*"(2) have ‹ev a # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ✓(s) # tu), A)›
        by (subst list.collapse[OF ‹ts ≠ []›, symmetric])
          (simp add: ‹a ∉ A› ‹tv = ev a # tv'› ‹hd ts = ev a›)
      moreover from "*"(1)
      have ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev a # tw), A)›
        by (cases tr, auto simp add: ‹a ∉ A› ‹tv = ev a # tv'› setinterleavingptick_simps
            split: eventptick.split)
      ultimately show ?case by blast
    qed
  next
    case (tick_setinterleavingptick_ev rt tt b tu)
    from tick_setinterleavingptick_ev.prems(1)
    obtain rr rs tr' ts' where ‹(rr ⊗✓1 rs) = ⌊rt⌋› ‹tr = ✓(rr) # tr'› ‹ts = ✓(rs) # ts'›
      by (auto elim: Cons_tick_setinterleavesptickE)
    from tick_setinterleavingptick_ev.prems(2) obtain tv'
      where ‹b ∉ A› ‹tv = ev b # tv'›
        and $ : ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((✓(rt) # tt, tu), A)›
      by (auto split: if_split_asm)
    from tick_setinterleavingptick_ev.hyps[OF ‹b ∉ A› tick_setinterleavingptick_ev.prems(1) "$"]
    obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A)›
      ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A)› by blast
    hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ev b # tw), A) ∧
         ev b # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ev b # tu), A)›
      by (simp add: ‹b ∉ A› ‹tv = ev b # tv'› ‹tr = ✓(rr) # tr'› ‹ts = ✓(rs) # ts'›)
    thus ?case ..
  next
    case (tick_setinterleavingptick_tick rt tt ru tu)
    from tick_setinterleavingptick_tick.prems(1)
    obtain rr rs tr' ts' where ‹rr ⊗✓1 rs = ⌊rt⌋› ‹tr = ✓(rr) # tr'› ‹ts = ✓(rs) # ts'›
      ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts'), A)›
      by (auto elim: Cons_tick_setinterleavesptickE)
    from tick_setinterleavingptick_tick.prems(2)
    obtain rv tv' where ‹rt ⊗✓2 ru = ⌊rv⌋› ‹tv = ✓(rv) # tv'›
      ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A)›
      by (auto split: option.split_asm)
    from ‹rr ⊗✓1 rs = ⌊rt⌋› ‹rt ⊗✓2 ru = ⌊rv⌋› obtain rw where ‹rs ⊗✓4 ru = ⌊rw⌋›
      by (metis None_assms_tick_join(3) not_None_eq option.sel)
    from ‹rs ⊗✓4 ru = ⌊rw⌋› ‹rr ⊗✓1 rs = ⌊rt⌋› ‹rt ⊗✓2 ru = ⌊rv⌋›
    obtain rx where ‹rr ⊗✓3 rw = ⌊rx⌋›
      by (metis None_assms_tick_join(4) option.distinct(1) option.exhaust_sel option.sel)
    have ‹⊗✓2⇒⊗✓3 rv = rx›
      by (metis ‹rr ⊗✓1 rs = ⌊rt⌋› ‹rr ⊗✓3 rw = ⌊rx⌋› ‹rs ⊗✓4 ru = ⌊rw⌋›
          ‹rt ⊗✓2 ru = ⌊rv⌋› tick_assoc_ren_hyp option.sel)
    from tick_setinterleavingptick_tick.hyps
      [OF ‹rt ⊗✓2 ru = ⌊rv⌋› ‹tt setinterleaves✓⇘(⊗✓1)⇙ ((tr', ts'), A)›
        ‹tv' setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A)›]
    obtain tw where ‹?map_event tv' setinterleaves✓⇘(⊗✓3)⇙ ((tr', tw), A)›
      ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts', tu), A)› by blast
    hence ‹?map_event tv setinterleaves✓⇘(⊗✓3)⇙ ((tr, ✓(rw) # tw), A) ∧
          ✓(rw) # tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, ✓(ru) # tu), A)›
      by (simp add: ‹tr = ✓(rr) # tr'› ‹ts = ✓(rs) # ts'› ‹tv = ✓(rv) # tv'›
          ‹rs ⊗✓4 ru = ⌊rw⌋› ‹rr ⊗✓3 rw = ⌊rx⌋› ‹⊗✓2⇒⊗✓3 rv = rx›)
    thus ?case ..
  qed
qed



lemma (in Syncptick_assoc_locale) setinterleavesptick_assoc_right :
  ‹tw setinterleaves✓⇘(⊗✓4)⇙ ((ts, tu), A) ⟹
   tx setinterleaves✓⇘(⊗✓3)⇙ ((tr, tw), A) ⟹
   ∃tt. map (map_eventptick id ⊗✓3⇒⊗✓2) tx setinterleaves✓⇘(⊗✓2)⇙ ((tt, tu), A) ∧
        tt setinterleaves✓⇘(⊗✓1)⇙ ((tr, ts), A)›
  by (subst (1 2) setinterleavesptick_sym, subst (asm) (1 2) setinterleavesptick_sym)
    (fact Syncptick_assoc_locale_sym.setinterleavesptick_assoc_left)



subsection ‹Associativity›

context Syncptick_assoc_locale
begin

notation Syncptick1.Syncptick (‹(_ ⟦_⟧✓1 _)› [70, 0, 71] 70)
notation Syncptick2.Syncptick (‹(_ ⟦_⟧✓2 _)› [70, 0, 71] 70)
notation Syncptick3.Syncptick (‹(_ ⟦_⟧✓3 _)› [70, 0, 71] 70)
notation Syncptick4.Syncptick (‹(_ ⟦_⟧✓4 _)› [70, 0, 71] 70)


lemma Syncptick_assoc_oneside :
  ‹P ⟦S⟧✓3 (Q ⟦S⟧✓4 R) ⊑FD RenamingTick (P ⟦S⟧✓1 Q ⟦S⟧✓2 R) ⊗✓2⇒⊗✓3› (is ‹?lhs ⊑FD ?rhs›)
proof -
  let ?map_event = ‹λt. map (map_eventptick id ⊗✓2⇒⊗✓3) t›
  let ?map_event_conv = ‹λt. map (map_eventptick id ⊗✓3⇒⊗✓2) t›
  show ‹?lhs ⊑FD ?rhs›
  proof (rule failure_divergence_refine_optimizedI)
    fix t assume ‹t ∈ 𝒟 ?rhs›
    then obtain t1 t2 where ‹t = ?map_event t1 @ t2›
      ‹tF t1› ‹ftF t2› ‹t1 ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
      unfolding D_Renaming by blast
    from ‹t1 ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)› obtain t11 t12 t_P_Q t_R
      where * : ‹t1 = t11 @ t12› ‹tF t11› ‹ftF t12›
        ‹t11 setinterleaves✓⇘(⊗✓2)⇙ ((t_P_Q, t_R), S)›
        ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q) ∧ t_R ∈ 𝒯 R ∨
         t_P_Q ∈ 𝒯 (P ⟦S⟧✓1 Q) ∧ t_P_Q ∉ 𝒟 (P ⟦S⟧✓1 Q) ∧ t_R ∈ 𝒟 R›
      unfolding Syncptick2.D_Syncptick using D_T by blast
    from "*"(5) show ‹t ∈ 𝒟 ?lhs›
    proof (elim disjE conjE)
      assume ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)› ‹t_R ∈ 𝒯 R›
      from ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)› obtain t_P_Q1 t_P_Q2 t_P t_Q
        where ** : ‹t_P_Q = t_P_Q1 @ t_P_Q2› ‹tF t_P_Q1› ‹ftF t_P_Q2›
          ‹t_P_Q1 setinterleaves✓⇘(⊗✓1)⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 P ∧ t_Q ∈ 𝒯 Q ∨ t_P ∈ 𝒯 P ∧ t_Q ∈ 𝒟 Q›
        unfolding Syncptick1.D_Syncptick by blast
      from "*"(4)[unfolded "**"(1), THEN setinterleavesptick_appendL]
      obtain t111 t112 t_R1 t_R2
        where *** : ‹t11 = t111 @ t112› ‹t_R = t_R1 @ t_R2›
          ‹t111 setinterleaves✓⇘(⊗✓2)⇙ ((t_P_Q1, t_R1), S)›
          ‹t112 setinterleaves✓⇘(⊗✓2)⇙ ((t_P_Q2, t_R2), S)› by blast
      from setinterleavesptick_assoc_left[OF "**"(4) "***"(3)]
      obtain t_Q_R where **** : ‹?map_event t111 setinterleaves✓⇘(⊗✓3)⇙ ((t_P, t_Q_R), S)›
        ‹t_Q_R setinterleaves✓⇘(⊗✓4)⇙ ((t_Q, t_R1), S)› by blast
      have ‹tF (?map_event t1)›
        by (simp add: ‹tF t1› map_eventptick_tickFree)
      moreover have ‹ftF (?map_event (t112 @ t12) @ t2)›
        by (metis "*"(1) "***"(1) ‹ftF t2› ‹tF t1› front_tickFree_append
            map_eventptick_tickFree tickFree_append_iff)
      moreover from "**"(5)
      have ‹t_P ∈ 𝒟 P ∧ t_Q_R ∈ 𝒯 (Q ⟦S⟧✓4 R) ∨ t_P ∈ 𝒯 P ∧ t_Q_R ∈ 𝒟 (Q ⟦S⟧✓4 R)›
      proof (elim disjE conjE)
        assume ‹t_P ∈ 𝒟 P› ‹t_Q ∈ 𝒯 Q›
        hence ‹t_P ∈ 𝒟 P ∧ t_Q_R ∈ 𝒯 (Q ⟦S⟧✓4 R)› 
          by (simp add: Syncptick4.T_Syncptick)
            (metis "****"(2) "***"(2) ‹t_R ∈ 𝒯 R› is_processT3_TR_append)
        thus ?thesis ..
      next
        assume ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒟 Q›
        from "**"(2, 4) have ‹tF t_Q› by (simp add: tickFree_setinterleavesptick_iff)
        with "****"(2) setinterleavesptick_tickFree_imp have ‹tF t_Q_R› by blast
        moreover from "***"(2) ‹t_R ∈ 𝒯 R› is_processT3_TR_append have ‹t_R1 ∈ 𝒯 R› by blast
        ultimately have ‹t_P ∈ 𝒯 P ∧ t_Q_R ∈ 𝒟 (Q ⟦S⟧✓4 R)›
          unfolding Syncptick4.D_Syncptick
          using "****"(2) ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒟 Q› front_tickFree_Nil by blast
        thus ?thesis ..
      qed
      ultimately show ‹t ∈ 𝒟 ?lhs›
        using "****"(1) by (auto simp add: ‹t = ?map_event t1 @ t2›
            "*"(1) "***"(1) Syncptick3.D_Syncptick)
    next
      assume ‹t_P_Q ∈ 𝒯 (P ⟦S⟧✓1 Q)› ‹t_P_Q ∉ 𝒟 (P ⟦S⟧✓1 Q)› ‹t_R ∈ 𝒟 R›
      from this(1, 2) obtain t_P t_Q
        where ** : ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t_P_Q setinterleaves✓⇘(⊗✓1)⇙ ((t_P, t_Q), S)›
        unfolding Syncptick1.Syncptick_projs by blast
      from setinterleavesptick_assoc_left[OF "**"(3) "*"(4)] obtain t_Q'
        where *** : ‹?map_event t11 setinterleaves✓⇘(⊗✓3)⇙ ((t_P, t_Q'), S)›
          ‹t_Q' setinterleaves✓⇘(⊗✓4)⇙ ((t_Q, t_R), S)› by blast
      from "*"(2) "**"(2) "***" ‹t_R ∈ 𝒟 R› have ‹t_Q' ∈ 𝒟 (Q ⟦S⟧✓4 R)›
        by (simp add: Syncptick4.D_Syncptick)
          (metis append.right_neutral front_tickFree_Nil
            map_eventptick_tickFree tickFree_setinterleavesptick_iff)
      moreover have ‹t = ?map_event t11 @ (?map_event t12 @ t2)›
        by (simp add: "*"(1) ‹t = ?map_event t1 @ t2›)
      moreover have ‹tF (?map_event t11)›
        by (simp add: "*"(2) map_eventptick_tickFree)
      moreover from "*"(1) ‹ftF t2› ‹tF t1› have ‹ftF (?map_event t12 @ t2)›
        using front_tickFree_append map_eventptick_tickFree tickFree_append_iff by blast
      ultimately show ‹t ∈ 𝒟 ?lhs›
        unfolding Syncptick3.D_Syncptick using "**"(1) "***"(1) by blast
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹𝒟 ?rhs ⊆ 𝒟 ?lhs›
    then consider ‹t ∈ 𝒟 ?rhs›
      | t1 where ‹t = ?map_event t1› ‹t ∉ 𝒟 ?rhs›
        ‹(t1, map_eventptick id ⊗✓2⇒⊗✓3 -` X) ∈ ℱ (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
      unfolding Renaming_projs by blast
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      assume ‹t ∈ 𝒟 ?rhs›
      with ‹𝒟 ?rhs ⊆ 𝒟 ?lhs› have ‹t ∈ 𝒟 ?lhs› by blast
      thus ‹(t, X) ∈ ℱ ?lhs› by (fact is_processT8)
    next
      fix t1 assume * : ‹t = ?map_event t1› ‹t ∉ 𝒟 ?rhs›
        ‹(t1, map_eventptick id ⊗✓2⇒⊗✓3 -` X) ∈ ℱ (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
      from "*"(1) ‹t ∉ 𝒟 ?rhs› have ‹t1 ∉ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
        by (cases ‹tF t1›, simp_all add: D_Renaming)
          (use front_tickFree_Nil in blast,
            metis D_imp_front_tickFree front_tickFree_append_iff is_processT9
            map_append map_eventptick_front_tickFree
            nonTickFree_n_frontTickFree non_tickFree_tick tickFree_Nil)
      with "*"(3) obtain t_P_Q X_P_Q t_R X_R
        where ** : ‹(t_P_Q, X_P_Q) ∈ ℱ (P ⟦S⟧✓1 Q)› ‹(t_R, X_R) ∈ ℱ R›
          ‹t1 setinterleaves✓⇘(⊗✓2)⇙ ((t_P_Q, t_R), S)›
          ‹map_eventptick id ⊗✓2⇒⊗✓3 -` X ⊆ super_ref_Syncptick (⊗✓2) X_P_Q S X_R›
        unfolding Syncptick2.Syncptick_projs by blast
      from "**"(1) consider ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)›
        | (fail) t_P X_P t_Q X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t_P_Q setinterleaves✓⇘(⊗✓1)⇙ ((t_P, t_Q), S)›
          ‹X_P_Q ⊆ super_ref_Syncptick (⊗✓1) X_P S X_Q›
        unfolding Syncptick1.Syncptick_projs by blast
      thus ‹(t, X) ∈ ℱ ?lhs›
      proof cases
        assume ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)›
        have ‹t1 ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
        proof (cases ‹tF t_P_Q›)
          assume ‹tF t_P_Q›
          with "**"(3)[THEN setinterleavesptick_tickFree_imp[rotated]] have ‹tF t1› by simp
          with "**"(3) "**"(2)[THEN F_T] ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)›
          show ‹t1 ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
            by (simp add: Syncptick2.D_Syncptick)
              (meson front_tickFree_Nil self_append_conv)
        next
          assume ‹¬ tF t_P_Q›
          then obtain t_P_Q' r where ‹tF t_P_Q'› ‹t_P_Q = t_P_Q' @ [✓(r)]›
            by (metis D_imp_front_tickFree ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)› butlast_snoc
                front_tickFree_iff_tickFree_butlast nonTickFree_n_frontTickFree)
          moreover from "**"(2,3) ‹¬ tF t_P_Q› obtain t_R' s
            where ‹tF t_R'› ‹t_R = t_R' @ [✓(s)]›
            by (metis  F_imp_front_tickFree butlast_snoc front_tickFree_iff_tickFree_butlast
                nonTickFree_n_frontTickFree setinterleavesptick_tickFree_imp)
          ultimately obtain r_s t1' where ‹t1 = t1' @ [✓(r_s)]›
            ‹t1' setinterleaves✓⇘(⊗✓2)⇙ ((t_P_Q', t_R'), S)›
            using "**"(3) by (auto elim!: setinterleavesptick_snoc_tick_snoc_tickE)
          moreover have ‹t_P_Q' ∈ 𝒟 (P ⟦S⟧✓1 Q)›
            by (metis D_imp_front_tickFree ‹¬ tF t_P_Q› ‹t_P_Q = t_P_Q' @ [✓(r)]›
                ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)› butlast_snoc div_butlast_when_non_tickFree_iff)
          moreover have ‹t_R' ∈ 𝒯 R›
            using "**"(2) F_T ‹t_R = t_R' @ [✓(s)]› is_processT3_TR_append by blast
          ultimately have ‹t1' ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
            by (simp add: Syncptick2.D_Syncptick)
              (metis "**"(3) D_imp_front_tickFree ‹tF t_R'› ‹t_P_Q ∈ 𝒟 (P ⟦S⟧✓1 Q)›
                ‹t_R = t_R' @ [✓(s)]› append.right_neutral butlast_snoc front_tickFree_charn
                front_tickFree_setinterleavesptick_iff tickFree_Nil tickFree_append_iff)
          thus ‹t1 ∈ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)›
            by (simp add: ‹t1 = t1' @ [✓(r_s)]›)
              (metis "*"(3) F_imp_front_tickFree ‹t1 = t1' @ [✓(r_s)]› butlast_snoc
                div_butlast_when_non_tickFree_iff non_tickFree_tick tickFree_append_iff)
        qed
        with ‹t1 ∉ 𝒟 (P ⟦S⟧✓1 Q ⟦S⟧✓2 R)› show ‹(t, X) ∈ ℱ ?lhs› ..
      next
        case fail
        from setinterleavesptick_assoc_left[OF fail(3) "**"(3)] obtain t_Q'
          where *** : ‹?map_event t1 setinterleaves✓⇘(⊗✓3)⇙ ((t_P, t_Q'), S)›
            ‹t_Q' setinterleaves✓⇘(⊗✓4)⇙ ((t_Q, t_R), S)› by blast
        from "**"(2) "***"(2) fail(2)
        have ‹(t_Q', super_ref_Syncptick (⊗✓4) X_Q S X_R) ∈ ℱ (Q ⟦S⟧✓4 R)›
          by (auto simp add: Syncptick4.F_Syncptick)
        moreover have ‹t setinterleaves✓⇘(⊗✓3)⇙ ((t_P, t_Q'), S)›
          by (simp add: "*"(1) "***"(1))
        have ‹X ⊆ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
        proof (rule subsetI)
          fix e assume ‹e ∈ X›
          show ‹e ∈ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
          proof (cases e)
            fix a assume ‹e = ev a›
            obtain a' where ‹map_eventptick id ⊗✓2⇒⊗✓3 (ev a') = ev a› by simp
            with ‹e ∈ X› have ‹ev a' ∈ map_eventptick id ⊗✓2⇒⊗✓3 -` X›
              by (simp add: ‹e = ev a›)
            with **(4)[THEN set_mp, OF this] fail(4)
              ‹map_eventptick id ⊗✓2⇒⊗✓3 (ev a') = ev a›
            show ‹e ∈ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
              by (auto simp add: ‹e = ev a› subset_iff super_ref_Syncptick_def)
          next
            fix r_s_t assume ‹e = ✓(r_s_t)›
            show ‹e ∈ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
            proof (cases ‹∃r s t s_t. s ⊗✓4 t = ⌊s_t⌋ ∧ r ⊗✓3 s_t = ⌊r_s_t⌋›)
              assume ‹∃r s t s_t. s ⊗✓4 t = ⌊s_t⌋ ∧ r ⊗✓3 s_t = ⌊r_s_t⌋›
              then obtain r s t s_t
                where $ : ‹s ⊗✓4 t = ⌊s_t⌋› ‹r ⊗✓3 s_t = ⌊r_s_t⌋› by blast
              then obtain r' s' t' r_s'
                where $$ : ‹r' ⊗✓1 s' = ⌊r_s'⌋› ‹r_s' ⊗✓2 t' = ⌊⊗✓3⇒⊗✓2 r_s_t⌋›
                by (metis None_assms_tick_join(1,2) option.collapse option.discI
                    option.sel tick_assoc_ren_conv_hyp)
              have ‹✓(⊗✓3⇒⊗✓2 r_s_t) ∈ map_eventptick id ⊗✓2⇒⊗✓3 -` X›
                by (metis ‹e = ✓(r_s_t)› ‹e ∈ X› "$" eventptick.simps(10)
                    tick_assoc_ren_tick_assoc_ren_conv vimage_eq)
              from **(4)[THEN set_mp, OF this] fail(4)[THEN set_mp, of ‹✓(r_s')›]
              show ‹e ∈ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
                by (simp add: ‹e = ✓(r_s_t)› subset_iff super_ref_Syncptick_def)
                  (metis (no_types, lifting) "$$" None_assms_tick_join(3,4)
                    Syncptick2.inj_tick_join option.collapse option.discI
                    option.sel tick_assoc_ren_hyp tick_assoc_ren_tick_assoc_ren_conv)
            next
              assume ‹∄r s t s_t. s ⊗✓4 t = ⌊s_t⌋ ∧ r ⊗✓3 s_t = ⌊r_s_t⌋›
              thus ‹e ∈ super_ref_Syncptick (⊗✓3) X_P S (super_ref_Syncptick (⊗✓4) X_Q S X_R)›
                by (simp add: ‹e = ✓(r_s_t)› super_ref_Syncptick_def) blast
            qed
          qed
        qed
        ultimately show ‹(t, X) ∈ ℱ ?lhs›
          using "*"(1) "***"(1) fail(1) by (auto simp add: Syncptick3.F_Syncptick)
      qed
    qed
  qed
qed

end



lemma (in Syncptick_locale) strict_ticks_of_Syncptick_subset :
  ‹✓s(P ⟦S⟧✓ Q) ⊆ {r_s |r_s r s. r ⊗✓ s = ⌊r_s⌋ ∧
                                 r ∈ ✓s(P) ∧ s ∈ ✓s(Q)}› (is ‹_ ⊆ ?S›)
proof (rule subsetI, elim strict_ticks_of_memE)
  fix t r_s assume ‹t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)› ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)›
  from ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)› have ‹t @ [✓(r_s)] ∉ 𝒟 (P ⟦S⟧✓ Q)› by (meson is_processT9)
  with ‹t @ [✓(r_s)] ∈ 𝒯 (P ⟦S⟧✓ Q)› obtain t_P t_Q
    where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹t @ [✓(r_s)] setinterleaves✓⇘(⊗✓)⇙ ((t_P, t_Q), S)›
    unfolding Syncptick_projs by blast
  from this(3) show ‹r_s ∈ ?S›
  proof (elim snoc_tick_setinterleavesptickE)
    fix t_P' t_Q' r s
    assume * : ‹r ⊗✓ s = Some r_s› ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
      ‹t setinterleaves✓⇘(⊗✓)⇙ ((t_P', t_Q'), S)›
    have ‹t_P' ∉ 𝒟 P ∧ t_Q' ∉ 𝒟 Q›
    proof (rule ccontr)
      assume ‹¬ (t_P' ∉ 𝒟 P ∧ t_Q' ∉ 𝒟 Q)›
      with ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› have ‹t ∈ 𝒟 (P ⟦S⟧✓ Q)›
        by (simp add: D_Syncptick "*"(2,3,4))
          (metis "*"(4) append.right_neutral append_T_imp_tickFree front_tickFree_Nil
            is_processT3_TR_append not_Cons_self2 setinterleavesptick_tickFree_imp)
      with ‹t ∉ 𝒟 (P ⟦S⟧✓ Q)› show False ..
    qed
    with "*"(2, 3) ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› have ‹r ∈ ✓s(P)› ‹s ∈ ✓s(Q)›
      by (metis is_processT9 strict_ticks_of_memI)+
    with "*"(1) show ‹r_s ∈ ?S› by blast
  qed
qed


theorem (in Syncptick_assoc_locale) Syncptick_assoc :
  ‹P ⟦S⟧✓3 (Q ⟦S⟧✓4 R) = RenamingTick (P ⟦S⟧✓1 Q ⟦S⟧✓2 R) ⊗✓2⇒⊗✓3› (is ‹?lhs = ?rhs›)
proof (rule FD_antisym)
  show ‹?lhs ⊑FD ?rhs› by (fact Syncptick_assoc_oneside)
next
  from Syncptick_assoc_locale_sym.Syncptick_assoc_oneside[of R S Q P]
  have ‹Syncptick2.Syncptick_locale_sym.Syncptick R S
        (Syncptick1.Syncptick_locale_sym.Syncptick Q S P) ⊑FD
        RenamingTick (Syncptick3.Syncptick_locale_sym.Syncptick
        (Syncptick4.Syncptick_locale_sym.Syncptick R S Q) S P) ⊗✓3⇒⊗✓2› .
  also have ‹Syncptick1.Syncptick_locale_sym.Syncptick Q S P = P ⟦S⟧✓1 Q›
    by (simp add: Syncptick1.Syncptick_sym)
  also have ‹Syncptick2.Syncptick_locale_sym.Syncptick R S P_Q = P_Q ⟦S⟧✓2 R› for P_Q
    by (simp add: Syncptick2.Syncptick_sym)
  also have ‹Syncptick4.Syncptick_locale_sym.Syncptick R S Q = Q ⟦S⟧✓4 R›
    by (simp add: Syncptick4.Syncptick_sym)
  also have ‹Syncptick3.Syncptick_locale_sym.Syncptick Q_R S P = P ⟦S⟧✓3 Q_R› for Q_R
    by (simp add: Syncptick3.Syncptick_sym)
  finally have ‹P ⟦S⟧✓1 Q ⟦S⟧✓2 R ⊑FD RenamingTick ?lhs ⊗✓3⇒⊗✓2› .
  hence ‹?rhs ⊑FD RenamingTick (RenamingTick ?lhs ⊗✓3⇒⊗✓2) ⊗✓2⇒⊗✓3›
    by (fact mono_Renaming_FD)
  also have ‹… = RenamingTick ?lhs (⊗✓2⇒⊗✓3 ∘ ⊗✓3⇒⊗✓2)›
    by (simp add: RenamingTick_comp)
  also have ‹… = RenamingTick ?lhs id›
  proof (rule RenamingTick_is_restrictable_on_strict_ticks_of)
    fix r_s_t assume ‹r_s_t ∈ ✓s(P ⟦S⟧✓3 (Q ⟦S⟧✓4 R))›
    with Syncptick3.strict_ticks_of_Syncptick_subset obtain r s_t
      where ‹r ⊗✓3 s_t = ⌊r_s_t⌋› ‹r ∈ ✓s(P)› ‹s_t ∈ ✓s(Q ⟦S⟧✓4 R)› by blast
    from this(3) Syncptick4.strict_ticks_of_Syncptick_subset obtain s t
      where ‹s ⊗✓4 t = ⌊s_t⌋› ‹s ∈ ✓s(Q)› ‹t ∈ ✓s(R)› by blast
    from ‹r ⊗✓3 s_t = ⌊r_s_t⌋› ‹s ⊗✓4 t = ⌊s_t⌋›
    show ‹(⊗✓2⇒⊗✓3 ∘ ⊗✓3⇒⊗✓2) r_s_t = id r_s_t›
      by (auto intro!: tick_assoc_ren_tick_assoc_ren_conv)
  qed
  also have ‹… = ?lhs› by simp
  finally show ‹?rhs ⊑FD ?lhs› .
qed


(*<*)
end
  (*>*)