Isabelle/HOL Support Wiki

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== 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 =====
  * 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$.

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

$\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)
Isabelle/HOL Support Wiki

User Tools

Site Tools

Page Tools
