library-support

(in-package "ACL2")

(include-book "acl2s/defdata/records" :dir :system)

(defconst *tag* :0tag)

(defthm records-lemma-acl2-count
  (<= (acl2-count (mget k r)) (acl2-count r))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes :linear)

(defun good-map (x) (recordp x))

(defun non-empty-good-map
  (x)
  (declare (xargs :guard t))
  (and (consp x) (recordp x)))

(defthm records-acl2-count-linear-arith-<
  (implies (mget k r)
    (< (acl2-count (mget k r)) (acl2-count r)))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes :linear)

(defthm records-acl2-count
  (implies (consp r)
    (< (acl2-count (mget k r)) (acl2-count r)))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes :linear)

(defun map-identity2
  (a x)
  "for map elim rule -- dummy destructor"
  (declare (ignore a))
  x)

(defthmd map-elim-rule
  (implies (recordp r)
    (equal (mset k (mget k r) (map-identity2 k r)) r))
  :rule-classes :elim)

(defun list-identity2
  (a x)
  "for list elim rule -- dummy destructor"
  (declare (ignore a))
  x)

(defthmd list-elim-rule
  (implies (and (true-listp x) (natp i) (< i (len x)))
    (equal (update-nth i (nth i x) (list-identity2 i x)) x))
  :hints (("Goal" :in-theory (e/d (update-nth len nth) (true-listp (tau-system)))))
  :rule-classes :elim)

(defun put-assoc-equal-elim-rule-version
  (e x)
  "put entry e=(key . value) in its rightful place in alist x"
  (put-assoc-equal (car e) (cdr e) x))

(defun alist-identity2
  (a x)
  "for alist elim rule -- dummy destructor"
  (declare (ignore a))
  x)

(defthm assoc-eq-answer-car
  (implies (assoc-equal k x)
    (equal (car (assoc-equal k x)) k)))

(defthmd alist-elim-rule
  (implies (and (alistp x) (assoc-equal k x))
    (equal (put-assoc-equal-elim-rule-version (assoc-equal k x)
        (alist-identity2 k x))
      x))
  :rule-classes :elim)

(defthm mset-aux-consp
  (implies v (consp (mset a v r)))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes ((:forward-chaining :trigger-terms ((mset a v r))) (:rewrite :backchain-limit-lst 1)))

(defthm s-nil-no-op
  (implies (and (force (recordp r)) (not (mget a r)))
    (equal (mset a nil r) r))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes ((:forward-chaining :trigger-terms ((mset a nil r))) (:rewrite :backchain-limit-lst 1)))

(defthm field-not-empty-implies-record-not-empty1
  (implies (mget a r) (consp r))
  :hints (("goal" :in-theory (enable minimal-records-theory)))
  :rule-classes ((:forward-chaining) (:rewrite :backchain-limit-lst 0)))

(defthmd s-diff-entry-non-empty-good-map-is-consp2
  (implies (and (not (equal a b)) (mget a r))
    (consp (mset b v r)))
  :hints (("goal" :in-theory (enable mset
       mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes ((:forward-chaining :trigger-terms ((mset b v r))) (:rewrite :backchain-limit-lst 1)))

(defthmd s-diff-entry-non-empty-good-map-is-consp-tag
  (implies (and (not (equal *tag* b)) (mget *tag* r))
    (consp (mset b v r)))
  :hints (("goal" :in-theory (enable mset
       mget
       recordp
       no-nil-val-alistp
       ordered-unique-key-alistp)))
  :rule-classes ((:forward-chaining :trigger-terms ((mset b v r))) (:rewrite :backchain-limit-lst 1)))

(defthmd s-diff-entry-non-empty-good-map-is-non-nil
  (implies (and (mget a r) (not (equal a b))) (mset b v r))
  :hints (("goal" :use ((:instance s-diff-entry-non-empty-good-map-is-consp2))))
  :rule-classes ((:forward-chaining :trigger-terms ((mset b v r))) (:rewrite :backchain-limit-lst 1)))

(defthmd s-diff-entry-tag-is-non-nil
  (implies (and (mget *tag* r) (not (equal b *tag*)))
    (mset b v r))
  :rule-classes ((:forward-chaining :trigger-terms ((mset b v r))) (:rewrite :backchain-limit-lst 1)))

(defthm non-empty-record-consp
  (implies (and (recordp r) r) (consp r))
  :hints (("goal" :in-theory (enable recordp)))
  :rule-classes ((:forward-chaining)))

(defthm non-empty-record-consp-car
  (implies (and (recordp r) (car r)) (consp (car r)))
  :hints (("goal" :in-theory (enable recordp)))
  :rule-classes ((:forward-chaining)))