
paulson@3126: \ProvidesPackage{proof}[1995/05/22]
paulson@3126: %       proof.sty       (Proof Figure Macros)
berghofe@3095: %
paulson@3126: %       version 2.0
paulson@3126: %       June 24, 1991
paulson@3126: %       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
paulson@3126: %
paulson@3126: %Modified for LaTeX-2e by L. C. Paulson
berghofe@3095: % 
berghofe@3095: % This program is free software; you can redistribute it or modify
berghofe@3095: % it under the terms of the GNU General Public License as published by
berghofe@3095: % the Free Software Foundation; either versions 1, or (at your option)
berghofe@3095: % any later version.
berghofe@3095: % 
berghofe@3095: % This program is distributed in the hope that it will be useful
berghofe@3095: % but WITHOUT ANY WARRANTY; without even the implied warranty of
berghofe@3095: % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
berghofe@3095: % GNU General Public License for more details.
berghofe@3095: %
paulson@3126: %       Usage:
paulson@3126: %               In \documentstyle, specify an optional style `proof', say,
paulson@3126: %                       \documentstyle[proof]{article}.
berghofe@3095: %
paulson@3126: %       The following macros are available:
berghofe@3095: %
paulson@3126: %       In all the following macros, all the arguments such as
paulson@3126: %       <Lowers> and <Uppers> are processed in math mode.
berghofe@3095: %
paulson@3126: %       \infer<Lower><Uppers>
paulson@3126: %               draws an inference.
berghofe@3095: %
paulson@3126: %               Use & in <Uppers> to delimit upper formulae.
paulson@3126: %               <Uppers> consists more than 0 formulae.
berghofe@3095: %
paulson@3126: %               \infer returns \hbox{ ... } or \vbox{ ... } and
paulson@3126: %               sets \@LeftOffset and \@RightOffset globally.
berghofe@3095: %
paulson@3126: %       \infer[<Label>]<Lower><Uppers>
paulson@3126: %               draws an inference labeled with <Label>.
berghofe@3095: %
paulson@3126: %       \infer*<Lower><Uppers>
paulson@3126: %               draws a many step deduction.
berghofe@3095: %
paulson@3126: %       \infer*[<Label>]<Lower><Uppers>
paulson@3126: %               draws a many step deduction labeled with <Label>.
berghofe@3095: %
paulson@3126: %       \infer=<Lower><Uppers>
paulson@3126: %               draws a double-ruled deduction.
berghofe@3095: %
paulson@3126: %       \infer=[<Label>]<Lower><Uppers>
paulson@3126: %               draws a double-ruled deduction labeled with <Label>.
berghofe@3095: %
paulson@3126: %       \deduce<Lower><Uppers>
paulson@3126: %               draws an inference without a rule.
paulson@3126: %
paulson@3126: %       \deduce[<Proof>]<Lower><Uppers>
paulson@3126: %               draws a many step deduction with a proof name.
paulson@3126: %
paulson@3126: %       Example:
paulson@3126: %               If you want to write
paulson@3126: %                           B C
paulson@3126: %                          -----
paulson@3126: %                      A     D
paulson@3126: %                     ----------
paulson@3126: %                         E
paulson@3126: %       use
paulson@3126: %               \infer{E}{
paulson@3126: %                       A
paulson@3126: %                       &
paulson@3126: %                       \infer{D}{B & C}
paulson@3126: %               }
berghofe@3095: %
berghofe@3095: 
paulson@3126: %       Style Parameters
berghofe@3095: 
paulson@3126: \newdimen\inferLineSkip         \inferLineSkip=2pt
paulson@3126: \newdimen\inferLabelSkip        \inferLabelSkip=5pt
berghofe@3095: \def\inferTabSkip{\quad}
berghofe@3095: 
paulson@3126: %       Variables
berghofe@3095: 
paulson@3126: \newdimen\@LeftOffset   % global
paulson@3126: \newdimen\@RightOffset  % global
paulson@3126: \newdimen\@SavedLeftOffset      % safe from users
berghofe@3095: 
berghofe@3095: \newdimen\UpperWidth
berghofe@3095: \newdimen\LowerWidth
berghofe@3095: \newdimen\LowerHeight
berghofe@3095: \newdimen\UpperLeftOffset
berghofe@3095: \newdimen\UpperRightOffset
berghofe@3095: \newdimen\UpperCenter
berghofe@3095: \newdimen\LowerCenter
berghofe@3095: \newdimen\UpperAdjust
berghofe@3095: \newdimen\RuleAdjust
berghofe@3095: \newdimen\LowerAdjust
berghofe@3095: \newdimen\RuleWidth
berghofe@3095: \newdimen\HLabelAdjust
berghofe@3095: \newdimen\VLabelAdjust
berghofe@3095: \newdimen\WidthAdjust
berghofe@3095: 
berghofe@3095: \newbox\@UpperPart
berghofe@3095: \newbox\@LowerPart
berghofe@3095: \newbox\@LabelPart
berghofe@3095: \newbox\ResultBox
berghofe@3095: 
paulson@3126: %       Flags
berghofe@3095: 
paulson@3126: \newif\if@inferRule     % whether \@infer draws a rule.
paulson@3126: \newif\if@DoubleRule    % whether \@infer draws doulbe rules.
paulson@3126: \newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
paulson@3126: \newif\if@MathSaved     % whether inner math mode where \infer or
paulson@3126:                         % \deduce appears.
berghofe@3095: 
paulson@3126: %       Special Fonts
berghofe@3095: 
berghofe@3095: \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
berghofe@3095:     \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
berghofe@3095: 
paulson@3126: %       Math Save Macros
berghofe@3095: %
paulson@3126: %       \@SaveMath is called in the very begining of toplevel macros
paulson@3126: %       which are \infer and \deduce.
paulson@3126: %       \@RestoreMath is called in the very last before toplevel macros end.
paulson@3126: %       Remark \infer and \deduce ends calling \@infer.
paulson@3126: %TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty"
berghofe@3095: 
paulson@3126: \def\@SaveMath{}
berghofe@3095: 
paulson@3126: \def\@RestoreMath{}
berghofe@3095: 
paulson@3126: %       Macros
berghofe@3095: 
berghofe@3095: \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
paulson@3126:         \ifx \@tempa \@tempb #2\else #3\fi }
berghofe@3095: 
paulson@3126: \def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax
paulson@3126:         \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
berghofe@3095: 
paulson@3126: \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
paulson@3126:         \@ifnextchar [{\@infer}{\@infer[\@empty]}}
paulson@3126: 
paulson@3126: \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
paulson@3126:         \@ifnextchar [{\@infer}{\@infer[\@empty]}}
berghofe@3095: 
berghofe@3095: \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
berghofe@3095: 
berghofe@3095: \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
berghofe@3095: 
berghofe@3095: \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
paulson@3126:         {\@inferRulefalse \@infer[\@empty]}}
berghofe@3095: 
paulson@3126: %       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
berghofe@3095: 
berghofe@3095: \def\@deduce#1[#2]#3#4{\@inferRulefalse
paulson@3126:         \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
berghofe@3095: 
paulson@3126: %       \@infer[<Label>]<Lower><Uppers>
paulson@3126: %               If \@inferRuletrue, it draws a rule and <Label> is right to
paulson@3126: %               a rule. In this case, if \@DoubleRuletrue, it draws
paulson@3126: %               double rules.
paulson@3126: %
paulson@3126: %               Otherwise, draws no rule and <Label> is right to <Lower>.
berghofe@3095: 
berghofe@3095: \def\@infer[#1]#2#3{\relax
berghofe@3095: % Get parameters
paulson@3126:         \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
paulson@3126:         \setbox\@LabelPart=\hbox{$#1$}\relax
paulson@3126:         \setbox\@LowerPart=\hbox{$#2$}\relax
berghofe@3095: %
paulson@3126:         \global\@LeftOffset=0pt
paulson@3126:         \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
paulson@3126:                 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
paulson@3126:                 \inferTabSkip
paulson@3126:                 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
paulson@3126:                 #3\cr}}\relax
paulson@3126: %                       Here is a little trick.
paulson@3126: %                       \@ReturnLeftOffsettrue(false) influences on \infer or
paulson@3126: %                       \deduce placed in ## locally
paulson@3126: %                       because of \@SaveMath and \@RestoreMath.
paulson@3126:         \UpperLeftOffset=\@LeftOffset
paulson@3126:         \UpperRightOffset=\@RightOffset
berghofe@3095: % Calculate Adjustments
paulson@3126:         \LowerWidth=\wd\@LowerPart
paulson@3126:         \LowerHeight=\ht\@LowerPart
paulson@3126:         \LowerCenter=0.5\LowerWidth
berghofe@3095: %
paulson@3126:         \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
paulson@3126:         \advance\UpperWidth by -\UpperRightOffset
paulson@3126:         \UpperCenter=\UpperLeftOffset
paulson@3126:         \advance\UpperCenter by 0.5\UpperWidth
berghofe@3095: %
paulson@3126:         \ifdim \UpperWidth > \LowerWidth
paulson@3126:                 % \UpperCenter > \LowerCenter
paulson@3126:         \UpperAdjust=0pt
paulson@3126:         \RuleAdjust=\UpperLeftOffset
paulson@3126:         \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
paulson@3126:         \RuleWidth=\UpperWidth
paulson@3126:         \global\@LeftOffset=\LowerAdjust
berghofe@3095: %
paulson@3126:         \else   % \UpperWidth <= \LowerWidth
paulson@3126:         \ifdim \UpperCenter > \LowerCenter
berghofe@3095: %
paulson@3126:         \UpperAdjust=0pt
paulson@3126:         \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
paulson@3126:         \LowerAdjust=\RuleAdjust
paulson@3126:         \RuleWidth=\LowerWidth
paulson@3126:         \global\@LeftOffset=\LowerAdjust
berghofe@3095: %
paulson@3126:         \else   % \UpperWidth <= \LowerWidth
paulson@3126:                 % \UpperCenter <= \LowerCenter
berghofe@3095: %
paulson@3126:         \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
paulson@3126:         \RuleAdjust=0pt
paulson@3126:         \LowerAdjust=0pt
paulson@3126:         \RuleWidth=\LowerWidth
paulson@3126:         \global\@LeftOffset=0pt
berghofe@3095: %
paulson@3126:         \fi\fi
berghofe@3095: % Make a box
paulson@3126:         \if@inferRule
berghofe@3095: %
paulson@3126:         \setbox\ResultBox=\vbox{
paulson@3126:                 \moveright \UpperAdjust \box\@UpperPart
paulson@3126:                 \nointerlineskip \kern\inferLineSkip
paulson@3126:                 \if@DoubleRule
paulson@3126:                 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
paulson@3126:                         \kern 1pt\hrule width\RuleWidth}\relax
paulson@3126:                 \else
paulson@3126:                 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
paulson@3126:                 \fi
paulson@3126:                 \nointerlineskip \kern\inferLineSkip
paulson@3126:                 \moveright \LowerAdjust \box\@LowerPart }\relax
berghofe@3095: %
paulson@3126:         \@ifEmpty{#1}{}{\relax
berghofe@3095: %
paulson@3126:         \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
paulson@3126:         \advance\HLabelAdjust by -\RuleWidth
paulson@3126:         \WidthAdjust=\HLabelAdjust
paulson@3126:         \advance\WidthAdjust by -\inferLabelSkip
paulson@3126:         \advance\WidthAdjust by -\wd\@LabelPart
paulson@3126:         \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
berghofe@3095: %
paulson@3126:         \VLabelAdjust=\dp\@LabelPart
paulson@3126:         \advance\VLabelAdjust by -\ht\@LabelPart
paulson@3126:         \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
paulson@3126:         \advance\VLabelAdjust by \inferLineSkip
berghofe@3095: %
paulson@3126:         \setbox\ResultBox=\hbox{\box\ResultBox
paulson@3126:                 \kern -\HLabelAdjust \kern\inferLabelSkip
paulson@3126:                 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
berghofe@3095: %
paulson@3126:         }\relax % end @ifEmpty
berghofe@3095: %
paulson@3126:         \else % \@inferRulefalse
berghofe@3095: %
paulson@3126:         \setbox\ResultBox=\vbox{
paulson@3126:                 \moveright \UpperAdjust \box\@UpperPart
paulson@3126:                 \nointerlineskip \kern\inferLineSkip
paulson@3126:                 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
paulson@3126:                         \@ifEmpty{#1}{}{\relax
paulson@3126:                         \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
paulson@3126:         \fi
berghofe@3095: %
paulson@3126:         \global\@RightOffset=\wd\ResultBox
paulson@3126:         \global\advance\@RightOffset by -\@LeftOffset
paulson@3126:         \global\advance\@RightOffset by -\LowerWidth
paulson@3126:         \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
berghofe@3095: %
paulson@3126:         \box\ResultBox
paulson@3126:         \@RestoreMath
berghofe@3095: }
paulson@3126: \endinput




