		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Termination-theorem$

A logic-mode guard-verified version of the built-in termination-theorem.

Signature
(termination-theorem$ fn state) → term?
Arguments: fn — Guard (symbolp fn).
Returns: term? — Type (or (and (consp term?) (equal (car term?) :failed) (msgp (cdr term?))) (symbolp term?) (and (consp term?) (not (equal (car term?) :failed)) (pseudo-termp term?))) .

We use magic-ev-fncall to call termination-theorem, and check that the result is either a term or a pair (:failed . msg) where msg is an error message. We check the returned value, so that we can have a return type theorem. Hard errors happening in termination-theorem are not suppressed, i.e. cause termination-theorem$ to stop with those hard errors. If magic-ev-fncall fails, or if the result is not a symbol, we also stop with hard errors.

Compared to termination-theorem, this utility requires a state argument. It may also be slightly less efficient due the magic-ev-fncall overhead. However, it can be used in logic-mode guard-verified code that follows a statically typed discipline.

Definitions and Theorems

Function: termination-theorem$

(defun termination-theorem$ (fn state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbolp fn)))
  (declare (xargs :guard (and (function-symbolp fn (w state))
                              (logicp fn (w state)))))
  (let ((__function__ 'termination-theorem$))
    (declare (ignorable __function__))
    (b* (((mv erp term?)
          (magic-ev-fncall 'termination-theorem
                           (list fn (w state))
                           state nil t))
         ((when erp)
          (raise "Internal error: ~@0" term?)
          (cons :failed ""))
         ((unless (and (consp term?)
                       (or (and (equal (car term?) :failed)
                                (msgp (cdr term?)))
                           (and (not (equal (car term?) :failed))
                                (pseudo-termp term?)))))
          (raise "Internal error: ~x0 is malformed."
                 term?)
          (cons :failed "")))
      term?)))

Theorem: return-type-of-termination-theorem$

(defthm return-type-of-termination-theorem$
  (b* ((term? (termination-theorem$ fn state)))
    (or (and (consp term?)
             (equal (car term?) :failed)
             (msgp (cdr term?)))
        (symbolp term?)
        (and (consp term?)
             (not (equal (car term?) :failed))
             (pseudo-termp term?))))
  :rule-classes :rewrite)

Theorem: consp-of-termination-theorem$

(defthm consp-of-termination-theorem$
  (b* ((term? (termination-theorem$ fn state)))
    (consp term?))
  :rule-classes :type-prescription)

Theorem: msgp-of-termination-theorem-when-failed

(defthm msgp-of-termination-theorem-when-failed
  (b* ((?term? (termination-theorem$ fn state)))
    (implies (equal (car term?) :failed)
             (msgp (cdr term?)))))

Theorem: msgp-of-termination-theorem-when-not-failed

(defthm msgp-of-termination-theorem-when-not-failed
  (b* ((?term? (termination-theorem$ fn state)))
    (implies (not (equal (car term?) :failed))
             (pseudo-termp term?))))