1% ===================================================================== 2% 3% Macros for typesetting the HOL system manual 4% 5% ===================================================================== 6 7% --------------------------------------------------------------------- 8% Abbreviations for words and phrases 9% --------------------------------------------------------------------- 10 11\newcommand\TUTORIAL{{\footnotesize\sl TUTORIAL}} 12\newcommand\DESCRIPTION{{\footnotesize\sl DESCRIPTION}} 13\newcommand\REFERENCE{{\footnotesize\sl REFERENCE}} 14\newcommand\LOGIC{{\footnotesize\sl LOGIC}} 15\newcommand\LIBRARIES{{\footnotesize\sl LIBRARIES}} 16\usepackage{textcomp} 17 18\newcommand{\bs}{\texttt{\char'134}} % backslash 19\newcommand{\lb}{\texttt{\char'173}} % left brace 20\newcommand{\rb}{\texttt{\char'175}} % right brace 21\newcommand{\td}{\texttt{\char'176}} % tilde 22\newcommand{\lt}{\texttt{\char'74}} % less than 23\newcommand{\gt}{\texttt{\char'76}} % greater than 24\newcommand{\dol}{\texttt{\char'44}} % dollar 25\newcommand{\pipe}{\texttt{\char'174}} 26\newcommand{\apost}{\texttt{\textquotesingle}} 27% back quote (tt font) 28\newcommand{\bq}{\texttt{\char'140}} 29% double back quotes `` 30\newcommand{\dq}{\bq\bq} 31\newcommand{\ldquo}{\mbox{\textrm{``}}} 32\newcommand{\rdquo}{\mbox{\textrm{''}}} 33 34%These macros were included by slind: 35 36\newcommand{\holquote}[1]{\dq#1\dq} 37\newcommand{\uholquote}[1]{\mbox{\rmfamily\upshape ``}#1\mbox{\rmfamily\upshape ''}} 38 39\def\HOL{\textsc{Hol}} 40\def\holn{\HOL} % i.e. hol n(inety-eight), no digits in 41 % macro names is a bit of a pain; deciding to do away 42 % with hol98 nomenclature means that we just want to 43 % write HOL for hol98. 44\def\holnversion{Kananaskis-12} 45\def\holnsversion{Kananaskis~12} % version with space rather than hyphen 46\def\LCF{{\small LCF}} 47\def\LCFLSM{{\small LCF{\kern-.2em}{\normalsize\_}{\kern0.1em}LSM}} 48\def\PPL{{\small PP}{\kern-.095em}$\lambda$} 49\def\PPLAMBDA{{\small PPLAMBDA}} 50\def\ML{{\small ML}} 51\def\holmake{\texttt{Holmake}} 52 53\newcommand\ie{\mbox{\textit{i{.}e{.}}}} 54\newcommand\eg{\mbox{\textit{e{.}g{.}}}} 55\newcommand\viz{\mbox{viz{.}}} 56\newcommand\adhoc{\mbox{\it ad hoc}} 57\newcommand\etal{{\it et al.\/}} 58% NOTE: \etc produces wrong spacing if used between sentences, that is 59% like here \etc End such sentences with non-macro etc. 60\newcommand\etc{\mbox{\textit{etc{.}}}} 61 62% --------------------------------------------------------------------- 63% Simple abbreviations and macros for mathematical typesetting 64% --------------------------------------------------------------------- 65 66\newcommand\fun{{\to}} 67\newcommand\prd{{\times}} 68 69\newcommand\conj{\ \wedge\ } 70\newcommand\disj{\ \vee\ } 71\newcommand\imp{ \Rightarrow } 72\newcommand\eqv{\ \equiv\ } 73\newcommand\cond{\rightarrow} 74\newcommand\vbar{\mid} 75\newcommand\turn{\ \vdash\ } % FIXME: "\ " results in extra space 76\newcommand\hilbert{\varepsilon} 77\providecommand\eqdef{\ \equiv\ } 78\renewcommand\eqdef{\ \equiv\ } 79 80\newcommand\natnums{\mbox{${\sf N}\!\!\!\!{\sf N}$}} 81\newcommand\bools{\mbox{${\sf T}\!\!\!\!{\sf T}$}} 82 83\newcommand\p{$\prime$} 84\newcommand\f{$\forall$\ } 85\newcommand\e{$\exists$\ } 86 87\newcommand\orr{$\vee$\ } 88\newcommand\negg{$\neg$\ } 89 90\newcommand\arrr{$\rightarrow$} 91\newcommand\hex{$\sharp $} 92 93\newcommand{\uquant}[1]{\forall #1.\ } 94\newcommand{\equant}[1]{\exists #1.\ } 95\newcommand{\hquant}[1]{\hilbert #1.\ } 96\newcommand{\iquant}[1]{\exists ! #1.\ } 97\newcommand{\lquant}[1]{\lambda #1.\ } 98 99\newcommand{\leave}[1]{\\[#1]\noindent} 100\newcommand\entails{\mbox{\rule{.3mm}{4mm}\rule[2mm]{.2in}{.3mm}}} 101 102% --------------------------------------------------------------------- 103% Font-changing commands 104% --------------------------------------------------------------------- 105 106\newcommand{\theory}[1]{\hbox{{\small\tt #1}}} 107\newcommand{\theoryimp}[1]{\texttt{#1}} 108 109\newcommand{\con}[1]{{\sf #1}} 110\newcommand{\rul}[1]{{\tt #1}} 111\newcommand{\ty}[1]{\textsl{#1}} 112 113\newcommand{\ml}[1]{\mbox{{\def\_{\char'137}\texttt{#1}}}} 114\newcommand{\holtxt}[1]{\ml{#1}} 115\newcommand\ms{\tt} 116\newcommand{\s}[1]{{\small #1}} 117 118\newcommand{\pin}[1]{{\bf #1}} 119% FIXME: for multichar symbols \mathit should be used. 120\def\m#1{\mbox{\normalsize$#1$}} 121 122% --------------------------------------------------------------------- 123% Abbreviations for particular mathematical constants etc. 124% --------------------------------------------------------------------- 125 126\providecommand{\T}{\con{T}} 127\renewcommand{\T}{\con{T}} 128\newcommand\F{\con{F}} 129\newcommand\OneOne{\con{One\_One}} 130\newcommand\OntoSubset{\con{Onto\_Subset}} 131\newcommand\Onto{\con{Onto}} 132\newcommand\TyDef{\con{Type\_Definition}} 133\newcommand\Inv{\con{Inv}} 134\newcommand\com{\con{o}} 135\newcommand\Id{\con{I}} 136\newcommand\MkPair{\con{Mk\_Pair}} 137\newcommand\IsPair{\con{Is\_Pair}} 138\newcommand\Fst{\con{Fst}} 139\newcommand\Snd{\con{Snd}} 140\newcommand\Suc{\con{Suc}} 141\newcommand\Nil{\con{Nil}} 142\newcommand\Cons{\con{Cons}} 143\newcommand\Hd{\con{Hd}} 144\newcommand\Tl{\con{Tl}} 145\newcommand\Null{\con{Null}} 146\newcommand\ListPrimRec{\con{List\_Prim\_Rec}} 147 148 149\newcommand\SimpRec{\con{Simp\_Rec}} 150\newcommand\SimpRecRel{\con{Simp\_Rec\_Rel}} 151\newcommand\SimpRecFun{\con{Simp\_Rec\_Fun}} 152\newcommand\PrimRec{\con{Prim\_Rec}} 153\newcommand\PrimRecRel{\con{Prim\_Rec\_Rel}} 154\newcommand\PrimRecFun{\con{Prim\_Rec\_Fun}} 155 156\newcommand\bool{\ty{bool}} 157\newcommand\num{\ty{num}} 158\newcommand\ind{\ty{ind}} 159\newcommand\lst{\ty{list}} 160 161% --------------------------------------------------------------------- 162% \minipagewidth = \textwidth minus 1.02 em 163% --------------------------------------------------------------------- 164 165\newlength{\minipagewidth} 166\setlength{\minipagewidth}{\textwidth} 167\addtolength{\minipagewidth}{-1.02em} 168 169% --------------------------------------------------------------------- 170% Environment for the items on the title page of a case study 171% --------------------------------------------------------------------- 172 173\newenvironment{inset}[1]{\noindent{\large\bf #1}\begin{list}% 174{}{\setlength{\leftmargin}{\parindent}% 175\setlength{\topsep}{-.1in}}\item }{\end{list}\vskip .4in} 176 177% --------------------------------------------------------------------- 178% Macros for little HOL sessions displayed in boxes. 179% 180% Usage: (1) \setcounter{sessioncount}{1} resets the session counter 181% 182% (2) \begin{session}\begin{verbatim} 183% . 184% < lines from hol session > 185% . 186% \end{verbatim}\end{session} 187% 188% typesets the session in a numbered box. 189% --------------------------------------------------------------------- 190 191\newlength{\hsbw} 192\setlength{\hsbw}{\textwidth} 193\addtolength{\hsbw}{-\arrayrulewidth} 194\addtolength{\hsbw}{-\tabcolsep} 195\newcommand\HOLSpacing{13pt} 196 197\newcounter{sessioncount} 198\setcounter{sessioncount}{0} 199 200\newenvironment{session}{\begin{flushleft} 201 \refstepcounter{sessioncount} 202 \begin{tabular}{@{}|c@{}|@{}}\hline 203 \begin{minipage}[b]{\hsbw} 204 \vspace*{-.5pt} 205 \begin{flushright} 206 \rule{0.01in}{.15in}\rule{0.3in}{0.01in}\hspace{-0.35in} 207 \raisebox{0.04in}{\makebox[0.3in][c]{\footnotesize\sl \thesessioncount}} 208 \end{flushright} 209 \vspace*{-.55in} 210 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline 211 \end{tabular} 212 \end{flushleft}} 213 214% --------------------------------------------------------------------- 215% Macro for boxed ML functions, etc. 216% 217% Usage: (1) \begin{holboxed}\begin{verbatim} 218% . 219% < lines giving names and types of mk functions > 220% . 221% \end{verbatim}\end{holboxed} 222% 223% typesets the given lines in a box. 224% 225% Conventions: lines are left-aligned under the "g" of begin, 226% and used to highlight primary reference for the ml function(s) 227% that appear in the box. 228% --------------------------------------------------------------------- 229 230\newenvironment{holboxed}{\begin{flushleft} 231 \begin{tabular}{@{}|c@{}|@{}}\hline 232 \begin{minipage}[b]{\hsbw} 233% \vspace*{-.55in} 234 \vspace*{.06in} 235 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ \hline 236 \end{tabular} 237 \end{flushleft}} 238 239% --------------------------------------------------------------------- 240% Macro for unboxed ML functions, etc. 241% 242% Usage: (1) \begin{hol}\begin{verbatim} 243% . 244% < lines giving names and types of mk functions > 245% . 246% \end{verbatim}\end{hol} 247% 248% typesets the given lines exactly like {boxed}, except there's 249% no box. 250% 251% Conventions: lines are left-aligned under the "g" of begin, 252% and used to display ML code in verbatim, left aligned. 253% --------------------------------------------------------------------- 254 255\newenvironment{hol}{\begin{flushleft} 256 \begin{tabular}{c@{}@{}} 257 \begin{minipage}[b]{\hsbw} 258% \vspace*{-.55in} 259 \vspace*{.06in} 260 \begingroup\small\baselineskip\HOLSpacing}{\endgroup\end{minipage}\\ 261 \end{tabular} 262 \end{flushleft}} 263 264% --------------------------------------------------------------------- 265% Emphatic brackets 266% --------------------------------------------------------------------- 267 268\newcommand\leb{\lbrack\!\lbrack} 269\newcommand\reb{\rbrack\!\rbrack} 270 271 272% --------------------------------------------------------------------- 273% Quotations 274% --------------------------------------------------------------------- 275 276 277%These macros were included by ap; they are used in Chapters 9 and 10 278%of the HOL DESCRIPTION 279 280\newcommand{\inds}%standard infinite set 281 {\mbox{\rm I}} 282 283\newcommand{\ch}%standard choice function 284 {\mbox{\rm ch}} 285 286\newcommand{\den}[1]%denotational brackets 287 {[\![#1]\!]} 288 289\newcommand{\two}%standard 2-element set 290 {\mbox{\rm 2}} 291