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 FD 60)
  where P FD Q  P  Q


definition trace_divergence_refine :: 'a process  'a process  bool   (infix DT 53)
  (* an experimental order considered also in our theories*)
  where P DT 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 FD P
  and idem_DT[simp]: P DT 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 FD Q  Q FD P  P = Q
  by (simp add: failure_divergence_refine_def)

lemma DT_antisym: P DT Q  Q DT 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 FD Q  Q FD S  P FD S
  and trans_DT: P DT Q  Q DT S  P DT 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 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: 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]:  FD Q
  and BOT_leDT[simp]:  DT Q
  by (simp_all add: leF_leD_imp_leFD leD_leT_imp_leDT)

lemma leDT_STOP[simp]: P DT 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 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)






end