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