Theory Process_Order

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye, Benoît Ballenghien
 *
 * This file       : A Normalization Theory
 *
 * Copyright (c) 2022 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 ‹ Refinements › (* find a better name *)

theory Process_Order
  imports Process Stop
begin


definition trace_refine :: ‹'a process ⇒ 'a process ⇒ bool›              (infix ‹⊑⇩T› 60)
  where ‹P ⊑⇩T Q ≡ 𝒯 Q ⊆ 𝒯 P›

definition failure_refine :: ‹'a process ⇒ 'a process ⇒ bool›            (infix ‹⊑⇩F› 60)
  where ‹P ⊑⇩F Q ≡ ℱ Q ⊆ ℱ P›

definition divergence_refine :: ‹'a process ⇒ 'a process ⇒ bool›         (infix ‹⊑⇩D› 53)
  where ‹P ⊑⇩D Q ≡ 𝒟 Q ⊆ 𝒟 P›

definition failure_divergence_refine :: ‹'a process ⇒ 'a process ⇒ bool› (infix ‹⊑⇩F⇩D› 60)
  where ‹P ⊑⇩F⇩D Q ≡ P ≤ Q›


definition trace_divergence_refine :: ‹'a process ⇒ 'a process ⇒ bool›   (infix ‹⊑⇩D⇩T› 53)
  (* an experimental order considered also in our theories*)
  where ‹P ⊑⇩D⇩T Q ≡ P ⊑⇩T Q ∧ P ⊑⇩D Q›


section ‹Idempotency›

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 ⊑⇩F⇩D P›
  and idem_DT[simp]: ‹P ⊑⇩D⇩T P›
  by (simp_all add: failure_refine_def divergence_refine_def trace_refine_def
                    failure_divergence_refine_def trace_divergence_refine_def) 


section ‹Some obvious refinements›

lemma BOT_leF[simp]: ‹⊥ ⊑⇩F Q›
  and BOT_leD[simp]: ‹⊥ ⊑⇩D Q›
  and BOT_leT[simp]: ‹⊥ ⊑⇩T Q›
  by (simp_all add: failure_refine_def le_approx_lemma_F trace_refine_def
                    le_approx1 divergence_refine_def le_approx_lemma_T)



section ‹Antisymmetry›

lemma FD_antisym: ‹P ⊑⇩F⇩D Q ⟹ Q ⊑⇩F⇩D P ⟹ P = Q›
  by (simp add: failure_divergence_refine_def)

lemma DT_antisym: ‹P ⊑⇩D⇩T Q ⟹ Q ⊑⇩D⇩T P ⟹ P = Q›
  apply (simp add: trace_divergence_refine_def)
  oops 



section ‹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 ⊑⇩F⇩D Q ⟹ Q ⊑⇩F⇩D S ⟹ P ⊑⇩F⇩D S›
  and trans_DT: ‹P ⊑⇩D⇩T Q ⟹ Q ⊑⇩D⇩T S ⟹ P ⊑⇩D⇩T S›
  by (meson failure_refine_def order_trans, meson divergence_refine_def order_trans,
      meson trace_refine_def order_trans, meson failure_divergence_refine_def order_trans,
      meson divergence_refine_def order_trans trace_divergence_refine_def trace_refine_def)



section ‹Relations between refinements›

lemma      leF_imp_leT: ‹P ⊑⇩F Q ⟹ P ⊑⇩T Q›
  and     leFD_imp_leF: ‹P ⊑⇩F⇩D Q ⟹ P ⊑⇩F Q›
  and     leFD_imp_leD: ‹P ⊑⇩F⇩D Q ⟹ P ⊑⇩D Q›
  and     leDT_imp_leD: ‹P ⊑⇩D⇩T Q ⟹ P ⊑⇩D Q›
  and     leDT_imp_leT: ‹P ⊑⇩D⇩T Q ⟹ P ⊑⇩T Q›
  and leF_leD_imp_leFD: ‹P ⊑⇩F Q ⟹ P ⊑⇩D Q ⟹ P ⊑⇩F⇩D Q›
  and leD_leT_imp_leDT: ‹P ⊑⇩D Q ⟹ P ⊑⇩T Q ⟹ P ⊑⇩D⇩T Q›
  by (simp_all add: F_subset_imp_T_subset failure_refine_def trace_refine_def divergence_refine_def
                    trace_divergence_refine_def  failure_divergence_refine_def le_ref_def)
 


