1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/proof.sty Fri May 02 16:18:11 1997 +0200
1.3 @@ -0,0 +1,250 @@
1.4 +% proof.sty (Proof Figure Macros)
1.5 +%
1.6 +% version 1.0
1.7 +% October 13, 1990
1.8 +% Copyright (C) 1990 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
1.9 +%
1.10 +% This program is free software; you can redistribute it or modify
1.11 +% it under the terms of the GNU General Public License as published by
1.12 +% the Free Software Foundation; either versions 1, or (at your option)
1.13 +% any later version.
1.14 +%
1.15 +% This program is distributed in the hope that it will be useful
1.16 +% but WITHOUT ANY WARRANTY; without even the implied warranty of
1.17 +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
1.18 +% GNU General Public License for more details.
1.19 +%
1.20 +% Usage:
1.21 +% In \documentstyle, specify an optional style `proof', say,
1.22 +% \documentstyle[proof]{article}.
1.23 +%
1.24 +% The following macros are available:
1.25 +%
1.26 +% In all the following macros, all the arguments such as
1.27 +% <Lowers> and <Uppers> are processed in math mode.
1.28 +%
1.29 +% \infer<Lower><Uppers>
1.30 +% draws an inference.
1.31 +%
1.32 +% Use & in <Uppers> to delimit upper formulae.
1.33 +% <Uppers> consists more than 0 formulae.
1.34 +%
1.35 +% \infer returns \hbox{ ... } or \vbox{ ... } and
1.36 +% sets \@LeftOffset and \@RightOffset globally.
1.37 +%
1.38 +% \infer[<Label>]<Lower><Uppers>
1.39 +% draws an inference labeled with <Label>.
1.40 +%
1.41 +% \infer*<Lower><Uppers>
1.42 +% draws a many step deduction.
1.43 +%
1.44 +% \infer*[<Label>]<Lower><Uppers>
1.45 +% draws a many step deduction labeled with <Label>.
1.46 +%
1.47 +% \deduce<Lower><Uppers>
1.48 +% draws an inference without a rule.
1.49 +%
1.50 +% \deduce[<Proof>]<Lower><Uppers>
1.51 +% draws a many step deduction with a proof name.
1.52 +%
1.53 +% Example:
1.54 +% If you want to write
1.55 +% B C
1.56 +% -----
1.57 +% A D
1.58 +% ----------
1.59 +% E
1.60 +% use
1.61 +% \infer{E}{
1.62 +% A
1.63 +% &
1.64 +% \infer{D}{B & C}
1.65 +% }
1.66 +%
1.67 +
1.68 +% Style Parameters
1.69 +
1.70 +\newdimen\inferLineSkip \inferLineSkip=2pt
1.71 +\newdimen\inferLabelSkip \inferLabelSkip=5pt
1.72 +\def\inferTabSkip{\quad}
1.73 +
1.74 +% Variables
1.75 +
1.76 +\newdimen\@LeftOffset % global
1.77 +\newdimen\@RightOffset % global
1.78 +\newdimen\@SavedLeftOffset % safe from users
1.79 +
1.80 +\newdimen\UpperWidth
1.81 +\newdimen\LowerWidth
1.82 +\newdimen\LowerHeight
1.83 +\newdimen\UpperLeftOffset
1.84 +\newdimen\UpperRightOffset
1.85 +\newdimen\UpperCenter
1.86 +\newdimen\LowerCenter
1.87 +\newdimen\UpperAdjust
1.88 +\newdimen\RuleAdjust
1.89 +\newdimen\LowerAdjust
1.90 +\newdimen\RuleWidth
1.91 +\newdimen\HLabelAdjust
1.92 +\newdimen\VLabelAdjust
1.93 +\newdimen\WidthAdjust
1.94 +
1.95 +\newbox\@UpperPart
1.96 +\newbox\@LowerPart
1.97 +\newbox\@LabelPart
1.98 +\newbox\ResultBox
1.99 +
1.100 +% Flags
1.101 +
1.102 +\newif\if@inferRule % whether \@infer draws a rule.
1.103 +\newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset.
1.104 +\newif\if@MathSaved % whether inner math mode where \infer or
1.105 + % \deduce appears.
1.106 +
1.107 +% Special Fonts
1.108 +
1.109 +\def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
1.110 + \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
1.111 +
1.112 +% Math Save Macros
1.113 +%
1.114 +% \@SaveMath is called in the very begining of toplevel macros
1.115 +% which are \infer and \deduce.
1.116 +% \@RestoreMath is called in the very last before toplevel macros end.
1.117 +% Remark \infer and \deduce ends calling \@infer.
1.118 +
1.119 +\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
1.120 + \relax $\relax \@MathSavedtrue \fi\fi }
1.121 +
1.122 +\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
1.123 +
1.124 +% Macros
1.125 +
1.126 +\def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
1.127 + \ifx \@tempa \@tempb #2\else #3\fi }
1.128 +
1.129 +\def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
1.130 +
1.131 +\def\@inferOneStep{\@inferRuletrue
1.132 + \@ifnextchar [{\@infer}{\@infer[\@empty]}}
1.133 +
1.134 +\def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
1.135 +
1.136 +\def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
1.137 +
1.138 +\def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
1.139 + {\@inferRulefalse \@infer[\@empty]}}
1.140 +
1.141 +% \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
1.142 +
1.143 +\def\@deduce#1[#2]#3#4{\@inferRulefalse
1.144 + \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
1.145 +
1.146 +% \@infer[<Label>]<Lower><Uppers>
1.147 +% If \@inferRuletrue, draws a rule and <Label> is right to
1.148 +% a rule.
1.149 +% Otherwise, draws no rule and <Label> is right to <Lower>.
1.150 +
1.151 +\def\@infer[#1]#2#3{\relax
1.152 +% Get parameters
1.153 + \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
1.154 + \setbox\@LabelPart=\hbox{$#1$}\relax
1.155 + \setbox\@LowerPart=\hbox{$#2$}\relax
1.156 +%
1.157 + \global\@LeftOffset=0pt
1.158 + \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
1.159 + \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
1.160 + \inferTabSkip
1.161 + \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
1.162 + #3\cr}}\relax
1.163 +% Here is a little trick.
1.164 +% \@ReturnLeftOffsettrue(false) influences on \infer or
1.165 +% \deduce placed in ## locally
1.166 +% because of \@SaveMath and \@RestoreMath.
1.167 + \UpperLeftOffset=\@LeftOffset
1.168 + \UpperRightOffset=\@RightOffset
1.169 +% Calculate Adjustments
1.170 + \LowerWidth=\wd\@LowerPart
1.171 + \LowerHeight=\ht\@LowerPart
1.172 + \LowerCenter=0.5\LowerWidth
1.173 +%
1.174 + \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
1.175 + \advance\UpperWidth by -\UpperRightOffset
1.176 + \UpperCenter=\UpperLeftOffset
1.177 + \advance\UpperCenter by 0.5\UpperWidth
1.178 +%
1.179 + \ifdim \UpperWidth > \LowerWidth
1.180 + % \UpperCenter > \LowerCenter
1.181 + \UpperAdjust=0pt
1.182 + \RuleAdjust=\UpperLeftOffset
1.183 + \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
1.184 + \RuleWidth=\UpperWidth
1.185 + \global\@LeftOffset=\LowerAdjust
1.186 +%
1.187 + \else % \UpperWidth <= \LowerWidth
1.188 + \ifdim \UpperCenter > \LowerCenter
1.189 +%
1.190 + \UpperAdjust=0pt
1.191 + \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
1.192 + \LowerAdjust=\RuleAdjust
1.193 + \RuleWidth=\LowerWidth
1.194 + \global\@LeftOffset=\LowerAdjust
1.195 +%
1.196 + \else % \UpperWidth <= \LowerWidth
1.197 + % \UpperCenter <= \LowerCenter
1.198 +%
1.199 + \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
1.200 + \RuleAdjust=0pt
1.201 + \LowerAdjust=0pt
1.202 + \RuleWidth=\LowerWidth
1.203 + \global\@LeftOffset=0pt
1.204 +%
1.205 + \fi\fi
1.206 +% Make a box
1.207 + \if@inferRule
1.208 +%
1.209 + \setbox\ResultBox=\vbox{
1.210 + \moveright \UpperAdjust \box\@UpperPart
1.211 + \nointerlineskip \kern\inferLineSkip
1.212 + \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
1.213 + \nointerlineskip \kern\inferLineSkip
1.214 + \moveright \LowerAdjust \box\@LowerPart }\relax
1.215 +%
1.216 + \@ifEmpty{#1}{}{\relax
1.217 +%
1.218 + \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust
1.219 + \advance\HLabelAdjust by -\RuleWidth
1.220 + \WidthAdjust=\HLabelAdjust
1.221 + \advance\WidthAdjust by -\inferLabelSkip
1.222 + \advance\WidthAdjust by -\wd\@LabelPart
1.223 + \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
1.224 +%
1.225 + \VLabelAdjust=\dp\@LabelPart
1.226 + \advance\VLabelAdjust by -\ht\@LabelPart
1.227 + \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight
1.228 + \advance\VLabelAdjust by \inferLineSkip
1.229 +%
1.230 + \setbox\ResultBox=\hbox{\box\ResultBox
1.231 + \kern -\HLabelAdjust \kern\inferLabelSkip
1.232 + \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
1.233 +%
1.234 + }\relax % end @ifEmpty
1.235 +%
1.236 + \else % \@inferRulefalse
1.237 +%
1.238 + \setbox\ResultBox=\vbox{
1.239 + \moveright \UpperAdjust \box\@UpperPart
1.240 + \nointerlineskip \kern\inferLineSkip
1.241 + \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
1.242 + \@ifEmpty{#1}{}{\relax
1.243 + \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
1.244 + \fi
1.245 +%
1.246 + \global\@RightOffset=\wd\ResultBox
1.247 + \global\advance\@RightOffset by -\@LeftOffset
1.248 + \global\advance\@RightOffset by -\LowerWidth
1.249 + \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
1.250 +%
1.251 + \box\ResultBox
1.252 + \@RestoreMath
1.253 +}