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.
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.
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
a reasonable approach is to do an induction over all even numbers; this can be done by
apply (erule even.induct)