		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Gin-update

Update a gin with a gout.

Signature
(gin-update gin gout) → new-gin
Arguments: gin — Guard (ginp gin).; gout — Guard (goutp gout).
Returns: new-gin — Type (ginp new-gin).

The list of theorems generated so far and the index for unique theorem names are threaded through the transformation functions; both are common components of gin and gout. This function updates an input (to the next call of a transformation function) with an output (from the previous call of a transformation function), by updating those common components.

Although both gin and gout have a vartys component, that one is not threaded through; it is handled differently (see the transformation functions). Thus, this function does not involve that component.

Definitions and Theorems

Function: gin-update

(defun gin-update (gin gout)
  (declare (xargs :guard (and (ginp gin) (goutp gout))))
  (let ((__function__ 'gin-update))
    (declare (ignorable __function__))
    (b* (((gout gout) gout))
      (change-gin gin
                  :events gout.events
                  :thm-index gout.thm-index))))

Theorem: ginp-of-gin-update

(defthm ginp-of-gin-update
  (b* ((new-gin (gin-update gin gout)))
    (ginp new-gin))
  :rule-classes :rewrite)

Theorem: gin-update-of-gin-fix-gin

(defthm gin-update-of-gin-fix-gin
  (equal (gin-update (gin-fix gin) gout)
         (gin-update gin gout)))

Theorem: gin-update-gin-equiv-congruence-on-gin

(defthm gin-update-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (gin-update gin gout)
                  (gin-update gin-equiv gout)))
  :rule-classes :congruence)

Theorem: gin-update-of-gout-fix-gout

(defthm gin-update-of-gout-fix-gout
  (equal (gin-update gin (gout-fix gout))
         (gin-update gin gout)))

Theorem: gin-update-gout-equiv-congruence-on-gout

(defthm gin-update-gout-equiv-congruence-on-gout
  (implies (gout-equiv gout gout-equiv)
           (equal (gin-update gin gout)
                  (gin-update gin gout-equiv)))
  :rule-classes :congruence)