1 | \message{<Paul Taylor's Proof Trees, 2 August 1996>} |
---|
2 | %% Build proof tree for Natural Deduction, Sequent Calculus, etc. |
---|
3 | %% WITH SHORTENING OF PROOF RULES! |
---|
4 | %% Paul Taylor, begun 10 Oct 1989 |
---|
5 | %% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! *** |
---|
6 | %% |
---|
7 | %% 2 Aug 1996: fixed \mscount and \proofdotnumber |
---|
8 | %% |
---|
9 | %% \prooftree |
---|
10 | %% hyp1 produces: |
---|
11 | %% hyp2 |
---|
12 | %% hyp3 hyp1 hyp2 hyp3 |
---|
13 | %% \justifies -------------------- rulename |
---|
14 | %% concl concl |
---|
15 | %% \thickness=0.08em |
---|
16 | %% \shiftright 2em |
---|
17 | %% \using |
---|
18 | %% rulename |
---|
19 | %% \endprooftree |
---|
20 | %% |
---|
21 | %% where the hypotheses may be similar structures or just formulae. |
---|
22 | %% |
---|
23 | %% To get a vertical string of dots instead of the proof rule, do |
---|
24 | %% |
---|
25 | %% \prooftree which produces: |
---|
26 | %% [hyp] |
---|
27 | %% \using [hyp] |
---|
28 | %% name . |
---|
29 | %% \proofdotseparation=1.2ex .name |
---|
30 | %% \proofdotnumber=4 . |
---|
31 | %% \leadsto . |
---|
32 | %% concl concl |
---|
33 | %% \endprooftree |
---|
34 | %% |
---|
35 | %% Within a prooftree, \[ and \] may be used instead of \prooftree and |
---|
36 | %% \endprooftree; this is not permitted at the outer level because it |
---|
37 | %% conflicts with LaTeX. Also, |
---|
38 | %% \Justifies |
---|
39 | %% produces a double line. In LaTeX you can use \begin{prooftree} and |
---|
40 | %% \end{prootree} at the outer level (however this will not work for the inner |
---|
41 | %% levels, but in any case why would you want to be so verbose?). |
---|
42 | %% |
---|
43 | %% All of of the keywords except \prooftree and \endprooftree are optional |
---|
44 | %% and may appear in any order. They may also be combined in \newcommand's |
---|
45 | %% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation |
---|
46 | %% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and |
---|
47 | %% some standard abbreviations will be found at the end of this file. |
---|
48 | %% |
---|
49 | %% \thickness specifies the breadth of the rule in any units, although |
---|
50 | %% font-relative units such as "ex" or "em" are preferable. |
---|
51 | %% It may optionally be followed by "=". |
---|
52 | %% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be |
---|
53 | %% used either in place of \thickness or globally; the default is 0.04em. |
---|
54 | %% \proofdotseparation and \proofdotnumber control the size of the |
---|
55 | %% string of dots |
---|
56 | %% |
---|
57 | %% If proof trees and formulae are mixed, some explicit spacing is needed, |
---|
58 | %% but don't put anything to the left of the left-most (or the right of |
---|
59 | %% the right-most) hypothesis, or put it in braces, because this will cause |
---|
60 | %% the indentation to be lost. |
---|
61 | %% |
---|
62 | %% By default the conclusion is centered wrt the left-most and right-most |
---|
63 | %% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves |
---|
64 | %% it relative to this position. (Not sure about this specification or how |
---|
65 | %% it should affect spreading of proof tree.) |
---|
66 | % |
---|
67 | % global assignments to dimensions seem to have the effect of stretching |
---|
68 | % diagrams horizontally. |
---|
69 | % |
---|
70 | %%========================================================================== |
---|
71 | |
---|
72 | \def\introrule{{\cal I}}\def\elimrule{{\cal E}}%% |
---|
73 | \def\andintro{\using{\land}\introrule\justifies}%% |
---|
74 | \def\impelim{\using{\Rightarrow}\elimrule\justifies}%% |
---|
75 | \def\allintro{\using{\forall}\introrule\justifies}%% |
---|
76 | \def\allelim{\using{\forall}\elimrule\justifies}%% |
---|
77 | \def\falseelim{\using{\bot}\elimrule\justifies}%% |
---|
78 | \def\existsintro{\using{\exists}\introrule\justifies}%% |
---|
79 | |
---|
80 | %% #1 is meant to be 1 or 2 for the first or second formula |
---|
81 | \def\andelim#1{\using{\land}#1\elimrule\justifies}%% |
---|
82 | \def\orintro#1{\using{\lor}#1\introrule\justifies}%% |
---|
83 | |
---|
84 | %% #1 is meant to be a label corresponding to the discharged hypothesis/es |
---|
85 | \def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%% |
---|
86 | \def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%% |
---|
87 | \def\existselim#1{\using{\exists}\elimrule_{#1}\justifies} |
---|
88 | |
---|
89 | %%========================================================================== |
---|
90 | |
---|
91 | \newdimen\proofrulebreadth \proofrulebreadth=.05em |
---|
92 | \newdimen\proofdotseparation \proofdotseparation=1.25ex |
---|
93 | \newdimen\proofrulebaseline \proofrulebaseline=2ex |
---|
94 | \newcount\proofdotnumber \proofdotnumber=3 |
---|
95 | \let\then\relax |
---|
96 | \def\hfi{\hskip0pt plus.0001fil} |
---|
97 | \mathchardef\squigto="3A3B |
---|
98 | % |
---|
99 | % flag where we are |
---|
100 | \newif\ifinsideprooftree\insideprooftreefalse |
---|
101 | \newif\ifonleftofproofrule\onleftofproofrulefalse |
---|
102 | \newif\ifproofdots\proofdotsfalse |
---|
103 | \newif\ifdoubleproof\doubleprooffalse |
---|
104 | \let\wereinproofbit\relax |
---|
105 | % |
---|
106 | % dimensions and boxes of bits |
---|
107 | \newdimen\shortenproofleft |
---|
108 | \newdimen\shortenproofright |
---|
109 | \newdimen\proofbelowshift |
---|
110 | \newbox\proofabove |
---|
111 | \newbox\proofbelow |
---|
112 | \newbox\proofrulename |
---|
113 | % |
---|
114 | % miscellaneous commands for setting values |
---|
115 | \def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 } |
---|
116 | \def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }% |
---|
117 | \afterassignment\setshiftproofbelow\dimen0 } |
---|
118 | \def\setshiftproofbelow{\next\proofbelowshift=\dimen0 } |
---|
119 | \def\setproofrulebreadth{\proofrulebreadth} |
---|
120 | |
---|
121 | %============================================================================= |
---|
122 | \def\prooftree{% NESTED ZERO (\ifonleftofproofrule) |
---|
123 | % |
---|
124 | % first find out whether we're at the left-hand end of a proof rule |
---|
125 | \ifnum \lastpenalty=1 |
---|
126 | \then \unpenalty |
---|
127 | \else \onleftofproofrulefalse |
---|
128 | \fi |
---|
129 | % |
---|
130 | % some space on left (except if we're on left, and no infinity for outermost) |
---|
131 | \ifonleftofproofrule |
---|
132 | \else \ifinsideprooftree |
---|
133 | \then \hskip.5em plus1fil |
---|
134 | \fi |
---|
135 | \fi |
---|
136 | % |
---|
137 | % begin our proof tree environment |
---|
138 | \bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove, |
---|
139 | % \shortenproofleft, \shortenproofright, \proofrulebreadth) |
---|
140 | \setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}% |
---|
141 | \let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl |
---|
142 | \let\using\proofusing\let\[\prooftree |
---|
143 | \ifinsideprooftree\let\]\endprooftree\fi |
---|
144 | \proofdotsfalse\doubleprooffalse |
---|
145 | \let\thickness\setproofrulebreadth |
---|
146 | \let\shiftright\shiftproofbelow \let\shift\shiftproofbelow |
---|
147 | \let\shiftleft\shiftproofbelowneg |
---|
148 | \let\ifwasinsideprooftree\ifinsideprooftree |
---|
149 | \insideprooftreetrue |
---|
150 | % |
---|
151 | % now begin to set the top of the rule (definitions local to it) |
---|
152 | \setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO |
---|
153 | \let\wereinproofbit\prooftree |
---|
154 | % |
---|
155 | % these local variables will be copied out: |
---|
156 | \shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt |
---|
157 | % |
---|
158 | % flags to enable inner proof tree to detect if on left: |
---|
159 | \onleftofproofruletrue\penalty1 |
---|
160 | } |
---|
161 | |
---|
162 | %============================================================================= |
---|
163 | % end whatever box and copy crucial values out of it |
---|
164 | \def\eproofbit{% NESTED TWO |
---|
165 | % |
---|
166 | % various hacks applicable to hypothesis list |
---|
167 | \ifx \wereinproofbit\prooftree |
---|
168 | \then \ifcase \lastpenalty |
---|
169 | \then \shortenproofright=0pt % 0: some other object, no indentation |
---|
170 | \or \unpenalty\hfil % 1: empty hypotheses, just glue |
---|
171 | \or \unpenalty\unskip % 2: just had a tree, remove glue |
---|
172 | \else \shortenproofright=0pt % eh? |
---|
173 | \fi |
---|
174 | \fi |
---|
175 | % |
---|
176 | % pass out crucial values from scope |
---|
177 | \global\dimen0=\shortenproofleft |
---|
178 | \global\dimen1=\shortenproofright |
---|
179 | \global\dimen2=\proofrulebreadth |
---|
180 | \global\dimen3=\proofbelowshift |
---|
181 | \global\dimen4=\proofdotseparation |
---|
182 | \global\count255=\proofdotnumber |
---|
183 | % |
---|
184 | % end the box |
---|
185 | $\egroup % NESTED ONE |
---|
186 | % |
---|
187 | % restore the values |
---|
188 | \shortenproofleft=\dimen0 |
---|
189 | \shortenproofright=\dimen1 |
---|
190 | \proofrulebreadth=\dimen2 |
---|
191 | \proofbelowshift=\dimen3 |
---|
192 | \proofdotseparation=\dimen4 |
---|
193 | \proofdotnumber=\count255 |
---|
194 | } |
---|
195 | |
---|
196 | %============================================================================= |
---|
197 | \def\proofover{% NESTED TWO |
---|
198 | \eproofbit % NESTED ONE |
---|
199 | \setbox\proofbelow=\hbox\bgroup % NESTED TWO |
---|
200 | \let\wereinproofbit\proofover |
---|
201 | $\displaystyle |
---|
202 | }% |
---|
203 | % |
---|
204 | %============================================================================= |
---|
205 | \def\proofoverdbl{% NESTED TWO |
---|
206 | \eproofbit % NESTED ONE |
---|
207 | \doubleprooftrue |
---|
208 | \setbox\proofbelow=\hbox\bgroup % NESTED TWO |
---|
209 | \let\wereinproofbit\proofoverdbl |
---|
210 | $\displaystyle |
---|
211 | }% |
---|
212 | % |
---|
213 | %============================================================================= |
---|
214 | \def\proofoverdots{% NESTED TWO |
---|
215 | \eproofbit % NESTED ONE |
---|
216 | \proofdotstrue |
---|
217 | \setbox\proofbelow=\hbox\bgroup % NESTED TWO |
---|
218 | \let\wereinproofbit\proofoverdots |
---|
219 | $\displaystyle |
---|
220 | }% |
---|
221 | % |
---|
222 | %============================================================================= |
---|
223 | \def\proofusing{% NESTED TWO |
---|
224 | \eproofbit % NESTED ONE |
---|
225 | \setbox\proofrulename=\hbox\bgroup % NESTED TWO |
---|
226 | \let\wereinproofbit\proofusing |
---|
227 | \kern0.3em$ |
---|
228 | } |
---|
229 | |
---|
230 | %============================================================================= |
---|
231 | \def\endprooftree{% NESTED TWO |
---|
232 | \eproofbit % NESTED ONE |
---|
233 | % \dimen0 = length of proof rule |
---|
234 | % \dimen1 = indentation of conclusion wrt rule |
---|
235 | % \dimen2 = new \shortenproofleft, ie indentation of conclusion |
---|
236 | % \dimen3 = new \shortenproofright, ie |
---|
237 | % space on right of conclusion to end of tree |
---|
238 | % \dimen4 = space on right of conclusion below rule |
---|
239 | \dimen5 =0pt% spread of hypotheses |
---|
240 | % \dimen6, \dimen7 = height & depth of rule |
---|
241 | % |
---|
242 | % length of rule needed by proof above |
---|
243 | \dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft |
---|
244 | \advance\dimen0-\shortenproofright |
---|
245 | % |
---|
246 | % amount of spare space below |
---|
247 | \dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow |
---|
248 | \dimen4=\dimen1 |
---|
249 | \advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift |
---|
250 | % |
---|
251 | % conclusion sticks out to left of immediate hypotheses |
---|
252 | \ifdim \dimen1<0pt |
---|
253 | \then \advance\shortenproofleft\dimen1 |
---|
254 | \advance\dimen0-\dimen1 |
---|
255 | \dimen1=0pt |
---|
256 | % now it sticks out to left of tree! |
---|
257 | \ifdim \shortenproofleft<0pt |
---|
258 | \then \setbox\proofabove=\hbox{% |
---|
259 | \kern-\shortenproofleft\unhbox\proofabove}% |
---|
260 | \shortenproofleft=0pt |
---|
261 | \fi |
---|
262 | \fi |
---|
263 | % |
---|
264 | % and to the right |
---|
265 | \ifdim \dimen4<0pt |
---|
266 | \then \advance\shortenproofright\dimen4 |
---|
267 | \advance\dimen0-\dimen4 |
---|
268 | \dimen4=0pt |
---|
269 | \fi |
---|
270 | % |
---|
271 | % make sure enough space for label |
---|
272 | \ifdim \shortenproofright<\wd\proofrulename |
---|
273 | \then \shortenproofright=\wd\proofrulename |
---|
274 | \fi |
---|
275 | % |
---|
276 | % calculate new indentations |
---|
277 | \dimen2=\shortenproofleft \advance\dimen2 by\dimen1 |
---|
278 | \dimen3=\shortenproofright\advance\dimen3 by\dimen4 |
---|
279 | % |
---|
280 | % make the rule or dots, with name attached |
---|
281 | \ifproofdots |
---|
282 | \then |
---|
283 | \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0 |
---|
284 | \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}% |
---|
285 | \setbox0=\hbox{% |
---|
286 | \advance\dimen6-.5\wd1 |
---|
287 | \kern\dimen6 |
---|
288 | $\vcenter to\proofdotnumber\proofdotseparation |
---|
289 | {\leaders\box1\vfill}$% |
---|
290 | \unhbox\proofrulename}% |
---|
291 | \else \dimen6=\fontdimen22\the\textfont2 % height of maths axis |
---|
292 | \dimen7=\dimen6 |
---|
293 | \advance\dimen6by.5\proofrulebreadth |
---|
294 | \advance\dimen7by-.5\proofrulebreadth |
---|
295 | \setbox0=\hbox{% |
---|
296 | \kern\shortenproofleft |
---|
297 | \ifdoubleproof |
---|
298 | \then \hbox to\dimen0{% |
---|
299 | $\mathsurround0pt\mathord=\mkern-6mu% |
---|
300 | \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill |
---|
301 | \mkern-6mu\mathord=$}% |
---|
302 | \else \vrule height\dimen6 depth-\dimen7 width\dimen0 |
---|
303 | \fi |
---|
304 | \unhbox\proofrulename}% |
---|
305 | \ht0=\dimen6 \dp0=-\dimen7 |
---|
306 | \fi |
---|
307 | % |
---|
308 | % set up to centre outermost tree only |
---|
309 | \let\doll\relax |
---|
310 | \ifwasinsideprooftree |
---|
311 | \then \let\VBOX\vbox |
---|
312 | \else \ifmmode\else$\let\doll=$\fi |
---|
313 | \let\VBOX\vcenter |
---|
314 | \fi |
---|
315 | % this \vbox or \vcenter is the actual output: |
---|
316 | \VBOX {\baselineskip\proofrulebaseline \lineskip.2ex |
---|
317 | \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi |
---|
318 | \hbox spread\dimen5 {\hfi\unhbox\proofabove\hfi}% |
---|
319 | \hbox{\box0}% |
---|
320 | \hbox {\kern\dimen2 \box\proofbelow}}\doll% |
---|
321 | % |
---|
322 | % pass new indentations out of scope |
---|
323 | \global\dimen2=\dimen2 |
---|
324 | \global\dimen3=\dimen3 |
---|
325 | \egroup % NESTED ZERO |
---|
326 | \ifonleftofproofrule |
---|
327 | \then \shortenproofleft=\dimen2 |
---|
328 | \fi |
---|
329 | \shortenproofright=\dimen3 |
---|
330 | % |
---|
331 | % some space on right and flag we've just made a tree |
---|
332 | \onleftofproofrulefalse |
---|
333 | \ifinsideprooftree |
---|
334 | \then \hskip.5em plus 1fil \penalty2 |
---|
335 | \fi |
---|
336 | } |
---|
337 | |
---|
338 | %========================================================================== |
---|
339 | % IDEAS |
---|
340 | % 1. Specification of \shiftright and how to spread trees. |
---|
341 | % 2. Spacing command \m which causes 1em+1fil spacing, over-riding |
---|
342 | % exisiting space on sides of trees and not affecting the |
---|
343 | % detection of being on the left or right. |
---|
344 | % 3. Hack using \@currenvir to detect LaTeX environment; have to |
---|
345 | % use \aftergroup to pass \shortenproofleft/right out. |
---|
346 | % 4. (Pie in the sky) detect how much trees can be "tucked in" |
---|
347 | % 5. Discharged hypotheses (diagonal lines). |
---|