arithmetic

other

(in-package "ACL2")

include-book

(include-book "coerce")

include-book

(include-book "arithmetic/top" :dir :system)

include-book

(include-book "std/lists/take" :dir :system)

include-book

(include-book "std/lists/len" :dir :system)

include-book

(include-book "std/lists/nthcdr" :dir :system)

include-book

(include-book "std/lists/append" :dir :system)

include-book

(include-book "std/lists/repeat" :dir :system)

negative-when-natptheorem

(defthm negative-when-natp
  (implies (natp x) (equal (< x 0) nil)))

eqlablep-when-characterptheorem

(defthm eqlablep-when-characterp
  (implies (characterp x) (eqlablep x)))

nth-of-lentheorem

(defthm nth-of-len (equal (nth (len x) x) nil))

nth-when-biggertheorem

(defthm nth-when-bigger
  (implies (<= (len x) (nfix n)) (equal (nth n x) nil))
  :hints (("Goal" :in-theory (enable nth))))

car-of-repeattheorem

(defthm car-of-repeat
  (equal (car (repeat n x))
    (if (zp n)
      nil
      x))
  :hints (("Goal" :in-theory (enable repeat))))

len-of-nonempty-string-is-positivetheorem

(defthm len-of-nonempty-string-is-positive
  (implies (and (stringp x) (not (equal x "")))
    (< 0 (len (explode x))))
  :rule-classes ((:rewrite) (:linear)))

length-zero-when-stringptheorem

(defthm length-zero-when-stringp
  (implies (stringp x)
    (equal (equal 0 (length x)) (equal x ""))))

length-zero-when-stringp-alttheorem

(defthm length-zero-when-stringp-alt
  (implies (stringp x)
    (equal (equal 0 (len (explode x))) (equal x ""))))

subsetp-equal-of-cons-righttheorem

(defthm subsetp-equal-of-cons-right
  (implies (subsetp-equal x y) (subsetp-equal x (cons b y))))

subsetp-equal-reflexivetheorem

(defthm subsetp-equal-reflexive (subsetp-equal x x))

char-code-of-code-char-of-sum-with-char-codeencapsulate

(encapsulate nil
  (local (defthm l1
      (implies (or (not (natp x)) (<= 256 x))
        (equal (code-char x) (code-char 0)))
      :hints (("Goal" :use ((:instance completion-of-code-char))))))
  (local (defthm l2
      (implies (natp k)
        (equal (char-code (code-char (+ k (char-code a))))
          (if (and (integerp k)
              (<= 0 (+ k (char-code a)))
              (< (+ k (char-code a)) 256))
            (+ k (char-code a))
            0)))
      :hints (("Goal" :cases ((< (+ k (char-code a)) 256))))))
  (local (defthm l0
      (implies (and (integerp a) (not (integerp b)))
        (equal (integerp (+ a b)) (not (acl2-numberp b))))))
  (defthm char-code-of-code-char-of-sum-with-char-code
    (equal (char-code (code-char (+ k (char-code a))))
      (cond ((integerp k) (if (and (<= 0 (+ k (char-code a))) (< (+ k (char-code a)) 256))
            (+ k (char-code a))
            0))
        ((acl2-numberp k) 0)
        (t (char-code a))))
    :hints (("Goal" :in-theory (e/d nil
         (code-char-char-code-is-identity equal-of-char-codes))))))

characterp-of-car-when-character-listptheorem

(defthm characterp-of-car-when-character-listp
  (implies (character-listp x)
    (equal (characterp (car x)) (consp x))))

character-listp-of-cdr-when-character-listptheorem

(defthm character-listp-of-cdr-when-character-listp
  (implies (character-listp x) (character-listp (cdr x))))

character-listp-of-repeattheorem

(defthm character-listp-of-repeat
  (implies (characterp x) (character-listp (repeat n x)))
  :hints (("Goal" :in-theory (enable repeat))))

character-listp-of-taketheorem

(defthm character-listp-of-take
  (implies (character-listp x)
    (equal (character-listp (take n x)) (<= (nfix n) (len x))))
  :hints (("Goal" :in-theory (enable take))))

character-listp-of-revtheorem

(defthm character-listp-of-rev
  (equal (character-listp (rev x))
    (character-listp (list-fix x)))
  :hints (("Goal" :induct (len x))))

Included Books