1\documentclass{scrartcl} 2 3\usepackage{holindex} 4 5\setHOLlinewidth{80} %default is 80 6%\setHOLoverrides{over} %option 7 8\begin{document} 9 10\section{Holindex usage} 11 12Similar usage as bibtex, makeindex etc. 13 14\begin{enumerate} 15\item create jobname.tex with header 16\begin{verbatim} 17\usepackage{holindex} 18\setHOLlinewidth{80} %optional default is 80 19\setHOLoverrides{file} %optional 20\end{verbatim} 21\item make sure that \texttt{holindex} is loaded after packages like 22 \texttt{natbib}, since it loads \texttt{underscore} and this will 23 break commands like \texttt{cite} that get arguments with 24 underscores if they are not properly protected 25\item run \texttt{mkmunge.exe theories} to generate \texttt{munge.exe} 26 for your theories 27\item run latex on jobname.tex to generate jobname.hix 28\item run \texttt{munge.exe -index jobname} to create jobname.tde and jobname.tid 29\item rerun latex to use jobname.tid and jobname.tde 30\item rerun the munger whenever some significant HOL stuff changed 31\item if using emacs with AucTex you might want to add to your \texttt{.emacs} 32\begin{alltt} 33(eval-after-load "tex" 34 '(add-to-list 'TeX-command-list 35 '("Holindex" "munge.exe -index %s" 36 TeX-run-background t t :help "Run Holindex") t)) 37\end{alltt} 38\end{enumerate} 39 40 41\section{Defining} 42\begin{verbatim} 43 \defHOLtm{unique_id}{label}{def} 44 \defHOLty{unique_id}{label}{def} 45 \defHOLthm{unique_id}{label}{def} 46 47 (Theorems don't need defining. Theorem IDs of the form 48 theory.name are automatically recognised. 49 The label is their name and the def 50 is stored in the theory. Giving them an extra label 51 will add this label after their name. 52 53 You can define theorems anyhow. This is useful, when 54 - the theorem name is too lengthy / contains special characters 55 - you want to use one theorem with different formating options 56 - you want to add a theorem several times to the index) 57 58 Use the same formating options as the munger 59 \formatHOLtm{unique_id}{options} 60 \formatHOLty{unique_id}{options} 61 \formatHOLthm{unique_id}{options} 62 63 Combine definition and formating 64 \formatDefHOLtm{unique_id}{label}{options}{def} 65 \formatDefHOLty{unique_id}{label}{options}{def} 66 67 Add it explicitly to the index (citations are added automatically) 68 \indexHOLtm{unique_id} 69 \indexHOLty{unique_id} 70 \indexHOLthm{unique_id} 71 72 Print long version in the index 73 \longIndexHOLthm{unique_id} 74 \longIndexHOLty{unique_id} 75 \longIndexHOLtm{unique_id} 76 \shortIndexHOLthm{unique_id} 77 \shortIndexHOLty{unique_id} 78 \shortIndexHOLtm{unique_id} 79 80 Use boolean flags to determine the default 81 \setboolean{holIndexLongTermFlag}{true} 82 \setboolean{holIndexLongTypeFlag}{true} 83 \setboolean{holIndexLongThmFlag}{false} 84 85 Add comments in the index 86 \commentHOLtm{unique_id}{comment} 87 \commentHOLty{unique_id}{comment} 88 \commentHOLthm{unique_id}{comment} 89\end{verbatim} 90% 91Definitions like these inside a latex file are tedious, 92especially for long terms. I strongly recommend using 93an external file for all these definitions. There 94is a construct 95\begin{verbatim} 96 \useHOLfile{filename} 97\end{verbatim} 98that parses files in a syntax similar to BibTex. 99Printout of \texttt{holindex-demo.hdf}: 100 101\begin{verbatim} 102@Term{term_id_4, 103 label = "a short description of term form external file", 104 force_index, 105 options = "width=20", 106 content = ``SOME_FUN = SUC a < 0 /\ 0 > SUC b`` 107} 108 109@Type{type_id_4, 110 label = "a short description of the type from external file", 111 force_index, 112 short-index, 113 content = ``:bool`` 114} 115 116 117@Thm{arithmetic.LESS_SUC_EQ_COR, 118 force-index, 119 long-index, 120 latex = "My latex code for \texttt{LESS_SUC_EQ_COR}" 121} 122 123@Thm{arithmetic.LESS_EQ_0, 124 force-index, long-index 125} 126 127@Thm{thm_1, 128 label = "(second instance)", 129 content = "arithmetic.LESS_SUC_EQ_COR", 130 options = "width=20", 131 comment = "some lengthy\\comment 132 133 with \textbf{formats} and newlines", 134 force-index, 135 long-index 136} 137 138@Theorems{ 139 ids = [arithmetic.LESS_ADD_SUC, 140 arithmetic.LESS_EQ*], 141 force-index 142} 143\end{verbatim} 144 145 146%use external file 147\useHOLfile{holindex-demo.hdf} 148 149%or define inline (recommended only for short, simple ones) 150\defHOLtm{term_id_1}{The first term}{SUC a > 0 /\ X > 2} 151\defHOLtm{term_id_2}{The second term}{SUC a < 0 /\ X > 3} 152\defHOLty{type_id_1}{The first type}{:bool} 153\defHOLty{type_id_2}{The second type}{:num} 154\formatDefHOLtm{term_width_5}{Test term width=5}{width=5}{SUC a > 0 /\ X > 2} 155\formatDefHOLtm{term_width_10}{Test term width=10}{width=10}{SUC a > 0 /\ X > 2} 156\formatDefHOLtm{term_width_50}{Test term width=50}{width=50}{SUC a > 0 /\ X > 2} 157 158 159 160\section{Printing} 161 162\begin{verbatim} 163 Print inline 164 \inlineHOLtm{id} 165 \inlineHOLty{id} 166 \inlineHOLthm{id} 167 168 Print as block 169 \blockHOLtm{id} 170 \blockHOLty{id} 171 \blockHOLthm{id} 172 173 Use def without encapsulation (seldom useful) 174 \useHOLtm{id} 175 \useHOLty{id} 176 \useHOLthm{id} 177\end{verbatim} 178 179\subsection{Block Examples} 180\begin{itemize} 181\item Example 1 \blockHOLtm{term_width_5} 182\item Example 2 \blockHOLtm{term_width_10} 183\item Example 3 \blockHOLtm{term_width_50} 184\item Example 4 \blockHOLthm{arithmetic.DIVMOD_THM} 185\end{itemize} 186 187 188\subsection{Inline Examples} 189\begin{itemize} 190\item Example 1 \inlineHOLtm{term_width_5} 191\item Example 2 \inlineHOLtm{term_width_10} 192\item Example 3 \inlineHOLtm{term_width_50} 193\item Example 4 \inlineHOLthm{arithmetic.DIVMOD_THM} 194\end{itemize} 195 196 197 198\section{Citing} 199 200\begin{verbatim} 201 Pure numbers 202 \citePureHOLtm{id} 203 \citePureHOLty{id} 204 \citePureHOLthm{id} 205 206 Single citations 207 \citeHOLtm{id} 208 \citeHOLty{id} 209 \citeHOLthm{id} 210 211 Multiple citations 212 \mciteHOLtm{id,id,...} 213 \mciteHOLty{id,id,...} 214 \mciteHOLthm{id,id,...} 215 216 Hidden citations (adds page to index, 217 but does not print anything) 218 \citeHiddenHOLtm{id} 219 \citeHiddenHOLty{id} 220 \citeHiddenHOLthm{id} 221 222 223 Printing Index 224 \printHOLIndex 225 \printShortHOLIndex 226 \printLongHOLIndex 227 228 Sort the index by occurence in the text, not by names 229 \sortHOLIndexOccurence 230\end{verbatim} 231 232Sometimes, it might be tiresome to write a lengthy theory name over and over again. 233One can easily define printing and citing commands for theorems of a specific 234theory by e.\,g.: 235\begin{verbatim} 236\newcommand{\citeMyTheorythm}[1]{\citeHOLthm{lengthyTheoryName.#1}} 237\end{verbatim} 238It is a little bit trickier to get the same effect for citation lists. There is however, 239a version of \texttt{mciteHOLthm} that accepts a theorem prefix: 240\begin{verbatim} 241\newcommand{\mciteMyTheorythm}[1]{\mciteHOLthmPrefix{lengthyTheoryName.}{#1}} 242\end{verbatim} 243 244If you are using many theorem citations it might become tricky to keep track of what you are citing. 245There is a debug flag that prints the theorem name as well as it's index number. To use it, add the following 246line to the header of your file: 247\begin{verbatim} 248\setboolean{holThmCiteDebug}{true} 249\end{verbatim} 250 251 252\section{Printing} 253There are some macros just concerned with the resulting output. 254One can adapt these easily to personal preferences. Here the standard 255definitions are printed. Just copy them to the header of your file 256and modify them to your taste: 257 258\begin{verbatim} 259The environment for printing something as a 260block and the inline command (found in holtexbasic.sty): 261\renewcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}} 262\renewenvironment{HOLblock}{\begin{alltt}}{\end{alltt}} 263 264Format of citations 265\renewcommand[\protect]{\citeHOLthm}[1]{(HOL-Thm~\citePureHOLthm{#1})} 266\renewcommand[\protect]{\citeHOLtm}[1]{(HOL-Term~\citePureHOLtm{#1})} 267\renewcommand[\protect]{\citeHOLty}[1]{(HOL-Type~\citePureHOLty{#1})} 268 269\renewcommand[\protect]{\mciteHOLthmPrefix}[2] 270 {(HOL-Thms~\foreach{\citePureHOLthmPrefix{#1}}{, }{#2})} 271\renewcommand[\protect]{\mciteHOLtm}[1] 272 {(HOL-Terms~\foreach{\citePureHOLtm}{, }{#1})} 273\renewcommand[\protect]{\mciteHOLty}[1] 274 {(HOL-Types~\foreach{\citePureHOLty}{, }{#1})} 275 276 277How theorem names are printed in the index 278\renewcommand{\HOLThmName}[1]{{\tt{}#1}} 279 280Headers in the index 281\rewenvironment{HOLTermIndex}{\section*{HOL-Term Index}}{} 282\renewenvironment{HOLTypeIndex}{\section*{HOL-Type Index}}{} 283\renewenvironment{HOLThmIndex}{\section*{HOL-Theorem Index}}{} 284\renewcommand{\HOLThmIndexTheory}[1]{\subsection*{#1Theory}} 285\end{verbatim} 286\pagebreak 287\begin{verbatim} 288Much more complicated: Index entries themselves 289% Arg 1 : number in the index 290% Arg 2 : unique ID 291% Arg 3 : Label 292% Arg 4 : Pages 293% Arg 5 : Long index? 294% Arg 6 : is the pages argument non-empty? 295% Arg 7 : comment 296% Arg 8 : latex printed version of theorem/type/term 297\renewcommand{\HOLIndexEntryFormat}[8]{% 298 \makebox[0.1\textwidth][r]{(#1)\ }%number 299 \begin{minipage}[t]{0.9\textwidth}%everything else in minibox 300 \begin{flushright}#3 \ldots$\!$\dotfill #4\end{flushright}{%first line 301 \ifthenelse{\(\not\boolean{holShortIndexFlag}\) \and %use short or 302 \(\boolean{#5} \or \boolean{holLongIndexFlag}\)}% long version 303 {#7\begin{blockHOL}#8\end{blockHOL}\medskip}%long version 304 {}% else short version 305 }%end if-then-else 306 \end{minipage}\\} 307 308 309And index entries for the theorems, types and terms using this definition 310 311% Arg 1 : unique ID 312% Arg 2 : Label 313% Arg 3 : Pages 314% Arg 4 : Long index? 315% Arg 5 : is the pages argument non-empty? 316% Arg 6 : comment 317% Arg 7 : latex printed version of theorem/type/term 318\renewcommand{\HOLThmIndexEntryFormat}[7]{% 319 \HOLIndexEntryFormat{\arabic{holThmCounter}}{thm@#1}{#2}{#3}{#4}{#5}{#6}{#7}% 320} 321\renewcommand{\HOLTypeIndexEntryFormat}[7]{% 322 \HOLIndexEntryFormat{\arabic{holTypeCounter}}{type@#1}{#2}{#3}{#4}{#5}{#6}{#7}% 323} 324\renewcommand{\HOLTermIndexEntryFormat}[7]{% 325 \HOLIndexEntryFormat{\arabic{holTermCounter}}{term@#1}{#2}{#3}{#4}{#5}{#6}{#7}% 326} 327\end{verbatim} 328 329 330 331\section{Some citing to fill the index} 332 333\citeHOLthm{arithmetic.LESS_SUC_EQ_COR} 334\citeHOLtm{term_id_1} 335\citeHOLty{type_id_2} 336 337\mciteHOLthm{arithmetic.LESS_SUC_EQ_COR,prim_rec.INV_SUC_EQ,arithmetic.LESS_SUC_EQ_COR} 338 339\pagebreak 340 341\citeHOLthm{prim_rec.INV_SUC_EQ} 342\citeHOLthm{arithmetic.PRE_SUC_EQ} 343 344\pagebreak 345 346\citeHOLthm{prim_rec.INV_SUC_EQ} 347\citeHOLthm{arithmetic.PRE_SUC_EQ} 348 349\pagebreak 350 351\citeHOLthm{prim_rec.INV_SUC_EQ} 352 353\pagebreak 354 355\citeHOLthm{prim_rec.INV_SUC_EQ} 356\citeHOLthm{arithmetic.PRE_SUC_EQ} 357\citeHOLthm{list.list_repfns} 358 359\longIndexHOLthm{arithmetic.PRE_SUC_EQ} 360\shortIndexHOLty{type_id_2} 361\commentHOLty{type_id_4}{Some short comment} 362 363%Sort index by occurence 364%\sortHOLIndexOccurence 365 366\setboolean{holIndexLongTermFlag}{false} 367 368 369\section{Long Index} 370\printLongHOLIndex 371 372\pagebreak 373\section{Index} 374\printHOLIndex 375 376\pagebreak 377\section{Short Index} 378\printShortHOLIndex 379 380 381\end{document}