Theory CSP_Refinements

(*<*)
―‹ ********************************************************************
 * 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       : CSP refinements
 *
 * 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 ‹ The CSP Refinements ›

section ‹Definitions and first Properties›

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

subsection ‹Definitions›

definition trace_refine :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›              (infix ‹⊑T› 50)
  where ‹P ⊑T Q ≡ 𝒯 Q ⊆ 𝒯 P›

definition failure_refine :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›            (infix ‹⊑F› 50)
  where ‹P ⊑F Q ≡ ℱ Q ⊆ ℱ P›

definition divergence_refine :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›         (infix ‹⊑D› 50)
  where ‹P ⊑D Q ≡ 𝒟 Q ⊆ 𝒟 P›

abbreviation failure_divergence_refine :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool› (infix ‹⊑FD› 50)
  where ‹P ⊑FD Q ≡ P ≤ Q›


definition trace_divergence_refine :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›   (infix ‹⊑DT› 50)
  (* an experimental order considered also in our theories*)
  where ‹P ⊑DT Q ≡ P ⊑T Q ∧ P ⊑D Q›


lemma failure_divergence_refine_def : ‹P ⊑FD Q ⟷ P ⊑F Q ∧ P ⊑D Q›
  unfolding less_eq_processptick_def failure_refine_def divergence_refine_def by argo

lemmas refine_defs = failure_divergence_refine_def trace_divergence_refine_def
  failure_refine_def divergence_refine_def trace_refine_def


lemma failure_divergence_refineI :
  ‹⟦⋀s. s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P; ⋀s X. (s, X) ∈ ℱ Q ⟹ (s, X) ∈ ℱ P⟧ ⟹ P ⊑FD Q›
  by (auto simp add: refine_defs)

lemma failure_divergence_refine_optimizedI :
  ‹⟦⋀s. s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P; ⋀s X. (s, X) ∈ ℱ Q ⟹ 𝒟 Q ⊆ 𝒟 P ⟹ (s, X) ∈ ℱ P⟧ ⟹ P ⊑FD Q›
  by (simp add: failure_divergence_refineI subsetI)

lemma trace_divergence_refineI :
  ‹⟦⋀s. s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P; ⋀s. s ∈ 𝒯 Q ⟹ s ∈ 𝒯 P⟧ ⟹ P ⊑DT Q›
  by (auto simp add: refine_defs)

lemma trace_divergence_refine_optimizedI :
  ‹⟦⋀s. s ∈ 𝒟 Q ⟹ s ∈ 𝒟 P; ⋀s. s ∈ 𝒯 Q ⟹ 𝒟 Q ⊆ 𝒟 P ⟹ s ∈ 𝒯 P⟧ ⟹ P ⊑DT Q›
  by (simp add: trace_divergence_refineI subsetI)



subsection ‹Idempotency›

(* TODO: rename in ..._refl ? *)

lemma  idem_F[simp] : ‹P ⊑F P›
  and  idem_D[simp] : ‹P ⊑D P›
  and  idem_T[simp] : ‹P ⊑T P›
  and idem_FD[simp] : ‹P ⊑FD P›
  and idem_DT[simp] : ‹P ⊑DT P›
  by (simp_all add: refine_defs) 


subsection ‹Some obvious refinements›

lemma BOT_leF [simp] : ‹⊥ ⊑F Q›
  and BOT_leD [simp] : ‹⊥ ⊑D Q›
  and BOT_leT [simp] : ‹⊥ ⊑T Q›
  and BOT_leFD[simp] : ‹⊥ ⊑FD Q›
  and BOT_leDT[simp] : ‹⊥ ⊑DT Q›
  by (simp_all add: refine_defs le_approx_lemma_F
      le_approx_lemma_T le_approx1)



subsection ‹Antisymmetry›

lemma FD_antisym: ‹P ⊑FD Q ⟹ Q ⊑FD P ⟹ P = Q› by simp

lemma DT_antisym: ‹P ⊑DT Q ⟹ Q ⊑DT P ⟹ P = Q›
  apply (simp add: trace_divergence_refine_def)
  oops (* obviously false *)



  subsection ‹Transitivity›

lemma  trans_F : ‹P ⊑F Q ⟹ Q ⊑F S ⟹ P ⊑F S›
  and  trans_D : ‹P ⊑D Q ⟹ Q ⊑D S ⟹ P ⊑D S›
  and  trans_T : ‹P ⊑T Q ⟹ Q ⊑T S ⟹ P ⊑T S›
  and trans_FD : ‹P ⊑FD Q ⟹ Q ⊑FD S ⟹ P ⊑FD S›
  and trans_DT : ‹P ⊑DT Q ⟹ Q ⊑DT S ⟹ P ⊑DT S›
  by (auto simp add: failure_refine_def divergence_refine_def
      trace_refine_def trace_divergence_refine_def)



subsection ‹Relations between refinements›

