SET-TAU-AUTO-MODE

to turn on or off automatic generation of :tau-system rules
Major Section:  SWITCHES-PARAMETERS-AND-MODES

Examples:
(set-tau-auto-mode t)
(set-tau-auto-mode nil)

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.

The initial value is nil and we say that the tau-system is in manual mode. In manual mode, the only events that may 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. If the :tau-system rule class is specified but the formula is not of an appropriate shape, an error is signalled.

The tau system is initially in manual mode.

When the value of :tau-auto-modep is t we say the tau system is in automatic mode. In automatic mode, a :tau-system rule may be created even by events not explicitly specifying the :tau-system rule class.

In particular, in 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:

* defun events introducing ``big switch'' or ``mv-nth synonyms,''

* defun events creating type-prescription rules that may be also represented as ``signature rules'' of form 1, and

* 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.

See tau-system for a description of the various shapes named 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 :tau-system rules may be created also.

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.

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.