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