		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-termination-thm

Generate the version of the termination theorem tailored to the limits and measure function.

Signature
(atc-gen-loop-termination-thm fn measure-of-fn measure-formals natp-of-measure-of-fn-thm names-to-avoid state) → (mv erp event name updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; measure-of-fn — Guard (symbolp measure-of-fn).; measure-formals — Guard (symbol-listp measure-formals).; natp-of-measure-of-fn-thm — Guard (symbolp natp-of-measure-of-fn-thm).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: event — Type (pseudo-event-formp event).; name — Type (symbolp name).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

We generate a local theorem that is just like the termination theorem of the function except that o< is replaced with <, and that the measure terms are abstracted to calls of the generated measure functions. The theorem is proved using the fact that the measure yields a natural number, which means that o< reduces to < (see above). The purpose of this variant of the termination theorem is to help establish the induction hypothesis in the loop correctness theorem, as explained below.

Definitions and Theorems

Function: atc-gen-loop-termination-thm

(defun atc-gen-loop-termination-thm
       (fn measure-of-fn measure-formals
           natp-of-measure-of-fn-thm
           names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fn)
                             (symbolp measure-of-fn)
                             (symbol-listp measure-formals)
                             (symbolp natp-of-measure-of-fn-thm)
                             (symbol-listp names-to-avoid))))
 (declare (xargs :guard (and (function-symbolp fn (w state))
                             (logicp fn (w state))
                             (irecursivep+ fn (w state))
                             (not (eq measure-of-fn 'quote)))))
 (let ((__function__ 'atc-gen-loop-termination-thm))
  (declare (ignorable __function__))
  (b*
   (((reterr) '(_) nil nil)
    (wrld (w state))
    (termination-of-fn-thm (packn-pos (list 'termination-of- fn)
                                      fn))
    ((mv termination-of-fn-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix termination-of-fn-thm
                                        nil names-to-avoid wrld))
    (tthm (termination-theorem$ fn state))
    ((when (eq (car tthm) :failed))
     (reterr
      (raise
           "Internal error: cannot find termination theorem of ~x0."
           fn)))
    ((erp tthm-formula)
     (atc-gen-loop-tthm-formula
          tthm
          fn measure-of-fn measure-formals state))
    ((mv termination-of-fn-thm-event &)
     (evmac-generate-defthm
      termination-of-fn-thm
      :formula tthm-formula
      :rule-classes nil
      :hints
      (cons
       (cons
        '"Goal"
        (cons
         ':use
         (cons
          (cons (cons ':termination-theorem
                      (cons fn 'nil))
                (cons natp-of-measure-of-fn-thm 'nil))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons measure-of-fn
                    '(acl2::natp-compound-recognizer o-p o-finp o<))
              'nil))
            'nil)))))
       'nil))))
   (retok termination-of-fn-thm-event
          termination-of-fn-thm names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-loop-termination-thm.event

(defthm pseudo-event-formp-of-atc-gen-loop-termination-thm.event
  (b*
    (((mv acl2::?erp acl2::?event
          ?name ?updated-names-to-avoid)
      (atc-gen-loop-termination-thm fn measure-of-fn measure-formals
                                    natp-of-measure-of-fn-thm
                                    names-to-avoid state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-loop-termination-thm.name

(defthm symbolp-of-atc-gen-loop-termination-thm.name
  (b*
    (((mv acl2::?erp acl2::?event
          ?name ?updated-names-to-avoid)
      (atc-gen-loop-termination-thm fn measure-of-fn measure-formals
                                    natp-of-measure-of-fn-thm
                                    names-to-avoid state)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop-termination-thm.updated-names-to-avoid

(defthm
 symbol-listp-of-atc-gen-loop-termination-thm.updated-names-to-avoid
 (implies
   (symbol-listp names-to-avoid)
   (b*
    (((mv acl2::?erp acl2::?event
          ?name ?updated-names-to-avoid)
      (atc-gen-loop-termination-thm fn measure-of-fn measure-formals
                                    natp-of-measure-of-fn-thm
                                    names-to-avoid state)))
    (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)