From 7c66be090a8f715558548cd32698b294caff2fc0 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 10 Aug 2019 22:00:15 +0100 Subject: [PATCH] Removed example - not needed as we have Chapter 3 (and various examples in the actual distribution). --- .../Isabelle_DOF-Manual/04_RefMan.thy | 195 ------------------ 1 file changed, 195 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index f1d35737..c59390ff 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -659,8 +659,6 @@ super-classes. Overloading of attributes is not permitted in \ - - 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 @@ -702,199 +700,6 @@ by a text-element with a higher level, \ie{}, must contain a section or subsecti \ -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 -ontology (\autoref{lst:doc}): -\begin{isar} -theory Steam_Boiler - imports - tiny_cert (* The ontology defined in Listing 1.1. *) -begin -\end{isar} -This opens a new document (theory), called -\texttt{Steam\_Boiler} that imports our conceptual example ontology -``\texttt{tiny\_cert}'' (stored in a file -\texttt{tiny\_cert.thy}).\footnote{The usual import-mechanisms of the - Isabelle document model applies also to ODL: ontologies can be - extended, several ontologies may be imported, a document can - validate several ontologies.} - -\noindent Now we can continue to annotate our text as follows: -\begin{isar} -title*[a] \The Steam Boiler Controller\ -abstract*[abs, safety_level="SIL4", keywordlist = "[''controller'']"]\ - We present a formalization of a program which serves to control the - level of water in a steam boiler. -\ - -section*[intro::introduction]\Introduction\ -text\We present ...\ - -section*[T1::technical]\Physical Environment\ -text\ - The system comprises the following units - [*] the steam-boiler - [*] a device to measure the quantity of water in the steam-boiler - [*] ... -\ -\end{isar} - -\ - -text\ -Where \inlineisar+title*[a ...]+ is a predefined macro for -\inlineisar+text*[a::title,...]\...\+ (similarly \inlineisar+abstract*+). -The macro \inlineisar+section*+ assumes a class-id referring to a class that has -a \inlineisar+level+ attribute. We continue our example text: -\begin{isar}[mathescape] -text*[c1::contrib_claim, based_on="[''pumps'',''steam boiler'']" ]\ - As indicated in <@>{introduction "intro"}, we the water level of the - boiler is always between the minimum a$$nd the maximum allowed level. -\ -\end{isar} -\ -text\ -The first text element in this example fragment \<^emph>\defines\ the -text entity \inlineisar+c1+ and also references the formerly defined -text element \inlineisar+intro+ (which will be represented in the PDF -output, for example, by a text anchor ``Section 1'' and a hyperlink to -its beginning). The antiquotation \inlineisar+<@>{introduction ...}+, -which is automatically generated from the ontology, is immediately -validated (the link to \inlineisar+intro+ is defined) and type-checked (it -is indeed a link to an \inlineisar+introduction+ -text-element). Moreover, the IDE automatically provides editing and -development support such as auto-completion or the possibility to -``jump'' to its definition by clicking on the antiquotation. The -consistency checking ensures, among others, that the final document -will not contain any ``dangling references'' or references to entities of -another type. -\ -text\ -\dof as such does not require a particular evaluation strategy; -however, if the underlying implementation is based on a -declaration-before-use strategy, a mechanism for forward declarations -of references is necessary: -\begin{isar} -declare_reference* [] -\end{isar} -This command declares the existence of a text-element and allows for -referencing it, although the actual text-element will occur later in -the document. -\ - - -subsection\Editing Documents with Ontology Meta-Data: Inner Syntax\ -text\We continue our running example as follows: -\begin{isar}[mathescape] -text*[d1::definition]\ - We define the water level <@>{term "level"} of a system state - <@>{term "\"} of the steam boiler as follows: -\ -definition level :: "state \ real" where - "level \ = level0 + ..." -update_instance*[d1::definition, - property += "[<@>{term ''level \ = level0 + ...''}]"] - -text*[only::result,evidence="proof"]\ - The water level is never lower than <@>{term "level0"}: -\ -theorem level_always_above_level_0: "\ \. level \ \ level0" - unfolding level_def - by auto -update_instance*[only::result, - property += "[<@>{thm ''level_always_above_level_0''}]"] -\end{isar} -\ -text\ -As mentioned earlier, instances of document classes are mutable. We -use this feature to modify meta-data of these text-elements and -``assign'' them to the property-list afterwards and add results -from Isabelle definitions and proofs. The notation -\inlineisar|A+=X| stands for \inlineisar|A := A + X|. This mechanism -can also be used to define the required relation between \<^emph>\claims\ -and \<^emph>\results\ required in the \inlineisar|establish|-relation -required in a \inlineisar|summary|. -\ - - - section*["document-templates"::technical]\Defining Document Templates\ text\