Theory CSP_PTick_Monotonicities

(***********************************************************************************
 * 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
 ***********************************************************************************)


chapter ‹Monotonicity Properties›

(*<*)
theory CSP_PTick_Monotonicities
  imports Sequential_Composition_Generalized_Cont
    Synchronization_Product_Generalized_Cont
begin
  (*>*)


subsection ‹Sequential Composition›

lemma mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_FD : ‹P ⊑⇩_F⇩_D P' ⟹ (⋀r. Q r ⊑⇩_F⇩_D Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_F⇩_D P' ❙;⇩_✓ Q'›
proof (rule trans_FD[of _ ‹P' ❙;⇩_✓ Q›])
  show ‹P ⊑⇩_F⇩_D P' ⟹ (⋀r. Q r ⊑⇩_F⇩_D Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_F⇩_D P' ❙;⇩_✓ Q›
    unfolding refine_defs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs
    by (auto simp add: subset_iff T_F_spec[symmetric])
next
  show ‹P ⊑⇩_F⇩_D P' ⟹ (⋀r. Q r ⊑⇩_F⇩_D Q' r) ⟹ P' ❙;⇩_✓ Q ⊑⇩_F⇩_D P' ❙;⇩_✓ Q'›
    unfolding less_eq_process⇩_p⇩_t⇩_i⇩_c⇩_k_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs
    by (simp add: subset_iff T_F_spec[symmetric]) metis
qed

lemma mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_DT : ‹P ⊑⇩_D⇩_T P' ⟹ (⋀r. Q r ⊑⇩_D⇩_T Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_D⇩_T P' ❙;⇩_✓ Q'›
proof (rule trans_DT[of _ ‹P' ❙;⇩_✓ Q›])
  show ‹P ❙;⇩_✓ Q ⊑⇩_D⇩_T P' ❙;⇩_✓ Q› if ‹P ⊑⇩_D⇩_T P'›
  proof (rule trace_divergence_refine_optimizedI)
    from ‹P ⊑⇩_D⇩_T P'› show ‹s ∈ 𝒟 (P' ❙;⇩_✓ Q) ⟹ s ∈ 𝒟 (P ❙;⇩_✓ Q)› for s
      by (auto simp add: refine_defs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs)
  next
    from ‹P ⊑⇩_D⇩_T P'› show ‹s ∈ 𝒯 (P' ❙;⇩_✓ Q) ⟹ s ∈ 𝒯 (P ❙;⇩_✓ Q)› for s
      by (auto simp add: Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs refine_defs)
  qed
next
  show ‹(⋀r. Q r ⊑⇩_D⇩_T Q' r) ⟹ P' ❙;⇩_✓ Q ⊑⇩_D⇩_T P' ❙;⇩_✓ Q'›
    by (simp add: refine_defs Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast
qed


lemma mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_F_right : ‹(⋀r. Q r ⊑⇩_F Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_F P ❙;⇩_✓ Q'›
  by (auto simp add: failure_refine_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast

lemma mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_D_right : ‹(⋀r. Q r ⊑⇩_D Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_D P ❙;⇩_✓ Q'›
  by (simp add: divergence_refine_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast

lemma  mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_T_right : ‹(⋀r. Q r ⊑⇩_T Q' r) ⟹ P ❙;⇩_✓ Q ⊑⇩_T P ❙;⇩_✓ Q'›
  by (simp add: trace_refine_def Seq⇩_p⇩_t⇩_i⇩_c⇩_k_projs) blast

text ‹Left Sequence monotonicity doesn't hold for \<^term>‹(⊑⇩_F)›, \<^term>‹(⊑⇩_D)› and \<^term>‹(⊑⇩_T)›.›

lemmas monos_Seq⇩_p⇩_t⇩_i⇩_c⇩_k = mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_FD mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_DT
  mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_F_right mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_D_right mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k_T_right



subsection ‹Multiple Sequential Composition›

lemma mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹(⋀x r. x ∈ set L ⟹ P x r ⊑ Q x r) ⟹
   (SEQ⇩_✓ l ∈@ L. P l) r ⊑ (SEQ⇩_✓ l ∈@ L. Q l) r›
  by (induct L arbitrary: r, simp_all add: fun_belowI mono_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)

lemma mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k_FD :
  ‹(⋀x r. x ∈ set L ⟹ P x r ⊑⇩_F⇩_D Q x r) ⟹
   (SEQ⇩_✓ l ∈@ L. P l) r ⊑⇩_F⇩_D (SEQ⇩_✓ l ∈@ L. Q l) r›
  and mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k_DT :
  ‹(⋀x r. x ∈ set L ⟹ P x r ⊑⇩_D⇩_T Q x r) ⟹
   (SEQ⇩_✓ l ∈@ L. P l) r ⊑⇩_D⇩_T (SEQ⇩_✓ l ∈@ L. Q l) r›
  by (induct L arbitrary: r, simp_all add: monos_Seq⇩_p⇩_t⇩_i⇩_c⇩_k)

lemmas monos_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k =
  mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k_FD mono_MultiSeq⇩_p⇩_t⇩_i⇩_c⇩_k_FD



subsection ‹Synchronization Product›

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

lemma mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_DT :
  ‹P ⊑⇩_D⇩_T P' ⟹ Q ⊑⇩_D⇩_T Q' ⟹ P ⟦A⟧⇩_✓ Q ⊑⇩_D⇩_T P' ⟦A⟧⇩_✓ Q'›
  by (simp add: refine_defs T_Sync⇩_p⇩_t⇩_i⇩_c⇩_k D_Sync⇩_p⇩_t⇩_i⇩_c⇩_k) blast

lemma mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_FD : ‹P ⟦A⟧⇩_✓ Q ⊑⇩_F⇩_D P' ⟦A⟧⇩_✓ Q'›
  if ‹P ⊑⇩_F⇩_D P'› and ‹Q ⊑⇩_F⇩_D Q'›
proof -
  from ‹P ⊑⇩_F⇩_D P'› ‹Q ⊑⇩_F⇩_D Q'› have ‹P ⊑⇩_D⇩_T P'› ‹Q ⊑⇩_D⇩_T Q'›
    by (simp_all add: le_ref2T refine_defs)
  with mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_DT have ‹P ⟦A⟧⇩_✓ Q ⊑⇩_D⇩_T P' ⟦A⟧⇩_✓ Q'› by blast
  hence * : ‹P ⟦A⟧⇩_✓ Q ⊑⇩_D P' ⟦A⟧⇩_✓ Q'› by (simp add: leDT_imp_leD)
  show ‹P ⟦A⟧⇩_✓ Q ⊑⇩_F⇩_D P' ⟦A⟧⇩_✓ Q'›
  proof (rule leF_leD_imp_leFD[OF _ "*"],
      unfold failure_refine_def, safe)
    fix t X assume ‹(t, X) ∈ ℱ (P' ⟦A⟧⇩_✓ Q')›
    then consider ‹t ∈ 𝒟 (P' ⟦A⟧⇩_✓ Q')›
      | (fail) t_P t_Q X_P X_Q
      where ‹(t_P, X_P) ∈ ℱ P'› ‹(t_Q, X_Q) ∈ ℱ Q'›
        ‹t setinterleaves⇩_✓⇘tick_join⇙ ((t_P, t_Q), A)›
        ‹X ⊆ super_ref_Sync⇩_p⇩_t⇩_i⇩_c⇩_k tick_join X_P A X_Q›
      unfolding Sync⇩_p⇩_t⇩_i⇩_c⇩_k_projs by blast
    thus ‹(t, X) ∈ ℱ (P ⟦A⟧⇩_✓ Q)›
    proof cases
      show ‹t ∈ 𝒟 (P' ⟦A⟧⇩_✓ Q') ⟹ (t, X) ∈ ℱ (P ⟦A⟧⇩_✓ Q)›
        using "*" D_F unfolding divergence_refine_def by blast
    next
      case fail
      from fail(1, 2) ‹P ⊑⇩_F⇩_D P'› ‹Q ⊑⇩_F⇩_D Q'›
      have ‹(t_P, X_P) ∈ ℱ P› ‹(t_Q, X_Q) ∈ ℱ Q›
        unfolding refine_defs by auto
      with fail(3, 4) show ‹(t, X) ∈ ℱ (P ⟦A⟧⇩_✓ Q)›
        by (auto simp add: F_Sync⇩_p⇩_t⇩_i⇩_c⇩_k)
    qed
  qed
qed




lemmas monos_Sync⇩_p⇩_t⇩_i⇩_c⇩_k = mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_FD mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_DT


end


subsection ‹Multiple Synchronization Product›

lemma mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k :
  ‹(⋀l. l ∈ set L ⟹ P l ⊑ Q l) ⟹ ❙⟦S❙⟧⇩_✓ l ∈@ L. P l ⊑ ❙⟦S❙⟧⇩_✓ l ∈@ L. Q l›
  by (induct L rule: induct_list012)
    (simp_all add: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k mono_Renaming)

lemma mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_FD :
  ‹(⋀l. l ∈ set L ⟹ P l ⊑⇩_F⇩_D Q l) ⟹ ❙⟦S❙⟧⇩_✓ l ∈@ L. P l ⊑⇩_F⇩_D ❙⟦S❙⟧⇩_✓ l ∈@ L. Q l›
  by (induct L rule: induct_list012)
    (simp_all add: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_FD mono_Renaming_FD)


lemma mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_DT :
  ‹(⋀l. l ∈ set L ⟹ P l ⊑⇩_D⇩_T Q l) ⟹ ❙⟦S❙⟧⇩_✓ l ∈@ L. P l ⊑⇩_D⇩_T ❙⟦S❙⟧⇩_✓ l ∈@ L. Q l›
  by (induct L rule: induct_list012)
    (simp_all add: Sync⇩_R⇩_l⇩_i⇩_s⇩_t.mono_Sync⇩_p⇩_t⇩_i⇩_c⇩_k_DT mono_Renaming_DT)


lemmas monos_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k =
  mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_FD mono_MultiSync⇩_p⇩_t⇩_i⇩_c⇩_k_DT




(*<*)
end
  (*>*)