Theory Sliding

(*<*)
―‹ ******************************************************************** 
 * Project         : HOL-CSP_OpSem - Operational semantics for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : The Sliding operator
 *
 * Copyright (c) 2023 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‹ New Operators ›

text ‹Three operators of CSP has not been defined yet in \<^session>‹HOL-CSP› 
      (and not in \<^session>‹HOL-CSPM› either): Sliding, Interrupt and Throw.
      Since they are mentioned by Roscoe \<^cite>‹"Roscoe2010UnderstandingCS"› (and since 
      he provides operational laws for them too in \<^cite>‹"DBLP:journals/entcs/Roscoe15"›), 
      it would  be a shame not to include them in our work.
      
      We will therefore define them now before moving on to the construction
      of our correspondence between semantics.›


section‹ The Sliding Operator (also called Timeout)›

theory  Sliding
  imports "HOL-CSPM.CSPM"
begin


subsection ‹Definition›

definition Sliding :: ‹'α process ⇒ 'α process ⇒ 'α process› (infixl ‹⊳› 78)
  where ‹P ⊳ Q ≡ (P □ Q) ⊓ Q›

― ‹See if we want to define a MultiSliding operator like MultiSeq.›



subsection ‹Projections›

lemma F_Sliding:
  ‹ℱ (P ⊳ Q) = ℱ Q ∪ {(s, X). s ≠ [] ∧ (s, X) ∈ ℱ P ∨ 
                               s = [] ∧ (s ∈ 𝒟 P ∨ tick ∉ X ∧ [tick] ∈ 𝒯 P)}›
  by (auto simp add: Sliding_def F_Ndet F_Det NF_ND is_processT6_S2)

corollary ‹ℱ (Mprefix A P ⊳ Q) = ℱ Q ∪ {(s, X) ∈ ℱ (Mprefix A P). s ≠ []}›
  by (auto simp add: F_Sliding)

lemma D_Sliding: ‹𝒟 (P ⊳ Q) = 𝒟 P ∪ 𝒟 Q›
  by (simp add: Sliding_def D_Ndet D_Det)

lemma T_Sliding: ‹𝒯 (P ⊳ Q) = 𝒯 P ∪ 𝒯 Q›
  by (simp add: Sliding_def T_Ndet T_Det)



subsection ‹Monotony›

lemma mono_right_Sliding_F: ‹Q ⊑⇩F Q' ⟹ P ⊳ Q ⊑⇩F P ⊳ Q'›
  and mono_Sliding_D:  ‹P ⊑⇩D P' ⟹ Q ⊑⇩D Q' ⟹ P ⊳ Q ⊑⇩D P' ⊳ Q'›
  and mono_Sliding_T:  ‹P ⊑⇩T P' ⟹ Q ⊑⇩T Q' ⟹ P ⊳ Q ⊑⇩T P' ⊳ Q'›
  and mono_Sliding_FD: ‹P ⊑⇩F⇩D P' ⟹ Q ⊑⇩F⇩D Q' ⟹ P ⊳ Q ⊑⇩F⇩D P' ⊳ Q'›
  and mono_Sliding_DT: ‹P ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ P ⊳ Q ⊑⇩D⇩T P' ⊳ Q'›
  by (simp add: failure_refine_def F_Sliding subset_iff)
     (simp_all add: Sliding_def)



subsection ‹Properties›

lemma Sliding_id: ‹P ⊳ P = P›
  by (simp add: Det_id Ndet_id Sliding_def)

lemma STOP_Sliding: ‹STOP ⊳ P = P›
  unfolding Sliding_def by (simp add: Det_commute Det_STOP Ndet_id)


text ‹Of course, \<^term>‹P ⊳ STOP ≠ STOP› and \<^term>‹P ⊳ STOP ≠ P› in general.›
lemma ‹∃P. P ⊳ STOP ≠ STOP ∧ P ⊳ STOP ≠ P›
proof (intro exI)
  show ‹SKIP ⊳ STOP ≠ STOP ∧ SKIP ⊳ STOP ≠ SKIP›
    by (metis Det_STOP Ndet_commute SKIP_F_iff SKIP_Neq_STOP
            STOP_F_iff Sliding_def mono_Ndet_F_left)
qed
  

text ‹But we still have this result.›
lemma Sliding_is_STOP_iff: ‹P ⊳ Q = STOP ⟷ P = STOP ∧ Q = STOP›
  by (auto simp add: STOP_iff_T T_Sliding intro: Nil_elem_T)


lemma Sliding_STOP_Det: ‹(P ⊳ STOP) □ Q = P ⊳ Q›
  by (simp add: Det_STOP Det_commute Det_distrib Sliding_def)


lemma BOT_Sliding: ‹⊥ ⊳ P = ⊥›
  and Sliding_BOT: ‹P ⊳ ⊥ = ⊥›
  unfolding Sliding_def by (simp_all add: Det_commute Det_BOT Ndet_commute Ndet_BOT)

lemma Sliding_is_BOT_iff: ‹P ⊳ Q = ⊥ ⟷ P = ⊥ ∨ Q = ⊥›
  by (simp add: Det_is_BOT_iff Ndet_is_BOT_iff Sliding_def)


lemma Sliding_assoc: ‹P1 ⊳ P2 ⊳ P3 = P1 ⊳ (P2 ⊳ P3)›
  by (metis Det_assoc Det_commute Det_distrib Ndet_assoc
            Ndet_commute Ndet_distrib Ndet_id Sliding_def)


lemma SKIP_Sliding: ‹SKIP ⊳ P = P ⊓ SKIP›
  by (auto simp add: Sliding_def Process_eq_spec F_Ndet
                     F_Det T_SKIP D_Ndet D_Det F_SKIP D_SKIP NF_ND)

lemma Sliding_SKIP: ‹P ⊳ SKIP = P □ SKIP› 
  by (auto simp add: Sliding_def Process_eq_spec F_Ndet
                     F_Det T_SKIP D_Ndet D_Det F_SKIP D_SKIP)


lemma Sliding_Det: ‹(P ⊳ P') □ Q = P ⊳ P' □ Q›
  by (metis Det_assoc Det_commute Det_distrib Sliding_def)


lemma Sliding_Ndet: ‹(P ⊓ P') ⊳ Q = (P ⊳ Q) ⊓ (P' ⊳ Q)›
                    ‹P ⊳ (Q ⊓ Q') = (P ⊳ Q) ⊓ (P ⊳ Q')›
  by (auto simp add: Process_eq_spec F_Ndet D_Ndet T_Ndet F_Sliding D_Sliding)
  

lemma Renaming_Sliding:
  ‹Renaming (P ⊳ Q) f = Renaming P f ⊳ Renaming Q f›
  by (simp add: Renaming_Det Renaming_Ndet Sliding_def)


lemma events_Sliding: ‹events_of (P ⊳ Q) = events_of P ∪ events_of Q›
  unfolding Sliding_def by (simp add: events_of_def T_Det T_Ndet)



subsection ‹Continuity›

text ‹From the definition, continuity is obvious.›

lemma Sliding_cont[simp] : ‹cont f ⟹ cont g ⟹ cont (λx. f x ⊳ g x)›
  by (simp add: Sliding_def)


end