1\DOC INDUCT_TAC
2
3\TYPE {INDUCT_TAC : tactic}
4
5\SYNOPSIS
6Performs tactical proof by mathematical induction on the natural numbers.
7
8\KEYWORDS
9tactic, induction.
10
11\DESCRIBE
12{INDUCT_TAC} reduces a goal {!n.P[n]}, where {n} has type {num}, to two
13subgoals corresponding to the base and step cases in a proof by mathematical
14induction on {n}. The induction hypothesis appears among the assumptions of the
15subgoal for the step case.  The specification of {INDUCT_TAC} is:
16{
17                A ?- !n. P
18    ========================================  INDUCT_TAC
19     A ?- P[0/n]     A u {P} ?- P[SUC n'/n]
20}
21where {n'} is a primed variant of {n} that does not appear free in
22the assumptions {A} (usually, {n'} just equals {n}). When {INDUCT_TAC} is
23applied to a goal of the form {!n.P}, where {n} does not appear free in {P},
24the subgoals are just {A ?- P} and {A u {P} ?- P}.
25
26\FAILURE
27{INDUCT_TAC g} fails unless the conclusion of the goal {g} has the form {!n.t},
28where the variable {n} has type {num}.
29
30\ENDDOC
31