Differences

This shows you the differences between two versions of the page.

--- reference:induct [2011/07/13 12:37] – created 131.246.161.187
+++ reference:induct [2011/07/13 12:52] (current) – 131.246.161.187
@@ Line 12: / Line 12: @@
       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 =====
@@ Line 20: / Line 22: @@
       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 =====
@@ Line 28: / Line 32: @@
   * 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)