Theory Constant_Processes

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : Constant processes
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * 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‹ Constant Processes ›

(*<*)
theory     Constant_Processes
  imports    Process
begin 
  (*>*)

section‹The Undefined Process: \<^term>‹⊥››

text‹ This is the key result: @{term "⊥"} --- which we know to exist 
from the process instantiation --- can be explicitly written with its projections.
›

lemma F_BOT : ‹ℱ ⊥ = {(s :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k, X). ftF s}›
  and D_BOT : ‹𝒟 ⊥ = {d :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k. ftF d}›
  and T_BOT : ‹𝒯 ⊥ = {s :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k. ftF s}›
proof -
  define bot⇩0 :: ‹('a, 'r) process⇩0› where ‹bot⇩0 ≡ ({(s, X). ftF s}, {d. ftF d})›
  define bot :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k› where ‹bot ≡ process_of_process⇩0 bot⇩0›

  have ‹is_process bot⇩0›
    unfolding is_process_def bot⇩0_def
    by (simp add: FAILURES_def DIVERGENCES_def)
      (meson ftF_append_iff ftF_dw_closed)
  have F_bot : ‹ℱ bot = {(s, X). ftF s}›
    by (metis CollectI FAILURES_def Failures.rep_eq ‹is_process bot⇩0› 
        bot⇩0_def bot_def fst_eqD process_of_process⇩0_inverse)
  have D_bot : ‹𝒟 bot = {d. ftF d}›
    by (metis CollectI DIVERGENCES_def Divergences.rep_eq ‹is_process bot⇩0›
        bot⇩0_def bot_def process_of_process⇩0_inverse prod.sel(2))
  hence T_bot : ‹𝒯 bot = {s. ftF s}›
    by (metis D_T T_imp_ftF mem_Collect_eq subsetI subset_Un_eq sup.orderE)
  have ‹bot = ⊥›
    by (metis (no_types, opaque_lifting) Process_eq_spec is_processT2
        is_processT8 le_approxD(1) mem_Collect_eq minimal subrelI
        subset_antisym subset_eq D_bot)
  with F_bot D_bot T_bot
  show ‹ℱ ⊥ = {(s :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k, X). ftF s}›
    ‹𝒟 ⊥ = {d :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k. ftF d}›
    ‹𝒯 ⊥ = {s :: ('a, 'r) trace⇩p⇩t⇩i⇩c⇩k. ftF s}› by simp_all
qed

lemma D⇩m⇩i⇩n_BOT : ‹𝒟⇩m⇩i⇩n ⊥ = {[]}›
  by (simp add: Divergences⇩m⇩i⇩n_def D_BOT min_elems_Collect_ftF_is_singl_Nil)

lemmas BOT_projs = F_BOT D_BOT T_BOT D⇩m⇩i⇩n_BOT


lemma BOT_iff_Nil_D : ‹P = ⊥ ⟷ [] ∈ 𝒟 P›
proof (rule iffI)
  show ‹P = ⊥ ⟹ [] ∈ 𝒟 P› by (simp add: D_BOT)
next
  show ‹P = ⊥› if ‹[] ∈ 𝒟 P›
  proof (subst Process_eq_spec_optimized, safe)
    show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 ⊥› for s by (simp add: D_BOT D_imp_ftF)
  next
    show ‹s ∈ 𝒟 ⊥ ⟹ s ∈ 𝒟 P› for s
      by (metis ‹[] ∈ 𝒟 P› append_Nil process_charn tF_Nil)
  next
    show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ ⊥› for s X
      using le_approx_lemma_F by blast
  next
    show ‹𝒟 P = 𝒟 ⊥ ⟹ (s, X) ∈ ℱ ⊥ ⟹ (s, X) ∈ ℱ P› for s X
      using D_BOT F_T T_BOT is_processT8 by blast
  qed
qed

lemma Divergences⇩m⇩i⇩n_def_bis : ‹𝒟⇩m⇩i⇩n P = (if P = ⊥ then {[]} else {t ∈ 𝒟 P. butlast t ∉ 𝒟 P})›
  by (auto simp add: D⇩m⇩i⇩n_BOT intro: D⇩m⇩i⇩n_memI D⇩m⇩i⇩n_D)
    (metis BOT_iff_Nil_D D⇩m⇩i⇩n_D Divergences⇩m⇩i⇩n_def Prefix_Order.prefixI
      append_self_conv min_elems_no_list_set_list_set snoc_eq_iff_butlast)

lemma BOT_iff_tick_D : ‹P = ⊥ ⟷ (∃r. [✓(r)] ∈ 𝒟 P)›
  by (metis BOT_iff_Nil_D D_BOT ftF_single is_processT9_tick mem_Collect_eq)



section‹The SKIP Process›

