Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

added Lemma*, Theorem* and Definition* support. Bug: referencing does not work.

This commit is contained in:
Burkhart Wolff 2020-11-04 15:55:43 +01:00
parent 4ad06ce39a
commit 2ecb62a80e
5 changed files with 26 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

39
examples/scholarly_paper/2020-iFM-CSP/paper.thy
View File

@ -353,7 +353,7 @@ Roscoe and Brooks @{cite "Roscoe1992AnAO"} finally proposed another ordering, ca
that completeness could at least be assured for read-operations. This more complex ordering that completeness could at least be assured for read-operations. This more complex ordering
is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close> is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close>
text*[process_ordering::"definition", short_name="''process ordering''"]\<open> Definition*[process_ordering, short_name="''process ordering''"]\<open>
We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where \<^vs>\<open>-0.2cm\<close> We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where \<^vs>\<open>-0.2cm\<close>
\<^enum> \<^vs>\<open>-0.2cm\<close> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close> \<^enum> \<^vs>\<open>-0.2cm\<close> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
\<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close> \<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>
@ -528,21 +528,21 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
%thus must be without it. %thus must be without it.
\<close> \<close>
(* (*
text*[X2::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close> Definition*[X22]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
text*[X3::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close> Definition*[X32]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
text*[X4::"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> 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\<open> The \<open>RUN\<close>-process defined @{definition X2} represents the process that accepts all text\<open> The \<open>RUN\<close>-process defined @{definition X22} represents the process that accepts all
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
@{definition X3} and @{definition X4}: the process that non-deterministically stops or @{definition X32} and @{definition X42}: the process that non-deterministically stops or
accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close> accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
*) *)
text*[X2::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close> Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
text*[X3::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<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>
text*[X4::"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> 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>
text*[X5::"definition"]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> 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>
text*[X6::"definition"]\<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*[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> 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>. 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>.
@ -605,18 +605,19 @@ In the literature, deadlock and lifelock are phenomena that are often
handled separately. One contribution of our work is establish their precise relationship inside handled separately. One contribution of our work is establish their precise relationship inside
the Failure/Divergence Semantics of \<^csp>.\<close> the Failure/Divergence Semantics of \<^csp>.\<close>
text*[X10::"definition"] \<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<^vs>\<open>-0.3cm\<close> \<close> (* bizarre: Definition* does not work for this single case *)
text*[X10::"definition"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<^vs>\<open>-0.3cm\<close> \<close>
text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close> text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close>
and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot
be deadlocked after any non-terminating trace. be deadlocked after any non-terminating trace.
\<^vs>\<open>-0.2cm\<close>\<close> \<^vs>\<open>-0.2cm\<close>\<close>
text*[T1::"theorem", short_name="\<open>DF definition captures deadlock-freeness\<close>"] Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]
\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<^vs>\<open>-0.4cm\<close>\<close> \<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<^vs>\<open>-0.4cm\<close>\<close>
text*[X11::"definition"]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<^vs>\<open>-0.2cm\<close>\<close> Definition*[X11]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<^vs>\<open>-0.2cm\<close>\<close>
text\<open> Recall that all five reference processes are livelock-free. text\<open> Recall that all five reference processes are livelock-free.
We also have the following lemmas about the We also have the following lemmas about the
@ -630,12 +631,12 @@ text\<open>\<^vs>\<open>-0.3cm\<close>
Finally, we proved the following theorem that confirms the relationship between the two vital Finally, we proved the following theorem that confirms the relationship between the two vital
properties:\<^vs>\<open>-0.3cm\<close> properties:\<^vs>\<open>-0.3cm\<close>
\<close> \<close>
text*[T2::"theorem", short_name="''DF implies LF''"] Theorem*[T2, short_name="''DF implies LF''"]
\<open> \hspace{0.5cm} \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<^vs>\<open>-0.3cm\<close>\<close> \<open> \hspace{0.5cm} \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<^vs>\<open>-0.3cm\<close>\<close>
text\<open> text\<open>
This is totally natural, at a first glance, but surprising as the proof of deadlock-freeness only requires This is totally natural, at a first glance, but surprising as the proof of deadlock-freeness only requires
failure refinement \<open>\<sqsubseteq>\<^sub>\<F>\<close> (see @{definition X10}) where divergence traces are mixed within the failures set. failure refinement \<open>\<sqsubseteq>\<^sub>\<F>\<close> (see @{definition \<open>X10\<close>}) where divergence traces are mixed within the failures set.
Note that the existing tools in the literature normally detect these two phenomena Note that the existing tools in the literature normally detect these two phenomena
separately, such as FDR for which checking livelock-freeness is very costly. separately, such as FDR for which checking livelock-freeness is very costly.
In our framework, deadlock-freeness of a given system In our framework, deadlock-freeness of a given system
@ -684,7 +685,7 @@ processes and we call the resulting process \<open>SYSTEM\<close>: \<^vs>\<open>
@{theory_text [display,indent=5] \<open> @{theory_text [display,indent=5] \<open>
definition SEND \<equiv> (\<mu> X. left?x \<rightarrow> (mid!x \<rightarrow> (ack \<rightarrow> X))) definition SEND \<equiv> (\<mu> X. left?x \<rightarrow> (mid!x \<rightarrow> (ack \<rightarrow> X)))
definition REC \<equiv> (\<mu> X. mid?x \<rightarrow> (right!x \<rightarrow> (ack \<rightarrow> X))) definition REC \<equiv> (\<mu> X. mid?x \<rightarrow> (right!x \<rightarrow> (ack \<rightarrow> X)))
definition SYN \<equiv> (range mid) \<union> {ack} definition SYN \<equiv> (range mid) \<union> {ack}
definition "SYSTEM \<equiv> (SEND \<lbrakk>SYN\<rbrakk> REC) \\ SYN"\<close>} definition "SYSTEM \<equiv> (SEND \<lbrakk>SYN\<rbrakk> REC) \\ SYN"\<close>}
@ -788,7 +789,7 @@ Roughly similar to labelled transition systems, we provide for deterministic \<^
form that is based on an explicit state. The general schema of normalized processes is defined as form that is based on an explicit state. The general schema of normalized processes is defined as
follows: follows:
\<^vs>\<open>0.1cm\<close> \<^vs>\<open>0.1cm\<close>
@{cartouche [display,indent=20] \<open>P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>,\<upsilon>\<rbrakk> \<equiv> \<mu> X. (\<lambda>\<sigma>. \<box>e\<in>(\<tau> \<sigma>) \<rightarrow> X (\<upsilon> \<sigma> e))\<close>} @{cartouche [display,indent=20] \<open>P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>,\<upsilon>\<rbrakk> \<equiv> \<mu> X. (\<lambda>\<sigma>. \<box>e\<in>(\<tau> \<sigma>) \<rightarrow> X(\<upsilon> \<sigma> e))\<close>}
\<^vs>\<open>-0.1cm\<close> where \<open>\<tau>\<close> is a transition function which returns the set of events that can be triggered from \<^vs>\<open>-0.1cm\<close> where \<open>\<tau>\<close> is a transition function which returns the set of events that can be triggered from
the current state \<open>\<sigma>\<close> given as parameter. the current state \<open>\<sigma>\<close> given as parameter.
The update function \<open>\<upsilon>\<close> takes two parameters \<open>\<sigma>\<close> and an event \<open>e\<close> and returns the new state. The update function \<open>\<upsilon>\<close> takes two parameters \<open>\<sigma>\<close> and an event \<open>e\<close> and returns the new state.
@ -893,7 +894,7 @@ denotational semantics.
%\<open>FORK i = picks \<rightarrow> putsdown \<rightarrow> FORK i\<close>. After that we apply the same method %\<open>FORK i = picks \<rightarrow> putsdown \<rightarrow> FORK i\<close>. After that we apply the same method
%to get the philosopher process under a normal form. %to get the philosopher process under a normal form.
Thanks to @{math_content \<open>T3\<close>}, we obtain normalized processes Thanks to @{theorem \<open>T3\<close>}, we obtain normalized processes
for \<open>FORKs\<close>, \<open>PHILs\<close> and \<open>DINING\<close>: for \<open>FORKs\<close>, \<open>PHILs\<close> and \<open>DINING\<close>:
@{theory_text [display,indent=5] @{theory_text [display,indent=5]
\<open>definition "trans\<^sub>F \<equiv> \<lambda>fs. (\<Inter>\<^sub>i\<^sub><\<^sub>N. trans\<^sub>f i (fs!i))" \<open>definition "trans\<^sub>F \<equiv> \<lambda>fs. (\<Inter>\<^sub>i\<^sub><\<^sub>N. trans\<^sub>f i (fs!i))"

BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/definition-use-CSP.png Executable file → Normal file
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 226 KiB

After

Width:  |  Height:  |  Size: 196 KiB

4
src/DOF/Isa_DOF.thy
View File

@ -1397,13 +1397,13 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
(* for the moment naive, i.e. without textual normalization of (* for the moment naive, i.e. without textual normalization of
attribute names and adapted term printing *) attribute names and adapted term printing *)
let val l = "label = "^ (enclose "{" "}" lab) let val l = "label = "^ (enclose "{" "}" lab)
val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
val cid_long = case cid_opt of val cid_long = case cid_opt of
NONE => (case DOF_core.get_object_global lab thy of NONE => (case DOF_core.get_object_global lab thy of
NONE => DOF_core.default_cid NONE => DOF_core.default_cid
| SOME X => #cid X) | SOME X => #cid X)
| SOME(cid,_) => DOF_core.parse_cid_global thy cid | SOME(cid,_) => DOF_core.parse_cid_global thy cid
val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
val cid_txt = "type = " ^ (enclose "{" "}" cid_long); val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2) fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2)

2
src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
View File

@ -20,7 +20,7 @@
\newtheorem{example}{Example} \newtheorem{example}{Example}
\newtheorem{definition}{Definition} \newtheorem{definition}{Definition}
\newtheorem{theorem}{Theorem} \newtheorem{theorem}{Theorem}

3
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -341,6 +341,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung ! % Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text.scholarly_paper.definition},#1]{\BODY}}
\newisadof{text.scholarly_paper.definition}% \newisadof{text.scholarly_paper.definition}%
[label=,type=% [label=,type=%
, scholarly_paper.math_content.short_name =% , scholarly_paper.math_content.short_name =%
@ -399,6 +400,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Besser: Einfach durchreichen wg Vererbung ! %% Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
\newisadof{text.scholarly_paper.lemma}% \newisadof{text.scholarly_paper.lemma}%
[label=,type=% [label=,type=%
, scholarly_paper.math_content.short_name =% , scholarly_paper.math_content.short_name =%
@ -426,6 +428,7 @@
} }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Besser: Einfach durchreichen wg Vererbung ! % Besser: Einfach durchreichen wg Vererbung !
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
\newisadof{text.scholarly_paper.theorem}% \newisadof{text.scholarly_paper.theorem}%
[label=,type=% [label=,type=%
, scholarly_paper.math_content.short_name =% , scholarly_paper.math_content.short_name =%