		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svex-alist->absindexed

Signature
(svex-alist->absindexed x scope moddb) → (mv fails xx)
Arguments: x — Guard (svex-alist-p x).; scope — Guard (modscope-p scope).; moddb — Guard (moddb-ok moddb).
Returns: fails — Type (svarlist-p fails).; xx — Type (svex-alist-p xx).

Definitions and Theorems

Function: svex-alist->absindexed

(defun svex-alist->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (svex-alist-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (svex-alist-vars x)
                              (modscope-local-bound scope moddb))
        (svarlist-idxaddr-okp (svex-alist-keys x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'svex-alist->absindexed))
   (declare (ignorable __function__))
   (b* (((when (atom x)) (mv nil nil))
        ((unless (mbt (and (consp (car x))
                           (svar-p (caar x)))))
         (svex-alist->absindexed (cdr x)
                                 scope moddb))
        ((cons key val) (car x))
        ((mv ok new-key)
         (svar->absindexed key scope moddb))
        ((unless ok)
         (b* (((mv fails1 rest)
               (svex-alist->absindexed (cdr x)
                                       scope moddb)))
           (mv (cons (svar-fix key) fails1) rest)))
        ((mv fails2 new-val)
         (svex->absindexed val scope moddb))
        ((mv fails3 rest)
         (svex-alist->absindexed (cdr x)
                                 scope moddb)))
     (mv (append-without-guard fails2 fails3)
         (cons (cons new-key new-val) rest)))))

Theorem: svarlist-p-of-svex-alist->absindexed.fails

(defthm svarlist-p-of-svex-alist->absindexed.fails
  (b* (((mv ?fails ?xx)
        (svex-alist->absindexed x scope moddb)))
    (svarlist-p fails))
  :rule-classes :rewrite)

Theorem: svex-alist-p-of-svex-alist->absindexed.xx

(defthm svex-alist-p-of-svex-alist->absindexed.xx
  (b* (((mv ?fails ?xx)
        (svex-alist->absindexed x scope moddb)))
    (svex-alist-p xx))
  :rule-classes :rewrite)

Theorem: svex-alist-boundedp-of-svex-alist->absindexed

(defthm svex-alist-boundedp-of-svex-alist->absindexed
 (b* (((mv ?fails res)
       (svex-alist->absindexed x scope moddb)))
  (implies
      (and (svarlist-idxaddr-okp (svex-alist-vars x)
                                 (modscope-local-bound scope moddb))
           (svarlist-idxaddr-okp (svex-alist-keys x)
                                 (modscope-local-bound scope moddb))
           (modscope-okp scope moddb)
           (moddb-ok moddb))
      (and (svarlist-boundedp (svex-alist-vars res)
                              (modscope-top-bound scope moddb))
           (svarlist-boundedp (svex-alist-keys res)
                              (modscope-top-bound scope moddb))))))

Theorem: svex-alist->absindexed-of-svex-alist-fix-x

(defthm svex-alist->absindexed-of-svex-alist-fix-x
  (equal (svex-alist->absindexed (svex-alist-fix x)
                                 scope moddb)
         (svex-alist->absindexed x scope moddb)))

Theorem: svex-alist->absindexed-svex-alist-equiv-congruence-on-x

(defthm svex-alist->absindexed-svex-alist-equiv-congruence-on-x
  (implies (svex-alist-equiv x x-equiv)
           (equal (svex-alist->absindexed x scope moddb)
                  (svex-alist->absindexed x-equiv scope moddb)))
  :rule-classes :congruence)

Theorem: svex-alist->absindexed-of-modscope-fix-scope

(defthm svex-alist->absindexed-of-modscope-fix-scope
  (equal (svex-alist->absindexed x (modscope-fix scope)
                                 moddb)
         (svex-alist->absindexed x scope moddb)))

Theorem: svex-alist->absindexed-modscope-equiv-congruence-on-scope

(defthm svex-alist->absindexed-modscope-equiv-congruence-on-scope
  (implies (modscope-equiv scope scope-equiv)
           (equal (svex-alist->absindexed x scope moddb)
                  (svex-alist->absindexed x scope-equiv moddb)))
  :rule-classes :congruence)

Theorem: svex-alist->absindexed-of-moddb-fix-moddb

(defthm svex-alist->absindexed-of-moddb-fix-moddb
  (equal (svex-alist->absindexed x scope (moddb-fix moddb))
         (svex-alist->absindexed x scope moddb)))

Theorem: svex-alist->absindexed-moddb-equiv-congruence-on-moddb

(defthm svex-alist->absindexed-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (svex-alist->absindexed x scope moddb)
                  (svex-alist->absindexed x scope moddb-equiv)))
  :rule-classes :congruence)