		Search-engine friendly clone of the ACL2 documentation.

Stobj

Def-stobj-frame

Automatically, opportunistically generate nth/update-nth frame theorems for a function that accesses or updates a stobj.

Example:

(defstobj foo bar baz biz)

(defun baz-to-bar (foo)
  (declare (xargs :stobjs foo))
  (update-bar (baz foo) foo))

(include-book "data-structures/list-defthms" :dir :system)

(in-theory (disable nth update-nth))

(def-stobj-frame baz-to-bar foo
  :hints ('(:in-theory (disable nth update-nth)))
  :ruleset foo-frame-thms)

This last event generates the following events:

(DEFTHMD NTH-FOO-OF-BAZ-TO-BAR
  (IMPLIES (AND (NOT (EQUAL (NFIX N) *BAR*)))
           (EQUAL (NTH N (BAZ-TO-BAR FOO))
                  (NTH N FOO))))

(ADD-TO-RULESET FOO-FRAME-THMS NTH-FOO-OF-BAZ-TO-BAR)

(DEFTHM BAZ-TO-BAR-FOO-FRAME
  (IMPLIES (OR (EQUAL (NFIX N) *BIZ*))
           (EQUAL (BAZ-TO-BAR (UPDATE-NTH N V FOO))
                  (UPDATE-NTH N V (BAZ-TO-BAR FOO)))))

(ADD-TO-RULESET FOO-FRAME-THMS BAZ-TO-BAR-FOO-FRAME)

The def-stobj-frame macro attempts to prove the following lemmas for each field of the stobj:

If the function returns the stobj:

(equal (nth *field* (fn stobj))            ;; type 1
       (nth *field* stobj))

and

(equal (fn (update-nth *field* val stobj)) ;; type 2
       (update-nth *field val (fn stobj)))

Otherwise,

(equal (fn (update-nth *field* val stobj)) ;; type 3
       (fn stobj))

It then generates defthm events based on which of these were successful.

It is probably important that nth and update-nth be disabled and suitable rules about them, such as the ones in data-structures/list-defthms, exist.

These proof attempts are done only with simplification and an expand hints. You may supply an additional hints, but only simplification is used. In particular, this utility won't work well on recursive functions, because generally they'll need induction to do the proofs (future work).