		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Assigns->absindexed

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

Definitions and Theorems

Function: assigns->absindexed

(defun assigns->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (assigns-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (assigns-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'assigns->absindexed))
   (declare (ignorable __function__))
   (b* ((x (assigns-fix x))
        ((when (atom x)) (mv nil nil))
        ((cons lhs (driver rhs)) (car x))
        ((mv fails1 lhs)
         (lhs->absindexed lhs scope moddb))
        ((mv fails2 val)
         (svex->absindexed rhs.value scope moddb))
        ((mv fails3 rest)
         (assigns->absindexed (cdr x)
                              scope moddb)))
     (mv (append-without-guard fails1 fails2 fails3)
         (cons (cons lhs (change-driver rhs :value val))
               rest)))))

Theorem: svarlist-p-of-assigns->absindexed.fails

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

Theorem: assigns-p-of-assigns->absindexed.xx

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

Theorem: assigns->absindexed-of-assigns-fix-x

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

Theorem: assigns->absindexed-assigns-equiv-congruence-on-x

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

Theorem: assigns->absindexed-of-modscope-fix-scope

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

Theorem: assigns->absindexed-modscope-equiv-congruence-on-scope

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

Theorem: assigns->absindexed-of-moddb-fix-moddb

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

Theorem: assigns->absindexed-moddb-equiv-congruence-on-moddb

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

Theorem: assigns-boundedp-of-assigns->absindexed

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