default class checking bug fixed; new attributes for default classes in ontological macros Definition* Theorem* Lemma*
This commit is contained in:
parent
c11e68e3ea
commit
8771d8581b
|
|
@ -8,6 +8,9 @@ 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"]]
|
||||
|
||||
setup \<open> DOF_lib.define_shortcut \<^binding>\<open>csp\<close> "CSP"
|
||||
#> DOF_lib.define_shortcut \<^binding>\<open>isabelle\<close> "Isabelle/HOL"\<close>
|
||||
|
|
@ -528,15 +531,17 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
|
|||
%thus must be without it.
|
||||
\<close>
|
||||
|
||||
text*[X22::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||
text*[X32::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X42::"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>\<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>
|
||||
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 @{definition X22} represents the process that accepts all
|
||||
text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all
|
||||
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
||||
@{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>
|
||||
|
||||
@{definition X32} and @{definition X42} @{definition X52}: 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>
|
||||
(*>*)
|
||||
|
||||
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>
|
||||
|
|
@ -605,8 +610,7 @@ In the literature, deadlock and lifelock are phenomena that are often
|
|||
handled separately. One contribution of our work is establish their precise relationship inside
|
||||
the Failure/Divergence Semantics of \<^csp>.\<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>
|
||||
Definition*[X10]\<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>
|
||||
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
|
||||
|
|
@ -635,9 +639,9 @@ 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>
|
||||
|
||||
text\<open>
|
||||
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 \<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
|
||||
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 \<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
|
||||
separately, such as FDR for which checking livelock-freeness is very costly.
|
||||
In our framework, deadlock-freeness of a given system
|
||||
implies its livelock-freeness. However, if a system is not deadlock-free,
|
||||
|
|
|
|||
|
|
@ -98,7 +98,7 @@ fun transform_cid thy NONE X = X
|
|||
in if DOF_core.is_subclass_global thy sub_cid_long cid_long
|
||||
then (SOME (sub_cid,pos))
|
||||
else (* (SOME (sub_cid,pos)) *)
|
||||
(* BUG : check reveals problem of Definition* misuse. *)
|
||||
(* BUG : check reveals problem of Definition* misuse. *)
|
||||
error("class "^sub_cid_long^
|
||||
" must be sub-class of "^cid_long)
|
||||
end
|
||||
|
|
|
|||
|
|
@ -909,8 +909,8 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) =
|
|||
| _ => error("can not infer type for: "^ name)
|
||||
in if cid <> DOF_core.default_cid
|
||||
andalso not(DOF_core.is_subclass ctxt cid req_class)
|
||||
then error("reference ontologically inconsistent: "^
|
||||
Position.here pos_decl)
|
||||
then error("reference ontologically inconsistent: "
|
||||
^cid^" vs. "^req_class^ Position.here pos_decl)
|
||||
else ()
|
||||
end
|
||||
else err ("faulty reference to docitem: "^name) pos
|
||||
|
|
@ -1533,9 +1533,9 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_re
|
|||
val markup = docref_markup false name id pos_decl;
|
||||
val _ = Context_Position.report ctxt pos markup;
|
||||
(* this sends a report for a ref application to the PIDE interface ... *)
|
||||
val _ = if cid <> DOF_core.default_cid
|
||||
andalso not(DOF_core.is_subclass ctxt cid cid_decl)
|
||||
then error("reference ontologically inconsistent:" ^ Position.here pos_decl)
|
||||
val _ = if not(DOF_core.is_subclass ctxt cid cid_decl)
|
||||
then error("reference ontologically inconsistent: "^cid
|
||||
^" must be subclass of "^cid_decl^ Position.here pos_decl)
|
||||
else ()
|
||||
in () end
|
||||
else if DOF_core.is_declared_oid_global name thy
|
||||
|
|
|
|||
|
|
@ -244,38 +244,79 @@ doc_class "math_example" = math_content +
|
|||
mcc :: "math_content_class" <= "expl"
|
||||
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
|
||||
|
||||
subsection\<open>Ontological Macros\<close>
|
||||
|
||||
subsection\<open>Ontological Macros \<^verbatim>\<open>Definition*\<close> , \<^verbatim>\<open>Lemma**\<close>, \<^verbatim>\<open>Theorem*\<close> ... \<close>
|
||||
|
||||
text\<open>These ontological macros allow notations are defined for the class
|
||||
\<^typ>\<open>math_content\<close> in order to allow for a variety of free-form formats;
|
||||
in order to provide specific sub-classes, default options can be set
|
||||
in order to support more succinct notations and avoid constructs
|
||||
such as :
|
||||
|
||||
\<^theory_text>\<open>Definition*[l::"definition"]\<open>...\<close>\<close>.
|
||||
|
||||
Instead, the more convenient global declaration
|
||||
\<^theory_text>\<open>declare[[Definition_default_class="definition"]]\<close>
|
||||
supports subsequent abbreviations:
|
||||
|
||||
\<^theory_text>\<open>Definition*[l]\<open>...\<close>\<close>.
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
val (Definition_default_class, Definition_default_class_setup)
|
||||
= Attrib.config_string \<^binding>\<open>Definition_default_class\<close> (K "");
|
||||
val (Lemma_default_class, Lemma_default_class_setup)
|
||||
= Attrib.config_string \<^binding>\<open>Lemma_default_class\<close> (K "");
|
||||
val (Theorem_default_class, Theorem_default_class_setup)
|
||||
= Attrib.config_string \<^binding>\<open>Theorem_default_class\<close> (K "");
|
||||
|
||||
|
||||
\<close>
|
||||
setup\<open>Definition_default_class_setup\<close>
|
||||
setup\<open>Lemma_default_class_setup\<close>
|
||||
setup\<open>Theorem_default_class_setup\<close>
|
||||
|
||||
ML\<open> local open ODL_Command_Parser in
|
||||
(* *********************************************************************** *)
|
||||
(* Ontological Macro Command Support *)
|
||||
(* *********************************************************************** *)
|
||||
|
||||
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
|
||||
accepted. *)
|
||||
(* {markdown = true} sets the parsing process such that in the text-core
|
||||
markdown elements are accepted. *)
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command
|
||||
(SOME "math_content") (* should be (SOME "definition") *)
|
||||
[("mcc","defn")]
|
||||
{markdown = true} )));
|
||||
|
||||
val _ = let fun use_Definition_default thy =
|
||||
let val ddc = Config.get_global thy Definition_default_class
|
||||
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
|
||||
in Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (fn args => fn thy =>
|
||||
Onto_Macros.enriched_formal_statement_command
|
||||
(use_Definition_default thy)
|
||||
[("mcc","defn")]
|
||||
{markdown = true} args thy)))
|
||||
end;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command
|
||||
(SOME "lemma")
|
||||
[("mcc","lem")]
|
||||
{markdown = true} )));
|
||||
val _ = let fun use_Lemma_default thy =
|
||||
let val ddc = Config.get_global thy Definition_default_class
|
||||
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
|
||||
in Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (fn args => fn thy =>
|
||||
Onto_Macros.enriched_formal_statement_command
|
||||
(use_Lemma_default thy)
|
||||
[("mcc","lem")]
|
||||
{markdown = true} args thy)))
|
||||
end;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command
|
||||
(SOME "theorem")
|
||||
[("mcc","thm")]
|
||||
{markdown = true} )));
|
||||
val _ = let fun use_Theorem_default thy =
|
||||
let val ddc = Config.get_global thy Definition_default_class
|
||||
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
|
||||
in Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
|
||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||
>> (Toplevel.theory o (fn args => fn thy =>
|
||||
Onto_Macros.enriched_formal_statement_command
|
||||
(use_Theorem_default thy)
|
||||
[("mcc","thm")]
|
||||
{markdown = true} args thy)))
|
||||
end;
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
|
@ -442,10 +483,6 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
|
|||
|
||||
section\<open>Miscelleous\<close>
|
||||
|
||||
ML\<open>
|
||||
Parse.int
|
||||
\<close>
|
||||
|
||||
subsection\<open>Layout Trimming Commands\<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>
|
||||
|
|
|
|||
Loading…
Reference in New Issue