compress11 - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "kestrel/alists-light/assoc-equal" :dir :system))

local

(local (include-book "bounded-integer-alistp"))

in-theory

(in-theory (disable compress11))

local

(local (defthm not-equal-of-car-of-assoc-equal
    (implies (and (not (equal val key)) val)
      (not (equal val (car (assoc-equal key array)))))
    :hints (("Goal" :in-theory (enable assoc-equal)))))

assoc-equal-of-header-and-compress11theorem

(defthm assoc-equal-of-header-and-compress11
  (implies (integerp i)
    (equal (assoc-equal :header (compress11 name l i n default))
      nil))
  :hints (("Goal" :in-theory (enable compress11))))

header-of-compress11theorem

(defthm header-of-compress11
  (implies (integerp i)
    (equal (header name (compress11 name2 array i n default))
      nil))
  :hints (("Goal" :in-theory (enable compress11))))

dimensions-of-compress11theorem

(defthm dimensions-of-compress11
  (implies (integerp i)
    (equal (dimensions name (compress11 name2 array i n default))
      nil))
  :hints (("Goal" :in-theory (enable compress11))))

default-of-compress11theorem

(defthm default-of-compress11
  (implies (integerp i)
    (equal (default name (compress11 name2 array i n default))
      nil))
  :hints (("Goal" :in-theory (enable compress11))))

alistp-of-compress11theorem

(defthm alistp-of-compress11
  (implies (or (alistp array) (not default))
    (alistp (compress11 name array i n default)))
  :hints (("Goal" :induct t :in-theory (enable compress11))))

assoc-equal-of-compress11-when-too-smalltheorem

(defthm assoc-equal-of-compress11-when-too-small
  (implies (< index i)
    (equal (assoc-equal index (compress11 name l i n default))
      nil))
  :hints (("Goal" :in-theory (enable compress11))))

bounded-integer-alistp-of-compress11theorem

(defthm bounded-integer-alistp-of-compress11
  (implies (and (bounded-integer-alistp array n))
    (bounded-integer-alistp (compress11 name array i index default)
      n))
  :hints (("Goal" :in-theory (e/d (compress11 bounded-integer-alistp
         assoc-equal-forward-when-bounded-integer-alistp)
       (car-of-assoc-equal-cheap)))))

local

(local (defthmd assoc-equal-of-compress11
    (implies (and (<= i index) (< index n) (integerp i) (integerp index))
      (equal (assoc-equal index (compress11 name l i n default))
        (if (or (not (integerp (- n i)))
            (equal default (cdr (assoc-equal index l))))
          nil
          (assoc-equal index l))))
    :hints (("Goal" :do-not '(generalize eliminate-destructors)
       :in-theory (enable compress11)))))

local

(local (defthmd assoc-equal-of-compress11-too-high
    (implies (and (<= n index)
        (<= i index)
        (integerp i)
        (integerp index))
      (equal (assoc-equal index (compress11 name l i n default))
        nil))
    :hints (("Goal" :do-not '(generalize eliminate-destructors)
       :in-theory (enable compress11)))))

assoc-equal-of-compress11-boththeorem

(defthm assoc-equal-of-compress11-both
  (implies (and (integerp i) (integerp index))
    (equal (assoc-equal index (compress11 name l i n default))
      (if (or (< index i) (<= n index) (not (integerp (- n i))))
        nil
        (if (equal default (cdr (assoc-equal index l)))
          nil
          (assoc-equal index l)))))
  :hints (("Goal" :use (assoc-equal-of-compress11-too-high assoc-equal-of-compress11)
     :in-theory (disable assoc-equal))))

normalize-compress11-nametheorem

(defthmd normalize-compress11-name
  (implies (syntaxp (not (equal name '':fake-name)))
    (equal (compress11 name l i n default)
      (compress11 :fake-name l i n default)))
  :hints (("Goal" :in-theory (enable compress11))))

no-duplicatesp-of-strip-cars-of-compress11theorem

(defthm no-duplicatesp-of-strip-cars-of-compress11
  (implies (integerp i)
    (no-duplicatesp (strip-cars (compress11 name l i n default))))
  :hints (("Goal" :in-theory (enable compress11
       member-equal-of-strip-cars-iff-assoc-equal))))