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
     1 %       proof.sty       (Proof Figure Macros)
     2 %
     3 %       version 1.0
     4 %       October 13, 1990
     5 %       Copyright (C) 1990 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 %       \deduce<Lower><Uppers>
    45 %               draws an inference without a rule.
    46 %
    47 %       \deduce[<Proof>]<Lower><Uppers>
    48 %               draws a many step deduction with a proof name.
    49 %
    50 %       Example:
    51 %               If you want to write
    52 %                           B C
    53 %                          -----
    54 %                      A     D
    55 %                     ----------
    56 %                         E
    57 %       use
    58 %               \infer{E}{
    59 %                       A
    60 %                       &
    61 %                       \infer{D}{B & C}
    62 %               }
    63 %
    64 
    65 %       Style Parameters
    66 
    67 \newdimen\inferLineSkip         \inferLineSkip=2pt
    68 \newdimen\inferLabelSkip        \inferLabelSkip=5pt
    69 \def\inferTabSkip{\quad}
    70 
    71 %       Variables
    72 
    73 \newdimen\@LeftOffset   % global
    74 \newdimen\@RightOffset  % global
    75 \newdimen\@SavedLeftOffset      % safe from users
    76 
    77 \newdimen\UpperWidth
    78 \newdimen\LowerWidth
    79 \newdimen\LowerHeight
    80 \newdimen\UpperLeftOffset
    81 \newdimen\UpperRightOffset
    82 \newdimen\UpperCenter
    83 \newdimen\LowerCenter
    84 \newdimen\UpperAdjust
    85 \newdimen\RuleAdjust
    86 \newdimen\LowerAdjust
    87 \newdimen\RuleWidth
    88 \newdimen\HLabelAdjust
    89 \newdimen\VLabelAdjust
    90 \newdimen\WidthAdjust
    91 
    92 \newbox\@UpperPart
    93 \newbox\@LowerPart
    94 \newbox\@LabelPart
    95 \newbox\ResultBox
    96 
    97 %       Flags
    98 
    99 \newif\if@inferRule     % whether \@infer draws a rule.
   100 \newif\if@ReturnLeftOffset      % whether \@infer returns \@LeftOffset.
   101 \newif\if@MathSaved     % whether inner math mode where \infer or
   102                         % \deduce appears.
   103 
   104 %       Special Fonts
   105 
   106 \def\DeduceSym{\vtop{\baselineskip4\p@ \lineskiplimit\z@
   107     \vbox{\hbox{.}\hbox{.}\hbox{.}}\hbox{.}}}
   108 
   109 %       Math Save Macros
   110 %
   111 %       \@SaveMath is called in the very begining of toplevel macros
   112 %       which are \infer and \deduce.
   113 %       \@RestoreMath is called in the very last before toplevel macros end.
   114 %       Remark \infer and \deduce ends calling \@infer.
   115 
   116 %\def\@SaveMath{\@MathSavedfalse \ifmmode \ifinner
   117 %        \relax $\relax \@MathSavedtrue \fi\fi }
   118 %
   119 %\def\@RestoreMath{\if@MathSaved \relax $\relax\fi }
   120 
   121 \def\@SaveMath{\relax}
   122 \def\@RestoreMath{\relax}
   123 
   124 
   125 %       Macros
   126 
   127 \def\@ifEmpty#1#2#3{\def\@tempa{\@empty}\def\@tempb{#1}\relax
   128         \ifx \@tempa \@tempb #2\else #3\fi }
   129 
   130 \def\infer{\@SaveMath \@ifnextchar *{\@inferSteps}{\@inferOneStep}}
   131 
   132 \def\@inferOneStep{\@inferRuletrue
   133         \@ifnextchar [{\@infer}{\@infer[\@empty]}}
   134 
   135 \def\@inferSteps*{\@ifnextchar [{\@@inferSteps}{\@@inferSteps[\@empty]}}
   136 
   137 \def\@@inferSteps[#1]{\@deduce{#1}[\DeduceSym]}
   138 
   139 \def\deduce{\@SaveMath \@ifnextchar [{\@deduce{\@empty}}
   140         {\@inferRulefalse \@infer[\@empty]}}
   141 
   142 %       \@deduce<Proof Label>[<Proof>]<Lower><Uppers>
   143 
   144 \def\@deduce#1[#2]#3#4{\@inferRulefalse
   145         \@infer[\@empty]{#3}{\@SaveMath \@infer[{#1}]{#2}{#4}}}
   146 
   147 %       \@infer[<Label>]<Lower><Uppers>
   148 %               If \@inferRuletrue, draws a rule and <Label> is right to
   149 %               a rule.
   150 %               Otherwise, draws no rule and <Label> is right to <Lower>.
   151 
   152 \def\@infer[#1]#2#3{\relax
   153 % Get parameters
   154         \if@ReturnLeftOffset \else \@SavedLeftOffset=\@LeftOffset \fi
   155         \setbox\@LabelPart=\hbox{$#1$}\relax
   156         \setbox\@LowerPart=\hbox{$#2$}\relax
   157 %
   158         \global\@LeftOffset=0pt
   159         \setbox\@UpperPart=\vbox{\tabskip=0pt \halign{\relax
   160                 \global\@RightOffset=0pt \@ReturnLeftOffsettrue $##$&&
   161                 \inferTabSkip
   162                 \global\@RightOffset=0pt \@ReturnLeftOffsetfalse $##$\cr
   163                 #3\cr}}\relax
   164 %                       Here is a little trick.
   165 %                       \@ReturnLeftOffsettrue(false) influences on \infer or
   166 %                       \deduce placed in ## locally
   167 %                       because of \@SaveMath and \@RestoreMath.
   168         \UpperLeftOffset=\@LeftOffset
   169         \UpperRightOffset=\@RightOffset
   170 % Calculate Adjustments
   171         \LowerWidth=\wd\@LowerPart
   172         \LowerHeight=\ht\@LowerPart
   173         \LowerCenter=0.5\LowerWidth
   174 %
   175         \UpperWidth=\wd\@UpperPart \advance\UpperWidth by -\UpperLeftOffset
   176         \advance\UpperWidth by -\UpperRightOffset
   177         \UpperCenter=\UpperLeftOffset
   178         \advance\UpperCenter by 0.5\UpperWidth
   179 %
   180         \ifdim \UpperWidth > \LowerWidth
   181                 % \UpperCenter > \LowerCenter
   182         \UpperAdjust=0pt
   183         \RuleAdjust=\UpperLeftOffset
   184         \LowerAdjust=\UpperCenter \advance\LowerAdjust by -\LowerCenter
   185         \RuleWidth=\UpperWidth
   186         \global\@LeftOffset=\LowerAdjust
   187 %
   188         \else   % \UpperWidth <= \LowerWidth
   189         \ifdim \UpperCenter > \LowerCenter
   190 %
   191         \UpperAdjust=0pt
   192         \RuleAdjust=\UpperCenter \advance\RuleAdjust by -\LowerCenter
   193         \LowerAdjust=\RuleAdjust
   194         \RuleWidth=\LowerWidth
   195         \global\@LeftOffset=\LowerAdjust
   196 %
   197         \else   % \UpperWidth <= \LowerWidth
   198                 % \UpperCenter <= \LowerCenter
   199 %
   200         \UpperAdjust=\LowerCenter \advance\UpperAdjust by -\UpperCenter
   201         \RuleAdjust=0pt
   202         \LowerAdjust=0pt
   203         \RuleWidth=\LowerWidth
   204         \global\@LeftOffset=0pt
   205 %
   206         \fi\fi
   207 % Make a box
   208         \if@inferRule
   209 %
   210         \setbox\ResultBox=\vbox{
   211                 \moveright \UpperAdjust \box\@UpperPart
   212                 \nointerlineskip \kern\inferLineSkip
   213                 \moveright \RuleAdjust \vbox{\hrule width\RuleWidth}\relax
   214                 \nointerlineskip \kern\inferLineSkip
   215                 \moveright \LowerAdjust \box\@LowerPart }\relax
   216 %
   217         \@ifEmpty{#1}{}{\relax
   218 %
   219         \HLabelAdjust=\wd\ResultBox     \advance\HLabelAdjust by -\RuleAdjust
   220         \advance\HLabelAdjust by -\RuleWidth
   221         \WidthAdjust=\HLabelAdjust
   222         \advance\WidthAdjust by -\inferLabelSkip
   223         \advance\WidthAdjust by -\wd\@LabelPart
   224         \ifdim \WidthAdjust < 0pt \WidthAdjust=0pt \fi
   225 %
   226         \VLabelAdjust=\dp\@LabelPart
   227         \advance\VLabelAdjust by -\ht\@LabelPart
   228         \VLabelAdjust=0.5\VLabelAdjust  \advance\VLabelAdjust by \LowerHeight
   229         \advance\VLabelAdjust by \inferLineSkip
   230 %
   231         \setbox\ResultBox=\hbox{\box\ResultBox
   232                 \kern -\HLabelAdjust \kern\inferLabelSkip
   233                 \raise\VLabelAdjust \box\@LabelPart \kern\WidthAdjust}\relax
   234 %
   235         }\relax % end @ifEmpty
   236 %
   237         \else % \@inferRulefalse
   238 %
   239         \setbox\ResultBox=\vbox{
   240                 \moveright \UpperAdjust \box\@UpperPart
   241                 \nointerlineskip \kern\inferLineSkip
   242                 \moveright \LowerAdjust \hbox{\unhbox\@LowerPart
   243                         \@ifEmpty{#1}{}{\relax
   244                         \kern\inferLabelSkip \unhbox\@LabelPart}}}\relax
   245         \fi
   246 %
   247         \global\@RightOffset=\wd\ResultBox
   248         \global\advance\@RightOffset by -\@LeftOffset
   249         \global\advance\@RightOffset by -\LowerWidth
   250         \if@ReturnLeftOffset \else \global\@LeftOffset=\@SavedLeftOffset \fi
   251 %
   252         \box\ResultBox
   253         \@RestoreMath
   254 }