		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

Svstack-assign

Signature
(svstack-assign k v stack) → new-stack
Arguments: k — Guard (svar-p k).; v — Guard (svex-p v).; stack — Guard (svstack-p stack).
Returns: new-stack — Type (svstack-p new-stack).

Definitions and Theorems

Function: svstack-assign

(defun svstack-assign (k v stack)
  (declare (xargs :guard (and (svar-p k)
                              (svex-p v)
                              (svstack-p stack))))
  (let ((__function__ 'svstack-assign))
    (declare (ignorable __function__))
    (cond ((atom stack)
           (list (svex-fastacons k v nil)))
          ((atom (cdr stack))
           (list (svex-fastacons k v (car stack))))
          ((svex-fastlookup k (car stack))
           (cons (svex-fastacons k v (car stack))
                 (svstack-fix (cdr stack))))
          (t (cons (svex-alist-fix (car stack))
                   (svstack-assign k v (cdr stack)))))))

Theorem: svstack-p-of-svstack-assign

(defthm svstack-p-of-svstack-assign
  (b* ((new-stack (svstack-assign k v stack)))
    (svstack-p new-stack))
  :rule-classes :rewrite)

Theorem: svex-lookup-of-svstack-assign

(defthm svex-lookup-of-svstack-assign
  (b* ((?new-stack (svstack-assign k v stack)))
    (equal (svex-lookup k1 (svstack-to-svex-alist new-stack))
           (if (svar-equiv k1 k)
               (svex-fix v)
             (svex-lookup k1 (svstack-to-svex-alist stack))))))

Theorem: vars-of-svstack-assign

(defthm vars-of-svstack-assign
 (b* ((?new-stack (svstack-assign k v stack)))
   (iff (member q
                (svex-alist-vars (svstack-to-svex-alist new-stack)))
        (or (member q
                    (svex-alist-vars (svstack-to-svex-alist stack)))
            (member q (svex-vars v))))))

Theorem: consp-of-svstack-assign

(defthm consp-of-svstack-assign
  (b* ((?new-stack (svstack-assign k v stack)))
    (implies (consp stack)
             (consp new-stack))))

Theorem: len-of-svstack-assign

(defthm len-of-svstack-assign
  (b* ((?new-stack (svstack-assign k v stack)))
    (<= (len stack) (len new-stack)))
  :rule-classes :linear)

Theorem: svstack-assign-of-svar-fix-k

(defthm svstack-assign-of-svar-fix-k
  (equal (svstack-assign (svar-fix k) v stack)
         (svstack-assign k v stack)))

Theorem: svstack-assign-svar-equiv-congruence-on-k

(defthm svstack-assign-svar-equiv-congruence-on-k
  (implies (svar-equiv k k-equiv)
           (equal (svstack-assign k v stack)
                  (svstack-assign k-equiv v stack)))
  :rule-classes :congruence)

Theorem: svstack-assign-of-svex-fix-v

(defthm svstack-assign-of-svex-fix-v
  (equal (svstack-assign k (svex-fix v) stack)
         (svstack-assign k v stack)))

Theorem: svstack-assign-svex-equiv-congruence-on-v

(defthm svstack-assign-svex-equiv-congruence-on-v
  (implies (svex-equiv v v-equiv)
           (equal (svstack-assign k v stack)
                  (svstack-assign k v-equiv stack)))
  :rule-classes :congruence)

Theorem: svstack-assign-of-svstack-fix-stack

(defthm svstack-assign-of-svstack-fix-stack
  (equal (svstack-assign k v (svstack-fix stack))
         (svstack-assign k v stack)))

Theorem: svstack-assign-svstack-equiv-congruence-on-stack

(defthm svstack-assign-svstack-equiv-congruence-on-stack
  (implies (svstack-equiv stack stack-equiv)
           (equal (svstack-assign k v stack)
                  (svstack-assign k v stack-equiv)))
  :rule-classes :congruence)