3095

1 
% proof.sty (Proof Figure Macros)


2 
%


3 
% version 1.0


4 
% October 13, 1990


5 
% Copyright (C) 1990 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 
% \deduce<Lower><Uppers>


45 
% draws an inference without a rule.


46 
%


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


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


49 
%


50 
% Example:


51 
% If you want to write


52 
% B C


53 
% 


54 
% A D


55 
% 


56 
% E


57 
% use


58 
% \infer{E}{


59 
% A


60 
% &


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


62 
% }


63 
%


64 


65 
% Style Parameters


66 


67 
\newdimen\inferLineSkip \inferLineSkip=2pt


68 
\newdimen\inferLabelSkip \inferLabelSkip=5pt


69 
\def\inferTabSkip{\quad}


70 


71 
% Variables


72 


73 
\newdimen\@LeftOffset % global


74 
\newdimen\@RightOffset % global


75 
\newdimen\@SavedLeftOffset % safe from users


76 


77 
\newdimen\UpperWidth


78 
\newdimen\LowerWidth


79 
\newdimen\LowerHeight


80 
\newdimen\UpperLeftOffset


81 
\newdimen\UpperRightOffset


82 
\newdimen\UpperCenter


83 
\newdimen\LowerCenter


84 
\newdimen\UpperAdjust


85 
\newdimen\RuleAdjust


86 
\newdimen\LowerAdjust


87 
\newdimen\RuleWidth


88 
\newdimen\HLabelAdjust


89 
\newdimen\VLabelAdjust


90 
\newdimen\WidthAdjust


91 


92 
\newbox\@UpperPart


93 
\newbox\@LowerPart


94 
\newbox\@LabelPart


95 
\newbox\ResultBox


96 


97 
% Flags


98 


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


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


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


102 
% \deduce appears.


103 


104 
% Special Fonts


105 


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


107 
\vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}


108 


109 
% Math Save Macros


110 
%


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


112 
% which are \infer and \deduce.


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


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


115 


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


117 
\relax $\relax \@MathSavedtrue \fi\fi }


118 


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


120 


121 
% Macros


122 


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


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


125 


126 
\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}


127 


128 
\def\@inferOneStep{\@inferRuletrue


129 
\@ifnextchar [{\@infer}{\@infer[\@empty]}}


130 


131 
\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}


132 


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


134 


135 
\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}


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


137 


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


139 


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


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


142 


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


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


145 
% a rule.


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


147 


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


149 
% Get parameters


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


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


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


153 
%


154 
\global\@LeftOffset=0pt


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


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


157 
\inferTabSkip


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


159 
#3\cr}}\relax


160 
% Here is a little trick.


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


162 
% \deduce placed in ## locally


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


164 
\UpperLeftOffset=\@LeftOffset


165 
\UpperRightOffset=\@RightOffset


166 
% Calculate Adjustments


167 
\LowerWidth=\wd\@LowerPart


168 
\LowerHeight=\ht\@LowerPart


169 
\LowerCenter=0.5\LowerWidth


170 
%


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


172 
\advance\UpperWidth by \UpperRightOffset


173 
\UpperCenter=\UpperLeftOffset


174 
\advance\UpperCenter by 0.5\UpperWidth


175 
%


176 
\ifdim \UpperWidth > \LowerWidth


177 
% \UpperCenter > \LowerCenter


178 
\UpperAdjust=0pt


179 
\RuleAdjust=\UpperLeftOffset


180 
\LowerAdjust=\UpperCenter \advance\LowerAdjust by \LowerCenter


181 
\RuleWidth=\UpperWidth


182 
\global\@LeftOffset=\LowerAdjust


183 
%


184 
\else % \UpperWidth <= \LowerWidth


185 
\ifdim \UpperCenter > \LowerCenter


186 
%


187 
\UpperAdjust=0pt


188 
\RuleAdjust=\UpperCenter \advance\RuleAdjust by \LowerCenter


189 
\LowerAdjust=\RuleAdjust


190 
\RuleWidth=\LowerWidth


191 
\global\@LeftOffset=\LowerAdjust


192 
%


193 
\else % \UpperWidth <= \LowerWidth


194 
% \UpperCenter <= \LowerCenter


195 
%


196 
\UpperAdjust=\LowerCenter \advance\UpperAdjust by \UpperCenter


197 
\RuleAdjust=0pt


198 
\LowerAdjust=0pt


199 
\RuleWidth=\LowerWidth


200 
\global\@LeftOffset=0pt


201 
%


202 
\fi\fi


203 
% Make a box


204 
\if@inferRule


205 
%


206 
\setbox\ResultBox=\vbox{


207 
\moveright \UpperAdjust \box\@UpperPart


208 
\nointerlineskip \kern\inferLineSkip


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


210 
\nointerlineskip \kern\inferLineSkip


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


212 
%


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


214 
%


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


216 
\advance\HLabelAdjust by \RuleWidth


217 
\WidthAdjust=\HLabelAdjust


218 
\advance\WidthAdjust by \inferLabelSkip


219 
\advance\WidthAdjust by \wd\@LabelPart


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


221 
%


222 
\VLabelAdjust=\dp\@LabelPart


223 
\advance\VLabelAdjust by \ht\@LabelPart


224 
\VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight


225 
\advance\VLabelAdjust by \inferLineSkip


226 
%


227 
\setbox\ResultBox=\hbox{\box\ResultBox


228 
\kern \HLabelAdjust \kern\inferLabelSkip


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


230 
%


231 
}\relax % end @ifEmpty


232 
%


233 
\else % \@inferRulefalse


234 
%


235 
\setbox\ResultBox=\vbox{


236 
\moveright \UpperAdjust \box\@UpperPart


237 
\nointerlineskip \kern\inferLineSkip


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


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


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


241 
\fi


242 
%


243 
\global\@RightOffset=\wd\ResultBox


244 
\global\advance\@RightOffset by \@LeftOffset


245 
\global\advance\@RightOffset by \LowerWidth


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


247 
%


248 
\box\ResultBox


249 
\@RestoreMath


250 
}
