First corrections inrelation to the reviews

- Add ontology in document
- Add antiquations to reference classes, etc.

examples/scholarly_paper/2020-iFM-CSP/paper.thy

@@ -48,8 +48,8 @@ abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Alg
 
    If you consider citing this paper, please refer to @{cite "HOL-CSP-iFM2020"}.
 \<close>
-text\<open>\<close>
-section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close> 
+
+section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close>
 text*[introtext::introduction]\<open>
 Communicating Sequential Processes (\<^csp>) is a language 
 to specify and verify patterns of interaction of concurrent systems.

examples/scholarly_paper/2021-ITP-PMTI/ROOT

@@ -0,0 +1,29 @@
+session "2021-ITP-PMTI" = "Isabelle_DOF" +
+  options [document = pdf, document_output = "output", document_build = dof,
+    document_comment_latex = true]
+  theories
+    "paper"
+  document_files
+    "isadof.cfg"
+    "root.bib"
+    "preamble.tex"
+    "lipics-v2021.cls"
+    "cc-by.pdf"
+    "lipics-logo-bw.pdf"
+    "orcid.pdf"
+    "figures/Req-Appl-ex.png"
+    "figures/formal-development.png"
+    "figures/Req-Def-ex.png"
+    "figures/odometer.jpeg"
+    "figures/cicm2018-combined.png"
+    "figures/three-phase-odo.pdf"
+    "figures/df-numerics-encshaft.png"
+    "figures/wheel-df.png"
+    "figures/invariant-checking-violated-example.png"
+    "figures/inherited-invariant-checking-violated-example.png"
+    "figures/term-context-checking-example.png"
+    "figures/term-context-failed-checking-example.png"
+    "figures/term-context-evaluation-example.png"
+    "figures/term-context-failed-evaluation-example.png"
+    "figures/term-context-equality-evaluation-example.png"
+    "lstisadof.sty"

examples/scholarly_paper/2021-ITP-PMTI/document/isadof.cfg

@@ -0,0 +1,2 @@
+Template: lipics-v2021
+Ontology: scholarly_paper

examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof.sty

@@ -0,0 +1,195 @@
+%% Copyright (C) 2018 The University of Sheffield
+%%               2018 The University of Paris-Saclay
+%%               2019 The University of Exeter
+%%
+%% License:
+%%   This program can be redistributed and/or modified under the terms
+%%   of the LaTeX Project Public License Distributed from CTAN
+%%   archives in directory macros/latex/base/lppl.txt; either
+%%   version 1.3c of the License, or (at your option) any later version.
+%%   OR
+%%   The 2-clause BSD-style license.
+%%
+%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
+\usepackage{listings}
+\usepackage{listingsutf8}
+\usepackage{tikz}
+\usepackage[many]{tcolorbox}
+\tcbuselibrary{listings}
+\tcbuselibrary{skins}
+\usepackage{xstring}
+
+\definecolor{OliveGreen}    {cmyk}{0.64,0,0.95,0.40}
+\definecolor{BrickRed}      {cmyk}{0,0.89,0.94,0.28}
+\definecolor{Blue}          {cmyk}{1,1,0,0}
+\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
+
+%%%\lst@BeginAspect[keywords]{isar}
+\gdef\lst@tagtypes{s}
+\gdef\lst@TagKey#1#2{%
+    \lst@Delim\lst@tagstyle #2\relax
+        {Tag}\lst@tagtypes #1%
+                     {\lst@BeginTag\lst@EndTag}%
+        \@@end\@empty{}}
+\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
+\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
+\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
+\gdef\lst@BeginTag{%
+    \lst@DelimOpen
+        \lst@ifextags\else
+        {\let\lst@ifkeywords\iftrue
+         \lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
+\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
+\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
+\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
+\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
+\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
+\global\let\lst@iffirstintag\iffalse
+ \lst@AddToHook{PostOutput}{\lst@tagresetfirst}
+ \lst@AddToHook{Output}
+     {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
+ \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
+\lst@AddToHook{Output}
+    {\ifnum\lst@mode=\lst@tagmode
+         \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
+         \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
+     \fi}
+\lst@NewMode\lst@tagmode
+\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
+    \lst@CArg #1\relax\lst@DefDelimB {}{}%
+        {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
+        #3\lst@tagmode{#5}%
+    \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
+\gdef\lst@BeginCDATA#1\@empty{%
+    \lst@TrackNewLines \lst@PrintToken
+    \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
+    \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
+%%\lst@EndAspect
+
+
+
+% \gdef\lst@BeginTag{%
+%     \lst@DelimOpen
+%     \lst@ifextags\else
+%         {\let\lst@ifkeywords\iftrue
+%          \lst@ifmarkfirstintag\lst@firstintagtrue\fi\color{green}}}
+% \gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else\color{green}}
+
+\def\beginlstdelim#1#2#3%
+{%
+    \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
+    \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% <isar>
+\providecolor{isar}{named}{gray}
+%\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
+\newcommand{\inlineisarbox}[1]{#1}
+\NewTColorBox[]{isarbox}{}{
+     ,boxrule=0pt
+     ,boxsep=0pt
+     ,colback=white!90!isar
+     ,enhanced jigsaw
+     ,borderline west={2pt}{0pt}{isar!60!black}
+     ,sharp corners
+     ,before skip balanced=0.5\baselineskip plus 2pt
+     % ,before skip=10pt
+     % ,after skip=10pt
+     ,enlarge top by=0mm
+     ,enhanced
+     ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
+       east,font=\bfseries\footnotesize\color{white}]
+                at (frame.north east) {Isabelle code};}
+}
+%% </isar>
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\subscr}[1]{\ensuremath{_{\mbox{#1}}}}
+\newcommand{\supscr}[1]{\ensuremath{^{\mbox{#1}}}}
+\lstdefinestyle{ISAR}{%
+  language=%
+  ,basicstyle=\ttfamily%
+  ,showspaces=false%
+  ,showlines=false%
+  ,columns=flexible%
+  ,morecomment=[s]{(*}{*)}%
+  % ,moredelim=*[s][\rmfamily]{\{*}{*\}}%
+  ,moredelim = **[is][\beginlstdelim{\{*}{*\}}{black}]{\{*}{*\}}
+  ,showstringspaces=false%
+  ,moredelim=*[is][\supscr]{\\<^bsup>}{\\<^esup>}%
+  ,literate={%
+    {...}{\,\ldots\,}3%
+    {\\<Open>}{\ensuremath{\isacartoucheopen}}1%
+    {\\at}{@}1%
+    {\\<Close>}{\ensuremath{\isacartoucheclose}}1%
+    {\\<Gamma>}{\ensuremath{\Gamma}}1%
+    {\\<times>}{\ensuremath{\times}}1%
+    {\\<rbrakk>}{\ensuremath{\mathclose{\rbrack\mkern-3mu\rbrack}}}1%
+    {\\<rbrace>}{\ensuremath{\mathclose{\mid\mkern-4.5mu\rbrace}}}1%
+    {\\<lbrakk>}{\ensuremath{\mathopen{\lbrack\mkern-3mu\lbrack}}}1%
+    {\\<lbrace>}{\ensuremath{\mathopen{\lbrace\mkern-4.5mu\mid}}}1%
+    {\\<Rightarrow>}{\ensuremath{\Rightarrow}}1%
+    {\{*}{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}1%
+    {*\}}{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}1%
+  }%
+  % % Defining "tags" (text-antiquotations) based on 1-keywords
+   ,tag=**[s]{@\{}{\}}%
+   ,tagstyle=\color{CornflowerBlue}%
+   ,markfirstintag=true%
+   ,keywordstyle=\bfseries%
+   ,keywords={}
+   % Defining 2-keywords
+   ,keywordstyle=[2]{\color{Blue!60}\bfseries}%
+   ,alsoletter={*,-}
+   ,morekeywords=[2]{theory, begin, end, ML,section,subsection,paragraph,chapter,text}%
+   %,moredelim=[s][\textit]{<}{>}
+   % Defining 3-keywords
+   ,keywordstyle=[3]{\color{OliveGreen!60}\bfseries}%
+   ,morekeywords=[3]{doc_class,declare_reference,update_instance*,
+     open_monitor*, close_monitor*, figure*, title*, subtitle*,declare_reference*,section*,text*}%
+   % Defining 4-keywords
+   ,keywordstyle=[4]{\color{black!60}\bfseries}%
+   ,morekeywords=[4]{where, imports}%
+   % Defining 5-keywords
+   ,keywordstyle=[5]{\color{BrickRed!70}\bfseries}%
+   ,morekeywords=[5]{datatype, typedecl, consts, theorem}%
+   % Defining 6-keywords
+   ,keywordstyle=[6]{\itshape}%
+   ,morekeywords=[6]{meta-args, ref, expr, class_id}%
+  % 
+}%
+%% 
+\lstnewenvironment{isar}[1][]{\lstset{style=ISAR,
+    backgroundcolor=\color{black!2},
+    frame=lines,
+    mathescape=true,
+    basicstyle=\footnotesize\ttfamily,#1}}{}
+%%% 
+\def\inlineisar{\lstinline[style=ISAR,breaklines=true,mathescape,breakatwhitespace=true]}
+
+\lstnewenvironment{out}[1][]{\lstset{
+    backgroundcolor=\color{green!2},
+    frame=lines,mathescape,breakatwhitespace=true
+    ,columns=flexible%
+    ,basicstyle=\footnotesize\rmfamily,#1}}{}
+
+
+%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%
+\lstloadlanguages{ML}
+\lstdefinestyle{sml}{basicstyle=\ttfamily,%
+                     commentstyle=\itshape,%
+                     keywordstyle=\bfseries\color{CornflowerBlue},%
+                     ndkeywordstyle=\color{red},%
+                     language=ML,
+                      ,keywordstyle=[6]{\itshape}%
+                      ,morekeywords=[6]{args_type}%
+                    }%
+
+\lstnewenvironment{sml}[1][]{\lstset{style=sml,
+    backgroundcolor=\color{Blue!4},
+    frame=lines,
+    basicstyle=\footnotesize\ttfamily,#1}}{}
+%%% 
+\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}

examples/scholarly_paper/2021-ITP-PMTI/document/preamble.tex

@@ -0,0 +1,40 @@
+%% This is a placeholder for user-specific configuration and packages. 
+
+\usepackage{stmaryrd}
+\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}%
+\IfFileExists{upquote.sty}{\usepackage{upquote}}{}%
+\usepackage{textcomp}
+\usepackage{xcolor}
+\usepackage{paralist}
+\usepackage{listings}
+\usepackage{lstisadof}
+\usepackage{xspace}
+
+\newcommand{\fixIsarList}{\vspace{-\topsep}\vspace{-\baselineskip}\mbox{}\\[0pt]\noindent}
+
+\nolinenumbers
+%\title{<TITLE>}
+%\author{<AUTHOR>}
+\titlerunning{Proving Ontology-Relations, Testing Ontology Instances}
+\author{Idir Ait-Sadoune}
+  {LMF, CentraleSupélec, Université Paris-Saclay, Paris, France}
+  {idir.aitsadoune@centralesupelec.fr}
+  {https://orcid.org/0000-0002-6484-8276}
+  {}
+%\author{Nicolas Méric}
+%  {LMF, Université Paris-Saclay, Paris, France}
+%  {nicolas.meric@universite-paris-saclay.fr}
+%  {https://orcid.org/0000-0002-0756-7072}
+%  {}
+%\author{Burkhart Wolff}
+%  {LMF, Université Paris-Saclay, Paris, France}
+%  {burkhart.wolff@universite-paris-saclay.fr}
+%  {}
+%  {}
+\Copyright{Idir Ait-Sadoune, Nicolas Méric, and Burkhart Wolff}
+\authorrunning{I. Ait-Sadoune, N. Méric and B. Wolff}
+\keywords{Ontologies, Formal Documents, Formal Development, Isabelle/HOL, Ontology Mapping}
+\ccsdesc{Computing methodologies~Ontology engineering}
+\ccsdesc{Information systems~Ontologies}
+\ccsdesc{Theory of computation~Interactive proof systems}
+\ccsdesc{Theory of computation~Higher order logic}

src/tests/Mapped_PILIB_Ontology.thy

@@ -0,0 +1,197 @@
+theory Mapped_PILIB_Ontology
+  imports "Isabelle_DOF.Isa_DOF"
+
+
+begin
+
+
+define_shortcut* hol      \<rightleftharpoons> \<open>HOL\<close>
+                 isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+                 dof      \<rightleftharpoons> \<open>Isabelle/DOF\<close>
+                 LaTeX    \<rightleftharpoons> \<open>LaTeX\<close>
+                 html     \<rightleftharpoons> \<open>HTML\<close>
+                 csp      \<rightleftharpoons> \<open>CSP\<close>      \<comment>\<open>obsolete\<close>
+                 holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>  \<comment>\<open>obsolete\<close> 
+
+
+
+
+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
+
+text\<open>
+\<^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.
+\<close>
+
+(* 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
+
+text\<open>
+To illustrate this process, we use the reference ontology (considered as a standard) described 
+in the listing X, defining the Resource, Electronic, Component, Informatic, Hardware and 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.  
+\<close>
+
+(* 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>))"
+
+text\<open>
+For the needs of our document, we have defined a simple ontology to classify Software and Hardware 
+objects. This ontology is described in listing X 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.
+\<close>
+
+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>" 
+
+
+text\<open>
+To check the coherence of our local ontology, we define a relationship between the local ontology 
+and the reference ontology using morphism functions (or mapping rules). These rules are applied to 
+define the relationship between one class of the local ontology to one or several other class(es) 
+described in the reference ontology. 
+
+For example,\<open>Product_to_Component_morphism\<close> and \<open>Computer_Hardware_to_Hardware_morphism\<close> definitions,
+detailed in the figure Z, specify how \<open>Product\<close> or \<open>Computer_Hardware\<close> objects are mapped to \<open>Component\<close> 
+or \<open>Hardware\<close> 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. 
+\<close>
+
+
+
+
+find_theorems Hardware.composed_of
+
+find_theorems Hardware.mass
+
+find_theorems map "(o)"
+
+
+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
+
+
+
+
+declare[[invariants_checking]]
+declare[[invariants_checking_with_tactics]]
+
+text*[c1::Component, mass=4]\<open>\<close>
+text*[c2::Component, mass=4]\<open>\<close>
+
+text*[h1::Hardware, mass=8, composed_of="[@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}]"]\<open>\<close>
+text*[h2::Hardware, mass=8, composed_of="[@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}]"]\<open>\<close>
+
+value*\<open>
+sum (map Component.mass [@{Component \<open>c1\<close>},@{Component \<open>c2\<close>}])
+\<close>
+
+value*\<open>
+@{Hardware \<open>h1\<close>} = @{Hardware \<open>h2\<close>}
+\<close>
+
+end

src/tests/OntoMathPro_Ontology.thy

@@ -0,0 +1,75 @@
+theory OntoMathPro_Ontology
+  imports "Isabelle_DOF.Isa_DOF"
+begin
+
+datatype dc = creator string | title string
+
+datatype owl =
+    backwardCompatibleWith string
+  | deprecated string
+  | incompatibleWith string
+  | priorVersion string
+  | versionInfo string
+  
+datatype rdfs =
+    comment string
+  | isDefinedBy string
+  | label string
+  | seeAlso string
+
+datatype annotation = DC dc | OWL owl |  RDFS rdfs
+
+
+onto_class Top =
+  Annotations :: "annotation list"
+
+onto_class Field_of_mathematics =
+  Annotations :: "annotation list"
+  invariant restrict_annotation_F ::"set (Annotations \<sigma>) \<subseteq>
+                                              range (RDFS o label) \<union> range (RDFS o comment)"
+
+onto_class Mathematical_knowledge_object =
+  Annotations :: "annotation list"
+  invariant restrict_annotation_M ::"set (Annotations \<sigma>) \<subseteq>
+                                              range (RDFS o label) \<union> range (RDFS o comment)"
+
+onto_class assoc_F_M =
+  contains:: "(Field_of_mathematics \<times> Mathematical_knowledge_object) set"
+  invariant contains_defined :: "\<forall> x. x \<in> Domain (contains \<sigma>)
+                                              \<longrightarrow> (\<exists> y \<in> Range (contains \<sigma>). (x, y) \<in> contains \<sigma>)"
+
+onto_class assoc_M_F =
+  belongs_to :: "(Mathematical_knowledge_object \<times> Field_of_mathematics) set"
+  invariant belong_to_defined :: "\<forall> x. x \<in> Domain (belongs_to \<sigma>)
+                                           \<longrightarrow> (\<exists> y \<in> Range (belongs_to \<sigma>). (x, y) \<in> belongs_to \<sigma>)"
+
+onto_class assoc_M_M =
+  is_defined_by :: "(Mathematical_knowledge_object \<times> Mathematical_knowledge_object) set"
+  invariant is_defined_by_defined :: "\<forall> x. x \<in> Domain (is_defined_by \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (is_defined_by \<sigma>). (x, y) \<in> is_defined_by \<sigma>)"
+
+onto_class assoc_M_M' =
+  "defines" :: "(Mathematical_knowledge_object \<times> Mathematical_knowledge_object) set"
+  invariant defines_defined :: "\<forall> x. x \<in> Domain (defines \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (defines \<sigma>). (x, y) \<in> defines \<sigma>)"
+
+onto_class assoc_M_M_see_also =
+  see_also :: "(Mathematical_knowledge_object rel) set" 
+  invariant see_also_trans :: "\<forall> r \<in> (see_also \<sigma>). trans r"
+  invariant see_also_sym :: "\<forall> r \<in> (see_also \<sigma>). sym r"
+
+onto_class Problem = Mathematical_knowledge_object +
+  Annotations :: "annotation list"
+  
+onto_class Method = Mathematical_knowledge_object +
+  Annotations :: "annotation list"
+
+onto_class assoc_Problem_Method =
+  is_solved_by :: "(Problem \<times> Method) set"
+  invariant is_solved_by_defined :: "\<forall> x. x \<in> Domain (is_solved_by \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (is_solved_by \<sigma>). (x, y) \<in> is_solved_by \<sigma>)"
+
+onto_class assoc_Method_Problem =
+  solves :: "(Method \<times> Problem) set"
+  invariant solves_defined :: "\<forall> x. x \<in> Domain (solves \<sigma>)
+                                    \<longrightarrow> (\<exists> y \<in> Range (solves \<sigma>). (x, y) \<in> solves \<sigma>)"

src/tests/Ontology_Matching_Example.thy

@@ -9,44 +9,44 @@ text\<open>Using HOL, we can define a mapping between two ontologies.
   Here is an example which show how to map two classes.
   HOL also allows us to map the invariants (ontological rules) of the classes!\<close>
 
-type_synonym UTF8 = string
+type_synonym UTF8 = string        \<comment> \<open>for the sake of the demonstration\<close>
 
 definition utf8_to_string
-  where "utf8_to_string x = x"
+  where "utf8_to_string x = x"    \<comment> \<open>for the sake of the demonstration\<close>
 
 
 doc_class A =
-  first_name :: UTF8
-  last_name :: UTF8
-  age :: nat
-  married_to :: "string option"
+  first_name  :: UTF8
+  last_name   :: UTF8
+  age         :: nat
+  married_to  :: "string option"
   invariant a :: "age \<sigma> < 18 \<longrightarrow> married_to \<sigma> = None"
+
 doc_class B =
-  name :: string 
-  adult :: bool
-  is_married :: bool
+  name        :: string 
+  adult       :: bool
+  is_married  :: bool
   invariant b :: "is_married \<sigma> \<longrightarrow> adult \<sigma>"
 
-text\<open>We define the mapping between the two classes,
-  i.e. how to transform the class @{doc_class A} in to the class @{doc_class B}:\<close>
+text\<open>We define the mapping between the two classes,  i.e. how to transform 
+     the class @{doc_class A} in to the class @{doc_class B}:\<close>
 
-definition A_to_B_morphism
-  where "A_to_B_morphism X =
-        \<lparr> tag_attribute = A.tag_attribute X
-          , name = utf8_to_string (first_name X) @ '' ''  @ utf8_to_string (last_name X)
-          , adult = (age X \<ge> 18)
-          , is_married = (married_to X \<noteq> None) \<rparr>" 
+
+definition A_to_B_mapping :: "'a A_scheme \<Rightarrow> B" ("_ \<langle>B\<rangle>\<^sub>A" [1000]999)
+  where "\<sigma> \<langle>B\<rangle>\<^sub>A =
+        \<lparr> tag_attribute = A.tag_attribute \<sigma>
+          , name = utf8_to_string (first_name \<sigma>) @ '' ''  @ utf8_to_string (last_name \<sigma>)
+          , adult = (age \<sigma> \<ge> 18)
+          , is_married = (married_to \<sigma> \<noteq> None) \<rparr>" 
 
 text\<open>Now we check that the invariant is preserved through the morphism:\<close>
 
 lemma inv_a_preserved :
-  "a_inv X \<Longrightarrow> b_inv (A_to_B_morphism X)"
-  unfolding a_inv_def b_inv_def A_to_B_morphism_def
-  by auto
+  "a_inv \<sigma> \<Longrightarrow> b_inv (\<sigma> \<langle>B\<rangle>\<^sub>A)"
+  unfolding a_inv_def b_inv_def A_to_B_mapping_def  by auto
 
 lemma A_morphism_B_total :
-  "A_to_B_morphism ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
-  using inv_a_preserved
-  by auto
+  "A_to_B_mapping ` ({X::A. a_inv X}) \<subseteq> ({X::B. b_inv X})"
+  using inv_a_preserved by auto
 
 end