Theory Process_norm

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : A Normalization Theory
 *
 * Copyright (c) 2020 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‹ Normalisation of Deterministic CSP Processes ›

theory Process_norm

imports "HOL-CSP.Assertions" "HOL-CSP.CSP_Induct"

begin

section‹Deterministic normal-forms with explicit state›

abbreviation "P_dnorm τ υ ≡ (μ X. (λ s. □ e ∈ (τ s) → X (υ s e)))"

notation      P_dnorm ("P⇩n⇩o⇩r⇩m⟦_,_⟧" 60)

lemma dnorm_cont[simp]:
  fixes τ::"'σ::type ⇒ 'event::type set" and υ::"'σ ⇒ 'event ⇒ 'σ"
  shows "cont (λX. (λs. □ e ∈ (τ s) → X (υ s e)))" (is "cont ?f")
proof -
  have  "cont (λX. ?f X s)" for s by (simp add:cont_fun) 
  then show ?thesis by simp
qed

section‹Interleaving product lemma›

lemma dnorm_inter:  
  fixes τ⇩1 ::"'σ⇩1::type ⇒ 'event::type set" and τ⇩2::"'σ⇩2::type ⇒ 'event set" 
    and υ⇩1 ::"'σ⇩1 ⇒ 'event ⇒ 'σ⇩1"          and υ⇩2::"'σ⇩2 ⇒ 'event ⇒ 'σ⇩2"
  defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ⇩1,υ⇩1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ P⇩n⇩o⇩r⇩m⟦τ⇩2,υ⇩2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")

  assumes indep: ‹∀s⇩1 s⇩2. τ⇩1 s⇩1 ∩ τ⇩2 s⇩2 = {}›

  defines Tr: "τ ≡ (λ(s⇩1,s⇩2). τ⇩1 s⇩1 ∪ τ⇩2 s⇩2)"
  defines Up: "υ ≡ (λ(s⇩1,s⇩2) e. if e ∈ τ⇩1 s⇩1 then (υ⇩1 s⇩1 e,s⇩2)
                                else if e ∈ τ⇩2 s⇩2 then (s⇩1, υ⇩2 s⇩2 e) else (s⇩1,s⇩2))"  
  defines S: "S ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "S ≡ fix⋅(Λ X. ?S X)")
  
  shows "(P s⇩1 ||| Q s⇩2) = S (s⇩1,s⇩2)"

proof -
  have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp 
  have Q_rec: "Q = ?Q Q" using fix_eq[of "(Λ X. ?Q X)"] Q by simp 
  have S_rec: "S = ?S S" using fix_eq[of "(Λ X. ?S X)"] S by simp
  have dir1: "∀ s⇩1 s⇩2. (P s⇩1 ||| Q s⇩2) ⊑⇩F⇩D S (s⇩1, s⇩2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind_inc[of "λx y. ∀ s⇩1 s⇩2. (x s⇩1 ||| y s⇩2) ⊑⇩F⇩D S (s⇩1,s⇩2)"])
    case admissibility
    then show ?case
        by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
  next
    case (base_fst y)
    then show ?case by (metis app_strict BOT_leFD Sync_BOT Sync_commute)
  next
    case (base_snd x)
    then show ?case by (simp add: Sync_BOT)
  next
    case (step x)
    then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
      proof(intro allI)
        fix s⇩1 s⇩2
        show "?C s⇩1 s⇩2"
          apply simp
          apply (subst Mprefix_Sync_distr_indep[where S = "{}", simplified])
          apply (subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
          apply (intro mono_Det_FD mono_Mprefix_FD)
          using step(3)[simplified] indep apply simp
          using step(2)[simplified] indep by fastforce
      qed
    qed         
  have dir2: "∀ s⇩1 s⇩2.  S (s⇩1, s⇩2) ⊑⇩F⇩D (P s⇩1 ||| Q s⇩2)"
    proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s⇩1 s⇩2. x (s⇩1,s⇩2) ⊑⇩F⇩D (P s⇩1 ||| Q s⇩2)" 1])
      case admissibility
      show ?case  by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI) 
    next
      case base_k_steps
      then show ?case by simp
    next
      case step
      then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
      proof(intro allI)
        fix s⇩1 s⇩2
        have P_rec_sym:"Mprefix (τ⇩1 s⇩1) (λe. P (υ⇩1 s⇩1 e)) = P s⇩1" using P_rec by metis
        have Q_rec_sym:"Mprefix (τ⇩2 s⇩2) (λe. Q (υ⇩2 s⇩2 e)) = Q s⇩2" using Q_rec by metis
        show "?C s⇩1 s⇩2"
          apply (simp add: Tr Up Mprefix_Un_distrib)
          apply (subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_indep[where S="{}", simplified])
          apply (intro mono_Det_FD mono_Mprefix_FD)
          apply (subst Q_rec_sym, simp add:step[simplified])
          apply (subst P_rec_sym) using step[simplified] indep by fastforce
      qed
    qed
  from dir1 dir2 show ?thesis using FD_antisym by blast
qed

section ‹Synchronous product lemma›

