		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Get-theorem

Find the theorem with a given name in a list of top-level constructs.

Signature
(get-theorem name tops) → thm?
Arguments: name — Guard (identifierp name).; tops — Guard (toplevel-listp tops).
Returns: thm? — Type (maybe-theoremp thm?).

We return nil if the specification is not found.

Definitions and Theorems

Function: get-theorem

(defun get-theorem (name tops)
  (declare (xargs :guard (and (identifierp name)
                              (toplevel-listp tops))))
  (let ((__function__ 'get-theorem))
    (declare (ignorable __function__))
    (b* (((when (endp tops)) nil)
         (top (car tops)))
      (toplevel-case
           top :type (get-theorem name (cdr tops))
           :types (get-theorem name (cdr tops))
           :function (get-theorem name (cdr tops))
           :functions (get-theorem name (cdr tops))
           :specification
           (get-theorem name (cdr tops))
           :theorem
           (if (identifier-equiv name (theorem->name top.get))
               top.get
             (get-theorem name (cdr tops)))
           :transform (get-theorem name (cdr tops))))))

Theorem: maybe-theoremp-of-get-theorem

(defthm maybe-theoremp-of-get-theorem
  (b* ((thm? (get-theorem name tops)))
    (maybe-theoremp thm?))
  :rule-classes :rewrite)

Theorem: get-theorem-of-identifier-fix-name

(defthm get-theorem-of-identifier-fix-name
  (equal (get-theorem (identifier-fix name) tops)
         (get-theorem name tops)))

Theorem: get-theorem-identifier-equiv-congruence-on-name

(defthm get-theorem-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (get-theorem name tops)
                  (get-theorem name-equiv tops)))
  :rule-classes :congruence)

Theorem: get-theorem-of-toplevel-list-fix-tops

(defthm get-theorem-of-toplevel-list-fix-tops
  (equal (get-theorem name (toplevel-list-fix tops))
         (get-theorem name tops)))

Theorem: get-theorem-toplevel-list-equiv-congruence-on-tops

(defthm get-theorem-toplevel-list-equiv-congruence-on-tops
  (implies (toplevel-list-equiv tops tops-equiv)
           (equal (get-theorem name tops)
                  (get-theorem name tops-equiv)))
  :rule-classes :congruence)