diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index 2c2df5d2..e85bf84a 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -13,6 +13,13 @@ @STRING{j-tosem= "" } @STRING{pub-acm:adr= "" } +@Manual{ wenzel:isabelle-isar:2020, + title = {The Isabelle/Isar Reference Manual}, + author = {Makarius Wenzel}, + year = 2020, + note = {Part of the Isabelle distribution.} +} + @TechReport{ bsi:50128:2014, type = {Standard}, key = {BS EN 50128:2011}, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 3c157485..1b88a247 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -258,12 +258,119 @@ subsection\Code-Generation in Isabelle\ text\Explain eval and nbe, and refer to references.\ + + + section\Invariants in DOF\ +text\ + A novel mechanism to specify invariants is implemented + and can now be specified in common HOL syntax. +% These invariants can be checked when an instance of the class is defined. +% To enable the checking of the invariants, the \<^emph>\invariants\_checking\ +% theory attribute must be set: +% \begin{isar} +% declare[[invariants_checking = true]] +% \end{isar} + If we take back the ontology example of~@{cite "brucker.ea:isabelledof:2019"}, we can now + specify the constraints, like that any instance of a \<^emph>\result\ class finally has + a non-empty property list, if its \<^emph>\kind\ is \<^emph>\proof\, or that + the \<^emph>\establish\ relation between \<^emph>\claim\ and + \<^emph>\result\ is total, using the keyword \<^emph>\invariant\ in the class definition: + \begin{isar} +doc_class title = + short_title :: "string option" <= "None" +doc_class author = + email :: "string" <= "''''" + +datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4 + +doc_class abstract = + keywordlist :: "string list" <= "[]" + safety_level :: "classification" <= "SIL3" +doc_class text_section = + authored_by :: "author set" <= "{}" + level :: "int option" <= "None" + +type_synonym notion = string + + doc_class introduction = text_section + + authored_by :: "author set" <= "UNIV" + uses :: "notion set" + invariant author_finite :: "finite (authored_by \)" +doc_class claim = introduction + + based_on :: "notion list" +doc_class technical = text_section + + formal_results :: "thm list" +doc_class "definition" = technical + + is_formal :: "bool" + property :: "term list" <= "[]" + +datatype kind = expert_opinion | argument | "proof" + + doc_class result = technical + + evidence :: kind + property :: "thm list" <= "[]" + invariant has_property :: "evidence \ = proof \ property \ \ []" + doc_class example = technical + + referring_to :: "(notion + definition) set" <= "{}" + doc_class conclusion = text_section + + establish :: "(claim \ result) set" + invariant total_rel :: "\ x. x \ Domain (establish \) + \ (\ y \ Range (establish \). (x, y) \ establish \)" +\end{isar} + + In our example, the invariant \<^emph>\author\_finite\ enforces that the user sets the + \<^emph>\authored\_by\ set. + The \<^emph>\$\sigma$\ symbol is reserved and references the future instance class. + By relying on the implementation of the Records + in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"}, + one can reference an attribute of an instance using its selector function. + For example, \<^emph>\establish $\sigma$\ denotes the value + of the \<^emph>\establish\ attribute + of the future instance of the class \<^emph>\conclusion\. + + if we define some instances like: (ADD EXAMPLE !!!) + The value of each attribute defined for the instances is checked at run-time + against their class invariants. + SPEAK ABOUT INVARIANTS INHERITAGE ??? + As the class \<^emph>\class\_inv2\ is a subsclass + of the class \<^emph>\class\_inv1\, it inherits \<^emph>\class\_inv1\ invariants. + Hence the \<^emph>\inv1\ invariant is checked + when the instance \<^emph>\testinv2\ is defined. +\ + + section\Proving Morphisms on Ontologies\ section\Example and Queries\ +text\ +A new mechanism to make query on instances is available and uses the HOL implementation of Lists. +So complex queries can be defined using functions over the instances list. +With the class: +\begin{isar} +doc_class Z = + z::"int" +\end{isar} +and some instances: +\begin{isar} +text*[test1Z::Z, z=1]\lorem ipsum...\ +text*[test2Z::Z, z=4]\lorem ipsum...\ +text*[test3Z::Z, z=3]\lorem ipsum...\ +\end{isar} +we can get all the instances of the class Z: +\begin{isar} +value*\@{Z-instances}\ +\end{isar} +or the instances of the class Z whose attribute z > 2: +\begin{isar} +value*\filter (\\. Z.z \ > 2) @{Z-instances}\ +\end{isar} + +EXPLAIN VALUE* ??? +\ + section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"] \Applications\ subsection\Engineering Example : An Extract from PLib\ @@ -271,7 +378,6 @@ subsection\Engineering Example : An Extract from PLib\ subsection\Mathematics Example : An Extract from OntoMathPro\ - section\Conclusion\ subsection\Related Works\ subsubsection\The notion of \<^emph>\Integrated Source\\ @@ -311,8 +417,6 @@ https://doi.org/10.1145/2479787.2479830 section\ Related work \ -ML\open Goal\ - text\ \<^item> Geschwalle: Tom Gruber's "Ontology for Engineering Mathematics" \<^url>\https://tomgruber.org/writing/an-ontology-for-engineering-mathematics\