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 (Pnorm_,_ 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  Pnormτ1,υ1" (is "P  fix(Λ X. ?P X)")
  defines Q: "Q  Pnormτ2,υ2" (is "Q  fix(Λ X. ?Q X)")

  assumes indep: s1 s2. τ1 s1  τ2 s2 = {}

  defines Tr: "τ  (λ(s1,s2). τ1 s1  τ2 s2)"
  defines Up: "υ  (λ(s1,s2) e. if e  τ1 s1 then (υ1 s1 e,s2)
                                else if e  τ2 s2 then (s1, υ2 s2 e) else (s1,s2))"  
  defines S: "S  Pnormτ,υ" (is "S  fix(Λ X. ?S X)")
  
  shows "(P s1 ||| Q s2) = S (s1,s2)"

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: " s1 s2. (P s1 ||| Q s2) FD S (s1, s2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind_inc[of "λx y.  s1 s2. (x s1 ||| y s2) FD S (s1,s2)"])
    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 " s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        show "?C s1 s2"
          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: " s1 s2.  S (s1, s2) FD (P s1 ||| Q s2)"
    proof(subst S, induct rule:fix_ind_k[of "λx.  s1 s2. x (s1,s2) FD (P s1 ||| Q s2)" 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 " s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        have P_rec_sym:"Mprefix (τ1 s1) (λe. P (υ1 s1 e)) = P s1" using P_rec by metis
        have Q_rec_sym:"Mprefix (τ2 s2) (λe. Q (υ2 s2 e)) = Q s2" using Q_rec by metis
        show "?C s1 s2"
          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  Pnormτ1,υ1" (is "P  fix(Λ X. ?P X)")
  defines Q: "Q  Pnormτ2,υ2" (is "Q  fix(Λ X. ?Q X)")

  defines Tr: "τ  (λ(s1,s2).  τ1 s1  τ2 s2)"
  defines Up: "υ  (λ(s1,s2) e. (υ1 s1 e, υ2 s2 e))"  
  defines S: "S  Pnormτ,υ" (is "S  fix(Λ X. ?S X)")
  
  shows "(P s1 || Q s2) = S (s1,s2)"

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: " s1 s2. (P s1 || Q s2) FD S (s1, s2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind[of "λx y.  s1 s2. (x s1 || y s2) FD S (s1,s2)"])
      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 " s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        show "?C s1 s2"
          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: " s1 s2.  S (s1, s2) FD (P s1 || Q s2)"
    proof(subst S, induct rule:fix_ind_k[of "λx.  s1 s2. x (s1,s2) FD (P s1 || Q s2)" 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 " s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        have P_rec_sym:"Mprefix (τ1 s1) (λe. P (υ1 s1 e)) = P s1" using P_rec by metis
        have Q_rec_sym:"Mprefix (τ2 s2) (λe. Q (υ2 s2 e)) = Q s2" using Q_rec by metis
        show "?C s1 s2"
          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  Pnormτ,υ" (is "P  fix(Λ X. ?P X)")
  shows  "s   τ υ σ0  deadlock_free_v2 (P s)"
proof(unfold deadlock_free_v2_FD DFSKIP_def, induct arbitrary:s rule:fix_ind)
  show "adm (λa. x. x   τ υ σ0  a FD P x)" by (simp add: monofun_def) 
next
  fix s :: "" 
  show "s   τ υ σ0   FD 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 FD P s" 
   and   2 : "s   τ υ σ0 "
  from   1 2 show "(Λ x. (xaUNIV   x)  SKIP)x FD 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