Compare commits
172 Commits
main
...
parametric
Author | SHA1 | Date |
---|---|---|
Nicolas Méric | 3d02461aa2 | |
Nicolas Méric | ee647d2822 | |
Nicolas Méric | 92b515730d | |
Nicolas Méric | fb55ed8ded | |
Nicolas Méric | 8b1b7736ee | |
Burkhart Wolff | fbf34f9a35 | |
Idir AIT SADOUNE | 1714703272 | |
Nicolas Méric | 7b0d446724 | |
Nicolas Méric | 0cc17a136e | |
Nicolas Méric | e69808750c | |
Nicolas Méric | d5b195d873 | |
Nicolas Méric | a5796277fd | |
Nicolas Méric | 4f5f4996af | |
Nicolas Méric | 763c0a515b | |
Idir AIT SADOUNE | a803d999c0 | |
Nicolas Méric | e4e8199e33 | |
Nicolas Méric | 7618f8b2c4 | |
Nicolas Méric | 30fc7a306f | |
Nicolas Méric | 3260ae3406 | |
Nicolas Méric | 108be68f19 | |
Nicolas Méric | 0ee58a65e6 | |
Nicolas Méric | f30ff6a967 | |
Nicolas Méric | b448b87395 | |
Nicolas Méric | 57c984d4dc | |
Nicolas Méric | 35b50e419f | |
Burkhart Wolff | 230336f0a4 | |
Burkhart Wolff | 8e056e0e8a | |
Nicolas Méric | 9770f8c332 | |
Nicolas Méric | 8aba7f272a | |
Nicolas Méric | 9b396b6096 | |
Burkhart Wolff | 53333d7096 | |
Burkhart Wolff | 624b0e4af1 | |
Burkhart Wolff | 301d4ac5c2 | |
Burkhart Wolff | 908827e0ea | |
Burkhart Wolff | 5e97dfb6fe | |
Burkhart Wolff | ee3428d384 | |
Burkhart Wolff | c9beb99b7a | |
Idir AIT SADOUNE | aa6d11f73c | |
Idir AIT SADOUNE | 681b8f828d | |
Burkhart Wolff | 6e928f5af6 | |
Burkhart Wolff | c11124966b | |
Burkhart Wolff | 818cb34a0b | |
Burkhart Wolff | c9e2f22c8b | |
Burkhart Wolff | d422e78849 | |
Burkhart Wolff | 346b28f732 | |
Burkhart Wolff | de1354625e | |
Burkhart Wolff | d0bedee42d | |
Nicolas Méric | 46841c4d1b | |
Burkhart Wolff | 081309b5cd | |
Burkhart Wolff | 8722b21c3d | |
Nicolas Méric | 26ddfe5b0c | |
Idir AIT SADOUNE | abeb2f7f5e | |
Idir AIT SADOUNE | acbaa582ef | |
Burkhart Wolff | 76cff5beab | |
Burkhart Wolff | 1c31a11bdc | |
Burkhart Wolff | 11ef56965f | |
Burkhart Wolff | ca418f60b0 | |
Burkhart Wolff | 6f4259cc2c | |
Nicolas Méric | 7201101a6c | |
Burkhart Wolff | 65e6240fa8 | |
Burkhart Wolff | 0496ce3080 | |
Burkhart Wolff | 4f6ac66167 | |
Burkhart Wolff | 74ba9aa892 | |
Nicolas Méric | d6468274d7 | |
Nicolas Méric | 1c550a962a | |
Nicolas Méric | 4a5523ac17 | |
Nicolas Méric | 7f02cbbde4 | |
Nicolas Méric | e125775350 | |
Nicolas Méric | 7bd1b61ddd | |
Nicolas Méric | b3fd073b38 | |
Nicolas Méric | 8f2e194501 | |
Nicolas Méric | 258fcc2f8e | |
Nicolas Méric | d95a5aa2a8 | |
Nicolas Méric | f96db62396 | |
Burkhart Wolff | 913bf49b3f | |
Burkhart Wolff | 51b3e74c36 | |
Burkhart Wolff | 6863995671 | |
Burkhart Wolff | 01c196086b | |
Burkhart Wolff | c2e39edd99 | |
Burkhart Wolff | 62c816781e | |
Nicolas Méric | 930630e368 | |
Nicolas Méric | f681ab54a7 | |
Nicolas Méric | b10cb9d54d | |
Nicolas Méric | eea88bccfd | |
Nicolas Méric | 2d33ad814c | |
Nicolas Méric | 9711b079a4 | |
Nicolas Méric | 12588fa6e9 | |
Nicolas Méric | 8b7162d104 | |
Burkhart Wolff | a4708957d5 | |
Burkhart Wolff | f1e01a5b86 | |
Burkhart Wolff | 27d90fc87e | |
Burkhart Wolff | f93e62d54b | |
Burkhart Wolff | 676edd7d54 | |
Burkhart Wolff | 7acd0af628 | |
Nicolas Méric | 4cfb33856b | |
Idir AIT SADOUNE | 31de87dfca | |
Nicolas Méric | f99be4d3a3 | |
Nicolas Méric | 00511848ed | |
Nicolas Méric | d96d6124ef | |
Nicolas Méric | 1a23140534 | |
Nicolas Méric | 4b05c9a9a1 | |
Nicolas Méric | 1fca5a37b7 | |
Nicolas Méric | e511049ba8 | |
Nicolas Méric | 4edcb1acd1 | |
Nicolas Méric | 8bfe06db9e | |
Idir AIT SADOUNE | 28fecba621 | |
Idir AIT SADOUNE | 9b9a4dcfb0 | |
Nicolas Méric | f2f6cfad98 | |
Nicolas Méric | 41e8c4975a | |
Idir AIT SADOUNE | ca21aa81f4 | |
Idir AIT SADOUNE | f674ca8ca3 | |
Idir AIT SADOUNE | 7cd7a4d15d | |
Idir AIT SADOUNE | b9c72124c0 | |
Burkhart Wolff | fe728ef9af | |
Burkhart Wolff | c2fa80953a | |
Burkhart Wolff | f180a87fbf | |
Burkhart Wolff | 3226fdf0c8 | |
Idir AIT SADOUNE | f35a7eb5bd | |
Nicolas Méric | 34a57b2c9f | |
Burkhart Wolff | 17c6e87b8d | |
Idir AIT SADOUNE | 861986a443 | |
Idir AIT SADOUNE | 57a32ce39d | |
Nicolas Méric | 9d3b701c27 | |
Idir AIT SADOUNE | 893e239ce5 | |
Idir AIT SADOUNE | d4f8ee344b | |
Nicolas Méric | 46450e951c | |
Nicolas Méric | 307bb4e3d4 | |
Nicolas Méric | 1051e2cd7b | |
Nicolas Méric | c914b201ee | |
Nicolas Méric | b2aac7288d | |
Nicolas Méric | 94baf69f25 | |
Nicolas Méric | 33d991a1c7 | |
Nicolas Méric | 36276fc3b4 | |
Nicolas Méric | 68417e01d3 | |
Nicolas Méric | 30793f5c51 | |
Nicolas Méric | 35a117a361 | |
Nicolas Méric | 09129bfbf8 | |
Idir AIT SADOUNE | 8663703d53 | |
Nicolas Méric | 2e645ed5ff | |
Burkhart Wolff | 092d552ef8 | |
Nicolas Méric | 927f0446a0 | |
Idir AIT SADOUNE | b0a29ac00d | |
Idir AIT SADOUNE | 4b43756eb3 | |
Idir AIT SADOUNE | 4936a8142e | |
Nicolas Méric | 7033335e3f | |
Nicolas Méric | a2f3057545 | |
Burkhart Wolff | e6721b548d | |
Burkhart Wolff | d319ab2555 | |
Nicolas Méric | 502f5c5cd2 | |
Nicolas Méric | 7ac669e52e | |
Nicolas Méric | d9f2d5c0c4 | |
Burkhart Wolff | ae96c7cef0 | |
Burkhart Wolff | 9d9fd03b72 | |
Burkhart Wolff | b243f30252 | |
Burkhart Wolff | 05b896291b | |
Burkhart Wolff | cc151291f6 | |
Burkhart Wolff | 3e06e659b6 | |
Burkhart Wolff | eaef236dcc | |
Burkhart Wolff | b35c774d27 | |
Burkhart Wolff | c5cdf5f826 | |
Nicolas Méric | a38d13198c | |
Idir AIT SADOUNE | f8c125bcff | |
Burkhart Wolff | 9cd021d7fa | |
Burkhart Wolff | 9d7fc957c6 | |
Burkhart Wolff | b1fb509d8b | |
Burkhart Wolff | 63145e0d3a | |
Burkhart Wolff | be0352cab7 | |
Nicolas Méric | 6d42f122b1 | |
Burkhart Wolff | e53984feea | |
Burkhart Wolff | d7c7a98138 | |
Idir AIT SADOUNE | 8629dda85e | |
Nicolas Méric | 688e823463 |
|
@ -12,3 +12,4 @@ session "mini_odo" = "Isabelle_DOF" +
|
|||
"figures/odometer.jpeg"
|
||||
"figures/three-phase-odo.pdf"
|
||||
"figures/wheel-df.png"
|
||||
"figures/CENELEC-Fig.3-docStructure.png"
|
After Width: | Height: | Size: 355 KiB |
|
@ -3,7 +3,6 @@ theory "paper"
|
|||
imports "Isabelle_DOF.scholarly_paper"
|
||||
begin
|
||||
|
||||
|
||||
open_monitor*[this::article]
|
||||
|
||||
declare[[ strict_monitor_checking = false]]
|
||||
|
@ -48,8 +47,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.
|
||||
|
|
|
@ -0,0 +1,24 @@
|
|||
session "2021-ITP-PMTI" = "Isabelle_DOF" +
|
||||
options [document = pdf, document_output = "output", document_build = dof]
|
||||
theories
|
||||
"paper"
|
||||
document_files
|
||||
"isadof.cfg"
|
||||
"root.bib"
|
||||
"preamble.tex"
|
||||
"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"
|
|
@ -0,0 +1,99 @@
|
|||
%% 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
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-COL}
|
||||
[<isadofltxversion>%
|
||||
Document-Type Support Framework for Isabelle.]
|
||||
|
||||
\RequirePackage{DOF-core}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: figure*
|
||||
\NewEnviron{isamarkupfigure*}[1][]{\isaDof[env={figure},#1]{\BODY}}
|
||||
\newisadof{figure.Isa_COL.figure}%
|
||||
[label=,type=%
|
||||
,Isa_COL.figure.relative_width=%
|
||||
,Isa_COL.figure.placement=%
|
||||
,Isa_COL.figure.src=%
|
||||
,Isa_COL.figure.spawn_columns=enum False True%
|
||||
][1]{%
|
||||
\begin{figure}[]
|
||||
\centering
|
||||
\ifcommandkey{Isa_COL.figure.relative_width}
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
|
||||
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}
|
||||
\caption{#1}\label{\commandkey{label}}%
|
||||
\end{figure}
|
||||
}
|
||||
% end: figure*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: side_by_side_figure*
|
||||
\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
|
||||
\newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
|
||||
[label=,type=%
|
||||
,Isa_COL.figure.relative_width=%
|
||||
,Isa_COL.figure.placement=%
|
||||
,Isa_COL.figure.src=%
|
||||
,Isa_COL.side_by_side_figure.anchor=%
|
||||
,Isa_COL.side_by_side_figure.caption=%
|
||||
,Isa_COL.side_by_side_figure.relative_width2=%
|
||||
,Isa_COL.side_by_side_figure.src2=%
|
||||
,Isa_COL.side_by_side_figure.anchor2=%
|
||||
,Isa_COL.side_by_side_figure.caption2=%
|
||||
,Isa_COL.side_by_side_figure.placement=%
|
||||
,Isa_COL.figure.spawn_columns=enum False True%
|
||||
][1]{%
|
||||
\begin{figure}[]
|
||||
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor}}\commandkey{Isa_COL.side_by_side_figure.caption}]%
|
||||
{\ifcommandkey{Isa_COL.figure.relative_width}%
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{Isa_COL.figure.relative_width}}
|
||||
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{Isa_COL.figure.src}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}%
|
||||
}%
|
||||
\hfill%
|
||||
\subfloat[\label{\commandkey{Isa_COL.side_by_side_figure.anchor2}}\commandkey{Isa_COL.side_by_side_figure.caption2}]%
|
||||
{\ifcommandkey{Isa_COL.side_by_side_figure.relative_width2}%
|
||||
{%
|
||||
\gdef\dof@width{\commandkey{Isa_COL.side_by_side_figure.relative_width2}}
|
||||
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
|
||||
\FPdiv\scale{\dof@width}{100}%
|
||||
\includegraphics[width=\scale\textwidth]{\dof@src}%
|
||||
}{%
|
||||
\gdef\dof@src{\commandkey{Isa_COL.side_by_side_figure.src2}}
|
||||
\includegraphics[]{\dof@src}%
|
||||
}%
|
||||
}%
|
||||
\caption{#1}\label{\commandkey{label}}%
|
||||
\end{figure}
|
||||
}
|
||||
% end: side_by_side_figure*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
@ -0,0 +1,26 @@
|
|||
%% Copyright (C) 2021 University of Exeter
|
||||
%% 2021 University of Paris-Saclay
|
||||
%%
|
||||
%% 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
|
||||
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-amssymb}
|
||||
[<isadofltxversion>%
|
||||
Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
|
||||
|
||||
\usepackage{ifxetex,ifluatex}
|
||||
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
|
||||
\usepackage{amssymb}
|
||||
\else % if luatex or xetex
|
||||
\usepackage{unicode-math}
|
||||
\usepackage{latexsym}
|
||||
\fi
|
|
@ -0,0 +1,160 @@
|
|||
%% 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
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-core}
|
||||
[<isadofltxversion>%
|
||||
Document-Type Support Framework for Isabelle.]
|
||||
|
||||
\RequirePackage{keycommand}
|
||||
\RequirePackage{environ}
|
||||
\RequirePackage{graphicx}
|
||||
\RequirePackage{xspace}
|
||||
\RequirePackage{etoolbox}
|
||||
\RequirePackage{fp}
|
||||
|
||||
\newcommand{\isabelleurl}{UNDEFINED}
|
||||
\newcommand{\dofurl}{UNDEFINED}
|
||||
\newcommand{\dof@isabelleversion}{UNDEFINED}
|
||||
\newcommand{\isabellefullversion}{UNDEFINED\xspace}
|
||||
\newcommand{\dof@version}{UNDEFINED}
|
||||
\newcommand{\dof@artifacturl}{UNDEFINED}
|
||||
\newcommand{\doflatestversion}{UNDEFINED}
|
||||
\newcommand{\isadoflatestdoi}{UNDEFINED}
|
||||
\newcommand{\isadofgenericdoi}{UNDEFINED}
|
||||
\newcommand{\isabellelatestversion}{Isabelle2019}
|
||||
|
||||
%%% CONFIG %%%
|
||||
|
||||
\newcommand{\isabelleversion}{\dof@isabelleversion\xspace}
|
||||
\newcommand{\dofversion}{\dof@version\xspace}
|
||||
\newcommand{\isadofversion}{\dofversion/\isabelleversion}
|
||||
\newcommand{\isadoflatestversion}{\doflatestversion/\isabellelatestversion}
|
||||
\newcommand{\isadofdir}{Isabelle_DOF-\dof@version_\dof@isabelleversion}
|
||||
\newcommand{\isadofdirn}{Isabelle\_DOF-\dof@version\_\dof@isabelleversion}
|
||||
\newcommand{\isadofarchive}{\isadofdir.tar.xz}
|
||||
\newcommand{\isadofarchiven}{\isadofdirn.tar.xz}
|
||||
\newcommand{\isadofarchiveurl}{\dof@artifacturl/\isadofarchive}
|
||||
|
||||
\newcommand{\isadof}{Isabelle/DOF\xspace}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: newcommand wrapper
|
||||
\newcommand\newisadof[1]{\expandafter\newkeycommand\csname isaDof.#1\endcsname}%
|
||||
\newcommand\renewisadof[1]{\expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
|
||||
\newcommand\provideisadof[1]{\expandafter\providekeycommand\csname isaDof.#1\endcsname}%
|
||||
% end: newcommand wrapper
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: generic dispatcher
|
||||
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
|
||||
\ifcsname isaDof.\commandkey{type}\endcsname%
|
||||
\csname isaDof.\commandkey{type}\endcsname%
|
||||
[label=\commandkey{label},\commandkey{args}]{#1}%
|
||||
\else\relax\fi%
|
||||
\ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
|
||||
\csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
|
||||
[label=\commandkey{label},\commandkey{args}]{#1}%
|
||||
\else%
|
||||
\message{Isabelle/DOF: Using default LaTeX representation for concept %
|
||||
"\commandkey{env}.\commandkey{type}".}%
|
||||
\ifcsname isaDof.\commandkey{env}\endcsname%
|
||||
\csname isaDof.\commandkey{env}\endcsname%
|
||||
[label=\commandkey{label}]{#1}%
|
||||
\else%
|
||||
\errmessage{Isabelle/DOF: No LaTeX representation for concept %
|
||||
"\commandkey{env}.\commandkey{type}" defined and no default %
|
||||
definition for "\commandkey{env}" available either.}%
|
||||
\fi%
|
||||
\fi%
|
||||
}
|
||||
% end: generic dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: text*-dispatcher
|
||||
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}}
|
||||
% end: text*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: chapter*-dispatcher
|
||||
\NewEnviron{isamarkupchapter*}[1][]{\isaDof[env={chapter},#1]{\BODY}}
|
||||
% end: chapter*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: section*-dispatcher
|
||||
\NewEnviron{isamarkupsection*}[1][]{\isaDof[env={section},#1]{\BODY}}
|
||||
% end: section*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: subsection*-dispatcher
|
||||
\NewEnviron{isamarkupsubsection*}[1][]{\isaDof[env={subsection},#1]{\BODY}}
|
||||
% end: subsection*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: subsubsection*-dispatcher
|
||||
\NewEnviron{isamarkupsubsubsection*}[1][]{\isaDof[env={subsubsection},#1]{\BODY}}
|
||||
% end: subsubsection*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: paragraph*-dispatcher
|
||||
\NewEnviron{isamarkupparagraph*}[1][]{\isaDof[env={paragraph},#1]{\BODY}}
|
||||
% end: paragraph*-dispatcher
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: text default implementation
|
||||
\newisadof{text}[label=,type=][1]{%
|
||||
\begin{isamarkuptext}\label{\commandkey{label}}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
% end: text default implementation
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: chapter/section default implementations
|
||||
\newisadof{chapter}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupchapter{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
\newisadof{section}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
\newisadof{subsection}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
\newisadof{subsubsection}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
\newisadof{paragraph}[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupparagraph{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
% end: chapter/section default implementations
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: label and ref
|
||||
\newisadof{label}[label=,type=][1]{\label{#1}}
|
||||
\newisadof{ref}[label=,type=][1]{\autoref{#1}}
|
||||
\newisadof{macroDef}[label=,type=][1]{MMM \label{#1}} %% place_holder
|
||||
\newisadof{macroExp}[label=,type=][1]{MMM \autoref{#1}} %% place_holder
|
||||
% end: label and ref
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
@ -0,0 +1,499 @@
|
|||
%% 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
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-scholarly_paper}
|
||||
[2021/03/22 Unreleased/Isabelle2021%
|
||||
Document-Type Support Framework for Isabelle (LNCS).]
|
||||
|
||||
\RequirePackage{DOF-COL}
|
||||
\RequirePackage{ifthen}
|
||||
|
||||
\RequirePackage{ifthen}
|
||||
\newboolean{DOF@scholarlypaper@force}
|
||||
\DeclareOption{force}{\setboolean{DOF@scholarlypaper@force}{true}}
|
||||
|
||||
\ProcessOptions\relax
|
||||
|
||||
\ifthenelse{\boolean{DOF@scholarlypaper@force}}{%
|
||||
}{%
|
||||
\@ifclassloaded{llncs}%
|
||||
{}%
|
||||
{%
|
||||
\@ifclassloaded{scrartcl}%
|
||||
{%
|
||||
\newcommand{\institute}[1]{}%
|
||||
\newcommand{\inst}[1]{}%
|
||||
\newcommand{\orcidID}[1]{}%
|
||||
\newcommand{\email}[1]{}%
|
||||
\RequirePackage{DOF-scholarly_paper-thm}%
|
||||
}%
|
||||
{%
|
||||
\@ifclassloaded{lipics-v2021}%
|
||||
{%
|
||||
\newcommand{\institute}[1]{}%
|
||||
\newcommand{\inst}[1]{}%
|
||||
\newcommand{\orcidID}[1]{}%
|
||||
\newcommand{\email}[1]{}%
|
||||
}%
|
||||
{%
|
||||
{%
|
||||
\@ifclassloaded{eptcs}%
|
||||
{%
|
||||
\newcommand{\inst}[1]{}%
|
||||
\newcommand{\orcidID}[1]{}%
|
||||
}%
|
||||
{%
|
||||
\@ifclassloaded{svjour3}%
|
||||
{%
|
||||
\newcommand{\inst}[1]{}%
|
||||
}%
|
||||
{%
|
||||
\PackageError{DOF-scholarly_paper}
|
||||
{Scholarly Paper only supports LNCS or scrartcl as document class.}
|
||||
{}\stop%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}
|
||||
}
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: title*
|
||||
\NewEnviron{isamarkuptitle*}[1][]{\isaDof[env={title},#1]{\BODY}}
|
||||
\newisadof{title.scholarly_paper.title}%
|
||||
[label=,type=%
|
||||
,scholarly_paper.title.short_title=%
|
||||
][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
||||
}
|
||||
% end: title*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: subtitle*
|
||||
\NewEnviron{isamarkupsubtitle*}[1][]{\isaDof[env={subtitle},#1]{\BODY}}
|
||||
\newisadof{subtitle.scholarly_paper.subtitle}%
|
||||
[label=,type=%
|
||||
,scholarly_paper.subtitle.abbrev=%
|
||||
][1]{%
|
||||
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
|
||||
}
|
||||
% end: subtitle*
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: scholarly_paper.author
|
||||
\def\dof@author{}%
|
||||
\def\dof@affiliation{}%
|
||||
|
||||
\newcommand{\DOFauthor}{\author{\dof@author}}
|
||||
\newcommand{\DOFinstitute}{\institute{\dof@affiliation}}
|
||||
|
||||
\AtBeginDocument{%
|
||||
\DOFauthor
|
||||
\DOFinstitute
|
||||
}
|
||||
|
||||
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
|
||||
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
|
||||
|
||||
\newcounter{dof@cnt@author}
|
||||
\newcommand{\addauthor}[1]{%
|
||||
\ifthenelse{\equal{\dof@author}{}}{%
|
||||
\gdef\dof@author{#1}%
|
||||
}{%
|
||||
\leftadd\dof@author{\protect\and #1}%
|
||||
}
|
||||
}
|
||||
|
||||
\newcommand{\addaffiliation}[1]{%
|
||||
\ifthenelse{\equal{\dof@affiliation}{}}{%
|
||||
\gdef\dof@affiliation{#1}%
|
||||
}{%
|
||||
\leftadd\dof@affiliation{\protect\and #1}%
|
||||
}
|
||||
}
|
||||
|
||||
\NewEnviron{isamarkupauthor*}[1][]{\isaDof[env={text},#1]{\BODY}}
|
||||
\provideisadof{text.scholarly_paper.author}%
|
||||
[label=,type=%
|
||||
,scholarly_paper.author.email=%
|
||||
,scholarly_paper.author.affiliation=%
|
||||
,scholarly_paper.author.orcid=%
|
||||
,scholarly_paper.author.http_site=%
|
||||
][1]{%
|
||||
\stepcounter{dof@cnt@author}
|
||||
\def\dof@a{\commandkey{scholarly_paper.author.affiliation}}
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.author.orcid}}{}}{%
|
||||
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}}}%
|
||||
}{%
|
||||
\protected@write\@auxout{}{\string\addauthor{#1\string\inst{\thedof@cnt@author}\string\orcidID{\commandkey{scholarly_paper.author.orcid}}}}%
|
||||
}
|
||||
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{scholarly_paper.author.email}}}}%
|
||||
}
|
||||
% end: scholarly_paper.author
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% begin: scholarly_paper.abstract
|
||||
\providecommand{\keywords}[1]{\mbox{}\\[2ex]\mbox{}\noindent{\textbf{Keywords:}} #1}
|
||||
\NewEnviron{isamarkupabstract*}[1][]{\isaDof[env={text.scholarly_paper.abstract},#1]{\BODY}}
|
||||
\newisadof{text.scholarly_paper.abstract}%
|
||||
[label=,type=%
|
||||
,scholarly_paper.abstract.keywordlist=%
|
||||
][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
\begin{abstract}%
|
||||
#1%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.abstract.keywordlist}}{}}{}{%
|
||||
\keywords{\commandkey{scholarly_paper.abstract.keywordlist}}%
|
||||
}%
|
||||
\end{abstract}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\newtheorem{axiom}{Axiom}
|
||||
\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
|
||||
\newtheorem{assertion}{Assertion}
|
||||
|
||||
% \newcommand{\formalMathStmt[label, mcc, ]
|
||||
% end: scholarly_paper.abstract
|
||||
% | "rule" | "assn" | "expl" | rem | "notation" | "terminology"
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newisadof{text.scholarly_paper.math_content}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name ={} % {} or \relax
|
||||
, scholarly_paper.math_content.mcc = % "def" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn"
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
|
||||
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{definition}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{axiom} \label{\commandkey{label}} #1 \end{axiom} }
|
||||
{\begin{axiom} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{axiom}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
|
||||
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{theorem}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
|
||||
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{lemma}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
|
||||
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{example}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{cor}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{corrollary} \label{\commandkey{label}} #1 \end{corrollary} }
|
||||
{\begin{corrollary} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{corrollary}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prop}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{property} \label{\commandkey{label}} #1 \end{property} }
|
||||
{\begin{property} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{property}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rule}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
|
||||
{\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{ruleX}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rem}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{remark} \label{\commandkey{label}} #1 \end{remark} }
|
||||
{\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{remark}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
|
||||
{\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{assertion}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notation}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
|
||||
{\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{notation}}
|
||||
}%
|
||||
}%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{terminology}}
|
||||
{%
|
||||
{\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
|
||||
{\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{terminology}}
|
||||
}%
|
||||
}%
|
||||
{%
|
||||
\typeout{Internal error: enumeration out of sync with ontology scholarly-paper.}
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
|
||||
|
||||
% end: scholarly_paper.math_content
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% Besser: Einfach durchreichen wg Vererbung !
|
||||
\newisadof{text.scholarly_paper.math_example}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name =%
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
|
||||
{\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
|
||||
\label{\commandkey{label}} #1
|
||||
\end{example}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
|
||||
\newisadof{text.scholarly_paper.definition}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name =%
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
|
||||
{\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
% An experiment in inheritance of the default behaviour.
|
||||
% \newisadof{text.scholarly_paper.definition}%
|
||||
% [label=,type=%
|
||||
% , scholarly_paper.math_content.short_name =%
|
||||
% , scholarly_paper.math_content.mcc =%
|
||||
% , Isa_COL.text_element.level =%
|
||||
% , Isa_COL.text_element.referentiable =%
|
||||
% , Isa_COL.text_element.variants =%
|
||||
% , scholarly_paper.text_section.main_author =%
|
||||
% , scholarly_paper.text_section.fixme_list =%
|
||||
% , scholarly_paper.technical.definition_list =%
|
||||
% , scholarly_paper.technical.status =%
|
||||
% ]
|
||||
% [1]
|
||||
% {%
|
||||
% \cscommand{text.scholarly_paper.math_content}%
|
||||
% [label=\commandkey{label},type=\commandkey{type}%
|
||||
% , scholarly_paper.math_content.short_name =\commandkey{scholarly_paper.math_content.short_name}%
|
||||
% , scholarly_paper.math_content.mcc =\commandkey{scholarly_paper.math_content.mcc}%
|
||||
% , Isa_COL.text_element.level =\commandkey{Isa_COL.text_element.level}%
|
||||
% , Isa_COL.text_element.referentiable =\commandkey{Isa_COL.text_element.referentiable}%
|
||||
% , Isa_COL.text_element.variants =\commandkey{Isa_COL.text_element.variants}%
|
||||
% , scholarly_paper.text_section.main_author =\commandkey{scholarly_paper.text_section.main_author}%
|
||||
% , scholarly_paper.text_section.fixme_list =\commandkey{scholarly_paper.text_section.fixme_list}%
|
||||
% , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
|
||||
% , scholarly_paper.technical.status =\commandkey{scholarly_paper.technical.status}%
|
||||
% ]
|
||||
% {#1}%
|
||||
% }
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%% Besser: Einfach durchreichen wg Vererbung !
|
||||
\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
|
||||
\newisadof{text.scholarly_paper.lemma}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name =%
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
|
||||
{\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% Besser: Einfach durchreichen wg Vererbung !
|
||||
\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
|
||||
\newisadof{text.scholarly_paper.theorem}%
|
||||
[label=,type=%
|
||||
, scholarly_paper.math_content.short_name =%
|
||||
, scholarly_paper.math_content.mcc =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, Isa_COL.text_element.level =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.technical.status =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
|
||||
{\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
|
||||
{\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
|
||||
}{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
% Generic Example. Different inheritance hierachy.
|
||||
\newisadof{text.scholarly_paper.example}%
|
||||
[label=,type=%
|
||||
, Isa_COL.text_element.level =%
|
||||
, Isa_COL.text_element.referentiable =%
|
||||
, Isa_COL.text_element.variants =%
|
||||
, scholarly_paper.text_section.main_author =%
|
||||
, scholarly_paper.text_section.fixme_list =%
|
||||
, scholarly_paper.technical.definition_list =%
|
||||
, scholarly_paper.example.status =%
|
||||
, scholarly_paper.example.short_name =%
|
||||
]
|
||||
[1]
|
||||
{%
|
||||
\begin{isamarkuptext}%
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
|
||||
\ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }
|
||||
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
|
||||
{\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
|
||||
\label{\commandkey{label}} #1 %
|
||||
\end{example}} %
|
||||
}%
|
||||
{%
|
||||
#1%
|
||||
}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
|
||||
%% Miscellaneous
|
||||
\usepackage{xspace}
|
||||
\newcommand{\ie}{i.\,e.\xspace}
|
||||
\newcommand{\eg}{e.\,g.\xspace}
|
||||
\newcommand{\etc}{etc}
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
\usepackage{DOF-core}
|
||||
\usepackage{DOF-scholarly_paper}
|
|
@ -0,0 +1,146 @@
|
|||
\begin{thebibliography}{10}
|
||||
\providecommand{\url}[1]{\texttt{#1}}
|
||||
\providecommand{\urlprefix}{URL }
|
||||
\providecommand{\doi}[1]{https://doi.org/#1}
|
||||
|
||||
\bibitem{AehligHN12}
|
||||
Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of
|
||||
normalisation by evaluation. J. Funct. Program. \textbf{22}(1), 9--30
|
||||
(2012). \doi{10.1017/S0956796812000019}
|
||||
|
||||
\bibitem{BGPP95}
|
||||
Ameur, Y.A., Besnard, F., Girard, P., Pierra, G., Potier, J.: Formal
|
||||
specification and metaprogramming in the {EXPRESS} language. In: SEKE'95, Proceedings. pp.
|
||||
181--188. Knowledge Systems Institute (1995)
|
||||
|
||||
\bibitem{10.1007/978-3-540-76298-0_52}
|
||||
Auer, S., Bizer, C., Kobilarov, G., Lehmann, J., Cyganiak, R., Ives, Z.:
|
||||
{DB}pedia: A nucleus for a web of open data. In: The Semantic Web.
|
||||
pp. 722--735. Springer, Berlin, Heidelberg (2007)
|
||||
|
||||
\bibitem{brucker.ea:isabelle-ontologies:2018}
|
||||
Brucker, A.D., Ait-Sadoune, I., Crisafulli, P., Wolff, B.: Using the {Isabelle}
|
||||
ontology framework: Linking the formal with the informal.
|
||||
In: CICM. No. 11006 in LNCS, Springer-Verlag, Heidelberg (2018).
|
||||
\doi{10.1007/978-3-319-96812-4_3}
|
||||
|
||||
\bibitem{brucker.ea:upf-firewall:2017}
|
||||
Brucker, A.D., Br{\"u}gger, L., Wolff, B.: Formal network models and their
|
||||
application to firewall policies. AFP (Jan 2017),
|
||||
\url{http://www.isa-afp.org/entries/UPF_Firewall.shtml}
|
||||
|
||||
\bibitem{brucker.ea:afp-core-dom:2018}
|
||||
Brucker, A.D., Herzberg, M.: The {Core} {DOM}. AFP (Dec
|
||||
2018),
|
||||
\url{http://www.isa-afp.org/entries/Core_DOM.html}
|
||||
|
||||
\bibitem{brucker.ea:featherweight:2014}
|
||||
Brucker, A.D., Tuong, F., Wolff, B.: {Featherweight} {OCL}: A proposal for a
|
||||
machine-checked formal semantics for {OCL} 2.5. AFP (Jan 2014),
|
||||
\url{http://www.isa-afp.org/entries/Featherweight_OCL.shtml}
|
||||
|
||||
\bibitem{brucker.ea:isabelledof:2019}
|
||||
Brucker, A.D., Wolff, B.: {Isabelle/DOF}: Design and implementation. In:
|
||||
SEFM. No. 11724 in LNCS,
|
||||
Springer-Verlag, Heidelberg (2019). \doi{10.1007/978-3-030-30446-1_15}
|
||||
|
||||
\bibitem{DBLP:conf-ifm-BruckerW19}
|
||||
Brucker, A.D., Wolff, B.: Using ontologies in formal developments targeting
|
||||
certification. In: {IFM} 2019, Proceedings. LNCS, vol. 11918, pp.
|
||||
65--82. Springer (2019). \doi{10.1007/978-3-030-34968-4_4}
|
||||
|
||||
\bibitem{bsi:50128:2014}
|
||||
Bs en 50128:2011: Railway applications -- communication, signalling and
|
||||
processing systems -- software for railway control and protecting systems.
|
||||
Standard, Britisch Standards Institute (BSI) (Apr 2014)
|
||||
|
||||
\bibitem{books/daglib/0032976}
|
||||
Euzenat, J., Shvaiko, P.: Ontology Matching, Second Edition. Springer (2013).
|
||||
\doi{10.1007/978-3-642-38721-0}
|
||||
|
||||
\bibitem{atl}
|
||||
{Eclipse Foundation}: Atl - a model transformation technology,
|
||||
\url{https://www.eclipse.org/atl/}, {A}ccessed: 2022-03-15
|
||||
|
||||
\bibitem{FotsoFLM18}
|
||||
Fotso, S.J.T., Frappier, M., Laleau, R., Mammar, A.: Modeling the hybrid
|
||||
{ERTMS/ETCS} level 3 standard using a formal requirements engineering
|
||||
approach. In: Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th
|
||||
International Conference, {ABZ}, Southampton, UK. LLNCS, vol. 10817, pp.
|
||||
262--276. Springer (2018). \doi{10.1007/978-3-319-91271-4_18}
|
||||
|
||||
\bibitem{HaftmannN10}
|
||||
Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In:
|
||||
{FLOPS} 2010, Proceedings. LNCS, vol.~6009, pp. 103--117.
|
||||
Springer (2010). \doi{10.1007/978-3-642-12251-4_9}
|
||||
|
||||
\bibitem{SPARCv8-AFP}
|
||||
Hou, Z., Sanan, D., Tiu, A., Liu, Y.: A formal model for the sparcv8 isa and a
|
||||
proof of non-interference for the leon3 processor. AFP
|
||||
(Oct 2016), \url{http://isa-afp.org/entries/SPARCv8.html}
|
||||
|
||||
\bibitem{CakeML-AFP}
|
||||
Hupel, L., Zhang, Y.: Cakeml. AFP (Mar 2018),
|
||||
\url{http://isa-afp.org/entries/CakeML.html}
|
||||
|
||||
\bibitem{klein.ea:comprehensive:2014}
|
||||
Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski,
|
||||
R., Heiser, G.: Comprehensive formal verification of an {OS} microkernel.
|
||||
{ACM} Trans. Comput. Syst. \textbf{32}(1), 2:1--2:70 (2014).
|
||||
\doi{10.1145/2560537}
|
||||
|
||||
\bibitem{KohlhaseR21}
|
||||
Kohlhase, M., Rabe, F.: Experiences from exporting major proof assistant
|
||||
libraries. J. Autom. Reason. \textbf{65}(8), 1265--1298 (2021).
|
||||
\doi{10.1007/s10817-021-09604-0}
|
||||
|
||||
\bibitem{AFP-ref22}
|
||||
{M.Eberl and G. Klein and A. Lochbihler and T. Nipkow and L. Paulson and R.
|
||||
Thiemann (eds)}: Archive of Formal Proofs. \url{https://afp-isa.org}
|
||||
(2022), {A}ccessed: 2022-03-15
|
||||
|
||||
\bibitem{MendilASMP21}
|
||||
Mendil, I., A{\"{\i}}t-Ameur, Y., Singh, N.K., M{\'{e}}ry, D., Palanque, P.A.:
|
||||
Standard conformance-by-construction with event-b. In: {FMICS}.
|
||||
LNCS, vol. 12863, pp. 126--146. Springer (2021).
|
||||
\doi{10.1007/978-3-030-85248-1_8}
|
||||
|
||||
\bibitem{protege}
|
||||
Musen, M.A.: The prot\'{e}g\'{e} project: A look back and a look forward. AI
|
||||
Matters \textbf{1}(4), 4–12 (jun 2015). \doi{10.1145/2757001.2757003}
|
||||
|
||||
\bibitem{Nevzorova2014OntoMathPO}
|
||||
Nevzorova, O., Zhiltsov, N., Kirillovich, A., Lipachev, E.K.:
|
||||
Onto{Ma}th\textsuperscript{PRO} ontology: {A} linked data hub for
|
||||
mathematics. ArXiv \textbf{abs/1407.4833} (2014).
|
||||
\doi{10.1007/978-3-319-11716-4_9}
|
||||
|
||||
\bibitem{Splay_Tree-AFP}
|
||||
Nipkow, T.: Splay tree. AFP (Aug 2014),
|
||||
\url{http://isa-afp.org/entries/Splay_Tree.html}
|
||||
|
||||
\bibitem{10.1007/978-3-030-79876-5_6}
|
||||
Nipkow, T., Ro{\ss}kopf, S.: Isabelle's metalogic: Formalization and proof
|
||||
checker. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction -- CADE
|
||||
28. pp. 93--110. Springer International Publishing, Cham (2021)
|
||||
|
||||
\bibitem{OWL2014}
|
||||
Sengupta, K., Hitzler, P.: Web ontology language {(OWL)}. In: Encyclopedia of
|
||||
Social Network Analysis and Mining, pp. 2374--2378 (2014).
|
||||
\doi{10.1007/978-1-4614-6170-8_113}
|
||||
|
||||
\bibitem{Security_Protocol_Refinement-AFP}
|
||||
Sprenger, C., Somaini, I.: Developing security protocols by refinement. AFP (May 2017),
|
||||
\url{http://isa-afp.org/entries/Security_Protocol_Refinement.html}
|
||||
|
||||
\bibitem{verbeek.ea:formal:2014}
|
||||
Verbeek, F., Tverdyshev, S., Havle, O., Blasum, H., Langenstein, B., Stephan,
|
||||
W., Nemouchi, Y., Feliachi, A., Wolff, B., Schmaltz, J.: Formal specification
|
||||
of a generic separation kernel. AFP (Jul 2014),
|
||||
\url{http://isa-afp.org/entries/CISC-Kernel.html}
|
||||
|
||||
\bibitem{wenzel:isabelle-isar:2020}
|
||||
Wenzel, M.: The Isabelle/Isar Reference Manual (2020), part of the Isabelle
|
||||
distribution.
|
||||
|
||||
\end{thebibliography}
|
|
@ -0,0 +1,113 @@
|
|||
%% Copyright (c) 2019 University of Exeter
|
||||
%% 2018-2019 University of Paris-Saclay
|
||||
%% 2018-2019 The University of Sheffield
|
||||
%%
|
||||
%% 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
|
||||
|
||||
%% <isadofltxversion>
|
||||
|
||||
%% Warning: Do Not Edit!
|
||||
%% =====================
|
||||
%% This is the root file for the Isabelle/DOF using the lncs class.
|
||||
%%
|
||||
%% All customization and/or additional packages should be added to the file
|
||||
%% preamble.tex.
|
||||
|
||||
\RequirePackage{ifvtex}
|
||||
\documentclass{llncs}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[USenglish]{babel}
|
||||
\usepackage{isabelle}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{isabellesym}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{DOF-amssymb}
|
||||
\IfFileExists{DOF-core.sty}{}{%
|
||||
\PackageError{DOF-core}{Isabelle/DOF not installed.
|
||||
This is a Isabelle_DOF project. The document preparation requires
|
||||
the Isabelle_DOF component from:
|
||||
<isadofurl>
|
||||
}{For further help, see <isadofurl>}
|
||||
}
|
||||
\input{ontologies}
|
||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||
\usepackage{graphicx}
|
||||
\usepackage{hyperref}
|
||||
\setcounter{tocdepth}{3}
|
||||
\hypersetup{%
|
||||
bookmarksdepth=3
|
||||
,pdfpagelabels
|
||||
,pageanchor=true
|
||||
,bookmarksnumbered
|
||||
,plainpages=false
|
||||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\renewcommand{\topfraction}{0.9} % max fraction of floats at top
|
||||
\renewcommand{\bottomfraction}{0.8} % max fraction of floats at bottom
|
||||
\setcounter{topnumber}{2}
|
||||
\setcounter{bottomnumber}{2}
|
||||
\setcounter{totalnumber}{4} % 2 may work better
|
||||
\setcounter{dbltopnumber}{2} % for 2-column pages
|
||||
\renewcommand{\dbltopfraction}{0.9} % fit big float above 2-col. text
|
||||
\renewcommand{\textfraction}{0.07} % allow minimal text w. figs
|
||||
\renewcommand{\floatpagefraction}{0.7} % require fuller float pages
|
||||
\renewcommand{\dblfloatpagefraction}{0.7} % require fuller float pages
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
|
||||
%%% etc. should not be used (they are deprecated since more than a
|
||||
%%% decade)
|
||||
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
|
||||
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
|
||||
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
|
||||
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
|
||||
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\begin{document}
|
||||
\selectlanguage{USenglish}%
|
||||
\renewcommand{\bibname}{References}%
|
||||
\renewcommand{\figurename}{Fig.}
|
||||
\renewcommand{\abstractname}{Abstract.}
|
||||
\renewcommand{\subsubsectionautorefname}{Sect.}
|
||||
\renewcommand{\subsectionautorefname}{Sect.}
|
||||
\renewcommand{\sectionautorefname}{Sect.}
|
||||
\renewcommand{\figureautorefname}{Fig.}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\newcommand{\lstnumberautorefname}{Line}
|
||||
|
||||
|
||||
|
||||
\maketitle
|
||||
\input{session}
|
||||
% optional bibliography
|
||||
\IfFileExists{root.bib}{%
|
||||
{\small
|
||||
\newcommand{\urlprefix}{}
|
||||
|
||||
\bibliographystyle{splncs04}
|
||||
|
||||
\bibliography{root}
|
||||
}}{}
|
||||
\end{document}
|
||||
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: t
|
||||
%%% End:
|
After Width: | Height: | Size: 101 KiB |
After Width: | Height: | Size: 85 KiB |
After Width: | Height: | Size: 15 KiB |
After Width: | Height: | Size: 18 KiB |
After Width: | Height: | Size: 214 KiB |
After Width: | Height: | Size: 27 KiB |
After Width: | Height: | Size: 256 KiB |
After Width: | Height: | Size: 19 KiB |
After Width: | Height: | Size: 17 KiB |
After Width: | Height: | Size: 1.4 MiB |
After Width: | Height: | Size: 9.6 KiB |
After Width: | Height: | Size: 9.7 KiB |
After Width: | Height: | Size: 9.1 KiB |
After Width: | Height: | Size: 8.4 KiB |
After Width: | Height: | Size: 8.5 KiB |
After Width: | Height: | Size: 24 KiB |
|
@ -0,0 +1,2 @@
|
|||
Template: lncs
|
||||
Ontology: scholarly_paper
|
|
@ -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]}
|
|
@ -0,0 +1,45 @@
|
|||
%% 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>}
|
||||
%\author{First Author\inst{1}\orcidID{0000-1111-2222-3333}}
|
||||
%\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
|
||||
%Second Author\inst{2,3}\orcidID{1111-2222-3333-4444}}
|
||||
%\institute{Inst1}
|
||||
%\institute{ Inst1 \and Inst2 \and Inst3}
|
||||
\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}
|
|
@ -1195,6 +1195,11 @@ fun create_default_object thy class_name =
|
|||
fun attr_to_free (binding, typ, _) = Free (purified_class_name ^ "_"
|
||||
^ (Binding.name_of binding)
|
||||
^ "_Attribute_Not_Initialized", typ)
|
||||
fun init_tag_attr (binding, typ, _) = HOLogic.mk_string (purified_class_name ^ "_"
|
||||
^ (Binding.name_of binding))
|
||||
val id = serial ()
|
||||
fun init_tag_attr (binding, typ, _) = Syntax.read_term_global thy
|
||||
((LargeInt.toString id) ^ "::int")
|
||||
val class_list' = DOF_core.get_attributes class_name thy
|
||||
fun attrs_filter [] = []
|
||||
| attrs_filter (x::xs) =
|
||||
|
@ -1209,10 +1214,10 @@ fun create_default_object thy class_name =
|
|||
val class_list'' = rev (attrs_filter (rev class_list'))
|
||||
fun add_tag_to_attrs_free tag_attr thy (cid, filtered_attr_list) =
|
||||
if DOF_core.is_virtual cid thy
|
||||
then (attr_to_free tag_attr)::(map (attr_to_free) filtered_attr_list)
|
||||
then (init_tag_attr tag_attr)::(map (attr_to_free) filtered_attr_list)
|
||||
else (map (attr_to_free) filtered_attr_list)
|
||||
val class_list''' = flat (map (add_tag_to_attrs_free DOF_core.tag_attr thy) class_list'')
|
||||
in list_comb (make_const, (attr_to_free DOF_core.tag_attr)::class_list''') end
|
||||
in list_comb (make_const, (init_tag_attr DOF_core.tag_attr)::class_list''') end
|
||||
|
||||
fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy =
|
||||
let
|
||||
|
@ -1449,7 +1454,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
thy cid_long assns' defaults
|
||||
val (value_term', _(*ty*), _) = calc_update_term {mk_elaboration=true}
|
||||
thy cid_long assns' defaults
|
||||
in (input_term, value_term') end
|
||||
in (input_term, Value_Command.value (Proof_Context.init_global thy) value_term') end
|
||||
val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor)
|
||||
o Context.Theory
|
||||
|
||||
|
@ -2025,7 +2030,7 @@ fun print_doc_items b ctxt =
|
|||
ctxt (Value_Command.value_without_elaboration ctxt input_term)));
|
||||
writeln (" value: "
|
||||
^ (Syntax.string_of_term
|
||||
ctxt (Value_Command.value_without_elaboration ctxt value)))
|
||||
ctxt (value)))
|
||||
)
|
||||
| print_item (n, NONE) =
|
||||
(writeln ("forward reference for docitem: "^n));
|
||||
|
@ -2412,6 +2417,10 @@ val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \<times> stri
|
|||
|
||||
fun def_cmd (decl, spec, prems, params) lthy =
|
||||
let
|
||||
val _ = writeln("In def_cmd decl: " ^ @{make_string} decl)
|
||||
val _ = writeln("In def_cmd spec: " ^ @{make_string} spec)
|
||||
val _ = writeln("In def_cmd prems: " ^ @{make_string} prems)
|
||||
val _ = writeln("In def_cmd params: " ^ @{make_string} params)
|
||||
val ((lhs as Free (x, T), _), lthy') = Specification.definition decl params prems spec lthy;
|
||||
val lhs' = Morphism.term (Local_Theory.target_morphism lthy') lhs;
|
||||
val _ =
|
||||
|
@ -2425,38 +2434,87 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
|
|||
fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) =
|
||||
let val bdg = Binding.suffix_name cond_suffix binding
|
||||
val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond)
|
||||
val _ = writeln("In define_cond eg: "
|
||||
^ Syntax.string_of_term ctxt eq)
|
||||
val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
|
||||
val _ = writeln("DDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD")
|
||||
in def_cmd args ctxt end
|
||||
|
||||
fun define_inv cid_long ((lbl, pos), inv) thy =
|
||||
let val bdg = Binding.make (lbl,pos)
|
||||
val inv_term = Syntax.read_term (Proof_Context.init_global thy) inv
|
||||
fun update_attribute_type thy class_scheme_ty
|
||||
val _ = writeln("In define_inv inv_term: "
|
||||
^ Syntax.string_of_term (Proof_Context.init_global thy) inv_term)
|
||||
val _ = writeln("In define_inv inv_term: "
|
||||
^ @{make_string} inv_term)
|
||||
val inv_term_test = DOF_core.transduce_term_global {mk_elaboration=true} (inv_term, pos) thy
|
||||
val _ = writeln("In define_inv inv_term_test: "
|
||||
^ Syntax.string_of_term (Proof_Context.init_global thy) inv_term_test)
|
||||
val _ = writeln("In define_inv inv_term_test: "
|
||||
^ @{make_string} inv_term_test)
|
||||
(*val inv_term_test' = Value_Command.value (Proof_Context.init_global thy) inv_term_test
|
||||
val _ = writeln("In define_inv inv_term_test': "
|
||||
^ Syntax.string_of_term (Proof_Context.init_global thy) inv_term_test')
|
||||
val _ = writeln("In define_inv inv_term_test': "
|
||||
^ @{make_string} inv_term_test')*)
|
||||
val _ = writeln("AAAAAAAAAAAAAAAAAAAAAAAAAAAAA")
|
||||
fun update_attribute_type thy cid_long class_scheme_ty
|
||||
(Const (s, Type (st,[ty, ty'])) $ t) =
|
||||
let
|
||||
val cid = Long_Name.qualifier s
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => Const (s, Type(st,[ty, ty']))
|
||||
$ (update_attribute_type thy class_scheme_ty t)
|
||||
| SOME _ => Const(s, Type(st,[class_scheme_ty, ty']))
|
||||
$ (update_attribute_type thy class_scheme_ty t)
|
||||
$ (update_attribute_type thy cid_long class_scheme_ty t)
|
||||
| SOME _ => Const(s, Type(st,[class_scheme_ty, ty']))
|
||||
$ (update_attribute_type thy cid_long class_scheme_ty t)
|
||||
end
|
||||
| update_attribute_type thy class_scheme_ty (t $ t') =
|
||||
(update_attribute_type thy class_scheme_ty t)
|
||||
$ (update_attribute_type thy class_scheme_ty t')
|
||||
| update_attribute_type thy class_scheme_ty (Abs(s, ty, t)) =
|
||||
Abs(s, ty, update_attribute_type thy class_scheme_ty t)
|
||||
| update_attribute_type _ class_scheme_ty (Free(s, ty)) = if s = invariantN
|
||||
| update_attribute_type thy cid_long class_scheme_ty (t $ t') =
|
||||
(update_attribute_type thy cid_long class_scheme_ty t)
|
||||
$ (update_attribute_type thy cid_long class_scheme_ty t')
|
||||
| update_attribute_type thy cid_long class_scheme_ty (Abs(s, ty, t)) =
|
||||
Abs(s, ty, update_attribute_type thy cid_long class_scheme_ty t)
|
||||
| update_attribute_type _ cid_long class_scheme_ty (Free(s, ty)) = if s = invariantN
|
||||
then Free (s, class_scheme_ty)
|
||||
else Free (s, ty)
|
||||
| update_attribute_type _ _ t = t
|
||||
| update_attribute_type _ cid_long _ t = t
|
||||
fun update_attribute_type' thy cid_long class_scheme_ty
|
||||
(Const (s, Type (st,[ty, ty'])) $ t) =
|
||||
let
|
||||
val cid = Long_Name.qualifier s
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
NONE => Const (s, Type(st,[ty, ty']))
|
||||
$ (update_attribute_type' thy cid_long class_scheme_ty t)
|
||||
| SOME _ => if DOF_core.is_subclass_global thy cid_long cid then
|
||||
Const(s, Type(st,[class_scheme_ty, ty']))
|
||||
$ (update_attribute_type' thy cid_long class_scheme_ty t)
|
||||
else
|
||||
Const (s, Type(st,[ty, ty']))
|
||||
$ (update_attribute_type' thy cid_long class_scheme_ty t)
|
||||
end
|
||||
| update_attribute_type' thy cid_long class_scheme_ty (t $ t') =
|
||||
(update_attribute_type' thy cid_long class_scheme_ty t)
|
||||
$ (update_attribute_type' thy cid_long class_scheme_ty t')
|
||||
| update_attribute_type' thy cid_long class_scheme_ty (Abs(s, ty, t)) =
|
||||
Abs(s, ty, update_attribute_type' thy cid_long class_scheme_ty t)
|
||||
| update_attribute_type' _ cid_long class_scheme_ty (Free(s, ty)) = if s = invariantN
|
||||
then Free (s, class_scheme_ty)
|
||||
else Free (s, ty)
|
||||
| update_attribute_type' _ cid_long _ t = t
|
||||
val inv_ty = Syntax.read_typ (Proof_Context.init_global thy)
|
||||
(Name.aT ^ " " ^ cid_long ^ schemeN)
|
||||
val _ = writeln("In define_inv cid_long: " ^ cid_long)
|
||||
(* Update the type of each attribute update function to match the type of the
|
||||
current class. *)
|
||||
val inv_term' = update_attribute_type thy inv_ty inv_term
|
||||
(*val inv_term' = update_attribute_type' thy cid_long inv_ty inv_term*)
|
||||
val inv_term' = update_attribute_type' thy cid_long inv_ty inv_term_test
|
||||
(*val inv_term' = update_attribute_type' thy cid_long inv_ty inv_term_test'*)
|
||||
val _ = writeln("In define_inv inv_term': "
|
||||
^ Syntax.string_of_term (Proof_Context.init_global thy) inv_term')
|
||||
val eq_inv_ty = inv_ty --> HOLogic.boolT
|
||||
val _ = writeln("CCCCCCCCCCCCCCCCCCCCCCCCC")
|
||||
val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term'
|
||||
val _ = writeln("In define_inv abs_term: "
|
||||
^ Syntax.string_of_term (Proof_Context.init_global thy) abs_term)
|
||||
in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end
|
||||
|
||||
fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||
|
|
|
@ -98,7 +98,7 @@
|
|||
\input{session}
|
||||
% optional bibliography
|
||||
\IfFileExists{root.bib}{%
|
||||
{\small \renewcommand{\doi}[1]{}
|
||||
{\small
|
||||
\newcommand{\urlprefix}{}
|
||||
|
||||
\bibliographystyle{splncs04}
|
||||
|
|
|
@ -272,34 +272,36 @@ NOTE Verification is mostly based on document reviews (design, implementation, t
|
|||
Definition*[verifier, short_name="''verifier''"]
|
||||
\<open>entity that is responsible for one or more verification activities\<close>
|
||||
|
||||
chapter\<open>Software Management and Organisation\<close>
|
||||
text\<open>Representing chapter 5 in @{cite "bsi:50128:2014"}.\<close>
|
||||
|
||||
section\<open>Organization, Roles and Responsabilities\<close>
|
||||
text\<open>see also section \<^emph>\<open>Software management and organization\<close>.\<close>
|
||||
|
||||
datatype role = PM (* Program Manager *)
|
||||
| RQM (* Requirements Manager *)
|
||||
| DES (* Designer *)
|
||||
| IMP (* Implementer *)
|
||||
| ASR (* Assessor *)
|
||||
| INT (* Integrator *)
|
||||
| TST (* Tester *)
|
||||
| VER (* Verifier *)
|
||||
| VnV (* Verification and Validation *)
|
||||
| VAL (* Validator *)
|
||||
datatype role = PM \<comment> \<open>Program Manager\<close>
|
||||
| RQM \<comment> \<open>Requirements Manager\<close>
|
||||
| DES \<comment> \<open>Designer\<close>
|
||||
| IMP \<comment> \<open>Implementer\<close>
|
||||
| ASR \<comment> \<open>Assessor\<close>
|
||||
| INT \<comment> \<open>Integrator\<close>
|
||||
| TST \<comment> \<open>Tester\<close>
|
||||
| VER \<comment> \<open>Verifier\<close>
|
||||
| VnV \<comment> \<open>Verification and Validation\<close>
|
||||
| VAL \<comment> \<open>Validator\<close>
|
||||
|
||||
|
||||
|
||||
datatype phase = SYSDEV_ext (* System Development Phase (external) *)
|
||||
| SPl (* Software Planning *)
|
||||
| SR (* Software Requirement *)
|
||||
| SA (* Software Architecture *)
|
||||
| SDES (* Software Design *)
|
||||
| SCDES (* Software Component Design *)
|
||||
| CInT (* Component Implementation and Testing *)
|
||||
| SI (* Software Integration *)
|
||||
| SV (* Software Validation *)
|
||||
| SD (* Software Deployment *)
|
||||
| SM (* Software Maintenance *)
|
||||
datatype phase = SYSDEV_ext \<comment> \<open> System Development Phase (external)\<close>
|
||||
| SPl \<comment> \<open>Software Planning\<close>
|
||||
| SR \<comment> \<open>Software Requirement\<close>
|
||||
| SA \<comment> \<open>Software Architecture\<close>
|
||||
| SDES \<comment> \<open>Software Design\<close>
|
||||
| SCDES \<comment> \<open>Software Component Design\<close>
|
||||
| CInT \<comment> \<open>Component Implementation and Testing\<close>
|
||||
| SI \<comment> \<open>Software Integration\<close>
|
||||
| SV \<comment> \<open>Software Validation\<close>
|
||||
| SD \<comment> \<open>Software Deployment\<close>
|
||||
| SM \<comment> \<open>Software Maintenance\<close>
|
||||
|
||||
abbreviation software_requirement :: "phase" where "software_requirement \<equiv> SR"
|
||||
abbreviation software_architecture :: "phase" where "software_architecture \<equiv> SA"
|
||||
|
@ -429,6 +431,21 @@ doc_class TC = requirement +
|
|||
is_concerned :: "role set" <= "UNIV"
|
||||
type_synonym timing_constraint = TC
|
||||
|
||||
|
||||
section\<open>Personal Competence\<close>
|
||||
|
||||
text\<open>pp. 20 MORE TO COME\<close>
|
||||
|
||||
section\<open>Lifecycle Issues and Documentation\<close>
|
||||
|
||||
text\<open>Figure 3 in Chapter 5: Illustrative Development Lifecycle 1\<close>
|
||||
|
||||
text\<open>Global Overview\<close>
|
||||
|
||||
figure*[fig3::figure, relative_width="100",
|
||||
src="''examples/CENELEC_50128/mini_odo/document/figures/CENELEC-Fig.3-docStructure.png''"]
|
||||
\<open>Illustrative Development Lifecycle 1\<close>
|
||||
|
||||
section\<open>Software Assurance related Entities and Concepts\<close>
|
||||
|
||||
|
||||
|
@ -494,121 +511,145 @@ doc_class judgement =
|
|||
|
||||
section\<open> Design and Test Documents \<close>
|
||||
|
||||
doc_class cenelec_text = text_element +
|
||||
doc_class cenelec_document = text_element +
|
||||
phase :: "phase"
|
||||
level :: "int option" <= "Some(0)"
|
||||
written_by :: role \<comment> \<open>Annex C Table C.1 \<close>
|
||||
fst_check :: role \<comment> \<open>Annex C Table C.1\<close>
|
||||
snd_check :: role \<comment> \<open>Annex C Table C.1\<close>
|
||||
is_concerned :: "role set" <= "UNIV"
|
||||
invariant must_be_chapter :: "text_element.level \<sigma> = Some(0)"
|
||||
invariant three_eyes_prcpl:: " written_by \<sigma> \<noteq> fst_check \<sigma>
|
||||
\<and> written_by \<sigma> \<noteq> snd_check \<sigma>"
|
||||
text\<open>see Fig.3.\<close>
|
||||
|
||||
|
||||
|
||||
doc_class SYSREQS = cenelec_text +
|
||||
doc_class SYSREQS = cenelec_document +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
accepts "\<lbrace>objectives||requirement||cenelec_text\<rbrace>\<^sup>+ "
|
||||
accepts "\<lbrace>objectives||requirement||cenelec_document\<rbrace>\<^sup>+ "
|
||||
type_synonym system_requirements_specification = SYSREQS
|
||||
|
||||
doc_class SYSSREQS = cenelec_text +
|
||||
doc_class SYSSREQS = cenelec_document +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_safety_requirements_specification = SYSSREQS
|
||||
|
||||
doc_class SYSAD = cenelec_text +
|
||||
doc_class SYSAD = cenelec_document +
|
||||
phase :: "phase" <= "SYSDEV_ext"
|
||||
type_synonym system_architecture_description = SYSAD
|
||||
|
||||
doc_class SYSS_pl = cenelec_text +
|
||||
doc_class SYSS_pl = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
type_synonym system_safety_plan = SYSS_pl
|
||||
|
||||
doc_class SYS_VnV_pl = cenelec_text +
|
||||
doc_class SYS_VnV_pl = cenelec_document +
|
||||
phase :: "phase" <= "SPl"
|
||||
type_synonym system_VnV_plan = SYS_VnV_pl
|
||||
|
||||
doc_class SWRS = cenelec_text +
|
||||
doc_class SWRS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_requirements_specification = SWRS
|
||||
|
||||
doc_class SWRVR = cenelec_text +
|
||||
doc_class SWRVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_requirements_verification_report = SWRVR
|
||||
|
||||
|
||||
doc_class SWTS = cenelec_text +
|
||||
doc_class SWTS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_test_specification = SWTS
|
||||
|
||||
doc_class SWAS = cenelec_text +
|
||||
|
||||
doc_class SWAS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_architecture_specification = SWAS
|
||||
|
||||
doc_class SWDS = cenelec_text +
|
||||
doc_class SWDS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_design_specification = SWDS
|
||||
|
||||
doc_class SWIS = cenelec_text +
|
||||
phase :: "phase" <= "SD"
|
||||
doc_class SWIS_E =
|
||||
\<comment> \<open>input - output of an operation; alternatives could be channels or public global variables ...\<close>
|
||||
op_name :: "string"
|
||||
op_args_ty :: "(string \<times> typ) list \<times> typ"
|
||||
raises_exn :: "(string \<times> typ) list" \<comment> \<open>exn name and value\<close>
|
||||
pre_cond :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
|
||||
post_cond :: "(string \<times> thm) list" <= "[]" \<comment> \<open>labels and predicates\<close>
|
||||
boundary_pre_cond :: "thm list" <= "[]"
|
||||
type_synonym software_interface_specification_element = SWIS_E
|
||||
|
||||
|
||||
doc_class SWIS = cenelec_document +
|
||||
phase :: "phase" <= "SCDES"
|
||||
written_by :: "role" <= "DES"
|
||||
fst_check :: "role" <= "VER"
|
||||
snd_check :: "role" <= "VAL"
|
||||
components :: "SWIS_E list"
|
||||
type_synonym software_interface_specification = SWIS
|
||||
|
||||
doc_class SWITS = cenelec_text +
|
||||
doc_class SWITS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_integration_test_specification = SWITS
|
||||
|
||||
doc_class SWHITS = cenelec_text +
|
||||
doc_class SWHITS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_hardware_integration_test_specification = SWHITS
|
||||
|
||||
doc_class SWADVR = cenelec_text +
|
||||
doc_class SWADVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_architecture_and_design_verification_report = SWADVR
|
||||
|
||||
doc_class SWCDS = cenelec_text +
|
||||
doc_class SWCDS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_design_specification = SWCDS
|
||||
|
||||
doc_class SWCTS = cenelec_text +
|
||||
doc_class SWCTS = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_test_specification = SWCTS
|
||||
|
||||
doc_class SWCDVR = cenelec_text +
|
||||
doc_class SWCDVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_design_verification_report = SWCDVR
|
||||
|
||||
|
||||
doc_class SWSCD = cenelec_text +
|
||||
doc_class SWSCD = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_source_code_and_documentation = SWSCD
|
||||
|
||||
doc_class SWCTR = cenelec_text +
|
||||
doc_class SWCTR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_component_test_report = SWCTR
|
||||
|
||||
doc_class SWSCVR = cenelec_text +
|
||||
doc_class SWSCVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_source_code_verification_report = SWSCVR
|
||||
|
||||
doc_class SWHAITR = cenelec_text +
|
||||
doc_class SWHAITR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_hardware_integration_test_report = SWHAITR
|
||||
|
||||
doc_class SWIVR = cenelec_text +
|
||||
doc_class SWIVR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_integration_verification_report = SWIVR
|
||||
|
||||
doc_class SWTR_global = cenelec_text +
|
||||
doc_class SWTR_global = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym overall_software_test_report = SWTR_global
|
||||
|
||||
doc_class SWVALR = cenelec_text +
|
||||
doc_class SWVALR = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_validation_report = SWVALR
|
||||
|
||||
doc_class SWDD = cenelec_text +
|
||||
doc_class SWDD = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_deployment_documents = SWDD
|
||||
|
||||
doc_class SWMD = cenelec_text +
|
||||
doc_class SWMD = cenelec_document +
|
||||
phase :: "phase" <= "SD"
|
||||
type_synonym software_maintenance_documents = SWMD
|
||||
|
||||
|
||||
section\<open> Software Assurance \<close>
|
||||
\<comment> \<open>MORE TO COME\<close>
|
||||
|
||||
subsection\<open> Software Testing \<close>
|
||||
text\<open>Objective:
|
||||
|
@ -725,20 +766,26 @@ doc_class test_requirement = test_item +
|
|||
doc_class test_adm_role = test_item +
|
||||
name :: string
|
||||
|
||||
doc_class test_documentation =
|
||||
doc_class test_documentation = (* OUTDATED ? *)
|
||||
no :: "nat"
|
||||
accepts "test_specification ~~
|
||||
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement\<rbrakk> ~~
|
||||
test_adm_role"
|
||||
accepts "test_specification ~~
|
||||
\<lbrace>test_case~~test_result\<rbrace>\<^sup>+ ~~
|
||||
\<lbrace>test_environment||test_tool\<rbrace>\<^sup>+ ~~
|
||||
\<lbrakk>test_requirement \<rbrakk> ~~
|
||||
test_adm_role"
|
||||
|
||||
|
||||
section\<open>Global Documentation Structure\<close>
|
||||
|
||||
doc_class global_documentation_structure = text_element +
|
||||
level :: "int option" <= "Some(-1::int)" \<comment> \<open>document must be a chapter\<close>
|
||||
accepts "SYSREQS ~~ \<comment> \<open>system_requirements_specification\<close>
|
||||
SYSSREQS ~~ \<comment> \<open>system_safety_requirements_specification\<close>
|
||||
SYSAD ~~ \<comment> \<open>system_architecture description\<close>
|
||||
SYSS_pl ~~ \<comment> \<open>system safety plan\<close>
|
||||
(SWRS || SWTS) " \<comment> \<open>software requirements specification OR
|
||||
overall software test specification\<close>
|
||||
(* MORE TO COME : *)
|
||||
|
||||
section\<open> META : Testing and Validation \<close>
|
||||
|
||||
|
|
|
@ -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
|
|
@ -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>)"
|
|
@ -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
|
||||
|
|