lemma dnorm_par:  
  fixes τ⇩1 ::"'σ⇩1::type ⇒ 'event::type set" and τ⇩2::"'σ⇩2::type ⇒ 'event set" 
    and υ⇩1 ::"'σ⇩1 ⇒ 'event ⇒ 'σ⇩1"          and υ⇩2::"'σ⇩2 ⇒ 'event ⇒ 'σ⇩2"
  defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ⇩1,υ⇩1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ P⇩n⇩o⇩r⇩m⟦τ⇩2,υ⇩2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")

  defines Tr: "τ ≡ (λ(s⇩1,s⇩2).  τ⇩1 s⇩1 ∩ τ⇩2 s⇩2)"
  defines Up: "υ ≡ (λ(s⇩1,s⇩2) e. (υ⇩1 s⇩1 e, υ⇩2 s⇩2 e))"  
  defines S: "S ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "S ≡ fix⋅(Λ X. ?S X)")
  
  shows "(P s⇩1 || Q s⇩2) = S (s⇩1,s⇩2)"

proof -
  have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp 
  have Q_rec: "Q = ?Q Q" using fix_eq[of "(Λ X. ?Q X)"] Q by simp 
  have S_rec: "S = ?S S" using fix_eq[of "(Λ X. ?S X)"] S by simp
  have dir1: "∀ s⇩1 s⇩2. (P s⇩1 || Q s⇩2) ⊑⇩F⇩D S (s⇩1, s⇩2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind[of "λx y. ∀ s⇩1 s⇩2. (x s⇩1 || y s⇩2) ⊑⇩F⇩D S (s⇩1,s⇩2)"])
      case adm:1
      then show ?case
        by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
    next
      case base:2
      then show ?case by (simp add: Sync_BOT)
    next
      case step:(3 x y)
      then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
      proof(intro allI)
        fix s⇩1 s⇩2
        show "?C s⇩1 s⇩2"
          apply(simp)
          apply(subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
          apply(subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
          by (simp add: step)
      qed
    qed     
  have dir2: "∀ s⇩1 s⇩2.  S (s⇩1, s⇩2) ⊑⇩F⇩D (P s⇩1 || Q s⇩2)"
    proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s⇩1 s⇩2. x (s⇩1,s⇩2) ⊑⇩F⇩D (P s⇩1 || Q s⇩2)" 1])
      case admissibility
      show ?case  by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI) 
    next
      case base_k_steps
      then show ?case by simp
    next
      case step
      then show ?case (is "∀ s⇩1 s⇩2. ?C s⇩1 s⇩2")
      proof(intro allI)
        fix s⇩1 s⇩2
        have P_rec_sym:"Mprefix (τ⇩1 s⇩1) (λe. P (υ⇩1 s⇩1 e)) = P s⇩1" using P_rec by metis
        have Q_rec_sym:"Mprefix (τ⇩2 s⇩2) (λe. Q (υ⇩2 s⇩2 e)) = Q s⇩2" using Q_rec by metis
        show "?C s⇩1 s⇩2"
          apply(simp add: Tr Up)
          apply(subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
          apply(rule mono_Mprefix_FD) 
          using step by auto
      qed
    qed
  from dir1 dir2 show ?thesis using FD_antisym by blast
qed

section‹Consequences›

―‹reachable states from one starting state›

inductive_set ℜ for     τ  ::"'σ::type ⇒ 'event::type set"
                    and υ  ::"'σ ⇒ 'event ⇒ 'σ" 
                    and σ⇩0 ::'σ 
  where rbase: "σ⇩0 ∈ ℜ τ υ σ⇩0"
      | rstep: "s ∈ ℜ τ υ σ⇩0 ⟹ e ∈ τ s  ⟹ υ s e ∈ ℜ τ υ σ⇩0"



―‹Deadlock freeness›
lemma deadlock_free_dnorm_ :
  fixes τ ::"'σ::type ⇒ 'event::type set" 
    and υ ::"'σ ⇒ 'event ⇒ 'σ" 
    and σ⇩0 ::'σ 
  assumes non_reachable_sink: "∀s ∈ ℜ τ υ σ⇩0. τ s ≠ {}"
  defines P: "P ≡ P⇩n⇩o⇩r⇩m⟦τ,υ⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  shows  "s ∈ ℜ τ υ σ⇩0 ⟹ deadlock_free_v2 (P s)"
proof(unfold deadlock_free_v2_FD DF⇩S⇩K⇩I⇩P_def, induct arbitrary:s rule:fix_ind)
  show "adm (λa. ∀x. x ∈ ℜ τ υ σ⇩0 ⟶ a ⊑⇩F⇩D P x)" by (simp add: monofun_def) 
next
  fix s :: "'σ" 
  show "s ∈ ℜ τ υ σ⇩0 ⟹ ⊥ ⊑⇩F⇩D P s" by simp
next
  fix s :: "'σ"  and x :: "'event process"
  have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp 
  assume 1 : "⋀s. s ∈ ℜ τ υ σ⇩0 ⟹ x ⊑⇩F⇩D P s" 
   and   2 : "s ∈ ℜ τ υ σ⇩0 "
  from   1 2 show "(Λ x. (⊓xa∈UNIV →  x) ⊓ SKIP)⋅x ⊑⇩F⇩D P s"
    apply (subst P_rec, rule_tac trans_FD[rotated, OF Mprefix_refines_Mndetprefix_FD])
    apply simp
    apply (rule mono_Ndet_FD_left)
    apply (rule trans_FD[OF mono_Mndetprefix_FD_set[of ‹τ s› ‹UNIV›]
                            mono_Mndetprefix_FD[rule_format, OF 1]])
    using non_reachable_sink[rule_format, OF 2] apply assumption
    by blast (meson ℜ.rstep)
qed



lemmas deadlock_free_dnorm = deadlock_free_dnorm_[rotated, OF rbase, rule_format]

end