Theory Read_Write_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
 ***********************************************************************************)


(*<*)
theory Read_Write_CSP_PTick_Laws
  imports Step_CSP_PTick_Laws_Extended
begin
  (*>*)

section ‹Read and Write Laws›

subsection ‹Sequential Composition›

lemma read_Seq⇩p⇩t⇩i⇩c⇩k : ‹c❙?a∈A → P a ❙;⇩✓ Q = c❙?a∈A → (P a ❙;⇩✓ Q)›
  by (simp add: read_def Mprefix_Seq⇩p⇩t⇩i⇩c⇩k comp_def)

lemma write0_Seq⇩p⇩t⇩i⇩c⇩k : ‹a → P ❙;⇩✓ Q = a → (P ❙;⇩✓ Q)›
  by (simp add: write0_def Mprefix_Seq⇩p⇩t⇩i⇩c⇩k)

lemma ndet_write_Seq⇩p⇩t⇩i⇩c⇩k : ‹c❙!❙!a∈A → P a ❙;⇩✓ Q = c❙!❙!a∈A → (P a ❙;⇩✓ Q)›
  by (simp add: ndet_write_is_GlobalNdet_write0 Seq⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right write0_Seq⇩p⇩t⇩i⇩c⇩k)

lemma write_Seq⇩p⇩t⇩i⇩c⇩k : ‹c❙!a → P ❙;⇩✓ Q = c❙!a → (P ❙;⇩✓ Q)›
  by (simp add: write0_Seq⇩p⇩t⇩i⇩c⇩k write_is_write0)



subsection ‹Synchronization Product›

subsubsection ‹General Laws›

context Sync⇩p⇩t⇩i⇩c⇩k_locale begin

paragraph ‹ \<^const>‹read› ›

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read : 
  ― ‹This is the general case.›
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
   (d❙?b∈(B - d -` S) → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (□x∈(c ` A ∩ d ` B ∩ S) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x)))›
  (is ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3›)
  if ‹c ` A ∩ S = {} ∨ c ` A ⊆ S ∨ inj_on c A›
    ‹d ` B ∩ S = {} ∨ d ` B ⊆ S ∨ inj_on d B›
    ― ‹Assumptions may seem strange, but the motivation is that when \<^term>‹A - c -` S ≠ {}›
     (which is equivalent to \<^term>‹¬ c ` A ⊆ S›), we need to ensure that 
     \<^term>‹inv_into (A - c -` S) c› is equal to \<^term>‹inv_into A c›.
     This requires \<^term>‹A - c -` S = A› (which is equivalent to \<^term>‹c ` A ∩ S = {}›)
     or \<^term>‹inj_on c A›. We need obviously a similar assumption for \<^term>‹B›.›
proof -
  have * : ‹⋀e X. e ` (X - e -` S) = e ` X - S› by auto
  have ‹?lhs = (□a∈(c ` A - S) → (P (inv_into A c a) ⟦S⟧⇩✓ (□x∈d ` B → Q (inv_into B d x)))) □
               (□b∈(d ` B - S) → ((□x∈c ` A → P (inv_into A c x)) ⟦S⟧⇩✓ Q (inv_into B d b))) □
               (□x∈(c ` A ∩ d ` B ∩ S) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x)))›
    (is ‹?lhs = ?rhs1' □ ?rhs2' □ ?rhs3›)
    by (simp add: read_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix comp_def)
  also from that(1) have ‹?rhs1' = ?rhs1›
  proof (elim disjE)
    assume ‹c ` A ∩ S = {}›
    hence ‹A - c -` S = A ∧ c ` A - S = c ` A› by fast
    thus ‹?rhs1' = ?rhs1› by (simp add: read_def comp_def)
  next
    assume ‹c ` A ⊆ S›
    hence ‹A - c -` S = {} ∧ c ` A - S = {}› by fast
    show ‹?rhs1' = ?rhs1› by (simp add: ‹?this›)
  next
    assume ‹inj_on c A›
    hence ‹inj_on c (A - c -` S)› by (simp add: inj_on_diff)
    with ‹inj_on c A› show ‹?rhs1' = ?rhs1›
      by (auto simp add: read_def comp_def "*" intro: mono_Mprefix_eq)
  qed
  also from that(2) have ‹?rhs2' = ?rhs2›
  proof (elim disjE)
    assume ‹d ` B ∩ S = {}›
    hence ‹B - d -` S = B ∧ d ` B - S = d ` B› by fast
    thus ‹?rhs2' = ?rhs2› by (simp add: read_def comp_def)
  next
    assume ‹d ` B ⊆ S›
    hence ‹B - d -` S = {} ∧ d ` B - S = {}› by fast
    show ‹?rhs2' = ?rhs2› by (simp add: ‹?this›)
  next
    assume ‹inj_on d B›
    hence ‹inj_on d (B - d -` S)› by (simp add: inj_on_diff)
    with ‹inj_on d B› show ‹?rhs2' = ?rhs2›
      by (auto simp add: read_def comp_def "*" intro: mono_Mprefix_eq)
  qed
  finally show ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3› .
qed


paragraph ‹Enforce read›

― ‹With stronger assumptions, we can fully rewrite the right hand side with \<^const>‹read›.›
― ‹Remember that now, channels \<^term>‹c› and \<^term>‹d› must have the same type.
   This was not the case on the previous lemma.›
lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_left : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
   (d❙?b∈(B - d -` S) → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (c❙?x∈(A ∩ c -` (d ` B ∩ S)) → (P x ⟦S⟧⇩✓ Q x))›
  (is ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3›)
  if ‹c ` A ∩ S = {} ∨ inj_on c A›
    ‹d ` B ∩ S = {} ∨ inj_on d B›
    ‹⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ d b ∈ S ⟹ a = b›
proof -
  let ?rhs3' = ‹(□x∈(c ` A ∩ d ` B ∩ S) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x)))›
  have  * : ‹c ` (A ∩ c -` (d ` B ∩ S)) = c ` A ∩ d ` B ∩ S› by blast
  have ** : ‹c ` (A ∩ c -` d ` B) = c ` A ∩ d ` B› by blast
  from that(1, 2) consider ‹c ` A ∩ S = {} ∨ d ` B ∩ S = {}›
    | ‹inj_on c A› ‹inj_on d B› by blast
  hence ‹?rhs3' = ?rhs3›
  proof cases
    assume ‹c ` A ∩ S = {} ∨ d ` B ∩ S = {}›
    hence ‹c ` A ∩ d ` B ∩ S = {} ∧ A ∩ c -` (d ` B ∩ S) = {}› by blast
    thus ‹?rhs3' = ?rhs3› by simp
  next
    assume ‹inj_on c A› ‹inj_on d B›
    show ‹?rhs3' = ?rhs3›
    proof (unfold read_def "*" comp_def,
        intro mono_Mprefix_eq arg_cong2[where f = ‹λP Q. P ⟦S⟧⇩✓ Q›])
      fix x assume ‹x ∈ c ` A ∩ d ` B ∩ S›
      moreover from ‹inj_on c A› inj_on_Int
      have ‹inj_on c A ∧ inj_on c (A ∩ c -` (d ` B ∩ S))› by blast
      ultimately show ‹P (inv_into A c x) = P (inv_into (A ∩ c -` (d ` B ∩ S)) c x)›
        by (simp add: image_iff, elim conjE bexE, simp)
    next
      fix x assume $ : ‹x ∈ c ` A ∩ d ` B ∩ S›
      then obtain a b where $$ : ‹x = c a› ‹a ∈ A› ‹x = d b› ‹b ∈ B› by blast
      from ‹inj_on c A› inj_on_Int have $$$ : ‹inj_on c (A ∩ c -` (d ` B ∩ S))› by blast
      have ‹inv_into B d x = b› by (simp add: "$$"(3, 4) ‹inj_on d B›)
      also have ‹b = a› by (metis "$" "$$" Int_iff that(3))
      also have ‹a = inv_into (A ∩ c -` (d ` B ∩ S)) c x›
        by (metis "$" "$$"(1, 2) "$$$" "*" Int_lower1
            ‹inj_on c A› inj_on_image_mem_iff inv_into_f_eq)
      finally have ‹inv_into B d x = inv_into (A ∩ c -` (d ` B ∩ S)) c x› .
      thus ‹Q (inv_into B d x) = Q (inv_into (A ∩ c -` (d ` B ∩ S)) c x)› by simp
    qed
  qed
  moreover have ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3'›
    using that(1, 2) by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read) auto
  ultimately show ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3› by argo
