Theory Step_CSP_PTick_Laws_Extended

(***********************************************************************************
 * 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 Step_CSP_PTick_Laws_Extended
  imports Basic_CSP_PTick_Laws Step_CSP_PTick_Laws
    Non_Deterministic_CSP_PTick_Distributivity
begin
  (*>*)

unbundle option_type_syntax


section ‹Extended step Laws›

subsection ‹Sequential Composition›

lemma Mndetprefix_Seqptick: ‹⊓a ∈ A → P a ;✓ Q = ⊓a ∈ A → (P a ;✓ Q)›
  by (auto simp add: Mndetprefix_GlobalNdet Seqptick_distrib_GlobalNdet_right
      write0_def Mprefix_Seqptick intro: mono_GlobalNdet_eq)


subsection ‹Synchronization Product›

subsubsection ‹Behaviour of const‹SKIPS››

lemma (in Syncptick_locale) SKIPS_Syncptick_SKIPS :
  ‹SKIPS R ⟦A⟧✓ SKIPS S = ⊓(r, s) ∈ R × S. (case r ⊗✓ s of ⌊r_s⌋ ⇒ SKIP r_s | ◇ ⇒ STOP)›
  by (simp add: SKIPS_def Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right)
    (simp add: GlobalNdet_cartprod[of R S ‹λr s. case r ⊗✓ s of ◇ ⇒ STOP | ⌊r_s⌋ ⇒ SKIP r_s›]
      GlobalNdet_sets_commute[of R S ‹λr s. case r ⊗✓ s of ◇ ⇒ STOP | ⌊r_s⌋ ⇒ SKIP r_s›])


text ‹In order for the right-hand side to be rewritten as a SKIPS, an assumption is required:
      the ticks involved must be able to be combined.›

lemma GlobalNdet_prod_SKIP_is_SKIPS :
  ‹⊓(r, s) ∈ R × S. SKIP ⌈tick_join r s⌉ =
   SKIPS ((the ∘ (λ(r, s). tick_join r s)) ` (R × S))›
  by (simp add: SKIPS_def mono_GlobalNdet_eq2 split_def)


lemma GlobalNdet_prod_case_SKIP_STOP_is_GlobalNdet_prod_SKIP_iff :
  ‹⊓(r, s) ∈ R × S. (case tick_join r s of ◇ ⇒ STOP | ⌊r_s⌋ ⇒ SKIP r_s) =
   ⊓(r, s) ∈ R × S. SKIP ⌈tick_join r s⌉
   ⟷ (∀r s. r ∈ R ⟶ s ∈ S ⟶ tick_join r s ≠ ◇)›
  (is ‹?lhs1 = ?lhs2 ⟷ ?rhs›)
proof (rule iffI)
  show ‹?rhs ⟹ ?lhs1 = ?lhs2›
    by (force intro: mono_GlobalNdet_eq)
next
  have ‹UNIV ∈ ℛ ?lhs2 ⟷ R = {} ∨ S = {}›
    by (simp add: Refusals_iff F_GlobalNdet F_SKIP)
  moreover have ‹UNIV ∈ ℛ ?lhs1 ⟷ R = {} ∨ S = {} ∨ (∃r s. r ∈ R ∧ s ∈ S ∧ tick_join r s = ◇)›
    by (auto simp add: Refusals_iff F_GlobalNdet F_SKIP F_STOP split: option.split)
  ultimately show ‹?lhs1 = ?lhs2 ⟹ ?rhs› by (metis empty_iff)
qed

lemma (in Syncptick_locale) SKIPS_Syncptick_SKIPS_bis :
  ‹SKIPS R ⟦A⟧✓ SKIPS S = SKIPS ((the ∘ (λ(r, s). r ⊗✓ s)) ` (R × S))›
  if ‹⋀r s. r ∈ R ⟹ s ∈ S ⟹ r ⊗✓ s ≠ ◇›
  by (unfold SKIPS_Syncptick_SKIPS, fold GlobalNdet_prod_SKIP_is_SKIPS)
    (simp add: SKIPS_Syncptick_SKIPS GlobalNdet_prod_case_SKIP_STOP_is_GlobalNdet_prod_SKIP_iff that)


lemma (in Syncptick_locale)
  SKIPS_Syncptick_STOP [simp] : ‹SKIPS R ⟦A⟧✓ STOP = STOP›
  and STOP_Syncptick_SKIPS [simp] : ‹STOP ⟦A⟧✓ SKIPS S = STOP›
  by (fact SKIPS_Syncptick_SKIPS[where S = ‹{}›, simplified]
      SKIPS_Syncptick_SKIPS[where R = ‹{}›, simplified])+




subsubsection ‹Derived step Laws with Non-Determinism›

context Syncptick_locale begin

lemma Mprefix_Interptick_Mprefix :
  ‹□a∈A → P a |||✓ □b∈B → Q b =
   (□a∈A → (P a |||✓ □b∈B → Q b)) □ (□b∈B → (□a ∈ A → P a |||✓ Q b))›
  by (fact Mprefix_Syncptick_Mprefix[where S = ‹{}›, simplified])

lemma Mprefix_Parptick_Mprefix : ‹□a∈A → P a ||✓ □b∈B → Q b = □x∈(A ∩ B) → (P x ||✓ Q x)›
  by (fact Mprefix_Syncptick_Mprefix[where S = ‹UNIV›, simplified])

lemma Mprefix_Syncptick_Mprefix_subset :
  ‹⟦A ⊆ S; B ⊆ S⟧ ⟹ □a∈A → P a ⟦S⟧✓ □b∈B → Q b  = □x∈(A ∩ B) → (P x ⟦S⟧✓ Q x)›
  by (fact Mprefix_Syncptick_Mprefix_bis[of ‹{}› S A ‹{}› B, simplified])

lemma Mprefix_Syncptick_Mprefix_indep :
  ‹⟦A ∩ S = {}; B ∩ S = {}⟧ ⟹
   □a∈A → P a ⟦S⟧✓ □b∈B → Q b =
   (□a∈A → (P a ⟦S⟧✓ □b∈B → Q b)) □ (□b∈B → (□a∈A → P a ⟦S⟧✓ Q b))›
  by (fact Mprefix_Syncptick_Mprefix_bis[of A S ‹{}› B ‹{}›, simplified])

lemma Mprefix_Syncptick_Mprefix_left :
  ‹⟦A ∩ S = {}; B ⊆ S⟧ ⟹ □a∈A → P a ⟦S⟧✓ □b∈B → Q b = □a∈A → (P a ⟦S⟧✓ □b∈B → Q b)›
  by (fact Mprefix_Syncptick_Mprefix_bis[of A S ‹{}› ‹{}› B, simplified])

lemma Mprefix_Syncptick_Mprefix_right :
  ‹⟦A ⊆ S; B ∩ S = {}⟧ ⟹ □a∈A → P a ⟦S⟧✓ □b∈B → Q b = □b∈B → (□a∈A → P a ⟦S⟧✓ Q b)›
  by (fact Mprefix_Syncptick_Mprefix_bis[of ‹{}› S A B ‹{}›, simplified])


lemma Mprefix_Syncptick_STOP : ‹□a ∈ A → P a ⟦S⟧✓ STOP = □a ∈ (A - S) → (P a ⟦S⟧✓ STOP)›
  by (subst Mprefix_empty[symmetric], subst Mprefix_Syncptick_Mprefix, simp)

lemma STOP_Syncptick_Mprefix : ‹STOP ⟦S⟧✓ □b ∈ B → Q b = □b ∈ (B - S) → (STOP ⟦S⟧✓ Q b)›
  by (subst Mprefix_empty[symmetric], subst Mprefix_Syncptick_Mprefix, simp)



paragraph ‹Mixing deterministic and non deterministic prefix choices›

lemma Mndetprefix_Syncptick_Mprefix :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧✓ (□b ∈ B → Q b)
    else ⊓a∈A. (if a ∈ S then STOP else (a → (P a ⟦S⟧✓ (□b ∈ B → Q b)))) □
                (□b∈(B - S) → ((a → P a) ⟦S⟧✓ Q b)) □
                (if a ∈ B ∩ S then (a → (P a ⟦S⟧✓ Q a)) else STOP))›
  unfolding Mndetprefix_GlobalNdet Syncptick_distrib_GlobalNdet_right
    write0_def Mprefix_Syncptick_Mprefix
  by (auto simp add: Mprefix_singl insert_Diff_if Int_insert_left
      intro: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])

