%-------------------------------------------
%
% HOL Macros. 
% Jim Alves-Foss (foss@iris.eecs.ucdavis.edu) [128.120.57.20]
% BETA VERSION November 1990
%
% Thanks to Tom Schubert, Jim Buffenbarger, and Phil Windley for
%   their help and contributions (directly or indirectly)
%
% This file consists of a collection of definitions and macros
% for use in LaTeX documents discussing the HOL language and
% its associated proofs.
%
% The primary macros introduced here are given below.
%
% NOTE: for holdef and holthm you must replace ALL lambda symbols
% `\' by `\. ' this can be accomplished automatically in HOL by the command:
%   set_lambda`\\.`;;
% Which will then display the lamda symbol as`\. ' but will permit input to
% still be `\'.
%
% \holthm{defn}  Which takes defn (cut directly from HOL output
%                and converts all the symbols (ie. |- ==>) to their
%                mathematical equivalents.
%
% \holdef{defn}  Same as holthm except that the turnstile is subscripted 
%                by ``def''
%
% \begin{hol} ... \end{hol} Defines an environment for HOL theorems and
%                definitions. This environment it identical to alltt except
%                that it places a box around the text and ~ still works
%
% \begin{holnb} ... \end{holnb} Same as ``hol'' but no box
%
% and you must include this file:
% \include{hol_macros}
%
%-------------------------------------------


% HOLTT DOCUMENT-STYLE OPTION - 
% Modified for HOL macro use Nov 1990 by Jim Alves-Foss and Phil Windley from :

% ALLTT DOCUMENT-STYLE OPTION - released 17 December 1987
%    for LaTeX version 2.09
% Copyright (C) 1987 by Leslie Lamport


% Defines the `alltt' environment, which is like the `verbatim'
% environment except that `\', `\{', and `\}' have their usual meanings.
% Thus, other commands and environemnts can appear within an `alltt'
% environment.  Here are some things you may want to do in an `alltt'
% environment:
% 
% * Change fonts--e.g., by typing `{\em empasized text\/}'.
% 
% * Insert text from a file foo.tex by typing `input{foo}'.  Beware that
%   each <return> stars a new line, so if foo.tex ends with a <return>
%   you can wind up with an extra blank line if you're not careful.
% 
% * Insert a math formula.  Note that `$' just produces a dollar sign,
%   so you'll have to type `\(...\)' or `\[...\]'.  Also, `^' and `_'
%   just produce their characters; use `\sp' or `\sb' for super- and
%   subscripts, as in `\(x\sp{2}\)'.


\makeatletter

\def\holdocspecials{\do\ \do\$\do\&%
  \do\#\do\^\do\^^K\do\_\do\^^A\do\%}

\def\holtt{\trivlist \item[]\if@minipage\else\vskip\parskip\fi
\leftskip\@totalleftmargin\rightskip\z@
\parindent\z@\parfillskip\@flushglue\parskip\z@
\@tempswafalse \def\par{\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
%\obeylines \tt \catcode``=13 \@noligs \let\do\@makeother \holdocspecials
\obeylines \tt \let\do\@makeother \holdocspecials
 \frenchspacing\@vobeyspaces}

\let\endholtt=\endtrivlist

\makeatother

\newlength{\hsbw}
\setlength{\hsbw}{\textwidth}
\addtolength{\hsbw}{-\arrayrulewidth}
\addtolength{\hsbw}{-\tabcolsep}
\newcommand\HOLSpacing{13pt}

% ---------------------------------------------------------------------
% Macro for boxed ML functions, etc.
%
% Usage: (1) \begin{boxed}\begin{verbatim}
%	        .
%	        < lines giving names and types of mk functions >
%	        .
%	     \end{verbatim}\end{boxed}   
%
%            typesets the given lines in a box.  
%
%            Conventions: lines are left-aligned under the "g" of begin, 
%	     and used to highlight primary reference for the ml function(s)
%	     that appear in the box.
% ---------------------------------------------------------------------

\newenvironment{boxed}{\begin{flushleft}
 \begin{tabular}{@{}|c@{}|@{}}\hline 
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline 
 \end{tabular}
 \end{flushleft}}

\newenvironment{hol}{\begin{flushleft}
 \begin{tabular}{@{}|c@{}|@{}}\hline 
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing\footnotesize
 \begin{holtt}}{\end{holtt}\endgroup
 \end{minipage}\\ \hline 
 \end{tabular}
 \end{flushleft}}

% HOL environment not boxed %
\newenvironment{holnb}{\begin{flushleft}
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing\footnotesize
 \begin{holtt}}{\end{holtt}\endgroup
 \end{minipage}
 \end{flushleft}}

   \newcommand\hilbert{\varepsilon}
   \newcommand{\Defn}{\(\vdash\sb{\it def}\)}
   \newcommand{\Thm}{\(\vdash\)}
   \newcommand{\Cond}{\(\rightarrow\)}
   \newcommand{\Eqv}{\(\equiv\)}
   \newcommand{\Iff}{\(\Longleftrightarrow\)}
   \newcommand{\Fa}{\(\forall\)}
   \newcommand{\Et}{\(\exists\)}
   \newcommand{\Eu}{\(\exists_{unique}\)}
   \newcommand{\La}{\(\land\)}
   \newcommand{\Lo}{\(\lor\)}
   \newcommand{\Lx}{\(\oplus\)}
   \newcommand{\Lc}{\(\lnot\)}
   \newcommand{\Impl}{\(\Longrightarrow\)}
   \newcommand{\Func}{\(\to\)}
   \newcommand{\Bar}{\(\mid\)}
   \newcommand{\uqu}[1]{\(\forall\)\ #1.\ }
   \newcommand{\equ}[1]{\(\exists\)\ #1.\ }
   \newcommand{\hqu}[1]{\(\hilbert\)\ #1.\ }
   \newcommand{\lqu}[1]{\(\lambda\)\ #1.\ }
   \newcommand{\Lam}{\(\lambda\)}
   \newcommand{\Plus}{\(+\)}
   \newcommand{\Minus}{\(-\)}
   \newcommand{\Prime}{\('\)}
   \newcommand{\Und}{\_}
   \newcommand{\Lt}{\(<\)}
   \newcommand{\Gt}{\(>\)}
   \newcommand{\Leq}{\(\leq\)}
   \newcommand{\Geq}{\(\geq\)}
   \newcommand{\Eq}{\(=\)}

\newcommand{\Hilbert}{\(\hilbert\)}
\newcommand{\Imp}{\(\Rightarrow\)}
\newcommand{\Conj}{\(\wedge\)}
\newcommand{\Disj}{\(\vee\)}
\newcommand{\Neg}{\(\neg\)}
\newcommand{\Pnd}{\(\Diamond\)}
\newcommand{\var}[1]{{\it #1}}

%----------------
%  The following are recursive definitions that take HOL output and convert
%  it into a nice mathematical format in LaTeX. Use holthm for theorems and
%  holdef for definitions (Warning do not include too many definitions or
%  theorems together, as the TeX buffer will overflow
%---------------

\long\def\holthm#1{{\def\Turns{\Thm} \rechol#1\end\end\end}}

\long\def\holdef#1{{\def\Turns{\Defn} \rechol#1\end\end\end}}

\long\def\rechol#1#2#3{\let\next=\rechol\def\postnext{#2#3}\ifx#1\end
\let\next=\relax\def\postnext{\relax}
\else\ifx#1!\Fa                                          % For all !
\else\ifx#1@\Hilbert                                     % Hilbert Choice @
\else\ifx#1\#\Pnd                                        % Product #
\else\ifx#1'\Prime                                       % Prime  ' 
\else\ifx#1~\Neg                                         % Negation  ~ 
\else\ifx#1\~\Neg
\else\ifx#1_\Und                                         % Underscore  _
\else\ifx#1+\Plus
\else\ifx#1\/\Disj                                       % Disjunction  \/
\else\ifx#1\.\Lam                                        % Remove cntrl seq
\else\ifx#1>\ifx#2=\Geq\def\postnext{#3}\else\Gt\fi      % Greater, Geq >  >=
\else\ifx#1?\ifx#2!\Eu\def\postnext{#3}\else\Et\fi       % Exists(unique) ? ?!
\else\ifx#1-\ifx#2\>\Func\def\postnext{#3}               % Minus, Function
	    \else\Minus\fi				 % - ->
\else\ifx#1|\ifx#2-\Turns\def\postnext{#3}\else\Bar\fi   % Turnstile,Bar |- |
\else\ifx#1<\ifx#2=\ifx#3>\Iff\def\postnext{}            % Less, Leq, Iff
                   \else\Leq\def\postnext{#3}\fi         $ <  <=  <=>
            \else\Lt\fi
\else\ifx#1=\ifx#2=\ifx#3>\Imp\def\postnext{}            % Eq, Eqv, Cond, Imp
                   \else\Eqv\def\postnext{#3}\fi         % = == => ==>
            \else\ifx#2>\Cond\def\postnext{#3}
                 \else\Eq\fi\fi
\else\ifx#1/\ifx#2\^^M\Conj\par\def\postnext{#3}         % Conjunction, slash
            \else\ifx#2\ \Conj\ \def\postnext{#3}\else#1\fi\fi  % /\  /
\else#1\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi
\expandafter\next\postnext}
