source: Papers/polymorphic-variants-2012/prooftree.sty @ 3622

Last change on this file since 3622 was 2424, checked in by mulligan, 7 years ago

Changes to the file including making a start on incorporating Garrigue's typing rules in to the paper. Also added prooftree.sty to get the paper to compile.

File size: 12.3 KB
Line 
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).
Note: See TracBrowser for help on using the repository browser.