Theory Synchronization_Product_Generalized_Non_Destructive

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


(*<*)
theory Synchronization_Product_Generalized_Non_Destructive
  imports "HOL-CSP_RS" CSP_PTick_Monotonicities Events_Ticks_CSP_PTick_Laws 
begin
  (*>*)


section ‹Synchronization Product›

subsection ‹Refinement›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD_div_oneside :
  assumes ‹tF u› ‹ftF v› ‹t_P ∈ 𝒟 (P ↓ n)› ‹t_Q ∈ 𝒯 (Q ↓ n)›
    ‹u setinterleaves⇩✓⇘tick_join⇙ ((t_P, t_Q), 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⇩p⇩t⇩i⇩c⇩k)
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 setinterleaves⇩p⇩t⇩i⇩c⇩k_le_prefixR[OF assms(5) this]
  obtain t_P' t_P'' u' u''
    where ** : ‹u = u' @ u''› ‹t_P = t_P' @ t_P''›
      ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), 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⇩p⇩t⇩i⇩c⇩k) (metis D_T is_processT3_TR_append)
  moreover have ‹length t_Q' ≤ length u'›
    using "**"(3) setinterleaves⇩p⇩t⇩i⇩c⇩k_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 setinterleaves⇩p⇩t⇩i⇩c⇩k_le_prefixL[OF assms(5) this]
  obtain t_Q' t_Q'' u' u''
    where ** : ‹u = u' @ u''› ‹t_Q = t_Q' @ t_Q''›
      ‹u' setinterleaves⇩✓⇘tick_join⇙ ((t_P', t_Q'), 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⇩p⇩t⇩i⇩c⇩k) (metis is_processT3_TR_append)
  moreover have ‹length t_P' ≤ length u'›
    using "**"(3) setinterleaves⇩p⇩t⇩i⇩c⇩k_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 setinterleaves⇩p⇩t⇩i⇩c⇩k_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⇩✓⇘tick_join⇙ ((t_P', t_Q'''), 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⇩p⇩t⇩i⇩c⇩k)
    moreover have ‹n ≤ length u'›
      using "$"(3) "$$"(3) setinterleaves⇩p⇩t⇩i⇩c⇩k_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⇩✓⇘tick_join⇙ ((t_P''', t_Q'), 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⇩p⇩t⇩i⇩c⇩k)
    moreover have ‹n ≤ length u'›
      using "$"(8) "$$"(3) setinterleaves⇩p⇩t⇩i⇩c⇩k_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



lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_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⇩p⇩t⇩i⇩c⇩k, safe)
      (solves ‹simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD_div_oneside›,
        metis Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD_div_oneside
        Sync⇩p⇩t⇩i⇩c⇩k_sym setinterleaves⇩p⇩t⇩i⇩c⇩k_sym)
  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⇩p⇩t⇩i⇩c⇩k 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 (in Sync⇩p⇩t⇩i⇩c⇩k_locale) strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k :
  ‹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⇩p⇩t⇩i⇩c⇩k_FD)
next
  have div : ‹t ∈ 𝒟 (P ⟦A⟧⇩✓ Q) ⟹ t ∈ 𝒟 ?rhs› for t
    by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k 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⇩✓⇘tick_join⇙ ((t_P, t_Q), A)›
      unfolding Sync⇩p⇩t⇩i⇩c⇩k_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⇩✓⇘tick_join⇙ ((t_P, t_Q), 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)› by (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
        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 setinterleaves⇩p⇩t⇩i⇩c⇩k_subsetL[OF ‹tF u› _ setinter]
          setinterleaves⇩p⇩t⇩i⇩c⇩k_subsetR[OF ‹tF u› _ setinter]
        have ‹u = map ev (map of_ev t_P) ∨ u = map ev (map of_ev t_Q)› by blast
        with ‹length u = n› have ‹length t_P = n ∨ length t_Q = n› by auto
        moreover from ‹tF u› tickFree_setinterleaves⇩p⇩t⇩i⇩c⇩k_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 (auto simp add: D_Sync⇩p⇩t⇩i⇩c⇩k)
      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⇩✓⇘tick_join⇙ ((t_P, t_Q), A)›
          ‹X ⊆ super_ref_Sync⇩p⇩t⇩i⇩c⇩k tick_join X_P A X_Q›
        unfolding Sync⇩p⇩t⇩i⇩c⇩k_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⇩p⇩t⇩i⇩c⇩k 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⇩p⇩t⇩i⇩c⇩k_FD :
  ‹❙⟦A❙⟧⇩✓ l ∈@ L. P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧⇩✓ l ∈@ L. (P l ↓ n)›
proof (induct L rule: induct_list012)
  show ‹❙⟦A❙⟧⇩✓ l ∈@ []. P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧⇩✓ l ∈@ []. (P l ↓ n)› by simp
next
  show ‹❙⟦A❙⟧⇩✓ l ∈@ [l1]. P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧⇩✓ l ∈@ [l1]. (P l ↓ n)› for l1
    by (simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Renaming)
next
  fix l1 l2 L
  assume hyp : ‹❙⟦A❙⟧⇩✓ l ∈@ (l2 # L). P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧⇩✓ l ∈@ (l2 # L). (P l ↓ n)›
  show ‹❙⟦A❙⟧⇩✓ l ∈@ (l1 # l2 # L). P l ↓ n ⊑⇩F⇩D ❙⟦A❙⟧⇩✓ l ∈@ (l1 # l2 # L). (P l ↓ n)›
    by simp
      (fact trans_FD[OF Sync⇩R⇩l⇩i⇩s⇩t.restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD
          Sync⇩R⇩l⇩i⇩s⇩t.mono_Sync⇩p⇩t⇩i⇩c⇩k_FD[OF idem_FD hyp]])
qed

text (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ‹
The generalization of the lemma
@{thm strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k[no_vars]}
is not straightforward. We can already observe with only three processes that
one can not expect the first synchronization to have its strict alphabets
contained in the synchronization set. Therefore, we have to assume the
condition on at least \<^term>‹length L - 1› processes.›

corollary strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_MultiSync⇩p⇩t⇩i⇩c⇩k :
  ‹❙⟦A❙⟧⇩✓ l ∈@ L. P l ↓ n = (if n = 0 then ⊥ else ❙⟦A❙⟧⇩✓ l ∈@ L. (P l ↓ n))›
  ―‹‹if n = 0 then ⊥ else _› is necessary because we can have \<^term>‹L = []›.›
  if ‹⋀l. l ∈ set (tl L) ⟹ ❙α(P l) ⊆ A›
proof (split if_split, intro conjI impI)
  show ‹n = 0 ⟹ ❙⟦A❙⟧⇩✓ l ∈@ L. P l ↓ n = ⊥› by simp
next
  from that show ‹❙⟦A❙⟧⇩✓ l ∈@ L. P l ↓ n = ❙⟦A❙⟧⇩✓ l ∈@ L. (P l ↓ n)› if ‹n ≠ 0›
  proof (induct L rule: induct_list012)
    case 1 show ?case by (simp add: ‹n ≠ 0›)
  next
    case (2 l1) show ?case by (simp add: restriction_process⇩p⇩t⇩i⇩c⇩k_Renaming)
  next
    case (3 l1 l2 L)
    from "3.prems" have * : ‹❙α(MultiSync⇩p⇩t⇩i⇩c⇩k A (l2 # L) P) ⊆ A›
      by (intro subset_trans[OF strict_events_of_MultiSync⇩p⇩t⇩i⇩c⇩k_subset]) auto
    have ‹❙⟦A❙⟧⇩✓ l ∈@ (l1 # l2 # L). P l ↓ n =
          P l1 ⟦A⟧⇩✓⇩R⇩l⇩i⇩s⇩t ❙⟦A❙⟧⇩✓ l ∈@ (l2 # L). P l ↓ n› by simp
    also have ‹… = (P l1 ↓ n) ⟦A⟧⇩✓⇩R⇩l⇩i⇩s⇩t (❙⟦A❙⟧⇩✓ l ∈@ (l2 # L). P l ↓ n)›
      by (simp add: Sync⇩R⇩l⇩i⇩s⇩t.strict_events_of_subset_restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k "*")
    also have ‹… = (P l1 ↓ n) ⟦A⟧⇩✓⇩R⇩l⇩i⇩s⇩t ❙⟦A❙⟧⇩✓ l ∈@ (l2 # L). (P l ↓ n)›
      using "3.hyps"(2) "3.prems" by auto
    also have ‹… = ❙⟦A❙⟧⇩✓ l ∈@ (l1 # l2 # L). (P l ↓ n)› by simp
    finally show ?case .
  qed
qed


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

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



subsection ‹Non Destructiveness›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Sync⇩p⇩t⇩i⇩c⇩k_non_destructive :
  ‹non_destructive (λ(P, Q). P ⟦A⟧⇩✓ Q)›
proof (rule order_non_destructiveI, clarify)
  fix P P' :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› and Q Q' :: ‹('a, 's) 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 ‹t ∈ 𝒟 (P' ⟦A⟧⇩✓ Q') ⟹ t ∈ 𝒟 (P ⟦A⟧⇩✓ Q ↓ n)› for t
      by (metis (no_types, lifting) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n› in_mono le_ref1 mono_Sync⇩p⇩t⇩i⇩c⇩k_FD
          restriction_process⇩p⇩t⇩i⇩c⇩k_FD_self restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD)
  next
    show ‹(t, X) ∈ ℱ (P' ⟦A⟧⇩✓ Q') ⟹ (t, X) ∈ ℱ (P ⟦A⟧⇩✓ Q ↓ n)› for t X
      by (metis (no_types, lifting) ‹P ↓ n = P' ↓ n› ‹Q ↓ n = Q' ↓ n› le_ref2 mono_Sync⇩p⇩t⇩i⇩c⇩k_FD
                restriction_process⇩p⇩t⇩i⇩c⇩k_FD_self restriction_process⇩p⇩t⇩i⇩c⇩k_Sync⇩p⇩t⇩i⇩c⇩k_FD subsetD)
  qed
qed



subsection ‹Setup›

lemma (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Sync⇩p⇩t⇩i⇩c⇩k_restriction_shift_process⇩p⇩t⇩i⇩c⇩k
  [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset, simp] :
  ‹non_destructive f ⟹ non_destructive g ⟹ non_destructive (λx. f x ⟦S⟧⇩✓ g x)›
  ‹constructive f ⟹ constructive g ⟹ constructive (λx. f x ⟦S⟧⇩✓ g x)›
  by (fact non_destructive_comp_non_destructive
      [OF Sync⇩p⇩t⇩i⇩c⇩k_non_destructive non_destructive_prod_codomain, simplified])
    (fact non_destructive_comp_constructive
      [OF Sync⇩p⇩t⇩i⇩c⇩k_non_destructive constructive_prod_codomain, simplified])


lemma MultiSync⇩p⇩t⇩i⇩c⇩k_restriction_shift_process⇩p⇩t⇩i⇩c⇩k
  [restriction_shift_process⇩p⇩t⇩i⇩c⇩k_simpset, simp] :
  ‹(⋀l. l ∈ set L ⟹ non_destructive (f l)) ⟹ non_destructive (λx. ❙⟦S❙⟧⇩✓ l ∈@ L. f l x)›
  ‹(⋀l. l ∈ set L ⟹ constructive (f l)) ⟹ constructive (λx. ❙⟦S❙⟧⇩✓ l ∈@ L. f l x)›
  by (induct L rule: induct_list012; simp)+


corollary MultiSync⇩p⇩t⇩i⇩c⇩k_non_destructive : ‹non_destructive (λP. ❙⟦S❙⟧⇩✓ l ∈@ L. P l)›
  by (rule MultiSync⇩p⇩t⇩i⇩c⇩k_restriction_shift_process⇩p⇩t⇩i⇩c⇩k(1)[of L ‹λm x. x m›]) simp




(*<*)
end
  (*>*)