records

other

(in-package "ACL2")

include-book

(include-book "misc/total-order" :dir :system)

include-book

(include-book "tools/flag" :dir :system)

ordered-unique-key-alistpfunction

(defun ordered-unique-key-alistp
  (a)
  (declare (xargs :guard (alistp a)))
  (or (null (cdr a))
    (and (<< (caar a) (caadr a))
      (ordered-unique-key-alistp (cdr a)))))

no-nil-val-alistpfunction

(defun no-nil-val-alistp
  (a)
  (declare (xargs :guard (alistp a)))
  (or (null a)
    (and (not (null (cdar a))) (no-nil-val-alistp (cdr a)))))

recordpfunction

(defun recordp
  (r)
  (declare (xargs :guard t))
  (and (alistp r)
    (no-nil-val-alistp r)
    (ordered-unique-key-alistp r)))

mgetfunction

(defun mget
  (a r)
  (declare (xargs :guard (recordp r)))
  (cond ((or (atom r) (<< a (caar r))) nil)
    ((equal a (caar r)) (cdar r))
    (t (mget a (cdr r)))))

mset-consfunction

(defun mset-cons
  (a v r)
  (declare (xargs :guard (recordp r)))
  (if v
    (acons a v r)
    r))

msetfunction

(defun mset
  (a v r)
  (declare (xargs :guard (recordp r)))
  (cond ((atom r) (mset-cons a v r))
    ((<< a (caar r)) (mset-cons a v r))
    ((equal a (caar r)) (mset-cons a v (cdr r)))
    (t (cons (car r) (mset a v (cdr r))))))

recordp-implies-true-listptheorem

(defthm recordp-implies-true-listp
  (implies (recordp x) (true-listp x))
  :rule-classes ((:forward-chaining) (:compound-recognizer)))

recordp-implies-alistptheorem

(defthm recordp-implies-alistp
  (implies (recordp x) (alistp x))
  :rule-classes ((:forward-chaining)))

recordp-implies-no-nil-val-alistptheorem

(defthm recordp-implies-no-nil-val-alistp
  (implies (recordp x) (no-nil-val-alistp x))
  :rule-classes ((:forward-chaining)))

mset-preserves-no-nil-val-alistptheorem

(defthm mset-preserves-no-nil-val-alistp
  (implies (and (alistp r) (no-nil-val-alistp r))
    (no-nil-val-alistp (mset a v r)))
  :hints (("goal" :in-theory (enable <<))))

recordp-implies-ordered-unique-key-alistptheorem

(defthm recordp-implies-ordered-unique-key-alistp
  (implies (recordp x) (ordered-unique-key-alistp x))
  :rule-classes ((:forward-chaining)))

mset-preserves-ordered-unique-key-alistptheorem

(defthm mset-preserves-ordered-unique-key-alistp
  (implies (and (alistp r) (ordered-unique-key-alistp r))
    (ordered-unique-key-alistp (mset a v r)))
  :hints (("goal" :in-theory (enable <<))))

mset-preserves-recordptheorem

(defthm mset-preserves-recordp
  (implies (force (recordp r)) (recordp (mset a v r))))

mset-preserves-record-niltheorem

(defthm mset-preserves-record-nil (recordp (mset a v nil)))

record-<<-of-caartheorem

(defthm record-<<-of-caar
  (implies (and (force (recordp r))
      (<< k a)
      (<< k (caar r))
      (mset a v r))
    (<< k (caar (mset a v r)))))

recordp-of-constheorem

(defthm recordp-of-cons
  (implies (and (consp (double-rewrite e))
      (cdr e)
      (recordp s)
      (<< (car (double-rewrite e)) (caar (double-rewrite s))))
    (recordp (cons e s))))

mget-is-nil-for-<<theorem

(defthm mget-is-nil-for-<<
  (implies (<< a (caar r)) (equal (mget a r) nil))
  :rule-classes :forward-chaining)

non-nil-if-mget-non-niltheorem

(defthm non-nil-if-mget-non-nil
  (implies (mget a r) r)
  :rule-classes :forward-chaining)

mget-of-mset-expandtheorem

(defthm mget-of-mset-expand
  (implies (force (recordp r))
    (equal (mget a (mset b v r))
      (if (equal a b)
        v
        (mget a r)))))

in-theory

(in-theory (disable mget-of-mset-expand))

mget-diff-msettheorem

(defthm mget-diff-mset
  (implies (and (force (recordp r)) (not (equal a b)))
    (equal (mget a (mset b v r)) (mget a r))))

mget-same-msettheorem

(defthm mget-same-mset
  (implies (force (recordp r))
    (equal (mget a (mset a v r)) v)))

mget-of-nil-is-niltheorem

(defthm mget-of-nil-is-nil (not (mget a nil)))

mset-non-nil-cannot-be-niltheorem

(defthm mset-non-nil-cannot-be-nil
  (implies v (mset a v r))
  :rule-classes ((:forward-chaining :trigger-terms ((mset a v r))) (:rewrite :backchain-limit-lst 1)))

mset-same-mgettheorem

(defthm mset-same-mget
  (implies (force (recordp r))
    (equal (mset a (mget a r) r) r)))

mset-diff-msettheorem

(defthm mset-diff-mset
  (implies (and (force (recordp r)) (not (equal a b)))
    (equal (mset b y (mset a x r)) (mset a x (mset b y r))))
  :rule-classes nil)

mset-diff-mset2theorem

(defthm mset-diff-mset2
  (implies (and (syntaxp (or (not (quotep a)) (not (quotep b))))
      (force (recordp r))
      (not (equal a b)))
    (equal (mset b y (mset a x r)) (mset a x (mset b y r))))
  :rule-classes ((:rewrite :loop-stopper ((a b mset)))))

mset-diff-mset1theorem

(defthm mset-diff-mset1
  (implies (and (syntaxp (quotep a))
      (syntaxp (quotep b))
      (syntaxp (term-order (unquote a) (unquote b)))
      (force (recordp r))
      (not (equal a b)))
    (equal (mset b y (mset a x r)) (mset a x (mset b y r))))
  :rule-classes ((:rewrite :loop-stopper nil)))

mset-same-msettheorem

(defthm mset-same-mset
  (implies (force (recordp r))
    (equal (mset a y (mset a x r)) (mset a y r))))

msets-macrofunction

(defun msets-macro
  (r msets)
  (declare (xargs :guard (and (true-listp msets) (evenp (len msets)))))
  (if (endp msets)
    r
    (msets-macro `(mset ,(CAR MSETS) ,(CADR MSETS) ,R)
      (cddr msets))))

msetsmacro

(defmacro msets
  (r &rest msets)
  (declare (xargs :guard (and (true-listp msets) (evenp (len msets)))))
  (msets-macro r msets))

in-theory

(in-theory (disable mset
    mget
    recordp
    ordered-unique-key-alistp
    no-nil-val-alistp))

other

(deftheory minimal-records-theory
  '(recordp ordered-unique-key-alistp
    no-nil-val-alistp
    mset
    mget))

other

(deftheory maximal-records-theory
  '(minimal-records-theory <<))

Included Books