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}. paulson@3126: % paulson@3126: % The following macros are available: berghofe@3095: % paulson@3126: % In all the following macros, all the arguments such as paulson@3126: % and are processed in math mode. berghofe@3095: % paulson@3126: % \infer paulson@3126: % draws an inference. berghofe@3095: % paulson@3126: % Use & in to delimit upper formulae. paulson@3126: % 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[] paulson@3126: % draws an inference labeled with . berghofe@3095: % paulson@3126: % \infer* paulson@3126: % draws a many step deduction. berghofe@3095: % paulson@3126: % \infer*[] paulson@3126: % draws a many step deduction labeled with . berghofe@3095: % paulson@3126: % \infer= paulson@3126: % draws a double-ruled deduction. berghofe@3095: % paulson@3126: % \infer=[] paulson@3126: % draws a double-ruled deduction labeled with . berghofe@3095: % paulson@3126: % \deduce paulson@3126: % draws an inference without a rule. berghofe@3095: % paulson@3126: % \deduce[] 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 } paulson@3126: 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]}} berghofe@3095: 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[] 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[] paulson@3126: % If \@inferRuletrue, it draws a rule and 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 is right to . 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 paulson@3126: % 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 paulson@3126: % 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