%------------------------------------------- % % 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 stars a new line, so if foo.tex ends with a % 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}