Session CSP_RefTK

Theory Introduction

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : An Introduction
 *
 * 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‹Context›
(*<*)
theory Introduction
    imports HOLCF
begin
(*>*)

section‹Introduction›

text‹
Communicating Sequential Processes CSP is a language 
to specify and verify patterns of interaction of concurrent systems.
Together with CCS and LOTOS, it belongs to the family of ∗‹process algebras›. 
CSP's rich theory comprises denotational, operational and algebraic semantic facets 
and has influenced programming languages such as Limbo, Crystal, Clojure and
most notably Golang @{cite "donovan2015go"}. CSP has been applied in 
industry as a tool for specifying and verifying the concurrent aspects of hardware 
systems, such as the T9000 transputer @{cite "Barret95"}. 

The theory of CSP, in particular the denotational Failure/Divergence Denotational Semantics,
has been initially proposed in the book by Tony Hoare @{cite "Hoare:1985:CSP:3921"}, but evolved
substantially since @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.

Verification of CSP properties has been centered around the notion of ∗‹process refinement orderings›,
most notably ‹_⊑FD_› and ‹_⊑_›. The latter turns the denotational domain of CSP into a Scott cpo 
@{cite "scott:cpo:1972"}, which yields semantics for the fixed point operator ‹μx. f(x)› provided 
that ‹f› is continuous with respect to ‹_⊑_›. Since it is possible to express deadlock-freeness and 
livelock-freeness as a refinement problem, the verification of properties has been reduced 
traditionally to a model-checking problem for a finite set of events ‹A›.

We are interested in verification techniques for arbitrary event sets ‹A› or arbitrarily 
parameterized processes. Such processes can be used to model dense-timed processes, processes 
with dynamic thread creation, and processes with unbounded thread-local variables and buffers.
Events may even be higher-order objects such as functions or again processes, paving the way
for the modeling of re-programmable compute servers or dynamic distributed computing architectures.
However, this adds substantial complexity to the process theory: when it comes to study the 
interplay of different denotational models, refinement-orderings, and side-conditions for 
continuity, paper-and-pencil proofs easily reach their limits of precision. 

Several attempts have been undertaken to develop the formal theory of CSP in an interactive proof system, 
mostly in Isabelle/HOL @{cite "Camilleri91" and "tej.ea:corrected:1997" and  "IsobeRoggenbach2010"}. 
This work is based on the most recent instance in this line, HOL-CSP 2.0, which has been published 
as AFP submission  @{cite "HOL-CSP-AFP"} and whose development is hosted at 
🌐‹https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0›. 

The present AFP Module is an add-on on this work and develops some support for 
▸ advanced induction schemes (mutual fixed-point Induction, K-induction),
▸ bridge-Lemmas between the classical refinement relations in the FD-semantics,
  which allow for reduced refinement proof complexity in certain cases, and
▸ a theory of explicit state normalisation which allows for proofs over certain
  communicating networks of arbitrary size.

\newpage
›



section‹The Global Architecture of CSP\_RefTk›
text‹
\begin{figure}[ht]
  \centering
  \includegraphics[width=0.60\textwidth]{figures/session_graph.pdf}
	\caption{The overall architecture: HOLCF, HOL-CSP, and CSP\_RefTk}
	\label{fig:fig1}
\end{figure}
›

text‹The global architecture of CSP\_RefTk is shown in \autoref{fig:fig1}.
The entire package resides on: 
▸ session‹HOL-Eisbach› from the Isabelle/HOL distribution,
▸ session‹HOLCF› from the Isabelle/HOL distribution, and
▸ session‹HOL-CSP› 2.0 from the Isabelle Archive of Formal Proofs.

⇤ The theories ▩‹Assertion_ext› and ▩‹Fixind_ext› are extensions of the 
corresponding theories in session‹HOL-CSP›.›


(*<*)
end
(*>*)

Theory Assertions_ext

(*<*)
―‹ ******************************************************************** 
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : Assertions on DF and LF and their Relations
 *
 * 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‹Basic CSP\_RefTk-Theories›

theory Assertions_ext
  imports "HOL-CSP.Assertions"
begin

section ‹Preliminaries›

lemma DFSKIP_unfold : "DFSKIP A = ((⊓ z ∈ A → DFSKIP A) ⊓ SKIP)"
  by(simp add: DFSKIP_def, rule trans, rule fix_eq, simp)

section ‹All refinements definitions›

thm failure_divergence_refine_def[simplified le_ref_def] trace_refine_def failure_refine_def

definition divergence_refine :: "'a process ⇒ 'a process ⇒ bool" (infix "⊑D" 60)
  where "P ⊑D Q ≡ D Q ⊆ D P"

definition trace_divergence_refine :: "'a process ⇒ 'a process ⇒ bool" (infix "⊑DT" 60)
  where "P ⊑DT Q ≡ P ⊑T Q ∧ P ⊑D Q"

section ‹Relations between refinements›

lemma le_F_T: "P ⊑F Q ⟹ P ⊑T Q"
  by (simp add: F_subset_imp_T_subset failure_refine_def trace_refine_def) 

lemma FD_F: "P ⊑FD Q ⟹ P ⊑F Q"
  by (simp add: failure_divergence_refine_def failure_refine_def le_ref_def)
  
lemma FD_D: "P ⊑FD Q ⟹ P ⊑D Q"
  by (simp add: divergence_refine_def failure_divergence_refine_def le_ref_def)

lemma DT_D: "P ⊑DT Q ⟹ P ⊑D Q"
  by (simp add: trace_divergence_refine_def)

lemma DT_T: "P ⊑DT Q ⟹ P ⊑T Q"
  by (simp add: trace_divergence_refine_def)

lemma F_D_FD:"P ⊑F Q ⟹ P ⊑D Q ⟹ P ⊑FD Q"
  by (simp add: divergence_refine_def failure_divergence_refine_def failure_refine_def le_ref_def)

lemma D_T_DT:"P ⊑D Q ⟹ P ⊑T Q ⟹ P ⊑DT Q"
  by (simp add: trace_divergence_refine_def)

section ‹Some obvious refinements›

lemma bot_FD[simp]: "⊥ ⊑FD Q"
  by (simp add: failure_divergence_refine_def)

corollary bot_F[simp]: "⊥ ⊑F Q"
      and bot_D[simp]: "⊥ ⊑D Q"
      and bot_T[simp]: "⊥ ⊑T Q"
      and bot_DT[simp]: "⊥ ⊑DT Q"
  by (simp_all add: FD_F FD_D le_F_T D_T_DT)

lemma STOP_leDT[simp]: "P ⊑DT STOP"
  by (simp add: D_STOP D_T_DT Nil_elem_T T_STOP divergence_refine_def trace_refine_def)

―‹For refinement proofs, we need admissibility and monotony starting with idempotency and 
  transitivity›

section ‹Idempotency›

lemma idem_F[simp]: "P ⊑F P"
  by (simp add: failure_refine_def) 

lemma idem_D[simp]: "P ⊑D P"
  by (simp add: divergence_refine_def)

lemma idem_T[simp]: "P ⊑T P"
  by (simp add: trace_refine_def)

lemma idem_FD[simp]: "P ⊑FD P"
  by (simp add: failure_divergence_refine_def)

lemma idem_DT[simp]: "P ⊑DT P"
  by (simp add: trace_divergence_refine_def)

section ‹Transitivity›

lemma trans_F: "P ⊑F Q ⟹ Q ⊑F S ⟹ P ⊑F S"
  by (meson failure_refine_def order_trans)

lemma trans_D: "P ⊑D Q ⟹ Q ⊑D S ⟹ P ⊑D S"
  by (meson divergence_refine_def order_trans)

lemma trans_T: "P ⊑T Q ⟹ Q ⊑T S ⟹ P ⊑T S"
  by (meson trace_refine_def order_trans)

lemma trans_FD: "P ⊑FD Q ⟹ Q ⊑FD S ⟹ P ⊑FD S"
  by (meson failure_divergence_refine_def order_trans)

lemma trans_DT: "P ⊑DT Q ⟹ Q ⊑DT S ⟹ P ⊑DT S"
  by (meson trace_divergence_refine_def order_trans trans_D trans_T)

section ‹Admissibility›

lemma le_F_adm: "cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑F v x)"
proof(auto simp add:cont2contlubE adm_def failure_refine_def)
  fix Y a b
  assume 1:"cont u" 
     and 2:"monofun v" 
     and 3:"chain Y" 
     and 4:"∀i. F (v (Y i)) ⊆ F (u (Y i))" 
     and 5:" (a, b) ∈ F (v (⨆x. Y x))"
  hence "v (Y i)  ⊑ v (⨆i. Y i)" for i by (simp add: is_ub_thelub monofunE)
  hence "F (v (⨆i. Y i)) ⊆ F (u (Y i))" for i using 4 le_approx_lemma_F by blast   
  then show "(a, b) ∈ F (⨆i. u (Y i))"
    using F_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed

lemma le_T_adm: "cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑T v x)"
proof(auto simp add:cont2contlubE adm_def trace_refine_def)
  fix Y x
  assume 1:"cont u" 
     and 2:"monofun v" 
     and 3:"chain Y" 
     and 4:"∀i. T (v (Y i)) ⊆ T (u (Y i))" 
     and 5:" x ∈ T (v (⨆i. Y i))"
  hence "v (Y i)  ⊑ v (⨆i. Y i)" for i by (simp add: is_ub_thelub monofunE)
  hence "T (v (⨆i. Y i)) ⊆ T (u (Y i))" for i using 4 le_approx_lemma_T by blast  
  then show "x ∈ T (⨆i. u (Y i))"
    using T_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed

lemma le_D_adm: "cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑D v x)"
proof(auto simp add:cont2contlubE adm_def divergence_refine_def)
  fix Y x
  assume 1:"cont u" 
     and 2:"monofun v" 
     and 3:"chain Y" 
     and 4:"∀i. D (v (Y i)) ⊆ D (u (Y i))" 
     and 5:" x ∈ D (v (⨆i. Y i))"
  hence "v (Y i)  ⊑ v (⨆i. Y i)" for i by (simp add: is_ub_thelub monofunE)
  hence "D (v (⨆i. Y i)) ⊆ D (u (Y i))" for i using 4 le_approx1 by blast  
  then show "x ∈ D (⨆i. u (Y i))"
    using D_LUB[OF ch2ch_cont[OF 1 3]] limproc_is_thelub[OF ch2ch_cont[OF 1 3]] 5 by force
qed

lemma le_DT_adm: "cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ⊑DT v x)"
  using adm_conj[OF le_T_adm[of u v] le_D_adm[of u v]] by (simp add:trace_divergence_refine_def)

lemmas le_FD_adm = le_adm[simplified failure_divergence_refine_def[symmetric]]

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[simplified failure_divergence_refine_def[symmetric]]

―‹Deterministic choice monotony doesn't hold for ‹⊑F››


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[simplified failure_divergence_refine_def[symmetric]]

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) 

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[simplified failure_divergence_refine_def[symmetric]] and
mono_ndet_FD_right[simp] = 
             mono_ndet_FD_right[simplified failure_divergence_refine_def[symmetric]]

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: FD_F FD_D le_F_T D_T_DT) 


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 ⊑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[simplified failure_divergence_refine_def[symmetric]]


lemma mono_mprefix_F_process[simp]: "∀x. P x ⊑F Q x ⟹ Mprefix A P ⊑F Mprefix A Q"
  by (auto simp: failure_refine_def F_Mprefix)

lemma mono_mprefix_D_process[simp]: "∀x. P x ⊑D Q x ⟹ Mprefix A P ⊑D Mprefix A Q"
  by (auto simp: divergence_refine_def D_Mprefix)

lemma mono_mprefix_T_process[simp]: "∀x. P x ⊑T Q x ⟹ Mprefix A P ⊑T Mprefix A Q"
  by (auto simp: trace_refine_def T_Mprefix)

corollary mono_mprefix_DT_process[simp]: "∀x. P x ⊑DT Q x ⟹ Mprefix A P ⊑DT Mprefix A Q"
  by (simp add: trace_divergence_refine_def)
  
lemmas 
mono_mprefix_FD_process[simp] = 
                mono_mprefix_FD[simplified failure_divergence_refine_def[symmetric]]

lemma mono_mprefix_DT_set[simp]: "A ⊆ B ⟹ Mprefix B P ⊑DT Mprefix A P"
  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: DT_D DT_T)

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