qed


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_right:
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
   (d❙?b∈(B - d -` S) → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (d❙?x∈(B ∩ d -` (c ` A ∩ S)) → (P x ⟦S⟧⇩✓ Q x))›
  (is ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3›)
  if ‹c ` A ∩ S = {} ∨ inj_on c A›
    ‹d ` B ∩ S = {} ∨ inj_on d B›
    ‹⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ d b ∈ S ⟹ a = b›
  unfolding Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym
  by (subst Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_left[OF that(2, 1)], metis that(3))
    (auto simp add: Det_commute intro: arg_cong2[where f = ‹(□)›])



paragraph ‹Special Cases›

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   □x∈(c ` A ∩ d ` B) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x))›
  if ‹c ` A ⊆ S› ‹d ` B ⊆ S›
proof -
  from that have * : ‹A - c -` S = {}› ‹B - d -` S = {}› by auto
  from that(1) have ** : ‹c ` A ∩ d ` B ∩ S = c ` A ∩ d ` B› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read)
      (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_forced_read_left : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = c❙?x∈(A ∩ c -` d ` B) → (P x ⟦S⟧⇩✓ Q x)›
  if ‹c ` A ⊆ S› ‹d ` B ⊆ S› ‹inj_on c A› ‹inj_on d B›
    ‹⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ d b ∈ S ⟹ a = b›
proof -
  from that have * : ‹A - c -` S = {}› ‹B - d -` S = {}› by auto
  from that(1) have ** : ‹A ∩ (c -` d ` B ∩ c -` S) = A ∩ c -` d ` B› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_left)
      (use that(3, 4, 5) in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_forced_read_right : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?x∈(B ∩ d -` c ` A) → (P x ⟦S⟧⇩✓ Q x)›
  if ‹c ` A ⊆ S› ‹d ` B ⊆ S› ‹inj_on c A› ‹inj_on d B›
    ‹⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ d b ∈ S ⟹ a = b›
proof -
  from that have * : ‹B - d -` S = {}› ‹A - c -` S = {}› by auto
  from that(1) have ** : ‹B ∩ (d -` c ` A ∩ d -` S) = B ∩ d -` c ` A› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_right)
      (use that(3, 4, 5) in ‹simp_all add: "*" "**"›)
qed


lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_indep : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (c❙?a∈A → (P a ⟦S⟧⇩✓ (d❙?b∈B → Q b))) □ (d❙?b∈B → ((c❙?a∈A → P a) ⟦S⟧⇩✓ Q b))›
  if ‹c ` A ∩ S = {}› ‹d ` B ∩ S = {}›
proof -
  from that have * : ‹A - c -` S = A› ‹B - d -` S = B› by auto
  from that(1) have ** : ‹c ` A ∩ d ` B ∩ S = {}› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read) (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_left : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = c❙?a∈A → (P a ⟦S⟧⇩✓ (d❙?b∈B → Q b))›
  if ‹c ` A ∩ S = {}› ‹d ` B ⊆ S›
proof -
  from that(1) have * : ‹A - c -` S = A› ‹c ` A ∩ d ` B ∩ S = {}› by auto
  from that(2) have ** : ‹B - d -` S = {}› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read)
      (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_right :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈B → ((c❙?a∈A → P a) ⟦S⟧⇩✓ Q b)›
  if ‹c ` A ⊆ S› ‹d ` B ∩ S = {}›
proof -
  from that(2) have * : ‹B - d -` S = B› ‹c ` A ∩ d ` B ∩ S = {}› by auto
  from that(1) have ** : ‹A - c -` S = {}› by blast
  show ?thesis by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read)
      (use that in ‹simp_all add: "*" "**"›)
qed


corollary read_Par⇩p⇩t⇩i⇩c⇩k_read :
  ‹c❙?a∈A → P a ||⇩✓ d❙?b∈B → Q b =
   □x∈(c ` A ∩ d ` B) → (P (inv_into A c x) ||⇩✓ Q (inv_into B d x))›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset)

corollary read_Par⇩p⇩t⇩i⇩c⇩k_read_forced_read_left :
  ‹⟦inj_on c A; inj_on d B; ⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ a = b⟧ ⟹
   c❙?a∈A → P a ||⇩✓ d❙?b∈B → Q b = c❙?x∈(A ∩ c -` d ` B) → (P x ||⇩✓ Q x)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_left) simp_all

corollary read_Par⇩p⇩t⇩i⇩c⇩k_read_forced_read_right :
  ‹⟦inj_on c A; inj_on d B; ⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ a = b⟧ ⟹
   c❙?a∈A → P a ||⇩✓ d❙?b∈B → Q b = d❙?x∈(B ∩ d -` c ` A) → (P x ||⇩✓ Q x)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_right) simp_all


corollary read_Inter⇩p⇩t⇩i⇩c⇩k_read :
  ‹⟦inj_on c A; inj_on d B; ⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = d b ⟹ a = b⟧ ⟹
   c❙?a∈A → P a |||⇩✓ d❙?b∈B → Q b =
   (c❙?a∈A → (P a |||⇩✓ d❙?b∈B → Q b)) □ (d❙?b∈B → (c❙?a∈A → P a |||⇩✓ Q b))›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_read)



paragraph ‹Same channel›

text ‹Some results can be rewritten when we have the same channel.›


lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_same_chan : 
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ c❙?b∈B → Q b =
   (c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ c❙?b∈B → Q b)) □
   (c❙?b∈(B - c -` S) → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (c❙?x∈(A ∩ B ∩ c -` S) → (P x ⟦S⟧⇩✓ Q x))›
  (is ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3›)
  if ‹c ` A ∩ S = {} ∨ inj_on c A› ‹c ` B ∩ S = {} ∨ inj_on c B›
    ‹⋀a b. a ∈ A ⟹ b ∈ B ⟹ c a = c b ⟹ c b ∈ S ⟹ a = b›
proof -
  ― ‹Actually, the third assumption is equivalent to the following
     (we of course do not use that(3) in the proof of equivalence).›
  from that(1, 2)
  have ‹inj_on c ((A ∪ B) ∩ c -` S) ⟷
        (∀a b. a ∈ A ⟶ b ∈ B ⟶ c a = c b ⟶ c b ∈ S ⟶ a = b)›
    by (elim disjE, simp_all add: inj_on_def)
      ((auto)[3], metis Int_iff Un_iff vimageE vimageI)

  from that(3) have * : ‹A ∩ (c -` c ` B ∩ c -` S) = A ∩ B ∩ c -` S› by auto blast
  show ?thesis by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_left that "*")
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_same_chan_weaker :
  ― ‹Easier with a stronger assumption.›
  ‹inj_on c (A ∪ B) ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ c❙?b∈B → Q b =
   (c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ c❙?b∈B → Q b)) □
   (c❙?b∈(B - c -` S) → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)) □
   (c❙?x∈(A ∩ B ∩ c -` S) → (P x ⟦S⟧⇩✓ Q x))›
  by (rule read_Sync⇩p⇩t⇩i⇩c⇩k_read_forced_read_same_chan)
    (simp_all add: inj_on_Un, metis Un_iff inj_onD inj_on_Un)


lemma read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_forced_read_same_chan :
  ― ‹In the subset case, the assumption \<^term>‹inj_on c (A ∪ B)› is equivalent.
      The result is not weaker anymore.›
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ c❙?b∈B → Q b = c❙?x∈(A ∩ B) → (P x ⟦S⟧⇩✓ Q x)›
  if ‹c ` A ⊆ S› ‹c ` B ⊆ S› ‹inj_on c (A ∪ B)›
proof -
  from that(3) have ‹A ∩ c -` c ` B = A ∩ B› by (auto simp add: inj_on_def)
  with that(3) show ?thesis
    by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_forced_read_left)
      (simp_all add: that(1, 2) inj_on_Un, meson Un_iff inj_on_contraD that(3))
qed



paragraph ‹\<^const>‹read› and \<^const>‹ndet_write›.›

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (  if A = {} then STOP ⟦S⟧⇩✓ d❙?b∈B → Q b
    else ⊓a∈c ` A. (if a ∈ S then STOP else a → (P (inv_into A c a) ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
                   (□b∈(d ` B - S) → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d b))) □
                   (if a ∈ d ` B ∩ S then a → (P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d a)) else STOP))›
  by (auto simp add: ndet_write_def read_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then c❙?a∈A → P a ⟦S⟧⇩✓ STOP
    else ⊓b∈d ` B. (if b ∈ S then STOP else b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q (inv_into B d b))) □
                   (□a∈(c ` A - S) → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
                   (if b ∈ c ` A ∩ S then b → (P (inv_into A c b) ⟦S⟧⇩✓ Q (inv_into B d b)) else STOP))›
  by (auto simp add: ndet_write_def read_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset :
  ‹c ` A ⊆ S ⟹ d ` B ⊆ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (  if c ` A ⊆ d ` B then ⊓a∈c ` A → (P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d a))
    else (⊓a∈(c ` A ∩ d ` B) → (P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d a))) ⊓ STOP)›
  by (simp add: read_def ndet_write_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_subset)

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset :
  ‹c ` A ⊆ S ⟹ d ` B ⊆ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if d ` B ⊆ c ` A then ⊓b∈d ` B → (P (inv_into A c b) ⟦S⟧⇩✓ Q (inv_into B d b))
    else (⊓b∈(c ` A ∩ d ` B) → (P (inv_into A c b) ⟦S⟧⇩✓ Q (inv_into B d b))) ⊓ STOP)›
  by (simp add: read_def ndet_write_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_subset)


― ‹If we have the same injective channel, it's better.›
lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan:
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ c❙?b∈B → Q b =
   (if A ⊆ B then c❙!❙!a∈A → (P a ⟦S⟧⇩✓ Q a) else (c❙!❙!a∈(A ∩ B) → (P a ⟦S⟧⇩✓ Q a)) ⊓ STOP)›
  if ‹c ` A ⊆ S› ‹c ` B ⊆ S› ‹inj_on c (A ∪ B)›
proof -
  from ‹inj_on c (A ∪ B)› have  * : ‹c ` A ⊆ c ` B ⟷ A ⊆ B›
    by (auto simp add: inj_on_eq_iff)
  from ‹inj_on c (A ∪ B)› have ** : ‹c ` A ∩ c ` B = c ` (A ∩ B)›
    by (auto simp add: inj_on_Un)
  from ‹inj_on c (A ∪ B)› show ?thesis
    by (unfold ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset[OF ‹c ` A ⊆ S› ‹c ` B ⊆ S›] "*" "**")
      (auto simp add: ndet_write_def inj_on_Un inj_on_Int
        intro!: mono_Mndetprefix_eq arg_cong2[where f = ‹(⊓)›])
qed

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset_same_chan:
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ c❙!❙!b∈B → Q b =
   (if B ⊆ A then c❙!❙!b∈B → (P b ⟦S⟧⇩✓ Q b) else (c❙!❙!b∈(A ∩ B) → (P b ⟦S⟧⇩✓ Q b)) ⊓ STOP)›
  if ‹c ` A ⊆ S› ‹c ` B ⊆ S› ‹inj_on c (A ∪ B)›
  by (subst (1 2 3) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan
      [OF that(2, 1)] Un_commute Int_commute that(3))


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_indep :
  ‹c ` A ∩ S = {} ⟹ d ` B ∩ S = {} ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (  if A = {} then d❙?b∈B →  (STOP ⟦S⟧⇩✓ Q b)
    else ⊓a∈c ` A. (a → (P (inv_into A c a) ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
                   (d❙?b∈B → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q b)))›
  by (auto simp add: ndet_write_def read_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_indep comp_def
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep :
  ‹c ` A ∩ S = {} ⟹ d ` B ∩ S = {} ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then c❙?a∈A → (P a ⟦S⟧⇩✓ STOP)
    else ⊓b∈d ` B. (b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q (inv_into B d b))) □
                   (c❙?a∈A → (P a ⟦S⟧⇩✓ b → Q (inv_into B d b))))›
  by (auto simp add: ndet_write_def read_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_indep comp_def
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_left :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = c❙!❙!a∈A → (P a ⟦S⟧⇩✓ d❙?b∈B → Q b)›
  (is ‹?lhs = ?rhs›) if ‹c ` A ∩ S = {}› ‹d ` B ⊆ S›
proof -
  from that have ‹?lhs = (if A = {} then STOP ⟦S⟧⇩✓ d❙?b∈B → Q b else ?rhs)›
    by (auto simp add: ndet_write_def read_def
        Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_left comp_def
        intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])
  also have ‹… = ?rhs›
    by (simp add: read_def ndet_write_def Mprefix_is_STOP_iff
        STOP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix that(2))
  finally show ‹?lhs = ?rhs› .
qed

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = c❙?a∈A → (P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b)›
  (is ‹?lhs = ?rhs›) if ‹c ` A ∩ S = {}› ‹d ` B ⊆ S›
proof -
  from that have ‹?lhs = (if B = {} then (c❙?a∈A → P a) ⟦S⟧⇩✓ STOP else ?rhs)›
    by (auto simp add: ndet_write_def read_def
        Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_left comp_def
        intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])
  also have ‹… = ?rhs›
    by (simp add: read_def comp_def)
      (use Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix_left that(1) in force)
  finally show ‹?lhs = ?rhs› .
qed


corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_right :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈B → (c❙!❙!a∈A → P a ⟦S⟧⇩✓ Q b)›
  if ‹c ` A ⊆ S› ‹d ` B ∩ S = {}›
  by (subst (1 2) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left[OF that(2, 1)])

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = d❙!❙!b∈B → (c❙?a∈A → P a ⟦S⟧⇩✓ Q b)›
  if ‹c ` A ⊆ S› ‹d ` B ∩ S = {}›
  by (subst (1 2) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_left[OF that(2, 1)])



paragraph ‹\<^const>‹read› and \<^const>‹write›.›

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read :
  ‹c❙!a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
   (□b∈(d ` B - S) → (c❙!a → P ⟦S⟧⇩✓ Q (inv_into B d b))) □
   (if c a ∈ d ` B ∩ S then c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a))) else STOP)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read[where A = ‹{a}›, simplified])
    (simp add: write_is_write0 image_iff)

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ d❙!b → Q =
   (if d b ∈ S then STOP else d❙!b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)) □
   (□a∈(c ` A - S) → (P (inv_into A c a) ⟦S⟧⇩✓ d❙!b → Q)) □
   (if d b ∈ c ` A ∩ S then d❙!b → (P (inv_into A c (d b)) ⟦S⟧⇩✓ Q) else STOP)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write[where B = ‹{b}›, simplified])
    (simp add: write_is_write0 image_iff)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset :
  ‹c a ∈ S ⟹ d ` B ⊆ S ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (if c a ∈ d ` B then c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a))) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read)
    (metis Det_STOP Det_commute Diff_eq_empty_iff Mprefix_empty)

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write_subset :
  ‹c ` A ⊆ S ⟹ d b ∈ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!b → Q =
   (if d b ∈ c ` A then d❙!b → (P (inv_into A c (d b)) ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write)
    (metis Diff_eq_empty_iff Mprefix_empty STOP_Det)


― ‹If we have the same injective channel, it's better.›
lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan:
  ‹c a ∈ S ⟹ c ` B ⊆ S ⟹ inj_on c (insert a B) ⟹
   c❙!a → P ⟦S⟧⇩✓ c❙?b∈B → Q b = (if a ∈ B then c❙!a → (P ⟦S⟧⇩✓ Q a) else STOP)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan[where A = ‹{a}›, simplified]) simp_all

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write_subset_same_chan:
  ‹c ` A ⊆ S ⟹ c b ∈ S ⟹ inj_on c (insert b A) ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ c❙!b → Q = (if b ∈ A then c❙!b → (P b ⟦S⟧⇩✓ Q) else STOP)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset_same_chan[where B = ‹{b}›, simplified]) simp_all


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read_indep :
  ‹c a ∉ S ⟹ d ` B ∩ S = {} ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (c❙!a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)) □ (d❙?b∈B → (c❙!a → P ⟦S⟧⇩✓ Q b))›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_indep[where A = ‹{a}›, simplified])
    (simp_all add: write_is_write0)

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write_indep :
  ‹c ` A ∩ S = {} ⟹ d b ∉ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!b → Q =
   (d❙!b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)) □ (c❙?a∈A → (P a ⟦S⟧⇩✓ d❙!b → Q))›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep[where B = ‹{b}›, simplified])
    (simp_all add: write_is_write0)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read_left :
  ‹c a ∉ S ⟹ d ` B ⊆ S ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙?b∈B → Q b = c❙!a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_left[where A = ‹{a}›, simplified]) simp_all

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write_left :
  ‹c ` A ∩ S = {} ⟹ d b ∈ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!b → Q = c❙?a∈A → (P a ⟦S⟧⇩✓ d❙!b → Q)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left[where B = ‹{b}›, simplified]) simp_all


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_read_right :
  ‹c a ∈ S ⟹ d ` B ∩ S = {} ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈B → (c❙!a → P ⟦S⟧⇩✓ Q b)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read_right[where A = ‹{a}›, simplified]) simp_all

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write_right :
  ‹c ` A ⊆ S ⟹ d b ∉ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ d❙!b → Q = d❙!b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right[where B = ‹{b}›, simplified]) simp_all



paragraph ‹\<^const>‹ndet_write› and \<^const>‹ndet_write››

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if A = {} then   if d ` B ∩ S = {} then d❙!❙!b∈B → (STOP ⟦S⟧⇩✓ Q b)
                     else (⊓x∈d ` (B - d -` S) → (STOP ⟦S⟧⇩✓ Q (inv_into B d x))) ⊓ STOP
    else   if B = {} then   if c ` A ∩ S = {} then c❙!❙!a∈A → (P a ⟦S⟧⇩✓ STOP)
                          else (⊓x∈c ` (A - c -` S) → (P (inv_into A c x) ⟦S⟧⇩✓ STOP)) ⊓ STOP
         else ⊓b∈d ` B. ⊓a∈c ` A.
              (if a ∈ S then STOP else a → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
              (if b ∈ S then STOP else b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d b))) □
              (if a = b ∧ b ∈ S then b → (P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d b)) else STOP))›
proof -
  have ‹d ` (B - d -` S) = d ` B - S› ‹c ` (A - c -` S) = c ` A - S› by auto
  thus ?thesis
    by (auto simp add: ndet_write_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix comp_def
        intro!: mono_GlobalNdet_eq split: if_split_asm)
qed


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset :
  ‹c ` A ⊆ S ⟹ d ` B ⊆ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if ∃b. c ` A = {b} ∧ d ` B = {b}
    then (THE b. d ` B = {b}) → (P (inv_into A c (THE a. c ` A = {a})) ⟦S⟧⇩✓ Q (inv_into B d (THE b. d ` B = {b})))
    else (⊓x∈(c ` A ∩ d ` B) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x))) ⊓ STOP)›
  by (auto simp add: ndet_write_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_subset)


