Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

...

This commit is contained in:
Burkhart Wolff 2021-03-14 12:03:52 +01:00
parent 9bba4301c1 46875b0560
commit ad18d3c179
27 changed files with 362 additions and 639 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.config
View File

@ -6,9 +6,9 @@ DOF_LATEST_DOI="10.5281/zenodo.3370483"
DOF_GENERIC_DOI="10.5281/zenodo.3370482" DOF_GENERIC_DOI="10.5281/zenodo.3370482"
# #
# Isabelle and AFP Configuration # Isabelle and AFP Configuration
ISABELLE_VERSION="Isabelle2020: April 2020" ISABELLE_VERSION="Isabelle2021: February 2021"
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2020/" ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021/"
AFP_DATE="afp-2020-04-20" AFP_DATE="afp-2021-03-09"
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz" AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
# #
# Isabelle/DOF Repository Configuration # Isabelle/DOF Repository Configuration

12
README.md
View File

@ -20,11 +20,11 @@ foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-u
Isabelle/DOF has two major pre-requisites: Isabelle/DOF has two major pre-requisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle 2020](http://isabelle.in.tum.de/website-Isabelle2020/). * **Isabelle:** Isabelle/DOF requires [Isabelle 2021](http://isabelle.in.tum.de/website-Isabelle2021/).
Please download the Isabelle 2020 distribution for your operating Please download the Isabelle 2021 distribution for your operating
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2020/). system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
* **LaTeX:** Isabelle/DOF requires a modern pdfTeX-engine supporting the \expanded{}-primitive. This * **LaTeX:** Isabelle/DOF requires a modern TeX-engine supporting the \expanded{}-primitive. This
is, for example, included in the [TeXLive 2019](https://www.tug.org/texlive/) (or later) is, for example, included in the [TeXLive 2020](https://www.tug.org/texlive/) (or later)
distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html) distribution. Please follow the [TeXLive installation instructions](https://www.tug.org/texlive/acquire-netinstall.html)
for installing TeXLive. for installing TeXLive.
@ -41,7 +41,7 @@ one), the full path to the ``isabelle`` command needs to be passed as
using the ``--isabelle`` command line argument of the ``install`` script: using the ``--isabelle`` command line argument of the ``install`` script:
```console ```console
foo@bar:~$ ./install --isabelle /usr/local/Isabelle2020/bin/isabelle foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021/bin/isabelle
``` ```
For further command line options of the installer, please use the For further command line options of the installer, please use the

1
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex
View File

@ -22,7 +22,6 @@
\usepackage{listings} \usepackage{listings}
\usepackage{lstisadof} \usepackage{lstisadof}
\usepackage{xspace} \usepackage{xspace}
\usepackage[draft]{fixme}
\lstloadlanguages{bash} \lstloadlanguages{bash}
\lstdefinestyle{bash}{language=bash, \lstdefinestyle{bash}{language=bash,

13
examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019-2020 The University of Exeter * 2019-2021 The University of Exeter
* 2018-2020 The University of Paris-Saclay * 2018-2021 The University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -18,7 +18,7 @@ begin
section\<open>Local Document Setup.\<close> section\<open>Local Document Setup.\<close>
text\<open>... introducing document specific abbreviations and macros.\<close> text\<open>Introducing document specific abbreviations and macros:\<close>
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close> define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
isadof \<rightleftharpoons> \<open>\isadof\<close> isadof \<rightleftharpoons> \<open>\isadof\<close>
@ -28,7 +28,6 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
LaTeX \<rightleftharpoons> \<open>\LaTeX{}\<close> LaTeX \<rightleftharpoons> \<open>\LaTeX{}\<close>
TeX \<rightleftharpoons> \<open>\TeX{}\<close> TeX \<rightleftharpoons> \<open>\TeX{}\<close>
pdf \<rightleftharpoons> \<open>PDF\<close> pdf \<rightleftharpoons> \<open>PDF\<close>
pdftex \<rightleftharpoons> \<open>\pdftex{}\<close>
text\<open>Note that these setups assume that the associated \<^LaTeX> macros text\<open>Note that these setups assume that the associated \<^LaTeX> macros
are defined, \<^eg>, in the document prelude. \<close> are defined, \<^eg>, in the document prelude. \<close>
@ -94,9 +93,6 @@ setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close> boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close>
\<close> \<close>
open_monitor*[this::report] open_monitor*[this::report]
(*>*) (*>*)
@ -140,7 +136,8 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
the link between formal and informal content in documents in a machine the link between formal and informal content in documents in a machine
checked way. These links can connect both text elements as well as formal checked way. These links can connect both text elements as well as formal
modelling elements such as terms, definitions, code and logical formulas, modelling elements such as terms, definitions, code and logical formulas,
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover. alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
\<close> \<close>
(*<*) (*<*)

2
examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
View File

@ -91,7 +91,7 @@ text\<open>
by simp\<close>} by simp\<close>}
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output): \<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
@{boxed_pdf [display] \<open>The axiom refl\<close>} @{boxed_pdf [display] \<open>The axiom refl\<close>}
\<^item> a red background for For (S)ML-code: \<^item> a red background for (S)ML-code:
@{boxed_sml [display] \<open>fun id x = x\<close>} @{boxed_sml [display] \<open>fun id x = x\<close>}
\<^item> a yellow background for \LaTeX-code: \<^item> a yellow background for \LaTeX-code:
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>} @{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}

34
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -47,7 +47,7 @@ The current system framework offers moreover the following features:
The Isabelle system architecture shown in @{docitem \<open>architecture\<close>} comes with many layers, 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 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 \inlinesml{Context}. 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 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>. 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 On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
@ -56,9 +56,9 @@ support for higher specification constructs were built.\<close>
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close> section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
text\<open> text\<open>
In this section, we explain the assumed document model underlying our Document Ontology Framework In this section, we explain the assumed document model underlying our Document Ontology Framework
(\<^dof>) in general. In particular we discuss the concepts \<^emph>\<open>integrated document\<close> (\<^dof>) in general. In particular we discuss the concepts
\<^bindex>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>, \<^bindex>\<open>sub-document\<close>, \<^emph>\<open>integrated document\<close>\<^bindex>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>\<^bindex>\<open>sub-document\<close>,
\<^emph>\<open>text-element\<close> \<^bindex>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> \<^bindex>\<open>semantic macros\<close> occurring \<^emph>\<open>text-element\<close>\<^bindex>\<open>text-element\<close>, and \<^emph>\<open>semantic macros\<close>\<^bindex>\<open>semantic macros\<close> occurring
inside text-elements. Furthermore, we assume two different levels of parsers inside text-elements. Furthermore, we assume two different levels of parsers
(for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically a typed \<open>\<lambda>\<close>-calculus (for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically a typed \<open>\<lambda>\<close>-calculus
and some Higher-order Logic (HOL)\<^bindex>\<open>HOL\<close>. and some Higher-order Logic (HOL)\<^bindex>\<open>HOL\<close>.
@ -81,14 +81,14 @@ text\<open>
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
\<^boxed_theory_text>\<open>keyword\<close> section, for example: \<^boxed_theory_text>\<open>keyword\<close> section, for example:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
theory Example (* Name of the 'theory' *) theory Example \<comment>\<open>Name of the 'theory'\<close>
imports (* Declaration of 'theory' dependencies *) imports \<comment>\<open>Declaration of 'theory' dependencies\<close>
Main (* Imports a library called 'Main' *) Main \<comment>\<open>Imports a library called 'Main'\<close>
keywords (* Registration of keywords defined locally *) keywords \<comment>\<open>Registration of keywords defined locally\<close>
requirement (* A command for describing requirements *)\<close>} requirement \<comment>\<open>A command for describing requirements\<close> \<close>}
where \<^boxed_theory_text>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_theory_text>\<open>Main\<close> refers to an where \<^boxed_theory_text>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_theory_text>\<open>Main\<close>
imported theory (recall that the import relation must be acyclic) and \<^boxed_theory_text>\<open>keywords\<close> are refers to an imported theory (recall that the import relation must be acyclic) and
used to separate commands from each other. \<^boxed_theory_text>\<open>keywords\<close> are used to separate commands from each other.
\<close> \<close>
text\<open> A text-element \<^index>\<open>text-element\<close> may look like this: text\<open> A text-element \<^index>\<open>text-element\<close> may look like this:
@ -98,18 +98,16 @@ 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>} 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> contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
(here in the notation \<^theory_text>\<open>@{term "fac 5"}).\<close> (here \<^theory_text>\<open>@{term "fac 5"}).\<close>
\<close> \<close>
text\<open> text\<open>
We distinguish fundamentally two different syntactic levels: 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 \<^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 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 \<^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. syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type checking.
On the semantic level, we assume a validation process for an integrated document, where the 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>. 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 This document model can be instantiated with outer-syntax commands for common
@ -142,7 +140,7 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"] figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
\<open>A Theory-Graph in the Document Model. \<close> \<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 Required Document Model\<close>
text\<open> text\<open>
Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family, 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 \<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems
@ -153,9 +151,8 @@ text\<open>
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which "wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which
in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle
versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be
nested along the \<open>\<open>...\<close>\<close> barriers, while \<^dof> actually only requires a two-level syntax model. nested along the \<open>\<open>...\<close>\<close> barriers), while \<^dof> actually only requires a two-level syntax model.
\<close> \<close>
(* end experiment *)
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open> figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page
@ -182,7 +179,6 @@ text\<open>
sub-documents into sessions, \<^ie>, sub-graphs of the document-structure that can be ``pre-compiled'' sub-documents into sessions, \<^ie>, sub-graphs of the document-structure that can be ``pre-compiled''
and loaded instantaneously, \<^ie>, without re-processing, which is an important means to scale up. \<close> and loaded instantaneously, \<^ie>, without re-processing, which is an important means to scale up. \<close>
(*<*) (*<*)
end end
(*>*) (*>*)

