SET-TAU-AUTO-MODE

turn on or off automatic (``greedy'') generation of :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.