forked from Isabelle_DOF/Isabelle_DOF
activated the new markup wherever possible. Started to revise chap 3.
This commit is contained in:
parent
bb68be990b
commit
fd532d985a
|
@ -82,6 +82,13 @@ fun boxed_bash_antiquotation name =
|
||||||
#> DOF_lib.enclose_env ctxt "bash")
|
#> DOF_lib.enclose_env ctxt "bash")
|
||||||
(* the simplest conversion possible *)
|
(* the simplest conversion possible *)
|
||||||
|
|
||||||
|
fun boxed_isar_antiquotation name =
|
||||||
|
DOF_lib.gen_text_antiquotation name (K(K()))
|
||||||
|
(fn ctxt => Input.source_content
|
||||||
|
#> Latex.text
|
||||||
|
#> DOF_lib.enclose_env ctxt "isar")
|
||||||
|
(* the simplest conversion possible *)
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #> *)
|
setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #> *)
|
||||||
|
@ -94,7 +101,9 @@ setup\<open>(* std_text_antiquotation \<^binding>\<open>my_text\<close> #
|
||||||
boxed_sml_text_antiquotation \<^binding>\<open>boxed_sml\<close> #>
|
boxed_sml_text_antiquotation \<^binding>\<open>boxed_sml\<close> #>
|
||||||
boxed_pdf_antiquotation \<^binding>\<open>boxed_pdf\<close> #>
|
boxed_pdf_antiquotation \<^binding>\<open>boxed_pdf\<close> #>
|
||||||
boxed_latex_antiquotation \<^binding>\<open>boxed_latex\<close>#>
|
boxed_latex_antiquotation \<^binding>\<open>boxed_latex\<close>#>
|
||||||
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close>\<close>
|
boxed_bash_antiquotation \<^binding>\<open>boxed_bash\<close> #>
|
||||||
|
boxed_isar_antiquotation \<^binding>\<open>boxed_isar\<close> (* should be replaced by boxed_theory_text*)
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -86,6 +86,9 @@ text\<open>
|
||||||
separating multiple technological layers or languages. To help the reader with this, we
|
separating multiple technological layers or languages. To help the reader with this, we
|
||||||
will type-set the different languages in different styles. In particular, we will use
|
will type-set the different languages in different styles. In particular, we will use
|
||||||
\<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
|
\<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
|
||||||
|
|
||||||
|
\<^boxed_isar>\<open>lemma refl: "x = x"\<close>
|
||||||
|
|
||||||
\begin{isar}
|
\begin{isar}
|
||||||
lemma refl: "x = x"
|
lemma refl: "x = x"
|
||||||
by simp
|
by simp
|
||||||
|
|
|
@ -56,10 +56,12 @@ 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>, \<^emph>\<open>sub-document\<close>,
|
(\<^dof>) in general. In particular we discuss the concepts \<^emph>\<open>integrated document\<close>
|
||||||
\<^emph>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> occurring inside text-elements. Furthermore, we assume two
|
\<^bindex>\<open>integrated document\<close>, \<^emph>\<open>sub-document\<close>, \<^bindex>\<open>sub-document\<close>,
|
||||||
different levels of parsers (for \<^emph>\<open>outer\<close> and \<^emph>\<open>inner syntax\<close>) where the inner-syntax is basically
|
\<^emph>\<open>text-element\<close> \<^bindex>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> \<^bindex>\<open>semantic macros\<close> occurring
|
||||||
a typed \inlineisar|\<lambda>|-calculus and some Higher-order Logic (HOL).
|
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
|
||||||
|
and some Higher-order Logic (HOL)\<^bindex>\<open>HOL\<close>.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
|
@ -76,8 +78,8 @@ text\<open>
|
||||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||||
consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||||
the header consists of a sequence of commands used for introductory text elements not depending on
|
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||||
any context. The context-definition contains an \inlineisar{import} and a
|
any context. The context-definition contains an \<^boxed_isar>\<open>import\<close> and a
|
||||||
\inlineisar{keyword} section, for example:
|
\<^boxed_isar>\<open>keyword\<close> section, for example:
|
||||||
\begin{isar}
|
\begin{isar}
|
||||||
" theory Example (* Name of the 'theory' *)
|
" theory Example (* Name of the 'theory' *)
|
||||||
" imports (* Declaration of 'theory' dependencies *)
|
" imports (* Declaration of 'theory' dependencies *)
|
||||||
|
@ -85,10 +87,9 @@ text\<open>
|
||||||
" keywords (* Registration of keywords defined locally *)
|
" keywords (* Registration of keywords defined locally *)
|
||||||
" requirement (* A command for describing requirements *)
|
" requirement (* A command for describing requirements *)
|
||||||
\end{isar}
|
\end{isar}
|
||||||
where \inlineisar{Example} is the abstract name of the text-file,
|
where \<^boxed_isar>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_isar>\<open>Main\<close> refers to an
|
||||||
\inlineisar{Main} refers to an imported theory (recall that the import
|
imported theory (recall that the import relation must be acyclic) and \inlineisar{keywords} are
|
||||||
relation must be acyclic) and \inlineisar{keywords} are used to
|
used to separate commands from each other.
|
||||||
separate commands from each other.
|
|
||||||
\<close>
|
\<close>
|
||||||
(* experiment starts here *)
|
(* experiment starts here *)
|
||||||
(* somewhere we destroyed the standard antiquotation thm ...
|
(* somewhere we destroyed the standard antiquotation thm ...
|
||||||
|
@ -97,8 +98,14 @@ text\<open> \<^emph>\<open>blabla\<close> @{thm \<open>refl\<close>}\<close>
|
||||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
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>
|
for @{term "fac 5"} the result @{value "fac 5"}.\<close>
|
||||||
*)
|
*)
|
||||||
text\<open> \<^theory_text>\<open>text\<open> According to the *\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
text\<open> A text-element \<^index>\<open>text-element\<close> may look like this:
|
||||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>\<close>
|
|
||||||
|
\<^theory_text>\<open>text\<open> According to the *\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
||||||
|
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
|
||||||
|
so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||||
|
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>
|
||||||
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
|
|
||||||
|
@ -172,6 +179,7 @@ text\<open>
|
||||||
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
|
||||||
|
@ -183,19 +191,21 @@ text\<open>
|
||||||
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
|
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
|
||||||
while the generated presentation in PDF is shown on the right.
|
while the generated presentation in PDF is shown on the right.
|
||||||
|
|
||||||
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits. For
|
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits.
|
||||||
example, it also allows the asynchronous evaluation and checking of the document
|
Besides UTF8-support for characters used in text-elements, Isabelle offers built-in already a
|
||||||
content~@{cite "wenzel:asynchronous:2014" and "wenzel:system:2014" and
|
mechanism user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
|
||||||
"barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE provides a
|
semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
|
||||||
\<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and auto-completion.
|
as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous
|
||||||
It also provides infrastructure for displaying meta-information (\<^eg>, binding and type annotation)
|
evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and
|
||||||
as pop-ups, while hovering over sub-expressions. A fine-grained dependency analysis allows the
|
"wenzel:system:2014" and "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE
|
||||||
processing of individual parts of theory files asynchronously, allowing Isabelle to interactively
|
provides a \<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and
|
||||||
process large (hundreds of theory files) documents. Isabelle can group sub-documents into sessions,
|
auto-completion. It also provides infrastructure for displaying meta-information (\<^eg>, binding
|
||||||
\<^ie>, sub-graphs of the document-structure that can be ``pre-compiled'' and loaded
|
and type annotation) as pop-ups, while hovering over sub-expressions. A fine-grained dependency
|
||||||
instantaneously, \<^ie>, without re-processing. \<close>
|
analysis allows the processing of individual parts of theory files asynchronously, allowing
|
||||||
|
Isabelle to interactively process large (hundreds of theory files) documents. Isabelle can group
|
||||||
|
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>
|
||||||
|
|
||||||
(* end experiment *)
|
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
end
|
end
|
||||||
|
|
|
@ -34,12 +34,12 @@ 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:
|
||||||
|
|
||||||
\begin{bash}
|
@{boxed_bash [display]
|
||||||
ë\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
|
||||||
\end{bash}
|
\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection*[installation::technical]\<open>Installation\<close>
|
subsection*[installation::technical]\<open>Installation\<close>
|
||||||
|
@ -51,52 +51,63 @@ text\<open>
|
||||||
subsubsection*[prerequisites::technical]\<open>Pre-requisites\<close>
|
subsubsection*[prerequisites::technical]\<open>Pre-requisites\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
\<^isadof> has to major pre-requisites:
|
\<^isadof> has to major pre-requisites:
|
||||||
\<^item> \<^bold>\<open>Isabelle\<close>\bindex{Isabelle} (\isabellefullversion).
|
\<^item> \<^bold>\<open>Isabelle\<close>\<^bindex>\<open>Isabelle\<close> (\isabellefullversion).
|
||||||
\<^isadof> uses a two-part version system (e.g., 1.0.0/2020),
|
\<^isadof> uses a two-part version system (e.g., 1.0.0/2020), where the first part is the version
|
||||||
where the first part is the version of \<^isadof> (using semantic versioning) and the second
|
of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle.
|
||||||
part is the supported version of Isabelle. Thus, the same version of \<^isadof> might be
|
Thus, the same version of \<^isadof> might be available for different versions of Isabelle.
|
||||||
available for different versions of Isabelle.
|
\<^item> \<^bold>\<open>\<^TeXLive> 2020\<close>\<^bindex>\<open>TexLive@\<^TeXLive>\<close> (or any other modern \<^LaTeX>-distribution where
|
||||||
\<^item> \<^bold>\<open>\TeXLive 2020\<close>\bindex{TexLive@\TeXLive} (or any other modern
|
\<^pdftex> supports the \<^boxed_latex>\<open>\expanded\<close> primitive).
|
||||||
\<^LaTeX>-distribution where \<^pdftex> supports
|
|
||||||
the \inlineltx|\expanded| primitive).
|
|
||||||
\<^footnote>\<open>see \<^url>\<open>https://www.texdev.net/2018/12/06/a-new-primitive-expanded\<close>\<close>
|
\<^footnote>\<open>see \<^url>\<open>https://www.texdev.net/2018/12/06/a-new-primitive-expanded\<close>\<close>
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
paragraph\<open>Installing Isabelle\<close>
|
paragraph\<open>Installing Isabelle\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
\enlargethispage{\baselineskip}
|
%\enlargethispage{\baselineskip}
|
||||||
Please download and install the Isabelle \isabelleversion distribution for your operating system
|
Please download and install the Isabelle \isabelleversion distribution for your operating system
|
||||||
from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful
|
from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful
|
||||||
installation of Isabelle, you should be able to call the \inlinebash|isabelle| tool on the
|
installation of Isabelle, you should be able to call the \<^boxed_bash>\<open>isabelle\<close> tool on the
|
||||||
command line:
|
command line:
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë isabelle version
|
ë\prompt{}ë isabelle version
|
||||||
ë\isabellefullversionë
|
ë\isabellefullversionë
|
||||||
\end{bash}
|
\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 \inlinebash{bin} directory
|
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
|
||||||
in your \inlinebash|PATH|, you will need to invoke \inlinebash|isabelle| 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>:
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
|
ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/ëbin/isabelle version
|
||||||
ë\isabellefullversionë
|
ë\isabellefullversionë
|
||||||
\end{bash}
|
\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:
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
|
ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
|
||||||
\end{bash}
|
\end{bash}
|
||||||
|
%@ {boxed_bash [display]\<open>
|
||||||
|
%ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra
|
||||||
|
%\<close>}
|
||||||
|
|
||||||
Please check that this, indeed, installs a version of \<^pdftex> that supports the
|
Please check that this, indeed, installs a version of \<^pdftex> that supports the
|
||||||
\inlineltx|\expanded|-primitive. To check your \pdfTeX-binary, execute
|
\<^boxed_latex>\<open>\expanded\<close>. To check your \<^pdftex>-binary, execute
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{}ë pdftex \\expanded{Success}\\end
|
ë\prompt{}ë pdftex \\expanded{Success}\\end
|
||||||
|
@ -104,9 +115,15 @@ This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian).
|
||||||
Output written on texput.pdf (1 page, 8650 bytes).
|
Output written on texput.pdf (1 page, 8650 bytes).
|
||||||
Transcript written on texput.log.
|
Transcript written on texput.log.
|
||||||
\end{bash}
|
\end{bash}
|
||||||
|
%@ {boxed_bash [display]\<open>
|
||||||
|
%ë\prompt{}ë pdftex \\expanded{Success}\\end
|
||||||
|
%This is pdfTeX, Version 3.14159265-2.6-1.40.20 (TeX Live 2019/Debian).
|
||||||
|
%Output written on texput.pdf (1 page, 8650 bytes).
|
||||||
|
%Transcript written on texput.log.
|
||||||
|
%\<close>}
|
||||||
|
|
||||||
If this generates successfully a file \inlinebash|texput.pdf|, your \<^pdftex>-binary supports
|
If this generates successfully a file \inlinebash|texput.pdf|, your \<^pdftex>-binary supports
|
||||||
the \inlineltx|\expanded|-primitive. If your Linux distribution does not (yet) ship \<^TeXLive>
|
the \<^boxed_latex>\<open>\expanded\<close>-primitive. If your Linux distribution does not (yet) ship \<^TeXLive>
|
||||||
2019 or your are running Windows or OS X, please follow the installation instructions from
|
2019 or your are running Windows or OS X, please follow the installation instructions from
|
||||||
\<^url>\<open>https://www.tug.org/texlive/acquire-netinstall.html\<close>.
|
\<^url>\<open>https://www.tug.org/texlive/acquire-netinstall.html\<close>.
|
||||||
\<close>
|
\<close>
|
||||||
|
@ -122,17 +139,17 @@ text\<open>
|
||||||
ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë
|
ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë
|
||||||
\end{bash}
|
\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 \inlinebash|install| 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{https://www.isa-afp.org}),
|
automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>),
|
||||||
namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"}
|
namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"}
|
||||||
and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a
|
and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a
|
||||||
few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system,
|
few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system,
|
||||||
which requires \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as
|
which requires \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as
|
||||||
Isabelle component.
|
Isabelle component.
|
||||||
|
|
||||||
If the \inlinebash|isabelle| tool is not in your \inlinebash|PATH|, you need to call the
|
If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your \<^boxed_bash>\<open>PATH\<close>, you need to call the
|
||||||
\inlinebash|install| script with the \inlinebash|--isabelle| option, passing the full-qualified
|
\<^boxed_bash>\<open>install\<close> script with the \<^boxed_bash>\<open>--isabelle\<close> option, passing the full-qualified
|
||||||
path of the \inlinebash|isabelle| tool (\inlinebash|install --help| 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}
|
\begin{bash}
|
||||||
|
@ -266,31 +283,41 @@ ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isab
|
||||||
\<^isadof>'s document setup does not make use of a file \inlinebash|root.tex|: this file is
|
\<^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
|
replaced by built-in document templates.\<close> The main two configuration files for
|
||||||
users are:
|
users are:
|
||||||
\<^item> The file \inlinebash|ROOT|\index{ROOT}, which defines the Isabelle session. New theory files as well as new
|
\<^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
|
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
|
\<^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"}.
|
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
|
||||||
\<^item> The file \inlinebash|praemble.tex|\index{praemble.tex}, which allows users to add additional
|
\<^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.
|
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
section*[scholar_onto::example]\<open>Writing Academic Publications (scholarly\_paper)\<close>
|
section*[scholar_onto::example]\<open>Writing Academic Publications (scholarly\_paper)\<close>
|
||||||
subsection\<open>The Scholarly Paper Example\<close>
|
subsection\<open>The Scholarly Paper Examples\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
The ontology ``scholarly\_paper''\index{ontology!scholarly\_paper} is a small ontology modeling
|
The ontology ``scholarly\_paper''\<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
|
||||||
academic/scientific papers. In this \<^isadof> application scenario, we deliberately refrain from
|
academic/scientific papers, with a slight bias to texts in the domain of mathematics and engineering.
|
||||||
integrating references to (Isabelle) formal content in order demonstrate that \<^isadof> is not a
|
We explain first the principles of its underlying ontology, and then we present two ''real''
|
||||||
framework from Isabelle users to Isabelle users only. Of course, such references can be added
|
example instances of our own.
|
||||||
easily and represent a particular strength of \<^isadof>.
|
\<^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 complex cross-referencing
|
||||||
|
between statements, definitions and proofs which is ontologically tracked. However, wrt.
|
||||||
|
to 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, deliberately
|
||||||
|
not exploiting \<^isadof>'s full potential with this regard.
|
||||||
|
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
|
||||||
|
refrain from integrating references to formal content in order demonstrate that \<^isadof> is not
|
||||||
|
a framework from Isabelle users to Isabelle users only, but people just avoiding as much as
|
||||||
|
possible \<^LaTeX> notation.
|
||||||
|
|
||||||
The \<^isadof> distribution contains an example (actually, our CICM 2018
|
The \<^isadof> distribution contains both examples using the ontology ``scholarly\_paper'' in
|
||||||
paper~@{cite "brucker.ea:isabelle-ontologies:2018"}) using the ontology ``scholarly\_paper'' in
|
the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or
|
||||||
the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/}. You
|
\nolinkurl{examples/scholarly_paper/2020-ifm-csp-applications/}.
|
||||||
can inspect/edit the example in Isabelle's IDE, by either
|
|
||||||
|
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
|
\<^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
|
Isabelle-Icon provided by the Isabelle installation) and loading the file
|
||||||
\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 calling:
|
\<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling:
|
||||||
|
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
ë\prompt{\isadofdirn}ë
|
ë\prompt{\isadofdirn}ë
|
||||||
|
@ -298,46 +325,85 @@ text\<open>
|
||||||
IsaDofApplications.thy
|
IsaDofApplications.thy
|
||||||
\end{bash}
|
\end{bash}
|
||||||
\<close>
|
\<close>
|
||||||
text\<open>
|
(* We should discuss if we shouldn't put the iFM paper more in the foreground *)
|
||||||
You can build the PDF-document by calling:
|
|
||||||
|
|
||||||
\begin{bash}
|
text\<open> You can build the PDF-document at the command line by calling:
|
||||||
ë\prompt{}ë isabelle build \
|
|
||||||
2018-cicm-isabelle_dof-applications
|
@{boxed_bash [display]
|
||||||
\end{bash}
|
\<open>ë\prompt{}ë isabelle build \
|
||||||
|
2018-cicm-isabelle_dof-applications\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
subsection\<open>A Bluffers Guide to the "scholarly\_paper" Ontology\<close>
|
||||||
|
text\<open> In this section we give a minimal overview of the ontology formalized in
|
||||||
|
@{theory \<open>Isabelle_DOF.scholarly_paper\<close>}.\<close>
|
||||||
|
|
||||||
subsection\<open>Modeling Academic Publications\<close>
|
text\<open> We start by modeling the usual text-elements of an academic paper: the title and author
|
||||||
text\<open>
|
|
||||||
We start by modeling the usual text-elements of an academic paper: the title and author
|
|
||||||
information, abstract, and text section:
|
information, abstract, and text section:
|
||||||
|
@{theory_text [display]
|
||||||
\begin{isar}
|
\<open>doc_class title =
|
||||||
doc_class title =
|
short_title :: "string option" <= "None"
|
||||||
short_title :: "string option" <= None
|
|
||||||
|
|
||||||
doc_class subtitle =
|
doc_class subtitle =
|
||||||
abbrev :: "string option" <= None
|
abbrev :: "string option" <= "None"
|
||||||
|
|
||||||
doc_class author =
|
doc_class author =
|
||||||
|
email :: "string" <= "''''"
|
||||||
|
http_site :: "string" <= "''''"
|
||||||
|
orcid :: "string" <= "''''"
|
||||||
affiliation :: "string"
|
affiliation :: "string"
|
||||||
|
|
||||||
doc_class abstract =
|
doc_class abstract =
|
||||||
keyword_list :: "string list" <= None
|
keywordlist :: "string list" <= "[]"
|
||||||
|
principal_theorems :: "thm list"\<close>}
|
||||||
|
\<close>
|
||||||
|
|
||||||
doc_class text_section =
|
text\<open>Note \<open>short_title\<close> and \<open>abbrev\<close> are optional and have the default \<open>None\<close> (no value).
|
||||||
|
Note further, that abstracts may have a \<open>principal_theorems\<close> list, where the built-in \<^isadof> type
|
||||||
|
\<open>thm list\<close> which contain references to formally proven theorems that must exist in the logical
|
||||||
|
context of this document; this is a decisive feature of \<^isadof> that conventional ontological
|
||||||
|
languages lack.\<close>
|
||||||
|
|
||||||
|
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
|
||||||
|
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
|
||||||
|
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
|
||||||
|
access-control features in a suitably adapted front-end.
|
||||||
|
|
||||||
|
@{theory_text [display] \<open>
|
||||||
|
doc_class text_section = text_element +
|
||||||
main_author :: "author option" <= None
|
main_author :: "author option" <= None
|
||||||
todo_list :: "string list" <= "[]"
|
fixme_list :: "string list" <= "[]"
|
||||||
\end{isar}
|
level :: "int option" <= "None"
|
||||||
|
\<close>}
|
||||||
|
|
||||||
|
The \<open>level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for headers, chapters, sections, and subsections;
|
||||||
|
we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
|
||||||
|
The values are interpreted accordingly to the \<^LaTeX> standard.
|
||||||
|
|
||||||
|
\<^enum> part \<^index>\<open>part\<close> \<^bigskip>\<^bigskip> \<open>Some -1\<close>
|
||||||
|
\<^enum> chapter \<^index>\<open>chapter\<close> \<^bigskip>\<^bigskip> \<open>Some 0\<close>
|
||||||
|
\<^enum> section \<^index>\<open>section\<close> \<^bigskip>\<^bigskip> \<open>Some 1\<close>
|
||||||
|
\<^enum> subsection \<^index>\<open>subsection\<close> \<^bigskip>\<^bigskip> \<open>Some 2\<close>
|
||||||
|
\<^enum> subsubsection \<^index>\<open>subsubsection\<close> \<^bigskip>\<^bigskip> \<open>Some 3\<close>
|
||||||
|
|
||||||
|
Additional means assure that the following invariant is maintained in a document
|
||||||
|
conforming to @{theory \<open>Isabelle_DOF.scholarly_paper\<close>}:
|
||||||
|
|
||||||
|
\center {\<open>level > 0\<close>}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
text\<open> The rest of the ontology introduces concepts for \<open>introductions\<close>, \<open>conclusion\<close>, \<open>related_work\<close>,
|
||||||
|
\<open>bibliography\<close> etc. More details can be found in \<close>
|
||||||
|
|
||||||
|
subsection\<open>Writing Academic Publications I \<close>
|
||||||
|
text*[xxx::technical, main_author = "Some bu"]\<open>The CSP paper. New screenshots to init sequence
|
||||||
|
required. Focus: Mathematical content. Definition, theorem, and citations...\<close>
|
||||||
|
|
||||||
|
subsection\<open>Writing Academic Publications II (somewhat outdated)\<close>
|
||||||
|
text\<open> In our next example we concentrate on non-text-elements. Figures...
|
||||||
|
|
||||||
The attributes \inlineisar+short_title+, \inlineisar+abbrev+ etc are introduced with their types as
|
|
||||||
well as their default values. Our model prescribes an optional \inlineisar+main_author+ and a
|
|
||||||
todo-list attached to an arbitrary text section; since instances of this class are mutable
|
|
||||||
(meta)-objects of text-elements, they can be modified arbitrarily through subsequent text and of
|
|
||||||
course globally during text evolution. Since \inlineisar+author+ is a HOL-type internally generated
|
|
||||||
by \<^isadof> framework and can therefore appear in the \inlineisar+main_author+ attribute of the
|
|
||||||
\inlineisar+text_section+ class; semantic links between concepts can be modeled this way.
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
|
figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogfood-Intro''"]
|
||||||
|
@ -429,6 +495,8 @@ text\<open>
|
||||||
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}).
|
||||||
\<close>
|
\<close>
|
||||||
|
(* Bu : This autoref stuff could be avoided if we would finally have monitors... *)
|
||||||
|
|
||||||
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>
|
||||||
|
|
||||||
|
|
|
@ -116,6 +116,24 @@
|
||||||
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf}
|
pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-isabelle-ontologies-2018.pdf}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@InCollection{ taha.ea:philosophers:2020,
|
||||||
|
keywords = {CSP, Isabelle/HOL, Process-Algebra,Formal Verification, Refinement},
|
||||||
|
author = {Safouan Taha and Burkhart Wolff and Lina Ye},
|
||||||
|
booktitle = {International Conference on Integrated Formal Methods (IFM)},
|
||||||
|
language = {USenglish},
|
||||||
|
publisher = {Springer-Verlag},
|
||||||
|
address = {Heidelberg},
|
||||||
|
series = {Lecture Notes in Computer Science},
|
||||||
|
number = {to appear},
|
||||||
|
title = {Philosophers may dine --- definitively!},
|
||||||
|
classification= {conference},
|
||||||
|
areas = {formal methods, software},
|
||||||
|
public = {yes},
|
||||||
|
year = {2020}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
@Book{ boulanger:cenelec-50128:2015,
|
@Book{ boulanger:cenelec-50128:2015,
|
||||||
author = {Boulanger, Jean-Louis},
|
author = {Boulanger, Jean-Louis},
|
||||||
title = {{CENELEC} 50128 and {IEC} 62279 Standards},
|
title = {{CENELEC} 50128 and {IEC} 62279 Standards},
|
||||||
|
|
Reference in New Issue