diff options
author | Karl Berry <karl@freefriends.org> | 2006-01-11 23:56:25 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2006-01-11 23:56:25 +0000 |
commit | 5e778ae71ee25dfa40530308f8e4cd5c1bf6b10b (patch) | |
tree | 11e8ce2402e9a13ca62badacf3ce22560c550a96 | |
parent | 377ce899e33cb201168f4018c5413d76668f32e6 (diff) |
trunk/Master/texmf-dist/source/latex/proofs
git-svn-id: svn://tug.org/texlive/trunk@464 c570f23f-e606-0410-a88d-b1316a301751
6 files changed, 2425 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty b/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty new file mode 100644 index 00000000000..788479059a9 --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/QED-.sty @@ -0,0 +1,580 @@ +\message{<Paul Taylor's right-justified end-of-proof mark, 2 June 1993>} +%%======================================================================== +%************************************************************************% +%* *% +%* Maybe you already have a \qed macro to put a little square *% +%* on the right hand side at the end of a mathematical proof? *% +%* *% +%* IT'S PROBABLY MINE! *% +%* *% +%* Please compare yours with \parag@pushright below. *% +%* *% +%* This new file is compatible, it fixes the bugs, has extra *% +%* features, and is maintained and portable. Please use it! *% +%* *% +%************************************************************************% +%========================================================================% + +% COPYRIGHT (C) 1993 Paul Taylor, Imperial College, London SW7 2BZ, UK +% You may use this file for any purpose. You may copy it on condition that +% you do so in exactly the form in which it was supplied, make no charge +% for the copy and impose the same conditions on the recipient. +% This software is supplied ``as is'' without warranty, express or implied, +% including but not limited to merchantability and fitness for any particular +% purpose. No liability is accepted by the author, Imperial College or any +% third party for any direct or consequential damages, however caused. +% In all cases you must keep several backup versions of your files in a place +% to which your machine cannot write, and you must check documents visually +% before submitting the final version to a publisher or expensive printer. + +% WARNING: If you use this with Frank Mittlebach's "theorem.sty" you +% MUST load theorem first, then QED, then do the \newtheorem commands. +% "theorem.sty" provides a number of typographical styles and is +% available by anonymous ftp from ftp.uni-stuttgart.de (129.69.1.12) +% in the directory /pub/soft/tex/macros/latex/styles/base/theorem +% also Aston: ftp.tex.ac.uk:/pub/archive/macros/latex/styles/base/theorem + +% Authoritative version: /tex/contrib/Taylor/tex/QED.sty +% by anonymous FTP from: theory.doc.ic.ac.uk (146.169.2.27) +% author/maintained by: Dr Paul Taylor <pt@doc.ic.ac.uk> + +% WARNING: This file replaces some of the functions of "Paul.sty" +% and MUST NOT be used with it as serious conflicts will arise. +% A new version is available as /tex/contrib/Taylor/Paul.sty as above. + +%========================================================================= + +% USER INTERFACE AND EXAMPLES (see also OPTIONS below) + +% \begin{Proof} ... \end{Proof} +% or \Proof ... \endProof +% or \Proof ... \endproof +% or \Proof ... \qed also \QED and \QEI + +% WARNING: \qed which doesn't follow \Proof will not print the square. + +% Each properly nested Proof/endProof pair gets a single +% \qedsymbol at the end, on the far right hand side. +% Unfortunately, this may still be in the wrong place +% if the proof ends with a display or itemisation. +% To solve this, \qed may be put *inside* the last substantive +% environment; the \qedsymbol will be put at that point +% (the visual end) and suppressed at the logical end of proof. + +% Examples: +% \begin{Proof} \begin{Proof} +% ... ... +% \begin{eqnarray} \begin{itemize} +% ... &=& ... \\ \item ... +% .. &=& ... &\qed \item ... \qed +% \end{eqnarray} \end{itemize} +% \end{Proof} \end{Proof} +% also works with $$...$$ and \[...\] displays, including fleqn.sty. + +% Unfortunately some environments, such as picture, do not allow this at all. +% In fact \qed will only work in those environments which provide access to +% the right hand side of the page. In other words, wherever you think +% "\hfill\square" ought to work then \qed will; of course it is just because +% that naive method doesn't work that this macro file is needed at all. +% The macro was designed to solve the problem in the case of "unrestricted +% horizontal mode" (ie at the end of a paragraph); it also works in $$ +% displays by pretending to be an equation number. In most other cases it +% basically does "\hfill\square" or "\hfill$\square$" and hopes for the best. + +% If you have to put \qed outside the environment, it may be appropriate to +% put \vskip-\baselineskip before it, unless of course this would over-print. +% There is, however, still a danger that TeX will break the page here. + +% The eqnarray example above does not in fact work: if you try it you'll +% get "! Paragraph ended before \llap was complete" with LaTeX in a mess. +% This is a very common place where you might want to put the end of proof +% mark, and I also consider that the fourth column should be available for +% "reasons" for equational steps. The following substitute for \eqnarray +% allows this, whilst being compatible with automatic numbering. I have +% proposed it to Rainer Sch\"opf for inclusion in LaTeX. If you want to +% use it, please copy it to another file rather than uncommenting it here. +% Don't forget to use \makeatletter or put it in a documentstyle (.sty) file. +% +% \def\eqnarray{\stepcounter{equation}\let\@currentlabel\theequation +% \global\@eqnswtrue\m@th\global\@eqcnt\z@\tabskip\@centering\let\\\@eqncr +% $$\halign to\displaywidth\bgroup\@eqnsel\hskip\@centering$\displaystyle +% \tabskip\z@{##}$&\global\@eqcnt\@ne\hskip 2\arraycolsep \hfil${##}$\hfil +% &\global\@eqcnt\tw@\hskip2\arraycolsep$\displaystyle\tabskip\z@{##}$\hfil +% \tabskip\@centering&% +% \global\@eqcnt\thr@@\hbox to\z@\bgroup\hss##%*** instead of "\llap{##}" +% \tabskip\z@\cr}% +% \def\@@eqncr{\let\@tempa\relax +% \ifcase\@eqcnt \def\@tempa{& & &}\or \def\@tempa{& &}% +% \or\def\@tempa{&}\else\@eqnswfalse%*** instead of "\else\def\@tempa{&}" +% \fi\@tempa\if@eqnsw\@eqnnum\stepcounter{equation}\fi +% \egroup%*** added, to match \bgroup in fourth cell of preamble +% \global\@eqnswtrue\global\@eqcnt\z@\cr} +% +% More generally, each individual environment (both the standard ones and +% those defined by the user) needs to co-operate in order to make this work. +% But it is not the business of this macro to rewrite LaTeX in this way. + +% Why can't we do all of this with \endProof? Because by that stage +% the damage has been done: the environments, paragraphs or +% displays have already been closed and their \hbox'es added +% to the current vertical list, and cannot be removed for +% alteration if this is the current page. + +% Even if you don't need to put \qed inside an inner environment +% to avoid a blank line, it's still a good idea to do so, because +% otherwise it's possible that intervening end-of-environment +% material may allow TeX to put the mark on the next page. + +% This file may be called QED.sty, QED.tex, qed.sty or qed.tex. +% It may be loaded either as a \documentstyle option or using \input, +% as it is careful to handle the \catcode of @ appropriately. + +% If you don't use theorem.sty, this file instead provides options to use +% commands to begin theorems, instead of enclosing them in environments, +% and to suppress numbering and italicisation. A rudimentary version of +% \newtheorem for plain TeX is also implemented (always using commands +% rather than environments). + +% At the end of the file some useful \newtheorem +% commands are listed but not executed. + +% \Theorem\Proof\endProof\qed will print the second square, whereas +% \begin{Theorem}\end{Theorem}\begin{Proof}\end{Proof}\qed will not. + +%========================================================================= +% Make @ letter, saving its old code to restore at the end of this file. +% Look for this towards the end of the file if you think something's missing! +% "plain.tex" defines \lq as a synonym for back quote (character constant); +% I use it to avoid corruption when sending TeX files by email via BITNET. +\edef\qedrestoreat{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}%% +\catcode\lq\@=11 + +% in LaTeX, \protect the user commands; +% in plain TeX, ensure that it is defined. +\ifx\protect\undefined\let\protect\relax\fi + +%========================================================================= + +% OPTIONS + +% These are the user commands. + +\def\qed{\protect\@qed{$\qedsymbol$}}% suppressible printing of \qedsymbol +\def\pushright{\protect\@pushright}% takes an argument, which it always prints + +% theoremata in Euclid needed proof: "which was to be shown" +\def\QED{\protect\@qed{{\rm Q.E.D.}}}% "quod erat demonstrandum" + +% but problemata needed construction: "which was to be found" +\def\QEI{\protect\@qed{{\rm Q.E.I.}}}% "quod erat inveniendum" + +% a LaTeX environment +\def\Proof{\protect\@Proof}\def\endProof{\protect\@endProof}% +\let\proof\Proof\let\endproof\endProof + + +% These are the user-settable parameters. + +% The actual (maths) symbol used by \qed +\def\qedsymbol{\square}% PLEASE NOTE: this is in the AMS symbols font. +%\def\qedsymbol{\blacksquare}% use one of these instead +%\def\qedsymbol{\hbox{\rm Q.E.D.}}% if you prefer + +% This is the text used by \Proof. +% A new paragraph is begun without indentation. +% Change it to {\kern\parindent\sc D\'emonstration: } if you like. +\def\TheWordProof{\bf Proof\enskip} + +% This is the font command used for the text of proofs +\def\ProofFont{} + +% The command \AutoQEDtrue causes a \qed in \end{Theorem}, so you do +% \begin{Theorem} ... \begin{Proof} ... \end{Proof} \end{Theorem} +% but if you omit the proof, the statement gets a little square at the end. +\newif\ifAutoQED\AutoQEDfalse + +% The remaining options are redundant with theorem.sty +% so are not defined if this has been loaded. +\newif\ifNumberResults +\ifx\theorem@style\undefined + % + % How to print the name (#1), number (#2) and attribution (#3) of a theorem. + \NumberResultstrue + % If the number (#2) is absent, "\unskip" removes the + % unwanted space "\ " from before it (16 Feb 1993). + \def\TheoremHeader#1#2#3{\bf #1\ifNumberResults\ #2\unskip\fi#3} + % + % This is the font command used for the text of theorem enunciations + % change to {\rm} or {\small} if you like. + \def\TheoremFont{\it} + % + % The command \NumberResultsfalse will suppress theorem numbering. + % + % The command \TheoremsAsCommands will allow you to write + % \Theorem instead of \begin{Theorem} ... \end{Theorem}. + % In this case italicisation is suppressed by default. + % To do this with theorem.sty would involve rewriting the substyles. + % + % WARNING: if you subsequently redefine \TheoremFont, and use the command + % instead of the environment, the font will remain in force afterwards! +\fi + +%========================================================================= +% If you already have a macro called \qed, \endproof or \pushright +% which is laid out in a similar way to the following two definitions +% (but with \hbox@pushright incorporated) then it is almost certainly +% my code, which has been copied anonymously via numerous people since +% my Cambridge PhD thesis in August 1986. Belated acknowledgements to +% Chris Thompson of the Cambridge University Computing Service for his +% help with my early attempts at TeX, in particular this problem. + +% The complexity of the macro necessary to get a little box on the +% right-hand-side at the end of a proof is amazing. It really does +% have to be this long! Otherwise you're liable to get it at the +% beginning of the next line, or even on the next page. + +\def\parag@pushright#1{{% set up + \parfillskip=0pt % so \par doesnt push \square to left + \widowpenalty=10000 % so we dont break the page before \square + \displaywidowpenalty=10000 % ditto + \finalhyphendemerits=0 % TeXbook exercise 14.32 + % + % horizontal + %\leavevmode % not needed since we now only use it in hmode + \hbox@pushright % this used to be incorporated + #1% % the end-of-proof mark (or whatever) + % + % vertical + \par}}% % build paragraph with the above parameters + +\def\hbox@pushright{% horizontal + \unskip % remove previous space or glue + \nobreak % don't break lines + \hfil % ragged right if we spill over + \penalty50 % discouragement to do so + \hskip.2em % ensure some space + \null % anchor following \hfill + \hfill % push \square to right +}% + +% Ideally, we would do the above by completing the paragraph, display or +% other structure, and then modifying its last line (\hbox). +% Unfortunately this cannot be done, because TeX does not allow you to +% remove a box (using \lastbox) which has already been contributed to the +% main vertical list (current page). + +% It would, I suppose, be possible to do it by collecting the entire proof +% in its own \vbox, modifying that and \unvbox'ing it to the current page. +% This approach may lead to the following problems: +% (i) overflow of TeX's main memory, especially if the \end{Proof} is missing; +% (ii) footnotes, floats, marginpars, labels and index items may be lost. +% (iii) I don't know how page-breaking would be handled. + +%======================================================================== + +% Switch to enable/suppress \qedsymbol; since suppression may be done +% within a nested scope it must be global, so we do our own save/restore +% in a symbol which is local to the Proof environment. +% On first use, we check to see whether an obsolete version of Paul.sty +% is around, and complain loudly if it is, because they interfere seriously. + +\newif\if@qed\@qedfalse +\def\save@set@qed{\check@pt@sty@v\let\saved@ifqed\if@qed\global\@qedtrue}% +\def\restore@qed{\global\let\if@qed\saved@ifqed} + +% prefer proofs with statements if possible - hence \penalty700 +% the only essential part of this is \save@set@qed +\def\@Proof{% + \par\removelastskip\smallskip\penalty700 + \save@set@qed + \noindent\ProofFont{\TheWordProof\enskip}% +}% + +\def\@endProof{% + \qed\restore@qed + \penalty-700 \smallskip +} + +\def\@qed#1{\check@pt@fm@thm +\if@qed % have we already done \qed? + \global\@qedfalse\pushright{#1}% - no - do it now, but not again +\else\ifhmode\ifinner\else\par\fi\fi% - yes - just end paragraph, if any +\fi} + +% \pushright{text} always prints its argument, on the far right, in text mode +\def\@pushright#1{% + \ifvmode % vertical mode (see comments below) + \nobreak % 22 Feb 1993: don't break page here + \null\hfill{#1}\par % --- #1 alone in a paragraph! + \else\ifmmode\maths@pushright{\hbox{#1}}% maths (force a text argument) + \else\ifinner\hbox@pushright{#1}% inside an \hbox + \else\parag@pushright{#1}% in a paragraph + \fi \fi \fi +}% (22 Feb 1993) removed extra {} which would destroy our \] below + +% In the \hbox and maths cases we are really at the mercy of the environment. +% Assuming that we have $\qed$ simply embedded in a paragraph, the horizontal +% processing by \hbox@pushright will at least make sure that the square isn't +% at the beginning of the line, but we can't stop it being on the next page. +% However it is more likely that the reason why we're in maths mode is that +% we're inside an eqnarray or similar, in which case \hfill will do its best +% to put the square on the right of the available space. (See \vadjust below.) +\def\maths@pushright#1{% + \ifinner + \hbox@pushright{#1}% + \else + \eqno#1% use TeX's right equation number feature (\eqno) within $$. + \def\]{$$\ignorespaces}% suppress LaTeX's error checking (HACK!) + \fi +}% (22 Feb 1993) removed extra {} which would destroy our \] above + +% An idea that didn't work: see TeXbook p188. (16 Feb 1993) +% Use \predisplaysize to find out the width of the previous box, +% in the case where it has already been completed. +% But this can only be used inside displays ($$), and a display in +% vertical mode begins a paragraph first, so we end up with +% \predisplaysize=\parindent+2em whatever happened in the previous +% paragraph. + +% \ifinner is true inside a \vbox or \vadjust; in both of these +% circumstances we are allowed to remove boxes with \lastbox etc. +% Maybe it's worth testing this case and doing it. + +% Another idea: it may be worth trying \vadjust, if only to insert \nobreak. +% The problem with this is that if we are too deeply nested in horizontal +% or maths lists, the adjustment may not be able to find its way out to the +% enclosing vertical list. In the case of array-like environments, it will +% appear (assuming it manages to get out) after the current row of the array. + +%=========================================================================== +% We have to add to the theorem environments the commands to enable \qed. +% This is done by re-defining \@thm#1#2. +% Note that Mittelbach's theorem.sty re-defines \@thm and \@endtheorem, so +% that must be loaded before us, otherwise our changes will get over-written +% and \qed will never be enabled. +% Paul.sty didn't use this method of gaining control inside a theorem, +% whereas it did define \qed and \pushright, so here is the one place +% where we can check for it. + +\ifx\nonqed@thm\undefined % otherwise double loading causes a loop 22 Feb 1993 + \let\nonqed@thm\@thm % save original + \let\nonqed@endthm\@endtheorem +\fi + +\def\@thm{\save@set@qed\nonqed@thm}% +\def\@endtheorem{\ifAutoQED\qed\fi\restore@qed\nonqed@endthm}% + +%=========================================================================== +% Check for obsolete versions and clashes of this and other macro files. +% Why do I do this? Because of those people who complain to me that +% something doesn't work but refuse to read the manual, and those +% who refuse to update their software, and then publish papers with +% commutative diagrams full of the bugs which I fixed several years ago. + +\def\obsolete@pt@version#1{\errhelp={% +% ***************************************************************** +% * The master version is available by * + Anonymous FTP theory.doc.ic.ac.uk /tex/contrib/Taylor/tex/#1}%* +% ***************************************************************** +\errmessage{You have an obsolete version of #1 - please get a new one}}% + +% First check QED.sty +\ifnum\year>1993 \obsolete@pt@version{QED.sty}\fi + +% If theorem.sty hasn't been loaded, arrange to check it again in \@qed. +% And check (then) whether you've actually defined \square. +% changed 2 June 1993: don't define it now, as that would confuse amssymb.sty +\ifx\theorem@style\undefined + \def\check@pt@fm@thm{\relax + \ifx\square\undefined + \gdef\square{\bigcirc + \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}% + \errmessage{\string\square\space is an AMS symbol}% + \global\let\square\bigcirc}% + \fi + \ifx\theorem@style\undefined + \global\let\check@pt@fm@thm\relax + \else\errhelp={The macros \@thm and \@endtheorem need to be re-defined.}% + \errmessage{QED.sty must be loaded AFTER theorem.sty but before + using \string\newtheorem}% + \fi + \global\let\check@pt@fm@thm\relax + }% +\else + \def\check@pt@fm@thm{% + \ifx\square\undefined + \def\square{\bigcirc + \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}% + \errmessage{\string\square\space is an AMS symbol}% + \global\let\square\bigcirc}% + \fi + \global\let\check@pt@fm@thm\relax + }% +\fi + +% Check for Paul.sty, which SERIOUSLY conflicts with this file. +% and also for version 2 or version 3 of commutative diagrams. +\def\check@pt@sty@v{% + \relax + \ifx\@@begintheorem\undefined + \else\message{*** QED.sty and the old Paul.sty seriously conflict! ***}% + \obsolete@pt@version{Paul.sty}% + \fi + \ifx\execHorizontalMap\undefined + \gdef\obsolete@pt@version##1{}% + \else\global\let\di@gr@m\diagram + \gdef\diagram{\obsolete@pt@version{diagrams.tex}\di@gr@m}% + \fi + \global\let\check@pt@sty@v\relax +}% + + +%=========================================================================== +% If Mittelbach's theorem.sty is loaded, skip the rest of the file. +\ifx\theorem@style\undefined\else\qedrestoreat\expandafter\endinput\fi +%=========================================================================== + +% Allow the user to suppress italicisation and numbering. + +% The following two macros are called by LaTeX to begin a theorem +% respectively with and without an optional (``attribution'') argument. +% It is clear from latex.tex that they are intended to be customised. +% The code common to the two has been taken out as \begin@theorem and +% \TheoremHeader. Of these, the former is re-defined by \TheoremsAsCommands. + +\def\@opargbegintheorem#1#2#3{\begin@theorem{\TheoremHeader{#1}{#2}{ (#3)} }} + +\def\@begintheorem#1#2{\begin@theorem{\TheoremHeader{#1}{#2}{} }} + +\def\begin@theorem#1{% + \trivlist\item[\hskip\labelsep {#1}]% % LaTeX likes this method. + \TheoremFont % Italicise the enunciation + \ifx\ProofFont\empty\def\ProofFont{\rm}\fi % but not any nested proof. + }% + + +%%% Here's what LaTeX (92/1/14) does: +%%%% RmS 91/08/14 Moved \it after \item to make it work with NFSS +%%\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]\it} +%%\def\@opargbegintheorem#1#2#3{\trivlist +%% \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]\it} +%%\def\@endtheorem{\endtrivlist} + + +% The document style option "theorems-as-commands" will allow you to +% write \Theorem instead of \begin{Theorem} ... \end{Theorem}. +\def\TheoremsAsCommands{% + \def\TheoremFont{}% suppress italicised theorems. + \def\begin@theorem##1{% + \par\removelastskip\smallskip + \save@set@qed % enable \qed + \noindent{##1}% the name + \TheoremFont % italicise at your own risk! + }% + \def\@endtheorem{\ifAutoQED\qed\fi\restore@qed}% +}% + +\expandafter\let\csname ds@theorems-as-commands\endcsname\TheoremsAsCommands + +%=========================================================================== +% If we're running under LaTeX, skip the rest of the file. +\ifx\newtheorem\undefined\else\qedrestoreat\expandafter\endinput\fi +%=========================================================================== + +% This implements a rudimentary version of \newtheorem for plain TeX. +% Only the unattributed theorems and the +% declarations \newtheorem{Theorem}[Result]{Theorem} and +% \newtheorem{Convention}[Unnumbered]{Convention} are supported. +% The numbering is based on the counts \chapternumber, \sectionnumber +% and \subsectionnumber, which it is up to you to define with \newcount. +% It's also up to you to reset \c@Result at the beginning of each section. + +% Form the number: (chapter).(section).(subsection).(#1) +% where any of the first three parts which is zero +% negative or undefined is omitted. +\def\ther@sult#1{% +\ifx\chapternumber\undefined\else + \ifnum\chapternumber>0 \number\chapternumber.\fi\fi +\ifx\sectionnumber\undefined\else + \ifnum\sectionnumber>0 \number\sectionnumber.\fi\fi +\ifx\subsectionnumber\undefined\else + \ifnum\subsectionnumber>0 \number\subsectionnumber.\fi\fi +\expandafter\number\csname c@#1\endcsname}% + +% plain version of LaTeX's \@thm +\def\plain@thm#1#2{% #1=counter, #2=text + \save@set@qed + \expandafter\advance\csname c@#1\endcsname1 + \@begintheorem{#2}{\csname the#1\endcsname}% +}% + +% Rudimentary \newtheorem +\def\newtheorem#1[#2]#3{% #1=command, #2=counter, #3=text + % + % \def\#1{\plain@thm{#2}{#3}} + \expandafter\def\csname #1\endcsname{\plain@thm{#2}{#3}}% + % + % \def\end#1{\@endtheorem} + \expandafter\def\csname end#1\endcsname{\@endtheorem}% + % + % if \c@#2 is not defined + % \newcount\c@#2 + % \def\the#2{\ther@sult{#2}} + \expandafter\ifx\csname c@#2\endcsname\relax + \expandafter\expandafter\csname newcount\endcsname + \csname c@#2\endcsname + \expandafter\def\csname the#2\endcsname{\ther@sult{#2}}% + \fi +}% + +\TheoremsAsCommands + +\qedrestoreat\endinput + +%=========================================================================== + +% The following commands are not executed (because of \endinput above), +% but you may find it convenient to include some of them. + +% First set up uniform numbering in LaTeX; +% don't use this in plain TeX because this usage of \newcommand is not +% supported and we have already done by hand what it would do in LaTeX, +% viz to define the macro \theResult and the count \c@Result. +\ifx\@@thm\undefined + \newtheorem{Result}{Result}[subsection]% + \@addtoreset{Result}{section}% + \ifx\chapter\undefined\else\@addtoreset{Result}{chapter}\fi +\fi + +\let\theUnnumbered\relax\countdef\c@Unnumbered255 \def\p@Unnumbered{} + +\newtheorem{Answer}[Result]{Answer} +\newtheorem{Answers}[Result]{Answers} +\newtheorem{Conjecture}[Result]{Conjecture} +\newtheorem{Construction}[Result]{Construction} +\newtheorem{Convention}[Unnumbered]{Convention} +\newtheorem{Corollary}[Result]{Corollary} +\newtheorem{Counterexample}[Result]{Counterexample} +\newtheorem{Definition}[Result]{Definition} +\newtheorem{Example}[Result]{Example} +\newtheorem{Examples}[Result]{Examples} +\newtheorem{Exercise}[Result]{Exercise} +\newtheorem{Exercises}[Result]{Exercises} +\newtheorem{Fact}[Result]{Fact} +\newtheorem{Facts}[Result]{Facts} +\newtheorem{Lemma}[Result]{Lemma} +\newtheorem{NB}[Unnumbered]{NB} +\newtheorem{Notation}[Result]{Notation} +\newtheorem{Note}[Unnumbered]{Note} +\newtheorem{Observation}[Result]{Observation} +\newtheorem{Observations}[Result]{Observations} +\newtheorem{Problem}[Result]{Problem} +\newtheorem{Proposition}[Result]{Proposition} +\newtheorem{PS}[Unnumbered]{PS} +\newtheorem{Remark}[Result]{Remark} +\newtheorem{Question}[Result]{Question} +\newtheorem{Questions}[Result]{Questions} +\newtheorem{Theorem}[Result]{Theorem} +\newtheorem{Thesis}[Result]{Thesis} +\newtheorem{Warning}[Result]{Warning} + diff --git a/Master/texmf-dist/source/latex/proofs/taylor/QED.sty b/Master/texmf-dist/source/latex/proofs/taylor/QED.sty new file mode 100644 index 00000000000..bdf443cee19 --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/QED.sty @@ -0,0 +1,731 @@ +\message{<Paul Taylor's right-justified end-of-proof mark, 24 June 1995>} +%%======================================================================== +%************************************************************************% +%* *% +%* Maybe you already have a \qed macro to put a little square *% +%* on the right hand side at the end of a mathematical proof? *% +%* *% +%* IT'S PROBABLY MINE! *% +%* *% +%* Please compare yours with \parag@pushright below. *% +%* *% +%* This new file is compatible, it fixes the bugs, has extra *% +%* features, and is maintained and portable. Please use it! *% +%* *% +%* NEW FEATURE \WillHandleQED and \HandleQED for environments *% +%* which do not give access to the right hand side of the page. *% +%* *% +%* Now also available: \DefineStandardTheorems or *% +%* \usepackage[define-standard-theorems]{QED} *% +%* *% +%************************************************************************% +%========================================================================% + +% COPYRIGHT (C) 1993-6 Paul Taylor, Department of Computer Science, +% Queen Mary & Westfield College, London E1 4NS. +% You may use this file for any purpose. You may copy it on condition that +% you do so in exactly the form in which it was supplied, make no charge +% for the copy and impose the same conditions on the recipient. +% This software is supplied ``as is'' without warranty, express or implied, +% including but not limited to merchantability and fitness for any particular +% purpose. No liability is accepted by the author, Queen Mary and Westfield +% College, Imperial College or any third party for any direct or consequential +% damages, however caused. +% In all cases you must keep several backup versions of your files in a place +% to which your machine cannot write, and you must check documents visually +% before submitting the final version to a publisher or expensive printer. + +% WARNING: If you use this with Frank Mittlebach's "theorem.sty" you +% MUST load theorem first, then QED, then do the \newtheorem commands. + +% Authoritative version: /pub/tex/contrib/pt/proofs/QED.sty +% by anonymous FTP from: ftp.dcs.qmw.ac.uk +% also CTAN: macros/generic/proofs/taylor/QED.sty +% author/maintained by: Dr Paul Taylor <pt@dcs.qmw.ac.uk> + +% WARNING: This file replaces some of the functions of "Paul.sty" +% and MUST NOT be used with it as serious conflicts will arise. + +%========================================================================= + +% USER INTERFACE AND EXAMPLES (see also OPTIONS below) + +% LaTeX2e \usepackage options: see \DeclareOption commands below +% theorems-as-commands roman-theorems italic-theorems +% auto-QED explicit-QED number-theorems dont-number-theorems +% black-square open-square + +% \begin{Proof} ... \end{Proof} +% or \Proof ... \endProof +% or \Proof ... \endproof +% or \Proof ... \qed also \QED \QEF and \QEI + +% WARNING: \qed which doesn't follow \Proof will not print the square. + +% Each properly nested Proof/endProof pair gets a single +% \qedsymbol at the end, on the far right hand side. +% Unfortunately, this may still be in the wrong place +% if the proof ends with a display or itemisation. +% To solve this, \qed may be put *inside* the last substantive +% environment; the \qedsymbol will be put at that point +% (the visual end) and suppressed at the logical end of proof. + +% Examples: +% \begin{Proof} \begin{Proof} +% ... ... +% \begin{eqnarray} \begin{itemize} +% ... &=& ... \\ \item ... +% .. &=& ... &\qed \item ... \qed +% \end{eqnarray} \end{itemize} +% \end{Proof} \end{Proof} +% also works with $$...$$ and \[...\] displays, including fleqn.sty. + +% Unfortunately some environments, such as picture, do not allow this at all. +% See the section "centering environments" below for the mechanism for +% passing \qed to such an environment for special processing. + +% In fact \qed will only work in those environments which provide access to +% the right hand side of the page. In other words, wherever you think +% "\hfill\square" ought to work then \qed will; of course it is just because +% that naive method doesn't work that this macro file is needed at all. +% The macro was designed to solve the problem in the case of "unrestricted +% horizontal mode" (ie at the end of a paragraph); it also works in $$ +% displays by pretending to be an equation number. In most other cases it +% basically does "\hfill\square" or "\hfill$\square$" and hopes for the best. + +% If you have to put \qed outside the environment, it may be appropriate to +% put \vskip-\baselineskip before it, unless of course this would over-print. +% There is, however, still a danger that TeX will break the page here. +% This seems to be unavoidable if the environment ends with a \penalty. + +% The eqnarray example above does not in fact work: if you try it you'll +% get "! Paragraph ended before \llap was complete" with LaTeX in a mess. +% This is a very common place where you might want to put the end of proof +% mark, and I also consider that the fourth column should be available for +% "reasons" for equational steps. The following substitute for \eqnarray +% allows this, whilst being compatible with automatic numbering. I have +% proposed it to Rainer Sch\"opf for inclusion in LaTeX. If you want to +% use it, please copy it to another file rather than uncommenting it here. +% Don't forget to use \makeatletter or put it in a documentstyle (.sty) file. +% +% \def\eqnarray{\stepcounter{equation}\let\@currentlabel\theequation +% \global\@eqnswtrue\m@th\global\@eqcnt\z@\tabskip\@centering\let\\\@eqncr +% $$\halign to\displaywidth\bgroup\@eqnsel\hskip\@centering$\displaystyle +% \tabskip\z@{##}$&\global\@eqcnt\@ne\hskip 2\arraycolsep \hfil${##}$\hfil +% &\global\@eqcnt\tw@\hskip2\arraycolsep$\displaystyle\tabskip\z@{##}$\hfil +% \tabskip\@centering&% +% \global\@eqcnt\thr@@\hbox to\z@\bgroup\hss##%*** instead of "\llap{##}" +% \tabskip\z@\cr}% +% \def\@@eqncr{\let\@tempa\relax +% \ifcase\@eqcnt \def\@tempa{& & &}\or \def\@tempa{& &}% +% \or\def\@tempa{&}\else\@eqnswfalse%*** instead of "\else\def\@tempa{&}" +% \fi\@tempa\if@eqnsw\@eqnnum\stepcounter{equation}\fi +% \egroup%*** added, to match \bgroup in fourth cell of preamble +% \global\@eqnswtrue\global\@eqcnt\z@\cr} + +% Why can't we do all of this with \endProof? Because by that stage +% the damage has been done: the environments, paragraphs or +% displays have already been closed and their \hbox'es added +% to the current vertical list, and cannot be removed for +% alteration if this is the current page. + +% Even if you don't need to put \qed inside an inner environment +% to avoid a blank line, it's still a good idea to do so, because +% otherwise it's possible that intervening end-of-environment +% material may allow TeX to put the mark on the next page. + +% This file may be called QED.sty, QED.tex, qed.sty or qed.tex. +% It may be loaded using \input, \usepackage or as a \documentstyle option, +% as it is careful to handle the \catcode of @ appropriately. + +% If you don't use theorem.sty, this file instead provides options to use +% commands to begin theorems, instead of enclosing them in environments, +% and to suppress numbering and italicisation. A rudimentary version of +% \newtheorem for plain TeX is also implemented (always using commands +% rather than environments). + +% At the end of the file some useful \newtheorem +% commands are listed but not executed. + +% NB \Theorem\Proof\endProof\qed will print the second square, whereas +% \begin{Theorem}\end{Theorem}\begin{Proof}\end{Proof}\qed will not. + +%========================================================================= +% Make @ letter, saving its old code to restore at the end of this file. +% Look for this towards the end of the file if you think something's missing! +% "plain.tex" defines \lq as a synonym for back quote (character constant); +% I use it to avoid corruption when sending TeX files by email via BITNET. +\edef\qedrestoreat{\noexpand\catcode\lq\noexpand\@=\the\catcode\lq\@}%% +\catcode\lq\@=11 + +% in LaTeX, \protect the user commands; +% in plain TeX, ensure that it is defined. +\ifx\protect\undefined\let\protect\relax\fi + +%========================================================================= + +% OPTIONS + +% These are the user commands. + +\def\qed{\protect\@qed{$\qedsymbol$}}% suppressible printing of \qedsymbol +% \pushright takes an argument, which it always prints +% it is (re)defined by \WillHandleQED and \UnHandleQED below (12.4.94) + +% theoremata in Euclid needed proof: "which was to be shown" +\def\QED{\protect\@qed{{\rm Q.E.D.}}}% "quod erat demonstrandum" + +% but problemata needed construction: "which was to be found" +\def\QEI{\protect\@qed{{\rm Q.E.I.}}}% "quod erat inveniendum" + +% alternatively: "which was to be done/made" +\def\QEF{\protect\@qed{{\rm Q.E.F.}}}% "quod erat faciendum" + +% a LaTeX environment +\def\Proof{\protect\@Proof}\def\endProof{\protect\@endProof}% +\let\proof\Proof\let\endproof\endProof + + +% These are the user-settable parameters. + +% The actual (maths) symbol used by \qed +\def\qedsymbol{\square}% PLEASE NOTE: this is in the AMS symbols font. +%\def\qedsymbol{\blacksquare}% use one of these instead +%\def\qedsymbol{\hbox{\rm Q.E.D.}}% if you prefer +%\def\qedsymbol{\dashv}% this is what the Journal of Symbolc Logic likes. + +% This is the text used by \Proof. +% A new paragraph is begun without indentation. +% Change it to {\kern\parindent\sc D\'emonstration: } if you like. +\def\TheWordProof{\bf Proof\enskip} + +% This is the font command used for the text of proofs +\def\ProofFont{} + +% The command \AutoQEDtrue causes a \qed in \end{Theorem}, so you do +% \begin{Theorem} ... \begin{Proof} ... \end{Proof} \end{Theorem} +% but if you omit the proof, the statement gets a little square at the end. +\newif\ifAutoQED\AutoQEDfalse + +% The remaining options are redundant with theorem.sty +% so are not defined if this has been loaded. +\newif\ifNumberResults +\ifx\theorem@style\undefined + % + % How to print the name (#1), number (#2) and attribution (#3) of a theorem. + \NumberResultstrue + % If the number (#2) is absent, "\unskip" removes the + % unwanted space "\ " from before it (16 Feb 1993). + \def\TheoremHeader#1#2#3{\bf #1\ifNumberResults\ #2\unskip\fi#3} + % + % This is the font command used for the text of theorem enunciations + % change to {\rm} or {\small} if you like. + \def\TheoremFont{\it} + % + % The command \NumberResultsfalse will suppress theorem numbering. + % + % The command \TheoremsAsCommands will allow you to write + % \Theorem instead of \begin{Theorem} ... \end{Theorem}. + % In this case italicisation is suppressed by default. + % To do this with theorem.sty would involve rewriting the substyles. + % + % WARNING: if you subsequently redefine \TheoremFont, and use the command + % instead of the environment, the font will remain in force afterwards! +\fi + +% The document style option "theorems-as-commands" will allow you to +% write \Theorem instead of \begin{Theorem} ... \end{Theorem}. +% Moved here from further down. 10 Jan 1994 +\def\TheoremsAsCommands{% + \def\TheoremFont{}% suppress italicised theorems. + \def\begin@theorem##1{% + \par\removelastskip\smallskip + \save@set@qed % enable \qed + \noindent{##1}% the name + %\TheoremFont % italicise at your own risk! + }% + \def\@endtheorem{\ifAutoQED\qed\fi\restore@qed}% +}% + +\expandafter\let\csname ds@theorems-as-commands\endcsname\TheoremsAsCommands + +%========================================================================= +% If you already have a macro called \qed, \endproof or \pushright +% which is laid out in a similar way to the following two definitions +% (but with \hbox@pushright incorporated) then it is almost certainly +% my code, which has been copied anonymously via numerous people since +% my Cambridge PhD thesis in August 1986. Belated acknowledgements to +% Chris Thompson of the Cambridge University Computing Service for his +% help with my early attempts at TeX, in particular this problem. + +% The complexity of the macro necessary to get a little box on the +% right-hand-side at the end of a proof is amazing. It really does +% have to be this long! Otherwise you're liable to get it at the +% beginning of the next line, or even on the next page. + +\def\parag@pushright#1{{% set up + \parfillskip=0pt % so \par doesnt push \square to left + \widowpenalty=10000 % so we dont break the page before \square + \displaywidowpenalty=10000 % ditto + \finalhyphendemerits=0 % TeXbook exercise 14.32 + % + % horizontal + %\leavevmode % not needed since we now only use it in hmode + \hbox@pushright % this used to be incorporated + #1% % the end-of-proof mark (or whatever) + % + % vertical + \par}}% % build paragraph with the above parameters + +\def\hbox@pushright{% horizontal + \unskip % remove previous space or glue + \nobreak % don't break lines + \hfil % ragged right if we spill over + \penalty50 % discouragement to do so + \hskip.2em % ensure some space + \null % anchor the following \hfill + \hfill % push \square to right +}% + +% Ideally \endProof should do all this. We should be able to add the symbol +% to the last line after the paragraph, display or whatever other structure +% has been completed and we've returned to vertical mode. This isn't possible +% on the current page (outer vmode) because \lastbox doesn't work there. + +% But \ifinner is true inside a \vbox, \vadjust or \insert (LaTeX \parbox, +% minipage, figure or table), and in these circumstances we can use \lastbox. +% We would have to strip & restore glue & penalties (\insert, \mark and \write +% are obstacles to this) to get access to the last line (box), which may +% still not have the correct baseline. We could check its natural width +% against the page width, but if we re-set it, centering and (right) +% justification might be disturbed. Is this worth the trouble? +\def\vbox@pushright#1{\expandafter\message % (2 Jan 1994) + {QED.sty could be improved in this case (line \the\inputlineno): please ask}% + \page@pushright{#1}}% + +% Using this method the Proof environment could be implemented by collecting +% the entire proof in its own \vbox, modifying that and \unvbox'ing it to the +% current page. This approach may lead to the following problems: +% (i) footnotes, floats, marginpars, labels and index items may be lost; +% (ii) overflow of TeX's main memory, especially if \end{Proof} is missing; +% (iii) I don't know how page-breaking would be handled. + +%======================================================================== + +% Switch to enable/suppress \qedsymbol; since suppression may be done +% within a nested scope it must be global, so we do our own save/restore +% in a symbol which is local to the Proof environment. +% On first use, we check to see whether an obsolete version of Paul.sty +% is around, and complain loudly if it is, because they interfere seriously. + +\newif\if@qed\@qedfalse +\def\save@set@qed{\check@pt@sty@v\let\saved@ifqed\if@qed\global\@qedtrue}% +\def\restore@qed{\global\let\if@qed\saved@ifqed} + +% prefer proofs with statements if possible - hence \penalty700 +% the only essential part of this is \save@set@qed +\def\@Proof{% + \par\removelastskip\smallskip\penalty700 + \save@set@qed + \noindent\ProofFont{\TheWordProof\enskip}% +}% + +\def\@endProof{% + \qed\restore@qed + \penalty-700 \smallskip +} + +\def\@qed#1{\check@pt@fm@thm +\if@qed % have we already done \qed? + \global\@qedfalse\pushright{#1}% - no - do it now, but not again +\else\ifhmode\ifinner\else\par\fi\fi% - yes - just end paragraph, if any +\fi} + +% \pushright{text} always prints its argument, on the far right, in text mode +\def\@pushright#1{% + \ifvmode + \ifinner\vbox@pushright{#1}% vertical mode (see comments above) + \else \page@pushright{#1}% + \fi + \else\ifmmode\maths@pushright{\hbox{#1}}% maths (force a text argument) + \else\ifinner\hbox@pushright{#1}% inside an \hbox + \else\parag@pushright{#1}% in a paragraph + \fi \fi \fi +}% (22 Feb 1993) removed extra {} which would destroy our \] below + +% In the \hbox and maths cases we are really at the mercy of the environment. +% Assuming that we have $\qed$ simply embedded in a paragraph, the horizontal +% processing by \hbox@pushright will at least make sure that the square isn't +% at the beginning of the line, but we can't stop it being on the next page. +% However it is more likely that the reason why we're in maths mode is that +% we're inside an eqnarray or similar, in which case \hfill will do its best +% to put the square on the right of the available space. (See \vadjust below.) +\def\maths@pushright#1{% + \ifinner + \hbox@pushright{#1}% + \else + \eqno#1% use TeX's right equation number feature (\eqno) within $$. + \def\]{$$\ignorespaces}% suppress LaTeX's error checking (HACK!) + \fi +}% (22 Feb 1993) removed extra {} which would destroy our \] above + +% outer vertical mode (the current page) +% There's very little we can do in these circumstances! +% Penalties still allow the page to be broken. +% If the user has put negative glue in, leave it alone. (15 Feb 1994) +\def\page@pushright#1{% 18 Jan 1994 + %\unpenalty % ineffective + \skip@\lastskip + \ifdim\skip@>\z@ + \unskip % remove \parskip, but only (15 Feb 1994) if it's positive + \else\skip@\z@\relax + \fi + %\unpenalty % TeX won't let me do this + \dimen@\baselineskip + \advance\dimen@-\prevdepth % save \prevdepth to make a strut + \nobreak % don't break the page here + \nointerlineskip + \hbox to\hsize{% + \setbox\z@\null + \ifdim\dimen@>\z@\ht\z@\dimen@\fi % simulate \baselineskip + \box\z@ + \hfill + #1}% + \vskip\skip@ % replace old \parskip +}% + +% An idea that didn't work: see TeXbook p188. (16 Feb 1993) +% Use \predisplaysize to find out the width of the previous box, +% in the case where it has already been completed. +% But this can only be used inside displays ($$), and a display in +% vertical mode begins a paragraph first, so we end up with +% \predisplaysize=\parindent+2em whatever happened in the previous +% paragraph. + +% Another idea: it may be worth trying \vadjust, if only to insert \nobreak. +% The problem with this is that if we are too deeply nested in horizontal +% or maths lists, the adjustment may not be able to find its way out to the +% enclosing vertical list. In the case of array-like environments, it will +% appear (assuming it manages to get out) after the current row of the array. + +%=========================================================================== +% We have to add to the theorem environments the commands to enable \qed. +% This is done by re-defining \@thm#1#2. +% Note that Mittelbach's theorem.sty re-defines \@thm and \@endtheorem, so +% that must be loaded before us, otherwise our changes will get over-written +% and \qed will never be enabled. +% Paul.sty didn't use this method of gaining control inside a theorem, +% whereas it did define \qed and \pushright, so here is the one place +% where we can check for it. + +\ifx\nonqed@thm\undefined % otherwise double loading causes a loop 22 Feb 1993 + \let\nonqed@thm\@thm % save original + \let\nonqed@endthm\@endtheorem +\fi + +\def\@thm{\save@set@qed\nonqed@thm}% +\def\@endtheorem{\ifAutoQED\qed\fi\restore@qed\nonqed@endthm}% + +%=========================================================================== +% "CENTERING" ENVIRONMENTS - +% those which don't give their contents access to the right hand side +% of the page, such as center, picture, ... (12 April 1994) + +% Each individual environment (both the standard ones and those defined +% by the user) needs to co-operate in order to make \qed and \pushright work. +% It is not the business of this package to rewrite LaTeX in this way, +% but the following mechanism may be inserted in to other environments. +% - put \WillHandleQED in the \begin part of the environment definition; +% then if a \qed occurs in the body of the environment it is stored +% in \QEDbox until... +% - \HandleQED anywhere in the \end part of the environment definition +% (even inside dollars, braces or another environment) prints it. +% +% For example: +% \newenvironment{qedpicture}% +% {\begin{picture}\WillHandleQED}% +% {\put(0,0){\HandleQED}\end{picture}} +% +% To make this compatible with *not* loading QED.sty, +% add the following to macro files which use \WillHandleQED and \HandleQED: +% \ifx\WillHandleQED\undefined +% \let\WillHandleQED\relax +% \let\HandleQED\relax +% \let\UnHandleQED\relax % if you use it +% \let\QEDbox\voidb@x % must have \makeatletter here! +% \fi +% +% \UnHandleQED restores normal processing; this may be useful for +% the minipage environment, which has its own notion of "right hand side" +% of the page. +% +% The width of the saved \qed is available for testing as \wd\QEDbox + +\newbox\qed@box % the box in which to save \qed for special handling + +\def\WillHandleQED{\relax +\ifx\HandleQED\nohandle@qed + % no enclosing environment has declared \WillHandleQED + \def\pushright{\global\setbox\qed@box\hbox}% \qed will be saved + \let\QEDbox\qed@box % point at the right box + \def\HandleQED{\unhbox\QEDbox}% print it + \aftergroup\check@handle@qed % check that this really gets done +\else + % an enclosing environment already wants to catch \qed + % \HandleQED doesn't print anything - let the saved \qed pass through + \let\QEDbox\voidb@x % by pointing at an empty box +\fi} + +\def\nohandle@qed{% +\errhelp{One of them is missing: see QED.sty.}% +\errmessage{This environment uses \string\WillHandleQED\space and +\string\HandleQED\space incorrectly}} + +\def\check@handle@qed{\relax +\ifvoid\qed@box\else\expandafter\nohandle@qed\fi} + +\def\UnHandleQED{% +\let\HandleQED\nohandle@qed +\let\QEDbox\voidb@x +\def\pushright{\protect\@pushright}}% + +\UnHandleQED + +%=========================================================================== +% Check for obsolete versions and clashes of this and other macro files. +% Why do I do this? Because of those people who complain to me that +% something doesn't work but refuse to read the manual, and those +% who refuse to update their software, and then publish papers with +% commutative diagrams full of the bugs which I fixed several years ago. + +\def\obsolete@pt@version#1{\errhelp={% +% ***************************************************************** +% * The master version is available by * + Anonymous FTP ftp.dcs.qmw.ac.uk /pub/tex/contrib/pt/tex/#1}%* +% ***************************************************************** +\errmessage{You have an obsolete version of #1 - please get a new one}}% + +% First check QED.sty +%\ifnum\year>1996 \obsolete@pt@version{QED.sty}\fi + +% If theorem.sty hasn't been loaded, arrange to check it again in \@qed. +% And check (then) whether you've actually defined \square. +% changed 2 June 1993: don't define it now, as that would confuse amssymb.sty +\ifx\theorem@style\undefined + \def\check@pt@fm@thm{\relax + \ifx\square\undefined + \gdef\square{\bigcirc + \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}% + \errmessage{\string\square\space is an AMS symbol}% + \global\let\square\bigcirc}% + \fi + \ifx\theorem@style\undefined + \global\let\check@pt@fm@thm\relax + \else\errhelp={The macros \@thm and \@endtheorem need to be re-defined.}% + \errmessage{QED.sty must be loaded AFTER theorem.sty but before + using \string\newtheorem}% + \fi + \global\let\check@pt@fm@thm\relax + }% +\else + \def\check@pt@fm@thm{% + \ifx\square\undefined + \def\square{\bigcirc + \errhelp={Anonymous ftp e-math.ams.com /ams/amsfonts}% + \errmessage{\string\square\space is an AMS symbol}% + \global\let\square\bigcirc}% + \fi + \global\let\check@pt@fm@thm\relax + }% +\fi + +% Check for Paul.sty, which SERIOUSLY conflicts with this file. +% and also for version 2 or version 3 of commutative diagrams. +\def\check@pt@sty@v{% + \relax + \ifx\@@begintheorem\undefined + \else\message{*** QED.sty and the old Paul.sty seriously conflict! ***}% + \obsolete@pt@version{Paul.sty}% + \fi + \ifx\execHorizontalMap\undefined + \gdef\obsolete@pt@version##1{}% it's no longer needed + \else\global\let\di@gr@m\diagram + \gdef\diagram{\obsolete@pt@version{diagrams.tex}\di@gr@m}% + \fi + \global\let\check@pt@sty@v\relax +}% + +%=========================================================================== + +% Define some standard ``theorem'' types. + +\def\DefineStandardTheorems{% +% +% First set up uniform numbering in LaTeX; +% don't use this in plain TeX because this usage of \newcommand is not +% supported and we have already done by hand what it would do in LaTeX, +% viz to define the macro \theResult and the count \c@Result. +\relax\ifx\@@thm\undefined + \newtheorem{Result}{Result}[subsection]% + \@addtoreset{Result}{section}% + \ifx\chapter\undefined\else\@addtoreset{Result}{chapter}\fi +\fi +% +\let\theUnnumbered\relax\countdef\c@Unnumbered255 \def\p@Unnumbered{}% +\let\DefineStandardTheorems\relax +% +\newtheorem{Answer}[Result]{Answer}% +\newtheorem{Answers}[Result]{Answers}% +\newtheorem{Conjecture}[Result]{Conjecture}% +\newtheorem{Construction}[Result]{Construction}% +\newtheorem{Convention}[Unnumbered]{Convention}% +\newtheorem{Corollary}[Result]{Corollary}% +\newtheorem{Counterexample}[Result]{Counterexample}% +\newtheorem{Definition}[Result]{Definition}% +\newtheorem{Example}[Result]{Example}% +\newtheorem{Examples}[Result]{Examples}% +\newtheorem{Exercise}[Result]{Exercise}% +\newtheorem{Exercises}[Result]{Exercises}% +\newtheorem{Fact}[Result]{Fact}% +\newtheorem{Facts}[Result]{Facts}% +\newtheorem{Lemma}[Result]{Lemma}% +\newtheorem{NB}[Unnumbered]{NB}% +\newtheorem{Notation}[Result]{Notation}% +\newtheorem{Note}[Unnumbered]{Note}% +\newtheorem{Observation}[Result]{Observation}% +\newtheorem{Observations}[Result]{Observations}% +\newtheorem{Problem}[Result]{Problem}% +\newtheorem{Proposition}[Result]{Proposition}% +\newtheorem{PS}[Unnumbered]{PS}% +\newtheorem{Remark}[Result]{Remark}% +\newtheorem{Question}[Result]{Question}% +\newtheorem{Questions}[Result]{Questions}% +\newtheorem{Theorem}[Result]{Theorem}% +\newtheorem{Thesis}[Result]{Thesis}% +\newtheorem{Warning}[Result]{Warning}% +} + +%=========================================================================== +% Interaction with LaTeX2e (2 Jan 1994) + +\ifx\newtheorem\undefined\else\ifx\ProvidesPackage\undefined + \message{^^J^^J}% + \message{****************************************************************}% + \message{! ***** You are using an obsolete implementation of LaTeX ******}% + \message{* A new version - called LaTeX2e - has been available from TeX *}% + \message{* FTP archives such as ftp.tex.ac.uk, ftp.uni-stuttgart.de and *}% + \message{* pip.shsu.edu since December 1993. It incorporates NFSS2 (the *}% + \message{* Mittelbach-Schoepf New Font Selection Scheme) but is reverse *}% + \message{* compatible with LaTeX versions 2.09 and is now the standard. *}% + \message{****************************************************************}% + \message{^^J^^J}% +\else + \ProvidesPackage{QED}[1996/06/24 right-justified end-of-proof mark]% + %\ProvidesFile{QED.sty}% I don't understand what this is for + \DeclareOption{roman-theorems}{\def\TheoremFont{\rm}}% + \DeclareOption{italic-theorems}{\def\TheoremFont{\it}}% + \DeclareOption{theorems-as-commands}{\TheoremsAsCommands}% + \DeclareOption{auto-QED}{\AutoQEDtrue}% + \DeclareOption{explicit-QED}{\AutoQEDfalse}% + \DeclareOption{number-theorems}{\NumberResultstrue}% + \DeclareOption{dont-number-theorems}{\NumberResultsfalse}% + \DeclareOption{black-square}{\def\qedsymbol{\blacksquare}}% + \DeclareOption{open-square}{\def\qedsymbol{\square}}% + \DeclareOption{define-standard-theorems}{\DefineStandardTheorems}% + \ProcessOptions +\fi\fi + +%=========================================================================== +% If Mittelbach's theorem.sty is loaded, skip the rest of the file. +\ifx\theorem@style\undefined\else\qedrestoreat\expandafter\endinput\fi +%=========================================================================== + +% Allow the user to suppress italicisation and numbering. + +% The following two macros are called by LaTeX to begin a theorem +% respectively with and without an optional (``attribution'') argument. +% It is clear from latex.tex that they are intended to be customised. +% The code common to the two has been taken out as \begin@theorem and +% \TheoremHeader. Of these, the former is re-defined by \TheoremsAsCommands. + +\def\@opargbegintheorem#1#2#3{\begin@theorem{\TheoremHeader{#1}{#2}{ (#3)} }} + +\def\@begintheorem#1#2{\begin@theorem{\TheoremHeader{#1}{#2}{} }} + +\def\begin@theorem#1{% + \trivlist\item[\hskip\labelsep {#1}]% % LaTeX likes this method. + \TheoremFont % Italicise the enunciation + \ifx\ProofFont\empty\def\ProofFont{\rm}\fi % but not any nested proof. + }% + + +%%% Here's what LaTeX (92/1/14) does: +%%%% RmS 91/08/14 Moved \it after \item to make it work with NFSS +%%\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]\it} +%%\def\@opargbegintheorem#1#2#3{\trivlist +%% \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]\it} +%%\def\@endtheorem{\endtrivlist} + + + +%=========================================================================== +% If we're running under LaTeX, skip the rest of the file. +\ifx\newtheorem\undefined\else\qedrestoreat\expandafter\endinput\fi +%=========================================================================== + +% This implements a rudimentary version of \newtheorem for plain TeX. +% Only the unattributed theorems and the +% declarations \newtheorem{Theorem}[Result]{Theorem} and +% \newtheorem{Convention}[Unnumbered]{Convention} are supported. +% The numbering is based on the counts \chapternumber, \sectionnumber +% and \subsectionnumber, which it is up to you to define with \newcount. +% It's also up to you to reset \c@Result at the beginning of each section. + +% Form the number: (chapter).(section).(subsection).(#1) +% where any of the first three parts which is zero +% negative or undefined is omitted. +\def\ther@sult#1{% +\ifx\chapternumber\undefined\else + \ifnum\chapternumber>0 \number\chapternumber.\fi\fi +\ifx\sectionnumber\undefined\else + \ifnum\sectionnumber>0 \number\sectionnumber.\fi\fi +\ifx\subsectionnumber\undefined\else + \ifnum\subsectionnumber>0 \number\subsectionnumber.\fi\fi +\expandafter\number\csname c@#1\endcsname}% + +% plain version of LaTeX's \@thm +\def\plain@thm#1#2{% #1=counter, #2=text + \save@set@qed + \expandafter\advance\csname c@#1\endcsname1 + \@begintheorem{#2}{\csname the#1\endcsname}% +}% + +% Rudimentary \newtheorem +\def\newtheorem#1[#2]#3{% #1=command, #2=counter, #3=text + % + % \def\#1{\plain@thm{#2}{#3}} + \expandafter\def\csname #1\endcsname{\plain@thm{#2}{#3}}% + % + % \def\end#1{\@endtheorem} + \expandafter\def\csname end#1\endcsname{\@endtheorem}% + % + % if \c@#2 is not defined + % \newcount\c@#2 + % \def\the#2{\ther@sult{#2}} + \expandafter\ifx\csname c@#2\endcsname\relax + \expandafter\expandafter\csname newcount\endcsname + \csname c@#2\endcsname + \expandafter\def\csname the#2\endcsname{\ther@sult{#2}}% + \fi +}% + +\TheoremsAsCommands + +\qedrestoreat\endinput + +%=========================================================================== +% BUGS +% \item\qed\end{letterlist} puts the square above the item label. + +% ! You can't use `\unskip' in vertical mode. +% from \qed in a paragraph on its own. diff --git a/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex b/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex new file mode 100644 index 00000000000..e42924bb08d --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/boxproof-old.tex @@ -0,0 +1,142 @@ +% mangletex (11 May 1992) run at 19:39 BST Monday 29 June 1992 +\message{<Paul Taylor's Proof Boxes, 29 June 1992>}%% +%%======================================================= +%% There is now a PROTOTYPE proof-box macro mackage for TRIAL only. +%% The syntax and implementation may change. +%% It is "boxproof.tex" in the TeX system (so just "\input boxproof"). +%% There are some examples in ~pt/utilities/misctex/proofboxeg.tex and +%% proofboxeg1.tex. +%% +%% Syntax as follows: +%% each line is of the form +%% <all/exists_variables> <latex_label> \: <formula> \= <reason> \\ +%% where +%% <all/exists_variables> is something like "x,y" - its for variables +%% declared at the beginning of all-intro and exists-elim boxes +%% <latex_label> is a command "\label{fred}" which defines "fred" to +%% be the label text, which may be used anywhere as "\ref{fred}" +%% - see LaTeX book. +%% <formula> is the proposition being asserted +%% <reason> is "\intro\land(\ref{john},\ref{mary})" +%%% note that the parts are separated by "\:", "\=" and "\\"; these correspond +%% to "let identifier = expression : type" in a declarative language. +%% +%% Proof boxes are "wrapped up" as follows: +%% the whole proof in "\begin{proofbox}...\end{proofbox}" +%% single-column boxes (all-intro, implies-intro, exists-elim) in "\[...\]" +%% double-column boxes are of two kinds: +%% separate (and-intro) "\(...\*...\)" +%% stuck together (or-elim) "\(...\+...\)" +%% +%%% At the moment you may only have pairs of parallel boxes, and the width is +%%% split in two; later there will be options for mutiple boxes and adjustable +%% widths. +%% +%% Comments please. +%% +%% WARNING: this is for temporary use only at the moment. +%%======================================================= +\catcode`\@=11 \let\plaint@bplus\+\let\+\relax\newcount\prooflineinbox +\newcount\prooflineinnextbox\newcount\prooflinetotal\newcount\pr@@flinetotal +\newcount\pr@@flinemax\newcount\proofboxesacross\newdimen\prooflinenowidth +\newdimen\proofboxformulawidth\newdimen\proofboxrulebreadth\newdimen +\proofboxrulespace\newdimen\proofboxsurround\newdimen\proofboxmargin\newdimen +\pr@@fboxhadjust\newdimen\proofboxintercol\newif\ifinproofbox\newif +\ifleftmostproofbox\newif\ifparallelisand\newskip\proofboxlefttabskip\newskip +\proofboxrighttabskip\newskip\proofboxbaselineskip\def\runningproofline{% +\number\prooflinetotal}\def\nestedproofline{\ifinproofbox\enclosingproofline.% +\fi\number\prooflineinbox}\def\enclosingproofline{}\prooflinenowidth=1em +\proofboxformulawidth=15em \proofboxrulebreadth=.03em \proofboxrulespace=.2em +\proofboxsurround=.5em \proofboxlefttabskip=1em \proofboxrighttabskip=1em plus +1 fil \proofboxbaselineskip=1.8em \proofboxmargin=5em \proofboxintercol=3em +\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}% +\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@ +\hfill}\let\theproofline\runningproofline\def\proofboxmakelabel#1{{% +\ifleftmostproofbox\setbox0=\hbox{\hss\the\scriptfont1 #1}\ifdim\wd0<% +\prooflinenowidth\setbox0=\hbox to\prooflinenowidth{\unhbox0}\fi\box0 \fi}}% +\def\proofboxnonumbers{\def\proofboxmakelabel##1{}} \def\proofbox{\global +\prooflinetotal=0 \ifvmode\else\vtop\fi\bgroup\let\[\intofullpr@@fbox\let\(% +\intohalfpr@@fbox\let\:\pr@@fboxcolon\let\=\pr@@fboxequals\let\proofbox +\intofullpr@@fbox\proofboxesacross=1 \pr@@fb@x}\let\pr@@fb@x\csname\let +\endpr@@fb@x\endcsname\def\endproofbox{\endpr@@fb@x\proofboxmargin\z@\vskip1% +ex \unvbox9 \vskip1ex \egroup}\def\intofullpr@@fbox{\pr@@ffirst\pr@@fb@x}\def +\+#1{<"7C#1}\def\outofpr@@fbox{\endpr@@fb@x\z@\z@\endpr@@ffirst +\proofboxleftside\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f +\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\intohalfpr@@fbox{% +\pr@@ffirst\advance\proofboxformulawidth-\proofboxintercol\advance +\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \pr@@fb@x +}\def\pr@@fvalign{m}\def\orpr@@ffirst{\endpr@@fb@x\z@{.5\proofboxintercol}% +\endpr@@ffirst\proofboxleftside\advance\proofboxformulawidth-% +\proofboxintercol\advance\proofboxformulawidth-\proofboxsurround\divide +\proofboxformulawidth2 \let\*\orpr@@fmore\let\+\orpr@@fmore\let\]\orpr@@flast +\let\)\orpr@@flast\let\endproof\orpr@@flast\pr@@fvalign\putpr@@fedge +\proofboxleftside\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def +\putpr@@forsep{o}\def\orpr@@fmore{\endpr@@fb@x{.5\proofboxintercol}{.5% +\proofboxintercol}\putpr@@f\putpr@@forsep\proofboxorseparator\pr@@fb@x}\def +\putpr@@fedge{n}\def\orpr@@flast{\endpr@@fb@x{.5\proofboxintercol}\z@ +\putpr@@f\putpr@@fedge\proofboxrightside\endpr@@fvalign}\def\putpr@@f{t}\def +\endpr@@fvalign{h}\def\andpr@@ffirst{\endpr@@fb@x\z@\z@\endpr@@ffirst +\proofboxleftside\advance\proofboxformulawidth-\proofboxintercol\advance +\proofboxformulawidth-\proofboxsurround\divide\proofboxformulawidth2 \let\*% +\andpr@@fmore\let\+\andpr@@fmore\let\]\andpr@@flast\let\)\andpr@@flast\let +\endproof\andpr@@flast\pr@@fvalign\putpr@@fedge\proofboxleftside\putpr@@f +\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=\proofboxintercol\advance +\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2\dimen2 \pr@@fb@x}\def +\la@math{a}\def\andpr@@fmore{\endpr@@fb@x\z@\z@\hadjustandpr@@f\putpr@@fedge +\proofboxleftside\putpr@@f\putpr@@fedge\proofboxrightside\pr@@fboxhadjust=% +\proofboxintercol\advance\pr@@fboxhadjust-\dimen8 \advance\pr@@fboxhadjust-2% +\dimen2 \pr@@fb@x}\def\la@ket{r}\def\andpr@@flast{\endpr@@fb@x\z@\z@ +\hadjustandpr@@f\putpr@@fedge\proofboxleftside\putpr@@f\putpr@@fedge +\proofboxrightside\endpr@@fvalign}\def\hadjustandpr@@f{\advance +\pr@@fboxhadjust-\dimen6 \ifdim\pr@@fboxhadjust<\proofboxsurround +\pr@@fboxhadjust=\proofboxsurround\fi\hrule width\pr@@fboxhadjust height\z@ +depth\z@\cr}\def\pr@@fboxcr{\cr}\def\pr@@fboxequals{&}\def\pr@@fboxcolon{&}% +\ifnum\pr@@fb@x\pr@@fvalign\putpr@@forsep\putpr@@fedge\putpr@@f +\endpr@@fvalign\endpr@@fb@x<13\let\pr@@fmtb\relax\else\def\pr@@fmtb#1{}\fi +\def\pr@@ffirst{\omit\prooflineinnextbox=\prooflineinbox\edef +\enclosingproofline{\theproofline}%% its line label +\pr@@flinetotal=\prooflinetotal\let\endproofbox\outofpr@@fbox +\proofboxesacross=1 \let\+\orpr@@ffirst\let\*\andpr@@ffirst\let\)% +\outofpr@@fbox\let\]\outofpr@@fbox\inproofboxtrue}\def\la@bra{y}\def +\endpr@@ffirst#1{\setbox0=\vbox{#1}\global\advance\dimen6\wd0 \advance\dimen6% +\proofboxsurround\hskip\dimen6 plus 1fil \global\count@=\pr@@flinetotal&\omit +\setbox8=\hbox\bgroup\pr@@flinetotal=\count@\hskip-\dimen6 \pr@@flinemax=% +\prooflinetotal\global\prooflinetotal=\pr@@flinetotal\leftmostproofboxfalse +\inproofboxtrue}\def\pr@@fvalign{\valign\bgroup\vfil##&##&##\vfil&##&##\vfil +\cr}\def\endpr@@fvalign{\vfil&\vfil&\vfil&\vfil&\vfil\cr\egroup\setbox0=% +\lastbox\setbox0=\vbox{\unvbox0\unskip\setbox5=\lastbox\unskip\setbox4=% +\lastbox\unskip\setbox3=\lastbox\unskip\setbox2=\lastbox\unskip\setbox1=% +\lastbox\global\dimen9=\ht5 \global\advance\dimen9\dp5\global\advance\dimen9% +\ht4\global\advance\dimen9\dp4\global\dimen4=\ht1 \global\advance\dimen4\dp1% +\global\advance\dimen4\ht2\global\advance\dimen4\dp1}\global\advance\dimen8% +\dimen2\kern-\dimen8 \global\prooflinetotal=\pr@@flinemax\egroup\dimen0=\dp8 +\advance\dimen0-\dimen4 \vtop{\setbox0=\null\ht0=\dimen4 \dp0=-\dimen4 \box0% +\nointerlineskip\box8}\ifdim\dimen0<\z@\dimen0\z@\fi\advance\dimen0-\dimen9 +\vadjust{\vskip-\dimen0}&\omit\global\advance\dimen8\proofboxsurround\hskip +\dimen8 plus 1 fil \cr}\def\putpr@@fedge#1{\span\omit\span\omit\span\omit +\span\omit\setbox0=\vbox{#1}\global\dimen2=\wd0 \unvbox0\vfil\cr}\def +\la@displ{e}\def\putpr@@forsep#1{&\multispan3 \setbox0=\vbox{#1}\global\dimen +2=\wd0 \unvbox0 &\vfil\cr\noalign{\kern-\dimen2}}\def\putpr@@f{\hbox to\dimen +5{\proofboxtopside}&\advance\dimen4\proofboxrulespace\vskip\dimen4 plus 1fil&% +\vskip-\dimen4 \unvbox9 \vskip-\dimen9&\advance\dimen9\proofboxrulespace +\vskip\dimen9 plus 1 fil&\hbox to\dimen5{\proofboxbottomside}\cr}\ifnum +\pr@@fb@x\la@bra\la@displ\la@math\la@ket\endpr@@fb@x\+A\let\pr@@fytb\relax +\else\def\pr@@fytb#1{}\fi\def\pr@@fb@x{\global\setbox9=\vtop\bgroup +\nointerlineskip\global\prooflineinbox=0 \baselineskip=\proofboxbaselineskip +\tabskip=\z@\let\\\pr@@fboxcr\halign\bgroup\hskip\proofboxrulespace plus 1fil% +\let\(\la@math\let\[\la@displ\global\advance\prooflineinbox1 \global\advance +\prooflinetotal1 \edef\@currentlabel{\theproofline}$##\proofboxmakelabel +\@currentlabel$&\hskip\proofboxlefttabskip\let\(\la@math\let\[\la@displ$% +\displaystyle##$\hskip\proofboxrighttabskip&\let\(\la@math\let\[\la@displ$##$% +\hskip\proofboxrulespace plus1fil \cr}\def\endpr@@fb@x#1#2{\crcr\omit\hskip#1 +plus 1 fil&\omit\hskip\proofboxformulawidth plus 1fil&\omit\hskip#2 plus 1fil% +\cr\egroup\setbox0=\lastbox\unskip\global\dimen5=\wd0 \setbox0=\hbox{\unhbox0% +\unskip\setbox0=\lastbox\global\dimen8=\wd0\unskip\setbox0=\lastbox\global +\dimen7=\wd0\unskip\setbox0=\lastbox\global\dimen6=\wd0\unskip}\setbox0=% +\lastbox\global\dimen9=\dp0 \nointerlineskip\pr@@fytb{\box0}\egroup\global +\dimen4=\ht9 }\inproofboxfalse\leftmostproofboxtrue\let\la@bra\(\let\la@ket\)% +\def\la@math{\la@bra\let\)\la@ket}\def\la@displ{\la@bra\displaystyle\let\]% +\la@ket}\let\+\plaint@bplus\catcode`\@=12
\ No newline at end of file diff --git a/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex b/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex new file mode 100644 index 00000000000..fef01ef661d --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/boxproof.tex @@ -0,0 +1,427 @@ +% mangletex (11 May 1992) run at 22:09 GMT Monday 08 November 1993 +%%\title {\TeX\ macros for proof boxes} +%%\author {Paul Taylor\\ +%% Department of Computing,\\ +%% Imperial College,\\ +%% London SW7 2BZ\\ +%% +44 71 589 5111 {\em ext.} 5057\\ +%% {\tt<pt@doc.ic.ac.uk>}} +%%\date{8 November 1993} +%% % to get the provisional user documentation do +%% % grep ^%% boxproof.tex | sed 's/^%*//' > boxproof-manual.tex +%%\documentstyle{article} +%%\input boxproof.tex +%%\def\meta#1{\mbox{$\langle\hbox{#1}\rangle$}} +%%\def\macrowitharg#1#2{{\tt\string#1\bra\meta{#2}\ket}} +%%{\escapechar-1 \xdef\bra{\string\{}\xdef\ket{\string\}}} +%%\let\subsection\section +%%\begin{document} +%%\maketitle +%% +%% \subsection{Introduction} +%% The proof +%%\begin{proofbox} +%% \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\=\\ +%% \:\Some\beta.\psi(x,\beta)\=\mathsf{total}\\ +%% \[\exists\beta\kern-1em\:\psi(x,\beta)\\ +%% \(\:\beta\=\\ +%% \:\beta=\top\=(*)\\ +%% \:\psi(x,\!\top)\=\mathsf{subs}\\ +%% \:\alpha\=\elim\leftrightarrow(\ref{1})\\ +%% \*\:\alpha\=\\ +%% \:\psi(x,\!\top)\=\elim\leftrightarrow(\ref{1})\\ +%% \:\beta=\top\=\mathsf{func}\\ +%% \:\beta\=(*)\\ +%% \)\:\alpha=\beta\=\intro\leftrightarrow\\ +%% \:\psi(x,\alpha)\=\mathsf{subs}\\ +%% \] \:\psi(x,\alpha)\=\elim\exists\\ +%% \* \:\psi(x,\alpha)\=\\ +%% \(\:\alpha\=\\ +%% \:\alpha=\top\=(*)\\ +%% \:\phi(x,\!\top)\=\mathsf{subs}\\ +%% \*\:\psi(x,\!\top)\=\\ +%% \:\alpha=\top\=\mathsf{func}\\ +%% \:\alpha\=(*)\\ +%% \)\:\alpha\leftrightarrow\psi(x,\!\top)\=\intro\leftrightarrow\\ +%%% \) \:\psi(x,\alpha)\leftrightarrow(\alpha\leftrightarrow\psi(x,\!\top)) +%% \=\intro\leftrightarrow\\ +%%\end{proofbox} +%% is produced by +%%\begin{verbatim} +%%\begin{proofbox} +%% \(\"1"\:\alpha\leftrightarrow\psi(x,\top)\\ +%% \:\Some\beta.\psi(x,\beta) \=\mathsf{total}\\ +%% \[\exists\beta\kern-1em\:\psi(x,\beta)\\ +%% \(\:\beta\\ +%% \:\beta=\top \=(*)\\ +%% \:\psi(x,\!\top) \=\mathsf{subs}\\ +%% \:\alpha \=\elim\leftrightarrow(\ref{1})\\ +%% \*\:\alpha\\ +%% \:\psi(x,\!\top) \=\elim\leftrightarrow(\ref{1})\\ +%% \:\beta=\top \=\mathsf{func}\\ +%% \:\beta\=(*)\\ +%% \)\:\alpha=\beta \=\intro\leftrightarrow\\ +%% \:\psi(x,\alpha) \=\mathsf{subs}\\ +%% \] \:\psi(x,\alpha) \=\elim\exists\\ +%% \* \:\psi(x,\alpha)\\ +%% \(\:\alpha\\ +%% \:\alpha=\top \=(*)\\ +%% \:\phi(x,\!\top) \=\mathsf{subs}\\ +%% \*\:\psi(x,\!\top)\\ +%% \:\alpha=\top \=\mathsf{func}\\ +%% \:\alpha \=(*)\\ +%% \)\:\alpha\leftrightarrow\psi(x,\!\top) \=\intro\leftrightarrow\\ +%% \) \:\psi(x,\alpha)\leftrightarrow +%% (\alpha\leftrightarrow\psi(x,\!\top)) \=\intro\leftrightarrow\\ +%%\end{proofbox} +%%\end{verbatim} +%% +%% Syntax as follows: +%% each line is of the form +%% \begin{center} +%% \meta{variables} +%% \meta{name} +%% \verb/\:/ \meta{formula} +%% \verb/\=/ \meta{reason} +%% \verb/\-/ \meta{use} +%% \verb/\\/ +%% \end{center} +%% where +%% \begin{itemize} +%% \item \meta{variables} is something like ``$x,y$'' --- +%% it's for variables declared at the beginning of $\intro\forall$- and +%% $\elim\exists$-boxes. +%% \item \meta{name} is a command \verb/\label{fred}/ which +%% defines \verb/fred/ to be the label text, which may be used anywhere +%% as \verb/\ref{fred}/ --- see {\em The \LaTeX book.} +%% Local labels are also available, using \macrowitharg\lbl{name} +%% or \verb/\"/\meta{name}\verb/"/; these obey the scoping rules of +%% the boxes. +%% You may also refer to the previous line as \verb/\ref{-}/. +%% \item \meta{formula} is the proposition being asserted. +%% \item \meta{reason} is \verb/\intro\land(\ref{john},\ref{mary})/ +%% or \verb/\elim\forall(\ref{jim})/. +%% \item \meta{use} is provided for linear logic, to record the step +%%% which uses this one. How this accords with theory I don't yet know. +%% \end{itemize} +%% Note that the parts are separated by \verb/\:/, \verb/\=/ and \verb/\\/; +%% these correspond to +%% \begin{center} +%% {\bf let } \meta{name} = \meta{expression} : \meta{type} +%% \end{center} +%% in a declarative language. +%% The \verb/\:/, \verb/\=/ and \verb/\-/ fields are optional and may occur +%% in any order. If any of them is repeated the last is taken. +%% If none of them is present the \meta{variables} field is also ignored. +%% +%% Proof {\em boxes\/} are ``wrapped up'' as follows: +%% \begin{itemize} +%%% \item the whole proof in \verb/\begin{proofbox}/...\verb/\end{proofbox}/; +%%% \item single-column boxes ($\intro\forall$, $\intro\imp$, $\elim\exists$), +%% in \verb/\[/...\verb/\]/. +%% \item multiple-column boxes are of two kinds: +%% \begin{itemize} +%%% \item separate ($\intro\land$) boxes: \verb/\(/...\verb/\*/...\verb/\)/. +%% \item stuck together ($\elim\lor$) boxes: +%% \verb/\(/...\verb/\+/...\verb/\)/. +%% \end{itemize} +%% \end{itemize} +%% You may put more than two columns in \verb/\(/...\verb/\)/ and even mix +%% the \verb/\+/ and \verb/\*/ separators. +%% +%% The whole proof is enclosed in \verb/\proofbox/...\verb/\endproofbox/ +%% or \verb/\begin{proofbox}/...\verb/\end{proofbox}/, but the \LaTeX\ +%% environment form {\em must not\/} be used for nested boxes. +%% +%% If the proof occurs in paragraph mode (ie in vertical or +%% unrestricted horizontal mode) then it is set as a display, using the +%% full width of the page. Otherwise it uses only the required width. +%% +%% A lot of the internals are potentially configurable, but there is not +%% yet a user interface suitable for doing this. This will be provided +%% in the next version. +%% +%% This is a {\em prototype\/} proof-box macro package; +%% the syntax and implementation may change. +%% It is {\tt boxproof.tex} in the \TeX\ system +%% (so just \verb/\input boxproof/). +%% +%% There are some examples in +%% \verb+~pt/utilities/proofs/proofboxeg.tex+ and +%% \verb+proofboxeg1.tex+. +%% +%% The prototype version was begun on 2 August 1991, the new one on +%% 4 June 1993. +%% +%% +\message{<Paul Taylor's Proof Boxes, 8 November 1993>}\edef\proofboxrestoreat +{\noexpand\catcode`\noexpand\@\the\catcode`\@}\catcode`\@=11 \count@\year +\multiply\count@12 \advance\count@\month\ifnum\count@> 23970 \message{ ****** +This is an experimental version - please get an up-to-date one ******}% +\message{ by anonymous FTP theory.doc.ic.ac.uk /tex/contrib/Taylor/tex/% +boxproof.tex}\fi\let\pb@A\+\let\+\relax\let\pb@B\(\let\pb@C\)\def\pb@D{\pb@B +\let\)\pb@C}\def\pb@E{\pb@B\displaystyle\let\]\pb@C}%% +%% The following are user-settable dimensions. +%% +\newdimen\prooflinenowidth\prooflinenowidth1em \newdimen\proofboxfullwidth +\newdimen\proofboxleftmargin\proofboxleftmargin3em \newdimen +\proofboxrightmargin\newdimen\proofboxrulebreadth\proofboxrulebreadth.4pt +\newdimen\proofboxseparation\proofboxseparation.2em \newdimen +\proofboxbaselineskip\proofboxbaselineskip4ex %% +%% +%% The following are user-accessible numbers. +%% +\newcount\proofcolumns\newcount\prooflinetotal\newcount\prooflineinbox%% +%% +%% These boxes receive the fields of the proof steps. +%% They are used in \verb/\proofboxmakeleftcolumn/ {\em etc}. +%% +\newbox\proofboxproposition\newbox\proofboxreason\newbox\proofboxuse\newbox +\proofboxvariables%% +%% The left-most switch is used by +%%% \verb/\proofboxmakelabel/ to suppress the label in all but the first column. +%% On the outside it is true. +\newif\ifleftmostproofbox\leftmostproofboxtrue%% +%% +%% The following are obsolete: they are only included for reverse +%% compatibility with the prototype version. +\newdimen\proofboxintercol\newdimen\proofboxsurround\newdimen +\proofboxformulawidth\newdimen\proofboxmargin\newskip\proofboxlefttabskip +\newskip\proofboxrighttabskip%% +%% +%% \subsection{Redefinable macros} +%% WARNING: most of these commands will be hidden and replaced with +%% optional arguments to \verb/\proofbox/ in a future version. +%% Do not rely on them. +%% +%% We provide three different ways of numbering the lines of the proof: +%% \begin{itemize} +%% \item \verb/\runningproofline/: a global running sequence (default), +%% +\def\runningproofline{\number\prooflinetotal}%% +%% \item \verb/\nestedproofline/: a hierarchical system with dots, +%% +\def\nestedproofline{\relax\ifx\enclosingproofline\empty\else +\enclosingproofline{.}\fi\number\prooflineinbox}\def\enclosingproofline{}%% +%% \item \verb/\nestedproofline/: a fully hierarchical system which +%% also includes the column number +%% (\verb/\proof@columns/) as a letter (ASCII quote plus number). +%% +\def\proofboxcolumn{\ifnum\proofcolumns>\z@{\count@96\advance\count@ +\proofcolumns\char\count@}\fi}\def\fullynestedproofline{\relax\ifx +\enclosingproofline\empty\enclosingproofline\proofboxcolumn.\else +\proofboxcolumn\fi\number\prooflineinbox}%% +%% \end{itemize} +%% \verb/\theproofline/ is the default. +%% +\let\theproofline\runningproofline%% +%% The macro \verb/\proofboxmakelabel#1/ is used to print the line label. +%% We only put it in the leftmost box. +%% It is printed in small non-ranging Arabic numerals +%% ({\the\scriptfont1 0123456789}). +%% Right-justify it in \verb/\prooflinenowidth/ if it will fit, +%% otherwise let it stick out on the right, {\em i.e.}~left-justify it. +%% +\def\proofboxmakelabel#1{{\relax\ifleftmostproofbox\setbox\z@\hbox{\hss\the +\scriptfont\@ne#1}\ifdim\wd\z@<\prooflinenowidth\setbox\z@\hbox to% +\prooflinenowidth{\unhbox\z@}\fi\box\z@\quad\fi}}%% +%% Kill the numbers altogether with \verb/\proofboxnonumbers/. +%% +\def\proofboxnonumbers{\def\proofboxmakelabel##1{}}%% +%% How to make the left column of the proof box: +%% use the variables field, a space if necessary and the line label. +%% +\def\proofboxmakeleftcolumn{\kern\proofboxseparation\hfil\dimen@\wd +\proofboxvariables\unhbox\proofboxvariables\ifdim\dimen@>\z@\quad\fi +\proofboxmakelabel\@currentlabel}%% +%% How to make the middle column of the proof box: +%% left justify the formula field. +%% +\def\proofboxmakemiddlecolumn{\unhbox\proofboxproposition\hfil\quad}%% +%% How to make the right column of the proof box: +%% use the reason and use fields. +%% +\def\proofboxmakerightcolumn{\box\proofboxreason\box\proofboxuse\hfil\kern +\proofboxseparation}%% +%% +%% Make the four edges of a rectangular box and the separator +%% between \verb/\+/ columns. +%% +\def\proofboxleftside{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxrightside{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxorseparator{\leaders\hrule width\proofboxrulebreadth\vfill}\def +\proofboxtopside{\leaders\vrule height\proofboxrulebreadth depth\z@\hfill}% +\def\proofboxbottomside{\leaders\vrule height\proofboxrulebreadth depth\z@ +\hfill}%% +%% +%% Use dotted lines: \verb/\dottedproofbox/. +%% +\def\dottedproofbox{\def\proofboxleftside{\leaders\pb@F\vfill} \def +\proofboxrightside{\leaders\pb@F\vfill} \def\proofboxorseparator{\leaders +\pb@F\vfill} \def\proofboxtopside{\leaders\pb@F\hfill}\def\proofboxbottomside +{\leaders\pb@F\hfill}%% +}\def\pb@F{\vbox to 5pt{\vss\hbox to 5pt{\hss.\hss}\vss}}%% +%% Leave the boxes open at the bottom: \verb/\openproofbox/ +%% +\def\openproofbox{\def\proofboxbottomside{\hfill}} %% +%% \subsection{Miscellaneous logical notations} +%% +%% Print the names of the introduction and elimination rules, for example: +%% \begin{quote} +%% \verb/\elim\forall/ $\elim\forall$ \qquad +%% \verb/\intro\land/ $\intro\land$ \qquad +%% \end{quote} +\def\intro#1{{{#1}{\cal I}}}\def\elim#1{{{#1}{\cal E}}}%% +%% Recall that in \TeX\ the logical connectives and quantifiers are called +%% \begin{center} +%% \verb/\lor/ $\lor$\quad +%% \verb/\land/ $\land$\quad +%% \verb/\lnot/ $\lnot$\quad +%% \verb/\forall/ $\forall$\quad +%% \verb/\exists/ $\exists$ +%% \end{center} +%% The following provide macros for the \verb/\implies/ {\em relation\/} +%% and for the binary {\em operation\/} which yields the abstract +%% \verb/\implic/ation between formulae. +%% The point is that \TeX\ spaces them and breaks the lines differently: +%% \begin{center} +%% \verb/A\implies B/ $A\implies B$\quad{\em versus\/}\quad +%% \verb/A\implic B/ $A\implic B$ +%% \end{center} +%% There are forward and reverse, single and Double versions. +%% +\mathchardef\implies="3221 \mathchardef\impliedby="3220 \mathchardef\Implies=% +"3229 \mathchardef\Impliedby="3228 \mathchardef\implic="2221 \mathchardef +\implicby="2220 \mathchardef\Implic="2229 \mathchardef\Implicby="2228 \let +\imp\to%% +%% Handle the spacing after a variable (and optionally its type) +%% bound by a quantifier symbol. For example +%% \begin{quote} +%% \verb/\All x:X. \phi(x)/\quad prints as\quad $\All x:X.\phi(x)$\quad +%% instead of\quad $\forall x:X.\phi(x)$ +%% \end{quote} +\def\Quantifier#1#2.{\pb@G{#1}#2::.}\def\pb@G#1#2:#3:#4.{{{#1}{#2}\def\next{#% +3}\ifx\next\empty{.}\mkern1mu \else\mkern1mu{\colon}\mkern1mu{#3}\mkern.5mu{.% +}\mkern3mu \fi}}% +%% We provide some commonly used forms; \verb/\iota/ ($\iota$) is Russell's +%% description operator and should really be inverted. +\def\All{\Quantifier\forall}\def\Some{\Quantifier\exists}\def\Function{% +\Quantifier\lambda}\def\Product{\Quantifier\Pi}\def\Sum{\Quantifier\Sigma}% +\def\TheOne{\Quantifier\iota}\def\Least{\Quantifier\mu}\def\Greatest{% +\Quantifier\nu}%% +%% There are several notations for substitution. +%% After writing $a[x:=b]$ throughout my book I~thought I~might change to +%% $[b/x]^*a$. +%% This macro reads the source in the first form and prints in the second. +%% If you use it you can, like me, defer the decision about +%% which notation to use until the final stages, doing +%% \begin{quote} +%% \verb/\renewcommand{\Subst}{\plainsubstitution}/ +%% \end{quote} +%% if you finally decide on making substitution act on the right. +%% This is already an improvement on the literal text, because it +%% automatically enlarges the brackets according to the text inside. +%% \verb/\Subst/ itself is (following my book) +%% defined in terms of the action of a context morphism (\verb/\CtxtMor/) +%% on a term. Again you can do +%% \begin{quote} +%% \verb/\renewcommand{\CtxtMor}{\plaincontextmorphism}/ +%% \end{quote} +%% for something simpler. +%% This macro interprets its argument as a comma-separated list +%% of items in the form $x:=b$, which it switches to $b/x$. +\def\swappingsubstitution#1[#2]{{\CtxtMor[#2]^*{#1}}}\def +\swappingcontextmorphism[#1]{{\let\pb@J\empty\left[\pb@H#1,[],\/\right]}}\def +\pb@H#1,{\def\next{#1}\ifx\next\pb@K\else\pb@J\let\pb@J,\pb@I#1:=:=,% +\expandafter\pb@H\fi}\def\pb@I#1:=#2:=#3,{{\def\next{#2}\ifx\next\empty\else{% +#2}/\fi{#1} }}\def\pb@K{[]}\def\Subst{\swappingsubstitution}\def\CtxtMor{% +\swappingcontextmorphism}%% +%% The simple versions. +\def\plainsubstitution#1#2{{#1}{\left[{#2}\right]}}\def\plaincontextmorphism#% +1{{\left[#1\right]}}\newbox\pb@L\newdimen\pb@T\newdimen\pb@U\newdimen\pb@M +\newdimen\pb@N\newdimen\pb@O\newdimen\pb@P\newdimen\pb@Q\newdimen\pb@R +\newdimen\pb@S\def\pb@V#1#2{\relax\ifdim#1<#2\relax#1=#2\relax\fi}\count@ +\year\multiply\count@12 \advance\count@\month\ifnum\count@> 23966 \message{% +because this one has expired and will no longer work!}\endinput\fi%% +\def\proofbox{\relax\ifmmode\let\next\pb@a\else\let\next\pb@b\ifhmode\ifinner +\let\next\pb@a\fi\fi\fi\next\global\prooflinetotal\@ne\boxmaxdepth\maxdimen +\def\[{\pb@w\pb@f\pb@W}\def\({\pb@w\pb@f\pb@X}\def\proofbox{\[}\let\lbl\pb@y +\def\"##1"{\pb@y{##1}}\def\:{\pb@v\proofboxproposition\displaystyle}\def\={% +\pb@v\proofboxreason}\def\-{\pb@v\proofboxuse}\def\\{\pb@w\pb@u}\let\+\pb@c +\let\*\pb@c\let\]\pb@c\pb@p\pb@s}\def\endproofbox{\pb@q\pb@IA\box\pb@L\egroup +}\def\pb@W{\let\+\pb@d\let\*\pb@d\def\){\pb@e\[\)}\let\]\pb@Y\proofcolumns\z@ +}\def\pb@X{\proofcolumns\@ne\def\+{\pb@j\pb@l}\def\*{\pb@j\pb@m}\def\]{\pb@e +\(\]}\let\)\pb@Y}\def\pb@Y{\pb@o\pb@u}\def\pb@a{\hbox\bgroup}\def\pb@b{$$% +\kern-\displayindent\hbox to\hsize\bgroup\proofboxfullwidth\hsize\aftergroup$% +\aftergroup$}\def\pb@c{\errmessage{Box proofs: \string\+, \string\*, \string +\) and \string\] may not be used at the top level}}\def\pb@d{\errmessage{Box +proofs: enclose \string\+ and \string\* in \string\(\string\), not \string\[% +\string\]}}\def\pb@e#1#2{\errmessage{Box proofs: \string#1 closed by \string#% +2}\pb@Y}\def\pb@f#1{\setbox\pb@L\hbox\bgroup#1\let\pb@g\pb@n\let +\enclosingproofline\@currentlabel\edef\pb@h{\the\prooflinetotal}\let\pb@i +\pb@h\pb@O\z@\pb@M\z@\pb@N-\maxdimen\pb@P\z@\pb@p\pb@t}\def\pb@j#1{\pb@q\pb@k +\let\pb@g#1\advance\proofcolumns\@ne\global\prooflinetotal\pb@h +\leftmostproofboxfalse\pb@p\pb@t}\def\pb@k{\pb@g\pb@V\pb@M{\wd\pb@L}\advance +\pb@O\wd\pb@L\ifnum\pb@i<\prooflinetotal\edef\pb@i{\the\prooflinetotal}\fi +\ifdim\pb@N<\dp\pb@L\pb@N\dp\pb@L\pb@P\pb@Q\fi\setbox\z@\hbox{% +\proofboxtopside}\wd\z@\z@\box\z@\setbox\z@\hbox{\proofboxbottomside}\wd\z@ +\z@\box\z@\kern\pb@R\box\pb@L\kern\pb@S}\def\pb@l{\vtop{\proofboxorseparator}% +\penalty\thr@@}\def\pb@m{\vtop{\proofboxrightside}\kern\proofboxseparation +\vtop{\proofboxleftside}\penalty\tw@}\def\pb@n{\pb@T\pb@R\setbox\z@\vtop{% +\proofboxleftside}\dimen@\wd\z@\advance\pb@T\dimen@\advance\pb@T +\proofboxseparation\kern-\pb@T\kern\proofboxseparation\box\z@\penalty\@ne}% +\def\pb@o{\pb@q\pb@k\setbox\z@\vtop{\proofboxrightside}\global\advance\pb@S +\wd\z@\box\z@\global\advance\pb@S\proofboxseparation\kern\proofboxseparation +\global\prooflinetotal\pb@i\global\pb@R\pb@T\global\pb@Q\pb@P\ifnum +\proofcolumns<\@ne\proofcolumns\@ne\fi\penalty\proofcolumns\kern-\pb@M\kern +\pb@M\kern-\pb@O\kern\pb@O\kern-\pb@S\penalty\@ne\egroup\pb@r}\def\pb@p#1{% +\setbox\pb@L\vtop\bgroup\baselineskip\proofboxbaselineskip\prooflineinbox\@ne +\pb@T\z@\pb@U\z@#1\pb@u}\def\pb@q{\pb@w\global\pb@R\pb@T\global\pb@S\pb@U +\egroup}\def\pb@r{\pb@V\pb@T\pb@R\pb@V\pb@U\pb@S\box\pb@L\prevdepth\pb@Q}\def +\pb@s{}\def\pb@t{}\def\pb@u{\edef\@currentlabel{\theproofline}\let\label@name +\@currentlabel\setbox\proofboxproposition\box\voidb@x\setbox\proofboxreason +\box\voidb@x\setbox\proofboxuse\box\voidb@x\setbox\proofboxvariables\hbox +\bgroup\let\pb@z\pb@AA\let\pb@w\pb@x$}\def\pb@v#1{$\egroup\setbox#1\hbox +\bgroup\let\pb@z\pb@AA$}\def\pb@w{$\egroup\global\advance\prooflinetotal\@ne +\advance\prooflineinbox\@ne\setbox\pb@L\hbox{\setbox\z@\hbox{% +\proofboxmakeleftcolumn}\global\pb@R\wd\z@\kern-\pb@R\box\z@\hbox{% +\proofboxmakemiddlecolumn}\setbox\z@\hbox{\proofboxmakerightcolumn}\global +\pb@S\wd\z@\box\z@\kern-\pb@S\penalty\tw@}\global\pb@Q\dp\pb@L\pb@r}\def\pb@x +{$\egroup}\def\pb@y#1{\aftergroup\pb@z\expandafter\aftergroup\csname r@#1% +\endcsname}\def\pb@z#1{\edef#1{{\@currentlabel}{}}\expandafter\pb@@A\string#1% +\\}\expandafter\def\expandafter\pb@@A\string\r@#1\\{\def\label@name{#1}}\def +\pb@AA#1{\aftergroup\pb@z\aftergroup#1}\expandafter\def\csname r@-\endcsname{% +{\previous@label}{}}\dimendef\pb@BA=\@ne\dimendef\pb@CA=\tw@\dimendef\pb@DA=% +\thr@@\dimendef\pb@EA=4 \dimendef\pb@FA=5 \dimendef\pb@GA=6 \chardef\pb@HA=9 +\def\pb@IA{\pb@GA\proofboxfullwidth\pb@T\proofboxleftmargin\pb@V\pb@T\pb@R +\advance\pb@GA-\pb@T\pb@U\proofboxrightmargin\pb@V\pb@U\pb@S\advance\pb@GA-% +\pb@U\pb@V\pb@GA{\wd\pb@L}\pb@JA}\def\pb@JA{\setbox\pb@L\vtop{\unvbox\pb@L +\loop\skip@\lastskip\unskip\setbox\pb@HA\lastbox\ifhbox\pb@HA\pb@KA\repeat +\unvbox\pb@L\unskip}}\def\pb@KA{\pb@DA\dp\pb@HA\pb@EA\ht\pb@HA\pb@CA\wd\pb@HA +\setbox\pb@HA\hbox{\unhbox\pb@HA\count@\lastpenalty\unpenalty\unkern\ifodd +\count@\pb@LA\else\setbox\thr@@\lastbox\setbox\tw@\lastbox\setbox\@ne\lastbox +\unkern\hbox to\pb@T{\unhbox\@ne}\hbox to\pb@GA{\unhbox\tw@}\hbox to\pb@U{% +\unhbox\thr@@}\fi}\dp\pb@HA\pb@DA\ht\pb@HA\pb@EA\setbox\pb@L\vtop{\box\pb@HA +\nointerlineskip\vskip\skip@\unvbox\pb@L}}\def\pb@LA{\pb@O\lastkern\unkern +\unkern\pb@M\lastkern\unkern\unkern\proofcolumns\lastpenalty\unpenalty\pb@FA +\pb@T\ifnum\@ne=\proofcolumns\let\pb@MA\pb@NA\else\advance\pb@GA-\pb@CA\pb@BA +\pb@GA\advance\pb@GA\pb@O\ifdim\pb@GA<\proofcolumns\pb@M\divide\pb@BA +\proofcolumns\let\pb@MA\pb@PA\else\divide\pb@GA\proofcolumns\let\pb@MA\pb@OA +\fi\fi\dimen@\lastkern\unkern\setbox\@ne\lastbox\pb@RA\setbox\pb@HA\hbox{\box +\@ne\kern\dimen@}\advance\pb@U-\wd\pb@HA\unkern\loop\setbox\pb@L\lastbox\pb@T +\lastkern\unkern\setbox\tw@\lastbox\setbox\thr@@\lastbox\count@\lastpenalty +\unpenalty\pb@MA\pb@JA\setbox\@ne\vbox{\offinterlineskip\pb@QA\thr@@\vfil +\pb@QA\tw@}\pb@RA\pb@TA{\box\@ne\box\pb@L}\ifnum\count@>\@ne\pb@SA\pb@U +\lastkern\unkern\repeat\unhbox\pb@HA}\def\pb@NA{\pb@T\pb@FA\setbox\@ne +\lastbox\advance\pb@T-\wd\@ne\dimen@\lastkern\unkern\unkern\kern\dimen@\pb@RA +\box\@ne\advance\pb@T-\dimen@}\def\pb@OA{\ifnum\@ne=\count@\pb@NA\fi}\def +\pb@PA{\pb@GA\wd\pb@L\advance\pb@GA\pb@BA\pb@OA}\def\pb@QA#1{\setbox#1\hbox to% +\wd\pb@L{\unhbox#1}\wd#1\z@\box#1\relax}\def\pb@RA{\setbox\@ne\vbox to\pb@EA{% +\offinterlineskip\vskip-\proofboxseparation\unvbox\@ne\vskip-% +\proofboxseparation\setbox\z@\null\ht\z@-\pb@DA\dp\z@\pb@DA\box\z@}}\def +\pb@SA{\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne}\ifodd\count@\else\dimen@ +\lastkern\unkern\setbox\@ne\lastbox\pb@RA\pb@TA{\box\@ne\kern\dimen@}\fi}\def +\pb@TA#1{\setbox\pb@HA\hbox{#1\unhbox\pb@HA}}\let\+\pb@A\proofboxrestoreat +\endinput\def\x{}%% +%% \end{document} +% \fi diff --git a/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex b/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex new file mode 100644 index 00000000000..a4ed2959b4e --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/prooftree-doc.tex @@ -0,0 +1,198 @@ +\documentstyle{article} +\input prooftree +\title{Build proof tree for Natural Deduction, Sequent Calculus, etc.} +\author{Paul Taylor\\ +Department of Computing,\\ +Imperial College,\\ +London SW7 2BZ\\ ++44 71 589 5111 {\em ext\/} 5057\\ +{\tt<pt@doc.ic.ac.uk>}} +\def\X{x} +\let\imp\Rightarrow +\def\T{{\rm t\!t}}\def\F{{\rm f\!f}} +\def\P#1{p#1}% +\def\Q#1{q#1}% +\def\E#1#2{\exists#2.\X_{#2}={#1}} +\def\A#1#2{\exists#1.\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)} +\def\B#1#2{\forall#1.\left(\left(\E{#1}{#2}\right)\imp\P{#1}\right)} +\def\C#1#2{\exists#1.\P{#1}\land\left(\left(\left(\E{#1}{#2}\right)\land\Q{#1}\right)\right)} +\overfullrule0pt +\begin{document} +\maketitle +Using my Proof Tree macros, you can produce +{\small +$$\begin{prooftree} +\[ \[ [(\A y n)\land(\B w n)]_\alpha + \andelim1 + \A y n + \] + \kern-26em + \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha + \andelim2 \shiftright60pt + \B w n + \] + \allelim + (\E y n)\imp\P y + \] + \[ + [(\E y n)\land\Q y]_\beta + \andelim1 + \E y n + \] + \impelim \shiftright50pt + \P y + \] + \kern-25pt + [(\E y n)\land\Q y]_\beta + \andintro + \P y\land((\E y n)\land\Q y) + \] + \existsintro + \C z n + \] + \existselim\beta + \C z n +\] +\impintro\alpha +(\A yn)\land(\B w n)\imp(\C z n) +\end{prooftree}$$} +using the \TeX\ or \LaTeX\ code +\begin{verbatim} +\input prooftree +$$ +\begin{prooftree} +\[ \[ [(\A y n)\land(\B w n)]_\alpha + \andelim1 + \A y n + \] + \kern-26em + \[ \[ \[ \[ \[ [(\A y n)\land(\B w n)]_\alpha + \andelim2 \shiftright60pt + \B w n + \] + \allelim + (\E y n)\imp\P y + \] + \[ + [(\E y n)\land\Q y]_\beta + \andelim1 + \E y n + \] + \impelim \shiftright50pt + \P y + \] + \kern-25pt + [(\E y n)\land\Q y]_\beta + \andintro + \P y\land((\E y n)\land\Q y) + \] + \existsintro + \C z n + \] + \existselim\beta + \C z n +\] +\impintro\alpha +(\A yn)\land(\B w n)\imp(\C z n) +\end{prooftree}$$ +\end{verbatim} + + + +In fact the commands \verb/\allintro/, {\it etc.,} are not primitive; +the basic form is +\begin{verbatim} +\[ + A\quad + B +\justifies + A \land B +\thickness=0.08em +\shiftright 2em +\using + {\land}{\cal I} +\] +\end{verbatim} +which gives +$$\begin{prooftree} + A\quad + B +\justifies + A \land B +\thickness=0.08em +\shiftright 2em +\using + {\land}{\cal I} +\end{prooftree}$$ +The hypotheses may themselves be proof trees (enclosed in +\verb/\[/\ldots\verb/\]/) +and the purpose of the macros is to adjust +the length of the horizontal ``deduction'' line. When the hypotheses +are proof trees, suitable space is put between them, but of course +this must be supplied by hand for simple formulae. The \verb/\thickness/ +and \verb/\shiftright/ commands are, of course, optional; they apply to +the horizontal line and to the positioning of the conclusion relative to +it. For a double line, use \verb/\Justifies/ instead of \verb/\justifies/. + +Notice the overloading of the \verb/\[/\ldots\verb/\]/; the outermost proof +tree must be enclosed with \verb/\begin{prooftree}/ and \verb/\end{prooftree}/ +or \verb/\prooftree/ and \verb/\endprooftree/. + +To get a vertical string of dots instead of the proof rule, do +\begin{verbatim} +\[ + [A] +\using + \pi +\proofdotseparation=1.2ex +\proofdotnumber=4 +\leadsto + B +\] +\end{verbatim} +to get +\prooftree + [A] +\using + \pi +\proofdotseparation=1.2ex +\proofdotnumber=4 +\leadsto + B +\endprooftree + +All of of the keywords except \verb/\prooftree/ and \verb/\endprooftree/ +are optional and may appear in any order. They may also be combined in +\verb/\newcommand/s, for example +\begin{verbatim} +\newcommand\Cut{\using\sf cut\thickness.08em\justifies} +\end{verbatim} +with the abbreviation +\begin{verbatim} +\[ A \vdash B \qquad + B \vdash C + \Cut + A \vdash C +\] +\end{verbatim} + +\verb/\thickness/ specifies the breadth of the rule in any units, although +font-relative units such as ex or em are preferable. +It may optionally be followed by =. +\verb/\proofrulebreadth=.08em/ or \verb/\setlength\proofrulebreadth{.08em}/ +may also be used either in place of \verb/\thickness/ or globally; the +default is 0.04em. \verb/\proofdotseparation/ and \verb/\proofdotnumber/ +control the size of the string of dots. + +If proof trees and formulae are mixed, some explicit spacing is needed, +but don't put anything to the left of the left-most (or the right of +the right-most) hypothesis, or put it in braces, because this will cause +the indentation to be lost. + +By default the conclusion is centered wrt the left-most and right-most +immediate hypotheses (not their proofs); \verb/\shiftright/ or +\verb/\shiftleft/ moves it relative to this position. +(Not sure about this specification or how +it should affect spreading of proof tree.) + +\end{document}
\ No newline at end of file diff --git a/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex b/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex new file mode 100644 index 00000000000..abb7d448642 --- /dev/null +++ b/Master/texmf-dist/source/latex/proofs/taylor/prooftree.tex @@ -0,0 +1,347 @@ +\message{<Paul Taylor's Proof Trees, 2 August 1996>} +%% Build proof tree for Natural Deduction, Sequent Calculus, etc. +%% WITH SHORTENING OF PROOF RULES! +%% Paul Taylor, begun 10 Oct 1989 +%% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! *** +%% +%% 2 Aug 1996: fixed \mscount and \proofdotnumber +%% +%% \prooftree +%% hyp1 produces: +%% hyp2 +%% hyp3 hyp1 hyp2 hyp3 +%% \justifies -------------------- rulename +%% concl concl +%% \thickness=0.08em +%% \shiftright 2em +%% \using +%% rulename +%% \endprooftree +%% +%% where the hypotheses may be similar structures or just formulae. +%% +%% To get a vertical string of dots instead of the proof rule, do +%% +%% \prooftree which produces: +%% [hyp] +%% \using [hyp] +%% name . +%% \proofdotseparation=1.2ex .name +%% \proofdotnumber=4 . +%% \leadsto . +%% concl concl +%% \endprooftree +%% +%% Within a prooftree, \[ and \] may be used instead of \prooftree and +%% \endprooftree; this is not permitted at the outer level because it +%% conflicts with LaTeX. Also, +%% \Justifies +%% produces a double line. In LaTeX you can use \begin{prooftree} and +%% \end{prootree} at the outer level (however this will not work for the inner +%% levels, but in any case why would you want to be so verbose?). +%% +%% All of of the keywords except \prooftree and \endprooftree are optional +%% and may appear in any order. They may also be combined in \newcommand's +%% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation +%% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and +%% some standard abbreviations will be found at the end of this file. +%% +%% \thickness specifies the breadth of the rule in any units, although +%% font-relative units such as "ex" or "em" are preferable. +%% It may optionally be followed by "=". +%% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be +%% used either in place of \thickness or globally; the default is 0.04em. +%% \proofdotseparation and \proofdotnumber control the size of the +%% string of dots +%% +%% If proof trees and formulae are mixed, some explicit spacing is needed, +%% but don't put anything to the left of the left-most (or the right of +%% the right-most) hypothesis, or put it in braces, because this will cause +%% the indentation to be lost. +%% +%% By default the conclusion is centered wrt the left-most and right-most +%% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves +%% it relative to this position. (Not sure about this specification or how +%% it should affect spreading of proof tree.) +% +% global assignments to dimensions seem to have the effect of stretching +% diagrams horizontally. +% +%%========================================================================== + +\def\introrule{{\cal I}}\def\elimrule{{\cal E}}%% +\def\andintro{\using{\land}\introrule\justifies}%% +\def\impelim{\using{\Rightarrow}\elimrule\justifies}%% +\def\allintro{\using{\forall}\introrule\justifies}%% +\def\allelim{\using{\forall}\elimrule\justifies}%% +\def\falseelim{\using{\bot}\elimrule\justifies}%% +\def\existsintro{\using{\exists}\introrule\justifies}%% + +%% #1 is meant to be 1 or 2 for the first or second formula +\def\andelim#1{\using{\land}#1\elimrule\justifies}%% +\def\orintro#1{\using{\lor}#1\introrule\justifies}%% + +%% #1 is meant to be a label corresponding to the discharged hypothesis/es +\def\impintro#1{\using{\Rightarrow}\introrule_{#1}\justifies}%% +\def\orelim#1{\using{\lor}\elimrule_{#1}\justifies}%% +\def\existselim#1{\using{\exists}\elimrule_{#1}\justifies} + +%%========================================================================== + +\newdimen\proofrulebreadth \proofrulebreadth=.05em +\newdimen\proofdotseparation \proofdotseparation=1.25ex +\newdimen\proofrulebaseline \proofrulebaseline=2ex +\newcount\proofdotnumber \proofdotnumber=3 +\let\then\relax +\def\hfi{\hskip0pt plus.0001fil} +\mathchardef\squigto="3A3B +% +% flag where we are +\newif\ifinsideprooftree\insideprooftreefalse +\newif\ifonleftofproofrule\onleftofproofrulefalse +\newif\ifproofdots\proofdotsfalse +\newif\ifdoubleproof\doubleprooffalse +\let\wereinproofbit\relax +% +% dimensions and boxes of bits +\newdimen\shortenproofleft +\newdimen\shortenproofright +\newdimen\proofbelowshift +\newbox\proofabove +\newbox\proofbelow +\newbox\proofrulename +% +% miscellaneous commands for setting values +\def\shiftproofbelow{\let\next\relax\afterassignment\setshiftproofbelow\dimen0 } +\def\shiftproofbelowneg{\def\next{\multiply\dimen0 by-1 }% +\afterassignment\setshiftproofbelow\dimen0 } +\def\setshiftproofbelow{\next\proofbelowshift=\dimen0 } +\def\setproofrulebreadth{\proofrulebreadth} + +%============================================================================= +\def\prooftree{% NESTED ZERO (\ifonleftofproofrule) +% +% first find out whether we're at the left-hand end of a proof rule +\ifnum \lastpenalty=1 +\then \unpenalty +\else \onleftofproofrulefalse +\fi +% +% some space on left (except if we're on left, and no infinity for outermost) +\ifonleftofproofrule +\else \ifinsideprooftree + \then \hskip.5em plus1fil + \fi +\fi +% +% begin our proof tree environment +\bgroup% NESTED ONE (\proofbelow, \proofrulename, \proofabove, +% \shortenproofleft, \shortenproofright, \proofrulebreadth) +\setbox\proofbelow=\hbox{}\setbox\proofrulename=\hbox{}% +\let\justifies\proofover\let\leadsto\proofoverdots\let\Justifies\proofoverdbl +\let\using\proofusing\let\[\prooftree +\ifinsideprooftree\let\]\endprooftree\fi +\proofdotsfalse\doubleprooffalse +\let\thickness\setproofrulebreadth +\let\shiftright\shiftproofbelow \let\shift\shiftproofbelow +\let\shiftleft\shiftproofbelowneg +\let\ifwasinsideprooftree\ifinsideprooftree +\insideprooftreetrue +% +% now begin to set the top of the rule (definitions local to it) +\setbox\proofabove=\hbox\bgroup$\displaystyle % NESTED TWO +\let\wereinproofbit\prooftree +% +% these local variables will be copied out: +\shortenproofleft=0pt \shortenproofright=0pt \proofbelowshift=0pt +% +% flags to enable inner proof tree to detect if on left: +\onleftofproofruletrue\penalty1 +} + +%============================================================================= +% end whatever box and copy crucial values out of it +\def\eproofbit{% NESTED TWO +% +% various hacks applicable to hypothesis list +\ifx \wereinproofbit\prooftree +\then \ifcase \lastpenalty + \then \shortenproofright=0pt % 0: some other object, no indentation + \or \unpenalty\hfil % 1: empty hypotheses, just glue + \or \unpenalty\unskip % 2: just had a tree, remove glue + \else \shortenproofright=0pt % eh? + \fi +\fi +% +% pass out crucial values from scope +\global\dimen0=\shortenproofleft +\global\dimen1=\shortenproofright +\global\dimen2=\proofrulebreadth +\global\dimen3=\proofbelowshift +\global\dimen4=\proofdotseparation +\global\count255=\proofdotnumber +% +% end the box +$\egroup % NESTED ONE +% +% restore the values +\shortenproofleft=\dimen0 +\shortenproofright=\dimen1 +\proofrulebreadth=\dimen2 +\proofbelowshift=\dimen3 +\proofdotseparation=\dimen4 +\proofdotnumber=\count255 +} + +%============================================================================= +\def\proofover{% NESTED TWO +\eproofbit % NESTED ONE +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofover +$\displaystyle +}% +% +%============================================================================= +\def\proofoverdbl{% NESTED TWO +\eproofbit % NESTED ONE +\doubleprooftrue +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofoverdbl +$\displaystyle +}% +% +%============================================================================= +\def\proofoverdots{% NESTED TWO +\eproofbit % NESTED ONE +\proofdotstrue +\setbox\proofbelow=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofoverdots +$\displaystyle +}% +% +%============================================================================= +\def\proofusing{% NESTED TWO +\eproofbit % NESTED ONE +\setbox\proofrulename=\hbox\bgroup % NESTED TWO +\let\wereinproofbit\proofusing +\kern0.3em$ +} + +%============================================================================= +\def\endprooftree{% NESTED TWO +\eproofbit % NESTED ONE +% \dimen0 = length of proof rule +% \dimen1 = indentation of conclusion wrt rule +% \dimen2 = new \shortenproofleft, ie indentation of conclusion +% \dimen3 = new \shortenproofright, ie +% space on right of conclusion to end of tree +% \dimen4 = space on right of conclusion below rule + \dimen5 =0pt% spread of hypotheses +% \dimen6, \dimen7 = height & depth of rule +% +% length of rule needed by proof above +\dimen0=\wd\proofabove \advance\dimen0-\shortenproofleft +\advance\dimen0-\shortenproofright +% +% amount of spare space below +\dimen1=.5\dimen0 \advance\dimen1-.5\wd\proofbelow +\dimen4=\dimen1 +\advance\dimen1\proofbelowshift \advance\dimen4-\proofbelowshift +% +% conclusion sticks out to left of immediate hypotheses +\ifdim \dimen1<0pt +\then \advance\shortenproofleft\dimen1 + \advance\dimen0-\dimen1 + \dimen1=0pt +% now it sticks out to left of tree! + \ifdim \shortenproofleft<0pt + \then \setbox\proofabove=\hbox{% + \kern-\shortenproofleft\unhbox\proofabove}% + \shortenproofleft=0pt + \fi +\fi +% +% and to the right +\ifdim \dimen4<0pt +\then \advance\shortenproofright\dimen4 + \advance\dimen0-\dimen4 + \dimen4=0pt +\fi +% +% make sure enough space for label +\ifdim \shortenproofright<\wd\proofrulename +\then \shortenproofright=\wd\proofrulename +\fi +% +% calculate new indentations +\dimen2=\shortenproofleft \advance\dimen2 by\dimen1 +\dimen3=\shortenproofright\advance\dimen3 by\dimen4 +% +% make the rule or dots, with name attached +\ifproofdots +\then + \dimen6=\shortenproofleft \advance\dimen6 .5\dimen0 + \setbox1=\vbox to\proofdotseparation{\vss\hbox{$\cdot$}\vss}% + \setbox0=\hbox{% + \advance\dimen6-.5\wd1 + \kern\dimen6 + $\vcenter to\proofdotnumber\proofdotseparation + {\leaders\box1\vfill}$% + \unhbox\proofrulename}% +\else \dimen6=\fontdimen22\the\textfont2 % height of maths axis + \dimen7=\dimen6 + \advance\dimen6by.5\proofrulebreadth + \advance\dimen7by-.5\proofrulebreadth + \setbox0=\hbox{% + \kern\shortenproofleft + \ifdoubleproof + \then \hbox to\dimen0{% + $\mathsurround0pt\mathord=\mkern-6mu% + \cleaders\hbox{$\mkern-2mu=\mkern-2mu$}\hfill + \mkern-6mu\mathord=$}% + \else \vrule height\dimen6 depth-\dimen7 width\dimen0 + \fi + \unhbox\proofrulename}% + \ht0=\dimen6 \dp0=-\dimen7 +\fi +% +% set up to centre outermost tree only +\let\doll\relax +\ifwasinsideprooftree +\then \let\VBOX\vbox +\else \ifmmode\else$\let\doll=$\fi + \let\VBOX\vcenter +\fi +% this \vbox or \vcenter is the actual output: +\VBOX {\baselineskip\proofrulebaseline \lineskip.2ex + \expandafter\lineskiplimit\ifproofdots0ex\else-0.6ex\fi + \hbox spread\dimen5 {\hfi\unhbox\proofabove\hfi}% + \hbox{\box0}% + \hbox {\kern\dimen2 \box\proofbelow}}\doll% +% +% pass new indentations out of scope +\global\dimen2=\dimen2 +\global\dimen3=\dimen3 +\egroup % NESTED ZERO +\ifonleftofproofrule +\then \shortenproofleft=\dimen2 +\fi +\shortenproofright=\dimen3 +% +% some space on right and flag we've just made a tree +\onleftofproofrulefalse +\ifinsideprooftree +\then \hskip.5em plus 1fil \penalty2 +\fi +} + +%========================================================================== +% IDEAS +% 1. Specification of \shiftright and how to spread trees. +% 2. Spacing command \m which causes 1em+1fil spacing, over-riding +% exisiting space on sides of trees and not affecting the +% detection of being on the left or right. +% 3. Hack using \@currenvir to detect LaTeX environment; have to +% use \aftergroup to pass \shortenproofleft/right out. +% 4. (Pie in the sky) detect how much trees can be "tucked in" +% 5. Discharged hypotheses (diagonal lines). |