Theory Non_Deterministic_CSP_Distributivity

(*<*)
―‹ ********************************************************************
 * 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       : Distributivity of non determinism
 *
 * 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.
 ******************************************************************************›
(*>*)

chapter‹Algebraic Rules of CSP›

section‹ The Non-Deterministic Distributivity ›

(*<*)
theory Non_Deterministic_CSP_Distributivity                                               
  imports Constant_Processes Deterministic_Choice Non_Deterministic_Choice
    Global_Non_Deterministic_Choice Sliding_Choice
    Multi_Deterministic_Prefix_Choice Multi_Non_Deterministic_Prefix_Choice
    Sequential_Composition Synchronization_Product Hiding Renaming
begin
  (*>*)

text ‹CSP operators are distributive over non deterministic choice.›

subsection ‹Global Distributivity›

lemma Mndetprefix_distrib_GlobalNdet :
  ‹B ≠ {} ⟹ (⊓a ∈ A → ⊓b ∈ B. P a b) = ⊓b ∈ B. ⊓a ∈ A → P a b›
  by (simp add: Mndetprefix_GlobalNdet GlobalNdet_sets_commute[of A] write0_GlobalNdet)

lemma Det_distrib_GlobalNdet_left :
  ‹P □ (⊓a∈A. Q a) = (if A = {} then P else ⊓a∈A. P □ Q a)›
  by (auto simp add: Process_eq_spec Det_projs GlobalNdet_projs
      intro: is_processT8 is_processT6_TR_notin)

corollary Det_distrib_GlobalNdet_right :
  ‹(⊓a∈A. P a) □ Q = (if A = {} then Q else ⊓a∈A. P a □ Q)›
  by (simp add: Det_commute Det_distrib_GlobalNdet_left)


lemma Sliding_distrib_GlobalNdet_left :
  ‹P ⊳ (⊓a∈A. Q a) = (if A = {} then P ⊓ STOP else ⊓a∈A. P ⊳ Q a)›
  by (auto simp add: Process_eq_spec GlobalNdet_projs
      Sliding_projs Ndet_projs STOP_projs)

lemma Sliding_distrib_GlobalNdet_right :
  ‹(⊓a∈A. P a) ⊳ Q = (if A = {} then Q else ⊓a∈A. P a ⊳ Q)›
  by (auto simp add: Process_eq_spec GlobalNdet_projs Sliding_projs)


lemma Sync_distrib_GlobalNdet_left : 
  ‹P ⟦S⟧ (⊓ a∈A. Q a) = (if A = {} then P ⟦S⟧ STOP else ⊓ a∈A. (P ⟦S⟧ Q a))›
proof (split if_split, intro conjI impI)
  show ‹A = {} ⟹ P ⟦S⟧ (⊓ a∈A. Q a) = P ⟦S⟧ STOP›
    by (simp add: GlobalNdet.abs_eq STOP.abs_eq)
next
  show ‹A ≠ {} ⟹ P ⟦S⟧ (⊓ a∈A. Q a) = ⊓ a∈A. (P ⟦S⟧ Q a)›
    by (simp add: Process_eq_spec Sync_projs F_GlobalNdet D_GlobalNdet T_GlobalNdet)
      (safe; simp; use front_tickFree_Nil in blast) ― ‹quicker than auto proof›
qed

corollary Sync_distrib_GlobalNdet_right : 
  ‹(⊓ a∈A. P a) ⟦S⟧ Q = (if A = {} then STOP ⟦S⟧ Q else ⊓ a∈A. (P a ⟦S⟧ Q))›
  by (simp add: Sync_commute Sync_distrib_GlobalNdet_left)

lemmas Inter_distrib_GlobalNdet_left = Sync_distrib_GlobalNdet_left[where S = ‹{}›]
  and Par_distrib_GlobalNdet_left = Sync_distrib_GlobalNdet_left[where S = UNIV]
  and Inter_distrib_GlobalNdet_right = Sync_distrib_GlobalNdet_right[where S = ‹{}›]
  and Par_distrib_GlobalNdet_right = Sync_distrib_GlobalNdet_right[where S = UNIV]


lemma Seq_distrib_GlobalNdet_left :
  ‹P ❙; ⊓ a∈A. Q a = (if A = {} then P ❙; STOP else ⊓ a∈A. (P ❙; Q a))›
  by (simp add: Process_eq_spec GlobalNdet_projs STOP_projs Seq_projs) blast

lemma Seq_distrib_GlobalNdet_right : ‹(⊓ a∈A. P a) ❙; Q = ⊓ a∈A. (P a ❙; Q)›
  by (simp add: Process_eq_spec GlobalNdet_projs STOP_projs Seq_projs)
    (safe; simp; blast) ― ‹quicker than auto proof›