lemma      leF_imp_leT : ‹P ⊑F Q ⟹ P ⊑T Q›
  and     leFD_imp_leF : ‹P ⊑FD Q ⟹ P ⊑F Q›
  and     leFD_imp_leD : ‹P ⊑FD Q ⟹ P ⊑D Q›
  and     leDT_imp_leD : ‹P ⊑DT Q ⟹ P ⊑D Q›
  and     leDT_imp_leT : ‹P ⊑DT Q ⟹ P ⊑T Q›
  and leF_leD_imp_leFD : ‹P ⊑F Q ⟹ P ⊑D Q ⟹ P ⊑FD Q›
  and leD_leT_imp_leDT : ‹P ⊑D Q ⟹ P ⊑T Q ⟹ P ⊑DT Q›
  by (simp_all add: failure_refine_def trace_refine_def divergence_refine_def
      trace_divergence_refine_def less_eq_processptick_def)
    (use T_F_spec in blast)



subsection ‹More obvious refinements›

lemma  leD_STOP[simp] : ‹P ⊑D STOP›
  and  leT_STOP[simp] : ‹P ⊑T STOP›
  and leDT_STOP[simp] : ‹P ⊑DT STOP›
  by (simp_all add: refine_defs T_STOP D_STOP)



subsection ‹Admissibility›

lemma le_F_adm [simp] : ‹adm (λx. u x ⊑F v x)› if ‹cont u› and ‹monofun v›
proof (unfold adm_def failure_refine_def, safe)
  fix Y s X assume * : ‹chain Y› ‹∀i. ℱ (v (Y i)) ⊆ ℱ (u (Y i))› ‹(s, X) ∈ ℱ (v (Lub Y))›
  have ‹v (Y i) ⊑ v (⨆i. Y i)› for i by (simp add: "*"(1) is_ub_thelub monofunE ‹monofun v›)
  with "*"(2) le_approx_lemma_F have ‹ℱ (v (⨆i. Y i)) ⊆ ℱ (u (Y i))› for i by blast
  with "*"(3) show ‹(s, X) ∈ ℱ (u (Lub Y))›
    by (auto simp add: ch2ch_cont ‹cont u› ‹chain Y› F_LUB limproc_is_thelub cont2contlubE)
qed


lemma le_T_adm [simp] : ‹adm (λx. u x ⊑T v x)› if ‹cont u› and ‹monofun v›
proof (unfold adm_def trace_refine_def, intro allI impI subsetI)
  fix Y s assume * : ‹chain Y› ‹∀i. 𝒯 (v (Y i)) ⊆ 𝒯 (u (Y i))› ‹s ∈ 𝒯 (v (Lub Y))›
  have ‹v (Y i) ⊑ v (⨆i. Y i)› for i by (simp add: "*"(1) is_ub_thelub monofunE ‹monofun v›)
  with "*"(2) le_approx_lemma_T have ‹𝒯 (v (⨆i. Y i)) ⊆ 𝒯 (u (Y i))› for i by blast
  with "*"(3) show ‹s ∈ 𝒯 (u (Lub Y))›
    by (auto simp add: ch2ch_cont ‹cont u› ‹chain Y› T_LUB limproc_is_thelub cont2contlubE)
qed


lemma le_D_adm [simp] : ‹adm (λx. u x ⊑D v x)› if ‹cont u› and ‹monofun v›
proof (unfold adm_def divergence_refine_def, intro allI impI subsetI)
  fix Y s assume * : ‹chain Y› ‹∀i. 𝒟 (v (Y i)) ⊆ 𝒟 (u (Y i))› ‹s ∈ 𝒟 (v (Lub Y))›
  have ‹v (Y i) ⊑ v (⨆i. Y i)› for i by (simp add: "*"(1) is_ub_thelub monofunE ‹monofun v›)
  with "*"(2) le_approx1 have ‹𝒟 (v (⨆i. Y i)) ⊆ 𝒟 (u (Y i))› for i by blast
  with "*"(3) show ‹s ∈ 𝒟 (u (Lub Y))›
    by (auto simp add: ch2ch_cont ‹cont u› ‹chain Y› D_LUB limproc_is_thelub cont2contlubE)
qed

declare le_FD_adm [simp]

thm le_FD_adm le_FD_adm_cont (* already proven *)


lemma le_DT_adm [simp] : ‹cont (u::('b::cpo) ⇒ ('a, 'r) processptick) ⟹ monofun v ⟹ adm(λx. u x ⊑DT v x)›
  using adm_conj[OF le_T_adm[of u v] le_D_adm[of u v]] by (simp add: trace_divergence_refine_def)


lemmas le_F_adm_cont[simp] =  le_F_adm[OF _ cont2mono]
  and  le_T_adm_cont[simp] =  le_T_adm[OF _ cont2mono]
  and  le_D_adm_cont[simp] =  le_D_adm[OF _ cont2mono]
  and le_DT_adm_cont[simp] = le_DT_adm[OF _ cont2mono]

(*<*)
end
  (*>*)