		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Add-frame

Add a frame to a canonical representation of computation states.

Signature
(add-frame fun compst) → new-compst
Arguments: fun — Guard (identp fun).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

This adds a frame with an empty scope.

Definitions and Theorems

Function: add-frame

(defun add-frame (fun compst)
  (declare (xargs :guard (and (identp fun)
                              (compustatep compst))))
  (let ((__function__ 'add-frame))
    (declare (ignorable __function__))
    (push-frame (make-frame :function fun
                            :scopes (list nil))
                compst)))

Theorem: compustatep-of-add-frame

(defthm compustatep-of-add-frame
  (b* ((new-compst (add-frame fun compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: add-frame-of-ident-fix-fun

(defthm add-frame-of-ident-fix-fun
  (equal (add-frame (ident-fix fun) compst)
         (add-frame fun compst)))

Theorem: add-frame-ident-equiv-congruence-on-fun

(defthm add-frame-ident-equiv-congruence-on-fun
  (implies (ident-equiv fun fun-equiv)
           (equal (add-frame fun compst)
                  (add-frame fun-equiv compst)))
  :rule-classes :congruence)

Theorem: add-frame-of-compustate-fix-compst

(defthm add-frame-of-compustate-fix-compst
  (equal (add-frame fun (compustate-fix compst))
         (add-frame fun compst)))

Theorem: add-frame-compustate-equiv-congruence-on-compst

(defthm add-frame-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (add-frame fun compst)
                  (add-frame fun compst-equiv)))
  :rule-classes :congruence)