Proving Theorems about Models

But ACL2 is a **logic**. We can **prove theorems about the
model**.

Theorem. MC 'mult is a multiplier(implies (and (natp x) (natp y)) (equal (lookup 'z (mc (s 'mult x y) (mclk x))) (* x y))).

This theorem says that a certain program running on the **mc** machine
will correctly multiply **any two natural numbers**.

It is a statement about an **infinite** number of test cases!

We know it is true about the model because we **proved** it.

Of course, models of actual machines usually only accept a finite number of
different inputs. For example, engineers at Advanced Micro Devices (AMD),
Centaur, and IBM have ACL2 models of floating point units that operate on
double precision IEEE floating point numbers. These are finite models. But
the size of their inputs is sufficiently large that they are verified by the
same mathematical methods used to prove theorems about infinite state systems
like our little