Theory CSPM_Monotonies

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

section‹ Monotonies ›

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


subsection ‹The Throw Operator›

lemma mono_Throw_F_right :
  ‹(⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑⇩F Q' a) ⟹ P Θ a ∈ A. Q a ⊑⇩F P Θ a ∈ A. Q' a›
  unfolding failure_refine_def by (simp add: F_Throw subset_iff disjoint_iff)
    (metis events_of_memI in_set_conv_decomp)

lemma mono_Throw_T_right : 
  ‹(⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑⇩T Q' a) ⟹ P Θ a ∈ A. Q a ⊑⇩T P Θ a ∈ A. Q' a›
  unfolding trace_refine_def by (simp add: T_Throw subset_iff disjoint_iff)
    (metis events_of_memI in_set_conv_decomp)

lemma mono_Throw_D_right : 
  ‹(⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑⇩D Q' a) ⟹ P Θ a ∈ A. Q a ⊑⇩D P Θ a ∈ A. Q' a›
  unfolding divergence_refine_def by (simp add: D_Throw subset_iff disjoint_iff)
    (metis events_of_memI in_set_conv_decomp)

lemma mono_Throw_FD : ‹P Θ a ∈ A. Q a ⊑⇩F⇩D P' Θ a ∈ A. Q' a›
  if ‹P ⊑⇩F⇩D P'› and ‹⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑⇩F⇩D Q' a›
proof (rule trans_FD)
  from ‹P ⊑⇩F⇩D P'› show ‹P Θ a ∈ A. Q a ⊑⇩F⇩D P' Θ a ∈ A. Q a›
    by (simp add: refine_defs Throw_projs subset_iff, safe, simp_all flip: T_F_spec, blast)
next
  show ‹P' Θ a ∈ A. Q a ⊑⇩F⇩D P' Θ a ∈ A. Q' a›
    by (meson anti_mono_events_of_FD failure_divergence_refine_def
        mono_Throw_D_right mono_Throw_F_right subsetD that)
qed


lemma mono_Throw_DT : ‹P Θ a ∈ A. Q a ⊑⇩D⇩T P' Θ a ∈ A. Q' a›
  if ‹P ⊑⇩D⇩T P'› and ‹⋀a. a ∈ A ⟹ a ∈ α(P) ⟹ Q a ⊑⇩D⇩T Q' a›
proof (rule trans_DT)
  from ‹P ⊑⇩D⇩T P'› show ‹P Θ a ∈ A. Q a ⊑⇩D⇩T P' Θ a ∈ A. Q a›
    by (simp add: refine_defs Throw_projs subset_iff, safe, auto)
next
  show ‹P' Θ a ∈ A. Q a ⊑⇩D⇩T P' Θ a ∈ A. Q' a›
    by (meson anti_mono_events_of_DT leDT_imp_leD leDT_imp_leT leD_leT_imp_leDT
        mono_Throw_D_right mono_Throw_T_right subsetD that)
qed


lemmas monos_Throw = mono_Throw mono_Throw_FD mono_Throw_DT
  mono_Throw_F_right mono_Throw_D_right mono_Throw_T_right



subsection ‹The Interrupt Operator›

lemma mono_Interrupt_T: ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P △ Q ⊑⇩T P' △ Q'›
  unfolding trace_refine_def by (auto simp add: T_Interrupt)

lemma mono_Interrupt_D_right : ‹Q ⊑⇩D Q' ⟹ P △ Q ⊑⇩D P △ Q'›
  unfolding divergence_refine_def by (auto simp add: D_Interrupt) 

―‹We have no monotony, even partial, with \<^term>‹(⊑⇩F)›.›

lemma mono_Interrupt_FD:
  ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P △ Q ⊑⇩F⇩D P' △ Q'›
  unfolding failure_divergence_refine_def failure_refine_def divergence_refine_def
  by (simp add: D_Interrupt F_Interrupt, safe;
      metis [[metis_verbose = false]] F_subset_imp_T_subset subsetD)

lemma mono_Interrupt_DT:
  ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P △ Q ⊑⇩D⇩T P' △ Q'›
  unfolding trace_divergence_refine_def trace_refine_def divergence_refine_def
  by (auto simp add: T_Interrupt D_Interrupt subset_iff)


lemmas monos_Interrupt = mono_Interrupt mono_Interrupt_FD mono_Interrupt_DT
  mono_Interrupt_D_right mono_Interrupt_T



subsection ‹Global Deterministic Choice›

lemma mono_GlobalDet_DT : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D⇩T Q a) ⟹ (□a ∈ A. P a) ⊑⇩D⇩T (□a ∈ A. Q a)›
  and mono_GlobalDet_T  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩T Q a) ⟹ (□a ∈ A. P a) ⊑⇩T (□a ∈ A. Q a)›
  and mono_GlobalDet_D  : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩D Q a) ⟹ (□a ∈ A. P a) ⊑⇩D (□a ∈ A. Q a)›
  by (auto simp add: refine_defs GlobalDet_projs)

