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}