|
|
|---|
|
|
|
|---|
In a term that represents the body of a loop, replace each recursive call with a term that returns the affected variables.
(atc-loop-body-term-subst term fn affect) → new-term
This is needed to express the correctness theorem for the loop body. The theorem needs to relate the execution of the loop body statement to the ACL2 term that represents it. However, the latter has recursive calls in it, which we therefore replace with terms that just return the affected variables. This ACL2 function does that. This gives us the appropriate ACL2 term to relate to the execution of the loop body statement, because the execution of the loop body statement just ends with the affected variables, i.e. it does not go back to the loop, which would be the equivalent of making the recursive call.
Note that we apply the substitution without regard to lambda variables, because we only use this ACL2 function on terms that satisfy the restrictions for loop body terms described in the user documentation. In particular, this means that the recursive calls are always on the formals of the loop function, and the affected variables also always have the same meaning.
Theorem:
(defthm return-type-of-atc-loop-body-term-subst.new-term (b* ((?new-term (atc-loop-body-term-subst term fn affect))) (pseudo-termp new-term)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-atc-loop-body-term-subst-lst.new-terms (b* ((?new-terms (atc-loop-body-term-subst-lst terms fn affect))) (pseudo-term-listp new-terms)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atc-loop-body-term-subst-lst (b* ((?new-terms (atc-loop-body-term-subst-lst terms fn affect))) (equal (len new-terms) (len terms))))