diff --git a/thys/CSP_RefTK/Assertions_ext.thy b/thys/CSP_RefTK/Assertions_ext.thy
deleted file mode 100644
--- a/thys/CSP_RefTK/Assertions_ext.thy
+++ /dev/null
@@ -1,818 +0,0 @@
-(*<*)
-\<comment>\<open> ******************************************************************** 
- * 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.
- ******************************************************************************\<close>
-(*>*)
-
-chapter\<open>Basic CSP\_RefTk-Theories\<close>
-
-theory Assertions_ext
-  imports "HOL-CSP.Assertions"
-begin
-
-section \<open>Preliminaries\<close>
-
-lemma DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold : "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A = ((\<sqinter> z \<in> A \<rightarrow> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) \<sqinter> SKIP)"
-  by(simp add: DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule trans, rule fix_eq, simp)
-
-section \<open>All refinements definitions\<close>
-
-thm failure_divergence_refine_def[simplified le_ref_def] trace_refine_def failure_refine_def
-
-definition divergence_refine :: "'a process \<Rightarrow> 'a process \<Rightarrow> bool" (infix "\<sqsubseteq>\<^sub>D" 60)
-  where "P \<sqsubseteq>\<^sub>D Q \<equiv> D Q \<subseteq> D P"
-
-definition trace_divergence_refine :: "'a process \<Rightarrow> 'a process \<Rightarrow> bool" (infix "\<sqsubseteq>\<^sub>D\<^sub>T" 60)
-  where "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<equiv> P \<sqsubseteq>\<^sub>T Q \<and> P \<sqsubseteq>\<^sub>D Q"
-
-section \<open>Relations between refinements\<close>
-
-lemma le_F_T: "P \<sqsubseteq>\<^sub>F Q \<Longrightarrow> P \<sqsubseteq>\<^sub>T Q"
-  by (simp add: F_subset_imp_T_subset failure_refine_def trace_refine_def) 
-
-lemma FD_F: "P \<sqsubseteq>\<^sub>F\<^sub>D Q \<Longrightarrow> P \<sqsubseteq>\<^sub>F Q"
-  by (simp add: failure_divergence_refine_def failure_refine_def le_ref_def)
-  
-lemma FD_D: "P \<sqsubseteq>\<^sub>F\<^sub>D Q \<Longrightarrow> P \<sqsubseteq>\<^sub>D Q"
-  by (simp add: divergence_refine_def failure_divergence_refine_def le_ref_def)
-
-lemma DT_D: "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> P \<sqsubseteq>\<^sub>D Q"
-  by (simp add: trace_divergence_refine_def)
-
-lemma DT_T: "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> P \<sqsubseteq>\<^sub>T Q"
-  by (simp add: trace_divergence_refine_def)
-
-lemma F_D_FD:"P \<sqsubseteq>\<^sub>F Q \<Longrightarrow> P \<sqsubseteq>\<^sub>D Q \<Longrightarrow> P \<sqsubseteq>\<^sub>F\<^sub>D Q"
-  by (simp add: divergence_refine_def failure_divergence_refine_def failure_refine_def le_ref_def)
-
-lemma D_T_DT:"P \<sqsubseteq>\<^sub>D Q \<Longrightarrow> P \<sqsubseteq>\<^sub>T Q \<Longrightarrow> P \<sqsubseteq>\<^sub>D\<^sub>T Q"
-  by (simp add: trace_divergence_refine_def)
-
-section \<open>Some obvious refinements\<close>
-
-lemma bot_FD[simp]: "\<bottom> \<sqsubseteq>\<^sub>F\<^sub>D Q"
-  by (simp add: failure_divergence_refine_def)
-
-corollary bot_F[simp]: "\<bottom> \<sqsubseteq>\<^sub>F Q"
-      and bot_D[simp]: "\<bottom> \<sqsubseteq>\<^sub>D Q"
-      and bot_T[simp]: "\<bottom> \<sqsubseteq>\<^sub>T Q"
-      and bot_DT[simp]: "\<bottom> \<sqsubseteq>\<^sub>D\<^sub>T Q"
-  by (simp_all add: FD_F FD_D le_F_T D_T_DT)
-
-lemma STOP_leDT[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T STOP"
-  by (simp add: D_STOP D_T_DT Nil_elem_T T_STOP divergence_refine_def trace_refine_def)
-
-\<comment>\<open>For refinement proofs, we need admissibility and monotony starting with idempotency and 
-  transitivity\<close>
-
-section \<open>Idempotency\<close>
-
-lemma idem_F[simp]: "P \<sqsubseteq>\<^sub>F P"
-  by (simp add: failure_refine_def) 
-
-lemma idem_D[simp]: "P \<sqsubseteq>\<^sub>D P"
-  by (simp add: divergence_refine_def)
-
-lemma idem_T[simp]: "P \<sqsubseteq>\<^sub>T P"
-  by (simp add: trace_refine_def)
-
-lemma idem_FD[simp]: "P \<sqsubseteq>\<^sub>F\<^sub>D P"
-  by (simp add: failure_divergence_refine_def)
-
-lemma idem_DT[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T P"
-  by (simp add: trace_divergence_refine_def)
-
-section \<open>Transitivity\<close>
-
-lemma trans_F: "P \<sqsubseteq>\<^sub>F Q \<Longrightarrow> Q \<sqsubseteq>\<^sub>F S \<Longrightarrow> P \<sqsubseteq>\<^sub>F S"
-  by (meson failure_refine_def order_trans)
-
-lemma trans_D: "P \<sqsubseteq>\<^sub>D Q \<Longrightarrow> Q \<sqsubseteq>\<^sub>D S \<Longrightarrow> P \<sqsubseteq>\<^sub>D S"
-  by (meson divergence_refine_def order_trans)
-
-lemma trans_T: "P \<sqsubseteq>\<^sub>T Q \<Longrightarrow> Q \<sqsubseteq>\<^sub>T S \<Longrightarrow> P \<sqsubseteq>\<^sub>T S"
-  by (meson trace_refine_def order_trans)
-
-lemma trans_FD: "P \<sqsubseteq>\<^sub>F\<^sub>D Q \<Longrightarrow> Q \<sqsubseteq>\<^sub>F\<^sub>D S \<Longrightarrow> P \<sqsubseteq>\<^sub>F\<^sub>D S"
-  by (meson failure_divergence_refine_def order_trans)
-
-lemma trans_DT: "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> Q \<sqsubseteq>\<^sub>D\<^sub>T S \<Longrightarrow> P \<sqsubseteq>\<^sub>D\<^sub>T S"
-  by (meson trace_divergence_refine_def order_trans trans_D trans_T)
-
-section \<open>Admissibility\<close>
-
-lemma le_F_adm: "cont (u::('a::cpo) \<Rightarrow> 'b process) \<Longrightarrow> monofun v \<Longrightarrow> adm(\<lambda>x. u x \<sqsubseteq>\<^sub>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:"\<forall>i. F (v (Y i)) \<subseteq> F (u (Y i))" 
-     and 5:" (a, b) \<in> F (v (\<Squnion>x. Y x))"
-  hence "v (Y i)  \<sqsubseteq> v (\<Squnion>i. Y i)" for i by (simp add: is_ub_thelub monofunE)
-  hence "F (v (\<Squnion>i. Y i)) \<subseteq> F (u (Y i))" for i using 4 le_approx_lemma_F by blast   
-  then show "(a, b) \<in> F (\<Squnion>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) \<Rightarrow> 'b process) \<Longrightarrow> monofun v \<Longrightarrow> adm(\<lambda>x. u x \<sqsubseteq>\<^sub>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:"\<forall>i. T (v (Y i)) \<subseteq> T (u (Y i))" 
-     and 5:" x \<in> T (v (\<Squnion>i. Y i))"
-  hence "v (Y i)  \<sqsubseteq> v (\<Squnion>i. Y i)" for i by (simp add: is_ub_thelub monofunE)
-  hence "T (v (\<Squnion>i. Y i)) \<subseteq> T (u (Y i))" for i using 4 le_approx_lemma_T by blast  
-  then show "x \<in> T (\<Squnion>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) \<Rightarrow> 'b process) \<Longrightarrow> monofun v \<Longrightarrow> adm(\<lambda>x. u x \<sqsubseteq>\<^sub>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:"\<forall>i. D (v (Y i)) \<subseteq> D (u (Y i))" 
-     and 5:" x \<in> D (v (\<Squnion>i. Y i))"
-  hence "v (Y i)  \<sqsubseteq> v (\<Squnion>i. Y i)" for i by (simp add: is_ub_thelub monofunE)
-  hence "D (v (\<Squnion>i. Y i)) \<subseteq> D (u (Y i))" for i using 4 le_approx1 by blast  
-  then show "x \<in> D (\<Squnion>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) \<Rightarrow> 'b process) \<Longrightarrow> monofun v \<Longrightarrow> adm(\<lambda>x. u x \<sqsubseteq>\<^sub>D\<^sub>T 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 \<open>Monotonicity\<close>
-
-lemma mono_det_D[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>D P'; S \<sqsubseteq>\<^sub>D S'\<rbrakk> \<Longrightarrow> (P \<box> S) \<sqsubseteq>\<^sub>D (P' \<box> S')"
-  by (metis D_det Un_mono divergence_refine_def)
-
-lemma mono_det_T[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>T P'; S \<sqsubseteq>\<^sub>T S'\<rbrakk> \<Longrightarrow> (P \<box> S) \<sqsubseteq>\<^sub>T (P' \<box> S')"
-  by (metis T_det Un_mono trace_refine_def)
-
-corollary mono_det_DT[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>D\<^sub>T P'; S \<sqsubseteq>\<^sub>D\<^sub>T S'\<rbrakk> \<Longrightarrow> (P \<box> S) \<sqsubseteq>\<^sub>D\<^sub>T (P' \<box> S')"
-  by (simp_all add: trace_divergence_refine_def)
-
-lemmas mono_det_FD[simp]= mono_det_FD[simplified failure_divergence_refine_def[symmetric]]
-
-\<comment>\<open>Deterministic choice monotony doesn't hold for \<open>\<sqsubseteq>\<^sub>F\<close>\<close>
-
-
-lemma mono_ndet_F[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>F P'; S \<sqsubseteq>\<^sub>F S'\<rbrakk> \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>F (P' \<sqinter> S')"
-  by (metis F_ndet Un_mono failure_refine_def) 
-
-lemma mono_ndet_D[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>D P'; S \<sqsubseteq>\<^sub>D S'\<rbrakk> \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>D (P' \<sqinter> S')"
-  by (metis D_ndet Un_mono divergence_refine_def)
-
-lemma mono_ndet_T[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>T P'; S \<sqsubseteq>\<^sub>T S'\<rbrakk> \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>T (P' \<sqinter> S')"
-  by (metis T_ndet Un_mono trace_refine_def) 
-
-corollary mono_ndet_DT[simp]: "\<lbrakk>P \<sqsubseteq>\<^sub>D\<^sub>T P'; S \<sqsubseteq>\<^sub>D\<^sub>T S'\<rbrakk> \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>D\<^sub>T (P' \<sqinter> 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 \<sqsubseteq>\<^sub>F Q \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>F Q"
-  by (simp add: F_ndet failure_refine_def order_trans) 
-
-lemma mono_ndet_D_left[simp]: "P \<sqsubseteq>\<^sub>D Q \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>D Q"
-  by (simp add: D_ndet divergence_refine_def order_trans) 
-
-lemma mono_ndet_T_left[simp]: "P \<sqsubseteq>\<^sub>T Q \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>T Q"
-  by (simp add: T_ndet trace_refine_def order_trans) 
-
-corollary mono_ndet_DT_left[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> (P \<sqinter> S) \<sqsubseteq>\<^sub>D\<^sub>T Q"
-     and mono_ndet_F_right[simp]: "P \<sqsubseteq>\<^sub>F Q \<Longrightarrow> (S \<sqinter> P) \<sqsubseteq>\<^sub>F Q"
-     and mono_ndet_D_right[simp]: "P \<sqsubseteq>\<^sub>D Q \<Longrightarrow> (S \<sqinter> P) \<sqsubseteq>\<^sub>D Q"
-     and mono_ndet_T_right[simp]: "P \<sqsubseteq>\<^sub>T Q \<Longrightarrow> (S \<sqinter> P) \<sqsubseteq>\<^sub>T Q"
-     and mono_ndet_DT_right[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> (S \<sqinter> P) \<sqsubseteq>\<^sub>D\<^sub>T 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 \<sqinter> S) \<sqsubseteq>\<^sub>F\<^sub>D (P \<box> 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 \<sqinter> S) \<sqsubseteq>\<^sub>F (P \<box> S)"
-      and mono_ndet_det_D[simp]: "(P \<sqinter> S) \<sqsubseteq>\<^sub>D (P \<box> S)"
-      and mono_ndet_det_T[simp]: "(P \<sqinter> S) \<sqsubseteq>\<^sub>T (P \<box> S)"
-      and mono_ndet_det_DT[simp]: "(P \<sqinter> S) \<sqsubseteq>\<^sub>D\<^sub>T (P \<box> S)" 
-  by (simp_all add: FD_F FD_D le_F_T D_T_DT) 
-
-
-lemma mono_seq_F_right[simp]: "S \<sqsubseteq>\<^sub>F S' \<Longrightarrow> (P `;` S) \<sqsubseteq>\<^sub>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 \<sqsubseteq>\<^sub>D S' \<Longrightarrow> (P `;` S) \<sqsubseteq>\<^sub>D (P `;` S')"
-  by (auto simp: divergence_refine_def D_seq)
-
-lemma  mono_seq_T_right[simp]: "S \<sqsubseteq>\<^sub>T S' \<Longrightarrow> (P `;` S)  \<sqsubseteq>\<^sub>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 \<sqsubseteq>\<^sub>D\<^sub>T S' \<Longrightarrow> (P `;` S)  \<sqsubseteq>\<^sub>D\<^sub>T (P `;` S')"
-  by (simp add: trace_divergence_refine_def)
-
-lemma mono_seq_DT_left[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T P' \<Longrightarrow> (P `;` S)  \<sqsubseteq>\<^sub>D\<^sub>T (P' `;` S)"
-  apply (auto simp: trace_divergence_refine_def divergence_refine_def trace_refine_def D_seq T_seq)
-  by (metis (no_types, lifting) Nil_elem_T Process.F_T T_F append.right_neutral 
-            is_processT5_S3 subset_eq) 
-
-\<comment>\<open>left sequence monotony doesn't hold for \<open>\<sqsubseteq>\<^sub>F\<close>, \<open>\<sqsubseteq>\<^sub>D\<close> and \<open>\<sqsubseteq>\<^sub>T\<close>\<close>
-
-corollary mono_seq_DT[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T P' \<Longrightarrow> S \<sqsubseteq>\<^sub>D\<^sub>T S' \<Longrightarrow> (P `;` S)  \<sqsubseteq>\<^sub>D\<^sub>T (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]: "\<forall>x. P x \<sqsubseteq>\<^sub>F Q x \<Longrightarrow> Mprefix A P \<sqsubseteq>\<^sub>F Mprefix A Q"
-  by (auto simp: failure_refine_def F_Mprefix)
-
-lemma mono_mprefix_D_process[simp]: "\<forall>x. P x \<sqsubseteq>\<^sub>D Q x \<Longrightarrow> Mprefix A P \<sqsubseteq>\<^sub>D Mprefix A Q"
-  by (auto simp: divergence_refine_def D_Mprefix)
-
-lemma mono_mprefix_T_process[simp]: "\<forall>x. P x \<sqsubseteq>\<^sub>T Q x \<Longrightarrow> Mprefix A P \<sqsubseteq>\<^sub>T Mprefix A Q"
-  by (auto simp: trace_refine_def T_Mprefix)
-
-corollary mono_mprefix_DT_process[simp]: "\<forall>x. P x \<sqsubseteq>\<^sub>D\<^sub>T Q x \<Longrightarrow> Mprefix A P \<sqsubseteq>\<^sub>D\<^sub>T 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 \<subseteq> B \<Longrightarrow> Mprefix B P \<sqsubseteq>\<^sub>D\<^sub>T 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 \<subseteq> B \<Longrightarrow> Mprefix B P \<sqsubseteq>\<^sub>D Mprefix A P"
-      and mono_mprefix_T_set[simp]: "A \<subseteq> B \<Longrightarrow> Mprefix B P \<sqsubseteq>\<^sub>T Mprefix A P"
-  by (simp_all add: DT_D DT_T)
-
-\<comment>\<open>Mprefix set monotony doesn't hold for \<open>\<sqsubseteq>\<^sub>F\<close> and \<open>\<sqsubseteq>\<^sub>F\<^sub>D\<close> where it holds for deterministic choice\<close>
-
-
-lemma mono_hide_F[simp]: "P \<sqsubseteq>\<^sub>F Q \<Longrightarrow> P \\ A \<sqsubseteq>\<^sub>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 \<in> A" by blast
-  define f where A:"f = rec_nat t (\<lambda>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 \<in> range f" by (metis (mono_tags, lifting) old.nat.simps(6) range_eqI)
-  { fix i
-    have "f i \<in> D Q \<and> tickFree (f i) \<and> 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 \<and> t \<in> 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 \<sqsubseteq>\<^sub>T Q \<Longrightarrow> P \\ A \<sqsubseteq>\<^sub>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 \<in> 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 \<and> t \<in> 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 (\<lambda>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 \<in> range f" 
-      by (metis (mono_tags, lifting) old.nat.simps(6) range_eqI)
-    { fix i
-      have "f i \<in> D Q \<and> tickFree (f i) \<and> 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 \<and> t \<in> 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 \<sqsubseteq>\<^sub>D\<^sub>T Q \<Longrightarrow> P \\ A \<sqsubseteq>\<^sub>D\<^sub>T Q \\ A"
-proof -
-  assume as:"P \<sqsubseteq>\<^sub>D\<^sub>T Q"
-  then have "P \\ A \<sqsubseteq>\<^sub>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]]
-
-\<comment>\<open>Obviously, Hide monotony doesn't hold for \<open>\<sqsubseteq>\<^sub>D\<close>\<close>
-
-
-lemma mono_sync_DT[simp]: "P \<sqsubseteq>\<^sub>D\<^sub>T P' \<Longrightarrow> Q \<sqsubseteq>\<^sub>D\<^sub>T Q' \<Longrightarrow> (P \<lbrakk> A \<rbrakk> Q) \<sqsubseteq>\<^sub>D\<^sub>T (P' \<lbrakk> A \<rbrakk> 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]]
-
-\<comment>\<open>synchronization monotony doesn't hold for \<open>\<sqsubseteq>\<^sub>F\<close>, \<open>\<sqsubseteq>\<^sub>D\<close> and \<open>\<sqsubseteq>\<^sub>T\<close>\<close>
-
-
-lemma mono_mndet_F_process[simp]: "\<forall>x\<in>A. P x \<sqsubseteq>\<^sub>F Q x \<Longrightarrow> mndet A P \<sqsubseteq>\<^sub>F mndet A Q"
-  by (cases "A = {}", auto simp: failure_refine_def F_mndet write0_def F_Mprefix) 
-
-lemma mono_mndet_D_process[simp]: "\<forall>x\<in>A. P x \<sqsubseteq>\<^sub>D Q x \<Longrightarrow> mndet A P \<sqsubseteq>\<^sub>D mndet A Q"
-  by (cases "A = {}", auto simp: divergence_refine_def D_mndet write0_def D_Mprefix)
-
-lemma mono_mndet_T_process[simp]: "\<forall>x\<in>A. P x \<sqsubseteq>\<^sub>T Q x \<Longrightarrow> mndet A P \<sqsubseteq>\<^sub>T mndet A Q"
-  by (cases "A = {}", auto simp: trace_refine_def T_mndet write0_def T_Mprefix)
-
-corollary mono_mndet_DT_process[simp]: "\<forall>x\<in>A. P x \<sqsubseteq>\<^sub>D\<^sub>T Q x \<Longrightarrow> mndet A P \<sqsubseteq>\<^sub>D\<^sub>T 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 \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> mndet B P \<sqsubseteq>\<^sub>F mndet A P"
-      and mono_mndet_D_set[simp]: "A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> mndet B P \<sqsubseteq>\<^sub>D mndet A P"
-      and mono_mndet_T_set[simp]: "A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> mndet B P \<sqsubseteq>\<^sub>T mndet A P"
-      and mono_mndet_DT_set[simp]: "A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> mndet B P \<sqsubseteq>\<^sub>D\<^sub>T 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 \<sqsubseteq>\<^sub>F Mprefix A P"
-      and Mprefix_refines_Mndet_D[simp]: "mndet A P \<sqsubseteq>\<^sub>D Mprefix A P"
-      and Mprefix_refines_Mndet_T[simp]: "mndet A P \<sqsubseteq>\<^sub>T Mprefix A P"
-      and Mprefix_refines_Mndet_DT[simp]: "mndet A P \<sqsubseteq>\<^sub>D\<^sub>T Mprefix A P"
-  by (simp_all add: FD_F FD_D le_F_T D_T_DT) 
-
-
-section \<open>Reference processes and their unfolding rules\<close>
-
-thm DF_def DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def RUN_def CHAOS_def
-
-definition CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P :: "'a set \<Rightarrow> 'a process" 
-  where   "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))"
-
-
-thm DF_unfold DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold
-
-lemma RUN_unfold : "RUN A = (\<box> z \<in> A \<rightarrow> RUN A)"
-  by(simp add: RUN_def, rule trans, rule fix_eq, simp)
-
-lemma CHAOS_unfold : "CHAOS A = (STOP \<sqinter> (\<box> z \<in> A \<rightarrow> CHAOS A))"
-  by(simp add: CHAOS_def, rule trans, rule fix_eq, simp)
-                                              
-lemma CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A)"
-  unfolding CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def using fix_eq[of "\<Lambda> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))"] by simp
-
-section \<open>Process events and reference processes events\<close>
-
-definition events_of where "events_of P \<equiv> (\<Union>t\<in>T P. {a. ev a \<in> set t})"
-
-lemma events_DF: "events_of (DF A) = A"
-proof(auto simp add:events_of_def)
-  fix x t
-  show "t \<in> T (DF A) \<Longrightarrow> ev x \<in> set t \<Longrightarrow> x \<in> A"
-  proof(induct t)
-    case Nil
-    then show ?case by simp
-  next
-    case (Cons a t)
-    from Cons(2) have "a # t \<in> T (\<sqinter>z\<in>A \<rightarrow>  DF A)" using DF_unfold by metis
-    then obtain aa where "a = ev aa \<and> aa \<in> A \<and> t \<in> 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 \<in> A \<Longrightarrow> \<exists>xa\<in>T (DF A). ev x \<in> 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_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P: "events_of (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = A"
-proof(auto simp add:events_of_def)
-  fix x t
-  show "t \<in> T (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) \<Longrightarrow> ev x \<in> set t \<Longrightarrow> x \<in> A"
-  proof(induct t)
-    case Nil
-    then show ?case by simp
-  next
-    case (Cons a t)
-    from Cons(2) have "a # t \<in> T ((\<sqinter>z\<in>A \<rightarrow>  DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) \<sqinter> SKIP)" using DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold by metis
-    with Cons obtain aa where "a = ev aa \<and> aa \<in> A \<and> t \<in> T (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P 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 \<in> A \<Longrightarrow> \<exists>xa\<in>T (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A). ev x \<in> set xa"
-    apply(subst DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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 \<in> T (RUN A) \<Longrightarrow> ev x \<in> set t \<Longrightarrow> x \<in> A"
-  proof(induct t)
-    case Nil
-    then show ?case by simp
-  next
-    case (Cons a t)
-    from Cons(2) have "a # t \<in> T (\<box>z\<in>A \<rightarrow>  RUN A)" using RUN_unfold by metis
-    then obtain aa where "a = ev aa \<and> aa \<in> A \<and> t \<in> T (RUN A)" by (auto simp add:T_Mprefix)
-    with Cons show ?case by auto
-  qed
-next
-  fix x
-  show "x \<in> A \<Longrightarrow> \<exists>xa\<in>T (RUN A). ev x \<in> 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 \<in> T (CHAOS A) \<Longrightarrow> ev x \<in> set t \<Longrightarrow> x \<in> A"
-  proof(induct t)
-    case Nil
-    then show ?case by simp
-  next
-    case (Cons a t)
-    from Cons(2) have "a # t \<in> T (STOP \<sqinter> (\<box> z \<in> A \<rightarrow> CHAOS A))" using CHAOS_unfold by metis
-    then obtain aa where "a = ev aa \<and> aa \<in> A \<and> t \<in> 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 \<in> A \<Longrightarrow> \<exists>xa\<in>T (CHAOS A). ev x \<in> 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_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P: "events_of (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = A"
-proof(auto simp add:events_of_def)
-  fix x t
-  show "t \<in> T (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) \<Longrightarrow> ev x \<in> set t \<Longrightarrow> x \<in> A"
-  proof(induct t)
-    case Nil
-    then show ?case by simp
-  next
-    case (Cons a t)
-    from Cons(2) have "a # t \<in> T (SKIP \<sqinter> STOP \<sqinter> (\<box> z \<in> A \<rightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A))" 
-      using CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold by metis
-    with Cons obtain aa where "a = ev aa \<and> aa \<in> A \<and> t \<in> T (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P 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 \<in> A \<Longrightarrow> \<exists>xa\<in>T (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A). ev x \<in> set xa"
-    apply(subst CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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) \<noteq> {} \<Longrightarrow>  events_of (P) = UNIV"
-proof(auto simp add:events_of_def)
-  fix x xa
-  assume 1: "x \<in> D P"
-  show "\<exists>x\<in>T P. ev xa \<in> set x"
-  proof(cases "tickFree x")
-    case True  
-    hence "x@[ev xa] \<in> 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] \<in> 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 DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_subset_FD: "A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P B \<sqsubseteq>\<^sub>F\<^sub>D DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-  apply(subst DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule fix_ind, rule le_FD_adm, simp_all add:monofunI, subst DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold)
-  by (rule mono_ndet_FD, simp_all) (meson mono_mndet_FD_process mono_mndet_FD_set trans_FD) 
-
-lemma RUN_subset_DT: "A \<subseteq> B \<Longrightarrow> RUN B \<sqsubseteq>\<^sub>D\<^sub>T 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 \<subseteq> B \<Longrightarrow> CHAOS B \<sqsubseteq>\<^sub>F\<^sub>D 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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_subset_FD: "A \<subseteq> B \<Longrightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P B \<sqsubseteq>\<^sub>F\<^sub>D CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-  apply(subst CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule fix_ind, rule le_FD_adm) 
-     apply(simp_all add:monofunI, subst CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold)
-  by (auto simp add: failure_divergence_refine_def le_ref_def 
-                     D_Mprefix D_ndet F_STOP F_Mprefix F_ndet)
-
-section \<open>Relations between refinements on reference processes\<close>
-
-lemma CHAOS_has_all_tickFree_failures: 
-      "tickFree a \<Longrightarrow> {x. ev x \<in> set a} \<subseteq> A \<Longrightarrow> (a,b) \<in> 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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures: 
-  assumes as:"(events_of P) \<subseteq> A" 
-  shows "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>F P"
-proof -
-  have "front_tickFree a \<Longrightarrow> set a \<subseteq> (\<Union>t\<in>T P. set t) \<Longrightarrow> (a,b) \<in> F (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A)" for a b
-  proof(induct a)
-    case Nil
-    then show ?case 
-      by (subst CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures_ev: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P (events_of P) \<sqsubseteq>\<^sub>F P" 
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures_Un: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>F P"
-  by (simp_all add: CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures)
-
-
-lemma DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF_refine_F: "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F DF A"
-  by (simp add:DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule fix_ind, simp_all add:le_F_adm monofunI, subst DF_unfold, simp) 
-
-lemma DF_RUN_refine_F: "DF A  \<sqsubseteq>\<^sub>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  \<sqsubseteq>\<^sub>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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_CHAOS_refine_F: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F CHAOS A"
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_refine_F: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-  by (simp_all add: CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures events_CHAOS events_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P 
-                    trans_F[OF CHAOS_DF_refine_F DF_RUN_refine_F])
-
-
-lemma div_free_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P: "D(DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = {}"
-proof(simp add:DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def fix_def) 
-  define Y where "Y \<equiv> \<lambda>i. iterate i\<cdot>(\<Lambda> x. (\<sqinter>xa\<in>A \<rightarrow>  x) \<sqinter> SKIP)\<cdot>\<bottom>"
-  hence a:"chain Y" by simp
-  have "D (Y (Suc i)) = {d. d \<noteq> [] \<and> hd d  \<in> (ev ` A) \<and> tl d \<in> 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 \<in> D(Y i) \<Longrightarrow> length d \<ge> i" for d i
-    by (induct i arbitrary:d, simp_all add: Nitpick.size_list_simp(2))
-  { fix x
-    assume c:"\<forall> i. x \<in> D (Y i)"
-    from b have "x \<notin> D (Y (Suc (length x)))" using Suc_n_not_le_n by blast
-    with c have False by simp
-  }
-  with a show "D (\<Squnion>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 "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>D DF A"
-    by (simp add:DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule fix_ind, simp_all add:le_D_adm monofunI, subst DF_unfold, simp) 
-  then show ?thesis using divergence_refine_def div_free_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P by blast 
-qed
-
-lemma div_free_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P: "D (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = {}"
-proof -
-  have "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>D CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-  proof (simp add:DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, rule fix_ind, simp_all add:le_D_adm monofunI, subst CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold)
-    fix x
-    assume 1:"x \<sqsubseteq>\<^sub>D CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-    have a:"((\<sqinter>xa\<in>A \<rightarrow>  x) \<sqinter> SKIP) = (SKIP \<sqinter> SKIP \<sqinter> (\<sqinter>xa\<in>A \<rightarrow>  x))" 
-      by (simp add: Ndet_commute ndet_id)
-    from 1 have b:"(SKIP \<sqinter> SKIP \<sqinter> (\<sqinter>xa\<in>A \<rightarrow>  x)) \<sqsubseteq>\<^sub>D (SKIP \<sqinter> STOP \<sqinter> (\<box>xa\<in>A \<rightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P 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 "((\<sqinter>xa\<in>A \<rightarrow>  x) |-| SKIP) \<sqsubseteq>\<^sub>D (SKIP |-| STOP |-| Mprefix A (\<lambda>x. CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A))" 
-      by simp
-  qed
-  then show ?thesis using divergence_refine_def div_free_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P by blast 
-qed
-
-lemma div_free_CHAOS: "D(CHAOS A) = {}"
-proof - 
-  have "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>D CHAOS A"
-    apply (simp add:CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P by blast 
-qed
-
-lemma div_free_RUN: "D(RUN A) = {}"
-proof - 
-  have "CHAOS A  \<sqsubseteq>\<^sub>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 DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF_refine_FD: "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F\<^sub>D DF A"
-      and DF_RUN_refine_FD: "DF A  \<sqsubseteq>\<^sub>F\<^sub>D RUN A"
-      and CHAOS_DF_refine_FD: "CHAOS A  \<sqsubseteq>\<^sub>F\<^sub>D DF A"
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_CHAOS_refine_FD: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F\<^sub>D CHAOS A"
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_refine_FD: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A  \<sqsubseteq>\<^sub>F\<^sub>D DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A"
-  using div_free_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P[of A] div_free_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P[of A] div_free_DF[of A] div_free_RUN[of A] 
-        div_free_CHAOS[of A] 
-        F_D_FD[OF DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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 CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_CHAOS_refine_F, of A] 
-        F_D_FD[OF CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_refine_F, of A]
-  by (auto simp add:divergence_refine_def) 
-
-
-lemma traces_CHAOS_sub: "T(CHAOS A) \<subseteq> {s. set s \<subseteq> ev ` A}"
-proof(auto)
-  fix s sa
-  assume "s \<in> T (CHAOS A)" and "sa \<in> set s"
-  then show "sa \<in> 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 \<subseteq> ev ` A} \<subseteq> T(RUN A)"
-proof(auto)
-  fix s
-  assume "set s \<subseteq> ev ` A"
-  then show "s \<in> 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 \<subseteq> ev ` A}" 
-      and DF_all_tickfree_traces1: "T(DF A) = {s. set s \<subseteq> ev ` A}" 
-      and CHAOS_all_tickfree_traces1: "T(CHAOS A) = {s. set s \<subseteq> 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 \<Longrightarrow> s \<in> T(RUN UNIV)" 
-      and DF_all_tickfree_traces2: "tickFree s \<Longrightarrow> s \<in> T(DF UNIV)" 
-      and CHAOS_all_tickfree_trace2: "tickFree s \<Longrightarrow> s \<in> 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_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_sub: "T(CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) \<subseteq> {s. front_tickFree s \<and> set s \<subseteq> (ev ` A \<union> {tick})}"
-proof(auto simp add:is_processT2_TR)
-  fix s sa
-  assume "s \<in> T (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A)" and "sa \<in> set s" and "sa \<notin> ev ` A"
-  then show "sa = tick"
-    apply (induct s, simp) 
-    by (subst (asm) (2) CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold, cases "A={}", auto simp add:T_ndet T_STOP T_SKIP T_Mprefix)  
-qed
-
-lemma traces_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_sub: 
-                      "{s. front_tickFree s \<and> set s \<subseteq> (ev ` A \<union> {tick})} \<subseteq> T(DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A::'a process)"
-proof(auto)
-  fix s
-  assume a:"front_tickFree s" and b:"set s \<subseteq> insert tick (ev ` A)"
-  have c:"front_tickFree ((tick::'a event) # s) \<Longrightarrow> s = []" for s
-    by (metis butlast.simps(2) butlast_snoc front_tickFree_charn list.distinct(1) tickFree_Cons) 
-  with a b show "s \<in> T (DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A)"
-    apply (induct s, simp add: Nil_elem_T, subst DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_unfold, cases "A={}") 
-     apply (subst DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_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 DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces1: 
-                              "T(DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = {s. front_tickFree s \<and> set s \<subseteq> (ev ` A \<union> {tick})}" 
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces1: 
-                              "T(CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A) = {s. front_tickFree s \<and> set s \<subseteq> (ev ` A \<union> {tick})}"
-  using CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_refine_F[THEN le_F_T, simplified trace_refine_def]
-        traces_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_sub traces_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_sub by blast+
-
-corollary DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces2: "front_tickFree s \<Longrightarrow> s \<in> T(DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)" 
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces2: "front_tickFree s \<Longrightarrow> s \<in> T(CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)"
-   apply(simp_all add:tickFree_def DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces1 
-                      CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces1)
-  by (metis event_set subsetI)+
-
-corollary DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_traces: "DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>T P"
-      and CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_traces: "CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>T P"
-  apply (simp add:trace_refine_def DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces2 is_processT2_TR subsetI) 
-  by (simp add:trace_refine_def CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_all_front_tickfree_traces2 is_processT2_TR subsetI) 
-
-end
diff --git a/thys/CSP_RefTK/CopyBuffer_props.thy b/thys/CSP_RefTK/CopyBuffer_props.thy
--- a/thys/CSP_RefTK/CopyBuffer_props.thy
+++ b/thys/CSP_RefTK/CopyBuffer_props.thy
@@ -1,120 +1,89 @@
 (*<*)
 \<comment>\<open> ********************************************************************
  * 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.
  ******************************************************************************\<close>
 (*>*)
 
 chapter\<open>Examples\<close>
 
 section\<open>CopyBuffer Refinement over an infinite alphabet\<close>
 
 theory     CopyBuffer_props
- imports   "HOL-CSP.CopyBuffer" "Properties"
+ imports   "HOL-CSP.CopyBuffer" "HOL-CSP.Assertions"
 begin 
 
 subsection\<open> The Copy-Buffer vs. reference processes \<close>
 
 lemma DF_COPY: "(DF (range left \<union> range right)) \<sqsubseteq>\<^sub>F\<^sub>D COPY"
-    apply(simp add: DF_def,rule fix_ind2, simp_all)
-proof -
-  show "adm (\<lambda>a. a \<sqsubseteq>\<^sub>F\<^sub>D COPY)" by (rule le_FD_adm, simp_all add: monofunI)
-next
-  have 1: "(\<sqinter>xa\<in> range left \<union> range right \<rightarrow> \<bottom>) \<sqsubseteq>\<^sub>F\<^sub>D (\<sqinter>xa\<in> range left \<rightarrow>  \<bottom>)" by simp
-  have 2: "(\<sqinter>xa\<in> range left \<rightarrow>  \<bottom>) \<sqsubseteq>\<^sub>F\<^sub>D (left\<^bold>?x \<rightarrow>  \<bottom>)" 
-    unfolding read_def
-    by (meson BOT_leFD mono_Mndetprefix_FD Mprefix_refines_Mndetprefix_FD trans_FD)
-  show "(\<sqinter>x\<in>range left \<union> range right \<rightarrow>  \<bottom>) \<sqsubseteq>\<^sub>F\<^sub>D COPY"
-    by (metis (mono_tags, lifting) "1" "2" BOT_leFD COPY_rec mono_read_FD trans_FD)
-next
-  fix P::"'a channel process"
-  assume  *: "P \<sqsubseteq>\<^sub>F\<^sub>D COPY" and ** : "(\<sqinter>x\<in>range left \<union> range right \<rightarrow>  P) \<sqsubseteq>\<^sub>F\<^sub>D COPY"
-  have 1: "(\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P) \<sqsubseteq>\<^sub>F\<^sub>D (\<sqinter>xa\<in> range right \<rightarrow>  P)" by force
-  have 2: "(\<sqinter>xa\<in> range right \<rightarrow>  P) \<sqsubseteq>\<^sub>F\<^sub>D (right\<^bold>!x \<rightarrow>  P)" for x
-    by (metis mono_Mndetprefix_FD_set[of "{right x}" "range right"] Mprefix_refines_Mndetprefix_FD 
-              empty_not_insert insert_subset rangeI sup_bot_left sup_ge1 trans_FD write_def)
+  by (simp add: DF_COPY)
 
- 
-  from 1 2 have ab: "(\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P) \<sqsubseteq>\<^sub>F\<^sub>D (right\<^bold>!x \<rightarrow>  P)" for x
-    using trans_FD by blast
-  hence 3: "(left\<^bold>?x \<rightarrow> (\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P)) \<sqsubseteq>\<^sub>F\<^sub>D (left\<^bold>?x \<rightarrow>(right\<^bold>!x \<rightarrow>  P))" by simp
-  have 4: "\<And>X. (\<sqinter>xa\<in> range left \<union> range right \<rightarrow> X) \<sqsubseteq>\<^sub>F\<^sub>D (\<sqinter>xa\<in> range left \<rightarrow> X)" by simp
-  have 5: "\<And>X. (\<sqinter>xa\<in> range left \<rightarrow> X) \<sqsubseteq>\<^sub>F\<^sub>D (left\<^bold>?x \<rightarrow> X)" by (simp add: read_def K_record_comp)
-  from 3 4[of "(\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P)"] 
-       5  [of "(\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P)"] 
-  have 6:"(\<sqinter>xa\<in> range left \<union> range right \<rightarrow> 
-                  (\<sqinter>xa\<in> range left \<union> range right \<rightarrow>  P)) \<sqsubseteq>\<^sub>F\<^sub>D (left\<^bold>?x \<rightarrow> (right\<^bold>!x \<rightarrow>  P))"
-    using trans_FD by blast
-  from * ** have 7: "(left\<^bold>?x \<rightarrow> (right\<^bold>!x \<rightarrow>  P)) \<sqsubseteq>\<^sub>F\<^sub>D (left\<^bold>?x \<rightarrow> (right\<^bold>!x \<rightarrow>  COPY))" by fastforce
-  show "(\<sqinter>x\<in>range left \<union> range right \<rightarrow>  \<sqinter>x\<in>range left \<union> range right \<rightarrow>  P) \<sqsubseteq>\<^sub>F\<^sub>D COPY"
-    by (metis (mono_tags, lifting) "6" "7" COPY_rec trans_FD)
-qed
 
 subsection\<open> ... and abstract consequences \<close>
 
 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 \<sqsubseteq>\<^sub>F\<^sub>D SYSTEM"
   using DF_subset[of "(range left \<union> range right)" UNIV, simplified]
         DF_COPY impl_refines_spec 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
diff --git a/thys/CSP_RefTK/Fix_ind_ext.thy b/thys/CSP_RefTK/Fix_ind_ext.thy
deleted file mode 100644
--- a/thys/CSP_RefTK/Fix_ind_ext.thy
+++ /dev/null
@@ -1,142 +0,0 @@
-(*<*)
-\<comment>\<open> ********************************************************************
- * 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.
- ******************************************************************************\<close>
-(*>*)
-
-chapter \<open> Advanced Induction Schemata \<close>
-
-theory Fix_ind_ext
-
-imports HOLCF
-
-begin
-
-section\<open>k-fixpoint-induction\<close>
-
-lemma nat_k_induct: 
-  fixes k::nat
-  assumes "\<forall>i<k. P i" and "\<forall>n\<^sub>0. (\<forall>i<k. P (n\<^sub>0+i)) \<longrightarrow> P (n\<^sub>0+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: "\<forall>i<k. P (iterate i\<cdot>f\<cdot>\<bottom>)"
-  assumes step: "\<And>x. (\<forall>i<k.  P (iterate i\<cdot>f\<cdot>x)) \<Longrightarrow> P (iterate k\<cdot>f\<cdot>x)"
-  shows "P (fix\<cdot>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 \<ge> 1" and "\<forall>i<k. P i" and "\<forall>n\<^sub>0. P (n\<^sub>0) \<longrightarrow> P (n\<^sub>0+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 \<ge> 1"
-  assumes adm: "adm P"
-  assumes base_k_steps: "\<forall>i<k. P (iterate i\<cdot>f\<cdot>\<bottom>)"
-  assumes step: "\<And>x. P x \<Longrightarrow> P (iterate k\<cdot>f\<cdot>x)"
-  shows "P (fix\<cdot>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\<open>Parallel fixpoint-induction\<close>
-
-lemma parallel_fix_ind_inc:
-  assumes adm: "adm (\<lambda>x. P (fst x) (snd x))"
-  assumes base_fst: "\<And>y. P \<bottom> y" and base_snd: "\<And>x. P x \<bottom>"
-  assumes step: "\<And>x y. P x y \<Longrightarrow> P (G\<cdot>x) y \<Longrightarrow> P x (H\<cdot>y) \<Longrightarrow> P (G\<cdot>x) (H\<cdot>y)"
-  shows "P (fix\<cdot>G) (fix\<cdot>H)"
-proof -
-  from adm have adm': "adm (case_prod P)"
-    unfolding split_def .
-  have "P (iterate i\<cdot>G\<cdot>\<bottom>) (iterate j\<cdot>H\<cdot>\<bottom>)" 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'\<cdot>G\<cdot>\<bottom>) (iterate j'\<cdot>H\<cdot>\<bottom>)" 
-       and "P (iterate i'\<cdot>G\<cdot>\<bottom>) (iterate j\<cdot>H\<cdot>\<bottom>)" 
-       and "P (iterate i\<cdot>G\<cdot>\<bottom>) (iterate j'\<cdot>H\<cdot>\<bottom>)"
-        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 "\<And>i. case_prod P (iterate i\<cdot>G\<cdot>\<bottom>, iterate i\<cdot>H\<cdot>\<bottom>)"
-    by simp
-  then have "case_prod P (\<Squnion>i. (iterate i\<cdot>G\<cdot>\<bottom>, iterate i\<cdot>H\<cdot>\<bottom>))"
-    by - (rule admD [OF adm'], simp, assumption)
-  then have "P (\<Squnion>i. iterate i\<cdot>G\<cdot>\<bottom>) (\<Squnion>i. iterate i\<cdot>H\<cdot>\<bottom>)"
-    by (simp add: lub_Pair)  
-  then show "P (fix\<cdot>G) (fix\<cdot>H)"
-    by (simp add: fix_def2)
-qed
-
-end
\ No newline at end of file
diff --git a/thys/CSP_RefTK/Introduction.thy b/thys/CSP_RefTK/Introduction.thy
--- a/thys/CSP_RefTK/Introduction.thy
+++ b/thys/CSP_RefTK/Introduction.thy
@@ -1,123 +1,124 @@
 (*<*)
 \<comment>\<open> ********************************************************************
  * 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.
  ******************************************************************************\<close>
 (*>*)
 
 chapter\<open>Context\<close>
 (*<*)
 theory Introduction
     imports HOLCF
 begin
 (*>*)
 
 section\<open>Introduction\<close>
 
 text\<open>
 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 \<^emph>\<open>process algebras\<close>. 
 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 \<^emph>\<open>process refinement orderings\<close>,
 most notably \<open>_\<sqsubseteq>\<^sub>F\<^sub>D_\<close> and \<open>_\<sqsubseteq>_\<close>. The latter turns the denotational domain of CSP into a Scott cpo 
 @{cite "scott:cpo:1972"}, which yields semantics for the fixed point operator \<open>\<mu>x. f(x)\<close> provided 
 that \<open>f\<close> is continuous with respect to \<open>_\<sqsubseteq>_\<close>. 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 \<open>A\<close>.
 
 We are interested in verification techniques for arbitrary event sets \<open>A\<close> 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 
 \<^url>\<open>https://gitlri.lri.fr/burkhart.wolff/hol-csp2.0\<close>. 
 
 The present AFP Module is an add-on on this work and develops some support for 
-\<^enum> advanced induction schemes (mutual fixed-point Induction, K-induction),
-\<^enum> bridge-Lemmas between the classical refinement relations in the FD-semantics,
-  which allow for reduced refinement proof complexity in certain cases, and
+\<^enum> example of induction schemes (mutual fixed-point Induction, K-induction),
 \<^enum> a theory of explicit state normalisation which allows for proofs over certain
   communicating networks of arbitrary size.
 
 \newpage
 \<close>
 
-
+(* \<^enum> bridge-Lemmas between the classical refinement relations in the FD-semantics,
+  which allow for reduced refinement proof complexity in certain cases, and *)
 
 section\<open>The Global Architecture of CSP\_RefTk\<close>
 text\<open>
 \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}
 \<close>
 
 text\<open>The global architecture of CSP\_RefTk is shown in \autoref{fig:fig1}.
 The entire package resides on: 
 \<^enum> \<^session>\<open>HOL-Eisbach\<close> from the Isabelle/HOL distribution,
 \<^enum> \<^session>\<open>HOLCF\<close> from the Isabelle/HOL distribution, and
 \<^enum> \<^session>\<open>HOL-CSP\<close> 2.0 from the Isabelle Archive of Formal Proofs.
+\<close>
 
+(* 
 \<^noindent> The theories \<^verbatim>\<open>Assertion_ext\<close> and \<^verbatim>\<open>Fixind_ext\<close> are extensions of the 
-corresponding theories in \<^session>\<open>HOL-CSP\<close>.\<close>
+corresponding theories in \<^session>\<open>HOL-CSP\<close>. *)
 
 
 (*<*)
 end
 (*>*)
diff --git a/thys/CSP_RefTK/Process_norm.thy b/thys/CSP_RefTK/Process_norm.thy
--- a/thys/CSP_RefTK/Process_norm.thy
+++ b/thys/CSP_RefTK/Process_norm.thy
@@ -1,246 +1,246 @@
 (*<*)
 \<comment>\<open> ********************************************************************
  * 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.
  ******************************************************************************\<close>
 (*>*)
 
 chapter\<open> Normalisation of Deterministic CSP Processes \<close>
 
 theory Process_norm
 
-imports "Properties" "HOL-CSP.Induction_ext"
+imports "HOL-CSP.Assertions" "HOL-CSP.CSP_Induct"
 
 begin
 
 section\<open>Deterministic normal-forms with explicit state\<close>
 
 abbreviation "P_dnorm \<tau> \<upsilon> \<equiv> (\<mu> X. (\<lambda> s. \<box> e \<in> (\<tau> s) \<rightarrow> X (\<upsilon> s e)))"
 
 notation      P_dnorm ("P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>_,_\<rbrakk>" 60)
 
 lemma dnorm_cont[simp]:
   fixes \<tau>::"'\<sigma>::type \<Rightarrow> 'event::type set" and \<upsilon>::"'\<sigma> \<Rightarrow> 'event \<Rightarrow> '\<sigma>"
   shows "cont (\<lambda>X. (\<lambda>s. \<box> e \<in> (\<tau> s) \<rightarrow> X (\<upsilon> s e)))" (is "cont ?f")
 proof -
   have  "cont (\<lambda>X. ?f X s)" for s by (simp add:cont_fun) 
   then show ?thesis by simp
 qed
 
 section\<open>Interleaving product lemma\<close>
 
 lemma dnorm_inter:  
   fixes \<tau>\<^sub>1 ::"'\<sigma>\<^sub>1::type \<Rightarrow> 'event::type set" and \<tau>\<^sub>2::"'\<sigma>\<^sub>2::type \<Rightarrow> 'event set" 
     and \<upsilon>\<^sub>1 ::"'\<sigma>\<^sub>1 \<Rightarrow> 'event \<Rightarrow> '\<sigma>\<^sub>1"          and \<upsilon>\<^sub>2::"'\<sigma>\<^sub>2 \<Rightarrow> 'event \<Rightarrow> '\<sigma>\<^sub>2"
   defines P: "P \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk>" (is "P \<equiv> fix\<cdot>(\<Lambda> X. ?P X)")
   defines Q: "Q \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk>" (is "Q \<equiv> fix\<cdot>(\<Lambda> X. ?Q X)")
 
   assumes indep: \<open>\<forall>s\<^sub>1 s\<^sub>2. \<tau>\<^sub>1 s\<^sub>1 \<inter> \<tau>\<^sub>2 s\<^sub>2 = {}\<close>
 
   defines Tr: "\<tau> \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2). \<tau>\<^sub>1 s\<^sub>1 \<union> \<tau>\<^sub>2 s\<^sub>2)"
   defines Up: "\<upsilon> \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2) e. if e \<in> \<tau>\<^sub>1 s\<^sub>1 then (\<upsilon>\<^sub>1 s\<^sub>1 e,s\<^sub>2)
                                 else if e \<in> \<tau>\<^sub>2 s\<^sub>2 then (s\<^sub>1, \<upsilon>\<^sub>2 s\<^sub>2 e) else (s\<^sub>1,s\<^sub>2))"  
   defines S: "S \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk>" (is "S \<equiv> fix\<cdot>(\<Lambda> X. ?S X)")
   
   shows "(P s\<^sub>1 ||| Q s\<^sub>2) = S (s\<^sub>1,s\<^sub>2)"
 
 proof -
   have P_rec: "P = ?P P" using fix_eq[of "(\<Lambda> X. ?P X)"] P by simp 
   have Q_rec: "Q = ?Q Q" using fix_eq[of "(\<Lambda> X. ?Q X)"] Q by simp 
   have S_rec: "S = ?S S" using fix_eq[of "(\<Lambda> X. ?S X)"] S by simp
   have dir1: "\<forall> s\<^sub>1 s\<^sub>2. (P s\<^sub>1 ||| Q s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D S (s\<^sub>1, s\<^sub>2)"
   proof(subst P, subst Q, 
         induct rule:parallel_fix_ind_inc[of "\<lambda>x y. \<forall> s\<^sub>1 s\<^sub>2. (x s\<^sub>1 ||| y s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D S (s\<^sub>1,s\<^sub>2)"])
     case admissibility
     then show ?case
         by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
   next
     case (base_fst y)
     then show ?case by (metis app_strict BOT_leFD Sync_BOT Sync_commute)
   next
     case (base_snd x)
     then show ?case by (simp add: Sync_BOT)
   next
     case (step x)
     then show ?case (is "\<forall> s\<^sub>1 s\<^sub>2. ?C s\<^sub>1 s\<^sub>2")
       proof(intro allI)
         fix s\<^sub>1 s\<^sub>2
         show "?C s\<^sub>1 s\<^sub>2"
           apply simp
           apply (subst Mprefix_Sync_distr_indep[where S = "{}", simplified])
           apply (subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
           apply (intro mono_Det_FD mono_Mprefix_FD)
           using step(3)[simplified] indep apply simp
           using step(2)[simplified] indep by fastforce
       qed
     qed         
   have dir2: "\<forall> s\<^sub>1 s\<^sub>2.  S (s\<^sub>1, s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D (P s\<^sub>1 ||| Q s\<^sub>2)"
     proof(subst S, induct rule:fix_ind_k[of "\<lambda>x. \<forall> s\<^sub>1 s\<^sub>2. x (s\<^sub>1,s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D (P s\<^sub>1 ||| Q s\<^sub>2)" 1])
       case admissibility
       show ?case  by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI) 
     next
       case base_k_steps
       then show ?case by simp
     next
       case step
       then show ?case (is "\<forall> s\<^sub>1 s\<^sub>2. ?C s\<^sub>1 s\<^sub>2")
       proof(intro allI)
         fix s\<^sub>1 s\<^sub>2
         have P_rec_sym:"Mprefix (\<tau>\<^sub>1 s\<^sub>1) (\<lambda>e. P (\<upsilon>\<^sub>1 s\<^sub>1 e)) = P s\<^sub>1" using P_rec by metis
         have Q_rec_sym:"Mprefix (\<tau>\<^sub>2 s\<^sub>2) (\<lambda>e. Q (\<upsilon>\<^sub>2 s\<^sub>2 e)) = Q s\<^sub>2" using Q_rec by metis
         show "?C s\<^sub>1 s\<^sub>2"
           apply (simp add: Tr Up Mprefix_Un_distrib)
           apply (subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_indep[where S="{}", simplified])
           apply (intro mono_Det_FD mono_Mprefix_FD)
           apply (subst Q_rec_sym, simp add:step[simplified])
           apply (subst P_rec_sym) using step[simplified] indep by fastforce
       qed
     qed
   from dir1 dir2 show ?thesis using FD_antisym by blast
 qed
 
 section \<open>Synchronous product lemma\<close>
 
 lemma dnorm_par:  
   fixes \<tau>\<^sub>1 ::"'\<sigma>\<^sub>1::type \<Rightarrow> 'event::type set" and \<tau>\<^sub>2::"'\<sigma>\<^sub>2::type \<Rightarrow> 'event set" 
     and \<upsilon>\<^sub>1 ::"'\<sigma>\<^sub>1 \<Rightarrow> 'event \<Rightarrow> '\<sigma>\<^sub>1"          and \<upsilon>\<^sub>2::"'\<sigma>\<^sub>2 \<Rightarrow> 'event \<Rightarrow> '\<sigma>\<^sub>2"
   defines P: "P \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk>" (is "P \<equiv> fix\<cdot>(\<Lambda> X. ?P X)")
   defines Q: "Q \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk>" (is "Q \<equiv> fix\<cdot>(\<Lambda> X. ?Q X)")
 
   defines Tr: "\<tau> \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2).  \<tau>\<^sub>1 s\<^sub>1 \<inter> \<tau>\<^sub>2 s\<^sub>2)"
   defines Up: "\<upsilon> \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2) e. (\<upsilon>\<^sub>1 s\<^sub>1 e, \<upsilon>\<^sub>2 s\<^sub>2 e))"  
   defines S: "S \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk>" (is "S \<equiv> fix\<cdot>(\<Lambda> X. ?S X)")
   
   shows "(P s\<^sub>1 || Q s\<^sub>2) = S (s\<^sub>1,s\<^sub>2)"
 
 proof -
   have P_rec: "P = ?P P" using fix_eq[of "(\<Lambda> X. ?P X)"] P by simp 
   have Q_rec: "Q = ?Q Q" using fix_eq[of "(\<Lambda> X. ?Q X)"] Q by simp 
   have S_rec: "S = ?S S" using fix_eq[of "(\<Lambda> X. ?S X)"] S by simp
   have dir1: "\<forall> s\<^sub>1 s\<^sub>2. (P s\<^sub>1 || Q s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D S (s\<^sub>1, s\<^sub>2)"
   proof(subst P, subst Q, 
         induct rule:parallel_fix_ind[of "\<lambda>x y. \<forall> s\<^sub>1 s\<^sub>2. (x s\<^sub>1 || y s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D S (s\<^sub>1,s\<^sub>2)"])
       case adm:1
       then show ?case
         by (intro adm_all le_FD_adm) (simp_all add: cont2cont_fun monofunI)
     next
       case base:2
       then show ?case by (simp add: Sync_BOT)
     next
       case step:(3 x y)
       then show ?case (is "\<forall> s\<^sub>1 s\<^sub>2. ?C s\<^sub>1 s\<^sub>2")
       proof(intro allI)
         fix s\<^sub>1 s\<^sub>2
         show "?C s\<^sub>1 s\<^sub>2"
           apply(simp)
           apply(subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
           apply(subst S_rec, simp add: Tr Up Mprefix_Un_distrib)
           by (simp add: step)
       qed
     qed     
   have dir2: "\<forall> s\<^sub>1 s\<^sub>2.  S (s\<^sub>1, s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D (P s\<^sub>1 || Q s\<^sub>2)"
     proof(subst S, induct rule:fix_ind_k[of "\<lambda>x. \<forall> s\<^sub>1 s\<^sub>2. x (s\<^sub>1,s\<^sub>2) \<sqsubseteq>\<^sub>F\<^sub>D (P s\<^sub>1 || Q s\<^sub>2)" 1])
       case admissibility
       show ?case  by (intro adm_all le_FD_adm) (simp_all add: cont_fun monofunI) 
     next
       case base_k_steps
       then show ?case by simp
     next
       case step
       then show ?case (is "\<forall> s\<^sub>1 s\<^sub>2. ?C s\<^sub>1 s\<^sub>2")
       proof(intro allI)
         fix s\<^sub>1 s\<^sub>2
         have P_rec_sym:"Mprefix (\<tau>\<^sub>1 s\<^sub>1) (\<lambda>e. P (\<upsilon>\<^sub>1 s\<^sub>1 e)) = P s\<^sub>1" using P_rec by metis
         have Q_rec_sym:"Mprefix (\<tau>\<^sub>2 s\<^sub>2) (\<lambda>e. Q (\<upsilon>\<^sub>2 s\<^sub>2 e)) = Q s\<^sub>2" using Q_rec by metis
         show "?C s\<^sub>1 s\<^sub>2"
           apply(simp add: Tr Up)
           apply(subst P_rec, subst Q_rec, subst Mprefix_Sync_distr_subset[where S="UNIV", simplified])
           apply(rule mono_Mprefix_FD) 
           using step by auto
       qed
     qed
   from dir1 dir2 show ?thesis using FD_antisym by blast
 qed
 
 section\<open>Consequences\<close>
 
 \<comment>\<open>reachable states from one starting state\<close>
 
 inductive_set \<RR> for     \<tau>  ::"'\<sigma>::type \<Rightarrow> 'event::type set"
                     and \<upsilon>  ::"'\<sigma> \<Rightarrow> 'event \<Rightarrow> '\<sigma>" 
                     and \<sigma>\<^sub>0 ::'\<sigma> 
   where rbase: "\<sigma>\<^sub>0 \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0"
       | rstep: "s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 \<Longrightarrow> e \<in> \<tau> s  \<Longrightarrow> \<upsilon> s e \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0"
 
 
 
 \<comment>\<open>Deadlock freeness\<close>
 lemma deadlock_free_dnorm_ :
   fixes \<tau> ::"'\<sigma>::type \<Rightarrow> 'event::type set" 
     and \<upsilon> ::"'\<sigma> \<Rightarrow> 'event \<Rightarrow> '\<sigma>" 
     and \<sigma>\<^sub>0 ::'\<sigma> 
   assumes non_reachable_sink: "\<forall>s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0. \<tau> s \<noteq> {}"
   defines P: "P \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk>" (is "P \<equiv> fix\<cdot>(\<Lambda> X. ?P X)")
   shows  "s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 \<Longrightarrow> deadlock_free_v2 (P s)"
 proof(unfold deadlock_free_v2_FD DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P_def, induct arbitrary:s rule:fix_ind)
   show "adm (\<lambda>a. \<forall>x. x \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 \<longrightarrow> a \<sqsubseteq>\<^sub>F\<^sub>D P x)" by (simp add: monofun_def) 
 next
   fix s :: "'\<sigma>" 
   show "s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 \<Longrightarrow> \<bottom> \<sqsubseteq>\<^sub>F\<^sub>D P s" by simp
 next
   fix s :: "'\<sigma>"  and x :: "'event process"
   have P_rec: "P = ?P P" using fix_eq[of "(\<Lambda> X. ?P X)"] P by simp 
   assume 1 : "\<And>s. s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 \<Longrightarrow> x \<sqsubseteq>\<^sub>F\<^sub>D P s" 
    and   2 : "s \<in> \<RR> \<tau> \<upsilon> \<sigma>\<^sub>0 "
   from   1 2 show "(\<Lambda> x. (\<sqinter>xa\<in>UNIV \<rightarrow>  x) \<sqinter> SKIP)\<cdot>x \<sqsubseteq>\<^sub>F\<^sub>D P s"
     apply (subst P_rec, rule_tac trans_FD[rotated, OF Mprefix_refines_Mndetprefix_FD])
     apply simp
     apply (rule mono_Ndet_FD_left)
     apply (rule trans_FD[OF mono_Mndetprefix_FD_set[of \<open>\<tau> s\<close> \<open>UNIV\<close>]
                             mono_Mndetprefix_FD[rule_format, OF 1]])
     using non_reachable_sink[rule_format, OF 2] apply assumption
     by blast (meson \<RR>.rstep)
 qed
 
 
 
 lemmas deadlock_free_dnorm = deadlock_free_dnorm_[rotated, OF rbase, rule_format]
 
 end
 
diff --git a/thys/CSP_RefTK/Properties.thy b/thys/CSP_RefTK/Properties.thy
deleted file mode 100644
--- a/thys/CSP_RefTK/Properties.thy
+++ /dev/null
@@ -1,133 +0,0 @@
-\<comment>\<open> ******************************************************************** 
- * 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.
- ******************************************************************************\<close>
-
-theory Properties
-  imports "HOL-CSP.Assertions"
-begin
-
-
-
-section \<open>Non-terminating Runs\<close>
-
-definition non_terminating  :: "'a process \<Rightarrow> bool"
-  where   "non_terminating P \<equiv> RUN UNIV \<sqsubseteq>\<^sub>T P"
-
-corollary non_terminating_refine_DF: "non_terminating P = DF UNIV \<sqsubseteq>\<^sub>T P"
-  and non_terminating_refine_CHAOS: "non_terminating P = CHAOS UNIV \<sqsubseteq>\<^sub>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) \<longleftrightarrow> (\<forall>s\<in>\<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 \<Longrightarrow> \<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 \<Longrightarrow> CHAOS UNIV \<sqsubseteq>\<^sub>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 \<sqsubseteq>\<^sub>F P"
-  by (auto simp add:non_terminating_implies_F non_terminating_refine_CHAOS leF_imp_leT)
-
-corollary non_terminating_FD: "non_terminating P = CHAOS UNIV \<sqsubseteq>\<^sub>F\<^sub>D P"
-  unfolding non_terminating_F
-  using div_free_CHAOS nonterminating_implies_div_free leFD_imp_leF
-        leF_leD_imp_leFD divergence_refine_def non_terminating_F 
-  by fastforce 
-
-
-section \<open>Lifelock Freeness\<close>
-
-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 = {} \<longleftrightarrow> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>D P" 
-  "\<D> P = {} \<longleftrightarrow> CHAOS UNIV    \<sqsubseteq>\<^sub>D P" 
-  "\<D> P = {} \<longleftrightarrow> RUN UNIV      \<sqsubseteq>\<^sub>D P" 
-  "\<D> P = {} \<longleftrightarrow> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV    \<sqsubseteq>\<^sub>D P" 
-  "\<D> P = {} \<longleftrightarrow> DF UNIV       \<sqsubseteq>\<^sub>D P" 
-  by (simp_all add: div_free_CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P div_free_CHAOS div_free_RUN div_free_DF 
-                    div_free_DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P divergence_refine_def)
-
-definition lifelock_free_v2 :: "'a process \<Rightarrow> bool"
-  where   "lifelock_free_v2 P \<equiv> CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>F\<^sub>D P"
-
-lemma div_free_is_lifelock_free_v2: "lifelock_free_v2 P \<longleftrightarrow> \<D> P = {}"
-  using CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P_has_all_failures_Un leFD_imp_leD leF_leD_imp_leFD
-        div_free_divergence_refine(1) lifelock_free_v2_def 
-  by blast
-  
-lemma lifelock_free_is_lifelock_free_v2: "lifelock_free P \<Longrightarrow> lifelock_free_v2 P"
-  by (simp add: leFD_imp_leD 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 \<Longrightarrow> lifelock_free_v2 P"
-  by (simp add: deadlock_free_v2_implies_div_free div_free_is_lifelock_free_v2)
-
-
-section \<open>New laws\<close>
-
-lemma non_terminating_Seq: 
-  "non_terminating P \<Longrightarrow> (P \<^bold>; 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_Sync: 
-  "non_terminating P \<Longrightarrow> lifelock_free_v2 Q \<Longrightarrow> non_terminating (P \<lbrakk>A\<rbrakk> Q)"
-  apply(auto simp add: non_terminating_is_right div_free_is_lifelock_free_v2 T_Sync) 
-  apply (metis equals0D ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)
-  apply (meson NT_ND is_processT7_S tickFree_append)
-  by (metis D_T empty_iff ftf_Sync1 ftf_Sync21 insertI1 tickFree_def)
-
-lemmas non_terminating_Par = non_terminating_Sync[where A = \<open>UNIV\<close>]
-   and non_terminating_Inter = non_terminating_Sync[where A = \<open>{}\<close>]
-
-
-end
diff --git a/thys/CSP_RefTK/ROOT b/thys/CSP_RefTK/ROOT
--- a/thys/CSP_RefTK/ROOT
+++ b/thys/CSP_RefTK/ROOT
@@ -1,66 +1,65 @@
 chapter AFP
 
 (*****************************************************************************
  *
  * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
  * Version         : 2.0
  *
  * Author          : Burkhart Wolff, Safouan Taha & Lina Ye
  *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
  *
  * This file       : The Process Refinement Toolkit CSP_RefTK
  *
  * 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.
  ******************************************************************************)
 (* $Id:$ *)
 
-session "CSP_RefTK" = "HOL-CSP" +
+session "CSP_RefTK" (AFP) = "HOL-CSP" +
   description  \<open>An Environment for Advanced Refinement Proofs based on Normalization.
                 Together with a proof of the generalized dining philosophers problem.\<close> 
-  options [timeout = 1200, quick_and_dirty]
+  options [document = pdf, document_output = "output",timeout = 1200]
   sessions
      "HOLCF-Library"
   theories
      Introduction
-     Properties
      Process_norm
      CopyBuffer_props
      DiningPhilosophers
      Conclusion
   document_files
     "root.tex"
     "adb-long.bib"
     "root.bib"
     "figures/session_graph.pdf"