540
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019 The University of Exeter * 2019-2021 The University of Exeter
* 2018-2019 The University of Paris-Saclay * 2018-2021 The University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -35,89 +35,55 @@ available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus
\href{https://www.docker.com}{Docker} installed and \href{https://www.docker.com}{Docker} installed and
your installation of Docker supports X11 application, you can start \<^isadof> as follows: your installation of Docker supports X11 application, you can start \<^isadof> as follows:
@{boxed_bash [display] @{boxed_bash [display] \<open>ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \
\<open>ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \
-v /tmp/.X11-unix:/tmp/.X11-unix \ -v /tmp/.X11-unix:/tmp/.X11-unix \
logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \ logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \
isabelle jedit isabelle jedit\<close>}
\<close>}
\<close> \<close>
subsection*[installation::technical]\<open>Installation\<close> subsection*[installation::technical]\<open>Installation\<close>
text\<open> text\<open>
In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and In this section, we will show how to install \<^isadof> and its pre-requisites: Isabelle and
\<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell). \<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell).
\<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> (\isabellefullversion) with a recent \<^LaTeX>-distribution
(e.g., TexLive 2020 or later).
\<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version
of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle.
Thus, the same version of \<^isadof> might be available for different versions of Isabelle.
\<close> \<close>
subsubsection*[prerequisites::technical]\<open>Pre-requisites\<close> paragraph\<open>Installing Isabelle.\<close>
text\<open> text\<open>
\<^isadof> has to major pre-requisites: Please download and install Isabelle (version: \isabelleversion) from the
\<^item> \<^bold>\<open>Isabelle\<close>\<^bindex>\<open>Isabelle\<close> (\isabellefullversion). \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the
\<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version successful installation of Isabelle, you should be able to call the \<^boxed_bash>\<open>isabelle\<close>
of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle. tool on the command line:
Thus, the same version of \<^isadof> might be available for different versions of Isabelle. @{boxed_bash [display]\<open>ë\prompt{}ë isabelle version
\<^item> \<^bold>\<open>\<^TeXLive> 2020\<close>\<^bindex>\<open>TexLive@\<^TeXLive>\<close> (or any other modern \<^LaTeX>-distribution where ë\isabellefullversionë\<close>}
\<^pdftex> supports the \<^boxed_latex>\<open>\expanded\<close> primitive).
\<^footnote>\<open>see \<^url>\<open>https://www.texdev.net/2018/12/06/a-new-primitive-expanded\<close>\<close>
\<close>
paragraph\<open>Installing Isabelle\<close>
text\<open>
%\enlargethispage{\baselineskip}
Please download and install the Isabelle \isabelleversion distribution for your operating system
from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful
installation of Isabelle, you should be able to call the \<^boxed_bash>\<open>isabelle\<close> tool on the
command line:
\begin{bash}
ë\prompt{}ë isabelle version
ë\isabellefullversionë
\end{bash}
% bu : do not know why this does not work here ...
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë isabelle version
%ë\isabellefullversionë
%\<close>}
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its
full qualified path, \<^eg>: full qualified path, \<^eg>:
@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version
\begin{bash} ë\isabellefullversionë\<close>}
ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
ë\isabellefullversionë
\end{bash}
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
%ë\isabellefullversionë
%\<close>}
\<close> \<close>
paragraph\<open>Installing \<^TeXLive>\<close> paragraph\<open>Installing \<^TeXLive>.\<close>
text\<open> text\<open>
Modern Linux distribution will allow you to install \<^TeXLive> using their respective package Modern Linux distribution will allow you to install \<^TeXLive> using their respective package
managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command
should install all required \<^LaTeX> packages: should install all required \<^LaTeX> packages:
@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra\<close>}
\begin{bash}
ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
\end{bash}
%@ {boxed_bash [display]\<open>
%ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
%\<close>}
\<close> \<close>
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close> subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
text\<open> text\<open>
In the following, we assume that you already downloaded the \<^isadof> distribution In the following, we assume that you already downloaded the \<^isadof> distribution
(\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for (\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for
installing are extracting the \<^isadof> distribution and calling its \inlinebash|install| script. installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install\<close> script.
We start by extracting the \<^isadof> archive: We start by extracting the \<^isadof> archive:
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
\begin{bash}
ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë
\end{bash}
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution. This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installations Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installations
automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>),
@ -132,24 +98,23 @@ If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your \<^boxed_bash>
path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives
you an overview of all available configuration options): you an overview of all available configuration options):
\begin{bash} @{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
ë\prompt{}ë cd ë\isadofdirnë
ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
Isabelle/DOF Installer Isabelle/DOF Installer
====================== ======================
* Checking Isabelle version: * Checking Isabelle version:
Success: found supported Isabelle version ë(\isabellefullversion)ë Success: found supported Isabelle version ë(\isabellefullversion)ë
* Checking (La)TeX installation:
Success: pdftex supports \expanded{} primitive.
* Check availability of Isabelle/DOF patch: * Check availability of Isabelle/DOF patch:
Warning: Isabelle/DOF patch is not available or outdated. Warning: Isabelle/DOF patch is not available or outdated.
Trying to patch system .... Trying to patch system ....
Applied patch successfully, Isabelle/HOL will be rebuilt during Applied patch successfully, Isabelle/HOL will be rebuilt during
the next start of Isabelle. the next start of Isabelle.
* Checking availability of AFP entries: * Checking availability of AFP entries:\<close>}
Warning: could not find AFP entry Regular-Sets.
Warning: could not find AFP entry Functional-Automata. @{boxed_bash [display]
\<open>ëë Warning: could not find AFP entry Regular-Sets.
Warning: could not find AFP entry Functional-Automata.
Trying to install AFP (this might take a few *minutes*) .... Trying to install AFP (this might take a few *minutes*) ....
Registering Regular-Sets iëën Registering Regular-Sets iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë /home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
@ -170,26 +135,76 @@ Isabelle/DOF Installer
/home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë /home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë
* Installation successful. Enjoy Isabelle/DOF, you can build the session * Installation successful. Enjoy Isabelle/DOF, you can build the session
Isabelle/DOF and all example documents by executing: Isabelle/DOF and all example documents by executing:
/usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . /usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
\end{bash}
After the successful installation, you can now explore the examples (in the sub-directory After the successful installation, you can explore the examples (in the sub-directory
\inlinebash|examples| or create your own project. On the first start, the session \<^boxed_bash>\<open>examples\<close> or create your own project. On the first start, the session
\inlinebash|Isabelle_DOF| will be built automatically. If you want to pre-build this \<^boxed_bash>\<open>Isabelle_DOF\<close> will be built automatically. If you want to pre-build this
session and all example documents, execute: session and all example documents, execute:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build -D . \<close>}
\begin{bash}
ë\prompt{\isadofdirn}ë isabelle build -D .
\end{bash}
\<close> \<close>
subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close> subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
text\<open> text\<open>
\<^isadof> provides its own variant of Isabelle's \<^isadof> provides its own variant of Isabelle's
\inlinebash|mkroot| tool, called \inlinebash|mkroot_DOF|:\index{mkroot\_DOF} \<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>mkroot_DOF\<close>\index{mkroot\_DOF}:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF myproject
\begin{bash} Preparing session "myproject" iëën "myproject"
ë\prompt{}ë isabelle mkroot_DOF -h creating "myproject/ROOT"
creating "myproject/document/root.tex"
Now use the following coëëmmand line to build the session:
isabelle build -D myproject \<close>}
The created project uses the default configuration (the ontology for writing academic papers
(scholarly\_paper) using a report layout based on the article class (\<^boxed_latex>\<open>scrartcl\<close>) of
the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}. The directory \<^boxed_bash>\<open>myproject\<close>
contains the \<^isadof>-setup for your new document. To check the document formally, including the
generation of the document in PDF, you only need to execute
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle build -d . myproject \<close>}
The dictory \<^boxed_bash>\<open>myproject\<close> contains the following files and directories:
\begin{center}
\begin{minipage}{.9\textwidth}
\dirtree{%
.1 .
.2 myproject.
.3 document.
.4 build\DTcomment{Build Script}.
.4 isadof.cfg\DTcomment{\<^isadof> configuraiton}.
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
.3 ROOT\DTcomment{Isabelle build-configuration}.
}
\end{minipage}
\end{center}
The \<^isadof> configuration (\<^boxed_bash>\<open>isadof.cfg\<close>) specifies the required
ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that
\<^isadof>'s document setup does not make use of a file \<^boxed_bash>\<open>root.tex\<close>: this file is
replaced by built-in document templates.\<close> The main two configuration files for
users are:
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
\<close>
text\<open>
Creating a new document setup requires two decisions:
\<^item> which ontologies (\<^eg>, scholarly\_paper) are required and
\<^item> which document template (layout)\index{document template} should be used
(\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually
obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \<^boxed_bash>\<open>llncs.cls\<close>.
This is due to licensing restrictions).\<close>
text\<open>
This can be configured by using the command-line options of of \<^boxed_bash>\<open>mkroot_DOF\<close>. In
Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows to selecting
the document template. The built-in help (using \<^boxed_bash>\<open>-h\<close>) shows all available options
as well as a complete list of the available document templates and ontologies:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF -h
Usage: isabelle mkroot_DOF [OPTIONS] [DIR] Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
@ -209,70 +224,12 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
* scrreprt-modern * scrreprt-modern
* scrreprt * scrreprt
Prepare session root DIR (default: current directory). Prepare session root DIR (default: current directory). \<close>}
\end{bash}
Creating a new document setup requires two decisions:
\<^item> which ontologies (\<^eg>, scholarly\_paper) are required and
\<^item> which document template (layout)\index{document template} should be used
(\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually
obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \inlinebash|llncs.cls|.
This is due to licensing restrictions).
\<close>
text\<open>
If you are happy with the defaults, \ie, using the ontology for writing academic papers
(scholarly\_paper) using a report layout based on the article class (\inlineltx|scrartcl|) of
the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}, you can create your first project
\inlinebash|myproject| as follows:
\begin{bash}
ë\prompt{}ë isabelle mkroot_DOF myproject
Preparing session "myproject" iëën "myproject"
creating "myproject/ROOT"
creating "myproject/document/root.tex"
Now use the following coëëmmand line to build the session:
isabelle build -D myproject
\end{bash}
This creates a directory \inlinebash|myproject| containing the \<^isadof>-setup for your
new document. To check the document formally, including the generation of the document in PDF,
you only need to execute
\begin{bash}
ë\prompt{}ë isabelle build -d . myproject
\end{bash}
This will create the directory \inlinebash|myproject|:
\begin{center}
\begin{minipage}{.9\textwidth}
\dirtree{%
.1 .
.2 myproject.
.3 document.
.4 build\DTcomment{Build Script}.
.4 isadof.cfg\DTcomment{\<^isadof> configuraiton}.
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
.3 ROOT\DTcomment{Isabelle build-configuration}.
}
\end{minipage}
\end{center}
The \<^isadof> configuration (\inlinebash|isadof.cfg|) specifies the required
ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that
\<^isadof>'s document setup does not make use of a file \inlinebash|root.tex|: this file is
replaced by built-in document templates.\<close> The main two configuration files for
users are:
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
\<^item> The file \<^boxed_bash>\<open>praemble.tex\<close>\<^index>\<open>praemble.tex\<close>, which allows users to add additional
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
\<close> \<close>
section*[scholar_onto::example]\<open>Writing Academic Publications in \<^boxed_theory_text>\<open>scholarly_paper\<close>\<close> section*[scholar_onto::example]\<open>Writing Academic Publications in \<^boxed_theory_text>\<open>scholarly_paper\<close>\<close>
subsection\<open>Papers in freeform-style\<close> subsection\<open>Writing Academic Papers\<close>
text\<open> text\<open>
The ontology \<^boxed_theory_text>\<open>scholarly_paper\<close> The ontology \<^boxed_theory_text>\<open>scholarly_paper\<close>
\<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling \<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
@ -284,7 +241,7 @@ text\<open>
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text, \<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
between statements, definitions and proofs which is ontologically tracked. However, wrt. between statements, definitions and proofs which is ontologically tracked. However, wrt.
to the possible linking between the underlying formal theory and this mathematical presentation, the possible linking between the underlying formal theory and this mathematical presentation,
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems, it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
deliberately not exploiting \<^isadof> 's full potential with this regard. deliberately not exploiting \<^isadof> 's full potential with this regard.
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately \<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
@ -302,17 +259,13 @@ text\<open>
\nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}. \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}.
\<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling: \<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling:
\begin{bash} @{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
ë\prompt{\isadofdirn}ë isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \<close>}
isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy
\end{bash}
\<close> \<close>
(* We should discuss if we shouldn't put the iFM paper more in the foreground *)
text\<open> You can build the PDF-document at the command line by calling: text\<open> You can build the PDF-document at the command line by calling:
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build -d . 2020-iFM-csp \<close>}
@{boxed_bash [display]
\<open>ë\prompt{}ë isabelle build -d . 2020-iFM-csp \<close>}
\<close> \<close>
subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close> subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close>
@ -346,7 +299,7 @@ context of this document; this is a decisive feature of \<^isadof> that conventi
languages lack.\<close> languages lack.\<close>
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
to \<open>figure\<close> or \<open>table\<close> or similar. Note that to \<open>figure\<close> or \<open>table\<close> or similar). Note that
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
the document class definition \<open>author\<close> shown above. It is used to express which author currently the document class definition \<open>author\<close> shown above. It is used to express which author currently
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even ``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
@ -436,22 +389,6 @@ standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism i
for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type
definition. \<close> definition. \<close>
(* For Achim zum spielen...
text\<open>For example, this allows the following presentation in the source:
@{boxed_theory_text [display] \<open>
text*[X2::"definition"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<^vs>\<open>-0.7cm\<close>\<close>
text*[X3::"definition"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<^vs>\<open>-0.7cm\<close>\<close>
text*[X4::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<^vs>\<open>-0.7cm\<close>\<close>
text\<open> The \<open>RUN\<close>-process defined @{definition X2} represents the process that accepts all
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
@{definition X3} and @{definition X4}: the process that non-deterministically stops or
accepts any offered event, wheras \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionaly terminate.\<close>
\<close>}
\<close>
*)
(* alternative *)
figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"] figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"]
\<open> A screenshot of the integrated source with definitions ...\<close> \<open> A screenshot of the integrated source with definitions ...\<close>
text\<open>An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as text\<open>An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as
@ -460,11 +397,15 @@ later is shown in \<^figure>\<open>fig01\<close> in its presentation as the inte
Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close> Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. to the sub-typing by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the
defining occurrence of this text-element in the integrated source. defining occurrence of this text-element in the integrated source.
Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> interact with standard Isabelle document % TODO:
% The definition \<^theory_text>\<open>@{definition X4}\<close> is not present in the screenshot,
% it might be better to use \<^theory_text>\<open>@{definition X22}\<close>.
Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> interact with standard Isabelle document
antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail. antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail.
We refrain ourselves here to briefly describe three freeform antiquotations used her in this text: We refrain ourselves here to briefly describe three freeform antiquotations used her in this text:
@ -477,58 +418,20 @@ We refrain ourselves here to briefly describe three freeform antiquotations used
\<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements. \<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
\<close> \<close>
figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
\<open> ... and the corresponding pdf-oputput.\<close>
text\<open> text\<open>
\<^isadof> text-elements such as \<^theory_text>\<open>text*\<close> allow to have such standard term-antiquotations inside their \<^isadof> text-elements such as \<^theory_text>\<open>text*\<close> allow to have such standard term-antiquotations inside their
text, permitting to give the whole text entity a formal, referentiable status with typed meta- text, permitting to give the whole text entity a formal, referentiable status with typed meta-
information attached to it that may be used for presentation issues, search, or other technical information attached to it that may be used for presentation issues, search, or other technical
purposes. purposes. The corresponding output of this snippet in the integrated source is shown in \<^figure>\<open>fig02\<close>.
\<close> \<close>
figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
\<open> ... and the corresponding pdf-oputput.\<close>
text\<open>The corresponding output of this snippet in the integrated source is shown in\<^figure>\<open>fig02\<close>. \<close>
subsection*[scholar_pide::example]\<open>More Freeform Elements, and Resulting Navigation\<close> subsection*[scholar_pide::example]\<open>More Freeform Elements, and Resulting Navigation\<close>
(*
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
\<open> Ouroboros I: This paper from inside \ldots \<close>
text\<open>
@{docitem \<open>fig1\<close>} shows the corresponding view in the Isabelle/jedit of the start of an academic
paper. The text uses \<^isadof>'s own text-commands containing the meta-information provided by the
underlying ontology. We proceed by a definition of \<^boxed_theory_text>\<open>introduction\<close>'s, which we define
as the extension of \<^boxed_theory_text>\<open>text_section\<close> which is intended to capture common infrastructure:
@{boxed_theory_text [display]\<open>
doc_class introduction = text_section +
comment :: string
\<close>}
As a consequence of the definition as extension, the \<^boxed_theory_text>\<open>introduction\<close> class
inherits the attributes \<^boxed_theory_text>\<open>main_author\<close> and \<^boxed_theory_text>\<open>todo_list\<close>
together with the corresponding default values.
We proceed more or less conventionally by the subsequent sections:
@{boxed_theory_text [display]\<open>
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
doc_class example = text_section +
comment :: string
doc_class conclusion = text_section +
main_author :: "author option" <= None
doc_class related_work = conclusion +
main_author :: "author option" <= None
\<close>}
*)
text\<open> In the following, we present some other text-elements provided by the Common Ontology Library text\<open> In the following, we present some other text-elements provided by the Common Ontology Library
in @{theory "Isabelle_DOF.Isa_COL"}. it provides a document class for figures: in @{theory "Isabelle_DOF.Isa_COL"}. It provides a document class for figures:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
datatype placement = h | t | b | ht | hb datatype placement = h | t | b | ht | hb
@ -559,8 +462,12 @@ text\<open>
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~ where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~ introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
bibliography)" bibliography)"
\<close>} \<close>}\<close>
(* % TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects. *)
text\<open>
In a integrated document source, the body of the content can be paranthesized into: In a integrated document source, the body of the content can be paranthesized into:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
@ -594,9 +501,8 @@ text\<open>
meta-information. Clicking on a document class identifier permits to hyperlink into the meta-information. Clicking on a document class identifier permits to hyperlink into the
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
attribute-definition (which is qualified in order to disambiguate; attribute-definition (which is qualified in order to disambiguate;
\autoref{fig:Dogfood-V-attribute}). \autoref{fig:Dogfood-V-attribute}) shows its type.
\<close> \<close>
(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *)
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"] figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
\<open> Exploring an attribute (hyperlinked to the class). \<close> \<open> Exploring an attribute (hyperlinked to the class). \<close>
@ -621,16 +527,12 @@ text\<open>
\nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}. \nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}.
\<^item> starting Isabelle/jedit from the command line by calling: \<^item> starting Isabelle/jedit from the command line by calling:
\begin{bash} @{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
ë\prompt{\isadofdirn}ë isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \<close>}
isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy
\end{bash}
\<close> \<close>
text\<open>\<^noindent> Finally, you text\<open>\<^noindent> Finally, you
\<^item> can build the PDF-document by calling: \<^item> can build the PDF-document by calling:
\begin{bash} @{boxed_bash [display]\<open>ë\prompt{}ë isabelle build mini_odo \<close>}
ë\prompt{}ë isabelle build mini_odo
\end{bash}
\<close> \<close>
subsection\<open>Modeling CENELEC 50128\<close> subsection\<open>Modeling CENELEC 50128\<close>
@ -646,12 +548,10 @@ text\<open>
processes. Making the link-structure machine-checkable, be it between requirements, assumptions, processes. Making the link-structure machine-checkable, be it between requirements, assumptions,
their implementation and their discharge by evidence (be it tests, proofs, or authoritative their implementation and their discharge by evidence (be it tests, proofs, or authoritative
arguments), has the potential in our view to decrease the cost of software developments arguments), has the potential in our view to decrease the cost of software developments
targeting certifications. Note that continuously checking the links between the formal and the targeting certifications.
semi-formal parts of such documents is particularly valuable during the development,
which is usually a collaborative effort.
As in many other cases, formal certification documents come with an own terminology and pragmatics As in many other cases, formal certification documents come with an own terminology and pragmatics
of what has to be demonstrated and where, and how the trace-ability of requirements through of what has to be demonstrated and where, and how the traceability of requirements through
design-models over code to system environment assumptions has to be assured. design-models over code to system environment assumptions has to be assured.
In the sequel, we present a simplified version of an ontological model used in a In the sequel, we present a simplified version of an ontological model used in a
@ -663,7 +563,11 @@ doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat" doc_class requirement_analysis = no :: "nat"
where "requirement_item +" where "requirement_item +"
(*
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
*)
doc_class hypothesis = requirement + doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *) hyp_type :: hyp_type <= physical (* default *)
@ -675,7 +579,7 @@ doc_class assumption = requirement +
Such ontologies can be enriched by larger explanations and examples, which may help Such ontologies can be enriched by larger explanations and examples, which may help
the team of engineers substantially when developing the central document for a certification, the team of engineers substantially when developing the central document for a certification,
like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an like an explication of what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each \<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
document class its definition available by a simple mouse-click, this kind on meta-knowledge document class its definition available by a simple mouse-click, this kind on meta-knowledge
can be made far more accessible during the document evolution. can be made far more accessible during the document evolution.
@ -683,23 +587,23 @@ can be made far more accessible during the document evolution.
For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions.
It has formal, semi-formal and informal sub-categories. They have to be It has formal, semi-formal and informal sub-categories. They have to be
tracked and discharged by appropriate validation procedures within a tracked and discharged by appropriate validation procedures within a
certification process, by it by test or proof. It is different from a hypothesis, which is certification process, be it by test or proof. It is different from a hypothesis, which is
globally assumed and accepted. globally assumed and accepted.
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short) In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
is used for formal assumptions, that arise during the analysis, is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final design or implementation and have to be tracked till the final
evaluation target, and discharged by appropriate validation procedures evaluation target, and discharged by appropriate validation procedures
within the certification process, by it by test or proof. A particular class of interest within the certification process, be it by test or proof. A particular class of interest
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close> is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>SRAC\<close>
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
of the evaluation target. Their track-ability throughout the certification of the evaluation target. Their traceability throughout the certification
is therefore particularly critical. This is naturally modeled as follows: is therefore particularly critical. This is naturally modeled as follows:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
doc_class ec = assumption + doc_class ec = assumption +
assumption_kind :: ass_kind <= (*default *) formal assumption_kind :: ass_kind <= (*default *) formal
doc_class srac = ec + doc_class SRAC = ec +
assumption_kind :: ass_kind <= (*default *) formal assumption_kind :: ass_kind <= (*default *) formal
\<close>} \<close>}
@ -725,12 +629,18 @@ subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"] figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
\<open> Standard antiquotations referring to theory elements.\<close> \<open> Standard antiquotations referring to theory elements.\<close>
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts @{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
of a document get ``formal content'' and become more robust under change.\<close> of a document get ``formal content'' and become more robust under change.\<close>
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"] figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
\<open> Defining a "SRAC" in the integrated source \ldots \<close> \<open> Defining a "SRAC" in the integrated source \ldots \<close>
text\<open>
TODO:
The screenshot (figures/srac-definition) of the figure figfig5 should be updated
to have a SRAC type in uppercase.
\<close>
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"] figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
\<open> Using a "SRAC" as "EC" document element. \<close> \<open> Using a "SRAC" as "EC" document element. \<close>
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an
@ -742,130 +652,6 @@ safety-related condition; however, this happens in a context where general \<^em
are listed. \<^isadof>'s checks establish that this is legal in the given ontology. are listed. \<^isadof>'s checks establish that this is legal in the given ontology.
\<close> \<close>
(*
section*[math_exam::example]\<open>Writing Exams (math\_exam)\<close>
subsection\<open>The Math Exam Example\<close>
text\<open>
The ontology ``math\_exam''\index{ontology!math\_exam} is an experimental ontology modeling
the process of writing exams at higher education institution in the United Kingdom, where exams
undergo both an internal and external review process. The \<^isadof> distribution contains a tiny
example using the ontology ``math\_exam'' in the directory
\nolinkurl{examples/math_exam/MathExam/}. You can inspect/edit the example
in Isabelle's IDE, by either
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/math_exam/MathExam/MathExam.thy}.
\<^item> starting Isabelle/jedit from the command line by calling:
\begin{bash}
ë\prompt{\isadofdirn}ë
isabelle jedit examples/math_exam/MathExam/MathExam.thy
\end{bash}
\<close>
text\<open>
You can build the PDF-document by calling:
\begin{bash}
ë\prompt{}ë isabelle build MathExam
\end{bash}
\<close>
subsection\<open>Modeling Exams\<close>
text\<open>
The math-exam scenario is an application with mixed formal and semi-formal content. It addresses
applications where the author of the exam is not present during the exam and the preparation
requires a very rigorous process.
We assume that the content has four different types of addressees, which have a different
\<^emph>\<open>view\<close> on the integrated document:
\<^item> the \<^emph>\<open>setter\<close>, \ie, the author of the exam,
\<^item> the \<^emph>\<open>checker\<close>, \ie, an internal person that checks
the exam for feasibility and non-ambiguity,
\<^item> the \<^emph>\<open>external\<close>, \ie, an external person that checks
the exam for feasibility and non-ambiguity, and
\<^item> the \<^emph>\<open>student\<close>, \ie, the addressee of the exam.
\<close>
text\<open>
The latter quality assurance mechanism is used in many universities,
where for organizational reasons the execution of an exam takes place in facilities
where the author of the exam is not expected to be physically present.
Furthermore, we assume a simple grade system (thus, some calculation is required). We
can model this as follows:
@{boxed_theory_text [display]\<open>
doc_class Author = ...
datatype Subject = algebra | geometry | statistical
datatype Grade = A1 | A2 | A3
doc_class Header = examTitle :: string
examSubject :: Subject
date :: string
timeAllowed :: int -- minutes
datatype ContentClass = setter
| checker
| external_examiner
| student
doc_class Exam_item = concerns :: "ContentClass set"
doc_class Exam_item = concerns :: "ContentClass set"
type_synonym SubQuestion = string
\<close>}
The heart of this ontology is an alternation of questions and answers, where the answers can
consist of simple yes-no answers or lists of formulas. Since we do not assume familiarity of
the students with Isabelle (\<^boxed_theory_text>\<open>term\<close> would assume that this is a parse-able and
type-checkable entity), we basically model a derivation as a sequence of strings:
@{boxed_theory_text [display]\<open>
doc_class Answer_Formal_Step = Exam_item +
justification :: string
"term" :: "string"
doc_class Answer_YesNo = Exam_item +
step_label :: string
yes_no :: bool -- \<open>for checkboxes\<close>
datatype Question_Type =
formal | informal | mixed
doc_class Task = Exam_item +
level :: Level
type :: Question_Type
subitems :: "(SubQuestion *
(Answer_Formal_Step list + Answer_YesNo) list) list"
concerns :: "ContentClass set" <= "UNIV"
mark :: int
doc_class Exercise = Exam_item +
type :: Question_Type
content :: "(Task) list"
concerns :: "ContentClass set" <= "UNIV"
mark :: int
\<close>}
In many institutions, having a rigorous process of validation for exam subjects makes sense: is
the initial question correct? Is a proof in the sense of the question possible? We model the
possibility that the @{term examiner} validates a question by a sample proof validated by Isabelle:
@{boxed_theory_text [display]\<open>
doc_class Validation =
tests :: "term list" <="[]"
proofs :: "thm list" <="[]"
doc_class Solution = Exam_item +
content :: "Exercise list"
valids :: "Validation list"
concerns :: "ContentClass set" <= "{setter,checker,external_examiner}"
doc_class MathExam=
content :: "(Header + Author + Exercise) list"
global_grade :: Grade
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
\<close>}
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \ie, not exposed to the
students but just additional material for the internal review process of the exam.
\<close>
*)
section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close> section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>
text\<open>While it is perfectly possible to write documents in the text\<open>While it is perfectly possible to write documents in the
@ -882,27 +668,25 @@ underlying logical context, which turns the arguments into \<^emph>\<open>formal
source, in contrast to the free-form antiquotations which basically influence the presentation. source, in contrast to the free-form antiquotations which basically influence the presentation.
We still mention a few of these document antiquotations here: We still mention a few of these document antiquotations here:
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> ou \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference \<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
to a theorem; the additional "style" argument changes the presentation by printing the to a theorem; the additional "style" argument changes the presentation by printing the
formula into the output instead of the reference itself, formula into the output instead of the reference itself,
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee \<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee
that it is a corrollary of the current context, that it is a corrollary of the current context,
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>, \<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>, \<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> pa,rses and type-checks \<open>ml-term\<close>, \<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> parses and type-checks \<open>ml-term\<close>,
\<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and \<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and
verifies its existance in the (Isabelle-virtual) file-system, verifies its existance in the (Isabelle-virtual) file-system.
\<^item> ... \<close>
text\<open>There are options to display sub-parts of formulas etc., but it is a consequence
Note that there are options to display sub-parts of formulas etc., but it is a consequence
of tight-checking that the information must be given complete and exactly in the syntax of of tight-checking that the information must be given complete and exactly in the syntax of
Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may
motivate authors to choose the aforementioned freeform-style. motivate authors to choose the aforementioned freeform-style.
\<close> \<close>
subsection\<open>A \<^verbatim>\<open>technical_report\<close> in tight-checking-style: \<open>MyCommentedIsabelle\<close> - Programming Manual \<close> subsection\<open>A Technical Report with Tight Checking\<close>
text\<open>An example of tight checking is a small programming manual developed by the
text\<open>An example of tight checking is a small programming programming manual developed by the
second author in order to document programming trick discoveries while implementing in Isabelle. second author in order to document programming trick discoveries while implementing in Isabelle.
While not necessarily a meeting standards of a scientific text, it appears to us that this information While not necessarily a meeting standards of a scientific text, it appears to us that this information
is often missing in the Isabelle community. is often missing in the Isabelle community.
@ -914,29 +698,13 @@ So its value is that readers can just reuse some of these snippets and adapt the
purposes. purposes.
\<close> \<close>
(*
@{boxed_theory_text [display] \<open>
text\<open>Finally, a number of commonly used "squigglish" combinators is listed:
\<^item> @{ML "op ! : 'a Unsynchronized.ref->'a"}, access operation on a program variable
\<^item> @{ML "op := : ('a Unsynchronized.ref * 'a)->unit"}, update operation on a program variable
\<^item> @{ML "op #> : ('a->'b) * ('b->'c)->'a->'c"}, a reversed function composition
\<^item> @{ML "op o : (('b->'c) * ('a->'b))->'a->'c"}, function composition
\<^item> @{ML "op || : ('a->'b) * ('a->'b) -> 'a -> 'b"}, parse alternative
\<^item> @{ML "op -- : ('a->'b*'c) * ('c->'d*'e)->'a->('b*'d)*'e"}, parse pair
\<^item> @{ML "op ? : bool * ('a->'a)->'a->'a"}, if then else
\<^item> @{ML "I : 'a -> 'a"}, the I combinator
\<^item> @{ML "K : 'a -> 'b -> 'a"}, the K combinator \<close>
\<close>}
*)
figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"] figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabelle.png''"]
\<open>A table with a number of SML functions, together with their type.\<close> \<open>A table with a number of SML functions, together with their type.\<close>
text\<open> text\<open>
\<open>MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"} \<open>TR_MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source gives an idea why ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
it tight-checking allows for keeping track of underlying Isabelle changes: its tight-checking allows for keeping track of underlying Isabelle changes:
Any reference to an SML operation in some library module is type-checked, and the displayed Any reference to an SML operation in some library module is type-checked, and the displayed
SML-type really corresponds to the type of the operations in the underlying SML environment. SML-type really corresponds to the type of the operations in the underlying SML environment.
In the pdf output, these text-fragments were displayed verbatim. In the pdf output, these text-fragments were displayed verbatim.
@ -946,12 +714,12 @@ In the pdf output, these text-fragments were displayed verbatim.
section\<open>Style Guide\<close> section\<open>Style Guide\<close>
text\<open> text\<open>
The document generation process of \<^isadof> is based on Isabelle's document generation framework, The document generation of \<^isadof> is based on Isabelle's document generation framework,
using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is
possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>: possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
text\<open> This is \emph{emphasized} a$$nd this is a text\<open> This is \emph{emphasized} and this is a
citation~\cite{brucker.ea:isabelle-ontologies:2018}\<close> citation~\cite{brucker.ea:isabelle-ontologies:2018}\<close>
\<close>} \<close>}
@ -959,8 +727,8 @@ text\<open> This is \emph{emphasized} a$$nd this is a
Isabelle) provided alternatives: Isabelle) provided alternatives:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
text\<open> This is *\<open>emphasized\<close> a$$nd this is a text\<open> This is *\<open>emphasized\<close> and this is a
citation <@>{cite "brucker.ea:isabelle-ontologies:2018"}.\<close> citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
\<close>} \<close>}
Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain
@ -976,7 +744,7 @@ document generation (\<^eg>, HTML) which, naturally, are only available to docum
too complex native \<^LaTeX>-commands. too complex native \<^LaTeX>-commands.
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
create dangeling references during the document generation that break the document generation. create dangling references during the document generation that break the document generation.
Finally, we recommend to use the @{command "check_doc_global"} command at the end of your Finally, we recommend to use the @{command "check_doc_global"} command at the end of your
document to check the global reference structure. document to check the global reference structure.

