Theory CSP

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

theory CSP
  imports Process_Order CSP_Laws CSP_Induct
begin





section ‹Monotonicity›

lemma mono_Det_D[simp]: P D P'; S D S'  (P  S) D (P'  S')
  by (metis D_Det Un_mono divergence_refine_def)

lemma mono_Det_T[simp]: P T P'; S T S'  (P  S) T (P'  S')
  by (metis T_Det Un_mono trace_refine_def)

corollary mono_Det_DT[simp]: P DT P'; S DT S'  (P  S) DT (P'  S')
  by (simp_all add: trace_divergence_refine_def)

lemmas mono_Det_FD[simp]= mono_Det_FD[folded failure_divergence_refine_def]

―‹Deterministic choice monotony doesn't hold for F



lemma mono_Ndet_F_left[simp]: P F Q  (P  S) F Q
  by (simp add: F_Ndet failure_refine_def order_trans) 

lemma mono_Ndet_D_left[simp]: P D Q  (P  S) D Q
  by (simp add: D_Ndet divergence_refine_def order_trans) 

lemma mono_Ndet_T_left[simp]: P T Q  (P  S) T Q
  by (simp add: T_Ndet trace_refine_def order_trans) 

section ‹Monotonicity›

lemma mono_Ndet_F[simp]: P F P'; S F S'  (P  S) F (P'  S')
  by (metis F_Ndet Un_mono failure_refine_def) 

lemma mono_Ndet_D[simp]: P D P'; S D S'  (P  S) D (P'  S')
  by (metis D_Ndet Un_mono divergence_refine_def)

lemma mono_Ndet_T[simp]: P T P'; S T S'  (P  S) T (P'  S')
  by (metis T_Ndet Un_mono trace_refine_def) 


corollary mono_Ndet_DT[simp]: P DT P'; S DT S'  (P  S) DT (P'  S')
  by (auto simp add: trace_divergence_refine_def)

lemmas mono_Ndet_FD[simp]= mono_Ndet_FD[folded failure_divergence_refine_def]


corollary  mono_Ndet_DT_left[simp]: P DT Q  (P  S) DT Q
      and  mono_Ndet_F_right[simp]: P F Q  (S  P) F Q
      and  mono_Ndet_D_right[simp]: P D Q  (S  P) D Q
      and  mono_Ndet_T_right[simp]: P T Q  (S  P) T Q
      and mono_Ndet_DT_right[simp]: P DT Q  (S  P) DT Q
  by (simp_all add: trace_divergence_refine_def Ndet_commute) 
  

lemmas mono_Ndet_FD_left[simp] = mono_Ndet_FD_left[folded failure_divergence_refine_def]
   and mono_Ndet_FD_right[simp] = mono_Ndet_FD_right[folded failure_divergence_refine_def]

lemma mono_Ndet_Det_FD[simp]: (P  S) FD (P  S)
  by (metis Det_id failure_divergence_refine_def mono_Det_FD mono_Ndet_FD_left 
            mono_Ndet_FD_right order_refl) 


corollary  mono_Ndet_Det_F[simp]: (P  S) F (P  S)
      and  mono_Ndet_Det_D[simp]: (P  S) D (P  S)
      and  mono_Ndet_Det_T[simp]: (P  S) T (P  S)
      and mono_Ndet_Det_DT[simp]: (P  S) DT (P  S) 
  by (simp_all add: leFD_imp_leF leFD_imp_leD leF_imp_leT leD_leT_imp_leDT) 


lemma mono_Seq_F_right[simp]: S F S'  (P ; S) F (P ; S')
  by (auto simp: failure_refine_def F_Seq append_single_T_imp_tickFree)

lemma mono_Seq_D_right[simp]: S D S'  (P ; S) D (P ; S')
  by (auto simp: divergence_refine_def D_Seq)

lemma  mono_Seq_T_right[simp]: S T S'  (P ; S) T (P ; S')
  by (auto simp: trace_refine_def T_Seq append_single_T_imp_tickFree)

corollary mono_Seq_DT_right[simp]: S DT S'  (P ; S)  DT (P ; S')
  by (simp add: trace_divergence_refine_def)

lemma mono_Seq_DT_left[simp]: P DT P'  (P ; S)  DT (P' ; S)
  apply (auto simp: trace_divergence_refine_def divergence_refine_def trace_refine_def D_Seq T_Seq)
  by (metis (no_types, lifting) Nil_elem_T Process.F_T T_F append.right_neutral 
            is_processT5_S3 subset_eq) 

―‹left Sequence monotony doesn't hold for F, D and T

corollary mono_Seq_DT[simp]: P DT P'  S DT S'  (P ; S)  DT (P' ; S')
  using mono_Seq_DT_left mono_Seq_DT_right trans_DT by blast
  
