% \iffalse meta-comment % An Infrastructure for Mathematical Statements in sTeX % Copyright (C) 2004-2008 Michael Kohlhase, all rights reserved % this file is released under the % LaTeX Project Public License (LPPL) % % The original of this file is in the public repository at % http://github.com/KWARC/sTeX/ % \fi % % \iffalse %\NeedsTeXFormat{LaTeX2e}[1999/12/01] %\ProvidesPackage{statements}[2019/03/20 v1.4 Semantic Markup for Statements] % %<*driver> \documentclass{ltxdoc} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} \usepackage{url,array,float,amsfonts} \usepackage{statements,presentation} \usepackage{paralist} \usepackage[show]{ed} \usepackage[hyperref=auto,style=alphabetic]{biblatex} \addbibresource{kwarcpubs.bib} \addbibresource{extpubs.bib} \addbibresource{kwarccrossrefs.bib} \addbibresource{extcrossrefs.bib} \usepackage{stex-logo} \usepackage{ctangit} \usepackage{hyperref} \makeindex \floatstyle{boxed} \newfloat{exfig}{thp}{lop} \floatname{exfig}{Example} \def\githubissue#1{\cite{sTeX:github:on}, \hyperlink{https://github.com/KWARC/sTeX/issues/#1}{issue #1}} \begin{document} \RecordChanges \DocInput{statements.dtx} \end{document} % % \fi % % \CheckSum{809} % % \changes{v0.9}{2005/06/14}{First Version with Documentation} % \changes{v0.9a}{2005/07/01}{Completed Documentation} % \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation} % \changes{v0.9c}{2006/01/13}{more packaging} % \changes{v0.9d}{2007/09/09}{moved omtext and friends to the omdoc package} % \changes{v0.9d}{2007/09/09}{made dependence on the omdoc package explicit} % \changes{v0.9d}{2007/09/09}{adding ids to many elements} % \changes{v0.9e}{2008/05/27}{adding cross-references} % \changes{v0.9e}{2008/09/29}{augmenting the index macros with optional values} % \changes{v0.9f}{2008/12/04}{changed 'consymb' to 'symboldec' and documented it.} % \changes{v0.9g}{2010/01/14}{the package is now based on {\texttt{ntheorem for presentation}}} % \changes{v0.9g}{2010/01/19}{Added support for localization} % \changes{v0.9g}{2010/02/23}{added {\texttt{\textbackslash symref}}} % \changes{v1.0}{2010/06/18}{now based on {\texttt{omtext}} package instead of {\texttt{omdoc}}} % \changes{v1.0}{2010/07/13}{adding {\texttt{\textbackslash inlineex}}} % \changes{v1.1}{2011/08/25}{renaming all convenience macros for {\texttt{\textbackslash % definendum}} and {\texttt{\textbackslash termref}}} % \changes{v1.1}{2012/07/06}{adding \texttt{\textbackslash usevocab} to example for importing} % \changes{v1.1}{2013/05/17}{more support for types: \texttt{typedec} and % \texttt{\textbackslash inlinetypedec}} % \changes{v1.2}{2015/04/03}{adding optional last arg to \texttt{\textbackslash \*defi*}} % \changes{v1.2}{2015/04/17}{adding \texttt{\textbackslash inlineass}} % \changes{v1.2}{2015/09/05}{adding \texttt{\textbackslash defis} and friends} % \changes{v1.3}{2017/07/31}{adding \texttt{\textbackslash Defi}, \texttt{\textbackslash Trefi} and friends} % \changes{v1.4}{2017/10/15}{changing the optional argument of \texttt{\textbackslash % defi} and friends to a keyval argument} % % \GetFileInfo{statements.sty} % % \MakeShortVerb{\|} % \def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}} % \def\xml{\scsys{Xml}} % \def\mathml{\scsys{MathML}} % \def\omdoc{\scsys{OMDoc}} % \def\openmath{\scsys{OpenMath}} % \def\latexml{\scsys{LaTeXML}} % \def\perl{\scsys{Perl}} % \def\activemath{\scsys{ActiveMath}} % \title{Semantic Markup for Mathematical Statements\thanks{Version {\fileversion} (last revised % {\filedate})}} % \author{Michael Kohlhase\\ % FAU Erlangen-N\"urnberg\\ % \url{http://kwarc.info/kohlhase}} % \maketitle % % \begin{abstract} % The |statements| package is part of the {\stex} collection, a version of {\TeX/\LaTeX} % that allows to markup {\TeX/\LaTeX} documents semantically without leaving the % document format, essentially turning {\TeX/\LaTeX} into a document format for % mathematical knowledge management (MKM). % % This package provides semantic markup facilities for mathematical statements like % Theorems, Lemmata, Axioms, Definitions, etc. in {\stex} files. This structure can be % used by MKM systems for added-value services, either directly from the {\sTeX} % sources, or after translation. % \end{abstract} % % \setcounter{tocdepth}{2}\tableofcontents\newpage % % \section{Introduction}\label{sec:intro} % % The motivation for the |statements| package is very similar to that for semantic macros % in the |modules| package: We want to annotate the structural semantic properties of % statements in the source, but present them as usual in the formatted documents. In % contrast to the case for mathematical objects, the repertoire of mathematical statements % and their structure is more or less fixed. % % This structure can be used by MKM systems for added-value services, either directly from % the {\sTeX} sources, or after translation. Even though it is part of the {\stex} % collection, it can be used independently, like it's sister package |sproofs|. % % {\stex}~\cite{Kohlhase:ulsmf08,sTeX:online} is a version of {\TeX/\LaTeX} that allows to % markup {\TeX/\LaTeX} documents semantically without leaving the document format, % essentially turning {\TeX/\LaTeX} into a document format for mathematical knowledge % management (MKM). Currently the {\omdoc} format~\cite{Kohlhase:OMDoc1.2} is directly % supported. % % \section{The User Interface}\label{sec:user-interface} % % The |statements| package supplies a semantically oriented infrastructure for marking up % mathematical statements: fragments of natural language that state properties of % mathematical objects, e.g. axioms, definitions, or theorems. The |statement| package % provides an infrastructure for marking up the semantic relations between statements for % the {\omdoc} transformation and uses the |ntheorem| package~\cite{MaySch:eltte09} for % formatting (i.e. transformation to PDF). % % \subsection{Package Options}\label{sec:user:options} % % The |statements| package provides the \DescribeMacro{defindex}|defindex| option to % \sTeX. If this is set, then definienda are automatically passed into the index of the % document. Furthermore, the |statements| package passes the % \DescribeMacro{showmeta}|showmeta| to the |metakeys| package. If this is set, then the % metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details and customization % options). The |nontheorem| option tells statements not to load the |ntheorem| package -- % in case some other theorem package is already loaded; e.g. by the |beamer| package and % we prefer that. Note that using the |nontheorem| option in a case where no theorem % package is loaded will lead to errors. % % \subsection{Statements}\label{sec:statements} % % All the statements are marked up as environments, that take a |KeyVal| argument that % allows to annotate semantic information. Generally, we distinguish two forms of % statements: % \begin{description} % \item[{\twintoo{block}{statement}s}] have explicit discourse markers that delimit their % content in the surrounding text, e.g. the boldface word ``{\bf{Theorem}:}'' as a start % marker and a little line-end box as an end marker of a proof. % \item[{\twintoo{flow}{statement}s}] do not have explicit markers, they are interspersed % with the surrounding text. % \end{description} % Since they have the same semantic status, they must both be marked up, but styled % differently. We distinguish between these two presentational forms with the % \DescribeMacro{display=}|display| key, which is allowed on all statement % environments. If it has the value |block| (the default), then the statement will be % presented in a paragraph of its own, have explicit discourse markers for its begin and % end, possibly numbering, etc. If it has the value |flow|, then no extra presentation % will be added the semantic information is invisible to the reader. Another key that is % present on all statement environments in the \DescribeMacro{id=}|id| key it allows to % identify the statement with a name and to reference it with the semantic referencing % infrastructure provided by the |sref| package~\ctancite{Kohlhase:sref}. % % \subsubsection{Axioms and Assertions}\label{sec:user:axiomassertion} % % The \DescribeEnv{assertion}|assertion| environment is used for marking up statements % that can be justified from previously existing knowledge (usually marked with the % monikers ``Theorem'', ``Lemma'', ``Proposition'', etc. in mathematical vernacular). The % environment |assertion| is used for all of them, and the particular subtype of % assertion is given in the \DescribeMacro{type=}|type| key. So instead of % |\begin{Lemma}|\iffalse\end{Lemma}\fi we have to write % |\begin{assertion}[type=lemma]|\iffalse\end{assertion}\fi (see % Example~\ref{fig:assertion} for an example). % \begin{exfig} % \begin{verbatim} % \begin{assertion}[id=sum-over-odds,type=lemma] % $\sum_{i=1}^n{2i-1}=n^2$ % \end{assertion} % \end{verbatim} % \vspace{-1em}will lead to the result\vspace{-2em}\par\noindent % \begin{assertion}[id=sum-over-odds,type=lemma] % $\sum_{i=1}^n{2i-1}=n^2$ % \end{assertion} % \caption{Semantic Markup for a Lemma in a {\texttt{module}} context}\label{fig:assertion} % \end{exfig} % % Whether we will see the keyword ``Lemma'' will depend on the value of the optional % |display| key. In all of the |assertion| environments, the presentation expectation is % that the text will be presented in italic font. The presentation (keywords, spacing, and % numbering) of the |assertion| environment is delegated to a theorem styles from the % |ntheorem| environment. For an assertion of type \meta{type} the |assertion| environment % calls the |ST|\meta{type}|AssEnv| environment provided by the |statements| package; see % Figure~\ref{fig:assertion-types} for a list of provided assertion types. Their % formatting can be customized by redefining the |ST|\meta{type}|AssEnv| environment via % the |\renewtheorem| command from the |ntheorem| package; see~\cite{MaySch:eltte09} for % details. % % \begin{exfig} % \begin{tabular}{|l|l|}\hline % Value & Explanation \\\hline\hline % \textbf{theorem}, \textbf{proposition} % & an important assertion with a proof\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize Note that the meaning of \textbf{theorem} % (in this case the existence of a proof) is not % enforced by {\omdoc} applications. It can be appropriate to give an assertion % the \textbf{theorem}, if the % author knows of a proof (e.g. in the literature), but has not formalized it in % {\omdoc} yet.}\\\hline\hline % \textbf{lemma} & a less important assertion with a proof\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize The difference of importance specified % here is even softer than the other ones, since e.g. reusing % a mathematical paper as a chapter in a larger monograph, may make it necessary to % downgrade a theorem (e.g. the main theorem of the paper) and give it the status of % a lemma in the overall work.}\\\hline\hline % \textbf{corollary} & a simple consequence\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize An assertion is % sometimes marked as a corollary to some other statement, if the proof is % considered simple. This is often the case for important theorems that are simple % to get from technical lemmata.}\\\hline\hline % \textbf{postulate}, \textbf{conjecture} % & an assertion without proof or counter-exam\-ple\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize Conjectures are assertions, whose % semantic value is not yet decided, but which the author considers likely to be % true. In particular, there is no proof or counter-example.}\\\hline\hline % \textbf{false-conjecture} % & an assertion with a counter-example\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize A conjecture that has proven to be false, % i.e. it has a counter-example. Such assertions are often kept for illustration and % historical purposes.}\\\hline\hline % \textbf{obligation}, \textbf{assumption} % & an assertion on which a proof of another depends\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions % are convenient during the exploration of a mathematical theory. They can be used % and proven later (or assumed as an axiom).}\\\hline\hline % \textbf{rule} % & a normative assertion\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions can be interpreted % procedurally to trigger actions}\\\hline\hline % \textbf{observation}, \textbf{remark} & if everything else fails\\\hline % \multicolumn{2}{|p{12cm}|}{\footnotesize This type is the catch-all if none of the others % applies.}\\\hline % \end{tabular} % \caption{Types of Mathematical Assertions}\label{fig:assertion-types} % \end{exfig} % % \DescribeEnv{axiom} The |axiom| environment is similar to |assertion|, but the content % has a different ontological status: axioms are assumed without (formal) justification, % whereas assertions are expected to be justified from other assertions, axioms or % definitions. This environment relegates the formatting to the |STaxiomEnv| environment, % which can be redefined for configuration. % % \subsubsection{Symbols}\label{sec:user:symbol} % % \DescribeEnv{symboldec} The |symboldec| environment can be used for declaring concepts % and symbols. Note the the |symdef| forms from the |modules| package will not do this % automatically (but the |definition| environment and the |\inlinedef| macro will for all % the definienda; see below). The |symboldec| environment takes an optional keywords % argument with the keys |id|, |role|, |title| and |name|. The first is for general % identification, the |role| specifies the {\openmath}/{\omdoc} role, which is one of % |object|, |type|, |sort|, |binder|, |attribution|, |application|, |constant|, % |semantic-attribution|, and |error| (see the {\omdoc} specification for details). The % |name| key specifies the {\openmath} name of the symbol, it should coincide with the % control sequence introduced by the corresponding |\symdef| (if one is present). The % |title| key is for presenting the title of this symbol as in other statements. Usually, % |axiom| and |symboldec| environments are used together as in Figure~\ref{fig:axioms}. % %\begin{exfig} % \begin{verbatim} % \symdef{zero}{0} % \begin{symboldec}[name=zero,title=The number zero,type=constant] % The number zero, it is used as the base case of the inductive definition % of natural numbers via the Peano Axioms. % \end{symboldec} % % \symdef{succ}[1]{\prefix{s}{#1}} % \begin{symboldec}[name=succ,title=The Successor Function,type=application] % The successor function, it is used for the step case of the inductive % definition of natural numbers via the Peano Axioms. % \end{symboldec} % % \symdef{NaturalNumbers}{\mathbb{N}} % \begin{symboldec}[name=succ,title=The Natural Numbers,type=constant] % The natural numbers inductively defined via the Peano Axioms. % \end{symboldec} % % \begin{axiom}[id=peano.P1,title=P1] % $\zero$ is a natural number. % \end{axiom} % ... % \begin{axiom}[id=peano.P5,title=P5] % Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$ % holds for all $n$ in $\NaturalNumbers$ % \end{axiom} % \end{verbatim} % \vspace{-1em}will lead to the result\medskip\par\noindent % \begin{module}[id=peano] % \symdef{zero}{0} % \begin{symboldec}[name=zero,title=The number zero,role=constant] % The number zero, it is used as the base case of the inductive definition % of natural numbers via the Peano Axioms. % \end{symboldec} % % \symdef{succ}[1]{\prefix{s}{#1}} % \begin{symboldec}[name=succ,title=The Successor Function,role=application] % The successor function, it is used for the step case of the inductive % definition of natural numbers via the Peano Axioms. % \end{symboldec} % % \symdef{NaturalNumbers}{\mathbb{N}} % \begin{symboldec}[name=succ,title=The Natural Numbers,role=constant] % The natural numbers inductively defined via the Peano Axioms. % \end{symboldec} % % \begin{axiom}[id=peano.P1,title=P1] % $\zero$ is a natural number. % \end{axiom} % \ldots \stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv} % \begin{axiom}[id=peano.P5,title=P5] % Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$ % holds for all $n$ in $\NaturalNumbers$ % \end{axiom} % \end{module} % \caption{Semantic Markup for the Peano Axioms}\label{fig:axioms} % \end{exfig} % % \subsubsection{Types}\label{sec:user:types} % % In many cases, we can give additional information for symbols in the form of type % assignments. \sTeX does not fix a type system, but allows types to be arbitrary % mathematical objects that they can be defined in (imported) modules. The % \DescribeMacro{\symtype}|\symtype| macro can be used to assign a type to a symbol: % \begin{quote} % |\symtype[|\meta{keys}|]{|\meta{sym}|}{|\meta{type}|}| % \end{quote} % assigns the type \meta{type} to a symbol with name \meta{sym}. For instance % % \begin{center}% % |\symtype[id=plus-nat.type,system=sts]{plus}{\fntype{\Nat,\Nat}\Nat}| % \end{center} % % \noindent assigns the type $\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ (in the % |sts| type system) to the symbol |plus|. This states (type assignments are statements % epistemologically) that addition is a binary function on natural numbers. The |\symtype| % macro supports the keys |id| (for identifiers) and |system| for the type system. % % Often, type assignments occur in informal context, where the type assignment is given by % a natural language sentence or phrase. For this, the |statements| package supplies the % \DescribeEnv{typedec}|typedec| environment and the % \DescribeMacro{\inlinetypedec}|\inlinetypedec| macro. Both take an optional keyval % argument followed by the type. The phrase/sentence is the body of the |typedec| % environment and the last argument of the |\inlinetypedec| macro. The symbol name is % given in via the |for| key. For convenience, the macro % \DescribeMacro{\thedectype}|\thedectype| is bound to the type. So we can use %\begin{verbatim} % \begin{typedec}[for=plus,id=plus-nat.type]{\fntype{\Nat,\Nat}\Nat} % $+:\thedectype$ is a binary function on $\Nat$ % \end{typedec} % \end{verbatim} % instead of the |\symtype| above in an informal setting. % % \subsubsection{Definitions, and Definienda}\label{sec:definition} % % \DescribeEnv{definition} The |definition| environment is used for marking up % mathematical definitions. Its peculiarity is that it defines (i.e. gives a meaning to) % new mathematical concepts or objects. These\DescribeMacro{\definiendum} are identified % by the |\definiendum| macro, which is used as % |\definiendum[|\meta{keys}|]{|\meta{text}|}|. Here, \meta{text} is the text that is to % be emphasized in the presentation. |\definiendum| takes the key % \DescribeMacro{name}|name| for the optional system name of the symbol defined (for % reference via |\termref|, see Section~\ref{sec:user:crossref}). If the |name| key is not % given, then \meta{text} is used as a system name instead, which is usually sufficient % for most situations. The set of keys is extensible to add additional metadata for the % definiendum. Currently only the \DescribeMacro{lemma}|lemma| key is supported, which % allows to specify the base form of the name of the concept involved -- e.g. for % referencing in a glossary or index. % %\begin{exfig} % \def\succ#1{s(#1)} % \begin{verbatim} % \symdef{one}{1} % \begin{definition}[id=one.def,for=one] % $\notatiendum[one]{\one}$ is the successor of $\zero$ % (formally: $\one :=\succ\zero$) % \end{definition} % \end{verbatim} % \vspace{-1em}will lead to the result\medskip\par\noindent\vspace*{-1em} % \begin{module}[id=onedef] % \importmodule{peano} % \symdef{one}{1} % \begin{definition}[id=one.def,for=one] % $\notatiendum[one]{\one}$ is the successor of $\zero$ % (formally: $\one :=\succ\zero$) % \end{definition} % \end{module} % \caption{A Definition based on Figure {\ref{fig:axioms}}}\label{fig:definition} % \end{exfig} % The \DescribeMacro{defi}|\defi{|\meta{word}|}| macro combines the functionality of the % |\definiendum| macro with index markup from the |omdoc| % package~\ctancite{Kohlhase:smomdl}: For definienda where the lemma and \meta{text} % coincide use % \begin{center} % |\defi[|\meta{name}|]{|\meta{lemma}|}[|\meta{indexkeys}|]| % \end{center} % to markup a definiendum \meta{lemma} with system name \meta{name} that appear in the % index (where \meta{indexkeys} are passed to the |\omdoc@index*| macros from the |omtext| % package) --- in other words in almost all definitions of single-word concepts. We also % have the variants \DescribeMacro{\defii}|\defii|, \DescribeMacro{\defiii}|\defiii|, and % \DescribeMacro{\defiv}|\defiv| for (adjectivized) multi-word compounds. Note that if % the definiendum contains semantic macros, then we need to specify the |loadmodules| key % and also protect the semantic macro. For instance if |\eset| is the semantic macro for % $\emptyset$, then we would use % \begin{verbatim} % \defii[eset-comp]{$\protect\eset$}{compatible}[loadmodules] % \end{verbatim} % for the definiendum markup. % % \begin{exfig} % \begin{verbatim} % A \defi{graph} consists of \adefi{vertices}{vertex} and \defis{edge}. % \end{verbatim} % \caption{Definienda where Lemma and Text Form differ}\label{fig:lemma} % \end{exfig} % % For the cases where the lemma and \meta{text} are different we can use the variants % \DescribeMacro{\adefi}|\adefi|, \DescribeMacro{\adefii}|\adefii|, % \DescribeMacro{\adefiii}|\adefiii|, and \DescribeMacro{\adefiv}|\adefiv| that have % an additional first argument that allows to specify an alternative \meta{text}; see % Figure~\ref{fig:defin}. The main use of these is to mark up inflected forms as in % Figure~\ref{fig:lemma}. % % As the greatest number of these are plurals, which tends to be regular (e.g. adding a % trailing ``s'' in English), we provide the variants \DescribeMacro{\defis}|\defis|, % \DescribeMacro{\defiis}|\defiis|, \DescribeMacro{\defiiis}|\defiiis|, and % \DescribeMacro{\defivs}|\defivs| for that case: |\defiis{simple}{group}| is % equivalent to much longer |\adefii{simple groups}{simple}{group}| (but also see % Figure~\ref{fig:lemma}). % % \begin{exfig} % \begin{tabular}{l|l|l} % \multicolumn{3}{l}{source}\\\hline % system name & result & index \\\hline\hline % \multicolumn{3}{l}{\texttt{\textbackslash defi\{concept\}}}\\\hline % |concept| & concept& concept\\\hline\hline % \multicolumn{3}{l}{\texttt{\textbackslash defi[csymbol]\{concept\}}}\\\hline % |csymbol| & concept & concept\\\hline\hline % \multicolumn{3}{l}{\texttt{\textbackslash adefi[csymbol]\{concepts\}\{concept\}}}\\\hline % |csymbol| & concepts & concept\\\hline\hline % \multicolumn{3}{l}{\texttt{\textbackslash defii\{concept\}\{group\}}}\\\hline % |concept-group| & concept group & concept group, \\ % && group - , concept\\\hline\hline % \multicolumn{3}{l}{\texttt{\textbackslash adefii\{small\}\{concept\}\{group\}}}\\\hline % |small-concept-group| & small concept group & small concept group, \\ % && concept group - , small\\\hline % \end{tabular} % \caption{Some definienda with Index}\label{fig:defin} % \end{exfig} % % Note that the |\definiendum|, |\defi*|, |\adefi*|, and |\defi*s|, macros can only be % used inside the definitional situation, i.e. in a |definition| or |symboldec| % environment or a |\inlinedef| macro. If you find yourself in a situation where you want % to use it outside, you will most likely want to wrap the appropriate text fragment in a % |\begin{definition}[display=flow]| ... and |\end{definition}|. For instance, we could % continue the example in Figure~\ref{fig:axioms} with the |definition| environment in % Figure~\ref{fig:definition}. % % \DescribeMacro{\inlinedef} Sometimes we define mathematical concepts in passing, e.g. in % a phrase like ``\ldots $s(o)$ which we call {\textbf{one}}.''. For this we cannot use % the |definition| environment, which presupposes that its content gives all that is % needed to understand the definition. But we do want to make use of the infrastructure % introduced for the |definition| environment. In this situation, we just wrap the phrase % in an |\inlinedef| macro that makes them available. The |\inlinedef| macro accepts the % same |id| and |for| keys in its optional argument, and additionally the |verbalizes| key % which can be used to point to a full definition of the concept somewhere else. % % Note that definienda can only be referenced via a |\term| element, if they are only % allowed inside a named module, i.e. a |module| environment with a name given by the % |id=| key or the |theory=| key on is specified on the definitional environment. % % \subsubsection{Examples}\label{sec:user:example} % % \DescribeEnv{example} The |example| environment is a generic statement environment, % except that the |for| key should be given to specify the identifier what this is an % example for. The |example| environment also expects a |type| key to be specified, so % that we know whether this is an example or a counterexample. % % \DescribeMacro{\inlineex} The |\inlineex| is analogous to |\inlinedef|, only that it is % used for inline examples, e.g. ``\ldots mammals, e.g. goats''. Note that we have used an % inline example for an inline example. % % % \subsection{Cross-Referencing Symbols and Concepts}\label{sec:user:crossref} % % If we have defined a concept with the |\definiendum| macro, then we can mark up other % occurrences of the term as referring to this concept. Note that this process cannot be % fully automatized yet, since that would need advanced language technology to get around % problems of disambiguation, inflection, and non-contiguous phrases\footnote{We do have a % program that helps annotate larger text collections spotting the easy cases; see % {\url{http://kwarc.info/projects/stex}} and look for the program % |termin|.}. Therefore, the \DescribeMacro{\termref}|\termref| can be used to make this % information explicit. It takes the keys % \begin{compactdesc} % \item[\texttt{cdbase}] to specify a URI (a path actually, since {\LaTeX} cannot load % from URIs) where the module can be found. % \item[\texttt{cd}] to specify the module in which the term is defined. If the |cd| key % is not given, then the current module is assumed. If no |cdbase| is specified (this is % the usual case), then the CD has to be imported via a |\importmodule| from the % |modules| package~\ctancite{KohAmb:smmssl}. % \item[\texttt{name}] to specify the name of the definiendum (which is given in the body % of the |\definiendum| or the optional argument). If the |name| key is not specified, % then argument of the |\termref| macro is used. % \item[\texttt{role}] is currently unused. % \end{compactdesc} % |\termref[cd=|\meta{cd}|,name=|\meta{name}|]{|\meta{text}|}| will just typeset the link % text \meta{text} with (if the |hyperref| package is loaded) a hyperlink to the % definition in module \meta{cd} that defines the concept \meta{name}, e.g. that contains % |\defi[|\meta{name}|]{|\meta{text}|}|. % % Just as the |\definiendum| macro has the convenience variants |\defi| and |\?defi*|, the % |\termref| has variants |\trefi|, |\trefii|, |\trefiii|, and |\trefiv| that take two and % three arguments for the parts of the compositum. In the same module, concepts that are % marked up by |\defi{|\meta{name}|}| in the definition can be referenced by % \DescribeMacro{\trefi}|\trefi{|\meta{name}|}|. Here the link text is just % \meta{name}. Concepts defined via |\defii{|\meta{first}|}{|\meta{second}|}| can be % referenced by \DescribeMacro{\trefii}|\trefii{|\meta{first}|}{|\meta{second}|}| (with % link text ``\meta{first} \meta{second}'') and analogously for % |\defiii|/\DescribeMacro{\trefiii}|\trefiii| and % |\defiv|/\DescribeMacro{\trefiv}|\trefiv|. % % We have variants \DescribeMacro{\atref*}|\atrefi|, |\atrefii|, |\atrefiii|, and % |\atrefiv| with alternative link text. For instance % |\atrefii{|\meta{text}|{|\meta{first}|}{|\meta{second}|}| references a concept % introduced by |\defii{|\meta{first}|}{|\meta{second}|}| but with link text \meta{text}. % Of course, if the system identifier is given explicitly in the optional argument of the % definition form, as in |\defii[|\meta{name}|]{|\meta{first}|}{|\meta{second}|}|, then % the terms are referenced by |\trefi{|\meta{name}|}|. % % For referencing terms outside the current module, the module name can be specified in % the first optional argument of the |\*tref*| macros. To specify the |cdbase|, we have to % resort to the |\termref| macro with the keyval arguments. % % Note that the |\termref| treatment above is natural for ``concepts'' declared by the % |\termdef| macro from the |modules| package~\ctancite{KohAmb:smmssl}. Concepts are % natural language names for mathematical objects. For ``symbols'', i.e. symbolic % identifiers for mathematical objects used in mathematical formulae, we use the |\symdef| % macro from the |modules| package. Sometimes, symbols also have an associated natural % language concept, and we want to use the symbol name to reference it (instead of % specifying |cd| and |name| which is more inconvenient). For this the |statements| % package supplies the \DescribeMacro{\symref}|\symref| macro. Like |\termref|, and % invocation of |\symref{|\meta{cseq}|}{|\meta{text}|}| will just typeset \meta{text} with % a hyperlink to the relevant definition (i.e. the one that has the declaration % |for=|\meta{cseq} in the metadata argument.) % % The \DescribeMacro{\term}|\term| macro is a variant of the |\termref| macro that marks % up a phrase as a (possible) term reference, which does not have a link \emph{yet}. This % macro is a convenient placeholder for authoring, where a |\termref| annotation is % (currently) too tedious or the link target has not been authored yet. It facilitates % lazy flexiformalization workflows, where definitions for mathematical concepts are % supplied or marked up by need (e.g. after a |grep| shows that the number of |\term| % annotations of a concept is above a threshold). Editors or active documents can also % support the |\term| macro like a wiki-like dangling link: a click on % |\term{|\meta{phrase}|}| could generate a new editor buffer with a stub definition (an % |definition| environment with |\definiendum| macro and appropriate metadata).\ednote{MK: % we probably need multi-part variants for |?tref*|} % % \section{Configuration of the Presentation}\label{sec:conf} % % \DescribeMacro{\defemph} The |\defemph| macro is a configuration hook that allows to % specify the style of presentation of the {\index*{definiendum}}. By default, it is set to % |\bf| as a fallback, since we can be sure that this is always available. It can be % customized by redefinition: For instance |\renewcommand{\defemph}[1]{\emph{#1}}|, % changes the default behavior to italics. % % \DescribeMacro{\termemph} The |\termenph| macro does the same for the style for % |\termref|, it is empty by default. Note the term might carry an implicit hyper-reference % to the defining occurrence and that the presentation engine might mark this up, changing % this behavior. % % \DescribeMacro{\stDMemph} The |\stDMemph| macro does the same for the style for the % markup of the discourse markers like ``Theorem''. If it is not defined, it is set to % |\bf|; that allows to preset this in the class file. \ednote{function declarations} % % Some authors like to lowercase the semantic references, i.e. use ``axiom 2.6'' instead % of the default ``\sref{peano.P5}'' to refer to the last axiom in % Figure~\ref{fig:axioms}. This can be achieved by redefining the % \DescribeMacro{\STpresent}|\STpresent| macro, which is applied to the keyword of the % |ST*Env| theorem environments.\ednote{this does not quite work as yet, since % \textbf{STpresent} is applied when the label is written. But we would really like to % have it applied when the reference is constructed. But for that we need to split the % label into keyword and number in package |sref|.} % % Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the statement % types provided by the |statement| package. These are mainly intended for package % authors building on |statements|, e.g. for multi-language support. The language % bindings are given in the |smultiling|~\cite{KohGin:smss:svn} package not in % |statements| itself. % %\begin{exfig} % \begin{tabular}{lll} % Environment & configuration macro & value\\\hline\hline % \texttt{STtheoremAssEnv} & \texttt{\textbackslash st@theorem@kw} & \makeatletter\st@theorem@kw\\\hline % \texttt{STlemmaAssEnv} & \texttt{\textbackslash st@lemma@kw} & \makeatletter\st@lemma@kw \\\hline % \texttt{STpropositionAssEnv} & \texttt{\textbackslash st@proposition@kw} & \makeatletter\st@proposition@kw \\\hline % \texttt{STcorollaryAssEnv} & \texttt{\textbackslash st@corollary@kw} & \makeatletter\st@corollary@kw\\\hline % \texttt{STconjectureAssEnv} & \texttt{\textbackslash st@conjecture@kw} & \makeatletter\st@conjecture@kw\\\hline % \texttt{STfalseconjectureAssEnv} & \texttt{\textbackslash st@falseconjecture@kw} & \makeatletter\st@falseconjecture@kw\\\hline % \texttt{STpostulateAssEnv} & \texttt{\textbackslash st@postulate@kw} & \makeatletter\st@postulate@kw\\\hline % \texttt{STobligationAssEnv} & \texttt{\textbackslash st@obligation@kw} & \makeatletter\st@obligation@kw\\\hline % \texttt{STassumptionAssEnv} & \texttt{\textbackslash st@assumption@kw} & \makeatletter\st@assumption@kw\\\hline % \texttt{STobservationAssEnv} & \texttt{\textbackslash st@observation@kw} & \makeatletter\st@observation@kw\\\hline % \texttt{STremarkAssEnv} & \texttt{\textbackslash st@remark@kw} & \makeatletter\st@remark@kw\\\hline % \texttt{STruleAssEnv} & \texttt{\textbackslash st@rule@kw} & \makeatletter\st@rule@kw\\\hline % \texttt{STexampleEnv} & \texttt{\textbackslash st@example@kw} & \makeatletter\st@example@kw\\\hline % \texttt{STaxiomEnv} & \texttt{\textbackslash st@axiom@kw} & \makeatletter\st@axiom@kw\\\hline % \texttt{STdefinitionEnv} & \texttt{\textbackslash st@definition@kw} & \makeatletter\st@definition@kw\\\hline % \texttt{STnotationEnv} & \texttt{\textbackslash st@notation@kw} & \makeatletter\st@notation@kw % \end{tabular} % \caption{Configuration Hooks for statement types}\label{fig:hooks} % \end{exfig} % % \section{Limitations}\label{sec:limitations} % % In this section we document known limitations. If you want to help alleviate them, % please feel free to contact the package author. Some of them are currently discussed in % the \sTeX GitHub repository~\cite{sTeX:github:on}. % \begin{enumerate} % \item none reported yet % \end{enumerate} % % \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\printbibliography} % % \section{The Implementation}\label{sec:impl} % % \subsection{Package Options}\label{sec:impl:options} % % We declare some switches which will modify the behavior according to the package % options. Generally, an option |xxx| will just set the appropriate switches to true % (otherwise they stay false). First we have the general options: |msection| specifies % that theorems should be numbered in the |msection| counter provided by the |mikoslides| % package/class. % \begin{macrocode} %<*package> \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 % \end{macrocode} % % The next measure is to ensure that some {\sTeX} packages are loaded: |omdoc| for the % statement keys, |modules| since we need module identifiers for referencing. Furthermore, % we need the |ntheorem| package for presenting statements. % \begin{macrocode} \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 % \end{macrocode} % Now, we define an auxiliary function that lowercases strings % \begin{macrocode} % \end{macrocode} % Sometimes it is necessary to fallback to symbol names in order to generate xml:id % attributes. For this purpose, we define an auxiliary function which ensures the name % receives a unique NCName equivalent.\ednote{Hard to be unique here, e.g. the names % "foo\_bar" and "foo bar" would receive the same xml:id attributes... of course we can % devise a more complex scheme for the symbol replacement.} % \begin{macrocode} % \end{macrocode} % The following functions are strictly utility functions that makes our life easier later on % \begin{macrocode} % \end{macrocode} % % For the other languages, we set up triggers % \begin{macrocode} \AfterBabelLanguage{ngerman}{\input{statements-ngerman.ldf}} \AfterBabelLanguage{arabic}{\input{statements-arabic.ldf}} % \end{macrocode} % % \subsection{Statements}\label{sec:impl:statements} % % \begin{macro}{\STpresent} % \begin{macrocode} \providecommand\STpresent[1]{#1} % \end{macrocode} % \end{macro} % % \begin{macro}{\define@statement@env} % We define a meta-macro that allows us to define several variants of statements. Upon % beginning this environment, we first set the |KeyVal| attributes, then we decide % whether to print the discourse marker based on the value of the |display| key, then % (given the right Options were set), we show the semantic annotations, and finally % initialize the environment using the appropriate macro. Upon ending the environment, % we just run the respective termination macro. % \begin{macrocode} \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}} % \end{macrocode} % \end{macro} % % \begin{environment}{assertion} % \begin{macrocode} \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} % \end{macrocode} % \end{environment} % % \begin{macro}{\st@*@kw} % We configure the default keywords for the various theorem environments. % \begin{macrocode} \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} % \end{macrocode} % % \end{macro} % Then we configure the presentation of the theorem environments % \begin{macrocode} \if@nthm \theorembodyfont{\itshape} \theoremheaderfont{\normalfont\bfseries} \else \theoremstyle{plain} \fi % \end{macrocode} % % \begin{environment}{ST*AssEnv} % We define a number of internal assertion environments according to the values of its % |type| key. % \begin{macrocode} \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} % \end{macrocode} % \end{environment} % % \begin{environment}{example} % \begin{macrocode} \def\st@example@initialize{}\def\st@example@terminate{} \define@statement@env{example} \def\st@example@kw{Example} \newtheorem{STexampleEnv}[STtheoremAssEnv]{\st@example@kw} % \end{macrocode} % \end{environment} % % \begin{environment}{axiom} % \begin{macrocode} \def\st@axiom@initialize{}\def\st@axiom@terminate{} \define@statement@env{axiom} \def\st@axiom@kw{Axiom} \newtheorem{STaxiomEnv}[STtheoremAssEnv]{\st@axiom@kw} % \end{macrocode} % \end{environment} % % \begin{environment}{symboldec} % We use |\symdef@type| from the |modules| package as the visual cue. % \begin{macrocode} \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}{} % \end{macrocode} % \end{environment} % % \subsubsection{Types}\label{sec:impl:types} % % \begin{macro}{\symtype}\ednote{MK@DG; the type element should percolate up.} % \begin{macrocode} \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$} % \end{macrocode} % \end{macro} % % \begin{macro}{\inlinetypedec} % \begin{macrocode} \newcommand\inlinetypedec[3][]{\metasetkeys{symtype}{#1}\sref@target{\def\thedectype{#2}#3}} % \end{macrocode} % \end{macro} % % \begin{environment}{typedec} % We first define a theorem environment % \begin{macrocode} \def\st@typedec@kw{Type Declaration} \newtheorem{STtypedecEnv}[STtheoremAssEnv]{\st@typedec@kw} % \end{macrocode} % and then the environment itself. % \begin{macrocode} \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} % \end{macrocode} % \end{environment} % % \begin{environment}{definition} % The |definition| environment itself is quite similar to the other's but we need to set % the |\st@indef| switch to suppress warnings from |\st@def@target|. % \begin{macrocode} \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} % \end{macrocode} % \end{environment} % % \begin{environment}{notation} % We initialize the |\def\st@notation@initialize{}| here, and extend it with % functionality below. % \begin{macrocode} \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} % \end{macrocode} % \end{environment} % % \begin{macro}{\st@def@target} % the next macro is a variant of the |\sref@target| macro provided by the |sref| package % specialized for the use in the |\definiendum|, |\defi*|, |\Defi*|, |\defi*s|, and |\Defi*s| % macros. |\st@def@target{|\meta{opt}|}{|\meta{name}|}{|\meta{text}|}| makes a target % with label |sref@|\meta{opt}|@|\meta{modulename}|@target|, if \meta{opt} is non-empty, % else with the label |sref@|\meta{name}|@|\meta{modulename}|@target| (the first time it % encounters this symbol; i.e. if |\sref@|\meta{name}|@|\meta{modulename}|@defined| is % undefined). And it formats the |\defemph|-emphasized \meta{text}. Also it generates % the necessary warnings for a definiendum-like macro. % \begin{macrocode} \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}}% %\footnote{sTeX: target sref@\@@name @\@@cd @target}% for testing targets \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 % \end{macrocode} % \end{macro} % % The |\definiendum| and |\notatiendum| macros are very simple. % % \begin{macro}{\@termdef} % This macro is experimental, it is supposed to be invoked in |\definiendum| to define a % macro with the definiendum text, so that can be re-used later in term assignments (see % the |modules| package). But in the current context, where we rely on {\TeX} groupings % for visibility, this does not work, since the invocations of |\definiendum| are in % |definition| environments and thus one group level too low. Keeping this for future % reference. % \begin{macrocode} \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}}} % \end{macrocode} % \end{macro} % % \begin{macro}{\definiendum} % \begin{macrocode} \addmetakey{definiendum}{name} \addmetakey{definiendum}{lemma} \newcommand\definiendum[2][]{\setkeys{definiendum}{#1}% \st@def@target{\definiendum@name}{\definiendum@name}{#2}} % \end{macrocode} % \end{macro} % % \begin{macro}{\notatiendum} % the |notatiendum| macro also needs to be visible in the |notation| and |definition| % environments % \begin{macrocode} \newcommand\notatiendum[2][]{\notemph{#2}} % \end{macrocode} % \end{macro} % % We expand the {\latexml} bindings for |\defi|, |\defii|, |\defiii| and |\defiv| into two % instances one will be used for the definition and the other for indexing. % % \begin{macro}{\defi} % We split the |\defi| macro in two: |\defi| does the definiendum bit and |\@defi| % handles the last optional argument and does the indexing. The information flow between % them goes via the local |\@phrase| macro. % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\adefi} % Again we split the |\adefi| macro into two parts: |\adef| does the definiendum bit and % |\@adefi| handles the last optional argument and does the indexing. % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\defii} % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\adefii} % analogous to |\adefi| % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\defiii} % similar to |\defii| % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\adefiii} % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\defiv} % similar to |\defiii| % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\adefiv} % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \begin{macro}{\inlineex} % \begin{macrocode} \newcommand\inlineex[2][]{\metasetkeys{omtext}{#1}% \sref@target\sref@label@id{here}#2} % \end{macrocode} % \end{macro} % % \begin{macro}{\inlineass} % \begin{macrocode} \newcommand\inlineass[2][]{\metasetkeys{omtext}{#1}% \sref@target\sref@label@id{here}#2} % \end{macrocode} % \end{macro} % % \begin{macro}{\inlinedef} % \begin{macrocode} \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} % \end{macrocode} % \end{macro} % % \subsection{Cross-Referencing Symbols and Concepts}\label{sec:impl:crossref} % % \begin{macro}{\termref} % |\termref{|\meta{opt}|}{|\meta{text}|}| makes a hyperlink with link text \meta{text} % to the definitional occurrence of the symbol specified by the |name|, |cd|, and % |cdbase| keys in \meta{opt}. We first set sensible defaults if the keys are not % given. If the symbol is defined in the current document (i.e. if the macro % |\sref@|\meta{name}|@|\meta{cd}|@defined| is defined), then we make a local hyperref, % otherwise we punt to |\mod@termref|. % \begin{macrocode} \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} }} % \end{macrocode} % \end{macro} % % \begin{macro}{\tref*} % \begin{macrocode} \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}} % \end{macrocode} % \end{macro} % % \begin{macro}{\tref*} % \begin{macrocode} \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}} % \end{macrocode} % \end{macro} % % \begin{macro}{\Tref*} % \begin{macrocode} \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}} % \end{macrocode} % \end{macro} % % Now we care about the configuration switches, they are set to sensible values, if they % are not defined already. These are just configuration parameters, which should not % appear in documents, therefore we do not provide {\latexml} bindings for them. % \begin{macro}{\*emph} % \begin{macrocode} \providecommand{\termemph}[1]{#1} \providecommand{\defemph}[1]{{\textbf{#1}}} \providecommand{\stDMemph}[1]{{\textbf{#1}}} % \end{macrocode} % \end{macro} % % \begin{macro}{\term} % The |\term| macro is used for wiki-style dangling links with editor support.\ednote{MK: document above} % \begin{macrocode} \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}}} % \end{macrocode} % \end{macro} % \begin{macro}{\symref} % The |\symref| macros is quite simple, since we have done all the heavy lifting in the % |modules| package: we simply apply |\mod@symref@|\meta{arg1} to % \meta{arg2}. % \begin{macrocode} \newcommand\symref[2]{\@nameuse{mod@symref@#1}{#2}} % \end{macrocode} % \end{macro} % % \subsection{Deprecated Functionality}\label{sec:deprecated} % % In this section we centralize old interfaces that are only partially supported any % more. % \begin{macro}{\*def*} % \begin{macrocode} \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}} % \end{macrocode} % \end{macro} % % \begin{macro}{\*def*} % \begin{macrocode} \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}} % % \end{macrocode} % \end{macro} % \Finale % \endinput % \iffalse %%% Local Variables: %%% mode: doctex %%% TeX-master: t %%% End: % \fi % LocalWords: GPL structuresharing STR dtx keyval env envfalse idfalse idtrue typedec st % LocalWords: displayfalse envtrue displaytrue forfalse typefalse titlefalse filedate eg % LocalWords: continuesfalse fortrue fromtrue typetrue titletrue CPERL omdoc thedectype % LocalWords: continuestrue symboldec omtext RequirePackage lowcase lc ToString termin % LocalWords: foreach hyperref href hlink DefStatement OptionalKeyVals ne NeedsTeXFormat % LocalWords: KeyVal xml CMP simpleDef PatternDef DefStatement PatternRule thedectype % LocalWords: requation PatternCMP RecDef DefConstructor keyvals defs psymbols tref eset % LocalWords: openElement symb closeElement ffor getValue attrs metadata undef rangle % LocalWords: afterDigestBegin setProperty AssignValue afterDigest definiendum rangle % LocalWords: cd addr LookupValue getArg toString idx idt definiendum ide idp st@flow % LocalWords: DefMacro args unlist inlinedef uri pdf afterOpen numberIt texttt XMath % LocalWords: iffalse consymb ntheorem textbackslash symref def scsys sc sc kw endinput % LocalWords: mathml openmath latexml activemath fileversion maketitle stex importmodule % LocalWords: setcounter tocdepth tableofcontents newpage sproofs ulsmf08 sref usevocab % LocalWords: MaySch eltte09 twintoo sref subsubsection exfig vspace vspace usemhvocab % LocalWords: noindent renewtheorem hline textbf textbf footnotesize ple peano inlineass % LocalWords: STaxiomEnv symdef medskip succ mathbb ldots stepcounter ednote usemhmodule % LocalWords: STtheoremAssEnv stepcounter STtheoremAssEnv stepcounter defin STtypedecEnv % LocalWords: STtheoremAssEnv notatiendum defin smomdl biblatex twindef cdbase defis % LocalWords: twindef atwindef atwindef adjectivized varaiants twindefalt cseq defindex % LocalWords: twindefalt atwindefalt atwindefalt csymbol definalt termref emph emptyset % LocalWords: termref compactdesc KohAmb smmssl twinref atwinref newpart impl customized % LocalWords: termdef defemph defemph renewcommand termemph termenph stDMemph formalized % LocalWords: stDMemph STpresent STpresent makeatletter STlemmaAssEnv textsf emphasized % LocalWords: STpropositionAssEnv STcorollaryAssEnv STconjectureAssEnv langle defiis % LocalWords: STfalseconjectureAssEnv STpostulateAssEnv STobligationAssEnv foo defiis % LocalWords: STassumptionAssEnv STobservationAssEnv STexampleEnv textsf ltxml defiiis % LocalWords: STdefinitionEnv STnotationEnv printbibliography langle ncname localization % LocalWords: theoremstyle sym newenvironment ifx csname endcsname inlineex loadmodules % LocalWords: currentlabel theorembodyfont itshape theoremheaderfont bfseries defiiis % LocalWords: normalfont newtheorem upshape srefaddidkey definendum customization gdef % LocalWords: newcommand indef newif ifst indeffalse indeftrue attr whatsit automatized % LocalWords: STdefinitionEnvKeyword notemph modulename ifundefined atwin defi behavior % LocalWords: expandafter providecommand nameuse doctex ctancite funval defii initialize % LocalWords: funsymbs findnodes symbolnode defsref showmeta showmeta sysname ngerman % LocalWords: defii defiii defiii adefi adefi adefii adefii adefiii adefiii STruleAssEnv % LocalWords: trefi trefii trefiii atref atrefi atrefii atrefiii conf metakeys setkeys % LocalWords: compactenum Deref metasetkeys addmetakey symtype ltx ltx sts specialized % LocalWords: ifmetakeys fntype rightarrow inlinetypedec inlinetypedec STremarkAssEnv % LocalWords: ignorespaces usemodule textcolor STtypedecEnvKeyword flexiformalization % LocalWords: statements-ngerman.ldf omdoc@indexi xspace trefis trefiis trefiiis % LocalWords: importmhmodule % \endinput % Local Variables: % mode: doctex % TeX-master: t % End: