|
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 |