lemmas mono_Seq_FD[simp]= mono_Seq_FD[folded failure_divergence_refine_def]


lemma mono_Mprefix_F[simp]: x  A. P x F Q x  Mprefix A P F Mprefix A Q
  by (auto simp: failure_refine_def F_Mprefix) blast+

lemma mono_Mprefix_D[simp]: x  A. P x D Q x  Mprefix A P D Mprefix A Q
  by (auto simp: divergence_refine_def D_Mprefix) blast+

lemma mono_Mprefix_T[simp]: x  A. P x T Q x  Mprefix A P T Mprefix A Q
  by (auto simp: trace_refine_def T_Mprefix)

corollary mono_Mprefix_DT[simp]: x  A. P x DT Q x  Mprefix A P DT Mprefix A Q
  by (simp add: trace_divergence_refine_def)

lemmas mono_Mprefix_FD[simp] = mono_Mprefix_FD[folded failure_divergence_refine_def]

lemma mono_Mprefix_DT_set[simp]: A  B  Mprefix B P DT Mprefix A P (* rename this in mono_Mprefix_D_subset ? *)
  by (auto simp add:T_Mprefix D_Mprefix trace_divergence_refine_def 
                    trace_refine_def divergence_refine_def)

corollary mono_Mprefix_D_set[simp]: A  B  Mprefix B P D Mprefix A P
      and mono_Mprefix_T_set[simp]: A  B  Mprefix B P T Mprefix A P
  by (simp_all add: leDT_imp_leD leDT_imp_leT)

―‹Mprefix set monotony doesn't hold for F and FD where it holds for deterministic choice›


lemma mono_Hiding_F[simp]: P F Q  (P \ A) F (Q \ A)
  apply(cases A = {}, simp_all add: Hiding_set_empty failure_refine_def F_Hiding, intro conjI, blast)
proof(subst (2) Un_commute, rule subsetI, rule UnCI, auto, goal_cases)
  case (1 b t u)
  then obtain a where a:a  A by blast
  define f where A: f = rec_nat t (λi t. t @ [ev a]) 
  hence AA: f (Suc i) = (f i) @ [ev a] for i by simp
  hence B: strict_mono f by (simp add:strict_mono_def lift_Suc_mono_less_iff)
  from A have C: t  range f by (metis (mono_tags, lifting) old.nat.simps(6) range_eqI)
  { fix i
    have f i  𝒟 Q  tickFree (f i)  trace_hide (f i) (ev ` A) = (trace_hide t (ev ` A))
    proof(induct i)
      case 0
      then show ?case by (simp add: 1(4) 1(7) A)
    next
      case (Suc i)
      then show ?case 
        apply (simp add:AA a) 
        using is_processT7[rule_format, of f i Q [ev a]] front_tickFree_single by blast 
    qed
  } 
  with B C have isInfHiddenRun f P A  t  range f 
    by (metis 1(1) D_T F_subset_imp_T_subset subsetD)
  with 1 show ?case by metis
next
  case (2 b u f x)
  then show ?case using F_subset_imp_T_subset by blast 
qed 

lemma mono_Hiding_T[simp]: P T Q  (P \ A) T (Q \ A)
  apply(cases A={}, simp add: Hiding_set_empty, 
                      simp add:trace_refine_def T_Hiding, intro conjI)
proof(goal_cases)
  case 1
  then show ?case
  proof(subst Un_commute, rule_tac subsetI, rule_tac UnCI, auto, goal_cases)
    case 11:(1 t a)
    hence tt: t  𝒯 P by (meson Process.F_T subset_eq) 
    with 11(1) inf_hidden[of A t P] obtain f where isInfHiddenRun f P A  t  range f by auto
    with 11(4)[rule_format, of t []] show ?case
      by (metis 11(1) tt append_Nil2 front_tickFree_Nil is_processT2_TR 
                nonTickFree_n_frontTickFree tick_T_F)
  qed
next
  case 2
  then show ?case
  proof(subst Un_commute, auto, goal_cases)
    case 21:(1 t u a)
    define f where A: f = rec_nat t (λi t. t @ [ev a]) 
    hence AA: f (Suc i) = (f i) @ [ev a] for i by simp
    hence B: strict_mono f by (simp add:strict_mono_def lift_Suc_mono_less_iff)
    from A have C: t  range f 
      by (metis (mono_tags, lifting) old.nat.simps(6) range_eqI)
    { fix i
      have f i  𝒟 Q  tickFree (f i)  trace_hide (f i) (ev ` A) = (trace_hide t (ev ` A))
      proof(induct i)
        case 0
        then show ?case by (simp add: 21(4) 21(7) A)
      next
        case (Suc i)
        then show ?case 
          apply (simp add:AA 21(6)) 
          using is_processT7[rule_format, of f i Q [ev a]] front_tickFree_single by blast 
      qed
    } 
    with B C have isInfHiddenRun f P A  t  range f by (metis 21(1) D_T subsetD)
    with 21 show ?case by metis
  next
    case 22:(2 b u f x)
    then show ?case by blast
  qed
