|
1 % proof.sty (Proof Figure Macros) |
|
2 % |
|
3 % version 2.0 |
|
4 % June 24, 1991 |
|
5 % Copyright (C) 1990,1991 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 % \infer=<Lower><Uppers> |
|
45 % draws a double-ruled deduction. |
|
46 % |
|
47 % \infer=[<Label>]<Lower><Uppers> |
|
48 % draws a double-ruled deduction labeled with <Label>. |
|
49 % |
|
50 % \deduce<Lower><Uppers> |
|
51 % draws an inference without a rule. |
|
52 % |
|
53 % \deduce[<Proof>]<Lower><Uppers> |
|
54 % draws a many step deduction with a proof name. |
|
55 % |
|
56 % Example: |
|
57 % If you want to write |
|
58 % B C |
|
59 % ----- |
|
60 % A D |
|
61 % ---------- |
|
62 % E |
|
63 % use |
|
64 % \infer{E}{ |
|
65 % A |
|
66 % & |
|
67 % \infer{D}{B & C} |
|
68 % } |
|
69 % |
|
70 |
|
71 % Style Parameters |
|
72 |
|
73 \newdimen\inferLineSkip \inferLineSkip=2pt |
|
74 \newdimen\inferLabelSkip \inferLabelSkip=5pt |
|
75 \def\inferTabSkip{\quad} |
|
76 |
|
77 % Variables |
|
78 |
|
79 \newdimen\@LeftOffset % global |
|
80 \newdimen\@RightOffset % global |
|
81 \newdimen\@SavedLeftOffset % safe from users |
|
82 |
|
83 \newdimen\UpperWidth |
|
84 \newdimen\LowerWidth |
|
85 \newdimen\LowerHeight |
|
86 \newdimen\UpperLeftOffset |
|
87 \newdimen\UpperRightOffset |
|
88 \newdimen\UpperCenter |
|
89 \newdimen\LowerCenter |
|
90 \newdimen\UpperAdjust |
|
91 \newdimen\RuleAdjust |
|
92 \newdimen\LowerAdjust |
|
93 \newdimen\RuleWidth |
|
94 \newdimen\HLabelAdjust |
|
95 \newdimen\VLabelAdjust |
|
96 \newdimen\WidthAdjust |
|
97 |
|
98 \newbox\@UpperPart |
|
99 \newbox\@LowerPart |
|
100 \newbox\@LabelPart |
|
101 \newbox\ResultBox |
|
102 |
|
103 % Flags |
|
104 |
|
105 \newif\if@inferRule % whether \@infer draws a rule. |
|
106 \newif\if@DoubleRule % whether \@infer draws doulbe rules. |
|
107 \newif\if@ReturnLeftOffset % whether \@infer returns \@LeftOffset. |
|
108 \newif\if@MathSaved % whether inner math mode where \infer or |
|
109 % \deduce appears. |
|
110 |
|
111 % Special Fonts |
|
112 |
|
113 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@ |
|
114 \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}} |
|
115 |
|
116 % Math Save Macros |
|
117 % |
|
118 % \@SaveMath is called in the very begining of toplevel macros |
|
119 % which are \infer and \deduce. |
|
120 % \@RestoreMath is called in the very last before toplevel macros end. |
|
121 % Remark \infer and \deduce ends calling \@infer. |
|
122 |
|
123 \def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner |
|
124 \relax $\relax \@MathSavedtrue \fi\fi } |
|
125 |
|
126 \def\@RestoreMath{\if@MathSaved \relax $\relax\fi } |
|
127 |
|
128 % Macros |
|
129 |
|
130 \def\@Ifnextchar#1#2#3{\let\@tempe=#1\def\@tempa{#2}\def\@tempb{#3}\futurelet |
|
131 \@tempc\@ifnch} |
|
132 % It can compare an = character, though the one in latex.tex cannot. |
|
133 |
|
134 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax |
|
135 \ifx \@tempa \@tempb #2\else #3\fi } |
|
136 |
|
137 \def\infer{\@SaveMath \@Ifnextchar *{\@inferSteps}{\relax |
|
138 \@Ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}} |
|
139 |
|
140 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse |
|
141 \@Ifnextchar [{\@infer}{\@infer[\@empty]}} |
|
142 |
|
143 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue |
|
144 \@Ifnextchar [{\@infer}{\@infer[\@empty]}} |
|
145 |
|
146 \def\@inferSteps*{\@Ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}} |
|
147 |
|
148 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]} |
|
149 |
|
150 \def\deduce{\@SaveMath \@Ifnextchar [{\@deduce{\@empty}} |
|
151 {\@inferRulefalse \@infer[\@empty]}} |
|
152 |
|
153 % \@deduce<Proof Label>[<Proof>]<Lower><Uppers> |
|
154 |
|
155 \def\@deduce#1[#2]#3#4{\@inferRulefalse |
|
156 \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}} |
|
157 |
|
158 % \@infer[<Label>]<Lower><Uppers> |
|
159 % If \@inferRuletrue, it draws a rule and <Label> is right to |
|
160 % a rule. In this case, if \@DoubleRuletrue, it draws |
|
161 % double rules. |
|
162 % |
|
163 % Otherwise, draws no rule and <Label> is right to <Lower>. |
|
164 |
|
165 \def\@infer[#1]#2#3{\relax |
|
166 % Get parameters |
|
167 \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi |
|
168 \setbox\@LabelPart=\hbox{$#1$}\relax |
|
169 \setbox\@LowerPart=\hbox{$#2$}\relax |
|
170 % |
|
171 \global\@LeftOffset=0pt |
|
172 \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax |
|
173 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&& |
|
174 \inferTabSkip |
|
175 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr |
|
176 #3\cr}}\relax |
|
177 % Here is a little trick. |
|
178 % \@ReturnLeftOffsettrue(false) influences on \infer or |
|
179 % \deduce placed in ## locally |
|
180 % because of \@SaveMath and \@RestoreMath. |
|
181 \UpperLeftOffset=\@LeftOffset |
|
182 \UpperRightOffset=\@RightOffset |
|
183 % Calculate Adjustments |
|
184 \LowerWidth=\wd\@LowerPart |
|
185 \LowerHeight=\ht\@LowerPart |
|
186 \LowerCenter=0.5\LowerWidth |
|
187 % |
|
188 \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset |
|
189 \advance\UpperWidth by -\UpperRightOffset |
|
190 \UpperCenter=\UpperLeftOffset |
|
191 \advance\UpperCenter by 0.5\UpperWidth |
|
192 % |
|
193 \ifdim \UpperWidth > \LowerWidth |
|
194 % \UpperCenter > \LowerCenter |
|
195 \UpperAdjust=0pt |
|
196 \RuleAdjust=\UpperLeftOffset |
|
197 \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter |
|
198 \RuleWidth=\UpperWidth |
|
199 \global\@LeftOffset=\LowerAdjust |
|
200 % |
|
201 \else % \UpperWidth <= \LowerWidth |
|
202 \ifdim \UpperCenter > \LowerCenter |
|
203 % |
|
204 \UpperAdjust=0pt |
|
205 \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter |
|
206 \LowerAdjust=\RuleAdjust |
|
207 \RuleWidth=\LowerWidth |
|
208 \global\@LeftOffset=\LowerAdjust |
|
209 % |
|
210 \else % \UpperWidth <= \LowerWidth |
|
211 % \UpperCenter <= \LowerCenter |
|
212 % |
|
213 \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter |
|
214 \RuleAdjust=0pt |
|
215 \LowerAdjust=0pt |
|
216 \RuleWidth=\LowerWidth |
|
217 \global\@LeftOffset=0pt |
|
218 % |
|
219 \fi\fi |
|
220 % Make a box |
|
221 \if@inferRule |
|
222 % |
|
223 \setbox\ResultBox=\vbox{ |
|
224 \moveright \UpperAdjust \box\@UpperPart |
|
225 \nointerlineskip \kern\inferLineSkip |
|
226 \if@DoubleRule |
|
227 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth |
|
228 \kern 1pt\hrule width\RuleWidth}\relax |
|
229 \else |
|
230 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax |
|
231 \fi |
|
232 \nointerlineskip \kern\inferLineSkip |
|
233 \moveright \LowerAdjust \box\@LowerPart }\relax |
|
234 % |
|
235 \@ifEmpty{#1}{}{\relax |
|
236 % |
|
237 \HLabelAdjust=\wd\ResultBox \advance\HLabelAdjust by -\RuleAdjust |
|
238 \advance\HLabelAdjust by -\RuleWidth |
|
239 \WidthAdjust=\HLabelAdjust |
|
240 \advance\WidthAdjust by -\inferLabelSkip |
|
241 \advance\WidthAdjust by -\wd\@LabelPart |
|
242 \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi |
|
243 % |
|
244 \VLabelAdjust=\dp\@LabelPart |
|
245 \advance\VLabelAdjust by -\ht\@LabelPart |
|
246 \VLabelAdjust=0.5\VLabelAdjust \advance\VLabelAdjust by \LowerHeight |
|
247 \advance\VLabelAdjust by \inferLineSkip |
|
248 % |
|
249 \setbox\ResultBox=\hbox{\box\ResultBox |
|
250 \kern -\HLabelAdjust \kern\inferLabelSkip |
|
251 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax |
|
252 % |
|
253 }\relax % end @ifEmpty |
|
254 % |
|
255 \else % \@inferRulefalse |
|
256 % |
|
257 \setbox\ResultBox=\vbox{ |
|
258 \moveright \UpperAdjust \box\@UpperPart |
|
259 \nointerlineskip \kern\inferLineSkip |
|
260 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart |
|
261 \@ifEmpty{#1}{}{\relax |
|
262 \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax |
|
263 \fi |
|
264 % |
|
265 \global\@RightOffset=\wd\ResultBox |
|
266 \global\advance\@RightOffset by -\@LeftOffset |
|
267 \global\advance\@RightOffset by -\LowerWidth |
|
268 \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi |
|
269 % |
|
270 \box\ResultBox |
|
271 \@RestoreMath |
|
272 } |