Filtering...

stobj-help

books/tools/stobj-help

Included Books

top simplify-thm
other
(in-package "ACL2")
nth-out-of-rangetheorem
(defthm nth-out-of-range
  (implies (<= (len lst) (nfix n)) (not (nth n lst))))
len-resize-listtheorem
(defthm len-resize-list
  (equal (len (resize-list lst n default)) (nfix n)))
nth-rsz-inductionfunction
(defun nth-rsz-induction
  (n len lst)
  (if (or (zp n) (zp len))
    lst
    (nth-rsz-induction (1- n)
      (1- len)
      (if (consp lst)
        (cdr lst)
        lst))))
nth-resize-list-niltheorem
(defthm nth-resize-list-nil
  (implies (<= (nfix len) (nfix n))
    (equal (nth n (resize-list lst len default)) nil))
  :hints (("goal" :induct (nth-rsz-induction n len lst))))
nth-resize-listtheorem
(defthm nth-resize-list
  (equal (nth n (resize-list lst len default))
    (and (< (nfix n) (nfix len))
      (if (< (nfix n) (len lst))
        (nth n lst)
        default)))
  :hints (("goal" :induct (nth-rsz-induction n len lst)
     :in-theory (enable zp len)) ("Subgoal *1/1" :expand ((resize-list lst len default) (len lst)))))
nth-make-list-ac-indfunction
(defun nth-make-list-ac-ind
  (m n)
  (if (or (zp m) (zp n))
    nil
    (nth-make-list-ac-ind (1- m) (1- n))))
make-list-ac-opentheorem
(defthmd make-list-ac-open
  (implies (not (zp n))
    (equal (make-list-ac n elt tail)
      (cons elt (make-list-ac (1- n) elt tail)))))
nth-make-list-acencapsulate
(encapsulate nil
  (local (include-book "arithmetic-5/top" :dir :system))
  (defthm nth-make-list-ac
    (equal (nth i (make-list-ac j val ac))
      (if (< (nfix i) (nfix j))
        val
        (nth (- i (nfix j)) ac)))
    :hints (("goal" :induct (nth-make-list-ac-ind i j)
       :in-theory (enable make-list-ac-open)))))
