compress1 - ACL2 Book

Included Books

alen1 compress11 bounded-integer-alistp default dimensions header array1p aref1 alistp strip-cars assoc-equal reverse-list true-list-fix

other

(in-package "ACL2")

include-book

(include-book "alen1")

local

(local (include-book "compress11"))

local

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

local

(local (include-book "default"))

local

(local (include-book "dimensions"))

local

(local (include-book "header"))

local

(local (include-book "array1p"))

local

(local (include-book "aref1"))

local

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

local

(local (include-book "kestrel/alists-light/strip-cars" :dir :system))

local

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

local

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

local

(local (include-book "kestrel/lists-light/true-list-fix" :dir :system))

in-theory

(in-theory (disable compress1))

local

(local (in-theory (enable normalize-header-name
      normalize-compress11-name
      normalize-default-name
      normalize-dimensions-name
      normalize-alen1-name
      normalize-array1p-name)))

local

(local (defthm alistp-of-reverse-list
    (equal (alistp (reverse-list x)) (alistp (true-list-fix x)))
    :hints (("Goal" :in-theory (enable alistp reverse-list)))))

local

(local (defthm bounded-integer-alistp-of-reverse-list
    (equal (bounded-integer-alistp (reverse-list x) n)
      (bounded-integer-alistp (true-list-fix x) n))
    :hints (("Goal" :in-theory (enable alistp reverse-list)))))

local

(local (defthm strip-cars-of-reverse-list
    (equal (strip-cars (reverse-list alist))
      (reverse-list (strip-cars alist)))
    :hints (("Goal" :in-theory (enable reverse-list)))))

local

(local (defthm assoc-equal-of-reverse-list
    (implies (and (no-duplicatesp (strip-cars alist)) (alistp alist))
      (equal (assoc-equal key (reverse-list alist))
        (assoc-equal key alist)))
    :hints (("Goal" :in-theory (enable assoc-equal
         reverse-list
         no-duplicatesp
         assoc-equal-iff-member-equal-of-strip-cars)))))

equal-of-assoc-equal-sametheorem

(defthm equal-of-assoc-equal-same
  (implies key
    (iff (equal key (car (assoc-equal key array)))
      (assoc-equal key array)))
  :hints (("Goal" :in-theory (enable assoc-equal))))

header-of-compress1theorem

(defthm header-of-compress1
  (equal (header array-name (compress1 array-name2 array))
    (header array-name array))
  :hints (("Goal" :in-theory (enable compress1 compress11 header))))

maximum-length-of-compress1theorem

(defthm maximum-length-of-compress1
  (equal (maximum-length array-name (compress1 array-name2 array))
    (maximum-length array-name array))
  :hints (("Goal" :in-theory (enable compress1 compress11 maximum-length header))))

dimensions-of-compress1theorem

(defthm dimensions-of-compress1
  (equal (dimensions array-name (compress1 array-name2 array))
    (dimensions array-name array))
  :hints (("Goal" :in-theory (enable compress1 dimensions-intro header-intro))))

default-of-compress1theorem

(defthm default-of-compress1
  (equal (default name (compress1 name2 l))
    (if (or (equal (array-order (header name2 l)) '<)
        (equal (array-order (header name2 l)) '>))
      (default name2 l)
      (default name l)))
  :hints (("Goal" :in-theory (e/d (compress1 default) (array-order default-intro)))))

alistp-of-compress1theorem

(defthm alistp-of-compress1
  (implies (and (alistp array) (consp (header array-name array)))
    (alistp (compress1 array-name array)))
  :hints (("Goal" :in-theory (enable compress1))))

bounded-integer-alistp-of-compress1theorem

(defthm bounded-integer-alistp-of-compress1
  (implies (and (bounded-integer-alistp array n) (natp n))
    (iff (bounded-integer-alistp (compress1 array-name array) n)
      (header array-name array)))
  :hints (("Goal" :in-theory (enable compress1))))

array1p-of-compress1theorem

(defthm array1p-of-compress1
  (implies (array1p array-name l)
    (array1p array-name (compress1 array-name2 l)))
  :hints (("Goal" :in-theory (enable array1p compress1 header))))

normalize-compress1-nametheorem

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

assoc-equal-of-compress1theorem

(defthm assoc-equal-of-compress1
  (implies (and (natp index) (array1p :fake-name l))
    (equal (assoc-equal index (compress1 name l))
      (if (and (equal (cdr (assoc-equal index l)) (default name l))
          (or (equal (array-order (assoc-equal :header l)) '>)
            (equal (array-order (assoc-equal :header l)) '<)))
        nil
        (assoc-equal index l))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (e/d (array1p compress1
         header-intro
         not-assoc-equal-when-bounded-integer-alistp-out-of-bounds
         dimensions-intro)
       (assoc-equal header)))))

local

(local (defthm assoc-equal-of-reverse-list-iff
    (implies (or (alistp x) key)
      (iff (assoc-equal key (reverse-list x)) (assoc-equal key x)))
    :hints (("Goal" :in-theory (enable reverse-list)))))

assoc-equal-of-compress1-when-<theorem

(defthm assoc-equal-of-compress1-when-<
  (implies (and (natp index)
      (< index (car (dimensions name l)))
      (alistp l)
      (integerp (car (dimensions name l))))
    (equal (assoc-equal index (compress1 name l))
      (if (and (equal (cdr (assoc-equal index l)) (default name l))
          (or (equal (array-order (assoc-equal :header l)) '>)
            (equal (array-order (assoc-equal :header l)) '<)))
        nil
        (assoc-equal index l))))
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (e/d (compress1 header
         not-assoc-equal-when-bounded-integer-alistp-out-of-bounds)
       (assoc-equal array1p)))))

assoc-equal-of-header-of-compress1theorem

(defthm assoc-equal-of-header-of-compress1
  (equal (assoc-equal :header (compress1 name l))
    (header name l))
  :hints (("Goal" :in-theory (enable compress1 header-intro))))

local

(local (defthm aref1-of-compress1-small
    (implies (and (< n (alen1 array-name array))
        (natp n)
        (alistp array)
        (integerp (alen1 array-name array)))
      (equal (aref1 array-name (compress1 array-name2 array) n)
        (aref1 array-name array n)))
    :hints (("Goal" :in-theory (enable aref1 dimensions-intro)))))

local

(local (defthm aref1-of-compress1-too-large
    (implies (and (<= (alen1 array-name array) n)
        (natp n)
        (array1p array-name array)
        (alistp array))
      (equal (aref1 array-name (compress1 array-name2 array) n)
        (default array-name array)))
    :hints (("Goal" :in-theory (e/d (aref1-when-too-large) (array1p))))))

aref1-of-compress1theorem

(defthm aref1-of-compress1
  (implies (and (natp n) (array1p array-name array))
    (equal (aref1 array-name (compress1 array-name2 array) n)
      (if (< n (alen1 array-name array))
        (aref1 array-name array n)
        (default array-name array))))
  :hints (("Goal" :in-theory (enable aref1-when-too-large))))