bussproofs (21aug12)

git-svn-id: svn://tug.org/texlive/trunk@27488 c570f23f-e606-0410-a88d-b1316a301751

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
 }
 
+