coerce - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "kestrel/lists-light/len" :dir :system))

local

(local (include-book "kestrel/typed-lists-light/make-character-list" :dir :system))

consp-of-coerce-of-listtheorem

(defthm consp-of-coerce-of-list
  (equal (consp (coerce x 'list))
    (and (stringp x) (not (equal x ""))))
  :hints (("Goal" :use (:instance coerce-inverse-2)
     :cases ((coerce x 'list)))))

coerce-of-list-ifftheorem

(defthm coerce-of-list-iff
  (iff (coerce x 'list) (and (stringp x) (not (equal x ""))))
  :hints (("Goal" :use (:instance consp-of-coerce-of-list)
     :in-theory (disable consp-of-coerce-of-list))))

equal-of-len-of-coerce-of-list-and-0theorem

(defthm equal-of-len-of-coerce-of-list-and-0
  (equal (equal (len (coerce str 'list)) 0)
    (or (not (stringp str)) (equal str ""))))

coerce-of-make-character-listtheorem

(defthm coerce-of-make-character-list
  (equal (coerce (make-character-list x) 'string)
    (coerce x 'string))
  :hints (("Goal" :use (:instance completion-of-coerce (y 'string)))))

equal-of-coerce-of-stringtheorem

(defthmd equal-of-coerce-of-string
  (implies (character-listp x)
    (equal (equal (coerce x 'string) str)
      (and (stringp str) (equal x (coerce str 'list))))))

equal-of-coerce-of-string-strongtheorem

(defthmd equal-of-coerce-of-string-strong
  (equal (equal (coerce x 'string) str)
    (and (stringp str)
      (equal (make-character-list x) (coerce str 'list))))
  :hints (("Goal" :use ((:instance equal-of-coerce-of-string
        (x (make-character-list x))) coerce-of-make-character-list)
     :in-theory (disable coerce-of-make-character-list))))

equal-of-coerce-of-string-when-quoteptheorem

(defthm equal-of-coerce-of-string-when-quotep
  (implies (and (syntaxp (quotep str)) (character-listp x))
    (equal (equal (coerce x 'string) str)
      (and (stringp str) (equal x (coerce str 'list))))))

equal-of-coerce-of-string-when-quotep-strongtheorem

(defthm equal-of-coerce-of-string-when-quotep-strong
  (implies (syntaxp (quotep str))
    (equal (equal (coerce x 'string) str)
      (and (stringp str)
        (equal (make-character-list x) (coerce str 'list)))))
  :hints (("Goal" :in-theory (enable equal-of-coerce-of-string-strong))))

equal-of-coerce-of-list-when-quoteptheorem

(defthm equal-of-coerce-of-list-when-quotep
  (implies (and (syntaxp (quotep chars)) (stringp x))
    (equal (equal (coerce x 'list) chars)
      (and (character-listp chars)
        (equal x (coerce chars 'string))))))

equal-of-coerce-and-coerce-string-casetheorem

(defthm equal-of-coerce-and-coerce-string-case
  (implies (and (character-listp x) (character-listp y))
    (equal (equal (coerce x 'string) (coerce y 'string))
      (equal x y)))
  :hints (("Goal" :use ((:instance coerce-inverse-1 (x x)) (:instance coerce-inverse-1 (x y)))
     :in-theory (disable coerce-inverse-1))))

equal-of-coerce-and-coerce-list-casetheorem

(defthm equal-of-coerce-and-coerce-list-case
  (implies (and (stringp x) (stringp y))
    (equal (equal (coerce x 'list) (coerce y 'list))
      (equal x y)))
  :hints (("Goal" :use ((:instance coerce-inverse-2 (x x)) (:instance coerce-inverse-2 (x y)))
     :in-theory (disable coerce-inverse-2))))

coerce-injectivetheorem

(defthm coerce-injective
  (implies (and (equal (coerce x 'list) (coerce y 'list))
      (stringp x)
      (stringp y))
    (equal x y))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable coerce-inverse-2)
     :use ((:instance coerce-inverse-2 (x x)) (:instance coerce-inverse-2 (x y))))))

coerce-inverse-1-forcedtheorem

(defthmd coerce-inverse-1-forced
  (implies (force (character-listp x))
    (equal (coerce (coerce x 'string) 'list) x)))

coerce-inverse-1-gentheorem

(defthmd coerce-inverse-1-gen
  (equal (coerce (coerce x 'string) 'list)
    (make-character-list x))
  :hints (("Goal" :use (:instance coerce-inverse-1-forced
       (x (make-character-list x))))))

local

(local (defthm length-of-coerce-string-helper
    (implies (character-listp x)
      (equal (length (coerce x 'string)) (len x)))
    :hints (("Goal" :use (completion-of-coerce)))))

length-of-coerce-stringtheorem

(defthm length-of-coerce-string
  (equal (length (coerce x 'string)) (len x))
  :hints (("Goal" :use ((:instance completion-of-coerce (y 'string)) length-of-coerce-string-helper
       (:instance length-of-coerce-string-helper
         (x (make-character-list x)))))))

len-of-coerce-listtheorem

(defthmd len-of-coerce-list
  (equal (len (coerce x 'list))
    (if (stringp x)
      (length x)
      0)))

other

(theory-invariant (incompatible (:rewrite len-of-coerce-list)
    (:definition length)))