• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-about-symbols

Built-in theorems about symbols.

Definition: stringp-symbol-package-name

(defaxiom stringp-symbol-package-name
          (stringp (symbol-package-name x))
          :rule-classes :type-prescription)

Definition: symbolp-intern-in-package-of-symbol

(defaxiom symbolp-intern-in-package-of-symbol
          (symbolp (intern-in-package-of-symbol x y))
          :rule-classes :type-prescription)

Definition: symbolp-pkg-witness

(defaxiom symbolp-pkg-witness
          (symbolp (pkg-witness x))
          :rule-classes :type-prescription)

Definition: intern-in-package-of-symbol-symbol-name

(defaxiom
     intern-in-package-of-symbol-symbol-name
     (implies (and (symbolp x)
                   (equal (symbol-package-name x)
                          (symbol-package-name y)))
              (equal (intern-in-package-of-symbol (symbol-name x)
                                                  y)
                     x)))

Definition: symbol-name-pkg-witness

(defaxiom symbol-name-pkg-witness
          (equal (symbol-name (pkg-witness pkg-name))
                 *pkg-witness-name*))

Definition: symbol-package-name-pkg-witness-name

(defaxiom symbol-package-name-pkg-witness-name
          (equal (symbol-package-name (pkg-witness pkg-name))
                 (if (and (stringp pkg-name)
                          (not (equal pkg-name "")))
                     pkg-name "ACL2")))

Definition: symbol-name-intern-in-package-of-symbol

(defaxiom
 symbol-name-intern-in-package-of-symbol
 (implies
     (and (stringp s) (symbolp any-symbol))
     (equal (symbol-name (intern-in-package-of-symbol s any-symbol))
            s)))

Definition: symbol-package-name-intern-in-package-of-symbol

(defaxiom
 symbol-package-name-intern-in-package-of-symbol
 (implies
  (and
   (stringp x)
   (symbolp y)
   (not (member-symbol-name x
                            (pkg-imports (symbol-package-name y)))))
  (equal (symbol-package-name (intern-in-package-of-symbol x y))
         (symbol-package-name y))))

Definition: intern-in-package-of-symbol-is-identity

(defaxiom
 intern-in-package-of-symbol-is-identity
 (implies
  (and (stringp x)
       (symbolp y)
       (member-symbol-name x
                           (pkg-imports (symbol-package-name y))))
  (equal
   (intern-in-package-of-symbol x y)
   (car
      (member-symbol-name x
                          (pkg-imports (symbol-package-name y)))))))

Definition: symbol-listp-pkg-imports

(defaxiom symbol-listp-pkg-imports
          (symbol-listp (pkg-imports pkg))
          :rule-classes
          ((:forward-chaining :trigger-terms ((pkg-imports pkg)))))

Definition: no-duplicatesp-eq-pkg-imports

(defaxiom no-duplicatesp-eq-pkg-imports
          (no-duplicatesp-eq (pkg-imports pkg))
          :rule-classes :rewrite)

Definition: completion-of-pkg-imports

(defaxiom completion-of-pkg-imports
          (equal (pkg-imports x)
                 (if (stringp x) (pkg-imports x) nil))
          :rule-classes nil)

Definition: acl2-input-channel-package

(defaxiom acl2-input-channel-package
          (equal (pkg-imports "ACL2-INPUT-CHANNEL")
                 nil))

Definition: acl2-output-channel-package

(defaxiom acl2-output-channel-package
          (equal (pkg-imports "ACL2-OUTPUT-CHANNEL")
                 nil))

Definition: acl2-package

(defaxiom acl2-package
          (equal (pkg-imports "ACL2")
                 *common-lisp-symbols-from-main-lisp-package*))

Definition: keyword-package

(defaxiom keyword-package
          (equal (pkg-imports "KEYWORD") nil))

Definition: string-is-not-circular

