B.3.4 induction: Perform Mathematical Induction

B.3.4 induction: Perform Mathematical Induction

Synopsis

Alternative Invocations

• Formula Menu [F]: induction ... in F

Applicable

In proving mode.

Description

The command applies the principle of mathematical induction to a universally quantified goal with a natural number variable, i.e., a variable with type NAT (but see below for the potential application of the command to an integer variable). If the proof state has a single goal with a single universally quantified natural number variable, the command form induction selects this goal and its variable for performing the induction. If the proof state has a single goal with multiple universally quantified variables, the command form induction I selects the variable with name I. If the proof state has multiple goals, the command form induction I in F selects the goal with label F and the variable I in this goal. If I does not denote a natural number variable or F does not denote a universally quantified goal with such a variable, the command has no effect.

Otherwise, the command creates two child states which are identical to the current state with the following exceptions:

1. The first child state (the induction base) instantiates the variable in the goal by the number 0.
2. The second child state (the induction step) has as an additional assumption the original goal with the variable instantiated by a constant a not occurring in the environment of the current proof state and instantiates the variable in the goal by the term a+1.

If the quantified goal only has a single variable, the quantifier is dropped from the instantiated versions. The command thus implements the following rule:

[E] ... |- ..., /\ ...: G[0/x], ...
[E,a:N] ..., /\ ...: G[a/x] |- ..., /\ ...: G[a+1/x], ...
~\/ T: [E] |- a:T
---------------------------------------------------------
[E] ... |- ..., /\ x in N, ...: G, ...

The command may also be applied to an integer variable, i.e., a variable with type INT. In this case, a third goal is created which ensures the validity of the application of the induction principle by proving that the original goal can be proved by only considering non-negative integer values for the variable according to the following rule:

[E] ... |- ..., /\ ...: G[0/x], ...
[E,a:N] ..., /\ ...: G[a/x] |- ..., /\ ...: G[a+1/x], ...
[E] ..., /\ x in Z, ...: x >= 0 => G |- /\ x in Z: G
~\/ T: [E] |- a:T
---------------------------------------------------------
[E] ... |- ..., \/ x in Z, ...: G, ...

Pragmatics

For better readability, the name of the induction constant a is derived from the name of the bound variable x by appending some natural number subscript (x₀, x₁, ...) respectively by replacing an already existing subscript.

B.3.4 induction: Perform Mathematical Induction