diff --git a/src/tests/Mapped_PILIB_Ontology.thy b/src/tests/Mapped_PILIB_Ontology.thy index 87bc3c8..93325a4 100644 --- a/src/tests/Mapped_PILIB_Ontology.thy +++ b/src/tests/Mapped_PILIB_Ontology.thy @@ -25,21 +25,6 @@ term\fold (+) S 0\ definition sum where "sum S = (fold (+) S 0)" -text\Local Ontology\ - -onto_class Item = - item_name :: string - -onto_class Product = Item + - serial_number :: int - provider :: string - mass :: int - -onto_class U_Software = Item + - version :: int - -onto_class Electronic_Component = Product + - dimensions :: "int set" datatype Hardware_Type = Motherboard | @@ -50,15 +35,11 @@ datatype Hardware_Type = Input_Device | Output_Device -onto_class Computer_Hardware = Product + - type :: Hardware_Type - composed_of :: "Product list" - invariant c1 :: "Product.mass \ = sum(map Product.mass (composed_of \))" text\Reference Ontology\ onto_class Resource = - resource_name :: string + name :: string onto_class Electronic = Resource + provider :: string @@ -66,13 +47,13 @@ onto_class Electronic = Resource + onto_class Component = Electronic + mass :: int - dimensions :: "int set" + dimensions :: "int list" onto_class Simulation_Model = Electronic + type :: string onto_class Informatic = Resource + - att :: string + description :: string onto_class Hardware = Informatic + type :: Hardware_Type @@ -80,6 +61,95 @@ onto_class Hardware = Informatic + composed_of :: "Component list" invariant c2 :: "mass \ = sum(map Component.mass (composed_of \))" +onto_class R_Software = Informatic + + version :: int + + +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). +\ + + +text\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 c1 :: "Product.mass \ = sum(map Product.mass (composed_of \))" + + +text\ +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. +\ + +definition Item_to_Resource_morphism + where "Item_to_Resource_morphism (\::'a Item_scheme) = + \ + Resource.tag_attribute = 0::int , + Resource.name = name \ + \" + +definition Product_to_Component_morphism + where "Product_to_Component_morphism (\::'a Product_scheme) = + \ + Resource.tag_attribute = 1::int , + Resource.name = name \ , + Electronic.provider = Product.provider \ , + Electronic.manufacturer = '''' , + Component.mass = Product.mass \ , + Component.dimensions = [] + \" + +definition Computer_Hardware_to_Hardware_morphism + where "Computer_Hardware_to_Hardware_morphism (\::'a Computer_Hardware_scheme) = + \ + 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 \) + \" + + +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. +\ + +text\Now we check that the invariant is preserved through the morphism:\ + +lemma inv_c1_preserved : + "c1_inv \ \ c2_inv (Computer_Hardware_to_Hardware_morphism \)" + unfolding c2_inv_def c1_inv_def Computer_Hardware_to_Hardware_morphism_def + by auto + + +lemma Computer_Hardware_to_Hardware_morphism_total : + "Computer_Hardware_to_Hardware_morphism ` ({X::Computer_Hardware. c1_inv X}) \ ({X::Hardware. c2_inv X})" + using inv_c1_preserved + by auto + declare[[invariants_checking]] declare[[invariants_checking_with_tactics]] @@ -97,51 +167,4 @@ value*\ @{Hardware \h1\} = @{Hardware \h2\} \ -onto_class R_Software = Informatic + - version :: int - -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. -\ - -definition Item_to_Resource_morphism - where "Item_to_Resource_morphism (\::'a Item_scheme) = - \ tag_attribute = 0::int - , resource_name = item_name \ - \" - - -definition Resource_to_Item_morphism - where "Resource_to_Item_morphism (\::'a Resource_scheme) = - \ Item.tag_attribute = 1::int - , item_name = '' '' - \" - -definition Hardware_to_Computer_Hardware_morphism - where "Hardware_to_Computer_Hardware_morphism (\::'a Hardware_scheme) = - \ Item.tag_attribute = 2::int - , item_name = Resource.resource_name \ - \" - -(* -definition U_Software_to_R_Software_morphism - where "U_Software_to_R_Software_morphism (\::'a U_Software_scheme) = - \ tag_attribute = 2::int - , resource_name = Item.item_name \ - , att = '''' - , version = U_Software.version \ - \" -*) - end \ No newline at end of file