Compare commits
2 Commits
e01cc2d019
...
6ad8391cc1
Author | SHA1 | Date |
---|---|---|
Achim D. Brucker | 6ad8391cc1 | |
Achim D. Brucker | 9feeb63665 |
|
@ -169,7 +169,7 @@ lemma drc_acyclic : "acyclic doc_class_rel"
|
||||||
cid_of listing := 1, cid_of figure := 1, cid_of proposition := 1)"
|
cid_of listing := 1, cid_of figure := 1, cid_of proposition := 1)"
|
||||||
show ?thesis
|
show ?thesis
|
||||||
unfolding doc_class_rel_def
|
unfolding doc_class_rel_def
|
||||||
apply(rule_tac f = "?measure" in acyclicI_order)
|
apply(rule acyclicI_order [where f = "?measure"])
|
||||||
by(simp only: class_ids)(auto)
|
by(simp only: class_ids)(auto)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
|
|
|
@ -24,17 +24,17 @@ The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\
|
||||||
digitization of knowledge and its propagation. This challenge incites numerous research efforts
|
digitization of knowledge and its propagation. This challenge incites numerous research efforts
|
||||||
summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic''
|
summarized under the labels ``semantic web,'' ``data mining,'' or any form of advanced ``semantic''
|
||||||
text processing. A key role in structuring this linking plays is \<^emph>\<open>document ontologies\<close> (also called
|
text processing. A key role in structuring this linking plays is \<^emph>\<open>document ontologies\<close> (also called
|
||||||
\<^emph>\<open>vocabulary\<close> in the semantic web community~@{cite "w3c:ontologies:2015"}), \<^ie>, a machine-readable
|
\<^emph>\<open>vocabulary\<close> in the semantic web community~\<^cite>\<open>"w3c:ontologies:2015"\<close>), \<^ie>, a machine-readable
|
||||||
form of the structure of documents as well as the document discourse.
|
form of the structure of documents as well as the document discourse.
|
||||||
|
|
||||||
Such ontologies can be used for the scientific discourse within scholarly articles, mathematical
|
Such ontologies can be used for the scientific discourse within scholarly articles, mathematical
|
||||||
libraries, and in the engineering discourse of standardized software certification
|
libraries, and in the engineering discourse of standardized software certification
|
||||||
documents~@{cite "boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"}. All these
|
documents~\<^cite>\<open>"boulanger:cenelec-50128:2015" and "cc:cc-part3:2006"\<close>. All these
|
||||||
documents contain formal content and have to follow a given structure. In practice, large groups of developers have to produce a substantial
|
documents contain formal content and have to follow a given structure. In practice, large groups of developers have to produce a substantial
|
||||||
set of documents where consistency is notoriously difficult to maintain. In particular,
|
set of documents where consistency is notoriously difficult to maintain. In particular,
|
||||||
certifications are centred around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
|
certifications are centred around the \<^emph>\<open>traceability\<close> of requirements throughout the entire
|
||||||
set of documents. While technical solutions for the traceability problem exist (most notably:
|
set of documents. While technical solutions for the traceability problem exist (most notably:
|
||||||
DOORS~@{cite "ibm:doors:2019"}), they are weak in the treatment of formal entities (such as formulas
|
DOORS~\<^cite>\<open>"ibm:doors:2019"\<close>), they are weak in the treatment of formal entities (such as formulas
|
||||||
and their logical contexts).
|
and their logical contexts).
|
||||||
|
|
||||||
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
Further applications are the domain-specific discourse in juridical texts or medical reports.
|
||||||
|
@ -53,7 +53,7 @@ the Document Ontology Framework (\<^dof>) and an implementation of \<^dof> calle
|
||||||
provers. \<^isadof> is an instance of this novel framework, implemented as an extension of Isabelle/HOL,
|
provers. \<^isadof> is an instance of this novel framework, implemented as an 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
|
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
|
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"}),
|
assertions. Based on a novel adaption of the Isabelle IDE (called PIDE, \<^cite>\<open>"wenzel:asynchronous:2014"\<close>),
|
||||||
a document is checked to be \<^emph>\<open>conform\<close> to a particular ontology---\<^isadof> is designed to give fast
|
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 the case of document
|
user-feedback \<^emph>\<open>during the capture of content\<close>. This is particularly valuable in the case of document
|
||||||
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can
|
evolution, where the \<^emph>\<open>coherence\<close> between the formal and the informal parts of the content can
|
||||||
|
@ -63,7 +63,7 @@ To avoid any misunderstanding: \<^isadof> is \<^emph>\<open>not a theory in HOL
|
||||||
track and trace links in texts. It is an \<^emph>\<open>environment to write structured text\<close> which
|
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
|
\<^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
|
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"}. However,
|
into the Isabelle/Isar framework in the style of~\<^cite>\<open>"wenzel.ea:building:2007"\<close>. However,
|
||||||
\<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
|
\<^isadof> will generate from ontologies a theory infrastructure consisting of types, terms, theorems
|
||||||
and code that allows both interactive checking and formal reasoning over meta-data
|
and code that allows both interactive checking and formal reasoning over meta-data
|
||||||
related to annotated documents.\<close>
|
related to annotated documents.\<close>
|
||||||
|
@ -113,7 +113,7 @@ CHANGELOG.md CITATION examples install LICENSE README.md ROOTS src\<close
|
||||||
subsubsection\<open>How to Cite \<^isadof>\<close>
|
subsubsection\<open>How to Cite \<^isadof>\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
If you use or extend \<^isadof> in your publications, please use
|
If you use or extend \<^isadof> in your publications, please use
|
||||||
\<^item> for the \<^isadof> system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
\<^item> for the \<^isadof> system~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>:
|
||||||
\begin{quote}\small
|
\begin{quote}\small
|
||||||
A.~D. Brucker, I.~Ait-Sadoune, N. Méric, and B.~Wolff. Using Deep Ontologies in Formal
|
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>,
|
Software Engineering. In \<^emph>\<open>International Conference on Rigorous State-Based Methods (ABZ 2023)\<close>,
|
||||||
|
@ -122,7 +122,7 @@ text\<open>
|
||||||
\end{quote}
|
\end{quote}
|
||||||
A \<^BibTeX>-entry is available at:
|
A \<^BibTeX>-entry is available at:
|
||||||
\<^url>\<open>https://www.lri.fr/~wolff/bibtex/wolff.html\<close>.
|
\<^url>\<open>https://www.lri.fr/~wolff/bibtex/wolff.html\<close>.
|
||||||
\<^item> an older description of the system~@{cite "brucker.ea:isabelle-ontologies:2018"}:
|
\<^item> an older description of the system~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>:
|
||||||
\begin{quote}\small
|
\begin{quote}\small
|
||||||
A.~D. Brucker, I.~Ait-Sadoune, P.~Crisafulli, and B.~Wolff. Using the {Isabelle} ontology
|
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
|
framework: Linking the formal with the informal. In \<^emph>\<open>Conference on Intelligent Computer
|
||||||
|
@ -132,7 +132,7 @@ text\<open>
|
||||||
\end{quote}
|
\end{quote}
|
||||||
A \<^BibTeX>-entry is available at:
|
A \<^BibTeX>-entry is available at:
|
||||||
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018\<close>.
|
\<^url>\<open>https://www.brucker.ch/bibliography/abstract/brucker.ea-isabelle-ontologies-2018\<close>.
|
||||||
\<^item> for the implementation of \<^isadof>~@{cite "brucker.ea:isabelledof:2019"}:
|
\<^item> for the implementation of \<^isadof>~\<^cite>\<open>"brucker.ea:isabelledof:2019"\<close>:
|
||||||
\begin{quote}\small
|
\begin{quote}\small
|
||||||
A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and
|
A.~D. Brucker and B.~Wolff. \<^isadof>: Design and implementation. In P.C.~{\"O}lveczky and
|
||||||
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
|
G.~Sala{\"u}n, editors, \<^emph>\<open>Software Engineering and Formal Methods (SEFM)\<close>, number 11724 in
|
||||||
|
|
|
@ -27,17 +27,17 @@ figure*[architecture::figure,relative_width="95",file_src="''figures/isabelle-ar
|
||||||
|
|
||||||
text*[bg::introduction]\<open>
|
text*[bg::introduction]\<open>
|
||||||
While Isabelle is widely perceived as an interactive theorem
|
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
|
prover for HOL (Higher-order Logic)~\<^cite>\<open>"nipkow.ea:isabelle:2002"\<close>, 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
|
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.
|
refers to the ``\<^emph>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.
|
||||||
Among other things, Isabelle provides an infrastructure for Isabelle plug-ins, comprising extensible
|
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
|
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',
|
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"}
|
with explicit infrastructure for building derivative systems.\<close>''~\<^cite>\<open>"wenzel.ea:building:2007"\<close>
|
||||||
|
|
||||||
The current system framework offers moreover the following features:
|
The current system framework offers moreover the following features:
|
||||||
\<^item> a build management grouping components into to pre-compiled sessions,
|
\<^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> a prover IDE (PIDE) framework~\<^cite>\<open>"wenzel:asynchronous:2014"\<close> with various front-ends,
|
||||||
\<^item> documentation-generation,
|
\<^item> documentation-generation,
|
||||||
\<^item> code generators for various target languages,
|
\<^item> code generators for various target languages,
|
||||||
\<^item> an extensible front-end language Isabelle/Isar, and,
|
\<^item> an extensible front-end language Isabelle/Isar, and,
|
||||||
|
@ -151,7 +151,7 @@ to switch from a text-context to a term-context, for example. Therefore, antiquo
|
||||||
literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used 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>
|
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||||
Isabelle comes with a number of built-in antiquotations for text- and code-contexts;
|
Isabelle comes with a number of built-in antiquotations for text- and code-contexts;
|
||||||
a detailed overview can be found in @{cite "wenzel:isabelle-isar:2020"}. \<^dof> reuses this general
|
a detailed overview can be found in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. \<^dof> reuses this general
|
||||||
infrastructure but \<^emph>\<open>generates\<close> its own families of antiquotations from ontologies.\<close>
|
infrastructure but \<^emph>\<open>generates\<close> its own families of antiquotations from ontologies.\<close>
|
||||||
|
|
||||||
text\<open> An example for a text-element \<^index>\<open>text-element\<close> using built-in antoquotations
|
text\<open> An example for a text-element \<^index>\<open>text-element\<close> using built-in antoquotations
|
||||||
|
@ -203,19 +203,19 @@ text\<open>
|
||||||
(protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or Coq
|
(protected by a kernel). This includes, \<^eg>, ProofPower, HOL4, HOL-light, Isabelle, or Coq
|
||||||
and its derivatives. \<^dof> is, however, designed for fast interaction in an IDE. If a user wants
|
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
|
to benefit from this experience, only Isabelle and Coq have the necessary infrastructure of
|
||||||
asynchronous proof-processing and support by a PIDE~@{cite "wenzel:asynchronous:2014" and
|
asynchronous proof-processing and support by a PIDE~\<^cite>\<open>"wenzel:asynchronous:2014" and
|
||||||
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"} which
|
"wenzel:system:2014" and "barras.ea:pervasive:2013" and "faithfull.ea:coqoon:2018"\<close> which
|
||||||
in many features over-accomplishes the required features of \<^dof>.
|
in many features over-accomplishes the required features of \<^dof>.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
figure*["fig_dof_ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\<open>
|
figure*["fig_dof_ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\<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
|
||||||
of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
|
of~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>.\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> .
|
We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> .
|
||||||
@{figure "fig_dof_ide"} shows a screenshot of an introductory paper on
|
@{figure "fig_dof_ide"} shows a screenshot of an introductory paper on
|
||||||
\<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left,
|
\<^isadof>~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>: 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.
|
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits.
|
||||||
|
@ -223,8 +223,8 @@ text\<open>
|
||||||
mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
|
mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
|
||||||
semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
|
semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
|
||||||
as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous
|
as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous
|
||||||
evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and
|
evaluation and checking of the document content~\<^cite>\<open>"wenzel:asynchronous:2014" and
|
||||||
"wenzel:system:2014" and "barras.ea:pervasive:2013"} and is dynamically extensible. Its PIDE
|
"wenzel:system:2014" and "barras.ea:pervasive:2013"\<close> and is dynamically extensible. Its PIDE
|
||||||
provides a \<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and
|
provides a \<^emph>\<open>continuous build, continuous check\<close> functionality, syntax highlighting, and
|
||||||
auto-completion. It also provides infrastructure for displaying meta-information (\<^eg>, binding
|
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
|
and type annotation) as pop-ups, while hovering over sub-expressions. A fine-grained dependency
|
||||||
|
|
|
@ -74,12 +74,12 @@ is currently consisting out of three AFP entries:
|
||||||
contains the \<^isadof> system itself, including the \<^isadof> manual.
|
contains the \<^isadof> system itself, including the \<^isadof> manual.
|
||||||
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-I\<close>: This entry contains an example of
|
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-I\<close>: This entry contains an example of
|
||||||
an academic paper written using the \<^isadof> system oriented towards an
|
an academic paper written using the \<^isadof> system oriented towards an
|
||||||
introductory paper. The text is based on~@{cite "brucker.ea:isabelle-ontologies:2018"};
|
introductory paper. The text is based on~\<^cite>\<open>"brucker.ea:isabelle-ontologies:2018"\<close>;
|
||||||
in the document, we deliberately refrain from integrating references to formal content in order
|
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
|
to demonstrate that \<^isadof> can be used for writing documents with very little direct use of
|
||||||
\<^LaTeX>.
|
\<^LaTeX>.
|
||||||
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of
|
\<^item> \<^verbatim>\<open>Isabelle_DOF-Example-II\<close>: This entry contains another example of
|
||||||
a mathematics-oriented academic paper. It is based on~@{cite "taha.ea:philosophers:2020"}.
|
a mathematics-oriented academic paper. It is based on~\<^cite>\<open>"taha.ea:philosophers:2020"\<close>.
|
||||||
It represents a typical mathematical text, heavy in definitions with complex mathematical notation
|
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
|
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
|
are ontologically tracked. However, with respect to the possible linking between the underlying formal theory
|
||||||
|
@ -289,7 +289,7 @@ contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \
|
||||||
subsection\<open>Writing Academic Publications: A Freeform Mathematics Text \<close>
|
subsection\<open>Writing Academic Publications: A Freeform Mathematics Text \<close>
|
||||||
text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
|
text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
|
||||||
paper focusing on its form, not referring in any sense to its content which is out of scope here.
|
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,
|
As mentioned before, we chose the paper~\<^cite>\<open>"taha.ea:philosophers:2020"\<close> for this purpose,
|
||||||
which is written in the so-called free-form style: Formulas are superficially parsed and
|
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
|
type-set, but no deeper type-checking and checking with the underlying logical context
|
||||||
is undertaken. \<close>
|
is undertaken. \<close>
|
||||||
|
@ -629,7 +629,7 @@ text\<open> This is *\<open>emphasized\<close> and this is a
|
||||||
citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
|
citation @{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
|
||||||
\<close>}
|
\<close>}
|
||||||
The list of standard Isabelle document antiquotations, as well as their options and styles,
|
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"},
|
can be found in the Isabelle reference manual \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
|
||||||
section 4.2.
|
section 4.2.
|
||||||
|
|
||||||
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
|
In practice, \<^isadof> documents with ambitious layout will contain a certain number of
|
||||||
|
@ -638,7 +638,7 @@ not possible. As far as possible, raw \<^LaTeX> should be restricted to the defi
|
||||||
of ontologies and macros (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}). If raw
|
of ontologies and macros (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}). If raw
|
||||||
\<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
|
\<^LaTeX> commands can not be avoided, it is recommended to use the Isabelle document comment
|
||||||
\<^latex>\<open>\verb+\+\verb+<^latex>+\<close>\<open>\<open>argument\<close>\<close> to isolate these parts
|
\<^latex>\<open>\verb+\+\verb+<^latex>+\<close>\<open>\<open>argument\<close>\<close> to isolate these parts
|
||||||
(cf. @{cite "wenzel:isabelle-isar:2020"}).
|
(cf. \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
|
||||||
|
|
||||||
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
|
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
|
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can
|
||||||
|
|
|
@ -176,7 +176,7 @@ proof(induct S)
|
||||||
then show ?case by simp
|
then show ?case by simp
|
||||||
next
|
next
|
||||||
case (Cons a S)
|
case (Cons a S)
|
||||||
then show ?case apply(auto)
|
then show ?case apply(auto)[1]
|
||||||
using concatWith.elims apply blast
|
using concatWith.elims apply blast
|
||||||
using concatWith.elims apply blast
|
using concatWith.elims apply blast
|
||||||
using list.set_cases by force
|
using list.set_cases by force
|
||||||
|
|
|
@ -119,7 +119,7 @@ text\<open>
|
||||||
\<^item> attributes may have default values in order to facilitate notation.
|
\<^item> attributes may have default values in order to facilitate notation.
|
||||||
|
|
||||||
\<^boxed_theory_text>\<open>doc_class\<close>'es and \<^boxed_theory_text>\<open>onto_class\<close>'es respectively, have a semantics,
|
\<^boxed_theory_text>\<open>doc_class\<close>'es and \<^boxed_theory_text>\<open>onto_class\<close>'es respectively, have a semantics,
|
||||||
\<^ie>, a logical representation as extensible records in HOL (@{cite "wenzel:isabelle-isar:2020"},
|
\<^ie>, a logical representation as extensible records in HOL (\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
|
||||||
pp. 11.6); there are therefore amenable to logical reasoning.
|
pp. 11.6); there are therefore amenable to logical reasoning.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -169,25 +169,25 @@ text\<open>
|
||||||
As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily
|
As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily
|
||||||
mixed with standard HOL specification constructs. To make this manual self-contained, we present
|
mixed with standard HOL specification constructs. To make this manual self-contained, we present
|
||||||
syntax and semantics of the specification constructs that are most likely relevant for the
|
syntax and semantics of the specification constructs that are most likely relevant for the
|
||||||
developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}). Our
|
developer of ontologies (for more details, see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>). Our
|
||||||
presentation is a simplification of the original sources following the needs of ontology developers
|
presentation is a simplification of the original sources following the needs of ontology developers
|
||||||
in \<^isadof>:
|
in \<^isadof>:
|
||||||
\<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close>
|
\<^item> \<open>name\<close>:\<^index>\<open>name@\<open>name\<close>\<close>
|
||||||
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
|
with the syntactic category of \<open>name\<close>'s we refer to alpha-numerical identifiers
|
||||||
(called \<open>short_ident\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
|
(called \<open>short_ident\<close>'s in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>) and identifiers
|
||||||
in \<^boxed_theory_text>\<open>...\<close> which might contain certain ``quasi-letters'' such
|
in \<^boxed_theory_text>\<open>...\<close> which might contain certain ``quasi-letters'' such
|
||||||
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
|
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close> for
|
||||||
details).
|
details).
|
||||||
% TODO
|
% TODO
|
||||||
% This phrase should be reviewed to clarify identifiers.
|
% This phrase should be reviewed to clarify identifiers.
|
||||||
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
|
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
|
||||||
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
|
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
|
||||||
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
|
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
|
||||||
\<open>typefree\<close> denotes fixed type variable (\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
|
\<open>typefree\<close> denotes fixed type variable (\<open>'a\<close>, \<open>'b\<close>, ...) (see~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>)
|
||||||
\<^item> \<open>dt_name\<close>:\<^index>\<open>dt\_npurdahame@\<open>dt_name\<close>\<close>
|
\<^item> \<open>dt_name\<close>:\<^index>\<open>dt\_npurdahame@\<open>dt_name\<close>\<close>
|
||||||
\<^rail>\<open> (tyargs?) name (mixfix?)\<close>
|
\<^rail>\<open> (tyargs?) name (mixfix?)\<close>
|
||||||
The syntactic entity \<open>name\<close> denotes an identifier, \<open>mixfix\<close> denotes the usual
|
The syntactic entity \<open>name\<close> denotes an identifier, \<open>mixfix\<close> denotes the usual
|
||||||
parenthesized mixfix notation (see @{cite "wenzel:isabelle-isar:2020"}).
|
parenthesized mixfix notation (see \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
|
||||||
The \<^emph>\<open>name\<close>'s referred here are type names such as \<^typ>\<open>int\<close>, \<^typ>\<open>string\<close>,
|
The \<^emph>\<open>name\<close>'s referred here are type names such as \<^typ>\<open>int\<close>, \<^typ>\<open>string\<close>,
|
||||||
\<^type>\<open>list\<close>, \<^type>\<open>set\<close>, etc.
|
\<^type>\<open>list\<close>, \<^type>\<open>set\<close>, etc.
|
||||||
\<^item> \<open>type_spec\<close>:\index{type_spec@\<open>type_spec\<close>}
|
\<^item> \<open>type_spec\<close>:\index{type_spec@\<open>type_spec\<close>}
|
||||||
|
@ -212,13 +212,13 @@ text\<open>
|
||||||
% Show string in the document output for \<^boxed_theory_text>\<open>ab c\<close> (strings)
|
% Show string in the document output for \<^boxed_theory_text>\<open>ab c\<close> (strings)
|
||||||
\<^boxed_theory_text>\<open>{1,2,3}\<close> (sets), \<^boxed_theory_text>\<open>(1,2,3)\<close> (tuples),
|
\<^boxed_theory_text>\<open>{1,2,3}\<close> (sets), \<^boxed_theory_text>\<open>(1,2,3)\<close> (tuples),
|
||||||
\<^boxed_theory_text>\<open>\<forall> x. P(x) \<and> Q x = C\<close> (formulas). For comprehensive overview,
|
\<^boxed_theory_text>\<open>\<forall> x. P(x) \<and> Q x = C\<close> (formulas). For comprehensive overview,
|
||||||
see~@{cite "nipkow:whats:2020"}.
|
see~\<^cite>\<open>"nipkow:whats:2020"\<close>.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
Advanced ontologies can, \<^eg>, use recursive function definitions with
|
Advanced ontologies can, \<^eg>, use recursive function definitions with
|
||||||
pattern-matching~@{cite "kraus:defining:2020"}, extensible record
|
pattern-matching~\<^cite>\<open>"kraus:defining:2020"\<close>, extensible record
|
||||||
specifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations.
|
specifications~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>, and abstract type declarations.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>\<^isadof> works internally with fully qualified names in order to avoid confusions
|
text\<open>\<^isadof> works internally with fully qualified names in order to avoid confusions
|
||||||
|
@ -290,7 +290,7 @@ text\<open>
|
||||||
class representation, the identifier \<^boxed_latex>\<open>#1\<close> refers to the content of the main text of the
|
class representation, the identifier \<^boxed_latex>\<open>#1\<close> refers to the content of the main text of the
|
||||||
document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced
|
document class (written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>) and the attributes can be referenced
|
||||||
by their name using the \<^ltxinline>\<open>\commandkey{...}\<close>-command (see the documentation of the
|
by their name using the \<^ltxinline>\<open>\commandkey{...}\<close>-command (see the documentation of the
|
||||||
\<^LaTeX>-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
|
\<^LaTeX>-package ``keycommand''~\<^cite>\<open>"chervet:keycommand:2010"\<close> for details). Usually, the
|
||||||
representations definition needs to be wrapped in a
|
representations definition needs to be wrapped in a
|
||||||
\<^ltxinline>\<open>\begin{isarmarkup}...\end{isamarkup}\<close>-environment, to ensure the correct context
|
\<^ltxinline>\<open>\begin{isarmarkup}...\end{isamarkup}\<close>-environment, to ensure the correct context
|
||||||
within Isabelle's \<^LaTeX>-setup.
|
within Isabelle's \<^LaTeX>-setup.
|
||||||
|
@ -353,7 +353,7 @@ text\<open>
|
||||||
as specified in @{technical \<open>odl_manual0\<close>}.
|
as specified in @{technical \<open>odl_manual0\<close>}.
|
||||||
\<^item> \<open>meta_args\<close> :
|
\<^item> \<open>meta_args\<close> :
|
||||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||||
\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
|
\<^item> \<^emph>\<open>evaluator\<close>: from \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>, evaluation is tried first using ML,
|
||||||
falling back to normalization by evaluation if this fails. Alternatively a specific
|
falling back to normalization by evaluation if this fails. Alternatively a specific
|
||||||
evaluator can be selected using square brackets; typical evaluators use the
|
evaluator can be selected using square brackets; typical evaluators use the
|
||||||
current set of code equations to normalize and include \<open>simp\<close> for fully
|
current set of code equations to normalize and include \<open>simp\<close> for fully
|
||||||
|
@ -433,7 +433,7 @@ term antiquotations:
|
||||||
will get the value of the \<^const>\<open>definition_list\<close> attribute of the instance \<open>odl-manual1\<close>.
|
will get the value of the \<^const>\<open>definition_list\<close> attribute of the instance \<open>odl-manual1\<close>.
|
||||||
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
|
\<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator:
|
||||||
\<^theory_text>\<open>@{value_ [nbe] \<open>definition_list @{technical \<open>odl-manual1\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
|
\<^theory_text>\<open>@{value_ [nbe] \<open>definition_list @{technical \<open>odl-manual1\<close>}\<close>}\<close> forces \<open>value_\<close> to evaluate
|
||||||
the term using normalization by evaluation (see @{cite "wenzel:isabelle-isar:2020"}).
|
the term using normalization by evaluation (see \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>).
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
|
@ -514,7 +514,7 @@ with the \<^boxed_theory_text>\<open>disable_assert_evaluation\<close> theory at
|
||||||
Then @{command "assert*"} will act like @{command "term*"}.
|
Then @{command "assert*"} will act like @{command "term*"}.
|
||||||
|
|
||||||
The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
|
The @{command "definition*"}-command allows \<open>prop\<close>, \<open>spec_prems\<close>, and \<open>for_fixes\<close>
|
||||||
(see the @{command "definition"} command in @{cite "wenzel:isabelle-isar:2020"}) to contain
|
(see the @{command "definition"} command in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>) to contain
|
||||||
term-antiquotations. For example:
|
term-antiquotations. For example:
|
||||||
@{boxed_theory_text [display]
|
@{boxed_theory_text [display]
|
||||||
\<open>doc_class A =
|
\<open>doc_class A =
|
||||||
|
@ -525,7 +525,7 @@ definition*[a1::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a
|
||||||
The @{term_ [source] \<open>@{A \<open>a1\<close>}\<close>} term-antiquotation is used both in \<open>prop\<close> and in \<open>spec_prems\<close>.
|
The @{term_ [source] \<open>@{A \<open>a1\<close>}\<close>} term-antiquotation is used both in \<open>prop\<close> and in \<open>spec_prems\<close>.
|
||||||
|
|
||||||
@{command "lemma*"}, @{command "theorem*"}, etc., are extended versions of the goal commands
|
@{command "lemma*"}, @{command "theorem*"}, etc., are extended versions of the goal commands
|
||||||
defined in @{cite "wenzel:isabelle-isar:2020"}. Term-antiquotations can be used either in
|
defined in \<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. Term-antiquotations can be used either in
|
||||||
a \<open>long_statement\<close> or in a \<open>short_statement\<close>.
|
a \<open>long_statement\<close> or in a \<open>short_statement\<close>.
|
||||||
For instance:
|
For instance:
|
||||||
@{boxed_theory_text [display]
|
@{boxed_theory_text [display]
|
||||||
|
@ -960,7 +960,7 @@ subsubsection\<open>For Isabelle Hackers: Defining New Top-Level Commands\<close
|
||||||
text\<open>
|
text\<open>
|
||||||
Defining such new top-level commands requires some Isabelle knowledge as well as
|
Defining such new top-level commands requires some Isabelle knowledge as well as
|
||||||
extending the dispatcher of the \<^LaTeX>-backend. For the details of defining top-level
|
extending the dispatcher of the \<^LaTeX>-backend. For the details of defining top-level
|
||||||
commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2020"}.
|
commands, we refer the reader to the Isar manual~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>.
|
||||||
Here, we only give a brief example how the \<^boxed_theory_text>\<open>section*\<close>-command is defined; we
|
Here, we only give a brief example how the \<^boxed_theory_text>\<open>section*\<close>-command is defined; we
|
||||||
refer the reader to the source code of \<^isadof> for details.
|
refer the reader to the source code of \<^isadof> for details.
|
||||||
|
|
||||||
|
@ -1157,7 +1157,7 @@ text\<open>
|
||||||
|
|
||||||
The \<^boxed_theory_text>\<open>\<sigma>\<close> symbol is reserved and references the future instance class.
|
The \<^boxed_theory_text>\<open>\<sigma>\<close> symbol is reserved and references the future instance class.
|
||||||
By relying on the implementation of the Records
|
By relying on the implementation of the Records
|
||||||
in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"},
|
in Isabelle/HOL~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>,
|
||||||
one can reference an attribute of an instance using its selector function.
|
one can reference an attribute of an instance using its selector function.
|
||||||
For example, \<^boxed_theory_text>\<open>int1 \<sigma>\<close> denotes the value
|
For example, \<^boxed_theory_text>\<open>int1 \<sigma>\<close> denotes the value
|
||||||
of the \<^boxed_theory_text>\<open>int1\<close> attribute
|
of the \<^boxed_theory_text>\<open>int1\<close> attribute
|
||||||
|
@ -1542,8 +1542,8 @@ text\<open>
|
||||||
Examples of this can be found, \<^eg>, in the ontology-style
|
Examples of this can be found, \<^eg>, in the ontology-style
|
||||||
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>.
|
\<^file>\<open>../../ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close>.
|
||||||
For details about the expansion mechanism
|
For details about the expansion mechanism
|
||||||
in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~@{cite "knuth:texbook:1986"
|
in general, we refer the reader to the \<^LaTeX> literature (\<^eg>,~\<^cite>\<open>"knuth:texbook:1986"
|
||||||
and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"}).
|
and "mittelbach.ea:latex:1999" and "eijkhout:latex-cs:2012"\<close>).
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -33,7 +33,7 @@ text\<open>
|
||||||
\<close>
|
\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
Semantic macros, as required by our document model, are called \<^emph>\<open>document antiquotations\<close>
|
Semantic macros, as required by our document model, are called \<^emph>\<open>document antiquotations\<close>
|
||||||
in the Isabelle literature~@{cite "wenzel:isabelle-isar:2020"}. While Isabelle's code-antiquotations
|
in the Isabelle literature~\<^cite>\<open>"wenzel:isabelle-isar:2020"\<close>. While Isabelle's code-antiquotations
|
||||||
are an old concept going back to Lisp and having found via SML and OCaml their ways into modern
|
are an old concept going back to Lisp and having found via SML and OCaml their ways into modern
|
||||||
proof systems, special annotation syntax inside documentation comments have their roots in
|
proof systems, special annotation syntax inside documentation comments have their roots in
|
||||||
documentation generators such as Javadoc. Their use, however, as a mechanism to embed
|
documentation generators such as Javadoc. Their use, however, as a mechanism to embed
|
||||||
|
@ -210,13 +210,13 @@ text\<open>
|
||||||
possible;
|
possible;
|
||||||
otherwise, if \<^boxed_sml>\<open>next\<close> fails, an error is reported. The automata implementation
|
otherwise, if \<^boxed_sml>\<open>next\<close> fails, an error is reported. The automata implementation
|
||||||
is, in large parts, generated from a formalization of functional automata
|
is, in large parts, generated from a formalization of functional automata
|
||||||
@{cite "nipkow.ea:functional-Automata-afp:2004"}.
|
\<^cite>\<open>"nipkow.ea:functional-Automata-afp:2004"\<close>.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
section\<open>The \<^LaTeX>-Core of \<^isadof>\<close>
|
section\<open>The \<^LaTeX>-Core of \<^isadof>\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
The \<^LaTeX>-implementation of \<^isadof> heavily relies on the
|
The \<^LaTeX>-implementation of \<^isadof> heavily relies on the
|
||||||
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \<^LaTeX>-commands
|
``keycommand''~\<^cite>\<open>"chervet:keycommand:2010"\<close> package. In fact, the core \<^isadof> \<^LaTeX>-commands
|
||||||
are just wrappers for the corresponding commands from the keycommand package:
|
are just wrappers for the corresponding commands from the keycommand package:
|
||||||
|
|
||||||
@{boxed_latex [display]
|
@{boxed_latex [display]
|
||||||
|
|
Loading…
Reference in New Issue