Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

some elements of chapter Proof_Ontologies.

This commit is contained in:
Burkhart Wolff 2024-04-07 22:04:09 +02:00
parent 28d1fa926e
commit 4745c58803
3 changed files with 262 additions and 139 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
Isabelle_DOF/document/root.bib
View File

@ -10,6 +10,39 @@
year = 2015
}
@
Book{ books/daglib/0032976,
added-at = {2014-03-12T00:00:00.000+0100},
author = {Euzenat, J{\~A}<7D>r{\~A}<7D>me and Shvaiko, Pavel},
biburl = {https://www.bibsonomy.org/bibtex/28d5372a81f181d9d5a761ca12209cf39/dblp},
interhash = {fc55a5b84d114e38db0a0303cc1bd7da},
intrahash = {8d5372a81f181d9d5a761ca12209cf39},
isbn = {978-3-642-38720-3},
keywords = {dblp},
pages = {I-XVII, 1--511},
publisher = {Springer},
timestamp = {2015-06-18T09:49:52.000+0200},
title = {Ontology Matching, Second Edition.},
year = 2013,
doi = {10.1007/978-3-642-38721-0}
}
@Misc{ atl,
title = {{ATL} -- A model transformation technology},
url = {https://www.eclipse.org/atl/},
author = {{Eclipse Foundation}},
}
@InProceedings{ BGPP95,
author = {Yamine A{\"{\i}}t Ameur and Frederic Besnard and Patrick Girard and Guy Pierra and Jean{-}Claude
Potier},
title = {Formal Specification and Metaprogramming in the {EXPRESS} Language},
booktitle = {The 7th International Conference on Software Engineering and Knowledge Engineering (SEKE)},
pages = {181--188},
publisher = {Knowledge Systems Institute},
year = 1995
}
@Misc{ ibm:doors:2019,
author = {IBM},
title = {{IBM} Engineering Requirements Management {DOORS} Family},

1
Isabelle_DOF/ontologies/technical_report/technical_report.thy
View File

@ -106,7 +106,6 @@ theorem articles_sub_reports: \<open>(Lang article_monitor) \<subseteq> Lang rep
text\<open>The proof proceeds by blindly applying the monotonicity rules
on the language of regular expressions.\<close>
print_doc_classes
text\<open>All Class-Id's --- should be generated.\<close>
lemmas class_ids =

367
Isabelle_DOF/thys/manual/M_05_Proofs_Ontologies.thy
View File

@ -22,149 +22,41 @@ begin
(*>*)
section*["morphisms"::scholarly_paper.text_section] \<open>Proving Morphisms on Ontologies\<close>
chapter*[onto_proofs::technical]\<open>Proofs on Ontologies\<close>
(* rethink examples: should we "morph" previdence too ? ? ? *)
text\<open>It is a distinguishing feature of \<^dof> that it does not directly generate meta-data rather
than generating a \<^emph>\<open>theory of meta-data\<close> that can be used in HOL-terms on various levels
of the Isabelle-system and its document generation technology. Meta-data theories can be
converted into executable code and efficiently used in validations, but also used for theoretic
reasoning over given ontologies. While the full potential of this latter possibility still
needs to be explored, we present in the following sections two applications:
(*<*)
(* Mapped_PILIB_Ontology example *)
term\<open>fold (+) S 0\<close>
\<^enum> Verified ontological morphisms, also called \<^emph>\<open>ontological mappings\<close> in the literature
\<^cite>\<open>"books/daglib/0032976" and "atl" and "BGPP95"\<close>, \<^ie> proofs of invariant preservation
along translations of \<^verbatim>\<open>doc_class\<close>-instances.
\<^enum> Verified refinement relations between the structural descriptions of theory documents,
\<^ie> proofs of language inclusions of monitors of global ontology classes.
\<close>
definition sum
where "sum S = (fold (+) S 0)"
section*["morphisms"::scholarly_paper.text_section] \<open>Proving Properties over Ontologies\<close>
datatype Hardware_Type =
Motherboard |
Expansion_Card |
Storage_Device |
Fixed_Media |
Removable_Media |
Input_Device |
Output_Device
subsection\<open>Proving the Preservation of Ontological Mappings : A Document-Ontology Morphism\<close>
datatype Software_Type =
Operating_system |
Text_editor |
Web_Navigator |
Development_Environment
(* Reference Ontology *)
onto_class Resource =
name :: string
onto_class Electronic = Resource +
provider :: string
manufacturer :: string
onto_class Component = Electronic +
mass :: int
onto_class Simulation_Model = Electronic +
simulate :: Component
composed_of :: "Component list"
version :: int
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 Software = Informatic +
type :: Software_Type
version :: int
(* Local Ontology *)
onto_class Item =
name :: string
onto_class Product = Item +
serial_number :: int
provider :: string
mass :: int
onto_class Electronic_Component = Product +
serial_number :: int
onto_class Monitor = Product +
composed_of :: "Electronic_Component list"
invariant c2 :: "Product.mass \<sigma> = sum(map Product.mass (composed_of \<sigma>))"
term\<open>Product.mass \<sigma> = sum(map Product.mass (composed_of \<sigma>))\<close>
onto_class Computer_Software = Item +
type :: Software_Type
version :: int
(* Mapping or Morphism *)
definition Item_to_Resource_morphism :: "Item \<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 = 1::int ,
Resource.name = name \<sigma> \<rparr>"
definition Product_to_Resource_morphism :: "Product \<Rightarrow> Resource"
("_ \<langle>Resource\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999)
where " \<sigma> \<langle>Resource\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t =
\<lparr> Resource.tag_attribute = 2::int ,
Resource.name = name \<sigma> \<rparr>"
definition Computer_Software_to_Software_morphism :: "Computer_Software \<Rightarrow> Software"
("_ \<langle>Software\<rangle>\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p" [1000]999)
where "\<sigma> \<langle>Software\<rangle>\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p =
\<lparr> Resource.tag_attribute = 3::int ,
Resource.name = name \<sigma> ,
Informatic.description = ''no description'',
Software.type = type \<sigma> ,
Software.version = version \<sigma> \<rparr>"
definition Electronic_Component_to_Component_morphism :: "Electronic_Component \<Rightarrow> Component"
("_ \<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p" [1000]999)
where "\<sigma> \<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p =
\<lparr> Resource.tag_attribute = 4::int ,
Resource.name = name \<sigma> ,
Electronic.provider = provider \<sigma> ,
Electronic.manufacturer = ''no manufacturer'' ,
Component.mass = mass \<sigma> \<rparr>"
definition Monitor_to_Hardware_morphism :: "Monitor \<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 = 5::int ,
Resource.name = name \<sigma> ,
Informatic.description = ''no description'',
Hardware.type = Output_Device,
Hardware.mass = mass \<sigma> ,
Hardware.composed_of = map Electronic_Component_to_Component_morphism (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
Monitor_to_Hardware_morphism_def Electronic_Component_to_Component_morphism_def
by (auto simp: comp_def)
lemma Monitor_to_Hardware_morphism_total :
"Monitor_to_Hardware_morphism ` ({X::Monitor. c2_inv X}) \<subseteq> ({X::Hardware. c1_inv X})"
using inv_c2_preserved
by auto
type_synonym local_ontology = "Item * Electronic_Component * Monitor"
type_synonym reference_ontology = "Resource * Component * Hardware"
fun ontology_mapping :: "local_ontology \<Rightarrow> reference_ontology" where
"ontology_mapping (x, y, z) = (x \<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m , y \<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p, z \<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)"
lemma ontology_mapping_total :
"ontology_mapping ` {X. c2_inv (snd (snd X))}
\<subseteq> {X. c1_inv (snd (snd X))}"
using inv_c2_preserved
by auto
text\<open>\<^dof> as a system is currently particularly geared towards \<^emph>\<open>document\<close>-ontologies, in
particular for documentations generated from Isabelle theories. We used it meanwhile for the
generation of various conference and journal papers, notably using the
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close> and \<^theory>\<open>Isabelle_DOF.technical_report\<close>-ontologies,
targeting a (small) variety of \<^LaTeX> style-files. A particular aspect of these ontologies,
especially when targeting journals from publishers such as ACM, Springer or Elsevier, is the
description of publication meta-data. Publishers tend to have their own styles on what kind
meta-data should be associated with a journal publication; thus, the depth and
precise format of affiliations, institution, their relation to authors, and author descriptions
(with photos or without, hair left-combed or right-combed, etcpp...) varies.
In the following, we present an attempt to generalized ontology with several ontology mappings
to more specialized ones such as concrete journals and/or the \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>-
ontology which we mostly used for our own publications.
\<close>
doc_class "title" = short_title :: "string option" <= "None"
@ -405,13 +297,212 @@ onto_morphism (AA, BB, CC, DD, EE) to FF
find_consts name:"convert"
find_theorems name:"convert"
subsection\<open>Proving the Preservation of Ontological Mappings : A Domain-Ontology Morphism\<close>
(* rethink examples: should we "morph" providence too ? ? ? Why not ? bu *)
(*<*)
(* 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
datatype Software_Type =
Operating_system |
Text_editor |
Web_Navigator |
Development_Environment
chapter*[onto_proofs::technical]\<open>Proofs on Ontologies\<close>
(* Reference Ontology *)
onto_class Resource =
name :: string
onto_class Electronic = Resource +
provider :: string
manufacturer :: string
onto_class Component = Electronic +
mass :: int
onto_class Simulation_Model = Electronic +
simulate :: Component
composed_of :: "Component list"
version :: int
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 Software = Informatic +
type :: Software_Type
version :: int
(* Local Ontology *)
onto_class Item =
name :: string
onto_class Product = Item +
serial_number :: int
provider :: string
mass :: int
onto_class Electronic_Component = Product +
serial_number :: int
onto_class Monitor = Product +
composed_of :: "Electronic_Component list"
invariant c2 :: "Product.mass \<sigma> = sum(map Product.mass (composed_of \<sigma>))"
term\<open>Product.mass \<sigma> = sum(map Product.mass (composed_of \<sigma>))\<close>
onto_class Computer_Software = Item +
type :: Software_Type
version :: int
(* Mapping or Morphism *)
definition Item_to_Resource_morphism :: "Item \<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 = 1::int ,
Resource.name = name \<sigma> \<rparr>"
definition Product_to_Resource_morphism :: "Product \<Rightarrow> Resource"
("_ \<langle>Resource\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t" [1000]999)
where " \<sigma> \<langle>Resource\<rangle>\<^sub>P\<^sub>r\<^sub>o\<^sub>d\<^sub>u\<^sub>c\<^sub>t =
\<lparr> Resource.tag_attribute = 2::int ,
Resource.name = name \<sigma> \<rparr>"
definition Computer_Software_to_Software_morphism :: "Computer_Software \<Rightarrow> Software"
("_ \<langle>Software\<rangle>\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p" [1000]999)
where "\<sigma> \<langle>Software\<rangle>\<^sub>S\<^sub>o\<^sub>f\<^sub>t\<^sub>C\<^sub>m\<^sub>p =
\<lparr> Resource.tag_attribute = 3::int ,
Resource.name = name \<sigma> ,
Informatic.description = ''no description'',
Software.type = type \<sigma> ,
Software.version = version \<sigma> \<rparr>"
definition Electronic_Component_to_Component_morphism :: "Electronic_Component \<Rightarrow> Component"
("_ \<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p" [1000]999)
where "\<sigma> \<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p =
\<lparr> Resource.tag_attribute = 4::int ,
Resource.name = name \<sigma> ,
Electronic.provider = provider \<sigma> ,
Electronic.manufacturer = ''no manufacturer'' ,
Component.mass = mass \<sigma> \<rparr>"
definition Monitor_to_Hardware_morphism :: "Monitor \<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 = 5::int ,
Resource.name = name \<sigma> ,
Informatic.description = ''no description'',
Hardware.type = Output_Device,
Hardware.mass = mass \<sigma> ,
Hardware.composed_of = map Electronic_Component_to_Component_morphism (composed_of \<sigma>)
\<rparr>"
text\<open>On this basis, we can state the following invariant preservation theorems:\<close>
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
Monitor_to_Hardware_morphism_def Electronic_Component_to_Component_morphism_def
by (auto simp: comp_def)
lemma Monitor_to_Hardware_morphism_total :
"Monitor_to_Hardware_morphism ` ({X::Monitor. c2_inv X}) \<subseteq> ({X::Hardware. c1_inv X})"
using inv_c2_preserved
by auto
type_synonym local_ontology = "Item * Electronic_Component * Monitor"
type_synonym reference_ontology = "Resource * Component * Hardware"
fun ontology_mapping :: "local_ontology \<Rightarrow> reference_ontology"
where "ontology_mapping (x, y, z) = (x\<langle>Resource\<rangle>\<^sub>I\<^sub>t\<^sub>e\<^sub>m, y\<langle>Component\<rangle>\<^sub>E\<^sub>l\<^sub>e\<^sub>c\<^sub>C\<^sub>m\<^sub>p, z\<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)"
lemma ontology_mapping_total :
"ontology_mapping ` {X. c2_inv (snd (snd X))} \<subseteq> {X. c1_inv (snd (snd X))}"
using inv_c2_preserved
by auto
(*<*)
(* switch on regexp syntax *)
notation Star ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
notation Plus (infixr "||" 55)
notation Times (infixr "~~" 60)
notation Atom ("\<lfloor>_\<rfloor>" 65)
(*>*)
subsection\<open>Proving Monitor-Refinements\<close>
text\<open>Monitors are regular-expressions that allow for specifying instances of classes to appear in
a particular order in a document. They are used to specify some structural aspects of a document.
Based on an AFP theory by Tobias Nipkow on Functional Automata
(\<^ie> a characterization of regular automata using functional polymorphic descriptions of transition
functions avoiding any of the ad-hoc finitizations commonly used in automata theory), which
comprises also functions to generate executable deterministic and non-deterministic automata,
this theory is compiled to SML-code that was integrated in the \<^dof> system. The necessary
adaptions of this integration can be found in the theory \<^theory>\<open>Isabelle_DOF.RegExpInterface\<close>,
which also contains the basic definitions and theorems for the concepts used here.
Recall that the monitor of \<^term>\<open>scholarly_paper.article\<close> is defined by: \<^vs>\<open>0.5cm\<close>
@{thm [indent=20, margin=70, names_short] scholarly_paper.article_monitor_def}
\<^vs>\<open>0.5cm\<close> However, it is possible to reason over the language of monitors and prove classical
refinement notions such as trace-refinement on the monitor-level, so once-and-for-all for all
instances of validated documents conforming to a particular ontology. The primitive recursive
operators\<^term>\<open>RegExpInterface.Lang\<close> and \<^term>\<open>RegExpInterface.L\<^sub>s\<^sub>u\<^sub>b\<close> generate the languages of the
regular expression language, where \<^term>\<open>L\<^sub>s\<^sub>u\<^sub>b\<close> takes the sub-ordering relation of classes into
account.
The proof of : \<^vs>\<open>0.5cm\<close>
@{thm [indent=20,margin=70,names_short] articles_sub_reports}
\<^vs>\<open>0.5cm\<close> can be found in theory \<^theory>\<open>Isabelle_DOF.technical_report\<close>;
it is, "as simple as it should be" (to cite Tony Hoare).
The proof of: \<^vs>\<open>0.5cm\<close>
@{thm [indent=20,margin=70,names_short] articles_Lsub_reports}
\<^vs>\<open>0.5cm\<close> is slightly more evolved; this is due to the fact that \<^dof> does not generate a proof of the
acyclicity of the graph of the class-hierarchy @{term doc_class_rel} automatically. For a given
hierarchy, this proof will always succeed (since \<^dof> checks this on the meta-level, of course),
which permits to deduce the anti-symmetry of the transitive closure of @{term doc_class_rel}
and therefore to establish that the doc-classes can be organized in an order (\<^ie> the
type \<^typ>\<open>doc_class\<close> is an instance of the type-class \<^class>\<open>order\<close>). On this basis, the proof
of the above language refinement is quasi automatic. This proof is also part of
\<^theory>\<open>Isabelle_DOF.technical_report\<close>.
\<close>
(*<*)
(* switch on regexp syntax *)
no_notation Star ("\<lbrace>(_)\<rbrace>\<^sup>*" [0]100)
no_notation Plus (infixr "||" 55)
no_notation Times (infixr "~~" 60)
no_notation Atom ("\<lfloor>_\<rfloor>" 65)
end
(*>*)