Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Ad hoc conversion: \inlineisar|...| -> @{boxed_theory_text ... }.

This commit is contained in:
Achim D. Brucker 2020-09-08 07:30:14 +01:00
parent 3dabf4fc82
commit 37a71a613e
3 changed files with 101 additions and 101 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -462,17 +462,17 @@ figure*[fig1::figure,spawn_columns=False,relative_width="95",src="''figures/Dogf
text\<open>
@{docitem \<open>fig1\<close>} shows the corresponding view in the Isabelle/jedit of the start of an academic
paper. The text uses \<^isadof>'s own text-commands containing the meta-information provided by the
underlying ontology. We proceed by a definition of \inlineisar+introduction+'s, which we define
as the extension of \inlineisar+text_section+ which is intended to capture common infrastructure:
underlying ontology. We proceed by a definition of \<^boxed_theory_text>\<open>introduction\<close>'s, which we define
as the extension of \<^boxed_theory_text>\<open>text_section\<close> which is intended to capture common infrastructure:
@{boxed_theory_text [display]\<open>
doc_class introduction = text_section +
comment :: string
\<close>}
As a consequence of the definition as extension, the \inlineisar+introduction+ class
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
the corresponding default values.
As a consequence of the definition as extension, the \<^boxed_theory_text>\<open>introduction\<close> class
inherits the attributes \<^boxed_theory_text>\<open>main_author\<close> and \<^boxed_theory_text>\<open>todo_list\<close>
together with the corresponding default values.
We proceed more or less conventionally by the subsequent sections:
@ -507,8 +507,9 @@ figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figur
\<open> Ouroboros II: figures \ldots \<close>
text\<open>
The document class \inlineisar+figure+ (supported by the \<^isadof> command \inlineisar+figure*+)
makes it possible to express the pictures and diagrams such as @{docitem \<open>fig_figures\<close>}.
The document class \<^boxed_theory_text>\<open>figure\<close> (supported by the \<^isadof> command
\<^boxed_theory_text>\<open>figure*\<close>) makes it possible to express the pictures and diagrams
such as @{docitem \<open>fig_figures\<close>}.
Finally, we define a monitor class definition that enforces a textual ordering
in the document core by a regular expression:
@ -552,7 +553,7 @@ figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-
text\<open>
An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the
ontology-dependant antiquotation \inlineisar|@ {example ...}| refers to the corresponding
ontology-dependant antiquotation \<^boxed_theory_text>\<open>@ {example ...}\<close> refers to the corresponding
text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the
link does not exist or has a non-compatible type, the text is not validated.
\<close>
@ -759,7 +760,7 @@ type_synonym SubQuestion = string
The heart of this ontology is an alternation of questions and answers, where the answers can
consist of simple yes-no answers or lists of formulas. Since we do not assume familiarity of
the students with Isabelle (\inlineisar+term+ would assume that this is a parse-able and
the students with Isabelle (\<^boxed_theory_text>\<open>term\<close> would assume that this is a parse-able and
type-checkable entity), we basically model a derivation as a sequence of strings:
@{boxed_theory_text [display]\<open>

129
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -159,7 +159,7 @@ text\<open>
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
formal entities of Isabelle, and monitors are due to its specific application in the
Isabelle context. Conceptually, ontologies specified in ODL consist of:
\<^item> \<^emph>\<open>document classes\<close> (\inlineisar{doc_class}) that describe concepts;
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) that describe concepts;
\<^item> an optional document base class expressing single inheritance
class extensions;
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
@ -192,15 +192,15 @@ text\<open>
text\<open>
Attributes referring to other ontological concepts are called \<^emph>\<open>links\<close>. The HOL-types inside the
document specification language support built-in types for Isabelle/HOL \inlineisar+typ+'s,
\inlineisar+term+'s, and \inlineisar+thm+'s reflecting internal Isabelle's internal types for
document specification language support built-in types for Isabelle/HOL \<^boxed_theory_text>\<open>typ\<close>'s,
\<^boxed_theory_text>\<open>term\<close>'s, and \<^boxed_theory_text>\<open>thm\<close>'s reflecting internal Isabelle's internal types for
these entities; when denoted in HOL-terms to instantiate an attribute, for example, there is a
specific syntax (called \<^emph>\<open>inner syntax antiquotations\<close>) that is checked by
\isadof for consistency.
Document classes\bindex{document class}\index{class!document@see document class} support
\inlineisar+where+-clauses\index{where clause} containing a regular expression over class
names. Classes with a \inlineisar+where+ were called
\<^boxed_theory_text>\<open>where\<close>-clauses\index{where clause} containing a regular expression over class
names. Classes with a \<^boxed_theory_text>\<open>where\<close> were called
\<^emph>\<open>monitor classes\<close>.\bindex{monitor class}\index{class!monitor@see monitor class} While document
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
@ -208,8 +208,8 @@ text\<open>
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,
\inlineisar+string+ or \inlineisar+int+ as well as parameterized types, \eg, \inlineisar+_ option+,
\inlineisar+_ list+, \inlineisar+_ set+, or products \inlineisar+_ \<times> _+. As a consequence of the
\<^boxed_theory_text>\<open>string\<close> or \<^boxed_theory_text>\<open>int\<close> as well as parameterized types, \eg, \<^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
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>
to and between ontological concepts.
@ -226,8 +226,8 @@ text\<open>
\<^item> \<open>name\<close>:\index{name@\<open>name\<close>}
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
in \inlineisar+" ... "+ which might contain certain ``quasi-letters'' such
as \inlineisar+_+, \inlineisar+-+, \inlineisar+.+ (see~@{cite "wenzel:isabelle-isar:2020"} for
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
details).
\<^item> \<open>tyargs\<close>:\index{tyargs@\<open>tyargs\<close>}
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
@ -242,7 +242,6 @@ text\<open>
The \<open>name\<close>'s referred here are type names such as \<^verbatim>\<open>int\<close>, \<^verbatim>\<open>string\<close>, \<^verbatim>\<open>list\<close>, \<^verbatim>\<open>set\<close>, etc.
\<^item> \<open>type\<close>:\index{type@\<open>type\<close>}
\<^rail>\<open> (( '(' ( type * ',') ')' )? name) | typefree \<close>
\clearpage
\<^item> \<open>dt_ctor\<close>:\index{dt\_ctor@\<open>dt_ctor\<close>}
\<^rail>\<open> name (type*) (mixfix?)\<close>
\<^item> \<open>datatype_specification\<close>:\index{datatype\_specification@\<open>datatype_specification\<close>}
@ -254,9 +253,9 @@ text\<open>
\<^item> \<open>expr\<close>:\index{expr@\<open>expr\<close>}
the syntactic category \<open>expr\<close> here denotes the very rich ``inner-syntax'' language of
mathematical notations for $\lambda$-terms in Isabelle/HOL. Example expressions are:
\inlineisar|1+2| (arithmetics), \inlineisar|[1,2,3]| (lists), \inlineisar|''ab c''| (strings),
\inlineisar|{1,2,3}| (sets), \inlineisar|(1,2,3)| (tuples),
\inlineisar|\<forall> x. P(x) \<and> Q x = C| (formulas). For details, see~@{cite "nipkow:whats:2020"}.
\<^boxed_theory_text>\<open>1+2\<close> (arithmetics), \<^boxed_theory_text>\<open>[1,2,3]\<close> (lists), \<^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>\<forall> x. P(x) \<and> Q x = C\<close> (formulas). For details, see~@{cite "nipkow:whats:2020"}.
\<close>
text\<open>
@ -267,11 +266,11 @@ text\<open>
text\<open>Note that \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 \inlineisar|doc_class|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 (\inlineisar|0.thy|
is a legal theory name), this can lead to subtle problems when constructing a class: \inlineisar|foo|
can be a legal name for a type definition, the corresponding type-name \inlineisar|0.foo| is not.
For this reason, additional checks at the definition of a \inlineisar|doc_class| reject problematic
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 (\<^boxed_theory_text>\<open>0.thy\<close>
is a legal theory name), this can lead to subtle problems when constructing a class: \<^boxed_theory_text>\<open>foo\<close>
can be a legal name for a type definition, the corresponding type-name \<^boxed_theory_text>\<open>0.foo\<close> is not.
For this reason, additional checks at the definition of a \<^boxed_theory_text>\<open>doc_class\<close> reject problematic
lexical overlaps.\<close>
@ -310,7 +309,7 @@ text\<open>
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
contents or an index. Overall, the \inlineltx|\newisadof[]{}| command follows the structure
of the \inlineisar|doc_class|-command:
of the \<^boxed_theory_text>\<open>doc_class\<close>-command:
\begin{ltx}[escapechar=ë]
\newisadof{ë\<open>class_id\<close>ë}[label=,type=, ë\<open>attribute_decl\<close>ë][1]{%
@ -324,7 +323,7 @@ text\<open>
The \<open>class_id\<close> is the full-qualified name of the document class and the list of \<open>attribute_decl\<close>
needs to declare all attributes of the document class. Within the \LaTeX-definition of the document
class representation, the identifier \inlineltx|#1| refers to the content of the main text of the
document class (written in \inlineisar|\<open> ... \<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 \inlineltx|\commandkey{...}|-command (see the documentation of the
\LaTeX-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
representations definition needs to be wrapped in a
@ -344,7 +343,7 @@ text\<open>
Moreover, as usual, special care has to be taken for commands that write into aux-files
that are included in a following \LaTeX-run. For such complex examples, we refer the interested
reader, in general, to the style files provided in the \isadof distribution. In particular
the definitions of the concepts \inlineisar|title*| and \inlineisar|author*| in the file
the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the file
\path{ontologies/scholarly_paper/DOF-scholarly_paper.sty} show examples of protecting special
characters in definitions that need to make use of a entries in an aux-file.
\<close>
@ -352,7 +351,7 @@ text\<open>
subsection\<open>Common Ontology Library (COL)\<close>
text\<open>\isadof uses the concept of implicit abstract classes (or: \emph{shadow classes}).
These refer to the set of possible \inlineisar+doc_class+ declarations that posses a number
These refer to the set of possible \<^boxed_theory_text>\<open>doc_class\<close> declarations that posses a number
of attributes with their types in common. Shadow classes represent an implicit requirement
(or pre-condition) on a given class to posses these attributes in order to work properly
for certain \isadof commands.
@ -387,7 +386,7 @@ text\<open> \isadof provides a Common Ontology Library (COL)\index{Common Ontol
text\<open>
In particular it defines the super-class \inlineisar|text_element|: the
In particular it defines the super-class \<^boxed_theory_text>\<open>text_element\<close>: the
root of all text-elements,
@{boxed_theory_text [display]\<open>
@ -397,16 +396,16 @@ doc_class text_element =
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
\<close>}
Here, \inlineisar|level| defines the section-level (\eg, using a \LaTeX-inspired hierarchy:
from \inlineisar|Some -1| (corresponding to \inlineltx|\part|) to
\inlineisar|Some 0| (corresponding to \inlineltx|\chapter|, respectively, \inlineisar|chapter*|)
to \inlineisar|Some 3| (corresponding to \inlineltx|\subsubsection|, respectively,
\inlineisar|subsubsection*|). Using an invariant, a derived ontology could, \eg, require that
Here, \<^boxed_theory_text>\<open>level\<close> defines the section-level (\eg, using a \LaTeX-inspired hierarchy:
from \<^boxed_theory_text>\<open>Some -1\<close> (corresponding to \inlineltx|\part|) to
\<^boxed_theory_text>\<open>Some 0\<close> (corresponding to \inlineltx|\chapter|, respectively, \<^boxed_theory_text>\<open>chapter*\<close>)
to \<^boxed_theory_text>\<open>Some 3\<close> (corresponding to \inlineltx|\subsubsection|, respectively,
\<^boxed_theory_text>\<open>subsubsection*\<close>). Using an invariant, a derived ontology could, \eg, require that
any sequence of technical-elements must be introduced by a text-element with a higher level
(this would require that technical text section are introduce by a section element).
Similarly, we provide "minimal" instances of the \inlineisar+ASSERTION_ALIKES+
and \inlineisar+FORMAL_STATEMENT_ALIKE+ shadow classes:
Similarly, we provide "minimal" instances of the \<^boxed_theory_text>\<open>ASSERTION_ALIKES\<close>
and \<^boxed_theory_text>\<open>FORMAL_STATEMENT_ALIKE\<close> shadow classes:
@{boxed_theory_text [display]\<open>
doc_class assertions =
properties :: "term list"
@ -436,9 +435,9 @@ doc_class EC = AC +
register the definition of ECs in a dedicated table of contents (\inlineltx{tos})
and use an earlier defined environment \inlineltx|\begin{EC}...\end{EC}| for their graphical
representation. Note that the \inlineltx|\newisadof{}[]{}|-command requires the
full-qualified names, \eg, \inlineisar|t$$ext.CENELEC_50128.EC| for the document class and
\inlineisar|CENELEC_50128.requirement.long_name| for the attribute \inlineisar|long_name|,
inherited from the document class \inlineisar|requirement|. The representation of ECs
full-qualified names, \eg, \<^boxed_theory_text>\<open>text.CENELEC_50128.EC\<close> for the document class and
\<^boxed_theory_text>\<open>CENELEC_50128.requirement.long_name\<close> for the attribute \<^boxed_theory_text>\<open>long_name\<close>,
inherited from the document class \<^boxed_theory_text>\<open>requirement\<close>. The representation of ECs
can now be defined as follows:
\begin{ltx}
@ -493,18 +492,18 @@ assert*[claim::assertions] "last[1,2,3,4::int] = 4"
\<close>}
\<close>
text\<open>As an \inlineisar+ASSERTION_ALIKES+, the \inlineisar+assertions+ class possesses a
\inlineisar+properties+ attribute. The \inlineisar+assert*+ command evaluates its argument;
in case it evaluates to true the property is added to the property list of the \inlineisar+claim+ -
text-element. Commands like \inlineisar+Definitions*+ or \inlineisar+Theorem*+ work analogously.\<close>
text\<open>As an \<^boxed_theory_text>\<open>ASSERTION_ALIKES\<close>, the \<^boxed_theory_text>\<open>assertions\<close> class possesses a
\<^boxed_theory_text>\<open>properties\<close> attribute. The \<^boxed_theory_text>\<open>assert*\<close> command evaluates its argument;
in case it evaluates to true the property is added to the property list of the \<^boxed_theory_text>\<open>claim\<close> -
text-element. Commands like \<^boxed_theory_text>\<open>Definitions*\<close> or \<^boxed_theory_text>\<open>Theorem*\<close> work analogously.\<close>
subsection*["text-elements"::technical]\<open>Annotatable Top-level Text-Elements\<close>
text\<open>
While the default user interface for class definitions via the
\inlineisar|text*\<open> ... \<close>|-command allow to access all features of the document
\<^boxed_theory_text>\<open>text*\<open> ... \<close>\<close>-command allow to access all features of the document
class, \isadof provides short-hands for certain, widely-used, concepts such as
\inlineisar|title*\<open> ... \<close>| or \inlineisar|section*\<open> ... \<close>|, \eg:
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \eg:
@{boxed_theory_text [display]\<open>
title*[title::title]\<open>Isabelle/DOF\<close>
@ -554,10 +553,10 @@ text\<open>
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
commands, we refer the reader to the Isar manual~@{cite "wenzel:isabelle-isar:2020"}.
Here, we only give a brief example how the \inlineisar|section*|-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.
First, new top-level keywords need to be declared in the \inlineisar|keywords|-section of
First, new top-level keywords need to be declared in the \<^boxed_theory_text>\<open>keywords\<close>-section of
the theory header defining new keywords:
@{boxed_theory_text [display]\<open>
@ -632,24 +631,24 @@ text\<open>
\<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of
these types. They are just declared abstract types,
``inhabited'' by special constant symbols carrying strings, for
example of the format \inlineisar+<@>{thm <string>}+. When HOL
expressions were used to denote values of \inlineisar+doc_class+
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>. When HOL
expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
instance attributes, this requires additional checks after
conventional type-checking that this string represents actually a
defined entity in the context of the system state
\inlineisar+\<theta>+. For example, the \inlineisar+establish+
\<^boxed_theory_text>\<open>\<theta>\<close>. For example, the \<^boxed_theory_text>\<open>establish\<close>
attribute in the previous section is the power of the ODL: here, we model
a relation between \<^emph>\<open>claims\<close> and \<^emph>\<open>results\<close> which may be a
formal, machine-check theorem of type \inlinesml+thm+ denoted by, for
example: \inlineisar+property = "[<@>{thm ''system_is_safe''}]"+ in a
system context \inlineisar+\<theta>+ where this theorem is
example: \<^boxed_theory_text>\<open>property = "[@{thm "system_is_safe"}]"\<close> in a
system context \<^boxed_theory_text>\<open>\<theta>\<close> where this theorem is
established. Similarly, attribute values like
\inlineisar+property = "<@>{term \<open>A \<leftrightarrow> B\<close>}"+
require that the HOL-string \inlineisar+A \<leftrightarrow> B+ is
\<^boxed_theory_text>\<open>property = "@{term \<open>A \<leftrightarrow> B\<close>}"\<close>
require that the HOL-string \<^boxed_theory_text>\<open>A \<leftrightarrow> B\<close> is
again type-checked and represents indeed a formula in $\theta$. Another instance of
this process, which we call \<open>second-level type-checking\<close>, are term-constants
generated from the ontology such as
\inlineisar+<@>{definition <string>}+.
\<^boxed_theory_text>\<open>@{definition <string>}\<close>.
\<close>
@ -688,17 +687,17 @@ text\<open>
text\<open>
Monitored document sections can be nested and overlap; thus, it is
possible to combine the effect of different monitors. For example, it
would be possible to refine the \inlineisar+example+ section by its own
would be possible to refine the \<^boxed_theory_text>\<open>example\<close> section by its own
monitor and enforce a particular structure in the presentation of
examples.
Monitors manage an implicit attribute \inlineisar+trace+ containing
Monitors manage an implicit attribute \<^boxed_theory_text>\<open>trace\<close> containing
the list of ``observed'' text element instances belonging to the
accept-set. Together with the concept of ODL class invariants, it is
possible to specify properties of a sequence of instances occurring in
the document section. For example, it is possible to express that in
the sub-list of \inlineisar+introduction+-elements, the first has an
\inlineisar+introduction+ element with a \inlineisar+level+ strictly
the sub-list of \<^boxed_theory_text>\<open>introduction\<close>-elements, the first has an
\<^boxed_theory_text>\<open>introduction\<close> element with a \<^boxed_theory_text>\<open>level\<close> strictly
smaller than the others. Thus, an introduction is forced to have a
header delimiting the borders of its representation. Class invariants
on monitors allow for specifying structural properties on document
@ -708,9 +707,9 @@ text\<open>
subsubsection*["sec:class_inv"::technical]\<open>ODL Class Invariants\<close>
text\<open>
Ontological classes as described so far are too liberal in many situations. For example, one
would like to express that any instance of a \inlineisar+result+ class finally has a non-empty
property list, if its \inlineisar+kind+ is \inlineisar+p$$roof+, or that the \inlineisar+establish+
relation between \inlineisar+claim+ and \inlineisar+result+ is surjective.
would like to express that any instance of a \<^boxed_theory_text>\<open>result\<close> class finally has a non-empty
property list, if its \<^boxed_theory_text>\<open>kind\<close> is \<^boxed_theory_text>\<open>proof\<close>, or that the \<^boxed_theory_text>\<open>establish\<close>
relation between \<^boxed_theory_text>\<open>claim\<close> and \<^boxed_theory_text>\<open>result\<close> is surjective.
In a high-level syntax, this type of constraints could be expressed, \eg, by:
@ -721,11 +720,11 @@ text\<open>
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
\<close>}
where \inlineisar+result+, \inlineisar+conclusion+, and \inlineisar+introduction+ are the set of
where \<^boxed_theory_text>\<open>result\<close>, \<^boxed_theory_text>\<open>conclusion\<close>, and \<^boxed_theory_text>\<open>introduction\<close> are the set of
all possible instances of these document classes. All specified constraints are already checked
in the IDE of \dof while editing; it is however possible to delay a final error message till the
closing of a monitor (see next section). The third constraint enforces that the user sets the
\inlineisar+authored_by+ set, otherwise an error will be reported.
\<^boxed_theory_text>\<open>authored_by\<close> set, otherwise an error will be reported.
For the moment, there is no high-level syntax for the definition of class invariants. A
formulation, in SML, of the first class-invariant in \autoref{sec:class_inv} is straight-forward:
@ -744,10 +743,10 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
"tiny_cert.result" check_result_inv)
\end{sml}
The \inlinesml{setup}-command (last line) registers the \inlineisar+check_result_inv+ function
The \inlinesml{setup}-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
into the \isadof kernel, which activates any creation or modification of an instance of
\inlineisar+result+. We cannot replace \inlineisar+compute_attr_access+ by the corresponding
antiquotation \inlineisar+<@>{docitem_value kind::oid}+, since \inlineisar+oid+ is bound to a
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding
antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is bound to a
variable here and can therefore not be statically expanded.
\<close>
@ -896,7 +895,7 @@ text\<open>
The new command \inlineltx|\addauthor| and a similarly defined command \inlineltx|\addaffiliation|
can now be used in the definition of the representation of the concept
\inlineisar|text.scholarly_paper.author|, which writes the collected information in the
\<^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
(\ie, when \LaTeX's \inlineltx|\maketitle| is invoked) while \isadof allows to define authors at
@ -962,10 +961,10 @@ text\<open>
We encourage this clear and machine-checkable enforcement of restrictions while, at the same
time, we also encourage to provide a package option to overwrite them. The latter allows
inherited ontologies to overwrite these restrictions and, therefore, to provide also support
for additional document templates. For example, the ontology \inlineisar|technical_report|
extends the \inlineisar|scholarly_paper| ontology and its \LaTeX supports provides support
for additional document templates. For example, the ontology \<^boxed_theory_text>\<open>technical_report\<close>
extends the \<^boxed_theory_text>\<open>scholarly_paper\<close> ontology and its \LaTeX supports provides support
for the \inlineltx|scrrept|-class which is not supported by the \LaTeX support for
\inlineisar|scholarly_paper|.
\<^boxed_theory_text>\<open>scholarly_paper\<close>.
\<close>
subsubsection\<open>Outdated Version of \path{comment.sty}\<close>

54
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2019-2020 University of Exeter
* 2018-2019 University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -93,7 +93,7 @@ in (Data.map(apfst decl)(ctxt)
error("multiple declaration of document reference"))
end
\end{sml}
where \inlineisar+Data.map+ is the update function resulting from the instantiation of the
where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the
functor \inlinesml|Generic_Data|. This code fragment uses operations from a library structure
\inlinesml+Symtab+ that were used to update the appropriate table for document objects in
the plugin-local state. Possible exceptions to the update operation were mapped to a system-global
@ -125,7 +125,7 @@ val attributes =(Parse.$$$ "[" |-- (reference
|--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"
\end{sml}
The ``model'' \inlineisar+declare_reference_opn+ and ``new'' \inlineisar+attributes+ parts were
The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were
combined via the piping operator and registered in the Isar toplevel:
\begin{sml}
@ -144,7 +144,7 @@ declare_reference [lal::requirement, alpha="main", beta=42]
\<close>}
The construction also generates implicitly some markup information; for example, when hovering
over the \inlineisar|declare_reference| command in the IDE, a popup window with the text:
over the \<^boxed_theory_text>\<open>declare_reference\<close> command in the IDE, a popup window with the text:
``declare document reference'' will appear.
\<close>
@ -162,7 +162,7 @@ val _ = Theory.setup(
ML_Antiquotation.inline <@>{binding docitem_value}
ML_antiq_docitem_value)
\end{sml}
the text antiquotation \inlineisar+docitem+ is declared and bounded to a parser for the argument
the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument
syntax and the overall semantics. This code defines a generic antiquotation to be used in text
elements such as
@ -170,34 +170,34 @@ val _ = Theory.setup(
text\<open>as defined in <@>{docitem \<open>d1\<close>} ...\<close>
\<close>}
The subsequent registration \inlineisar+docitem_value+ binds code to a ML-antiquotation usable
The subsequent registration \<^boxed_theory_text>\<open>docitem_value\<close> binds code to a ML-antiquotation usable
in an ML context for user-defined extensions; it permits the access to the current ``value''
of document element, \ie; a term with the entire update history.
It is possible to generate antiquotations \emph{dynamically}, as a consequence of a class
definition in ODL. The processing of the ODL class \inlineisar+d$$efinition+ also \emph{generates}
a text antiquotation \inlineisar+<@>{definition \<open>d1\<close>}+, which works similar to
\inlineisar+<@>{docitem \<open>d1\<close>}+ except for an additional type-check that assures that
\inlineisar+d1+ is a reference to a definition. These type-checks support the subclass hierarchy.
definition in ODL. The processing of the ODL class \<^boxed_theory_text>\<open>definition\<close> also \emph{generates}
a text antiquotation \<^boxed_theory_text>\<open>@{definition \<open>d1\<close>}\<close>, which works similar to
\<^boxed_theory_text>\<open>@{docitem \<open>d1\<close>}\<close> except for an additional type-check that assures that
\<^boxed_theory_text>\<open>d1\<close> is a reference to a definition. These type-checks support the subclass hierarchy.
\<close>
section\<open>Implementing Second-level Type-Checking\<close>
text\<open>
On expressions for attribute values, for which we chose to use HOL syntax to avoid that users
need to learn another syntax, we implemented an own pass over type-checked terms. Stored in the
late-binding table \inlineisar+ISA_transformer_tab+, we register for each inner-syntax-annotation
late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
(ISA's), a function of type
\begin{sml}
theory -> term * typ * Position.T -> term option
\end{sml}
Executed in a second pass of term parsing, ISA's may just return \inlineisar+None+. This is
adequate for ISA's just performing some checking in the logical context \inlineisar+theory+;
Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\<open>None\<close>. This is
adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\<open>theory\<close>;
ISA's of this kind report errors by exceptions. In contrast, \<^emph>\<open>transforming\<close> ISA's will
yield a term; this is adequate, for example, by replacing a string-reference to some term denoted
by it. This late-binding table is also used to generate standard inner-syntax-antiquotations from
a \inlineisar+doc_class+.
a \<^boxed_theory_text>\<open>doc_class\<close>.
\<close>
section\<open>Programming Class Invariants\<close>
@ -219,30 +219,30 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
"tiny_cert.result" check_result_inv)
\end{sml}
The \inlinesml{setup}-command (last line) registers the \inlineisar+check_result_inv+ function
The \inlinesml{setup}-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
into the \isadof kernel, which activates any creation or modification of an instance of
\inlineisar+result+. We cannot replace \inlineisar+compute_attr_access+ by the corresponding
antiquotation \inlineisar+<@>{docitem_value kind::oid}+, since \inlineisar+oid+ is
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding
antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
bound to a variable here and can therefore not be statically expanded.
\<close>
section\<open>Implementing Monitors\<close>
text\<open>
Since monitor-clauses have a regular expression syntax, it is natural to implement them as
deterministic automata. These are stored in the \inlineisar+docobj_tab+ for monitor-objects
deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects
in the \isadof component. We implemented the functions:
\begin{sml}
val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton
\end{sml}
where \inlineisar+env+ is basically a map between internal automaton states and class-id's
(\inlineisar+cid+'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's
(\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
top-down document validation, whenever a text-element is encountered, it is checked if a monitor
is \emph{enabled} for this class; in this case, the \inlineisar+next+-operation is executed. The
transformed automaton recognizing the rest-language is stored in \inlineisar+docobj_tab+ if
possible; otherwise, if \inlineisar+next+ fails, an error is reported. The automata implementation
is \emph{enabled} for this class; in this case, the \<^boxed_theory_text>\<open>next\<close>-operation is executed. The
transformed automaton recognizing the rest-language is stored in \<^boxed_theory_text>\<open>docobj_tab\<close> if
possible; otherwise, if \<^boxed_theory_text>\<open>next\<close> fails, an error is reported. The automata implementation
is, in large parts, generated from a formalization of functional automata~\cite{nipkow.ea:functional-Automata-afp:2004}.
\<close>
@ -261,8 +261,8 @@ text\<open>
\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
\end{ltx}
The \LaTeX-generator of \isadof maps each \inlineisar{doc_item} to an \LaTeX-environment (recall
@{docitem "text-elements"}). As generic \inlineisar{doc_item} are derived from the text element,
The \LaTeX-generator of \isadof maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall
@{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element,
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \isadof's \LaTeX{} implementation.
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
@ -283,7 +283,7 @@ This environment is mapped to a plain \LaTeX command via (again, recall @{docite
\end{ltx}
For the command-based setup, \isadof provides a dispatcher that selects the most specific
implementation for a given \inlineisar|doc_class|:
implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
\begin{ltx}
%% The Isabelle/DOF dispatcher: