(*<*)
―‹ ********************************************************************
 * 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.HOL-CSP"

begin

section‹Deterministic normal-forms with explicit state›

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

notation      P_dnorm ("P_norm[_,_]" 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 τ₁ ::"'σ₁::type → 'event::type set" and τ₂::"'σ₂::type → 'event set" 
    and υ₁ ::"'σ₁ → 'event → 'σ₁"          and υ₂::"'σ₂ → 'event → 'σ₂"
  defines P: "P ≡ P_norm[τ₁,υ₁]" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ P_norm[τ₂,υ₂]" (is "Q ≡ fix⋅(Λ X. ?Q X)")

assumes indep: ‹∀s₁ s₂. τ₁ s₁ ∩ τ₂ s₂ = {}›

defines Tr: "τ ≡ (λ(s₁,s₂). τ₁ s₁ ∪ τ₂ s₂)"
defines Up: "υ ≡ (λ(s₁,s₂) e. if e ∈ τ₁ s₁ then (υ₁ s₁ e,s₂)
                                else if e ∈ τ₂ s₂ then (s₁, υ₂ s₂ e) else (s₁,s₂))"  
defines S: "S ≡ P_norm[τ,υ]" (is "S ≡ fix⋅(Λ X. ?S X)")

shows "(P s₁ ||| Q s₂) = S (s₁,s₂)"

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₁ s₂. (P s₁ ||| Q s₂) ⊑_FD S (s₁, s₂)"
  proof(subst P, subst Q, 
      induct rule:parallel_fix_ind_inc[of "λx y. ∀ s₁ s₂. (x s₁ ||| y s₂) ⊑_FD S (s₁,s₂)"])
    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
  next
    case (step x)
    then show ?case (is "∀ s₁ s₂. ?C s₁ s₂")
    proof(intro allI)
      fix s₁ s₂
      show "?C s₁ s₂"
        apply simp
        apply (subst Mprefix_Sync_Mprefix_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₁ s₂. S (s₁, s₂) ⊑_FD (P s₁ ||| Q s₂)"
  proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s₁ s₂. x (s₁,s₂) ⊑_FD (P s₁ ||| Q s₂)" 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₁ s₂. ?C s₁ s₂")
    proof(intro allI)
      fix s₁ s₂
      have P_rec_sym:"Mprefix (τ₁ s₁) (λe. P (υ₁ s₁ e)) = P s₁" using P_rec by metis
      have Q_rec_sym:"Mprefix (τ₂ s₂) (λe. Q (υ₂ s₂ e)) = Q s₂" using Q_rec by metis
      show "?C s₁ s₂"
        apply (simp add: Tr Up Mprefix_Un_distrib)
        apply (subst P_rec, subst Q_rec, subst Mprefix_Sync_Mprefix_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 τ₁ ::"'σ₁::type → 'event::type set" and τ₂::"'σ₂::type → 'event set" 
    and υ₁ ::"'σ₁ → 'event → 'σ₁"          and υ₂::"'σ₂ → 'event → 'σ₂"
  defines P: "P ≡ P_norm[τ₁,υ₁]" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ P_norm[τ₂,υ₂]" (is "Q ≡ fix⋅(Λ X. ?Q X)")

defines Tr: "τ ≡ (λ(s₁,s₂). τ₁ s₁ ∩ τ₂ s₂)"
defines Up: "υ ≡ (λ(s₁,s₂) e. (υ₁ s₁ e, υ₂ s₂ e))"  
defines S: "S ≡ P_norm[τ,υ]" (is "S ≡ fix⋅(Λ X. ?S X)")

shows "(P s₁ || Q s₂) = S (s₁,s₂)"

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₁ s₂. (P s₁ || Q s₂) ⊑_FD S (s₁, s₂)"
  proof(subst P, subst Q, 
      induct rule:parallel_fix_ind[of "λx y. ∀ s₁ s₂. (x s₁ || y s₂) ⊑_FD S (s₁,s₂)"])
    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
  next
    case step:(3 x y)
    then show ?case (is "∀ s₁ s₂. ?C s₁ s₂")
    proof(intro allI)
      fix s₁ s₂
      show "?C s₁ s₂"
        apply(simp)
        apply(subst Mprefix_Sync_Mprefix_subset[where S="UNIV", simplified])
        apply(subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
        by (simp add: step mono_Mprefix_FD)
    qed
  qed     
  have dir2: "∀ s₁ s₂. S (s₁, s₂) ⊑_FD (P s₁ || Q s₂)"
  proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s₁ s₂. x (s₁,s₂) ⊑_FD (P s₁ || Q s₂)" 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₁ s₂. ?C s₁ s₂")
    proof(intro allI)
      fix s₁ s₂
      have P_rec_sym:"Mprefix (τ₁ s₁) (λe. P (υ₁ s₁ e)) = P s₁" using P_rec by metis
      have Q_rec_sym:"Mprefix (τ₂ s₂) (λe. Q (υ₂ s₂ e)) = Q s₂" using Q_rec by metis
      show "?C s₁ s₂"
        apply(simp add: Tr Up)
        apply(subst P_rec, subst Q_rec, subst Mprefix_Sync_Mprefix_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 R for     τ  ::"'σ::type → 'event::type set"
  and υ  ::"'σ → 'event → 'σ" 
  and σ₀ ::'σ 
where rbase: "σ₀ ∈ R τ υ σ₀"
| rstep: "s ∈ R τ υ σ₀ ==> e ∈ τ s ==> υ s e ∈ R τ υ σ₀"



―‹Deadlock freeness›
lemma deadlock_free_dnorm_ :
  fixes τ ::"'σ::type → 'event::type set" 
    and υ ::"'σ → 'event → 'σ" 
    and σ₀ ::'σ 
  assumes non_reachable_sink: "∀s ∈ R τ υ σ₀. τ s ≠ {}"
  defines P: "P ≡ P_norm[τ,υ]" (is "P ≡ fix⋅(Λ X. ?P X)")
  shows  "s ∈ R τ υ σ₀ ==> deadlock_free (P s)"
proof(unfold deadlock_free_def DF_def, induct arbitrary:s rule:fix_ind)
  show "adm (λa. ∀x. x ∈ R τ υ σ₀ ⟶ a ⊑_FD P x)" by (simp add: monofun_def) 
next
  fix s :: "'σ" 
  show "s ∈ R τ υ σ₀ ==> ⊥ ⊑_FD P s" by simp
next
  fix s x assume 1 : "∧s. s ∈ R τ υ σ₀ ==> x ⊑_FD P s" 
    and   2 : "s ∈ R τ υ σ₀ "
  have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp 

  from   1 2 show "(Λ x. (⊓xa∈UNIV → x))⋅x ⊑_FD P s"
    apply (subst P_rec, rule_tac trans_FD[rotated, OF Mndetprefix_FD_Mprefix])
    apply simp
    apply (rule trans_FD[OF Mndetprefix_FD_subset[of ‹τ s› ‹UNIV›]
          mono_Mndetprefix_FD[rule_format, OF 1]])
    using non_reachable_sink[rule_format, OF 2] apply assumption
    by blast (meson R.rstep)
qed



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

end