lemma mono_GlobalDet_FD : ‹(⋀a. a ∈ A ⟹ P a ⊑⇩F⇩D Q a) ⟹ (□a ∈ A. P a) ⊑⇩F⇩D (□a ∈ A. Q a)›
  by (simp add: refine_defs GlobalDet_projs subset_iff) (meson F_T T_F in_mono)

lemmas monos_GlobalDet = mono_GlobalDet mono_GlobalDet_FD mono_GlobalDet_DT
  mono_GlobalDet_T mono_GlobalDet_D

lemma GlobalNdet_FD_GlobalDet : ‹(⊓a ∈ A. P a) ⊑⇩F⇩D (□a ∈ A. P a)›
  and GlobalNdet_DT_GlobalDet : ‹(⊓a ∈ A. P a) ⊑⇩D⇩T (□a ∈ A. P a)›
  and GlobalNdet_F_GlobalDet  : ‹(⊓a ∈ A. P a) ⊑⇩F (□a ∈ A. P a)›
  and GlobalNdet_T_GlobalDet  : ‹(⊓a ∈ A. P a) ⊑⇩T (□a ∈ A. P a)›
  and GlobalNdet_D_GlobalDet  : ‹(⊓a ∈ A. P a) ⊑⇩D (□a ∈ A. P a)›
  by (simp_all add: refine_defs GlobalDet_projs GlobalNdet_projs subset_iff, safe)
    (blast, blast intro: is_processT8, metis append_Nil is_processT6_TR_notin)+

lemmas GlobalNdet_le_GlobalDet = GlobalNdet_FD_GlobalDet GlobalNdet_DT_GlobalDet
  GlobalNdet_F_GlobalDet GlobalNdet_T_GlobalDet GlobalNdet_D_GlobalDet



subsection ‹Multiple Synchronization Product›

lemma mono_MultiSync_FD :
  ‹(⋀m. m ∈# M ⟹ P m ⊑⇩F⇩D Q m) ⟹ (❙⟦S❙⟧ m ∈# M. P m) ⊑⇩F⇩D (❙⟦S❙⟧ m ∈# M. Q m)›
  and mono_MultiSync_DT :
  ‹(⋀m. m ∈# M ⟹ P m ⊑⇩D⇩T Q m) ⟹ (❙⟦S❙⟧ m ∈# M. P m) ⊑⇩D⇩T (❙⟦S❙⟧ m ∈# M. Q m)›
  by (cases ‹M = {#}›, simp, erule mset_induct_nonempty, simp_all add: monos_Sync)+

lemmas mono_MultiInter_FD = mono_MultiSync_FD[where S = ‹{}›]
  and mono_MultiInter_DT = mono_MultiSync_DT[where S = ‹{}›]
  and   mono_MultiPar_FD = mono_MultiSync_FD[where S = ‹UNIV›]
  and   mono_MultiPar_DT = mono_MultiSync_DT[where S = ‹UNIV›]

lemmas monos_MultiSync = mono_MultiSync mono_MultiSync_FD mono_MultiSync_DT
  and monos_MultiPar = mono_MultiPar mono_MultiPar_FD mono_MultiPar_DT
  and monos_MultiInter = mono_MultiInter mono_MultiInter_FD mono_MultiInter_DT

text ‹Monotony doesn't hold for \<^term>‹(⊑⇩F)›, \<^term>‹(⊑⇩T)› and \<^term>‹(⊑⇩D)›.›



subsection ‹Multiple Sequential Composition›

lemma mono_MultiSeq_FD :
  ‹(⋀x. x ∈ set L ⟹ P x ⊑⇩F⇩D Q x) ⟹ SEQ l ∈@ L. P l ⊑⇩F⇩D SEQ l ∈@ L. Q l›
  and mono_MultiSeq_DT :
  ‹(⋀x. x ∈ set L ⟹ P x ⊑⇩D⇩T Q x) ⟹ SEQ l ∈@ L. P l ⊑⇩D⇩T SEQ l ∈@ L. Q l›
  by (induct L rule: rev_induct, simp_all add: monos_Seq)

lemmas monos_MultiSeq = mono_MultiSeq mono_MultiSeq_FD  mono_MultiSeq_FD



(*<*)
end
  (*>*)