diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 93ea350..6e8a8fe 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -36,14 +36,18 @@ abstract*[abs, keywordlist="[\Ontologies\,\Formal Documents\< Thus, \<^dof> is designed to annotate and interact with typed meta-data within formal developments in Isabelle. - While prior versions of \<^dof> provided already a mechanism to check ontological \<^emph>\rules\ - (in OWL terminology) or \<^emph>\class invariants\ (in UML/OCL terminology) via hand-written SML test-code, - we provide in this paper a novel mechanism to specify \<^emph>\invariants\ in \<^hol> via a reflection - mechanism. This allows for both efficient run-time checking of abstract properties of formal +% While prior versions of \<^dof> provided already a mechanism to check ontological \<^emph>\rules\ +% (in OWL terminology) or \<^emph>\class invariants\ (in UML/OCL terminology) via hand-written SML test-code, +% we provide in this paper a novel mechanism to specify \<^emph>\invariants\ in \<^hol> via a reflection +% mechanism. + In this paper we extend \<^dof> with \<^emph>\invariants\ via a reflection mechanism, + which serve as equivalent to the concept of ontological \<^emph>\rules\ (in OWL terminology) or + \<^emph>\class invariants\ (in UML/OCL terminology). + This allows for both efficient run-time checking of abstract properties of formal content \<^bold>\as well as\ formal proofs that establish mappings between different ontologies in general and specific ontology instances in concrete cases. With this feature widely called \<^emph>\ontology mapping\ in the literature, our framework paves the - way for a deeper integration of ontological information in + way for a deeper integration of ontological information in, for example, the articles of the Archive of Formal Proofs. \ @@ -58,19 +62,20 @@ Formal Proofs @{cite "AFP-ref22"}, which passed the impressive numbers of 650 ar written by 420 authors at the beginning of 2022. Still, while the problem of logical consistency even under system-changes and pervasive theory evolution is technically solved via continuous proof-checking, the problem of knowledge retrieval and of linking semi-formal explanations to -definitions and proofs remains largely unresolved. +definitions and proofs remains largely open. The \<^emph>\knowledge\ problem of the increasingly massive \<^emph>\digital information\ available incites numerous research efforts summarized under the labels ``semantic web'', ``integrated document management'', or any form of advanced ``semantic'' text processing. -The central role in these technologies, that are increasingly important in jurisprudence, -medical research and life-sciences in order to tame their respective publication tsunamies, -is played by \<^emph>\document ontologies\, \<^ie>, a machine-readable form of meta-data attached to -document-elements as well as their document discourse. In order to make these techniques -applicable to the area of \<^emph>\formal theory development\, -the following is needed: +These technologies are increasingly important in jurisprudence, medical research and +life-sciences in order to tame their respective publication tsunamies. The central role +in these technologies is played by \<^emph>\document ontologies\, \<^ie>, a machine-readable form +of meta-data attached to document-elements as well as their document discourse. In order +to make these techniques applicable to the area of \<^emph>\formal theory development\, +the following is needed: \<^vs>\0.2cm\ + \<^item> a general mechanism to define and develop \<^emph>\domain-specific\ ontologies, -\<^item> this mechanism should be adapted to entities occurring in formal theories, +\<^item> ... that should be adapted to entities occurring in formal theories, \<^ie>, provide built-in support for types, terms, theorems, proofs, etc., \<^item> ways to annotate meta-data generated by ontologies to the document elements, as ``deep'' as possible, together with strong validation checks, @@ -81,62 +86,56 @@ the following is needed: @{cite "books/daglib/0032976"}, pp. 39 ff.\}. \ -text\Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"} -\<^footnote>\The official releases are available on \<^url>\https://zenodo.org/record/3370483#.YfWg6S-B1qt\, the - developer version on \<^url>\https://github.com/logicalhacking/Isabelle_DOF\\ +text\ \<^vs>\-0.2cm\ +Recently, \<^dof> @{cite "brucker.ea:isabelledof:2019" and "brucker.ea:isabelle-ontologies:2018"} +\<^footnote>\The official releases are available at \<^url>\https://zenodo.org/record/3370483#.YfWg6S-B1qt\, the + developer version at \<^url>\https://github.com/logicalhacking/Isabelle_DOF\.\ has been designed as an Isabelle component that attempts to answer these needs. \<^dof> generates from ontology definitions directly integrated into Isabelle theories typed meta-data, that may be annotated to a number of document elements and that were validated ``on-the-fly'' during the general continuous type and proof-checking process -in the Prover IDE (Isabelle/PIDE). Thus, \<^dof> profits and extends Isabelle's -document-centric view on code, definitions, proofs, text-elements and other modeling -elements. +in an IDE (Isabelle/PIDE). Thus, we extend the document-centric view on code, definitions, +proofs, text-elements, etc., prevailing in the Isabelle system framework. -In more detail, the schema of \<^dof> text elements --- whose syntax follows closely -the corresponding Isabelle standard elements, except that these do not -posses the brackets with the meta-data --- looks as follows: -@{theory_text [display,indent=10, margin=70] -\ - text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\ some formal text \ - -\} -while code-elements have the form: +In more detail, \<^dof> introduces a number of ``ontology aware'' text-elements with analogous +syntax to standard ones. The difference is a bracket with meta-data of the form: \<^vs>\-0.3cm\ @{theory_text [display,indent=10, margin=70] \ + text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\ some semi-formal text \ ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\ some SML code \ + ... \} -which means for each element that a meta-data object is created and associated to it. -This meta-data can be referenced via its label and used in further computations in text - -or code elements. +\<^vs>\-0.3cm\ In these \<^dof> elements, a meta-data object is created and associated to it. This +meta-data can be referenced via its label and used in further computations in text or code. %; the details will be explained in the subsequent section. -Admittedly, Isabelle is not the first system that comes into one's mind when -writing a scientific paper, a book, or a larger technical documentation. -However, it has a typesetting system inside which is in the -tradition of document generation systems such as mkd, Document! X, Doxygen, -Javadoc, etc., and which embed formal content elements such as formula pretty-prints -into formal text. In Isabelle, these embedded meta-text elements using references -to the context represent a machine-checked macro called \<^emph>\antiquotation\. +Admittedly, Isabelle is not the first system that comes into one's mind when writing a scientific +paper, a book, or a larger technical documentation. However, it has a typesetting system inside +which is in the tradition of document generation systems such as mkd, Document! X, Doxygen, +Javadoc, etc., and which embed formal content such as formula pretty-prints into semi-formal text +or code. The analogous mechanism the Isabelle system provides is a machine-checked macro +called \<^emph>\antiquotation\ that depends on the logical context of the document element. With standard Isabelle antiquotations, for example, the following text element -inside the integrated source will appear in Isabelle/PIDE as follows: +of the integrated source will appear in Isabelle/PIDE as follows: \<^vs>\-0.3cm\ @{theory_text [display,indent=10, margin=70] \ text\ According to the reflexivity axiom @{thm refl}, we obtain in \ for @{term "fac 5"} the result @{value "fac 5"}.\ \} -In the generated document represented in the generated \<^LaTeX> or HTML output, it is shown as: +\<^vs>\-0.5cm\ In the corresponding generated \<^LaTeX> or HTML output, this looks like this: +\<^vs>\-0.1cm\ @{theory_text [display,indent=10, margin=70] \According to the reflexivity axiom \x = x\, we obtain in \ for \fac 5\ the result \120\.\ } -where the meta-texts \@{thm refl}\ ("give the presentation of theorem 'refl'"), +\<^vs>\-0.1cm\where the meta-texts \@{thm refl}\ ("give the presentation of theorem 'refl'"), \@{term "fac 5"}\ ("parse and type-check 'fac 5' in the previous logical context") and \@{value "fac 5"}\ ("compile and execute 'fac 5' according to its definitions") are built-in antiquotations in \<^hol>. -One distinguishing feature of \<^dof> is that specific antiquotations were generated from -an ontology rather than being hard-coded into the Isabelle system infrastructure. +One distinguishing feature of \<^dof> is that specific antiquotations \<^emph>\were generated from +an ontology\ rather than being hard-coded into the Isabelle system infrastructure. \ (* @@ -166,24 +165,31 @@ and typed reference mechanisms inside text- and ML-contexts. *) -text\ - -In this paper, we extend prior versions of \<^dof> by -\<^enum> a new form of contexts, namely \<^emph>\term contexts\. Thus, annotations generated - from \<^dof> may also occur in \\\-terms used to denote meta-data, and +text\In this paper, we extend prior versions of \<^dof> by +\<^enum> support of antiquotions in a new class of contexts, namely \<^emph>\term contexts\ + (rather than SML code or semi-formal text). Thus, annotations generated + from \<^dof> may also occur in \\\-terms used to denote meta-data. \<^enum> formal, machine-checked invariants on meta-data, which correspond to the concept of - "rules" in ontology languages such as OWL, and which can be specified in + "rules" in OWL or "constraints" in UML, and which can be specified in common HOL \\\-term syntax. \ -text\ -Beyond the gain of expressivity in \<^dof> ontologies, these features pave the way -for advanced queries of elements inside an integrated document, and for formal proofs -over the relations/translations of ontologies and ontology-instances --- The latter -question raised scientific interest under the label "ontology alignment" for which -we therefore present a (partial) solution. To sum up, we completed \<^dof> to a +text\ For example, the \<^dof> evaluation command taking a HOL-expression: +@{theory_text [display,indent=10, margin=70] +\ value*[ass::Assertion, relev=2::int] \mapfilter (\ \. relev \ > 2) @{instance_of \Assertion\}\\ +} +where \<^dof> command \value*\ type-checks, expands in an own validation phase +the \instance_of\-term antiquotation, and evaluates the resulting HOL expression +above. Assuming an ontology providing the class \Assertion\ having at least the +integer attribute \relev\, the command finally creates an instance of \Assertion\ and +binds this to the label \ass\ for further use. + +Beyond the gain of expressivity in \<^dof> ontologies, term-antiquotations pave the way +for advanced queries of elements inside an integrated source, and invariants +allow for formal proofs over the relations/translations of ontologies and ontology-instances. +The latter question raised scientific interest under the label "ontology alignment" for +which we therefore present a formal solution. To sum up, we completed \<^dof> to a a fairly rich, ITP-oriented ontology language, which is a concrete proposal for the -Isabelle community for a deeper structuring of the Archive of Formal Proofs (AFP; -\<^url>\https://www.isa-afp.org\). +ITP community allowing a deeper structuring of mathematical libraries such as the AFP. \