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