header

(in-package "ACL2")

(in-theory (disable header))

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

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

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

(defthm consp-of-header-when-array1p-free
  (implies (array1p name2 l) (consp (header name l)))
  :hints (("Goal" :in-theory (enable array1p header))))

(defthm consp-of-header-when-array1p
  (implies (array1p name array) (consp (header name array)))
  :hints (("Goal" :in-theory (enable array1p header))))

(defthmd keyword-value-listp-of-cdr-of-header-when-array1p
  (implies (array1p array-name array)
    (keyword-value-listp (cdr (header array-name array))))
  :hints (("Goal" :in-theory (enable array1p header))))

(defthm equal-of-header-and-car-of-header
  (iff (equal :header (car (header array-name array)))
    (header array-name array))
  :hints (("Goal" :in-theory (enable header))))

(defthm header-of-cons
  (equal (header array-name (cons entry alist))
    (if (eq :header (car entry))
      entry
      (header array-name alist)))
  :hints (("Goal" :in-theory (enable header))))

(defthm header-of-nil
  (equal (header name nil) nil)
  :hints (("Goal" :in-theory (enable header))))

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

(defthm car-of-header
  (equal (car (header name l))
    (if (header name l)
      :header nil)))