(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:
(equal (fn (update-nth *field* val stobj)) ;; type 2 (update-nth *field val (fn stobj)))
(equal (fn (update-nth *field* val stobj)) ;; type 3 (fn stobj))
It then generates defthm events based on which of these were successful.
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).