|
|
|---|
|
|
|
|---|
A basic theory of algebra for all ACL2-numberps.
The ACL2-NUMBERP-ALGEBRA theory is designed to be a simple, compact basis for building other theories. This theory contains a minimal set of rules for basic algebraic manipulation including associativity and commutativity, simplification, cancellation, and normalization. It is extended by the theories RATIONALP-ALGEBRA and INTEGERP-ALGEBRA to include selected linear rules and rules for integers respectively. This theory also contains the DEFUN-THEORY (which see) of all built-in function symbols that would normally occur during reasoning about the ACL2-NUMBERPs.
We used keep this theory (and book) separate but roughly equal to the books maintained by Matt K. in order to have a solid, simple, and predictable foundation on which to build the rest of the books in the IHS hierarchy. However it was decided that this was too much trouble and we just select the rules of Matt K. that we want.