Theory FunSeriesInHOL-CSP_RS

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff.
 *
 * This file       : Examples Related to Numerical Series and State-based Modeling
 *
 * 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.
 ******************************************************************************›
(*>*)

chapter‹Annex: A Note on State-based Processes in HOL-CSP (Restriction Spaces)›

theory    "FunSeriesInHOL-CSP_RS"
  imports "HOL-CSP" "HOL.Transcendental" "GenFixrec-RS"
begin

text‹This section is intended to give an intuition to the power of HOL-CSP processes by a set 
of examples. In our view, it can be stated that HOL-CSP are a more powerful modeling instrument
for indefinite behavior than, for example, co-inductive definitions, since they posses a theory
of synchronisation and monadic sequential composition that co-inductively defined streams lack.
On the other hand, there is no denying that the entire machinery is more complex. 

This is the variant of the theory ▩‹FunSeriesInHOL-CSP› in which all processes are defined as
unique fixpoints of constructive functionals (restriction spaces, ‹υ›) instead of least fixpoints
of continuous functionals (HOLCF, ‹μ›). Uniqueness replaces fixpoint induction in proofs of
process equalities (see ‹parallel_exec_Join› below).
›

section‹The 'Random' Key-Generator›

subsection‹Example for the basic Construction with ‹υ››


abbreviation key_generator_fun :: ‹('α set ⇒ 'α process) ⇒ ('α set ⇒ 'α process)›
  where ‹key_generator_fun X A ≡ ⊓a ∈ A → X (A - {a})›

definition key_generator :: ‹'α set ⇒ 'α process› (‹KEY›)
  where   ‹key_generator ≡ υ X. (λ A. ⊓a ∈ A → X (A - {a}))›

lemma key_generator_fun_constructive[simp]: ‹constructive key_generator_fun›
  by simp

lemma key_generator_unfold: ‹KEY A = ⊓a ∈ A → KEY (A - {a})›
  unfolding key_generator_def by (subst restriction_fix_eq) simp_all


text‹Now, the process term‹KEY ℕ› denotes the set of all traces that enumerate the natural
numbers without repetition... ›

subsection‹Example in High-level Notation›

text‹The ‹Fixrec ... where ...› notation provided by the generic fixpoint-support package
has the same effect as the construction above:›

Fixrec [RS] keygen ::"'α set ⇒ 'α process" 
  where kg_rec :  "keygen A =  (⊓a ∈ A → keygen (A - {a}))"


section‹Cauchy-Series as Processes›

subsection‹The Construction in basic Steps (Again)›

text‹It is kind of fun - but also instructive wrt. the power and generality of the process type -
to see Cauchy-sequences of numerical approximations in the number system with base 10 as processes.
This shows that processes in HOL-CSP are not finite, not rational, but transcendent objects with
a non-enumerable cardinality.  
›

definition digits :: ‹real ⇒ int process› 
  where   ‹digits ≡ υ X. (λx. ⌊x⌋ → X ((frac x) * 10)) ›

lemma digits_unfold: ‹digits x = ⌊x⌋ → digits (frac x * 10)›
  unfolding digits_def by (subst restriction_fix_eq) simp_all

text‹ Note that the floor function ‹⌊x⌋› yields the largest integer smaller or equal ‹x›, while
‹frac x› returns the rest between ‹⌊x⌋› and ‹x›.

Now, the process term‹digits pi› enumerates the representation at base 10 of the
transcendental number ‹π›, so: ‹3 → 1 → 4 → 1 → 5 → 9 →  ...›, while
while term‹digits (exp (1::real))› does the same for the transcendental number ‹e›. 
While these two perfectly well-defined mathematical objects imported from the
theory‹HOL.Transcendental› theory have as such no computational content, their approximation
by a HOL-CSP process has. Although we do not yet have a code-generator that shows this... ;-)›

subsection‹The Example again in High-level Notation›

text‹The ‹Fixrec›-package supports this construction directly: ›
Fixrec [RS] digits' ::"real ⇒ int process" 
  where digits'_rec :  "digits' x = ⌊x⌋ → digits' (frac x * 10)"

section‹The Collatz-Function as Process›

text‹Note that the Collatz function is unknown to be terminating; a standard definition in HOL 
via the recursive function definitions such as @{command primrec} or  @{command fun} is therefore 
out of reach. This example shows, however, that it is perfectly possible to represent the Collatz 
process as a recursive HOL-CSP process, since HOL-CSP is built for modeling potentially 
non-terminating computations. ›

abbreviation Even where "Even ≡ Collect even"  ― ‹the set of even numbers›
abbreviation Odd where  "Odd ≡ Collect odd"     ― ‹the set of odd numbers›
abbreviation Div3 where "Div3 ≡ {x. x mod 3 = 0}"

text‹We use the deterministic choice to express a case-distinction:›

Fixrec [RS]  Collatz ::"nat ⇒ nat process" 
  where Collatz_rec :  "Collatz n =  (□x ∈ ({0, 1} ∩ {n}) → Skip)
                                   □ (□x ∈ ((Even - {0}) ∩ {n}) → Collatz (x div 2  ))
                                   □ (□x ∈ ((Odd  - {1}) ∩ {n}) → Collatz (3 * x + 1))"

section‹True Concurrent Evolution of States.›

text‹It is a common misconception of CSP that it can not handle "true-concurrent' computations 
given that its fundamental concept of ∗‹events›: They are "indivisible obervations on a specific 
time-point". However, the contrary is the case: Since HOL-CSP allows for modeling non-determinism
and potentially infinite states,  
true-concurrent calculations over non-overlapping parts of a state are possible
between synchronisation points. If portions of a state are overlapping and computations do not
agree --- so: races will occur --- then these situations are represented in HOL-CSP as deadlock. ›

