first version with macro syntax (no ML support)
This commit is contained in:
parent
de5c0fc6e2
commit
5593c22a36
|
|
@ -26,8 +26,7 @@ define_shortcut* isadof \<rightleftharpoons> \<open>\isadof\<close>
|
|||
Protege \<rightleftharpoons> \<open>Prot{\'e}g{\'e}\<close>
|
||||
|
||||
(* slanted text in contrast to italics *)
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>slanted_text\<close> "\\textsl{" "}" (K(K()))\<close>
|
||||
|
||||
define_macro* slanted_text \<rightleftharpoons> \<open>\textsl{\<close> \<open>}\<close>
|
||||
|
||||
(*>*)
|
||||
|
||||
|
|
|
|||
|
|
@ -1,18 +1,18 @@
|
|||
(*<*)
|
||||
theory "paper"
|
||||
imports
|
||||
"Isabelle_DOF.scholarly_paper"
|
||||
imports "Isabelle_DOF.scholarly_paper"
|
||||
begin
|
||||
|
||||
|
||||
open_monitor*[this::article]
|
||||
|
||||
declare[[strict_monitor_checking = false]]
|
||||
declare[[ Definition_default_class="definition"]]
|
||||
declare[[ Lemma_default_class="lemma"]]
|
||||
declare[[ Theorem_default_class="theorem"]]
|
||||
declare[[ strict_monitor_checking = false]]
|
||||
declare[[ Definition_default_class = "definition"]]
|
||||
declare[[ Lemma_default_class = "lemma"]]
|
||||
declare[[ Theorem_default_class = "theorem"]]
|
||||
|
||||
define_shortcut* csp \<rightleftharpoons> \<open>CSP\<close>
|
||||
holcsp \<rightleftharpoons> \<open>HOL-CSP\<close>
|
||||
isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
|
||||
|
||||
(*>*)
|
||||
|
|
@ -24,7 +24,7 @@ author*[bu,email= "\<open>wolff@lri.fr\<close>",affiliation = "\<open>LRI, Unive
|
|||
author*[lina,email="\<open>lina.ye@lri.fr\<close>",affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]\<open>Lina Ye\<close>
|
||||
|
||||
abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
|
||||
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
|
||||
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
|
||||
\<open> The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today
|
||||
one of the reference theories for concurrent specification and computing. In 1997, a first
|
||||
formalization in \<^isabelle> of the denotational semantics of the Failure/Divergence Model of
|
||||
|
|
@ -63,8 +63,8 @@ systems, such as the T9000 transansputer @{cite "Barret95"}.
|
|||
The theory of \<^csp> was first described in 1978 in a book by Tony Hoare @{cite "Hoare:1985:CSP:3921"},
|
||||
but has since evolved substantially @{cite "BrookesHR84" and "brookes-roscoe85" and "roscoe:csp:1998"}.
|
||||
\<^csp> describes the most common communication and synchronization mechanisms
|
||||
with one single language primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is described
|
||||
by a fully abstract model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational
|
||||
with one single language primitive: synchronous communication written \<open>_\<lbrakk>_\<rbrakk>_\<close>. \<^csp> semantics is
|
||||
described by a fully abstract model of behaviour designed to be \<^emph>\<open>compositional\<close>: the denotational
|
||||
semantics of a process \<open>P\<close> encompasses all possible behaviours of this process in the context of all
|
||||
possible environments \<open>P \<lbrakk>S\<rbrakk> Env\<close> (where \<open>S\<close> is the set of \<open>atomic events\<close> both \<open>P\<close> and \<open>Env\<close> must
|
||||
synchronize). This design objective has the consequence that two kinds of choice have to
|
||||
|
|
@ -248,7 +248,7 @@ Second, in the traditional literature, the semantic domain is implicitly describ
|
|||
over the three semantic functions \<open>\<T>\<close>, \<open>\<F>\<close> and \<open>\<D>\<close>.
|
||||
Informally, these are:
|
||||
|
||||
\<^item> the initial trace of a process must be empty;
|
||||
\<^item> the initial trace of a process must be empty;
|
||||
\<^item> any allowed trace must be \<open>front\<^sub>-tickFree\<close>;
|
||||
\<^item> traces of a process are \<^emph>\<open>prefix-closed\<close>;
|
||||
\<^item> a process can refuse all subsets of a refusal set;
|
||||
|
|
@ -272,10 +272,10 @@ Informally, these are:
|
|||
(\<forall> s t. s \<in> \<D> P \<and> tickFree s \<and> front_tickFree t \<longrightarrow> s@t \<in> \<D> P) \<and>
|
||||
(\<forall> s X. s \<in> \<D> P \<longrightarrow> (s,X) \<in> \<F> P) \<and>
|
||||
(\<forall> s. s@[\<surd>] \<in> \<D> P \<longrightarrow> s \<in> \<D> P)\<close>}
|
||||
|
||||
\<^vs>\<open>-0.1cm\<close>
|
||||
|
||||
Our objective is to encapsulate this wishlist into a type constructed as a conservative
|
||||
theory extension in our theory HOL-\<^csp>.
|
||||
theory extension in our theory \<^holcsp>.
|
||||
Therefore third, we define a pre-type for processes \<open>\<Sigma> process\<^sub>0\<close> by \<open> \<P>(\<Sigma>\<^sup>\<surd>\<^sup>* \<times> \<P>(\<Sigma>\<^sup>\<surd>)) \<times> \<P>(\<Sigma>\<^sup>\<surd>)\<close>.
|
||||
Forth, we turn our wishlist of "axioms" above into the definition of a predicate \<open>is_process P\<close>
|
||||
of type \<open>\<Sigma> process\<^sub>0 \<Rightarrow> bool\<close> deciding if its conditions are fulfilled. Since \<open>P\<close> is a pre-process,
|
||||
|
|
@ -302,7 +302,7 @@ maintains \<open>is_process\<close>, \<^ie> this predicate remains invariant on
|
|||
For example, we define \<open>_\<sqinter>_\<close> on the pre-process type as follows:
|
||||
|
||||
\<^vs>\<open>0.1cm\<close>
|
||||
\<^item> \<^theory_text>\<open>definition "P \<sqinter> Q \<equiv> Abs_process(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)"\<close>
|
||||
\<^item> \<^theory_text>\<open>definition "P \<sqinter> Q \<equiv> Abs_processxx(\<F> P \<union> \<F> Q , \<D> P \<union> \<D> Q)"\<close>
|
||||
|
||||
\<^vs>\<open>-0.2cm\<close>
|
||||
\<^noindent> where \<open>\<F> = fst \<circ> Rep_process\<close> and \<open>\<D> = snd \<circ> Rep_process\<close> and where \<open>Rep_process\<close> and
|
||||
|
|
@ -532,9 +532,9 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
|
|||
\<close>
|
||||
|
||||
(*<*) (* a test ...*)
|
||||
text*[X22 ::math_content ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close> \<close>
|
||||
text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X)) \<^vs>\<open>-0.7cm\<close>\<close>\<close>
|
||||
Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
text*[X22 ::math_content ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X52::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
|
||||
text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all
|
||||
|
|
@ -546,21 +546,19 @@ stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I
|
|||
Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X4]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<^vs>\<open>-0.7cm\<close> \<close>
|
||||
Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<^vs>\<open>-0.7cm\<close>\<close>
|
||||
Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<^vs>\<open>-0.7cm\<close> \<close>
|
||||
|
||||
text\<open> \<^vs>\<open>-0.3cm\<close> \<^noindent>
|
||||
In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>.
|
||||
text\<open> \<^vs>\<open>-0.3cm\<close> \<^noindent> In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>.
|
||||
All five reference processes are divergence-free.
|
||||
%which was done by using a particular lemma \<open>\<D> (\<mu> x. f x) = \<Inter>\<^sub>i\<^sub>\<in>\<^sub>\<nat> \<D> (f\<^sup>i \<bottom>)\<close>.
|
||||
|
||||
\<^vs>\<open>-0.2cm\<close>
|
||||
@{cartouche [display,indent=8] \<open> D (\<PP> UNIV) = {} where \<PP> \<in> \<R>\<P> and UNIV is the set of all events\<close>}
|
||||
|
||||
\<^vs>\<open>-0.1cm\<close>
|
||||
@{cartouche
|
||||
[display,indent=8] \<open> D (\<PP> UNIV) = {} where \<PP> \<in> \<R>\<P> and UNIV is the set of all events\<close>
|
||||
}
|
||||
Regarding the failure refinement ordering, the set of failures \<open>\<F> P\<close> for any process \<open>P\<close> is
|
||||
a subset of \<open>\<F> (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\<close>.% and the following lemma was proved:
|
||||
% This proof is performed by induction, based on the failure projection of \<open>STOP\<close> and that of internal choice.
|
||||
% This proof is performed by induction, based on the failure projection of \<open>STOP\<close> and that of
|
||||
% internal choice.
|
||||
|
||||
\<^vs>\<open>-0.2cm\<close>
|
||||
@{cartouche [display, indent=25] \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close>}
|
||||
|
|
|
|||
|
|
@ -17,13 +17,11 @@ theory "00_Frontmatter"
|
|||
begin
|
||||
|
||||
|
||||
section\<open>Document Local Setup.\<close>
|
||||
text\<open>Some internal setup, introducing document specific abbreviations and macros.\<close>
|
||||
section\<open>Local Document Setup.\<close>
|
||||
text\<open>... introducing document specific abbreviations and macros.\<close>
|
||||
|
||||
|
||||
|
||||
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
|
||||
isadof \<rightleftharpoons> \<open>\isadof\<close>
|
||||
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
|
||||
isadof \<rightleftharpoons> \<open>\isadof\<close>
|
||||
|
||||
define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
|
||||
BibTeX \<rightleftharpoons> \<open>\BibTeX{}\<close>
|
||||
|
|
@ -32,11 +30,11 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
|
|||
pdf \<rightleftharpoons> \<open>PDF\<close>
|
||||
pdftex \<rightleftharpoons> \<open>\pdftex{}\<close>
|
||||
|
||||
text\<open>Note that these setups assume that the associated \<^LaTeX> macros are defined, \<^eg>,
|
||||
in the document prelude. \<close>
|
||||
text\<open>Note that these setups assume that the associated \<^LaTeX> macros
|
||||
are defined, \<^eg>, in the document prelude. \<close>
|
||||
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>index\<close> "\\index{" "}" (K(K())) (*no checking, no reporting*)
|
||||
#> DOF_lib.define_macro \<^binding>\<open>bindex\<close> "\\bindex{" "}"(K(K()))\<close>
|
||||
define_macro* index \<rightleftharpoons> \<open>\index{\<close> \<open>}\<close>
|
||||
define_macro* bindex \<rightleftharpoons> \<open>\bindex{\<close> \<open>}\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
|
|||
text\<open>
|
||||
In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on
|
||||
the following design-decisions:
|
||||
\<^item> the entire \<^isadof> is a ``pure add-on,'' \ie, we deliberately resign on the possibility to
|
||||
\<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign on the possibility to
|
||||
modify Isabelle itself.
|
||||
\<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation
|
||||
about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}).
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ theory Isa_COL
|
|||
and "figure*" "side_by_side_figure*" :: document_body
|
||||
and "assert*" :: thy_decl
|
||||
|
||||
and "define_shortcut*" :: thy_decl
|
||||
and "define_shortcut*" "define_macro*":: thy_decl
|
||||
|
||||
begin
|
||||
|
||||
|
|
@ -293,9 +293,9 @@ fun define_macro name s1 s2 reportNtest =
|
|||
|
||||
local (* hide away really strange local construction *)
|
||||
fun enclose_body2 front body1 middle body2 post =
|
||||
(if front = "" then [] else [Latex.string front]) @ body1 @
|
||||
(if front = "" then [] else [Latex.string front]) @ body1 @
|
||||
(if middle = "" then [] else [Latex.string middle]) @ body2 @
|
||||
(if post = "" then [] else [Latex.string post]);
|
||||
(if post = "" then [] else [Latex.string post]);
|
||||
in
|
||||
fun define_macro2 name front middle post reportNtest1 reportNtest2 =
|
||||
Thy_Output.antiquotation_raw_embedded name (Scan.lift ( Args.cartouche_input
|
||||
|
|
@ -416,19 +416,33 @@ end
|
|||
|
||||
ML\<open>
|
||||
local
|
||||
val parse_define_shortcut = Parse.binding --
|
||||
((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- (Parse.alt_string || Parse.cartouche))
|
||||
val parse_literal = Parse.alt_string || Parse.cartouche
|
||||
val parse_define_shortcut = Parse.binding -- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal)
|
||||
val define_shortcuts = fold(uncurry DOF_lib.define_shortcut)
|
||||
in
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>define_shortcut*\<close> "define LaTeX shortcut"
|
||||
(Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o define_shortcuts));
|
||||
val _ = Outer_Syntax.command \<^command_keyword>\<open>define_shortcut*\<close> "define LaTeX shortcut"
|
||||
(Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o define_shortcuts));
|
||||
end
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val parse_literal = Parse.alt_string || Parse.cartouche
|
||||
val parse_define_shortcut = (Parse.binding
|
||||
-- ((\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>) |-- parse_literal))
|
||||
-- parse_literal
|
||||
-- (Scan.option (\<^keyword>\<open>(\<close> |-- Parse.ML_source --|\<^keyword>\<open>)\<close>))
|
||||
|
||||
fun define_macro (X,NONE) = (uncurry(uncurry(uncurry DOF_lib.define_macro)))(X,K(K()));
|
||||
|
||||
|
||||
val _ = Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "define LaTeX shortcut"
|
||||
(Scan.repeat1 parse_define_shortcut >> (Toplevel.theory o (fold define_macro)));
|
||||
|
||||
\<close>
|
||||
|
||||
|
||||
section\<open>Tables\<close>
|
||||
(* TODO ! ! ! *)
|
||||
|
||||
(* dito the future monitor: table - block *)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -477,12 +477,17 @@ subsection\<open>Common Abbreviations\<close>
|
|||
|
||||
define_shortcut* eg \<rightleftharpoons> \<open>\eg\<close> (* Latin: „exempli gratia“ meaning „for example“. *)
|
||||
ie \<rightleftharpoons> \<open>\ie\<close> (* Latin: „id est“ meaning „that is to say“. *)
|
||||
etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : et cetera *)
|
||||
etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : „et cetera“ meaning „et cetera“ *)
|
||||
|
||||
subsection\<open>Layout Trimming Commands\<close>
|
||||
|
||||
define_macro* hs \<rightleftharpoons> \<open>\hspace{\<close> \<open>}\<close>
|
||||
define_macro* vs \<rightleftharpoons> \<open>\vspace{\<close> \<open>}\<close>
|
||||
|
||||
(*
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>hs\<close> "\\hspace{" "}" (K(K())) \<close>
|
||||
setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close> "\\vspace{" "}" (K(K())) \<close>
|
||||
*)
|
||||
|
||||
define_shortcut* clearpage \<rightleftharpoons> \<open>\clearpage{}\<close>
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue