ch05.tex

\chapter{Binary Numerals}
\label{ch:binary-numerals}
\section{Numbers and Numerals}
\label{sec:numbers-numerals}
Numbers are mathematical objects with certain properties,
and they come with operators, such as addition
and multiplication, that produce new numbers from numeric
operands.
Because numbers are mathematical objects, they are ephemeral.
You can't really get your hands on them.
They are figments of the imagination.

However, numbers are useful, and to use them
we need to be able to write them down.
Decimal numerals are one way to do this.
The \index{numeral!decimal}numeral 144 stands for the number
of eggs in a dozen cartons of eggs.
The numeral 1215 stands for the number of
years between the twenty-seventh year of the reign
of Caesar Augustus and the signing of the Magna Carta.

However, ``144'' and ``1215'' are \index{numeral!vs number}numerals.
They are not numbers. They are symbols that stand for numbers,
and they are not the only symbols in use for that purpose.
The symbols CXLIV and MCCXV (Roman \index{numeral!Roman}numerals) stand for the same two numbers.
So do the symbols $90_{16}$ and $4BF_{16}$ (hexadecimal \index{numeral!hexadecimal}numerals),
but most people use decimal numerals like 144 and 1215 when they do arithmetic.

The decimal representation is so embedded in
our experience and practice that we often conflate
numerals and numbers. Some dictionaries treat the terms as synonyms.
Usually there is no harm in considering numbers and numerals
to be the same thing, but we are going to use numerals
to do arithmetic in a mechanized way, so we will
do well to distinguish between
\index{number!vs numeral}numbers (mathematical objects)
and \index{numeral!vs number}numerals (symbols for numbers).

Let's think about how we interpret a decimal numeral as a number.
Consider the \index{numeral!decimal}numeral 1215, for example.
Each digit in the numeral has a different interpretation.
The first digit is the number of thousands in the number
that 1215 stands for. The second tells us the number
of hundreds, then the tens, and finally the units.
The following formula is a way to express this interpretation:
\begin{center}
$\textbf{1} \times 10^3 + \textbf{2} \times 10^2 + \textbf{1} \times 10^1 + \textbf{5} \times 10^0$
\end{center}

This formula computes a number from the individual digits
in the numeral using standard arithmetic operations
(addition, multiplication, and exponentiation).
It shows us what the individual digits in the numeral stand for,
and it gives us a leg up on figuring out other kinds of numerals.
The digits in the hexadecimal numeral have a similar meaning
but with a different base. Decimal numerals are based on
powers of ten and hexadecimal numerals are based on powers of sixteen.

\begin{aside}{aside-digits-as-numbers}{Digits as Numbers}
Perhaps you noticed a subtle confusion in the formulas we use
to explain the meaning of numerals. At first, we claim that
1215 is merely a \index{symbol, for number}symbol standing for a mathematical object.
And we claim that the digit 2 is merely a symbol standing
for the number of items in a pair, along with similar
claims for the digits 1 and 5.
Then, we use those symbols in the formula
$1 \times 10^3 + 2 \times 10^2 + 1 \times 10^1 + 5 \times 10^0$
as if they were numbers.

There is some sleight of hand going on here.
Numbers as mathematical objects are figments of our imagination,
but when we write formulas, we have to choose some symbols to
represent them.
So, in the formula $1 \times 10^3 + 2 \times 10^2 + 1 \times 10^1 + 5 \times 10^0$,
we use the symbols 1, 10, 3, 2, 5, and 0 as if they were numbers.
But, in the numeral 1215, the symbols 1, 2, and 5 are not numbers.
They are symbols standing for numbers.

It's even worse with the hexadecimal numeral $4BF_{16}$
and the formula $4 \times 16^2 + 11 \times 16^1 + 15 \times 16^0$.
In the formula, we have rewritten the symbol B
as the hexadecimal numeral for 11
and the symbol F as the hexadecimal numeral for 15.
And we've had the temerity to pretend that symbols
in the formula are numbers when they are really hexadecimal numerals,
as they were in the formula for the meaning of the decimal numeral 1215.

Furthermore, we've really mixed things up in the numeral
$4BF_{16}$ because the ``4BF'' part is in hexadecimal notation
and the ``16'' part is a decimal numeral, indicating that we are
to interpret the digits in base sixteen rather than base ten.
Try to get your head around this.
We're more or less stuck with it. Figments of our imagination have
to be materialized somehow if we are going to talk about
them.\index{digit}
%\caption{Digits as Numbers}
%\label{aside-digits-as-numbers}
\end{aside}

The system of decimal numerals calls on ten different symbols to represent digits:
0, 1, 2, \dots 9.
The hexadecimal system requires sixteen different symbols, conventionally
0, 1, 2, \dots 9, A, B, C, D, E, F.
The digits stand for the customary numbers
(0 for zero, 1 for one, 2 for two, and so on)
and the letters A through F
stand for the numbers ten through fifteen.\footnote{There
are no conventional squiggles for digits beyond fifteen,
presumably because no numeral system
with a base exceeding sixteen is in common use.
A few thousand years ago, the Mayan civilization used a base twenty system
with twenty different symbols for digits.
The ancient Sumerians used a system with base sixty
but with special arrangements to deal with the lack of a symbol for zero.}
That leads to the following
formula to express the meaning of the hexadecimal numeral $4BF_{16}$.
(Remember, B stands for eleven, F for fifteen.)
\begin{center}
$\textbf{4} \times 16^2 + \textbf{11} \times 16^1 + \textbf{15} \times 16^0$
\end{center}
Formulas like this
convert numerals to numbers.
No doubt you could construct the appropriate formula
for any given numeral: decimal, hexadecimal, or any other base.

We'll say more about converting numerals to numbers later,
but what about going the other direction, converting
numbers to numerals?
Suppose someone gives you an operator called \textsf{dgts} that
converts a number to a decimal numeral.
Let's say that \textsf{(dgts 1215)} would deliver the list \textsf{[5 1 2 1]}.
That is, \textsf{dgts} delivers a list of the decimal digits
of its operand,
\index{representation!decimal numeral}
starting with the ones digit (a 5 in this case),
then the tens digit, and so on, reading right to left from
the customary way of writing the numeral.
If you had a definition of \textsf{dgts},
you might test it on a few numbers to see if it does what you expect.
\begin{code}
\begin{verbatim}
(check-expect (dgts 1215) (list 5 1 2 1))
(check-expect (dgts 1964) (list 4 6 9 1))
(check-expect (dgts 12345) (list 5 4 3 2 1))
(check-expect (dgts 0) nil)
\end{verbatim}
\end{code}

\begin{aside}{numeral-as-sequence}{Numerals as Lists \dots Backwards}
\emph{What! The \textsf{dgts} operator delivers the digits backwards! Why is that?}

Of course
\seeonlyindex{dgts}{operator}\index{operator, by name!dgts (digits from number)}\textsf{dgts}
could have delivered the digits in the
customary order, but reverse order simplifies some of the
equations we will use to interpret numerals.
We will write numerals like 1215 in the usual way, but
the \textsf{dgts} operator delivers them in the form of
a list with the digits in reverse order: \textsf{[5 1 2 1]}.

Besides being backwards,\index{representation!decimal numeral}
the elements in the list are numbers,
not symbolic digits.
We could use pure symbols, but we indulge in
this sleight of hand to
simplify parts of the discussion.
In a similar vein, the list notation \textsf{[5 1 2 1]} is the symbol we use
to describe the
\index{list!for numeral}\index{numeral!list for}\index{sequence!for numeral}\index{numeral!sequence for}list,
but the list itself is a mathematical object.
It's another figment of our imagination,
ephemeral in the same sense as a number.
%\caption{Numerals as Lists \dots Backwards}
%\label{numeral-as-sequence}
\end{aside}

Wait a minute!
Why does \textsf{(dgts 0)} deliver the empty list
instead of the one-element list \textsf{[0]}?
That's another little trick.
Besides delivering the digits in reverse order,
\index{representation!decimal numeral}
\index{leading zero}\index{numeral!leading zero}leading zeros are omitted.
We could write the numeral 1964 with as many leading zeros as we like.
The numerals 1964, 01964, and 000001964 all stand for the same number.
Those numerals correspond to
\textsf{[4 6 9 1]}, \textsf{[4 6 9 1 0]}, and \textsf{[4 6 9 1 0 0 0 0 0]}
in our list format. ``Leading zeros'' come at the end when the
digits are in reverse order.

However, \textsf{dgts} doesn't include any
 \index{leading zero}\index{numeral!leading zero}leading zeros
in the numerals it delivers.
It leaves them all off, even for the number zero.
That's why \textsf{(dgts 0)} is \textsf{nil}.
The numeral \textsf{(dgts 012345)} is
the same as the numeral \textsf{(dgts 12345)} too
because \textsf{dgts} interprets its operand as a number.
Since 012345 and 12345 stand for the same number,
the formula \textsf{(dgts 012345)} and the formula \textsf{(dgts 12345)}
both deliver the list \textsf{[5 4 3 2 1]}.
No leading zeros.

The computer interprets the
decimal numeral 012345 in the formula \textsf{(dgts 012345)}
as a mathematical object.
How does the computer represent the object? None of your business.
That's the computer's business.
It has its own way of dealing with numbers.
Later, we'll study the way most computers do this,
but for now we will assume that the computer has some way of turning
numerals into whatever form it uses to represent numbers.

After running a few sanity checks on the \textsf{dgts} operator,
you might want to do some serious testing.
Big batches of automated tests using random data, perhaps.
Coming up with automated tests calls for some thought.
Let's start small. How about the units digit in a decimal numeral?
What mathematical formula would deliver the units digit in a
decimal numeral given an arbitrary positive integer $n$?

The units digit in a decimal numeral is the remainder when you divide
the number by ten. The formula that converts a numeral to a number
makes that clear.
\begin{center}
$1 \times 10^3 + 2 \times 10^2 + 1 \times 10^1 + 5 \times 10^0$
\end{center}

Each of the terms in the formula is a product of a power
of ten with another number. A power of ten is, of course,
a multiple of ten, so none of those terms contribute to the remainder
when dividing by ten. None of them, that is, except the units digit.
It does not have a factor of ten in it because
$10^0$ is one, which is not a multiple of ten.
So, to get the units digit in the numeral,
compute the remainder in the division of the number by ten.

\begin{aside}{third-grade-division}{\textsf{mod} and \textsf{floor}: Think Third-Grade Division}
Transport yourself back to the third grade,
or whenever you learned long division.
There were four parts to the problem, and they all had names.

\begin{tabular}{ll}
\emph{divisor}   & number you divide by \\
\emph{dividend}  & number you divide by the divisor \\
\emph{quotient}  & what you get when you do the division \\
\emph{remainder} & what's left over to make up the difference
\end{tabular}
\begin{center}
\begin{tabular}{ll}
$q$ $=$ \textsf{(floor $n$ $d$)} & \emph{quotient}  \\
$r$ $=$ \textsf{(mod $n$ $d$)}   & \emph{remainder} \\
$n = qd + r$            & \{\emph{check}$\div$\} \\
\end{tabular}
\end{center}\index{division!third grade}\index{division!long division}\index{division!floor (round down)}
\seeonlyindex{long division}{division}\index{modular arithmetic}\index{operator, by name!floor (divide, round down)}
\seeonlyindex{mod}{operator}\index{operator, by name!mod (remainder)}
\index{arithmetic!clock}\index{clock arithmetic}\index{arithmetic!modular}\index{division!mod (remainder)}
%\caption{\textsf{mod} and \textsf{floor}: Think Third-Grade Division}
%\label{third-grade-division}
\end{aside}

The remainder is
what the \textsf{mod} operator delivers
(box~\ref{third-grade-division}). %, page \pageref{third-grade-division}).
The following test uses \textsf{mod} to make sure the units digit in the numeral
that the \textsf{dgts} operator delivers for the number $n$ is correct.
\begin{code}
\begin{verbatim}
(= (first (dgts n)) (mod n 10))
\end{verbatim}
\end{code}

Since \textsf{dgts} delivers the digits backwards,
\textsf{(first (dgts $n$))}, the first digit in the list,
is the units digit in the numeral, which is the last digit
when the numeral is written in the conventional format.
The formula checks to make sure that
the units digit of the numeral that
\textsf{dgts} delivers is \textsf{(mod $n$ 10)},
the remainder when dividing $n$ by 10.

We can use the DoubleCheck facility of Proof Pad to run this test on a batch of random numbers.
We need to be careful not to allow zero to pop up in the testing
because \textsf{(dgts 0)} is nil, so there is no first digit to check.
Besides, we've already completed the testing of \textsf{(dgts 0)} in our sanity checks.
We can avoid retesting zero by adding one to a random natural number.
That produces a random, nonzero, positive integer.
\index{definition!property}\index{data, random test}\index{random data}\index{defproperty}
\begin{code}
\begin{verbatim}
(defproperty dgts-last-digit-tst
  (n-1  :value (random-natural))
  (let* ((n (+ n-1 1))) ; avoid n=0
    (= (first (dgts n))
       (mod n 10))))
\end{verbatim}
\end{code}

That takes care of testing the units digit, but what about the others?
We can do something about those by observing that the quotient
when $n$ is divided by ten
is a number with the same digits as $n$
except that the units digit is missing.
Remember, we're doing third-grade arithmetic here.
The quotient is the main result of the division.
No fraction, no decimal point, no remainder. Just the whole-number quotient.
Since we've already tested to make sure the units digit is correct,
we don't need to worry about that.
We only need to worry about the other digits.
The intrinsic operator \textsf{floor}
(box~\ref{third-grade-division}, page \pageref{third-grade-division})
produces the quotient, discarding the remainder.
We can get those other digits by applying \textsf{dgts} to
the operand \textsf{(floor $n$ $10$)}.

The following formula implements the test we have in mind.
It checks to make sure the digits other than the units digit
in the list that \textsf{(dgts $n$)} delivers
are the same as the digits in the list that
\textsf{dgts} delivers when its operand is the quotient in
the division $(n \div 10)$.
\begin{code}
\begin{verbatim}
(equal (rest (dgts n))      ; all digits except the units digit
       (dgts (floor n 10))) ; digits of the quotient
\end{verbatim}
\end{code}

As with the test of the units digit,
we can run a batch of tests based on
our rest-of-the-digits observation by defining a DoubleCheck property.

\index{definition!property}\index{data, random test}\index{random data}\index{defproperty}observation.
\begin{code}
\begin{verbatim}
(defproperty dgts-other-digits-tst
  (n-1  :value (random-natural))
  (let* ((n (+ n-1 1)))          ; avoid n=0
    (equal (rest (dgts n))
           (dgts (floor n 10)))))
\end{verbatim}
\end{code}

It would be nice to run these tests, but
\textsf{dgts} is not an intrinsic operator.
We have to provide a definition for it.
To do that we use the \textsf{defun} command,
which is similar to \textsf{defproperty}
but without any value specifications.

The definition of the \textsf{dgts} operator will be inductive, will
use some ideas we discussed in putting together tests,
and will conform to the requirements of the
\index{three C's}\index{definition!inductive (circular)}three C's
(figure~\ref{fig:inductive-def-keys}, page \pageref{fig:inductive-def-keys}),
repeated here and customized for \textsf{dgts}.
%\begin{samepage}
\begin{center}
\begin{tabular}{lp{3.5in}}
\emph{Complete}      & Two cases: the number is zero or it isn't. So, two formulas.\\
\emph{Consistent}    & The cases do not overlap---no chance for inconsistency.\\
\emph{Computational} & Inductive case ($n > 0$): operand is
                       divided by ten, making it closer to zero
                       (the noninductive case).
\end{tabular}
\end{center}
%\end{samepage}

\label{dgts-defun}\index{operator, by name!dgts (digits from number)}\index{numeral!from number}\index{representation!decimal numeral}\index{axiom, by name!\{dgts0\}, \{dgts1\}}\index{equation, by name!\{dgts0\}, \{dgts1\}}
\begin{code}
\begin{verbatim}
(defun dgts (n)
  (if (zp n)
      nil                                     ; {dgts0}
      (cons (mod n 10) (dgts (floor n 10))))) ; {dgts1}
\end{verbatim}
\end{code}

This definition uses the predicate \textsf{zp}
(box~\ref{zp-def}, page \pageref{zp-def})
to detect the value zero within the domain of natural numbers.
If you put the definition of \textsf{dgts} at the beginning of a program,
import the ``testing'' and ``DoubleCheck'' facilities
(\textsf{include-book},
chapter~\ref{ch:software-testing-prefix-notation}, pages \pageref{testing-include}--\pageref{dblchk-include}),
and import some theorems about modular arithmetic
(box~\ref{admit-def}), %, page \pageref{admit-def}),
you can enter the tests and run them using Proof Pad.
You can also enter formulas in the command panel to compute
decimal numerals for any natural numbers you choose.

\begin{aside}{admit-def}{Termination, ACL2 Admit, and \textsf{floor}/\textsf{mod} Equations}
ACL2 will not accept the definition of
an operator unless
it can prove that the operator always delivers a value in
a finite number of computation steps.
Nonterminating operators complicate the reasoning process.
Proving that \textsf{dgts} terminates
requires applying some theorems of modular arithmetic.
Fortunately, experts have put together some theorems on that topic,
and the following \textsf{include-book} directive will import them
to make it possible for the mechanized logic to prove termination
and admit the \textsf{dgts} operator to the ACL2 logic.\\
\hspace*{5mm}\textsf{(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)}\label{floor-mod-book}\index{ACL2!admit}\index{admit, ACL2}\index{book!arithmetic-3/floor-mod}\label{floor-mod-include-book}\index{directory (:dir)!:system}\index{book!directory (:dir)}\index{directive!include-book}\index{directory (:dir)!:system}\index{system, :dir}\index{theorem!algebra, ACL2}
%\caption{Termination, ACL2 Admit, and floor/mod Equations}
%\label{admit-def}
\end{aside}

\begin{exercises}
\exer {Let $y$ stand for the number of years
between the signing of the Magna Carta and
the signing of the United States Declaration of Independence.
Find the numeral for $y$ and use \textsf{dgts} (page \pageref{dgts-defun})
to verify that you got it right.}

\exer {\label{modular-division}Prove theorem \{\emph{mod-div}\}:
\textsf{(mod ($*$ $a$ $x$) ($*$ $a$ $b$))} $=$ \textsf{($*$ $a$ (mod $x$ $b$))} \\
\emph{Hint}: \index{theorem, by name!\{mod-div\}}
\index{division!floor, mod}You won't need induction,
but the following facts will help.
Suppose $x$ is the dividend and $d$ the divisor
in a third-grade division problem
(box~\ref{third-grade-division}, page \pageref{third-grade-division}).
Then, $r$ $=$ \textsf{(mod $x$ $d$)} is the remainder
and $q$ $=$ \textsf{(floor $x$ $d$)} is the quotient.
Third-graders use the equation $(qd + r) = x$
to make sure they have done the division correctly.
They also know that $0 \le r < d$:
\textsf{(mod $x$ $d$)} is the number $r$
in the range $0 \le r < d$ such that $qd + r = x$.}

\exer {\label{mod-div-defthm}\index{division!floor, mod}Define
the \{\emph{mod-div}\} theorem
in ACL2 notation, and use ACL2 to verify that it is a theorem.
Since the theorem does not hold for all numbers $a$, $b$, and $x$,
you will need to ask ACL2 to prove an implication with
hypotheses that constrain the theorem to the domain in which it is true.
If you state it correctly and import the
theorems about modular arithmetic contained in the floor-mod book
(box~\ref{admit-def}, page \pageref{admit-def}),
ACL2 will succeed.\\
\emph{Hint}: \textsf{(posp $n$)} is true if $n$ is a nonzero natural number and false otherwise.}
\end{exercises}

\section{Numbers from Numerals}
\label{sec:numbers-from-numerals}
The \textsf{dgts} operator (page \pageref{dgts-defun})
provides a way to compute a decimal
numeral given a number. How about going in the other direction?
Given a decimal numeral, compute the corresponding number.
You already know the formula.
\begin{samepage}
\begin{center}
\begin{tabular}{rrr}
$1 \times 10^3 + 2 \times 10^2 + 1 \times 10^1 + 5 \times 10^0$ &$=$ & 1215 \\
$1 \times 10^2 + 4 \times 10^1 + 4 \times 10^0$                 &$=$ &  144 \\
\end{tabular}
\end{center}
\end{samepage}

What properties would an operator
converting decimal numerals to numbers have?
Let's assume that numerals are represented
in the manner of the \textsf{dgts} operator:
units digit first,
then the tens digit, then hundreds, and so on.
We want to define an operator, \textsf{nmb10},
that converts decimal numerals in that form to numbers.
We know that \textsf{(nmb10 nil)} must be zero
because \textsf{(dgts 0)} $=$ \textsf{nil},
and we are trying to convert numerals produced by \textsf{dgts}
back to the numbers they came from.
How about a one-digit numeral \textsf{[$x_0$]}?
The equation in that case would be \textsf{(nmb10 [$x_0$])} $=$ $x_0$.
If there are two or more digits,
\textsf{[$x_0$ $x_1$ \dots $x_{n+1}$]},
then the equation would take the following form:\\
\hspace*{1cm}
\textsf{(nmb10 [$x_0$ $x_1$ $x_2$ \dots $x_{n+1}$])} $=$
$x_0 + x_1 \times 10^1 + x_2 \times 10^2 + \dots x_{n+1} \times 10^{n+1}$ \hfill \{\emph{a}\}\\

\vspace{-1mm}  %%% FRAGILE FRAGILE FRAGILE
All of the terms in the sum
include a factor of ten except the first term,
so we can factor ten out of those terms.
Factoring the formula in this way produces a new equation.\\
\hspace*{1cm}
\textsf{(nmb10 [$x_0$ $x_1$ $x_2$ \dots $x_{n+1}$])} $=$
$x_0 + 10 \times (x_1 \times 10^0 + x_2 \times 10^1 + \dots x_{n+1} \times 10^n)$ \hfill \{\emph{b}\}\\

\vspace{-1mm}   %%% FRAGILE FRAGILE FRAGILE
The list \textsf{[$x_1$ $x_2$ \dots $x_{n+1}$]} is also a decimal numeral,
albeit for a different number.
The number it denotes is
$(x_1 \times 10^0 + x_2 \times 10^1 + \dots x_{n+1} \times 10^n)$,
which is the value \textsf{nmb10} should deliver given the numeral \textsf{[$x_1$ $x_2$ \dots $x_{n+1}$]}.\\
\hspace*{1cm}
\textsf{(nmb10 [$x_1$ $x_2$ \dots $x_{n+1}$])} $=$ $x_1 + x_2 \times 10^1 + \dots x_{n+1} \times 10^n$ \hfill \{\emph{c}\}\\

\vspace{-1mm}   %%% FRAGILE FRAGILE FRAGILE
Observe that the right-hand side of equation \{\emph{c}\}
is equal
to the part of the formula in equation \{\emph{b}\} that is multiplied by ten.
Therefore, we can rewrite equation \{\emph{b}\} as follows:\\
\hspace*{1cm}
\textsf{(nmb10 [$x_0$ $x_1$ $x_2$ \dots $x_{n+1}$])} $=$
$x_0 + 10$ $\times$ \textsf{(nmb10 [$x_1$ $x_2$ \dots $x_{n+1}$])} \hfill \{\emph{d}\}\\

\vspace{-1mm}   %%% FRAGILE FRAGILE FRAGILE
Equation \{\emph{d}\} is an inductive equation that delivers the right value for
numerals with two or more digits. It also works
for one-digit numerals because (nmb10 nil) is zero.\\
\hspace*{1cm}
\textsf{(nmb10 [$x_0$])} $=$ $x_0 + 10$ $\times$ \textsf{(nmb10 nil)} $=$ $(x_0 + 10 \times 0) = x_0$ \hfill \{\emph{d}$*$\}\\

Together, equation \{\emph{d}\} for numerals with one or more digits
and the equation for empty numerals, \textsf{(nmb10 nil)} $=$ $0$, conform to the
rule of the three C's (page \pageref{fig:inductive-def-keys}),
so we have the makings of an inductive definition of \textsf{nmb10}.
The following equations summarize our analysis and show how
the \textsf{first} and \textsf{rest} operators
(page \pageref{first-rest-cons})
extract the required digits from the numeral.
From that point, constructing the ACL2 definition
is a straightforward translation of the equations to prefix notation.
\vspace{2mm}   %%% FRAGILE FRAGILE FRAGILE
\begin{center}\seeonlyindex{nmb10}{operator}\index{number!from numeral}\index{axiom, by name!\{n10.0\}, \{n10.1\}}\index{equation, by name!\{n10.0\}, \{n10.1\}}
\addtolength{\tabcolsep}{-3pt}
\begin{tabular}{rlll}
\textsf{(nmb10 [$x_0$ $x_1$ $x_2$ $\dots$ $x_{n+1}$])} & $=$ &$x_0 + 10$ $\times$ \textsf{(nmb10 [$x_1$ $x_2$ \dots $x_{n+1}$])} &\{n10.1\} (below)\\
\textsf{(nmb10 nil)}                           & $=$ &$0$   &\{n10.0\} (below)\\
$x_0$                         & $=$ &\textsf{(first [$x_0$ $x_1$ $\dots$ $x_n$])} &\{\emph{cons}\} (page \pageref{first-rest-cons})\\
\textsf{{[$x_1$ $\dots$ $x_n$]}}       & $=$ &\textsf{(rest  [$x_0$ $x_1$ $\dots$ $x_n$])} &\{\emph{rest}\} (page \pageref{first-rest-cons})\\ % mysterious error without curly braces {[ ... ]}, something to do with an optional parameter after
\end{tabular}
\addtolength{\tabcolsep}{3pt}
\end{center}\label{nmb10-defun}\index{operator, by name!nmb10 (number from digits)}
\vspace{-2mm}   %%% FRAGILE FRAGILE FRAGILE
\begin{code}
\begin{verbatim}
(defun nmb10 (xs)
  (if (consp xs)
      (+ (first xs) (* 10 (nmb10 (rest xs)))) ; {n10.1}
      0))                                     ; {n10.0}
\end{verbatim}
\end{code}

\vspace{-2mm}   %%% FRAGILE FRAGILE FRAGILE
We have derived this definition carefully
from things we know about numbers,
and we can use logic to be sure we got it right.
We want to prove that
\textsf{(nmb10 [$x_0$ $x_1$ \dots $x_{n}$])}
delivers the same number as the formula
$(x_0 + x_1 \times 10^1 + x_2 \times 10^2 + \dots x_{n} \times 10^{n})$.
\begin{center}
\label{horner10-thm}\index{theorem!Horner}\index{theorem, by name!\{horner 3\}@\{Horner 10\}}Theorem
\{\emph{Horner 10}\}:
\textsf{(nmb10 [$x_0$ $x_1$ \dots $x_{n}$])} $=$
$x_0 + x_1 \times 10^1 + x_2 \times 10^2 +$ $\dots$ $x_{n} \times 10^{n}$
\end{center}
\vspace{2mm}

The theorem asserts that the operator \textsf{nmb10}
computes a sum of multiples of successive powers of ten.
The multipliers
(known as \index{coefficient, polynomial}polynomial coefficients)
of the powers of ten are the digits in a decimal numeral.
We call the theorem \emph{Horner 10} because
the scheme that the operator \textsf{nmb10} uses to carry out the computation is
known as \index{Horner's rule}Horner's rule.
Proving theorem \{\emph{Horner 10}\} amounts to
verifying that $(\forall n.H(n))$ is true,
where the predicate $H$ is defined for each natural number $n$
as follows:
\begin{center}
$H(n)$ $\equiv$ $($\textsf{(nmb10 [$x_0$ $x_1$ \dots $x_{n}$])} $=$
$x_0 + x_1 \times 10^1 + x_2 \times 10^2 +$ $\dots$ $x_{n} \times 10^{n})$
\end{center}

Figures \ref{fig:horner10-base} (base case) and \ref{fig:horner10-induc}
(inductive case) provide a proof by induction of theorem \{\emph{Horner 10}\}.
As usual, the inductive case, $\forall n. (H(n) \rightarrow H(n+1))$,
derives $H(n+1)$ from the induction hypothesis $H(n)$ and other known
equations.
We conclude that $\forall n.H(n)$ is true,
citing mathematical induction
(figure~\ref{induction-rule}, page \pageref{induction-rule}).

\begin{figure}
\begin{center}
\begin{tabular}{rll}
&$H(0) \equiv ($\textsf{(nmb10 [$x_0$])} $=$ $x_0)$&\\
\hline
    & \textsf{(nmb10 [$x_0$])}           & \\
$=$ & \textsf{(nmb10 (cons $x_0$ nil))}  & \{\emph{cons}\} (page \pageref{first-rest-cons}) \\
$=$ & \textsf{(+ (first (cons $x_0$ nil))}  & \{n10.1\} (page \pageref{nmb10-defun}) \\
    & \phantom{\textsf{(+ }}\textsf{($*$ 10 (nmb10 (rest (cons $x_0$ nil)))))} &\\
$=$ & \textsf{(+ $x_0$ ($*$ 10 (nmb10 (rest (cons $x_0$ nil)))))}  & \{\emph{first}\} (page \pageref{first-rest-cons}) \\
$=$ & \textsf{(+ $x_0$ ($*$ 10 (nmb10 nil)))}  & \{\emph{rest}\} (page \pageref{first-rest-cons}) \\
$=$ & \textsf{(+ $x_0$ ($*$ 10 0))}  & \{n10.0\} (page \pageref{nmb10-defun}) \\
$=$ & $x_0$  & \{\emph{algebra}\} \\
\end{tabular}
\end{center}
\caption{\{\emph{Horner 10}\}: proof of base case.}
\label{fig:horner10-base}
\end{figure}

\begin{figure}
\begin{center}
\begin{tabular}{rlll}
&\multicolumn{3}{l}{$H(n+1) \equiv ($\textsf{(nmb10 [$x_0$ $x_1$ \dots $x_{n+1}$])} $=$
$x_0 + x_1 \times 10^1 +$  $\dots$ $x_{n+1} \times 10^{n+1})$}\\
\hline
    & \textsf{(nmb10 [$x_0$ $x_1$ $\dots$ $x_{n+1}$])}           & &\\
$=$ & \textsf{(nmb10 (cons $x_0$ [$x_1$ $\dots$ $x_{n+1}$]))}    & \{\emph{cons}\}&\\
$=$ & \textsf{(+ (first (cons $x_0$ [$x_1$ $\dots$ $x_{n+1}$]))}  & \{n10.1\} &\\
    & \phantom{\textsf{(+ }}\textsf{($*$ 10 (nmb10 (rest (cons $x_0$ [$x_1$ $\dots$ $x_{n+1}$])))))} &&\\
$=$ & \textsf{(+ $x_0$ ($*$ 10 (nmb10 (rest (cons $x_0$ [$x_1$ $\dots$ $x_{n+1}$])))))}      & \{\emph{first}\} &\\
$=$ & \textsf{(+ $x_0$ ($*$ 10 (nmb10 [$x_1$ $\dots$ $x_{n+1}$])))}                          & \{\emph{rest}\}&\\
$=$ & \textsf{(+ $x_0$ ($*$ 10 $(x_1 + x_2 \times 10^1 + \dots$ $x_{n+1} \times 10^{n})))$}  & \{$H(n)$\}&\\
$=$ & $x_0 + x_1 \times 10^1 + x_2 \times 10^2 + \dots$ $x_{n+1} \times 10^{n+1}$   & \{\emph{algebra}\} &\\
\end{tabular}
\end{center}
\caption{\{\emph{Horner 10}\}: proof of inductive case.}
\label{fig:horner10-induc}
\end{figure}

Theorem \{\emph{Horner 10}\} confirms that \textsf{nmb10} delivers the
number that its operand, which is a base 10 numeral, denotes.
We also expect the inverse to be true.
That is, we expect the formula \textsf{(dgts $n$)}
to deliver the base 10 numeral for the natural number $n$
as stated in the following theorem:
\label{dgts-ok}\index{theorem, by name!\{dgts-ok\}}\index{number!from digits}
\vspace{2mm}\\
%\begin{center}
\hspace*{5mm}Theorem \{\emph{dgts-ok}\}:
$\forall n.($\textsf{(nmb10 (dgts $n$))} $=$ $n)$
\vspace{1cm}
%\end{center}

Define $D(n) \equiv ($\textsf{(nmb10 (dgts $n$))} $=$ $n)$.
We want to prove that $(\forall n.D(n))$ is true.
The universe of discourse
of the predicate $D$ is the natural numbers,
so a proof of $D(0)$
together with a proof of
$(\forall n.(D(n) \rightarrow D(n+1)))$
leads by natural deduction to the desired conclusion.
Both of the required proofs appear in
figure~\ref{fig:horner10-inverse}.

\begin{figure}
\begin{center}
\begin{tabular}{rll}
&\multicolumn{2}{l}{Base Case: $D(0) \equiv ($\textsf{(nmb10 (dgts $0$))} $=$ $0)$}\\
    \hline
    & \textsf{(nmb10 (dgts $0$))} & \\
$=$ & \textsf{(nmb10 nil)}        & \{dgts0\} (page \pageref{dgts-defun}) \\
$=$ & \textsf{0}                  & \{n10.0\} (page \pageref{nmb10-defun}) \\
\end{tabular}
\end{center}
\begin{center}
\addtolength{\tabcolsep}{-2pt}
\begin{tabular}{rll}
&Inductive Case: $D(n+1) \equiv ($\textsf{(nmb10 (dgts $(n+1)$))} $=$ $(n + 1))$&\\
    \hline
    & \textsf{(nmb10 (dgts $(n+1)$))}           & \\
$=$ & \textsf{(nmb10 (cons (mod $(n+1)$ 10) (dgts (floor $(n+1)$ 10)))}  & \{dgts1\} (page \pageref{dgts-defun})\\
$=$ & \textsf{(+ (mod $(n+1)$ 10)}              & \{n10.1\} (page \pageref{nmb10-defun})\\
    & \phantom{\textsf{(+ }}\textsf{($*$ 10 (nmb10 (dgts (floor $(n+1)$ 10)))))} &\\
$=$ & \textsf{(+ (mod $(n+1)$) 10) ($*$ 10 (floor $(n+1)$ 10)))}  & \{$D$(floor $(n+1)$ 10)\} \\
$=$ & $(n+1)$  & \{\emph{check}$\div$\} (page \pageref{third-grade-division})
\end{tabular}
\addtolength{\tabcolsep}{2pt}
\end{center}
\caption{Proof by induction of theorem \{\emph{dgts-ok}\}.}
\label{fig:horner10-inverse}\index{theorem, by name!\{dgts-ok\}}
\end{figure}

If you look carefully at the proof of $D(n) \rightarrow D(n+1)$,
you may notice that it is not according to Hoyle.
In a proof by mathematical induction,
we can cite $D(n)$ to justify any step in a proof of $D(n+1)$,
but figure~\ref{fig:horner10-inverse} cites a different
proposition, $D$\textsf{(floor $(n+1)$ $10$)},
in its proof of $D(n+1)$.
However, \textsf{(floor $(n+1)$ 10)}
is strictly smaller than $(n+1)$, and
the proof relies on an inference rule
known as \emph{strong induction}.
Strong induction is equivalent to ordinary mathematical induction,
even though it looks more powerful because any or all of the
propositions $D(0)$, $D(1)$, \dots $D(n)$ can be cited in the proof of $D(n+1)$.
Ordinary mathematical induction allows citing $D(n)$, but not the other
propositions.
Nevertheless, it is possible to verify
that if the rule of ordinary mathematical induction
is a valid rule of inference, then so is strong induction, and vice versa.
The proof is not difficult, but it's a distraction,
so we will present a rationale and leave it at that.

\label{strong-induction-rationale}The \index{induction!rationale}rationale for
\index{induction!proof by}\index{proof!by induction}\index{strong induction}\index{induction!strong}strong induction is similar to
the rationale for ordinary mathematical induction (page \pageref{induction-rationale}).
Suppose you are proving the propositions
$P(0)$, $P(1)$, $P(2)$, \dots and so on,
one by one, in sequence.
When you get to the point where you want to prove $P(n+1)$,
you will have already proven all of the propositions
with smaller indices:
$P(0)$, $P(1)$, $P(2)$, \dots $P(n)$.
So, in the proof of $P(n+1)$, you would be able to
cite any of the previous propositions, not just $P(n)$.
When you cite $P(n)$, but not propositions with smaller indices,
in the proof of $P(n+1)$, you are using ordinary mathematical induction.
When you cite one or more propositions with indices smaller than $n$,
you are using strong induction.

To put it another way, the formal statement of the strong induction rule
(figure~\ref{strong-induction-rule}) %, page \pageref{strong-induction-rule})
is different from the formal statement of ordinary induction
(figure~\ref{induction-rule}, page \pageref{induction-rule}), but
in practice strong induction encompasses the ordinary induction rule
as a special case. A proof of $P(n+1)$ that cites only $P(n)$
and not propositions in the predicate $P$ with smaller indices
could cite strong induction because $P(n)$ is one of the propositions
that the \index{hypothesis!induction}\index{induction!hypothesis}strong-induction
hypothesis, $(\forall m<n+1.P(m))$, assumes are true.
So, we may as well cite strong induction, even when we're only relying
on the ordinary induction rule.

\begin{figure}
\begin{center}
\begin{spacing}{0.9}
\begin{tabular}{l}
Prove $(\forall m<n.P(m))\rightarrow P(n)$ \\
--------------------------------------\{strong induction\}\\
Infer $(\forall n.P(n))$
\end{tabular}
\end{spacing}
\end{center}
\vspace*{-4mm}
\caption{Mathematical induction (strong induction version).}
\label{strong-induction-rule}\index{strong induction}\index{induction!strong}\index{inference rule, by name!\{strong induction\}}\index{induction!proof by}\index{proof!by induction}\index{induction!inference rule}
\end{figure}

\begin{exercises}
\exer {Let $d$ stand for the number of furlongs in
     the Boston Marathon, not counting the last 165 yards.
     Prove that \textsf{(nmb10 (dgts $d$))} $=$ $d$
     using the definitions of \textsf{dgts} (page \pageref{dgts-defun})
     and \textsf{nmb10} (page \pageref{nmb10-defun})
     but without citing any of the theorems from this section.}

\exer {Define a DoubleCheck property to test
     the equation \textsf{(nmb10 (dgts $n$))} $=$ $n$ for random
     natural numbers $n$.
     Of course, all of the tests should succeed because
     we proved that the formula always delivers true.
     If a test fails, something is wrong
     with the definition of the property or the operators it refers to.}

\exer {Define a DoubleCheck property to test
     \textsf{(equal (dgts (nmb10 $xs$)) $xs$)} for random
     decimal numerals $xs$.\\
     \emph{Note}: \textsf{(random-list-of (random-between 0 9))}
     generates random decimal numerals.\\
     \emph{Note}: The test must use the operator
     \textsf{equal} because \textsf{(= $x$ $y$)}
     requires $x$ and $y$ to be numbers.\\
     \emph{Note}: This test can fail.
     If it does, check out the data that causes the failure.}

\exer {We proved that
     $\forall n. ($\textsf{(nmb10 (dgts $n$))} $=$ $n)$ (page \pageref{dgts-ok}).
     That is, the operator \textsf{nmb10}
     inverts the operator \textsf{dgts}.
     However, it is not quite true that \textsf{dgts} inverts \textsf{nmb10}.
     Why not? Give an example of a decimal numeral
     $xs$ for which \textsf{(dgts (nmb10 $xs$))} $\neq$ $xs$.}

\exer {\label{ex:dgts-inverts-nmb10}Describe a constraint on $xs$ such that
     \textsf{(dgts (nmb10 $xs$))} $=$ $xs$.}

\exer {Prove that
    \textsf{(dgts (nmb10 $xs$))} $=$ $xs$
     if $xs$ satisfies the constraint of exercise \ref{ex:dgts-inverts-nmb10}.}

\exer {Prove that
    $\forall n.($\textsf{(len (dgts $(n+1)$))} $=$ $\lfloor log(n+1) \rfloor + 1)$~~~\{len-bits 10\}\\
    \emph{Note}: $\lfloor log(n+1) \rfloor$ $=$ an integer such that
    $10^{\lfloor log(n+1) \rfloor} \le (n+1) < 10^{\lfloor log(n+1) \rfloor + 1}$\\
    \emph{Note}: The operators \textsf{len} and \textsf{dgts}
    are defined on pages \pageref{len-equations} and \pageref{dgts-defun}.}

\end{exercises}

\begin{aside}{strong-induction-rule-2-hyps-or-1}{Strong Induction Requires Two Proofs or One?}
The inference rule for ordinary mathematical induction
(figure~\ref{induction-rule}, page \pageref{induction-rule})
requires two proofs above the line:
(1)~Prove $P(0)$ and (2)~Prove $\forall$$n$.(P($n$)$\rightarrow$P($n+1$)).
The strong induction rule
(figure~\ref{strong-induction-rule})
calls for only one proof:
Prove $(\forall m<n.P(m))\rightarrow P(n)$.
However, when $n = 0$, this is
$(\forall m<0.P(m))\rightarrow P(0)$.
Since there
are no natural numbers less than zero,
$(\forall m<0.P(m))$ is true because
a $\forall$ quantification with an empty universe of discourse
is true by default
(page \pageref{empty-forall}).

So, proving $(\forall m<0.P(m))\rightarrow P(0)$
is the same as proving $True \rightarrow P(0)$,
which is equivalent to proving $P(0)$,
just as in ordinary induction.
In other words, in strong induction there are really two proofs to do,
one for $P(0)$ and one for $(\forall m<n.P(m))\rightarrow P(n)$
when $n$ is not zero, which we usually state in the
equivalent form $(\forall m<n+1.P(m))\rightarrow P(n+1)$.

Looking at it this way makes a proof citing strong induction look like
a proof citing ordinary mathematical induction except that
in the proof of $P(n+1)$, the
\index{hypothesis!induction}\index{induction!hypothesis}induction hypothesis
includes all of the propositions $P(0)$, $P(1)$, $P(2) \dots P(n)$, not just $P(n)$.
The key is that a proof by strong induction
can cite any (or some, or even all) of those propositions
to justify steps in the proof of
$P(n+1)$.\index{strong induction}\index{induction!strong}\index{induction!proof by}\index{proof!by induction}\index{induction!inference rule}
%\caption{Strong Induction Requires Two Proofs or One?}
%\label{strong-induction-rule-2-hyps-or-1}
\end{aside}

\section{Binary Numerals}
\label{sec:binary-numerals}

Digital circuits, since they are materializations of formulas in mathematical logic,
have components that can represent two different values.
We call them zero and one, and it happens that those names
make it convenient to discuss circuits that deal with binary numerals,
which use 0 and 1 to denote binary digits (that is,
\index{zeros \& ones}\index{ones \& zeros}\index{bit (binary digit)}\emph{bits}).
Before delving into circuits, let's talk about binary numerals.

Decimal numerals represent numbers as sums of multiples of powers of ten.
Binary numerals are similar, but they use two as a base instead of ten.
So, a binary numeral with bits $x_nx_{n-1}\dots x_2x_1x_0$,
where each $x_i$ is either a zero or a one, stands for the number
$(x_0 + x_1 \times 2^1 + x_2 \times 2^2 + \dots + x_{n} \times 2^{n})$.
The only differences between this formula and the one that interprets
decimal numerals is that it uses powers of two instead of
powers of ten and the multipliers are bits (0, 1) instead of
digits (0, 1, 2, \dots 9).

Therefore, we can convert the operators for decimal numerals to binary
by changing the base from ten to two.
The operators \textsf{bits} and \textsf{numb},
which are used to construct and interpret binary numerals,
are defined in
figure~\ref{fig:defun-dgts-bits} (page \pageref{fig:defun-dgts-bits}).
Like the corresponding operators for decimal numerals
(\textsf{dgts}, page \pageref{dgts-defun}, and \textsf{nmb10}, page \pageref{nmb10-defun}),
\textsf{bits} and \textsf{numb} use the predicate \textsf{zp} (page \pageref{zp-def}) to choose
between the base case ($n = 0$) and the inductive case ($n > 0$).
ACL2 needs access to the theorems
in the floor-mod book (box~\ref{admit-def}, page \pageref{admit-def})
to admit the \textsf{bits} operator to its logic,
just as it did for the definition of \textsf{dgts}.

\begin{figure}
\begin{code}
\begin{verbatim}
(defun bits (n)
  (if (zp n)
      nil                                   ; {bits0}
      (cons (mod n 2) (bits (floor n 2))))) ; {bits1}

(defun numb (xs)
  (if (consp xs)
      (if (= (first xs) 1)
          (+ 1 (* 2 (numb (rest xs)))) ; {2numb+1}
          (* 2 (numb (rest xs))))      ; {2numb}
      0))                              ; {numb0}
\end{verbatim}
\end{code}
\caption{Definitions of operators \textsf{bits} and \textsf{numb}.}
\label{fig:defun-dgts-bits}
\label{nmb-defun}
\label{bits-defun}
\index{numeral!binary}\index{binary numeral}\index{operator, by name!bits (numeral from number)}\seeonlyindex{bits}{operator}
\index{axiom, by name!\{bits0\}, \{bits1\}}\index{equation, by name!\{bits0\}, \{bits1\}}
\index{representation!binary numeral}\index{operator, by name!numb (number from bits)}\seeonlyindex{numb}{operator}\index{axiom, by name!\{numb0\}, \{2numb\}, \{2numb+1\}}\index{equation, by name!\{numb0\}, \{2numb\}, \{2numb+1\}}
\end{figure}
	
A theorem about \textsf{numb} concerning the interpretation of
binary numerals as numbers and a theorem about \textsf{numb}
being the inverse of the \textsf{bits} operator are true,
and the proofs are similar to the proofs of the corresponding
theorems about decimal numerals presented earlier in this chapter.
Constructing those proofs can
clarify your understanding of both decimal numerals
and binary numerals.

\begin{aside}{aside:numeral-representation-trick}{Representation Trick: Any List Is a Binary Numeral}
A difference between the definition of \textsf{numb} (figure \ref{fig:defun-dgts-bits})
and the definition of \textsf{nmb10} (page \pageref{nmb10-defun})
is that \textsf{numb} treats bits as symbols,
whereas \textsf{nmb10} assumes that digits are numbers.
A $1$ in our representation of binary numerals
stands for a one-bit. Anything else stands for a zero-bit.
That's why the definition of \textsf{numb} has two equations (\{2numb+1\} and \{2numb\})
for nonempty numerals,
whereas the definition of \textsf{nmb10} has only one equation (\{n10.1\}).

There are two motivations for this design decision.
One is that it makes binary numerals entirely symbolic,
with no ephemeral entities like mathematical numbers.
Circuits represent bits symbolically by electronic signals,
and so the definition of \textsf{numb} is more closely
related to a circuit than it would be if it treated
bits as numbers.

The other motivation is to reduce the number of constraints
in theorems about ACL2 models of circuits.
Bits don't have to be lists of zeros and ones.
Any list is a numeral.
That numeral has one-bits where the elements of the list are ones
and zero-bits where its elements are anything other than ones.
In fact, numerals are entirely unconstrained.
The empty list represents the number zero,
but so does any ACL2 entity $x$ such that \textsf{(consp $x$)} is false.
Many picayune details in theorems about binary numerals
are avoided by this elimination of constraints.\index{numeral!list representation}
%\caption{Representation Trick: Any List is a Binary Numeral}
%\label{aside:numeral-representation-trick}
\end{aside}

\begin{exercises}

\exer {\label{horner2-thm}%
Adapt the proof of \{\emph{Horner 10}\} (page \pageref{horner10-thm}) to prove theorem
\index{theorem!Horner}\index{theorem, by name!\{horner 2\}@\{Horner 2\}}\index{Horner}\{\emph{Horner 2}\}.\\
\hspace*{1cm}$\forall n.($\textsf{(numb [$x_0$ $x_1$ $\dots$ $x_{n}$])}
$=$ $x_0 + x_1 \times 2^1 + x_2 \times 2^2 +$ $\dots$ $x_{n} \times 2^{n})$~~~\{\emph{Horner 2}\}}

\exer {\label{bits-ok}%
Prove theorem
\index{theorem, by name!\{bits-ok\}}\{\emph{bits ok}\}.
%\hspace*{1cm}
$\forall n.$(\textsf{((numb (bits $n$)) $=$ $n$)}$)$~~~\{\emph{bits ok}\}
%That is, the operator numb (page \pageref{nmb-defun})
%inverts the operator bits (page \pageref{bits-defun}).
}

\exer {\label{nmb1}%
Prove theorem
\index{equation, by name!\{nmb1\}}\index{theorem, by name!\{nmb1\}}\{nmb1\}.\\
\hspace*{1cm}$\forall n.($\textsf{(numb [$x_0$ $x_1$ $\dots$ $x_{n}$])}
$=$ \textsf{(numb [$x_0$]) $+$ $2\times$(numb [$x_1$ $x_2$ $\dots$ $x_{n}$])}$)$~~~\{nmb1\}}

\exer {\label{nmb1-acl2}\index{theorem, by name!\{nmb1\}}%
ACL2 succeeds in proving theorem \{nmb1\} (exercise \ref{nmb1}).
Confirm that assertion by running the following
formalization of the theorem through the mechanized logic:}
\begin{quote}
\begin{code}
\begin{verbatim}
(defthm nmb1
   (implies (consp xs)
            (= (+ (numb (list (first xs)))
                  (* 2 (numb (rest xs))))
               (numb xs))))
\end{verbatim}
\end{code}
\end{quote}

\exer {\label{ex:pad-defun}%
Given the following definition of operator \textsf{pad},
prove \index{theorem, by name!\{len-pad\}}theorem \{\emph{len-pad}\}:\\
\hspace*{1cm}$\forall n.($\textsf{(len (pad $n$ $x$ $xs$))} $=$ $n)$~~~ \{\emph{len-pad}\}}
%\begin{samepage}
\label{pad-defun}\index{operator, by name!pad (append padding)}\seeonlyindex{pad}{operator}\index{axiom, by name!\{pad$+$\}, \{pad$-$\}}\index{equation, by name!\{pad$+$\}, \{pad$-$\}}
\begin{quote}
\begin{code}
\begin{verbatim}
(defun pad (n x xs)
  (let* ((padding (- n (len xs))))
    (if (natp padding)
        (append xs (rep padding x)) ; {pad+}
        (prefix n xs))))            ; {pad-}
\end{verbatim}
\end{code}
\end{quote}

%\end{samepage}
\begin{quote}
\emph{Note}: The definition of \textsf{pad} refers to the operators
\textsf{rep} (page \pageref{rep-equations}) and \textsf{prefix} (page \pageref{prefix-equations}).
It uses a \textsf{let$*$} formula (box~\ref{let-star-def}, page \pageref{let-star-def})
to associate the name ``\textsf{padding}'' with the number of elements to append to $xs$
to form a list of the desired length. If $n$ is less than \textsf{(len $xs$)},
\textsf{pad} delivers the first $n$ elements of $xs$. In any case, the length of
\textsf{(pad $n$ $x$ $xs$)} is $n$.
\end{quote}

\exer {\label{hi-1}%
Given the following definition of operator \textsf{fin}, prove theorem \{\emph{hi-1}\}:\\
\hspace*{1cm}$\forall n. ($\textsf{(fin (bits $n$))} $=$ $1)$ if $n > 0$~~~\{\emph{hi-1}\}}
\label{fin-defun}\index{operator, by name!fin (extract last element)}\seeonlyindex{fin}{operator}\index{axiom, by name!\{fin1\}, \{fin2\}}\index{equation, by name!\{fin1\}, \{fin2\}}
\begin{quote}
\begin{code}
\begin{verbatim}
(defun fin (xs)
  (if (consp (rest xs))
      (fin (rest xs)) ; {fin2}
      (first xs)))    ; {fin1}
\end{verbatim}
\end{code}
\end{quote}

\exer {\label{hi-1-defthm}%
Define theorem
\index{theorem, by name!\{hi-1\}}\{\emph{hi-1}\}
of exercise \ref{hi-1} in ACL2
and run it through the mechanized logic.
ACL2 will succeed if you use
\textsf{implies} and \textsf{posp} (box~\ref{zp-def}, page \pageref{zp-def})
to constrain the theorem to nonzero, natural numbers.
Of course, the definition of the operator \textsf{bits} (page \pageref{bits-defun})
will need to be admitted to the ACL2 logic  (box~\ref{admit-def}, page \pageref{admit-def})
before it can attempt the proof of this theorem.}

\exer {\label{len-bits}%
\index{theorem, by name!\{len-bits\}, \{len-bits$\le$\}}Prove theorem \{\emph{len-bits}\}.
$\forall n.((\lfloor 2^{n-1}\rfloor \le m < 2^n) \rightarrow ($\textsf{(len (bits $m$))} $=$ $n))$~~~\{\emph{len-bits}\}}

\exer {\label{len-bitsLE}%
\index{theorem, by name!\{len-bits\}, \{len-bits$\le$\}}Prove theorem \{\emph{len-bits}$\le$\}.
$\forall n.((0 \le m < 2^n) \rightarrow$ (\textsf{(len (bits $m$))} $\le n))$~~~\{\emph{len-bits}$\le$\}}

\exer {\label{log-bits}%
\index{theorem, by name!\{log-bits\}}\index{numeral!length}Prove theorem \{\emph{log-bits}\}.
$\forall n.($\textsf{(len (bits $(n+1)$))} $=$ $\lfloor log_2(n+1) \rfloor + 1)$~~~\{\emph{log-bits}\} \\
\emph{Note}: $\lfloor x \rfloor$ is the greatest integer not exceeding $x$.}

\exer {\label{leading-0}%
\index{theorem, by name!\{leading-0\}, \{leading-0s\}}Prove theorem \{\emph{leading-0}\}.\\
\hspace*{1cm}$\forall n.($\textsf{(numb (append (bits $n$) (list 0)))} $=$ \textsf{(numb (bits $n$))}$)$~~~\{\emph{leading-0}\}}

\exer {\label{leading-0s}%
\index{theorem, by name!\{leading-0\}, \{leading-0s\}}\index{leading zero}\index{numeral!leading zero}Assume
theorem \{\emph{leading-0}\} (exercise~\ref{leading-0}) is true.
Prove theorem \{\emph{leading-0s}\}.\\
\hspace*{1cm}$\forall m.(\forall n.($\textsf{(numb (append (bits $n$) (rep $m$ 0)))} $=$
\textsf{(numb (bits $n$))}$))$~~~\{\emph{leading-0s}\}\\
\emph{Note}: The operator \textsf{rep} is defined on page \pageref{rep-equations}.}

\exer {\label{leading-0s-defthm}%
Express theorem \{\emph{leading-0s}\}
of the previous exercise in ACL2 notation
and run it through the ACL2 mechanized logic.
ACL2 will succeed if you state the theorem correctly as an implication,
referring to the predicate \textsf{natp} to constrain $n$ and $m$ to be natural numbers.
Of course, the definitions of the operators
\textsf{bits} and \textsf{numb} (page \pageref{bits-defun})
will need to be admitted to the ACL2 logic
(box~\ref{admit-def}, page \pageref{admit-def})
before it can attempt the proof of this theorem.}

\exer {\label{pfx-mod}%
\index{theorem, by name!\{pfx-mod\}}Prove theorem \{\emph{pfx-mod}\}:\\
\hspace*{1cm}
$\forall w.(\forall n.($\textsf{(numb (prefix $w$ (bits $n$)))} $=$ \textsf{(mod $n$ $2^w$)}$))$~~~\{\emph{pfx-mod}\}\\
\emph{Hint}: The universe of discourse of $\forall w$ is the natural numbers.
Induct on $w$.
Split the inductive case into two cases: $n = 0$ and $n > 0$.
Do a separate proof of the theorem for each case.
In the $n > 0$ case, the \{\emph{mod-div}\} theorem
(page \pageref{modular-division}) will be helpful.\\
\emph{Note}: The \{$\vee$ elimination\} rule
(figure~\ref{fig-02-deduction-rules}, page \pageref{fig-02-deduction-rules})
formally justifies case-by-case proofs.}

%\Exercise We created the definitions of bits and numb
%by copying those of dgts and nmb10, and changing the twos to tens.
%The practice of defining new entities by copying
%old ones and making a few changes can lead to erroors
%(page \pageref{abstraction}).
%It might have been better to define new operators with
%an additional parameter for the base to deal with positional
%numerals with any base.
%\label{numeral-from-number-defun}
%\begin{Verbatim}
%(defun numeral-from-number (b n)
%  (if (zp n)
%      nil
%      (cons (mod n b)
%            (numeral-from-number b (floor n b)))))
%\end{Verbatim}
%\label{number-from-numeral-defun}
%\begin{Verbatim}
%(defun number-from-numeral (b xs)
%  (if (consp xs)
%      (+ (first xs)
%         (* b (number-from-numeral b (rest xs))))
%      0))
%\end{Verbatim}
%Make new definitions of the operators dgts, nmb10, bits, and numb
%that rely on the abstraction of the base in
%the operators numeral-from-number and number-from-numeral.
%
%\Exercise In a manner similar to that suggested in the previous exercise,
%       define operators to convert
%       between numbers and hexadecimal (base 16) numerals.
%
%\Exercise The hexadecimal numerals in the previous exercise
%       use numbers between zero and fifteen to represent
%       hexadecimal digits. Define new operators that use,
%       instead, strings of characters from the set
%       {0, 1, 2, \dots, 9, A, B, C, D, E, F} to represent
%       hexadecimal numerals.
%       While you're at it, represent the numerals as string
%       in the usual ordering from high-order hexadecimal digit to
%       low-order, instead of the reverse order we have been using.
%       You may refer to the operators defined below that convert
%       between hex strings and numerals.
%       Strings in ACL2 are delimited by double-quote characters.
%\begin{Verbatim}
%(defun char-to-digit (chr)
%  (let* ((dgt9  (char-code #\9))
%         (code (char-code chr)))
%    (if (> code dgt9)
%        (+ 10 (- code (char-code #\A)))
%        (- code (char-code #\0)))))
%(defun chars-to-digits (chrs)
%  (if (consp chrs)
%      (cons (char-to-digit (first chrs))
%            (chars-to-digits (rest chrs)))
%      nil))
%(defun digits-to-chars (dgts)
%  (if (consp dgts)
%      (cons (digit-to-char (first dgts))
%            (digits-to-chars (rest dgts)))
%      nil))
%(defun string-to-numeral (str)
%  ; example: (string-to-numeral "41C5") = '(5 11 1 4)
%  (let* ((chrs (coerce (string-upcase str) 'list)))
%    (chars-to-digits (reverse chrs))))
%(defun numeral-to-string (nml)
%  ; example: (numeral-to-string '(5 11 1 4)) = "41C5"
%  (let* ((dgts (reverse nml)))
%    (coerce (digits-to-chars dgts) 'string)))
%\end{Verbatim}

\end{exercises}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "book"
%%% End: