Induction

Induction methods can be used with induction rules to prove theorems over inductive datatypes or sets as well as recursive functions.

Note that induction typically creates multiple new subgoals: one for each base case and one for the inductive step.

Performs an induction over a free variable. Consider this example:

  lemma "a#l = [a]@l"
    apply (induct l)
    apply simp+
  done

induct tries to find a suitable induction rule. See below for details how to have it use a specific rule.

Performs an induction over a free or meta-quantified variable that should not occur among the assumptions.

  lemma "⋀a l. a#l = [a]@l"
    apply (induct_tac l)
    apply simp+
  done

induct_tac tries to find a suitable induction rule. See below for details how to have it use a specific rule.

• Theorems about recursive functions are proved by induction.
• Generalise goals for induction by
  • replacing constants with variables.
  • universally quantifying all free variables (except the induction variable itself).
• The right-hand side of an equation should (in some sense) be simpler than the left-hand side.
• Put all occurrences of the induction variable into the conclusion using $\longrightarrow$.

The induction methods can not always find a fitting induction rule. In other cases, the one found might be unsuitable to prove the current goal.

  !!TODO!!

If you have a specific induction rule you want to apply—for instance one provided by an inductive definition— you can use it as you would any rule. As an example, consider the set of all even natural numbers, defined by:

  inductive_set even :: "nat set" where
    "0 ∈ even"
  | "n ∈ even ⟹ (Suc (Suc n)) ∈ even"
  

Then, Isabelle automatically generates an induction rule even.induct. If we now want to prove a theorem like

$\quad n \in \text{even}\ \Longrightarrow 2\ \text{dvd}\ n$

a reasonable approach is to do an induction over all even numbers; this can be done by

  apply (erule even.induct)