		Search-engine friendly clone of the ACL2 documentation.

Defabsstobj-events

Alternative to defabsstobj that tries to prove the necessary correspondence and preservation theorems instead of making you prove them ahead of time.

This is essentially a drop-in replacement for defabsstobj that. Instead of requiring you to copy/paste the preservation/correspondence theorems and prove them ahead of time, it just tries to go ahead and prove them before submitting the defabsstobj form.

This can often eliminate a lot of tedious copy/paste updating. It is also useful in macros that generate abstract stobjs, such as def-1d-arr and similar.

The syntax is like that of defabsstobj, e.g.,:

(defabsstobj-events st
  :foundation st$c
  :recognizer (stp :logic st$ap :exec st$cp)
  :creator (create-st :logic create-st$a :exec create-st$c)
  :corr-fn st$corr
  :exports ((foo :logic foo$a :exec foo$c)
            ...
            (baz :exec baz$a :exec baz$c)))

The macro operates very simply:

Use defabsstobj-missing-events to generate the necessary theorems, then
Try to submit these events to ACL2 via a make-event, then finally
Submit the defabsstobj form.

The theorems submitted in Step 2 are just attempted in your current theory and with no hints. If some theorem can't be proven, the easiest thing to do is extract it (copy and paste it) above your defabsstobj-events form so that you can give it hints. For instance:

(encapsulate ()
 (local (defthm foo{correspondence}  ;; presumably need hints
          ...
          :hints (...)))
 (defabsstobj-events st ...))