% proof.sty (Proof Figure Macros) % % version 1.0 % October 13, 1990 % Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp) % % 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>. % % \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} % } %
\newif\if@inferRule % whether \@infer draws a rule. \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. \newif\if@MathSaved % whether inner math mode where \infer or % \deduce appears.
% 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.
% \@infer[<Label>]<Lower><Uppers> % If \@inferRuletrue, draws a rule and <Label> is right to % a rule. % 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 \moveright\RuleAdjust\vbox{\hrule width\RuleWidth}\relax \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
}
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
