This shows you the differences between two versions of the page.
reference:induct [2011/07/13 12:37] 131.246.161.187 created |
reference:induct [2011/07/13 12:52] (current) 131.246.161.187 |
||
---|---|---|---|
Line 12: | Line 12: | ||
apply simp+ | apply simp+ | ||
done | done | ||
+ | |||
+ | ''induct'' tries to find a suitable induction rule. See below for details how to have it use a specific rule. | ||
===== induct_tac ===== | ===== induct_tac ===== | ||
Line 20: | Line 22: | ||
apply simp+ | apply simp+ | ||
done | done | ||
+ | |||
+ | ''induct_tac'' tries to find a suitable induction rule. See below for details how to have it use a specific rule. | ||
===== Heuristics ===== | ===== Heuristics ===== | ||
Line 28: | Line 32: | ||
* The right-hand side of an equation should (in some sense) be simpler than the left-hand side. | * 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$. | * 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) |