revision of front, intro and bachgrnd (incomplete)
This commit is contained in:
parent
25473b177b
commit
4157954506
|
@ -448,7 +448,7 @@ fun doc_cmd kwd txt flag key =
|
|||
in
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition"
|
||||
Definition_default_class \<^const_name>\<open>defn\<close>;
|
||||
Definition_default_class \<^const_name>\<open>defn\<close>;
|
||||
|
||||
val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close> "Freeform Lemma Description"
|
||||
Lemma_default_class \<^const_name>\<open>lemm\<close>;
|
||||
|
@ -554,6 +554,7 @@ print_doc_classes
|
|||
print_doc_class_template "definition" (* just a sample *)
|
||||
print_doc_class_template "lemma" (* just a sample *)
|
||||
print_doc_class_template "theorem" (* just a sample *)
|
||||
print_doc_class_template "premise" (* just a sample *)
|
||||
|
||||
|
||||
subsection\<open>Structuring Enforcement in Engineering/Math Papers \<close>
|
||||
|
|
|
@ -30,6 +30,7 @@ define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
|
|||
BibTeX \<rightleftharpoons> \<open>\BibTeX{}\<close>
|
||||
LaTeX \<rightleftharpoons> \<open>\LaTeX{}\<close>
|
||||
TeX \<rightleftharpoons> \<open>\TeX{}\<close>
|
||||
dofurl \<rightleftharpoons> \<open>\dofurl\<close>
|
||||
pdf \<rightleftharpoons> \<open>PDF\<close>
|
||||
|
||||
text\<open>Note that these setups assume that the associated \<^LaTeX> macros
|
||||
|
|
|
@ -38,26 +38,34 @@ and their logical contexts).
|
|||
|
||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||
In general, an ontology is a formal explicit description of \<^emph>\<open>concepts\<close> in a domain of discourse
|
||||
(called \<^emph>\<open>classes\<close>), properties of each concept describing \<^emph>\<open>attributes\<close> of the concept, as well
|
||||
as \<^emph>\<open>links\<close> between them. A particular link between concepts is the \<^emph>\<open>is-a\<close> relation declaring
|
||||
(called \<^emph>\<open>classes\<close>), components (called \<^emph>\<open>attributes\<close>) of the concept, and properties (called
|
||||
\<^emph>\<open>invariants\<close>) on concepts. Logically, classes are represented by a type (the class type) and
|
||||
particular terms representing \<^emph>\<open>instances\<close> of them. Since components are typed, it is therefore
|
||||
possible to express \<^emph>\<open>links\<close> like \<open>m\<close>-to-\<open>n\<close> relations between classes.
|
||||
Another form of link between concepts is the \<^emph>\<open>is-a\<close> relation declaring
|
||||
the instances of a subclass to be instances of the super-class.
|
||||
|
||||
To address this challenge, we present the Document Ontology Framework (\<^dof>) and an
|
||||
implementation of \<^dof> called \<^isadof>. \<^dof> is designed for building scalable and user-friendly
|
||||
tools on top of interactive theorem provers. \<^isadof> is an instance of this novel framework,
|
||||
implemented as extension of Isabelle/HOL, to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them
|
||||
during document evolution. Based on Isabelle's infrastructures, ontologies may refer to types,
|
||||
terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle
|
||||
IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}), a document is checked to be
|
||||
\<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast user-feedback \<^emph>\<open>during the
|
||||
capture of content\<close>. This is particularly valuable in case of document evolution, where the
|
||||
\<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can be mechanically checked.
|
||||
Engineering an ontological language for documents that contain both formal and informal elements
|
||||
as occuring in formal theories is a particular challenge. To address this latter, we present
|
||||
the Document Ontology Framework (\<^dof>) and an implementation of \<^dof> called \<^isadof>.
|
||||
\<^dof> is designed for building scalable and user-friendly tools on top of interactive theorem
|
||||
provers. \<^isadof> is an instance of this novel framework, implemented as extension of Isabelle/HOL,
|
||||
to \<^emph>\<open>model\<close> typed ontologies and to \<^emph>\<open>enforce\<close> them during document evolution. Based on Isabelle's
|
||||
infrastructures, ontologies may refer to types, terms, proven theorems, code, or established
|
||||
assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, @{cite "wenzel:asynchronous:2014"}),
|
||||
a document is checked to be \<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast
|
||||
user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in case of document
|
||||
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can
|
||||
be mechanically checked.
|
||||
|
||||
To avoid any misunderstanding: \<^isadof> is \<^emph>\<open>not a theory in HOL\<close> on ontologies and operations to
|
||||
track and trace links in texts, it is an \<^emph>\<open>environment to write structured text\<close> which
|
||||
\<^emph>\<open>may contain\<close> Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and
|
||||
scientific papers---as the present one, which is written in \<^isadof> itself. \<^isadof> is a plugin
|
||||
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}.\<close>
|
||||
into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. However,
|
||||
\<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
|
||||
and code that allows both interactive checking as well as formal reasoning over meta-data
|
||||
related to annotated documents.\<close>
|
||||
|
||||
subsubsection\<open>How to Read This Manual\<close>
|
||||
(*<*)
|
||||
|
@ -91,9 +99,9 @@ text\<open>
|
|||
by simp\<close>}
|
||||
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
|
||||
@{boxed_pdf [display] \<open>The axiom refl\<close>}
|
||||
\<^item> a red background for (S)ML-code:
|
||||
\<^item> a red background for SML-code:
|
||||
@{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>}
|
||||
\<^item> a grey background for shell scripts and interactive shell sessions:
|
||||
@{boxed_bash [display]\<open>ë\prompt{}ë ls
|
||||
|
@ -104,6 +112,15 @@ subsubsection\<open>How to Cite \<^isadof>\<close>
|
|||
text\<open>
|
||||
If you use or extend \<^isadof> in your publications, please use
|
||||
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker, I.~Ait-Sadoune, N. Méric, and B.~Wolff. Using Deep Ontologies in Formal
|
||||
Software Engineering. In \<^emph>\<open>International Conference on Rigorous State-Based Methods (ABZ 2023)\<close>,
|
||||
To appear in Lecture Notes in Computer Science. Springer-Verlag,
|
||||
Heidelberg, 2023. \href{https://doi.org/???} {10.1007/????????}.
|
||||
\end{quote}
|
||||
A \<^BibTeX>-entry is available at:
|
||||
\<^url>\<open>https://www.lri.fr/~wolff/bibtex/wolff.html\<close>.
|
||||
\<^item> an older description of the system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
||||
\begin{quote}\small
|
||||
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
|
||||
framework: Linking the formal with the informal. In \<^emph>\<open>Conference on Intelligent Computer
|
||||
|
@ -128,13 +145,13 @@ text\<open>
|
|||
Using Ontologies in Formal Developments Targeting Certification.
|
||||
In W. Ahrendt and S. Tarifa, editors. \<^emph>\<open>Integrated Formal Methods (IFM)\<close>, number 11918.
|
||||
Lecture Notes in Computer Science. Springer-Verlag, Heidelberg, 2019.
|
||||
\href{https://doi.org/10.1007/978-3-030-34968-4\_4}.
|
||||
\<^url>\<open>https://doi.org/10.1007/978-3-030-34968-4_4\<close>.
|
||||
\end{quote}
|
||||
\<close>
|
||||
subsubsection\<open>Availability\<close>
|
||||
text\<open>
|
||||
The implementation of the framework is available at
|
||||
\url{\dofurl}. The website also provides links to the latest releases. \<^isadof> is licensed
|
||||
\url{\<^dofurl>}. The website also provides links to the latest releases. \<^isadof> is licensed
|
||||
under a 2-clause BSD license (SPDX-License-Identifier: BSD-2-Clause).
|
||||
\<close>
|
||||
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2019-2023 The University of Exeter
|
||||
* 2018-2023 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
@ -30,8 +30,8 @@ While Isabelle 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 ``\<^emph>\<open>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
|
||||
Among other things, Isabelle provides an infrastructure for Isabelle plug-ins, comprising extensible
|
||||
state components and extensible syntax that can be bound to SML programs. Thus, the Isabelle
|
||||
architecture may be understood as an extension and refinement of the traditional `LCF approach',
|
||||
with explicit infrastructure for building derivative systems.\<close>''~@{cite "wenzel.ea:building:2007"}
|
||||
|
||||
|
@ -49,9 +49,13 @@ The Isabelle system architecture shown in @{docitem \<open>architecture\<close>}
|
|||
with Standard ML (SML) at the bottom layer as implementation language. The architecture actually
|
||||
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
|
||||
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 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>
|
||||
support for higher specification constructs were built.
|
||||
\<^footnote>\<open>We use the term \<^emph>\<open>plugin\<close> for a collection of HOL-definitions, SML and Scala code in order
|
||||
to distinguish it from the official Isabelle term \<^emph>\<open>component\<close> which implies a particular
|
||||
format and support by the Isabelle build system.\<close>
|
||||
\<close>
|
||||
|
||||
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
|
||||
text\<open>
|
||||
|
@ -72,13 +76,13 @@ declare_reference*["fig:dependency"::figure]
|
|||
text\<open>
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>\<^bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured
|
||||
in a set of \<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy of \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
|
||||
acyclic at this level.
|
||||
Sub-documents can have different document types in order to capture documentations consisting of
|
||||
Document parts can have different document types in order to capture documentations consisting of
|
||||
documentation, models, proofs, code of various forms and other technical artifacts. We call the
|
||||
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
|
||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||
|
@ -108,9 +112,9 @@ contains characters and a special notation for semantic macros \<^bindex>\<open>
|
|||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
|
||||
use of \<^dof> in its current stage --- it is important to note that there are actually three
|
||||
families of ``ontology aware'' document elements with analogous
|
||||
text\<open>While \<^theory_text>\<open>text\<close>- elements play a major role in this manual on
|
||||
--- this is the main use of \<^dof> in its current stage --- it is important to note that there
|
||||
are actually three families of ``ontology aware'' document elements with analogous
|
||||
syntax to standard ones. The difference is a bracket with meta-data of the form:
|
||||
@{theory_text [display,indent=5, margin=70]
|
||||
\<open>
|
||||
|
@ -123,7 +127,8 @@ Depending on the family, we will speak about \<^emph>\<open>(formal) text-contex
|
|||
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
|
||||
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
|
||||
framework allows for nesting cartouches that permits to support switching into a different
|
||||
context. In general, this has also the effect that the evaluation of antiquotations changes.
|
||||
context, albeit not all combinations are actually supported.
|
||||
In general, nesting contexts has the effect that the evaluation of antiquotations changes.
|
||||
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||
\<close>
|
||||
|
|
Loading…
Reference in New Issue