• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
        • Soft-future-work
        • Soft-macros
        • Updates-to-workshop-material
        • Soft-implementation
          • Soft-implementation-core
          • Gen-macro2-of-macro
          • Defun-inst-implementation
          • Defthm-inst-implementation
            • Defthm-inst-fn
            • Check-sothm-inst
            • Show-defthm-inst
            • Defthm-inst-macro-definition
          • Defsoft-implementation
          • Defunvar-implementation
          • Defund-sk2-implementation
          • Defun-sk2-implementation
          • Define-sk2-implementation
          • Defchoose2-implementation
          • Defund2-implementation
          • Defun2-implementation
          • Define2-implementation
        • Soft-notions
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• 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))))