Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Jim Alves-Foss <jimaf@ptolemy-ethernet.arc.nasa.gov>
Message-Id: <9407121608.AA14658@ptolemy.arc.nasa.gov>
Subject: Hol Macros for LaTeX (2.09)
To: info-hol@leopard.cs.byu.edu
Date: Tue, 12 Jul 1994 09:08:50 -0700 (PDT)
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 11046

Hi all,

Periodically I have received requests for adjustments for modifications to
my HOL macros package for LaTeX (v 2.09). With the new version of LaTeX(2e) 
being recently released I am considering updating the macro package. If any
of you have questions/comments/suggestions about changes/enhancements
please let me know. (I have included a copy of the lastest version of the
package, which is almost 2 years old).

===============================================================================
-Jim Alves-Foss, Assistant Professor
 Computer Science Department                voice: (208) 885-7232
 University of Idaho                        fax  : (208) 885-6645
 Moscow, ID 83844-1010                      email: jimaf@cs.uidaho.edu

===============================================================================
%-------------------------------------------
%
% HOL Macros (hol_macs.tex)
% Jim Alves-Foss (jimaf@cs.uidaho.edu)
% ALPHA VERSION October 1992
%
% 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 `\'.
%
% For set notation you must replace `{' and `}' with `\{` and `\}'
%
% \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''
%
%	         NOTE: You must encapsulate these macros in one of the
%                following environments to maintain your spacing, otherwise
%                LaTeX will eat the spaces. (Hopefully this will be fixed
%                in a later version.
%
% \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}
%
% Revision History:
%==================
% June 1994      - Request for enhancements sent out.
%
% October 1992   - Added parsing for set theory.
                 - ALPHA Version Released
% June 1992      - Fixed minor typographical error
% Nov 1990       - BETA version released 
%-------------------------------------------


% 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\^^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}{\columnwidth}
\addtolength{\hsbw}{-\arrayrulewidth}
\addtolength{\hsbw}{-\tabcolsep}
\newcommand\HOLSpacing{13pt}
\def\holsinglespace{\def\baselinestretch{1}\large\normalsize}
\def\endholsinglespace{}

% ---------------------------------------------------------------------
% 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.
% ---------------------------------------------------------------------

% A boxed environment 

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

% A boxed environment for HOL code that floats. 
% 
% NOTE: You must add the folowing to your style file (article.sty) to
% use fhol
%  
%  \def\fps@fhol{tbh} \def\ftype@fhol{3} \def\fhol{\@float{fhol}}
%  \let\endfhol\end@float \@namedef{fhol*}{\@dblfloat{fhol}}
%  \@namedef{endfhol*}{\end@dblfloat}
% 

\newenvironment{holfloat}{\holsinglespace\begin{fhol}[tbh]
\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}
\end{fhol}}

% A boxed environment for hol that does not float 

\newenvironment{hol}{\holsinglespace\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}}

\newenvironment{holfix}{\holsinglespace\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}{\holsinglespace\begin{flushleft}
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing\footnotesize
 \begin{holtt}}{\end{holtt}\endgroup
 \end{minipage}
 \end{flushleft}}

% An unboxed HOL environment whose font size is defined by HOLsize.
% To change size to small
% \newcommand\HOLsize{\small}
%
\newcommand\HOLsize{\footnotesize}
\newenvironment{holsizenb}{\holsinglespace\begin{flushleft}
 \begin{minipage}[b]{\hsbw}
 \vspace*{.06in}
 \begingroup\small\baselineskip\HOLSpacing\HOLsize
 \begin{holtt}}{\end{holtt}\endgroup
 \end{minipage}
 \end{flushleft}}

% Various commands for HOL symbols

   \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{\Lb}{\(\{\)}
   \newcommand{\Rb}{\(\}\)}

   \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\{\Lb                                         % {
\else\ifx#1\}\Rb                                         % }
\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>\Impl\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\fi\fi
\expandafter\next\postnext}