lemma mono_hide_F[simp]: "P ⊑F Q ⟹ P \\ A ⊑F Q \\ A"
  apply(cases "A={}", simp_all add: hide_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 ∈ D 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_hide_T[simp]: "P ⊑T Q ⟹ P \\ A ⊑T Q \\ A"
  apply(cases "A={}", simp add: hide_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 ∈ 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 ∈ D 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_hide_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 DT_T[THEN mono_hide_T, OF as] show ?thesis by (simp add: trace_divergence_refine_def) 
qed

lemmas mono_hide_FD[simp] = 
                 mono_hide_FD[simplified failure_divergence_refine_def[symmetric]]

―‹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[simplified failure_divergence_refine_def[symmetric]]

―‹synchronization monotony doesn't hold for ‹⊑F›, ‹⊑D› and ‹⊑T››


lemma mono_mndet_F_process[simp]: "∀x∈A. P x ⊑F Q x ⟹ mndet A P ⊑F mndet A Q"
  by (cases "A = {}", auto simp: failure_refine_def F_mndet write0_def F_Mprefix) 

lemma mono_mndet_D_process[simp]: "∀x∈A. P x ⊑D Q x ⟹ mndet A P ⊑D mndet A Q"
  by (cases "A = {}", auto simp: divergence_refine_def D_mndet write0_def D_Mprefix)

lemma mono_mndet_T_process[simp]: "∀x∈A. P x ⊑T Q x ⟹ mndet A P ⊑T mndet A Q"
  by (cases "A = {}", auto simp: trace_refine_def T_mndet write0_def T_Mprefix)

corollary mono_mndet_DT_process[simp]: "∀x∈A. P x ⊑DT Q x ⟹ mndet A P ⊑DT mndet A Q"
  by (simp add: trace_divergence_refine_def)
  
lemmas 
mono_mndet_FD_process[simp] = 
              mono_mndet_FD[simplified failure_divergence_refine_def[symmetric]]

lemmas 
mono_mndet_FD_set[simp] = 
              mndet_FD_subset[simplified failure_divergence_refine_def[symmetric]]

corollary mono_mndet_F_set[simp]: "A ≠ {} ⟹ A ⊆ B ⟹ mndet B P ⊑F mndet A P"
      and mono_mndet_D_set[simp]: "A ≠ {} ⟹ A ⊆ B ⟹ mndet B P ⊑D mndet A P"
      and mono_mndet_T_set[simp]: "A ≠ {} ⟹ A ⊆ B ⟹ mndet B P ⊑T mndet A P"
      and mono_mndet_DT_set[simp]: "A ≠ {} ⟹ A ⊆ B ⟹ mndet B P ⊑DT mndet A P"
  by (simp_all add: FD_F FD_D le_F_T D_T_DT)

lemmas 
Mprefix_refines_Mndet_FD[simp] = 
                          Mprefix_refines_Mndet[simplified failure_divergence_refine_def[symmetric]]

corollary Mprefix_refines_Mndet_F[simp]: "mndet A P ⊑F Mprefix A P"
      and Mprefix_refines_Mndet_D[simp]: "mndet A P ⊑D Mprefix A P"
      and Mprefix_refines_Mndet_T[simp]: "mndet A P ⊑T Mprefix A P"
      and Mprefix_refines_Mndet_DT[simp]: "mndet A P ⊑DT Mprefix A P"
  by (simp_all add: FD_F FD_D le_F_T D_T_DT) 


section ‹Reference processes and their unfolding rules›

thm DF_def DFSKIP_def RUN_def CHAOS_def

definition CHAOSSKIP :: "'a set ⇒ 'a process" 
  where   "CHAOSSKIP A ≡ μ X. (SKIP ⊓ STOP ⊓ (□ x ∈ A → X))"


thm DF_unfold DFSKIP_unfold

lemma RUN_unfold : "RUN A = (□ z ∈ A → RUN A)"
  by(simp add: RUN_def, rule trans, rule fix_eq, simp)

lemma CHAOS_unfold : "CHAOS A = (STOP ⊓ (□ z ∈ A → CHAOS A))"
  by(simp add: CHAOS_def, rule trans, rule fix_eq, simp)
                                              
lemma CHAOSSKIP_unfold: "CHAOSSKIP A ≡ SKIP ⊓ STOP ⊓ (□ x ∈ A → CHAOSSKIP A)"
  unfolding CHAOSSKIP_def using fix_eq[of "Λ X. (SKIP ⊓ STOP ⊓ (□ x ∈ A → X))"] by simp

section ‹Process events and reference processes events›

definition events_of where "events_of P ≡ (⋃t∈T P. {a. ev a ∈ set t})"

lemma events_DF: "events_of (DF A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t ∈ T (DF A) ⟹ ev x ∈ set t ⟹ x ∈ A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t ∈ T (⊓z∈A →  DF A)" using DF_unfold by metis
    then obtain aa where "a = ev aa ∧ aa ∈ A ∧ t ∈ T (DF A)" 
      by (cases "A={}", auto simp add:T_mndet write0_def T_Mprefix T_STOP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x ∈ A ⟹ ∃xa∈T (DF A). ev x ∈ set xa"
    apply(subst DF_unfold, cases "A={}", auto simp add:T_mndet write0_def T_Mprefix)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_DFSKIP: "events_of (DFSKIP A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t ∈ T (DFSKIP A) ⟹ ev x ∈ set t ⟹ x ∈ A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t ∈ T ((⊓z∈A →  DFSKIP A) ⊓ SKIP)" using DFSKIP_unfold by metis
    with Cons obtain aa where "a = ev aa ∧ aa ∈ A ∧ t ∈ T (DFSKIP A)" 
      by (cases "A={}", auto simp add:T_mndet write0_def T_Mprefix T_STOP T_SKIP T_ndet)  
    with Cons show ?case by auto
  qed
next
  fix x
  show "x ∈ A ⟹ ∃xa∈T (DFSKIP A). ev x ∈ set xa"
    apply(subst DFSKIP_unfold, cases "A={}")
     apply(auto simp add:T_mndet write0_def T_Mprefix T_SKIP T_ndet)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_RUN: "events_of (RUN A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t ∈ T (RUN A) ⟹ ev x ∈ set t ⟹ x ∈ A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t ∈ T (□z∈A →  RUN A)" using RUN_unfold by metis
    then obtain aa where "a = ev aa ∧ aa ∈ A ∧ t ∈ T (RUN A)" by (auto simp add:T_Mprefix)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x ∈ A ⟹ ∃xa∈T (RUN A). ev x ∈ set xa"
    apply(subst RUN_unfold, simp add: T_Mprefix)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_CHAOS: "events_of (CHAOS A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t ∈ T (CHAOS A) ⟹ ev x ∈ set t ⟹ x ∈ A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t ∈ T (STOP ⊓ (□ z ∈ A → CHAOS A))" using CHAOS_unfold by metis
    then obtain aa where "a = ev aa ∧ aa ∈ A ∧ t ∈ T (CHAOS A)" 
      by (auto simp add:T_ndet T_Mprefix T_STOP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x ∈ A ⟹ ∃xa∈T (CHAOS A). ev x ∈ set xa"
    apply(subst CHAOS_unfold, simp add:T_ndet T_Mprefix T_STOP)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_CHAOSSKIP: "events_of (CHAOSSKIP A) = A"
proof(auto simp add:events_of_def)
  fix x t
  show "t ∈ T (CHAOSSKIP A) ⟹ ev x ∈ set t ⟹ x ∈ A"
  proof(induct t)
    case Nil
    then show ?case by simp
  next
    case (Cons a t)
    from Cons(2) have "a # t ∈ T (SKIP ⊓ STOP ⊓ (□ z ∈ A → CHAOSSKIP A))" 
      using CHAOSSKIP_unfold by metis
    with Cons obtain aa where "a = ev aa ∧ aa ∈ A ∧ t ∈ T (CHAOSSKIP A)" 
      by (auto simp add:T_ndet T_Mprefix T_STOP T_SKIP)
    with Cons show ?case by auto
  qed
next
  fix x
  show "x ∈ A ⟹ ∃xa∈T (CHAOSSKIP A). ev x ∈ set xa"
    apply(subst CHAOSSKIP_unfold, simp add:T_ndet T_Mprefix T_STOP T_SKIP)
    by (metis Nil_elem_T list.sel(1) list.sel(3) list.set_intros(1))
qed

lemma events_div: "D(P) ≠ {} ⟹  events_of (P) = UNIV"
proof(auto simp add:events_of_def)
  fix x xa
  assume 1: "x ∈ D P"
  show "∃x∈T P. ev xa ∈ set x"
  proof(cases "tickFree x")
    case True  
    hence "x@[ev xa] ∈ T P"
      using 1 NT_ND front_tickFree_single is_processT7 by blast   
    then show ?thesis by force 
  next
    case False
    hence "(butlast x)@[ev xa] ∈ T P"
      by (metis "1" D_T D_imp_front_tickFree append_single_T_imp_tickFree butlast_snoc 
                front_tickFree_single nonTickFree_n_frontTickFree process_charn) 
    then show ?thesis by force
  qed
qed


thm DF_subset

lemma DFSKIP_subset_FD: "A ≠ {} ⟹ A ⊆ B ⟹ DFSKIP B ⊑FD DFSKIP A"
  apply(subst DFSKIP_def, rule fix_ind, rule le_FD_adm, simp_all add:monofunI, subst DFSKIP_unfold)
  by (rule mono_ndet_FD, simp_all) (meson mono_mndet_FD_process mono_mndet_FD_set trans_FD) 

lemma RUN_subset_DT: "A ⊆ B ⟹ RUN B ⊑DT RUN A"
  apply(subst RUN_def, rule fix_ind, rule le_DT_adm, simp_all add:monofunI, subst RUN_unfold)
  by (meson mono_mprefix_DT_process mono_mprefix_DT_set trans_DT)

lemma CHAOS_subset_FD: "A ⊆ B ⟹ CHAOS B ⊑FD CHAOS A"
  apply(subst CHAOS_def, rule fix_ind, rule le_FD_adm, simp_all add:monofunI, subst CHAOS_unfold)
  by (auto simp add: failure_divergence_refine_def le_ref_def 
                     D_Mprefix D_ndet F_STOP F_Mprefix F_ndet) 

lemma CHAOSSKIP_subset_FD: "A ⊆ B ⟹ CHAOSSKIP B ⊑FD CHAOSSKIP A"
  apply(subst CHAOSSKIP_def, rule fix_ind, rule le_FD_adm) 
     apply(simp_all add:monofunI, subst CHAOSSKIP_unfold)
  by (auto simp add: failure_divergence_refine_def le_ref_def 
                     D_Mprefix D_ndet F_STOP F_Mprefix F_ndet)

section ‹Relations between refinements on reference processes›

lemma CHAOS_has_all_tickFree_failures: 
      "tickFree a ⟹ {x. ev x ∈ set a} ⊆ A ⟹ (a,b) ∈ F (CHAOS A)"
proof(induct a)
  case Nil
  then show ?case 
    by (subst CHAOS_unfold, simp add:F_ndet F_STOP)
next
  case (Cons a0 al)
  hence "tickFree al"
    by (metis append.left_neutral append_Cons front_tickFree_charn front_tickFree_mono)
  with Cons show ?case 
    apply (subst CHAOS_unfold, simp add:F_ndet F_STOP F_Mprefix events_of_def)
    using event_set by blast
qed

lemma CHAOSSKIP_has_all_failures: 
  assumes as:"(events_of P) ⊆ A" 
  shows "CHAOSSKIP A ⊑F P"
proof -
  have "front_tickFree a ⟹ set a ⊆ (⋃t∈T P. set t) ⟹ (a,b) ∈ F (CHAOSSKIP A)" for a b
  proof(induct a)
    case Nil
    then show ?case 
      by (subst CHAOSSKIP_unfold, simp add:F_ndet F_STOP)
  next
    case (Cons a0 al)
    hence "front_tickFree al"
      by (metis append.left_neutral append_Cons front_tickFree_charn front_tickFree_mono)
    with Cons show ?case 
      apply (subst CHAOSSKIP_unfold, simp add:F_ndet F_STOP F_SKIP F_Mprefix events_of_def as)
      apply(cases "a0=tick")
       apply (metis append.simps(2) front_tickFree_charn 
                    front_tickFree_mono list.distinct(1) tickFree_Cons)
      using event_set image_iff as[simplified events_of_def] by fastforce
  qed
  thus ?thesis 
    by (simp add: F_T SUP_upper failure_refine_def process_charn subrelI) 
qed

corollary CHAOSSKIP_has_all_failures_ev: "CHAOSSKIP (events_of P) ⊑F P" 
      and CHAOSSKIP_has_all_failures_Un: "CHAOSSKIP UNIV ⊑F P"
  by (simp_all add: CHAOSSKIP_has_all_failures)


lemma DFSKIP_DF_refine_F: "DFSKIP A  ⊑F DF A"
  by (simp add:DFSKIP_def, rule fix_ind, simp_all add:le_F_adm monofunI, subst DF_unfold, simp) 

lemma DF_RUN_refine_F: "DF A  ⊑F RUN A"
  apply (simp add:DF_def, rule fix_ind, simp_all add:le_F_adm monofunI, subst RUN_unfold)
  by (meson Mprefix_refines_Mndet_F mono_mndet_F_process trans_F)

lemma CHAOS_DF_refine_F: "CHAOS A  ⊑F DF A"
  apply (simp add:CHAOS_def DF_def, rule parallel_fix_ind, simp_all add: monofunI)
   apply (rule le_F_adm, simp_all add: monofun_snd)
  by (cases "A={}", auto simp add:adm_def failure_refine_def F_mndet 
                                  F_Mprefix write0_def F_ndet F_STOP)

corollary CHAOSSKIP_CHAOS_refine_F: "CHAOSSKIP A  ⊑F CHAOS A"
      and CHAOSSKIP_DFSKIP_refine_F: "CHAOSSKIP A  ⊑F DFSKIP A"
  by (simp_all add: CHAOSSKIP_has_all_failures events_CHAOS events_DFSKIP 
                    trans_F[OF CHAOS_DF_refine_F DF_RUN_refine_F])


lemma div_free_DFSKIP: "D(DFSKIP A) = {}"
proof(simp add:DFSKIP_def fix_def) 
  define Y where "Y ≡ λi. iterate i⋅(Λ x. (⊓xa∈A →  x) ⊓ SKIP)⋅⊥"
  hence a:"chain Y" by simp
  have "D (Y (Suc i)) = {d. d ≠ [] ∧ hd d  ∈ (ev ` A) ∧ tl d ∈ D(Y i)}" for i
    by (cases "A={}", auto simp add:Y_def D_STOP D_SKIP D_mndet write0_def D_Mprefix D_ndet) 
  hence b:"d ∈ D(Y i) ⟹ length d ≥ i" for d i
    by (induct i arbitrary:d, simp_all add: Nitpick.size_list_simp(2))
  { fix x
    assume c:"∀ i. x ∈ D (Y i)"
    from b have "x ∉ D (Y (Suc (length x)))" using Suc_n_not_le_n by blast
    with c have False by simp
  }
  with a show "D (⨆i. Y i) = {}"
  using D_LUB[OF a] limproc_is_thelub[OF a] by auto
qed

lemma div_free_DF: "D(DF A) = {}"
proof - 
  have "DFSKIP A  ⊑D DF A"
    by (simp add:DFSKIP_def, rule fix_ind, simp_all add:le_D_adm monofunI, subst DF_unfold, simp) 
  then show ?thesis using divergence_refine_def div_free_DFSKIP by blast 
qed

lemma div_free_CHAOSSKIP: "D (CHAOSSKIP A) = {}"
proof -
  have "DFSKIP A  ⊑D CHAOSSKIP A"
  proof (simp add:DFSKIP_def, rule fix_ind, simp_all add:le_D_adm monofunI, subst CHAOSSKIP_unfold)
    fix x
    assume 1:"x ⊑D CHAOSSKIP A"
    have a:"((⊓xa∈A →  x) ⊓ SKIP) = (SKIP ⊓ SKIP ⊓ (⊓xa∈A →  x))" 
      by (simp add: Ndet_commute ndet_id)
    from 1 have b:"(SKIP ⊓ SKIP ⊓ (⊓xa∈A →  x)) ⊑D (SKIP ⊓ STOP ⊓ (□xa∈A → CHAOSSKIP A))"
      by (meson DT_D Mprefix_refines_Mndet_D STOP_leDT idem_D 
                mono_mprefix_D_process mono_ndet_D trans_D)
    from a b show "((⊓xa∈A →  x) |-| SKIP) ⊑D (SKIP |-| STOP |-| Mprefix A (λx. CHAOSSKIP A))" 
      by simp
  qed
  then show ?thesis using divergence_refine_def div_free_DFSKIP by blast 
qed

lemma div_free_CHAOS: "D(CHAOS A) = {}"
proof - 
  have "CHAOSSKIP A  ⊑D CHAOS A"
    apply (simp add:CHAOSSKIP_def, rule fix_ind)
    by (simp_all add:le_D_adm monofunI, subst CHAOS_unfold, simp) 
  then show ?thesis using divergence_refine_def div_free_CHAOSSKIP by blast 
qed

lemma div_free_RUN: "D(RUN A) = {}"
proof - 
  have "CHAOS A  ⊑D RUN A"
    by (simp add:CHAOS_def, rule fix_ind, simp_all add:le_D_adm monofunI, subst RUN_unfold, simp) 
  then show ?thesis using divergence_refine_def div_free_CHAOS by blast 
qed

corollary DFSKIP_DF_refine_FD: "DFSKIP A  ⊑FD DF A"
      and DF_RUN_refine_FD: "DF A  ⊑FD RUN A"
      and CHAOS_DF_refine_FD: "CHAOS A  ⊑FD DF A"
      and CHAOSSKIP_CHAOS_refine_FD: "CHAOSSKIP A  ⊑FD CHAOS A"
      and CHAOSSKIP_DFSKIP_refine_FD: "CHAOSSKIP A  ⊑FD DFSKIP A"
  using div_free_DFSKIP[of A] div_free_CHAOSSKIP[of A] div_free_DF[of A] div_free_RUN[of A] 
        div_free_CHAOS[of A] 
        F_D_FD[OF DFSKIP_DF_refine_F, of A] F_D_FD[OF DF_RUN_refine_F, of A] 
        F_D_FD[OF CHAOS_DF_refine_F, of A] F_D_FD[OF CHAOSSKIP_CHAOS_refine_F, of A] 
        F_D_FD[OF CHAOSSKIP_DFSKIP_refine_F, of A]
  by (auto simp add:divergence_refine_def) 


lemma traces_CHAOS_sub: "T(CHAOS A) ⊆ {s. set s ⊆ ev ` A}"
proof(auto)
  fix s sa
  assume "s ∈ T (CHAOS A)" and "sa ∈ set s"
  then show "sa ∈ ev ` A"
    apply (induct s, simp) 
    by (subst (asm) (2) CHAOS_unfold, cases "A={}", auto simp add:T_ndet T_STOP T_Mprefix)  
qed

lemma traces_RUN_sub: "{s. set s ⊆ ev ` A} ⊆ T(RUN A)"
proof(auto)
  fix s
  assume "set s ⊆ ev ` A"
  then show "s ∈ T (RUN A)"
    by (induct s, simp add: Nil_elem_T) (subst RUN_unfold, auto simp add:T_Mprefix)
qed

corollary RUN_all_tickfree_traces1: "T(RUN A) = {s. set s ⊆ ev ` A}" 
      and DF_all_tickfree_traces1: "T(DF A) = {s. set s ⊆ ev ` A}" 
      and CHAOS_all_tickfree_traces1: "T(CHAOS A) = {s. set s ⊆ ev ` A}"
  using DF_RUN_refine_F[THEN le_F_T, simplified trace_refine_def]
        CHAOS_DF_refine_F[THEN le_F_T,simplified trace_refine_def] 
        traces_CHAOS_sub traces_RUN_sub by blast+

corollary RUN_all_tickfree_traces2: "tickFree s ⟹ s ∈ T(RUN UNIV)" 
      and DF_all_tickfree_traces2: "tickFree s ⟹ s ∈ T(DF UNIV)" 
      and CHAOS_all_tickfree_trace2: "tickFree s ⟹ s ∈ T(CHAOS UNIV)"
    apply(simp_all add:tickFree_def RUN_all_tickfree_traces1 
                       DF_all_tickfree_traces1 CHAOS_all_tickfree_traces1)
  by (metis event_set insertE subsetI)+

lemma traces_CHAOSSKIP_sub: "T(CHAOSSKIP A) ⊆ {s. front_tickFree s ∧ set s ⊆ (ev ` A ∪ {tick})}"
proof(auto simp add:is_processT2_TR)
  fix s sa
  assume "s ∈ T (CHAOSSKIP A)" and "sa ∈ set s" and "sa ∉ ev ` A"
  then show "sa = tick"
    apply (induct s, simp) 
    by (subst (asm) (2) CHAOSSKIP_unfold, cases "A={}", auto simp add:T_ndet T_STOP T_SKIP T_Mprefix)  
qed

lemma traces_DFSKIP_sub: 
                      "{s. front_tickFree s ∧ set s ⊆ (ev ` A ∪ {tick})} ⊆ T(DFSKIP A::'a process)"
proof(auto)
  fix s
  assume a:"front_tickFree s" and b:"set s ⊆ insert tick (ev ` A)"
  have c:"front_tickFree ((tick::'a event) # s) ⟹ s = []" for s
    by (metis butlast.simps(2) butlast_snoc front_tickFree_charn list.distinct(1) tickFree_Cons) 
  with a b show "s ∈ T (DFSKIP A)"
    apply (induct s, simp add: Nil_elem_T, subst DFSKIP_unfold, cases "A={}") 
     apply (subst DFSKIP_unfold, cases "A={}")
      apply(auto simp add:T_Mprefix T_mndet write0_def T_SKIP T_ndet T_STOP)
    apply (metis append_Cons append_Nil front_tickFree_charn front_tickFree_mono)
    by (metis append_Cons append_Nil front_tickFree_mono)
  qed

corollary DFSKIP_all_front_tickfree_traces1: 
                              "T(DFSKIP A) = {s. front_tickFree s ∧ set s ⊆ (ev ` A ∪ {tick})}" 
      and CHAOSSKIP_all_front_tickfree_traces1: 
                              "T(CHAOSSKIP A) = {s. front_tickFree s ∧ set s ⊆ (ev ` A ∪ {tick})}"
  using CHAOSSKIP_DFSKIP_refine_F[THEN le_F_T, simplified trace_refine_def]
        traces_CHAOSSKIP_sub traces_DFSKIP_sub by blast+

corollary DFSKIP_all_front_tickfree_traces2: "front_tickFree s ⟹ s ∈ T(DFSKIP UNIV)" 
      and CHAOSSKIP_all_front_tickfree_traces2: "front_tickFree s ⟹ s ∈ T(CHAOSSKIP UNIV)"
   apply(simp_all add:tickFree_def DFSKIP_all_front_tickfree_traces1 
                      CHAOSSKIP_all_front_tickfree_traces1)
  by (metis event_set subsetI)+

corollary DFSKIP_has_all_traces: "DFSKIP UNIV ⊑T P"
      and CHAOSSKIP_has_all_traces: "CHAOSSKIP UNIV ⊑T P"
  apply (simp add:trace_refine_def DFSKIP_all_front_tickfree_traces2 is_processT2_TR subsetI) 
  by (simp add:trace_refine_def CHAOSSKIP_all_front_tickfree_traces2 is_processT2_TR subsetI) 

end

Theory Properties

―‹ ******************************************************************** 
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : Theorems on DF and LF
 *
 * 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.
 ******************************************************************************›

theory Properties
  imports "Assertions_ext"
begin

section ‹Deadlock Free›

thm deadlock_free_def

lemma deadlock_free_implies_div_free: "deadlock_free P ⟹ D P = {}"
  by (simp add: deadlock_free_def div_free_DF failure_divergence_refine_def le_ref_def)

lemma deadlock_free_implies_non_terminating: "deadlock_free (P::'a process) ⟹ ∀s∈T P. tickFree s"
  unfolding deadlock_free_def apply(drule FD_F, drule le_F_T) unfolding trace_refine_def 
  using DF_all_tickfree_traces1[of "(UNIV::'a set)"] tickFree_def by fastforce 

definition deadlock_free_v2 :: "'a process ⇒ bool"
  where   "deadlock_free_v2 P ≡ DFSKIP UNIV ⊑F P"

lemma deadlock_free_v2_is_right: 
  "deadlock_free_v2 (P::'a process) ⟷ (∀s∈T P. tickFree s ⟶ (s, UNIV::'a event set) ∉ F P)"
proof
  assume a:"deadlock_free_v2 P"
  have "tickFree s ⟶ (s, UNIV) ∉ F (DFSKIP UNIV)" for s::"'a event list"
  proof(induct s)
    case Nil
    then show ?case by (subst DFSKIP_unfold, simp add:F_mndet write0_def F_Mprefix F_ndet F_SKIP)
  next
    case (Cons a s)
    then show ?case 
      by (subst DFSKIP_unfold, simp add:F_mndet write0_def F_Mprefix F_ndet F_SKIP)
  qed
  with a show "∀s∈T P. tickFree s ⟶ (s, UNIV) ∉ F P"
    using deadlock_free_v2_def failure_refine_def by blast
next 
  assume as1:"∀s∈T P. tickFree s ⟶ (s, UNIV) ∉ F P"
  have as2:"front_tickFree s ⟹ (∃aa ∈ UNIV. ev aa ∉ b) ⟹ (s, b) ∈ F (DFSKIP (UNIV::'a set))" 
       for s b
  proof(induct s)
    case Nil
    then show ?case
      by (subst DFSKIP_unfold, auto simp add:F_mndet write0_def F_Mprefix F_ndet F_SKIP)
  next
    case (Cons hda tla)
    then show ?case 
    proof(simp add:DFSKIP_def fix_def)
      define Y where "Y ≡ λi. iterate i⋅(Λ x. (⊓xa∈(UNIV::'a set) →  x) ⊓ SKIP)⋅⊥"
      assume a:"front_tickFree (hda # tla)" and b:"front_tickFree tla ⟹ (tla, b) ∈ F (⨆i. Y i)"
             and c:"∃aa. ev aa ∉ b"
      from Y_def have cc:"chain Y" by simp
      from b have d:"front_tickFree tla ⟹ ∃aa∈UNIV. ev aa ∉ b ⟹(tla, b) ∈ F (Y i)" for i 
        using F_LUB[OF cc] limproc_is_thelub[OF cc] by simp
      from Y_def have e:"F(mndet UNIV (λx. Y i) ⊓ SKIP) ⊆ F (Y (Suc i))" for i by(simp)
      from a have f:"tla ≠ [] ⟹ hda ≠ tick" "front_tickFree tla"
        apply (metis butlast.simps(2) butlast_snoc front_tickFree_charn 
                      list.distinct(1) tickFree_Cons)
        by (metis a append_Cons append_Nil front_tickFree_Nil front_tickFree_mono) 
      have g:"(hda#tla, b) ∈ F (Y (Suc i))" for i
        using f c e[of i] d[of i] 
        by (auto simp: F_mndet write0_def F_Mprefix Y_def F_ndet F_SKIP) (metis event.exhaust)+ 
      have h:"(hda#tla, b) ∈ F (Y 0)"
        using NF_ND cc g po_class.chainE proc_ord2a by blast
      from a b c show "(hda#tla, b) ∈ F (⨆i. Y i)"
        using F_LUB[OF cc] is_ub_thelub[OF cc] 
        by (metis D_LUB_2 cc g limproc_is_thelub po_class.chainE proc_ord2a process_charn) 
    qed   
  qed
  show "deadlock_free_v2 P"
  proof(auto simp add:deadlock_free_v2_def failure_refine_def)
    fix s b
    assume as3:"(s, b) ∈ F P"
    hence a1:"s ∈ T P" "front_tickFree s" 
       using F_T apply blast
      using as3 is_processT2 by blast
    show "(s, b) ∈ F (DFSKIP UNIV)" 
    proof(cases "tickFree s")
      case FT_True:True
      hence a2:"(s, UNIV) ∉ F P"
        using a1 as1 by blast
      then show ?thesis 
        by (metis FT_True UNIV_I UNIV_eq_I a1(2) as2 as3 emptyE event.exhaust 
                  is_processT6_S1 tickFree_implies_front_tickFree_single) 
    next
      case FT_False: False                                                                 
      then show ?thesis 
        by (meson T_F_spec UNIV_witness a1(2) append_single_T_imp_tickFree 
                  as2 emptyE is_processT5_S7)
    qed 
  qed
qed  

lemma deadlock_free_v2_implies_div_free: "deadlock_free_v2 P ⟹ D P = {}"
  by (metis F_T append_single_T_imp_tickFree deadlock_free_v2_is_right ex_in_conv 
            nonTickFree_n_frontTickFree process_charn)

corollary deadlock_free_v2_FD: "deadlock_free_v2 P = DFSKIP UNIV ⊑FD P"
  unfolding deadlock_free_v2_def 
  using deadlock_free_v2_implies_div_free FD_F F_D_FD deadlock_free_v2_def divergence_refine_def 
  by fastforce 

lemma all_events_refusal: 
                        "(s, {tick} ∪ ev ` (events_of P)) ∈ F P ⟹ (s, UNIV::'a event set) ∈ F P"
proof -
  assume a1:"(s, {tick} ∪ ev ` events_of P) ∈ F P"
  { assume "(s, UNIV) ∉ F P"
    then obtain c where "c ∉ {tick} ∪ ev ` events_of P ∧ s @ [c] ∈ T P"
      using is_processT5_S1[of s "{tick} ∪ ev ` events_of P" P 
            "UNIV - ({tick} ∪ ev ` events_of P)", simplified] F_T a1 by auto
    hence False by (simp add:events_of_def, cases c) fastforce+
  }  
  with a1 show "(s, UNIV) ∈ F P" by blast 
qed

corollary deadlock_free_v2_is_right_wrt_events:
  "deadlock_free_v2 (P::'a process) ⟷ 
                                  (∀s∈T P. tickFree s ⟶ (s, {tick} ∪ ev ` (events_of P)) ∉ F P)"
  unfolding deadlock_free_v2_is_right using all_events_refusal apply auto 
  using is_processT4 by blast 

lemma deadlock_free_is_deadlock_free_v2:
  "deadlock_free P ⟹ deadlock_free_v2 P"
  using DFSKIP_DF_refine_FD deadlock_free_def deadlock_free_v2_FD trans_FD by blast 


section ‹Non-terminating Runs›

definition non_terminating  :: "'a process ⇒ bool"
  where   "non_terminating P ≡ RUN UNIV ⊑T P"

corollary non_terminating_refine_DF: "non_terminating P = DF UNIV ⊑T P"
  and non_terminating_refine_CHAOS: "non_terminating P = CHAOS UNIV ⊑T P"
  by (simp_all add: DF_all_tickfree_traces1 RUN_all_tickfree_traces1 CHAOS_all_tickfree_traces1 
                    non_terminating_def trace_refine_def)

lemma non_terminating_is_right: "non_terminating (P::'a process) ⟷ (∀s∈T P. tickFree s)"
  apply (rule iffI)
  by (auto simp add:non_terminating_def trace_refine_def tickFree_def RUN_all_tickfree_traces1)[1]
     (auto simp add:non_terminating_def trace_refine_def RUN_all_tickfree_traces2)

lemma nonterminating_implies_div_free: "non_terminating P ⟹ D P = {}"
  unfolding non_terminating_is_right
  by (metis NT_ND equals0I front_tickFree_charn process_charn tickFree_Cons tickFree_append) 

lemma non_terminating_implies_F: "non_terminating P ⟹ CHAOS UNIV ⊑F P"
  apply(auto simp add: non_terminating_is_right failure_refine_def)
  using CHAOS_has_all_tickFree_failures F_T by blast 

corollary non_terminating_F: "non_terminating P = CHAOS UNIV ⊑F P"
  by (auto simp add:non_terminating_implies_F non_terminating_refine_CHAOS le_F_T)

corollary non_terminating_FD: "non_terminating P = CHAOS UNIV ⊑FD P"
  unfolding non_terminating_F
  using div_free_CHAOS nonterminating_implies_div_free FD_F F_D_FD divergence_refine_def 
        non_terminating_F by fastforce 


section ‹Lifelock Freeness›

thm lifelock_free_def

corollary lifelock_free_is_non_terminating: "lifelock_free P = non_terminating P"
  unfolding lifelock_free_def non_terminating_FD by rule

lemma div_free_divergence_refine:
  "D P = {} ⟷ CHAOSSKIP UNIV ⊑D P" 
  "D P = {} ⟷ CHAOS UNIV ⊑D P" 
  "D P = {} ⟷ RUN UNIV ⊑D P" 
  "D P = {} ⟷ DFSKIP UNIV ⊑D P" 
  "D P = {} ⟷ DF UNIV ⊑D P" 
  by (simp_all add: div_free_CHAOSSKIP div_free_CHAOS div_free_RUN div_free_DF div_free_DFSKIP 
                    divergence_refine_def)

definition lifelock_free_v2 :: "'a process ⇒ bool"
  where   "lifelock_free_v2 P ≡ CHAOSSKIP UNIV ⊑FD P"

lemma div_free_is_lifelock_free_v2: "lifelock_free_v2 P ⟷ D P = {}"
  using CHAOSSKIP_has_all_failures_Un FD_D F_D_FD div_free_divergence_refine(1) lifelock_free_v2_def 
  by blast
  
lemma lifelock_free_is_lifelock_free_v2: "lifelock_free P ⟹ lifelock_free_v2 P"
  by (simp add: FD_D div_free_divergence_refine(2) div_free_is_lifelock_free_v2 lifelock_free_def)

corollary deadlock_free_v2_is_lifelock_free_v2: "deadlock_free_v2 P ⟹ lifelock_free_v2 P"
  by (simp add: deadlock_free_v2_implies_div_free div_free_is_lifelock_free_v2)


section ‹New laws›

lemma non_terminating_seq: "non_terminating P ⟹ (P `;` Q) = P"
  apply(auto simp add: non_terminating_is_right Process_eq_spec D_seq F_seq F_T is_processT7)
      using process_charn apply blast
    using process_charn apply blast
   using F_T is_processT5_S2a apply fastforce
  using D_T front_tickFree_Nil by blast

lemma non_terminating_inter: "non_terminating P ⟹ lifelock_free_v2 Q ⟹ non_terminating (P ⟦C⟧ Q)"
  apply(auto simp add: non_terminating_is_right div_free_is_lifelock_free_v2 T_sync) 
  apply (metis equals0D ftf_syn1 ftf_syn21 insertI1 tickFree_def)
  apply (meson NT_ND is_processT7_S tickFree_append)
  by (metis D_T empty_iff ftf_syn1 ftf_syn21 insertI1 tickFree_def)


end

Theory Fix_ind_ext

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : More Fixpoint and k-Induction Schemata
 *
 * 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 ‹ Advanced Induction Schemata ›

theory Fix_ind_ext

imports HOLCF

begin

section‹k-fixpoint-induction›

lemma nat_k_induct: 
  fixes k::nat
  assumes "∀i<k. P i" and "∀n0. (∀i<k. P (n0+i)) ⟶ P (n0+k)"
  shows "P (n::nat)"
proof(induct rule:nat_less_induct)
  case (1 n)
  then show ?case 
    apply(cases "n < k") 
     using assms(1) apply blast
    using assms(2)[rule_format, of "n-k"] by auto
qed

thm fix_ind fix_ind2 

lemma fix_ind_k:
  fixes k::nat
  assumes adm: "adm P"
  assumes base_k_steps: "∀i<k. P (iterate i⋅f⋅⊥)"
  assumes step: "⋀x. (∀i<k.  P (iterate i⋅f⋅x)) ⟹ P (iterate k⋅f⋅x)"
  shows "P (fix⋅f)"
  unfolding fix_def2 apply (rule admD [OF adm chain_iterate])
  apply(rule nat_k_induct[of k], simp add: base_k_steps) 
  using step by (subst (1 2) add.commute, unfold iterate_iterate[symmetric]) blast 

lemma nat_k_skip_induct:
  fixes k::nat
  assumes "k ≥ 1" and "∀i<k. P i" and "∀n0. P (n0) ⟶ P (n0+k)"
  shows "P (n::nat)"
proof(induct rule:nat_less_induct)
  case (1 n)
  then show ?case 
    apply(cases "n < k") 
     using assms(2) apply blast
    using assms(3)[rule_format, of "n-k"] assms(1) by auto
qed

lemma fix_ind_k_skip:
  fixes k::nat
  assumes k_1: "k ≥ 1"
  assumes adm: "adm P"
  assumes base_k_steps: "∀i<k. P (iterate i⋅f⋅⊥)"
  assumes step: "⋀x. P x ⟹ P (iterate k⋅f⋅x)"
  shows "P (fix⋅f)"
  unfolding fix_def2 apply (rule admD [OF adm chain_iterate])
  apply(rule nat_k_skip_induct[of k]) 
  using k_1 base_k_steps apply auto
  using step by (subst add.commute, unfold iterate_iterate[symmetric]) blast

thm parallel_fix_ind

section‹Parallel fixpoint-induction›

lemma parallel_fix_ind_inc:
  assumes adm: "adm (λx. P (fst x) (snd x))"
  assumes base_fst: "⋀y. P ⊥ y" and base_snd: "⋀x. P x ⊥"
  assumes step: "⋀x y. P x y ⟹ P (G⋅x) y ⟹ P x (H⋅y) ⟹ P (G⋅x) (H⋅y)"
  shows "P (fix⋅G) (fix⋅H)"
proof -
  from adm have adm': "adm (case_prod P)"
    unfolding split_def .
  have "P (iterate i⋅G⋅⊥) (iterate j⋅H⋅⊥)" for i j
  proof(induct "i+j" arbitrary:i j rule:nat_less_induct)
    case 1
    { fix i' j'
      assume i:"i = Suc i'" and j:"j = Suc j'"
      have "P (iterate i'⋅G⋅⊥) (iterate j'⋅H⋅⊥)" 
       and "P (iterate i'⋅G⋅⊥) (iterate j⋅H⋅⊥)" 
       and "P (iterate i⋅G⋅⊥) (iterate j'⋅H⋅⊥)"
        using "1.hyps" add_strict_mono i j apply blast 
        using "1.hyps" i apply auto[1] 
        using "1.hyps" j by auto
      hence ?case by (simp add: i j step)
    }
    thus ?case
      apply(cases i, simp add:base_fst)
      apply(cases j, simp add:base_snd)
      by assumption
  qed
  then have "⋀i. case_prod P (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥)"
    by simp
  then have "case_prod P (⨆i. (iterate i⋅G⋅⊥, iterate i⋅H⋅⊥))"
    by - (rule admD [OF adm'], simp, assumption)
  then have "P (⨆i. iterate i⋅G⋅⊥) (⨆i. iterate i⋅H⋅⊥)"
    by (simp add: lub_Pair)  
  then show "P (fix⋅G) (fix⋅H)"
    by (simp add: fix_def2)
qed

end

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 "Properties" "Fix_ind_ext"

begin

section‹Deterministic normal-forms with explicit state›

abbreviation "P_dnorm Tr Up ≡ (μ X. (λ s. □ e ∈ (Tr s) → X (Up s e)))"

notation P_dnorm ("Pnorm⟦_,_⟧" 60)

lemma dnorm_cont[simp]:
  fixes Tr::"'state::type ⇒ 'event::type set" and Up::"'state ⇒ 'event ⇒ 'state"
  shows "cont (λX. (λs. □ e ∈ (Tr s) → X (Ur 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 Tr1 ::"'state1::type ⇒ 'event::type set" and Tr2::"'state2::type ⇒ 'event set" 
    and Up1 ::"'state1 ⇒ 'event ⇒ 'state1" and Up2::"'state2 ⇒ 'event ⇒ 'state2"
  defines P: "P ≡ Pnorm⟦Tr1,Up1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ Pnorm⟦Tr2,Up2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")

  assumes indep: ‹∀s1 s2. Tr1 s1 ∩ Tr2 s2 = {}›

  defines Tr: "Tr ≡ (λ(s1,s2). Tr1 s1 ∪ Tr2 s2)"
  defines Up: "Up ≡ (λ(s1,s2) e. if e ∈ Tr1 s1 then (Up1 s1 e,s2)
                                else if e ∈ Tr2 s2 then (s1, Up2 s2 e)
                                else (s1,s2))"  
  defines S: "S ≡ Pnorm⟦Tr,Up⟧" (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) ⊑ S (s1, s2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind_inc[of "λx y. ∀ s1 s2. (x s1 ||| y s2) ⊑ S (s1,s2)"])
      case adm:1                                       
      then show ?case
        by (intro adm_all adm_below) (simp_all add: cont2cont_fun)
    next
      case base_fst:(2 y)
      then show ?case by (metis Inter_commute app_strict minimal par_Int_bot) 
    next
      case base_snd:(3 x)
      then show ?case by (simp add: par_Int_bot)
    next
      case step:(4 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_Par_Int[where C="{}", simplified])
          apply(subst S_rec, simp add: Tr Up mprefix_Un_distr)
          apply(intro mono_det_ref mono_mprefix_ref)
          using step(3)[simplified] indep apply simp
          using step(2)[simplified] indep by fastforce
      qed
    qed     
  have dir2: "∀ s1 s2.  S (s1, s2) ⊑ (P s1 ||| Q s2)"
    proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s1 s2. x (s1,s2) ⊑ (P s1 ||| Q s2)" 1])
      case adm:1
      show ?case  by (intro adm_all adm_below) (simp_all add: cont_fun) 
    next
      case base_k_steps:2
      then show ?case by simp
    next
      case step:(3 x)
      then show ?case (is "∀ s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        have P_rec_sym:"Mprefix (Tr1 s1) (λe. P (Up1 s1 e)) = P s1" using P_rec by metis
        have Q_rec_sym:"Mprefix (Tr2 s2) (λe. Q (Up2 s2 e)) = Q s2" using Q_rec by metis
        show "?C s1 s2"
          apply(simp add: Tr Up mprefix_Un_distr)
          apply(subst P_rec, subst Q_rec, subst mprefix_Par_Int[where C="{}", simplified])
          apply(intro mono_det_ref mono_mprefix_ref)
          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 below_antisym by blast
qed

section ‹Synchronous product lemma›
lemma dnorm_par:  
  fixes Tr1 ::"'state1::type ⇒ 'event::type set" and Tr2::"'state2::type ⇒ 'event set" 
    and Up1 ::"'state1 ⇒ 'event ⇒ 'state1" and Up2::"'state2 ⇒ 'event ⇒ 'state2"
  defines P: "P ≡ Pnorm⟦Tr1,Up1⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  defines Q: "Q ≡ Pnorm⟦Tr2,Up2⟧" (is "Q ≡ fix⋅(Λ X. ?Q X)")

  defines Tr: "Tr ≡ (λ(s1,s2). Tr1 s1 ∩ Tr2 s2)"
  defines Up: "Up ≡ (λ(s1,s2) e. (Up1 s1 e, Up2 s2 e))"  
  defines S: "S ≡ Pnorm⟦Tr,Up⟧" (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) ⊑ S (s1, s2)"
  proof(subst P, subst Q, 
        induct rule:parallel_fix_ind[of "λx y. ∀ s1 s2. (x s1 || y s2) ⊑ S (s1,s2)"])
      case adm:1
      then show ?case
        by (intro adm_all adm_below) (simp_all add: cont2cont_fun)
    next
      case base:2
      then show ?case by (simp add: par_Int_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_Par_distr[where C="UNIV", simplified])
          apply(subst S_rec, simp add: Tr Up mprefix_Un_distr)
          by (simp add:step mono_mprefix_ref)
      qed
    qed     
  have dir2: "∀ s1 s2.  S (s1, s2) ⊑ (P s1 || Q s2)"
    proof(subst S, induct rule:fix_ind_k[of "λx. ∀ s1 s2. x (s1,s2) ⊑ (P s1 || Q s2)" 1])
      case adm:1
      show ?case  by (intro adm_all adm_below) (simp_all add: cont_fun) 
    next
      case base_k_steps:2
      then show ?case by simp
    next
      case step:(3 x)
      then show ?case (is "∀ s1 s2. ?C s1 s2")
      proof(intro allI)
        fix s1 s2
        have P_rec_sym:"Mprefix (Tr1 s1) (λe. P (Up1 s1 e)) = P s1" using P_rec by metis
        have Q_rec_sym:"Mprefix (Tr2 s2) (λe. Q (Up2 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_Par_distr[where C="UNIV", simplified])
          apply(rule mono_mprefix_ref) 
          using step by auto
      qed
    qed
  from dir1 dir2 show ?thesis using below_antisym by blast
qed

section‹Consequences›
―‹reachable states from one starting state›
inductive_set ℜ for Tr ::"'state::type ⇒ 'event::type set" 
                and Up::"'state ⇒ 'event ⇒ 'state" 
                and s0::'state 
  where rbase: "s0 ∈ ℜ Tr Up s0"
      | rstep: "s ∈ ℜ Tr Up s0 ⟹ e ∈ Tr s  ⟹ Up s e ∈ ℜ Tr Up s0"



―‹Deadlock freeness›
lemma deadlock_free_dnorm_ :
  fixes Tr ::"'state::type ⇒ 'event::type set" 
    and Up ::"'state ⇒ 'event ⇒ 'state" 
    and s0::'state 
  assumes non_reachable_sink: "∀s ∈ ℜ Tr Up s0. Tr s ≠ {}"
  defines P: "P ≡ Pnorm⟦Tr,Up⟧" (is "P ≡ fix⋅(Λ X. ?P X)")
  shows  "s ∈ ℜ Tr Up s0 ⟹ deadlock_free_v2 (P s)"
proof(unfold deadlock_free_v2_FD DFSKIP_def, induct arbitrary:s rule:fix_ind)
  show "adm (λa. ∀x. x ∈ ℜ Tr Up s0 ⟶ a ⊑FD P x)" by (simp add: le_FD_adm monofun_def) 
next
  fix s :: "'state" 
  show "s ∈ ℜ Tr Up s0 ⟹ ⊥ ⊑FD P s" by simp
next
  fix s :: "'state"  and x :: "'event process"
  have P_rec: "P = ?P P" using fix_eq[of "(Λ X. ?P X)"] P by simp 
  assume 1 : "⋀s. s ∈ ℜ Tr Up s0 ⟹ x ⊑FD P s" 
   and   2 : "s ∈ ℜ Tr Up s0 "
  from   1 2 show "(Λ x. (⊓xa∈UNIV →  x) ⊓ SKIP)⋅x ⊑FD P s"
    apply(simp add:failure_divergence_refine_def)
    apply(subst P_rec, rule_tac trans_FD[simplified failure_divergence_refine_def, 
                       rotated, OF Mprefix_refines_Mndet])
    apply(rule_tac CSP.mono_ndet_FD_left)      
    by (metis CSP.mono_ndet_FD_right rstep empty_not_UNIV mndet_distrib mono_mndet_FD 
              non_reachable_sink sup_top_left)
qed



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

end

Theory CopyBuffer_props

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : The Copy-Buffer Example Revisited
 *
 * 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‹Examples›

section‹CopyBuffer Refinement over an infinite alphabet›

theory     CopyBuffer_props
 imports   "HOL-CSP.CopyBuffer" "Properties"
begin 

subsection‹ The Copy-Buffer vs. reference processes ›

lemma DF_COPY: "(DF (range left ∪ range right)) ⊑FD COPY"
    apply(simp add:DF_def,rule fix_ind2, simp_all)
  unfolding failure_divergence_refine_def 
proof -
  show "adm (λa. a ≤ COPY)"   by(rule le_adm, simp_all add:monofunI)
next
    have 1:"(⊓xa∈ range left ∪ range right → ⊥) ≤ (⊓xa∈ range left →  ⊥)"
      using mndet_subset_FD by (metis UNIV_I empty_iff imageI)
    have 2:"(⊓xa∈ range left →  ⊥) ≤ (left`?`x →  ⊥)" 
      unfolding read_def
      by (metis Mprefix_refines_Mndet comp_apply dual_order.antisym mono_mprefix_FD order_refl)

  show "(⊓x∈range left ∪ range right →  ⊥) ≤ COPY"
    by (metis (mono_tags, lifting)  1 2 COPY_rec bot_less1 mono_read_FD order.trans)
next
  fix P::"'a channel process"
  assume  *: "P ≤ COPY" and ** : "(⊓x∈range left ∪ range right →  P) ≤ COPY"
    have 1:"(⊓xa∈ range left ∪ range right →  P) ≤ (⊓xa∈ range right →  P)"
      using mndet_subset_FD by (metis UNIV_I Un_commute empty_iff imageI)
    have 2:"(⊓xa∈ range right →  P) ≤ (right`!`x →  P)" for x
      using mndet_subset_FD[of "{right x}" "range right"]
      by(simp add:write_def write0_def mndet_unit)
    from 1 2 have ab:"(⊓xa∈ range left ∪ range right →  P) ≤ (right`!`x →  P)" for x
      using dual_order.trans by blast
    hence 3:"(left`?`x → (⊓xa∈ range left ∪ range right →  P)) ≤ (left`?`x →(right`!`x →  P))"
      by (simp add: mono_read_FD)
    have 4:"⋀X. (⊓xa∈ range left ∪ range right → X) ≤ (⊓xa∈ range left → X)"
      using mndet_subset_FD by (metis UNIV_I empty_iff imageI)
    have 5:"⋀X. (⊓xa∈ range left → X) ≤ (left`?`x → X)"
      unfolding read_def
      by (metis Mprefix_refines_Mndet comp_apply dual_order.antisym mono_mprefix_FD order_refl)
    from 3 4[of "(⊓xa∈ range left ∪ range right →  P)"] 
         5  [of "(⊓xa∈ range left ∪ range right →  P)"] 
    have 6:"(⊓xa∈ range left ∪ range right → 
                    (⊓xa∈ range left ∪ range right →  P)) ≤ (left`?`x → (right`!`x →  P))"
      by (meson dual_order.trans)
    from * ** have 7:"(left`?`x → (right`!`x →  P)) ≤ (left`?`x → (right`!`x →  COPY))"
      by (simp add: mono_read_FD mono_write_FD)

  show "(⊓x∈range left ∪ range right →  ⊓x∈range left ∪ range right →  P) ≤ COPY"
    by (metis (mono_tags, lifting) 6 7  COPY_rec dual_order.trans)
qed

subsection‹ ... and abstract consequences ›

corollary df_COPY: "deadlock_free COPY"
      and lf_COPY: "lifelock_free COPY"
   apply (meson DF_COPY DF_Univ_freeness UNIV_not_empty image_is_empty sup_eq_bot_iff)
  by (meson CHAOS_DF_refine_FD DF_COPY DF_Univ_freeness UNIV_not_empty deadlock_free_def 
            image_is_empty lifelock_free_def sup_eq_bot_iff trans_FD)

corollary df_v2_COPY: "deadlock_free_v2 COPY" 
      and lf_v2_COPY: "lifelock_free_v2 COPY"
      and nt_COPY: "non_terminating COPY"
  apply (simp add: df_COPY deadlock_free_is_deadlock_free_v2)
  apply (simp add: lf_COPY lifelock_free_is_lifelock_free_v2)
  using lf_COPY lifelock_free_is_non_terminating by blast

lemma DF_SYSTEM: "DF UNIV ⊑FD SYSTEM"
  using DF_subset[of "(range left ∪ range right)" UNIV, simplified]
  impl_refines_spec[THEN le_approx_implies_le_ref] DF_COPY 
  failure_divergence_refine_def trans_FD by blast 

corollary df_SYSTEM: "deadlock_free SYSTEM"
      and lf_SYSTEM: "lifelock_free SYSTEM"
  apply (simp add: DF_SYSTEM deadlock_free_def)
  using CHAOS_DF_refine_FD DF_SYSTEM lifelock_free_def trans_FD by blast 

corollary df_v2_SYSTEM: "deadlock_free_v2 SYSTEM" 
      and lf_v2_SYSTEM: "lifelock_free_v2 SYSTEM"
      and nt_SYSTEM: "non_terminating SYSTEM"
  apply (simp add: df_SYSTEM deadlock_free_is_deadlock_free_v2)
  apply (simp add: lf_SYSTEM lifelock_free_is_lifelock_free_v2)
  using lf_SYSTEM lifelock_free_is_non_terminating by blast

end

Theory DiningPhilosophers

(*<*)
―‹ ********************************************************************
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : Example on Structural Parameterisation: Dining Philosophers
 *
 * 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.
 *
 * TrHIS SOFTrWARE IS PROVIDED BY TrHE COPYRIGHTr HOLDERS AND CONTrRIBUTrORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTrIES, INCLUDING, BUTr NOTr
 * LIMITrED TrO, TrHE IMPLIED WARRANTrIES OF MERCHANTrABILITrY AND FITrNESS FOR
 * A PARTrICULAR PURPOSE ARE DISCLAIMED. IN NO EVENTr SHALL TrHE COPYRIGHTr
 * OWNER OR CONTrRIBUTrORS BE LIABLE FOR ANY DIRECTr, INDIRECTr, INCIDENTrAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTrIAL DAMAGES (INCLUDING, BUTr NOTr
 * LIMITrED TrO, PROCUREMENTr OF SUBSTrITrUTrE GOODS OR SERVICES; LOSS OF USE,
 * DATrA, OR PROFITrS; OR BUSINESS INTrERRUPTrION) HOWEVER CAUSED AND ON ANY
 * TrHEORY OF LIABILITrY, WHETrHER IN CONTrRACTr, STrRICTr LIABILITrY, OR TrORTr
 * (INCLUDING NEGLIGENCE OR OTrHERWISE) ARISING IN ANY WAY OUTr OF TrHE USE
 * OF TrHIS SOFTrWARE, EVEN IF ADVISED OF TrHE POSSIBILITrY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)

section‹ Generalized Dining Philosophers ›

theory     DiningPhilosophers
 imports   "Process_norm"
begin

subsection ‹Preliminary lemmas for proof automation›

lemma Suc_mod: "n > 1 ⟹ i ≠ Suc i mod n"
  by (metis One_nat_def mod_Suc mod_if mod_mod_trivial n_not_Suc_n)

lemmas suc_mods = Suc_mod Suc_mod[symmetric]

lemma l_suc: "n > 1 ⟹ ¬ n ≤ Suc 0"
  by simp

lemma minus_suc: "n > 0 ⟹ n - Suc 0 ≠ n"
  by linarith

lemma numeral_4_eq_4:"4 = Suc (Suc (Suc (Suc 0)))"
  by simp

lemma numeral_5_eq_5:"5 = Suc (Suc (Suc (Suc (Suc 0))))"
  by simp

subsection‹The dining processes definition›

locale DiningPhilosophers =

  fixes N::nat
  assumes N_g1[simp] : "N > 1"

begin

datatype dining_event  = picks (phil:nat) (fork:nat)
                       | putsdown (phil:nat) (fork:nat)

definition RPHIL::  "nat ⇒ dining_event process"
 where "RPHIL i = (μ X. (picks i i → (picks i (i-1) → (putsdown i (i-1) → (putsdown i i → X)))))"

definition LPHIL0::  "dining_event process"
  where "LPHIL0 = (μ X. (picks 0 (N-1) → (picks 0 0 → (putsdown 0 0 → (putsdown 0 (N-1) → X)))))"

definition FORK  :: "nat ⇒ dining_event process"
  where "FORK i = (μ X.   (picks i i → (putsdown i i → X))
                        □ (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → X)))"


abbreviation "foldPHILs n ≡ fold (λ i P. P ||| RPHIL i) [1..< n] (LPHIL0)"
abbreviation "foldFORKs n ≡ fold (λ i P. P ||| FORK i) [1..< n] (FORK 0)"

abbreviation "PHILs ≡ foldPHILs N"
abbreviation "FORKs ≡ foldFORKs N"

corollary FORKs_def2: "FORKs = fold (λ i P. P ||| FORK i) [0..< N] SKIP"
  using N_g1 by (subst (2) upt_rec, auto) (metis (no_types, lifting) Inter_commute Inter_skip1)

corollary "N = 3 ⟹ PHILs = (LPHIL0 ||| RPHIL 1 ||| RPHIL 2)"
  by (subst upt_rec, auto simp add:numeral_2_eq_2)+


definition DINING :: "dining_event process"
  where "DINING = (FORKs || PHILs)"

subsubsection ‹Unfolding rules›

lemma RPHIL_rec:
  "RPHIL i = (picks i i → (picks i (i-1) → (putsdown i (i-1) → (putsdown i i  → RPHIL i))))"
  by (simp add:RPHIL_def write0_def, subst fix_eq, simp)

lemma LPHIL0_rec:
  "LPHIL0 = (picks 0 (N-1) → (picks 0 0 → (putsdown 0 0 → (putsdown 0 (N-1) → LPHIL0))))"
  by (simp add:LPHIL0_def write0_def, subst fix_eq, simp)

lemma FORK_rec: "FORK i = (  (picks i i → (putsdown i i → (FORK i)))
                          □ (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → (FORK i))))"
  by (simp add:FORK_def write0_def, subst fix_eq, simp)

subsection ‹Translation into normal form›

lemma N_pos[simp]: "N > 0"
  using N_g1 neq0_conv by blast

lemmas N_pos_simps[simp] = suc_mods[OF N_g1] l_suc[OF N_g1] minus_suc[OF N_pos]

text ‹The one-fork process›

type_synonym fork_id = nat
type_synonym fork_state = nat

definition fork_transitions:: "fork_id ⇒ fork_state ⇒ dining_event set" ("Trf")
  where "Trf i s = (if s = 0        then {picks i i} ∪ {picks ((i+1) mod N) i}
                    else if s = 1   then {putsdown i i}
                    else if s = 2   then {putsdown ((i+1) mod N) i}
                    else                 {})"
declare Un_insert_right[simp del] Un_insert_left[simp del]

lemma ev_fork_idx[simp]: "e ∈ Trf i s ⟹ fork e = i"
  by (auto simp add:fork_transitions_def split:if_splits)

definition fork_state_update:: "fork_id ⇒ fork_state ⇒ dining_event ⇒ fork_state" ("Upf")
  where "Upf i s e = ( if e = (picks i i)                   then 1
                      else if e = (picks ((i+1) mod N) i)  then 2
                      else                                      0 )"

definition FORKnorm:: "fork_id ⇒ fork_state ⇒ dining_event process"
  where "FORKnorm i = Pnorm⟦Trf i ,Upf i⟧"

lemma FORKnorm_rec:  "FORKnorm i = (λ s. □ e ∈ (Trf i s) → FORKnorm i (Upf i s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trf i s) (λe. X (Upf i s e)))"] FORKnorm_def by simp

lemma FORK_refines_FORKnorm: "FORKnorm i 0 ⊑ FORK i"
proof(unfold FORKnorm_def,
      induct rule:fix_ind_k_skip[where k=2 and f="Λ x.(λs. Mprefix (Trf i s) (λe. x (Upf i s e)))"])
  show "(1::nat) ≤ 2" by simp
next
  show "adm (λa. a 0 ⊑ FORK i)" by (simp add: cont_fun)
next
  case base_k_steps:3
  show ?case (is "∀j<2. (iterate j⋅?f⋅⊥) 0 ⊑ FORK i")
  proof -
    have less_2:"⋀j. (j::nat) < 2 = (j = 0 ∨ j = 1)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑ FORK i" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑ FORK i"
      by (subst FORK_rec)
         (simp add: write0_def
                    fork_transitions_def
                    mprefix_Un_distr mono_det_ref mono_mprefix_ref)
    ultimately show ?thesis by simp
  qed
next
  case step:(4 x)
  then show ?case (is "(iterate 2⋅?f⋅x) 0 ⊑ FORK i")
    by (subst FORK_rec)
       (simp add: write0_def numeral_2_eq_2
                  fork_transitions_def fork_state_update_def
                  mprefix_Un_distr mono_det_ref mono_mprefix_ref)
qed

lemma FORKnorm_refines_FORK: "FORK i ⊑ FORKnorm i 0"
proof(unfold FORK_def,
      induct rule:fix_ind_k_skip[where k=1])
  show "(1::nat) ≤ 1" by simp
next
  show "adm (λa. a ⊑ FORKnorm i 0)" by simp
next
  case base_k_steps:3
  show ?case by simp
next
  case step:(4 x)
  then show ?case (is "iterate 1⋅?f⋅x ⊑ FORKnorm i 0")
    apply (subst FORKnorm_rec)
    apply (simp add: write0_def
                     fork_transitions_def fork_state_update_def
                     mprefix_Un_distr)
    by (subst (1 2) FORKnorm_rec)
       (simp add: fork_transitions_def fork_state_update_def
                  mprefix_Un_distr mono_det_ref mono_mprefix_ref)
qed

lemma FORKnorm_is_FORK: "FORK i = FORKnorm i 0"
  using FORK_refines_FORKnorm FORKnorm_refines_FORK below_antisym by blast


text ‹The all-forks process in normal form›

type_synonym forks_state = "nat list"

definition forks_transitions:: "nat ⇒ forks_state ⇒ dining_event set" ("TrF")
  where "TrF n fs = (⋃i<n. Trf i (fs!i))"

lemma forks_transitions_take: "TrF n fs = TrF n (take n fs)"
  by (simp add:forks_transitions_def)

definition forks_state_update:: "forks_state ⇒ dining_event ⇒ forks_state" ("UpF")
  where "UpF fs e = (let i=(fork e) in fs[i:=(Upf i (fs!i) e)])"

lemma forks_update_take: "take n (UpF fs e) = UpF (take n fs) e"
  unfolding forks_state_update_def
  by (metis nat_less_le nat_neq_iff nth_take order_refl take_update_cancel take_update_swap)

definition FORKsnorm:: "nat ⇒ forks_state ⇒ dining_event process"
  where "FORKsnorm n = Pnorm⟦TrF n ,UpF⟧"

lemma FORKsnorm_rec:  "FORKsnorm n = (λ fs. □ e ∈ (TrF n fs) → FORKsnorm n (UpF fs e))"
  using fix_eq[of "Λ X. (λfs. Mprefix (TrF n fs) (λe. X (UpF fs e)))"] FORKsnorm_def by simp

lemma FORKsnorm_0: "FORKsnorm 0 fs = STOP"
  by (subst FORKsnorm_rec, simp add:forks_transitions_def Mprefix_STOP)

lemma FORKsnorm_1_dir1: "length fs > 0 ⟹ FORKsnorm 1 fs ⊑ (FORKnorm 0 (fs!0))"
proof(unfold FORKsnorm_def,
      induct arbitrary:fs rule:fix_ind_k[where k=1
                                         and f="Λ x. (λfs. Mprefix (TrF 1 fs) (λe. x (UpF fs e)))"])
  case adm:1
  then show ?case by (simp add:cont_fun)
next
  case base_k_steps:2
  then show ?case by simp
next
  case step:(3 X)
  hence "(⋃i<Suc 0. Trf i (fs ! i)) = Trf 0 (fs ! 0)" by auto
  with step show ?case
    apply (subst FORKnorm_rec, simp add:forks_state_update_def forks_transitions_def)
    apply (intro mono_mprefix_ref, safe)
    by (metis ev_fork_idx step.prems list_update_nonempty nth_list_update_eq)
qed

lemma FORKsnorm_1_dir2: "length fs > 0 ⟹ (FORKnorm 0 (fs!0)) ⊑ FORKsnorm 1 fs"
proof(unfold FORKnorm_def,
      induct arbitrary:fs rule:fix_ind_k[where k=1
                                         and f="Λ x. (λs. Mprefix (Trf 0 s) (λe. x (Upf 0 s e)))"])
  case adm:1
  then show ?case by (simp add:cont_fun)
next
  case base_k_steps:2
  then show ?case by simp
next
  case step:(3 X)
  have "(⋃i<Suc 0. Trf i (fs ! i)) = Trf 0 (fs ! 0)" by auto
  with step show ?case
    apply (subst FORKsnorm_rec, simp add:forks_state_update_def forks_transitions_def)
    apply (intro mono_mprefix_ref, safe)
    by (metis ev_fork_idx step.prems list_update_nonempty nth_list_update_eq)
qed

lemma FORKsnorm_1: "length fs > 0 ⟹ (FORKnorm 0 (fs!0)) = FORKsnorm 1 fs"
  using FORKsnorm_1_dir1 FORKsnorm_1_dir2 below_antisym by blast

lemma FORKsnorm_unfold:
"0 < n ⟹ length fs = Suc n ⟹
                              FORKsnorm (Suc n) fs = (FORKsnorm n (butlast fs)|||(FORKnorm n (fs!n)))"
proof(rule below_antisym)
  show "0 < n ⟹ length fs = Suc n ⟹
                               FORKsnorm (Suc n) fs ⊑ (FORKsnorm n (butlast fs)|||FORKnorm n (fs!n))"
  proof(subst FORKsnorm_def,
        induct arbitrary:fs
               rule:fix_ind_k[where k=1
                              and f="Λ x. (λfs. Mprefix (TrF (Suc n) fs) (λe. x (UpF fs e)))"])
    case adm:1
    then show ?case by (simp add:cont_fun)
  next
    case base_k_steps:2
    then show ?case by simp
  next
    case step:(3 X)
    have indep:"∀s1 s2. TrF n s1 ∩ Trf n s2 = {}"
      by (auto simp add:forks_transitions_def fork_transitions_def)
    from step show ?case
      apply (auto simp add:indep dnorm_inter FORKsnorm_def FORKnorm_def)
      apply (subst fix_eq, simp add:forks_transitions_def Un_commute lessThan_Suc nth_butlast)
    proof(rule mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      from 1(4) have a:"fork e = n"
        by (auto simp add:fork_transitions_def split:if_splits)
      show ?case
        using 1(1)[rule_format, of "(UpF fs e)"]
        apply (simp add: 1 a butlast_list_update forks_state_update_def)
        by (metis 1(4) ev_fork_idx lessThan_iff less_not_refl)
    next
      case (2 e m)
      hence a:"e ∉ Trf n (fs ! n)"
        using ev_fork_idx by fastforce
      hence c:"UpF fs e ! n = fs ! n"
        by (metis 2(4) ev_fork_idx forks_state_update_def nth_list_update_neq)
      have d:"UpF (butlast fs) e = butlast (UpF fs e)"
        apply(simp add:forks_state_update_def)
        by (metis butlast_conv_take forks_state_update_def forks_update_take length_list_update)
      from 2 a show ?case
        using 2(1)[rule_format, of "(UpF fs e)"] c d forks_state_update_def by auto
    qed
  qed
next
  have indep:"∀s1 s2. TrF n s1 ∩ Trf n s2 = {}"
    by (auto simp add:forks_transitions_def fork_transitions_def)
  show "0 < n ⟹ length fs = Suc n ⟹
                              (FORKsnorm n (butlast fs)|||FORKnorm n (fs!n)) ⊑ FORKsnorm (Suc n) fs"
    apply (subst FORKsnorm_def, auto simp add:indep dnorm_inter FORKnorm_def)
  proof(rule fix_ind[where
        P="λa. 0 < n ⟶ (∀x. length x = Suc n ⟶ a (butlast x, x ! n) ⊑ FORKsnorm (Suc n) x)",
        rule_format], simp_all, goal_cases)
    case base:1
    then show ?case by (simp add:cont_fun)
  next
    case step:(2 X fs)
    then show ?case
      apply (unfold FORKsnorm_def, subst fix_eq, simp add:forks_transitions_def
                                                          Un_commute lessThan_Suc nth_butlast)
    proof(rule mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      from 1(6) have a:"fork e = n"
        by (auto simp add:fork_transitions_def split:if_splits)
      show ?case
        using 1(1)[rule_format, of "(UpF fs e)"]
        apply (simp add: 1 a butlast_list_update forks_state_update_def)
        using a ev_fork_idx by blast
    next
      case (2 e m)
      have a:"UpF (butlast fs) e = butlast (UpF fs e)"
        apply(simp add:forks_state_update_def)
        by (metis butlast_conv_take forks_state_update_def forks_update_take length_list_update)
      from 2 show ?case
        using 2(1)[rule_format, of "(UpF fs e)"] a forks_state_update_def by auto
    qed
  qed
qed

lemma ft: "0 < n ⟹ FORKsnorm n (replicate n 0) = foldFORKs n"
proof (induct n, simp)
  case (Suc n)
  then show ?case
    apply (auto simp add: FORKsnorm_unfold FORKnorm_is_FORK)
    apply (metis Suc_le_D butlast_snoc replicate_Suc replicate_append_same)
    by (metis FORKsnorm_1 One_nat_def leI length_replicate less_Suc0 nth_replicate replicate_Suc)
qed

corollary FORKs_is_FORKsnorm: "FORKsnorm N (replicate N 0) = FORKs"
  using ft N_pos by simp

text ‹The one-philosopher process in normal form:›

type_synonym phil_id = nat
type_synonym phil_state = nat

definition rphil_transitions:: "phil_id ⇒ phil_state ⇒ dining_event set" ("Trrp")
  where "Trrp i s = ( if      s = 0  then {picks i i}
                     else if s = 1  then {picks i (i-1)}
                     else if s = 2  then {putsdown i (i-1)}
                     else if s = 3  then {putsdown i i}
                     else                {})"

definition lphil0_transitions:: "phil_state ⇒ dining_event set" ("Trlp")
    where "Trlp s = ( if s = 0       then {picks 0 (N-1)}
                     else if s = 1  then {picks 0 0}
                     else if s = 2  then {putsdown 0 0}
                     else if s = 3  then {putsdown 0 (N-1)}
                     else                {})"

corollary rphil_phil: "e ∈ Trrp i s ⟹ phil e = i"
      and lphil0_phil: "e ∈ Trlp s ⟹ phil e = 0"
  by (simp_all add:rphil_transitions_def lphil0_transitions_def split:if_splits)

definition rphil_state_update:: "fork_id ⇒ fork_state ⇒ dining_event ⇒ fork_state" ("Uprp")
  where "Uprp i s e = ( if e = (picks i i)               then 1
                       else if e = (picks i (i-1))      then 2
                       else if e = (putsdown i (i-1))   then 3
                       else                                  0 )"

definition lphil0_state_update:: "fork_state ⇒ dining_event ⇒ fork_state" ("Uplp")
  where "Uplp s e = ( if e = (picks 0 (N-1))         then 1
                     else if e = (picks 0 0)        then 2
                     else if e = (putsdown 0 0)     then 3
                     else                                0 )"

definition RPHILnorm:: "fork_id ⇒ fork_state ⇒ dining_event process"
  where "RPHILnorm i = Pnorm⟦Trrp i,Uprp i⟧"

definition LPHIL0norm:: "fork_state ⇒ dining_event process"
  where "LPHIL0norm = Pnorm⟦Trlp,Uplp⟧"

lemma RPHILnorm_rec:  "RPHILnorm i = (λ s. □ e ∈ (Trrp i s) → RPHILnorm i (Uprp i s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trrp i s) (λe. X (Uprp i s e)))"] RPHILnorm_def by simp

lemma LPHIL0norm_rec:  "LPHIL0norm = (λ s. □ e ∈ (Trlp s) → LPHIL0norm (Uplp s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (Trlp s) (λe. X (Uplp s e)))"] LPHIL0norm_def by simp

lemma RPHIL_refines_RPHILnorm:
  assumes i_pos: "i > 0"
  shows "RPHILnorm i 0 ⊑ RPHIL i"
proof(unfold RPHILnorm_def,
      induct rule:fix_ind_k_skip[where k=4
                                 and f="Λ x. (λs. Mprefix (Trrp i s) (λe. x (Uprp i s e)))"])
  show "(1::nat) ≤ 4" by simp
next
  show "adm (λa. a 0 ⊑ RPHIL i)" by (simp add: cont_fun)
next
  case base_k_steps:3
  show ?case (is "∀j<4. (iterate j⋅?f⋅⊥) 0 ⊑ RPHIL i")
  proof -
    have less_2:"⋀j. (j::nat) < 4 = (j = 0 ∨ j = 1  ∨ j = 2  ∨ j = 3)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑ RPHIL i" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑ RPHIL i"
      by (subst RPHIL_rec)
         (simp add: write0_def rphil_transitions_def mono_mprefix_ref)
    moreover have "(iterate 2⋅?f⋅⊥) 0 ⊑ RPHIL i"
      by (subst RPHIL_rec)
         (simp add: numeral_2_eq_2 write0_def rphil_transitions_def
                    rphil_state_update_def mono_mprefix_ref)
    moreover have "(iterate 3⋅?f⋅⊥) 0 ⊑ RPHIL i"
      by (subst RPHIL_rec)
         (simp add: numeral_3_eq_3 write0_def rphil_transitions_def
                    rphil_state_update_def mono_mprefix_ref minus_suc[OF i_pos])
    ultimately show ?thesis by simp
  qed
next
  case step:(4 x)
  then show ?case (is "(iterate 4⋅?f⋅x) 0 ⊑ RPHIL i")
    apply (subst RPHIL_rec)
    apply (simp add: write0_def numeral_4_eq_4 rphil_transitions_def rphil_state_update_def)
    apply (rule mono_mprefix_ref, auto simp:minus_suc[OF i_pos])+
    using minus_suc[OF i_pos] by auto
qed

lemma LPHIL0_refines_LPHIL0norm: "LPHIL0norm 0 ⊑ LPHIL0"
proof(unfold LPHIL0norm_def,
      induct rule:fix_ind_k_skip[where k=4 and f="Λ x. (λs. Mprefix (Trlp s) (λe. x (Uplp s e)))"])
  show "(1::nat) ≤ 4" by simp
next
  show "adm (λa. a 0 ⊑ LPHIL0)" by (simp add: cont_fun)
next
  case base_k_steps:3
  show ?case (is "∀j<4. (iterate j⋅?f⋅⊥) 0 ⊑ LPHIL0")
  proof -
    have less_2:"⋀j. (j::nat) < 4 = (j = 0 ∨ j = 1  ∨ j = 2  ∨ j = 3)" by linarith
    moreover have "(iterate 0⋅?f⋅⊥) 0 ⊑ LPHIL0" by simp
    moreover have "(iterate 1⋅?f⋅⊥) 0 ⊑ LPHIL0"
      by (subst LPHIL0_rec)
         (simp add: write0_def lphil0_transitions_def mono_mprefix_ref)
    moreover have "(iterate 2⋅?f⋅⊥) 0 ⊑ LPHIL0"
      by (subst LPHIL0_rec)
         (simp add: numeral_2_eq_2 write0_def lphil0_transitions_def
                    lphil0_state_update_def mono_mprefix_ref)
    moreover have "(iterate 3⋅?f⋅⊥) 0 ⊑ LPHIL0"
      by (subst LPHIL0_rec)
         (simp add: numeral_3_eq_3 write0_def lphil0_transitions_def
                    lphil0_state_update_def mono_mprefix_ref)
    ultimately show ?thesis by simp
  qed
next
  case step:(4 x)
  then show ?case (is "(iterate 4⋅?f⋅x) 0 ⊑ LPHIL0")
    by (subst LPHIL0_rec)
       (simp add: write0_def numeral_4_eq_4 lphil0_transitions_def
                  lphil0_state_update_def mono_mprefix_ref)
qed

lemma RPHILnorm_refines_RPHIL:
  assumes i_pos: "i > 0"
  shows "RPHIL i ⊑ RPHILnorm i 0"
proof(unfold RPHIL_def,
      induct rule:fix_ind_k_skip[where k=1])
  show "(1::nat) ≤ 1" by simp
next
  show "adm (λa. a ⊑ RPHILnorm i 0)" by simp
next
  case base_k_steps:3
  show ?case by simp
next
  case step:(4 x)
  then show ?case
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_mprefix_ref, simp)
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_mprefix_ref, simp add:minus_suc[OF i_pos])
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_mprefix_ref, simp add:minus_suc[OF i_pos])
    apply (subst RPHILnorm_rec, simp add: write0_def rphil_transitions_def rphil_state_update_def)
    apply (rule mono_mprefix_ref, simp add:minus_suc[OF i_pos])
    using minus_suc[OF i_pos] by auto
qed

lemma LPHIL0norm_refines_LPHIL0: "LPHIL0 ⊑ LPHIL0norm 0"
proof(unfold LPHIL0_def,
      induct rule:fix_ind_k_skip[where k=1])
  show "(1::nat) ≤ 1" by simp
next
  show "adm (λa. a ⊑ LPHIL0norm 0)" by simp
next
  case base_k_steps:3
  show ?case by simp
next
  case step:(4 x)
  then show ?case (is "iterate 1⋅?f⋅x ⊑ LPHIL0norm 0")
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def)
    apply (rule mono_mprefix_ref, simp)
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def)
    apply (rule mono_mprefix_ref, simp)
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def)
    apply (rule mono_mprefix_ref, simp)
    apply (subst LPHIL0norm_rec, simp add: write0_def lphil0_transitions_def lphil0_state_update_def)
    apply (rule mono_mprefix_ref, simp)
    done
qed

lemma RPHILnorm_is_RPHIL: "i > 0 ⟹ RPHIL i = RPHILnorm i 0"
  using RPHIL_refines_RPHILnorm RPHILnorm_refines_RPHIL below_antisym by blast

lemma LPHIL0norm_is_LPHIL0: "LPHIL0 = LPHIL0norm 0"
  using LPHIL0_refines_LPHIL0norm LPHIL0norm_refines_LPHIL0 below_antisym by blast

subsection ‹The normal form for the global philosopher network›

type_synonym phils_state = "nat list"

definition phils_transitions:: "nat ⇒ phils_state ⇒ dining_event set" ("TrP")
  where "TrP n ps = Trlp (ps!0) ∪ (⋃i∈{1..< n}. Trrp i (ps!i))"

corollary phils_phil: "0 < n ⟹ e ∈ TrP n s ⟹ phil e < n"
  by (auto simp add:phils_transitions_def lphil0_phil rphil_phil)

lemma phils_transitions_take: "0 < n ⟹ TrP n ps = TrP n (take n ps)"
  by (auto simp add:phils_transitions_def)

definition phils_state_update:: "phils_state ⇒ dining_event ⇒ phils_state" ("UpP")
  where "UpP ps e = (let i=(phil e) in if i = 0 then ps[i:=(Uplp (ps!i) e)]
                                       else          ps[i:=(Uprp i (ps!i) e)])"

lemma phils_update_take: "take n (UpP ps e) = UpP (take n ps) e"
  by (cases e) (simp_all add: phils_state_update_def lphil0_state_update_def
                              rphil_state_update_def take_update_swap)

definition PHILsnorm:: "nat ⇒ phils_state ⇒ dining_event process"
  where "PHILsnorm n = Pnorm⟦TrP n,UpP⟧"

lemma PHILsnorm_rec:  "PHILsnorm n = (λ ps. □ e ∈ (TrP n ps) → PHILsnorm n (UpP ps e))"
  using fix_eq[of "Λ X. (λps. Mprefix (TrP n ps) (λe. X (UpP ps e)))"] PHILsnorm_def by simp

lemma PHILsnorm_1_dir1: "length ps > 0 ⟹ PHILsnorm 1 ps ⊑ (LPHIL0norm (ps!0))"
proof(unfold PHILsnorm_def,
      induct arbitrary:ps
             rule:fix_ind_k[where k=1
                            and f="Λ x. (λps. Mprefix (TrP 1 ps) (λe. x (UpP ps e)))"])
  case adm:1
  then show ?case by (simp add:cont_fun)
next
  case base_k_steps:2
  then show ?case by simp
next
  case step:(3 X)
  then show ?case
    apply (subst LPHIL0norm_rec, simp add:phils_state_update_def phils_transitions_def)
    proof (intro mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      with 1(2) show ?case
        using 1(1)[rule_format, of "ps[0 := Uplp (ps ! 0) e]"]
        by (simp add:lphil0_transitions_def split:if_splits)
    qed
qed

lemma PHILsnorm_1_dir2: "length ps > 0 ⟹ (LPHIL0norm (ps!0)) ⊑ PHILsnorm 1 ps"
proof(unfold LPHIL0norm_def,
      induct arbitrary:ps rule:fix_ind_k[where k=1
                                         and f="Λ x. (λs. Mprefix (Trlp s) (λe. x (Uplp s e)))"])
  case adm:1
  then show ?case by (simp add:cont_fun)
next
  case base_k_steps:2
  then show ?case by simp
next
  case step:(3 X)
  then show ?case
    apply (subst PHILsnorm_rec, simp add:phils_state_update_def phils_transitions_def)
    proof (intro mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      with 1(2) show ?case
        using 1(1)[rule_format, of "ps[0 := Uplp (ps ! 0) e]"]
        by (simp add:lphil0_transitions_def split:if_splits)
    qed
qed

lemma PHILsnorm_1: "length ps > 0 ⟹ PHILsnorm 1 ps = (LPHIL0norm (ps!0))"
  using PHILsnorm_1_dir1 PHILsnorm_1_dir2 below_antisym by blast

lemma PHILsnorm_unfold:
  assumes n_pos:"0 < n"
  shows "length ps = Suc n ⟹
                            PHILsnorm (Suc n) ps = (PHILsnorm n (butlast ps)|||(RPHILnorm n (ps!n)))"
proof(rule below_antisym)
  show "length ps = Suc n ⟹ PHILsnorm (Suc n) ps ⊑ (PHILsnorm n (butlast ps)|||RPHILnorm n (ps!n))"
  proof(subst PHILsnorm_def,
        induct arbitrary:ps
               rule:fix_ind_k[where k=1
                              and f="Λ x. (λps. Mprefix (TrP (Suc n) ps) (λe. x (UpP ps e)))"])
    case adm:1
    then show ?case by (simp add:cont_fun)
  next
    case base_k_steps:2
    then show ?case by simp
  next
    case step:(3 X)
    have indep:"∀s1 s2. TrP n s1 ∩ Trrp n s2 = {}"
      using phils_phil rphil_phil n_pos by blast
    from step have tra:"(TrP (Suc n) ps) =(TrP n (butlast ps) ∪ Trrp n (ps ! n))"
      by (auto simp add:n_pos phils_transitions_def nth_butlast Suc_leI
                        atLeastLessThanSuc Un_commute Un_assoc)
    from step show ?case
      apply (auto simp add:indep dnorm_inter PHILsnorm_def RPHILnorm_def)
      apply (subst fix_eq, auto simp add:tra)
    proof(rule mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      hence c:"UpP ps e ! n = ps ! n"
        using 1(3) phils_phil phils_state_update_def step n_pos
        by (cases "phil e", auto) (metis exists_least_iff nth_list_update_neq)
      have d:"UpP (butlast ps) e = butlast (UpP ps e)"
        by (cases "phil e", auto simp add:phils_state_update_def butlast_list_update
                                          lphil0_state_update_def rphil_state_update_def)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(2) length_list_update phils_state_update_def)
      from 1 show ?case
        using 1(1)[rule_format, of "(UpP ps e)"] c d e by auto
    next
      case (2 e)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(2) length_list_update phils_state_update_def)
      from 2 show ?case
        using 2(1)[rule_format, of "(UpP ps e)", OF e] n_pos
        apply(auto simp add: butlast_list_update rphil_phil phils_state_update_def)
        by (meson disjoint_iff_not_equal indep)
    qed
  qed
next
  have indep:"∀s1 s2. TrP n s1 ∩ Trrp n s2 = {}"
    using phils_phil rphil_phil using n_pos by blast

  show "length ps = Suc n ⟹ (PHILsnorm n (butlast ps)|||RPHILnorm n (ps!n)) ⊑ PHILsnorm (Suc n) ps"
    apply (subst PHILsnorm_def, auto simp add:indep dnorm_inter RPHILnorm_def)
  proof(rule fix_ind[where
        P="λa. ∀x. length x = Suc n ⟶ a (butlast x, x ! n) ⊑ PHILsnorm (Suc n) x", rule_format],
        simp_all, goal_cases base step)
    case base
    then show ?case by (simp add:cont_fun)
  next
    case (step X ps)
    hence tra:"(TrP (Suc n) ps) =(TrP n (butlast ps) ∪ Trrp n (ps ! n))"
      by (auto simp add:n_pos phils_transitions_def nth_butlast
                        Suc_leI atLeastLessThanSuc Un_commute Un_assoc)
    from step show ?case
      apply (auto simp add:indep dnorm_inter PHILsnorm_def RPHILnorm_def)
      apply (subst fix_eq, auto simp add:tra)
    proof(rule mono_mprefix_ref, safe, goal_cases)
      case (1 e)
      hence c:"UpP ps e ! n = ps ! n"
        using 1(3) phils_phil phils_state_update_def step n_pos
        by (cases "phil e", auto) (metis exists_least_iff nth_list_update_neq)
      have d:"UpP (butlast ps) e = butlast (UpP ps e)"
        by (cases "phil e", auto simp add:phils_state_update_def butlast_list_update
                                          lphil0_state_update_def rphil_state_update_def)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) step(3) length_list_update phils_state_update_def)
      from 1 show ?case
        using 1(2)[rule_format, of "(UpP ps e)", OF e] c d by auto
    next
      case (2 e)
      have e:"length (UpP ps e) = Suc n"
        by (metis (full_types) 2(3) length_list_update phils_state_update_def)
      from 2 show ?case
        using 2(2)[rule_format, of "(UpP ps e)", OF e] n_pos
        apply(auto simp add: butlast_list_update rphil_phil phils_state_update_def)
        by (meson disjoint_iff_not_equal indep)
    qed
  qed
qed

lemma pt: "0 < n ⟹ PHILsnorm n (replicate n 0) = foldPHILs n"
proof (induct n, simp)
  case (Suc n)
  then show ?case
    apply (auto simp add: PHILsnorm_unfold LPHIL0norm_is_LPHIL0)
     apply (metis Suc_le_eq butlast.simps(2) butlast_snoc RPHILnorm_is_RPHIL
                    nat_neq_iff replicate_append_same replicate_empty)
    by (metis One_nat_def leI length_replicate less_Suc0 PHILsnorm_1 nth_Cons_0 replicate_Suc)
qed

corollary PHILs_is_PHILsnorm: "PHILsnorm N (replicate N 0) = PHILs"
  using pt N_pos by simp

subsection ‹The complete process system under normal form›

definition dining_transitions:: "nat ⇒ phils_state × forks_state ⇒ dining_event set" ("TrD")
  where "TrD n = (λ(ps,fs). (TrP n ps) ∩ (TrF n fs))"

definition dining_state_update::
  "phils_state × forks_state ⇒ dining_event ⇒ phils_state × forks_state" ("UpD")
  where "UpD = (λ(ps,fs) e. (UpP ps e, UpF fs e))"

definition DININGnorm:: "nat ⇒ phils_state × forks_state ⇒ dining_event process"
  where "DININGnorm n = Pnorm⟦TrD n, UpD⟧"

lemma ltsDining_rec:  "DININGnorm n = (λ s. □ e ∈ (TrD n s) → DININGnorm n (UpD s e))"
  using fix_eq[of "Λ X. (λs. Mprefix (TrD n s) (λe. X (UpD s e)))"] DININGnorm_def by simp

lemma DINING_is_DININGnorm: "DINING = DININGnorm N (replicate N 0, replicate N 0)"
proof -
  have "DININGnorm N (replicate N 0, replicate N 0) =
                                        (PHILsnorm N (replicate N 0) || FORKsnorm N (replicate N 0))"
    unfolding DININGnorm_def PHILsnorm_def FORKsnorm_def dining_transitions_def
              dining_state_update_def dnorm_par by simp
  thus ?thesis
    using PHILs_is_PHILsnorm FORKs_is_FORKsnorm DINING_def
    by (simp add: par_comm)
qed

subsection ‹And finally: Philosophers may dine ! Always !›

corollary lphil_states:"Uplp r e = 0 ∨ Uplp r e = 1 ∨ Uplp r e = 2 ∨ Uplp r e = 3"
      and rphil_states:"Uprp i r e = 0 ∨ Uprp i r e = 1 ∨ Uprp i r e = 2 ∨ Uprp i r e = 3"
  unfolding lphil0_state_update_def rphil_state_update_def by auto

lemma dining_events:
"e ∈ TrD N s ⟹
        (∃i∈{1..<N}. e = picks i i ∨ e = picks i (i-1)  ∨ e = putsdown i i ∨ e = putsdown i (i-1))
     ∨ (e = picks 0 0 ∨ e = picks 0 (N-1) ∨ e = putsdown 0 0 ∨ e = putsdown 0 (N-1))"
  by (auto simp add:dining_transitions_def phils_transitions_def rphil_transitions_def
                    lphil0_transitions_def split:prod.splits if_splits)

definition "inv_dining ps fs ≡
            (∀i. Suc i < N ⟶  ((fs!(Suc i) = 1) ⟷ ps!Suc i ≠ 0)) ∧ (fs!(N-1) = 2 ⟷ ps!0 ≠ 0)
          ∧ (∀i < N - 1.                 fs!i = 2 ⟷  ps!Suc i = 2)  ∧   (fs!0 = 1 ⟷ ps!0 = 2)
          ∧ (∀i < N. fs!i = 0 ∨ fs!i = 1 ∨ fs!i = 2)
          ∧ (∀i < N. ps!i = 0 ∨ ps!i = 1 ∨ ps!i = 2 ∨ ps!i = 3)
          ∧ length fs = N ∧ length ps = N"

lemma inv_DINING: "s ∈ ℜ (TrD N) UpD (replicate N 0, replicate N 0) ⟹ inv_dining (fst s) (snd s)"
proof(induct rule:ℜ.induct)
  case rbase
  show ?case
    unfolding inv_dining_def
    by (simp add:dining_transitions_def phils_transitions_def forks_transitions_def
                 lphil0_transitions_def rphil_transitions_def fork_transitions_def)
next
  case (rstep s e)
  from rstep(2,3) show ?case
    apply(auto simp add:dining_transitions_def phils_transitions_def forks_transitions_def
                       lphil0_transitions_def rphil_transitions_def fork_transitions_def
                       lphil0_state_update_def rphil_state_update_def fork_state_update_def
                       dining_state_update_def phils_state_update_def forks_state_update_def
                   split:if_splits prod.split)
    unfolding inv_dining_def
  proof(goal_cases)
    case (1 ps fs)
    then show ?case
      by (simp add:nth_list_update) force
  next
    case (2 ps fs)
    then show ?case
      by (auto simp add:nth_list_update)
  next
    case (3 ps fs)
    then show ?case
      using N_g1 by auto
  next
    case (4 ps fs)
    then show ?case
      by (simp add:nth_list_update) force
  next
    case (5 ps fs)
    then show ?case
      using N_g1 by linarith
  next
    case (6 ps fs)
    then show ?case
      by (auto simp add:nth_list_update)
  next
    case (7 ps fs i)
    then show ?case
      apply (simp add:nth_list_update, intro impI conjI, simp_all)
      by  auto[1] (metis N_pos Suc_pred less_antisym, metis zero_neq_numeral)
  next
    case (8 ps fs i)
    then show ?case
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all)
      by (metis "8"(1) zero_neq_one)+
  next
    case (9 ps fs i)
    then show ?case
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all)
      by (metis N_pos Suc_pred less_antisym) (metis n_not_Suc_n numeral_2_eq_2)
  next
    case (10 ps fs i)
    then show ?case
      apply (simp add:nth_list_update, intro impI conjI allI, simp_all)
      by (metis "10"(1) "10"(5) One_nat_def n_not_Suc_n numeral_2_eq_2)+
  qed
qed

lemma inv_implies_DF:"inv_dining ps fs ⟹ TrD N (ps, fs) ≠ {}"
  unfolding inv_dining_def
  apply(simp add:dining_transitions_def phils_transitions_def forks_transitions_def
                 lphil0_transitions_def
             split: if_splits prod.splits)
proof(elim conjE, intro conjI impI, goal_cases)
  case 1
  hence "putsdown 0 (N - Suc 0) ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def)
  then show ?case
    by blast
next
  case 2
  hence "putsdown 0 0 ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def)
  then show ?case
    by (simp add:fork_transitions_def) force
next
  case 3
  hence a:"fs!0 = 0 ⟹ picks 0 0 ∈ (⋃i<N. Trf i (fs ! i))"
     by (auto simp add:fork_transitions_def)
  from 3 have b1:"ps!1 = 2 ⟹ putsdown 1 0 ∈ (⋃x∈{Suc 0..<N}. Trrp x (ps ! x))"
    using N_g1 by (auto simp add:rphil_transitions_def)
  from 3 have b2:"fs!0 = 2 ⟹ putsdown 1 0 ∈ Trf 0 (fs ! 0)"
    using N_g1 by (auto simp add:fork_transitions_def) fastforce
  from 3 have c:"fs!0 ≠ 0 ⟹ ps!1 = 2"
    by (metis N_pos N_pos_simps(3) One_nat_def diff_is_0_eq neq0_conv)
  from 3 have d:"fs!0 ≠ 0 ⟹ fs!0 = 2"
    using N_pos by meson
  then show ?case
    apply(cases "fs!0 = 0")
    using a apply (simp add: fork_transitions_def Un_insert_left)
    using b1[OF c] b2[OF d] N_pos by blast
next
  case 4
  then show ?case
    using 4(5)[rule_format, of 0, OF N_pos] apply(elim disjE)
  proof(goal_cases)
    case 41:1 (* fs!0 = 0 *)
    then show ?case
    using 4(5)[rule_format, of 1, OF N_g1] apply(elim disjE)
    proof(goal_cases)
      case 411:1 (* fs!1 = 0 *)
      from 411 have a0: "ps!1 = 0"
        by (metis N_g1 One_nat_def neq0_conv)
      from 411 have a1: "picks 1 1 ∈ (⋃i<N. Trf i (fs ! i))"
        apply (auto simp add:fork_transitions_def)
        by (metis (mono_tags, lifting) N_g1 Int_Collect One_nat_def lessThan_iff)
      from 411 have a2: "ps!1 = 0 ⟹ picks 1 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
        apply (auto simp add:rphil_transitions_def)
        using N_g1 by linarith
      from 411 show ?case
        using a0 a1 a2 by blast
    next
      case 412:2 (* fs!1 = 1 *)
      hence "ps!1 = 1 ∨ ps!1 = 3"
        by (metis N_g1 One_nat_def less_numeral_extra(3) zero_less_diff)
      with 412 show ?case
      proof(elim disjE, goal_cases)
        case 4121:1 (* ps!1 = 1 *)
        from 4121 have b1: "picks 1 0 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def)
          by (metis (full_types) Int_Collect N_g1 N_pos One_nat_def lessThan_iff mod_less)
        from 4121 have b2: "picks 1 0 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def)
          using N_g1 by linarith
        from 4121 show ?case
          using b1 b2 by blast
      next
        case 4122:2 (* ps!1 = 3 *)
        from 4122 have b3: "putsdown 1 1 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def)
          using N_g1 by linarith
        from 4122 have b4: "putsdown 1 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def)
          using N_g1 by linarith
        then show ?case
          using b3 b4 by blast
      qed
    next
      case 413:3 (* fs!1 = 2 *)
      then show ?case
      proof(cases "N = 2")
        case True
        with 413 show ?thesis by simp
      next
        case False
        from False 413 have c0: "ps!2 = 2"
          by (metis N_g1 Suc_1 Suc_diff_1 nat_neq_iff not_gr0 zero_less_diff)
        from False 413 have c1: "putsdown 2 1 ∈ (⋃i<N. Trf i (fs ! i))"
          apply (auto simp add:fork_transitions_def)
          using N_g1 apply linarith
          using N_g1 by auto
        from False 413 have c2: "ps!2 = 2 ⟹ putsdown 2 1 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
          apply (auto simp add:rphil_transitions_def)
          using N_g1 by linarith
        from 413 False show ?thesis
          using c0 c1 c2 by blast
      qed
    qed
  next
    case 42:2 (* fs!0 = 1 *)
    then show ?case by blast
  next
    case 43:3 (* fs!0 = 2*)
    from 43 have d0: "ps!1 = 2"
      by (metis One_nat_def gr0I)
    from 43 have d1: "putsdown 1 0 ∈ (⋃i<N. Trf i (fs ! i))"
      by (auto simp add:fork_transitions_def)
    from 43 have d2: "ps!1 = 2 ⟹ putsdown 1 0 ∈ (⋃i∈{Suc 0..<N}. Trrp i (ps ! i))"
      apply (auto simp add:rphil_transitions_def)
      using N_g1 by linarith
    from 43 show ?case
      using d0 d1 d2 by blast
  qed
next
  case 5
  then show ?case
    using 5(6)[rule_format, of 0] by simp
qed

corollary DF_DINING: "deadlock_free_v2 DINING"
  unfolding DINING_is_DININGnorm DININGnorm_def
  using inv_DINING inv_implies_DF by (subst deadlock_free_dnorm) auto

end

end

Theory Conclusion

(*<*)
―‹ ******************************************************************** 
 * Project         : CSP-RefTK - A Refinement Toolkit for HOL-CSP
 * Version         : 1.0
 *
 * Author          : Burkhart Wolff, Safouan Taha, Lina Ye.
 *
 * This file       : Conclusion
 *
 * 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‹Conclusion›
(*<*)
theory Conclusion
    imports HOLCF
begin
(*>*)

text‹ We presented a formalisation of the most comprehensive semantic model for CSP, a 'classical' 
language for the specification and analysis of concurrent systems studied in a rich body of 
literature. For this purpose, we ported @{cite "tej.ea:corrected:1997"} to a modern version
of Isabelle, restructured the proofs, and extended the resulting theory of the language 
substantially. The result HOL-CSP 2 has been submitted to the Isabelle AFP @{cite "HOL-CSP-AFP"}, 
thus a fairly sustainable format accessible to other researchers and tools.

We developed a novel set of deadlock - and livelock inference proof principles based on 
classical and denotational characterizations. In particular, we formally investigated the relations
between different refinement notions in the presence of deadlock - and livelock; an area where
traditional CSP literature skates over the nitty-gritty details. Finally, we demonstrated how to
exploit these results for deadlock/livelock analysis of protocols.

We put a large body of abstract CSP laws and induction principles together to form
concrete verification technologies for generalized classical problems, which have been considered
so far from the perspective of data-independence or structural parametricity. The underlying novel
principle of ``trading rich structure against rich state'' allows one to convert processes 
into classical transition systems for which established invariant techniques become applicable.

Future applications of HOL-CSP 2 could comprise a combination with model checkers, where our theory
with its derived rules can be used to certify the output of a model-checker over CSP. In our experience,
labelled transition systems generated by model checkers may be used to steer inductions or to construct
the normalized processes ‹Pnorm⟦τ,υ⟧› automatically, thus combining efficient finite reasoning 
over finite sub-systems with globally infinite systems in a logically safe way. 
›


(*<*)
end
(*>*)