Theory Non_Deterministic_CSPM_Distributivity

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Distributivity of non determinism
 *
 * 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.
 ******************************************************************************›
(*>*)


(*<*)
theory Non_Deterministic_CSPM_Distributivity
  imports Global_Deterministic_Choice Multi_Synchronization_Product
    Multi_Sequential_Composition Interrupt Throw
begin
  (*>*)

subsection ‹The Throw Operator›

lemma Throw_distrib_Ndet_right :
  ‹P ⊓ P' Θ a ∈ A. Q a = (P Θ a ∈ A. Q a) ⊓ (P' Θ a ∈ A. Q a)›
  and Throw_distrib_Ndet_left :
  ‹P Θ a ∈ A. Q a ⊓ Q' a = (P Θ a ∈ A. Q a) ⊓ (P Θ a ∈ A. Q' a)›
  by (simp add: Process_eq_spec F_Throw F_Ndet D_Throw D_Ndet T_Ndet,
      safe, simp_all; blast)+


lemma Throw_distrib_GlobalNdet_right :
  ‹(⊓a ∈ A. P a) Θ b ∈ B. Q b = ⊓a ∈ A. (P a Θ b ∈ B. Q b)›
  and Throw_distrib_GlobalNdet_left :
  ‹P' Θ a ∈ A. (⊓b ∈ B. Q' a b) = 
   (if B = {} then P' Θ a ∈ A. STOP else ⊓b ∈ B. (P' Θ a ∈ A. Q' a b))›                
  by (simp add: Process_eq_spec Throw_projs GlobalNdet_projs, safe, simp_all; blast)
    (simp add: Process_eq_spec Throw_projs GlobalNdet_projs STOP_projs; blast)



subsection ‹The Interrupt Operator›

lemma Interrupt_distrib_GlobalNdet_left :
  ‹P △ (⊓a ∈ A. Q a) = (if A = {} then P else ⊓a ∈ A. P △ Q a)›
  (is ‹?lhs = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = P› by simp
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (auto simp add: ‹A ≠ {}› D_Interrupt D_GlobalNdet)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: ‹A ≠ {}› D_Interrupt D_GlobalNdet)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    with ‹A ≠ {}› consider r u where ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 P›
      | r where ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 P›
      | a where ‹a ∈ A› ‹(t, X) ∈ ℱ P› ‹tF t› ‹([], X) ∈ ℱ (Q a)›
      | a u v where ‹a ∈ A› ‹t = u @ v› ‹u ∈ 𝒯 P› ‹tF u› ‹(v, X) ∈ ℱ (Q a)› ‹v ≠ []›
      | a r where ‹a ∈ A› ‹✓(r) ∉ X› ‹t ∈ 𝒯 P› ‹tF t› ‹[✓(r)] ∈ 𝒯 (Q a)›
      unfolding Interrupt_projs GlobalNdet_projs by force
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      from ‹A ≠ {}› show ‹t = u @ [✓(r)] ⟹ u @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?rhs› for r u
        by (auto simp add: F_GlobalNdet F_Interrupt)
    next
      show ‹✓(r) ∉ X ⟹ t @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?rhs› for r
        by (simp add: F_GlobalNdet F_Interrupt)
          (metis Diff_insert_absorb all_not_in_conv ‹A ≠ {}›)
    next
      show ‹a ∈ A ⟹ (t, X) ∈ ℱ P ⟹ tF t ⟹ ([], X) ∈ ℱ (Q a) ⟹ (t, X) ∈ ℱ ?rhs› for a
        by (auto simp add: F_GlobalNdet F_Interrupt)
    next
      show ‹⟦a ∈ A; t = u @ v; u ∈ 𝒯 P; tF u; (v, X) ∈ ℱ (Q a); v ≠ []⟧
            ⟹ (t, X) ∈ ℱ ?rhs› for a u v by (auto simp add: F_GlobalNdet F_Interrupt)
    next
      show ‹⟦a ∈ A; ✓(r) ∉ X; t ∈ 𝒯 P; tF t; [✓(r)] ∈ 𝒯 (Q a)⟧ ⟹ (t, X) ∈ ℱ ?rhs› for a r
        by (simp add: F_GlobalNdet F_Interrupt) (metis Diff_insert_absorb ‹A ≠ {}›)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    from ‹(t, X) ∈ ℱ ?rhs› obtain a where ‹a ∈ A› ‹(t, X) ∈ ℱ (P △ Q a)›
      by (auto simp add: ‹A ≠ {}› F_GlobalNdet)
    with ‹t ∉ 𝒟 ?rhs› consider u r where ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 P›
      | r where ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 P›
      | ‹(t, X) ∈ ℱ P› ‹tF t› ‹([], X) ∈ ℱ (Q a)›
      | u v where ‹t = u @ v› ‹u ∈ 𝒯 P› ‹tF u› ‹(v, X) ∈ ℱ (Q a)› ‹v ≠ []›
      | r where ‹✓(r) ∉ X› ‹t ∈ 𝒯 P› ‹tF t› ‹[✓(r)] ∈ 𝒯 (Q a)›
      unfolding D_GlobalNdet Interrupt_projs by blast
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      show ‹t = u @ [✓(r)] ⟹ u @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?lhs› for u r
        by (simp add: F_Interrupt)
    next
      show ‹✓(r) ∉ X ⟹ t @ [✓(r)] ∈ 𝒯 P ⟹ (t, X) ∈ ℱ ?lhs› for r
        by (auto simp add: F_Interrupt)
    next
      from ‹a ∈ A› show ‹⟦(t, X) ∈ ℱ P; tF t; ([], X) ∈ ℱ (Q a)⟧ ⟹ (t, X) ∈ ℱ ?lhs›
        by (auto simp add: F_Interrupt F_GlobalNdet)
    next
      from ‹a ∈ A› show ‹⟦t = u @ v; u ∈ 𝒯 P; tF u; (v, X) ∈ ℱ (Q a); v ≠ []⟧ ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: ‹A ≠ {}› F_Interrupt F_GlobalNdet) blast
    next
      from ‹a ∈ A› show ‹⟦✓(r) ∉ X; t ∈ 𝒯 P; tF t; [✓(r)] ∈ 𝒯 (Q a)⟧ ⟹ (t, X) ∈ ℱ ?lhs› for r
        by (simp add: F_Interrupt GlobalNdet_projs) blast
    qed
  qed
