unwind/Manual/description.tex

1 \chapter{The unwind Library}
4 for the HOL system~\cite{description}. The library provides conversions and
9 Most of the functions fall into one of five groups. The first group consists
12 \ml{CONJ\_FORALL} or \ml{FORALL\_CONJ}. The second group of functions are for
13 unfolding, that is expanding sub-components using their definitions. The names
14 of these begin with \ml{UNFOLD}. The functions in the third group perform
15 unwinding and have names beginning with \ml{UNWIND}. The fourth group of
17 \ml{PRUNE}. The final group of functions combine unfolding, unwinding and
20 I have tried to make the behaviour of the functions uniform. The conversions
21 apply to the smallest term possible, to provide maximum flexibility. The
32 The \ml{unwind} library can be loaded into a \HOL\ session using the function
34 manual for a general description of library loading). The first action in the
36 help\index{help!updating search path} search path. The help search path is
41 The following session shows how the \ml{unwind} library may be loaded using
135 The function \ml{EXPAND\_AUTO\_RIGHT\_RULE} can be used to unfold, unwind and
158 representation. The mutual dependencies between lines can cause a brute-force
160 which lines to unwind. The tools in the \ml{unwind} library allow the user
162 be selective. The function \ml{UNWIND\_AUTO\_CONV} attempts to analyze the
255 The problem with the approach just described is that it only unwinds fully if
367 The function also gives priority to non-internal lines when determining where
371 The algorithm used determines from the term a list of line variables. Each
372 line variable has a right-hand side of an equation associated with it. The
427 The dependency structure for the circuit is:
441 The loops for the circuit are:
478 The technique does not always yield a single recursive equation. Mutual
529 is sufficient to break all the loops. The result is three equations: an