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