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