Filtering...

records0

books/misc/records0

Included Books

total-order
other
(in-package "ACL2")
include-book
(include-book "total-order")
rcdpfunction
(defun rcdp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (consp (car x))
      (cdar x)
      (if (atom (cdr x))
        (null (cdr x))
        (and (rcdp (cdr x)) (<< (caar x) (caadr x)))))))
lspfunction
(defun lsp
  (x)
  (declare (xargs :guard t))
  (or (rcdp x)
    (and (consp x) (not (lsp (cdr x))) (rcdp (car x)) (car x))))
gfunction
(defun g
  (a x)
  (declare (xargs :guard t))
  (cond ((rcdp x) (cdr (assoc-equal a x)))
    ((lsp x) (cdr (assoc-equal a (car x))))
    (t nil)))
s-auxfunction
(defun s-aux
  (a v r)
  (declare (xargs :guard (rcdp r)))
  (cond ((endp r) (cons (cons a v) nil))
    ((equal a (caar r)) (cons (cons a v) (cdr r)))
    ((<< a (caar r)) (cons (cons a v) r))
    (t (cons (car r) (s-aux a v (cdr r))))))
delete-keyfunction
(defun delete-key
  (key alist)
  (declare (xargs :guard (rcdp alist)))
  (cond ((endp alist) alist)
    ((equal key (caar alist)) (cdr alist))
    (t (cons (car alist) (delete-key key (cdr alist))))))
sfunction
(defun s
  (a v x)
  (declare (xargs :guard t))
  (cond ((rcdp x) (if (null v)
        (delete-key a x)
        (s-aux a v x)))
    ((not (lsp x)) (if v
        (cons (list (cons a v)) x)
        x))
    ((null v) (if (and (null (cdr (car x))) (equal (caar (car x)) a))
        (cdr x)
        (cons (delete-key a (car x)) (cdr x))))
    (t (cons (s-aux a v (car x)) (cdr x)))))
local
(local (defthm delete-key-no-op
    (implies (and (rcdp alist) (not (assoc-equal key alist)))
      (equal (delete-key key alist) alist))))
local
(local (defthm values-not-nil
    (implies (rcdp alist)
      (iff (assoc-equal key alist) (cdr (assoc-equal key alist))))))
local
(local (defthm key-order-lemma
    (implies (and (rcdp alist) (<< a (caar alist)))
      (not (cdr (assoc-equal a alist))))))
local
(local (defthm s-aux-to-same
    (implies (and (rcdp alist) (cdr (assoc-equal a alist)))
      (equal (s-aux a (cdr (assoc-equal a alist)) alist) alist))))
local
(local (defthm value-s-aux
    (implies (rcdp alist)
      (equal (cdr (assoc-equal a (s-aux a v alist))) v))))
local
(local (defthm s-aux-preserves-rcdp
    (implies (and (rcdp x) v) (rcdp (s-aux a v x)))))
local
(local (defthm cdr-assoc-equal-delete-key
    (implies (rcdp x)
      (not (cdr (assoc-equal a (delete-key a x)))))))
local
(local (defthm rcdp-delete-key
    (implies (rcdp alist) (rcdp (delete-key a alist)))))
local
(local (defthm s-aux-s-aux-same
    (implies (rcdp alist)
      (equal (s-aux a v (s-aux a w alist)) (s-aux a v alist)))))
local
(local (defthm delete-key-s-aux-same
    (implies (rcdp alist)
      (equal (delete-key a (s-aux a v alist))
        (delete-key a alist)))))
local
(local (defthm <<-s-aux
    (implies (and (rcdp alist)
        (<< b (caar alist))
        (not (<< a b))
        (not (equal a b)))
      (<< b (caar (s-aux a v alist))))))
local
(local (defthm value-nil-sufficiency
    (implies (and (rcdp alist) (<< a (caar alist)))
      (equal (cdr (assoc-equal a alist)) nil))))
local
(local (defthm caar-delete-key
    (implies (rcdp alist)
      (equal (caar (delete-key a alist))
        (if (eq a (caar alist))
          (caadr alist)
          (caar alist))))))
local
(local (defthm s-aux-delete-key
    (implies (rcdp alist)
      (equal (s-aux a x (delete-key a alist)) (s-aux a x alist)))))
local
(local (defthm <<-hack
    (implies (and (<< r6 r9) (not (<< r4 r9)) (not (equal r6 r4)))
      (<< r6 r4))
    :hints (("Goal" :in-theory (disable <<-trichotomy)
       :use ((:instance <<-trichotomy (x r6) (y r4)))))))
local
(local (defthm s-aux-diff-s-aux
    (implies (and (not (equal a b)) (rcdp r) x y)
      (equal (s-aux b y (s-aux a x r)) (s-aux a x (s-aux b y r))))
    :rule-classes ((:rewrite :loop-stopper ((b a s-aux))))))
local
(local (defthm rcdp-s-aux
    (implies (and (rcdp x) v) (rcdp (s-aux a v x)))))
local
(local (defthm consp-delete-key
    (implies (rcdp alist)
      (equal (consp (delete-key a alist))
        (or (consp (cdr alist))
          (and (consp alist) (not (equal a (caar alist)))))))))
local
(local (defthm delete-key-delete-key
    (implies (rcdp r)
      (equal (delete-key b (delete-key a r))
        (delete-key a (delete-key b r))))
    :rule-classes ((:rewrite :loop-stopper ((b a delete-key))))))
local
(local (defthm delete-key-s-aux
    (implies (and (not (equal a b)) (rcdp r) x)
      (equal (delete-key b (s-aux a x r))
        (s-aux a x (delete-key b r))))))
local
(local (defthm delete-key-nil
    (implies (not (delete-key a x))
      (not (delete-key a (delete-key b x))))))
local
(local (defthm assoc-equal-s-aux-different
    (implies (not (equal a b))
      (equal (assoc-equal a (s-aux b v alist))
        (assoc-equal a alist)))))
local
(local (defthm assoc-equal-delete-key-different
    (implies (not (equal a b))
      (equal (assoc-equal a (delete-key b alist))
        (assoc-equal a alist)))))
bad-fieldfunction
(defun bad-field
  (r1 r2)
  (declare (xargs :guard (and (rcdp r1) (rcdp r2))))
  (cond ((endp r1) (caar r2))
    ((endp r2) (caar r1))
    ((equal (car r1) (car r2)) (bad-field (cdr r1) (cdr r2)))
    ((<< (caar r1) (caar r2)) (caar r1))
    (t (caar r2))))
local
(local (defthm assoc-eq-symbol<
    (implies (and (rcdp s) (<< field (caar s)))
      (equal (assoc-equal field s) nil))))
access-of-nil-is-niltheorem
(defthm access-of-nil-is-nil (not (g a nil)))
record-set-cannot-be-niltheorem
(defthm record-set-cannot-be-nil (implies v (s a v r)))
record-get-non-nil-cannot-be-niltheorem
(defthm record-get-non-nil-cannot-be-nil
  (implies (g a r) r)
  :rule-classes :forward-chaining)
s-same-gtheorem
(defthm s-same-g (equal (s a (g a r) r) r))
g-same-stheorem
(defthm g-same-s (equal (g a (s a v r)) v))
s-same-stheorem
(defthm s-same-s (equal (s a y (s a x r)) (s a y r)))
s-diff-stheorem
(defthm s-diff-s
  (implies (not (equal a b))
    (equal (s b y (s a x r)) (s a x (s b y r))))
  :rule-classes ((:rewrite :loop-stopper ((b a s)))))
g-diff-stheorem
(defthm g-diff-s
  (implies (not (equal a b)) (equal (g a (s b v r)) (g a r))))
s-preserves-recordptheorem
(defthm s-preserves-recordp
  (implies (rcdp r) (rcdp (s a v r)))
  :rule-classes ((:forward-chaining :trigger-terms ((s a v r))) :rewrite))
rcdp-equality-sufficiencytheorem
(defthm rcdp-equality-sufficiency
  (implies (and (rcdp r1) (rcdp r2))
    (equal (equal r1 r2)
      (let ((field (bad-field r1 r2)))
        (equal (g field r1) (g field r2)))))
  :hints (("Goal" :induct (bad-field r1 r2))))
in-theory
(in-theory (disable s g bad-field rcdp-equality-sufficiency))