1 \ProvidesPackage{proof}[1995/05/22]
2 % proof.sty (Proof Figure Macros)
6 % Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
8 %Modified for LaTeX-2e by L. C. Paulson
10 % This program is free software; you can redistribute it or modify
11 % it under the terms of the GNU General Public License as published by
12 % the Free Software Foundation; either versions 1, or (at your option)
15 % This program is distributed in the hope that it will be useful
16 % but WITHOUT ANY WARRANTY; without even the implied warranty of
17 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18 % GNU General Public License for more details.
21 % In \documentstyle, specify an optional style `proof', say,
22 % \documentstyle[proof]{article}.
24 % The following macros are available:
26 % In all the following macros, all the arguments such as
27 % <Lowers> and <Uppers> are processed in math mode.
29 % \infer<Lower><Uppers>
32 % Use & in <Uppers> to delimit upper formulae.
33 % <Uppers> consists more than 0 formulae.
35 % \infer returns \hbox{ ... } or \vbox{ ... } and
36 % sets \@LeftOffset and \@RightOffset globally.
38 % \infer[<Label>]<Lower><Uppers>
39 % draws an inference labeled with <Label>.
41 % \infer*<Lower><Uppers>
42 % draws a many step deduction.
44 % \infer*[<Label>]<Lower><Uppers>
45 % draws a many step deduction labeled with <Label>.
47 % \infer=<Lower><Uppers>
48 % draws a double-ruled deduction.
50 % \infer=[<Label>]<Lower><Uppers>
51 % draws a double-ruled deduction labeled with <Label>.
53 % \deduce<Lower><Uppers>
54 % draws an inference without a rule.
56 % \deduce[<Proof>]<Lower><Uppers>
57 % draws a many step deduction with a proof name.
60 % If you want to write
76 \newdimen\inferLineSkip \inferLineSkip=2pt
77 \newdimen\inferLabelSkip \inferLabelSkip=5pt
78 \def\inferTabSkip{\quad}
82 \newdimen\@LeftOffset % global
83 \newdimen\@RightOffset % global
84 \newdimen\@SavedLeftOffset % safe from users
89 \newdimen\UpperLeftOffset
90 \newdimen\UpperRightOffset
97 \newdimen\HLabelAdjust
98 \newdimen\VLabelAdjust
108 \newif\if@inferRule % whether \@infer draws a rule.
109 \newif\if@DoubleRule % whether \@infer draws doulbe rules.
110 \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
111 \newif\if@MathSaved % whether inner math mode where \infer or
116 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
117 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
121 % \@SaveMath is called in the very begining of toplevel macros
122 % which are \infer and \deduce.
123 % \@RestoreMath is called in the very last before toplevel macros end.
124 % Remark \infer and \deduce ends calling \@infer.
125 %TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
133 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
134 \ifx \@tempa \@tempb #2\else #3\fi }
136 \def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
137 \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
139 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
140 \@ifnextchar [{\@infer}{\@infer[\@empty]}}
142 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
143 \@ifnextchar [{\@infer}{\@infer[\@empty]}}
145 \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
147 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
149 \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
150 {\@inferRulefalse \@infer[\@empty]}}
152 % \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
154 \def\@deduce#1[#2]#3#4{\@inferRulefalse
155 \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
157 % \@infer[<Label>]<Lower><Uppers>
158 % If \@inferRuletrue, it draws a rule and <Label> is right to
159 % a rule. In this case, if \@DoubleRuletrue, it draws
162 % Otherwise, draws no rule and <Label> is right to <Lower>.
164 \def\@infer[#1]#2#3{\relax
166 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
167 \setbox\@LabelPart=\hbox{$#1$}\relax
168 \setbox\@LowerPart=\hbox{$#2$}\relax
170 \global\@LeftOffset=0pt
171 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
172 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
174 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
176 % Here is a little trick.
177 % \@ReturnLeftOffsettrue(false) influences on \infer or
178 % \deduce placed in ## locally
179 % because of \@SaveMath and \@RestoreMath.
180 \UpperLeftOffset=\@LeftOffset
181 \UpperRightOffset=\@RightOffset
182 % Calculate Adjustments
183 \LowerWidth=\wd\@LowerPart
184 \LowerHeight=\ht\@LowerPart
185 \LowerCenter=0.5\LowerWidth
187 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
188 \advance\UpperWidth by -\UpperRightOffset
189 \UpperCenter=\UpperLeftOffset
190 \advance\UpperCenter by 0.5\UpperWidth
192 \ifdim \UpperWidth > \LowerWidth
193 % \UpperCenter > \LowerCenter
195 \RuleAdjust=\UpperLeftOffset
196 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
197 \RuleWidth=\UpperWidth
198 \global\@LeftOffset=\LowerAdjust
200 \else % \UpperWidth <= \LowerWidth
201 \ifdim \UpperCenter > \LowerCenter
204 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
205 \LowerAdjust=\RuleAdjust
206 \RuleWidth=\LowerWidth
207 \global\@LeftOffset=\LowerAdjust
209 \else % \UpperWidth <= \LowerWidth
210 % \UpperCenter <= \LowerCenter
212 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
215 \RuleWidth=\LowerWidth
216 \global\@LeftOffset=0pt
222 \setbox\ResultBox=\vbox{
223 \moveright \UpperAdjust \box\@UpperPart
224 \nointerlineskip \kern\inferLineSkip
226 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
227 \kern 1pt\hrule width\RuleWidth}\relax
229 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
231 \nointerlineskip \kern\inferLineSkip
232 \moveright \LowerAdjust \box\@LowerPart }\relax
234 \@ifEmpty{#1}{}{\relax
236 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
237 \advance\HLabelAdjust by -\RuleWidth
238 \WidthAdjust=\HLabelAdjust
239 \advance\WidthAdjust by -\inferLabelSkip
240 \advance\WidthAdjust by -\wd\@LabelPart
241 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
243 \VLabelAdjust=\dp\@LabelPart
244 \advance\VLabelAdjust by -\ht\@LabelPart
245 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
246 \advance\VLabelAdjust by \inferLineSkip
248 \setbox\ResultBox=\hbox{\box\ResultBox
249 \kern -\HLabelAdjust \kern\inferLabelSkip
250 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
252 }\relax % end @ifEmpty
254 \else % \@inferRulefalse
256 \setbox\ResultBox=\vbox{
257 \moveright \UpperAdjust \box\@UpperPart
258 \nointerlineskip \kern\inferLineSkip
259 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
260 \@ifEmpty{#1}{}{\relax
261 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
264 \global\@RightOffset=\wd\ResultBox
265 \global\advance\@RightOffset by -\@LeftOffset
266 \global\advance\@RightOffset by -\LowerWidth
267 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi