219 lines
12 KiB
Plaintext
219 lines
12 KiB
Plaintext
(*<*)
|
|
theory "02_Background"
|
|
imports "01_Introduction"
|
|
begin
|
|
(*>*)
|
|
|
|
chapter*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
|
|
\<open> Background: The Isabelle System \<close>
|
|
section*[bgrnd1::introduction]\<open>Document Processing in Isabelle\<close>
|
|
text*[background::introduction]\<open>
|
|
While Isabelle @{cite "nipkow.ea:isabelle:2002"} is widely perceived as an interactive theorem prover
|
|
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
|
|
would like to emphasize the view that Isabelle is far more than that:
|
|
it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>. This refers to the
|
|
``\textsl{generic system framework of Isabelle/Isar underlying recent
|
|
versions of Isabelle. Among other things, Isar provides an
|
|
infrastructure for Isabelle plug-ins, comprising extensible state
|
|
components and extensible syntax that can be bound to ML
|
|
programs. Thus, the Isabelle/Isar architecture may be understood as
|
|
an extension and refinement of the traditional `LCF approach', with
|
|
explicit infrastructure for building derivative
|
|
\<^emph>\<open>systems\<close>.}''~@{cite "wenzel.ea:building:2007"}
|
|
|
|
The current system framework offers moreover the following features:
|
|
|
|
\<^item> a build management grouping components into to pre-compiled sessions,
|
|
\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends
|
|
\<^item> documentation - and code generators,
|
|
\<^item> an extensible front-end language Isabelle/Isar, and,
|
|
\<^item> last but not least, an LCF style, generic theorem prover kernel as
|
|
the most prominent and deeply integrated system component.
|
|
\<close>
|
|
|
|
figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open>
|
|
The system architecture of Isabelle (left-hand side) and the
|
|
asynchronous communication between the Isabelle system and
|
|
the IDE (right-hand side). \<close>
|
|
|
|
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
|
|
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
|
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
|
resides in the SML structure \texttt{Context}. This structure provides a kind of container called
|
|
\<^emph>\<open>context\<close> providing an identity, an ancestor-list as well as typed, user-defined state
|
|
for components (plugins) such as \isadof. On top of the latter, the LCF-Kernel, tactics,
|
|
automated proof procedures as well as specific support for higher specification constructs
|
|
were built. \<close>
|
|
|
|
|
|
text\<open> Of particular interest for \dof is documentation generation of the architecture,
|
|
which is based on literate specification commands such as \inlineisar+section+ \ldots,
|
|
\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. Moreover, we assume that
|
|
\<^emph>\<open>inside\<close> text-elements, there are generic and extendible ways to add "semantic", i.e.
|
|
machine-checked sub-elements.
|
|
|
|
In the sequel, we will outline the general assumptions that \dof makes for the underlying
|
|
document model, and than explain how Isabelle as a framework fits into this picture.
|
|
\<close>
|
|
|
|
|
|
(*
|
|
Thus, a user can add a simple text:
|
|
\begin{isar}
|
|
text\<Open>This is a description.\<Close>
|
|
\end{isar}
|
|
These text-commands can be arbitrarily mixed with other commands stating definitions, proofs, code, etc.,
|
|
and will result in the corresponding output in generated \LaTeX{} or HTML documents.
|
|
Now, \<^emph>\<open>inside\<close> the textual content, it is possible to embed a \<^emph>\<open>text-antiquotation\<close>:
|
|
\begin{isar}
|
|
text\<Open>According to the reflexivity axiom \at{thm refl}, we obtain in \<Gamma>
|
|
for \at{term "fac 5"} the result \at{value "fac 5"}.\<Close>
|
|
\end{isar}
|
|
which is represented in the generated output by:
|
|
\begin{out}
|
|
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
|
|
\end{out}
|
|
where \inlineisar+refl+ is actually the reference to the axiom of reflexivity in HOL.
|
|
For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual definition for
|
|
\inlineisar+fac+ in HOL.
|
|
\<close>
|
|
|
|
text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being
|
|
displayed and can be used for calculations before actually being typeset. When editing,
|
|
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
|
\<^emph>\<open>semi-formal\<close> content. \<close>
|
|
*)
|
|
|
|
|
|
section*["sec:background"::introduction]\<open>The Required Document Model\<close>
|
|
text\<open>
|
|
In this section, we explain the assumed document model underlying
|
|
\dof in general; in particular the concepts \<^emph>\<open>integrated document\<close>,
|
|
\<^emph>\<open>sub-document\<close> , \<^emph>\<open>text-element\<close> and \<^emph>\<open>semantic macros\<close> occurring
|
|
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
|
|
$\lambda$-calculus and some Higher-order Logic (HOL).\<close>
|
|
|
|
figure*["fig:dependency"::figure,relative_width="50",src="''figures/document-hierarchy''"]\<open>
|
|
A Theory-Graph in the Document Model. \<close>
|
|
|
|
|
|
text\<open>
|
|
We assume a hierarchical document model, \ie, an \<^emph>\<open>integrated\<close>
|
|
document consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that
|
|
can depend acyclically on each other. Sub-documents can have different
|
|
document types in order to capture documentations consisting of
|
|
documentation, models, proofs, code of various forms and other
|
|
technical artifacts. We call the main sub-document type, for
|
|
historical reasons, \<^emph>\<open>theory\<close>-files. A theory file consists of a
|
|
\<^emph>\<open>header\<close>, a \<^emph>\<open>context definition\<close>, and a body consisting of a
|
|
sequence of \<^emph>\<open>command\<close>s (@{figure "fig:dependency"}). Even the
|
|
header consists of a sequence of commands used for introductory text
|
|
elements not depending on any context. The context-definition
|
|
contains an \inlineisar{import} and a \inlineisar{keyword} section,
|
|
for example:
|
|
\begin{isar}
|
|
theory Example (* Name of the "theory" *)
|
|
imports (* Declaration of "theory" dependencies *)
|
|
Main (* Imports a library called "Main" *)
|
|
keywords (* Registration of keywords defined locally *)
|
|
requirement (* A command for describing requirements *)
|
|
\end{isar}
|
|
where \inlineisar{Example} is the abstract name of the text-file,
|
|
\texttt{Main} refers to an imported theory (recall that the import
|
|
relation must be acyclic) and \inlineisar{keywords} are used to
|
|
separate commands from each other.\<close>
|
|
|
|
text\<open>We distinguish fundamentally two different syntactic levels:
|
|
\begin{compactenum}
|
|
\item the \emph{outer-syntax} (\ie, the syntax for commands) is processed
|
|
by a lexer-library and parser combinators built on top, and
|
|
\item the \emph{inner-syntax} (\ie, the syntax for $\lambda$-terms in
|
|
HOL) with its own parametric polymorphism type checking.
|
|
\end{compactenum}
|
|
On the semantic level, we assume a validation process for an
|
|
integrated document, where the semantics of a command is a
|
|
transformation \inlineisar+\<theta> \<rightarrow> \<theta>+ for some
|
|
system state \inlineisar+\<theta>+. This document model can be
|
|
instantiated with outer-syntax commands for common text elements, \eg,
|
|
\inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add informal text to a
|
|
sub-document using a text command:
|
|
\begin{isar}
|
|
text\<Open>This is a description.\<Close>
|
|
\end{isar}
|
|
This will type-set the corresponding text in, for example, a PDF document.
|
|
However, this translation is not necessarily one-to-one: text
|
|
elements can be enriched by formal, \ie, machine-checked content via
|
|
\emph{semantic macros}, called antiquotations:
|
|
\begin{isar}
|
|
text\<Open>According to the reflexivity axiom @{thm refl}, we obtain in \<Gamma>
|
|
for @{term "fac 5"} the result @{value "fac 5"}.\<Close>
|
|
\end{isar}
|
|
which is represented in the final document (\eg, a PDF) by:
|
|
\begin{out}
|
|
According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$.
|
|
\end{out}
|
|
Semantic macros are partial functions of type %
|
|
\inlineisar+\<theta> \<rightarrow> text+; since they can use the
|
|
system state, they can perform all sorts of specific checks or
|
|
evaluations (type-checks, executions of code-elements, references to
|
|
text-elements or proven theorems such as \inlineisar+refl+, which is
|
|
the reference to the axiom of reflexivity).
|
|
|
|
Semantic macros establish \<^emph>\<open>formal content\<close> inside informal content; they can be
|
|
type-checked before being displayed and can be used for calculations before being
|
|
typeset. They represent the device for linking the formal with the informal. \<close>
|
|
|
|
|
|
|
|
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model.\<close>
|
|
text\<open> Batch-mode checkers for \dof can be implemented in all systems of the
|
|
LCF-style prover family, \ie, systems with a type-checked
|
|
\inlinesml{term}, and abstract \inlinesml{thm}-type for
|
|
theorems (protected by a kernel). This includes, \eg, ProofPower,
|
|
HOL4, HOL-light, Isabelle, as well as Coq and its derivatives. \dof
|
|
is, however, designed for fast interaction in an IDE. If a user wants
|
|
to benefit from this experience, only Isabelle and Coq have the
|
|
necessary infrastructure of asynchronous proof-processing and support
|
|
by a PIDE
|
|
@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and "DBLP:conf/mkm/BarrasGHRTWW13"
|
|
and "Faithfull:2018:COQ:3204179.3204223"} which 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 nested along the \inlineisar+ \<Open> ... \<Close> + barriers, while
|
|
\dof actually only requires a 2-level syntax model.\<close>
|
|
|
|
figure*["fig:dof-ide"::figure,relative_width="80",src="''figures/cicm2018-combined''"]\<open>
|
|
The \isadof IDE (left) and the corresponding PDF (right).% , showing the first page
|
|
% of~\cite{brucker.ea:isabelle-ontologies:2018}. \<close>
|
|
|
|
text\<open> We call the present implementation of \dof on the
|
|
Isabelle platform \isadof. In
|
|
@{docitem "fig:dof-ide"}, a screen-shot of an introductory paper on \isadof
|
|
@{cite "brucker.ea:isabelle-ontologies:2018"} is shown;
|
|
this paper focusses on a number of application scenarios and user-interface aspects.
|
|
In @{docitem "fig:dof-ide"}, the \isadof PIDE can be seen on the left, 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 example, it also allows the asynchronous
|
|
evaluation and checking of the document content
|
|
@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and
|
|
"DBLP:conf/mkm/BarrasGHRTWW13"}
|
|
and is dynamically extensible. Its PIDE provides a \<^emph>\<open>continuous build, continuous check\<close>
|
|
functionality, syntax highlighting, and IntelliSense-like auto-completion.
|
|
It also provides infrastructure for
|
|
displaying meta-information (\eg, binding and type annotation) as
|
|
pop-ups, while hovering over sub-expressions. A fine-grained
|
|
dependency 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. \<close>
|
|
|
|
(*<*)
|
|
end
|
|
(*>*)
|
|
|