		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Lhs-named->indexed

Signature
(lhs-named->indexed x modidx moddb) → (mv errmsg xx)
Arguments: x — Guard (lhs-p x).; modidx — Guard (natp modidx).; moddb — Guard (moddb-ok moddb).
Returns: xx — Type (lhs-p xx).

Definitions and Theorems

Function: lhs-named->indexed

(defun lhs-named->indexed (x modidx moddb)
  (declare (xargs :stobjs (moddb)))
  (declare (xargs :guard (and (lhs-p x)
                              (natp modidx)
                              (moddb-ok moddb))))
  (declare (xargs :guard (and (svarlist-addr-p (lhs-vars x))
                              (< modidx (moddb->nmods moddb)))))
  (let ((__function__ 'lhs-named->indexed))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv nil nil))
         ((lhrange xf) (car x))
         ((mv err2 rest)
          (lhs-named->indexed (cdr x)
                              modidx moddb)))
      (lhatom-case
           xf.atom :z
           (mv err2 (cons (lhrange-fix (car x)) rest))
           :var
           (b* (((mv err1 name)
                 (svar-named->indexed xf.atom.name modidx moddb)))
             (mv (or err1 err2)
                 (cons (lhrange xf.w (lhatom-var name xf.atom.rsh))
                       rest)))))))

Theorem: lhs-p-of-lhs-named->indexed.xx

(defthm lhs-p-of-lhs-named->indexed.xx
  (b* (((mv ?errmsg ?xx)
        (lhs-named->indexed x modidx moddb)))
    (lhs-p xx))
  :rule-classes :rewrite)

Theorem: lhs-named->indexed-of-lhs-fix-x

(defthm lhs-named->indexed-of-lhs-fix-x
  (equal (lhs-named->indexed (lhs-fix x)
                             modidx moddb)
         (lhs-named->indexed x modidx moddb)))

Theorem: lhs-named->indexed-lhs-equiv-congruence-on-x

(defthm lhs-named->indexed-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-named->indexed x modidx moddb)
                  (lhs-named->indexed x-equiv modidx moddb)))
  :rule-classes :congruence)

Theorem: lhs-named->indexed-of-nfix-modidx

(defthm lhs-named->indexed-of-nfix-modidx
  (equal (lhs-named->indexed x (nfix modidx)
                             moddb)
         (lhs-named->indexed x modidx moddb)))

Theorem: lhs-named->indexed-nat-equiv-congruence-on-modidx

(defthm lhs-named->indexed-nat-equiv-congruence-on-modidx
  (implies (nat-equiv modidx modidx-equiv)
           (equal (lhs-named->indexed x modidx moddb)
                  (lhs-named->indexed x modidx-equiv moddb)))
  :rule-classes :congruence)

Theorem: lhs-named->indexed-of-moddb-fix-moddb

(defthm lhs-named->indexed-of-moddb-fix-moddb
  (equal (lhs-named->indexed x modidx (moddb-fix moddb))
         (lhs-named->indexed x modidx moddb)))

Theorem: lhs-named->indexed-moddb-equiv-congruence-on-moddb

(defthm lhs-named->indexed-moddb-equiv-congruence-on-moddb
  (implies (moddb-equiv moddb moddb-equiv)
           (equal (lhs-named->indexed x modidx moddb)
                  (lhs-named->indexed x modidx moddb-equiv)))
  :rule-classes :congruence)

Theorem: lhs-idxaddr-okp-of-lhs-named->indexed

(defthm lhs-idxaddr-okp-of-lhs-named->indexed
 (b* (((mv err ans)
       (lhs-named->indexed x modidx moddb)))
  (implies
       (and (moddb-ok moddb)
            (< (nfix modidx)
               (nfix (nth *moddb->nmods* moddb)))
            (not err))
       (svarlist-idxaddr-okp (lhs-vars ans)
                             (moddb-mod-totalwires modidx moddb)))))