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

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

• 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$.