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