INDUCT_TAC : tactic
STRUCTURE
numLib
SYNOPSIS
Performs tactical proof by mathematical induction on the natural numbers.
DESCRIPTION
INDUCT_TAC reduces a goal !n.P[n], where n has type num, to two subgoals corresponding to the base and step cases in a proof by mathematical induction on n. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of INDUCT_TAC is: 
                A ?- !n. P
    ========================================  INDUCT_TAC
     A ?- P[0/n]     A u {P} ?- P[SUC n'/n]
where n' is a primed variant of n that does not appear free in the assumptions A (usually, n' just equals n). When INDUCT_TAC is applied to a goal of the form !n.P, where n does not appear free in P, the subgoals are just A ?- P and A u {P} ?- P.
FAILURE
INDUCT_TAC g fails unless the conclusion of the goal g has the form !n.t, where the variable n has type num.
HOL  Kananaskis-13