(defaxiom
 string-is-not-circular
 (equal
  'string
  (intern-in-package-of-symbol
    (coerce (cons #\S
                  (cons #\T
                        (cons #\R
                              (cons #\I (cons #\N (cons #\G 0))))))
            (cons #\S
                  (cons #\T
                        (cons #\R
                              (cons #\I (cons #\N (cons #\G 0)))))))
    (intern-in-package-of-symbol 0 0)))
 :rule-classes nil)

Definition: nil-is-not-circular

(defaxiom nil-is-not-circular
          (equal nil
                 (intern-in-package-of-symbol
                      (coerce (cons #\N (cons #\I (cons #\L 0)))
                              'string)
                      'string))
          :rule-classes nil)

Definition: completion-of-intern-in-package-of-symbol

(defaxiom completion-of-intern-in-package-of-symbol
          (equal (intern-in-package-of-symbol x y)
                 (if (and (stringp x) (symbolp y))
                     (intern-in-package-of-symbol x y)
                     nil))
          :rule-classes nil)

Definition: completion-of-symbol-name

(defaxiom completion-of-symbol-name
          (equal (symbol-name x)
                 (if (symbolp x) (symbol-name x) ""))
          :rule-classes nil)

Definition: completion-of-symbol-package-name

(defaxiom completion-of-symbol-package-name
          (equal (symbol-package-name x)
                 (if (symbolp x)
                     (symbol-package-name x)
                     ""))
          :rule-classes nil)

Theorem: keywordp-forward-to-symbolp

(defthm keywordp-forward-to-symbolp
        (implies (keywordp x) (symbolp x))
        :rule-classes :forward-chaining)

Theorem: symbol-package-name-of-symbol-is-not-empty-string

(defthm
     symbol-package-name-of-symbol-is-not-empty-string
     (implies (symbolp x)
              (not (equal (symbol-package-name x) "")))
     :rule-classes
     ((:forward-chaining :trigger-terms ((symbol-package-name x)))))

Theorem: symbol-equality

(defthm symbol-equality
        (implies (and (or (symbolp s1) (symbolp s2))
                      (equal (symbol-name s1)
                             (symbol-name s2))
                      (equal (symbol-package-name s1)
                             (symbol-package-name s2)))
                 (equal s1 s2))
        :rule-classes nil)

Theorem: default-pkg-imports

(defthm default-pkg-imports
        (implies (not (stringp x))
                 (equal (pkg-imports x) nil)))

Theorem: symbol<-asymmetric

(defthm symbol<-asymmetric
        (implies (symbol< sym1 sym2)
                 (not (symbol< sym2 sym1))))

Theorem: symbol<-transitive

(defthm symbol<-transitive
        (implies (and (symbol< x y)
                      (symbol< y z)
                      (symbolp x)
                      (symbolp y)
                      (symbolp z))
                 (symbol< x z))
        :rule-classes ((:rewrite :match-free :all)))

Theorem: symbol<-trichotomy

(defthm symbol<-trichotomy
        (implies (and (symbolp x)
                      (symbolp y)
                      (not (symbol< x y)))
                 (iff (symbol< y x) (not (equal x y)))))

Theorem: symbol<-irreflexive

(defthm symbol<-irreflexive
        (implies (symbolp x)
                 (not (symbol< x x))))

Theorem: default-intern-in-package-of-symbol

(defthm default-intern-in-package-of-symbol
        (implies (not (and (stringp x) (symbolp y)))
                 (equal (intern-in-package-of-symbol x y)
                        nil)))

Theorem: default-symbol-name

(defthm default-symbol-name
        (implies (not (symbolp x))
                 (equal (symbol-name x) "")))

Theorem: default-symbol-package-name

(defthm default-symbol-package-name
        (implies (not (symbolp x))
                 (equal (symbol-package-name x) "")))

Theorem: symbol-listp-cdr-assoc-equal

(defthm symbol-listp-cdr-assoc-equal
        (implies (symbol-list-listp x)
                 (symbol-listp (cdr (assoc-equal key x)))))