diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index 8d43ce64..24b840ef 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -57,12 +57,16 @@ year = {1995} } -@MISC{owl2012, - title = {OWL 2 Web Ontology Language}, - note={\url{https://www.w3.org/TR/owl2-overview/}, Document Overview (Second Edition)}, - author = {World Wide Web Consortium} +@TechReport{owl2012, + author = "", + title = "{OWL} 2 Web Ontology Language Document Overview (Second Edition)", + month = dec, + note = "https://www.w3.org/TR/2012/REC-owl2-overview-20121211/", + year = "2012", + bibsource = "https://w2.syronex.com/jmr/w3c-biblio", + type = "", + institution = "W3C", } - @MISC{protege, title = {Prot{\'e}g{\'e}}, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index e7ca740a..a4eb3a01 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -162,14 +162,14 @@ in an IDE (Isabelle/PIDE). Thus, we extend the document-centric view on code, de proofs, text-elements, etc., prevailing in the Isabelle system framework. 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] +syntax to standard ones. The difference is a bracket with meta-data of the form: +@{theory_text [display,indent=5, 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 \ - ... +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 \ +... \} -\<^vs>\-0.3cm\ In these \<^dof> elements, a meta-data object is created and associated to it. This +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. @@ -181,19 +181,18 @@ or code. The analogous mechanism the Isabelle system provides is a machine-check called \<^emph>\antiquotation\ that depends on the logical context of the document element. With standard Isabelle antiquotations, for example, the following text element -of the integrated source will appear in Isabelle/PIDE as follows: \<^vs>\-0.3cm\ -@{theory_text [display,indent=10, margin=70] +of the integrated source will appear in Isabelle/PIDE as follows: +@{theory_text [display,indent=5, margin=70] \ - text\ According to the reflexivity axiom @{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\ - +text\ According to the reflexivity axiom @{thm refl}, we obtain in \ + for @{term "fac 5"} the result @{value "fac 5"}.\ \} -\<^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\.\ -} -\<^vs>\-0.1cm\where the meta-texts \@{thm refl}\ (``give the presentation of theorem `refl'\,\!''), +In the corresponding generated \<^LaTeX> or HTML output, this looks like this: +@{theory_text [display,indent=5, 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'\,\!''), \@{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>. @@ -234,13 +233,14 @@ text\As novel contribution, this work extends prior versions of \<^dof> by (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 OWL or ``constraints'' in UML, and which can be specified in + ``rules'' in OWL~ @{cite "owl2012"} or ``constraints'' in UML, and which can be specified in common \<^hol> \\\-term syntax. \ text\ For example, the \<^dof> evaluation command taking a \<^hol>-expression: -@{theory_text [display,indent=6, margin=70] -\ value*[ass::Assertion, relvce=2::int] \filter (\ \. relvce \ > 2) @{Assertion-instances}\\ -} +@{theory_text [display,indent=5, margin=70] \ +value*[ass::Assertion, relvce=2::int] + \filter (\ \. relvce \ > 2) @{Assertion-instances}\ +\} where \<^dof> command \value*\ type-checks, expands in an own validation phase the \Assertion-instances\-term antiquotation, and evaluates the resulting \<^hol> expression above. Assuming an ontology providing the class \Assertion\ having at least the @@ -337,11 +337,11 @@ text\ \<^hol>-types, allowing for formal \<^emph>\links\ to and between ontological concepts. For example, the basic concept of requirements from CENELEC 50128~@{cite "bsi:50128:2014"} is captured in ODL as follows: - @{theory_text [display,indent=10, margin=70] + @{theory_text [display,indent=5, margin=70] \ - doc_class requirement = text_element + (* derived from text_element *) - long_name ::"string option" (* an optional string attribute *) - is_concerned::"role set" (* roles working with this req. *) +doc_class requirement = text_element + (* derived from text_element *) + long_name ::"string option" (* an optional string attribute *) + is_concerned::"role set" (* roles working with this req. *) \} This ODL class definition maybe part of one or more Isabelle theory--files capturing the entire ontology definition. Isabelle's session management allows for pre-compiling them before being @@ -529,7 +529,6 @@ text\ for example, by the object they refer to in the logical context, \<^item> Generation of markup information for the Isabelle/PIDE, and \<^item> Code generation: -\<^vs>\-0.3cm\ \<^item> Evaluation of \<^hol> expressions with ontological annotations, \<^item> Generation of ontological invariants processed simultaneously with the generation of the document (a theory in \<^hol>). @@ -548,7 +547,7 @@ declare_reference*["type-checking-example"::side_by_side_figure] (*>*) text\ - If we take back the ontology example for mathematical papers + If we take back the example ontology for mathematical papers of~@{cite "brucker.ea:isabelledof:2019"} shown in \autoref{fig-ontology-example} \begin{figure} @{boxed_theory_text [display] \ @@ -779,19 +778,20 @@ text\ Thus, to get the list of the properties of the instances of the class \<^typ>\myresult\, it suffices to get list of the authors of the instances of the \<^typ>\myintroduction\ class, and to treat this meta-data as usual: - @{theory_text [display,indent=10, margin=70] \ - value*\map (myresult.property) @{myresult-instances}\ - value*\map (mytext_section.authored_by) @{myintroduction-instances}\ + @{theory_text [display,indent=5, margin=70] \ +value*\map (myresult.property) @{myresult-instances}\ +value*\map (mytext_section.authored_by) @{myintroduction-instances}\ \} In order to get the list of the instances of the class \<^typ>\myresult\ whose \<^const>\evidence\ is a \<^const>\proof\, on can use the command: - @{theory_text [display,indent=10, margin=70] \ - value*\filter (\\. myresult.evidence \ = proof) @{myresult-instances}\ + @{theory_text [display,indent=5, margin=70] \ +value*\filter (\\. myresult.evidence \ = proof) @{myresult-instances}\ \} Analogously, the list of the instances of the class \<^typ>\myintroduction\ whose \<^const>\level\ > 1, can be filtered by: - @{theory_text [display,indent=10, margin=70] \ - value*\filter (\\. the (mytext_section.level \) > 1) @{myintroduction-instances}\ + @{theory_text [display,indent=5, margin=70] \ +value*\filter (\\. the (mytext_section.level \) > 1) + @{myintroduction-instances}\ \} \ @@ -1018,6 +1018,7 @@ equals the sum of all the masses of the products composing the object. text\ \begin{figure} @{boxed_theory_text [display] \ + definition Item_to_Resource_morphism :: "'a Item_scheme \ Resource" ("_ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999) where "\ \Resource\\<^sub>I\<^sub>t\<^sub>e\<^sub>m = \ Resource.tag_attribute = 0::int , @@ -1032,17 +1033,18 @@ definition Product_to_Component_morphism :: "'a Product_scheme \ Com Component.mass = Product.mass \ , Component.dimensions = [] \" -definition Computer_Hardware_to_Hardware_morphism :: "'a Computer_Hardware_scheme \ Hardware" - ("_ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e" [1000]999) +definition Computer_Hardware_to_Hardware_morphism :: + "'a Computer_Hardware_scheme \ Hardware" + ("_ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e" [1000]999) where "\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e = \ Resource.tag_attribute = 2::int , Resource.name = name \ , Informatic.description = ''no description'', Hardware.type = Computer_Hardware.type \ , Hardware.mass = mass \ , - Hardware.composed_of = map Product_to_Component_morphism - (Computer_Hardware.composed_of \) - \" + Hardware.composed_of = + map Product_to_Component_morphism + (Computer_Hardware.composed_of \) \" \} \caption{An extract of a mapping definitions.} \label{fig-mapping-example} @@ -1079,8 +1081,8 @@ lemma inv_c2_preserved : using comp_def by (auto) lemma Computer_Hardware_to_Hardware_morphism_total : - "Computer_Hardware_to_Hardware_morphism ` ({X::Computer_Hardware. c2_inv X}) - \ ({X::Hardware. c1_inv X})" + "Computer_Hardware_to_Hardware_morphism ` ({X::Computer_Hardware. c2_inv X}) + \ ({X::Hardware. c1_inv X})" using inv_c2_preserved by auto \} \caption{Proofs establishing the Invariant Preservation.} @@ -1120,7 +1122,7 @@ onto_class Top = Annotations :: "annotation list" onto_class Field_of_mathematics = - Annotations :: "annotation list" + Annotations :: "annotation list" <= "[RDFS (label ''Field of mathematics'')]" invariant restrict_annotation_F ::"set (Annotations \) \ range (RDFS o label) \ range (RDFS o comment)" @@ -1193,7 +1195,7 @@ text\ We can represent the annotations properties as datatypes and then attach them as an attributes list to a class. For example the declaration: -@{theory_text [display,indent=10, margin=70] \ +@{theory_text [display,indent=5, margin=70] \ datatype dc = creator string | title string datatype owl = backwardCompatibleWith string | deprecated string @@ -1207,12 +1209,12 @@ datatype rdfs = comment string datatype annotation = DC dc | OWL owl | RDFS rdfs onto_class Field_of_mathematics = - Annotations :: "annotation list" + Annotations :: "annotation list" <= "[RDFS (label ''Field of mathematics'')]" invariant restrict_annotation_F ::"set (Annotations \) \ - range (RDFS o label) \ range (RDFS o comment)" - + range (RDFS o label) + \ range (RDFS o comment)" \} - defines the class \<^typ>\Field_of_mathematics\ with an attribute \<^const>\Annotations\ + defines the class \<^typ>\Field_of_mathematics\ with an attribute \<^theory_text>\Annotations\ which is a \<^type>\list\ of \<^typ>\annotation\s. We can even constraint the type of allowed \<^typ>\annotation\s with an invariant. Here the \<^theory_text>\invariant restrict_annotation_F\ forces the \<^typ>\annotation\s to be @@ -1222,7 +1224,7 @@ onto_class Field_of_mathematics = a \<^typ>\Problem\ and a \<^typ>\Method\ as subclasses of the class \<^typ>\Mathematical_knowledge_object\. It gives in \<^dof>: -@{theory_text [display,indent=10, margin=70] \ +@{theory_text [display,indent=5, margin=70] \ onto_class Problem = Mathematical_knowledge_object + Annotations :: "annotation list" @@ -1234,16 +1236,16 @@ onto_class Method = Mathematical_knowledge_object + the relation as an attribute and enforces the relation with an \<^theory_text>\invariant\. The two directed relations \<^const>\is_solved_by\ and \<^const>\solves\ between \<^typ>\Problem\ and a \<^typ>\Method\ can be represented in \<^dof> like this: -@{theory_text [display,indent=10, margin=70] \ +@{theory_text [display,indent=5, margin=70] \ onto_class assoc_Problem_Method = is_solved_by :: "(Problem \ Method) set" invariant is_solved_by_defined :: "\ x. x \ Domain (is_solved_by \) - \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" + \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" onto_class assoc_Method_Problem = solves :: "(Method \ Problem) set" invariant solves_defined :: "\ x. x \ Domain (solves \) - \ (\ y \ Range (solves \). (x, y) \ solves \)" + \ (\ y \ Range (solves \). (x, y) \ solves \)" \} where the attributes \<^const>\is_solved_by\ and \<^const>\solves\ define the relations of the classes and the invariants \<^theory_text>\is_solved_by_defined\ and \<^theory_text>\solves_defined\ enforce @@ -1267,7 +1269,7 @@ way for the abstract specification of meta-data constraints as well the possibil of advanced search in the meta-data of document elements. Thus it profits and extends Isabelle's document-centric view on formal development. -Many ontological languages such OWL @{cite "owl2012"} as well as the meta-modeling technology +Many ontological languages such as OWL as well as the meta-modeling technology available for UML/OCL provide concepts for semantic rules and constraints, but leave the validation checking usually to external tools (if implementing them at all). This limits their practical usefulness drastically. Our approach treats invariants as @@ -1338,7 +1340,7 @@ of formal content, be it in the engineering or the mathematics domain. \<^footnote>\This paper has been edited in \<^dof>, of course.\ Another line of future application is to increase the ``depth'' of built-in term antiquotations such -as \<^theory_text>\@{typ \'\\}\, \<^term>\@{term \a + b\}\ and \<^term>\@{thm \HOL.refl\}\, which are currently implemented +as \<^theory_text>\@{typ \'\\}\, \<^theory_text>\@{term \a + b\}\ and \<^theory_text>\@{thm \HOL.refl\}\, which are currently implemented just as validations in the current logical context. In the future, they could optionally be expanded to the types, terms and theorems (with proof objects attached) in a meta-model of the Isabelle Kernel such as the one presented in @{cite "10.1007/978-3-030-79876-5_6"} (also available in the AFP).