		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Induction-machine+

Enhanced variant of induction-machine.

Signature
(induction-machine+ fn wrld) → result
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: result — Type (pseudo-tests-and-calls-listp result).

This returns the same result as induction-machine, but it includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a singly recursive logic-mode function; the reason for ensuring logic-mode is that recursive program-mode functions do not have a measure; the reason for ensuring single recursion is that only singly-recursive functions have an induction machine.

Definitions and Theorems

Function: induction-machine+

(defun induction-machine+ (fn wrld)
 (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
 (let ((__function__ 'induction-machine+))
  (declare (ignorable __function__))
  (if (not (= (len (irecursivep+ fn wrld)) 1))
      (raise "The function ~x0 is not singly recursive."
             fn)
   (b* ((result (induction-machine fn wrld)))
    (if (pseudo-tests-and-calls-listp result)
        result
     (raise
      "Internal error: ~
                the INDUCTION-MACHINE property ~x0 of ~x1 ~
                does not have the expected form."
      result fn))))))

Theorem: pseudo-tests-and-calls-listp-of-induction-machine+

(defthm pseudo-tests-and-calls-listp-of-induction-machine+
  (b* ((result (induction-machine+ fn wrld)))
    (pseudo-tests-and-calls-listp result))
  :rule-classes :rewrite)