		Search-engine friendly clone of the ACL2 documentation.

Z3-py

Smt-names

SMT-names generates SMT solver friendly names.

Definitions and Theorems

Function: character-fix

(defun character-fix (x)
  (declare (xargs :guard (characterp x)))
  (let ((acl2::__function__ 'character-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic (if (characterp x) x (code-char 0))
         :exec x)))

Theorem: character-fix-idempotent-lemma

(defthm character-fix-idempotent-lemma
  (equal (character-fix (character-fix x))
         (character-fix x)))

Function: character-equiv$inline

(defun character-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (characterp acl2::x)
                              (characterp acl2::y))))
  (equal (character-fix acl2::x)
         (character-fix acl2::y)))

Theorem: character-equiv-is-an-equivalence

(defthm character-equiv-is-an-equivalence
  (and (booleanp (character-equiv x y))
       (character-equiv x x)
       (implies (character-equiv x y)
                (character-equiv y x))
       (implies (and (character-equiv x y)
                     (character-equiv y z))
                (character-equiv x z)))
  :rule-classes (:equivalence))

Theorem: character-equiv-implies-equal-character-fix-1

(defthm character-equiv-implies-equal-character-fix-1
  (implies (character-equiv acl2::x x-equiv)
           (equal (character-fix acl2::x)
                  (character-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: character-fix-under-character-equiv

(defthm character-fix-under-character-equiv
  (character-equiv (character-fix acl2::x)
                   acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: special-char-alistp

(defun special-char-alistp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'special-char-alistp))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        t
      (and (consp (car x))
           (characterp (caar x))
           (character-listp (cdar x))
           (special-char-alistp (cdr x))))))

Theorem: special-char-alistp-of-revappend

(defthm special-char-alistp-of-revappend
  (equal (special-char-alistp (revappend acl2::x acl2::y))
         (and (special-char-alistp (acl2::list-fix acl2::x))
              (special-char-alistp acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-remove

(defthm special-char-alistp-of-remove
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-last

(defthm special-char-alistp-of-last
  (implies (special-char-alistp (double-rewrite acl2::x))
           (special-char-alistp (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-nthcdr

(defthm special-char-alistp-of-nthcdr
  (implies (special-char-alistp (double-rewrite acl2::x))
           (special-char-alistp (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-butlast

(defthm special-char-alistp-of-butlast
  (implies (special-char-alistp (double-rewrite acl2::x))
           (special-char-alistp (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-update-nth

(defthm special-char-alistp-of-update-nth
 (implies
     (special-char-alistp (double-rewrite acl2::x))
     (iff (special-char-alistp (update-nth acl2::n acl2::y acl2::x))
          (and (and (consp acl2::y)
                    (characterp (car acl2::y))
                    (character-listp (cdr acl2::y)))
               (or (<= (nfix acl2::n) (len acl2::x))
                   (and (consp nil)
                        (characterp (car nil))
                        (character-listp (cdr nil)))))))
 :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-repeat

(defthm special-char-alistp-of-repeat
  (iff (special-char-alistp (acl2::repeat acl2::n acl2::x))
       (or (and (consp acl2::x)
                (characterp (car acl2::x))
                (character-listp (cdr acl2::x)))
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-take

(defthm special-char-alistp-of-take
  (implies (special-char-alistp (double-rewrite acl2::x))
           (iff (special-char-alistp (take acl2::n acl2::x))
                (or (and (consp nil)
                         (characterp (car nil))
                         (character-listp (cdr nil)))
                    (<= (nfix acl2::n) (len acl2::x)))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-union-equal

(defthm special-char-alistp-of-union-equal
  (equal (special-char-alistp (union-equal acl2::x acl2::y))
         (and (special-char-alistp (acl2::list-fix acl2::x))
              (special-char-alistp (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-intersection-equal-2

(defthm special-char-alistp-of-intersection-equal-2
  (implies
       (special-char-alistp (double-rewrite acl2::y))
       (special-char-alistp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-intersection-equal-1

(defthm special-char-alistp-of-intersection-equal-1
  (implies
       (special-char-alistp (double-rewrite acl2::x))
       (special-char-alistp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-set-difference-equal

(defthm special-char-alistp-of-set-difference-equal
  (implies
       (special-char-alistp acl2::x)
       (special-char-alistp (set-difference-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-set-equiv-congruence

(defthm special-char-alistp-set-equiv-congruence
  (implies (acl2::set-equiv acl2::x acl2::y)
           (equal (special-char-alistp acl2::x)
                  (special-char-alistp acl2::y)))
  :rule-classes :congruence)

Theorem: special-char-alistp-when-subsetp-equal

(defthm special-char-alistp-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (special-char-alistp acl2::y))
                (special-char-alistp acl2::x))
       (implies (and (special-char-alistp acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (special-char-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-rcons

(defthm special-char-alistp-of-rcons
  (iff (special-char-alistp (acl2::rcons acl2::a acl2::x))
       (and (and (consp acl2::a)
                 (characterp (car acl2::a))
                 (character-listp (cdr acl2::a)))
            (special-char-alistp (acl2::list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-rev

(defthm special-char-alistp-of-rev
  (equal (special-char-alistp (acl2::rev acl2::x))
         (special-char-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-duplicated-members

(defthm special-char-alistp-of-duplicated-members
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (acl2::duplicated-members acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-difference

(defthm special-char-alistp-of-difference
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (set::difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-intersect-2

(defthm special-char-alistp-of-intersect-2
  (implies (special-char-alistp acl2::y)
           (special-char-alistp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-intersect-1

(defthm special-char-alistp-of-intersect-1
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-union

(defthm special-char-alistp-of-union
  (iff (special-char-alistp (set::union acl2::x acl2::y))
       (and (special-char-alistp (set::sfix acl2::x))
            (special-char-alistp (set::sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-mergesort

(defthm special-char-alistp-of-mergesort
  (iff (special-char-alistp (set::mergesort acl2::x))
       (special-char-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-delete

(defthm special-char-alistp-of-delete
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (set::delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-insert

(defthm special-char-alistp-of-insert
  (iff (special-char-alistp (set::insert acl2::a acl2::x))
       (and (special-char-alistp (set::sfix acl2::x))
            (and (consp acl2::a)
                 (characterp (car acl2::a))
                 (character-listp (cdr acl2::a)))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-sfix

(defthm special-char-alistp-of-sfix
  (iff (special-char-alistp (set::sfix acl2::x))
       (or (special-char-alistp acl2::x)
           (not (set::setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-list-fix

(defthm special-char-alistp-of-list-fix
  (equal (special-char-alistp (acl2::list-fix acl2::x))
         (special-char-alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-append

(defthm special-char-alistp-of-append
  (equal (special-char-alistp (append acl2::a acl2::b))
         (and (special-char-alistp acl2::a)
              (special-char-alistp acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-when-not-consp

(defthm special-char-alistp-when-not-consp
  (implies (not (consp acl2::x))
           (special-char-alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-cdr-when-special-char-alistp

(defthm special-char-alistp-of-cdr-when-special-char-alistp
  (implies (special-char-alistp (double-rewrite acl2::x))
           (special-char-alistp (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-cons

(defthm special-char-alistp-of-cons
  (equal (special-char-alistp (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (characterp (car acl2::a))
                   (character-listp (cdr acl2::a)))
              (special-char-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-fast-alist-clean

(defthm special-char-alistp-of-fast-alist-clean
  (implies (special-char-alistp acl2::x)
           (special-char-alistp (fast-alist-clean acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-hons-shrink-alist

(defthm special-char-alistp-of-hons-shrink-alist
 (implies (and (special-char-alistp acl2::x)
               (special-char-alistp acl2::y))
          (special-char-alistp (hons-shrink-alist acl2::x acl2::y)))
 :rule-classes ((:rewrite)))

Theorem: special-char-alistp-of-hons-acons

(defthm special-char-alistp-of-hons-acons
  (equal (special-char-alistp (hons-acons acl2::a acl2::n acl2::x))
         (and (characterp acl2::a)
              (character-listp acl2::n)
              (special-char-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: character-listp-of-cdr-of-hons-assoc-equal-when-special-char-alistp

(defthm
 character-listp-of-cdr-of-hons-assoc-equal-when-special-char-alistp
 (implies
     (special-char-alistp acl2::x)
     (iff (character-listp (cdr (hons-assoc-equal acl2::k acl2::x)))
          (or (hons-assoc-equal acl2::k acl2::x)
              (character-listp nil))))
 :rule-classes ((:rewrite)))

Theorem: character-listp-of-cdar-when-special-char-alistp

(defthm character-listp-of-cdar-when-special-char-alistp
  (implies (special-char-alistp acl2::x)
           (iff (character-listp (cdar acl2::x))
                (or (consp acl2::x)
                    (character-listp nil))))
  :rule-classes ((:rewrite)))

Theorem: characterp-of-caar-when-special-char-alistp

(defthm characterp-of-caar-when-special-char-alistp
  (implies (special-char-alistp acl2::x)
           (iff (characterp (caar acl2::x))
                (or (consp acl2::x) (characterp nil))))
  :rule-classes ((:rewrite)))

Function: special-char-alist-fix$inline

(defun special-char-alist-fix$inline (x)
  (declare (xargs :guard (special-char-alistp x)))
  (let ((acl2::__function__ 'special-char-alist-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             x
           (if (consp (car x))
               (cons (cons (character-fix (caar x))
                           (make-character-list (cdar x)))
                     (special-char-alist-fix (cdr x)))
             (special-char-alist-fix (cdr x))))
         :exec x)))

Theorem: special-char-alistp-of-special-char-alist-fix

(defthm special-char-alistp-of-special-char-alist-fix
  (b* ((fty::newx (special-char-alist-fix$inline x)))
    (special-char-alistp fty::newx))
  :rule-classes :rewrite)

Theorem: special-char-alist-fix-when-special-char-alistp

(defthm special-char-alist-fix-when-special-char-alistp
  (implies (special-char-alistp x)
           (equal (special-char-alist-fix x) x)))

Function: special-char-alist-equiv$inline

(defun special-char-alist-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (special-char-alistp acl2::x)
                              (special-char-alistp acl2::y))))
  (equal (special-char-alist-fix acl2::x)
         (special-char-alist-fix acl2::y)))

Theorem: special-char-alist-equiv-is-an-equivalence

(defthm special-char-alist-equiv-is-an-equivalence
  (and (booleanp (special-char-alist-equiv x y))
       (special-char-alist-equiv x x)
       (implies (special-char-alist-equiv x y)
                (special-char-alist-equiv y x))
       (implies (and (special-char-alist-equiv x y)
                     (special-char-alist-equiv y z))
                (special-char-alist-equiv x z)))
  :rule-classes (:equivalence))

Theorem: special-char-alist-equiv-implies-equal-special-char-alist-fix-1

(defthm
    special-char-alist-equiv-implies-equal-special-char-alist-fix-1
  (implies (special-char-alist-equiv acl2::x x-equiv)
           (equal (special-char-alist-fix acl2::x)
                  (special-char-alist-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: special-char-alist-fix-under-special-char-alist-equiv

(defthm special-char-alist-fix-under-special-char-alist-equiv
  (special-char-alist-equiv (special-char-alist-fix acl2::x)
                            acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-special-char-alist-fix-1-forward-to-special-char-alist-equiv

(defthm
 equal-of-special-char-alist-fix-1-forward-to-special-char-alist-equiv
 (implies (equal (special-char-alist-fix acl2::x)
                 acl2::y)
          (special-char-alist-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: equal-of-special-char-alist-fix-2-forward-to-special-char-alist-equiv

(defthm
 equal-of-special-char-alist-fix-2-forward-to-special-char-alist-equiv
 (implies (equal acl2::x
                 (special-char-alist-fix acl2::y))
          (special-char-alist-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: special-char-alist-equiv-of-special-char-alist-fix-1-forward

(defthm special-char-alist-equiv-of-special-char-alist-fix-1-forward
 (implies (special-char-alist-equiv (special-char-alist-fix acl2::x)
                                    acl2::y)
          (special-char-alist-equiv acl2::x acl2::y))
 :rule-classes :forward-chaining)

Theorem: special-char-alist-equiv-of-special-char-alist-fix-2-forward

(defthm special-char-alist-equiv-of-special-char-alist-fix-2-forward
  (implies
       (special-char-alist-equiv acl2::x
                                 (special-char-alist-fix acl2::y))
       (special-char-alist-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: cons-of-character-fix-k-under-special-char-alist-equiv

(defthm cons-of-character-fix-k-under-special-char-alist-equiv
  (special-char-alist-equiv
       (cons (cons (character-fix acl2::k) acl2::v)
             acl2::x)
       (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-character-equiv-congruence-on-k-under-special-char-alist-equiv

(defthm
 cons-character-equiv-congruence-on-k-under-special-char-alist-equiv
 (implies
   (character-equiv acl2::k k-equiv)
   (special-char-alist-equiv (cons (cons acl2::k acl2::v) acl2::x)
                             (cons (cons k-equiv acl2::v) acl2::x)))
 :rule-classes :congruence)

Theorem: cons-of-make-character-list-v-under-special-char-alist-equiv

(defthm cons-of-make-character-list-v-under-special-char-alist-equiv
  (special-char-alist-equiv
       (cons (cons acl2::k (make-character-list acl2::v))
             acl2::x)
       (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-charlisteqv-congruence-on-v-under-special-char-alist-equiv

(defthm
    cons-charlisteqv-congruence-on-v-under-special-char-alist-equiv
 (implies
   (charlisteqv acl2::v v-equiv)
   (special-char-alist-equiv (cons (cons acl2::k acl2::v) acl2::x)
                             (cons (cons acl2::k v-equiv) acl2::x)))
 :rule-classes :congruence)

Theorem: cons-of-special-char-alist-fix-y-under-special-char-alist-equiv

(defthm
    cons-of-special-char-alist-fix-y-under-special-char-alist-equiv
  (special-char-alist-equiv (cons acl2::x
                                  (special-char-alist-fix acl2::y))
                            (cons acl2::x acl2::y)))

Theorem: cons-special-char-alist-equiv-congruence-on-y-under-special-char-alist-equiv

(defthm
 cons-special-char-alist-equiv-congruence-on-y-under-special-char-alist-equiv
 (implies (special-char-alist-equiv acl2::y y-equiv)
          (special-char-alist-equiv (cons acl2::x acl2::y)
                                    (cons acl2::x y-equiv)))
 :rule-classes :congruence)

Theorem: special-char-alist-fix-of-acons

(defthm special-char-alist-fix-of-acons
  (equal (special-char-alist-fix (cons (cons acl2::a acl2::b) x))
         (cons (cons (character-fix acl2::a)
                     (make-character-list acl2::b))
               (special-char-alist-fix x))))

Theorem: special-char-alist-fix-of-append

(defthm special-char-alist-fix-of-append
  (equal (special-char-alist-fix (append std::a std::b))
         (append (special-char-alist-fix std::a)
                 (special-char-alist-fix std::b))))

Theorem: consp-car-of-special-char-alist-fix

(defthm consp-car-of-special-char-alist-fix
  (equal (consp (car (special-char-alist-fix x)))
         (consp (special-char-alist-fix x))))

Function: special-list

(defun special-list nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'special-list))
    (declare (ignorable acl2::__function__))
    '((#\_ #\_ #\u #\s #\c #\_)
      (#\- #\_ #\s #\u #\b #\_)
      (#\+ #\_ #\a #\d #\d #\_)
      (#\* #\_ #\m #\l #\t #\_)
      (#\/ #\_ #\d #\i #\v #\_)
      (#\< #\_ #\l #\t #\_)
      (#\> #\_ #\g #\t #\_)
      (#\= #\_ #\e #\q #\l #\_)
      (#\! #\_ #\e #\x #\c #\_)
      (#\@ #\_ #\a #\t #\_)
      (#\# #\_ #\h #\s #\h #\_)
      (#\$ #\_ #\d #\l #\r #\_)
      (#\% #\_ #\p #\c #\t #\_)
      (#\^ #\_ #\c #\a #\r #\_)
      (#\& #\_ #\a #\m #\p #\_))))

Theorem: special-char-alistp-of-special-list

(defthm special-char-alistp-of-special-list
  (b* ((special-list (special-list)))
    (special-char-alistp special-list))
  :rule-classes :rewrite)

Function: special-char

(defun special-char (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'special-char))
    (declare (ignorable acl2::__function__))
    (if (assoc char (special-list)) t nil)))

Theorem: booleanp-of-special-char

(defthm booleanp-of-special-char
  (b* ((special-char? (special-char char)))
    (booleanp special-char?))
  :rule-classes :rewrite)

Function: transform-special

(defun transform-special (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'transform-special))
    (declare (ignorable acl2::__function__))
    (cdr (assoc char (special-list)))))

Theorem: character-listp-of-transform-special

(defthm character-listp-of-transform-special
  (b* ((special (transform-special char)))
    (character-listp special))
  :rule-classes :rewrite)

Function: to-hex

(defun to-hex (n)
  (declare (xargs :guard (natp n)))
  (let ((acl2::__function__ 'to-hex))
    (declare (ignorable acl2::__function__))
    (nat-to-hex-chars n)))

Theorem: hex-digit-char-list*p-of-to-hex

(defthm hex-digit-char-list*p-of-to-hex
  (b* ((hex (to-hex n)))
    (hex-digit-char-list*p hex))
  :rule-classes :rewrite)

Function: construct-hex

(defun construct-hex (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'construct-hex))
    (declare (ignorable acl2::__function__))
    (append '(#\_)
            (to-hex (char-code char))
            '(#\_))))

Theorem: character-listp-of-construct-hex

(defthm character-listp-of-construct-hex
  (b* ((hex (construct-hex char)))
    (character-listp hex))
  :rule-classes :rewrite)

Function: char-is-number

(defun char-is-number (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'char-is-number))
    (declare (ignorable acl2::__function__))
    (cond ((not (characterp char)) nil)
          ((and (>= (char-code char) 48)
                (<= (char-code char) 57))
           t)
          (t nil))))

Theorem: booleanp-of-char-is-number

(defthm booleanp-of-char-is-number
  (b* ((is-number? (char-is-number char)))
    (booleanp is-number?))
  :rule-classes :rewrite)

Theorem: characterp-of-char-is-number

(defthm characterp-of-char-is-number
  (b* ((is-number? (char-is-number char)))
    (implies is-number? (characterp char)))
  :rule-classes :rewrite)

Function: char-is-letter

(defun char-is-letter (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'char-is-letter))
    (declare (ignorable acl2::__function__))
    (cond ((not (characterp char)) nil)
          ((or (and (>= (char-code char) 65)
                    (<= (char-code char) 90))
               (and (>= (char-code char) 97)
                    (<= (char-code char) 122)))
           t)
          (t nil))))

Theorem: booleanp-of-char-is-letter

(defthm booleanp-of-char-is-letter
  (b* ((is-letter? (char-is-letter char)))
    (booleanp is-letter?))
  :rule-classes :rewrite)

Theorem: characterp-of-char-is-letter

(defthm characterp-of-char-is-letter
  (b* ((is-letter? (char-is-letter char)))
    (implies is-letter? (characterp char)))
  :rule-classes :rewrite)

Function: lisp-to-python-names-char

(defun lisp-to-python-names-char (char)
  (declare (xargs :guard (characterp char)))
  (let ((acl2::__function__ 'lisp-to-python-names-char))
    (declare (ignorable acl2::__function__))
    (cond ((or (char-is-number char)
               (char-is-letter char))
           (list char))
          ((special-char char)
           (transform-special char))
          (t (construct-hex char)))))

Theorem: character-listp-of-lisp-to-python-names-char

(defthm character-listp-of-lisp-to-python-names-char
  (b* ((expanded-char (lisp-to-python-names-char char)))
    (character-listp expanded-char))
  :rule-classes :rewrite)

Function: lisp-to-python-names-list

(defun lisp-to-python-names-list (var-char)
  (declare (xargs :guard (character-listp var-char)))
  (let ((acl2::__function__ 'lisp-to-python-names-list))
    (declare (ignorable acl2::__function__))
    (if (endp var-char)
        nil
      (append (lisp-to-python-names-char (car var-char))
              (lisp-to-python-names-list (cdr var-char))))))

Theorem: character-listp-of-lisp-to-python-names-list

(defthm character-listp-of-lisp-to-python-names-list
  (b* ((new-name (lisp-to-python-names-list var-char)))
    (character-listp new-name))
  :rule-classes :rewrite)

Function: lisp-to-python-names-list-top

(defun lisp-to-python-names-list-top (var-char)
  (declare (xargs :guard (character-listp var-char)))
  (let ((acl2::__function__ 'lisp-to-python-names-list-top))
    (declare (ignorable acl2::__function__))
    (cond ((endp var-char) nil)
          ((char-is-number (car var-char))
           (cons #\_
                 (lisp-to-python-names-list var-char)))
          (t (lisp-to-python-names-list var-char)))))

Theorem: character-listp-of-lisp-to-python-names-list-top

(defthm character-listp-of-lisp-to-python-names-list-top
  (b* ((new-name (lisp-to-python-names-list-top var-char)))
    (character-listp new-name))
  :rule-classes :rewrite)

Function: string-or-symbol-p

(defun string-or-symbol-p (name)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'string-or-symbol-p))
    (declare (ignorable acl2::__function__))
    (or (stringp name) (symbolp name))))

Theorem: booleanp-of-string-or-symbol-p

(defthm booleanp-of-string-or-symbol-p
  (b* ((p? (string-or-symbol-p name)))
    (booleanp p?))
  :rule-classes :rewrite)

Function: string-or-symbol-fix

(defun string-or-symbol-fix (x)
  (declare (xargs :guard (string-or-symbol-p x)))
  (let ((acl2::__function__ 'string-or-symbol-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic (if (string-or-symbol-p x) x nil)
         :exec x)))

Function: string-or-symbol-equiv$inline

(defun string-or-symbol-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (string-or-symbol-p acl2::x)
                              (string-or-symbol-p acl2::y))))
  (equal (string-or-symbol-fix acl2::x)
         (string-or-symbol-fix acl2::y)))

Theorem: string-or-symbol-equiv-is-an-equivalence

(defthm string-or-symbol-equiv-is-an-equivalence
  (and (booleanp (string-or-symbol-equiv x y))
       (string-or-symbol-equiv x x)
       (implies (string-or-symbol-equiv x y)
                (string-or-symbol-equiv y x))
       (implies (and (string-or-symbol-equiv x y)
                     (string-or-symbol-equiv y z))
                (string-or-symbol-equiv x z)))
  :rule-classes (:equivalence))

Theorem: string-or-symbol-equiv-implies-equal-string-or-symbol-fix-1

(defthm string-or-symbol-equiv-implies-equal-string-or-symbol-fix-1
  (implies (string-or-symbol-equiv acl2::x x-equiv)
           (equal (string-or-symbol-fix acl2::x)
                  (string-or-symbol-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: string-or-symbol-fix-under-string-or-symbol-equiv

(defthm string-or-symbol-fix-under-string-or-symbol-equiv
  (string-or-symbol-equiv (string-or-symbol-fix acl2::x)
                          acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: lisp-to-python-names

(defun lisp-to-python-names (var)
  (declare (xargs :guard (string-or-symbol-p var)))
  (let ((acl2::__function__ 'lisp-to-python-names))
    (declare (ignorable acl2::__function__))
    (b* ((var (string-or-symbol-fix var))
         (var (if (stringp var) var (string var)))
         (var-char (coerce var 'list)))
      (coerce (lisp-to-python-names-list-top var-char)
              'string))))

Theorem: stringp-of-lisp-to-python-names

(defthm stringp-of-lisp-to-python-names
  (b* ((name (lisp-to-python-names var)))
    (stringp name))
  :rule-classes :rewrite)