		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Svar-map->absindexed

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

Definitions and Theorems

Function: svar-map->absindexed

(defun svar-map->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (svar-map-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (svar-map-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'svar-map->absindexed))
   (declare (ignorable __function__))
   (b* ((x (svar-map-fix x))
        ((when (atom x)) (mv nil nil))
        ((cons lhs rhs) (car x))
        ((mv ok1 lhs)
         (svar->absindexed lhs scope moddb))
        ((mv ok2 rhs)
         (svar->absindexed rhs scope moddb))
        ((mv fails3 rest)
         (svar-map->absindexed (cdr x)
                               scope moddb)))
     (mv (append-without-guard (and (not ok1) (list lhs))
                               (and (not ok2) (list rhs))
                               fails3)
         (if (and ok1 ok2)
             (cons (cons lhs rhs) rest)
           rest)))))

Theorem: svarlist-p-of-svar-map->absindexed.fails

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

Theorem: svar-map-p-of-svar-map->absindexed.xx

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

Theorem: svar-map->absindexed-of-svar-map-fix-x

(defthm svar-map->absindexed-of-svar-map-fix-x
  (equal (svar-map->absindexed (svar-map-fix x)
                               scope moddb)
         (svar-map->absindexed x scope moddb)))

Theorem: svar-map->absindexed-svar-map-equiv-congruence-on-x

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

Theorem: svar-map->absindexed-of-modscope-fix-scope

(defthm svar-map->absindexed-of-modscope-fix-scope
  (equal (svar-map->absindexed x (modscope-fix scope)
                               moddb)
         (svar-map->absindexed x scope moddb)))

Theorem: svar-map->absindexed-modscope-equiv-congruence-on-scope

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

Theorem: svar-map->absindexed-of-moddb-fix-moddb

(defthm svar-map->absindexed-of-moddb-fix-moddb
  (equal (svar-map->absindexed x scope (moddb-fix moddb))
         (svar-map->absindexed x scope moddb)))

Theorem: svar-map->absindexed-moddb-equiv-congruence-on-moddb

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

Theorem: svar-map-boundedp-of-svar-map->absindexed

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