qed

lemma mono_Hiding_DT[simp]: P DT Q  (P \ A) DT (Q \ A)
proof -
  assume as: P DT Q
  then have (P \ A) D (Q \ A)
    apply(auto simp:trace_divergence_refine_def divergence_refine_def 
                    trace_refine_def D_Hiding T_Hiding)
    by blast+
  with leDT_imp_leT[THEN mono_Hiding_T, OF as] show ?thesis by (simp add: trace_divergence_refine_def) 
qed

lemmas mono_Hiding_FD[simp] = mono_Hiding_FD[folded failure_divergence_refine_def]

―‹Obviously, Hide monotony doesn't hold for D


lemma mono_Sync_DT[simp]: P DT P'  Q DT Q'  (P  A  Q) DT (P'  A  Q')
  by (simp add:trace_divergence_refine_def divergence_refine_def trace_refine_def T_Sync D_Sync) 
     blast

lemmas mono_Sync_FD[simp] = mono_Sync_FD[folded failure_divergence_refine_def]

―‹Synchronization monotony doesn't hold for F, D and T


lemma mono_Mndetprefix_F[simp]: xA. P x F Q x  Mndetprefix A P F Mndetprefix A Q
  by (cases A = {}, auto simp: failure_refine_def F_Mndetprefix write0_def F_Mprefix) 

lemma mono_Mndetprefix_D[simp]: xA. P x D Q x  Mndetprefix A P D Mndetprefix A Q
  by (cases A = {}, auto simp: divergence_refine_def D_Mndetprefix write0_def D_Mprefix)

lemma mono_Mndetprefix_T[simp]: xA. P x T Q x  Mndetprefix A P T Mndetprefix A Q
  by (cases A = {}, auto simp: trace_refine_def T_Mndetprefix write0_def T_Mprefix)

corollary mono_Mndetprefix_DT[simp]: xA. P x DT Q x  Mndetprefix A P DT Mndetprefix A Q
  by (simp add: trace_divergence_refine_def)
  
lemmas mono_Mndetprefix_FD[simp] = mono_Mndetprefix_FD[folded failure_divergence_refine_def]

lemmas mono_Mndetprefix_FD_set[simp] = Mndetprefix_FD_subset[folded failure_divergence_refine_def]

corollary mono_Mndetprefix_F_set[simp] : A  {}  A  B  Mndetprefix B P F Mndetprefix A P
      and mono_Mndetprefix_D_set[simp] : A  B  Mndetprefix B P D  Mndetprefix A P
      and mono_Mndetprefix_T_set[simp] : A  B  Mndetprefix B P T  Mndetprefix A P
      and mono_Mndetprefix_DT_set[simp]: A  B  Mndetprefix B P DT Mndetprefix A P
  by (cases A = {}, simp_all add: leFD_imp_leF leFD_imp_leD leF_imp_leT leD_leT_imp_leDT)+

lemmas Mprefix_refines_Mndetprefix_FD[simp] = 
       Mprefix_refines_Mndetprefix[folded failure_divergence_refine_def]

corollary Mprefix_refines_Mndetprefix_F[simp] : Mndetprefix A P F  Mprefix A P
      and Mprefix_refines_Mndetprefix_D[simp] : Mndetprefix A P D  Mprefix A P
      and Mprefix_refines_Mndetprefix_T[simp] : Mndetprefix A P T  Mprefix A P
      and Mprefix_refines_Mndetprefix_DT[simp]: Mndetprefix A P DT Mprefix A P
  by (simp_all add: leFD_imp_leF leFD_imp_leD leF_imp_leT leD_leT_imp_leDT) 






lemma mono_read_FD[simp, elim]: "(x. P x FD Q x)  (c?x  (P x)) FD (c?x  (Q x))"
  by (simp add: read_def)

lemma mono_write_FD[simp, elim]: "(P FD Q)   (c!x  P) FD (c!x  Q)"
  by (simp add: write_def)

lemma mono_write0_FD[simp, elim]: "P FD Q  (a  P) FD (a  Q)"
  by (simp add: write0_def)

(* make this with ⊑DT and ⊑F ? *)
lemma mono_read_DT[simp, elim]: "(x. P x DT Q x)  (c?x  (P x)) DT (c?x  (Q x))"
  by (simp add: read_def)

lemma mono_write_DT[simp, elim]: "(P DT Q)   (c!x  P) DT (c!x  Q)"
  by (simp add: write_def)

lemma mono_write0_DT[simp, elim]: "P DT Q  (a  P) DT (a  Q)"
  by (simp add: write0_def)




