summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2012-08-21 22:30:39 +0000
committerKarl Berry <karl@freefriends.org>2012-08-21 22:30:39 +0000
commit7b9f0907404079d0b41248fc94a2308340f2e402 (patch)
tree41d615414663a19733838ec81a2ad396de0f397b /Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
parent98b09023bc993f9a7970677d1c865b59fee90732 (diff)
bussproofs (21aug12)
git-svn-id: svn://tug.org/texlive/trunk@27488 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty')
-rw-r--r--Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty233
1 files changed, 220 insertions, 13 deletions
diff --git a/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
index 8d2d4481a10..d5b46d389cf 100644
--- a/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
+++ b/Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty
@@ -1,7 +1,8 @@
%
-\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.0.}
-% bussproofs.sty. Version 1.0
-% (c) 1994,1995,1996,2004,2005,2006. Copyright retained by Samuel R. Buss.
+\def\BPmessage{Proof Tree (bussproofs) style macros. Version 1.1.}
+% bussproofs.sty. Version 1.1
+% (c) 1994,1995,1996,2004,2005,2006, 2011.
+% Copyright retained by Samuel R. Buss.
%
% ==== Legal statement: ====
% This work may be distributed and/or modified under the
@@ -15,7 +16,7 @@
% This work has the LPPL maintenance status 'maintained'.
%
% The Current Maintainer of the work is Sam Buss.
-%
+%
% This work consists of bussproofs.sty.
% =====
% Informal summary of legal situation:
@@ -48,9 +49,16 @@
% New feature: root of proof may now be at the bottom instead of
% at just the top. Thanks to Alex Hertel for the suggestion to implement
% this.
+% June 2011, version 1.1.
+% New feature: 4-ary and 5-ary inferences. Thanks to Thomas Strathmann
+% for taking the initiative to implement these.
+% Four new commands: QuaternaryInf(C) and QuinaryInf(C).
+% Bug fix: \insertBetweenHyps now works for proofs with root at top and
+% three or more hypotheses..
% A good exposition of how to use bussproofs.sty (version 0.9) has been written
-% by Peter Smith and is available on the internet.
+% by Peter Smith and is available on the internet and in the CTAN
+% distribution.
% The comments below also describe the features of bussproofs.sty,
% including user-modifiable parameters.
@@ -102,13 +110,15 @@
% lines may be combined in a single proof.
%
% By using the optional \EnableBpAbbreviations command, various
-% abbreviated two letter commands are enabled. This allows
+% abbreviated two or three letter commands are enabled. This allows,
+% in particular:
% \AX and \AXC for \Axiom and \AxiomC, (resp.),
% \DP for \DisplayProof,
% \BI and \BIC for \BinaryInf and \BinaryInfC,
% \UI and \UIC for \UnaryInf and \UnaryInfC,
% \TI and \TIC for \TrinaryInf and \TrinaryInfC,
% \LL and \RL for \LeftLabel and \RightLabel.
+% See the source code below for additional abbreviations.
% The enabling of these short abbreviations is OPTIONAL, since
% there is the possibility of conflicting with names from other
% macro packages.
@@ -144,7 +154,7 @@
% --------- X
% C
%
-% use the commands
+% use the commands
% \AxiomC{A}
% \AxiomC{B}
% \RightLabel{X}
@@ -187,6 +197,7 @@
% is prohibited in $\Axiom. On the other hand, the $'s are optional
% in \AxiomC and are mandatory in \Axiom. To typeset the argument
% to \AxiomC in math mode, you must use $'s (or \(...\) ).
+% The same comments apply to the inference commands below.
%
% \UnaryInf$<antecendent>\fCenter<succedent>$
%
@@ -200,6 +211,14 @@
%
% \TrinaryInfC{<whole sequent or formula>}
%
+% \QuaternaryInf$<antecendent>\fCenter<succedent>$
+%
+% \QuaternaryInfC{<whole sequent or formula>}
+%
+% \QuinaryInf$<antecendent>\fCenter<succedent>$
+%
+% \QuinaryInfC{<whole sequent or formula>}
+%
% \LeftLabel{<text>} - Puts <text> as a label to the left
% of the next inference line. (Works even if
% \noLine is used too.)
@@ -275,6 +294,10 @@
\let\BIC\BinaryInfC
\let\TI\TrinaryInf
\let\TIC\TrinaryInfC
+ \let\QI\QuaternaryInf
+ \let\QIC\QuaternaryInfC
+ \let\QuI\QuinaryInf
+ \let\QuIC\QuinaryInfC
\let\LL\LeftLabel
\let\RL\RightLabel
\let\DP\DisplayProof
@@ -284,8 +307,8 @@
% The user may wish to override these parameters locally or globally.
% BUT DON'T CHANGE THE PARAMETERS BY CHANGING THIS FILE (to avoid
% future incompatibilities). Instead, you should change them in your
-% TeX document right after including this style file in the
-% header material of your LaTeX document.
+% TeX document right after including this style file in the
+% header material of your LaTeX document.
\def\ScoreOverhang{4pt} % How much underlines extend out
\def\ScoreOverhangLeft{\ScoreOverhang}
@@ -380,6 +403,8 @@
\newdimen\scoreDepth% Score Depth
\newdimen\htLbox%
\newdimen\htRbox%
+\newdimen\htRRbox%
+\newdimen\htRRRbox%
\newdimen\htAbox%
\newdimen\htCbox%
@@ -532,6 +557,187 @@
\ignorespaces%
}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\prepQuaternary{%
+ \ifnum\theLevel<4
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
+ \edef\rrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrcurCenter{\thecur{myCenter}}%
+ \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
+ \edef\ccurScoreStart{\thecur{myScoreStart}}%
+ \edef\ccurCenter{\thecur{myCenter}}%
+ \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\QuaternaryInf$#1\fCenter#2${%
+ \prepQuaternary%
+ \buildConclusion{#1}{#2}%
+ \joinQuaternary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\QuaternaryInfC#1{%
+ \prepQuaternary%
+ \buildConclusionC{#1}%
+ \joinQuaternary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\joinQuaternary{% Construct the quarterary inference into a vbox.
+ % Join the four hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rrcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\rcurBox%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\ccurBox%
+ \advance\lcurScoreEnd by3\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
+ \unhcopy\myBoxA\box\rcurBox
+ \unhcopy\myBoxA\box\rrcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htCbox = \ht\ccurBox%
+ \htRbox = \ht\rcurBox%
+ \htRRbox = \ht\rrcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\def\prepQuinary{%
+ \ifnum\theLevel<5
+ \errmessage{Hypotheses missing!}
+ \fi%
+ \edef\rrrcurBox{\thecur{myBox}}% Set up names of very very right hypothesis
+ \edef\rrrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrrcurCenter{\thecur{myCenter}}%
+ \edef\rrrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rrcurBox{\thecur{myBox}}% Set up names of very right hypothesis
+ \edef\rrcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rrcurCenter{\thecur{myCenter}}%
+ \edef\rrcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\rcurBox{\thecur{myBox}}% Set up names of right hypothesis
+ \edef\rcurScoreStart{\thecur{myScoreStart}}%
+ \edef\rcurCenter{\thecur{myCenter}}%
+ \edef\rcurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\ccurBox{\thecur{myBox}}% Set up names of center hypothesis
+ \edef\ccurScoreStart{\thecur{myScoreStart}}%
+ \edef\ccurCenter{\thecur{myCenter}}%
+ \edef\ccurScoreEnd{\thecur{myScoreEnd}}%
+ \advance\theLevel by-1%
+ \edef\lcurBox{\thecur{myBox}}% Set up names of left hypothesis
+ \edef\lcurScoreStart{\thecur{myScoreStart}}%
+ \edef\lcurCenter{\thecur{myCenter}}%
+ \edef\lcurScoreEnd{\thecur{myScoreEnd}}%
+}
+
+\def\QuinaryInf$#1\fCenter#2${%
+ \prepQuinary%
+ \buildConclusion{#1}{#2}%
+ \joinQuinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\QuinaryInfC#1{%
+ \prepQuinary%
+ \buildConclusionC{#1}%
+ \joinQuinary%
+ \resetInferenceDefaults%
+ \ignorespaces%
+}
+
+\def\joinQuinary{% Construct the quinary inference into a vbox.
+ % Join the five hypotheses's boxes into one hbox.
+ \setbox\myBoxA=\hbox{\theHypSeparation}%
+ \lcurScoreEnd=\rrrcurScoreEnd%
+ \advance\lcurScoreEnd by\wd\rrcurBox%
+ \advance\lcurScoreEnd by\wd\rcurBox%
+ \advance\lcurScoreEnd by\wd\lcurBox%
+ \advance\lcurScoreEnd by\wd\ccurBox%
+ \advance\lcurScoreEnd by4\wd\myBoxA%
+ \displace=\lcurScoreEnd%
+ \advance\displace by -\lcurScoreStart%
+ \lcurCenter=.5\displace%
+ \advance\lcurCenter by\lcurScoreStart%
+ \ifx\rootAtBottomFlag\myTrue%
+ \setbox\lcurBox=%
+ \hbox{\box\lcurBox\unhcopy\myBoxA\box\ccurBox%
+ \unhcopy\myBoxA\box\rcurBox
+ \unhcopy\myBoxA\box\rrcurBox
+ \unhcopy\myBoxA\box\rrrcurBox}%
+ \else%
+ \htLbox = \ht\lcurBox%
+ \htAbox = \ht\myBoxA%
+ \htCbox = \ht\ccurBox%
+ \htRbox = \ht\rcurBox%
+ \htRRbox = \ht\rrcurBox%
+ \htRRRbox = \ht\rrrcurBox%
+ \setbox\lcurBox=%
+ \hbox{\lower\htLbox\box\lcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRbox\box\rrcurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRRRbox\box\rrrcurBox}%
+ \fi%
+ % Adjust center of upper hypotheses according to how much
+ % the lower sequent is off-center.
+ \displace=\newCenter%
+ \advance\displace by -.5\newScoreStart%
+ \advance\displace by -.5\newScoreEnd%
+ \advance\lcurCenter by \displace%
+ %Align and join the curBox and the two hypotheses's box into one vbox.
+ \edef\curBox{\lcurBox}%
+ \edef\curScoreStart{\lcurScoreStart}%
+ \edef\curScoreEnd{\lcurScoreEnd}%
+ \edef\curCenter{\lcurCenter}%
+ \joinUnary%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
\def\buildConclusion#1#2{% Build lower sequent w/ center at \fCenter position.
% Define the boxes
\setbox\myBoxA=\hbox{$\mathord{#1}\fCenter\mathord{\relax}$}%
@@ -587,7 +793,7 @@
% Form the score and labels into a box.
\buildScoreLabels%
% Form the new box and its dimensions
- \ifx\rootAtBottomFlag\myTrue%
+ \ifx\rootAtBottomFlag\myTrue%
\buildRootBottom%
\else%
\buildRootTop%
@@ -597,7 +803,7 @@
\global \curCenter=\newCenter%
}
-\def\buildRootBottom{%
+\def\buildRootBottom{%
\global \setbox \curBox =%
\vbox{\box\curBox%
\vskip\thisAboveSkip \relax%
@@ -688,8 +894,8 @@
\htRbox = \ht\rcurBox%
\setbox\lcurBox=%
\hbox{\lower\htLbox\box\lcurBox%
- \lower\htAbox\box\myBoxA\lower\htCbox\box\ccurBox%
- \lower\htAbox\box\myBoxA\lower\htRbox\box\rcurBox}%
+ \lower\htAbox\copy\myBoxA\lower\htCbox\box\ccurBox%
+ \lower\htAbox\copy\myBoxA\lower\htRbox\box\rcurBox}%
\fi%
% Adjust center of upper hypotheses according to how much
% the lower sequent is off-center.
@@ -928,3 +1134,4 @@
\rootAtTop
}
+