diff --git a/src/tests/Mapped_PILIB_Ontology.thy b/src/tests/Mapped_PILIB_Ontology.thy new file mode 100644 index 00000000..eb184392 --- /dev/null +++ b/src/tests/Mapped_PILIB_Ontology.thy @@ -0,0 +1,77 @@ +theory Mapped_PILIB_Ontology + imports "Isabelle_DOF.Isa_DOF" + +begin + +text\User 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 | + Expansion_Card | + Storage_Device | + Fixed_Media | + Removable_Media | + Input_Device | + Output_Device + +onto_class Computer_Hardware = Product + + type :: Hardware_Type + composed_of :: "Product set" + +text\Reference Ontology\ + +onto_class Resource = + resource_name :: string + +onto_class Electronic = Resource + + provider :: string + manufacturer :: string + +onto_class Component = Electronic + + mass :: int + dimensions :: "int set" + +onto_class Simulation_Model = Electronic + + type :: string + +onto_class Informatic = Resource + + att :: string + +onto_class Hardware = Informatic + + type :: Hardware_Type + mass :: int + composed_of :: "Component set" + +onto_class R_Software = Informatic + + version :: int + +definition Item_to_Resource_morphism + where "Item_to_Resource_morphism (\::'a Item_scheme) = + \ tag_attribute = 0::int + , resource_name = item_name \ + \" + + +definition U_Software_to_R_Software_morphism + where "U_Software_to_R_Software_morphism (\::'a U_Software_scheme) = + \ tag_attribute = 1::int + , resource_name = Item.item_name \ + , att = '''' + , version = U_Software.version \ + \" + +end \ No newline at end of file