174
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019-2020 University of Exeter * 2019-2021 University of Exeter
* 2018-2020 University of Paris-Saclay * 2018-2021 University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -51,17 +51,17 @@ text\<open>
\<close> \<close>
text\<open> text\<open>
Similarly to Isabelle, which is based on a core logic \<^theory>\<open>Pure\<close> and then extended by libraries Similarly to Isabelle, which is based on a core logic \<^theory>\<open>Pure\<close> and then extended by libraries
to major systems like \<^verbatim>\<open>HOL\<close> or \<^verbatim>\<open>FOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then to major systems like \<^verbatim>\<open>HOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then
presents itself to users via major library extensions, which add domain-specific 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 system-extensions. Ontologies in \<^isadof> are not just a sequence of descriptions in
\<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated \<^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. sources that provide textual decriptions, abbreviations, macro-support and even ML-code.
Conceptually, the library of \<^isadof> is currently organized as follows Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close>
\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close> organisation is slightly different and shown in organisation is slightly different and shown in
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>: @{technical (unchecked) \<open>infrastructure\<close>}.\<close>:
% %
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.1 COL\DTcomment{The Common Ontology Library}. .1 COL\DTcomment{The Common Ontology Library}.
.2 scholarly\_paper\DTcomment{Scientific Papers}. .2 scholarly\_paper\DTcomment{Scientific Papers}.
@ -114,12 +114,15 @@ text\<open>
\<^emph>\<open>is-a\<close> relation between classes; \<^emph>\<open>is-a\<close> relation between classes;
\<^item> classes may refer to other classes via a regular expression in a \<^item> classes may refer to other classes via a regular expression in a
\<^emph>\<open>where\<close> clause; \<^emph>\<open>where\<close> clause;
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
\<^item> attributes may have default values in order to facilitate notation. \<^item> attributes may have default values in order to facilitate notation.
\<close> \<close>
text\<open> text\<open>
The \<^isadof> ontology specification language consists basically on a notation for document classes, The \<^isadof> ontology specification language consists basically on a notation for document classes,
where the attributes were typed with HOL-types and can be instantiated by terms HOL-terms, \<^ie>, where the attributes were typed with HOL-types and can be instantiated by HOL-terms, \<^ie>,
the actual parsers and type-checkers of the Isabelle system were reused. This has the particular the actual parsers and type-checkers of the Isabelle system were reused. This has the particular
advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the
machinery for type declarations and term specifications such machinery for type declarations and term specifications such
@ -146,6 +149,9 @@ text\<open>
classes and their inheritance relation structure meta-data of text-elements in an object-oriented classes and their inheritance relation structure meta-data of text-elements in an object-oriented
manner, monitor classes enforce structural organization of documents via the language specified manner, monitor classes enforce structural organization of documents via the language specified
by the regular expression enforcing a sequence of text-elements. by the regular expression enforcing a sequence of text-elements.
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types. A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types.
Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>, Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,
@ -153,7 +159,7 @@ text\<open>
\<^boxed_theory_text>\<open>_ option\<close>, \<^boxed_theory_text>\<open>_ list\<close>, \<^boxed_theory_text>\<open>_ set\<close>, or products \<^boxed_theory_text>\<open>_ option\<close>, \<^boxed_theory_text>\<open>_ list\<close>, \<^boxed_theory_text>\<open>_ set\<close>, or products
\<^boxed_theory_text>\<open>_ \<times> _\<close>. As a consequence of the \<^boxed_theory_text>\<open>_ \<times> _\<close>. As a consequence of the
document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions. document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions.
Finally, document class definitions result in themselves in a HOL-types in order to allow \<^emph>\<open>links\<close> Finally, document class definitions result in themselves in a HOL-type in order to allow \<^emph>\<open>links\<close>
to and between ontological concepts. to and between ontological concepts.
\<close> \<close>
@ -167,10 +173,13 @@ text\<open>
in \<^isadof>: in \<^isadof>:
\<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close> \<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close>
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
(called \<open>short_id\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers (called \<open>short_ident\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
details). details).
% TODO
% This phrase should be reviewed to clarify identifiers.
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close> \<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close> \<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"}) \<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
@ -230,7 +239,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close> \<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close> \<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close> \<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
An invariants can be specified as predicate over document classes represented as Invariants can be specified as predicates over document classes represented as
records in HOL. Note that sufficient type information must be provided in order to records in HOL. Note that sufficient type information must be provided in order to
disambiguate the argument of the \<open>\<lambda>\<close>-expression. disambiguate the argument of the \<open>\<lambda>\<close>-expression.
\<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close> \<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
@ -251,10 +260,10 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
text\<open> text\<open>
\<^isadof> provides a default document representation (\<^ie>, content and layout of the generated \<^isadof> provides a default document representation (\<^ie>, content and layout of the generated
PDF) that only prints the main text, omitting all attributes. \<^isadof> provides the PDF) that only prints the main text, omitting all attributes. \<^isadof> provides the
\inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\inlineltx{\newisadof}\<close>\<^index>\<open>document class!PDF\<close> \inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\<^boxed_latex>\<open>\newisadof\<close>\<close>\<^index>\<open>document class!PDF\<close>
command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document
class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific
highlighting, printing of certain attributes), it can also generate entries in in the table of highlighting, printing of certain attributes), it can also generate entries in the table of
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
of the \<^boxed_theory_text>\<open>doc_class\<close>-command: of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
@ -269,18 +278,20 @@ text\<open>
The \<open>class_id\<close> is the full-qualified name of the document class and the list of \<open>attribute_decl\<close> The \<open>class_id\<close> is the full-qualified name of the document class and the list of \<open>attribute_decl\<close>
needs to declare all attributes of the document class. Within the \<^LaTeX>-definition of the document needs to declare all attributes of the document class. Within the \<^LaTeX>-definition of the document
class representation, the identifier \inlineltx|#1| refers to the content of the main text of the class representation, the identifier \<^boxed_latex>\<open>#1\<close> refers to the content of the main text of the
document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced
by their name using the \inlineltx|\commandkey{...}|-command (see the documentation of the by their name using the \inlineltx|\commandkey{...}|-command (see the documentation of the
\<^LaTeX>-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the \<^LaTeX>-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
representations definition needs to be wrapped in a representations definition needs to be wrapped in a
\inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context \inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context
within Isabelle's \<^LaTeX>-setup. within Isabelle's \<^LaTeX>-setup.
(* % TODO:
% For the "(written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>" part, to give some examples should be clearer.
*)
Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|: Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
\<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\inlineltx{\renewisadof}\<close> for re-defining \<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\<^boxed_latex>\<open>\renewisadof\<close>\<close> for re-defining
(over-writing) an already defined command, and (over-writing) an already defined command, and
\<^item> \inlineltx|\provideisadof{}[]{}|\<^index>\<open>provideisadof@\inlineltx{\provideisadof}\<close> for providing \<^item> \inlineltx|\provideisadof{}[]{}|\<^index>\<open>provideisadof@\<^boxed_latex>\<open>\provideisadof\<close>\<close> for providing
a definition if it is not yet defined. a definition if it is not yet defined.
\<close> \<close>
text\<open> text\<open>
@ -289,7 +300,7 @@ text\<open>
underscore ``\_'') that do have a special meaning in \<^LaTeX>. underscore ``\_'') that do have a special meaning in \<^LaTeX>.
Moreover, as usual, special care has to be taken for commands that write into aux-files Moreover, as usual, special care has to be taken for commands that write into aux-files
that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested
reader, in general, to the style files provided in the \<^isadof> distribution. In particular reader to the style files provided in the \<^isadof> distribution. In particular
the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the
file \<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting file \<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting
special characters in definitions that need to make use of a entries in an aux-file. special characters in definitions that need to make use of a entries in an aux-file.
@ -339,7 +350,7 @@ layout (such as \<^LaTeX>); these commands have to be wrapped into
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close> \<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
subsection\<open>Ontologic Text-Elements and their Management\<close> subsection\<open>Ontologic Text-Elements and their Management\<close>
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open>\<open>\<close> \<dots> text \<dots> \<open>\<close>\<close> \<close> is the core-command of \<^isadof>: it permits to create text\<open> \<^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 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. 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 and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
@ -360,8 +371,6 @@ For a declared class \<^theory_text>\<open>cid\<close>, there exists a text anti
The precise presentation is decided in the \<^emph>\<open>layout definitions\<close>, for example by suitable The precise presentation is decided in the \<^emph>\<open>layout definitions\<close>, for example by suitable
\<^LaTeX>-template code. Declared but not yet defined instances must be referenced with a particular \<^LaTeX>-template code. Declared but not yet defined instances must be referenced with a particular
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>. pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
% there should also exist a *term* antiquotation ...
\<close> \<close>
(*<*) (*<*)
@ -377,12 +386,12 @@ text\<open>\<^isadof> provides a number of inspection commands.
\<^item> \<^theory_text>\<open>print_doc_items\<close> allows to view the status of the internal \<^item> \<^theory_text>\<open>print_doc_items\<close> allows to view the status of the internal
object-table of text-elements that were tracked, and object-table of text-elements that were tracked, and
\<^item> \<^theory_text>\<open>check_doc_global\<close> checks if all declared object references have been \<^item> \<^theory_text>\<open>check_doc_global\<close> checks if all declared object references have been
defined, and all monitors are in a final state and final invariant checks defined, all monitors are in a final state, and checks the final invariant
on all objects are satisfied (cf. @{technical (unchecked) \<open>sec:advanced\<close>}) on all objects (cf. @{technical (unchecked) \<open>sec:advanced\<close>})
\<close> \<close>
subsection\<open>Macros\<close> subsection\<open>Macros\<close>
text\<open>There is a mechanism to define document-local short-cuts and macros which text\<open>There is a mechanism to define document-local macros which
were PIDE-supported but lead to an expansion in the integrated source; this feature were PIDE-supported but lead to an expansion in the integrated source; this feature
can be used to define can be used to define
\<^item> \<^theory_text>\<open>shortcuts\<close>, \<^ie>, short names that were expanded to, for example, \<^item> \<^theory_text>\<open>shortcuts\<close>, \<^ie>, short names that were expanded to, for example,
@ -390,7 +399,7 @@ can be used to define
\<^item> \<^theory_text>\<open>macro\<close>'s (= parameterized short-cuts), which allow for \<^item> \<^theory_text>\<open>macro\<close>'s (= parameterized short-cuts), which allow for
passing an argument to the expansion mechanism. passing an argument to the expansion mechanism.
\<close> \<close>
text\<open>Note that the argument can be checked by an own SML-function with respect to syntactic text\<open>The argument can be checked by an own SML-function with respect to syntactic
as well as semantic regards; however, the latter feature is currently only accessible at as well as semantic regards; however, the latter feature is currently only accessible at
the SML level and not directly in the Isar language. We would like to stress, that this the SML level and not directly in the Isar language. We would like to stress, that this
feature is basically an abstract interface to existing Isabelle functionality in the document feature is basically an abstract interface to existing Isabelle functionality in the document
@ -431,11 +440,10 @@ ML\<open>writeln (DOF_core.print_doc_class_tree @{context} (fn (n,l) => String.i
text\<open> text\<open>
\<^isadof> provides a Common Ontology Library (COL)\<^index>\<open>Common Ontology Library@see COL\<close> \<^isadof> provides a Common Ontology Library (COL)\<^index>\<open>Common Ontology Library@see COL\<close>
\<^bindex>\<open>COL\<close> \<^footnote>\<open>contained in \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>\<close> \<^bindex>\<open>COL\<close> \<^footnote>\<open>contained in \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>\<close>
that introduces several ontology root concepts such as common text-elements and that introduces several ontology concepts; its overall class-tree it provides looks as follows:
figures. The overall class-tree it provides looks as follows:
% %
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.0 . .0 .
.1 Isa\_COL.text\_element. .1 Isa\_COL.text\_element.
@ -453,8 +461,7 @@ text\<open>
text\<open> text\<open>
In particular it defines the super-class \<^boxed_theory_text>\<open>text_element\<close>: the root of all In particular it defines the super-class \<^boxed_theory_text>\<open>text_element\<close>: the root of all
text-elements, text-elements:
@{boxed_theory_text [display]\<open> @{boxed_theory_text [display]\<open>
doc_class text_element = doc_class text_element =
level :: "int option" <= "None" level :: "int option" <= "None"
@ -464,12 +471,12 @@ doc_class text_element =
As mentioned in @{technical \<open>sss\<close>} (without explaining the origin of \<^typ>\<open>text_element\<close>) As mentioned in @{technical \<open>sss\<close>} (without explaining the origin of \<^typ>\<open>text_element\<close>)
, \<^boxed_theory_text>\<open>level\<close> defines the section-level (\<^eg>, using a \<^LaTeX>-inspired hierarchy: , \<^boxed_theory_text>\<open>level\<close> defines the section-level (\<^eg>, using a \<^LaTeX>-inspired hierarchy:
from \<^boxed_theory_text>\<open>Some -1\<close> (corresponding to \inlineltx|\part|) to from \<^boxed_theory_text>\<open>Some -1\<close> (corresponding to \<^boxed_latex>\<open>\part\<close>) to
\<^boxed_theory_text>\<open>Some 0\<close> (corresponding to \inlineltx|\chapter|, respectively, \<^boxed_theory_text>\<open>chapter*\<close>) \<^boxed_theory_text>\<open>Some 0\<close> (corresponding to \<^boxed_latex>\<open>\chapter\<close>, respectively, \<^boxed_theory_text>\<open>chapter*\<close>)
to \<^boxed_theory_text>\<open>Some 3\<close> (corresponding to \inlineltx|\subsubsection|, respectively, to \<^boxed_theory_text>\<open>Some 3\<close> (corresponding to \<^boxed_latex>\<open>\subsubsection\<close>, respectively,
\<^boxed_theory_text>\<open>subsubsection*\<close>). Using an invariant, a derived ontology could, \<^eg>, require that \<^boxed_theory_text>\<open>subsubsection*\<close>). Using an invariant, a derived ontology could, \<^eg>, require that
any sequence of technical-elements must be introduced by a text-element with a higher level any sequence of technical-elements must be introduced by a text-element with a higher level
(this would require that technical text section are introduce by a section element). (this requires that technical text section are introduce by a section element).
The attribute \<^term>\<open>referentiable\<close> captures the information if a text-element can be target The attribute \<^term>\<open>referentiable\<close> captures the information if a text-element can be target
for a reference, which is the case for sections or subsections, for example, but not arbitrary for a reference, which is the case for sections or subsections, for example, but not arbitrary
@ -477,11 +484,9 @@ elements such as, \<^ie>, paragraphs (this mirrors restrictions of the target \<
The attribute \<^term>\<open>variants\<close> refers to an Isabelle-configuration attribute that permits The attribute \<^term>\<open>variants\<close> refers to an Isabelle-configuration attribute that permits
to steer the different versions a \<^LaTeX>-presentation of the integrated source. to steer the different versions a \<^LaTeX>-presentation of the integrated source.
For further information of the root classes such as \<^typ>\<open>figure\<close>'s, please consult the ontology For further information of the root classes such as \<^typ>\<open>figure\<close>'s, please consult the ontology
\<^theory>\<open>Isabelle_DOF.Isa_COL\<close> directly. \<^theory>\<open>Isabelle_DOF.Isa_COL\<close> directly. COL finally provides macros that extend the command-language
of the DOF-core by the following
COL finally provides macros that extend the command-language of the DOF-core by the following
abbreviations: abbreviations:
\<^item> \<open>derived_text_element\<close> : \<^item> \<open>derived_text_element\<close> :
@ -516,7 +521,7 @@ text\<open> The \<^verbatim>\<open>scholarly_paper\<close> ontology is oriented
It extends \<^verbatim>\<open>COL\<close> by the following concepts: It extends \<^verbatim>\<open>COL\<close> by the following concepts:
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.0 . .0 .
.1 scholarly\_paper.title. .1 scholarly\_paper.title.
@ -555,10 +560,10 @@ It extends \<^verbatim>\<open>COL\<close> by the following concepts:
} }
\end{minipage} \end{minipage}
\end{center} \end{center}
TODO: There are some slight problems in the hierarchy ...
\<close> \<close>
(*
TODO: There are some slight problems in the hierarchy ...
*)
text\<open>A pivotal abstract class in the hierarchy is: text\<open>A pivotal abstract class in the hierarchy is:
@{boxed_theory_text [display] @{boxed_theory_text [display]
@ -692,7 +697,7 @@ high-level arranged at root-class level,
% %
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.0 . .0 .
.1 technical\_report.front\_matter\DTcomment{...}. .1 technical\_report.front\_matter\DTcomment{...}.
@ -726,7 +731,7 @@ appropriate for this type of long-and-tedious documents,
% %
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.0 . .0 .
.1 CENELEC\_50128.judgement\DTcomment{...}. .1 CENELEC\_50128.judgement\DTcomment{...}.
@ -790,7 +795,7 @@ doc_class EC = AC +
We now define the document representations, in the file We now define the document representations, in the file
\<^file>\<open>../../../src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty\<close>. Let us assume that we want to \<^file>\<open>../../../src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty\<close>. Let us assume that we want to
register the definition of EC's in a dedicated table of contents (\inlineltx{tos}) register the definition of EC's in a dedicated table of contents (\<^boxed_latex>\<open>tos\<close>)
and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for their graphical and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for their graphical
representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the
full-qualified names, \<^eg>, \<^boxed_theory_text>\<open>text.CENELEC_50128.EC\<close> for the document class and full-qualified names, \<^eg>, \<^boxed_theory_text>\<open>text.CENELEC_50128.EC\<close> for the document class and
@ -881,7 +886,7 @@ schemata:
\end{ltx} \end{ltx}
After the definition of the dispatcher, one can, optionally, define a custom representation After the definition of the dispatcher, one can, optionally, define a custom representation
using the \inlineltx|newisadof|-command, as introduced in the previous section: using the \<^boxed_latex>\<open>newisadof\<close>-command, as introduced in the previous section:
\begin{ltx} \begin{ltx}
\newisadof{section}[label=,type=][1]{% \newisadof{section}[label=,type=][1]{%
@ -1031,15 +1036,15 @@ section*[infrastructure::technical]\<open>Technical Infrastructure\<close>
text\<open> text\<open>
The list of fully supported (\<^ie>, supporting both interactive ontological modeling and The list of fully supported (\<^ie>, supporting both interactive ontological modeling and
document generation) ontologies and the list of supported document templates can be document generation) ontologies and the list of supported document templates can be
obtained by calling \inlinebash|isabelle mkroot_DOF -h| (see \<^technical>\<open>first_project\<close>). obtained by calling \<^boxed_bash>\<open>isabelle mkroot_DOF -h\<close> (see \<^technical>\<open>first_project\<close>).
Note that the postfix \inlinebash|-UNSUPPORTED| denotes experimental ontologies or templates Note that the postfix \<^boxed_bash>\<open>-UNSUPPORTED\<close> denotes experimental ontologies or templates
for which further manual setup steps might be required or that are not fully tested. Also note 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 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 system. This is mostly a problem for publisher specific templates (\<^eg>, Springer's
\<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions. \<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
\<close> \<close>
subsection\<open>Developing Ontologies and their Represenation Mappings\<close> subsection\<open>Developing Ontologies and their Representation Mappings\<close>
text\<open> text\<open>
The document core \<^emph>\<open>may\<close>, but \<^emph>\<open>must\<close> not use Isabelle definitions or proofs for checking the The document core \<^emph>\<open>may\<close>, but \<^emph>\<open>must\<close> not use Isabelle definitions or proofs for checking the
formal content---this manual is actually an example of a document not containing any proof. formal content---this manual is actually an example of a document not containing any proof.
@ -1054,10 +1059,10 @@ text\<open>
the Isabelle proof language, for example, or other more advanced concepts. the Isabelle proof language, for example, or other more advanced concepts.
Technically, ontologies\<^index>\<open>ontology!directory structure\<close> are stored in a directory Technically, ontologies\<^index>\<open>ontology!directory structure\<close> are stored in a directory
\inlinebash|src/ontologies| and consist of a Isabelle theory file and a \<^LaTeX> -style file: \<^boxed_bash>\<open>src/ontologies\<close> and consist of a Isabelle theory file and a \<^LaTeX> -style file:
% %
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.1 . .1 .
.2 src. .2 src.
@ -1078,9 +1083,9 @@ text\<open>
\end{center} \end{center}
\<close> \<close>
text\<open> text\<open>
Developing a new ontology ``\inlinebash|foo|'' requires, from a technical perspective, the Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires, from a technical perspective, the
following steps: following steps:
\<^item> create a new sub-directory \inlinebash|foo| in the directory \inlinebash|src/ontologies| \<^item> create a new sub-directory \<^boxed_bash>\<open>foo\<close> in the directory \<^boxed_bash>\<open>src/ontologies\<close>
\<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in \<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in
a new theory file \<^path>\<open>src/ontologies/foo/foo.thy\<close>. a new theory file \<^path>\<open>src/ontologies/foo/foo.thy\<close>.
\<^item> definition of the document representation for the ontological concepts in a \LaTeX-style \<^item> definition of the document representation for the ontological concepts in a \LaTeX-style
@ -1089,11 +1094,8 @@ text\<open>
\<^path>\<open>src/ontologies/ontologies.thy\<close>. \<^path>\<open>src/ontologies/ontologies.thy\<close>.
\<^item> activation of the new document setup by executing the install script. You can skip the lengthy \<^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 checks for the AFP entries and the installation of the Isabelle patch by using the
\inlinebash|--skip-patch-and-afp| option: \<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
\begin{bash}
ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp
\end{bash}
\<close> \<close>
subsection\<open>Document Templates\<close> subsection\<open>Document Templates\<close>
@ -1104,7 +1106,7 @@ text\<open>
are stored in a directory are stored in a directory
\<^path>\<open>src/document-templates\<close>:\<^index>\<open>document template!directory structure\<close> \<^path>\<open>src/document-templates\<close>:\<^index>\<open>document template!directory structure\<close>
\begin{center} \begin{center}
\begin{minipage}{.9\textwidth} \begin{minipage}{.9\textwidth}\small
\dirtree{% \dirtree{%
.1 . .1 .
.2 src. .2 src.
@ -1119,22 +1121,18 @@ text\<open>
\<close> \<close>
text\<open> text\<open>
Developing a new document template ``\inlinebash|bar|'' requires the following steps: Developing a new document template ``\<^boxed_bash>\<open>bar\<close>'' requires the following steps:
\<^item> develop a new \<^LaTeX>-template \inlinebash|src/document-templates/root-bar.tex| \<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
\<^item> activation of the new document template by executing the install script. You can skip the lengthy \<^item> activation of the new document template 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 checks for the AFP entries and the installation of the Isabelle patch by using the
\inlinebash|--skip-patch-and-afp| option: \<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
\begin{bash}
ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp
\end{bash}
\<close> \<close>
text\<open> text\<open>
As the document generation of \<^isadof> is based As the document generation of \<^isadof> is based on \<^LaTeX>, the \<^isadof> document templates can (and
on \<^LaTeX>, the \<^isadof> document templates can (and should) make use of any \<^LaTeX>-classes provided should) make use of any \<^LaTeX>-classes provided by publishers or standardization bodies.
by publishers or standardization bodies.
\<close> \<close>
@ -1155,7 +1153,7 @@ text\<open>
Moreover, you might want to add/modify the template specific configuration Moreover, you might want to add/modify the template specific configuration
(\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in (\autoref{lst:config-start}-\ref{lst:config-end}). The new template should be stored in
\<^path>\<open>src/document-templates\<close> and its file name should start with the prefix \<^path>\<open>root-\<close>. After \<^path>\<open>src/document-templates\<close> and its file name should start with the prefix \<^path>\<open>root-\<close>. After
adding a new template, call the \inlinebash{install} script (see \<^technical>\<open>infrastructure\<close> adding a new template, call the \<^boxed_bash>\<open>install\<close> script (see \<^technical>\<open>infrastructure\<close>
The common structure of an \<^isadof> document template looks as follows: The common structure of an \<^isadof> document template looks as follows:
\begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm] \begin{ltx}[escapechar=ë, numbers=left,numberstyle=\tiny,xleftmargin=5mm]
@ -1194,25 +1192,22 @@ text\<open>
subsection\<open>Tips, Tricks, and Known Limitations\<close> subsection\<open>Tips, Tricks, and Known Limitations\<close>
text\<open> text\<open>
In this sectin, we sill discuss several tips and tricks for developing In this section, we will discuss several tips and tricks for developing
new or adapting existing document templates or \<^LaTeX>-represenations of ontologies. new or adapting existing document templates or \<^LaTeX>-representations of ontologies.
\<close> \<close>
subsubsection\<open>Getting Started\<close> subsubsection\<open>Getting Started\<close>
text\<open> text\<open>
In general, we recommend to create a test project (\<^eg>, using \inlinebash|isabelle mkroot_DOF|) In general, we recommend to create a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
to develop new document templates or ontology representations. The default setup of the \<^isadof> to develop new document templates or ontology representations. The default setup of the \<^isadof>
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>: this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:
@{boxed_bash [display] \<open>ë\prompt{MyProject/output/document}ë lualatex root.tex\<close>}
\begin{bash}
ë\prompt{MyProject/output/document}ë pdflatex root.tex
\end{bash}
This allows you to develop and check your \<^LaTeX>-setup without the overhead of running This allows you to develop and check your \<^LaTeX>-setup without the overhead of running
\inlinebash|isabelle build| after each change of your template (or ontology-style). Note that \<^boxed_bash>\<open>isabelle build\<close> after each change of your template (or ontology-style). Note that
the content of the \<^path>\<open>output\<close> directory is overwritten by executing the content of the \<^path>\<open>output\<close> directory is overwritten by executing
\inlinebash|isabelle build|. \<^boxed_bash>\<open>isabelle build\<close>.
\<close> \<close>
subsubsection\<open>Truncated Warning and Error Messages\<close> subsubsection\<open>Truncated Warning and Error Messages\<close>
@ -1220,12 +1215,9 @@ text\<open>
By default, \<^LaTeX> cuts of many warning or error messages after 79 characters. Due to the By default, \<^LaTeX> cuts of many warning or error messages after 79 characters. Due to the
use of full-qualified names in \<^isadof>, this can often result in important information being use of full-qualified names in \<^isadof>, this can often result in important information being
cut off. Thus, it can be very helpful to configure \<^LaTeX> in such a way that it prints cut off. Thus, it can be very helpful to configure \<^LaTeX> in such a way that it prints
long error or warning messages. This can easily be done on the command line for individual long error or warning messages. This can easily be done for individual
\<^LaTeX> invocations: \<^LaTeX> invocations:
@{boxed_bash [display] \<open>ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100 lualatex root.tex\<close>}
\begin{bash}
ë\prompt{MyProject/output/document}ë max_print_line=200 error_line=200 half_error_line=100 pdflatex root.tex
\end{bash}
\<close> \<close>
subsubsection\<open>Deferred Declaration of Information\<close> subsubsection\<open>Deferred Declaration of Information\<close>
@ -1260,7 +1252,7 @@ text\<open>
\<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> contains an example that, firstly, \<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> contains an example that, firstly,
shows how to write the author and affiliation information into the auxiliary file for re-use shows how to write the author and affiliation information into the auxiliary file for re-use
in the next \<^LaTeX>-run and, secondly, shows how to collect the author and affiliation in the next \<^LaTeX>-run and, secondly, shows how to collect the author and affiliation
information into an \inlineltx|\author| and a \inlineltx|\institution| statement, each of information into an \<^boxed_latex>\<open>\author\<close> and a \<^boxed_latex>\<open>\institution\<close> statement, each of
which containing the information for all authors. The collection of the author information which containing the information for all authors. The collection of the author information
is provided by the following \<^LaTeX>-code: is provided by the following \<^LaTeX>-code:
@ -1280,13 +1272,12 @@ text\<open>
} }
\end{ltx} \end{ltx}
The new command \inlineltx|\addauthor| and a similarly defined command \inlineltx|\addaffiliation| The new command \<^boxed_latex>\<open>\addauthor\<close> and a similarly defined command \<^boxed_latex>\<open>\addaffiliation\<close>
can now be used in the definition of the representation of the concept can now be used in the definition of the representation of the concept
\<^boxed_theory_text>\<open>text.scholarly_paper.author\<close>, which writes the collected information in the \<^boxed_theory_text>\<open>text.scholarly_paper.author\<close>, which writes the collected information in the
job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary, job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary,
as the author and affiliation information is required right at the begin of the document as the author and affiliation information is required right at the begin of the document
(\<^ie>, when \<^LaTeX>'s \inlineltx|\maketitle| is invoked) while \<^isadof> allows to define authors at while \<^isadof> allows to define authors at any place within a document:
any place within a document:
\begin{ltx} \begin{ltx}
\provideisadof{text.scholarly_paper.author}% \provideisadof{text.scholarly_paper.author}%
@ -1313,8 +1304,8 @@ any place within a document:
} }
\end{ltx} \end{ltx}
Finally, the collected information is used in the \inlineltx|\author| command using the Finally, the collected information is used in the \<^boxed_latex>\<open>\author\<close> command using the
\inlineltx|AtBeginDocument|-hook: \<^boxed_latex>\<open>AtBeginDocument\<close>-hook:
\begin{ltx} \begin{ltx}
\newcommand{\DOFauthor}{\author{\dof@author}} \newcommand{\DOFauthor}{\author{\dof@author}}
@ -1350,7 +1341,7 @@ text\<open>
inherited ontologies to overwrite these restrictions and, therefore, to provide also support inherited ontologies to overwrite these restrictions and, therefore, to provide also support
for additional document templates. For example, the ontology \<^boxed_theory_text>\<open>technical_report\<close> for additional document templates. For example, the ontology \<^boxed_theory_text>\<open>technical_report\<close>
extends the \<^boxed_theory_text>\<open>scholarly_paper\<close> ontology and its \<^LaTeX> supports provides support extends the \<^boxed_theory_text>\<open>scholarly_paper\<close> ontology and its \<^LaTeX> supports provides support
for the \inlineltx|scrrept|-class which is not supported by the \<^LaTeX> support for for the \<^boxed_latex>\<open>scrrept\<close>-class which is not supported by the \<^LaTeX> support for
\<^boxed_theory_text>\<open>scholarly_paper\<close>. \<^boxed_theory_text>\<open>scholarly_paper\<close>.
\<close> \<close>
@ -1362,7 +1353,6 @@ text\<open>
\<close> \<close>
(*<*) (*<*)
end end
(*>*) (*>*)

128
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019-2020 University of Exeter * 2019-2021 University of Exeter
* 2018-2019 University of Paris-Saclay * 2018-2021 University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -41,74 +41,55 @@ text\<open>
IDE support. IDE support.
\<close> \<close>
(* should work as text*, but doesn't. *) section\<open>\<^isadof>: A User-Defined Plugin in Isabelle/Isar\<close>
(* text\<open>
text*[xxx::SML] A plugin in Isabelle starts with defining the local data and registering it in the framework. As
mentioned before, contexts are structures with independent cells/compartments having three
primitives \<^boxed_sml>\<open>init\<close>, \<^boxed_sml>\<open>extend\<close> and \<^boxed_sml>\<open>merge\<close>. Technically this is done by
instantiating a functor \<^boxed_sml>\<open>Generic_Data\<close>, and the following fairly typical code-fragment
is drawn from \<^isadof>:
@{boxed_sml [display]
\<open>structure Data = Generic_Data \<open>structure Data = Generic_Data
( type T = docobj_tab * docclass_tab * ... ( type T = docobj_tab * docclass_tab * ...
val empty = (initial_docobj_tab, initial_docclass_tab, ...) val empty = (initial_docobj_tab, initial_docclass_tab, ...)
val extend = I val extend = I
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...)) merge_docclass_tab(c1,c2,...))
); );\<close>}
\<close> where the table \<^boxed_sml>\<open>docobj_tab\<close> manages document classes and \<^boxed_sml>\<open>docclass_tab\<close> the
*)
section\<open>\<^isadof>: A User-Defined Plugin in Isabelle/Isar\<close>
text\<open>
A plugin in Isabelle starts with defining the local data and registering it in the framework. As
mentioned before, contexts are structures with independent cells/compartments having three
primitives \inlinesml+init+, \inlinesml+extend+ and \inlinesml+merge+. Technically this is done by
instantiating a functor \inlinesml+Generic_Data+, and the following fairly typical code-fragment
is drawn from \<^isadof>:
\begin{sml}
structure Data = Generic_Data
( type T = docobj_tab * docclass_tab * ...
val empty = (initial_docobj_tab, initial_docclass_tab, ...)
val extend = I
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...))
);
\end{sml}
where the table \inlinesml+docobj_tab+ manages document classes and \inlinesml+docclass_tab+ the
environment for class definitions (inducing the inheritance relation). Other tables capture, \eg, environment for class definitions (inducing the inheritance relation). Other tables capture, \eg,
the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where
Isabelle/Isar provides the controller part. A typical model operation has the type: Isabelle/Isar provides the controller part. A typical model operation has the type:
\begin{sml} @{boxed_sml [display]
val opn :: <args_type> -> Context.generic -> Context.generic \<open>val opn :: <args_type> -> Context.generic -> Context.generic\<close>}
\end{sml}
representing a transformation on system contexts. For example, the operation of declaring a local representing a transformation on system contexts. For example, the operation of declaring a local
reference in the context is presented as follows: reference in the context is presented as follows:
\begin{sml} @{boxed_sml [display]
fun declare_object_local oid ctxt = \<open>fun declare_object_local oid ctxt =
let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab,
maxano=maxano} maxano=maxano}
in (Data.map(apfst decl)(ctxt) in (Data.map(apfst decl)(ctxt)
handle Symtab.DUP _ => handle Symtab.DUP _ =>
error("multiple declaration of document reference")) error("multiple declaration of document reference"))
end end\<close>}
\end{sml}
where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the
functor \inlinesml|Generic_Data|. This code fragment uses operations from a library structure functor \<^boxed_sml>\<open>Generic_Data\<close>. This code fragment uses operations from a library structure
\inlinesml+Symtab+ that were used to update the appropriate table for document objects in \<^boxed_sml>\<open>Symtab\<close> that were used to update the appropriate table for document objects in
the plugin-local state. Possible exceptions to the update operation were mapped to a system-global the plugin-local state. Possible exceptions to the update operation were mapped to a system-global
error reporting function. error reporting function.
Finally, the view-aspects were handled by an API for parsing-combinators. The library structure Finally, the view-aspects were handled by an API for parsing-combinators. The library structure
\inlinesml+Scan+ provides the operators: \<^boxed_sml>\<open>Scan\<close> provides the operators:
\begin{sml} @{boxed_sml [display]
op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b \<open>op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
\end{sml}
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
combinators have the advantage that they can be smoothlessly integrated into standard programs, combinators have the advantage that they can be smoothlessly integrated into standard programs,
and they enable the dynamic extension of the grammar. There is a more high-level structure and they enable the dynamic extension of the grammar. There is a more high-level structure
@ -128,13 +109,12 @@ val attributes =(Parse.$$$ "[" |-- (reference
The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were
combined via the piping operator and registered in the Isar toplevel: combined via the piping operator and registered in the Isar toplevel:
\begin{sml} @{boxed_sml [display]
fun declare_reference_opn (((oid,_),_),_) = \<open>fun declare_reference_opn (((oid,_),_),_) =
(Toplevel.theory (DOF_core.declare_object_global oid)) (Toplevel.theory (DOF_core.declare_object_global oid))
val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"} val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"}
"declare document reference" "declare document reference"
(attributes >> declare_reference_opn); (attributes >> declare_reference_opn);\<close>}
\end{sml}
Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the
new \emph{command}: new \emph{command}:
@ -154,14 +134,13 @@ text\<open>
principle: based on a number of combinators, new user-defined antiquotation syntax and semantics principle: based on a number of combinators, new user-defined antiquotation syntax and semantics
can be added to the system that works on the internal plugin-data freely. For example, in can be added to the system that works on the internal plugin-data freely. For example, in
\begin{sml} @{boxed_sml [display]
val _ = Theory.setup( \<open>val _ = Theory.setup(
Thy_Output.antiquotation <@>{binding docitem} Thy_Output.antiquotation <@>{binding docitem}
docitem_antiq_parser docitem_antiq_parser
(docitem_antiq_gen default_cid) #> (docitem_antiq_gen default_cid) #>
ML_Antiquotation.inline <@>{binding docitem_value} ML_Antiquotation.inline <@>{binding docitem_value}
ML_antiq_docitem_value) ML_antiq_docitem_value)\<close>}
\end{sml}
the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument
syntax and the overall semantics. This code defines a generic antiquotation to be used in text syntax and the overall semantics. This code defines a generic antiquotation to be used in text
elements such as elements such as
@ -188,9 +167,8 @@ text\<open>
late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
(ISA's), a function of type (ISA's), a function of type
\begin{sml} @{boxed_sml [display]
theory -> term * typ * Position.T -> term option \<open> theory -> term * typ * Position.T -> term option\<close>}
\end{sml}
Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\<open>None\<close>. This is Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\<open>None\<close>. This is
adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\<open>theory\<close>; adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\<open>theory\<close>;
@ -205,8 +183,8 @@ text\<open>
For the moment, there is no high-level syntax for the definition of class invariants. A For the moment, there is no high-level syntax for the definition of class invariants. A
formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward: formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
\begin{sml} @{boxed_sml [display]
fun check_result_inv oid {is_monitor:bool} ctxt = \<open>fun check_result_inv oid {is_monitor:bool} ctxt =
let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here} let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here} val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
val tS = HOLogic.dest_list prop val tS = HOLogic.dest_list prop
@ -216,10 +194,9 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
| _ => false | _ => false
end end
val _ = Theory.setup (DOF_core.update_class_invariant val _ = Theory.setup (DOF_core.update_class_invariant
"tiny_cert.result" check_result_inv) "tiny_cert.result" check_result_inv)\<close>}
\end{sml}
The \inlinesml{setup}-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function The \<^boxed_sml>\<open>setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
into the \<^isadof> kernel, which activates any creation or modification of an instance of into the \<^isadof> kernel, which activates any creation or modification of an instance of
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding \<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding
antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
@ -232,10 +209,9 @@ text\<open>
deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects
in the \<^isadof> component. We implemented the functions: in the \<^isadof> component. We implemented the functions:
\begin{sml} @{boxed_sml [display]
val enabled : automaton -> env -> cid list \<open> val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton val next : automaton -> env -> cid -> automaton\<close>}
\end{sml}
where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's
(\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id, (\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
@ -252,41 +228,38 @@ text\<open>
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands ``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands
are just wrappers for the corresponding commands from the keycommand package: are just wrappers for the corresponding commands from the keycommand package:
\begin{ltx} @{boxed_latex [display]
\newcommand\newisadof[1]{% \<open>\newcommand\newisadof[1]{%
\expandafter\newkeycommand\csname isaDof.#1\endcsname}% \expandafter\newkeycommand\csname isaDof.#1\endcsname}%
\newcommand\renewisadof[1]{% \newcommand\renewisadof[1]{%
\expandafter\renewkeycommand\csname isaDof.#1\endcsname}% \expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
\newcommand\provideisadof[1]{% \newcommand\provideisadof[1]{%
\expandafter\providekeycommand\csname isaDof.#1\endcsname}% \expandafter\providekeycommand\csname isaDof.#1\endcsname}%\<close>}
\end{ltx}
The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall
@{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element, @{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element,
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation. the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation.
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
\begin{ltx} @{boxed_latex [display]
\begin{isamarkuptext*}% \<open>\begin{isamarkuptext*}%
[label = {ass122},type = {CENELEC_50128.SRAC}, [label = {ass122},type = {CENELEC_50128.SRAC},
args={label = {ass122}, type = {CENELEC_50128.SRAC}, args={label = {ass122}, type = {CENELEC_50128.SRAC},
CENELEC_50128.EC.assumption_kind = {formal}} CENELEC_50128.EC.assumption_kind = {formal}}
] The overall sampling frequence of the odometer subsystem is therefore ] The overall sampling frequence of the odometer subsystem is therefore
14 khz, which includes sampling, computing and result communication 14 khz, which includes sampling, computing and result communication
times ... times ...
\end{isamarkuptext*} \end{isamarkuptext*}\<close>}
\end{ltx}
This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}): This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
\begin{ltx} @{boxed_latex [display]
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<open> \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<close>}
\end{ltx}
For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific
implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>: implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
\begin{ltx} @{boxed_latex [display]
%% The Isabelle/DOF dispatcher: \<open>%% The Isabelle/DOF dispatcher:
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% \newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
\ifcsname isaDof.\commandkey{type}\endcsname% \ifcsname isaDof.\commandkey{type}\endcsname%
\csname isaDof.\commandkey{type}\endcsname% \csname isaDof.\commandkey{type}\endcsname%
@ -307,8 +280,7 @@ implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
definition for "\commandkey{env}" available either.}% definition for "\commandkey{env}" available either.}%
\fi% \fi%
\fi% \fi%
} }\<close>}
\end{ltx}
\<close> \<close>
(*<*) (*<*)

1
examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty
View File

@ -184,6 +184,7 @@
\lstdefinestyle{lltx}{language=[AlLaTeX]TeX, \lstdefinestyle{lltx}{language=[AlLaTeX]TeX,
,basicstyle=\ttfamily% ,basicstyle=\ttfamily%
,showspaces=false% ,showspaces=false%
,escapechar=ë
,showlines=false% ,showlines=false%
,morekeywords={newisadof} ,morekeywords={newisadof}
% ,keywordstyle=\bfseries% % ,keywordstyle=\bfseries%

6
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019 The University of Exeter * 2019-2021 The University of Exeter
* 2018-2019 The University of Paris-Saclay * 2018-2021 The University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -1196,7 +1196,7 @@ text\<open>
Registers \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition\<close> parsers to the Registers \<^ML_type>\<open>Toplevel.transition -> Toplevel.transition\<close> parsers to the
Isar interpreter.\<close> Isar interpreter.\<close>
text\<open>The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command definitions, with the text\<open>The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command definitions, with the
all-important theory header declarations for outer syntax keywords.\<close> all-important theory header declarations for outer syntax keywords.\<close>
subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close> subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close>

1
examples/technical_report/TR_my_commented_isabelle/document/preamble.tex
View File

@ -13,6 +13,7 @@
%% This is a placeholder for user-specific configuration and packages. %% This is a placeholder for user-specific configuration and packages.
\renewcommand{\isasymtheta}{\texorpdfstring{\isamath{\vartheta}}{ϑ}}
\usepackage{prooftree} \usepackage{prooftree}
\title{<TITLE>} \title{<TITLE>}
\author{<AUTHOR>} \author{<AUTHOR>}

29
install
View File

@ -84,34 +84,6 @@ check_isabelle_version() {
fi fi
} }
check_pdftex() {
echo "* Checking (La)TeX installation:"
OLDDIR=`pwd`
DIR=`mktemp -d`
cd $DIR;
pdftex -interaction=nonstopmode \\expanded{Success}\\end > /dev/null
if [ $? -eq 0 ]; then
echo " Success: pdftex supports \\expanded{} primitive."
else
cd $OLDDIR
echo " WARNING:"
echo " The version of pdf(La)TeX you are using is outdated (and does"
echo " not support the \\expanded primitive). It is not supported by the"
echo " current version of Isabelle/DOF. Please install a supported TeX"
echo " distribution (e.g., TeXLive 2019 or later)."
echo
read -p " Still continue (y/N)? " -n 1 -r
echo
if [[ $REPLY =~ ^[Yy]$ ]];
then
echo " Continuing installation on your OWN risk."
else
exit_error
fi
fi
cd $OLDDIR
}
check_afp_entries() { check_afp_entries() {
echo "* Checking availability of AFP entries:" echo "* Checking availability of AFP entries:"
missing="" missing=""
@ -286,7 +258,6 @@ echo ""
echo "Isabelle/DOF Installer" echo "Isabelle/DOF Installer"
echo "======================" echo "======================"
check_isabelle_version check_isabelle_version
check_pdftex
if [ "$SKIP" = "true" ]; then if [ "$SKIP" = "true" ]; then
echo "* Warning: skipping installation of Isabelle patch and AFP entries." echo "* Warning: skipping installation of Isabelle patch and AFP entries."
else else

6
src/DOF/Isa_DOF.thy
View File

@ -854,11 +854,13 @@ fun err msg pos = error (msg ^ Position.here pos);
fun check_path check_file ctxt dir (name, pos) = fun check_path check_file ctxt dir (name, pos) =
let let
val _ = Context_Position.report ctxt pos Markup.language_path; val _ = Context_Position.report ctxt pos (Markup.language_path true); (* TODO: pos should be
"lifted" to
type source *)
val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos; val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
val _ = Path.expand path handle ERROR msg => err msg pos; val _ = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
val _ = val _ =
(case check_file of (case check_file of
NONE => path NONE => path

0
src/DOF/latex/DOF-COL.sty Executable file → Normal file
View File

26
src/DOF/latex/DOF-amssymb.sty Normal file
View File

@ -0,0 +1,26 @@
%% Copyright (C) 2021 University of Exeter
%% 2021 University of Paris-Saclay
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-amssymb}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
\usepackage{ifxetex,ifluatex}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
\usepackage{amssymb}
\else % if luatex or xetex
\usepackage{unicode-math}
\usepackage{latexsym}
\fi

0
src/DOF/latex/DOF-core.sty Executable file → Normal file
View File

2
src/document-templates/root-eptcs-UNSUPPORTED.tex
View File

@ -34,7 +34,7 @@
\usepackage{xcolor} \usepackage{xcolor}
\usepackage{isabellesym} \usepackage{isabellesym}
\usepackage{amsmath} \usepackage{amsmath}
\usepackage{amssymb} \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\IfFileExists{DOF-core.sty}{}{% \IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed. \PackageError{DOF-core}{Isabelle/DOF not installed.

2
src/document-templates/root-lipics-v2019-UNSUPPORTED.tex
View File

@ -29,7 +29,7 @@
\usepackage{isabelle} \usepackage{isabelle}
\usepackage{isabellesym} \usepackage{isabellesym}
% \usepackage{amsmath} % \usepackage{amsmath}
% \usepackage{amssymb} % \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\IfFileExists{DOF-core.sty}{}{% \IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed. \PackageError{DOF-core}{Isabelle/DOF not installed.

2
src/document-templates/root-lncs.tex
View File

@ -34,7 +34,7 @@
\usepackage{xcolor} \usepackage{xcolor}
\usepackage{isabellesym} \usepackage{isabellesym}
\usepackage{amsmath} \usepackage{amsmath}
\usepackage{amssymb} \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\IfFileExists{DOF-core.sty}{}{% \IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed. \PackageError{DOF-core}{Isabelle/DOF not installed.

6
src/document-templates/root-scrartcl.tex
View File

@ -22,7 +22,7 @@
%% preamble.tex. %% preamble.tex.
\RequirePackage{ifvtex} \RequirePackage{ifvtex}
\documentclass[fontsize=11pt,DIV=12,paper=a4]{scrartcl} \documentclass[abstract=true,fontsize=11pt,DIV=12,paper=a4]{scrartcl}
\usepackage[T1]{fontenc} \usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc} \usepackage[utf8]{inputenc}
\usepackage{textcomp} \usepackage{textcomp}
@ -44,7 +44,7 @@
\input{ontologies} \input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}% \IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath} \usepackage{amsmath}
\usepackage{amssymb} \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx} \usepackage{graphicx}
\usepackage{hyperref} \usepackage{hyperref}
@ -75,7 +75,7 @@
\begin{document} \begin{document}
\begin{frontmatter} \begin{frontmatter}
\maketitle \maketitle
\tableofcontents % \tableofcontents
\end{frontmatter} \end{frontmatter}
\input{session} \input{session}
% optional bibliography % optional bibliography

2
src/document-templates/root-scrreprt-modern.tex
View File

@ -65,7 +65,7 @@
\input{ontologies} \input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}% \IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath} \usepackage{amsmath}
\usepackage{amssymb} \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx} \usepackage{graphicx}
\usepackage{hyperref} \usepackage{hyperref}

2
src/document-templates/root-scrreprt.tex
View File

@ -44,7 +44,7 @@
\input{ontologies} \input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}% \IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath} \usepackage{amsmath}
\usepackage{amssymb} \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib} \usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx} \usepackage{graphicx}
\usepackage{hyperref} \usepackage{hyperref}

2
src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty
View File

@ -14,7 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax \NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-cenelec_50128} \ProvidesPackage{DOF-cenelec_50128}
[2019/08/18 Unreleased/Isabelle2020% [<isadofltxversion>%
Document-Type Support Framework for Isabelle (CENELEC 50128).] Document-Type Support Framework for Isabelle (CENELEC 50128).]
\RequirePackage{DOF-COL} \RequirePackage{DOF-COL}

2
src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
View File

@ -13,7 +13,7 @@
\NeedsTeXFormat{LaTeX2e}\relax \NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper-thm} \ProvidesPackage{DOF-scholarly_paper-thm}
[2020/01/14 Unreleased/Isabelle2020% [<isadofltxversion>%
Document-Type Support Framework for Isabelle (LNCS).] Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{amsthm} \RequirePackage{amsthm}

2
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -14,7 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax \NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper} \ProvidesPackage{DOF-scholarly_paper}
[2020/01/14 Unreleased/Isabelle2020% [<isadofltxversion>%
Document-Type Support Framework for Isabelle (LNCS).] Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{DOF-COL} \RequirePackage{DOF-COL}

0
src/patches/thy_output.Isabelle2020.ML → src/patches/thy_output.Isabelle2021.ML Executable file → Normal file
View File