lemma Renaming_distrib_GlobalNdet : ‹Renaming (⊓ a∈A. P a) f g = ⊓ a∈A. Renaming (P a) f g›
  by (simp add: Process_eq_spec Renaming_projs GlobalNdet_projs)
    (safe; simp; blast) ― ‹quicker than auto proof›


text ‹The \<^const>‹Hiding› operator does not distribute the \<^const>‹GlobalNdet› in general.
      We give a finite version derived from the binary version below.›



subsection ‹Binary Distributivity›

lemma Mndetprefix_distrib_Ndet :
  ‹(⊓a ∈ A → P a ⊓ Q a) = (⊓a ∈ A → P a) ⊓ (⊓a ∈ A → Q a)›
  by (simp add: Process_eq_spec Mndetprefix_projs Ndet_projs, safe) auto

lemma Det_distrib_Ndet_left : ‹P □ Q ⊓ R = (P □ Q) ⊓ (P □ R)›
  by (auto simp add: Process_eq_spec Det_projs Ndet_projs)

corollary Det_distrib_Ndet_right : ‹P ⊓ Q □ R = (P □ R) ⊓ (Q □ R)›
  by (simp add: Det_commute Det_distrib_Ndet_left)


lemma Ndet_distrib_Det_left : ‹P ⊓ (Q □ R) = P ⊓ Q □ P ⊓ R›
  by (auto simp add: Process_eq_spec Det_projs Ndet_projs
      is_processT8 is_processT6_TR_notin)

corollary Ndet_distrib_Det_right : ‹(P □ Q) ⊓ R = P ⊓ R □ Q ⊓ R›
  by (simp add: Ndet_commute Ndet_distrib_Det_left)


lemma Sliding_distrib_Ndet_left  : ‹P ⊳ (Q ⊓ R) = (P ⊳ Q) ⊓ (P ⊳ R)›
  and Sliding_distrib_Ndet_right : ‹(P ⊓ Q) ⊳ R = (P ⊳ R) ⊓ (Q ⊳ R)›
  by (auto simp add: Process_eq_spec Ndet_projs Sliding_projs)


lemma Sync_distrib_Ndet_left : ‹M ⟦S⟧ P ⊓ Q = (M ⟦S⟧ P) ⊓ (M ⟦S⟧ Q)›
  by (auto simp: Process_eq_spec, simp_all add: Sync_projs Ndet_projs) blast+

corollary Sync_distrib_Ndet_right : ‹P ⊓ Q ⟦S⟧ M = (P ⟦S⟧ M) ⊓ (Q ⟦S⟧ M)›
  by (metis Sync_commute Sync_distrib_Ndet_left)


lemma Seq_distrib_Ndet_left : ‹P ❙; Q ⊓ R = (P ❙; Q) ⊓ (P ❙; R)›
  by (fact Seq_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_distrib_Ndet_right : ‹P ⊓ Q ❙; R = (P ❙; R) ⊓ (Q ❙; R)›
  by (fact Seq_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])



lemma Renaming_distrib_Ndet : ‹Renaming (P ⊓ Q) f g = Renaming P f g ⊓ Renaming Q f g›
  by (fact Renaming_distrib_GlobalNdet[of ‹{0 :: nat, 1}›
        ‹λn. if n = 0 then P else if n = 1 then Q else undefined›,
        simplified GlobalNdet_distrib_unit_bis, simplified])


