		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-tthm-formula

Generate the formula for the loop termination theorem.

Signature
(atc-gen-loop-tthm-formula term fn measure-of-fn measure-formals state) → (mv erp new-term)
Arguments: term — Guard (pseudo-termp term).; fn — Guard (symbolp fn).; measure-of-fn — Guard (symbolp measure-of-fn).; measure-formals — Guard (symbol-listp measure-formals).

This is obtained from the loop function's termination theorem, transformed as follows.

The o< relation is replaced with <. This is justified by the fact that the measure yields a natural number, as guaranteed by the applicability condition.

Furthermore, the measure term is replaced with a call of the generated measure function. More precisely, this is done in every term of the form (o< A B) (at the same replacing o< with < as mentioned above), where we expect B to be the measure term, and A to be the instantiation of the measure term to one of the recursive calls of the loop function. We replace B with a generic call of the measure function, and A with an instantiated call of the measure function; we obtain the instantiation by matching B to A. It is not yet clear whether this approach will work in all cases.

Theorem: len-of-atc-gen-loop-tthm-formula

(defthm len-of-atc-gen-loop-tthm-formula
  (b* nil t)
  :rule-classes nil)

Theorem: len-of-atc-gen-loop-tthm-formula-lst

(defthm len-of-atc-gen-loop-tthm-formula-lst
  (b* (((mv acl2::?erp ?new-terms)
        (atc-gen-loop-tthm-formula-lst
             terms fn
             measure-of-fn measure-formals state)))
    (implies (not erp)
             (equal (len new-terms) (len terms)))))

Theorem: pseudo-termp-of-atc-gen-loop-tthm-formula

(defthm pseudo-termp-of-atc-gen-loop-tthm-formula
  (implies (and (pseudo-termp term)
                (symbolp measure-of-fn)
                (not (eq measure-of-fn 'quote))
                (symbol-listp measure-formals))
           (b* (((mv acl2::?erp ?new-term)
                 (atc-gen-loop-tthm-formula
                      term fn
                      measure-of-fn measure-formals state)))
             (pseudo-termp new-term))))

Theorem: pseudo-termp-of-atc-gen-loop-tthm-formula-lst

(defthm pseudo-termp-of-atc-gen-loop-tthm-formula-lst
  (implies (and (pseudo-term-listp terms)
                (symbolp measure-of-fn)
                (not (eq measure-of-fn 'quote))
                (symbol-listp measure-formals))
           (b* (((mv acl2::?erp ?new-terms)
                 (atc-gen-loop-tthm-formula-lst
                      terms fn
                      measure-of-fn measure-formals state)))
             (pseudo-term-listp new-terms))))

Subtopics

Atc-gen-loop-tthm-formula-lst