		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-fresh-defiso-thm-names

Return fresh defiso theorem names.

Signature
(isodata-fresh-defiso-thm-names isoname verify-guards$ names-to-avoid wrld) → (mv forth-image back-image back-of-forth forth-of-back oldp-guard newp-guard forth-guard back-guard forth-injective back-injective updated-names-to-avoid)
Arguments: isoname — Guard (symbolp isoname).; 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.; forth-of-back — A symbolp.; oldp-guard — A symbolp.; newp-guard — A symbolp.; forth-guard — A symbolp.; back-guard — A symbolp.; forth-injective — A symbolp.; back-injective — A symbolp.; updated-names-to-avoid — A symbol-listp.

These are used as the :thm-names input of a defiso that isodata generates locally, when the iso input is not a name.

In order for the generated defiso 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 defiso name (which is generated by isodata-fresh-defiso-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: isodata-fresh-defiso-thm-names

(defun isodata-fresh-defiso-thm-names
       (isoname verify-guards$ names-to-avoid wrld)
  (declare (xargs :guard (and (symbolp isoname)
                              (booleanp verify-guards$)
                              (symbol-listp names-to-avoid)
                              (plist-worldp wrld))))
  (let ((__function__ 'isodata-fresh-defiso-thm-names))
    (declare (ignorable __function__))
    (b* ((prefix (add-suffix isoname "-"))
         ((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 forth-of-back names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :alpha-of-beta))
               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 back-injective names-to-avoid)
          (fresh-logical-name-with-$s-suffix
               (add-suffix prefix (symbol-name :beta-injective))
               nil names-to-avoid wrld)))
      (mv forth-image back-image back-of-forth
          forth-of-back oldp-guard newp-guard
          forth-guard back-guard forth-injective
          back-injective names-to-avoid))))