corollary inj_on_ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if ∃b. c ` A = {b} ∧ d ` B = {b}
    then d (THE b. B = {b}) → (P (THE a. A = {a}) ⟦S⟧⇩✓ Q (THE b. B = {b}))
    else (⊓x∈(c ` A ∩ d ` B) → (P (inv_into A c x) ⟦S⟧⇩✓ Q (inv_into B d x))) ⊓ STOP)›
  if ‹inj_on c A› ‹inj_on d B› ‹c ` A ⊆ S› ‹d ` B ⊆ S›
proof -
  from that(1) have ‹c ` A = {a'} ⟹ ∃!a. A = {a} ∧ a' = c a› for a'
    by (fastforce elim!: inj_img_insertE)
  moreover from that(2) have ‹d ` B = {b'} ⟹ ∃!b. B = {b} ∧ b' = d b› for b'
    by (fastforce elim!: inj_img_insertE)
  ultimately show ?thesis
    by (auto simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset[OF that(3, 4)] inv_into_f_eq
        intro: arg_cong2[where f = ‹(→)›] arg_cong2[where f = ‹λP Q. P ⟦S⟧⇩✓ Q›])
qed


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep :
  ‹c ` A ∩ S = {} ⟹ d ` B ∩ S = {} ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if A = {} then d❙!❙!b∈B → (STOP ⟦S⟧⇩✓ Q b)
    else   if B = {} then c❙!❙!a∈A → (P a ⟦S⟧⇩✓ STOP)
         else ⊓b∈d ` B. ⊓a∈c ` A.
              ((a → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q (inv_into B d b)))) □
              ((b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q (inv_into B d b)))))›
  by (auto simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write disjoint_iff intro!: mono_GlobalNdet_eq)


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left :
  ‹c ` A ∩ S = {} ⟹ d ` B ⊆ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = c❙!❙!a∈A → (P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b)›
  by (simp add: ndet_write_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_left comp_def)


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right :
  ‹c ` A ⊆ S ⟹ d ` B ∩ S = {} ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = d❙!❙!b∈B → (c❙!❙!a∈A → P a ⟦S⟧⇩✓ Q b)›
  by (simp add: ndet_write_def Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_Mndetprefix_right comp_def)