include-book
(include-book "misc/simplify-thm" :dir :system)
other
(program)
other
(set-state-ok t)
array-specpfunction
(defun array-specp
  (spec)
  (let ((type (cadr (assoc-keyword :type (cdr spec)))))
    (and (consp type) (eq (car type) 'array))))
ht-specpfunction
(defun ht-specp
  (spec)
  (let ((type (cadr (assoc-keyword :type (cdr spec)))))
    (and (consp type) (eq (car type) 'hash-table))))
mutator-callsfunction
(defun mutator-calls
  (spec stobj renaming)
  (let ((field (car spec)))
    (cond ((ht-specp spec) `((,(DEFSTOBJ-FNNAME FIELD :UPDATER :HASH-TABLE RENAMING) mk
           v
           ,STOBJ) (,(DEFSTOBJ-FNNAME FIELD :REMOVE :HASH-TABLE RENAMING) mk
            ,STOBJ)
          (,(DEFSTOBJ-FNNAME FIELD :CLEAR :HASH-TABLE RENAMING) ,STOBJ)))
      ((array-specp spec) `((,(DEFSTOBJ-FNNAME FIELD :UPDATER :ARRAY RENAMING) mi
           v
           ,STOBJ) (,(DEFSTOBJ-FNNAME FIELD :RESIZE :ARRAY RENAMING) len
            ,STOBJ)))
      (t `((,(DEFSTOBJ-FNNAME FIELD :UPDATER NIL RENAMING) v ,STOBJ))))))
accessor-callsfunction
(defun accessor-calls
  (spec stobj renaming)
  (let ((field (car spec)))
    (cond ((ht-specp spec) `((,(DEFSTOBJ-FNNAME FIELD :ACCESSOR :HASH-TABLE RENAMING) ak
           ,STOBJ) (,(DEFSTOBJ-FNNAME FIELD :BOUNDP :HASH-TABLE RENAMING) ak
            ,STOBJ)
          (,(DEFSTOBJ-FNNAME FIELD :COUNT :HASH-TABLE RENAMING) ,STOBJ)))
      ((array-specp spec) `((,(DEFSTOBJ-FNNAME FIELD :ACCESSOR :ARRAY RENAMING) ai
           ,STOBJ) (,(DEFSTOBJ-FNNAME FIELD :LENGTH :ARRAY RENAMING) ,STOBJ)))
      (t `((,(DEFSTOBJ-FNNAME FIELD :ACCESSOR NIL RENAMING) ,STOBJ))))))
def-stobj-self-mod-thmsfunction
(defun def-stobj-self-mod-thms
  (spec stobj renaming)
  (let ((field (car spec)) (create (defstobj-fnname stobj :creator nil renaming))
      (init (cadr (assoc-keyword :initially (cdr spec)))))
    (cond ((ht-specp spec) (let* ((upd (defstobj-fnname field :updater :hash-table renaming)) (rem (defstobj-fnname field :remove :hash-table renaming))
            (clr (defstobj-fnname field :clear :hash-table renaming))
            (acc (defstobj-fnname field :accessor :hash-table renaming))
            (bdp (defstobj-fnname field :boundp :hash-table renaming))
            (cnt (defstobj-fnname field :count :hash-table renaming)))
          `((defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-"
  (SYMBOL-NAME CREATE))
             (equal (,ACC ak (,CREATE)) nil)) (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-" (SYMBOL-NAME UPD))
              (equal (,ACC ak (,UPD mk v ,STOBJ))
                (if (equal ak mk)
                  v
                  (,ACC ak ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-" (SYMBOL-NAME REM))
              (equal (,ACC ak (,REM mk ,STOBJ))
                (if (equal ak mk)
                  nil
                  (,ACC ak ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-" (SYMBOL-NAME CLR))
              (equal (,ACC ak (,CLR ,STOBJ)) nil))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME BDP) "-"
  (SYMBOL-NAME CREATE))
              (equal (,BDP ak (,CREATE)) nil))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME BDP) "-" (SYMBOL-NAME UPD))
              (equal (,BDP ak (,UPD mk v ,STOBJ))
                (if (equal ak mk)
                  t
                  (,BDP ak ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME BDP) "-" (SYMBOL-NAME REM))
              (equal (,BDP ak (,REM mk ,STOBJ))
                (if (equal ak mk)
                  nil
                  (,BDP ak ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME BDP) "-" (SYMBOL-NAME CLR))
              (equal (,BDP ak (,CLR ,STOBJ)) nil))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME CNT) "-"
  (SYMBOL-NAME CREATE))
              (equal (,CNT (,CREATE)) 0))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME CNT) "-" (SYMBOL-NAME UPD))
              (equal (,CNT (,UPD mk v ,STOBJ))
                (if (,BDP mk ,STOBJ)
                  (,CNT ,STOBJ)
                  (+ 1 (,CNT ,STOBJ)))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME CNT) "-" (SYMBOL-NAME REM))
              (equal (,CNT (,REM mk ,STOBJ))
                (if (,BDP mk ,STOBJ)
                  (- (,CNT ,STOBJ) 1)
                  (,CNT ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME CNT) "-" (SYMBOL-NAME CLR))
              (equal (,CNT (,CLR ,STOBJ)) 0)))))
      ((array-specp spec) (let* ((upd (defstobj-fnname field :updater :array renaming)) (rsz (defstobj-fnname field :resize :array renaming))
            (acc (defstobj-fnname field :accessor :array renaming))
            (len (defstobj-fnname field :length :array renaming))
            (size (car (caddr (cadr (assoc-keyword :type (cdr spec)))))))
          `((defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-"
  (SYMBOL-NAME CREATE))
             (equal (,ACC ai (,CREATE)) (and (< (nfix ai) ,SIZE) ,INIT))
             :hints (("Goal" :in-theory (disable make-list-ac (make-list-ac))))) (defthmd ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-OUT-OF-RANGE")
              (implies (<= (,LEN ,STOBJ) (nfix n)) (not (,ACC n ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-NON-NATP")
              (implies (not (natp n))
                (equal (,ACC n ,STOBJ) (,ACC 0 ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-" (SYMBOL-NAME UPD))
              (equal (,ACC ai (,UPD mi v ,STOBJ))
                (if (equal (nfix ai) (nfix mi))
                  v
                  (,ACC ai ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME UPD) "-NON-NATP")
              (implies (not (natp n))
                (equal (,UPD n v ,STOBJ) (,UPD 0 v ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) (SYMBOL-NAME RSZ))
              (equal (,ACC ai (,RSZ len ,STOBJ))
                (and (< (nfix ai) (nfix len))
                  (if (< (nfix ai) (,LEN ,STOBJ))
                    (,ACC ai ,STOBJ)
                    ,INIT))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME LEN) "-"
  (SYMBOL-NAME CREATE))
              (equal (,LEN (,CREATE)) ,SIZE))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME LEN) "-" (SYMBOL-NAME UPD))
              (equal (,LEN (,UPD mi v ,STOBJ))
                (max (+ 1 (nfix mi)) (,LEN ,STOBJ))))
            (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME LEN) "-" (SYMBOL-NAME RSZ))
              (equal (,LEN (,RSZ len ,STOBJ)) (nfix len))))))
      (t (let* ((upd (defstobj-fnname field :updater nil renaming)) (acc (defstobj-fnname field :accessor nil renaming)))
          `((defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-"
  (SYMBOL-NAME CREATE))
             (equal (,ACC (,CREATE)) ,INIT)) (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-" (SYMBOL-NAME UPD))
              (equal (,ACC (,UPD v ,STOBJ)) v))))))))
def-stobj-acc-of-upd-thms1111function
(defun def-stobj-acc-of-upd-thms1111
  (stobj acc upds)
  (if (atom upds)
    nil
    (cons `(defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME (CAR ACC)) "-"
  (SYMBOL-NAME (CAAR UPDS)))
        (equal ,(SUBST (CAR UPDS) STOBJ ACC) ,ACC))
      (def-stobj-acc-of-upd-thms1111 stobj acc (cdr upds)))))
def-stobj-acc-of-upd-thms111function
(defun def-stobj-acc-of-upd-thms111
  (stobj accs upds)
  (if (atom accs)
    nil
    (append (def-stobj-acc-of-upd-thms1111 stobj (car accs) upds)
      (def-stobj-acc-of-upd-thms111 stobj (cdr accs) upds))))
def-stobj-acc-of-upd-thms11function
(defun def-stobj-acc-of-upd-thms11
  (stobj spec specs renaming)
  (if (atom specs)
    nil
    (append (if (equal spec (car specs))
        (def-stobj-self-mod-thms spec stobj renaming)
        (def-stobj-acc-of-upd-thms111 stobj
          (accessor-calls spec stobj renaming)
          (mutator-calls (car specs) stobj renaming)))
      (def-stobj-acc-of-upd-thms11 stobj
        spec
        (cdr specs)
        renaming))))
def-stobj-acc-of-upd-thms1function
(defun def-stobj-acc-of-upd-thms1
  (stobj specs all-specs renaming)
  (if (atom specs)
    nil
    (append (def-stobj-acc-of-upd-thms11 stobj
        (car specs)
        all-specs
        renaming)
      (def-stobj-acc-of-upd-thms1 stobj
        (cdr specs)
        all-specs
        renaming))))
def-stobj-acc-of-upd-thms-mkeventfunction
(defun def-stobj-acc-of-upd-thms-mkevent
  (stobj state)
  (let* ((rb (getprop stobj
         'redundancy-bundle
         nil
         'current-acl2-world
         (w state))) (specs (car rb))
      (renaming (cdr rb)))
    (def-stobj-acc-of-upd-thms1 stobj specs specs renaming)))
def-stobj-acc-of-upd-thmsmacro
(defmacro def-stobj-acc-of-upd-thms
  (stobj)
  `(make-event `(progn . ,(DEF-STOBJ-ACC-OF-UPD-THMS-MKEVENT ',STOBJ STATE))))
def-stobj-type-theory-fnfunction
(defun def-stobj-type-theory-fn
  (stobj specs renaming state)
  (declare (xargs :mode :program))
  (if (atom specs)
    (value nil)
    (er-let* ((thms (let* ((spec (car specs)) (field (car spec)))
           (cond ((ht-specp spec) (let* ((upd (defstobj-fnname field :updater :hash-table renaming)) (rem (defstobj-fnname field :remove :hash-table renaming))
                   (clr (defstobj-fnname field :clear :hash-table renaming))
                   (bdp (defstobj-fnname field :boundp :hash-table renaming))
                   (cnt (defstobj-fnname field :count :hash-table renaming))
                   (stobj-rec (defstobj-fnname stobj :recognizer :top renaming)))
                 (value `((defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-BOOLEANP-" (SYMBOL-NAME BDP))
                      (booleanp (,BDP ak ,STOBJ))
                      :rule-classes :type-prescription) (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ) "-NATP-" (SYMBOL-NAME CNT))
                       (natp (,CNT ,STOBJ))
                       :rule-classes :type-prescription)
                     (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ-REC) "-" (SYMBOL-NAME UPD))
                       (implies (,STOBJ-REC ,STOBJ)
                         (,STOBJ-REC (,UPD mk v ,STOBJ))))
                     (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ-REC) "-" (SYMBOL-NAME REM))
                       (implies (,STOBJ-REC ,STOBJ) (,STOBJ-REC (,REM mk ,STOBJ))))
                     (defthm ,(INCAT STOBJ (SYMBOL-NAME STOBJ-REC) "-" (SYMBOL-NAME CLR))
                       (implies (,STOBJ-REC ,STOBJ) (,STOBJ-REC (,CLR ,STOBJ))))))))
             ((array-specp spec) (let* ((upd (defstobj-fnname field :updater :array renaming)) (rsz (defstobj-fnname field :resize :array renaming))
                   (acc (defstobj-fnname field :accessor :array renaming))
                   (len (defstobj-fnname field :length :array renaming))
                   (field-rec (defstobj-fnname field :recognizer :hash-table renaming))
                   (stobj-rec (defstobj-fnname stobj :recognizer :top renaming))
                   (init (cadr (assoc-keyword :initially (cdr spec))))
                   (type (cadr (cadr (assoc-keyword :type (cdr spec)))))
                   (pred (translate-declaration-to-guard type 'x (w state)))
                   (stobj-rec-upd-form `(implies (and (,STOBJ-REC ,STOBJ) ,PRED (< (nfix i) (,LEN ,STOBJ)))
                       (,STOBJ-REC (,UPD i x ,STOBJ)))))
                 (er-let* ((stobj-rec-upd-thms (simplify-thm-fn (incat field (symbol-name stobj-rec) "-" (symbol-name upd))
                        stobj-rec-upd-form
                        `(("Goal" :in-theory (theory 'minimal-theory)))
                        nil
                        state)))
                   (value `((defthmd ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME FIELD-REC) "-NTH-TYPE")
                        (implies (and (,FIELD-REC x) (< (nfix n) (len x)))
                          ,(SUBST '(NTH N X) 'X PRED))
                        :rule-classes :type-prescription) (defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-TYPE")
                         (implies (and (,STOBJ-REC ,STOBJ) (< (nfix i) (,LEN ,STOBJ)))
                           ,(SUBST `(,ACC I ,STOBJ) 'X PRED))
                         :hints (("goal" :in-theory (enable ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME FIELD-REC) "-NTH-TYPE"))))
                         :rule-classes :type-prescription)
                       (defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME FIELD-REC) "-UPDATE-NTH")
                         (implies (and (,FIELD-REC fld) (< (nfix n) (len fld)) ,PRED)
                           (,FIELD-REC (update-nth n x fld))))
                       ,@STOBJ-REC-UPD-THMS
                       (defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME LEN) "-TYPE")
                         (natp (,LEN ,STOBJ))
                         :rule-classes :type-prescription)
                       (defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME FIELD-REC) "-RESIZE-LIST")
                         (implies (,FIELD-REC x)
                           (,FIELD-REC (resize-list x n ,INIT))))
                       (defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME RSZ) "-"
  (SYMBOL-NAME STOBJ-REC))
                         (implies (,STOBJ-REC ,STOBJ) (,STOBJ-REC (,RSZ n ,STOBJ)))))))))
             (t (let* ((upd (defstobj-fnname field :updater nil renaming)) (acc (defstobj-fnname field :accessor nil renaming))
                   (type (cadr (assoc-keyword :type (cdr spec))))
                   (pred (translate-declaration-to-guard type 'x (w state)))
                   (stobj-rec (defstobj-fnname stobj :recognizer :top renaming))
                   (stobj-rec-upd-form `(implies (and (,STOBJ-REC ,STOBJ)
                         ,@(IF (EQUAL PRED ''NIL)
      NIL
      (LIST PRED)))
                       (,STOBJ-REC (,UPD x ,STOBJ)))))
                 (er-let* ((stobj-rec-upd-thms (simplify-thm-fn (incat field (symbol-name stobj-rec) "-" (symbol-name upd))
                        stobj-rec-upd-form
                        '(("Goal" :in-theory (theory 'minimal-theory)))
                        nil
                        state)))
                   (if (equal pred ''nil)
                     (value stobj-rec-upd-thms)
                     (value `((defthm ,(INCAT FIELD (SYMBOL-NAME STOBJ) "-" (SYMBOL-NAME ACC) "-TYPE")
                          (implies (,STOBJ-REC ,STOBJ)
                            ,(SUBST `(,ACC ,STOBJ) 'X PRED))
                          :rule-classes :type-prescription) . ,STOBJ-REC-UPD-THMS))))))))) (rest (def-stobj-type-theory-fn stobj (cdr specs) renaming state)))
      (value (append thms rest)))))
def-stobj-simple-field-equivs11function
(defun def-stobj-simple-field-equivs11
  (stobj equiv calls)
  (if (atom calls)
    nil
    (cons `(defthm ,(INCAT EQUIV (SYMBOL-NAME EQUIV) "-" (SYMBOL-NAME (CAAR CALLS)))
        (,EQUIV ,(CAR CALLS) ,STOBJ))
      (def-stobj-simple-field-equivs11 stobj equiv (cdr calls)))))
def-stobj-simple-field-equivs1function
(defun def-stobj-simple-field-equivs1
  (stobj cspec equiv specs renaming)
  (if (atom specs)
    nil
    (if (equal cspec (car specs))
      (def-stobj-simple-field-equivs1 stobj
        cspec
        equiv
        (cdr specs)
        renaming)
      (let* ((spec (car specs)) (calls (mutator-calls spec stobj renaming)))
        (append (def-stobj-simple-field-equivs11 stobj equiv calls)
          (def-stobj-simple-field-equivs1 stobj
            cspec
            equiv
            (cdr specs)
            renaming))))))
def-stobj-simple-field-equivsfunction
(defun def-stobj-simple-field-equivs
  (stobj specs all-specs renaming)
  (if (atom specs)
    nil
    (if (or (ht-specp (car specs)) (array-specp (car specs)))
      (def-stobj-simple-field-equivs stobj
        (cdr specs)
        all-specs
        renaming)
      (let* ((spec (car specs)) (field (car spec))
          (equiv (incat stobj
              (symbol-name stobj)
              "-"
              (symbol-name field)
              "-EQ"))
          (acc (defstobj-fnname field :accessor nil renaming))
          (upd (defstobj-fnname field :updater nil renaming)))
        `((defun-nx ,EQUIV (a b) (equal (,ACC a) (,ACC b))) (defequiv ,EQUIV)
          (defcong ,EQUIV equal (,ACC ,STOBJ) 1)
          (defthm ,(INCAT STOBJ (SYMBOL-NAME EQUIV) "-" (SYMBOL-NAME UPD) "-NORM")
            (implies (syntaxp (not (equal ,STOBJ ''t)))
              (,EQUIV (,UPD x ,STOBJ) (,UPD x t))))
          ,@(DEF-STOBJ-SIMPLE-FIELD-EQUIVS1 STOBJ SPEC EQUIV ALL-SPECS RENAMING)
          ,@(DEF-STOBJ-SIMPLE-FIELD-EQUIVS STOBJ (CDR SPECS) ALL-SPECS RENAMING)
          (in-theory (disable ,EQUIV)))))))
def-stobj-theory-fn-names1function
(defun def-stobj-theory-fn-names1
  (specs stobj renaming)
  (if (atom specs)
    nil
    (append (strip-cars (mutator-calls (car specs) stobj renaming))
      (strip-cars (accessor-calls (car specs) stobj renaming))
      (def-stobj-theory-fn-names1 (cdr specs) stobj renaming))))
def-stobj-theory-fn-namesfunction
(defun def-stobj-theory-fn-names
  (specs stobj renaming)
  (list* (defstobj-fnname stobj :recognizer :top renaming)
    (def-stobj-theory-fn-names1 specs stobj renaming)))
def-stobj-theory-mkeventfunction
(defun def-stobj-theory-mkevent
  (stobj state)
  (declare (xargs :mode :program :stobjs state))
  (let* ((rb (getprop stobj
         'redundancy-bundle
         nil
         'current-acl2-world
         (w state))) (specs (car rb))
      (renaming (cdr rb))
      (fn-names (def-stobj-theory-fn-names specs stobj renaming)))
    (er-let* ((type-thms (def-stobj-type-theory-fn stobj specs renaming state)))
      (value `(encapsulate nil
          ,@(DEF-STOBJ-ACC-OF-UPD-THMS1 STOBJ SPECS SPECS RENAMING)
          ,@TYPE-THMS
          (in-theory (disable . ,FN-NAMES)) . ,(DEF-STOBJ-SIMPLE-FIELD-EQUIVS STOBJ SPECS SPECS RENAMING))))))
def-stobj-theorymacro
(defmacro def-stobj-theory
  (stobj)
  `(make-event (def-stobj-theory-mkevent ',STOBJ state)))