text ‹In this new parameterized version, the SKIP process is of course also parameterized.›

lift_definition SKIP :: ‹'r ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  is ‹λr. ({([], X)| X. ✓(r) ∉ X} ∪ {(s, X). s = [✓(r)]}, {})›
  unfolding is_process_def FAILURES_def DIVERGENCES_def
  by (auto simp add: append_eq_Cons_conv)

abbreviation SKIP_unit :: ‹'a process› (‹Skip›) where ‹Skip ≡ SKIP ()›


lemma F_SKIP :
  ‹ℱ (SKIP r) = {([], X)| X. ✓(r) ∉ X} ∪ {(s, X). s = [✓(r)]}›
  by (simp add: FAILURES_def Failures.rep_eq SKIP.rep_eq)

lemma D_SKIP : ‹𝒟 (SKIP r) = {}›
  by (simp add: DIVERGENCES_def Divergences.rep_eq SKIP.rep_eq)

lemma T_SKIP : ‹𝒯 (SKIP r) = {[], [✓(r)]}›
  by (auto simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_SKIP)

lemma D⇩m⇩i⇩n_SKIP : ‹𝒟⇩m⇩i⇩n (SKIP r) = {}›
  by (simp_all add: Divergences⇩m⇩i⇩n_def D_SKIP)

lemmas SKIP_projs = F_SKIP D_SKIP T_SKIP D⇩m⇩i⇩n_SKIP


lemma inj_SKIP : ‹inj SKIP›
  by (rule injI, simp add: Process_eq_spec F_SKIP) blast

lemma SKIP_eq_SKIP_iff [simp] : ‹SKIP r = SKIP s ⟷ r = s›
  by (meson injD inj_SKIP)



section‹ The STOP Process ›

lift_definition STOP :: ‹('a, 'r) process⇩p⇩t⇩i⇩c⇩k›
  is ‹({(s, X). s = []}, {})›
  unfolding is_process_def FAILURES_def DIVERGENCES_def by simp


lemma F_STOP : ‹ℱ STOP = {(s, X). s = []}›
  by (simp add: FAILURES_def Failures.rep_eq STOP.rep_eq)

lemma D_STOP : ‹𝒟 STOP = {}›
  by (simp add: DIVERGENCES_def Divergences.rep_eq STOP.rep_eq)

lemma T_STOP : ‹𝒯 STOP = {[]}›
  by (simp add: Traces.rep_eq TRACES_def Failures.rep_eq[symmetric] F_STOP)

lemma D⇩m⇩i⇩n_STOP : ‹𝒟⇩m⇩i⇩n STOP = {}›
  by (simp_all add: Divergences⇩m⇩i⇩n_def D_STOP)

lemmas STOP_projs = F_STOP D_STOP T_STOP D⇩m⇩i⇩n_STOP


lemma STOP_iff_T : ‹P = STOP ⟷ 𝒯 P = {[]}›
proof (rule iffI)
  show ‹P = STOP ⟹ 𝒯 P = {[]}› by (simp add: T_STOP)
next
  assume ‹𝒯 P = {[]}›
  show ‹P = STOP›
  proof (subst Process_eq_spec, safe)
    show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 STOP› for s
      by (metis D_T ‹𝒯 P = {[]}› ftF_single not_Cons_self
          process_charn self_append_conv2 singletonD tF_Nil)
  next
    show ‹s ∈ 𝒟 STOP ⟹ s ∈ 𝒟 P› for s by (simp add: D_STOP)
  next
    show ‹(s, X) ∈ ℱ P ⟹ (s, X) ∈ ℱ STOP› for s X
      using F_STOP F_T ‹𝒯 P = {[]}› by blast
  next
    show ‹(s, X) ∈ ℱ STOP ⟹ (s, X) ∈ ℱ P› for s X
      by (metis F_T T_STOP ‹𝒯 P = {[]}› is_processT5_S7 singletonD snoc_eq_iff_butlast)
  qed
qed



section ‹The Guard Operator›

text ‹New in Isabelle26.›

definition Guard :: ‹bool ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k ⇒ ('a, 'r) process⇩p⇩t⇩i⇩c⇩k › (infixl ‹❙&› 84)
  where ‹b ❙& P ≡ if b then P else STOP›


lemma Guard_True  [simp] : ‹True ❙& P = P›
  and Guard_False [simp] : ‹False ❙& P = STOP›
  and Guard_STOP  [simp] : ‹b ❙& STOP = STOP›
  and Guard_Guard [simp] : ‹b ❙& (b' ❙& P) = (b ∧ b') ❙& P›
  by (simp_all add: Guard_def)


lemma Guard_cont [simp] : ‹cont P ⟹ cont (λx. b ❙& P x)›
  by (simp add: Guard_def)


(*<*)
end
  (*>*)