Theory M_03_GuidedTour
theory
"M_03_GuidedTour"
imports
"M_02_Background"
begin
chapter*[isadof_tour::text_section]‹\<^isadof>: A Guided Tour›
text‹
In this chapter, we will give an introduction into using \<^isadof> for users that want to create and
maintain documents following an existing document ontology\<^bindex>‹ontology› in ODL\<^bindex>‹ODL›.
›
section*[getting_started::technical]‹Getting Started›
subsection*[installation::technical]‹Installation›
text‹
In this section, we will show how to install \<^isadof>. We assume a basic familiarity with a
Linux/Unix-like command line (i.e., a shell).
We focus on the installation of the latest official release of \<^isadof> as
available in the Archive of Formal Proofs (AFP).⁋‹If you want to work with the development version
of \<^isadof>, please obtain its source code from the \<^isadof> Git repostitory
(🌐‹https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF› and follow the instructions
in provided ▩‹README.MD› file.›
\<^isadof> requires Isabelle\<^bindex>‹Isabelle› with a recent \<^LaTeX>-distribution
(e.g., Tex Live 2022 or later).
›
paragraph‹Installing Isabelle and the AFP.›
text‹
Please download and install the latest official Isabelle release from the Isabelle Website
(🌐‹https://isabelle.in.tum.de›). After the successful installation of Isabelle, you should be
able to call the \<^boxed_bash>‹isabelle› tool on the command line:
@{boxed_bash [display]‹ë\prompt{}ë isabelle version›}
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>‹bin› directory
in your \<^boxed_bash>‹PATH›, you will need to invoke \<^boxed_bash>‹isabelle› using its
full qualified path.
›
text‹
Next, download the the AFP from 🌐‹https://www.isa-afp.org/download/› and
follow the instructions given at 🌐‹https://www.isa-afp.org/help/› for installing the AFP as an
Isabelle component.›
paragraph‹Installing \<^TeXLive>.›
text‹
On a Debian-based Linux system (\<^eg>, Ubuntu), the following command
should install all required \<^LaTeX> packages:
@{boxed_bash [display]‹ë\prompt{}ë sudo aptitude install texlive-full›}
›
subsubsection*[isadof::technical]‹Installing \<^isadof>›
text‹
By installing the AFP in the previous steps, you already installed \<^isadof>. In fact, \<^isadof>
is currently consisting out of three AFP entries:
▪ ▩‹Isabelle_DOF›: This entry
contains the \<^isadof> system itself, including the \<^isadof> manual.
▪ ▩‹Isabelle_DOF-Example-I›: This entry contains an example of
an academic paper written using the \<^isadof> system oriented towards an
introductory paper. The text is based on~\<^cite>‹"brucker.ea:isabelle-ontologies:2018"›;
in the document, we deliberately refrain from integrating references to formal content in order
to demonstrate that \<^isadof> can be used for writing documents with very little direct use of
\<^LaTeX>.
▪ ▩‹Isabelle_DOF-Example-II›: This entry contains another example of
a mathematics-oriented academic paper. It is based on~\<^cite>‹"taha.ea:philosophers:2020"›.
It represents a typical mathematical text, heavy in definitions with complex mathematical notation
and a lot of non-trivial cross-referencing between statements, definitions, and proofs which
are ontologically tracked. However, with respect 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, and therefore does deliberately not exploit \<^isadof> 's full potential.›
section*[writing_doc::technical]‹Writing Documents›
subsection*[document::example]‹Document Generation›
text‹\<^isadof> provides an enhanced setup for generating PDF document. In particular, it does
not make use of a file called ▩‹document/root.tex›. Instead, the use of document templates and
ontology represenations is done within theory files. To make use of this feature, one needs
to add the option ▩‹document_build = dof› to the ▩‹ROOT› file.
An example ▩‹ROOT› file looks as follows:
›
text‹
\begin{config}{ROOT}
session example = Isabelle_DOF +
options [document = pdf, document_output = "output", document_build = dof]
(*theories [document = false]
A
theories
B*)
\end{config}
The document template and ontology can be selected as follows:
@{boxed_theory_text [display]
‹
theory C imports Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper begin
list_templates
use_template "scrreprt-modern"
list_ontologies
use_ontology "technical_report" and "scholarly_paper"
end
›}
The commands @{boxed_theory_text
‹
list_templates
›} and
@{boxed_theory_text
‹
list_ontologies
›}
can be used for inspecting (and selecting) the available ontologies and templates:
@{boxed_theory_text [display]
‹
list_templates
list_ontologies
›}
Note that you need to import the theories that define the ontologies that you
want to use. Otherwise, they will not be available.
›
paragraph‹Warning.›
text‹
Note that the session \<^session>‹Isabelle_DOF› needs to be part of the ``main'' session
hierarchy. Loading the \<^isadof> theories as part of a session section, e.g.,
›
text‹\<^latex>‹
\begin{config}{ROOT}
session example = HOL +
options [document = pdf, document_output = "output", document_build = dof]
session
Isabelle_DOF.scholarly_paper
theories
C
\end{config}
››
text‹
will not work. Trying to build a document using such a setup will result in the
following error message:
@{boxed_bash [display]‹ë\prompt{}ë
isabelle build -D .
Running example ...
Bad document_build engine "dof"
example FAILED›}
›
subsection*[naming::example]‹Name-Spaces, Long- and Short-Names›
text‹\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were
composed of a name of the session, the name of the theory, and a sequence of local names referring
to, \<^eg>, nested specification constructs that were used to identify types, constant symbols,
definitions, \<^etc>. The general format of a long-name is
\<^boxed_theory_text>‹ session_name.theory_name.local_name. ... .local_name›
By lexical conventions, theory-names must be unique inside a session
(and session names must be unique too), such that long-names are unique by construction.
There are actually different name categories that form a proper name space, \<^eg>, the name space for
constant symbols and type symbols are distinguished.
Additionally, \<^isadof> objects also come with a proper name space: classes (and monitors), instances,
low-level class invariants (SML-defined invariants) all follow the lexical conventions of
Isabelle. For instance, a class can be referenced outside its theory using
its short-name or its long-name if another class with the same name is defined
in the current theory.
Isabelle identifies names already with the shortest suffix that is unique in the global
context and in the appropriate name category. This also holds for pretty-printing, which can
at times be confusing since names stemming from the same specification construct may
be printed with different prefixes according to their uniqueness.
›
subsection*[cartouches::example]‹Caveat: Lexical Conventions of Cartouches, Strings, Names, ... ›
text‹WARNING: The embedding of strings, terms, names \<^etc>, as parts of commands, anti-quotations,
terms, \<^etc>, is unfortunately not always so consistent as one might expect, when it comes
to variants that should be lexically equivalent in principle. This can be a nuisance for
users, but is again a consequence that we build on existing technology that has been developed
over decades.
›
text‹At times, this causes idiosyncrasies like the ones cited in the following incomplete list:
▪ text-antiquotations
⬚‹text‹@{thm \<doublequote>srac⇩1_def\<doublequote>}››
while ⬚‹text‹@{thm ‹srac⇩1_def›}›› fails
▪ commands ⬚‹thm fundamental_theorem_of_calculus› and
⬚‹thm \<doublequote>fundamental_theorem_of_calculus\<doublequote>›
or ⬚‹lemma \<doublequote>H\<doublequote>› and ⬚‹lemma ‹H›› and ⬚‹lemma H›
▪ string expressions
⬚‹term‹\<quote>\<quote>abc\<quote>\<quote> @ \<quote>\<quote>cd\<quote>\<quote>›› and equivalent
⬚‹term ‹‹abc› @ ‹cd›››;
but ⬚‹term‹‹A ⟶ B››› not equivalent to ⬚‹term‹\<quote>\<quote>A ⟶ B\<quote>\<quote>››
which fails.
›
section*[scholar_onto::example]‹Writing Academic Publications in \<^boxed_theory_text>‹scholarly_paper››
subsection‹Editing Major Examples›
text‹
The ontology ▩‹scholarly_paper› \<^index>‹ontology!scholarly\_paper› is an ontology modeling
academic/scientific papers, with a slight bias towards texts in the domain of mathematics and
engineering.
You can inspect/edit the example in Isabelle's IDE, by either
▪ 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>‹Isabelle_DOF-Example-I/IsaDofApplications.thy"›
›
text‹ You can build the \<^pdf>-document at the command line by calling:
@{boxed_bash [display] ‹ë\prompt{}ë isabelle build Isabelle_DOF-Example-I›}
›
subsection*[sss::technical]‹A Bluffers Guide to the ▩‹scholarly_paper› Ontology›
text‹ In this section we give a minimal overview of the ontology formalized in
\<^theory>‹Isabelle_DOF.scholarly_paper›. We start by modeling the usual text-elements of an
academic paper: the title and author information, abstract, and text section:
@{boxed_theory_text [display]
‹doc_class title =
short_title :: "string option" <= "None"
doc_class subtitle =
abbrev :: "string option" <= "None"
doc_class author =
email :: "string" <= "''''"
http_site :: "string" <= "''''"
orcid :: "string" <= "''''"
affiliation :: "string"
doc_class abstract =
keywordlist :: "string list" <= "[]"
principal_theorems :: "thm list"›}
›
text‹Note \<^const>‹short_title› and \<^const>‹abbrev› are optional and have the default \<^const>‹None›
(no value). Note further, that \<^typ>‹abstract›s may have a \<^const>‹principal_theorems› list, where
the built-in \<^isadof> type \<^typ>‹thm list› contains 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.›
text‹We continue by the introduction of a main class: the text-element \<^typ>‹text_section›
(in contrast to \<^typ>‹figure› or ‹table› or similar). Note that
the \<^const>‹main_author› is typed with the class \<^typ>‹author›, a HOL type that is automatically
derived from the document class definition \<^typ>‹author› shown above. It is used to express which
author currently ``owns'' this \<^typ>‹text_section›, an information that can give rise to
presentational or even access-control features in a suitably adapted front-end.
@{boxed_theory_text [display] ‹
doc_class text_section = text_element +
main_author :: "author option" <= None
fixme_list :: "string list" <= "[]"
level :: "int option" <= "None"
›}
The \<^const>‹Isa_COL.text_element.level›-attibute \<^index>‹level› 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. The correspondence between the levels and the structural entities is summarized
as follows:
▪ part \<^index>‹part› ‹Some -1› \<^vs>‹-0.3cm›
▪ chapter \<^index>‹chapter› ‹Some 0› \<^vs>‹-0.3cm›
▪ section \<^index>‹section› ‹Some 1› \<^vs>‹-0.3cm›
▪ subsection \<^index>‹subsection› ‹Some 2› \<^vs>‹-0.3cm›
▪ subsubsection \<^index>‹subsubsection› ‹Some 3› \<^vs>‹-0.3cm›
Additional means assure that the following invariant is maintained in a document
conforming to ▩‹scholarly_paper›: ‹level > 0›.
›
text‹ The rest of the ontology introduces concepts for \<^typ>‹introduction›, \<^typ>‹conclusion›,
\<^typ>‹related_work›, \<^typ>‹bibliography› etc. More details can be found in ▩‹scholarly_paper›
contained in the theory \<^theory>‹Isabelle_DOF.scholarly_paper›. ›
subsection‹Writing Academic Publications: A Freeform Mathematics Text ›
text*[csp_paper_synthesis::technical, main_author = "Some bu"]‹We present a typical mathematical
paper focusing on its form, not referring in any sense to its content which is out of scope here.
As mentioned before, we chose the paper~\<^cite>‹"taha.ea:philosophers:2020"› for this purpose,
which is written in the so-called free-form style: Formulas are superficially parsed and
type-set, but no deeper type-checking and checking with the underlying logical context
is undertaken. ›
figure*[fig0::figure,relative_width="85",file_src="''figures/header_CSP_source.png''"]
‹ A mathematics paper as integrated document source ... ›
figure*[fig0B::figure,relative_width="85",file_src="''figures/header_CSP_pdf.png''"]
‹ ... and as corresponding \<^pdf>-output. ›
text‹The integrated source of this paper-excerpt is shown in \<^figure>‹fig0›, while the
document build process converts this to the corresponding \<^pdf>-output shown in \<^figure>‹fig0B›.›
text‹Recall that the standard syntax for a text-element in \<^isadof> is
⬚‹text*[<id>::<class_id>,<attrs>]‹ ... text ...››, but there are a few built-in abbreviations like
⬚‹title*[<id>,<attrs>]‹ ... text ...›› that provide special command-level syntax for text-elements.
The other text-elements provide the authors and the abstract as specified by their
∗‹class\_id›\<^index>‹class\_id@‹class_id››
referring to the ⬚‹doc_class›es of ▩‹scholarly_paper›;
we say that these text elements are ∗‹instances›
\<^bindex>‹instance› of the ⬚‹doc_class›es \<^bindex>‹doc\_class› of the underlying ontology. ›
text‹The paper proceeds by providing instances for introduction, technical sections,
examples, \<^etc>. We would like to concentrate on one --- mathematical paper oriented --- detail in the
ontology ▩‹scholarly_paper›:
@{boxed_theory_text [display]
‹doc_class technical = text_section + ...
type_synonym tc = technical
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ...
doc_class math_content = tc + ...
doc_class "definition" = math_content +
mcc :: "math_content_class" <= "defn" ...
doc_class "theorem" = math_content +
mcc :: "math_content_class" <= "thm" ...
›}›
text‹The class \<^typ>‹technical› regroups a number of text-elements that contain typical
technical content in mathematical or engineering papers: code, definitions, theorems,
lemmas, examples. From this class, the stricter class of @{typ ‹math_content›} is derived,
which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these
class definitions are omitted here). Note, however, that class identifiers can be abbreviated by
standard ⬚‹type_synonym›s for convenience and enumeration types can be defined by the
standard inductive ⬚‹datatype› definition mechanism in Isabelle, since any HOL type is admitted
for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type
definition. ›
figure*[fig01::figure,relative_width="95",file_src="''figures/definition-use-CSP.png''"]
‹ A screenshot of the integrated source with definitions ...›
text‹An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as
\<^typ>‹definition›s in terms of the ▩‹scholarly_paper›-ontology and their type-conform referencing
later is shown in \<^figure>‹fig01› in its presentation as the integrated source.
Note that the use in the ontology-generated antiquotation ⬚‹@{definition X4}›
is type-checked; referencing ▩‹X4› as ⬚‹theorem› would be a type-error and be reported directly
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing
hierarchy makes ▩‹X4› ∗‹navigable› in Isabelle/jEdit; a click will cause the IDE to present the
defining occurrence of this text-element in the integrated source.
Note, further, how \<^isadof>-commands like ⬚‹text*› interact with standard Isabelle document
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 in this text:
▪ the freeform term antiquotation, also called ∗‹cartouche›, written by
‹@{cartouche [style-parms] ‹...›}› or just by ‹‹...›› if the list of style parameters
is empty,
▪ the freeform antiquotation for theory fragments written ‹@{theory_text [style-parms] ‹...›}›
or just ▩‹⬚›‹‹...›› if the list of style parameters is empty,
▪ the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
›
figure*[fig02::figure,relative_width="95",file_src="''figures/definition-use-CSP-pdf.png''"]
‹ ... and the corresponding \<^pdf>-output.›
text‹
\<^isadof> text-elements such as ⬚‹text*› allow to have such standard term-antiquotations inside their
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 purposes.
The corresponding output of this snippet in the integrated source is shown in \<^figure>‹fig02›.
›
subsection*[scholar_pide::example]‹More Freeform Elements, and Resulting Navigation›
text‹ 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:
@{boxed_theory_text [display]‹
datatype placement = h | t | b | ht | hb
doc_class figure = text_section +
relative_width :: "int"
src :: "string"
placement :: placement
spawn_columns :: bool <= True
›}
›
figure*[fig_figures::figure,relative_width="85",file_src="''figures/Dogfood-figures.png''"]
‹ Declaring figures in the integrated source.›
text‹
The document class \<^typ>‹figure› (supported by the \<^isadof> command abbreviation
\<^boxed_theory_text>‹figure*›) makes it possible to express the pictures and diagrams
as shown in \<^figure>‹fig_figures›, which presents its own representation in the
integrated source as screenshot.›
text‹
Finally, we define a ∗‹monitor class› \<^index>‹monitor class› that enforces a textual ordering
in the document core by a regular expression:
@{boxed_theory_text [display]‹
doc_class article =
style_id :: string <= "''LNCS''"
version :: "(int × int × int)" <= "(0,0,0)"
accepts "(title ~~ ⟦subtitle⟧ ~~ ⦃author⦄⇧+ ~~ abstract ~~ ⦃introduction⦄⇧+
~~ ⦃background⦄⇧* ~~ ⦃technical || example ⦄⇧+ ~~ ⦃conclusion⦄⇧+
~~ bibliography ~~ ⦃annex⦄⇧* )"
›}›
text‹
In a integrated document source, the body of the content can be paranthesized into:
@{boxed_theory_text [display]‹
open_monitor* [this::article]
...
close_monitor*[this]
›}
which signals to \<^isadof> begin and end of the part of the integrated source
in which the text-elements instances are expected to appear in the textual ordering
defined by \<^typ>‹article›.
›
text*[exploring::float,
main_caption="‹Exploring text elements.›"]
‹
@{fig_content (width=45, caption="Exploring a reference of a text-element.") "figures/Dogfood-II-bgnd1.png"
}\<^hfill>@{fig_content (width=45, caption="Exploring the class of a text element.") "figures/Dogfood-III-bgnd-text_section.png"}
›
text*[hyperlinks::float,
main_caption="‹Navigation via generated hyperlinks.›"]
‹
@{fig_content (width=45, caption="Hyperlink to class-definition.") "figures/Dogfood-IV-jumpInDocCLass.png"
}\<^hfill>@{fig_content (width=45, caption="Exploring an attribute (hyperlinked to the class).") "figures/Dogfood-V-attribute.png"}
›
text‹
From these class definitions, \<^isadof> also automatically generated editing
support for Isabelle/jEdit. In
@{float "exploring"}(left)
% \autoref{fig-Dogfood-II-bgnd1}
and
@{float "exploring"}(right)
% \autoref{fig-bgnd-text_section}
we show how hovering over links permits to explore its
meta-information. Clicking on a document class identifier permits to hyperlink into the
corresponding class definition (
@{float "hyperlinks"}(left)
%\autoref{fig:Dogfood-IV-jumpInDocCLass})
; hovering over an attribute-definition (which is qualified in order to disambiguate; cf.
@{float "hyperlinks"}(right)
%\autoref{fig:Dogfood-V-attribute}
) shows its type.
›
figure*[figDogfoodVIlinkappl::figure,relative_width="80",file_src="''figures/Dogfood-VI-linkappl.png''"]
‹Exploring an ontological reference.›
text‹
An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the
ontology-dependant antiquotation \<^boxed_theory_text>‹@{example ‹ex1›}› refers to the corresponding
text-element \<^boxed_theory_text>‹ex1›. Hovering allows for inspection, clicking for jumping to the
definition. If the link does not exist or has a non-compatible type, the text is not validated,
\<^ie>, Isabelle/jEdit will respond with an error.›
text‹We advise users to experiment with different notation variants.
Note, further, that the Isabelle \<^latex>‹@\{cite ...\}›-text-anti-quotation makes its checking
on the level of generated ▩‹.aux›-files, which are not necessarily up-to-date. Ignoring the PIDE
error-message and compiling it with a consistent bibtex usually makes disappear this behavior.
›
subsection*["using_term_aq"::technical, main_author = "Some @{author ''bu''}"]
‹Using Term-Antiquotations›
text‹The present version of \<^isadof> is the first version that supports the novel feature of
\<^dof>-generated term-antiquotations\<^bindex>‹term-antiquotations›, \<^ie>, antiquotations embedded
in HOL-‹λ›-terms possessing arguments that were validated in the ontological context.
These ‹λ›-terms may occur in definitions, lemmas, or in values to define attributes
in class instances. They have the format: ‹@{name arg⇩1 ... arg⇩n⇩-⇩1} arg⇩n››
text‹Logically, they are defined as an identity in the last argument ‹arg⇩n›; thus,
ontologically checked prior arguments ‹arg⇩1 ... arg⇩n⇩-⇩1› can be ignored during a proof
process; ontologically, they can be used to assure the traceability of, \<^eg>, semi-formal
assumptions throughout their way to formalisation and use in lemmas and proofs. ›
figure*[doc_termAq::figure,relative_width="35",file_src="''figures/doc-mod-term-aq.pdf''"]
‹Term-Antiquotations Referencing to Annotated Elements›
text‹As shown in @{figure ‹doc_termAq›}, this feature of \<^isadof> substantially increases
the expressibility of links between the formal and the informal in \<^dof> documents.›
text‹ In the following, we describe a common scenario linking semi-formal assumptions and
formal ones:
@{boxed_theory_text [display]
‹
declare_reference*[e2::"definition"]
Assumption*[a1::"assumption", short_name="‹safe environment.›"]
‹The system shall only be used in the temperature range from 0 to 60 degrees Celsius.
Formally, this is stated as follows in @{definition (unchecked) ‹e2›}.›
definition*[e2, status=formal] safe_env :: "state ⇒ bool"
where "safe_env σ ≡ (temp σ ∈ {0 .. 60})"
theorem*[e3::"theorem"] safety_preservation::" @{assumption ‹a1›} (safe_env σ) ⟹ ... "
›}
›
text‹Note that Isabelle procedes in a strict ``declaration-before-use''-manner, \<^ie> assumes
linear visibility on all references. This also holds for the declaration of ontological
references. In order to represent cyclic dependencies, it is therefore necessary to
start with the forward declaration ⬚‹declare_reference*›. From there on, this reference
can be used in text, term, and code-contexts, albeit its definition appears textually later.
The corresponding freeform-formulation of this assumption can be explicitly referred in the
assumption of a theorem establishing the link. The ⬚‹theorem*›-variant of the common
Isabelle/Isar ⬚‹theorem›-command will in contrast to the latter not ignore ‹‹a1››,
\<^ie> parse just as string, but also validate it in the previous context.
Note that the ⬚‹declare_reference*› command will appear in the \<^LaTeX> generated from this
document fragment. In order to avoid this, one has to enclose this command into the
document comments : ‹(*<*) ... (*>*)›.›
section*[tech_onto::example]‹Writing Technical Reports in \<^boxed_theory_text>‹technical_report››
text‹While it is perfectly possible to write documents in the
▩‹technical_report› ontology in freeform-style (this manual is mostly such an
example), we will briefly explain here the tight-checking-style in which
most Isabelle reference manuals themselves are written.
The idea has already been put forward by Isabelle itself; besides the general infrastructure on
which this work is also based, current Isabelle versions provide around 20 built-in
document and code antiquotations described in the Reference Manual pp.75 ff. in great detail.
Most of them provide strict-checking, \<^ie> the argument strings were parsed and machine-checked in the
underlying logical context, which turns the arguments into ∗‹formal content› in the integrated
source, in contrast to the free-form antiquotations which basically influence the presentation.
We still mention a few of these document antiquotations here:
▪ ⬚‹@{thm \<doublequote>refl\<doublequote>}› or ⬚‹@{thm [display] \<doublequote>refl\<doublequote>}›
check that ⬚‹refl› is indeed a reference
to a theorem; the additional ``style" argument changes the presentation by printing the
formula into the output instead of the reference itself,
▪ ⬚‹@{lemma ‹prop› by method} › allows deriving ‹prop› on the fly, thus guarantee
that it is a corollary of the current context,
▪ ⬚‹@{term ‹term› }› parses and type-checks ‹term›,
▪ ⬚‹@{value ‹term› }› performs the evaluation of ‹term›,
▪ ⬚‹@{ML ‹ml-term› }› parses and type-checks ‹ml-term›,
▪ ⬚‹@{ML_file ‹ml-file› }› parses the path for ‹ml-file› and
verifies its existance in the (Isabelle-virtual) file-system.
›
text‹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
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.
Additionally, documents antiquotations were added to check and evaluate terms with
term antiquotations:
▪ ⬚‹@{term_ ‹term› }› parses and type-checks ‹term› with term antiquotations,
for instance ⬚‹\<^term_> ‹@{technical ‹isadof›}›› will parse and check
that ‹isadof› is indeed an instance of the class \<^typ>‹technical›,
▪ ⬚‹@{value_ ‹term› }› performs the evaluation of ‹term› with term antiquotations,
for instance ⬚‹@{value_ ‹definition_list @{technical ‹isadof›}›}›
will print the value of the \<^const>‹definition_list› attribute of the instance ‹isadof›.
⬚‹value_› may have an optional argument between square brackets to specify the evaluator but this
argument must be specified after a default optional argument already defined
by the text antiquotation implementation.
So one must use the following syntax if he does not want to specify the first optional argument:
⬚‹@{value_ [] [nbe] ‹definition_list @{technical ‹isadof›}›}›. Note the empty brackets.
›
declare_reference*["subsec_onto_term_ctxt"::technical]
text‹They are text-contexts equivalents to the ⬚‹term*› and ⬚‹value*› commands
for term-contexts introduced in @{technical (unchecked) ‹subsec_onto_term_ctxt›}›
subsection‹A Technical Report with Tight Checking›
text‹An example of tight checking is a small programming manual 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
is often missing in the Isabelle community.
So, if this text addresses only a very limited audience and will never be famous for its style,
it is nevertheless important to be ∗‹exact› in the sense that code-snippets and interface descriptions
should be accurate with the most recent version of Isabelle in which this document is generated.
So its value is that readers can just reuse some of these snippets and adapt them to their
purposes.
›
figure*[strict_em::figure, relative_width="95", file_src="''figures/MyCommentedIsabelle.png''"]
‹A table with a number of SML functions, together with their type.›
text‹
This manual is written according to the ▩‹technical_report› ontology in
\<^theory>‹Isabelle_DOF.technical_report›.
\<^figure>‹strict_em› shows a snippet from this integrated source and gives an idea why
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
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.
›
section‹Some Recommendations: A little Style Guide›
text‹
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
possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>:
@{boxed_theory_text [display]‹
text‹ This is \emph{emphasized} and this is a
citation~\cite{brucker.ea:isabelle-ontologies:2018}›
›}
In general, we advise against this practice and, whenever positive, use the \<^isadof> (respetively
Isabelle) provided alternatives:
@{boxed_theory_text [display]‹
text‹ This is *‹emphasized› and this is a
citation @{cite "brucker.ea:isabelle-ontologies:2018"}.›
›}
The list of standard Isabelle document antiquotations, as well as their options and styles,
can be found in the Isabelle reference manual \<^cite>‹"wenzel:isabelle-isar:2020"›,
section 4.2.
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
\<^LaTeX>-commands, but this should be restricted to layout improvements that otherwise are (currently)
not possible. As far as possible, raw \<^LaTeX> should be restricted to the definition
of ontologies and macros (see @{docitem (unchecked) ‹isadof_ontologies›}). If raw
\<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
\<^latex>‹\verb+\+\verb+<^latex>+›‹‹argument›› to isolate these parts
(cf. \<^cite>‹"wenzel:isabelle-isar:2020"›).
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can
ensure that a document that does not generate any error messages in Isabelle/jEdit also generated
a \<^pdf> document. Second, future version of \<^isadof> might support different targets for the
document generation (\<^eg>, HTML) which, naturally, are only available to documents not using
too complex native \<^LaTeX>-commands.
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
create dangling references during the document generation that break the document generation.
Finally, we recommend using the @{command "check_doc_global"} command at the end of your
document to check the global reference structure.
›
end