section ‹More obvious refinements›

lemma BOT_leFD[simp]: ‹⊥ ⊑⇩F⇩D Q›
  and BOT_leDT[simp]: ‹⊥ ⊑⇩D⇩T Q›
  by (simp_all add: leF_leD_imp_leFD leD_leT_imp_leDT)

lemma leDT_STOP[simp]: ‹P ⊑⇩D⇩T STOP›
  by (simp add: D_STOP leD_leT_imp_leDT Nil_elem_T T_STOP divergence_refine_def trace_refine_def)

lemma leD_STOP[simp]: ‹P ⊑⇩D STOP›
  and leT_STOP[simp]: ‹P ⊑⇩T STOP›
  by (simp_all add: leDT_imp_leD leDT_imp_leT)



section ‹Admissibility›

lemma le_F_adm[simp]:  ‹cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑⇩F v x)›
proof(auto simp add:cont2contlubE adm_def failure_refine_def)
  fix Y a b
  assume 1: ‹cont u› 
     and 2: ‹monofun v› 
     and 3: ‹chain Y› 
     and 4: ‹∀i. ℱ (v (Y i)) ⊆ ℱ (u (Y i))› 
     and 5: ‹(a, b) ∈ ℱ (v (⨆x. Y x))›
  hence ‹v (Y i)  ⊑ v (⨆i. Y i)› for i by (simp add: is_ub_thelub monofunE)
  hence ‹ℱ (v (⨆i. Y i)) ⊆ ℱ (u (Y i))› for i using 4 le_approx_lemma_F by blast   
  then show ‹(a, b) ∈ ℱ (⨆i. u (Y i))›
    using F_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed

lemma le_T_adm[simp]: ‹cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑⇩T v x)›
proof(auto simp add:cont2contlubE adm_def trace_refine_def)
  fix Y x
  assume 1: ‹cont u› 
     and 2: ‹monofun v› 
     and 3: ‹chain Y› 
     and 4: ‹∀i. 𝒯 (v (Y i)) ⊆ 𝒯 (u (Y i))› 
     and 5: ‹x ∈ 𝒯 (v (⨆i. Y i))›
  hence ‹v (Y i)  ⊑ v (⨆i. Y i)› for i by (simp add: is_ub_thelub monofunE)
  hence ‹𝒯 (v (⨆i. Y i)) ⊆ 𝒯 (u (Y i))› for i using 4 le_approx_lemma_T by blast  
  then show ‹x ∈ 𝒯 (⨆i. u (Y i))›
    using T_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed

lemma le_D_adm[simp]: ‹cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑⇩D v x)›
proof(auto simp add:cont2contlubE adm_def divergence_refine_def)
  fix Y x
  assume 1: ‹cont u› 
     and 2: ‹monofun v› 
     and 3: ‹chain Y› 
     and 4: ‹∀i. 𝒟 (v (Y i)) ⊆ 𝒟 (u (Y i))› 
     and 5: ‹x ∈ 𝒟 (v (⨆i. Y i))›
  hence ‹v (Y i)  ⊑ v (⨆i. Y i)› for i by (simp add: is_ub_thelub monofunE)
  hence ‹𝒟 (v (⨆i. Y i)) ⊆ 𝒟 (u (Y i))› for i using 4 le_approx1 by blast  
  then show ‹x ∈ 𝒟 (⨆i. u (Y i))›
    using D_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed


lemmas le_FD_adm[simp] = le_adm[folded failure_divergence_refine_def]


lemma le_DT_adm[simp]: ‹cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑⇩D⇩T 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)






end