Theory Step_CSP_PTick_Laws

(***********************************************************************************
 * 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
 ***********************************************************************************)


chapter ‹Communications›

(*<*)
theory Step_CSP_PTick_Laws
  imports Sequential_Composition_Generalized
    Synchronization_Product_Generalized
begin
  (*>*)

section ‹Step Laws›

subsection ‹Sequential Composition›

lemma Mprefix_Seq⇩p⇩t⇩i⇩c⇩k: ‹□a ∈ A → P a ❙;⇩✓ Q = □a ∈ A → (P a ❙;⇩✓ Q)› (is ‹?lhs = ?rhs›)
proof (rule Process_eq_optimizedI)
  show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    by (cases t, auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs Mprefix_projs image_iff Cons_eq_append_conv) blast
next
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (cases t, auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs Mprefix_projs image_iff Cons_eq_map_conv Cons_eq_append_conv)
      (metis event⇩p⇩t⇩i⇩c⇩k.disc(1) event⇩p⇩t⇩i⇩c⇩k.sel(1) tickFree_Cons_iff,
        metis append_Cons event⇩p⇩t⇩i⇩c⇩k.discI(1) event⇩p⇩t⇩i⇩c⇩k.sel(1) tickFree_Cons_iff)
next
  fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
  then consider (F_P) t' where ‹t = map (ev ∘ of_ev) t'›
    ‹(t', ref_Seq⇩p⇩t⇩i⇩c⇩k X) ∈ ℱ (□a ∈ A → P a)› ‹tF t'›
  | (F_Q) t' r u where ‹t = map (ev ∘ of_ev) t' @ u› ‹t' @ [✓(r)] ∈ 𝒯 (□a ∈ A → P a)› ‹tF t'› ‹(u, X) ∈ ℱ (Q r)›
    unfolding Seq⇩p⇩t⇩i⇩c⇩k_projs by fast
  thus ‹(t, X) ∈ ℱ ?rhs›
  proof cases
    case F_P thus ‹(t, X) ∈ ℱ ?rhs›
      by (cases t'; simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs ref_Seq⇩p⇩t⇩i⇩c⇩k_def Mprefix_projs disjoint_iff image_iff)
        (metis IntI event⇩p⇩t⇩i⇩c⇩k.sel(1) rangeI, metis event⇩p⇩t⇩i⇩c⇩k.sel(1))
  next
    case F_Q thus ‹(t, X) ∈ ℱ ?rhs›
      by (cases t) (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs Mprefix_projs Cons_eq_append_conv)+
  qed
next
  fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
  from ‹(t, X) ∈ ℱ ?rhs› consider ‹t = []› ‹X ∩ ev ` A = {}›
    | a t' where ‹t = ev a # t'› ‹a ∈ A› ‹(t', X) ∈ ℱ (P a ❙;⇩✓ Q)›
    unfolding F_Mprefix by blast
  thus ‹(t, X) ∈ ℱ ?lhs›
  proof cases
    show ‹t = [] ⟹ X ∩ ev ` A = {} ⟹ (t, X) ∈ ℱ ?lhs›
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs ref_Seq⇩p⇩t⇩i⇩c⇩k_def F_Mprefix)
  next
    fix a t' assume ‹t = ev a # t'› ‹a ∈ A› ‹(t', X) ∈ ℱ (P a ❙;⇩✓ Q)›
    from ‹(t', X) ∈ ℱ (P a ❙;⇩✓ Q)› ‹t ∉ 𝒟 ?rhs› ‹a ∈ A› ‹t = ev a # t'›
    consider (F_P) t'' where ‹t' = map (ev ∘ of_ev) t''› ‹(t'', ref_Seq⇩p⇩t⇩i⇩c⇩k X) ∈ ℱ (P a)› ‹tF t''›
      | (F_Q) t'' r u where ‹t' = map (ev ∘ of_ev) t'' @ u› ‹t'' @ [✓(r)] ∈ 𝒯 (P a)› ‹tF t''› ‹(u, X) ∈ ℱ (Q r)›
      by (auto simp add: Seq⇩p⇩t⇩i⇩c⇩k_projs D_Mprefix) 
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      case F_P thus ‹(t, X) ∈ ℱ ?lhs›
        by (simp add: Mprefix_projs Seq⇩p⇩t⇩i⇩c⇩k_projs ‹t = ev a # t'› Cons_eq_map_conv)
          (metis ‹a ∈ A› event⇩p⇩t⇩i⇩c⇩k.disc(1) event⇩p⇩t⇩i⇩c⇩k.sel(1) tickFree_Cons_iff)
    next
      case F_Q thus ‹(t, X) ∈ ℱ ?lhs›
        by (simp add: Mprefix_projs Seq⇩p⇩t⇩i⇩c⇩k_projs ‹t = ev a # t'› Cons_eq_map_conv append_eq_Cons_conv)
          (metis (no_types, lifting) ‹a ∈ A› append_Cons comp_apply event⇩p⇩t⇩i⇩c⇩k.disc(1)
            event⇩p⇩t⇩i⇩c⇩k.sel(1) list.simps(9) tickFree_Cons_iff)
    qed
  qed
qed




subsection ‹Synchronization Product›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_bis :
  ‹□a∈(A ∪ A') → P a ⟦S⟧⇩✓ □b∈(B ∪ B') → Q b =
   (□a∈A → (P a ⟦S⟧⇩✓ □b∈(B ∪ B') → Q b)) □
   (□b∈B → (□a∈(A ∪ A') → P a ⟦S⟧⇩✓ Q b)) □
   (□x∈(A' ∩ B') → (P x ⟦S⟧⇩✓ Q x))›
  (is ‹?lhs1 ⟦S⟧⇩✓ ?lhs2 = ?rhs1 □ ?rhs2 □ ?rhs3›) 
  if sets_assms: ‹A ∩ S = {}› ‹A' ⊆ S› ‹B ∩ S = {}› ‹B' ⊆ S›
proof (rule Process_eq_optimizedI)
  fix t assume ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
  then obtain u v t_P t_Q
    where * : ‹t = u @ v› ‹tF u› ‹ftF v›
      ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
      ‹t_P ∈ 𝒟 ?lhs1 ∧ t_Q ∈ 𝒯 ?lhs2 ∨
               t_P ∈ 𝒯 ?lhs1 ∧ t_Q ∈ 𝒟 ?lhs2›
    unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
  from "*"(5) show ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
  proof (elim disjE conjE)
    assume ‹t_P ∈ 𝒟 ?lhs1› ‹t_Q ∈ 𝒯 ?lhs2›
    from ‹t_P ∈ 𝒟 ?lhs1› obtain a t_P'
      where ** : ‹a ∈ A ∨ a ∈ A'› ‹t_P = ev a # t_P'› ‹t_P' ∈ 𝒟 (P a)›
      unfolding D_Mprefix by blast
    from ‹t_Q ∈ 𝒯 ?lhs2› consider ‹t_Q = []›
      | b t_Q' where ‹b ∈ B ∨ b ∈ B'› ‹t_Q = ev b # t_Q'› ‹t_Q' ∈ 𝒯 (Q b)›
      unfolding T_Mprefix by blast
    thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
    proof cases
      assume ‹t_Q = []›
      with "*"(4) obtain u' where ‹a ∉ S› ‹u = ev a # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q), S)›
        by (auto simp add: "**"(2) split: if_split_asm)
      moreover from ‹u = ev a # u'› "*"(2) have ‹tF u'› by simp
      ultimately have ‹t ∈ 𝒟 ?rhs1›
        using "*"(1, 3) "**"(1, 3) ‹t_Q ∈ 𝒯 ?lhs2› ‹A' ⊆ S›
        by (auto simp add: simp add: D_Mprefix D_Sync⇩p⇩t⇩i⇩c⇩k)
      thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
    next
      fix b t_Q' assume *** : ‹b ∈ B ∨ b ∈ B'› ‹t_Q = ev b # t_Q'› ‹t_Q' ∈ 𝒯 (Q b)›
      from "*"(2) have $ : ‹u = ev x # u' ⟹ tF u'› for x u' by simp
      from "*"(4) sets_assms "**"(1) "***"(1)
      consider (mv_both)  u' where ‹a ∈ S› ‹b = a› ‹a ∈ A'› ‹a ∈ B'› ‹u = ev a # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), S)›
      |        (mv_left)  u' where ‹a ∉ S› ‹a ∈ A› ‹u = ev a # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q), S)›
      |        (mv_right) u' where ‹b ∉ S› ‹b ∈ B› ‹u = ev b # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q'), S)›
        by (auto simp add: "**"(2) "***"(2) disjoint_iff
            split: if_split_asm)
      thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
      proof cases
        case mv_both
        have ‹tF u'› by (simp add: "$" mv_both(5))
        with "*"(3) "**"(3) "***"(3) mv_both(2, 6)
        have ‹u' @ v ∈ 𝒟 (P a ⟦S⟧⇩✓ Q a)› by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs3› by (simp add: D_Mprefix "*"(1) mv_both(3-5))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      next
        case mv_left
        have ‹tF u'› by (simp add: "$" mv_left(3))
        with "*"(3) "**"(3) ‹t_Q ∈ 𝒯 ?lhs2› mv_left(4)
        have ‹u' @ v ∈ 𝒟 (P a ⟦S⟧⇩✓ □b∈(B ∪ B') → Q b)› by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs1› by (simp add: D_Mprefix "*"(1) mv_left(2, 3))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      next
        case mv_right
        have ‹tF u'› by (simp add: "$" mv_right(3))
        with "*"(3) "***"(3) mv_right(4) ‹t_P ∈ 𝒟 ?lhs1›
        have ‹u' @ v ∈ 𝒟 (□a∈(A ∪ A') → P a ⟦S⟧⇩✓ Q b)›
          by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs2› by (simp add: D_Mprefix "*"(1) mv_right(2, 3))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      qed
    qed
  next
    assume ‹t_P ∈ 𝒯 ?lhs1› ‹t_Q ∈ 𝒟 ?lhs2›
    from ‹t_Q ∈ 𝒟 ?lhs2› obtain b t_Q'
      where ** : ‹b ∈ B ∨ b ∈ B'› ‹t_Q = ev b # t_Q'› ‹t_Q' ∈ 𝒟 (Q b)›
      unfolding D_Mprefix by blast
    from ‹t_P ∈ 𝒯 ?lhs1› consider ‹t_P = []›
      | a t_P' where ‹a ∈ A ∨ a ∈ A'› ‹t_P = ev a # t_P'› ‹t_P' ∈ 𝒯 (P a)›
      unfolding T_Mprefix by blast
    thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
    proof cases
      assume ‹t_P = []›
      with "*"(4) obtain u' where ‹b ∉ S› ‹u = ev b # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q'), S)›
        by (auto simp add: "**"(2) split: if_split_asm)
      moreover from ‹u = ev b # u'› ‹tF u› have ‹tF u'› by simp
      ultimately have ‹t ∈ 𝒟 ?rhs2›
        using "*"(1, 3) "**"(1, 3) ‹t_P ∈ 𝒯 ?lhs1› ‹B' ⊆ S›
        by (auto simp add: simp add: D_Mprefix D_Sync⇩p⇩t⇩i⇩c⇩k)
      thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
    next
      fix a t_P' assume *** : ‹a ∈ A ∨ a ∈ A'› ‹t_P = ev a # t_P'› ‹t_P' ∈ 𝒯 (P a)›
      from ‹tF u› have $ : ‹u = ev x # u' ⟹ tF u'› for x u' by simp
      from "*"(4) sets_assms "**"(1) "***"(1)
      consider (mv_both)  u' where ‹a ∈ S› ‹b = a› ‹a ∈ A'› ‹a ∈ B'›
        ‹u = ev a # u'› ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), S)›
      |        (mv_left)  u' where ‹a ∉ S› ‹a ∈ A› ‹u = ev a # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q), S)›
      |        (mv_right) u' where ‹b ∉ S› ‹b ∈ B› ‹u = ev b # u'›
        ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q'), S)›
        by (auto simp add: "**"(2) "***"(2) disjoint_iff split: if_split_asm)
      thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
      proof cases
        case mv_both
        have ‹tF u'› by (simp add: "$" mv_both(5))
        with "*"(3) "**"(3) "***"(3) mv_both(2, 6)
        have ‹u' @ v ∈ 𝒟 (P a ⟦S⟧⇩✓ Q a)› by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs3› by (simp add: D_Mprefix "*"(1) mv_both(3-5))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      next
        case mv_left
        have ‹tF u'› by (simp add: "$" mv_left(3))
        with "*"(3) "***"(3) mv_left(4) ‹t_Q ∈ 𝒟 ?lhs2›
        have ‹u' @ v ∈ 𝒟 (P a ⟦S⟧⇩✓ □b∈(B ∪ B') → Q b)› by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs1› by (simp add: D_Mprefix "*"(1) mv_left(2, 3))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      next
        case mv_right
        have ‹tF u'› by (simp add: "$" mv_right(3))
        with "*"(3) "**"(3) ‹t_P ∈ 𝒯 ?lhs1› mv_right(4)
        have ‹u' @ v ∈ 𝒟 (□a∈(A ∪ A') → P a ⟦S⟧⇩✓ Q b)›
          by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        hence ‹t ∈ 𝒟 ?rhs2› by (simp add: D_Mprefix "*"(1) mv_right(2, 3))
        thus ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› by (simp add: D_Det)
      qed
    qed
  qed
