From 7b9f0907404079d0b41248fc94a2308340f2e402 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Tue, 21 Aug 2012 22:30:39 +0000 Subject: bussproofs (21aug12) git-svn-id: svn://tug.org/texlive/trunk@27488 c570f23f-e606-0410-a88d-b1316a301751 --- .../texmf-dist/tex/latex/bussproofs/bussproofs.sty | 233 +++++++++++++++++++-- 1 file changed, 220 insertions(+), 13 deletions(-) (limited to 'Master/texmf-dist/tex/latex/bussproofs/bussproofs.sty') 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$\fCenter$ % @@ -200,6 +211,14 @@ % % \TrinaryInfC{} % +% \QuaternaryInf$\fCenter$ +% +% \QuaternaryInfC{} +% +% \QuinaryInf$\fCenter$ +% +% \QuinaryInfC{} +% % \LeftLabel{} - Puts 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 } + -- cgit v1.2.3