Theory CSP

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye, Benoît Ballenghien, Catherine Dubois
 *
 * 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‹ Generalisation of Normalisation of Non Deterministic CSP Processes ›

theory CSP
  imports CSP_Laws Process_Order (*Induction*)
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 ⊑⇩D⇩T P'; S ⊑⇩D⇩T S'⟧ ⟹ (P □ S) ⊑⇩D⇩T (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 ⊑⇩D⇩T P'; S ⊑⇩D⇩T S'⟧ ⟹ (P ⊓ S) ⊑⇩D⇩T (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 ⊑⇩D⇩T Q ⟹ (P ⊓ S) ⊑⇩D⇩T 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 ⊑⇩D⇩T Q ⟹ (S ⊓ P) ⊑⇩D⇩T 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) ⊑⇩F⇩D (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) ⊑⇩D⇩T (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')›
  apply (auto simp: failure_refine_def F_Seq append_single_T_imp_tickFree)
  using NF_ND by fastforce+

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')›
  apply (auto simp: trace_refine_def T_Seq append_single_T_imp_tickFree)
  using D_T by fastforce+

corollary mono_Seq_DT_right[simp]: ‹S ⊑⇩D⇩T S' ⟹ (P ❙; S)  ⊑⇩D⇩T (P ❙; S')›
  by (simp add: trace_divergence_refine_def)

lemma mono_Seq_DT_left[simp]: ‹P ⊑⇩D⇩T P' ⟹ (P ❙; S)  ⊑⇩D⇩T (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 ⊑⇩D⇩T P' ⟹ S ⊑⇩D⇩T S' ⟹ (P ❙; S)  ⊑⇩D⇩T (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 ⊑⇩D⇩T Q x ⟹ Mprefix A P ⊑⇩D⇩T 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 ⊑⇩D⇩T 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 ‹⊑⇩F⇩D› 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 ⊑⇩D⇩T Q ⟹ (P \ A) ⊑⇩D⇩T (Q \ A)›
proof -
  assume as: ‹P ⊑⇩D⇩T 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 ⊑⇩D⇩T P' ⟹ Q ⊑⇩D⇩T Q' ⟹ (P ⟦ A ⟧ Q) ⊑⇩D⇩T (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››


(* choose between mono_Mndetprefix_F and mono_mndet_F *)
lemma mono_Mndetprefix_F[simp]: ‹∀x∈A. 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]: ‹∀x∈A. 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]: ‹∀x∈A. 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]: ‹∀x∈A. P x ⊑⇩D⇩T Q x ⟹ Mndetprefix A P ⊑⇩D⇩T 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›
      (* removed nonempty hypothesis in the 3 following propositions *)
      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 ⊑⇩D⇩T 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 ⊑⇩D⇩T Mprefix A P›
  by (simp_all add: leFD_imp_leF leFD_imp_leD leF_imp_leT leD_leT_imp_leDT) 



(* see where we put this *)


lemma mono_read_FD[simp, elim]: "(⋀x. P x ⊑⇩F⇩D Q x) ⟹ (c❙?x → (P x)) ⊑⇩F⇩D (c❙?x → (Q x))"
  by (simp add: read_def)

lemma mono_write_FD[simp, elim]: "(P ⊑⇩F⇩D Q) ⟹  (c❙!x → P) ⊑⇩F⇩D (c❙!x → Q)"
  by (simp add: write_def)

lemma mono_write0_FD[simp, elim]: "P ⊑⇩F⇩D Q ⟹ (a → P) ⊑⇩F⇩D (a → Q)"
  by (simp add: write0_def)

(* make this with ⊑⇩D ⊑⇩T and ⊑⇩F ? *)
lemma mono_read_DT[simp, elim]: "(⋀x. P x ⊑⇩D⇩T Q x) ⟹ (c❙?x → (P x)) ⊑⇩D⇩T (c❙?x → (Q x))"
  by (simp add: read_def)

lemma mono_write_DT[simp, elim]: "(P ⊑⇩D⇩T Q) ⟹  (c❙!x → P) ⊑⇩D⇩T (c❙!x → Q)"
  by (simp add: write_def)

lemma mono_write0_DT[simp, elim]: "P ⊑⇩D⇩T Q ⟹ (a → P) ⊑⇩D⇩T (a → Q)"
  by (simp add: write0_def)



― ‹The following result is very useful, but we are not sure about where is its place›

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



end