Make a rule that suggests a certain induction

Example: (defthm recursion-by-sub2-induction-rule t :rule-classes ((:induction :pattern (* 1/2 i) :condition (and (integerp i) (>= i 0)) :scheme (recursion-by-sub2 i))))

In ACL2, as in Nqthm, the functions in a conjecture ``suggest'' the inductions considered by the system. Because every recursively defined function must be admitted with a justification in terms of a measure that decreases in a well-founded way on a given set of ``controlling'' arguments, every recursive definition suggests a dual induction scheme that ``unwinds'' the function from a given application. The case analysis in the induction scheme suggested by a function call is determined by the case analysis used to prove termination. That case analysis chooses a subset of the tests governing recursive calls and then generates base cases for the combinations of tests that do not lead to recursive calls and induction steps for the combinations that do. See rulers and induction-coarse-v-fine-grained.

For example, since `append` (actually `binary-append`, but
we'll ignore the distinction here) decomposes its first argument by successive
`cdr`s as long as it is a cons, the induction scheme suggested by
`append`. Observe that
an induction scheme is suggested by a recursive function application only if
the controlling actuals are distinct variables, a condition that is sufficient
to ensure that the ``substitution'' used to create the induction hypothesis is
indeed a substitution and that it drives down a certain measure. In
particular, `append` because the induction scheme suggested by

Once ACL2 has collected together all the suggested induction schemes it massages them in various ways, combining some to simultaneously unwind certain cliques of functions and vetoing others because they ``flaw'' others. We do not further discuss the induction heuristics here; the interested reader should see induction-heuristics.

However, unlike Nqthm, ACL2 provides a means by which the user can
elaborate the rules under which function applications suggest induction
schemes. Such rules are called `defthm`.

Technically we are ``overloading'' `defthm` by using it in the
creation of `defthm` is generally used to create rules and rule-class objects are
generally used to specify the exact form of each rule, we maintain that
convention and introduce the notion of an

General Form of an :induction Lemma or Corollary: T General Form of an :induction rule-class: (:induction :pattern pat-term :condition cond-term :scheme scheme-term)

where

The induction rule created is used as follows. When an instance of the

(Remark. Unlike

Consider, for example, the example given above,

(:induction :pattern (* 1/2 i) :condition (and (integerp i) (>= i 0)) :scheme (recursion-by-sub2 i)).

In this example, we imagine that

(defun recursion-by-sub2 (i) (if (and (integerp i) (< 1 i)) (recursion-by-sub2 (- i 2)) t))

Observe that this function recursively decomposes its natural number
argument by subtracting

(and (implies (not (and (integerp i) (< 1 i))) ; base case (:p i)) (implies (and (and (integerp i) (< 1 i)) ; induction step (:p (- i 2))) (:p i)))

We can think of the base case as covering two situations. The first is
when

Suppose the above

Continuing this example one step further illustrates the utility of
`consp` argument two
`cdr`s at a time. We could then add the `cddr`.

Observe that `defthm` event, the theorem proved is
irrelevant. The easiest theorem to prove is, of course,

(defthm name T :rule-classes ((:induction :pattern pat-term :condition cond-term :scheme scheme-term)))

The name of the rule created is

Note that if

- Induction-depth-limit
- The maximum number permitted of nested inductions
- Set-induction-depth-limit!
- Set the induction-depth-limit non-
`local`ly