summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/sproof.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/sproof.dtx')
-rw-r--r--Master/texmf-dist/source/latex/stex/sproof.dtx770
1 files changed, 0 insertions, 770 deletions
diff --git a/Master/texmf-dist/source/latex/stex/sproof.dtx b/Master/texmf-dist/source/latex/stex/sproof.dtx
deleted file mode 100644
index eb3581d1a53..00000000000
--- a/Master/texmf-dist/source/latex/stex/sproof.dtx
+++ /dev/null
@@ -1,770 +0,0 @@
-% \iffalse meta-comment
-% An Infrastructure for Structural Markup for Proofs
-% Copyright (C) 2004-2006 Michael Kohlhase, all rights reserved
-% this file is released under the
-% LaTeX Project Public License (LPPL)
-%
-% The development version of this file can be found at
-% $URL: https://svn.kwarc.info/repos/stex/sty/stex/sproof/sproof.dtx $
-% $Rev: 423 $; last modified by $Author: kohlhase $
-% $Date: 2008-05-07 15:39:51 +0200 (Wed, 07 May 2008) $
-% \fi
-%
-% \iffalse
-%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
-%<package>\ProvidesPackage{sproof}[2006/01/13 v0.9a Semantic Markup for Proofs]
-%
-%<*driver>
-\documentclass{ltxdoc}
-\usepackage{url,array,stex,float,moreverb}
-\usepackage[show]{ed}
-\usepackage{hyperref}
-\makeindex
-\floatstyle{boxed}
-\newfloat{exfig}{thp}{lop}
-\floatname{exfig}{Example}
-\begin{document}\DocInput{sproof.dtx}\end{document}
-%</driver>
-% \fi
-%
-% \CheckSum{407}
-%
-% \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}{2006/10/31}{made sproof.dtx independent of statements.dtx}
-% \changes{v0.9d}{2006/10/31}{revamped the proof end mark management}
-%
-% \GetFileInfo{sproofs.sty}
-%
-% \MakeShortVerb{\|}
-%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}}
-% \def\stex{{\raisebox{-.5ex}S\kern-.5ex\TeX}}
-% \def\sTeX{\stex}
-% \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\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}}
-% \def\activemath{\scsys{ActiveMath}}
-% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
-% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
-% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
-% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
-% \title{Structural Markup for Proofs\thanks{Version {\fileversion} (last revised
-% {\filedate})}}
-% \author{Michael Kohlhase\\
-% Jacobs University, Bremen\\
-% \url{http://kwarc.info/kohlhase}}
-% \maketitle
-%
-% \begin{abstract}
-% The |sproof| packge 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 supplies macros and environment that allow to annotate the structure of
-% mathematical proofs 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}
-%
-%\section{Introduction}\label{sec:sproof}
-%
-% The |sproof| ({\twintoo{semantic}{proofs}}) package supplies macros and environment that
-% allow to annotate the structure of mathematical proofs in {\stex} files. 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 |statements|.
-%
-% {\stex} 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).
-%
-% \begin{exfig}\scriptsize
-% \begin{verbatim}
-% \begin{sproof}[id=simple-proof,for=sum-over-odds]
-% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
-% \begin{spfcases}{For the induction we have to consider the following cases:}
-% \begin{spfcase}{$n=1$}
-% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n=2$}
-% \begin{sproofcomment}[display=flow]
-% This case is not really necessary, but we do it for the
-% fun of it (and to get more intuition).
-% \end{sproofcomment}
-% \begin{spfstep}[display=flow] We compute $1+3=2^{2}=4$.\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n>1$}
-% \begin{spfstep}[type=assumption,id=ind-hyp]
-% Now, we assume that the assertion is true for a certain $k\geq 1$,
-% i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$.
-% \end{spfstep}
-% \begin{sproofcomment}
-% We have to show that we can derive the assertion for $n=k+1$ from
-% this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
-% \end{sproofcomment}
-% \begin{spfstep}
-% We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$
-% \begin{justification}[method=arith:split-sum]
-% by splitting the sum.
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}
-% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
-% \begin{justification}[method=fertilize] by inductive hypothesis.\end{justification}
-% \end{spfstep}
-% \begin{spfstep}[type=conclusion]
-% We can \begin{justification}[method=simplify]simplify\end{justification}
-% the right-hand side to ${k+1}^2$, which proves the assertion.
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfstep}[type=conclusion]
-% We have considered all the cases, so we have proven the assertion.
-% \end{spfstep}
-% \end{spfcases}
-% \end{sproof}
-% \end{verbatim}
-% \vspace*{-.5cm}
-% \caption{A very explicit proof, marked up semantically}\label{fig:proof:src}
-% \end{exfig}
-%
-% We will go over the general intuition by way of our running example (see
-% Figure~\ref{fig:proof:src} for the source and Figure~\ref{fig:proof:result} for the
-% formatted result).\ednote{talk a bit more about proofs and their structure,... maybe
-% copy from OMDoc spec. }
-%
-% \section{The User Interface}
-%
-% \subsection{Proofs and Proof steps}
-%
-% \DescribeEnv{sproof} The |proof| environment is the main container for proofs. It takes
-% an optional |KeyVal| argument that allows to specify the |id| (identifier) and |for|
-% (for which assertion is this a proof) keys. The regular argument of the |proof|
-% environment contains an introductory comment, that may be used to announce the proof
-% style. The |proof| environment contains a sequence of |\step|, |proofcomment|, and
-% |pfcases| environments that are used to markup the proof steps. The |proof| environment
-% has a variant |Proof|, which does not use the proof end marker. This is convenient, if a
-% proof ends in a case distinction, which brings it's own proof end marker with it.
-% \DescribeEnv{sProof} The |Proof| environment is a variant of |proof| that does not mark
-% the end of a proof with a little box; presumably, since one of the subproofs already has
-% one and then a box supplied by the outer proof would generate an otherwise empty line.
-% \DescribeMacro{\sproofidea} The |\sproofidea| macro allows to give a one-paragraph
-% description of the proof idea.
-%
-% \DescribeEnv{spfstep} Regular proof steps are marked up with the |step| environment, which
-% takes an optional |KeyVal| argument for annotations. A proof step usually contains a
-% local assertion (the text of the step) together with some kind of evidence that this can
-% be derived from already established assertions.
-%
-% Note that both |\premise| and |\justarg| can be used with an empty second argument to
-% mark up premises and arguments that are not explicitly mentioned in the text.
-%
-% \begin{exfig}
-% \begin{sproof}[id=simple-proof,for=sum-over-odds]
-% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
-% \begin{spfcases}{For the induction we have to consider the following cases:}
-% \begin{spfcase}{$n=1$}
-% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n=2$}
-% \begin{sproofcomment}[display=flow]
-% This case is not really necessary, but we do it for the fun
-% of it (and to get more intuition).
-% \end{sproofcomment}
-% \begin{spfstep}[display=flow]
-% We compute $1+3=2^{2}=4$
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n>1$}
-% \begin{spfstep}[type=hypothesis,id=ind-hyp]
-% Now, we assume that the assertion is true for a certain $k\geq 1$, i.e.
-% $\sum_{i=1}^k{(2i-1)}=k^{2}$.
-% \end{spfstep}
-% \begin{sproofcomment}
-% We have to show that we can derive the assertion for $n=k+1$ from this
-% assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
-% \end{sproofcomment}
-% \begin{spfstep}[id=splitit]
-% We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$
-% \begin{justification}[method=arith:split-sum]
-% by splitting the sum
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}[id=byindhyp]
-% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
-% \begin{justification}[method=fertilize]
-% by \premise[ind-hyp]{inductive hypothesis}.
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}[type=conclusion]
-% We can \begin{justification}[method=simplify-eq]
-% simplify the {\justarg[rhs]{right-hand side}}
-% \end{justification} to ${k+1}^2$, which proves the assertion.
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfstep}[type=conclusion]
-% We have considered all the cases, so we have proven the assertion.
-% \end{spfstep}
-% \end{spfcases}
-% \end{sproof}
-% \caption{The formatted result of the proof in Figure~\ref{fig:proof:src}}\label{fig:proof:result}
-% \end{exfig}
-%
-% \subsection{Justifications}
-%
-% \DescribeEnv{justification} This evidence is marked up with the |justification|
-% environment in the |sproof| package. This environment totally invisible to the formatted
-% result; it wraps the text in the proof step that corresponds to the evidence. The
-% environment takes an optional |KeyVal| argument, which can have the |method| key, whose
-% value is the name of a proof method (this will only need to mean something to the
-% application that consumes the semantic annotations). Furthermore, the justification can
-% contain ``premises'' (specifications to assertions that were used justify the step) and
-% ``arguments'' (other information taken into account by the proof method).
-%
-% \DescribeMacro{\premise} The |\premise| macro allows to mark up part of the text as
-% reference to an assertion that is used in the argumentation. In the example in
-% Figure~\ref{fig:proof:src} we have used the |\premise| macro to identify the inductive
-% hypothesis.
-%
-% \DescribeMacro{\justarg} The |\justarg| macro is very similar to |\premise| with the
-% difference that it is used to mark up arguments to the proof method. Therefore the
-% content of the first argument is interpreted as a mathematical object rather than as an
-% identifier as in the case of |\premise|. In our example, we specified that the
-% simplification should take place on the right hand side of the equation. Other examples
-% include proof methods that instantiate. Here we would indicate the substituted object in
-% a |\justarg| macro.
-%
-% \subsection{Proof Structure}
-%
-% \DescribeEnv{spfcases} The |pfcases| environment is used to mark up a proof by
-% cases. This environment takes an optional |KeyVal| argument for semantic annotations and
-% a second argument that allows to specify an introductory comment (just like in the
-% |proof| environment).
-%
-% \DescribeEnv{spfcase} The content of a |pfcases| environment are a sequence of case
-% proofs marked up in the |pfcase| environment, which takes an optional |KeyVal| argument
-% for semantic annotations. The second argument is used to specify the the description of
-% the case under considertation. The content of a |pfcase| environment is the same as that
-% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases| environments.
-%
-% \DescribeEnv{sproofcomment} The |proofcomment| environment is much like a |step|, only
-% that it does not have an obejct-level assertion of its own. Rather than asserting some
-% fact that is relevant for the proof, it is used to explain where the proof is going,
-% what we are attempting to to, or what we have achieved so far. As such, it cannot be the
-% target of a |\premise|.
-%
-% \subsection{Proof End Markers}
-%
-% Traditionally, the end of a mathematical proof is marked with a little box at the end of
-% the last line of the proof (if there is space and on the end of the next line if there
-% isn't), like so:\sproofend
-%
-% The |sproof| package provides the \DescribeMacro{\sproofend}|\sproofend| macro for
-% this. If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then
-% this can be obtained by specifying it using the
-% \DescribeMacro{\sProofEndSymbol}|\sProofEndSymbol| configuration macro (e.g. by specifying
-% |\sProofEndSymbol{q.e.d}|).
-%
-% Some of the proof structuring macros above will insert proof end symbols for sub-proofs,
-% in most cases, this is desirable to make the proof structure explicit, but sometimes
-% this wastes space (especially, if a proof ends in a case analysis which will supply its
-% own proof end marker). Therefore, all proof environments have the
-% \DescribeMacro{noproofend}|noproofend| keyword that suppresses the proof end markers for
-% this element. It can be specified on its own, and does not need a value (if one is
-% specified, that is completely ignored).
-%
-% \StopEventually{\ednotemessage}
-%
-% \section{The Implementation}
-%
-% We first set up the Perl Packages for {\latexml}
-% \begin{macrocode}
-%<*ltxml>
-# -*- CPERL -*-
-package LaTeXML::Package::Pool;
-use strict;
-use LaTeXML::Package;
-RequirePackage('omdoc');
-%</ltxml>
-% Then we make sure that the {\stex} |omdoc| package is loaded.
-% \begin{macrocode}
-%<*package>
-\RequirePackage{omdoc}[2007/09/09]
-%</package>
-% \end{macrocode}
-% Then we define the pacakge options and what they do.
-% \begin{macrocode}
-%<*package>
-\newif\ifjust@method\just@methodfalse
-\DeclareOption{method}{\just@methodtrue}
-%</package>
-% \end{macrocode}
-% 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). Firpf we have the general options
-% \begin{macrocode}
-%<*package>
-\newif\ifspf@env\spf@envfalse
-\newif\ifspf@id\spf@idfalse
-\newif\ifspf@display\spf@displayfalse
-\DeclareOption{id}{\spf@idtrue\spf@envtrue}
-\DeclareOption{env}{\spf@envtrue}
-\DeclareOption{display}{\spf@displaytrue\spf@envtrue}
-% \end{macrocode}
-% And then the options that are specific to the |sproof| package.
-% \begin{macrocode}
-\newif\ifspf@for\spf@forfalse
-\newif\ifspf@from\spf@forfalse
-\newif\ifspf@type\spf@typefalse
-\newif\ifspf@title\spf@titlefalse
-\newif\ifspf@proofend\spf@proofendtrue
-\newif\ifspf@continues\spf@continuesfalse
-\DeclareOption{for}{\spf@fortrue\spf@envtrue}
-\DeclareOption{from}{\spf@fromtrue\spf@envtrue}
-\DeclareOption{type}{\spf@typetrue\spf@envtrue}
-\DeclareOption{title}{\spf@titletrue\spf@envtrue}
-\DeclareOption{continues}{\spf@continuepfrue\spf@envtrue}
-\DeclareOption{noproofend}{\spf@proofendfalse\spf@envtrue}
-% \end{macrocode}
-% \begin{macro}{\spftrue}
-% For convenience, we collect the switches into one.
-% \begin{macrocode}
-\def\spftrue{\spf@fortrue\spf@fromtrue\spf@typetrue\spf@continuepfrue}
-% \end{macrocode}
-% \end{macro}
-%
-% Now, we define a set of collective options and tell {\LaTeX} about the end of the
-% declaration section.
-% \begin{macrocode}
-\DeclareOption{draft}{\spf@envtrue\just@methodtrue}
-\DeclareOption{all}{\spf@envtrue\just@medhodtrue}
-\ProcessOptions
-%</package>
-% \end{macrocode}
-%
-% \subsection{Proofs}\label{sec:impl:proofs}
-%
-% \begin{macrocode}
-%<*package>
-\define@key{spf}{id}{\def\spf@id{#1}}
-\define@key{spf}{display}{\def\spf@display{#1}}
-\define@key{spf}{for}{\def\spf@for{#1}}
-\define@key{spf}{from}{\def\spf@from{#1}}
-\define@key{spf}{sproofend}{\spf@proofendtrue\def\sproof@box{#1}}
-\define@key{spf}{noproofend}[imeanit]{\spf@proofendfalse}
-\define@key{spf}{type}{\def\spf@type{#1}}
-\define@key{spf}{title}{\def\spf@title{#1}}
-\define@key{spf}{continues}{\def\spf@continues{#1}}
-%</package>
-%<*ltxml>
-DefKeyVal('pf','id','Semiverbatim');
-DefKeyVal('pf','display','Semiverbatim'); # not used at the moment
-DefKeyVal('pf','for','Semiverbatim');
-DefKeyVal('pf','from','Semiverbatim');
-DefKeyVal('pf','proofend','Semiverbatim');
-DefKeyVal('pf','noproofend','Semiverbatim');
-DefKeyVal('pf','type','Semiverbatim');
-DefKeyVal('pf','title','Semiverbatim');
-DefKeyVal('pf','continues','Semiverbatim');
-%</ltxml>
-% \end{macrocode}
-%
-% \begin{macro}{\show@st@keys@aux}
-% We now define a macro that shows the |st| keys, if in draft mode, they annotate the
-% document with key/value pairs.
-% \begin{macrocode}
-%<*package>
-\def\show@st@keys@aux{%
-\@ifundefined{spf@id}{}{\ifspf@id{id=\spf@id},\fi}%
-\@ifundefined{spf@display}{}{\ifspf@display{display=\spf@display}\fi}}
-\def\clear@pf@keys{\let\spf@id=\relax\let\spf@display=\relax}
-%</package>
-% \end{macrocode}
-% \end{macro}
-% \begin{macro}{\show@pf@keys@aux}
-% we do the same for the |pf| keys.
-% \begin{macrocode}
-%<*package>
-\def\show@pf@keys@aux{%
-\@ifundefined{spf@for}{}{\ifspf@for{for=\spf@for},\fi}%
-\@ifundefined{spf@from}{}{\ifspf@from{from=\spf@from},\fi}%
-\@ifundefined{spf@prefix}{}{\ifspf@prefix{prefix=\spf@prefix},\fi}%
-\@ifundefined{spf@type}{}{\ifspf@type{type=\spf@type},\fi}%
-\@ifundefined{spf@title}{}{\ifspf@title{title=\spf@title},\fi}%
-\@ifundefined{spf@continues}{}{\ifspf@continues{continues=\spf@continues}\fi}}
-%</package>
-% \end{macrocode}
-% \end{macro}
-% \begin{macro}{\show@pf@keys}
-% and combine them, so that the code is more readable.
-% \begin{macrocode}
-%<*package>
-\def\show@pf@keys#1{\footnote{#1[\show@pf@keys@aux\show@pf@keys@aux]}%
-\clear@pf@keys\clear@pf@keys}
-\def\clear@pf@keys{\let\spf@for=\relax\let\spf@from=\relax\let\spf@prefix=\relax%
-\let\spf@type=\relax\let\spf@title=\relax\let\spf@continues=\relax}
-%</package>
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\spf@flow}
-% We define this macro, so that we can test whether the |display| key has the value |flow|
-% \begin{macrocode}
-%<package>\def\spf@flow{flow}
-% \end{macrocode}
-% \end{macro}
-%
-% For proofs, we will have to have deeply nested structures of enumerated list-like
-% environments. However, {\LaTeX} only allows |enumerate| environments up to nesing depth
-% 4 and general list environments up to listing depth 6. This is not enough for us.
-% Therefore we have decided to go along the route proposed by Leslie Lamport to use a
-% single top-level list with dotted sequences of numbers to identify the position in the
-% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does
-% not do automatic numbering, and we have to add keyword arguments all over the place, to
-% accomodate semantic information.
-%
-% \begin{environment}{pst@with@label}
-% This environment manages\ednote{This gets the labeling right but only works 8 levels
-% deep} the path labeling of the proof steps in the description envionment of the
-% outermost |proof| environment. The argument is the label prefix up to now; which we
-% cache in |\pst@label| (we need evaluate it first, since are in the right place
-% now!). Then we increment the proof depth which is stored in |\count10| (lower
-% counters are used by {\TeX} for page numbering) and initialize
-% the next level counter |\count\count10| with 1. In the end call for this environment,
-% we just decrease the proof depth counter by 1 again.
-% \begin{macrocode}
-%<*package>
-\newenvironment{pst@with@label}[1]{\edef\pst@label{#1}\advance\count10 by 1\count\count10=1}
-{\advance\count10 by -1}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\the@pst@label}
-% |\the@pst@label| evaluates to the current step label.
-% \begin{macrocode}
-\def\the@pst@label{\pst@label.\number\count\count10}
-% \end{macrocode}
-%\end{macro}
-%
-% \begin{macro}{\next@pst@label}
-% |\next@pst@label| increments the step label at the current level.
-% \begin{macrocode}
-\def\next@pst@label{\global\advance\count\count10 by 1}
-% \end{macrocode}
-%\end{macro}
-%
-%\begin{macro}{\sproofend}
-% This macro places a little box at the end of the line if there is space, or at the
-% end of the next line if there isn't
-% \begin{macrocode}
-\def\sproof@box{\hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}}
-\def\sproofend{\ifspf@proofend\hfil\null\nobreak\hfill\sproof@box\par\smallskip\fi}
-\def\sProofEndSymbol#1{\def\sproof@box{#1}}
-%</package>
-%<ltxml>DefConstructor('\sproofend',"");
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{environment}{sproof}
-% In this environment, we initialize the proof depth counter |\count10| to 10, and set
-% up the description environment that will take the proof steps. At the end of the
-% proof, we position the proof end into the last line.
-% \begin{macrocode}
-%<*package>
-\newenvironment{@proof}[2][]{\setkeys{spf}{#1}
-\count10=10\ifx\spf@display\spf@flow\else{\stDMemph{Proof}:}\fi%
-\ifspf@env\show@pf@keys{sproof}\fi{ #2}%
-\def\pst@label{}\newcount\pst@count% initialize the labeling mechanism
-\begin{description}\begin{pst@with@label}{P}}
-{\end{pst@with@label}\end{description}}
-\newenvironment{sproof}[2][]{\begin{@proof}[#1]{#2}}{\sproofend\end{@proof}}
-%</package>
-%<*ltxml>
-DefEnvironment('{sproof} OptionalKeyVals:pf{}',
- "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n"
- . "?#2(<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n)()"
- . "#body"
- . "</omdoc:proof>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{sproofidea}
-% \begin{macrocode}
-%<package>\newcommand{\sproofidea}[2][]{{\stDMemph{Proof Idea}:} #2\sproofend}
-%<*ltxml>
-DefEnvironment('{sproofidea} OptionalKeyVals:pf {}',
- "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n"
- . "<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n"
- . "</omdoc:proof>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% The next two environments (proof steps) and comments, are mostly semantical, they take
-% |KeyVal| arguments that specify their semantic role. In draft mode, they read these
-% values and show them. If the surrounging proof had |display=flow|, then no new |\item| is
-% generated, otherwise it is. In any case, the proof step number (at the current level) is
-% incremented.
-% \begin{environment}{spfstep}
-% \begin{macrocode}
-%<*package>
-\newenvironment{spfstep}[1][]{\setkeys{spf}{#1}
-\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
-\@ifundefined{spf@title}{}{(\stDMemph{\spf@title})}%
-\ifspf@env\show@pf@keys{spfstep}\fi}
-{\next@pst@label}
-%</package>
-%<*ltxml>
-DefCMPEnvironment('{spfstep} OptionalKeyVals:pf',
- "<omdoc:derive ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
- . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
- . "</omdoc:derive>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{sproofcomment}
-% \begin{macrocode}
-%<*package>
-\newenvironment{sproofcomment}[1][]{\setkeys{spf}{#1}
-\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
-\ifspf@env\show@pf@keys{sproofcomment}\fi}
-{\next@pst@label}
-%</package>
-%<*ltxml>
-DefCMPEnvironment('{sproofcomment} OptionalKeyVals:pf',
- "<omdoc:omtext ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
- . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
- . "</omdoc:omtext>");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% The next two environments also take a |KeyVal| arguement, but also a regular one, which
-% contains a start text. Both environments start a new numbered proof level.
-%
-% \begin{environment}{spfcases}
-% In the |pfcases| environment, the start text is displayed as the first comment of the
-% proof.
-% \begin{macrocode}
-%<*package>
-\newenvironment{spfcases}[2][]{\setkeys{spf}{#1}
-\def\@test{#2}\ifx\@test\empty\else
-\ifx\spf@display\spf@flow {#2}\else\item[\the@pst@label]{#2} \fi\fi
-\ifspf@env\show@pf@keys{spfcases}\fi
-\begin{pst@with@label}{\pst@label.\number\count\count10}}
-{\end{pst@with@label}\next@pst@label}
-%</package>
-%<*ltxml>
-DefEnvironment('{spfcases} OptionalKeyVals:pf {}',
- "<omdoc:derive ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n"
- . "<omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP>\n"
- . "<omdoc:method xref='#proof-by-cases'>"
- . "#body"
- . "</omdoc:method>"
- . "</omdoc:derive>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{spfcase}
-% In the |pfcase| environment, the start text is displayed specification of the case
-% after the |\item|
-% \begin{macrocode}
-%<*package>
-\newenvironment{spfcase}[2][]{\setkeys{spf}{#1}
-\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
-\def\@test{#2}\ifx\@test\empty\else{\stDMemph{#2}:}\fi
-\ifspf@env\show@pf@keys{spfcase}\fi
-\begin{pst@with@label}{\pst@label.\number\count\count10}}
-{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}\next@pst@label}
-%</package>
-%<*ltxml>
-DefEnvironment('{spfcase} OptionalKeyVals:pf{}',
- "<omdoc:proof ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>\n"
- . "?#2(<omdoc:omtext><omdoc:CMP><omdoc:p>#2</omdoc:p></omdoc:CMP></omdoc:omtext>\n)()"
- . "#body"
- . "</omdoc:proof>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{subproof}
-% In the |subproof| environment, a new (lower-level) proof environment is
-% started.\ednote{document this above}
-% \begin{macrocode}
-%<*package>
-\newenvironment{subproof}{\begin{pst@with@label}{\pst@label.\number\count\count10}}
-{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}}
-%</package>
-%<*ltxml>
-DefEnvironment('{subproof}',
- "<omdoc:proof>\n #body\n</omdoc:proof>\n");
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \subsection{Justifications}
-%
-% We define the actions that are undertaken, when the keys for justifications are
-% encountered. Here this is very simple, we just define an internal macro with the value,
-% so that we can use it later.\ednote{why are there more in ltxml?, why st@id?}
-% \begin{macrocode}
-%<*package>
-\define@key{just}{id}{\def\just@id{#1}}
-\define@key{just}{method}{\def\just@method{#1}}
-%</package>
-%<*ltxml>
-DefKeyVal('just','id','Semiverbatim');
-DefKeyVal('just','method','Semiverbatim');
-DefKeyVal('just','premises','Semiverbatim');
-DefKeyVal('just','args','Semiverbatim');
-%</ltxml>
-% \end{macrocode}
-%
-% \begin{macro}{\show@just@keys}
-% This macro shows all the key/value pairs when in draft mode.
-% \begin{macrocode}
-%<*package>
-\def\show@just@keys#1{\footnote{#1[\show@pf@keys@aux\show@just@keys@aux]}}%
-\def\show@just@keys@aux{%
-\@ifundefined{just@method}{\relax}{\ifjust@method{method=\just@method},\fi}%
-\clear@pf@keys\clear@just@keys}
-\def\clear@just@keys{\let\just@method=\relax}
-%</package>
-% \end{macrocode}
-% \end{macro}
-%
-% The next three environments and macros are purely semantic, so we ignore the keyval
-% arguments for now and only display the content.\ednote{need to do something about the
-% premise in draft mode.}
-%
-% \begin{environment}{justification}
-% \begin{macrocode}
-%<*package>
-\newenvironment{justification}[1][]{\ifspf@env\setkeys{just}{#1}
- \show@just@keys{justification}\fi}{}
-%</package>
-%<*ltxml>
-sub extractBodyText {
- my ($box, $remove) = @_;
- my $str = '';
- my @boxes = $box->unlist;
- foreach my $b(@boxes) {
- my $s = '';
- if ($b =~ /LaTeXML::Whatsit/) {
- my $body = $b->getBody;
- $s = $body ? extractBodyText($body, $remove) : '';
- } elsif ($b =~ /LaTeXML::Box/) {
- $s = $b->toString || '';
- @{$b}[0] = '' if $remove; }
- $str .= $s; }
- $str =~ s/\s+/ /g;
- $str; }
-
-DefEnvironment('{justification} OptionalKeyVals:just', sub {
- my ($doc, $keys, %props) = @_;
- my $text = extractBodyText($props{body}, 1);
- my $node = LookupValue('_LastSeenCMP');
- $node->appendText($text) if $node;
- my $method = $keys ? $keys->getValue('method') : undef;
- $doc->openElement("omdoc:method", $method ? (xref => $method) : ());
- $doc->absorb($props{body}) if $props{body};
- $doc->closeElement("omdoc:method");
- return; });
-%</ltxml>
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\premise}
-% \begin{macrocode}
-%<*package>
-\newcommand{\premise}[2][]{#2}
-%</package>
-%<*ltxml>
-DefMacro('\premise[]{}', sub {
- my ($xref, $text) = ($_[1], $_[2]);
- my @res = (T_CS('\premise@content'));
- push(@res, T_OTHER('['), $xref->unlist, T_OTHER(']')) if $xref;
- push(@res, T_SPACE, $text->unlist) if $text;
- @res; });
-DefConstructor('\premise@content[]', "<omdoc:premise xref='#1'/>");
-%</ltxml>
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\justarg}
-% the |\justarg| macro is purely semantic, so we ignore the keyval arguments for now and
-% only display the content.
-% \begin{macrocode}
-%<*package>
-\newcommand{\justarg}[2][]{#2}
-%</package>
-%<*ltxml>
-DefMacro('\justarg[]{}', sub { (($_[1] ? $_[1]->unlist : ()),
- T_SPACE, $_[2]->unlist, T_SPACE); });
-
-Tag('omdoc:derive', afterClose=>sub {
- my ($doc, $node) = @_;
- my @children = grep($_->nodeType == XML_ELEMENT_NODE, $node->childNodes);
- my $firstCMP = undef;
- foreach my $child(@children) {
- next unless ($child->localname || '') eq 'CMP';
- if ($child->hasChildNodes()) {
- next unless $#{$child->childNodes} == 0;
- next unless $child->firstChild->nodeType == XML_TEXT_NODE; }
-
- if ($firstCMP) {
- $firstCMP->appendText($child->textContent);
- $node->removeChild($child);
- } else { $firstCMP = $child; }
- }
- });
-
-%</ltxml>
-% \end{macrocode}
-% \end{macro}
-%
-% \subsection{Providing IDs for {\omdoc} Elements}\label{sec:impl:ids}
-%
-% To provide default identifiers, we tag all {\omdoc}
-% elements that allow |xml:id| attributes by excuting the |numberIt| procedure from |omdoc.sty.ltxml|.
-%
-% \begin{macrocode}
-%<*ltxml>
-Tag('omdoc:proof',afterOpen=>\&numberIt);
-Tag('omdoc:derive',afterOpen=>\&numberIt);
-Tag('omdoc:method',afterOpen=>\&numberIt);
-%</ltxml>
-% \end{macrocode}
-%
-% \section{Finale}
-%
-% Finally, we need to terminate the file with a success mark for perl.
-% \begin{macrocode}
-%<ltxml>1;
-% \end{macrocode}
-% \Finale
-\endinput
-
-% \iffalse
-% LocalWords: GPL structuresharing STR sproof dtx CPERL keyval methodfalse env
-%%% Local Variables:
-%%% mode: doctex
-%%% TeX-master: t
-%%% End:
-% \fi
-% LocalWords: methodtrue envtrue medhodtrue DefKeyVal Semiverbatim omdoc args
-% LocalWords: DefEnvironment OptionalKeyVals KeyVal omtext DefConstructor str
-% LocalWords: proofidea KeyVal pfstep DefCMPEnvironment KeyVal proofcomment eq
-% LocalWords: KeyVal pfcases KeyVal pfcase KeyVal extractBodyText unlist elsif
-% LocalWords: foreach getBody toString str str str LookupValue LastSeenCMP
-% LocalWords: appendText getValue undef openElement closeElement DefMacro
-% LocalWords: afterClose nodeType childNodes firstCMP localname hasChildNodes
-% LocalWords: firstChild textContent removeChild