1% define page layout 2\setlength{\textwidth}{5.7in} 3\setlength{\textheight}{8.5in} 4%\setlength{\topmargin}{-0.125in} 5\setlength{\oddsidemargin}{18pt} 6\setlength{\evensidemargin}{18pt} 7%\setlength{\columnseprule}{.4pt} 8\setlength{\headheight}{19pt} 9\setlength{\headsep}{18pt} 10%\setlength{\footheight}{16pt} 11%\setlength{\footskip}{34pt} 12%\setlength{\headrulewidth}{2pt} 13%\setlength{\footrulewidth}{0pt} 14 15\renewcommand{\sectionmark}[1]{ } 16\renewcommand{\subsectionmark}[1]{ } 17 18 19%% FILE: holmac.tex 20%% This is a LaTeX macro for formatting HOL theory generated by the latex-hol 21%% library function 22%% By Wai Wong on 21 May 1991 23%% 24 25% check to see if this macro file has already been loaded 26\ifx\undefined\holmacs\def\holmacs{}\else\endinput\fi 27 28% Special symbols 29 30\def\US{\_} 31\def\SH{\#} 32\def\AM{\&} 33\def\PC{\%} 34\def\DO{\$} 35\def\BS{{\tt\char'134}} 36\def\PR{{\tt\char'23}} 37\def\TI{{\tt\char'176}} 38\def\AS{{\tt\char'52}} 39\def\LE{{\tt\char'74}} 40\def\BA{{\tt\char'174}} 41\def\GR{{\tt\char'76}} 42\def\LB{{\tt\char'133}} 43\def\RB{{\tt\char'135}} 44\def\CI{{\tt\char'136}} 45\def\LC{{\tt\char'173}} 46\def\RC{{\tt\char'175}} 47 48\def\GOAL{\relax\ifmmode\hbox{?\kern0.2em --}\quad\else\hbox{?kern0.2em --}\quad\fi} 49\def\THM{\relax\ifmmode\vdash\else$\vdash$\fi} 50\def\DEF{\relax\ifmmode\vdash\!\!\lower .5ex\hbox{{\scriptsize\sl def}}\quad% 51 \else$\vdash\!\!\lower.5ex\hbox{{\scriptsize\sl def}}\quad$\fi} 52\def\AND{\relax\ifmmode\wedge\else$\wedge$\fi} 53\def\OR{\relax\ifmmode\vee\else$\vee$\fi} 54\def\IMP{\relax\ifmmode\supset\else$\supset$\fi} 55\def\LONG{\relax\ifmmode\longrightarrow\else$\longrightarrow$\fi} 56\def\IFF{\relax\ifmmode\Longleftrightarrow\else$\Longleftrightarrow$\fi} 57\def\LEE{\relax\ifmmode\leq\else$\leq$\fi} 58\def\GEE{\relax\ifmmode\geq\else$\geq$\fi} 59\def\EXISTSUNIQUE{\relax\ifmmode\exists\forall\else$\exists\forall$\fi} 60\def\LES{\relax\ifmmode<\else$<$\fi} 61\def\GRE{\relax\ifmmode>\else$>$\fi} 62\def\MUL{\relax\ifmmode\times\else$\times$\fi} 63\def\NOT{\relax\ifmmode\neg\else{$\neg$}\fi} 64\def\FORALL{\relax\ifmmode\forall\else$\forall$\fi} 65\def\EXISTS{\relax\ifmmode\exists\else$\exists$\fi} 66\def\SELECT{\relax\ifmmode\varepsilon\else$\varepsilon$\fi} 67\def\FUNCOM{\relax\ifmmode\circ\else$\circ$\fi} 68\def\LAMBDA{\relax\ifmmode\lambda\else$\lambda$\fi} 69\def\RESDOT{\relax\ifmmode::\else$::$\fi} 70\def\DOT{\relax\ifmmode.\,\else$.\,$\fi} 71\def\NIL{\relax\ifmmode[\:]\else$[\:]$\fi} 72\def\EMPTYSET{\relax\ifmmode{\{\:\}}\else{$\{\:\}$}\fi} 73\def\BEGINSET{\relax\ifmmode\left\{\else{$\left\{\right.$}\fi} 74\def\ENDSET{\relax\ifmmode\right\}\else{$\left.\right\}$}\fi} 75\def\SUCHTHAT{\relax\ifmmode\mid\else$\mid$\fi} 76 77%\def\makeulactive{\catcode`\_=\active\relax} 78%\def\makeulsub{\catcode`\_=8\relax} 79%\let\ul=\_ 80%\begingroup 81% \makeulactive 82% \gdef\_{\ul} 83% \gdef_{\ul} 84%\endgroup 85%\def\dotoken#1#2{\mbox{#1#2}\endgroup} 86%\def\mlname{\begingroup\makeulactive\dotoken{\tt}} 87%\def\CONST{\begingroup\makeulactive\dotoken{\constfont}} 88%\def\KEYWD{\begingroup\makeulactive\dotoken{\keyfont}} 89 90\def\HOL{{\sc HOL}} 91% Tells TeX to break line after binary operators. 92\def\setholprec{\relpenalty=10000 \binoppenalty=9999 \raggedright} 93 94% The parents and types sections are set in ttlist environment 95\newenvironment{ttlist}{\begingroup\typefont}{\endgroup} 96 97% The constants and infix sections are set in typelist environment. 98% The labels are left justified. 99\def\labeledlabel#1{#1\hfil} 100\newenvironment{typelist}% 101 {\begin{list}{\ }% 102 {\typefont \setlength{\leftmargin}{0.8in}% 103 \setlength{\labelwidth}{0.7in}\setlength{\labelsep}{0.1in}% 104 \renewcommand{\makelabel}{\labeledlabel}}}% 105 {\end{list}} 106 107% The Axioms, definitions and theorems sections are set in thmlist environment 108\newenvironment{thmlist} 109 {\begin{list}{\ }% 110 {\setholprec \setlength{\leftmargin}{0.8in}% 111 \setlength{\labelwidth}{0.7in}\setlength{\labelsep}{0.1in}% 112 \renewcommand{\makelabel}{\labeledlabel}}}% 113 {\end{list}} 114 115 116\def\monthname{\ifcase\month 117v \or Jan\or Feb\or Mar\or Apr\or May\or Jun% 118 \or Jul\or Aug\or Sep\or Oct\or Nov\or Dec\fi}% 119\def\timestring{\begingroup 120 \count0 = \time \divide\count0 by 60 121 \count2 = \count0 % the hour 122 \count4 = \time \multiply\count0 by 60 123 \advance\count4 by -\count0 % the minute 124 \ifnum\count4<10 \toks1 = {0}% get a leading zero 125 \else \toks1 = {}% 126 \fi 127 \ifnum\count2<12 \toks0 = {a.m.}% 128 \else \toks0 = {p.m.}% 129 \advance\count2 by -12 130 \fi 131 \ifnum\count2=0 \count2 = 12 \fi 132 \number\count2:\the\toks1 \number\count4 133 \thinspace \the\toks0 134\endgroup}% 135\def\timestamp{\number\day\space\monthname\space 136 \number\year\quad\timestring}% 137\def\printtimestamp{Printed at \timestring\space% 138 on \number\day\space\monthname\space\number\year.} 139 140% The following commands are generated by latex_theory_to 141% They may be redefined to suit your style. 142% \sec{section_name} marks the sections within a theory, e.g., Types, Theorems. 143% \theory{theory_name} marks the beginning of the theory, if the file is 144% generated for being included in other LaTeX files. 145% \endthy{theory_name} marks the end of the theory. 146% 147\def\sec#1{\section*{#1}\noindent} 148\def\theory#1{\section{#1}} 149\def\endthy#1{\hbox to\hsize{\hrulefill\ End of theory {\tt#1}\ \hrulefill}} 150 151\def\typefont{\tt} % for types, ML identifiers 152\def\constfont{\sf} % for HOL constants 153\def\keyfont{\bf} % for keywords 154 155 156 157\makeatletter 158\def\verb{\begingroup \catcode``=13 \@noligs 159\verbatim@font \let\do\@makeother \dospecials 160\@ifstar{\@sverb}{\@verb}} 161 162% Definitions of \@sverb and \@verb changed so \verb+ foo+ does not lose 163% leading blanks when it comes at the beginning of a line. 164% Change made 24 May 89. Suggested by Frank Mittelbach and Rainer Sch\"opf. 165% 166\def\@sverb#1{\def\@tempa ##1#1{\leavevmode\null##1\endgroup}\@tempa} 167 168\def\@verb{\@vobeyspaces \frenchspacing \@sverb} 169 170\def\wordn{\verb|:word|$n$} 171\def\word{\@ifnextchar[{\@word}{\@word[*]}} 172\def\@word[#1]{\verb|:(#1)word|} 173\def\sect{\@startsection {subsection}{1}{\z@}{-3.5ex plus -1ex minus 174 -.2ex}{1.5ex plus .2ex}{\normalsize\bf}} 175\def\subsect{\@startsection {subsubsection}{2}{\z@}{-3.5ex plus -1ex minus 176 -.2ex}{-1em}{\footnotesize\bf}} 177\def\inputmlfile#1{\begingroup \footnotesize \input#1 \endgroup} 178 179\renewenvironment{theindex}{\begin{multicols}{2}[\section*{\indexname}]% 180 \columnseprule \z@ \columnsep 35\p@ 181 \parindent\z@ \parskip\z@ plus.3\p@\relax\let\item\@idxitem}{\end{multicols}} 182 183\def\@idxitem{\par\hangindent 40\p@} 184 185\def\subitem{\par\hangindent 40\p@ \hspace*{20\p@}} 186 187\def\subsubitem{\par\hangindent 40\p@ \hspace*{30\p@}} 188 189\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax} 190 191\makeatother 192 193 194\def\NBWORD#1#2{\CONST{NBWORD}\,\CONST{#1}\,\CONST{#2}} 195\def\SEG#1#2#3{\CONST{SEG}\,\CONST{#1}\,\CONST{#2}\,#3} 196\def\T{\CONST{T}} 197 198\def\dotoken#1#2{\mbox{#1#2}\endgroup} 199\def\idxname#1{\begingroup\makeulother\dotoken#1} 200\def\dotokenidx#1#2{\mbox{#1#2}\index{#2@\string\idxname{#1}{#2}}\endgroup} 201\def\mlname{\begingroup\makeulother\dotokenidx{\tt}} 202\def\CONST{\begingroup\makeulother\dotokenidx{\constfont}} 203\def\KEYWD{\begingroup\makeulother\dotoken{\keyfont}} 204 205\def\idxmlname{\begingroup\makeulother\dotoken{\tt}} 206\def\idxconst{\begingroup\makeulother\dotoken{\constfont}} 207\def\ul#1{\relax\ifmmode\underline#1\else$\underline{#1}$\fi} 208 209% define environment for HOL definitions and theorems 210\def\makeulother{\catcode`\_=12\relax} 211\def\makeulsub{\catcode`\_=8\relax} 212%\begingroup 213% \makeulother 214% \gdef\_{\ul} 215%\endgroup 216\def\doholdef#1{\par\vspace*{5pt}\index{#1@\string\idxmlname{#1}|ul}% 217 \flushleft{\bf HOL Definition }({\tt#1})\label{def-#1}\endgroup} 218\def\holdef{\begingroup\makeulother\doholdef} 219\let\endholdef=\endflushleft 220 221\def\doholthm#1{\par\index{#1@\string\idxmlname{#1}|ul}% 222 \flushleft{\bf HOL Theorem }({\tt#1})\label{thm-#1}\endgroup} 223\def\holthm{\begingroup\makeulother\doholthm} 224\let\endholthm=\endflushleft 225 226\def\sfc\sf \def\constfont{\sfc} 227