Fixrec [RS]  TwosL :: ‹nat ⇒ (nat × nat) process›
  where TwosL_unfold: ‹TwosL n1 =  (□σ ∈ ({n1<..} ∩ Even) × UNIV → TwosL (fst σ))›

Fixrec [RS] ThreesR :: ‹nat ⇒ (nat × nat) process›
  where  ThreesR_unfold: ‹ThreesR n2 = (□σ ∈ UNIV × ({n2<..} ∩ Div3) → ThreesR (snd σ))›


text‹These two processes work on a state ‹σ›, consisting of a pair of two counters ‹n1› and ‹n2›.
While const‹TwosL› choses an even number larger than its current local state ‹n1›,  const‹ThreesR›
chooses a number devisable by three larger than its current local state ‹n2›. Putting these two
together via:

     @{term [indent=10, margin=60]‹TwosL 0 ⟦Id⟧  ThreesR 0›}

... where term‹Id› is the identity relation, this synchronization over these two processes 
calculate independently two values but have to agree on a joint state. A trace of this combined 
processes is,  for example:
 
     @{cartouche [indent=10, margin=60]‹(2,6) → (24,24) → (16,33) → ... ›}

Of course, this example is a bit simplistic since the the global state ‹σ=(n1,n2)› has a simple 
structure, the access to the global variables is distinct and the underlying choices are deter-
ministic, so to speak, ∗‹angelic›. An obvious generalization of this handling of the common state 
are algebraic lenses as provided by the theory ▩‹Optics› in the AFP. Wrt. to the choice, one might
model a more aggressive, i.e. ∗‹demonic› behaviour as follows: ›

Fixrec [RS] TwosL' :: ‹nat ⇒ (nat × nat) process›
  where TwosL'_unfold: ‹TwosL' n1 = (⊓σ ∈ ({n1<..} ∩ Even) × UNIV → TwosL' (fst σ))›

Fixrec [RS] ThreesR' :: ‹nat ⇒ (nat × nat) process›
  where ThreesR'_unfold: ‹ThreesR' n2 = (⊓σ ∈ UNIV × ({n2<..} ∩ Div3) → ThreesR' (snd σ))›

text‹The intersection may again be defined via:

     @{term [indent=10, margin=60]‹TwosL' 0 ⟦Id⟧ ThreesR' 0›} 

but the traces of this combined process will contain explicit deadlocks on all places
where an agreement could not be reached due to "ruthless behaviour" demonic processes that
chose deviant values from each other... Which means that races occurred. ›

text‹One might want to prove these facts, i.e. that the synchronized processes produce only
streams enjoying the conjunction of the devisability properties and the agreement is angelic 
or demonic. The handy recursive equations needed for this, e.g. @{thm [source] TwosL_unfold} 
and @{thm [source] ThreesR'_unfold}, are provided by the ‹Fixrec›-package.›

text‹Of course, we could use this modeling technique --- which is roughly similar to the conjunction
of two preconditions --- by adding a process that ensures that first and second component of 
the joint agree in their value, that is: 

     @{cartouche [indent=10, margin=60]‹(6,6) → (24,24) → (36,36) → ... ›}

We bind the combined process to the constant ‹Join›:
›

Fixrec [RS] Join :: ‹nat × nat ⇒ (nat × nat) process›
  where Join_unfold: ‹Join (n1, n2) = (□σ ∈ ({n1<..} ∩ Even) × ({n2<..} ∩ Div3) → Join σ)›

text‹And there we go: We state that const‹TwosL› and const‹ThreesR› in parallel composition
are the same as const‹Join›, which does these computations in one step. In restriction spaces,
no fixpoint induction is needed: the parallel composition satisfies the recursive equation of
const‹Join›, whose functional is constructive, hence has a unique fixpoint.›

lemma parallel_exec_Join: ‹(TwosL (fst σ) || ThreesR (snd σ)) = Join σ›
proof -
  let ?F = ‹λX. λ(n1, n2). □σ ∈ ({n1<..} ∩ Even) × ({n2<..} ∩ Div3) → X σ›
  let ?P = ‹λσ. TwosL (fst σ) || ThreesR (snd σ)›
  have eqP : ‹?F ?P = ?P›
  proof (rule ext)
    fix σ :: ‹nat × nat›
    obtain n1 n2 where σ : ‹σ = (n1, n2)› by (cases σ)
    have ‹?P (n1, n2) = (□σ ∈ ({n1<..} ∩ Even) × UNIV → TwosL (fst σ))
                      || (□σ ∈ UNIV × ({n2<..} ∩ Div3) → ThreesR (snd σ))›
      by (simp only: fst_conv snd_conv, subst TwosL_unfold, subst ThreesR_unfold, rule refl)
    also have ‹… = □σ ∈ (({n1<..} ∩ Even) × UNIV ∩ UNIV × ({n2<..} ∩ Div3))
                      → (TwosL (fst σ) || ThreesR (snd σ))›
      by (rule Mprefix_Par_Mprefix)
    also have ‹… = ?F ?P (n1, n2)› by (simp add: Times_Int_Times)
    finally show ‹?F ?P σ = ?P σ› by (simp only: σ)
  qed
  have constr : ‹constructive ?F› by (simp add: case_prod_beta)
  have ‹(υ X. ?F X) = ?P› using restriction_fix_unique[OF constr eqP] .
  hence ‹Join = ?P› by (simp add: Join_def Join_rec_def)
  thus ?thesis by metis
qed

text‹... which is set under the constraint as follows:

     term‹ Join σ || (υ X . (λσ. □σ∈Id → X σ)) σ ›

We refrain from a formal proof which will follow the lines of @{thm [source] parallel_exec_Join}.›

end