aref1

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

(defthmd aref1-when-too-large
  (implies (and (<= (alen1 array-name array) n)
      (array1p array-name array)
      (natp n))
    (equal (aref1 array-name array n)
      (default array-name array)))
  :hints (("Goal" :in-theory (enable aref1
       array1p-rewrite
       header
       not-assoc-equal-when-bounded-integer-alistp-out-of-bounds))))

(defthm aref1-when-too-large-cheap
  (implies (and (<= (alen1 array-name array) n)
      (array1p array-name array)
      (natp n))
    (equal (aref1 array-name array n)
      (default array-name array)))
  :rule-classes ((:rewrite :backchain-limit-lst (0 nil nil)))
  :hints (("Goal" :in-theory (enable aref1-when-too-large))))

(defthm aref1-of-cons-of-cons-of-header
  (implies (natp n)
    (equal (aref1 array-name (cons (cons :header header) alist) n)
      (if (assoc-equal n alist)
        (aref1 array-name alist n)
        (cadr (assoc-keyword :default header)))))
  :hints (("Goal" :in-theory (enable aref1 header))))

(defthm aref1-of-acons-of-header
  (implies (natp n)
    (equal (aref1 array-name (acons :header header alist) n)
      (if (assoc-equal n alist)
        (aref1 array-name alist n)
        (cadr (assoc-keyword :default header)))))
  :hints (("Goal" :in-theory (enable acons))))

(defthm aref1-of-cons-of-cons-of-header-alt
  (implies (and (equal (default array-name array)
        (cadr (assoc-keyword :default header-args))))
    (equal (aref1 array-name (cons (cons :header header-args) array) n)
      (aref1 array-name array n)))
  :hints (("Goal" :in-theory (enable aref1 header))))

(defthmd aref1-when-not-assoc-equal
  (implies (not (assoc-equal n alist))
    (equal (aref1 array-name alist n)
      (default array-name alist)))
  :hints (("Goal" :in-theory (enable aref1))))