Levels of simplification for guard proof obligations

ACL2 provides several features for obtaining the proof obligations generated for guard verification. Each of these features can be invoked with an argument that controls the level of simplification to be applied before returning those proof obligations. This topic examines those simplification levels. It starts by splitting the features into two groups; then continues by explaining the three levels of simplification; and finally, makes the key point that one group allows the top two levels of simplification and the other group allows the bottom two levels.

These features can be partitioned into two groups, which we reference below
as the ``**AT**'' and ``**AFTER**'' groups, as follows. These
correspond respectively to the two groups discussed in the documentation
topic, guard-formula-utilities, for capturing formulas produced either
during guard verification or when a

- Simplification
**AT**guard-verification time:

- the
`xargs`keyword:guard-simplify , - the
`guard-obligation`utility, and - the
`verify-guards-formula`utility.

- the
- Simplification
**AFTER**guard-verification time:

- the
: `gthm`utility, and - the
: `guard-theorem`lemma-instance (and related low-level utility,guard-theorem .

- the

Each feature above has an argument (possibly optional) that control the level of simplification. Each such argument can take any of three values, as follows.

T :

Full simplification, which is the default behavior for`verify-guards`:LIMITED :

Reduced simplification, skipping simplifications that depend on the set of currently enabled rulesNIL :

No simplification

The key point of this topic is the following specification of the values
allowed for the simplification argument, for the features in each group. For
features in the **AT** group, **AFTER** group,

First consider the **AFTER** group. A `guard-theorem`
`current-theory` at the time of that
`guard-theorem` hint. Instead, the default is `gthm`
utility provides a way to show the formula that would be provided by a
`verify-guards-formula` is more appropriate than

Now consider the **AT** group, which relates to guard verification.