%% %% This is file `statements.sty', %% generated with the docstrip utility. %% %% The original source files were: %% %% statements.dtx (with options: `package') %% \NeedsTeXFormat{LaTeX2e}[1999/12/01] \ProvidesPackage{statements}[2019/03/20 v1.4 Semantic Markup for Statements] \newif\ifdef@index\def@indexfalse \DeclareOption{defindex}{\def@indextrue} \newif\if@nthm\@nthmtrue \DeclareOption{nontheorem}{\@nthmfalse} \newif\if@msection\@msectionfalse \DeclareOption{msection}{\@msectiontrue} \DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omtext}} \ProcessOptions \RequirePackage{omtext} \RequirePackage[base]{babel} \ifcsdef{proof}{\cslet{proof}{\relax}\cslet{endproof}{\relax}}{}% to redefine if necessary \if@nthm \RequirePackage[hyperref]{ntheorem} \theoremstyle{plain} \else \RequirePackage{amsthm} \fi \AfterBabelLanguage{ngerman}{\input{statements-ngerman.ldf}} \AfterBabelLanguage{arabic}{\input{statements-arabic.ldf}} \providecommand\STpresent[1]{#1} \def\define@statement@env#1{% \ifcsdef{#1}{\cslet{#1}{\relax}\cslet{end#1}{\relax}}{}% to redefine if necessary \newenvironment{#1}[1][]{\metasetkeys{omtext}{##1}\sref@target% \@in@omtexttrue% \ifx\omtext@display\st@flow\else% \ifx\omtext@title\@empty\begin{ST#1Env}\else\begin{ST#1Env}[\omtext@title]\fi% \ifx\sref@id\@empty\else\label{#1.\sref@id}\fi \csname st@#1@initialize\endcsname\fi% display \ifx\sref@id\@empty\sref@label@id{here}\else% \sref@label@id{\STpresent{\csname st@#1@kw\endcsname}~\@currentlabel}\fi% \strut\ignorespaces} {\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi% \omtext@post@skip\@in@omtextfalse}} \newenvironment{assertion}[1][]{\metasetkeys{omtext}{#1}\sref@target% \@in@omtexttrue% \ifx\omtext@display\st@flow \itshape\noindent\ignorespaces% \else% display!=flow \xdef\@@@type{\omtext@type}% to keep it safe from \inlinedef \ifx\omtext@title\@empty\begin{ST\@@@type AssEnv}% \else\begin{ST\@@@type AssEnv}[\omtext@title]% \fi% \fi %display=flow \ifx\omtext@type\@empty\else% \sref@label@id{\STpresent{\csname st@\@@@type @kw\endcsname}~\@currentlabel} \fi} {\ifx\omtext@display\st@flow\else\end{ST\@@@type AssEnv}\@in@omtextfalse\fi} \def\st@theorem@kw{Theorem} \def\st@lemma@kw{Lemma} \def\st@proposition@kw{Proposition} \def\st@corollary@kw{Corollary} \def\st@conjecture@kw{Conjecture} \def\st@falseconjecture@kw{Conjecture (false)} \def\st@postulate@kw{Postulate} \def\st@obligation@kw{Obligation} \def\st@assumption@kw{Assumption} \def\st@rule@kw{Rule} \def\st@observation@kw{Observation} \def\st@remark@kw{Remark} \if@nthm \theorembodyfont{\itshape} \theoremheaderfont{\normalfont\bfseries} \else \theoremstyle{plain} \fi \if@msection \newtheorem{STtheoremAssEnv}{\st@theorem@kw}[msection] \else \ifdef{\thesection} {\newtheorem{STtheoremAssEnv}{\st@theorem@kw}[section]} {\newtheorem{STtheoremAssEnv}{\st@theorem@kw}} \fi \newtheorem{STlemmaAssEnv}[STtheoremAssEnv]{\st@lemma@kw} \newtheorem{STpropositionAssEnv}[STtheoremAssEnv]{\st@proposition@kw} \newtheorem{STcorollaryAssEnv}[STtheoremAssEnv]{\st@corollary@kw} \newtheorem{STconjectureAssEnv}[STtheoremAssEnv]{\st@conjecture@kw} \newtheorem{STfalseconjectureAssEnv}[STtheoremAssEnv]{\st@falseconjecture@kw} \newtheorem{STpostulateAssEnv}[STtheoremAssEnv]{\st@postulate@kw} \newtheorem{STobligationAssEnv}[STtheoremAssEnv]{\st@obligation@kw} \newtheorem{STassumptionAssEnv}[STtheoremAssEnv]{\st@assumption@kw} \newtheorem{STobservationAssEnv}[STtheoremAssEnv]{\st@observation@kw} \if@nthm\theorembodyfont{\rmfamily}\else\theoremstyle{definition}\fi \newtheorem{STremarkAssEnv}[STtheoremAssEnv]{\st@remark@kw} \newtheorem{STruleAssEnv}[STtheoremAssEnv]{\st@rule@kw} \def\st@example@initialize{}\def\st@example@terminate{} \define@statement@env{example} \def\st@example@kw{Example} \newtheorem{STexampleEnv}[STtheoremAssEnv]{\st@example@kw} \def\st@axiom@initialize{}\def\st@axiom@terminate{} \define@statement@env{axiom} \def\st@axiom@kw{Axiom} \newtheorem{STaxiomEnv}[STtheoremAssEnv]{\st@axiom@kw} \srefaddidkey{symboldec} \addmetakey{symboldec}{functions} \addmetakey{symboldec}{role} \addmetakey*{symboldec}{title} \addmetakey*{symboldec}{name} \addmetakey{symboldec}{subject} \addmetakey*{symboldec}{display} \newenvironment{symboldec}[1][]{\metasetkeys{symboldec}{#1}\sref@target\st@indeftrue% \ifx\symboldec@display\st@flow\else{\noindent\stDMemph{\symdef@type} \symboldec@name:}\fi% \ifx\symboldec@title\@empty~\else~(\stDMemph{\symboldec@title})\par\fi}{} \srefaddidkey{symtype} \addmetakey*{symtype}{system} \addmetakey*{symtype}{for} \newcommand\type@type{Type} \newcommand\symtype[3][]{\metasetkeys{symtype}{#1}\sref@target% \noindent\type@type \ifx\symtype@\@empty\else (\symtype@system)\fi #2: $#3$} \newcommand\inlinetypedec[3][]{\metasetkeys{symtype}{#1}\sref@target{\def\thedectype{#2}#3}} \def\st@typedec@kw{Type Declaration} \newtheorem{STtypedecEnv}[STtheoremAssEnv]{\st@typedec@kw} \newenvironment{typedec}[2][]{\metasetkeys{omtext}{#1}\sref@target% \def\thedectype{#2}% \ifx\omtext@display\st@flow\else% \ifx\omtext@title\@empty\begin{STtypedecEnv}\else\begin{STtypedecEnv}[\omtext@title]\fi% \ifx\sref@id\@empty\else\label{typedec.\sref@id}\fi \ifx\sref@id\@empty\sref@label@id{here}\else% \sref@label@id{\STpresent{\csname st@typedec@kw\endcsname}~\@currentlabel}\fi% \ignorespaces} {\ifx\omtext@display\st@flow\else\end{STtypedecEnv}\fi\omtext@post@skip} \newif\ifst@indef\st@indeffalse \ifcsdef{definition}{\cslet{definition}{\relax}\cslet{enddefinition}{\relax}}{}% to redefine if necessary \newenvironment{definition}[1][]{\metasetkeys{omtext}{#1}\sref@target\st@indeftrue% \ifx\omtext@display\st@flow\else% \ifx\omtext@title\@empty\begin{STdefinitionEnv}\else\begin{STdefinitionEnv}[\omtext@title]\fi\fi% \ifx\sref@id\@empty\sref@label@id{here}\else% \sref@label@id{\STpresent{\csname st@definition@kw\endcsname}~\@currentlabel}\fi% \ignorespaces} {\ifx\omtext@display\st@flow\else\end{STdefinitionEnv}\fi} \def\st@definition@kw{Definition} \newtheorem{STdefinitionEnv}[STtheoremAssEnv]{\st@definition@kw} \def\notemph#1{#1} \def\st@notation@terminate{} \def\st@notation@initialize{} \define@statement@env{notation} \def\st@notation@kw{Notation} \newtheorem{STnotationEnv}[STtheoremAssEnv]{\st@notation@kw} \newcommand\st@def@target[3]{\edef\@symname{#1}\def\@verbname{#2}% \ifst@indef% if we are in a definition or such \@ifundefined{mod@id}% if we are not in a module {\PackageWarning{statements}{definiendum in unidentified module\MessageBreak \protect\definiendum, \protect\defi*, \protect\Defi*, \protect\defi*s, \protect\Defi*s\MessageBreak can only be referenced when called in a module with id key}}% {% now we are in a module \edef\@@cd{\ifx\omtext@theory\@empty\mod@id\else\omtext@theory\fi}% \edef\@@name{\ifx\@symname\@empty\@verbname\else\@symname\fi}% \defemph{\@ifundefined{sref@\@@name @\@@cd @defined}% {\expandafter\sref@target@ifh{sref@\@@name @\@@cd @target}{#3}}% {#3}}% \expandafter\gdef\csname sref@\@@name @\@@cd @defined\endcsname{yes}% \ifmetakeys@showmeta\metakeys@show@keys{\@@cd}{name:\@@name}\fi}% \else% st@indef: we are not in a definition or such \PackageError{statements}% {definiendum outside definition context\MessageBreak \protect\definiendum, \protect\defi, \protect\Defi, \protect\defi*s, \protect\Defi*s\MessageBreak do not make sense semantically outside a definition.} {Consider wrapping the defining phrase in a \protect\inlinedef}% \fi}% st@indef \newcommand\@termdef[2][]{\def\@test{#1}% \@ifundefined{mod@id}{}{\ifx\@test\@empty\def\@@name{#2}\else\def\@@name{#1}\fi% \termdef{\mod@id @\@@name}{#2}}} \addmetakey{definiendum}{name} \addmetakey{definiendum}{lemma} \newcommand\definiendum[2][]{\setkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{\definiendum@name}{#2}} \newcommand\notatiendum[2][]{\notemph{#2}} \newcommand\@defi[1][]{\ifdef@index\omdoc@indexi[#1]{\@phrase}\fi\xspace} \newcommand\defi[2][]{\metasetkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{#2}{#2}\def\@phrase{#2}\@defi} \newcommand\defis[2][]{\metasetkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{#2}{#2s}\def\@phrase{#2}\@defi} \newcommand\Defi[2][]{\metasetkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{#2}{\capitalize{#2}}\def\@phrase{#2}\@defi} \newcommand\Defis[2][]{\metasetkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{#2}{\capitalize{#2s}}\def\@phrase{#2}\@defi} \newcommand\adefi[3][]{\metasetkeys{definiendum}{#1}\def\@verb{#3}% \st@def@target{\definiendum@name}{#3}{#2}\@adefi} \newcommand\@adefi[1][]{% \ifdef@index% \ifx\definiendum@name\@empty\omdoc@indexi[#1]{\@verb}% \else\omdoc@indexi[at=\definiendum@name,#1]{\@verb}\fi% \fi\xspace} \newcommand\@defii[1][]{\ifdef@index\omdoc@indexii[#1]{\@pone}{\@ptwo}\fi\xspace} \newcommand\defii[3][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}% \st@def@target{\definiendum@name}{#2-#3}{#2 #3}\@defii} \newcommand\defiis[3][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}% \st@def@target{\definiendum@name}{#2-#3}{#2 #3s}\@defii} \newcommand\Defii[3][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}% \st@def@target{\definiendum@name}{#2-#3}{\capitalize{#2 #3}}\@defii} \newcommand\Defiis[3][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}% \st@def@target{\definiendum@name}{#2-#3}{\capitalize{#2 #3s}}\@defii} \newcommand\adefii[4][]{\metasetkeys{definiendum}{#1}\def\@pone{#3}\def\@ptwo{#4}% \st@def@target{\definiendum@name}{#3-#4}{#2}\@adefii} \newcommand\@adefii[1][]{% \ifdef@index% \ifx\definiendum@name\@empty\omdoc@indexii[#1]{\@pone}{\@ptwo}% \else\omdoc@indexii[at=\definiendum@name,#1]{\@pone}{\@ptwo}\fi% \fi\xspace} \newcommand\@defiii[1][]{\ifdef@index\omdoc@indexiii[#1]{\@pone}{\@ptwo}{\@pthree}\fi\xspace} \newcommand\defiii[4][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}% \st@def@target{\definiendum@name}{#2-#3-#4}{#2 #3 #4}\@defiii} \newcommand\defiiis[4][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}% \st@def@target{\definiendum@name}{#2-#3-#4}{#2 #3 #4s}\@defiii} \newcommand\Defiii[4][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}% \st@def@target{\definiendum@name}{#2-#3-#4}{\capitalize{#2 #3 #4}}\@defiii} \newcommand\Defiiis[4][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}% \st@def@target{\definiendum@name}{#2-#3-#4}{\capitalize{#2 #3 #4s}}\@defiii} \newcommand\adefiii[5][]{\metasetkeys{definiendum}{#1}\def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#5}% \st@def@target{\definiendum@name}{#3-#4-#5}{#2}\@adefiii} \newcommand\@adefiii[1][]{% \ifdef@index% \ifx\definiendum@name\@empty\omdoc@indexiii[#1]{\@pone}{\@ptwo}{\@pthree}% \else\omdoc@indexiii[at=\definiendum@name,#1]{\@pone}{\@ptwo}{\@pthree}\fi% \fi\xspace} \newcommand\@defiv[1][]{\ifdef@index\omdoc@indexiv[#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}\fi\xspace} \newcommand\defiv[5][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}% \st@def@target{\definiendum@name}{#2-#3-#4-#5}{#2 #3 #4 #5}\@defiv} \newcommand\defivs[5][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}% \st@def@target{\definiendum@name}{#2-#3-#4-#5}{#2 #3 #4 #5s}\@defiv} \newcommand\Defiv[5][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}% \st@def@target{\definiendum@name}{#2-#3-#4-#5}{\capitalize{#2 #3 #4 #5}}\@defiv} \newcommand\Defivs[5][]{\metasetkeys{definiendum}{#1}% \def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}% \st@def@target{\definiendum@name}{#2-#3-#4-#5}{\capitalize{#2 #3 #4 #5s}}\@defiv} \newcommand\adefiv[6][]{\metasetkeys{definiendum}{#1}% \def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#5}\def\@ptfour{#6}% \st@def@target{\definiendum@name}{#3-#4-#5-#6}{#2}\@adefiv} \newcommand\@adefiv[1][]{% \ifdef@index% \ifx\definiendum@name\@empty\@indiv[#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}% \else\@indiv[at=\definiendum@name,#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}\fi% \fi\xspace} \newcommand\inlineex[2][]{\metasetkeys{omtext}{#1}% \sref@target\sref@label@id{here}#2} \newcommand\inlineass[2][]{\metasetkeys{omtext}{#1}% \sref@target\sref@label@id{here}#2} \newcommand\inlinedef[2][]{\metasetkeys{omtext}{#1}% \if@in@omtext\else% we are not in an omtext or statement \PackageError{modules}{\protect\inlinedef\space outside a statement!}% {Try wrapping the paragraph in a\MessageBreak \protect\begin{omtext}, \protect\begin{assertion}, \protect\begin{axiom}, ... \MessageBreak whatever is suitable semantically}\fi% \sref@target\sref@label@id{here}\st@indeftrue #2} \addmetakey*{termref}{cd} \addmetakey*{termref}{cdbase} \addmetakey*{termref}{name} \addmetakey*{termref}{role} \newcommand\termref[2][]{\metasetkeys{termref}{#1}% \ifx\termref@cd\@empty\def\termref@cd{\mod@id}\fi% \ifx\termref@name\@empty\def\termref@name{#2}\fi% \@ifundefined{sref@\termref@name @\termref@cd @defined}% {\ifx\termref@cdbase\@empty% external reference \mod@termref\termref@cd\termref@name{#2}% \else\sref@href@ifh\termref@cdbase{#2}% \fi}% {\def\@label{sref@\termref@name @\termref@cd @target}% \sref@hlink@ifh\@label{#2}%\footnote{termref: internal reference to \@label} }} \newcommand\atrefi[3][]{\def\@test{#1}% \ifx\@test\@empty\termref[name=#3]{#2}\else\termref[cd=#1,name=#3]{#2}\fi} \newcommand\atrefii[4][]{\atrefi[#1]{#2}{#3-#4}} \newcommand\atrefiii[5][]{\atrefi[#1]{#2}{#3-#4-#5}} \newcommand\atrefiv[6][]{\atrefi[#1]{#2}{#3-#4-#5-#6}} \newcommand\trefi[2][]{\atrefi[#1]{#2}{#2}} \newcommand\trefii[3][]{\atrefi[#1]{#2 #3}{#2-#3}} \newcommand\trefiii[4][]{\atrefi[#1]{#2 #3 #4}{#2-#3-#4}} \newcommand\trefiv[5][]{\atrefi[#1]{#2 #3 #4 #5}{#2-#3-#4-#5}} \newcommand\trefis[2][]{\atrefi[#1]{#2s}{#2}} \newcommand\trefiis[3][]{\atrefi[#1]{#2 #3s}{#2-#3}} \newcommand\trefiiis[4][]{\atrefi[#1]{#2 #3 #4s}{#2-#3-#4}} \newcommand\trefivs[5][]{\atrefi[#1]{#2 #3 #4 #5s}{#2-#3-#4-#5}} \newcommand\Trefi[2][]{\atrefi[#1]{\capitalize{#2}}{#2}} \newcommand\Trefii[3][]{\atrefi[#1]{\capitalize{#2 #3}}{#2-#3}} \newcommand\Trefiii[4][]{\atrefi[#1]{\capitalize{#2 #3 #4}}{#2-#3-#4}} \newcommand\Trefiv[5][]{\atrefi[#1]{\capitalize{#2 #3 #4 #5}}{#2-#3-#4-#5}} \newcommand\Trefis[2][]{\atrefi[#1]{\capitalize{#2s}}{#2}} \newcommand\Trefiis[3][]{\atrefi[#1]{\capitalize{#2 #3s}}{#2-#3}} \newcommand\Trefiiis[4][]{\atrefi[#1]{\capitalize{#2 #3 #4s}}{#2-#3-#4}} \newcommand\Trefivs[5][]{\atrefi[#1]{\capitalize{#2 #3 #4 #5s}}{#2-#3-#4-#5}} \providecommand{\termemph}[1]{#1} \providecommand{\defemph}[1]{{\textbf{#1}}} \providecommand{\stDMemph}[1]{{\textbf{#1}}} \newcommand\term[2][]{\def\@test{#1}% \ifx\@test\@empty\else \@ifundefined{module@defs@#1}{\PackageWarning{statements}% {{\protect\term} specifies module #1 which is not in scope\MessageBreak import it via e.g. via \protect\importmhmodule}}{} \fi% \PackageWarning{statements}% {Dangling link (\protect\term) for "#2" still needs to be specified}% \textcolor{blue}{\underline{#2}}} \newcommand\symref[2]{\@nameuse{mod@symref@#1}{#2}} \newcommand\defin[2][]{\defi[#1]{#2}% \PackageWarning{statements}{\protect\defin\space is deprecated, use \protect\defi\space instead}} \newcommand\twindef[3][]{\defii[#1]{#2}{#3}% \PackageWarning{statements}{\protect\twindef\space is deprecated, use \protect\defii\space instead}} \newcommand\atwindef[4][]{\defiii[#1]{#2}{#3}{#4}% \PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\defiii\space instead}} \newcommand\definalt[3][]{\adefi[#1]{#2}{#3}% \PackageWarning{statements}{\protect\definalt\space is deprecated, use \protect\adefi\space instead}} \newcommand\twindefalt[4][]{\adefii[#1]{#2}{#3}{#4}% \PackageWarning{statements}{\protect\twindefalt\space is deprecated, use \protect\adefii\space instead}} \newcommand\atwindefalt[5][]{\adefiii[#1]{#2}{#3}{#4}{#5}% \PackageWarning{statements}{\protect\atwindefalt\space is deprecated, use \protect\adefiii\space instead}} \newcommand\twinref[3][]{\trefii[#1]{#2}{#3}% \PackageWarning{statements}{\protect\twinref\space is deprecated, use \protect\trefii\space instead}} \newcommand\atwinref[4][]{\atrefiii[#1]{#2}{#3}{#4}% \PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\trefiii\space instead}} \endinput %% %% End of file `statements.sty'.