Theory Fixrec_HOLCF_CSPM

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - Seeing Processes as a Scott Space
 *
 * Author          : Benoît Ballenghien, Burkhart Wolff
 *
 * This file       : Conceptual tests of the HOLCF instance of Fixrec requiring HOL-CSPM 
 *
 * Copyright (c) 2025/26 Université Paris-Saclay, France
 ******************************************************************************›
(*>*)

chapter ‹The HOLCF Instance of ▩‹Fixrec› and the Operators of \<^session>‹HOL-CSPM››

theory Fixrec_HOLCF_CSPM
  imports "HOL-CSP.Fixrec_HOLCF" "HOL-CSPM"
begin

text ‹The tests of @{theory "HOL-CSP.Fixrec_HOLCF"} that involve operators of \<^session>‹HOL-CSPM›.›

text ‹Recursion through the continuation of the exception operator ‹Θ› (FDR's ‹[| A |>›),
also when the exception event is initial (as in the crash handling of Dali):›
Fixrec cr :: ‹int process› and cr' :: ‹int process›
  where cr_eq  : ‹cr  = ((1 → Skip) ||| (0 → Skip)) Θ a ∈ {0}. cr'›
  |     cr'_eq : ‹cr' = ((2 → Skip) ||| (0 → Skip)) Θ a ∈ {0}. cr'›

end