		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gen-thm-name

Generate a theorem name.

Signature
(gen-thm-name const-new thm-index) → (mv name updated-thm-index)
Arguments: const-new — Guard (symbolp const-new).; thm-index — Guard (posp thm-index).
Returns: name — Type (symbolp name).; updated-thm-index — Type (posp updated-thm-index).

This is formed from the name of the constant for the new code and an increasing index. This function also increases and return the index.

For greater robustness, this function should ensure that the theorem name is not already present in the ACL2 works, and is not already present in a list of names to avoid; the latter list would consist of names that have been already used for generating events that have not been submitted to ACL2 yet (e.g. theorem names from a tool used before this transformation). But for now we do not perform these checks, since they are unlikely to fail anyhow. Note that, due to the increasing indices, we would not use the list of names to avoid for the theorems generated by this transformation.

Definitions and Theorems

Function: gen-thm-name

(defun gen-thm-name (const-new thm-index)
  (declare (xargs :guard (and (symbolp const-new)
                              (posp thm-index))))
  (let ((__function__ 'gen-thm-name))
    (declare (ignorable __function__))
    (b* ((name (packn-pos (list const-new '-thm- thm-index)
                          const-new))
         (thm-index (1+ (pos-fix thm-index))))
      (mv name thm-index))))

Theorem: symbolp-of-gen-thm-name.name

(defthm symbolp-of-gen-thm-name.name
  (b* (((mv ?name ?updated-thm-index)
        (gen-thm-name const-new thm-index)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: posp-of-gen-thm-name.updated-thm-index

(defthm posp-of-gen-thm-name.updated-thm-index
  (b* (((mv ?name ?updated-thm-index)
        (gen-thm-name const-new thm-index)))
    (posp updated-thm-index))
  :rule-classes :rewrite)