		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Constraintlist->absindexed

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

Definitions and Theorems

Function: constraintlist->absindexed

(defun constraintlist->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (constraintlist-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (constraintlist-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'constraintlist->absindexed))
   (declare (ignorable __function__))
   (b* (((when (atom x)) (mv nil nil))
        ((constraint x1) (car x))
        ((mv fails1 new-cond)
         (svex->absindexed x1.cond scope moddb))
        ((mv fails2 rest)
         (constraintlist->absindexed (cdr x)
                                     scope moddb)))
     (mv (append-without-guard fails1 fails2)
         (cons (change-constraint x1 :cond new-cond)
               rest)))))

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

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

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

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

Theorem: constraintlist-boundedp-of-constraintlist->absindexed

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

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

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

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

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

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

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

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

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

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

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

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

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