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