Theory Operational_Semantics_CSP_PTick_Laws

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


(*<*)
theory Operational_Semantics_CSP_PTick_Laws
  imports After_CSP_PTick_Laws
    Non_Deterministic_CSP_PTick_Distributivity
    "HOL-CSP_OpSem"
begin
  (*>*)


section ‹Small Steps Transitions›

subsection ‹Extension of the After Operator›

subsection ‹Sequential Composition›

locale AfterExtDuplicated_same_events = AfterExtDuplicated Ψα Ωα Ψβ Ωβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and Ψβ :: ‹[('a, 's) processptick, 'a] ⇒ ('a, 's) processptick›
    and Ωβ :: ‹[('a, 's) processptick, 's] ⇒ ('a, 's) processptick› 


sublocale AfterExtDuplicated_same_events ⊆ AfterDuplicated_same_events .
    ―‹Recovering @{thm [source] AfterDuplicated_same_events.After_Seqptick}›


context AfterExtDuplicated_same_events
begin 

notation Aftertickα.After (infixl ‹afterα› 86)
notation Aftertickβ.After (infixl ‹afterβ› 86)
notation Aftertickα.Aftertick (infixl ‹after✓α› 86)
notation Aftertickβ.Aftertick (infixl ‹after✓β› 86)


lemma Aftertick_Seqptick : 
  ‹(P ;✓ Q) after✓β e =
   (case e of ✓(r) ⇒ Ωβ (P ;✓ Q) r
            | ev a ⇒
      if ∀r. ✓(r) ∈ P0 ⟶ ev a ∉ (Q r)0
    then   if ev a ∈ P0
         then P after✓α ev a ;✓ Q else Ψβ (P ;✓ Q) a
         else   if ev a ∈ P0
              then (P after✓α ev a ;✓ Q) ⊓
                   (⊓r∈{r. ✓(r) ∈ P0 ∧ ev a ∈ (Q r)0}. Q r after✓β ev a)
              else ⊓r∈{r. ✓(r) ∈ P0 ∧ ev a ∈ (Q r)0}. Q r after✓β ev a)›
  by (auto simp add: Aftertickβ.Aftertick_def Aftertickα.Aftertick_def After_Seqptick split: eventptick.split)

end



subsubsection ‹Synchronization Product›

locale AfterExt_Syncptick_locale = Syncptick_locale tick_join +
  AfterExtlhs : AfterExt Ψlhs Ωlhs +
  AfterExtrhs : AfterExt Ψrhs Ωrhs +
  AfterExtptick : AfterExt Ψptick Ωptick
  for tick_join :: ‹'r ⇒ 's ⇒ 't option›
    and Ψlhs :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωlhs :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and Ψrhs :: ‹[('a, 's) processptick, 'a] ⇒ ('a, 's) processptick›
    and Ωrhs :: ‹[('a, 's) processptick, 's] ⇒ ('a, 's) processptick›
    and Ψptick :: ‹[('a, 't) processptick, 'a] ⇒ ('a, 't) processptick›
    and Ωptick :: ‹[('a, 't) processptick, 't] ⇒ ('a, 't) processptick›
begin

sublocale After_Syncptick_locale tick_join Ψlhs Ψrhs Ψptick by unfold_locales

sublocale AfterExt_Syncptick_locale_sym :
  AfterExt_Syncptick_locale ‹λs r. tick_join r s› Ψrhs Ωrhs Ψlhs Ωlhs Ψptick Ωptick
  by unfold_locales

(*
notation AfterExtlhs.After (infixl ‹afterlhs› 86)
notation AfterExtrhs.After (infixl ‹afterrhs› 86)
notation AfterExtptick.After (infixl ‹afterptick› 86)
*)
notation AfterExtlhs.Aftertick (infixl ‹after✓lhs› 86)
notation AfterExtrhs.Aftertick (infixl ‹after✓rhs› 86)
notation AfterExtptick.Aftertick (infixl ‹after✓ptick› 86)
  (* 
definition Ωptickrev :: ‹('a, 't) processptick ⇒ 't ⇒ ('a, 's × 'r) processptick›
  where ‹Ωptickrev P s_r ≡ TickSwap (Ωptick (TickSwap P) (case s_r of (s, r) ⇒ (r, s)))›

sublocale AfterExtptickrev : AfterExt Ψptickrev Ωptickrev .

notation AfterExtptickrev.Aftertick (infixl ‹after✓ptickrev› 86)

sublocale AfterExtptickDuplicated : AfterExtDuplicated Ψptick Ωptick Ψptickrev Ωptickrev .



lemma Aftertick_TickSwap :
  ‹TickSwap P after✓ptickrev e =
   (case e of ✓(s_r) ⇒ Ωptickrev (TickSwap P) s_r
              | ev a ⇒  if P = ⊥ then ⊥
                       else   if ev a ∈ P0
                            then TickSwap (P after✓ptick ev a)
                            else Ψptickrev (TickSwap P) a)›
  by (simp add: AfterExtptickrev.Aftertick_def AfterExtptick.Aftertick_def
      After.After_BOT split: eventptick.split)
      (simp add: After_TickSwap)


lemma TickSwap_Aftertick [simp] :
  ‹TickSwap (P after✓ptick e) = TickSwap P after✓ptickrev tick_swap e›
  by (cases e) (auto simp add: AfterExt.Aftertick_def Ωptickrev_def)

lemma TickSwap_is_Aftertick_iff [simp] :
  ‹TickSwap P = (Q after✓ptick e) ⟷ P = TickSwap Q after✓ptickrev tick_swap e›
  by (simp add: TickSwap_eq_iff_eq_TickSwap)
 *)

theorem Aftertick_Syncptick: 
  ‹(P ⟦S⟧✓ Q) after✓ptick e =
   (case e of ✓(r_s) ⇒ Ωptick (P ⟦S⟧✓ Q) r_s
            |  ev a ⇒ 
     if P = ⊥ ∨ Q = ⊥ then ⊥
    else   if ev a ∈ P0 ∧ ev a ∈ Q0
         then   if a ∈ S then P after✓lhs ev a ⟦S⟧✓ Q after✓rhs ev a
              else (P after✓lhs ev a ⟦S⟧✓ Q) ⊓ (P ⟦S⟧✓ Q after✓rhs ev a)
         else   if ev a ∈ P0 ∧ a ∉ S then P after✓lhs ev a ⟦S⟧✓ Q
              else   if ev a ∈ Q0 ∧ a ∉ S then P ⟦S⟧✓ Q after✓rhs ev a
                   else Ψptick (P ⟦S⟧✓ Q) a)›
  by (cases e) (simp_all add: AfterExt.Aftertick_def After_Syncptick)

end



subsection ‹Generic Operational Semantics as Locales›

subsubsection ‹Sequential Composition›

locale OpSemTransitionsDuplicated_same_events =
  OpSemTransitionsDuplicated Ψα Ωα τ_transα Ψβ Ωβ τ_transβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_transα :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹α↝τ› 50)
    and Ψβ :: ‹[('a, 's) processptick, 'a] ⇒ ('a, 's) processptick›
    and Ωβ :: ‹[('a, 's) processptick, 's] ⇒ ('a, 's) processptick›
    and τ_transβ :: ‹[('a, 's) processptick, ('a, 's) processptick] ⇒ bool› (infixl ‹β↝τ› 50)

sublocale OpSemTransitionsDuplicated_same_events ⊆ AfterExtDuplicated_same_events
  by unfold_locales 

context OpSemTransitionsDuplicated_same_events begin

notation OpSemTransitionsα.ev_trans   (‹_ α↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsα.tick_trans (‹_ α↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsβ.ev_trans   (‹_ β↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsβ.tick_trans (‹_ β↝✓⇘_⇙ _› [50, 3, 51] 50)

lemma τ_trans_SeqptickR: ‹P ;✓ Q β↝τ Q'› if ‹P α↝✓⇘r⇙ P'› and ‹Q r β↝τ Q'›
proof -
  from that(1) have ‹P ⊑FD SKIP r› 
    by (meson OpSemTransitionsα.exists_tick_trans_is_initial_tick initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹P = P ⊓ SKIP r› ..
  hence ‹P ;✓ Q = (P ;✓ Q) ⊓ (SKIP r ;✓ Q)› 
    by (metis Seqptick_distrib_Ndet_right)
  also have ‹… = (P ;✓ Q) ⊓ Q r› by simp
  also have ‹… β↝τ Q r› by (simp add: OpSemTransitionsβ.τ_trans_NdetR)
  finally show ‹P ;✓ Q β↝τ Q'› by (rule OpSemTransitionsβ.τ_trans_transitivity) (fact that(2))
qed

lemma ‹✓(r) ∈ P0 ⟹ Q r β↝⇘e⇙ Q' ⟹ P ;✓ Q β↝⇘e⇙ Q'› for P :: ‹('a, 'r) processptick›
  by (meson OpSemTransitionsβ.τ_trans_eq OpSemTransitionsβ.τ_trans_ev_trans
            τ_trans_SeqptickR OpSemTransitionsα.exists_tick_trans_is_initial_tick)


end



locale OpSemTransitionsSeqptick =
  OpSemTransitionsDuplicated_same_events Ψα Ωα τ_transα Ψβ Ωβ τ_transβ
  for Ψα :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωα :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_transα :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹α↝τ› 50)
    and Ψβ :: ‹[('a, 's) processptick, 'a] ⇒ ('a, 's) processptick›
    and Ωβ :: ‹[('a, 's) processptick, 's] ⇒ ('a, 's) processptick›
    and τ_transβ :: ‹[('a, 's) processptick, ('a, 's) processptick] ⇒ bool› (infixl ‹β↝τ› 50) +
  assumes τ_trans_SeqptickL : ‹P α↝τ P' ⟹ P ;✓ Q β↝τ P' ;✓ Q›
begin

lemma ev_trans_SeqptickL: ‹P α↝⇘e⇙ P' ⟹ P ;✓ Q β↝⇘e⇙ P' ;✓ Q›
  by (cases ‹P = ⊥›, solves ‹simp add: OpSemTransitionsβ.BOT_ev_trans_anything›)
    (auto simp add: OpSemTransitionsβ.ev_trans_def Aftertick_Seqptick initials_Seqptick
                    OpSemTransitionsα.ev_trans_def
             intro: OpSemTransitionsβ.τ_trans_NdetL OpSemTransitionsβ.τ_trans_transitivity τ_trans_SeqptickL)

lemmas Seqptick_OpSem_rules = τ_trans_SeqptickL ev_trans_SeqptickL τ_trans_SeqptickR


end


subsubsection ‹Synchronization Product›

locale OpSemTransitions_Syncptick_locale = Syncptick_locale ‹(⊗✓)› +
  OpSemTransitionslhs  : OpSemTransitions Ψlhs   Ωlhs   ‹(lhs↝τ)›  +
  OpSemTransitionsrhs  : OpSemTransitions Ψrhs   Ωrhs   ‹(rhs↝τ)›  +
  OpSemTransitionsptick : OpSemTransitions Ψptick Ωptick ‹(ptick↝τ)›
  for tick_join :: ‹'r ⇒ 's ⇒ 't option› (infixl ‹⊗✓› 100)
    and Ψlhs :: ‹[('a, 'r) processptick, 'a] ⇒ ('a, 'r) processptick›
    and Ωlhs :: ‹[('a, 'r) processptick, 'r] ⇒ ('a, 'r) processptick›
    and τ_translhs :: ‹[('a, 'r) processptick, ('a, 'r) processptick] ⇒ bool› (infixl ‹lhs↝τ› 50)
    and Ψrhs :: ‹[('a, 's) processptick, 'a] ⇒ ('a, 's) processptick›
    and Ωrhs :: ‹[('a, 's) processptick, 's] ⇒ ('a, 's) processptick›
    and τ_transrhs :: ‹[('a, 's) processptick, ('a, 's) processptick] ⇒ bool› (infixl ‹rhs↝τ› 50)
    and Ψptick :: ‹[('a, 't) processptick, 'a] ⇒ ('a, 't) processptick›
    and Ωptick :: ‹[('a, 't) processptick, 't] ⇒ ('a, 't) processptick›
    and τ_transptick :: ‹[('a, 't) processptick, ('a, 't) processptick] ⇒ bool› (infixl ‹ptick↝τ› 50) +
  assumes τ_trans_SyncptickL : ‹P lhs↝τ P' ⟹ P ⟦A⟧✓ Q ptick↝τ P' ⟦A⟧✓ Q›
    and τ_trans_SyncptickR : ‹Q rhs↝τ Q' ⟹ P ⟦A⟧✓ Q ptick↝τ P ⟦A⟧✓ Q'›
begin

sublocale AfterExt_Syncptick_locale by unfold_locales


sublocale OpSemTransitions_Syncptick_locale_sym :
  OpSemTransitions_Syncptick_locale
  ‹λs r. r ⊗✓ s› Ψrhs Ωrhs ‹(rhs↝τ)› Ψlhs Ωlhs ‹(lhs↝τ)› Ψptick Ωptick ‹(ptick↝τ)›
proof unfold_locales
  show ‹P rhs↝τ P' ⟹ P ⟦A⟧✓sym Q ptick↝τ P' ⟦A⟧✓sym Q› for P P' A Q
    by (simp add: Syncptick_sym τ_trans_SyncptickR)
next
  show ‹Q lhs↝τ Q' ⟹ P ⟦A⟧✓sym Q ptick↝τ P ⟦A⟧✓sym Q'› for Q Q' A P
    by (simp add: Syncptick_sym τ_trans_SyncptickL)
qed


notation OpSemTransitionslhs.ev_trans (‹_ lhs↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionslhs.tick_trans (‹_ lhs↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsrhs.ev_trans (‹_ rhs↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsrhs.tick_trans (‹_ rhs↝✓⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsptick.ev_trans (‹_ ptick↝⇘_⇙ _› [50, 3, 51] 50)
notation OpSemTransitionsptick.tick_trans (‹_ ptick↝✓⇘_⇙ _› [50, 3, 51] 50)


text ‹
We do not need the assumptions @{thm [source] τ_trans_SyncptickL τ_trans_SyncptickR}
for the three following lemmas.
›

lemma τ_trans_SKIP_SyncptickL :
  ‹P ⟦A⟧✓ Q ptick↝τ SKIP r ⟦A⟧✓ Q› if ‹P lhs↝✓⇘r⇙ P'›
proof -
  from that have ‹P ⊑FD SKIP r›
    by (simp add: OpSemTransitionslhs.tick_trans_def initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹P = P ⊓ SKIP r› ..
  hence ‹P ⟦A⟧✓ Q = (P ⟦A⟧✓ Q) ⊓ (SKIP r ⟦A⟧✓ Q)›
    by (metis Syncptick_distrib_Ndet_right)
  also have ‹… ptick↝τ SKIP r ⟦A⟧✓ Q›
    by (fact OpSemTransitionsptick.τ_trans_NdetR)
  finally show ‹P ⟦A⟧✓ Q ptick↝τ SKIP r ⟦A⟧✓ Q› .
qed

lemma τ_trans_SKIP_SyncptickR :
  ‹P ⟦A⟧✓ Q ptick↝τ P ⟦A⟧✓ SKIP s› if ‹Q rhs↝✓⇘s⇙ Q'›
proof -
  from that have ‹Q ⊑FD SKIP s›
    by (simp add: OpSemTransitionsrhs.tick_trans_def initial_tick_iff_FD_SKIP)
  with FD_iff_eq_Ndet have ‹Q = Q ⊓ SKIP s› ..
  hence ‹P ⟦A⟧✓ Q = (P ⟦A⟧✓ Q) ⊓ (P ⟦A⟧✓ SKIP s)›
    by (metis Syncptick_distrib_Ndet_left)
  also have ‹… ptick↝τ P ⟦A⟧✓ SKIP s›
    by (fact OpSemTransitionsptick.τ_trans_NdetR)
  finally show ‹P ⟦A⟧✓ Q ptick↝τ P ⟦A⟧✓ SKIP s› .
qed


lemma tick_trans_SKIP_Syncptick_SKIP:
  ‹r ⊗✓ s = Some r_s ⟹ SKIP r ⟦A⟧✓ SKIP s ptick↝✓⇘r_s⇙ Ωptick (SKIP r_s) r_s›
  by (simp add: OpSemTransitionsptick.SKIP_trans_tick_Ω_SKIP)


lemma ev_trans_SyncptickL :
  ‹a ∉ A ⟹ P lhs↝⇘a⇙ P' ⟹ P ⟦A⟧✓ Q ptick↝⇘a⇙ P' ⟦A⟧✓ Q›
  by (auto simp add: OpSemTransitionsptick.ev_trans_def Aftertick_Syncptick
                     initials_Syncptick OpSemTransitionslhs.ev_trans_def
              intro: OpSemTransitionsptick.BOT_τ_trans_anything OpSemTransitionsptick.τ_trans_NdetL
                     OpSemTransitionsptick.τ_trans_transitivity τ_trans_SyncptickL)


lemma ev_trans_SyncptickR :
  ‹a ∉ A ⟹ Q rhs↝⇘a⇙ Q' ⟹ P ⟦A⟧✓ Q ptick↝⇘a⇙ P ⟦A⟧✓ Q'›
  by (auto simp add: OpSemTransitionsptick.ev_trans_def Aftertick_Syncptick
                     initials_Syncptick OpSemTransitionsrhs.ev_trans_def
              intro: OpSemTransitionsptick.BOT_τ_trans_anything OpSemTransitionsptick.τ_trans_NdetR
                     OpSemTransitionsptick.τ_trans_transitivity τ_trans_SyncptickR)

lemma ev_trans_SyncptickLR :
  ‹a ∈ A ⟹ P lhs↝⇘a⇙ P' ⟹ Q rhs↝⇘a⇙ Q' ⟹ P ⟦A⟧✓ Q ptick↝⇘a⇙ P' ⟦A⟧✓ Q'›
  by (auto simp add: OpSemTransitionsptick.ev_trans_def OpSemTransitionslhs.ev_trans_def
                     OpSemTransitionsrhs.ev_trans_def Aftertick_Syncptick initials_Syncptick
              intro: OpSemTransitionsptick.BOT_τ_trans_anything
                     OpSemTransitionsptick.τ_trans_transitivity
                     τ_trans_SyncptickL τ_trans_SyncptickR)


lemmas Syncptick_OpSem_rules = τ_trans_SyncptickL τ_trans_SyncptickR
  ev_trans_SyncptickL ev_trans_SyncptickR
  ev_trans_SyncptickLR
  τ_trans_SKIP_SyncptickL τ_trans_SKIP_SyncptickR
  tick_trans_SKIP_Syncptick_SKIP

end



(*<*)
end
  (*>*)