lemma mono_Renaming_D: P D Q  Renaming P f D Renaming Q f
  unfolding divergence_refine_def D_Renaming by blast


lemma mono_Renaming_FD: P FD Q  Renaming P f FD Renaming Q f
  unfolding failure_divergence_refine_def le_ref_def
  apply (simp add: mono_Renaming_D[unfolded divergence_refine_def])
  unfolding F_Renaming D_Renaming by blast


lemma mono_Renaming_DT: P DT Q  Renaming P f DT Renaming Q f
  unfolding trace_divergence_refine_def 
  apply (simp add: mono_Renaming_D)
  unfolding trace_refine_def divergence_refine_def T_Renaming by blast




text ‹Some new and very useful results›

lemma Ndet_is_STOP_iff: P  Q = STOP  P = STOP  Q = STOP
  using Nil_subset_T by (simp add: STOP_iff_T T_Ndet, blast)

lemma Det_is_STOP_iff: P  Q = STOP  P = STOP  Q = STOP
  using Nil_subset_T by (simp add: STOP_iff_T T_Det, blast)


lemma Det_is_BOT_iff: P  Q =   P =   Q = 
  by (simp add: BOT_iff_D D_Det)

lemma Ndet_is_BOT_iff: P  Q =   P =   Q = 
  by (simp add: BOT_iff_D D_Ndet)

lemma Sync_is_BOT_iff: P S Q =   P =   Q = 
  by (rule HOL.sym, intro iffI, metis Sync_BOT Sync_commute)
     (use empty_setinterleaving in auto simp add: BOT_iff_D D_Sync)


lemma STOP_neq_BOT: STOP  
  by (simp add: D_STOP BOT_iff_D)

lemma SKIP_neq_BOT: SKIP  
  by (simp add: D_SKIP BOT_iff_D)


lemma Mprefix_neq_BOT: Mprefix A P  
  by (simp add: BOT_iff_D)

lemma Mndetprefix_neq_BOT: Mndetprefix A P  
  by (cases A = {}) (simp_all add: D_STOP BOT_iff_D D_Mndetprefix write0_def)


lemma STOP_T_iff: STOP T P  P = STOP
  by auto (metis Nil_elem_T STOP_iff_T empty_iff subset_singletonD trace_refine_def)

lemma STOP_F_iff: STOP F P  P = STOP
  by auto (metis Nil_elem_T STOP_iff_T empty_iff leF_imp_leT subset_singletonD trace_refine_def)

lemma STOP_FD_iff: STOP FD P  P = STOP
  using STOP_F_iff idem_FD leFD_imp_leF by blast

lemma SKIP_FD_iff: SKIP FD P  P = SKIP
  apply (subst Process_eq_spec, auto simp add: failure_divergence_refine_def le_ref_def F_SKIP D_SKIP subset_iff)
  by (metis F_T insertI1 is_processT5_S6 is_processT6_S2)
     (metis F_T append.left_neutral insertI1 is_processT5_S6 tick_T_F)

lemma SKIP_F_iff: SKIP F P  P = SKIP
  apply (subst Process_eq_spec, auto simp add: failure_refine_def le_ref_def F_SKIP D_SKIP subset_iff)
    apply (metis F_T insertI1 is_processT5_S6 is_processT6_S2)
   apply (metis F_T append.left_neutral insertI1 is_processT5_S6 tick_T_F)
  by (metis append_Nil insertI1 neq_Nil_conv process_charn)



lemma Seq_is_SKIP_iff: P ; Q = SKIP  P = SKIP  Q = SKIP
  apply (intro iffI, simp_all add: Seq_SKIP)
  apply (simp add: SKIP_F_iff[symmetric])
  unfolding failure_refine_def
proof (auto simp add: F_Seq F_SKIP D_Seq D_SKIP subset_iff intro: T_F, goal_cases)
  case (1 s X)
  thus ?case
    apply (cases tickFree s) 
     apply (erule_tac x = s in allE, 
            metis F_T append.right_neutral is_processT4_empty is_processT5_S4 process_charn)
    by (erule_tac x = butlast s in allE,
        metis F_T append.right_neutral append_butlast_last_id append_single_T_imp_tickFree
        last_snoc nonTickFree_n_frontTickFree non_tickFree_tick process_charn self_append_conv2)
next
  case (2 s X)
  thus ?case
    by (metis F_T append_Nil2 append_self_conv2 butlast_snoc front_tickFree_butlast
        insert_Diff insert_Diff_single nonTickFree_n_frontTickFree non_tickFree_tick process_charn)
qed (metis F_T append.left_neutral insertI1 insert_absorb2 is_processT5_S6 tickFree_Nil)+
 



― ‹The following result is very useful (especially for ProcOmata).›

lemma cont_process_rec: P = (μ X. f X)  cont f  P = f P by (simp add: def_cont_fix_eq)



end