forked from Isabelle_DOF/Isabelle_DOF
Merge remote-tracking branch 'origin/add-todos-fix-typos'
This commit is contained in:
commit
243556467a
|
@ -137,7 +137,8 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
|
||||||
the link between formal and informal content in documents in a machine
|
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
|
checked way. These links can connect both text elements as well as formal
|
||||||
modelling elements such as terms, definitions, code and logical formulas,
|
modelling elements such as terms, definitions, code and logical formulas,
|
||||||
alltogether *\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
|
|
|
@ -91,7 +91,7 @@ text\<open>
|
||||||
by simp\<close>}
|
by simp\<close>}
|
||||||
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
|
\<^item> a green background for examples of generated document fragments (\<^ie>, PDF output):
|
||||||
@{boxed_pdf [display] \<open>The axiom refl\<close>}
|
@{boxed_pdf [display] \<open>The axiom refl\<close>}
|
||||||
\<^item> a red background for For (S)ML-code:
|
\<^item> a red background for (S)ML-code:
|
||||||
@{boxed_sml [display] \<open>fun id x = x\<close>}
|
@{boxed_sml [display] \<open>fun id x = x\<close>}
|
||||||
\<^item> a yellow background for \LaTeX-code:
|
\<^item> a yellow background for \LaTeX-code:
|
||||||
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
|
@{boxed_latex [display] \<open>\newcommand{\refl}{$x = x$}\<close>}
|
||||||
|
|
|
@ -151,7 +151,7 @@ text\<open>
|
||||||
"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"} which
|
||||||
in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle
|
in many features over-accomplishes the required features of \<^dof>. For example, current Isabelle
|
||||||
versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be
|
versions offer cascade-syntaxes (different syntaxes and even parser-technologies which can be
|
||||||
nested along the \<open>\<open>...\<close>\<close> barriers, while \<^dof> actually only requires a two-level syntax model.
|
nested along the \<open>\<open>...\<close>\<close> barriers), while \<^dof> actually only requires a two-level syntax model.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
|
figure*["fig:dof-ide"::figure,relative_width="95",src="''figures/cicm2018-combined''"]\<open>
|
||||||
|
|
|
@ -267,7 +267,7 @@ users are:
|
||||||
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
|
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
|
||||||
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
|
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
|
||||||
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
|
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
|
||||||
\<^item> The file \<^boxed_bash>\<open>praemble.tex\<close>\<^index>\<open>praemble.tex\<close>, which allows users to add additional
|
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
|
||||||
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -284,7 +284,7 @@ text\<open>
|
||||||
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
|
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
|
||||||
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
|
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
|
||||||
between statements, definitions and proofs which is ontologically tracked. However, wrt.
|
between statements, definitions and proofs which is ontologically tracked. However, wrt.
|
||||||
to the possible linking between the underlying formal theory and this mathematical presentation,
|
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,
|
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
|
||||||
deliberately not exploiting \<^isadof> 's full potential with this regard.
|
deliberately not exploiting \<^isadof> 's full potential with this regard.
|
||||||
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
|
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
|
||||||
|
@ -346,7 +346,7 @@ context of this document; this is a decisive feature of \<^isadof> that conventi
|
||||||
languages lack.\<close>
|
languages lack.\<close>
|
||||||
|
|
||||||
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
|
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
|
||||||
to \<open>figure\<close> or \<open>table\<close> or similar. Note that
|
to \<open>figure\<close> or \<open>table\<close> or similar). Note that
|
||||||
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
|
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
|
||||||
the document class definition \<open>author\<close> shown above. It is used to express which author currently
|
the document class definition \<open>author\<close> shown above. It is used to express which author currently
|
||||||
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
|
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
|
||||||
|
@ -460,10 +460,14 @@ later is shown in \<^figure>\<open>fig01\<close> in its presentation as the inte
|
||||||
|
|
||||||
Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
|
Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
|
||||||
is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
|
is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
|
||||||
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. to the sub-typing
|
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing
|
||||||
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the
|
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.
|
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
|
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.
|
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 her in this text:
|
We refrain ourselves here to briefly describe three freeform antiquotations used her in this text:
|
||||||
|
@ -528,7 +532,7 @@ doc_class related_work = conclusion +
|
||||||
\<close>}
|
\<close>}
|
||||||
*)
|
*)
|
||||||
text\<open> In the following, we present some other text-elements provided by the Common Ontology Library
|
text\<open> 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:
|
in @{theory "Isabelle_DOF.Isa_COL"}. It provides a document class for figures:
|
||||||
|
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
datatype placement = h | t | b | ht | hb
|
datatype placement = h | t | b | ht | hb
|
||||||
|
@ -559,6 +563,9 @@ text\<open>
|
||||||
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
||||||
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
||||||
bibliography)"
|
bibliography)"
|
||||||
|
% TODO:
|
||||||
|
% Update to the new implementation.
|
||||||
|
% where is deprecated and the new implementation uses accepts and rejects.
|
||||||
\<close>}
|
\<close>}
|
||||||
|
|
||||||
In a integrated document source, the body of the content can be paranthesized into:
|
In a integrated document source, the body of the content can be paranthesized into:
|
||||||
|
@ -595,6 +602,9 @@ text\<open>
|
||||||
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
|
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
|
||||||
attribute-definition (which is qualified in order to disambiguate;
|
attribute-definition (which is qualified in order to disambiguate;
|
||||||
\autoref{fig:Dogfood-V-attribute}).
|
\autoref{fig:Dogfood-V-attribute}).
|
||||||
|
% TODO for Burkhart Wolff.
|
||||||
|
% The last phrase should be completed to make it clearer:
|
||||||
|
% In this part "hovering over an...in order to disambiguate", something is missing.
|
||||||
\<close>
|
\<close>
|
||||||
(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *)
|
(* Bu : This autoref stuff could be avoided if we would finally have monitors over figures... *)
|
||||||
|
|
||||||
|
@ -651,7 +661,7 @@ text\<open>
|
||||||
which is usually a collaborative effort.
|
which is usually a collaborative effort.
|
||||||
|
|
||||||
As in many other cases, formal certification documents come with an own terminology and pragmatics
|
As in many other cases, formal certification documents come with an own terminology and pragmatics
|
||||||
of what has to be demonstrated and where, and how the trace-ability of requirements through
|
of what has to be demonstrated and where, and how the traceability of requirements through
|
||||||
design-models over code to system environment assumptions has to be assured.
|
design-models over code to system environment assumptions has to be assured.
|
||||||
|
|
||||||
In the sequel, we present a simplified version of an ontological model used in a
|
In the sequel, we present a simplified version of an ontological model used in a
|
||||||
|
@ -664,6 +674,10 @@ doc_class requirement = long_name :: "string option"
|
||||||
doc_class requirement_analysis = no :: "nat"
|
doc_class requirement_analysis = no :: "nat"
|
||||||
where "requirement_item +"
|
where "requirement_item +"
|
||||||
|
|
||||||
|
% TODO:
|
||||||
|
% Update to the new implementation.
|
||||||
|
% where is deprecated and the new implementation uses accepts and rejects.
|
||||||
|
|
||||||
doc_class hypothesis = requirement +
|
doc_class hypothesis = requirement +
|
||||||
hyp_type :: hyp_type <= physical (* default *)
|
hyp_type :: hyp_type <= physical (* default *)
|
||||||
|
|
||||||
|
@ -675,7 +689,7 @@ doc_class assumption = requirement +
|
||||||
|
|
||||||
Such ontologies can be enriched by larger explanations and examples, which may help
|
Such ontologies can be enriched by larger explanations and examples, which may help
|
||||||
the team of engineers substantially when developing the central document for a certification,
|
the team of engineers substantially when developing the central document for a certification,
|
||||||
like an explication what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
|
like an explication of what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
|
||||||
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
|
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
|
||||||
document class its definition available by a simple mouse-click, this kind on meta-knowledge
|
document class its definition available by a simple mouse-click, this kind on meta-knowledge
|
||||||
can be made far more accessible during the document evolution.
|
can be made far more accessible during the document evolution.
|
||||||
|
@ -683,23 +697,23 @@ can be made far more accessible during the document evolution.
|
||||||
For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions.
|
For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions.
|
||||||
It has formal, semi-formal and informal sub-categories. They have to be
|
It has formal, semi-formal and informal sub-categories. They have to be
|
||||||
tracked and discharged by appropriate validation procedures within a
|
tracked and discharged by appropriate validation procedures within a
|
||||||
certification process, by it by test or proof. It is different from a hypothesis, which is
|
certification process, be it by test or proof. It is different from a hypothesis, which is
|
||||||
globally assumed and accepted.
|
globally assumed and accepted.
|
||||||
|
|
||||||
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
|
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
|
||||||
is used for formal assumptions, that arise during the analysis,
|
is used for formal assumptions, that arise during the analysis,
|
||||||
design or implementation and have to be tracked till the final
|
design or implementation and have to be tracked till the final
|
||||||
evaluation target, and discharged by appropriate validation procedures
|
evaluation target, and discharged by appropriate validation procedures
|
||||||
within the certification process, by it by test or proof. A particular class of interest
|
within the certification process, be it by test or proof. A particular class of interest
|
||||||
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>srac\<close>
|
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>SRAC\<close>
|
||||||
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
|
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
|
||||||
of the evaluation target. Their track-ability throughout the certification
|
of the evaluation target. Their traceability throughout the certification
|
||||||
is therefore particularly critical. This is naturally modeled as follows:
|
is therefore particularly critical. This is naturally modeled as follows:
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
doc_class ec = assumption +
|
doc_class ec = assumption +
|
||||||
assumption_kind :: ass_kind <= (*default *) formal
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
|
|
||||||
doc_class srac = ec +
|
doc_class SRAC = ec +
|
||||||
assumption_kind :: ass_kind <= (*default *) formal
|
assumption_kind :: ass_kind <= (*default *) formal
|
||||||
\<close>}
|
\<close>}
|
||||||
|
|
||||||
|
@ -725,12 +739,18 @@ subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
|
||||||
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
|
||||||
\<open> Standard antiquotations referring to theory elements.\<close>
|
\<open> Standard antiquotations referring to theory elements.\<close>
|
||||||
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
|
||||||
conformimg to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
|
||||||
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
|
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
|
||||||
of a document get ``formal content'' and become more robust under change.\<close>
|
of a document get ``formal content'' and become more robust under change.\<close>
|
||||||
|
|
||||||
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
|
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
|
||||||
\<open> Defining a "SRAC" in the integrated source \ldots \<close>
|
\<open> Defining a "SRAC" in the integrated source \ldots \<close>
|
||||||
|
text\<open>
|
||||||
|
TODO:
|
||||||
|
The screenshot (figures/srac-definition) of the figure figfig5 should be updated
|
||||||
|
to have a SRAC type in uppercase.
|
||||||
|
\<close>
|
||||||
|
|
||||||
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
|
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
|
||||||
\<open> Using a "SRAC" as "EC" document element. \<close>
|
\<open> Using a "SRAC" as "EC" document element. \<close>
|
||||||
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an
|
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an
|
||||||
|
@ -882,14 +902,14 @@ underlying logical context, which turns the arguments into \<^emph>\<open>formal
|
||||||
source, in contrast to the free-form antiquotations which basically influence the presentation.
|
source, in contrast to the free-form antiquotations which basically influence the presentation.
|
||||||
|
|
||||||
We still mention a few of these document antiquotations here:
|
We still mention a few of these document antiquotations here:
|
||||||
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> ou \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
|
\<^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
|
to a theorem; the additional "style" argument changes the presentation by printing the
|
||||||
formula into the output instead of the reference itself,
|
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 to derive \<open>prop\<close> on the fly, thus garantee
|
||||||
that it is a corrollary of the current context,
|
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>@{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>,
|
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
|
||||||
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> pa,rses and type-checks \<open>ml-term\<close>,
|
\<^item> \<^theory_text>\<open>@{ML \<open>ml-term\<close> }\<close> parses and type-checks \<open>ml-term\<close>,
|
||||||
\<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and
|
\<^item> \<^theory_text>\<open>@{ML_file \<open>ml-file\<close> }\<close> parses the path for \<open>ml-file\<close> and
|
||||||
verifies its existance in the (Isabelle-virtual) file-system,
|
verifies its existance in the (Isabelle-virtual) file-system,
|
||||||
\<^item> ...
|
\<^item> ...
|
||||||
|
@ -900,9 +920,9 @@ Isabelle. This may be over-precise and a burden to readers not familiar with Isa
|
||||||
motivate authors to choose the aforementioned freeform-style.
|
motivate authors to choose the aforementioned freeform-style.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection\<open>A \<^verbatim>\<open>technical_report\<close> in tight-checking-style: \<open>MyCommentedIsabelle\<close> - Programming Manual \<close>
|
subsection\<open>A \<^verbatim>\<open>technical_report\<close> in tight-checking-style: \<open>TR_MyCommentedIsabelle\<close> - Programming Manual \<close>
|
||||||
|
|
||||||
text\<open>An example of tight checking is a small programming programming manual developed by the
|
text\<open>An example of tight checking is a small programming manual developed by the
|
||||||
second author in order to document programming trick discoveries while implementing in Isabelle.
|
second author in order 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
|
While not necessarily a meeting standards of a scientific text, it appears to us that this information
|
||||||
is often missing in the Isabelle community.
|
is often missing in the Isabelle community.
|
||||||
|
@ -934,9 +954,9 @@ figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabel
|
||||||
\<open>A table with a number of SML functions, together with their type.\<close>
|
\<open>A table with a number of SML functions, together with their type.\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
\<open>MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
|
\<open>TR_MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
|
||||||
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source gives an idea why
|
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
|
||||||
it tight-checking allows for keeping track of underlying Isabelle changes:
|
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
|
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.
|
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.
|
In the pdf output, these text-fragments were displayed verbatim.
|
||||||
|
@ -976,7 +996,7 @@ document generation (\<^eg>, HTML) which, naturally, are only available to docum
|
||||||
too complex native \<^LaTeX>-commands.
|
too complex native \<^LaTeX>-commands.
|
||||||
|
|
||||||
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
|
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
|
||||||
create dangeling references during the document generation that break the document generation.
|
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 to use the @{command "check_doc_global"} command at the end of your
|
||||||
document to check the global reference structure.
|
document to check the global reference structure.
|
||||||
|
|
|
@ -114,12 +114,15 @@ text\<open>
|
||||||
\<^emph>\<open>is-a\<close> relation between classes;
|
\<^emph>\<open>is-a\<close> relation between classes;
|
||||||
\<^item> classes may refer to other classes via a regular expression in a
|
\<^item> classes may refer to other classes via a regular expression in a
|
||||||
\<^emph>\<open>where\<close> clause;
|
\<^emph>\<open>where\<close> clause;
|
||||||
|
% TODO:
|
||||||
|
% Update to the new implementation.
|
||||||
|
% where is deprecated and the new implementation uses accepts and rejects.
|
||||||
\<^item> attributes may have default values in order to facilitate notation.
|
\<^item> attributes may have default values in order to facilitate notation.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
The \<^isadof> ontology specification language consists basically on a notation for document classes,
|
The \<^isadof> ontology specification language consists basically on a notation for document classes,
|
||||||
where the attributes were typed with HOL-types and can be instantiated by terms HOL-terms, \<^ie>,
|
where the attributes were typed with HOL-types and can be instantiated by HOL-terms, \<^ie>,
|
||||||
the actual parsers and type-checkers of the Isabelle system were reused. This has the particular
|
the actual parsers and type-checkers of the Isabelle system were reused. This has the particular
|
||||||
advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the
|
advantage that \<^isadof> commands can be arbitrarily mixed with Isabelle/HOL commands providing the
|
||||||
machinery for type declarations and term specifications such
|
machinery for type declarations and term specifications such
|
||||||
|
@ -146,6 +149,9 @@ text\<open>
|
||||||
classes and their inheritance relation structure meta-data of text-elements in an object-oriented
|
classes and their inheritance relation structure meta-data of text-elements in an object-oriented
|
||||||
manner, monitor classes enforce structural organization of documents via the language specified
|
manner, monitor classes enforce structural organization of documents via the language specified
|
||||||
by the regular expression enforcing a sequence of text-elements.
|
by the regular expression enforcing a sequence of text-elements.
|
||||||
|
% TODO:
|
||||||
|
% Update to the new implementation.
|
||||||
|
% where is deprecated and the new implementation uses accepts and rejects.
|
||||||
|
|
||||||
A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types.
|
A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types.
|
||||||
Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,
|
Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,
|
||||||
|
@ -153,7 +159,7 @@ text\<open>
|
||||||
\<^boxed_theory_text>\<open>_ option\<close>, \<^boxed_theory_text>\<open>_ list\<close>, \<^boxed_theory_text>\<open>_ set\<close>, or products
|
\<^boxed_theory_text>\<open>_ option\<close>, \<^boxed_theory_text>\<open>_ list\<close>, \<^boxed_theory_text>\<open>_ set\<close>, or products
|
||||||
\<^boxed_theory_text>\<open>_ \<times> _\<close>. As a consequence of the
|
\<^boxed_theory_text>\<open>_ \<times> _\<close>. As a consequence of the
|
||||||
document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions.
|
document model, ODL definitions may be arbitrarily intertwined with standard HOL type definitions.
|
||||||
Finally, document class definitions result in themselves in a HOL-types in order to allow \<^emph>\<open>links\<close>
|
Finally, document class definitions result in themselves in a HOL-type in order to allow \<^emph>\<open>links\<close>
|
||||||
to and between ontological concepts.
|
to and between ontological concepts.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -167,10 +173,13 @@ text\<open>
|
||||||
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_id\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) and identifiers
|
(called \<open>short_ident\<close>'s in @{cite "wenzel:isabelle-isar:2020"}) 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 "wenzel:isabelle-isar:2020"} for
|
||||||
details).
|
details).
|
||||||
|
% TODO for Burkhart Wolff.
|
||||||
|
% This phrase should be reviewed to clarify identifiers.
|
||||||
|
% 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 "wenzel:isabelle-isar:2020"})
|
||||||
|
@ -230,7 +239,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
||||||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||||
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
|
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
|
||||||
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
|
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>
|
||||||
An invariants can be specified as predicate over document classes represented as
|
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. Note that sufficient type information must be provided in order to
|
||||||
disambiguate the argument of the \<open>\<lambda>\<close>-expression.
|
disambiguate the argument of the \<open>\<lambda>\<close>-expression.
|
||||||
\<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
|
\<^rail>\<open> 'inv' (name '::')? '"' term '"' \<close>
|
||||||
|
@ -254,7 +263,7 @@ text\<open>
|
||||||
\inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\inlineltx{\newisadof}\<close>\<^index>\<open>document class!PDF\<close>
|
\inlineltx|\newisadof[]{}|\<^index>\<open>newisadof@\inlineltx{\newisadof}\<close>\<^index>\<open>document class!PDF\<close>
|
||||||
command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document
|
command for defining a dedicated layout for a document class in \<^LaTeX>. Such a document
|
||||||
class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific
|
class-specific \<^LaTeX>-definition can not only provide a specific layout (\<^eg>, a specific
|
||||||
highlighting, printing of certain attributes), it can also generate entries in in the table of
|
highlighting, printing of certain attributes), it can also generate entries in the table of
|
||||||
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
|
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
|
||||||
of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
|
of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
|
||||||
|
|
||||||
|
@ -276,6 +285,8 @@ text\<open>
|
||||||
representations definition needs to be wrapped in a
|
representations definition needs to be wrapped in a
|
||||||
\inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context
|
\inlineltx|\begin{isarmarkup}...\end{isamarkup}|-environment, to ensure the correct context
|
||||||
within Isabelle's \<^LaTeX>-setup.
|
within Isabelle's \<^LaTeX>-setup.
|
||||||
|
% TODO:
|
||||||
|
% For the "(written in \<^boxed_theory_text>\<open>\<open> ... \<close>\<close>" part, to give some examples should be clearer.
|
||||||
|
|
||||||
Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
|
Moreover, \<^isadof> also provides the following two variants of \inlineltx|\newisadof{}[]{}|:
|
||||||
\<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\inlineltx{\renewisadof}\<close> for re-defining
|
\<^item> \inlineltx|\renewisadof{}[]{}|\<^index>\<open>renewisadof@\inlineltx{\renewisadof}\<close> for re-defining
|
||||||
|
@ -339,7 +350,7 @@ layout (such as \<^LaTeX>); these commands have to be wrapped into
|
||||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||||
|
|
||||||
subsection\<open>Ontologic Text-Elements and their Management\<close>
|
subsection\<open>Ontologic Text-Elements and their Management\<close>
|
||||||
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open>\<open>\<close> \<dots> text \<dots> \<open>\<close>\<close> \<close> is the core-command of \<^isadof>: it permits to create
|
text\<open> \<^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>. This is viewed as the \<^emph>\<open>definition\<close> of
|
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>. This is viewed as the \<^emph>\<open>definition\<close> of
|
||||||
an instance of a document class. This instance object is attached to the text-element
|
an instance of a document class. This instance object is attached to the text-element
|
||||||
and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
|
and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
|
||||||
|
@ -1039,7 +1050,7 @@ text\<open>
|
||||||
\<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
|
\<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection\<open>Developing Ontologies and their Represenation Mappings\<close>
|
subsection\<open>Developing Ontologies and their Representation Mappings\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
The document core \<^emph>\<open>may\<close>, but \<^emph>\<open>must\<close> not use Isabelle definitions or proofs for checking the
|
The document core \<^emph>\<open>may\<close>, but \<^emph>\<open>must\<close> not use Isabelle definitions or proofs for checking the
|
||||||
formal content---this manual is actually an example of a document not containing any proof.
|
formal content---this manual is actually an example of a document not containing any proof.
|
||||||
|
@ -1194,7 +1205,7 @@ text\<open>
|
||||||
|
|
||||||
subsection\<open>Tips, Tricks, and Known Limitations\<close>
|
subsection\<open>Tips, Tricks, and Known Limitations\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
In this sectin, we sill discuss several tips and tricks for developing
|
In this section, we will discuss several tips and tricks for developing
|
||||||
new or adapting existing document templates or \<^LaTeX>-represenations of ontologies.
|
new or adapting existing document templates or \<^LaTeX>-represenations of ontologies.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
Reference in New Issue