		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Lstate-renamevarp

Variable renaming relation over local states.

Signature
(lstate-renamevarp old new ren) → yes/no
Arguments: old — Guard (lstatep old).; new — Guard (lstatep new).; ren — Guard (renamingp ren).
Returns: yes/no — Type (booleanp yes/no).

The renaming must cover all the variables in the old and new local states, i.e. every variable in the states must be in the renaming. Furthermore, the two states must agree on the renaming: see lstate-match-renamevarp.

Definitions and Theorems

Function: lstate-renamevarp

(defun lstate-renamevarp (old new ren)
  (declare (xargs :guard (and (lstatep old)
                              (lstatep new)
                              (renamingp ren))))
  (let ((__function__ 'lstate-renamevarp))
    (declare (ignorable __function__))
    (and (subset (omap::keys (lstate-fix old))
                 (renaming-old ren))
         (subset (omap::keys (lstate-fix new))
                 (renaming-new ren))
         (lstate-match-renamevarp old new ren))))

Theorem: booleanp-of-lstate-renamevarp

(defthm booleanp-of-lstate-renamevarp
  (b* ((yes/no (lstate-renamevarp old new ren)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: same-defined-when-lstate-renamevarp

(defthm same-defined-when-lstate-renamevarp
  (implies (and (lstatep old-lstate)
                (lstatep new-lstate)
                (identifierp old-var)
                (identifierp new-var)
                (lstate-renamevarp old-lstate new-lstate ren)
                (member-equal (cons old-var new-var)
                              (renaming->list ren)))
           (iff (in old-var (omap::keys old-lstate))
                (in new-var (omap::keys new-lstate)))))

Theorem: lstate-renamevarp-of-nil

(defthm lstate-renamevarp-of-nil
  (lstate-renamevarp nil nil (renaming nil)))

Theorem: lstate-renamevarp-of-lstate-fix-old

(defthm lstate-renamevarp-of-lstate-fix-old
  (equal (lstate-renamevarp (lstate-fix old)
                            new ren)
         (lstate-renamevarp old new ren)))

Theorem: lstate-renamevarp-lstate-equiv-congruence-on-old

(defthm lstate-renamevarp-lstate-equiv-congruence-on-old
  (implies (lstate-equiv old old-equiv)
           (equal (lstate-renamevarp old new ren)
                  (lstate-renamevarp old-equiv new ren)))
  :rule-classes :congruence)

Theorem: lstate-renamevarp-of-lstate-fix-new

(defthm lstate-renamevarp-of-lstate-fix-new
  (equal (lstate-renamevarp old (lstate-fix new)
                            ren)
         (lstate-renamevarp old new ren)))

Theorem: lstate-renamevarp-lstate-equiv-congruence-on-new

(defthm lstate-renamevarp-lstate-equiv-congruence-on-new
  (implies (lstate-equiv new new-equiv)
           (equal (lstate-renamevarp old new ren)
                  (lstate-renamevarp old new-equiv ren)))
  :rule-classes :congruence)

Theorem: lstate-renamevarp-of-renaming-fix-ren

(defthm lstate-renamevarp-of-renaming-fix-ren
  (equal (lstate-renamevarp old new (renaming-fix ren))
         (lstate-renamevarp old new ren)))

Theorem: lstate-renamevarp-renaming-equiv-congruence-on-ren

(defthm lstate-renamevarp-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (lstate-renamevarp old new ren)
                  (lstate-renamevarp old new ren-equiv)))
  :rule-classes :congruence)