lemma Hiding_distrib_Ndet : ‹P ⊓ Q \ S = (P \ S) ⊓ (Q \ S)›
proof (subst Process_eq_spec_optimized, safe)
  fix s assume ‹s ∈ 𝒟 (P ⊓ Q \ S)›
  then obtain t u
    where * : ‹front_tickFree u› ‹tickFree t› ‹s = trace_hide t (ev ` S) @ u›
      ‹t ∈ 𝒟 (P ⊓ Q) ∨ (∃f. isInfHiddenRun f (P ⊓ Q) S ∧ t ∈ range f)›
    unfolding D_Hiding by blast
  from "*"(4) show ‹s ∈ 𝒟 ((P \ S) ⊓ (Q \ S))›
  proof (elim disjE exE)
    from "*"(1, 2) show ‹t ∈ 𝒟 (P ⊓ Q) ⟹ s ∈ 𝒟 ((P \ S) ⊓ (Q \ S))›
      unfolding D_Ndet D_Hiding "*"(3) by blast
  next
    fix f assume ‹isInfHiddenRun f (P ⊓ Q) S ∧ t ∈ range f›
    hence ‹isInfHiddenRun f P S ∨ isInfHiddenRun f Q S›
      by (simp add: T_Ndet) (meson is_processT3_TR linorder_le_cases strict_mono_less_eq)
    with "*"(1, 2) ‹isInfHiddenRun f (P ⊓ Q) S ∧ t ∈ range f›
    show ‹s ∈ 𝒟 ((P \ S) ⊓ (Q \ S))› unfolding D_Ndet D_Hiding "*"(3) by blast
  qed
next
  show ‹s ∈ 𝒟 ((P \ S) ⊓ (Q \ S)) ⟹ s ∈ 𝒟 (P ⊓ Q \ S)› for s
    unfolding Ndet_projs D_Hiding by blast
next
  assume same_div : ‹𝒟 (P ⊓ Q \ S) = 𝒟 ((P \ S) ⊓ (Q \ S))›
  fix s X assume ‹(s, X) ∈ ℱ (P ⊓ Q \ S)›
  then consider ‹s ∈ 𝒟 (P ⊓ Q \ S)›
    | t where ‹s = trace_hide t (ev ` S)› ‹(t, X ∪ ev ` S) ∈ ℱ (P ⊓ Q)›
    by (simp add: F_Hiding D_Hiding) blast
  thus ‹(s, X) ∈ ℱ ((P \ S) ⊓ (Q \ S))›
  proof cases
    from same_div D_F show ‹s ∈ 𝒟 (P ⊓ Q \ S) ⟹ (s, X) ∈ ℱ ((P \ S) ⊓ (Q \ S))› by blast
  next
    show ‹s = trace_hide t (ev ` S) ⟹ (t, X ∪ ev ` S) ∈ ℱ (P ⊓ Q)
          ⟹ (s, X) ∈ ℱ ((P \ S) ⊓ (Q \ S))› for t
      by (auto simp add: F_Ndet F_Hiding)
  qed
next
  show ‹(s, X) ∈ ℱ ((P \ S) ⊓ (Q \ S)) ⟹ (s, X) ∈ ℱ (P ⊓ Q \ S)› for s X
    unfolding Ndet_projs F_Hiding by blast
qed


lemma Hiding_distrib_finite_GlobalNdet :
  ‹finite A ⟹ (⊓a ∈ A. P a) \ S = ⊓a ∈ A. (P a \ S)›
proof (induct A rule: finite_induct)
  show ‹(⊓a ∈ {}. P a) \ S = ⊓a ∈ {}. (P a \ S)›
    by (auto simp add: Process_eq_spec GlobalNdet_projs
        Hiding_seqRun_projs seqRun_def)
next
  fix A a assume ‹finite A› ‹a ∉ A› and hyp : ‹(⊓a ∈ A. P a) \ S = ⊓a ∈ A. (P a \ S)›
  show ‹(⊓a ∈ insert a A. P a) \ S = ⊓a ∈ insert a A. (P a \ S)› (is ‹?lhs = ?rhs›)
  proof (cases ‹A = {}›)
    show ‹A = {} ⟹ ?lhs = ?rhs› by simp
  next
    assume ‹A ≠ {}›
    have ‹?lhs = P a ⊓ (⊓a ∈ A. P a) \ S›
      by (simp add: GlobalNdet_distrib_unit ‹A ≠ {}› ‹a ∉ A›)
    also have ‹… = (P a \ S) ⊓ ((⊓a ∈ A. P a) \ S)› by (simp add: Hiding_distrib_Ndet)
    also have ‹… = (P a \ S) ⊓ (⊓a ∈ A. (P a \ S))› by (simp add: hyp)
    also have ‹… = ?rhs› by (simp add: GlobalNdet_distrib_unit_bis ‹A ≠ {}› ‹a ∉ A›)
    finally show ‹?lhs = ?rhs› .
  qed
qed



text ‹For the \<^const>‹Mprefix› operator, we obviously do not have a
      conventional distributivity: \<^term>‹(⊓)› becomes \<^term>‹(□)›.›

lemma Mprefix_distrib_Ndet :
  ‹(□a ∈ A → P ⊓ Q) = (□a ∈ A → P) □ (□a ∈ A → Q)› (is ‹?lhs = ?rhs›)
proof (subst Process_eq_spec, safe)
  show ‹s ∈ 𝒟 ?lhs ⟹ s ∈ 𝒟 ?rhs›
    and ‹s ∈ 𝒟 ?rhs ⟹ s ∈ 𝒟 ?lhs› for s
    by (auto simp add: D_Det D_Ndet D_Mprefix)
next
  show ‹(s, X) ∈ ℱ ?lhs ⟹ (s, X) ∈ ℱ ?rhs› for s X
    by (cases s) (auto simp add: F_Mprefix F_Det F_Ndet)
next
  show ‹(s, X) ∈ ℱ ?rhs ⟹ (s, X) ∈ ℱ ?lhs› for s X
    by (auto simp add: F_Mprefix F_Det F_Ndet)
qed


(*<*)
end
  (*>*)