Theory CSP_PTick_Introduction

(***********************************************************************************
 * 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 CSP_PTick_Introduction
  imports "HOL-CSP"
begin
  (*>*)

chapter ‹Introduction›

section ‹Motivations›

text ‹
Recently, the question arose whether \<^session>‹HOL-CSP› could accommodate
a parameterized notion of termination.⁋‹This idea was sparked by an innocent remark
from Simon Foster, which we later explored in depth.›
The idea is very simple: replace at the very beginning of the formalization
@{theory_text [display] ‹datatype 'a event = ev 'a | tick (‹✓›)›}
(isomorphic to option type) by
@{theory_text [display] ‹datatype ('a, 'r) event⇩p⇩t⇩i⇩c⇩k = ev 'a | tick 'r (‹✓'(_')›)›}
(isomorphic to sum type), so that the explicit termination event carries a return value.
›


text ‹
Certain definitions must therefore be adapted
(mainly by replacing \<^term>‹✓› with \<^term>‹range tick›).
For example, a trace \<^term>‹t› was said to be tick-free if \<^term>‹✓ ∉ set t›.
In this new setup, such a trace instead satisfies @{thm (rhs) tickFree_def[of t]}.
Surprisingly, once these few intuitive adjustments have been made,
most of the existing Isar proofs remain valid with little to no modification.
This generalization has already been carried out, and the AFP entries for
\<^session>‹HOL-CSP›, \<^session>‹HOL-CSPM›, and \<^session>‹HOL-CSP_OpSem›
have all been updated accordingly \<^cite>‹"HOL-CSP-AFP" and "HOL-CSPM-AFP" and "HOL-CSP_OpSem-AFP"›.
More recently, \<^session>‹HOL-CSP_RS› \<^cite>‹"HOL-CSP_RS-AFP"› has been added as well.
However, two operators do not behave as satisfactorily as one might hope.
›

text ‹
Firstly, sequential composition no longer admits \<^const>‹SKIP› as a neutral element.
In the classical theory, we have @{thm SKIP_Seq[of ‹()› P]} and @{thm Seq_SKIP[of P]}.
But in the generalized setting, \<^const>‹SKIP› carries a value and
if the first law can still be adapted and proven: @{thm SKIP_Seq[of r P]},
the second one only holds when the return type is \<^typ>‹unit›
(which amounts to ignoring the generalization).
From a broader perspective, one would in fact like the right-hand process
to depend on the return value of the left-hand process,
which is not the case in the current framework.
›



text ‹
Secondly, the synchronization product does not properly support synchronized termination.
Classically, we have
\<^term>‹Skip ⟦S⟧ Skip = Skip›, adapted in the last version of \<^session>‹HOL-CSP›
as @{thm SKIP_Sync_SKIP[of r A s]}.
When restricted to \<^typ>‹'a process› (which is \<^typ>‹('a, unit) process⇩p⇩t⇩i⇩c⇩k›) the behavior is fine,
but with general return values deadlocks may occur.
One would rather expect a law like ‹SKIP r ⟦A⟧ SKIP s = SKIP (r, s)›,
yet defining such an operator raises non-trivial technical challenges.
›

text ‹
In this entry, we propose generalized definitions for
sequential composition and synchronization product
that not only respect the invariant \<^const>‹is_process›
but also fulfill the expectations outlined above.
Beyond this substantial work, we establish algebraic
and operational properties of these operators,
as well as the lemmas required for fixed-point reasoning.
In particular, it can be pointed out that the resulting
sequential composition operator fulfills the laws of a monad.
›


section‹The Global Architecture of \<^session>‹HOL-CSP_PTick››

text‹
\begin{figure}[ht]
  \centering
  \includegraphics[width=\textwidth]{session_graph.pdf}
	\caption{The overall architecture}
	\label{fig:fig1}
\end{figure}
›

text ‹
Our formalization attempts to take full advantage of parallelization,
explaining the shape of the session graph shown in \autoref{fig:fig1}.
›


(*<*)
end
  (*>*)