|
|
|---|
|
|
|
|---|
A controlled boot-strap theory.
We begin with the theory at 'IHS-THEORIES (see :DOC IHS-THEORIES), and remove all of the :DEFINITION and :REWRITE rules. To this theory we add back in the theories BUILT-INS, MEASURES, and the following 3 names: CAR-CONS, CDR-CONS, and CAR-CDR-ELIM. This theory provides a controlled base for devloping books. Note that this theory is of limited use without some simple theory of arithmetic such as the theory ALGEBRA from the book "math-lemmas".
The key point of BASIC-BOOT-STRAP is to eliminate recursive definitions, and all of the random :REWRITE rules contained in the ACL2 boot-strap theory, while maintaining :EXECUTABLE-COUNTERPART and :TYPE-PRESCRIPTION rules. Of course, many useful non-recursive definitions and useful lemmas have also been disabled, but other theories should take care of ENABLEing those as the need arises.