From 3895ba550c8d6a2e36c38a3a3701ae92f2b66508 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 14 Mar 2022 17:08:59 +0100
Subject: [PATCH] Import of DOF manual changes from /2021-ITP-PMTI

---
 .../Isabelle_DOF-Manual/01_Introduction.thy   |  9 ++-
 .../Isabelle_DOF-Manual/02_Background.thy     | 60 +++++++++++++------
 .../Isabelle_DOF-Manual/04_RefMan.thy         | 57 +++++++++++++++---
 .../Isabelle_DOF-Manual/document/preamble.tex | 12 ++--
 4 files changed, 104 insertions(+), 34 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
index 7acdcf5e..6988d674 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
@@ -119,10 +119,17 @@ text\<open>
       G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
       Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
       \href{https://doi.org/10.1007/978-3-030-30446-1_15}{10.1007/978-3-030-30446-1\_15}.
-
     \end{quote}
     A \<^BibTeX>-entry is available at: 
     \<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelledof-2019\<close>.
+  \<^item> for an application of \<^isadof> in the context of certifications:
+    \begin{quote}\small
+     A.~D. Brucker and B.~Wolff.
+     Using Ontologies in Formal Developments Targeting Certification. 
+     In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
+     Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
+     \href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
+    \end{quote}
 \<close>
 subsubsection\<open>Availability\<close>
 text\<open>
diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
index 820b9715..fce573bc 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
@@ -43,11 +43,11 @@ The current system framework offers moreover the following features:
 \<^item> an extensible front-end language Isabelle/Isar, and,
 \<^item> last but not least, an LCF style, generic theorem prover kernel as 
   the most prominent and deeply integrated system component.
-
-
+\<close>
+text\<open>
 The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, 
 with Standard ML (SML) at the bottom layer as implementation  language. The architecture actually 
-foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure\<^boxed_sml>\<open>Context\<close>. 
+foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>. 
 This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an 
 ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>. 
 On top of the latter, the LCF-Kernel, tactics,  automated proof procedures as well as specific 
@@ -70,13 +70,20 @@ declare_reference*["fig:dependency"::text_section]
 
 
 text\<open>
-  We assume a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document 
-  consist of a hierarchy \<^emph>\<open>sub-documents\<close>  (files) that can depend acyclically on each other. 
+  The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>  bindex>\<open>document-centric view\<close> of 
+  a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close> 
+  that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of 
+  \<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
+
+  Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document 
+  consist of a hierarchy \<^emph>\<open>sub-documents\<close>  (files); dependencies are restricted to be
+  acyclic at this level. 
   Sub-documents can have different document types in order to capture documentations consisting of 
   documentation, models, proofs, code of various forms and other technical artifacts.  We call the 
   main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files.  A theory file\<^bindex>\<open>theory!file\<close>
   consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body 
-  consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even 
+  consisting of a sequence of document elements called
+  \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
   the header consists of a sequence of commands used for introductory text elements not depending on 
   any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a 
   \<^boxed_theory_text>\<open>keyword\<close> section, for example:
@@ -96,30 +103,43 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
   @{boxed_theory_text [display]\<open>
 text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, 
    we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
-so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> paranthesis) which 
+... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in  \<open>\<open> ... \<close>\<close> paranthesis) which 
 contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close> 
 (here \<^theory_text>\<open>@{term "fac 5"}).\<close>
 \<close>
 
-text\<open>
-  We distinguish fundamentally two different syntactic levels:
-  \<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the 
-    syntax for commands) is processed by a lexer-library and parser combinators built on top, and
-  \<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the 
-    syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type  checking.
+text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
+use of \<^dof> in its current stage --- it is important to note that there are actually three
+families of ``ontology aware'' document elements with analogous 
+syntax to standard ones. The difference is a bracket with meta-data of the form:
+@{theory_text [display,indent=5, margin=70] 
+\<open>
+text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
+ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
+value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
+\<close>}
 
+Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close> 
+\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer 
+to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
+framework allows for nesting cartouches that permits to support to switch into a different
+context. In general, this has also the effect that the evaluation of antiquotations changes.
+\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the 
+Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>  
+\<close>
+text\<open>
   On the semantic level, we assume a validation process for an integrated document, where the 
   semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
-  This document model can be instantiated with outer-syntax commands for common 
-  text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.  
-  Thus, users can add informal text to a sub-document using a text command:
+  This document model can be instantiated depending on  the text-code-, or term-contexts.
+  For common text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>, 
+  users can add informal text to a sub-document using a text command:
   @{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
   This will type-set the corresponding text in, for example, a PDF document.  However, this 
   translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>, 
   machine-checked content via \<^emph>\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
   @{boxed_theory_text [display]
-  \<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma> 
-         for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
+  \<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm "refl"}, we obtain in \<Gamma> 
+         for @{term \<open>fac 5\<close>} the result @{value \<open>fac 5\<close>}.\<close>\<close>
   }
 which is represented in the final document (\<^eg>, a PDF) by:
 @{boxed_pdf [display]
@@ -137,10 +157,12 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
   typeset. They represent the device for linking the formal with the informal. 
 \<close>
 
+
+
 figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
        \<open>A Theory-Graph in the Document Model. \<close>
 
-section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model\<close>
+section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
 text\<open> 
   Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family, 
   \<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems 
diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 7787c2ae..eba7ccee 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -100,7 +100,8 @@ text\<open>
   to instances, and class-invariants. Some concepts like  advanced type-checking, referencing to 
   formal entities of Isabelle, and monitors are due to its specific application in the 
   Isabelle context. Conceptually, ontologies specified in ODL consist of:
-  \<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) that describe concepts;
+  \<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts;
+    the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accpted equally; 
   \<^item> an optional document base class expressing single inheritance
   class extensions;
   \<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
@@ -233,7 +234,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
 \<^item> \<open>doc_class_specification\<close>:\<^index>\<open>doc\_class\_specification@\<open>doc_class_specification\<close>\<close>
      We call document classes with an \<open>accepts_clause\<close> 
      \<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
-     \<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
+     \<^rail>\<open> (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) \<newline>
            (invariant_decl *) 
            (accepts_clause rejects_clause?)?\<close>
 \<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
@@ -319,12 +320,17 @@ supported on the Isabelle/Isar level. Note that some more advanced functionality
 is currently only available in the SML API's of the kernel. 
 
 \<^item> \<open>meta_args\<close> : 
-   \<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' term) *) \<close>
+   \<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
 \<^item> \<open>upd_meta_args\<close> :
-   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') term) * ))\<close>
+   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
 \<^item> \<open>annotated_text_element\<close> :
-\<^rail>\<open>
-    (  @@{command "text*"}'[' meta_args ']' '\<open>' text '\<close>' |
+\<^rail>\<open> 
+    (  (  @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
+        | @@{command "ML*"}   '[' meta_args ']' '\<open>' SML_code '\<close>'
+        | @@{command "term*"} '[' meta_args ']' '\<open>' HOL_term  '\<close>'
+        | @@{command "value*"}'[' meta_args ']' '\<open>' HOL_term  '\<close>'
+       )
+      |
        (  @@{command "open_monitor*"}  
         | @@{command "close_monitor*"} 
         | @@{command "declare_reference*"} 
@@ -350,10 +356,14 @@ text\<open>Recall that with the exception of \<^theory_text>\<open>text* \<dots>
 layout (such as \<^LaTeX>); these commands have to be wrapped into 
  \<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
 
-subsection\<open>Ontologic Text-Elements and their Management\<close>
-text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create 
+subsection\<open>Ontologic Text-Contexts and their Management\<close>
+text\<open> With respect to the family of text elements,
+ \<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
  an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>. This is viewed as the \<^emph>\<open>definition\<close> of
-an instance of a document class. This instance object is attached to the text-element
+an instance of a document class. The class invariants were checked for all attribute values
+at creation time if not specified otherwise. Unspecified attributed values were represented
+by fresh free variables.
+This instance object is attached to the text-element
 and makes it thus "trackable" for  \<^isadof>, \<^ie>, it can be referenced via the  \<^theory_text>\<open>oid\<close>, its attributes
 can be set by defaults in the class-definitions, or set at creation time, or modified at any
 point after creation via  \<^theory_text>\<open>update_instance*[oid, ...]\<close>. The \<^theory_text>\<open>class_id\<close> is syntactically optional;
@@ -374,6 +384,35 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
 pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
 \<close>
 
+subsection\<open>Ontologic Code-Contexts and their Management\<close>
+
+text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly : 
+a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional 
+ attributes and bound to \<^theory_text>\<open>oid\<close>. The SML-code is type-checked and executed 
+in the context of the SML toplevel of the Isabelle system as in the corresponding 
+\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
+\<close>
+
+subsection\<open>Ontologic Term-Contexts and their Management\<close>
+text\<open>The major commands providing term-contexts are 
+\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
+\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
+Wrt. to creation, track-ability and checking they are analogous to the ontological text and 
+code-commands. However the argument terms may contain term-antiquotations stemming from an
+ontology definition. Both term-contexts ware type-checked and \<^emph>\<open>validated\<close> against
+the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers 
+to a meta-object belonging to the document class \<open>A\<close>, for example).
+The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
+denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
+executable HOL-functions to interact with meta-objects.
+
+Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
+to choose either to the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or to a proof attempt via
+the \<^theory_text>\<open>auto\<close>. A failure of these strategies will be reported and regarded as non-validation
+of this meta-object. The latter leads to a failure of the entire command.
+
+\<close>
+
 (*<*)
 declare_reference*["sec:advanced"::technical]
 (*>*)
diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
index e507c1a8..01960819 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
+++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
@@ -41,8 +41,8 @@
 \pagestyle{headings}
 
 \uppertitleback{
-Copyright \copyright{} 2019--2021 University of Exeter, UK\\
-\phantom{Copyright \copyright{}} 2018--2021 Universit\'e Paris-Saclay, France\\
+Copyright \copyright{} 2019--2022 University of Exeter, UK\\
+\phantom{Copyright \copyright{}} 2018--2022 Universit\'e Paris-Saclay, France\\
 \phantom{Copyright \copyright{}} 2018--2019 The University of Sheffield, UK\\
 
 \smallskip
@@ -77,11 +77,13 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 
 \lowertitleback{%
 This manual describes \isadof version \isadofversion.  The latest official 
-release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest release.  The latest development version as well as official releases are available at 
+release is \isadoflatestversion{} (\href{https://doi.org/\isadoflatestdoi}{doi:\isadoflatestdoi}). 
+The DOI \href{https://doi.org/\isadofgenericdoi}{\isadofgenericdoi} will allways point to the latest 
+release.  The latest development version as well as official releases are available at 
 \url{\dofurl}.
 
 \paragraph*{Contributors.} We would like to thank the following contributors to \isadof 
-(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, Chantal Keller, and Nicolas M{\'e}ric.
+(in alphabetical order): Idir Ait-Sadoune, Paolo Crisafulli, and Nicolas M{\'e}ric.
 
 \paragraph*{Acknowledgments.} This work has been partially supported by IRT SystemX, Paris-Saclay, 
 France, and therefore granted with public funds of the Program ``Investissements d'Avenir.''
@@ -107,7 +109,7 @@ France, and therefore granted with public funds of the Program ``Investissements
   \hfill
   \begin{minipage}{8cm}
     \raggedleft\normalsize
-    Laboratoire en Recherche en Informatique (LRI)\\
+    Laboratoire des Methodes Formelles (LMF)\\
     Universit\'e Paris-Saclay\\
     91405 Orsay Cedex\\
     France