		Search-engine friendly clone of the ACL2 documentation.

Defthm-inst-implementation

Defthm-inst-fn

Validate some of the inputs to defthm-inst and generate the event form to submit.

Signature
(defthm-inst-fn thm sothm-inst options ctx state) → (mv erp event state)
Arguments: ctx — Context for errors.
Returns: erp — booleanp flag of the error triple.; event — A maybe-pseudo-event-formp.

We directly check all the inputs except for the :rule-classes option, relying on defthm to check it.

Definitions and Theorems

Function: defthm-inst-fn

(defun defthm-inst-fn (thm sothm-inst options ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defthm-inst-fn))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (symbolp thm))
     (er-soft+ ctx t nil
               "The first input must be a symbol, but ~x0 is not."
               thm))
    ((unless (check-sothm-inst sothm-inst wrld))
     (er-soft+
      ctx t nil
      "The second input must be ~
                   the name of a second-order theorem ~
                   followed by the pairs of an instantiation, ~
                   but ~x0 is not."
      sothm-inst))
    (sothm (car sothm-inst))
    (inst (cdr sothm-inst))
    ((unless (subsetp (alist-keys inst)
                      (funvars-of-thm sothm wrld)))
     (er-soft+
      ctx t nil
      "Each function variable key of ~x0 must be ~
                   among function variable that ~x1 depends on."
      inst sothm))
    ((unless (keyword-value-listp options))
     (er-soft+
      ctx t nil
      "The inputs after the second input ~
                   must be a keyword-value list, ~
                   but ~x0 is not."
      options))
    (keywords (evens options))
    ((unless (no-duplicatesp keywords))
     (er-soft+ ctx t nil
               "The inputs keywords must be unique."))
    ((unless (subsetp keywords
                      '(:rule-classes :enable :print)))
     (er-soft+
      ctx t nil
      "Only the input keywords ~
                   :RULE-CLASSES, :ENABLE, and :PRINT are allowed."))
    (print-pair (assoc-keyword :print options))
    (print (if print-pair (cadr print-pair)
             :result))
    ((unless (member-eq print '(nil :all :result)))
     (er-soft+
      ctx t nil
      "The :PRINT input must be NIL, :ALL, or :RESULT, ~
                   but ~x0 is not."
      print))
    (options (remove-keyword :print options))
    (enable-pair (assoc-keyword :enable options))
    (enable (if enable-pair (cadr enable-pair) t))
    ((unless (booleanp enable))
     (er-soft+
      ctx t nil
      "The :ENABLE input must be T or NIL, ~
                   but it is ~x0 instead."
      enable))
    (options (remove-keyword :enable options))
    (sothm-formula (formula sothm nil wrld))
    (thm-formula (fun-subst-term inst sothm-formula wrld))
    (thm-formula (untranslate thm-formula t wrld))
    (fsbs (ext-fun-subst-term sothm-formula inst wrld))
    (thm-proof (sothm-inst-proof sothm fsbs wrld))
    (macro (if enable 'defthm 'defthmd))
    (defthm-event (cons macro
                        (cons thm
                              (cons thm-formula
                                    (append thm-proof options)))))
    (defthm-event-without-proof
         (cons macro
               (cons thm (cons thm-formula options))))
    (return-value-event (cons 'value-triple
                              (cons (cons 'quote (cons thm 'nil))
                                    'nil)))
    (event
     (cond
      ((eq print nil)
       (cons 'progn
             (cons defthm-event
                   (cons return-value-event 'nil))))
      ((eq print :all)
       (restore-output
            (cons 'progn
                  (cons defthm-event
                        (cons return-value-event 'nil)))))
      ((eq print :result)
       (cons
        'progn
        (cons
         defthm-event
         (cons
          (cons
           'cw-event
           (cons '"~x0~|"
                 (cons (cons 'quote
                             (cons defthm-event-without-proof 'nil))
                       'nil)))
          (cons return-value-event 'nil)))))
      (t (impossible)))))
   (value event))))