next

  fix t assume ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
  consider ‹t = []› | r_s t' where ‹t = ✓(r_s) # t'› | x t' where ‹t = ev x # t'›
    by (metis event⇩p⇩t⇩i⇩c⇩k.exhaust neq_Nil_conv)
  thus ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
  proof cases
    assume ‹t = []›
    with ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› have False
      by (simp add: D_Det D_Mprefix)
    thus ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
  next
    fix r_s t' assume ‹t = ✓(r_s) # t'›
    with ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› have False
      by (simp add: D_Det D_Mprefix)
    thus ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
  next
    fix x t' assume ‹t = ev x # t'›
    with ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› consider
      (mv_left)  ‹x ∈ A› ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ ?lhs2)›
      | (mv_right) ‹x ∈ B› ‹t' ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ Q x)›
      | (mv_both)  ‹x ∈ A'› ‹x ∈ B'› ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ Q x)›
      by (auto simp add: D_Det D_Mprefix)
    thus ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
    proof cases
      case mv_left
      from ‹x ∈ A› ‹A ∩ S = {}› have ‹x ∉ S› by blast
      from mv_left(2) obtain u v t_P t_Q
        where * : ‹t' = u @ v› ‹tF u› ‹ftF v›
          ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 (P x) ∧ t_Q ∈ 𝒯 ?lhs2 ∨
                   t_P ∈ 𝒯 (P x) ∧ t_Q ∈ 𝒟 ?lhs2›
        unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
      have ‹t = (ev x # u) @ v› by (simp add: "*"(1) ‹t = ev x # t'›)
      moreover have ‹tF (ev x # u)› by (simp add: "*"(2))
      moreover from "*"(4) have ‹ev x # u setinterleaves⇩✓⇘tick_join⇙ ((ev x # t_P, t_Q), S)›
        by (cases t_Q) (auto simp add: ‹x ∉ S› setinterleaving⇩p⇩t⇩i⇩c⇩k_simps split: event⇩p⇩t⇩i⇩c⇩k.split)
      moreover from "*"(5) mv_left(1)
      have ‹ev x # t_P ∈ 𝒟 ?lhs1 ∧ t_Q ∈ 𝒯 ?lhs2 ∨
            ev x # t_P ∈ 𝒯 ?lhs1 ∧ t_Q ∈ 𝒟 ?lhs2› by (simp add: Mprefix_projs)
      ultimately show ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
        using "*"(3) by (simp (no_asm) add: D_Sync⇩p⇩t⇩i⇩c⇩k) blast
    next
      case mv_right
      from ‹x ∈ B› ‹B ∩ S = {}› have ‹x ∉ S› by blast
      from mv_right(2) obtain u v t_P t_Q
        where * : ‹t' = u @ v› ‹tF u› ‹ftF v›
          ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 ?lhs1 ∧ t_Q ∈ 𝒯 (Q x) ∨
                   t_P ∈ 𝒯 ?lhs1 ∧ t_Q ∈ 𝒟 (Q x)›
        unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
      have ‹t = (ev x # u) @ v› by (simp add: "*"(1) ‹t = ev x # t'›)
      moreover have ‹tF (ev x # u)› by (simp add: "*"(2))
      moreover from "*"(4) have ‹ev x # u setinterleaves⇩✓⇘tick_join⇙ ((t_P, ev x # t_Q), S)›
        by (cases t_P) (auto simp add: ‹x ∉ S› setinterleaving⇩p⇩t⇩i⇩c⇩k_simps split: event⇩p⇩t⇩i⇩c⇩k.split)
      moreover from "*"(5) mv_right(1)
      have ‹t_P ∈ 𝒟 ?lhs1 ∧ ev x # t_Q ∈ 𝒯 ?lhs2 ∨
            t_P ∈ 𝒯 ?lhs1 ∧ ev x # t_Q ∈ 𝒟 ?lhs2› by (simp add: Mprefix_projs)
      ultimately show ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
        using "*"(3) by (simp (no_asm) add: D_Sync⇩p⇩t⇩i⇩c⇩k) blast
    next
      case mv_both
      from ‹x ∈ A'› ‹A' ⊆ S› have ‹x ∈ S› by blast
      from mv_both(3) obtain u v t_P t_Q
        where * : ‹t' = u @ v› ‹tF u› ‹ftF v›
          ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹t_P ∈ 𝒟 (P x) ∧ t_Q ∈ 𝒯 (Q x) ∨
                   t_P ∈ 𝒯 (P x) ∧ t_Q ∈ 𝒟 (Q x)›
        unfolding D_Sync⇩p⇩t⇩i⇩c⇩k by blast
      have ‹t = (ev x # u) @ v› by (simp add: "*"(1) ‹t = ev x # t'›)
      moreover have ‹tF (ev x # u)› by (simp add: "*"(2))
      moreover from "*"(4) have ‹ev x # u setinterleaves⇩✓⇘tick_join⇙ ((ev x # t_P, ev x # t_Q), S)›
        by (auto simp add: ‹x ∈ S›)
      moreover from "*"(5) mv_both(1, 2)
      have ‹ev x # t_P ∈ 𝒟 ?lhs1 ∧ ev x # t_Q ∈ 𝒯 ?lhs2 ∨
            ev x # t_P ∈ 𝒯 ?lhs1 ∧ ev x # t_Q ∈ 𝒟 ?lhs2› by (simp add: Mprefix_projs)
      ultimately show ‹t ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
        using "*"(3) by (simp (no_asm) add: D_Sync⇩p⇩t⇩i⇩c⇩k) blast
    qed
  qed
next

  fix t X assume ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ‹t ∉ 𝒟 (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
  then obtain t_P t_Q X_P X_Q
    where fail : ‹(t_P, X_P) ∈ ℱ ?lhs1› ‹(t_Q, X_Q) ∈ ℱ ?lhs2›
      ‹t setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
      ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P S X_Q›
    unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
  consider ‹t = []› | r_s t' where ‹t = ✓(r_s) # t'› | a t' where ‹t = ev a # t'›
    by (metis event⇩p⇩t⇩i⇩c⇩k.exhaust neq_Nil_conv)
  thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
  proof cases
    assume ‹t = []›
    with Nil_setinterleaves⇩p⇩t⇩i⇩c⇩k fail(3) have ‹t_P = []› ‹t_Q = []› by blast+
    with fail(1, 2) have ‹X_P ∩ ev ` (A ∪ A') = {}› ‹X_Q ∩ ev ` (B ∪ B') = {}› 
      by (simp_all add: F_Mprefix)
    with fail(4) ‹A ∩ S = {}› ‹B ∩ S = {}› show ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
      by (simp add: ‹t = []› Det_projs Mprefix_projs super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def)
        (use event⇩p⇩t⇩i⇩c⇩k.distinct(1) in blast)
  next
    fix r_s t' assume ‹t = ✓(r_s) # t'›
    hence ‹t = [✓(r_s)]›
      by (metis F_imp_front_tickFree ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
          event⇩p⇩t⇩i⇩c⇩k.disc(2) front_tickFree_Cons_iff)
    with fail(3) obtain r s where ‹tick_join r s = Some r_s›
      by (auto elim: Cons_tick_setinterleaves⇩p⇩t⇩i⇩c⇩kE)
    from ‹t = [✓(r_s)]› fail(3) ‹tick_join r s = Some r_s›
    have ‹t_P = [✓(r)]›
      by (auto dest: inj_tick_join Nil_setinterleaves⇩p⇩t⇩i⇩c⇩k
          elim: Cons_tick_setinterleaves⇩p⇩t⇩i⇩c⇩kE)
    with fail(1) ‹t = [✓(r_s)]› have False by (simp add: F_Mprefix)
    thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)› ..
  next
    fix a t' assume ‹t = ev a # t'›
    from fail(1-3) sets_assms consider
      (mv_left)  t_P' where
      ‹a ∉ S› ‹a ∈ A› ‹t_P = ev a # t_P'› ‹(t_P', X_P) ∈ ℱ (P a)›
      ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q), S)›
    | (mv_right) t_Q' where
      ‹a ∉ S› ‹a ∈ B› ‹t_Q = ev a # t_Q'› ‹(t_Q', X_Q) ∈ ℱ (Q a)›
      ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q'), S)›
    | (mv_both) t_P' t_Q' where
      ‹a ∈ S› ‹a ∈ A'› ‹a ∈ B'› ‹t_P = ev a # t_P'› ‹t_Q = ev a # t_Q'›
      ‹(t_P', X_P) ∈ ℱ (P a)› ‹(t_Q', X_Q) ∈ ℱ (Q a)› ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), S)›
      by (unfold ‹t = ev a # t'›, elim Cons_ev_setinterleaves⇩p⇩t⇩i⇩c⇩kE)
        (simp_all add: F_Mprefix subset_iff disjoint_iff, blast+)
    thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
    proof cases
      case mv_left
      with fail(2, 4) have ‹(t, X) ∈ ℱ ?rhs1›
        by (subst F_Mprefix) (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k ‹t = ev a # t'›)
      thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
        by (simp add: F_Det ‹t = ev a # t'›)
    next
      case mv_right
      with fail(1, 4) have ‹(t, X) ∈ ℱ ?rhs2›
        by (subst F_Mprefix) (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k ‹t = ev a # t'›)
      thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
        by (simp add: F_Det ‹t = ev a # t'›)
    next
      case mv_both
      with fail(4) have ‹(t, X) ∈ ℱ ?rhs3›
        by (auto simp add: F_Mprefix F_Sync⇩p⇩t⇩i⇩c⇩k ‹t = ev a # t'›)
      thus ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
        by (simp add: F_Det ‹t = ev a # t'›)
    qed
  qed
next

  fix t X assume ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
    ‹t ∉ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
  consider ‹t = []› | r_s t' where ‹t = ✓(r_s) # t'› | a t' where ‹t = ev a # t'›
    by (metis event⇩p⇩t⇩i⇩c⇩k.exhaust neq_Nil_conv)
  thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
  proof cases
    define X_P where ‹X_P ≡ {ev a |a. ev a ∈ X ∧ a ∈ - (A ∪ A')} ∪
                             {✓(r) |r_s r s. tick_join r s = Some r_s ∧ ✓(r_s) ∈ X}›
    define X_Q where ‹X_Q ≡ {ev b |b. ev b ∈ X ∧ b ∈ - (B ∪ B')} ∪
                             {✓(s) |r_s r s. tick_join r s = Some r_s ∧ ✓(r_s) ∈ X}›
    assume ‹t = []›
    with ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
    have ‹X ∩ ev ` A = {} ∧ X ∩ ev ` B = {} ∧ X ∩ ev ` (A' ∩ B') = {}›
      unfolding Det_projs F_Mprefix by auto
    with sets_assms(2, 4) have ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P S X_Q›
      by (simp add: super_ref_Sync⇩p⇩t⇩i⇩c⇩k_def X_P_def X_Q_def
          subset_iff disjoint_iff image_iff)
        (metis IntI event⇩p⇩t⇩i⇩c⇩k.exhaust)
    moreover have ‹([], X_P) ∈ ℱ ?lhs1› by (auto simp add: F_Mprefix X_P_def)
    moreover have ‹([], X_Q) ∈ ℱ ?lhs2› by (auto simp add: F_Mprefix X_Q_def)
    ultimately show ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
      by (simp add: ‹t = []› F_Sync⇩p⇩t⇩i⇩c⇩k) (use Nil_setinterleaving⇩p⇩t⇩i⇩c⇩k_Nil in blast)
  next
    fix r_s t' assume ‹t = ✓(r_s) # t'›
    with ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
    have False by (simp add: F_Det F_Mprefix)
    thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
  next
    fix x t' assume ‹t = ev x # t'›
    with ‹(t, X) ∈ ℱ (?rhs1 □ ?rhs2 □ ?rhs3)›
    consider (mv_left)  ‹x ∈ A› ‹(t', X) ∈ ℱ (P x ⟦S⟧⇩✓ ?lhs2)›
      |      (mv_right) ‹x ∈ B› ‹(t', X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ Q x)›
      |      (mv_both)  ‹x ∈ A'› ‹x ∈ B'› ‹(t', X) ∈ ℱ (P x ⟦S⟧⇩✓ Q x)›
      unfolding F_Det F_Mprefix by auto
    thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
    proof cases
      case mv_left
      from mv_left(2) consider ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ ?lhs2)›
        | (fail) t_P t_Q X_P X_Q where
          ‹(t_P, X_P) ∈ ℱ (P x)› ‹(t_Q, X_Q) ∈ ℱ ?lhs2›
          ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P S X_Q›
        unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
      thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
      proof cases
        assume ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ ?lhs2)›
        hence ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
          by (simp add: D_Det D_Mprefix ‹t = ev x # t'› mv_left(1))
        with ‹t ∉ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› have False ..
        thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
      next
        case fail
        have ‹(ev x # t_P, X_P) ∈ ℱ ?lhs1›  
          by (simp add: F_Mprefix fail(1) mv_left(1))
        moreover from ‹t = ev x # t'› fail(3) mv_left(1) ‹A ∩ S = {}›
        have ‹t setinterleaves⇩✓⇘tick_join⇙ ((ev x # t_P, t_Q), S)›
          by (cases t_Q) (auto simp add: setinterleaving⇩p⇩t⇩i⇩c⇩k_simps split: event⇩p⇩t⇩i⇩c⇩k.split)
        ultimately show ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
          using fail(2, 4) by (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k)
      qed
    next
      case mv_right
      from mv_right(2) consider ‹t' ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ Q x)›
        | (fail) t_P t_Q X_P X_Q where
          ‹(t_P, X_P) ∈ ℱ ?lhs1› ‹(t_Q, X_Q) ∈ ℱ (Q x)›
          ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)›
          ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P S X_Q›
        unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
      thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
      proof cases
        assume ‹t' ∈ 𝒟 (?lhs1 ⟦S⟧⇩✓ Q x)›
        hence ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
          by (simp add: D_Det D_Mprefix ‹t = ev x # t'› mv_right(1))
        with ‹t ∉ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› have False ..
        thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
      next
        case fail
        have ‹(ev x # t_Q, X_Q) ∈ ℱ ?lhs2›  
          by (simp add: F_Mprefix fail(2) mv_right(1))
        moreover from ‹t = ev x # t'› fail(3) mv_right(1) ‹B ∩ S = {}›
        have ‹t setinterleaves⇩✓⇘tick_join⇙ ((t_P, ev x # t_Q), S)›
          by (cases t_P) (auto simp add: setinterleaving⇩p⇩t⇩i⇩c⇩k_simps split: event⇩p⇩t⇩i⇩c⇩k.split)
        ultimately show ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
          using fail(1, 4) by (auto simp add: F_Sync⇩p⇩t⇩i⇩c⇩k)
      qed
    next
      case mv_both
      from mv_both(3) consider ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ Q x)›
        | (fail) t_P t_Q X_P X_Q where
          ‹(t_P, X_P) ∈ ℱ (P x)› ‹(t_Q, X_Q) ∈ ℱ (Q x)›
          ‹t' setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), S)› ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P S X_Q›
        unfolding Sync⇩p⇩t⇩i⇩c⇩k_projs by blast
      thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
      proof cases
        assume ‹t' ∈ 𝒟 (P x ⟦S⟧⇩✓ Q x)›
        hence ‹t ∈ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)›
          by (simp add: D_Det D_Mprefix ‹t = ev x # t'› mv_both(1, 2))
        with ‹t ∉ 𝒟 (?rhs1 □ ?rhs2 □ ?rhs3)› have False ..
        thus ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)› ..
      next
        case fail
        have ‹(ev x # t_P, X_P) ∈ ℱ ?lhs1›  
          by (simp add: F_Mprefix fail(1) mv_both(1))
        moreover have ‹(ev x # t_Q, X_Q) ∈ ℱ ?lhs2›  
          by (simp add: F_Mprefix fail(2) mv_both(2))
        moreover from ‹t = ev x # t'› fail(3) mv_both(1) ‹A' ⊆ S›
        have ‹t setinterleaves⇩✓⇘tick_join⇙ ((ev x # t_P, ev x # t_Q), S)› by auto
        ultimately show ‹(t, X) ∈ ℱ (?lhs1 ⟦S⟧⇩✓ ?lhs2)›
          using fail(4) by (simp (no_asm) add: F_Sync⇩p⇩t⇩i⇩c⇩k) blast
      qed
    qed
  qed
qed


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix:
  ―‹This version is easier to use.›
  ‹□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b =
   (□a∈(A - S) → (P a ⟦S⟧⇩✓ □b∈B → Q b)) □
   (□b∈(B - S) → (□a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (□x∈(A ∩ B ∩ S) → (P x ⟦S⟧⇩✓ Q x))›
  by (subst Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_bis
      [of ‹A - S› S ‹A ∩ S› ‹B - S› ‹B ∩ S›, simplified Un_Diff_Int])
    (simp_all add: Int_commute inf_left_commute)


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_for_procomata:
  ― ‹Specialized version for Proc-Omata.›
  ‹□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b =
   (□a∈(A - S - B) → (P a ⟦S⟧⇩✓ □b∈B → Q b))                          □
   (□b∈(B - S - A) → (□a∈A → P a ⟦S⟧⇩✓ Q b))                          □
   (□x∈(A ∩ B - S) → (P x ⟦S⟧⇩✓ □b∈B → Q b) ⊓ (□a∈A → P a ⟦S⟧⇩✓ Q x)) □
   (□x∈(A ∩ B ∩ S) → (P x ⟦S⟧⇩✓ Q x))›
proof -
  have  * : ‹□a∈(A - S) → (P a ⟦S⟧⇩✓ □b∈B → Q b) =
            (□a∈(A - S - B) → (P a ⟦S⟧⇩✓ □b∈B → Q b)) □
            (□a∈(A ∩ B - S) → (P a ⟦S⟧⇩✓ □b∈B → Q b))›
    by (metis Diff_Int2 Diff_Int_distrib2 Mprefix_Un_distrib Un_Diff_Int)
  have ** : ‹□b∈(B - S) → (□a∈A → P a ⟦S⟧⇩✓ Q b) =
            (□b∈(B - S - A) → (□a∈A → P a ⟦S⟧⇩✓ Q b)) □
            (□b∈(A ∩ B - S) → (□a∈A → P a ⟦S⟧⇩✓ Q b))›
    by (metis (no_types) Int_Diff Int_commute Mprefix_Un_distrib Un_Diff_Int)
  have ‹□a∈A → P a ⟦S⟧⇩✓ □b∈B → Q b =
        (□a∈(A - S - B) → (P a ⟦S⟧⇩✓ □b∈B → Q b))    □
        (□b∈(B - S - A) → (□a∈A → P a ⟦S⟧⇩✓ Q b))    □
        ((□a∈(A ∩ B - S) → (P a ⟦S⟧⇩✓ □b∈B → Q b))   □
         (□b∈(A ∩ B - S) → (□a∈A → P a ⟦S⟧⇩✓ Q b)))  □
        (□x∈(A ∩ B ∩ S) → (P x ⟦S⟧⇩✓ Q x))›
    unfolding Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix
    by (auto simp add: "**" Det_assoc intro!: arg_cong[where f = ‹λP. P □ _›])
      (subst (3) Det_commute, subst Det_assoc,
        auto simp add: "*" Det_commute intro: arg_cong[where f = ‹λP. P □ _›])
  also have ‹(□a∈(A ∩ B - S) → (P a ⟦S⟧⇩✓ □b∈B → Q b)) □
             (□b∈(A ∩ B - S) → (□a∈A → P a ⟦S⟧⇩✓ Q b)) =
             □x∈(A ∩ B - S) → ((P x ⟦S⟧⇩✓ □b∈B → Q b)) ⊓ (□a∈A → P a ⟦S⟧⇩✓ Q x)›
    by (simp add: Mprefix_Det_Mprefix, rule mono_Mprefix_eq, simp)
  finally show ?thesis .
qed


(*<*)
end
  (*>*)