defined-const

(defun defined-const-fn
  (constname term thmname rule-classes evisc hons)
  (let ((thmname (or thmname
         (intern-in-package-of-symbol (concatenate 'string (symbol-name constname) "-DEF")
           constname))))
    `(with-output :off :all :on (error)
      (encapsulate nil
        (local (progn (in-theory '((:definition hons-copy)))
            (defun defined-const-memoize-fn1
              nil
              (declare (xargs :verify-guards nil))
              ,TERM)
            (in-theory (disable (defined-const-memoize-fn1)))
            (defun defined-const-memoize-fn
              nil
              (declare (xargs :guard t))
              ,(IF HONS
     '(HONS-COPY (EC-CALL (DEFINED-CONST-MEMOIZE-FN1)))
     '(EC-CALL (DEFINED-CONST-MEMOIZE-FN1))))
            (defthm defined-const-memoize-fn-is-term
              (equal ,TERM (defined-const-memoize-fn))
              :hints (("goal" :in-theory (disable (defined-const-memoize-fn))))
              :rule-classes nil)
            (memoize 'defined-const-memoize-fn)))
        (make-event `(make-event (let ((val ,(IF (EQ
      (GETPROP 'DEFINED-CONST-MEMOIZE-FN 'FORMALS 'NONE 'CURRENT-ACL2-WORLD
               (W STATE))
      'NONE)
     ',TERM
     '(DEFINED-CONST-MEMOIZE-FN))))
              `(progn (with-output :stack :pop (defconst ,',',CONSTNAME
                    ,,,(IF HONS
       ```(HONS-COPY ',VAL)
       ```',VAL)))
                (with-output :stack :pop (defthm ,',',THMNAME
                    (equal ,',',TERM ,',',CONSTNAME)
                    :hints (("goal" :use defined-const-memoize-fn-is-term))
                    :rule-classes ,',',RULE-CLASSES))
                (with-output :stack :pop (table defined-const-table ',',',CONSTNAME ',',',THMNAME))
                ,@(AND ,,EVISC
       `((WITH-OUTPUT :STACK :POP
                      (TABLE EVISC-TABLE ,',',CONSTNAME
                             ,(LET ((NAME (SYMBOL-NAME ',',CONSTNAME)))
                                (IF (MAY-NEED-SLASHES NAME)
                                    (CONCATENATE 'STRING "#.|" NAME "|")
                                    (CONCATENATE 'STRING "#." NAME)))))))
                ,@(AND ,,HONS
       `((WITH-OUTPUT :STACK :POP
                      (TABLE PERSISTENT-HONS-TABLE ,',',CONSTNAME T))))))))))))