• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
      • Fresh-logical-name-with-$s-suffix
      • Irrelevant-formals-info
      • Std/system/function-queries
      • Std/system/term-queries
      • Std/system/term-transformations
      • Std/system/enhanced-utilities
      • Install-not-normalized-event
      • Install-not-normalized-event-lst
      • Std/system/term-function-recognizers
      • Genvar$
      • Std/system/event-name-queries
      • Pseudo-tests-and-call-listp
      • Maybe-pseudo-event-formp
      • Add-suffix-to-fn-or-const
      • Chk-irrelevant-formals-ok
      • Table-alist+
      • Pseudo-tests-and-callp
      • Add-suffix-to-fn-or-const-lst
      • Known-packages+
      • Add-suffix-to-fn-lst
      • Unquote-term
      • Event-landmark-names
      • Add-suffix-lst
      • Std/system/theorem-queries
        • Thm-formula
        • Classes+
        • Thm-formula+
        • Guard-verified-p+
        • Guard-verified-p
        • Classes
      • Unquote-term-list
      • Std/system/macro-queries
      • Pseudo-command-landmark-listp
      • Install-not-normalized$
      • Pseudo-event-landmark-listp
      • Known-packages
      • Std/system/partition-rest-and-keyword-args
      • Rune-enabledp
      • Rune-disabledp
      • Included-books
      • Std/system/pseudo-event-formp
      • Std/system/plist-worldp-with-formals
      • Std/system/w
      • Std/system/geprops
      • Std/system/arglistp
      • Std/system/constant-queries
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/system/theorem-queries

Thm-formula+

Enhanced variant of thm-formula.

Signature

(thm-formula+ thm wrld) → formula

Arguments

thm — Guard (symbolp thm).

wrld — Guard (plist-worldp wrld).

Returns

formula — Type (pseudo-termp formula).

This returns the same result as thm-formula, but it includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a theorem.

Definitions and Theorems

Function: thm-formula+

(defun thm-formula+ (thm wrld)
 (declare (xargs :guard (and (symbolp thm)
                             (plist-worldp wrld))))
 (let ((__function__ 'thm-formula+))
  (declare (ignorable __function__))
  (if (not (theorem-symbolp thm wrld))
      (raise "The symbol ~x0 does not name a theorem."
             thm)
   (b* ((result (thm-formula thm wrld)))
    (if (pseudo-termp result)
        result
     (raise
      "Internal error: ~
                the FORMULA property ~x0 of ~x1 is not a pseudo-term."
      result thm))))))

Theorem: pseudo-termp-of-thm-formula+

(defthm pseudo-termp-of-thm-formula+
  (b* ((formula (thm-formula+ thm wrld)))
    (pseudo-termp formula))
  :rule-classes :rewrite)