lemma Mprefix_Syncptick_Mndetprefix :
  ‹(□a ∈ A → P a) ⟦S⟧✓ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧✓ STOP
    else ⊓b∈B. (if b ∈ S then STOP else (b → ((□a ∈ A → P a) ⟦S⟧✓ Q b))) □
                (□a∈(A - S) → (P a ⟦S⟧✓ (b → Q b))) □
                (if b ∈ A ∩ S then (b → (P b ⟦S⟧✓ Q b)) else STOP))›
  unfolding Mndetprefix_GlobalNdet Syncptick_distrib_GlobalNdet_left
    write0_def Mprefix_Syncptick_Mprefix
  by (subst Det_commute)
    (auto simp add: Diff_triv Mprefix_singl Mprefix_is_STOP_iff disjoint_iff
      intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›] split: if_split_asm)


text ‹In particular, we can obtain the theorem for const‹Mndetprefix› synchronized with const‹STOP›.›

lemma Mndetprefix_Syncptick_STOP :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ STOP =
   (  if A ∩ S = {} then ⊓a ∈ A → (P a ⟦S⟧✓ STOP)
    else (⊓a ∈ (A - S) → (P a ⟦S⟧✓ STOP)) ⊓ STOP)›
  (is ‹?lhs = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›)
proof -
  have ‹(⊓a ∈ A → P a) ⟦S⟧✓ STOP =
        ⊓a∈A. (if a ∈ S then STOP else (a → (P a ⟦S⟧✓ STOP)))› (is ‹?lhs = ?rhs'›)
    by (subst Mndetprefix_Syncptick_Mprefix[where B = ‹{}›, simplified])
      (auto intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›
  proof (split if_split, intro conjI impI)
    show ‹A ∩ S = {} ⟹ ?rhs' = ?rhs1›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A ∩ S ≠ {}›
    proof (cases ‹A - S = {}›)
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A - S = {}›
        by (simp add: ‹A - S = {}› GlobalNdet_is_STOP_iff)
          (use ‹A - S = {}› in blast)
    next
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹A - S ≠ {}›
      proof (subst Int_Diff_Un[symmetric],
          subst GlobalNdet_factorization_union
          [OF ‹A ∩ S ≠ {}› ‹A - S ≠ {}›, symmetric])
        have ‹(⊓a∈(A ∩ S). (if a ∈ S then STOP else (a → (P a ⟦S⟧✓ STOP))))
              = STOP› (is ‹?fact1 = STOP›)
          by (simp add: GlobalNdet_is_STOP_iff)
        moreover have ‹(⊓a∈(A - S). (if a ∈ S then STOP else (a → (P a ⟦S⟧✓ STOP))))
                       = ?rhs2› (is ‹?fact2 = ?rhs2›)
          by (auto simp add: Mndetprefix_GlobalNdet intro: mono_GlobalNdet_eq)
        ultimately show ‹?fact1 ⊓ ?fact2 = ?rhs2 ⊓ STOP› by (metis Ndet_commute)
      qed
    qed
  qed
  finally show ‹?lhs = (if A ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)› .
qed

lemma STOP_Syncptick_Mndetprefix :
  ‹STOP ⟦S⟧✓ (⊓b ∈ B → Q b)  =
   (  if B ∩ S = {} then ⊓b ∈ B → (STOP ⟦S⟧✓ Q b)
    else (⊓b ∈ (B - S) → (STOP ⟦S⟧✓ Q b)) ⊓ STOP)›
  (is ‹?lhs = (if B ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›)
proof -
  have ‹STOP ⟦S⟧✓ (⊓b ∈ B → Q b) =
        ⊓b∈B. (if b ∈ S then STOP else (b → (STOP ⟦S⟧✓ Q b)))› (is ‹?lhs = ?rhs'›)
    by (subst Mprefix_Syncptick_Mndetprefix[where A = ‹{}›, simplified])
      (auto intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if B ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)›
  proof (split if_split, intro conjI impI)
    show ‹B ∩ S = {} ⟹ ?rhs' = ?rhs1›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹B ∩ S ≠ {}›
    proof (cases ‹B - S = {}›)
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹B - S = {}›
        by (simp add: ‹B - S = {}› GlobalNdet_is_STOP_iff)
          (use ‹B - S = {}› in blast)
    next
      show ‹?rhs' = ?rhs2 ⊓ STOP› if ‹B - S ≠ {}›
      proof (subst Int_Diff_Un[symmetric],
          subst GlobalNdet_factorization_union
          [OF ‹B ∩ S ≠ {}› ‹B - S ≠ {}›, symmetric])
        have ‹(⊓b∈(B ∩ S). (if b ∈ S then STOP else (b → (STOP ⟦S⟧✓ Q b))))
              = STOP› (is ‹?fact1 = STOP›)
          by (simp add: GlobalNdet_is_STOP_iff)
        moreover have ‹(⊓b∈(B - S). (if b ∈ S then STOP else (b → (STOP ⟦S⟧✓ Q b))))
                       = ?rhs2› (is ‹?fact2 = ?rhs2›)
          by (auto simp add: Mndetprefix_GlobalNdet intro: mono_GlobalNdet_eq)
        ultimately show ‹?fact1 ⊓ ?fact2 = ?rhs2 ⊓ STOP› by (metis Ndet_commute)
      qed
    qed
  qed
  finally show ‹?lhs = (if B ∩ S = {} then ?rhs1 else ?rhs2 ⊓ STOP)› .
qed


corollary Mndetprefix_Syncptick_Mprefix_subset :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ (□b ∈ B → Q b) =
   (  if A ⊆ B then ⊓ a ∈ A → (P a ⟦S⟧✓ Q a)
    else (⊓a ∈ (A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP)›
  (is ‹?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)›) if ‹A ⊆ S› ‹B ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)›
    by (simp add: Mprefix_is_STOP_iff STOP_Syncptick_Mprefix ‹B ⊆ S›)
next
  from ‹A ⊆ S› have  * : ‹a ∈ A ⟹ a ∈ S› for a by blast
  from ‹B ⊆ S› have ** : ‹B - S = {}› ‹b ∈ B ∧ b ∈ S ⟷ b ∈ B› for b by auto
  assume ‹A ≠ {}›
  have ‹?lhs = ⊓a∈A. (if a ∈ B then (a → (P a ⟦S⟧✓ Q a)) else STOP)› (is ‹?lhs = ?rhs'›)
    by (auto simp add: Mndetprefix_Syncptick_Mprefix "*" "**" ‹A ≠ {}› intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if A ⊆ B then ?rhs1 else ?rhs2)›
  proof (split if_split, intro conjI impI)
    show ‹A ⊆ B ⟹ ?rhs' = ⊓a∈A → (P a ⟦S⟧✓ Q a)›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP› if ‹¬ A ⊆ B›
    proof (cases ‹A ∩ B = {}›)
      show ‹A ∩ B = {} ⟹ ?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP›
        by (auto simp add: GlobalNdet_is_STOP_iff)
    next
      assume ‹A ∩ B ≠ {}›
      from ‹¬ A ⊆ B› have ‹A - B ≠ {}› by blast
      show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP›
        by (auto simp add: Mndetprefix_GlobalNdet GlobalNdet_is_STOP_iff
            simp flip: GlobalNdet_factorization_union
            [OF ‹A ∩ B ≠ {}› ‹A - B ≠ {}›, unfolded Int_Diff_Un]
            intro!: arg_cong2[where f = ‹(⊓)›] mono_GlobalNdet_eq)
    qed
  qed
  finally show ‹?lhs = (if A ⊆ B then ?rhs1 else ?rhs2)› by simp
qed


corollary Mprefix_Syncptick_Mndetprefix_subset :
  ‹□a ∈ A → P a ⟦S⟧✓ ⊓b ∈ B → Q b =
   (  if B ⊆ A then ⊓b ∈ B → (P b ⟦S⟧✓ Q b)
    else (⊓b ∈ (A ∩ B) → (P b ⟦S⟧✓ Q b)) ⊓ STOP)›
  (is ‹?lhs = (if B ⊆ A then ?rhs1 else ?rhs2)›) if ‹A ⊆ S› ‹B ⊆ S›
proof (cases ‹B = {}›)
  show ‹B = {} ⟹ ?lhs = (if B ⊆ A then ?rhs1 else ?rhs2)›
    by (simp add: Mprefix_is_STOP_iff Mprefix_Syncptick_STOP ‹A ⊆ S›)
next
  from ‹B ⊆ S› have  * : ‹b ∈ B ⟹ b ∈ S› for b by blast
  from ‹A ⊆ S› have ** : ‹A - S = {}› ‹a ∈ A ∧ a ∈ S ⟷ a ∈ A› for a by auto
  assume ‹B ≠ {}›
  have ‹?lhs = ⊓b∈B. (if b ∈ A then (b → (P b ⟦S⟧✓ Q b)) else STOP)› (is ‹?lhs = ?rhs'›)
    by (auto simp add: Mprefix_Syncptick_Mndetprefix "*" "**" ‹B ≠ {}› intro: mono_GlobalNdet_eq)
  also have ‹?rhs' = (if B ⊆ A then ?rhs1 else ?rhs2)›
  proof (split if_split, intro conjI impI)
    show ‹B ⊆ A ⟹ ?rhs' = ⊓b∈B → (P b ⟦S⟧✓ Q b)›
      by (auto simp add: Mndetprefix_GlobalNdet intro!: mono_GlobalNdet_eq)
  next
    show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP› if ‹¬ B ⊆ A›
    proof (cases ‹A ∩ B = {}›)
      show ‹A ∩ B = {} ⟹ ?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP›
        by (auto simp add: GlobalNdet_is_STOP_iff)
    next
      assume ‹A ∩ B ≠ {}›
      hence ‹B ∩ A ≠ {}› by blast 
      from ‹¬ B ⊆ A› have ‹B - A ≠ {}› by blast
      show ‹?rhs' = (⊓a∈(A ∩ B) → (P a ⟦S⟧✓ Q a)) ⊓ STOP›
        by (auto simp add: Mndetprefix_GlobalNdet GlobalNdet_is_STOP_iff
            simp flip: Int_commute GlobalNdet_factorization_union
            [OF ‹B ∩ A ≠ {}› ‹B - A ≠ {}›, unfolded Int_Diff_Un]
            intro!: arg_cong2[where f = ‹(⊓)›] mono_GlobalNdet_eq)
    qed
  qed
  finally show ‹?lhs = (if B ⊆ A then ?rhs1 else ?rhs2)› by simp
qed



corollary Mndetprefix_Syncptick_Mprefix_indep :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ (□b ∈ B → Q b) =
   (  if A = {} then □b∈B → (STOP ⟦S⟧✓ Q b)
    else ⊓a∈A. (a → (P a ⟦S⟧✓ (□b ∈ B → Q b))) □
                (□b∈B → ((a → P a) ⟦S⟧✓ Q b)))›
  if ‹A ∩ S = {}› and ‹B ∩ S = {}›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis›
    by (simp add: Diff_triv STOP_Syncptick_Mprefix ‹B ∩ S = {}›)
next
  from that(1) have  * : ‹a ∈ A ⟹ a ∉ S› for a by blast
  from that(2) have ** : ‹B - S = B› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Syncptick_Mprefix ‹A ≠ {}›)   
      (rule mono_GlobalNdet_eq, simp add: "*" "**")
qed

corollary Mprefix_Syncptick_Mndetprefix_indep :
  ‹(□a ∈ A → P a) ⟦S⟧✓ (⊓b ∈ B → Q b) =
   (  if B = {} then □a ∈ A → (P a ⟦S⟧✓ STOP)
    else ⊓b∈B. (b → ((□a ∈ A → P a) ⟦S⟧✓ Q b)) □
                (□a∈A → (P a ⟦S⟧✓ (b → Q b))))›
  if ‹A ∩ S = {}› ‹B ∩ S = {}›
proof (cases ‹B = {}›)
  show ‹B = {} ⟹ ?thesis›
    by (simp add: Diff_triv Mprefix_Syncptick_STOP ‹A ∩ S = {}›)
next
  from that(2) have  * : ‹b ∈ B ⟹ b ∉ S› for b by blast
  from that(1) have ** : ‹A - S = A› by blast
  show ?thesis if ‹B ≠ {}›
    by (simp add: Mprefix_Syncptick_Mndetprefix ‹B ≠ {}›)   
      (rule mono_GlobalNdet_eq, simp add: "*" "**")
qed


corollary Mndetprefix_Syncptick_Mprefix_left :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧✓ (□b ∈ B → Q b)
    else ⊓a∈A → (P a ⟦S⟧✓ (□b ∈ B → Q b)))›
  if ‹A ∩ S = {}› and ‹B ⊆ S›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis› by simp
next
  from that(1) have   * : ‹a ∈ A ⟹ a ∉ S› for a by blast
  from that(2) have  ** : ‹B - S = {}› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Syncptick_Mprefix ‹A ≠ {}›, unfold Mndetprefix_GlobalNdet)
      (rule mono_GlobalNdet_eq, simp add: "*" "**")
qed

corollary Mndetprefix_Syncptick_Mprefix_right :
  ‹(⊓a ∈ A → P a) ⟦S⟧✓ (□b ∈ B → Q b) =
   (  if A = {} then STOP ⟦S⟧✓ (□b ∈ B → Q b)
    else □b∈B → ((⊓a∈A → P a) ⟦S⟧✓ Q b))›
  if ‹A ⊆ S› and ‹B ∩ S = {}›
proof (cases ‹A = {}›)
  show ‹A = {} ⟹ ?thesis› by simp
next
  from that(1) have   * : ‹a ∈ A ⟹ a ∈ S› for a by blast
  from that(2) have  ** : ‹B - S = B› by blast
  show ?thesis if ‹A ≠ {}›
    by (simp add: Mndetprefix_Syncptick_Mprefix ‹A ≠ {}›,
        simp add: Mndetprefix_GlobalNdet Syncptick_distrib_GlobalNdet_right ‹A ≠ {}›
        flip: GlobalNdet_Mprefix_distr)
      (rule mono_GlobalNdet_eq, use "*" "**" in auto)
qed

corollary Mprefix_Syncptick_Mndetprefix_left :
  ‹(□a ∈ A → P a) ⟦S⟧✓ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧✓ STOP
    else □a∈A → (P a ⟦S⟧✓ (⊓b ∈ B → Q b)))›
  if ‹A ∩ S = {}› ‹B ⊆ S›
proof (cases ‹B = {}›)
  show ‹B = {} ⟹ ?thesis› by simp
next
  from that(2) have   * : ‹b ∈ B ⟹ b ∈ S› for b by blast
  from that(1) have  ** : ‹A - S = A› by blast
  show ?thesis if ‹B ≠ {}›
    by (simp add: Mprefix_Syncptick_Mndetprefix ‹B ≠ {}›,
        simp add: Mndetprefix_GlobalNdet Syncptick_distrib_GlobalNdet_left ‹B ≠ {}›
        flip: GlobalNdet_Mprefix_distr)
      (rule mono_GlobalNdet_eq, use "*" "**" in auto)
qed

corollary Mprefix_Syncptick_Mndetprefix_right :
  ‹(□a ∈ A → P a) ⟦S⟧✓ (⊓b ∈ B → Q b) =
   (  if B = {} then (□a ∈ A → P a) ⟦S⟧✓ STOP
    else ⊓b∈B → ((□a ∈ A → P a) ⟦S⟧✓ Q b))›
  if ‹A ⊆ S› ‹B ∩ S = {}›
proof (cases ‹B = {}›)
  show ‹B = {} ⟹ ?thesis› by simp
next
  from that(2) have   * : ‹b ∈ B ⟹ b ∉ S› for b by blast
  from that(1) have  ** : ‹A - S = {}› by blast
  show ?thesis if ‹B ≠ {}›
    by (simp add: Mprefix_Syncptick_Mndetprefix ‹B ≠ {}›,
        unfold Mndetprefix_GlobalNdet)
      (rule mono_GlobalNdet_eq, simp add: "*" "**")
qed



corollary Mndetprefix_Parptick_Mprefix :
  ‹⊓a ∈ A → P a ||✓ □b ∈ B → Q b =
   (if A ⊆ B then ⊓a ∈ A → (P a ||✓ Q a) else (⊓a ∈ (A ∩ B) → (P a ||✓ Q a)) ⊓ STOP)›
  by (simp add: Mndetprefix_Syncptick_Mprefix_subset)

corollary Mprefix_Parptick_Mndetprefix :
  ‹□a ∈ A → P a ||✓ ⊓b ∈ B → Q b =
   (if B ⊆ A then ⊓b ∈ B → (P b ||✓ Q b) else (⊓b ∈ (A ∩ B) → (P b ||✓ Q b)) ⊓ STOP)›
  by (simp add: Mprefix_Syncptick_Mndetprefix_subset)

corollary Mndetprefix_Interptick_Mprefix :
  ‹⊓a ∈ A → P a |||✓ □b ∈ B → Q b =
   (  if A = {} then □b ∈ B → RenamingTick (Q b ; STOP) (λs. the (tick_join (g s) s))
    else ⊓a∈A. (a → (P a |||✓ □b ∈ B → Q b)) □
                (□b∈B → (a → P a |||✓ Q b)))›
  by (simp add: Mndetprefix_Syncptick_Mprefix_indep
      Mprefix_Seq STOP_Interptick[of _ g])

corollary Mprefix_Interptick_Mndetprefix :
  ‹□a ∈ A → P a |||✓ ⊓b ∈ B → Q b =
   (  if B = {} then □a ∈ A → RenamingTick (P a ; STOP) (λr. the (tick_join r (g r)))
    else ⊓b∈B. (b → (□a ∈ A → P a |||✓ Q b)) □
                (□a∈A → (P a |||✓ b → Q b)))›
  by (simp add: Mprefix_Syncptick_Mndetprefix_indep
      Mprefix_Seq Interptick_STOP[of _ g])



paragraph ‹Mixing two non deterministic prefix choices›

lemma Mndetprefix_Syncptick_Mndetprefix :
  ‹⊓a∈A → P a ⟦S⟧✓ ⊓b∈B → Q b =
   (  if A = {} then   if B ∩ S = {} then ⊓b∈B → (STOP ⟦S⟧✓ Q b)
                     else (⊓x ∈ (B - S) → (STOP ⟦S⟧✓ Q x)) ⊓ STOP
    else   if B = {} then   if A ∩ S = {} then ⊓a∈A → (P a ⟦S⟧✓ STOP)
                          else (⊓x ∈(A - S) → (P x ⟦S⟧✓ STOP)) ⊓ STOP
         else ⊓b∈B. ⊓a∈A.
              (if a ∈ S then STOP else a → (P a ⟦S⟧✓ b → Q b)) □
              (if b ∈ S then STOP else b → (a → P a ⟦S⟧✓ Q b)) □
              (if a = b ∧ b ∈ S then b → (P a ⟦S⟧✓ Q b) else STOP))›
  (is ‹?lhs = (  if A = {} then if B ∩ S = {} then ?mv_right else ?mv_right' ⊓ STOP
               else   if B = {} then if A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP
                    else ?huge_mess)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = (if B ∩ S = {} then ?mv_right else ?mv_right' ⊓ STOP)›
    by (auto simp add: STOP_Syncptick_Mndetprefix intro: mono_Mndetprefix_eq)
next
  show ‹?lhs = (if B = {} then if A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP else ?huge_mess)› if ‹A ≠ {}›
  proof (split if_split, intro conjI impI)
    show ‹B = {} ⟹ ?lhs = (if A ∩ S = {} then ?mv_left else ?mv_left' ⊓ STOP)›
      by (auto simp add: Mndetprefix_Syncptick_STOP intro: mono_Mndetprefix_eq)
  next
    assume ‹B ≠ {}›
    have ‹?lhs = ⊓b∈B. ⊓a∈A. (a → P a ⟦S⟧✓ (b → Q b))›
      by (simp add: Mndetprefix_GlobalNdet ‹A ≠ {}› ‹B ≠ {}›
          Syncptick_distrib_GlobalNdet_left Syncptick_distrib_GlobalNdet_right)
    also have ‹… = ?huge_mess›
      by (auto simp add: write0_def Mprefix_Syncptick_Mprefix Diff_triv Mprefix_is_STOP_iff
          intro!: mono_GlobalNdet_eq arg_cong2[where f = ‹(□)›])
    finally show ‹?lhs = ?huge_mess› .
  qed
qed


lemma Mndetprefix_Syncptick_Mndetprefix_subset :
  ‹⊓a∈A → P a ⟦S⟧✓ ⊓b∈B → Q b =
   (  if ∃b. A = {b} ∧ B = {b}
    then (THE b. B = {b}) → (P (THE a. A = {a}) ⟦S⟧✓ Q (THE b. B = {b}))
    else (⊓x ∈ (A ∩ B) → (P x ⟦S⟧✓ Q x)) ⊓ STOP)›
  (is ‹?lhs = (if ?cond then ?rhs1 else ?rhs2)›) if ‹A ⊆ S› ‹B ⊆ S›
proof (split if_split, intro conjI impI)
  show ‹?cond ⟹ ?lhs = ?rhs1›
    by (elim exE, simp add: write0_def)
      (subst Mprefix_Syncptick_Mprefix_subset, use ‹A ⊆ S› in simp_all)
next
  assume ‹¬ ?cond›
  let ?term = ‹λa b. (b → (P a ⟦S⟧✓ Q b))›
  have ‹?lhs = ⊓b∈B. ⊓a∈A. (if a = b then ?term a b else STOP)›
    (is ‹?lhs = ⊓b∈B. ⊓a∈A. ?rhs' b a›)
  proof (cases ‹A = {} ∨ B = {}›)
    from ‹A ⊆ S› ‹B ⊆ S› show ‹A = {} ∨ B = {} ⟹ ?lhs = (⊓b∈B. ⊓a∈A. ?rhs' b a)›
      by (elim disjE) (simp_all add: Mndetprefix_Syncptick_STOP STOP_Syncptick_Mndetprefix
          Int_absorb2 Mndetprefix_is_STOP_iff Ndet_is_STOP_iff)
  next
    show ‹¬ (A = {} ∨ B = {}) ⟹ ?lhs = (⊓b∈B. ⊓a∈A. ?rhs' b a)›
      by (simp add: Mndetprefix_Syncptick_Mndetprefix)
        (intro mono_GlobalNdet_eq, use ‹A ⊆ S› ‹B ⊆ S› in auto)
  qed

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

      hence ‹⊓b ∈ B. ⊓a∈A. ?rhs' b a =
             ⊓b ∈ B. (if b ∈ A then if A = {b} then ?term b b else (?term b b) ⊓ STOP else STOP)›
        by (fact mono_GlobalNdet_eq)
      also from ‹B - A ≠ {}› have ‹… = (⊓b ∈ B. (if b ∈ 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 ‹B ∩ A ≠ {}› ‹B - A ≠ {}›, unfolded Int_Diff_Un])
        have ‹⊓b∈(B ∩ A). (if b ∈ A then ?term b b else STOP) =
              ⊓b∈(B ∩ A). ?term b b› by (auto intro: mono_GlobalNdet_eq)
        moreover have ‹⊓b∈(B - A). (if b ∈ A then ?term b b else STOP) = STOP›
          by (simp add: GlobalNdet_is_STOP_iff)
        ultimately show ‹(⊓b∈(B ∩ A). (if b ∈ A then ?term b b else STOP)) ⊓
                         (⊓b∈(B - A). (if b ∈ A then ?term b b else STOP)) ⊓ STOP = ?rhs2›
          by (metis Mndetprefix_GlobalNdet Int_commute Ndet_assoc Ndet_id)
      qed
      finally show ‹(⊓b ∈ B. ⊓a ∈ A. ?rhs' b a) = ?rhs2› .
    qed
  qed
  finally show ‹?lhs = ?rhs2› .
qed


lemma Mndetprefix_Syncptick_Mndetprefix_indep :
  ‹A ∩ S = {} ⟹ B ∩ S = {} ⟹
   ⊓a∈A → P a ⟦S⟧✓ ⊓b∈B → Q b =
   (  if A = {} then ⊓b∈B → (STOP ⟦S⟧✓ Q b)
    else   if B = {} then ⊓a∈A → (P a ⟦S⟧✓ STOP)
         else ⊓b∈B. ⊓a∈A.
              ((a → (P a ⟦S⟧✓ b → Q b))) □
              ((b → (a → P a ⟦S⟧✓ Q b))))›
  by (simp add: Mndetprefix_Syncptick_STOP STOP_Syncptick_Mndetprefix)
    (auto simp add: Mndetprefix_GlobalNdet Syncptick_distrib_GlobalNdet_left
      Syncptick_distrib_GlobalNdet_right disjoint_iff write0_def
      Mprefix_Syncptick_Mprefix Int_assoc insert_Diff_if
      intro!: mono_GlobalNdet_eq)


lemma Mndetprefix_Syncptick_Mndetprefix_left :
  ‹⊓a∈A → P a ⟦S⟧✓ ⊓b∈B → Q b = ⊓a∈A → (P a ⟦S⟧✓ ⊓b∈B → Q b)›
  (is ‹?lhs = ?rhs›) if ‹A ∩ S = {}› ‹B ⊆ S›
proof -
  let ?rhs' = ‹⊓b∈B. ⊓a∈A. a → (P a ⟦S⟧✓ b → Q b)›
  have ‹?lhs = (  if A = {} then   if B ∩ S = {} then ⊓b∈B → (STOP ⟦S⟧✓ Q b)
                                 else (⊓x∈(B - S) → (STOP ⟦S⟧✓ Q x)) ⊓ STOP
                else   if B = {} then   if A ∩ S = {} then ⊓a∈A → (P a ⟦S⟧✓ STOP)
                                      else (⊓x∈(A - S) → (P x ⟦S⟧✓ STOP)) ⊓ STOP
                     else ⊓b∈B. ⊓a∈A.
                          (if a ∈ S then STOP else (a → (P a ⟦S⟧✓ b → Q b))) □
                          (if b ∈ S then STOP else (b → (a → P a ⟦S⟧✓ Q b))) □
                          (if a = b ∧ b ∈ S then b → (P a ⟦S⟧✓ Q b) else STOP))›
    (is ‹?lhs = (if A = {} then ?rhs1 else if B = {} then ?rhs2 else ?rhs3)›)
    by (fact Mndetprefix_Syncptick_Mndetprefix)
  also from ‹B ⊆ S› have ‹?rhs1 = STOP›
    by (auto simp add: Ndet_is_STOP_iff Mndetprefix_GlobalNdet GlobalNdet_is_STOP_iff)
  also from ‹A ∩ S = {}› have ‹?rhs2 = ⊓a∈A → (P a ⟦S⟧✓ STOP)› by presburger
  also from ‹A ∩ S = {}› ‹B ⊆ S›
  have ‹?rhs3 = ⊓b∈B. ⊓a∈A. a → (P a ⟦S⟧✓ b → Q b)›
    by (intro mono_GlobalNdet_eq) auto
  finally have ‹?lhs = (  if A = {} then STOP
                        else   if B = {} then ⊓a∈A → (P a ⟦S⟧✓ STOP)
                             else ?rhs')› .
  moreover have ‹B ≠ {} ⟹ ?rhs' = ⊓a∈A. a → (P a ⟦S⟧✓ ⊓b∈B. b → Q b)›
    by (subst GlobalNdet_sets_commute)
      (simp add: Syncptick_distrib_GlobalNdet_left write0_GlobalNdet)
  moreover have ‹… = ⊓a∈A → (P a ⟦S⟧✓ ⊓b∈B → Q b)›
    by (simp add: Mndetprefix_GlobalNdet)
  ultimately show ‹?lhs = ?rhs› by simp
qed

end


corollary (in Syncptick_locale) Mndetprefix_Syncptick_Mndetprefix_right :
  ‹⊓a∈A → P a ⟦S⟧✓ ⊓b∈B → Q b = ⊓b∈B → (⊓a∈A → P a ⟦S⟧✓ Q b)›
  (is ‹?lhs = ?rhs›) if ‹A ⊆ S› ‹B ∩ S = {}›
  by (subst (1 2) Syncptick_locale_sym.Syncptick_sym)
    (simp add: Syncptick_locale_sym.Mndetprefix_Syncptick_Mndetprefix_left that)



(*<*)
end
  (*>*)