Theory Synchronization_Product_Non_Destructive

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
           CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, 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 ‹Non Destructiveness of Synchronization Product›

(*<*)
theory Synchronization_Product_Non_Destructive
  imports Process_Restriction_Space "HOL-CSPM.CSPM"
begin
  (*>*)

subsection ‹Preliminaries›

lemma D_Sync_optimized :
  ‹𝒟 (P ⟦A⟧ Q) =
   {v @ w |t u v w. tF v ∧ ftF w ∧
                    v setinterleaves ((t, u), range tick ∪ ev ` A) ∧
                    (t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P)}›
  (is ‹_ = ?rhs›)
proof (intro subset_antisym subsetI)
  show ‹d ∈ ?rhs ⟹ d ∈ 𝒟 (P ⟦A⟧ Q)› for d
    by (auto simp add: D_Sync)
next
  fix d assume ‹d ∈ 𝒟 (P ⟦A⟧ Q)›
  then obtain t u v w
    where * : ‹d = v @ w› ‹ftF w› ‹tF v ∨ w = []›
      ‹v setinterleaves ((t, u), range tick ∪ ev ` A)›
      ‹t ∈ 𝒟 P ∧ u ∈ 𝒯 Q ∨ t ∈ 𝒟 Q ∧ u ∈ 𝒯 P›
    unfolding D_Sync by blast
  show ‹d ∈ ?rhs›
  proof (cases ‹tF v›)
    from "*" show ‹tF v ⟹ d ∈ ?rhs› by blast
  next
    assume ‹¬ tF v›
    with "*"(1, 3) have ‹w = []› ‹d = v› by simp_all
    from D_imp_front_tickFree ‹d = v› ‹d ∈ 𝒟 (P ⟦A⟧ Q)›
    have ‹ftF v› by blast
    with ‹¬ tF v› obtain r v' where ‹v = v' @ [✓(r)]›
      by (meson nonTickFree_n_frontTickFree)
    with "*"(4) obtain t' u'
      where ** : ‹t = t' @ [✓(r)]› ‹u = u' @ [✓(r)]›
        ‹v' setinterleaves ((t', u'), range tick ∪ ev ` A)›
      by (simp add: ‹v = v' @ [✓(r)]›)
        (meson "*"(5) D_imp_front_tickFree SyncWithTick_imp_NTF T_imp_front_tickFree)
    have ‹t' ∈ 𝒟 P ∧ u' ∈ 𝒯 Q ∨ t' ∈ 𝒟 Q ∧ u' ∈ 𝒯 P›
      by (metis "*"(5) "**"(1,2) is_processT3_TR_append is_processT9)
    with "**"(3) ‹d = v› ‹ftF v› ‹v = v' @ [✓(r)]›
      front_tickFree_nonempty_append_imp show ‹d ∈ ?rhs› by blast
  qed
qed

lemma tickFree_interleave_iff :
  ‹t setinterleaves ((u, v), S) ⟹ tF t ⟷ tF u ∧ tF v›
  by (induct ‹(u, S, v)› arbitrary: t u v rule: setinterleaving.induct)
    (auto split: if_split_asm option.split_asm)

lemma interleave_subsetL :
  ‹tF t ⟹ {a. ev a ∈ set u} ⊆ A ⟹
   t setinterleaves ((u, v), range tick ∪ ev ` A) ⟹ t = v›
  for t u v :: ‹('a, 'r) trace⇩p⇩t⇩i⇩c⇩k›
proof (induct ‹(u, range tick ∪ ev ` A :: ('a, 'r) refusal⇩p⇩t⇩i⇩c⇩k, v)›
    arbitrary: t u v rule: setinterleaving.induct)
  case 1 thus ?case by simp
next
  case (2 y v) thus ?case by (auto simp add: image_iff split: if_split_asm)
next
  case (3 x u) thus ?case
    by (simp add: image_iff subset_iff split: if_split_asm)
      (metis (mono_tags, lifting) event⇩p⇩t⇩i⇩c⇩k.exhaust)
next
  case (4 x u y v)
  from "4.prems" show ?case
    apply (simp add: subset_iff split: if_split_asm)
       apply (metis (no_types, lifting) "4.hyps"(1) Un_iff
        mem_Collect_eq subsetI tickFree_Cons_iff)
      apply (metis (no_types, lifting) "4.hyps"(2,4) "4.prems"(2,3) SyncHd_Tl
        SyncSameHdTl list.sel(1) setinterleaving_sym tickFree_Cons_iff)
    by (metis event⇩p⇩t⇩i⇩c⇩k.exhaust imageI rangeI)+
qed

lemma interleave_subsetR :
  ‹tF t ⟹ {a. ev a ∈ set v} ⊆ A ⟹
   t setinterleaves ((u, v), range tick ∪ ev ` A) ⟹ t = u›
  by (simp add: interleave_subsetL setinterleaving_sym)


lemma interleave_imp_lengthLR_le :
  ‹t setinterleaves ((u, v), S) ⟹
   length u ≤ length t ∧ length v ≤ length t›
  by (induct ‹(u, S, v)› arbitrary: t u v rule: setinterleaving.induct;
      simp split: if_split_asm; use nat_le_linear not_less_eq_eq in fastforce)

lemma interleave_le_prefixLR :
  ‹t setinterleaves ((u, v), S) ⟹ u' ≤ u ⟹ v' ≤ v ⟹
   (∃t' ≤ t. ∃v'' ≤ v'. t' setinterleaves ((u', v''), S)) ∨
   (∃t' ≤ t. ∃u'' ≤ u'. t' setinterleaves ((u'', v'), S))›
proof (induct ‹(u, S, v)›
    arbitrary: t u u' v v' rule: setinterleaving.induct)
  case 1
  then show ?case by simp
next
  case (2 y v)
  thus ?case by (simp split: if_split_asm)
      (metis si_empty1 insert_iff nil_le)
next
  case (3 x u)
  thus ?case by (simp split: if_split_asm)
      (metis si_empty1 insert_iff nil_le)
next
  case (4 x u y v)
  show ?case
  proof (cases ‹u' = [] ∨ v' = []›)
    show ‹u' = [] ∨ v' = [] ⟹ ?case› by force
  next
    assume ‹¬ (u' = [] ∨ v' = [])›
    with "4.prems"(2, 3)
    obtain u'' v'' where ‹u' = x # u''› ‹u'' ≤ u› ‹v' = y # v''› ‹v'' ≤ v›
      by (meson Prefix_Order.prefix_Cons)
    with "4.prems"(1) consider (both_in)   t' where ‹x ∈ S› ‹y ∈ S› ‹x = y› ‹t = x # t'›
      ‹t' setinterleaves ((u, v), S)›
    |      (inR_mvL)   t' where ‹x ∉ S› ‹y ∈ S› ‹t = x # t'›
      ‹t' setinterleaves ((u, y # v), S)›
    |      (inL_mvR)   t' where ‹x ∈ S› ‹y ∉ S› ‹t = y # t'›
      ‹t' setinterleaves ((x # u, v), S)›
    |      (notin_mvL) t' where ‹x ∉ S› ‹y ∉ S› ‹t = x # t'›
      ‹t' setinterleaves ((u, y # v), S)›
    |      (notin_mvR) t' where ‹x ∉ S› ‹y ∉ S› ‹t = y # t'›
      ‹t' setinterleaves ((x # u, v), S)›
      by (auto split: if_split_asm)
    thus ?case
    proof cases
      case both_in
      from "4.hyps"(1)[OF both_in(1-3, 5) ‹u'' ≤ u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves ((u'', v'''), S)›
        hence ‹y # t'' ≤ t ∧ y # v''' ≤ v' ∧
              (y # t'') setinterleaves ((u', y # v'''), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› both_in(2-4))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves ((u''', v''), S)›
        hence ‹x # t'' ≤ t ∧ x # u''' ≤ u' ∧
              (x # t'') setinterleaves ((x # u''', v'), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› both_in(2-4))
        thus ?thesis by blast
      qed
    next
      case inR_mvL
      from "4.hyps"(5)[simplified, OF inR_mvL(1, 2 ,4) ‹u'' ≤ u› ‹v' ≤ y # v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v'› ‹t'' setinterleaves ((u'', v'''), S)›
        hence ‹x # t'' ≤ t ∧ v''' ≤ v' ∧
              (x # t'') setinterleaves ((u', v'''), S)›
          by (cases v''') (simp_all add: ‹u' = x # u''› ‹v' = y # v''› inR_mvL(1, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves ((u''', v'), S)›
        hence ‹x # t'' ≤ t ∧ x # u''' ≤ u' ∧
              (x # t'') setinterleaves ((x # u''', v'), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› inR_mvL(1, 3))
        thus ?thesis by blast
      qed
    next
      case inL_mvR
      from "4.hyps"(2)[OF inL_mvR(1, 2, 4) ‹u' ≤ x # u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves ((u', v'''), S)›
        hence ‹y # t'' ≤ t ∧ y # v''' ≤ v' ∧
               (y # t'') setinterleaves ((u', y # v'''), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› inL_mvR(2, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u'› ‹t'' setinterleaves ((u''', v''), S)›
        hence ‹y # t'' ≤ t ∧ u''' ≤ u' ∧
               (y # t'') setinterleaves ((u''', v'), S)›
          by (cases u''') (simp_all add: ‹u' = x # u''› ‹v' = y # v''› inL_mvR(2, 3))
        thus ?thesis by blast
      qed
    next
      case notin_mvL
      from "4.hyps"(3)[OF notin_mvL(1, 2, 4) ‹u'' ≤ u› ‹v' ≤ y # v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v'› ‹t'' setinterleaves ((u'', v'''), S)›
        hence ‹x # t'' ≤ t ∧ v''' ≤ v' ∧
               (x # t'') setinterleaves ((u', v'''), S)›
          by (cases v''') (simp_all add: ‹u' = x # u''› ‹v' = y # v''› notin_mvL(1, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u''› ‹t'' setinterleaves ((u''', v'), S)›
        hence ‹x # t'' ≤ t ∧ x # u''' ≤ u' ∧
               (x # t'') setinterleaves ((x # u''', v'), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› notin_mvL(1, 3))
        thus ?thesis by blast
      qed
    next
      case notin_mvR
      from "4.hyps"(4)[OF notin_mvR(1, 2, 4) ‹u' ≤ x # u› ‹v'' ≤ v›]
      show ?thesis
      proof (elim disjE exE conjE)
        fix t'' v'''
        assume ‹t'' ≤ t'› ‹v''' ≤ v''› ‹t'' setinterleaves ((u', v'''), S)›
        hence ‹y # t'' ≤ t ∧ y # v''' ≤ v' ∧
               (y # t'') setinterleaves ((u', y # v'''), S)›
          by (simp add: ‹u' = x # u''› ‹v' = y # v''› notin_mvR(2, 3))
        thus ?thesis by blast
      next
        fix t'' u'''
        assume ‹t'' ≤ t'› ‹u''' ≤ u'› ‹t'' setinterleaves ((u''', v''), S)›
        hence ‹y # t'' ≤ t ∧ u''' ≤ u' ∧
               (y # t'') setinterleaves ((u''', v'), S)›
          by (cases u''') (simp_all add: ‹u' = x # u''› ‹v' = y # v''› notin_mvR(2, 3))
        thus ?thesis by blast
      qed
    qed
  qed
qed


lemma restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD_div_oneside :
  assumes ‹tF u› ‹ftF v› ‹t_P ∈ 𝒟 (P ↓ n)› ‹t_Q ∈ 𝒯 (Q ↓ n)›
    ‹u setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
  shows ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
proof (insert assms(3, 4), elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE T_restriction_process⇩p⇩t⇩i⇩c⇩kE)
  from assms(1, 2, 5) show ‹t_P ∈ 𝒟 P ⟹ t_Q ∈ 𝒯 Q ⟹ u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
    by (auto simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩k D_Sync)
next
  fix t_Q' t_Q''
  assume * : ‹t_P ∈ 𝒟 P› ‹length t_P ≤ n› ‹t_Q = t_Q' @ t_Q''›
    ‹t_Q' ∈ 𝒯 Q› ‹length t_Q' = n› ‹tF t_Q'› ‹ftF t_Q''›
  from ‹t_Q = t_Q' @ t_Q''› have ‹t_Q' ≤ t_Q› by simp
  from interleave_le_right[OF assms(5) this]
  obtain t_P' t_P'' u' u''
    where ** : ‹u = u' @ u''› ‹t_P = t_P' @ t_P''›
      ‹u' setinterleaves ((t_P', t_Q'), range tick ∪ ev ` A)›
    by (meson Prefix_Order.prefixE)
  from assms(1) ‹u = u' @ u''› have ‹tF u'› by auto
  moreover from "*"(1,4) "**"(2,3) have ‹u' ∈ 𝒯 (P ⟦A⟧ Q)›
    by (simp add: T_Sync) (metis D_T is_processT3_TR_append)
  moreover have ‹length t_Q' ≤ length u'›
    using "**"(3) interleave_imp_lengthLR_le by blast
  ultimately have ‹u' ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
    by (metis "*"(5) D_restriction_process⇩p⇩t⇩i⇩c⇩kI nless_le)
  with "**"(1) assms(1, 2) show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
    by (metis is_processT7 tickFree_append_iff tickFree_imp_front_tickFree)
next
  fix t_P' t_P''
  assume * : ‹t_P = t_P' @ t_P''› ‹t_P' ∈ 𝒯 P› ‹length t_P' = n›
    ‹tF t_P'› ‹ftF t_P''› ‹t_Q ∈ 𝒯 Q› ‹length t_Q ≤ n›
  from ‹t_P = t_P' @ t_P''› have ‹t_P' ≤ t_P› by simp
  from interleave_le_left[OF assms(5) this]
  obtain t_Q' t_Q'' u' u''
    where ** : ‹u = u' @ u''› ‹t_Q = t_Q' @ t_Q''›
      ‹u' setinterleaves ((t_P', t_Q'), range tick ∪ ev ` A)›
    by (meson Prefix_Order.prefixE)
  from assms(1) ‹u = u' @ u''› have ‹tF u'› by auto
  moreover from "*"(2,6) "**"(2,3) have ‹u' ∈ 𝒯 (P ⟦A⟧ Q)›
    by (simp add: T_Sync) (metis is_processT3_TR_append)
  moreover have ‹length t_P' ≤ length u'›
    using "**"(3) interleave_imp_lengthLR_le by blast
  ultimately have ‹u' ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
    by (metis "*"(3) D_restriction_process⇩p⇩t⇩i⇩c⇩kI nless_le)
  with "**"(1) assms(1, 2) show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
    by (metis is_processT7 tickFree_append_iff tickFree_imp_front_tickFree)
next
  fix t_P' t_P'' t_Q' t_Q''
  assume $ : ‹t_P = t_P' @ t_P''› ‹t_P' ∈ 𝒯 P› ‹length t_P' = n›
    ‹tF t_P'› ‹ftF t_P''› ‹t_Q = t_Q' @ t_Q''› ‹t_Q' ∈ 𝒯 Q›
    ‹length t_Q' = n› ‹tF t_Q'› ‹ftF t_Q''›
  from "$"(1, 6) have ‹t_P' ≤ t_P› ‹t_Q' ≤ t_Q› by simp_all
  from interleave_le_prefixLR[OF assms(5) this]
  show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
  proof (elim disjE conjE exE)
    fix u' t_Q''' assume $$ : ‹u' ≤ u› ‹t_Q''' ≤ t_Q'›
      ‹u' setinterleaves ((t_P', t_Q'''), range tick ∪ ev ` A)›
    from "$"(7) "$$"(2) is_processT3_TR have ‹t_Q''' ∈ 𝒯 Q› by blast
    with $$(3) ‹t_P' ∈ 𝒯 P› have ‹u' ∈ 𝒯 (P ⟦A⟧ Q)›
      by (auto simp add: T_Sync)
    moreover have ‹n ≤ length u'›
      using "$"(3) "$$"(3) interleave_imp_lengthLR_le by blast
    ultimately have ‹u' ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      by (metis "$$"(1) D_restriction_process⇩p⇩t⇩i⇩c⇩kI Prefix_Order.prefixE
          assms(1) nless_le tickFree_append_iff)
    thus ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      by (metis "$$"(1) Prefix_Order.prefixE assms(1,2) is_processT7
          tickFree_append_iff tickFree_imp_front_tickFree)
  next
    fix u' t_P''' assume $$ : ‹u' ≤ u› ‹t_P''' ≤ t_P'›
      ‹u' setinterleaves ((t_P''', t_Q'), range tick ∪ ev ` A)›
    from "$"(2) "$$"(2) is_processT3_TR have ‹t_P''' ∈ 𝒯 P› by blast
    with $$(3) ‹t_Q' ∈ 𝒯 Q› have ‹u' ∈ 𝒯 (P ⟦A⟧ Q)›
      by (auto simp add: T_Sync)
    moreover have ‹n ≤ length u'›
      using "$"(8) "$$"(3) interleave_imp_lengthLR_le by blast
    ultimately have ‹u' ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      by (metis "$$"(1) D_restriction_process⇩p⇩t⇩i⇩c⇩kI Prefix_Order.prefixE
          assms(1) nless_le tickFree_append_iff)
    thus ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      by (metis "$$"(1) Prefix_Order.prefixE assms(1,2) is_processT7
          tickFree_append_iff tickFree_imp_front_tickFree)
  qed
qed


subsection ‹Refinement›



lemma restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD :
  ‹P ⟦A⟧ Q ↓ n ⊑⇩F⇩D (P ↓ n) ⟦A⟧ (Q ↓ n)› (is ‹?lhs ⊑⇩F⇩D ?rhs›)
proof (unfold refine_defs, safe)
  show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
    by (unfold D_Sync_optimized, safe)
      (solves ‹simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD_div_oneside›,
        metis Sync_commute restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD_div_oneside)
  thus ‹(t, X) ∈ ℱ ((P ↓ n) ⟦A⟧ (Q ↓ n)) ⟹ (t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)› for t X
    by (meson is_processT8 le_approx2 mono_Sync restriction_process⇩p⇩t⇩i⇩c⇩k_approx_self)
qed

text ‹The equality does not hold in general, but we can establish it
      by adding an assumption over the strict alphabets of the processes.›

lemma strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync :
  ‹P ⟦A⟧ Q ↓ n = (P ↓ n) ⟦A⟧ (Q ↓ n)› (is ‹?lhs = ?rhs›)
  if ‹❙α(P) ⊆ A ∨ ❙α(Q) ⊆ A›
proof (rule FD_antisym)
  show ‹?lhs ⊑⇩F⇩D ?rhs› by (fact restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD)
next
  have div : ‹t ∈ 𝒟 (P ⟦A⟧ Q) ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: D_Sync restriction_process⇩p⇩t⇩i⇩c⇩k_projs)

  { fix t u v assume ‹t = u @ v› ‹u ∈ 𝒯 (P ⟦A⟧ Q)› ‹length u = n› ‹tF u› ‹ftF v›
    from this(2) consider ‹u ∈ 𝒟 (P ⟦A⟧ Q)›
      | t_P t_Q where ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
        ‹u setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
      unfolding Sync_projs by blast
    hence ‹t ∈ 𝒟 ?rhs›
    proof cases
      show ‹u ∈ 𝒟 (P ⟦A⟧ Q) ⟹ t ∈ 𝒟 ?rhs›
        by (simp add: ‹ftF v› ‹t = u @ v› ‹tF u› div is_processT7)
    next
      fix t_P t_Q assume ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
        and setinter : ‹u setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
      consider ‹t_P ∈ 𝒟 P ∨ t_Q ∈ 𝒟 Q› | ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q› by blast
      thus ‹t ∈ 𝒟 ?rhs›
      proof cases
        assume ‹t_P ∈ 𝒟 P ∨ t_Q ∈ 𝒟 Q›
        with ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› setinter ‹ftF v› ‹t = u @ v› ‹tF u›
        have ‹t ∈ 𝒟 (P ⟦A⟧ Q)›
          using setinterleaving_sym by (simp add: D_Sync) blast
        thus ‹t ∈ 𝒟 ?rhs› by (fact div)
      next
        assume ‹t_P ∉ 𝒟 P› ‹t_Q ∉ 𝒟 Q›
        with ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› ‹❙α(P) ⊆ A ∨ ❙α(Q) ⊆ A›
        have ‹{a. ev a ∈ set t_P} ⊆ A ∨ {a. ev a ∈ set t_Q} ⊆ A›
          by (auto dest: subsetD intro: strict_events_of_memI)
        with interleave_subsetL[OF ‹tF u› _ setinter]
          interleave_subsetR[OF ‹tF u› _ setinter]
        have ‹u = t_P ∨ u = t_Q› by blast
        with ‹length u = n› have ‹length t_P = n ∨ length t_Q = n› by auto
        moreover from ‹tF u› tickFree_interleave_iff[OF setinter]
        have ‹tF t_P› ‹tF t_Q› by simp_all
        ultimately have ‹t_P ∈ 𝒟 (P ↓ n) ∨ t_Q ∈ 𝒟 (Q ↓ n)›
          using ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        moreover from ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
        have ‹t_P ∈ 𝒯 (P ↓ n)› ‹t_Q ∈ 𝒯 (Q ↓ n)›
          by (simp_all add: T_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        ultimately show ‹t ∈ 𝒟 ?rhs›
          using ‹ftF v› ‹t = u @ v› ‹tF u› setinter
          by (simp add: D_Sync_optimized)
            (metis setinterleaving_sym)
      qed
    qed
  } note * = this

  show ‹?rhs ⊑⇩F⇩D ?lhs›
  proof (unfold refine_defs, safe)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
    proof (elim D_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      show ‹t ∈ 𝒟 (P ⟦A⟧ Q) ⟹ t ∈ 𝒟 ?rhs› by (fact div)
    next
      show ‹⟦t = u @ v; u ∈ 𝒯 (P ⟦A⟧ Q); length u = n; tF u; ftF v⟧
            ⟹ t ∈ 𝒟 ?rhs› for u v by (fact "*")
    qed
  next
    show ‹(t, X) ∈ ℱ ?lhs ⟹ (t, X) ∈ ℱ ?rhs› for t X
    proof (elim F_restriction_process⇩p⇩t⇩i⇩c⇩kE)
      assume ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)›
      then consider ‹t ∈ 𝒟 (P ⟦A⟧ Q)›
        | (fail) t_P t_Q X_P X_Q where ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          ‹t setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
          ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
        unfolding Sync_projs by blast
      thus ‹(t, X) ∈ ℱ ?rhs›
      proof cases
        from div D_F show ‹t ∈ 𝒟 (P ⟦A⟧ Q) ⟹ (t, X) ∈ ℱ ?rhs› by blast
      next
        case fail
        thus ‹(t, X) ∈ ℱ ?rhs›
          by (auto simp add: F_Sync F_restriction_process⇩p⇩t⇩i⇩c⇩k)
      qed
    next
      show ‹⟦t = u @ v; u ∈ 𝒯 (P ⟦A⟧ Q); length u = n; tF u; ftF v⟧
            ⟹ (t, X) ∈ ℱ ?rhs› for u v by (simp add: "*" is_processT8)
    qed
  qed
qed


corollary restriction_process⇩p⇩t⇩i⇩c⇩k_MultiSync_FD :
  ‹❙⟦A❙⟧ m ∈# M. P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧ m ∈# M. (P l ↓ n)›
proof (induct M rule: induct_subset_mset_empty_single)
  case 1 show ?case by simp
next
  case (2 m) show ?case by simp
next
  case (3 N m)
  show ?case
    by (simp add: ‹N ≠ {#}›)
      (fact trans_FD[OF restriction_process⇩p⇩t⇩i⇩c⇩k_Sync_FD mono_Sync_FD[OF idem_FD "3.hyps"(4)]])
qed



text ‹In the following corollary, we could be more precise by having
      the condition on at least \<^term>‹size M - 1› processes.›

corollary strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_MultiSync :
  ‹❙⟦A❙⟧ m ∈# M. P m ↓ n = (if n = 0 then ⊥ else ❙⟦A❙⟧ m ∈# M. (P m ↓ n))›
  ―‹‹if n = 0 then ⊥ else _› is necessary because we can have \<^term>‹M = {#}›.›
  if ‹⋀m. m ∈# M ⟹ ❙α(P m) ⊆ A›
proof (split if_split, intro conjI impI)
  show ‹n = 0 ⟹ ❙⟦A❙⟧ m ∈# M. P m ↓ n = ⊥› by simp
next
  show ‹❙⟦A❙⟧ m ∈# M. P m ↓ n = ❙⟦A❙⟧ m ∈# M. (P m ↓ n)› if ‹n ≠ 0›
  proof (induct M rule: induct_subset_mset_empty_single)
    case 1 from ‹n ≠ 0› show ?case by simp
  next
    case (2 m) show ?case by simp
  next
    case (3 N m)
    have ‹(❙⟦A❙⟧ n∈#add_mset m N. P n) ↓ n = (P m ⟦A⟧ ❙⟦A❙⟧ n∈#N. P n) ↓ n›
      by (simp add: ‹N ≠ {#}›)
    also have ‹… = (P m ↓ n) ⟦A⟧ (❙⟦A❙⟧ n∈#N. P n ↓ n)›
      by (rule strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync)
        (simp add: "3.hyps"(1) ‹⋀m. m ∈# M ⟹ ❙α(P m) ⊆ A›)
    also have ‹(❙⟦A❙⟧ m∈#N. P m) ↓ n = ❙⟦A❙⟧ m∈#N. (P m ↓ n)› by (fact "3.hyps"(4))
    finally show ?case by (simp add: ‹N ≠ {#}›)
  qed
qed



corollary restriction_process⇩p⇩t⇩i⇩c⇩k_Par :
  ‹P || Q ↓ n = (P ↓ n) || (Q ↓ n)›
  by (simp add: strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync)

corollary restriction_process⇩p⇩t⇩i⇩c⇩k_MultiPar :
  ‹❙|❙| m ∈# M. P l ↓ n = (if n = 0 then ⊥ else ❙|❙| m ∈# M. (P l ↓ n))›
  by (simp add: strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_MultiSync)




subsection ‹Non Destructiveness›

lemma Sync_non_destructive :
  ‹non_destructive (λ(P, Q). P ⟦A⟧ Q)›
proof (rule order_non_destructiveI, clarify)
  fix P P' Q Q' :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and n
  assume ‹(P, Q) ↓ n = (P', Q') ↓ n›
  hence ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
    by (simp_all add: restriction_prod_def)
  show ‹P ⟦A⟧ Q ↓ n ⊑⇩F⇩D P' ⟦A⟧ Q' ↓ n›
  proof (rule leFD_restriction_process⇩p⇩t⇩i⇩c⇩kI)
    show div : ‹t ∈ 𝒟 (P' ⟦A⟧ Q') ⟹ t ∈ 𝒟 (P ⟦A⟧ Q ↓ n)› if ‹length t ≤ n› for t
    proof (unfold D_Sync_optimized, safe)
      fix u v t_P t_Q
      assume * : ‹t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
        ‹t_P ∈ 𝒟 P'› ‹t_Q ∈ 𝒯 Q'›
      from "*"(1) ‹length t ≤ n› have ‹length u ≤ n› by simp
      from ‹length u ≤ n› interleave_imp_lengthLR_le[OF "*"(4)]
      have ‹length t_P ≤ n› ‹length t_Q ≤ n› by simp_all
      from ‹t_Q ∈ 𝒯 Q'› ‹length t_Q ≤ n› ‹Q ↓ n = Q' ↓ n› have ‹t_Q ∈ 𝒯 Q›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      proof (cases ‹length u = n›)
        assume ‹length u = n›
        from ‹t_P ∈ 𝒟 P'› ‹length t_P ≤ n› ‹P ↓ n = P' ↓ n› have ‹t_P ∈ 𝒯 P›
          by (simp add: D_T D_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹t_Q ∈ 𝒯 Q› "*"(4) have ‹u ∈ 𝒯 (P ⟦A⟧ Q)›
          unfolding T_Sync by blast
        with ‹length u = n› "*"(2, 3) show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI is_processT7)
      next
        assume ‹length u ≠ n›
        with ‹length u ≤ n› have ‹length u < n› by simp
        with interleave_imp_lengthLR_le[OF "*"(4)]
        have ‹length t_P < n› by simp
        with ‹t_P ∈ 𝒟 P'› ‹P ↓ n = P' ↓ n› have ‹t_P ∈ 𝒟 P›
          by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI
              length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹t_Q ∈ 𝒯 Q› "*"(2-4) have ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q)›
          unfolding D_Sync by blast
        thus ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    next
      fix u v t_P t_Q
      assume * : ‹t = u @ v› ‹tF u› ‹ftF v›
        ‹u setinterleaves ((t_Q, t_P), range tick ∪ ev ` A)›
        ‹t_P ∈ 𝒯 P'› ‹t_Q ∈ 𝒟 Q'›
      from "*"(1) ‹length t ≤ n› have ‹length u ≤ n› by simp
      from ‹length u ≤ n› interleave_imp_lengthLR_le[OF "*"(4)]
      have ‹length t_P ≤ n› ‹length t_Q ≤ n› by simp_all
      from ‹t_P ∈ 𝒯 P'› ‹length t_P ≤ n› ‹P ↓ n = P' ↓ n› have ‹t_P ∈ 𝒯 P›
        by (metis T_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
      show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
      proof (cases ‹length u = n›)
        assume ‹length u = n›
        from ‹t_Q ∈ 𝒟 Q'› ‹length t_Q ≤ n› ‹Q ↓ n = Q' ↓ n› have ‹t_Q ∈ 𝒯 Q›
          by (simp add: D_T D_restriction_process⇩p⇩t⇩i⇩c⇩kI length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹t_P ∈ 𝒯 P› "*"(4) have ‹u ∈ 𝒯 (P ⟦A⟧ Q)›
          unfolding T_Sync using setinterleaving_sym by blast
        with ‹length u = n› "*"(2, 3) show ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI is_processT7)
      next
        assume ‹length u ≠ n›
        with ‹length u ≤ n› have ‹length u < n› by simp
        with interleave_imp_lengthLR_le[OF "*"(4)]
        have ‹length t_Q < n› by simp
        with ‹t_Q ∈ 𝒟 Q'› ‹Q ↓ n = Q' ↓ n› have ‹t_Q ∈ 𝒟 Q›
          by (metis D_restriction_process⇩p⇩t⇩i⇩c⇩kI
              length_less_in_D_restriction_process⇩p⇩t⇩i⇩c⇩k)
        with ‹t_P ∈ 𝒯 P› "*"(2-4) have ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q)›
          unfolding D_Sync by blast
        thus ‹u @ v ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
          by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    qed

    fix t X assume ‹(t, X) ∈ ℱ (P' ⟦A⟧ Q')› ‹length t ≤ n›
    then consider ‹t ∈ 𝒟 (P' ⟦A⟧ Q')›
      | (fail) t_P t_Q X_P X_Q
      where ‹(t_P, X_P) ∈ ℱ P'› ‹(t_Q, X_Q) ∈ ℱ Q'›
        ‹t setinterleaves ((t_P, t_Q), range tick ∪ ev ` A)›
        ‹X = (X_P ∪ X_Q) ∩ (range tick ∪ ev ` A) ∪ X_P ∩ X_Q›
      unfolding Sync_projs by blast
    thus ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)›
    proof cases
      from div ‹length t ≤ n› D_F
      show ‹t ∈ 𝒟 (P' ⟦A⟧ Q') ⟹ (t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)› by blast
    next
      case fail
      show ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)›
      proof (cases ‹length t = n›)
        assume ‹length t = n›
        from ‹length t ≤ n› interleave_imp_lengthLR_le[OF fail(3)]
        have ‹length t_P ≤ n› ‹length t_Q ≤ n› by simp_all
        with fail(1, 2) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
        have ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q›
          by (metis F_T T_restriction_process⇩p⇩t⇩i⇩c⇩kI
              length_le_in_T_restriction_process⇩p⇩t⇩i⇩c⇩k)+
        from F_imp_front_tickFree ‹(t, X) ∈ ℱ (P' ⟦A⟧ Q')›
        have ‹ftF t› by blast
        with fail(3) consider ‹tF t›
          | r s t_P' t_Q' where ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
          by (metis F_imp_front_tickFree SyncWithTick_imp_NTF
              fail(1-2) nonTickFree_n_frontTickFree)
        thus ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)›
        proof cases
          assume ‹tF t›
          from ‹t_P ∈ 𝒯 P› ‹t_Q ∈ 𝒯 Q› fail(3)
          have ‹t ∈ 𝒯 (P ⟦A⟧ Q)› unfolding T_Sync by blast
          hence ‹t ∈ 𝒟 (P ⟦A⟧ Q ↓ n)›
            by (simp add: D_restriction_process⇩p⇩t⇩i⇩c⇩kI ‹length t = n› ‹tF t›)
          thus ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)› by (simp add: is_processT8)
        next
          fix r s t_P' t_Q' assume ‹t_P = t_P' @ [✓(r)]› ‹t_Q = t_Q' @ [✓(s)]›
          have ‹(t_P, X_P) ∈ ℱ P›
            by (metis ‹t_P ∈ 𝒯 P› ‹t_P = t_P' @ [✓(r)]› tick_T_F)
          moreover have ‹(t_Q, X_Q) ∈ ℱ Q›
            by (metis ‹t_Q ∈ 𝒯 Q› ‹t_Q = t_Q' @ [✓(s)]› tick_T_F)
          ultimately have ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)›
            using fail(3, 4) unfolding F_Sync by fast
          thus ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)›
            by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
        qed
      next
        assume ‹length t ≠ n›
        with ‹length t ≤ n› have ‹length t < n› by simp
        with interleave_imp_lengthLR_le[OF fail(3)]
        have ‹length t_P < n› ‹length t_Q < n› by simp_all
        with fail(1, 2) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n›
        have ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
          by (metis F_restriction_process⇩p⇩t⇩i⇩c⇩kI
              length_less_in_F_restriction_process⇩p⇩t⇩i⇩c⇩k)+
        with fail(3, 4) have ‹(t, X) ∈ ℱ (P ⟦A⟧ Q)›
          unfolding F_Sync by fast
        thus ‹(t, X) ∈ ℱ (P ⟦A⟧ Q ↓ n)›
          by (simp add: F_restriction_process⇩p⇩t⇩i⇩c⇩kI)
      qed
    qed
  qed
qed


(*>*)
end
  (*>*)