		Search-engine friendly clone of the ACL2 documentation.

Fresh-ident-utility

Fresh-ident

Signature
(fresh-ident ident blacklist &key (force-suffix 'nil) (number-prefix '"_") (number-suffix '"")) → ident$
Arguments: ident — Guard (identp ident).; blacklist — Guard (ident-setp blacklist).; force-suffix — Guard (booleanp force-suffix).; number-prefix — Guard (stringp number-prefix).; number-suffix — Guard (stringp number-suffix).
Returns: ident$ — Type (identp ident$).

Definitions and Theorems

Function: fresh-ident-fn

(defun fresh-ident-fn (ident blacklist force-suffix
                             number-prefix number-suffix)
 (declare (xargs :guard (and (identp ident)
                             (ident-setp blacklist)
                             (booleanp force-suffix)
                             (stringp number-prefix)
                             (stringp number-suffix))))
 (let ((__function__ 'fresh-ident))
  (declare (ignorable __function__))
  (b* ((ident-string (ident->unwrap ident))
       ((unless (stringp ident-string))
        (raise "Identifier ~x0 does not contain a string."
               ident)
        (c$::irr-ident))
       (string-blacklist (map-ident->unwrap blacklist)))
    (ident (fresh-string-wrt ident-string force-suffix number-prefix
                             number-suffix string-blacklist)))))

Theorem: identp-of-fresh-ident

(defthm identp-of-fresh-ident
  (b* ((ident$ (fresh-ident-fn ident blacklist force-suffix
                               number-prefix number-suffix)))
    (identp ident$))
  :rule-classes :rewrite)

Theorem: fresh-ident-fn-of-ident-fix-ident

(defthm fresh-ident-fn-of-ident-fix-ident
  (equal (fresh-ident-fn (ident-fix ident)
                         blacklist force-suffix
                         number-prefix number-suffix)
         (fresh-ident-fn ident blacklist force-suffix
                         number-prefix number-suffix)))

Theorem: fresh-ident-fn-ident-equiv-congruence-on-ident

(defthm fresh-ident-fn-ident-equiv-congruence-on-ident
  (implies (c$::ident-equiv ident ident-equiv)
           (equal (fresh-ident-fn ident blacklist force-suffix
                                  number-prefix number-suffix)
                  (fresh-ident-fn ident-equiv blacklist force-suffix
                                  number-prefix number-suffix)))
  :rule-classes :congruence)

Theorem: fresh-ident-fn-of-ident-set-fix-blacklist

(defthm fresh-ident-fn-of-ident-set-fix-blacklist
  (equal (fresh-ident-fn ident (ident-set-fix blacklist)
                         force-suffix
                         number-prefix number-suffix)
         (fresh-ident-fn ident blacklist force-suffix
                         number-prefix number-suffix)))

Theorem: fresh-ident-fn-ident-set-equiv-congruence-on-blacklist

(defthm fresh-ident-fn-ident-set-equiv-congruence-on-blacklist
  (implies (c$::ident-set-equiv blacklist blacklist-equiv)
           (equal (fresh-ident-fn ident blacklist force-suffix
                                  number-prefix number-suffix)
                  (fresh-ident-fn ident blacklist-equiv force-suffix
                                  number-prefix number-suffix)))
  :rule-classes :congruence)

Theorem: fresh-ident-fn-of-bool-fix-force-suffix

(defthm fresh-ident-fn-of-bool-fix-force-suffix
  (equal (fresh-ident-fn ident
                         blacklist (acl2::bool-fix force-suffix)
                         number-prefix number-suffix)
         (fresh-ident-fn ident blacklist force-suffix
                         number-prefix number-suffix)))

Theorem: fresh-ident-fn-iff-congruence-on-force-suffix

(defthm fresh-ident-fn-iff-congruence-on-force-suffix
  (implies (iff force-suffix force-suffix-equiv)
           (equal (fresh-ident-fn ident blacklist force-suffix
                                  number-prefix number-suffix)
                  (fresh-ident-fn ident blacklist force-suffix-equiv
                                  number-prefix number-suffix)))
  :rule-classes :congruence)

Theorem: fresh-ident-fn-of-str-fix-number-prefix

(defthm fresh-ident-fn-of-str-fix-number-prefix
  (equal (fresh-ident-fn ident blacklist force-suffix
                         (acl2::str-fix number-prefix)
                         number-suffix)
         (fresh-ident-fn ident blacklist force-suffix
                         number-prefix number-suffix)))

Theorem: fresh-ident-fn-streqv-congruence-on-number-prefix

(defthm fresh-ident-fn-streqv-congruence-on-number-prefix
  (implies
       (acl2::streqv number-prefix number-prefix-equiv)
       (equal (fresh-ident-fn ident blacklist force-suffix
                              number-prefix number-suffix)
              (fresh-ident-fn ident blacklist force-suffix
                              number-prefix-equiv number-suffix)))
  :rule-classes :congruence)

Theorem: fresh-ident-fn-of-str-fix-number-suffix

(defthm fresh-ident-fn-of-str-fix-number-suffix
  (equal (fresh-ident-fn ident
                         blacklist force-suffix number-prefix
                         (acl2::str-fix number-suffix))
         (fresh-ident-fn ident blacklist force-suffix
                         number-prefix number-suffix)))

Theorem: fresh-ident-fn-streqv-congruence-on-number-suffix

(defthm fresh-ident-fn-streqv-congruence-on-number-suffix
  (implies
       (acl2::streqv number-suffix number-suffix-equiv)
       (equal (fresh-ident-fn ident blacklist force-suffix
                              number-prefix number-suffix)
              (fresh-ident-fn ident blacklist force-suffix
                              number-prefix number-suffix-equiv)))
  :rule-classes :congruence)