dimensions

(in-package "ACL2")

(in-theory (disable dimensions))

(defthm dimensions-intro
  (equal (cadr (assoc-keyword :dimensions (cdr (header name l))))
    (dimensions name l))
  :hints (("Goal" :in-theory (enable dimensions))))

(theory-invariant (incompatible (:rewrite dimensions-intro)
    (:definition dimensions)))

(defthmd dimensions-intro2
  (equal (cadr (assoc-keyword :dimensions (cdr (assoc-equal :header l))))
    (dimensions name l))
  :hints (("Goal" :in-theory (e/d (dimensions header) (dimensions-intro)))))

(theory-invariant (incompatible (:rewrite dimensions-intro2)
    (:definition dimensions)))

(defthm true-listp-of-dimensions-when-array1p
  (implies (array1p array-name array)
    (true-listp (dimensions array-name array)))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (e/d (dimensions) (dimensions-intro)))))

(defthm dimensions-of-cons
  (equal (dimensions array-name (cons entry alist))
    (if (eq :header (car entry))
      (cadr (assoc-keyword :dimensions (cdr entry)))
      (dimensions array-name alist)))
  :hints (("Goal" :in-theory (e/d (dimensions) (dimensions-intro)))))

(defthm posp-of-car-of-dimensions-when-array1p
  (implies (array1p array-name array)
    (posp (car (dimensions array-name array))))
  :rule-classes :type-prescription :hints (("Goal" :in-theory (e/d (array1p dimensions) (dimensions-intro)))))

(defthm natp-of-nth-of-0-and-dimensions-when-array1p
  (implies (array1p array-name array)
    (natp (nth 0 (dimensions array-name array))))
  :hints (("Goal" :in-theory (e/d (array1p dimensions) (dimensions-intro)))))

(defthm rationalp-of-nth-of-0-and-dimensions-when-array1p
  (implies (array1p array-name array)
    (rationalp (nth 0 (dimensions array-name array))))
  :hints (("Goal" :in-theory (e/d (array1p dimensions) (dimensions-intro)))))

(defthm consp-of-dimensions-when-array1p
  (implies (array1p dag-array-name dag-array)
    (consp (dimensions dag-array-name dag-array)))
  :hints (("Goal" :in-theory (e/d (array1p dimensions) (dimensions-intro)))))

(defthmd normalize-dimensions-name
  (implies (syntaxp (not (equal name '':fake-name)))
    (equal (dimensions name l) (dimensions :fake-name l)))
  :hints (("Goal" :in-theory (e/d (dimensions) (dimensions-intro)))))

(defthm dimensions-when-not-consp-of-header-cheap
  (implies (not (consp (header name l)))
    (equal (dimensions name l) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (e/d (dimensions) (dimensions-intro)))))