diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index 3302e56..00018de 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -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 \ DOF_lib.define_shortcut \<^binding>\csp\ "CSP" #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL"\ @@ -528,15 +531,17 @@ To handle termination better, we added two new processes \CHAOS\<^sub>S\<^ %thus must be without it. \ -text*[X22::"definition"]\\RUN A \ \ X. \ x \ A \ X\ \ -text*[X32::"definition"]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ -Definition*[X42::"definition"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\\ +(*<*) (* a test ...*) +text*[X22 ::math_content ]\\RUN A \ \ X. \ x \ A \ X\ \<^vs>\-0.7cm\ \ +text*[X32::"definition", mcc=defn]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X)) \<^vs>\-0.7cm\\\ +Definition*[X42]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \<^vs>\-0.7cm\\ +Definition*[X52::"definition"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \<^vs>\-0.7cm\\ -text\ The \RUN\-process defined @{definition X22} represents the process that accepts all +text\ The \RUN\-process defined @{math_content X22} represents the process that accepts all events, but never stops nor deadlocks. The \CHAOS\-process comes in two variants shown in -@{definition X32} and @{definition X42}: the process that non-deterministically stops or -accepts any offered event, whereas \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\ can additionally terminate.\ - +@{definition X32} and @{definition X42} @{definition X52}: the process that non-deterministically +stops or accepts any offered event, whereas \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\ can additionally terminate.\ +(*>*) Definition*[X2]\\RUN A \ \ X. \ x \ A \ X\ \<^vs>\-0.7cm\\ Definition*[X3]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \<^vs>\-0.7cm\\ @@ -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>.\ -(* bizarre: Definition* does not work for this single case *) -text*[X10::"definition"]\ \deadlock\<^sub>-free P \ DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \\<^sub>\ P\ \<^vs>\-0.3cm\ \ +Definition*[X10]\ \deadlock\<^sub>-free P \ DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \\<^sub>\ P\ \<^vs>\-0.3cm\ \ text\\<^noindent> A process \P\ is deadlock-free if and only if after any trace \s\ without \\\, the union of \\\ and all events of \P\ can never be a refusal set associated to \s\, which means that \P\ cannot @@ -635,9 +639,9 @@ Theorem*[T2, short_name="''DF implies LF''"] \ \hspace{0.5cm} \deadlock_free P \ livelock_free P\ \<^vs>\-0.3cm\\ text\ -This is totally natural, at a first glance, but surprising as the proof of deadlock-freeness only requires -failure refinement \\\<^sub>\\ (see @{definition \X10\}) 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 \\\<^sub>\\ (see @{definition \X10\}) 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, diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 35f26df..62b1e84 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -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 diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 210bfb8..5955683 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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 diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 58e820a..27eba57 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -244,38 +244,79 @@ doc_class "math_example" = math_content + mcc :: "math_content_class" <= "expl" invariant d5 :: "\ \::math_example. mcc \ = expl" -subsection\Ontological Macros\ + +subsection\Ontological Macros \<^verbatim>\Definition*\ , \<^verbatim>\Lemma**\, \<^verbatim>\Theorem*\ ... \ + +text\These ontological macros allow notations are defined for the class + \<^typ>\math_content\ 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>\Definition*[l::"definition"]\...\\. + + Instead, the more convenient global declaration + \<^theory_text>\declare[[Definition_default_class="definition"]]\ + supports subsequent abbreviations: + + \<^theory_text>\Definition*[l]\...\\. +\ + +ML\ +val (Definition_default_class, Definition_default_class_setup) + = Attrib.config_string \<^binding>\Definition_default_class\ (K ""); +val (Lemma_default_class, Lemma_default_class_setup) + = Attrib.config_string \<^binding>\Lemma_default_class\ (K ""); +val (Theorem_default_class, Theorem_default_class_setup) + = Attrib.config_string \<^binding>\Theorem_default_class\ (K ""); + + +\ +setup\Definition_default_class_setup\ +setup\Lemma_default_class_setup\ +setup\Theorem_default_class_setup\ + ML\ 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 \ @@ -442,10 +483,6 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ; section\Miscelleous\ -ML\ -Parse.int -\ - subsection\Layout Trimming Commands\ setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (K(K())) \ setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (K(K())) \