Theory Non_Deterministic_CSP_PTick_Distributivity

(***********************************************************************************
 * 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 Non_Deterministic_CSP_PTick_Distributivity
  imports Sequential_Composition_Generalized
    Synchronization_Product_Generalized
begin
  (*>*)


section ‹Distributivity of Non-Determinism›

subsection ‹Sequential Composition›

lemma Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left :
  ‹P ❙;⇩_✓ (λr. ⊓ a∈A. Q a r) = (if A = {} then P ❙;⇩_✓ (λr. STOP) else ⊓ a∈A. (P ❙;⇩_✓ Q a))›
  by simp (auto simp add: Process_eq_spec GlobalNdet_projs STOP_projs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)

lemma Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right : ‹(⊓ a∈A. P a) ❙;⇩_✓ Q = ⊓ a∈A. (P a ❙;⇩_✓ Q)›
  by (simp add: Process_eq_spec GlobalNdet_projs STOP_projs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
    (safe; simp; blast) ― ‹quicker than auto proof›


lemma Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_left : ‹P ❙;⇩_✓ (λr. Q r ⊓ R r) = (P ❙;⇩_✓ Q) ⊓ (P ❙;⇩_✓ R)›
  by (fact Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left[of P ‹{0 :: nat, 1}›
        ‹λn. if n = 0 then Q else if n = 1 then R else undefined›,
        simplified GlobalNdet_distrib_unit_bis, simplified])

lemma Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_right : ‹P ⊓ Q ❙;⇩_✓ R = (P ❙;⇩_✓ R) ⊓ (Q ❙;⇩_✓ R)›
  by (fact Seq⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right[of ‹{0 :: nat, 1}›
        ‹λn. if n = 0 then P else if n = 1 then Q else undefined› R,
        simplified GlobalNdet_distrib_unit_bis, simplified])



subsection ‹Synchronization Product›

context Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale begin

lemma Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left : 
  ‹P ⟦S⟧⇩_✓ ⊓ a∈A. Q a = (if A = {} then P ⟦S⟧⇩_✓ STOP else ⊓ a∈A. (P ⟦S⟧⇩_✓ Q a))›
  (is ‹?lhs = (if A = {} then P ⟦S⟧⇩_✓ STOP else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = P ⟦S⟧⇩_✓ STOP›
    by (simp add: GlobalNdet.abs_eq STOP.abs_eq)
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (subst Process_eq_spec_optimized, safe)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (simp add: D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k GlobalNdet_projs)
        (metis ‹A ≠ {}› ex_in_conv is_processT1_TR)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (simp add: GlobalNdet_projs D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast
  next
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    fix t X assume ‹(t, X) ∈ ℱ ?lhs›
    with ‹A ≠ {}› consider ‹t ∈ 𝒟 ?lhs›
      | (fail) t_P t_Q X_P X_Q a where
        ‹(t_P, X_P) ∈ ℱ P› ‹a ∈ A› ‹(t_Q, X_Q) ∈ ℱ (Q a)›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs F_GlobalNdet by force
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 ?lhs ⟹ (t, X) ∈ ℱ ?rhs› by blast
    next
      case fail
      thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: F_GlobalNdet F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast
    qed
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X  
      by (simp add: GlobalNdet_projs F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k ‹A ≠ {}›) blast
  qed
qed

lemma Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right : 
  ‹⊓ a∈A. P a ⟦S⟧⇩_✓ Q = (if A = {} then STOP ⟦S⟧⇩_✓ Q else ⊓ a∈A. (P a ⟦S⟧⇩_✓ Q))›
  (is ‹?lhs = (if A = {} then STOP ⟦S⟧⇩_✓ Q else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = STOP ⟦S⟧⇩_✓ Q›
    by (simp add: GlobalNdet.abs_eq STOP.abs_eq)
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (subst Process_eq_spec_optimized, safe)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (simp add: D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k GlobalNdet_projs)
        (metis ‹A ≠ {}› ex_in_conv is_processT1_TR)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (simp add: GlobalNdet_projs D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast
  next
    assume same_div : ‹𝒟 ?lhs = 𝒟 ?rhs›
    fix t X assume ‹(t, X) ∈ ℱ ?lhs›
    with ‹A ≠ {}› consider ‹t ∈ 𝒟 ?lhs›
      | (fail) t_P t_Q X_P X_Q a where
        ‹(t_P, X_P) ∈ ℱ (P a)› ‹a ∈ A› ‹(t_Q, X_Q) ∈ ℱ Q›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), S)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P S X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs F_GlobalNdet by force
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      from same_div D_F show ‹t ∈ 𝒟 ?lhs ⟹ (t, X) ∈ ℱ ?rhs› by blast
    next
      case fail
      thus ‹(t, X) ∈ ℱ ?rhs› by (simp add: F_GlobalNdet F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast
    qed
  next
    show ‹(t, X) ∈ ℱ ?rhs ⟹ (t, X) ∈ ℱ ?lhs› for t X  
      by (simp add: GlobalNdet_projs F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k ‹A ≠ {}›) blast
  qed
qed


lemma (in Sync⇩_p⇩_t⇩_i⇩_c⇩_k_locale) Sync⇩_p⇩_t⇩_i⇩_c⇩_k_GlobalNdet_cartprod:
  ‹(⊓ (a, b) ∈ A × B. (P a ⟦S⟧⇩_✓ Q b)) = 
   (if A = {} ∨ B = {} then STOP else (⊓a ∈ A. P a) ⟦S⟧⇩_✓ (⊓b ∈ B. Q b))›  
  by (simp add: GlobalNdet_cartprod Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left
      Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right GlobalNdet_sets_commute[of A])


lemma Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_left : 
  ‹P ⟦S⟧⇩_✓ Q ⊓ R = (P ⟦S⟧⇩_✓ Q) ⊓ (P ⟦S⟧⇩_✓ R)›
  by (rule trans[OF trans[OF _ Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_left
          [of P S ‹{True, False}› ‹λb. if b then Q else R›]]])
    (simp_all add: GlobalNdet_distrib_unit)

corollary Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_Ndet_right : 
  ‹P ⊓ Q ⟦S⟧⇩_✓ R = (P ⟦S⟧⇩_✓ R) ⊓ (Q ⟦S⟧⇩_✓ R)›
  by (rule trans[OF trans[OF _ Sync⇩_p⇩_t⇩_i⇩_c⇩_k_distrib_GlobalNdet_right
          [of ‹{True, False}› ‹λb. if b then P else Q› S R]]])
    (simp_all add: GlobalNdet_distrib_unit)


end

(*<*)
end
  (*>*)