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