Major Section: OTHER

Below, when we talk about ``an event `A`

'', we mean an event whose name is
`A`

.

When event `A`

is used in a proof performed to admit event `B`

that you
submit to ACL2, we say that `A`

is a ``proof-supporter'' of `B`

. ACL2
stores an association list such that for every event `B`

with at least one
proof-supporter, `B`

is associated with a list of all of its
proof-supporters, sorted by `symbol-<`

. The following form evaluates to
that alist, which is called the ``proof-supporters-alist''.

(global-val 'proof-supporters-alist (w state))By ``used in a proof'' above, we mean: applied as a rule or supplied explicitly via hints of type

`:use`

, `:by`

, or
`:clause-processor`

. That is, the events ``used in a proof'' for
admitting an event `E`

are those listed in the summary printed at the
conclusion of admitting `E`

.
Note that if proofs are skipped when admitting event `E`

, say because the
last admission of `E`

was done by `include-book`

(or `certify-book`

,
which ends with an `include-book`

), then there will be no entry in that
alist for `E`

. (An exception is made however for `encapsulate`

events, where proof-supporters are remembered from the first pass; see
below.) So if you want the proof-supporters-alist to include supporters for
events in a book, use `ld`

rather than `include-book`

or
`certify-book`

to process the events in that book. If however you are
interested in the proof-supporters FROM a book that support a later event,
then it is fine to include that book.

The case for `encapsulate`

is slightly tricky. Consider an example of
the following form.

A ; event preceding the encapsulate (encapsulate () B (local C) ; uses A and B in a proof D ; uses C in a proof )At the conclusion of this

`encapsulate`

event, the proof-supporters-alist
associates `D`

with `A`

and `B`

, but not `C`

(which has disappeared,
since it is local).Note that this sort of ``transitive closure'' operation is only performed
when necessary due to the disappearance of local events. For
example, if we replace `(local C)`

above by just `C`

, then `D`

is
associated in the proof-supporters-alist only with `C`

, not with `A`

or
`B`

. If you want the transitive closure of the relation computed by the
proof-supporters-alist, you have to compute it yourself. (This was a
deliberate design decision, in order to avoid slowing down event processing.)
However, there is help available on how to do such a computation:

A distributed book, `books/misc/dead-events.lisp`

, does such a transitive
closure, and moreover uses that information to find ``dead events'' relative
to a list of ``desired'' events. For example, suppose you use `LD`

to
process the events, with proofs, in a book intended to prove theorems
`MAIN-1`

and `MAIN-2`

. (Remember, `certify-book`

will not save such
information.) Suppose furthermore that the book begins with some
`include-book`

forms followed by `(deflabel book-start)`

. You could
evaluate this form:

(dead-events '(main-1 main-2) :start 'book-start)The result is a list of events that you probably can delete from the book without causing any proofs to fail. See the

`dead-events.lisp`

book for
further documentation.You might also find the code in the above book to be helpful for writing your own utilities based on the proof-supporters-alist.