(in-package "ACL2") (defun fieldp (x) (or (symbolp x) (integerp x))) (defthm fieldp-compound-recognizer (iff (fieldp x) (or (symbolp x) (integerp x))) :rule-classes :compound-recognizer) (defthm integerp-forward-chain-fieldp (implies (integerp x) (fieldp x)) :rule-classes :forward-chaining) (defthm symbolp-forward-chain-fieldp (implies (symbolp x) (fieldp x)) :rule-classes :forward-chaining) (in-theory (disable fieldp)) (defun field-< (x y) (if (symbolp x) (and (symbolp y) (symbol-< x y)) (or (symbolp y) (< x y)))) (local (defthm field-<-irreflexive (not (field-< x x)))) (local (defthm field-<-transitive (implies (and (field-< x y) (field-< y z)) (field-< x z)))) (local (defthm field-<-asymmetric (implies (field-< x y) (not (field-< y x))))) (local (defthm field-<-trichotomy (implies (and (fieldp x) (fieldp y) (not (field-< y x))) (iff (field-< x y) (not (equal x y)))))) (in-theory (disable field-<)) ; Ordered field-alist with no nil cdrs: (defun sap (x) (if (atom x) (null x) (and (consp (car x)) (fieldp (caar x)) (cdar x) (if (atom (cdr x)) (null (cdr x)) (and (sap (cdr x)) ;; We unforunately probably ruin tail-recursion here, but at ;; least we can verify the guards. (field-< (caar x) (caadr x))))))) ; Lookup structure: (defun lsp (x) (or (sap x) (and (consp x) (not (lsp (cdr x))) (sap (car x)) (car x)))) (defun g (a x) (cond ((sap x) (cdr (assoc-equal a x))) ((lsp x) (cdr (assoc-equal a (car x)))) (t nil))) ; Ordinary setting, used for non-nil values: (defun s-aux (a v r) (cond ((endp r) (cons (cons a v) nil)) ((equal a (caar r)) (cons (cons a v) (cdr r))) ((field-< a (caar r)) (cons (cons a v) r)) (t (cons (car r) (s-aux a v (cdr r)))))) (defun delete-key (key alist) (cond ((endp alist) alist) ((equal key (caar alist)) (cdr alist)) (t (cons (car alist) (delete-key key (cdr alist)))))) (defun s (a v x) (cond ((sap x) (if (null v) (delete-key a x) (s-aux a v x))) ((not (lsp x)) (if v ;; then make x into the cdr of the returned lookup structure (cons (list (cons a v)) x) ;; else x already is an appropriate result 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))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Interaction properties for s and g; ;;; search for \$\$\$ for main theorems. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (local (defthm not-field-<-x-x (not (field-< x x)) :hints (("Goal" :in-theory (enable field-<))))) (local (defthm delete-key-no-op (implies (and (sap alist) (not (assoc-equal key alist))) (equal (delete-key key alist) alist)))) (local (defthm values-not-nil (implies (sap alist) ;; The order below ooks dangerous, but apparently the prover's ;; heuristics save us. (iff (assoc-equal key alist) (cdr (assoc-equal key alist)))))) (local (defthm key-order-lemma (implies (and (fieldp a) (sap alist) (field-< a (caar alist))) (not (cdr (assoc-equal a alist)))))) (local (defthm s-aux-to-same (implies (and (fieldp a) (sap alist) (cdr (assoc-equal a alist))) (equal (s-aux a (cdr (assoc-equal a alist)) alist) alist)))) ; \$\$\$ A main theorem (defthm s-same-g (implies (force (fieldp a)) (equal (s a (g a r) r) r))) (local (defthm value-s-aux (implies (and (fieldp a) (sap alist)) (equal (cdr (assoc-equal a (s-aux a v alist))) v)))) (local (defthm s-aux-preserves-sap (implies (and (sap x) (fieldp a) v) (sap (s-aux a v x))))) (local (defthm cdr-assoc-equal-delete-key (implies (sap x) (not (cdr (assoc-equal a (delete-key a x))))))) ; G-diff-s should go here, but I forgot it on the first pass, so I'll put ; it at the end where more lemmas are available. (local (defthm sap-delete-key (implies (sap alist) (sap (delete-key a alist))))) (local (defthm sap-forward-to-fieldp-caar (implies (sap alist) (fieldp (caar alist))) :rule-classes :forward-chaining)) ; \$\$\$ A main theorem (defthm g-same-s (implies (force (fieldp a)) (equal (g a (s a v r)) v))) (local (defthm s-aux-s-aux-same (implies (and (fieldp a) (sap alist)) (equal (s-aux a v (s-aux a w alist)) (s-aux a v alist))))) (local (defthm delete-key-s-aux-same (implies (and (fieldp a) (sap alist)) (equal (delete-key a (s-aux a v alist)) (delete-key a alist))))) (local (defthm field-<-s-aux (implies (and (sap alist) (fieldp a) (fieldp b) (field-< b (caar alist)) (not (field-< a b)) (not (equal a b))) (field-< b (caar (s-aux a v alist)))))) (local (defthm value-nil-sufficiency (implies (and (sap alist) (fieldp a) (field-< a (caar alist))) (equal (cdr (assoc-equal a alist)) nil)))) (local (defthm caar-delete-key (implies (sap alist) (equal (caar (delete-key a alist)) (if (eq a (caar alist)) (caadr alist) (caar alist)))))) (local (defthm s-aux-delete-key (implies (sap alist) (equal (s-aux a x (delete-key a alist)) (s-aux a x alist))))) (local (defthm field-<-hack (implies (and (field-< r6 r9) (not (field-< r4 r9)) (not (equal r6 r4)) (fieldp r4) (fieldp r6) (fieldp r9)) (field-< r6 r4)) :hints (("Goal" :in-theory (disable field-<-trichotomy) :use ((:instance field-<-trichotomy (x r6) (y r4))))))) ; \$\$\$ A main theorem (defthm s-same-s (implies (force (fieldp a)) (equal (s a y (s a x r)) (s a y r)))) (local (defthm s-aux-diff-s-aux (implies (and (not (equal a b)) (sap r) x y (fieldp a) (fieldp b)) (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)))) ;; The earlier forward-chaining rule hurts here. :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar))))) (local (defthm sap-s-aux (implies (and (sap x) (fieldp a) v) (sap (s-aux a v x))))) (local (defthm consp-delete-key (implies (sap alist) (equal (consp (delete-key a alist)) (or (consp (cdr alist)) (and (consp alist) (not (equal a (caar alist))))))))) (local (defthm delete-key-delete-key (implies (sap 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 (defthm delete-key-s-aux (implies (and (not (equal a b)) (sap r) x (fieldp a) (fieldp b)) (equal (delete-key b (s-aux a x r)) (s-aux a x (delete-key b r)))) ;; The earlier forward-chaining rule hurts here. :hints (("Goal" :in-theory (disable sap-forward-to-fieldp-caar))))) (local (defthm delete-key-nil (implies (not (delete-key a x)) (not (delete-key a (delete-key b x)))))) ; \$\$\$ A main theorem (defthm s-diff-s (implies (and (force (fieldp a)) (force (fieldp b)) (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))))) (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 (defthm assoc-equal-delete-key-different (implies (not (equal a b)) (equal (assoc-equal a (delete-key b alist)) (assoc-equal a alist))))) ; \$\$\$ A main theorem (defthm g-diff-s (implies (and (force (fieldp a)) (force (fieldp b)) (not (equal a b))) (equal (g a (s b v r)) (g a r)))) ;;;; some simple macros for defining sets and gets.. (in-theory (disable s g)) (defmacro <- (x a) `(g ,a ,x)) (defmacro -> (x a v) `(s ,a ,v ,x)) (defun update-macro (upds result) (declare (xargs :guard (keyword-value-listp upds))) (if (endp upds) result (update-macro (cddr upds) (list 's (car upds) (cadr upds) result)))) (defmacro update (old &rest updates) (declare (xargs :guard (keyword-value-listp updates))) (update-macro updates old))