% $Id$
%
% Calculational proofs, a la Dijkstra, Gries, Back and von Wright, etc.
% See: David Gries, "Teaching Calculation and Discrimination:
%      A More Effective Curriculum", CACM 34(3):44-55, Mar. 1991.
% and
%      Ralph-Johan Back and Joakim von Wright,
%      "Refinement Calculus: A Systematic Introduction",
%      Springer-Verlag, 1998.
%
% Examples of usage of these macros are found in the accompanying file
% calculation-sample.tex.
%
% AUTHOR: Gary T. Leavens

%%% You may want to define the following with \renewcommand...

% Brackets around normal and fixed width reasons
\newcommand{\LEFTREASONBRACKET}{\langle}
\newcommand{\RIGHTREASONBRACKET}{\rangle}
% Brackets for long reasons
\newcommand{\LONGLEFTREASONBRACKET}{\left\LEFTREASONBRACKET}
\newcommand{\LONGRIGHTREASONBRACKET}{\right\RIGHTREASONBRACKET}
% width of long and fixed width reasons
\newcommand{\LONGREASONWIDTH}{5.4in}
\newcommand{\FIXEDWIDTHREASONWIDTH}{\LONGREASONWIDTH}
% The phrase that starts each reason
\newcommand{\BYPHRASE}{by~}
% Provability symbol
\newcommand{\PROVABILITYSYMBOL}{\vdash}
% Has type symbol
\newcommand{\CALCULATIONHASTYPE}{:}
% Subdeduction symbols a la Back and von Wright
\newcommand{\SUBDEDUCTIONMARKER}{\bullet}
\newcommand{\CONCLUDEMARKER}{\cdot}

% The macros below assume that you have defined \QED,
% e.g., as \newcommand{\QED}{q.e.d.}


%%% The rest shouldn't usually need to be redefined

% The main environment
\newenvironment{calculation}{
\samepage
\begin{tabbing}
mm \= n \= mm \= n \= mm \= n \= mm \= n \= mm \= n \= mm \= n \= \kill
}{
\end{tabbing}
}

% Use for the last formula (to avoid extra vertical space)
\newcommand{\LASTFORMULA}[1]{\> \ensuremath{#1}}
% Use for the last formula in a proof that concludes the proof
\newcommand{\QEDATEND}{~~\QED}
\newcommand{\QEDFORMULA}[1]{\LASTFORMULA{#1\QEDATEND}}

% All other formulas in a calculation
\newcommand{\FORMULA}[1]{\LASTFORMULA{#1} \\}

% Generic reason, with connective and the justification
\newcommand{\REASON}[2]{%
    \ensuremath{#1}\> \>
       \mbox{\ensuremath{\LEFTREASONBRACKET}{\BYPHRASE}#2\ensuremath{\RIGHTREASONBRACKET}} \\}

% Reasons with longer justifications, with the right bracket at the end
\newcommand{\FIXEDWIDTHREASON}[2]{%
     \ensuremath{#1}\> \>
       \ensuremath{\LEFTREASONBRACKET}{\BYPHRASE}%
       \parbox[t]{\FIXEDWIDTHREASONWIDTH}{#2\ensuremath{\RIGHTREASONBRACKET}}
       \\
     }

% Reasons with longer justifications, with big brackets around the reason
\newcommand{\LONGREASON}[2]{%
    \ensuremath{#1}\> \>
      \ensuremath{\LONGLEFTREASONBRACKET
                  \parbox[c]{\LONGREASONWIDTH}{{\BYPHRASE}#2}
                  \LONGRIGHTREASONBRACKET
                 }
      \\
    }

% Specialization of reasons to equality
\newcommand{\EQREASON}[1]{\REASON{=}{#1}}
\newcommand{\EQLONGREASON}[1]{\LONGREASON{=}{#1}}
\newcommand{\EQFIXEDWIDTHREASON}[1]{\FIXEDWIDTHREASON{=}{#1}}

% Use \FOCUS{E} to say that subformula E will be changed in the following step
\newcommand{\FOCUS}[1]{\mbox{``}#1\mbox{''}}


%% The following are for Back and von Wright style calculations.
%% First time users may want to ignore these.

% Use for assumptions in a type-deduction style proof
\newcommand{\GIVEN}[1]{\FORMULA{#1}}
% Use \PROVETHAT to start the body of a type-deduction style proof.
\newcommand{\PROOFLINE}[2]{\ensuremath{#1} \> \ensuremath{#2} \\}
\newcommand{\PROVETHAT}[1]{\PROOFLINE{\PROVABILITYSYMBOL}{#1}}
%% Subdeductions
% Use to start a subdeduction
\newcommand{\SUBDEDUCTION}[1]{\+\+\kill\PROOFLINE{\SUBDEDUCTIONMARKER}{#1}}
% Use to separate one subdeduction from another
\newcommand{\ANDALSO}{\-\-\kill}
% Use to start the next subdeduction after \ANDALSO
\newcommand{\NEXTDEDUCTION}[1]{\PROOFLINE{\SUBDEDUCTIONMARKER}{#1}}
% Use to conclude a subdeduction 
\newcommand{\CONCLUDE}[1]{\-\-\kill\PROOFLINE{\CONCLUDEMARKER}{#1}}
% Use when the last formula is also a conclusion
\newcommand{\LASTCONCLUDE}[1]{\-\-\kill\ensuremath{\CONCLUDEMARKER} \> \ensuremath{#1}}
% Use in a type-deduction proof instead of \REASON, to give the rule name
\newcommand{\TYPINGRULE}[1]{\ensuremath{\CALCULATIONHASTYPE} \> ~~~ #1 \\}

% end of calculation.tex
