diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 1d9da10..f3b5e92 100755 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -534,14 +534,14 @@ text\ text\Examples for declaration of typed doc-items "assumption" and "hypothesis", concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \ -text*[ass1::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ +text*[ass2::assumption, long_name="Some ''assumption one''"] \ The subsystem Y is safe. \ text*[hyp1::hypothesis] \ P not equal NP \ text\A real example fragment from a larger project, declaring a text-element as a "safety-related application condition", a concept defined in the @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\ -text*[hyp2::hypothesis]\Under the assumption @{assumption \ass1\} we establish the following: ... \ +text*[hyp2::hypothesis]\Under the assumption @{assumption \ass2\} we establish the following: ... \ text*[ass122::SRAC, long_name="Some ''ass122''"] \ The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index 47abf77..2cc4c55 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -19,17 +19,14 @@ begin open_monitor*[this::article] declare[[strict_monitor_checking=false]] -setup \ DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof" - #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}" - #> DOF_lib.define_shortcut \<^binding>\Protege\ "Prot{\\'e}g{\\'e}" - #> DOF_lib.define_shortcut \<^binding>\dots\ "\\ldots" - #> DOF_lib.define_shortcut \<^binding>\isabelle\ "Isabelle/HOL" - -\ +define_shortcut* isadof \ \\isadof\ + LaTeX \ \\LaTeX{}\ + dots \ \\ldots\ + isabelle \ \Isabelle/HOL\ + Protege \ \Prot{\'e}g{\'e}\ (* slanted text in contrast to italics *) -setup\ DOF_lib.define_macro \<^binding>\slanted_text\ "\\textsl{" "}" (K(K()))\ - +define_macro* slanted_text \ \\textsl{\ _ \}\ (*>*) diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index fe9d466..0e29455 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -1,27 +1,30 @@ (*<*) theory "paper" - imports - "Isabelle_DOF.scholarly_paper" + imports "Isabelle_DOF.scholarly_paper" begin open_monitor*[this::article] -declare[[strict_monitor_checking = false]] +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"\ +define_shortcut* csp \ \CSP\ + holcsp \ \HOL-CSP\ + isabelle \ \Isabelle/HOL\ (*>*) title*[tit::title]\Philosophers may Dine - Definitively!\ - + author*[safouan,email="\safouan.taha@lri.fr\",affiliation="\LRI, CentraleSupelec\"]\Safouan Taha\ author*[bu,email= "\wolff@lri.fr\",affiliation = "\LRI, Université Paris-Saclay\"]\Burkhart Wolff\ author*[lina,email="\lina.ye@lri.fr\",affiliation="\LRI, Inria, LSV, CentraleSupelec\"]\Lina Ye\ - + abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Algebra\, - \Concurrency\,\Computational Models\]"] + \Concurrency\,\Computational Models\]"] \ 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 @@ -60,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 \_\_\_\. \<^csp> semantics is described -by a fully abstract model of behaviour designed to be \<^emph>\compositional\: the denotational +with one single language primitive: synchronous communication written \_\_\_\. \<^csp> semantics is +described by a fully abstract model of behaviour designed to be \<^emph>\compositional\: the denotational semantics of a process \P\ encompasses all possible behaviours of this process in the context of all possible environments \P \S\ Env\ (where \S\ is the set of \atomic events\ both \P\ and \Env\ must synchronize). This design objective has the consequence that two kinds of choice have to @@ -156,7 +159,7 @@ Let two processes be defined as follows: \<^enum> \P\<^sub>n\<^sub>d\<^sub>e\<^sub>t = (a \ Stop) \ (b \ Stop)\ \ -text\\<^noindent> These two processes \P\<^sub>d\<^sub>e\<^sub>t\ and \P\<^sub>n\<^sub>d\<^sub>e\<^sub>t\ cannot be distinguished by using +text\These two processes \P\<^sub>d\<^sub>e\<^sub>t\ and \P\<^sub>n\<^sub>d\<^sub>e\<^sub>t\ cannot be distinguished by using the trace semantics: \\(P\<^sub>d\<^sub>e\<^sub>t) = \(P\<^sub>n\<^sub>d\<^sub>e\<^sub>t) = {[],[a],[b]}\. To resolve this problem, Brookes @{cite "BrookesHR84"} proposed the failures model, where communication traces were augmented with the constraint information for further communication that is represented negatively as a refusal set. @@ -181,7 +184,7 @@ many times. However, using the \<^csp> hiding operator \_\_\, this \ -text\\<^noindent> where \P\<^sub>i\<^sub>n\<^sub>f\ will be equivalent to \\\ in the process cpo ordering. +text\where \P\<^sub>i\<^sub>n\<^sub>f\ will be equivalent to \\\ in the process cpo ordering. To distinguish divergences from the deadlock process, Brookes and Roscoe proposed failure/divergence model to incorporate divergence traces @{cite "brookes-roscoe85"}. A divergence trace is the one leading to a possible divergent behavior. @@ -245,7 +248,7 @@ Second, in the traditional literature, the semantic domain is implicitly describ over the three semantic functions \\\, \\\ and \\\. 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 \front\<^sub>-tickFree\; \<^item> traces of a process are \<^emph>\prefix-closed\; \<^item> a process can refuse all subsets of a refusal set; @@ -256,8 +259,7 @@ Informally, these are: \<^item> a trace ending with \\\ belonging to divergence set implies that its maximum prefix without \\\ is also a divergent trace. - -\<^noindent> More formally, a process \P\ of the type \\ process\ should have the following properties: +More formally, a process \P\ of the type \\ process\ should have the following properties: @{cartouche [display] \([],{}) \ \ P \ @@ -270,9 +272,8 @@ Informally, these are: (\ s X. s \ \ P \ (s,X) \ \ P) \ (\ s. s@[\] \ \ P \ s \ \ P)\} - 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 \\ process\<^sub>0\ by \ \

(\\<^sup>\\<^sup>* \ \

(\\<^sup>\)) \ \

(\\<^sup>\)\. Forth, we turn our wishlist of "axioms" above into the definition of a predicate \is_process P\ of type \\ process\<^sub>0 \ bool\ deciding if its conditions are fulfilled. Since \P\ is a pre-process, @@ -281,7 +282,7 @@ And last not least fifth, we use the following type definition: \<^item> \<^theory_text>\typedef '\ process = "{P :: '\ process\<^sub>0 . is_process P}"\ -\<^noindent> Isabelle requires a proof for the existence of a witness for this set, +Isabelle requires a proof for the existence of a witness for this set, but this can be constructed in a straight-forward manner. Suitable definitions for \\\, \\\ and \\\ lifting \fst\ and \snd\ on the new \'\ process\-type allows to derive the above properties for any \P::'\ process\. \ @@ -298,11 +299,9 @@ This boils down to a proof that an equivalent definition on the pre-process type maintains \is_process\, \<^ie> this predicate remains invariant on the elements of the semantic domain. For example, we define \_\_\ on the pre-process type as follows: - \<^item> \<^theory_text>\definition "P \ Q \ Abs_process(\ P \ \ Q , \ P \ \ Q)"\ - -\<^noindent> where \\ = fst \ Rep_process\ and \\ = snd \ Rep_process\ and where \Rep_process\ and +where \\ = fst \ Rep_process\ and \\ = snd \ Rep_process\ and where \Rep_process\ and \Abs_process\ are the representation and abstraction morphisms resulting from the type definition linking \'\ process\ isomorphically to \'\ process\<^sub>0\. Proving the above properties for \\ (P \ Q)\ and \\ (P \ Q)\ requires a proof that \(\ P \ \ Q , \ P \ \ Q)\ @@ -360,7 +359,7 @@ We define \P \ Q \ \\<^sub>\ \ \\<^su \<^enum> \\\<^sub>\ = Mins(\ P) \ \ Q \ \ -text\\<^noindent> Note that the third condition \\\<^sub>\\ implies that the set of minimal divergent traces +text\The third condition \\\<^sub>\\ implies that the set of minimal divergent traces (ones with no proper prefix that is also a divergence) in \P\, denoted by \Mins(\ P)\, should be a subset of the trace set of \Q\. %One may note that each element in \Mins(\ P)\ do actually not contain the \\\, @@ -397,7 +396,7 @@ The port of HOL-CSP 2 on HOLCF implied that the derivation of the entire continu had to be completely re-done (3000 loc). -\<^noindent> HOL-CSP provides an important proof principle, the fixed-point induction: +HOL-CSP provides an important proof principle, the fixed-point induction: @{cartouche [display, indent=5] \cont f \ adm P \ P \ \ (\X. P X \ P(f X)) \ P(\X. f X)\} @@ -528,34 +527,34 @@ 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\ \ +text*[X32::"definition", mcc=defn]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ +Definition*[X42]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ +Definition*[X52::"definition"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ -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\ \ -Definition*[X3]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ +Definition*[X2]\\RUN A \ \ X. \ x \ A \ X\ \ +Definition*[X3]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ Definition*[X4]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\\ -Definition*[X5]\\DF A \ \ X. (\ x \ A \ X)\ \ -Definition*[X6]\\DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. ((\ x \ A \ X) \ SKIP)\ \ +Definition*[X5]\\DF A \ \ X. (\ x \ A \ X)\ \ +Definition*[X6]\\DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. ((\ x \ A \ X) \ SKIP)\ \ -text\ \<^noindent> -In the following, we denote \ \\

= {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\. +text\In the following, we denote \ \\

= {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\. All five reference processes are divergence-free. %which was done by using a particular lemma \\ (\ x. f x) = \\<^sub>i\<^sub>\\<^sub>\ \ (f\<^sup>i \)\. - - - @{cartouche [display,indent=8] \ D (\ UNIV) = {} where \ \ \\

and UNIV is the set of all events\} - - +@{cartouche + [display,indent=8] \ D (\ UNIV) = {} where \ \ \\

and UNIV is the set of all events\ +} Regarding the failure refinement ordering, the set of failures \\ P\ for any process \P\ is a subset of \\ (CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV)\.% and the following lemma was proved: -% This proof is performed by induction, based on the failure projection of \STOP\ and that of internal choice. +% This proof is performed by induction, based on the failure projection of \STOP\ and that of +% internal choice. @{cartouche [display, indent=25] \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \\<^sub>\ P\} @@ -615,8 +614,6 @@ be deadlocked after any non-terminating trace. Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] \ \hfill \break \deadlock_free P \ (\s\\ P. tickFree s \ (s, {\}\events_of P) \ \ P)\ \ - - Definition*[X11]\ \livelock\<^sub>-free P \ \ P = {} \ \ text\ Recall that all five reference processes are livelock-free. @@ -632,12 +629,12 @@ Finally, we proved the following theorem that confirms the relationship between properties: \ Theorem*[T2, short_name="''DF implies LF''"] - \ \hspace{0.5cm} \deadlock_free P \ livelock_free P\ \ + \ \deadlock_free P \ livelock_free P\ \ 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, @@ -695,13 +692,13 @@ refinement orderings. We state: @{theory_text [display,indent=5] \lemma: COPY \ SYSTEM\} -\<^noindent> and apply fixed-point induction over \COPY\; this leaves us to the three subgoals: +and apply fixed-point induction over \COPY\; this leaves us to the three subgoals: \<^enum> \adm (\a. a \ (SEND \SYN\ REC) \ SYN)\ \<^enum> \\ \ (SEND \SYN\ REC) \ SYN\ \<^enum> @{cartouche [display]\P \ (SEND \SYN\ REC) \ SYN \ left?x \ right!x \ P \ (SEND \SYN\ REC) \ SYN\} -\<^noindent> The first two sub-proofs are automatic simplification proofs; the third requires unfolding +The first two sub-proofs are automatic simplification proofs; the third requires unfolding \SEND\ and \REC\ one step and applying the algebraic laws. No denotational semantics reasoning is necessary here; it is just an induct-simplify proof consisting of 2 lines proof-script involving the derived algebraic laws of \<^csp>. diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index 4abb810..42848a2 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -16,24 +16,25 @@ theory "00_Frontmatter" imports "Isabelle_DOF.technical_report" begin -section\Document Local Setup.\ -text\Some internal setup, introducing document specific abbreviations and macros.\ -setup \DOF_lib.define_shortcut \<^binding>\dof\ "\\dof"\ -setup \DOF_lib.define_shortcut \<^binding>\isadof\ "\\isadof"\ -setup \ DOF_lib.define_shortcut \<^binding>\TeXLive\"\\TeXLive" - #> DOF_lib.define_shortcut \<^binding>\BibTeX\ "\\BibTeX{}" - #> DOF_lib.define_shortcut \<^binding>\LaTeX\ "\\LaTeX{}" - #> DOF_lib.define_shortcut \<^binding>\TeX\ "\\TeX{}" - #> DOF_lib.define_shortcut \<^binding>\pdf\ "PDF" - #> DOF_lib.define_shortcut \<^binding>\pdftex\ "\\pdftex{}" -\ +section\Local Document Setup.\ +text\... introducing document specific abbreviations and macros.\ -text\Note that these setups assume that the associated \<^LaTeX> macros are defined, \<^eg>, - in the document prelude. \ +define_shortcut* dof \ \\dof\ + isadof \ \\isadof\ -setup\ DOF_lib.define_macro \<^binding>\index\ "\\index{" "}" (K(K())) (*no checking, no reporting*) - #> DOF_lib.define_macro \<^binding>\bindex\ "\\bindex{" "}"(K(K()))\ +define_shortcut* TeXLive \ \\TeXLive\ + BibTeX \ \\BibTeX{}\ + LaTeX \ \\LaTeX{}\ + TeX \ \\TeX{}\ + pdf \ \PDF\ + pdftex \ \\pdftex{}\ + +text\Note that these setups assume that the associated \<^LaTeX> macros + are defined, \<^eg>, in the document prelude. \ + +define_macro* index \ \\index{\ _ \}\ +define_macro* bindex \ \\bindex{\ _ \}\ ML\ diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index f70dfe3..6805a41 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -16,6 +16,7 @@ theory "03_GuidedTour" imports "02_Background" + "Isabelle_DOF.technical_report" "Isabelle_DOF.CENELEC_50128" begin (*>*) @@ -424,6 +425,7 @@ doc_class "theorem" = math_content + mcc :: "math_content_class" <= "thm" ... \}\ + text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical "technical content" in mathematical or engineering papers: code, definitions, theorems, lemmas, examples. From this class, the more stricter class of @{typ \math_content\} is derived, diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index eada145..c089ee5 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -16,144 +16,84 @@ theory "04_RefMan" imports "03_GuidedTour" - "Isabelle_DOF.Isa_COL" + "Isabelle_DOF.technical_report" begin + +declare_reference*[infrastructure::technical] + (*>*) -chapter*[isadof_ontologies::technical]\Developing Ontologies\ +chapter*[isadof_ontologies::technical]\Ontologies and their Development\ text\ - In this chapter, we explain the concepts for modeling new ontologies, developing a document - representation for them, as well as developing new document templates. -\ + In this chapter, we explain the concepts of \<^isadof> in a more systematic way, and give + guidelines for modeling new ontologies, present underlying concepts for a mapping to a + representation, and give hints for the development of new document templates. -section*[infrastructure::technical]\Overview and Technical Infrastructure\ -text\ \<^isadof> is embedded in the underlying generic document model of Isabelle as described in \<^introduction>\dof\. Recall that the document language can be extended dynamically, \<^ie>, new \user-defined\ can be introduced at run-time. This is similar to the definition of new functions - in an interpreter. \<^isadof> as a system plugin is is a number of new command definitions in + in an interpreter. \<^isadof> as a system plugin provides a number of new command definitions in Isabelle's document model. - \<^isadof> consists consists basically of four components: - \<^item> an own \<^emph>\family of text-elements\ such as \<^boxed_theory_text>\title*\, \<^boxed_theory_text>\chapter*\ - \<^boxed_theory_text>\text*\, etc., which can be annotated with meta-information defined in the - underlying ontology definition and allow to build a \<^emph>\core\ document, - \<^item> the \<^emph>\ontology definition language\ (called ODL) which allow for the definitions - of document-classes and necessary auxiliary datatypes, + \<^isadof> consists consists basically of five components: + \<^item> the \<^emph>\DOF-core\ providing the \<^emph>\ontology definition language\ (called ODL) + which allow for the definitions of document-classes and necessary auxiliary datatypes, + \<^item> the \<^emph>\DOF-core\ also provides an own \<^emph>\family of commands\ such as + \<^boxed_theory_text>\text*\, \<^boxed_theory_text>\declare_reference*\, \<^etc>.; + They allow for the annotation of text-elements with meta-information defined in ODL, + \<^item> the \<^isadof> library of ontologies providing ontological concepts as well + as supporting infrastructure, \<^item> an infrastructure for ontology-specific \<^emph>\layout definitions\, exploiting this meta-information, and \<^item> an infrastructure for generic \<^emph>\layout definitions\ for documents following, \<^eg>, the format guidelines of publishers or standardization bodies. \ - -text\ - The list of fully supported (\<^ie>, supporting both interactive ontological modeling and - document generation) ontologies and the list of supported document templates can be - obtained by calling \inlinebash|isabelle mkroot_DOF -h| (see \<^technical>\first_project\). - Note that the postfix \inlinebash|-UNSUPPORTED| denotes experimental ontologies or templates - for which further manual setup steps might be required or that are not fully tested. Also note - that the \<^LaTeX>-class files required by the templates need to be already installed on your - system. This is mostly a problem for publisher specific templates (\<^eg>, Springer's - \<^path>\llncs.cls\), which cannot be re-distributed due to copyright restrictions. -\ - -subsection\Ontologies\ text\ - The document core \<^emph>\may\, but \<^emph>\must\ not use Isabelle definitions or proofs for checking the - formal content---this manual is actually an example of a document not containing any proof. - Consequently, the document editing and checking facility provided by \<^isadof> addresses the needs - of common users for an advanced text-editing environment, neither modeling nor proof knowledge is - inherently required. - - We expect authors of ontologies to have experience in the use of \<^isadof>, basic modeling (and, - potentially, some basic SML programming) experience, basic \<^LaTeX> knowledge, and, last but not - least, domain knowledge of the ontology to be modeled. Users with experience in UML-like - meta-modeling will feel familiar with most concepts; however, we expect no need for insight in - the Isabelle proof language, for example, or other more advanced concepts. - - Technically, ontologies\<^index>\ontology!directory structure\ are stored in a directory - \inlinebash|src/ontologies| and consist of a Isabelle theory file and a \<^LaTeX> -style file: + Similarly to Isabelle, which is based on a core logic \<^theory>\Pure\ and then extended by libraries + to major systems like \<^verbatim>\HOL\ or \<^verbatim>\FOL\, \<^isadof> has a generic core infrastructure \<^dof> and then + presents itself to users via major library extensions, which add domain-specific + system-extensions. Consequently, ontologies in \<^isadof> are not just a sequence of descriptions in + \<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated + sources that provide textual decriptions, abbreviations, macro-support and even ML-code. + Conceptually, the library of \<^isadof> is currently organized as follows + \<^footnote>\Note that the \<^emph>\technical\ organisation is slightly different and shown in + @{technical (unchecked) \infrastructure\}.\: +% \begin{center} \begin{minipage}{.9\textwidth} \dirtree{% -.1 . -.2 src. -.3 ontologies\DTcomment{Ontologies}. -.4 ontologies.thy\DTcomment{Ontology Registration}. -.4 CENELEC\_50128\DTcomment{CENELEC\_50128}. -.5 CENELEC\_50128.thy. -.5 DOF-CENELEC\_50128.sty. -.4 scholarly\_paper\DTcomment{scholarly\_paper}. -.5 scholarly\_paper.thy. -.5 DOF-scholarly\_paper.sty. +.1 COL\DTcomment{The Common Ontology Library}. +.2 scholarly\_paper\DTcomment{Scientific Papers}. +.3 technical\_report\DTcomment{Extended Papers}. +.4 CENELEC\_50128\DTcomment{Papers according to CENELEC\_50128}. +.4 CC\_v3\_1\_R5\DTcomment{Papers according to Common Criteria}. .4 \ldots. } \end{minipage} \end{center} -\ -text\ - Developing a new ontology ``\inlinebash|foo|'' requires, from a technical perspective, the - following steps: - \<^item> create a new sub-directory \inlinebash|foo| in the directory \inlinebash|src/ontologies| - \<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in - a new theory file \<^path>\src/ontologies/foo/foo.thy\. - \<^item> definition of the document representation for the ontological concepts in a \LaTeX-style - file \<^path>\src/ontologies/foo/DOF-foo.sty\ - \<^item> registration (as import) of the new ontology in the file. - \<^path>\src/ontologies/ontologies.thy\. - \<^item> activation of the new document setup by executing the install script. You can skip the lengthy - checks for the AFP entries and the installation of the Isabelle patch by using the - \inlinebash|--skip-patch-and-afp| option: - - \begin{bash} -ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp - \end{bash} -\ -subsection\Document Templates\ -text\ - Document-templates\<^index>\document template\ define the overall layout (page size, margins, fonts, - etc.) of the generated documents and are the the main technical means for implementing layout - requirements that are, \<^eg>, required by publishers or standardization bodies. Document-templates - are stored in a directory - \<^path>\src/document-templates\:\<^index>\document template!directory structure\ -\begin{center} -\begin{minipage}{.9\textwidth} -\dirtree{% -.1 . -.2 src. -.3 document-templates\DTcomment{Document templates}. -.4 root-lncs.tex. -.4 root-scrartcl.tex. -.4 root-scrreprt-modern.tex. -.4 root-scrreprt.tex. -} -\end{minipage} -\end{center} -\ + These libraries not only provide ontological concepts, but also syntactic sugar in Isabelle's + command language Isar that is of major importance for users (and may be felt as \<^isadof> key + features by many authors). In reality, + they are derived concepts from more generic ones; for example, the commands + \<^boxed_theory_text>\title*\, \<^boxed_theory_text>\section*\, \<^boxed_theory_text>\subsection*\, \<^etc>, + are in reality a kind of macros for \<^boxed_theory_text>\text*[

dentified @{docitem toe_def}\ -Definition* [slct_def::concept, tag="''selection''"] +Definition* [slct_def, tag="''selection''"] \specification of one or more items from a list in a component\ -Definition* [smfrml_def::concept, tag="''semiformal''"] +Definition* [smfrml_def, tag="''semiformal''"] \expressed in a restricted syntax language with defined semantics\ -Definition* [spcfy_def::concept, tag= "''specify''"] +Definition* [spcfy_def, tag= "''specify''"] \provide specific details about an entity in a rigorous and precise manner\ -Definition* [strct_conf_def::concept, tag="''strict conformance''"] +Definition* [strct_conf_def, tag="''strict conformance''"] \hierarchical relationship between a PP and an ST where all the requirements in the PP also exist in the ST @@ -344,36 +347,36 @@ Definition* [strct_conf_def::concept, tag="''strict conformance''"] be used for stringent requirements that are to be adhered to in a single manner. \ -Definition* [st_eval_def::concept, tag="''ST evaluation''"] +Definition* [st_eval_def, tag="''ST evaluation''"] \assessment of an ST against defined criteria\ -Definition* [subj_def::concept, tag="''subject''"] +Definition* [subj_def, tag="''subject''"] \active entity in the TOE that performs operations on objects\ -Definition* [toe::concept, tag= "''target of evaluation''"] +Definition* [toe, tag= "''target of evaluation''"] \set of software, firmware and/or hardware possibly accompanied by guidance\ -Definition* [thrt_agnt_def::concept, tag="''threat agent''"] +Definition* [thrt_agnt_def, tag="''threat agent''"] \entity that can adversely act on assets\ -Definition* [toe_eval_def::concept, tag="''TOE evaluation''"] +Definition* [toe_eval_def, tag="''TOE evaluation''"] \assessment of a TOE against defined criteria\ -Definition* [toe_res_def::concept, tag="''TOE resource''"] +Definition* [toe_res_def, tag="''TOE resource''"] \anything useable or consumable in the TOE\ -Definition* [toe_sf_def::concept, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"] +Definition* [toe_sf_def, tag="''TOE security functionality''", short_tag= "Some(''TSF'')"] \combined functionality of all hardware, software, and firmware of a TOE that must be relied upon for the correct enforcement of the @{docitem sfr_def}s\ -Definition* [tr_vrb_def::concept, tag="''trace, verb''"] +Definition* [tr_vrb_def, tag="''trace, verb''"] \perform an informal correspondence analysis between two entities with only a minimal level of rigour\ -Definition* [trnsfs_out_toe_def::concept, tag="''transfers outside of the TOE''"] +Definition* [trnsfs_out_toe_def, tag="''transfers outside of the TOE''"] \TSF mediated communication of data to entities not under the control of the TSF\ -Definition* [transl_def::concept, tag= "''translation''"] +Definition* [transl_def, tag= "''translation''"] \ describes the process of describing security requirements in a standardised language. @@ -381,45 +384,45 @@ use of the term translation in this context is not literal and does not imply that every SFR expressed in standardised language can also be translated back to the security objectives.\ -Definition* [trst_chan_def::concept, tag="''trusted channel''"] +Definition* [trst_chan_def, tag="''trusted channel''"] \a means by which a TSF and another trusted IT product can communicate with necessary confidence\ -Definition* [trst_it_prod_def::concept, tag="''trusted IT product''"] +Definition* [trst_it_prod_def, tag="''trusted IT product''"] \IT product, other than the TOE, which has its security functional requirements administratively coordinated with the TOE and which is assumed to enforce its security functional requirements correctly An example of a trusted IT product would be one that has been separately evaluated.\ -Definition* [trst_path_def::concept, tag="''trusted path''"] +Definition* [trst_path_def, tag="''trusted path''"] \means by which a user and a TSF can communicate with the necessary confidence\ -Definition* [tsf_data_def::concept, tag="''TSF data''"] +Definition* [tsf_data_def, tag="''TSF data''"] \data for the operation of the TOE upon which the enforcement of the SFR relies\ -Definition* [tsf_intrfc_def::concept, tag="''TSF interface''"] +Definition* [tsf_intrfc_def, tag="''TSF interface''"] \means by which external entities (or subjects in the TOE but outside of the TSF) supply data to the TSF, receive data from the TSF and invoke services from the TSF\ -Definition* [usr_def::concept, tag="''user''"] \see external entity\ +Definition* [usr_def, tag="''user''"] \see external entity\ -Definition* [usr_datat_def::concept, tag="''user data''"] +Definition* [usr_datat_def, tag="''user data''"] \data for the user, that does not affect the operation of the TSF\ -Definition* [vrfy_def::concept, tag="''verify''"] +Definition* [vrfy_def, tag="''verify''"] \rigorously review in detail with an independent determination of sufficiency Also see “confirm”. This term has more rigorous connotations. The term “verify” is used in the context of evaluator actions where an independent effort is required of the evaluator.\ -Definition* [dev_def::concept, tag="''Developer''"] +Definition* [dev_def, tag="''Developer''"] \who respond to actual or perceived consumer security requirements in constructing a @{docitem toe_def}, reference this CC_Part_3 when interpreting statements of assurance requirements and determining assurance approaches of @{docitem toe}s.\ -Definition*[evalu_def::concept, tag="'' Evaluator''"] +Definition*[evalu_def, tag="'' Evaluator''"] \who use the assurance requirements defined in CC_Part_3 as mandatory statement of evaluation criteria when determining the assurance of @{docitem toe_def}s and when evaluating @{docitem pp_def}s and @{docitem st_def}s.\ diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index c31eafe..f4496ba 100755 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -28,8 +28,20 @@ theory CENELEC_50128 imports "../technical_report/technical_report" begin +(* this is a hack and should go into an own ontology, providing thingsd like: + - Assumption* + - Hypothesis* + - Definition*. (Une redefinition de ce qui se passe dans tech-report, cible a semi-formal + “Definitions of terminology” \ ) + - Objective" + - Claim* + - Requirement* + +*) + + text\We re-use the class @\typ math_content\, which provides also a framework for -semi-formal terminology, which we re-use by this definition.\ +semi-formal "math-alike" terminology, which we re-use by this definition.\ doc_class semi_formal_content = math_content + status :: status <= "semiformal" @@ -39,27 +51,29 @@ type_synonym sfc = semi_formal_content (*>>*) +declare[[ Definition_default_class="semi_formal_content"]] + + text\ Excerpt of the BE EN 50128:2011, page 22. \ section\Terms and Definitions\ -typ "sfc" -Definition*[assessment::sfc,short_name="''assessment''"] +Definition*[assessment,short_name="''assessment''"] \process of analysis to determine whether software, which may include process, documentation, system, subsystem hardware and/or software components, meets the specified requirements and to form a judgement as to whether the software is fit for its intended purpose. Safety assessment is focused on but not limited to the safety properties of a system.\ -Definition*[assessor::sfc, short_name="''assessor''"] +Definition*[assessor, short_name="''assessor''"] \entity that carries out an assessment\ -Definition*[COTS::sfc, short_name="''commercial off-the-shelf software''"] +Definition*[COTS, short_name="''commercial off-the-shelf software''"] \software defined by market-driven need, commercially available and whose fitness for purpose has been demonstrated by a broad spectrum of commercial users\ -Definition*[component::sfc] +Definition*[component] \a constituent part of software which has well-defined interfaces and behaviour with respect to the software architecture and design and fulfils the following criteria: @@ -71,53 +85,53 @@ criteria: \ typ "sfc" -Definition*[CMGR::sfc, short_name="''configuration manager''"] +Definition*[CMGR, short_name="''configuration manager''"] \entity that is responsible for implementing and carrying out the processes for the configuration management of documents, software and related tools including \<^emph>\change management\\ -Definition*[customer::sfc] +Definition*[customer] \entity which purchases a railway control and protection system including the software\ -Definition*[designer::sfc] +Definition*[designer] \entity that analyses and transforms specified requirements into acceptable design solutions which have the required safety integrity level\ -Definition*[entity::sfc] +Definition*[entity] \person, group or organisation who fulfils a role as defined in this European Standard\ -declare_reference*[fault::sfc] -Definition*[error::sfc] +declare_reference*[fault] +Definition*[error] \defect, mistake or inaccuracy which could result in failure or in a deviation from the intended performance or behaviour (cf. @{semi_formal_content (unchecked) \fault\}))\ -Definition*[fault::sfc] +Definition*[fault] \defect, mistake or inaccuracy which could result in failure or in a deviation from the intended performance or behaviour (cf @{semi_formal_content \error\})\ -Definition*[failure::sfc] +Definition*[failure] \unacceptable difference between required and observed performance\ -Definition*[FT::sfc, short_name="''fault tolerance''"] +Definition*[FT, short_name="''fault tolerance''"] \built-in capability of a system to provide continued correct provision of service as specified, in the presence of a limited number of hardware or software faults\ -Definition*[firmware::sfc] +Definition*[firmware] \software stored in read-only memory or in semi-permanent storage such as flash memory, in a way that is functionally independent of applicative software\ -Definition*[GS::sfc,short_name="''generic software''"] +Definition*[GS,short_name="''generic software''"] \software which can be used for a variety of installations purely by the provision of application-specific data and/or algorithms\ -Definition*[implementer::sfc] +Definition*[implementer] \entity that transforms specified designs into their physical realisation\ -Definition*[integration::sfc] +Definition*[integration] \process of assembling software and/or hardware items, according to the architectural and design specification, and testing the integrated unit\ -Definition*[integrator::sfc] +Definition*[integrator] \entity that carries out software integration\ Definition*[PES :: sfc, short_name="''pre-existing software''"] @@ -127,52 +141,52 @@ off-the shelf) and open source software\ Definition*[OSS :: sfc, short_name="''open source software''"] \source code available to the general public with relaxed or non-existent copyright restrictions\ -Definition*[PLC::sfc, short_name="''programmable logic controller''"] +Definition*[PLC, short_name="''programmable logic controller''"] \solid-state control system which has a user programmable memory for storage of instructions to implement specific functions\ -Definition*[PM::sfc, short_name="''project management''"] +Definition*[PM, short_name="''project management''"] \administrative and/or technical conduct of a project, including safety aspects\ -Definition*[PGMGR::sfc, short_name="''project manager''"] +Definition*[PGMGR, short_name="''project manager''"] \entity that carries out project management\ -Definition*[reliability::sfc] +Definition*[reliability] \ability of an item to perform a required function under given conditions for a given period of time\ -Definition*[robustness::sfc] +Definition*[robustness] \ability of an item to detect and handle abnormal situations\ -Definition*[RMGR::sfc, short_name="''requirements manager''"] +Definition*[RMGR, short_name="''requirements manager''"] \entity that carries out requirements management\ -Definition*[RMGMT::sfc, short_name="''requirements management''"] +Definition*[RMGMT, short_name="''requirements management''"] \the process of eliciting, documenting, analysing, prioritising and agreeing on requirements and then controlling change and communicating to relevant stakeholders. It is a continuous process throughout a project\ -Definition*[risk::sfc] +Definition*[risk] \combination of the rate of occurrence of accidents and incidents resulting in harm (caused by a hazard) and the degree of severity of that harm\ -Definition*[safety::sfc] +Definition*[safety] \freedom from unacceptable levels of risk of harm to people\ -Definition*[SA::sfc, short_name="''safety authority''"] +Definition*[SA, short_name="''safety authority''"] \body responsible for certifying that safety related software or services comply with relevant statutory safety requirements\ -Definition*[SF::sfc, short_name="''safety function''"] +Definition*[SF, short_name="''safety function''"] \a function that implements a part or whole of a safety requirement\ -Definition*[SFRS::sfc, short_name= "''safety-related software''"] +Definition*[SFRS, short_name= "''safety-related software''"] \software which performs safety functions\ -Definition*[software::sfc] +Definition*[software] \intellectual creation comprising the programs, procedures, rules, data and any associated documentation pertaining to the operation of a system\ -Definition*[SB::sfc, short_name="''software baseline''"] +Definition*[SB, short_name="''software baseline''"] \complete and consistent set of source code, executable files, configuration files, installation scripts and documentation that are needed for a software release. Information about compilers, operating systems, preexisting software and dependent tools is stored as part of the @@ -183,7 +197,7 @@ released and assessed -Definition*[SWLC::sfc, short_name="''software life-cycle''"] +Definition*[SWLC, short_name="''software life-cycle''"] \those activities occurring during a period of time that starts when software is conceived and ends when the software is no longer available for use. The software life cycle typically includes a requirements phase, design phase,test phase, integration phase, @@ -191,35 +205,35 @@ deployment phase and a maintenance phase 3.1.35 software maintainability capability of the software to be modified; to correct faults, improve to a different environment \ -Definition*[SM::sfc, short_name="''software maintenance''"] +Definition*[SM, short_name="''software maintenance''"] \ action, or set of actions, carried out on software after deployment functionality performance or other attributes, or adapt it with the aim of enhancing or correcting its\ -Definition*[SOSIL::sfc, short_name="''software safety integrity level''"] +Definition*[SOSIL, short_name="''software safety integrity level''"] \classification number which determines the techniques and measures that have to be applied to software NOTE Safety-related software has been classified into five safety integrity levels, where 0 is the lowest and 4 the highest.\ -Definition*[supplier::sfc] +Definition*[supplier] \entity that designs and builds a railway control and protection system including the software or parts thereof\ -Definition*[SYSIL::sfc, short_name="''system safety integrity level''"] +Definition*[SYSIL, short_name="''system safety integrity level''"] \classification number which indicates the required degree of confidence that an integrated system comprising hardware and software will meet its specified safety requirements\ -Definition*[tester::sfc]\an entity that carries out testing\ +Definition*[tester]\an entity that carries out testing\ -Definition*[testing::sfc] +Definition*[testing] \process of executing software under controlled conditions as to ascertain its behaviour and performance compared to the corresponding requirements specification\ -Definition*[TCT1::sfc, short_name="''tool class T1''"] +Definition*[TCT1, short_name="''tool class T1''"] \generates no outputs which can directly or indirectly contribute to the executable code (including data) of the software NOTE 11 examples include: a text editor or a requirement or design support tool with no automatic code generation capabilities; configuration control tools.\ -Definition*[TCT2::sfc,short_name="''tool class T2''"] +Definition*[TCT2,short_name="''tool class T2''"] \supports the test or verification of the design or executable code, where errors in the tool can fail to reveal defects but cannot directly create errors in the executable software NOTE T2 examples include: a test harness generator; a test coverage measurement tool; a static @@ -227,35 +241,35 @@ analysis tool. reproduce defined versions and be the input for future releases a at upgrade in the maintenance phase \ -Definition*[TCT3::sfc, short_name="''tool class T3''"] +Definition*[TCT3, short_name="''tool class T3''"] \generates outputs which can directly or indirectly contribute to the executable code (including data) of the safety related system NOTE T3 examples include: a source code compiler, a data/algorithms compiler, a tool to change set-points during system operation; an optimising compiler where the relationship between the source code program and the generated object code is not obvious; a compiler that incorporates an executable run-time package into the executable code. \ -Definition*[traceability::sfc, short_name="''traceability''"] +Definition*[traceability, short_name="''traceability''"] \degree to which relationship can be established between two or more products of a development process, especially those having a predecessor/successor or master/subordinate relationship to one another\ -Definition*[validation::sfc, short_name="''validation''"] +Definition*[validation, short_name="''validation''"] \process of analysis followed by a judgment based on evidence to documentation, software or application) fits the user needs,in particular with respect to safety and quality and determine whether an item (e.g. process, with emphasis on the suitability of its operation in accordance to its purpose in its intended environment\ -Definition*[validator::sfc, short_name="''validator''"] +Definition*[validator, short_name="''validator''"] \entity that is responsible for the validation\ -Definition*[verification::sfc, short_name="''verification''"] +Definition*[verification, short_name="''verification''"] \process of examination followed by a judgment based on evidence that output items (process, documentation, software or application) of a specific development phase fulfils the requirements of that phase with respect to completeness, correctness and consistency. NOTE Verification is mostly based on document reviews (design, implementation, test documents etc.). \ -Definition*[verifier::sfc, short_name="''verifier''"] +Definition*[verifier, short_name="''verifier''"] \entity that is responsible for one or more verification activities\ diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index b02be6b..135a891 100755 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -49,7 +49,7 @@ doc_class E = D + -doc_class F = +doc_class F = properties :: "term list" r :: "thm list" u :: "file" @@ -62,7 +62,7 @@ doc_class F = doc_class G = C + - g :: "thm" <= "@{thm ''HOL.refl''}" + g :: "thm" <= "@{thm \HOL.refl\}" doc_class M = trace :: "(A + C + D + F) list" @@ -79,8 +79,8 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl section*[test::A]\Test and Validation\ text\Defining some document elements to be referenced in later on in another theory: \ text*[sdf]\ Lorem ipsum @{thm refl}\ -text*[ sdfg] \ Lorem ipsum @{thm refl}\ -text*[ xxxy ] \ Lorem ipsum @{docitem \sdfg\} rate @{thm refl}\ +text*[ sdfg :: F] \ Lorem ipsum @{thm refl}\ +text*[ xxxy ] \ Lorem ipsum @{F \sdfg\} rate @{thm refl}\ end diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 58e820a..daa7d55 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -11,12 +11,13 @@ * SPDX-License-Identifier: BSD-2-Clause *************************************************************************) -section\An example ontology for a scholarly paper\ +section\An example ontology for scientific, MINT-oriented papers.\ theory scholarly_paper imports "../../DOF/Isa_COL" keywords "author*" "abstract*" "Definition*" "Lemma*" "Theorem*" :: document_body + and "assert*" :: thy_decl begin @@ -123,7 +124,7 @@ A formal statement can, but must not have a reference to true formal Isabelle/Is subsection\Technical Content and its Formats\ -datatype status = semiformal | description +datatype status = formal | semiformal | description text\The class \<^verbatim>\technical\ regroups a number of text-elements that contain typical "technical content" in mathematical or engineering papers: definitions, theorems, lemmas, examples. \ @@ -154,7 +155,7 @@ doc_class example = text_section + short_name :: string <= "''''" -subsection\Mathematical Content\ +subsection\Freeform Mathematical Content\ text\We follow in our enumeration referentiable mathematical content class the AMS style and its provided \<^emph>\theorem environments\ (see \<^verbatim>\texdoc amslatex\). We add, however, the concepts @@ -189,8 +190,21 @@ doc_class math_content = tc + invariant s2 :: "\ \::math_content. status \ = semiformal" type_synonym math_tc = math_content +text\The class \<^typ>\math_content\ is perhaps more adequaltely described as "math-alike content". +Sub-classes can englobe instances such as: +\<^item> terminological definitions such as: + \Definition*[assessor::sfc, short_name="''assessor''"]\entity that carries out an assessment\\ +\<^item> free-form mathematical definitions such as: + \Definition*[process_ordering, short_name="''process ordering''"]\ + We define \P \ Q \ \\<^sub>\ \ \\<^sub>\ \ \\<^sub>\ \, where \<^vs>\-0.2cm\ + 1) \<^vs>\-0.2cm\ \\\<^sub>\ = \ P \ \ Q \ + 2) ... + \\ +\<^item> semi-formal descriptions, which are free-form mathematical definitions on which finally + an attribute with a formal Isabelle definition is attached. + +\ -find_theorems name:"s1" name:"scholarly" (* type qualification is a work around *) @@ -244,42 +258,139 @@ doc_class "math_example" = math_content + mcc :: "math_content_class" <= "expl" invariant d5 :: "\ \::math_example. mcc \ = expl" -subsection\Ontological Macros\ + +subsubsection\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 \ + +subsection\Formal Mathematical Content\ +text\While this library is intended to give a lot of space to freeform text elements in +order to counterbalance Isabelle's standard view, it should not be forgot that the real strength +of Isabelle is its ability to handle both - and to establish links between both worlds. Therefore:\ + +doc_class math_formal = math_content + + referentiable :: bool <= False + status :: status <= "formal" + properties :: "term list" +type_synonym math_fc = math_formal + +doc_class assertion = math_formal + + referentiable :: bool <= True (* No support in Backend yet. *) + status :: status <= "formal" + properties :: "term list" + + +ML\ +(* TODO : Rework this code and make it closer to Definition*. There is still + a rest of "abstract classes in it: any class possessing a properties attribute + is admissible to this command, not just ... *) +local open ODL_Command_Parser in + +fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), + prop) = + let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy)) + fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]") + ::doc_attrs + fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy) + fun mks thy = case DOF_core.get_object_global_opt oid thy of + SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) + | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) + | NONE => (create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos cid_pos (conv_attrs thy) thy) + val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global + in + (* Toplevel.keep (check o Toplevel.context_of) *) + Toplevel.theory (fn thy => (check thy; mks thy)) + end + +val attributes = attributes (* re-export *) + +end +val _ = + Outer_Syntax.command @{command_keyword "assert*"} + "evaluate and print term" + (attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd'); + +\ + +subsubsection*[ex_ass::example]\Example\ +text\Assertions allow for logical statements to be checked in the global context). \ +assert*[ass1::assertion, short_name = "\This is an assertion\"] \(3::int) < 4\ + subsection\Example Statements\ text\ \<^verbatim>\examples\ are currently considered \<^verbatim>\technical\. Is a main category to be refined @@ -293,7 +404,8 @@ doc_class tech_example = technical + subsection\Content in Engineering/Tech Papers \ - +text\This section is currently experimental and not supported by the documentation + generation backend.\ doc_class engineering_content = tc + short_name :: string <= "''''" @@ -415,52 +527,60 @@ setup\ let val cidS = ["scholarly_paper.introduction","scholarly_paper.tec true) in DOF_core.update_class_invariant "scholarly_paper.article" body end\ - -(* some test code *) -ML\ -(* - -val trace = AttributeAccess.compute_trace_ML (Context.Proof @{context}) "this" @{here} @{here} -val groups = partition ( @{context}) cidS trace -val _::_::_::_:: _ ::_ ::_ ::a::_ = groups; -check; - -fun get_level_raw oid = AttributeAccess.compute_attr_access (Context.Proof @{context}) "level" oid @{here} @{here}; -fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid)); -fun check_level_hd a = case (get_level (snd a)) of - NONE => error("Invariant violation: leading section" ^ snd a ^ - " must have lowest level") - | SOME X => X -fun check_group_elem level_hd a = case (get_level (snd a)) of - NONE => true - | SOME y => if y > level_hd then true - else error("Invariant violation: subsequent section " ^ snd a ^ - " must have higher level."); -fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ; -*) -\ +ML\ \ 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())) \ -setup\ DOF_lib.define_shortcut \<^binding>\clearpage\ "\\clearpage{}" \ - - subsection\Common Abbreviations\ -setup \ DOF_lib.define_shortcut \<^binding>\eg\ "\\eg" - (* Latin: „exempli gratia“ meaning „for example“. *) - #> DOF_lib.define_shortcut \<^binding>\ie\ "\\ie" - (* Latin: „id est“ meaning „that is to say“. *) - #> DOF_lib.define_shortcut \<^binding>\etc\ "\\etc"\ - - (* this is an alternative style for macro definitions equivalent to setup ... setup ...*) +define_shortcut* eg \ \\eg\ (* Latin: „exempli gratia“ meaning „for example“. *) + ie \ \\ie\ (* Latin: „id est“ meaning „that is to say“. *) + etc \ \\etc\ (* Latin : „et cetera“ meaning „et cetera“ *) + +subsection\Layout Trimming Commands (with syntactic checks)\ + +ML\ +local + +val scan_cm = Scan.ahead (Basic_Symbol_Pos.$$$ "c" |-- Basic_Symbol_Pos.$$$ "m" ) ; +val scan_pt = Scan.ahead (Basic_Symbol_Pos.$$$ "p" |-- Basic_Symbol_Pos.$$$ "t" ) ; +val scan_blank = Scan.repeat ( Basic_Symbol_Pos.$$$ " " + || Basic_Symbol_Pos.$$$ "\t" + || Basic_Symbol_Pos.$$$ "\n"); + +val scan_latex_measure = (scan_blank + |-- Scan.option (Basic_Symbol_Pos.$$$ "-") + |-- Symbol_Pos.scan_nat + |-- (Scan.option ((Basic_Symbol_Pos.$$$ ".") |-- Symbol_Pos.scan_nat)) + |-- scan_blank + |-- (scan_cm || scan_pt) + |-- scan_blank + ); +in + +fun check_latex_measure _ src = + let val _ = ((Scan.catch scan_latex_measure (Symbol_Pos.explode(Input.source_content src))) + handle Fail _ => error ("syntax error in LaTeX measure") ) + in () end +end\ + + + +setup\ DOF_lib.define_macro \<^binding>\vs\ "\\vspace{" "}" (check_latex_measure) \ +setup\ DOF_lib.define_macro \<^binding>\hs\ "\\hspace{" "}" (check_latex_measure) \ + +(*<*) + +text\Tests: \<^vs>\-0.14cm\\ +ML\ check_latex_measure @{context} (Input.string "-3.14 cm") \ +define_macro* vs2 \ \\vspace{\ _ \}\ (check_latex_measure) (* checkers NYI on Isar-level *) +define_macro* hs2 \ \\hspace{\ _ \}\ (* works fine without checker.*) + +(*>*) + +define_shortcut* clearpage \ \\clearpage{}\ + hf \ \\hfill\ + br \ \\break\ end diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy index 014235b..731d48b 100755 --- a/src/ontologies/technical_report/technical_report.thy +++ b/src/ontologies/technical_report/technical_report.thy @@ -35,7 +35,7 @@ doc_class index = section\Code Statement Elements\ doc_class "code" = technical + - checked :: bool <= "False" + checked :: bool <= "False" caption :: "string" <= "''''" @@ -79,251 +79,3 @@ doc_class report = end - -(* -===================================== -docclass: Isa_COL.thms - name: "thms" - origin: Isa_COL - attrs: "properties" - invs: -docclass: Isa_COL.figure - name: "figure" - origin: Isa_COL - attrs: "relative_width", "src", "placement", "spawn_columns"(True) - invs: -docclass: Isa_COL.chapter = Isa_COL.text_element + - name: "chapter" - origin: Isa_COL - attrs: "level"(Some 0) - invs: -docclass: Isa_COL.concept - name: "concept" - origin: Isa_COL - attrs: "tag"([]), "properties"([]) - invs: -docclass: Isa_COL.section = Isa_COL.text_element + - name: "section" - origin: Isa_COL - attrs: "level"(Some 1) - invs: -docclass: Isa_COL.assertions - name: "assertions" - origin: Isa_COL - attrs: "properties" - invs: -docclass: Isa_COL.subsection = Isa_COL.text_element + - name: "subsection" - origin: Isa_COL - attrs: "level"(Some 2) - invs: -docclass: Isa_COL.definitions - name: "definitions" - origin: Isa_COL - attrs: "requires", "establishes" - invs: -docclass: Isa_COL.formal_item - name: "formal_item" - origin: Isa_COL - attrs: "item" - invs: -docclass: Isa_COL.figure_group - name: "figure_group" - origin: Isa_COL - attrs: "trace"([]), "caption" - invs: -docclass: Isa_COL.text_element - name: "text_element" - origin: Isa_COL - attrs: "level"(None), "referentiable"(False), "variants"({STR ''outline'', STR ''document''}) - invs: -docclass: scholarly_paper.data = scholarly_paper.engineering_content + - name: "data" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: technical_report.SML = technical_report.code + - name: "SML" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: Isa_COL.subsubsection = Isa_COL.text_element + - name: "subsubsection" - origin: Isa_COL - attrs: "level"(Some 3) - invs: -docclass: scholarly_paper.annex = scholarly_paper.text_section + - name: "annex" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.lemma = scholarly_paper.math_content + - name: "lemma" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(lem) - invs: d3::\\. lemma.mcc \ = lem -docclass: scholarly_paper.title - name: "title" - origin: scholarly_paper - attrs: "short_title"(None) - invs: -docclass: technical_report.ISAR = technical_report.code + - name: "ISAR" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: technical_report.code = scholarly_paper.technical + - name: "code" - origin: technical_report - attrs: "checked"(False), "label"([]) - invs: -docclass: Isa_COL.formal_content - name: "formal_content" - origin: Isa_COL - attrs: "trace"([]), "style" - invs: -docclass: scholarly_paper.author - name: "author" - origin: scholarly_paper - attrs: "email"([]), "http_site"([]), "orcid"([]), "affiliation" - invs: -docclass: technical_report.LATEX = technical_report.code + - name: "LATEX" - origin: technical_report - attrs: "checked"(False) - invs: -docclass: technical_report.index - name: "index" - origin: technical_report - attrs: "kind", "level" - invs: -docclass: scholarly_paper.article - name: "article" - origin: scholarly_paper - attrs: "trace"([]), "style_id"(''LNCS''), "version"((0, 0, 0)) - invs: -docclass: scholarly_paper.example = scholarly_paper.text_section + - name: "example" - origin: scholarly_paper - attrs: "referentiable"(True), "status"(description), "short_name"([]) - invs: -docclass: scholarly_paper.theorem = scholarly_paper.math_content + - name: "theorem" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(thm) - invs: d2::\\. theorem.mcc \ = thm -docclass: scholarly_paper.abstract - name: "abstract" - origin: scholarly_paper - attrs: "keywordlist"([]), "principal_theorems" - invs: -docclass: scholarly_paper.subtitle - name: "subtitle" - origin: scholarly_paper - attrs: "abbrev"(None) - invs: -docclass: scholarly_paper.corollary = scholarly_paper.math_content + - name: "corollary" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(cor) - invs: d4::\\. corollary.mcc \ = thm -docclass: scholarly_paper.technical = scholarly_paper.text_section + - name: "technical" - origin: scholarly_paper - attrs: "definition_list"([]), "status"(description), "formal_results" - invs: L1::\\. 0 < the (text_section.level \) -docclass: scholarly_paper.conclusion = scholarly_paper.text_section + - name: "conclusion" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.definition = scholarly_paper.math_content + - name: "definition" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(defn) - invs: d1::\\. definition.mcc \ = defn -docclass: scholarly_paper.evaluation = scholarly_paper.engineering_content + - name: "evaluation" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: scholarly_paper.experiment = scholarly_paper.engineering_content + - name: "experiment" - origin: scholarly_paper - attrs: "tag"([]) - invs: -docclass: Isa_COL.side_by_side_figure = Isa_COL.figure + - name: "side_by_side_figure" - origin: Isa_COL - attrs: "anchor", "caption", "relative_width2", "src2", "anchor2", "caption2" - invs: -docclass: scholarly_paper.bibliography = scholarly_paper.text_section + - name: "bibliography" - origin: scholarly_paper - attrs: "style"(Some ''LNCS'') - invs: -docclass: scholarly_paper.introduction = scholarly_paper.text_section + - name: "introduction" - origin: scholarly_paper - attrs: "comment", "claims" - invs: -docclass: scholarly_paper.math_content = scholarly_paper.technical + - name: "math_content" - origin: scholarly_paper - attrs: "referentiable"(True), "short_name"([]), "status"(semiformal), "mcc"(thm) - invs: s1::\\. \ math_content.referentiable \ \ - math_content.short_name \ = [], s2::\\. math_content.status \ = semiformal -docclass: scholarly_paper.math_example = scholarly_paper.math_content + - name: "math_example" - origin: scholarly_paper - attrs: "referentiable"(True), "mcc"(expl) - invs: d5::\\. math_example.mcc \ = expl -docclass: scholarly_paper.related_work = scholarly_paper.conclusion + - name: "related_work" - origin: scholarly_paper - attrs: "main_author"(None) - invs: -docclass: scholarly_paper.tech_example = scholarly_paper.technical + - name: "tech_example" - origin: scholarly_paper - attrs: "referentiable"(True), "tag"([]) - invs: -docclass: scholarly_paper.text_section = Isa_COL.text_element + - name: "text_section" - origin: scholarly_paper - attrs: "main_author"(None), "fixme_list"([]), "level"(None) - invs: -docclass: technical_report.front_matter - name: "front_matter" - origin: technical_report - attrs: "front_matter_style" - invs: -docclass: scholarly_paper.math_motivation = scholarly_paper.technical + - name: "math_motivation" - origin: scholarly_paper - attrs: "referentiable"(False) - invs: -docclass: scholarly_paper.math_semiformal = scholarly_paper.math_content + - name: "math_semiformal" - origin: scholarly_paper - attrs: "referentiable"(True) - invs: -docclass: scholarly_paper.math_explanation = scholarly_paper.technical + - name: "math_explanation" - origin: scholarly_paper - attrs: "referentiable"(False) - invs: -docclass: technical_report.table_of_contents - name: "table_of_contents" - origin: technical_report - attrs: "bookmark_depth"(3), "depth"(3) - invs: -docclass: scholarly_paper.engineering_content = scholarly_paper.technical + - name: "engineering_content" - origin: scholarly_paper - attrs: "short_name"([]), "status" - invs: -===================================== - - -*) diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy index ab71072..064c8af 100755 --- a/src/tests/AssnsLemmaThmEtc.thy +++ b/src/tests/AssnsLemmaThmEtc.thy @@ -16,6 +16,7 @@ theory imports "Isabelle_DOF.Conceptual" "Isabelle_DOF.math_paper" + "Isabelle_DOF.scholarly_paper" (* for assert notation *) begin section\Elementary Creation of Doc-items and Access of their Attibutes\ diff --git a/src/tests/ROOT b/src/tests/ROOT index f429670..759e0bd 100755 --- a/src/tests/ROOT +++ b/src/tests/ROOT @@ -4,5 +4,5 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" + "AssnsLemmaThmEtc" "Concept_ExampleInvariant" "Concept_Example" - "InnerSyntaxAntiquotations" + "TermAntiquotations" "Attributes" diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/TermAntiquotations.thy similarity index 95% rename from src/tests/InnerSyntaxAntiquotations.thy rename to src/tests/TermAntiquotations.thy index 164be01..ee8a72f 100755 --- a/src/tests/InnerSyntaxAntiquotations.thy +++ b/src/tests/TermAntiquotations.thy @@ -18,7 +18,7 @@ For historical reasons, \<^emph>\term antiquotations\ are called th "Inner Syntax Antiquotations". \ theory - InnerSyntaxAntiquotations + TermAntiquotations imports "Isabelle_DOF.Conceptual" begin @@ -50,7 +50,7 @@ text\Some sample lemma:\ lemma murks : "Example=Example" by simp text\Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the - file @{file "InnerSyntaxAntiquotations.thy"}\ + file @{file "TermAntiquotations.thy"}\ (* not working: text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\Lorem ipsum ...\ *) @@ -65,7 +65,7 @@ text*[xcv2::C, g="@{thm ''HOL.refl''}"]\Lorem ipsum ...\ text\Major sample: test-item of doc-class \F\ with a relational link between class instances, and links to formal Isabelle items like \typ\, \term\ and \thm\. \ text*[xcv4::F, r="[@{thm ''HOL.refl''}, - @{thm \InnerSyntaxAntiquotations.murks\}]", (* long names required *) + @{thm \TermAntiquotations.murks\}]", (* long names required *) b="{(@{docitem ''xcv1''},@{docitem \xcv2\})}", (* notations \...\ vs. ''...'' *) s="[@{typ \int list\}]", properties = "[@{term \H \ H\}]" (* notation \...\ required for UTF8*)