		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhspairs->absindexed

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

Definitions and Theorems

Function: lhspairs->absindexed

(defun lhspairs->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (lhspairs-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (lhspairs-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'lhspairs->absindexed))
  (declare (ignorable __function__))
  (mbe :logic
       (b* ((x (lhspairs-fix x))
            ((when (atom x)) (mv nil nil))
            ((cons lhs rhs) (car x))
            ((mv fails1 lhs)
             (lhs->absindexed lhs scope moddb))
            ((mv fails2 rhs)
             (lhs->absindexed rhs scope moddb))
            ((mv fails3 rest)
             (lhspairs->absindexed (cdr x)
                                   scope moddb)))
         (mv (append-without-guard fails1 fails2 fails3)
             (cons (cons lhs rhs) rest)))
       :exec
       (if (atom x)
           (mv nil nil)
         (b* (((acl2::local-stobjs nrev nrev1)
               (mv fails ans nrev nrev1))
              ((mv nrev nrev1)
               (lhspairs->absindexed-nrev x scope moddb nrev nrev1))
              ((mv fails nrev)
               (acl2::nrev-finish nrev))
              ((mv ans nrev1)
               (acl2::nrev-finish nrev1)))
           (mv fails ans nrev nrev1))))))

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

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

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

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

Theorem: lhspairs->absindexed-true-listp

(defthm lhspairs->absindexed-true-listp
  (b* (((mv ?fails ?xx)
        (lhspairs->absindexed x scope moddb)))
    (true-listp xx))
  :rule-classes :type-prescription)

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: lhspairs-boundedp-of-lhspairs->absindexed

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