intern-in-package-of-symbol

Included Books

other

(in-package "ACL2")

local

(local (include-book "map-symbol-name"))

local

(local (in-theory (disable member-equal)))

symbol-equality-strongtheorem

(defthmd symbol-equality-strong
  (implies (or (symbolp s1) (symbolp s2))
    (equal (equal s1 s2)
      (and (equal (symbol-name s1) (symbol-name s2))
        (equal (symbol-package-name s1) (symbol-package-name s2)))))
  :hints (("Goal" :use (:instance symbol-equality))))

equal-of-intern-in-package-of-symbol-and-intern-in-package-of-symbol-same-arg2theorem

(defthm equal-of-intern-in-package-of-symbol-and-intern-in-package-of-symbol-same-arg2
  (implies (and (stringp x1) (stringp x2) (symbolp y))
    (equal (equal (intern-in-package-of-symbol x1 y)
        (intern-in-package-of-symbol x2 y))
      (equal x1 x2)))
  :hints (("Goal" :use (:instance symbol-equality-strong
       (s1 (intern-in-package-of-symbol x1 y))
       (s2 (intern-in-package-of-symbol x2 y))))))

equal-of-intern-in-package-of-symboltheorem

(defthmd equal-of-intern-in-package-of-symbol
  (implies (and (stringp str)
      (symbolp sym2)
      (not (member-symbol-name str
          (pkg-imports (symbol-package-name sym2)))))
    (equal (equal sym (intern-in-package-of-symbol str sym2))
      (and (symbolp sym)
        (equal str (symbol-name sym))
        (equal (symbol-package-name sym) (symbol-package-name sym2)))))
  :hints (("Goal" :cases ((symbol-package-name sym2)))))

local

(local (defthm member-symbol-name-iff
    (iff (member-symbol-name str l)
      (member-equal str (map-symbol-name l)))
    :hints (("Goal" :in-theory (enable member-symbol-name member-equal map-symbol-name)))))

local

(local (defthm car-of-member-symbol-name-iff
    (implies (not (equal "NIL" str))
      (iff (car (member-symbol-name str l))
        (member-equal str (map-symbol-name l))))
    :hints (("GOAL" :in-theory (enable member-symbol-name member-equal map-symbol-name)))))

intern-in-package-of-symbol-ifftheorem

(defthm intern-in-package-of-symbol-iff
  (implies (and (equal (symbol-package-name sym) "ACL2") (stringp str))
    (iff (intern-in-package-of-symbol str sym)
      (not (equal str "NIL"))))
  :hints (("Goal" :use (:instance equal-of-intern-in-package-of-symbol
       (sym2 sym)
       (sym nil))
     :cases ((symbolp sym))
     :in-theory (e/d (intern-in-package-of-symbol-is-identity)
       (equal-of-intern-in-package-of-symbol)))))

symbol-package-name-of-intern-in-package-of-symboltheorem

(defthm symbol-package-name-of-intern-in-package-of-symbol
  (equal (symbol-package-name (intern-in-package-of-symbol str sym))
    (if (and (symbolp sym) (stringp str))
      (if (member-symbol-name str
          (pkg-imports (symbol-package-name sym)))
        (symbol-package-name (car (member-symbol-name str
              (pkg-imports (symbol-package-name sym)))))
        (symbol-package-name sym))
      "COMMON-LISP")))

keywordp-of-intern-in-package-of-symbol-when-keywordptheorem

(defthm keywordp-of-intern-in-package-of-symbol-when-keywordp
  (implies (keywordp sym)
    (equal (keywordp (intern-in-package-of-symbol str sym))
      (stringp str)))
  :hints (("Goal" :in-theory (enable keywordp member-equal))))