:tau-system rules
Major Section: SWITCHES-PARAMETERS-AND-MODES
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 signalled. (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 signalled 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 sytem
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.
