forked from Isabelle_DOF/Isabelle_DOF
Update Morphisms section
- Add ontology in document - Add antiquations to reference classes, etc.
This commit is contained in:
parent
4b05c9a9a1
commit
1a23140534
|
@ -790,6 +790,108 @@ text\<open>
|
||||||
|
|
||||||
section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \<open>Proving Morphisms on Ontologies\<close>
|
section*["morphisms"::technical,main_author="Some(@{docitem ''idir''}::author)"] \<open>Proving Morphisms on Ontologies\<close>
|
||||||
|
|
||||||
|
(*<*)
|
||||||
|
(* Mapped_PILIB_Ontology example *)
|
||||||
|
term\<open>fold (+) S 0\<close>
|
||||||
|
|
||||||
|
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 \<sigma> = sum(map Component.mass (composed_of \<sigma>))"
|
||||||
|
|
||||||
|
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 \<sigma> = sum(map Product.mass (composed_of \<sigma>))"
|
||||||
|
|
||||||
|
definition Item_to_Resource_morphism :: "'a Item_scheme \<Rightarrow> Resource"
|
||||||
|
("_ \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m" [1000]999)
|
||||||
|
where "\<sigma> \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m = \<lparr> Resource.tag_attribute = 0::int ,
|
||||||
|
Resource.name = name \<sigma> \<rparr>"
|
||||||
|
|
||||||
|
definition Product_to_Component_morphism :: "'a Product_scheme \<Rightarrow> Component"
|
||||||
|
("_ \<langle>Component\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999)
|
||||||
|
where " \<sigma> \<langle>Component\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t = \<lparr> Resource.tag_attribute = 1::int ,
|
||||||
|
Resource.name = name \<sigma> ,
|
||||||
|
Electronic.provider = Product.provider \<sigma> ,
|
||||||
|
Electronic.manufacturer = ''no manufacturer'' ,
|
||||||
|
Component.mass = Product.mass \<sigma> ,
|
||||||
|
Component.dimensions = [] \<rparr>"
|
||||||
|
|
||||||
|
definition Computer_Hardware_to_Hardware_morphism :: "'a Computer_Hardware_scheme \<Rightarrow> Hardware"
|
||||||
|
("_ \<langle>Hardware\<rangle>\<^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 "\<sigma> \<langle>Hardware\<rangle>\<^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 =
|
||||||
|
\<lparr> Resource.tag_attribute = 2::int ,
|
||||||
|
Resource.name = name \<sigma> ,
|
||||||
|
Informatic.description = ''no description'',
|
||||||
|
Hardware.type = Computer_Hardware.type \<sigma> ,
|
||||||
|
Hardware.mass = mass \<sigma> ,
|
||||||
|
Hardware.composed_of = map Product_to_Component_morphism
|
||||||
|
(Computer_Hardware.composed_of \<sigma>)
|
||||||
|
\<rparr>"
|
||||||
|
|
||||||
|
lemma inv_c2_preserved :
|
||||||
|
"c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^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}) \<subseteq> ({X::Hardware. c1_inv X})"
|
||||||
|
using inv_c2_preserved
|
||||||
|
by auto
|
||||||
|
|
||||||
|
(*>*)
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
\<^dof> framework does not assume that all documents reference the same ontology.
|
\<^dof> framework does not assume that all documents reference the same ontology.
|
||||||
Each document may build its local ontology without any external reference.
|
Each document may build its local ontology without any external reference.
|
||||||
|
@ -851,14 +953,17 @@ onto_class R_Software = Informatic +
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
To illustrate this process, we use the reference ontology (considered as a standard) described
|
To illustrate this process, we use the reference ontology (considered as a standard) described
|
||||||
in the listing \autoref{fig-Reference-Ontology-example}, defining the \<open>Resource\<close>, \<open>Electronic\<close>,
|
in the listing \autoref{fig-Reference-Ontology-example}, defining the \<^typ>\<open>Resource\<close>,
|
||||||
\<open>Component\<close>, \<open>Informatic\<close>, \<open>Hardware\<close> and \<open>Software\<close> concepts (or classes).
|
\<^typ>\<open>Electronic\<close>, \<^typ>\<open>Component\<close>,\<^typ>\<open>Informatic\<close>, \<^typ>\<open>Hardware\<close> and \<^typ>\<open>R_Software\<close>
|
||||||
|
concepts (or classes).
|
||||||
Each class contains a set of attributes or properties and some local invariants.
|
Each class contains a set of attributes or properties and some local invariants.
|
||||||
|
|
||||||
In our example, we focus on the \<open>Hardware\<close> class containing a \<open>mass\<close> attribute and composed of a list
|
In our example, we focus on the \<^typ>\<open>Hardware\<close> class containing a \<^const>\<open>mass\<close> attribute
|
||||||
of components with a \<open>mass\<close> attribute formalising the mass value of each component. The \<open>Hardware\<close>
|
and composed of a list of components with a \<^const>\<open>mass\<close> attribute formalising
|
||||||
class also contains a local invariant \<open>c1\<close> to define a constraint linking the global mass of
|
the mass value of each component.
|
||||||
a \<open>Hardware\<close> object with the masses of its own components.
|
The \<^typ>\<open>Hardware\<close> class also contains a local \<^theory_text>\<open>invariant c1\<close>
|
||||||
|
to define a constraint linking the global mass of a \<^typ>\<open>Hardware\<close> object
|
||||||
|
with the masses of its own components.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
|
@ -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
|
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
|
objects. This ontology is described in \autoref{fig-Local-Ontology-example} and
|
||||||
defines the \<open>Item\<close>, \<open>Product\<close>, \<open>Computer_Software\<close>
|
defines the \<^typ>\<open>Item\<close>, \<^typ>\<open>Product\<close>, \<^typ>\<open>Computer_Software\<close>
|
||||||
and \<open>Computer_Hardware\<close> concepts. As for the reference ontology, we focus on the \<open>Computer_Hardware\<close>
|
and \<^typ>\<open>Computer_Hardware\<close> concepts.
|
||||||
class defined as a list of products characterised by their mass value. This class contains a local
|
As for the reference ontology, we focus on the \<^typ>\<open>Computer_Hardware\<close>
|
||||||
invariant \<open>c2\<close> to guarantee that its own mass value equals the sum of all the masses of the products
|
class defined as a list of products characterised by their mass value.
|
||||||
composing the object.
|
This class contains a local \<^theory_text>\<open>invariant c2\<close> to guarantee that its own mass value
|
||||||
|
equals the sum of all the masses of the products composing the object.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
@ -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)
|
define the relationship between one class of the local ontology to one or several other class(es)
|
||||||
described in the reference ontology.
|
described in the reference ontology.
|
||||||
|
|
||||||
For example,\<open>Product_to_Component_morphism\<close> and \<open>Computer_Hardware_to_Hardware_morphism\<close> definitions,
|
For example, \<^const>\<open>Product_to_Component_morphism\<close> and \<^const>\<open>Computer_Hardware_to_Hardware_morphism\<close>
|
||||||
detailed in the figure \autoref{fig-mapping-example}, specify how \<open>Product\<close> or \<open>Computer_Hardware\<close>
|
definitions, detailed in \autoref{fig-mapping-example},
|
||||||
objects are mapped to \<open>Component\<close>
|
specify how \<^typ>\<open>Product\<close> or \<^typ>\<open>Computer_Hardware\<close> objects are mapped to \<^typ>\<open>Component\<close>
|
||||||
or \<open>Hardware\<close> objects defined in the reference ontology. This mapping shows that the structure
|
or \<^typ>\<open>Hardware\<close> objects defined in the reference ontology.
|
||||||
of a (user) ontology may be quite different from the one of a standard ontology she references.
|
This mapping shows that the structure of a (user) ontology may be quite different
|
||||||
|
from the one of a standard ontology it references.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue