		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscope-update-subscope

Signature
(vl-elabscope-update-subscope key val x) → new-x
Arguments: key — Guard (vl-elabkey-p key).; val — Guard (vl-elabscope-p val).; x — Guard (vl-elabscope-p x).
Returns: new-x — Type (vl-elabscope-p new-x).

Definitions and Theorems

Function: vl-elabscope-update-subscope

(defun vl-elabscope-update-subscope (key val x)
  (declare (xargs :guard (and (vl-elabkey-p key)
                              (vl-elabscope-p val)
                              (vl-elabscope-p x))))
  (let ((__function__ 'vl-elabscope-update-subscope))
    (declare (ignorable __function__))
    (change-vl-elabscope
         x
         :subscopes (hons-acons (vl-elabkey-fix key)
                                (vl-elabscope-fix val)
                                (vl-elabscope->subscopes x)))))

Theorem: vl-elabscope-p-of-vl-elabscope-update-subscope

(defthm vl-elabscope-p-of-vl-elabscope-update-subscope
  (b* ((new-x (vl-elabscope-update-subscope key val x)))
    (vl-elabscope-p new-x))
  :rule-classes :rewrite)

Theorem: vl-elabscope-update-subscope-of-vl-elabkey-fix-key

(defthm vl-elabscope-update-subscope-of-vl-elabkey-fix-key
  (equal (vl-elabscope-update-subscope (vl-elabkey-fix key)
                                       val x)
         (vl-elabscope-update-subscope key val x)))

Theorem: vl-elabscope-update-subscope-vl-elabkey-equiv-congruence-on-key

(defthm
    vl-elabscope-update-subscope-vl-elabkey-equiv-congruence-on-key
  (implies (vl-elabkey-equiv key key-equiv)
           (equal (vl-elabscope-update-subscope key val x)
                  (vl-elabscope-update-subscope key-equiv val x)))
  :rule-classes :congruence)

Theorem: vl-elabscope-update-subscope-of-vl-elabscope-fix-val

(defthm vl-elabscope-update-subscope-of-vl-elabscope-fix-val
  (equal (vl-elabscope-update-subscope key (vl-elabscope-fix val)
                                       x)
         (vl-elabscope-update-subscope key val x)))

Theorem: vl-elabscope-update-subscope-vl-elabscope-equiv-congruence-on-val

(defthm
  vl-elabscope-update-subscope-vl-elabscope-equiv-congruence-on-val
  (implies (vl-elabscope-equiv val val-equiv)
           (equal (vl-elabscope-update-subscope key val x)
                  (vl-elabscope-update-subscope key val-equiv x)))
  :rule-classes :congruence)

Theorem: vl-elabscope-update-subscope-of-vl-elabscope-fix-x

(defthm vl-elabscope-update-subscope-of-vl-elabscope-fix-x
  (equal (vl-elabscope-update-subscope key val (vl-elabscope-fix x))
         (vl-elabscope-update-subscope key val x)))

Theorem: vl-elabscope-update-subscope-vl-elabscope-equiv-congruence-on-x

(defthm
    vl-elabscope-update-subscope-vl-elabscope-equiv-congruence-on-x
  (implies (vl-elabscope-equiv x x-equiv)
           (equal (vl-elabscope-update-subscope key val x)
                  (vl-elabscope-update-subscope key val x-equiv)))
  :rule-classes :congruence)