Table of Contents

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.

induct

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.

induct_tac

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.

Heuristics

Custom Rules

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!!

Applying Induction Rules By Hand

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)