Set-tau-auto-mode
Turn on or off automatic (``greedy'') generation of :tau-system
rules
Examples:
(set-tau-auto-mode t) ; select automatic (``greedy'') mode
(set-tau-auto-mode nil) ; select manual mode
This event is equivalent to (table acl2-defaults-table :tau-auto-modep
<t-or-nil>), and hence is local to any books and encapsulate events in which it occurs; see ACL2-defaults-table.
See introduction-to-the-tau-system for background details.
The tau system gathers rules for its database in one of two ways: greedily
or only at the explicit command of the user. ``Greedy'' mode is officially
called ``automatic mode'' and is the default. The other mode is called
``manual mode.''
In automatic mode, all rules processed by ACL2 are also considered for
inclusion in the tau database: if the :corollary of some proved theorem
happens to fit into one of the forms described in :tau-system,
that rule is quietly added to the tau database regardless of what
:rule-classes the user named for the :corollary. Of course,
such rules are also stored in the ways named by the user. See the Design
Philosophy section of introduction-to-the-tau-system for a
discussion of why the tau system is greedy by default. More details are given
on automatic mode after we explain manual mode.
To more tightly control the rules available to the tau system, the user may
select manual mode by executing (set-tau-auto-mode nil). In manual mode,
the only events that create :tau-system rules are defthm events
explicitly specifying the :tau-system rule class in the
:rule-classes argument. Of course, for a :tau-system rule
to be created from a proved formula (or its specified :corollary), the
formula must be of the appropriate shape (syntactic form). See tau-system. In manual mode, if the :tau-system rule class is specified
but the formula is not of an appropriate form an error is signaled. (Note:
even in manual mode, monadic functions that are recognized as Boolean are
classified as tau predicates; but no rules are created for them.)
Returning to our discussion of automatic mode, a :tau-system
rule may be created by any of the events below, provided the definition or
formula proved is of an appropriate shape:
(1) defun events introducing ``big switch'' or ``mv-nth
synonyms,''
(2) defun events creating type-prescription rules that may be also
represented as ``signature rules'' of form 1, and
(3) any defthm event with a non-nil :rule-classes argument
if no :tau-system rule is among the rule classes and the formula proved
is in the shape of any tau-system rule.
Of course, events such as defstobj and defevaluator may
also add rules to the tau database when they execute the defun and
defthm events implicit in their descriptions. See tau-system
for a description of the various shapes mentioned above.
Note that any rule (of any rule class) created when the tau system is in
manual mode is also created in automatic mode. For example, if an event would
create a :DEFINITION, :TYPE-PRESCRIPTION, FORWARD-CHAINING, or
:REWRITE rule when the tau system is in manual mode, then the event will
create that same rule when the tau system is in automatic mode. Automatic
mode just means that some additional :tau-system rules may be
created.
Of course, if a defthm event explicitly specifies a :tau-system
rule class, then even if the tau system is in automatic mode, that tau rule is
created from the proved formula (or the specified :corollary) or else an
error is caused. But if the tau system is in automatic mode and a defthm
event doesn't explicitly specify a :tau-system rule class, then the
system quietly checks each specified :corollary — or, in the
absence of any :corollary, it checks the proved formula — for
whether it can be stored as a tau rule. If so, then the system stores a tau
rule, in addition to storing the specified rule. Of course, no error is
signaled if a proved formula of some non-:tau-system rule class fails to
be of an appropriate shape for the tau system.
In automatic mode, if the :rule-classes specified for defthm
included several corollaries and any one of them is of class :tau-system
then the only tau system rules created are those explicitly classed as
:tau-system rules. For example, suppose a defthm has one
:corollary stored as a :rewrite rule and another :corollary
stored as a :tau-system rule. But suppose the :rewrite rule happens
to also to fit the form of a :tau-system rule. Is it added to the tau
database or not? The answer is no. If you have taken the trouble to specify
:tau-system corollaries for an event, then those corollaries are the only
ones stored as tau system rules from that event. Note that had both
corollaries been classed as :rewrite rules (and been of acceptable
:tau-system form) both would have also been made :tau-system rules.
This also allows you be in automatic mode and state a :rewrite or other
non-:tau-system rule and prevent it from being also made a tau system
rule: just add a frivolous :tau-system :corollary like (booleanp
(integerp x)).
Recall that the use of tau rules is controlled by the rune
(:EXECUTABLE-COUNTERPART TAU-SYSTEM). When that rune is disabled, no tau
rules are used in proofs. However, the tau system continues to collect
tau rules if the system is in automatic mode. Thus, if and when the tau
system is re-enabled, rules automatically generated while the tau system was
disabled will be used as usual by the tau system.
Finally, note that defthm events with :rule-classes nil do
not create :tau-system rules even if the formula proved is of an
appropriate shape, regardless of whether the tau system is in automatic or
manual mode.
The macro tau-status provides a convenient way to enable/disable
the :executable-counterpart of tau-system and/or to switch
between manual and automatic modes. It may also be used to determine the
current settings of those two flags.
