summaryrefslogtreecommitdiff
path: root/Master
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2016-01-11 22:14:10 +0000
committerKarl Berry <karl@freefriends.org>2016-01-11 22:14:10 +0000
commitfa0bec11de440831d4a6869435a36bae6aa332a8 (patch)
tree4bcfefd43e84b5571dd627e275254ae4f9036409 /Master
parentd4448f82dcc77711f4ff520ec6fe31463991ac8b (diff)
prftree (11jan16)
git-svn-id: svn://tug.org/texlive/trunk@39356 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master')
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.pdfbin273555 -> 278480 bytes
-rw-r--r--Master/texmf-dist/doc/latex/prftree/prftreedoc.tex210
-rw-r--r--Master/texmf-dist/tex/latex/prftree/prftree.sty159
3 files changed, 247 insertions, 122 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
index 87e9d490d6a..f92aee2c858 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
index b28e254b1d5..9db4c1f9e90 100644
--- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
+++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex
@@ -1,4 +1,6 @@
\documentclass{amsart}
+\usepackage{color}
+\usepackage{graphics}
\usepackage[ND,SEQ]{prftree}
\usepackage{url}
@@ -284,9 +286,10 @@ sub-proof basis, as will be done in most examples.\vspace{2ex}
There are various \TeX{} dimensions that influence how proofs are
constructed:
\begin{itemize}
-\item\ \verb|\prflinepad| (default 0.3ex): the space between the
- bottom line of assumptions and the proof line, and also the space
- between the proof line and the top of the conclusion;
+\item\ \verb|\prflinepadbefore| (default 0.3ex): the space between the
+ bottom line of assumptions and the proof line
+\item\ \verb|\prflinepadafter| (default 0.3ex): the space between the
+ proof line and the top of the conclusion;
\item\ \verb|\prflineextra| (default 0.3em): the length which extends
on the left and on the right the proof line so that it is slightly
longer than the largest between the conclusion and the list of
@@ -309,7 +312,7 @@ constructed:
For example,
\begin{displaymath}
- \prflinepad=.7ex
+ \prflinepadafter=.7ex
\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$E}
@@ -321,7 +324,7 @@ For example,
\end{displaymath}
is typeset by
\begin{verbatim}
- \prflinepad=.7ex
+ \prflinepadafter=.7ex
\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$I}
{\prftree[r]{$\supset$E}
@@ -496,6 +499,25 @@ sub-proof whose conclusion is $C$, one obtains the more pleasant
\rightarrow (A \rightarrow C))}
\end{displaymath}\vspace{.2ex}
+The \verb|Strut| option of the package controls a subtle point about
+spacing around a proof line: assumptions and conclusion are usually
+typeset so that the height and the depth of their box is at least the
+one of \verb|\mathstrut|. In this way, adjacent proofs will have their
+proof lines aligned (well, whenever they don't have huge
+conclusions). But, as signalled by Dominic Hughes, sometimes one wants
+the height and the depth to be the ``real'' ones, especially when
+there are no characters/symbols with a positive depth: this forces the
+perceived space above and below the proof line to be exactly the
+values of \verb|\prflinepadbefore| and \verb|\prflinepadafter|. This
+behaviour can be achieved by calling the package with the \verb|STRUT|
+option. Alternatively, one may use the \verb|\prfSTRUToptionfalse|
+command to locally force this behaviour, and
+\verb|\prfSTRUToptiontrue| to return to the standard one. Similarly,
+the \verb|STRUTlabel| package option, together with the pair of
+commands \verb|\prfSTRUTlabeloptiontrue| and
+\verb|\prfSTRUTlabeloptionfalse|, operate on rule names and rule
+labels.\vspace{2ex}
+
The rendering of bounded assumptions is modified by
\verb|\prfboundedstyle|. When $\verb|\prfboundedstyle| = 0$, the
format of the assumption is $[\mbox{formula}]$, which is the default
@@ -574,12 +596,15 @@ command. This can be modified at will. The package defines it as
The assumptions, conclusions, labels, and rule names are drawn using
the following commands, which may be redefined:
\begin{verbatim}
- \def\prfConclusionBox#1{\hbox%
- {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
- \def\prfAssumptionBox#1{\hbox%
- {$\displaystyle\begingroup#1\endgroup\mathstrut$}}
- \def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}
- \def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfConclusionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+\def\prfAssumptionBox#1{%
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
\end{verbatim}
It is not advisable to change these commands in a radical way, unless
one understands how the graphical engine works.
@@ -597,7 +622,7 @@ value aside the labelled point of the proof.
For example,
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
{\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
{\prftree[r]{$\supset$E}
@@ -606,11 +631,11 @@ For example,
{\bot}}
{\neg\neg A}}
{A \supset \neg\neg A}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
is generated by the following code
\begin{verbatim}
- \begin{prooftree}
+ \begin{prfenv}
\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:A>}$}
{\prftree[r]{$\supset\mathrm{I}_{\prfref<assum:not_A>}$}
{\prftree[r]{$\supset$E}
@@ -619,17 +644,17 @@ is generated by the following code
{\bot}}
{\neg\neg A}}
{A \supset \neg\neg A}
- \end{prooftree}
+ \end{prfenv}
\end{verbatim}
The labels are \verb|assum:A| and \verb|assum:not_A|, the reference
values are $1$ and $2$, respectively, and the anchors are these values
on the discharged assumptions on the top of the proof. The references
to these labels are the values in the rule names.\vspace{2ex}
-The \verb|prooftree| environment delimits the scope of labels: the
-\verb|\end{prooftree}| declaration makes the labels still available
+The \verb|prfenv| environment delimits the scope of labels: the
+\verb|\end{prfenv}| declaration makes the labels still available
for reference, but numbering of new labels will restart from
-$1$. Enclosing a proof tree in a \verb|prooftree| environment is not
+$1$. Enclosing a proof tree in a \verb|prfenv| environment is not
mandatory: in such case, labels will be global to the
document.\vspace{2ex}
@@ -687,7 +712,7 @@ For example, the disjunction elimination rule is a perfect way to
illustrate the reason behind the \textbf{label} option, i.e., the need
to discharge a pair of assumptions:
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\prfinterspace=1.2em
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -695,7 +720,7 @@ to discharge a pair of assumptions:
\prfboundedassumption<assum:orE>{A}}{C}}
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orE>{B}}{C}}{C}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
\begin{verbatim}
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orE>}$}
@@ -713,7 +738,7 @@ may indicate that a label is reused when it should not.
The same example can be used to show how the other options work:
\begin{displaymath}
\begin{array}{@{}ccc@{}}
- \begin{prooftree}
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -722,8 +747,8 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEn>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEr>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -732,8 +757,8 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEr>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orER>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -742,8 +767,8 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orER>{B}}{C}}
{C}
- \end{prooftree} \\
- \begin{prooftree}
+ \end{prfenv} \\
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEa>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -752,8 +777,8 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEa>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEA>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -762,8 +787,8 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEA>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEf>}$}
{\prfsummary{\Gamma}{A \vee B}}
@@ -772,7 +797,7 @@ The same example can be used to show how the other options work:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEf>{B}}{C}}
{C}
- \end{prooftree}
+ \end{prfenv}
\end{array}
\end{displaymath}
@@ -780,7 +805,7 @@ Also, as the \verb|\prfboundedstyle| varies, the resulting proof trees
are:
\begin{displaymath}
\begin{array}{ccc}
- \begin{prooftree}
+ \begin{prfenv}
\prfboundedstyle=0
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:AorE>}$}
@@ -790,8 +815,8 @@ are:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:AorE>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfboundedstyle=1
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:BorE>}$}
@@ -801,8 +826,8 @@ are:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:BorE>{B}}{C}}
{C}
- \end{prooftree} &
- \begin{prooftree}
+ \end{prfenv} &
+ \begin{prfenv}
\prfboundedstyle=2
\prfsummarystyle=4
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:CorE>}$}
@@ -812,7 +837,7 @@ are:
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:CorE>{B}}{C}}
{C}
- \end{prooftree}
+ \end{prfenv}
\end{array}
\end{displaymath}
@@ -821,7 +846,7 @@ generate the assumption values. It contains the last used value, and
initially, it is set to $0$. By modifying its value, e.g., to
\verb|\setcounter{prfassumptioncounter}{1}|,
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\setcounter{prfassumptioncounter}{1}
\prfsummarystyle=2
\prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEff>}$}
@@ -831,7 +856,7 @@ initially, it is set to $0$. By modifying its value, e.g., to
{\prfsummary{\Gamma,
\prfboundedassumption<[l]assum:orEff>{B}}{C}}
{C}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
A labelled assumption box is graphically constructed by the package
@@ -974,7 +999,7 @@ elimination or disjunction introduction.
For example, the proof
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\NDOREL{simp:notA}{\NDLEM{A \vee \neg A}}
{\NDIMPI{\NDDL{[l]simp:notA}{A}}{\neg\neg A \supset A}}
{\NDIMPIL{simp:notnotA}
@@ -982,7 +1007,7 @@ For example, the proof
{\NDDL{simp:notA}{\neg A}}{\bot}}{A}}
{\neg\neg A \supset A}}
{\neg\neg A \supset A}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
is typeset in abbreviated form by the following code
\begin{verbatim}
@@ -996,7 +1021,7 @@ is typeset in abbreviated form by the following code
\end{verbatim}\vspace{2ex}
Similarly, by loading the package as
-\verb|\usepackage[SEQ]{prooftree.sty}|, the following abbreviations
+\verb|\usepackage[SEQ]{prftree.sty}|, the following abbreviations
are available, which roughly correspond to the inference rule of
sequent calculi:
\begin{itemize}
@@ -1044,7 +1069,7 @@ best.\vspace{2ex}
Consider the proof:
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
{\NDIMPI{\NDDL{a:notA}{A}}{\neg\neg A \supset A}}
{\NDIMPIL{a:notnotA}
@@ -1052,7 +1077,7 @@ Consider the proof:
{\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
{\neg\neg A \supset A}}
{\neg\neg A \supset A}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
the space between the axiom and the sub-proof of the positive case is
visually much less than the space between the positive and the
@@ -1065,7 +1090,7 @@ negative case closer to the positive one.
The first strategy yields:
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\NDOREL{a:notA}{\NDLEM{A \vee \neg A}\hspace{.8em}}
{\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
{\NDIMPIL{a:notnotA}
@@ -1073,7 +1098,7 @@ The first strategy yields:
{\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
{\neg\neg A \supset A}}
{\neg\neg A \supset A}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
and this effect is given by adding an appropriate \verb|\hspace| after
the axiom, as in
@@ -1091,7 +1116,7 @@ Adding the same space in front of the positive case is equivalent.
The second strategy yields:
\begin{displaymath}
- \begin{prooftree}
+ \begin{prfenv}
\NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
{\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
{\hspace{-.4em}\NDIMPIL{a:notnotA}
@@ -1099,7 +1124,7 @@ The second strategy yields:
{\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
{\neg\neg A \supset A}}
{\neg\neg A \supset A}
- \end{prooftree}
+ \end{prfenv}
\end{displaymath}
Again, this is obtained by adding a negative \verb|hspace| after the
positive case, or, equivalently, before the negative one:
@@ -1132,7 +1157,7 @@ align proof trees, as in
\begin{center}
\fbox{\prfsummarystyle=1
\prfsummary{f}{g}{f \wedge g}}\qquad
- \fbox{$\begin{prooftree}
+ \fbox{$\begin{prfenv}
\NDOREL{a:notA}{\NDLEM{A \vee \neg A}}
{\NDIMPI{\NDDL{[l]a:notA}{A}}{\neg\neg A \supset A}}
{\hspace{-.4em}\NDIMPIL{a:notnotA}
@@ -1140,7 +1165,7 @@ align proof trees, as in
{\NDDL{[l]a:notA}{\neg A}}{\bot}}{A}}
{\neg\neg A \supset A}}
{\neg\neg A \supset A}
- \end{prooftree}$}
+ \end{prfenv}$}
\end{center}
since this is the natural way to put proofs side by side:
\begin{verbatim}
@@ -1533,6 +1558,85 @@ A deduction in a sequent calculus:
\rightarrow B) \rightarrow (A \rightarrow C))}
\end{displaymath}
+Proof tree can be coloured, as kindly pointed out by Dominic Hughes:
+\begin{displaymath}
+ \begin{prfenv}
+ \color{green}\NDIMPIL{ex6:1}
+ {\NDANDI
+ {\color{red}\NDNOTIL{ex6:2}
+ {\NDNOTE
+ {\NDDL{ex6:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex6:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}
+ {\color{blue}\NDNOTIL{ex6:3}
+ {\NDNOTE
+ {\NDDL{[l]ex6:1}{\neg (A \vee B)}}
+ {\NDORIR
+ {\NDDL{ex6:3}{B}}
+ {A \vee B}}
+ {\bot}}
+ {\neg B}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}
+\end{displaymath}\vspace{.2ex}
+
+Also. all the standard box manipulation commands can be freely applied.
+The following examples are not significant for doing mathematics, but
+the mechanics behind can be occasionally useful, for example, to
+shrink a large proof to fit the page length:
+\begin{displaymath}
+ \rotatebox{15}{\begin{prfenv}
+ \NDIMPIL{ex5:1}
+ {\NDANDI
+ {\NDNOTIL{ex5:2}
+ {\NDNOTE
+ {\NDDL{ex5:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex5:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}
+ {\NDNOTIL{ex5:3}
+ {\NDNOTE
+ {\NDDL{[l]ex5:1}{\neg (A \vee B)}}
+ {\NDORIR
+ {\NDDL{ex5:3}{B}}
+ {A \vee B}}
+ {\bot}}
+ {\neg B}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}}
+\end{displaymath}
+\begin{displaymath}
+ \begin{prfenv}
+ \NDIMPIL{ex7:1}
+ {\NDANDI
+ {\reflectbox{\NDNOTIL{ex7:2}
+ {\NDNOTE
+ {\NDDL{ex7:1}{\neg (A \vee B)}}
+ {\NDORIL
+ {\NDDL{ex7:2}{A}}
+ {A \vee B}}
+ {\bot}}
+ {\neg A}}}
+ {\resizebox{20em}{!}{\NDNOTIL{ex7:3}
+ {\NDNOTE
+ {\NDDL{[l]ex7:1}{\neg (A \vee B)}}
+ {\scalebox{.7}[1]{\NDORIR
+ {\NDDL{ex7:3}{B}}
+ {A \vee B}}}
+ {\bot}}
+ {\neg B}}}
+ {\neg A \wedge \neg B}}
+ {\neg (A \vee B) \supset \neg A \wedge \neg B}
+ \end{prfenv}
+\end{displaymath}
+
% -------------------------------------
\clearpage
\section{Internals}\label{sec:internals}
@@ -1645,7 +1749,8 @@ occurrence of a reference, which can be resolved.
Most difficulties in the implementation of references lie in the way
to construct the boxes to be used in the proof tree. But, the tricky
part is the interaction with the \LaTeX{} and \TeX{} kernel for error
-reporting.
+reporting. A small hack has been introduced to force recompilation
+when the references in a proof change.
% -------------------------------------
\clearpage
@@ -1673,7 +1778,6 @@ difficulty is how to represent skylines and how to store them, since
\TeX{} provides no abstract data structures. Hence, the implementation
of this feature has been postponed to a remote future, or to the will
of a real \TeX{} magician.
-
\vfill
\end{document}
diff --git a/Master/texmf-dist/tex/latex/prftree/prftree.sty b/Master/texmf-dist/tex/latex/prftree/prftree.sty
index 2bec5c8f07a..425c1493d71 100644
--- a/Master/texmf-dist/tex/latex/prftree/prftree.sty
+++ b/Master/texmf-dist/tex/latex/prftree/prftree.sty
@@ -1,7 +1,7 @@
%
% prftree.sty
-% by Marco Benini - 31st October 2015
-% v1.2
+% by Marco Benini - 11th January 2016
+% v1.4
%
% A package to typeset natural deduction proofs, or sequent proofs, or
% tableau proofs
@@ -10,16 +10,20 @@
%
\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{prftree}[2015/10/31 Natural Deduction Proofs]
+\ProvidesPackage{prftree}[2016/01/11 Natural Deduction Proofs]
% Package options: deactivated by default
\newif\ifprf@NDOption\prf@NDOptionfalse
\newif\ifprf@SEQOption\prf@SEQOptionfalse
\newif\ifprfIMPOption\prfIMPOptionfalse
+\newif\ifprfSTRUToption\prfSTRUToptiontrue
+\newif\ifprfSTRUTlabeloption\prfSTRUTlabeloptiontrue
\DeclareOption{ND}{\prf@NDOptiontrue}
\DeclareOption{SEQ}{\prf@SEQOptiontrue}
\DeclareOption{IMP}{\prfIMPOptiontrue}
+\DeclareOption{Strut}{\prfSTRUToptionfalse}
+\DeclareOption{StrutLabel}{\prfSTRUTlabeloptionfalse}
\ProcessOptions\relax
%--------------------------------------------------------------------
@@ -121,10 +125,13 @@
% future version of the package.
%--------------------------------------------------------------------
-% \prflinepad default 0.3ex
-% the space between the baseline of assumptions and the proof line and
-% also the space between the proof line and the top of the conclusion
-\newdimen\prflinepad\prflinepad.3ex
+% \prflinepadbefore default 0.3ex
+% the space between the bottom of assumptions and the proof line
+\newdimen\prflinepadbefore\prflinepadbefore.3ex
+
+% \prflinepadafter default 0.3ex
+% the space between the proof line and the top of the conclusion
+\newdimen\prflinepadafter\prflinepadafter.3ex
% \prflineextra default 0.3em
% the length which extends on the left and on the right the proof line
@@ -181,20 +188,24 @@
% \prfConclusionBox
% the command to draw the conclusion box
\def\prfConclusionBox#1{%
- \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
% \prfAssumptionBox
% the command to draw the assumption box
\def\prfAssumptionBox#1{%
- \hbox{$\displaystyle\begingroup#1\endgroup\mathstrut$}}
+ \hbox{$\displaystyle\begingroup#1\endgroup%
+ \ifprfSTRUToption\mathstrut\fi$}}
% \prfRuleNameBox
% the command to draw the rule name box.
-\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfRuleNameBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
% \prfLabelBox
% the command to draw the label box.
-\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup\strut}}
+\def\prfLabelBox#1{\hbox{\begingroup#1\endgroup%
+ \ifprfSTRUTlabeloption\strut\fi}}
% \prfdiscargedassumption
% the command to draw a discharged assumption in a custom way.
@@ -326,9 +337,9 @@
\newif\ifprf@lbl@fnsymbol\prf@lbl@fnsymbolfalse
\newif\ifprf@lbl@label\prf@lbl@labelfalse
-% The prooftree environment is used to define the scope of the
+% The prftree environment is used to define the scope of the
% assumption references
-\newenvironment{prooftree}%
+\newenvironment{prfenv}%
{\setcounter{prfassumptioncounter}{0}}%
{\setcounter{prfassumptioncounter}{0}}
@@ -336,15 +347,23 @@
\def\ifprf@undefref<#1>{%
\expandafter\ifx\csname prf@ref@@#1\endcsname\relax}
+% Test whether a reference has never been referenced before
+\def\ifprf@unrefref<#1>{%
+ \expandafter\ifx\csname prf@refref@@#1\endcsname\relax}
+
% Test whether a reference has been written in the .aux file
\def\ifprf@unwrittenref<#1>{%
\expandafter\ifx\csname prf@w@ref@#1\endcsname\relax}
% Write a reference
+\newif\ifprf@refhack\prf@refhacktrue
\protected\def\prfref<#1>{%
\ifprf@undefref<#1>\relax\mbox{??}%
- \PackageWarningNoLine{prftree}{Undefined reference <#1>}\relax%
- \else\csname prf@ref@@#1\endcsname\relax\fi\relax}
+ \ifprf@refhack\label{prf@ref@hack}% to force recompilation
+ \global\prf@refhackfalse\fi%
+ \PackageWarningNoLine{prftree}{Undefined reference <#1>}%
+ \expandafter\gdef\csname prf@ref@@#1\endcsname{\mbox{??}}\else%
+ \csname prf@ref@@#1\endcsname\fi\relax}
% Create the anchor from what stored in the .aux file
\def\prfauxlabel#1#2{%
@@ -682,7 +701,9 @@
% #1 the line options
% #2 the rule name
\def\prf@@NNtree#1#2{%
- \edef\prf@choice{\ifprf@label{#1}{#2}\else{#1}{#2}{}\fi}%
+ \def\prf@hackpar{#2}%
+ \edef\prf@choice{\ifprf@label{#1}{\noexpand\prf@hackpar}\else%
+ {#1}{\noexpand\prf@hackpar}{}\fi}%
\expandafter\prf@tree\prf@choice}
% We collect the first assumption, if any, or the conclusion otherwise
@@ -735,6 +756,7 @@
% #6 the list of assumptions
%--------------------------------------------------------------------
+\newbox\prf@@@@proofbox
\def\prf@draw#1#2#3#4#5#6{%
% We construct the boxes which will constitute the proof
\ifprf@first\prf@push{1}\else\prf@push{0}\fi%
@@ -878,7 +900,6 @@
% the centre of the rule name and the rule box gets attached to the
% proof line box.
\prf@linedp\z@%
- \ifprf@noline\setbox\prf@fancybox\hbox to2\prf@linewd{}\fi%
\ifprf@rule\advance\prf@linedp.5\ht\prf@fancybox%
\advance\prf@linedp-.5\ht\prf@rulenamebox%
\advance\prf@linedp.5\dp\prf@rulenamebox%
@@ -904,8 +925,8 @@
\hbox{\hskip\prf@temp\raise\dp\prf@linebox\box\prf@linebox}%
% We need to calculate the distance between the assumptions and the
% proofline: if there are no assumptions, it is zero; if there are
- % assumptions but no rule name, it is \prflinepad; otherwise it is
- % \linepad plus half of the "real" line's height
+ % assumptions but no rule name, it is \prflinepadbefore; otherwise
+ % it is \linepadbefore plus half of the "real" line's height
\prf@tmp\z@%
\ifprf@assum%
\ifprf@rule\prf@tmp-.5\ht\prf@linebox%
@@ -915,17 +936,17 @@
\prf@tmp-.5\ht\prf@linebox%
\advance\prf@tmp.5\ht\prf@fancybox%
\advance\prf@tmp.5\dp\prf@fancybox\fi\fi%
- \advance\prf@tmp\prflinepad%
+ \advance\prf@tmp\prflinepadbefore%
\setbox\prf@assumptionsbox%
\vbox{\box\prf@assumptionsbox\nointerlineskip\vskip\prf@tmp}\fi%
% We need to calculate the distance between the proofline and the
% conclusion: it is slightly complex to explain... try to draw the
% whole thing to make it clear!!
- \prf@temp\prflinepad%
+ \prf@temp\prflinepadafter%
\ifprf@noline%
\ifprf@assum%
- \advance\prf@temp\prfemptylinethickness\fi%
- \advance\prf@temp-\prflinepad\fi%
+ \advance\prf@temp\prfemptylinethickness\else%
+ \advance\prf@temp-\prflinepadafter\fi\fi%
\ifprf@rule%
\advance\prf@temp-.5\ht\prf@linebox%
\advance\prf@temp.5\ht\prf@fancybox%
@@ -968,61 +989,61 @@
\def\NDDL#1{\prfboundedassumption<#1>}
\def\NDP{\prftree}
\def\NDANDI{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDANDEL{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}_1$}}
+ \textup{E}_1$}}
\def\NDANDER{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}_2$}}
+ \textup{E}_2$}}
\def\NDANDE{\prftree[by]{$\scriptstyle\mathord{\wedge}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDORIL{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}_1$}}
+ \textup{I}_1$}}
\def\NDORIR{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}_2$}}
+ \textup{I}_2$}}
\def\NDORI{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDORE{\prftree[by]{$\scriptstyle\mathord{\vee}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDOREL#1{\prftree[by]{$\scriptstyle{\vee}%
- {\noexpand\textup{E}}^{\noexpand\prfref<#1>}$}}
+ {\textup{E}}^{\prfref<#1>}$}}
\ifprfIMPOption
\def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDIMPIL#1{\prftree[by]{$\scriptstyle\mathord{\supset}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
+ \textup{I}^{\prfref<#1>}$}}
\else
\def\NDIMPI{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDIMPE{\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDIMPIL#1{%
\prftree[by]{$\scriptstyle\mathord{\rightarrow}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}\fi
+ \textup{I}^{\prfref<#1>}$}}\fi
\def\NDNOTI{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDNOTIL#1{\prftree[by]{$\scriptstyle{\neg}%
- \noexpand\textup{I}^{\noexpand\prfref<#1>}$}}
+ \textup{I}^{\prfref<#1>}$}}
\def\NDNOTE{\prftree[by]{$\scriptstyle\mathord{\neg}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDALLI{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDALLE{\prftree[by]{$\scriptstyle\mathord{\forall}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDEXI{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDEXE{\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{E}$}}
+ \textup{E}$}}
\def\NDEXEL#1{%
\prftree[by]{$\scriptstyle\mathord{\exists}%
- \noexpand\textup{E}^{\noexpand\prfref<#1>}$}}
+ \textup{E}^{\prfref<#1>}$}}
\def\NDTI{\prftree[by]{$\scriptstyle\mathord{\top}%
- \noexpand\textup{I}$}}
+ \textup{I}$}}
\def\NDFE{\prftree[by]{$\scriptstyle\mathord{\bot}%
- \noexpand\textup{E}$}}
- \def\NDLEM{\prftree[by]{$\scriptstyle\noexpand\textup{lem}$}}
- \def\NDAX{\prftree[by]{$\scriptstyle\noexpand\textup{ax}$}}
+ \textup{E}$}}
+ \def\NDLEM{\prftree[by]{$\scriptstyle\textup{lem}$}}
+ \def\NDAX{\prftree[by]{$\scriptstyle\textup{ax}$}}
\fi
% -------------------------------------------------------------------
@@ -1035,40 +1056,40 @@
\def\SEQA{\prfassumption}
\def\SEQD{\prfboundedassumption}
\def\SEQP{\prftree}
- \def\SEQAX{\prftree[by]{$\scriptstyle\noexpand\textup{Ax}$}}
- \def\SEQLF{\prftree[by]{$\scriptstyle\noexpand\textup{L}\bot$}}
- \def\SEQLW{\prftree[by]{$\scriptstyle\noexpand\textup{LW}$}}
- \def\SEQRW{\prftree[by]{$\scriptstyle\noexpand\textup{RW}$}}
- \def\SEQLC{\prftree[by]{$\scriptstyle\noexpand\textup{LC}$}}
- \def\SEQRC{\prftree[by]{$\scriptstyle\noexpand\textup{RC}$}}
- \def\SEQLAND{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQAX{\prftree[by]{$\scriptstyle\textup{Ax}$}}
+ \def\SEQLF{\prftree[by]{$\scriptstyle\textup{L}\bot$}}
+ \def\SEQLW{\prftree[by]{$\scriptstyle\textup{LW}$}}
+ \def\SEQRW{\prftree[by]{$\scriptstyle\textup{RW}$}}
+ \def\SEQLC{\prftree[by]{$\scriptstyle\textup{LC}$}}
+ \def\SEQRC{\prftree[by]{$\scriptstyle\textup{RC}$}}
+ \def\SEQLAND{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\wedge}$}}
- \def\SEQRAND{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRAND{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\wedge}$}}
- \def\SEQLOR{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLOR{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\vee}$}}
- \def\SEQROR{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQROR{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\vee}$}}
\ifprfIMPOption
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\supset}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\supset}$}}
\else
- \def\SEQLIMP{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLIMP{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\rightarrow}$}}
- \def\SEQRIMP{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRIMP{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\rightarrow}$}}
\fi
- \def\SEQLALL{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLALL{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\forall}$}}
- \def\SEQRALL{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQRALL{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\forall}$}}
- \def\SEQLEX{\prftree[by]{$\scriptstyle\noexpand\textup{L}%
+ \def\SEQLEX{\prftree[by]{$\scriptstyle\textup{L}%
\mathord{\exists}$}}
- \def\SEQREX{\prftree[by]{$\scriptstyle\noexpand\textup{R}%
+ \def\SEQREX{\prftree[by]{$\scriptstyle\textup{R}%
\mathord{\exists}$}}
- \def\SEQCUT{\prftree[by]{$\scriptstyle\noexpand\textup{Cut}$}}
+ \def\SEQCUT{\prftree[by]{$\scriptstyle\textup{Cut}$}}
\fi
% -------------------------------------------------------------------