qed


lemma Interrupt_distrib_GlobalNdet_right :
  ‹(⊓a ∈ A. P a) △ Q = (if A = {} then Q else ⊓a ∈ A. P a △ Q)›
  (is ‹?lhs = (if _ then _ else ?rhs)›)
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ ?lhs = Q› by simp
next
  show ‹?lhs = ?rhs› if ‹A ≠ {}›
  proof (rule Process_eq_optimizedI)
    show ‹t ∈ 𝒟 ?lhs ⟹ t ∈ 𝒟 ?rhs› for t
      by (simp add: GlobalNdet_projs D_Interrupt)
        (metis ex_in_conv is_processT1_TR ‹A ≠ {}›)
  next
    show ‹t ∈ 𝒟 ?rhs ⟹ t ∈ 𝒟 ?lhs› for t
      by (auto simp add: GlobalNdet_projs D_Interrupt)
  next
    fix t X assume ‹(t, X) ∈ ℱ ?lhs› ‹t ∉ 𝒟 ?lhs›
    then consider u r where ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 (⊓a ∈ A. P a)›
      | r where ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 (⊓a ∈ A. P a)›
      | ‹(t, X) ∈ ℱ (⊓a ∈ A. P a)› ‹tF t› ‹([], X) ∈ ℱ Q›
      | u v where ‹t = u @ v› ‹u ∈ 𝒯 (⊓a ∈ A. P a)› ‹tF u› ‹(v, X) ∈ ℱ Q› ‹v ≠ []›
      | r where ‹✓(r) ∉ X› ‹t ∈ 𝒯 (⊓a ∈ A. P a)› ‹tF t› ‹[✓(r)] ∈ 𝒯 Q›
      unfolding Interrupt_projs by blast
    thus ‹(t, X) ∈ ℱ ?rhs›
    proof cases
      show ‹t = u @ [✓(r)] ⟹ u @ [✓(r)] ∈ 𝒯 (⊓a ∈ A. P a) ⟹ (t, X) ∈ ℱ ?rhs› for u r
        by (auto simp add: ‹A ≠ {}› GlobalNdet_projs F_Interrupt)
    next
      show ‹✓(r) ∉ X ⟹ t @ [✓(r)] ∈ 𝒯 (⊓a ∈ A. P a) ⟹ (t, X) ∈ ℱ ?rhs› for r
        by (simp add: ‹A ≠ {}› GlobalNdet_projs F_Interrupt) (metis Diff_insert_absorb)
    next
      show ‹(t, X) ∈ ℱ (⊓a ∈ A. P a) ⟹ tF t ⟹ ([], X) ∈ ℱ Q ⟹ (t, X) ∈ ℱ ?rhs›
        by (auto simp add: ‹A ≠ {}› F_GlobalNdet F_Interrupt)
    next
      show ‹⟦t = u @ v; u ∈ 𝒯 (⊓a ∈ A. P a); tF u; (v, X) ∈ ℱ Q; v ≠ []⟧
            ⟹ (t, X) ∈ ℱ ?rhs› for u v
        by (simp add: ‹A ≠ {}› GlobalNdet_projs F_Interrupt)
          (metis ex_in_conv is_processT1_TR ‹A ≠ {}›)
    next
      show ‹✓(r) ∉ X ⟹ t ∈ 𝒯 (⊓a ∈ A. P a) ⟹ tF t ⟹ [✓(r)] ∈ 𝒯 Q ⟹ (t, X) ∈ ℱ ?rhs› for r
        by (simp add: ‹A ≠ {}› GlobalNdet_projs F_Interrupt)
          (metis Diff_insert_absorb equals0I is_processT1_TR ‹A ≠ {}›)
    qed
  next
    fix t X assume ‹(t, X) ∈ ℱ ?rhs› ‹t ∉ 𝒟 ?rhs›
    from ‹(t, X) ∈ ℱ ?rhs› obtain a where ‹a ∈ A› ‹(t, X) ∈ ℱ (P a △ Q)›
      by (auto simp add: ‹A ≠ {}› F_GlobalNdet)
    with ‹t ∉ 𝒟 ?rhs› consider u r where ‹t = u @ [✓(r)]› ‹u @ [✓(r)] ∈ 𝒯 (P a)›
      | r where ‹✓(r) ∉ X› ‹t @ [✓(r)] ∈ 𝒯 (P a)›
      | ‹(t, X) ∈ ℱ (P a)› ‹tF t› ‹([], X) ∈ ℱ Q›
      | u v where ‹t = u @ v› ‹u ∈ 𝒯 (P a)› ‹tF u› ‹(v, X) ∈ ℱ Q› ‹v ≠ []›
      | r where ‹✓(r) ∉ X› ‹t ∈ 𝒯 (P a)› ‹tF t› ‹[✓(r)] ∈ 𝒯 Q›
      unfolding D_GlobalNdet Interrupt_projs by blast
    thus ‹(t, X) ∈ ℱ ?lhs›
    proof cases
      from ‹a ∈ A› show ‹t = u @ [✓(r)] ⟹ u @ [✓(r)] ∈ 𝒯 (P a) ⟹ (t, X) ∈ ℱ ?lhs› for u r
        by (auto simp add: F_Interrupt T_GlobalNdet)
    next
      from ‹a ∈ A› show ‹✓(r) ∉ X ⟹ t @ [✓(r)] ∈ 𝒯 (P a) ⟹ (t, X) ∈ ℱ ?lhs› for r
        by (auto simp add: F_Interrupt GlobalNdet_projs)
    next
      from ‹a ∈ A› show ‹(t, X) ∈ ℱ (P a) ⟹ tF t ⟹ ([], X) ∈ ℱ Q ⟹ (t, X) ∈ ℱ ?lhs›
        by (auto simp add: F_Interrupt F_GlobalNdet)
    next
      from ‹a ∈ A› show ‹⟦t = u @ v; u ∈ 𝒯 (P a); tF u; (v, X) ∈ ℱ Q; v ≠ []⟧
                         ⟹ (t, X) ∈ ℱ ?lhs› for u v
        by (simp add: F_Interrupt GlobalNdet_projs) blast
    next
      from ‹a ∈ A› show ‹⟦✓(r) ∉ X; t ∈ 𝒯 (P a); tF t; [✓(r)] ∈ 𝒯 Q⟧ ⟹ (t, X) ∈ ℱ ?lhs› for r
        by (simp add: F_Interrupt GlobalNdet_projs) blast
    qed
  qed
qed



corollary Interrupt_distrib_Ndet_left : ‹P △ Q1 ⊓ Q2 = (P △ Q1) ⊓ (P △ Q2)›
proof -
  have ‹P △ Q1 ⊓ Q2 = P △ (⊓n ∈ {0::nat, 1}. (if n = 0 then Q1 else Q2))›
    by (simp add: GlobalNdet_distrib_unit)
  also have ‹… = (⊓n ∈ {0::nat, 1}. P △ (if n = 0 then Q1 else Q2))›
    by (simp add: Interrupt_distrib_GlobalNdet_left)
  also have ‹… = (P △ Q1) ⊓ (P △ Q2)›
    by (simp add: GlobalNdet_distrib_unit)
  finally show ?thesis .
qed

corollary Interrupt_distrib_Ndet_right : ‹P1 ⊓ P2 △ Q = (P1 △ Q) ⊓ (P2 △ Q)›
proof -
  have ‹P1 ⊓ P2 △ Q = (⊓n ∈ {0::nat, 1}. (if n = 0 then P1 else P2)) △ Q›
    by (simp add: GlobalNdet_distrib_unit)
  also have ‹… = (⊓n ∈ {0::nat, 1}. (if n = 0 then P1 else P2) △ Q)›
    by (simp add: Interrupt_distrib_GlobalNdet_right)
  also have ‹… = (P1 △ Q) ⊓ (P2 △ Q)›
    by (simp add: GlobalNdet_distrib_unit)
  finally show ?thesis .
