doc-src/proof209.sty
author oheimb
Sat Feb 15 16:10:00 1997 +0100 (1997-02-15)
changeset 2628 1fe7c9f599c2
parent 1210 230b9b4b783e
permissions -rw-r--r--
description of del(eq)congs, safe and unsafe solver
     1 %       proof.sty       (Proof Figure Macros)
     2 %
     3 %       version 2.0
     4 %       June 24, 1991
     5 %       Copyright (C) 1990,1991 Makoto Tatsuta (tatsuta@riec.tohoku.ac.jp)
     6 % 
     7 % This program is free software; you can redistribute it or modify
     8 % it under the terms of the GNU General Public License as published by
     9 % the Free Software Foundation; either versions 1, or (at your option)
    10 % any later version.
    11 % 
    12 % This program is distributed in the hope that it will be useful
    13 % but WITHOUT ANY WARRANTY; without even the implied warranty of
    14 % MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    15 % GNU General Public License for more details.
    16 %
    17 %       Usage:
    18 %               In \documentstyle, specify an optional style `proof', say,
    19 %                       \documentstyle[proof]{article}.
    20 %
    21 %       The following macros are available:
    22 %
    23 %       In all the following macros, all the arguments such as
    24 %       <Lowers> and <Uppers> are processed in math mode.
    25 %
    26 %       \infer<Lower><Uppers>
    27 %               draws an inference.
    28 %
    29 %               Use & in <Uppers> to delimit upper formulae.
    30 %               <Uppers> consists more than 0 formulae.
    31 %
    32 %               \infer returns \hbox{ ... } or \vbox{ ... } and
    33 %               sets \@LeftOffset and \@RightOffset globally.
    34 %
    35 %       \infer[<Label>]<Lower><Uppers>
    36 %               draws an inference labeled with <Label>.
    37 %
    38 %       \infer*<Lower><Uppers>
    39 %               draws a many step deduction.
    40 %
    41 %       \infer*[<Label>]<Lower><Uppers>
    42 %               draws a many step deduction labeled with <Label>.
    43 %
    44 %       \infer=<Lower><Uppers>
    45 %               draws a double-ruled deduction.
    46 %
    47 %       \infer=[<Label>]<Lower><Uppers>
    48 %               draws a double-ruled deduction labeled with <Label>.
    49 %
    50 %       \deduce<Lower><Uppers>
    51 %               draws an inference without a rule.
    52 %
    53 %       \deduce[<Proof>]<Lower><Uppers>
    54 %               draws a many step deduction with a proof name.
    55 %
    56 %       Example:
    57 %               If you want to write
    58 %                           B C
    59 %                          -----
    60 %                      A     D
    61 %                     ----------
    62 %                         E
    63 %       use
    64 %               \infer{E}{
    65 %                       A
    66 %                       &
    67 %                       \infer{D}{B & C}
    68 %               }
    69 %
    70 
    71 %       Style Parameters
    72 
    73 \newdimen\inferLineSkip         \inferLineSkip=2pt
    74 \newdimen\inferLabelSkip        \inferLabelSkip=5pt
    75 \def\inferTabSkip{\quad}
    76 
    77 %       Variables
    78 
    79 \newdimen\@LeftOffset   % global
    80 \newdimen\@RightOffset  % global
    81 \newdimen\@SavedLeftOffset      % safe from users
    82 
    83 \newdimen\UpperWidth
    84 \newdimen\LowerWidth
    85 \newdimen\LowerHeight
    86 \newdimen\UpperLeftOffset
    87 \newdimen\UpperRightOffset
    88 \newdimen\UpperCenter
    89 \newdimen\LowerCenter
    90 \newdimen\UpperAdjust
    91 \newdimen\RuleAdjust
    92 \newdimen\LowerAdjust
    93 \newdimen\RuleWidth
    94 \newdimen\HLabelAdjust
    95 \newdimen\VLabelAdjust
    96 \newdimen\WidthAdjust
    97 
    98 \newbox\@UpperPart
    99 \newbox\@LowerPart
   100 \newbox\@LabelPart
   101 \newbox\ResultBox
   102 
   103 %       Flags
   104 
   105 \newif\if@inferRule     % whether \@infer draws a rule.
   106 \newif\if@DoubleRule    % whether \@infer draws doulbe rules.
   107 \newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
   108 \newif\if@MathSaved     % whether inner math mode where \infer or
   109                         % \deduce appears.
   110 
   111 %       Special Fonts
   112 
   113 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
   114     \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
   115 
   116 %       Math Save Macros
   117 %
   118 %       \@SaveMath is called in the very begining of toplevel macros
   119 %       which are \infer and \deduce.
   120 %       \@RestoreMath is called in the very last before toplevel macros end.
   121 %       Remark \infer and \deduce ends calling \@infer.
   122 
   123 \def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
   124         \relax $\relax \@MathSavedtrue \fi\fi }
   125 
   126 \def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
   127 
   128 %       Macros
   129 
   130 \def\@Ifnextchar#1#2#3{\let\@tempe=#1\def\@tempa{#2}\def\@tempb{#3}\futurelet
   131     \@tempc\@ifnch}
   132         % It can compare an = character, though the one in latex.tex cannot.
   133 
   134 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
   135         \ifx \@tempa \@tempb #2\else #3\fi }
   136 
   137 \def\infer{\@SaveMath \@Ifnextchar *{\@inferSteps}{\relax
   138         \@Ifnextchar ={\@inferDoubleRule}{\@inferOneStep}}}
   139 
   140 \def\@inferOneStep{\@inferRuletrue \@DoubleRulefalse
   141         \@Ifnextchar [{\@infer}{\@infer[\@empty]}}
   142 
   143 \def\@inferDoubleRule={\@inferRuletrue \@DoubleRuletrue
   144         \@Ifnextchar [{\@infer}{\@infer[\@empty]}}
   145 
   146 \def\@inferSteps*{\@Ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
   147 
   148 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
   149 
   150 \def\deduce{\@SaveMath \@Ifnextchar [{\@deduce{\@empty}}
   151         {\@inferRulefalse \@infer[\@empty]}}
   152 
   153 %       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
   154 
   155 \def\@deduce#1[#2]#3#4{\@inferRulefalse
   156         \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
   157 
   158 %       \@infer[<Label>]<Lower><Uppers>
   159 %               If \@inferRuletrue, it draws a rule and <Label> is right to
   160 %               a rule. In this case, if \@DoubleRuletrue, it draws
   161 %               double rules.
   162 %
   163 %               Otherwise, draws no rule and <Label> is right to <Lower>.
   164 
   165 \def\@infer[#1]#2#3{\relax
   166 % Get parameters
   167         \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
   168         \setbox\@LabelPart=\hbox{$#1$}\relax
   169         \setbox\@LowerPart=\hbox{$#2$}\relax
   170 %
   171         \global\@LeftOffset=0pt
   172         \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
   173                 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
   174                 \inferTabSkip
   175                 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
   176                 #3\cr}}\relax
   177 %                       Here is a little trick.
   178 %                       \@ReturnLeftOffsettrue(false) influences on \infer or
   179 %                       \deduce placed in ## locally
   180 %                       because of \@SaveMath and \@RestoreMath.
   181         \UpperLeftOffset=\@LeftOffset
   182         \UpperRightOffset=\@RightOffset
   183 % Calculate Adjustments
   184         \LowerWidth=\wd\@LowerPart
   185         \LowerHeight=\ht\@LowerPart
   186         \LowerCenter=0.5\LowerWidth
   187 %
   188         \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
   189         \advance\UpperWidth by -\UpperRightOffset
   190         \UpperCenter=\UpperLeftOffset
   191         \advance\UpperCenter by 0.5\UpperWidth
   192 %
   193         \ifdim \UpperWidth > \LowerWidth
   194                 % \UpperCenter > \LowerCenter
   195         \UpperAdjust=0pt
   196         \RuleAdjust=\UpperLeftOffset
   197         \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
   198         \RuleWidth=\UpperWidth
   199         \global\@LeftOffset=\LowerAdjust
   200 %
   201         \else   % \UpperWidth <= \LowerWidth
   202         \ifdim \UpperCenter > \LowerCenter
   203 %
   204         \UpperAdjust=0pt
   205         \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
   206         \LowerAdjust=\RuleAdjust
   207         \RuleWidth=\LowerWidth
   208         \global\@LeftOffset=\LowerAdjust
   209 %
   210         \else   % \UpperWidth <= \LowerWidth
   211                 % \UpperCenter <= \LowerCenter
   212 %
   213         \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
   214         \RuleAdjust=0pt
   215         \LowerAdjust=0pt
   216         \RuleWidth=\LowerWidth
   217         \global\@LeftOffset=0pt
   218 %
   219         \fi\fi
   220 % Make a box
   221         \if@inferRule
   222 %
   223         \setbox\ResultBox=\vbox{
   224                 \moveright \UpperAdjust \box\@UpperPart
   225                 \nointerlineskip \kern\inferLineSkip
   226                 \if@DoubleRule
   227                 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth
   228                         \kern 1pt\hrule width\RuleWidth}\relax
   229                 \else
   230                 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
   231                 \fi
   232                 \nointerlineskip \kern\inferLineSkip
   233                 \moveright \LowerAdjust \box\@LowerPart }\relax
   234 %
   235         \@ifEmpty{#1}{}{\relax
   236 %
   237         \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
   238         \advance\HLabelAdjust by -\RuleWidth
   239         \WidthAdjust=\HLabelAdjust
   240         \advance\WidthAdjust by -\inferLabelSkip
   241         \advance\WidthAdjust by -\wd\@LabelPart
   242         \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
   243 %
   244         \VLabelAdjust=\dp\@LabelPart
   245         \advance\VLabelAdjust by -\ht\@LabelPart
   246         \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
   247         \advance\VLabelAdjust by \inferLineSkip
   248 %
   249         \setbox\ResultBox=\hbox{\box\ResultBox
   250                 \kern -\HLabelAdjust \kern\inferLabelSkip
   251                 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
   252 %
   253         }\relax % end @ifEmpty
   254 %
   255         \else % \@inferRulefalse
   256 %
   257         \setbox\ResultBox=\vbox{
   258                 \moveright \UpperAdjust \box\@UpperPart
   259                 \nointerlineskip \kern\inferLineSkip
   260                 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
   261                         \@ifEmpty{#1}{}{\relax
   262                         \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
   263         \fi
   264 %
   265         \global\@RightOffset=\wd\ResultBox
   266         \global\advance\@RightOffset by -\@LeftOffset
   267         \global\advance\@RightOffset by -\LowerWidth
   268         \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
   269 %
   270         \box\ResultBox
   271         \@RestoreMath
   272 }