Version of the proof macros for LaTeX 2e
authorberghofe
Fri May 02 16:18:11 1997 +0200 (1997-05-02)
changeset 309520251c80be78
parent 3094 76aa0d5554f0
child 3096 ccc2c92bb232
Version of the proof macros for LaTeX 2e
doc-src/proof.sty
     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 +}