qed



subsection ‹Global Deterministic Choice›

lemma GlobalDet_distrib_Ndet_left :
  ‹(□a ∈ A. P a ⊓ Q) = (if A = {} then STOP else (□a ∈ A. P a) ⊓ Q)›
  by (auto simp add: Process_eq_spec Ndet_projs GlobalDet_projs F_STOP D_STOP
      intro: is_processT8 is_processT6_TR_notin)

lemma GlobalDet_distrib_Ndet_right :
  ‹(□a ∈ A. P ⊓ Q a) = (if A = {} then STOP else P ⊓ (□a ∈ A. Q a))›
  by (subst (1 2) Ndet_commute) (fact GlobalDet_distrib_Ndet_left)

lemma Ndet_distrib_GlobalDet_left :
  ‹P ⊓ (□a ∈ A. Q a) = (if A = {} then P ⊓ STOP else □a ∈ A. P ⊓ Q a)›
  by (simp add: GlobalDet_distrib_Ndet_right)

lemma Ndet_distrib_GlobalDet_right :
  ‹(□a ∈ A. P a) ⊓ Q = (if A = {} then Q ⊓ STOP else □a ∈ A. P a ⊓ Q)›
  by (metis (no_types) GlobalDet_distrib_Ndet_left GlobalDet_empty Ndet_commute)


(*<*)
end
  (*>*)