1\chapter{The reduce Library}
2
3This manual describes the use of the \ml{reduce} library, as well as discussing
4its design. The library is intended to ease the burden of performing tedious
5and intellectually trivial tasks of arithmetic such as proving:
6
7\begin{hol}\begin{verbatim}
8  |- 2 EXP 6 = 64
9\end{verbatim}\end{hol}
10
11\noindent Anyone trying to prove the above by hand will testify to its extreme
12tediousness. However, using the \ml{reduce} library, the evaluation of:
13
14\begin{hol}\begin{verbatim}
15  REDUCE_CONV "2 EXP 6"
16\end{verbatim}\end{hol}
17
18\noindent will perform the above automatically, and probably in far fewer
19primitive inferences than a human would take. The library will also take care
20of certain boolean expressions. This is mainly for the sake of completeness,
21since the same effect can be achieved by careful use of rewriting.
22
23
24\section{The representation of numbers}
25
26The approach to representing natural number constants in \HOL\ is to provide a
27conversion \ml{num\_CONV} which generates the definition of any nonzero numeral
28in terms of its predecessor, for example:
29
30\begin{hol}\begin{verbatim}
31   #num_CONV "1";;
32   |- 1 = SUC 0
33
34   #num_CONV "256";;
35   |- 256 = SUC 255
36\end{verbatim}\end{hol}
37
38\noindent This conversion uses \ml{mk\_thm}, so could be regarded as
39unsatisfactory; however it is arguably no worse than expanding a constant
40defined through the normal constant definition mechanism.
41
42The \ml{reduce} library uses only the above conversion, together with certain
43definitions and preproved theorems concerning the various arithmetic and
44boolean operators, to derive, strictly by inference, reduction theorems for
45certain expressions.
46
47
48\section{Sample algorithm}
49
50The following is an example of an algorithm for reducing addition expressions.
51In fact, for reasons of efficiency, the library's \ml{ADD\_CONV} conversion is
52implemented in a slightly more sophisticated way, but this example gives the
53general flavour of how the various arithmetic conversions are defined.  Suppose
54we want to apply the conversion to \ml{"m + n"} where \ml{m} and \ml{n} are
55both numerals. Then
56
57\begin{itemize}
58  \item If the first numeral is zero, we need only specialize the first
59  conjunct of the inbuilt definition \ml{ADD}:
60
61  {\small\begin{verbatim}
62    SPEC "n" (CONJUNCT1 ADD)
63  \end{verbatim}}
64
65  \item If the first numeral is not zero, then we call the conversion
66  recursively to give:
67
68  {\small\begin{verbatim}
69    |- p + n = s
70  \end{verbatim}}
71
72  where \ml{p} is the predecessor of \ml{m}, and \ml{s} the corresponding sum.
73  Now we can apply the following inferences:
74
75  {\small\begin{verbatim}
76    |- p + n = s                % [1] From recursive call             %
77    |- (SUC p) + n = SUC(p + n) % [2] Instance of 2nd conjunct of ADD %
78    |- (SUC p) + n = SUC s      % [3] Substituting [1] in [2]         %
79    |- SUC p = m                % [4] SYM (num_CONV m)                %
80    |- SUC s = t                % [5] SYM (num_CONV (s+1))            %
81    |- m + n = t                % [6] Substituting [4] and [5] in [6] %
82  \end{verbatim}}
83
84  This gives the desired result. The above can easily be converted into a
85  simple recursive procedure.
86
87\end{itemize}
88
89\section{Using the library}
90
91The straightforward way to use the library is simply to do:
92
93\begin{hol}\begin{verbatim}
94   load_library `reduce`;;
95\end{verbatim}\end{hol}
96
97\noindent This will work only if the \HOL\/ being used has been installed
98correctly; if this is not the case the user should refer to the \TUTORIAL\/ or
99the \DESCRIPTION.
100
101The library provides the following three ML bindings, which should be all that
102is needed for most purposes:
103
104\begin{itemize}
105
106  \item \ml{REDUCE\_CONV} is a conversion which, when given an expression, will
107  return a theorem expressing its equivalence with a reduced version, which in
108  many cases will be simply a single numeral or boolean literal. For example:
109
110  {\small\begin{verbatim}
111    #REDUCE_CONV "(50 < 51) => (2 * 25) | (60 - 17)";;
112    |- (50 < 51 => 2 * 25 | 60 - 17) = 50
113
114    #REDUCE_CONV "(3 * x) + (1 + 2)";;
115    |- (3 * x) + (1 + 2) = (3 * x) + 3
116
117    #REDUCE_CONV "(1 < 2) /\ (2 <= 2)";;
118    |- 1 < 2 /\ 2 <= 2 = T
119  \end{verbatim}}
120
121  \item \ml{REDUCE\_RULE} is a rule which applies the reductions corresponding
122  to \ml{REDUCE\_CONV} to subterms of the theorem's conclusion
123
124  \item \ml{REDUCE\_TAC} performs the same reductions on a goal.
125
126\end{itemize}
127
128\noindent For more sophisticated use, there are conversions specific to each
129operator, for example \ml{ADD\_CONV} and \ml{OR\_CONV}. For more details of
130these, refer to the next chapter. The arithmetic conversions and boolean
131conversions may be loaded separately by loading (with \ml{loadt} for instance)
132\ml{arithconv.ml} and \ml{boolconv.ml} respectively, in the main library
133directory.
134