From f35a7eb5bd93983b014118909f01208406465af4 Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Mon, 7 Feb 2022 21:28:40 +0100 Subject: [PATCH] Adding Idir's part to the paper --- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 103 ++++++++++++++++++ src/tests/Mapped_PILIB_Ontology.thy | 48 +++++--- 2 files changed, 133 insertions(+), 18 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 884144d..8c907a9 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -775,6 +775,109 @@ text\ section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \Proving Morphisms on Ontologies\ +text\ +\<^dof> framework does not assume that all documents reference the same ontology. +Each document may build its local ontology without any external reference. +It may also build it based upon one or several reference ontologies (i.e., standard ones). + +The relationship between the local ontology and the reference one is formalised using a morphism function. +More precisely, a class of a local ontology may be described as a consequence of a transformation applied +to one or several other class(es) defined in other ontologies. This means that each instance of the former can be +computed from one or more instances of the latter. + + +Thanks to the morphism relationship, the obtained class may either import properties (definitions are preserved) +or map properties (the properties are different but are semantically equivalent) that are defined in the referenced class(es). +It may also define additional properties. +\ + +(*<*) +(* Reference Ontology *) +definition sum + where "sum S = (fold (+) S 0)" + +datatype Hardware_Type = + Motherboard | + Expansion_Card | + Storage_Device | + Fixed_Media | + Removable_Media | + Input_Device | + Output_Device + +onto_class Resource = + name :: string + +onto_class Electronic = Resource + + provider :: string + manufacturer :: string + +onto_class Component = Electronic + + mass :: int + dimensions :: "int list" + +onto_class Simulation_Model = Electronic + + type :: string + +onto_class Informatic = Resource + + description :: string + +onto_class Hardware = Informatic + + type :: Hardware_Type + mass :: int + composed_of :: "Component list" + invariant c1 :: "mass \ = sum(map Component.mass (composed_of \))" + +onto_class R_Software = Informatic + + version :: int + +(*>*) + + +text\ +To illustrate this process, we use the reference ontology (considered as a standard) described +in the listing X, defining the Resource, Electronic, Component, Informatic, Hardware and Software +concepts (or classes). Each class contains a set of attributes or properties and some local +invariants. + +In our example, we focus on the Hardware class containing a mass attribute and composed of a list +of components with a mass attribute formalising the mass value of each component. The Hardware +class also contains a local invariant ''c1'' to define a constraint linking the global mass of +a Hardware object with the masses of its own components. +\ + +(*<*) +(* Local Ontology *) +onto_class Item = + name :: string + +onto_class Product = Item + + serial_number :: int + provider :: string + mass :: int + +onto_class Computer_Software = Item + + version :: int + +onto_class Electronic_Component = Product + + dimensions :: "int set" + +onto_class Computer_Hardware = Product + + type :: Hardware_Type + composed_of :: "Product list" + invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))" + +(*>*) + +text\ +For the needs of our document, we have defined a simple ontology to classify Software and Hardware +objects. This ontology is described in listing X and defines the Item, Product, Computer_Software +and Computer_Hardware concepts. As for the reference ontology, we focus on the Computer_Hardware +class defined as a list of products characterised by their mass value. This class contains a local +invariant ''c2'' to guarantee that its own mass value equals the sum of all the masses of the products +composing the object. +\ + section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author)"] \Applications\ subsection\Engineering Example : An Extract from PLib\ diff --git a/src/tests/Mapped_PILIB_Ontology.thy b/src/tests/Mapped_PILIB_Ontology.thy index 073ab61..511907f 100644 --- a/src/tests/Mapped_PILIB_Ontology.thy +++ b/src/tests/Mapped_PILIB_Ontology.thy @@ -21,7 +21,6 @@ term\fold (+) S 0\ definition sum where "sum S = (fold (+) S 0)" - datatype Hardware_Type = Motherboard | Expansion_Card | @@ -40,6 +39,11 @@ The relationship between the local ontology and the reference one is formalised More precisely, a class of a local ontology may be described as a consequence of a transformation applied to one or several other class(es) defined in other ontologies. This means that each instance of the former can be computed from one or more instances of the latter. + + +Thanks to the morphism relationship, the obtained class may either import properties (definitions are preserved) +or map properties (the properties are different but are semantically equivalent) that are defined in the referenced class(es). +It may also define additional properties. \ (* Reference Ontology *) @@ -70,12 +74,15 @@ onto_class R_Software = Informatic + version :: int text\ -To illustrate this process, we use the reference ontology (considered as a standard) described in the listing X, defining the Resource, Electronic, Component, -Informatic, Hardware and Software concepts (or classes). Each class contains a set of attributes or properties and some local invariants. +To illustrate this process, we use the reference ontology (considered as a standard) described +in the listing X, defining the Resource, Electronic, Component, Informatic, Hardware and Software +concepts (or classes). Each class contains a set of attributes or properties and some local +invariants. -In our example, we focus on the Hardware class containing a mass attribute and composed of a list of components with a mass attribute formalising -the mass value of each component. The Hardware class also contains a local invariant ''c1'' to define a constraint linking the global mass of a Hardware -object with the masses of its own components. +In our example, we focus on the Hardware class containing a mass attribute and composed of a list +of components with a mass attribute formalising the mass value of each component. The Hardware +class also contains a local invariant ''c1'' to define a constraint linking the global mass of +a Hardware object with the masses of its own components. \ (* Local Ontology *) @@ -99,10 +106,12 @@ onto_class Computer_Hardware = Product + invariant c2 :: "Product.mass \ = sum(map Product.mass (composed_of \))" text\ -For the needs of our document, we have defined a simple ontology to classify Software and Hardware objects. -This ontology is described in listing X and defines the Item, Product, Computer_Software and Computer_Hardware concepts. -As for the reference ontology, we focus on the Computer_Hardware class defined as a list of products characterised by their mass value. -This class contains a local invariant to guarantee that its own mass value equals the sum of all the masses of the products composing the object. +For the needs of our document, we have defined a simple ontology to classify Software and Hardware +objects. This ontology is described in listing X and defines the Item, Product, Computer_Software +and Computer_Hardware concepts. As for the reference ontology, we focus on the Computer_Hardware +class defined as a list of products characterised by their mass value. This class contains a local +invariant ''c2'' to guarantee that its own mass value equals the sum of all the masses of the products +composing the object. \ definition Item_to_Resource_morphism :: "'a Item_scheme \ Resource" @@ -133,20 +142,22 @@ definition Computer_Hardware_to_Hardware_morphism :: "'a Computer_Hardware_schem text\ -To check the coherence of our local ontology, we define some transformation rules as a mapping applied to one or several -other class(es) described in the reference ontology. +To check the coherence of our local ontology, we define a relationship between the local ontology +and the reference ontology using morphism functions (or mapping rules). These rules are applied to +define the relationship between one class of the local ontology to one or several other class(es) +described in the reference ontology. + +For example, \ text\ -Thanks to the morphism relationship, the obtained class may either import properties (definitions are preserved) -or map properties (the properties are different but are semantically equivalent) that are defined in the referenced class(es). -It may also define additional properties. - -As shown by our example, the structure of a (user) ontology may be quite different from the one of a standard ontology she references. +As shown by our example, the structure of a (user) ontology may be quite different from the one +of a standard ontology she references. \ -text\Now we check that the invariant is preserved through the morphism:\ + + find_theorems Hardware.composed_of @@ -165,6 +176,7 @@ lemma Computer_Hardware_to_Hardware_morphism_total : using inv_c2_preserved by auto + declare[[invariants_checking]] declare[[invariants_checking_with_tactics]]