		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhs->absindexed

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

Definitions and Theorems

Function: lhs->absindexed

(defun lhs->absindexed (x scope moddb)
 (declare (xargs :stobjs (moddb)))
 (declare (xargs :guard (and (lhs-p x)
                             (modscope-p scope)
                             (moddb-ok moddb))))
 (declare
  (xargs
   :guard
   (and (modscope-okp scope moddb)
        (svarlist-idxaddr-okp (lhs-vars x)
                              (modscope-local-bound scope moddb)))))
 (let ((__function__ 'lhs->absindexed))
  (declare (ignorable __function__))
  (b* (((when (atom x)) (mv nil nil))
       ((lhrange xf) (car x))
       ((mv rest-fails rest)
        (lhs->absindexed (cdr x) scope moddb)))
   (lhatom-case
      xf.atom :z
      (mv rest-fails
          (cons (lhrange-fix (car x)) rest))
      :var
      (b* (((mv ok var)
            (svar->absindexed xf.atom.name scope moddb)))
        (if ok (mv rest-fails
                   (cons (lhrange xf.w (lhatom-var var xf.atom.rsh))
                         rest))
          (mv (cons xf.atom.name rest-fails)
              (cons (make-lhrange :w xf.w :atom (lhatom-z))
                    rest))))))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: lhs-boundedp-of-lhs->absindexed

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