forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'v1.2.x/Isabelle2021'
This commit is contained in:
commit
f4286404fb
6
.config
6
.config
|
|
@ -1,8 +1,8 @@
|
|||
# Isabelle/DOF Version Information
|
||||
DOF_VERSION="Unreleased" # "Unreleased" for development, semantic version for releases
|
||||
DOF_LATEST_VERSION="1.1.0"
|
||||
DOF_VERSION="1.2.0" # "Unreleased" for development, semantic version for releases
|
||||
DOF_LATEST_VERSION="1.2.0"
|
||||
DOF_LATEST_ISABELLE="Isabelle2021"
|
||||
DOF_LATEST_DOI="10.5281/zenodo.4625176"
|
||||
DOF_LATEST_DOI="10.5281/zenodo.6385695"
|
||||
DOF_GENERIC_DOI="10.5281/zenodo.3370482"
|
||||
#
|
||||
# Isabelle and AFP Configuration
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#!/usr/bin/env bash
|
||||
# Copyright (c) 2019The University of Exeter.
|
||||
# 2019 The University of Paris-Saclay.
|
||||
# Copyright (c) 2019-2022 University of Exeter.
|
||||
# 2019 University of Paris-Saclay.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions
|
||||
|
|
|
|||
|
|
@ -5,11 +5,7 @@ All notable changes to this project will be documented in this file.
|
|||
The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
|
||||
and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
|
||||
|
||||
## [Unreleased]
|
||||
|
||||
### Added
|
||||
|
||||
### Changed
|
||||
## 1.2.0 - 2022-03-26
|
||||
|
||||
## 1.1.0 - 2021-03-20
|
||||
|
||||
|
|
|
|||
|
|
@ -2,8 +2,8 @@
|
|||
|
||||
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
||||
Isabelle/DOF allows for both conventional typesetting as well as formal
|
||||
development. The manual for [Isabelle/DOF 1.1.0/Isabelle2021 is available
|
||||
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.pdf)
|
||||
development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
|
||||
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
|
||||
|
||||
## Pre-requisites
|
||||
|
||||
|
|
@ -125,6 +125,10 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
|||
For releases, signed archives including a PDF version of the Isabelle/DOF manual are
|
||||
are available:
|
||||
|
||||
* Isabelle/DOF 1.2.0/Isabelle2021
|
||||
* [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
|
||||
* [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz)
|
||||
* [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc)
|
||||
* Isabelle/DOF 1.1.0/Isabelle2021
|
||||
* [Isabelle_DOF-1.1.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.pdf)
|
||||
* [Isabelle_DOF-1.1.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.tar.xz)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -134,9 +134,9 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
|
|||
|
||||
It is an unique feature of \<^isadof> that ontologies may be used to control
|
||||
the link between formal and informal content in documents in a machine
|
||||
checked way. These links can connect both text elements as well as formal
|
||||
modelling elements such as terms, definitions, code and logical formulas,
|
||||
alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
checked way. These links can connect both text elements and formal
|
||||
modeling elements such as terms, definitions, code and logical formulas,
|
||||
altogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -50,7 +50,7 @@ with Standard ML (SML) at the bottom layer as implementation language. The arch
|
|||
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>.
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
|
||||
support for higher specification constructs were built.\<close>
|
||||
|
||||
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
|
||||
|
|
@ -72,7 +72,7 @@ declare_reference*["fig:dependency"::text_section]
|
|||
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 and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
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
|
||||
|
|
@ -103,7 +103,7 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
|
|||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
|
||||
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> parenthesis) which
|
||||
contains characters and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
|
||||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 The University of Exeter
|
||||
* 2018-2021 The University of Paris-Saclay
|
||||
* 2019-2022 The University of Exeter
|
||||
* 2018-2022 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -235,7 +235,7 @@ section*[writing_doc::technical]\<open>Writing Documents: General Remarks\<close
|
|||
|
||||
subsection*[naming::example]\<open>Name-Spaces, Long- and Short-Names\<close>
|
||||
text\<open>\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were
|
||||
composed from a name of the session, the name of the theory, and a sequence of local names referring
|
||||
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
|
||||
|
||||
|
|
@ -385,10 +385,10 @@ contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<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
|
||||
paper focussing on its form, not refering 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,
|
||||
which is written in the so-called free-form style: Formulas are superficially parsed and
|
||||
type-setted, 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>
|
||||
|
||||
figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
|
||||
|
|
@ -432,8 +432,8 @@ doc_class "theorem" = math_content +
|
|||
|
||||
|
||||
text\<open>The class \<^typ>\<open>technical\<close> 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 more stricter class of @{typ \<open>math_content\<close>} is derived,
|
||||
technical content in mathematical or engineering papers: code, definitions, theorems,
|
||||
lemmas, examples. From this class, the stricter class of @{typ \<open>math_content\<close>} 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 \<^theory_text>\<open>type_synonym\<close>s for convenience and enumeration types can be defined by the
|
||||
|
|
@ -453,10 +453,6 @@ by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt.
|
|||
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jEdit; a click will cause the IDE to present the
|
||||
defining occurrence of this text-element in the integrated source.
|
||||
|
||||
% TODO:
|
||||
% The definition \<^theory_text>\<open>@{definition X4}\<close> is not present in the screenshot,
|
||||
% it might be better to use \<^theory_text>\<open>@{definition X22}\<close>.
|
||||
|
||||
Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> 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:
|
||||
|
|
@ -573,7 +569,7 @@ Isabelle/jEdit will respond with an error.\<close>
|
|||
text\<open>We advise users to experiment with different notation variants.
|
||||
Note, further, that the Isabelle \<^latex>\<open>@\{cite ...\}\<close>-text-anti-quotation makes its checking
|
||||
on the level of generated \<^verbatim>\<open>.aux\<close>-files, which are not necessarily up-to-date. Ignoring the PIDE
|
||||
error-message and compiling a with a consistent bibtex usually makes disappear this behaviour.
|
||||
error-message and compiling a with a consistent bibtex usually makes disappear this behavior.
|
||||
\<close>
|
||||
|
||||
section*[cenelec_onto::example]\<open>Writing Certification Documents \<^boxed_theory_text>\<open>CENELEC_50128\<close>\<close>
|
||||
|
|
@ -605,7 +601,7 @@ text\<open>
|
|||
much profit from the control of ontological consistency: a substantial amount of the work
|
||||
of evaluators in formal certification processes consists in tracing down the links from
|
||||
requirements over assumptions down to elements of evidence, be it in form of semi-formal
|
||||
documentation, models, code, or tests. In a certification process, traceability becomes a major
|
||||
documentation, models, code, or tests. In a certification process, traceability becomes a major
|
||||
concern; and providing mechanisms to ensure complete traceability already at the development of
|
||||
the integrated source can in our view increase the speed and reduce the risk certification
|
||||
processes. Making the link-structure machine-checkable, be it between requirements, assumptions,
|
||||
|
|
@ -675,7 +671,7 @@ text*[ass123::SRAC]\<open>
|
|||
|
||||
This will be shown in the \<^pdf> as follows:
|
||||
\<close>
|
||||
text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer
|
||||
text*[ass123::SRAC] \<open> The overall sampling frequency of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times \ldots \<close>
|
||||
|
||||
|
|
@ -722,7 +718,7 @@ We still mention a few of these document antiquotations here:
|
|||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> 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,
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee
|
||||
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows deriving \<open>prop\<close> on the fly, thus guarantee
|
||||
that it is a corrollary of the current context,
|
||||
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
|
||||
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
|
||||
|
|
@ -798,7 +794,7 @@ 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 to use the @{command "check_doc_global"} command at the end of your
|
||||
Finally, we recommend using the @{command "check_doc_global"} command at the end of your
|
||||
document to check the global reference structure.
|
||||
|
||||
\<close>
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 University of Exeter
|
||||
* 2018-2021 University of Paris-Saclay
|
||||
* 2019-2022 University of Exeter
|
||||
* 2018-2022 University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -38,8 +38,8 @@ text\<open>
|
|||
|
||||
\<^isadof> consists consists basically of five components:
|
||||
\<^item> the \<^emph>\<open>core\<close> in \<^theory>\<open>Isabelle_DOF.Isa_DOF\<close> providing the \<^emph>\<open>ontology definition language\<close>
|
||||
(called ODL) which allow for the definitions of document-classes
|
||||
and necessary auxiliary datatypes,
|
||||
(ODL) which allow for the definitions of document-classes
|
||||
and necessary datatypes,
|
||||
\<^item> the \<^emph>\<open>core\<close> also provides an own \<^emph>\<open>family of commands\<close> such as
|
||||
\<^boxed_theory_text>\<open>text*\<close>, \<^boxed_theory_text>\<open>declare_reference*\<close>, \<^etc>.;
|
||||
They allow for the annotation of text-elements with meta-information defined in ODL,
|
||||
|
|
@ -57,12 +57,12 @@ text\<open>
|
|||
system-extensions. Ontologies in \<^isadof> are not just a sequence of descriptions in
|
||||
\<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated
|
||||
sources that provide textual descriptions, abbreviations, macro-support and even ML-code.
|
||||
Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close>
|
||||
organisation is slightly different and shown in
|
||||
Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>The \<^emph>\<open>technical\<close>
|
||||
organization is slightly different and shown in
|
||||
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>:
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.1 COL\DTcomment{The Common Ontology Library}.
|
||||
.2 scholarly\_paper\DTcomment{Scientific Papers}.
|
||||
|
|
@ -88,9 +88,9 @@ text\<open>
|
|||
"knowledge-based" search procedures as well as tool interaction). For this reason, ontologies
|
||||
are coupled with \<^emph>\<open>layout definitions\<close> allowing an automatic mapping of an integrated
|
||||
source into \<^LaTeX> and finally \<^pdf>. The mapping of an ontology to a specific representation
|
||||
in \<^LaTeX> is steered via associated \<^LaTeX> stylefiles which were included during Isabelle's
|
||||
in \<^LaTeX> is steered via associated \<^LaTeX> style files which were included during Isabelle's
|
||||
document generation process. This mapping is potentially a one-to-many mapping;
|
||||
this implies a certain technical organisation and some resulting restrictions
|
||||
this implies a certain technical organization and some resulting restrictions
|
||||
described in @{technical (unchecked) \<open>infrastructure\<close>} in more detail.
|
||||
\<close>
|
||||
|
||||
|
|
@ -216,7 +216,7 @@ text\<open>
|
|||
specifications~@{cite "wenzel:isabelle-isar:2020"}, and abstract type declarations.
|
||||
\<close>
|
||||
|
||||
text\<open>Note that \<^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
|
||||
occurring otherwise, for example, in disjoint class hierarchies. This also extends to names for
|
||||
\<^boxed_theory_text>\<open>doc_class\<close>es, which must be representable as type-names as well since they
|
||||
can be used in attribute types. Since theory names are lexically very liberal
|
||||
|
|
@ -241,7 +241,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
|
||||
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
|
||||
Invariants can be specified as predicates over document classes represented as
|
||||
records in HOL. Note that sufficient type information must be provided in order to
|
||||
records in HOL. Sufficient type information must be provided in order to
|
||||
disambiguate the argument of the expression
|
||||
and the \<^boxed_text>\<open>\<sigma>\<close> symbol is reserved to reference the instance of the class itself.
|
||||
\<^rail>\<open> 'invariant' (name '::' '"' term '"' + 'and') \<close>
|
||||
|
|
@ -317,7 +317,7 @@ text-elements and, in some cases, terms.
|
|||
|
||||
subsection\<open>Syntax\<close>
|
||||
text\<open>In the following, we formally introduce the syntax of the core commands as
|
||||
supported on the Isabelle/Isar level. Note that some more advanced functionality of the core
|
||||
supported on the Isabelle/Isar level. Some more advanced functionality of the core
|
||||
is currently only available in the SML API's of the kernel.
|
||||
|
||||
\<^item> \<open>obj_id\<close>:\<^index>\<open>obj\_id@\<open>obj_id\<close>\<close> (or \<^emph>\<open>oid\<close>\<^index>\<open>oid!oid@\<open>see obj_id\<close>\<close> for short) a \<^emph>\<open>name\<close>
|
||||
|
|
@ -355,11 +355,11 @@ is currently only available in the SML API's of the kernel.
|
|||
| @@{command "define_macro*"} name ('\<rightleftharpoons>' | '==')
|
||||
\<newline> '\<open>' string '\<close>' '_' '\<open>' string '\<close>' \<close>
|
||||
\<close>
|
||||
text\<open>Recall that with the exception of \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
layout (such as \<^LaTeX>); these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||
text\<open>Recall that except \<^theory_text>\<open>text*[]\<open>...\<close>\<close>, all \<^isadof> commands were mapped to visible
|
||||
layout; these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontologic Text-Contexts and their Management\<close>
|
||||
subsection\<open>Ontological Text-Contexts and their Management\<close>
|
||||
text\<open> With respect to the family of text elements,
|
||||
\<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>\<^index>\<open>cid!cid@\<open>see class_id\<close>\<close>.
|
||||
|
|
@ -368,7 +368,7 @@ The class invariants were checked for all attribute values
|
|||
at creation time if not specified otherwise. Unspecified attributed values were represented
|
||||
by fresh free variables.
|
||||
This instance object is attached to the text-element
|
||||
and makes it thus ``trackable" for \<^isadof>, \<^ie>, it can be referenced
|
||||
and makes it thus ``trackable'' for \<^isadof>, \<^ie>, it can be referenced
|
||||
via the \<^theory_text>\<open>oid\<close>\<^index>\<open>oid!oid@\<open>see obj_id\<close>\<close>, its attributes
|
||||
can be set by defaults in the class-definitions, or set at creation time, or modified at any
|
||||
point after creation via \<^theory_text>\<open>update_instance*[oid, ...]\<close>. The \<^theory_text>\<open>class_id\<close> is syntactically optional;
|
||||
|
|
@ -389,7 +389,7 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
|
|||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Code-Contexts and their Management\<close>
|
||||
subsection\<open>Ontological Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly:
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
|
|
@ -399,10 +399,10 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
|
|||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Term-Contexts and their Management\<close>
|
||||
subsection\<open>Ontological Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
||||
Wrt. creation, track-ability and checking they are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
||||
|
|
@ -413,7 +413,7 @@ denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> e
|
|||
executable HOL-functions to interact with meta-objects.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
\<close>
|
||||
|
|
@ -485,7 +485,7 @@ text\<open>
|
|||
that introduces several ontology concepts; its overall class-tree it provides looks as follows:
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 Isa\_COL.text\_element.
|
||||
|
|
@ -511,7 +511,7 @@ doc_class text_element =
|
|||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||
\<close>}
|
||||
|
||||
As mentioned in @{technical \<open>sss\<close>} (without explaining the origin of \<^typ>\<open>text_element\<close>),
|
||||
As mentioned in @{technical \<open>sss\<close>},
|
||||
\<^const>\<open>level\<close> defines the section-level (\<^eg>, using a \<^LaTeX>-inspired hierarchy:
|
||||
from \<^boxed_theory_text>\<open>Some -1\<close> (corresponding to \<^boxed_latex>\<open>\part\<close>) to
|
||||
\<^boxed_theory_text>\<open>Some 0\<close> (corresponding to \<^boxed_latex>\<open>\chapter\<close>, respectively, \<^boxed_theory_text>\<open>chapter*\<close>)
|
||||
|
|
@ -543,9 +543,9 @@ abbreviations:
|
|||
)
|
||||
\<close>
|
||||
\<close>
|
||||
text\<open> Note that the command syntax follows the implicit convention to add a "*" to
|
||||
the command in order to distinguish them from the standard Isabelle text-commands
|
||||
which are not "ontology-aware" but function similar otherwise.\<close>
|
||||
text\<open>The command syntax follows the implicit convention to add a ``*''
|
||||
to distinguish them from the (similar) standard Isabelle text-commands
|
||||
which are not ontology-aware.\<close>
|
||||
|
||||
subsection*["text-elements"::technical]\<open>The Ontology \<^verbatim>\<open>scholarly_paper\<close>\<close>
|
||||
(*<*)
|
||||
|
|
@ -556,14 +556,11 @@ ML\<open>writeln (DOF_core.print_doc_class_tree
|
|||
toLaTeX)\<close>
|
||||
(*>*)
|
||||
text\<open> The \<^verbatim>\<open>scholarly_paper\<close> ontology is oriented towards the classical domains in science:
|
||||
\<^enum> mathematics
|
||||
\<^enum> informatics
|
||||
\<^enum> natural sciences
|
||||
\<^enum> technology and/or engineering
|
||||
mathematics, informatics, natural sciences, technology, or engineering.
|
||||
|
||||
It extends \<^verbatim>\<open>COL\<close> by the following concepts:
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 scholarly\_paper.title.
|
||||
|
|
@ -659,19 +656,19 @@ of the \<^isadof> language:
|
|||
text\<open>Usually, command macros for text elements will assign the generated instance
|
||||
to the default class corresponding for this class.
|
||||
For pragmatic reasons, \<^theory_text>\<open>Definition*\<close>, \<^theory_text>\<open>Lemma*\<close> and \<^theory_text>\<open>Theorem*\<close> represent an exception
|
||||
of this rule and are set up such that the default class is the super class @{typ \<open>math_content\<close>}
|
||||
to this rule and are set up such that the default class is the super class @{typ \<open>math_content\<close>}
|
||||
(rather than to the class @{typ \<open>definition\<close>}).
|
||||
This way, it is possible to use these macros for several different sorts of the very generic
|
||||
concept ``definition", which can be used as a freeform mathematical definition but also for a
|
||||
This way, it is possible to use these macros for several sorts of the very generic
|
||||
concept ``definition'', which can be used as a freeform mathematical definition but also for a
|
||||
freeform terminological definition as used in certification standards. Moreover, new subclasses
|
||||
of @{typ \<open>math_content\<close>} might be introduced in a derived ontology with an own specific layout
|
||||
definition.
|
||||
\<close>
|
||||
|
||||
text\<open>While this library is intended to give a lot of space to freeform text elements in
|
||||
order to counterbalance Isabelle's standard view, it should not be forgot that the real strength
|
||||
of Isabelle is its ability to handle both - and to establish links between both worlds.
|
||||
Therefore the formal assertion command has been integrated to capture some form of formal content.\<close>
|
||||
order to counterbalance Isabelle's standard view, it should not be forgotten that the real strength
|
||||
of Isabelle is its ability to handle both, and to establish links between both worlds.
|
||||
Therefore, the formal assertion command has been integrated to capture some form of formal content.\<close>
|
||||
|
||||
|
||||
subsubsection*["text-elements-expls"::example]\<open>Examples\<close>
|
||||
|
|
@ -742,7 +739,7 @@ high-level arranged at root-class level,
|
|||
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 technical\_report.front\_matter\DTcomment{...}.
|
||||
|
|
@ -777,7 +774,7 @@ appropriate for this type of long-and-tedious documents,
|
|||
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.0 .
|
||||
.1 CENELEC\_50128.judgement\DTcomment{...}.
|
||||
|
|
@ -924,7 +921,7 @@ val _ =
|
|||
|
||||
text\<open>
|
||||
Finally, for the document generation, a new dispatcher has to be defined in \<^LaTeX>---this is
|
||||
mandatory, otherwise the document generation will break. These dispatcher always follow the same
|
||||
mandatory, otherwise the document generation will break. These dispatchers always follow the same
|
||||
schemata:
|
||||
|
||||
\begin{ltx}
|
||||
|
|
@ -1068,7 +1065,7 @@ text\<open>
|
|||
The value of each attribute defined for the instances is checked against their classes invariants.
|
||||
As the class \<^boxed_theory_text>\<open>class_inv2\<close> is a subsclass
|
||||
of the class \<^boxed_theory_text>\<open>class_inv1\<close>, it inherits \<^boxed_theory_text>\<open>class_inv1\<close> invariants.
|
||||
Hence the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
|
||||
Hence, the \<^boxed_theory_text>\<open>inv1\<close> invariant is checked
|
||||
when the instance \<^boxed_theory_text>\<open>testinv2\<close> is defined.
|
||||
|
||||
Now let's add some invariants to our example in \<^technical>\<open>sec:example\<close>.
|
||||
|
|
@ -1157,7 +1154,7 @@ text\<open>
|
|||
header delimiting the borders of its representation. Class invariants
|
||||
on monitors allow for specifying structural properties on document
|
||||
sections.
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use the
|
||||
For now, the high-level syntax of invariants is not supported for monitors and you must use
|
||||
the low-level class invariants (see \<^technical>\<open>sec:low_level_inv\<close>.\<close>
|
||||
|
||||
|
||||
|
|
@ -1204,8 +1201,8 @@ text\<open>
|
|||
This paves the way for a new mechanism to query the ``current'' instances presented as a
|
||||
HOL \<^type>\<open>list\<close>.
|
||||
Arbitrarily complex queries can therefore be defined inside the logical language.
|
||||
Thus, to get the list of the properties of the instances of the class \<open>result\<close>,
|
||||
or to get the list of the authors of the instances of the \<open>introduction\<close> class,
|
||||
To get the list of the properties of the instances of the class \<open>result\<close>,
|
||||
or to get the list of the authors of the instances of \<open>introduction\<close>,
|
||||
it suffices to treat this meta-data as usual:
|
||||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>map (result.property) @{result-instances}\<close>
|
||||
|
|
@ -1216,7 +1213,7 @@ value*\<open>map (text_section.authored_by) @{introduction-instances}\<close>
|
|||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>filter (\<lambda>\<sigma>. result.evidence \<sigma> = proof) @{result-instances}\<close>
|
||||
\<close>}
|
||||
Analogously, the list of the instances of the class \<open>introduction\<close> whose \<open>level\<close> > 1,
|
||||
The list of the instances of the class \<open>introduction\<close> whose \<open>level\<close> > 1,
|
||||
can be filtered by:
|
||||
@{theory_text [display,indent=5, margin=70] \<open>
|
||||
value*\<open>filter (\<lambda>\<sigma>. the (text_section.level \<sigma>) > 1)
|
||||
|
|
@ -1252,10 +1249,10 @@ text\<open>
|
|||
the Isabelle proof language, for example, or other more advanced concepts.
|
||||
|
||||
Technically, ontologies\<^index>\<open>ontology!directory structure\<close> are stored in a directory
|
||||
\<^boxed_bash>\<open>src/ontologies\<close> and consist of a Isabelle theory file and a \<^LaTeX>-style file:
|
||||
\<^boxed_bash>\<open>src/ontologies\<close> and consist of an Isabelle theory file and a \<^LaTeX>-style file:
|
||||
%
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.1 .
|
||||
.2 src.
|
||||
|
|
@ -1276,7 +1273,7 @@ text\<open>
|
|||
\end{center}
|
||||
\<close>
|
||||
text\<open>
|
||||
Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires, from a technical perspective, the
|
||||
Developing a new ontology ``\<^boxed_bash>\<open>foo\<close>'' requires the
|
||||
following steps:
|
||||
\<^item> create a new sub-directory \<^boxed_bash>\<open>foo\<close> in the directory \<^boxed_bash>\<open>src/ontologies\<close>
|
||||
\<^item> definition of the ontological concepts, using \<^isadof>'s Ontology Definition Language (ODL), in
|
||||
|
|
@ -1293,12 +1290,11 @@ text\<open>
|
|||
subsection\<open>Document Templates\<close>
|
||||
text\<open>
|
||||
Document-templates\<^index>\<open>document template\<close> define the overall layout (page size, margins, fonts,
|
||||
etc.) of the generated documents and are the main technical means for implementing layout
|
||||
requirements that are, \<^eg>, required by publishers or standardization bodies. Document-templates
|
||||
etc.) of the generated documents. Document-templates
|
||||
are stored in a directory
|
||||
\<^path>\<open>src/document-templates\<close>:\<^index>\<open>document template!directory structure\<close>
|
||||
\begin{center}
|
||||
\begin{minipage}{.9\textwidth}\small
|
||||
\begin{minipage}{.9\textwidth}\footnotesize
|
||||
\dirtree{%
|
||||
.1 .
|
||||
.2 src.
|
||||
|
|
@ -1315,7 +1311,7 @@ text\<open>
|
|||
text\<open>
|
||||
Developing a new document template ``\<^boxed_bash>\<open>bar\<close>'' requires the following steps:
|
||||
\<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
|
||||
\<^item> activation of the new document template by executing the install script. You can skip the lengthy
|
||||
\<^item> activation of the new document template by executing the \<^boxed_bash>\<open>install\<close> script. You can skip the lengthy
|
||||
checks for the AFP entries and the installation of the Isabelle patch by using the
|
||||
\<^boxed_bash>\<open>--skip-afp\<close> option:
|
||||
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
|
||||
|
|
@ -1333,11 +1329,9 @@ subsection\<open>The Core Template\<close>
|
|||
|
||||
text\<open>
|
||||
Document-templates\<^bindex>\<open>document template\<close> define the overall layout (page size, margins, fonts,
|
||||
etc.) of the generated documents and are the main technical means for implementing layout
|
||||
requirements that are, \<^eg>, required by publishers or standardization bodies.
|
||||
etc.) of the generated documents.
|
||||
If a new layout is already supported by a \<^LaTeX>-class, then developing basic support for it
|
||||
is straightforward: after reading the authors guidelines of the new template,
|
||||
developing basic support for a new document template is straightforward. In most cases, it is
|
||||
is straightforward: In most cases, it is
|
||||
sufficient to replace the document class in \autoref{lst:dc} of the template and add the
|
||||
\<^LaTeX>-packages that are (strictly) required by the used \<^LaTeX>-setup. In general, we recommend
|
||||
to only add \<^LaTeX>-packages that are always necessary for this particular template, as loading
|
||||
|
|
@ -1390,7 +1384,7 @@ text\<open>
|
|||
|
||||
subsubsection\<open>Getting Started\<close>
|
||||
text\<open>
|
||||
In general, we recommend to create a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
|
||||
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
|
||||
to develop new document templates or ontology representations. The default setup of the \<^isadof>
|
||||
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
|
||||
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:
|
||||
|
|
@ -1468,8 +1462,8 @@ The new command \<^boxed_latex>\<open>\addauthor\<close> and a similarly defined
|
|||
can now be used in the definition of the representation of the concept
|
||||
\<^boxed_theory_text>\<open>text.scholarly_paper.author\<close>, which writes the collected information in the
|
||||
job's aux-file. The intermediate step of writing this information into the job's aux-file is necessary,
|
||||
as the author and affiliation information is required right at the begin of the document
|
||||
while \<^isadof> allows to define authors at any place within a document:
|
||||
as the author and affiliation information is required right at the beginning of the document
|
||||
while \<^isadof> allows defining authors at any place within a document:
|
||||
|
||||
\begin{ltx}
|
||||
\provideisadof{text.scholarly_paper.author}%
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019-2021 University of Exeter
|
||||
* 2018-2021 University of Paris-Saclay
|
||||
* 2019-2022 University of Exeter
|
||||
* 2018-2022 University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -92,7 +92,7 @@ op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
|
|||
op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
|
||||
op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
|
||||
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
|
||||
combinators have the advantage that they can be smoothlessly integrated into standard programs,
|
||||
combinators have the advantage that they can be integrated into standard programs,
|
||||
and they enable the dynamic extension of the grammar. There is a more high-level structure
|
||||
\inlinesml{Parse} providing specific combinators for the command-language Isar:
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue