ACL2-pc::in-theory
(primitive)
set the current proof-builder theory
Example:
(in-theory
(union-theories (theory 'minimal-theory) '(true-listp binary-append)))
General Form:
(in-theory &optional atom-or-theory-expression)
If the argument is not supplied, then this command sets the current
interactive proof-builder theory (see below for explanation) to agree with the
current ACL2 theory. Otherwise, the argument should be a theory expression,
and in that case the proof-builder theory is set to the value of that theory
expression.
The current interactive proof-builder theory is used in all calls to the
ACL2 theorem prover and rewriter from inside the proof-builder. Thus, the
most recent in-theory instruction in the current state-stack has an
effect in the proof-builder totally analogous to the effect caused by an
in-theory hint or event in ACL2. All in-theory instructions before
the last are ignored, because they refer to the current theory in the ACL2
state, not to the existing proof-builder theory. For example:
ACL2 !>:trans1 (enable bar)
(UNION-THEORIES (CURRENT-THEORY :HERE)
'(BAR))
ACL2 !>:trans1 (CURRENT-THEORY :HERE)
(CURRENT-THEORY-FN :HERE WORLD)
ACL2 !>
Thus (in-theory (enable bar)) modifies the current theory of the
current ACL2 world. So for example, suppose that foo is disabled outside
the proof-builder and you execute the following instructions, in this
order.
(in-theory (enable foo))
(in-theory (enable bar))
Then after the second of these, bar will be enabled in the
proof-builder, but foo will be disabled. The reason is that
(in-theory (enable bar)) instructs the proof-builder to modify the
current theory (from outside the proof-builder, not from inside the
proof-builder) by enabling bar.
Note that in-theory instructions in the proof-builder have no effect
outside the proof-builder's interactive loop.
If the most recent in-theory instruction in the current state of the
proof-builder has no arguments, or if there is no in-theory instruction
in the current state of the proof-builder, then the proof-builder will use the
current ACL2 theory. This is true even if the user has interrupted the
interactive loop by exiting and changing the global ACL2 theory. However, if
the most recent in-theory instruction in the current state of the
proof-builder had an argument, then global changes to the current theory will
have no effect on the proof-builder state.
