From f1a6b6c60fc611d415272f63eb6ffe3b029dbde9 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 7 Aug 2019 09:04:53 +0100 Subject: [PATCH] Section restructuring. --- .../Isabelle_DOF-Manual/04_RefMan.thy | 360 +++++++++--------- 1 file changed, 188 insertions(+), 172 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 958e06e..cbf4faf 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -267,81 +267,75 @@ text\ \ -subsection*["odl-design"::example]\An Ontology Example\ - -text\We illustrate the design of \dof by modeling a small ontology - that can be used for writing formal specifications that, \eg, could - build the basis for an ontology for certification documents used in - processes such as Common Criteria~@{cite "cc:cc-part3:2006"} or CENELEC - 50128~@{cite "bsi:50128:2014"}.@{footnote \The \isadof distribution - contains an ontology for writing documents for a certification - according to CENELEC 50128.\} Moreover, in examples of certification - documents, we refer to a controller of a steam boiler that is - inspired by the famous steam boiler formalization - challenge~@{cite "abrial:steam-boiler:1996"}.\ - text\ -\begin{figure} -\begin{isar} -doc_class title = short_title :: "string option" <= "None" -doc_class author = email :: "string" <= "''''" - -datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 - -doc_class abstract = - keywordlist :: "string list" <= [] - safety_level :: "classification" <= "SIL3" -doc_class text_section = - authored_by :: "author set" <= "{}" - level :: "int option" <= "None" - -type_synonym notion = string - -doc_class introduction = text_section + - authored_by :: "author set" <= "UNIV" - uses :: "notion set" -doc_class claim = introduction + - based_on :: "notion list" -doc_class technical = text_section + - formal_results :: "thm list" -doc_class "d$$efinition" = technical + - is_formal :: "bool" - property :: "term list" <= "[]" - -datatype kind = expert_opinion | argument | proof - -doc_class result = technical + - evidence :: kind - property :: "thm list" <= "[]" -doc_class example = technical + - referring_to :: "(notion + d$$efinition) set" <= "{}" -doc_class "conclusion" = text_section + - establish :: "(claim \ result) set" -\end{isar}%$ - -\caption{An example ontology modeling simple certification documents, including - scientific papers such as~@{cite "brucker.ea:isabelle-ontologies:2018"}; also - recall \autoref{fig:dof-ide}.}\label{lst:doc} -\end{figure} +\begin{ltx} +\newisadof{text.CENELEC_50128.hypothesis}% +[label=,type=% +,Isa_COL.text_element.level=% +,Isa_COL.text_element.referentiable=% +,Isa_COL.text_element.variants=% +,CENELEC_50128.requirement.is_concerned=% +,CENELEC_50128.requirement.long_name=% +,CENELEC_50128.SRAC.formal_repr=% +,CENELEC_50128.SRAC.hypothesis_kind=% +,CENELEC_50128.hypothesis.hyp_type=% +][1]{ +#1 +} +\end{ltx} \ + +subsection*["core-manual1"::technical]\Annotatable Test-Elements: Syntax\ + +text\The syntax of toplevel \isadof commands reads as follows: +\<^item> \annotated_text_element\ : +\<^rail>\ + ( ( @@{command "title*"} + | @@{command "subtitle*"} + | @@{command "chapter*"} + | @@{command "section*"} | @@{command "subsection*"} + | @@{command "subsubsection*"} | @@{command "paragraph*"} | @@{command "subparagraph*"} + | @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"} + | @@{command "open_monitor*"} | @@{command "close_monitor*"} + | @@{command "Definition*"} | @@{command "Lemma*"} + | @@{command "Theorem*"} | @@{command "Conjecture*"} + ) + \ + '[' meta_args ']' '\' text '\' + ) + | change_status_command + | inspection_command + \ +\<^item> \meta_args\ : + \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ +\<^item> \rich_meta_args\ : + \<^rail>\ (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\ +\<^item> \isadof\change_status_command\ : + \<^rail>\ (@@{command "update_instance*"} '[' rich_meta_args ']') + | (@@{command "declare_reference*"} (obj_id ('::' class_id)))\ +\<^item> \isadof\inspection_command\ : + \<^rail>\ @@{command "print_doc_classes"} + | @@{command "print_doc_items"} + | @@{command "check_doc_global"}\ +\ + +subsubsection\Experts: Defining new top-level commands\ + text\ - \autoref{lst:doc} shows an example ontology for mathematical papers - (an extended version of this ontology was used for writing - @{cite "brucker.ea:isabelle-ontologies:2018"}, also recall - \autoref{fig:dof-ide}). The commands \inlineisar+datatype+ (modeling - fixed enumerations) and \inlineisar+type_synonym+ (defining type - synonyms) are standard mechanisms in HOL systems. Since ODL is an - add-on, we have to quote sometimes constant symbols (\eg, - \inlineisar+"proof"+) to avoid confusion with predefined keywords. ODL - admits overriding (such as \inlineisar+authored_by+ in the document - class \inlineisar+introduction+), where it is set to another library - constant, but no overloading. All \inlineisar+text_section+ elements - have an optional \inlineisar+level+ attribute, which will be used in - the output generation for the decision if the context is a section - header and its level (\eg, chapter, section, subsection). While - \within\ an inheritance hierarchy overloading is prohibited, - attributes may be re-declared freely in independent parts (as is the - case for \inlineisar+property+).\ +\begin{sml} +... +\end{sml} +\ + + +text\ +\begin{ltx} +... +\end{ltx} +\ + + + subsection*["sec:advanced"::technical]\Advanced ODL Concepts\ subsubsection\Meta-types as Types\ @@ -371,7 +365,7 @@ text\To express the dependencies between text elements to the formal generated from the ontology such as \inlineisar+<@>{definition }+. For the latter, the argument string must be checked that it represents a reference to a text-element - having the type \inlineisar+definition+ according to the ontology in @{example "odl-design"}.\ + having the type \inlineisar+definition+ according to the ontology in example ... .\ subsubsection*["sec:monitors"::technical]\ODL Monitors\ @@ -517,6 +511,126 @@ super-classes. Overloading of attributes is not permitted in \dof. \ + + + +subsection*["commonlib"::technical]\Common Ontology Library (COL)\ +text\ The COL library is used to capture a couple of text-elements +that are expected to be common to all document types, a class +that is actually not easy to define. After a lot of thought, we excluded +things like @{command "title*"} and abstract-related classes back again +to specific ontologies, for example. + +Finally, it is currently reduced to +\<^enum> the common infra-structure on text-elements (section is a text-element of a certain "level"), +\<^enum> common infrastructure to semi-formal Isabelle elements (Definitions, Assertions, Proofs), and +\<^enum> the common infra-structure for figures. + +Future extensions might include, for example, the infra-structure for tables. +\ + +text\ The super-class \<^verbatim>\text_element\ is the root of all text-elements used in \isadof. +It is defined as follows: +\begin{isar} +doc_class text_element = + level :: "int option" <= "None" + referentiable :: bool <= "False" + variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" +\end{isar} +Of major importance is the @{term "level"} which influences, inspired by a LaTeX convention, +the following classification: +\<^enum> part = Some -1 +\<^enum> chapter = Some 0 +\<^enum> section = Some 1 +\<^enum> subsection = Some 2 +\<^enum> subsubsection = Some 3 +\<^enum> ... +for scholarly paper: invariant level > + +The attribute @{term "level"} in the subsequent enables doc-notation --- a kind of macro --- +for support of @{command "chapter*"}, @{command "section*"} etc. This class definition forms +for a number of invariants; for example, the derived ontology \scholarly_paper\ contains an +invariant that any sequence of, for example, \technical\ - elements must be introduced +by a text-element with a higher level, \ie{}, must contain a section or subsection header. +\ + + +section\Example\ +text\We illustrate the design of \dof by modeling a small ontology + that can be used for writing formal specifications that, \eg, could + build the basis for an ontology for certification documents used in + processes such as Common Criteria~@{cite "cc:cc-part3:2006"} or CENELEC + 50128~@{cite "bsi:50128:2014"}.@{footnote \The \isadof distribution + contains an ontology for writing documents for a certification + according to CENELEC 50128.\} Moreover, in examples of certification + documents, we refer to a controller of a steam boiler that is + inspired by the famous steam boiler formalization + challenge~@{cite "abrial:steam-boiler:1996"}.\ + +text\ +\begin{figure} +\begin{isar} +doc_class title = short_title :: "string option" <= "None" +doc_class author = email :: "string" <= "''''" + +datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 + +doc_class abstract = + keywordlist :: "string list" <= [] + safety_level :: "classification" <= "SIL3" +doc_class text_section = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" + +type_synonym notion = string + +doc_class introduction = text_section + + authored_by :: "author set" <= "UNIV" + uses :: "notion set" +doc_class claim = introduction + + based_on :: "notion list" +doc_class technical = text_section + + formal_results :: "thm list" +doc_class "d$$efinition" = technical + + is_formal :: "bool" + property :: "term list" <= "[]" + +datatype kind = expert_opinion | argument | proof + +doc_class result = technical + + evidence :: kind + property :: "thm list" <= "[]" +doc_class example = technical + + referring_to :: "(notion + d$$efinition) set" <= "{}" +doc_class "conclusion" = text_section + + establish :: "(claim \ result) set" +\end{isar}%$ + +\caption{An example ontology modeling simple certification documents, including + scientific papers such as~@{cite "brucker.ea:isabelle-ontologies:2018"}; also + recall \autoref{fig:dof-ide}.}\label{lst:doc} +\end{figure} +\ +text\ + \autoref{lst:doc} shows an example ontology for mathematical papers + (an extended version of this ontology was used for writing + @{cite "brucker.ea:isabelle-ontologies:2018"}, also recall + \autoref{fig:dof-ide}). The commands \inlineisar+datatype+ (modeling + fixed enumerations) and \inlineisar+type_synonym+ (defining type + synonyms) are standard mechanisms in HOL systems. Since ODL is an + add-on, we have to quote sometimes constant symbols (\eg, + \inlineisar+"proof"+) to avoid confusion with predefined keywords. ODL + admits overriding (such as \inlineisar+authored_by+ in the document + class \inlineisar+introduction+), where it is set to another library + constant, but no overloading. All \inlineisar+text_section+ elements + have an optional \inlineisar+level+ attribute, which will be used in + the output generation for the decision if the context is a section + header and its level (\eg, chapter, section, subsection). While + \within\ an inheritance hierarchy overloading is prohibited, + attributes may be re-declared freely in independent parts (as is the + case for \inlineisar+property+).\ + + text\ We can now annotate a text as follows. First, we have to place a particular document into the context of our conceptual example @@ -632,87 +746,6 @@ and \<^emph>\results\ required in the \inlineisar|establish|-relati required in a \inlineisar|summary|. \ -subsection*["core-manual1"::technical]\Annotatable Test-Elements: Syntax\ - -text\The syntax of toplevel \isadof commands reads as follows: -\<^item> \annotated_text_element\ : -\<^rail>\ - ( ( @@{command "title*"} - | @@{command "subtitle*"} - | @@{command "chapter*"} - | @@{command "section*"} | @@{command "subsection*"} - | @@{command "subsubsection*"} | @@{command "paragraph*"} | @@{command "subparagraph*"} - | @@{command "text*"} | @@{command "figure*"} | @@{command "side_by_side_figure*"} - | @@{command "open_monitor*"} | @@{command "close_monitor*"} - | @@{command "Definition*"} | @@{command "Lemma*"} - | @@{command "Theorem*"} | @@{command "Conjecture*"} - ) - \ - '[' meta_args ']' '\' text '\' - ) - | change_status_command - | inspection_command - \ -\<^item> \meta_args\ : - \<^rail>\(obj_id ('::' class_id) ((attribute '=' term)) * ',')\ -\<^item> \rich_meta_args\ : - \<^rail>\ (obj_id ('::' class_id) ((attribute (('=' | '+=') term)) * ','))\ -\<^item> \isadof\change_status_command\ : - \<^rail>\ (@@{command "update_instance*"} '[' rich_meta_args ']') - | (@@{command "declare_reference*"} (obj_id ('::' class_id)))\ -\<^item> \isadof\inspection_command\ : - \<^rail>\ @@{command "print_doc_classes"} - | @@{command "print_doc_items"} - | @@{command "check_doc_global"}\ -\ - -subsection*["commonlib"::technical]\Common Ontology Library (COL)\ -text\ The COL library is used to capture a couple of text-elements -that are expected to be common to all document types, a class -that is actually not easy to define. After a lot of thought, we excluded -things like @{command "title*"} and abstract-related classes back again -to specific ontologies, for example. - -Finally, it is currently reduced to -\<^enum> the common infra-structure on text-elements (section is a text-element of a certain "level"), -\<^enum> common infrastructure to semi-formal Isabelle elements (Definitions, Assertions, Proofs), and -\<^enum> the common infra-structure for figures. - -Future extensions might include, for example, the infra-structure for tables. -\ - -text\ The super-class \<^verbatim>\text_element\ is the root of all text-elements used in \isadof. -It is defined as follows: -\begin{isar} -doc_class text_element = - level :: "int option" <= "None" - referentiable :: bool <= "False" - variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}" -\end{isar} -Of major importance is the @{term "level"} which influences, inspired by a LaTeX convention, -the following classification: -\<^enum> part = Some -1 -\<^enum> chapter = Some 0 -\<^enum> section = Some 1 -\<^enum> subsection = Some 2 -\<^enum> subsubsection = Some 3 -\<^enum> ... -for scholarly paper: invariant level > - -The attribute @{term "level"} in the subsequent enables doc-notation --- a kind of macro --- -for support of @{command "chapter*"}, @{command "section*"} etc. This class definition forms -for a number of invariants; for example, the derived ontology \scholarly_paper\ contains an -invariant that any sequence of, for example, \technical\ - elements must be introduced -by a text-element with a higher level, \ie{}, must contain a section or subsection header. -\ - -doc_class F = - property :: "term list" - r :: "thm list" - u :: "file" - s :: "typ list" - - section*["document-templates"::technical]\Defining Document Templates\ @@ -845,27 +878,10 @@ The general process as such is straight-forward: \end{document} \end{ltx} \ -section\Old Stuff \ -text\ -\begin{ltx} -\newisadof{text.CENELEC_50128.hypothesis}% -[label=,type=% -,Isa_COL.text_element.level=% -,Isa_COL.text_element.referentiable=% -,Isa_COL.text_element.variants=% -,CENELEC_50128.requirement.is_concerned=% -,CENELEC_50128.requirement.long_name=% -,CENELEC_50128.SRAC.formal_repr=% -,CENELEC_50128.SRAC.hypothesis_kind=% -,CENELEC_50128.hypothesis.hyp_type=% -][1]{ -#1 -} -\end{ltx} -\ + (*<*)