paragraph ‹\<^const>‹ndet_write› and \<^const>‹write››

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹c❙!a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then c❙!a → P ⟦S⟧⇩✓ STOP
    else ⊓b∈d ` B. (if b ∈ S then STOP else b → (c❙!a → P ⟦S⟧⇩✓ Q (inv_into B d b))) □
                   (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
                   (if b = c a ∧ c a ∈ S then c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a))) else STOP))›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write[where A = ‹{a}›, simplified],
      auto simp add: write_def Mprefix_singl split: if_split_asm
      intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›] mono_Mprefix_eq)
    (simp add: insert_Diff_if write0_def)

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!b → Q =
   (  if A = {} then STOP ⟦S⟧⇩✓ d❙!b → Q
    else ⊓a∈c ` A. (if a ∈ S then STOP else a → (P (inv_into A c a) ⟦S⟧⇩✓ d❙!b → Q)) □
                   (if d b ∈ S then STOP else d❙!b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q)) □
                   (if a = d b ∧ d b ∈ S then d❙!b → (P (inv_into A c a) ⟦S⟧⇩✓ Q) else STOP))›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_read[where B = ‹{b}›, simplified],
      auto simp add: write_def Mprefix_singl split: if_split_asm
      intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›] mono_Mprefix_eq)
    (simp add: insert_Diff_if write0_def)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset :
  ‹c❙!a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if c a ∉ d ` B then STOP else if d ` B = {c a} then c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a)))
    else (c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a)))) ⊓ STOP)› if ‹c a ∈ S› ‹d ` B ⊆ S›
proof (subst read_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset[where A = ‹{a}›, simplified])
  from ‹c a ∈ S› show ‹c a ∈ S› .
next
  from ‹d ` B ⊆ S› show ‹d ` B ⊆ S› .
next
  show ‹(  if d ` B ⊆ {c a} then ⊓b∈d ` B → (P ⟦S⟧⇩✓ Q (inv_into B d b))
         else (⊓b∈(c ` {a} ∩ d ` B) → (P ⟦S⟧⇩✓ Q (inv_into B d b))) ⊓ STOP) =
        (  if c a ∉ d ` B then STOP else if d ` B = {c a} then c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a)))
         else (c❙!a → (P ⟦S⟧⇩✓ Q (inv_into B d (c a)))) ⊓ STOP)›
    (is ‹?lhs = (if c a ∉ d ` B then STOP else if d ` B = {c a} then ?rhs else ?rhs ⊓ STOP)›)
  proof (split if_split, intro conjI impI)
    show ‹c a ∉ d ` B ⟹ ?lhs = STOP›
      by (auto simp add: GlobalNdet_is_STOP_iff image_subset_iff image_iff)
  next
    show ‹¬ c a ∉ d ` B ⟹ ?lhs = (if d ` B = {c a} then ?rhs else ?rhs ⊓ STOP)›
      by (auto simp add: image_subset_iff Ndet_is_STOP_iff write_is_write0)
  qed
