Theory Read_Write_CSP_Laws

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Support for read and write operations
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)

section‹Read and Write Laws›

(*<*)
theory Read_Write_CSP_Laws
  imports Step_CSP_Laws_Extended
begin
  (*>*)


subsection ‹Projections›

subsubsection ‹\<^const>‹read››

lemma F_read :
  ‹ℱ (c❙?a∈A → P a) = {([], X) |X. X ∩ ev ` c ` A = {}} ∪
                      {(ev a # s, X) |a s X. a ∈ c ` A ∧ (s, X) ∈ ℱ ((P ∘ inv_into A c) a)}›
  by (simp add: read_def F_Mprefix)

lemma F_read_inj_on :
  ‹inj_on c A ⟹
   ℱ (c❙?a∈A → P a) = {([], X) |X. X ∩ ev ` c ` A = {}} ∪
                      {(ev (c a) # s, X) |a s X. a ∈ A ∧ (s, X) ∈ ℱ (P a)}›
  by (auto simp add: F_read)


lemma D_read :
  ‹𝒟 (c❙?a∈A → P a) = {ev a # s |a s. a ∈ c ` A ∧ s ∈ 𝒟 ((P ∘ inv_into A c) a)}›
  by (simp add: read_def D_Mprefix)

lemma D_read_inj_on :
  ‹inj_on c A ⟹ 𝒟 (c❙?a∈A → P a) = {ev (c a) # s |a s. a ∈ A ∧ s ∈ 𝒟 (P a)}›
  by (auto simp add: D_read)


lemma T_read :
  ‹𝒯 (c❙?a∈A → P a) = insert [] {ev a # s |a s. a ∈ c ` A ∧ s ∈ 𝒯 ((P ∘ inv_into A c) a)}›
  by (simp add: read_def T_Mprefix)

lemma T_read_inj_on :
  ‹inj_on c A ⟹ 𝒯 (c❙?a∈A → P a) = insert [] {ev (c a) # s |a s. a ∈ A ∧ s ∈ 𝒯 (P a)}›
  by (auto simp add: T_read)


lemmas read_projs = F_read D_read T_read
  and read_inj_on_projs = F_read_inj_on D_read_inj_on T_read_inj_on



subsubsection ‹\<^const>‹ndet_write››

lemma F_ndet_write :
  ‹ℱ (c❙!❙!a∈A → P a) =
   (  if A = {} then {(s, X). s = []}
    else {([], X) |X. ∃a∈A. ev (c a) ∉ X} ∪
         {(ev a # s, X) |a s X. a ∈ c ` A ∧ (s, X) ∈ ℱ ((P ∘ inv_into A c) a)})›
  by (simp add: ndet_write_def F_Mndetprefix')

lemma F_ndet_write_inj_on :
  ‹inj_on c A ⟹
   ℱ (c❙!❙!a∈A → P a) =
   (  if A = {} then {(s, X). s = []}
    else {([], X) |X. ∃a∈A. ev (c a) ∉ X} ∪
         {(ev (c a) # s, X) |a s X. a ∈ A ∧ (s, X) ∈ ℱ (P a)})›
  by (auto simp add: F_ndet_write)


lemma D_ndet_write :
  ‹𝒟 (c❙!❙!a∈A → P a) = {ev a # s |a s. a ∈ c ` A ∧ s ∈ 𝒟 ((P ∘ inv_into A c) a)}›
  by (simp add: ndet_write_def D_Mndetprefix')

lemma D_ndet_write_inj_on :
  ‹inj_on c A ⟹ 𝒟 (c❙!❙!a∈A → P a) = {ev (c a) # s |a s. a ∈ A ∧ s ∈ 𝒟 (P a)}›
  by (auto simp add: D_ndet_write)


lemma T_ndet_write :
  ‹𝒯 (c❙!❙!a∈A → P a) = insert [] {ev a # s |a s. a ∈ c ` A ∧ s ∈ 𝒯 ((P ∘ inv_into A c) a)}›
  by (simp add: ndet_write_def T_Mndetprefix')

lemma T_ndet_write_inj_on :
  ‹inj_on c A ⟹ 𝒯 (c❙!❙!a∈A → P a) = insert [] {ev (c a) # s |a s. a ∈ A ∧ s ∈ 𝒯 (P a)}›
  by (auto simp add: T_ndet_write)


lemmas ndet_write_projs = F_ndet_write D_ndet_write T_ndet_write
  and ndet_write_inj_on_projs = F_ndet_write_inj_on D_ndet_write_inj_on T_ndet_write_inj_on



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

lemma F_write :
  ‹ℱ (c❙!a → P) = {([], X) |X. ev (c a) ∉ X} ∪ {(ev (c a) # s, X) |s X. (s, X) ∈ ℱ P}›
  by (simp add: write_def F_Mprefix)

lemma F_write0 :
  ‹ℱ (a → P) = {([], X) |X. ev a ∉ X} ∪ {(ev a # s, X) |s X. (s, X) ∈ ℱ P}›
  by (simp add: write0_def F_Mprefix)


lemma D_write : ‹𝒟 (c❙!a → P) = {ev (c a) # s |s. s ∈ 𝒟 P}›
  by (simp add: write_def D_Mprefix)

lemma D_write0 : ‹𝒟 (a → P) = {ev a # s |s. s ∈ 𝒟 P}›
  by (simp add: write0_def D_Mprefix)


lemma T_write : ‹𝒯 (c❙!a → P) = insert [] {ev (c a) # s |s. s ∈ 𝒯 P}›
  by (simp add: write_def T_Mprefix)

lemma T_write0 : ‹𝒯 (a → P) = insert [] {ev a # s |s. s ∈ 𝒯 P}›
  by (simp add: write0_def T_Mprefix)


lemmas write_projs = F_write D_write T_write
  and write0_projs = F_write0 D_write0 T_write0




subsection ‹Equality with Constant Process›

subsubsection ‹\<^const>‹STOP››

lemma read_is_STOP_iff : ‹c❙?a∈A → P a = STOP ⟷ A = {}›
  by (simp add: read_def Mprefix_is_STOP_iff)

lemma read_empty [simp] : ‹c❙?a∈{} → P a = STOP› by (simp add: read_def)

lemma ndet_write_is_STOP_iff : ‹c❙!❙!a∈A → P a = STOP ⟷ A = {}›
  by (simp add: ndet_write_def Mndetprefix_is_STOP_iff)

lemma ndet_write_empty [simp] : ‹c❙!❙!a∈{} → P a = STOP› by (simp add: ndet_write_def)

lemma write0_neq_STOP [simp] : ‹a → P ≠ STOP› by (simp add: write0_def Mprefix_is_STOP_iff)

lemma write_neq_STOP [simp] : ‹c❙!a → P ≠ STOP› by (simp add: write_is_write0)



subsubsection ‹\<^const>‹SKIP››

lemma read_neq_SKIP [simp] : ‹c❙?a∈A → P a ≠ SKIP r› by (simp add: read_def)

lemma ndet_write_neq_SKIP [simp] : ‹c❙!❙!a∈A → P a ≠ SKIP r› by (simp add: ndet_write_def)

lemma write0_neq_SKIP [simp] : ‹a → P ≠ SKIP r› by (simp add: write0_def)

lemma write_neq_SKIP [simp] : ‹c❙!a → P ≠ SKIP r› by (simp add: write_is_write0)



subsubsection ‹\<^term>‹⊥››

lemma read_neq_BOT [simp] : ‹c❙?a∈A → P a ≠ ⊥› by (simp add: read_def)

lemma ndet_write_neq_BOT [simp] : ‹c❙!❙!a∈A → P a ≠ ⊥› by (simp add: ndet_write_def)

lemma write0_neq_BOT [simp] : ‹a → P ≠ ⊥› by (simp add: write0_def)

lemma write_neq_BOT [simp] : ‹c❙!a → P ≠ ⊥› by (simp add: write_is_write0)




subsection ‹Extensions of Step-Laws›

subsubsection ‹Monotony for equality›

lemma mono_read_eq :
  ‹(⋀a. a ∈ A ⟹ P a = Q a) ⟹ read c A P = read c A Q›
  by (auto simp add: read_def inv_into_into intro!: mono_Mprefix_eq)

lemma mono_ndet_write_eq :
  ‹(⋀a. a ∈ A ⟹ P a = Q a) ⟹ ndet_write c A P = ndet_write c A Q›
  by (auto simp add: ndet_write_def inv_into_into intro!: mono_Mndetprefix_eq)


subsubsection ‹\<^const>‹Det› and \<^const>‹Ndet››

lemma read_Ndet_read :
  ‹(c❙?a∈A → P a) ⊓ (c❙?b∈B → Q b) =
   (c❙?a∈(A - B) → P a) ⊓ (c❙?b∈(B - A) → Q b) □ (c❙?x∈(A ∩ B) → P x ⊓ Q x)›
  (is ‹?lhs = ?rhs›) if ‹inj_on c (A ∪ B)›
proof -
  have   * : ‹c ` A - c ` B = c ` (A - B)›
    by (metis Diff_subset inj_on_image_set_diff le_supI1 sup.cobounded2 ‹inj_on c (A ∪ B)›)
  have  ** : ‹c ` B - c ` A = c ` (B - A)›
    by (metis Diff_subset Un_upper1 inj_on_image_set_diff le_supI2 ‹inj_on c (A ∪ B)›)
  have *** : ‹c ` A ∩ c ` B = c ` (A ∩ B)›
    by (metis inf_sup_ord(3) inj_on_image_Int sup_ge2 ‹inj_on c (A ∪ B)›)
  from ‹inj_on c (A ∪ B)› have ‹inj_on c (A - B)› by (simp add: inj_on_Un inj_on_diff)
  with ‹inj_on c (A ∪ B)› have   $ : ‹a ∈ A - B ⟹ inv_into A c (c a) = inv_into (A - B) c (c a)› for a
    by (auto simp add: inj_on_Un)
  from ‹inj_on c (A ∪ B)› have ‹inj_on c (B - A)› by (simp add: inj_on_Un inj_on_diff)
  with ‹inj_on c (A ∪ B)› have  $$ : ‹b ∈ B - A ⟹ inv_into B c (c b) = inv_into (B - A) c (c b)› for b
    by (auto simp add: inj_on_Un)
  have $$$ : ‹inv_into A c (c a) = inv_into (A ∩ B) c (c a)›
    ‹inv_into B c (c a) = inv_into (A ∩ B) c (c a)› if ‹a ∈ A ∩ B› for a
    using ‹a ∈ A ∩ B› ‹inj_on c (A ∪ B)› by (auto simp add: inj_on_Un inj_on_Int)
  show ‹?lhs = ?rhs›
    by (unfold read_def, subst Mprefix_Ndet_Mprefix)
      (auto simp add: "*" "**" "***" "$" "$$" "$$$"
        intro!: mono_Mprefix_eq arg_cong[where f = P] arg_cong2[where f = ‹(□)›]
        arg_cong2[where f = ‹(⊓)›])
qed

lemma read_Det_read :
  ‹(c❙?a∈A → P a) □ (c❙?b∈B → Q b) =
   c❙?a∈(A ∪ B) → (if a ∈ A ∩ B then P a ⊓ Q a else if a ∈ A then P a else Q a)›
  (is ‹?lhs = ?rhs›) if ‹inj_on c (A ∪ B)›
proof -
  have * : ‹c ` A ∪ c ` B = c ` (A ∪ B)› by blast
  from ‹inj_on c (A ∪ B)›
  have $ : ‹a ∈ A ⟹ inv_into A c (c a) = inv_into (A ∪ B) c (c a)›
    ‹b ∈ B ⟹ inv_into B c (c b) = inv_into (A ∪ B) c (c b)› for a b
    by (simp_all add: inj_on_Un)
  from ‹inj_on c (A ∪ B)› show ‹?lhs = ?rhs›
    by (auto simp add: read_def Mprefix_Det_Mprefix "*" "$"
        intro!: mono_Mprefix_eq) (metis Un_iff inj_onD)+
qed


lemma ndet_write_Det_ndet_write :
  ‹(c❙!❙!a∈A → P a) □ (c❙!❙!b∈B → Q b) =
   (  if A = {} then (c❙!❙!b∈B → Q b)
    else   if B = {} then (c❙!❙!a∈A → P a)
         else ⊓a∈A. ⊓b∈B. (if a = b then c❙!a → P a ⊓ Q a else (c❙!a → P a) □ (c❙!b → Q b)))›
  if ‹inj_on c (A ∪ B)›
proof -
  have * : ‹a ∈ A ⟹ inv_into A c (c a) = inv_into (A ∪ B) c (c a)›
    ‹b ∈ B ⟹ inv_into B c (c b) = inv_into (A ∪ B) c (c b)› for a b
    using ‹inj_on c (A ∪ B)› by (auto simp add: inj_on_Un)
  from ‹inj_on c (A ∪ B)› show ?thesis
    by (auto simp add: ndet_write_def Mndetprefix_Det_Mndetprefix "*" write_is_write0 inj_on_eq_iff
        split: if_split_asm intro!: mono_GlobalNdet_eq2)
qed

lemma ndet_write_Ndet_ndet_write :
  ‹(c❙!❙!a∈A → P a) ⊓ (c❙!❙!b∈B → Q b) =
   (  if A = B then (c❙!❙!b∈B → P b ⊓ Q b)
    else   if A ⊆ B
         then (c❙!❙!b∈(B - A) → Q b) ⊓ (c❙!❙!a∈A → P a ⊓ Q a)
         else   if B ⊆ A
              then (c❙!❙!a∈(A - B) → P a) ⊓ (c❙!❙!b∈B → P b ⊓ Q b)
              else (c❙!❙!a∈(A - B) → P a) ⊓ (c❙!❙!b∈(B - A) → Q b) ⊓ (c❙!❙!a∈(A ∩ B) → P a ⊓ Q a))›
  if ‹A ∩ B ≠ {}› ‹inj_on c (A ∪ B)›
proof -
  have * : ‹a ∈ A ⟹ inv_into A c (c a) = inv_into (A ∪ B) c (c a)›
    ‹b ∈ B ⟹ inv_into B c (c b) = inv_into (A ∪ B) c (c b)›
    ‹a ∈ A - B ⟹ inv_into (A - B) c (c a) = inv_into A c (c a)›
    ‹b ∈ B - A ⟹ inv_into (B - A) c (c b) = inv_into B c (c b)›
    ‹x ∈ A ∩ B ⟹ inv_into (A ∪ B) c (c x) = inv_into (A ∩ B) c (c x)› for a b x
    using ‹inj_on c (A ∪ B)› by (auto simp add: inj_on_Un inj_on_diff inj_on_Int)
  from ‹inj_on c (A ∪ B)› have $ : ‹c ` A ⊆ c ` B ⟷ A ⊆ B› ‹c ` B ⊆ c ` A ⟷ B ⊆ A›
    by (auto simp add: inj_on_eq_iff)
  hence $$ : ‹c ` A = c ` B ⟷ A = B› by blast
  from ‹inj_on c (A ∪ B)› 
  have $$$ : ‹c ` A - c ` B = c ` (A - B)› ‹c ` B - c ` A = c ` (B - A)› ‹c ` A ∩ c ` B = c ` (A ∩ B)›
    by (auto simp add: inj_on_eq_iff)
  from ‹A ∩ B ≠ {}› have ‹c ` A ∩ c ` B ≠ {}› by blast
  show ?thesis
    by (auto simp add: Mndetprefix_Ndet_Mndetprefix[OF ‹c ` A ∩ c ` B ≠ {}›]
        "$" "$$" "$$$" "*" comp_def ndet_write_def
        intro!: mono_Mndetprefix_eq arg_cong2[where f = ‹(⊓)›])
qed



lemma write0_Ndet_write0 : ‹(a → P) ⊓ (a → Q) = a → P ⊓ Q›
  by (auto simp: Process_eq_spec write0_def D_Ndet F_Ndet F_Mprefix D_Mprefix Un_def)

lemma write0_Det_write0_is_write0_Ndet_write0 : ‹(a → P) □ (a → Q) = (a → P) ⊓ (a → Q)›
  by (simp add: write0_def Mprefix_Det_Mprefix) (simp add: Mprefix_singl write0_Ndet_write0)

lemma write_Ndet_write : ‹(c❙!a → P) ⊓ (c❙!a → Q) = c❙!a → P ⊓ Q›
  by (simp add: write0_Ndet_write0 write_is_write0)

lemma write_Det_write_is_write_Ndet_write: ‹(c❙!a → P) □ (c❙!a → Q) = (c❙!a → P) ⊓ (c❙!a → Q)›
  by (simp add: write0_Det_write0_is_write0_Ndet_write0 write_is_write0)



lemma write_Ndet_read :
  ‹(c❙!a → P) ⊓ (c❙?b∈B → Q b) =
   (if a ∈ B then STOP else c❙!a → P) ⊓ (c❙?b∈(B - {a}) → Q b) □ (if a ∈ B then c❙!a → P ⊓ Q a else STOP)›
  if ‹inj_on c ({a} ∪ B)›
  by (subst read_Ndet_read[OF ‹inj_on c ({a} ∪ B)›, simplified])
    (auto simp add: insert_Diff_if intro: arg_cong2[where f = ‹(□)›] arg_cong2[where f = ‹(⊓)›])

lemma read_Ndet_write :
  ‹inj_on c (A ∪ {b}) ⟹ (c❙?a∈A → P a) ⊓ (c❙!b → Q) =
   (if b ∈ A then STOP else c❙!b → Q) ⊓ (c❙?a∈(A - {b}) → P a) □ (if b ∈ A then c❙!b → P b ⊓ Q else STOP)›
  by (subst Ndet_commute, subst write_Ndet_read) (simp_all add: Ndet_commute)

lemma write0_Ndet_Mprefix :
  ‹(a → P) ⊓ (□b∈B → Q b) =
   (if a ∈ B then STOP else a → P) ⊓ (□b∈(B - {a}) → Q b) □ (if a ∈ B then a → P ⊓ Q a else STOP)›
  by (subst write_Ndet_read[where c = id, unfolded write_is_write0, simplified]) simp

lemma Mprefix_Ndet_write0 :
  ‹(□a∈A → P a) ⊓ (b → Q) =
   (if b ∈ A then STOP else b → Q) ⊓ (□a∈(A - {b}) → P a) □ (if b ∈ A then b → P b ⊓ Q else STOP)›
  by (subst read_Ndet_write[where c = id, unfolded write_is_write0, simplified]) simp 


lemma write_Det_read :
  ‹inj_on c (insert a B) ⟹ (c❙!a → P) □ (c❙?b∈B → Q b) =
   c❙?b∈(insert a B) → (if b = a ∧ a ∈ B then P ⊓ Q a else if b = a then P else Q b)›
  by (subst read_Det_read[where A = ‹{a}›, simplified]) (auto intro: mono_read_eq)

lemma read_Det_write :
  ‹inj_on c (insert b A) ⟹ (c❙?a∈A → P a) □ (c❙!b → Q) =
   c❙?a∈(insert b A) → (if a = b ∧ b ∈ A then P a ⊓ Q else if a = b then Q else P a)›
  by (subst read_Det_read[where B = ‹{b}›, simplified]) (auto intro: mono_read_eq)

lemma write0_Det_Mprefix :
  ‹(a → P) □ (□b∈B → Q b) =
   □b∈(insert a B) → (if b = a ∧ a ∈ B then P ⊓ Q a else if b = a then P else Q b)›
  by (subst write_Det_read[where c = id, unfolded write_is_write0, simplified]) simp

lemma Mprefix_Det_write0 :
  ‹(□a∈A → P a) □ (b → Q) =
   □a∈(insert b A) → (if a = b ∧ b ∈ A then P a ⊓ Q else if a = b then Q else P a)›
  by (subst read_Det_write[where c = id, unfolded write_is_write0, simplified]) simp


(* TODO: really useful ? and do we want versions for ndet_write and write/write0 ? *)



subsubsection ‹ @{const [source] ‹Sliding›} ›

lemma write0_Sliding_write0 :
  ‹(a → P) ⊳ (b → Q) =
   (□x ∈ {a, b} → (if a = b then P ⊓ Q else if x = a then P else Q)) ⊓
   (b → (if a = b then P ⊓ Q else Q))›
  by (auto simp add: Process_eq_spec write0_def
      Sliding_projs Ndet_projs Mprefix_projs)

lemma write_Sliding_write :
  ‹(c❙!a → P) ⊳ (d❙!b → Q) =
   (□x ∈ {c a, d b} → (if c a = d b then P ⊓ Q else if x = c a then P else Q)) ⊓
   (d❙!b → (if c a = d b then P ⊓ Q else Q))›
  by (simp add: write_is_write0 write0_Sliding_write0)

lemma write0_Sliding_write :
  ‹(a → P) ⊳ (d❙!b → Q) =
   (□x ∈ {a, d b} → (if a = d b then P ⊓ Q else if x = a then P else Q)) ⊓
   (d❙!b → (if a = d b then P ⊓ Q else Q))›
  by (simp add: write_is_write0 write0_Sliding_write0)

lemma write_Sliding_write0 :
  ‹(c❙!a → P) ⊳ (b → Q) =
   (□x ∈ {c a, b} → (if c a = b then P ⊓ Q else if x = c a then P else Q)) ⊓
   (b → (if c a = b then P ⊓ Q else Q))›
  by (simp add: write_is_write0 write0_Sliding_write0)



lemma read_Sliding_superset_read :
  ― ‹Not really interesting without the additional assumptions.›
  ‹A ⊆ B ⟹ inj_on c B ⟹
   (c❙?a∈A → P a) ⊳ (c❙?b∈B → Q b) = c❙?b∈B → (if b ∈ A then P b ⊓ Q b else Q b)›
  by (unfold read_def, subst Mprefix_Sliding_superset_Mprefix)
    (auto simp add: inj_on_eq_iff subset_iff intro!: mono_Mprefix_eq, metis inj_on_subset inv_into_f_f subset_eq)

lemma read_Sliding_same_set_read :
  ‹inj_on c A ⟹ (c❙?a∈A → P a) ⊳ (c❙?a∈A → Q a) = c❙?a∈A → P a ⊓ Q a›
  by (unfold read_def Mprefix_Sliding_same_set_Mprefix)
    (auto simp add: inj_on_eq_iff subset_iff intro: mono_Mprefix_eq)

lemma ndet_write_Sliding_superset_ndet_write :
  ‹A ⊆ B ⟹ inj_on c B ⟹
   (c❙!❙!a∈A → P a) ⊳ (c❙!❙!b∈B → Q b) = c❙!❙!b∈B → (if b ∈ A then P b ⊓ Q b else Q b)›
  by (unfold ndet_write_def, subst Mndetprefix_Sliding_superset_Mndetprefix)
    (auto simp add: inj_on_eq_iff subset_iff intro!: mono_Mndetprefix_eq, metis inj_on_subset inv_into_f_f subset_eq)

lemma ndet_write_Sliding_same_set_ndet_write :
  ‹inj_on c A ⟹ (c❙!❙!a∈A → P a) ⊳ (c❙!❙!a∈A → Q a) = c❙!❙!a∈A → P a ⊓ Q a›
  by (unfold ndet_write_def Mndetprefix_Sliding_same_set_Mndetprefix)
    (auto simp add: inj_on_eq_iff subset_iff intro: mono_Mndetprefix_eq)


lemma write_Sliding_superset_read :
  ‹a ∈ B ⟹ inj_on c B ⟹
   (c❙!a → P) ⊳ (c❙?b∈B → Q b) = c❙?b∈B → (if b = a then P ⊓ Q b else Q b)›
  by (subst read_Sliding_superset_read[where A = ‹{a}›, simplified]) simp_all

lemma write0_Sliding_superset_Mprefix :
  ‹a ∈ B ⟹ (a → P) ⊳ (□b∈B → Q b) = □b∈B → (if b = a then P ⊓ Q b else Q b)›
  by (subst read_Sliding_superset_read
      [where A = ‹{a}› and c = id, simplified, unfolded write_is_write0, simplified]) simp_all

lemma write_Sliding_superset_ndet_write :
  ‹a ∈ B ⟹ inj_on c B ⟹
   (c❙!a → P) ⊳ (c❙!❙!b∈B → Q b) = c❙!❙!b∈B → (if b = a then P ⊓ Q b else Q b)›
  by (subst ndet_write_Sliding_superset_ndet_write[where A = ‹{a}›, simplified]) simp_all

lemma write0_Sliding_superset_Mndetprefix :
  ‹a ∈ B ⟹ (a → P) ⊳ (⊓b∈B → Q b) = ⊓b∈B → (if b = a then P ⊓ Q b else Q b)›
  by (subst ndet_write_Sliding_superset_ndet_write
      [where A = ‹{a}› and c = id, simplified, unfolded write_is_write0, simplified]) simp_all



subsubsection ‹ @{const [source] ‹Seq›} ›

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

lemma write0_Seq : ‹a → P ❙; Q = a → (P ❙; Q)›
  by (simp add: write0_def Mprefix_Seq)

lemma ndet_write_Seq : ‹c❙!❙!a∈A → P a ❙; Q = c❙!❙!a∈A → (P a ❙; Q)›
  by (simp add: ndet_write_is_GlobalNdet_write0 Seq_distrib_GlobalNdet_right write0_Seq)

lemma write_Seq : ‹c❙!a → P ❙; Q = c❙!a → (P ❙; Q)›
  by (simp add: write0_Seq write_is_write0)



subsubsection ‹ \<^const>‹Renaming› ›

lemma Renaming_read :
  ‹Renaming (c❙?a∈A → P a) f g = (f ∘ c)❙?a∈A → Renaming (P a) f g›
  if ‹inj_on c A› and ‹inj_on f (c ` A)›
proof -
  have ‹f ` c ` A = (f ∘ c) ` A› by auto
  have ‹inj_on (f ∘ c) A› by (simp add: comp_inj_on ‹inj_on c A› ‹inj_on f (c ` A)›)
  have * : ‹y ∈ (λx. f (c x)) ` A ⟹ {x ∈ c ` A. y = f x} = {inv_into (c ` A) f y}› for y
    using ‹inj_on f (c ` A)› by auto
  show ‹Renaming (c❙?a∈A → P a) f g = (f ∘ c)❙?a∈A → Renaming (P a) f g›
  proof (unfold read_def Renaming_Mprefix ‹f ` c ` A = (f ∘ c) ` A›, rule mono_Mprefix_eq)
    from ‹inj_on (f ∘ c) A›
    show ‹a ∈ (f ∘ c) ` A ⟹
          ⊓a∈{x ∈ c ` A. a = f x}. Renaming ((P ∘ inv_into A c) a) f g =
          ((λa. Renaming (P a) f g) ∘ inv_into A (f ∘ c)) a› for a
      by (auto simp add: "*" inv_into_f_eq ‹inj_on c A› ‹inj_on f (c ` A)›
          intro: arg_cong[where f = ‹λa. Renaming (P a) f g›])
  qed
qed

lemma Renaming_write :
  ‹Renaming (c❙!a → P) f g = (f ∘ c)❙!a → Renaming P f g›
  by (fact Renaming_read[where A = ‹{a}›, simplified])

lemma Renaming_write0 :
  ‹Renaming (a → P) f g = f a → Renaming P f g›
  by (fact Renaming_write[where c = id, unfolded write_is_write0, simplified])

lemma Renaming_ndet_write :
  ‹Renaming (c❙!❙!a∈A → P a) f g = (f ∘ c)❙!❙!a∈A → Renaming (P a) f g›
  if ‹inj_on c A› and ‹inj_on f (c ` A)›
proof -
  have ‹inj_on (f ∘ c) A› by (simp add: comp_inj_on ‹inj_on c A› ‹inj_on f (c ` A)›)
  have ‹(λx. f (c x)) ` A = f ` (c ` A)› by auto
  show ‹Renaming (c❙!❙!a∈A → P a) f g = (f ∘ c)❙!❙!a∈A → Renaming (P a) f g›
    by (simp add: ‹?this› ndet_write_is_GlobalNdet_write0 Renaming_distrib_GlobalNdet Renaming_write0, rule sym)
      (use ‹inj_on (f ∘ c) A› ‹inj_on c A› in
        ‹auto simp add: inv_into_f_eq
                 intro: mono_GlobalNdet_eq2 arg_cong[where f = ‹λa. _ → Renaming (P a) f g›]›)
qed



subsubsection ‹ \<^const>‹Hiding› ›

lemma Hiding_read_disjoint :
  ‹c ` A ∩ S = {} ⟹ c❙?a∈A → P a \ S = c❙?a∈A → (P a \ S)›
  by (unfold read_def, subst Hiding_Mprefix_disjoint)
    (auto simp add: disjoint_iff image_iff intro: mono_Mprefix_eq)

lemma ‹A ⊆ B ⟹ a ∈ A ⟹ (inv_into A c) a = (inv_into B c) a›
  oops ― ‹Not provable, therefore we need the injectivity for the non disjoint case.›

lemma Hiding_read_non_disjoint :
  ‹c❙?a∈A → P a \ S = (c❙?a∈(A - c -` S) → (P a \ S)) ⊳ (⊓a∈(A ∩ c -` S). (P a \ S))›
  if ‹inj_on c A› and ‹c ` A ∩ S ≠ {}›
proof -
  have * : ‹(P ∘ inv_into A c) x = (P ∘ inv_into (A - c -` S) c) x›
    if ‹x ∈ c ` (A - c -` S)› for x
  proof -
    from ‹x ∈ c ` (A - c -` S)› obtain a where ‹a ∈ A - c -` S› ‹x = c a› by blast
    from ‹a ∈ A - c -` S› have ‹a ∈ A› by blast
    from ‹inj_on c A› inj_on_subset have ‹inj_on c (A - c -` S)› by force
    from ‹a ∈ A - c -` S› ‹x = c a› ‹inj_on c (A - c -` S)›
    have ‹(inv_into (A - c -` S) c) x = a› by simp
    moreover from ‹a ∈ A› ‹x = c a› ‹inj_on c A› have ‹(inv_into A c) x = a› by simp
    ultimately show ‹(P ∘ inv_into A c) x = (P ∘ inv_into (A - c -` S) c) x› by simp
  qed
  have ** : ‹c ` (A - c -` S) = c ` A - S› by blast
  have *** : ‹c ` A ∩ S = c ` (A ∩ (c -` S))› by blast
  have ‹(c❙?a∈A → P a) \ S = (c❙?a∈(A - c -` S) → (P a \ S)) ⊳
                             (⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S))›
  proof (unfold read_def comp_def, subst Hiding_Mprefix_non_disjoint,
      use ‹c ` A ∩ S ≠ {}› in blast, rule arg_cong[where f = ‹λP. P ⊳ _›])
    show ‹□a∈(c ` A - S) → (P (inv_into A c a) \ S) =
          □x∈c ` (A - c -` S) → (P (inv_into (A - c -` S) c x) \ S)›
      by (use "*" in ‹force simp add: "**" intro : mono_Mprefix_eq›)
  qed
  also have ‹(⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)) = ⊓a∈(A ∩ c -` S). (P a \ S)›
    by (subst "***", rule mono_GlobalNdet_eq2) (simp add: ‹inj_on c A›)
  finally show ‹(c❙?a∈A → P a) \ S =
                (c❙?a∈(A - c -` S) → (P a \ S)) ⊳ (⊓a∈(A ∩ c -` S). (P a \ S))› .
qed

lemma Hiding_read_subset :
  ‹c❙?a∈A → P a \ S = ⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)›
  if ‹inj_on c A› and ‹c ` A ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ c❙?a∈A → P a \ S = ⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)›
    by (auto simp add: Process_eq_spec GlobalNdet_projs F_Hiding_seqRun D_Hiding_seqRun read_def Mprefix_projs)
next
  assume ‹A ≠ {}›
  with ‹c ` A ⊆ S› have ‹c ` A ∩ S ≠ {}› ‹c ` A - S = {}› by auto
  show ‹c❙?a∈A → P a \ S = ⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)›
    by (simp add: read_def Hiding_Mprefix_non_disjoint[OF ‹c ` A ∩ S ≠ {}›] ‹c ` A - S = {}›
        Process_eq_spec Sliding_projs GlobalNdet_projs Mprefix_projs)
qed



lemma Hiding_ndet_write_disjoint :
  ‹c ` A ∩ S = {} ⟹ (c❙!❙!a∈A → P a) \ S = (c❙!❙!a∈A → (P a \ S))›
  by (unfold ndet_write_def, subst Hiding_Mndetprefix_disjoint)
    (auto simp add: disjoint_iff image_iff intro: mono_Mndetprefix_eq)

lemma Hiding_ndet_write_subset :
  ‹c ` A ⊆ S ⟹ (c❙!❙!a∈A → P a) \ S = ⊓a∈c ` A. (P (inv_into A c a) \ S)›
  by (unfold ndet_write_def, subst Hiding_Mndetprefix_subset)
    (auto simp add: disjoint_iff image_iff intro: mono_GlobalNdet_eq)

lemma Hiding_ndet_write_subset_bis :
  ― ‹With the injectivity...›
  ‹inj_on c A ⟹ c ` A ⊆ S ⟹ (c❙!❙!a∈A → P a) \ S = ⊓a∈A. (P a \ S)›
  by (simp add: Hiding_ndet_write_subset mono_GlobalNdet_eq2)

lemma ‹A ⊆ B ⟹ a ∈ A ⟹ (inv_into A c) a = (inv_into B c) a›
  oops ― ‹Not provable, therefore we need the injectivity for the non disjoint case.›

lemma Hiding_ndet_write_non_disjoint_not_subset :
  ‹(c❙!❙!a∈A → P a) \ S =
   (c❙!❙!a∈(A - c -` S) → (P a \ S)) ⊓ (⊓a∈(A ∩ c -` S). (P a \ S))›
  if ‹inj_on c A› and ‹c ` A ∩ S ≠ {}› and ‹¬ c ` A ⊆ S›
proof -
  have * : ‹(P ∘ inv_into A c) x = (P ∘ inv_into (A - c -` S) c) x›
    if ‹x ∈ c ` (A - c -` S)› for x
  proof -
    from ‹x ∈ c ` (A - c -` S)› obtain a where ‹a ∈ A - c -` S› ‹x = c a› by blast
    from ‹a ∈ A - c -` S› have ‹a ∈ A› by blast
    from ‹inj_on c A› inj_on_subset have ‹inj_on c (A - c -` S)› by force
    from ‹a ∈ A - c -` S› ‹x = c a› ‹inj_on c (A - c -` S)›
    have ‹(inv_into (A - c -` S) c) x = a› by simp
    moreover from ‹a ∈ A› ‹x = c a› ‹inj_on c A› have ‹(inv_into A c) x = a› by simp
    ultimately show ‹(P ∘ inv_into A c) x = (P ∘ inv_into (A - c -` S) c) x› by simp
  qed
  have ** : ‹c ` (A - c -` S) = c ` A - S› by blast
  have *** : ‹c ` A ∩ S = c ` (A ∩ c -` S)› by blast
  have ‹(c❙!❙!a∈A → P a) \ S = (c❙!❙!a∈(A - c -` S) → (P a \ S)) ⊓
                              (⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S))›
  proof (unfold ndet_write_def comp_def
      Hiding_Mndetprefix_non_disjoint_not_subset
      [OF ‹c ` A ∩ S ≠ {}› ‹¬ c ` A ⊆ S›])
    show ‹(⊓a∈(c ` A - S) → (P (inv_into A c a) \ S)) ⊓
          (⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)) =
          (⊓x∈c ` (A - c -` S) → (P (inv_into (A - c -` S) c x) \ S)) ⊓
          (⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S))›
      by (rule arg_cong[where f = ‹λP. P ⊓ _›])
        (use "*" in ‹force simp add: "**" intro : mono_Mndetprefix_eq›)
  qed
  also have ‹(⊓a∈(c ` A ∩ S). (P (inv_into A c a) \ S)) = ⊓a∈(A ∩ c -` S). (P a \ S)›
    by (auto simp add: "***" ‹inj_on c A› intro: mono_GlobalNdet_eq2)
  finally show ‹c❙!❙!a∈A → P a \ S =
                (c❙!❙!a∈(A - c -` S) → (P a \ S)) ⊓ (⊓a∈(A ∩ c -` S). (P a \ S))› .
qed



lemma Hiding_write0_disjoint :
  ‹a ∉ S ⟹ a → P \ S = a → (P \ S)›
  by (simp add: write0_def Hiding_Mprefix_disjoint)

lemma Hiding_write0_non_disjoint :
  ‹a ∈ S ⟹ a → P \ S = P \ S›
  by (simp add: write0_def Hiding_Mprefix_non_disjoint)

lemma Hiding_write_disjoint :
  ‹c a ∉ S ⟹ c❙!a → P \ S = c❙!a → (P \ S)›
  by (simp add: Hiding_write0_disjoint write_is_write0)

lemma Hiding_write_subset :
  ‹c a ∈ S ⟹ c❙!a → P \ S = P \ S›
  by (simp add: Hiding_write0_non_disjoint write_is_write0)





subsubsection ‹ \<^const>‹Sync› ›

paragraph ‹ \<^const>‹read› ›

lemma read_Sync_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_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_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_read) auto
  ultimately show ‹?lhs = ?rhs1 □ ?rhs2 □ ?rhs3› by argo
qed


lemma read_Sync_read_forced_read_right:
  ‹⟦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⟧ ⟹
   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))›
  by (subst Sync_commute, subst Det_commute, subst read_Sync_read_forced_read_left)
    (blast, blast, metis, auto simp add: Sync_commute intro: arg_cong2[where f = ‹(□)›])


paragraph ‹Special Cases›

lemma read_Sync_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_read)
      (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync_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_read_forced_read_left)
      (use that(3, 4, 5) in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync_read_subset_forced_read_right : 
  ‹⟦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⟧ ⟹
   c❙?a∈A → P a ⟦S⟧ d❙?b∈B → Q b = d❙?x∈(B ∩ d -` c ` A) → (P x ⟦S⟧ Q x)›
  by (subst Sync_commute, subst read_Sync_read_subset_forced_read_left)
    (simp_all add: Sync_commute, metis)


lemma read_Sync_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_read) (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync_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_read)
      (use that in ‹simp_all add: "*" "**"›)
qed

lemma read_Sync_read_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 (subst Sync_commute, subst read_Sync_read_left)
    (simp_all add: Sync_commute)


corollary read_Par_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_read_subset)

corollary read_Par_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_read_forced_read_left) simp_all

corollary read_Par_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_read_forced_read_right) simp_all


corollary read_Inter_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_read)



paragraph ‹Same channel›

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


lemma read_Sync_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_read_forced_read_left that "*")
qed

lemma read_Sync_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_read_forced_read_same_chan)
    (simp_all add: inj_on_Un, metis Un_iff inj_onD inj_on_Un)


lemma read_Sync_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_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_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_Mprefix
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])

lemma read_Sync_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_Mndetprefix
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])


lemma ndet_write_Sync_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_Mprefix_subset)

lemma read_Sync_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_Mndetprefix_subset)


― ‹If we have the same injective channel, it's better.›
lemma ndet_write_Sync_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_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

lemma read_Sync_ndet_write_subset_same_chan:
  ‹c ` A ⊆ S ⟹ c ` B ⊆ S ⟹ inj_on c (A ∪ B) ⟹
   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)›
  by (subst (1 2 3) Sync_commute)
    (simp add: Int_commute Un_commute ndet_write_Sync_read_subset_same_chan)


lemma ndet_write_Sync_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_Mprefix_indep comp_def
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])

lemma read_Sync_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_Mndetprefix_indep comp_def
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])


lemma ndet_write_Sync_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 c❙!❙!a∈A → (P a ⟦S⟧ d❙?b∈B → Q b))›
    by (auto simp add: ndet_write_def read_def Mndetprefix_Sync_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_Mprefix that(2))
  finally show ‹?lhs = ?rhs› .
qed

lemma read_Sync_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_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_Mprefix_left that(1) in force)
  finally show ‹?lhs = ?rhs› .
qed


lemma ndet_write_Sync_read_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 (subst (1 2) Sync_commute) (simp add: read_Sync_ndet_write_left)

lemma read_Sync_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 (subst (1 2) Sync_commute) (simp add: ndet_write_Sync_read_left)



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

lemma write_Sync_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_read[where A = ‹{a}›, simplified])
    (simp add: write_is_write0 image_iff)

lemma read_Sync_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_ndet_write[where B = ‹{b}›, simplified])
    (simp add: write_is_write0 image_iff)


lemma write_Sync_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_read)
    (metis Det_STOP Det_commute Diff_eq_empty_iff Mprefix_empty)

lemma read_Sync_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 (metis Sync_commute write_Sync_read_subset)


― ‹If we have the same injective channel, it's better.›
lemma write_Sync_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_read_subset_same_chan[where A = ‹{a}›, simplified]) simp_all

lemma read_Sync_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 (metis Sync_commute write_Sync_read_subset_same_chan)


lemma write_Sync_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_read_indep[where A = ‹{a}›, simplified])
    (simp_all add: write_is_write0)

lemma read_Sync_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_ndet_write_indep[where B = ‹{b}›, simplified])
    (simp_all add: write_is_write0)


lemma write_Sync_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_read_left[where A = ‹{a}›, simplified]) simp_all

lemma read_Sync_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_ndet_write_left[where B = ‹{b}›, simplified]) simp_all


lemma write_Sync_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 (1 2) Sync_commute) (simp add: read_Sync_write_left)

lemma read_Sync_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 (1 2) Sync_commute) (simp add: write_Sync_read_left)



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

lemma ndet_write_Sync_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))›
  (is ‹?lhs = (  if A = {} then if d ` B ∩ S = {} then ?mv_right else ?mv_right' ⊓ STOP
               else   if B = {} then if c ` A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP
                    else ?huge_mess)›)
proof (split if_split, intro conjI impI)
  have ‹d ` (B - d -` S) = d ` B - S› by blast
  thus ‹A = {} ⟹ ?lhs = (if d ` B ∩ S = {} then ?mv_right else ?mv_right' ⊓ STOP)›
    by (auto simp add: ndet_write_def STOP_Sync_Mndetprefix comp_def
        intro: mono_Mndetprefix_eq)
next
  show ‹?lhs = (if B = {} then if c ` A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP else ?huge_mess)› if ‹A ≠ {}›
  proof (split if_split, intro conjI impI)
    have ‹c ` (A - c -` S) = c ` A - S› by blast
    thus ‹B = {} ⟹ ?lhs = (if c ` A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP)›
      by (auto simp add: ndet_write_def Mndetprefix_Sync_STOP comp_def
          intro: mono_Mndetprefix_eq)
  next
    assume ‹B ≠ {}›
    have ‹?lhs = (⊓b∈d ` B. ⊓a∈c ` A. (a → P (inv_into A c a) ⟦S⟧ (b → Q (inv_into B d b))))›
      by (simp add: ndet_write_def Mndetprefix_GlobalNdet ‹A ≠ {}› ‹B ≠ {}›
          Sync_distrib_GlobalNdet_left Sync_distrib_GlobalNdet_right)
    also have ‹… = ?huge_mess›
      by (auto simp add: write0_def Mprefix_Sync_Mprefix Diff_triv Mprefix_is_STOP_iff disjoint_iff
          intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])
    finally show ‹?lhs = ?huge_mess› .
  qed
qed


lemma ndet_write_Sync_ndet_write_subset :
  ‹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)›
  (is ‹?lhs = (if ?cond then ?rhs1 else ?rhs2)›) if ‹c ` A ⊆ S› ‹d ` B ⊆ S›
proof (split if_split, intro conjI impI)
  show ‹?cond ⟹ ?lhs = ?rhs1›
    by (elim exE, simp add: ndet_write_is_GlobalNdet_write0 write0_def)
      (subst Mprefix_Sync_Mprefix_subset, use ‹c ` A ⊆ S› in simp_all)
next
  assume ‹¬ ?cond›
  let ?term = ‹λa b. (b → (P (inv_into A c a) ⟦S⟧ Q (inv_into B d b)))›
  have ‹?lhs = ⊓b∈d ` B. ⊓a∈c ` A. (if a = b then ?term a b else STOP)›
    (is ‹?lhs = ⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a›)
  proof (cases ‹A = {} ∨ B = {}›)
    from ‹c ` A ⊆ S› ‹d ` B ⊆ S› show ‹A = {} ∨ B = {} ⟹ ?lhs = (⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a)›
      by (elim disjE) (simp_all add: ndet_write_def Mndetprefix_Sync_STOP STOP_Sync_Mndetprefix
          Int_absorb2 Mndetprefix_is_STOP_iff Ndet_is_STOP_iff)
  next
    show ‹¬ (A = {} ∨ B = {}) ⟹ ?lhs = (⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a)›
      by (simp add: ndet_write_Sync_ndet_write)
        (intro mono_GlobalNdet_eq, use ‹c ` A ⊆ S› ‹d ` B ⊆ S› in auto)
  qed

  also have ‹(⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a) = ?rhs2›
  proof (cases ‹d ` B ∩ c ` A = {}›)
    assume ‹d ` B ∩ c ` A = {}›
    hence ‹c ` A ∩ d ` B = {}› by blast
    hence ‹(⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a) = STOP› by (auto simp add: GlobalNdet_is_STOP_iff)
    thus ‹(⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a) = ?rhs2›
      by (auto simp add: ‹c ` A ∩ d ` B = {}›)
  next
    show ‹(⊓b∈d ` B. ⊓a∈c ` A. ?rhs' b a) = ?rhs2› if ‹d ` B ∩ c ` A ≠ {}›
    proof (cases ‹d ` B - c ` A = {}›)
      assume ‹d ` B - c ` A = {}›
      hence ‹c ` A ∩ d ` B = d ` B› by blast
      have ‹(⊓a∈c ` A. ?rhs' b a) = (if c ` A = {b} then ?term b b else ?term b b ⊓ STOP)›
        (is ‹(⊓a∈c ` A. ?rhs' b a) = ?rhs'' b›) if ‹b ∈ d ` B› for b
      proof (cases ‹c ` A ∩ {b} = {}›)
        from ‹d ` B - c ` A = {}› ‹b ∈ d ` B›
        show ‹c ` A ∩ {b} = {} ⟹ (⊓a∈c ` A. ?rhs' b a) = ?rhs'' b› by auto
      next
        show ‹(⊓a∈c ` A. ?rhs' b a) = ?rhs'' b› if ‹c ` A ∩ {b} ≠ {}›
        proof (cases ‹c ` A - {b} = {}›)
          show ‹c ` A - {b} = {} ⟹ (⊓a∈c ` A. ?rhs' b a) = ?rhs'' b›
            using ‹c ` A ∩ {b} ≠ {}› by auto
        next
          show ‹(⊓a∈c ` A. ?rhs' b a) = ?rhs'' b› if ‹c ` A - {b} ≠ {}›
            using ‹c ` A - {b} ≠ {}› ‹c ` A ∩ {b} ≠ {}›
            by (auto simp add: GlobalNdet_is_STOP_iff
                simp flip: GlobalNdet_factorization_union
                [OF ‹c ` A ∩ {b} ≠ {}› ‹c ` A - {b} ≠ {}›, unfolded Int_Diff_Un]
                intro: arg_cong2[where f = ‹(⊓)›])
        qed
      qed
      hence ‹(⊓b ∈ d ` B. ⊓a∈c ` A. ?rhs' b a) = ⊓b ∈ d ` B. ?rhs'' b›
        by (fact mono_GlobalNdet_eq)
      also have ‹(⊓b ∈ d ` B. ?rhs'' b) = ?rhs2›
      proof -
        from ‹¬ ?cond› have ‹(⊓b ∈ d ` B. ?rhs'' b) = ⊓b ∈ d ` B. ?term b b ⊓ STOP›
          by (metis Diff_eq_empty_iff Int_commute ‹c ` A ∩ d ` B = d ` B›
              ‹d ` B - c ` A = {}› subset_singleton_iff ‹d ` B ∩ c ` A ≠ {}›)
        also have ‹… = (⊓b ∈ d ` B. ?term b b) ⊓ STOP›
          by (simp add: Process_eq_spec Ndet_projs GlobalNdet_projs STOP_projs)
        finally show ‹(⊓b ∈ d ` B. ?rhs'' b) = ?rhs2›
          by (simp add: Mndetprefix_GlobalNdet ‹c ` A ∩ d ` B = d ` B›)
      qed
      finally show ‹(⊓b ∈ d ` B. ⊓a∈c ` A. ?rhs' b a) = ?rhs2› .
    next
      assume ‹d ` B - c ` A ≠ {}›
      have ‹⊓a∈c ` A. (if a = b then ?term a b else STOP) =
            (if b ∈ c ` A then if c ` A = {b} then ?term b b else (?term b b) ⊓ STOP else STOP)›
        if ‹b ∈ d ` B› for b
      proof (split if_split, intro conjI impI)
        show ‹⊓a∈c ` A. (if a = b then ?term a b else STOP) =
              (if c ` A = {b} then ?term b b else (?term b b) ⊓ STOP)› if ‹b ∈ c ` A›
        proof (split if_split, intro conjI impI)
          show ‹c ` A = {b} ⟹ ⊓a∈c ` A. (if a = b then ?term a b else STOP) = ?term b b› by simp
        next
          assume ‹c ` A ≠ {b}›
          with ‹b ∈ c ` A› have ‹insert b (c ` A) = c ` A› ‹c ` A - {b} ≠ {}› by auto
          show ‹c ` A ≠ {b} ⟹ ⊓a∈c ` A. (if a = b then ?term a b else STOP) = ?term b b ⊓ STOP›
            by (auto simp add: GlobalNdet_is_STOP_iff intro!: arg_cong2[where f = ‹(⊓)›]
                simp flip: GlobalNdet_factorization_union
                [of ‹{b}›, OF _ ‹c ` A - {b} ≠ {}›, simplified, unfolded ‹insert b (c ` A) = c ` A›])
        qed
      next
        show ‹b ∉ c ` A ⟹ ⊓a∈c ` A. (if a = b then ?term a b else STOP) = STOP›
          by (auto simp add: GlobalNdet_is_STOP_iff)
      qed

      hence ‹⊓b ∈ d ` B. ⊓a∈c ` A. ?rhs' b a =
             ⊓b ∈ d ` B. (if b ∈ c ` A then if c ` A = {b} then ?term b b else (?term b b) ⊓ STOP else STOP)›
        by (fact mono_GlobalNdet_eq)
      also from ‹d ` B - c ` A ≠ {}› have ‹… = (⊓b ∈ d ` B. (if b ∈ c ` A then ?term b b else STOP)) ⊓ STOP›
        by (simp add: Process_eq_spec GlobalNdet_projs, safe)
          (simp_all add: GlobalNdet_projs STOP_projs Ndet_projs split: if_split_asm, auto)
      also have ‹… = ?rhs2›
      proof (fold GlobalNdet_factorization_union
          [OF ‹d ` B ∩ c ` A ≠ {}› ‹d ` B - c ` A ≠ {}›, unfolded Int_Diff_Un])
        have ‹⊓b∈(d ` B ∩ c ` A). (if b ∈ c ` A then ?term b b else STOP) =
              ⊓b∈(d ` B ∩ c ` A). ?term b b› by (auto intro: mono_GlobalNdet_eq)
        moreover have ‹⊓b∈(d ` B - c ` A). (if b ∈ c ` A then ?term b b else STOP) = STOP›
          by (simp add: GlobalNdet_is_STOP_iff)
        ultimately show ‹(⊓b∈(d ` B ∩ c ` A). (if b ∈ c ` A then ?term b b else STOP)) ⊓
                         (⊓b∈(d ` B - c ` A). (if b ∈ c ` A then ?term b b else STOP)) ⊓ STOP = ?rhs2›
          by (metis Mndetprefix_GlobalNdet Int_commute Ndet_assoc Ndet_id)
      qed
      finally show ‹(⊓b ∈ d ` B. ⊓a∈c ` A. ?rhs' b a) = ?rhs2› .
    qed
  qed
  finally show ‹?lhs = ?rhs2› .
qed


lemma ndet_write_Sync_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_ndet_write disjoint_iff intro!: mono_GlobalNdet_eq)


lemma ndet_write_Sync_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 -
  let ?rhs' = ‹⊓b∈d ` B. ⊓a∈c ` A. a → (P (inv_into A c a) ⟦S⟧ b → Q (inv_into B d b))›
  have ‹?lhs = (  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))›
    (is ‹?lhs = (if A = {} then ?rhs1 else if B = {} then ?rhs2 else ?rhs3)›)
    by (fact ndet_write_Sync_ndet_write)
  also from ‹d ` B ⊆ S› have ‹?rhs1 = STOP›
    by (auto simp add: Ndet_is_STOP_iff ndet_write_def Mndetprefix_GlobalNdet GlobalNdet_is_STOP_iff)
  also from ‹c ` A ∩ S = {}› have ‹?rhs2 = c❙!❙!a∈A → (P a ⟦S⟧ STOP)› by presburger
  also from ‹c ` A ∩ S = {}› ‹d ` B ⊆ S›
  have ‹?rhs3 = ⊓b∈d ` B. ⊓a∈c ` A. a → (P (inv_into A c a) ⟦S⟧ b → Q (inv_into B d b))›
    by (intro mono_GlobalNdet_eq) auto
  finally have ‹?lhs = (  if A = {} then STOP
                        else   if B = {} then c❙!❙!a∈A → (P a ⟦S⟧ STOP)
                             else ?rhs')› .
  moreover have ‹B ≠ {} ⟹ ?rhs' = ⊓a∈c ` A. a → (P (inv_into A c a) ⟦S⟧ ⊓b∈d ` B. b → Q (inv_into B d b))›
    by (subst GlobalNdet_sets_commute)
      (simp add: Sync_distrib_GlobalNdet_left write0_GlobalNdet)
  moreover have ‹… = c❙!❙!a∈A → (P a ⟦S⟧ d❙!❙!b∈B → Q b)›
    by (simp add: ndet_write_is_GlobalNdet_write0)
  ultimately show ‹?lhs = ?rhs› by simp
qed


lemma ndet_write_Sync_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 (subst (1 2) Sync_commute) (simp add: ndet_write_Sync_ndet_write_left)


text ‹Note that \<^const>‹Mndetprefix› versions can be recovered
      as corollaries through @{thm [source] ndet_write_id}.›



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

lemma write_Sync_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_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_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 (1 2 3 4 5) Sync_commute)
    (auto simp add: write_Sync_ndet_write intro: mono_GlobalNdet_eq)


lemma write_Sync_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_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

lemma ndet_write_Sync_write_subset :
  ‹c ` A ⊆ S ⟹ d b ∈ S ⟹
   (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)›
  by (subst (1 2 3) Sync_commute) (simp add: write_Sync_ndet_write_subset)


lemma write_Sync_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_ndet_write_indep[where A = ‹{a}›, simplified])
    (auto simp add: write_is_write0 intro: mono_GlobalNdet_eq)

lemma ndet_write_Sync_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 (1 2 3 4) Sync_commute, subst Det_commute)
    (simp add: write_Sync_ndet_write_indep)


lemma write_Sync_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_ndet_write_left[where A = ‹{a}›, simplified]) simp_all

lemma ndet_write_Sync_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_ndet_write_left[where B = ‹{b}›, simplified]) simp_all


lemma write_Sync_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_ndet_write_right[where A = ‹{a}›, simplified]) simp_all

lemma ndet_write_Sync_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_ndet_write_right[where B = ‹{b}›, simplified]) simp_all



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

lemma write_Sync_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_read[where A = ‹{a}› and B = ‹{b}›, simplified])
    (simp add: write_def insert_Diff_if Det_commute Int_insert_right)

lemma write_Inter_write :
  ‹c❙!a → P ||| d❙!b → Q = (c❙!a → (P ||| d❙!b → Q)) □ (d❙!b → (c❙!a → P ||| Q))›
  by (simp add: write_Sync_write Det_commute)

lemma write_Par_write :
  ‹c❙!a → P || d❙!b → Q = (if c a = d b then c❙!a → (P || Q) else STOP)›
  by (simp add: write_Sync_write)


lemma write_Sync_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_write)

lemma write_Sync_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_write)


lemma write_Sync_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_write)


lemma write_Sync_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_write)




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

lemma write0_Sync_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_read[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_read_subset[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write_subset[where d = ‹λx. x›, unfolded write_is_write0])

lemma write0_Sync_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_read_subset_same_chan
      [where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write_subset_same_chan
      [where c = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_read_indep[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write_indep[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_read_left[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write_left[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_read_right[where c = id, unfolded write_is_write0, simplified])

lemma read_Sync_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_write_right[where d = id, unfolded write_is_write0, simplified])



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

lemma write0_Sync_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_ndet_write[where c = ‹λx. x›, unfolded write_is_write0, simplified])

lemma ndet_write_Sync_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_write[where d = ‹λx. x›, unfolded write_is_write0, simplified])

lemma write0_Sync_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_ndet_write_subset[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync_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_write_subset[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_ndet_write_indep[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync_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_write_indep[where d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_ndet_write_left[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync_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_write_left[where d = id, unfolded write_is_write0, simplified])

lemma write_Sync_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_ndet_write_right[where c = id, unfolded write_is_write0, simplified])

lemma ndet_write_Sync_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_write_right[where d = id, unfolded write_is_write0, simplified])



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

lemma write0_Sync_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_write[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_write0 Det_commute)

lemma write0_Inter_write0 :
  ‹a → P ||| b → Q = (a → (P ||| b → Q)) □ (b → (a → P ||| Q))›
  by (simp add: write0_Sync_write0 Det_commute)

lemma write0_Par_write0 :
  ‹a → P || b → Q = (if a = b then a → (P || Q) else STOP)›
  by (simp add: write0_Sync_write0)



lemma write0_Sync_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_write_subset[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_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_write_indep[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_write0_left :
  ‹a ∉ S ⟹ b ∈ S ⟹ a → P ⟦S⟧ b → Q = a → (P ⟦S⟧ b → Q)›
  by (simp add: write_Sync_write_left[where c = id and d = id, unfolded write_is_write0, simplified])

lemma write0_Sync_write0_right :
  ‹a ∈ S ⟹ b ∉ S ⟹ a → P ⟦S⟧ b → Q = b → (a → P ⟦S⟧ Q)›
  by (simp add: write_Sync_write_right[where c = id and d = id, unfolded write_is_write0, simplified]) 


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

lemma write0_Sync_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_write0 write_is_write0)

lemma write_Sync_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_write0 write_is_write0)


lemma write0_Sync_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_write)

lemma write_Sync_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_write0)


lemma write0_Sync_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_write)

lemma write_Sync_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_write0)


lemma write0_Sync_write_left :
  ‹a ∉ S ⟹ d b ∈ S ⟹ a → P ⟦S⟧ d❙!b → Q = a → (P ⟦S⟧ d❙!b → Q)›
  by (simp add: write0_Sync_write0_left write_is_write0)

lemma write_Sync_write0_left :
  ‹c a ∉ S ⟹ b ∈ S ⟹ c❙!a → P ⟦S⟧ b → Q = c❙!a → (P ⟦S⟧ b → Q)›
  by (simp add: write0_Sync_write0_left write_is_write0)


lemma write0_Sync_write_right :
  ‹a ∈ S ⟹ d b ∉ S ⟹ a → P ⟦S⟧ d❙!b → Q = d❙!b → (a → P ⟦S⟧ Q)›
  by (simp add: write0_Sync_write0_right write_is_write0)

lemma write_Sync_write0_right :
  ‹c a ∈ S ⟹ b ∉ S ⟹ c❙!a → P ⟦S⟧ b → Q = b → (c❙!a → P ⟦S⟧ Q)›
  by (simp add: Sync_commute write0_Sync_write_left)



subsection ‹\<^const>‹Sync›, \<^const>‹SKIP› and \<^const>‹STOP››

subsubsection ‹\<^const>‹SKIP››

text ‹Without injectivity, the result is a trivial corollary of
      @{thm read_def} and @{thm Mprefix_Sync_SKIP}.›

lemma read_Sync_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_SKIP ‹?this› inj_on_diff ‹inj_on c A›
        intro: mono_Mprefix_eq)
qed

lemma SKIP_Sync_read :
  ‹inj_on d B ⟹ SKIP r ⟦S⟧ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (SKIP r ⟦S⟧ Q b)›
  by (subst (1 2) Sync_commute) (simp add: read_Sync_SKIP)


corollary write_Sync_SKIP :
  ‹c❙!a → P ⟦S⟧ SKIP r = (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧ SKIP r))›
  and SKIP_Sync_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_SKIP SKIP_Sync_Mprefix Diff_triv)

corollary write0_Sync_SKIP :
  ‹a → P ⟦S⟧ SKIP r = (if a ∈ S then STOP else a → (P ⟦S⟧ SKIP r))›
  and SKIP_Sync_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_SKIP SKIP_Sync_Mprefix Diff_triv)


lemma ndet_write_Sync_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 c ` A ∩ S = {} 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_distrib_GlobalNdet_right write0_Sync_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_distrib_GlobalNdet_right write0_Sync_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_distrib_GlobalNdet_right)
        (auto simp add: GlobalNdet_is_STOP_iff write0_Sync_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 SKIP_Sync_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_commute) (simp add: ndet_write_Sync_SKIP)


subsubsection ‹\<^const>‹STOP››

text ‹Without injectivity, the result is a trivial corollary of
      @{thm read_def} and @{thm Mprefix_Sync_SKIP}.›

lemma read_Sync_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_STOP inj_on_diff ‹inj_on c A›
        intro: mono_Mprefix_eq)
qed

lemma STOP_Sync_read :
  ‹inj_on d B ⟹ STOP ⟦S⟧ d❙?b∈B → Q b = d❙?b∈(B - d -` S) → (STOP ⟦S⟧ Q b)›
  by (subst (1 2) Sync_commute) (simp add: read_Sync_STOP)


corollary write_Sync_STOP :
  ‹c❙!a → P ⟦S⟧ STOP = (if c a ∈ S then STOP else c❙!a → (P ⟦S⟧ STOP))›
  and STOP_Sync_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_STOP STOP_Sync_Mprefix Diff_triv)

corollary write0_Sync_STOP :
  ‹a → P ⟦S⟧ STOP = (if a ∈ S then STOP else a → (P ⟦S⟧ STOP))›
  and STOP_Sync_write0 :
  ‹STOP ⟦S⟧ b → Q = (if b ∈ S then STOP else b → (STOP ⟦S⟧ Q))›
  by (simp_all add: write0_def Mprefix_Sync_STOP STOP_Sync_Mprefix Diff_triv)


lemma ndet_write_Sync_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 c ` A ∩ S = {} 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_distrib_GlobalNdet_right write0_Sync_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_distrib_GlobalNdet_right write0_Sync_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_distrib_GlobalNdet_right)
        (auto simp add: GlobalNdet_is_STOP_iff write0_Sync_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 STOP_Sync_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_commute) (simp add: ndet_write_Sync_STOP)




(*<*)
end
  (*>*)