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

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