1.1 --- a/doc-src/proof.sty Wed May 07 13:51:22 1997 +0200
1.2 +++ b/doc-src/proof.sty Wed May 07 16:26:02 1997 +0200
1.3 @@ -1,8 +1,11 @@
1.4 -% proof.sty (Proof Figure Macros)
1.5 +\ProvidesPackage{proof}[1995/05/22]
1.6 +% proof.sty (Proof Figure Macros)
1.7 %
1.8 -% version 1.0
1.9 -% October 13, 1990
1.10 -% Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
1.11 +% version 2.0
1.12 +% June 24, 1991
1.13 +% Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
1.14 +%
1.15 +%Modified for LaTeX-2e by L. C. Paulson
1.16 %
1.17 % This program is free software; you can redistribute it or modify
1.18 % it under the terms of the GNU General Public License as published by
1.19 @@ -14,65 +17,71 @@
1.20 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
1.21 % GNU General Public License for more details.
1.22 %
1.23 -% Usage:
1.24 -% In \documentstyle, specify an optional style `proof', say,
1.25 -% \documentstyle[proof]{article}.
1.26 +% Usage:
1.27 +% In \documentstyle, specify an optional style `proof', say,
1.28 +% \documentstyle[proof]{article}.
1.29 %
1.30 -% The following macros are available:
1.31 +% The following macros are available:
1.32 %
1.33 -% In all the following macros, all the arguments such as
1.34 -% <Lowers> and <Uppers> are processed in math mode.
1.35 +% In all the following macros, all the arguments such as
1.36 +% <Lowers> and <Uppers> are processed in math mode.
1.37 %
1.38 -% \infer<Lower><Uppers>
1.39 -% draws an inference.
1.40 +% \infer<Lower><Uppers>
1.41 +% draws an inference.
1.42 %
1.43 -% Use & in <Uppers> to delimit upper formulae.
1.44 -% <Uppers> consists more than 0 formulae.
1.45 +% Use & in <Uppers> to delimit upper formulae.
1.46 +% <Uppers> consists more than 0 formulae.
1.47 %
1.48 -% \infer returns \hbox{ ... } or \vbox{ ... } and
1.49 -% sets \@LeftOffset and \@RightOffset globally.
1.50 +% \infer returns \hbox{ ... } or \vbox{ ... } and
1.51 +% sets \@LeftOffset and \@RightOffset globally.
1.52 %
1.53 -% \infer[<Label>]<Lower><Uppers>
1.54 -% draws an inference labeled with <Label>.
1.55 +% \infer[<Label>]<Lower><Uppers>
1.56 +% draws an inference labeled with <Label>.
1.57 %
1.58 -% \infer*<Lower><Uppers>
1.59 -% draws a many step deduction.
1.60 +% \infer*<Lower><Uppers>
1.61 +% draws a many step deduction.
1.62 %
1.63 -% \infer*[<Label>]<Lower><Uppers>
1.64 -% draws a many step deduction labeled with <Label>.
1.65 +% \infer*[<Label>]<Lower><Uppers>
1.66 +% draws a many step deduction labeled with <Label>.
1.67 %
1.68 -% \deduce<Lower><Uppers>
1.69 -% draws an inference without a rule.
1.70 +% \infer=<Lower><Uppers>
1.71 +% draws a double-ruled deduction.
1.72 %
1.73 -% \deduce[<Proof>]<Lower><Uppers>
1.74 -% draws a many step deduction with a proof name.
1.75 +% \infer=[<Label>]<Lower><Uppers>
1.76 +% draws a double-ruled deduction labeled with <Label>.
1.77 %
1.78 -% Example:
1.79 -% If you want to write
1.80 -% B C
1.81 -% -----
1.82 -% A D
1.83 -% ----------
1.84 -% E
1.85 -% use
1.86 -% \infer{E}{
1.87 -% A
1.88 -% &
1.89 -% \infer{D}{B & C}
1.90 -% }
1.91 +% \deduce<Lower><Uppers>
1.92 +% draws an inference without a rule.
1.93 +%
1.94 +% \deduce[<Proof>]<Lower><Uppers>
1.95 +% draws a many step deduction with a proof name.
1.96 +%
1.97 +% Example:
1.98 +% If you want to write
1.99 +% B C
1.100 +% -----
1.101 +% A D
1.102 +% ----------
1.103 +% E
1.104 +% use
1.105 +% \infer{E}{
1.106 +% A
1.107 +% &
1.108 +% \infer{D}{B & C}
1.109 +% }
1.110 %
1.111
1.112 -% Style Parameters
1.113 +% Style Parameters
1.114
1.115 -\newdimen\inferLineSkip \inferLineSkip=2pt
1.116 -\newdimen\inferLabelSkip \inferLabelSkip=5pt
1.117 +\newdimen\inferLineSkip \inferLineSkip=2pt
1.118 +\newdimen\inferLabelSkip \inferLabelSkip=5pt
1.119 \def\inferTabSkip{\quad}
1.120
1.121 -% Variables
1.122 +% Variables
1.123
1.124 -\newdimen\@LeftOffset % global
1.125 -\newdimen\@RightOffset % global
1.126 -\newdimen\@SavedLeftOffset % safe from users
1.127 +\newdimen\@LeftOffset % global
1.128 +\newdimen\@RightOffset % global
1.129 +\newdimen\@SavedLeftOffset % safe from users
1.130
1.131 \newdimen\UpperWidth
1.132 \newdimen\LowerWidth
1.133 @@ -94,157 +103,170 @@
1.134 \newbox\@LabelPart
1.135 \newbox\ResultBox
1.136
1.137 -% Flags
1.138 +% Flags
1.139
1.140 -\newif\if@inferRule % whether \@infer draws a rule.
1.141 -\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
1.142 -\newif\if@MathSaved % whether inner math mode where \infer or
1.143 - % \deduce appears.
1.144 +\newif\if@inferRule % whether \@infer draws a rule.
1.145 +\newif\if@DoubleRule % whether \@infer draws doulbe rules.
1.146 +\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
1.147 +\newif\if@MathSaved % whether inner math mode where \infer or
1.148 + % \deduce appears.
1.149
1.150 -% Special Fonts
1.151 +% Special Fonts
1.152
1.153 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
1.154 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
1.155
1.156 -% Math Save Macros
1.157 +% Math Save Macros
1.158 %
1.159 -% \@SaveMath is called in the very begining of toplevel macros
1.160 -% which are \infer and \deduce.
1.161 -% \@RestoreMath is called in the very last before toplevel macros end.
1.162 -% Remark \infer and \deduce ends calling \@infer.
1.163 +% \@SaveMath is called in the very begining of toplevel macros
1.164 +% which are \infer and \deduce.
1.165 +% \@RestoreMath is called in the very last before toplevel macros end.
1.166 +% Remark \infer and \deduce ends calling \@infer.
1.167 +%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
1.168
1.169 -\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
1.170 - \relax $\relax \@MathSavedtrue \fi\fi }
1.171 +\def\@SaveMath{}
1.172
1.173 -\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
1.174 +\def\@RestoreMath{}
1.175
1.176 -% Macros
1.177 +% Macros
1.178
1.179 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
1.180 - \ifx \@tempa \@tempb #2\else #3\fi }
1.181 + \ifx \@tempa \@tempb #2\else #3\fi }
1.182
1.183 -\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
1.184 +\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
1.185 + \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
1.186
1.187 -\def\@inferOneStep{\@inferRuletrue
1.188 - \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.189 +\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
1.190 + \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.191 +
1.192 +\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
1.193 + \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.194
1.195 \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
1.196
1.197 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
1.198
1.199 \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
1.200 - {\@inferRulefalse \@infer[\@empty]}}
1.201 + {\@inferRulefalse \@infer[\@empty]}}
1.202
1.203 -% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
1.204 +% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
1.205
1.206 \def\@deduce#1[#2]#3#4{\@inferRulefalse
1.207 - \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
1.208 + \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
1.209
1.210 -% \@infer[<Label>]<Lower><Uppers>
1.211 -% If \@inferRuletrue, draws a rule and <Label> is right to
1.212 -% a rule.
1.213 -% Otherwise, draws no rule and <Label> is right to <Lower>.
1.214 +% \@infer[<Label>]<Lower><Uppers>
1.215 +% If \@inferRuletrue, it draws a rule and <Label> is right to
1.216 +% a rule. In this case, if \@DoubleRuletrue, it draws
1.217 +% double rules.
1.218 +%
1.219 +% Otherwise, draws no rule and <Label> is right to <Lower>.
1.220
1.221 \def\@infer[#1]#2#3{\relax
1.222 % Get parameters
1.223 - \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
1.224 - \setbox\@LabelPart=\hbox{$#1$}\relax
1.225 - \setbox\@LowerPart=\hbox{$#2$}\relax
1.226 + \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
1.227 + \setbox\@LabelPart=\hbox{$#1$}\relax
1.228 + \setbox\@LowerPart=\hbox{$#2$}\relax
1.229 %
1.230 - \global\@LeftOffset=0pt
1.231 - \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
1.232 - \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
1.233 - \inferTabSkip
1.234 - \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
1.235 - #3\cr}}\relax
1.236 -% Here is a little trick.
1.237 -% \@ReturnLeftOffsettrue(false) influences on \infer or
1.238 -% \deduce placed in ## locally
1.239 -% because of \@SaveMath and \@RestoreMath.
1.240 - \UpperLeftOffset=\@LeftOffset
1.241 - \UpperRightOffset=\@RightOffset
1.242 + \global\@LeftOffset=0pt
1.243 + \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
1.244 + \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
1.245 + \inferTabSkip
1.246 + \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
1.247 + #3\cr}}\relax
1.248 +% Here is a little trick.
1.249 +% \@ReturnLeftOffsettrue(false) influences on \infer or
1.250 +% \deduce placed in ## locally
1.251 +% because of \@SaveMath and \@RestoreMath.
1.252 + \UpperLeftOffset=\@LeftOffset
1.253 + \UpperRightOffset=\@RightOffset
1.254 % Calculate Adjustments
1.255 - \LowerWidth=\wd\@LowerPart
1.256 - \LowerHeight=\ht\@LowerPart
1.257 - \LowerCenter=0.5\LowerWidth
1.258 + \LowerWidth=\wd\@LowerPart
1.259 + \LowerHeight=\ht\@LowerPart
1.260 + \LowerCenter=0.5\LowerWidth
1.261 %
1.262 - \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
1.263 - \advance\UpperWidth by -\UpperRightOffset
1.264 - \UpperCenter=\UpperLeftOffset
1.265 - \advance\UpperCenter by 0.5\UpperWidth
1.266 + \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
1.267 + \advance\UpperWidth by -\UpperRightOffset
1.268 + \UpperCenter=\UpperLeftOffset
1.269 + \advance\UpperCenter by 0.5\UpperWidth
1.270 %
1.271 - \ifdim \UpperWidth > \LowerWidth
1.272 - % \UpperCenter > \LowerCenter
1.273 - \UpperAdjust=0pt
1.274 - \RuleAdjust=\UpperLeftOffset
1.275 - \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
1.276 - \RuleWidth=\UpperWidth
1.277 - \global\@LeftOffset=\LowerAdjust
1.278 + \ifdim \UpperWidth > \LowerWidth
1.279 + % \UpperCenter > \LowerCenter
1.280 + \UpperAdjust=0pt
1.281 + \RuleAdjust=\UpperLeftOffset
1.282 + \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
1.283 + \RuleWidth=\UpperWidth
1.284 + \global\@LeftOffset=\LowerAdjust
1.285 %
1.286 - \else % \UpperWidth <= \LowerWidth
1.287 - \ifdim \UpperCenter > \LowerCenter
1.288 + \else % \UpperWidth <= \LowerWidth
1.289 + \ifdim \UpperCenter > \LowerCenter
1.290 %
1.291 - \UpperAdjust=0pt
1.292 - \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
1.293 - \LowerAdjust=\RuleAdjust
1.294 - \RuleWidth=\LowerWidth
1.295 - \global\@LeftOffset=\LowerAdjust
1.296 + \UpperAdjust=0pt
1.297 + \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
1.298 + \LowerAdjust=\RuleAdjust
1.299 + \RuleWidth=\LowerWidth
1.300 + \global\@LeftOffset=\LowerAdjust
1.301 %
1.302 - \else % \UpperWidth <= \LowerWidth
1.303 - % \UpperCenter <= \LowerCenter
1.304 + \else % \UpperWidth <= \LowerWidth
1.305 + % \UpperCenter <= \LowerCenter
1.306 %
1.307 - \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
1.308 - \RuleAdjust=0pt
1.309 - \LowerAdjust=0pt
1.310 - \RuleWidth=\LowerWidth
1.311 - \global\@LeftOffset=0pt
1.312 + \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
1.313 + \RuleAdjust=0pt
1.314 + \LowerAdjust=0pt
1.315 + \RuleWidth=\LowerWidth
1.316 + \global\@LeftOffset=0pt
1.317 %
1.318 - \fi\fi
1.319 + \fi\fi
1.320 % Make a box
1.321 - \if@inferRule
1.322 + \if@inferRule
1.323 %
1.324 - \setbox\ResultBox=\vbox{
1.325 - \moveright \UpperAdjust \box\@UpperPart
1.326 - \nointerlineskip \kern\inferLineSkip
1.327 - \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
1.328 - \nointerlineskip \kern\inferLineSkip
1.329 - \moveright \LowerAdjust \box\@LowerPart }\relax
1.330 + \setbox\ResultBox=\vbox{
1.331 + \moveright \UpperAdjust \box\@UpperPart
1.332 + \nointerlineskip \kern\inferLineSkip
1.333 + \if@DoubleRule
1.334 + \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
1.335 + \kern 1pt\hrule width\RuleWidth}\relax
1.336 + \else
1.337 + \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
1.338 + \fi
1.339 + \nointerlineskip \kern\inferLineSkip
1.340 + \moveright \LowerAdjust \box\@LowerPart }\relax
1.341 %
1.342 - \@ifEmpty{#1}{}{\relax
1.343 + \@ifEmpty{#1}{}{\relax
1.344 %
1.345 - \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
1.346 - \advance\HLabelAdjust by -\RuleWidth
1.347 - \WidthAdjust=\HLabelAdjust
1.348 - \advance\WidthAdjust by -\inferLabelSkip
1.349 - \advance\WidthAdjust by -\wd\@LabelPart
1.350 - \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
1.351 + \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
1.352 + \advance\HLabelAdjust by -\RuleWidth
1.353 + \WidthAdjust=\HLabelAdjust
1.354 + \advance\WidthAdjust by -\inferLabelSkip
1.355 + \advance\WidthAdjust by -\wd\@LabelPart
1.356 + \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
1.357 %
1.358 - \VLabelAdjust=\dp\@LabelPart
1.359 - \advance\VLabelAdjust by -\ht\@LabelPart
1.360 - \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
1.361 - \advance\VLabelAdjust by \inferLineSkip
1.362 + \VLabelAdjust=\dp\@LabelPart
1.363 + \advance\VLabelAdjust by -\ht\@LabelPart
1.364 + \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
1.365 + \advance\VLabelAdjust by \inferLineSkip
1.366 %
1.367 - \setbox\ResultBox=\hbox{\box\ResultBox
1.368 - \kern -\HLabelAdjust \kern\inferLabelSkip
1.369 - \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
1.370 + \setbox\ResultBox=\hbox{\box\ResultBox
1.371 + \kern -\HLabelAdjust \kern\inferLabelSkip
1.372 + \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
1.373 %
1.374 - }\relax % end @ifEmpty
1.375 + }\relax % end @ifEmpty
1.376 %
1.377 - \else % \@inferRulefalse
1.378 + \else % \@inferRulefalse
1.379 %
1.380 - \setbox\ResultBox=\vbox{
1.381 - \moveright \UpperAdjust \box\@UpperPart
1.382 - \nointerlineskip \kern\inferLineSkip
1.383 - \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
1.384 - \@ifEmpty{#1}{}{\relax
1.385 - \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
1.386 - \fi
1.387 + \setbox\ResultBox=\vbox{
1.388 + \moveright \UpperAdjust \box\@UpperPart
1.389 + \nointerlineskip \kern\inferLineSkip
1.390 + \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
1.391 + \@ifEmpty{#1}{}{\relax
1.392 + \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
1.393 + \fi
1.394 %
1.395 - \global\@RightOffset=\wd\ResultBox
1.396 - \global\advance\@RightOffset by -\@LeftOffset
1.397 - \global\advance\@RightOffset by -\LowerWidth
1.398 - \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
1.399 + \global\@RightOffset=\wd\ResultBox
1.400 + \global\advance\@RightOffset by -\@LeftOffset
1.401 + \global\advance\@RightOffset by -\LowerWidth
1.402 + \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
1.403 %
1.404 - \box\ResultBox
1.405 - \@RestoreMath
1.406 + \box\ResultBox
1.407 + \@RestoreMath
1.408 }
1.409 +\endinput