From 1a23140534a30e70fdb08d0558391a12c63a4959 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Tue, 8 Feb 2022 12:10:25 +0100 Subject: [PATCH] Update Morphisms section - Add ontology in document - Add antiquations to reference classes, etc. --- .../scholarly_paper/2021-ITP-PMTI/paper.thy | 141 +++++++++++++++--- 1 file changed, 124 insertions(+), 17 deletions(-) diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 54e88667..556d859b 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -790,6 +790,108 @@ text\ section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \Proving Morphisms on Ontologies\ +(*<*) +(* Mapped_PILIB_Ontology example *) +term\fold (+) S 0\ + +definition sum + where "sum S = (fold (+) S 0)" + +datatype Hardware_Type = + Motherboard | + Expansion_Card | + Storage_Device | + Fixed_Media | + Removable_Media | + Input_Device | + Output_Device + +(* Reference Ontology *) +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 + +(* 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 \))" + +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 , + Resource.name = name \ \" + +definition Product_to_Component_morphism :: "'a Product_scheme \ Component" + ("_ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999) + where " \ \Component\\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = \ Resource.tag_attribute = 1::int , + Resource.name = name \ , + Electronic.provider = Product.provider \ , + Electronic.manufacturer = ''no manufacturer'' , + 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) + 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 \) + \" + +lemma inv_c2_preserved : + "c2_inv \ \ c1_inv (\ \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)" + unfolding c1_inv_def c2_inv_def + Computer_Hardware_to_Hardware_morphism_def Product_to_Component_morphism_def + by (auto simp: comp_def) + +lemma Computer_Hardware_to_Hardware_morphism_total : + "Computer_Hardware_to_Hardware_morphism ` ({X::Computer_Hardware. c2_inv X}) \ ({X::Hardware. c1_inv X})" + using inv_c2_preserved + by auto + +(*>*) + text\ \<^dof> framework does not assume that all documents reference the same ontology. Each document may build its local ontology without any external reference. @@ -851,14 +953,17 @@ onto_class R_Software = Informatic + \end{figure} To illustrate this process, we use the reference ontology (considered as a standard) described -in the listing \autoref{fig-Reference-Ontology-example}, defining the \Resource\, \Electronic\, -\Component\, \Informatic\, \Hardware\ and \Software\ concepts (or classes). +in the listing \autoref{fig-Reference-Ontology-example}, defining the \<^typ>\Resource\, +\<^typ>\Electronic\, \<^typ>\Component\,\<^typ>\Informatic\, \<^typ>\Hardware\ and \<^typ>\R_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 \<^typ>\Hardware\ class containing a \<^const>\mass\ attribute +and composed of a list of components with a \<^const>\mass\ attribute formalising +the mass value of each component. +The \<^typ>\Hardware\ class also contains a local \<^theory_text>\invariant c1\ +to define a constraint linking the global mass of a \<^typ>\Hardware\ object +with the masses of its own components. \ text\ @@ -889,12 +994,13 @@ onto_class Computer_Hardware = Product + For the needs of our document, we have defined a simple ontology to classify Software and Hardware -objects. This ontology is described in the figure \autoref{fig-Local-Ontology-example} 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. +objects. This ontology is described in \autoref{fig-Local-Ontology-example} and +defines the \<^typ>\Item\, \<^typ>\Product\, \<^typ>\Computer_Software\ +and \<^typ>\Computer_Hardware\ concepts. +As for the reference ontology, we focus on the \<^typ>\Computer_Hardware\ +class defined as a list of products characterised by their mass value. +This class contains a local \<^theory_text>\invariant c2\ to guarantee that its own mass value +equals the sum of all the masses of the products composing the object. \ @@ -937,11 +1043,12 @@ and the reference ontology using morphism functions (or mapping rules). These ru define the relationship between one class of the local ontology to one or several other class(es) described in the reference ontology. -For example,\Product_to_Component_morphism\ and \Computer_Hardware_to_Hardware_morphism\ definitions, -detailed in the figure \autoref{fig-mapping-example}, specify how \Product\ or \Computer_Hardware\ -objects are mapped to \Component\ -or \Hardware\ objects defined in the reference ontology. This mapping shows that the structure -of a (user) ontology may be quite different from the one of a standard ontology she references. +For example, \<^const>\Product_to_Component_morphism\ and \<^const>\Computer_Hardware_to_Hardware_morphism\ +definitions, detailed in \autoref{fig-mapping-example}, +specify how \<^typ>\Product\ or \<^typ>\Computer_Hardware\ objects are mapped to \<^typ>\Component\ +or \<^typ>\Hardware\ objects defined in the reference ontology. +This mapping shows that the structure of a (user) ontology may be quite different +from the one of a standard ontology it references. \