array1p

(defthmd array1p-rewrite
  (equal (array1p name l)
    (and (symbolp name)
      (alistp l)
      (let ((header-keyword-list (cdr (header name l))))
        (and (keyword-value-listp header-keyword-list)
          (let* ((dimensions (dimensions name l)) (len (car dimensions))
              (maximum-length (maximum-length name l)))
            (and (true-listp dimensions)
              (equal (len dimensions) 1)
              (integerp len)
              (integerp maximum-length)
              (< 0 len)
              (< len maximum-length)
              (<= maximum-length *max-array-maximum-length*)
              (bounded-integer-alistp l len)))))))
  :hints (("Goal" :in-theory (e/d (array1p header dimensions maximum-length)
       (dimensions-intro maximum-length-intro)))))

(defthmd array1p-rewrite2
  (equal (array1p name l)
    (and (symbolp name)
      (alistp l)
      (let ((header-keyword-list (cdr (header name l))))
        (and (keyword-value-listp header-keyword-list)
          (let* ((dimensions (dimensions name l)) (len (alen1 name l))
              (maximum-length (maximum-length name l)))
            (and (true-listp dimensions)
              (equal (len dimensions) 1)
              (integerp len)
              (integerp maximum-length)
              (< 0 len)
              (< len maximum-length)
              (<= maximum-length *max-array-maximum-length*)
              (bounded-integer-alistp l len)))))))
  :hints (("Goal" :in-theory (enable array1p-rewrite))))

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

(defthmd array1p-of-cons-header
  (equal (array1p name2
      (cons (list :header :dimensions (list dim)
          :maximum-length max
          :default nil
          :name name)
        alist))
    (and (bounded-integer-alistp alist dim)
      (posp dim)
      (< dim max)
      (symbolp name2)
      (<= max *max-array-maximum-length*)
      (integerp max)))
  :hints (("Goal" :in-theory (enable array1p-rewrite))))

(defthm array1p-of-acons-header
  (equal (array1p name2
      (acons :header (list :dimensions (list dim)
          :maximum-length max
          :default nil
          :name name)
        alist))
    (and (bounded-integer-alistp alist dim)
      (posp dim)
      (< dim max)
      (symbolp name2)
      (<= max *max-array-maximum-length*)
      (integerp max)))
  :hints (("Goal" :in-theory (enable array1p-rewrite))))

(defthm array1p-forward-to-<=-of-alen1
  (implies (array1p array-name array)
    (<= (alen1 array-name array) *max-1d-array-length*))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable array1p-rewrite))))

(defthm array1p-forward-to-<=-of-alen1-2
  (implies (array1p array-name array)
    (<= 1 (alen1 array-name array)))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable array1p-rewrite))))

(defthm array1p-of-cons-of-header-and-nil
  (equal (array1p array-name
      (list (list :header :dimensions dims
          :maximum-length maximum-length
          :default default
          :name array-name)))
    (and (symbolp array-name)
      (equal 1 (len dims))
      (true-listp dims)
      (posp (car dims))
      (natp maximum-length)
      (< (car dims) maximum-length)
      (<= maximum-length *max-array-maximum-length*)))
  :hints (("Goal" :in-theory (enable array1p-rewrite))))

(defthm assoc-equal-when-array1p-and-out-of-bounds
  (implies (and (<= (alen1 name array) n)
      (integerp n)
      (array1p name2 array))
    (equal (assoc-equal n array) nil))
  :hints (("Goal" :in-theory (enable array1p-rewrite
       not-assoc-equal-when-bounded-integer-alistp-out-of-bounds
       normalize-alen1-name))))