bossLib.Induct

STRUCTURE

SYNOPSIS

Performs structural induction, using the type of the given term.

LIBRARY

BasicProvers

DESCRIPTION

Given a term M, Induct_on attempts to perform an induction based on the type of M. The induction theorem to be used is extracted from the TypeBase database, which holds useful facts about the system’s defined types.

Induct_on can be used to specify variables that are buried in the quantifier prefix, i.e., not the leading quantified variable. Induct_on can also perform induction on non-variable terms. If M is a non-variable term that does not occur bound in the goal, then Induct_on equates M to a new variable v (one not occurring in the goal), moves all hypotheses in which free variables of M occur to the conclusion of the goal, adds the antecedent v = M, and quantifies all free variables of M before universally quantifying v and then finally inducting on v.

Induct_on may also be used to apply an induction theorem coming from declaration of a mutually recursive datatype.

FAILURE

Induct_on fails if an induction theorem corresponding to the type of M is not found in the TypeBase database.

EXAMPLE

If attempting to prove

   !x. LENGTH (REVERSE x) = LENGTH x

one can apply Induct_on `x` to begin a proof by induction on the list structure of x. In this case, Induct_on serves as an explicit version of Induct.

SEEALSO

Induct, completeInduct_on, measureInduct_on, INDUCT_THEN, Cases, Hol_datatype, g, e