1\ProvidesPackage{proof}[1995/05/22] 2% proof.sty (Proof Figure Macros) 3% 4% version 2.0 5% June 24, 1991 6% Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp) 7% 8%Modified for LaTeX-2e by L. C. Paulson 9% 10% This program is free software; you can redistribute it or modify 11% it under the terms of the GNU General Public License as published by 12% the Free Software Foundation; either versions 1, or (at your option) 13% any later version. 14% 15% This program is distributed in the hope that it will be useful 16% but WITHOUT ANY WARRANTY; without even the implied warranty of 17% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 18% GNU General Public License for more details. 19% 20% Usage: 21% In \documentstyle, specify an optional style `proof', say, 22% \documentstyle[proof]{article}. 23% 24% The following macros are available: 25% 26% In all the following macros, all the arguments such as 27% <Lowers> and <Uppers> are processed in math mode. 28% 29% \infer<Lower><Uppers> 30% draws an inference. 31% 32% Use & in <Uppers> to delimit upper formulae. 33% <Uppers> consists more than 0 formulae. 34% 35% \infer returns \hbox{ ... } or \vbox{ ... } and 36% sets \@LeftOffset and \@RightOffset globally. 37% 38% \infer[<Label>]<Lower><Uppers> 39% draws an inference labeled with <Label>. 40% 41% \infer*<Lower><Uppers> 42% draws a many step deduction. 43% 44% \infer*[<Label>]<Lower><Uppers> 45% draws a many step deduction labeled with <Label>. 46% 47% \infer=<Lower><Uppers> 48% draws a double-ruled deduction. 49% 50% \infer=[<Label>]<Lower><Uppers> 51% draws a double-ruled deduction labeled with <Label>. 52% 53% \deduce<Lower><Uppers> 54% draws an inference without a rule. 55% 56% \deduce[<Proof>]<Lower><Uppers> 57% draws a many step deduction with a proof name. 58% 59% Example: 60% If you want to write 61% B C 62% ----- 63% A D 64% ---------- 65% E 66% use 67% \infer{E}{ 68% A 69% & 70% \infer{D}{B & C} 71% } 72% 73 74% Style Parameters 75 76\newdimen\inferLineSkip \inferLineSkip=2pt 77\newdimen\inferLabelSkip \inferLabelSkip=5pt 78\def\inferTabSkip{\quad} 79 80% Variables 81 82\newdimen\@LeftOffset % global 83\newdimen\@RightOffset % global 84\newdimen\@SavedLeftOffset % safe from users 85 86\newdimen\UpperWidth 87\newdimen\LowerWidth 88\newdimen\LowerHeight 89\newdimen\UpperLeftOffset 90\newdimen\UpperRightOffset 91\newdimen\UpperCenter 92\newdimen\LowerCenter 93\newdimen\UpperAdjust 94\newdimen\RuleAdjust 95\newdimen\LowerAdjust 96\newdimen\RuleWidth 97\newdimen\HLabelAdjust 98\newdimen\VLabelAdjust 99\newdimen\WidthAdjust 100 101\newbox\@UpperPart 102\newbox\@LowerPart 103\newbox\@LabelPart 104\newbox\ResultBox 105 106% Flags 107 108\newif\if@inferRule % whether \@infer draws a rule. 109\newif\if@DoubleRule % whether \@infer draws doulbe rules. 110\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. 111\newif\if@MathSaved % whether inner math mode where \infer or 112 % \deduce appears. 113 114% Special Fonts 115 116\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@ 117 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}} 118 119% Math Save Macros 120% 121% \@SaveMath is called in the very begining of toplevel macros 122% which are \infer and \deduce. 123% \@RestoreMath is called in the very last before toplevel macros end. 124% Remark \infer and \deduce ends calling \@infer. 125%TEMPORARILY DELETED BY LCP DUE TO CONFLICT WITH CLASS "amsmath.sty" 126 127\def\@SaveMath{} 128 129\def\@RestoreMath{} 130 131% Macros 132 133\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax 134 \ifx \@tempa \@tempb #2\else #3\fi } 135 136\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\relax 137 \@ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}} 138 139\def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse 140 \@ifnextchar [{\@infer}{\@infer[\@empty]}} 141 142\def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue 143 \@ifnextchar [{\@infer}{\@infer[\@empty]}} 144 145\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}} 146 147\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]} 148 149\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}} 150 {\@inferRulefalse \@infer[\@empty]}} 151 152% \@deduce<Proof Label>[<Proof>]<Lower><Uppers> 153 154\def\@deduce#1[#2]#3#4{\@inferRulefalse 155 \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}} 156 157% \@infer[<Label>]<Lower><Uppers> 158% If \@inferRuletrue, it draws a rule and <Label> is right to 159% a rule. In this case, if \@DoubleRuletrue, it draws 160% double rules. 161% 162% Otherwise, draws no rule and <Label> is right to <Lower>. 163 164\def\@infer[#1]#2#3{\relax 165% Get parameters 166 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi 167 \setbox\@LabelPart=\hbox{$#1$}\relax 168 \setbox\@LowerPart=\hbox{$#2$}\relax 169% 170 \global\@LeftOffset=0pt 171 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax 172 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&& 173 \inferTabSkip 174 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr 175 #3\cr}}\relax 176% Here is a little trick. 177% \@ReturnLeftOffsettrue(false) influences on \infer or 178% \deduce placed in ## locally 179% because of \@SaveMath and \@RestoreMath. 180 \UpperLeftOffset=\@LeftOffset 181 \UpperRightOffset=\@RightOffset 182% Calculate Adjustments 183 \LowerWidth=\wd\@LowerPart 184 \LowerHeight=\ht\@LowerPart 185 \LowerCenter=0.5\LowerWidth 186% 187 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset 188 \advance\UpperWidth by -\UpperRightOffset 189 \UpperCenter=\UpperLeftOffset 190 \advance\UpperCenter by 0.5\UpperWidth 191% 192 \ifdim \UpperWidth > \LowerWidth 193 % \UpperCenter > \LowerCenter 194 \UpperAdjust=0pt 195 \RuleAdjust=\UpperLeftOffset 196 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter 197 \RuleWidth=\UpperWidth 198 \global\@LeftOffset=\LowerAdjust 199% 200 \else % \UpperWidth <= \LowerWidth 201 \ifdim \UpperCenter > \LowerCenter 202% 203 \UpperAdjust=0pt 204 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter 205 \LowerAdjust=\RuleAdjust 206 \RuleWidth=\LowerWidth 207 \global\@LeftOffset=\LowerAdjust 208% 209 \else % \UpperWidth <= \LowerWidth 210 % \UpperCenter <= \LowerCenter 211% 212 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter 213 \RuleAdjust=0pt 214 \LowerAdjust=0pt 215 \RuleWidth=\LowerWidth 216 \global\@LeftOffset=0pt 217% 218 \fi\fi 219% Make a box 220 \if@inferRule 221% 222 \setbox\ResultBox=\vbox{ 223 \moveright \UpperAdjust \box\@UpperPart 224 \nointerlineskip \kern\inferLineSkip 225 \if@DoubleRule 226 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth 227 \kern 1pt\hrule width\RuleWidth}\relax 228 \else 229 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax 230 \fi 231 \nointerlineskip \kern\inferLineSkip 232 \moveright \LowerAdjust \box\@LowerPart }\relax 233% 234 \@ifEmpty{#1}{}{\relax 235% 236 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust 237 \advance\HLabelAdjust by -\RuleWidth 238 \WidthAdjust=\HLabelAdjust 239 \advance\WidthAdjust by -\inferLabelSkip 240 \advance\WidthAdjust by -\wd\@LabelPart 241 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi 242% 243 \VLabelAdjust=\dp\@LabelPart 244 \advance\VLabelAdjust by -\ht\@LabelPart 245 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight 246 \advance\VLabelAdjust by \inferLineSkip 247% 248 \setbox\ResultBox=\hbox{\box\ResultBox 249 \kern -\HLabelAdjust \kern\inferLabelSkip 250 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax 251% 252 }\relax % end @ifEmpty 253% 254 \else % \@inferRulefalse 255% 256 \setbox\ResultBox=\vbox{ 257 \moveright \UpperAdjust \box\@UpperPart 258 \nointerlineskip \kern\inferLineSkip 259 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart 260 \@ifEmpty{#1}{}{\relax 261 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax 262 \fi 263% 264 \global\@RightOffset=\wd\ResultBox 265 \global\advance\@RightOffset by -\@LeftOffset 266 \global\advance\@RightOffset by -\LowerWidth 267 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi 268% 269 \box\ResultBox 270 \@RestoreMath 271} 272\endinput 273