User Tools
reference:induct
Differences
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) | ||
reference/induct.1310553454.txt.gz · Last modified: 2011/07/13 12:37 by 131.246.161.187
Page Tools
