Commit 8b92c67e authored by Manuel Eberl's avatar Manuel Eberl
Browse files

New submission: CSP_RefTK

parent 2da14e4d854f
This diff is collapsed.
(*<*)
\<comment>\<open> ********************************************************************
* 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.
******************************************************************************\<close>
(*>*)
chapter\<open>Conclusion\<close>
(*<*)
theory Conclusion
imports HOLCF
begin
(*>*)
text\<open> 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 \<open>P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>,\<upsilon>\<rbrakk>\<close> automatically, thus combining efficient finite reasoning
over finite sub-systems with globally infinite systems in a logically safe way.
\<close>
(*<*)
end
(*>*)
(*<*)
\<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"
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)
unfolding failure_divergence_refine_def
proof -
show "adm (\<lambda>a. a \<le> COPY)" by(rule le_adm, simp_all add:monofunI)
next
have 1:"(\<sqinter>xa\<in> range left \<union> range right \<rightarrow> \<bottom>) \<le> (\<sqinter>xa\<in> range left \<rightarrow> \<bottom>)"
using mndet_subset_FD by (metis UNIV_I empty_iff imageI)
have 2:"(\<sqinter>xa\<in> range left \<rightarrow> \<bottom>) \<le> (left`?`x \<rightarrow> \<bottom>)"
unfolding read_def
by (metis Mprefix_refines_Mndet comp_apply dual_order.antisym mono_mprefix_FD order_refl)
show "(\<sqinter>x\<in>range left \<union> range right \<rightarrow> \<bottom>) \<le> 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 \<le> COPY" and ** : "(\<sqinter>x\<in>range left \<union> range right \<rightarrow> P) \<le> COPY"
have 1:"(\<sqinter>xa\<in> range left \<union> range right \<rightarrow> P) \<le> (\<sqinter>xa\<in> range right \<rightarrow> P)"
using mndet_subset_FD by (metis UNIV_I Un_commute empty_iff imageI)
have 2:"(\<sqinter>xa\<in> range right \<rightarrow> P) \<le> (right`!`x \<rightarrow> 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:"(\<sqinter>xa\<in> range left \<union> range right \<rightarrow> P) \<le> (right`!`x \<rightarrow> P)" for x
using dual_order.trans by blast
hence 3:"(left`?`x \<rightarrow> (\<sqinter>xa\<in> range left \<union> range right \<rightarrow> P)) \<le> (left`?`x \<rightarrow>(right`!`x \<rightarrow> P))"
by (simp add: mono_read_FD)
have 4:"\<And>X. (\<sqinter>xa\<in> range left \<union> range right \<rightarrow> X) \<le> (\<sqinter>xa\<in> range left \<rightarrow> X)"
using mndet_subset_FD by (metis UNIV_I empty_iff imageI)
have 5:"\<And>X. (\<sqinter>xa\<in> range left \<rightarrow> X) \<le> (left`?`x \<rightarrow> X)"
unfolding read_def
by (metis Mprefix_refines_Mndet comp_apply dual_order.antisym mono_mprefix_FD order_refl)
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)) \<le> (left`?`x \<rightarrow> (right`!`x \<rightarrow> P))"
by (meson dual_order.trans)
from * ** have 7:"(left`?`x \<rightarrow> (right`!`x \<rightarrow> P)) \<le> (left`?`x \<rightarrow> (right`!`x \<rightarrow> COPY))"
by (simp add: mono_read_FD mono_write_FD)
show "(\<sqinter>x\<in>range left \<union> range right \<rightarrow> \<sqinter>x\<in>range left \<union> range right \<rightarrow> P) \<le> COPY"
by (metis (mono_tags, lifting) 6 7 COPY_rec dual_order.trans)
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]
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
This diff is collapsed.
(*<*)
\<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
(*<*)
\<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> a theory of explicit state normalisation which allows for proofs over certain
communicating networks of arbitrary size.
\newpage
\<close>
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.
\<^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>
(*<*)
end
(*>*)
(*<*)
\<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" "Fix_ind_ext"
begin
section\<open>Deterministic normal-forms with explicit state\<close>
abbreviation "P_dnorm Tr Up \<equiv> (\<mu> X. (\<lambda> s. \<box> e \<in> (Tr s) \<rightarrow> X (Up s e)))"
notation P_dnorm ("P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>_,_\<rbrakk>" 60)
lemma dnorm_cont[simp]:
fixes Tr::"'state::type \<Rightarrow> 'event::type set" and Up::"'state \<Rightarrow> 'event \<Rightarrow> 'state"
shows "cont (\<lambda>X. (\<lambda>s. \<box> e \<in> (Tr s) \<rightarrow> X (Ur 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 Tr\<^sub>1 ::"'state\<^sub>1::type \<Rightarrow> 'event::type set" and Tr\<^sub>2::"'state\<^sub>2::type \<Rightarrow> 'event set"
and Up\<^sub>1 ::"'state\<^sub>1 \<Rightarrow> 'event \<Rightarrow> 'state\<^sub>1" and Up\<^sub>2::"'state\<^sub>2 \<Rightarrow> 'event \<Rightarrow> 'state\<^sub>2"
defines P: "P \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>Tr\<^sub>1,Up\<^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>Tr\<^sub>2,Up\<^sub>2\<rbrakk>" (is "Q \<equiv> fix\<cdot>(\<Lambda> X. ?Q X)")
assumes indep: \<open>\<forall>s\<^sub>1 s\<^sub>2. Tr\<^sub>1 s\<^sub>1 \<inter> Tr\<^sub>2 s\<^sub>2 = {}\<close>
defines Tr: "Tr \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2). Tr\<^sub>1 s\<^sub>1 \<union> Tr\<^sub>2 s\<^sub>2)"
defines Up: "Up \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2) e. if e \<in> Tr\<^sub>1 s\<^sub>1 then (Up\<^sub>1 s\<^sub>1 e,s\<^sub>2)
else if e \<in> Tr\<^sub>2 s\<^sub>2 then (s\<^sub>1, Up\<^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>Tr,Up\<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> 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> S (s\<^sub>1,s\<^sub>2)"])
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 "\<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_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: "\<forall> s\<^sub>1 s\<^sub>2. S (s\<^sub>1, s\<^sub>2) \<sqsubseteq> (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> (P s\<^sub>1 ||| Q s\<^sub>2)" 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 "\<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 (Tr\<^sub>1 s\<^sub>1) (\<lambda>e. P (Up\<^sub>1 s\<^sub>1 e)) = P s\<^sub>1" using P_rec by metis
have Q_rec_sym:"Mprefix (Tr\<^sub>2 s\<^sub>2) (\<lambda>e. Q (Up\<^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_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 \<open>Synchronous product lemma\<close>
lemma dnorm_par:
fixes Tr\<^sub>1 ::"'state\<^sub>1::type \<Rightarrow> 'event::type set" and Tr\<^sub>2::"'state\<^sub>2::type \<Rightarrow> 'event set"
and Up\<^sub>1 ::"'state\<^sub>1 \<Rightarrow> 'event \<Rightarrow> 'state\<^sub>1" and Up\<^sub>2::"'state\<^sub>2 \<Rightarrow> 'event \<Rightarrow> 'state\<^sub>2"
defines P: "P \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>Tr\<^sub>1,Up\<^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>Tr\<^sub>2,Up\<^sub>2\<rbrakk>" (is "Q \<equiv> fix\<cdot>(\<Lambda> X. ?Q X)")
defines Tr: "Tr \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2). Tr\<^sub>1 s\<^sub>1 \<inter> Tr\<^sub>2 s\<^sub>2)"
defines Up: "Up \<equiv> (\<lambda>(s\<^sub>1,s\<^sub>2) e. (Up\<^sub>1 s\<^sub>1 e, Up\<^sub>2 s\<^sub>2 e))"
defines S: "S \<equiv> P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>Tr,Up\<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