qed

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_subset :
  ‹(c❙!❙!a∈A → P a) ⟦S⟧⇩✓ (d❙!b → Q) =
   (  if d b ∉ c ` A then STOP else if c ` A = {d b} then d❙!b → (P (inv_into A c (d b)) ⟦S⟧⇩✓ Q)
    else (d❙!b → (P (inv_into A c (d b)) ⟦S⟧⇩✓ Q)) ⊓ STOP)› if ‹c ` A ⊆ S› ‹d b ∈ S›
  by (subst (1 2 3) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset that)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep :
  ‹c a ∉ S ⟹ d ` B ∩ S = {} ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then c❙!a → (P ⟦S⟧⇩✓ STOP)
    else ⊓b∈d ` B. (c❙!a → (P ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
                   (b → (c❙!a → P ⟦S⟧⇩✓ Q (inv_into B d b))))›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep[where A = ‹{a}›, simplified])
    (auto simp add: write_is_write0 intro: mono_GlobalNdet_eq)

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_indep :
  ‹c ` A ∩ S = {} ⟹ d b ∉ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!b → Q =
   (  if A = {} then d❙!b → (STOP ⟦S⟧⇩✓ Q)
    else ⊓a∈c ` A. (a → (P (inv_into A c a) ⟦S⟧⇩✓ d❙!b → Q)) □
                   (d❙!b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q)))›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep[where B = ‹{b}›, simplified])
    (auto simp add: write_is_write0 intro: mono_GlobalNdet_eq)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left :
  ‹c a ∉ S ⟹ d ` B ⊆ S ⟹ c❙!a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = c❙!a → (P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left[where A = ‹{a}›, simplified]) simp_all

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_left :
  ‹c ` A ∩ S = {} ⟹ d b ∈ S ⟹ c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!b → Q = c❙!❙!a∈A → (P a ⟦S⟧⇩✓ d❙!b → Q)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left[where B = ‹{b}›, simplified]) simp_all


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right :
  ‹c a ∈ S ⟹ d ` B ∩ S = {} ⟹ c❙!a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = d❙!❙!b∈B → (c❙!a → P ⟦S⟧⇩✓ Q b)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right[where A = ‹{a}›, simplified]) simp_all

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_right :
  ‹c ` A ⊆ S ⟹ d b ∉ S ⟹ c❙!❙!a∈A → P a ⟦S⟧⇩✓ d❙!b → Q = d❙!b → (c❙!❙!a∈A → P a ⟦S⟧⇩✓ Q)›
  by (subst ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right[where B = ‹{b}›, simplified]) simp_all



paragraph ‹\<^const>‹write› and \<^const>‹write››

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹c❙!a → P ⟦S⟧⇩✓ d❙!b → Q =
   (if d b ∈ S then STOP else d❙!b → (c❙!a → P ⟦S⟧⇩✓ Q)) □
   (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ d❙!b → Q)) □
   (if c a = d b ∧ d b ∈ S then c❙!a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (subst read_Sync⇩p⇩t⇩i⇩c⇩k_read[where A = ‹{a}› and B = ‹{b}›, simplified])
    (simp add: write_def insert_Diff_if Det_commute Int_insert_right)

lemma write_Inter⇩p⇩t⇩i⇩c⇩k_write :
  ‹c❙!a → P |||⇩✓ d❙!b → Q = (c❙!a → (P |||⇩✓ d❙!b → Q)) □ (d❙!b → (c❙!a → P |||⇩✓ Q))›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write Det_commute)

lemma write_Par⇩p⇩t⇩i⇩c⇩k_write :
  ‹c❙!a → P ||⇩✓ d❙!b → Q = (if c a = d b then c❙!a → (P ||⇩✓ Q) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write_subset :
  ‹c a ∈ S ⟹ d b ∈ S ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙!b → Q = (if c a = d b then c❙!a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write_indep :
  ‹c a ∉ S ⟹ d b ∉ S ⟹
   c❙!a → P ⟦S⟧⇩✓ d❙!b → Q = (c❙!a → (P ⟦S⟧⇩✓ d❙!b → Q)) □ (d❙!b → (c❙!a → P ⟦S⟧⇩✓ Q))›
  by (simp add: Det_commute write_Sync⇩p⇩t⇩i⇩c⇩k_write)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write_left :
  ‹c a ∉ S ⟹ d b ∈ S ⟹ c❙!a → P ⟦S⟧⇩✓ d❙!b → Q = c❙!a → (P ⟦S⟧⇩✓ d❙!b → Q)›
  by (auto simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write)


lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write_right :
  ‹c a ∈ S ⟹ d b ∉ S ⟹ c❙!a → P ⟦S⟧⇩✓ d❙!b → Q = d❙!b → (c❙!a → P ⟦S⟧⇩✓ Q)›
  by (auto simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write)




paragraph ‹\<^const>‹read› and \<^const>‹write0›.›

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read :
  ‹a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)) □
   (□b∈(d ` B - S) → (a → P ⟦S⟧⇩✓ Q (inv_into B d b))) □
   (if a ∈ d ` B ∩ S then a → (P ⟦S⟧⇩✓ Q (inv_into B d a)) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ b → Q =
   (if b ∈ S then STOP else b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)) □
   (□a∈(c ` A - S) → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q)) □
   (if b ∈ c ` A ∩ S then b → (P (inv_into A c b) ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read_subset :
  ‹a ∈ S ⟹ d ` B ⊆ S ⟹
   a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (if a ∈ d ` B then a → (P ⟦S⟧⇩✓ Q (inv_into B d a)) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0_subset :
  ‹c ` A ⊆ S ⟹ b ∈ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ b → Q =
   (if b ∈ c ` A then b → (P (inv_into A c b) ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write_subset[where d = ‹λx. x›, unfolded write_is_write0])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan:
  ‹a ∈ S ⟹ B ⊆ S ⟹
   a → P ⟦S⟧⇩✓ id❙?b∈B → Q b = (if a ∈ B then a → (P ⟦S⟧⇩✓ Q a) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read_subset_same_chan
      [where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0_subset_same_chan:
  ‹A ⊆ S ⟹ b ∈ S ⟹
   id❙?a∈A → P a ⟦S⟧⇩✓ b → Q = (if b ∈ A then b → (P b ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write_subset_same_chan
      [where c = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read_indep :
  ‹a ∉ S ⟹ d ` B ∩ S = {} ⟹
   a → P ⟦S⟧⇩✓ d❙?b∈B → Q b =
   (a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)) □ (d❙?b∈B → (a → P ⟦S⟧⇩✓ Q b))›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read_indep[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0_indep :
  ‹c ` A ∩ S = {} ⟹ b ∉ S ⟹
   c❙?a∈A → P a ⟦S⟧⇩✓ b → Q =
   (b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)) □ (c❙?a∈A → (P a ⟦S⟧⇩✓ b → Q))›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write_indep[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read_left :
  ‹a ∉ S ⟹ d ` B ⊆ S ⟹ a → P ⟦S⟧⇩✓ d❙?b∈B → Q b = a → (P ⟦S⟧⇩✓ d❙?b∈B → Q b)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read_left[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0_left :
  ‹c ` A ∩ S = {} ⟹ b ∈ S ⟹ c❙?a∈A → P a ⟦S⟧⇩✓ b → Q = c❙?a∈A → (P a ⟦S⟧⇩✓ b → Q)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write_left[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_read_right :
  ‹a ∈ S ⟹ d ` B ∩ S = {} ⟹ a → P ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈B → (a → P ⟦S⟧⇩✓ Q b)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_read_right[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_write0_right :
  ‹c ` A ⊆ S ⟹ b ∉ S ⟹ c❙?a∈A → P a ⟦S⟧⇩✓ b → Q = b → (c❙?a∈A → P a ⟦S⟧⇩✓ Q)›
  by (simp add: read_Sync⇩p⇩t⇩i⇩c⇩k_write_right[where d = id, unfolded write_is_write0, simplified])



paragraph ‹\<^const>‹ndet_write› and \<^const>‹write0››

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then a → P ⟦S⟧⇩✓ STOP
    else ⊓b∈d ` B. (if b ∈ S then STOP else b → (a → P ⟦S⟧⇩✓ Q (inv_into B d b))) □
                   (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
                   (if b = a ∧ a ∈ S then a → (P ⟦S⟧⇩✓ Q (inv_into B d a)) else STOP))›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write[where c = ‹λx. x›, unfolded write_is_write0, simplified])

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ b → Q =
   (  if A = {} then STOP ⟦S⟧⇩✓ b → Q
    else ⊓a∈c ` A. (if a ∈ S then STOP else a → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q)) □
                   (if b ∈ S then STOP else b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q)) □
                   (if a = b ∧ b ∈ S then b → (P (inv_into A c a) ⟦S⟧⇩✓ Q) else STOP))›
  by (simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write[where d = ‹λx. x›, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset :
  ‹a ∈ S ⟹ d ` B ⊆ S ⟹
   a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if a ∉ d ` B then STOP else if d ` B = {a} then a → (P ⟦S⟧⇩✓ Q (inv_into B d a))
    else (a → (P ⟦S⟧⇩✓ Q (inv_into B d a))) ⊓ STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_subset[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write0_subset :
  ‹c ` A ⊆ S ⟹ b ∈ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ b → Q =
   (  if b ∉ c ` A then STOP else if c ` A = {b} then b → (P (inv_into A c b) ⟦S⟧⇩✓ Q)
    else (b → (P (inv_into A c b) ⟦S⟧⇩✓ Q)) ⊓ STOP)›
  by (simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_subset[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep :
  ‹a ∉ S ⟹ d ` B ∩ S = {} ⟹
   a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if B = {} then a → (P ⟦S⟧⇩✓ STOP)
    else ⊓b∈d ` B. (a → (P ⟦S⟧⇩✓ b → Q (inv_into B d b))) □
                   (b → (a → P ⟦S⟧⇩✓ Q (inv_into B d b))))›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_indep[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write0_indep :
  ‹c ` A ∩ S = {} ⟹ b ∉ S ⟹
   c❙!❙!a∈A → P a ⟦S⟧⇩✓ b → Q =
   (  if A = {} then b → (STOP ⟦S⟧⇩✓ Q)
    else ⊓a∈c ` A. (a → (P (inv_into A c a) ⟦S⟧⇩✓ b → Q)) □
                   (b → (a → P (inv_into A c a) ⟦S⟧⇩✓ Q)))›
  by (simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_indep[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left :
  ‹a ∉ S ⟹ d ` B ⊆ S ⟹ a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = a → (P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_left[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write0_left :
  ‹c ` A ∩ S = {} ⟹ b ∈ S ⟹ c❙!❙!a∈A → P a ⟦S⟧⇩✓ b → Q = c❙!❙!a∈A → (P a ⟦S⟧⇩✓ b → Q)›
  by (simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_left[where d = id, unfolded write_is_write0, simplified])

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write0_right :
  ‹a ∈ S ⟹ d ` B ∩ S = {} ⟹ a → P ⟦S⟧⇩✓ d❙!❙!b∈B → Q b = d❙!❙!b∈B → (a → P ⟦S⟧⇩✓ Q b)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write_right[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write0_right :
  ‹c ` A ⊆ S ⟹ b ∉ S ⟹ c❙!❙!a∈A → P a ⟦S⟧⇩✓ b → Q = b → (c❙!❙!a∈A → P a ⟦S⟧⇩✓ Q)›
  by (simp add: ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_write_right[where d = id, unfolded write_is_write0, simplified])



paragraph ‹\<^const>‹write0› and \<^const>‹write0››

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹a → P ⟦S⟧⇩✓ b → Q =
   (if b ∈ S then STOP else b → (a → P ⟦S⟧⇩✓ Q)) □
   (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ b → Q)) □
   (if a = b ∧ b ∈ S then a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_bis :
  ‹(a → P) ⟦S⟧⇩✓ (b → Q) =
   (  if a ∈ S
    then   if b ∈ S
         then   if a = b
              then a → (P ⟦S⟧⇩✓ Q)
              else STOP
         else (b → ((a → P) ⟦S⟧⇩✓ Q))
    else   if b ∈ S
         then a → (P ⟦S⟧⇩✓ (b → Q))
    else (a → (P ⟦S⟧⇩✓ (b → Q))) □ (b → ((a → P) ⟦S⟧⇩✓ Q)))›
  by (cases ‹a ∈ S›; cases ‹b ∈ S›) (auto simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0 Det_commute)

lemma write0_Inter⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹a → P |||⇩✓ b → Q = (a → (P |||⇩✓ b → Q)) □ (b → (a → P |||⇩✓ Q))›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0 Det_commute)

lemma write0_Par⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹a → P ||⇩✓ b → Q = (if a = b then a → (P ||⇩✓ Q) else STOP)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0)



lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_subset :
  ‹a ∈ S ⟹ b ∈ S ⟹ a → P ⟦S⟧⇩✓ b → Q = (if a = b then a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write_subset[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_indep :
  ‹a ∉ S ⟹ b ∉ S ⟹ a → P ⟦S⟧⇩✓ b → Q = (a → (P ⟦S⟧⇩✓ b → Q)) □ (b → (a → P ⟦S⟧⇩✓ Q))›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write_indep[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_left :
  ‹a ∉ S ⟹ b ∈ S ⟹ a → P ⟦S⟧⇩✓ b → Q = a → (P ⟦S⟧⇩✓ b → Q)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write_left[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_right :
  ‹a ∈ S ⟹ b ∉ S ⟹ a → P ⟦S⟧⇩✓ b → Q = b → (a → P ⟦S⟧⇩✓ Q)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write_right[where c = id and d = id, unfolded write_is_write0, simplified]) 


paragraph ‹\<^const>‹write› and \<^const>‹write0››

lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹a → P ⟦S⟧⇩✓ d❙!b → Q =
   (if d b ∈ S then STOP else d❙!b → (a → P ⟦S⟧⇩✓ Q)) □
   (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ d❙!b → Q)) □
   (if a = d b ∧ d b ∈ S then a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0 write_is_write0)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹c❙!a → P ⟦S⟧⇩✓ b → Q =
   (if b ∈ S then STOP else b → (c❙!a → P ⟦S⟧⇩✓ Q)) □
   (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ b → Q)) □
   (if c a = b ∧ b ∈ S then c❙!a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0 write_is_write0)


lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write_subset :
  ‹a ∈ S ⟹ d b ∈ S ⟹
   a → P ⟦S⟧⇩✓ d❙!b → Q = (if a = d b then a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write0_subset :
  ‹c a ∈ S ⟹ b ∈ S ⟹
   c❙!a → P ⟦S⟧⇩✓ b → Q = (if c a = b then c❙!a → (P ⟦S⟧⇩✓ Q) else STOP)›
  by (simp add: write_Sync⇩p⇩t⇩i⇩c⇩k_write0)


lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write_indep :
  ‹a ∉ S ⟹ d b ∉ S ⟹
   a → P ⟦S⟧⇩✓ d❙!b → Q = (a → (P ⟦S⟧⇩✓ d❙!b → Q)) □ (d❙!b → (a → P ⟦S⟧⇩✓ Q))›
  by (simp add: Det_commute write0_Sync⇩p⇩t⇩i⇩c⇩k_write)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write0_indep :
  ‹c a ∉ S ⟹ b ∉ S ⟹
   c❙!a → P ⟦S⟧⇩✓ b → Q = (c❙!a → (P ⟦S⟧⇩✓ b → Q)) □ (b → (c❙!a → P ⟦S⟧⇩✓ Q))›
  by (simp add: Det_commute write_Sync⇩p⇩t⇩i⇩c⇩k_write0)


lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write_left :
  ‹a ∉ S ⟹ d b ∈ S ⟹ a → P ⟦S⟧⇩✓ d❙!b → Q = a → (P ⟦S⟧⇩✓ d❙!b → Q)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_left write_is_write0)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write0_left :
  ‹c a ∉ S ⟹ b ∈ S ⟹ c❙!a → P ⟦S⟧⇩✓ b → Q = c❙!a → (P ⟦S⟧⇩✓ b → Q)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_left write_is_write0)


lemma write0_Sync⇩p⇩t⇩i⇩c⇩k_write_right :
  ‹a ∈ S ⟹ d b ∉ S ⟹ a → P ⟦S⟧⇩✓ d❙!b → Q = d❙!b → (a → P ⟦S⟧⇩✓ Q)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_right write_is_write0)

lemma write_Sync⇩p⇩t⇩i⇩c⇩k_write0_right :
  ‹c a ∈ S ⟹ b ∉ S ⟹ c❙!a → P ⟦S⟧⇩✓ b → Q = b → (c❙!a → P ⟦S⟧⇩✓ Q)›
  by (simp add: write0_Sync⇩p⇩t⇩i⇩c⇩k_write0_right write_is_write0)



subsubsection ‹Synchronization with \<^const>‹SKIP› and \<^const>‹STOP››

paragraph ‹\<^const>‹SKIP››

text ‹Without injectivity, the result is a trivial corollary of
      @{thm read_def[no_vars]} and @{thm Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP[no_vars]}.›

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ SKIP r = c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ SKIP r)› if ‹inj_on c A›
proof -
  have ‹c ` (A - c -` S) = c ` A - S› by blast
  show ‹c❙?a∈A → P a ⟦S⟧⇩✓ SKIP r = c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ SKIP r)›
    by (auto simp add: read_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP ‹?this› inj_on_diff ‹inj_on c A›
        intro: mono_Mprefix_eq)
qed

lemma SKIP_Sync⇩p⇩t⇩i⇩c⇩k_read :
  ‹SKIP r ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (SKIP r ⟦S⟧⇩✓ Q b)› if ‹inj_on d B›
proof -
  have ‹d ` (B - d -` S) = d ` B - S› by blast
  show ‹SKIP r ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (SKIP r ⟦S⟧⇩✓ Q b)›
    by (auto simp add: read_def SKIP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix ‹?this› inj_on_diff ‹inj_on d B›
        intro: mono_Mprefix_eq)
qed


corollary write_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹c❙!a → P ⟦S⟧⇩✓ SKIP s = (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ SKIP s))›
  and SKIP_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹SKIP r ⟦S⟧⇩✓ d❙!b → Q = (if d b ∈ S then STOP else d❙!b → (SKIP r ⟦S⟧⇩✓ Q))›
  by (simp_all add: write_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP SKIP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix Diff_triv)

corollary write0_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹a → P ⟦S⟧⇩✓ SKIP s = (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ SKIP s))›
  and SKIP_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹SKIP r ⟦S⟧⇩✓ b → Q = (if b ∈ S then STOP else b → (SKIP r ⟦S⟧⇩✓ Q))›
  by (simp_all add: write0_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP SKIP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix Diff_triv)


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ SKIP r =
   (  if c ` A ∩ S = {} then c❙!❙!a∈A → (P a ⟦S⟧⇩✓ SKIP r)
    else (c❙!❙!a∈(A - c -` S) → (P a ⟦S⟧⇩✓ SKIP r)) ⊓ STOP)›
  (is ‹?lhs = (if _ then ?rhs1 else ?rhs2 ⊓ STOP)›) if ‹inj_on c A›
proof (split if_split, intro conjI impI)
  assume ‹c ` A ∩ S = {}›
  hence ‹A - c -` S = A› by blast
  from ‹c ` A ∩ S = {}› show ‹?lhs = ?rhs1›
    by (auto simp add: ‹?this› ndet_write_is_GlobalNdet_write0 disjoint_iff
        Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right write0_Sync⇩p⇩t⇩i⇩c⇩k_SKIP
        intro!: mono_GlobalNdet_eq split: if_split_asm)
next
  show ‹?lhs = ?rhs2 ⊓ STOP› if ‹c ` A ∩ S ≠ {}›
  proof (cases ‹c ` A - S = {}›)
    assume ‹c ` A - S = {}›
    hence ‹A - c -` S = {}› by blast
    from ‹c ` A - S = {}› show ‹?lhs = ?rhs2 ⊓ STOP›
      by (auto simp add: ndet_write_is_GlobalNdet_write0 GlobalNdet_is_STOP_iff
          ‹?this› Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right write0_Sync⇩p⇩t⇩i⇩c⇩k_SKIP)
  next
    have ‹c ` (A - c -` S) = c ` A - S› by blast
    show ‹?lhs = ?rhs2 ⊓ STOP› if ‹c ` A - S ≠ {}›
      by (subst Ndet_commute, unfold ndet_write_is_GlobalNdet_write0 Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right)
        (auto simp add: GlobalNdet_is_STOP_iff write0_Sync⇩p⇩t⇩i⇩c⇩k_SKIP
          ‹?this› ‹inj_on c A› inj_on_diff
          simp flip: GlobalNdet_factorization_union
          [OF ‹c ` A ∩ S ≠ {}› ‹c ` A - S ≠ {}›, unfolded Int_Diff_Un]
          intro!: arg_cong2[where f = ‹(⊓)›] mono_GlobalNdet_eq)
  qed
qed

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) SKIP_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹inj_on d B ⟹ SKIP r ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if d ` B ∩ S = {} then d❙!❙!b∈B → (SKIP r ⟦S⟧⇩✓ Q b)
    else (d❙!❙!b∈(B - d -` S) → (SKIP r ⟦S⟧⇩✓ Q b)) ⊓ STOP)›
  by (subst (1 2 3) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_SKIP)




corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP :
  ‹⊓a ∈ A → P a ⟦S⟧⇩✓ SKIP r =
   (if A ∩ S = {} then ⊓a ∈ A → (P a ⟦S⟧⇩✓ SKIP r)
   else (⊓a ∈ (A - S) → (P a ⟦S⟧⇩✓ SKIP r)) ⊓ STOP)›  
  using ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_SKIP[of id A P S r]
  by (simp add: ndet_write_id_is_Mndetprefix)

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) Sync⇩p⇩t⇩i⇩c⇩k_SKIP_Mndetprefix :
  ‹SKIP r ⟦S⟧⇩✓ ⊓b ∈ B → Q b =
   (  if B ∩ S = {} then ⊓b ∈ B → (SKIP r ⟦S⟧⇩✓ Q b)
    else (⊓b ∈ (B - S) → (SKIP r ⟦S⟧⇩✓ Q b)) ⊓ STOP)›
  by (subst (1 2 3) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Mndetprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP)



paragraph ‹\<^const>‹STOP››

text ‹Without injectivity, the result is a trivial corollary of
      @{thm read_def[no_vars]} and @{thm Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_SKIP[no_vars]}.›

lemma read_Sync⇩p⇩t⇩i⇩c⇩k_STOP :
  ‹c❙?a∈A → P a ⟦S⟧⇩✓ STOP = c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ STOP)› if ‹inj_on c A›
proof -
  have ‹c ` (A - c -` S) = c ` A - S› by blast
  show ‹c❙?a∈A → P a ⟦S⟧⇩✓ STOP = c❙?a∈(A - c -` S) → (P a ⟦S⟧⇩✓ STOP)›
    by (auto simp add: ‹?this› read_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_STOP inj_on_diff ‹inj_on c A›
        intro: mono_Mprefix_eq)
qed

lemma STOP_Sync⇩p⇩t⇩i⇩c⇩k_read :
  ‹STOP ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (STOP ⟦S⟧⇩✓ Q b)› if ‹inj_on d B›
proof -
  have ‹d ` (B - d -` S) = d ` B - S› by blast
  show ‹STOP ⟦S⟧⇩✓ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (STOP ⟦S⟧⇩✓ Q b)›
    by (auto simp add: ‹?this› read_def STOP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix inj_on_diff ‹inj_on d B›
        intro: mono_Mprefix_eq)
qed


corollary write_Sync⇩p⇩t⇩i⇩c⇩k_STOP :
  ‹c❙!a → P ⟦S⟧⇩✓ STOP = (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧⇩✓ STOP))›
  and STOP_Sync⇩p⇩t⇩i⇩c⇩k_write :
  ‹STOP ⟦S⟧⇩✓ d❙!b → Q = (if d b ∈ S then STOP else d❙!b → (STOP ⟦S⟧⇩✓ Q))›
  by (simp_all add: write_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_STOP STOP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix Diff_triv)

corollary write0_Sync⇩p⇩t⇩i⇩c⇩k_STOP :
  ‹a → P ⟦S⟧⇩✓ STOP = (if a ∈ S then STOP else a → (P ⟦S⟧⇩✓ STOP))›
  and STOP_Sync⇩p⇩t⇩i⇩c⇩k_write0 :
  ‹STOP ⟦S⟧⇩✓ b → Q = (if b ∈ S then STOP else b → (STOP ⟦S⟧⇩✓ Q))›
  by (simp_all add: write0_def Mprefix_Sync⇩p⇩t⇩i⇩c⇩k_STOP STOP_Sync⇩p⇩t⇩i⇩c⇩k_Mprefix Diff_triv)


lemma ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_STOP :
  ‹c❙!❙!a∈A → P a ⟦S⟧⇩✓ STOP =
   (  if c ` A ∩ S = {} then c❙!❙!a∈A → (P a ⟦S⟧⇩✓ STOP)
    else (c❙!❙!a∈(A - c -` S) → (P a ⟦S⟧⇩✓ STOP)) ⊓ STOP)›
  (is ‹?lhs = (if _ then ?rhs1 else ?rhs2 ⊓ STOP)›) if ‹inj_on c A›
proof (split if_split, intro conjI impI)
  assume ‹c ` A ∩ S = {}›
  hence ‹A - c -` S = A› by blast
  from ‹c ` A ∩ S = {}› show ‹?lhs = ?rhs1›
    by (auto simp add: ‹?this› ndet_write_is_GlobalNdet_write0 disjoint_iff
        Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right write0_Sync⇩p⇩t⇩i⇩c⇩k_STOP
        intro!: mono_GlobalNdet_eq split: if_split_asm)
next
  show ‹?lhs = ?rhs2 ⊓ STOP› if ‹c ` A ∩ S ≠ {}›
  proof (cases ‹c ` A - S = {}›)
    assume ‹c ` A - S = {}›
    hence ‹A - c -` S = {}› by blast
    from ‹c ` A - S = {}› show ‹?lhs = ?rhs2 ⊓ STOP›
      by (auto simp add: ndet_write_is_GlobalNdet_write0 GlobalNdet_is_STOP_iff
          ‹?this› Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right write0_Sync⇩p⇩t⇩i⇩c⇩k_STOP)
  next
    have ‹c ` (A - c -` S) = c ` A - S› by blast
    show ‹?lhs = ?rhs2 ⊓ STOP› if ‹c ` A - S ≠ {}›
      by (subst Ndet_commute, unfold ndet_write_is_GlobalNdet_write0 Sync⇩p⇩t⇩i⇩c⇩k_distrib_GlobalNdet_right)
        (auto simp add: GlobalNdet_is_STOP_iff write0_Sync⇩p⇩t⇩i⇩c⇩k_STOP
          ‹?this› ‹inj_on c A› inj_on_diff
          simp flip: GlobalNdet_factorization_union
          [OF ‹c ` A ∩ S ≠ {}› ‹c ` A - S ≠ {}›, unfolded Int_Diff_Un]
          intro!: arg_cong2[where f = ‹(⊓)›] mono_GlobalNdet_eq)
  qed
qed

corollary (in Sync⇩p⇩t⇩i⇩c⇩k_locale) STOP_Sync⇩p⇩t⇩i⇩c⇩k_ndet_write :
  ‹inj_on d B ⟹ STOP ⟦S⟧⇩✓ d❙!❙!b∈B → Q b =
   (  if d ` B ∩ S = {} then d❙!❙!b∈B → (STOP ⟦S⟧⇩✓ Q b)
    else (d❙!❙!b∈(B - d -` S) → (STOP ⟦S⟧⇩✓ Q b)) ⊓ STOP)›
  by (subst (1 2 3) Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.Sync⇩p⇩t⇩i⇩c⇩k_sym)
    (simp add: Sync⇩p⇩t⇩i⇩c⇩k_locale_sym.ndet_write_Sync⇩p⇩t⇩i⇩c⇩k_STOP)


end



(*<*)
end
  (*>*)