Built-in axioms and theorems about symbols.
Definition:
(defaxiom stringp-symbol-package-name (stringp (symbol-package-name x)) :rule-classes :type-prescription)
Definition:
(defaxiom symbolp-intern-in-package-of-symbol (symbolp (intern-in-package-of-symbol x y)) :rule-classes :type-prescription)
Definition:
(defaxiom symbolp-pkg-witness (symbolp (pkg-witness x)) :rule-classes :type-prescription)
Definition:
(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:
(defaxiom symbol-name-pkg-witness (equal (symbol-name (pkg-witness pkg-name)) *pkg-witness-name*))
Definition:
(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:
(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:
(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:
(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:
(defaxiom symbol-listp-pkg-imports (symbol-listp (pkg-imports pkg)) :rule-classes ((:forward-chaining :trigger-terms ((pkg-imports pkg)))))
Definition:
(defaxiom no-duplicatesp-eq-pkg-imports (no-duplicatesp-eq (pkg-imports pkg)) :rule-classes :rewrite)
Definition:
(defaxiom completion-of-pkg-imports (equal (pkg-imports x) (if (stringp x) (pkg-imports x) nil)) :rule-classes nil)
Definition:
(defaxiom acl2-input-channel-package (equal (pkg-imports "ACL2-INPUT-CHANNEL") nil))
Definition:
(defaxiom acl2-output-channel-package (equal (pkg-imports "ACL2-OUTPUT-CHANNEL") nil))
Definition:
(defaxiom acl2-package (equal (pkg-imports "ACL2") *common-lisp-symbols-from-main-lisp-package*))
Definition:
(defaxiom keyword-package (equal (pkg-imports "KEYWORD") nil))
Definition:
(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:
(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:
(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:
(defaxiom completion-of-symbol-name (equal (symbol-name x) (if (symbolp x) (symbol-name x) "")) :rule-classes nil)
Definition:
(defaxiom completion-of-symbol-package-name (equal (symbol-package-name x) (if (symbolp x) (symbol-package-name x) "")) :rule-classes nil)
Theorem:
(defthm keywordp-forward-to-symbolp (implies (keywordp x) (symbolp x)) :rule-classes :forward-chaining)
Theorem:
(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:
(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:
(defthm default-pkg-imports (implies (not (stringp x)) (equal (pkg-imports x) nil)))
Theorem:
(defthm symbol<-asymmetric (implies (symbol< sym1 sym2) (not (symbol< sym2 sym1))))
Theorem:
(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:
(defthm symbol<-trichotomy (implies (and (symbolp x) (symbolp y) (not (symbol< x y))) (iff (symbol< y x) (not (equal x y)))))
Theorem:
(defthm symbol<-irreflexive (implies (symbolp x) (not (symbol< x x))))
Theorem:
(defthm default-intern-in-package-of-symbol (implies (not (and (stringp x) (symbolp y))) (equal (intern-in-package-of-symbol x y) nil)))
Theorem:
(defthm default-symbol-name (implies (not (symbolp x)) (equal (symbol-name x) "")))
Theorem:
(defthm default-symbol-package-name (implies (not (symbolp x)) (equal (symbol-package-name x) "")))
Theorem:
(defthm symbol-listp-cdr-assoc-equal (implies (symbol-list-listp x) (symbol-listp (cdr (assoc-equal key x)))))
Theorem:
(defthm symbol-listp-strict-merge-sort-symbol< (implies (symbol-listp x) (symbol-listp (strict-merge-sort-symbol< x))))