1210

1 
% proof.sty (Proof Figure Macros)


2 
%


3 
% version 2.0


4 
% June 24, 1991


5 
% Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)


6 
%


7 
% This program is free software; you can redistribute it or modify


8 
% it under the terms of the GNU General Public License as published by


9 
% the Free Software Foundation; either versions 1, or (at your option)


10 
% any later version.


11 
%


12 
% This program is distributed in the hope that it will be useful


13 
% but WITHOUT ANY WARRANTY; without even the implied warranty of


14 
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the


15 
% GNU General Public License for more details.


16 
%


17 
% Usage:


18 
% In \documentstyle, specify an optional style `proof', say,


19 
% \documentstyle[proof]{article}.


20 
%


21 
% The following macros are available:


22 
%


23 
% In all the following macros, all the arguments such as


24 
% <Lowers> and <Uppers> are processed in math mode.


25 
%


26 
% \infer<Lower><Uppers>


27 
% draws an inference.


28 
%


29 
% Use & in <Uppers> to delimit upper formulae.


30 
% <Uppers> consists more than 0 formulae.


31 
%


32 
% \infer returns \hbox{ ... } or \vbox{ ... } and


33 
% sets \@LeftOffset and \@RightOffset globally.


34 
%


35 
% \infer[<Label>]<Lower><Uppers>


36 
% draws an inference labeled with <Label>.


37 
%


38 
% \infer*<Lower><Uppers>


39 
% draws a many step deduction.


40 
%


41 
% \infer*[<Label>]<Lower><Uppers>


42 
% draws a many step deduction labeled with <Label>.


43 
%


44 
% \infer=<Lower><Uppers>


45 
% draws a doubleruled deduction.


46 
%


47 
% \infer=[<Label>]<Lower><Uppers>


48 
% draws a doubleruled deduction labeled with <Label>.


49 
%


50 
% \deduce<Lower><Uppers>


51 
% draws an inference without a rule.


52 
%


53 
% \deduce[<Proof>]<Lower><Uppers>


54 
% draws a many step deduction with a proof name.


55 
%


56 
% Example:


57 
% If you want to write


58 
% B C


59 
% 


60 
% A D


61 
% 


62 
% E


63 
% use


64 
% \infer{E}{


65 
% A


66 
% &


67 
% \infer{D}{B & C}


68 
% }


69 
%


70 


71 
% Style Parameters


72 


73 
\newdimen\inferLineSkip \inferLineSkip=2pt


74 
\newdimen\inferLabelSkip \inferLabelSkip=5pt


75 
\def\inferTabSkip{\quad}


76 


77 
% Variables


78 


79 
\newdimen\@LeftOffset % global


80 
\newdimen\@RightOffset % global


81 
\newdimen\@SavedLeftOffset % safe from users


82 


83 
\newdimen\UpperWidth


84 
\newdimen\LowerWidth


85 
\newdimen\LowerHeight


86 
\newdimen\UpperLeftOffset


87 
\newdimen\UpperRightOffset


88 
\newdimen\UpperCenter


89 
\newdimen\LowerCenter


90 
\newdimen\UpperAdjust


91 
\newdimen\RuleAdjust


92 
\newdimen\LowerAdjust


93 
\newdimen\RuleWidth


94 
\newdimen\HLabelAdjust


95 
\newdimen\VLabelAdjust


96 
\newdimen\WidthAdjust


97 


98 
\newbox\@UpperPart


99 
\newbox\@LowerPart


100 
\newbox\@LabelPart


101 
\newbox\ResultBox


102 


103 
% Flags


104 


105 
\newif\if@inferRule % whether \@infer draws a rule.


106 
\newif\if@DoubleRule % whether \@infer draws doulbe rules.


107 
\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.


108 
\newif\if@MathSaved % whether inner math mode where \infer or


109 
% \deduce appears.


110 


111 
% Special Fonts


112 


113 
\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@


114 
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}


115 


116 
% Math Save Macros


117 
%


118 
% \@SaveMath is called in the very begining of toplevel macros


119 
% which are \infer and \deduce.


120 
% \@RestoreMath is called in the very last before toplevel macros end.


121 
% Remark \infer and \deduce ends calling \@infer.


122 


123 
\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner


124 
\relax $\relax \@MathSavedtrue \fi\fi }


125 


126 
\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }


127 


128 
% Macros


129 


130 
\def\@Ifnextchar#1#2#3{\let\@tempe=#1\def\@tempa{#2}\def\@tempb{#3}\futurelet


131 
\@tempc\@ifnch}


132 
% It can compare an = character, though the one in latex.tex cannot.


133 


134 
\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax


135 
\ifx \@tempa \@tempb #2\else #3\fi }


136 


137 
\def\infer{\@SaveMath \@Ifnextchar *{\@inferSteps}{\relax


138 
\@Ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}


139 


140 
\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse


141 
\@Ifnextchar [{\@infer}{\@infer[\@empty]}}


142 


143 
\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue


144 
\@Ifnextchar [{\@infer}{\@infer[\@empty]}}


145 


146 
\def\@inferSteps*{\@Ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}


147 


148 
\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}


149 


150 
\def\deduce{\@SaveMath \@Ifnextchar [{\@deduce{\@empty}}


151 
{\@inferRulefalse \@infer[\@empty]}}


152 


153 
% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>


154 


155 
\def\@deduce#1[#2]#3#4{\@inferRulefalse


156 
\@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}


157 


158 
% \@infer[<Label>]<Lower><Uppers>


159 
% If \@inferRuletrue, it draws a rule and <Label> is right to


160 
% a rule. In this case, if \@DoubleRuletrue, it draws


161 
% double rules.


162 
%


163 
% Otherwise, draws no rule and <Label> is right to <Lower>.


164 


165 
\def\@infer[#1]#2#3{\relax


166 
% Get parameters


167 
\if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi


168 
\setbox\@LabelPart=\hbox{$#1$}\relax


169 
\setbox\@LowerPart=\hbox{$#2$}\relax


170 
%


171 
\global\@LeftOffset=0pt


172 
\setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax


173 
\global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&


174 
\inferTabSkip


175 
\global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr


176 
#3\cr}}\relax


177 
% Here is a little trick.


178 
% \@ReturnLeftOffsettrue(false) influences on \infer or


179 
% \deduce placed in ## locally


180 
% because of \@SaveMath and \@RestoreMath.


181 
\UpperLeftOffset=\@LeftOffset


182 
\UpperRightOffset=\@RightOffset


183 
% Calculate Adjustments


184 
\LowerWidth=\wd\@LowerPart


185 
\LowerHeight=\ht\@LowerPart


186 
\LowerCenter=0.5\LowerWidth


187 
%


188 
\UpperWidth=\wd\@UpperPart \advance\UpperWidth by \UpperLeftOffset


189 
\advance\UpperWidth by \UpperRightOffset


190 
\UpperCenter=\UpperLeftOffset


191 
\advance\UpperCenter by 0.5\UpperWidth


192 
%


193 
\ifdim \UpperWidth > \LowerWidth


194 
% \UpperCenter > \LowerCenter


195 
\UpperAdjust=0pt


196 
\RuleAdjust=\UpperLeftOffset


197 
\LowerAdjust=\UpperCenter \advance\LowerAdjust by \LowerCenter


198 
\RuleWidth=\UpperWidth


199 
\global\@LeftOffset=\LowerAdjust


200 
%


201 
\else % \UpperWidth <= \LowerWidth


202 
\ifdim \UpperCenter > \LowerCenter


203 
%


204 
\UpperAdjust=0pt


205 
\RuleAdjust=\UpperCenter \advance\RuleAdjust by \LowerCenter


206 
\LowerAdjust=\RuleAdjust


207 
\RuleWidth=\LowerWidth


208 
\global\@LeftOffset=\LowerAdjust


209 
%


210 
\else % \UpperWidth <= \LowerWidth


211 
% \UpperCenter <= \LowerCenter


212 
%


213 
\UpperAdjust=\LowerCenter \advance\UpperAdjust by \UpperCenter


214 
\RuleAdjust=0pt


215 
\LowerAdjust=0pt


216 
\RuleWidth=\LowerWidth


217 
\global\@LeftOffset=0pt


218 
%


219 
\fi\fi


220 
% Make a box


221 
\if@inferRule


222 
%


223 
\setbox\ResultBox=\vbox{


224 
\moveright \UpperAdjust \box\@UpperPart


225 
\nointerlineskip \kern\inferLineSkip


226 
\if@DoubleRule


227 
\moveright \RuleAdjust \vbox{\hrule width\RuleWidth


228 
\kern 1pt\hrule width\RuleWidth}\relax


229 
\else


230 
\moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax


231 
\fi


232 
\nointerlineskip \kern\inferLineSkip


233 
\moveright \LowerAdjust \box\@LowerPart }\relax


234 
%


235 
\@ifEmpty{#1}{}{\relax


236 
%


237 
\HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by \RuleAdjust


238 
\advance\HLabelAdjust by \RuleWidth


239 
\WidthAdjust=\HLabelAdjust


240 
\advance\WidthAdjust by \inferLabelSkip


241 
\advance\WidthAdjust by \wd\@LabelPart


242 
\ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi


243 
%


244 
\VLabelAdjust=\dp\@LabelPart


245 
\advance\VLabelAdjust by \ht\@LabelPart


246 
\VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight


247 
\advance\VLabelAdjust by \inferLineSkip


248 
%


249 
\setbox\ResultBox=\hbox{\box\ResultBox


250 
\kern \HLabelAdjust \kern\inferLabelSkip


251 
\raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax


252 
%


253 
}\relax % end @ifEmpty


254 
%


255 
\else % \@inferRulefalse


256 
%


257 
\setbox\ResultBox=\vbox{


258 
\moveright \UpperAdjust \box\@UpperPart


259 
\nointerlineskip \kern\inferLineSkip


260 
\moveright \LowerAdjust \hbox{\unhbox\@LowerPart


261 
\@ifEmpty{#1}{}{\relax


262 
\kern\inferLabelSkip \unhbox\@LabelPart}}}\relax


263 
\fi


264 
%


265 
\global\@RightOffset=\wd\ResultBox


266 
\global\advance\@RightOffset by \@LeftOffset


267 
\global\advance\@RightOffset by \LowerWidth


268 
\if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi


269 
%


270 
\box\ResultBox


271 
\@RestoreMath


272 
}
