		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-fresh-defsurj-thm-names

Return fresh defsurj theorem names.

Signature
(expdata-fresh-defsurj-thm-names surjname verify-guards$ names-to-avoid wrld) → (mv forth-image back-image back-of-forth oldp-guard newp-guard forth-guard back-guard forth-injective updated-names-to-avoid)
Arguments: surjname — Guard (symbolp surjname).; verify-guards$ — Guard (booleanp verify-guards$).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: forth-image — A symbolp.; back-image — A symbolp.; back-of-forth — A symbolp.; oldp-guard — A symbolp.; newp-guard — A symbolp.; forth-guard — A symbolp.; back-guard — A symbolp.; forth-injective — A symbolp.; updated-names-to-avoid — A symbol-listp.

These are used as the :thm-names input of a defsurj that expdata generates locally, when the surj input is not a name.

In order for the generated defsurj to succeed, we supply explicit fresh theorem names to use. These are returned by this function.

We append the keyword (without colon) that denotes the theorem at the end of the defsurj name (which is generated by expdata-fresh-defsurj-name-with-*s-suffix, and add enough $ characters, if needed, to make them fresh. We expect that adding $ characters will rarely be necessary.

The names of the guard-related theorems are nil if guards must not be verified, since those theorems are not generated or used in that case.

Definitions and Theorems

Function: expdata-fresh-defsurj-thm-names

(defun expdata-fresh-defsurj-thm-names
       (surjname verify-guards$ names-to-avoid wrld)
  (declare (xargs :guard (and (symbolp surjname)
                              (booleanp verify-guards$)
                              (symbol-listp names-to-avoid)
                              (plist-worldp wrld))))
  (let ((__function__ 'expdata-fresh-defsurj-thm-names))
    (declare (ignorable __function__))
    (b* ((prefix (add-suffix surjname "-"))
         ((mv forth-image names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :alpha-image))
               nil names-to-avoid wrld))
         ((mv back-image names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :beta-image))
               nil names-to-avoid wrld))
         ((mv back-of-forth names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :beta-of-alpha))
               nil names-to-avoid wrld))
         ((mv oldp-guard names-to-avoid)
          (if verify-guards$
              (fresh-logical-name-with-$s-suffix
                   (add-suffix prefix (symbol-name :doma-guard))
                   nil names-to-avoid wrld)
            (mv nil names-to-avoid)))
         ((mv newp-guard names-to-avoid)
          (if verify-guards$
              (fresh-logical-name-with-$s-suffix
                   (add-suffix prefix (symbol-name :domb-guard))
                   nil names-to-avoid wrld)
            (mv nil names-to-avoid)))
         ((mv forth-guard names-to-avoid)
          (if verify-guards$
              (fresh-logical-name-with-$s-suffix
                   (add-suffix prefix (symbol-name :alpha-guard))
                   nil names-to-avoid wrld)
            (mv nil names-to-avoid)))
         ((mv back-guard names-to-avoid)
          (if verify-guards$
              (fresh-logical-name-with-$s-suffix
                   (add-suffix prefix (symbol-name :beta-guard))
                   nil names-to-avoid wrld)
            (mv nil names-to-avoid)))
         ((mv forth-injective names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :alpha-injective))
               nil names-to-avoid wrld)))
      (mv forth-image
          back-image back-of-forth oldp-guard
          newp-guard forth-guard back-guard
          forth-injective names-to-avoid))))