diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 0b611a8..5921a76 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -40,8 +40,8 @@ text\ (ODL) which allow for the definitions of document-classes and necessary datatypes, \<^item> the \<^emph>\core\ also provides an own \<^emph>\family of commands\ such as - \<^boxed_theory_text>\text*\, \<^boxed_theory_text>\declare_reference*\, \<^etc>.; - They allow for the annotation of text-elements with meta-information defined in ODL, + \<^boxed_theory_text>\text*\, \<^boxed_theory_text>\ML*\, \<^boxed_theory_text>\value*\ , \<^etc>.; + They allow for the annotation of document-elements with meta-information defined in ODL, \<^item> the \<^isadof> library \<^theory>\Isabelle_DOF.Isa_COL\ providing ontological basic (documents) concepts \<^bindex>\ontology\ as well as supporting infrastructure, \<^item> an infrastructure for ontology-specific \<^emph>\layout definitions\, exploiting this meta-information, @@ -103,8 +103,9 @@ text\ 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>\document classes\ (\<^boxed_theory_text>\doc_class\) \<^index>\doc\_class\ that describe concepts, - the keyword (\<^boxed_theory_text>\onto_class\) \<^index>\onto\_class\ is accepted equally, + the keyword (\<^boxed_theory_text>\onto_class\) \<^index>\onto\_class\ is syntactically equivalent, \<^item> an optional document base class expressing single inheritance class extensions, + restricting the class-hierarchy basically to a tree, \<^item> \<^emph>\attributes\ specific to document classes, where \<^item> attributes are HOL-typed, \<^item> attributes of instances of document elements are mutable, @@ -116,6 +117,10 @@ text\ \<^item> classes may refer to other classes via a regular expression in an \<^emph>\accepts\ clause, or via a list in a \<^emph>\rejects\ clause, \<^item> attributes may have default values in order to facilitate notation. + +\<^boxed_theory_text>\doc_class\'es and \<^boxed_theory_text>\onto_class\'es respectively, have a semantics, +\<^ie>, a logical representation as extensible records in HOL (@{cite "wenzel:isabelle-isar:2020"}, +pp. 11.6); there are therefore amenable to logical reasoning. \ text\ @@ -137,7 +142,7 @@ text\ document specification language support built-in types for Isabelle/HOL \<^boxed_theory_text>\typ\'s, \<^boxed_theory_text>\term\'s, and \<^boxed_theory_text>\thm\'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>\inner syntax antiquotations\) that is checked by + there is a specific syntax (called \<^emph>\term antiquotations\) that is checked by \<^isadof> for consistency. Document classes\<^bindex>\document class\\<^index>\class!document@see document class\ support @@ -164,7 +169,7 @@ text\ As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily mixed with standard HOL specification constructs. To make this manual self-contained, we present syntax and semantics of the specification constructs that are most likely relevant for the - developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}. Our + developer of ontologies (for more details, see~@{cite "wenzel:isabelle-isar:2020"}). Our presentation is a simplification of the original sources following the needs of ontology developers in \<^isadof>: \<^item> \name\:\<^index>\name@\name\\ @@ -200,13 +205,14 @@ text\ \<^item> \constant_definition\ :\<^index>\constant\_definition@\constant_definition\\ \<^rail>\ @@{command "definition"} name '::' type 'where' '"' name '=' \ expr '"'\ \<^item> \expr\:\<^index>\expr@\expr\\ - the syntactic category \expr\ here denotes the very rich ``inner-syntax'' language of - mathematical notations for $\lambda$-terms in Isabelle/HOL. Example expressions are: + the syntactic category \expr\ here denotes the very rich language of + mathematical notations encoded in \\\-terms in Isabelle/HOL. Example expressions are: \<^boxed_theory_text>\1+2\ (arithmetics), \<^boxed_theory_text>\[1,2,3]\ (lists), \<^boxed_theory_text>\ab c\ (strings), % TODO % Show string in the document output for \<^boxed_theory_text>\ab c\ (strings) \<^boxed_theory_text>\{1,2,3}\ (sets), \<^boxed_theory_text>\(1,2,3)\ (tuples), - \<^boxed_theory_text>\\ x. P(x) \ Q x = C\ (formulas). For details, see~@{cite "nipkow:whats:2020"}. + \<^boxed_theory_text>\\ x. P(x) \ Q x = C\ (formulas). For comprehensive overview, + see~@{cite "nipkow:whats:2020"}. \ text\ @@ -308,26 +314,39 @@ text\ special characters in definitions that need to make use of a entries in an aux-file. \ -section\Fundamental Commands of the \<^isadof> Core\ +section\The main Ontology-aware Document Elements\ text\Besides the core-commands to define an ontology as presented in the previous section, the \<^isadof> core provides a number of mechanisms to \<^emph>\use\ the resulting data to annotate -text-elements and, in some cases, terms. -In the following, we formally introduce the syntax of the core commands as -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. +texts, code, and terms. As mentioned already in the introduction, this boils down two three major +groups of commands used to annotate text-. code-, and term contexts with instances of ontological +classes, \<^ie>, meta-information specified in an ontology. Representatives of these three groups, +which refer by name to equivalent standard Isabelle commands by their name suffixed with a \*\, +are presented as follows in a railroad diagram: + + \<^item> \annotated_text_element\ : + \<^rail>\( @@{command "text*"} '[' meta_args ']' '\' text context '\' ) + \ + \<^item> \annotated_code_element\ : + \<^rail>\( @@{command "ML*"} '[' meta_args ']' '\' code context '\' ) + \ + \<^item> \annotated_term_element\ : + \<^rail>\( @@{command "value*"} '[' meta_args ']' '\' term context '\' ) + \ + +In the following, we will formally introduce the syntax of the core commands as +supported on the Isabelle/Isar level. On this basis, concepts such as the freeform +\<^theory_text>\Definition*\ and \<^theory_text>\Lemma*\ elements were derived from \<^theory_text>\text*\. Similarly,the +corresponding formal \<^theory_text>\definition*\ and \<^theory_text>\lemma*\ elements were built on top of +functionality of the \<^theory_text>\value*\-family. \ -subsection\Syntax\ -text\ +subsection\General Syntactic Elements for Document Management\ - -\ text\Recall that except \<^theory_text>\text*[]\...\\, all \<^isadof> commands were mapped to visible layout; these commands have to be wrapped into \<^verbatim>\(*<*) ... (*>*)\ if this is undesired. \ -subsection\Ontological Text-Contexts and their Management\ text\ \<^item> \obj_id\:\<^index>\obj\_id@\obj_id\\ (or \<^emph>\oid\\<^index>\oid!oid@\see obj_id\\ for short) a \<^emph>\name\ @@ -344,8 +363,6 @@ text\ \<^rail>\ (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term ) * ))\ \<^item> \annotated_text_element\ : -\<^rail>\( @@{command "text*"} '[' meta_args ']' '\' formal_text '\' ) - \ \<^rail>\ ( @@{command "open_monitor*"} | @@{command "close_monitor*"} @@ -358,8 +375,6 @@ text\ \<^item> \<^isadof> \change_status_command\ : \<^rail>\ (@@{command "update_instance*"} '[' upd_meta_args ']')\ - - With respect to the family of text elements, \<^theory_text>\text*[oid::cid, ...] \ \ text \ \ \ is the core-command of \<^isadof>: it permits to create an object of meta-data belonging to the class \<^theory_text>\cid\\<^index>\cid!cid@\see class_id\\.